awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
ht :
  Function.Injective (α := (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₂)
⊢ t ≫ r = l ≫ b ∧
    (∀ (x₁ y₁ : (fun (X : Type u) ↦ X) X₁),
        Eq (α := (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₂)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) t :
                    (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂)
                  y₁ :
                (fun (X : Type u) ↦ X) X₂) ∧
            Eq (α := (fun (X : Type u) ↦ X) X₃)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) l :
                    (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) l :
                    (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃)
                  y₁ :
                (fun (X : Type u) ↦ X) X₃) →
          x₁ = y₁) ∧
      ∀ (x₂ : (fun (X : Type u) ↦ X) X₂) (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) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄)
                x₃ :
              (fun (X : Type u) ↦ X) 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₁ =
                x₂ ∧
              (ConcreteCategory.hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃)
                  x₁ =
                x₃

Tactic:
⟨h.w, fun x₁ y₁ ⟨h₂, _⟩ ↦ ht h₂, fun x₂ x₃ hx ↦ ?_⟩

Premises used: _private.0.CategoryTheory.Limits.Types.isPullback_of_isPushout.match_1, And.intro, CategoryTheory.IsPushout.toCommSq, CategoryTheory.CommSq.w, Eq
-- 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
ht :
  Function.Injective (α := (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₂)
refine :
  ∀ (x₂ : (fun (X : Type u) ↦ X) X₂) (x₃ : (fun (X : Type u) ↦ X) X₃)
    (hx :
      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) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) x₃ :
          (fun (X : Type u) ↦ X) 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₁ =
          x₂ ∧
        (ConcreteCategory.hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) x₁ =
          x₃
⊢ t ≫ r = l ≫ b ∧
    (∀ (x₁ y₁ : (fun (X : Type u) ↦ X) X₁),
        Eq (α := (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₂)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) t :
                    (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂)
                  y₁ :
                (fun (X : Type u) ↦ X) X₂) ∧
            Eq (α := (fun (X : Type u) ↦ X) X₃)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) l :
                    (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) l :
                    (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃)
                  y₁ :
                (fun (X : Type u) ↦ X) X₃) →
          x₁ = y₁) ∧
      ∀ (x₂ : (fun (X : Type u) ↦ X) X₂) (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) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄)
                x₃ :
              (fun (X : Type u) ↦ X) 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₁ =
                x₂ ∧
              (ConcreteCategory.hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃)
                  x₁ =
                x₃

Tactic:
refine ⟨h.w, fun x₁ y₁ ⟨h₂, _⟩ ↦ ht h₂, fun x₂ x₃ hx ↦ ?_⟩
-- 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
ht :
  Function.Injective (α := (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₂
x₃ : (fun (X : Type u) ↦ X) X₃
hx :
  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) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) x₃ :
      (fun (X : Type u) ↦ X) X₄)
⊢ ∃ (s : X₁),
    (ConcreteCategory.hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) s = x₂ ∧
      (ConcreteCategory.hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) s = x₃

Tactic:
have := (pushoutCocone_inl_eq_inr_iff_of_isColimit h.isColimit ht x₂ x₃).1 hx
-- 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
ht :
  Function.Injective (α := (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₂
x₃ : (fun (X : Type u) ↦ X) X₃
hx :
  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) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) x₃ :
      (fun (X : Type u) ↦ X) X₄)
this :
  ∃ (s : X₁),
    (ConcreteCategory.hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) s = x₂ ∧
      (ConcreteCategory.hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) s = 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₁ = x₂ ∧
      (ConcreteCategory.hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) x₁ = x₃

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
hr' : Mono r'
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉
        Set.range (ι := (fun (X : Type u) ↦ X) X₁)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
            (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
      y₃ ∉
          Set.range (ι := (fun (X : Type u) ↦ X) X₁)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
              (a : (fun (X : Type u) ↦ X) 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) b' : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₅)
                y₃ :
              (fun (X : Type u) ↦ X) X₅) →
          x₃ = y₃
⊢ Mono (r ≫ k)

Tactic:
subst facr facb
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
hr' : Mono r'
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉
        Set.range (ι := (fun (X : Type u) ↦ X) X₁)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
            (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
      y₃ ∉
          Set.range (ι := (fun (X : Type u) ↦ X) X₁)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
              (a : (fun (X : Type u) ↦ X) 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) b' : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₅)
                y₃ :
              (fun (X : Type u) ↦ X) X₅) →
          x₃ = y₃
hr'₁ : Mono (r ≫ k)
⊢ ∀ (x₃ y₃ : X₃),
    x₃ ∉
        Set.range (ι := (fun (X : Type u) ↦ X) X₁)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
            (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
      y₃ ∉
          Set.range (ι := (fun (X : Type u) ↦ X) X₁)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
              (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
        Eq (α := (fun (X : Type u) ↦ X) X₅)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (b ≫ k) :
                  (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) (b ≫ k) :
                  (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₅)
                y₃ :
              (fun (X : Type u) ↦ X) X₅) →
          x₃ = y₃

Tactic:
subst facr facb
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
hr' : Mono r'
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉
        Set.range (ι := (fun (X : Type u) ↦ X) X₁)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
            (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
      y₃ ∉
          Set.range (ι := (fun (X : Type u) ↦ X) X₁)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
              (a : (fun (X : Type u) ↦ X) 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) b' : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₅)
                y₃ :
              (fun (X : Type u) ↦ X) X₅) →
          x₃ = y₃
hr'₁ : Mono (r ≫ k)
H₁ :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉
        Set.range (ι := (fun (X : Type u) ↦ X) X₁)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
            (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
      y₃ ∉
          Set.range (ι := (fun (X : Type u) ↦ X) X₁)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
              (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
        Eq (α := (fun (X : Type u) ↦ X) X₅)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (b ≫ k) :
                  (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) (b ≫ k) :
                  (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₅)
                y₃ :
              (fun (X : Type u) ↦ X) X₅) →
          x₃ = y₃
⊢ IsPullback t l (r ≫ k) (b ≫ k)

Tactic:
subst facr facb
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Mono (r ≫ k)
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉
        Set.range (ι := (fun (X : Type u) ↦ X) X₁)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
            (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
      y₃ ∉
          Set.range (ι := (fun (X : Type u) ↦ X) X₁)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
              (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
        Eq (α := (fun (X : Type u) ↦ X) X₅)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (b ≫ k) :
                  (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) (b ≫ k) :
                  (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₅)
                y₃ :
              (fun (X : Type u) ↦ X) X₅) →
          x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
x₁ y₁ : (fun (X : Type u) ↦ X) X₁
h :
  Eq (α := (fun (X : Type u) ↦ X) X₃)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) l : (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) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) y₁ :
      (fun (X : Type u) ↦ X) X₃)
⊢ Eq (α := X₅) ((ConcreteCategory.hom (FC := TypeCat.Fun) (l ≫ b ≫ k) : (a : X₁) → X₅) x₁ : X₅)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (l ≫ b ≫ k) : (a : X₁) → X₅) y₁ : X₅)

Tactic:
simp [h]
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Mono (r ≫ k)
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉
        Set.range (ι := (fun (X : Type u) ↦ X) X₁)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
            (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
      y₃ ∉
          Set.range (ι := (fun (X : Type u) ↦ X) X₁)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
              (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
        Eq (α := (fun (X : Type u) ↦ X) X₅)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (b ≫ k) :
                  (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) (b ≫ k) :
                  (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₅)
                y₃ :
              (fun (X : Type u) ↦ X) X₅) →
          x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
⊢ Function.Injective (α := (fun (X : Type u) ↦ X) X₁) (β := (fun (X : Type u) ↦ X) X₃)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃)

Tactic:
have : Function.Injective l :=
    fun x₁ y₁ h ↦ ext_of_isPullback h₂ ((mono_iff_injective _).1 hr'
      ((ConcreteCategory.congr_hom h₂.w x₁).trans (Eq.trans (by simp [h])
      (ConcreteCategory.congr_hom h₂.w.symm y₁)))) h
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Mono (r ≫ k)
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉
        Set.range (ι := (fun (X : Type u) ↦ X) X₁)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
            (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
      y₃ ∉
          Set.range (ι := (fun (X : Type u) ↦ X) X₁)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
              (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
        Eq (α := (fun (X : Type u) ↦ X) X₅)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (b ≫ k) :
                  (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) (b ≫ k) :
                  (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₅)
                y₃ :
              (fun (X : Type u) ↦ X) X₅) →
          x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this :
  Function.Injective (α := (fun (X : Type u) ↦ X) X₁) (β := (fun (X : Type u) ↦ X) X₃)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃)
rw :
  ∀
    (hr' :
      Function.Injective (α := (fun (X : Type u) ↦ X) X₂) (β := (fun (X : Type u) ↦ X) X₅)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (r ≫ k)) :
          (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₅))
    (H :
      ∀ (x₃ y₃ : X₃),
        x₃ ∉
            Set.range (ι := (fun (X : Type u) ↦ X) X₁)
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
                (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
          y₃ ∉
              Set.range (ι := (fun (X : Type u) ↦ X) X₁)
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
                  (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
            Eq (α := (fun (X : Type u) ↦ X) X₅)
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (b ≫ k) :
                      (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) (b ≫ k) :
                      (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₅)
                    y₃ :
                  (fun (X : Type u) ↦ X) X₅) →
              x₃ = y₃)
    (h₂ : IsPullback t l (r ≫ k) (b ≫ k))
    (this :
      Function.Injective (α := (fun (X : Type u) ↦ X) X₁) (β := (fun (X : Type u) ↦ X) X₃)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃)),
    Function.Injective (α := (fun (X : Type u) ↦ X) X₄) (β := (fun (X : Type u) ↦ X) X₅)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) k) : (a : (fun (X : Type u) ↦ X) X₄) → (fun (X : Type u) ↦ X) X₅)
⊢ Mono k

Tactic:
rw [mono_iff_injective] at hr' ⊢

Premises used: CategoryTheory.mono_iff_injective
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' :
  Function.Injective (α := (fun (X : Type u) ↦ X) X₂) (β := (fun (X : Type u) ↦ X) X₅)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (r ≫ k)) : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₅)
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉
        Set.range (ι := (fun (X : Type u) ↦ X) X₁)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
            (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
      y₃ ∉
          Set.range (ι := (fun (X : Type u) ↦ X) X₁)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
              (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
        Eq (α := (fun (X : Type u) ↦ X) X₅)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (b ≫ k) :
                  (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) (b ≫ k) :
                  (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₅)
                y₃ :
              (fun (X : Type u) ↦ X) X₅) →
          x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this :
  Function.Injective (α := (fun (X : Type u) ↦ X) X₁) (β := (fun (X : Type u) ↦ X) X₃)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃)
⊢ ∀ (x : ToType (FC := TypeCat.Fun) X₁),
    Eq (α := X₄) ((ConcreteCategory.hom (FC := TypeCat.Fun) (t ≫ r) : (a : X₁) → X₄) x : X₄)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (l ≫ b) : (a : X₁) → X₄) x : X₄)

Tactic:
have w := ConcreteCategory.congr_hom h₁.w
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' :
  Function.Injective (α := (fun (X : Type u) ↦ X) X₂) (β := (fun (X : Type u) ↦ X) X₅)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (r ≫ k)) : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₅)
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉
        Set.range (ι := (fun (X : Type u) ↦ X) X₁)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
            (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
      y₃ ∉
          Set.range (ι := (fun (X : Type u) ↦ X) X₁)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
              (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
        Eq (α := (fun (X : Type u) ↦ X) X₅)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (b ≫ k) :
                  (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) (b ≫ k) :
                  (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₅)
                y₃ :
              (fun (X : Type u) ↦ X) X₅) →
          x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this :
  Function.Injective (α := (fun (X : Type u) ↦ X) X₁) (β := (fun (X : Type u) ↦ X) X₃)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃)
w :
  ∀ (x : ToType (FC := TypeCat.Fun) X₁),
    Eq (α := X₄) ((ConcreteCategory.hom (FC := TypeCat.Fun) (t ≫ r) : (a : X₁) → X₄) x : X₄)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (l ≫ b) : (a : X₁) → X₄) x : X₄)
⊢ ∀ (x : ToType (FC := TypeCat.Fun) X₁),
    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) b : (a : X₃) → X₄)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) l : (a : X₁) → X₃) x : X₃) :
        X₄)

Tactic:
simp only [comp_apply] at w

Premises used: CategoryTheory.comp_apply