awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
I : Ideal R
⊢ Eq (α := HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))
    ((quotEquivQuotMap f I :
          (a : AdjoinRoot f ⧸ Ideal.map (of f) I) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})
        ((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) g)) :
      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})
        (Polynomial.map (Ideal.Quotient.mk I) g) :
      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}))
  ((quotAdjoinRootEquivQuotPolynomialQuot I f :
        (a : AdjoinRoot f ⧸ Ideal.map (of f) I) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})
      ((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) g)) :
    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})
      (Polynomial.map (Ideal.Quotient.mk I) g) :
    HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))
Tactic: rw [AdjoinRoot.quotEquivQuotMap_apply, AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_mk_of]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
I : Ideal R
rw :
  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})
        ((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) g)) :
      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})
        (Polynomial.map (Ideal.Quotient.mk I) g) :
      HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))
⊢ Eq (α := HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))
    ((quotEquivQuotMap f I :
          (a : AdjoinRoot f ⧸ Ideal.map (of f) I) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})
        ((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) g)) :
      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})
        (Polynomial.map (Ideal.Quotient.mk I) g) :
      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})
      (Polynomial.map (Ideal.Quotient.mk I) g) :
    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})
      (Polynomial.map (Ideal.Quotient.mk I) g) :
    HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) f}))
Tactic: rw [AdjoinRoot.quotEquivQuotMap_apply, AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_mk_of]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
I : Ideal R
⊢ Eq (α := HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
    (((quotEquivQuotMap f I).symm :
          (a : (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f}) → AdjoinRoot f ⧸ Ideal.map (of f) I)
        ((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})
          (Polynomial.map (Ideal.Quotient.mk I) g)) :
      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) g) :
      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))
  (((quotAdjoinRootEquivQuotPolynomialQuot I f).symm :
        (a : (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f}) → AdjoinRoot f ⧸ Ideal.map (of f) I)
      ((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})
        (Polynomial.map (Ideal.Quotient.mk I) g)) :
    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) g) :
    HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
Tactic: rw [AdjoinRoot.quotEquivQuotMap_symm_apply,
    AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
I : Ideal R
rw :
  Eq (α := HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
    (((quotAdjoinRootEquivQuotPolynomialQuot I f).symm :
          (a : (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f}) → AdjoinRoot f ⧸ Ideal.map (of f) I)
        ((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})
          (Polynomial.map (Ideal.Quotient.mk I) g)) :
      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) g) :
      HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
⊢ Eq (α := HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
    (((quotEquivQuotMap f I).symm :
          (a : (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f}) → AdjoinRoot f ⧸ Ideal.map (of f) I)
        ((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})
          (Polynomial.map (Ideal.Quotient.mk I) g)) :
      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) g) :
      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))
  ((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) g) :
    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) g) :
    HasQuotient.Quotient (AdjoinRoot f) (B := Ideal (AdjoinRoot f)) (Ideal.map (of f) I))
Tactic: rw [AdjoinRoot.quotEquivQuotMap_symm_apply,
    AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk]
-- 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
pb : PowerBasis R S
I : Ideal R
x : R
⊢ Eq (α := AdjoinRoot (minpoly R pb.gen))
    ((aeval (root (minpoly R pb.gen)) : (a : R[X]) → AdjoinRoot (minpoly R pb.gen)) (minpoly R pb.gen)) 0
have rw : Eq (α := AdjoinRoot (minpoly R pb.gen))
  ((AdjoinRoot.mk (minpoly R pb.gen) : (a : R[X]) → AdjoinRoot (minpoly R pb.gen)) (minpoly R pb.gen)) 0
Tactic: rw [AdjoinRoot.aeval_eq, AdjoinRoot.mk_self]
-- 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
pb : PowerBasis R S
I : Ideal R
x : R
rw :
  Eq (α := AdjoinRoot (minpoly R pb.gen))
    ((AdjoinRoot.mk (minpoly R pb.gen) : (a : R[X]) → AdjoinRoot (minpoly R pb.gen)) (minpoly R pb.gen)) 0
⊢ Eq (α := AdjoinRoot (minpoly R pb.gen))
    ((aeval (root (minpoly R pb.gen)) : (a : R[X]) → AdjoinRoot (minpoly R pb.gen)) (minpoly R pb.gen)) 0
have rw₁ : Eq.{u_1 + 1} (α := AdjoinRoot (minpoly R pb.gen)) 0 0
Tactic: rw [AdjoinRoot.aeval_eq, AdjoinRoot.mk_self]
-- 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
pb : PowerBasis R S
I : Ideal R
x : R
⊢ Eq (α := Ideal (AdjoinRoot (minpoly R pb.gen)))
    (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (of (minpoly R pb.gen)) I)
    (Ideal.map (R := S) (F := RingHom.{u_2, u_1} S (AdjoinRoot (minpoly R pb.gen)))
      (↑(equiv' (minpoly R pb.gen) pb ⋯ ⋯).symm.toRingEquiv : S →+* AdjoinRoot (minpoly R pb.gen))
      (Ideal.map (F := R →+* S) (algebraMap R S) I))
have rw : Eq (α := Ideal (AdjoinRoot (minpoly R pb.gen)))
  (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (of (minpoly R pb.gen)) I)
  (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(equiv' (minpoly R pb.gen) pb sorry sorry).symm.toRingEquiv : S →+* AdjoinRoot (minpoly R pb.gen)) (algebraMap R S))
    I)
Tactic: rw [Ideal.map_map,
                      ← AlgEquiv.coe_ringHom_commutes, ← AdjoinRoot.algebraMap_eq,
                      AlgHom.comp_algebraMap]
-- 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
pb : PowerBasis R S
I : Ideal R
x : R
rw :
  Eq (α := Ideal (AdjoinRoot (minpoly R pb.gen)))
    (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (of (minpoly R pb.gen)) I)
    (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen))
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
        (↑(equiv' (minpoly R pb.gen) pb ⋯ ⋯).symm.toRingEquiv : S →+* AdjoinRoot (minpoly R pb.gen)) (algebraMap R S))
      I)
⊢ Eq (α := Ideal (AdjoinRoot (minpoly R pb.gen)))
    (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (of (minpoly R pb.gen)) I)
    (Ideal.map (R := S) (F := RingHom.{u_2, u_1} S (AdjoinRoot (minpoly R pb.gen)))
      (↑(equiv' (minpoly R pb.gen) pb ⋯ ⋯).symm.toRingEquiv : S →+* AdjoinRoot (minpoly R pb.gen))
      (Ideal.map (F := R →+* S) (algebraMap R S) I))
have rw₁ : Eq (α := Ideal (AdjoinRoot (minpoly R pb.gen)))
  (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (of (minpoly R pb.gen)) I)
  (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(↑(equiv' (minpoly R pb.gen) pb sorry sorry).symm : S →ₐ[R] AdjoinRoot (minpoly R pb.gen)) :
        S →+* AdjoinRoot (minpoly R pb.gen))
      (algebraMap R S))
    I)
Tactic: rw [Ideal.map_map,
                      ← AlgEquiv.coe_ringHom_commutes, ← AdjoinRoot.algebraMap_eq,
                      AlgHom.comp_algebraMap]
-- 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
pb : PowerBasis R S
I : Ideal R
x : R
rw :
  Eq (α := Ideal (AdjoinRoot (minpoly R pb.gen)))
    (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (of (minpoly R pb.gen)) I)
    (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen))
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
        (↑(equiv' (minpoly R pb.gen) pb ⋯ ⋯).symm.toRingEquiv : S →+* AdjoinRoot (minpoly R pb.gen)) (algebraMap R S))
      I)
rw₁ :
  Eq (α := Ideal (AdjoinRoot (minpoly R pb.gen)))
    (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (of (minpoly R pb.gen)) I)
    (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen))
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
        (↑(↑(equiv' (minpoly R pb.gen) pb ⋯ ⋯).symm : S →ₐ[R] AdjoinRoot (minpoly R pb.gen)) :
          S →+* AdjoinRoot (minpoly R pb.gen))
        (algebraMap R S))
      I)
⊢ Eq (α := Ideal (AdjoinRoot (minpoly R pb.gen)))
    (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (of (minpoly R pb.gen)) I)
    (Ideal.map (R := S) (F := RingHom.{u_2, u_1} S (AdjoinRoot (minpoly R pb.gen)))
      (↑(equiv' (minpoly R pb.gen) pb ⋯ ⋯).symm.toRingEquiv : S →+* AdjoinRoot (minpoly R pb.gen))
      (Ideal.map (F := R →+* S) (algebraMap R S) I))
have rw₂ : Eq (α := Ideal (AdjoinRoot (minpoly R pb.gen)))
  (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (algebraMap R (AdjoinRoot (minpoly R pb.gen))) I)
  (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(↑(equiv' (minpoly R pb.gen) pb sorry sorry).symm : S →ₐ[R] AdjoinRoot (minpoly R pb.gen)) :
        S →+* AdjoinRoot (minpoly R pb.gen))
      (algebraMap R S))
    I)
Tactic: rw [Ideal.map_map,
                      ← AlgEquiv.coe_ringHom_commutes, ← AdjoinRoot.algebraMap_eq,
                      AlgHom.comp_algebraMap]
-- 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
pb : PowerBasis R S
I : Ideal R
x : R
rw :
  Eq (α := Ideal (AdjoinRoot (minpoly R pb.gen)))
    (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (of (minpoly R pb.gen)) I)
    (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen))
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
        (↑(equiv' (minpoly R pb.gen) pb ⋯ ⋯).symm.toRingEquiv : S →+* AdjoinRoot (minpoly R pb.gen)) (algebraMap R S))
      I)
rw₁ :
  Eq (α := Ideal (AdjoinRoot (minpoly R pb.gen)))
    (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (of (minpoly R pb.gen)) I)
    (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen))
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
        (↑(↑(equiv' (minpoly R pb.gen) pb ⋯ ⋯).symm : S →ₐ[R] AdjoinRoot (minpoly R pb.gen)) :
          S →+* AdjoinRoot (minpoly R pb.gen))
        (algebraMap R S))
      I)
rw₂ :
  Eq (α := Ideal (AdjoinRoot (minpoly R pb.gen)))
    (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (algebraMap R (AdjoinRoot (minpoly R pb.gen))) I)
    (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen))
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
        (↑(↑(equiv' (minpoly R pb.gen) pb ⋯ ⋯).symm : S →ₐ[R] AdjoinRoot (minpoly R pb.gen)) :
          S →+* AdjoinRoot (minpoly R pb.gen))
        (algebraMap R S))
      I)
⊢ Eq (α := Ideal (AdjoinRoot (minpoly R pb.gen)))
    (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (of (minpoly R pb.gen)) I)
    (Ideal.map (R := S) (F := RingHom.{u_2, u_1} S (AdjoinRoot (minpoly R pb.gen)))
      (↑(equiv' (minpoly R pb.gen) pb ⋯ ⋯).symm.toRingEquiv : S →+* AdjoinRoot (minpoly R pb.gen))
      (Ideal.map (F := R →+* S) (algebraMap R S) I))
have rw₃ : Eq (α := Ideal (AdjoinRoot (minpoly R pb.gen)))
  (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (algebraMap R (AdjoinRoot (minpoly R pb.gen))) I)
  (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (algebraMap R (AdjoinRoot (minpoly R pb.gen))) I)
Tactic: rw [Ideal.map_map,
                      ← AlgEquiv.coe_ringHom_commutes, ← AdjoinRoot.algebraMap_eq,
                      AlgHom.comp_algebraMap]
-- 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
pb : PowerBasis R S
I : Ideal R
g : R[X]
⊢ Eq.{u_1 + 1} (α :=
    HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X])
      (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}))
    ((pb.quotientEquivQuotientMinpolyMap I :
          (a : S ⧸ Ideal.map (algebraMap R S) I) →
            (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)})
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I)
          ((aeval pb.gen : (a : R[X]) → S) g)) :
      HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X])
        (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}))
    ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}) :
          (a : (R ⧸ I)[X]) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)})
        (Polynomial.map (Ideal.Quotient.mk I) g) :
      HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X])
        (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}))
have rw : Eq.{u_1 + 1} (α :=
  HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X])
    (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}))
  (((ofRingEquiv sorry).trans (quotEquivQuotMap (minpoly R pb.gen) I) :
        (a : S ⧸ Ideal.map (algebraMap R S) I) →
          (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)})
      ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I)
        ((aeval pb.gen : (a : R[X]) → S) g)) :
    HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X])
      (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}))
  ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}) :
        (a : (R ⧸ I)[X]) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)})
      (Polynomial.map (Ideal.Quotient.mk I) g) :
    HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X])
      (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}))
Tactic: rw [PowerBasis.quotientEquivQuotientMinpolyMap, AlgEquiv.trans_apply, AlgEquiv.ofRingEquiv_apply,
    quotientEquiv_mk, AlgEquiv.coe_ringEquiv', AdjoinRoot.equiv'_symm_apply, PowerBasis.lift_aeval,
    AdjoinRoot.aeval_eq, AdjoinRoot.quotEquivQuotMap_apply_mk]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (hypothesis)
Goal:
K : Type u_6
L : Type u_7
inst : CommRing K
inst_1 : IsDomain K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra.IsIntegral K L
f : L[X]
hf : Irreducible f
⊢ ∃ (g : K[X]), g.Monic ∧ Irreducible g ∧ f ∣ Polynomial.map (algebraMap K L) g
have this : Fact (Irreducible f)
Tactic: haveI := Fact.mk hf
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (hypothesis)
Goal:
K : Type u_6
L : Type u_7
inst : CommRing K
inst_1 : IsDomain K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra.IsIntegral K L
f : L[X]
hf : Irreducible f
this : Fact (Irreducible f)
⊢ ∃ (g : K[X]), g.Monic ∧ Irreducible g ∧ f ∣ Polynomial.map (algebraMap K L) g
have h : f ≠ 0
Tactic: have h := hf.ne_zero
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (hypothesis)
Goal:
K : Type u_6
L : Type u_7
inst : CommRing K
inst_1 : IsDomain K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra.IsIntegral K L
f : L[X]
hf : Irreducible f
this : Fact (Irreducible f)
h : f ≠ 0
⊢ ∃ (g : K[X]), g.Monic ∧ Irreducible g ∧ f ∣ Polynomial.map (algebraMap K L) g
have h2 : IsIntegral K (AdjoinRoot.root f)
Tactic: have h2 := isIntegral_trans (R := K) _ (AdjoinRoot.isIntegral_root h)
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (hypothesis)
Goal:
K : Type u_6
L : Type u_7
inst : CommRing K
inst_1 : IsDomain K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra.IsIntegral K L
f : L[X]
hf : Irreducible f
this : Fact (Irreducible f)
h : f ≠ 0
h2 : IsIntegral K (AdjoinRoot.root f)
⊢ ∃ (g : K[X]), g.Monic ∧ Irreducible g ∧ f ∣ Polynomial.map (algebraMap K L) g
have h3 : HMul.hMul (β := L[X]) f ((C : (a : L) → L[X]) f.leadingCoeff⁻¹ : L[X]) ∣
  Polynomial.map (algebraMap K L) (minpoly K (AdjoinRoot.root f))
Tactic: have h3 := (AdjoinRoot.minpoly_root h) ▸ minpoly.dvd_map_of_isScalarTower K L (AdjoinRoot.root f)
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : R[X]} (hp : p.Monic) (hn : p.natDegree = m),
      ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
        (Polynomial.map (algebraMap R S) p).Splits
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
hn : p.natDegree = n
⊢ ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
    (Polynomial.map (algebraMap R S) p).Splits
have pos : ∀ (hpu : IsUnit p),
  ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
    (Polynomial.map (algebraMap R S) p).Splits
Tactic: by_cases hpu : IsUnit p
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : R[X]} (hp : p.Monic) (hn : p.natDegree = m),
      ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
        (Polynomial.map (algebraMap R S) p).Splits
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
hn : p.natDegree = n
pos :
  ∀ (hpu : IsUnit p),
    ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
      (Polynomial.map (algebraMap R S) p).Splits
⊢ ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
    (Polynomial.map (algebraMap R S) p).Splits
have neg : ∀ (hpu : ¬IsUnit p),
  ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
    (Polynomial.map (algebraMap R S) p).Splits
Tactic: by_cases hpu : IsUnit p