[GOAL]
R : Type u_1
inst✝ : Semiring R
r✝ : R
f✝ : R[X]
r c : R
f : R[X]
⊢ AddHom.toFun
      { toFun := fun f => comp f (X + ↑C r),
        map_add' := (_ : ∀ (f g : R[X]), comp (f + g) (X + ↑C r) = comp f (X + ↑C r) + comp g (X + ↑C r)) }
      (c • f) =
    ↑(RingHom.id R) c •
      AddHom.toFun
        { toFun := fun f => comp f (X + ↑C r),
          map_add' := (_ : ∀ (f g : R[X]), comp (f + g) (X + ↑C r) = comp f (X + ↑C r) + comp g (X + ↑C r)) }
        f
[PROOFSTEP]
simp only [smul_eq_C_mul, C_mul_comp, RingHom.id_apply]
[GOAL]
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ ↑(taylor r) X = X + ↑C r
[PROOFSTEP]
simp only [taylor_apply, X_comp]
[GOAL]
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
x : R
⊢ ↑(taylor r) (↑C x) = ↑C x
[PROOFSTEP]
simp only [taylor_apply, C_comp]
[GOAL]
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ taylor 0 = LinearMap.id
[PROOFSTEP]
ext
[GOAL]
case h.h.a
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
n✝¹ n✝ : ℕ
⊢ coeff (↑(LinearMap.comp (taylor 0) (monomial n✝¹)) 1) n✝ = coeff (↑(LinearMap.comp LinearMap.id (monomial n✝¹)) 1) n✝
[PROOFSTEP]
simp only [taylor_apply, add_zero, comp_X, _root_.map_zero, LinearMap.id_comp, Function.comp_apply, LinearMap.coe_comp]
[GOAL]
R : Type u_1
inst✝ : Semiring R
r : R
f✝ f : R[X]
⊢ ↑(taylor 0) f = f
[PROOFSTEP]
rw [taylor_zero', LinearMap.id_apply]
[GOAL]
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ ↑(taylor r) 1 = ↑C 1
[PROOFSTEP]
rw [← C_1, taylor_C]
[GOAL]
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
i : ℕ
k : R
⊢ ↑(taylor r) (↑(monomial i) k) = ↑C k * (X + ↑C r) ^ i
[PROOFSTEP]
simp [taylor_apply]
[GOAL]
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
n : ℕ
⊢ ↑(LinearMap.comp (lcoeff R n) (taylor r)) f = ↑(LinearMap.comp (leval r) (hasseDeriv n)) f
[PROOFSTEP]
congr 1
[GOAL]
case e_a
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
n : ℕ
⊢ LinearMap.comp (lcoeff R n) (taylor r) = LinearMap.comp (leval r) (hasseDeriv n)
[PROOFSTEP]
clear! f
[GOAL]
case e_a
R : Type u_1
inst✝ : Semiring R
r : R
n : ℕ
⊢ LinearMap.comp (lcoeff R n) (taylor r) = LinearMap.comp (leval r) (hasseDeriv n)
[PROOFSTEP]
ext i
[GOAL]
case e_a.h.h
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
⊢ ↑(LinearMap.comp (LinearMap.comp (lcoeff R n) (taylor r)) (monomial i)) 1 =
    ↑(LinearMap.comp (LinearMap.comp (leval r) (hasseDeriv n)) (monomial i)) 1
[PROOFSTEP]
simp only [leval_apply, mul_one, one_mul, eval_monomial, LinearMap.comp_apply, coeff_C_mul, hasseDeriv_monomial,
  taylor_apply, monomial_comp, C_1, (commute_X (C r)).add_pow i, LinearMap.map_sum]
[GOAL]
case e_a.h.h
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
⊢ (Finset.sum (Finset.range (i + 1)) fun x => ↑(lcoeff R n) (X ^ x * ↑C r ^ (i - x) * ↑(Nat.choose i x))) =
    ↑(Nat.choose i n) * r ^ (i - n)
[PROOFSTEP]
simp only [lcoeff_apply, ← C_eq_nat_cast, mul_assoc, ← C_pow, ← C_mul, coeff_mul_C, (Nat.cast_commute _ _).eq,
  coeff_X_pow, boole_mul, Finset.sum_ite_eq, Finset.mem_range]
[GOAL]
case e_a.h.h
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
⊢ (if n < i + 1 then r ^ (i - n) * ↑(Nat.choose i n) else 0) = r ^ (i - n) * ↑(Nat.choose i n)
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
h : n < i + 1
⊢ r ^ (i - n) * ↑(Nat.choose i n) = r ^ (i - n) * ↑(Nat.choose i n)
[PROOFSTEP]
rfl
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
h : ¬n < i + 1
⊢ 0 = r ^ (i - n) * ↑(Nat.choose i n)
[PROOFSTEP]
push_neg at h
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
h : i + 1 ≤ n
⊢ 0 = r ^ (i - n) * ↑(Nat.choose i n)
[PROOFSTEP]
rw [Nat.choose_eq_zero_of_lt h, Nat.cast_zero, mul_zero]
[GOAL]
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ coeff (↑(taylor r) f) 0 = eval r f
[PROOFSTEP]
rw [taylor_coeff, hasseDeriv_zero, LinearMap.id_apply]
[GOAL]
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ coeff (↑(taylor r) f) 1 = eval r (↑derivative f)
[PROOFSTEP]
rw [taylor_coeff, hasseDeriv_one]
[GOAL]
R : Type u_1
inst✝ : Semiring R
r✝ : R
f p : R[X]
r : R
⊢ natDegree (↑(taylor r) p) = natDegree p
[PROOFSTEP]
refine' map_natDegree_eq_natDegree _ _
[GOAL]
R : Type u_1
inst✝ : Semiring R
r✝ : R
f p : R[X]
r : R
⊢ ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree (↑(taylor r) (↑(monomial n) c)) = n
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u_1
inst✝ : Semiring R
r✝ : R
f p : R[X]
r : R
✝ : Nontrivial R
⊢ ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree (↑(taylor r) (↑(monomial n) c)) = n
[PROOFSTEP]
intro n c c0
[GOAL]
R : Type u_1
inst✝ : Semiring R
r✝ : R
f p : R[X]
r : R
✝ : Nontrivial R
n : ℕ
c : R
c0 : c ≠ 0
⊢ natDegree (↑(taylor r) (↑(monomial n) c)) = n
[PROOFSTEP]
simp [taylor_monomial, natDegree_C_mul_eq_of_mul_ne_zero, natDegree_pow_X_add_C, c0]
[GOAL]
R✝ : Type u_1
inst✝¹ : Semiring R✝
r✝ : R✝
f : R✝[X]
R : Type u_2
inst✝ : CommSemiring R
r : R
p q : R[X]
⊢ ↑(taylor r) (p * q) = ↑(taylor r) p * ↑(taylor r) q
[PROOFSTEP]
simp only [taylor_apply, mul_comp]
[GOAL]
R✝ : Type u_1
inst✝¹ : Semiring R✝
r✝ : R✝
f✝ : R✝[X]
R : Type u_2
inst✝ : CommSemiring R
f : R[X]
r s : R
⊢ ↑(taylor r) (↑(taylor s) f) = ↑(taylor (r + s)) f
[PROOFSTEP]
simp only [taylor_apply, comp_assoc, map_add, add_comp, X_comp, C_comp, C_add, add_assoc]
[GOAL]
R✝ : Type u_1
inst✝¹ : Semiring R✝
r✝ : R✝
f✝ : R✝[X]
R : Type u_2
inst✝ : CommSemiring R
r : R
f : R[X]
s : R
⊢ eval s (↑(taylor r) f) = eval (s + r) f
[PROOFSTEP]
simp only [taylor_apply, eval_comp, eval_C, eval_X, eval_add]
[GOAL]
R✝ : Type u_1
inst✝¹ : Semiring R✝
r✝ : R✝
f✝ : R✝[X]
R : Type u_2
inst✝ : CommRing R
r : R
f : R[X]
s : R
⊢ eval (s - r) (↑(taylor r) f) = eval s f
[PROOFSTEP]
rw [taylor_eval, sub_add_cancel]
[GOAL]
R✝ : Type u_1
inst✝¹ : Semiring R✝
r✝ : R✝
f : R✝[X]
R : Type u_2
inst✝ : CommRing R
r : R
⊢ Function.Injective ↑(taylor r)
[PROOFSTEP]
intro f g h
[GOAL]
R✝ : Type u_1
inst✝¹ : Semiring R✝
r✝ : R✝
f✝ : R✝[X]
R : Type u_2
inst✝ : CommRing R
r : R
f g : R[X]
h : ↑(taylor r) f = ↑(taylor r) g
⊢ f = g
[PROOFSTEP]
apply_fun taylor (-r) at h
[GOAL]
R✝ : Type u_1
inst✝¹ : Semiring R✝
r✝ : R✝
f✝ : R✝[X]
R : Type u_2
inst✝ : CommRing R
r : R
f g : R[X]
h : ↑(taylor (-r)) (↑(taylor r) f) = ↑(taylor (-r)) (↑(taylor r) g)
⊢ f = g
[PROOFSTEP]
simpa only [taylor_apply, comp_assoc, add_comp, X_comp, C_comp, C_neg, neg_add_cancel_right, comp_X] using h
[GOAL]
R✝ : Type u_1
inst✝¹ : Semiring R✝
r✝ : R✝
f✝ : R✝[X]
R : Type u_2
inst✝ : CommRing R
f : R[X]
r : R
h : ∀ (k : ℕ), eval r (↑(hasseDeriv k) f) = 0
⊢ f = 0
[PROOFSTEP]
apply taylor_injective r
[GOAL]
case a
R✝ : Type u_1
inst✝¹ : Semiring R✝
r✝ : R✝
f✝ : R✝[X]
R : Type u_2
inst✝ : CommRing R
f : R[X]
r : R
h : ∀ (k : ℕ), eval r (↑(hasseDeriv k) f) = 0
⊢ ↑(taylor r) f = ↑(taylor r) 0
[PROOFSTEP]
rw [LinearMap.map_zero]
[GOAL]
case a
R✝ : Type u_1
inst✝¹ : Semiring R✝
r✝ : R✝
f✝ : R✝[X]
R : Type u_2
inst✝ : CommRing R
f : R[X]
r : R
h : ∀ (k : ℕ), eval r (↑(hasseDeriv k) f) = 0
⊢ ↑(taylor r) f = 0
[PROOFSTEP]
ext k
[GOAL]
case a.a
R✝ : Type u_1
inst✝¹ : Semiring R✝
r✝ : R✝
f✝ : R✝[X]
R : Type u_2
inst✝ : CommRing R
f : R[X]
r : R
h : ∀ (k : ℕ), eval r (↑(hasseDeriv k) f) = 0
k : ℕ
⊢ coeff (↑(taylor r) f) k = coeff 0 k
[PROOFSTEP]
simp only [taylor_coeff, h, coeff_zero]
[GOAL]
R✝ : Type u_1
inst✝¹ : Semiring R✝
r✝ : R✝
f✝ : R✝[X]
R : Type u_2
inst✝ : CommRing R
f : R[X]
r : R
⊢ (sum (↑(taylor r) f) fun i a => ↑C a * (X - ↑C r) ^ i) = f
[PROOFSTEP]
rw [← comp_eq_sum_left, sub_eq_add_neg, ← C_neg, ← taylor_apply, taylor_taylor, neg_add_self, taylor_zero]


[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
M : R[X] → Prop
p : R[X]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ (p q : R[X]), M p → M q → M (p + q)
h_monomial : ∀ (n : ℕ) (a : R), M (↑C a * X ^ n) → M (↑C a * X ^ (n + 1))
⊢ M p
[PROOFSTEP]
have A : ∀ {n : ℕ} {a}, M (C a * X ^ n) := by
  intro n a
  induction' n with n ih
  · rw [pow_zero, mul_one]; exact h_C a
  · exact h_monomial _ _ ih
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
M : R[X] → Prop
p : R[X]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ (p q : R[X]), M p → M q → M (p + q)
h_monomial : ∀ (n : ℕ) (a : R), M (↑C a * X ^ n) → M (↑C a * X ^ (n + 1))
⊢ ∀ {n : ℕ} {a : R}, M (↑C a * X ^ n)
[PROOFSTEP]
intro n a
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
M : R[X] → Prop
p : R[X]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ (p q : R[X]), M p → M q → M (p + q)
h_monomial : ∀ (n : ℕ) (a : R), M (↑C a * X ^ n) → M (↑C a * X ^ (n + 1))
n : ℕ
a : R
⊢ M (↑C a * X ^ n)
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a✝ b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
M : R[X] → Prop
p : R[X]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ (p q : R[X]), M p → M q → M (p + q)
h_monomial : ∀ (n : ℕ) (a : R), M (↑C a * X ^ n) → M (↑C a * X ^ (n + 1))
a : R
⊢ M (↑C a * X ^ Nat.zero)
[PROOFSTEP]
rw [pow_zero, mul_one]
[GOAL]
case zero
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a✝ b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
M : R[X] → Prop
p : R[X]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ (p q : R[X]), M p → M q → M (p + q)
h_monomial : ∀ (n : ℕ) (a : R), M (↑C a * X ^ n) → M (↑C a * X ^ (n + 1))
a : R
⊢ M (↑C a)
[PROOFSTEP]
exact h_C a
[GOAL]
case succ
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
M : R[X] → Prop
p : R[X]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ (p q : R[X]), M p → M q → M (p + q)
h_monomial : ∀ (n : ℕ) (a : R), M (↑C a * X ^ n) → M (↑C a * X ^ (n + 1))
a : R
n : ℕ
ih : M (↑C a * X ^ n)
⊢ M (↑C a * X ^ Nat.succ n)
[PROOFSTEP]
exact h_monomial _ _ ih
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A✝ : Type z
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
M : R[X] → Prop
p : R[X]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ (p q : R[X]), M p → M q → M (p + q)
h_monomial : ∀ (n : ℕ) (a : R), M (↑C a * X ^ n) → M (↑C a * X ^ (n + 1))
A : ∀ {n : ℕ} {a : R}, M (↑C a * X ^ n)
⊢ M p
[PROOFSTEP]
have B : ∀ s : Finset ℕ, M (s.sum fun n : ℕ => C (p.coeff n) * X ^ n) :=
  by
  apply Finset.induction
  · convert h_C 0
    exact C_0.symm
  · intro n s ns ih
    rw [sum_insert ns]
    exact h_add _ _ A ih
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A✝ : Type z
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
M : R[X] → Prop
p : R[X]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ (p q : R[X]), M p → M q → M (p + q)
h_monomial : ∀ (n : ℕ) (a : R), M (↑C a * X ^ n) → M (↑C a * X ^ (n + 1))
A : ∀ {n : ℕ} {a : R}, M (↑C a * X ^ n)
⊢ ∀ (s : Finset ℕ), M (Finset.sum s fun n => ↑C (coeff p n) * X ^ n)
[PROOFSTEP]
apply Finset.induction
[GOAL]
case empty
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A✝ : Type z
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
M : R[X] → Prop
p : R[X]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ (p q : R[X]), M p → M q → M (p + q)
h_monomial : ∀ (n : ℕ) (a : R), M (↑C a * X ^ n) → M (↑C a * X ^ (n + 1))
A : ∀ {n : ℕ} {a : R}, M (↑C a * X ^ n)
⊢ M (Finset.sum ∅ fun n => ↑C (coeff p n) * X ^ n)
[PROOFSTEP]
convert h_C 0
[GOAL]
case h.e'_1
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A✝ : Type z
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
M : R[X] → Prop
p : R[X]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ (p q : R[X]), M p → M q → M (p + q)
h_monomial : ∀ (n : ℕ) (a : R), M (↑C a * X ^ n) → M (↑C a * X ^ (n + 1))
A : ∀ {n : ℕ} {a : R}, M (↑C a * X ^ n)
⊢ (Finset.sum ∅ fun n => ↑C (coeff p n) * X ^ n) = ↑C 0
[PROOFSTEP]
exact C_0.symm
[GOAL]
case insert
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A✝ : Type z
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
M : R[X] → Prop
p : R[X]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ (p q : R[X]), M p → M q → M (p + q)
h_monomial : ∀ (n : ℕ) (a : R), M (↑C a * X ^ n) → M (↑C a * X ^ (n + 1))
A : ∀ {n : ℕ} {a : R}, M (↑C a * X ^ n)
⊢ ∀ ⦃a : ℕ⦄ {s : Finset ℕ},
    ¬a ∈ s →
      M (Finset.sum s fun n => ↑C (coeff p n) * X ^ n) → M (Finset.sum (insert a s) fun n => ↑C (coeff p n) * X ^ n)
[PROOFSTEP]
intro n s ns ih
[GOAL]
case insert
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A✝ : Type z
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
M : R[X] → Prop
p : R[X]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ (p q : R[X]), M p → M q → M (p + q)
h_monomial : ∀ (n : ℕ) (a : R), M (↑C a * X ^ n) → M (↑C a * X ^ (n + 1))
A : ∀ {n : ℕ} {a : R}, M (↑C a * X ^ n)
n : ℕ
s : Finset ℕ
ns : ¬n ∈ s
ih : M (Finset.sum s fun n => ↑C (coeff p n) * X ^ n)
⊢ M (Finset.sum (insert n s) fun n => ↑C (coeff p n) * X ^ n)
[PROOFSTEP]
rw [sum_insert ns]
[GOAL]
case insert
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A✝ : Type z
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
M : R[X] → Prop
p : R[X]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ (p q : R[X]), M p → M q → M (p + q)
h_monomial : ∀ (n : ℕ) (a : R), M (↑C a * X ^ n) → M (↑C a * X ^ (n + 1))
A : ∀ {n : ℕ} {a : R}, M (↑C a * X ^ n)
n : ℕ
s : Finset ℕ
ns : ¬n ∈ s
ih : M (Finset.sum s fun n => ↑C (coeff p n) * X ^ n)
⊢ M (↑C (coeff p n) * X ^ n + Finset.sum s fun x => ↑C (coeff p x) * X ^ x)
[PROOFSTEP]
exact h_add _ _ A ih
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A✝ : Type z
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
M : R[X] → Prop
p : R[X]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ (p q : R[X]), M p → M q → M (p + q)
h_monomial : ∀ (n : ℕ) (a : R), M (↑C a * X ^ n) → M (↑C a * X ^ (n + 1))
A : ∀ {n : ℕ} {a : R}, M (↑C a * X ^ n)
B : ∀ (s : Finset ℕ), M (Finset.sum s fun n => ↑C (coeff p n) * X ^ n)
⊢ M p
[PROOFSTEP]
rw [← sum_C_mul_X_pow_eq p, Polynomial.sum]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A✝ : Type z
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
M : R[X] → Prop
p : R[X]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ (p q : R[X]), M p → M q → M (p + q)
h_monomial : ∀ (n : ℕ) (a : R), M (↑C a * X ^ n) → M (↑C a * X ^ (n + 1))
A : ∀ {n : ℕ} {a : R}, M (↑C a * X ^ n)
B : ∀ (s : Finset ℕ), M (Finset.sum s fun n => ↑C (coeff p n) * X ^ n)
⊢ M (Finset.sum (support p) fun n => ↑C (coeff p n) * X ^ n)
[PROOFSTEP]
exact B (support p)
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
M : R[X] → Prop
p : R[X]
h_add : ∀ (p q : R[X]), M p → M q → M (p + q)
h_monomial : ∀ (n : ℕ) (a : R), M (↑(monomial n) a)
n : ℕ
a : R
_h : M (↑C a * X ^ n)
⊢ M (↑C a * X ^ (n + 1))
[PROOFSTEP]
rw [C_mul_X_pow_eq_monomial]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
M : R[X] → Prop
p : R[X]
h_add : ∀ (p q : R[X]), M p → M q → M (p + q)
h_monomial : ∀ (n : ℕ) (a : R), M (↑(monomial n) a)
n : ℕ
a : R
_h : M (↑C a * X ^ n)
⊢ M (↑(monomial (n + 1)) a)
[PROOFSTEP]
exact h_monomial _ _
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : Semiring R
p q r f : R[X]
I : Ideal R[X]
cf : ∀ (i : ℕ), ↑C (coeff f i) ∈ I
⊢ Ideal.span {g | ∃ i, g = ↑C (coeff f i)} ≤ I
[PROOFSTEP]
simp (config := { singlePass := true }) only [@eq_comm _ _ (C _)]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : Semiring R
p q r f : R[X]
I : Ideal R[X]
cf : ∀ (i : ℕ), ↑C (coeff f i) ∈ I
⊢ Ideal.span {g | ∃ i, ↑C (coeff f i) = g} ≤ I
[PROOFSTEP]
exact (Ideal.span_le.trans range_subset_iff).mpr cf
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : Semiring R
p q r f : R[X]
I : Ideal R[X]
⊢ f ∈ Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
[PROOFSTEP]
let p := Ideal.span {g : R[X] | ∃ i : ℕ, g = C (coeff f i)}
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r f : R[X]
I : Ideal R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
⊢ f ∈ Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
[PROOFSTEP]
nth_rw 1 [(sum_C_mul_X_pow_eq f).symm]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r f : R[X]
I : Ideal R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
⊢ (sum f fun n a => ↑C a * X ^ n) ∈ Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
[PROOFSTEP]
refine' Submodule.sum_mem _ fun n _hn => _
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q r f : R[X]
I : Ideal R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
n : ℕ
_hn : n ∈ support f
⊢ (fun n a => ↑C a * X ^ n) n (coeff f n) ∈ Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
[PROOFSTEP]
dsimp
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q r f : R[X]
I : Ideal R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
n : ℕ
_hn : n ∈ support f
⊢ ↑C (coeff f n) * X ^ n ∈ Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
[PROOFSTEP]
have : C (coeff f n) ∈ p := by
  apply subset_span
  rw [mem_setOf_eq]
  use n
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q r f : R[X]
I : Ideal R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
n : ℕ
_hn : n ∈ support f
⊢ ↑C (coeff f n) ∈ p
[PROOFSTEP]
apply subset_span
[GOAL]
case a
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q r f : R[X]
I : Ideal R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
n : ℕ
_hn : n ∈ support f
⊢ ↑C (coeff f n) ∈ {g | ∃ i, g = ↑C (coeff f i)}
[PROOFSTEP]
rw [mem_setOf_eq]
[GOAL]
case a
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q r f : R[X]
I : Ideal R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
n : ℕ
_hn : n ∈ support f
⊢ ∃ i, ↑C (coeff f n) = ↑C (coeff f i)
[PROOFSTEP]
use n
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q r f : R[X]
I : Ideal R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
n : ℕ
_hn : n ∈ support f
this : ↑C (coeff f n) ∈ p
⊢ ↑C (coeff f n) * X ^ n ∈ Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
[PROOFSTEP]
have : monomial n (1 : R) • C (coeff f n) ∈ p := p.smul_mem _ this
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q r f : R[X]
I : Ideal R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
n : ℕ
_hn : n ∈ support f
this✝ : ↑C (coeff f n) ∈ p
this : ↑(monomial n) 1 • ↑C (coeff f n) ∈ p
⊢ ↑C (coeff f n) * X ^ n ∈ Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
[PROOFSTEP]
convert this using 1
[GOAL]
case h.e'_4
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q r f : R[X]
I : Ideal R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
n : ℕ
_hn : n ∈ support f
this✝ : ↑C (coeff f n) ∈ p
this : ↑(monomial n) 1 • ↑C (coeff f n) ∈ p
⊢ ↑C (coeff f n) * X ^ n = ↑(monomial n) 1 • ↑C (coeff f n)
[PROOFSTEP]
simp only [monomial_mul_C, one_mul, smul_eq_mul]
[GOAL]
case h.e'_4
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q r f : R[X]
I : Ideal R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = ↑C (coeff f i)}
n : ℕ
_hn : n ∈ support f
this✝ : ↑C (coeff f n) ∈ p
this : ↑(monomial n) 1 • ↑C (coeff f n) ∈ p
⊢ ↑C (coeff f n) * X ^ n = ↑(monomial n) (coeff f n)
[PROOFSTEP]
rw [← C_mul_X_pow_eq_monomial]


[GOAL]
z w : ℂ
H : z = w
⊢ z.re = w.re ∧ z.im = w.im
[PROOFSTEP]
simp [H]
[GOAL]
z w : ℝ
⊢ z = w → ↑z = ↑w
[PROOFSTEP]
apply congrArg
[GOAL]
r s : ℝ
⊢ (↑(r + s)).re = (↑r + ↑s).re ∧ (↑(r + s)).im = (↑r + ↑s).im
[PROOFSTEP]
simp [ofReal']
[GOAL]
r : ℝ
⊢ (↑(bit0 r)).re = (bit0 ↑r).re ∧ (↑(bit0 r)).im = (bit0 ↑r).im
[PROOFSTEP]
simp [bit0]
[GOAL]
r : ℝ
⊢ (↑(bit1 r)).re = (bit1 ↑r).re ∧ (↑(bit1 r)).im = (bit1 ↑r).im
[PROOFSTEP]
simp [bit1]
[GOAL]
r : ℝ
⊢ (↑(-r)).re = (-↑r).re ∧ (↑(-r)).im = (-↑r).im
[PROOFSTEP]
simp [ofReal']
[GOAL]
r s : ℝ
⊢ (↑(r * s)).re = (↑r * ↑s).re ∧ (↑(r * s)).im = (↑r * ↑s).im
[PROOFSTEP]
simp [ofReal']
[GOAL]
r : ℝ
z : ℂ
⊢ (↑r * z).re = r * z.re
[PROOFSTEP]
simp [ofReal']
[GOAL]
r : ℝ
z : ℂ
⊢ (↑r * z).im = r * z.im
[PROOFSTEP]
simp [ofReal']
[GOAL]
⊢ (I * I).re = (-1).re ∧ (I * I).im = (-1).im
[PROOFSTEP]
simp
[GOAL]
z : ℂ
⊢ (I * z).re = { re := -z.im, im := z.re }.re ∧ (I * z).im = { re := -z.im, im := z.re }.im
[PROOFSTEP]
simp
[GOAL]
a b : ℝ
⊢ { re := a, im := b }.re = (↑a + ↑b * I).re ∧ { re := a, im := b }.im = (↑a + ↑b * I).im
[PROOFSTEP]
simp [ofReal']
[GOAL]
z : ℂ
⊢ (↑z.re + ↑z.im * I).re = z.re ∧ (↑z.re + ↑z.im * I).im = z.im
[PROOFSTEP]
simp [ofReal']
[GOAL]
z : ℂ
⊢ (z * I).re = -z.im
[PROOFSTEP]
simp
[GOAL]
z : ℂ
⊢ (z * I).im = z.re
[PROOFSTEP]
simp
[GOAL]
z : ℂ
⊢ (I * z).re = -z.im
[PROOFSTEP]
simp
[GOAL]
z : ℂ
⊢ (I * z).im = z.re
[PROOFSTEP]
simp
[GOAL]
p : ℝ × ℝ
⊢ ↑equivRealProd.symm p = ↑p.fst + ↑p.snd * I
[PROOFSTEP]
ext
[GOAL]
case a
p : ℝ × ℝ
⊢ (↑equivRealProd.symm p).re = (↑p.fst + ↑p.snd * I).re
[PROOFSTEP]
simp [Complex.equivRealProd, ofReal']
[GOAL]
case a
p : ℝ × ℝ
⊢ (↑equivRealProd.symm p).im = (↑p.fst + ↑p.snd * I).im
[PROOFSTEP]
simp [Complex.equivRealProd, ofReal']
[GOAL]
R : Type u_1
inst✝ : SMul R ℝ
r : R
z : ℂ
⊢ (r • z).re = r • z.re
[PROOFSTEP]
simp [(· • ·), SMul.smul]
[GOAL]
R : Type u_1
inst✝ : SMul R ℝ
r : R
z : ℂ
⊢ (r • z).im = r • z.im
[PROOFSTEP]
simp [(· • ·), SMul.smul]
[GOAL]
⊢ ∀ (a b c : ℂ), a + b + c = a + (b + c)
[PROOFSTEP]
intros
[GOAL]
a✝ b✝ c✝ : ℂ
⊢ a✝ + b✝ + c✝ = a✝ + (b✝ + c✝)
[PROOFSTEP]
ext
[GOAL]
case a
a✝ b✝ c✝ : ℂ
⊢ (a✝ + b✝ + c✝).re = (a✝ + (b✝ + c✝)).re
[PROOFSTEP]
simp [add_assoc]
[GOAL]
case a
a✝ b✝ c✝ : ℂ
⊢ (a✝ + b✝ + c✝).im = (a✝ + (b✝ + c✝)).im
[PROOFSTEP]
simp [add_assoc]
[GOAL]
⊢ ∀ (a : ℂ), 0 + a = a
[PROOFSTEP]
intros
[GOAL]
a✝ : ℂ
⊢ 0 + a✝ = a✝
[PROOFSTEP]
ext
[GOAL]
case a
a✝ : ℂ
⊢ (0 + a✝).re = a✝.re
[PROOFSTEP]
simp
[GOAL]
case a
a✝ : ℂ
⊢ (0 + a✝).im = a✝.im
[PROOFSTEP]
simp
[GOAL]
⊢ ∀ (a : ℂ), a + 0 = a
[PROOFSTEP]
intros
[GOAL]
a✝ : ℂ
⊢ a✝ + 0 = a✝
[PROOFSTEP]
ext
[GOAL]
case a
a✝ : ℂ
⊢ (a✝ + 0).re = a✝.re
[PROOFSTEP]
simp
[GOAL]
case a
a✝ : ℂ
⊢ (a✝ + 0).im = a✝.im
[PROOFSTEP]
simp
[GOAL]
⊢ ∀ (x : ℂ), (fun n z => n • z) 0 x = 0
[PROOFSTEP]
intros
[GOAL]
x✝ : ℂ
⊢ (fun n z => n • z) 0 x✝ = 0
[PROOFSTEP]
ext
[GOAL]
case a
x✝ : ℂ
⊢ ((fun n z => n • z) 0 x✝).re = 0.re
[PROOFSTEP]
simp [smul_re, smul_im]
[GOAL]
case a
x✝ : ℂ
⊢ ((fun n z => n • z) 0 x✝).im = 0.im
[PROOFSTEP]
simp [smul_re, smul_im]
[GOAL]
⊢ ∀ (n : ℕ) (x : ℂ), (fun n z => n • z) (n + 1) x = x + (fun n z => n • z) n x
[PROOFSTEP]
intros
[GOAL]
n✝ : ℕ
x✝ : ℂ
⊢ (fun n z => n • z) (n✝ + 1) x✝ = x✝ + (fun n z => n • z) n✝ x✝
[PROOFSTEP]
ext
[GOAL]
case a
n✝ : ℕ
x✝ : ℂ
⊢ ((fun n z => n • z) (n✝ + 1) x✝).re = (x✝ + (fun n z => n • z) n✝ x✝).re
[PROOFSTEP]
simp [AddMonoid.nsmul_succ, add_mul, add_comm, smul_re, smul_im]
[GOAL]
case a
n✝ : ℕ
x✝ : ℂ
⊢ ((fun n z => n • z) (n✝ + 1) x✝).im = (x✝ + (fun n z => n • z) n✝ x✝).im
[PROOFSTEP]
simp [AddMonoid.nsmul_succ, add_mul, add_comm, smul_re, smul_im]
[GOAL]
⊢ ∀ (a : ℂ), (fun n z => n • z) 0 a = 0
[PROOFSTEP]
intros
[GOAL]
a✝ : ℂ
⊢ (fun n z => n • z) 0 a✝ = 0
[PROOFSTEP]
ext
[GOAL]
case a
a✝ : ℂ
⊢ ((fun n z => n • z) 0 a✝).re = 0.re
[PROOFSTEP]
simp [smul_re, smul_im]
[GOAL]
case a
a✝ : ℂ
⊢ ((fun n z => n • z) 0 a✝).im = 0.im
[PROOFSTEP]
simp [smul_re, smul_im]
[GOAL]
⊢ ∀ (n : ℕ) (a : ℂ), (fun n z => n • z) (Int.ofNat (Nat.succ n)) a = a + (fun n z => n • z) (Int.ofNat n) a
[PROOFSTEP]
intros
[GOAL]
n✝ : ℕ
a✝ : ℂ
⊢ (fun n z => n • z) (Int.ofNat (Nat.succ n✝)) a✝ = a✝ + (fun n z => n • z) (Int.ofNat n✝) a✝
[PROOFSTEP]
ext
[GOAL]
case a
n✝ : ℕ
a✝ : ℂ
⊢ ((fun n z => n • z) (Int.ofNat (Nat.succ n✝)) a✝).re = (a✝ + (fun n z => n • z) (Int.ofNat n✝) a✝).re
[PROOFSTEP]
simp [SubNegMonoid.zsmul_succ', add_mul, add_comm, smul_re, smul_im]
[GOAL]
case a
n✝ : ℕ
a✝ : ℂ
⊢ ((fun n z => n • z) (Int.ofNat (Nat.succ n✝)) a✝).im = (a✝ + (fun n z => n • z) (Int.ofNat n✝) a✝).im
[PROOFSTEP]
simp [SubNegMonoid.zsmul_succ', add_mul, add_comm, smul_re, smul_im]
[GOAL]
⊢ ∀ (n : ℕ) (a : ℂ), (fun n z => n • z) (Int.negSucc n) a = -(fun n z => n • z) (↑(Nat.succ n)) a
[PROOFSTEP]
intros
[GOAL]
n✝ : ℕ
a✝ : ℂ
⊢ (fun n z => n • z) (Int.negSucc n✝) a✝ = -(fun n z => n • z) (↑(Nat.succ n✝)) a✝
[PROOFSTEP]
ext
[GOAL]
case a
n✝ : ℕ
a✝ : ℂ
⊢ ((fun n z => n • z) (Int.negSucc n✝) a✝).re = (-(fun n z => n • z) (↑(Nat.succ n✝)) a✝).re
[PROOFSTEP]
simp [zsmul_neg', add_mul, smul_re, smul_im]
[GOAL]
case a
n✝ : ℕ
a✝ : ℂ
⊢ ((fun n z => n • z) (Int.negSucc n✝) a✝).im = (-(fun n z => n • z) (↑(Nat.succ n✝)) a✝).im
[PROOFSTEP]
simp [zsmul_neg', add_mul, smul_re, smul_im]
[GOAL]
⊢ ∀ (a : ℂ), -a + a = 0
[PROOFSTEP]
intros
[GOAL]
a✝ : ℂ
⊢ -a✝ + a✝ = 0
[PROOFSTEP]
ext
[GOAL]
case a
a✝ : ℂ
⊢ (-a✝ + a✝).re = 0.re
[PROOFSTEP]
simp
[GOAL]
case a
a✝ : ℂ
⊢ (-a✝ + a✝).im = 0.im
[PROOFSTEP]
simp
[GOAL]
⊢ ∀ (a b : ℂ), a + b = b + a
[PROOFSTEP]
intros
[GOAL]
a✝ b✝ : ℂ
⊢ a✝ + b✝ = b✝ + a✝
[PROOFSTEP]
ext
[GOAL]
case a
a✝ b✝ : ℂ
⊢ (a✝ + b✝).re = (b✝ + a✝).re
[PROOFSTEP]
simp [add_comm]
[GOAL]
case a
a✝ b✝ : ℂ
⊢ (a✝ + b✝).im = (b✝ + a✝).im
[PROOFSTEP]
simp [add_comm]
[GOAL]
src✝ : AddCommGroup ℂ := addCommGroup
⊢ NatCast.natCast 0 = 0
[PROOFSTEP]
ext
[GOAL]
case a
src✝ : AddCommGroup ℂ := addCommGroup
⊢ (NatCast.natCast 0).re = 0.re
[PROOFSTEP]
simp [Nat.cast, AddMonoidWithOne.natCast_zero]
[GOAL]
case a
src✝ : AddCommGroup ℂ := addCommGroup
⊢ (NatCast.natCast 0).im = 0.im
[PROOFSTEP]
simp [Nat.cast, AddMonoidWithOne.natCast_zero]
[GOAL]
src✝ : AddCommGroup ℂ := addCommGroup
x✝ : ℕ
⊢ NatCast.natCast (x✝ + 1) = NatCast.natCast x✝ + 1
[PROOFSTEP]
ext
[GOAL]
case a
src✝ : AddCommGroup ℂ := addCommGroup
x✝ : ℕ
⊢ (NatCast.natCast (x✝ + 1)).re = (NatCast.natCast x✝ + 1).re
[PROOFSTEP]
simp [Nat.cast, AddMonoidWithOne.natCast_succ]
[GOAL]
case a
src✝ : AddCommGroup ℂ := addCommGroup
x✝ : ℕ
⊢ (NatCast.natCast (x✝ + 1)).im = (NatCast.natCast x✝ + 1).im
[PROOFSTEP]
simp [Nat.cast, AddMonoidWithOne.natCast_succ]
[GOAL]
src✝ : AddCommGroup ℂ := addCommGroup
x✝ : ℕ
⊢ IntCast.intCast ↑x✝ = ↑x✝
[PROOFSTEP]
ext
[GOAL]
case a
src✝ : AddCommGroup ℂ := addCommGroup
x✝ : ℕ
⊢ (IntCast.intCast ↑x✝).re = (↑x✝).re
[PROOFSTEP]
rfl
[GOAL]
case a
src✝ : AddCommGroup ℂ := addCommGroup
x✝ : ℕ
⊢ (IntCast.intCast ↑x✝).im = (↑x✝).im
[PROOFSTEP]
rfl
[GOAL]
src✝ : AddCommGroup ℂ := addCommGroup
n : ℕ
⊢ IntCast.intCast (Int.negSucc n) = -↑(n + 1)
[PROOFSTEP]
ext
[GOAL]
case a
src✝ : AddCommGroup ℂ := addCommGroup
n : ℕ
⊢ (IntCast.intCast (Int.negSucc n)).re = (-↑(n + 1)).re
[PROOFSTEP]
simp [AddGroupWithOne.intCast_negSucc]
[GOAL]
case a
src✝ : AddCommGroup ℂ := addCommGroup
n : ℕ
⊢ -1 + -↑n = -(↑(n + 1)).re
[PROOFSTEP]
show -(1 : ℝ) + (-n) = -(↑(n + 1))
[GOAL]
case a
src✝ : AddCommGroup ℂ := addCommGroup
n : ℕ
⊢ -1 + -↑n = -↑(n + 1)
[PROOFSTEP]
simp [Nat.cast_add, add_comm]
[GOAL]
case a
src✝ : AddCommGroup ℂ := addCommGroup
n : ℕ
⊢ (IntCast.intCast (Int.negSucc n)).im = (-↑(n + 1)).im
[PROOFSTEP]
simp [AddGroupWithOne.intCast_negSucc]
[GOAL]
case a
src✝ : AddCommGroup ℂ := addCommGroup
n : ℕ
⊢ (↑(n + 1)).im = 0
[PROOFSTEP]
show im ⟨n, 0⟩ = 0
[GOAL]
case a
src✝ : AddCommGroup ℂ := addCommGroup
n : ℕ
⊢ { re := ↑n, im := 0 }.im = 0
[PROOFSTEP]
rfl
[GOAL]
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
⊢ ∀ (a b : ℂ), a + b = b + a
[PROOFSTEP]
intros
[GOAL]
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ : ℂ
⊢ a✝ + b✝ = b✝ + a✝
[PROOFSTEP]
ext
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ : ℂ
⊢ (a✝ + b✝).re = (b✝ + a✝).re
[PROOFSTEP]
simp [add_comm]
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ : ℂ
⊢ (a✝ + b✝).im = (b✝ + a✝).im
[PROOFSTEP]
simp [add_comm]
[GOAL]
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
⊢ ∀ (a b c : ℂ), a * (b + c) = a * b + a * c
[PROOFSTEP]
intros
[GOAL]
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ c✝ : ℂ
⊢ a✝ * (b✝ + c✝) = a✝ * b✝ + a✝ * c✝
[PROOFSTEP]
ext
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ c✝ : ℂ
⊢ (a✝ * (b✝ + c✝)).re = (a✝ * b✝ + a✝ * c✝).re
[PROOFSTEP]
simp [mul_re, mul_im]
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ c✝ : ℂ
⊢ (a✝ * (b✝ + c✝)).im = (a✝ * b✝ + a✝ * c✝).im
[PROOFSTEP]
simp [mul_re, mul_im]
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ c✝ : ℂ
⊢ a✝.re * (b✝.re + c✝.re) - a✝.im * (b✝.im + c✝.im) = a✝.re * b✝.re - a✝.im * b✝.im + (a✝.re * c✝.re - a✝.im * c✝.im)
[PROOFSTEP]
ring
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ c✝ : ℂ
⊢ a✝.re * (b✝.im + c✝.im) + a✝.im * (b✝.re + c✝.re) = a✝.re * b✝.im + a✝.im * b✝.re + (a✝.re * c✝.im + a✝.im * c✝.re)
[PROOFSTEP]
ring
[GOAL]
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
⊢ ∀ (a b c : ℂ), (a + b) * c = a * c + b * c
[PROOFSTEP]
intros
[GOAL]
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ c✝ : ℂ
⊢ (a✝ + b✝) * c✝ = a✝ * c✝ + b✝ * c✝
[PROOFSTEP]
ext
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ c✝ : ℂ
⊢ ((a✝ + b✝) * c✝).re = (a✝ * c✝ + b✝ * c✝).re
[PROOFSTEP]
simp [mul_re, mul_im]
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ c✝ : ℂ
⊢ ((a✝ + b✝) * c✝).im = (a✝ * c✝ + b✝ * c✝).im
[PROOFSTEP]
simp [mul_re, mul_im]
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ c✝ : ℂ
⊢ (a✝.re + b✝.re) * c✝.re - (a✝.im + b✝.im) * c✝.im = a✝.re * c✝.re - a✝.im * c✝.im + (b✝.re * c✝.re - b✝.im * c✝.im)
[PROOFSTEP]
ring
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ c✝ : ℂ
⊢ (a✝.re + b✝.re) * c✝.im + (a✝.im + b✝.im) * c✝.re = a✝.re * c✝.im + a✝.im * c✝.re + (b✝.re * c✝.im + b✝.im * c✝.re)
[PROOFSTEP]
ring
[GOAL]
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
⊢ ∀ (a : ℂ), 0 * a = 0
[PROOFSTEP]
intros
[GOAL]
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ : ℂ
⊢ 0 * a✝ = 0
[PROOFSTEP]
ext
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ : ℂ
⊢ (0 * a✝).re = 0.re
[PROOFSTEP]
simp [zero_mul]
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ : ℂ
⊢ (0 * a✝).im = 0.im
[PROOFSTEP]
simp [zero_mul]
[GOAL]
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
⊢ ∀ (a : ℂ), a * 0 = 0
[PROOFSTEP]
intros
[GOAL]
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ : ℂ
⊢ a✝ * 0 = 0
[PROOFSTEP]
ext
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ : ℂ
⊢ (a✝ * 0).re = 0.re
[PROOFSTEP]
simp [mul_zero]
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ : ℂ
⊢ (a✝ * 0).im = 0.im
[PROOFSTEP]
simp [mul_zero]
[GOAL]
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
⊢ ∀ (a b c : ℂ), a * b * c = a * (b * c)
[PROOFSTEP]
intros
[GOAL]
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ c✝ : ℂ
⊢ a✝ * b✝ * c✝ = a✝ * (b✝ * c✝)
[PROOFSTEP]
ext
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ c✝ : ℂ
⊢ (a✝ * b✝ * c✝).re = (a✝ * (b✝ * c✝)).re
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ c✝ : ℂ
⊢ (a✝ * b✝ * c✝).im = (a✝ * (b✝ * c✝)).im
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ c✝ : ℂ
⊢ (a✝.re * b✝.re - a✝.im * b✝.im) * c✝.re - (a✝.re * b✝.im + a✝.im * b✝.re) * c✝.im =
    a✝.re * (b✝.re * c✝.re - b✝.im * c✝.im) - a✝.im * (b✝.re * c✝.im + b✝.im * c✝.re)
[PROOFSTEP]
ring
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ c✝ : ℂ
⊢ (a✝.re * b✝.re - a✝.im * b✝.im) * c✝.im + (a✝.re * b✝.im + a✝.im * b✝.re) * c✝.re =
    a✝.re * (b✝.re * c✝.im + b✝.im * c✝.re) + a✝.im * (b✝.re * c✝.re - b✝.im * c✝.im)
[PROOFSTEP]
ring
[GOAL]
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
⊢ ∀ (a : ℂ), 1 * a = a
[PROOFSTEP]
intros
[GOAL]
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ : ℂ
⊢ 1 * a✝ = a✝
[PROOFSTEP]
ext
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ : ℂ
⊢ (1 * a✝).re = a✝.re
[PROOFSTEP]
simp [one_mul]
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ : ℂ
⊢ (1 * a✝).im = a✝.im
[PROOFSTEP]
simp [one_mul]
[GOAL]
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
⊢ ∀ (a : ℂ), a * 1 = a
[PROOFSTEP]
intros
[GOAL]
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ : ℂ
⊢ a✝ * 1 = a✝
[PROOFSTEP]
ext
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ : ℂ
⊢ (a✝ * 1).re = a✝.re
[PROOFSTEP]
simp [mul_one]
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ : ℂ
⊢ (a✝ * 1).im = a✝.im
[PROOFSTEP]
simp [mul_one]
[GOAL]
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
⊢ ∀ (a b : ℂ), a * b = b * a
[PROOFSTEP]
intros
[GOAL]
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ : ℂ
⊢ a✝ * b✝ = b✝ * a✝
[PROOFSTEP]
ext
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ : ℂ
⊢ (a✝ * b✝).re = (b✝ * a✝).re
[PROOFSTEP]
simp [mul_comm]
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ : ℂ
⊢ (a✝ * b✝).im = (b✝ * a✝).im
[PROOFSTEP]
simp [mul_comm]
[GOAL]
case a
src✝ : AddGroupWithOne ℂ := Complex.addGroupWithOne
a✝ b✝ : ℂ
⊢ a✝.re * b✝.im + b✝.re * a✝.im = b✝.re * a✝.im + a✝.re * b✝.im
[PROOFSTEP]
ring
[GOAL]
⊢ Ring ℂ
[PROOFSTEP]
infer_instance
[GOAL]
n : ℕ
⊢ I ^ bit0 n = (-1) ^ n
[PROOFSTEP]
rw [pow_bit0', Complex.I_mul_I]
[GOAL]
n : ℕ
⊢ I ^ bit1 n = (-1) ^ n * I
[PROOFSTEP]
rw [pow_bit1', Complex.I_mul_I]
[GOAL]
x : ℂ
⊢ star (star x) = x
[PROOFSTEP]
simp only [eta, neg_neg]
[GOAL]
a b : ℂ
⊢ star (a * b) = star b * star a
[PROOFSTEP]
ext
[GOAL]
case a
a b : ℂ
⊢ (star (a * b)).re = (star b * star a).re
[PROOFSTEP]
simp [add_comm]
[GOAL]
case a
a b : ℂ
⊢ (star (a * b)).im = (star b * star a).im
[PROOFSTEP]
simp [add_comm]
[GOAL]
case a
a b : ℂ
⊢ a.re * b.re - a.im * b.im = b.re * a.re - b.im * a.im
[PROOFSTEP]
ring
[GOAL]
case a
a b : ℂ
⊢ -(a.re * b.im) + -(a.im * b.re) = -(b.re * a.im) + -(b.im * a.re)
[PROOFSTEP]
ring
[GOAL]
a b : ℂ
⊢ star (a + b) = star a + star b
[PROOFSTEP]
ext
[GOAL]
case a
a b : ℂ
⊢ (star (a + b)).re = (star a + star b).re
[PROOFSTEP]
simp [add_comm]
[GOAL]
case a
a b : ℂ
⊢ (star (a + b)).im = (star a + star b).im
[PROOFSTEP]
simp [add_comm]
[GOAL]
r : ℝ
⊢ (↑(starRingEnd ℂ) ↑r).re = (↑r).re ∧ (↑(starRingEnd ℂ) ↑r).im = (↑r).im
[PROOFSTEP]
simp [star]
[GOAL]
⊢ (↑(starRingEnd ℂ) I).re = (-I).re ∧ (↑(starRingEnd ℂ) I).im = (-I).im
[PROOFSTEP]
simp
[GOAL]
z : ℂ
⊢ (↑(starRingEnd ℂ) (bit0 z)).re = (bit0 (↑(starRingEnd ℂ) z)).re ∧
    (↑(starRingEnd ℂ) (bit0 z)).im = (bit0 (↑(starRingEnd ℂ) z)).im
[PROOFSTEP]
simp [bit0]
[GOAL]
z : ℂ
⊢ (↑(starRingEnd ℂ) (bit1 z)).re = (bit1 (↑(starRingEnd ℂ) z)).re ∧
    (↑(starRingEnd ℂ) (bit1 z)).im = (bit1 (↑(starRingEnd ℂ) z)).im
[PROOFSTEP]
simp [bit0]
[GOAL]
⊢ (↑(starRingEnd ℂ) (-I)).re = I.re ∧ (↑(starRingEnd ℂ) (-I)).im = I.im
[PROOFSTEP]
simp
[GOAL]
z : ℂ
x✝ : ∃ r, z = ↑r
h : ℝ
e : z = ↑h
⊢ ↑(starRingEnd ℂ) z = z
[PROOFSTEP]
rw [e, conj_ofReal]
[GOAL]
z : ℂ
⊢ (∃ r, z = ↑r) → ↑z.re = z
[PROOFSTEP]
rintro ⟨r, rfl⟩
[GOAL]
case intro
r : ℝ
⊢ ↑(↑r).re = ↑r
[PROOFSTEP]
simp [ofReal']
[GOAL]
⊢ (fun z => z.re * z.re + z.im * z.im) 0 = 0
[PROOFSTEP]
simp
[GOAL]
⊢ ZeroHom.toFun { toFun := fun z => z.re * z.re + z.im * z.im, map_zero' := (_ : 0 * 0 + 0 * 0 = 0) } 1 = 1
[PROOFSTEP]
simp
[GOAL]
z w : ℂ
⊢ ZeroHom.toFun { toFun := fun z => z.re * z.re + z.im * z.im, map_zero' := (_ : 0 * 0 + 0 * 0 = 0) } (z * w) =
    ZeroHom.toFun { toFun := fun z => z.re * z.re + z.im * z.im, map_zero' := (_ : 0 * 0 + 0 * 0 = 0) } z *
      ZeroHom.toFun { toFun := fun z => z.re * z.re + z.im * z.im, map_zero' := (_ : 0 * 0 + 0 * 0 = 0) } w
[PROOFSTEP]
dsimp
[GOAL]
z w : ℂ
⊢ (z.re * w.re - z.im * w.im) * (z.re * w.re - z.im * w.im) +
      (z.re * w.im + z.im * w.re) * (z.re * w.im + z.im * w.re) =
    (z.re * z.re + z.im * z.im) * (w.re * w.re + w.im * w.im)
[PROOFSTEP]
ring
[GOAL]
r : ℝ
⊢ ↑normSq ↑r = r * r
[PROOFSTEP]
simp [normSq, ofReal']
[GOAL]
x y : ℝ
⊢ ↑normSq (↑x + ↑y * I) = x ^ 2 + y ^ 2
[PROOFSTEP]
rw [← mk_eq_add_mul_I, normSq_mk, sq, sq]
[GOAL]
z : ℂ
⊢ ↑(↑normSq z) = ↑(starRingEnd ℂ) z * z
[PROOFSTEP]
ext
[GOAL]
case a
z : ℂ
⊢ (↑(↑normSq z)).re = (↑(starRingEnd ℂ) z * z).re
[PROOFSTEP]
simp [normSq, mul_comm, ofReal']
[GOAL]
case a
z : ℂ
⊢ (↑(↑normSq z)).im = (↑(starRingEnd ℂ) z * z).im
[PROOFSTEP]
simp [normSq, mul_comm, ofReal']
[GOAL]
⊢ ↑normSq I = 1
[PROOFSTEP]
simp [normSq]
[GOAL]
x : ℝ
hx : x ∈ Ici 0
⊢ ↑normSq ↑(Real.sqrt x) = x
[PROOFSTEP]
rw [normSq_ofReal, Real.mul_self_sqrt hx]
[GOAL]
z : ℂ
⊢ ↑normSq (-z) = ↑normSq z
[PROOFSTEP]
simp [normSq]
[GOAL]
z : ℂ
⊢ ↑normSq (↑(starRingEnd ℂ) z) = ↑normSq z
[PROOFSTEP]
simp [normSq]
[GOAL]
z w : ℂ
⊢ ↑normSq (z + w) = ↑normSq z + ↑normSq w + 2 * (z * ↑(starRingEnd ℂ) w).re
[PROOFSTEP]
dsimp [normSq]
[GOAL]
z w : ℂ
⊢ (z.re + w.re) * (z.re + w.re) + (z.im + w.im) * (z.im + w.im) =
    z.re * z.re + z.im * z.im + (w.re * w.re + w.im * w.im) + 2 * (z.re * w.re - z.im * -w.im)
[PROOFSTEP]
ring
[GOAL]
z : ℂ
⊢ (z * ↑(starRingEnd ℂ) z).re = (↑(↑normSq z)).re ∧ (z * ↑(starRingEnd ℂ) z).im = (↑(↑normSq z)).im
[PROOFSTEP]
simp [normSq, mul_comm, sub_eq_neg_add, add_comm, ofReal']
[GOAL]
z : ℂ
⊢ (z + ↑(starRingEnd ℂ) z).re = (↑(2 * z.re)).re ∧ (z + ↑(starRingEnd ℂ) z).im = (↑(2 * z.re)).im
[PROOFSTEP]
simp [two_mul, ofReal']
[GOAL]
⊢ I ^ 2 = -1
[PROOFSTEP]
rw [sq, I_mul_I]
[GOAL]
r s : ℝ
⊢ (↑(r - s)).re = (↑r - ↑s).re ∧ (↑(r - s)).im = (↑r - ↑s).im
[PROOFSTEP]
simp [ofReal']
[GOAL]
r : ℝ
n : ℕ
⊢ ↑(r ^ n) = ↑r ^ n
[PROOFSTEP]
induction n
[GOAL]
case zero
r : ℝ
⊢ ↑(r ^ Nat.zero) = ↑r ^ Nat.zero
[PROOFSTEP]
simp [*, ofReal_mul, pow_succ]
[GOAL]
case succ
r : ℝ
n✝ : ℕ
n_ih✝ : ↑(r ^ n✝) = ↑r ^ n✝
⊢ ↑(r ^ Nat.succ n✝) = ↑r ^ Nat.succ n✝
[PROOFSTEP]
simp [*, ofReal_mul, pow_succ]
[GOAL]
z : ℂ
⊢ (z - ↑(starRingEnd ℂ) z).re = (↑(2 * z.im) * I).re ∧ (z - ↑(starRingEnd ℂ) z).im = (↑(2 * z.im) * I).im
[PROOFSTEP]
simp [two_mul, sub_eq_add_neg, ofReal']
[GOAL]
z w : ℂ
⊢ ↑normSq (z - w) = ↑normSq z + ↑normSq w - 2 * (z * ↑(starRingEnd ℂ) w).re
[PROOFSTEP]
rw [sub_eq_add_neg, normSq_add]
[GOAL]
z w : ℂ
⊢ ↑normSq z + ↑normSq (-w) + 2 * (z * ↑(starRingEnd ℂ) (-w)).re =
    ↑normSq z + ↑normSq w - 2 * (z * ↑(starRingEnd ℂ) w).re
[PROOFSTEP]
simp only [RingHom.map_neg, mul_neg, neg_re, normSq_neg]
[GOAL]
z w : ℂ
⊢ ↑normSq z + ↑normSq w + -(2 * (z * ↑(starRingEnd ℂ) w).re) = ↑normSq z + ↑normSq w - 2 * (z * ↑(starRingEnd ℂ) w).re
[PROOFSTEP]
ring
[GOAL]
z : ℂ
⊢ z⁻¹.re = z.re / ↑normSq z
[PROOFSTEP]
simp [inv_def, division_def, ofReal']
[GOAL]
z : ℂ
⊢ z⁻¹.im = -z.im / ↑normSq z
[PROOFSTEP]
simp [inv_def, division_def, ofReal']
[GOAL]
r : ℝ
⊢ (↑r⁻¹).re = (↑r)⁻¹.re ∧ (↑r⁻¹).im = (↑r)⁻¹.im
[PROOFSTEP]
simp [ofReal']
[GOAL]
⊢ 0⁻¹ = 0
[PROOFSTEP]
rw [← ofReal_zero, ← ofReal_inv, inv_zero]
[GOAL]
z : ℂ
h : z ≠ 0
⊢ z * z⁻¹ = 1
[PROOFSTEP]
rw [inv_def, ← mul_assoc, mul_conj, ← ofReal_mul, mul_inv_cancel (mt normSq_eq_zero.1 h), ofReal_one]
[GOAL]
n : ℕ
⊢ (↑n).re = ↑n
[PROOFSTEP]
rw [← ofReal_nat_cast, ofReal_re]
[GOAL]
n : ℕ
⊢ (↑n).im = 0
[PROOFSTEP]
rw [← ofReal_nat_cast, ofReal_im]
[GOAL]
n : ℤ
⊢ (↑n).re = ↑n
[PROOFSTEP]
rw [← ofReal_int_cast, ofReal_re]
[GOAL]
n : ℤ
⊢ (↑n).im = 0
[PROOFSTEP]
rw [← ofReal_int_cast, ofReal_im]
[GOAL]
q : ℚ
⊢ (↑q).im = 0
[PROOFSTEP]
show (Rat.castRec q : ℂ).im = 0
[GOAL]
q : ℚ
⊢ (Rat.castRec q).im = 0
[PROOFSTEP]
cases q
[GOAL]
case mk'
num✝ : ℤ
den✝ : ℕ
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs num✝) den✝
⊢ (Rat.castRec (Rat.mk' num✝ den✝)).im = 0
[PROOFSTEP]
simp [Rat.castRec]
[GOAL]
q : ℚ
⊢ (↑q).re = ↑q
[PROOFSTEP]
show (Rat.castRec q : ℂ).re = _
[GOAL]
q : ℚ
⊢ (Rat.castRec q).re = ↑q
[PROOFSTEP]
cases q
[GOAL]
case mk'
num✝ : ℤ
den✝ : ℕ
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs num✝) den✝
⊢ (Rat.castRec (Rat.mk' num✝ den✝)).re = ↑(Rat.mk' num✝ den✝)
[PROOFSTEP]
simp [Rat.castRec, normSq, Rat.mk_eq_divInt, Rat.mkRat_eq_div, div_eq_mul_inv, *]
[GOAL]
n : ℚ
z : ℂ
⊢ ((fun n z => n • z) n z).re = (↑n * z).re ∧ ((fun n z => n • z) n z).im = (↑n * z).im
[PROOFSTEP]
simp [Rat.smul_def, smul_re, smul_im]
[GOAL]
n : ℤ
⊢ I ^ bit0 n = (-1) ^ n
[PROOFSTEP]
rw [zpow_bit0', I_mul_I]
[GOAL]
n : ℤ
⊢ I ^ bit1 n = (-1) ^ n * I
[PROOFSTEP]
rw [zpow_bit1', I_mul_I]
[GOAL]
z w : ℂ
⊢ (z / w).re = z.re * w.re / ↑normSq w + z.im * w.im / ↑normSq w
[PROOFSTEP]
simp [div_eq_mul_inv, mul_assoc, sub_eq_add_neg]
[GOAL]
z w : ℂ
⊢ (z / w).im = z.im * w.re / ↑normSq w - z.re * w.im / ↑normSq w
[PROOFSTEP]
simp [div_eq_mul_inv, mul_assoc, sub_eq_add_neg, add_comm]
[GOAL]
z : ℂ
⊢ -(z * I) * I = z
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
⊢ I⁻¹ = -I
[PROOFSTEP]
rw [inv_eq_one_div, div_I, one_mul]
[GOAL]
n : ℕ
h : ↑n = 0
⊢ n = 0
[PROOFSTEP]
rwa [← ofReal_nat_cast, ofReal_eq_zero, Nat.cast_eq_zero] at h
[GOAL]
z : ℂ
⊢ ↑z.re = (z + ↑(starRingEnd ℂ) z) / 2
[PROOFSTEP]
have : (↑(↑2 : ℝ) : ℂ) = (2 : ℂ) := by rfl
[GOAL]
z : ℂ
⊢ ↑2 = 2
[PROOFSTEP]
rfl
[GOAL]
z : ℂ
this : ↑2 = 2
⊢ ↑z.re = (z + ↑(starRingEnd ℂ) z) / 2
[PROOFSTEP]
simp only [add_conj, ofReal_mul, ofReal_one, ofReal_bit0, this, mul_div_cancel_left (z.re : ℂ) two_ne_zero]
[GOAL]
z : ℂ
⊢ ↑z.im = (z - ↑(starRingEnd ℂ) z) / (2 * I)
[PROOFSTEP]
have : (↑2 : ℝ) * I = 2 * I := by rfl
[GOAL]
z : ℂ
⊢ ↑2 * I = 2 * I
[PROOFSTEP]
rfl
[GOAL]
z : ℂ
this : ↑2 * I = 2 * I
⊢ ↑z.im = (z - ↑(starRingEnd ℂ) z) / (2 * I)
[PROOFSTEP]
simp only [sub_conj, ofReal_mul, ofReal_one, ofReal_bit0, mul_right_comm, this,
  mul_div_cancel_left _ (mul_ne_zero two_ne_zero I_ne_zero : 2 * I ≠ 0)]
[GOAL]
z : ℂ
⊢ Real.sqrt (↑normSq (↑(starRingEnd ℂ) z)) = Real.sqrt (↑normSq z)
[PROOFSTEP]
simp
[GOAL]
z : ℂ
⊢ |z.re| ≤ Real.sqrt (↑normSq z)
[PROOFSTEP]
rw [mul_self_le_mul_self_iff (abs_nonneg z.re) (abs_nonneg' _), abs_mul_abs_self, mul_self_abs]
[GOAL]
z : ℂ
⊢ z.re * z.re ≤ ↑normSq z
[PROOFSTEP]
apply re_sq_le_normSq
[GOAL]
z w : ℂ
⊢ Real.sqrt (↑normSq (z * w)) = Real.sqrt (↑normSq z) * Real.sqrt (↑normSq w)
[PROOFSTEP]
rw [normSq_mul, Real.sqrt_mul (normSq_nonneg _)]
[GOAL]
z w : ℂ
⊢ Real.sqrt (↑normSq (z + w)) * Real.sqrt (↑normSq (z + w)) ≤
    (Real.sqrt (↑normSq z) + Real.sqrt (↑normSq w)) * (Real.sqrt (↑normSq z) + Real.sqrt (↑normSq w))
[PROOFSTEP]
rw [mul_self_abs, add_mul_self_eq, mul_self_abs, mul_self_abs, add_right_comm, normSq_add, add_le_add_iff_left,
  mul_assoc, mul_le_mul_left (zero_lt_two' ℝ), ← Real.sqrt_mul <| normSq_nonneg z, ← normSq_conj w, ← map_mul]
[GOAL]
z w : ℂ
⊢ (z * ↑(starRingEnd ℂ) w).re ≤ Real.sqrt (↑normSq (z * ↑(starRingEnd ℂ) w))
[PROOFSTEP]
exact re_le_abs (z * conj w)
[GOAL]
r : ℝ
⊢ ↑abs ↑r = |r|
[PROOFSTEP]
simp [Complex.abs, normSq_ofReal, Real.sqrt_mul_self_eq_abs]
[GOAL]
n : ℕ
⊢ ↑abs ↑n = ↑abs ↑↑n
[PROOFSTEP]
rw [ofReal_nat_cast]
[GOAL]
z : ℂ
⊢ ↑abs z ^ 2 - z.re ^ 2 = z.im ^ 2
[PROOFSTEP]
rw [sq_abs, normSq_apply, ← sq, ← sq, add_sub_cancel']
[GOAL]
z : ℂ
⊢ ↑abs z ^ 2 - z.im ^ 2 = z.re ^ 2
[PROOFSTEP]
rw [← sq_abs_sub_sq_re, sub_sub_cancel]
[GOAL]
⊢ ↑abs I = 1
[PROOFSTEP]
simp [Complex.abs]
[GOAL]
⊢ ↑abs 2 = ↑abs ↑2
[PROOFSTEP]
rfl
[GOAL]
⊢ 0 ≤ 2
[PROOFSTEP]
norm_num
[GOAL]
⊢ range ↑abs ⊆ Ici 0
[PROOFSTEP]
simp only [range_subset_iff, Ici, mem_setOf_eq, map_nonneg, forall_const]
[GOAL]
z : ℂ
⊢ z.re ^ 2 ≤ ↑normSq z
[PROOFSTEP]
rw [normSq_apply, ← sq]
[GOAL]
z : ℂ
⊢ z.re ^ 2 ≤ z.re ^ 2 + z.im * z.im
[PROOFSTEP]
exact le_add_of_nonneg_right (mul_self_nonneg _)
[GOAL]
z : ℂ
⊢ z.im ^ 2 ≤ ↑normSq z
[PROOFSTEP]
rw [normSq_apply, ← sq, ← sq]
[GOAL]
z : ℂ
⊢ z.im ^ 2 ≤ z.re ^ 2 + z.im ^ 2
[PROOFSTEP]
exact le_add_of_nonneg_left (sq_nonneg _)
[GOAL]
z : ℂ
⊢ |z.re| < ↑abs z ↔ z.im ≠ 0
[PROOFSTEP]
rw [Complex.abs, AbsoluteValue.coe_mk, MulHom.coe_mk, Real.lt_sqrt (abs_nonneg _), normSq_apply, _root_.sq_abs, ← sq,
  lt_add_iff_pos_right, mul_self_pos]
[GOAL]
z : ℂ
⊢ |z.im| < ↑abs z ↔ z.re ≠ 0
[PROOFSTEP]
simpa using @abs_re_lt_abs (z * I)
[GOAL]
z : ℂ
⊢ ↑abs z ≤ |z.re| + |z.im|
[PROOFSTEP]
simpa [re_add_im] using Complex.abs.add_le z.re (z.im * I)
[GOAL]
⊢ 1 ≠ 0
[PROOFSTEP]
apply one_ne_zero
[GOAL]
z : ℂ
⊢ ↑abs z ≤ Real.sqrt 2 * max |z.re| |z.im|
[PROOFSTEP]
cases' z with x y
[GOAL]
case mk
x y : ℝ
⊢ ↑abs { re := x, im := y } ≤ Real.sqrt 2 * max |{ re := x, im := y }.re| |{ re := x, im := y }.im|
[PROOFSTEP]
simp only [abs_apply, normSq_mk, ← sq]
[GOAL]
case mk
x y : ℝ
⊢ Real.sqrt (x ^ 2 + y ^ 2) ≤ Real.sqrt 2 * max |x| |y|
[PROOFSTEP]
by_cases hle : |x| ≤ |y|
[GOAL]
case pos
x y : ℝ
hle : |x| ≤ |y|
⊢ Real.sqrt (x ^ 2 + y ^ 2) ≤ Real.sqrt 2 * max |x| |y|
[PROOFSTEP]
calc
  Real.sqrt (x ^ 2 + y ^ 2) ≤ Real.sqrt (y ^ 2 + y ^ 2) := Real.sqrt_le_sqrt (add_le_add_right (sq_le_sq.2 hle) _)
  _ = Real.sqrt 2 * max |x| |y| := by rw [max_eq_right hle, ← two_mul, Real.sqrt_mul two_pos.le, Real.sqrt_sq_eq_abs]
[GOAL]
x y : ℝ
hle : |x| ≤ |y|
⊢ Real.sqrt (y ^ 2 + y ^ 2) = Real.sqrt 2 * max |x| |y|
[PROOFSTEP]
rw [max_eq_right hle, ← two_mul, Real.sqrt_mul two_pos.le, Real.sqrt_sq_eq_abs]
[GOAL]
case neg
x y : ℝ
hle : ¬|x| ≤ |y|
⊢ Real.sqrt (x ^ 2 + y ^ 2) ≤ Real.sqrt 2 * max |x| |y|
[PROOFSTEP]
have hle' := le_of_not_le hle
[GOAL]
case neg
x y : ℝ
hle : ¬|x| ≤ |y|
hle' : |y| ≤ |x|
⊢ Real.sqrt (x ^ 2 + y ^ 2) ≤ Real.sqrt 2 * max |x| |y|
[PROOFSTEP]
rw [add_comm]
[GOAL]
case neg
x y : ℝ
hle : ¬|x| ≤ |y|
hle' : |y| ≤ |x|
⊢ Real.sqrt (y ^ 2 + x ^ 2) ≤ Real.sqrt 2 * max |x| |y|
[PROOFSTEP]
calc
  Real.sqrt (y ^ 2 + x ^ 2) ≤ Real.sqrt (x ^ 2 + x ^ 2) := Real.sqrt_le_sqrt (add_le_add_right (sq_le_sq.2 hle') _)
  _ = Real.sqrt 2 * max |x| |y| := by rw [max_eq_left hle', ← two_mul, Real.sqrt_mul two_pos.le, Real.sqrt_sq_eq_abs]
[GOAL]
x y : ℝ
hle : ¬|x| ≤ |y|
hle' : |y| ≤ |x|
⊢ Real.sqrt (x ^ 2 + x ^ 2) = Real.sqrt 2 * max |x| |y|
[PROOFSTEP]
rw [max_eq_left hle', ← two_mul, Real.sqrt_mul two_pos.le, Real.sqrt_sq_eq_abs]
[GOAL]
z : ℂ
hz : z = 0
⊢ |z.re / ↑abs z| ≤ 1
[PROOFSTEP]
simp [hz, zero_le_one]
[GOAL]
z : ℂ
hz : ¬z = 0
⊢ |z.re / ↑abs z| ≤ 1
[PROOFSTEP]
simp_rw [_root_.abs_div, abs_abs, div_le_iff (AbsoluteValue.pos Complex.abs hz), one_mul, abs_re_le_abs]
[GOAL]
z : ℂ
hz : z = 0
⊢ |z.im / ↑abs z| ≤ 1
[PROOFSTEP]
simp [hz, zero_le_one]
[GOAL]
z : ℂ
hz : ¬z = 0
⊢ |z.im / ↑abs z| ≤ 1
[PROOFSTEP]
simp_rw [_root_.abs_div, abs_abs, div_le_iff (AbsoluteValue.pos Complex.abs hz), one_mul, abs_im_le_abs]
[GOAL]
n : ℕ
⊢ ↑abs ↑n = ↑n
[PROOFSTEP]
rw [← ofReal_nat_cast, abs_of_nonneg (Nat.cast_nonneg n)]
[GOAL]
n : ℤ
⊢ |↑n| = ↑abs ↑n
[PROOFSTEP]
rw [← ofReal_int_cast, abs_ofReal]
[GOAL]
x : ℂ
⊢ ↑normSq x = ↑abs x ^ 2
[PROOFSTEP]
simp [abs, sq, abs_def, Real.mul_self_sqrt (normSq_nonneg _)]
[GOAL]
f : CauSeq ℂ ↑abs
ε : ℝ
ε0 : ε > 0
i : ℕ
H : ∀ (j : ℕ), j ≥ i → ↑abs (↑f j - ↑f i) < ε
j : ℕ
ij : j ≥ i
⊢ abs' ((fun n => (↑f n).re) j - (fun n => (↑f n).re) i) ≤ ↑abs (↑f j - ↑f i)
[PROOFSTEP]
simpa using abs_re_le_abs (f j - f i)
[GOAL]
f : CauSeq ℂ ↑abs
ε : ℝ
ε0 : ε > 0
i : ℕ
H : ∀ (j : ℕ), j ≥ i → ↑abs (↑f j - ↑f i) < ε
j : ℕ
ij : j ≥ i
⊢ abs' ((fun n => (↑f n).im) j - (fun n => (↑f n).im) i) ≤ ↑abs (↑f j - ↑f i)
[PROOFSTEP]
simpa using abs_im_le_abs (f j - f i)
[GOAL]
f : CauSeq ℂ ↑abs
ε : ℝ
ε0 : ε > 0
i : ℕ
H :
  ∀ (j : ℕ),
    j ≥ i →
      abs'
            (↑({ val := fun n => (↑f n).re, property := (_ : IsCauSeq abs' fun n => (↑f n).re) } -
                  CauSeq.const abs'
                    (CauSeq.lim { val := fun n => (↑f n).re, property := (_ : IsCauSeq abs' fun n => (↑f n).re) }))
              j) <
          ε / 2 ∧
        abs'
            (↑({ val := fun n => (↑f n).im, property := (_ : IsCauSeq abs' fun n => (↑f n).im) } -
                  CauSeq.const abs'
                    (CauSeq.lim { val := fun n => (↑f n).im, property := (_ : IsCauSeq abs' fun n => (↑f n).im) }))
              j) <
          ε / 2
j : ℕ
ij : j ≥ i
⊢ ↑abs (↑(f - CauSeq.const (↑abs) (limAux f)) j) < ε
[PROOFSTEP]
cases' H _ ij with H₁ H₂
[GOAL]
case intro
f : CauSeq ℂ ↑abs
ε : ℝ
ε0 : ε > 0
i : ℕ
H :
  ∀ (j : ℕ),
    j ≥ i →
      abs'
            (↑({ val := fun n => (↑f n).re, property := (_ : IsCauSeq abs' fun n => (↑f n).re) } -
                  CauSeq.const abs'
                    (CauSeq.lim { val := fun n => (↑f n).re, property := (_ : IsCauSeq abs' fun n => (↑f n).re) }))
              j) <
          ε / 2 ∧
        abs'
            (↑({ val := fun n => (↑f n).im, property := (_ : IsCauSeq abs' fun n => (↑f n).im) } -
                  CauSeq.const abs'
                    (CauSeq.lim { val := fun n => (↑f n).im, property := (_ : IsCauSeq abs' fun n => (↑f n).im) }))
              j) <
          ε / 2
j : ℕ
ij : j ≥ i
H₁ :
  abs'
      (↑({ val := fun n => (↑f n).re, property := (_ : IsCauSeq abs' fun n => (↑f n).re) } -
            CauSeq.const abs'
              (CauSeq.lim { val := fun n => (↑f n).re, property := (_ : IsCauSeq abs' fun n => (↑f n).re) }))
        j) <
    ε / 2
H₂ :
  abs'
      (↑({ val := fun n => (↑f n).im, property := (_ : IsCauSeq abs' fun n => (↑f n).im) } -
            CauSeq.const abs'
              (CauSeq.lim { val := fun n => (↑f n).im, property := (_ : IsCauSeq abs' fun n => (↑f n).im) }))
        j) <
    ε / 2
⊢ ↑abs (↑(f - CauSeq.const (↑abs) (limAux f)) j) < ε
[PROOFSTEP]
apply lt_of_le_of_lt (abs_le_abs_re_add_abs_im _)
[GOAL]
case intro
f : CauSeq ℂ ↑abs
ε : ℝ
ε0 : ε > 0
i : ℕ
H :
  ∀ (j : ℕ),
    j ≥ i →
      abs'
            (↑({ val := fun n => (↑f n).re, property := (_ : IsCauSeq abs' fun n => (↑f n).re) } -
                  CauSeq.const abs'
                    (CauSeq.lim { val := fun n => (↑f n).re, property := (_ : IsCauSeq abs' fun n => (↑f n).re) }))
              j) <
          ε / 2 ∧
        abs'
            (↑({ val := fun n => (↑f n).im, property := (_ : IsCauSeq abs' fun n => (↑f n).im) } -
                  CauSeq.const abs'
                    (CauSeq.lim { val := fun n => (↑f n).im, property := (_ : IsCauSeq abs' fun n => (↑f n).im) }))
              j) <
          ε / 2
j : ℕ
ij : j ≥ i
H₁ :
  abs'
      (↑({ val := fun n => (↑f n).re, property := (_ : IsCauSeq abs' fun n => (↑f n).re) } -
            CauSeq.const abs'
              (CauSeq.lim { val := fun n => (↑f n).re, property := (_ : IsCauSeq abs' fun n => (↑f n).re) }))
        j) <
    ε / 2
H₂ :
  abs'
      (↑({ val := fun n => (↑f n).im, property := (_ : IsCauSeq abs' fun n => (↑f n).im) } -
            CauSeq.const abs'
              (CauSeq.lim { val := fun n => (↑f n).im, property := (_ : IsCauSeq abs' fun n => (↑f n).im) }))
        j) <
    ε / 2
⊢ abs' (↑(f - CauSeq.const (↑abs) (limAux f)) j).re + abs' (↑(f - CauSeq.const (↑abs) (limAux f)) j).im < ε
[PROOFSTEP]
dsimp [limAux] at *
[GOAL]
case intro
f : CauSeq ℂ ↑abs
ε : ℝ
ε0 : ε > 0
i : ℕ
H :
  ∀ (j : ℕ),
    j ≥ i →
      abs' ((↑f j).re - CauSeq.lim { val := fun n => (↑f n).re, property := (_ : IsCauSeq abs' fun n => (↑f n).re) }) <
          ε / 2 ∧
        abs'
            ((↑f j).im - CauSeq.lim { val := fun n => (↑f n).im, property := (_ : IsCauSeq abs' fun n => (↑f n).im) }) <
          ε / 2
j : ℕ
ij : j ≥ i
H₁ :
  abs' ((↑f j).re - CauSeq.lim { val := fun n => (↑f n).re, property := (_ : IsCauSeq abs' fun n => (↑f n).re) }) <
    ε / 2
H₂ :
  abs' ((↑f j).im - CauSeq.lim { val := fun n => (↑f n).im, property := (_ : IsCauSeq abs' fun n => (↑f n).im) }) <
    ε / 2
⊢ abs' ((↑f j).re - CauSeq.lim (cauSeqRe f)) + abs' ((↑f j).im - CauSeq.lim (cauSeqIm f)) < ε
[PROOFSTEP]
have := add_lt_add H₁ H₂
[GOAL]
case intro
f : CauSeq ℂ ↑abs
ε : ℝ
ε0 : ε > 0
i : ℕ
H :
  ∀ (j : ℕ),
    j ≥ i →
      abs' ((↑f j).re - CauSeq.lim { val := fun n => (↑f n).re, property := (_ : IsCauSeq abs' fun n => (↑f n).re) }) <
          ε / 2 ∧
        abs'
            ((↑f j).im - CauSeq.lim { val := fun n => (↑f n).im, property := (_ : IsCauSeq abs' fun n => (↑f n).im) }) <
          ε / 2
j : ℕ
ij : j ≥ i
H₁ :
  abs' ((↑f j).re - CauSeq.lim { val := fun n => (↑f n).re, property := (_ : IsCauSeq abs' fun n => (↑f n).re) }) <
    ε / 2
H₂ :
  abs' ((↑f j).im - CauSeq.lim { val := fun n => (↑f n).im, property := (_ : IsCauSeq abs' fun n => (↑f n).im) }) <
    ε / 2
this :
  abs' ((↑f j).re - CauSeq.lim { val := fun n => (↑f n).re, property := (_ : IsCauSeq abs' fun n => (↑f n).re) }) +
      abs' ((↑f j).im - CauSeq.lim { val := fun n => (↑f n).im, property := (_ : IsCauSeq abs' fun n => (↑f n).im) }) <
    ε / 2 + ε / 2
⊢ abs' ((↑f j).re - CauSeq.lim (cauSeqRe f)) + abs' ((↑f j).im - CauSeq.lim (cauSeqIm f)) < ε
[PROOFSTEP]
rwa [add_halves] at this
[GOAL]
f : CauSeq ℂ ↑abs
x✝ : ℕ
⊢ (↑(CauSeq.const (↑abs) (limAux f)) x✝).re =
    (↑(CauSeq.const (↑abs) (↑(CauSeq.lim (cauSeqRe f)) + ↑(CauSeq.lim (cauSeqIm f)) * I)) x✝).re
[PROOFSTEP]
simp [limAux, cauSeqRe, ofReal']
[GOAL]
f : CauSeq ℂ ↑abs
x✝ : ℕ
⊢ (↑(CauSeq.const (↑abs) (limAux f)) x✝).im =
    (↑(CauSeq.const (↑abs) (↑(CauSeq.lim (cauSeqRe f)) + ↑(CauSeq.lim (cauSeqIm f)) * I)) x✝).im
[PROOFSTEP]
simp [limAux, cauSeqIm, ofReal']
[GOAL]
f : CauSeq ℂ ↑abs
⊢ CauSeq.lim (cauSeqRe f) = (CauSeq.lim f).re
[PROOFSTEP]
rw [lim_eq_lim_im_add_lim_re]
[GOAL]
f : CauSeq ℂ ↑abs
⊢ CauSeq.lim (cauSeqRe f) = (↑(CauSeq.lim (cauSeqRe f)) + ↑(CauSeq.lim (cauSeqIm f)) * I).re
[PROOFSTEP]
simp [ofReal']
[GOAL]
f : CauSeq ℂ ↑abs
⊢ CauSeq.lim (cauSeqIm f) = (CauSeq.lim f).im
[PROOFSTEP]
rw [lim_eq_lim_im_add_lim_re]
[GOAL]
f : CauSeq ℂ ↑abs
⊢ CauSeq.lim (cauSeqIm f) = (↑(CauSeq.lim (cauSeqRe f)) + ↑(CauSeq.lim (cauSeqIm f)) * I).im
[PROOFSTEP]
simp [ofReal']
[GOAL]
f : CauSeq ℂ ↑abs
ε : ℝ
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → ↑abs (↑f j - ↑f i) < ε
j : ℕ
hj : j ≥ i
⊢ ↑abs ((fun n => ↑(starRingEnd ℂ) (↑f n)) j - (fun n => ↑(starRingEnd ℂ) (↑f n)) i) < ε
[PROOFSTEP]
rw [← RingHom.map_sub, abs_conj]
[GOAL]
f : CauSeq ℂ ↑abs
ε : ℝ
ε0 : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → ↑abs (↑f j - ↑f i) < ε
j : ℕ
hj : j ≥ i
⊢ ↑abs (↑f j - ↑f i) < ε
[PROOFSTEP]
exact hi j hj
[GOAL]
f : CauSeq ℂ ↑abs
⊢ (CauSeq.lim (cauSeqConj f)).re = (↑(starRingEnd ℂ) (CauSeq.lim f)).re
[PROOFSTEP]
simp [cauSeqConj, (lim_re _).symm, cauSeqRe]
[GOAL]
f : CauSeq ℂ ↑abs
⊢ (CauSeq.lim (cauSeqConj f)).im = (↑(starRingEnd ℂ) (CauSeq.lim f)).im
[PROOFSTEP]
simp [cauSeqConj, (lim_im _).symm, cauSeqIm, (lim_neg _).symm]
[GOAL]
f : CauSeq ℂ ↑abs
⊢ CauSeq.lim { val := fun n => -(↑f n).im, property := (_ : (fun f => IsCauSeq abs' f) fun n => -(↑f n).im) } =
    CauSeq.lim (-{ val := fun n => (↑f n).im, property := (_ : IsCauSeq abs' fun n => (↑f n).im) })
[PROOFSTEP]
rfl


[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q✝ r p q : R[X]
n : ℕ
⊢ coeff (p + q) n = coeff p n + coeff q n
[PROOFSTEP]
rcases p with ⟨⟩
[GOAL]
case ofFinsupp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q✝ r q : R[X]
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ coeff ({ toFinsupp := toFinsupp✝ } + q) n = coeff { toFinsupp := toFinsupp✝ } n + coeff q n
[PROOFSTEP]
rcases q with ⟨⟩
[GOAL]
case ofFinsupp.ofFinsupp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ coeff ({ toFinsupp := toFinsupp✝¹ } + { toFinsupp := toFinsupp✝ }) n =
    coeff { toFinsupp := toFinsupp✝¹ } n + coeff { toFinsupp := toFinsupp✝ } n
[PROOFSTEP]
simp_rw [← ofFinsupp_add, coeff]
[GOAL]
case ofFinsupp.ofFinsupp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ↑(toFinsupp✝¹ + toFinsupp✝) n = ↑toFinsupp✝¹ n + ↑toFinsupp✝ n
[PROOFSTEP]
exact Finsupp.add_apply _ _ _
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
⊢ coeff (bit0 p) n = bit0 (coeff p n)
[PROOFSTEP]
simp [bit0]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝¹ : Semiring R
p✝ q r✝ : R[X]
inst✝ : SMulZeroClass S R
r : S
p : R[X]
n : ℕ
⊢ coeff (r • p) n = r • coeff p n
[PROOFSTEP]
rcases p with ⟨⟩
[GOAL]
case ofFinsupp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝¹ : Semiring R
p q r✝ : R[X]
inst✝ : SMulZeroClass S R
r : S
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ coeff (r • { toFinsupp := toFinsupp✝ }) n = r • coeff { toFinsupp := toFinsupp✝ } n
[PROOFSTEP]
simp_rw [← ofFinsupp_smul, coeff]
[GOAL]
case ofFinsupp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝¹ : Semiring R
p q r✝ : R[X]
inst✝ : SMulZeroClass S R
r : S
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ↑(r • toFinsupp✝) n = r • ↑toFinsupp✝ n
[PROOFSTEP]
exact Finsupp.smul_apply _ _ _
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝² : Semiring R
p✝ q r✝ : R[X]
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
r : S
p : R[X]
⊢ support (r • p) ⊆ support p
[PROOFSTEP]
intro i hi
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝² : Semiring R
p✝ q r✝ : R[X]
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
r : S
p : R[X]
i : ℕ
hi : i ∈ support (r • p)
⊢ i ∈ support p
[PROOFSTEP]
simp [mem_support_iff] at hi ⊢
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝² : Semiring R
p✝ q r✝ : R[X]
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
r : S
p : R[X]
i : ℕ
hi : ¬r • coeff p i = 0
⊢ ¬coeff p i = 0
[PROOFSTEP]
contrapose! hi
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝² : Semiring R
p✝ q r✝ : R[X]
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
r : S
p : R[X]
i : ℕ
hi : coeff p i = 0
⊢ r • coeff p i = 0
[PROOFSTEP]
simp [hi]
[GOAL]
R✝ : Type u
S : Type v
a b : R✝
n m : ℕ
inst✝⁵ : Semiring R✝
p✝ q r : R✝[X]
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : AddCommMonoid M
inst✝¹ : Module R A
inst✝ : Module R M
f : ℕ → A →ₗ[R] M
c : R
p : A[X]
⊢ AddHom.toFun
      { toFun := fun p => sum p fun x x_1 => ↑(f x) x_1,
        map_add' :=
          (_ :
            ∀ (p q : A[X]),
              (sum (p + q) fun x x_1 => ↑(f x) x_1) = (sum p fun x x_1 => ↑(f x) x_1) + sum q fun x x_1 => ↑(f x) x_1) }
      (c • p) =
    ↑(RingHom.id R) c •
      AddHom.toFun
        { toFun := fun p => sum p fun x x_1 => ↑(f x) x_1,
          map_add' :=
            (_ :
              ∀ (p q : A[X]),
                (sum (p + q) fun x x_1 => ↑(f x) x_1) =
                  (sum p fun x x_1 => ↑(f x) x_1) + sum q fun x x_1 => ↑(f x) x_1) }
        p
[PROOFSTEP]
dsimp only []
[GOAL]
R✝ : Type u
S : Type v
a b : R✝
n m : ℕ
inst✝⁵ : Semiring R✝
p✝ q r : R✝[X]
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : AddCommMonoid M
inst✝¹ : Module R A
inst✝ : Module R M
f : ℕ → A →ₗ[R] M
c : R
p : A[X]
⊢ (sum (c • p) fun x x_1 => ↑(f x) x_1) = ↑(RingHom.id R) c • sum p fun x x_1 => ↑(f x) x_1
[PROOFSTEP]
rw [sum_eq_of_subset (f · ·) (fun n => (f n).map_zero) (support_smul c p)]
[GOAL]
R✝ : Type u
S : Type v
a b : R✝
n m : ℕ
inst✝⁵ : Semiring R✝
p✝ q r : R✝[X]
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : AddCommMonoid M
inst✝¹ : Module R A
inst✝ : Module R M
f : ℕ → A →ₗ[R] M
c : R
p : A[X]
⊢ ∑ n in support p, ↑(f n) (coeff (c • p) n) = ↑(RingHom.id R) c • sum p fun x x_1 => ↑(f x) x_1
[PROOFSTEP]
simp only [sum_def, Finset.smul_sum, coeff_smul, LinearMap.map_smul, RingHom.id_apply]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
n : ℕ
f : ℕ → R → S[X]
⊢ coeff (sum p f) n = sum p fun a b => coeff (f a b) n
[PROOFSTEP]
rcases p with
  ⟨⟩
    -- Porting note: Was `simp [Polynomial.sum, support, coeff]`.
[GOAL]
case ofFinsupp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝¹ : Semiring R
q r : R[X]
inst✝ : Semiring S
n : ℕ
f : ℕ → R → S[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ coeff (sum { toFinsupp := toFinsupp✝ } f) n = sum { toFinsupp := toFinsupp✝ } fun a b => coeff (f a b) n
[PROOFSTEP]
simp [Polynomial.sum, support_ofFinsupp, coeff_ofFinsupp]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q✝ r p q : R[X]
n : ℕ
⊢ coeff (p * q) n = ∑ x in Nat.antidiagonal n, coeff p x.fst * coeff q x.snd
[PROOFSTEP]
rcases p with ⟨p⟩
[GOAL]
case ofFinsupp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q✝ r q : R[X]
n : ℕ
p : AddMonoidAlgebra R ℕ
⊢ coeff ({ toFinsupp := p } * q) n = ∑ x in Nat.antidiagonal n, coeff { toFinsupp := p } x.fst * coeff q x.snd
[PROOFSTEP]
rcases q with ⟨q⟩
[GOAL]
case ofFinsupp.ofFinsupp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q✝ r : R[X]
n : ℕ
p q : AddMonoidAlgebra R ℕ
⊢ coeff ({ toFinsupp := p } * { toFinsupp := q }) n =
    ∑ x in Nat.antidiagonal n, coeff { toFinsupp := p } x.fst * coeff { toFinsupp := q } x.snd
[PROOFSTEP]
simp_rw [← ofFinsupp_mul, coeff]
[GOAL]
case ofFinsupp.ofFinsupp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q✝ r : R[X]
n : ℕ
p q : AddMonoidAlgebra R ℕ
⊢ ↑(p * q) n = ∑ x in Nat.antidiagonal n, ↑p x.fst * ↑q x.snd
[PROOFSTEP]
exact AddMonoidAlgebra.mul_apply_antidiagonal p q n _ Nat.mem_antidiagonal
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ r p q : R[X]
⊢ coeff (p * q) 0 = coeff p 0 * coeff q 0
[PROOFSTEP]
simp [coeff_mul]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
⊢ coeff (p * X) 0 = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
⊢ coeff (X * p) 0 = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
x : R
k n : ℕ
⊢ coeff (↑C x * X ^ k) n = if n = k then x else 0
[PROOFSTEP]
rw [C_mul_X_pow_eq_monomial, coeff_monomial]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
x : R
k n : ℕ
⊢ (if k = n then x else 0) = if n = k then x else 0
[PROOFSTEP]
congr 1
[GOAL]
case e_c
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
x : R
k n : ℕ
⊢ (k = n) = (n = k)
[PROOFSTEP]
simp [eq_comm]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
x : R
n : ℕ
⊢ coeff (↑C x * X) n = if n = 1 then x else 0
[PROOFSTEP]
rw [← pow_one X, coeff_C_mul_X_pow]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
⊢ coeff (↑C a * p) n = a * coeff p n
[PROOFSTEP]
rcases p with ⟨p⟩
[GOAL]
case ofFinsupp
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
p : AddMonoidAlgebra R ℕ
⊢ coeff (↑C a * { toFinsupp := p }) n = a * coeff { toFinsupp := p } n
[PROOFSTEP]
simp_rw [← monomial_zero_left, ← ofFinsupp_single, ← ofFinsupp_mul, coeff]
[GOAL]
case ofFinsupp
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
p : AddMonoidAlgebra R ℕ
⊢ ↑(Finsupp.single 0 a * p) n = a * ↑p n
[PROOFSTEP]
exact AddMonoidAlgebra.single_zero_mul_apply p a n
[GOAL]
R : Type u
S : Type v
a✝ b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
f : R[X]
⊢ ↑C a * f = a • f
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u
S : Type v
a✝ b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
f : R[X]
n✝ : ℕ
⊢ coeff (↑C a * f) n✝ = coeff (a • f) n✝
[PROOFSTEP]
rw [coeff_C_mul, coeff_smul, smul_eq_mul]
[GOAL]
R : Type u
S : Type v
a✝ b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
a : R
⊢ coeff (p * ↑C a) n = coeff p n * a
[PROOFSTEP]
rcases p with ⟨p⟩
[GOAL]
case ofFinsupp
R : Type u
S : Type v
a✝ b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
n : ℕ
a : R
p : AddMonoidAlgebra R ℕ
⊢ coeff ({ toFinsupp := p } * ↑C a) n = coeff { toFinsupp := p } n * a
[PROOFSTEP]
simp_rw [← monomial_zero_left, ← ofFinsupp_single, ← ofFinsupp_mul, coeff]
[GOAL]
case ofFinsupp
R : Type u
S : Type v
a✝ b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
n : ℕ
a : R
p : AddMonoidAlgebra R ℕ
⊢ ↑(p * Finsupp.single 0 a) n = ↑p n * a
[PROOFSTEP]
exact AddMonoidAlgebra.mul_single_zero_apply p a n
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
k n : ℕ
⊢ coeff (X ^ k) n = if n = k then 1 else 0
[PROOFSTEP]
simp only [one_mul, RingHom.map_one, ← coeff_C_mul_X_pow]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
⊢ coeff (X ^ n) n = 1
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
a b : R
n m✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
k m : ℕ
hkm : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ support (↑C x * X ^ k + ↑C y * X ^ m) = {k, m}
[PROOFSTEP]
apply subset_antisymm (support_binomial' k m x y)
[GOAL]
R : Type u
S : Type v
a b : R
n m✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
k m : ℕ
hkm : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ {k, m} ⊆ support (↑C x * X ^ k + ↑C y * X ^ m)
[PROOFSTEP]
simp_rw [insert_subset_iff, singleton_subset_iff, mem_support_iff, coeff_add, coeff_C_mul, coeff_X_pow_self, mul_one,
  coeff_X_pow, if_neg hkm, if_neg hkm.symm, mul_zero, zero_add, add_zero, Ne.def, hx, hy]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ support (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) = {k, m, n}
[PROOFSTEP]
apply subset_antisymm (support_trinomial' k m n x y z)
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ {k, m, n} ⊆ support (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n)
[PROOFSTEP]
simp_rw [insert_subset_iff, singleton_subset_iff, mem_support_iff, coeff_add, coeff_C_mul, coeff_X_pow_self, mul_one,
  coeff_X_pow, if_neg hkm.ne, if_neg hkm.ne', if_neg hmn.ne, if_neg hmn.ne', if_neg (hkm.trans hmn).ne,
  if_neg (hkm.trans hmn).ne', mul_zero, add_zero, zero_add, Ne.def, hx, hy, hz]
[GOAL]
R : Type u
S : Type v
a b : R
n m✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
k m : ℕ
h : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ card (support (↑C x * X ^ k + ↑C y * X ^ m)) = 2
[PROOFSTEP]
rw [support_binomial h hx hy, card_insert_of_not_mem (mt mem_singleton.mp h), card_singleton]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ card (support (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n)) = 3
[PROOFSTEP]
rw [support_trinomial hkm hmn hx hy hz,
  card_insert_of_not_mem (mt mem_insert.mp (not_or_of_not hkm.ne (mt mem_singleton.mp (hkm.trans hmn).ne))),
  card_insert_of_not_mem (mt mem_singleton.mp hmn.ne), card_singleton]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d : ℕ
⊢ coeff (p * X ^ n) (d + n) = coeff p d
[PROOFSTEP]
rw [coeff_mul, sum_eq_single (d, n), coeff_X_pow, if_pos rfl, mul_one]
[GOAL]
case h₀
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d : ℕ
⊢ ∀ (b : ℕ × ℕ), b ∈ Nat.antidiagonal (d + n) → b ≠ (d, n) → coeff p b.fst * coeff (X ^ n) b.snd = 0
[PROOFSTEP]
rintro ⟨i, j⟩ h1 h2
[GOAL]
case h₀.mk
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d i j : ℕ
h1 : (i, j) ∈ Nat.antidiagonal (d + n)
h2 : (i, j) ≠ (d, n)
⊢ coeff p (i, j).fst * coeff (X ^ n) (i, j).snd = 0
[PROOFSTEP]
rw [coeff_X_pow, if_neg, mul_zero]
[GOAL]
case h₀.mk.hnc
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d i j : ℕ
h1 : (i, j) ∈ Nat.antidiagonal (d + n)
h2 : (i, j) ≠ (d, n)
⊢ ¬(i, j).snd = n
[PROOFSTEP]
rintro rfl
[GOAL]
case h₀.mk.hnc
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
d i j : ℕ
h1 : (i, j) ∈ Nat.antidiagonal (d + (i, j).snd)
h2 : (i, j) ≠ (d, (i, j).snd)
⊢ False
[PROOFSTEP]
apply h2
[GOAL]
case h₀.mk.hnc
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
d i j : ℕ
h1 : (i, j) ∈ Nat.antidiagonal (d + (i, j).snd)
h2 : (i, j) ≠ (d, (i, j).snd)
⊢ (i, j) = (d, (i, j).snd)
[PROOFSTEP]
rw [Nat.mem_antidiagonal, add_right_cancel_iff] at h1
[GOAL]
case h₀.mk.hnc
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
d i j : ℕ
h1 : (i, j).fst = d
h2 : (i, j) ≠ (d, (i, j).snd)
⊢ (i, j) = (d, (i, j).snd)
[PROOFSTEP]
subst h1
[GOAL]
case h₀.mk.hnc
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
i j : ℕ
h2 : (i, j) ≠ ((i, j).fst, (i, j).snd)
⊢ (i, j) = ((i, j).fst, (i, j).snd)
[PROOFSTEP]
rfl
[GOAL]
case h₁
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d : ℕ
⊢ ¬(d, n) ∈ Nat.antidiagonal (d + n) → coeff p (d, n).fst * coeff (X ^ n) (d, n).snd = 0
[PROOFSTEP]
exact fun h1 => (h1 (Nat.mem_antidiagonal.2 rfl)).elim
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d : ℕ
⊢ coeff (X ^ n * p) (d + n) = coeff p d
[PROOFSTEP]
rw [(commute_X_pow p n).eq, coeff_mul_X_pow]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d : ℕ
⊢ coeff (p * X ^ n) d = if n ≤ d then coeff p (d - n) else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d : ℕ
h : n ≤ d
⊢ coeff (p * X ^ n) d = coeff p (d - n)
[PROOFSTEP]
rw [← tsub_add_cancel_of_le h, coeff_mul_X_pow, add_tsub_cancel_right]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d : ℕ
h : ¬n ≤ d
⊢ coeff (p * X ^ n) d = 0
[PROOFSTEP]
refine' (coeff_mul _ _ _).trans (Finset.sum_eq_zero fun x hx => _)
[GOAL]
case neg
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ Nat.antidiagonal d
⊢ coeff p x.fst * coeff (X ^ n) x.snd = 0
[PROOFSTEP]
rw [coeff_X_pow, if_neg, mul_zero]
[GOAL]
case neg.hnc
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ Nat.antidiagonal d
⊢ ¬x.snd = n
[PROOFSTEP]
exact ((le_of_add_le_right (Finset.Nat.mem_antidiagonal.mp hx).le).trans_lt <| not_le.mp h).ne
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d : ℕ
⊢ coeff (X ^ n * p) d = if n ≤ d then coeff p (d - n) else 0
[PROOFSTEP]
rw [(commute_X_pow p n).eq, coeff_mul_X_pow']
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
⊢ coeff (p * X) (n + 1) = coeff p n
[PROOFSTEP]
simpa only [pow_one] using coeff_mul_X_pow p 1 n
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
⊢ coeff (X * p) (n + 1) = coeff p n
[PROOFSTEP]
rw [(commute_X p).eq, coeff_mul_X]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r✝ p : R[X]
n d : ℕ
r : R
⊢ coeff (p * ↑(monomial n) r) (d + n) = coeff p d * r
[PROOFSTEP]
rw [← C_mul_X_pow_eq_monomial, ← X_pow_mul, ← mul_assoc, coeff_mul_C, coeff_mul_X_pow]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r✝ p : R[X]
n d : ℕ
r : R
⊢ coeff (↑(monomial n) r * p) (d + n) = r * coeff p d
[PROOFSTEP]
rw [← C_mul_X_pow_eq_monomial, mul_assoc, coeff_C_mul, X_pow_mul, coeff_mul_X_pow]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ IsRegular X
[PROOFSTEP]
suffices : IsLeftRegular (X : R[X])
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
this : IsLeftRegular X
⊢ IsRegular X
[PROOFSTEP]
exact ⟨this, this.right_of_commute commute_X⟩
[GOAL]
case this
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ IsLeftRegular X
[PROOFSTEP]
intro P Q (hPQ : X * P = X * Q)
[GOAL]
case this
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r P Q : R[X]
hPQ : X * P = X * Q
⊢ P = Q
[PROOFSTEP]
ext i
[GOAL]
case this.a
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r P Q : R[X]
hPQ : X * P = X * Q
i : ℕ
⊢ coeff P i = coeff Q i
[PROOFSTEP]
rw [← coeff_X_mul P i, hPQ, coeff_X_mul Q i]
  -- TODO Unify this with `Polynomial.Monic.isRegular`
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
n k : ℕ
⊢ coeff ((X + ↑C r) ^ n) k = r ^ (n - k) * ↑(Nat.choose n k)
[PROOFSTEP]
rw [(commute_X (C r : R[X])).add_pow, ← lcoeff_apply, LinearMap.map_sum]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
n k : ℕ
⊢ ∑ i in range (n + 1), ↑(lcoeff R k) (X ^ i * ↑C r ^ (n - i) * ↑(Nat.choose n i)) = r ^ (n - k) * ↑(Nat.choose n k)
[PROOFSTEP]
simp only [one_pow, mul_one, lcoeff_apply, ← C_eq_nat_cast, ← C_pow, coeff_mul_C, Nat.cast_id]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
n k : ℕ
⊢ ∑ x in range (n + 1), coeff (X ^ x) k * r ^ (n - x) * ↑(Nat.choose n x) = r ^ (n - k) * ↑(Nat.choose n k)
[PROOFSTEP]
rw [Finset.sum_eq_single k, coeff_X_pow_self, one_mul]
[GOAL]
case h₀
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
n k : ℕ
⊢ ∀ (b : ℕ), b ∈ range (n + 1) → b ≠ k → coeff (X ^ b) k * r ^ (n - b) * ↑(Nat.choose n b) = 0
[PROOFSTEP]
intro _ _ h
[GOAL]
case h₀
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
n k b✝ : ℕ
a✝ : b✝ ∈ range (n + 1)
h : b✝ ≠ k
⊢ coeff (X ^ b✝) k * r ^ (n - b✝) * ↑(Nat.choose n b✝) = 0
[PROOFSTEP]
simp [coeff_X_pow, h.symm]
[GOAL]
case h₁
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
n k : ℕ
⊢ ¬k ∈ range (n + 1) → coeff (X ^ k) k * r ^ (n - k) * ↑(Nat.choose n k) = 0
[PROOFSTEP]
simp only [coeff_X_pow_self, one_mul, not_lt, Finset.mem_range]
[GOAL]
case h₁
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
n k : ℕ
⊢ n + 1 ≤ k → r ^ (n - k) * ↑(Nat.choose n k) = 0
[PROOFSTEP]
intro h
[GOAL]
case h₁
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
n k : ℕ
h : n + 1 ≤ k
⊢ r ^ (n - k) * ↑(Nat.choose n k) = 0
[PROOFSTEP]
rw [Nat.choose_eq_zero_of_lt h, Nat.cast_zero, mul_zero]
[GOAL]
R✝ : Type u
S : Type v
a b : R✝
n✝ m : ℕ
inst✝¹ : Semiring R✝
p q r : R✝[X]
R : Type u_1
inst✝ : Semiring R
n k : ℕ
⊢ coeff ((X + 1) ^ n) k = ↑(Nat.choose n k)
[PROOFSTEP]
rw [← C_1, coeff_X_add_C_pow, one_pow, one_mul]
[GOAL]
R✝ : Type u
S : Type v
a b : R✝
n✝ m : ℕ
inst✝¹ : Semiring R✝
p q r : R✝[X]
R : Type u_1
inst✝ : Semiring R
n k : ℕ
⊢ coeff ((1 + X) ^ n) k = ↑(Nat.choose n k)
[PROOFSTEP]
rw [add_comm _ X, coeff_X_add_one_pow]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
⊢ ↑C r ∣ φ ↔ ∀ (i : ℕ), r ∣ coeff φ i
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
⊢ ↑C r ∣ φ → ∀ (i : ℕ), r ∣ coeff φ i
[PROOFSTEP]
rintro ⟨φ, rfl⟩ c
[GOAL]
case mp.intro
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ
⊢ r ∣ coeff (↑C r * φ) c
[PROOFSTEP]
rw [coeff_C_mul]
[GOAL]
case mp.intro
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ
⊢ r ∣ r * coeff φ c
[PROOFSTEP]
apply dvd_mul_right
[GOAL]
case mpr
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
⊢ (∀ (i : ℕ), r ∣ coeff φ i) → ↑C r ∣ φ
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
h : ∀ (i : ℕ), r ∣ coeff φ i
⊢ ↑C r ∣ φ
[PROOFSTEP]
choose c hc using h
[GOAL]
case mpr
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
⊢ ↑C r ∣ φ
[PROOFSTEP]
classical
let c' : ℕ → R := fun i => if i ∈ φ.support then c i else 0
let ψ : R[X] := ∑ i in φ.support, monomial i (c' i)
use ψ
ext i
simp only [coeff_C_mul, mem_support_iff, coeff_monomial, finset_sum_coeff, Finset.sum_ite_eq']
split_ifs with hi
· rw [hc]
· rw [Classical.not_not] at hi
  rwa [mul_zero]
[GOAL]
case mpr
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
⊢ ↑C r ∣ φ
[PROOFSTEP]
let c' : ℕ → R := fun i => if i ∈ φ.support then c i else 0
[GOAL]
case mpr
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
c' : ℕ → R := fun i => if i ∈ support φ then c i else 0
⊢ ↑C r ∣ φ
[PROOFSTEP]
let ψ : R[X] := ∑ i in φ.support, monomial i (c' i)
[GOAL]
case mpr
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
c' : ℕ → R := fun i => if i ∈ support φ then c i else 0
ψ : R[X] := ∑ i in support φ, ↑(monomial i) (c' i)
⊢ ↑C r ∣ φ
[PROOFSTEP]
use ψ
[GOAL]
case h
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
c' : ℕ → R := fun i => if i ∈ support φ then c i else 0
ψ : R[X] := ∑ i in support φ, ↑(monomial i) (c' i)
⊢ φ = ↑C r * ψ
[PROOFSTEP]
ext i
[GOAL]
case h.a
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
c' : ℕ → R := fun i => if i ∈ support φ then c i else 0
ψ : R[X] := ∑ i in support φ, ↑(monomial i) (c' i)
i : ℕ
⊢ coeff φ i = coeff (↑C r * ψ) i
[PROOFSTEP]
simp only [coeff_C_mul, mem_support_iff, coeff_monomial, finset_sum_coeff, Finset.sum_ite_eq']
[GOAL]
case h.a
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
c' : ℕ → R := fun i => if i ∈ support φ then c i else 0
ψ : R[X] := ∑ i in support φ, ↑(monomial i) (c' i)
i : ℕ
⊢ coeff φ i = r * if coeff φ i ≠ 0 then if coeff φ i ≠ 0 then c i else 0 else 0
[PROOFSTEP]
split_ifs with hi
[GOAL]
case pos
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
c' : ℕ → R := fun i => if i ∈ support φ then c i else 0
ψ : R[X] := ∑ i in support φ, ↑(monomial i) (c' i)
i : ℕ
hi : coeff φ i ≠ 0
⊢ coeff φ i = r * c i
[PROOFSTEP]
rw [hc]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
c' : ℕ → R := fun i => if i ∈ support φ then c i else 0
ψ : R[X] := ∑ i in support φ, ↑(monomial i) (c' i)
i : ℕ
hi : ¬coeff φ i ≠ 0
⊢ coeff φ i = r * 0
[PROOFSTEP]
rw [Classical.not_not] at hi
[GOAL]
case neg
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
c' : ℕ → R := fun i => if i ∈ support φ then c i else 0
ψ : R[X] := ∑ i in support φ, ↑(monomial i) (c' i)
i : ℕ
hi : coeff φ i = 0
⊢ coeff φ i = r * 0
[PROOFSTEP]
rwa [mul_zero]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r P Q : R[X]
n : ℕ
⊢ coeff (bit0 P * Q) n = 2 * coeff (P * Q) n
[PROOFSTEP]
simp [bit0, add_mul, two_mul]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r P Q : R[X]
n : ℕ
⊢ coeff (bit1 P * Q) n = 2 * coeff (P * Q) n + coeff Q n
[PROOFSTEP]
simp [bit1, add_mul, coeff_bit0_mul]
[GOAL]
R : Type u
S : Type v
a✝ b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
⊢ a • p = ↑C a * p
[PROOFSTEP]
simp [ext_iff]
[GOAL]
R✝ : Type u
S : Type v
a✝ b : R✝
n✝ m : ℕ
inst✝¹ : Semiring R✝
p✝ q r : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
a : R
⊢ update p n a = p + ↑C (a - coeff p n) * X ^ n
[PROOFSTEP]
ext
[GOAL]
case a
R✝ : Type u
S : Type v
a✝ b : R✝
n✝¹ m : ℕ
inst✝¹ : Semiring R✝
p✝ q r : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
a : R
n✝ : ℕ
⊢ coeff (update p n a) n✝ = coeff (p + ↑C (a - coeff p n) * X ^ n) n✝
[PROOFSTEP]
rw [coeff_update_apply, coeff_add, coeff_C_mul_X_pow]
[GOAL]
case a
R✝ : Type u
S : Type v
a✝ b : R✝
n✝¹ m : ℕ
inst✝¹ : Semiring R✝
p✝ q r : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
a : R
n✝ : ℕ
⊢ (if n✝ = n then a else coeff p n✝) = coeff p n✝ + if n✝ = n then a - coeff p n else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R✝ : Type u
S : Type v
a✝ b : R✝
n✝¹ m : ℕ
inst✝¹ : Semiring R✝
p✝ q r : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
a : R
n✝ : ℕ
h : n✝ = n
⊢ a = coeff p n✝ + (a - coeff p n)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
R✝ : Type u
S : Type v
a✝ b : R✝
n✝¹ m : ℕ
inst✝¹ : Semiring R✝
p✝ q r : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
a : R
n✝ : ℕ
h : ¬n✝ = n
⊢ coeff p n✝ = coeff p n✝ + 0
[PROOFSTEP]
simp [h]
[GOAL]
R✝ : Type u
S : Type v
a b : R✝
n✝ m : ℕ
inst✝¹ : Semiring R✝
p q r : R✝[X]
n : ℕ
R : Type u_1
inst✝ : Semiring R
⊢ coeff (↑n) 0 = ↑n
[PROOFSTEP]
simp only [coeff_nat_cast_ite, ite_true]
[GOAL]
R✝ : Type u
S : Type v
a b : R✝
n✝ m✝ : ℕ
inst✝² : Semiring R✝
p q r : R✝[X]
m n : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
⊢ ↑m = ↑n ↔ m = n
[PROOFSTEP]
constructor
[GOAL]
case mp
R✝ : Type u
S : Type v
a b : R✝
n✝ m✝ : ℕ
inst✝² : Semiring R✝
p q r : R✝[X]
m n : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
⊢ ↑m = ↑n → m = n
[PROOFSTEP]
intro h
[GOAL]
case mp
R✝ : Type u
S : Type v
a b : R✝
n✝ m✝ : ℕ
inst✝² : Semiring R✝
p q r : R✝[X]
m n : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
h : ↑m = ↑n
⊢ m = n
[PROOFSTEP]
apply_fun fun p => p.coeff 0 at h
[GOAL]
case mp
R✝ : Type u
S : Type v
a b : R✝
n✝ m✝ : ℕ
inst✝² : Semiring R✝
p q r : R✝[X]
m n : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
h : coeff (↑m) 0 = coeff (↑n) 0
⊢ m = n
[PROOFSTEP]
simpa using h
[GOAL]
case mpr
R✝ : Type u
S : Type v
a b : R✝
n✝ m✝ : ℕ
inst✝² : Semiring R✝
p q r : R✝[X]
m n : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
⊢ m = n → ↑m = ↑n
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
R✝ : Type u
S : Type v
a b : R✝
n m✝ : ℕ
inst✝² : Semiring R✝
p q r : R✝[X]
m : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
⊢ ↑m = ↑m
[PROOFSTEP]
rfl
[GOAL]
R✝ : Type u
S : Type v
a b : R✝
n m : ℕ
inst✝¹ : Semiring R✝
p q r : R✝[X]
i : ℤ
R : Type u_1
inst✝ : Ring R
⊢ coeff (↑i) 0 = ↑i
[PROOFSTEP]
cases i
[GOAL]
case ofNat
R✝ : Type u
S : Type v
a b : R✝
n m : ℕ
inst✝¹ : Semiring R✝
p q r : R✝[X]
R : Type u_1
inst✝ : Ring R
a✝ : ℕ
⊢ coeff (↑(Int.ofNat a✝)) 0 = ↑(Int.ofNat a✝)
[PROOFSTEP]
simp
[GOAL]
case negSucc
R✝ : Type u
S : Type v
a b : R✝
n m : ℕ
inst✝¹ : Semiring R✝
p q r : R✝[X]
R : Type u_1
inst✝ : Ring R
a✝ : ℕ
⊢ coeff (↑(Int.negSucc a✝)) 0 = ↑(Int.negSucc a✝)
[PROOFSTEP]
simp
[GOAL]
R✝ : Type u
S : Type v
a b : R✝
n✝ m✝ : ℕ
inst✝² : Semiring R✝
p q r : R✝[X]
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ ↑m = ↑n ↔ m = n
[PROOFSTEP]
constructor
[GOAL]
case mp
R✝ : Type u
S : Type v
a b : R✝
n✝ m✝ : ℕ
inst✝² : Semiring R✝
p q r : R✝[X]
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ ↑m = ↑n → m = n
[PROOFSTEP]
intro h
[GOAL]
case mp
R✝ : Type u
S : Type v
a b : R✝
n✝ m✝ : ℕ
inst✝² : Semiring R✝
p q r : R✝[X]
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
h : ↑m = ↑n
⊢ m = n
[PROOFSTEP]
apply_fun fun p => p.coeff 0 at h
[GOAL]
case mp
R✝ : Type u
S : Type v
a b : R✝
n✝ m✝ : ℕ
inst✝² : Semiring R✝
p q r : R✝[X]
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
h : coeff (↑m) 0 = coeff (↑n) 0
⊢ m = n
[PROOFSTEP]
simpa using h
[GOAL]
case mpr
R✝ : Type u
S : Type v
a b : R✝
n✝ m✝ : ℕ
inst✝² : Semiring R✝
p q r : R✝[X]
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ m = n → ↑m = ↑n
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
R✝ : Type u
S : Type v
a b : R✝
n m✝ : ℕ
inst✝² : Semiring R✝
p q r : R✝[X]
m : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ ↑m = ↑m
[PROOFSTEP]
rfl