awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (hypothesis)
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 R S
inst_4 : Algebra R T
inst_5 : IsStandardEtale R S
inst_6 : Etale R T
f : S →ₐ[R] T
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑f : (a : S) → T)
this : Algebra S T := f.toAlgebra
⊢ IsStandardEtale R T
have this₁ : IsScalarTower R S T
Tactic: have : IsScalarTower R S T := .of_algebraMap_eq' f.comp_algebraMap.symm
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
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 R S
inst_4 : Algebra R T
inst_5 : IsStandardEtale R S
inst_6 : Etale R T
f : S →ₐ[R] T
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑f : (a : S) → T)
this_1 : Algebra S T := f.toAlgebra
this : IsScalarTower R S T
⊢ IsStandardEtale R T
have obtain : ∀ (e : S) (he : IsIdempotentElem e) (hfe : Eq (α := Ideal S) (RingHom.ker f.toRingHom) (S ∙ e)), IsStandardEtale R T
Tactic: obtain ⟨e, he, hfe⟩ :=
    (Ideal.isIdempotentElem_iff_of_fg _ (Algebra.FinitePresentation.ker_fG_of_surjective f hf)).mp
      ((Algebra.FormallyEtale.iff_of_surjective hf).mp (.of_restrictScalars (R := R)))
-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (hypothesis)
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 R S
inst_4 : Algebra R T
inst_5 : IsStandardEtale R S
inst_6 : Etale R T
f : S →ₐ[R] T
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑f : (a : S) → T)
this_1 : Algebra S T := f.toAlgebra
this : IsScalarTower R S T
e : S
he : IsIdempotentElem e
hfe : Eq (α := Ideal S) (RingHom.ker f.toRingHom) (S ∙ e)
⊢ IsStandardEtale R T
have this₁ : IsLocalization.Away (1 - e) T
Tactic: have := IsLocalization.away_of_isIdempotentElem he.one_sub (hfe.trans (by simp)) hf
-- Lean 4 proof step from Mathlib.RingTheory.EuclideanDomain (goal)
Goal:
R : Type u_1
inst : EuclideanDomain R
inst_1 : GCDMonoid R
p q : R
hp : p ≠ 0
⊢ p / @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0
have obtain : ∀ (r : R) (hr : p = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q * r),
  p / @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0
Tactic: obtain ⟨r, hr⟩ := GCDMonoid.gcd_dvd_left p q
-- Lean 4 proof step from Mathlib.RingTheory.EuclideanDomain (hypothesis)
Goal:
R : Type u_1
inst : EuclideanDomain R
inst_1 : GCDMonoid R
p q : R
hp : p ≠ 0
r : R
hr : p = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q * r
⊢ p / @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0
have pq0 : @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0
Tactic: obtain ⟨pq0, r0⟩ : GCDMonoid.gcd p q ≠ 0 ∧ r ≠ 0 := mul_ne_zero_iff.mp (hr ▸ hp)
-- Lean 4 proof step from Mathlib.RingTheory.EuclideanDomain (hypothesis)
Goal:
R : Type u_1
inst : EuclideanDomain R
inst_1 : GCDMonoid R
p q : R
hp : p ≠ 0
r : R
hr : p = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q * r
pq0 : @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0
⊢ p / @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0
have r0 : r ≠ 0
Tactic: obtain ⟨pq0, r0⟩ : GCDMonoid.gcd p q ≠ 0 ∧ r ≠ 0 := mul_ne_zero_iff.mp (hr ▸ hp)
-- Lean 4 proof step from Mathlib.RingTheory.EuclideanDomain (goal)
Goal:
R : Type u_1
inst : EuclideanDomain R
inst_1 : GCDMonoid R
p q : R
hp : p ≠ 0
r : R
hr : p = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q * r
pq0 : @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0
r0 : r ≠ 0
⊢ p / @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0
have nth_rw : @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q * r /
    @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠
  0
Tactic: nth_rw 1 [hr]
-- Lean 4 proof step from Mathlib.RingTheory.EuclideanDomain (goal)
Goal:
R : Type u_1
inst : EuclideanDomain R
inst_1 : GCDMonoid R
p q : R
hq : q ≠ 0
⊢ q / @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0
have obtain : ∀ (r : R) (hr : q = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q * r),
  q / @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0
Tactic: obtain ⟨r, hr⟩ := GCDMonoid.gcd_dvd_right p q
-- Lean 4 proof step from Mathlib.RingTheory.EuclideanDomain (hypothesis)
Goal:
R : Type u_1
inst : EuclideanDomain R
inst_1 : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q * r
⊢ q / @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0
have pq0 : @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0
Tactic: obtain ⟨pq0, r0⟩ : GCDMonoid.gcd p q ≠ 0 ∧ r ≠ 0 := mul_ne_zero_iff.mp (hr ▸ hq)
-- Lean 4 proof step from Mathlib.RingTheory.EuclideanDomain (hypothesis)
Goal:
R : Type u_1
inst : EuclideanDomain R
inst_1 : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q * r
pq0 : @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0
⊢ q / @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0
have r0 : r ≠ 0
Tactic: obtain ⟨pq0, r0⟩ : GCDMonoid.gcd p q ≠ 0 ∧ r ≠ 0 := mul_ne_zero_iff.mp (hr ▸ hq)
-- Lean 4 proof step from Mathlib.RingTheory.EuclideanDomain (goal)
Goal:
R : Type u_1
inst : EuclideanDomain R
inst_1 : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q * r
pq0 : @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0
r0 : r ≠ 0
⊢ q / @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠ 0
have nth_rw : @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q * r /
    @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ p q ≠
  0
Tactic: nth_rw 1 [hr]
-- Lean 4 proof step from Mathlib.RingTheory.EuclideanDomain (goal)
Goal:
R : Type u_1
inst : EuclideanDomain R
inst_1 : DecidableEq R
a b : R
⊢ Associated (gcd a b * lcm a b) (a * b)
have rw : Associated (a * b) (a * b)
Tactic: rw [EuclideanDomain.gcd_mul_lcm]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R₀ : Type u_1
inst_3 : CommRing R₀
inst_4 : Algebra R₀ R
inst_5 : Algebra R₀ S
inst_6 : IsScalarTower R₀ R S
R₁ : Type u_2
inst_7 : CommRing R₁
inst_8 : Algebra R₁ R
inst_9 : Algebra R₁ S
inst_10 : IsScalarTower R₁ R S
inst_11 : Algebra R₀ R₁
inst_12 : IsScalarTower R₀ R₁ R
⊢ Eq (α := RingHom.{u_1, w} R₀ P.Ring) (algebraMap R₀ P.Ring)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R₁ P.Ring) (algebraMap R₀ R₁))
have rw : Eq (α := RingHom.{u_1, w} R₀ P.Ring)
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R P.Ring) (algebraMap R₀ R))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R₁ P.Ring) (algebraMap R₀ R₁))
Tactic: rw [IsScalarTower.algebraMap_eq R₀ R, IsScalarTower.algebraMap_eq R₁ R,
    RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq R₀ R₁ R]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R₀ : Type u_1
inst_3 : CommRing R₀
inst_4 : Algebra R₀ R
inst_5 : Algebra R₀ S
inst_6 : IsScalarTower R₀ R S
R₁ : Type u_2
inst_7 : CommRing R₁
inst_8 : Algebra R₁ R
inst_9 : Algebra R₁ S
inst_10 : IsScalarTower R₁ R S
inst_11 : Algebra R₀ R₁
inst_12 : IsScalarTower R₀ R₁ R
rw :
  Eq (α := RingHom.{u_1, w} R₀ P.Ring)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R P.Ring) (algebraMap R₀ R))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R₁ P.Ring) (algebraMap R₀ R₁))
⊢ Eq (α := RingHom.{u_1, w} R₀ P.Ring) (algebraMap R₀ P.Ring)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R₁ P.Ring) (algebraMap R₀ R₁))
have rw₁ : Eq (α := RingHom.{u_1, w} R₀ P.Ring)
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R P.Ring) (algebraMap R₀ R))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R P.Ring) (algebraMap R₁ R)) (algebraMap R₀ R₁))
Tactic: rw [IsScalarTower.algebraMap_eq R₀ R, IsScalarTower.algebraMap_eq R₁ R,
    RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq R₀ R₁ R]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R₀ : Type u_1
inst_3 : CommRing R₀
inst_4 : Algebra R₀ R
inst_5 : Algebra R₀ S
inst_6 : IsScalarTower R₀ R S
R₁ : Type u_2
inst_7 : CommRing R₁
inst_8 : Algebra R₁ R
inst_9 : Algebra R₁ S
inst_10 : IsScalarTower R₁ R S
inst_11 : Algebra R₀ R₁
inst_12 : IsScalarTower R₀ R₁ R
rw :
  Eq (α := RingHom.{u_1, w} R₀ P.Ring)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R P.Ring) (algebraMap R₀ R))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R₁ P.Ring) (algebraMap R₀ R₁))
rw₁ :
  Eq (α := RingHom.{u_1, w} R₀ P.Ring)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R P.Ring) (algebraMap R₀ R))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R P.Ring) (algebraMap R₁ R)) (algebraMap R₀ R₁))
⊢ Eq (α := RingHom.{u_1, w} R₀ P.Ring) (algebraMap R₀ P.Ring)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R₁ P.Ring) (algebraMap R₀ R₁))
have rw₂ : Eq (α := RingHom.{u_1, w} R₀ P.Ring)
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R P.Ring) (algebraMap R₀ R))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R P.Ring)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R₁ R) (algebraMap R₀ R₁)))
Tactic: rw [IsScalarTower.algebraMap_eq R₀ R, IsScalarTower.algebraMap_eq R₁ R,
    RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq R₀ R₁ R]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R₀ : Type u_1
inst_3 : CommRing R₀
inst_4 : Algebra R₀ R
inst_5 : Algebra R₀ S
inst_6 : IsScalarTower R₀ R S
R₁ : Type u_2
inst_7 : CommRing R₁
inst_8 : Algebra R₁ R
inst_9 : Algebra R₁ S
inst_10 : IsScalarTower R₁ R S
inst_11 : Algebra R₀ R₁
inst_12 : IsScalarTower R₀ R₁ R
rw :
  Eq (α := RingHom.{u_1, w} R₀ P.Ring)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R P.Ring) (algebraMap R₀ R))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R₁ P.Ring) (algebraMap R₀ R₁))
rw₁ :
  Eq (α := RingHom.{u_1, w} R₀ P.Ring)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R P.Ring) (algebraMap R₀ R))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R P.Ring) (algebraMap R₁ R)) (algebraMap R₀ R₁))
rw₂ :
  Eq (α := RingHom.{u_1, w} R₀ P.Ring)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R P.Ring) (algebraMap R₀ R))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R P.Ring)
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R₁ R) (algebraMap R₀ R₁)))
⊢ Eq (α := RingHom.{u_1, w} R₀ P.Ring) (algebraMap R₀ P.Ring)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R₁ P.Ring) (algebraMap R₀ R₁))
have rw₃ : Eq (α := RingHom.{u_1, w} R₀ P.Ring)
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R P.Ring) (algebraMap R₀ R))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R P.Ring) (algebraMap R₀ R))
Tactic: rw [IsScalarTower.algebraMap_eq R₀ R, IsScalarTower.algebraMap_eq R₁ R,
    RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq R₀ R₁ R]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R₀ : Type u_1
inst_3 : CommRing R₀
inst_4 : Algebra R₀ R
inst_5 : Algebra R₀ S
inst_6 : IsScalarTower R₀ R S
⊢ Eq (α := R₀ →+* S) (algebraMap R₀ S)
    (@RingHom.comp.{u_1, w, v} _ P.Ring _ _ Semiring.toNonAssocSemiring _ (algebraMap P.Ring S) (algebraMap R₀ P.Ring))
have rw : Eq (α := R₀ →+* S) (algebraMap R₀ S)
  (@RingHom.comp.{u_1, w, v} _ P.Ring _ _ Semiring.toNonAssocSemiring _ (algebraMap P.Ring S)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R P.Ring) (algebraMap R₀ R)))
Tactic: rw [IsScalarTower.algebraMap_eq R₀ R P.Ring, ← RingHom.comp_assoc,
    ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R₀ : Type u_1
inst_3 : CommRing R₀
inst_4 : Algebra R₀ R
inst_5 : Algebra R₀ S
inst_6 : IsScalarTower R₀ R S
rw :
  Eq (α := R₀ →+* S) (algebraMap R₀ S)
    (@RingHom.comp.{u_1, w, v} _ P.Ring _ _ Semiring.toNonAssocSemiring _ (algebraMap P.Ring S)
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R P.Ring) (algebraMap R₀ R)))
⊢ Eq (α := R₀ →+* S) (algebraMap R₀ S)
    (@RingHom.comp.{u_1, w, v} _ P.Ring _ _ Semiring.toNonAssocSemiring _ (algebraMap P.Ring S) (algebraMap R₀ P.Ring))
have rw₁ : Eq (α := R₀ →+* S) (algebraMap R₀ S)
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
    (@RingHom.comp.{u, w, v} _ P.Ring _ _ Semiring.toNonAssocSemiring _ (algebraMap P.Ring S) (algebraMap R P.Ring))
    (algebraMap R₀ R))
Tactic: rw [IsScalarTower.algebraMap_eq R₀ R P.Ring, ← RingHom.comp_assoc,
    ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R₀ : Type u_1
inst_3 : CommRing R₀
inst_4 : Algebra R₀ R
inst_5 : Algebra R₀ S
inst_6 : IsScalarTower R₀ R S
rw :
  Eq (α := R₀ →+* S) (algebraMap R₀ S)
    (@RingHom.comp.{u_1, w, v} _ P.Ring _ _ Semiring.toNonAssocSemiring _ (algebraMap P.Ring S)
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R P.Ring) (algebraMap R₀ R)))
rw₁ :
  Eq (α := R₀ →+* S) (algebraMap R₀ S)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp.{u, w, v} _ P.Ring _ _ Semiring.toNonAssocSemiring _ (algebraMap P.Ring S) (algebraMap R P.Ring))
      (algebraMap R₀ R))
⊢ Eq (α := R₀ →+* S) (algebraMap R₀ S)
    (@RingHom.comp.{u_1, w, v} _ P.Ring _ _ Semiring.toNonAssocSemiring _ (algebraMap P.Ring S) (algebraMap R₀ P.Ring))
have rw₂ : Eq (α := R₀ →+* S) (algebraMap R₀ S)
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R S) (algebraMap R₀ R))
Tactic: rw [IsScalarTower.algebraMap_eq R₀ R P.Ring, ← RingHom.comp_assoc,
    ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R₀ : Type u_1
inst_3 : CommRing R₀
inst_4 : Algebra R₀ R
inst_5 : Algebra R₀ S
inst_6 : IsScalarTower R₀ R S
rw :
  Eq (α := R₀ →+* S) (algebraMap R₀ S)
    (@RingHom.comp.{u_1, w, v} _ P.Ring _ _ Semiring.toNonAssocSemiring _ (algebraMap P.Ring S)
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R P.Ring) (algebraMap R₀ R)))
rw₁ :
  Eq (α := R₀ →+* S) (algebraMap R₀ S)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp.{u, w, v} _ P.Ring _ _ Semiring.toNonAssocSemiring _ (algebraMap P.Ring S) (algebraMap R P.Ring))
      (algebraMap R₀ R))
rw₂ :
  Eq (α := R₀ →+* S) (algebraMap R₀ S)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap R S) (algebraMap R₀ R))
⊢ Eq (α := R₀ →+* S) (algebraMap R₀ S)
    (@RingHom.comp.{u_1, w, v} _ P.Ring _ _ Semiring.toNonAssocSemiring _ (algebraMap P.Ring S) (algebraMap R₀ P.Ring))
have rw₃ : Eq (α := R₀ →+* S) (algebraMap R₀ S) (algebraMap R₀ S)
Tactic: rw [IsScalarTower.algebraMap_eq R₀ R P.Ring, ← RingHom.comp_assoc,
    ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
x y : S
⊢ P.σ x • y = x * y
have rw : HMul.hMul (α := S) ((algebraMap P.Ring S : (a : P.Ring) → S) (P.σ x) : S) y = x * y
Tactic: rw [Algebra.smul_def, algebraMap_σ]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
x y : S
rw : HMul.hMul (α := S) ((algebraMap P.Ring S : (a : P.Ring) → S) (P.σ x) : S) y = x * y
⊢ P.σ x • y = x * y
have rw₁ : x * y = x * y
Tactic: rw [Algebra.smul_def, algebraMap_σ]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
x y : S
e : P.σ x = P.σ y
⊢ x = y
have rw : (algebraMap P.Ring S : (a : P.Ring) → S) (P.σ x) = y
Tactic: rw [← P.algebraMap_σ x, ← P.algebraMap_σ y, e]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
x y : S
e : P.σ x = P.σ y
rw : (algebraMap P.Ring S : (a : P.Ring) → S) (P.σ x) = y
⊢ x = y
have rw₁ : Eq.{v + 1} (α := S) ((algebraMap P.Ring S : (a : P.Ring) → S) (P.σ x) : S)
  ((algebraMap P.Ring S : (a : P.Ring) → S) (P.σ y) : S)
Tactic: rw [← P.algebraMap_σ x, ← P.algebraMap_σ y, e]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
x y : S
e : P.σ x = P.σ y
rw : (algebraMap P.Ring S : (a : P.Ring) → S) (P.σ x) = y
rw₁ :
  Eq.{v + 1} (α := S) ((algebraMap P.Ring S : (a : P.Ring) → S) (P.σ x) : S)
    ((algebraMap P.Ring S : (a : P.Ring) → S) (P.σ y) : S)
⊢ x = y
have rw₂ : Eq.{v + 1} (α := S) ((algebraMap P.Ring S : (a : P.Ring) → S) (P.σ y) : S)
  ((algebraMap P.Ring S : (a : P.Ring) → S) (P.σ y) : S)
Tactic: rw [← P.algebraMap_σ x, ← P.algebraMap_σ y, e]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Extension.{w, u, v} R S
M : Submonoid S
S' : Type u_1
inst_3 : CommRing S'
inst_4 : Algebra S S'
inst_5 : IsLocalization M S'
inst_6 : Algebra R S'
inst_7 : IsScalarTower R S S'
P : Extension.{w, u, v} R S
this : Algebra.{w, u_1} (Localization (Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M)) S' :=
  RingHom.toAlgebra
    (IsLocalization.lift (R := P.Ring) (M := Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M)
      (g := @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (algebraMap P.Ring S)) ⋯)
⊢ IsScalarTower.{u, w, u_1} R (Localization (Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M)) S'
have h : Eq (α := R →+* S') (algebraMap R S')
  (@RingHom.comp.{u, w, u_1} _ (Localization (Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M)) _
    _ Semiring.toNonAssocSemiring _
    (algebraMap (Localization (Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M)) S')
    (algebraMap R (Localization (Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M))))
Tactic: apply IsScalarTower.of_algebraMap_eq'
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Extension.{w, u, v} R S
M : Submonoid S
S' : Type u_1
inst_3 : CommRing S'
inst_4 : Algebra S S'
inst_5 : IsLocalization M S'
inst_6 : Algebra R S'
inst_7 : IsScalarTower R S S'
P : Extension.{w, u, v} R S
this : Algebra.{w, u_1} (Localization (Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M)) S' :=
  RingHom.toAlgebra
    (IsLocalization.lift (R := P.Ring) (M := Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M)
      (g := @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (algebraMap P.Ring S)) ⋯)
⊢ Eq (α := R →+* S') (algebraMap R S')
    (@RingHom.comp.{u, w, u_1} _ (Localization (Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M))
      _ _ Semiring.toNonAssocSemiring _
      (algebraMap (Localization (Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M)) S')
      (algebraMap R (Localization (Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M))))
have h : Eq (α := R →+* S') (algebraMap R S')
  (@RingHom.comp.{u, w, u_1} _ (Localization (Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M)) _
    _ Semiring.toNonAssocSemiring _
    (IsLocalization.lift (R := P.Ring) (M := Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M)
      (g := @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (algebraMap P.Ring S)) sorry)
    (algebraMap R (Localization (Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M))))
Tactic: rw [RingHom.algebraMap_toAlgebra, IsScalarTower.algebraMap_eq R P.Ring (Localization _),
      ← RingHom.comp_assoc, IsLocalization.lift_comp, RingHom.comp_assoc,
      ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Extension.{w, u, v} R S
M : Submonoid S
S' : Type u_1
inst_3 : CommRing S'
inst_4 : Algebra S S'
inst_5 : IsLocalization M S'
inst_6 : Algebra R S'
inst_7 : IsScalarTower R S S'
P : Extension.{w, u, v} R S
this : Algebra.{w, u_1} (Localization (Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M)) S' :=
  RingHom.toAlgebra
    (IsLocalization.lift (R := P.Ring) (M := Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M)
      (g := @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (algebraMap P.Ring S)) ⋯)
h :
  Eq (α := R →+* S') (algebraMap R S')
    (@RingHom.comp.{u, w, u_1} _ (Localization (Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M))
      _ _ Semiring.toNonAssocSemiring _
      (IsLocalization.lift (R := P.Ring) (M := Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M)
        (g := @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (algebraMap P.Ring S)) ⋯)
      (algebraMap R (Localization (Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M))))
⊢ Eq (α := R →+* S') (algebraMap R S')
    (@RingHom.comp.{u, w, u_1} _ (Localization (Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M))
      _ _ Semiring.toNonAssocSemiring _
      (algebraMap (Localization (Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M)) S')
      (algebraMap R (Localization (Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M))))
have h₁ : Eq (α := R →+* S') (algebraMap R S')
  (@RingHom.comp.{u, w, u_1} _ (Localization (Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M)) _
    _ Semiring.toNonAssocSemiring _
    (IsLocalization.lift (R := P.Ring) (M := Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M)
      (g := @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (algebraMap P.Ring S)) sorry)
    (@RingHom.comp _ P.Ring _ _ Semiring.toNonAssocSemiring _
      (algebraMap P.Ring (Localization (Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M)))
      (algebraMap R P.Ring)))
Tactic: rw [RingHom.algebraMap_toAlgebra, IsScalarTower.algebraMap_eq R P.Ring (Localization _),
      ← RingHom.comp_assoc, IsLocalization.lift_comp, RingHom.comp_assoc,
      ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]