awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sheaves.Sheafify
Goal:
X : TopCat
F : Presheaf (Type v) X
x : (↑X : Type v)
U : Opens (↑X : Type v)
m : x ∈ U
s : ToType (FC := TypeCat.Fun) (F.obj (op U))
⊢ ∃ (_ :
    (Sheafify.isLocallyGerm F).toPrelocalPredicate (T := fun (x : (↑X : Type v)) ↦ F.stalk x).pred (T :=
      fun (x : (↑X : Type v)) ↦ F.stalk x) (U :=
      (↑(Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) U m) : Opens (↑X : Type v)))
      fun (y : ↥(↑(Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) U m) : Opens (↑X : Type v))) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.germ (↑(Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) U m) : Opens (↑X : Type v))
              (↑y : (↑X : Type v)) ⋯) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op (↑⟨U, m⟩ : Opens (↑X : Type v))))) →
            (fun (X : Type v) ↦ X) (F.stalk (↑y : (↑X : Type v))))
        s),
    Eq (α :=
      F.stalk
        (↑(Subtype.mk (p := fun (x_2 : (↑X : Type v)) ↦
              x_2 ∈ (↑(Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) U m) : Opens (↑X : Type v))) x ⋯) :
          (↑X : Type v)))
      ((fun (y : ↥(↑(Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) U m) : Opens (↑X : Type v))) ↦
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (F.germ (↑(Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) U m) : Opens (↑X : Type v))
                      (↑y : (↑X : Type v)) ⋯) :
                  (a : (fun (X : Type v) ↦ X) (F.obj (op (↑⟨U, m⟩ : Opens (↑X : Type v))))) →
                    (fun (X : Type v) ↦ X) (F.stalk (↑y : (↑X : Type v))))
                s :
              (fun (X : Type v) ↦ X) (F.stalk (↑y : (↑X : Type v)))))
          (Subtype.mk (p := fun (x_2 : (↑X : Type v)) ↦
            x_2 ∈ (↑(Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) U m) : Opens (↑X : Type v))) x ⋯) :
        (fun (X : Type v) ↦ X)
          (F.stalk
            (↑(Subtype.mk (p := fun (x_2 : (↑X : Type v)) ↦
                  x_2 ∈ (↑(Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) U m) : Opens (↑X : Type v))) x ⋯) :
              (↑X : Type v))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.germ U x m) : (a : F.obj (op U)) → F.stalk x) s : F.stalk x)

Tactic:
⟨PrelocalPredicate.sheafifyOf ⟨s, fun _ => rfl⟩, rfl⟩

Premises used: TopCat.PrelocalPredicate.sheafifyOf, Exists.intro, rfl
-- Module: Mathlib.Topology.Sheaves.Sheafify
Goal:
X : TopCat
F : Presheaf (Type v) X
x : (↑X : Type v)
U : Opens (↑X : Type v)
m : x ∈ U
s : ToType (FC := TypeCat.Fun) (F.obj (op U))
⊢ ∃ (_ :
    (Sheafify.isLocallyGerm F).toPrelocalPredicate (T := fun (x : (↑X : Type v)) ↦ F.stalk x).pred (T :=
      fun (x : (↑X : Type v)) ↦ F.stalk x) (U :=
      (↑(Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) U m) : Opens (↑X : Type v)))
      fun (y : ↥(↑(Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) U m) : Opens (↑X : Type v))) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.germ (↑(Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) U m) : Opens (↑X : Type v))
              (↑y : (↑X : Type v)) ⋯) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op (↑⟨U, m⟩ : Opens (↑X : Type v))))) →
            (fun (X : Type v) ↦ X) (F.stalk (↑y : (↑X : Type v))))
        s),
    Eq (α :=
      F.stalk
        (↑(Subtype.mk (p := fun (x_2 : (↑X : Type v)) ↦
              x_2 ∈ (↑(Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) U m) : Opens (↑X : Type v))) x ⋯) :
          (↑X : Type v)))
      ((fun (y : ↥(↑(Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) U m) : Opens (↑X : Type v))) ↦
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (F.germ (↑(Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) U m) : Opens (↑X : Type v))
                      (↑y : (↑X : Type v)) ⋯) :
                  (a : (fun (X : Type v) ↦ X) (F.obj (op (↑⟨U, m⟩ : Opens (↑X : Type v))))) →
                    (fun (X : Type v) ↦ X) (F.stalk (↑y : (↑X : Type v))))
                s :
              (fun (X : Type v) ↦ X) (F.stalk (↑y : (↑X : Type v)))))
          (Subtype.mk (p := fun (x_2 : (↑X : Type v)) ↦
            x_2 ∈ (↑(Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) U m) : Opens (↑X : Type v))) x ⋯) :
        (fun (X : Type v) ↦ X)
          (F.stalk
            (↑(Subtype.mk (p := fun (x_2 : (↑X : Type v)) ↦
                  x_2 ∈ (↑(Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) U m) : Opens (↑X : Type v))) x ⋯) :
              (↑X : Type v))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.germ U x m) : (a : F.obj (op U)) → F.stalk x) s : F.stalk x)

Tactic:
exact ⟨PrelocalPredicate.sheafifyOf ⟨s, fun _ => rfl⟩, rfl⟩
-- Module: Mathlib.Topology.Sheaves.Sheafify
Goal:
X : TopCat
F : Presheaf (Type v) X
x : (↑X : Type v)
w :
  ∀ (U V : OpenNhds x) (fU : (y : ↥(↑U : Opens (↑X : Type v))) → F.stalk (↑y : (↑X : Type v))),
    (Sheafify.isLocallyGerm F).toPrelocalPredicate (T := fun (x : (↑X : Type v)) ↦ F.stalk x).pred (T :=
        fun (x : (↑X : Type v)) ↦ F.stalk x) fU →
      ∀ (fV : (y : ↥(↑V : Opens (↑X : Type v))) → F.stalk (↑y : (↑X : Type v))),
        (Sheafify.isLocallyGerm F).toPrelocalPredicate (T := fun (x : (↑X : Type v)) ↦ F.stalk x).pred (T :=
            fun (x : (↑X : Type v)) ↦ F.stalk x) fV →
          Eq.{v + 1} (α :=
              F.stalk
                (↑(Subtype.mk (p := fun (x_3 : (↑X : Type v)) ↦ x_3 ∈ (↑U : Opens (↑X : Type v))) x ⋯) : (↑X : Type v)))
              (fU (Subtype.mk (p := fun (x_3 : (↑X : Type v)) ↦ x_3 ∈ (↑U : Opens (↑X : Type v))) x ⋯))
              (fV (Subtype.mk (p := fun (x_3 : (↑X : Type v)) ↦ x_3 ∈ (↑V : Opens (↑X : Type v))) x ⋯)) →
            ∃ (W : OpenNhds x) (iU : W ⟶ U) (iV : W ⟶ V),
              ∀ (w : ↥(↑W : Opens (↑X : Type v))),
                Eq.{v + 1} (α :=
                  F.stalk (↑((iU : (a : ↥(↑W : Opens (↑X : Type v))) → ↥(↑U : Opens (↑X : Type v))) w) : (↑X : Type v)))
                  (fU ((iU : (a : ↥(↑W : Opens (↑X : Type v))) → ↥(↑U : Opens (↑X : Type v))) w))
                  (fV ((iV : (a : ↥(↑W : Opens (↑X : Type v))) → ↥(↑V : Opens (↑X : Type v))) w))
⊢ Function.Injective (α := (fun (X : Type v) ↦ X) (F.sheafify.presheaf.stalk x)) (β :=
    (fun (X : Type v) ↦ X) (F.stalk x))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.stalkToFiber x)) :
      (a : (fun (X : Type v) ↦ X) (F.sheafify.presheaf.stalk x)) → (fun (X : Type v) ↦ X) (F.stalk x))

Tactic:
apply TopCat.stalkToFiber_injective

Premises used: TopCat.stalkToFiber_injective
-- Module: Mathlib.Topology.Sheaves.Sheafify
Goal:
X : TopCat
F : Presheaf (Type v) X
x : (↑X : Type v)
U V : OpenNhds x
fU : (y : ↥(↑U : Opens (↑X : Type v))) → F.stalk (↑y : (↑X : Type v))
hU :
  (Sheafify.isLocallyGerm F).toPrelocalPredicate (T := fun (x : (↑X : Type v)) ↦ F.stalk x).pred (T :=
    fun (x : (↑X : Type v)) ↦ F.stalk x) fU
fV : (y : ↥(↑V : Opens (↑X : Type v))) → F.stalk (↑y : (↑X : Type v))
hV :
  (Sheafify.isLocallyGerm F).toPrelocalPredicate (T := fun (x : (↑X : Type v)) ↦ F.stalk x).pred (T :=
    fun (x : (↑X : Type v)) ↦ F.stalk x) fV
e :
  Eq (α :=
    F.stalk (↑(Subtype.mk (p := fun (x_1 : (↑X : Type v)) ↦ x_1 ∈ (↑U : Opens (↑X : Type v))) x ⋯) : (↑X : Type v)))
    (fU (Subtype.mk (p := fun (x_1 : (↑X : Type v)) ↦ x_1 ∈ (↑U : Opens (↑X : Type v))) x ⋯))
    (fV (Subtype.mk (p := fun (x_1 : (↑X : Type v)) ↦ x_1 ∈ (↑V : Opens (↑X : Type v))) x ⋯))
w :
  ∀ (U' : Opens (↑X : Type v))
    (mU : (↑(Subtype.mk (p := fun (x_1 : (↑X : Type v)) ↦ x_1 ∈ (↑U : Opens (↑X : Type v))) x ⋯) : (↑X : Type v)) ∈ U')
    (iU : U' ⟶ (↑U : Opens (↑X : Type v))) (gU : F.obj (op U'))
    (wU :
      ∀ (x_1 : ↥U'),
        Eq (α := F.stalk (↑x_1 : (↑X : Type v)))
          ((fun (x_2 : ↥U') ↦
                (fU ((iU : (a : ↥U') → ↥(↑U : Opens (↑X : Type v))) x_2) :
                  ?T (↑((iU : (a : ↥U') → ↥(↑U : Opens (↑X : Type v))) x_2) : (↑?X : Type ?u.5027))))
              x_1 :
            F.stalk (↑((iU : (a : ↥U') → ↥(↑U : Opens (↑X : Type v))) x_1) : (↑X : Type ?u.5027)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.germ U' (↑x_1 : (↑X : Type v)) ⋯) :
                (a : (fun (X : Type v) ↦ X) (F.obj (op U'))) → (fun (X : Type v) ↦ X) (F.stalk (↑x_1 : (↑X : Type v))))
              gU :
            (fun (X : Type v) ↦ X) (F.stalk (↑x_1 : (↑X : Type v))))),
    ∃ (W : OpenNhds x) (iU : W ⟶ U) (iV : W ⟶ V),
      ∀ (w : ↥(↑W : Opens (↑X : Type v))),
        Eq (α := F.stalk (↑((iU : (a : ↥(↑W : Opens (↑X : Type v))) → ↥(↑U : Opens (↑X : Type v))) w) : (↑X : Type v)))
          (fU ((iU : (a : ↥(↑W : Opens (↑X : Type v))) → ↥(↑U : Opens (↑X : Type v))) w))
          (fV ((iV : (a : ↥(↑W : Opens (↑X : Type v))) → ↥(↑V : Opens (↑X : Type v))) w))
⊢ ∃ (W : OpenNhds x) (iU : W ⟶ U) (iV : W ⟶ V),
    ∀ (w : ↥(↑W : Opens (↑X : Type v))),
      Eq (α := F.stalk (↑((iU : (a : ↥(↑W : Opens (↑X : Type v))) → ↥(↑U : Opens (↑X : Type v))) w) : (↑X : Type v)))
        (fU ((iU : (a : ↥(↑W : Opens (↑X : Type v))) → ↥(↑U : Opens (↑X : Type v))) w))
        (fV ((iV : (a : ↥(↑W : Opens (↑X : Type v))) → ↥(↑V : Opens (↑X : Type v))) w))

Tactic:
rcases hU ⟨x, U.2⟩ with ⟨U', mU, iU, gU, wU⟩

Premises used: Subtype.mk, Subtype.property
-- Module: Mathlib.Topology.Sheaves.Sheafify
Goal:
X : TopCat
p₀ : (↑X : Type v)
C : Type u
inst : Category.{v, u} C
inst_1 : Limits.HasColimits.{v, u} C
inst_2 : Limits.HasTerminal.{v, u} C
𝓕 : Presheaf C X
inst_3 : HasWeakSheafify.{v, v, v, u} (C := Opens (↑X : Type v)) (Opens.grothendieckTopology (↑X : Type v)) C
⊢ IsIso (X := Functor.obj (stalkFunctor C p₀) 𝓕) (Y :=
    Functor.obj (stalkFunctor C p₀) (CategoryTheory.sheafify (Opens.grothendieckTopology (↑X : Type v)) 𝓕))
    (CategoryTheory.Functor.map (stalkFunctor C p₀)
      (CategoryTheory.toSheafify (Opens.grothendieckTopology (↑X : Type v)) 𝓕))

Tactic:
Adjunction.isIso_map_unit_of_isLeftAdjoint_comp (sheafificationAdjunction _ C)
    (skyscraperSheafForgetAdjunction p₀)

Premises used: CategoryTheory.sheafificationAdjunction, CategoryTheory.Adjunction.isIso_map_unit_of_isLeftAdjoint_comp, skyscraperSheafForgetAdjunction
-- Module: Mathlib.Topology.Sheaves.Sheafify
Goal:
X : TopCat
p₀ : (↑X : Type v)
C : Type u
inst : Category.{v, u} C
inst_1 : Limits.HasColimits.{v, u} C
inst_2 : Limits.HasTerminal.{v, u} C
𝓕 : Presheaf C X
inst_3 : HasWeakSheafify.{v, v, v, u} (C := Opens (↑X : Type v)) (Opens.grothendieckTopology (↑X : Type v)) C
⊢ IsIso (X := Functor.obj (stalkFunctor C p₀) 𝓕) (Y :=
    Functor.obj (stalkFunctor C p₀) (CategoryTheory.sheafify (Opens.grothendieckTopology (↑X : Type v)) 𝓕))
    (CategoryTheory.Functor.map (stalkFunctor C p₀)
      (CategoryTheory.toSheafify (Opens.grothendieckTopology (↑X : Type v)) 𝓕))

Tactic:
exact Adjunction.isIso_map_unit_of_isLeftAdjoint_comp (sheafificationAdjunction _ C)
    (skyscraperSheafForgetAdjunction p₀)

Premises used: CategoryTheory.sheafificationAdjunction, CategoryTheory.Adjunction.isIso_map_unit_of_isLeftAdjoint_comp, skyscraperSheafForgetAdjunction
-- Module: Mathlib.Topology.Sheaves.Sheafify
Goal:
X : TopCat
p₀ : (↑X : Type v)
C : Type u
inst : Category.{v, u} C
inst_1 : Limits.HasColimits.{v, u} C
inst_2 : Limits.HasTerminal.{v, u} C
𝓕 : Presheaf C X
inst_3 : HasWeakSheafify.{v, v, v, u} (C := Opens (↑X : Type v)) (Opens.grothendieckTopology (↑X : Type v)) C
⊢ IsIso (X := Functor.obj (stalkFunctor C p₀) 𝓕) (Y :=
    Functor.obj (stalkFunctor C p₀) (CategoryTheory.sheafify (Opens.grothendieckTopology (↑X : Type v)) 𝓕))
    (CategoryTheory.Functor.map (stalkFunctor C p₀)
      (CategoryTheory.toSheafify (Opens.grothendieckTopology (↑X : Type v)) 𝓕))

Tactic:
classical
  exact Adjunction.isIso_map_unit_of_isLeftAdjoint_comp (sheafificationAdjunction _ C)
    (skyscraperSheafForgetAdjunction p₀)
-- Module: Mathlib.Topology.Sheaves.Skyscraper
Goal:
X : TopCat
p₀ : (↑X : Type u)
inst : (U : Opens (↑X : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{w, v} C
inst_2 : HasTerminal.{w, v} C
A : C
U V : (Opens (↑X : Type u))ᵒᵖ
i : U ⟶ V
h : p₀ ∈ unop V
⊢ p₀ ∈ unop U

Tactic:
simpa using i.unop.le h

Premises used: Quiver.Hom.le, Quiver.Hom.unop
-- Module: Mathlib.Topology.Sheaves.Skyscraper
Goal:
X : TopCat
p₀ : (↑X : Type u)
inst : (U : Opens (↑X : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{w, v} C
inst_2 : HasTerminal.{w, v} C
A : C
U V : (Opens (↑X : Type u))ᵒᵖ
i : U ⟶ V
h : p₀ ∈ unop V
rw : (if p₀ ∈ unop U then A else terminal.{w, v} C) = A
rw₁ rw₂ : A = A
⊢ (if p₀ ∈ unop U then A else terminal.{w, v} C) = if p₀ ∈ unop V then A else terminal.{w, v} C

Tactic:
rw [if_pos h, if_pos (by simpa using i.unop.le h)]

Premises used: if_pos
-- Module: Mathlib.Topology.Sheaves.Skyscraper
Goal:
X : TopCat
p₀ : (↑X : Type u)
inst : (U : Opens (↑X : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{w, v} C
inst_2 : HasTerminal.{w, v} C
A : C
U V W : (Opens (↑X : Type u))ᵒᵖ
iVU : U ⟶ V
iWV : V ⟶ W
pos :
  ∀ (hW : p₀ ∈ unop W),
    Eq.{w + 1} (α := (if p₀ ∈ unop U then A else terminal.{w, v} C) ⟶ if p₀ ∈ unop W then A else terminal.{w, v} C)
      (if h : p₀ ∈ unop W then eqToHom ⋯
      else
        IsTerminal.from (Eq.ndrec (motive := IsTerminal.{w, v}) terminalIsTerminal ⋯)
          (if p₀ ∈ unop U then A else terminal.{w, v} C))
      (CategoryStruct.comp (Y := if p₀ ∈ unop V then A else terminal.{w, v} C)
        (if h : p₀ ∈ unop V then eqToHom ⋯
        else
          IsTerminal.from (Eq.ndrec (motive := IsTerminal.{w, v}) terminalIsTerminal ⋯)
            (if p₀ ∈ unop U then A else terminal.{w, v} C))
        (if h : p₀ ∈ unop W then eqToHom ⋯
        else
          IsTerminal.from (Eq.ndrec (motive := IsTerminal.{w, v}) terminalIsTerminal ⋯)
            (if p₀ ∈ unop V then A else terminal.{w, v} C)))
neg :
  ∀ (hW : p₀ ∉ unop W),
    Eq.{w + 1} (α := (if p₀ ∈ unop U then A else terminal.{w, v} C) ⟶ if p₀ ∈ unop W then A else terminal.{w, v} C)
      (if h : p₀ ∈ unop W then eqToHom ⋯
      else
        IsTerminal.from (Eq.ndrec (motive := IsTerminal.{w, v}) terminalIsTerminal ⋯)
          (if p₀ ∈ unop U then A else terminal.{w, v} C))
      (CategoryStruct.comp (Y := if p₀ ∈ unop V then A else terminal.{w, v} C)
        (if h : p₀ ∈ unop V then eqToHom ⋯
        else
          IsTerminal.from (Eq.ndrec (motive := IsTerminal.{w, v}) terminalIsTerminal ⋯)
            (if p₀ ∈ unop U then A else terminal.{w, v} C))
        (if h : p₀ ∈ unop W then eqToHom ⋯
        else
          IsTerminal.from (Eq.ndrec (motive := IsTerminal.{w, v}) terminalIsTerminal ⋯)
            (if p₀ ∈ unop V then A else terminal.{w, v} C)))
⊢ Eq.{w + 1} (α := (if p₀ ∈ unop U then A else terminal.{w, v} C) ⟶ if p₀ ∈ unop W then A else terminal.{w, v} C)
    (if h : p₀ ∈ unop W then eqToHom ⋯
    else
      IsTerminal.from (Eq.ndrec (motive := IsTerminal.{w, v}) terminalIsTerminal ⋯)
        (if p₀ ∈ unop U then A else terminal.{w, v} C))
    (CategoryStruct.comp (Y := if p₀ ∈ unop V then A else terminal.{w, v} C)
      (if h : p₀ ∈ unop V then eqToHom ⋯
      else
        IsTerminal.from (Eq.ndrec (motive := IsTerminal.{w, v}) terminalIsTerminal ⋯)
          (if p₀ ∈ unop U then A else terminal.{w, v} C))
      (if h : p₀ ∈ unop W then eqToHom ⋯
      else
        IsTerminal.from (Eq.ndrec (motive := IsTerminal.{w, v}) terminalIsTerminal ⋯)
          (if p₀ ∈ unop V then A else terminal.{w, v} C)))

Tactic:
by_cases hW : p₀ ∈ unop W

Premises used: Opposite.unop
-- Module: Mathlib.Topology.Sheaves.Skyscraper
Goal:
X : TopCat
p₀ : (↑X : Type u)
inst : (U : Opens (↑X : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{w, v} C
inst_2 : HasTerminal.{w, v} C
A : C
U V W : (Opens (↑X : Type u))ᵒᵖ
iVU : U ⟶ V
iWV : V ⟶ W
hW : p₀ ∈ unop W
⊢ p₀ ∈ unop V

Tactic:
have hV : p₀ ∈ unop V := leOfHom iWV.unop hW
-- Module: Mathlib.Topology.Sheaves.Skyscraper
Goal:
X : TopCat
p₀ : (↑X : Type u)
inst : (U : Opens (↑X : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{w, v} C
inst_2 : HasTerminal.{w, v} C
A : C
U V W : (Opens (↑X : Type u))ᵒᵖ
iVU : U ⟶ V
iWV : V ⟶ W
hW : p₀ ∈ unop W
hV : p₀ ∈ unop V
⊢ Eq.{w + 1} (α := (if p₀ ∈ unop U then A else terminal.{w, v} C) ⟶ if p₀ ∈ unop W then A else terminal.{w, v} C)
    (if h : p₀ ∈ unop W then eqToHom ⋯
    else
      IsTerminal.from (Eq.ndrec (motive := IsTerminal.{w, v}) terminalIsTerminal ⋯)
        (if p₀ ∈ unop U then A else terminal.{w, v} C))
    (CategoryStruct.comp (Y := if p₀ ∈ unop V then A else terminal.{w, v} C)
      (if h : p₀ ∈ unop V then eqToHom ⋯
      else
        IsTerminal.from (Eq.ndrec (motive := IsTerminal.{w, v}) terminalIsTerminal ⋯)
          (if p₀ ∈ unop U then A else terminal.{w, v} C))
      (if h : p₀ ∈ unop W then eqToHom ⋯
      else
        IsTerminal.from (Eq.ndrec (motive := IsTerminal.{w, v}) terminalIsTerminal ⋯)
          (if p₀ ∈ unop V then A else terminal.{w, v} C)))

Tactic:
simp only [dif_pos hW, dif_pos hV, eqToHom_trans]

Premises used: dif_pos, CategoryTheory.eqToHom_trans
-- Module: Mathlib.Topology.Sheaves.Skyscraper
Goal:
X : TopCat
p₀ : (↑X : Type u)
inst : (U : Opens (↑X : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{w, v} C
inst_2 : HasTerminal.{w, v} C
A : C
U V W : (Opens (↑X : Type u))ᵒᵖ
iVU : U ⟶ V
iWV : V ⟶ W
hW : p₀ ∉ unop W
neg :
  Eq.{w + 1} (α := (if p₀ ∈ unop U then A else terminal.{w, v} C) ⟶ if p₀ ∈ unop W then A else terminal.{w, v} C)
    (if h : p₀ ∈ unop W then eqToHom ⋯
    else
      IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
          (if p₀ ∈ unop W then A else terminal.{w, v} C) ⋯)
        (if p₀ ∈ unop U then A else terminal.{w, v} C))
    (CategoryStruct.comp (Y := if p₀ ∈ unop V then A else terminal.{w, v} C)
      (if h : p₀ ∈ unop V then eqToHom ⋯
      else
        IsTerminal.from
          (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
            (if p₀ ∈ unop V then A else terminal.{w, v} C) ⋯)
          (if p₀ ∈ unop U then A else terminal.{w, v} C))
      (if h : p₀ ∈ unop W then eqToHom ⋯
      else
        IsTerminal.from
          (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
            (if p₀ ∈ unop W then A else terminal.{w, v} C) ⋯)
          (if p₀ ∈ unop V then A else terminal.{w, v} C)))
⊢ Eq.{w + 1} (α := (if p₀ ∈ unop U then A else terminal.{w, v} C) ⟶ if p₀ ∈ unop W then A else terminal.{w, v} C)
    (if h : p₀ ∈ unop W then eqToHom ⋯
    else
      IsTerminal.from (Eq.ndrec (motive := IsTerminal.{w, v}) terminalIsTerminal ⋯)
        (if p₀ ∈ unop U then A else terminal.{w, v} C))
    (CategoryStruct.comp (Y := if p₀ ∈ unop V then A else terminal.{w, v} C)
      (if h : p₀ ∈ unop V then eqToHom ⋯
      else
        IsTerminal.from (Eq.ndrec (motive := IsTerminal.{w, v}) terminalIsTerminal ⋯)
          (if p₀ ∈ unop U then A else terminal.{w, v} C))
      (if h : p₀ ∈ unop W then eqToHom ⋯
      else
        IsTerminal.from (Eq.ndrec (motive := IsTerminal.{w, v}) terminalIsTerminal ⋯)
          (if p₀ ∈ unop V then A else terminal.{w, v} C)))

Tactic:
dsimp
-- Module: Mathlib.Topology.Sheaves.Skyscraper
Goal:
X : TopCat
p₀ : (↑X : Type u)
inst : (U : Opens (↑X : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{w, v} C
inst_2 : HasTerminal.{w, v} C
A : C
U V W : (Opens (↑X : Type u))ᵒᵖ
iVU : U ⟶ V
iWV : V ⟶ W
hW : p₀ ∉ unop W
neg :
  Eq.{w + 1} (α := (if p₀ ∈ unop U then A else terminal.{w, v} C) ⟶ if p₀ ∈ unop W then A else terminal.{w, v} C)
    (IsTerminal.from
      (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
        (if p₀ ∈ unop W then A else terminal.{w, v} C) ⋯)
      (if p₀ ∈ unop U then A else terminal.{w, v} C))
    (CategoryStruct.comp (Y := if p₀ ∈ unop V then A else terminal.{w, v} C)
      (if h : p₀ ∈ unop V then eqToHom ⋯
      else
        IsTerminal.from
          (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
            (if p₀ ∈ unop V then A else terminal.{w, v} C) ⋯)
          (if p₀ ∈ unop U then A else terminal.{w, v} C))
      (if h : p₀ ∈ unop W then eqToHom ⋯
      else
        IsTerminal.from
          (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
            (if p₀ ∈ unop W then A else terminal.{w, v} C) ⋯)
          (if p₀ ∈ unop V then A else terminal.{w, v} C)))
⊢ Eq.{w + 1} (α := (if p₀ ∈ unop U then A else terminal.{w, v} C) ⟶ if p₀ ∈ unop W then A else terminal.{w, v} C)
    (if h : p₀ ∈ unop W then eqToHom ⋯
    else
      IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
          (if p₀ ∈ unop W then A else terminal.{w, v} C) ⋯)
        (if p₀ ∈ unop U then A else terminal.{w, v} C))
    (CategoryStruct.comp (Y := if p₀ ∈ unop V then A else terminal.{w, v} C)
      (if h : p₀ ∈ unop V then eqToHom ⋯
      else
        IsTerminal.from
          (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
            (if p₀ ∈ unop V then A else terminal.{w, v} C) ⋯)
          (if p₀ ∈ unop U then A else terminal.{w, v} C))
      (if h : p₀ ∈ unop W then eqToHom ⋯
      else
        IsTerminal.from
          (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
            (if p₀ ∈ unop W then A else terminal.{w, v} C) ⋯)
          (if p₀ ∈ unop V then A else terminal.{w, v} C)))

Tactic:
rw [dif_neg hW]

Premises used: dif_neg
-- Module: Mathlib.Topology.Sheaves.Skyscraper
Goal:
X : TopCat
p₀ : (↑X : Type u)
inst : (U : Opens (↑X : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{w, v} C
inst_2 : HasTerminal.{w, v} C
A : C
U V W : (Opens (↑X : Type u))ᵒᵖ
iVU : U ⟶ V
iWV : V ⟶ W
hW : p₀ ∉ unop W
⊢ Eq.{w + 1} (α := (if p₀ ∈ unop U then A else terminal.{w, v} C) ⟶ if p₀ ∈ unop W then A else terminal.{w, v} C)
    (IsTerminal.from
      (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
        (if p₀ ∈ unop W then A else terminal.{w, v} C) ⋯)
      (if p₀ ∈ unop U then A else terminal.{w, v} C))
    (CategoryStruct.comp (Y := if p₀ ∈ unop V then A else terminal.{w, v} C)
      (if h : p₀ ∈ unop V then eqToHom ⋯
      else
        IsTerminal.from
          (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
            (if p₀ ∈ unop V then A else terminal.{w, v} C) ⋯)
          (if p₀ ∈ unop U then A else terminal.{w, v} C))
      (if h : p₀ ∈ unop W then eqToHom ⋯
      else
        IsTerminal.from
          (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
            (if p₀ ∈ unop W then A else terminal.{w, v} C) ⋯)
          (if p₀ ∈ unop V then A else terminal.{w, v} C)))

Tactic:
apply ((if_neg hW).symm.ndrec terminalIsTerminal).hom_ext

Premises used: Eq.ndrec, CategoryTheory.Limits.IsTerminal.hom_ext, CategoryTheory.Limits.terminalIsTerminal, Eq.symm, if_neg
-- Module: Mathlib.Topology.Sheaves.Skyscraper
Goal:
X : TopCat
p₀ : (↑X : Type u)
inst : (U : Opens (↑X : Type u)) → Decidable (p₀ ∈ U)
C : Type v
inst_1 : Category.{w, v} C
inst_2 : HasTerminal.{w, v} C
A : C
hd : (U : Opens (↑(of PUnit.{u + 1}) : Type u)) → Decidable (PUnit.unit ∈ U)
h : Eq (α := Presheaf.{u, w, v} C X) (skyscraperPresheaf p₀ A) (skyscraperPresheaf p₀ A)
convert_2 :
  Eq (α := Presheaf.{u, w, v} C X) (skyscraperPresheaf p₀ A)
    (Functor.obj (C := Presheaf.{u, w, v} C (of (↑(of PUnit.{u + 1}) : Type u)))
      (Presheaf.pushforward C (ofHom (ContinuousMap.const (↑(of PUnit.{u + 1}) : Type u) p₀)))
      (skyscraperPresheaf PUnit.unit A))
⊢ Eq (α := Presheaf.{u, w, v} C X) (skyscraperPresheaf p₀ A)
    (Functor.obj (C := Presheaf.{u, w, v} C (of (↑(of PUnit.{u + 1}) : Type u)))
      (Presheaf.pushforward C (ofHom (ContinuousMap.const (↑(of PUnit.{u + 1}) : Type u) p₀)))
      (skyscraperPresheaf PUnit.unit A))

Tactic:
convert_to @skyscraperPresheaf X p₀ (fun U => hd <| (Opens.map <| ofHom <|
      ContinuousMap.const _ p₀).obj U)
    C _ _ A = _

Premises used: skyscraperPresheaf