-- 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ᵒᵖ
⊢ 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₃
have refine_1 : ∀ (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₁
Tactic: refine ⟨congr(($(comp_χ_eq m)).app X), ?_, ?_⟩