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
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
g : R[X]
pb : PowerBasis R S
h₁ : Eq (α := AdjoinRoot g) ((aeval (root g) : (a : R[X]) → AdjoinRoot g) (minpoly R pb.gen)) 0
h₂ : Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : R[X]) → S) g : S) (0 : S)
h : Nontrivial S
f : R[X]
_hf : f.natDegree < pb.dim
⊢ Eq.{u_2 + 1} (α := S)
    ((liftAlgHom g (Algebra.ofId R S) pb.gen h₂ : (a : AdjoinRoot g) → S)
        ((pb.lift (root g) h₁ : (a : S) → AdjoinRoot g) ((aeval pb.gen : (a : R[X]) → S) f) : AdjoinRoot g) :
      S)
    ((aeval pb.gen : (a : R[X]) → S) f : S)
have rw : Eq.{u_2 + 1} (α := S)
  ((liftAlgHom g (Algebra.ofId R S) pb.gen h₂ : (a : AdjoinRoot g) → S)
      ((aeval (root g) : (a : R[X]) → AdjoinRoot g) f : AdjoinRoot g) :
    S)
  ((aeval pb.gen : (a : R[X]) → S) f : S)
Tactic: rw [pb.lift_aeval, aeval_eq, liftAlgHom_mk, Polynomial.aeval_def, Algebra.toRingHom_ofId]
-- 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
inst_1 : CommRing S
inst_2 : Algebra R S
g : R[X]
pb : PowerBasis R S
h₁ : Eq (α := AdjoinRoot g) ((aeval (root g) : (a : R[X]) → AdjoinRoot g) (minpoly R pb.gen)) 0
h₂ : Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : R[X]) → S) g : S) (0 : S)
h : Nontrivial S
f : R[X]
_hf : f.natDegree < pb.dim
rw :
  Eq.{u_2 + 1} (α := S)
    ((liftAlgHom g (Algebra.ofId R S) pb.gen h₂ : (a : AdjoinRoot g) → S)
        ((aeval (root g) : (a : R[X]) → AdjoinRoot g) f : AdjoinRoot g) :
      S)
    ((aeval pb.gen : (a : R[X]) → S) f : S)
⊢ Eq.{u_2 + 1} (α := S)
    ((liftAlgHom g (Algebra.ofId R S) pb.gen h₂ : (a : AdjoinRoot g) → S)
        ((pb.lift (root g) h₁ : (a : S) → AdjoinRoot g) ((aeval pb.gen : (a : R[X]) → S) f) : AdjoinRoot g) :
      S)
    ((aeval pb.gen : (a : R[X]) → S) f : S)
have rw₁ : Eq.{u_2 + 1} (α := S)
  ((liftAlgHom g (Algebra.ofId R S) pb.gen h₂ : (a : AdjoinRoot g) → S)
      ((mk g : (a : R[X]) → AdjoinRoot g) f : AdjoinRoot g) :
    S)
  ((aeval pb.gen : (a : R[X]) → S) f : S)
Tactic: rw [pb.lift_aeval, aeval_eq, liftAlgHom_mk, Polynomial.aeval_def, Algebra.toRingHom_ofId]
-- 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
inst_1 : CommRing S
inst_2 : Algebra R S
g : R[X]
pb : PowerBasis R S
h₁ : Eq (α := AdjoinRoot g) ((aeval (root g) : (a : R[X]) → AdjoinRoot g) (minpoly R pb.gen)) 0
h₂ : Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : R[X]) → S) g : S) (0 : S)
h : Nontrivial S
f : R[X]
_hf : f.natDegree < pb.dim
rw :
  Eq.{u_2 + 1} (α := S)
    ((liftAlgHom g (Algebra.ofId R S) pb.gen h₂ : (a : AdjoinRoot g) → S)
        ((aeval (root g) : (a : R[X]) → AdjoinRoot g) f : AdjoinRoot g) :
      S)
    ((aeval pb.gen : (a : R[X]) → S) f : S)
rw₁ :
  Eq.{u_2 + 1} (α := S)
    ((liftAlgHom g (Algebra.ofId R S) pb.gen h₂ : (a : AdjoinRoot g) → S)
        ((mk g : (a : R[X]) → AdjoinRoot g) f : AdjoinRoot g) :
      S)
    ((aeval pb.gen : (a : R[X]) → S) f : S)
⊢ Eq.{u_2 + 1} (α := S)
    ((liftAlgHom g (Algebra.ofId R S) pb.gen h₂ : (a : AdjoinRoot g) → S)
        ((pb.lift (root g) h₁ : (a : S) → AdjoinRoot g) ((aeval pb.gen : (a : R[X]) → S) f) : AdjoinRoot g) :
      S)
    ((aeval pb.gen : (a : R[X]) → S) f : S)
have rw₂ : eval₂ (↑(Algebra.ofId R S) : R →+* S) pb.gen f = (aeval pb.gen : (a : R[X]) → S) f
Tactic: rw [pb.lift_aeval, aeval_eq, liftAlgHom_mk, Polynomial.aeval_def, Algebra.toRingHom_ofId]
-- 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
inst_1 : CommRing S
inst_2 : Algebra R S
g : R[X]
pb : PowerBasis R S
h₁ : Eq (α := AdjoinRoot g) ((aeval (root g) : (a : R[X]) → AdjoinRoot g) (minpoly R pb.gen)) 0
h₂ : Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : R[X]) → S) g : S) (0 : S)
h : Nontrivial S
f : R[X]
_hf : f.natDegree < pb.dim
rw :
  Eq.{u_2 + 1} (α := S)
    ((liftAlgHom g (Algebra.ofId R S) pb.gen h₂ : (a : AdjoinRoot g) → S)
        ((aeval (root g) : (a : R[X]) → AdjoinRoot g) f : AdjoinRoot g) :
      S)
    ((aeval pb.gen : (a : R[X]) → S) f : S)
rw₁ :
  Eq.{u_2 + 1} (α := S)
    ((liftAlgHom g (Algebra.ofId R S) pb.gen h₂ : (a : AdjoinRoot g) → S)
        ((mk g : (a : R[X]) → AdjoinRoot g) f : AdjoinRoot g) :
      S)
    ((aeval pb.gen : (a : R[X]) → S) f : S)
rw₂ : eval₂ (↑(Algebra.ofId R S) : R →+* S) pb.gen f = (aeval pb.gen : (a : R[X]) → S) f
⊢ Eq.{u_2 + 1} (α := S)
    ((liftAlgHom g (Algebra.ofId R S) pb.gen h₂ : (a : AdjoinRoot g) → S)
        ((pb.lift (root g) h₁ : (a : S) → AdjoinRoot g) ((aeval pb.gen : (a : R[X]) → S) f) : AdjoinRoot g) :
      S)
    ((aeval pb.gen : (a : R[X]) → S) f : S)
have rw₃ : eval₂ (↑(Algebra.ofId R S) : R →+* S) pb.gen f = eval₂ (algebraMap R S) pb.gen f
Tactic: rw [pb.lift_aeval, aeval_eq, liftAlgHom_mk, Polynomial.aeval_def, Algebra.toRingHom_ofId]
-- 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
inst_1 : CommRing S
inst_2 : Algebra R S
g : R[X]
pb : PowerBasis R S
h₁ : Eq (α := AdjoinRoot g) ((aeval (root g) : (a : R[X]) → AdjoinRoot g) (minpoly R pb.gen)) 0
h₂ : Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : R[X]) → S) g : S) (0 : S)
h : Nontrivial S
f : R[X]
_hf : f.natDegree < pb.dim
rw :
  Eq.{u_2 + 1} (α := S)
    ((liftAlgHom g (Algebra.ofId R S) pb.gen h₂ : (a : AdjoinRoot g) → S)
        ((aeval (root g) : (a : R[X]) → AdjoinRoot g) f : AdjoinRoot g) :
      S)
    ((aeval pb.gen : (a : R[X]) → S) f : S)
rw₁ :
  Eq.{u_2 + 1} (α := S)
    ((liftAlgHom g (Algebra.ofId R S) pb.gen h₂ : (a : AdjoinRoot g) → S)
        ((mk g : (a : R[X]) → AdjoinRoot g) f : AdjoinRoot g) :
      S)
    ((aeval pb.gen : (a : R[X]) → S) f : S)
rw₂ : eval₂ (↑(Algebra.ofId R S) : R →+* S) pb.gen f = (aeval pb.gen : (a : R[X]) → S) f
rw₃ : eval₂ (↑(Algebra.ofId R S) : R →+* S) pb.gen f = eval₂ (algebraMap R S) pb.gen f
⊢ Eq.{u_2 + 1} (α := S)
    ((liftAlgHom g (Algebra.ofId R S) pb.gen h₂ : (a : AdjoinRoot g) → S)
        ((pb.lift (root g) h₁ : (a : S) → AdjoinRoot g) ((aeval pb.gen : (a : R[X]) → S) f) : AdjoinRoot g) :
      S)
    ((aeval pb.gen : (a : R[X]) → S) f : S)
have rw₄ : eval₂ (algebraMap R S) pb.gen f = eval₂ (algebraMap R S) pb.gen f
Tactic: rw [pb.lift_aeval, aeval_eq, liftAlgHom_mk, Polynomial.aeval_def, Algebra.toRingHom_ofId]
-- 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
L : Type u_6
F : Type u_7
inst : Field F
inst_1 : CommRing L
inst_2 : IsDomain L
inst_3 : Algebra F L
f : F[X]
hf : f ≠ 0
x : L
⊢ x ∈ aroots (minpoly F (powerBasis hf).gen) L ↔
    Membership.mem (α := L) (f.aroots L) ((Equiv.refl L : (a : L) → L) x : L)
have rw : HMul.hMul (β := F[X]) f ((C : (a : F) → F[X]) f.leadingCoeff⁻¹ : F[X]) ≠ 0
Tactic: rw [powerBasis_gen, minpoly_root hf, aroots_mul, aroots_C, add_zero, Equiv.refl_apply]
-- 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
I : Ideal R
f : R[X]
⊢ Eq (α := Ideal (AdjoinRoot f)) (Ideal.map (of f) I) (Ideal.map (R := R[X]) (mk f) (Ideal.map (F := R →+* R[X]) C I))
have rw : Eq (α := Ideal (AdjoinRoot f)) (Ideal.map ((mk f).comp C) I)
  (Ideal.map (R := R[X]) (mk f) (Ideal.map (F := R →+* R[X]) C I))
Tactic: rw [of, AdjoinRoot.mk, Ideal.map_map]
-- 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
I : Ideal R
f : R[X]
rw :
  Eq (α := Ideal (AdjoinRoot f)) (Ideal.map ((mk f).comp C) I)
    (Ideal.map (R := R[X]) (mk f) (Ideal.map (F := R →+* R[X]) C I))
⊢ Eq (α := Ideal (AdjoinRoot f)) (Ideal.map (of f) I) (Ideal.map (R := R[X]) (mk f) (Ideal.map (F := R →+* R[X]) C I))
have rw₁ : Eq (α := Ideal (AdjoinRoot f)) (Ideal.map (F := R →+* AdjoinRoot f) (RingHom.comp (Ideal.Quotient.mk (span {f})) C) I)
  (Ideal.map (R := R[X]) (F := R[X] →+* AdjoinRoot f) (Ideal.Quotient.mk (span {f})) (Ideal.map (F := R →+* R[X]) C I))
Tactic: rw [of, AdjoinRoot.mk, Ideal.map_map]
-- 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
I : Ideal R
f : R[X]
rw :
  Eq (α := Ideal (AdjoinRoot f)) (Ideal.map ((mk f).comp C) I)
    (Ideal.map (R := R[X]) (mk f) (Ideal.map (F := R →+* R[X]) C I))
rw₁ :
  Eq (α := Ideal (AdjoinRoot f)) (Ideal.map (F := R →+* AdjoinRoot f) (RingHom.comp (Ideal.Quotient.mk (span {f})) C) I)
    (Ideal.map (R := R[X]) (F := R[X] →+* AdjoinRoot f) (Ideal.Quotient.mk (span {f}))
      (Ideal.map (F := R →+* R[X]) C I))
⊢ Eq (α := Ideal (AdjoinRoot f)) (Ideal.map (of f) I) (Ideal.map (R := R[X]) (mk f) (Ideal.map (F := R →+* R[X]) C I))
have rw₂ : Eq (α := Ideal (AdjoinRoot f)) (Ideal.map (F := R →+* AdjoinRoot f) (RingHom.comp (Ideal.Quotient.mk (span {f})) C) I)
  (Ideal.map (F := R →+* AdjoinRoot f) (RingHom.comp (Ideal.Quotient.mk (span {f})) C) I)
Tactic: rw [of, AdjoinRoot.mk, Ideal.map_map]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
f : R[X]
x : AdjoinRoot f
⊢ Eq (α := HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
    (((quotMapOfEquivQuotMapCMapMk I f).symm :
          (a : AdjoinRoot f ⧸ Ideal.map (mk f) (Ideal.map C I)) → AdjoinRoot f ⧸ Ideal.map (of f) I)
        ((Ideal.Quotient.mk
              (Ideal.map (R := R[X]) (F := R[X] →+* HasQuotient.Quotient R[X] (B := Ideal R[X]) (span {f}))
                (Ideal.Quotient.mk (span {f})) (Ideal.map (F := R →+* R[X]) C I)) :
            (a : R[X] ⧸ span {f}) → (R[X] ⧸ span {f}) ⧸ Ideal.map (Ideal.Quotient.mk (span {f})) (Ideal.map C I))
          x) :
      HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
    ((Ideal.Quotient.mk (Ideal.map (of f) I) : (a : AdjoinRoot f) → AdjoinRoot f ⧸ Ideal.map (of f) I) x :
      HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
have rw : Eq (α := HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
  ((quotEquivOfEq sorry : (a : AdjoinRoot f ⧸ Ideal.map (mk f) (Ideal.map C I)) → AdjoinRoot f ⧸ Ideal.map (of f) I)
      ((Ideal.Quotient.mk
            (Ideal.map (R := R[X]) (F := R[X] →+* HasQuotient.Quotient R[X] (B := Ideal R[X]) (span {f}))
              (Ideal.Quotient.mk (span {f})) (Ideal.map (F := R →+* R[X]) C I)) :
          (a : R[X] ⧸ span {f}) → (R[X] ⧸ span {f}) ⧸ Ideal.map (Ideal.Quotient.mk (span {f})) (Ideal.map C I))
        x) :
    HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
  ((Ideal.Quotient.mk (Ideal.map (of f) I) : (a : AdjoinRoot f) → AdjoinRoot f ⧸ Ideal.map (of f) I) x :
    HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
Tactic: rw [quotMapOfEquivQuotMapCMapMk, Ideal.quotEquivOfEq_symm]
-- 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
I : Ideal R
f : R[X]
⊢ Eq (α := Ideal (HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I)))
    (span
      (singleton (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ Ideal.map C I) f :
          HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))))
    (Ideal.map (R := (R ⧸ I)[X]) (F :=
      (R ⧸ I)[X] →+* HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))
      (↑I.polynomialQuotientEquivQuotientPolynomial : (R ⧸ I)[X] →+* R[X] ⧸ Ideal.map C I)
      (span {Polynomial.map (Ideal.Quotient.mk I) f}))
have rw : Eq (α := Ideal (HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I)))
  (span
    (singleton (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))
      ((Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ Ideal.map C I) f :
        HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))))
  (span
    (Set.image (α := (R ⧸ I)[X])
      (⇑(↑I.polynomialQuotientEquivQuotientPolynomial : (R ⧸ I)[X] →+* R[X] ⧸ Ideal.map C I) :
        (a : (R ⧸ I)[X]) → R[X] ⧸ Ideal.map C I)
      {Polynomial.map (Ideal.Quotient.mk I) f}))
Tactic: rw [map_span, Set.image_singleton, RingEquiv.coe_toRingHom,
        polynomialQuotientEquivQuotientPolynomial_map_mk I f]
-- 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
I : Ideal R
f : R[X]
rw :
  Eq (α := Ideal (HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I)))
    (span
      (singleton (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ Ideal.map C I) f :
          HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))))
    (span
      (Set.image (α := (R ⧸ I)[X])
        (⇑(↑I.polynomialQuotientEquivQuotientPolynomial : (R ⧸ I)[X] →+* R[X] ⧸ Ideal.map C I) :
          (a : (R ⧸ I)[X]) → R[X] ⧸ Ideal.map C I)
        {Polynomial.map (Ideal.Quotient.mk I) f}))
⊢ Eq (α := Ideal (HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I)))
    (span
      (singleton (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ Ideal.map C I) f :
          HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))))
    (Ideal.map (R := (R ⧸ I)[X]) (F :=
      (R ⧸ I)[X] →+* HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))
      (↑I.polynomialQuotientEquivQuotientPolynomial : (R ⧸ I)[X] →+* R[X] ⧸ Ideal.map C I)
      (span {Polynomial.map (Ideal.Quotient.mk I) f}))
have rw₁ : Eq (α := Ideal (HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I)))
  (span
    (singleton (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))
      ((Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ Ideal.map C I) f :
        HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))))
  (span
    (singleton (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))
      (((↑I.polynomialQuotientEquivQuotientPolynomial : (R ⧸ I)[X] →+* R[X] ⧸ Ideal.map C I) :
            (a : (R ⧸ I)[X]) → R[X] ⧸ Ideal.map C I)
          (Polynomial.map (Ideal.Quotient.mk I) f) :
        HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))))
Tactic: rw [map_span, Set.image_singleton, RingEquiv.coe_toRingHom,
        polynomialQuotientEquivQuotientPolynomial_map_mk I f]
-- 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
I : Ideal R
f : R[X]
⊢ Eq (α := Ideal (HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I)))
    (Ideal.map (R := R[X]) (F := R[X] →+* HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) C I)) (span {f}))
    (span
      (singleton (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ Ideal.map C I) f :
          HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))))
have rw : Eq (α := Ideal (HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I)))
  (span
    (Set.image (α := R[X]) (⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) C I)) : (a : R[X]) → R[X] ⧸ Ideal.map C I)
      {f}))
  (span
    (singleton (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))
      ((Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ Ideal.map C I) f :
        HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))))
Tactic: rw [map_span, Set.image_singleton]
-- 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
I : Ideal R
f : R[X]
rw :
  Eq (α := Ideal (HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I)))
    (span
      (Set.image (α := R[X])
        (⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) C I)) : (a : R[X]) → R[X] ⧸ Ideal.map C I) {f}))
    (span
      (singleton (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ Ideal.map C I) f :
          HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))))
⊢ Eq (α := Ideal (HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I)))
    (Ideal.map (R := R[X]) (F := R[X] →+* HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) C I)) (span {f}))
    (span
      (singleton (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ Ideal.map C I) f :
          HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))))
have rw₁ : Eq (α := Ideal (HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I)))
  (span
    (singleton (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))
      ((Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ Ideal.map C I) f :
        HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))))
  (span
    (singleton (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))
      ((Ideal.Quotient.mk (Ideal.map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ Ideal.map C I) f :
        HasQuotient.Quotient R[X] (B := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I))))
Tactic: rw [map_span, Set.image_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
I_1 : Ideal R
f_1 f : R[X]
I : Ideal R
x : R
⊢ Eq (α := HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))
    ((quotAdjoinRootEquivQuotPolynomialQuot I f :
          (a : AdjoinRoot f ⧸ Ideal.map (of f) I) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})
        ((algebraMap R (HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I)) :
            (a : R) → AdjoinRoot f ⧸ Ideal.map (of f) I)
          x) :
      HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))
    ((algebraMap R
            (HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f})) :
          (a : R) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})
        x :
      HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))
have this : Eq (α := HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
  ((algebraMap R (HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I)) :
        (a : R) → AdjoinRoot f ⧸ Ideal.map (of f) I)
      x :
    HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
  ((Ideal.Quotient.mk (Ideal.map (of f) I) : (a : AdjoinRoot f) → AdjoinRoot f ⧸ Ideal.map (of f) I)
      ((mk f : (a : R[X]) → AdjoinRoot f) ((C : (a : R) → R[X]) x)) :
    HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
Tactic: have :
        algebraMap R (AdjoinRoot f ⧸ Ideal.map (of f) I) x =
          Ideal.Quotient.mk (Ideal.map (AdjoinRoot.of f) I) ((mk f) (C x)) :=
        rfl
-- 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
I_1 : Ideal R
f_1 f : R[X]
I : Ideal R
x : R
this :
  Eq (α := HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
    ((algebraMap R (HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I)) :
          (a : R) → AdjoinRoot f ⧸ Ideal.map (of f) I)
        x :
      HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
    ((Ideal.Quotient.mk (Ideal.map (of f) I) : (a : AdjoinRoot f) → AdjoinRoot f ⧸ Ideal.map (of f) I)
        ((mk f : (a : R[X]) → AdjoinRoot f) ((C : (a : R) → R[X]) x)) :
      HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
⊢ Eq (α := HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))
    ((quotAdjoinRootEquivQuotPolynomialQuot I f :
          (a : AdjoinRoot f ⧸ Ideal.map (of f) I) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})
        ((algebraMap R (HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I)) :
            (a : R) → AdjoinRoot f ⧸ Ideal.map (of f) I)
          x) :
      HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))
    ((algebraMap R
            (HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f})) :
          (a : R) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})
        x :
      HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))
have rw : Eq (α := HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))
  ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f}) :
        (a : (R ⧸ I)[X]) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})
      ((C : (a : R ⧸ I) → (R ⧸ I)[X]) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x)) :
    HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))
  ((@RingHom.comp _ (R ⧸ I)[X] _ _ Semiring.toNonAssocSemiring _
          (algebraMap (R ⧸ I)[X]
            (HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f})))
          (algebraMap R (R ⧸ I)[X]) :
        (a : R) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})
      x :
    HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))
Tactic: rw [this, quotAdjoinRootEquivQuotPolynomialQuot_mk_of, map_C, Quotient.alg_map_eq]