-- Mathlib/Topology/ContinuousMap/Ideals.lean
theorem setOfIdeal_ofSet_eq_interior (s : Set X) : setOfIdeal (idealOfSet 𝕜 s) = interior s

Proof state:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Set X
x : X
hx : x ∈ (closure sᶜ)ᶜ
g : C(X, ℝ)
hgs : Set.EqOn (⇑g) 0 (closure sᶜ)
hgx : Set.EqOn (⇑g) 1 {x}
⊢ ∀ ⦃x : X⦄, x ∈ sᶜ → { toFun := fun x => ↑(g x), continuous_toFun := ⋯ } x = 0

Tactic:
simpa only [coe_mk, ofReal_eq_zero] using fun x hx => hgs (subset_closure hx)

Result:
no goals

Proof state:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Set X
x : X
hx : x ∈ interior s
⊢ x ∈ setOfIdeal (idealOfSet 𝕜 s)

Tactic:
rw [← compl_compl (interior s), ← closure_compl] at hx

Result:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Set X
x : X
hx : x ∈ (closure sᶜ)ᶜ
⊢ x ∈ setOfIdeal (idealOfSet 𝕜 s)

Proof state:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Set X
x : X
hx : x ∈ (closure sᶜ)ᶜ
⊢ x ∈ setOfIdeal (idealOfSet 𝕜 s)

Tactic:
simp_rw [mem_setOfIdeal, mem_idealOfSet]

Result:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Set X
x : X
hx : x ∈ (closure sᶜ)ᶜ
⊢ ∃ f, (∀ ⦃x : X⦄, x ∈ sᶜ → f x = 0) ∧ f x ≠ 0

Proof state:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Set X
x : X
hx : x ∈ (closure sᶜ)ᶜ
⊢ ∃ f, (∀ ⦃x : X⦄, x ∈ sᶜ → f x = 0) ∧ f x ≠ 0

Tactic:
obtain ⟨g, hgs, hgx : Set.EqOn g 1 {x}, -⟩ :=
  exists_continuous_zero_one_of_isClosed isClosed_closure isClosed_singleton
    (Set.disjoint_singleton_right.mpr hx)

Result:
case intro.intro.intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Set X
x : X
hx : x ∈ (closure sᶜ)ᶜ
g : C(X, ℝ)
hgs : Set.EqOn (⇑g) 0 (closure sᶜ)
hgx : Set.EqOn (⇑g) 1 {x}
⊢ ∃ f, (∀ ⦃x : X⦄, x ∈ sᶜ → f x = 0) ∧ f x ≠ 0

Proof state:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Set X
x : X
hx : x ∈ (closure sᶜ)ᶜ
g : C(X, ℝ)
hgs : Set.EqOn (⇑g) 0 (closure sᶜ)
hgx : Set.EqOn (⇑g) 1 {x}
⊢ { toFun := fun x => ↑(g x), continuous_toFun := ⋯ } x ≠ 0

Tactic:
simpa only [coe_mk, hgx (Set.mem_singleton x), Pi.one_apply, RCLike.ofReal_one] using
  one_ne_zero

Result:
no goals

Proof state:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Set X
⊢ setOfIdeal (idealOfSet 𝕜 s) = interior s

Tactic:
refine
  Set.Subset.antisymm
    ((setOfIdeal_open (idealOfSet 𝕜 s)).subset_interior_iff.mpr fun x hx =>
      let ⟨f, hf, hfx⟩ := mem_setOfIdeal.mp hx
      Set.not_mem_compl_iff.mp (mt (@hf x) hfx))
    fun x hx => ?_

Result:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Set X
x : X
hx : x ∈ interior s
⊢ x ∈ setOfIdeal (idealOfSet 𝕜 s)

Proof state:
case intro.intro.intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Set X
x : X
hx : x ∈ (closure sᶜ)ᶜ
g : C(X, ℝ)
hgs : Set.EqOn (⇑g) 0 (closure sᶜ)
hgx : Set.EqOn (⇑g) 1 {x}
⊢ ∃ f, (∀ ⦃x : X⦄, x ∈ sᶜ → f x = 0) ∧ f x ≠ 0

Tactic:
exact
  ⟨⟨fun x => g x, continuous_ofReal.comp (map_continuous g)⟩, by
    simpa only [coe_mk, ofReal_eq_zero] using fun x hx => hgs (subset_closure hx), by
    simpa only [coe_mk, hgx (Set.mem_singleton x), Pi.one_apply, RCLike.ofReal_one] using
      one_ne_zero⟩

Result:
no goals