awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
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₂
⊢ ∀ (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χ'
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
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}) ↦ ⊤
⊢ ∀ (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χ'
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
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₁
⊢ ∀ (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χ'
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
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

Tactic:
Sieve.ext fun Y f => ?_

Premises used: CategoryTheory.Sieve.ext
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
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₂
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
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app X)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((χ m).app X)).toFun x

Tactic:
refine Sieve.ext fun Y f => ?_

Premises used: CategoryTheory.Sieve.ext
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
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
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 := ⋯ : Sieve.{v, u} (Opposite.unop X) }))
        x)
      f
⊢ ((ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app X)).toFun x).arrows f ↔
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((χ m).app X)).toFun x).arrows f

Tactic:
simp only [χ_app, Opposite.op_unop]

Premises used: CategoryTheory.Presheaf.χ_app, Opposite.op_unop
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
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
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 := ⋯ : Sieve.{v, u} (Opposite.unop X) }))
        x)
      f.op.unop
⊢ ((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

Tactic:
rw [Sieve.mem_iff_pullback_eq_top, ← Quiver.Hom.unop_op f]

Premises used: CategoryTheory.Sieve.mem_iff_pullback_eq_top, Quiver.Hom.unop_op
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
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
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))
⊢ 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

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
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
⊢ Eq (α := Functor.obj (Functor.sieves C) (Opposite.op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.sieves C) f.op) :
          (a : (Functor.sieves C).obj (Opposite.op (Opposite.unop X))) → (Functor.sieves C).obj (Opposite.op Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.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) :
      Functor.obj (Functor.sieves C) (Opposite.op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (↾fun (S : Sieve.{v, u} (Opposite.unop (Opposite.op (Opposite.unop X)))) ↦ Sieve.pullback f.op.unop S) :
          (a : (Functor.sieves C).obj (Opposite.op (Opposite.unop X))) → (Functor.sieves C).obj (Opposite.op Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.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) :
      Functor.obj (Functor.sieves C) (Opposite.op Y))

Tactic:
have := ConcreteCategory.congr_hom (Functor.sieves_map C (f.op)) (χ'.app X x)
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
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
this :
  Eq (α := Functor.obj (Functor.sieves C) (Opposite.op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.sieves C) f.op) :
          (a : (Functor.sieves C).obj (Opposite.op (Opposite.unop X))) → (Functor.sieves C).obj (Opposite.op Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.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) :
      Functor.obj (Functor.sieves C) (Opposite.op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (↾fun (S : Sieve.{v, u} (Opposite.unop (Opposite.op (Opposite.unop X)))) ↦ Sieve.pullback f.op.unop S) :
          (a : (Functor.sieves C).obj (Opposite.op (Opposite.unop X))) → (Functor.sieves C).obj (Opposite.op Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.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) :
      Functor.obj (Functor.sieves C) (Opposite.op Y))
a : F.obj (Opposite.op Y)
h :
  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))
w :
  Eq (α := Sieve.{v, u} Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app (Opposite.op Y)) : (a : G.obj (Opposite.op Y)) → Sieve Y)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Y)) :
            (a : F.obj (Opposite.op Y)) → G.obj (Opposite.op Y))
          a) :
      Sieve.{v, u} Y)
    (⊤ : Sieve.{v, u} Y)
⊢ Eq (α := Sieve.{v, u} Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app (Opposite.op Y)) : (a : G.obj (Opposite.op Y)) → Sieve Y)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f.op) : (a : G.obj X) → G.obj (Opposite.op Y)) x) :
      Sieve.{v, u} Y)
    (⊤ : Sieve.{v, u} Y)

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
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
this :
  Eq (α := Functor.obj (Functor.sieves C) (Opposite.op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.sieves C) f.op) :
          (a : (Functor.sieves C).obj (Opposite.op (Opposite.unop X))) → (Functor.sieves C).obj (Opposite.op Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.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) :
      Functor.obj (Functor.sieves C) (Opposite.op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (↾fun (S : Sieve.{v, u} (Opposite.unop (Opposite.op (Opposite.unop X)))) ↦ Sieve.pullback f.op.unop S) :
          (a : (Functor.sieves C).obj (Opposite.op (Opposite.unop X))) → (Functor.sieves C).obj (Opposite.op Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.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) :
      Functor.obj (Functor.sieves C) (Opposite.op Y))
a : F.obj (Opposite.op Y)
h :
  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))
⊢ Eq (α := Sieve.{v, u} Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app (Opposite.op Y)) : (a : G.obj (Opposite.op Y)) → Sieve Y)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Y)) :
            (a : F.obj (Opposite.op Y)) → G.obj (Opposite.op Y))
          a) :
      Sieve.{v, u} Y)
    (⊤ : Sieve.{v, u} Y)

Tactic:
simpa using congr($(h₁ (.op Y)) a)
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst_1 : Mono m
hF : Presieve.IsSheaf J F
hG : Presieve.IsSeparated J G
X : Cᵒᵖ
x : G.obj X
Y : C
f : Y ⟶ Opposite.unop X
hf :
  J.Covers
    ((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)
    f
simp :
  Sieve.arrows
    ((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) }) :
        (a : G.obj X) → (Functor.sieves C).obj X)
      x)
    f
⊢ Sieve.arrows
    ((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)
    f

Tactic:
simp only [Presheaf.χ_app, Opposite.op_unop] at hf ⊢

Premises used: CategoryTheory.Presheaf.χ_app, Opposite.op_unop
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : GrothendieckTopology.{v, u} C
F G : Sheaf J_1 (Type (max u v))
J : GrothendieckTopology.{v, u} C
rw : Presieve.IsSheaf J (closedSieves J).toFunctor
⊢ Presheaf.IsSheaf J (closedSieves J).toFunctor

Tactic:
rw [CategoryTheory.isSheaf_iff_isSheaf_of_type]

Premises used: CategoryTheory.isSheaf_iff_isSheaf_of_type