awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
inst_3 : Nontrivial S
x : R
⊢ Eq.{u + 1} (α := ℕ → R) ((h.coeff : (a : S) → ℕ → R) ((algebraMap R S : (a : R) → S) x : S) : ℕ → R)
    (Pi.single (M := fun (j : ℕ) ↦ R) 0 x : (j : ℕ) → R)
have h₁ : ∀ (i : ℕ),
  Eq.{u + 1} (α := R) ((h.coeff : (a : S) → ℕ → R) ((algebraMap R S : (a : R) → S) x : S) i : R)
    (Pi.single (M := fun (j : ℕ) ↦ R) 0 x i : R)
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
inst_3 : Nontrivial S
x : R
i : ℕ
⊢ Eq.{u + 1} (α := R) ((h.coeff : (a : S) → ℕ → R) ((algebraMap R S : (a : R) → S) x : S) i : R)
    (Pi.single (M := fun (j : ℕ) ↦ R) 0 x i : R)
have h₁ : HMul.hMul (β := R) x (Pi.single (M := fun (j : ℕ) ↦ R) 0 1 i : R) = Pi.single (M := fun (j : ℕ) ↦ R) 0 x i
Tactic: rw [Algebra.algebraMap_eq_smul_one, map_smul, coeff_one, Pi.smul_apply, smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
inst_3 : Nontrivial S
x : R
i : ℕ
⊢ HMul.hMul (β := R) x (Pi.single (M := fun (j : ℕ) ↦ R) 0 1 i : R) = Pi.single (M := fun (j : ℕ) ↦ R) 0 x i
have h₁ : ∀ (i : ℕ), Eq.{u + 1} (α := R) ((fun (x_1 : ℕ) (y : R) ↦ x * y) i 0) 0
Tactic: refine (Pi.apply_single (fun _ y => x * y) ?_ 0 1 i).trans (by simp)
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
x y : S
hxy : ∀ i < f.natDegree, Eq.{u + 1} (α := R) ((h.coeff : (a : S) → ℕ → R) x i : R) ((h.coeff : (a : S) → ℕ → R) y i : R)
i : Fin f.natDegree
⊢ Eq.{u + 1} (α := R) ((h.basis.equivFun : (a : S) → Fin f.natDegree → R) x i : R)
    ((h.basis.equivFun : (a : S) → Fin f.natDegree → R) y i : R)
have rw : Eq.{u + 1} (α := R)
  ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R) x : Fin f.natDegree →₀ R) : (a : Fin f.natDegree) → R) i : R)
  ((h.basis.equivFun : (a : S) → Fin f.natDegree → R) y i : R)
Tactic: rw [Basis.equivFun_apply, ← h.coeff_apply_coe, Basis.equivFun_apply, ← h.coeff_apply_coe,
        hxy i i.prop]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
x y : S
hxy : ∀ i < f.natDegree, Eq.{u + 1} (α := R) ((h.coeff : (a : S) → ℕ → R) x i : R) ((h.coeff : (a : S) → ℕ → R) y i : R)
i : Fin f.natDegree
rw :
  Eq.{u + 1} (α := R)
    ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R) x : Fin f.natDegree →₀ R) : (a : Fin f.natDegree) → R) i : R)
    ((h.basis.equivFun : (a : S) → Fin f.natDegree → R) y i : R)
⊢ Eq.{u + 1} (α := R) ((h.basis.equivFun : (a : S) → Fin f.natDegree → R) x i : R)
    ((h.basis.equivFun : (a : S) → Fin f.natDegree → R) y i : R)
have rw₁ : Eq.{u + 1} (α := R) ((h.coeff : (a : S) → ℕ → R) x (↑i : ℕ) : R)
  ((h.basis.equivFun : (a : S) → Fin f.natDegree → R) y i : R)
Tactic: rw [Basis.equivFun_apply, ← h.coeff_apply_coe, Basis.equivFun_apply, ← h.coeff_apply_coe,
        hxy i i.prop]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
x y : S
hxy : ∀ i < f.natDegree, Eq.{u + 1} (α := R) ((h.coeff : (a : S) → ℕ → R) x i : R) ((h.coeff : (a : S) → ℕ → R) y i : R)
i : Fin f.natDegree
rw :
  Eq.{u + 1} (α := R)
    ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R) x : Fin f.natDegree →₀ R) : (a : Fin f.natDegree) → R) i : R)
    ((h.basis.equivFun : (a : S) → Fin f.natDegree → R) y i : R)
rw₁ :
  Eq.{u + 1} (α := R) ((h.coeff : (a : S) → ℕ → R) x (↑i : ℕ) : R)
    ((h.basis.equivFun : (a : S) → Fin f.natDegree → R) y i : R)
⊢ Eq.{u + 1} (α := R) ((h.basis.equivFun : (a : S) → Fin f.natDegree → R) x i : R)
    ((h.basis.equivFun : (a : S) → Fin f.natDegree → R) y i : R)
have rw₂ : Eq.{u + 1} (α := R) ((h.coeff : (a : S) → ℕ → R) x (↑i : ℕ) : R)
  ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R) y : Fin f.natDegree →₀ R) : (a : Fin f.natDegree) → R) i : R)
Tactic: rw [Basis.equivFun_apply, ← h.coeff_apply_coe, Basis.equivFun_apply, ← h.coeff_apply_coe,
        hxy i i.prop]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
x y : S
hxy : ∀ i < f.natDegree, Eq.{u + 1} (α := R) ((h.coeff : (a : S) → ℕ → R) x i : R) ((h.coeff : (a : S) → ℕ → R) y i : R)
i : Fin f.natDegree
rw :
  Eq.{u + 1} (α := R)
    ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R) x : Fin f.natDegree →₀ R) : (a : Fin f.natDegree) → R) i : R)
    ((h.basis.equivFun : (a : S) → Fin f.natDegree → R) y i : R)
rw₁ :
  Eq.{u + 1} (α := R) ((h.coeff : (a : S) → ℕ → R) x (↑i : ℕ) : R)
    ((h.basis.equivFun : (a : S) → Fin f.natDegree → R) y i : R)
rw₂ :
  Eq.{u + 1} (α := R) ((h.coeff : (a : S) → ℕ → R) x (↑i : ℕ) : R)
    ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R) y : Fin f.natDegree →₀ R) : (a : Fin f.natDegree) → R) i : R)
⊢ Eq.{u + 1} (α := R) ((h.basis.equivFun : (a : S) → Fin f.natDegree → R) x i : R)
    ((h.basis.equivFun : (a : S) → Fin f.natDegree → R) y i : R)
have rw₃ : Eq.{u + 1} (α := R) ((h.coeff : (a : S) → ℕ → R) x (↑i : ℕ) : R) ((h.coeff : (a : S) → ℕ → R) y (↑i : ℕ) : R)
Tactic: rw [Basis.equivFun_apply, ← h.coeff_apply_coe, Basis.equivFun_apply, ← h.coeff_apply_coe,
        hxy i i.prop]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
x y : S
hxy : ∀ i < f.natDegree, Eq.{u + 1} (α := R) ((h.coeff : (a : S) → ℕ → R) x i : R) ((h.coeff : (a : S) → ℕ → R) y i : R)
i : Fin f.natDegree
rw :
  Eq.{u + 1} (α := R)
    ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R) x : Fin f.natDegree →₀ R) : (a : Fin f.natDegree) → R) i : R)
    ((h.basis.equivFun : (a : S) → Fin f.natDegree → R) y i : R)
rw₁ :
  Eq.{u + 1} (α := R) ((h.coeff : (a : S) → ℕ → R) x (↑i : ℕ) : R)
    ((h.basis.equivFun : (a : S) → Fin f.natDegree → R) y i : R)
rw₂ :
  Eq.{u + 1} (α := R) ((h.coeff : (a : S) → ℕ → R) x (↑i : ℕ) : R)
    ((((h.basis.repr : (a : S) → Fin f.natDegree →₀ R) y : Fin f.natDegree →₀ R) : (a : Fin f.natDegree) → R) i : R)
rw₃ : Eq.{u + 1} (α := R) ((h.coeff : (a : S) → ℕ → R) x (↑i : ℕ) : R) ((h.coeff : (a : S) → ℕ → R) y (↑i : ℕ) : R)
⊢ Eq.{u + 1} (α := R) ((h.basis.equivFun : (a : S) → Fin f.natDegree → R) x i : R)
    ((h.basis.equivFun : (a : S) → Fin f.natDegree → R) y i : R)
have rw₄ : Eq.{u + 1} (α := R) ((h.coeff : (a : S) → ℕ → R) y (↑i : ℕ) : R) ((h.coeff : (a : S) → ℕ → R) y (↑i : ℕ) : R)
Tactic: rw [Basis.equivFun_apply, ← h.coeff_apply_coe, Basis.equivFun_apply, ← h.coeff_apply_coe,
        hxy i i.prop]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X]
h : IsAdjoinRoot S f
x : S
⊢ (h.lift (algebraMap R S) h.root ⋯ : (a : S) → S) x = x
have rw : Eq (α := S) ((h.lift (algebraMap R S) h.root sorry : (a : S) → S) ((h.map : (a : R[X]) → S) (h.repr x) : S) : S)
  ((h.map : (a : R[X]) → S) (h.repr x) : S)
Tactic: rw [← h.map_repr x, lift_map, ← aeval_def, h.aeval_root_eq_map]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X]
h : IsAdjoinRoot S f
x : S
rw :
  Eq (α := S) ((h.lift (algebraMap R S) h.root ⋯ : (a : S) → S) ((h.map : (a : R[X]) → S) (h.repr x) : S) : S)
    ((h.map : (a : R[X]) → S) (h.repr x) : S)
⊢ (h.lift (algebraMap R S) h.root ⋯ : (a : S) → S) x = x
have rw₁ : eval₂ (algebraMap R S) h.root (h.repr x) = (h.map : (a : R[X]) → S) (h.repr x)
Tactic: rw [← h.map_repr x, lift_map, ← aeval_def, h.aeval_root_eq_map]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X]
h : IsAdjoinRoot S f
x : S
rw :
  Eq (α := S) ((h.lift (algebraMap R S) h.root ⋯ : (a : S) → S) ((h.map : (a : R[X]) → S) (h.repr x) : S) : S)
    ((h.map : (a : R[X]) → S) (h.repr x) : S)
rw₁ : eval₂ (algebraMap R S) h.root (h.repr x) = (h.map : (a : R[X]) → S) (h.repr x)
⊢ (h.lift (algebraMap R S) h.root ⋯ : (a : S) → S) x = x
have rw₂ : Eq.{v + 1} (α := S) ((aeval h.root : (a : R[X]) → S) (h.repr x) : S) ((h.map : (a : R[X]) → S) (h.repr x) : S)
Tactic: rw [← h.map_repr x, lift_map, ← aeval_def, h.aeval_root_eq_map]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X]
h : IsAdjoinRoot S f
x : S
rw :
  Eq (α := S) ((h.lift (algebraMap R S) h.root ⋯ : (a : S) → S) ((h.map : (a : R[X]) → S) (h.repr x) : S) : S)
    ((h.map : (a : R[X]) → S) (h.repr x) : S)
rw₁ : eval₂ (algebraMap R S) h.root (h.repr x) = (h.map : (a : R[X]) → S) (h.repr x)
rw₂ : Eq.{v + 1} (α := S) ((aeval h.root : (a : R[X]) → S) (h.repr x) : S) ((h.map : (a : R[X]) → S) (h.repr x) : S)
⊢ (h.lift (algebraMap R S) h.root ⋯ : (a : S) → S) x = x
have rw₃ : Eq.{v + 1} (α := S) ((h.map : (a : R[X]) → S) (h.repr x) : S) ((h.map : (a : R[X]) → S) (h.repr x) : S)
Tactic: rw [← h.map_repr x, lift_map, ← aeval_def, h.aeval_root_eq_map]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X]
h : IsAdjoinRoot S f
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsTorsionFree R S
inst_6 : IsIntegrallyClosed R
α : S
hα : IsIntegral R α
hα₂ : Eq (α := Subalgebra R S) R[α] ⊤
⊢ Function.Surjective.{u + 1, v + 1} (α := R[X]) (β := S) (⇑(aeval α) : (a : R[X]) → S)
have rw : Eq.{v + 1} (α := Set S) (Set.range.{v, u + 1} (ι := R[X]) (⇑(aeval α) : (a : R[X]) → S)) Set.univ
Tactic: rw [← Set.range_eq_univ, ← AlgHom.coe_range, ← Algebra.adjoin_singleton_eq_range_aeval,
      hα₂, Algebra.coe_top]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X]
h : IsAdjoinRoot S f
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsTorsionFree R S
inst_6 : IsIntegrallyClosed R
α : S
hα : IsIntegral R α
hα₂ : Eq (α := Subalgebra R S) R[α] ⊤
rw : Eq.{v + 1} (α := Set S) (Set.range.{v, u + 1} (ι := R[X]) (⇑(aeval α) : (a : R[X]) → S)) Set.univ
⊢ Function.Surjective.{u + 1, v + 1} (α := R[X]) (β := S) (⇑(aeval α) : (a : R[X]) → S)
have rw₁ : (↑(AlgHom.range (aeval α)) : Set S) = Set.univ
Tactic: rw [← Set.range_eq_univ, ← AlgHom.coe_range, ← Algebra.adjoin_singleton_eq_range_aeval,
      hα₂, Algebra.coe_top]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X]
h : IsAdjoinRoot S f
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsTorsionFree R S
inst_6 : IsIntegrallyClosed R
α : S
hα : IsIntegral R α
hα₂ : Eq (α := Subalgebra R S) R[α] ⊤
rw : Eq.{v + 1} (α := Set S) (Set.range.{v, u + 1} (ι := R[X]) (⇑(aeval α) : (a : R[X]) → S)) Set.univ
rw₁ : (↑(AlgHom.range (aeval α)) : Set S) = Set.univ
⊢ Function.Surjective.{u + 1, v + 1} (α := R[X]) (β := S) (⇑(aeval α) : (a : R[X]) → S)
have rw₂ : (↑R[α] : Set S) = Set.univ
Tactic: rw [← Set.range_eq_univ, ← AlgHom.coe_range, ← Algebra.adjoin_singleton_eq_range_aeval,
      hα₂, Algebra.coe_top]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X]
h : IsAdjoinRoot S f
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsTorsionFree R S
inst_6 : IsIntegrallyClosed R
α : S
hα : IsIntegral R α
hα₂ : Eq (α := Subalgebra R S) R[α] ⊤
rw : Eq.{v + 1} (α := Set S) (Set.range.{v, u + 1} (ι := R[X]) (⇑(aeval α) : (a : R[X]) → S)) Set.univ
rw₁ : (↑(AlgHom.range (aeval α)) : Set S) = Set.univ
rw₂ : (↑R[α] : Set S) = Set.univ
⊢ Function.Surjective.{u + 1, v + 1} (α := R[X]) (β := S) (⇑(aeval α) : (a : R[X]) → S)
have rw₃ : (↑⊤ : Set S) = Set.univ
Tactic: rw [← Set.range_eq_univ, ← AlgHom.coe_range, ← Algebra.adjoin_singleton_eq_range_aeval,
      hα₂, Algebra.coe_top]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X]
h : IsAdjoinRoot S f
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsTorsionFree R S
inst_6 : IsIntegrallyClosed R
α : S
hα : IsIntegral R α
hα₂ : Eq (α := Subalgebra R S) R[α] ⊤
rw : Eq.{v + 1} (α := Set S) (Set.range.{v, u + 1} (ι := R[X]) (⇑(aeval α) : (a : R[X]) → S)) Set.univ
rw₁ : (↑(AlgHom.range (aeval α)) : Set S) = Set.univ
rw₂ : (↑R[α] : Set S) = Set.univ
rw₃ : (↑⊤ : Set S) = Set.univ
⊢ Function.Surjective.{u + 1, v + 1} (α := R[X]) (β := S) (⇑(aeval α) : (a : R[X]) → S)
have rw₄ : Eq.{v + 1} (α := Set S) Set.univ Set.univ
Tactic: rw [← Set.range_eq_univ, ← AlgHom.coe_range, ← Algebra.adjoin_singleton_eq_range_aeval,
      hα₂, Algebra.coe_top]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X]
h : IsAdjoinRoot S f
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsTorsionFree R S
inst_6 : IsIntegrallyClosed R
α : S
hα : IsIntegral R α
hα₂ : Eq (α := Subalgebra R S) R[α] ⊤
⊢ Eq (α := Ideal R[X]) (RingHom.ker (F := R[X] →ₐ[R] S) (aeval α)) (Ideal.span {minpoly R α})
have h₁ : ∀ (x : R[X]),
  Membership.mem (γ := Ideal R[X]) (RingHom.ker (F := R[X] →ₐ[R] S) (aeval α)) x ↔
    Membership.mem (γ := Ideal R[X]) (Ideal.span {minpoly R α}) x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X]
h : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
h' : IsAdjoinRoot T f
U : Type u_2
inst_5 : CommRing U
i : R →+* U
x : U
hx : eval₂ i x f = 0
z : S
⊢ Eq.{u_2 + 1} (α := U) ((h'.lift i x hx : (a : T) → U) ((h.algEquiv h' : (a : S) → T) z : T) : U)
    ((h.lift i x hx : (a : S) → U) z : U)
have rw : Eq.{u_2 + 1} (α := U)
  ((h'.lift i x hx : (a : T) → U) ((h.algEquiv h' : (a : S) → T) ((h.map : (a : R[X]) → S) (h.repr z) : S) : T) : U)
  ((h.lift i x hx : (a : S) → U) ((h.map : (a : R[X]) → S) (h.repr z) : S) : U)
Tactic: rw [← h.map_repr z]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X]
h : IsAdjoinRootMonic S f
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsTorsionFree R S
inst_6 : IsIntegrallyClosed R
hirr : Irreducible f
q : R[X]
hq : f = minpoly R h.root * q
⊢ Associated f (minpoly R h.root)
have h₁ : minpoly R h.root = HMul.hMul (α := R[X]) (minpoly R h.root) 1
Tactic: convert!
        Associated.mul_left (minpoly R h.root) <|
          associated_one_iff_isUnit.2 <|
            (hirr.isUnit_or_isUnit hq).resolve_left <| minpoly.not_isUnit R h.root
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R[X]
h : IsAdjoinRootMonic S f
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsTorsionFree R S
inst_6 : IsIntegrallyClosed R
hirr : Irreducible f
q : R[X]
hq : f = minpoly R h.root * q
⊢ minpoly R h.root = HMul.hMul (α := R[X]) (minpoly R h.root) 1
have h₁ : Eq (α := R[X]) (minpoly R h.root) (minpoly R h.root)
Tactic: rw [mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f_1 : R[X]
h : IsAdjoinRootMonic S f_1
inst_3 : Module.Finite R S
inst_4 : Free R S
α : S
hα : Eq (α := Subalgebra R S) R[α] ⊤
f : R[X] := minpoly R α
hf : Monic (minpoly R α)
φ : AdjoinRoot f →ₐ[R] S := AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α ⋯
⊢ Function.Surjective.{u + 1, v + 1} (α := AdjoinRoot f) (β := S) (⇑φ : (a : AdjoinRoot f) → S)
have rw : ∀ (hα : Function.Surjective.{u + 1, v + 1} (α := R[X]) (β := S) (⇑(aeval α) : (a : R[X]) → S)),
  let f : R[X] := minpoly R α;
  ∀ (hf : Monic (minpoly R α)),
    let φ := AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α sorry;
    Function.Surjective.{u + 1, v + 1} (α := AdjoinRoot f) (β := S) (⇑φ : (a : AdjoinRoot f) → S)
Tactic: rw [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at hα
Cleared hypotheses: hα, f, hf, φ
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f_1 : R[X]
h : IsAdjoinRootMonic S f_1
inst_3 : Module.Finite R S
inst_4 : Free R S
α : S
hα : Function.Surjective.{u + 1, v + 1} (α := R[X]) (β := S) (⇑(aeval α) : (a : R[X]) → S)
f : R[X] := minpoly R α
hf : Monic (minpoly R α)
φ : AdjoinRoot f →ₐ[R] S := AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α ⋯
s : S
⊢ ∃ (a : AdjoinRoot f), (φ : (a : AdjoinRoot f) → S) a = s
have obtain : ∀ (p : R[X]) (hp : (aeval α : (a : R[X]) → S) p = s), ∃ (a : AdjoinRoot f), (φ : (a : AdjoinRoot f) → S) a = s
Tactic: obtain ⟨p, hp⟩ := hα s
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f_1 : R[X]
h : IsAdjoinRootMonic S f_1
inst_3 : Module.Finite R S
inst_4 : Free R S
α : S
hα : Eq (α := Subalgebra R S) R[α] ⊤
f : R[X] := minpoly R α
hf : Monic (minpoly R α)
φ : AdjoinRoot f →ₐ[R] S := AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α ⋯
⊢ Function.Bijective.{u + 1, v + 1} (α := AdjoinRoot (minpoly R α)) (β := S) (⇑φ : (a : AdjoinRoot (minpoly R α)) → S)
have hφ : Function.Surjective.{u + 1, v + 1} (α := AdjoinRoot f) (β := S) (⇑φ : (a : AdjoinRoot f) → S)
Tactic: have hφ : Function.Surjective φ := by
        rw [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at hα
        intro s; obtain ⟨p, hp⟩ := hα s
        exact ⟨AdjoinRoot.mk f p, by simp [φ, ← aeval_def, hp]⟩
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f_1 : R[X]
h : IsAdjoinRootMonic S f_1
inst_3 : Module.Finite R S
inst_4 : Free R S
α : S
hα : Eq (α := Subalgebra R S) R[α] ⊤
f : R[X] := minpoly R α
hf : Monic (minpoly R α)
φ : AdjoinRoot f →ₐ[R] S := AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α ⋯
hφ : Function.Surjective.{u + 1, v + 1} (α := AdjoinRoot f) (β := S) (⇑φ : (a : AdjoinRoot f) → S)
⊢ Function.Bijective.{u + 1, v + 1} (α := AdjoinRoot (minpoly R α)) (β := S) (⇑φ : (a : AdjoinRoot (minpoly R α)) → S)
have this : Free R (AdjoinRoot (minpoly R α))
Tactic: haveI := hf.free_adjoinRoot
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f_1 : R[X]
h : IsAdjoinRootMonic S f_1
inst_3 : Module.Finite R S
inst_4 : Free R S
α : S
hα : Eq (α := Subalgebra R S) R[α] ⊤
f : R[X] := minpoly R α
hf : Monic (minpoly R α)
φ : AdjoinRoot f →ₐ[R] S := AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α ⋯
hφ : Function.Surjective.{u + 1, v + 1} (α := AdjoinRoot f) (β := S) (⇑φ : (a : AdjoinRoot f) → S)
this : Free R (AdjoinRoot (minpoly R α))
⊢ Function.Bijective.{u + 1, v + 1} (α := AdjoinRoot (minpoly R α)) (β := S) (⇑φ : (a : AdjoinRoot (minpoly R α)) → S)
have this₁ : Module.Finite R (AdjoinRoot (minpoly R α))
Tactic: haveI := hf.finite_adjoinRoot
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f_1 : R[X]
h : IsAdjoinRootMonic S f_1
inst_3 : Module.Finite R S
inst_4 : Free R S
α : S
hα : Eq (α := Subalgebra R S) R[α] ⊤
f : R[X] := minpoly R α
hf : Monic (minpoly R α)
φ : AdjoinRoot f →ₐ[R] S := AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α ⋯
hφ : Function.Surjective.{u + 1, v + 1} (α := AdjoinRoot f) (β := S) (⇑φ : (a : AdjoinRoot f) → S)
this_1 : Free R (AdjoinRoot (minpoly R α))
this : Module.Finite R (AdjoinRoot (minpoly R α))
⊢ Function.Bijective.{u + 1, v + 1} (α := AdjoinRoot (minpoly R α)) (β := S) (⇑φ : (a : AdjoinRoot (minpoly R α)) → S)
have pos : ∀ (h : Nontrivial R),
  Function.Bijective.{u + 1, v + 1} (α := AdjoinRoot (minpoly R α)) (β := S) (⇑φ : (a : AdjoinRoot (minpoly R α)) → S)
Tactic: by_cases h : Nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f_1 : R[X]
h : IsAdjoinRootMonic S f_1
inst_3 : Module.Finite R S
inst_4 : Free R S
α : S
hα : Eq (α := Subalgebra R S) R[α] ⊤
f : R[X] := minpoly R α
hf : Monic (minpoly R α)
φ : AdjoinRoot f →ₐ[R] S := AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α ⋯
hφ : Function.Surjective.{u + 1, v + 1} (α := AdjoinRoot f) (β := S) (⇑φ : (a : AdjoinRoot f) → S)
this_1 : Free R (AdjoinRoot (minpoly R α))
this : Module.Finite R (AdjoinRoot (minpoly R α))
pos :
  ∀ (h : Nontrivial R),
    Function.Bijective.{u + 1, v + 1} (α := AdjoinRoot (minpoly R α)) (β := S) (⇑φ : (a : AdjoinRoot (minpoly R α)) → S)
⊢ Function.Bijective.{u + 1, v + 1} (α := AdjoinRoot (minpoly R α)) (β := S) (⇑φ : (a : AdjoinRoot (minpoly R α)) → S)
have neg : ∀ (h : ¬Nontrivial R),
  Function.Bijective.{u + 1, v + 1} (α := AdjoinRoot (minpoly R α)) (β := S) (⇑φ : (a : AdjoinRoot (minpoly R α)) → S)
Tactic: by_cases h : Nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f_1 : R[X]
h_1 : IsAdjoinRootMonic S f_1
inst_3 : Module.Finite R S
inst_4 : Free R S
α : S
hα : Eq (α := Subalgebra R S) R[α] ⊤
f : R[X] := minpoly R α
hf : Monic (minpoly R α)
φ : AdjoinRoot f →ₐ[R] S := AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α ⋯
hφ : Function.Surjective.{u + 1, v + 1} (α := AdjoinRoot f) (β := S) (⇑φ : (a : AdjoinRoot f) → S)
this_1 : Free R (AdjoinRoot (minpoly R α))
this : Module.Finite R (AdjoinRoot (minpoly R α))
h : ¬Nontrivial R
⊢ Function.Bijective.{u + 1, v + 1} (α := AdjoinRoot (minpoly R α)) (β := S) (⇑φ : (a : AdjoinRoot (minpoly R α)) → S)
have h₁ : Subsingleton R
Tactic: apply not_nontrivial_iff_subsingleton.mp at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f_1 : R[X]
h_1 : IsAdjoinRootMonic S f_1
inst_3 : Module.Finite R S
inst_4 : Free R S
α : S
hα : Eq (α := Subalgebra R S) R[α] ⊤
f : R[X] := minpoly R α
hf : Monic (minpoly R α)
φ : AdjoinRoot f →ₐ[R] S := AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α ⋯
hφ : Function.Surjective.{u + 1, v + 1} (α := AdjoinRoot f) (β := S) (⇑φ : (a : AdjoinRoot f) → S)
this_1 : Free R (AdjoinRoot (minpoly R α))
this : Module.Finite R (AdjoinRoot (minpoly R α))
h : Subsingleton R
⊢ Function.Bijective.{u + 1, v + 1} (α := AdjoinRoot (minpoly R α)) (β := S) (⇑φ : (a : AdjoinRoot (minpoly R α)) → S)
have this₁ : Subsingleton.{u + 1} (AdjoinRoot f)
Tactic: haveI := Module.subsingleton R (AdjoinRoot f)
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsTorsionFree R S
inst_6 : IsIntegrallyClosed R
x : S
hx' : IsIntegral R x
⊢ Eq (α := R[X]) (minpoly R x) (minpoly R (powerBasis' hx').gen)
have this : IsDomain.{u} (AdjoinRoot (minpoly R x))
Tactic: have := isDomain_of_prime (prime_of_isIntegrallyClosed hx')