awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
f : R[X]
inst_1 : DistribSMul S R
inst_2 : IsScalarTower S R R
a : S
x : R
rw :
  HSMul.hSMul (β := AdjoinRoot f) a (((mk f).comp C : (a : R) → AdjoinRoot f) x : AdjoinRoot f) =
    ((mk f).comp C : (a : R) → AdjoinRoot f) (a • x)
rw₁ :
  HSMul.hSMul (β := AdjoinRoot f) a ((mk f : (a : R[X]) → AdjoinRoot f) ((C : (a : R) → R[X]) x) : AdjoinRoot f) =
    ((mk f).comp C : (a : R) → AdjoinRoot f) (a • x)
rw₂ :
  HSMul.hSMul (β := AdjoinRoot f) a ((mk f : (a : R[X]) → AdjoinRoot f) ((C : (a : R) → R[X]) x) : AdjoinRoot f) =
    (mk f : (a : R[X]) → AdjoinRoot f) ((C : (a : R) → R[X]) (a • x))
rw₃ :
  Eq (α := AdjoinRoot f)
    ((mk f : (a : R[X]) → AdjoinRoot f) (HSMul.hSMul (β := R[X]) a ((C : (a : R) → R[X]) x : R[X])) : AdjoinRoot f)
    ((mk f : (a : R[X]) → AdjoinRoot f) ((C : (a : R) → R[X]) (a • x)) : AdjoinRoot f)
⊢ HSMul.hSMul (β := AdjoinRoot f) a ((of f : (a : R) → AdjoinRoot f) x : AdjoinRoot f) =
    (of f : (a : R) → AdjoinRoot f) (a • x)
have rw₄ : Eq (α := AdjoinRoot f) ((mk f : (a : R[X]) → AdjoinRoot f) ((C : (a : R) → R[X]) (a • x)) : AdjoinRoot f)
  ((mk f : (a : R[X]) → AdjoinRoot f) ((C : (a : R) → R[X]) (a • x)) : AdjoinRoot f)
Tactic: rw [of, RingHom.comp_apply, RingHom.comp_apply, smul_mk, smul_C]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
T : Type u_3
inst : CommRing R
inst_1 : Semiring T
p : R[X]
f g : RingHom.{u_1, u_3} (AdjoinRoot p) T
hAlg : f.comp (of p) = g.comp (of p)
hRoot : Eq.{u_3 + 1} (α := T) ((f : (a : AdjoinRoot p) → T) (root p) : T) ((g : (a : AdjoinRoot p) → T) (root p) : T)
⊢ f = g
have h : f.comp (Ideal.Quotient.mk (span {p})) = g.comp (Ideal.Quotient.mk (span {p}))
Tactic: apply Ideal.Quotient.ringHom_ext
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
T : Type u_3
inst : CommRing R
inst_1 : Semiring T
p : R[X]
f g : RingHom.{u_1, u_3} (AdjoinRoot p) T
hAlg : f.comp (of p) = g.comp (of p)
hRoot : Eq.{u_3 + 1} (α := T) ((f : (a : AdjoinRoot p) → T) (root p) : T) ((g : (a : AdjoinRoot p) → T) (root p) : T)
⊢ f.comp (Ideal.Quotient.mk (span {p})) = g.comp (Ideal.Quotient.mk (span {p}))
have h : ∀ (x : R),
  Eq.{u_3 + 1} (α := T) (((f.comp (Ideal.Quotient.mk (span {p}))).comp C : (a : R) → T) x : T)
    (((g.comp (Ideal.Quotient.mk (span {p}))).comp C : (a : R) → T) x : T)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
T : Type u_3
inst : CommRing R
inst_1 : Semiring T
p : R[X]
f g : RingHom.{u_1, u_3} (AdjoinRoot p) T
hAlg : f.comp (of p) = g.comp (of p)
hRoot : Eq.{u_3 + 1} (α := T) ((f : (a : AdjoinRoot p) → T) (root p) : T) ((g : (a : AdjoinRoot p) → T) (root p) : T)
h :
  ∀ (x : R),
    Eq.{u_3 + 1} (α := T) (((f.comp (Ideal.Quotient.mk (span {p}))).comp C : (a : R) → T) x : T)
      (((g.comp (Ideal.Quotient.mk (span {p}))).comp C : (a : R) → T) x : T)
⊢ f.comp (Ideal.Quotient.mk (span {p})) = g.comp (Ideal.Quotient.mk (span {p}))
have h₁ : Eq.{u_3 + 1} (α := T) ((f.comp (Ideal.Quotient.mk (span {p})) : (a : R[X]) → T) X : T)
  ((g.comp (Ideal.Quotient.mk (span {p})) : (a : R[X]) → T) X : T)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommSemiring S
inst_2 : Semiring T
inst_3 : Algebra S R
inst_4 : Algebra S T
p : R[X]
f g : AlgHom.{u_2, u_1, u_3} S (AdjoinRoot p) T
hAlg : f.comp (ofAlgHom S p) = g.comp (ofAlgHom S p)
hRoot : Eq.{u_3 + 1} (α := T) ((f : (a : AdjoinRoot p) → T) (root p) : T) ((g : (a : AdjoinRoot p) → T) (root p) : T)
⊢ f = g
have a : Eq (α := RingHom.{u_1, u_3} (AdjoinRoot p) T) (↑f : AdjoinRoot p →+* T) (↑g : AdjoinRoot p →+* T)
Tactic: apply AlgHom.coe_ringHom_injective
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
⊢ f ∣ g - 0 ↔ f ∣ g
have rw : f ∣ g ↔ f ∣ g
Tactic: rw [sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : S[X]
a : R
⊢ Eq.{u_2 + 1} (α := AdjoinRoot f)
    ((aeval (root f) : (a : R[X]) → AdjoinRoot f) ((C : (a : R) → R[X]) a) : AdjoinRoot f)
    ((mk f : (a : S[X]) → AdjoinRoot f) (Polynomial.map (algebraMap R S) ((C : (a : R) → R[X]) a)) : AdjoinRoot f)
have C : Eq.{u_2 + 1} (α := AdjoinRoot f) ((algebraMap R (AdjoinRoot f) : (a : R) → AdjoinRoot f) a : AdjoinRoot f)
  ((of f : (a : S) → AdjoinRoot f) ((algebraMap R S : (a : R) → S) a) : AdjoinRoot f)
Tactic: simp only [Polynomial.aeval_C, Polynomial.map_C, mk_C]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : S[X]
a : R
⊢ Eq.{u_2 + 1} (α := AdjoinRoot f) ((algebraMap R (AdjoinRoot f) : (a : R) → AdjoinRoot f) a : AdjoinRoot f)
    ((of f : (a : S) → AdjoinRoot f) ((algebraMap R S : (a : R) → S) a) : AdjoinRoot f)
have C : Eq (α := AdjoinRoot f)
  ((algebraMap S (AdjoinRoot f) : (a : S) → AdjoinRoot f) ((algebraMap R S : (a : R) → S) a) : AdjoinRoot f)
  ((of f : (a : S) → AdjoinRoot f) ((algebraMap R S : (a : R) → S) a) : AdjoinRoot f)
Tactic: rw [IsScalarTower.algebraMap_apply R S]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : S[X]
p : R[X]
⊢ Eq.{u_2 + 1} (α := AdjoinRoot f) ((aeval (root f) : (a : R[X]) → AdjoinRoot f) p : AdjoinRoot f)
    ((mk f : (a : S[X]) → AdjoinRoot f) (Polynomial.map (algebraMap R S) p) : AdjoinRoot f)
have C : ∀ (a : R),
  Eq.{u_2 + 1} (α := AdjoinRoot f)
    ((aeval (root f) : (a : R[X]) → AdjoinRoot f) ((C : (a : R) → R[X]) a) : AdjoinRoot f)
    ((mk f : (a : S[X]) → AdjoinRoot f) (Polynomial.map (algebraMap R S) ((C : (a : R) → R[X]) a)) : AdjoinRoot f)
Tactic: induction p using Polynomial.induction_on with
  | C a =>
    simp only [Polynomial.aeval_C, Polynomial.map_C, mk_C]
    rw [IsScalarTower.algebraMap_apply R S]
    simp
  | add p q _ _ => simp_all
  | monomial n a _ => simp_all [pow_add, ← mul_assoc]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : S[X]
p : R[X]
C :
  ∀ (a : R),
    Eq.{u_2 + 1} (α := AdjoinRoot f)
      ((aeval (root f) : (a : R[X]) → AdjoinRoot f) ((Polynomial.C : (a : R) → R[X]) a) : AdjoinRoot f)
      ((mk f : (a : S[X]) → AdjoinRoot f) (Polynomial.map (algebraMap R S) ((Polynomial.C : (a : R) → R[X]) a)) :
        AdjoinRoot f)
⊢ Eq.{u_2 + 1} (α := AdjoinRoot f) ((aeval (root f) : (a : R[X]) → AdjoinRoot f) p : AdjoinRoot f)
    ((mk f : (a : S[X]) → AdjoinRoot f) (Polynomial.map (algebraMap R S) p) : AdjoinRoot f)
have add : ∀ (p q : R[X]),
  Eq.{u_2 + 1} (α := AdjoinRoot f) ((aeval (root f) : (a : R[X]) → AdjoinRoot f) p : AdjoinRoot f)
      ((mk f : (a : S[X]) → AdjoinRoot f) (Polynomial.map (algebraMap R S) p) : AdjoinRoot f) →
    Eq.{u_2 + 1} (α := AdjoinRoot f) ((aeval (root f) : (a : R[X]) → AdjoinRoot f) q : AdjoinRoot f)
        ((mk f : (a : S[X]) → AdjoinRoot f) (Polynomial.map (algebraMap R S) q) : AdjoinRoot f) →
      Eq.{u_2 + 1} (α := AdjoinRoot f) ((aeval (root f) : (a : R[X]) → AdjoinRoot f) (p + q) : AdjoinRoot f)
        ((mk f : (a : S[X]) → AdjoinRoot f) (Polynomial.map (algebraMap R S) (p + q)) : AdjoinRoot f)
Tactic: induction p using Polynomial.induction_on with
  | C a =>
    simp only [Polynomial.aeval_C, Polynomial.map_C, mk_C]
    rw [IsScalarTower.algebraMap_apply R S]
    simp
  | add p q _ _ => simp_all
  | monomial n a _ => simp_all [pow_add, ← mul_assoc]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : S[X]
p : R[X]
C :
  ∀ (a : R),
    Eq.{u_2 + 1} (α := AdjoinRoot f)
      ((aeval (root f) : (a : R[X]) → AdjoinRoot f) ((Polynomial.C : (a : R) → R[X]) a) : AdjoinRoot f)
      ((mk f : (a : S[X]) → AdjoinRoot f) (Polynomial.map (algebraMap R S) ((Polynomial.C : (a : R) → R[X]) a)) :
        AdjoinRoot f)
add :
  ∀ (p q : R[X]),
    Eq.{u_2 + 1} (α := AdjoinRoot f) ((aeval (root f) : (a : R[X]) → AdjoinRoot f) p : AdjoinRoot f)
        ((mk f : (a : S[X]) → AdjoinRoot f) (Polynomial.map (algebraMap R S) p) : AdjoinRoot f) →
      Eq.{u_2 + 1} (α := AdjoinRoot f) ((aeval (root f) : (a : R[X]) → AdjoinRoot f) q : AdjoinRoot f)
          ((mk f : (a : S[X]) → AdjoinRoot f) (Polynomial.map (algebraMap R S) q) : AdjoinRoot f) →
        Eq.{u_2 + 1} (α := AdjoinRoot f) ((aeval (root f) : (a : R[X]) → AdjoinRoot f) (p + q) : AdjoinRoot f)
          ((mk f : (a : S[X]) → AdjoinRoot f) (Polynomial.map (algebraMap R S) (p + q)) : AdjoinRoot f)
⊢ Eq.{u_2 + 1} (α := AdjoinRoot f) ((aeval (root f) : (a : R[X]) → AdjoinRoot f) p : AdjoinRoot f)
    ((mk f : (a : S[X]) → AdjoinRoot f) (Polynomial.map (algebraMap R S) p) : AdjoinRoot f)
have monomial : ∀ (n : ℕ) (a : R),
  Eq.{u_2 + 1} (α := AdjoinRoot f)
      ((aeval (root f) : (a : R[X]) → AdjoinRoot f)
          (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) :
        AdjoinRoot f)
      ((mk f : (a : S[X]) → AdjoinRoot f)
          (Polynomial.map (algebraMap R S)
            (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))) :
        AdjoinRoot f) →
    Eq.{u_2 + 1} (α := AdjoinRoot f)
      ((aeval (root f) : (a : R[X]) → AdjoinRoot f)
          (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))) :
        AdjoinRoot f)
      ((mk f : (a : S[X]) → AdjoinRoot f)
          (Polynomial.map (algebraMap R S)
            (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))) :
        AdjoinRoot f)
Tactic: induction p using Polynomial.induction_on with
  | C a =>
    simp only [Polynomial.aeval_C, Polynomial.map_C, mk_C]
    rw [IsScalarTower.algebraMap_apply R S]
    simp
  | add p q _ _ => simp_all
  | monomial n a _ => simp_all [pow_add, ← mul_assoc]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
inst : CommRing R
f p : R[X]
⊢ Eq (α := AdjoinRoot f) ((aeval (root f) : (a : R[X]) → AdjoinRoot f) p : AdjoinRoot f)
    ((mk f : (a : R[X]) → AdjoinRoot f) p : AdjoinRoot f)
have rw : Eq (α := AdjoinRoot f) ((mk f : (a : R[X]) → AdjoinRoot f) (Polynomial.map (algebraMap R R) p) : AdjoinRoot f)
  ((mk f : (a : R[X]) → AdjoinRoot f) p : AdjoinRoot f)
Tactic: rw [aeval_eq_of_algebra, Algebra.algebraMap_self, Polynomial.map_id]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
inst : CommRing R
f p : R[X]
rw :
  Eq (α := AdjoinRoot f) ((mk f : (a : R[X]) → AdjoinRoot f) (Polynomial.map (algebraMap R R) p) : AdjoinRoot f)
    ((mk f : (a : R[X]) → AdjoinRoot f) p : AdjoinRoot f)
⊢ Eq (α := AdjoinRoot f) ((aeval (root f) : (a : R[X]) → AdjoinRoot f) p : AdjoinRoot f)
    ((mk f : (a : R[X]) → AdjoinRoot f) p : AdjoinRoot f)
have rw₁ : Eq (α := AdjoinRoot f) ((mk f : (a : R[X]) → AdjoinRoot f) (Polynomial.map (RingHom.id R) p) : AdjoinRoot f)
  ((mk f : (a : R[X]) → AdjoinRoot f) p : AdjoinRoot f)
Tactic: rw [aeval_eq_of_algebra, Algebra.algebraMap_self, Polynomial.map_id]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
inst : CommRing R
f p : R[X]
rw :
  Eq (α := AdjoinRoot f) ((mk f : (a : R[X]) → AdjoinRoot f) (Polynomial.map (algebraMap R R) p) : AdjoinRoot f)
    ((mk f : (a : R[X]) → AdjoinRoot f) p : AdjoinRoot f)
rw₁ :
  Eq (α := AdjoinRoot f) ((mk f : (a : R[X]) → AdjoinRoot f) (Polynomial.map (RingHom.id R) p) : AdjoinRoot f)
    ((mk f : (a : R[X]) → AdjoinRoot f) p : AdjoinRoot f)
⊢ Eq (α := AdjoinRoot f) ((aeval (root f) : (a : R[X]) → AdjoinRoot f) p : AdjoinRoot f)
    ((mk f : (a : R[X]) → AdjoinRoot f) p : AdjoinRoot f)
have rw₂ : Eq (α := AdjoinRoot f) ((mk f : (a : R[X]) → AdjoinRoot f) p : AdjoinRoot f)
  ((mk f : (a : R[X]) → AdjoinRoot f) p : AdjoinRoot f)
Tactic: rw [aeval_eq_of_algebra, Algebra.algebraMap_self, Polynomial.map_id]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
⊢ Eq (α := Subalgebra R (AdjoinRoot f)) R[root f] ⊤
have refine : ∀ (x : AdjoinRoot f), Membership.mem (γ := Subalgebra R (AdjoinRoot f)) R[root f] x
Tactic: refine Algebra.eq_top_iff.2 fun x => ?_
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
x : AdjoinRoot f
⊢ Membership.mem (γ := Subalgebra R (AdjoinRoot f)) R[root f] x
have ih : ∀ (p : R[X]),
  Membership.mem (α := AdjoinRoot f) (γ := Subalgebra R (AdjoinRoot f)) R[root f]
    ((mk f : (a : R[X]) → AdjoinRoot f) p : AdjoinRoot f)
Tactic: induction x using AdjoinRoot.induction_on with
    | ih p => exact (Algebra.adjoin_singleton_eq_range_aeval R (root f)).symm ▸ ⟨p, aeval_eq p⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
⊢ eval₂ (of f) (root f) f = 0
have rw : eval₂ (algebraMap R (AdjoinRoot f)) (root f) f = 0
Tactic: rw [← algebraMap_eq, ← aeval_def, aeval_eq, mk_self]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
rw : eval₂ (algebraMap R (AdjoinRoot f)) (root f) f = 0
⊢ eval₂ (of f) (root f) f = 0
have rw₁ : Eq (α := AdjoinRoot f) ((aeval (root f) : (a : R[X]) → AdjoinRoot f) f) 0
Tactic: rw [← algebraMap_eq, ← aeval_def, aeval_eq, mk_self]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
rw : eval₂ (algebraMap R (AdjoinRoot f)) (root f) f = 0
rw₁ : Eq (α := AdjoinRoot f) ((aeval (root f) : (a : R[X]) → AdjoinRoot f) f) 0
⊢ eval₂ (of f) (root f) f = 0
have rw₂ : Eq (α := AdjoinRoot f) ((mk f : (a : R[X]) → AdjoinRoot f) f) 0
Tactic: rw [← algebraMap_eq, ← aeval_def, aeval_eq, mk_self]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
rw : eval₂ (algebraMap R (AdjoinRoot f)) (root f) f = 0
rw₁ : Eq (α := AdjoinRoot f) ((aeval (root f) : (a : R[X]) → AdjoinRoot f) f) 0
rw₂ : Eq (α := AdjoinRoot f) ((mk f : (a : R[X]) → AdjoinRoot f) f) 0
⊢ eval₂ (of f) (root f) f = 0
have rw₃ : Eq.{u_1 + 1} (α := AdjoinRoot f) 0 0
Tactic: rw [← algebraMap_eq, ← aeval_def, aeval_eq, mk_self]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
⊢ (Polynomial.map (of f) f).IsRoot (root f)
have rw : eval (root f) (Polynomial.map (of f) f) = 0
Tactic: rw [IsRoot, eval_map, eval₂_root]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
rw : eval (root f) (Polynomial.map (of f) f) = 0
⊢ (Polynomial.map (of f) f).IsRoot (root f)
have rw₁ : eval₂ (of f) (root f) f = 0
Tactic: rw [IsRoot, eval_map, eval₂_root]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
rw : eval (root f) (Polynomial.map (of f) f) = 0
rw₁ : eval₂ (of f) (root f) f = 0
⊢ (Polynomial.map (of f) f).IsRoot (root f)
have rw₂ : Eq.{u_1 + 1} (α := AdjoinRoot f) 0 0
Tactic: rw [IsRoot, eval_map, eval₂_root]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.degree ≠ 0
⊢ Function.Injective (α := R) (β := AdjoinRoot f) (⇑(of f) : (a : R) → AdjoinRoot f)
have rw : ∀ (a : R), Eq (α := AdjoinRoot f) ((of f : (a : R) → AdjoinRoot f) a : AdjoinRoot f) (0 : AdjoinRoot f) → a = 0
Tactic: rw [injective_iff_map_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.degree ≠ 0
p : R
hp : Eq (α := AdjoinRoot f) ((of f : (a : R) → AdjoinRoot f) p : AdjoinRoot f) (0 : AdjoinRoot f)
⊢ p = 0
have hp₁ : f ∣ (C : (a : R) → R[X]) p
Tactic: rw [AdjoinRoot.of, RingHom.comp_apply, AdjoinRoot.mk_eq_zero] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.degree ≠ 0
p : R
hp : f ∣ (C : (a : R) → R[X]) p
⊢ p = 0
have pos : ∀ (h : f = 0), p = 0
Tactic: by_cases h : f = 0
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.degree ≠ 0
p : R
hp : f ∣ (C : (a : R) → R[X]) p
pos : ∀ (h : f = 0), p = 0
⊢ p = 0
have neg : ∀ (h : ¬f = 0), p = 0
Tactic: by_cases h : f = 0
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.degree ≠ 0
p : R
hp : f ∣ (C : (a : R) → R[X]) p
h : f = 0
⊢ Dvd.dvd (α := R[X]) (0 : R[X]) ((C : (a : R) → R[X]) p : R[X])
have rwa : ∀ (hp : Dvd.dvd (α := R[X]) (0 : R[X]) ((C : (a : R) → R[X]) p : R[X])) (h : f = 0),
  Dvd.dvd (α := R[X]) (0 : R[X]) ((C : (a : R) → R[X]) p : R[X])
Tactic: rwa [h] at hp
Cleared hypotheses: hp, h
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.degree ≠ 0
p : R
hp : f ∣ (C : (a : R) → R[X]) p
h : ¬f = 0
⊢ p = 0
have neg : ∀ (h_contra : p ≠ 0), f.degree = 0
Tactic: contrapose! hf with h_contra
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
p : R
hp : f ∣ (C : (a : R) → R[X]) p
h : ¬f = 0
h_contra : p ≠ 0
⊢ f.degree = 0
have neg : f.degree = degree.{u_1} (R := R) ((C : (a : R) → R[X]) p)
Tactic: rw [← degree_C h_contra]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
p : R
hp : f ∣ (C : (a : R) → R[X]) p
h : ¬f = 0
h_contra : p ≠ 0
⊢ Ne (α := R[X]) ((C : (a : R) → R[X]) p : R[X]) (0 : R[X])
have rwa : ¬Eq (α := R[X]) ((C : (a : R) → R[X]) p : R[X]) (0 : R[X])
Tactic: rwa [Ne, C_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
p : R
hp : f ∣ (C : (a : R) → R[X]) p
h : ¬f = 0
h_contra : p ≠ 0
rwa : ¬Eq (α := R[X]) ((C : (a : R) → R[X]) p : R[X]) (0 : R[X])
⊢ Ne (α := R[X]) ((C : (a : R) → R[X]) p : R[X]) (0 : R[X])
have rwa₁ : ¬p = 0
Tactic: rwa [Ne, C_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
p : R
hp : f ∣ (C : (a : R) → R[X]) p
h : ¬f = 0
h_contra : p ≠ 0
⊢ f.degree = degree.{u_1} (R := R) ((C : (a : R) → R[X]) p)
have apply : degree.{u_1} (R := R) ((C : (a : R) → R[X]) p) ≤ f.degree
Tactic: apply le_antisymm (degree_le_of_dvd hp (by rwa [Ne, C_eq_zero])) _
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
p : R
hp : f ∣ (C : (a : R) → R[X]) p
h : ¬f = 0
h_contra : p ≠ 0
⊢ degree.{u_1} (R := R) ((C : (a : R) → R[X]) p) ≤ f.degree
have rwa : 0 ≤ f.degree
Tactic: rwa [degree_C h_contra, zero_le_degree_iff]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
p : R
hp : f ∣ (C : (a : R) → R[X]) p
h : ¬f = 0
h_contra : p ≠ 0
rwa : 0 ≤ f.degree
⊢ degree.{u_1} (R := R) ((C : (a : R) → R[X]) p) ≤ f.degree
have rwa₁ : f ≠ 0
Tactic: rwa [degree_C h_contra, zero_le_degree_iff]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f g : R[X]
inst_1 : CommRing S
i : R →+* S
x : S
h : eval₂ i x f = 0
⊢ RingHom.{u_1, u_2} (AdjoinRoot f) S
have apply : ∀ (a : R[X]),
  Membership.mem (γ := Ideal R[X]) (span {f}) a →
    Eq.{u_2 + 1} (α := S) ((eval₂RingHom i x : (a : R[X]) → S) a : S) (0 : S)
Tactic: apply Ideal.Quotient.lift _ (eval₂RingHom i x)
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f g_1 : R[X]
inst_1 : CommRing S
i : R →+* S
x : S
h : eval₂ i x f = 0
g : R[X]
H : Membership.mem (γ := Ideal R[X]) (span {f}) g
⊢ Eq.{u_2 + 1} (α := S) ((eval₂RingHom i x : (a : R[X]) → S) g : S) (0 : S)
have rcases : ∀ (y : R[X]) (hy : g = f * y), Eq.{u_2 + 1} (α := S) ((eval₂RingHom i x : (a : R[X]) → S) g : S) (0 : S)
Tactic: rcases mem_span_singleton.1 H with ⟨y, hy⟩
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f g_1 : R[X]
inst_1 : CommRing S
i : R →+* S
x : S
h : eval₂ i x f = 0
g : R[X]
H : Membership.mem (γ := Ideal R[X]) (span {f}) g
y : R[X]
hy : g = f * y
⊢ Eq.{u_2 + 1} (α := S) ((eval₂RingHom i x : (a : R[X]) → S) g : S) (0 : S)
have rw : Eq.{u_2 + 1} (α := S) ((eval₂RingHom i x : (a : R[X]) → S) (f * y) : S) (0 : S)
Tactic: rw [hy, map_mul, coe_eval₂RingHom, h, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f g_1 : R[X]
inst_1 : CommRing S
i : R →+* S
x : S
h : eval₂ i x f = 0
g : R[X]
H : Membership.mem (γ := Ideal R[X]) (span {f}) g
y : R[X]
hy : g = f * y
rw : Eq.{u_2 + 1} (α := S) ((eval₂RingHom i x : (a : R[X]) → S) (f * y) : S) (0 : S)
⊢ Eq.{u_2 + 1} (α := S) ((eval₂RingHom i x : (a : R[X]) → S) g : S) (0 : S)
have rw₁ : HMul.hMul (α := S) (β := S) ((eval₂RingHom i x : (a : R[X]) → S) f : S) ((eval₂RingHom i x : (a : R[X]) → S) y : S) = 0
Tactic: rw [hy, map_mul, coe_eval₂RingHom, h, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f g_1 : R[X]
inst_1 : CommRing S
i : R →+* S
x : S
h : eval₂ i x f = 0
g : R[X]
H : Membership.mem (γ := Ideal R[X]) (span {f}) g
y : R[X]
hy : g = f * y
rw : Eq.{u_2 + 1} (α := S) ((eval₂RingHom i x : (a : R[X]) → S) (f * y) : S) (0 : S)
rw₁ :
  HMul.hMul (α := S) (β := S) ((eval₂RingHom i x : (a : R[X]) → S) f : S) ((eval₂RingHom i x : (a : R[X]) → S) y : S) =
    0
⊢ Eq.{u_2 + 1} (α := S) ((eval₂RingHom i x : (a : R[X]) → S) g : S) (0 : S)
have rw₂ : eval₂ i x f * eval₂ i x y = 0
Tactic: rw [hy, map_mul, coe_eval₂RingHom, h, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f g_1 : R[X]
inst_1 : CommRing S
i : R →+* S
x : S
h : eval₂ i x f = 0
g : R[X]
H : Membership.mem (γ := Ideal R[X]) (span {f}) g
y : R[X]
hy : g = f * y
rw : Eq.{u_2 + 1} (α := S) ((eval₂RingHom i x : (a : R[X]) → S) (f * y) : S) (0 : S)
rw₁ :
  HMul.hMul (α := S) (β := S) ((eval₂RingHom i x : (a : R[X]) → S) f : S) ((eval₂RingHom i x : (a : R[X]) → S) y : S) =
    0
rw₂ : eval₂ i x f * eval₂ i x y = 0
⊢ Eq.{u_2 + 1} (α := S) ((eval₂RingHom i x : (a : R[X]) → S) g : S) (0 : S)
have rw₃ : 0 * eval₂ i x y = 0
Tactic: rw [hy, map_mul, coe_eval₂RingHom, h, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
f g_1 : R[X]
inst_1 : CommRing S
i : R →+* S
x : S
h : eval₂ i x f = 0
g : R[X]
H : Membership.mem (γ := Ideal R[X]) (span {f}) g
y : R[X]
hy : g = f * y
rw : Eq.{u_2 + 1} (α := S) ((eval₂RingHom i x : (a : R[X]) → S) (f * y) : S) (0 : S)
rw₁ :
  HMul.hMul (α := S) (β := S) ((eval₂RingHom i x : (a : R[X]) → S) f : S) ((eval₂RingHom i x : (a : R[X]) → S) y : S) =
    0
rw₂ : eval₂ i x f * eval₂ i x y = 0
rw₃ : 0 * eval₂ i x y = 0
⊢ Eq.{u_2 + 1} (α := S) ((eval₂RingHom i x : (a : R[X]) → S) g : S) (0 : S)
have rw₄ : Eq.{u_2 + 1} (α := S) 0 0
Tactic: rw [hy, map_mul, coe_eval₂RingHom, h, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
f : R[X]
inst_1 : CommRing S
i : R →+* S
a : S
h : eval₂ i a f = 0
⊢ (lift i a h : (a : AdjoinRoot f) → S) (root f) = a
have rw : (lift i a h : (a : AdjoinRoot f) → S) ((mk f : (a : R[X]) → AdjoinRoot f) X) = a
Tactic: rw [root, lift_mk, eval₂_X]