awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Thin (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Quiver.IsThin.{u₁, v₁} C
X Y : C
i₁ i₂ : X ≅ Y
⊢ i₁ = i₂
have w : i₁.hom = i₂.hom
Tactic: ext1
-- 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
X : Cᵒᵖ
x : G.obj X
Y Z : C
f : Y ⟶ Opposite.unop X
a : (fun (X : Type (max u v)) ↦ X) (F.obj (Opposite.op Y))
ha :
  Eq (α := (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f.op) :
          (a : (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op (Opposite.unop X)))) →
            (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y)))
        x :
      (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Y)) :
          (a : (fun (X : Type (max u v)) ↦ X) (F.obj (Opposite.op Y))) →
            (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y)))
        a :
      (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y)))
g : Z ⟶ Y
⊢ ∃ (a : (fun (X : Type (max u v)) ↦ X) (F.obj (Opposite.op Z))),
    Eq (α := (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map (g ≫ f).op) :
            (a : (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op (Opposite.unop X)))) →
              (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
          x :
        (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Z)) :
            (a : (fun (X : Type (max u v)) ↦ X) (F.obj (Opposite.op Z))) →
              (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
          a :
        (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
have h : Eq (α := (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map (g ≫ f).op) :
        (a : (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op (Opposite.unop X)))) →
          (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
      x :
    (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Z)) :
        (a : (fun (X : Type (max u v)) ↦ X) (F.obj (Opposite.op Z))) →
          (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g.op) :
          (a : (fun (X : Type (max u v)) ↦ X) (F.obj (Opposite.op Y))) →
            (fun (X : Type (max u v)) ↦ X) (F.obj (Opposite.op Z)))
        a) :
    (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
Tactic: use F.map g.op a
-- 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
⊢ m ≫ χ m = IsTerminal.from (Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit) F ≫ truth C
have w : ∀ (x : Cᵒᵖ) (x_1 : F.obj x),
  (ConcreteCategory.hom (FC := TypeCat.Fun) ((m ≫ χ m).app x)).toFun x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((IsTerminal.from (Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit) F ≫ truth C).app x)).toFun
      x_1
Tactic: ext
-- 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
x : Cᵒᵖ
x_1 : F.obj x
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) ((m ≫ χ m).app x)).toFun x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((IsTerminal.from (Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit) F ≫ truth C).app x)).toFun
      x_1
have w : ∀ ⦃Y : C⦄ (f : Y ⟶ Opposite.unop x),
  ((ConcreteCategory.hom (FC := TypeCat.Fun) ((m ≫ χ m).app x)).toFun x_1).arrows f ↔
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((IsTerminal.from (Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit) F ≫ truth C).app x)).toFun
          x_1).arrows
      f
Tactic: apply Sieve.ext
-- 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
⊢ IsPullback m (IsTerminal.from (Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit) F) (χ m) (truth C)
have refine : ∀ (X : Cᵒᵖ),
  IsPullback (m.app X) ((IsTerminal.from (Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit) F).app X) ((χ m).app X)
    (NatTrans.app (truth C) X)
Tactic: refine IsPullback.of_forall_isPullback_app fun X => ?_
-- 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ᵒᵖ
⊢ ∀ (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_2 : ∀ (x₂ : G.obj X),
  {
        arrows := fun (Y : C) (f : Y ⟶ Opposite.unop X) ↦
          ∃ (a : F.obj (Opposite.op Y)),
            Eq (α := G.obj (Opposite.op Y))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f.op) : (a : G.obj X) → G.obj (Opposite.op Y)) x₂ :
                G.obj (Opposite.op Y))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Y)) :
                    (a : F.obj (Opposite.op Y)) → G.obj (Opposite.op Y))
                  a :
                G.obj (Opposite.op Y)),
        downward_closed := sorry : Sieve.{v, u} (Opposite.unop X) } =
      ⊤ →
    ∃ (x₁ : F.obj X), (ConcreteCategory.hom (FC := TypeCat.Fun) (m.app X) : (a : F.obj X) → G.obj X) x₁ = x₂
Tactic: simp only [Functor.const_obj_obj, Functor.sieves_obj, χ_app, Opposite.op_unop,
      TypeCat.hom_ofHom, TypeCat.Fun.coe_mk, truth_app, Functor.isTerminalConst_from_app,
      Types.isTerminalPUnit_from_apply, and_true, forall_const]
-- 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
χ' : G ⟶ Functor.sieves C
hχ' : IsPullback m (IsTerminal.from (Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit) F) χ' (truth C)
⊢ χ' = χ m
have w : ∀ (X : Cᵒᵖ) (x : G.obj X),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app X)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((χ m).app X)).toFun x
Tactic: ext X x
-- Lean 4 proof step from Mathlib.CategoryTheory.Topos.Sheaf (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
χ' : G ⟶ Functor.sieves C
hχ' : IsPullback m (IsTerminal.from (Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit) F) χ' (truth C)
X : Cᵒᵖ
x : G.obj X
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app X)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((χ m).app X)).toFun x
have hχ'₁ : (∀ (x : Cᵒᵖ), m.app x ≫ χ'.app x = Types.isTerminalPUnit.from (F.obj x) ≫ ↾fun (x_1 : PUnit.{(max u v) + 1}) ↦ ⊤) ∧
  (∀ (x : Cᵒᵖ) (x₁ y₁ : F.obj x),
      Eq (α := G.obj x) ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) x₁ : G.obj x)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) y₁ : G.obj x) →
        x₁ = y₁) ∧
    ∀ (x : Cᵒᵖ) (x₂ : G.obj x),
      Eq (α := Sieve.{v, u} (Opposite.unop x))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app x) : (a : G.obj x) → Sieve (Opposite.unop x)) x₂ :
            Sieve.{v, u} (Opposite.unop x))
          (⊤ : Sieve.{v, u} (Opposite.unop x)) →
        ∃ (x₁ : F.obj x), (ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) x₁ = x₂
Tactic: simp only [IsPullback.iff_app, Functor.const_obj_obj, Functor.sieves_obj,
    Functor.isTerminalConst_from_app, truth_app, Types.isPullback_iff,
    Types.isTerminalPUnit_from_apply, and_true, TypeCat.hom_ofHom, TypeCat.Fun.coe_mk,
    forall_const, forall_and] at hχ'
Cleared hypotheses: hχ'
-- Lean 4 proof step from Mathlib.CategoryTheory.Topos.Sheaf (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
χ' : G ⟶ Functor.sieves C
X : Cᵒᵖ
x : G.obj X
hχ' :
  (∀ (x : Cᵒᵖ), m.app x ≫ χ'.app x = Types.isTerminalPUnit.from (F.obj x) ≫ ↾fun (x_1 : PUnit.{(max u v) + 1}) ↦ ⊤) ∧
    (∀ (x : Cᵒᵖ) (x₁ y₁ : F.obj x),
        Eq (α := G.obj x) ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) x₁ : G.obj x)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) y₁ : G.obj x) →
          x₁ = y₁) ∧
      ∀ (x : Cᵒᵖ) (x₂ : G.obj x),
        Eq (α := Sieve.{v, u} (Opposite.unop x))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app x) : (a : G.obj x) → Sieve (Opposite.unop x)) x₂ :
              Sieve.{v, u} (Opposite.unop x))
            (⊤ : Sieve.{v, u} (Opposite.unop x)) →
          ∃ (x₁ : F.obj x), (ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) x₁ = x₂
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app X)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((χ m).app X)).toFun x
have h₁ : ∀ (x : Cᵒᵖ), m.app x ≫ χ'.app x = Types.isTerminalPUnit.from (F.obj x) ≫ ↾fun (x_1 : PUnit.{(max u v) + 1}) ↦ ⊤
Tactic: obtain ⟨h₁, h₂, h₃⟩ := hχ'
Cleared hypotheses: hχ'
-- Lean 4 proof step from Mathlib.CategoryTheory.Topos.Sheaf (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
χ' : G ⟶ Functor.sieves C
X : Cᵒᵖ
x : G.obj X
hχ' :
  (∀ (x : Cᵒᵖ), m.app x ≫ χ'.app x = Types.isTerminalPUnit.from (F.obj x) ≫ ↾fun (x_1 : PUnit.{(max u v) + 1}) ↦ ⊤) ∧
    (∀ (x : Cᵒᵖ) (x₁ y₁ : F.obj x),
        Eq (α := G.obj x) ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) x₁ : G.obj x)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) y₁ : G.obj x) →
          x₁ = y₁) ∧
      ∀ (x : Cᵒᵖ) (x₂ : G.obj x),
        Eq (α := Sieve.{v, u} (Opposite.unop x))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app x) : (a : G.obj x) → Sieve (Opposite.unop x)) x₂ :
              Sieve.{v, u} (Opposite.unop x))
            (⊤ : Sieve.{v, u} (Opposite.unop x)) →
          ∃ (x₁ : F.obj x), (ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) x₁ = x₂
h₁ : ∀ (x : Cᵒᵖ), m.app x ≫ χ'.app x = Types.isTerminalPUnit.from (F.obj x) ≫ ↾fun (x_1 : PUnit.{(max u v) + 1}) ↦ ⊤
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app X)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((χ m).app X)).toFun x
have h₂ : ∀ (x : Cᵒᵖ) (x₁ y₁ : F.obj x),
  Eq (α := G.obj x) ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) x₁ : G.obj x)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) y₁ : G.obj x) →
    x₁ = y₁
Tactic: obtain ⟨h₁, h₂, h₃⟩ := hχ'
Cleared hypotheses: hχ'
-- Lean 4 proof step from Mathlib.CategoryTheory.Topos.Sheaf (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
χ' : G ⟶ Functor.sieves C
X : Cᵒᵖ
x : G.obj X
hχ' :
  (∀ (x : Cᵒᵖ), m.app x ≫ χ'.app x = Types.isTerminalPUnit.from (F.obj x) ≫ ↾fun (x_1 : PUnit.{(max u v) + 1}) ↦ ⊤) ∧
    (∀ (x : Cᵒᵖ) (x₁ y₁ : F.obj x),
        Eq (α := G.obj x) ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) x₁ : G.obj x)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) y₁ : G.obj x) →
          x₁ = y₁) ∧
      ∀ (x : Cᵒᵖ) (x₂ : G.obj x),
        Eq (α := Sieve.{v, u} (Opposite.unop x))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app x) : (a : G.obj x) → Sieve (Opposite.unop x)) x₂ :
              Sieve.{v, u} (Opposite.unop x))
            (⊤ : Sieve.{v, u} (Opposite.unop x)) →
          ∃ (x₁ : F.obj x), (ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) x₁ = x₂
h₁ : ∀ (x : Cᵒᵖ), m.app x ≫ χ'.app x = Types.isTerminalPUnit.from (F.obj x) ≫ ↾fun (x_1 : PUnit.{(max u v) + 1}) ↦ ⊤
h₂ :
  ∀ (x : Cᵒᵖ) (x₁ y₁ : F.obj x),
    Eq (α := G.obj x) ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) x₁ : G.obj x)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) y₁ : G.obj x) →
      x₁ = y₁
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app X)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((χ m).app X)).toFun x
have h₃ : ∀ (x : Cᵒᵖ) (x₂ : G.obj x),
  Eq (α := Sieve.{v, u} (Opposite.unop x))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app x) : (a : G.obj x) → Sieve (Opposite.unop x)) x₂ :
        Sieve.{v, u} (Opposite.unop x))
      (⊤ : Sieve.{v, u} (Opposite.unop x)) →
    ∃ (x₁ : F.obj x), (ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) x₁ = x₂
Tactic: obtain ⟨h₁, h₂, h₃⟩ := hχ'
Cleared hypotheses: hχ'
-- 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
χ' : G ⟶ Functor.sieves C
X : Cᵒᵖ
x : G.obj X
h₁ : ∀ (x : Cᵒᵖ), m.app x ≫ χ'.app x = Types.isTerminalPUnit.from (F.obj x) ≫ ↾fun (x_1 : PUnit.{(max u v) + 1}) ↦ ⊤
h₂ :
  ∀ (x : Cᵒᵖ) (x₁ y₁ : F.obj x),
    Eq (α := G.obj x) ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) x₁ : G.obj x)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) y₁ : G.obj x) →
      x₁ = y₁
h₃ :
  ∀ (x : Cᵒᵖ) (x₂ : G.obj x),
    Eq (α := Sieve.{v, u} (Opposite.unop x))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app x) : (a : G.obj x) → Sieve (Opposite.unop x)) x₂ :
          Sieve.{v, u} (Opposite.unop x))
        (⊤ : Sieve.{v, u} (Opposite.unop x)) →
      ∃ (x₁ : F.obj x), (ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) x₁ = x₂
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app X)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((χ m).app X)).toFun x
have w : ∀ (Y : C) (f : Y ⟶ Opposite.unop X),
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app X)).toFun x).arrows f ↔
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((χ m).app X)).toFun x).arrows f
Tactic: refine Sieve.ext fun Y f => ?_
-- 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
χ' : G ⟶ Functor.sieves C
X : Cᵒᵖ
x : G.obj X
h₁ : ∀ (x : Cᵒᵖ), m.app x ≫ χ'.app x = Types.isTerminalPUnit.from (F.obj x) ≫ ↾fun (x_1 : PUnit.{(max u v) + 1}) ↦ ⊤
h₂ :
  ∀ (x : Cᵒᵖ) (x₁ y₁ : F.obj x),
    Eq (α := G.obj x) ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) x₁ : G.obj x)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) y₁ : G.obj x) →
      x₁ = y₁
h₃ :
  ∀ (x : Cᵒᵖ) (x₂ : G.obj x),
    Eq (α := Sieve.{v, u} (Opposite.unop x))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app x) : (a : G.obj x) → Sieve (Opposite.unop x)) x₂ :
          Sieve.{v, u} (Opposite.unop x))
        (⊤ : Sieve.{v, u} (Opposite.unop x)) →
      ∃ (x₁ : F.obj x), (ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) x₁ = x₂
Y : C
f : Y ⟶ Opposite.unop X
⊢ ((ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app X)).toFun x).arrows f ↔
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((χ m).app X)).toFun x).arrows f
have w : ((ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app X)).toFun x).arrows f ↔
  Sieve.arrows
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾fun (x : G.obj X) ↦
          {
            arrows := fun (Y : C) (f : Y ⟶ Opposite.unop X) ↦
              ∃ (a : F.obj (Opposite.op Y)),
                Eq (α := G.obj (Opposite.op Y))
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f.op) : (a : G.obj X) → G.obj (Opposite.op Y)) x :
                    G.obj (Opposite.op Y))
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Y)) :
                        (a : F.obj (Opposite.op Y)) → G.obj (Opposite.op Y))
                      a :
                    G.obj (Opposite.op Y)),
            downward_closed := sorry : Sieve.{v, u} (Opposite.unop X) }))
      x)
    f
Tactic: simp only [χ_app, Opposite.op_unop]
-- 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
χ' : G ⟶ Functor.sieves C
X : Cᵒᵖ
x : G.obj X
h₁ : ∀ (x : Cᵒᵖ), m.app x ≫ χ'.app x = Types.isTerminalPUnit.from (F.obj x) ≫ ↾fun (x_1 : PUnit.{(max u v) + 1}) ↦ ⊤
h₂ :
  ∀ (x : Cᵒᵖ) (x₁ y₁ : F.obj x),
    Eq (α := G.obj x) ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) x₁ : G.obj x)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) y₁ : G.obj x) →
      x₁ = y₁
h₃ :
  ∀ (x : Cᵒᵖ) (x₂ : G.obj x),
    Eq (α := Sieve.{v, u} (Opposite.unop x))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app x) : (a : G.obj x) → Sieve (Opposite.unop x)) x₂ :
          Sieve.{v, u} (Opposite.unop x))
        (⊤ : Sieve.{v, u} (Opposite.unop x)) →
      ∃ (x₁ : F.obj x), (ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) x₁ = x₂
Y : C
f : Y ⟶ Opposite.unop X
⊢ ((ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app X)).toFun x).arrows f ↔
    Sieve.arrows
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾fun (x : G.obj X) ↦
            {
              arrows := fun (Y : C) (f : Y ⟶ Opposite.unop X) ↦
                ∃ (a : F.obj (Opposite.op Y)),
                  Eq (α := G.obj (Opposite.op Y))
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f.op) : (a : G.obj X) → G.obj (Opposite.op Y)) x :
                      G.obj (Opposite.op Y))
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Y)) :
                          (a : F.obj (Opposite.op Y)) → G.obj (Opposite.op Y))
                        a :
                      G.obj (Opposite.op Y)),
              downward_closed := ⋯ : Sieve.{v, u} (Opposite.unop X) }))
        x)
      f
have w : Sieve.pullback f.op.unop ((ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app X)).toFun x) = ⊤ ↔
  Sieve.arrows
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾fun (x : G.obj X) ↦
          {
            arrows := fun (Y : C) (f : Y ⟶ Opposite.unop X) ↦
              ∃ (a : F.obj (Opposite.op Y)),
                Eq (α := G.obj (Opposite.op Y))
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f.op) : (a : G.obj X) → G.obj (Opposite.op Y)) x :
                    G.obj (Opposite.op Y))
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Y)) :
                        (a : F.obj (Opposite.op Y)) → G.obj (Opposite.op Y))
                      a :
                    G.obj (Opposite.op Y)),
            downward_closed := sorry : Sieve.{v, u} (Opposite.unop X) }))
      x)
    f.op.unop
Tactic: rw [Sieve.mem_iff_pullback_eq_top, ← Quiver.Hom.unop_op f]
-- 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
χ' : G ⟶ Functor.sieves C
X : Cᵒᵖ
x : G.obj X
h₁ : ∀ (x : Cᵒᵖ), m.app x ≫ χ'.app x = Types.isTerminalPUnit.from (F.obj x) ≫ ↾fun (x_1 : PUnit.{(max u v) + 1}) ↦ ⊤
h₂ :
  ∀ (x : Cᵒᵖ) (x₁ y₁ : F.obj x),
    Eq (α := G.obj x) ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) x₁ : G.obj x)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) y₁ : G.obj x) →
      x₁ = y₁
h₃ :
  ∀ (x : Cᵒᵖ) (x₂ : G.obj x),
    Eq (α := Sieve.{v, u} (Opposite.unop x))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app x) : (a : G.obj x) → Sieve (Opposite.unop x)) x₂ :
          Sieve.{v, u} (Opposite.unop x))
        (⊤ : Sieve.{v, u} (Opposite.unop x)) →
      ∃ (x₁ : F.obj x), (ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) x₁ = x₂
Y : C
f : Y ⟶ Opposite.unop X
⊢ Sieve.pullback f.op.unop ((ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app X)).toFun x) = ⊤ ↔
    Sieve.arrows
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾fun (x : G.obj X) ↦
            {
              arrows := fun (Y : C) (f : Y ⟶ Opposite.unop X) ↦
                ∃ (a : F.obj (Opposite.op Y)),
                  Eq (α := G.obj (Opposite.op Y))
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f.op) : (a : G.obj X) → G.obj (Opposite.op Y)) x :
                      G.obj (Opposite.op Y))
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Y)) :
                          (a : F.obj (Opposite.op Y)) → G.obj (Opposite.op Y))
                        a :
                      G.obj (Opposite.op Y)),
              downward_closed := ⋯ : Sieve.{v, u} (Opposite.unop X) }))
        x)
      f.op.unop
have w : Sieve.pullback f ((ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app X) : (a : G.obj X) → Sieve (Opposite.unop X)) x) =
    ⊤ ↔
  ∃ (a : F.obj (Opposite.op Y)),
    Eq (α := G.obj (Opposite.op Y))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f.op) : (a : G.obj X) → G.obj (Opposite.op Y)) x :
        G.obj (Opposite.op Y))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Y)) :
            (a : F.obj (Opposite.op Y)) → G.obj (Opposite.op Y))
          a :
        G.obj (Opposite.op Y))
Tactic: dsimp