[GOAL]
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A : C
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
h : p₀ ∈ V.unop
⊢ (fun U => if p₀ ∈ U.unop then A else ⊤_ C) U = (fun U => if p₀ ∈ U.unop then A else ⊤_ C) V
[PROOFSTEP]
dsimp
[GOAL]
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A : C
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
h : p₀ ∈ V.unop
⊢ (if p₀ ∈ U.unop then A else ⊤_ C) = if p₀ ∈ V.unop then A else ⊤_ C
[PROOFSTEP]
erw [if_pos h, if_pos (leOfHom i.unop h)]
[GOAL]
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A : C
U V W : (Opens ↑X)ᵒᵖ
iVU : U ⟶ V
iWV : V ⟶ W
⊢ { obj := fun U => if p₀ ∈ U.unop then A else ⊤_ C,
          map := fun {U V} i =>
            if h : p₀ ∈ V.unop then
              eqToHom (_ : (fun U => if p₀ ∈ U.unop then A else ⊤_ C) U = (fun U => if p₀ ∈ U.unop then A else ⊤_ C) V)
            else
              IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then A else ⊤_ C) ▸ terminalIsTerminal)
                ((fun U => if p₀ ∈ U.unop then A else ⊤_ C) U) }.map
      (iVU ≫ iWV) =
    { obj := fun U => if p₀ ∈ U.unop then A else ⊤_ C,
            map := fun {U V} i =>
              if h : p₀ ∈ V.unop then
                eqToHom
                  (_ : (fun U => if p₀ ∈ U.unop then A else ⊤_ C) U = (fun U => if p₀ ∈ U.unop then A else ⊤_ C) V)
              else
                IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then A else ⊤_ C) ▸ terminalIsTerminal)
                  ((fun U => if p₀ ∈ U.unop then A else ⊤_ C) U) }.map
        iVU ≫
      { obj := fun U => if p₀ ∈ U.unop then A else ⊤_ C,
            map := fun {U V} i =>
              if h : p₀ ∈ V.unop then
                eqToHom
                  (_ : (fun U => if p₀ ∈ U.unop then A else ⊤_ C) U = (fun U => if p₀ ∈ U.unop then A else ⊤_ C) V)
              else
                IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then A else ⊤_ C) ▸ terminalIsTerminal)
                  ((fun U => if p₀ ∈ U.unop then A else ⊤_ C) U) }.map
        iWV
[PROOFSTEP]
by_cases hW : p₀ ∈ unop W
[GOAL]
case pos
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A : C
U V W : (Opens ↑X)ᵒᵖ
iVU : U ⟶ V
iWV : V ⟶ W
hW : p₀ ∈ W.unop
⊢ { obj := fun U => if p₀ ∈ U.unop then A else ⊤_ C,
          map := fun {U V} i =>
            if h : p₀ ∈ V.unop then
              eqToHom (_ : (fun U => if p₀ ∈ U.unop then A else ⊤_ C) U = (fun U => if p₀ ∈ U.unop then A else ⊤_ C) V)
            else
              IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then A else ⊤_ C) ▸ terminalIsTerminal)
                ((fun U => if p₀ ∈ U.unop then A else ⊤_ C) U) }.map
      (iVU ≫ iWV) =
    { obj := fun U => if p₀ ∈ U.unop then A else ⊤_ C,
            map := fun {U V} i =>
              if h : p₀ ∈ V.unop then
                eqToHom
                  (_ : (fun U => if p₀ ∈ U.unop then A else ⊤_ C) U = (fun U => if p₀ ∈ U.unop then A else ⊤_ C) V)
              else
                IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then A else ⊤_ C) ▸ terminalIsTerminal)
                  ((fun U => if p₀ ∈ U.unop then A else ⊤_ C) U) }.map
        iVU ≫
      { obj := fun U => if p₀ ∈ U.unop then A else ⊤_ C,
            map := fun {U V} i =>
              if h : p₀ ∈ V.unop then
                eqToHom
                  (_ : (fun U => if p₀ ∈ U.unop then A else ⊤_ C) U = (fun U => if p₀ ∈ U.unop then A else ⊤_ C) V)
              else
                IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then A else ⊤_ C) ▸ terminalIsTerminal)
                  ((fun U => if p₀ ∈ U.unop then A else ⊤_ C) U) }.map
        iWV
[PROOFSTEP]
have hV : p₀ ∈ unop V := leOfHom iWV.unop hW
[GOAL]
case pos
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A : C
U V W : (Opens ↑X)ᵒᵖ
iVU : U ⟶ V
iWV : V ⟶ W
hW : p₀ ∈ W.unop
hV : p₀ ∈ V.unop
⊢ { obj := fun U => if p₀ ∈ U.unop then A else ⊤_ C,
          map := fun {U V} i =>
            if h : p₀ ∈ V.unop then
              eqToHom (_ : (fun U => if p₀ ∈ U.unop then A else ⊤_ C) U = (fun U => if p₀ ∈ U.unop then A else ⊤_ C) V)
            else
              IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then A else ⊤_ C) ▸ terminalIsTerminal)
                ((fun U => if p₀ ∈ U.unop then A else ⊤_ C) U) }.map
      (iVU ≫ iWV) =
    { obj := fun U => if p₀ ∈ U.unop then A else ⊤_ C,
            map := fun {U V} i =>
              if h : p₀ ∈ V.unop then
                eqToHom
                  (_ : (fun U => if p₀ ∈ U.unop then A else ⊤_ C) U = (fun U => if p₀ ∈ U.unop then A else ⊤_ C) V)
              else
                IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then A else ⊤_ C) ▸ terminalIsTerminal)
                  ((fun U => if p₀ ∈ U.unop then A else ⊤_ C) U) }.map
        iVU ≫
      { obj := fun U => if p₀ ∈ U.unop then A else ⊤_ C,
            map := fun {U V} i =>
              if h : p₀ ∈ V.unop then
                eqToHom
                  (_ : (fun U => if p₀ ∈ U.unop then A else ⊤_ C) U = (fun U => if p₀ ∈ U.unop then A else ⊤_ C) V)
              else
                IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then A else ⊤_ C) ▸ terminalIsTerminal)
                  ((fun U => if p₀ ∈ U.unop then A else ⊤_ C) U) }.map
        iWV
[PROOFSTEP]
simp only [dif_pos hW, dif_pos hV, eqToHom_trans]
[GOAL]
case neg
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A : C
U V W : (Opens ↑X)ᵒᵖ
iVU : U ⟶ V
iWV : V ⟶ W
hW : ¬p₀ ∈ W.unop
⊢ { obj := fun U => if p₀ ∈ U.unop then A else ⊤_ C,
          map := fun {U V} i =>
            if h : p₀ ∈ V.unop then
              eqToHom (_ : (fun U => if p₀ ∈ U.unop then A else ⊤_ C) U = (fun U => if p₀ ∈ U.unop then A else ⊤_ C) V)
            else
              IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then A else ⊤_ C) ▸ terminalIsTerminal)
                ((fun U => if p₀ ∈ U.unop then A else ⊤_ C) U) }.map
      (iVU ≫ iWV) =
    { obj := fun U => if p₀ ∈ U.unop then A else ⊤_ C,
            map := fun {U V} i =>
              if h : p₀ ∈ V.unop then
                eqToHom
                  (_ : (fun U => if p₀ ∈ U.unop then A else ⊤_ C) U = (fun U => if p₀ ∈ U.unop then A else ⊤_ C) V)
              else
                IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then A else ⊤_ C) ▸ terminalIsTerminal)
                  ((fun U => if p₀ ∈ U.unop then A else ⊤_ C) U) }.map
        iVU ≫
      { obj := fun U => if p₀ ∈ U.unop then A else ⊤_ C,
            map := fun {U V} i =>
              if h : p₀ ∈ V.unop then
                eqToHom
                  (_ : (fun U => if p₀ ∈ U.unop then A else ⊤_ C) U = (fun U => if p₀ ∈ U.unop then A else ⊤_ C) V)
              else
                IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then A else ⊤_ C) ▸ terminalIsTerminal)
                  ((fun U => if p₀ ∈ U.unop then A else ⊤_ C) U) }.map
        iWV
[PROOFSTEP]
dsimp
[GOAL]
case neg
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A : C
U V W : (Opens ↑X)ᵒᵖ
iVU : U ⟶ V
iWV : V ⟶ W
hW : ¬p₀ ∈ W.unop
⊢ (if h : p₀ ∈ W.unop then eqToHom (_ : (if p₀ ∈ U.unop then A else ⊤_ C) = if p₀ ∈ W.unop then A else ⊤_ C)
    else
      IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ W.unop then A else ⊤_ C) ▸ terminalIsTerminal)
        (if p₀ ∈ U.unop then A else ⊤_ C)) =
    (if h : p₀ ∈ V.unop then eqToHom (_ : (if p₀ ∈ U.unop then A else ⊤_ C) = if p₀ ∈ V.unop then A else ⊤_ C)
      else
        IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then A else ⊤_ C) ▸ terminalIsTerminal)
          (if p₀ ∈ U.unop then A else ⊤_ C)) ≫
      if h : p₀ ∈ W.unop then eqToHom (_ : (if p₀ ∈ V.unop then A else ⊤_ C) = if p₀ ∈ W.unop then A else ⊤_ C)
      else
        IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ W.unop then A else ⊤_ C) ▸ terminalIsTerminal)
          (if p₀ ∈ V.unop then A else ⊤_ C)
[PROOFSTEP]
rw [dif_neg hW]
[GOAL]
case neg
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A : C
U V W : (Opens ↑X)ᵒᵖ
iVU : U ⟶ V
iWV : V ⟶ W
hW : ¬p₀ ∈ W.unop
⊢ IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ W.unop then A else ⊤_ C) ▸ terminalIsTerminal)
      (if p₀ ∈ U.unop then A else ⊤_ C) =
    (if h : p₀ ∈ V.unop then eqToHom (_ : (if p₀ ∈ U.unop then A else ⊤_ C) = if p₀ ∈ V.unop then A else ⊤_ C)
      else
        IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then A else ⊤_ C) ▸ terminalIsTerminal)
          (if p₀ ∈ U.unop then A else ⊤_ C)) ≫
      if h : p₀ ∈ W.unop then eqToHom (_ : (if p₀ ∈ V.unop then A else ⊤_ C) = if p₀ ∈ W.unop then A else ⊤_ C)
      else
        IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ W.unop then A else ⊤_ C) ▸ terminalIsTerminal)
          (if p₀ ∈ V.unop then A else ⊤_ C)
[PROOFSTEP]
apply ((if_neg hW).symm.ndrec terminalIsTerminal).hom_ext
[GOAL]
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A : C
hd : (U : Opens ↑(of PUnit)) → Decidable (PUnit.unit ∈ U)
⊢ skyscraperPresheaf p₀ A = ContinuousMap.const (↑(of PUnit)) p₀ _* skyscraperPresheaf PUnit.unit A
[PROOFSTEP]
convert_to @skyscraperPresheaf X p₀ (fun U => hd <| (Opens.map <| ContinuousMap.const _ p₀).obj U) C _ _ A = _
[GOAL]
case h.e'_2
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A : C
hd : (U : Opens ↑(of PUnit)) → Decidable (PUnit.unit ∈ U)
⊢ skyscraperPresheaf p₀ A = skyscraperPresheaf p₀ A
[PROOFSTEP]
congr
[GOAL]
case convert_2
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A : C
hd : (U : Opens ↑(of PUnit)) → Decidable (PUnit.unit ∈ U)
⊢ skyscraperPresheaf p₀ A = ContinuousMap.const (↑(of PUnit)) p₀ _* skyscraperPresheaf PUnit.unit A
[PROOFSTEP]
congr
[GOAL]
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A a b : C
f : a ⟶ b
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
⊢ (skyscraperPresheaf p₀ a).map i ≫
      (fun U =>
          if h : p₀ ∈ U.unop then
            eqToHom (_ : (if p₀ ∈ U.unop then a else ⊤_ C) = a) ≫ f ≫ eqToHom (_ : b = if p₀ ∈ U.unop then b else ⊤_ C)
          else
            IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ U.unop then b else ⊤_ C) ▸ terminalIsTerminal)
              ((skyscraperPresheaf p₀ a).obj U))
        V =
    (fun U =>
          if h : p₀ ∈ U.unop then
            eqToHom (_ : (if p₀ ∈ U.unop then a else ⊤_ C) = a) ≫ f ≫ eqToHom (_ : b = if p₀ ∈ U.unop then b else ⊤_ C)
          else
            IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ U.unop then b else ⊤_ C) ▸ terminalIsTerminal)
              ((skyscraperPresheaf p₀ a).obj U))
        U ≫
      (skyscraperPresheaf p₀ b).map i
[PROOFSTEP]
simp only [skyscraperPresheaf_map]
[GOAL]
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A a b : C
f : a ⟶ b
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
⊢ ((if h : p₀ ∈ V.unop then
        eqToHom (_ : (fun U => if p₀ ∈ U.unop then a else ⊤_ C) U = (fun U => if p₀ ∈ U.unop then a else ⊤_ C) V)
      else
        IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then a else ⊤_ C) ▸ terminalIsTerminal)
          (if p₀ ∈ U.unop then a else ⊤_ C)) ≫
      if h : p₀ ∈ V.unop then
        eqToHom (_ : (if p₀ ∈ V.unop then a else ⊤_ C) = a) ≫ f ≫ eqToHom (_ : b = if p₀ ∈ V.unop then b else ⊤_ C)
      else
        IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then b else ⊤_ C) ▸ terminalIsTerminal)
          ((skyscraperPresheaf p₀ a).obj V)) =
    (if h : p₀ ∈ U.unop then
        eqToHom (_ : (if p₀ ∈ U.unop then a else ⊤_ C) = a) ≫ f ≫ eqToHom (_ : b = if p₀ ∈ U.unop then b else ⊤_ C)
      else
        IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ U.unop then b else ⊤_ C) ▸ terminalIsTerminal)
          ((skyscraperPresheaf p₀ a).obj U)) ≫
      if h : p₀ ∈ V.unop then
        eqToHom (_ : (fun U => if p₀ ∈ U.unop then b else ⊤_ C) U = (fun U => if p₀ ∈ U.unop then b else ⊤_ C) V)
      else
        IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then b else ⊤_ C) ▸ terminalIsTerminal)
          (if p₀ ∈ U.unop then b else ⊤_ C)
[PROOFSTEP]
by_cases hV : p₀ ∈ V.unop
[GOAL]
case pos
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A a b : C
f : a ⟶ b
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
hV : p₀ ∈ V.unop
⊢ ((if h : p₀ ∈ V.unop then
        eqToHom (_ : (fun U => if p₀ ∈ U.unop then a else ⊤_ C) U = (fun U => if p₀ ∈ U.unop then a else ⊤_ C) V)
      else
        IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then a else ⊤_ C) ▸ terminalIsTerminal)
          (if p₀ ∈ U.unop then a else ⊤_ C)) ≫
      if h : p₀ ∈ V.unop then
        eqToHom (_ : (if p₀ ∈ V.unop then a else ⊤_ C) = a) ≫ f ≫ eqToHom (_ : b = if p₀ ∈ V.unop then b else ⊤_ C)
      else
        IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then b else ⊤_ C) ▸ terminalIsTerminal)
          ((skyscraperPresheaf p₀ a).obj V)) =
    (if h : p₀ ∈ U.unop then
        eqToHom (_ : (if p₀ ∈ U.unop then a else ⊤_ C) = a) ≫ f ≫ eqToHom (_ : b = if p₀ ∈ U.unop then b else ⊤_ C)
      else
        IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ U.unop then b else ⊤_ C) ▸ terminalIsTerminal)
          ((skyscraperPresheaf p₀ a).obj U)) ≫
      if h : p₀ ∈ V.unop then
        eqToHom (_ : (fun U => if p₀ ∈ U.unop then b else ⊤_ C) U = (fun U => if p₀ ∈ U.unop then b else ⊤_ C) V)
      else
        IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then b else ⊤_ C) ▸ terminalIsTerminal)
          (if p₀ ∈ U.unop then b else ⊤_ C)
[PROOFSTEP]
have hU : p₀ ∈ U.unop := leOfHom i.unop hV
[GOAL]
case pos
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A a b : C
f : a ⟶ b
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
hV : p₀ ∈ V.unop
hU : p₀ ∈ U.unop
⊢ ((if h : p₀ ∈ V.unop then
        eqToHom (_ : (fun U => if p₀ ∈ U.unop then a else ⊤_ C) U = (fun U => if p₀ ∈ U.unop then a else ⊤_ C) V)
      else
        IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then a else ⊤_ C) ▸ terminalIsTerminal)
          (if p₀ ∈ U.unop then a else ⊤_ C)) ≫
      if h : p₀ ∈ V.unop then
        eqToHom (_ : (if p₀ ∈ V.unop then a else ⊤_ C) = a) ≫ f ≫ eqToHom (_ : b = if p₀ ∈ V.unop then b else ⊤_ C)
      else
        IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then b else ⊤_ C) ▸ terminalIsTerminal)
          ((skyscraperPresheaf p₀ a).obj V)) =
    (if h : p₀ ∈ U.unop then
        eqToHom (_ : (if p₀ ∈ U.unop then a else ⊤_ C) = a) ≫ f ≫ eqToHom (_ : b = if p₀ ∈ U.unop then b else ⊤_ C)
      else
        IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ U.unop then b else ⊤_ C) ▸ terminalIsTerminal)
          ((skyscraperPresheaf p₀ a).obj U)) ≫
      if h : p₀ ∈ V.unop then
        eqToHom (_ : (fun U => if p₀ ∈ U.unop then b else ⊤_ C) U = (fun U => if p₀ ∈ U.unop then b else ⊤_ C) V)
      else
        IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then b else ⊤_ C) ▸ terminalIsTerminal)
          (if p₀ ∈ U.unop then b else ⊤_ C)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A a b : C
f : a ⟶ b
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
hV : p₀ ∈ V.unop
hU : p₀ ∈ U.unop
h✝ : p₀ ∈ V.unop
⊢ eqToHom (_ : (fun U => if p₀ ∈ U.unop then a else ⊤_ C) U = (fun U => if p₀ ∈ U.unop then a else ⊤_ C) V) ≫
      eqToHom (_ : (if p₀ ∈ V.unop then a else ⊤_ C) = a) ≫ f ≫ eqToHom (_ : b = if p₀ ∈ V.unop then b else ⊤_ C) =
    (eqToHom (_ : (if p₀ ∈ U.unop then a else ⊤_ C) = a) ≫ f ≫ eqToHom (_ : b = if p₀ ∈ U.unop then b else ⊤_ C)) ≫
      eqToHom (_ : (fun U => if p₀ ∈ U.unop then b else ⊤_ C) U = (fun U => if p₀ ∈ U.unop then b else ⊤_ C) V)
[PROOFSTEP]
simp only [eqToHom_trans_assoc, Category.assoc, eqToHom_trans]
[GOAL]
case neg
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A a b : C
f : a ⟶ b
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
hV : p₀ ∈ V.unop
hU : p₀ ∈ U.unop
h✝ : ¬p₀ ∈ V.unop
⊢ eqToHom (_ : (fun U => if p₀ ∈ U.unop then a else ⊤_ C) U = (fun U => if p₀ ∈ U.unop then a else ⊤_ C) V) ≫
      eqToHom (_ : (if p₀ ∈ V.unop then a else ⊤_ C) = a) ≫ f ≫ eqToHom (_ : b = if p₀ ∈ V.unop then b else ⊤_ C) =
    (eqToHom (_ : (if p₀ ∈ U.unop then a else ⊤_ C) = a) ≫ f ≫ eqToHom (_ : b = if p₀ ∈ U.unop then b else ⊤_ C)) ≫
      eqToHom (_ : (fun U => if p₀ ∈ U.unop then b else ⊤_ C) U = (fun U => if p₀ ∈ U.unop then b else ⊤_ C) V)
[PROOFSTEP]
simp only [eqToHom_trans_assoc, Category.assoc, eqToHom_trans]
[GOAL]
case neg
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A a b : C
f : a ⟶ b
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
hV : ¬p₀ ∈ V.unop
⊢ ((if h : p₀ ∈ V.unop then
        eqToHom (_ : (fun U => if p₀ ∈ U.unop then a else ⊤_ C) U = (fun U => if p₀ ∈ U.unop then a else ⊤_ C) V)
      else
        IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then a else ⊤_ C) ▸ terminalIsTerminal)
          (if p₀ ∈ U.unop then a else ⊤_ C)) ≫
      if h : p₀ ∈ V.unop then
        eqToHom (_ : (if p₀ ∈ V.unop then a else ⊤_ C) = a) ≫ f ≫ eqToHom (_ : b = if p₀ ∈ V.unop then b else ⊤_ C)
      else
        IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then b else ⊤_ C) ▸ terminalIsTerminal)
          ((skyscraperPresheaf p₀ a).obj V)) =
    (if h : p₀ ∈ U.unop then
        eqToHom (_ : (if p₀ ∈ U.unop then a else ⊤_ C) = a) ≫ f ≫ eqToHom (_ : b = if p₀ ∈ U.unop then b else ⊤_ C)
      else
        IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ U.unop then b else ⊤_ C) ▸ terminalIsTerminal)
          ((skyscraperPresheaf p₀ a).obj U)) ≫
      if h : p₀ ∈ V.unop then
        eqToHom (_ : (fun U => if p₀ ∈ U.unop then b else ⊤_ C) U = (fun U => if p₀ ∈ U.unop then b else ⊤_ C) V)
      else
        IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then b else ⊤_ C) ▸ terminalIsTerminal)
          (if p₀ ∈ U.unop then b else ⊤_ C)
[PROOFSTEP]
apply ((if_neg hV).symm.ndrec terminalIsTerminal).hom_ext
[GOAL]
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A a : C
⊢ map' p₀ (𝟙 a) = 𝟙 (skyscraperPresheaf p₀ a)
[PROOFSTEP]
refine NatTrans.ext _ _ <| funext fun U => ?_
[GOAL]
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A a : C
U : (Opens ↑X)ᵒᵖ
⊢ NatTrans.app (map' p₀ (𝟙 a)) U = NatTrans.app (𝟙 (skyscraperPresheaf p₀ a)) U
[PROOFSTEP]
simp only [SkyscraperPresheafFunctor.map'_app, NatTrans.id_app]
[GOAL]
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A a : C
U : (Opens ↑X)ᵒᵖ
⊢ (if h : p₀ ∈ U.unop then
      eqToHom (_ : (if p₀ ∈ U.unop then a else ⊤_ C) = a) ≫ 𝟙 a ≫ eqToHom (_ : a = if p₀ ∈ U.unop then a else ⊤_ C)
    else
      IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ U.unop then a else ⊤_ C) ▸ terminalIsTerminal)
        ((skyscraperPresheaf p₀ a).obj U)) =
    NatTrans.app (𝟙 (skyscraperPresheaf p₀ a)) U
[PROOFSTEP]
split_ifs
[GOAL]
case pos
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A a : C
U : (Opens ↑X)ᵒᵖ
h✝ : p₀ ∈ U.unop
⊢ eqToHom (_ : (if p₀ ∈ U.unop then a else ⊤_ C) = a) ≫ 𝟙 a ≫ eqToHom (_ : a = if p₀ ∈ U.unop then a else ⊤_ C) =
    NatTrans.app (𝟙 (skyscraperPresheaf p₀ a)) U
[PROOFSTEP]
aesop_cat
[GOAL]
case neg
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A a : C
U : (Opens ↑X)ᵒᵖ
h✝ : ¬p₀ ∈ U.unop
⊢ IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ U.unop then a else ⊤_ C) ▸ terminalIsTerminal)
      ((skyscraperPresheaf p₀ a).obj U) =
    NatTrans.app (𝟙 (skyscraperPresheaf p₀ a)) U
[PROOFSTEP]
aesop_cat
[GOAL]
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A a b c : C
f : a ⟶ b
g : b ⟶ c
⊢ map' p₀ (f ≫ g) = map' p₀ f ≫ map' p₀ g
[PROOFSTEP]
refine
  NatTrans.ext _ _ <|
    funext fun U =>
      ?_
        -- Porting note : change `simp` to `rw`
[GOAL]
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A a b c : C
f : a ⟶ b
g : b ⟶ c
U : (Opens ↑X)ᵒᵖ
⊢ NatTrans.app (map' p₀ (f ≫ g)) U = NatTrans.app (map' p₀ f ≫ map' p₀ g) U
[PROOFSTEP]
rw [NatTrans.comp_app]
[GOAL]
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A a b c : C
f : a ⟶ b
g : b ⟶ c
U : (Opens ↑X)ᵒᵖ
⊢ NatTrans.app (map' p₀ (f ≫ g)) U = NatTrans.app (map' p₀ f) U ≫ NatTrans.app (map' p₀ g) U
[PROOFSTEP]
simp only [SkyscraperPresheafFunctor.map'_app]
[GOAL]
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A a b c : C
f : a ⟶ b
g : b ⟶ c
U : (Opens ↑X)ᵒᵖ
⊢ (if h : p₀ ∈ U.unop then
      eqToHom (_ : (if p₀ ∈ U.unop then a else ⊤_ C) = a) ≫ (f ≫ g) ≫ eqToHom (_ : c = if p₀ ∈ U.unop then c else ⊤_ C)
    else
      IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ U.unop then c else ⊤_ C) ▸ terminalIsTerminal)
        ((skyscraperPresheaf p₀ a).obj U)) =
    (if h : p₀ ∈ U.unop then
        eqToHom (_ : (if p₀ ∈ U.unop then a else ⊤_ C) = a) ≫ f ≫ eqToHom (_ : b = if p₀ ∈ U.unop then b else ⊤_ C)
      else
        IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ U.unop then b else ⊤_ C) ▸ terminalIsTerminal)
          ((skyscraperPresheaf p₀ a).obj U)) ≫
      if h : p₀ ∈ U.unop then
        eqToHom (_ : (if p₀ ∈ U.unop then b else ⊤_ C) = b) ≫ g ≫ eqToHom (_ : c = if p₀ ∈ U.unop then c else ⊤_ C)
      else
        IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ U.unop then c else ⊤_ C) ▸ terminalIsTerminal)
          ((skyscraperPresheaf p₀ b).obj U)
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A a b c : C
f : a ⟶ b
g : b ⟶ c
U : (Opens ↑X)ᵒᵖ
h : p₀ ∈ U.unop
⊢ eqToHom (_ : (if p₀ ∈ U.unop then a else ⊤_ C) = a) ≫ (f ≫ g) ≫ eqToHom (_ : c = if p₀ ∈ U.unop then c else ⊤_ C) =
    (eqToHom (_ : (if p₀ ∈ U.unop then a else ⊤_ C) = a) ≫ f ≫ eqToHom (_ : b = if p₀ ∈ U.unop then b else ⊤_ C)) ≫
      eqToHom (_ : (if p₀ ∈ U.unop then b else ⊤_ C) = b) ≫ g ≫ eqToHom (_ : c = if p₀ ∈ U.unop then c else ⊤_ C)
[PROOFSTEP]
aesop_cat
[GOAL]
case neg
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A a b c : C
f : a ⟶ b
g : b ⟶ c
U : (Opens ↑X)ᵒᵖ
h : ¬p₀ ∈ U.unop
⊢ IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ U.unop then c else ⊤_ C) ▸ terminalIsTerminal)
      ((skyscraperPresheaf p₀ a).obj U) =
    IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ U.unop then b else ⊤_ C) ▸ terminalIsTerminal)
        ((skyscraperPresheaf p₀ a).obj U) ≫
      IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ U.unop then c else ⊤_ C) ▸ terminalIsTerminal)
        ((skyscraperPresheaf p₀ b).obj U)
[PROOFSTEP]
aesop_cat
[GOAL]
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : p₀ ⤳ y
U V : (OpenNhds y)ᵒᵖ
inc : U ⟶ V
⊢ ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A).map inc ≫
      (fun U => eqToHom (_ : (if p₀ ∈ U.unop.obj.carrier then A else ⊤_ C) = A)) V =
    (fun U => eqToHom (_ : (if p₀ ∈ U.unop.obj.carrier then A else ⊤_ C) = A)) U ≫
      ((Functor.const (OpenNhds y)ᵒᵖ).obj A).map inc
[PROOFSTEP]
change dite _ _ _ ≫ _ = _
[GOAL]
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : p₀ ⤳ y
U V : (OpenNhds y)ᵒᵖ
inc : U ⟶ V
⊢ (if h : p₀ ∈ ((OpenNhds.inclusion y).op.obj V).unop then
        (fun h =>
            eqToHom
              (_ :
                (fun U => if p₀ ∈ U.unop then A else ⊤_ C) ((OpenNhds.inclusion y).op.obj U) =
                  (fun U => if p₀ ∈ U.unop then A else ⊤_ C) ((OpenNhds.inclusion y).op.obj V)))
          h
      else
        (fun h =>
            IsTerminal.from
              ((_ : (⊤_ C) = if p₀ ∈ ((OpenNhds.inclusion y).op.obj V).unop then A else ⊤_ C) ▸ terminalIsTerminal)
              ((fun U => if p₀ ∈ U.unop then A else ⊤_ C) ((OpenNhds.inclusion y).op.obj U)))
          h) ≫
      (fun U => eqToHom (_ : (if p₀ ∈ U.unop.obj.carrier then A else ⊤_ C) = A)) V =
    (fun U => eqToHom (_ : (if p₀ ∈ U.unop.obj.carrier then A else ⊤_ C) = A)) U ≫
      ((Functor.const (OpenNhds y)ᵒᵖ).obj A).map inc
[PROOFSTEP]
rw [dif_pos]
[GOAL]
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : p₀ ⤳ y
U V : (OpenNhds y)ᵒᵖ
inc : U ⟶ V
⊢ (fun h =>
          eqToHom
            (_ :
              (fun U => if p₀ ∈ U.unop then A else ⊤_ C) ((OpenNhds.inclusion y).op.obj U) =
                (fun U => if p₀ ∈ U.unop then A else ⊤_ C) ((OpenNhds.inclusion y).op.obj V)))
        ?hc ≫
      (fun U => eqToHom (_ : (if p₀ ∈ U.unop.obj.carrier then A else ⊤_ C) = A)) V =
    (fun U => eqToHom (_ : (if p₀ ∈ U.unop.obj.carrier then A else ⊤_ C) = A)) U ≫
      ((Functor.const (OpenNhds y)ᵒᵖ).obj A).map inc
case hc
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : p₀ ⤳ y
U V : (OpenNhds y)ᵒᵖ
inc : U ⟶ V
⊢ p₀ ∈ ((OpenNhds.inclusion y).op.obj V).unop
[PROOFSTEP]
swap
  -- Porting note : swap goal to prevent proving same thing twice
[GOAL]
case hc
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : p₀ ⤳ y
U V : (OpenNhds y)ᵒᵖ
inc : U ⟶ V
⊢ p₀ ∈ ((OpenNhds.inclusion y).op.obj V).unop
[PROOFSTEP]
exact h.mem_open V.unop.1.2 V.unop.2
[GOAL]
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : p₀ ⤳ y
U V : (OpenNhds y)ᵒᵖ
inc : U ⟶ V
⊢ (fun h =>
          eqToHom
            (_ :
              (fun U => if p₀ ∈ U.unop then A else ⊤_ C) ((OpenNhds.inclusion y).op.obj U) =
                (fun U => if p₀ ∈ U.unop then A else ⊤_ C) ((OpenNhds.inclusion y).op.obj V)))
        (_ : p₀ ∈ ↑((OpenNhds.inclusion y).op.obj V).unop) ≫
      (fun U => eqToHom (_ : (if p₀ ∈ U.unop.obj.carrier then A else ⊤_ C) = A)) V =
    (fun U => eqToHom (_ : (if p₀ ∈ U.unop.obj.carrier then A else ⊤_ C) = A)) U ≫
      ((Functor.const (OpenNhds y)ᵒᵖ).obj A).map inc
[PROOFSTEP]
erw [Category.comp_id, eqToHom_trans]
[GOAL]
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : p₀ ⤳ y
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
⊢ NatTrans.app (skyscraperPresheafCoconeOfSpecializes p₀ A h).ι U ≫
      (fun c =>
          eqToHom
              (_ :
                (skyscraperPresheafCoconeOfSpecializes p₀ A h).pt =
                  if True then (skyscraperPresheafCoconeOfSpecializes p₀ A h).pt else ⊤_ C) ≫
            NatTrans.app c.ι (op ⊤))
        c =
    NatTrans.app c.ι U
[PROOFSTEP]
dsimp
  -- Porting note : added a `dsimp`
[GOAL]
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : p₀ ⤳ y
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
⊢ eqToHom (_ : (if p₀ ∈ U.unop.obj.carrier then A else ⊤_ C) = A) ≫
      eqToHom (_ : A = if True then A else ⊤_ C) ≫ NatTrans.app c.ι (op ⊤) =
    NatTrans.app c.ι U
[PROOFSTEP]
rw [← c.w (homOfLE <| (le_top : unop U ≤ _)).op]
[GOAL]
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : p₀ ⤳ y
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
⊢ eqToHom (_ : (if p₀ ∈ U.unop.obj.carrier then A else ⊤_ C) = A) ≫
      eqToHom (_ : A = if True then A else ⊤_ C) ≫
        ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A).map (homOfLE (_ : U.unop ≤ ⊤)).op ≫
          NatTrans.app c.ι (op U.unop) =
    NatTrans.app c.ι U
[PROOFSTEP]
change _ ≫ _ ≫ dite _ _ _ ≫ _ = _
[GOAL]
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : p₀ ⤳ y
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
⊢ eqToHom (_ : (if p₀ ∈ U.unop.obj.carrier then A else ⊤_ C) = A) ≫
      eqToHom (_ : A = if True then A else ⊤_ C) ≫
        (if h : p₀ ∈ ((OpenNhds.inclusion y).op.obj (op U.unop)).unop then
            (fun h =>
                eqToHom
                  (_ :
                    (fun U => if p₀ ∈ U.unop then A else ⊤_ C) ((OpenNhds.inclusion y).op.obj (op ⊤)) =
                      (fun U => if p₀ ∈ U.unop then A else ⊤_ C) ((OpenNhds.inclusion y).op.obj (op U.unop))))
              h
          else
            (fun h =>
                IsTerminal.from
                  ((_ : (⊤_ C) = if p₀ ∈ ((OpenNhds.inclusion y).op.obj (op U.unop)).unop then A else ⊤_ C) ▸
                    terminalIsTerminal)
                  ((fun U => if p₀ ∈ U.unop then A else ⊤_ C) ((OpenNhds.inclusion y).op.obj (op ⊤))))
              h) ≫
          NatTrans.app c.ι (op U.unop) =
    NatTrans.app c.ι U
[PROOFSTEP]
rw [dif_pos]
[GOAL]
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : p₀ ⤳ y
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
⊢ eqToHom (_ : (if p₀ ∈ U.unop.obj.carrier then A else ⊤_ C) = A) ≫
      eqToHom (_ : A = if True then A else ⊤_ C) ≫
        (fun h =>
              eqToHom
                (_ :
                  (fun U => if p₀ ∈ U.unop then A else ⊤_ C) ((OpenNhds.inclusion y).op.obj (op ⊤)) =
                    (fun U => if p₀ ∈ U.unop then A else ⊤_ C) ((OpenNhds.inclusion y).op.obj (op U.unop))))
            ?hc ≫
          NatTrans.app c.ι (op U.unop) =
    NatTrans.app c.ι U
[PROOFSTEP]
simp only [skyscraperPresheafCoconeOfSpecializes_ι_app, eqToHom_trans_assoc, eqToHom_refl, Category.id_comp, unop_op,
  op_unop]
[GOAL]
case hc
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : p₀ ⤳ y
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
⊢ p₀ ∈ ((OpenNhds.inclusion y).op.obj (op U.unop)).unop
[PROOFSTEP]
exact h.mem_open U.unop.1.2 U.unop.2
[GOAL]
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h✝ : p₀ ⤳ y
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
f : (skyscraperPresheafCoconeOfSpecializes p₀ A h✝).pt ⟶ c.pt
h : ∀ (j : (OpenNhds y)ᵒᵖ), NatTrans.app (skyscraperPresheafCoconeOfSpecializes p₀ A h✝).ι j ≫ f = NatTrans.app c.ι j
⊢ f =
    (fun c =>
        eqToHom
            (_ :
              (skyscraperPresheafCoconeOfSpecializes p₀ A h✝).pt =
                if True then (skyscraperPresheafCoconeOfSpecializes p₀ A h✝).pt else ⊤_ C) ≫
          NatTrans.app c.ι (op ⊤))
      c
[PROOFSTEP]
dsimp
  -- Porting note : added a `dsimp`
[GOAL]
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h✝ : p₀ ⤳ y
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
f : (skyscraperPresheafCoconeOfSpecializes p₀ A h✝).pt ⟶ c.pt
h : ∀ (j : (OpenNhds y)ᵒᵖ), NatTrans.app (skyscraperPresheafCoconeOfSpecializes p₀ A h✝).ι j ≫ f = NatTrans.app c.ι j
⊢ f = eqToHom (_ : A = if True then A else ⊤_ C) ≫ NatTrans.app c.ι (op ⊤)
[PROOFSTEP]
rw [← h, skyscraperPresheafCoconeOfSpecializes_ι_app, eqToHom_trans_assoc, eqToHom_refl, Category.id_comp]
[GOAL]
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : ¬p₀ ⤳ y
h1 : ∃ U, ¬p₀ ∈ U.obj :=
  match Iff.mp not_specializes_iff_exists_open h with
  | Exists.intro U { left := ho, right := { left := h₀, right := hy } } =>
    Exists.intro { obj := { carrier := U, is_open' := ho }, property := h₀ } hy
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
⊢ NatTrans.app (skyscraperPresheafCocone p₀ A y).ι U ≫
      (fun c =>
          eqToHom
              (_ :
                (skyscraperPresheafCocone p₀ A y).pt =
                  if p₀ ∈ (Exists.choose h1).obj then A else (skyscraperPresheafCocone p₀ A y).pt) ≫
            NatTrans.app c.ι (op (Exists.choose h1)))
        c =
    NatTrans.app c.ι U
[PROOFSTEP]
change _ = c.ι.app (op U.unop)
[GOAL]
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : ¬p₀ ⤳ y
h1 : ∃ U, ¬p₀ ∈ U.obj :=
  match Iff.mp not_specializes_iff_exists_open h with
  | Exists.intro U { left := ho, right := { left := h₀, right := hy } } =>
    Exists.intro { obj := { carrier := U, is_open' := ho }, property := h₀ } hy
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
⊢ NatTrans.app (skyscraperPresheafCocone p₀ A y).ι U ≫
      (fun c =>
          eqToHom
              (_ :
                (skyscraperPresheafCocone p₀ A y).pt =
                  if p₀ ∈ (Exists.choose h1).obj then A else (skyscraperPresheafCocone p₀ A y).pt) ≫
            NatTrans.app c.ι (op (Exists.choose h1)))
        c =
    NatTrans.app c.ι (op U.unop)
[PROOFSTEP]
simp only [← c.w (homOfLE <| @inf_le_left _ _ h1.choose U.unop).op, ←
  c.w (homOfLE <| @inf_le_right _ _ h1.choose U.unop).op, ← Category.assoc]
[GOAL]
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : ¬p₀ ⤳ y
h1 : ∃ U, ¬p₀ ∈ U.obj :=
  match Iff.mp not_specializes_iff_exists_open h with
  | Exists.intro U { left := ho, right := { left := h₀, right := hy } } =>
    Exists.intro { obj := { carrier := U, is_open' := ho }, property := h₀ } hy
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
⊢ ((NatTrans.app (skyscraperPresheafCocone p₀ A y).ι U ≫
          eqToHom
            (_ :
              (skyscraperPresheafCocone p₀ A y).pt =
                if p₀ ∈ (Exists.choose h1).obj then A else (skyscraperPresheafCocone p₀ A y).pt)) ≫
        ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A).map
          (homOfLE (_ : Exists.choose h1 ⊓ U.unop ≤ Exists.choose h1)).op) ≫
      NatTrans.app c.ι (op (Exists.choose (_ : ∃ U, ¬p₀ ∈ U.obj) ⊓ U.unop)) =
    ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A).map (homOfLE (_ : Exists.choose h1 ⊓ U.unop ≤ U.unop)).op ≫
      NatTrans.app c.ι (op (Exists.choose (_ : ∃ U, ¬p₀ ∈ U.obj) ⊓ U.unop))
[PROOFSTEP]
congr 1
[GOAL]
case e_a
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : ¬p₀ ⤳ y
h1 : ∃ U, ¬p₀ ∈ U.obj :=
  match Iff.mp not_specializes_iff_exists_open h with
  | Exists.intro U { left := ho, right := { left := h₀, right := hy } } =>
    Exists.intro { obj := { carrier := U, is_open' := ho }, property := h₀ } hy
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
⊢ (NatTrans.app (skyscraperPresheafCocone p₀ A y).ι U ≫
        eqToHom
          (_ :
            (skyscraperPresheafCocone p₀ A y).pt =
              if p₀ ∈ (Exists.choose h1).obj then A else (skyscraperPresheafCocone p₀ A y).pt)) ≫
      ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A).map
        (homOfLE (_ : Exists.choose h1 ⊓ U.unop ≤ Exists.choose h1)).op =
    ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A).map (homOfLE (_ : Exists.choose h1 ⊓ U.unop ≤ U.unop)).op
[PROOFSTEP]
refine' ((if_neg _).symm.ndrec terminalIsTerminal).hom_ext _ _
[GOAL]
case e_a
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : ¬p₀ ⤳ y
h1 : ∃ U, ¬p₀ ∈ U.obj :=
  match Iff.mp not_specializes_iff_exists_open h with
  | Exists.intro U { left := ho, right := { left := h₀, right := hy } } =>
    Exists.intro { obj := { carrier := U, is_open' := ho }, property := h₀ } hy
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
U : (OpenNhds y)ᵒᵖ
⊢ ¬p₀ ∈ ((OpenNhds.inclusion y).op.obj (op (Exists.choose (_ : ∃ U, ¬p₀ ∈ U.obj) ⊓ U.unop))).unop
[PROOFSTEP]
exact fun h => h1.choose_spec h.1
[GOAL]
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : ¬p₀ ⤳ y
h1 : ∃ U, ¬p₀ ∈ U.obj :=
  match Iff.mp not_specializes_iff_exists_open h with
  | Exists.intro U { left := ho, right := { left := h₀, right := hy } } =>
    Exists.intro { obj := { carrier := U, is_open' := ho }, property := h₀ } hy
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
f : (skyscraperPresheafCocone p₀ A y).pt ⟶ c.pt
H : ∀ (j : (OpenNhds y)ᵒᵖ), NatTrans.app (skyscraperPresheafCocone p₀ A y).ι j ≫ f = NatTrans.app c.ι j
⊢ f =
    (fun c =>
        eqToHom
            (_ :
              (skyscraperPresheafCocone p₀ A y).pt =
                if p₀ ∈ (Exists.choose h1).obj then A else (skyscraperPresheafCocone p₀ A y).pt) ≫
          NatTrans.app c.ι (op (Exists.choose h1)))
      c
[PROOFSTEP]
dsimp
  -- Porting note : added a `dsimp`
[GOAL]
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : ¬p₀ ⤳ y
h1 : ∃ U, ¬p₀ ∈ U.obj :=
  match Iff.mp not_specializes_iff_exists_open h with
  | Exists.intro U { left := ho, right := { left := h₀, right := hy } } =>
    Exists.intro { obj := { carrier := U, is_open' := ho }, property := h₀ } hy
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
f : (skyscraperPresheafCocone p₀ A y).pt ⟶ c.pt
H : ∀ (j : (OpenNhds y)ᵒᵖ), NatTrans.app (skyscraperPresheafCocone p₀ A y).ι j ≫ f = NatTrans.app c.ι j
⊢ f =
    eqToHom (_ : (⊤_ C) = if p₀ ∈ (Exists.choose (_ : ∃ U, ¬p₀ ∈ U.obj)).obj then A else ⊤_ C) ≫
      NatTrans.app c.ι (op (Exists.choose (_ : ∃ U, ¬p₀ ∈ U.obj)))
[PROOFSTEP]
rw [← Category.id_comp f, ← H, ← Category.assoc]
[GOAL]
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : ¬p₀ ⤳ y
h1 : ∃ U, ¬p₀ ∈ U.obj :=
  match Iff.mp not_specializes_iff_exists_open h with
  | Exists.intro U { left := ho, right := { left := h₀, right := hy } } =>
    Exists.intro { obj := { carrier := U, is_open' := ho }, property := h₀ } hy
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
f : (skyscraperPresheafCocone p₀ A y).pt ⟶ c.pt
H : ∀ (j : (OpenNhds y)ᵒᵖ), NatTrans.app (skyscraperPresheafCocone p₀ A y).ι j ≫ f = NatTrans.app c.ι j
⊢ 𝟙 (skyscraperPresheafCocone p₀ A y).pt ≫ f =
    (eqToHom (_ : (⊤_ C) = if p₀ ∈ (Exists.choose (_ : ∃ U, ¬p₀ ∈ U.obj)).obj then A else ⊤_ C) ≫
        NatTrans.app (skyscraperPresheafCocone p₀ A y).ι (op (Exists.choose (_ : ∃ U, ¬p₀ ∈ U.obj)))) ≫
      f
[PROOFSTEP]
congr 1
[GOAL]
case e_a
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : ¬p₀ ⤳ y
h1 : ∃ U, ¬p₀ ∈ U.obj :=
  match Iff.mp not_specializes_iff_exists_open h with
  | Exists.intro U { left := ho, right := { left := h₀, right := hy } } =>
    Exists.intro { obj := { carrier := U, is_open' := ho }, property := h₀ } hy
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
f : (skyscraperPresheafCocone p₀ A y).pt ⟶ c.pt
H : ∀ (j : (OpenNhds y)ᵒᵖ), NatTrans.app (skyscraperPresheafCocone p₀ A y).ι j ≫ f = NatTrans.app c.ι j
⊢ 𝟙 (skyscraperPresheafCocone p₀ A y).pt =
    eqToHom (_ : (⊤_ C) = if p₀ ∈ (Exists.choose (_ : ∃ U, ¬p₀ ∈ U.obj)).obj then A else ⊤_ C) ≫
      NatTrans.app (skyscraperPresheafCocone p₀ A y).ι (op (Exists.choose (_ : ∃ U, ¬p₀ ∈ U.obj)))
[PROOFSTEP]
apply terminalIsTerminal.hom_ext
[GOAL]
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
⊢ TopCat.Presheaf.IsSheaf (skyscraperPresheaf p₀ A)
[PROOFSTEP]
classical exact
  (Presheaf.isSheaf_iso_iff (eqToIso <| skyscraperPresheaf_eq_pushforward p₀ A)).mpr <|
    (Sheaf.pushforward_sheaf_of_sheaf _
      (Presheaf.isSheaf_on_punit_of_isTerminal _
        (by
          dsimp [skyscraperPresheaf]
          rw [if_neg]
          · exact terminalIsTerminal
          · exact Set.not_mem_empty PUnit.unit)))
[GOAL]
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
⊢ TopCat.Presheaf.IsSheaf (skyscraperPresheaf p₀ A)
[PROOFSTEP]
exact
  (Presheaf.isSheaf_iso_iff (eqToIso <| skyscraperPresheaf_eq_pushforward p₀ A)).mpr <|
    (Sheaf.pushforward_sheaf_of_sheaf _
      (Presheaf.isSheaf_on_punit_of_isTerminal _
        (by
          dsimp [skyscraperPresheaf]
          rw [if_neg]
          · exact terminalIsTerminal
          · exact Set.not_mem_empty PUnit.unit)))
[GOAL]
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
⊢ IsTerminal ((skyscraperPresheaf PUnit.unit A).obj (op ⊥))
[PROOFSTEP]
dsimp [skyscraperPresheaf]
[GOAL]
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
⊢ IsTerminal (if PUnit.unit ∈ ⊥ then A else ⊤_ C)
[PROOFSTEP]
rw [if_neg]
[GOAL]
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
⊢ IsTerminal (⊤_ C)
[PROOFSTEP]
exact terminalIsTerminal
[GOAL]
case hnc
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
⊢ ¬PUnit.unit ∈ ⊥
[PROOFSTEP]
exact Set.not_mem_empty PUnit.unit
[GOAL]
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : Presheaf.stalk 𝓕 p₀ ⟶ c
U V : (Opens ↑X)ᵒᵖ
inc : U ⟶ V
⊢ 𝓕.map inc ≫
      (fun U =>
          if h : p₀ ∈ U.unop then
            Presheaf.germ 𝓕 { val := p₀, property := h } ≫ f ≫ eqToHom (_ : c = if p₀ ∈ U.unop then c else ⊤_ C)
          else IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ U.unop then c else ⊤_ C) ▸ terminalIsTerminal) (𝓕.obj U))
        V =
    (fun U =>
          if h : p₀ ∈ U.unop then
            Presheaf.germ 𝓕 { val := p₀, property := h } ≫ f ≫ eqToHom (_ : c = if p₀ ∈ U.unop then c else ⊤_ C)
          else IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ U.unop then c else ⊤_ C) ▸ terminalIsTerminal) (𝓕.obj U))
        U ≫
      (skyscraperPresheaf p₀ c).map inc
[PROOFSTEP]
dsimp
[GOAL]
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : Presheaf.stalk 𝓕 p₀ ⟶ c
U V : (Opens ↑X)ᵒᵖ
inc : U ⟶ V
⊢ (𝓕.map inc ≫
      if h : p₀ ∈ V.unop then
        Presheaf.germ 𝓕 { val := p₀, property := h } ≫ f ≫ eqToHom (_ : c = if p₀ ∈ V.unop then c else ⊤_ C)
      else IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then c else ⊤_ C) ▸ terminalIsTerminal) (𝓕.obj V)) =
    (if h : p₀ ∈ U.unop then
        Presheaf.germ 𝓕 { val := p₀, property := h } ≫ f ≫ eqToHom (_ : c = if p₀ ∈ U.unop then c else ⊤_ C)
      else IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ U.unop then c else ⊤_ C) ▸ terminalIsTerminal) (𝓕.obj U)) ≫
      if h : p₀ ∈ V.unop then
        eqToHom (_ : (fun U => if p₀ ∈ U.unop then c else ⊤_ C) U = (fun U => if p₀ ∈ U.unop then c else ⊤_ C) V)
      else
        IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then c else ⊤_ C) ▸ terminalIsTerminal)
          (if p₀ ∈ U.unop then c else ⊤_ C)
[PROOFSTEP]
by_cases hV : p₀ ∈ V.unop
[GOAL]
case pos
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : Presheaf.stalk 𝓕 p₀ ⟶ c
U V : (Opens ↑X)ᵒᵖ
inc : U ⟶ V
hV : p₀ ∈ V.unop
⊢ (𝓕.map inc ≫
      if h : p₀ ∈ V.unop then
        Presheaf.germ 𝓕 { val := p₀, property := h } ≫ f ≫ eqToHom (_ : c = if p₀ ∈ V.unop then c else ⊤_ C)
      else IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then c else ⊤_ C) ▸ terminalIsTerminal) (𝓕.obj V)) =
    (if h : p₀ ∈ U.unop then
        Presheaf.germ 𝓕 { val := p₀, property := h } ≫ f ≫ eqToHom (_ : c = if p₀ ∈ U.unop then c else ⊤_ C)
      else IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ U.unop then c else ⊤_ C) ▸ terminalIsTerminal) (𝓕.obj U)) ≫
      if h : p₀ ∈ V.unop then
        eqToHom (_ : (fun U => if p₀ ∈ U.unop then c else ⊤_ C) U = (fun U => if p₀ ∈ U.unop then c else ⊤_ C) V)
      else
        IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then c else ⊤_ C) ▸ terminalIsTerminal)
          (if p₀ ∈ U.unop then c else ⊤_ C)
[PROOFSTEP]
have hU : p₀ ∈ U.unop := leOfHom inc.unop hV
[GOAL]
case pos
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : Presheaf.stalk 𝓕 p₀ ⟶ c
U V : (Opens ↑X)ᵒᵖ
inc : U ⟶ V
hV : p₀ ∈ V.unop
hU : p₀ ∈ U.unop
⊢ (𝓕.map inc ≫
      if h : p₀ ∈ V.unop then
        Presheaf.germ 𝓕 { val := p₀, property := h } ≫ f ≫ eqToHom (_ : c = if p₀ ∈ V.unop then c else ⊤_ C)
      else IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then c else ⊤_ C) ▸ terminalIsTerminal) (𝓕.obj V)) =
    (if h : p₀ ∈ U.unop then
        Presheaf.germ 𝓕 { val := p₀, property := h } ≫ f ≫ eqToHom (_ : c = if p₀ ∈ U.unop then c else ⊤_ C)
      else IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ U.unop then c else ⊤_ C) ▸ terminalIsTerminal) (𝓕.obj U)) ≫
      if h : p₀ ∈ V.unop then
        eqToHom (_ : (fun U => if p₀ ∈ U.unop then c else ⊤_ C) U = (fun U => if p₀ ∈ U.unop then c else ⊤_ C) V)
      else
        IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then c else ⊤_ C) ▸ terminalIsTerminal)
          (if p₀ ∈ U.unop then c else ⊤_ C)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : Presheaf.stalk 𝓕 p₀ ⟶ c
U V : (Opens ↑X)ᵒᵖ
inc : U ⟶ V
hV : p₀ ∈ V.unop
hU : p₀ ∈ U.unop
h✝ : p₀ ∈ V.unop
⊢ 𝓕.map inc ≫ Presheaf.germ 𝓕 { val := p₀, property := h✝ } ≫ f ≫ eqToHom (_ : c = if p₀ ∈ V.unop then c else ⊤_ C) =
    (Presheaf.germ 𝓕 { val := p₀, property := hU } ≫ f ≫ eqToHom (_ : c = if p₀ ∈ U.unop then c else ⊤_ C)) ≫
      eqToHom (_ : (fun U => if p₀ ∈ U.unop then c else ⊤_ C) U = (fun U => if p₀ ∈ U.unop then c else ⊤_ C) V)
case neg
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : Presheaf.stalk 𝓕 p₀ ⟶ c
U V : (Opens ↑X)ᵒᵖ
inc : U ⟶ V
hV : p₀ ∈ V.unop
hU : p₀ ∈ U.unop
h✝ : ¬p₀ ∈ V.unop
⊢ 𝓕.map inc ≫ Presheaf.germ 𝓕 { val := p₀, property := hV } ≫ f ≫ eqToHom (_ : c = if p₀ ∈ V.unop then c else ⊤_ C) =
    (Presheaf.germ 𝓕 { val := p₀, property := hU } ≫ f ≫ eqToHom (_ : c = if p₀ ∈ U.unop then c else ⊤_ C)) ≫
      eqToHom (_ : (fun U => if p₀ ∈ U.unop then c else ⊤_ C) U = (fun U => if p₀ ∈ U.unop then c else ⊤_ C) V)
[PROOFSTEP]
erw [← Category.assoc, 𝓕.germ_res inc.unop, Category.assoc, Category.assoc, eqToHom_trans]
[GOAL]
case neg
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : Presheaf.stalk 𝓕 p₀ ⟶ c
U V : (Opens ↑X)ᵒᵖ
inc : U ⟶ V
hV : p₀ ∈ V.unop
hU : p₀ ∈ U.unop
h✝ : ¬p₀ ∈ V.unop
⊢ 𝓕.map inc ≫ Presheaf.germ 𝓕 { val := p₀, property := hV } ≫ f ≫ eqToHom (_ : c = if p₀ ∈ V.unop then c else ⊤_ C) =
    (Presheaf.germ 𝓕 { val := p₀, property := hU } ≫ f ≫ eqToHom (_ : c = if p₀ ∈ U.unop then c else ⊤_ C)) ≫
      eqToHom (_ : (fun U => if p₀ ∈ U.unop then c else ⊤_ C) U = (fun U => if p₀ ∈ U.unop then c else ⊤_ C) V)
[PROOFSTEP]
aesop_cat
[GOAL]
case neg
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : Presheaf.stalk 𝓕 p₀ ⟶ c
U V : (Opens ↑X)ᵒᵖ
inc : U ⟶ V
hV : ¬p₀ ∈ V.unop
⊢ (𝓕.map inc ≫
      if h : p₀ ∈ V.unop then
        Presheaf.germ 𝓕 { val := p₀, property := h } ≫ f ≫ eqToHom (_ : c = if p₀ ∈ V.unop then c else ⊤_ C)
      else IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then c else ⊤_ C) ▸ terminalIsTerminal) (𝓕.obj V)) =
    (if h : p₀ ∈ U.unop then
        Presheaf.germ 𝓕 { val := p₀, property := h } ≫ f ≫ eqToHom (_ : c = if p₀ ∈ U.unop then c else ⊤_ C)
      else IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ U.unop then c else ⊤_ C) ▸ terminalIsTerminal) (𝓕.obj U)) ≫
      if h : p₀ ∈ V.unop then
        eqToHom (_ : (fun U => if p₀ ∈ U.unop then c else ⊤_ C) U = (fun U => if p₀ ∈ U.unop then c else ⊤_ C) V)
      else
        IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then c else ⊤_ C) ▸ terminalIsTerminal)
          (if p₀ ∈ U.unop then c else ⊤_ C)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : Presheaf.stalk 𝓕 p₀ ⟶ c
U V : (Opens ↑X)ᵒᵖ
inc : U ⟶ V
hV : ¬p₀ ∈ V.unop
h✝ : p₀ ∈ V.unop
⊢ 𝓕.map inc ≫ Presheaf.germ 𝓕 { val := p₀, property := h✝ } ≫ f ≫ eqToHom (_ : c = if p₀ ∈ V.unop then c else ⊤_ C) =
    (if h : p₀ ∈ U.unop then
        Presheaf.germ 𝓕 { val := p₀, property := h } ≫ f ≫ eqToHom (_ : c = if p₀ ∈ U.unop then c else ⊤_ C)
      else IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ U.unop then c else ⊤_ C) ▸ terminalIsTerminal) (𝓕.obj U)) ≫
      eqToHom (_ : (fun U => if p₀ ∈ U.unop then c else ⊤_ C) U = (fun U => if p₀ ∈ U.unop then c else ⊤_ C) V)
case neg
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : Presheaf.stalk 𝓕 p₀ ⟶ c
U V : (Opens ↑X)ᵒᵖ
inc : U ⟶ V
hV h✝ : ¬p₀ ∈ V.unop
⊢ 𝓕.map inc ≫ IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then c else ⊤_ C) ▸ terminalIsTerminal) (𝓕.obj V) =
    (if h : p₀ ∈ U.unop then
        Presheaf.germ 𝓕 { val := p₀, property := h } ≫ f ≫ eqToHom (_ : c = if p₀ ∈ U.unop then c else ⊤_ C)
      else IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ U.unop then c else ⊤_ C) ▸ terminalIsTerminal) (𝓕.obj U)) ≫
      IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then c else ⊤_ C) ▸ terminalIsTerminal)
        (if p₀ ∈ U.unop then c else ⊤_ C)
[PROOFSTEP]
apply ((if_neg hV).symm.ndrec terminalIsTerminal).hom_ext
[GOAL]
case neg
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : Presheaf.stalk 𝓕 p₀ ⟶ c
U V : (Opens ↑X)ᵒᵖ
inc : U ⟶ V
hV h✝ : ¬p₀ ∈ V.unop
⊢ 𝓕.map inc ≫ IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then c else ⊤_ C) ▸ terminalIsTerminal) (𝓕.obj V) =
    (if h : p₀ ∈ U.unop then
        Presheaf.germ 𝓕 { val := p₀, property := h } ≫ f ≫ eqToHom (_ : c = if p₀ ∈ U.unop then c else ⊤_ C)
      else IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ U.unop then c else ⊤_ C) ▸ terminalIsTerminal) (𝓕.obj U)) ≫
      IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ V.unop then c else ⊤_ C) ▸ terminalIsTerminal)
        (if p₀ ∈ U.unop then c else ⊤_ C)
[PROOFSTEP]
aesop_cat
[GOAL]
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U V : (OpenNhds p₀)ᵒᵖ
inc : U ⟶ V
⊢ ((OpenNhds.inclusion p₀).op ⋙ 𝓕).map inc ≫
      (fun U => NatTrans.app f (op U.unop.obj) ≫ eqToHom (_ : (if p₀ ∈ U.unop.obj then c else ⊤_ C) = c)) V =
    (fun U => NatTrans.app f (op U.unop.obj) ≫ eqToHom (_ : (if p₀ ∈ U.unop.obj then c else ⊤_ C) = c)) U ≫
      ((Functor.const (OpenNhds p₀)ᵒᵖ).obj c).map inc
[PROOFSTEP]
dsimp
[GOAL]
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U V : (OpenNhds p₀)ᵒᵖ
inc : U ⟶ V
⊢ 𝓕.map ((OpenNhds.inclusion p₀).map inc.unop).op ≫
      NatTrans.app f (op V.unop.obj) ≫ eqToHom (_ : (if p₀ ∈ V.unop.obj then c else ⊤_ C) = c) =
    (NatTrans.app f (op U.unop.obj) ≫ eqToHom (_ : (if p₀ ∈ U.unop.obj then c else ⊤_ C) = c)) ≫ 𝟙 c
[PROOFSTEP]
erw [Category.comp_id, ← Category.assoc, comp_eqToHom_iff, Category.assoc, eqToHom_trans, f.naturality,
  skyscraperPresheaf_map]
  -- Porting note : added this `dsimp` and `rfl` in the end
[GOAL]
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U V : (OpenNhds p₀)ᵒᵖ
inc : U ⟶ V
⊢ (NatTrans.app f (op ((OpenNhds.inclusion p₀).obj U.unop)) ≫
      if h : p₀ ∈ (op ((OpenNhds.inclusion p₀).obj V.unop)).unop then
        eqToHom
          (_ :
            (fun U => if p₀ ∈ U.unop then c else ⊤_ C) (op ((OpenNhds.inclusion p₀).obj U.unop)) =
              (fun U => if p₀ ∈ U.unop then c else ⊤_ C) (op ((OpenNhds.inclusion p₀).obj V.unop)))
      else
        IsTerminal.from
          ((_ : (⊤_ C) = if p₀ ∈ (op ((OpenNhds.inclusion p₀).obj V.unop)).unop then c else ⊤_ C) ▸ terminalIsTerminal)
          ((fun U => if p₀ ∈ U.unop then c else ⊤_ C) (op ((OpenNhds.inclusion p₀).obj U.unop)))) =
    NatTrans.app f (op U.unop.obj) ≫
      eqToHom (_ : (if p₀ ∈ U.unop.obj then c else ⊤_ C) = if p₀ ∈ V.unop.obj then c else ⊤_ C)
[PROOFSTEP]
dsimp only [skyscraperPresheaf_obj, unop_op, Eq.ndrec]
[GOAL]
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U V : (OpenNhds p₀)ᵒᵖ
inc : U ⟶ V
⊢ (NatTrans.app f (op ((OpenNhds.inclusion p₀).obj U.unop)) ≫
      if h : p₀ ∈ (OpenNhds.inclusion p₀).obj V.unop then
        eqToHom
          (_ :
            (fun U => if p₀ ∈ U.unop then c else ⊤_ C) (op ((OpenNhds.inclusion p₀).obj U.unop)) =
              (fun U => if p₀ ∈ U.unop then c else ⊤_ C) (op ((OpenNhds.inclusion p₀).obj V.unop)))
      else
        IsTerminal.from
          ((_ : (⊤_ C) = if p₀ ∈ (op ((OpenNhds.inclusion p₀).obj V.unop)).unop then c else ⊤_ C) ▸ terminalIsTerminal)
          (if p₀ ∈ (OpenNhds.inclusion p₀).obj U.unop then c else ⊤_ C)) =
    NatTrans.app f (op U.unop.obj) ≫
      eqToHom (_ : (if p₀ ∈ U.unop.obj then c else ⊤_ C) = if p₀ ∈ V.unop.obj then c else ⊤_ C)
[PROOFSTEP]
have hV : p₀ ∈ (OpenNhds.inclusion p₀).obj V.unop := V.unop.2
[GOAL]
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U V : (OpenNhds p₀)ᵒᵖ
inc : U ⟶ V
hV : p₀ ∈ (OpenNhds.inclusion p₀).obj V.unop
⊢ (NatTrans.app f (op ((OpenNhds.inclusion p₀).obj U.unop)) ≫
      if h : p₀ ∈ (OpenNhds.inclusion p₀).obj V.unop then
        eqToHom
          (_ :
            (fun U => if p₀ ∈ U.unop then c else ⊤_ C) (op ((OpenNhds.inclusion p₀).obj U.unop)) =
              (fun U => if p₀ ∈ U.unop then c else ⊤_ C) (op ((OpenNhds.inclusion p₀).obj V.unop)))
      else
        IsTerminal.from
          ((_ : (⊤_ C) = if p₀ ∈ (op ((OpenNhds.inclusion p₀).obj V.unop)).unop then c else ⊤_ C) ▸ terminalIsTerminal)
          (if p₀ ∈ (OpenNhds.inclusion p₀).obj U.unop then c else ⊤_ C)) =
    NatTrans.app f (op U.unop.obj) ≫
      eqToHom (_ : (if p₀ ∈ U.unop.obj then c else ⊤_ C) = if p₀ ∈ V.unop.obj then c else ⊤_ C)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U V : (OpenNhds p₀)ᵒᵖ
inc : U ⟶ V
hV : p₀ ∈ (OpenNhds.inclusion p₀).obj V.unop
h✝ : p₀ ∈ V.unop.obj
⊢ NatTrans.app f (op ((OpenNhds.inclusion p₀).obj U.unop)) ≫
      eqToHom
        (_ :
          (fun U => if p₀ ∈ U.unop then c else ⊤_ C) (op ((OpenNhds.inclusion p₀).obj U.unop)) =
            (fun U => if p₀ ∈ U.unop then c else ⊤_ C) (op ((OpenNhds.inclusion p₀).obj V.unop))) =
    NatTrans.app f (op U.unop.obj) ≫
      eqToHom (_ : (if p₀ ∈ U.unop.obj then c else ⊤_ C) = if p₀ ∈ V.unop.obj then c else ⊤_ C)
[PROOFSTEP]
simp only [comp_eqToHom_iff, Category.assoc, eqToHom_trans, eqToHom_refl, Category.comp_id]
[GOAL]
case neg
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U V : (OpenNhds p₀)ᵒᵖ
inc : U ⟶ V
hV : p₀ ∈ (OpenNhds.inclusion p₀).obj V.unop
h✝ : ¬p₀ ∈ V.unop.obj
⊢ NatTrans.app f (op ((OpenNhds.inclusion p₀).obj U.unop)) ≫
      eqToHom
        (_ :
          (fun U => if p₀ ∈ U.unop then c else ⊤_ C) (op ((OpenNhds.inclusion p₀).obj U.unop)) =
            (fun U => if p₀ ∈ U.unop then c else ⊤_ C) (op ((OpenNhds.inclusion p₀).obj V.unop))) =
    NatTrans.app f (op U.unop.obj) ≫
      eqToHom (_ : (if p₀ ∈ U.unop.obj then c else ⊤_ C) = if p₀ ∈ V.unop.obj then c else ⊤_ C)
[PROOFSTEP]
simp only [comp_eqToHom_iff, Category.assoc, eqToHom_trans, eqToHom_refl, Category.comp_id]
[GOAL]
case pos
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U V : (OpenNhds p₀)ᵒᵖ
inc : U ⟶ V
hV : p₀ ∈ (OpenNhds.inclusion p₀).obj V.unop
h✝ : p₀ ∈ V.unop.obj
⊢ NatTrans.app f (op ((OpenNhds.inclusion p₀).obj U.unop)) = NatTrans.app f (op U.unop.obj)
[PROOFSTEP]
rfl
[GOAL]
case neg
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U V : (OpenNhds p₀)ᵒᵖ
inc : U ⟶ V
hV : p₀ ∈ (OpenNhds.inclusion p₀).obj V.unop
h✝ : ¬p₀ ∈ V.unop.obj
⊢ NatTrans.app f (op ((OpenNhds.inclusion p₀).obj U.unop)) = NatTrans.app f (op U.unop.obj)
[PROOFSTEP]
rfl
[GOAL]
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U : (Opens ↑X)ᵒᵖ
h : p₀ ∈ U.unop
⊢ NatTrans.app (toSkyscraperPresheaf p₀ (fromStalk p₀ f)) U = NatTrans.app f U
[PROOFSTEP]
dsimp
[GOAL]
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U : (Opens ↑X)ᵒᵖ
h : p₀ ∈ U.unop
⊢ (if h : p₀ ∈ U.unop then
      Presheaf.germ 𝓕 { val := p₀, property := h } ≫ fromStalk p₀ f ≫ eqToHom (_ : c = if p₀ ∈ U.unop then c else ⊤_ C)
    else IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ U.unop then c else ⊤_ C) ▸ terminalIsTerminal) (𝓕.obj U)) =
    NatTrans.app f U
[PROOFSTEP]
split_ifs
[GOAL]
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U : (Opens ↑X)ᵒᵖ
h : p₀ ∈ U.unop
⊢ Presheaf.germ 𝓕 { val := p₀, property := h } ≫ fromStalk p₀ f ≫ eqToHom (_ : c = if p₀ ∈ U.unop then c else ⊤_ C) =
    NatTrans.app f U
[PROOFSTEP]
erw [← Category.assoc, colimit.ι_desc, Category.assoc, eqToHom_trans, eqToHom_refl, Category.comp_id]
[GOAL]
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U : (Opens ↑X)ᵒᵖ
h : p₀ ∈ U.unop
⊢ NatTrans.app f (op (op { obj := U.unop, property := (_ : ↑{ val := p₀, property := h } ∈ U.unop) }).unop.obj) =
    NatTrans.app f U
[PROOFSTEP]
rfl
[GOAL]
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U : (Opens ↑X)ᵒᵖ
h : ¬p₀ ∈ U.unop
⊢ NatTrans.app (toSkyscraperPresheaf p₀ (fromStalk p₀ f)) U = NatTrans.app f U
[PROOFSTEP]
dsimp
[GOAL]
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U : (Opens ↑X)ᵒᵖ
h : ¬p₀ ∈ U.unop
⊢ (if h : p₀ ∈ U.unop then
      Presheaf.germ 𝓕 { val := p₀, property := h } ≫ fromStalk p₀ f ≫ eqToHom (_ : c = if p₀ ∈ U.unop then c else ⊤_ C)
    else IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ U.unop then c else ⊤_ C) ▸ terminalIsTerminal) (𝓕.obj U)) =
    NatTrans.app f U
[PROOFSTEP]
split_ifs
[GOAL]
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U : (Opens ↑X)ᵒᵖ
h : ¬p₀ ∈ U.unop
⊢ IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ U.unop then c else ⊤_ C) ▸ terminalIsTerminal) (𝓕.obj U) = NatTrans.app f U
[PROOFSTEP]
apply ((if_neg h).symm.ndrec terminalIsTerminal).hom_ext
[GOAL]
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : Presheaf.stalk 𝓕 p₀ ⟶ c
U : (OpenNhds p₀)ᵒᵖ
⊢ colimit.ι (((whiskeringLeft (OpenNhds p₀)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion p₀).op).obj 𝓕) U ≫
      fromStalk p₀ (toSkyscraperPresheaf p₀ f) =
    colimit.ι (((whiskeringLeft (OpenNhds p₀)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion p₀).op).obj 𝓕) U ≫ f
[PROOFSTEP]
erw [colimit.ι_desc]
[GOAL]
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : Presheaf.stalk 𝓕 p₀ ⟶ c
U : (OpenNhds p₀)ᵒᵖ
⊢ NatTrans.app
      { pt := c,
          ι :=
            NatTrans.mk fun U =>
              NatTrans.app (toSkyscraperPresheaf p₀ f) (op U.unop.obj) ≫
                eqToHom (_ : (if p₀ ∈ U.unop.obj then c else ⊤_ C) = c) }.ι
      U =
    colimit.ι (((whiskeringLeft (OpenNhds p₀)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion p₀).op).obj 𝓕) U ≫ f
[PROOFSTEP]
dsimp
[GOAL]
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : Presheaf.stalk 𝓕 p₀ ⟶ c
U : (OpenNhds p₀)ᵒᵖ
⊢ (if h : p₀ ∈ U.unop.obj then
        Presheaf.germ 𝓕 { val := p₀, property := h } ≫
          f ≫ eqToHom (_ : c = if p₀ ∈ (op U.unop.obj).unop then c else ⊤_ C)
      else
        IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ (op U.unop.obj).unop then c else ⊤_ C) ▸ terminalIsTerminal)
          (𝓕.obj (op U.unop.obj))) ≫
      eqToHom (_ : (if p₀ ∈ U.unop.obj then c else ⊤_ C) = c) =
    colimit.ι ((OpenNhds.inclusion p₀).op ⋙ 𝓕) U ≫ f
[PROOFSTEP]
rw [dif_pos U.unop.2]
[GOAL]
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : Presheaf.stalk 𝓕 p₀ ⟶ c
U : (OpenNhds p₀)ᵒᵖ
⊢ (Presheaf.germ 𝓕 { val := p₀, property := (_ : p₀ ∈ U.unop.obj) } ≫
        f ≫ eqToHom (_ : c = if p₀ ∈ (op U.unop.obj).unop then c else ⊤_ C)) ≫
      eqToHom (_ : (if p₀ ∈ U.unop.obj then c else ⊤_ C) = c) =
    colimit.ι ((OpenNhds.inclusion p₀).op ⋙ 𝓕) U ≫ f
[PROOFSTEP]
rw [Category.assoc, Category.assoc, eqToHom_trans, eqToHom_refl, Category.comp_id, Presheaf.germ]
[GOAL]
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : Presheaf.stalk 𝓕 p₀ ⟶ c
U : (OpenNhds p₀)ᵒᵖ
⊢ colimit.ι ((OpenNhds.inclusion ↑{ val := p₀, property := (_ : p₀ ∈ U.unop.obj) }).op ⋙ 𝓕)
        (op { obj := U.unop.obj, property := (_ : ↑{ val := p₀, property := (_ : p₀ ∈ U.unop.obj) } ∈ U.unop.obj) }) ≫
      f =
    colimit.ι ((OpenNhds.inclusion p₀).op ⋙ 𝓕) U ≫ f
[PROOFSTEP]
congr 3
[GOAL]
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 𝓖 : Presheaf C X
f : 𝓕 ⟶ 𝓖
⊢ (𝟭 (Presheaf C X)).map f ≫ (fun 𝓕 => toSkyscraperPresheaf p₀ (𝟙 (Presheaf.stalk ((𝟭 (Presheaf C X)).obj 𝓕) p₀))) 𝓖 =
    (fun 𝓕 => toSkyscraperPresheaf p₀ (𝟙 (Presheaf.stalk ((𝟭 (Presheaf C X)).obj 𝓕) p₀))) 𝓕 ≫
      (Presheaf.stalkFunctor C p₀ ⋙ skyscraperPresheafFunctor p₀).map f
[PROOFSTEP]
ext U
[GOAL]
case w
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 𝓖 : Presheaf C X
f : 𝓕 ⟶ 𝓖
U : Opens ↑X
⊢ NatTrans.app
      ((𝟭 (Presheaf C X)).map f ≫
        (fun 𝓕 => toSkyscraperPresheaf p₀ (𝟙 (Presheaf.stalk ((𝟭 (Presheaf C X)).obj 𝓕) p₀))) 𝓖)
      (op U) =
    NatTrans.app
      ((fun 𝓕 => toSkyscraperPresheaf p₀ (𝟙 (Presheaf.stalk ((𝟭 (Presheaf C X)).obj 𝓕) p₀))) 𝓕 ≫
        (Presheaf.stalkFunctor C p₀ ⋙ skyscraperPresheafFunctor p₀).map f)
      (op U)
[PROOFSTEP]
dsimp
  -- Porting note : added the following `rw` and `dsimp` to make it compile
[GOAL]
case w
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 𝓖 : Presheaf C X
f : 𝓕 ⟶ 𝓖
U : Opens ↑X
⊢ NatTrans.app (f ≫ toSkyscraperPresheaf p₀ (𝟙 (Presheaf.stalk 𝓖 p₀))) (op U) =
    NatTrans.app
      (toSkyscraperPresheaf p₀ (𝟙 (Presheaf.stalk 𝓕 p₀)) ≫
        SkyscraperPresheafFunctor.map' p₀ ((Presheaf.stalkFunctor C p₀).map f))
      (op U)
[PROOFSTEP]
rw [NatTrans.comp_app, toSkyscraperPresheaf_app, NatTrans.comp_app, toSkyscraperPresheaf_app]
[GOAL]
case w
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 𝓖 : Presheaf C X
f : 𝓕 ⟶ 𝓖
U : Opens ↑X
⊢ (NatTrans.app f (op U) ≫
      if h : p₀ ∈ (op U).unop then
        Presheaf.germ 𝓖 { val := p₀, property := h } ≫
          𝟙 (Presheaf.stalk 𝓖 p₀) ≫
            eqToHom (_ : Presheaf.stalk 𝓖 p₀ = if p₀ ∈ (op U).unop then Presheaf.stalk 𝓖 p₀ else ⊤_ C)
      else
        IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ (op U).unop then Presheaf.stalk 𝓖 p₀ else ⊤_ C) ▸ terminalIsTerminal)
          (𝓖.obj (op U))) =
    (if h : p₀ ∈ (op U).unop then
        Presheaf.germ 𝓕 { val := p₀, property := h } ≫
          𝟙 (Presheaf.stalk 𝓕 p₀) ≫
            eqToHom (_ : Presheaf.stalk 𝓕 p₀ = if p₀ ∈ (op U).unop then Presheaf.stalk 𝓕 p₀ else ⊤_ C)
      else
        IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ (op U).unop then Presheaf.stalk 𝓕 p₀ else ⊤_ C) ▸ terminalIsTerminal)
          (𝓕.obj (op U))) ≫
      NatTrans.app (SkyscraperPresheafFunctor.map' p₀ ((Presheaf.stalkFunctor C p₀).map f)) (op U)
[PROOFSTEP]
dsimp only [skyscraperPresheaf_obj, unop_op, Eq.ndrec, SkyscraperPresheafFunctor.map'_app]
[GOAL]
case w
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 𝓖 : Presheaf C X
f : 𝓕 ⟶ 𝓖
U : Opens ↑X
⊢ (NatTrans.app f (op U) ≫
      if h : p₀ ∈ U then
        Presheaf.germ 𝓖 { val := p₀, property := h } ≫
          𝟙 (Presheaf.stalk 𝓖 p₀) ≫
            eqToHom (_ : Presheaf.stalk 𝓖 p₀ = if p₀ ∈ (op U).unop then Presheaf.stalk 𝓖 p₀ else ⊤_ C)
      else
        IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ (op U).unop then Presheaf.stalk 𝓖 p₀ else ⊤_ C) ▸ terminalIsTerminal)
          (𝓖.obj (op U))) =
    (if h : p₀ ∈ U then
        Presheaf.germ 𝓕 { val := p₀, property := h } ≫
          𝟙 (Presheaf.stalk 𝓕 p₀) ≫
            eqToHom (_ : Presheaf.stalk 𝓕 p₀ = if p₀ ∈ (op U).unop then Presheaf.stalk 𝓕 p₀ else ⊤_ C)
      else
        IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ (op U).unop then Presheaf.stalk 𝓕 p₀ else ⊤_ C) ▸ terminalIsTerminal)
          (𝓕.obj (op U))) ≫
      if h : p₀ ∈ U then
        eqToHom (_ : (if p₀ ∈ (op U).unop then Presheaf.stalk 𝓕 p₀ else ⊤_ C) = Presheaf.stalk 𝓕 p₀) ≫
          (Presheaf.stalkFunctor C p₀).map f ≫
            eqToHom (_ : Presheaf.stalk 𝓖 p₀ = if p₀ ∈ (op U).unop then Presheaf.stalk 𝓖 p₀ else ⊤_ C)
      else
        IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ (op U).unop then Presheaf.stalk 𝓖 p₀ else ⊤_ C) ▸ terminalIsTerminal)
          (if p₀ ∈ U then Presheaf.stalk 𝓕 p₀ else ⊤_ C)
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 𝓖 : Presheaf C X
f : 𝓕 ⟶ 𝓖
U : Opens ↑X
h : p₀ ∈ U
⊢ NatTrans.app f (op U) ≫
      Presheaf.germ 𝓖 { val := p₀, property := h } ≫
        𝟙 (Presheaf.stalk 𝓖 p₀) ≫
          eqToHom (_ : Presheaf.stalk 𝓖 p₀ = if p₀ ∈ (op U).unop then Presheaf.stalk 𝓖 p₀ else ⊤_ C) =
    (Presheaf.germ 𝓕 { val := p₀, property := h } ≫
        𝟙 (Presheaf.stalk 𝓕 p₀) ≫
          eqToHom (_ : Presheaf.stalk 𝓕 p₀ = if p₀ ∈ (op U).unop then Presheaf.stalk 𝓕 p₀ else ⊤_ C)) ≫
      eqToHom (_ : (if p₀ ∈ (op U).unop then Presheaf.stalk 𝓕 p₀ else ⊤_ C) = Presheaf.stalk 𝓕 p₀) ≫
        (Presheaf.stalkFunctor C p₀).map f ≫
          eqToHom (_ : Presheaf.stalk 𝓖 p₀ = if p₀ ∈ (op U).unop then Presheaf.stalk 𝓖 p₀ else ⊤_ C)
[PROOFSTEP]
simp only [Category.id_comp, ← Category.assoc]
[GOAL]
case pos
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 𝓖 : Presheaf C X
f : 𝓕 ⟶ 𝓖
U : Opens ↑X
h : p₀ ∈ U
⊢ (NatTrans.app f (op U) ≫ Presheaf.germ 𝓖 { val := p₀, property := h }) ≫
      eqToHom (_ : Presheaf.stalk 𝓖 p₀ = if p₀ ∈ (op U).unop then Presheaf.stalk 𝓖 p₀ else ⊤_ C) =
    (((Presheaf.germ 𝓕 { val := p₀, property := h } ≫
            eqToHom (_ : Presheaf.stalk 𝓕 p₀ = if p₀ ∈ (op U).unop then Presheaf.stalk 𝓕 p₀ else ⊤_ C)) ≫
          eqToHom (_ : (if p₀ ∈ (op U).unop then Presheaf.stalk 𝓕 p₀ else ⊤_ C) = Presheaf.stalk 𝓕 p₀)) ≫
        (Presheaf.stalkFunctor C p₀).map f) ≫
      eqToHom (_ : Presheaf.stalk 𝓖 p₀ = if p₀ ∈ (op U).unop then Presheaf.stalk 𝓖 p₀ else ⊤_ C)
[PROOFSTEP]
rw [comp_eqToHom_iff]
[GOAL]
case pos
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 𝓖 : Presheaf C X
f : 𝓕 ⟶ 𝓖
U : Opens ↑X
h : p₀ ∈ U
⊢ NatTrans.app f (op U) ≫ Presheaf.germ 𝓖 { val := p₀, property := h } =
    ((((Presheaf.germ 𝓕 { val := p₀, property := h } ≫
              eqToHom (_ : Presheaf.stalk 𝓕 p₀ = if p₀ ∈ (op U).unop then Presheaf.stalk 𝓕 p₀ else ⊤_ C)) ≫
            eqToHom (_ : (if p₀ ∈ (op U).unop then Presheaf.stalk 𝓕 p₀ else ⊤_ C) = Presheaf.stalk 𝓕 p₀)) ≫
          (Presheaf.stalkFunctor C p₀).map f) ≫
        eqToHom (_ : Presheaf.stalk 𝓖 p₀ = if p₀ ∈ (op U).unop then Presheaf.stalk 𝓖 p₀ else ⊤_ C)) ≫
      eqToHom (_ : (if p₀ ∈ U then Presheaf.stalk 𝓖 p₀ else ⊤_ C) = Presheaf.stalk 𝓖 p₀)
[PROOFSTEP]
simp only [Category.assoc, eqToHom_trans, eqToHom_refl, Category.comp_id]
[GOAL]
case pos
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 𝓖 : Presheaf C X
f : 𝓕 ⟶ 𝓖
U : Opens ↑X
h : p₀ ∈ U
⊢ NatTrans.app f (op U) ≫ Presheaf.germ 𝓖 { val := p₀, property := h } =
    Presheaf.germ 𝓕 { val := p₀, property := h } ≫ (Presheaf.stalkFunctor C p₀).map f
[PROOFSTEP]
erw [colimit.ι_map]
[GOAL]
case pos
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 𝓖 : Presheaf C X
f : 𝓕 ⟶ 𝓖
U : Opens ↑X
h : p₀ ∈ U
⊢ NatTrans.app f (op U) ≫ Presheaf.germ 𝓖 { val := p₀, property := h } =
    NatTrans.app (((whiskeringLeft (OpenNhds p₀)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion p₀).op).map f)
        (op { obj := U, property := (_ : ↑{ val := p₀, property := h } ∈ U) }) ≫
      colimit.ι (((whiskeringLeft (OpenNhds p₀)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion p₀).op).obj 𝓖)
        (op { obj := U, property := (_ : ↑{ val := p₀, property := h } ∈ U) })
[PROOFSTEP]
rfl
[GOAL]
case neg
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 𝓖 : Presheaf C X
f : 𝓕 ⟶ 𝓖
U : Opens ↑X
h : ¬p₀ ∈ U
⊢ NatTrans.app f (op U) ≫
      IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ (op U).unop then Presheaf.stalk 𝓖 p₀ else ⊤_ C) ▸ terminalIsTerminal)
        (𝓖.obj (op U)) =
    IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ (op U).unop then Presheaf.stalk 𝓕 p₀ else ⊤_ C) ▸ terminalIsTerminal)
        (𝓕.obj (op U)) ≫
      IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ (op U).unop then Presheaf.stalk 𝓖 p₀ else ⊤_ C) ▸ terminalIsTerminal)
        (if p₀ ∈ U then Presheaf.stalk 𝓕 p₀ else ⊤_ C)
[PROOFSTEP]
apply ((if_neg h).symm.ndrec terminalIsTerminal).hom_ext
[GOAL]
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
x y : C
f : x ⟶ y
U : (OpenNhds p₀)ᵒᵖ
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds p₀)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion p₀).op).obj
          ((skyscraperPresheafFunctor p₀).obj x))
        U ≫
      (skyscraperPresheafFunctor p₀ ⋙ Presheaf.stalkFunctor C p₀).map f ≫
        (fun c => (skyscraperPresheafStalkOfSpecializes p₀ c (_ : p₀ ⤳ p₀)).hom) y =
    colimit.ι
        (((whiskeringLeft (OpenNhds p₀)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion p₀).op).obj
          ((skyscraperPresheafFunctor p₀).obj x))
        U ≫
      (fun c => (skyscraperPresheafStalkOfSpecializes p₀ c (_ : p₀ ⤳ p₀)).hom) x ≫ (𝟭 C).map f
[PROOFSTEP]
erw [← Category.assoc, colimit.ι_map, colimit.isoColimitCocone_ι_hom_assoc,
  skyscraperPresheafCoconeOfSpecializes_ι_app (h := specializes_rfl), Category.assoc, colimit.ι_desc,
  whiskeringLeft_obj_map, whiskerLeft_app, SkyscraperPresheafFunctor.map'_app, dif_pos U.unop.2,
  skyscraperPresheafCoconeOfSpecializes_ι_app (h := specializes_rfl), comp_eqToHom_iff, Category.assoc,
  eqToHom_comp_iff, ← Category.assoc, eqToHom_trans, eqToHom_refl, Category.id_comp, comp_eqToHom_iff, Category.assoc,
  eqToHom_trans, eqToHom_refl, Category.comp_id, CategoryTheory.Functor.id_map]
[GOAL]
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
α : (Presheaf.stalkFunctor C p₀).obj 𝓕 ⟶ c
⊢ ↑((fun c 𝓕 =>
            { toFun := toSkyscraperPresheaf p₀, invFun := fromStalk p₀,
              left_inv := (_ : ∀ (f : Presheaf.stalk c p₀ ⟶ 𝓕), fromStalk p₀ (toSkyscraperPresheaf p₀ f) = f),
              right_inv := (_ : ∀ (f : c ⟶ skyscraperPresheaf p₀ 𝓕), toSkyscraperPresheaf p₀ (fromStalk p₀ f) = f) })
          𝓕 c)
      α =
    NatTrans.app (StalkSkyscraperPresheafAdjunctionAuxs.unit p₀) 𝓕 ≫ (skyscraperPresheafFunctor p₀).map α
[PROOFSTEP]
ext U
[GOAL]
case w
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
α : (Presheaf.stalkFunctor C p₀).obj 𝓕 ⟶ c
U : Opens ↑X
⊢ NatTrans.app
      (↑((fun c 𝓕 =>
              { toFun := toSkyscraperPresheaf p₀, invFun := fromStalk p₀,
                left_inv := (_ : ∀ (f : Presheaf.stalk c p₀ ⟶ 𝓕), fromStalk p₀ (toSkyscraperPresheaf p₀ f) = f),
                right_inv := (_ : ∀ (f : c ⟶ skyscraperPresheaf p₀ 𝓕), toSkyscraperPresheaf p₀ (fromStalk p₀ f) = f) })
            𝓕 c)
        α)
      (op U) =
    NatTrans.app (NatTrans.app (StalkSkyscraperPresheafAdjunctionAuxs.unit p₀) 𝓕 ≫ (skyscraperPresheafFunctor p₀).map α)
      (op U)
[PROOFSTEP]
rw [NatTrans.comp_app]
[GOAL]
case w
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
α : (Presheaf.stalkFunctor C p₀).obj 𝓕 ⟶ c
U : Opens ↑X
⊢ NatTrans.app
      (↑((fun c 𝓕 =>
              { toFun := toSkyscraperPresheaf p₀, invFun := fromStalk p₀,
                left_inv := (_ : ∀ (f : Presheaf.stalk c p₀ ⟶ 𝓕), fromStalk p₀ (toSkyscraperPresheaf p₀ f) = f),
                right_inv := (_ : ∀ (f : c ⟶ skyscraperPresheaf p₀ 𝓕), toSkyscraperPresheaf p₀ (fromStalk p₀ f) = f) })
            𝓕 c)
        α)
      (op U) =
    NatTrans.app (NatTrans.app (StalkSkyscraperPresheafAdjunctionAuxs.unit p₀) 𝓕) (op U) ≫
      NatTrans.app ((skyscraperPresheafFunctor p₀).map α) (op U)
[PROOFSTEP]
simp only [Equiv.coe_fn_mk, toSkyscraperPresheaf_app, SkyscraperPresheafFunctor.map'_app, skyscraperPresheafFunctor_map,
  unit_app]
[GOAL]
case w
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
α : (Presheaf.stalkFunctor C p₀).obj 𝓕 ⟶ c
U : Opens ↑X
⊢ (if h : p₀ ∈ (op U).unop then
      Presheaf.germ 𝓕 { val := p₀, property := (_ : p₀ ∈ (op U).unop) } ≫
        α ≫ eqToHom (_ : c = if p₀ ∈ (op U).unop then c else ⊤_ C)
    else IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ (op U).unop then c else ⊤_ C) ▸ terminalIsTerminal) (𝓕.obj (op U))) =
    (if h : p₀ ∈ (op U).unop then
        Presheaf.germ 𝓕 { val := p₀, property := (_ : p₀ ∈ (op U).unop) } ≫
          𝟙 (Presheaf.stalk ((𝟭 (Presheaf C X)).obj 𝓕) p₀) ≫
            eqToHom
              (_ :
                (Presheaf.stalkFunctor C p₀).obj 𝓕 =
                  if p₀ ∈ (op U).unop then (Presheaf.stalkFunctor C p₀).obj 𝓕 else ⊤_ C)
      else
        IsTerminal.from
          ((_ : (⊤_ C) = if p₀ ∈ (op U).unop then (Presheaf.stalkFunctor C p₀).obj 𝓕 else ⊤_ C) ▸ terminalIsTerminal)
          (𝓕.obj (op U))) ≫
      if h : p₀ ∈ (op U).unop then
        eqToHom
            (_ :
              (if p₀ ∈ (op U).unop then (Presheaf.stalkFunctor C p₀).obj 𝓕 else ⊤_ C) =
                (Presheaf.stalkFunctor C p₀).obj 𝓕) ≫
          α ≫ eqToHom (_ : c = if p₀ ∈ (op U).unop then c else ⊤_ C)
      else
        IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ (op U).unop then c else ⊤_ C) ▸ terminalIsTerminal)
          ((skyscraperPresheaf p₀ ((Presheaf.stalkFunctor C p₀).obj 𝓕)).obj (op U))
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
α : (Presheaf.stalkFunctor C p₀).obj 𝓕 ⟶ c
U : Opens ↑X
h : p₀ ∈ (op U).unop
⊢ Presheaf.germ 𝓕 { val := p₀, property := (_ : p₀ ∈ (op U).unop) } ≫
      α ≫ eqToHom (_ : c = if p₀ ∈ (op U).unop then c else ⊤_ C) =
    (Presheaf.germ 𝓕 { val := p₀, property := (_ : p₀ ∈ (op U).unop) } ≫
        𝟙 (Presheaf.stalk ((𝟭 (Presheaf C X)).obj 𝓕) p₀) ≫
          eqToHom
            (_ :
              (Presheaf.stalkFunctor C p₀).obj 𝓕 =
                if p₀ ∈ (op U).unop then (Presheaf.stalkFunctor C p₀).obj 𝓕 else ⊤_ C)) ≫
      eqToHom
          (_ :
            (if p₀ ∈ (op U).unop then (Presheaf.stalkFunctor C p₀).obj 𝓕 else ⊤_ C) =
              (Presheaf.stalkFunctor C p₀).obj 𝓕) ≫
        α ≫ eqToHom (_ : c = if p₀ ∈ (op U).unop then c else ⊤_ C)
[PROOFSTEP]
erw [Category.id_comp, ← Category.assoc, comp_eqToHom_iff, Category.assoc, Category.assoc, Category.assoc,
  Category.assoc, eqToHom_trans, eqToHom_refl, Category.comp_id, ← Category.assoc _ _ α, eqToHom_trans, eqToHom_refl,
  Category.id_comp]
[GOAL]
case neg
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
α : (Presheaf.stalkFunctor C p₀).obj 𝓕 ⟶ c
U : Opens ↑X
h : ¬p₀ ∈ (op U).unop
⊢ IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ (op U).unop then c else ⊤_ C) ▸ terminalIsTerminal) (𝓕.obj (op U)) =
    IsTerminal.from
        ((_ : (⊤_ C) = if p₀ ∈ (op U).unop then (Presheaf.stalkFunctor C p₀).obj 𝓕 else ⊤_ C) ▸ terminalIsTerminal)
        (𝓕.obj (op U)) ≫
      IsTerminal.from ((_ : (⊤_ C) = if p₀ ∈ (op U).unop then c else ⊤_ C) ▸ terminalIsTerminal)
        ((skyscraperPresheaf p₀ ((Presheaf.stalkFunctor C p₀).obj 𝓕)).obj (op U))
[PROOFSTEP]
apply ((if_neg h).symm.ndrec terminalIsTerminal).hom_ext
[GOAL]
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
α : 𝓕 ⟶ (skyscraperPresheafFunctor p₀).obj c
⊢ ↑((fun c 𝓕 =>
              { toFun := toSkyscraperPresheaf p₀, invFun := fromStalk p₀,
                left_inv := (_ : ∀ (f : Presheaf.stalk c p₀ ⟶ 𝓕), fromStalk p₀ (toSkyscraperPresheaf p₀ f) = f),
                right_inv := (_ : ∀ (f : c ⟶ skyscraperPresheaf p₀ 𝓕), toSkyscraperPresheaf p₀ (fromStalk p₀ f) = f) })
            𝓕 c).symm
      α =
    (Presheaf.stalkFunctor C p₀).map α ≫ NatTrans.app (StalkSkyscraperPresheafAdjunctionAuxs.counit p₀) c
[PROOFSTEP]
dsimp
[GOAL]
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
α : 𝓕 ⟶ (skyscraperPresheafFunctor p₀).obj c
⊢ fromStalk p₀ α = (Presheaf.stalkFunctor C p₀).map α ≫ (skyscraperPresheafStalkOfSpecializes p₀ c (_ : p₀ ⤳ p₀)).hom
[PROOFSTEP]
ext U
[GOAL]
case ih
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
α : 𝓕 ⟶ (skyscraperPresheafFunctor p₀).obj c
U : Opens ↑X
hxU✝ : p₀ ∈ U
⊢ Presheaf.germ 𝓕 { val := p₀, property := hxU✝ } ≫ fromStalk p₀ α =
    Presheaf.germ 𝓕 { val := p₀, property := hxU✝ } ≫
      (Presheaf.stalkFunctor C p₀).map α ≫ (skyscraperPresheafStalkOfSpecializes p₀ c (_ : p₀ ⤳ p₀)).hom
[PROOFSTEP]
simp only [Equiv.coe_fn_symm_mk, counit_app]
[GOAL]
case ih
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
α : 𝓕 ⟶ (skyscraperPresheafFunctor p₀).obj c
U : Opens ↑X
hxU✝ : p₀ ∈ U
⊢ Presheaf.germ 𝓕 { val := p₀, property := hxU✝ } ≫ fromStalk p₀ α =
    Presheaf.germ 𝓕 { val := p₀, property := hxU✝ } ≫
      (Presheaf.stalkFunctor C p₀).map α ≫ (skyscraperPresheafStalkOfSpecializes p₀ c (_ : p₀ ⤳ p₀)).hom
[PROOFSTEP]
erw [colimit.ι_desc, ← Category.assoc, colimit.ι_map, whiskerLeft_app, Category.assoc, colimit.ι_desc]
[GOAL]
case ih
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
α : 𝓕 ⟶ (skyscraperPresheafFunctor p₀).obj c
U : Opens ↑X
hxU✝ : p₀ ∈ U
⊢ NatTrans.app
      { pt := c,
          ι :=
            NatTrans.mk fun U =>
              NatTrans.app α (op U.unop.obj) ≫ eqToHom (_ : (if p₀ ∈ U.unop.obj then c else ⊤_ C) = c) }.ι
      (op { obj := U, property := (_ : ↑{ val := p₀, property := hxU✝ } ∈ U) }) =
    NatTrans.app α
        ((OpenNhds.inclusion p₀).op.obj (op { obj := U, property := (_ : ↑{ val := p₀, property := hxU✝ } ∈ U) })) ≫
      NatTrans.app
        { cocone := skyscraperPresheafCoconeOfSpecializes p₀ c (_ : p₀ ⤳ p₀),
              isColimit := skyscraperPresheafCoconeIsColimitOfSpecializes p₀ c (_ : p₀ ⤳ p₀) }.cocone.ι
        (op { obj := U, property := (_ : ↑{ val := p₀, property := hxU✝ } ∈ U) })
[PROOFSTEP]
rfl
[GOAL]
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓐 𝓑 : TopCat.Sheaf C X
f : 𝓐 ⟶ 𝓑
⊢ ((𝟭 (TopCat.Sheaf C X)).map f ≫
        (fun 𝓕 => { val := NatTrans.app (StalkSkyscraperPresheafAdjunctionAuxs.unit p₀) 𝓕.val }) 𝓑).val =
    ((fun 𝓕 => { val := NatTrans.app (StalkSkyscraperPresheafAdjunctionAuxs.unit p₀) 𝓕.val }) 𝓐 ≫
        ((Sheaf.forget C X ⋙ Presheaf.stalkFunctor C p₀) ⋙ skyscraperSheafFunctor p₀).map f).val
[PROOFSTEP]
apply (StalkSkyscraperPresheafAdjunctionAuxs.unit p₀).naturality


[GOAL]
X : Type u_1
M : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
f : C(X, Mˣ)
⊢ (fun f =>
        mk fun x =>
          { val := ↑↑f x, inv := ↑↑f⁻¹ x, val_inv := (_ : ↑(↑f * ↑f⁻¹) x = ↑1 x),
            inv_val := (_ : ↑(↑f⁻¹ * ↑f) x = ↑1 x) })
      ((fun f =>
          { val := mk fun x => ↑(↑f x), inv := mk fun x => ↑(↑f x)⁻¹,
            val_inv := (_ : ((mk fun x => ↑(↑f x)) * mk fun x => ↑(↑f x)⁻¹) = 1),
            inv_val := (_ : ((mk fun x => ↑(↑f x)⁻¹) * mk fun x => ↑(↑f x)) = 1) })
        f) =
    f
[PROOFSTEP]
ext
[GOAL]
case h.a
X : Type u_1
M : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
f : C(X, Mˣ)
a✝ : X
⊢ ↑(↑((fun f =>
              mk fun x =>
                { val := ↑↑f x, inv := ↑↑f⁻¹ x, val_inv := (_ : ↑(↑f * ↑f⁻¹) x = ↑1 x),
                  inv_val := (_ : ↑(↑f⁻¹ * ↑f) x = ↑1 x) })
            ((fun f =>
                { val := mk fun x => ↑(↑f x), inv := mk fun x => ↑(↑f x)⁻¹,
                  val_inv := (_ : ((mk fun x => ↑(↑f x)) * mk fun x => ↑(↑f x)⁻¹) = 1),
                  inv_val := (_ : ((mk fun x => ↑(↑f x)⁻¹) * mk fun x => ↑(↑f x)) = 1) })
              f))
        a✝) =
    ↑(↑f a✝)
[PROOFSTEP]
rfl
[GOAL]
X : Type u_1
M : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
f : C(X, M)ˣ
⊢ (fun f =>
        { val := mk fun x => ↑(↑f x), inv := mk fun x => ↑(↑f x)⁻¹,
          val_inv := (_ : ((mk fun x => ↑(↑f x)) * mk fun x => ↑(↑f x)⁻¹) = 1),
          inv_val := (_ : ((mk fun x => ↑(↑f x)⁻¹) * mk fun x => ↑(↑f x)) = 1) })
      ((fun f =>
          mk fun x =>
            { val := ↑↑f x, inv := ↑↑f⁻¹ x, val_inv := (_ : ↑(↑f * ↑f⁻¹) x = ↑1 x),
              inv_val := (_ : ↑(↑f⁻¹ * ↑f) x = ↑1 x) })
        f) =
    f
[PROOFSTEP]
ext
[GOAL]
case a.h
X : Type u_1
M : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
f : C(X, M)ˣ
a✝ : X
⊢ ↑↑((fun f =>
              { val := mk fun x => ↑(↑f x), inv := mk fun x => ↑(↑f x)⁻¹,
                val_inv := (_ : ((mk fun x => ↑(↑f x)) * mk fun x => ↑(↑f x)⁻¹) = 1),
                inv_val := (_ : ((mk fun x => ↑(↑f x)⁻¹) * mk fun x => ↑(↑f x)) = 1) })
            ((fun f =>
                mk fun x =>
                  { val := ↑↑f x, inv := ↑↑f⁻¹ x, val_inv := (_ : ↑(↑f * ↑f⁻¹) x = ↑1 x),
                    inv_val := (_ : ↑(↑f⁻¹ * ↑f) x = ↑1 x) })
              f))
      a✝ =
    ↑↑f a✝
[PROOFSTEP]
rfl
[GOAL]
X : Type u_1
M : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
f : C(X, M)ˣ
x : X
⊢ ↑(↑(↑unitsLift.symm f) x)⁻¹ = ↑↑f⁻¹ x
[PROOFSTEP]
rfl
[GOAL]
X : Type u_1
M : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (↑f x)
⊢ Continuous fun x => IsUnit.unit (_ : IsUnit (↑f x))
[PROOFSTEP]
refine'
  continuous_induced_rng.2
    (Continuous.prod_mk f.continuous (MulOpposite.continuous_op.comp (continuous_iff_continuousAt.mpr fun x => _)))
[GOAL]
X : Type u_1
M : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (↑f x)
x : X
⊢ ContinuousAt (fun x => ↑((fun x => IsUnit.unit (_ : IsUnit (↑f x))) x)⁻¹) x
[PROOFSTEP]
have := NormedRing.inverse_continuousAt (h x).unit
[GOAL]
X : Type u_1
M : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (↑f x)
x : X
this : ContinuousAt Ring.inverse ↑(IsUnit.unit (_ : IsUnit (↑f x)))
⊢ ContinuousAt (fun x => ↑((fun x => IsUnit.unit (_ : IsUnit (↑f x))) x)⁻¹) x
[PROOFSTEP]
simp only
[GOAL]
X : Type u_1
M : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (↑f x)
x : X
this : ContinuousAt Ring.inverse ↑(IsUnit.unit (_ : IsUnit (↑f x)))
⊢ ContinuousAt (fun x => ↑(IsUnit.unit (_ : IsUnit (↑f x)))⁻¹) x
[PROOFSTEP]
simp only [← Ring.inverse_unit, IsUnit.unit_spec] at this ⊢
[GOAL]
X : Type u_1
M : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (↑f x)
x : X
this : ContinuousAt Ring.inverse (↑f x)
⊢ ContinuousAt (fun x => Ring.inverse (↑f x)) x
[PROOFSTEP]
exact this.comp (f.continuousAt x)
[GOAL]
X : Type u_1
M : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (↑f x)
⊢ (mk fun x => ↑(↑(unitsOfForallIsUnit h) x)) = f
[PROOFSTEP]
ext
[GOAL]
case h
X : Type u_1
M : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (↑f x)
a✝ : X
⊢ ↑(mk fun x => ↑(↑(unitsOfForallIsUnit h) x)) a✝ = ↑f a✝
[PROOFSTEP]
rfl
[GOAL]
X : Type u_1
M : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (↑f x)
⊢ ↑(↑unitsLift (unitsOfForallIsUnit h)) = f
[PROOFSTEP]
ext
[GOAL]
case h
X : Type u_1
M : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (↑f x)
a✝ : X
⊢ ↑↑(↑unitsLift (unitsOfForallIsUnit h)) a✝ = ↑f a✝
[PROOFSTEP]
rfl
[GOAL]
X : Type u_1
M : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
f : C(X, 𝕜)
⊢ IsUnit f ↔ ∀ (x : X), ↑f x ≠ 0
[PROOFSTEP]
simp_rw [f.isUnit_iff_forall_isUnit, isUnit_iff_ne_zero]
[GOAL]
X : Type u_1
M : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
f : C(X, 𝕜)
⊢ spectrum 𝕜 f = Set.range ↑f
[PROOFSTEP]
ext x
[GOAL]
case h
X : Type u_1
M : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
f : C(X, 𝕜)
x : 𝕜
⊢ x ∈ spectrum 𝕜 f ↔ x ∈ Set.range ↑f
[PROOFSTEP]
simp only [spectrum.mem_iff, isUnit_iff_forall_ne_zero, not_forall, coe_sub, Pi.sub_apply, algebraMap_apply,
  Algebra.id.smul_eq_mul, mul_one, Classical.not_not, Set.mem_range, sub_eq_zero, @eq_comm _ x _]