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_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'
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)
hf :
  Eq (α := (↑s.pt : Type u)) ((h' : (a : A ⊗[R] B) → (↑s.pt : Type u)) x : (↑s.pt : Type u))
    ((Algebra.TensorProduct.productMap f' g' : (a : A ⊗[R] B) → (↑s.pt : Type u)) x : (↑s.pt : 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))

Tactic:
change h' x = Algebra.TensorProduct.productMap f' g' x

Premises used: Algebra.TensorProduct.productMap, 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_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'
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)
hf hf₁ :
  Eq (α := (↑s.pt : Type u))
    ((Algebra.TensorProduct.productMap f' g' : (a : A ⊗[R] B) → (↑s.pt : Type u)) x : (↑s.pt : Type u))
    ((Algebra.TensorProduct.productMap f' g' : (a : A ⊗[R] B) → (↑s.pt : Type u)) x : (↑s.pt : Type u))
⊢ Eq (α := (↑s.pt : Type u)) ((h' : (a : A ⊗[R] B) → (↑s.pt : Type u)) x : (↑s.pt : Type u))
    ((Algebra.TensorProduct.productMap f' g' : (a : A ⊗[R] B) → (↑s.pt : Type u)) x : (↑s.pt : Type u))

Tactic:
rw [this]
-- 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
h' : A ⊗[R] B →ₐ[R] (↑s.pt : Type u) :=
  let __src := Hom.hom h;
  { toRingHom := __src, commutes' := ⋯ }
property : h' = Algebra.TensorProduct.productMap f' g'
⊢ h = ofHom (Algebra.TensorProduct.productMap f' g').toRingHom

Tactic:
suffices h' = Algebra.TensorProduct.productMap f' g' by
      ext x
      change h' x = Algebra.TensorProduct.productMap f' g' x
      rw [this]
-- 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
h' : A ⊗[R] B →ₐ[R] (↑s.pt : Type u) :=
  let __src := Hom.hom h;
  { toRingHom := __src, commutes' := ⋯ }
property :
  ∀ (a : A) (b : B),
    Eq (α := (↑s.pt : Type u)) ((h' : (a : A ⊗[R] B) → (↑s.pt : Type u)) (a ⊗ₜ[R] b) : (↑s.pt : Type u))
      ((Algebra.TensorProduct.productMap f' g' : (a : A ⊗[R] B) → (↑s.pt : Type u)) (a ⊗ₜ[R] b) : (↑s.pt : Type u))
⊢ h' = Algebra.TensorProduct.productMap f' g'

Tactic:
apply Algebra.TensorProduct.ext'

Premises used: Algebra.TensorProduct.ext'
-- 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
h' : A ⊗[R] B →ₐ[R] (↑s.pt : Type u) :=
  let __src := Hom.hom h;
  { toRingHom := __src, commutes' := ⋯ }
a : A
b : B
property :
  (h' : (a : A ⊗[R] B) → (↑s.pt : Type u)) (a ⊗ₜ[R] b) =
    HMul.hMul (α := (↑s.pt : Type u)) (β := (↑s.pt : Type u))
      ((Hom.hom (ofHom Algebra.TensorProduct.includeLeftRingHom ≫ h) : (a : A) → (↑s.pt : Type u)) a : (↑s.pt : Type u))
      ((Hom.hom (ofHom (↑Algebra.TensorProduct.includeRight : B →+* A ⊗[R] B) ≫ h) : (a : B) → (↑s.pt : Type u)) b :
        (↑s.pt : Type u))
⊢ Eq (α := (↑s.pt : Type u)) ((h' : (a : A ⊗[R] B) → (↑s.pt : Type u)) (a ⊗ₜ[R] b) : (↑s.pt : Type u))
    ((Algebra.TensorProduct.productMap f' g' : (a : A ⊗[R] B) → (↑s.pt : Type u)) (a ⊗ₜ[R] b) : (↑s.pt : Type u))

Tactic:
simp only [f', g', ← eq1, pushoutCocone_pt, ← eq2, AlgHom.toRingHom_eq_coe,
      Algebra.TensorProduct.productMap_apply_tmul, AlgHom.coe_mk]

Premises used: CommRingCat.pushoutCocone_pt, AlgHom.coe_mk, Algebra.TensorProduct.productMap_apply_tmul, AlgHom.toRingHom_eq_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
h' : A ⊗[R] B →ₐ[R] (↑s.pt : Type u) :=
  let __src := Hom.hom h;
  { toRingHom := __src, commutes' := ⋯ }
a : A
b : B
property :
  (h' : (a : A ⊗[R] B) → (↑s.pt : Type u)) (a ⊗ₜ[R] b) =
    HMul.hMul (α := (↑s.pt : Type u)) (β := (↑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))
          (a ⊗ₜ[R] 1) :
        (↑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))
          (1 ⊗ₜ[R] b) :
        (↑s.pt : Type u))
⊢ (h' : (a : A ⊗[R] B) → (↑s.pt : Type u)) (a ⊗ₜ[R] b) =
    HMul.hMul (α := (↑s.pt : Type u)) (β := (↑s.pt : Type u))
      ((Hom.hom (ofHom Algebra.TensorProduct.includeLeftRingHom ≫ h) : (a : A) → (↑s.pt : Type u)) a : (↑s.pt : Type u))
      ((Hom.hom (ofHom (↑Algebra.TensorProduct.includeRight : B →+* A ⊗[R] B) ≫ h) : (a : B) → (↑s.pt : Type u)) b :
        (↑s.pt : Type u))

Tactic:
change _ = h (a ⊗ₜ 1) * h (1 ⊗ₜ b)

Premises used: CategoryTheory.ConcreteCategory.hom, 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
h' : A ⊗[R] B →ₐ[R] (↑s.pt : Type u) :=
  let __src := Hom.hom h;
  { toRingHom := __src, commutes' := ⋯ }
a : A
b : B
property :
  Eq (α := (↑s.pt : Type u)) ((h' : (a : A ⊗[R] B) → (↑s.pt : Type u)) (a ⊗ₜ[R] b) : (↑s.pt : Type u))
    ((Hom.hom h : (a : (↑(pushoutCocone R A B).pt : Type u)) → (↑s.pt : Type u)) (a ⊗ₜ[R] b) : (↑s.pt : Type u))
⊢ (h' : (a : A ⊗[R] B) → (↑s.pt : Type u)) (a ⊗ₜ[R] b) =
    HMul.hMul (α := (↑s.pt : Type u)) (β := (↑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))
          (a ⊗ₜ[R] 1) :
        (↑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))
          (1 ⊗ₜ[R] b) :
        (↑s.pt : Type u))

Tactic:
rw [← h.hom.map_mul, Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul]

Premises used: CommRingCat.Hom.hom, Algebra.TensorProduct.tmul_mul_tmul, RingHom.map_mul, mul_one, one_mul
-- 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
h' : A ⊗[R] B →ₐ[R] (↑s.pt : Type u) :=
  let __src := Hom.hom h;
  { toRingHom := __src, commutes' := ⋯ }
a : A
b : B
⊢ Eq (α := (↑s.pt : Type u)) ((h' : (a : A ⊗[R] B) → (↑s.pt : Type u)) (a ⊗ₜ[R] b) : (↑s.pt : Type u))
    ((Hom.hom h : (a : (↑(pushoutCocone R A B).pt : Type u)) → (↑s.pt : Type u)) (a ⊗ₜ[R] b) : (↑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
hf :
  ∀ (x : (↑(of R) : Type u)),
    Eq (α := (↑(of (A ⊗[R] B)) : Type u))
      ((Hom.hom
              (CategoryStruct.comp (Y := of A) (ofHom (algebraMap R A))
                (ofHom Algebra.TensorProduct.includeLeftRingHom)) :
            (a : (↑(of R) : Type u)) → (↑(of (A ⊗[R] B)) : Type u))
          x :
        (↑(of (A ⊗[R] B)) : Type u))
      ((Hom.hom
              (CategoryStruct.comp (Y := of B) (ofHom (algebraMap R B))
                (ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight))) :
            (a : (↑(of R) : Type u)) → (↑(of (A ⊗[R] B)) : Type u))
          x :
        (↑(of (A ⊗[R] B)) : Type u))
⊢ Eq (α := of R ⟶ of (A ⊗[R] B))
    (CategoryStruct.comp (Y := of A) (ofHom (algebraMap R A)) (ofHom Algebra.TensorProduct.includeLeftRingHom))
    (CategoryStruct.comp (Y := of B) (ofHom (algebraMap R B))
      (ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight)))

Tactic:
ext
-- 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
x : (↑(of R) : Type u)
⊢ Eq (α := (↑(of (A ⊗[R] B)) : Type u))
    ((Hom.hom
            (CategoryStruct.comp (Y := of A) (ofHom (algebraMap R A))
              (ofHom Algebra.TensorProduct.includeLeftRingHom)) :
          (a : (↑(of R) : Type u)) → (↑(of (A ⊗[R] B)) : Type u))
        x :
      (↑(of (A ⊗[R] B)) : Type u))
    ((Hom.hom
            (CategoryStruct.comp (Y := of B) (ofHom (algebraMap R B))
              (ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight))) :
          (a : (↑(of R) : Type u)) → (↑(of (A ⊗[R] B)) : Type u))
        x :
      (↑(of (A ⊗[R] B)) : Type u))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Ring.Constructions
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
⊢ ofHom (algebraMap R S) ≫ Iso.hom (Iso.refl (of S)) = Iso.hom (Iso.refl (of R)) ≫ ofHom (algebraMap R S)

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Ring.Constructions
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
⊢ ofHom (algebraMap R A) ≫ Iso.hom (Iso.refl (of A)) = Iso.hom (Iso.refl (of R)) ≫ ofHom (algebraMap R A)

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Ring.Constructions
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
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))
⊢ 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))

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Ring.Constructions
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
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:
simp [Algebra.IsPushout.equiv_tmul]

Premises used: Algebra.IsPushout.equiv_tmul
-- Module: Mathlib.Algebra.Category.Ring.Constructions
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
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))
⊢ 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))

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Ring.Constructions
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
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:
simp [Algebra.IsPushout.equiv_tmul]

Premises used: Algebra.IsPushout.equiv_tmul
-- 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'
⊢ 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:
⟨fun h ↦ ?_, fun h ↦ isPushout_of_isPushout ..⟩

Premises used: CommRingCat.isPushout_of_isPushout, Iff.intro
-- 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'
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'
⊢ 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 ..⟩