[GOAL]
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
⊢ ↑(expand R p) (cyclotomic n R) = cyclotomic (n * p) R * cyclotomic n R
[PROOFSTEP]
rcases Nat.eq_zero_or_pos n with (rfl | hnpos)
[GOAL]
case inl
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝ : CommRing R
hdiv : ¬p ∣ 0
⊢ ↑(expand R p) (cyclotomic 0 R) = cyclotomic (0 * p) R * cyclotomic 0 R
[PROOFSTEP]
simp
[GOAL]
case inr
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
⊢ ↑(expand R p) (cyclotomic n R) = cyclotomic (n * p) R * cyclotomic n R
[PROOFSTEP]
haveI := NeZero.of_pos hnpos
[GOAL]
case inr
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ ↑(expand R p) (cyclotomic n R) = cyclotomic (n * p) R * cyclotomic n R
[PROOFSTEP]
suffices expand ℤ p (cyclotomic n ℤ) = cyclotomic (n * p) ℤ * cyclotomic n ℤ by
  rw [← map_cyclotomic_int, ← map_expand, this, Polynomial.map_mul, map_cyclotomic_int, map_cyclotomic]
[GOAL]
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this✝ : NeZero n
this : ↑(expand ℤ p) (cyclotomic n ℤ) = cyclotomic (n * p) ℤ * cyclotomic n ℤ
⊢ ↑(expand R p) (cyclotomic n R) = cyclotomic (n * p) R * cyclotomic n R
[PROOFSTEP]
rw [← map_cyclotomic_int, ← map_expand, this, Polynomial.map_mul, map_cyclotomic_int, map_cyclotomic]
[GOAL]
case inr
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ ↑(expand ℤ p) (cyclotomic n ℤ) = cyclotomic (n * p) ℤ * cyclotomic n ℤ
[PROOFSTEP]
refine'
  eq_of_monic_of_dvd_of_natDegree_le ((cyclotomic.monic _ ℤ).mul (cyclotomic.monic _ _))
    ((cyclotomic.monic n ℤ).expand hp.pos) _ _
[GOAL]
case inr.refine'_1
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ cyclotomic (n * p) ℤ * cyclotomic n ℤ ∣ ↑(expand ℤ p) (cyclotomic n ℤ)
[PROOFSTEP]
refine'
  (IsPrimitive.Int.dvd_iff_map_cast_dvd_map_cast _ _
        (IsPrimitive.mul (cyclotomic.isPrimitive (n * p) ℤ) (cyclotomic.isPrimitive n ℤ))
        ((cyclotomic.monic n ℤ).expand hp.pos).isPrimitive).2
    _
[GOAL]
case inr.refine'_1
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ map (Int.castRingHom ℚ) (cyclotomic (n * p) ℤ * cyclotomic n ℤ) ∣
    map (Int.castRingHom ℚ) (↑(expand ℤ p) (cyclotomic n ℤ))
[PROOFSTEP]
rw [Polynomial.map_mul, map_cyclotomic_int, map_cyclotomic_int, map_expand, map_cyclotomic_int]
[GOAL]
case inr.refine'_1
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ cyclotomic (n * p) ℚ * cyclotomic n ℚ ∣ ↑(expand ℚ p) (cyclotomic n ℚ)
[PROOFSTEP]
refine' IsCoprime.mul_dvd (cyclotomic.isCoprime_rat fun h => _) _ _
[GOAL]
case inr.refine'_1.refine'_1
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
h : n * p = n
⊢ False
[PROOFSTEP]
replace h : n * p = n * 1 := by simp [h]
[GOAL]
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
h : n * p = n
⊢ n * p = n * 1
[PROOFSTEP]
simp [h]
[GOAL]
case inr.refine'_1.refine'_1
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
h : n * p = n * 1
⊢ False
[PROOFSTEP]
exact Nat.Prime.ne_one hp (mul_left_cancel₀ hnpos.ne' h)
[GOAL]
case inr.refine'_1.refine'_2
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ cyclotomic (n * p) ℚ ∣ ↑(expand ℚ p) (cyclotomic n ℚ)
[PROOFSTEP]
have hpos : 0 < n * p := mul_pos hnpos hp.pos
[GOAL]
case inr.refine'_1.refine'_2
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
hpos : 0 < n * p
⊢ cyclotomic (n * p) ℚ ∣ ↑(expand ℚ p) (cyclotomic n ℚ)
[PROOFSTEP]
have hprim := Complex.isPrimitiveRoot_exp _ hpos.ne'
[GOAL]
case inr.refine'_1.refine'_2
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
hpos : 0 < n * p
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p))) (n * p)
⊢ cyclotomic (n * p) ℚ ∣ ↑(expand ℚ p) (cyclotomic n ℚ)
[PROOFSTEP]
rw [cyclotomic_eq_minpoly_rat hprim hpos]
[GOAL]
case inr.refine'_1.refine'_2
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
hpos : 0 < n * p
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p))) (n * p)
⊢ minpoly ℚ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p))) ∣ ↑(expand ℚ p) (cyclotomic n ℚ)
[PROOFSTEP]
refine' @minpoly.dvd ℚ ℂ _ _ algebraRat _ _ _
[GOAL]
case inr.refine'_1.refine'_2
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
hpos : 0 < n * p
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p))) (n * p)
⊢ ↑(aeval (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p)))) (↑(expand ℚ p) (cyclotomic n ℚ)) = 0
[PROOFSTEP]
rw [aeval_def, ← eval_map, map_expand, map_cyclotomic, expand_eval, ← IsRoot.def, @isRoot_cyclotomic_iff]
[GOAL]
case inr.refine'_1.refine'_2
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
hpos : 0 < n * p
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p))) (n * p)
⊢ IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p)) ^ p) n
[PROOFSTEP]
convert IsPrimitiveRoot.pow_of_dvd hprim hp.ne_zero (dvd_mul_left p n)
[GOAL]
case h.e'_4
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
hpos : 0 < n * p
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p))) (n * p)
⊢ n = n * p / p
[PROOFSTEP]
rw [Nat.mul_div_cancel _ (Nat.Prime.pos hp)]
[GOAL]
case inr.refine'_1.refine'_3
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ cyclotomic n ℚ ∣ ↑(expand ℚ p) (cyclotomic n ℚ)
[PROOFSTEP]
have hprim := Complex.isPrimitiveRoot_exp _ hnpos.ne.symm
[GOAL]
case inr.refine'_1.refine'_3
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) n
⊢ cyclotomic n ℚ ∣ ↑(expand ℚ p) (cyclotomic n ℚ)
[PROOFSTEP]
rw [cyclotomic_eq_minpoly_rat hprim hnpos]
[GOAL]
case inr.refine'_1.refine'_3
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) n
⊢ minpoly ℚ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) ∣
    ↑(expand ℚ p) (minpoly ℚ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)))
[PROOFSTEP]
refine' @minpoly.dvd ℚ ℂ _ _ algebraRat _ _ _
[GOAL]
case inr.refine'_1.refine'_3
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) n
⊢ ↑(aeval (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)))
      (↑(expand ℚ p) (minpoly ℚ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)))) =
    0
[PROOFSTEP]
rw [aeval_def, ← eval_map, map_expand, expand_eval, ← IsRoot.def, ← cyclotomic_eq_minpoly_rat hprim hnpos,
  map_cyclotomic, @isRoot_cyclotomic_iff]
[GOAL]
case inr.refine'_1.refine'_3
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) n
⊢ IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n) ^ p) n
[PROOFSTEP]
exact IsPrimitiveRoot.pow_of_prime hprim hp hdiv
[GOAL]
case inr.refine'_2
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ natDegree (↑(expand ℤ p) (cyclotomic n ℤ)) ≤ natDegree (cyclotomic (n * p) ℤ * cyclotomic n ℤ)
[PROOFSTEP]
rw [natDegree_expand, natDegree_cyclotomic, natDegree_mul (cyclotomic_ne_zero _ ℤ) (cyclotomic_ne_zero _ ℤ),
  natDegree_cyclotomic, natDegree_cyclotomic, mul_comm n, Nat.totient_mul ((Nat.Prime.coprime_iff_not_dvd hp).2 hdiv),
  Nat.totient_prime hp, mul_comm (p - 1), ← Nat.mul_succ, Nat.sub_one, Nat.succ_pred_eq_of_pos hp.pos]
[GOAL]
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
⊢ ↑(expand R p) (cyclotomic n R) = cyclotomic (n * p) R
[PROOFSTEP]
rcases n.eq_zero_or_pos with (rfl | hzero)
[GOAL]
case inl
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝ : CommRing R
hdiv : p ∣ 0
⊢ ↑(expand R p) (cyclotomic 0 R) = cyclotomic (0 * p) R
[PROOFSTEP]
simp
[GOAL]
case inr
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
⊢ ↑(expand R p) (cyclotomic n R) = cyclotomic (n * p) R
[PROOFSTEP]
haveI := NeZero.of_pos hzero
[GOAL]
case inr
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this : NeZero n
⊢ ↑(expand R p) (cyclotomic n R) = cyclotomic (n * p) R
[PROOFSTEP]
suffices expand ℤ p (cyclotomic n ℤ) = cyclotomic (n * p) ℤ by
  rw [← map_cyclotomic_int, ← map_expand, this, map_cyclotomic_int, map_cyclotomic]
[GOAL]
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this✝ : NeZero n
this : ↑(expand ℤ p) (cyclotomic n ℤ) = cyclotomic (n * p) ℤ
⊢ ↑(expand R p) (cyclotomic n R) = cyclotomic (n * p) R
[PROOFSTEP]
rw [← map_cyclotomic_int, ← map_expand, this, map_cyclotomic_int, map_cyclotomic]
[GOAL]
case inr
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this : NeZero n
⊢ ↑(expand ℤ p) (cyclotomic n ℤ) = cyclotomic (n * p) ℤ
[PROOFSTEP]
refine' eq_of_monic_of_dvd_of_natDegree_le (cyclotomic.monic _ _) ((cyclotomic.monic n ℤ).expand hp.pos) _ _
[GOAL]
case inr.refine'_1
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this : NeZero n
⊢ cyclotomic (n * p) ℤ ∣ ↑(expand ℤ p) (cyclotomic n ℤ)
[PROOFSTEP]
have hpos := Nat.mul_pos hzero hp.pos
[GOAL]
case inr.refine'_1
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this : NeZero n
hpos : n * p > 0
⊢ cyclotomic (n * p) ℤ ∣ ↑(expand ℤ p) (cyclotomic n ℤ)
[PROOFSTEP]
have hprim := Complex.isPrimitiveRoot_exp _ hpos.ne.symm
[GOAL]
case inr.refine'_1
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this : NeZero n
hpos : n * p > 0
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p))) (n * p)
⊢ cyclotomic (n * p) ℤ ∣ ↑(expand ℤ p) (cyclotomic n ℤ)
[PROOFSTEP]
rw [cyclotomic_eq_minpoly hprim hpos]
[GOAL]
case inr.refine'_1
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this : NeZero n
hpos : n * p > 0
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p))) (n * p)
⊢ minpoly ℤ (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p))) ∣ ↑(expand ℤ p) (cyclotomic n ℤ)
[PROOFSTEP]
refine' minpoly.isIntegrallyClosed_dvd (hprim.isIntegral hpos) _
[GOAL]
case inr.refine'_1
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this : NeZero n
hpos : n * p > 0
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p))) (n * p)
⊢ ↑(aeval (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p)))) (↑(expand ℤ p) (cyclotomic n ℤ)) = 0
[PROOFSTEP]
rw [aeval_def, ← eval_map, map_expand, map_cyclotomic, expand_eval, ← IsRoot.def, @isRoot_cyclotomic_iff]
[GOAL]
case inr.refine'_1
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this : NeZero n
hpos : n * p > 0
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p))) (n * p)
⊢ IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p)) ^ p) n
[PROOFSTEP]
convert IsPrimitiveRoot.pow_of_dvd hprim hp.ne_zero (dvd_mul_left p n)
[GOAL]
case h.e'_4
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this : NeZero n
hpos : n * p > 0
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p))) (n * p)
⊢ n = n * p / p
[PROOFSTEP]
rw [Nat.mul_div_cancel _ hp.pos]
[GOAL]
case inr.refine'_2
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this : NeZero n
⊢ natDegree (↑(expand ℤ p) (cyclotomic n ℤ)) ≤ natDegree (cyclotomic (n * p) ℤ)
[PROOFSTEP]
rw [natDegree_expand, natDegree_cyclotomic, natDegree_cyclotomic, mul_comm n, Nat.totient_mul_of_prime_of_dvd hp hdiv,
  mul_comm]
[GOAL]
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n m : ℕ
hmn : m ≤ n
h : Irreducible (cyclotomic (p ^ n) R)
⊢ Irreducible (cyclotomic (p ^ m) R)
[PROOFSTEP]
rcases m.eq_zero_or_pos with (rfl | hm)
[GOAL]
case inl
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
h : Irreducible (cyclotomic (p ^ n) R)
hmn : 0 ≤ n
⊢ Irreducible (cyclotomic (p ^ 0) R)
[PROOFSTEP]
simpa using irreducible_X_sub_C (1 : R)
[GOAL]
case inr
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n m : ℕ
hmn : m ≤ n
h : Irreducible (cyclotomic (p ^ n) R)
hm : m > 0
⊢ Irreducible (cyclotomic (p ^ m) R)
[PROOFSTEP]
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn
[GOAL]
case inr.intro
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ
hm : m > 0
k : ℕ
hmn : m ≤ m + k
h : Irreducible (cyclotomic (p ^ (m + k)) R)
⊢ Irreducible (cyclotomic (p ^ m) R)
[PROOFSTEP]
induction' k with k hk
[GOAL]
case inr.intro.zero
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ
hm : m > 0
k : ℕ
hmn✝ : m ≤ m + k
h✝ : Irreducible (cyclotomic (p ^ (m + k)) R)
hmn : m ≤ m + Nat.zero
h : Irreducible (cyclotomic (p ^ (m + Nat.zero)) R)
⊢ Irreducible (cyclotomic (p ^ m) R)
[PROOFSTEP]
simpa using h
[GOAL]
case inr.intro.succ
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ
hm : m > 0
k✝ : ℕ
hmn✝ : m ≤ m + k✝
h✝ : Irreducible (cyclotomic (p ^ (m + k✝)) R)
k : ℕ
hk : m ≤ m + k → Irreducible (cyclotomic (p ^ (m + k)) R) → Irreducible (cyclotomic (p ^ m) R)
hmn : m ≤ m + Nat.succ k
h : Irreducible (cyclotomic (p ^ (m + Nat.succ k)) R)
⊢ Irreducible (cyclotomic (p ^ m) R)
[PROOFSTEP]
have : m + k ≠ 0 := (add_pos_of_pos_of_nonneg hm k.zero_le).ne'
[GOAL]
case inr.intro.succ
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ
hm : m > 0
k✝ : ℕ
hmn✝ : m ≤ m + k✝
h✝ : Irreducible (cyclotomic (p ^ (m + k✝)) R)
k : ℕ
hk : m ≤ m + k → Irreducible (cyclotomic (p ^ (m + k)) R) → Irreducible (cyclotomic (p ^ m) R)
hmn : m ≤ m + Nat.succ k
h : Irreducible (cyclotomic (p ^ (m + Nat.succ k)) R)
this : m + k ≠ 0
⊢ Irreducible (cyclotomic (p ^ m) R)
[PROOFSTEP]
rw [Nat.add_succ, pow_succ', ← cyclotomic_expand_eq_cyclotomic hp <| dvd_pow_self p this] at h
[GOAL]
case inr.intro.succ
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ
hm : m > 0
k✝ : ℕ
hmn✝ : m ≤ m + k✝
h✝ : Irreducible (cyclotomic (p ^ (m + k✝)) R)
k : ℕ
hk : m ≤ m + k → Irreducible (cyclotomic (p ^ (m + k)) R) → Irreducible (cyclotomic (p ^ m) R)
hmn : m ≤ m + Nat.succ k
h : Irreducible (↑(expand R p) (cyclotomic (p ^ (m + k)) R))
this : m + k ≠ 0
⊢ Irreducible (cyclotomic (p ^ m) R)
[PROOFSTEP]
exact hk (by linarith) (of_irreducible_expand hp.ne_zero h)
[GOAL]
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ
hm : m > 0
k✝ : ℕ
hmn✝ : m ≤ m + k✝
h✝ : Irreducible (cyclotomic (p ^ (m + k✝)) R)
k : ℕ
hk : m ≤ m + k → Irreducible (cyclotomic (p ^ (m + k)) R) → Irreducible (cyclotomic (p ^ m) R)
hmn : m ≤ m + Nat.succ k
h : Irreducible (↑(expand R p) (cyclotomic (p ^ (m + k)) R))
this : m + k ≠ 0
⊢ m ≤ m + k
[PROOFSTEP]
linarith
[GOAL]
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
⊢ cyclotomic (n * p) R = cyclotomic n R ^ (p - 1)
[PROOFSTEP]
letI : Algebra (ZMod p) R := ZMod.algebra _ _
[GOAL]
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic (n * p) R = cyclotomic n R ^ (p - 1)
[PROOFSTEP]
suffices cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) ^ (p - 1) by
  rw [← map_cyclotomic _ (algebraMap (ZMod p) R), ← map_cyclotomic _ (algebraMap (ZMod p) R), this, Polynomial.map_pow]
[GOAL]
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this✝ : Algebra (ZMod p) R := ZMod.algebra R p
this : cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) ^ (p - 1)
⊢ cyclotomic (n * p) R = cyclotomic n R ^ (p - 1)
[PROOFSTEP]
rw [← map_cyclotomic _ (algebraMap (ZMod p) R), ← map_cyclotomic _ (algebraMap (ZMod p) R), this, Polynomial.map_pow]
[GOAL]
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) ^ (p - 1)
[PROOFSTEP]
apply mul_right_injective₀ (cyclotomic_ne_zero n <| ZMod p)
[GOAL]
case a
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ (fun x x_1 => x * x_1) (cyclotomic n (ZMod p)) (cyclotomic (n * p) (ZMod p)) =
    (fun x x_1 => x * x_1) (cyclotomic n (ZMod p)) (cyclotomic n (ZMod p) ^ (p - 1))
[PROOFSTEP]
dsimp
[GOAL]
case a
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic n (ZMod p) * cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) * cyclotomic n (ZMod p) ^ (p - 1)
[PROOFSTEP]
rw [← pow_succ, tsub_add_cancel_of_le hp.out.one_lt.le, mul_comm, ← ZMod.expand_card]
[GOAL]
case a
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic (n * p) (ZMod p) * cyclotomic n (ZMod p) = ↑(expand (ZMod p) p) (cyclotomic n (ZMod p))
[PROOFSTEP]
conv_rhs => rw [← map_cyclotomic_int]
[GOAL]
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
| ↑(expand (ZMod p) p) (cyclotomic n (ZMod p))
[PROOFSTEP]
rw [← map_cyclotomic_int]
[GOAL]
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
| ↑(expand (ZMod p) p) (cyclotomic n (ZMod p))
[PROOFSTEP]
rw [← map_cyclotomic_int]
[GOAL]
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
| ↑(expand (ZMod p) p) (cyclotomic n (ZMod p))
[PROOFSTEP]
rw [← map_cyclotomic_int]
[GOAL]
case a
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic (n * p) (ZMod p) * cyclotomic n (ZMod p) =
    ↑(expand (ZMod p) p) (map (Int.castRingHom (ZMod p)) (cyclotomic n ℤ))
[PROOFSTEP]
rw [← map_expand, cyclotomic_expand_eq_cyclotomic_mul hp.out hn, Polynomial.map_mul, map_cyclotomic, map_cyclotomic]
[GOAL]
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : p ∣ n
⊢ cyclotomic (n * p) R = cyclotomic n R ^ p
[PROOFSTEP]
letI : Algebra (ZMod p) R := ZMod.algebra _ _
[GOAL]
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic (n * p) R = cyclotomic n R ^ p
[PROOFSTEP]
suffices cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) ^ p by
  rw [← map_cyclotomic _ (algebraMap (ZMod p) R), ← map_cyclotomic _ (algebraMap (ZMod p) R), this, Polynomial.map_pow]
[GOAL]
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : p ∣ n
this✝ : Algebra (ZMod p) R := ZMod.algebra R p
this : cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) ^ p
⊢ cyclotomic (n * p) R = cyclotomic n R ^ p
[PROOFSTEP]
rw [← map_cyclotomic _ (algebraMap (ZMod p) R), ← map_cyclotomic _ (algebraMap (ZMod p) R), this, Polynomial.map_pow]
[GOAL]
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) ^ p
[PROOFSTEP]
rw [← ZMod.expand_card, ← map_cyclotomic_int n, ← map_expand, cyclotomic_expand_eq_cyclotomic hp.out hn, map_cyclotomic,
  mul_comm]
[GOAL]
R : Type u_1
p m : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hm : ¬p ∣ m
x✝ : 0 < 1
⊢ cyclotomic (p ^ 1 * m) R = cyclotomic m R ^ (p ^ 1 - p ^ (1 - 1))
[PROOFSTEP]
rw [pow_one, Nat.sub_self, pow_zero, mul_comm, cyclotomic_mul_prime_eq_pow_of_not_dvd R hm]
[GOAL]
R : Type u_1
p m : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hm : ¬p ∣ m
a : ℕ
x✝ : 0 < a + 2
⊢ cyclotomic (p ^ (a + 2) * m) R = cyclotomic m R ^ (p ^ (a + 2) - p ^ (a + 2 - 1))
[PROOFSTEP]
have hdiv : p ∣ p ^ a.succ * m := ⟨p ^ a * m, by rw [← mul_assoc, pow_succ]⟩
[GOAL]
R : Type u_1
p m : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hm : ¬p ∣ m
a : ℕ
x✝ : 0 < a + 2
⊢ p ^ Nat.succ a * m = p * (p ^ a * m)
[PROOFSTEP]
rw [← mul_assoc, pow_succ]
[GOAL]
R : Type u_1
p m : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hm : ¬p ∣ m
a : ℕ
x✝ : 0 < a + 2
hdiv : p ∣ p ^ Nat.succ a * m
⊢ cyclotomic (p ^ (a + 2) * m) R = cyclotomic m R ^ (p ^ (a + 2) - p ^ (a + 2 - 1))
[PROOFSTEP]
rw [pow_succ, mul_assoc, mul_comm, cyclotomic_mul_prime_dvd_eq_pow R hdiv, cyclotomic_mul_prime_pow_eq _ _ a.succ_pos, ←
  pow_mul]
[GOAL]
R : Type u_1
p m : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hm : ¬p ∣ m
a : ℕ
x✝ : 0 < a + 2
hdiv : p ∣ p ^ Nat.succ a * m
⊢ cyclotomic m R ^ ((p ^ Nat.succ a - p ^ (Nat.succ a - 1)) * p) = cyclotomic m R ^ (p * p ^ (a + 1) - p ^ (a + 2 - 1))
R : Type u_1
p m : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hm : ¬p ∣ m
a : ℕ
x✝ : 0 < a + 2
hdiv : p ∣ p ^ Nat.succ a * m
⊢ ¬p ∣ m
[PROOFSTEP]
congr 1
[GOAL]
case e_a
R : Type u_1
p m : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hm : ¬p ∣ m
a : ℕ
x✝ : 0 < a + 2
hdiv : p ∣ p ^ Nat.succ a * m
⊢ (p ^ Nat.succ a - p ^ (Nat.succ a - 1)) * p = p * p ^ (a + 1) - p ^ (a + 2 - 1)
R : Type u_1
p m : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hm : ¬p ∣ m
a : ℕ
x✝ : 0 < a + 2
hdiv : p ∣ p ^ Nat.succ a * m
⊢ ¬p ∣ m
[PROOFSTEP]
simp only [tsub_zero, Nat.succ_sub_succ_eq_sub]
[GOAL]
case e_a
R : Type u_1
p m : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hm : ¬p ∣ m
a : ℕ
x✝ : 0 < a + 2
hdiv : p ∣ p ^ Nat.succ a * m
⊢ (p ^ Nat.succ a - p ^ a) * p = p * p ^ (a + 1) - p ^ (a + 1)
R : Type u_1
p m : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hm : ¬p ∣ m
a : ℕ
x✝ : 0 < a + 2
hdiv : p ∣ p ^ Nat.succ a * m
⊢ ¬p ∣ m
[PROOFSTEP]
rwa [Nat.mul_sub_right_distrib, mul_comm, pow_succ']
[GOAL]
m k p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
⊢ IsRoot (cyclotomic (p ^ k * m) R) μ ↔ IsPrimitiveRoot μ m
[PROOFSTEP]
rcases k.eq_zero_or_pos with (rfl | hk)
[GOAL]
case inl
m p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
⊢ IsRoot (cyclotomic (p ^ 0 * m) R) μ ↔ IsPrimitiveRoot μ m
[PROOFSTEP]
rw [pow_zero, one_mul, isRoot_cyclotomic_iff]
[GOAL]
case inr
m k p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
hk : k > 0
⊢ IsRoot (cyclotomic (p ^ k * m) R) μ ↔ IsPrimitiveRoot μ m
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case inr.refine'_1
m k p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
hk : k > 0
h : IsRoot (cyclotomic (p ^ k * m) R) μ
⊢ IsPrimitiveRoot μ m
[PROOFSTEP]
rw [IsRoot.def, cyclotomic_mul_prime_pow_eq R (NeZero.not_char_dvd R p m) hk, eval_pow] at h
[GOAL]
case inr.refine'_1
m k p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
hk : k > 0
h : eval μ (cyclotomic m R) ^ (p ^ k - p ^ (k - 1)) = 0
⊢ IsPrimitiveRoot μ m
[PROOFSTEP]
replace h := pow_eq_zero h
[GOAL]
case inr.refine'_1
m k p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
hk : k > 0
h : eval μ (cyclotomic m R) = 0
⊢ IsPrimitiveRoot μ m
[PROOFSTEP]
rwa [← IsRoot.def, isRoot_cyclotomic_iff] at h
[GOAL]
case inr.refine'_2
m k p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
hk : k > 0
h : IsPrimitiveRoot μ m
⊢ IsRoot (cyclotomic (p ^ k * m) R) μ
[PROOFSTEP]
rw [← isRoot_cyclotomic_iff, IsRoot.def] at h
[GOAL]
case inr.refine'_2
m k p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
hk : k > 0
h : eval μ (cyclotomic m R) = 0
⊢ IsRoot (cyclotomic (p ^ k * m) R) μ
[PROOFSTEP]
rw [cyclotomic_mul_prime_pow_eq R (NeZero.not_char_dvd R p m) hk, IsRoot.def, eval_pow, h, zero_pow]
[GOAL]
case inr.refine'_2
m k p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
hk : k > 0
h : eval μ (cyclotomic m R) = 0
⊢ 0 < p ^ k - p ^ (k - 1)
[PROOFSTEP]
simp only [tsub_pos_iff_lt]
[GOAL]
case inr.refine'_2
m k p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
hk : k > 0
h : eval μ (cyclotomic m R) = 0
⊢ p ^ (k - 1) < p ^ k
[PROOFSTEP]
apply pow_strictMono_right hp.out.one_lt (Nat.pred_lt hk.ne')


[GOAL]
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
a : R
b : S
hb : IsInteger R b
⊢ IsInteger R (a • b)
[PROOFSTEP]
rcases hb with ⟨b', hb⟩
[GOAL]
case intro
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
a : R
b : S
b' : R
hb : ↑(algebraMap R S) b' = b
⊢ IsInteger R (a • b)
[PROOFSTEP]
use a * b'
[GOAL]
case h
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
a : R
b : S
b' : R
hb : ↑(algebraMap R S) b' = b
⊢ ↑(algebraMap R S) (a * b') = a • b
[PROOFSTEP]
rw [← hb, (algebraMap R S).map_mul, Algebra.smul_def]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
a : S
⊢ ∃ b, IsInteger R (↑b • a)
[PROOFSTEP]
simp_rw [Algebra.smul_def, mul_comm _ a]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
a : S
⊢ ∃ b, IsInteger R (a * ↑(algebraMap R S) ↑b)
[PROOFSTEP]
apply exists_integer_multiple'
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
⊢ ∃ b, ∀ (i : ι), i ∈ s → IsInteger R (↑b • f i)
[PROOFSTEP]
haveI := Classical.propDecidable
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
⊢ ∃ b, ∀ (i : ι), i ∈ s → IsInteger R (↑b • f i)
[PROOFSTEP]
refine' ⟨∏ i in s, (sec M (f i)).2, fun i hi => ⟨_, _⟩⟩
[GOAL]
case refine'_1
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ R
[PROOFSTEP]
exact (∏ j in s.erase i, (sec M (f j)).2) * (sec M (f i)).1
[GOAL]
case refine'_2
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ ↑(algebraMap R S) (↑(∏ j in Finset.erase s i, (sec M (f j)).snd) * (sec M (f i)).fst) =
    ↑(∏ i in s, (sec M (f i)).snd) • f i
[PROOFSTEP]
rw [RingHom.map_mul, sec_spec', ← mul_assoc, ← (algebraMap R S).map_mul, ← Algebra.smul_def]
[GOAL]
case refine'_2
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ (↑(∏ j in Finset.erase s i, (sec M (f j)).snd) * ↑(sec M (f i)).snd) • f i = ↑(∏ i in s, (sec M (f i)).snd) • f i
[PROOFSTEP]
congr 2
[GOAL]
case refine'_2.e_a
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ ↑(∏ j in Finset.erase s i, (sec M (f j)).snd) * ↑(sec M (f i)).snd = ↑(∏ i in s, (sec M (f i)).snd)
[PROOFSTEP]
refine' _root_.trans _ ((Submonoid.subtype M).map_prod _ _).symm
[GOAL]
case refine'_2.e_a
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ ↑(∏ j in Finset.erase s i, (sec M (f j)).snd) * ↑(sec M (f i)).snd =
    ∏ x in s, ↑(Submonoid.subtype M) (sec M (f x)).snd
[PROOFSTEP]
rw [mul_comm, Submonoid.coe_finset_prod,
  -- Porting note: explicitly supplied `f`←
  Finset.prod_insert (f := fun i => ((sec M (f i)).snd : R)) (s.not_mem_erase i), Finset.insert_erase hi]
[GOAL]
case refine'_2.e_a
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ ∏ x in s, ↑(sec M (f x)).snd = ∏ x in s, ↑(Submonoid.subtype M) (sec M (f x)).snd
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
ι : Type u_4
inst✝ : Finite ι
f : ι → S
⊢ ∃ b, ∀ (i : ι), IsInteger R (↑b • f i)
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
ι : Type u_4
inst✝ : Finite ι
f : ι → S
val✝ : Fintype ι
⊢ ∃ b, ∀ (i : ι), IsInteger R (↑b • f i)
[PROOFSTEP]
obtain ⟨b, hb⟩ := exist_integer_multiples M Finset.univ f
[GOAL]
case intro.intro
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
ι : Type u_4
inst✝ : Finite ι
f : ι → S
val✝ : Fintype ι
b : { x // x ∈ M }
hb : ∀ (i : ι), i ∈ Finset.univ → IsInteger R (↑b • f i)
⊢ ∃ b, ∀ (i : ι), IsInteger R (↑b • f i)
[PROOFSTEP]
exact ⟨b, fun i => hb i (Finset.mem_univ _)⟩
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
⊢ ↑(algebraMap R S) '' ↑(finsetIntegerMultiple M s) = commonDenomOfFinset M s • ↑s
[PROOFSTEP]
delta finsetIntegerMultiple commonDenom
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
⊢ ↑(algebraMap R S) '' ↑(Finset.image (fun t => integerMultiple M s id t) (Finset.attach s)) =
    commonDenomOfFinset M s • ↑s
[PROOFSTEP]
rw [Finset.coe_image]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
⊢ ↑(algebraMap R S) '' ((fun t => integerMultiple M s id t) '' ↑(Finset.attach s)) = commonDenomOfFinset M s • ↑s
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
x✝ : S
⊢ x✝ ∈ ↑(algebraMap R S) '' ((fun t => integerMultiple M s id t) '' ↑(Finset.attach s)) ↔
    x✝ ∈ commonDenomOfFinset M s • ↑s
[PROOFSTEP]
constructor
[GOAL]
case h.mp
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
x✝ : S
⊢ x✝ ∈ ↑(algebraMap R S) '' ((fun t => integerMultiple M s id t) '' ↑(Finset.attach s)) →
    x✝ ∈ commonDenomOfFinset M s • ↑s
[PROOFSTEP]
rintro ⟨_, ⟨x, -, rfl⟩, rfl⟩
[GOAL]
case h.mp.intro.intro.intro.intro
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
x : { x // x ∈ s }
⊢ ↑(algebraMap R S) ((fun t => integerMultiple M s id t) x) ∈ commonDenomOfFinset M s • ↑s
[PROOFSTEP]
rw [map_integerMultiple]
[GOAL]
case h.mp.intro.intro.intro.intro
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
x : { x // x ∈ s }
⊢ commonDenom M s id • id ↑x ∈ commonDenomOfFinset M s • ↑s
[PROOFSTEP]
exact Set.mem_image_of_mem _ x.prop
[GOAL]
case h.mpr
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
x✝ : S
⊢ x✝ ∈ commonDenomOfFinset M s • ↑s →
    x✝ ∈ ↑(algebraMap R S) '' ((fun t => integerMultiple M s id t) '' ↑(Finset.attach s))
[PROOFSTEP]
rintro ⟨x, hx, rfl⟩
[GOAL]
case h.mpr.intro.intro
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
x : S
hx : x ∈ ↑s
⊢ (fun x => ↑(Submonoid.subtype M) (commonDenomOfFinset M s) • x) x ∈
    ↑(algebraMap R S) '' ((fun t => integerMultiple M s id t) '' ↑(Finset.attach s))
[PROOFSTEP]
exact ⟨_, ⟨⟨x, hx⟩, s.mem_attach _, rfl⟩, map_integerMultiple M s id _⟩


[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ T R (n + 2) = 2 * X * T R (n + 1) - T R n
[PROOFSTEP]
rw [T]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ T R 2 = 2 * X ^ 2 - 1
[PROOFSTEP]
simp only [T, sub_left_inj, sq, mul_assoc]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h : 2 ≤ n
⊢ T R n = 2 * X * T R (n - 1) - T R (n - 2)
[PROOFSTEP]
obtain ⟨n, rfl⟩ := Nat.exists_eq_add_of_le h
[GOAL]
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h : 2 ≤ 2 + n
⊢ T R (2 + n) = 2 * X * T R (2 + n - 1) - T R (2 + n - 2)
[PROOFSTEP]
rw [add_comm]
[GOAL]
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h : 2 ≤ 2 + n
⊢ T R (n + 2) = 2 * X * T R (n + 2 - 1) - T R (n + 2 - 2)
[PROOFSTEP]
exact T_add_two R n
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ U R (n + 2) = 2 * X * U R (n + 1) - U R n
[PROOFSTEP]
rw [U]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ U R 2 = 4 * X ^ 2 - 1
[PROOFSTEP]
simp only [U]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ 2 * X * (2 * X) - 1 = 4 * X ^ 2 - 1
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h : 2 ≤ n
⊢ U R n = 2 * X * U R (n - 1) - U R (n - 2)
[PROOFSTEP]
obtain ⟨n, rfl⟩ := Nat.exists_eq_add_of_le h
[GOAL]
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h : 2 ≤ 2 + n
⊢ U R (2 + n) = 2 * X * U R (2 + n - 1) - U R (2 + n - 2)
[PROOFSTEP]
rw [add_comm]
[GOAL]
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h : 2 ≤ 2 + n
⊢ U R (n + 2) = 2 * X * U R (n + 2 - 1) - U R (n + 2 - 2)
[PROOFSTEP]
exact U_add_two R n
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ U R (0 + 1) = X * U R 0 + T R (0 + 1)
[PROOFSTEP]
simp only [T, U, two_mul, mul_one]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ U R (1 + 1) = X * U R 1 + T R (1 + 1)
[PROOFSTEP]
simp only [T, U]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ 2 * X * (2 * X) - 1 = X * (2 * X) + (2 * X * X - 1)
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ U R (n + 2 + 1) = 2 * X * (X * U R (n + 1) + T R (n + 2)) - (X * U R n + T R (n + 1))
[PROOFSTEP]
rw [U_add_two, U_eq_X_mul_U_add_T n, U_eq_X_mul_U_add_T (n + 1), U_eq_X_mul_U_add_T n]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ 2 * X * (X * U R (n + 1) + T R (n + 2)) - (X * U R n + T R (n + 1)) =
    X * (2 * X * U R (n + 1) - U R n) + (2 * X * T R (n + 2) - T R (n + 1))
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ X * (2 * X * U R (n + 1) - U R n) + (2 * X * T R (n + 2) - T R (n + 1)) = X * U R (n + 2) + T R (n + 2 + 1)
[PROOFSTEP]
simp only [U_add_two, T_add_two]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ T R (n + 1) = U R (n + 1) - X * U R n
[PROOFSTEP]
rw [U_eq_X_mul_U_add_T, add_comm (X * U R n), add_sub_cancel]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ T R (0 + 2) = X * T R (0 + 1) - (1 - X ^ 2) * U R 0
[PROOFSTEP]
simp only [T, U]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ 2 * X * X - 1 = X * X - (1 - X ^ 2) * 1
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ T R (1 + 2) = X * T R (1 + 1) - (1 - X ^ 2) * U R 1
[PROOFSTEP]
simp only [T, U]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ 2 * X * (2 * X * X - 1) - X = X * (2 * X * X - 1) - (1 - X ^ 2) * (2 * X)
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ 2 * X * T R (n + 2 + 1) - T R (n + 2) =
    2 * X * (X * T R (n + 2) - (1 - X ^ 2) * U R (n + 1)) - (X * T R (n + 1) - (1 - X ^ 2) * U R n)
[PROOFSTEP]
simp only [T_eq_X_mul_T_sub_pol_U]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ 2 * X * (X * T R (n + 2) - (1 - X ^ 2) * U R (n + 1)) - (X * T R (n + 1) - (1 - X ^ 2) * U R n) =
    X * (2 * X * T R (n + 2) - T R (n + 1)) - (1 - X ^ 2) * (2 * X * U R (n + 1) - U R n)
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ X * (2 * X * T R (n + 2) - T R (n + 1)) - (1 - X ^ 2) * (2 * X * U R (n + 1) - U R n) =
    X * T R (n + 2 + 1) - (1 - X ^ 2) * U R (n + 2)
[PROOFSTEP]
rw [T_add_two _ (n + 1), U_add_two]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ (1 - X ^ 2) * U R n = X * T R (n + 1) - T R (n + 2)
[PROOFSTEP]
rw [T_eq_X_mul_T_sub_pol_U, ← sub_add, sub_self, zero_add]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ map f (T R 0) = T S 0
[PROOFSTEP]
simp only [T_zero, Polynomial.map_one]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ map f (T R 1) = T S 1
[PROOFSTEP]
simp only [T_one, map_X]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
n : ℕ
⊢ map f (T R (n + 2)) = T S (n + 2)
[PROOFSTEP]
simp only [T_add_two, Polynomial.map_mul, Polynomial.map_sub, map_X, Polynomial.map_add, Polynomial.map_one,
  Polynomial.map_ofNat, map_T f (n + 1), map_T f n]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ map f (U R 0) = U S 0
[PROOFSTEP]
simp only [U_zero, Polynomial.map_one]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ map f (U R 1) = U S 1
[PROOFSTEP]
simp [U_one, map_X, Polynomial.map_mul, Polynomial.map_add, Polynomial.map_one]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
n : ℕ
⊢ map f (U R (n + 2)) = U S (n + 2)
[PROOFSTEP]
simp only [U_add_two, Polynomial.map_mul, Polynomial.map_sub, map_X, Polynomial.map_add, Polynomial.map_one,
  map_U f (n + 1), map_U f n]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
n : ℕ
⊢ map f 2 * X * U S (n + 1) - U S n = 2 * X * U S (n + 1) - U S n
[PROOFSTEP]
norm_num
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ↑derivative (T R (0 + 1)) = (↑0 + 1) * U R 0
[PROOFSTEP]
simp only [T_one, U_zero, derivative_X, Nat.cast_zero, zero_add, mul_one]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ↑derivative (T R (1 + 1)) = (↑1 + 1) * U R 1
[PROOFSTEP]
simp [T_two, U_one, derivative_sub, derivative_one, derivative_mul, derivative_X_pow, add_mul]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ ↑derivative (T R (n + 2 + 1)) = 2 * T R (n + 2) + 2 * X * ↑derivative (T R (n + 1 + 1)) - ↑derivative (T R (n + 1))
[PROOFSTEP]
rw [T_add_two _ (n + 1), derivative_sub, derivative_mul, derivative_mul, derivative_X, derivative_ofNat]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ (0 * X + 2 * 1) * T R (n + 1 + 1) + 2 * X * ↑derivative (T R (n + 1 + 1)) - ↑derivative (T R (n + 1)) =
    2 * T R (n + 2) + 2 * X * ↑derivative (T R (n + 1 + 1)) - ↑derivative (T R (n + 1))
[PROOFSTEP]
ring_nf
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ 2 * T R (n + 2) + 2 * X * ↑derivative (T R (n + 1 + 1)) - ↑derivative (T R (n + 1)) =
    2 * (U R (n + 1 + 1) - X * U R (n + 1)) + 2 * X * ((↑n + 1 + 1) * U R (n + 1)) - (↑n + 1) * U R n
[PROOFSTEP]
rw_mod_cast [T_derivative_eq_U (n + 1), T_derivative_eq_U n, T_eq_U_sub_X_mul_U _ (n + 1)]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ 2 * (U R (n + 1 + 1) - X * U R (n + 1)) + 2 * X * ((↑n + 1 + 1) * U R (n + 1)) - (↑n + 1) * U R n =
    (↑n + 1) * (2 * X * U R (n + 1) - U R n) + 2 * U R (n + 2)
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ (↑n + 1) * (2 * X * U R (n + 1) - U R n) + 2 * U R (n + 2) = (↑n + 1) * U R (n + 2) + 2 * U R (n + 2)
[PROOFSTEP]
rw [U_add_two]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ (↑n + 1) * U R (n + 2) + 2 * U R (n + 2) = (↑n + 2 + 1) * U R (n + 2)
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ (↑n + 2 + 1) * U R (n + 2) = (↑(n + 2) + 1) * U R (n + 2)
[PROOFSTEP]
norm_cast
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ (1 - X ^ 2) * ↑derivative (T R (n + 1)) = (1 - X ^ 2) * ((↑n + 1) * U R n)
[PROOFSTEP]
rw [T_derivative_eq_U]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ (1 - X ^ 2) * ((↑n + 1) * U R n) = (↑n + 1) * ((1 - X ^ 2) * U R n)
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ (↑n + 1) * ((1 - X ^ 2) * U R n) = (↑n + 1) * (X * T R (n + 1) - (2 * X * T R (n + 1) - T R n))
[PROOFSTEP]
rw [one_sub_X_sq_mul_U_eq_pol_in_T, T_add_two]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ (↑n + 1) * (X * T R (n + 1) - (2 * X * T R (n + 1) - T R n)) = (↑n + 1) * (T R n - X * T R (n + 1))
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ (↑n + 1) * T R (n + 1) = X * U R n - (1 - X ^ 2) * ↑derivative (U R n)
[PROOFSTEP]
have h :
  derivative (T R (n + 2)) =
    U R (n + 1) - X * U R n + X * derivative (T R (n + 1)) + 2 * X * U R n - (1 - X ^ 2) * derivative (U R n) :=
  by
  conv_lhs => rw [T_eq_X_mul_T_sub_pol_U]
  simp only [derivative_sub, derivative_mul, derivative_X, derivative_one, derivative_X_pow, one_mul, T_derivative_eq_U]
  rw [T_eq_U_sub_X_mul_U, C_eq_nat_cast]
  ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ ↑derivative (T R (n + 2)) =
    U R (n + 1) - X * U R n + X * ↑derivative (T R (n + 1)) + 2 * X * U R n - (1 - X ^ 2) * ↑derivative (U R n)
[PROOFSTEP]
conv_lhs => rw [T_eq_X_mul_T_sub_pol_U]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
| ↑derivative (T R (n + 2))
[PROOFSTEP]
rw [T_eq_X_mul_T_sub_pol_U]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
| ↑derivative (T R (n + 2))
[PROOFSTEP]
rw [T_eq_X_mul_T_sub_pol_U]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
| ↑derivative (T R (n + 2))
[PROOFSTEP]
rw [T_eq_X_mul_T_sub_pol_U]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ ↑derivative (X * T R (n + 1) - (1 - X ^ 2) * U R n) =
    U R (n + 1) - X * U R n + X * ↑derivative (T R (n + 1)) + 2 * X * U R n - (1 - X ^ 2) * ↑derivative (U R n)
[PROOFSTEP]
simp only [derivative_sub, derivative_mul, derivative_X, derivative_one, derivative_X_pow, one_mul, T_derivative_eq_U]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ T R (n + 1) + X * ((↑n + 1) * U R n) - ((0 - ↑C ↑2 * X ^ (2 - 1)) * U R n + (1 - X ^ 2) * ↑derivative (U R n)) =
    U R (n + 1) - X * U R n + X * ((↑n + 1) * U R n) + 2 * X * U R n - (1 - X ^ 2) * ↑derivative (U R n)
[PROOFSTEP]
rw [T_eq_U_sub_X_mul_U, C_eq_nat_cast]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ U R (n + 1) - X * U R n + X * ((↑n + 1) * U R n) -
      ((0 - ↑2 * X ^ (2 - 1)) * U R n + (1 - X ^ 2) * ↑derivative (U R n)) =
    U R (n + 1) - X * U R n + X * ((↑n + 1) * U R n) + 2 * X * U R n - (1 - X ^ 2) * ↑derivative (U R n)
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h :
  ↑derivative (T R (n + 2)) =
    U R (n + 1) - X * U R n + X * ↑derivative (T R (n + 1)) + 2 * X * U R n - (1 - X ^ 2) * ↑derivative (U R n)
⊢ (↑n + 1) * T R (n + 1) = X * U R n - (1 - X ^ 2) * ↑derivative (U R n)
[PROOFSTEP]
calc
  ((n : R[X]) + 1) * T R (n + 1) =
      ((n : R[X]) + 1 + 1) * (X * U R n + T R (n + 1)) - X * ((n + 1 : R[X]) * U R n) - (X * U R n + T R (n + 1)) :=
    by ring
  _ = derivative (T R (n + 2)) - X * derivative (T R (n + 1)) - U R (n + 1) := by
    rw [← U_eq_X_mul_U_add_T, ← T_derivative_eq_U, ← Nat.cast_one, ← Nat.cast_add, Nat.cast_one, ←
      T_derivative_eq_U (n + 1)]
  _ =
      U R (n + 1) - X * U R n + X * derivative (T R (n + 1)) + 2 * X * U R n - (1 - X ^ 2) * derivative (U R n) -
          X * derivative (T R (n + 1)) -
        U R (n + 1) :=
    by rw [h]
  _ = X * U R n - (1 - X ^ 2) * derivative (U R n) := by ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h :
  ↑derivative (T R (n + 2)) =
    U R (n + 1) - X * U R n + X * ↑derivative (T R (n + 1)) + 2 * X * U R n - (1 - X ^ 2) * ↑derivative (U R n)
⊢ (↑n + 1) * T R (n + 1) = (↑n + 1 + 1) * (X * U R n + T R (n + 1)) - X * ((↑n + 1) * U R n) - (X * U R n + T R (n + 1))
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h :
  ↑derivative (T R (n + 2)) =
    U R (n + 1) - X * U R n + X * ↑derivative (T R (n + 1)) + 2 * X * U R n - (1 - X ^ 2) * ↑derivative (U R n)
⊢ (↑n + 1 + 1) * (X * U R n + T R (n + 1)) - X * ((↑n + 1) * U R n) - (X * U R n + T R (n + 1)) =
    ↑derivative (T R (n + 2)) - X * ↑derivative (T R (n + 1)) - U R (n + 1)
[PROOFSTEP]
rw [← U_eq_X_mul_U_add_T, ← T_derivative_eq_U, ← Nat.cast_one, ← Nat.cast_add, Nat.cast_one, ←
  T_derivative_eq_U (n + 1)]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h :
  ↑derivative (T R (n + 2)) =
    U R (n + 1) - X * U R n + X * ↑derivative (T R (n + 1)) + 2 * X * U R n - (1 - X ^ 2) * ↑derivative (U R n)
⊢ ↑derivative (T R (n + 2)) - X * ↑derivative (T R (n + 1)) - U R (n + 1) =
    U R (n + 1) - X * U R n + X * ↑derivative (T R (n + 1)) + 2 * X * U R n - (1 - X ^ 2) * ↑derivative (U R n) -
        X * ↑derivative (T R (n + 1)) -
      U R (n + 1)
[PROOFSTEP]
rw [h]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
h :
  ↑derivative (T R (n + 2)) =
    U R (n + 1) - X * U R n + X * ↑derivative (T R (n + 1)) + 2 * X * U R n - (1 - X ^ 2) * ↑derivative (U R n)
⊢ U R (n + 1) - X * U R n + X * ↑derivative (T R (n + 1)) + 2 * X * U R n - (1 - X ^ 2) * ↑derivative (U R n) -
        X * ↑derivative (T R (n + 1)) -
      U R (n + 1) =
    X * U R n - (1 - X ^ 2) * ↑derivative (U R n)
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (k : ℕ), 2 * T R 0 * T R (0 + k) = T R (2 * 0 + k) + T R k
[PROOFSTEP]
simp [two_mul, add_mul]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (k : ℕ), 2 * T R 1 * T R (1 + k) = T R (2 * 1 + k) + T R k
[PROOFSTEP]
simp [add_comm]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m : ℕ
⊢ ∀ (k : ℕ), 2 * T R (m + 2) * T R (m + 2 + k) = T R (2 * (m + 2) + k) + T R k
[PROOFSTEP]
intro k
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
⊢ 2 * T R (m + 2) * T R (m + 2 + k) = T R (2 * (m + 2) + k) + T R k
[PROOFSTEP]
suffices 2 * T R (m + 2) * T R (m + k + 2) = T R (2 * m + k + 4) + T R k
  by
  have h_nat₁ : 2 * (m + 2) + k = 2 * m + k + 4 := by ring
  have h_nat₂ : m + 2 + k = m + k + 2 := by ring
  simpa [h_nat₁, h_nat₂] using this
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
this : 2 * T R (m + 2) * T R (m + k + 2) = T R (2 * m + k + 4) + T R k
⊢ 2 * T R (m + 2) * T R (m + 2 + k) = T R (2 * (m + 2) + k) + T R k
[PROOFSTEP]
have h_nat₁ : 2 * (m + 2) + k = 2 * m + k + 4 := by ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
this : 2 * T R (m + 2) * T R (m + k + 2) = T R (2 * m + k + 4) + T R k
⊢ 2 * (m + 2) + k = 2 * m + k + 4
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
this : 2 * T R (m + 2) * T R (m + k + 2) = T R (2 * m + k + 4) + T R k
h_nat₁ : 2 * (m + 2) + k = 2 * m + k + 4
⊢ 2 * T R (m + 2) * T R (m + 2 + k) = T R (2 * (m + 2) + k) + T R k
[PROOFSTEP]
have h_nat₂ : m + 2 + k = m + k + 2 := by ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
this : 2 * T R (m + 2) * T R (m + k + 2) = T R (2 * m + k + 4) + T R k
h_nat₁ : 2 * (m + 2) + k = 2 * m + k + 4
⊢ m + 2 + k = m + k + 2
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
this : 2 * T R (m + 2) * T R (m + k + 2) = T R (2 * m + k + 4) + T R k
h_nat₁ : 2 * (m + 2) + k = 2 * m + k + 4
h_nat₂ : m + 2 + k = m + k + 2
⊢ 2 * T R (m + 2) * T R (m + 2 + k) = T R (2 * (m + 2) + k) + T R k
[PROOFSTEP]
simpa [h_nat₁, h_nat₂] using this
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
⊢ 2 * T R (m + 2) * T R (m + k + 2) = T R (2 * m + k + 4) + T R k
[PROOFSTEP]
have H₁ : 2 * T R (m + 1) * T R (m + k + 2) = T R (2 * m + k + 3) + T R (k + 1) :=
  by
  have h_nat₁ : m + 1 + (k + 1) = m + k + 2 := by ring
  have h_nat₂ : 2 * (m + 1) + (k + 1) = 2 * m + k + 3 := by ring
  simpa [h_nat₁, h_nat₂] using
    mul_T (m + 1)
      (k + 1)
        -- clean up the `T` nat indices in the inductive hypothesis applied to `m` and `k + 2`
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
⊢ 2 * T R (m + 1) * T R (m + k + 2) = T R (2 * m + k + 3) + T R (k + 1)
[PROOFSTEP]
have h_nat₁ : m + 1 + (k + 1) = m + k + 2 := by ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
⊢ m + 1 + (k + 1) = m + k + 2
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
h_nat₁ : m + 1 + (k + 1) = m + k + 2
⊢ 2 * T R (m + 1) * T R (m + k + 2) = T R (2 * m + k + 3) + T R (k + 1)
[PROOFSTEP]
have h_nat₂ : 2 * (m + 1) + (k + 1) = 2 * m + k + 3 := by ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
h_nat₁ : m + 1 + (k + 1) = m + k + 2
⊢ 2 * (m + 1) + (k + 1) = 2 * m + k + 3
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
h_nat₁ : m + 1 + (k + 1) = m + k + 2
h_nat₂ : 2 * (m + 1) + (k + 1) = 2 * m + k + 3
⊢ 2 * T R (m + 1) * T R (m + k + 2) = T R (2 * m + k + 3) + T R (k + 1)
[PROOFSTEP]
simpa [h_nat₁, h_nat₂] using
  mul_T (m + 1)
    (k + 1)
      -- clean up the `T` nat indices in the inductive hypothesis applied to `m` and `k + 2`
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
H₁ : 2 * T R (m + 1) * T R (m + k + 2) = T R (2 * m + k + 3) + T R (k + 1)
⊢ 2 * T R (m + 2) * T R (m + k + 2) = T R (2 * m + k + 4) + T R k
[PROOFSTEP]
have H₂ : 2 * T R m * T R (m + k + 2) = T R (2 * m + k + 2) + T R (k + 2) :=
  by
  have h_nat₁ : 2 * m + (k + 2) = 2 * m + k + 2 := by simp [add_assoc]
  have h_nat₂ : m + (k + 2) = m + k + 2 := by simp [add_assoc]
  simpa [h_nat₁, h_nat₂] using
    mul_T m
      (k + 2)
        -- state the `T` recurrence relation for a few useful indices
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
H₁ : 2 * T R (m + 1) * T R (m + k + 2) = T R (2 * m + k + 3) + T R (k + 1)
⊢ 2 * T R m * T R (m + k + 2) = T R (2 * m + k + 2) + T R (k + 2)
[PROOFSTEP]
have h_nat₁ : 2 * m + (k + 2) = 2 * m + k + 2 := by simp [add_assoc]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
H₁ : 2 * T R (m + 1) * T R (m + k + 2) = T R (2 * m + k + 3) + T R (k + 1)
⊢ 2 * m + (k + 2) = 2 * m + k + 2
[PROOFSTEP]
simp [add_assoc]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
H₁ : 2 * T R (m + 1) * T R (m + k + 2) = T R (2 * m + k + 3) + T R (k + 1)
h_nat₁ : 2 * m + (k + 2) = 2 * m + k + 2
⊢ 2 * T R m * T R (m + k + 2) = T R (2 * m + k + 2) + T R (k + 2)
[PROOFSTEP]
have h_nat₂ : m + (k + 2) = m + k + 2 := by simp [add_assoc]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
H₁ : 2 * T R (m + 1) * T R (m + k + 2) = T R (2 * m + k + 3) + T R (k + 1)
h_nat₁ : 2 * m + (k + 2) = 2 * m + k + 2
⊢ m + (k + 2) = m + k + 2
[PROOFSTEP]
simp [add_assoc]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
H₁ : 2 * T R (m + 1) * T R (m + k + 2) = T R (2 * m + k + 3) + T R (k + 1)
h_nat₁ : 2 * m + (k + 2) = 2 * m + k + 2
h_nat₂ : m + (k + 2) = m + k + 2
⊢ 2 * T R m * T R (m + k + 2) = T R (2 * m + k + 2) + T R (k + 2)
[PROOFSTEP]
simpa [h_nat₁, h_nat₂] using
  mul_T m
    (k + 2)
      -- state the `T` recurrence relation for a few useful indices
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
H₁ : 2 * T R (m + 1) * T R (m + k + 2) = T R (2 * m + k + 3) + T R (k + 1)
H₂ : 2 * T R m * T R (m + k + 2) = T R (2 * m + k + 2) + T R (k + 2)
⊢ 2 * T R (m + 2) * T R (m + k + 2) = T R (2 * m + k + 4) + T R k
[PROOFSTEP]
have h₁ := T_add_two R m
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
H₁ : 2 * T R (m + 1) * T R (m + k + 2) = T R (2 * m + k + 3) + T R (k + 1)
H₂ : 2 * T R m * T R (m + k + 2) = T R (2 * m + k + 2) + T R (k + 2)
h₁ : T R (m + 2) = 2 * X * T R (m + 1) - T R m
⊢ 2 * T R (m + 2) * T R (m + k + 2) = T R (2 * m + k + 4) + T R k
[PROOFSTEP]
have h₂ : T R (2 * m + k + 4) = 2 * X * T R (2 * m + k + 3) - T R (2 * m + k + 2) := T_add_two R (2 * m + k + 2)
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
H₁ : 2 * T R (m + 1) * T R (m + k + 2) = T R (2 * m + k + 3) + T R (k + 1)
H₂ : 2 * T R m * T R (m + k + 2) = T R (2 * m + k + 2) + T R (k + 2)
h₁ : T R (m + 2) = 2 * X * T R (m + 1) - T R m
h₂ : T R (2 * m + k + 4) = 2 * X * T R (2 * m + k + 3) - T R (2 * m + k + 2)
⊢ 2 * T R (m + 2) * T R (m + k + 2) = T R (2 * m + k + 4) + T R k
[PROOFSTEP]
have h₃ := T_add_two R k
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m k : ℕ
H₁ : 2 * T R (m + 1) * T R (m + k + 2) = T R (2 * m + k + 3) + T R (k + 1)
H₂ : 2 * T R m * T R (m + k + 2) = T R (2 * m + k + 2) + T R (k + 2)
h₁ : T R (m + 2) = 2 * X * T R (m + 1) - T R m
h₂ : T R (2 * m + k + 4) = 2 * X * T R (2 * m + k + 3) - T R (2 * m + k + 2)
h₃ : T R (k + 2) = 2 * X * T R (k + 1) - T R k
⊢ 2 * T R (m + 2) * T R (m + k + 2) = T R (2 * m + k + 4) + T R k
[PROOFSTEP]
linear_combination 2 * T R (m + k + 2) * h₁ + 2 * (X : R[X]) * H₁ - H₂ - h₂ - h₃
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (n : ℕ), T R (0 * n) = comp (T R 0) (T R n)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (n : ℕ), T R (1 * n) = comp (T R 1) (T R n)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m : ℕ
⊢ ∀ (n : ℕ), T R ((m + 2) * n) = comp (T R (m + 2)) (T R n)
[PROOFSTEP]
intro n
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m n : ℕ
⊢ T R ((m + 2) * n) = comp (T R (m + 2)) (T R n)
[PROOFSTEP]
have : 2 * T R n * T R ((m + 1) * n) = T R ((m + 2) * n) + T R (m * n) := by
  convert mul_T R n (m * n) using 1 <;> ring_nf
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m n : ℕ
⊢ 2 * T R n * T R ((m + 1) * n) = T R ((m + 2) * n) + T R (m * n)
[PROOFSTEP]
convert mul_T R n (m * n) using 1
[GOAL]
case h.e'_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m n : ℕ
⊢ 2 * T R n * T R ((m + 1) * n) = 2 * T R n * T R (n + m * n)
[PROOFSTEP]
ring_nf
[GOAL]
case h.e'_3
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m n : ℕ
⊢ T R ((m + 2) * n) + T R (m * n) = T R (2 * n + m * n) + T R (m * n)
[PROOFSTEP]
ring_nf
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
m n : ℕ
this : 2 * T R n * T R ((m + 1) * n) = T R ((m + 2) * n) + T R (m * n)
⊢ T R ((m + 2) * n) = comp (T R (m + 2)) (T R n)
[PROOFSTEP]
simp [this, T_mul m, ← T_mul (m + 1)]