awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c c' : PushoutCocone f g
e : c ≅ c'
x₁ : X₁
x₂ : X₂
h :
  Eq (α := (fun (X : Type u) ↦ X) c.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inl : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c.pt)
        x₁ :
      (fun (X : Type u) ↦ X) c.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inr : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c.pt)
        x₂ :
      (fun (X : Type u) ↦ X) c.pt)
h₁ :
  Eq (α := (fun (X : Type u) ↦ X) c'.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) c'.inl : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c'.pt)
        x₁ :
      (fun (X : Type u) ↦ X) c'.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) e.hom.hom :
          (a : (fun (X : Type u) ↦ X) c.pt) → (fun (X : Type u) ↦ X) c'.pt)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inl :
              (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c.pt)
            x₁ :
          (fun (X : Type u) ↦ X) c.pt) :
      (fun (X : Type u) ↦ X) c'.pt)
h₂ :
  Eq (α := (fun (X : Type u) ↦ X) c'.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) c'.inr : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c'.pt)
        x₂ :
      (fun (X : Type u) ↦ X) c'.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) e.hom.hom :
          (a : (fun (X : Type u) ↦ X) c.pt) → (fun (X : Type u) ↦ X) c'.pt)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inr :
              (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c.pt)
            x₂ :
          (fun (X : Type u) ↦ X) c.pt) :
      (fun (X : Type u) ↦ X) c'.pt)
⊢ Eq (α := (fun (X : Type u) ↦ X) c'.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) c'.inl : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c'.pt)
        x₁ :
      (fun (X : Type u) ↦ X) c'.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) c'.inr : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c'.pt)
        x₂ :
      (fun (X : Type u) ↦ X) c'.pt)

Tactic:
convert! congr_arg e.hom.hom h

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.CoconeMorphism.hom, congr_arg, CategoryTheory.Iso.hom, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c c' : PushoutCocone f g
e : c ≅ c'
x₁ : X₁
x₂ : X₂
h :
  Eq (α := (fun (X : Type u) ↦ X) c.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inl : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c.pt)
        x₁ :
      (fun (X : Type u) ↦ X) c.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inr : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c.pt)
        x₂ :
      (fun (X : Type u) ↦ X) c.pt)
⊢ Eq (α := (fun (X : Type u) ↦ X) c'.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) c'.inl : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c'.pt)
        x₁ :
      (fun (X : Type u) ↦ X) c'.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) e.hom.hom :
          (a : (fun (X : Type u) ↦ X) c.pt) → (fun (X : Type u) ↦ X) c'.pt)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inl :
              (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c.pt)
            x₁ :
          (fun (X : Type u) ↦ X) c.pt) :
      (fun (X : Type u) ↦ X) c'.pt)

Tactic:
ConcreteCategory.congr_hom (e.hom.w WalkingSpan.left).symm x₁

Premises used: CategoryTheory.Limits.CoconeMorphism.w, CategoryTheory.Limits.WalkingSpan.left, CategoryTheory.ConcreteCategory.congr_hom, Eq.symm, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c c' : PushoutCocone f g
e : c ≅ c'
x₁ : X₁
x₂ : X₂
h :
  Eq (α := (fun (X : Type u) ↦ X) c.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inl : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c.pt)
        x₁ :
      (fun (X : Type u) ↦ X) c.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inr : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c.pt)
        x₂ :
      (fun (X : Type u) ↦ X) c.pt)
⊢ Eq (α := (fun (X : Type u) ↦ X) c'.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) c'.inl : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c'.pt)
        x₁ :
      (fun (X : Type u) ↦ X) c'.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) e.hom.hom :
          (a : (fun (X : Type u) ↦ X) c.pt) → (fun (X : Type u) ↦ X) c'.pt)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inl :
              (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c.pt)
            x₁ :
          (fun (X : Type u) ↦ X) c.pt) :
      (fun (X : Type u) ↦ X) c'.pt)

Tactic:
exact ConcreteCategory.congr_hom (e.hom.w WalkingSpan.left).symm x₁

Premises used: CategoryTheory.Limits.CoconeMorphism.w, CategoryTheory.Limits.WalkingSpan.left, CategoryTheory.ConcreteCategory.congr_hom, Eq.symm, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c c' : PushoutCocone f g
e : c ≅ c'
x₁ : X₁
x₂ : X₂
h :
  Eq (α := (fun (X : Type u) ↦ X) c.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inl : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c.pt)
        x₁ :
      (fun (X : Type u) ↦ X) c.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inr : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c.pt)
        x₂ :
      (fun (X : Type u) ↦ X) c.pt)
⊢ Eq (α := (fun (X : Type u) ↦ X) c'.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) c'.inr : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c'.pt)
        x₂ :
      (fun (X : Type u) ↦ X) c'.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) e.hom.hom :
          (a : (fun (X : Type u) ↦ X) c.pt) → (fun (X : Type u) ↦ X) c'.pt)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inr :
              (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c.pt)
            x₂ :
          (fun (X : Type u) ↦ X) c.pt) :
      (fun (X : Type u) ↦ X) c'.pt)

Tactic:
ConcreteCategory.congr_hom (e.hom.w WalkingSpan.right).symm x₂

Premises used: CategoryTheory.Limits.CoconeMorphism.w, CategoryTheory.Limits.WalkingSpan.right, CategoryTheory.ConcreteCategory.congr_hom, Eq.symm, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c c' : PushoutCocone f g
e : c ≅ c'
x₁ : X₁
x₂ : X₂
h :
  Eq (α := (fun (X : Type u) ↦ X) c.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inl : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c.pt)
        x₁ :
      (fun (X : Type u) ↦ X) c.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inr : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c.pt)
        x₂ :
      (fun (X : Type u) ↦ X) c.pt)
⊢ Eq (α := (fun (X : Type u) ↦ X) c'.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) c'.inr : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c'.pt)
        x₂ :
      (fun (X : Type u) ↦ X) c'.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) e.hom.hom :
          (a : (fun (X : Type u) ↦ X) c.pt) → (fun (X : Type u) ↦ X) c'.pt)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inr :
              (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c.pt)
            x₂ :
          (fun (X : Type u) ↦ X) c.pt) :
      (fun (X : Type u) ↦ X) c'.pt)

Tactic:
exact ConcreteCategory.congr_hom (e.hom.w WalkingSpan.right).symm x₂

Premises used: CategoryTheory.Limits.CoconeMorphism.w, CategoryTheory.Limits.WalkingSpan.right, CategoryTheory.ConcreteCategory.congr_hom, Eq.symm, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c c' : PushoutCocone f g
e : c ≅ c'
x₁ : X₁
x₂ : X₂
mp :
  Eq (α := (fun (X : Type u) ↦ X) c.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inl : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c.pt)
          x₁ :
        (fun (X : Type u) ↦ X) c.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inr : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c.pt)
          x₂ :
        (fun (X : Type u) ↦ X) c.pt) →
    Eq (α := (fun (X : Type u) ↦ X) c'.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c'.inl :
            (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c'.pt)
          x₁ :
        (fun (X : Type u) ↦ X) c'.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c'.inr :
            (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c'.pt)
          x₂ :
        (fun (X : Type u) ↦ X) c'.pt)
mpr :
  Eq (α := (fun (X : Type u) ↦ X) c'.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c'.inl :
            (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c'.pt)
          x₁ :
        (fun (X : Type u) ↦ X) c'.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c'.inr :
            (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c'.pt)
          x₂ :
        (fun (X : Type u) ↦ X) c'.pt) →
    Eq (α := (fun (X : Type u) ↦ X) c.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inl : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c.pt)
          x₁ :
        (fun (X : Type u) ↦ X) c.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inr : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c.pt)
          x₂ :
        (fun (X : Type u) ↦ X) c.pt)
⊢ Eq (α := (fun (X : Type u) ↦ X) c.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inl : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c.pt)
          x₁ :
        (fun (X : Type u) ↦ X) c.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inr : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c.pt)
          x₂ :
        (fun (X : Type u) ↦ X) c.pt) ↔
    Eq (α := (fun (X : Type u) ↦ X) c'.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c'.inl :
            (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c'.pt)
          x₁ :
        (fun (X : Type u) ↦ X) c'.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c'.inr :
            (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c'.pt)
          x₂ :
        (fun (X : Type u) ↦ X) c'.pt)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c c' : PushoutCocone f g
e : c ≅ c'
x₁ : X₁
x₂ : X₂
⊢ Eq (α := (fun (X : Type u) ↦ X) c.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inl : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c.pt)
          x₁ :
        (fun (X : Type u) ↦ X) c.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inr : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c.pt)
          x₂ :
        (fun (X : Type u) ↦ X) c.pt) →
    Eq (α := (fun (X : Type u) ↦ X) c'.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c'.inl :
            (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c'.pt)
          x₁ :
        (fun (X : Type u) ↦ X) c'.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c'.inr :
            (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c'.pt)
          x₂ :
        (fun (X : Type u) ↦ X) c'.pt)

Tactic:
apply pushoutCocone_inl_eq_inr_imp_of_iso e

Premises used: CategoryTheory.Limits.Types.pushoutCocone_inl_eq_inr_imp_of_iso
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c c' : PushoutCocone f g
e : c ≅ c'
x₁ : X₁
x₂ : X₂
⊢ Eq (α := (fun (X : Type u) ↦ X) c'.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c'.inl :
            (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c'.pt)
          x₁ :
        (fun (X : Type u) ↦ X) c'.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c'.inr :
            (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c'.pt)
          x₂ :
        (fun (X : Type u) ↦ X) c'.pt) →
    Eq (α := (fun (X : Type u) ↦ X) c.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inl : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c.pt)
          x₁ :
        (fun (X : Type u) ↦ X) c.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inr : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c.pt)
          x₂ :
        (fun (X : Type u) ↦ X) c.pt)

Tactic:
apply pushoutCocone_inl_eq_inr_imp_of_iso e.symm

Premises used: CategoryTheory.Limits.Types.pushoutCocone_inl_eq_inr_imp_of_iso, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c : PushoutCocone f g
hc : IsColimit c
h₁ :
  Function.Injective (α := (fun (X : Type u) ↦ X) S) (β := (fun (X : Type u) ↦ X) X₁)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁)
x₁ : X₁
x₂ : X₂
⊢ ∀ (j : WalkingSpan),
    c.ι.app j ≫ (hc.coconePointUniqueUpToIso (Pushout.isColimitCocone f g)).hom = (Pushout.cocone f g).ι.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c : PushoutCocone f g
hc : IsColimit c
h₁ :
  Function.Injective (α := (fun (X : Type u) ↦ X) S) (β := (fun (X : Type u) ↦ X) X₁)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁)
x₁ : X₁
x₂ : X₂
rw :
  Eq (α := (fun (X : Type u) ↦ X) (Pushout.cocone f g).pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Pushout.cocone f g).inl :
            (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) (Pushout.cocone f g).pt)
          x₁ :
        (fun (X : Type u) ↦ X) (Pushout.cocone f g).pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Pushout.cocone f g).inr :
            (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) (Pushout.cocone f g).pt)
          x₂ :
        (fun (X : Type u) ↦ X) (Pushout.cocone f g).pt) ↔
    ∃ (s : S),
      (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) s = x₁ ∧
        (ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) s = x₂
⊢ Eq (α := (fun (X : Type u) ↦ X) c.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inl : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c.pt)
          x₁ :
        (fun (X : Type u) ↦ X) c.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inr : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c.pt)
          x₂ :
        (fun (X : Type u) ↦ X) c.pt) ↔
    ∃ (s : S),
      (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) s = x₁ ∧
        (ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) s = x₂

Tactic:
rw [pushoutCocone_inl_eq_inr_iff_of_iso
    (Cocone.ext (IsColimit.coconePointUniqueUpToIso hc (Pushout.isColimitCocone f g))
    (by simp))]

Premises used: CategoryTheory.Limits.Cocone.ext, CategoryTheory.Limits.Types.Pushout.isColimitCocone, CategoryTheory.Limits.Types.pushoutCocone_inl_eq_inr_iff_of_iso, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c : PushoutCocone f g
hc : IsColimit c
h₁ :
  Function.Injective (α := (fun (X : Type u) ↦ X) S) (β := (fun (X : Type u) ↦ X) X₁)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁)
x₁ : X₁
x₂ : X₂
⊢ Mono f

Tactic:
have := (mono_iff_injective f).2 h₁
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c : PushoutCocone f g
hc : IsColimit c
h₁ :
  Function.Injective (α := (fun (X : Type u) ↦ X) S) (β := (fun (X : Type u) ↦ X) X₁)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁)
x₁ : X₁
x₂ : X₂
this : Mono f
⊢ Eq (α := (fun (X : Type u) ↦ X) (Pushout.cocone f g).pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Pushout.cocone f g).inl :
            (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) (Pushout.cocone f g).pt)
          x₁ :
        (fun (X : Type u) ↦ X) (Pushout.cocone f g).pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Pushout.cocone f g).inr :
            (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) (Pushout.cocone f g).pt)
          x₂ :
        (fun (X : Type u) ↦ X) (Pushout.cocone f g).pt) ↔
    ∃ (s : S),
      (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) s = x₁ ∧
        (ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) s = x₂

Tactic:
apply Pushout.inl_eq_inr_iff

Premises used: CategoryTheory.Limits.Types.Pushout.inl_eq_inr_iff
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c : PushoutCocone f g
hc : IsColimit c
inst : Mono f
⊢ ∀ (j : WalkingSpan),
    c.ι.app j ≫ (hc.coconePointUniqueUpToIso (Pushout.isColimitCocone f g)).hom = (Pushout.cocone f g).ι.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c : PushoutCocone f g
hc : IsColimit c
inst : Mono f
change :
  Mono
    (Pushout.inr f g ≫
      ((Cocone.forget (span f g)).mapIso
          (Cocone.ext (hc.coconePointUniqueUpToIso (Pushout.isColimitCocone f g)) ⋯)).inv)
⊢ Mono c.inr

Tactic:
change Mono ((Pushout.inr f g) ≫
    ((Cocone.forget _).mapIso
      (Cocone.ext (IsColimit.coconePointUniqueUpToIso hc
        (Pushout.isColimitCocone f g)) (by simp))).inv)

Premises used: CategoryTheory.Mono, CategoryTheory.Limits.Cocone.ext, CategoryTheory.Limits.Types.Pushout.isColimitCocone, CategoryTheory.Limits.Cocone.forget, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.Types.Pushout.inr, CategoryTheory.Functor.mapIso, CategoryTheory.Iso.inv, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c : PushoutCocone f g
hc : IsColimit c
inst : Mono f
⊢ Mono
    (Pushout.inr f g ≫
      ((Cocone.forget (span f g)).mapIso
          (Cocone.ext (hc.coconePointUniqueUpToIso (Pushout.isColimitCocone f g)) ⋯)).inv)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c : PushoutCocone f g
hc : IsColimit c
h₁ :
  Function.Injective (α := (fun (X : Type u) ↦ X) S) (β := (fun (X : Type u) ↦ X) X₁)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁)
rw : ∀ (h₁ : Mono f), Mono c.inr
⊢ Function.Injective (α := (fun (X : Type u) ↦ X) X₂) (β := (fun (X : Type u) ↦ X) c.pt)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inr) : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c.pt)

Tactic:
rw [← mono_iff_injective] at h₁ ⊢

Premises used: CategoryTheory.mono_iff_injective
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c : PushoutCocone f g
hc : IsColimit c
h₁ : Mono f
⊢ Mono c.inr

Tactic:
pushoutCocone_inr_mono_of_isColimit hc

Premises used: CategoryTheory.Limits.Types.pushoutCocone_inr_mono_of_isColimit
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c : PushoutCocone f g
hc : IsColimit c
h₁ : Mono f
⊢ Mono c.inr

Tactic:
exact pushoutCocone_inr_mono_of_isColimit hc

Premises used: CategoryTheory.Limits.Types.pushoutCocone_inr_mono_of_isColimit
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst : Mono g
⊢ Mono (Pushout.inl f g)

Tactic:
pushoutCocone_inr_mono_of_isColimit
    (PushoutCocone.flipIsColimit (Pushout.isColimitCocone f g))

Premises used: CategoryTheory.Limits.Types.Pushout.isColimitCocone, CategoryTheory.Limits.Types.Pushout.inl, CategoryTheory.Limits.Types.pushoutCocone_inr_mono_of_isColimit, CategoryTheory.Limits.PushoutCocone.flipIsColimit, CategoryTheory.Limits.Types.Pushout
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst : Mono f
⊢ Mono (Y := pushout f g) (pushout.inr f g)

Tactic:
(pushoutCocone_inr_mono_of_isColimit (pushoutIsPushout f g) :)

Premises used: CategoryTheory.Limits.colimit, CategoryTheory.Limits.Types.pushoutCocone_inr_mono_of_isColimit, CategoryTheory.Limits.pushoutIsPushout, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst : Mono g
⊢ Mono (Y := pushout f g) (pushout.inl f g)

Tactic:
pushoutCocone_inr_mono_of_isColimit
    (PushoutCocone.flipIsColimit (pushoutIsPushout f g))

Premises used: CategoryTheory.Limits.WidePushoutShape.wideSpan, CategoryTheory.Limits.colimit, CategoryTheory.Limits.Types.pushoutCocone_inr_mono_of_isColimit, CategoryTheory.Limits.pushoutIsPushout, CategoryTheory.Limits.PushoutCocone.flipIsColimit, CategoryTheory.Limits.span, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPushout t l r b
x₄ : X₄
obtain :
  ∀ (j : WalkingSpan) (x : (span t l).obj j),
    (∃ (x₂ : (fun (X : Type u) ↦ X) X₂),
        Eq (α := (fun (X : Type u) ↦ X) X₄)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄)
              x₂ :
            (fun (X : Type u) ↦ X) X₄)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (h.cocone.ι.app j) :
                (a : (fun (X : Type u) ↦ X) ((span t l).obj j)) →
                  (fun (X : Type u) ↦ X) (((Functor.const WalkingSpan).obj h.cocone.pt).obj j))
              x :
            (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const WalkingSpan) h.cocone.pt) j))) ∨
      ∃ (x₃ : (fun (X : Type u) ↦ X) X₃),
        Eq (α := (fun (X : Type u) ↦ X) X₄)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄)
              x₃ :
            (fun (X : Type u) ↦ X) X₄)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (h.cocone.ι.app j) :
                (a : (fun (X : Type u) ↦ X) ((span t l).obj j)) →
                  (fun (X : Type u) ↦ X) (((Functor.const WalkingSpan).obj h.cocone.pt).obj j))
              x :
            (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const WalkingSpan) h.cocone.pt) j))
⊢ (∃ (x₂ : (fun (X : Type u) ↦ X) X₂),
      (ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) x₂ =
        x₄) ∨
    ∃ (x₃ : (fun (X : Type u) ↦ X) X₃),
      (ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) x₃ = x₄

Tactic:
obtain ⟨j, x, rfl⟩ := jointly_surjective_of_isColimit h.isColimit x₄

Premises used: CategoryTheory.Limits.Types.jointly_surjective_of_isColimit, CategoryTheory.IsPushout.isColimit, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPushout t l r b
x : (span t l).obj none
simp :
  Eq (α := X₄)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : X₂) → X₄)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) t : (a : X₁) → X₂) x : X₂) :
      X₄)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (t ≫ r) : (a : X₁) → h.cocone.pt) x : h.cocone.pt)
⊢ Eq (α := (fun (X : Type u) ↦ X) X₄)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) x :
          (fun (X : Type u) ↦ X) X₂) :
      (fun (X : Type u) ↦ X) X₄)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (h.cocone.ι.app none) :
          (a : (fun (X : Type u) ↦ X) ((span t l).obj none)) →
            (fun (X : Type u) ↦ X) (((Functor.const WalkingSpan).obj h.cocone.pt).obj none))
        x :
      (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const WalkingSpan) h.cocone.pt) none))

Tactic:
simp