-- Lean 4 proof step from Mathlib.CategoryTheory.Topos.Sheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst_1 : Mono m
X : Cᵒᵖ
⊢ IsPullback (m.app X) ((IsTerminal.from (Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit) F).app X) ((χ m).app X)
    (NatTrans.app (truth C) X)
have rw : m.app X ≫ (χ m).app X =
    (IsTerminal.from (Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit) F).app X ≫ NatTrans.app (truth C) X ∧
  (∀ (x₁ y₁ : (fun (X : Type (max u v)) ↦ X) (F.obj X)),
      Eq (α := (fun (X : Type (max u v)) ↦ X) (G.obj X))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app X) :
                  (a : (fun (X : Type (max u v)) ↦ X) (F.obj X)) → (fun (X : Type (max u v)) ↦ X) (G.obj X))
                x₁ :
              (fun (X : Type (max u v)) ↦ X) (G.obj X))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app X) :
                  (a : (fun (X : Type (max u v)) ↦ X) (F.obj X)) → (fun (X : Type (max u v)) ↦ X) (G.obj X))
                y₁ :
              (fun (X : Type (max u v)) ↦ X) (G.obj X)) ∧
          Eq (α :=
            (fun (X : Type (max u v)) ↦ X) (Functor.obj (Functor.obj (Functor.const Cᵒᵖ) PUnit.{(max u v) + 1}) X))
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    ((IsTerminal.from (Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit) F).app X) :
                  (a : (fun (X : Type (max u v)) ↦ X) (F.obj X)) →
                    (fun (X : Type (max u v)) ↦ X) (((Functor.const Cᵒᵖ).obj PUnit.{(max u v) + 1}).obj X))
                x₁ :
              (fun (X : Type (max u v)) ↦ X) (Functor.obj (Functor.obj (Functor.const Cᵒᵖ) PUnit.{(max u v) + 1}) X))
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    ((IsTerminal.from (Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit) F).app X) :
                  (a : (fun (X : Type (max u v)) ↦ X) (F.obj X)) →
                    (fun (X : Type (max u v)) ↦ X) (((Functor.const Cᵒᵖ).obj PUnit.{(max u v) + 1}).obj X))
                y₁ :
              (fun (X : Type (max u v)) ↦ X) (Functor.obj (Functor.obj (Functor.const Cᵒᵖ) PUnit.{(max u v) + 1}) X)) →
        x₁ = y₁) ∧
    ∀ (x₂ : (fun (X : Type (max u v)) ↦ X) (G.obj X))
      (x₃ : (fun (X : Type (max u v)) ↦ X) (Functor.obj (Functor.obj (Functor.const Cᵒᵖ) PUnit.{(max u v) + 1}) X)),
      Eq (α := (fun (X : Type (max u v)) ↦ X) (Functor.obj (Functor.sieves C) X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) ((χ m).app X) :
                (a : (fun (X : Type (max u v)) ↦ X) (G.obj X)) →
                  (fun (X : Type (max u v)) ↦ X) ((Functor.sieves C).obj X))
              x₂ :
            (fun (X : Type (max u v)) ↦ X) (Functor.obj (Functor.sieves C) X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (truth C) X) :
                (a : (fun (X : Type (max u v)) ↦ X) (((Functor.const Cᵒᵖ).obj PUnit.{(max u v) + 1}).obj X)) →
                  (fun (X : Type (max u v)) ↦ X) ((Functor.sieves C).obj X))
              x₃ :
            (fun (X : Type (max u v)) ↦ X) (Functor.obj (Functor.sieves C) X)) →
        ∃ (x₁ : (fun (X : Type (max u v)) ↦ X) (F.obj X)),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (m.app X) :
                  (a : (fun (X : Type (max u v)) ↦ X) (F.obj X)) → (fun (X : Type (max u v)) ↦ X) (G.obj X))
                x₁ =
              x₂ ∧
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                    ((IsTerminal.from (Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit) F).app X) :
                  (a : (fun (X : Type (max u v)) ↦ X) (F.obj X)) →
                    (fun (X : Type (max u v)) ↦ X) (((Functor.const Cᵒᵖ).obj PUnit.{(max u v) + 1}).obj X))
                x₁ =
              x₃
Tactic: rw [Types.isPullback_iff]