awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ Eq (α := Presheaf.{u, w, v} C X) (skyscraperPresheaf p₀ A) (skyscraperPresheaf p₀ A)

Tactic:
congr
-- 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)
⊢ 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:
congr
-- 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 a b : C
f : a ⟶ b
U V : (Opens (↑X : Type u))ᵒᵖ
i : U ⟶ V
simp :
  Eq.{w + 1} (α :=
    Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) U ⟶ Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ b) V)
    (CategoryStruct.comp (Y := Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) V)
      (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 V then eqToHom ⋯ ≫ f ≫ 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 b else terminal.{w, v} C) ⋯)
          (Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) V)))
    (CategoryStruct.comp (Y := Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ b) U)
      (if h : p₀ ∈ unop U then eqToHom ⋯ ≫ f ≫ eqToHom ⋯
      else
        IsTerminal.from
          (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
            (if p₀ ∈ unop U then b else terminal.{w, v} C) ⋯)
          (Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) U))
      (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 b else terminal.{w, v} C) ⋯)
          (if p₀ ∈ unop U then b else terminal.{w, v} C)))
⊢ Eq.{w + 1} (α :=
    Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) U ⟶ Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ b) V)
    (CategoryTheory.Functor.map (skyscraperPresheaf p₀ a) i ≫
      if h : p₀ ∈ unop V then eqToHom ⋯ ≫ f ≫ eqToHom ⋯
      else
        IsTerminal.from (Eq.ndrec (motive := IsTerminal.{w, v}) terminalIsTerminal ⋯)
          (Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) V))
    ((if h : p₀ ∈ unop U then eqToHom ⋯ ≫ f ≫ eqToHom ⋯
      else
        IsTerminal.from (Eq.ndrec (motive := IsTerminal.{w, v}) terminalIsTerminal ⋯)
          (Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) U)) ≫
      CategoryTheory.Functor.map (skyscraperPresheaf p₀ b) i)

Tactic:
simp only [skyscraperPresheaf_map]

Premises used: skyscraperPresheaf_map
-- 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 a b : C
f : a ⟶ b
U V : (Opens (↑X : Type u))ᵒᵖ
i : U ⟶ V
hV : p₀ ∈ unop V
⊢ p₀ ∈ unop U

Tactic:
have hU : p₀ ∈ U.unop := leOfHom i.unop hV
-- 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 a b : C
f : a ⟶ b
U V : (Opens (↑X : Type u))ᵒᵖ
i : U ⟶ V
hV : p₀ ∈ unop V
hU : p₀ ∈ unop U
⊢ Eq.{w + 1} (α :=
    Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) U ⟶ Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ b) V)
    (CategoryStruct.comp (Y := Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) V)
      (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 V then eqToHom ⋯ ≫ f ≫ 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 b else terminal.{w, v} C) ⋯)
          (Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) V)))
    (CategoryStruct.comp (Y := Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ b) U)
      (if h : p₀ ∈ unop U then eqToHom ⋯ ≫ f ≫ eqToHom ⋯
      else
        IsTerminal.from
          (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
            (if p₀ ∈ unop U then b else terminal.{w, v} C) ⋯)
          (Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) U))
      (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 b else terminal.{w, v} C) ⋯)
          (if p₀ ∈ unop U then b else terminal.{w, v} C)))

Tactic:
simp only [skyscraperPresheaf_obj, hU, hV, ↓reduceDIte, eqToHom_trans_assoc, Category.assoc,
        eqToHom_trans]

Premises used: CategoryTheory.Category.assoc, skyscraperPresheaf_obj, reduceDIte, CategoryTheory.eqToHom_trans_assoc, 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 a b : C
f : a ⟶ b
U V : (Opens (↑X : Type u))ᵒᵖ
i : U ⟶ V
hV : p₀ ∉ unop V
⊢ Eq.{w + 1} (α :=
    Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) U ⟶ Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ b) V)
    (CategoryStruct.comp (Y := Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) V)
      (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 V then eqToHom ⋯ ≫ f ≫ 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 b else terminal.{w, v} C) ⋯)
          (Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) V)))
    (CategoryStruct.comp (Y := Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ b) U)
      (if h : p₀ ∈ unop U then eqToHom ⋯ ≫ f ≫ eqToHom ⋯
      else
        IsTerminal.from
          (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
            (if p₀ ∈ unop U then b else terminal.{w, v} C) ⋯)
          (Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) U))
      (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 b else terminal.{w, v} C) ⋯)
          (if p₀ ∈ unop U then b else terminal.{w, v} C)))

Tactic:
apply ((if_neg hV).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
w :
  ∀ (U : Opens (↑X : Type u)),
    Eq.{w + 1} (α :=
      Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U) ⟶
        Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U))
      (NatTrans.app (map' p₀ (𝟙 a)) (op U)) (NatTrans.app (𝟙 (skyscraperPresheaf p₀ a)) (op U))
⊢ Eq (α := Quiver.Hom (V := Presheaf.{u, w, v} C X) (skyscraperPresheaf p₀ a) (skyscraperPresheaf p₀ a)) (map' p₀ (𝟙 a))
    (𝟙 (skyscraperPresheaf p₀ a))

Tactic:
ext U
-- 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 : Opens (↑X : Type u)
w :
  Eq.{w + 1} (α :=
    Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U) ⟶
      Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U))
    (if h : p₀ ∈ U then eqToHom ⋯ ≫ 𝟙 a ≫ eqToHom ⋯
    else
      IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
          (if p₀ ∈ U then a else terminal.{w, v} C) ⋯)
        (Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U)))
    (NatTrans.app (𝟙 (skyscraperPresheaf p₀ a)) (op U))
⊢ Eq.{w + 1} (α :=
    Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U) ⟶
      Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U))
    (NatTrans.app (map' p₀ (𝟙 a)) (op U)) (NatTrans.app (𝟙 (skyscraperPresheaf p₀ a)) (op U))

Tactic:
simp only [SkyscraperPresheafFunctor.map'_app]

Premises used: SkyscraperPresheafFunctor.map'_app
-- 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 : Opens (↑X : Type u)
pos :
  ∀ (h : p₀ ∈ U),
    Eq.{w + 1} (α :=
      Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U) ⟶
        Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U))
      (eqToHom ⋯ ≫ 𝟙 a ≫ eqToHom ⋯) (NatTrans.app (𝟙 (skyscraperPresheaf p₀ a)) (op U))
neg :
  ∀ (h : p₀ ∉ U),
    IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
          (if p₀ ∈ U then a else terminal.{w, v} C) ⋯)
        (Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U)) =
      NatTrans.app (𝟙 (skyscraperPresheaf p₀ a)) (op U)
⊢ Eq.{w + 1} (α :=
    Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U) ⟶
      Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U))
    (if h : p₀ ∈ U then eqToHom ⋯ ≫ 𝟙 a ≫ eqToHom ⋯
    else
      IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
          (if p₀ ∈ U then a else terminal.{w, v} C) ⋯)
        (Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U)))
    (NatTrans.app (𝟙 (skyscraperPresheaf p₀ a)) (op U))

Tactic:
split_ifs
-- 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 b c : C
f : a ⟶ b
g : b ⟶ c
w :
  ∀ (U : Opens (↑X : Type u)),
    Eq (α :=
      Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U) ⟶
        Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ c) (op U))
      (NatTrans.app (map' p₀ (f ≫ g)) (op U)) (NatTrans.app (map' p₀ f ≫ map' p₀ g) (op U))
⊢ Eq (α := Quiver.Hom (V := Presheaf.{u, w, v} C X) (skyscraperPresheaf p₀ a) (skyscraperPresheaf p₀ c))
    (map' p₀ (f ≫ g)) (map' p₀ f ≫ map' p₀ g)

Tactic:
ext U
-- 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 b c : C
f : a ⟶ b
g : b ⟶ c
U : Opens (↑X : Type u)
w :
  Eq (α :=
    Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U) ⟶
      Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ c) (op U))
    (if h : p₀ ∈ U then eqToHom ⋯ ≫ (f ≫ g) ≫ eqToHom ⋯
    else
      IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
          (if p₀ ∈ U then c else terminal.{w, v} C) ⋯)
        (Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U)))
    (NatTrans.app (map' p₀ f ≫ map' p₀ g) (op U))
⊢ Eq (α :=
    Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U) ⟶
      Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ c) (op U))
    (NatTrans.app (map' p₀ (f ≫ g)) (op U)) (NatTrans.app (map' p₀ f ≫ map' p₀ g) (op U))

Tactic:
simp only [SkyscraperPresheafFunctor.map'_app]

Premises used: SkyscraperPresheafFunctor.map'_app
-- 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 b c : C
f : a ⟶ b
g : b ⟶ c
U : Opens (↑X : Type u)
pos :
  ∀ (h : p₀ ∈ U),
    Eq (α :=
      Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U) ⟶
        Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ c) (op U))
      (eqToHom ⋯ ≫ (f ≫ g) ≫ eqToHom ⋯) (NatTrans.app (map' p₀ f ≫ map' p₀ g) (op U))
neg :
  ∀ (h : p₀ ∉ U),
    IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
          (if p₀ ∈ U then c else terminal.{w, v} C) ⋯)
        (Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U)) =
      NatTrans.app (map' p₀ f ≫ map' p₀ g) (op U)
⊢ Eq (α :=
    Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U) ⟶
      Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ c) (op U))
    (if h : p₀ ∈ U then eqToHom ⋯ ≫ (f ≫ g) ≫ eqToHom ⋯
    else
      IsTerminal.from
        (@Eq.rec _ _ (fun (x : C) (x_1 : terminal.{w, v} C = x) ↦ IsTerminal.{w, v} x) terminalIsTerminal
          (if p₀ ∈ U then c else terminal.{w, v} C) ⋯)
        (Functor.obj.{u, w, u, v} (skyscraperPresheaf p₀ a) (op U)))
    (NatTrans.app (map' p₀ f ≫ map' p₀ g) (op U))

Tactic:
split_ifs with h
-- 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.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
y : (↑X : Type u)
h : p₀ ⤳ y
U V : (OpenNhds y)ᵒᵖ
inc : U ⟶ V
change :
  Eq (α :=
    Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) U ⟶
      Functor.obj (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ) A) V)
    (CategoryStruct.comp (Y := Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) V)
        (if h : p₀ ∈ unop ((OpenNhds.inclusion y).op.obj V) then eqToHom ⋯
        else
          IsTerminal.from (Eq.ndrec (motive := IsTerminal.{u, v}) terminalIsTerminal ⋯)
            (if p₀ ∈ unop ((OpenNhds.inclusion y).op.obj U) then A else terminal.{u, v} C))
        (eqToHom ⋯) :
      Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) U ⟶
        Functor.obj (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ) A) V)
    (eqToHom ⋯ ≫ CategoryTheory.Functor.map (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ) A) inc :
      Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) U ⟶
        Functor.obj (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ) A) V)
⊢ Eq (α :=
    Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) U ⟶
      Functor.obj (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ) A) V)
    (CategoryTheory.Functor.map ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) inc ≫ eqToHom ⋯)
    (eqToHom ⋯ ≫ CategoryTheory.Functor.map (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ) A) inc)

Tactic:
change dite _ _ _ ≫ _ = _

Premises used: dite
-- 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.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
y : (↑X : Type u)
h : p₀ ⤳ y
U V : (OpenNhds y)ᵒᵖ
inc : U ⟶ V
rw :
  Eq.{u + 1} (α :=
    Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) U ⟶
      Functor.obj (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ) A) V)
    (eqToHom ⋯ ≫ eqToHom ⋯) (eqToHom ⋯ ≫ CategoryTheory.Functor.map (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ) A) inc)
hc : p₀ ∈ unop ((OpenNhds.inclusion y).op.obj V)
⊢ Eq (α :=
    Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) U ⟶
      Functor.obj (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ) A) V)
    (CategoryStruct.comp (Y := Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) V)
        (if h : p₀ ∈ unop ((OpenNhds.inclusion y).op.obj V) then eqToHom ⋯
        else
          IsTerminal.from (Eq.ndrec (motive := IsTerminal.{u, v}) terminalIsTerminal ⋯)
            (if p₀ ∈ unop ((OpenNhds.inclusion y).op.obj U) then A else terminal.{u, v} C))
        (eqToHom ⋯) :
      Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) U ⟶
        Functor.obj (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ) A) V)
    (eqToHom ⋯ ≫ CategoryTheory.Functor.map (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ) A) inc :
      Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) U ⟶
        Functor.obj (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ) A) V)

Tactic:
rw [dif_pos]

Premises used: dif_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.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
y : (↑X : Type u)
h : p₀ ⤳ y
U V : (OpenNhds y)ᵒᵖ
inc : U ⟶ V
⊢ p₀ ∈ unop ((OpenNhds.inclusion y).op.obj V)

Tactic:
h.mem_open V.unop.1.2 V.unop.2

Premises used: Specializes.mem_open, TopologicalSpace.Opens.is_open', Subtype.val, Opposite.unop, Subtype.property
-- 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.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
y : (↑X : Type u)
h : p₀ ⤳ y
U V : (OpenNhds y)ᵒᵖ
inc : U ⟶ V
⊢ p₀ ∈ unop ((OpenNhds.inclusion y).op.obj V)

Tactic:
exact h.mem_open V.unop.1.2 V.unop.2

Premises used: Specializes.mem_open, TopologicalSpace.Opens.is_open', Subtype.val, Opposite.unop, Subtype.property
-- 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.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
y : (↑X : Type u)
h : p₀ ⤳ y
U V : (OpenNhds y)ᵒᵖ
inc : U ⟶ V
⊢ Eq.{u + 1} (α :=
    Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) U ⟶
      Functor.obj (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ) A) V)
    (eqToHom ⋯ ≫ eqToHom ⋯) (eqToHom ⋯ ≫ CategoryTheory.Functor.map (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ) A) inc)

Tactic:
simp only [Functor.comp_obj, Functor.op_obj, skyscraperPresheaf_obj, unop_op,
            Functor.const_obj_obj, eqToHom_trans, Functor.const_obj_map, Category.comp_id]

Premises used: CategoryTheory.Functor.comp_obj, skyscraperPresheaf_obj, CategoryTheory.Category.comp_id, Opposite.unop_op, CategoryTheory.Functor.const_obj_obj, CategoryTheory.Functor.const_obj_map, CategoryTheory.Functor.op_obj, 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.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
y : (↑X : Type u)
h : p₀ ⤳ y
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
dsimp :
  eqToHom ⋯ ≫ CategoryStruct.comp (Y := if True then A else terminal.{u, v} C) (eqToHom ⋯) (c.ι.app (op ⊤)) = c.ι.app U
⊢ CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.obj (Functor.const (OpenNhds y)ᵒᵖ)
          (Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
            (skyscraperPresheafCoconeOfSpecializes p₀ A h)))
        U)
      (NatTrans.app (Cocone.ι (skyscraperPresheafCoconeOfSpecializes p₀ A h)) U)
      (CategoryStruct.comp (Y :=
        if True then
          Cocone.pt (F := (OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
            (skyscraperPresheafCoconeOfSpecializes p₀ A h)
        else terminal.{u, v} C)
        (eqToHom ⋯) (c.ι.app (op ⊤))) =
    c.ι.app U

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.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
y : (↑X : Type u)
h : p₀ ⤳ y
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
rw :
  eqToHom ⋯ ≫
      eqToHom ⋯ ≫
        CategoryStruct.comp (Y := Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (op (unop U)))
          (CategoryTheory.Functor.map ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (Quiver.Hom.op (homOfLE ⋯)))
          (c.ι.app (op (unop U))) =
    c.ι.app U
⊢ eqToHom ⋯ ≫ CategoryStruct.comp (Y := if True then A else terminal.{u, v} C) (eqToHom ⋯) (c.ι.app (op ⊤)) = c.ι.app U

Tactic:
rw [← c.w (homOfLE <| (le_top : unop U ≤ _)).op]

Premises used: Quiver.Hom.op, CategoryTheory.Limits.Cocone.w, le_top, CategoryTheory.homOfLE
-- 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.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
y : (↑X : Type u)
h : p₀ ⤳ y
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
change :
  eqToHom ⋯ ≫
      CategoryStruct.comp (Y := if True then A else terminal.{u, v} C) (eqToHom ⋯)
        (CategoryStruct.comp (Y := Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (op (unop U)))
          (if h : p₀ ∈ unop ((OpenNhds.inclusion y).op.obj (op (unop U))) then eqToHom ⋯
          else
            IsTerminal.from (Eq.ndrec (motive := IsTerminal.{u, v}) terminalIsTerminal ⋯)
              (if p₀ ∈ unop ((OpenNhds.inclusion y).op.obj (op ⊤)) then A else terminal.{u, v} C))
          (c.ι.app (op (unop U)))) =
    c.ι.app U
⊢ eqToHom ⋯ ≫
      eqToHom ⋯ ≫
        CategoryStruct.comp (Y := Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (op (unop U)))
          (CategoryTheory.Functor.map ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (Quiver.Hom.op (homOfLE ⋯)))
          (c.ι.app (op (unop U))) =
    c.ι.app U

Tactic:
change _ ≫ _ ≫ dite _ _ _ ≫ _ = _

Premises used: dite
-- 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.{u, v} C
A : C
inst_2 : HasTerminal.{u, v} C
y : (↑X : Type u)
h : p₀ ⤳ y
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
rw : eqToHom ⋯ ≫ eqToHom ⋯ ≫ eqToHom ⋯ ≫ c.ι.app (op (unop U)) = c.ι.app U
hc : p₀ ∈ unop ((OpenNhds.inclusion y).op.obj (op (unop U)))
⊢ eqToHom ⋯ ≫
      CategoryStruct.comp (Y := if True then A else terminal.{u, v} C) (eqToHom ⋯)
        (CategoryStruct.comp (Y := Functor.obj ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A) (op (unop U)))
          (if h : p₀ ∈ unop ((OpenNhds.inclusion y).op.obj (op (unop U))) then eqToHom ⋯
          else
            IsTerminal.from (Eq.ndrec (motive := IsTerminal.{u, v}) terminalIsTerminal ⋯)
              (if p₀ ∈ unop ((OpenNhds.inclusion y).op.obj (op ⊤)) then A else terminal.{u, v} C))
          (c.ι.app (op (unop U)))) =
    c.ι.app U

Tactic:
rw [dif_pos]

Premises used: dif_pos