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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : Ring T
inst_4 : Algebra R T
U : Type u_2
inst_5 : Ring U
inst_6 : Algebra R U
h'' : IsAdjoinRoot U f
e : S ≃ₐ[R] T
⊢ (h.ofAlgEquiv e).algEquiv h'' = e.symm.trans (h.algEquiv h'')
have h₁ : ∀ (a : T),
  Eq.{u_2 + 1} (α := U) (((h.ofAlgEquiv e).algEquiv h'' : (a : T) → U) a : U)
    ((e.symm.trans (h.algEquiv h'') : (a : T) → U) a : U)
Tactic: ext a
-- 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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : Ring T
inst_4 : Algebra R T
U : Type u_2
inst_5 : Ring U
inst_6 : Algebra R U
h'' : IsAdjoinRoot U f
e : S ≃ₐ[R] T
a : T
⊢ Eq.{u_2 + 1} (α := U) (((h.ofAlgEquiv e).algEquiv h'' : (a : T) → U) a : U)
    ((e.symm.trans (h.algEquiv h'') : (a : T) → U) a : U)
have h₁ : Eq.{u_2 + 1} (α := U) (((h.ofAlgEquiv e).adjoinRootAlgEquiv.symm.trans h''.adjoinRootAlgEquiv : (a : T) → U) a : U)
  ((e.symm.trans (h.adjoinRootAlgEquiv.symm.trans h''.adjoinRootAlgEquiv) : (a : T) → U) a : U)
Tactic: simp_rw [algEquiv_def, AlgEquiv.trans_apply, EmbeddingLike.apply_eq_iff_eq,
           AlgEquiv.symm_apply_eq, adjoinRootAlgEquiv_apply_eq_map, ofAlgEquiv_map_apply,
           ← adjoinRootAlgEquiv_apply_eq_map, AlgEquiv.apply_symm_apply]
-- 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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : Ring T
inst_4 : Algebra R T
U : Type u_2
inst_5 : Ring U
inst_6 : Algebra R U
h'' : IsAdjoinRoot U f
e : S ≃ₐ[R] T
a : T
h₁ :
  Eq.{u_2 + 1} (α := U) (((h.ofAlgEquiv e).adjoinRootAlgEquiv.symm.trans h''.adjoinRootAlgEquiv : (a : T) → U) a : U)
    ((e.symm.trans (h.adjoinRootAlgEquiv.symm.trans h''.adjoinRootAlgEquiv) : (a : T) → U) a : U)
⊢ Eq.{u_2 + 1} (α := U) (((h.ofAlgEquiv e).algEquiv h'' : (a : T) → U) a : U)
    ((e.symm.trans (h.algEquiv h'') : (a : T) → U) a : U)
have h₂ : Eq.{u_2 + 1} (α := U)
  ((h''.adjoinRootAlgEquiv : (a : AdjoinRoot f) → U)
      (((h.ofAlgEquiv e).adjoinRootAlgEquiv.symm : (a : T) → AdjoinRoot f) a : AdjoinRoot f) :
    U)
  ((h''.adjoinRootAlgEquiv : (a : AdjoinRoot f) → U)
      ((h.adjoinRootAlgEquiv.symm : (a : S) → AdjoinRoot f) ((e.symm : (a : T) → S) a) : AdjoinRoot f) :
    U)
Tactic: simp_rw [algEquiv_def, AlgEquiv.trans_apply, EmbeddingLike.apply_eq_iff_eq,
           AlgEquiv.symm_apply_eq, adjoinRootAlgEquiv_apply_eq_map, ofAlgEquiv_map_apply,
           ← adjoinRootAlgEquiv_apply_eq_map, AlgEquiv.apply_symm_apply]
-- 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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : Ring T
inst_4 : Algebra R T
U : Type u_2
inst_5 : Ring U
inst_6 : Algebra R U
h'' : IsAdjoinRoot U f
e : S ≃ₐ[R] T
a : T
h₁ :
  Eq.{u_2 + 1} (α := U) (((h.ofAlgEquiv e).adjoinRootAlgEquiv.symm.trans h''.adjoinRootAlgEquiv : (a : T) → U) a : U)
    ((e.symm.trans (h.adjoinRootAlgEquiv.symm.trans h''.adjoinRootAlgEquiv) : (a : T) → U) a : U)
h₂ :
  Eq.{u_2 + 1} (α := U)
    ((h''.adjoinRootAlgEquiv : (a : AdjoinRoot f) → U)
        (((h.ofAlgEquiv e).adjoinRootAlgEquiv.symm : (a : T) → AdjoinRoot f) a : AdjoinRoot f) :
      U)
    ((h''.adjoinRootAlgEquiv : (a : AdjoinRoot f) → U)
        ((h.adjoinRootAlgEquiv.symm : (a : S) → AdjoinRoot f) ((e.symm : (a : T) → S) a) : AdjoinRoot f) :
      U)
⊢ Eq.{u_2 + 1} (α := U) (((h.ofAlgEquiv e).algEquiv h'' : (a : T) → U) a : U)
    ((e.symm.trans (h.algEquiv h'') : (a : T) → U) a : U)
have h₃ : Eq.{u + 1} (α := AdjoinRoot f) (((h.ofAlgEquiv e).adjoinRootAlgEquiv.symm : (a : T) → AdjoinRoot f) a : AdjoinRoot f)
  ((h.adjoinRootAlgEquiv.symm : (a : S) → AdjoinRoot f) ((e.symm : (a : T) → S) a) : AdjoinRoot f)
Tactic: simp_rw [algEquiv_def, AlgEquiv.trans_apply, EmbeddingLike.apply_eq_iff_eq,
           AlgEquiv.symm_apply_eq, adjoinRootAlgEquiv_apply_eq_map, ofAlgEquiv_map_apply,
           ← adjoinRootAlgEquiv_apply_eq_map, AlgEquiv.apply_symm_apply]
-- 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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : Ring T
inst_4 : Algebra R T
U : Type u_2
inst_5 : Ring U
inst_6 : Algebra R U
h'' : IsAdjoinRoot U f
e : S ≃ₐ[R] T
a : T
h₁ :
  Eq.{u_2 + 1} (α := U) (((h.ofAlgEquiv e).adjoinRootAlgEquiv.symm.trans h''.adjoinRootAlgEquiv : (a : T) → U) a : U)
    ((e.symm.trans (h.adjoinRootAlgEquiv.symm.trans h''.adjoinRootAlgEquiv) : (a : T) → U) a : U)
h₂ :
  Eq.{u_2 + 1} (α := U)
    ((h''.adjoinRootAlgEquiv : (a : AdjoinRoot f) → U)
        (((h.ofAlgEquiv e).adjoinRootAlgEquiv.symm : (a : T) → AdjoinRoot f) a : AdjoinRoot f) :
      U)
    ((h''.adjoinRootAlgEquiv : (a : AdjoinRoot f) → U)
        ((h.adjoinRootAlgEquiv.symm : (a : S) → AdjoinRoot f) ((e.symm : (a : T) → S) a) : AdjoinRoot f) :
      U)
h₃ :
  Eq.{u + 1} (α := AdjoinRoot f) (((h.ofAlgEquiv e).adjoinRootAlgEquiv.symm : (a : T) → AdjoinRoot f) a : AdjoinRoot f)
    ((h.adjoinRootAlgEquiv.symm : (a : S) → AdjoinRoot f) ((e.symm : (a : T) → S) a) : AdjoinRoot f)
⊢ Eq.{u_2 + 1} (α := U) (((h.ofAlgEquiv e).algEquiv h'' : (a : T) → U) a : U)
    ((e.symm.trans (h.algEquiv h'') : (a : T) → U) a : U)
have h₄ : a =
  ((h.ofAlgEquiv e).adjoinRootAlgEquiv : (a : AdjoinRoot f) → T)
    ((h.adjoinRootAlgEquiv.symm : (a : S) → AdjoinRoot f) ((e.symm : (a : T) → S) a) : AdjoinRoot f)
Tactic: simp_rw [algEquiv_def, AlgEquiv.trans_apply, EmbeddingLike.apply_eq_iff_eq,
           AlgEquiv.symm_apply_eq, adjoinRootAlgEquiv_apply_eq_map, ofAlgEquiv_map_apply,
           ← adjoinRootAlgEquiv_apply_eq_map, AlgEquiv.apply_symm_apply]
-- 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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : Ring T
inst_4 : Algebra R T
U : Type u_2
inst_5 : Ring U
inst_6 : Algebra R U
h'' : IsAdjoinRoot U f
e : S ≃ₐ[R] T
a : T
h₁ :
  Eq.{u_2 + 1} (α := U) (((h.ofAlgEquiv e).adjoinRootAlgEquiv.symm.trans h''.adjoinRootAlgEquiv : (a : T) → U) a : U)
    ((e.symm.trans (h.adjoinRootAlgEquiv.symm.trans h''.adjoinRootAlgEquiv) : (a : T) → U) a : U)
h₂ :
  Eq.{u_2 + 1} (α := U)
    ((h''.adjoinRootAlgEquiv : (a : AdjoinRoot f) → U)
        (((h.ofAlgEquiv e).adjoinRootAlgEquiv.symm : (a : T) → AdjoinRoot f) a : AdjoinRoot f) :
      U)
    ((h''.adjoinRootAlgEquiv : (a : AdjoinRoot f) → U)
        ((h.adjoinRootAlgEquiv.symm : (a : S) → AdjoinRoot f) ((e.symm : (a : T) → S) a) : AdjoinRoot f) :
      U)
h₃ :
  Eq.{u + 1} (α := AdjoinRoot f) (((h.ofAlgEquiv e).adjoinRootAlgEquiv.symm : (a : T) → AdjoinRoot f) a : AdjoinRoot f)
    ((h.adjoinRootAlgEquiv.symm : (a : S) → AdjoinRoot f) ((e.symm : (a : T) → S) a) : AdjoinRoot f)
h₄ :
  a =
    ((h.ofAlgEquiv e).adjoinRootAlgEquiv : (a : AdjoinRoot f) → T)
      ((h.adjoinRootAlgEquiv.symm : (a : S) → AdjoinRoot f) ((e.symm : (a : T) → S) a) : AdjoinRoot f)
⊢ Eq.{u_2 + 1} (α := U) (((h.ofAlgEquiv e).algEquiv h'' : (a : T) → U) a : U)
    ((e.symm.trans (h.algEquiv h'') : (a : T) → U) a : U)
have h₅ : a =
  ((h.ofAlgEquiv e).map : (a : R[X]) → T)
    (Exists.choose (p := fun (a_1 : R[X]) ↦
      Eq (α := AdjoinRoot f) ((AdjoinRoot.mk f : (a : R[X]) → AdjoinRoot f) a_1 : AdjoinRoot f)
        ((h.adjoinRootAlgEquiv.symm : (a : S) → AdjoinRoot f) ((e.symm : (a : T) → S) a) : AdjoinRoot f))
      sorry)
Tactic: simp_rw [algEquiv_def, AlgEquiv.trans_apply, EmbeddingLike.apply_eq_iff_eq,
           AlgEquiv.symm_apply_eq, adjoinRootAlgEquiv_apply_eq_map, ofAlgEquiv_map_apply,
           ← adjoinRootAlgEquiv_apply_eq_map, AlgEquiv.apply_symm_apply]
-- 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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : Ring T
inst_4 : Algebra R T
U : Type u_2
inst_5 : Ring U
inst_6 : Algebra R U
h'' : IsAdjoinRoot U f
e : S ≃ₐ[R] T
a : T
h₁ :
  Eq.{u_2 + 1} (α := U) (((h.ofAlgEquiv e).adjoinRootAlgEquiv.symm.trans h''.adjoinRootAlgEquiv : (a : T) → U) a : U)
    ((e.symm.trans (h.adjoinRootAlgEquiv.symm.trans h''.adjoinRootAlgEquiv) : (a : T) → U) a : U)
h₂ :
  Eq.{u_2 + 1} (α := U)
    ((h''.adjoinRootAlgEquiv : (a : AdjoinRoot f) → U)
        (((h.ofAlgEquiv e).adjoinRootAlgEquiv.symm : (a : T) → AdjoinRoot f) a : AdjoinRoot f) :
      U)
    ((h''.adjoinRootAlgEquiv : (a : AdjoinRoot f) → U)
        ((h.adjoinRootAlgEquiv.symm : (a : S) → AdjoinRoot f) ((e.symm : (a : T) → S) a) : AdjoinRoot f) :
      U)
h₃ :
  Eq.{u + 1} (α := AdjoinRoot f) (((h.ofAlgEquiv e).adjoinRootAlgEquiv.symm : (a : T) → AdjoinRoot f) a : AdjoinRoot f)
    ((h.adjoinRootAlgEquiv.symm : (a : S) → AdjoinRoot f) ((e.symm : (a : T) → S) a) : AdjoinRoot f)
h₄ :
  a =
    ((h.ofAlgEquiv e).adjoinRootAlgEquiv : (a : AdjoinRoot f) → T)
      ((h.adjoinRootAlgEquiv.symm : (a : S) → AdjoinRoot f) ((e.symm : (a : T) → S) a) : AdjoinRoot f)
h₅ :
  a =
    ((h.ofAlgEquiv e).map : (a : R[X]) → T)
      (Exists.choose (p := fun (a_1 : R[X]) ↦
        Eq (α := AdjoinRoot f) ((AdjoinRoot.mk f : (a : R[X]) → AdjoinRoot f) a_1 : AdjoinRoot f)
          ((h.adjoinRootAlgEquiv.symm : (a : S) → AdjoinRoot f) ((e.symm : (a : T) → S) a) : AdjoinRoot f))
        ⋯)
⊢ Eq.{u_2 + 1} (α := U) (((h.ofAlgEquiv e).algEquiv h'' : (a : T) → U) a : U)
    ((e.symm.trans (h.algEquiv h'') : (a : T) → U) a : U)
have h₆ : a =
  (e : (a : S) → T)
    ((h.map : (a : R[X]) → S)
        (Exists.choose (p := fun (a_1 : R[X]) ↦
          Eq (α := AdjoinRoot f) ((AdjoinRoot.mk f : (a : R[X]) → AdjoinRoot f) a_1 : AdjoinRoot f)
            ((h.adjoinRootAlgEquiv.symm : (a : S) → AdjoinRoot f) ((e.symm : (a : T) → S) a) : AdjoinRoot f))
          sorry) :
      S)
Tactic: simp_rw [algEquiv_def, AlgEquiv.trans_apply, EmbeddingLike.apply_eq_iff_eq,
           AlgEquiv.symm_apply_eq, adjoinRootAlgEquiv_apply_eq_map, ofAlgEquiv_map_apply,
           ← adjoinRootAlgEquiv_apply_eq_map, AlgEquiv.apply_symm_apply]
-- 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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : Ring T
inst_4 : Algebra R T
U : Type u_2
inst_5 : Ring U
inst_6 : Algebra R U
h'' : IsAdjoinRoot U f
e : S ≃ₐ[R] T
a : T
h₁ :
  Eq.{u_2 + 1} (α := U) (((h.ofAlgEquiv e).adjoinRootAlgEquiv.symm.trans h''.adjoinRootAlgEquiv : (a : T) → U) a : U)
    ((e.symm.trans (h.adjoinRootAlgEquiv.symm.trans h''.adjoinRootAlgEquiv) : (a : T) → U) a : U)
h₂ :
  Eq.{u_2 + 1} (α := U)
    ((h''.adjoinRootAlgEquiv : (a : AdjoinRoot f) → U)
        (((h.ofAlgEquiv e).adjoinRootAlgEquiv.symm : (a : T) → AdjoinRoot f) a : AdjoinRoot f) :
      U)
    ((h''.adjoinRootAlgEquiv : (a : AdjoinRoot f) → U)
        ((h.adjoinRootAlgEquiv.symm : (a : S) → AdjoinRoot f) ((e.symm : (a : T) → S) a) : AdjoinRoot f) :
      U)
h₃ :
  Eq.{u + 1} (α := AdjoinRoot f) (((h.ofAlgEquiv e).adjoinRootAlgEquiv.symm : (a : T) → AdjoinRoot f) a : AdjoinRoot f)
    ((h.adjoinRootAlgEquiv.symm : (a : S) → AdjoinRoot f) ((e.symm : (a : T) → S) a) : AdjoinRoot f)
h₄ :
  a =
    ((h.ofAlgEquiv e).adjoinRootAlgEquiv : (a : AdjoinRoot f) → T)
      ((h.adjoinRootAlgEquiv.symm : (a : S) → AdjoinRoot f) ((e.symm : (a : T) → S) a) : AdjoinRoot f)
h₅ :
  a =
    ((h.ofAlgEquiv e).map : (a : R[X]) → T)
      (Exists.choose (p := fun (a_1 : R[X]) ↦
        Eq (α := AdjoinRoot f) ((AdjoinRoot.mk f : (a : R[X]) → AdjoinRoot f) a_1 : AdjoinRoot f)
          ((h.adjoinRootAlgEquiv.symm : (a : S) → AdjoinRoot f) ((e.symm : (a : T) → S) a) : AdjoinRoot f))
        ⋯)
h₆ :
  a =
    (e : (a : S) → T)
      ((h.map : (a : R[X]) → S)
          (Exists.choose (p := fun (a_1 : R[X]) ↦
            Eq (α := AdjoinRoot f) ((AdjoinRoot.mk f : (a : R[X]) → AdjoinRoot f) a_1 : AdjoinRoot f)
              ((h.adjoinRootAlgEquiv.symm : (a : S) → AdjoinRoot f) ((e.symm : (a : T) → S) a) : AdjoinRoot f))
            ⋯) :
        S)
⊢ Eq.{u_2 + 1} (α := U) (((h.ofAlgEquiv e).algEquiv h'' : (a : T) → U) a : U)
    ((e.symm.trans (h.algEquiv h'') : (a : T) → U) a : U)
have h₇ : a =
  (e : (a : S) → T)
    ((h.adjoinRootAlgEquiv : (a : AdjoinRoot f) → S)
        ((h.adjoinRootAlgEquiv.symm : (a : S) → AdjoinRoot f) ((e.symm : (a : T) → S) a) : AdjoinRoot f) :
      S)
Tactic: simp_rw [algEquiv_def, AlgEquiv.trans_apply, EmbeddingLike.apply_eq_iff_eq,
           AlgEquiv.symm_apply_eq, adjoinRootAlgEquiv_apply_eq_map, ofAlgEquiv_map_apply,
           ← adjoinRootAlgEquiv_apply_eq_map, AlgEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
z : S
w : R[X]
hzw : (h.map : (a : R[X]) → S) w = z
⊢ eval₂ i x (h.repr z) = eval₂ i x w
have hzw₁ : f ∣ h.repr z - w
Tactic: rw [eq_comm, ← sub_eq_zero, ← h.map_repr z, ← map_sub, h.map_eq_zero_iff] at hzw
Cleared hypotheses: hzw
-- 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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
z : S
w : R[X]
hzw : f ∣ h.repr z - w
⊢ eval₂ i x (h.repr z) = eval₂ i x w
have obtain : ∀ (y : R[X]) (hy : h.repr z - w = f * y), eval₂ i x (h.repr z) = eval₂ i x w
Tactic: obtain ⟨y, hy⟩ := hzw
Cleared hypotheses: hzw
-- 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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
z : S
w y : R[X]
hy : h.repr z - w = f * y
⊢ eval₂ i x (h.repr z) = eval₂ i x w
have rw : eval₂ i x (h.repr z) - eval₂ i x w = 0
Tactic: rw [← sub_eq_zero, ← eval₂_sub, hy, eval₂_mul, hx, zero_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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
z : S
w y : R[X]
hy : h.repr z - w = f * y
rw : eval₂ i x (h.repr z) - eval₂ i x w = 0
⊢ eval₂ i x (h.repr z) = eval₂ i x w
have rw₁ : eval₂ i x (h.repr z - w) = 0
Tactic: rw [← sub_eq_zero, ← eval₂_sub, hy, eval₂_mul, hx, zero_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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
z : S
w y : R[X]
hy : h.repr z - w = f * y
rw : eval₂ i x (h.repr z) - eval₂ i x w = 0
rw₁ : eval₂ i x (h.repr z - w) = 0
⊢ eval₂ i x (h.repr z) = eval₂ i x w
have rw₂ : eval₂ i x (f * y) = 0
Tactic: rw [← sub_eq_zero, ← eval₂_sub, hy, eval₂_mul, hx, zero_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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
z : S
w y : R[X]
hy : h.repr z - w = f * y
rw : eval₂ i x (h.repr z) - eval₂ i x w = 0
rw₁ : eval₂ i x (h.repr z - w) = 0
rw₂ : eval₂ i x (f * y) = 0
⊢ eval₂ i x (h.repr z) = eval₂ i x w
have rw₃ : eval₂ i x f * eval₂ i x y = 0
Tactic: rw [← sub_eq_zero, ← eval₂_sub, hy, eval₂_mul, hx, zero_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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
z : S
w y : R[X]
hy : h.repr z - w = f * y
rw : eval₂ i x (h.repr z) - eval₂ i x w = 0
rw₁ : eval₂ i x (h.repr z - w) = 0
rw₂ : eval₂ i x (f * y) = 0
rw₃ : eval₂ i x f * eval₂ i x y = 0
⊢ eval₂ i x (h.repr z) = eval₂ i x w
have rw₄ : 0 * eval₂ i x y = 0
Tactic: rw [← sub_eq_zero, ← eval₂_sub, hy, eval₂_mul, hx, zero_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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
z : S
w y : R[X]
hy : h.repr z - w = f * y
rw : eval₂ i x (h.repr z) - eval₂ i x w = 0
rw₁ : eval₂ i x (h.repr z - w) = 0
rw₂ : eval₂ i x (f * y) = 0
rw₃ : eval₂ i x f * eval₂ i x y = 0
rw₄ : 0 * eval₂ i x y = 0
⊢ eval₂ i x (h.repr z) = eval₂ i x w
have rw₅ : Eq.{u_1 + 1} (α := T) 0 0
Tactic: rw [← sub_eq_zero, ← eval₂_sub, hy, eval₂_mul, hx, zero_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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
⊢ (h.lift i x hx : (a : S) → T) h.root = x
have rw : (h.lift i x hx : (a : S) → T) ((h.map : (a : R[X]) → S) X : S) = x
Tactic: rw [← h.map_X, lift_map, eval₂_X]
-- 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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
rw : (h.lift i x hx : (a : S) → T) ((h.map : (a : R[X]) → S) X : S) = x
⊢ (h.lift i x hx : (a : S) → T) h.root = x
have rw₁ : eval₂ i x X = x
Tactic: rw [← h.map_X, lift_map, eval₂_X]
-- 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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
rw : (h.lift i x hx : (a : S) → T) ((h.map : (a : R[X]) → S) X : S) = x
rw₁ : eval₂ i x X = x
⊢ (h.lift i x hx : (a : S) → T) h.root = x
have rw₂ : x = x
Tactic: rw [← h.map_X, lift_map, eval₂_X]
-- 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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
g : S →+* T
hmap :
  ∀ (a : R),
    Eq.{u_1 + 1} (α := T) ((g : (a : S) → T) ((algebraMap R S : (a : R) → S) a : S) : T) ((i : (a : R) → T) a : T)
hroot : (g : (a : S) → T) h.root = x
a : S
⊢ Eq.{u_1 + 1} (α := T) ((g : (a : S) → T) a : T) ((h.lift i x hx : (a : S) → T) a : T)
have rw : Eq.{u_1 + 1} (α := T)
  ((g : (a : S) → T)
      ((h.map : (a : R[X]) → S)
          (∑ i ∈ Finset.range ((h.repr a).natDegree + 1),
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((h.repr a).coeff i) : R[X]) (HPow.hPow (α := R[X]) X i)) :
        S) :
    T)
  ((h.lift i x hx : (a : S) → T)
      ((h.map : (a : R[X]) → S)
          (∑ i ∈ Finset.range ((h.repr a).natDegree + 1),
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((h.repr a).coeff i) : R[X]) (HPow.hPow (α := R[X]) X i)) :
        S) :
    T)
Tactic: rw [← h.map_repr a, Polynomial.as_sum_range_C_mul_X_pow (h.repr a)]
-- 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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
x : T
inst_4 : Algebra R T
hx' : Eq.{u_1 + 1} (α := T) ((aeval x : (a : R[X]) → T) f : T) (0 : T)
z : R[X]
⊢ Eq.{u_1 + 1} (α := T) ((h.liftHom x hx' : (a : S) → T) ((h.map : (a : R[X]) → S) z : S) : T)
    ((aeval x : (a : R[X]) → T) z : T)
have rw : Eq.{u_1 + 1} (α := T) ((h.lift (algebraMap R T) x hx' : (a : S) → T) ((h.map : (a : R[X]) → S) z : S) : T)
  ((aeval x : (a : R[X]) → T) z : T)
Tactic: rw [← lift_algebraMap_apply, lift_map, aeval_def]
-- 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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
x : T
inst_4 : Algebra R T
hx' : Eq.{u_1 + 1} (α := T) ((aeval x : (a : R[X]) → T) f : T) (0 : T)
z : R[X]
rw :
  Eq.{u_1 + 1} (α := T) ((h.lift (algebraMap R T) x hx' : (a : S) → T) ((h.map : (a : R[X]) → S) z : S) : T)
    ((aeval x : (a : R[X]) → T) z : T)
⊢ Eq.{u_1 + 1} (α := T) ((h.liftHom x hx' : (a : S) → T) ((h.map : (a : R[X]) → S) z : S) : T)
    ((aeval x : (a : R[X]) → T) z : T)
have rw₁ : eval₂ (algebraMap R T) x z = (aeval x : (a : R[X]) → T) z
Tactic: rw [← lift_algebraMap_apply, lift_map, aeval_def]
-- 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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
x : T
inst_4 : Algebra R T
hx' : Eq.{u_1 + 1} (α := T) ((aeval x : (a : R[X]) → T) f : T) (0 : T)
z : R[X]
rw :
  Eq.{u_1 + 1} (α := T) ((h.lift (algebraMap R T) x hx' : (a : S) → T) ((h.map : (a : R[X]) → S) z : S) : T)
    ((aeval x : (a : R[X]) → T) z : T)
rw₁ : eval₂ (algebraMap R T) x z = (aeval x : (a : R[X]) → T) z
⊢ Eq.{u_1 + 1} (α := T) ((h.liftHom x hx' : (a : S) → T) ((h.map : (a : R[X]) → S) z : S) : T)
    ((aeval x : (a : R[X]) → T) z : T)
have rw₂ : eval₂ (algebraMap R T) x z = eval₂ (algebraMap R T) x z
Tactic: rw [← lift_algebraMap_apply, lift_map, aeval_def]
-- 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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
x : T
inst_4 : Algebra R T
hx' : Eq.{u_1 + 1} (α := T) ((aeval x : (a : R[X]) → T) f : T) (0 : T)
⊢ (h.liftHom x hx' : (a : S) → T) h.root = x
have rw : (h.lift (algebraMap R T) x hx' : (a : S) → T) h.root = x
Tactic: rw [← lift_algebraMap_apply, lift_root]
-- 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 : IsAdjoinRoot S f
T : Type u_1
inst_3 : CommRing T
x : T
inst_4 : Algebra R T
hx' : Eq.{u_1 + 1} (α := T) ((aeval x : (a : R[X]) → T) f : T) (0 : T)
rw : (h.lift (algebraMap R T) x hx' : (a : S) → T) h.root = x
⊢ (h.liftHom x hx' : (a : S) → T) h.root = x
have rw₁ : x = x
Tactic: rw [← lift_algebraMap_apply, lift_root]
-- 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
⊢ Eq (α := Ideal R[X]) (RingHom.ker (mkₐ f)) (Ideal.span {f})
have h : ∀ (x : R[X]),
  Membership.mem (γ := Ideal R[X]) (RingHom.ker (mkₐ f)) x ↔ Membership.mem (γ := Ideal R[X]) (Ideal.span {f}) x
Tactic: ext
-- 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
g : R[X]
⊢ Eq.{v + 1} (α := S) ((h.map : (a : R[X]) → S) (g %ₘ f) : S) ((h.map : (a : R[X]) → S) g : S)
have rw : f ∣ f * (g /ₘ f)
Tactic: rw [← RingHom.sub_mem_ker_iff, mem_ker_map, modByMonic_eq_sub_mul_div, sub_right_comm,
    sub_self, zero_sub, dvd_neg]
-- 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
g : R[X]
⊢ f ∣ h.repr ((h.map : (a : R[X]) → S) g) - g
have rw : Membership.mem (γ := Ideal R[X]) (RingHom.ker h.map) (h.repr ((h.map : (a : R[X]) → S) g) - g)
Tactic: rw [← h.mem_ker_map, RingHom.sub_mem_ker_iff, map_repr]
-- 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
g : R[X]
rw : Membership.mem (γ := Ideal R[X]) (RingHom.ker h.map) (h.repr ((h.map : (a : R[X]) → S) g) - g)
⊢ f ∣ h.repr ((h.map : (a : R[X]) → S) g) - g
have rw₁ : Eq.{v + 1} (α := S) ((h.map : (a : R[X]) → S) (h.repr ((h.map : (a : R[X]) → S) g)) : S)
  ((h.map : (a : R[X]) → S) g : S)
Tactic: rw [← h.mem_ker_map, RingHom.sub_mem_ker_iff, map_repr]