awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Unramified (goal)
Goal:
R S : Type u_3
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_3)),
    (@fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop)) _
      (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f)
algInst : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
r : S
hr : r ∈ s
hrx : Membership.mem (γ := TopologicalSpace.Opens (PrimeSpectrum S)) (PrimeSpectrum.basicOpen r) x
⊢ Algebra.FormallyUnramified R (Localization.Away r) ↔
    FormallyUnramified (S := Localization.Away r) (RingHom.comp (algebraMap S (Localization.Away r)) f)
have a : Algebra.FormallyUnramified R (Localization.Away r) ↔
  FormallyUnramified (S := Localization.Away r)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S (Localization.Away r)) (algebraMap R S))
Tactic: rw [← algebraMap_toAlgebra f, ← IsScalarTower.algebraMap_eq,
    formallyUnramified_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Unramified (goal)
Goal:
R S : Type u_3
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_3)),
    (@fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop)) _
      (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f)
algInst : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
r : S
hr : r ∈ s
hrx : Membership.mem (γ := TopologicalSpace.Opens (PrimeSpectrum S)) (PrimeSpectrum.basicOpen r) x
a :
  Algebra.FormallyUnramified R (Localization.Away r) ↔
    FormallyUnramified (S := Localization.Away r)
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S (Localization.Away r)) (algebraMap R S))
⊢ Algebra.FormallyUnramified R (Localization.Away r) ↔
    FormallyUnramified (S := Localization.Away r) (RingHom.comp (algebraMap S (Localization.Away r)) f)
have a₁ : Algebra.FormallyUnramified R (Localization.Away r) ↔
  FormallyUnramified (S := Localization.Away r) (algebraMap R (Localization.Away r))
Tactic: rw [← algebraMap_toAlgebra f, ← IsScalarTower.algebraMap_eq,
    formallyUnramified_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Unramified (goal)
Goal:
R S : Type u_3
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_3)),
    (@fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop)) _
      (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f)
algInst : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
r : S
hr : r ∈ s
hrx : Membership.mem (γ := TopologicalSpace.Opens (PrimeSpectrum S)) (PrimeSpectrum.basicOpen r) x
a :
  Algebra.FormallyUnramified R (Localization.Away r) ↔
    FormallyUnramified (S := Localization.Away r)
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S (Localization.Away r)) (algebraMap R S))
a₁ :
  Algebra.FormallyUnramified R (Localization.Away r) ↔
    FormallyUnramified (S := Localization.Away r) (algebraMap R (Localization.Away r))
⊢ Algebra.FormallyUnramified R (Localization.Away r) ↔
    FormallyUnramified (S := Localization.Away r) (RingHom.comp (algebraMap S (Localization.Away r)) f)
have a₂ : Algebra.FormallyUnramified R (Localization.Away r) ↔ Algebra.FormallyUnramified R (Localization.Away r)
Tactic: rw [← algebraMap_toAlgebra f, ← IsScalarTower.algebraMap_eq,
    formallyUnramified_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Unramified (goal)
Goal:
⊢ PropertyIsLocal.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ FormallyUnramified
have localizationAwayPreserves : LocalizationAwayPreserves.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ FormallyUnramified
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Unramified (goal)
Goal:
localizationAwayPreserves :
  LocalizationAwayPreserves.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ FormallyUnramified
⊢ PropertyIsLocal.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ FormallyUnramified
have ofLocalizationSpanTarget : OfLocalizationSpanTarget.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ FormallyUnramified
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Unramified (goal)
Goal:
localizationAwayPreserves :
  LocalizationAwayPreserves.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ FormallyUnramified
ofLocalizationSpanTarget :
  OfLocalizationSpanTarget.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ FormallyUnramified
⊢ PropertyIsLocal.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ FormallyUnramified
have ofLocalizationSpan : OfLocalizationSpan.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ FormallyUnramified
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Unramified (goal)
Goal:
localizationAwayPreserves :
  LocalizationAwayPreserves.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ FormallyUnramified
ofLocalizationSpanTarget :
  OfLocalizationSpanTarget.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ FormallyUnramified
ofLocalizationSpan : OfLocalizationSpan.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ FormallyUnramified
⊢ PropertyIsLocal.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ FormallyUnramified
have StableUnderCompositionWithLocalizationAwayTarget : StableUnderCompositionWithLocalizationAwayTarget.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] ↦
  FormallyUnramified
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Unramified (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
T : Type u_3
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : f.FormallyUnramified
h : (g.comp f).FormallyEtale
⊢ g.FormallyEtale
have algebraizeInst : Algebra.FormallyUnramified R S
Tactic: algebraize [f, g, g.comp f]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Unramified (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
T : Type u_3
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : f.FormallyUnramified
h : (g.comp f).FormallyEtale
algebraizeInst : Algebra.FormallyUnramified R S
⊢ g.FormallyEtale
have algebraizeInst₁ : Algebra.FormallyEtale R T
Tactic: algebraize [f, g, g.comp f]
-- Lean 4 proof step from Mathlib.RingTheory.RingHomProperties (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso @P
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
inst : IsIso f
H : P ((CommRingCat.Hom.hom g).comp (CommRingCat.Hom.hom f))
⊢ P (CommRingCat.Hom.hom g)
have h : CommRingCat.Hom.hom g = (CommRingCat.Hom.hom (f ≫ g)).comp (asIso f).symm.commRingCatIsoToRingEquiv.toRingHom
Tactic: convert! hP.2 (f ≫ g).hom (asIso f).symm.commRingCatIsoToRingEquiv H
-- Lean 4 proof step from Mathlib.RingTheory.RingHomProperties (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso @P
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
inst : IsIso g
H : P ((CommRingCat.Hom.hom g).comp (CommRingCat.Hom.hom f))
⊢ P (CommRingCat.Hom.hom f)
have h : CommRingCat.Hom.hom f = (asIso g).symm.commRingCatIsoToRingEquiv.toRingHom.comp (CommRingCat.Hom.hom (f ≫ g))
Tactic: convert! hP.1 (f ≫ g).hom (asIso g).symm.commRingCatIsoToRingEquiv H
-- Lean 4 proof step from Mathlib.RingTheory.RingHomProperties (goal)
Goal:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hQ : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
⊢ RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P f ∧ Q f
have refine_1 : ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (e : S ≃+* T),
  (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P f ∧ Q f) f →
    (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P f ∧ Q f) (e.toRingHom.comp f)
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.RingHomProperties (goal)
Goal:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hQ : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
refine_1 :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (e : S ≃+* T),
    (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P f ∧ Q f) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P f ∧ Q f) (e.toRingHom.comp f)
⊢ RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P f ∧ Q f
have refine_2 : ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : S →+* T) (e : R ≃+* S),
  (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P f ∧ Q f) f →
    (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P f ∧ Q f) (f.comp e.toRingHom)
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.RingHomProperties (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderComposition @P
hP' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), P e.toRingHom
⊢ RespectsIso @P
have left : ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (e : S ≃+* T),
  P f → P (e.toRingHom.comp f)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.RingHomProperties (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderComposition @P
hP' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), P e.toRingHom
left :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (e : S ≃+* T),
    P f → P (e.toRingHom.comp f)
⊢ RespectsIso @P
have right : ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : S →+* T) (e : R ≃+* S),
  P f → P (f.comp e.toRingHom)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.RingHomProperties (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hP : StableUnderComposition @P
hP' : ∀ {R S : Type u} [inst : CommRing R] [inst_3 : CommRing S] (e : R ≃+* S), P e.toRingHom
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
e : S ≃+* T
H left : P f
⊢ P (e.toRingHom.comp f)
have left₁ : P e.toRingHom
Tactic: apply hP
-- Lean 4 proof step from Mathlib.RingTheory.RingHomProperties (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hP : StableUnderComposition @P
hP' : ∀ {R S : Type u} [inst : CommRing R] [inst_3 : CommRing S] (e : R ≃+* S), P e.toRingHom
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : S →+* T
e : R ≃+* S
H : P f
⊢ P (f.comp e.toRingHom)
have right : P e.toRingHom
Tactic: apply hP
-- Lean 4 proof step from Mathlib.RingTheory.RingHomProperties (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_11 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso @P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_11 : CommRing S] [inst_12 : CommRing T] [inst_13 : Algebra R S]
    [inst_14 : Algebra R T], P (algebraMap R T) → P (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
R S R' S' : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R R'
inst_6 : Algebra R S'
inst_7 : Algebra S S'
inst_8 : Algebra R' S'
inst_9 : IsScalarTower R S S'
inst_10 : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
e : R' ⊗[R] S ≃ₛₗ[id R'] S' := IsBaseChange.equiv (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R S S')) ⋯
f' : R' ⊗[R] S →ₐ[R] S' :=
  Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
x : R' ⊗[R] S
⊢ Eq (α := S') ((e : (a : R' ⊗[R] S) → S') x : S') ((f' : (a : R' ⊗[R] S) → S') x : S')
have suffices : (↑R :
      {S M M₂ : Type u} →
        [inst : Semiring R] →
          [inst_11 : Semiring S] →
            [inst_12 : AddCommMonoid M] →
              [inst_13 : AddCommMonoid M₂] →
                [inst_14 : Module R M] →
                  [inst_15 : Module R M₂] →
                    [inst_16 : Module S M] →
                      [inst_17 : Module S M₂] →
                        [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₛₗ[id S] M₂) → M →ₛₗ[id R] M₂)
    (↑e : R' ⊗[R] S →ₛₗ[id R'] S') =
  f'.toLinearMap
Tactic: suffices e.toLinearMap.restrictScalars R = f'.toLinearMap from congr($this x)
-- Lean 4 proof step from Mathlib.RingTheory.RingHomProperties (hypothesis)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_11 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso @P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_11 : CommRing S] [inst_12 : CommRing T] [inst_13 : Algebra R S]
    [inst_14 : Algebra R T], P (algebraMap R T) → P (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
R S R' S' : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R R'
inst_6 : Algebra R S'
inst_7 : Algebra S S'
inst_8 : Algebra R' S'
inst_9 : IsScalarTower R S S'
inst_10 : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
e : R' ⊗[R] S ≃ₛₗ[id R'] S' := IsBaseChange.equiv (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R S S')) ⋯
f' : R' ⊗[R] S →ₐ[R] S' :=
  Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
⊢ P (algebraMap R' S')
have hef : ∀ (x : R' ⊗[R] S), Eq (α := S') ((e : (a : R' ⊗[R] S) → S') x : S') ((f' : (a : R' ⊗[R] S) → S') x : S')
Tactic: have hef (x : _) : e x = f' x := by
    suffices e.toLinearMap.restrictScalars R = f'.toLinearMap from congr($this x)
    exact ext' fun x y ↦ by simp [e, f', IsBaseChange.equiv_tmul, Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.RingHomProperties (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_11 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso @P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_11 : CommRing S] [inst_12 : CommRing T] [inst_13 : Algebra R S]
    [inst_14 : Algebra R T], P (algebraMap R T) → P (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
R S R' S' : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R R'
inst_6 : Algebra R S'
inst_7 : Algebra S S'
inst_8 : Algebra R' S'
inst_9 : IsScalarTower R S S'
inst_10 : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
e : R' ⊗[R] S ≃ₛₗ[id R'] S' := IsBaseChange.equiv (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R S S')) ⋯
f' : R' ⊗[R] S →ₐ[R] S' :=
  Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
hef : ∀ (x : R' ⊗[R] S), Eq (α := S') ((e : (a : R' ⊗[R] S) → S') x : S') ((f' : (a : R' ⊗[R] S) → S') x : S')
x y : R' ⊗[R] S
⊢ (e : (a : R' ⊗[R] S) → S') (x * y) =
    HMul.hMul (α := S') (β := S') ((e : (a : R' ⊗[R] S) → S') x : S') ((e : (a : R' ⊗[R] S) → S') y : S')
have simp_rw : (f' : (a : R' ⊗[R] S) → S') (x * y) =
  HMul.hMul (α := S') (β := S') ((f' : (a : R' ⊗[R] S) → S') x : S') ((f' : (a : R' ⊗[R] S) → S') y : S')
Tactic: simp_rw [hef, map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.RingHomProperties (hypothesis)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_11 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso @P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_11 : CommRing S] [inst_12 : CommRing T] [inst_13 : Algebra R S]
    [inst_14 : Algebra R T], P (algebraMap R T) → P (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
R S R' S' : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R R'
inst_6 : Algebra R S'
inst_7 : Algebra S S'
inst_8 : Algebra R' S'
inst_9 : IsScalarTower R S S'
inst_10 : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
e : R' ⊗[R] S ≃ₛₗ[id R'] S' := IsBaseChange.equiv (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R S S')) ⋯
f' : R' ⊗[R] S →ₐ[R] S' :=
  Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
hef : ∀ (x : R' ⊗[R] S), Eq (α := S') ((e : (a : R' ⊗[R] S) → S') x : S') ((f' : (a : R' ⊗[R] S) → S') x : S')
⊢ P (algebraMap R' S')
have hemul : ∀ (x y : R' ⊗[R] S),
  (e : (a : R' ⊗[R] S) → S') (x * y) =
    HMul.hMul (α := S') (β := S') ((e : (a : R' ⊗[R] S) → S') x : S') ((e : (a : R' ⊗[R] S) → S') y : S')
Tactic: have hemul (x y : _) : e (x * y) = e x * e y := by simp_rw [hef, map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.RingHomProperties (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_11 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso @P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_11 : CommRing S] [inst_12 : CommRing T] [inst_13 : Algebra R S]
    [inst_14 : Algebra R T], P (algebraMap R T) → P (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
R S R' S' : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R R'
inst_6 : Algebra R S'
inst_7 : Algebra S S'
inst_8 : Algebra R' S'
inst_9 : IsScalarTower R S S'
inst_10 : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
e : R' ⊗[R] S ≃ₛₗ[id R'] S' := IsBaseChange.equiv (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R S S')) ⋯
f' : R' ⊗[R] S →ₐ[R] S' :=
  Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
hef : ∀ (x : R' ⊗[R] S), Eq (α := S') ((e : (a : R' ⊗[R] S) → S') x : S') ((f' : (a : R' ⊗[R] S) → S') x : S')
hemul :
  ∀ (x y : R' ⊗[R] S),
    (e : (a : R' ⊗[R] S) → S') (x * y) =
      HMul.hMul (α := S') (β := S') ((e : (a : R' ⊗[R] S) → S') x : S') ((e : (a : R' ⊗[R] S) → S') y : S')
⊢ P (algebraMap R' S')
have h₃ : Eq (α := R' →+* S') (algebraMap R' S')
  ({ toFun := (↑e : R' ⊗[R] S →ₛₗ[id R'] S').toFun, invFun := e.invFun, left_inv := sorry, right_inv := sorry,
          map_mul' := hemul, map_add' := sorry : R' ⊗[R] S ≃+* S' }.toRingHom.comp
    (algebraMap R' (R' ⊗[R] S)))
Tactic: convert! h₁.1 _ { e with map_mul' := hemul } (h₂ H)
-- Lean 4 proof step from Mathlib.RingTheory.RingHomProperties (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_11 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso @P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_11 : CommRing S] [inst_12 : CommRing T] [inst_13 : Algebra R S]
    [inst_14 : Algebra R T], P (algebraMap R T) → P (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
R S R' S' : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R R'
inst_6 : Algebra R S'
inst_7 : Algebra S S'
inst_8 : Algebra R' S'
inst_9 : IsScalarTower R S S'
inst_10 : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
e : R' ⊗[R] S ≃ₛₗ[id R'] S' := IsBaseChange.equiv (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R S S')) ⋯
f' : R' ⊗[R] S →ₐ[R] S' :=
  Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
hef : ∀ (x : R' ⊗[R] S), Eq (α := S') ((e : (a : R' ⊗[R] S) → S') x : S') ((f' : (a : R' ⊗[R] S) → S') x : S')
hemul :
  ∀ (x y : R' ⊗[R] S),
    (e : (a : R' ⊗[R] S) → S') (x * y) =
      HMul.hMul (α := S') (β := S') ((e : (a : R' ⊗[R] S) → S') x : S') ((e : (a : R' ⊗[R] S) → S') y : S')
⊢ Eq (α := R' →+* S') (algebraMap R' S')
    ({ toFun := (↑e : R' ⊗[R] S →ₛₗ[id R'] S').toFun, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯,
            map_mul' := hemul, map_add' := ⋯ : R' ⊗[R] S ≃+* S' }.toRingHom.comp
      (algebraMap R' (R' ⊗[R] S)))
have h₃ : ∀ (x : R'),
  Eq (α := S') ((algebraMap R' S' : (a : R') → S') x : S')
    (({ toFun := (↑e : R' ⊗[R] S →ₛₗ[id R'] S').toFun, invFun := e.invFun, left_inv := sorry, right_inv := sorry,
                  map_mul' := hemul, map_add' := sorry : R' ⊗[R] S ≃+* S' }.toRingHom.comp
            (algebraMap R' (R' ⊗[R] S)) :
          (a : R') → S')
        x :
      S')
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.RingHomProperties (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange @P
hP' : RespectsIso @P
R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
H : P (CommRingCat.Hom.hom g)
this_1 : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom f).toAlgebra
this : Algebra (↑R : Type u) (↑T : Type u) := (CommRingCat.Hom.hom g).toAlgebra
⊢ P (S := (↑(pushout f g) : Type u)) (CommRingCat.Hom.hom (pushout.inl f g))
have rw : P (R := (↑S : Type u)) (S :=
  (↑(Functor.obj
        (Functor.obj (Functor.const WalkingSpan)
          (Cocone.pt (F :=
            span (X := CommRingCat.of (↑R : Type u)) (Y := CommRingCat.of (↑S : Type u)) (Z :=
              CommRingCat.of (↑T : Type u)) (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))
              (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑T : Type u))))
            (ColimitCocone.cocone
              { cocone := CommRingCat.pushoutCocone (↑R : Type u) (↑S : Type u) (↑T : Type u),
                isColimit := CommRingCat.pushoutCoconeIsColimit (↑R : Type u) (↑S : Type u) (↑T : Type u) :
                ColimitCocone
                  (span (X := CommRingCat.of (↑R : Type u)) (Y := CommRingCat.of (↑S : Type u)) (Z :=
                    CommRingCat.of (↑T : Type u)) (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))
                    (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑T : Type u)))) })))
        WalkingSpan.left) :
    Type u))
  (CommRingCat.Hom.hom
    (NatTrans.app
      (Cocone.ι
        (ColimitCocone.cocone
          { cocone := CommRingCat.pushoutCocone (↑R : Type u) (↑S : Type u) (↑T : Type u),
            isColimit := CommRingCat.pushoutCoconeIsColimit (↑R : Type u) (↑S : Type u) (↑T : Type u) }))
      WalkingSpan.left))
Tactic: rw [← show _ = pushout.inl f g from
      colimit.isoColimitCocone_ι_inv ⟨_, CommRingCat.pushoutCoconeIsColimit R S T⟩ WalkingSpan.left,
    CommRingCat.hom_comp, hP'.cancel_right_isIso]