awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AdjoinRoot
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)
rw₂ rw₃ :
  Eq (α := AdjoinRoot f) ((mk f : (a : R[X]) → AdjoinRoot f) 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)

Tactic:
rw [aeval_eq_of_algebra, Algebra.algebraMap_self, Polynomial.map_id]

Premises used: Algebra.algebraMap_self, AdjoinRoot.aeval_eq_of_algebra, Polynomial.map_id
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
⊢ Eq (α := Subalgebra R (AdjoinRoot f)) R[root f] ⊤

Tactic:
Algebra.eq_top_iff.2 fun x => ?_

Premises used: Iff.mpr, Algebra.eq_top_iff
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
refine : ∀ (x : AdjoinRoot f), Membership.mem (γ := Subalgebra R (AdjoinRoot f)) R[root f] x
⊢ Eq (α := Subalgebra R (AdjoinRoot f)) R[root f] ⊤

Tactic:
refine Algebra.eq_top_iff.2 fun x => ?_

Premises used: Iff.mpr, Algebra.eq_top_iff
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
f 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:
(Algebra.adjoin_singleton_eq_range_aeval R (root f)).symm ▸ ⟨p, aeval_eq p⟩

Premises used: Eq.rec, Algebra.adjoin_singleton_eq_range_aeval, AdjoinRoot.root, Exists.intro, AdjoinRoot.aeval_eq, Eq.symm
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
f 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:
exact (Algebra.adjoin_singleton_eq_range_aeval R (root f)).symm ▸ ⟨p, aeval_eq p⟩
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
x : AdjoinRoot f
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)
⊢ Membership.mem (γ := Subalgebra R (AdjoinRoot f)) R[root f] x

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⟩
-- Module: Mathlib.RingTheory.AdjoinRoot
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
rw₃ rw₄ : Eq.{u_1 + 1} (α := AdjoinRoot f) 0 0
⊢ eval₂ (of f) (root f) f = 0

Tactic:
rw [← algebraMap_eq, ← aeval_def, aeval_eq, mk_self]

Premises used: AdjoinRoot.algebraMap_eq, Polynomial.aeval_def, AdjoinRoot.aeval_eq, AdjoinRoot.mk_self
-- Module: Mathlib.RingTheory.AdjoinRoot
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
rw₂ rw₃ : Eq.{u_1 + 1} (α := AdjoinRoot f) 0 0
⊢ (Polynomial.map (of f) f).IsRoot (root f)

Tactic:
rw [IsRoot, eval_map, eval₂_root]

Premises used: Polynomial.eval_map, Polynomial.IsRoot, AdjoinRoot.eval₂_root
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f ≠ 0
⊢ IsAlgebraic R (root f)

Tactic:
⟨f, hf, eval₂_root f⟩

Premises used: IsAlgebraic, AdjoinRoot.eval₂_root, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.degree ≠ 0
rw : ∀ (a : R), Eq (α := AdjoinRoot f) ((of f : (a : R) → AdjoinRoot f) a : AdjoinRoot f) (0 : AdjoinRoot f) → a = 0
⊢ Function.Injective (α := R) (β := AdjoinRoot f) (⇑(of f) : (a : R) → AdjoinRoot f)

Tactic:
rw [injective_iff_map_eq_zero]

Premises used: injective_iff_map_eq_zero
-- Module: Mathlib.RingTheory.AdjoinRoot
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)
⊢ f ∣ (C : (a : R) → R[X]) p

Tactic:
rw [AdjoinRoot.of, RingHom.comp_apply, AdjoinRoot.mk_eq_zero] at hp

Premises used: AdjoinRoot.mk_eq_zero, RingHom.comp_apply, AdjoinRoot.of
-- Module: Mathlib.RingTheory.AdjoinRoot
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
neg : ∀ (h : ¬f = 0), p = 0
⊢ p = 0

Tactic:
by_cases h : f = 0
-- Module: Mathlib.RingTheory.AdjoinRoot
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
rwa rwa₁ rwa₂ 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])
⊢ Dvd.dvd (α := R[X]) (0 : R[X]) ((C : (a : R) → R[X]) p : R[X])

Tactic:
rwa [h] at hp
-- Module: Mathlib.RingTheory.AdjoinRoot
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

Tactic:
exact C_eq_zero.mp (eq_zero_of_zero_dvd (by rwa [h] at hp))

Premises used: Polynomial.C_eq_zero, Iff.mp
-- Module: Mathlib.RingTheory.AdjoinRoot
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
neg : ∀ (h_contra : p ≠ 0), f.degree = 0
⊢ p = 0

Tactic:
contrapose! hf with h_contra
-- Module: Mathlib.RingTheory.AdjoinRoot
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
neg : f.degree = degree.{u_1} (R := R) ((C : (a : R) → R[X]) p)
⊢ f.degree = 0

Tactic:
rw [← degree_C h_contra]

Premises used: Polynomial.degree_C
-- Module: Mathlib.RingTheory.AdjoinRoot
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])
rwa₁ rwa₂ rwa₃ rwa₄ : ¬p = 0
⊢ Ne (α := R[X]) ((C : (a : R) → R[X]) p : R[X]) (0 : R[X])

Tactic:
rwa [Ne, C_eq_zero]

Premises used: Polynomial.C_eq_zero, Ne
-- Module: Mathlib.RingTheory.AdjoinRoot
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
apply : degree.{u_1} (R := R) ((C : (a : R) → R[X]) p) ≤ f.degree
⊢ f.degree = degree.{u_1} (R := R) ((C : (a : R) → R[X]) p)

Tactic:
apply le_antisymm (degree_le_of_dvd hp (by rwa [Ne, C_eq_zero])) _

Premises used: Polynomial.degree_le_of_dvd, le_antisymm
-- Module: Mathlib.RingTheory.AdjoinRoot
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
rwa₁ rwa₂ rwa₃ rwa₄ : f ≠ 0
⊢ degree.{u_1} (R := R) ((C : (a : R) → R[X]) p) ≤ f.degree

Tactic:
rwa [degree_C h_contra, zero_le_degree_iff]

Premises used: Polynomial.zero_le_degree_iff, Polynomial.degree_C
-- Module: Mathlib.RingTheory.AdjoinRoot
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
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)
⊢ RingHom.{u_1, u_2} (AdjoinRoot f) S

Tactic:
apply Ideal.Quotient.lift _ (eval₂RingHom i x)

Premises used: Polynomial.eval₂RingHom, Ideal.Quotient.lift
-- Module: Mathlib.RingTheory.AdjoinRoot
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
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)
⊢ 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⟩

Premises used: Iff.mp, Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.AdjoinRoot
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
rw₄ rw₅ : Eq.{u_2 + 1} (α := S) 0 0
⊢ Eq.{u_2 + 1} (α := S) ((eval₂RingHom i x : (a : R[X]) → S) g : S) (0 : S)

Tactic:
rw [hy, map_mul, coe_eval₂RingHom, h, zero_mul]

Premises used: MulZeroClass.zero_mul, map_mul, Polynomial.coe_eval₂RingHom
-- Module: Mathlib.RingTheory.AdjoinRoot
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
g : R[X]
⊢ (lift i a h : (a : AdjoinRoot f) → S) ((mk f : (a : R[X]) → AdjoinRoot f) g : AdjoinRoot f) = eval₂ i a g

Tactic:
Ideal.Quotient.lift_mk _ _ _

Premises used: Ideal.Quotient.lift_mk
-- Module: Mathlib.RingTheory.AdjoinRoot
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
rw : (lift i a h : (a : AdjoinRoot f) → S) ((mk f : (a : R[X]) → AdjoinRoot f) X) = a
rw₁ : eval₂ i a X = a
rw₂ rw₃ : a = a
⊢ (lift i a h : (a : AdjoinRoot f) → S) (root f) = a

Tactic:
rw [root, lift_mk, eval₂_X]

Premises used: AdjoinRoot.lift_mk, Polynomial.eval₂_X, AdjoinRoot.root
-- Module: Mathlib.RingTheory.AdjoinRoot
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
x : R
rw :
  Eq.{u_2 + 1} (α := S)
    ((lift i a h : (a : AdjoinRoot f) → S)
        ((mk f : (a : R[X]) → AdjoinRoot f) ((C : (a : R) → R[X]) x) : AdjoinRoot f) :
      S)
    ((i : (a : R) → S) x : S)
rw₁ : eval₂ i a ((C : (a : R) → R[X]) x) = (i : (a : R) → S) x
rw₂ rw₃ : Eq.{u_2 + 1} (α := S) ((i : (a : R) → S) x : S) ((i : (a : R) → S) x : S)
⊢ Eq.{u_2 + 1} (α := S) ((lift i a h : (a : AdjoinRoot f) → S) ((of f : (a : R) → AdjoinRoot f) x : AdjoinRoot f) : S)
    ((i : (a : R) → S) x : S)

Tactic:
rw [← mk_C x, lift_mk, eval₂_C]

Premises used: AdjoinRoot.lift_mk, Polynomial.eval₂_C, AdjoinRoot.mk_C
-- Module: Mathlib.RingTheory.AdjoinRoot
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).comp (of f) = i

Tactic:
RingHom.ext fun _ => @lift_of _ _ _ _ _ _ _ h _

Premises used: RingHom.ext, AdjoinRoot.lift_of
-- Module: Mathlib.RingTheory.AdjoinRoot
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_1 : R →+* S
a : S
h_1 : eval₂ i_1 a f = 0
inst_2 : CommRing T
inst_3 : Algebra S R
inst_4 : Algebra S T
p : R[X]
i : R →ₐ[S] T
x : T
h : eval₂ (↑i : R →+* T) x p = 0
r : S
⊢ (↑(↑(lift i.toRingHom x h) : AdjoinRoot p →* T) : OneHom (AdjoinRoot p) T).toFun
      ((algebraMap S (AdjoinRoot p) : (a : S) → AdjoinRoot p) r) =
    (algebraMap S T : (a : S) → T) r

Tactic:
simp [lift_of h, AdjoinRoot.algebraMap_eq']

Premises used: AdjoinRoot.algebraMap_eq', AdjoinRoot.lift_of
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra S R
inst_4 : Algebra S T
p : R[X]
i : R →ₐ[S] T
x : T
h : eval₂ (↑i : R →+* T) x p = 0
⊢ (↑(liftAlgHom p i x h) : AdjoinRoot p →+* T) = lift i.toRingHom x h

Tactic:
rfl

Premises used: AdjoinRoot, Quotient.liftOn', Set.Mem, AddCon.liftOn, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, Ideal.Quotient.lift, Submodule.quotientRel, AddAction.orbitRel, AdjoinRoot.lift, AddCon.Quotient, rfl
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra S R
inst_4 : Algebra S T
p : R[X]
i : R →ₐ[S] T
x : T
h : eval₂ (↑i : R →+* T) x p = 0
⊢ Eq (α := (a : AdjoinRoot p) → T) (⇑(liftAlgHom p i x h) : (a : AdjoinRoot p) → T)
    (⇑(lift i.toRingHom x h) : (a : AdjoinRoot p) → T)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra S R
inst_4 : Algebra S T
p : R[X]
i : R →ₐ[S] T
x : T
h : eval₂ (↑i : R →+* T) x p = 0
r : R
⊢ Eq.{u_3 + 1} (α := T)
    ((liftAlgHom p i x h : (a : AdjoinRoot p) → T) ((of p : (a : R) → AdjoinRoot p) r : AdjoinRoot p) : T)
    ((i : (a : R) → T) r : T)

Tactic:
simp [liftAlgHom]

Premises used: AdjoinRoot.liftAlgHom
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra S R
inst_4 : Algebra S T
p : R[X]
i : R →ₐ[S] T
x : T
h : eval₂ (↑i : R →+* T) x p = 0
f : R[X]
⊢ (liftAlgHom p i x h : (a : AdjoinRoot p) → T) ((mk p : (a : R[X]) → AdjoinRoot p) f : AdjoinRoot p) =
    eval₂ (↑i : R →+* T) x f

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, rfl
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra S R
inst_4 : Algebra S T
p : R[X]
i : R →ₐ[S] T
x : T
h : eval₂ (↑i : R →+* T) x p = 0
⊢ (liftAlgHom p i x h : (a : AdjoinRoot p) → T) (root p) = x

Tactic:
simp [liftAlgHom]

Premises used: AdjoinRoot.liftAlgHom
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
f : R[X]
inst_1 : CommRing S
inst_2 : Algebra R S
ϕ : AdjoinRoot f →ₐ[R] S
⊢ ϕ.comp (of f) = algebraMap R S

Tactic:
have h : ϕ.toRingHom.comp (of f) = algebraMap R S := RingHom.ext_iff.mpr ϕ.commutes
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
f : R[X]
inst_1 : CommRing S
inst_2 : Algebra R S
ϕ : AdjoinRoot f →ₐ[R] S
h : ϕ.comp (of f) = algebraMap R S
rw :
  eval₂ (ϕ.comp (of f)) ((ϕ : (a : AdjoinRoot f) → S) (root f)) f =
    eval₂ (ϕ.comp (of f)) ((ϕ.toRingHom : (a : AdjoinRoot f) → S) (root f)) f
⊢ Eq.{u_2 + 1} (α := S) (((aeval ((ϕ : (a : AdjoinRoot f) → S) (root f)) : R[X] →ₐ[R] S) : (a : R[X]) → S) f : S)
    (0 : S)

Tactic:
rw [aeval_def, ← h, ← map_zero ϕ.toRingHom, ← eval₂_root f, hom_eval₂]

Premises used: Polynomial.hom_eval₂, map_zero, Polynomial.aeval_def, AdjoinRoot.eval₂_root, AlgHom.toRingHom
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
f : R[X]
inst_1 : CommRing S
inst_2 : Algebra R S
ϕ : AdjoinRoot f →ₐ[R] S
h : ϕ.comp (of f) = algebraMap R S
⊢ eval₂ (ϕ.comp (of f)) ((ϕ : (a : AdjoinRoot f) → S) (root f)) f =
    eval₂ (ϕ.comp (of f)) ((ϕ.toRingHom : (a : AdjoinRoot f) → S) (root f)) f

Tactic:
rfl
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
f : R[X]
inst_1 : CommRing S
inst_2 : Algebra R S
ϕ : AdjoinRoot f →ₐ[R] S
h :
  Eq.{u_2 + 1} (α := S)
    ((liftAlgHom f (Algebra.ofId R S) ((ϕ : (a : AdjoinRoot f) → S) (root f)) ⋯ : (a : AdjoinRoot f) → S) (root f) : S)
    ((ϕ : (a : AdjoinRoot f) → S) (root f) : S)
⊢ liftAlgHom f (Algebra.ofId R S) ((ϕ : (a : AdjoinRoot f) → S) (root f)) ⋯ = ϕ

Tactic:
ext
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
f : R[X]
inst_1 : CommRing S
inst_2 : Algebra R S
ϕ : AdjoinRoot f →ₐ[R] S
⊢ Eq.{u_2 + 1} (α := S)
    ((liftAlgHom f (Algebra.ofId R S) ((ϕ : (a : AdjoinRoot f) → S) (root f)) ⋯ : (a : AdjoinRoot f) → S) (root f) : S)
    ((ϕ : (a : AdjoinRoot f) → S) (root f) : S)

Tactic:
simp
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
r : R
⊢ eval₂ (of (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))
      (root (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X) =
    eval₂ (of (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))
      (root (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1)) 1

Tactic:
sub_eq_zero.1 ((eval₂_sub _).symm.trans <| eval₂_root <| C r * X - 1)

Premises used: Polynomial.C, HMul.hMul, sub_eq_zero, HSub.hSub, Polynomial.eval₂_sub, AdjoinRoot.eval₂_root, Iff.mp, OfNat.ofNat, Eq.symm, Polynomial.X, DFunLike.coe, Eq.trans
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
r : R
h :
  HMul.hMul (α := AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))
      ((of (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1) :
            (a : R) → AdjoinRoot ((C : (a : R) → R[X]) r * X - 1))
          r :
        AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))
      (root (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1)) =
    eval₂ (of (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))
      (root (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X)
h₁ :
  1 =
    eval₂ (of (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))
      (root (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1)) 1
⊢ HMul.hMul (α := AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))
      ((of (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1) :
            (a : R) → AdjoinRoot ((C : (a : R) → R[X]) r * X - 1))
          r :
        AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))
      (root (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1)) =
    1

Tactic:
convert! sub_eq_zero.1 ((eval₂_sub _).symm.trans <| eval₂_root <| C r * X - 1)

Premises used: Polynomial.C, HMul.hMul, sub_eq_zero, HSub.hSub, Polynomial.eval₂_sub, AdjoinRoot.eval₂_root, Iff.mp, OfNat.ofNat, Eq.symm, Polynomial.X, DFunLike.coe, Eq.trans
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
r : R
⊢ HMul.hMul (α := AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))
      ((of (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1) :
            (a : R) → AdjoinRoot ((C : (a : R) → R[X]) r * X - 1))
          r :
        AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))
      (root (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1)) =
    eval₂ (of (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))
      (root (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X)

Tactic:
simp only [eval₂_mul, eval₂_C, eval₂_X, eval₂_one]

Premises used: Polynomial.eval₂_one, Polynomial.eval₂_mul, Polynomial.eval₂_X, Polynomial.eval₂_C
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
r : R
⊢ 1 =
    eval₂ (of (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))
      (root (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1)) 1

Tactic:
simp only [eval₂_mul, eval₂_C, eval₂_X, eval₂_one]

Premises used: Polynomial.eval₂_one, Polynomial.eval₂_mul, Polynomial.eval₂_X, Polynomial.eval₂_C
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u_1
inst : CommRing R
S : Type u_6
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
f g : AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1) →ₐ[R] S
rw :
  HMul.hMul (α := S) (β := S)
      ((f : (a : AdjoinRoot ((C : (a : R) → R[X]) r * X - 1)) → S)
          ((algebraMap R (AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1)) :
                (a : R) → AdjoinRoot ((C : (a : R) → R[X]) r * X - 1))
              r :
            AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1)) :
        S)
      ((f : (a : AdjoinRoot ((C : (a : R) → R[X]) r * X - 1)) → S)
          (root (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1)) :
        S) =
    1
rw₁ :
  Eq.{u_6 + 1} (α := S)
    ((f : (a : AdjoinRoot ((C : (a : R) → R[X]) r * X - 1)) → S)
        (HMul.hMul (α := AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))
          ((algebraMap R (AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1)) :
                (a : R) → AdjoinRoot ((C : (a : R) → R[X]) r * X - 1))
              r :
            AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))
          (root (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))) :
      S)
    (1 : S)
rw₂ :
  Eq.{u_6 + 1} (α := S)
    ((f : (a : AdjoinRoot ((C : (a : R) → R[X]) r * X - 1)) → S)
        (HMul.hMul (α := AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))
          ((of (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1) :
                (a : R) → AdjoinRoot ((C : (a : R) → R[X]) r * X - 1))
              r :
            AdjoinRoot (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))
          (root (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1))) :
      S)
    (1 : S)
rw₃ : Eq.{u_6 + 1} (α := S) ((f : (a : AdjoinRoot ((C : (a : R) → R[X]) r * X - 1)) → S) 1 : S) (1 : S)
rw₄ rw₅ : Eq.{u_6 + 1} (α := S) 1 1
⊢ HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) r : S)
      ((f : (a : AdjoinRoot ((C : (a : R) → R[X]) r * X - 1)) → S)
          (root (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X - 1)) :
        S) =
    1

Tactic:
rw [← f.commutes, ← map_mul, algebraMap_eq, root_isInv, map_one]

Premises used: AdjoinRoot.algebraMap_eq, AdjoinRoot.root_isInv, map_mul, map_one, AlgHom.commutes