-- Mathlib/Topology/ContinuousMap/Ideals.lean
theorem ideal_gc : GaloisConnection (setOfIdeal : Ideal C(X, R) → Set X) (idealOfSet R)

Proof state:
case refine_1
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
I : Ideal C(X, R)
s : Set X
h : setOfIdeal I ≤ s
f : C(X, R)
hf : f ∈ I
h' : f ∉ idealOfSet R s
⊢ False

Tactic:
rcases not_mem_idealOfSet.mp h' with ⟨x, hx, hfx⟩

Result:
case refine_1.intro.intro
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
I : Ideal C(X, R)
s : Set X
h : setOfIdeal I ≤ s
f : C(X, R)
hf : f ∈ I
h' : f ∉ idealOfSet R s
x : X
hx : x ∈ sᶜ
hfx : f x ≠ 0
⊢ False

Proof state:
case refine_2.intro.intro
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
I : Ideal C(X, R)
s : Set X
h : I ≤ idealOfSet R s
x : X
hx : x ∈ setOfIdeal I
f : C(X, R)
hf : f ∈ I
hfx : f x ≠ 0
⊢ x ∈ s

Tactic:
by_contra hx'

Result:
case refine_2.intro.intro
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
I : Ideal C(X, R)
s : Set X
h : I ≤ idealOfSet R s
x : X
hx : x ∈ setOfIdeal I
f : C(X, R)
hf : f ∈ I
hfx : f x ≠ 0
hx' : x ∉ s
⊢ False

Proof state:
case refine_1.intro.intro
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
I : Ideal C(X, R)
s : Set X
h : setOfIdeal I ≤ s
f : C(X, R)
hf : f ∈ I
h' : f ∉ idealOfSet R s
x : X
hx : x ∈ sᶜ
hfx : f x ≠ 0
⊢ False

Tactic:
exact hfx (not_mem_setOfIdeal.mp (mt (@h x) hx) hf)

Result:
no goals

Proof state:
case refine_2
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
I : Ideal C(X, R)
s : Set X
h : I ≤ idealOfSet R s
x : X
hx : x ∈ setOfIdeal I
⊢ x ∈ s

Tactic:
obtain ⟨f, hf, hfx⟩ := mem_setOfIdeal.mp hx

Result:
case refine_2.intro.intro
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
I : Ideal C(X, R)
s : Set X
h : I ≤ idealOfSet R s
x : X
hx : x ∈ setOfIdeal I
f : C(X, R)
hf : f ∈ I
hfx : f x ≠ 0
⊢ x ∈ s

Proof state:
case refine_1
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
I : Ideal C(X, R)
s : Set X
h : setOfIdeal I ≤ s
f : C(X, R)
hf : f ∈ I
⊢ f ∈ idealOfSet R s

Tactic:
by_contra h'

Result:
case refine_1
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
I : Ideal C(X, R)
s : Set X
h : setOfIdeal I ≤ s
f : C(X, R)
hf : f ∈ I
h' : f ∉ idealOfSet R s
⊢ False

Proof state:
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
⊢ GaloisConnection setOfIdeal (idealOfSet R)

Tactic:
refine fun I s => ⟨fun h f hf => ?_, fun h x hx => ?_⟩

Result:
case refine_1
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
I : Ideal C(X, R)
s : Set X
h : setOfIdeal I ≤ s
f : C(X, R)
hf : f ∈ I
⊢ f ∈ idealOfSet R s

case refine_2
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
I : Ideal C(X, R)
s : Set X
h : I ≤ idealOfSet R s
x : X
hx : x ∈ setOfIdeal I
⊢ x ∈ s

Proof state:
case refine_2.intro.intro
X : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
I : Ideal C(X, R)
s : Set X
h : I ≤ idealOfSet R s
x : X
hx : x ∈ setOfIdeal I
f : C(X, R)
hf : f ∈ I
hfx : f x ≠ 0
hx' : x ∉ s
⊢ False

Tactic:
exact not_mem_idealOfSet.mpr ⟨x, hx', hfx⟩ (h hf)

Result:
no goals