awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
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
zero :
  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.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) Prequotient.zero) :
      (↑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) :
      (↑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))
have one : 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: induction x with
    | zero => simp
    | one => simp
    | neg x ih => simp [ih]
    | of j x =>
      exact congr_fun (congr_arg (fun f : F.obj j ⟶ s.pt => (f : F.obj j → s.pt)) (w j)) x
    | add x y ih_x ih_y => simp [ih_x, ih_y]
    | mul x y ih_x ih_y => simp [ih_x, ih_y]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
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
zero :
  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.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) Prequotient.zero) :
      (↑s.pt : Type v))
one :
  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.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) Prequotient.one) :
      (↑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) :
      (↑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))
have neg : ∀ (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: induction x with
    | zero => simp
    | one => simp
    | neg x ih => simp [ih]
    | of j x =>
      exact congr_fun (congr_arg (fun f : F.obj j ⟶ s.pt => (f : F.obj j → s.pt)) (w j)) x
    | add x y ih_x ih_y => simp [ih_x, ih_y]
    | mul x y ih_x ih_y => simp [ih_x, ih_y]
Cleared hypotheses: 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
⊢ PushoutCocone (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
have W : CommRingCat
Tactic: fapply Limits.PushoutCocone.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
W : CommRingCat
⊢ PushoutCocone (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
have inl : of A ⟶ of (A ⊗[R] B)
Tactic: fapply Limits.PushoutCocone.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
W : CommRingCat
inl : of A ⟶ of (A ⊗[R] B)
⊢ PushoutCocone (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
have inr : of B ⟶ of (A ⊗[R] B)
Tactic: fapply Limits.PushoutCocone.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
W : CommRingCat
inl : of A ⟶ of (A ⊗[R] B)
inr : of B ⟶ of (A ⊗[R] B)
⊢ PushoutCocone (X := of R) (Y := of A) (Z := of B) (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
have 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)))
Tactic: fapply Limits.PushoutCocone.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
⊢ 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 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))
Tactic: ext 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
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))
have 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)
Tactic: trans algebraMap R (A ⊗[R] B) 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
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)
⊢ 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))
have 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))
Tactic: trans algebraMap R (A ⊗[R] B) 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
⊢ { 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 }
have 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
Tactic: use ofHom (AlgHom.toRingHom (Algebra.TensorProduct.productMap f' g'))
-- 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
⊢ 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
have property : ofHom Algebra.TensorProduct.includeLeftRingHom ≫ ofHom (Algebra.TensorProduct.productMap f' g').toRingHom = s.inl
Tactic: constructor
-- 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
property :
  ofHom Algebra.TensorProduct.includeLeftRingHom ≫ ofHom (Algebra.TensorProduct.productMap f' g').toRingHom = s.inl
⊢ 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
have 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
Tactic: constructor
-- 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
⊢ ofHom Algebra.TensorProduct.includeLeftRingHom ≫ ofHom (Algebra.TensorProduct.productMap f' g').toRingHom = s.inl
have 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))
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 : 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
⊢ 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
have property : ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight) ≫ ofHom (Algebra.TensorProduct.productMap f' g').toRingHom =
  s.inr
Tactic: constructor
-- 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
property :
  ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight) ≫
      ofHom (Algebra.TensorProduct.productMap f' g').toRingHom =
    s.inr
⊢ 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
have 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
Tactic: constructor
-- 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
⊢ ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight) ≫
      ofHom (Algebra.TensorProduct.productMap f' g').toRingHom =
    s.inr
have 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))
Tactic: ext x