awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Ring.Constructions
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
⊢ ∀ (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))

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)
-- Module: Mathlib.Algebra.Category.Ring.Constructions
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))
⊢ ∀ (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)
-- Module: Mathlib.Algebra.Category.Ring.Constructions
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')
r : R'
⊢ e.toFun ((algebraMap R' (R' ⊗[R] S) : (a : R') → R' ⊗[R] S) r) = (algebraMap R' S' : (a : R') → S') r

Tactic:
simp [Iso.commRingCatIsoToRingEquiv, h2, e, h3]

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv
-- Module: Mathlib.Algebra.Category.Ring.Constructions
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'

Tactic:
Algebra.IsPushout.of_equiv e' ?_

Premises used: Algebra.IsPushout.of_equiv
-- Module: Mathlib.Algebra.Category.Ring.Constructions
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' := ⋯ }
refine : Eq (α := S →+* S') (e'.toRingEquiv.toRingHom.comp (algebraMap S (R' ⊗[R] S))) (algebraMap S S')
⊢ Algebra.IsPushout R R' S S'

Tactic:
refine Algebra.IsPushout.of_equiv e' ?_

Premises used: Algebra.IsPushout.of_equiv
-- Module: Mathlib.Algebra.Category.Ring.Constructions
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' := ⋯ }
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')
⊢ Eq (α := S →+* S') (e'.toRingEquiv.toRingHom.comp (algebraMap S (R' ⊗[R] S))) (algebraMap S S')

Tactic:
ext s
-- Module: Mathlib.Algebra.Category.Ring.Constructions
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ₘ := ⋯
⊢ IsScalarTower R S Sₘ

Tactic:
have : IsScalarTower R S Sₘ := .of_algebraMap_eq' H
-- Module: Mathlib.Algebra.Category.Ring.Constructions
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ₘ
⊢ IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ

Tactic:
have : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ := ‹_›
-- Module: Mathlib.Algebra.Category.Ring.Constructions
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_1 : IsScalarTower R S Sₘ
this : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
⊢ IsPushout (ofHom f) (ofHom (algebraMap R Rₘ)) (ofHom (algebraMap S Sₘ)) (ofHom fₘ)

Tactic:
CommRingCat.isPushout_iff_isPushout.mpr (Algebra.isPushout_of_isLocalization M _ _ _)

Premises used: Iff.mpr, Algebra.isPushout_of_isLocalization, CommRingCat.isPushout_iff_isPushout
-- Module: Mathlib.Algebra.Category.Ring.Constructions
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_1 : IsScalarTower R S Sₘ
this : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
⊢ IsPushout (ofHom f) (ofHom (algebraMap R Rₘ)) (ofHom (algebraMap S Sₘ)) (ofHom fₘ)

Tactic:
exact CommRingCat.isPushout_iff_isPushout.mpr (Algebra.isPushout_of_isLocalization M _ _ _)

Premises used: Iff.mpr, Algebra.isPushout_of_isLocalization, CommRingCat.isPushout_iff_isPushout
-- Module: Mathlib.Algebra.Category.Ring.Constructions
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)
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)) ⋯ 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)))))
⊢ 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))))
    ⊤

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]

Premises used: RingEquiv.injective, Subring.comap_map_eq_self_of_injective, top_le_iff, Subring.map_le_iff_le_comap, RingEquiv.symm, Subring.closure, Set.image_union, RingHom.map_closure