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 : 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
⊢ (lift i a h : (a : AdjoinRoot f) → S) (root f) = a
have rw₁ : eval₂ i a X = a
Tactic: rw [root, lift_mk, eval₂_X]
-- 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
rw : (lift i a h : (a : AdjoinRoot f) → S) ((mk f : (a : R[X]) → AdjoinRoot f) X) = a
rw₁ : eval₂ i a X = a
⊢ (lift i a h : (a : AdjoinRoot f) → S) (root f) = a
have rw₂ : a = a
Tactic: rw [root, lift_mk, eval₂_X]
-- 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
x : R
⊢ 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)
have 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)
Tactic: rw [← mk_C x, lift_mk, eval₂_C]
-- 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
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)
⊢ 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)
have rw₁ : eval₂ i a ((C : (a : R) → R[X]) x) = (i : (a : R) → S) x
Tactic: rw [← mk_C x, lift_mk, eval₂_C]
-- 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
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
⊢ 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)
have rw₂ : Eq.{u_2 + 1} (α := S) ((i : (a : R) → S) x : S) ((i : (a : R) → S) x : S)
Tactic: rw [← mk_C x, lift_mk, eval₂_C]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (hypothesis)
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) (((aeval ((ϕ : (a : AdjoinRoot f) → S) (root f)) : R[X] →ₐ[R] S) : (a : R[X]) → S) f : S)
    (0 : S)
have h : ϕ.comp (of f) = algebraMap R S
Tactic: have h : ϕ.toRingHom.comp (of f) = algebraMap R S := RingHom.ext_iff.mpr ϕ.commutes
-- 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
inst_2 : Algebra R S
ϕ : AdjoinRoot f →ₐ[R] S
h : ϕ.comp (of f) = algebraMap R S
⊢ Eq.{u_2 + 1} (α := S) (((aeval ((ϕ : (a : AdjoinRoot f) → S) (root f)) : R[X] →ₐ[R] S) : (a : R[X]) → S) f : S)
    (0 : S)
have rw : eval₂ (ϕ.comp (of f)) ((ϕ : (a : AdjoinRoot f) → S) (root f)) f =
  eval₂ (ϕ.comp (of f)) ((ϕ.toRingHom : (a : AdjoinRoot f) → S) (root f)) f
Tactic: rw [aeval_def, ← h, ← map_zero ϕ.toRingHom, ← eval₂_root f, hom_eval₂]
-- 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
inst_2 : Algebra R S
ϕ : AdjoinRoot f →ₐ[R] S
⊢ liftAlgHom f (Algebra.ofId R S) ((ϕ : (a : AdjoinRoot f) → S) (root f)) ⋯ = ϕ
have h : Eq.{u_2 + 1} (α := S)
  ((liftAlgHom f (Algebra.ofId R S) ((ϕ : (a : AdjoinRoot f) → S) (root f)) sorry : (a : AdjoinRoot f) → S) (root f) : S)
  ((ϕ : (a : AdjoinRoot f) → S) (root f) : S)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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)) =
    1
have 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)
Tactic: convert! sub_eq_zero.1 ((eval₂_sub _).symm.trans <| eval₂_root <| C r * X - 1)
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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)
⊢ 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
have 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
Tactic: convert! sub_eq_zero.1 ((eval₂_sub _).symm.trans <| eval₂_root <| C r * X - 1)
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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
⊢ 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
have 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
Tactic: rw [← f.commutes, ← map_mul, algebraMap_eq, root_isInv, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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
⊢ 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
have 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)
Tactic: rw [← f.commutes, ← map_mul, algebraMap_eq, root_isInv, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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)
⊢ 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
have 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)
Tactic: rw [← f.commutes, ← map_mul, algebraMap_eq, root_isInv, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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)
⊢ 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
have rw₃ : Eq.{u_6 + 1} (α := S) ((f : (a : AdjoinRoot ((C : (a : R) → R[X]) r * X - 1)) → S) 1 : S) (1 : S)
Tactic: rw [← f.commutes, ← map_mul, algebraMap_eq, root_isInv, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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)
⊢ 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
have rw₄ : Eq.{u_6 + 1} (α := S) 1 1
Tactic: rw [← f.commutes, ← map_mul, algebraMap_eq, root_isInv, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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
⊢ HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) r : S)
      ((g : (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
have rw : HMul.hMul (α := S) (β := S)
    ((g : (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)
    ((g : (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 [← g.commutes, ← map_mul, algebraMap_eq, root_isInv, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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)
      ((g : (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)
      ((g : (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
⊢ HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) r : S)
      ((g : (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
have rw₁ : Eq.{u_6 + 1} (α := S)
  ((g : (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)
Tactic: rw [← g.commutes, ← map_mul, algebraMap_eq, root_isInv, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
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)
      ((g : (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)
      ((g : (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)
    ((g : (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)
⊢ HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) r : S)
      ((g : (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
have rw₂ : Eq.{u_6 + 1} (α := S)
  ((g : (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)
Tactic: rw [← g.commutes, ← map_mul, algebraMap_eq, root_isInv, map_one]