awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
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
⊢ (↑(↑(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
have 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))
Tactic: change h (algebraMap R A r ⊗ₜ[R] 1) = s.inl (algebraMap R A r)
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
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 : (↑(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))
have 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))
Tactic: rw [← eq1]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
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 : (↑(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))
have 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))
Tactic: simp only [pushoutCocone_pt, coe_of]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
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'
⊢ h = ofHom (Algebra.TensorProduct.productMap f' g').toRingHom
have 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))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
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)
⊢ 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))
have 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))
Tactic: change h' x = Algebra.TensorProduct.productMap f' g' x
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
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)
⊢ 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))
have 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))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
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' := ⋯ }
⊢ h = ofHom (Algebra.TensorProduct.productMap f' g').toRingHom
have property : h' = Algebra.TensorProduct.productMap f' g'
Tactic: suffices h' = Algebra.TensorProduct.productMap f' g' by
      ext x
      change h' x = Algebra.TensorProduct.productMap f' g' x
      rw [this]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
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' := ⋯ }
⊢ h' = Algebra.TensorProduct.productMap f' g'
have 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))
Tactic: apply Algebra.TensorProduct.ext'
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
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))
    ((Algebra.TensorProduct.productMap f' g' : (a : A ⊗[R] B) → (↑s.pt : Type u)) (a ⊗ₜ[R] b) : (↑s.pt : Type u))
have 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))
Tactic: simp only [f', g', ← eq1, pushoutCocone_pt, ← eq2, AlgHom.toRingHom_eq_coe,
      Algebra.TensorProduct.productMap_apply_tmul, AlgHom.coe_mk]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
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
⊢ (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))
have 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))
Tactic: change _ = h (a ⊗ₜ 1) * h (1 ⊗ₜ b)
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
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
⊢ (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))
have 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))
Tactic: rw [← h.hom.map_mul, Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
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
⊢ 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)))
have 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))
Tactic: ext