awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
R A B : Type u
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : PushoutCocone (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
this_1 : Algebra R (↑s.pt : Type u) := RingHom.toAlgebra ((Hom.hom s.inl).comp (algebraMap R A))
f' : A →ₐ[R] (↑s.pt : Type u) :=
  let __src := Hom.hom s.inl;
  { toRingHom := __src, commutes' := ⋯ }
g' : B →ₐ[R] (↑s.pt : Type u) :=
  let __src := Hom.hom s.inr;
  { toRingHom := __src, commutes' := ⋯ }
this : Algebra R
  (↑(Cocone.pt (F := span (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B)))
        (pushoutCocone R A B)) :
    Type u) :=
  have this : Algebra R (A ⊗[R] B) := inferInstance;
  this
property :
  ofHom Algebra.TensorProduct.includeLeftRingHom ≫ ofHom (Algebra.TensorProduct.productMap f' g').toRingHom = s.inl
property₁ :
  ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight) ≫
        ofHom (Algebra.TensorProduct.productMap f' g').toRingHom =
      s.inr ∧
    ∀
      {m :
        Cocone.pt (F := span (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B)))
            (pushoutCocone R A B) ⟶
          s.pt},
      ofHom Algebra.TensorProduct.includeLeftRingHom ≫ m = s.inl →
        ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight) ≫ m = s.inr →
          m = ofHom (Algebra.TensorProduct.productMap f' g').toRingHom
⊢ ofHom Algebra.TensorProduct.includeLeftRingHom ≫ ofHom (Algebra.TensorProduct.productMap f' g').toRingHom = s.inl ∧
    ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight) ≫
          ofHom (Algebra.TensorProduct.productMap f' g').toRingHom =
        s.inr ∧
      ∀
        {m :
          Cocone.pt (F := span (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B)))
              (pushoutCocone R A B) ⟶
            s.pt},
        ofHom Algebra.TensorProduct.includeLeftRingHom ≫ m = s.inl →
          ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight) ≫ m = s.inr →
            m = ofHom (Algebra.TensorProduct.productMap f' g').toRingHom

Tactic:
constructor
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
R A B : Type u
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : PushoutCocone (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
this_1 : Algebra R (↑s.pt : Type u) := RingHom.toAlgebra ((Hom.hom s.inl).comp (algebraMap R A))
f' : A →ₐ[R] (↑s.pt : Type u) :=
  let __src := Hom.hom s.inl;
  { toRingHom := __src, commutes' := ⋯ }
g' : B →ₐ[R] (↑s.pt : Type u) :=
  let __src := Hom.hom s.inr;
  { toRingHom := __src, commutes' := ⋯ }
this : Algebra R
  (↑(Cocone.pt (F := span (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B)))
        (pushoutCocone R A B)) :
    Type u) :=
  have this : Algebra R (A ⊗[R] B) := inferInstance;
  this
property :
  ∀ (x : (↑(of A) : Type u)),
    Eq (α := (↑s.pt : Type u))
      ((Hom.hom
              (ofHom Algebra.TensorProduct.includeLeftRingHom ≫
                ofHom (Algebra.TensorProduct.productMap f' g').toRingHom) :
            (a : (↑(of A) : Type u)) → (↑s.pt : Type u))
          x :
        (↑s.pt : Type u))
      ((Hom.hom s.inl : (a : (↑(of A) : Type u)) → (↑s.pt : Type u)) x : (↑s.pt : Type u))
⊢ ofHom Algebra.TensorProduct.includeLeftRingHom ≫ ofHom (Algebra.TensorProduct.productMap f' g').toRingHom = s.inl

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
R A B : Type u
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : PushoutCocone (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
this_1 : Algebra R (↑s.pt : Type u) := RingHom.toAlgebra ((Hom.hom s.inl).comp (algebraMap R A))
f' : A →ₐ[R] (↑s.pt : Type u) :=
  let __src := Hom.hom s.inl;
  { toRingHom := __src, commutes' := ⋯ }
g' : B →ₐ[R] (↑s.pt : Type u) :=
  let __src := Hom.hom s.inr;
  { toRingHom := __src, commutes' := ⋯ }
this : Algebra R
  (↑(Cocone.pt (F := span (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B)))
        (pushoutCocone R A B)) :
    Type u) :=
  have this : Algebra R (A ⊗[R] B) := inferInstance;
  this
x : (↑(of A) : Type u)
⊢ Eq (α := (↑s.pt : Type u))
    ((Hom.hom
            (ofHom Algebra.TensorProduct.includeLeftRingHom ≫
              ofHom (Algebra.TensorProduct.productMap f' g').toRingHom) :
          (a : (↑(of A) : Type u)) → (↑s.pt : Type u))
        x :
      (↑s.pt : Type u))
    ((Hom.hom s.inl : (a : (↑(of A) : Type u)) → (↑s.pt : Type u)) x : (↑s.pt : Type u))

Tactic:
Algebra.TensorProduct.productMap_left_apply (A := A) _ _ x

Premises used: Quotient.liftOn', AddCon.liftOn, Algebra.TensorProduct.productMap_left_apply, List.foldl, FreeAddMonoid.sumAux
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
R A B : Type u
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : PushoutCocone (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
this_1 : Algebra R (↑s.pt : Type u) := RingHom.toAlgebra ((Hom.hom s.inl).comp (algebraMap R A))
f' : A →ₐ[R] (↑s.pt : Type u) :=
  let __src := Hom.hom s.inl;
  { toRingHom := __src, commutes' := ⋯ }
g' : B →ₐ[R] (↑s.pt : Type u) :=
  let __src := Hom.hom s.inr;
  { toRingHom := __src, commutes' := ⋯ }
this : Algebra R
  (↑(Cocone.pt (F := span (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B)))
        (pushoutCocone R A B)) :
    Type u) :=
  have this : Algebra R (A ⊗[R] B) := inferInstance;
  this
x : (↑(of A) : Type u)
⊢ Eq (α := (↑s.pt : Type u))
    ((Hom.hom
            (ofHom Algebra.TensorProduct.includeLeftRingHom ≫
              ofHom (Algebra.TensorProduct.productMap f' g').toRingHom) :
          (a : (↑(of A) : Type u)) → (↑s.pt : Type u))
        x :
      (↑s.pt : Type u))
    ((Hom.hom s.inl : (a : (↑(of A) : Type u)) → (↑s.pt : Type u)) x : (↑s.pt : Type u))

Tactic:
exact Algebra.TensorProduct.productMap_left_apply (A := A) _ _ x

Premises used: Algebra.TensorProduct.productMap_left_apply
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
R A B : Type u
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : PushoutCocone (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
this_1 : Algebra R (↑s.pt : Type u) := RingHom.toAlgebra ((Hom.hom s.inl).comp (algebraMap R A))
f' : A →ₐ[R] (↑s.pt : Type u) :=
  let __src := Hom.hom s.inl;
  { toRingHom := __src, commutes' := ⋯ }
g' : B →ₐ[R] (↑s.pt : Type u) :=
  let __src := Hom.hom s.inr;
  { toRingHom := __src, commutes' := ⋯ }
this : Algebra R
  (↑(Cocone.pt (F := span (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B)))
        (pushoutCocone R A B)) :
    Type u) :=
  have this : Algebra R (A ⊗[R] B) := inferInstance;
  this
property :
  ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight) ≫
      ofHom (Algebra.TensorProduct.productMap f' g').toRingHom =
    s.inr
property₁ :
  ∀
    {m :
      Cocone.pt (F := span (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B)))
          (pushoutCocone R A B) ⟶
        s.pt},
    ofHom Algebra.TensorProduct.includeLeftRingHom ≫ m = s.inl →
      ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight) ≫ m = s.inr →
        m = ofHom (Algebra.TensorProduct.productMap f' g').toRingHom
⊢ ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight) ≫
        ofHom (Algebra.TensorProduct.productMap f' g').toRingHom =
      s.inr ∧
    ∀
      {m :
        Cocone.pt (F := span (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B)))
            (pushoutCocone R A B) ⟶
          s.pt},
      ofHom Algebra.TensorProduct.includeLeftRingHom ≫ m = s.inl →
        ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight) ≫ m = s.inr →
          m = ofHom (Algebra.TensorProduct.productMap f' g').toRingHom

Tactic:
constructor
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
R A B : Type u
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : PushoutCocone (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
this_1 : Algebra R (↑s.pt : Type u) := RingHom.toAlgebra ((Hom.hom s.inl).comp (algebraMap R A))
f' : A →ₐ[R] (↑s.pt : Type u) :=
  let __src := Hom.hom s.inl;
  { toRingHom := __src, commutes' := ⋯ }
g' : B →ₐ[R] (↑s.pt : Type u) :=
  let __src := Hom.hom s.inr;
  { toRingHom := __src, commutes' := ⋯ }
this : Algebra R
  (↑(Cocone.pt (F := span (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B)))
        (pushoutCocone R A B)) :
    Type u) :=
  have this : Algebra R (A ⊗[R] B) := inferInstance;
  this
property :
  ∀ (x : (↑(of B) : Type u)),
    Eq (α := (↑s.pt : Type u))
      ((Hom.hom
              (ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight) ≫
                ofHom (Algebra.TensorProduct.productMap f' g').toRingHom) :
            (a : (↑(of B) : Type u)) → (↑s.pt : Type u))
          x :
        (↑s.pt : Type u))
      ((Hom.hom s.inr : (a : (↑(of B) : Type u)) → (↑s.pt : Type u)) x : (↑s.pt : Type u))
⊢ ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight) ≫
      ofHom (Algebra.TensorProduct.productMap f' g').toRingHom =
    s.inr

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
R A B : Type u
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : PushoutCocone (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
this_1 : Algebra R (↑s.pt : Type u) := RingHom.toAlgebra ((Hom.hom s.inl).comp (algebraMap R A))
f' : A →ₐ[R] (↑s.pt : Type u) :=
  let __src := Hom.hom s.inl;
  { toRingHom := __src, commutes' := ⋯ }
g' : B →ₐ[R] (↑s.pt : Type u) :=
  let __src := Hom.hom s.inr;
  { toRingHom := __src, commutes' := ⋯ }
this : Algebra R
  (↑(Cocone.pt (F := span (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B)))
        (pushoutCocone R A B)) :
    Type u) :=
  have this : Algebra R (A ⊗[R] B) := inferInstance;
  this
x : (↑(of B) : Type u)
⊢ Eq (α := (↑s.pt : Type u))
    ((Hom.hom
            (ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight) ≫
              ofHom (Algebra.TensorProduct.productMap f' g').toRingHom) :
          (a : (↑(of B) : Type u)) → (↑s.pt : Type u))
        x :
      (↑s.pt : Type u))
    ((Hom.hom s.inr : (a : (↑(of B) : Type u)) → (↑s.pt : Type u)) x : (↑s.pt : Type u))

Tactic:
Algebra.TensorProduct.productMap_right_apply (B := B) _ _ x

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, Algebra.TensorProduct.productMap_right_apply, FreeAddMonoid.sumAux
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
R A B : Type u
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : PushoutCocone (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
this_1 : Algebra R (↑s.pt : Type u) := RingHom.toAlgebra ((Hom.hom s.inl).comp (algebraMap R A))
f' : A →ₐ[R] (↑s.pt : Type u) :=
  let __src := Hom.hom s.inl;
  { toRingHom := __src, commutes' := ⋯ }
g' : B →ₐ[R] (↑s.pt : Type u) :=
  let __src := Hom.hom s.inr;
  { toRingHom := __src, commutes' := ⋯ }
this : Algebra R
  (↑(Cocone.pt (F := span (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B)))
        (pushoutCocone R A B)) :
    Type u) :=
  have this : Algebra R (A ⊗[R] B) := inferInstance;
  this
x : (↑(of B) : Type u)
⊢ Eq (α := (↑s.pt : Type u))
    ((Hom.hom
            (ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight) ≫
              ofHom (Algebra.TensorProduct.productMap f' g').toRingHom) :
          (a : (↑(of B) : Type u)) → (↑s.pt : Type u))
        x :
      (↑s.pt : Type u))
    ((Hom.hom s.inr : (a : (↑(of B) : Type u)) → (↑s.pt : Type u)) x : (↑s.pt : Type u))

Tactic:
exact Algebra.TensorProduct.productMap_right_apply (B := B) _ _ x

Premises used: Algebra.TensorProduct.productMap_right_apply
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
R A B : Type u
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : PushoutCocone (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
this_1 : Algebra R (↑s.pt : Type u) := RingHom.toAlgebra ((Hom.hom s.inl).comp (algebraMap R A))
f' : A →ₐ[R] (↑s.pt : Type u) :=
  let __src := Hom.hom s.inl;
  { toRingHom := __src, commutes' := ⋯ }
g' : B →ₐ[R] (↑s.pt : Type u) :=
  let __src := Hom.hom s.inr;
  { toRingHom := __src, commutes' := ⋯ }
this : Algebra R
  (↑(Cocone.pt (F := span (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B)))
        (pushoutCocone R A B)) :
    Type u) :=
  have this : Algebra R (A ⊗[R] B) := inferInstance;
  this
h :
  Cocone.pt (F := span (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B)))
      (pushoutCocone R A B) ⟶
    s.pt
eq1 : ofHom Algebra.TensorProduct.includeLeftRingHom ≫ h = s.inl
eq2 : ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight) ≫ h = s.inr
r : R
change :
  Eq (α := (↑s.pt : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) h :
          (a : (↑(pushoutCocone R A B).pt : Type u)) → (↑s.pt : Type u))
        ((algebraMap R A : (a : R) → A) r ⊗ₜ[R] 1 : A ⊗[R] B) :
      (↑s.pt : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) s.inl :
          (a : (↑(of A) : Type u)) → (↑s.pt : Type u))
        ((algebraMap R A : (a : R) → A) r : A) :
      (↑s.pt : Type u))
⊢ (↑(↑(Hom.hom h) : (↑(pushoutCocone R A B).pt : Type u) →* (↑s.pt : Type u)) :
          OneHom (↑(pushoutCocone R A B).pt : Type u) (↑s.pt : Type u)).toFun
      ((algebraMap R (A ⊗[R] B) : (a : R) → A ⊗[R] B) r) =
    (algebraMap R (↑s.pt : Type u) : (a : R) → (↑s.pt : Type u)) r

Tactic:
change h (algebraMap R A r ⊗ₜ[R] 1) = s.inl (algebraMap R A r)

Premises used: Algebra.algebraMap, CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.PushoutCocone.inl, TensorProduct.tmul, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
R A B : Type u
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : PushoutCocone (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
this_1 : Algebra R (↑s.pt : Type u) := RingHom.toAlgebra ((Hom.hom s.inl).comp (algebraMap R A))
f' : A →ₐ[R] (↑s.pt : Type u) :=
  let __src := Hom.hom s.inl;
  { toRingHom := __src, commutes' := ⋯ }
g' : B →ₐ[R] (↑s.pt : Type u) :=
  let __src := Hom.hom s.inr;
  { toRingHom := __src, commutes' := ⋯ }
this : Algebra R
  (↑(Cocone.pt (F := span (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B)))
        (pushoutCocone R A B)) :
    Type u) :=
  have this : Algebra R (A ⊗[R] B) := inferInstance;
  this
h :
  Cocone.pt (F := span (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B)))
      (pushoutCocone R A B) ⟶
    s.pt
eq1 : ofHom Algebra.TensorProduct.includeLeftRingHom ≫ h = s.inl
eq2 : ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight) ≫ h = s.inr
r : R
rw :
  Eq (α := (↑s.pt : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) h :
          (a : (↑(pushoutCocone R A B).pt : Type u)) → (↑s.pt : Type u))
        ((algebraMap R A : (a : R) → A) r ⊗ₜ[R] 1 : A ⊗[R] B) :
      (↑s.pt : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (X :=
            of A) (ofHom Algebra.TensorProduct.includeLeftRingHom ≫ h) :
          (a : (↑(of A) : Type u)) → (↑s.pt : Type u))
        ((algebraMap R A : (a : R) → A) r : A) :
      (↑s.pt : Type u))
⊢ Eq (α := (↑s.pt : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) h :
          (a : (↑(pushoutCocone R A B).pt : Type u)) → (↑s.pt : Type u))
        ((algebraMap R A : (a : R) → A) r ⊗ₜ[R] 1 : A ⊗[R] B) :
      (↑s.pt : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) s.inl :
          (a : (↑(of A) : Type u)) → (↑s.pt : Type u))
        ((algebraMap R A : (a : R) → A) r : A) :
      (↑s.pt : Type u))

Tactic:
rw [← eq1]
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
R A B : Type u
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : PushoutCocone (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
this_1 : Algebra R (↑s.pt : Type u) := RingHom.toAlgebra ((Hom.hom s.inl).comp (algebraMap R A))
f' : A →ₐ[R] (↑s.pt : Type u) :=
  let __src := Hom.hom s.inl;
  { toRingHom := __src, commutes' := ⋯ }
g' : B →ₐ[R] (↑s.pt : Type u) :=
  let __src := Hom.hom s.inr;
  { toRingHom := __src, commutes' := ⋯ }
this : Algebra R
  (↑(Cocone.pt (F := span (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B)))
        (pushoutCocone R A B)) :
    Type u) :=
  have this : Algebra R (A ⊗[R] B) := inferInstance;
  this
h :
  Cocone.pt (F := span (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B)))
      (pushoutCocone R A B) ⟶
    s.pt
eq1 : ofHom Algebra.TensorProduct.includeLeftRingHom ≫ h = s.inl
eq2 : ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight) ≫ h = s.inr
r : R
simp :
  Eq (α := (↑s.pt : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) h :
          (a : A ⊗[R] B) → (↑s.pt : Type u))
        ((algebraMap R A : (a : R) → A) r ⊗ₜ[R] 1 : A ⊗[R] B) :
      (↑s.pt : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (X :=
            of A) (ofHom Algebra.TensorProduct.includeLeftRingHom ≫ h) :
          (a : A) → (↑s.pt : Type u))
        ((algebraMap R A : (a : R) → A) r : A) :
      (↑s.pt : Type u))
⊢ Eq (α := (↑s.pt : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) h :
          (a : (↑(pushoutCocone R A B).pt : Type u)) → (↑s.pt : Type u))
        ((algebraMap R A : (a : R) → A) r ⊗ₜ[R] 1 : A ⊗[R] B) :
      (↑s.pt : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (X :=
            of A) (ofHom Algebra.TensorProduct.includeLeftRingHom ≫ h) :
          (a : (↑(of A) : Type u)) → (↑s.pt : Type u))
        ((algebraMap R A : (a : R) → A) r : A) :
      (↑s.pt : Type u))

Tactic:
simp only [pushoutCocone_pt, coe_of]

Premises used: CommRingCat.pushoutCocone_pt, CommRingCat.coe_of
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
R A B : Type u
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : PushoutCocone (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
this_1 : Algebra R (↑s.pt : Type u) := RingHom.toAlgebra ((Hom.hom s.inl).comp (algebraMap R A))
f' : A →ₐ[R] (↑s.pt : Type u) :=
  let __src := Hom.hom s.inl;
  { toRingHom := __src, commutes' := ⋯ }
g' : B →ₐ[R] (↑s.pt : Type u) :=
  let __src := Hom.hom s.inr;
  { toRingHom := __src, commutes' := ⋯ }
this : Algebra R
  (↑(Cocone.pt (F := span (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B)))
        (pushoutCocone R A B)) :
    Type u) :=
  have this : Algebra R (A ⊗[R] B) := inferInstance;
  this
h :
  Cocone.pt (F := span (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B)))
      (pushoutCocone R A B) ⟶
    s.pt
eq1 : ofHom Algebra.TensorProduct.includeLeftRingHom ≫ h = s.inl
eq2 : ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight) ≫ h = s.inr
r : R
⊢ Eq (α := (↑s.pt : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) h :
          (a : A ⊗[R] B) → (↑s.pt : Type u))
        ((algebraMap R A : (a : R) → A) r ⊗ₜ[R] 1 : A ⊗[R] B) :
      (↑s.pt : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (X :=
            of A) (ofHom Algebra.TensorProduct.includeLeftRingHom ≫ h) :
          (a : A) → (↑s.pt : Type u))
        ((algebraMap R A : (a : R) → A) r : A) :
      (↑s.pt : Type u))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
R A B : Type u
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : PushoutCocone (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
this_1 : Algebra R (↑s.pt : Type u) := RingHom.toAlgebra ((Hom.hom s.inl).comp (algebraMap R A))
f' : A →ₐ[R] (↑s.pt : Type u) :=
  let __src := Hom.hom s.inl;
  { toRingHom := __src, commutes' := ⋯ }
g' : B →ₐ[R] (↑s.pt : Type u) :=
  let __src := Hom.hom s.inr;
  { toRingHom := __src, commutes' := ⋯ }
this_2 : Algebra R
  (↑(Cocone.pt (F := span (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B)))
        (pushoutCocone R A B)) :
    Type u) :=
  have this : Algebra R (A ⊗[R] B) := inferInstance;
  this
h :
  Cocone.pt (F := span (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B)))
      (pushoutCocone R A B) ⟶
    s.pt
eq1 : ofHom Algebra.TensorProduct.includeLeftRingHom ≫ h = s.inl
eq2 : ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight) ≫ h = s.inr
h' : A ⊗[R] B →ₐ[R] (↑s.pt : Type u) :=
  let __src := Hom.hom h;
  { toRingHom := __src, commutes' := ⋯ }
this : h' = Algebra.TensorProduct.productMap f' g'
hf :
  ∀
    (x :
      (↑(Cocone.pt (F := span (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B)))
            (pushoutCocone R A B)) :
        Type u)),
    Eq (α := (↑s.pt : Type u))
      ((Hom.hom h : (a : (↑(pushoutCocone R A B).pt : Type u)) → (↑s.pt : Type u)) x : (↑s.pt : Type u))
      ((Hom.hom (ofHom (Algebra.TensorProduct.productMap f' g').toRingHom) :
            (a : (↑(pushoutCocone R A B).pt : Type u)) → (↑s.pt : Type u))
          x :
        (↑s.pt : Type u))
⊢ h = ofHom (Algebra.TensorProduct.productMap f' g').toRingHom

Tactic:
ext x