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₅
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₄ :
  (∃ (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₄
inl :
  ∀ (x₂ : X₂),
    ∃ (a : (fun (X : Type u) ↦ X) (pushout t l)),
      Eq (α := (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₄)
            a :
          (fun (X : Type u) ↦ X) X₄)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : X₂) → X₄) x₂ : X₄)
inr :
  ∀ (x₃ : X₃),
    ∃ (a : (fun (X : Type u) ↦ X) (pushout t l)),
      Eq (α := (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₄)
            a :
          (fun (X : Type u) ↦ X) X₄)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : X₃) → X₄) 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₄

Tactic:
obtain (⟨x₂, rfl⟩ | ⟨x₃, rfl⟩) := hx₄

Premises used: 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₃
φ : pushout t l ⟶ X₄
hφ₁ : pushout.inl t l ≫ φ = r
hφ₂ : pushout.inr t l ≫ φ = b
this : Mono (φ ≫ k)
x₂ : X₂
⊢ ∃ (a : (fun (X : Type u) ↦ X) (pushout t l)),
    Eq (α := (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₄)
          a :
        (fun (X : Type u) ↦ X) X₄)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : X₂) → X₄) x₂ : X₄)

Tactic:
⟨_, ConcreteCategory.congr_hom hφ₁ x₂⟩

Premises used: Exists.intro
-- 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₂ : X₂
⊢ ∃ (a : (fun (X : Type u) ↦ X) (pushout t l)),
    Eq (α := (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₄)
          a :
        (fun (X : Type u) ↦ X) X₄)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : X₂) → X₄) x₂ : X₄)

Tactic:
exact ⟨_, ConcreteCategory.congr_hom hφ₁ 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₃ : X₃
⊢ ∃ (a : (fun (X : Type u) ↦ X) (pushout t l)),
    Eq (α := (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₄)
          a :
        (fun (X : Type u) ↦ X) X₄)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : X₃) → X₄) x₃ : X₄)

Tactic:
⟨_, ConcreteCategory.congr_hom hφ₂ x₃⟩

Premises used: Exists.intro
-- 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₃ : X₃
⊢ ∃ (a : (fun (X : Type u) ↦ X) (pushout t l)),
    Eq (α := (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₄)
          a :
        (fun (X : Type u) ↦ X) X₄)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : X₃) → X₄) x₃ : X₄)

Tactic:
exact ⟨_, ConcreteCategory.congr_hom hφ₂ 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)
⊢ IsIso φ

Tactic:
have : IsIso φ := by
    rw [isIso_iff_bijective]
    refine ⟨(mono_iff_injective _).1 (mono_of_mono φ k), fun x₄ ↦ ?_⟩
    have hx₄ := Set.mem_univ x₄
    simp only [← h₂, Set.sup_eq_union, Set.mem_union, Set.mem_range] at hx₄
    obtain (⟨x₂, rfl⟩ | ⟨x₃, rfl⟩) := hx₄
    · exact ⟨_, ConcreteCategory.congr_hom hφ₁ x₂⟩
    · exact ⟨_, ConcreteCategory.congr_hom hφ₂ 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_1 : Mono (φ ≫ k)
this : IsIso φ
⊢ t ≫ Iso.hom (Iso.refl X₂) = Iso.hom (Iso.refl X₁) ≫ t

Tactic:
simp
-- 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_1 : Mono (φ ≫ k)
this : IsIso φ
⊢ l ≫ Iso.hom (Iso.refl X₃) = Iso.hom (Iso.refl X₁) ≫ l

Tactic:
simp
-- 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_1 : Mono (φ ≫ k)
this : IsIso φ
⊢ pushout.inl t l ≫ (asIso φ).hom = Iso.hom (Iso.refl X₂) ≫ r

Tactic:
simpa
-- 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_1 : Mono (φ ≫ k)
this : IsIso φ
⊢ pushout.inr t l ≫ (asIso φ).hom = Iso.hom (Iso.refl X₃) ≫ b

Tactic:
simpa
-- 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_1 : Mono (φ ≫ k)
this : IsIso φ
⊢ IsPushout t l r b

Tactic:
exact IsPushout.of_iso (IsPushout.of_hasPushout t l)
    (Iso.refl _) (Iso.refl _) (Iso.refl _) (asIso φ) (by simp) (by simp)
    (by simpa) (by simpa)

Premises used: CategoryTheory.IsPushout.of_hasPushout, CategoryTheory.Iso.refl, CategoryTheory.IsPushout.of_iso, CategoryTheory.asIso
-- 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₁ : IsPullback t l r b
inst : Mono r
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₃
⊢ r ≫ 𝟙 X₄ = r

Tactic:
simp