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₄
h : IsPullback t l r b
x₁ y₁ : X₁
h₁ :
  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₂)
h₂ :
  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₃)
dsimp :
  Eq (α := PullbackObj r b)
    (((h.isLimit.conePointUniqueUpToIso
              ((pullbackCone r b).isLimitAux
                (fun (s : PullbackCone r b) ↦
                  ↾fun (x : s.pt) ↦
                    Subtype.mk (p := fun (p : X₂ × X₃) ↦
                      Eq (α := X₄) ((hom (FC := TypeCat.Fun) r : (a : X₂) → X₄) p.1 : X₄)
                        ((hom (FC := TypeCat.Fun) b : (a : X₃) → X₄) p.2 : X₄))
                      ((hom (FC := TypeCat.Fun) s.fst : (a : s.pt) → X₂) x,
                        (hom (FC := TypeCat.Fun) s.snd : (a : s.pt) → X₃) x)
                      ⋯)
                ⋯ ⋯ ⋯)).toEquiv :
          (a : h.cone.pt) → PullbackObj r b)
        x₁ :
      PullbackObj r b)
    (((h.isLimit.conePointUniqueUpToIso
              ((pullbackCone r b).isLimitAux
                (fun (s : PullbackCone r b) ↦
                  ↾fun (x : s.pt) ↦
                    Subtype.mk (p := fun (p : X₂ × X₃) ↦
                      Eq (α := X₄) ((hom (FC := TypeCat.Fun) r : (a : X₂) → X₄) p.1 : X₄)
                        ((hom (FC := TypeCat.Fun) b : (a : X₃) → X₄) p.2 : X₄))
                      ((hom (FC := TypeCat.Fun) s.fst : (a : s.pt) → X₂) x,
                        (hom (FC := TypeCat.Fun) s.snd : (a : s.pt) → X₃) x)
                      ⋯)
                ⋯ ⋯ ⋯)).toEquiv :
          (a : h.cone.pt) → PullbackObj r b)
        y₁ :
      PullbackObj r b)
⊢ Eq (α := (pullbackLimitCone r b).cone.pt)
    (((h.isLimit.conePointUniqueUpToIso (pullbackLimitCone r b).isLimit).toEquiv :
          (a : h.cone.pt) → (pullbackLimitCone r b).cone.pt)
        x₁ :
      (pullbackLimitCone r b).cone.pt)
    (((h.isLimit.conePointUniqueUpToIso (pullbackLimitCone r b).isLimit).toEquiv :
          (a : h.cone.pt) → (pullbackLimitCone r b).cone.pt)
        y₁ :
      (pullbackLimitCone r b).cone.pt)

Tactic:
dsimp
-- 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₄
h : IsPullback t l r b
x₁ y₁ : X₁
h₁ :
  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₂)
h₂ :
  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₃)
⊢ Eq.{u + 1} (α := X₂)
    (↑(((h.isLimit.conePointUniqueUpToIso
                  ((pullbackCone r b).isLimitAux
                    (fun (s : PullbackCone r b) ↦
                      ↾fun (x : s.pt) ↦
                        Subtype.mk (p := fun (p : X₂ × X₃) ↦
                          Eq (α := X₄) ((hom (FC := TypeCat.Fun) r : (a : X₂) → X₄) p.1 : X₄)
                            ((hom (FC := TypeCat.Fun) b : (a : X₃) → X₄) p.2 : X₄))
                          ((hom (FC := TypeCat.Fun) s.fst : (a : s.pt) → X₂) x,
                            (hom (FC := TypeCat.Fun) s.snd : (a : s.pt) → X₃) x)
                          ⋯)
                    ⋯ ⋯ ⋯)).toEquiv :
              (a : h.cone.pt) → PullbackObj r b)
            x₁) :
        X₂ × X₃).1
    (↑(((h.isLimit.conePointUniqueUpToIso
                  ((pullbackCone r b).isLimitAux
                    (fun (s : PullbackCone r b) ↦
                      ↾fun (x : s.pt) ↦
                        Subtype.mk (p := fun (p : X₂ × X₃) ↦
                          Eq (α := X₄) ((hom (FC := TypeCat.Fun) r : (a : X₂) → X₄) p.1 : X₄)
                            ((hom (FC := TypeCat.Fun) b : (a : X₃) → X₄) p.2 : X₄))
                          ((hom (FC := TypeCat.Fun) s.fst : (a : s.pt) → X₂) x,
                            (hom (FC := TypeCat.Fun) s.snd : (a : s.pt) → X₃) x)
                          ⋯)
                    ⋯ ⋯ ⋯)).toEquiv :
              (a : h.cone.pt) → PullbackObj r b)
            y₁) :
        X₂ × X₃).1

Tactic:
assumption
-- 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₄
h : IsPullback t l r b
x₁ y₁ : X₁
h₁ :
  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₂)
h₂ :
  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₃)
⊢ Eq.{u + 1} (α := X₃)
    (↑(((h.isLimit.conePointUniqueUpToIso
                  ((pullbackCone r b).isLimitAux
                    (fun (s : PullbackCone r b) ↦
                      ↾fun (x : s.pt) ↦
                        Subtype.mk (p := fun (p : X₂ × X₃) ↦
                          Eq (α := X₄) ((hom (FC := TypeCat.Fun) r : (a : X₂) → X₄) p.1 : X₄)
                            ((hom (FC := TypeCat.Fun) b : (a : X₃) → X₄) p.2 : X₄))
                          ((hom (FC := TypeCat.Fun) s.fst : (a : s.pt) → X₂) x,
                            (hom (FC := TypeCat.Fun) s.snd : (a : s.pt) → X₃) x)
                          ⋯)
                    ⋯ ⋯ ⋯)).toEquiv :
              (a : h.cone.pt) → PullbackObj r b)
            x₁) :
        X₂ × X₃).2
    (↑(((h.isLimit.conePointUniqueUpToIso
                  ((pullbackCone r b).isLimitAux
                    (fun (s : PullbackCone r b) ↦
                      ↾fun (x : s.pt) ↦
                        Subtype.mk (p := fun (p : X₂ × X₃) ↦
                          Eq (α := X₄) ((hom (FC := TypeCat.Fun) r : (a : X₂) → X₄) p.1 : X₄)
                            ((hom (FC := TypeCat.Fun) b : (a : X₃) → X₄) p.2 : X₄))
                          ((hom (FC := TypeCat.Fun) s.fst : (a : s.pt) → X₂) x,
                            (hom (FC := TypeCat.Fun) s.snd : (a : s.pt) → X₃) x)
                          ⋯)
                    ⋯ ⋯ ⋯)).toEquiv :
              (a : h.cone.pt) → PullbackObj r b)
            y₁) :
        X₂ × X₃).2

Tactic:
assumption
-- 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₄
h : IsPullback t l r b
x₂ : X₂
x₃ : X₃
hx :
  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₄)
obtain :
  ∀ (x₁ : h.cone.pt)
    (hx₁ :
      Eq (α := PullbackObj r b)
        ((PullbackCone.IsLimit.equivPullbackObj h.isLimit : (a : h.cone.pt) → PullbackObj r b) x₁ : PullbackObj r b)
        (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₄))
            (x₂, x₃) hx :
          { 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₄) })),
    ∃ (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₁ : (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₃

Tactic:
obtain ⟨x₁, hx₁⟩ :=
    (PullbackCone.IsLimit.equivPullbackObj h.isLimit).surjective ⟨⟨x₂, x₃⟩, hx⟩

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj, Prod.mk, Subtype.mk, Equiv.surjective, CategoryTheory.IsPullback.isLimit
-- 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₄
h : IsPullback t l r b
x₂ : X₂
x₃ : X₃
hx :
  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₁ : h.cone.pt
hx₁ :
  Eq (α := PullbackObj r b)
    ((PullbackCone.IsLimit.equivPullbackObj h.isLimit : (a : h.cone.pt) → PullbackObj r b) x₁ : PullbackObj r b)
    (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₄))
        (x₂, x₃) hx :
      { 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₄) })
⊢ (↑((PullbackCone.IsLimit.equivPullbackObj h.isLimit : (a : h.cone.pt) → PullbackObj r b) x₁) : 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₄))
          (x₂, x₃) hx) :
      X₂ × X₃)

Tactic:
rw [Subtype.ext_iff] at hx₁

Premises used: Subtype.ext_iff
-- 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₄
h : IsPullback t l r b
x₂ : X₂
x₃ : X₃
hx :
  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₁ : h.cone.pt
hx₁ :
  (↑((PullbackCone.IsLimit.equivPullbackObj h.isLimit : (a : h.cone.pt) → PullbackObj r b) x₁) : 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₄))
          (x₂, x₃) hx) :
      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₃

Tactic:
⟨x₁, congr_arg _root_.Prod.fst hx₁,
    congr_arg _root_.Prod.snd hx₁⟩

Premises used: Prod.fst, congr_arg, And.intro, Exists.intro, 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₄
h : IsPullback t l r b
x₂ : X₂
x₃ : X₃
hx :
  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₁ : h.cone.pt
hx₁ :
  (↑((PullbackCone.IsLimit.equivPullbackObj h.isLimit : (a : h.cone.pt) → PullbackObj r b) x₁) : 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₄))
          (x₂, x₃) hx) :
      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₃

Tactic:
exact ⟨x₁, congr_arg _root_.Prod.fst hx₁,
    congr_arg _root_.Prod.snd hx₁⟩
-- 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₄
h : IsPullback t l r b
⊢ t ≫ r = l ≫ b ∧
    (∀ (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₁) ∧
      ∀ (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₃

Tactic:
⟨h.w, fun x₁ y₁ ⟨h₁, h₂⟩ ↦ ext_of_isPullback h h₁ h₂, exists_of_isPullback h⟩

Premises used: And.intro, _private.0.CategoryTheory.Limits.Types.isPullback_iff.match_1, CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w, Eq, CategoryTheory.Limits.Types.ext_of_isPullback, CategoryTheory.Limits.Types.exists_of_isPullback
-- 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₄
h : IsPullback t l r b
⊢ t ≫ r = l ≫ b ∧
    (∀ (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₁) ∧
      ∀ (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₃

Tactic:
exact ⟨h.w, fun x₁ y₁ ⟨h₁, h₂⟩ ↦ ext_of_isPullback h h₁ h₂, exists_of_isPullback 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₁)
      ⋯
rw :
  Function.Bijective (α := (fun (X : Type u) ↦ X) X₁) (β := (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))
⊢ IsIso φ

Tactic:
rw [isIso_iff_bijective]

Premises used: CategoryTheory.isIso_iff_bijective
-- 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₁)
      ⋯
left :
  Function.Injective (α := (fun (X : Type u) ↦ X) X₁) (β := (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))
right :
  Function.Surjective (α := (fun (X : Type u) ↦ X) X₁) (β := (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))
⊢ Function.Bijective (α := (fun (X : Type u) ↦ X) X₁) (β := (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))

Tactic:
constructor