awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Goal:
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
w : t ≫ r = l ≫ b
h₁ :
  ∀ (x₁ y₁ : (fun (X : Type u) ↦ X) X₁),
    Eq (α := (fun (X : Type u) ↦ X) X₂)
          ((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₂)
          ((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₃)
          ((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₃)
          ((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₁
h₂ :
  ∀ (x₂ : (fun (X : Type u) ↦ X) X₂) (x₃ : (fun (X : Type u) ↦ X) X₃),
    Eq (α := (fun (X : Type u) ↦ X) X₄)
        ((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₄)
        ((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₁),
        (hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) x₁ = x₂ ∧
          (hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) x₁ = x₃
φ : X₁ ⟶ PullbackObj r b :=
  ↾fun (x₁ : X₁) ↦
    Subtype.mk (p := fun (p : X₂ × X₃) ↦
      Eq (α := (fun (X : Type u) ↦ X) X₄)
        ((hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) p.1 :
          (fun (X : Type u) ↦ X) X₄)
        ((hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) p.2 :
          (fun (X : Type u) ↦ X) X₄))
      ((hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) x₁,
        (hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) x₁)
      ⋯
a₁ : X₁
left :
  ∀ ⦃a₂ : X₁⦄,
    Eq (α := (fun (X : Type u) ↦ X) (PullbackObj r b))
        ((hom (FC := TypeCat.Fun) φ : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) (PullbackObj r b)) a₁ :
          (fun (X : Type u) ↦ X) (PullbackObj r b))
        ((hom (FC := TypeCat.Fun) φ : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) (PullbackObj r b)) a₂ :
          (fun (X : Type u) ↦ X) (PullbackObj r b)) →
      a₁ = a₂
⊢ ∀ ⦃a₂ : (fun (X : Type u) ↦ X) X₁⦄,
    Eq (α := (fun (X : Type u) ↦ X) (PullbackObj r b))
        ((hom (FC := TypeCat.Fun) φ : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) (PullbackObj r b)) a₁ :
          (fun (X : Type u) ↦ X) (PullbackObj r b))
        ((hom (FC := TypeCat.Fun) φ : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) (PullbackObj r b)) a₂ :
          (fun (X : Type u) ↦ X) (PullbackObj r b)) →
      a₁ = a₂

Tactic:
_
-- Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Goal:
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
w : t ≫ r = l ≫ b
h₁ :
  ∀ (x₁ y₁ : (fun (X : Type u) ↦ X) X₁),
    Eq (α := (fun (X : Type u) ↦ X) X₂)
          ((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₂)
          ((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₃)
          ((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₃)
          ((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₁
h₂ :
  ∀ (x₂ : (fun (X : Type u) ↦ X) X₂) (x₃ : (fun (X : Type u) ↦ X) X₃),
    Eq (α := (fun (X : Type u) ↦ X) X₄)
        ((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₄)
        ((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₁),
        (hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) x₁ = x₂ ∧
          (hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) x₁ = x₃
φ : X₁ ⟶ PullbackObj r b :=
  ↾fun (x₁ : X₁) ↦
    Subtype.mk (p := fun (p : X₂ × X₃) ↦
      Eq (α := (fun (X : Type u) ↦ X) X₄)
        ((hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) p.1 :
          (fun (X : Type u) ↦ X) X₄)
        ((hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) p.2 :
          (fun (X : Type u) ↦ X) X₄))
      ((hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) x₁,
        (hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) x₁)
      ⋯
a₁ a₂ : X₁
h :
  Eq (α := (fun (X : Type u) ↦ X) (PullbackObj r b))
    ((hom (FC := TypeCat.Fun) φ : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) (PullbackObj r b)) a₁ :
      (fun (X : Type u) ↦ X) (PullbackObj r b))
    ((hom (FC := TypeCat.Fun) φ : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) (PullbackObj r b)) a₂ :
      (fun (X : Type u) ↦ X) (PullbackObj r b))
⊢ Eq (α := X₂) ((hom (FC := TypeCat.Fun) t : (a : X₁) → X₂) a₁ : X₂)
      ((hom (FC := TypeCat.Fun) t : (a : X₁) → X₂) a₂ : X₂) ∧
    Eq (α := X₃) ((hom (FC := TypeCat.Fun) l : (a : X₁) → X₃) a₁ : X₃)
      ((hom (FC := TypeCat.Fun) l : (a : X₁) → X₃) a₂ : X₃)

Tactic:
simp [φ] at h
-- Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Goal:
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
w : t ≫ r = l ≫ b
h₁ :
  ∀ (x₁ y₁ : (fun (X : Type u) ↦ X) X₁),
    Eq (α := (fun (X : Type u) ↦ X) X₂)
          ((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₂)
          ((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₃)
          ((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₃)
          ((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₁
h₂ :
  ∀ (x₂ : (fun (X : Type u) ↦ X) X₂) (x₃ : (fun (X : Type u) ↦ X) X₃),
    Eq (α := (fun (X : Type u) ↦ X) X₄)
        ((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₄)
        ((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₁),
        (hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) x₁ = x₂ ∧
          (hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) x₁ = x₃
φ : X₁ ⟶ PullbackObj r b :=
  ↾fun (x₁ : X₁) ↦
    Subtype.mk (p := fun (p : X₂ × X₃) ↦
      Eq (α := (fun (X : Type u) ↦ X) X₄)
        ((hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) p.1 :
          (fun (X : Type u) ↦ X) X₄)
        ((hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) p.2 :
          (fun (X : Type u) ↦ X) X₄))
      ((hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) x₁,
        (hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) x₁)
      ⋯
a₁ a₂ : X₁
h :
  Eq (α := X₂) ((hom (FC := TypeCat.Fun) t : (a : X₁) → X₂) a₁ : X₂)
      ((hom (FC := TypeCat.Fun) t : (a : X₁) → X₂) a₂ : X₂) ∧
    Eq (α := X₃) ((hom (FC := TypeCat.Fun) l : (a : X₁) → X₃) a₁ : X₃)
      ((hom (FC := TypeCat.Fun) l : (a : X₁) → X₃) a₂ : X₃)
⊢ a₁ = a₂

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Goal:
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
w : t ≫ r = l ≫ b
h₁ :
  ∀ (x₁ y₁ : (fun (X : Type u) ↦ X) X₁),
    Eq (α := (fun (X : Type u) ↦ X) X₂)
          ((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₂)
          ((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₃)
          ((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₃)
          ((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₁
h₂ :
  ∀ (x₂ : (fun (X : Type u) ↦ X) X₂) (x₃ : (fun (X : Type u) ↦ X) X₃),
    Eq (α := (fun (X : Type u) ↦ X) X₄)
        ((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₄)
        ((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₁),
        (hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) x₁ = x₂ ∧
          (hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) x₁ = x₃
φ : X₁ ⟶ PullbackObj r b :=
  ↾fun (x₁ : X₁) ↦
    Subtype.mk (p := fun (p : X₂ × X₃) ↦
      Eq (α := (fun (X : Type u) ↦ X) X₄)
        ((hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) p.1 :
          (fun (X : Type u) ↦ X) X₄)
        ((hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) p.2 :
          (fun (X : Type u) ↦ X) X₄))
      ((hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) x₁,
        (hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) x₁)
      ⋯
x : PullbackObj r b
⊢ Eq (α := (fun (X : Type u) ↦ X) X₄)
    ((hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) (↑x : X₂ × X₃).1 :
      (fun (X : Type u) ↦ X) X₄)
    ((hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) (↑x : X₂ × X₃).2 :
      (fun (X : Type u) ↦ X) X₄)

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Goal:
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
w : t ≫ r = l ≫ b
h₁ :
  ∀ (x₁ y₁ : (fun (X : Type u) ↦ X) X₁),
    Eq (α := (fun (X : Type u) ↦ X) X₂)
          ((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₂)
          ((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₃)
          ((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₃)
          ((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₁
h₂ :
  ∀ (x₂ : (fun (X : Type u) ↦ X) X₂) (x₃ : (fun (X : Type u) ↦ X) X₃),
    Eq (α := (fun (X : Type u) ↦ X) X₄)
        ((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₄)
        ((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₁),
        (hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) x₁ = x₂ ∧
          (hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) x₁ = x₃
φ : X₁ ⟶ PullbackObj r b :=
  ↾fun (x₁ : X₁) ↦
    Subtype.mk (p := fun (p : X₂ × X₃) ↦
      Eq (α := (fun (X : Type u) ↦ X) X₄)
        ((hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) p.1 :
          (fun (X : Type u) ↦ X) X₄)
        ((hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) p.2 :
          (fun (X : Type u) ↦ X) X₄))
      ((hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) x₁,
        (hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) x₁)
      ⋯
x : PullbackObj r b
right :
  ∀ (a : X₁)
    (ha :
      (hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) a = (↑x : X₂ × X₃).1 ∧
        (hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) a = (↑x : X₂ × X₃).2),
    ∃ (a : (fun (X : Type u) ↦ X) X₁),
      (hom (FC := TypeCat.Fun) φ : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) (PullbackObj r b)) a = x
⊢ ∃ (a : (fun (X : Type u) ↦ X) X₁),
    (hom (FC := TypeCat.Fun) φ : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) (PullbackObj r b)) a = x

Tactic:
obtain ⟨a, ha⟩ := h₂ x.1.1 x.1.2 (by grind)

Premises used: Prod.fst, Subtype.val, Prod.snd
-- Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Goal:
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
w : t ≫ r = l ≫ b
h₁ :
  ∀ (x₁ y₁ : (fun (X : Type u) ↦ X) X₁),
    Eq (α := (fun (X : Type u) ↦ X) X₂)
          ((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₂)
          ((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₃)
          ((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₃)
          ((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₁
h₂ :
  ∀ (x₂ : (fun (X : Type u) ↦ X) X₂) (x₃ : (fun (X : Type u) ↦ X) X₃),
    Eq (α := (fun (X : Type u) ↦ X) X₄)
        ((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₄)
        ((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₁),
        (hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) x₁ = x₂ ∧
          (hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) x₁ = x₃
φ : X₁ ⟶ PullbackObj r b :=
  ↾fun (x₁ : X₁) ↦
    Subtype.mk (p := fun (p : X₂ × X₃) ↦
      Eq (α := (fun (X : Type u) ↦ X) X₄)
        ((hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) p.1 :
          (fun (X : Type u) ↦ X) X₄)
        ((hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) p.2 :
          (fun (X : Type u) ↦ X) X₄))
      ((hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) x₁,
        (hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) x₁)
      ⋯
⊢ IsIso φ

Tactic:
have hφ : IsIso φ := by
      rw [isIso_iff_bijective]
      constructor
      · intro _ _ h
        simp [φ] at h
        grind
      · intro x
        obtain ⟨a, ha⟩ := h₂ x.1.1 x.1.2 (by grind)
        cat_disch
-- Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Goal:
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
w : t ≫ r = l ≫ b
h₁ :
  ∀ (x₁ y₁ : (fun (X : Type u) ↦ X) X₁),
    Eq (α := (fun (X : Type u) ↦ X) X₂)
          ((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₂)
          ((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₃)
          ((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₃)
          ((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₁
h₂ :
  ∀ (x₂ : (fun (X : Type u) ↦ X) X₂) (x₃ : (fun (X : Type u) ↦ X) X₃),
    Eq (α := (fun (X : Type u) ↦ X) X₄)
        ((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₄)
        ((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₁),
        (hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) x₁ = x₂ ∧
          (hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) x₁ = x₃
φ : X₁ ⟶ PullbackObj r b :=
  ↾fun (x₁ : X₁) ↦
    Subtype.mk (p := fun (p : X₂ × X₃) ↦
      Eq (α := (fun (X : Type u) ↦ X) X₄)
        ((hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) p.1 :
          (fun (X : Type u) ↦ X) X₄)
        ((hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) p.2 :
          (fun (X : Type u) ↦ X) X₄))
      ((hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) x₁,
        (hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) x₁)
      ⋯
hφ : IsIso φ
⊢ IsPullback t l r b

Tactic:
⟨⟨w⟩, ⟨IsLimit.ofIsoLimit ((Types.pullbackLimitCone r b).isLimit)
      (PullbackCone.ext (asIso φ)).symm⟩⟩

Premises used: CategoryTheory.IsPullback.mk, CategoryTheory.Limits.Types.pullbackLimitCone, CategoryTheory.CommSq.mk, Nonempty.intro, CategoryTheory.Limits.PullbackCone.ext, CategoryTheory.Iso.symm, CategoryTheory.Limits.LimitCone.isLimit, CategoryTheory.Limits.IsLimit.ofIsoLimit, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Goal:
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
w : t ≫ r = l ≫ b
h₁ :
  ∀ (x₁ y₁ : (fun (X : Type u) ↦ X) X₁),
    Eq (α := (fun (X : Type u) ↦ X) X₂)
          ((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₂)
          ((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₃)
          ((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₃)
          ((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₁
h₂ :
  ∀ (x₂ : (fun (X : Type u) ↦ X) X₂) (x₃ : (fun (X : Type u) ↦ X) X₃),
    Eq (α := (fun (X : Type u) ↦ X) X₄)
        ((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₄)
        ((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₁),
        (hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) x₁ = x₂ ∧
          (hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) x₁ = x₃
φ : X₁ ⟶ PullbackObj r b :=
  ↾fun (x₁ : X₁) ↦
    Subtype.mk (p := fun (p : X₂ × X₃) ↦
      Eq (α := (fun (X : Type u) ↦ X) X₄)
        ((hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) p.1 :
          (fun (X : Type u) ↦ X) X₄)
        ((hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) p.2 :
          (fun (X : Type u) ↦ X) X₄))
      ((hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) x₁,
        (hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) x₁)
      ⋯
hφ : IsIso φ
⊢ IsPullback t l r b

Tactic:
exact ⟨⟨w⟩, ⟨IsLimit.ofIsoLimit ((Types.pullbackLimitCone r b).isLimit)
      (PullbackCone.ext (asIso φ)).symm⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
⊢ HasPushouts (Type u)

Tactic:
hasPushouts_of_hasWidePushouts.{u} (Type u)

Premises used: CategoryTheory.Limits.hasPushouts_of_hasWidePushouts
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
h :
  ∀ (x : S),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ inl f g)).toFun x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (g ≫ inr f g)).toFun x
⊢ f ≫ inl f g = g ≫ inr f g

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x : S
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ inl f g)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (g ≫ inr f g)).toFun x

Tactic:
Quot.sound (Rel.inl_inr x)

Premises used: Quot.sound, CategoryTheory.Limits.Types.Pushout.Rel.inl_inr, CategoryTheory.Limits.Types.Pushout
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x : S
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ inl f g)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (g ≫ inr f g)).toFun x

Tactic:
exact Quot.sound (Rel.inl_inr x)

Premises used: Quot.sound, CategoryTheory.Limits.Types.Pushout.Rel.inl_inr
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s : PushoutCocone f g
t : S
⊢ Eq.{u + 1} (α := s.pt)
    ((fun (x : X₁ ⊕ X₂) ↦
        (match (motive := X₁ ⊕ X₂ → s.pt) x with
          | Sum.inl x₁ =>
            (ConcreteCategory.hom (FC := TypeCat.Fun) s.inl :
                (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) s.pt)
              x₁
          | Sum.inr x₂ =>
            (ConcreteCategory.hom (FC := TypeCat.Fun) s.inr :
                (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) s.pt)
              x₂ :
          s.pt))
      (Sum.inl
        ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) t)))
    ((fun (x : X₁ ⊕ X₂) ↦
        (match (motive := X₁ ⊕ X₂ → s.pt) x with
          | Sum.inl x₁ =>
            (ConcreteCategory.hom (FC := TypeCat.Fun) s.inl :
                (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) s.pt)
              x₁
          | Sum.inr x₂ =>
            (ConcreteCategory.hom (FC := TypeCat.Fun) s.inr :
                (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) s.pt)
              x₂ :
          s.pt))
      (Sum.inr
        ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) t)))

Tactic:
ConcreteCategory.congr_hom s.condition t

Premises used: CategoryTheory.Limits.PushoutCocone.condition, CategoryTheory.ConcreteCategory.congr_hom