awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x y : ColimitType F
⊢ descFun F s (x + y) = descFun F s x + descFun F s y

Tactic:
Quot.induction_on₂ x y fun a b => ?_

Premises used: Quot.induction_on₂
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x y : ColimitType F
refine :
  ∀ (a b : Prequotient F),
    descFun F s
        (HAdd.hAdd (α := ColimitType F) (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) a)
          (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) b)) =
      descFun F s (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) a) +
        descFun F s (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) b)
⊢ descFun F s (x + y) = descFun F s x + descFun F s y

Tactic:
refine Quot.induction_on₂ x y fun a b => ?_
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x y : ColimitType F
a b : Prequotient F
dsimp :
  Quot.lift (r := (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (descFunLift F s) ⋯
      (HAdd.hAdd (α := ColimitType F) (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) a)
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) b)) =
    descFunLift F s a + descFunLift F s b
⊢ descFun F s
      (HAdd.hAdd (α := ColimitType F) (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) a)
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) b)) =
    descFun F s (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) a) +
      descFun F s (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) b)

Tactic:
dsimp [descFun]

Premises used: CommRingCat.Colimits.descFun
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x y : ColimitType F
a b : Prequotient F
⊢ Quot.lift (r := (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop)) (descFunLift F s) ⋯
      (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) (a.add b)) =
    descFunLift F s a + descFunLift F s b

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x : (↑(colimitCocone F).pt : Type v)
⊢ Eq (α := (↑s.pt : Type v))
    ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v)) x : (↑s.pt : Type v))
    ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v)) x : (↑s.pt : Type v))

Tactic:
Quot.inductionOn x ?_

Premises used: Quot.inductionOn
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x : (↑(colimitCocone F).pt : Type v)
refine :
  ∀ (a : Prequotient F),
    Eq (α := (↑s.pt : Type v))
      ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
          (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) a) :
        (↑s.pt : Type v))
      ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
          (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) a) :
        (↑s.pt : Type v))
⊢ Eq (α := (↑s.pt : Type v))
    ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v)) x : (↑s.pt : Type v))
    ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v)) x : (↑s.pt : Type v))

Tactic:
refine Quot.inductionOn x ?_
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x : (↑(colimitCocone F).pt : Type v)
⊢ Eq (α := (↑s.pt : Type v))
    ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) zero) :
      (↑s.pt : Type v))
    ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) zero) :
      (↑s.pt : Type v))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x : (↑(colimitCocone F).pt : Type v)
⊢ Eq (α := (↑s.pt : Type v))
    ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) one) :
      (↑s.pt : Type v))
    ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) one) :
      (↑s.pt : Type v))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x_1 : (↑(colimitCocone F).pt : Type v)
x : Prequotient F
ih :
  Eq (α := (↑s.pt : Type v))
    ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x) :
      (↑s.pt : Type v))
    ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x) :
      (↑s.pt : Type v))
⊢ Eq (α := (↑s.pt : Type v))
    ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x.neg) :
      (↑s.pt : Type v))
    ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x.neg) :
      (↑s.pt : Type v))

Tactic:
simp [ih]
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x_1 : (↑(colimitCocone F).pt : Type v)
j : J
x : (↑(F.obj j) : Type v)
⊢ Eq (α := (↑s.pt : Type v))
    ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) (Prequotient.of j x)) :
      (↑s.pt : Type v))
    ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) (Prequotient.of j x)) :
      (↑s.pt : Type v))

Tactic:
congr_fun (congr_arg (fun f : F.obj j ⟶ s.pt => (f : F.obj j → s.pt)) (w j)) x

Premises used: CategoryTheory.ConcreteCategory.hom, CommRingCat.Colimits.coconeFun, congr_arg, congr_fun, CommRingCat.Colimits.descFunLift, DFunLike.coe, CommRingCat.Colimits.descFun
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x_1 : (↑(colimitCocone F).pt : Type v)
j : J
x : (↑(F.obj j) : Type v)
⊢ Eq (α := (↑s.pt : Type v))
    ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) (Prequotient.of j x)) :
      (↑s.pt : Type v))
    ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) (Prequotient.of j x)) :
      (↑s.pt : Type v))

Tactic:
exact congr_fun (congr_arg (fun f : F.obj j ⟶ s.pt => (f : F.obj j → s.pt)) (w j)) x

Premises used: CategoryTheory.ConcreteCategory.hom, congr_arg, congr_fun, DFunLike.coe
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x_1 : (↑(colimitCocone F).pt : Type v)
x y : Prequotient F
ih_x :
  Eq (α := (↑s.pt : Type v))
    ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x) :
      (↑s.pt : Type v))
    ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x) :
      (↑s.pt : Type v))
ih_y :
  Eq (α := (↑s.pt : Type v))
    ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) y) :
      (↑s.pt : Type v))
    ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) y) :
      (↑s.pt : Type v))
⊢ Eq (α := (↑s.pt : Type v))
    ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) (x.add y)) :
      (↑s.pt : Type v))
    ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) (x.add y)) :
      (↑s.pt : Type v))

Tactic:
simp [ih_x, ih_y]
-- Module: Mathlib.Algebra.Category.Ring.Colimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x_1 : (↑(colimitCocone F).pt : Type v)
x y : Prequotient F
ih_x :
  Eq (α := (↑s.pt : Type v))
    ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x) :
      (↑s.pt : Type v))
    ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x) :
      (↑s.pt : Type v))
ih_y :
  Eq (α := (↑s.pt : Type v))
    ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) y) :
      (↑s.pt : Type v))
    ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) y) :
      (↑s.pt : Type v))
⊢ Eq (α := (↑s.pt : Type v))
    ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) (x.mul y)) :
      (↑s.pt : Type v))
    ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) (x.mul y)) :
      (↑s.pt : Type v))

Tactic:
simp [ih_x, ih_y]
-- 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
W : CommRingCat
inl : of A ⟶ of (A ⊗[R] B)
inr : of B ⟶ of (A ⊗[R] B)
eq :
  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)))
⊢ PushoutCocone (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B))

Tactic:
fapply Limits.PushoutCocone.mk

Premises used: CategoryTheory.Limits.PushoutCocone.mk
-- 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
⊢ CommRingCat

Tactic:
exact CommRingCat.of (A ⊗[R] B)

Premises used: CommRingCat.of, TensorProduct
-- 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
⊢ of A ⟶ of (A ⊗[R] B)

Tactic:
exact ofHom <| Algebra.TensorProduct.includeLeftRingHom (A := A)

Premises used: Algebra.TensorProduct.includeLeftRingHom, CommRingCat.ofHom
-- 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
⊢ of B ⟶ of (A ⊗[R] B)

Tactic:
exact ofHom <| Algebra.TensorProduct.includeRight.toRingHom (A := B)

Premises used: CommRingCat.ofHom, AlgHom.toRingHom, Algebra.TensorProduct.includeRight
-- 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
eq :
  ∀ (r : (↑(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))
          r :
        (↑(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))
          r :
        (↑(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 r
-- 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
r : (↑(of R) : Type u)
trans :
  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))
        r :
      (↑(of (A ⊗[R] B)) : Type u))
    ((algebraMap R (A ⊗[R] B) : (a : R) → A ⊗[R] B) r : A ⊗[R] B)
trans₁ :
  Eq (α := A ⊗[R] B) ((algebraMap R (A ⊗[R] B) : (a : R) → A ⊗[R] B) r : A ⊗[R] B)
    ((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))
        r :
      (↑(of (A ⊗[R] B)) : 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))
        r :
      (↑(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))
        r :
      (↑(of (A ⊗[R] B)) : Type u))

Tactic:
trans algebraMap R (A ⊗[R] B) r

Premises used: Algebra.algebraMap, TensorProduct, 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
r : (↑(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))
        r :
      (↑(of (A ⊗[R] B)) : Type u))
    ((algebraMap R (A ⊗[R] B) : (a : R) → A ⊗[R] B) r : A ⊗[R] B)

Tactic:
Algebra.TensorProduct.includeLeft.commutes (R := R) r

Premises used: Algebra.TensorProduct.includeLeft, Quotient, AlgHom.commutes, TensorProduct, TensorProduct.tmul, AddCon.Quotient, AddCon.toQuotient
-- 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
r : (↑(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))
        r :
      (↑(of (A ⊗[R] B)) : Type u))
    ((algebraMap R (A ⊗[R] B) : (a : R) → A ⊗[R] B) r : A ⊗[R] B)

Tactic:
exact Algebra.TensorProduct.includeLeft.commutes (R := R) r

Premises used: Algebra.TensorProduct.includeLeft, AlgHom.commutes
-- 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
r : (↑(of R) : Type u)
⊢ Eq (α := A ⊗[R] B) ((algebraMap R (A ⊗[R] B) : (a : R) → A ⊗[R] B) r : A ⊗[R] B)
    ((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))
        r :
      (↑(of (A ⊗[R] B)) : Type u))

Tactic:
(Algebra.TensorProduct.includeRight.commutes (R := R) r).symm

Premises used: AlgHom.commutes, TensorProduct.tmul, Eq.symm, AddCon.toQuotient, Algebra.TensorProduct.includeRight
-- 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
r : (↑(of R) : Type u)
⊢ Eq (α := A ⊗[R] B) ((algebraMap R (A ⊗[R] B) : (a : R) → A ⊗[R] B) r : A ⊗[R] B)
    ((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))
        r :
      (↑(of (A ⊗[R] B)) : Type u))

Tactic:
exact (Algebra.TensorProduct.includeRight.commutes (R := R) r).symm

Premises used: AlgHom.commutes, Eq.symm, Algebra.TensorProduct.includeRight
-- 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
⊢ Eq (α :=
    of A ⟶
      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))
    (PushoutCocone.inl (pushoutCocone R A B)) (ofHom Algebra.TensorProduct.includeLeftRingHom)

Tactic:
rfl

Premises used: 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
⊢ Eq (α :=
    of B ⟶
      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))
    (PushoutCocone.inr (pushoutCocone R A B)) (ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight))

Tactic:
rfl

Premises used: 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
⊢ 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) =
    of (A ⊗[R] B)

Tactic:
rfl

Premises used: 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 : 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' := ⋯ }
⊢ Algebra R (A ⊗[R] B)

Tactic:
infer_instance
-- 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 :
  PushoutCocone.inl (pushoutCocone R A B) ≫ ofHom (Algebra.TensorProduct.productMap f' g').toRingHom = s.inl ∧
    PushoutCocone.inr (pushoutCocone R A B) ≫ 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},
        PushoutCocone.inl (pushoutCocone R A B) ≫ m = s.inl →
          PushoutCocone.inr (pushoutCocone R A B) ≫ m = s.inr →
            m = ofHom (Algebra.TensorProduct.productMap f' g').toRingHom
⊢ { l :
    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 //
    PushoutCocone.inl (pushoutCocone R A B) ≫ l = s.inl ∧
      PushoutCocone.inr (pushoutCocone R A B) ≫ l = 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},
          PushoutCocone.inl (pushoutCocone R A B) ≫ m = s.inl →
            PushoutCocone.inr (pushoutCocone R A B) ≫ m = s.inr → m = l }

Tactic:
use ofHom (AlgHom.toRingHom (Algebra.TensorProduct.productMap f' g'))

Premises used: CommRingCat.ofHom, AlgHom.toRingHom, Algebra.TensorProduct.productMap