awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pullbacks (goal)
Goal:
P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
e : P ≅ PullbackObj f g := h.isoPullback ≪≫ pullbackIsoPullback f g
this :
  Eq (α := (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) X)
    (⇑(hom (FC := TypeCat.Fun) fst) : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) X)
    (Function.comp (β := X × Y) _root_.Prod.fst
      (Function.comp (β :=
        { p : X × Y //
          Eq (α := (fun (X : Type u) ↦ X) Z)
            ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z) p.1 :
              (fun (X : Type u) ↦ X) Z)
            ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) p.2 :
              (fun (X : Type u) ↦ X) Z) })
        (Subtype.val (p := fun (p : X × Y) ↦
          Eq (α := (fun (X : Type u) ↦ X) Z)
            ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z) p.1 :
              (fun (X : Type u) ↦ X) Z)
            ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) p.2 :
              (fun (X : Type u) ↦ X) Z)))
        (⇑(hom (FC := TypeCat.Fun) e.hom) : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) (PullbackObj f g))))
⊢ Eq (α := Set ((fun (X : Type u) ↦ X) X))
    (Set.range (ι := (fun (X : Type u) ↦ X) P)
      (⇑(hom (FC := TypeCat.Fun) fst) : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) X))
    (Set.preimage (β := (fun (X : Type u) ↦ X) Z)
      (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z)
      (Set.range (ι := (fun (X : Type u) ↦ X) Y)
        (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z)))
have rw : Eq (α := Set ((fun (X : Type u) ↦ X) X))
  (Set.image (α := X × Y) _root_.Prod.fst
    (Set.image (α :=
      { p : X × Y //
        Eq (α := (fun (X : Type u) ↦ X) Z)
          ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z) p.1 :
            (fun (X : Type u) ↦ X) Z)
          ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) p.2 :
            (fun (X : Type u) ↦ X) Z) })
      (Subtype.val (p := fun (p : X × Y) ↦
        Eq (α := (fun (X : Type u) ↦ X) Z)
          ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z) p.1 :
            (fun (X : Type u) ↦ X) Z)
          ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) p.2 :
            (fun (X : Type u) ↦ X) Z)))
      Set.univ))
  (Set.preimage (β := (fun (X : Type u) ↦ X) Z)
    (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z)
    (Set.range (ι := (fun (X : Type u) ↦ X) Y)
      (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z)))
Tactic: rw [this, Set.range_comp, Set.range_comp, Set.range_eq_univ.mpr (surjective_of_epi e.hom)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pullbacks (goal)
Goal:
P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
⊢ Eq (α := Set ((fun (X : Type u) ↦ X) Y))
    (Set.range (ι := (fun (X : Type u) ↦ X) P)
      (⇑(hom (FC := TypeCat.Fun) snd) : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) Y))
    (Set.preimage (β := (fun (X : Type u) ↦ X) Z)
      (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z)
      (Set.range (ι := (fun (X : Type u) ↦ X) X)
        (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z)))
have rw : Eq (α := Set ((fun (X : Type u) ↦ X) Y))
  (Set.preimage (β := (fun (X : Type u) ↦ X) Z)
    (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z)
    (Set.range (ι := (fun (X : Type u) ↦ X) X)
      (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z)))
  (Set.preimage (β := (fun (X : Type u) ↦ X) Z)
    (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z)
    (Set.range (ι := (fun (X : Type u) ↦ X) X)
      (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z)))
Tactic: rw [range_fst_of_isPullback (IsPullback.flip h)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pullbacks (goal)
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 (α := (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)
have 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)
                    sorry)
              sorry sorry sorry)).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)
                    sorry)
              sorry sorry sorry)).toEquiv :
        (a : h.cone.pt) → PullbackObj r b)
      y₁ :
    PullbackObj r b)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pullbacks (goal)
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₁ : (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₃
have 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₃
Tactic: obtain ⟨x₁, hx₁⟩ :=
    (PullbackCone.IsLimit.equivPullbackObj h.isLimit).surjective ⟨⟨x₂, x₃⟩, hx⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pullbacks (hypothesis)
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₄) })
⊢ ∃ (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₃
have 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₃)
Tactic: rw [Subtype.ext_iff] at hx₁
Cleared hypotheses: hx₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pullbacks (goal)
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 φ
have 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))
Tactic: rw [isIso_iff_bijective]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pullbacks (goal)
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₁)
      ⋯
⊢ 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))
have 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))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pullbacks (goal)
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))
⊢ 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))
have 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))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pullbacks (hypothesis)
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))
⊢ a₁ = a₂
have 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₃)
Tactic: simp [φ] at h
Cleared hypotheses: h