[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : (α → ℕ) → ℤ
⊢ IsPoly f → IsPoly (-f)
[PROOFSTEP]
rw [← zero_sub]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : (α → ℕ) → ℤ
⊢ IsPoly f → IsPoly (0 - f)
[PROOFSTEP]
exact (IsPoly.const 0).sub
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : (α → ℕ) → ℤ
hf : IsPoly f
hg : IsPoly g
⊢ IsPoly (f + g)
[PROOFSTEP]
rw [← sub_neg_eq_add]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f g : (α → ℕ) → ℤ
hf : IsPoly f
hg : IsPoly g
⊢ IsPoly (f - -g)
[PROOFSTEP]
exact hf.sub hg.neg
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ AddCommGroup (Poly α)
[PROOFSTEP]
refine'
  { add := ((· + ·) : Poly α → Poly α → Poly α)
    neg := (Neg.neg : Poly α → Poly α)
    sub := Sub.sub
    zero := 0
    zsmul := @zsmulRec _ ⟨(0 : Poly α)⟩ ⟨(· + ·)⟩ ⟨Neg.neg⟩
    nsmul := @nsmulRec _ ⟨(0 : Poly α)⟩ ⟨(· + ·)⟩ .. }
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (a b c : Poly α), a + b + c = a + (b + c)
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (a : Poly α), 0 + a = a
case refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (a : Poly α), a + 0 = a
case refine'_4
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (x : Poly α), nsmulRec 0 x = 0
case refine'_5
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (n : ℕ) (x : Poly α), nsmulRec (n + 1) x = x + nsmulRec n x
case refine'_6
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (a b : Poly α), a - b = a + -b
case refine'_7
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (a : Poly α), zsmulRec 0 a = 0
case refine'_8
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (n : ℕ) (a : Poly α), zsmulRec (Int.ofNat (succ n)) a = a + zsmulRec (Int.ofNat n) a
case refine'_9
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (n : ℕ) (a : Poly α), zsmulRec (Int.negSucc n) a = -zsmulRec (↑(succ n)) a
case refine'_10
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (a : Poly α), -a + a = 0
case refine'_11 α : Type u_1 β : Type u_2 γ : Type u_3 ⊢ ∀ (a b : Poly α), a + b = b + a
[PROOFSTEP]
all_goals
  intros
  first
  | rfl
  | ext; simp_rw [add_apply]
    first
    | rw [← add_assoc]
    | rw [zero_apply, zero_add]
    | rw [zero_apply, add_zero]
    | rw [neg_apply, add_left_neg, zero_apply]
    | rw [add_comm]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (a b c : Poly α), a + b + c = a + (b + c)
[PROOFSTEP]
intros
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ b✝ c✝ : Poly α
⊢ a✝ + b✝ + c✝ = a✝ + (b✝ + c✝)
[PROOFSTEP]
first
| rfl
| ext; simp_rw [add_apply]
  first
  | rw [← add_assoc]
  | rw [zero_apply, zero_add]
  | rw [zero_apply, add_zero]
  | rw [neg_apply, add_left_neg, zero_apply]
  | rw [add_comm]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ b✝ c✝ : Poly α
⊢ a✝ + b✝ + c✝ = a✝ + (b✝ + c✝)
[PROOFSTEP]
rfl
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ b✝ c✝ : Poly α
⊢ a✝ + b✝ + c✝ = a✝ + (b✝ + c✝)
[PROOFSTEP]
ext
[GOAL]
case refine'_1.a
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ b✝ c✝ : Poly α
x✝ : α → ℕ
⊢ ↑(a✝ + b✝ + c✝) x✝ = ↑(a✝ + (b✝ + c✝)) x✝
[PROOFSTEP]
simp_rw [add_apply]
[GOAL]
case refine'_1.a
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ b✝ c✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ + ↑b✝ x✝ + ↑c✝ x✝ = ↑a✝ x✝ + (↑b✝ x✝ + ↑c✝ x✝)
[PROOFSTEP]
first
| rw [← add_assoc]
| rw [zero_apply, zero_add]
| rw [zero_apply, add_zero]
| rw [neg_apply, add_left_neg, zero_apply]
| rw [add_comm]
[GOAL]
case refine'_1.a
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ b✝ c✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ + ↑b✝ x✝ + ↑c✝ x✝ = ↑a✝ x✝ + (↑b✝ x✝ + ↑c✝ x✝)
[PROOFSTEP]
rw [← add_assoc]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (a : Poly α), 0 + a = a
[PROOFSTEP]
intros
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ : Poly α
⊢ 0 + a✝ = a✝
[PROOFSTEP]
first
| rfl
| ext; simp_rw [add_apply]
  first
  | rw [← add_assoc]
  | rw [zero_apply, zero_add]
  | rw [zero_apply, add_zero]
  | rw [neg_apply, add_left_neg, zero_apply]
  | rw [add_comm]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ : Poly α
⊢ 0 + a✝ = a✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ : Poly α
⊢ 0 + a✝ = a✝
[PROOFSTEP]
ext
[GOAL]
case refine'_2.a
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑(0 + a✝) x✝ = ↑a✝ x✝
[PROOFSTEP]
simp_rw [add_apply]
[GOAL]
case refine'_2.a
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑0 x✝ + ↑a✝ x✝ = ↑a✝ x✝
[PROOFSTEP]
first
| rw [← add_assoc]
| rw [zero_apply, zero_add]
| rw [zero_apply, add_zero]
| rw [neg_apply, add_left_neg, zero_apply]
| rw [add_comm]
[GOAL]
case refine'_2.a
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑0 x✝ + ↑a✝ x✝ = ↑a✝ x✝
[PROOFSTEP]
rw [← add_assoc]
[GOAL]
case refine'_2.a
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑0 x✝ + ↑a✝ x✝ = ↑a✝ x✝
[PROOFSTEP]
rw [zero_apply, zero_add]
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (a : Poly α), a + 0 = a
[PROOFSTEP]
intros
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ : Poly α
⊢ a✝ + 0 = a✝
[PROOFSTEP]
first
| rfl
| ext; simp_rw [add_apply]
  first
  | rw [← add_assoc]
  | rw [zero_apply, zero_add]
  | rw [zero_apply, add_zero]
  | rw [neg_apply, add_left_neg, zero_apply]
  | rw [add_comm]
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ : Poly α
⊢ a✝ + 0 = a✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ : Poly α
⊢ a✝ + 0 = a✝
[PROOFSTEP]
ext
[GOAL]
case refine'_3.a
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑(a✝ + 0) x✝ = ↑a✝ x✝
[PROOFSTEP]
simp_rw [add_apply]
[GOAL]
case refine'_3.a
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ + ↑0 x✝ = ↑a✝ x✝
[PROOFSTEP]
first
| rw [← add_assoc]
| rw [zero_apply, zero_add]
| rw [zero_apply, add_zero]
| rw [neg_apply, add_left_neg, zero_apply]
| rw [add_comm]
[GOAL]
case refine'_3.a
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ + ↑0 x✝ = ↑a✝ x✝
[PROOFSTEP]
rw [← add_assoc]
[GOAL]
case refine'_3.a
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ + ↑0 x✝ = ↑a✝ x✝
[PROOFSTEP]
rw [zero_apply, zero_add]
[GOAL]
case refine'_3.a
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ + ↑0 x✝ = ↑a✝ x✝
[PROOFSTEP]
rw [zero_apply, add_zero]
[GOAL]
case refine'_4
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (x : Poly α), nsmulRec 0 x = 0
[PROOFSTEP]
intros
[GOAL]
case refine'_4
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : Poly α
⊢ nsmulRec 0 x✝ = 0
[PROOFSTEP]
first
| rfl
| ext; simp_rw [add_apply]
  first
  | rw [← add_assoc]
  | rw [zero_apply, zero_add]
  | rw [zero_apply, add_zero]
  | rw [neg_apply, add_left_neg, zero_apply]
  | rw [add_comm]
[GOAL]
case refine'_4
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : Poly α
⊢ nsmulRec 0 x✝ = 0
[PROOFSTEP]
rfl
[GOAL]
case refine'_5
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (n : ℕ) (x : Poly α), nsmulRec (n + 1) x = x + nsmulRec n x
[PROOFSTEP]
intros
[GOAL]
case refine'_5
α : Type u_1
β : Type u_2
γ : Type u_3
n✝ : ℕ
x✝ : Poly α
⊢ nsmulRec (n✝ + 1) x✝ = x✝ + nsmulRec n✝ x✝
[PROOFSTEP]
first
| rfl
| ext; simp_rw [add_apply]
  first
  | rw [← add_assoc]
  | rw [zero_apply, zero_add]
  | rw [zero_apply, add_zero]
  | rw [neg_apply, add_left_neg, zero_apply]
  | rw [add_comm]
[GOAL]
case refine'_5
α : Type u_1
β : Type u_2
γ : Type u_3
n✝ : ℕ
x✝ : Poly α
⊢ nsmulRec (n✝ + 1) x✝ = x✝ + nsmulRec n✝ x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_6
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (a b : Poly α), a - b = a + -b
[PROOFSTEP]
intros
[GOAL]
case refine'_6
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ b✝ : Poly α
⊢ a✝ - b✝ = a✝ + -b✝
[PROOFSTEP]
first
| rfl
| ext; simp_rw [add_apply]
  first
  | rw [← add_assoc]
  | rw [zero_apply, zero_add]
  | rw [zero_apply, add_zero]
  | rw [neg_apply, add_left_neg, zero_apply]
  | rw [add_comm]
[GOAL]
case refine'_6
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ b✝ : Poly α
⊢ a✝ - b✝ = a✝ + -b✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_7
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (a : Poly α), zsmulRec 0 a = 0
[PROOFSTEP]
intros
[GOAL]
case refine'_7
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ : Poly α
⊢ zsmulRec 0 a✝ = 0
[PROOFSTEP]
first
| rfl
| ext; simp_rw [add_apply]
  first
  | rw [← add_assoc]
  | rw [zero_apply, zero_add]
  | rw [zero_apply, add_zero]
  | rw [neg_apply, add_left_neg, zero_apply]
  | rw [add_comm]
[GOAL]
case refine'_7
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ : Poly α
⊢ zsmulRec 0 a✝ = 0
[PROOFSTEP]
rfl
[GOAL]
case refine'_8
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (n : ℕ) (a : Poly α), zsmulRec (Int.ofNat (succ n)) a = a + zsmulRec (Int.ofNat n) a
[PROOFSTEP]
intros
[GOAL]
case refine'_8
α : Type u_1
β : Type u_2
γ : Type u_3
n✝ : ℕ
a✝ : Poly α
⊢ zsmulRec (Int.ofNat (succ n✝)) a✝ = a✝ + zsmulRec (Int.ofNat n✝) a✝
[PROOFSTEP]
first
| rfl
| ext; simp_rw [add_apply]
  first
  | rw [← add_assoc]
  | rw [zero_apply, zero_add]
  | rw [zero_apply, add_zero]
  | rw [neg_apply, add_left_neg, zero_apply]
  | rw [add_comm]
[GOAL]
case refine'_8
α : Type u_1
β : Type u_2
γ : Type u_3
n✝ : ℕ
a✝ : Poly α
⊢ zsmulRec (Int.ofNat (succ n✝)) a✝ = a✝ + zsmulRec (Int.ofNat n✝) a✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_9
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (n : ℕ) (a : Poly α), zsmulRec (Int.negSucc n) a = -zsmulRec (↑(succ n)) a
[PROOFSTEP]
intros
[GOAL]
case refine'_9
α : Type u_1
β : Type u_2
γ : Type u_3
n✝ : ℕ
a✝ : Poly α
⊢ zsmulRec (Int.negSucc n✝) a✝ = -zsmulRec (↑(succ n✝)) a✝
[PROOFSTEP]
first
| rfl
| ext; simp_rw [add_apply]
  first
  | rw [← add_assoc]
  | rw [zero_apply, zero_add]
  | rw [zero_apply, add_zero]
  | rw [neg_apply, add_left_neg, zero_apply]
  | rw [add_comm]
[GOAL]
case refine'_9
α : Type u_1
β : Type u_2
γ : Type u_3
n✝ : ℕ
a✝ : Poly α
⊢ zsmulRec (Int.negSucc n✝) a✝ = -zsmulRec (↑(succ n✝)) a✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_10
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (a : Poly α), -a + a = 0
[PROOFSTEP]
intros
[GOAL]
case refine'_10
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ : Poly α
⊢ -a✝ + a✝ = 0
[PROOFSTEP]
first
| rfl
| ext; simp_rw [add_apply]
  first
  | rw [← add_assoc]
  | rw [zero_apply, zero_add]
  | rw [zero_apply, add_zero]
  | rw [neg_apply, add_left_neg, zero_apply]
  | rw [add_comm]
[GOAL]
case refine'_10
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ : Poly α
⊢ -a✝ + a✝ = 0
[PROOFSTEP]
rfl
[GOAL]
case refine'_10
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ : Poly α
⊢ -a✝ + a✝ = 0
[PROOFSTEP]
ext
[GOAL]
case refine'_10.a
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑(-a✝ + a✝) x✝ = ↑0 x✝
[PROOFSTEP]
simp_rw [add_apply]
[GOAL]
case refine'_10.a
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑(-a✝) x✝ + ↑a✝ x✝ = ↑0 x✝
[PROOFSTEP]
first
| rw [← add_assoc]
| rw [zero_apply, zero_add]
| rw [zero_apply, add_zero]
| rw [neg_apply, add_left_neg, zero_apply]
| rw [add_comm]
[GOAL]
case refine'_10.a
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑(-a✝) x✝ + ↑a✝ x✝ = ↑0 x✝
[PROOFSTEP]
rw [← add_assoc]
[GOAL]
case refine'_10.a
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑(-a✝) x✝ + ↑a✝ x✝ = ↑0 x✝
[PROOFSTEP]
rw [zero_apply, zero_add]
[GOAL]
case refine'_10.a
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑(-a✝) x✝ + ↑a✝ x✝ = ↑0 x✝
[PROOFSTEP]
rw [zero_apply, add_zero]
[GOAL]
case refine'_10.a
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑(-a✝) x✝ + ↑a✝ x✝ = ↑0 x✝
[PROOFSTEP]
rw [neg_apply, add_left_neg, zero_apply]
[GOAL]
case refine'_11
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (a b : Poly α), a + b = b + a
[PROOFSTEP]
intros
[GOAL]
case refine'_11
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ b✝ : Poly α
⊢ a✝ + b✝ = b✝ + a✝
[PROOFSTEP]
first
| rfl
| ext; simp_rw [add_apply]
  first
  | rw [← add_assoc]
  | rw [zero_apply, zero_add]
  | rw [zero_apply, add_zero]
  | rw [neg_apply, add_left_neg, zero_apply]
  | rw [add_comm]
[GOAL]
case refine'_11
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ b✝ : Poly α
⊢ a✝ + b✝ = b✝ + a✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_11
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ b✝ : Poly α
⊢ a✝ + b✝ = b✝ + a✝
[PROOFSTEP]
ext
[GOAL]
case refine'_11.a
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ b✝ : Poly α
x✝ : α → ℕ
⊢ ↑(a✝ + b✝) x✝ = ↑(b✝ + a✝) x✝
[PROOFSTEP]
simp_rw [add_apply]
[GOAL]
case refine'_11.a
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ b✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ + ↑b✝ x✝ = ↑b✝ x✝ + ↑a✝ x✝
[PROOFSTEP]
first
| rw [← add_assoc]
| rw [zero_apply, zero_add]
| rw [zero_apply, add_zero]
| rw [neg_apply, add_left_neg, zero_apply]
| rw [add_comm]
[GOAL]
case refine'_11.a
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ b✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ + ↑b✝ x✝ = ↑b✝ x✝ + ↑a✝ x✝
[PROOFSTEP]
rw [← add_assoc]
[GOAL]
case refine'_11.a
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ b✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ + ↑b✝ x✝ = ↑b✝ x✝ + ↑a✝ x✝
[PROOFSTEP]
rw [zero_apply, zero_add]
[GOAL]
case refine'_11.a
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ b✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ + ↑b✝ x✝ = ↑b✝ x✝ + ↑a✝ x✝
[PROOFSTEP]
rw [zero_apply, add_zero]
[GOAL]
case refine'_11.a
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ b✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ + ↑b✝ x✝ = ↑b✝ x✝ + ↑a✝ x✝
[PROOFSTEP]
rw [neg_apply, add_left_neg, zero_apply]
[GOAL]
case refine'_11.a
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ b✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ + ↑b✝ x✝ = ↑b✝ x✝ + ↑a✝ x✝
[PROOFSTEP]
rw [add_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ CommRing (Poly α)
[PROOFSTEP]
refine'
  { (inferInstance : AddCommGroup (Poly α)),
    (inferInstance : AddGroupWithOne
        (Poly α)) with
    add := ((· + ·) : Poly α → Poly α → Poly α)
    zero := 0
    mul := (· * ·)
    one := 1
    npow := @npowRec _ ⟨(1 : Poly α)⟩ ⟨(· * ·)⟩ .. }
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
⊢ ∀ (a b c : Poly α), a * (b + c) = a * b + a * c
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
⊢ ∀ (a b c : Poly α), (a + b) * c = a * c + b * c
case refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
⊢ ∀ (a : Poly α), 0 * a = 0
case refine'_4
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
⊢ ∀ (a : Poly α), a * 0 = 0
case refine'_5
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
⊢ ∀ (a b c : Poly α), a * b * c = a * (b * c)
case refine'_6
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
⊢ ∀ (a : Poly α), 1 * a = a
case refine'_7
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
⊢ ∀ (a : Poly α), a * 1 = a
case refine'_8
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
⊢ ∀ (x : Poly α), npowRec 0 x = 1
case refine'_9
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
⊢ ∀ (n : ℕ) (x : Poly α), npowRec (n + 1) x = x * npowRec n x
case refine'_10
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
⊢ ∀ (a b : Poly α), a * b = b * a
[PROOFSTEP]
all_goals
  intros
  first
  | rfl
  | ext; simp only [add_apply, mul_apply]
    first
    | rw [mul_add]
    | rw [add_mul]
    | rw [zero_apply, zero_mul]
    | rw [zero_apply, mul_zero]
    | rw [← mul_assoc]
    | rw [one_apply, one_mul]
    | rw [one_apply, mul_one]
    | rw [mul_comm]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
⊢ ∀ (a b c : Poly α), a * (b + c) = a * b + a * c
[PROOFSTEP]
intros
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ b✝ c✝ : Poly α
⊢ a✝ * (b✝ + c✝) = a✝ * b✝ + a✝ * c✝
[PROOFSTEP]
first
| rfl
| ext; simp only [add_apply, mul_apply]
  first
  | rw [mul_add]
  | rw [add_mul]
  | rw [zero_apply, zero_mul]
  | rw [zero_apply, mul_zero]
  | rw [← mul_assoc]
  | rw [one_apply, one_mul]
  | rw [one_apply, mul_one]
  | rw [mul_comm]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ b✝ c✝ : Poly α
⊢ a✝ * (b✝ + c✝) = a✝ * b✝ + a✝ * c✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ b✝ c✝ : Poly α
⊢ a✝ * (b✝ + c✝) = a✝ * b✝ + a✝ * c✝
[PROOFSTEP]
ext
[GOAL]
case refine'_1.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ b✝ c✝ : Poly α
x✝ : α → ℕ
⊢ ↑(a✝ * (b✝ + c✝)) x✝ = ↑(a✝ * b✝ + a✝ * c✝) x✝
[PROOFSTEP]
simp only [add_apply, mul_apply]
[GOAL]
case refine'_1.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ b✝ c✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ * (↑b✝ x✝ + ↑c✝ x✝) = ↑a✝ x✝ * ↑b✝ x✝ + ↑a✝ x✝ * ↑c✝ x✝
[PROOFSTEP]
first
| rw [mul_add]
| rw [add_mul]
| rw [zero_apply, zero_mul]
| rw [zero_apply, mul_zero]
| rw [← mul_assoc]
| rw [one_apply, one_mul]
| rw [one_apply, mul_one]
| rw [mul_comm]
[GOAL]
case refine'_1.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ b✝ c✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ * (↑b✝ x✝ + ↑c✝ x✝) = ↑a✝ x✝ * ↑b✝ x✝ + ↑a✝ x✝ * ↑c✝ x✝
[PROOFSTEP]
rw [mul_add]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
⊢ ∀ (a b c : Poly α), (a + b) * c = a * c + b * c
[PROOFSTEP]
intros
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ b✝ c✝ : Poly α
⊢ (a✝ + b✝) * c✝ = a✝ * c✝ + b✝ * c✝
[PROOFSTEP]
first
| rfl
| ext; simp only [add_apply, mul_apply]
  first
  | rw [mul_add]
  | rw [add_mul]
  | rw [zero_apply, zero_mul]
  | rw [zero_apply, mul_zero]
  | rw [← mul_assoc]
  | rw [one_apply, one_mul]
  | rw [one_apply, mul_one]
  | rw [mul_comm]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ b✝ c✝ : Poly α
⊢ (a✝ + b✝) * c✝ = a✝ * c✝ + b✝ * c✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ b✝ c✝ : Poly α
⊢ (a✝ + b✝) * c✝ = a✝ * c✝ + b✝ * c✝
[PROOFSTEP]
ext
[GOAL]
case refine'_2.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ b✝ c✝ : Poly α
x✝ : α → ℕ
⊢ ↑((a✝ + b✝) * c✝) x✝ = ↑(a✝ * c✝ + b✝ * c✝) x✝
[PROOFSTEP]
simp only [add_apply, mul_apply]
[GOAL]
case refine'_2.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ b✝ c✝ : Poly α
x✝ : α → ℕ
⊢ (↑a✝ x✝ + ↑b✝ x✝) * ↑c✝ x✝ = ↑a✝ x✝ * ↑c✝ x✝ + ↑b✝ x✝ * ↑c✝ x✝
[PROOFSTEP]
first
| rw [mul_add]
| rw [add_mul]
| rw [zero_apply, zero_mul]
| rw [zero_apply, mul_zero]
| rw [← mul_assoc]
| rw [one_apply, one_mul]
| rw [one_apply, mul_one]
| rw [mul_comm]
[GOAL]
case refine'_2.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ b✝ c✝ : Poly α
x✝ : α → ℕ
⊢ (↑a✝ x✝ + ↑b✝ x✝) * ↑c✝ x✝ = ↑a✝ x✝ * ↑c✝ x✝ + ↑b✝ x✝ * ↑c✝ x✝
[PROOFSTEP]
rw [mul_add]
[GOAL]
case refine'_2.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ b✝ c✝ : Poly α
x✝ : α → ℕ
⊢ (↑a✝ x✝ + ↑b✝ x✝) * ↑c✝ x✝ = ↑a✝ x✝ * ↑c✝ x✝ + ↑b✝ x✝ * ↑c✝ x✝
[PROOFSTEP]
rw [add_mul]
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
⊢ ∀ (a : Poly α), 0 * a = 0
[PROOFSTEP]
intros
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
⊢ 0 * a✝ = 0
[PROOFSTEP]
first
| rfl
| ext; simp only [add_apply, mul_apply]
  first
  | rw [mul_add]
  | rw [add_mul]
  | rw [zero_apply, zero_mul]
  | rw [zero_apply, mul_zero]
  | rw [← mul_assoc]
  | rw [one_apply, one_mul]
  | rw [one_apply, mul_one]
  | rw [mul_comm]
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
⊢ 0 * a✝ = 0
[PROOFSTEP]
rfl
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
⊢ 0 * a✝ = 0
[PROOFSTEP]
ext
[GOAL]
case refine'_3.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑(0 * a✝) x✝ = ↑0 x✝
[PROOFSTEP]
simp only [add_apply, mul_apply]
[GOAL]
case refine'_3.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑0 x✝ * ↑a✝ x✝ = ↑0 x✝
[PROOFSTEP]
first
| rw [mul_add]
| rw [add_mul]
| rw [zero_apply, zero_mul]
| rw [zero_apply, mul_zero]
| rw [← mul_assoc]
| rw [one_apply, one_mul]
| rw [one_apply, mul_one]
| rw [mul_comm]
[GOAL]
case refine'_3.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑0 x✝ * ↑a✝ x✝ = ↑0 x✝
[PROOFSTEP]
rw [mul_add]
[GOAL]
case refine'_3.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑0 x✝ * ↑a✝ x✝ = ↑0 x✝
[PROOFSTEP]
rw [add_mul]
[GOAL]
case refine'_3.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑0 x✝ * ↑a✝ x✝ = ↑0 x✝
[PROOFSTEP]
rw [zero_apply, zero_mul]
[GOAL]
case refine'_4
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
⊢ ∀ (a : Poly α), a * 0 = 0
[PROOFSTEP]
intros
[GOAL]
case refine'_4
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
⊢ a✝ * 0 = 0
[PROOFSTEP]
first
| rfl
| ext; simp only [add_apply, mul_apply]
  first
  | rw [mul_add]
  | rw [add_mul]
  | rw [zero_apply, zero_mul]
  | rw [zero_apply, mul_zero]
  | rw [← mul_assoc]
  | rw [one_apply, one_mul]
  | rw [one_apply, mul_one]
  | rw [mul_comm]
[GOAL]
case refine'_4
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
⊢ a✝ * 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case refine'_4
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
⊢ a✝ * 0 = 0
[PROOFSTEP]
ext
[GOAL]
case refine'_4.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑(a✝ * 0) x✝ = ↑0 x✝
[PROOFSTEP]
simp only [add_apply, mul_apply]
[GOAL]
case refine'_4.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ * ↑0 x✝ = ↑0 x✝
[PROOFSTEP]
first
| rw [mul_add]
| rw [add_mul]
| rw [zero_apply, zero_mul]
| rw [zero_apply, mul_zero]
| rw [← mul_assoc]
| rw [one_apply, one_mul]
| rw [one_apply, mul_one]
| rw [mul_comm]
[GOAL]
case refine'_4.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ * ↑0 x✝ = ↑0 x✝
[PROOFSTEP]
rw [mul_add]
[GOAL]
case refine'_4.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ * ↑0 x✝ = ↑0 x✝
[PROOFSTEP]
rw [add_mul]
[GOAL]
case refine'_4.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ * ↑0 x✝ = ↑0 x✝
[PROOFSTEP]
rw [zero_apply, zero_mul]
[GOAL]
case refine'_4.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ * ↑0 x✝ = ↑0 x✝
[PROOFSTEP]
rw [zero_apply, mul_zero]
[GOAL]
case refine'_5
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
⊢ ∀ (a b c : Poly α), a * b * c = a * (b * c)
[PROOFSTEP]
intros
[GOAL]
case refine'_5
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ b✝ c✝ : Poly α
⊢ a✝ * b✝ * c✝ = a✝ * (b✝ * c✝)
[PROOFSTEP]
first
| rfl
| ext; simp only [add_apply, mul_apply]
  first
  | rw [mul_add]
  | rw [add_mul]
  | rw [zero_apply, zero_mul]
  | rw [zero_apply, mul_zero]
  | rw [← mul_assoc]
  | rw [one_apply, one_mul]
  | rw [one_apply, mul_one]
  | rw [mul_comm]
[GOAL]
case refine'_5
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ b✝ c✝ : Poly α
⊢ a✝ * b✝ * c✝ = a✝ * (b✝ * c✝)
[PROOFSTEP]
rfl
[GOAL]
case refine'_5
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ b✝ c✝ : Poly α
⊢ a✝ * b✝ * c✝ = a✝ * (b✝ * c✝)
[PROOFSTEP]
ext
[GOAL]
case refine'_5.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ b✝ c✝ : Poly α
x✝ : α → ℕ
⊢ ↑(a✝ * b✝ * c✝) x✝ = ↑(a✝ * (b✝ * c✝)) x✝
[PROOFSTEP]
simp only [add_apply, mul_apply]
[GOAL]
case refine'_5.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ b✝ c✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ * ↑b✝ x✝ * ↑c✝ x✝ = ↑a✝ x✝ * (↑b✝ x✝ * ↑c✝ x✝)
[PROOFSTEP]
first
| rw [mul_add]
| rw [add_mul]
| rw [zero_apply, zero_mul]
| rw [zero_apply, mul_zero]
| rw [← mul_assoc]
| rw [one_apply, one_mul]
| rw [one_apply, mul_one]
| rw [mul_comm]
[GOAL]
case refine'_5.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ b✝ c✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ * ↑b✝ x✝ * ↑c✝ x✝ = ↑a✝ x✝ * (↑b✝ x✝ * ↑c✝ x✝)
[PROOFSTEP]
rw [mul_add]
[GOAL]
case refine'_5.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ b✝ c✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ * ↑b✝ x✝ * ↑c✝ x✝ = ↑a✝ x✝ * (↑b✝ x✝ * ↑c✝ x✝)
[PROOFSTEP]
rw [add_mul]
[GOAL]
case refine'_5.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ b✝ c✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ * ↑b✝ x✝ * ↑c✝ x✝ = ↑a✝ x✝ * (↑b✝ x✝ * ↑c✝ x✝)
[PROOFSTEP]
rw [zero_apply, zero_mul]
[GOAL]
case refine'_5.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ b✝ c✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ * ↑b✝ x✝ * ↑c✝ x✝ = ↑a✝ x✝ * (↑b✝ x✝ * ↑c✝ x✝)
[PROOFSTEP]
rw [zero_apply, mul_zero]
[GOAL]
case refine'_5.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ b✝ c✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ * ↑b✝ x✝ * ↑c✝ x✝ = ↑a✝ x✝ * (↑b✝ x✝ * ↑c✝ x✝)
[PROOFSTEP]
rw [← mul_assoc]
[GOAL]
case refine'_6
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
⊢ ∀ (a : Poly α), 1 * a = a
[PROOFSTEP]
intros
[GOAL]
case refine'_6
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
⊢ 1 * a✝ = a✝
[PROOFSTEP]
first
| rfl
| ext; simp only [add_apply, mul_apply]
  first
  | rw [mul_add]
  | rw [add_mul]
  | rw [zero_apply, zero_mul]
  | rw [zero_apply, mul_zero]
  | rw [← mul_assoc]
  | rw [one_apply, one_mul]
  | rw [one_apply, mul_one]
  | rw [mul_comm]
[GOAL]
case refine'_6
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
⊢ 1 * a✝ = a✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_6
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
⊢ 1 * a✝ = a✝
[PROOFSTEP]
ext
[GOAL]
case refine'_6.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑(1 * a✝) x✝ = ↑a✝ x✝
[PROOFSTEP]
simp only [add_apply, mul_apply]
[GOAL]
case refine'_6.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑1 x✝ * ↑a✝ x✝ = ↑a✝ x✝
[PROOFSTEP]
first
| rw [mul_add]
| rw [add_mul]
| rw [zero_apply, zero_mul]
| rw [zero_apply, mul_zero]
| rw [← mul_assoc]
| rw [one_apply, one_mul]
| rw [one_apply, mul_one]
| rw [mul_comm]
[GOAL]
case refine'_6.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑1 x✝ * ↑a✝ x✝ = ↑a✝ x✝
[PROOFSTEP]
rw [mul_add]
[GOAL]
case refine'_6.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑1 x✝ * ↑a✝ x✝ = ↑a✝ x✝
[PROOFSTEP]
rw [add_mul]
[GOAL]
case refine'_6.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑1 x✝ * ↑a✝ x✝ = ↑a✝ x✝
[PROOFSTEP]
rw [zero_apply, zero_mul]
[GOAL]
case refine'_6.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑1 x✝ * ↑a✝ x✝ = ↑a✝ x✝
[PROOFSTEP]
rw [zero_apply, mul_zero]
[GOAL]
case refine'_6.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑1 x✝ * ↑a✝ x✝ = ↑a✝ x✝
[PROOFSTEP]
rw [← mul_assoc]
[GOAL]
case refine'_6.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑1 x✝ * ↑a✝ x✝ = ↑a✝ x✝
[PROOFSTEP]
rw [one_apply, one_mul]
[GOAL]
case refine'_7
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
⊢ ∀ (a : Poly α), a * 1 = a
[PROOFSTEP]
intros
[GOAL]
case refine'_7
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
⊢ a✝ * 1 = a✝
[PROOFSTEP]
first
| rfl
| ext; simp only [add_apply, mul_apply]
  first
  | rw [mul_add]
  | rw [add_mul]
  | rw [zero_apply, zero_mul]
  | rw [zero_apply, mul_zero]
  | rw [← mul_assoc]
  | rw [one_apply, one_mul]
  | rw [one_apply, mul_one]
  | rw [mul_comm]
[GOAL]
case refine'_7
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
⊢ a✝ * 1 = a✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_7
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
⊢ a✝ * 1 = a✝
[PROOFSTEP]
ext
[GOAL]
case refine'_7.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑(a✝ * 1) x✝ = ↑a✝ x✝
[PROOFSTEP]
simp only [add_apply, mul_apply]
[GOAL]
case refine'_7.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ * ↑1 x✝ = ↑a✝ x✝
[PROOFSTEP]
first
| rw [mul_add]
| rw [add_mul]
| rw [zero_apply, zero_mul]
| rw [zero_apply, mul_zero]
| rw [← mul_assoc]
| rw [one_apply, one_mul]
| rw [one_apply, mul_one]
| rw [mul_comm]
[GOAL]
case refine'_7.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ * ↑1 x✝ = ↑a✝ x✝
[PROOFSTEP]
rw [mul_add]
[GOAL]
case refine'_7.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ * ↑1 x✝ = ↑a✝ x✝
[PROOFSTEP]
rw [add_mul]
[GOAL]
case refine'_7.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ * ↑1 x✝ = ↑a✝ x✝
[PROOFSTEP]
rw [zero_apply, zero_mul]
[GOAL]
case refine'_7.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ * ↑1 x✝ = ↑a✝ x✝
[PROOFSTEP]
rw [zero_apply, mul_zero]
[GOAL]
case refine'_7.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ * ↑1 x✝ = ↑a✝ x✝
[PROOFSTEP]
rw [← mul_assoc]
[GOAL]
case refine'_7.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ * ↑1 x✝ = ↑a✝ x✝
[PROOFSTEP]
rw [one_apply, one_mul]
[GOAL]
case refine'_7.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ * ↑1 x✝ = ↑a✝ x✝
[PROOFSTEP]
rw [one_apply, mul_one]
[GOAL]
case refine'_8
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
⊢ ∀ (x : Poly α), npowRec 0 x = 1
[PROOFSTEP]
intros
[GOAL]
case refine'_8
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
x✝ : Poly α
⊢ npowRec 0 x✝ = 1
[PROOFSTEP]
first
| rfl
| ext; simp only [add_apply, mul_apply]
  first
  | rw [mul_add]
  | rw [add_mul]
  | rw [zero_apply, zero_mul]
  | rw [zero_apply, mul_zero]
  | rw [← mul_assoc]
  | rw [one_apply, one_mul]
  | rw [one_apply, mul_one]
  | rw [mul_comm]
[GOAL]
case refine'_8
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
x✝ : Poly α
⊢ npowRec 0 x✝ = 1
[PROOFSTEP]
rfl
[GOAL]
case refine'_9
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
⊢ ∀ (n : ℕ) (x : Poly α), npowRec (n + 1) x = x * npowRec n x
[PROOFSTEP]
intros
[GOAL]
case refine'_9
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
n✝ : ℕ
x✝ : Poly α
⊢ npowRec (n✝ + 1) x✝ = x✝ * npowRec n✝ x✝
[PROOFSTEP]
first
| rfl
| ext; simp only [add_apply, mul_apply]
  first
  | rw [mul_add]
  | rw [add_mul]
  | rw [zero_apply, zero_mul]
  | rw [zero_apply, mul_zero]
  | rw [← mul_assoc]
  | rw [one_apply, one_mul]
  | rw [one_apply, mul_one]
  | rw [mul_comm]
[GOAL]
case refine'_9
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
n✝ : ℕ
x✝ : Poly α
⊢ npowRec (n✝ + 1) x✝ = x✝ * npowRec n✝ x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_10
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
⊢ ∀ (a b : Poly α), a * b = b * a
[PROOFSTEP]
intros
[GOAL]
case refine'_10
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ b✝ : Poly α
⊢ a✝ * b✝ = b✝ * a✝
[PROOFSTEP]
first
| rfl
| ext; simp only [add_apply, mul_apply]
  first
  | rw [mul_add]
  | rw [add_mul]
  | rw [zero_apply, zero_mul]
  | rw [zero_apply, mul_zero]
  | rw [← mul_assoc]
  | rw [one_apply, one_mul]
  | rw [one_apply, mul_one]
  | rw [mul_comm]
[GOAL]
case refine'_10
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ b✝ : Poly α
⊢ a✝ * b✝ = b✝ * a✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_10
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ b✝ : Poly α
⊢ a✝ * b✝ = b✝ * a✝
[PROOFSTEP]
ext
[GOAL]
case refine'_10.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ b✝ : Poly α
x✝ : α → ℕ
⊢ ↑(a✝ * b✝) x✝ = ↑(b✝ * a✝) x✝
[PROOFSTEP]
simp only [add_apply, mul_apply]
[GOAL]
case refine'_10.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ b✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ * ↑b✝ x✝ = ↑b✝ x✝ * ↑a✝ x✝
[PROOFSTEP]
first
| rw [mul_add]
| rw [add_mul]
| rw [zero_apply, zero_mul]
| rw [zero_apply, mul_zero]
| rw [← mul_assoc]
| rw [one_apply, one_mul]
| rw [one_apply, mul_one]
| rw [mul_comm]
[GOAL]
case refine'_10.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ b✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ * ↑b✝ x✝ = ↑b✝ x✝ * ↑a✝ x✝
[PROOFSTEP]
rw [mul_add]
[GOAL]
case refine'_10.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ b✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ * ↑b✝ x✝ = ↑b✝ x✝ * ↑a✝ x✝
[PROOFSTEP]
rw [add_mul]
[GOAL]
case refine'_10.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ b✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ * ↑b✝ x✝ = ↑b✝ x✝ * ↑a✝ x✝
[PROOFSTEP]
rw [zero_apply, zero_mul]
[GOAL]
case refine'_10.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ b✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ * ↑b✝ x✝ = ↑b✝ x✝ * ↑a✝ x✝
[PROOFSTEP]
rw [zero_apply, mul_zero]
[GOAL]
case refine'_10.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ b✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ * ↑b✝ x✝ = ↑b✝ x✝ * ↑a✝ x✝
[PROOFSTEP]
rw [← mul_assoc]
[GOAL]
case refine'_10.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ b✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ * ↑b✝ x✝ = ↑b✝ x✝ * ↑a✝ x✝
[PROOFSTEP]
rw [one_apply, one_mul]
[GOAL]
case refine'_10.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ b✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ * ↑b✝ x✝ = ↑b✝ x✝ * ↑a✝ x✝
[PROOFSTEP]
rw [one_apply, mul_one]
[GOAL]
case refine'_10.a
α : Type u_1
β : Type u_2
γ : Type u_3
src✝¹ : AddCommGroup (Poly α) := inferInstance
src✝ : AddGroupWithOne (Poly α) := inferInstance
a✝ b✝ : Poly α
x✝ : α → ℕ
⊢ ↑a✝ x✝ * ↑b✝ x✝ = ↑b✝ x✝ * ↑a✝ x✝
[PROOFSTEP]
rw [mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
C : Poly α → Prop
H1 : ∀ (i : α), C (proj i)
H2 : ∀ (n : ℤ), C (const n)
H3 : ∀ (f g : Poly α), C f → C g → C (f - g)
H4 : ∀ (f g : Poly α), C f → C g → C (f * g)
f : Poly α
⊢ C f
[PROOFSTEP]
cases' f with f pf
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
C : Poly α → Prop
H1 : ∀ (i : α), C (proj i)
H2 : ∀ (n : ℤ), C (const n)
H3 : ∀ (f g : Poly α), C f → C g → C (f - g)
H4 : ∀ (f g : Poly α), C f → C g → C (f * g)
f : (α → ℕ) → ℤ
pf : IsPoly f
⊢ C { val := f, property := pf }
[PROOFSTEP]
induction' pf with i n f g pf pg ihf ihg f g pf pg ihf ihg
[GOAL]
case mk.proj
α : Type u_1
β : Type u_2
γ : Type u_3
C : Poly α → Prop
H1 : ∀ (i : α), C (proj i)
H2 : ∀ (n : ℤ), C (const n)
H3 : ∀ (f g : Poly α), C f → C g → C (f - g)
H4 : ∀ (f g : Poly α), C f → C g → C (f * g)
f : (α → ℕ) → ℤ
i : α
⊢ C { val := fun x => ↑(x i), property := (_ : IsPoly fun x => ↑(x i)) }
case mk.const
α : Type u_1
β : Type u_2
γ : Type u_3
C : Poly α → Prop
H1 : ∀ (i : α), C (proj i)
H2 : ∀ (n : ℤ), C (const n)
H3 : ∀ (f g : Poly α), C f → C g → C (f - g)
H4 : ∀ (f g : Poly α), C f → C g → C (f * g)
f : (α → ℕ) → ℤ
n : ℤ
⊢ C { val := fun x => n, property := (_ : IsPoly fun x => n) }
case mk.sub
α : Type u_1
β : Type u_2
γ : Type u_3
C : Poly α → Prop
H1 : ∀ (i : α), C (proj i)
H2 : ∀ (n : ℤ), C (const n)
H3 : ∀ (f g : Poly α), C f → C g → C (f - g)
H4 : ∀ (f g : Poly α), C f → C g → C (f * g)
f✝ f g : (α → ℕ) → ℤ
pf : IsPoly f
pg : IsPoly g
ihf : C { val := f, property := pf }
ihg : C { val := g, property := pg }
⊢ C { val := fun x => f x - g x, property := (_ : IsPoly fun x => f x - g x) }
case mk.mul
α : Type u_1
β : Type u_2
γ : Type u_3
C : Poly α → Prop
H1 : ∀ (i : α), C (proj i)
H2 : ∀ (n : ℤ), C (const n)
H3 : ∀ (f g : Poly α), C f → C g → C (f - g)
H4 : ∀ (f g : Poly α), C f → C g → C (f * g)
f✝ f g : (α → ℕ) → ℤ
pf : IsPoly f
pg : IsPoly g
ihf : C { val := f, property := pf }
ihg : C { val := g, property := pg }
⊢ C { val := fun x => f x * g x, property := (_ : IsPoly fun x => f x * g x) }
[PROOFSTEP]
apply H1
[GOAL]
case mk.const
α : Type u_1
β : Type u_2
γ : Type u_3
C : Poly α → Prop
H1 : ∀ (i : α), C (proj i)
H2 : ∀ (n : ℤ), C (const n)
H3 : ∀ (f g : Poly α), C f → C g → C (f - g)
H4 : ∀ (f g : Poly α), C f → C g → C (f * g)
f : (α → ℕ) → ℤ
n : ℤ
⊢ C { val := fun x => n, property := (_ : IsPoly fun x => n) }
case mk.sub
α : Type u_1
β : Type u_2
γ : Type u_3
C : Poly α → Prop
H1 : ∀ (i : α), C (proj i)
H2 : ∀ (n : ℤ), C (const n)
H3 : ∀ (f g : Poly α), C f → C g → C (f - g)
H4 : ∀ (f g : Poly α), C f → C g → C (f * g)
f✝ f g : (α → ℕ) → ℤ
pf : IsPoly f
pg : IsPoly g
ihf : C { val := f, property := pf }
ihg : C { val := g, property := pg }
⊢ C { val := fun x => f x - g x, property := (_ : IsPoly fun x => f x - g x) }
case mk.mul
α : Type u_1
β : Type u_2
γ : Type u_3
C : Poly α → Prop
H1 : ∀ (i : α), C (proj i)
H2 : ∀ (n : ℤ), C (const n)
H3 : ∀ (f g : Poly α), C f → C g → C (f - g)
H4 : ∀ (f g : Poly α), C f → C g → C (f * g)
f✝ f g : (α → ℕ) → ℤ
pf : IsPoly f
pg : IsPoly g
ihf : C { val := f, property := pf }
ihg : C { val := g, property := pg }
⊢ C { val := fun x => f x * g x, property := (_ : IsPoly fun x => f x * g x) }
[PROOFSTEP]
apply H2
[GOAL]
case mk.sub
α : Type u_1
β : Type u_2
γ : Type u_3
C : Poly α → Prop
H1 : ∀ (i : α), C (proj i)
H2 : ∀ (n : ℤ), C (const n)
H3 : ∀ (f g : Poly α), C f → C g → C (f - g)
H4 : ∀ (f g : Poly α), C f → C g → C (f * g)
f✝ f g : (α → ℕ) → ℤ
pf : IsPoly f
pg : IsPoly g
ihf : C { val := f, property := pf }
ihg : C { val := g, property := pg }
⊢ C { val := fun x => f x - g x, property := (_ : IsPoly fun x => f x - g x) }
case mk.mul
α : Type u_1
β : Type u_2
γ : Type u_3
C : Poly α → Prop
H1 : ∀ (i : α), C (proj i)
H2 : ∀ (n : ℤ), C (const n)
H3 : ∀ (f g : Poly α), C f → C g → C (f - g)
H4 : ∀ (f g : Poly α), C f → C g → C (f * g)
f✝ f g : (α → ℕ) → ℤ
pf : IsPoly f
pg : IsPoly g
ihf : C { val := f, property := pf }
ihg : C { val := g, property := pg }
⊢ C { val := fun x => f x * g x, property := (_ : IsPoly fun x => f x * g x) }
[PROOFSTEP]
apply H3 _ _ ihf ihg
[GOAL]
case mk.mul
α : Type u_1
β : Type u_2
γ : Type u_3
C : Poly α → Prop
H1 : ∀ (i : α), C (proj i)
H2 : ∀ (n : ℤ), C (const n)
H3 : ∀ (f g : Poly α), C f → C g → C (f - g)
H4 : ∀ (f g : Poly α), C f → C g → C (f * g)
f✝ f g : (α → ℕ) → ℤ
pf : IsPoly f
pg : IsPoly g
ihf : C { val := f, property := pf }
ihg : C { val := g, property := pg }
⊢ C { val := fun x => f x * g x, property := (_ : IsPoly fun x => f x * g x) }
[PROOFSTEP]
apply H4 _ _ ihf ihg
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x : α → ℕ
p : Poly α
ps : List (Poly α)
⊢ 0 ≤ ↑(sumsq (p :: ps)) x
[PROOFSTEP]
rw [sumsq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x : α → ℕ
p : Poly α
ps : List (Poly α)
⊢ 0 ≤ ↑(p * p + sumsq ps) x
[PROOFSTEP]
exact add_nonneg (mul_self_nonneg _) (sumsq_nonneg _ ps)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x : α → ℕ
p : Poly α
ps : List (Poly α)
⊢ ↑(sumsq (p :: ps)) x = 0 ↔ List.All₂ (fun a => ↑a x = 0) (p :: ps)
[PROOFSTEP]
rw [List.all₂_cons, ← sumsq_eq_zero _ ps]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x : α → ℕ
p : Poly α
ps : List (Poly α)
⊢ ↑(sumsq (p :: ps)) x = 0 ↔ ↑p x = 0 ∧ ↑(sumsq ps) x = 0
[PROOFSTEP]
rw [sumsq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x : α → ℕ
p : Poly α
ps : List (Poly α)
⊢ ↑(p * p + sumsq ps) x = 0 ↔ ↑p x = 0 ∧ ↑(sumsq ps) x = 0
[PROOFSTEP]
exact
  ⟨fun h : p x * p x + sumsq ps x = 0 =>
    have : p x = 0 :=
      eq_zero_of_mul_self_eq_zero <|
        le_antisymm
          (by
            rw [← h]
            have t := add_le_add_left (sumsq_nonneg x ps) (p x * p x)
            rwa [add_zero] at t )
          (mul_self_nonneg _)
    ⟨this, by simp [this] at h ; exact h⟩,
    fun ⟨h1, h2⟩ => by rw [add_apply, mul_apply, h1, h2]; rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x : α → ℕ
p : Poly α
ps : List (Poly α)
h : ↑p x * ↑p x + ↑(sumsq ps) x = 0
⊢ ↑p x * ↑p x ≤ 0
[PROOFSTEP]
rw [← h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x : α → ℕ
p : Poly α
ps : List (Poly α)
h : ↑p x * ↑p x + ↑(sumsq ps) x = 0
⊢ ↑p x * ↑p x ≤ ↑p x * ↑p x + ↑(sumsq ps) x
[PROOFSTEP]
have t := add_le_add_left (sumsq_nonneg x ps) (p x * p x)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x : α → ℕ
p : Poly α
ps : List (Poly α)
h : ↑p x * ↑p x + ↑(sumsq ps) x = 0
t : ↑p x * ↑p x + 0 ≤ ↑p x * ↑p x + ↑(sumsq ps) x
⊢ ↑p x * ↑p x ≤ ↑p x * ↑p x + ↑(sumsq ps) x
[PROOFSTEP]
rwa [add_zero] at t 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x : α → ℕ
p : Poly α
ps : List (Poly α)
h : ↑p x * ↑p x + ↑(sumsq ps) x = 0
this : ↑p x = 0
⊢ ↑(sumsq ps) x = 0
[PROOFSTEP]
simp [this] at h 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x : α → ℕ
p : Poly α
ps : List (Poly α)
this : ↑p x = 0
h : ↑(sumsq ps) x = 0
⊢ ↑(sumsq ps) x = 0
[PROOFSTEP]
exact h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x : α → ℕ
p : Poly α
ps : List (Poly α)
x✝ : ↑p x = 0 ∧ ↑(sumsq ps) x = 0
h1 : ↑p x = 0
h2 : ↑(sumsq ps) x = 0
⊢ ↑(p * p + sumsq ps) x = 0
[PROOFSTEP]
rw [add_apply, mul_apply, h1, h2]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x : α → ℕ
p : Poly α
ps : List (Poly α)
x✝ : ↑p x = 0 ∧ ↑(sumsq ps) x = 0
h1 : ↑p x = 0
h2 : ↑(sumsq ps) x = 0
⊢ 0 * 0 + 0 = 0
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type ?u.112659
β : Type ?u.112662
f : α → β
g : Poly α
i : α
⊢ (fun g => IsPoly fun v => ↑g (v ∘ f)) (proj i)
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type ?u.112659
β : Type ?u.112662
f : α → β
g : Poly α
i : α
⊢ IsPoly fun v => ↑(v (f i))
[PROOFSTEP]
apply IsPoly.proj
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type ?u.112659
β : Type ?u.112662
f : α → β
g : Poly α
n : ℤ
⊢ (fun g => IsPoly fun v => ↑g (v ∘ f)) (const n)
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type ?u.112659
β : Type ?u.112662
f : α → β
g : Poly α
n : ℤ
⊢ IsPoly fun v => n
[PROOFSTEP]
apply IsPoly.const
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type ?u.112659
β : Type ?u.112662
f✝ : α → β
g✝ f g : Poly α
pf : (fun g => IsPoly fun v => ↑g (v ∘ f✝)) f
pg : (fun g => IsPoly fun v => ↑g (v ∘ f✝)) g
⊢ (fun g => IsPoly fun v => ↑g (v ∘ f✝)) (f - g)
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type ?u.112659
β : Type ?u.112662
f✝ : α → β
g✝ f g : Poly α
pf : (fun g => IsPoly fun v => ↑g (v ∘ f✝)) f
pg : (fun g => IsPoly fun v => ↑g (v ∘ f✝)) g
⊢ IsPoly fun v => ↑f (v ∘ f✝) - ↑g (v ∘ f✝)
[PROOFSTEP]
apply IsPoly.sub pf pg
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type ?u.112659
β : Type ?u.112662
f✝ : α → β
g✝ f g : Poly α
pf : (fun g => IsPoly fun v => ↑g (v ∘ f✝)) f
pg : (fun g => IsPoly fun v => ↑g (v ∘ f✝)) g
⊢ (fun g => IsPoly fun v => ↑g (v ∘ f✝)) (f * g)
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type ?u.112659
β : Type ?u.112662
f✝ : α → β
g✝ f g : Poly α
pf : (fun g => IsPoly fun v => ↑g (v ∘ f✝)) f
pg : (fun g => IsPoly fun v => ↑g (v ∘ f✝)) g
⊢ IsPoly fun v => ↑f (v ∘ f✝) * ↑g (v ∘ f✝)
[PROOFSTEP]
apply IsPoly.mul pf pg
[GOAL]
α β γ : Type u
S S' : Set (α → ℕ)
d : Dioph S
H : ∀ (v : α → ℕ), v ∈ S ↔ v ∈ S'
⊢ Dioph S'
[PROOFSTEP]
rwa [← Set.ext H]
[GOAL]
α β γ : Type u
S S' : Set (α → ℕ)
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
⊢ (∃ t, ↑p (v ⊗ t) = 0) ↔ ∃ t, ↑(Poly.map (inl ⊗ inr ∘ f) p) (v ⊗ t) = 0
[PROOFSTEP]
dsimp
[GOAL]
α β γ : Type u
S S' : Set (α → ℕ)
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
⊢ (∃ t, ↑p (v ⊗ t) = 0) ↔ ∃ t, ↑p ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) = 0
[PROOFSTEP]
refine ⟨fun t => ?_, fun t => ?_⟩
[GOAL]
case refine_1
α β γ : Type u
S S' : Set (α → ℕ)
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : ∃ t, ↑p (v ⊗ t) = 0
⊢ ∃ t, ↑p ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) = 0
[PROOFSTEP]
cases' t with t ht
[GOAL]
case refine_2
α β γ : Type u
S S' : Set (α → ℕ)
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : ∃ t, ↑p ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) = 0
⊢ ∃ t, ↑p (v ⊗ t) = 0
[PROOFSTEP]
cases' t with t ht
[GOAL]
case refine_1.intro
α β γ : Type u
S S' : Set (α → ℕ)
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : ↑p (v ⊗ t) = 0
⊢ ∃ t, ↑p ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) = 0
[PROOFSTEP]
have : (v ⊗ (0 ::ₒ t) ∘ g) ∘ (inl ⊗ inr ∘ f) = v ⊗ t :=
  funext fun s => by cases' s with a b <;> dsimp [(· ∘ ·)]; try rw [inv]; rfl
[GOAL]
α β γ : Type u
S S' : Set (α → ℕ)
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : ↑p (v ⊗ t) = 0
s : α ⊕ β
⊢ ((v ⊗ (0 ::ₒ t) ∘ g) ∘ (inl ⊗ inr ∘ f)) s = (v ⊗ t) s
[PROOFSTEP]
cases' s with a b
[GOAL]
case inl
α β γ : Type u
S S' : Set (α → ℕ)
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : ↑p (v ⊗ t) = 0
a : α
⊢ ((v ⊗ (0 ::ₒ t) ∘ g) ∘ (inl ⊗ inr ∘ f)) (inl a) = (v ⊗ t) (inl a)
[PROOFSTEP]
dsimp [(· ∘ ·)]
[GOAL]
case inr
α β γ : Type u
S S' : Set (α → ℕ)
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : ↑p (v ⊗ t) = 0
b : β
⊢ ((v ⊗ (0 ::ₒ t) ∘ g) ∘ (inl ⊗ inr ∘ f)) (inr b) = (v ⊗ t) (inr b)
[PROOFSTEP]
dsimp [(· ∘ ·)]
[GOAL]
case inr
α β γ : Type u
S S' : Set (α → ℕ)
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : ↑p (v ⊗ t) = 0
b : β
⊢ (0 ::ₒ t) (g (f b)) = t b
[PROOFSTEP]
try rw [inv]; rfl
[GOAL]
case inr
α β γ : Type u
S S' : Set (α → ℕ)
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : ↑p (v ⊗ t) = 0
b : β
⊢ (0 ::ₒ t) (g (f b)) = t b
[PROOFSTEP]
rw [inv]
[GOAL]
case inr
α β γ : Type u
S S' : Set (α → ℕ)
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : ↑p (v ⊗ t) = 0
b : β
⊢ (0 ::ₒ t) (some b) = t b
[PROOFSTEP]
rfl
[GOAL]
case refine_1.intro
α β γ : Type u
S S' : Set (α → ℕ)
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : ↑p (v ⊗ t) = 0
this : (v ⊗ (0 ::ₒ t) ∘ g) ∘ (inl ⊗ inr ∘ f) = v ⊗ t
⊢ ∃ t, ↑p ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) = 0
[PROOFSTEP]
exact ⟨(0 ::ₒ t) ∘ g, by rwa [this]⟩
[GOAL]
α β γ : Type u
S S' : Set (α → ℕ)
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : ↑p (v ⊗ t) = 0
this : (v ⊗ (0 ::ₒ t) ∘ g) ∘ (inl ⊗ inr ∘ f) = v ⊗ t
⊢ ↑p ((v ⊗ (0 ::ₒ t) ∘ g) ∘ (inl ⊗ inr ∘ f)) = 0
[PROOFSTEP]
rwa [this]
[GOAL]
case refine_2.intro
α β γ : Type u
S S' : Set (α → ℕ)
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : γ → ℕ
ht : ↑p ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) = 0
⊢ ∃ t, ↑p (v ⊗ t) = 0
[PROOFSTEP]
have : v ⊗ t ∘ f = (v ⊗ t) ∘ (inl ⊗ inr ∘ f) := funext fun s => by cases' s with a b <;> rfl
[GOAL]
α β γ : Type u
S S' : Set (α → ℕ)
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : γ → ℕ
ht : ↑p ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) = 0
s : α ⊕ β
⊢ (v ⊗ t ∘ f) s = ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) s
[PROOFSTEP]
cases' s with a b
[GOAL]
case inl
α β γ : Type u
S S' : Set (α → ℕ)
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : γ → ℕ
ht : ↑p ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) = 0
a : α
⊢ (v ⊗ t ∘ f) (inl a) = ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) (inl a)
[PROOFSTEP]
rfl
[GOAL]
case inr
α β γ : Type u
S S' : Set (α → ℕ)
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : γ → ℕ
ht : ↑p ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) = 0
b : β
⊢ (v ⊗ t ∘ f) (inr b) = ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) (inr b)
[PROOFSTEP]
rfl
[GOAL]
case refine_2.intro
α β γ : Type u
S S' : Set (α → ℕ)
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : γ → ℕ
ht : ↑p ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) = 0
this : v ⊗ t ∘ f = (v ⊗ t) ∘ (inl ⊗ inr ∘ f)
⊢ ∃ t, ↑p (v ⊗ t) = 0
[PROOFSTEP]
exact ⟨t ∘ f, by rwa [this]⟩
[GOAL]
α β γ : Type u
S S' : Set (α → ℕ)
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : γ → ℕ
ht : ↑p ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) = 0
this : v ⊗ t ∘ f = (v ⊗ t) ∘ (inl ⊗ inr ∘ f)
⊢ ↑p (v ⊗ t ∘ f) = 0
[PROOFSTEP]
rwa [this]
[GOAL]
α β γ✝ : Type u
S S' : Set (α → ℕ)
f : α → β
γ : Type u
p : Poly (α ⊕ γ)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : β → ℕ
t : γ → ℕ
s : α ⊕ γ
⊢ (v ∘ f ⊗ t) s = ((v ⊗ t) ∘ (inl ∘ f ⊗ inr)) s
[PROOFSTEP]
cases' s with a b
[GOAL]
case inl
α β γ✝ : Type u
S S' : Set (α → ℕ)
f : α → β
γ : Type u
p : Poly (α ⊕ γ)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : β → ℕ
t : γ → ℕ
a : α
⊢ (v ∘ f ⊗ t) (inl a) = ((v ⊗ t) ∘ (inl ∘ f ⊗ inr)) (inl a)
[PROOFSTEP]
rfl
[GOAL]
case inr
α β γ✝ : Type u
S S' : Set (α → ℕ)
f : α → β
γ : Type u
p : Poly (α ⊕ γ)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : β → ℕ
t : γ → ℕ
b : γ
⊢ (v ∘ f ⊗ t) (inr b) = ((v ⊗ t) ∘ (inl ∘ f ⊗ inr)) (inr b)
[PROOFSTEP]
rfl
[GOAL]
α β γ✝ : Type u
S S' : Set (α → ℕ)
f : α → β
γ : Type u
p : Poly (α ⊕ γ)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : β → ℕ
t : γ → ℕ
this : v ∘ f ⊗ t = (v ⊗ t) ∘ (inl ∘ f ⊗ inr)
⊢ ↑p (v ∘ f ⊗ t) = 0 ↔ ↑(Poly.map (inl ∘ f ⊗ inr) p) (v ⊗ t) = 0
[PROOFSTEP]
simp [this]
[GOAL]
α β γ : Type u
S S' : Set (α → ℕ)
l : List (Set (α → ℕ))
d : List.All₂ Dioph l
⊢ Dioph {v | List.All₂ (fun S => v ∈ S) l}
[PROOFSTEP]
suffices
  ∃ (β : _) (pl : List (Poly (Sum α β))),
    ∀ v, List.All₂ (fun S : Set _ => S v) l ↔ ∃ t, List.All₂ (fun p : Poly (Sum α β) => p (v ⊗ t) = 0) pl
  from
  let ⟨β, pl, h⟩ := this
  ⟨β, Poly.sumsq pl, fun v => (h v).trans <| exists_congr fun t => (Poly.sumsq_eq_zero _ _).symm⟩
[GOAL]
α β γ : Type u
S S' : Set (α → ℕ)
l : List (Set (α → ℕ))
d : List.All₂ Dioph l
⊢ ∃ β pl, ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
[PROOFSTEP]
induction' l with S l IH
[GOAL]
case nil
α β γ : Type u
S S' : Set (α → ℕ)
l : List (Set (α → ℕ))
d✝ : List.All₂ Dioph l
d : List.All₂ Dioph []
⊢ ∃ β pl, ∀ (v : α → ℕ), List.All₂ (fun S => S v) [] ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
case cons
α β γ : Type u
S✝ S' : Set (α → ℕ)
l✝ : List (Set (α → ℕ))
d✝ : List.All₂ Dioph l✝
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH : List.All₂ Dioph l → ∃ β pl, ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
d : List.All₂ Dioph (S :: l)
⊢ ∃ β pl, ∀ (v : α → ℕ), List.All₂ (fun S => S v) (S :: l) ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
[PROOFSTEP]
exact ⟨ULift Empty, [], fun _ => by simp⟩
[GOAL]
α β γ : Type u
S S' : Set (α → ℕ)
l : List (Set (α → ℕ))
d✝ : List.All₂ Dioph l
d : List.All₂ Dioph []
x✝ : α → ℕ
⊢ List.All₂ (fun S => S x✝) [] ↔ ∃ t, List.All₂ (fun p => ↑p (x✝ ⊗ t) = 0) []
[PROOFSTEP]
simp
[GOAL]
case cons
α β γ : Type u
S✝ S' : Set (α → ℕ)
l✝ : List (Set (α → ℕ))
d✝ : List.All₂ Dioph l✝
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH : List.All₂ Dioph l → ∃ β pl, ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
d : List.All₂ Dioph (S :: l)
⊢ ∃ β pl, ∀ (v : α → ℕ), List.All₂ (fun S => S v) (S :: l) ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
[PROOFSTEP]
simp at d 
[GOAL]
case cons
α β γ : Type u
S✝ S' : Set (α → ℕ)
l✝ : List (Set (α → ℕ))
d✝ : List.All₂ Dioph l✝
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH : List.All₂ Dioph l → ∃ β pl, ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
d : Dioph S ∧ List.All₂ Dioph l
⊢ ∃ β pl, ∀ (v : α → ℕ), List.All₂ (fun S => S v) (S :: l) ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
[PROOFSTEP]
exact
  let ⟨⟨β, p, pe⟩, dl⟩ := d
  let ⟨γ, pl, ple⟩ := IH dl
  ⟨Sum β γ, p.map (inl ⊗ inr ∘ inl) :: pl.map fun q => q.map (inl ⊗ inr ∘ inr), fun v => by simp;
    exact
      Iff.trans (and_congr (pe v) (ple v))
        ⟨fun ⟨⟨m, hm⟩, ⟨n, hn⟩⟩ =>
          ⟨m ⊗ n, by
            rw [show (v ⊗ m ⊗ n) ∘ (inl ⊗ inr ∘ inl) = v ⊗ m from funext fun s => by cases' s with a b <;> rfl];
            exact hm, by
            refine List.All₂.imp (fun q hq => ?_) hn; dsimp [(· ∘ ·)]
            rw [show (fun x : Sum α γ => (v ⊗ m ⊗ n) ((inl ⊗ fun x : γ => inr (inr x)) x)) = v ⊗ n from
                funext fun s => by cases' s with a b <;> rfl];
            exact hq⟩,
          fun ⟨t, hl, hr⟩ =>
          ⟨⟨t ∘ inl, by
              rwa [show (v ⊗ t) ∘ (inl ⊗ inr ∘ inl) = v ⊗ t ∘ inl from funext fun s => by cases' s with a b <;> rfl] at
                hl ⟩,
            ⟨t ∘ inr, by
              refine List.All₂.imp (fun q hq => ?_) hr; dsimp [(· ∘ ·)] at hq 
              rwa [show (fun x : Sum α γ => (v ⊗ t) ((inl ⊗ fun x : γ => inr (inr x)) x)) = v ⊗ t ∘ inr from
                  funext fun s => by cases' s with a b <;> rfl] at
                hq ⟩⟩⟩⟩
[GOAL]
α β✝ γ✝ : Type u
S✝ S' : Set (α → ℕ)
l✝ : List (Set (α → ℕ))
d✝ : List.All₂ Dioph l✝
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH : List.All₂ Dioph l → ∃ β pl, ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
d : Dioph S ∧ List.All₂ Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
dl : List.All₂ Dioph l
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
v : α → ℕ
⊢ List.All₂ (fun S => S v) (S :: l) ↔
    ∃ t,
      List.All₂ (fun p => ↑p (v ⊗ t) = 0)
        (Poly.map (inl ⊗ inr ∘ inl) p :: List.map (fun q => Poly.map (inl ⊗ inr ∘ inr) q) pl)
[PROOFSTEP]
simp
[GOAL]
α β✝ γ✝ : Type u
S✝ S' : Set (α → ℕ)
l✝ : List (Set (α → ℕ))
d✝ : List.All₂ Dioph l✝
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH : List.All₂ Dioph l → ∃ β pl, ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
d : Dioph S ∧ List.All₂ Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
dl : List.All₂ Dioph l
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
v : α → ℕ
⊢ S v ∧ List.All₂ (fun S => S v) l ↔
    ∃ t,
      ↑p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0 ∧
        List.All₂ ((fun p => ↑p (v ⊗ t) = 0) ∘ fun q => Poly.map (inl ⊗ inr ∘ inr) q) pl
[PROOFSTEP]
exact
  Iff.trans (and_congr (pe v) (ple v))
    ⟨fun ⟨⟨m, hm⟩, ⟨n, hn⟩⟩ =>
      ⟨m ⊗ n, by rw [show (v ⊗ m ⊗ n) ∘ (inl ⊗ inr ∘ inl) = v ⊗ m from funext fun s => by cases' s with a b <;> rfl];
        exact hm, by
        refine List.All₂.imp (fun q hq => ?_) hn; dsimp [(· ∘ ·)]
        rw [show (fun x : Sum α γ => (v ⊗ m ⊗ n) ((inl ⊗ fun x : γ => inr (inr x)) x)) = v ⊗ n from
            funext fun s => by cases' s with a b <;> rfl];
        exact hq⟩,
      fun ⟨t, hl, hr⟩ =>
      ⟨⟨t ∘ inl, by
          rwa [show (v ⊗ t) ∘ (inl ⊗ inr ∘ inl) = v ⊗ t ∘ inl from funext fun s => by cases' s with a b <;> rfl] at hl
            ⟩,
        ⟨t ∘ inr, by
          refine List.All₂.imp (fun q hq => ?_) hr; dsimp [(· ∘ ·)] at hq 
          rwa [show (fun x : Sum α γ => (v ⊗ t) ((inl ⊗ fun x : γ => inr (inr x)) x)) = v ⊗ t ∘ inr from
              funext fun s => by cases' s with a b <;> rfl] at
            hq ⟩⟩⟩
[GOAL]
α β✝ γ✝ : Type u
S✝ S' : Set (α → ℕ)
l✝ : List (Set (α → ℕ))
d✝ : List.All₂ Dioph l✝
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH : List.All₂ Dioph l → ∃ β pl, ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
d : Dioph S ∧ List.All₂ Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
dl : List.All₂ Dioph l
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
v : α → ℕ
x✝ : (∃ t, ↑p (v ⊗ t) = 0) ∧ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
m : β → ℕ
hm : ↑p (v ⊗ m) = 0
n : γ → ℕ
hn : List.All₂ (fun p => ↑p (v ⊗ n) = 0) pl
⊢ ↑p ((v ⊗ m ⊗ n) ∘ (inl ⊗ inr ∘ inl)) = 0
[PROOFSTEP]
rw [show (v ⊗ m ⊗ n) ∘ (inl ⊗ inr ∘ inl) = v ⊗ m from funext fun s => by cases' s with a b <;> rfl]
[GOAL]
α β✝ γ✝ : Type u
S✝ S' : Set (α → ℕ)
l✝ : List (Set (α → ℕ))
d✝ : List.All₂ Dioph l✝
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH : List.All₂ Dioph l → ∃ β pl, ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
d : Dioph S ∧ List.All₂ Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
dl : List.All₂ Dioph l
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
v : α → ℕ
x✝ : (∃ t, ↑p (v ⊗ t) = 0) ∧ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
m : β → ℕ
hm : ↑p (v ⊗ m) = 0
n : γ → ℕ
hn : List.All₂ (fun p => ↑p (v ⊗ n) = 0) pl
s : α ⊕ β
⊢ ((v ⊗ m ⊗ n) ∘ (inl ⊗ inr ∘ inl)) s = (v ⊗ m) s
[PROOFSTEP]
cases' s with a b
[GOAL]
case inl
α β✝ γ✝ : Type u
S✝ S' : Set (α → ℕ)
l✝ : List (Set (α → ℕ))
d✝ : List.All₂ Dioph l✝
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH : List.All₂ Dioph l → ∃ β pl, ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
d : Dioph S ∧ List.All₂ Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
dl : List.All₂ Dioph l
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
v : α → ℕ
x✝ : (∃ t, ↑p (v ⊗ t) = 0) ∧ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
m : β → ℕ
hm : ↑p (v ⊗ m) = 0
n : γ → ℕ
hn : List.All₂ (fun p => ↑p (v ⊗ n) = 0) pl
a : α
⊢ ((v ⊗ m ⊗ n) ∘ (inl ⊗ inr ∘ inl)) (inl a) = (v ⊗ m) (inl a)
[PROOFSTEP]
rfl
[GOAL]
case inr
α β✝ γ✝ : Type u
S✝ S' : Set (α → ℕ)
l✝ : List (Set (α → ℕ))
d✝ : List.All₂ Dioph l✝
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH : List.All₂ Dioph l → ∃ β pl, ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
d : Dioph S ∧ List.All₂ Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
dl : List.All₂ Dioph l
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
v : α → ℕ
x✝ : (∃ t, ↑p (v ⊗ t) = 0) ∧ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
m : β → ℕ
hm : ↑p (v ⊗ m) = 0
n : γ → ℕ
hn : List.All₂ (fun p => ↑p (v ⊗ n) = 0) pl
b : β
⊢ ((v ⊗ m ⊗ n) ∘ (inl ⊗ inr ∘ inl)) (inr b) = (v ⊗ m) (inr b)
[PROOFSTEP]
rfl
[GOAL]
α β✝ γ✝ : Type u
S✝ S' : Set (α → ℕ)
l✝ : List (Set (α → ℕ))
d✝ : List.All₂ Dioph l✝
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH : List.All₂ Dioph l → ∃ β pl, ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
d : Dioph S ∧ List.All₂ Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
dl : List.All₂ Dioph l
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
v : α → ℕ
x✝ : (∃ t, ↑p (v ⊗ t) = 0) ∧ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
m : β → ℕ
hm : ↑p (v ⊗ m) = 0
n : γ → ℕ
hn : List.All₂ (fun p => ↑p (v ⊗ n) = 0) pl
⊢ ↑p (v ⊗ m) = 0
[PROOFSTEP]
exact hm
[GOAL]
α β✝ γ✝ : Type u
S✝ S' : Set (α → ℕ)
l✝ : List (Set (α → ℕ))
d✝ : List.All₂ Dioph l✝
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH : List.All₂ Dioph l → ∃ β pl, ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
d : Dioph S ∧ List.All₂ Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
dl : List.All₂ Dioph l
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
v : α → ℕ
x✝ : (∃ t, ↑p (v ⊗ t) = 0) ∧ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
m : β → ℕ
hm : ↑p (v ⊗ m) = 0
n : γ → ℕ
hn : List.All₂ (fun p => ↑p (v ⊗ n) = 0) pl
⊢ List.All₂ ((fun p => ↑p (v ⊗ m ⊗ n) = 0) ∘ fun q => Poly.map (inl ⊗ inr ∘ inr) q) pl
[PROOFSTEP]
refine List.All₂.imp (fun q hq => ?_) hn
[GOAL]
α β✝ γ✝ : Type u
S✝ S' : Set (α → ℕ)
l✝ : List (Set (α → ℕ))
d✝ : List.All₂ Dioph l✝
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH : List.All₂ Dioph l → ∃ β pl, ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
d : Dioph S ∧ List.All₂ Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
dl : List.All₂ Dioph l
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
v : α → ℕ
x✝ : (∃ t, ↑p (v ⊗ t) = 0) ∧ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
m : β → ℕ
hm : ↑p (v ⊗ m) = 0
n : γ → ℕ
hn : List.All₂ (fun p => ↑p (v ⊗ n) = 0) pl
q : Poly (α ⊕ γ)
hq : ↑q (v ⊗ n) = 0
⊢ ((fun p => ↑p (v ⊗ m ⊗ n) = 0) ∘ fun q => Poly.map (inl ⊗ inr ∘ inr) q) q
[PROOFSTEP]
dsimp [(· ∘ ·)]
[GOAL]
α β✝ γ✝ : Type u
S✝ S' : Set (α → ℕ)
l✝ : List (Set (α → ℕ))
d✝ : List.All₂ Dioph l✝
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH : List.All₂ Dioph l → ∃ β pl, ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
d : Dioph S ∧ List.All₂ Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
dl : List.All₂ Dioph l
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
v : α → ℕ
x✝ : (∃ t, ↑p (v ⊗ t) = 0) ∧ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
m : β → ℕ
hm : ↑p (v ⊗ m) = 0
n : γ → ℕ
hn : List.All₂ (fun p => ↑p (v ⊗ n) = 0) pl
q : Poly (α ⊕ γ)
hq : ↑q (v ⊗ n) = 0
⊢ (↑q fun x => (v ⊗ m ⊗ n) ((inl ⊗ fun x => inr (inr x)) x)) = 0
[PROOFSTEP]
rw [show (fun x : Sum α γ => (v ⊗ m ⊗ n) ((inl ⊗ fun x : γ => inr (inr x)) x)) = v ⊗ n from
    funext fun s => by cases' s with a b <;> rfl]
[GOAL]
α β✝ γ✝ : Type u
S✝ S' : Set (α → ℕ)
l✝ : List (Set (α → ℕ))
d✝ : List.All₂ Dioph l✝
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH : List.All₂ Dioph l → ∃ β pl, ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
d : Dioph S ∧ List.All₂ Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
dl : List.All₂ Dioph l
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
v : α → ℕ
x✝ : (∃ t, ↑p (v ⊗ t) = 0) ∧ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
m : β → ℕ
hm : ↑p (v ⊗ m) = 0
n : γ → ℕ
hn : List.All₂ (fun p => ↑p (v ⊗ n) = 0) pl
q : Poly (α ⊕ γ)
hq : ↑q (v ⊗ n) = 0
s : α ⊕ γ
⊢ (v ⊗ m ⊗ n) ((inl ⊗ fun x => inr (inr x)) s) = (v ⊗ n) s
[PROOFSTEP]
cases' s with a b
[GOAL]
case inl
α β✝ γ✝ : Type u
S✝ S' : Set (α → ℕ)
l✝ : List (Set (α → ℕ))
d✝ : List.All₂ Dioph l✝
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH : List.All₂ Dioph l → ∃ β pl, ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
d : Dioph S ∧ List.All₂ Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
dl : List.All₂ Dioph l
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
v : α → ℕ
x✝ : (∃ t, ↑p (v ⊗ t) = 0) ∧ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
m : β → ℕ
hm : ↑p (v ⊗ m) = 0
n : γ → ℕ
hn : List.All₂ (fun p => ↑p (v ⊗ n) = 0) pl
q : Poly (α ⊕ γ)
hq : ↑q (v ⊗ n) = 0
a : α
⊢ (v ⊗ m ⊗ n) ((inl ⊗ fun x => inr (inr x)) (inl a)) = (v ⊗ n) (inl a)
[PROOFSTEP]
rfl
[GOAL]
case inr
α β✝ γ✝ : Type u
S✝ S' : Set (α → ℕ)
l✝ : List (Set (α → ℕ))
d✝ : List.All₂ Dioph l✝
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH : List.All₂ Dioph l → ∃ β pl, ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
d : Dioph S ∧ List.All₂ Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
dl : List.All₂ Dioph l
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
v : α → ℕ
x✝ : (∃ t, ↑p (v ⊗ t) = 0) ∧ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
m : β → ℕ
hm : ↑p (v ⊗ m) = 0
n : γ → ℕ
hn : List.All₂ (fun p => ↑p (v ⊗ n) = 0) pl
q : Poly (α ⊕ γ)
hq : ↑q (v ⊗ n) = 0
b : γ
⊢ (v ⊗ m ⊗ n) ((inl ⊗ fun x => inr (inr x)) (inr b)) = (v ⊗ n) (inr b)
[PROOFSTEP]
rfl
[GOAL]
α β✝ γ✝ : Type u
S✝ S' : Set (α → ℕ)
l✝ : List (Set (α → ℕ))
d✝ : List.All₂ Dioph l✝
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH : List.All₂ Dioph l → ∃ β pl, ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
d : Dioph S ∧ List.All₂ Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
dl : List.All₂ Dioph l
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
v : α → ℕ
x✝ : (∃ t, ↑p (v ⊗ t) = 0) ∧ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
m : β → ℕ
hm : ↑p (v ⊗ m) = 0
n : γ → ℕ
hn : List.All₂ (fun p => ↑p (v ⊗ n) = 0) pl
q : Poly (α ⊕ γ)
hq : ↑q (v ⊗ n) = 0
⊢ ↑q (v ⊗ n) = 0
[PROOFSTEP]
exact hq
[GOAL]
α β✝ γ✝ : Type u
S✝ S' : Set (α → ℕ)
l✝ : List (Set (α → ℕ))
d✝ : List.All₂ Dioph l✝
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH : List.All₂ Dioph l → ∃ β pl, ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
d : Dioph S ∧ List.All₂ Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
dl : List.All₂ Dioph l
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
v : α → ℕ
x✝ :
  ∃ t,
    ↑p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0 ∧
      List.All₂ ((fun p => ↑p (v ⊗ t) = 0) ∘ fun q => Poly.map (inl ⊗ inr ∘ inr) q) pl
t : β ⊕ γ → ℕ
hl : ↑p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0
hr : List.All₂ ((fun p => ↑p (v ⊗ t) = 0) ∘ fun q => Poly.map (inl ⊗ inr ∘ inr) q) pl
⊢ ↑p (v ⊗ t ∘ inl) = 0
[PROOFSTEP]
rwa [show (v ⊗ t) ∘ (inl ⊗ inr ∘ inl) = v ⊗ t ∘ inl from funext fun s => by cases' s with a b <;> rfl] at hl 
[GOAL]
α β✝ γ✝ : Type u
S✝ S' : Set (α → ℕ)
l✝ : List (Set (α → ℕ))
d✝ : List.All₂ Dioph l✝
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH : List.All₂ Dioph l → ∃ β pl, ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
d : Dioph S ∧ List.All₂ Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
dl : List.All₂ Dioph l
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
v : α → ℕ
x✝ :
  ∃ t,
    ↑p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0 ∧
      List.All₂ ((fun p => ↑p (v ⊗ t) = 0) ∘ fun q => Poly.map (inl ⊗ inr ∘ inr) q) pl
t : β ⊕ γ → ℕ
hl : ↑p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0
hr : List.All₂ ((fun p => ↑p (v ⊗ t) = 0) ∘ fun q => Poly.map (inl ⊗ inr ∘ inr) q) pl
s : α ⊕ β
⊢ ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) s = (v ⊗ t ∘ inl) s
[PROOFSTEP]
cases' s with a b
[GOAL]
case inl
α β✝ γ✝ : Type u
S✝ S' : Set (α → ℕ)
l✝ : List (Set (α → ℕ))
d✝ : List.All₂ Dioph l✝
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH : List.All₂ Dioph l → ∃ β pl, ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
d : Dioph S ∧ List.All₂ Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
dl : List.All₂ Dioph l
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
v : α → ℕ
x✝ :
  ∃ t,
    ↑p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0 ∧
      List.All₂ ((fun p => ↑p (v ⊗ t) = 0) ∘ fun q => Poly.map (inl ⊗ inr ∘ inr) q) pl
t : β ⊕ γ → ℕ
hl : ↑p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0
hr : List.All₂ ((fun p => ↑p (v ⊗ t) = 0) ∘ fun q => Poly.map (inl ⊗ inr ∘ inr) q) pl
a : α
⊢ ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) (inl a) = (v ⊗ t ∘ inl) (inl a)
[PROOFSTEP]
rfl
[GOAL]
case inr
α β✝ γ✝ : Type u
S✝ S' : Set (α → ℕ)
l✝ : List (Set (α → ℕ))
d✝ : List.All₂ Dioph l✝
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH : List.All₂ Dioph l → ∃ β pl, ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
d : Dioph S ∧ List.All₂ Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
dl : List.All₂ Dioph l
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
v : α → ℕ
x✝ :
  ∃ t,
    ↑p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0 ∧
      List.All₂ ((fun p => ↑p (v ⊗ t) = 0) ∘ fun q => Poly.map (inl ⊗ inr ∘ inr) q) pl
t : β ⊕ γ → ℕ
hl : ↑p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0
hr : List.All₂ ((fun p => ↑p (v ⊗ t) = 0) ∘ fun q => Poly.map (inl ⊗ inr ∘ inr) q) pl
b : β
⊢ ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) (inr b) = (v ⊗ t ∘ inl) (inr b)
[PROOFSTEP]
rfl
[GOAL]
α β✝ γ✝ : Type u
S✝ S' : Set (α → ℕ)
l✝ : List (Set (α → ℕ))
d✝ : List.All₂ Dioph l✝
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH : List.All₂ Dioph l → ∃ β pl, ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
d : Dioph S ∧ List.All₂ Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
dl : List.All₂ Dioph l
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
v : α → ℕ
x✝ :
  ∃ t,
    ↑p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0 ∧
      List.All₂ ((fun p => ↑p (v ⊗ t) = 0) ∘ fun q => Poly.map (inl ⊗ inr ∘ inr) q) pl
t : β ⊕ γ → ℕ
hl : ↑p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0
hr : List.All₂ ((fun p => ↑p (v ⊗ t) = 0) ∘ fun q => Poly.map (inl ⊗ inr ∘ inr) q) pl
⊢ List.All₂ (fun p => ↑p (v ⊗ t ∘ inr) = 0) pl
[PROOFSTEP]
refine List.All₂.imp (fun q hq => ?_) hr
[GOAL]
α β✝ γ✝ : Type u
S✝ S' : Set (α → ℕ)
l✝ : List (Set (α → ℕ))
d✝ : List.All₂ Dioph l✝
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH : List.All₂ Dioph l → ∃ β pl, ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
d : Dioph S ∧ List.All₂ Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
dl : List.All₂ Dioph l
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
v : α → ℕ
x✝ :
  ∃ t,
    ↑p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0 ∧
      List.All₂ ((fun p => ↑p (v ⊗ t) = 0) ∘ fun q => Poly.map (inl ⊗ inr ∘ inr) q) pl
t : β ⊕ γ → ℕ
hl : ↑p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0
hr : List.All₂ ((fun p => ↑p (v ⊗ t) = 0) ∘ fun q => Poly.map (inl ⊗ inr ∘ inr) q) pl
q : Poly (α ⊕ γ)
hq : ((fun p => ↑p (v ⊗ t) = 0) ∘ fun q => Poly.map (inl ⊗ inr ∘ inr) q) q
⊢ ↑q (v ⊗ t ∘ inr) = 0
[PROOFSTEP]
dsimp [(· ∘ ·)] at hq 
[GOAL]
α β✝ γ✝ : Type u
S✝ S' : Set (α → ℕ)
l✝ : List (Set (α → ℕ))
d✝ : List.All₂ Dioph l✝
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH : List.All₂ Dioph l → ∃ β pl, ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
d : Dioph S ∧ List.All₂ Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
dl : List.All₂ Dioph l
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
v : α → ℕ
x✝ :
  ∃ t,
    ↑p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0 ∧
      List.All₂ ((fun p => ↑p (v ⊗ t) = 0) ∘ fun q => Poly.map (inl ⊗ inr ∘ inr) q) pl
t : β ⊕ γ → ℕ
hl : ↑p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0
hr : List.All₂ ((fun p => ↑p (v ⊗ t) = 0) ∘ fun q => Poly.map (inl ⊗ inr ∘ inr) q) pl
q : Poly (α ⊕ γ)
hq : (↑q fun x => (v ⊗ t) ((inl ⊗ fun x => inr (inr x)) x)) = 0
⊢ ↑q (v ⊗ t ∘ inr) = 0
[PROOFSTEP]
rwa [show (fun x : Sum α γ => (v ⊗ t) ((inl ⊗ fun x : γ => inr (inr x)) x)) = v ⊗ t ∘ inr from
    funext fun s => by cases' s with a b <;> rfl] at
  hq 
[GOAL]
α β✝ γ✝ : Type u
S✝ S' : Set (α → ℕ)
l✝ : List (Set (α → ℕ))
d✝ : List.All₂ Dioph l✝
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH : List.All₂ Dioph l → ∃ β pl, ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
d : Dioph S ∧ List.All₂ Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
dl : List.All₂ Dioph l
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
v : α → ℕ
x✝ :
  ∃ t,
    ↑p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0 ∧
      List.All₂ ((fun p => ↑p (v ⊗ t) = 0) ∘ fun q => Poly.map (inl ⊗ inr ∘ inr) q) pl
t : β ⊕ γ → ℕ
hl : ↑p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0
hr : List.All₂ ((fun p => ↑p (v ⊗ t) = 0) ∘ fun q => Poly.map (inl ⊗ inr ∘ inr) q) pl
q : Poly (α ⊕ γ)
hq : (↑q fun x => (v ⊗ t) ((inl ⊗ fun x => inr (inr x)) x)) = 0
s : α ⊕ γ
⊢ (v ⊗ t) ((inl ⊗ fun x => inr (inr x)) s) = (v ⊗ t ∘ inr) s
[PROOFSTEP]
cases' s with a b
[GOAL]
case inl
α β✝ γ✝ : Type u
S✝ S' : Set (α → ℕ)
l✝ : List (Set (α → ℕ))
d✝ : List.All₂ Dioph l✝
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH : List.All₂ Dioph l → ∃ β pl, ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
d : Dioph S ∧ List.All₂ Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
dl : List.All₂ Dioph l
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
v : α → ℕ
x✝ :
  ∃ t,
    ↑p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0 ∧
      List.All₂ ((fun p => ↑p (v ⊗ t) = 0) ∘ fun q => Poly.map (inl ⊗ inr ∘ inr) q) pl
t : β ⊕ γ → ℕ
hl : ↑p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0
hr : List.All₂ ((fun p => ↑p (v ⊗ t) = 0) ∘ fun q => Poly.map (inl ⊗ inr ∘ inr) q) pl
q : Poly (α ⊕ γ)
hq : (↑q fun x => (v ⊗ t) ((inl ⊗ fun x => inr (inr x)) x)) = 0
a : α
⊢ (v ⊗ t) ((inl ⊗ fun x => inr (inr x)) (inl a)) = (v ⊗ t ∘ inr) (inl a)
[PROOFSTEP]
rfl
[GOAL]
case inr
α β✝ γ✝ : Type u
S✝ S' : Set (α → ℕ)
l✝ : List (Set (α → ℕ))
d✝ : List.All₂ Dioph l✝
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH : List.All₂ Dioph l → ∃ β pl, ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
d : Dioph S ∧ List.All₂ Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
dl : List.All₂ Dioph l
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.All₂ (fun S => S v) l ↔ ∃ t, List.All₂ (fun p => ↑p (v ⊗ t) = 0) pl
v : α → ℕ
x✝ :
  ∃ t,
    ↑p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0 ∧
      List.All₂ ((fun p => ↑p (v ⊗ t) = 0) ∘ fun q => Poly.map (inl ⊗ inr ∘ inr) q) pl
t : β ⊕ γ → ℕ
hl : ↑p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0
hr : List.All₂ ((fun p => ↑p (v ⊗ t) = 0) ∘ fun q => Poly.map (inl ⊗ inr ∘ inr) q) pl
q : Poly (α ⊕ γ)
hq : (↑q fun x => (v ⊗ t) ((inl ⊗ fun x => inr (inr x)) x)) = 0
b : γ
⊢ (v ⊗ t) ((inl ⊗ fun x => inr (inr x)) (inr b)) = (v ⊗ t ∘ inr) (inr b)
[PROOFSTEP]
rfl
[GOAL]
α β✝ γ✝ : Type u
S S' : Set (α → ℕ)
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
γ : Type u
q : Poly (α ⊕ γ)
qe : ∀ (v : α → ℕ), S' v ↔ ∃ t, ↑q (v ⊗ t) = 0
v : α → ℕ
⊢ (S ∪ S') v ↔ ∃ t, ↑(Poly.map (inl ⊗ inr ∘ inl) p * Poly.map (inl ⊗ inr ∘ inr) q) (v ⊗ t) = 0
[PROOFSTEP]
refine
  Iff.trans (or_congr ((pe v).trans ?_) ((qe v).trans ?_))
    (exists_or.symm.trans
      (exists_congr fun t =>
        (@mul_eq_zero _ _ _ (p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl))) (q ((v ⊗ t) ∘ (inl ⊗ inr ∘ inr)))).symm))
      -- Porting note: putting everything on the same line fails
[GOAL]
case refine_1
α β✝ γ✝ : Type u
S S' : Set (α → ℕ)
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
γ : Type u
q : Poly (α ⊕ γ)
qe : ∀ (v : α → ℕ), S' v ↔ ∃ t, ↑q (v ⊗ t) = 0
v : α → ℕ
⊢ (∃ t, ↑p (v ⊗ t) = 0) ↔ ∃ x, ↑p ((v ⊗ x) ∘ (inl ⊗ inr ∘ inl)) = 0
[PROOFSTEP]
refine inject_dummies_lem _ ?_ ?_ _ _
[GOAL]
case refine_1.refine_1
α β✝ γ✝ : Type u
S S' : Set (α → ℕ)
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
γ : Type u
q : Poly (α ⊕ γ)
qe : ∀ (v : α → ℕ), S' v ↔ ∃ t, ↑q (v ⊗ t) = 0
v : α → ℕ
⊢ β ⊕ γ → Option β
case refine_1.refine_2
α β✝ γ✝ : Type u
S S' : Set (α → ℕ)
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
γ : Type u
q : Poly (α ⊕ γ)
qe : ∀ (v : α → ℕ), S' v ↔ ∃ t, ↑q (v ⊗ t) = 0
v : α → ℕ
⊢ ∀ (x : β), ?refine_1.refine_1 (inl x) = some x
[PROOFSTEP]
exact some ⊗ fun _ => none
[GOAL]
case refine_1.refine_2
α β✝ γ✝ : Type u
S S' : Set (α → ℕ)
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
γ : Type u
q : Poly (α ⊕ γ)
qe : ∀ (v : α → ℕ), S' v ↔ ∃ t, ↑q (v ⊗ t) = 0
v : α → ℕ
⊢ ∀ (x : β), (some ⊗ fun x => none) (inl x) = some x
[PROOFSTEP]
exact fun _ => by
  simp only [elim_inl]
    -- Porting note: putting everything on the same line fails
[GOAL]
α β✝ γ✝ : Type u
S S' : Set (α → ℕ)
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
γ : Type u
q : Poly (α ⊕ γ)
qe : ∀ (v : α → ℕ), S' v ↔ ∃ t, ↑q (v ⊗ t) = 0
v : α → ℕ
x✝ : β
⊢ (some ⊗ fun x => none) (inl x✝) = some x✝
[PROOFSTEP]
simp only [elim_inl]
  -- Porting note: putting everything on the same line fails
[GOAL]
case refine_2
α β✝ γ✝ : Type u
S S' : Set (α → ℕ)
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
γ : Type u
q : Poly (α ⊕ γ)
qe : ∀ (v : α → ℕ), S' v ↔ ∃ t, ↑q (v ⊗ t) = 0
v : α → ℕ
⊢ (∃ t, ↑q (v ⊗ t) = 0) ↔ ∃ x, ↑q ((v ⊗ x) ∘ (inl ⊗ inr ∘ inr)) = 0
[PROOFSTEP]
refine inject_dummies_lem _ ?_ ?_ _ _
[GOAL]
case refine_2.refine_1
α β✝ γ✝ : Type u
S S' : Set (α → ℕ)
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
γ : Type u
q : Poly (α ⊕ γ)
qe : ∀ (v : α → ℕ), S' v ↔ ∃ t, ↑q (v ⊗ t) = 0
v : α → ℕ
⊢ β ⊕ γ → Option γ
case refine_2.refine_2
α β✝ γ✝ : Type u
S S' : Set (α → ℕ)
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
γ : Type u
q : Poly (α ⊕ γ)
qe : ∀ (v : α → ℕ), S' v ↔ ∃ t, ↑q (v ⊗ t) = 0
v : α → ℕ
⊢ ∀ (x : γ), ?refine_2.refine_1 (inr x) = some x
[PROOFSTEP]
exact (fun _ => none) ⊗ some
[GOAL]
case refine_2.refine_2
α β✝ γ✝ : Type u
S S' : Set (α → ℕ)
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
γ : Type u
q : Poly (α ⊕ γ)
qe : ∀ (v : α → ℕ), S' v ↔ ∃ t, ↑q (v ⊗ t) = 0
v : α → ℕ
⊢ ∀ (x : γ), ((fun x => none) ⊗ some) (inr x) = some x
[PROOFSTEP]
exact fun _ => by simp only [elim_inr]
[GOAL]
α β✝ γ✝ : Type u
S S' : Set (α → ℕ)
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
γ : Type u
q : Poly (α ⊕ γ)
qe : ∀ (v : α → ℕ), S' v ↔ ∃ t, ↑q (v ⊗ t) = 0
v : α → ℕ
x✝ : γ
⊢ ((fun x => none) ⊗ some) (inr x✝) = some x✝
[PROOFSTEP]
simp only [elim_inr]
[GOAL]
α β γ : Type u
S S' : Set (α → ℕ)
f : (α → ℕ) → ℕ
g : α → β
d : DiophFn f
⊢ DiophFn fun v => f (v ∘ g)
[PROOFSTEP]
convert reindex_dioph (Option β) (Option.map g) d
[GOAL]
α β γ✝ : Type u
S✝ S' : Set (α → ℕ)
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : setOf (fun v => ∃ x, v ⊗ x ∈ S) v
x : β → ℕ
hx : v ⊗ x ∈ S
t : γ → ℕ
ht : ↑p ((v ⊗ x) ⊗ t) = 0
⊢ ↑(Poly.map ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr) p) (v ⊗ x ⊗ t) = 0
[PROOFSTEP]
simp
[GOAL]
α β γ✝ : Type u
S✝ S' : Set (α → ℕ)
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : setOf (fun v => ∃ x, v ⊗ x ∈ S) v
x : β → ℕ
hx : v ⊗ x ∈ S
t : γ → ℕ
ht : ↑p ((v ⊗ x) ⊗ t) = 0
⊢ ↑p ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) = 0
[PROOFSTEP]
rw [show (v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr) = (v ⊗ x) ⊗ t from
    funext fun s => by
      cases' s with a b <;>
        try {cases a <;> rfl
        };
      rfl]
[GOAL]
α β γ✝ : Type u
S✝ S' : Set (α → ℕ)
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : setOf (fun v => ∃ x, v ⊗ x ∈ S) v
x : β → ℕ
hx : v ⊗ x ∈ S
t : γ → ℕ
ht : ↑p ((v ⊗ x) ⊗ t) = 0
s : (α ⊕ β) ⊕ γ
⊢ ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) s = ((v ⊗ x) ⊗ t) s
[PROOFSTEP]
cases' s with a b
[GOAL]
case inl
α β γ✝ : Type u
S✝ S' : Set (α → ℕ)
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : setOf (fun v => ∃ x, v ⊗ x ∈ S) v
x : β → ℕ
hx : v ⊗ x ∈ S
t : γ → ℕ
ht : ↑p ((v ⊗ x) ⊗ t) = 0
a : α ⊕ β
⊢ ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inl a) = ((v ⊗ x) ⊗ t) (inl a)
[PROOFSTEP]
try {cases a <;> rfl
}
[GOAL]
case inl
α β γ✝ : Type u
S✝ S' : Set (α → ℕ)
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : setOf (fun v => ∃ x, v ⊗ x ∈ S) v
x : β → ℕ
hx : v ⊗ x ∈ S
t : γ → ℕ
ht : ↑p ((v ⊗ x) ⊗ t) = 0
a : α ⊕ β
⊢ ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inl a) = ((v ⊗ x) ⊗ t) (inl a)
[PROOFSTEP]
{cases a <;> rfl
}
[GOAL]
case inl
α β γ✝ : Type u
S✝ S' : Set (α → ℕ)
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : setOf (fun v => ∃ x, v ⊗ x ∈ S) v
x : β → ℕ
hx : v ⊗ x ∈ S
t : γ → ℕ
ht : ↑p ((v ⊗ x) ⊗ t) = 0
a : α ⊕ β
⊢ ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inl a) = ((v ⊗ x) ⊗ t) (inl a)
[PROOFSTEP]
cases a
[GOAL]
case inl.inl
α β γ✝ : Type u
S✝ S' : Set (α → ℕ)
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : setOf (fun v => ∃ x, v ⊗ x ∈ S) v
x : β → ℕ
hx : v ⊗ x ∈ S
t : γ → ℕ
ht : ↑p ((v ⊗ x) ⊗ t) = 0
val✝ : α
⊢ ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inl (inl val✝)) = ((v ⊗ x) ⊗ t) (inl (inl val✝))
[PROOFSTEP]
rfl
[GOAL]
case inl.inr
α β γ✝ : Type u
S✝ S' : Set (α → ℕ)
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : setOf (fun v => ∃ x, v ⊗ x ∈ S) v
x : β → ℕ
hx : v ⊗ x ∈ S
t : γ → ℕ
ht : ↑p ((v ⊗ x) ⊗ t) = 0
val✝ : β
⊢ ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inl (inr val✝)) = ((v ⊗ x) ⊗ t) (inl (inr val✝))
[PROOFSTEP]
rfl
[GOAL]
case inr
α β γ✝ : Type u
S✝ S' : Set (α → ℕ)
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : setOf (fun v => ∃ x, v ⊗ x ∈ S) v
x : β → ℕ
hx : v ⊗ x ∈ S
t : γ → ℕ
ht : ↑p ((v ⊗ x) ⊗ t) = 0
b : γ
⊢ ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inr b) = ((v ⊗ x) ⊗ t) (inr b)
[PROOFSTEP]
try {cases a <;> rfl
}
[GOAL]
case inr
α β γ✝ : Type u
S✝ S' : Set (α → ℕ)
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : setOf (fun v => ∃ x, v ⊗ x ∈ S) v
x : β → ℕ
hx : v ⊗ x ∈ S
t : γ → ℕ
ht : ↑p ((v ⊗ x) ⊗ t) = 0
b : γ
⊢ ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inr b) = ((v ⊗ x) ⊗ t) (inr b)
[PROOFSTEP]
{cases a <;> rfl
}
[GOAL]
case inr
α β γ✝ : Type u
S✝ S' : Set (α → ℕ)
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : setOf (fun v => ∃ x, v ⊗ x ∈ S) v
x : β → ℕ
hx : v ⊗ x ∈ S
t : γ → ℕ
ht : ↑p ((v ⊗ x) ⊗ t) = 0
b : γ
⊢ ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inr b) = ((v ⊗ x) ⊗ t) (inr b)
[PROOFSTEP]
cases a
[GOAL]
case inr
α β γ✝ : Type u
S✝ S' : Set (α → ℕ)
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : setOf (fun v => ∃ x, v ⊗ x ∈ S) v
x : β → ℕ
hx : v ⊗ x ∈ S
t : γ → ℕ
ht : ↑p ((v ⊗ x) ⊗ t) = 0
b : γ
⊢ ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inr b) = ((v ⊗ x) ⊗ t) (inr b)
[PROOFSTEP]
rfl
[GOAL]
α β γ✝ : Type u
S✝ S' : Set (α → ℕ)
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : setOf (fun v => ∃ x, v ⊗ x ∈ S) v
x : β → ℕ
hx : v ⊗ x ∈ S
t : γ → ℕ
ht : ↑p ((v ⊗ x) ⊗ t) = 0
⊢ ↑p ((v ⊗ x) ⊗ t) = 0
[PROOFSTEP]
exact ht
[GOAL]
α β γ✝ : Type u
S✝ S' : Set (α → ℕ)
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, ↑(Poly.map ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr) p) (v ⊗ t) = 0
t : β ⊕ γ → ℕ
ht : ↑(Poly.map ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr) p) (v ⊗ t) = 0
⊢ ↑p ((v ⊗ t ∘ inl) ⊗ t ∘ inr) = 0
[PROOFSTEP]
simp at ht 
[GOAL]
α β γ✝ : Type u
S✝ S' : Set (α → ℕ)
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, ↑(Poly.map ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr) p) (v ⊗ t) = 0
t : β ⊕ γ → ℕ
ht : ↑p ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) = 0
⊢ ↑p ((v ⊗ t ∘ inl) ⊗ t ∘ inr) = 0
[PROOFSTEP]
rwa [show (v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr) = (v ⊗ t ∘ inl) ⊗ t ∘ inr from
    funext fun s => by
      cases' s with a b <;>
        try {cases a <;> rfl
        };
      rfl] at
  ht 
[GOAL]
α β γ✝ : Type u
S✝ S' : Set (α → ℕ)
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, ↑(Poly.map ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr) p) (v ⊗ t) = 0
t : β ⊕ γ → ℕ
ht : ↑p ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) = 0
s : (α ⊕ β) ⊕ γ
⊢ ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) s = ((v ⊗ t ∘ inl) ⊗ t ∘ inr) s
[PROOFSTEP]
cases' s with a b
[GOAL]
case inl
α β γ✝ : Type u
S✝ S' : Set (α → ℕ)
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, ↑(Poly.map ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr) p) (v ⊗ t) = 0
t : β ⊕ γ → ℕ
ht : ↑p ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) = 0
a : α ⊕ β
⊢ ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inl a) = ((v ⊗ t ∘ inl) ⊗ t ∘ inr) (inl a)
[PROOFSTEP]
try {cases a <;> rfl
}
[GOAL]
case inl
α β γ✝ : Type u
S✝ S' : Set (α → ℕ)
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, ↑(Poly.map ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr) p) (v ⊗ t) = 0
t : β ⊕ γ → ℕ
ht : ↑p ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) = 0
a : α ⊕ β
⊢ ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inl a) = ((v ⊗ t ∘ inl) ⊗ t ∘ inr) (inl a)
[PROOFSTEP]
{cases a <;> rfl
}
[GOAL]
case inl
α β γ✝ : Type u
S✝ S' : Set (α → ℕ)
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, ↑(Poly.map ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr) p) (v ⊗ t) = 0
t : β ⊕ γ → ℕ
ht : ↑p ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) = 0
a : α ⊕ β
⊢ ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inl a) = ((v ⊗ t ∘ inl) ⊗ t ∘ inr) (inl a)
[PROOFSTEP]
cases a
[GOAL]
case inl.inl
α β γ✝ : Type u
S✝ S' : Set (α → ℕ)
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, ↑(Poly.map ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr) p) (v ⊗ t) = 0
t : β ⊕ γ → ℕ
ht : ↑p ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) = 0
val✝ : α
⊢ ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inl (inl val✝)) = ((v ⊗ t ∘ inl) ⊗ t ∘ inr) (inl (inl val✝))
[PROOFSTEP]
rfl
[GOAL]
case inl.inr
α β γ✝ : Type u
S✝ S' : Set (α → ℕ)
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, ↑(Poly.map ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr) p) (v ⊗ t) = 0
t : β ⊕ γ → ℕ
ht : ↑p ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) = 0
val✝ : β
⊢ ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inl (inr val✝)) = ((v ⊗ t ∘ inl) ⊗ t ∘ inr) (inl (inr val✝))
[PROOFSTEP]
rfl
[GOAL]
case inr
α β γ✝ : Type u
S✝ S' : Set (α → ℕ)
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, ↑(Poly.map ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr) p) (v ⊗ t) = 0
t : β ⊕ γ → ℕ
ht : ↑p ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) = 0
b : γ
⊢ ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inr b) = ((v ⊗ t ∘ inl) ⊗ t ∘ inr) (inr b)
[PROOFSTEP]
try {cases a <;> rfl
}
[GOAL]
case inr
α β γ✝ : Type u
S✝ S' : Set (α → ℕ)
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, ↑(Poly.map ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr) p) (v ⊗ t) = 0
t : β ⊕ γ → ℕ
ht : ↑p ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) = 0
b : γ
⊢ ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inr b) = ((v ⊗ t ∘ inl) ⊗ t ∘ inr) (inr b)
[PROOFSTEP]
{cases a <;> rfl
}
[GOAL]
case inr
α β γ✝ : Type u
S✝ S' : Set (α → ℕ)
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, ↑(Poly.map ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr) p) (v ⊗ t) = 0
t : β ⊕ γ → ℕ
ht : ↑p ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) = 0
b : γ
⊢ ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inr b) = ((v ⊗ t ∘ inl) ⊗ t ∘ inr) (inr b)
[PROOFSTEP]
cases a
[GOAL]
case inr
α β γ✝ : Type u
S✝ S' : Set (α → ℕ)
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, ↑(Poly.map ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr) p) (v ⊗ t) = 0
t : β ⊕ γ → ℕ
ht : ↑p ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) = 0
b : γ
⊢ ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inr b) = ((v ⊗ t ∘ inl) ⊗ t ∘ inr) (inr b)
[PROOFSTEP]
rfl
[GOAL]
α β✝ γ : Type u
S✝ S' : Set (α → ℕ)
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : setOf (fun v => ∃ x, x ::ₒ v ∈ S) v
x : ℕ
hx : x ::ₒ v ∈ S
t : β → ℕ
ht : ↑p (x ::ₒ v ⊗ t) = 0
⊢ ↑(Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p) (v ⊗ x ::ₒ t) = 0
[PROOFSTEP]
simp
[GOAL]
α β✝ γ : Type u
S✝ S' : Set (α → ℕ)
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : setOf (fun v => ∃ x, x ::ₒ v ∈ S) v
x : ℕ
hx : x ::ₒ v ∈ S
t : β → ℕ
ht : ↑p (x ::ₒ v ⊗ t) = 0
⊢ ↑p ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) = 0
[PROOFSTEP]
rw [show (v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some) = x ::ₒ v ⊗ t from
    funext fun s => by
      cases' s with a b <;>
        try {cases a <;> rfl
        };
      rfl]
[GOAL]
α β✝ γ : Type u
S✝ S' : Set (α → ℕ)
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : setOf (fun v => ∃ x, x ::ₒ v ∈ S) v
x : ℕ
hx : x ::ₒ v ∈ S
t : β → ℕ
ht : ↑p (x ::ₒ v ⊗ t) = 0
s : Option α ⊕ β
⊢ ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) s = (x ::ₒ v ⊗ t) s
[PROOFSTEP]
cases' s with a b
[GOAL]
case inl
α β✝ γ : Type u
S✝ S' : Set (α → ℕ)
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : setOf (fun v => ∃ x, x ::ₒ v ∈ S) v
x : ℕ
hx : x ::ₒ v ∈ S
t : β → ℕ
ht : ↑p (x ::ₒ v ⊗ t) = 0
a : Option α
⊢ ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inl a) = (x ::ₒ v ⊗ t) (inl a)
[PROOFSTEP]
try {cases a <;> rfl
}
[GOAL]
case inl
α β✝ γ : Type u
S✝ S' : Set (α → ℕ)
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : setOf (fun v => ∃ x, x ::ₒ v ∈ S) v
x : ℕ
hx : x ::ₒ v ∈ S
t : β → ℕ
ht : ↑p (x ::ₒ v ⊗ t) = 0
a : Option α
⊢ ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inl a) = (x ::ₒ v ⊗ t) (inl a)
[PROOFSTEP]
{cases a <;> rfl
}
[GOAL]
case inl
α β✝ γ : Type u
S✝ S' : Set (α → ℕ)
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : setOf (fun v => ∃ x, x ::ₒ v ∈ S) v
x : ℕ
hx : x ::ₒ v ∈ S
t : β → ℕ
ht : ↑p (x ::ₒ v ⊗ t) = 0
a : Option α
⊢ ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inl a) = (x ::ₒ v ⊗ t) (inl a)
[PROOFSTEP]
cases a
[GOAL]
case inl.none
α β✝ γ : Type u
S✝ S' : Set (α → ℕ)
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : setOf (fun v => ∃ x, x ::ₒ v ∈ S) v
x : ℕ
hx : x ::ₒ v ∈ S
t : β → ℕ
ht : ↑p (x ::ₒ v ⊗ t) = 0
⊢ ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inl none) = (x ::ₒ v ⊗ t) (inl none)
[PROOFSTEP]
rfl
[GOAL]
case inl.some
α β✝ γ : Type u
S✝ S' : Set (α → ℕ)
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : setOf (fun v => ∃ x, x ::ₒ v ∈ S) v
x : ℕ
hx : x ::ₒ v ∈ S
t : β → ℕ
ht : ↑p (x ::ₒ v ⊗ t) = 0
val✝ : α
⊢ ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inl (some val✝)) = (x ::ₒ v ⊗ t) (inl (some val✝))
[PROOFSTEP]
rfl
[GOAL]
case inr
α β✝ γ : Type u
S✝ S' : Set (α → ℕ)
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : setOf (fun v => ∃ x, x ::ₒ v ∈ S) v
x : ℕ
hx : x ::ₒ v ∈ S
t : β → ℕ
ht : ↑p (x ::ₒ v ⊗ t) = 0
b : β
⊢ ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inr b) = (x ::ₒ v ⊗ t) (inr b)
[PROOFSTEP]
try {cases a <;> rfl
}
[GOAL]
case inr
α β✝ γ : Type u
S✝ S' : Set (α → ℕ)
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : setOf (fun v => ∃ x, x ::ₒ v ∈ S) v
x : ℕ
hx : x ::ₒ v ∈ S
t : β → ℕ
ht : ↑p (x ::ₒ v ⊗ t) = 0
b : β
⊢ ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inr b) = (x ::ₒ v ⊗ t) (inr b)
[PROOFSTEP]
{cases a <;> rfl
}
[GOAL]
case inr
α β✝ γ : Type u
S✝ S' : Set (α → ℕ)
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : setOf (fun v => ∃ x, x ::ₒ v ∈ S) v
x : ℕ
hx : x ::ₒ v ∈ S
t : β → ℕ
ht : ↑p (x ::ₒ v ⊗ t) = 0
b : β
⊢ ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inr b) = (x ::ₒ v ⊗ t) (inr b)
[PROOFSTEP]
cases a
[GOAL]
case inr
α β✝ γ : Type u
S✝ S' : Set (α → ℕ)
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : setOf (fun v => ∃ x, x ::ₒ v ∈ S) v
x : ℕ
hx : x ::ₒ v ∈ S
t : β → ℕ
ht : ↑p (x ::ₒ v ⊗ t) = 0
b : β
⊢ ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inr b) = (x ::ₒ v ⊗ t) (inr b)
[PROOFSTEP]
rfl
[GOAL]
α β✝ γ : Type u
S✝ S' : Set (α → ℕ)
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : setOf (fun v => ∃ x, x ::ₒ v ∈ S) v
x : ℕ
hx : x ::ₒ v ∈ S
t : β → ℕ
ht : ↑p (x ::ₒ v ⊗ t) = 0
⊢ ↑p (x ::ₒ v ⊗ t) = 0
[PROOFSTEP]
exact ht
[GOAL]
α β✝ γ : Type u
S✝ S' : Set (α → ℕ)
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, ↑(Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p) (v ⊗ t) = 0
t : Option β → ℕ
ht : ↑(Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p) (v ⊗ t) = 0
⊢ ↑p (t none ::ₒ v ⊗ t ∘ some) = 0
[PROOFSTEP]
simp at ht 
[GOAL]
α β✝ γ : Type u
S✝ S' : Set (α → ℕ)
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, ↑(Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p) (v ⊗ t) = 0
t : Option β → ℕ
ht : ↑p ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) = 0
⊢ ↑p (t none ::ₒ v ⊗ t ∘ some) = 0
[PROOFSTEP]
rwa [show (v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some) = t none ::ₒ v ⊗ t ∘ some from
    funext fun s => by
      cases' s with a b <;>
        try {cases a <;> rfl
        };
      rfl] at
  ht 
[GOAL]
α β✝ γ : Type u
S✝ S' : Set (α → ℕ)
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, ↑(Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p) (v ⊗ t) = 0
t : Option β → ℕ
ht : ↑p ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) = 0
s : Option α ⊕ β
⊢ ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) s = (t none ::ₒ v ⊗ t ∘ some) s
[PROOFSTEP]
cases' s with a b
[GOAL]
case inl
α β✝ γ : Type u
S✝ S' : Set (α → ℕ)
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, ↑(Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p) (v ⊗ t) = 0
t : Option β → ℕ
ht : ↑p ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) = 0
a : Option α
⊢ ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inl a) = (t none ::ₒ v ⊗ t ∘ some) (inl a)
[PROOFSTEP]
try {cases a <;> rfl
}
[GOAL]
case inl
α β✝ γ : Type u
S✝ S' : Set (α → ℕ)
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, ↑(Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p) (v ⊗ t) = 0
t : Option β → ℕ
ht : ↑p ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) = 0
a : Option α
⊢ ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inl a) = (t none ::ₒ v ⊗ t ∘ some) (inl a)
[PROOFSTEP]
{cases a <;> rfl
}
[GOAL]
case inl
α β✝ γ : Type u
S✝ S' : Set (α → ℕ)
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, ↑(Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p) (v ⊗ t) = 0
t : Option β → ℕ
ht : ↑p ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) = 0
a : Option α
⊢ ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inl a) = (t none ::ₒ v ⊗ t ∘ some) (inl a)
[PROOFSTEP]
cases a
[GOAL]
case inl.none
α β✝ γ : Type u
S✝ S' : Set (α → ℕ)
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, ↑(Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p) (v ⊗ t) = 0
t : Option β → ℕ
ht : ↑p ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) = 0
⊢ ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inl none) = (t none ::ₒ v ⊗ t ∘ some) (inl none)
[PROOFSTEP]
rfl
[GOAL]
case inl.some
α β✝ γ : Type u
S✝ S' : Set (α → ℕ)
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, ↑(Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p) (v ⊗ t) = 0
t : Option β → ℕ
ht : ↑p ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) = 0
val✝ : α
⊢ ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inl (some val✝)) = (t none ::ₒ v ⊗ t ∘ some) (inl (some val✝))
[PROOFSTEP]
rfl
[GOAL]
case inr
α β✝ γ : Type u
S✝ S' : Set (α → ℕ)
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, ↑(Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p) (v ⊗ t) = 0
t : Option β → ℕ
ht : ↑p ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) = 0
b : β
⊢ ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inr b) = (t none ::ₒ v ⊗ t ∘ some) (inr b)
[PROOFSTEP]
try {cases a <;> rfl
}
[GOAL]
case inr
α β✝ γ : Type u
S✝ S' : Set (α → ℕ)
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, ↑(Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p) (v ⊗ t) = 0
t : Option β → ℕ
ht : ↑p ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) = 0
b : β
⊢ ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inr b) = (t none ::ₒ v ⊗ t ∘ some) (inr b)
[PROOFSTEP]
{cases a <;> rfl
}
[GOAL]
case inr
α β✝ γ : Type u
S✝ S' : Set (α → ℕ)
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, ↑(Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p) (v ⊗ t) = 0
t : Option β → ℕ
ht : ↑p ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) = 0
b : β
⊢ ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inr b) = (t none ::ₒ v ⊗ t ∘ some) (inr b)
[PROOFSTEP]
cases a
[GOAL]
case inr
α β✝ γ : Type u
S✝ S' : Set (α → ℕ)
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, ↑p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, ↑(Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p) (v ⊗ t) = 0
t : Option β → ℕ
ht : ↑p ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) = 0
b : β
⊢ ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inr b) = (t none ::ₒ v ⊗ t ∘ some) (inr b)
[PROOFSTEP]
rfl
[GOAL]
α β γ : Type u
S S' : Set (α → ℕ)
f : (α → ℕ) → ℕ
⊢ DiophFn f = DiophPfun ↑f
[PROOFSTEP]
refine' congr_arg Dioph (Set.ext fun v => _)
[GOAL]
α β γ : Type u
S S' : Set (α → ℕ)
f : (α → ℕ) → ℕ
v : Option α → ℕ
⊢ v ∈ {v | f (v ∘ some) = v none} ↔ v ∈ {v | PFun.graph ↑f (v ∘ some, v none)}
[PROOFSTEP]
exact PFun.lift_graph.symm
[GOAL]
α β γ : Type u
S S' : Set (α → ℕ)
p : Poly α
v : Option α → ℕ
⊢ setOf (fun v => (fun v => Int.natAbs (↑p v)) (v ∘ some) = v none) v ↔
    ↑((Poly.map some p - Poly.proj none) * (Poly.map some p + Poly.proj none)) v = 0
[PROOFSTEP]
dsimp
[GOAL]
α β γ : Type u
S S' : Set (α → ℕ)
p : Poly α
v : Option α → ℕ
⊢ setOf (fun v => Int.natAbs (↑p (v ∘ some)) = v none) v ↔ (↑p (v ∘ some) - ↑(v none)) * (↑p (v ∘ some) + ↑(v none)) = 0
[PROOFSTEP]
exact Int.eq_natAbs_iff_mul_eq_zero
[GOAL]
α β γ : Type u
S✝ S' : Set (α → ℕ)
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPfun f
v : α → ℕ
x✝ : v ∈ {v | ∃ x, x ::ₒ v ∈ S ∩ {v | PFun.graph f (v ∘ some, v none)}}
x : ℕ
hS : x ::ₒ v ∈ S
h : ∃ h, Part.get (f ((x ::ₒ v) ∘ some, (x ::ₒ v) none).fst) h = ((x ::ₒ v) ∘ some, (x ::ₒ v) none).snd
⊢ v ∈ {v | ∃ h, PFun.fn f v h ::ₒ v ∈ S}
[PROOFSTEP]
rw [show (x ::ₒ v) ∘ some = v from funext fun s => rfl] at h 
[GOAL]
α β γ : Type u
S✝ S' : Set (α → ℕ)
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPfun f
v : α → ℕ
x✝ : v ∈ {v | ∃ x, x ::ₒ v ∈ S ∩ {v | PFun.graph f (v ∘ some, v none)}}
x : ℕ
hS : x ::ₒ v ∈ S
h : ∃ h, Part.get (f (v, (x ::ₒ v) none).fst) h = (v, (x ::ₒ v) none).snd
⊢ v ∈ {v | ∃ h, PFun.fn f v h ::ₒ v ∈ S}
[PROOFSTEP]
cases' h with hf h
[GOAL]
case intro
α β γ : Type u
S✝ S' : Set (α → ℕ)
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPfun f
v : α → ℕ
x✝ : v ∈ {v | ∃ x, x ::ₒ v ∈ S ∩ {v | PFun.graph f (v ∘ some, v none)}}
x : ℕ
hS : x ::ₒ v ∈ S
hf : (f (v, (x ::ₒ v) none).fst).Dom
h : Part.get (f (v, (x ::ₒ v) none).fst) hf = (v, (x ::ₒ v) none).snd
⊢ v ∈ {v | ∃ h, PFun.fn f v h ::ₒ v ∈ S}
[PROOFSTEP]
refine' ⟨hf, _⟩
[GOAL]
case intro
α β γ : Type u
S✝ S' : Set (α → ℕ)
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPfun f
v : α → ℕ
x✝ : v ∈ {v | ∃ x, x ::ₒ v ∈ S ∩ {v | PFun.graph f (v ∘ some, v none)}}
x : ℕ
hS : x ::ₒ v ∈ S
hf : (f (v, (x ::ₒ v) none).fst).Dom
h : Part.get (f (v, (x ::ₒ v) none).fst) hf = (v, (x ::ₒ v) none).snd
⊢ PFun.fn f v hf ::ₒ v ∈ S
[PROOFSTEP]
rw [PFun.fn, h]
[GOAL]
case intro
α β γ : Type u
S✝ S' : Set (α → ℕ)
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPfun f
v : α → ℕ
x✝ : v ∈ {v | ∃ x, x ::ₒ v ∈ S ∩ {v | PFun.graph f (v ∘ some, v none)}}
x : ℕ
hS : x ::ₒ v ∈ S
hf : (f (v, (x ::ₒ v) none).fst).Dom
h : Part.get (f (v, (x ::ₒ v) none).fst) hf = (v, (x ::ₒ v) none).snd
⊢ (v, (x ::ₒ v) none).snd ::ₒ v ∈ S
[PROOFSTEP]
exact hS
[GOAL]
α β γ : Type u
S✝ S' : Set (α → ℕ)
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPfun f
v : α → ℕ
x✝ : v ∈ {v | ∃ h, PFun.fn f v h ::ₒ v ∈ S}
x : PFun.Dom f v
hS : PFun.fn f v x ::ₒ v ∈ S
⊢ ∃ h,
    Part.get (f ((PFun.fn f v x ::ₒ v) ∘ some, (PFun.fn f v x ::ₒ v) none).fst) h =
      ((PFun.fn f v x ::ₒ v) ∘ some, (PFun.fn f v x ::ₒ v) none).snd
[PROOFSTEP]
rw [show (f.fn v x ::ₒ v) ∘ some = v from funext fun s => rfl]
[GOAL]
α β γ : Type u
S✝ S' : Set (α → ℕ)
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPfun f
v : α → ℕ
x✝ : v ∈ {v | ∃ h, PFun.fn f v h ::ₒ v ∈ S}
x : PFun.Dom f v
hS : PFun.fn f v x ::ₒ v ∈ S
⊢ ∃ h, Part.get (f (v, (PFun.fn f v x ::ₒ v) none).fst) h = (v, (PFun.fn f v x ::ₒ v) none).snd
[PROOFSTEP]
exact ⟨x, rfl⟩
[GOAL]
α β : Type
n : ℕ
S : Set (Vector3 ℕ (succ n))
d : Dioph S
f : Vector3 ℕ n → ℕ
df : DiophFn f
v : Fin2 n → ℕ
⊢ v ∈ {v | f v ::ₒ v ∈ {v | (v ∘ none :: some) ∈ S}} ↔ v ∈ {v | (f v :: v) ∈ S}
[PROOFSTEP]
dsimp
  -- Porting note: `congr` use to be enough here
[GOAL]
α β : Type
n : ℕ
S : Set (Vector3 ℕ (succ n))
d : Dioph S
f : Vector3 ℕ n → ℕ
df : DiophFn f
v : Fin2 n → ℕ
⊢ ((f v ::ₒ v) ∘ none :: some) ∈ S ↔ v ∈ {v | (f v :: v) ∈ S}
[PROOFSTEP]
refine iff_of_eq (congrFun (congrArg Membership.mem ?_) S)
[GOAL]
α β : Type
n : ℕ
S : Set (Vector3 ℕ (succ n))
d : Dioph S
f : Vector3 ℕ n → ℕ
df : DiophFn f
v : Fin2 n → ℕ
⊢ ((f v ::ₒ v) ∘ none :: some) = f v :: v
[PROOFSTEP]
ext x
[GOAL]
case h
α β : Type
n : ℕ
S : Set (Vector3 ℕ (succ n))
d : Dioph S
f : Vector3 ℕ n → ℕ
df : DiophFn f
v : Fin2 n → ℕ
x : Fin2 (succ n)
⊢ ((f v ::ₒ v) ∘ none :: some) x = (f v :: v) x
[PROOFSTEP]
cases x
[GOAL]
case h.fz
α β : Type
n : ℕ
S : Set (Vector3 ℕ (succ n))
d : Dioph S
f : Vector3 ℕ n → ℕ
df : DiophFn f
v : Fin2 n → ℕ
⊢ ((f v ::ₒ v) ∘ none :: some) fz = (f v :: v) fz
[PROOFSTEP]
rfl
[GOAL]
case h.fs
α β : Type
n : ℕ
S : Set (Vector3 ℕ (succ n))
d : Dioph S
f : Vector3 ℕ n → ℕ
df : DiophFn f
v : Fin2 n → ℕ
a✝ : Fin2 n
⊢ ((f v ::ₒ v) ∘ none :: some) (fs a✝) = (f v :: v) (fs a✝)
[PROOFSTEP]
rfl
[GOAL]
α β : Type
n✝ n : ℕ
S : Set (Vector3 ℕ (succ n))
d : Dioph S
v : Fin2 n → ℕ
x : ℕ
⊢ x ::ₒ v ∈ {v | (v ∘ none :: some) ∈ S} ↔ (x :: v) ∈ S
[PROOFSTEP]
dsimp
[GOAL]
α β : Type
n✝ n : ℕ
S : Set (Vector3 ℕ (succ n))
d : Dioph S
v : Fin2 n → ℕ
x : ℕ
⊢ ((x ::ₒ v) ∘ none :: some) ∈ S ↔ (x :: v) ∈ S
[PROOFSTEP]
rw [show Option.elim' x v ∘ cons none some = x :: v from funext fun s => by cases' s with a b <;> rfl]
[GOAL]
α β : Type
n✝ n : ℕ
S : Set (Vector3 ℕ (succ n))
d : Dioph S
v : Fin2 n → ℕ
x : ℕ
s : Fin2 (succ n)
⊢ ((x ::ₒ v) ∘ none :: some) s = (x :: v) s
[PROOFSTEP]
cases' s with a b
[GOAL]
case fz
α β : Type
n✝ n : ℕ
S : Set (Vector3 ℕ (succ n))
d : Dioph S
v : Fin2 n → ℕ
x : ℕ
⊢ ((x ::ₒ v) ∘ none :: some) fz = (x :: v) fz
[PROOFSTEP]
rfl
[GOAL]
case fs
α β : Type
n✝ n : ℕ
S : Set (Vector3 ℕ (succ n))
d : Dioph S
v : Fin2 n → ℕ
x : ℕ
a✝ : Fin2 n
⊢ ((x ::ₒ v) ∘ none :: some) (fs a✝) = (x :: v) (fs a✝)
[PROOFSTEP]
rfl
[GOAL]
α β : Type
n : ℕ
S : Set (α ⊕ Fin2 0 → ℕ)
d : Dioph S
f : Vector3 ((α → ℕ) → ℕ) 0
x✝ : VectorAllP DiophFn f
v : α → ℕ
⊢ v ∈ {v | v ∘ (id ⊗ elim0) ∈ S} ↔ v ∈ {v | (v ⊗ fun i => f i v) ∈ S}
[PROOFSTEP]
dsimp
  -- Porting note: `congr` use to be enough here
[GOAL]
α β : Type
n : ℕ
S : Set (α ⊕ Fin2 0 → ℕ)
d : Dioph S
f : Vector3 ((α → ℕ) → ℕ) 0
x✝ : VectorAllP DiophFn f
v : α → ℕ
⊢ v ∘ (id ⊗ elim0) ∈ S ↔ (v ⊗ fun i => f i v) ∈ S
[PROOFSTEP]
refine iff_of_eq (congrFun (congrArg Membership.mem ?_) S)
[GOAL]
α β : Type
n : ℕ
S : Set (α ⊕ Fin2 0 → ℕ)
d : Dioph S
f : Vector3 ((α → ℕ) → ℕ) 0
x✝ : VectorAllP DiophFn f
v : α → ℕ
⊢ v ∘ (id ⊗ elim0) = v ⊗ fun i => f i v
[PROOFSTEP]
ext x
[GOAL]
case h
α β : Type
n : ℕ
S : Set (α ⊕ Fin2 0 → ℕ)
d : Dioph S
f : Vector3 ((α → ℕ) → ℕ) 0
x✝ : VectorAllP DiophFn f
v : α → ℕ
x : α ⊕ Fin2 0
⊢ (v ∘ (id ⊗ elim0)) x = (v ⊗ fun i => f i v) x
[PROOFSTEP]
obtain _ | _ | _ := x
[GOAL]
case h.inl
α β : Type
n : ℕ
S : Set (α ⊕ Fin2 0 → ℕ)
d : Dioph S
f : Vector3 ((α → ℕ) → ℕ) 0
x✝ : VectorAllP DiophFn f
v : α → ℕ
val✝ : α
⊢ (v ∘ (id ⊗ elim0)) (inl val✝) = (v ⊗ fun i => f i v) (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
α β : Type
n✝ n : ℕ
S : Set (α ⊕ Fin2 (succ n) → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) (succ n)
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
⊢ VectorAllP DiophFn (f :: fl) → Dioph {v | (v ⊗ fun i => (f :: fl) i v) ∈ S}
[PROOFSTEP]
simp
[GOAL]
α β : Type
n✝ n : ℕ
S : Set (α ⊕ Fin2 (succ n) → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) (succ n)
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
⊢ DiophFn f → VectorAllP DiophFn fl → Dioph {v | (v ⊗ fun i => (f :: fl) i v) ∈ S}
[PROOFSTEP]
exact fun df dfl =>
  have : Dioph {v | (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S} :=
    ext (diophFn_comp1 (reindex_dioph _ (some ∘ inl ⊗ none :: some ∘ inr) d) <| reindex_diophFn inl df) fun v =>
      by
      dsimp
        -- Porting note: `congr` use to be enough here
      refine iff_of_eq (congrFun (congrArg Membership.mem ?_) S)
      ext x; obtain _ | _ | _ := x <;> rfl
  have : Dioph {v | (v ⊗ f v :: fun i : Fin2 n => fl i v) ∈ S} :=
    @diophFn_compn n (fun v => S (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr)) this _ dfl
  ext this fun v => by
    dsimp;
    -- Porting note: `congr` use to be enough hererefine iff_of_eq (congrFun (congrArg Membership.mem ?_) S)
    ext x; obtain _ | _ | _ := x <;> rfl
[GOAL]
α β : Type
n✝ n : ℕ
S : Set (α ⊕ Fin2 (succ n) → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) (succ n)
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
v : α ⊕ Fin2 n → ℕ
⊢ v ∈ {v | f (v ∘ inl) ::ₒ v ∈ {v | v ∘ (some ∘ inl ⊗ none :: some ∘ inr) ∈ S}} ↔
    v ∈ {v | (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S}
[PROOFSTEP]
dsimp
  -- Porting note: `congr` use to be enough here
[GOAL]
α β : Type
n✝ n : ℕ
S : Set (α ⊕ Fin2 (succ n) → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) (succ n)
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
v : α ⊕ Fin2 n → ℕ
⊢ (f (v ∘ inl) ::ₒ v) ∘ (some ∘ inl ⊗ none :: some ∘ inr) ∈ S ↔ (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S
[PROOFSTEP]
refine iff_of_eq (congrFun (congrArg Membership.mem ?_) S)
[GOAL]
α β : Type
n✝ n : ℕ
S : Set (α ⊕ Fin2 (succ n) → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) (succ n)
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
v : α ⊕ Fin2 n → ℕ
⊢ (f (v ∘ inl) ::ₒ v) ∘ (some ∘ inl ⊗ none :: some ∘ inr) = v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr
[PROOFSTEP]
ext x
[GOAL]
case h
α β : Type
n✝ n : ℕ
S : Set (α ⊕ Fin2 (succ n) → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) (succ n)
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
v : α ⊕ Fin2 n → ℕ
x : α ⊕ Fin2 (succ n)
⊢ ((f (v ∘ inl) ::ₒ v) ∘ (some ∘ inl ⊗ none :: some ∘ inr)) x = (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) x
[PROOFSTEP]
obtain _ | _ | _ := x
[GOAL]
case h.inl
α β : Type
n✝ n : ℕ
S : Set (α ⊕ Fin2 (succ n) → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) (succ n)
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
v : α ⊕ Fin2 n → ℕ
val✝ : α
⊢ ((f (v ∘ inl) ::ₒ v) ∘ (some ∘ inl ⊗ none :: some ∘ inr)) (inl val✝) = (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case h.inr.fz
α β : Type
n✝ n : ℕ
S : Set (α ⊕ Fin2 (succ n) → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) (succ n)
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
v : α ⊕ Fin2 n → ℕ
⊢ ((f (v ∘ inl) ::ₒ v) ∘ (some ∘ inl ⊗ none :: some ∘ inr)) (inr fz) = (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) (inr fz)
[PROOFSTEP]
rfl
[GOAL]
case h.inr.fs
α β : Type
n✝ n : ℕ
S : Set (α ⊕ Fin2 (succ n) → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) (succ n)
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
v : α ⊕ Fin2 n → ℕ
a✝ : Fin2 n
⊢ ((f (v ∘ inl) ::ₒ v) ∘ (some ∘ inl ⊗ none :: some ∘ inr)) (inr (fs a✝)) =
    (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) (inr (fs a✝))
[PROOFSTEP]
rfl
[GOAL]
α β : Type
n✝ n : ℕ
S : Set (α ⊕ Fin2 (succ n) → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) (succ n)
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
this✝ : Dioph {v | (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S}
this : Dioph {v | (v ⊗ f v :: fun i => fl i v) ∈ S}
v : α → ℕ
⊢ v ∈ {v | (v ⊗ f v :: fun i => fl i v) ∈ S} ↔ v ∈ {v | (v ⊗ fun i => (f :: fl) i v) ∈ S}
[PROOFSTEP]
dsimp
[GOAL]
α β : Type
n✝ n : ℕ
S : Set (α ⊕ Fin2 (succ n) → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) (succ n)
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
this✝ : Dioph {v | (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S}
this : Dioph {v | (v ⊗ f v :: fun i => fl i v) ∈ S}
v : α → ℕ
⊢ (v ⊗ f v :: fun i => fl i v) ∈ S ↔ (v ⊗ fun i => (f :: fl) i v) ∈ S
[PROOFSTEP]
refine iff_of_eq (congrFun (congrArg Membership.mem ?_) S)
[GOAL]
α β : Type
n✝ n : ℕ
S : Set (α ⊕ Fin2 (succ n) → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) (succ n)
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
this✝ : Dioph {v | (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S}
this : Dioph {v | (v ⊗ f v :: fun i => fl i v) ∈ S}
v : α → ℕ
⊢ (v ⊗ f v :: fun i => fl i v) = v ⊗ fun i => (f :: fl) i v
[PROOFSTEP]
ext x
[GOAL]
case h
α β : Type
n✝ n : ℕ
S : Set (α ⊕ Fin2 (succ n) → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) (succ n)
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
this✝ : Dioph {v | (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S}
this : Dioph {v | (v ⊗ f v :: fun i => fl i v) ∈ S}
v : α → ℕ
x : α ⊕ Fin2 (succ n)
⊢ (v ⊗ f v :: fun i => fl i v) x = (v ⊗ fun i => (f :: fl) i v) x
[PROOFSTEP]
obtain _ | _ | _ := x
[GOAL]
case h.inl
α β : Type
n✝ n : ℕ
S : Set (α ⊕ Fin2 (succ n) → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) (succ n)
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
this✝ : Dioph {v | (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S}
this : Dioph {v | (v ⊗ f v :: fun i => fl i v) ∈ S}
v : α → ℕ
val✝ : α
⊢ (v ⊗ f v :: fun i => fl i v) (inl val✝) = (v ⊗ fun i => (f :: fl) i v) (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case h.inr.fz
α β : Type
n✝ n : ℕ
S : Set (α ⊕ Fin2 (succ n) → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) (succ n)
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
this✝ : Dioph {v | (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S}
this : Dioph {v | (v ⊗ f v :: fun i => fl i v) ∈ S}
v : α → ℕ
⊢ (v ⊗ f v :: fun i => fl i v) (inr fz) = (v ⊗ fun i => (f :: fl) i v) (inr fz)
[PROOFSTEP]
rfl
[GOAL]
case h.inr.fs
α β : Type
n✝ n : ℕ
S : Set (α ⊕ Fin2 (succ n) → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) (succ n)
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
this✝ : Dioph {v | (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S}
this : Dioph {v | (v ⊗ f v :: fun i => fl i v) ∈ S}
v : α → ℕ
a✝ : Fin2 n
⊢ (v ⊗ f v :: fun i => fl i v) (inr (fs a✝)) = (v ⊗ fun i => (f :: fl) i v) (inr (fs a✝))
[PROOFSTEP]
rfl
[GOAL]
α β : Type
n : ℕ
f : Vector3 ℕ n → ℕ
df : DiophFn f
g : Vector3 ((α → ℕ) → ℕ) n
dg : VectorAllP DiophFn g
⊢ VectorAllP DiophFn ((fun v => v none) :: fun i v => g i (v ∘ some))
[PROOFSTEP]
simp
[GOAL]
α β : Type
n : ℕ
f : Vector3 ℕ n → ℕ
df : DiophFn f
g : Vector3 ((α → ℕ) → ℕ) n
dg : VectorAllP DiophFn g
⊢ (DiophFn fun v => v none) ∧ VectorAllP DiophFn fun i v => g i (v ∘ some)
[PROOFSTEP]
exact ⟨proj_dioph none, (vectorAllP_iff_forall _ _).2 fun i => reindex_diophFn _ <| (vectorAllP_iff_forall _ _).1 dg _⟩
[GOAL]
α β : Type
n : ℕ
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
v : Fin2 2 → ℕ
⊢ v &0 = v &1 ↔ ↑(Poly.proj &0 - Poly.proj &1) v = 0
[PROOFSTEP]
exact Int.ofNat_inj.symm.trans ⟨@sub_eq_zero_of_eq ℤ _ (v &0) (v &1), eq_of_sub_eq_zero⟩
[GOAL]
α β : Type
n : ℕ
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
v : α → ℕ
⊢ v ∈ {v | f v < g v} ∪ {v | g v < f v} ↔ v ∈ {v | f v ≠ g v}
[PROOFSTEP]
dsimp
[GOAL]
α β : Type
n : ℕ
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
v : α → ℕ
⊢ v ∈ {v | f v < g v} ∪ {v | g v < f v} ↔ ¬f v = g v
[PROOFSTEP]
exact lt_or_lt_iff_ne (α := ℕ)
[GOAL]
α β : Type
n : ℕ
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
x y z : ℕ
o : y = x + z ∨ y ≤ z ∧ x = 0
⊢ y - z = x
[PROOFSTEP]
rcases o with (ae | ⟨yz, x0⟩)
[GOAL]
case inl
α β : Type
n : ℕ
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
x y z : ℕ
ae : y = x + z
⊢ y - z = x
[PROOFSTEP]
rw [ae, add_tsub_cancel_right]
[GOAL]
case inr.intro
α β : Type
n : ℕ
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
x y z : ℕ
yz : y ≤ z
x0 : x = 0
⊢ y - z = x
[PROOFSTEP]
rw [x0, tsub_eq_zero_iff_le.mpr yz]
[GOAL]
α β : Type
n : ℕ
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
x y z : ℕ
⊢ y - z = x → y = x + z ∨ y ≤ z ∧ x = 0
[PROOFSTEP]
rintro rfl
[GOAL]
α β : Type
n : ℕ
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
y z : ℕ
⊢ y = y - z + z ∨ y ≤ z ∧ y - z = 0
[PROOFSTEP]
cases' le_total y z with yz zy
[GOAL]
case inl
α β : Type
n : ℕ
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
y z : ℕ
yz : y ≤ z
⊢ y = y - z + z ∨ y ≤ z ∧ y - z = 0
[PROOFSTEP]
exact Or.inr ⟨yz, tsub_eq_zero_iff_le.mpr yz⟩
[GOAL]
case inr
α β : Type
n : ℕ
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
y z : ℕ
zy : z ≤ y
⊢ y = y - z + z ∨ y ≤ z ∧ y - z = 0
[PROOFSTEP]
exact Or.inl (tsub_add_cancel_of_le zy).symm
[GOAL]
α β : Type
n : ℕ
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph fun v => (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ x, v &0 + v &2 * x = v &1
z x y : ℕ
x✝ : (y = 0 ∨ z < y) ∧ ∃ c, z + y * c = x
h : y = 0 ∨ z < y
c : ℕ
hc : z + y * c = x
⊢ x % y = z
[PROOFSTEP]
rw [← hc]
[GOAL]
α β : Type
n : ℕ
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph fun v => (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ x, v &0 + v &2 * x = v &1
z x y : ℕ
x✝ : (y = 0 ∨ z < y) ∧ ∃ c, z + y * c = x
h : y = 0 ∨ z < y
c : ℕ
hc : z + y * c = x
⊢ (z + y * c) % y = z
[PROOFSTEP]
simp
[GOAL]
α β : Type
n : ℕ
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph fun v => (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ x, v &0 + v &2 * x = v &1
z x y : ℕ
x✝ : (y = 0 ∨ z < y) ∧ ∃ c, z + y * c = x
h : y = 0 ∨ z < y
c : ℕ
hc : z + y * c = x
⊢ z % y = z
[PROOFSTEP]
cases' h with x0 hl
[GOAL]
case inl
α β : Type
n : ℕ
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph fun v => (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ x, v &0 + v &2 * x = v &1
z x y : ℕ
x✝ : (y = 0 ∨ z < y) ∧ ∃ c, z + y * c = x
c : ℕ
hc : z + y * c = x
x0 : y = 0
⊢ z % y = z
case inr
α β : Type
n : ℕ
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph fun v => (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ x, v &0 + v &2 * x = v &1
z x y : ℕ
x✝ : (y = 0 ∨ z < y) ∧ ∃ c, z + y * c = x
c : ℕ
hc : z + y * c = x
hl : z < y
⊢ z % y = z
[PROOFSTEP]
rw [x0, mod_zero]
[GOAL]
case inr
α β : Type
n : ℕ
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph fun v => (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ x, v &0 + v &2 * x = v &1
z x y : ℕ
x✝ : (y = 0 ∨ z < y) ∧ ∃ c, z + y * c = x
c : ℕ
hc : z + y * c = x
hl : z < y
⊢ z % y = z
[PROOFSTEP]
exact mod_eq_of_lt hl
[GOAL]
α β : Type
n : ℕ
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph fun v => (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ x, v &0 + v &2 * x = v &1
z x y : ℕ
e : x % y = z
⊢ (y = 0 ∨ z < y) ∧ ∃ c, z + y * c = x
[PROOFSTEP]
rw [← e]
[GOAL]
α β : Type
n : ℕ
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph fun v => (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ x, v &0 + v &2 * x = v &1
z x y : ℕ
e : x % y = z
⊢ (y = 0 ∨ x % y < y) ∧ ∃ c, x % y + y * c = x
[PROOFSTEP]
exact ⟨or_iff_not_imp_left.2 fun h => mod_lt _ (Nat.pos_of_ne_zero h), x / y, mod_add_div _ _⟩
[GOAL]
α β : Type
n : ℕ
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph fun v => v &2 = 0 ∧ v &0 = 0 ∨ v &0 * v &2 ≤ v &1 ∧ v &1 < (v &0 + 1) * v &2
z x y : ℕ
⊢ y = 0 ∧ z = 0 ∨ z * y ≤ x ∧ x < (z + 1) * y ↔ x / y = z
[PROOFSTEP]
refine Iff.trans ?_ eq_comm
[GOAL]
α β : Type
n : ℕ
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph fun v => v &2 = 0 ∧ v &0 = 0 ∨ v &0 * v &2 ≤ v &1 ∧ v &1 < (v &0 + 1) * v &2
z x y : ℕ
⊢ y = 0 ∧ z = 0 ∨ z * y ≤ x ∧ x < (z + 1) * y ↔ z = x / y
[PROOFSTEP]
exact
  y.eq_zero_or_pos.elim
    (fun y0 => by
      rw [y0, Nat.div_zero]
      exact ⟨fun o => (o.resolve_right fun ⟨_, h2⟩ => Nat.not_lt_zero _ h2).right, fun z0 => Or.inl ⟨rfl, z0⟩⟩)
    fun ypos =>
    Iff.trans ⟨fun o => o.resolve_left fun ⟨h1, _⟩ => Nat.ne_of_gt ypos h1, Or.inr⟩
      (le_antisymm_iff.trans <|
          and_congr (Nat.le_div_iff_mul_le ypos) <|
            Iff.trans ⟨lt_succ_of_le, le_of_lt_succ⟩ (div_lt_iff_lt_mul ypos)).symm
[GOAL]
α β : Type
n : ℕ
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph fun v => v &2 = 0 ∧ v &0 = 0 ∨ v &0 * v &2 ≤ v &1 ∧ v &1 < (v &0 + 1) * v &2
z x y : ℕ
y0 : y = 0
⊢ y = 0 ∧ z = 0 ∨ z * y ≤ x ∧ x < (z + 1) * y ↔ z = x / y
[PROOFSTEP]
rw [y0, Nat.div_zero]
[GOAL]
α β : Type
n : ℕ
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph fun v => v &2 = 0 ∧ v &0 = 0 ∨ v &0 * v &2 ≤ v &1 ∧ v &1 < (v &0 + 1) * v &2
z x y : ℕ
y0 : y = 0
⊢ 0 = 0 ∧ z = 0 ∨ z * 0 ≤ x ∧ x < (z + 1) * 0 ↔ z = 0
[PROOFSTEP]
exact ⟨fun o => (o.resolve_right fun ⟨_, h2⟩ => Nat.not_lt_zero _ h2).right, fun z0 => Or.inl ⟨rfl, z0⟩⟩
[GOAL]
α β : Type
n : ℕ
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
⊢ Dioph fun v => ∃ h, xn h (v &1) = v &2 ∧ yn h (v &1) = v &3
[PROOFSTEP]
have proof :=
  D.1 D< D&0 D∧
    D&1 D≤ D&3 D∧
      ((D&2 D= D.1 D∧ D&3 D= D.0) D∨
        ((D∃) 4 <|
          (D∃) 5 <|
            (D∃) 6 <|
              (D∃) 7 <|
                (D∃) 8 <|
                  D&7 D* D&7 D- (D&5 D* D&5 D- D.1) D* D&8 D* D&8 D= D.1 D∧
                    D&4 D* D&4 D- (D&5 D* D&5 D- D.1) D* D&3 D* D&3 D= D.1 D∧
                      D&2 D* D&2 D- (D&0 D* D&0 D- D.1) D* D&1 D* D&1 D= D.1 D∧
                        D.1 D< D&0 D∧
                          ( D≡ (D&0) (D.1) (D.4 D* D&8)) D∧
                            ( D≡ (D&0) (D&5) (D&4)) D∧
                              D.0 D< D&3 D∧
                                D&8 D* D&8 D∣ D&3 D∧ ( D≡ (D&2) (D&7) (D&4)) D∧ ( D≡ (D&1) (D&6) (D.4 D* (D&8)))))
        -- Porting note: copying directly `proof` in the proof of the following have fails
[GOAL]
α β : Type
n : ℕ
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
proof :
  Dioph
    ({v | const (Fin2 4 → ℕ) 1 v < v &0} ∩
      ({v | v &1 ≤ v &3} ∩
        (((fun v => v &2 = const (Fin2 4 → ℕ) 1 v) ∩ fun v => v &3 = const (Fin2 4 → ℕ) 0 v) ∪
          {v |
            ∃ x,
              (x :: v) ∈
                {v |
                  ∃ x,
                    (x :: v) ∈
                      {v |
                        ∃ x,
                          (x :: v) ∈
                            {v |
                              ∃ x,
                                (x :: v) ∈
                                  {v |
                                    ∃ x,
                                      (x :: v) ∈
                                        (fun v =>
                                            v &7 * v &7 - (v &5 * v &5 - const (Fin2 (succ 8) → ℕ) 1 v) * v &8 * v &8 =
                                              const (Fin2 (succ 8) → ℕ) 1 v) ∩
                                          ((fun v =>
                                              v &4 * v &4 -
                                                  (v &5 * v &5 - const (Fin2 (succ 8) → ℕ) 1 v) * v &3 * v &3 =
                                                const (Fin2 (succ 8) → ℕ) 1 v) ∩
                                            ((fun v =>
                                                v &2 * v &2 -
                                                    (v &0 * v &0 - const (Fin2 (succ 8) → ℕ) 1 v) * v &1 * v &1 =
                                                  const (Fin2 (succ 8) → ℕ) 1 v) ∩
                                              ({v | const (Fin2 (succ 8) → ℕ) 1 v < v &0} ∩
                                                ((fun v =>
                                                    v &0 ≡ const (Fin2 (succ 8) → ℕ) 1 v [MOD
                                                      const (Fin2 (succ 8) → ℕ) 4 v * v &8]) ∩
                                                  ((fun v => v &0 ≡ v &5 [MOD v &4]) ∩
                                                    ({v | const (Fin2 (succ 8) → ℕ) 0 v < v &3} ∩
                                                      ((fun v => v &8 * v &8 ∣ v &3) ∩
                                                        ((fun v => v &2 ≡ v &7 [MOD v &4]) ∩ fun v =>
                                                          v &1 ≡ v &6 [MOD
                                                            const (Fin2 (succ 8) → ℕ) 4 v * v &8]))))))))}}}}})))
⊢ Dioph fun v => ∃ h, xn h (v &1) = v &2 ∧ yn h (v &1) = v &3
[PROOFSTEP]
have :
  Dioph
    {v : Vector3 ℕ 4 |
      1 < v &0 ∧
        v &1 ≤ v &3 ∧
          (v &2 = 1 ∧ v &3 = 0 ∨
            ∃ u w s t b : ℕ,
              v &2 * v &2 - (v &0 * v &0 - 1) * v &3 * v &3 = 1 ∧
                u * u - (v &0 * v &0 - 1) * w * w = 1 ∧
                  s * s - (b * b - 1) * t * t = 1 ∧
                    1 < b ∧
                      b ≡ 1 [MOD 4 * v &3] ∧
                        b ≡ v &0 [MOD u] ∧ 0 < w ∧ v &3 * v &3 ∣ w ∧ s ≡ v &2 [MOD u] ∧ t ≡ v &1 [MOD 4 * v &3])} :=
  by exact proof
[GOAL]
α β : Type
n : ℕ
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
proof :
  Dioph
    ({v | const (Fin2 4 → ℕ) 1 v < v &0} ∩
      ({v | v &1 ≤ v &3} ∩
        (((fun v => v &2 = const (Fin2 4 → ℕ) 1 v) ∩ fun v => v &3 = const (Fin2 4 → ℕ) 0 v) ∪
          {v |
            ∃ x,
              (x :: v) ∈
                {v |
                  ∃ x,
                    (x :: v) ∈
                      {v |
                        ∃ x,
                          (x :: v) ∈
                            {v |
                              ∃ x,
                                (x :: v) ∈
                                  {v |
                                    ∃ x,
                                      (x :: v) ∈
                                        (fun v =>
                                            v &7 * v &7 - (v &5 * v &5 - const (Fin2 (succ 8) → ℕ) 1 v) * v &8 * v &8 =
                                              const (Fin2 (succ 8) → ℕ) 1 v) ∩
                                          ((fun v =>
                                              v &4 * v &4 -
                                                  (v &5 * v &5 - const (Fin2 (succ 8) → ℕ) 1 v) * v &3 * v &3 =
                                                const (Fin2 (succ 8) → ℕ) 1 v) ∩
                                            ((fun v =>
                                                v &2 * v &2 -
                                                    (v &0 * v &0 - const (Fin2 (succ 8) → ℕ) 1 v) * v &1 * v &1 =
                                                  const (Fin2 (succ 8) → ℕ) 1 v) ∩
                                              ({v | const (Fin2 (succ 8) → ℕ) 1 v < v &0} ∩
                                                ((fun v =>
                                                    v &0 ≡ const (Fin2 (succ 8) → ℕ) 1 v [MOD
                                                      const (Fin2 (succ 8) → ℕ) 4 v * v &8]) ∩
                                                  ((fun v => v &0 ≡ v &5 [MOD v &4]) ∩
                                                    ({v | const (Fin2 (succ 8) → ℕ) 0 v < v &3} ∩
                                                      ((fun v => v &8 * v &8 ∣ v &3) ∩
                                                        ((fun v => v &2 ≡ v &7 [MOD v &4]) ∩ fun v =>
                                                          v &1 ≡ v &6 [MOD
                                                            const (Fin2 (succ 8) → ℕ) 4 v * v &8]))))))))}}}}})))
⊢ Dioph
    {v |
      1 < v &0 ∧
        v &1 ≤ v &3 ∧
          (v &2 = 1 ∧ v &3 = 0 ∨
            ∃ u w s t b,
              v &2 * v &2 - (v &0 * v &0 - 1) * v &3 * v &3 = 1 ∧
                u * u - (v &0 * v &0 - 1) * w * w = 1 ∧
                  s * s - (b * b - 1) * t * t = 1 ∧
                    1 < b ∧
                      b ≡ 1 [MOD 4 * v &3] ∧
                        b ≡ v &0 [MOD u] ∧ 0 < w ∧ v &3 * v &3 ∣ w ∧ s ≡ v &2 [MOD u] ∧ t ≡ v &1 [MOD 4 * v &3])}
[PROOFSTEP]
exact proof
[GOAL]
α β : Type
n : ℕ
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
proof :
  Dioph
    ({v | const (Fin2 4 → ℕ) 1 v < v &0} ∩
      ({v | v &1 ≤ v &3} ∩
        (((fun v => v &2 = const (Fin2 4 → ℕ) 1 v) ∩ fun v => v &3 = const (Fin2 4 → ℕ) 0 v) ∪
          {v |
            ∃ x,
              (x :: v) ∈
                {v |
                  ∃ x,
                    (x :: v) ∈
                      {v |
                        ∃ x,
                          (x :: v) ∈
                            {v |
                              ∃ x,
                                (x :: v) ∈
                                  {v |
                                    ∃ x,
                                      (x :: v) ∈
                                        (fun v =>
                                            v &7 * v &7 - (v &5 * v &5 - const (Fin2 (succ 8) → ℕ) 1 v) * v &8 * v &8 =
                                              const (Fin2 (succ 8) → ℕ) 1 v) ∩
                                          ((fun v =>
                                              v &4 * v &4 -
                                                  (v &5 * v &5 - const (Fin2 (succ 8) → ℕ) 1 v) * v &3 * v &3 =
                                                const (Fin2 (succ 8) → ℕ) 1 v) ∩
                                            ((fun v =>
                                                v &2 * v &2 -
                                                    (v &0 * v &0 - const (Fin2 (succ 8) → ℕ) 1 v) * v &1 * v &1 =
                                                  const (Fin2 (succ 8) → ℕ) 1 v) ∩
                                              ({v | const (Fin2 (succ 8) → ℕ) 1 v < v &0} ∩
                                                ((fun v =>
                                                    v &0 ≡ const (Fin2 (succ 8) → ℕ) 1 v [MOD
                                                      const (Fin2 (succ 8) → ℕ) 4 v * v &8]) ∩
                                                  ((fun v => v &0 ≡ v &5 [MOD v &4]) ∩
                                                    ({v | const (Fin2 (succ 8) → ℕ) 0 v < v &3} ∩
                                                      ((fun v => v &8 * v &8 ∣ v &3) ∩
                                                        ((fun v => v &2 ≡ v &7 [MOD v &4]) ∩ fun v =>
                                                          v &1 ≡ v &6 [MOD
                                                            const (Fin2 (succ 8) → ℕ) 4 v * v &8]))))))))}}}}})))
this :
  Dioph
    {v |
      1 < v &0 ∧
        v &1 ≤ v &3 ∧
          (v &2 = 1 ∧ v &3 = 0 ∨
            ∃ u w s t b,
              v &2 * v &2 - (v &0 * v &0 - 1) * v &3 * v &3 = 1 ∧
                u * u - (v &0 * v &0 - 1) * w * w = 1 ∧
                  s * s - (b * b - 1) * t * t = 1 ∧
                    1 < b ∧
                      b ≡ 1 [MOD 4 * v &3] ∧
                        b ≡ v &0 [MOD u] ∧ 0 < w ∧ v &3 * v &3 ∣ w ∧ s ≡ v &2 [MOD u] ∧ t ≡ v &1 [MOD 4 * v &3])}
⊢ Dioph fun v => ∃ h, xn h (v &1) = v &2 ∧ yn h (v &1) = v &3
[PROOFSTEP]
exact Dioph.ext this fun v => matiyasevic.symm
[GOAL]
α β : Type
n : ℕ
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
⊢ DiophFn fun v => f v ^ g v
[PROOFSTEP]
have proof :=
  let D_pell := pell_dioph.reindex_dioph (Fin2 9) [&4, &8, &1, &0]
  (D&2 D= D.0 D∧ D&0 D= D.1) D∨
    (D.0 D< D&2 D∧
      ((D&1 D= D.0 D∧ D&0 D= D.0) D∨
        (D.0 D< D&1 D∧
          ((D∃) 3 <|
            (D∃) 4 <|
              (D∃) 5 <|
                (D∃) 6 $
                  (D∃) 7 <|
                    (D∃) 8 <|
                      D_pell D∧
                        ( D≡ (D&1) (D&0 D* (D&4 D- D&7) D+ D&6) (D&3)) D∧
                          D.2 D* D&4 D* D&7 D= D&3 D+ (D&7 D* D&7 D+ D.1) D∧
                            D&6 D< D&3 D∧
                              D&7 D≤ D&5 D∧
                                D&8 D≤ D&5 D∧
                                  D&4 D* D&4 D- ((D&5 D+ D.1) D* (D&5 D+ D.1) D- D.1) D* (D&5 D* D&2) D* (D&5 D* D&2) D=
                                    D.1))))
      -- Porting note: copying directly `proof` in the proof of the following have fails
[GOAL]
α β : Type
n : ℕ
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
proof :
  Dioph
    (((fun v => v &2 = const (Fin2 3 → ℕ) 0 v) ∩ fun v => v &0 = const (Fin2 3 → ℕ) 1 v) ∪
      {v | const (Fin2 3 → ℕ) 0 v < v &2} ∩
        (((fun v => v &1 = const (Fin2 3 → ℕ) 0 v) ∩ fun v => v &0 = const (Fin2 3 → ℕ) 0 v) ∪
          {v | const (Fin2 3 → ℕ) 0 v < v &1} ∩
            {v |
              ∃ x,
                (x :: v) ∈
                  {v |
                    ∃ x,
                      (x :: v) ∈
                        {v |
                          ∃ x,
                            (x :: v) ∈
                              {v |
                                ∃ x,
                                  (x :: v) ∈
                                    {v |
                                      ∃ x,
                                        (x :: v) ∈
                                          {v |
                                            ∃ x,
                                              (x :: v) ∈
                                                {v |
                                                    (v ∘ &4 :: &8 :: &1 :: &0 :: []) ∈ fun v =>
                                                      ∃ h, xn h (v &1) = v &2 ∧ yn h (v &1) = v &3} ∩
                                                  ((fun v => v &1 ≡ v &0 * (v &4 - v &7) + v &6 [MOD v &3]) ∩
                                                    ((fun v =>
                                                        const (Fin2 (succ 8) → ℕ) 2 v * v &4 * v &7 =
                                                          v &3 + (v &7 * v &7 + const (Fin2 (succ 8) → ℕ) 1 v)) ∩
                                                      ({v | v &6 < v &3} ∩
                                                        ({v | v &7 ≤ v &5} ∩
                                                          ({v | v &8 ≤ v &5} ∩ fun v =>
                                                            v &4 * v &4 -
                                                                ((v &5 + const (Fin2 (succ 8) → ℕ) 1 v) *
                                                                        (v &5 + const (Fin2 (succ 8) → ℕ) 1 v) -
                                                                      const (Fin2 (succ 8) → ℕ) 1 v) *
                                                                    (v &5 * v &2) *
                                                                  (v &5 * v &2) =
                                                              const (Fin2 (succ 8) → ℕ) 1 v)))))}}}}}}))
⊢ DiophFn fun v => f v ^ g v
[PROOFSTEP]
have :
  Dioph
    {v : Vector3 ℕ 3 |
      v &2 = 0 ∧ v &0 = 1 ∨
        0 < v &2 ∧
          (v &1 = 0 ∧ v &0 = 0 ∨
            0 < v &1 ∧
              ∃ w a t z x y : ℕ,
                (∃ a1 : 1 < a, xn a1 (v &2) = x ∧ yn a1 (v &2) = y) ∧
                  x ≡ y * (a - v &1) + v &0 [MOD t] ∧
                    2 * a * v &1 = t + (v &1 * v &1 + 1) ∧
                      v &0 < t ∧ v &1 ≤ w ∧ v &2 ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1)} :=
  by exact proof
[GOAL]
α β : Type
n : ℕ
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
proof :
  Dioph
    (((fun v => v &2 = const (Fin2 3 → ℕ) 0 v) ∩ fun v => v &0 = const (Fin2 3 → ℕ) 1 v) ∪
      {v | const (Fin2 3 → ℕ) 0 v < v &2} ∩
        (((fun v => v &1 = const (Fin2 3 → ℕ) 0 v) ∩ fun v => v &0 = const (Fin2 3 → ℕ) 0 v) ∪
          {v | const (Fin2 3 → ℕ) 0 v < v &1} ∩
            {v |
              ∃ x,
                (x :: v) ∈
                  {v |
                    ∃ x,
                      (x :: v) ∈
                        {v |
                          ∃ x,
                            (x :: v) ∈
                              {v |
                                ∃ x,
                                  (x :: v) ∈
                                    {v |
                                      ∃ x,
                                        (x :: v) ∈
                                          {v |
                                            ∃ x,
                                              (x :: v) ∈
                                                {v |
                                                    (v ∘ &4 :: &8 :: &1 :: &0 :: []) ∈ fun v =>
                                                      ∃ h, xn h (v &1) = v &2 ∧ yn h (v &1) = v &3} ∩
                                                  ((fun v => v &1 ≡ v &0 * (v &4 - v &7) + v &6 [MOD v &3]) ∩
                                                    ((fun v =>
                                                        const (Fin2 (succ 8) → ℕ) 2 v * v &4 * v &7 =
                                                          v &3 + (v &7 * v &7 + const (Fin2 (succ 8) → ℕ) 1 v)) ∩
                                                      ({v | v &6 < v &3} ∩
                                                        ({v | v &7 ≤ v &5} ∩
                                                          ({v | v &8 ≤ v &5} ∩ fun v =>
                                                            v &4 * v &4 -
                                                                ((v &5 + const (Fin2 (succ 8) → ℕ) 1 v) *
                                                                        (v &5 + const (Fin2 (succ 8) → ℕ) 1 v) -
                                                                      const (Fin2 (succ 8) → ℕ) 1 v) *
                                                                    (v &5 * v &2) *
                                                                  (v &5 * v &2) =
                                                              const (Fin2 (succ 8) → ℕ) 1 v)))))}}}}}}))
⊢ Dioph
    {v |
      v &2 = 0 ∧ v &0 = 1 ∨
        0 < v &2 ∧
          (v &1 = 0 ∧ v &0 = 0 ∨
            0 < v &1 ∧
              ∃ w a t z x y,
                (∃ a1, xn a1 (v &2) = x ∧ yn a1 (v &2) = y) ∧
                  x ≡ y * (a - v &1) + v &0 [MOD t] ∧
                    2 * a * v &1 = t + (v &1 * v &1 + 1) ∧
                      v &0 < t ∧ v &1 ≤ w ∧ v &2 ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1)}
[PROOFSTEP]
exact proof
[GOAL]
α β : Type
n : ℕ
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
proof :
  Dioph
    (((fun v => v &2 = const (Fin2 3 → ℕ) 0 v) ∩ fun v => v &0 = const (Fin2 3 → ℕ) 1 v) ∪
      {v | const (Fin2 3 → ℕ) 0 v < v &2} ∩
        (((fun v => v &1 = const (Fin2 3 → ℕ) 0 v) ∩ fun v => v &0 = const (Fin2 3 → ℕ) 0 v) ∪
          {v | const (Fin2 3 → ℕ) 0 v < v &1} ∩
            {v |
              ∃ x,
                (x :: v) ∈
                  {v |
                    ∃ x,
                      (x :: v) ∈
                        {v |
                          ∃ x,
                            (x :: v) ∈
                              {v |
                                ∃ x,
                                  (x :: v) ∈
                                    {v |
                                      ∃ x,
                                        (x :: v) ∈
                                          {v |
                                            ∃ x,
                                              (x :: v) ∈
                                                {v |
                                                    (v ∘ &4 :: &8 :: &1 :: &0 :: []) ∈ fun v =>
                                                      ∃ h, xn h (v &1) = v &2 ∧ yn h (v &1) = v &3} ∩
                                                  ((fun v => v &1 ≡ v &0 * (v &4 - v &7) + v &6 [MOD v &3]) ∩
                                                    ((fun v =>
                                                        const (Fin2 (succ 8) → ℕ) 2 v * v &4 * v &7 =
                                                          v &3 + (v &7 * v &7 + const (Fin2 (succ 8) → ℕ) 1 v)) ∩
                                                      ({v | v &6 < v &3} ∩
                                                        ({v | v &7 ≤ v &5} ∩
                                                          ({v | v &8 ≤ v &5} ∩ fun v =>
                                                            v &4 * v &4 -
                                                                ((v &5 + const (Fin2 (succ 8) → ℕ) 1 v) *
                                                                        (v &5 + const (Fin2 (succ 8) → ℕ) 1 v) -
                                                                      const (Fin2 (succ 8) → ℕ) 1 v) *
                                                                    (v &5 * v &2) *
                                                                  (v &5 * v &2) =
                                                              const (Fin2 (succ 8) → ℕ) 1 v)))))}}}}}}))
this :
  Dioph
    {v |
      v &2 = 0 ∧ v &0 = 1 ∨
        0 < v &2 ∧
          (v &1 = 0 ∧ v &0 = 0 ∨
            0 < v &1 ∧
              ∃ w a t z x y,
                (∃ a1, xn a1 (v &2) = x ∧ yn a1 (v &2) = y) ∧
                  x ≡ y * (a - v &1) + v &0 [MOD t] ∧
                    2 * a * v &1 = t + (v &1 * v &1 + 1) ∧
                      v &0 < t ∧ v &1 ≤ w ∧ v &2 ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1)}
⊢ DiophFn fun v => f v ^ g v
[PROOFSTEP]
exact
  diophFn_comp2 df dg <|
    (diophFn_vec _).2 <|
      Dioph.ext this fun v =>
        Iff.symm <|
          eq_pow_of_pell.trans <|
            or_congr Iff.rfl <|
              and_congr Iff.rfl <|
                or_congr Iff.rfl <|
                  and_congr Iff.rfl <|
                    ⟨fun ⟨w, a, t, z, a1, h⟩ => ⟨w, a, t, z, _, _, ⟨a1, rfl, rfl⟩, h⟩,
                      fun ⟨w, a, t, z, _, _, ⟨a1, rfl, rfl⟩, h⟩ => ⟨w, a, t, z, a1, h⟩⟩
