[GOAL]
X : Type u_1
s : Set X
⊢ (some '' s)ᶜ = some '' sᶜ ∪ {∞}
[PROOFSTEP]
rw [coe_injective.compl_image_eq, compl_range_coe]
[GOAL]
X : Type u_1
x : OnePoint X
⊢ x ≠ ∞ ↔ ∃ y, ↑y = x
[PROOFSTEP]
induction x using OnePoint.rec
[GOAL]
case h₁
X : Type u_1
⊢ ∞ ≠ ∞ ↔ ∃ y, ↑y = ∞
[PROOFSTEP]
simp
[GOAL]
case h₂
X : Type u_1
x✝ : X
⊢ ↑x✝ ≠ ∞ ↔ ∃ y, ↑y = ↑x✝
[PROOFSTEP]
simp
[GOAL]
X : Type u_1
x : OnePoint X
⊢ ¬x ∈ range some ↔ x = ∞
[PROOFSTEP]
rw [← mem_compl_iff, compl_range_coe, mem_singleton_iff]
[GOAL]
X : Type u_1
⊢ some ⁻¹' {∞} = ∅
[PROOFSTEP]
ext
[GOAL]
case h
X : Type u_1
x✝ : X
⊢ x✝ ∈ some ⁻¹' {∞} ↔ x✝ ∈ ∅
[PROOFSTEP]
simp
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
⊢ (fun s => (∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ) ∧ IsOpen (some ⁻¹' s)) univ
[PROOFSTEP]
simp
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set (OnePoint X)
⊢ (fun s => (∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ) ∧ IsOpen (some ⁻¹' s)) s →
    (fun s => (∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ) ∧ IsOpen (some ⁻¹' s)) t →
      (fun s => (∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ) ∧ IsOpen (some ⁻¹' s)) (s ∩ t)
[PROOFSTEP]
rintro ⟨hms, hs⟩ ⟨hmt, ht⟩
[GOAL]
case intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set (OnePoint X)
hms : ∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ
hs : IsOpen (some ⁻¹' s)
hmt : ∞ ∈ t → IsCompact (some ⁻¹' t)ᶜ
ht : IsOpen (some ⁻¹' t)
⊢ (∞ ∈ s ∩ t → IsCompact (some ⁻¹' (s ∩ t))ᶜ) ∧ IsOpen (some ⁻¹' (s ∩ t))
[PROOFSTEP]
refine' ⟨_, hs.inter ht⟩
[GOAL]
case intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set (OnePoint X)
hms : ∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ
hs : IsOpen (some ⁻¹' s)
hmt : ∞ ∈ t → IsCompact (some ⁻¹' t)ᶜ
ht : IsOpen (some ⁻¹' t)
⊢ ∞ ∈ s ∩ t → IsCompact (some ⁻¹' (s ∩ t))ᶜ
[PROOFSTEP]
rintro ⟨hms', hmt'⟩
[GOAL]
case intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set (OnePoint X)
hms : ∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ
hs : IsOpen (some ⁻¹' s)
hmt : ∞ ∈ t → IsCompact (some ⁻¹' t)ᶜ
ht : IsOpen (some ⁻¹' t)
hms' : ∞ ∈ s
hmt' : ∞ ∈ t
⊢ IsCompact (some ⁻¹' (s ∩ t))ᶜ
[PROOFSTEP]
simpa [compl_inter] using (hms hms').union (hmt hmt')
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set (OnePoint X))
ho : ∀ (t : Set (OnePoint X)), t ∈ S → (fun s => (∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ) ∧ IsOpen (some ⁻¹' s)) t
⊢ (fun s => (∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ) ∧ IsOpen (some ⁻¹' s)) (⋃₀ S)
[PROOFSTEP]
suffices IsOpen ((↑) ⁻¹' ⋃₀ S : Set X) by
  refine' ⟨_, this⟩
  rintro ⟨s, hsS : s ∈ S, hs : ∞ ∈ s⟩
  refine' isCompact_of_isClosed_subset ((ho s hsS).1 hs) this.isClosed_compl _
  exact compl_subset_compl.mpr (preimage_mono <| subset_sUnion_of_mem hsS)
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set (OnePoint X))
ho : ∀ (t : Set (OnePoint X)), t ∈ S → (fun s => (∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ) ∧ IsOpen (some ⁻¹' s)) t
this : IsOpen (some ⁻¹' ⋃₀ S)
⊢ (fun s => (∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ) ∧ IsOpen (some ⁻¹' s)) (⋃₀ S)
[PROOFSTEP]
refine' ⟨_, this⟩
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set (OnePoint X))
ho : ∀ (t : Set (OnePoint X)), t ∈ S → (fun s => (∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ) ∧ IsOpen (some ⁻¹' s)) t
this : IsOpen (some ⁻¹' ⋃₀ S)
⊢ ∞ ∈ ⋃₀ S → IsCompact (some ⁻¹' ⋃₀ S)ᶜ
[PROOFSTEP]
rintro ⟨s, hsS : s ∈ S, hs : ∞ ∈ s⟩
[GOAL]
case intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set (OnePoint X))
ho : ∀ (t : Set (OnePoint X)), t ∈ S → (fun s => (∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ) ∧ IsOpen (some ⁻¹' s)) t
this : IsOpen (some ⁻¹' ⋃₀ S)
s : Set (OnePoint X)
hsS : s ∈ S
hs : ∞ ∈ s
⊢ IsCompact (some ⁻¹' ⋃₀ S)ᶜ
[PROOFSTEP]
refine' isCompact_of_isClosed_subset ((ho s hsS).1 hs) this.isClosed_compl _
[GOAL]
case intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set (OnePoint X))
ho : ∀ (t : Set (OnePoint X)), t ∈ S → (fun s => (∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ) ∧ IsOpen (some ⁻¹' s)) t
this : IsOpen (some ⁻¹' ⋃₀ S)
s : Set (OnePoint X)
hsS : s ∈ S
hs : ∞ ∈ s
⊢ (some ⁻¹' ⋃₀ S)ᶜ ⊆ (some ⁻¹' s)ᶜ
[PROOFSTEP]
exact compl_subset_compl.mpr (preimage_mono <| subset_sUnion_of_mem hsS)
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set (OnePoint X))
ho : ∀ (t : Set (OnePoint X)), t ∈ S → (fun s => (∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ) ∧ IsOpen (some ⁻¹' s)) t
⊢ IsOpen (some ⁻¹' ⋃₀ S)
[PROOFSTEP]
rw [preimage_sUnion]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set (OnePoint X))
ho : ∀ (t : Set (OnePoint X)), t ∈ S → (fun s => (∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ) ∧ IsOpen (some ⁻¹' s)) t
⊢ IsOpen (⋃ (t : Set (OnePoint X)) (_ : t ∈ S), some ⁻¹' t)
[PROOFSTEP]
exact isOpen_biUnion fun s hs => (ho s hs).2
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
h : ∞ ∈ s
⊢ IsOpen s ↔ IsCompact (some ⁻¹' s)ᶜ ∧ IsOpen (some ⁻¹' s)
[PROOFSTEP]
simp [isOpen_def, h]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
h : ∞ ∈ s
⊢ IsOpen s ↔ IsClosed (some ⁻¹' s)ᶜ ∧ IsCompact (some ⁻¹' s)ᶜ
[PROOFSTEP]
simp only [isOpen_iff_of_mem' h, isClosed_compl_iff, and_comm]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
h : ¬∞ ∈ s
⊢ IsOpen s ↔ IsOpen (some ⁻¹' s)
[PROOFSTEP]
simp [isOpen_def, h]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
h : ∞ ∈ s
⊢ IsClosed s ↔ IsClosed (some ⁻¹' s)
[PROOFSTEP]
have : ∞ ∉ sᶜ := fun H => H h
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
h : ∞ ∈ s
this : ¬∞ ∈ sᶜ
⊢ IsClosed s ↔ IsClosed (some ⁻¹' s)
[PROOFSTEP]
rw [← isOpen_compl_iff, isOpen_iff_of_not_mem this, ← isOpen_compl_iff, preimage_compl]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
h : ¬∞ ∈ s
⊢ IsClosed s ↔ IsClosed (some ⁻¹' s) ∧ IsCompact (some ⁻¹' s)
[PROOFSTEP]
rw [← isOpen_compl_iff, isOpen_iff_of_mem (mem_compl h), ← preimage_compl, compl_compl]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s✝ : Set (OnePoint X)
t s : Set X
⊢ IsOpen (some '' s) ↔ IsOpen s
[PROOFSTEP]
rw [isOpen_iff_of_not_mem infty_not_mem_image_coe, preimage_image_eq _ coe_injective]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s✝ : Set (OnePoint X)
t s : Set X
⊢ IsOpen (some '' s)ᶜ ↔ IsClosed s ∧ IsCompact s
[PROOFSTEP]
rw [isOpen_iff_of_mem, ← preimage_compl, compl_compl, preimage_image_eq _ coe_injective]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s✝ : Set (OnePoint X)
t s : Set X
⊢ ∞ ∈ (some '' s)ᶜ
[PROOFSTEP]
exact infty_not_mem_image_coe
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s✝ : Set (OnePoint X)
t s : Set X
⊢ IsClosed (some '' s) ↔ IsClosed s ∧ IsCompact s
[PROOFSTEP]
rw [← isOpen_compl_iff, isOpen_compl_image_coe]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
⊢ IsClosed {∞}
[PROOFSTEP]
rw [← compl_range_coe, isClosed_compl_iff]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
⊢ IsOpen (range some)
[PROOFSTEP]
exact isOpen_range_coe
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
x : X
h : NeBot (𝓝[{x}ᶜ] x)
⊢ NeBot (𝓝[{↑x}ᶜ] ↑x)
[PROOFSTEP]
simpa [nhdsWithin_coe, preimage, coe_eq_coe] using h.map some
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
⊢ 𝓝[{∞}ᶜ] ∞ = map some (coclosedCompact X)
[PROOFSTEP]
refine' (nhdsWithin_basis_open ∞ _).ext (hasBasis_coclosedCompact.map _) _ _
[GOAL]
case refine'_1
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
⊢ ∀ (i : Set (OnePoint X)), ∞ ∈ i ∧ IsOpen i → ∃ i', (IsClosed i' ∧ IsCompact i') ∧ some '' i'ᶜ ⊆ i ∩ {∞}ᶜ
[PROOFSTEP]
rintro s ⟨hs, hso⟩
[GOAL]
case refine'_1.intro
X : Type u_1
inst✝ : TopologicalSpace X
s✝ : Set (OnePoint X)
t : Set X
s : Set (OnePoint X)
hs : ∞ ∈ s
hso : IsOpen s
⊢ ∃ i', (IsClosed i' ∧ IsCompact i') ∧ some '' i'ᶜ ⊆ s ∩ {∞}ᶜ
[PROOFSTEP]
refine' ⟨_, (isOpen_iff_of_mem hs).mp hso, _⟩
[GOAL]
case refine'_1.intro
X : Type u_1
inst✝ : TopologicalSpace X
s✝ : Set (OnePoint X)
t : Set X
s : Set (OnePoint X)
hs : ∞ ∈ s
hso : IsOpen s
⊢ some '' (some ⁻¹' s)ᶜᶜ ⊆ s ∩ {∞}ᶜ
[PROOFSTEP]
simp [Subset.rfl]
[GOAL]
case refine'_2
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
⊢ ∀ (i' : Set X), IsClosed i' ∧ IsCompact i' → ∃ i, (∞ ∈ i ∧ IsOpen i) ∧ i ∩ {∞}ᶜ ⊆ some '' i'ᶜ
[PROOFSTEP]
rintro s ⟨h₁, h₂⟩
[GOAL]
case refine'_2.intro
X : Type u_1
inst✝ : TopologicalSpace X
s✝ : Set (OnePoint X)
t s : Set X
h₁ : IsClosed s
h₂ : IsCompact s
⊢ ∃ i, (∞ ∈ i ∧ IsOpen i) ∧ i ∩ {∞}ᶜ ⊆ some '' sᶜ
[PROOFSTEP]
refine' ⟨_, ⟨mem_compl infty_not_mem_image_coe, isOpen_compl_image_coe.2 ⟨h₁, h₂⟩⟩, _⟩
[GOAL]
case refine'_2.intro
X : Type u_1
inst✝ : TopologicalSpace X
s✝ : Set (OnePoint X)
t s : Set X
h₁ : IsClosed s
h₂ : IsCompact s
⊢ (some '' s)ᶜ ∩ {∞}ᶜ ⊆ some '' sᶜ
[PROOFSTEP]
simp [compl_image_coe, ← diff_eq, subset_preimage_image]
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝ : NoncompactSpace X
⊢ NeBot (𝓝[{∞}ᶜ] ∞)
[PROOFSTEP]
rw [nhdsWithin_compl_infty_eq]
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝ : NoncompactSpace X
⊢ NeBot (map some (coclosedCompact X))
[PROOFSTEP]
infer_instance
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
⊢ 𝓝 ∞ = map some (coclosedCompact X) ⊔ pure ∞
[PROOFSTEP]
rw [← nhdsWithin_compl_infty_eq, nhdsWithin_compl_singleton_sup_pure]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
⊢ HasBasis (𝓝 ∞) (fun s => IsClosed s ∧ IsCompact s) fun s => some '' sᶜ ∪ {∞}
[PROOFSTEP]
rw [nhds_infty_eq]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
⊢ HasBasis (map some (coclosedCompact X) ⊔ pure ∞) (fun s => IsClosed s ∧ IsCompact s) fun s => some '' sᶜ ∪ {∞}
[PROOFSTEP]
exact (hasBasis_coclosedCompact.map _).sup_pure _
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
⊢ comap some (𝓝 ∞) = coclosedCompact X
[PROOFSTEP]
simp [nhds_infty_eq, comap_sup, comap_map coe_injective]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
f : Filter (OnePoint X)
⊢ f ≤ 𝓝 ∞ ↔ ∀ (s : Set X), IsClosed s → IsCompact s → some '' sᶜ ∪ {∞} ∈ f
[PROOFSTEP]
simp only [hasBasis_nhds_infty.ge_iff, and_imp]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
f : Ultrafilter (OnePoint X)
⊢ ↑f ≤ 𝓝 ∞ ↔ ∀ (s : Set X), IsClosed s → IsCompact s → ¬some '' s ∈ f
[PROOFSTEP]
simp only [le_nhds_infty, ← compl_image_coe, Ultrafilter.mem_coe, Ultrafilter.compl_mem_iff_not_mem]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
α : Type u_2
f : OnePoint X → α
l : Filter α
⊢ Tendsto f (𝓝 ∞) l ↔ Tendsto f (pure ∞) l ∧ Tendsto (f ∘ some) (coclosedCompact X) l
[PROOFSTEP]
simp [nhds_infty_eq, and_comm]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
α : Type u_2
f : OnePoint X → α
l : Filter α
⊢ Tendsto f (pure ∞) l ∧ Tendsto (f ∘ some) (coclosedCompact X) l ↔
    ∀ (s : Set α), s ∈ l → f ∞ ∈ s ∧ ∃ t, IsClosed t ∧ IsCompact t ∧ MapsTo (f ∘ some) tᶜ s
[PROOFSTEP]
simp only [tendsto_pure_left, hasBasis_coclosedCompact.tendsto_left_iff, forall_and, and_assoc, exists_prop]
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
Y : Type u_2
inst✝ : TopologicalSpace Y
f : OnePoint X → Y
⊢ Tendsto (f ∘ some) (coclosedCompact X) (𝓝 (f ∞)) ↔
    ∀ (s : Set Y), s ∈ 𝓝 (f ∞) → ∃ t, IsClosed t ∧ IsCompact t ∧ MapsTo (f ∘ some) tᶜ s
[PROOFSTEP]
simp only [hasBasis_coclosedCompact.tendsto_left_iff, and_assoc]
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
Y : Type u_2
inst✝ : TopologicalSpace Y
f : OnePoint X → Y
x : X
⊢ ContinuousAt f ↑x ↔ ContinuousAt (f ∘ some) x
[PROOFSTEP]
rw [ContinuousAt, nhds_coe_eq, tendsto_map'_iff, ContinuousAt]
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
Y : Type u_2
inst✝ : TopologicalSpace Y
f : OnePoint X → Y
x : X
⊢ Tendsto (f ∘ some) (𝓝 x) (𝓝 (f ↑x)) ↔ Tendsto (f ∘ some) (𝓝 x) (𝓝 ((f ∘ some) x))
[PROOFSTEP]
rfl
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝ : NoncompactSpace X
⊢ DenseRange some
[PROOFSTEP]
rw [DenseRange, ← compl_infty]
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝ : NoncompactSpace X
⊢ Dense {∞}ᶜ
[PROOFSTEP]
exact dense_compl_singleton _
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
x y : OnePoint X
⊢ Inseparable x y ↔ x = ∞ ∧ y = ∞ ∨ ∃ x', x = ↑x' ∧ ∃ y', y = ↑y' ∧ Inseparable x' y'
[PROOFSTEP]
induction x using OnePoint.rec
[GOAL]
case h₁
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
y : OnePoint X
⊢ Inseparable ∞ y ↔ ∞ = ∞ ∧ y = ∞ ∨ ∃ x', ∞ = ↑x' ∧ ∃ y', y = ↑y' ∧ Inseparable x' y'
[PROOFSTEP]
induction y using OnePoint.rec
[GOAL]
case h₂
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
y : OnePoint X
x✝ : X
⊢ Inseparable (↑x✝) y ↔ ↑x✝ = ∞ ∧ y = ∞ ∨ ∃ x', ↑x✝ = ↑x' ∧ ∃ y', y = ↑y' ∧ Inseparable x' y'
[PROOFSTEP]
induction y using OnePoint.rec
[GOAL]
case h₁.h₁
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
⊢ Inseparable ∞ ∞ ↔ ∞ = ∞ ∧ ∞ = ∞ ∨ ∃ x', ∞ = ↑x' ∧ ∃ y', ∞ = ↑y' ∧ Inseparable x' y'
[PROOFSTEP]
simp [not_inseparable_infty_coe, not_inseparable_coe_infty, coe_eq_coe, Inseparable.refl]
[GOAL]
case h₁.h₂
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
x✝ : X
⊢ Inseparable ∞ ↑x✝ ↔ ∞ = ∞ ∧ ↑x✝ = ∞ ∨ ∃ x', ∞ = ↑x' ∧ ∃ y', ↑x✝ = ↑y' ∧ Inseparable x' y'
[PROOFSTEP]
simp [not_inseparable_infty_coe, not_inseparable_coe_infty, coe_eq_coe, Inseparable.refl]
[GOAL]
case h₂.h₁
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
x✝ : X
⊢ Inseparable ↑x✝ ∞ ↔ ↑x✝ = ∞ ∧ ∞ = ∞ ∨ ∃ x', ↑x✝ = ↑x' ∧ ∃ y', ∞ = ↑y' ∧ Inseparable x' y'
[PROOFSTEP]
simp [not_inseparable_infty_coe, not_inseparable_coe_infty, coe_eq_coe, Inseparable.refl]
[GOAL]
case h₂.h₂
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
x✝¹ x✝ : X
⊢ Inseparable ↑x✝¹ ↑x✝ ↔ ↑x✝¹ = ∞ ∧ ↑x✝ = ∞ ∨ ∃ x', ↑x✝¹ = ↑x' ∧ ∃ y', ↑x✝ = ↑y' ∧ Inseparable x' y'
[PROOFSTEP]
simp [not_inseparable_infty_coe, not_inseparable_coe_infty, coe_eq_coe, Inseparable.refl]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
⊢ IsCompact univ
[PROOFSTEP]
have : Tendsto ((↑) : X → OnePoint X) (cocompact X) (𝓝 ∞) :=
  by
  rw [nhds_infty_eq]
  exact (tendsto_map.mono_left cocompact_le_coclosedCompact).mono_right le_sup_left
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
⊢ Tendsto some (cocompact X) (𝓝 ∞)
[PROOFSTEP]
rw [nhds_infty_eq]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
⊢ Tendsto some (cocompact X) (map some (coclosedCompact X) ⊔ pure ∞)
[PROOFSTEP]
exact (tendsto_map.mono_left cocompact_le_coclosedCompact).mono_right le_sup_left
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
this : Tendsto some (cocompact X) (𝓝 ∞)
⊢ IsCompact univ
[PROOFSTEP]
rw [← insert_none_range_some X]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
this : Tendsto some (cocompact X) (𝓝 ∞)
⊢ IsCompact (insert none (range Option.some))
[PROOFSTEP]
exact this.isCompact_insert_range_of_cocompact continuous_coe
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝ : T0Space X
⊢ T0Space (OnePoint X)
[PROOFSTEP]
refine' ⟨fun x y hxy => _⟩
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝ : T0Space X
x y : OnePoint X
hxy : Inseparable x y
⊢ x = y
[PROOFSTEP]
rcases inseparable_iff.1 hxy with (⟨rfl, rfl⟩ | ⟨x, rfl, y, rfl, h⟩)
[GOAL]
case inl.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝ : T0Space X
hxy : Inseparable ∞ ∞
⊢ ∞ = ∞
case inr.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝ : T0Space X
x y : X
h : Inseparable x y
hxy : Inseparable ↑x ↑y
⊢ ↑x = ↑y
[PROOFSTEP]
exacts [rfl, congr_arg some h.eq]
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝ : T1Space X
z : OnePoint X
⊢ IsClosed {z}
[PROOFSTEP]
induction z using OnePoint.rec
[GOAL]
case h₁
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝ : T1Space X
⊢ IsClosed {∞}
[PROOFSTEP]
exact isClosed_infty
[GOAL]
case h₂
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝ : T1Space X
x✝ : X
⊢ IsClosed {↑x✝}
[PROOFSTEP]
rw [← image_singleton, isClosed_image_coe]
[GOAL]
case h₂
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝ : T1Space X
x✝ : X
⊢ IsClosed {x✝} ∧ IsCompact {x✝}
[PROOFSTEP]
exact ⟨isClosed_singleton, isCompact_singleton⟩
[GOAL]
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
⊢ NormalSpace (OnePoint X)
[PROOFSTEP]
have key : ∀ z : X, Disjoint (𝓝 (some z)) (𝓝 ∞) := fun z =>
  by
  rw [nhds_infty_eq, disjoint_sup_right, nhds_coe_eq, coclosedCompact_eq_cocompact, disjoint_map coe_injective, ←
    principal_singleton, disjoint_principal_right, compl_infty]
  exact ⟨disjoint_nhds_cocompact z, range_mem_map⟩
[GOAL]
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
z : X
⊢ Disjoint (𝓝 ↑z) (𝓝 ∞)
[PROOFSTEP]
rw [nhds_infty_eq, disjoint_sup_right, nhds_coe_eq, coclosedCompact_eq_cocompact, disjoint_map coe_injective, ←
  principal_singleton, disjoint_principal_right, compl_infty]
[GOAL]
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
z : X
⊢ Disjoint (𝓝 z) (cocompact X) ∧ range some ∈ map some (𝓝 z)
[PROOFSTEP]
exact ⟨disjoint_nhds_cocompact z, range_mem_map⟩
[GOAL]
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
⊢ NormalSpace (OnePoint X)
[PROOFSTEP]
suffices : T2Space (OnePoint X)
[GOAL]
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
this : T2Space (OnePoint X)
⊢ NormalSpace (OnePoint X)
case this
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
⊢ T2Space (OnePoint X)
[PROOFSTEP]
exact normalOfCompactT2
[GOAL]
case this
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
⊢ T2Space (OnePoint X)
[PROOFSTEP]
refine t2Space_iff_disjoint_nhds.2 fun x y hxy => ?_
[GOAL]
case this
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
x y : OnePoint X
hxy : x ≠ y
⊢ Disjoint (𝓝 x) (𝓝 y)
[PROOFSTEP]
induction x using OnePoint.rec
[GOAL]
case this.h₁
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
y : OnePoint X
hxy : ∞ ≠ y
⊢ Disjoint (𝓝 ∞) (𝓝 y)
[PROOFSTEP]
induction y using OnePoint.rec
[GOAL]
case this.h₂
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
y : OnePoint X
x✝ : X
hxy : ↑x✝ ≠ y
⊢ Disjoint (𝓝 ↑x✝) (𝓝 y)
[PROOFSTEP]
induction y using OnePoint.rec
[GOAL]
case this.h₁.h₁
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
hxy : ∞ ≠ ∞
⊢ Disjoint (𝓝 ∞) (𝓝 ∞)
[PROOFSTEP]
exact (hxy rfl).elim
[GOAL]
case this.h₁.h₂
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
x✝ : X
hxy : ∞ ≠ ↑x✝
⊢ Disjoint (𝓝 ∞) (𝓝 ↑x✝)
[PROOFSTEP]
exact (key _).symm
[GOAL]
case this.h₂.h₁
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
x✝ : X
hxy : ↑x✝ ≠ ∞
⊢ Disjoint (𝓝 ↑x✝) (𝓝 ∞)
[PROOFSTEP]
exact key _
[GOAL]
case this.h₂.h₂
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
key : ∀ (z : X), Disjoint (𝓝 ↑z) (𝓝 ∞)
x✝¹ x✝ : X
hxy : ↑x✝¹ ≠ ↑x✝
⊢ Disjoint (𝓝 ↑x✝¹) (𝓝 ↑x✝)
[PROOFSTEP]
rwa [nhds_coe_eq, nhds_coe_eq, disjoint_map coe_injective, disjoint_nhds_nhds, ← coe_injective.ne_iff]
[GOAL]
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : Infinite X
inst✝ : DiscreteTopology X
⊢ ¬Continuous ↑CofiniteTopology.of.symm
[PROOFSTEP]
inhabit X
[GOAL]
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : Infinite X
inst✝ : DiscreteTopology X
inhabited_h : Inhabited X
⊢ ¬Continuous ↑CofiniteTopology.of.symm
[PROOFSTEP]
simp only [continuous_iff_continuousAt, ContinuousAt, not_forall]
[GOAL]
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : Infinite X
inst✝ : DiscreteTopology X
inhabited_h : Inhabited X
⊢ ∃ x, ¬Tendsto (↑CofiniteTopology.of.symm) (𝓝 x) (𝓝 (↑CofiniteTopology.of.symm x))
[PROOFSTEP]
use CofiniteTopology.of ↑(default : X)
[GOAL]
case h
X : Type u_1
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
inst✝¹ : Infinite X
inst✝ : DiscreteTopology X
inhabited_h : Inhabited X
⊢ ¬Tendsto (↑CofiniteTopology.of.symm) (𝓝 (↑CofiniteTopology.of ↑default))
      (𝓝 (↑CofiniteTopology.of.symm (↑CofiniteTopology.of ↑default)))
[PROOFSTEP]
simpa [nhds_coe_eq, nhds_discrete, CofiniteTopology.nhds_eq] using
  (finite_singleton ((default : X) : OnePoint X)).infinite_compl


[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasLimits C
X : TopCat
F : J ⥤ Presheaf C X
H : ∀ (j : J), Presheaf.IsSheaf (F.obj j)
c : Cone F
hc : IsLimit c
⊢ Presheaf.IsSheaf c.pt
[PROOFSTEP]
let F' : J ⥤ Sheaf C X :=
  { obj := fun j => ⟨F.obj j, H j⟩
    map := fun f => ⟨F.map f⟩ }
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasLimits C
X : TopCat
F : J ⥤ Presheaf C X
H : ∀ (j : J), Presheaf.IsSheaf (F.obj j)
c : Cone F
hc : IsLimit c
F' : J ⥤ Sheaf C X :=
  CategoryTheory.Functor.mk
    { obj := fun j => { val := F.obj j, cond := (_ : Presheaf.IsSheaf (F.obj j)) },
      map := fun {X_1 Y} f => { val := F.map f } }
⊢ Presheaf.IsSheaf c.pt
[PROOFSTEP]
let e : F' ⋙ Sheaf.forget C X ≅ F := NatIso.ofComponents fun _ => Iso.refl _
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasLimits C
X : TopCat
F : J ⥤ Presheaf C X
H : ∀ (j : J), Presheaf.IsSheaf (F.obj j)
c : Cone F
hc : IsLimit c
F' : J ⥤ Sheaf C X :=
  CategoryTheory.Functor.mk
    { obj := fun j => { val := F.obj j, cond := (_ : Presheaf.IsSheaf (F.obj j)) },
      map := fun {X_1 Y} f => { val := F.map f } }
e : F' ⋙ Sheaf.forget C X ≅ F := NatIso.ofComponents fun x => Iso.refl ((F' ⋙ Sheaf.forget C X).obj x)
⊢ Presheaf.IsSheaf c.pt
[PROOFSTEP]
exact
  Presheaf.isSheaf_of_iso ((isLimitOfPreserves (Sheaf.forget C X) (limit.isLimit F')).conePointsIsoOfNatIso hc e)
    (limit F').2


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s t : Compacts α
h : s.carrier = t.carrier
⊢ s = t
[PROOFSTEP]
cases s
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
t : Compacts α
carrier✝ : Set α
isCompact'✝ : IsCompact carrier✝
h : { carrier := carrier✝, isCompact' := isCompact'✝ }.carrier = t.carrier
⊢ { carrier := carrier✝, isCompact' := isCompact'✝ } = t
[PROOFSTEP]
cases t
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
carrier✝¹ : Set α
isCompact'✝¹ : IsCompact carrier✝¹
carrier✝ : Set α
isCompact'✝ : IsCompact carrier✝
h :
  { carrier := carrier✝¹, isCompact' := isCompact'✝¹ }.carrier =
    { carrier := carrier✝, isCompact' := isCompact'✝ }.carrier
⊢ { carrier := carrier✝¹, isCompact' := isCompact'✝¹ } = { carrier := carrier✝, isCompact' := isCompact'✝ }
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Type u_4
s : Finset ι
f : ι → Compacts α
⊢ ↑(Finset.sup s f) = Finset.sup s fun i => ↑(f i)
[PROOFSTEP]
refine Finset.cons_induction_on s rfl fun a s _ h => ?_
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Type u_4
s✝ : Finset ι
f : ι → Compacts α
a : ι
s : Finset ι
x✝ : ¬a ∈ s
h : ↑(Finset.sup s f) = Finset.sup s fun i => ↑(f i)
⊢ ↑(Finset.sup (Finset.cons a s x✝) f) = Finset.sup (Finset.cons a s x✝) fun i => ↑(f i)
[PROOFSTEP]
simp_rw [Finset.sup_cons, coe_sup, sup_eq_union]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Type u_4
s✝ : Finset ι
f : ι → Compacts α
a : ι
s : Finset ι
x✝ : ¬a ∈ s
h : ↑(Finset.sup s f) = Finset.sup s fun i => ↑(f i)
⊢ ↑(f a) ∪ ↑(Finset.sup s f) = ↑(f a) ∪ Finset.sup s fun i => ↑(f i)
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α ≃ₜ β
s : Compacts α
⊢ Compacts.map ↑(Homeomorph.symm f) (_ : Continuous ↑(Homeomorph.symm f)) (Compacts.map ↑f (_ : Continuous ↑f) s) = s
[PROOFSTEP]
ext1
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α ≃ₜ β
s : Compacts α
⊢ ↑(Compacts.map ↑(Homeomorph.symm f) (_ : Continuous ↑(Homeomorph.symm f)) (Compacts.map ↑f (_ : Continuous ↑f) s)) =
    ↑s
[PROOFSTEP]
simp only [coe_map, ← image_comp, f.symm_comp_self, image_id]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α ≃ₜ β
s : Compacts β
⊢ Compacts.map ↑f (_ : Continuous ↑f) (Compacts.map ↑(Homeomorph.symm f) (_ : Continuous ↑(Homeomorph.symm f)) s) = s
[PROOFSTEP]
ext1
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α ≃ₜ β
s : Compacts β
⊢ ↑(Compacts.map ↑f (_ : Continuous ↑f) (Compacts.map ↑(Homeomorph.symm f) (_ : Continuous ↑(Homeomorph.symm f)) s)) =
    ↑s
[PROOFSTEP]
simp only [coe_map, ← image_comp, f.self_comp_symm, image_id]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s t : NonemptyCompacts α
h : (fun s => s.carrier) s = (fun s => s.carrier) t
⊢ s = t
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := s
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
t : NonemptyCompacts α
carrier✝ : Set α
isCompact'✝ : IsCompact carrier✝
nonempty'✝ : Set.Nonempty { carrier := carrier✝, isCompact' := isCompact'✝ }.carrier
h :
  (fun s => s.carrier) { toCompacts := { carrier := carrier✝, isCompact' := isCompact'✝ }, nonempty' := nonempty'✝ } =
    (fun s => s.carrier) t
⊢ { toCompacts := { carrier := carrier✝, isCompact' := isCompact'✝ }, nonempty' := nonempty'✝ } = t
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := t
[GOAL]
case mk.mk.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
carrier✝¹ : Set α
isCompact'✝¹ : IsCompact carrier✝¹
nonempty'✝¹ : Set.Nonempty { carrier := carrier✝¹, isCompact' := isCompact'✝¹ }.carrier
carrier✝ : Set α
isCompact'✝ : IsCompact carrier✝
nonempty'✝ : Set.Nonempty { carrier := carrier✝, isCompact' := isCompact'✝ }.carrier
h :
  (fun s => s.carrier)
      { toCompacts := { carrier := carrier✝¹, isCompact' := isCompact'✝¹ }, nonempty' := nonempty'✝¹ } =
    (fun s => s.carrier) { toCompacts := { carrier := carrier✝, isCompact' := isCompact'✝ }, nonempty' := nonempty'✝ }
⊢ { toCompacts := { carrier := carrier✝¹, isCompact' := isCompact'✝¹ }, nonempty' := nonempty'✝¹ } =
    { toCompacts := { carrier := carrier✝, isCompact' := isCompact'✝ }, nonempty' := nonempty'✝ }
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s t : PositiveCompacts α
h : (fun s => s.carrier) s = (fun s => s.carrier) t
⊢ s = t
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := s
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
t : PositiveCompacts α
carrier✝ : Set α
isCompact'✝ : IsCompact carrier✝
interior_nonempty'✝ : Set.Nonempty (interior { carrier := carrier✝, isCompact' := isCompact'✝ }.carrier)
h :
  (fun s => s.carrier)
      { toCompacts := { carrier := carrier✝, isCompact' := isCompact'✝ }, interior_nonempty' := interior_nonempty'✝ } =
    (fun s => s.carrier) t
⊢ { toCompacts := { carrier := carrier✝, isCompact' := isCompact'✝ }, interior_nonempty' := interior_nonempty'✝ } = t
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := t
[GOAL]
case mk.mk.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
carrier✝¹ : Set α
isCompact'✝¹ : IsCompact carrier✝¹
interior_nonempty'✝¹ : Set.Nonempty (interior { carrier := carrier✝¹, isCompact' := isCompact'✝¹ }.carrier)
carrier✝ : Set α
isCompact'✝ : IsCompact carrier✝
interior_nonempty'✝ : Set.Nonempty (interior { carrier := carrier✝, isCompact' := isCompact'✝ }.carrier)
h :
  (fun s => s.carrier)
      { toCompacts := { carrier := carrier✝¹, isCompact' := isCompact'✝¹ },
        interior_nonempty' := interior_nonempty'✝¹ } =
    (fun s => s.carrier)
      { toCompacts := { carrier := carrier✝, isCompact' := isCompact'✝ }, interior_nonempty' := interior_nonempty'✝ }
⊢ { toCompacts := { carrier := carrier✝¹, isCompact' := isCompact'✝¹ }, interior_nonempty' := interior_nonempty'✝¹ } =
    { toCompacts := { carrier := carrier✝, isCompact' := isCompact'✝ }, interior_nonempty' := interior_nonempty'✝ }
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
K : PositiveCompacts α
L : PositiveCompacts β
⊢ Set.Nonempty (interior (Compacts.prod K.toCompacts L.toCompacts).carrier)
[PROOFSTEP]
simp only [Compacts.carrier_eq_coe, Compacts.coe_prod, interior_prod_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
K : PositiveCompacts α
L : PositiveCompacts β
⊢ Set.Nonempty (interior ↑K.toCompacts ×ˢ interior ↑L.toCompacts)
[PROOFSTEP]
exact K.interior_nonempty.prod L.interior_nonempty
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s t : CompactOpens α
h : (fun s => s.carrier) s = (fun s => s.carrier) t
⊢ s = t
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := s
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
t : CompactOpens α
carrier✝ : Set α
isCompact'✝ : IsCompact carrier✝
isOpen'✝ : IsOpen { carrier := carrier✝, isCompact' := isCompact'✝ }.carrier
h :
  (fun s => s.carrier) { toCompacts := { carrier := carrier✝, isCompact' := isCompact'✝ }, isOpen' := isOpen'✝ } =
    (fun s => s.carrier) t
⊢ { toCompacts := { carrier := carrier✝, isCompact' := isCompact'✝ }, isOpen' := isOpen'✝ } = t
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := t
[GOAL]
case mk.mk.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
carrier✝¹ : Set α
isCompact'✝¹ : IsCompact carrier✝¹
isOpen'✝¹ : IsOpen { carrier := carrier✝¹, isCompact' := isCompact'✝¹ }.carrier
carrier✝ : Set α
isCompact'✝ : IsCompact carrier✝
isOpen'✝ : IsOpen { carrier := carrier✝, isCompact' := isCompact'✝ }.carrier
h :
  (fun s => s.carrier) { toCompacts := { carrier := carrier✝¹, isCompact' := isCompact'✝¹ }, isOpen' := isOpen'✝¹ } =
    (fun s => s.carrier) { toCompacts := { carrier := carrier✝, isCompact' := isCompact'✝ }, isOpen' := isOpen'✝ }
⊢ { toCompacts := { carrier := carrier✝¹, isCompact' := isCompact'✝¹ }, isOpen' := isOpen'✝¹ } =
    { toCompacts := { carrier := carrier✝, isCompact' := isCompact'✝ }, isOpen' := isOpen'✝ }
[PROOFSTEP]
congr


[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : NonUnitalNonAssocSemiring A
inst✝¹ : TopologicalSpace A
inst✝ : Module 𝕜 A
φ ψ : ↑(characterSpace 𝕜 A)
h : (fun φ => ↑↑φ) φ = (fun φ => ↑↑φ) ψ
⊢ φ = ψ
[PROOFSTEP]
ext1
[GOAL]
case a
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : NonUnitalNonAssocSemiring A
inst✝¹ : TopologicalSpace A
inst✝ : Module 𝕜 A
φ ψ : ↑(characterSpace 𝕜 A)
h : (fun φ => ↑↑φ) φ = (fun φ => ↑↑φ) ψ
⊢ ↑φ = ↑ψ
[PROOFSTEP]
apply FunLike.ext
[GOAL]
case a.h
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : NonUnitalNonAssocSemiring A
inst✝¹ : TopologicalSpace A
inst✝ : Module 𝕜 A
φ ψ : ↑(characterSpace 𝕜 A)
h : (fun φ => ↑↑φ) φ = (fun φ => ↑↑φ) ψ
⊢ ∀ (x : A), ↑↑φ x = ↑↑ψ x
[PROOFSTEP]
exact congr_fun h
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : ContinuousAdd 𝕜
inst✝⁴ : ContinuousConstSMul 𝕜 𝕜
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : TopologicalSpace A
inst✝¹ : Module 𝕜 A
inst✝ : Subsingleton A
φ : ↑(characterSpace 𝕜 A)
x : A
⊢ ↑↑φ x = ↑0 x
[PROOFSTEP]
rw [show x = 0 from Subsingleton.elim x 0, map_zero, map_zero]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : NonUnitalNonAssocSemiring A
inst✝¹ : TopologicalSpace A
inst✝ : Module 𝕜 A
⊢ characterSpace 𝕜 A ∪ {0} ≤ {φ | ∀ (x y : A), ↑φ (x * y) = ↑φ x * ↑φ y}
[PROOFSTEP]
rintro φ (hφ | rfl)
[GOAL]
case inl
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : NonUnitalNonAssocSemiring A
inst✝¹ : TopologicalSpace A
inst✝ : Module 𝕜 A
φ : WeakDual 𝕜 A
hφ : φ ∈ characterSpace 𝕜 A
⊢ φ ∈ {φ | ∀ (x y : A), ↑φ (x * y) = ↑φ x * ↑φ y}
[PROOFSTEP]
exact hφ.2
[GOAL]
case inr
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : NonUnitalNonAssocSemiring A
inst✝¹ : TopologicalSpace A
inst✝ : Module 𝕜 A
⊢ 0 ∈ {φ | ∀ (x y : A), ↑φ (x * y) = ↑φ x * ↑φ y}
[PROOFSTEP]
exact fun _ _ => by exact (zero_mul (0 : 𝕜)).symm
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : NonUnitalNonAssocSemiring A
inst✝¹ : TopologicalSpace A
inst✝ : Module 𝕜 A
x✝¹ x✝ : A
⊢ ↑0 (x✝¹ * x✝) = ↑0 x✝¹ * ↑0 x✝
[PROOFSTEP]
exact (zero_mul (0 : 𝕜)).symm
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : CommSemiring 𝕜
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : ContinuousAdd 𝕜
inst✝⁵ : ContinuousConstSMul 𝕜 𝕜
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : TopologicalSpace A
inst✝² : Module 𝕜 A
inst✝¹ : T2Space 𝕜
inst✝ : ContinuousMul 𝕜
⊢ IsClosed (characterSpace 𝕜 A ∪ {0})
[PROOFSTEP]
simp only [union_zero, Set.setOf_forall]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : CommSemiring 𝕜
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : ContinuousAdd 𝕜
inst✝⁵ : ContinuousConstSMul 𝕜 𝕜
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : TopologicalSpace A
inst✝² : Module 𝕜 A
inst✝¹ : T2Space 𝕜
inst✝ : ContinuousMul 𝕜
⊢ IsClosed (⋂ (i : A) (i_1 : A), {x | ↑x (i * i_1) = ↑x i * ↑x i_1})
[PROOFSTEP]
exact
  isClosed_iInter fun x =>
    isClosed_iInter fun y => isClosed_eq (eval_continuous _) <| (eval_continuous _).mul (eval_continuous _)
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
φ : ↑(characterSpace 𝕜 A)
⊢ ↑φ 1 = 1
[PROOFSTEP]
have h₁ : φ 1 * (1 - φ 1) = 0 := by rw [mul_sub, sub_eq_zero, mul_one, ← map_mul φ, one_mul]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
φ : ↑(characterSpace 𝕜 A)
⊢ ↑φ 1 * (1 - ↑φ 1) = 0
[PROOFSTEP]
rw [mul_sub, sub_eq_zero, mul_one, ← map_mul φ, one_mul]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
φ : ↑(characterSpace 𝕜 A)
h₁ : ↑φ 1 * (1 - ↑φ 1) = 0
⊢ ↑φ 1 = 1
[PROOFSTEP]
rcases mul_eq_zero.mp h₁ with (h₂ | h₂)
[GOAL]
case inl
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
φ : ↑(characterSpace 𝕜 A)
h₁ : ↑φ 1 * (1 - ↑φ 1) = 0
h₂ : ↑φ 1 = 0
⊢ ↑φ 1 = 1
[PROOFSTEP]
have : ∀ a, φ (a * 1) = 0 := fun a => by simp only [map_mul φ, h₂, mul_zero]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
φ : ↑(characterSpace 𝕜 A)
h₁ : ↑φ 1 * (1 - ↑φ 1) = 0
h₂ : ↑φ 1 = 0
a : A
⊢ ↑φ (a * 1) = 0
[PROOFSTEP]
simp only [map_mul φ, h₂, mul_zero]
[GOAL]
case inl
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
φ : ↑(characterSpace 𝕜 A)
h₁ : ↑φ 1 * (1 - ↑φ 1) = 0
h₂ : ↑φ 1 = 0
this : ∀ (a : A), ↑φ (a * 1) = 0
⊢ ↑φ 1 = 1
[PROOFSTEP]
exact False.elim (φ.prop.1 <| ContinuousLinearMap.ext <| by simpa only [mul_one] using this)
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
φ : ↑(characterSpace 𝕜 A)
h₁ : ↑φ 1 * (1 - ↑φ 1) = 0
h₂ : ↑φ 1 = 0
this : ∀ (a : A), ↑φ (a * 1) = 0
⊢ ∀ (x : A), ↑↑φ x = ↑0 x
[PROOFSTEP]
simpa only [mul_one] using this
[GOAL]
case inr
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
φ : ↑(characterSpace 𝕜 A)
h₁ : ↑φ 1 * (1 - ↑φ 1) = 0
h₂ : 1 - ↑φ 1 = 0
⊢ ↑φ 1 = 1
[PROOFSTEP]
exact (sub_eq_zero.mp h₂).symm
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
map_one' : ∀ (φ : ↑(characterSpace 𝕜 A)), ↑φ 1 = 1
src✝ : NonUnitalAlgHomClass (↑(characterSpace 𝕜 A)) 𝕜 A 𝕜 := instNonUnitalAlgHomClass
φ : ↑(characterSpace 𝕜 A)
r : 𝕜
⊢ ↑φ (↑(algebraMap 𝕜 A) r) = ↑(algebraMap 𝕜 𝕜) r
[PROOFSTEP]
rw [Algebra.algebraMap_eq_smul_one, Algebra.id.map_eq_id, RingHom.id_apply]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
map_one' : ∀ (φ : ↑(characterSpace 𝕜 A)), ↑φ 1 = 1
src✝ : NonUnitalAlgHomClass (↑(characterSpace 𝕜 A)) 𝕜 A 𝕜 := instNonUnitalAlgHomClass
φ : ↑(characterSpace 𝕜 A)
r : 𝕜
⊢ ↑φ (r • 1) = r
[PROOFSTEP]
rw [map_smul, Algebra.id.smul_eq_mul, map_one' φ, mul_one]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : CommRing 𝕜
inst✝⁷ : NoZeroDivisors 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : ContinuousAdd 𝕜
inst✝⁴ : ContinuousConstSMul 𝕜 𝕜
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial 𝕜
⊢ characterSpace 𝕜 A = {φ | ↑φ 1 = 1 ∧ ∀ (x y : A), ↑φ (x * y) = ↑φ x * ↑φ y}
[PROOFSTEP]
ext φ
[GOAL]
case h
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : CommRing 𝕜
inst✝⁷ : NoZeroDivisors 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : ContinuousAdd 𝕜
inst✝⁴ : ContinuousConstSMul 𝕜 𝕜
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial 𝕜
φ : WeakDual 𝕜 A
⊢ φ ∈ characterSpace 𝕜 A ↔ φ ∈ {φ | ↑φ 1 = 1 ∧ ∀ (x y : A), ↑φ (x * y) = ↑φ x * ↑φ y}
[PROOFSTEP]
refine' ⟨_, _⟩
[GOAL]
case h.refine'_1
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : CommRing 𝕜
inst✝⁷ : NoZeroDivisors 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : ContinuousAdd 𝕜
inst✝⁴ : ContinuousConstSMul 𝕜 𝕜
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial 𝕜
φ : WeakDual 𝕜 A
⊢ φ ∈ characterSpace 𝕜 A → φ ∈ {φ | ↑φ 1 = 1 ∧ ∀ (x y : A), ↑φ (x * y) = ↑φ x * ↑φ y}
[PROOFSTEP]
rintro hφ
[GOAL]
case h.refine'_1
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : CommRing 𝕜
inst✝⁷ : NoZeroDivisors 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : ContinuousAdd 𝕜
inst✝⁴ : ContinuousConstSMul 𝕜 𝕜
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial 𝕜
φ : WeakDual 𝕜 A
hφ : φ ∈ characterSpace 𝕜 A
⊢ φ ∈ {φ | ↑φ 1 = 1 ∧ ∀ (x y : A), ↑φ (x * y) = ↑φ x * ↑φ y}
[PROOFSTEP]
lift φ to characterSpace 𝕜 A using hφ
[GOAL]
case h.refine'_1.intro
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : CommRing 𝕜
inst✝⁷ : NoZeroDivisors 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : ContinuousAdd 𝕜
inst✝⁴ : ContinuousConstSMul 𝕜 𝕜
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial 𝕜
φ : { x // x ∈ characterSpace 𝕜 A }
⊢ ↑φ ∈ {φ | ↑φ 1 = 1 ∧ ∀ (x y : A), ↑φ (x * y) = ↑φ x * ↑φ y}
[PROOFSTEP]
exact ⟨map_one φ, map_mul φ⟩
[GOAL]
case h.refine'_2
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : CommRing 𝕜
inst✝⁷ : NoZeroDivisors 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : ContinuousAdd 𝕜
inst✝⁴ : ContinuousConstSMul 𝕜 𝕜
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial 𝕜
φ : WeakDual 𝕜 A
⊢ φ ∈ {φ | ↑φ 1 = 1 ∧ ∀ (x y : A), ↑φ (x * y) = ↑φ x * ↑φ y} → φ ∈ characterSpace 𝕜 A
[PROOFSTEP]
rintro ⟨hφ₁, hφ₂⟩
[GOAL]
case h.refine'_2.intro
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : CommRing 𝕜
inst✝⁷ : NoZeroDivisors 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : ContinuousAdd 𝕜
inst✝⁴ : ContinuousConstSMul 𝕜 𝕜
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial 𝕜
φ : WeakDual 𝕜 A
hφ₁ : ↑φ 1 = 1
hφ₂ : ∀ (x y : A), ↑φ (x * y) = ↑φ x * ↑φ y
⊢ φ ∈ characterSpace 𝕜 A
[PROOFSTEP]
refine' ⟨_, hφ₂⟩
[GOAL]
case h.refine'_2.intro
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : CommRing 𝕜
inst✝⁷ : NoZeroDivisors 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : ContinuousAdd 𝕜
inst✝⁴ : ContinuousConstSMul 𝕜 𝕜
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial 𝕜
φ : WeakDual 𝕜 A
hφ₁ : ↑φ 1 = 1
hφ₂ : ∀ (x y : A), ↑φ (x * y) = ↑φ x * ↑φ y
⊢ φ ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case h.refine'_2.intro
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : CommRing 𝕜
inst✝⁷ : NoZeroDivisors 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : ContinuousAdd 𝕜
inst✝⁴ : ContinuousConstSMul 𝕜 𝕜
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial 𝕜
hφ₁ : ↑0 1 = 1
hφ₂ : ∀ (x y : A), ↑0 (x * y) = ↑0 x * ↑0 y
⊢ False
[PROOFSTEP]
exact zero_ne_one hφ₁
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing 𝕜
inst✝⁹ : NoZeroDivisors 𝕜
inst✝⁸ : TopologicalSpace 𝕜
inst✝⁷ : ContinuousAdd 𝕜
inst✝⁶ : ContinuousConstSMul 𝕜 𝕜
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Semiring A
inst✝³ : Algebra 𝕜 A
inst✝² : Nontrivial 𝕜
inst✝¹ : T2Space 𝕜
inst✝ : ContinuousMul 𝕜
⊢ IsClosed (characterSpace 𝕜 A)
[PROOFSTEP]
rw [eq_set_map_one_map_mul, Set.setOf_and]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing 𝕜
inst✝⁹ : NoZeroDivisors 𝕜
inst✝⁸ : TopologicalSpace 𝕜
inst✝⁷ : ContinuousAdd 𝕜
inst✝⁶ : ContinuousConstSMul 𝕜 𝕜
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Semiring A
inst✝³ : Algebra 𝕜 A
inst✝² : Nontrivial 𝕜
inst✝¹ : T2Space 𝕜
inst✝ : ContinuousMul 𝕜
⊢ IsClosed ({a | ↑a 1 = 1} ∩ {a | ∀ (x y : A), ↑a (x * y) = ↑a x * ↑a y})
[PROOFSTEP]
refine' IsClosed.inter (isClosed_eq (eval_continuous _) continuous_const) _
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing 𝕜
inst✝⁹ : NoZeroDivisors 𝕜
inst✝⁸ : TopologicalSpace 𝕜
inst✝⁷ : ContinuousAdd 𝕜
inst✝⁶ : ContinuousConstSMul 𝕜 𝕜
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Semiring A
inst✝³ : Algebra 𝕜 A
inst✝² : Nontrivial 𝕜
inst✝¹ : T2Space 𝕜
inst✝ : ContinuousMul 𝕜
⊢ IsClosed {a | ∀ (x y : A), ↑a (x * y) = ↑a x * ↑a y}
[PROOFSTEP]
simpa only [(union_zero 𝕜 A).symm] using union_zero_isClosed _ _
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
φ ψ : ↑(characterSpace 𝕜 A)
h : RingHom.ker φ = RingHom.ker ψ
⊢ φ = ψ
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
φ ψ : ↑(characterSpace 𝕜 A)
h : RingHom.ker φ = RingHom.ker ψ
x : A
⊢ ↑φ x = ↑ψ x
[PROOFSTEP]
have : x - algebraMap 𝕜 A (ψ x) ∈ RingHom.ker φ := by
  simpa only [h, RingHom.mem_ker, map_sub, AlgHomClass.commutes] using sub_self (ψ x)
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
φ ψ : ↑(characterSpace 𝕜 A)
h : RingHom.ker φ = RingHom.ker ψ
x : A
⊢ x - ↑(algebraMap 𝕜 A) (↑ψ x) ∈ RingHom.ker φ
[PROOFSTEP]
simpa only [h, RingHom.mem_ker, map_sub, AlgHomClass.commutes] using sub_self (ψ x)
[GOAL]
case h
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : CommRing 𝕜
inst✝⁶ : NoZeroDivisors 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
φ ψ : ↑(characterSpace 𝕜 A)
h : RingHom.ker φ = RingHom.ker ψ
x : A
this : x - ↑(algebraMap 𝕜 A) (↑ψ x) ∈ RingHom.ker φ
⊢ ↑φ x = ↑ψ x
[PROOFSTEP]
rwa [RingHom.mem_ker, map_sub, AlgHomClass.commutes, sub_eq_zero] at this
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousAdd 𝕜
inst✝³ : ContinuousConstSMul 𝕜 𝕜
inst✝² : Ring A
inst✝¹ : TopologicalSpace A
inst✝ : Algebra 𝕜 A
φ : ↑(characterSpace 𝕜 A)
z : 𝕜
⊢ ↑φ (↑(algebraMap 𝕜 A) z) = z
[PROOFSTEP]
simp only [AlgHomClass.commutes, Algebra.id.map_eq_id, RingHom.id_apply]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommRing 𝕜
inst✝⁵ : NoZeroDivisors 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : TopologicalRing 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
⊢ (fun a => mk fun φ => ↑φ a) 1 = 1
[PROOFSTEP]
ext a
[GOAL]
case h
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommRing 𝕜
inst✝⁵ : NoZeroDivisors 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : TopologicalRing 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
a : ↑(characterSpace 𝕜 A)
⊢ ↑((fun a => mk fun φ => ↑φ a) 1) a = ↑1 a
[PROOFSTEP]
simp only [coe_mk, coe_one, Pi.one_apply, map_one a]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommRing 𝕜
inst✝⁵ : NoZeroDivisors 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : TopologicalRing 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
a b : A
⊢ OneHom.toFun { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) } (a * b) =
    OneHom.toFun { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) } a *
      OneHom.toFun { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) } b
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommRing 𝕜
inst✝⁵ : NoZeroDivisors 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : TopologicalRing 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
a b : A
a✝ : ↑(characterSpace 𝕜 A)
⊢ ↑(OneHom.toFun { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) } (a * b))
      a✝ =
    ↑(OneHom.toFun { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) } a *
          OneHom.toFun { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) } b)
      a✝
[PROOFSTEP]
simp only [map_mul, coe_mk, coe_mul, Pi.mul_apply]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommRing 𝕜
inst✝⁵ : NoZeroDivisors 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : TopologicalRing 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (a b : A),
                OneHom.toFun { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                    (a * b) =
                  OneHom.toFun
                      { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) } a *
                    OneHom.toFun
                      { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) } b) })
      0 =
    0
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommRing 𝕜
inst✝⁵ : NoZeroDivisors 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : TopologicalRing 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
a✝ : ↑(characterSpace 𝕜 A)
⊢ ↑(OneHom.toFun
          (↑{ toOneHom := { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (a b : A),
                    OneHom.toFun
                        { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                        (a * b) =
                      OneHom.toFun
                          { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                          a *
                        OneHom.toFun
                          { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                          b) })
          0)
      a✝ =
    ↑0 a✝
[PROOFSTEP]
simp only [map_zero, coe_mk, coe_mul, coe_zero, Pi.zero_apply]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommRing 𝕜
inst✝⁵ : NoZeroDivisors 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : TopologicalRing 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
a b : A
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (a b : A),
                OneHom.toFun { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                    (a * b) =
                  OneHom.toFun
                      { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) } a *
                    OneHom.toFun
                      { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) } b) })
      (a + b) =
    OneHom.toFun
        (↑{ toOneHom := { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (a b : A),
                  OneHom.toFun
                      { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                      (a * b) =
                    OneHom.toFun
                        { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) } a *
                      OneHom.toFun
                        { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                        b) })
        a +
      OneHom.toFun
        (↑{ toOneHom := { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (a b : A),
                  OneHom.toFun
                      { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                      (a * b) =
                    OneHom.toFun
                        { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) } a *
                      OneHom.toFun
                        { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                        b) })
        b
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommRing 𝕜
inst✝⁵ : NoZeroDivisors 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : TopologicalRing 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
a b : A
a✝ : ↑(characterSpace 𝕜 A)
⊢ ↑(OneHom.toFun
          (↑{ toOneHom := { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (a b : A),
                    OneHom.toFun
                        { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                        (a * b) =
                      OneHom.toFun
                          { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                          a *
                        OneHom.toFun
                          { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                          b) })
          (a + b))
      a✝ =
    ↑(OneHom.toFun
            (↑{ toOneHom := { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (a b : A),
                      OneHom.toFun
                          { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                          (a * b) =
                        OneHom.toFun
                            { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                            a *
                          OneHom.toFun
                            { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                            b) })
            a +
          OneHom.toFun
            (↑{ toOneHom := { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (a b : A),
                      OneHom.toFun
                          { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                          (a * b) =
                        OneHom.toFun
                            { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                            a *
                          OneHom.toFun
                            { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                            b) })
            b)
      a✝
[PROOFSTEP]
simp only [map_add, coe_mk, coe_add, Pi.add_apply]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommRing 𝕜
inst✝⁵ : NoZeroDivisors 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : TopologicalRing 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
k : 𝕜
⊢ OneHom.toFun
      (↑↑{
            toMonoidHom :=
              { toOneHom := { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (a b : A),
                      OneHom.toFun
                          { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                          (a * b) =
                        OneHom.toFun
                            { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                            a *
                          OneHom.toFun
                            { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                            b) },
            map_zero' :=
              (_ :
                OneHom.toFun
                    (↑{
                        toOneHom :=
                          { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) },
                        map_mul' :=
                          (_ :
                            ∀ (a b : A),
                              OneHom.toFun
                                  { toFun := fun a => mk fun φ => ↑φ a,
                                    map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                  (a * b) =
                                OneHom.toFun
                                    { toFun := fun a => mk fun φ => ↑φ a,
                                      map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                    a *
                                  OneHom.toFun
                                    { toFun := fun a => mk fun φ => ↑φ a,
                                      map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                    b) })
                    0 =
                  0),
            map_add' :=
              (_ :
                ∀ (a b : A),
                  OneHom.toFun
                      (↑{
                          toOneHom :=
                            { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) },
                          map_mul' :=
                            (_ :
                              ∀ (a b : A),
                                OneHom.toFun
                                    { toFun := fun a => mk fun φ => ↑φ a,
                                      map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                    (a * b) =
                                  OneHom.toFun
                                      { toFun := fun a => mk fun φ => ↑φ a,
                                        map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                      a *
                                    OneHom.toFun
                                      { toFun := fun a => mk fun φ => ↑φ a,
                                        map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                      b) })
                      (a + b) =
                    OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun a => mk fun φ => ↑φ a,
                                map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (a b : A),
                                  OneHom.toFun
                                      { toFun := fun a => mk fun φ => ↑φ a,
                                        map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                      (a * b) =
                                    OneHom.toFun
                                        { toFun := fun a => mk fun φ => ↑φ a,
                                          map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                        a *
                                      OneHom.toFun
                                        { toFun := fun a => mk fun φ => ↑φ a,
                                          map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                        b) })
                        a +
                      OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun a => mk fun φ => ↑φ a,
                                map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (a b : A),
                                  OneHom.toFun
                                      { toFun := fun a => mk fun φ => ↑φ a,
                                        map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                      (a * b) =
                                    OneHom.toFun
                                        { toFun := fun a => mk fun φ => ↑φ a,
                                          map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                        a *
                                      OneHom.toFun
                                        { toFun := fun a => mk fun φ => ↑φ a,
                                          map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                        b) })
                        b) })
      (↑(algebraMap 𝕜 A) k) =
    ↑(algebraMap 𝕜 C(↑(characterSpace 𝕜 A), 𝕜)) k
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : CommRing 𝕜
inst✝⁵ : NoZeroDivisors 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : TopologicalRing 𝕜
inst✝² : TopologicalSpace A
inst✝¹ : Semiring A
inst✝ : Algebra 𝕜 A
k : 𝕜
a✝ : ↑(characterSpace 𝕜 A)
⊢ ↑(OneHom.toFun
          (↑↑{
                toMonoidHom :=
                  {
                    toOneHom :=
                      { toFun := fun a => mk fun φ => ↑φ a, map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) },
                    map_mul' :=
                      (_ :
                        ∀ (a b : A),
                          OneHom.toFun
                              { toFun := fun a => mk fun φ => ↑φ a,
                                map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                              (a * b) =
                            OneHom.toFun
                                { toFun := fun a => mk fun φ => ↑φ a,
                                  map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                a *
                              OneHom.toFun
                                { toFun := fun a => mk fun φ => ↑φ a,
                                  map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                b) },
                map_zero' :=
                  (_ :
                    OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun a => mk fun φ => ↑φ a,
                                map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (a b : A),
                                  OneHom.toFun
                                      { toFun := fun a => mk fun φ => ↑φ a,
                                        map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                      (a * b) =
                                    OneHom.toFun
                                        { toFun := fun a => mk fun φ => ↑φ a,
                                          map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                        a *
                                      OneHom.toFun
                                        { toFun := fun a => mk fun φ => ↑φ a,
                                          map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                        b) })
                        0 =
                      0),
                map_add' :=
                  (_ :
                    ∀ (a b : A),
                      OneHom.toFun
                          (↑{
                              toOneHom :=
                                { toFun := fun a => mk fun φ => ↑φ a,
                                  map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) },
                              map_mul' :=
                                (_ :
                                  ∀ (a b : A),
                                    OneHom.toFun
                                        { toFun := fun a => mk fun φ => ↑φ a,
                                          map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                        (a * b) =
                                      OneHom.toFun
                                          { toFun := fun a => mk fun φ => ↑φ a,
                                            map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                          a *
                                        OneHom.toFun
                                          { toFun := fun a => mk fun φ => ↑φ a,
                                            map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                          b) })
                          (a + b) =
                        OneHom.toFun
                            (↑{
                                toOneHom :=
                                  { toFun := fun a => mk fun φ => ↑φ a,
                                    map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) },
                                map_mul' :=
                                  (_ :
                                    ∀ (a b : A),
                                      OneHom.toFun
                                          { toFun := fun a => mk fun φ => ↑φ a,
                                            map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                          (a * b) =
                                        OneHom.toFun
                                            { toFun := fun a => mk fun φ => ↑φ a,
                                              map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                            a *
                                          OneHom.toFun
                                            { toFun := fun a => mk fun φ => ↑φ a,
                                              map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                            b) })
                            a +
                          OneHom.toFun
                            (↑{
                                toOneHom :=
                                  { toFun := fun a => mk fun φ => ↑φ a,
                                    map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) },
                                map_mul' :=
                                  (_ :
                                    ∀ (a b : A),
                                      OneHom.toFun
                                          { toFun := fun a => mk fun φ => ↑φ a,
                                            map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                          (a * b) =
                                        OneHom.toFun
                                            { toFun := fun a => mk fun φ => ↑φ a,
                                              map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                            a *
                                          OneHom.toFun
                                            { toFun := fun a => mk fun φ => ↑φ a,
                                              map_one' := (_ : (fun a => mk fun φ => ↑φ a) 1 = 1) }
                                            b) })
                            b) })
          (↑(algebraMap 𝕜 A) k))
      a✝ =
    ↑(↑(algebraMap 𝕜 C(↑(characterSpace 𝕜 A), 𝕜)) k) a✝
[PROOFSTEP]
simp [AlgHomClass.commutes]


[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{max v u, w} D
inst✝ : Abelian D
J : GrothendieckTopology C
j : ℕ
F : Discrete (Fin j) ⥤ Sheaf J D
⊢ HasLimit F
[PROOFSTEP]
infer_instance


[GOAL]
X : TopCat
T : ↑X → Type u
ι : Type u
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type u)).obj ((presheafToTypes X T).obj (Opposite.op (U i)))
hsf : IsCompatible (presheafToTypes X T) U sf
⊢ ∃! s, IsGluing (presheafToTypes X T) U sf s
[PROOFSTEP]
choose index index_spec using fun x : ↑(iSup U) =>
  Opens.mem_iSup.mp
    x.2
      -- Using this data, we can glue our functions together to a single section
[GOAL]
X : TopCat
T : ↑X → Type u
ι : Type u
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type u)).obj ((presheafToTypes X T).obj (Opposite.op (U i)))
hsf : IsCompatible (presheafToTypes X T) U sf
index : { x // x ∈ iSup U } → ι
index_spec : ∀ (x : { x // x ∈ iSup U }), ↑x ∈ U (index x)
⊢ ∃! s, IsGluing (presheafToTypes X T) U sf s
[PROOFSTEP]
let s : ∀ x : ↑(iSup U), T x := fun x => sf (index x) ⟨x.1, index_spec x⟩
[GOAL]
X : TopCat
T : ↑X → Type u
ι : Type u
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type u)).obj ((presheafToTypes X T).obj (Opposite.op (U i)))
hsf : IsCompatible (presheafToTypes X T) U sf
index : { x // x ∈ iSup U } → ι
index_spec : ∀ (x : { x // x ∈ iSup U }), ↑x ∈ U (index x)
s : (x : { x // x ∈ iSup U }) → T ↑x := fun x => sf (index x) { val := ↑x, property := (_ : ↑x ∈ U (index x)) }
⊢ ∃! s, IsGluing (presheafToTypes X T) U sf s
[PROOFSTEP]
refine' ⟨s, _, _⟩
[GOAL]
case refine'_1
X : TopCat
T : ↑X → Type u
ι : Type u
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type u)).obj ((presheafToTypes X T).obj (Opposite.op (U i)))
hsf : IsCompatible (presheafToTypes X T) U sf
index : { x // x ∈ iSup U } → ι
index_spec : ∀ (x : { x // x ∈ iSup U }), ↑x ∈ U (index x)
s : (x : { x // x ∈ iSup U }) → T ↑x := fun x => sf (index x) { val := ↑x, property := (_ : ↑x ∈ U (index x)) }
⊢ (fun s => IsGluing (presheafToTypes X T) U sf s) s
[PROOFSTEP]
intro i
[GOAL]
case refine'_1
X : TopCat
T : ↑X → Type u
ι : Type u
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type u)).obj ((presheafToTypes X T).obj (Opposite.op (U i)))
hsf : IsCompatible (presheafToTypes X T) U sf
index : { x // x ∈ iSup U } → ι
index_spec : ∀ (x : { x // x ∈ iSup U }), ↑x ∈ U (index x)
s : (x : { x // x ∈ iSup U }) → T ↑x := fun x => sf (index x) { val := ↑x, property := (_ : ↑x ∈ U (index x)) }
i : ι
⊢ ↑((presheafToTypes X T).map (leSupr U i).op) s = sf i
[PROOFSTEP]
funext x
[GOAL]
case refine'_1.h
X : TopCat
T : ↑X → Type u
ι : Type u
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type u)).obj ((presheafToTypes X T).obj (Opposite.op (U i)))
hsf : IsCompatible (presheafToTypes X T) U sf
index : { x // x ∈ iSup U } → ι
index_spec : ∀ (x : { x // x ∈ iSup U }), ↑x ∈ U (index x)
s : (x : { x // x ∈ iSup U }) → T ↑x := fun x => sf (index x) { val := ↑x, property := (_ : ↑x ∈ U (index x)) }
i : ι
x : { x // x ∈ (Opposite.op (U i)).unop }
⊢ ↑((presheafToTypes X T).map (leSupr U i).op) s x = sf i x
[PROOFSTEP]
exact congr_fun (hsf (index ⟨x, _⟩) i) ⟨x, ⟨index_spec ⟨x.1, _⟩, x.2⟩⟩
[GOAL]
case refine'_2
X : TopCat
T : ↑X → Type u
ι : Type u
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type u)).obj ((presheafToTypes X T).obj (Opposite.op (U i)))
hsf : IsCompatible (presheafToTypes X T) U sf
index : { x // x ∈ iSup U } → ι
index_spec : ∀ (x : { x // x ∈ iSup U }), ↑x ∈ U (index x)
s : (x : { x // x ∈ iSup U }) → T ↑x := fun x => sf (index x) { val := ↑x, property := (_ : ↑x ∈ U (index x)) }
⊢ ∀ (y : (forget (Type u)).obj ((presheafToTypes X T).obj (Opposite.op (iSup U)))),
    (fun s => IsGluing (presheafToTypes X T) U sf s) y → y = s
[PROOFSTEP]
intro t ht
[GOAL]
case refine'_2
X : TopCat
T : ↑X → Type u
ι : Type u
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type u)).obj ((presheafToTypes X T).obj (Opposite.op (U i)))
hsf : IsCompatible (presheafToTypes X T) U sf
index : { x // x ∈ iSup U } → ι
index_spec : ∀ (x : { x // x ∈ iSup U }), ↑x ∈ U (index x)
s : (x : { x // x ∈ iSup U }) → T ↑x := fun x => sf (index x) { val := ↑x, property := (_ : ↑x ∈ U (index x)) }
t : (forget (Type u)).obj ((presheafToTypes X T).obj (Opposite.op (iSup U)))
ht : IsGluing (presheafToTypes X T) U sf t
⊢ t = s
[PROOFSTEP]
funext x
[GOAL]
case refine'_2.h
X : TopCat
T : ↑X → Type u
ι : Type u
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type u)).obj ((presheafToTypes X T).obj (Opposite.op (U i)))
hsf : IsCompatible (presheafToTypes X T) U sf
index : { x // x ∈ iSup U } → ι
index_spec : ∀ (x : { x // x ∈ iSup U }), ↑x ∈ U (index x)
s : (x : { x // x ∈ iSup U }) → T ↑x := fun x => sf (index x) { val := ↑x, property := (_ : ↑x ∈ U (index x)) }
t : (forget (Type u)).obj ((presheafToTypes X T).obj (Opposite.op (iSup U)))
ht : IsGluing (presheafToTypes X T) U sf t
x : { x // x ∈ (Opposite.op (iSup U)).unop }
⊢ t x = s x
[PROOFSTEP]
exact congr_fun (ht (index x)) ⟨x.1, index_spec x⟩


[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F✝ : Presheaf C X
ι : Type v
U✝ : ι → Opens ↑X
F : Presheaf (Discrete Unit) X
x✝² : Discrete Unit
U : Opens ↑X
S : Sieve U
x✝¹ : S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
x : Presieve.FamilyOfElements (F ⋙ coyoneda.obj (op x✝²)) S.arrows
x✝ : Presieve.FamilyOfElements.Compatible x
⊢ (fun t => Presieve.FamilyOfElements.IsAmalgamation x t) (eqToHom (_ : (op x✝²).unop = F.obj (op U)))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F✝ : Presheaf C X
ι : Type v
U✝ : ι → Opens ↑X
F : Presheaf (Discrete Unit) X
x✝³ : Discrete Unit
U : Opens ↑X
S : Sieve U
x✝² : S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
x : Presieve.FamilyOfElements (F ⋙ coyoneda.obj (op x✝³)) S.arrows
x✝¹ : Presieve.FamilyOfElements.Compatible x
x✝ : (F ⋙ coyoneda.obj (op x✝³)).obj (op U)
⊢ (fun t => Presieve.FamilyOfElements.IsAmalgamation x t) x✝ → x✝ = eqToHom (_ : (op x✝³).unop = F.obj (op U))
[PROOFSTEP]
aesop_cat


[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
U : TopologicalSpace.Opens ↑X
s : Sieve U
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
⊢ Presieve.IsSheafFor (F ⋙ coyoneda.obj (op c)) s.arrows
[PROOFSTEP]
obtain rfl | hne := eq_or_ne U ⊥
[GOAL]
case inl
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
s : Sieve ⊥
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊥
⊢ Presieve.IsSheafFor (F ⋙ coyoneda.obj (op c)) s.arrows
[PROOFSTEP]
intro _ _
[GOAL]
case inl
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
s : Sieve ⊥
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊥
x✝ : Presieve.FamilyOfElements (F ⋙ coyoneda.obj (op c)) s.arrows
a✝ : Presieve.FamilyOfElements.Compatible x✝
⊢ ∃! t, Presieve.FamilyOfElements.IsAmalgamation x✝ t
[PROOFSTEP]
rw [@exists_unique_iff_exists _ ⟨fun _ _ => _⟩]
[GOAL]
case inl
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
s : Sieve ⊥
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊥
x✝ : Presieve.FamilyOfElements (F ⋙ coyoneda.obj (op c)) s.arrows
a✝ : Presieve.FamilyOfElements.Compatible x✝
⊢ ∃ x, Presieve.FamilyOfElements.IsAmalgamation x✝ x
[PROOFSTEP]
refine' ⟨it.from _, fun U hU hs => IsTerminal.hom_ext _ _ _⟩
[GOAL]
case inl
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
s : Sieve ⊥
hs✝ : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊥
x✝ : Presieve.FamilyOfElements (F ⋙ coyoneda.obj (op c)) s.arrows
a✝ : Presieve.FamilyOfElements.Compatible x✝
U : TopologicalSpace.Opens ↑X
hU : U ⟶ ⊥
hs : s.arrows hU
⊢ IsTerminal (F.obj (op U))
[PROOFSTEP]
rwa [le_bot_iff.1 hU.le]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
s : Sieve ⊥
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊥
x✝ : Presieve.FamilyOfElements (F ⋙ coyoneda.obj (op c)) s.arrows
a✝ : Presieve.FamilyOfElements.Compatible x✝
⊢ ∀ (x x_1 : (F ⋙ coyoneda.obj (op c)).obj (op ⊥)), x = x_1
[PROOFSTEP]
apply it.hom_ext
[GOAL]
case inr
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
U : TopologicalSpace.Opens ↑X
s : Sieve U
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
hne : U ≠ ⊥
⊢ Presieve.IsSheafFor (F ⋙ coyoneda.obj (op c)) s.arrows
[PROOFSTEP]
convert Presieve.isSheafFor_top_sieve (F ⋙ coyoneda.obj (@op C c))
[GOAL]
case h.e'_5.h.h.e'_4
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
U : TopologicalSpace.Opens ↑X
s : Sieve U
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
hne : U ≠ ⊥
⊢ s = ⊤
[PROOFSTEP]
rw [← Sieve.id_mem_iff_eq_top]
[GOAL]
case h.e'_5.h.h.e'_4
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
U : TopologicalSpace.Opens ↑X
s : Sieve U
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
hne : U ≠ ⊥
⊢ s.arrows (𝟙 U)
[PROOFSTEP]
have := (U.eq_bot_or_top hind).resolve_left hne
[GOAL]
case h.e'_5.h.h.e'_4
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
U : TopologicalSpace.Opens ↑X
s : Sieve U
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
hne : U ≠ ⊥
this : U = ⊤
⊢ s.arrows (𝟙 U)
[PROOFSTEP]
subst this
[GOAL]
case h.e'_5.h.h.e'_4
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
s : Sieve ⊤
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊤
hne : ⊤ ≠ ⊥
⊢ s.arrows (𝟙 ⊤)
[PROOFSTEP]
obtain he | ⟨⟨x⟩⟩ := isEmpty_or_nonempty X
[GOAL]
case h.e'_5.h.h.e'_4.inl
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
s : Sieve ⊤
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊤
hne : ⊤ ≠ ⊥
he : IsEmpty ↑X
⊢ s.arrows (𝟙 ⊤)
[PROOFSTEP]
exact (hne <| SetLike.ext'_iff.2 <| Set.univ_eq_empty_iff.2 he).elim
[GOAL]
case h.e'_5.h.h.e'_4.inr.intro
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
s : Sieve ⊤
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊤
hne : ⊤ ≠ ⊥
x : ↑X
⊢ s.arrows (𝟙 ⊤)
[PROOFSTEP]
obtain ⟨U, f, hf, hm⟩ := hs x _root_.trivial
[GOAL]
case h.e'_5.h.h.e'_4.inr.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
s : Sieve ⊤
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊤
hne : ⊤ ≠ ⊥
x : ↑X
U : TopologicalSpace.Opens ↑X
f : U ⟶ ⊤
hf : s.arrows f
hm : x ∈ U
⊢ s.arrows (𝟙 ⊤)
[PROOFSTEP]
obtain rfl | rfl := U.eq_bot_or_top hind
[GOAL]
case h.e'_5.h.h.e'_4.inr.intro.intro.intro.intro.inl
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
s : Sieve ⊤
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊤
hne : ⊤ ≠ ⊥
x : ↑X
f : ⊥ ⟶ ⊤
hf : s.arrows f
hm : x ∈ ⊥
⊢ s.arrows (𝟙 ⊤)
[PROOFSTEP]
cases hm
[GOAL]
case h.e'_5.h.h.e'_4.inr.intro.intro.intro.intro.inr
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
s : Sieve ⊤
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊤
hne : ⊤ ≠ ⊥
x : ↑X
f : ⊤ ⟶ ⊤
hf : s.arrows f
hm : x ∈ ⊤
⊢ s.arrows (𝟙 ⊤)
[PROOFSTEP]
convert hf


[GOAL]
X : TopCat
T : ↑X → Type v
U : (Opens ↑X)ᵒᵖ
⊢ { obj := fun U => (x : { x // x ∈ U.unop }) → T ↑x,
          map := fun {U V} i g x => g ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x) }.map
      (𝟙 U) =
    𝟙
      ({ obj := fun U => (x : { x // x ∈ U.unop }) → T ↑x,
            map := fun {U V} i g x => g ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x) }.obj
        U)
[PROOFSTEP]
ext g
[GOAL]
case h
X : TopCat
T : ↑X → Type v
U : (Opens ↑X)ᵒᵖ
g :
  { obj := fun U => (x : { x // x ∈ U.unop }) → T ↑x,
        map := fun {U V} i g x => g ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x) }.obj
    U
⊢ { obj := fun U => (x : { x // x ∈ U.unop }) → T ↑x,
          map := fun {U V} i g x => g ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x) }.map
      (𝟙 U) g =
    𝟙
      ({ obj := fun U => (x : { x // x ∈ U.unop }) → T ↑x,
            map := fun {U V} i g x => g ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x) }.obj
        U)
      g
[PROOFSTEP]
rfl
[GOAL]
X : TopCat
T : Type v
U : (Opens ↑X)ᵒᵖ
⊢ { obj := fun U => { x // x ∈ U.unop } → T,
          map := fun {U V} i g => g ∘ fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) } }.map
      (𝟙 U) =
    𝟙
      ({ obj := fun U => { x // x ∈ U.unop } → T,
            map := fun {U V} i g => g ∘ fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) } }.obj
        U)
[PROOFSTEP]
ext g
[GOAL]
case h
X : TopCat
T : Type v
U : (Opens ↑X)ᵒᵖ
g :
  { obj := fun U => { x // x ∈ U.unop } → T,
        map := fun {U V} i g => g ∘ fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) } }.obj
    U
⊢ { obj := fun U => { x // x ∈ U.unop } → T,
          map := fun {U V} i g => g ∘ fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) } }.map
      (𝟙 U) g =
    𝟙
      ({ obj := fun U => { x // x ∈ U.unop } → T,
            map := fun {U V} i g => g ∘ fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) } }.obj
        U)
      g
[PROOFSTEP]
rfl
[GOAL]
X✝ : TopCat
X : TopCatᵒᵖ
R : TopCommRingCat
⊢ CommRing C(↑X.unop, ↑((forget₂ TopCommRingCat TopCat).obj R))
[PROOFSTEP]
infer_instance
[GOAL]
X✝ : TopCat
X Y : TopCatᵒᵖ
f : X ⟶ Y
R : TopCommRingCat
⊢ ∀ (x y : ↑(continuousFunctions X R)),
    OneHom.toFun { toFun := fun g => f.unop ≫ g, map_one' := (_ : (fun g => f.unop ≫ g) 1 = (fun g => f.unop ≫ g) 1) }
        (x * y) =
      OneHom.toFun { toFun := fun g => f.unop ≫ g, map_one' := (_ : (fun g => f.unop ≫ g) 1 = (fun g => f.unop ≫ g) 1) }
          x *
        OneHom.toFun
          { toFun := fun g => f.unop ≫ g, map_one' := (_ : (fun g => f.unop ≫ g) 1 = (fun g => f.unop ≫ g) 1) } y
[PROOFSTEP]
aesop_cat
[GOAL]
X✝ : TopCat
X Y : TopCatᵒᵖ
f : X ⟶ Y
R : TopCommRingCat
⊢ ∀ (x y : ↑(continuousFunctions X R)),
    OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := fun g => f.unop ≫ g, map_one' := (_ : (fun g => f.unop ≫ g) 1 = (fun g => f.unop ≫ g) 1) },
            map_mul' :=
              (_ :
                ∀ (x y : ↑(continuousFunctions X R)),
                  OneHom.toFun
                      { toFun := fun g => f.unop ≫ g,
                        map_one' := (_ : (fun g => f.unop ≫ g) 1 = (fun g => f.unop ≫ g) 1) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := fun g => f.unop ≫ g,
                          map_one' := (_ : (fun g => f.unop ≫ g) 1 = (fun g => f.unop ≫ g) 1) }
                        x *
                      OneHom.toFun
                        { toFun := fun g => f.unop ≫ g,
                          map_one' := (_ : (fun g => f.unop ≫ g) 1 = (fun g => f.unop ≫ g) 1) }
                        y) })
        (x + y) =
      OneHom.toFun
          (↑{
              toOneHom :=
                { toFun := fun g => f.unop ≫ g, map_one' := (_ : (fun g => f.unop ≫ g) 1 = (fun g => f.unop ≫ g) 1) },
              map_mul' :=
                (_ :
                  ∀ (x y : ↑(continuousFunctions X R)),
                    OneHom.toFun
                        { toFun := fun g => f.unop ≫ g,
                          map_one' := (_ : (fun g => f.unop ≫ g) 1 = (fun g => f.unop ≫ g) 1) }
                        (x * y) =
                      OneHom.toFun
                          { toFun := fun g => f.unop ≫ g,
                            map_one' := (_ : (fun g => f.unop ≫ g) 1 = (fun g => f.unop ≫ g) 1) }
                          x *
                        OneHom.toFun
                          { toFun := fun g => f.unop ≫ g,
                            map_one' := (_ : (fun g => f.unop ≫ g) 1 = (fun g => f.unop ≫ g) 1) }
                          y) })
          x +
        OneHom.toFun
          (↑{
              toOneHom :=
                { toFun := fun g => f.unop ≫ g, map_one' := (_ : (fun g => f.unop ≫ g) 1 = (fun g => f.unop ≫ g) 1) },
              map_mul' :=
                (_ :
                  ∀ (x y : ↑(continuousFunctions X R)),
                    OneHom.toFun
                        { toFun := fun g => f.unop ≫ g,
                          map_one' := (_ : (fun g => f.unop ≫ g) 1 = (fun g => f.unop ≫ g) 1) }
                        (x * y) =
                      OneHom.toFun
                          { toFun := fun g => f.unop ≫ g,
                            map_one' := (_ : (fun g => f.unop ≫ g) 1 = (fun g => f.unop ≫ g) 1) }
                          x *
                        OneHom.toFun
                          { toFun := fun g => f.unop ≫ g,
                            map_one' := (_ : (fun g => f.unop ≫ g) 1 = (fun g => f.unop ≫ g) 1) }
                          y) })
          y
[PROOFSTEP]
aesop_cat
[GOAL]
X✝ : TopCat
R : TopCommRingCat
X : TopCatᵒᵖ
⊢ { obj := fun X => continuousFunctions X R, map := fun {X Y} f => continuousFunctions.pullback f R }.map (𝟙 X) =
    𝟙 ({ obj := fun X => continuousFunctions X R, map := fun {X Y} f => continuousFunctions.pullback f R }.obj X)
[PROOFSTEP]
ext
[GOAL]
case w
X✝ : TopCat
R : TopCommRingCat
X : TopCatᵒᵖ
x✝ :
  (forget CommRingCat).obj
    ({ obj := fun X => continuousFunctions X R, map := fun {X Y} f => continuousFunctions.pullback f R }.obj X)
⊢ ↑({ obj := fun X => continuousFunctions X R, map := fun {X Y} f => continuousFunctions.pullback f R }.map (𝟙 X)) x✝ =
    ↑(𝟙 ({ obj := fun X => continuousFunctions X R, map := fun {X Y} f => continuousFunctions.pullback f R }.obj X)) x✝
[PROOFSTEP]
rfl
[GOAL]
X✝ : TopCat
X : TopCommRingCat
⊢ {
          obj := fun R =>
            CategoryTheory.Functor.mk
              { obj := fun X => continuousFunctions X R, map := fun {X Y} f => continuousFunctions.pullback f R },
          map := fun {R S} φ => NatTrans.mk fun X => continuousFunctions.map X φ }.map
      (𝟙 X) =
    𝟙
      ({
            obj := fun R =>
              CategoryTheory.Functor.mk
                { obj := fun X => continuousFunctions X R, map := fun {X Y} f => continuousFunctions.pullback f R },
            map := fun {R S} φ => NatTrans.mk fun X => continuousFunctions.map X φ }.obj
        X)
[PROOFSTEP]
ext
[GOAL]
case w.h.w
X✝ : TopCat
X : TopCommRingCat
x✝¹ : TopCatᵒᵖ
x✝ :
  (forget CommRingCat).obj
    (({
              obj := fun R =>
                CategoryTheory.Functor.mk
                  { obj := fun X => continuousFunctions X R, map := fun {X Y} f => continuousFunctions.pullback f R },
              map := fun {R S} φ => NatTrans.mk fun X => continuousFunctions.map X φ }.obj
          X).obj
      x✝¹)
⊢ ↑(NatTrans.app
          ({
                obj := fun R =>
                  CategoryTheory.Functor.mk
                    { obj := fun X => continuousFunctions X R, map := fun {X Y} f => continuousFunctions.pullback f R },
                map := fun {R S} φ => NatTrans.mk fun X => continuousFunctions.map X φ }.map
            (𝟙 X))
          x✝¹)
      x✝ =
    ↑(NatTrans.app
          (𝟙
            ({
                  obj := fun R =>
                    CategoryTheory.Functor.mk
                      { obj := fun X => continuousFunctions X R,
                        map := fun {X Y} f => continuousFunctions.pullback f R },
                  map := fun {R S} φ => NatTrans.mk fun X => continuousFunctions.map X φ }.obj
              X))
          x✝¹)
      x✝
[PROOFSTEP]
rfl