awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
R S A B : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Algebra R S
inst_5 : Algebra S B
inst_6 : Algebra R A
inst_7 : Algebra A B
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : Algebra.IsPushout R S A B
⊢ Eq (α := of S ⟶ of B)
    (CategoryStruct.comp (Y := of (S ⊗[R] A)) (ofHom Algebra.TensorProduct.includeLeftRingHom)
      (Iso.hom (RingEquiv.toCommRingCatIso (AlgEquiv.toRingEquiv (Algebra.IsPushout.equiv R S A B)))))
    (Iso.hom (Iso.refl (of S)) ≫ ofHom (algebraMap S B))
have hf : ∀ (x : (↑(of S) : Type u)),
  Eq (α := (↑(of B) : Type u))
    ((Hom.hom
            (CategoryStruct.comp (Y := of (S ⊗[R] A)) (ofHom Algebra.TensorProduct.includeLeftRingHom)
              (Iso.hom (RingEquiv.toCommRingCatIso (AlgEquiv.toRingEquiv (Algebra.IsPushout.equiv R S A B))))) :
          (a : (↑(of S) : Type u)) → (↑(of B) : Type u))
        x :
      (↑(of B) : Type u))
    ((Hom.hom (Iso.hom (Iso.refl (of S)) ≫ ofHom (algebraMap S B)) : (a : (↑(of S) : Type u)) → (↑(of B) : Type u)) x :
      (↑(of B) : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
R S A B : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Algebra R S
inst_5 : Algebra S B
inst_6 : Algebra R A
inst_7 : Algebra A B
inst_8 : Algebra R B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
inst_11 : Algebra.IsPushout R S A B
⊢ Eq (α := of A ⟶ of B)
    (CategoryStruct.comp (Y := of (S ⊗[R] A)) (ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight))
      (Iso.hom (RingEquiv.toCommRingCatIso (AlgEquiv.toRingEquiv (Algebra.IsPushout.equiv R S A B)))))
    (Iso.hom (Iso.refl (of A)) ≫ ofHom (algebraMap A B))
have hf : ∀ (x : (↑(of A) : Type u)),
  Eq (α := (↑(of B) : Type u))
    ((Hom.hom
            (CategoryStruct.comp (Y := of (S ⊗[R] A)) (ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight))
              (Iso.hom (RingEquiv.toCommRingCatIso (AlgEquiv.toRingEquiv (Algebra.IsPushout.equiv R S A B))))) :
          (a : (↑(of A) : Type u)) → (↑(of B) : Type u))
        x :
      (↑(of B) : Type u))
    ((Hom.hom (Iso.hom (Iso.refl (of A)) ≫ ofHom (algebraMap A B)) : (a : (↑(of A) : Type u)) → (↑(of B) : Type u)) x :
      (↑(of B) : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
R' S' : Type u
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
⊢ IsPushout (Z := of R) (X := of R') (Y := of S) (P := of S') (ofHom (algebraMap R R')) (ofHom (algebraMap R S))
      (ofHom (algebraMap R' S')) (ofHom (algebraMap S S')) ↔
    Algebra.IsPushout R R' S S'
have refine : ∀
  (h :
    IsPushout (Z := of R) (X := of R') (Y := of S) (P := of S') (ofHom (algebraMap R R')) (ofHom (algebraMap R S))
      (ofHom (algebraMap R' S')) (ofHom (algebraMap S S'))),
  Algebra.IsPushout R R' S S'
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ isPushout_of_isPushout ..⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (hypothesis)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
R' S' : Type u
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
h :
  IsPushout (Z := of R) (X := of R') (Y := of S) (P := of S') (ofHom (algebraMap R R')) (ofHom (algebraMap R S))
    (ofHom (algebraMap R' S')) (ofHom (algebraMap S S'))
e : R' ⊗[R] S ≃+* S' :=
  (Iso.trans (Y := pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))
      (IsPushout.isoPushout ⋯) (Iso.symm h.isoPushout)).commRingCatIsoToRingEquiv
⊢ Algebra.IsPushout R R' S S'
have h2 : ∀ (r : R'),
  Eq (α :=
    (↑(pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (X :=
            of (R' ⊗[R] S)) (Y :=
            pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))
            (Iso.hom (IsPushout.isoPushout sorry)) :
          (a : (↑(of (R' ⊗[R] S)) : Type u)) → (↑(pushout (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) : Type u))
        (r ⊗ₜ[R] 1) :
      (↑(pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (X :=
            of R') (Y :=
            pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))
            (pushout.inl (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) :
          (a : (↑(of R') : Type u)) → (↑(pushout (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) : Type u))
        r :
      (↑(pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) : Type u))
Tactic: have h2 (r : R') : (CommRingCat.isPushout_tensorProduct R R' S).isoPushout.hom
      (r ⊗ₜ 1) = (pushout.inl (ofHom _) (ofHom _)) r :=
    congr($((CommRingCat.isPushout_tensorProduct R R' S).inl_isoPushout_hom).hom r)
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (hypothesis)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
R' S' : Type u
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
h :
  IsPushout (Z := of R) (X := of R') (Y := of S) (P := of S') (ofHom (algebraMap R R')) (ofHom (algebraMap R S))
    (ofHom (algebraMap R' S')) (ofHom (algebraMap S S'))
e : R' ⊗[R] S ≃+* S' :=
  (Iso.trans (Y := pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))
      (IsPushout.isoPushout ⋯) (Iso.symm h.isoPushout)).commRingCatIsoToRingEquiv
h2 :
  ∀ (r : R'),
    Eq (α :=
      (↑(pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (X :=
              of (R' ⊗[R] S)) (Y :=
              pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))
              (Iso.hom (IsPushout.isoPushout ⋯)) :
            (a : (↑(of (R' ⊗[R] S)) : Type u)) →
              (↑(pushout (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) : Type u))
          (r ⊗ₜ[R] 1) :
        (↑(pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (X :=
              of R') (Y :=
              pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))
              (pushout.inl (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) :
            (a : (↑(of R') : Type u)) → (↑(pushout (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) : Type u))
          r :
        (↑(pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) : Type u))
⊢ Algebra.IsPushout R R' S S'
have h3 : ∀ (x : R'),
  Eq (α := (↑(of S') : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
            (CategoryStruct.comp (Y :=
              pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))
              (pushout.inl (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) (Iso.inv h.isoPushout)) :
          (a : (↑(of R') : Type u)) → (↑(of S') : Type u))
        x :
      (↑(of S') : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (X :=
            of R') (Y := of S') (ofHom (algebraMap R' S')) :
          (a : (↑(of R') : Type u)) → (↑(of S') : Type u))
        x :
      (↑(of S') : Type u))
Tactic: have h3 (x : R') := congr($(h.inl_isoPushout_inv) x)
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
R' S' : Type u
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
h :
  IsPushout (Z := of R) (X := of R') (Y := of S) (P := of S') (ofHom (algebraMap R R')) (ofHom (algebraMap R S))
    (ofHom (algebraMap R' S')) (ofHom (algebraMap S S'))
e : R' ⊗[R] S ≃+* S' :=
  (Iso.trans (Y := pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))
      (IsPushout.isoPushout ⋯) (Iso.symm h.isoPushout)).commRingCatIsoToRingEquiv
h2 :
  ∀ (r : R'),
    Eq (α :=
      (↑(pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (X :=
              of (R' ⊗[R] S)) (Y :=
              pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))
              (Iso.hom (IsPushout.isoPushout ⋯)) :
            (a : (↑(of (R' ⊗[R] S)) : Type u)) →
              (↑(pushout (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) : Type u))
          (r ⊗ₜ[R] 1) :
        (↑(pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (X :=
              of R') (Y :=
              pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))
              (pushout.inl (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) :
            (a : (↑(of R') : Type u)) → (↑(pushout (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) : Type u))
          r :
        (↑(pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) : Type u))
h3 :
  ∀ (x : R'),
    Eq (α := S')
      ((Hom.hom (Iso.inv h.isoPushout) :
            (a : (↑(pushout (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) : Type u)) → S')
          ((Hom.hom (pushout.inl (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) :
                (a : R') → (↑(pushout (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) : Type u))
              x :
            (↑(pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) :
              Type u)) :
        S')
      ((algebraMap R' S' : (a : R') → S') x : S')
e' : R' ⊗[R] S ≃ₐ[R'] S' :=
  let __spread.0 := e;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ Algebra.IsPushout R R' S S'
have refine : Eq (α := S →+* S') (e'.toRingEquiv.toRingHom.comp (algebraMap S (R' ⊗[R] S))) (algebraMap S S')
Tactic: refine Algebra.IsPushout.of_equiv e' ?_
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
R' S' : Type u
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
h :
  IsPushout (Z := of R) (X := of R') (Y := of S) (P := of S') (ofHom (algebraMap R R')) (ofHom (algebraMap R S))
    (ofHom (algebraMap R' S')) (ofHom (algebraMap S S'))
e : R' ⊗[R] S ≃+* S' :=
  (Iso.trans (Y := pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))
      (IsPushout.isoPushout ⋯) (Iso.symm h.isoPushout)).commRingCatIsoToRingEquiv
h2 :
  ∀ (r : R'),
    Eq (α :=
      (↑(pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (X :=
              of (R' ⊗[R] S)) (Y :=
              pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))
              (Iso.hom (IsPushout.isoPushout ⋯)) :
            (a : (↑(of (R' ⊗[R] S)) : Type u)) →
              (↑(pushout (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) : Type u))
          (r ⊗ₜ[R] 1) :
        (↑(pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (X :=
              of R') (Y :=
              pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))
              (pushout.inl (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) :
            (a : (↑(of R') : Type u)) → (↑(pushout (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) : Type u))
          r :
        (↑(pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) : Type u))
h3 :
  ∀ (x : R'),
    Eq (α := S')
      ((Hom.hom (Iso.inv h.isoPushout) :
            (a : (↑(pushout (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) : Type u)) → S')
          ((Hom.hom (pushout.inl (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) :
                (a : R') → (↑(pushout (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) : Type u))
              x :
            (↑(pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) :
              Type u)) :
        S')
      ((algebraMap R' S' : (a : R') → S') x : S')
e' : R' ⊗[R] S ≃ₐ[R'] S' :=
  let __spread.0 := e;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ Eq (α := S →+* S') (e'.toRingEquiv.toRingHom.comp (algebraMap S (R' ⊗[R] S))) (algebraMap S S')
have a : ∀ (s : S),
  Eq (α := S') ((e'.toRingEquiv.toRingHom.comp (algebraMap S (R' ⊗[R] S)) : (a : S) → S') s : S')
    ((algebraMap S S' : (a : S) → S') s : S')
Tactic: ext s
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (hypothesis)
Goal:
R S Rₘ Sₘ : Type u
inst : CommRing R
inst_1 : CommRing Rₘ
inst_2 : Algebra R Rₘ
inst_3 : CommRing S
inst_4 : CommRing Sₘ
inst_5 : Algebra S Sₘ
f : R →+* S
fₘ : Rₘ →+* Sₘ
H : fₘ.comp (algebraMap R Rₘ) = RingHom.comp (algebraMap S Sₘ) f
M : Submonoid R
inst_6 : IsLocalization M Rₘ
inst_7 : IsLocalization (Submonoid.map f M) Sₘ
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra Rₘ Sₘ := fₘ.toAlgebra
algInst_2 : Algebra R Sₘ := RingHom.toAlgebra (fₘ.comp (algebraMap R Rₘ))
scalarTowerInst : IsScalarTower R Rₘ Sₘ := ⋯
⊢ IsPushout (ofHom f) (ofHom (algebraMap R Rₘ)) (ofHom (algebraMap S Sₘ)) (ofHom fₘ)
have this : IsScalarTower R S Sₘ
Tactic: have : IsScalarTower R S Sₘ := .of_algebraMap_eq' H
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (hypothesis)
Goal:
R S Rₘ Sₘ : Type u
inst : CommRing R
inst_1 : CommRing Rₘ
inst_2 : Algebra R Rₘ
inst_3 : CommRing S
inst_4 : CommRing Sₘ
inst_5 : Algebra S Sₘ
f : R →+* S
fₘ : Rₘ →+* Sₘ
H : fₘ.comp (algebraMap R Rₘ) = RingHom.comp (algebraMap S Sₘ) f
M : Submonoid R
inst_6 : IsLocalization M Rₘ
inst_7 : IsLocalization (Submonoid.map f M) Sₘ
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra Rₘ Sₘ := fₘ.toAlgebra
algInst_2 : Algebra R Sₘ := RingHom.toAlgebra (fₘ.comp (algebraMap R Rₘ))
scalarTowerInst : IsScalarTower R Rₘ Sₘ := ⋯
this : IsScalarTower R S Sₘ
⊢ IsPushout (ofHom f) (ofHom (algebraMap R Rₘ)) (ofHom (algebraMap S Sₘ)) (ofHom fₘ)
have this₁ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
Tactic: have : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ := ‹_›
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
R A B X : CommRingCat
f : R ⟶ A
g : R ⟶ B
a : A ⟶ X
b : B ⟶ X
H : IsPushout f g a b
algInst : Algebra (↑R : Type u) (↑A : Type u) := (Hom.hom f).toAlgebra
algInst_1 : Algebra (↑R : Type u) (↑B : Type u) := (Hom.hom g).toAlgebra
e : (↑(of ((↑A : Type u) ⊗[(↑R : Type u)] (↑B : Type u))) : Type u) ≃+* (↑X : Type u) :=
  Iso.commRingCatIsoToRingEquiv
    (IsPushout.isoIsPushout A B (inl := ofHom Algebra.TensorProduct.includeLeftRingHom) (inr :=
      ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight)) ⋯ H)
⊢ Eq (α := Subring (↑X : Type u))
    (Subring.closure
      (Set.range (ι := (↑A : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
                a) :
            (a : (↑A : Type u)) → (↑X : Type u)) ∪
        Set.range (ι := (↑B : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
                b) :
            (a : (↑B : Type u)) → (↑X : Type u))))
    ⊤
have rw : LE.le (α := Subring (↑(of ((↑A : Type u) ⊗[(↑R : Type u)] (↑B : Type u))) : Type u))
  (Subring.map (R := (↑X : Type u))
    (Hom.hom
      (Iso.inv
        (IsPushout.isoIsPushout A B (inl := ofHom Algebra.TensorProduct.includeLeftRingHom) (inr :=
          ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight)) sorry H)))
    ⊤)
  (Subring.closure
    (Set.image (α := (↑X : Type u))
        (⇑(Hom.hom
              (Iso.inv
                (IsPushout.isoIsPushout A B (inl := ofHom Algebra.TensorProduct.includeLeftRingHom) (inr :=
                  ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight)) sorry H))) :
          (a : (↑X : Type u)) → (↑(of ((↑A : Type u) ⊗[(↑R : Type u)] (↑B : Type u))) : Type u))
        (Set.range (ι := (↑A : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
                a) :
            (a : (↑A : Type u)) → (↑X : Type u))) ∪
      Set.image (α := (↑X : Type u))
        (⇑(Hom.hom
              (Iso.inv
                (IsPushout.isoIsPushout A B (inl := ofHom Algebra.TensorProduct.includeLeftRingHom) (inr :=
                  ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight)) sorry H))) :
          (a : (↑X : Type u)) → (↑(of ((↑A : Type u) ⊗[(↑R : Type u)] (↑B : Type u))) : Type u))
        (Set.range (ι := (↑B : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
                b) :
            (a : (↑B : Type u)) → (↑X : Type u)))))
Tactic: rw [← Subring.comap_map_eq_self_of_injective e.symm.injective (.closure _), RingHom.map_closure,
    ← top_le_iff, ← Subring.map_le_iff_le_comap, Set.image_union]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
R A B X : CommRingCat
f : R ⟶ A
g : R ⟶ B
a : A ⟶ X
b : B ⟶ X
H : IsPushout f g a b
algInst : Algebra (↑R : Type u) (↑A : Type u) := (Hom.hom f).toAlgebra
algInst_1 : Algebra (↑R : Type u) (↑B : Type u) := (Hom.hom g).toAlgebra
e : (↑(of ((↑A : Type u) ⊗[(↑R : Type u)] (↑B : Type u))) : Type u) ≃+* (↑X : Type u) :=
  Iso.commRingCatIsoToRingEquiv
    (IsPushout.isoIsPushout A B (inl := ofHom Algebra.TensorProduct.includeLeftRingHom) (inr :=
      ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight)) ⋯ H)
⊢ LE.le (α := Subring (↑(of ((↑A : Type u) ⊗[(↑R : Type u)] (↑B : Type u))) : Type u))
    (Subring.map (R := (↑X : Type u))
      (Hom.hom
        (Iso.inv
          (IsPushout.isoIsPushout A B (inl := ofHom Algebra.TensorProduct.includeLeftRingHom) (inr :=
            ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight)) ⋯ H)))
      ⊤)
    (Subring.closure
      (Set.image (α := (↑X : Type u))
          (⇑(Hom.hom
                (Iso.inv
                  (IsPushout.isoIsPushout A B (inl := ofHom Algebra.TensorProduct.includeLeftRingHom) (inr :=
                    ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight)) ⋯ H))) :
            (a : (↑X : Type u)) → (↑(of ((↑A : Type u) ⊗[(↑R : Type u)] (↑B : Type u))) : Type u))
          (Set.range (ι := (↑A : Type u))
            (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  carrier) a) :
              (a : (↑A : Type u)) → (↑X : Type u))) ∪
        Set.image (α := (↑X : Type u))
          (⇑(Hom.hom
                (Iso.inv
                  (IsPushout.isoIsPushout A B (inl := ofHom Algebra.TensorProduct.includeLeftRingHom) (inr :=
                    ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight)) ⋯ H))) :
            (a : (↑X : Type u)) → (↑(of ((↑A : Type u) ⊗[(↑R : Type u)] (↑B : Type u))) : Type u))
          (Set.range (ι := (↑B : Type u))
            (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  carrier) b) :
              (a : (↑B : Type u)) → (↑X : Type u)))))
have simp : Subring.map (Hom.hom (IsPushout.isoIsPushout A B sorry H).inv) ⊤ ≤
  Subring.closure
    (Set.range (ι := (↑A : Type u))
        (⇑((Hom.hom (IsPushout.isoIsPushout A B sorry H).inv).comp
              (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                carrier) a)) :
          (a : (↑A : Type u)) → (↑A : Type u) ⊗[(↑R : Type u)] (↑B : Type u)) ∪
      Set.range (ι := (↑B : Type u))
        (⇑((Hom.hom (IsPushout.isoIsPushout A B sorry H).inv).comp
              (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                carrier) b)) :
          (a : (↑B : Type u)) → (↑A : Type u) ⊗[(↑R : Type u)] (↑B : Type u)))
Tactic: simp only [AlgHom.toRingHom_eq_coe, ← Set.range_comp, ← RingHom.coe_comp]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
R A B X : CommRingCat
f : R ⟶ A
g : R ⟶ B
a : A ⟶ X
b : B ⟶ X
H : IsPushout f g a b
algInst : Algebra (↑R : Type u) (↑A : Type u) := (Hom.hom f).toAlgebra
algInst_1 : Algebra (↑R : Type u) (↑B : Type u) := (Hom.hom g).toAlgebra
e : (↑(of ((↑A : Type u) ⊗[(↑R : Type u)] (↑B : Type u))) : Type u) ≃+* (↑X : Type u) :=
  Iso.commRingCatIsoToRingEquiv
    (IsPushout.isoIsPushout A B (inl := ofHom Algebra.TensorProduct.includeLeftRingHom) (inr :=
      ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight)) ⋯ H)
⊢ Subring.map (Hom.hom (IsPushout.isoIsPushout A B ⋯ H).inv) ⊤ ≤
    Subring.closure
      (Set.range (ι := (↑A : Type u))
          (⇑((Hom.hom (IsPushout.isoIsPushout A B ⋯ H).inv).comp
                (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  carrier) a)) :
            (a : (↑A : Type u)) → (↑A : Type u) ⊗[(↑R : Type u)] (↑B : Type u)) ∪
        Set.range (ι := (↑B : Type u))
          (⇑((Hom.hom (IsPushout.isoIsPushout A B ⋯ H).inv).comp
                (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  carrier) b)) :
            (a : (↑B : Type u)) → (↑A : Type u) ⊗[(↑R : Type u)] (↑B : Type u)))
have rw : Subring.map (Hom.hom (IsPushout.isoIsPushout A B sorry H).inv) ⊤ ≤
  Subring.closure
    (Set.range (ι := (↑A : Type u))
        (⇑Algebra.TensorProduct.includeLeftRingHom :
          (a : (↑A : Type u)) → (↑A : Type u) ⊗[(↑R : Type u)] (↑B : Type u)) ∪
      Set.range (ι := (↑B : Type u))
        (⇑(↑Algebra.TensorProduct.includeRight : (↑B : Type u) →+* (↑A : Type u) ⊗[(↑R : Type u)] (↑B : Type u)) :
          (a : (↑B : Type u)) → (↑A : Type u) ⊗[(↑R : Type u)] (↑B : Type u)))
Tactic: rw [← hom_comp, ← hom_comp, IsPushout.inl_isoIsPushout_inv, IsPushout.inr_isoIsPushout_inv,
    hom_ofHom, hom_ofHom]