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
x : (span t l).obj none
⊢ 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)

Tactic:
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
⊢ (∃ (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 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))) ∨
    ∃ (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 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:
exact Or.inl ⟨t x, by simp; rfl⟩

Premises used: Or.inl
-- 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 (some WalkingPair.left)
⊢ (∃ (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 (some WalkingPair.left)) :
              (a : (fun (X : Type u) ↦ X) ((span t l).obj (some WalkingPair.left))) →
                (fun (X : Type u) ↦ X) (((Functor.const WalkingSpan).obj h.cocone.pt).obj (some WalkingPair.left)))
            x :
          (fun (X : Type u) ↦ X)
            (Functor.obj (Functor.obj (Functor.const WalkingSpan) h.cocone.pt) (some WalkingPair.left)))) ∨
    ∃ (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 (some WalkingPair.left)) :
              (a : (fun (X : Type u) ↦ X) ((span t l).obj (some WalkingPair.left))) →
                (fun (X : Type u) ↦ X) (((Functor.const WalkingSpan).obj h.cocone.pt).obj (some WalkingPair.left)))
            x :
          (fun (X : Type u) ↦ X)
            (Functor.obj (Functor.obj (Functor.const WalkingSpan) h.cocone.pt) (some WalkingPair.left)))

Tactic:
Or.inl ⟨x, rfl⟩

Premises used: Exists.intro, Or.inl, 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 (some WalkingPair.left)
⊢ (∃ (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 (some WalkingPair.left)) :
              (a : (fun (X : Type u) ↦ X) ((span t l).obj (some WalkingPair.left))) →
                (fun (X : Type u) ↦ X) (((Functor.const WalkingSpan).obj h.cocone.pt).obj (some WalkingPair.left)))
            x :
          (fun (X : Type u) ↦ X)
            (Functor.obj (Functor.obj (Functor.const WalkingSpan) h.cocone.pt) (some WalkingPair.left)))) ∨
    ∃ (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 (some WalkingPair.left)) :
              (a : (fun (X : Type u) ↦ X) ((span t l).obj (some WalkingPair.left))) →
                (fun (X : Type u) ↦ X) (((Functor.const WalkingSpan).obj h.cocone.pt).obj (some WalkingPair.left)))
            x :
          (fun (X : Type u) ↦ X)
            (Functor.obj (Functor.obj (Functor.const WalkingSpan) h.cocone.pt) (some WalkingPair.left)))

Tactic:
exact Or.inl ⟨x, rfl⟩

Premises used: Or.inl
-- 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 (some WalkingPair.right)
⊢ (∃ (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 (some WalkingPair.right)) :
              (a : (fun (X : Type u) ↦ X) ((span t l).obj (some WalkingPair.right))) →
                (fun (X : Type u) ↦ X) (((Functor.const WalkingSpan).obj h.cocone.pt).obj (some WalkingPair.right)))
            x :
          (fun (X : Type u) ↦ X)
            (Functor.obj (Functor.obj (Functor.const WalkingSpan) h.cocone.pt) (some WalkingPair.right)))) ∨
    ∃ (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 (some WalkingPair.right)) :
              (a : (fun (X : Type u) ↦ X) ((span t l).obj (some WalkingPair.right))) →
                (fun (X : Type u) ↦ X) (((Functor.const WalkingSpan).obj h.cocone.pt).obj (some WalkingPair.right)))
            x :
          (fun (X : Type u) ↦ X)
            (Functor.obj (Functor.obj (Functor.const WalkingSpan) h.cocone.pt) (some WalkingPair.right)))

Tactic:
Or.inr ⟨x, rfl⟩

Premises used: Exists.intro, Or.inr, 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 (some WalkingPair.right)
⊢ (∃ (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 (some WalkingPair.right)) :
              (a : (fun (X : Type u) ↦ X) ((span t l).obj (some WalkingPair.right))) →
                (fun (X : Type u) ↦ X) (((Functor.const WalkingSpan).obj h.cocone.pt).obj (some WalkingPair.right)))
            x :
          (fun (X : Type u) ↦ X)
            (Functor.obj (Functor.obj (Functor.const WalkingSpan) h.cocone.pt) (some WalkingPair.right)))) ∨
    ∃ (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 (some WalkingPair.right)) :
              (a : (fun (X : Type u) ↦ X) ((span t l).obj (some WalkingPair.right))) →
                (fun (X : Type u) ↦ X) (((Functor.const WalkingSpan).obj h.cocone.pt).obj (some WalkingPair.right)))
            x :
          (fun (X : Type u) ↦ X)
            (Functor.obj (Functor.obj (Functor.const WalkingSpan) h.cocone.pt) (some WalkingPair.right)))

Tactic:
exact Or.inr ⟨x, rfl⟩

Premises used: Or.inr
-- 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₄
inl :
  ∀
    (h₁ :
      ∃ (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) 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₄ ∧
          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₃)
inr :
  ∀ (x₃ : X₃)
    (hx₃ :
      (ConcreteCategory.hom (FC := TypeCat.Fun) b : (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) 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₄ ∧
          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₃)
⊢ (∃ (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₄ ∧
        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₃)

Tactic:
obtain h₁ | ⟨x₃, hx₃⟩ := eq_or_eq_of_isPushout h x₄

Premises used: CategoryTheory.Limits.Types.eq_or_eq_of_isPushout
-- 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₄
h₁ :
  ∃ (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) 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₄ ∧
        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₃)

Tactic:
Or.inl h₁

Premises used: Or.inl
-- 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₄
h₁ :
  ∃ (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) 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₄ ∧
        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₃)

Tactic:
exact Or.inl h₁

Premises used: Or.inl
-- 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₄
x₃ : X₃
hx₃ : (ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) x₃ = x₄
pos :
  ∀
    (h₂ :
      Membership.mem (γ := Set ((fun (X : Type u) ↦ 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₃))
        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₂ =
          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₄ ∧
          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₃)
neg :
  ∀
    (h₂ :
      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₃)),
    (∃ (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₄ ∧
          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₃)
⊢ (∃ (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₄ ∧
        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₃)

Tactic:
by_cases h₂ : x₃ ∈ Set.range l

Premises used: CategoryTheory.ConcreteCategory.hom, Set.range, DFunLike.coe
-- 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₄
x₃ : X₃
hx₃ : (ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) x₃ = x₄
h₂ :
  Membership.mem (γ := Set ((fun (X : Type u) ↦ 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₃))
    x₃
pos :
  ∀ (x₁ : X₁)
    (hx₃ :
      (ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (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₁ :
            (fun (X : Type u) ↦ X) 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₂ =
          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₄ ∧
          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₃)
⊢ (∃ (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₄ ∧
        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₃)

Tactic:
obtain ⟨x₁, rfl⟩ := h₂

Premises used: 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₄ : X₄
x₁ : X₁
hx₃ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (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₁ :
        (fun (X : Type u) ↦ X) 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₂) =
    x₄

Tactic:
simpa only [← hx₃] using ConcreteCategory.congr_hom h.w x₁

Premises used: CategoryTheory.IsPushout.toCommSq, CategoryTheory.CommSq.w, CategoryTheory.ConcreteCategory.congr_hom
-- 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₄
x₁ : X₁
hx₃ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (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₁ :
        (fun (X : Type u) ↦ X) 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₂ =
        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₄ ∧
        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₃)

Tactic:
exact Or.inl ⟨t x₁, by simpa only [← hx₃] using ConcreteCategory.congr_hom h.w x₁⟩

Premises used: Or.inl
-- 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₄
x₃ : X₃
hx₃ : (ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) x₃ = x₄
h₂ :
  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₃)
⊢ (∃ (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₄ ∧
        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₃)

Tactic:
Or.inr ⟨x₃, hx₃, h₂⟩

Premises used: And.intro, Exists.intro, Or.inr
-- 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₄
x₃ : X₃
hx₃ : (ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) x₃ = x₄
h₂ :
  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₃)
⊢ (∃ (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₄ ∧
        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₃)

Tactic:
exact Or.inr ⟨x₃, hx₃, h₂⟩

Premises used: Or.inr
-- 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₂)
rw :
  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₃
⊢ IsPullback t l r b

Tactic:
rw [isPullback_iff]

Premises used: CategoryTheory.Limits.Types.isPullback_iff