[GOAL]
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
h : degree f ≠ 0
⊢ span {f} ≠ ⊤
[PROOFSTEP]
simp_rw [Ne.def, span_singleton_eq_top, Polynomial.isUnit_iff, not_exists, not_and]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
h : degree f ≠ 0
⊢ ∀ (x : R), IsUnit x → ¬↑C x = f
[PROOFSTEP]
rintro x hx rfl
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R
hx : IsUnit x
h : degree (↑C x) ≠ 0
⊢ False
[PROOFSTEP]
exact h (degree_C hx.ne_zero)
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
f : R[X]
inst✝¹ : DistribSMul S R
inst✝ : IsScalarTower S R R
a : S
x : R
⊢ a • ↑(of f) x = ↑(of f) (a • x)
[PROOFSTEP]
rw [of, RingHom.comp_apply, RingHom.comp_apply, smul_mk, smul_C]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
f g : R[X]
⊢ f ∣ g - 0 ↔ f ∣ g
[PROOFSTEP]
rw [sub_zero]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
f : R[X]
⊢ f ∣ -f + 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
f p : R[X]
x : R
⊢ ↑(aeval (root f)) (↑C x) = ↑(mk f) (↑C x)
[PROOFSTEP]
rw [aeval_C]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
f p : R[X]
x : R
⊢ ↑(algebraMap R (AdjoinRoot f)) x = ↑(mk f) (↑C x)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
f p✝ p q : R[X]
ihp : ↑(aeval (root f)) p = ↑(mk f) p
ihq : ↑(aeval (root f)) q = ↑(mk f) q
⊢ ↑(aeval (root f)) (p + q) = ↑(mk f) (p + q)
[PROOFSTEP]
rw [AlgHom.map_add, RingHom.map_add, ihp, ihq]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
f p : R[X]
n : ℕ
x : R
x✝ : ↑(aeval (root f)) (↑C x * X ^ n) = ↑(mk f) (↑C x * X ^ n)
⊢ ↑(aeval (root f)) (↑C x * X ^ (n + 1)) = ↑(mk f) (↑C x * X ^ (n + 1))
[PROOFSTEP]
rw [AlgHom.map_mul, aeval_C, AlgHom.map_pow, aeval_X, RingHom.map_mul, mk_C, RingHom.map_pow, mk_X]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
f p : R[X]
n : ℕ
x : R
x✝ : ↑(aeval (root f)) (↑C x * X ^ n) = ↑(mk f) (↑C x * X ^ n)
⊢ ↑(algebraMap R (AdjoinRoot f)) x * root f ^ (n + 1) = ↑(of f) x * root f ^ (n + 1)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
f : R[X]
⊢ Algebra.adjoin R {root f} = ⊤
[PROOFSTEP]
refine Algebra.eq_top_iff.2 fun x => ?_
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
f : R[X]
x : AdjoinRoot f
⊢ x ∈ Algebra.adjoin R {root f}
[PROOFSTEP]
induction x using AdjoinRoot.induction_on with
| ih p => exact (Algebra.adjoin_singleton_eq_range_aeval R (root f)).symm ▸ ⟨p, aeval_eq p⟩
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
f : R[X]
x : AdjoinRoot f
⊢ x ∈ Algebra.adjoin R {root f}
[PROOFSTEP]
induction x using AdjoinRoot.induction_on with
| ih p => exact (Algebra.adjoin_singleton_eq_range_aeval R (root f)).symm ▸ ⟨p, aeval_eq p⟩
[GOAL]
case ih
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
f p : R[X]
⊢ ↑(mk f) p ∈ Algebra.adjoin R {root f}
[PROOFSTEP]

| ih p => exact (Algebra.adjoin_singleton_eq_range_aeval R (root f)).symm ▸ ⟨p, aeval_eq p⟩
[GOAL]
case ih
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
f p : R[X]
⊢ ↑(mk f) p ∈ Algebra.adjoin R {root f}
[PROOFSTEP]
exact (Algebra.adjoin_singleton_eq_range_aeval R (root f)).symm ▸ ⟨p, aeval_eq p⟩
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
f✝ f : R[X]
⊢ eval₂ (of f) (root f) f = 0
[PROOFSTEP]
rw [← algebraMap_eq, ← aeval_def, aeval_eq, mk_self]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
f✝ f : R[X]
⊢ IsRoot (Polynomial.map (of f) f) (root f)
[PROOFSTEP]
rw [IsRoot, eval_map, eval₂_root]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : degree f ≠ 0
⊢ Function.Injective ↑(of f)
[PROOFSTEP]
rw [injective_iff_map_eq_zero]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : degree f ≠ 0
⊢ ∀ (a : R), ↑(of f) a = 0 → a = 0
[PROOFSTEP]
intro p hp
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : degree f ≠ 0
p : R
hp : ↑(of f) p = 0
⊢ p = 0
[PROOFSTEP]
rw [AdjoinRoot.of, RingHom.comp_apply, AdjoinRoot.mk_eq_zero] at hp
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : degree f ≠ 0
p : R
hp : f ∣ ↑C p
⊢ p = 0
[PROOFSTEP]
by_cases h : f = 0
[GOAL]
case pos
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : degree f ≠ 0
p : R
hp : f ∣ ↑C p
h : f = 0
⊢ p = 0
[PROOFSTEP]
exact C_eq_zero.mp (eq_zero_of_zero_dvd (by rwa [h] at hp ))
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : degree f ≠ 0
p : R
hp : f ∣ ↑C p
h : f = 0
⊢ 0 ∣ ↑C p
[PROOFSTEP]
rwa [h] at hp
[GOAL]
case neg
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : degree f ≠ 0
p : R
hp : f ∣ ↑C p
h : ¬f = 0
⊢ p = 0
[PROOFSTEP]
contrapose! hf with h_contra
[GOAL]
case neg
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
p : R
hp : f ∣ ↑C p
h : ¬f = 0
h_contra : p ≠ 0
⊢ degree f = 0
[PROOFSTEP]
rw [← degree_C h_contra]
[GOAL]
case neg
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
p : R
hp : f ∣ ↑C p
h : ¬f = 0
h_contra : p ≠ 0
⊢ degree f = degree (↑C p)
[PROOFSTEP]
apply le_antisymm (degree_le_of_dvd hp (by rwa [Ne.def, C_eq_zero])) _
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
p : R
hp : f ∣ ↑C p
h : ¬f = 0
h_contra : p ≠ 0
⊢ ↑C p ≠ 0
[PROOFSTEP]
rwa [Ne.def, C_eq_zero]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
p : R
hp : f ∣ ↑C p
h : ¬f = 0
h_contra : p ≠ 0
⊢ degree (↑C p) ≤ degree f
[PROOFSTEP]
rwa [degree_C h_contra, zero_le_degree_iff]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : CommRing S
i : R →+* S
x : S
h : eval₂ i x f = 0
⊢ AdjoinRoot f →+* S
[PROOFSTEP]
apply Ideal.Quotient.lift _ (eval₂RingHom i x)
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : CommRing S
i : R →+* S
x : S
h : eval₂ i x f = 0
⊢ ∀ (a : R[X]), a ∈ span {f} → ↑(eval₂RingHom i x) a = 0
[PROOFSTEP]
intro g H
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : CommRing S
i : R →+* S
x : S
h : eval₂ i x f = 0
g : R[X]
H : g ∈ span {f}
⊢ ↑(eval₂RingHom i x) g = 0
[PROOFSTEP]
rcases mem_span_singleton.1 H with ⟨y, hy⟩
[GOAL]
case intro
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : CommRing S
i : R →+* S
x : S
h : eval₂ i x f = 0
g : R[X]
H : g ∈ span {f}
y : R[X]
hy : g = f * y
⊢ ↑(eval₂RingHom i x) g = 0
[PROOFSTEP]
rw [hy, RingHom.map_mul, coe_eval₂RingHom, h, zero_mul]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : CommRing S
i : R →+* S
a : S
h : eval₂ i a f = 0
⊢ ↑(lift i a h) (root f) = a
[PROOFSTEP]
rw [root, lift_mk, eval₂_X]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
f : R[X]
inst✝ : CommRing S
i : R →+* S
a : S
h : eval₂ i a f = 0
x : R
⊢ ↑(lift i a h) (↑(of f) x) = ↑i x
[PROOFSTEP]
rw [← mk_C x, lift_mk, eval₂_C]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
f : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h : eval₂ i a f = 0
inst✝ : Algebra R S
ϕ : AdjoinRoot f →ₐ[R] S
⊢ ↑(aeval (↑ϕ (root f))) f = 0
[PROOFSTEP]
have h : ϕ.toRingHom.comp (of f) = algebraMap R S := RingHom.ext_iff.mpr ϕ.commutes
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
f : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f = 0
inst✝ : Algebra R S
ϕ : AdjoinRoot f →ₐ[R] S
h : RingHom.comp (↑ϕ) (of f) = algebraMap R S
⊢ ↑(aeval (↑ϕ (root f))) f = 0
[PROOFSTEP]
rw [aeval_def, ← h, ← RingHom.map_zero ϕ.toRingHom, ← eval₂_root f, hom_eval₂]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
f : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f = 0
inst✝ : Algebra R S
ϕ : AdjoinRoot f →ₐ[R] S
h : RingHom.comp (↑ϕ) (of f) = algebraMap R S
⊢ eval₂ (RingHom.comp (↑ϕ) (of f)) (↑ϕ (root f)) f = eval₂ (RingHom.comp (↑ϕ) (of f)) (↑↑ϕ (root f)) f
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
f✝ : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h : eval₂ i a f✝ = 0
inst✝ : Algebra R S
f : R[X]
ϕ : AdjoinRoot f →ₐ[R] S
⊢ liftHom f (↑ϕ (root f)) (_ : ↑(aeval (↑ϕ (root f))) f = 0) = ϕ
[PROOFSTEP]
suffices ϕ.equalizer (liftHom f (ϕ (root f)) (aeval_algHom_eq_zero f ϕ)) = ⊤ by
  exact (AlgHom.ext fun x => (SetLike.ext_iff.mp this x).mpr Algebra.mem_top).symm
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
f✝ : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h : eval₂ i a f✝ = 0
inst✝ : Algebra R S
f : R[X]
ϕ : AdjoinRoot f →ₐ[R] S
this : AlgHom.equalizer ϕ (liftHom f (↑ϕ (root f)) (_ : ↑(aeval (↑ϕ (root f))) f = 0)) = ⊤
⊢ liftHom f (↑ϕ (root f)) (_ : ↑(aeval (↑ϕ (root f))) f = 0) = ϕ
[PROOFSTEP]
exact (AlgHom.ext fun x => (SetLike.ext_iff.mp this x).mpr Algebra.mem_top).symm
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
f✝ : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h : eval₂ i a f✝ = 0
inst✝ : Algebra R S
f : R[X]
ϕ : AdjoinRoot f →ₐ[R] S
⊢ AlgHom.equalizer ϕ (liftHom f (↑ϕ (root f)) (_ : ↑(aeval (↑ϕ (root f))) f = 0)) = ⊤
[PROOFSTEP]
rw [eq_top_iff, ← adjoinRoot_eq_top, Algebra.adjoin_le_iff, Set.singleton_subset_iff]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
f✝ : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h : eval₂ i a f✝ = 0
inst✝ : Algebra R S
f : R[X]
ϕ : AdjoinRoot f →ₐ[R] S
⊢ root f ∈ ↑(AlgHom.equalizer ϕ (liftHom f (↑ϕ (root f)) (_ : ↑(aeval (↑ϕ (root f))) f = 0)))
[PROOFSTEP]
exact (@lift_root _ _ _ _ _ _ _ (aeval_algHom_eq_zero f ϕ)).symm
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
f : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h : eval₂ i a f = 0
inst✝ : Algebra R S
hfx : ↑(aeval a) f = 0
r : R
⊢ ↑(of (↑C r * X - 1)) r * root (↑C r * X - 1) = 1
[PROOFSTEP]
convert sub_eq_zero.1 ((eval₂_sub _).symm.trans <| eval₂_root <| C r * X - 1)
[GOAL]
case h.e'_2
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
f : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h : eval₂ i a f = 0
inst✝ : Algebra R S
hfx : ↑(aeval a) f = 0
r : R
⊢ ↑(of (↑C r * X - 1)) r * root (↑C r * X - 1) = eval₂ (of (↑C r * X - 1)) (root (↑C r * X - 1)) (↑C r * X)
[PROOFSTEP]
simp only [eval₂_mul, eval₂_C, eval₂_X, eval₂_one]
[GOAL]
case h.e'_3
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
f : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h : eval₂ i a f = 0
inst✝ : Algebra R S
hfx : ↑(aeval a) f = 0
r : R
⊢ 1 = eval₂ (of (↑C r * X - 1)) (root (↑C r * X - 1)) 1
[PROOFSTEP]
simp only [eval₂_mul, eval₂_C, eval₂_X, eval₂_one]
[GOAL]
R : Type u
S✝ : Type v
K : Type w
inst✝⁴ : CommRing R
f✝ : R[X]
inst✝³ : CommRing S✝
i : R →+* S✝
a : S✝
h : eval₂ i a f✝ = 0
inst✝² : Algebra R S✝
hfx : ↑(aeval a) f✝ = 0
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
f g : AdjoinRoot (↑C r * X - 1) →ₐ[R] S
⊢ ↑(algebraMap R S) r * ↑f (root (↑C r * X - 1)) = 1
[PROOFSTEP]
rw [← f.commutes, ← f.map_mul, algebraMap_eq, root_isInv, map_one]
[GOAL]
R : Type u
S✝ : Type v
K : Type w
inst✝⁴ : CommRing R
f✝ : R[X]
inst✝³ : CommRing S✝
i : R →+* S✝
a : S✝
h : eval₂ i a f✝ = 0
inst✝² : Algebra R S✝
hfx : ↑(aeval a) f✝ = 0
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
f g : AdjoinRoot (↑C r * X - 1) →ₐ[R] S
⊢ ↑(algebraMap R S) r * ↑g (root (↑C r * X - 1)) = 1
[PROOFSTEP]
rw [← g.commutes, ← g.map_mul, algebraMap_eq, root_isInv, map_one]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝¹ : Field K
f : K[X]
inst✝ : Fact (Irreducible f)
src✝ : GroupWithZero (K[X] ⧸ span {f}) := Quotient.groupWithZero (span {f})
a : ℤ
b : ℕ
h1 : b ≠ 0
h2 : Nat.coprime (Int.natAbs a) b
⊢ ↑(Rat.mk' a b) = ↑a * (↑b)⁻¹
[PROOFSTEP]
letI : GroupWithZero (AdjoinRoot f) :=
  Ideal.Quotient.groupWithZero
    _
      -- porting note: was
            -- `rw [Rat.cast_mk' (K := ℚ), _root_.map_mul, _root_.map_intCast, map_inv₀, map_natCast]`
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝¹ : Field K
f : K[X]
inst✝ : Fact (Irreducible f)
src✝ : GroupWithZero (K[X] ⧸ span {f}) := Quotient.groupWithZero (span {f})
a : ℤ
b : ℕ
h1 : b ≠ 0
h2 : Nat.coprime (Int.natAbs a) b
this : GroupWithZero (AdjoinRoot f) := Quotient.groupWithZero (span {f})
⊢ ↑(Rat.mk' a b) = ↑a * (↑b)⁻¹
[PROOFSTEP]
convert_to ((Rat.mk' a b h1 h2 : K) : AdjoinRoot f) = ((↑a * (↑b)⁻¹ : K) : AdjoinRoot f)
[GOAL]
case h.e'_3
R : Type u
S : Type v
K : Type w
inst✝¹ : Field K
f : K[X]
inst✝ : Fact (Irreducible f)
src✝ : GroupWithZero (K[X] ⧸ span {f}) := Quotient.groupWithZero (span {f})
a : ℤ
b : ℕ
h1 : b ≠ 0
h2 : Nat.coprime (Int.natAbs a) b
this : GroupWithZero (AdjoinRoot f) := Quotient.groupWithZero (span {f})
⊢ ↑a * (↑b)⁻¹ = ↑(of f) (↑a * (↑b)⁻¹)
[PROOFSTEP]
simp only [_root_.map_mul, map_intCast, map_inv₀, map_natCast]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝¹ : Field K
f : K[X]
inst✝ : Fact (Irreducible f)
src✝ : GroupWithZero (K[X] ⧸ span {f}) := Quotient.groupWithZero (span {f})
a : ℤ
b : ℕ
h1 : b ≠ 0
h2 : Nat.coprime (Int.natAbs a) b
this : GroupWithZero (AdjoinRoot f) := Quotient.groupWithZero (span {f})
⊢ ↑(of f) ↑(Rat.mk' a b) = ↑(of f) (↑a * (↑b)⁻¹)
[PROOFSTEP]
simp only [Rat.cast_mk', _root_.map_mul, map_intCast, map_inv₀, map_natCast]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝¹ : Field K
f : K[X]
inst✝ : Fact (Irreducible f)
src✝ : GroupWithZero (K[X] ⧸ span {f}) := Quotient.groupWithZero (span {f})
a : ℚ
x : AdjoinRoot f
p : K[X]
⊢ (fun y => a • y = ↑(of f) ↑a * y) (↑(mk f) p)
[PROOFSTEP]
simp only [smul_mk, of, RingHom.comp_apply, ← (mk f).map_mul, Polynomial.rat_smul_eq_C_mul]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
g : R[X]
hg : Monic g
⊢ Function.LeftInverse ↑(mk g) ↑(modByMonicHom hg)
[PROOFSTEP]
intro f
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
g : R[X]
hg : Monic g
f : AdjoinRoot g
⊢ ↑(mk g) (↑(modByMonicHom hg) f) = f
[PROOFSTEP]
induction f using AdjoinRoot.induction_on
[GOAL]
case ih
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
g : R[X]
hg : Monic g
p✝ : R[X]
⊢ ↑(mk g) (↑(modByMonicHom hg) (↑(mk g) p✝)) = ↑(mk g) p✝
[PROOFSTEP]
rw [modByMonicHom_mk hg, mk_eq_mk, modByMonic_eq_sub_mul_div _ hg, sub_sub_cancel_left, dvd_neg]
[GOAL]
case ih
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
g : R[X]
hg : Monic g
p✝ : R[X]
⊢ g ∣ g * (p✝ /ₘ g)
[PROOFSTEP]
apply dvd_mul_right
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
g : R[X]
hg : Monic g
f₁ f₂ : AdjoinRoot g
i : Fin (natDegree g)
⊢ (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) (f₁ + f₂) i =
    ((fun f i => coeff (↑(modByMonicHom hg) f) ↑i) f₁ + (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) f₂) i
[PROOFSTEP]
simp only [(modByMonicHom hg).map_add, coeff_add, Pi.add_apply]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
g : R[X]
hg : Monic g
f₁ : R
f₂ : AdjoinRoot g
i : Fin (natDegree g)
⊢ AddHom.toFun
      { toFun := fun f i => coeff (↑(modByMonicHom hg) f) ↑i,
        map_add' :=
          (_ :
            ∀ (f₁ f₂ : AdjoinRoot g),
              (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) (f₁ + f₂) =
                (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) f₁ + (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) f₂) }
      (f₁ • f₂) i =
    (↑(RingHom.id R) f₁ •
        AddHom.toFun
          { toFun := fun f i => coeff (↑(modByMonicHom hg) f) ↑i,
            map_add' :=
              (_ :
                ∀ (f₁ f₂ : AdjoinRoot g),
                  (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) (f₁ + f₂) =
                    (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) f₁ +
                      (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) f₂) }
          f₂)
      i
[PROOFSTEP]
simp only [(modByMonicHom hg).map_smul, coeff_smul, Pi.smul_apply, RingHom.id_apply]
  -- porting note: another proof that I converted to tactic mode
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
g : R[X]
hg : Monic g
⊢ Function.LeftInverse (fun c => ↑(mk g) (∑ i : Fin (natDegree g), ↑(monomial ↑i) (c i)))
    {
          toAddHom :=
            { toFun := fun f i => coeff (↑(modByMonicHom hg) f) ↑i,
              map_add' :=
                (_ :
                  ∀ (f₁ f₂ : AdjoinRoot g),
                    (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) (f₁ + f₂) =
                      (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) f₁ +
                        (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) f₂) },
          map_smul' :=
            (_ :
              ∀ (f₁ : R) (f₂ : AdjoinRoot g),
                AddHom.toFun
                    { toFun := fun f i => coeff (↑(modByMonicHom hg) f) ↑i,
                      map_add' :=
                        (_ :
                          ∀ (f₁ f₂ : AdjoinRoot g),
                            (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) (f₁ + f₂) =
                              (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) f₁ +
                                (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) f₂) }
                    (f₁ • f₂) =
                  ↑(RingHom.id R) f₁ •
                    AddHom.toFun
                      { toFun := fun f i => coeff (↑(modByMonicHom hg) f) ↑i,
                        map_add' :=
                          (_ :
                            ∀ (f₁ f₂ : AdjoinRoot g),
                              (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) (f₁ + f₂) =
                                (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) f₁ +
                                  (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) f₂) }
                      f₂) }.toAddHom.toFun
[PROOFSTEP]
intro f
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
g : R[X]
hg : Monic g
f : AdjoinRoot g
⊢ (fun c => ↑(mk g) (∑ i : Fin (natDegree g), ↑(monomial ↑i) (c i)))
      (AddHom.toFun
        {
            toAddHom :=
              { toFun := fun f i => coeff (↑(modByMonicHom hg) f) ↑i,
                map_add' :=
                  (_ :
                    ∀ (f₁ f₂ : AdjoinRoot g),
                      (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) (f₁ + f₂) =
                        (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) f₁ +
                          (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) f₂) },
            map_smul' :=
              (_ :
                ∀ (f₁ : R) (f₂ : AdjoinRoot g),
                  AddHom.toFun
                      { toFun := fun f i => coeff (↑(modByMonicHom hg) f) ↑i,
                        map_add' :=
                          (_ :
                            ∀ (f₁ f₂ : AdjoinRoot g),
                              (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) (f₁ + f₂) =
                                (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) f₁ +
                                  (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) f₂) }
                      (f₁ • f₂) =
                    ↑(RingHom.id R) f₁ •
                      AddHom.toFun
                        { toFun := fun f i => coeff (↑(modByMonicHom hg) f) ↑i,
                          map_add' :=
                            (_ :
                              ∀ (f₁ f₂ : AdjoinRoot g),
                                (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) (f₁ + f₂) =
                                  (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) f₁ +
                                    (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) f₂) }
                        f₂) }.toAddHom
        f) =
    f
[PROOFSTEP]
induction f using AdjoinRoot.induction_on
[GOAL]
case ih
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
g : R[X]
hg : Monic g
p✝ : R[X]
⊢ (fun c => ↑(mk g) (∑ i : Fin (natDegree g), ↑(monomial ↑i) (c i)))
      (AddHom.toFun
        {
            toAddHom :=
              { toFun := fun f i => coeff (↑(modByMonicHom hg) f) ↑i,
                map_add' :=
                  (_ :
                    ∀ (f₁ f₂ : AdjoinRoot g),
                      (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) (f₁ + f₂) =
                        (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) f₁ +
                          (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) f₂) },
            map_smul' :=
              (_ :
                ∀ (f₁ : R) (f₂ : AdjoinRoot g),
                  AddHom.toFun
                      { toFun := fun f i => coeff (↑(modByMonicHom hg) f) ↑i,
                        map_add' :=
                          (_ :
                            ∀ (f₁ f₂ : AdjoinRoot g),
                              (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) (f₁ + f₂) =
                                (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) f₁ +
                                  (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) f₂) }
                      (f₁ • f₂) =
                    ↑(RingHom.id R) f₁ •
                      AddHom.toFun
                        { toFun := fun f i => coeff (↑(modByMonicHom hg) f) ↑i,
                          map_add' :=
                            (_ :
                              ∀ (f₁ f₂ : AdjoinRoot g),
                                (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) (f₁ + f₂) =
                                  (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) f₁ +
                                    (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) f₂) }
                        f₂) }.toAddHom
        (↑(mk g) p✝)) =
    ↑(mk g) p✝
[PROOFSTEP]
simp only [modByMonicHom_mk, sum_modByMonic_coeff hg degree_le_natDegree]
[GOAL]
case ih
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
g : R[X]
hg : Monic g
p✝ : R[X]
⊢ ↑(mk g) (p✝ %ₘ g) = ↑(mk g) p✝
[PROOFSTEP]
refine (mk_eq_mk.mpr ?_).symm
[GOAL]
case ih
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
g : R[X]
hg : Monic g
p✝ : R[X]
⊢ g ∣ p✝ - p✝ %ₘ g
[PROOFSTEP]
rw [modByMonic_eq_sub_mul_div _ hg, sub_sub_cancel]
[GOAL]
case ih
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
g : R[X]
hg : Monic g
p✝ : R[X]
⊢ g ∣ g * (p✝ /ₘ g)
[PROOFSTEP]
exact dvd_mul_right _ _
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
g : R[X]
hg : Monic g
x : Fin (natDegree g) → R
i : Fin (natDegree g)
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := fun f i => coeff (↑(modByMonicHom hg) f) ↑i,
              map_add' :=
                (_ :
                  ∀ (f₁ f₂ : AdjoinRoot g),
                    (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) (f₁ + f₂) =
                      (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) f₁ +
                        (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) f₂) },
          map_smul' :=
            (_ :
              ∀ (f₁ : R) (f₂ : AdjoinRoot g),
                AddHom.toFun
                    { toFun := fun f i => coeff (↑(modByMonicHom hg) f) ↑i,
                      map_add' :=
                        (_ :
                          ∀ (f₁ f₂ : AdjoinRoot g),
                            (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) (f₁ + f₂) =
                              (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) f₁ +
                                (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) f₂) }
                    (f₁ • f₂) =
                  ↑(RingHom.id R) f₁ •
                    AddHom.toFun
                      { toFun := fun f i => coeff (↑(modByMonicHom hg) f) ↑i,
                        map_add' :=
                          (_ :
                            ∀ (f₁ f₂ : AdjoinRoot g),
                              (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) (f₁ + f₂) =
                                (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) f₁ +
                                  (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) f₂) }
                      f₂) }.toAddHom
      ((fun c => ↑(mk g) (∑ i : Fin (natDegree g), ↑(monomial ↑i) (c i))) x) i =
    x i
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
g : R[X]
hg : Monic g
x : Fin (natDegree g) → R
i : Fin (natDegree g)
✝ : Nontrivial R
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := fun f i => coeff (↑(modByMonicHom hg) f) ↑i,
              map_add' :=
                (_ :
                  ∀ (f₁ f₂ : AdjoinRoot g),
                    (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) (f₁ + f₂) =
                      (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) f₁ +
                        (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) f₂) },
          map_smul' :=
            (_ :
              ∀ (f₁ : R) (f₂ : AdjoinRoot g),
                AddHom.toFun
                    { toFun := fun f i => coeff (↑(modByMonicHom hg) f) ↑i,
                      map_add' :=
                        (_ :
                          ∀ (f₁ f₂ : AdjoinRoot g),
                            (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) (f₁ + f₂) =
                              (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) f₁ +
                                (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) f₂) }
                    (f₁ • f₂) =
                  ↑(RingHom.id R) f₁ •
                    AddHom.toFun
                      { toFun := fun f i => coeff (↑(modByMonicHom hg) f) ↑i,
                        map_add' :=
                          (_ :
                            ∀ (f₁ f₂ : AdjoinRoot g),
                              (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) (f₁ + f₂) =
                                (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) f₁ +
                                  (fun f i => coeff (↑(modByMonicHom hg) f) ↑i) f₂) }
                      f₂) }.toAddHom
      ((fun c => ↑(mk g) (∑ i : Fin (natDegree g), ↑(monomial ↑i) (c i))) x) i =
    x i
[PROOFSTEP]
simp only [modByMonicHom_mk]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
g : R[X]
hg : Monic g
x : Fin (natDegree g) → R
i : Fin (natDegree g)
✝ : Nontrivial R
⊢ coeff ((∑ x_1 : Fin (natDegree g), ↑(monomial ↑x_1) (x x_1)) %ₘ g) ↑i = x i
[PROOFSTEP]
rw [(modByMonic_eq_self_iff hg).mpr, finset_sum_coeff]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
g : R[X]
hg : Monic g
x : Fin (natDegree g) → R
i : Fin (natDegree g)
✝ : Nontrivial R
⊢ ∑ b : Fin (natDegree g), coeff (↑(monomial ↑b) (x b)) ↑i = x i
[PROOFSTEP]
simp_rw [coeff_monomial, Fin.val_eq_val, Finset.sum_ite_eq', if_pos (Finset.mem_univ _)]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
g : R[X]
hg : Monic g
x : Fin (natDegree g) → R
i : Fin (natDegree g)
✝ : Nontrivial R
⊢ degree (∑ x_1 : Fin (natDegree g), ↑(monomial ↑x_1) (x x_1)) < degree g
[PROOFSTEP]
simp_rw [← C_mul_X_pow_eq_monomial]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
g : R[X]
hg : Monic g
x : Fin (natDegree g) → R
i : Fin (natDegree g)
✝ : Nontrivial R
⊢ degree (∑ x_1 : Fin (natDegree g), ↑C (x x_1) * X ^ ↑x_1) < degree g
[PROOFSTEP]
exact (degree_eq_natDegree <| hg.ne_zero).symm ▸ degree_sum_fin_lt _
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
g : R[X]
hg : Monic g
i : Fin (natDegree g)
⊢ ↑(powerBasisAux' hg) i = root g ^ ↑i
[PROOFSTEP]
simp only [powerBasisAux', Basis.coe_ofEquivFun, LinearEquiv.coe_symm_mk]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
g : R[X]
hg : Monic g
i : Fin (natDegree g)
⊢ ↑(mk g) (∑ x : Fin (natDegree g), ↑(monomial ↑x) (Function.update 0 i 1 x)) = root g ^ ↑i
[PROOFSTEP]
rw [Finset.sum_eq_single i]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
g : R[X]
hg : Monic g
i : Fin (natDegree g)
⊢ ↑(mk g) (↑(monomial ↑i) (Function.update 0 i 1 i)) = root g ^ ↑i
[PROOFSTEP]
rw [Function.update_same, monomial_one_right_eq_X_pow, (mk g).map_pow, mk_X]
[GOAL]
case h₀
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
g : R[X]
hg : Monic g
i : Fin (natDegree g)
⊢ ∀ (b : Fin (natDegree g)), b ∈ Finset.univ → b ≠ i → ↑(monomial ↑b) (Function.update 0 i 1 b) = 0
[PROOFSTEP]
intro j _ hj
[GOAL]
case h₀
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
g : R[X]
hg : Monic g
i j : Fin (natDegree g)
a✝ : j ∈ Finset.univ
hj : j ≠ i
⊢ ↑(monomial ↑j) (Function.update 0 i 1 j) = 0
[PROOFSTEP]
rw [← monomial_zero_right _]
[GOAL]
case h₀
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
g : R[X]
hg : Monic g
i j : Fin (natDegree g)
a✝ : j ∈ Finset.univ
hj : j ≠ i
⊢ ↑(monomial ↑j) (Function.update 0 i 1 j) = ↑(monomial ?m.1619036) 0
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
g : R[X]
hg : Monic g
i j : Fin (natDegree g)
a✝ : j ∈ Finset.univ
hj : j ≠ i
⊢ ℕ
[PROOFSTEP]
convert
  congr_arg _
    (Function.update_noteq hj _ _)
      -- Fix `DecidableEq` mismatch
[GOAL]
case h₁
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
g : R[X]
hg : Monic g
i : Fin (natDegree g)
⊢ ¬i ∈ Finset.univ → ↑(monomial ↑i) (Function.update 0 i 1 i) = 0
[PROOFSTEP]
intros
[GOAL]
case h₁
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
g : R[X]
hg : Monic g
i : Fin (natDegree g)
a✝ : ¬i ∈ Finset.univ
⊢ ↑(monomial ↑i) (Function.update 0 i 1 i) = 0
[PROOFSTEP]
have := Finset.mem_univ i
[GOAL]
case h₁
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
g : R[X]
hg : Monic g
i : Fin (natDegree g)
a✝ : ¬i ∈ Finset.univ
this : i ∈ Finset.univ
⊢ ↑(monomial ↑i) (Function.update 0 i 1 i) = 0
[PROOFSTEP]
contradiction
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
⊢ minpoly K (root f) = f * ↑C (Polynomial.leadingCoeff f)⁻¹
[PROOFSTEP]
have f'_monic : Monic _ := monic_mul_leadingCoeff_inv hf
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
⊢ minpoly K (root f) = f * ↑C (Polynomial.leadingCoeff f)⁻¹
[PROOFSTEP]
refine' (minpoly.unique K _ f'_monic _ _).symm
[GOAL]
case refine'_1
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
⊢ ↑(aeval (root f)) (f * ↑C (Polynomial.leadingCoeff f)⁻¹) = 0
[PROOFSTEP]
rw [AlgHom.map_mul, aeval_eq, mk_self, zero_mul]
[GOAL]
case refine'_2
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
⊢ ∀ (q : K[X]), Monic q → ↑(aeval (root f)) q = 0 → degree (f * ↑C (Polynomial.leadingCoeff f)⁻¹) ≤ degree q
[PROOFSTEP]
intro q q_monic q_aeval
[GOAL]
case refine'_2
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
q : K[X]
q_monic : Monic q
q_aeval : ↑(aeval (root f)) q = 0
⊢ degree (f * ↑C (Polynomial.leadingCoeff f)⁻¹) ≤ degree q
[PROOFSTEP]
have commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f :=
  by
  ext
  · simp only [RingHom.comp_apply, mk_C, lift_of]
    rfl
  · simp only [RingHom.comp_apply, mk_X, lift_root]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
q : K[X]
q_monic : Monic q
q_aeval : ↑(aeval (root f)) q = 0
⊢ RingHom.comp (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval) (mk q) = mk f
[PROOFSTEP]
ext
[GOAL]
case h₁.a
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
q : K[X]
q_monic : Monic q
q_aeval : ↑(aeval (root f)) q = 0
x✝ : K
⊢ ↑(RingHom.comp (RingHom.comp (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval) (mk q)) C) x✝ =
    ↑(RingHom.comp (mk f) C) x✝
[PROOFSTEP]
simp only [RingHom.comp_apply, mk_C, lift_of]
[GOAL]
case h₁.a
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
q : K[X]
q_monic : Monic q
q_aeval : ↑(aeval (root f)) q = 0
x✝ : K
⊢ ↑(algebraMap K (AdjoinRoot f)) x✝ = ↑(of f) x✝
[PROOFSTEP]
rfl
[GOAL]
case h₂
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
q : K[X]
q_monic : Monic q
q_aeval : ↑(aeval (root f)) q = 0
⊢ ↑(RingHom.comp (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval) (mk q)) X = ↑(mk f) X
[PROOFSTEP]
simp only [RingHom.comp_apply, mk_X, lift_root]
[GOAL]
case refine'_2
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
q : K[X]
q_monic : Monic q
q_aeval : ↑(aeval (root f)) q = 0
commutes : RingHom.comp (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval) (mk q) = mk f
⊢ degree (f * ↑C (Polynomial.leadingCoeff f)⁻¹) ≤ degree q
[PROOFSTEP]
rw [degree_eq_natDegree f'_monic.ne_zero, degree_eq_natDegree q_monic.ne_zero, Nat.cast_withBot, Nat.cast_withBot,
  -- porting note: addedWithBot.coe_le_coe, natDegree_mul hf, natDegree_C, add_zero]
[GOAL]
case refine'_2
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
q : K[X]
q_monic : Monic q
q_aeval : ↑(aeval (root f)) q = 0
commutes : RingHom.comp (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval) (mk q) = mk f
⊢ natDegree f ≤ natDegree q
case refine'_2
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
q : K[X]
q_monic : Monic q
q_aeval : ↑(aeval (root f)) q = 0
commutes : RingHom.comp (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval) (mk q) = mk f
⊢ ↑C (Polynomial.leadingCoeff f)⁻¹ ≠ 0
[PROOFSTEP]
apply natDegree_le_of_dvd
[GOAL]
case refine'_2.h1
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
q : K[X]
q_monic : Monic q
q_aeval : ↑(aeval (root f)) q = 0
commutes : RingHom.comp (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval) (mk q) = mk f
⊢ f ∣ q
[PROOFSTEP]
have : mk f q = 0 := by rw [← commutes, RingHom.comp_apply, mk_self, RingHom.map_zero]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
q : K[X]
q_monic : Monic q
q_aeval : ↑(aeval (root f)) q = 0
commutes : RingHom.comp (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval) (mk q) = mk f
⊢ ↑(mk f) q = 0
[PROOFSTEP]
rw [← commutes, RingHom.comp_apply, mk_self, RingHom.map_zero]
[GOAL]
case refine'_2.h1
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
q : K[X]
q_monic : Monic q
q_aeval : ↑(aeval (root f)) q = 0
commutes : RingHom.comp (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval) (mk q) = mk f
this : ↑(mk f) q = 0
⊢ f ∣ q
[PROOFSTEP]
exact mk_eq_zero.1 this
[GOAL]
case refine'_2.h2
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
q : K[X]
q_monic : Monic q
q_aeval : ↑(aeval (root f)) q = 0
commutes : RingHom.comp (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval) (mk q) = mk f
⊢ q ≠ 0
[PROOFSTEP]
exact q_monic.ne_zero
[GOAL]
case refine'_2
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : Monic (f * ↑C (Polynomial.leadingCoeff f)⁻¹)
q : K[X]
q_monic : Monic q
q_aeval : ↑(aeval (root f)) q = 0
commutes : RingHom.comp (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval) (mk q) = mk f
⊢ ↑C (Polynomial.leadingCoeff f)⁻¹ ≠ 0
[PROOFSTEP]
rwa [Ne.def, C_eq_zero, inv_eq_zero, leadingCoeff_eq_zero]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
⊢ Basis (Fin (natDegree f)) K (AdjoinRoot f)
[PROOFSTEP]
let f' := f * C f.leadingCoeff⁻¹
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := f * ↑C (Polynomial.leadingCoeff f)⁻¹
⊢ Basis (Fin (natDegree f)) K (AdjoinRoot f)
[PROOFSTEP]
have deg_f' : f'.natDegree = f.natDegree :=
  by
  rw [natDegree_mul hf, natDegree_C, add_zero]
  · rwa [Ne.def, C_eq_zero, inv_eq_zero, leadingCoeff_eq_zero]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := f * ↑C (Polynomial.leadingCoeff f)⁻¹
⊢ natDegree f' = natDegree f
[PROOFSTEP]
rw [natDegree_mul hf, natDegree_C, add_zero]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := f * ↑C (Polynomial.leadingCoeff f)⁻¹
⊢ ↑C (Polynomial.leadingCoeff f)⁻¹ ≠ 0
[PROOFSTEP]
rwa [Ne.def, C_eq_zero, inv_eq_zero, leadingCoeff_eq_zero]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := f * ↑C (Polynomial.leadingCoeff f)⁻¹
deg_f' : natDegree f' = natDegree f
⊢ Basis (Fin (natDegree f)) K (AdjoinRoot f)
[PROOFSTEP]
have minpoly_eq : minpoly K (root f) = f' := minpoly_root hf
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := f * ↑C (Polynomial.leadingCoeff f)⁻¹
deg_f' : natDegree f' = natDegree f
minpoly_eq : minpoly K (root f) = f'
⊢ Basis (Fin (natDegree f)) K (AdjoinRoot f)
[PROOFSTEP]
apply @Basis.mk _ _ _ fun i : Fin f.natDegree => root f ^ i.val
[GOAL]
case hli
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := f * ↑C (Polynomial.leadingCoeff f)⁻¹
deg_f' : natDegree f' = natDegree f
minpoly_eq : minpoly K (root f) = f'
⊢ LinearIndependent K fun i => root f ^ ↑i
[PROOFSTEP]
rw [← deg_f', ← minpoly_eq]
[GOAL]
case hli
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := f * ↑C (Polynomial.leadingCoeff f)⁻¹
deg_f' : natDegree f' = natDegree f
minpoly_eq : minpoly K (root f) = f'
⊢ LinearIndependent K fun i => root f ^ ↑i
[PROOFSTEP]
exact linearIndependent_pow (root f)
[GOAL]
case hsp
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := f * ↑C (Polynomial.leadingCoeff f)⁻¹
deg_f' : natDegree f' = natDegree f
minpoly_eq : minpoly K (root f) = f'
⊢ ⊤ ≤ Submodule.span K (Set.range fun i => root f ^ ↑i)
[PROOFSTEP]
rintro y -
[GOAL]
case hsp
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := f * ↑C (Polynomial.leadingCoeff f)⁻¹
deg_f' : natDegree f' = natDegree f
minpoly_eq : minpoly K (root f) = f'
y : AdjoinRoot f
⊢ y ∈ Submodule.span K (Set.range fun i => root f ^ ↑i)
[PROOFSTEP]
rw [← deg_f', ← minpoly_eq]
[GOAL]
case hsp
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := f * ↑C (Polynomial.leadingCoeff f)⁻¹
deg_f' : natDegree f' = natDegree f
minpoly_eq : minpoly K (root f) = f'
y : AdjoinRoot f
⊢ y ∈ Submodule.span K (Set.range fun i => root f ^ ↑i)
[PROOFSTEP]
apply (isIntegral_root hf).mem_span_pow
[GOAL]
case hsp
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := f * ↑C (Polynomial.leadingCoeff f)⁻¹
deg_f' : natDegree f' = natDegree f
minpoly_eq : minpoly K (root f) = f'
y : AdjoinRoot f
⊢ ∃ f_1, y = ↑(aeval (root f)) f_1
[PROOFSTEP]
obtain ⟨g⟩ := y
[GOAL]
case hsp.mk
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g✝ : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := f * ↑C (Polynomial.leadingCoeff f)⁻¹
deg_f' : natDegree f' = natDegree f
minpoly_eq : minpoly K (root f) = f'
y : AdjoinRoot f
g : K[X]
⊢ ∃ f_1, Quot.mk Setoid.r g = ↑(aeval (root f)) f_1
[PROOFSTEP]
use g
[GOAL]
case h
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g✝ : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := f * ↑C (Polynomial.leadingCoeff f)⁻¹
deg_f' : natDegree f' = natDegree f
minpoly_eq : minpoly K (root f) = f'
y : AdjoinRoot f
g : K[X]
⊢ Quot.mk Setoid.r g = ↑(aeval (root f)) g
[PROOFSTEP]
rw [aeval_eq]
[GOAL]
case h
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g✝ : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := f * ↑C (Polynomial.leadingCoeff f)⁻¹
deg_f' : natDegree f' = natDegree f
minpoly_eq : minpoly K (root f) = f'
y : AdjoinRoot f
g : K[X]
⊢ Quot.mk Setoid.r g = ↑(mk f) g
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
⊢ ∀ (i : Fin (natDegree f)), ↑(powerBasisAux hf) i = root f ^ ↑i
[PROOFSTEP]
simp [powerBasisAux]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
⊢ minpoly K (powerBasis hf).gen = f * ↑C (Polynomial.leadingCoeff f)⁻¹
[PROOFSTEP]
rw [powerBasis_gen, minpoly_root hf]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝¹ : CommRing R
g : R[X]
inst✝ : Field K
f : K[X]
hf : Monic f
hf' : optParam (f ≠ 0) (_ : f ≠ 0)
⊢ minpoly K (powerBasis hf').gen = f
[PROOFSTEP]
rw [minpoly_powerBasis_gen hf', hf.leadingCoeff, inv_one, C.map_one, mul_one]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ ↑(aeval { val := x, property := (_ : x ∈ adjoin R {x}) }) (minpoly R x) = 0
[PROOFSTEP]
simp [← Subalgebra.coe_eq_zero, aeval_subalgebra_coe]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
a : AdjoinRoot (minpoly R x)
⊢ ↑(aeval { val := x, property := (_ : x ∈ adjoin R {x}) }) (minpoly R x) = 0
[PROOFSTEP]
simp [← Subalgebra.coe_eq_zero, aeval_subalgebra_coe]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ ↑(toAdjoin R x) (↑(mk (minpoly R x)) X) = { val := x, property := (_ : x ∈ adjoin R {x}) }
[PROOFSTEP]
simp [toAdjoin]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ Function.Surjective ↑(toAdjoin R x)
[PROOFSTEP]
rw [← range_top_iff_surjective, _root_.eq_top_iff, ← adjoin_adjoin_coe_preimage]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ adjoin R (Subtype.val ⁻¹' {x}) ≤ AlgHom.range (toAdjoin R x)
[PROOFSTEP]
refine' adjoin_le _
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ Subtype.val ⁻¹' {x} ⊆ ↑(AlgHom.range (toAdjoin R x))
[PROOFSTEP]
simp only [AlgHom.coe_range, Set.mem_range]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ Subtype.val ⁻¹' {x} ⊆ Set.range ↑(toAdjoin R x)
[PROOFSTEP]
rintro ⟨y₁, y₂⟩ h
[GOAL]
case mk
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y₁ : S
y₂ : y₁ ∈ ↑(adjoin R {x})
h : { val := y₁, property := y₂ } ∈ Subtype.val ⁻¹' {x}
⊢ { val := y₁, property := y₂ } ∈ Set.range ↑(toAdjoin R x)
[PROOFSTEP]
refine' ⟨mk (minpoly R x) X, by simpa [toAdjoin] using h.symm⟩
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y₁ : S
y₂ : y₁ ∈ ↑(adjoin R {x})
h : { val := y₁, property := y₂ } ∈ Subtype.val ⁻¹' {x}
⊢ ↑(toAdjoin R x) (↑(mk (minpoly R x)) X) = { val := y₁, property := y₂ }
[PROOFSTEP]
simpa [toAdjoin] using h.symm
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
g : R[X]
pb : PowerBasis R S
h₁ : ↑(aeval (root g)) (minpoly R pb.gen) = 0
h₂ : ↑(aeval pb.gen) g = 0
src✝ : AdjoinRoot g →ₐ[R] S := liftHom g pb.gen h₂
x : AdjoinRoot g
⊢ ↑(PowerBasis.lift pb (root g) h₁) (↑(liftHom g pb.gen h₂) x) = x
[PROOFSTEP]
induction x using AdjoinRoot.induction_on
[GOAL]
case ih
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
g : R[X]
pb : PowerBasis R S
h₁ : ↑(aeval (root g)) (minpoly R pb.gen) = 0
h₂ : ↑(aeval pb.gen) g = 0
src✝ : AdjoinRoot g →ₐ[R] S := liftHom g pb.gen h₂
p✝ : R[X]
⊢ ↑(PowerBasis.lift pb (root g) h₁) (↑(liftHom g pb.gen h₂) (↑(mk g) p✝)) = ↑(mk g) p✝
[PROOFSTEP]
rw [liftHom_mk, pb.lift_aeval, aeval_eq]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
g : R[X]
pb : PowerBasis R S
h₁ : ↑(aeval (root g)) (minpoly R pb.gen) = 0
h₂ : ↑(aeval pb.gen) g = 0
src✝ : AdjoinRoot g →ₐ[R] S := liftHom g pb.gen h₂
x : S
⊢ ↑(liftHom g pb.gen h₂) (↑(PowerBasis.lift pb (root g) h₁) x) = x
[PROOFSTEP]
nontriviality S
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
g : R[X]
pb : PowerBasis R S
h₁ : ↑(aeval (root g)) (minpoly R pb.gen) = 0
h₂ : ↑(aeval pb.gen) g = 0
src✝ : AdjoinRoot g →ₐ[R] S := liftHom g pb.gen h₂
x : S
✝ : Nontrivial S
⊢ ↑(liftHom g pb.gen h₂) (↑(PowerBasis.lift pb (root g) h₁) x) = x
[PROOFSTEP]
obtain ⟨f, _hf, rfl⟩ := pb.exists_eq_aeval x
[GOAL]
case intro.intro
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
g : R[X]
pb : PowerBasis R S
h₁ : ↑(aeval (root g)) (minpoly R pb.gen) = 0
h₂ : ↑(aeval pb.gen) g = 0
src✝ : AdjoinRoot g →ₐ[R] S := liftHom g pb.gen h₂
✝ : Nontrivial S
f : R[X]
_hf : natDegree f < pb.dim
⊢ ↑(liftHom g pb.gen h₂) (↑(PowerBasis.lift pb (root g) h₁) (↑(aeval pb.gen) f)) = ↑(aeval pb.gen) f
[PROOFSTEP]
rw [pb.lift_aeval, aeval_eq, liftHom_mk]
[GOAL]
R : Type u
S : Type v
K : Type w
L : Type u_1
F : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
pb : PowerBasis F K
f : F[X]
hf : f ≠ 0
x : L
⊢ x ∈ roots (Polynomial.map (algebraMap F L) (minpoly F (powerBasis hf).gen)) ↔
    ↑(Equiv.refl L) x ∈ roots (Polynomial.map (algebraMap F L) f)
[PROOFSTEP]
rw [powerBasis_gen, minpoly_root hf, Polynomial.map_mul, roots_mul, Polynomial.map_C, roots_C, add_zero,
  Equiv.refl_apply]
[GOAL]
R : Type u
S : Type v
K : Type w
L : Type u_1
F : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
pb : PowerBasis F K
f : F[X]
hf : f ≠ 0
x : L
⊢ Polynomial.map (algebraMap F L) f * Polynomial.map (algebraMap F L) (↑C (Polynomial.leadingCoeff f)⁻¹) ≠ 0
[PROOFSTEP]
rw [← Polynomial.map_mul]
[GOAL]
R : Type u
S : Type v
K : Type w
L : Type u_1
F : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
pb : PowerBasis F K
f : F[X]
hf : f ≠ 0
x : L
⊢ Polynomial.map (algebraMap F L) (f * ↑C (Polynomial.leadingCoeff f)⁻¹) ≠ 0
[PROOFSTEP]
exact map_monic_ne_zero (monic_mul_leadingCoeff_inv hf)
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
I : Ideal R
f : R[X]
⊢ Ideal.map (of f) I = Ideal.map (Ideal.Quotient.mk (span {f})) (Ideal.map C I)
[PROOFSTEP]
rw [of, AdjoinRoot.mk, Ideal.map_map]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
I : Ideal R
f : R[X]
x : AdjoinRoot f
⊢ ↑(RingEquiv.symm (quotMapOfEquivQuotMapCMapSpanMk I f))
      (↑(Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (span {f})) (Ideal.map C I))) x) =
    ↑(Ideal.Quotient.mk (Ideal.map (of f) I)) x
[PROOFSTEP]
rw [quotMapOfEquivQuotMapCMapSpanMk, Ideal.quotEquivOfEq_symm]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
I : Ideal R
f : R[X]
x : AdjoinRoot f
⊢ ↑(quotEquivOfEq (_ : Ideal.map (Ideal.Quotient.mk (span {f})) (Ideal.map C I) = Ideal.map (of f) I))
      (↑(Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (span {f})) (Ideal.map C I))) x) =
    ↑(Ideal.Quotient.mk (Ideal.map (of f) I)) x
[PROOFSTEP]
exact Ideal.quotEquivOfEq_mk _ _
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
I : Ideal R
f : R[X]
⊢ span {↑(Ideal.Quotient.mk (Ideal.map C I)) f} =
    Ideal.map (↑(polynomialQuotientEquivQuotientPolynomial I)) (span {Polynomial.map (Ideal.Quotient.mk I) f})
[PROOFSTEP]
rw [map_span, Set.image_singleton, RingEquiv.coe_toRingHom, polynomialQuotientEquivQuotientPolynomial_map_mk I f]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
I : Ideal R
f p : R[X]
⊢ ↑(quotQuotEquivComm I f)
      (↑(Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) p)) =
    ↑(Ideal.Quotient.mk (span {↑(Ideal.Quotient.mk (Ideal.map C I)) f})) (↑(Ideal.Quotient.mk (Ideal.map C I)) p)
[PROOFSTEP]
simp only [Polynomial.quotQuotEquivComm, quotientEquiv_mk, polynomialQuotientEquivQuotientPolynomial_map_mk]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
I : Ideal R
f p : R[X]
⊢ ↑(RingEquiv.symm (quotQuotEquivComm I f))
      (↑(Ideal.Quotient.mk (span {↑(Ideal.Quotient.mk (Ideal.map C I)) f})) (↑(Ideal.Quotient.mk (Ideal.map C I)) p)) =
    ↑(Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) p)
[PROOFSTEP]
simp only [Polynomial.quotQuotEquivComm, quotientEquiv_symm_mk, polynomialQuotientEquivQuotientPolynomial_symm_mk]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
I : Ideal R
f : R[X]
⊢ Ideal.map (Ideal.Quotient.mk (Ideal.map C I)) (span {f}) = span {↑(Ideal.Quotient.mk (Ideal.map C I)) f}
[PROOFSTEP]
rw [map_span, Set.image_singleton]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
I : Ideal R
f p : R[X]
⊢ ↑(RingEquiv.symm (quotAdjoinRootEquivQuotPolynomialQuot I f))
      (↑(Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) p)) =
    ↑(Ideal.Quotient.mk (Ideal.map (of f) I)) (↑(mk f) p)
[PROOFSTEP]
rw [quotAdjoinRootEquivQuotPolynomialQuot, RingEquiv.symm_trans_apply, RingEquiv.symm_trans_apply,
  RingEquiv.symm_trans_apply, RingEquiv.symm_symm, Polynomial.quotQuotEquivComm_mk, Ideal.quotEquivOfEq_symm,
  Ideal.quotEquivOfEq_mk, ← RingHom.comp_apply, ← DoubleQuot.quotQuotMk,
  quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_symm_quotQuotMk, quotMapOfEquivQuotMapCMapSpanMk_symm_mk]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
I✝ : Ideal R
f✝ f : R[X]
I : Ideal R
x : R
⊢ ↑(quotAdjoinRootEquivQuotPolynomialQuot I f) (↑(algebraMap R (AdjoinRoot f ⧸ Ideal.map (of f) I)) x) =
    ↑(algebraMap R ((R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})) x
[PROOFSTEP]
have :
  algebraMap R (AdjoinRoot f ⧸ Ideal.map (of f) I) x =
    Ideal.Quotient.mk (Ideal.map (AdjoinRoot.of f) I) ((mk f) (C x)) :=
  rfl
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
I✝ : Ideal R
f✝ f : R[X]
I : Ideal R
x : R
this :
  ↑(algebraMap R (AdjoinRoot f ⧸ Ideal.map (of f) I)) x = ↑(Ideal.Quotient.mk (Ideal.map (of f) I)) (↑(mk f) (↑C x))
⊢ ↑(quotAdjoinRootEquivQuotPolynomialQuot I f) (↑(algebraMap R (AdjoinRoot f ⧸ Ideal.map (of f) I)) x) =
    ↑(algebraMap R ((R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})) x
[PROOFSTEP]
rw [this, quotAdjoinRootEquivQuotPolynomialQuot_mk_of, map_C]
  -- Porting note: the following `rfl` was not needed
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
I✝ : Ideal R
f✝ f : R[X]
I : Ideal R
x : R
this :
  ↑(algebraMap R (AdjoinRoot f ⧸ Ideal.map (of f) I)) x = ↑(Ideal.Quotient.mk (Ideal.map (of f) I)) (↑(mk f) (↑C x))
⊢ ↑(Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f})) (↑C (↑(Ideal.Quotient.mk I) x)) =
    ↑(algebraMap R ((R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})) x
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
I✝ : Ideal R
f✝ f g : R[X]
I : Ideal R
⊢ ↑(quotEquivQuotMap f I) (↑(Ideal.Quotient.mk (Ideal.map (of f) I)) (↑(mk f) g)) =
    ↑(Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) g)
[PROOFSTEP]
rw [AdjoinRoot.quotEquivQuotMap_apply, AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_mk_of]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
I✝ : Ideal R
f✝ f g : R[X]
I : Ideal R
⊢ ↑(AlgEquiv.symm (quotEquivQuotMap f I))
      (↑(Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) g)) =
    ↑(Ideal.Quotient.mk (Ideal.map (of f) I)) (↑(mk f) g)
[PROOFSTEP]
rw [AdjoinRoot.quotEquivQuotMap_symm_apply, AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pb : PowerBasis R S
I : Ideal R
x : R
⊢ ↑(aeval (root (minpoly R pb.gen))) (minpoly R pb.gen) = 0
[PROOFSTEP]
rw [AdjoinRoot.aeval_eq, AdjoinRoot.mk_self]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pb : PowerBasis R S
I : Ideal R
x : R
⊢ Ideal.map (of (minpoly R pb.gen)) I =
    Ideal.map
      (↑(toRingEquiv
          (AlgEquiv.symm
            (equiv' (minpoly R pb.gen) pb (_ : ↑(aeval (root (minpoly R pb.gen))) (minpoly R pb.gen) = 0)
              (_ : ↑(aeval pb.gen) (minpoly R pb.gen) = 0)))))
      (Ideal.map (algebraMap R S) I)
[PROOFSTEP]
rw [Ideal.map_map, AlgEquiv.toRingEquiv_eq_coe, ← AlgEquiv.coe_ringHom_commutes, ← AdjoinRoot.algebraMap_eq,
  AlgHom.comp_algebraMap]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pb : PowerBasis R S
I : Ideal R
x : R
⊢ ↑(quotientEquiv (Ideal.map (algebraMap R S) I) (Ideal.map (of (minpoly R pb.gen)) I)
          (toRingEquiv
            (AlgEquiv.symm
              (equiv' (minpoly R pb.gen) pb (_ : ↑(aeval (root (minpoly R pb.gen))) (minpoly R pb.gen) = 0)
                (_ : ↑(aeval pb.gen) (minpoly R pb.gen) = 0))))
          (_ :
            Ideal.map (of (minpoly R pb.gen)) I =
              Ideal.map
                (↑(toRingEquiv
                    (AlgEquiv.symm
                      (equiv' (minpoly R pb.gen) pb (_ : ↑(aeval (root (minpoly R pb.gen))) (minpoly R pb.gen) = 0)
                        (_ : ↑(aeval pb.gen) (minpoly R pb.gen) = 0)))))
                (Ideal.map (algebraMap R S) I)))
      (↑(algebraMap R (S ⧸ Ideal.map (algebraMap R S) I)) x) =
    ↑(algebraMap R (AdjoinRoot (minpoly R pb.gen) ⧸ Ideal.map (of (minpoly R pb.gen)) I)) x
[PROOFSTEP]
rw [← Ideal.Quotient.mk_algebraMap, Ideal.quotientEquiv_apply, RingHom.toFun_eq_coe, Ideal.quotientMap_mk,
  AlgEquiv.toRingEquiv_eq_coe, RingEquiv.coe_toRingHom, AlgEquiv.coe_ringEquiv, AlgEquiv.commutes,
  Quotient.mk_algebraMap]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pb : PowerBasis R S
I : Ideal R
x : R
⊢ ↑(Ideal.Quotient.mk (Ideal.map (of (minpoly R pb.gen)) I)) (↑(algebraMap R (AdjoinRoot (minpoly R pb.gen))) x) =
    ↑(algebraMap R (AdjoinRoot (minpoly R pb.gen) ⧸ Ideal.map (of (minpoly R pb.gen)) I)) x
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pb : PowerBasis R S
I : Ideal R
g : R[X]
⊢ ↑(quotientEquivQuotientMinpolyMap pb I) (↑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) (↑(aeval pb.gen) g)) =
    ↑(Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}))
      (Polynomial.map (Ideal.Quotient.mk I) g)
[PROOFSTEP]
rw [PowerBasis.quotientEquivQuotientMinpolyMap, AlgEquiv.trans_apply, AlgEquiv.ofRingEquiv_apply, quotientEquiv_mk,
  AlgEquiv.coe_ringEquiv', AdjoinRoot.equiv'_symm_apply, PowerBasis.lift_aeval, AdjoinRoot.aeval_eq,
  AdjoinRoot.quotEquivQuotMap_apply_mk]
[GOAL]
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pb : PowerBasis R S
I : Ideal R
g : R[X]
⊢ ↑(AlgEquiv.symm (quotientEquivQuotientMinpolyMap pb I))
      (↑(Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}))
        (Polynomial.map (Ideal.Quotient.mk I) g)) =
    ↑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) (↑(aeval pb.gen) g)
[PROOFSTEP]
simp only [quotientEquivQuotientMinpolyMap, toRingEquiv_eq_coe, symm_trans_apply, quotEquivQuotMap_symm_apply_mk,
  ofRingEquiv_symm_apply, quotientEquiv_symm_mk, toRingEquiv_symm, RingEquiv.symm_symm, AdjoinRoot.equiv'_apply,
  coe_ringEquiv, liftHom_mk, symm_toRingEquiv]


[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
X Y : C
f : X ⟶ Y
⊢ d f ≫ f = 0
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
X Y : C
f : X ⟶ Y
⊢ π (kernel f) ≫ kernel.ι f ≫ cokernel.π (d f) = 0
[PROOFSTEP]
rw [← Category.assoc, cokernel.condition]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
hP : Projective P
⊢ PreservesFiniteColimits (preadditiveCoyonedaObj (op P))
[PROOFSTEP]
haveI := (projective_iff_preservesEpimorphisms_preadditiveCoyoneda_obj' P).mp hP
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
hP : Projective P
this : Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj (op P))
⊢ PreservesFiniteColimits (preadditiveCoyonedaObj (op P))
[PROOFSTEP]
haveI := @Functor.preservesEpimorphisms_of_preserves_of_reflects _ _ _ _ _ _ _ _ this _
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
hP : Projective P
this✝ : Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj (op P))
this : Functor.PreservesEpimorphisms (preadditiveCoyonedaObj (op P))
⊢ PreservesFiniteColimits (preadditiveCoyonedaObj (op P))
[PROOFSTEP]
apply Functor.preservesFiniteColimitsOfPreservesEpisAndKernels
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
hP : PreservesFiniteColimits (preadditiveCoyonedaObj (op P))
⊢ Projective P
[PROOFSTEP]
rw [projective_iff_preservesEpimorphisms_preadditiveCoyoneda_obj']
  -- porting note: this next line wasn't necessary in Lean 3
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
hP : PreservesFiniteColimits (preadditiveCoyonedaObj (op P))
⊢ Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj (op P))
[PROOFSTEP]
dsimp only [preadditiveCoyoneda]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
hP : PreservesFiniteColimits (preadditiveCoyonedaObj (op P))
⊢ Functor.PreservesEpimorphisms (preadditiveCoyonedaObj (op P) ⋙ forget₂ (ModuleCat (End (op P))) AddCommGroupCat)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ 0 ≫ HomologicalComplex.d ((ChainComplex.single₀ C).obj Z) 1 0 =
    HomologicalComplex.d (ofComplex Z) 1 0 ≫ Projective.π Z
[PROOFSTEP]
simp only [ofComplex_X, ChainComplex.single₀_obj_X_0, ChainComplex.single₀_obj_X_succ, ComplexShape.down_Rel, not_true,
  ChainComplex.single₀_obj_X_d, comp_zero, ofComplex_d, eqToHom_refl, Category.id_comp, dite_eq_ite, ite_true]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ 0 =
    (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
          (d (d (Projective.π Z)))
          (_ :
            {
                      fst :=
                        syzygies
                          { fst := over Z,
                                snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd,
                      snd :=
                        {
                          fst :=
                            d
                              { fst := over Z,
                                    snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd,
                          snd :=
                            (_ :
                              d
                                    { fst := over Z,
                                          snd :=
                                            { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd ≫
                                  { fst := over Z,
                                        snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd =
                                0) } }.snd.fst ≫
                { fst := over Z, snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.snd.snd =
              0)
          (fun t =>
            { fst := syzygies t.snd.snd.snd.snd.fst,
              snd :=
                { fst := d t.snd.snd.snd.snd.fst, snd := (_ : d t.snd.snd.snd.snd.fst ≫ t.snd.snd.snd.snd.fst = 0) } })
          0).d₀ ≫
      Projective.π Z
[PROOFSTEP]
exact (exact_d_f (Projective.π Z)).w.symm
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n : ℕ
⊢ Exact (HomologicalComplex.d (ofComplex Z) (0 + 2) (0 + 1)) (HomologicalComplex.d (ofComplex Z) (0 + 1) 0)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n : ℕ
⊢ Exact
    (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
        (d (d (Projective.π Z)))
        (_ :
          {
                    fst :=
                      syzygies
                        { fst := over Z, snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd,
                    snd :=
                      {
                        fst :=
                          d
                            { fst := over Z,
                                  snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd,
                        snd :=
                          (_ :
                            d
                                  { fst := over Z,
                                        snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd ≫
                                { fst := over Z,
                                      snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd =
                              0) } }.snd.fst ≫
              { fst := over Z, snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.snd.snd =
            0)
        (fun t =>
          { fst := syzygies t.snd.snd.snd.snd.fst,
            snd :=
              { fst := d t.snd.snd.snd.snd.fst, snd := (_ : d t.snd.snd.snd.snd.fst ≫ t.snd.snd.snd.snd.fst = 0) } })
        (0 + 1)).d₀
    (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
        (d (d (Projective.π Z)))
        (_ :
          {
                    fst :=
                      syzygies
                        { fst := over Z, snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd,
                    snd :=
                      {
                        fst :=
                          d
                            { fst := over Z,
                                  snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd,
                        snd :=
                          (_ :
                            d
                                  { fst := over Z,
                                        snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd ≫
                                { fst := over Z,
                                      snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd =
                              0) } }.snd.fst ≫
              { fst := over Z, snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.snd.snd =
            0)
        (fun t =>
          { fst := syzygies t.snd.snd.snd.snd.fst,
            snd :=
              { fst := d t.snd.snd.snd.snd.fst, snd := (_ : d t.snd.snd.snd.snd.fst ≫ t.snd.snd.snd.snd.fst = 0) } })
        0).d₀
[PROOFSTEP]
apply exact_d_f
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n m : ℕ
⊢ Exact (HomologicalComplex.d (ofComplex Z) (m + 1 + 2) (m + 1 + 1))
    (HomologicalComplex.d (ofComplex Z) (m + 1 + 1) (m + 1))
[PROOFSTEP]
simp only [ofComplex_X, ComplexShape.down_Rel, ofComplex_d, eqToHom_refl, Category.id_comp, dite_eq_ite, not_true,
  ite_true]
  -- Porting note: this is probably required now due to
        -- https://github.com/leanprover/lean4/pull/2146
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n m : ℕ
⊢ Exact
    (if m + 1 + 2 = m + 1 + 1 + 1 then
      (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
          (d (d (Projective.π Z)))
          (_ :
            {
                      fst :=
                        syzygies
                          { fst := over Z,
                                snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd,
                      snd :=
                        {
                          fst :=
                            d
                              { fst := over Z,
                                    snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd,
                          snd :=
                            (_ :
                              d
                                    { fst := over Z,
                                          snd :=
                                            { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd ≫
                                  { fst := over Z,
                                        snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd =
                                0) } }.snd.fst ≫
                { fst := over Z, snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.snd.snd =
              0)
          (fun t =>
            { fst := syzygies t.snd.snd.snd.snd.fst,
              snd :=
                { fst := d t.snd.snd.snd.snd.fst, snd := (_ : d t.snd.snd.snd.snd.fst ≫ t.snd.snd.snd.snd.fst = 0) } })
          (m + 1 + 1)).d₀
    else 0)
    (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
        (d (d (Projective.π Z)))
        (_ :
          {
                    fst :=
                      syzygies
                        { fst := over Z, snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd,
                    snd :=
                      {
                        fst :=
                          d
                            { fst := over Z,
                                  snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd,
                        snd :=
                          (_ :
                            d
                                  { fst := over Z,
                                        snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd ≫
                                { fst := over Z,
                                      snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd =
                              0) } }.snd.fst ≫
              { fst := over Z, snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.snd.snd =
            0)
        (fun t =>
          { fst := syzygies t.snd.snd.snd.snd.fst,
            snd :=
              { fst := d t.snd.snd.snd.snd.fst, snd := (_ : d t.snd.snd.snd.snd.fst ≫ t.snd.snd.snd.snd.fst = 0) } })
        (m + 1)).d₀
[PROOFSTEP]
erw [if_pos (c := m + 1 + 1 + 1 = m + 2 + 1) rfl]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n m : ℕ
⊢ Exact
    (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
        (d (d (Projective.π Z)))
        (_ :
          {
                    fst :=
                      syzygies
                        { fst := over Z, snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd,
                    snd :=
                      {
                        fst :=
                          d
                            { fst := over Z,
                                  snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd,
                        snd :=
                          (_ :
                            d
                                  { fst := over Z,
                                        snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd ≫
                                { fst := over Z,
                                      snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd =
                              0) } }.snd.fst ≫
              { fst := over Z, snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.snd.snd =
            0)
        (fun t =>
          { fst := syzygies t.snd.snd.snd.snd.fst,
            snd :=
              { fst := d t.snd.snd.snd.snd.fst, snd := (_ : d t.snd.snd.snd.snd.fst ≫ t.snd.snd.snd.snd.fst = 0) } })
        (m + 1 + 1)).d₀
    (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
        (d (d (Projective.π Z)))
        (_ :
          {
                    fst :=
                      syzygies
                        { fst := over Z, snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd,
                    snd :=
                      {
                        fst :=
                          d
                            { fst := over Z,
                                  snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd,
                        snd :=
                          (_ :
                            d
                                  { fst := over Z,
                                        snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd ≫
                                { fst := over Z,
                                      snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd =
                              0) } }.snd.fst ≫
              { fst := over Z, snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.snd.snd =
            0)
        (fun t =>
          { fst := syzygies t.snd.snd.snd.snd.fst,
            snd :=
              { fst := d t.snd.snd.snd.snd.fst, snd := (_ : d t.snd.snd.snd.snd.fst ≫ t.snd.snd.snd.snd.fst = 0) } })
        (m + 1)).d₀
[PROOFSTEP]
apply exact_d_f
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n : ℕ
x✝ :
  (f : HomologicalComplex.X (ofComplex Z) n ⟶ HomologicalComplex.X ((ChainComplex.single₀ C).obj Z) n) ×'
    (f' : HomologicalComplex.X (ofComplex Z) (n + 1) ⟶ HomologicalComplex.X ((ChainComplex.single₀ C).obj Z) (n + 1)) ×'
      f' ≫ HomologicalComplex.d ((ChainComplex.single₀ C).obj Z) (n + 1) n =
        HomologicalComplex.d (ofComplex Z) (n + 1) n ≫ f
⊢ 0 ≫ HomologicalComplex.d ((ChainComplex.single₀ C).obj Z) (n + 2) (n + 1) =
    HomologicalComplex.d (ofComplex Z) (n + 2) (n + 1) ≫ x✝.snd.fst
[PROOFSTEP]
apply HasZeroObject.to_zero_ext
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ ∀ (n : ℕ), Projective (HomologicalComplex.X (ofComplex Z) n)
[PROOFSTEP]
rintro (_ | _ | _ | n)
[GOAL]
case zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ Projective (HomologicalComplex.X (ofComplex Z) Nat.zero)
[PROOFSTEP]
apply Projective.projective_over
[GOAL]
case succ.zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ Projective (HomologicalComplex.X (ofComplex Z) (Nat.succ Nat.zero))
[PROOFSTEP]
apply Projective.projective_over
[GOAL]
case succ.succ.zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ Projective (HomologicalComplex.X (ofComplex Z) (Nat.succ (Nat.succ Nat.zero)))
[PROOFSTEP]
apply Projective.projective_over
[GOAL]
case succ.succ.succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n : ℕ
⊢ Projective (HomologicalComplex.X (ofComplex Z) (Nat.succ (Nat.succ (Nat.succ n))))
[PROOFSTEP]
apply Projective.projective_over
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ Exact (HomologicalComplex.d (ofComplex Z) 1 0)
    (HomologicalComplex.Hom.f
      (ChainComplex.mkHom (ofComplex Z) ((ChainComplex.single₀ C).obj Z) (Projective.π Z) 0
        (_ :
          0 ≫ HomologicalComplex.d ((ChainComplex.single₀ C).obj Z) 1 0 =
            HomologicalComplex.d (ofComplex Z) 1 0 ≫ Projective.π Z)
        fun n x =>
        { fst := 0,
          snd :=
            (_ :
              0 ≫ HomologicalComplex.d ((ChainComplex.single₀ C).obj Z) (n + 2) (n + 1) =
                HomologicalComplex.d (ofComplex Z) (n + 2) (n + 1) ≫ x.snd.fst) })
      0)
[PROOFSTEP]
simpa using exact_d_f (Projective.π Z)
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ HasProjectiveResolution Z
[PROOFSTEP]
infer_instance