awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) 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₄)
x₂ y₂ : X₂
eq :
  Eq (α := (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₅)
        ((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₄) :
      (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₅)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) y₂ :
          (fun (X : Type u) ↦ X) X₄) :
      (fun (X : Type u) ↦ X) X₅)
⊢ x₂ = y₂

Tactic:
hr' eq
-- 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) 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₄)
x₂ : X₂
eq :
  Eq (α := (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₅)
        ((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₄) :
      (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₅)
        ((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₄) :
      (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) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) x₂ :
      (fun (X : Type u) ↦ X) X₄)

Tactic:
rfl
-- 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) 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₄)
x₃ : X₃
hx₃ hy₃ :
  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₃)
eq :
  Eq (α := (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₅)
        ((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₄) :
      (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₅)
        ((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₄) :
      (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₄) x₃ :
      (fun (X : Type u) ↦ X) X₄)

Tactic:
rfl
-- 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₅
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₁ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
inst : Mono r'
inst_1 : Mono k
h₂ :
  Eq (α := Set ((fun (X : Type u) ↦ X) X₄))
    (Set.range (ι := (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₄) ⊔
      Set.range (ι := (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₄))
    Set.univ
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₃
⊢ t ≫ r = l ≫ b

Tactic:
simp only [← cancel_mono k, Category.assoc, facr, facb, h₁.w]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.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₅
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₁ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
inst : Mono r'
inst_1 : Mono k
h₂ :
  Eq (α := Set ((fun (X : Type u) ↦ X) X₄))
    (Set.range (ι := (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₄) ⊔
      Set.range (ι := (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₄))
    Set.univ
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₃
obtain : ∀ (φ : pushout t l ⟶ X₄) (hφ₁ : pushout.inl t l ≫ φ = r) (hφ₂ : pushout.inr t l ≫ φ = b), IsPushout t l r b
⊢ IsPushout t l r b

Tactic:
obtain ⟨φ, hφ₁, hφ₂⟩ := pushout.exists_desc t l r b
    (by simp only [← cancel_mono k, Category.assoc, facr, facb, h₁.w])

Premises used: CategoryTheory.Limits.pushout.exists_desc
-- 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₅
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₁ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
inst : Mono r'
inst_1 : Mono k
h₂ :
  Eq (α := Set ((fun (X : Type u) ↦ X) X₄))
    (Set.range (ι := (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₄) ⊔
      Set.range (ι := (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₄))
    Set.univ
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₃
φ : pushout t l ⟶ X₄
hφ₁ : pushout.inl t l ≫ φ = r
hφ₂ : pushout.inr t l ≫ φ = b
⊢ Mono (φ ≫ k)

Tactic:
have := mono_of_isPushout_of_isPullback (IsPushout.of_hasPushout t l) h₁
    (k := φ ≫ k) (by cat_disch) (by cat_disch) 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₅
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₁ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
inst : Mono r'
inst_1 : Mono k
h₂ :
  Eq (α := Set ((fun (X : Type u) ↦ X) X₄))
    (Set.range (ι := (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₄) ⊔
      Set.range (ι := (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₄))
    Set.univ
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₃
φ : pushout t l ⟶ X₄
hφ₁ : pushout.inl t l ≫ φ = r
hφ₂ : pushout.inr t l ≫ φ = b
this : Mono (φ ≫ k)
rw :
  Function.Bijective (α := (fun (X : Type u) ↦ X) (pushout t l)) (β := (fun (X : Type u) ↦ X) X₄)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) φ) :
      (a : (fun (X : Type u) ↦ X) (pushout t l)) → (fun (X : Type u) ↦ X) X₄)
⊢ IsIso φ

Tactic:
rw [isIso_iff_bijective]

Premises used: CategoryTheory.isIso_iff_bijective
-- 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₅
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₁ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
inst : Mono r'
inst_1 : Mono k
h₂ :
  Eq (α := Set ((fun (X : Type u) ↦ X) X₄))
    (Set.range (ι := (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₄) ⊔
      Set.range (ι := (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₄))
    Set.univ
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₃
φ : pushout t l ⟶ X₄
hφ₁ : pushout.inl t l ≫ φ = r
hφ₂ : pushout.inr t l ≫ φ = b
this : Mono (φ ≫ k)
⊢ Function.Bijective (α := (fun (X : Type u) ↦ X) (pushout t l)) (β := (fun (X : Type u) ↦ X) X₄)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) φ) :
      (a : (fun (X : Type u) ↦ X) (pushout t l)) → (fun (X : Type u) ↦ X) X₄)

Tactic:
⟨(mono_iff_injective _).1 (mono_of_mono φ k), fun x₄ ↦ ?_⟩

Premises used: CategoryTheory.mono_iff_injective, CategoryTheory.mono_of_mono, And.intro, Iff.mp, Function.Bijective
-- 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₅
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₁ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
inst : Mono r'
inst_1 : Mono k
h₂ :
  Eq (α := Set ((fun (X : Type u) ↦ X) X₄))
    (Set.range (ι := (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₄) ⊔
      Set.range (ι := (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₄))
    Set.univ
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₃
φ : pushout t l ⟶ X₄
hφ₁ : pushout.inl t l ≫ φ = r
hφ₂ : pushout.inr t l ≫ φ = b
this : Mono (φ ≫ k)
refine :
  ∀ (x₄ : (fun (X : Type u) ↦ X) X₄),
    ∃ (a : (fun (X : Type u) ↦ X) (pushout t l)),
      (ConcreteCategory.hom (FC := TypeCat.Fun) φ :
            (a : (fun (X : Type u) ↦ X) (pushout t l)) → (fun (X : Type u) ↦ X) X₄)
          a =
        x₄
⊢ Function.Bijective (α := (fun (X : Type u) ↦ X) (pushout t l)) (β := (fun (X : Type u) ↦ X) X₄)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) φ) :
      (a : (fun (X : Type u) ↦ X) (pushout t l)) → (fun (X : Type u) ↦ X) X₄)

Tactic:
refine ⟨(mono_iff_injective _).1 (mono_of_mono φ k), fun x₄ ↦ ?_⟩
-- 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₅
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₁ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
inst : Mono r'
inst_1 : Mono k
h₂ :
  Eq (α := Set ((fun (X : Type u) ↦ X) X₄))
    (Set.range (ι := (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₄) ⊔
      Set.range (ι := (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₄))
    Set.univ
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₃
φ : pushout t l ⟶ X₄
hφ₁ : pushout.inl t l ≫ φ = r
hφ₂ : pushout.inr t l ≫ φ = b
this : Mono (φ ≫ k)
x₄ : (fun (X : Type u) ↦ X) X₄
⊢ Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X₄)) Set.univ x₄

Tactic:
have hx₄ := Set.mem_univ x₄
-- 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₅
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₁ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
inst : Mono r'
inst_1 : Mono k
h₂ :
  Eq (α := Set ((fun (X : Type u) ↦ X) X₄))
    (Set.range (ι := (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₄) ⊔
      Set.range (ι := (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₄))
    Set.univ
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₃
φ : pushout t l ⟶ X₄
hφ₁ : pushout.inl t l ≫ φ = r
hφ₂ : pushout.inr t l ≫ φ = b
this : Mono (φ ≫ k)
x₄ : (fun (X : Type u) ↦ X) X₄
hx₄ : Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X₄)) Set.univ x₄
⊢ (∃ (y : X₂), (ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : X₂) → X₄) y = x₄) ∨
    ∃ (y : X₃), (ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : X₃) → X₄) y = x₄

Tactic:
simp only [← h₂, Set.sup_eq_union, Set.mem_union, Set.mem_range] at hx₄

Premises used: Set.mem_union, Set.mem_range, Set.sup_eq_union