awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
s : Set X
f : C(X, R)
⊢ Membership.mem (γ := Ideal C(X, R)) (idealOfSet R s) f ↔
    ∀ ⦃x : X⦄, x ∈ sᶜ → Eq.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)

Tactic:
convert! Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
s : Set X
f : C(X, R)
push :
  (∃ x ∈ sᶜ, Ne.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)) ↔
    ∃ x ∈ sᶜ, Ne.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)
⊢ (¬∀ ⦃x : X⦄, x ∈ sᶜ → Eq.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)) ↔
    ∃ x ∈ sᶜ, Ne.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
s : Set X
f : C(X, R)
⊢ (∃ x ∈ sᶜ, Ne.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)) ↔
    ∃ x ∈ sᶜ, Ne.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)

Tactic:
rfl
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
I : Ideal C(X, R)
x : X
rw : x ∈ (setOfIdeal I)ᶜ ↔ ∀ ⦃f : C(X, R)⦄, f ∈ I → Eq.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)
rw₁ :
  Membership.mem (γ := Set X) {x : X | ∀ f ∈ I, Eq.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)}ᶜᶜ x ↔
    ∀ ⦃f : C(X, R)⦄, f ∈ I → Eq.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)
rw₂ :
  Membership.mem (γ := Set X) {x : X | ∀ f ∈ I, Eq.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)} x ↔
    ∀ ⦃f : C(X, R)⦄, f ∈ I → Eq.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)
rw₃ rw₄ :
  (∀ f ∈ I, Eq.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)) ↔
    ∀ ⦃f : C(X, R)⦄, f ∈ I → Eq.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)
⊢ x ∉ setOfIdeal I ↔ ∀ ⦃f : C(X, R)⦄, f ∈ I → Eq.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)

Tactic:
rw [← Set.mem_compl_iff, setOfIdeal, compl_compl, Set.mem_setOf]

Premises used: compl_compl, Set.mem_setOf, ContinuousMap.setOfIdeal, Set.mem_compl_iff
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
I : Ideal C(X, R)
x : X
push :
  (∃ f ∈ I, Ne.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)) ↔
    ∃ f ∈ I, Ne.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)
⊢ (¬∀ f ∈ I, Eq.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)) ↔
    ∃ f ∈ I, Ne.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
I : Ideal C(X, R)
x : X
⊢ (∃ f ∈ I, Ne.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)) ↔
    ∃ f ∈ I, Ne.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)

Tactic:
rfl
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : T2Space R
I : Ideal C(X, R)
simp : IsClosed.{u_1} (X := X) (⋂ i ∈ I, {x : X | Eq.{u_2 + 1} (α := R) ((i : (a : X) → R) x : R) (0 : R)})
⊢ IsOpen (setOfIdeal I)

Tactic:
simp only [setOfIdeal, Set.setOf_forall, isOpen_compl_iff]

Premises used: ContinuousMap.setOfIdeal, Set.setOf_forall, isOpen_compl_iff
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : T2Space R
I : Ideal C(X, R)
⊢ IsClosed.{u_1} (X := X) (⋂ i ∈ I, {x : X | Eq.{u_2 + 1} (α := R) ((i : (a : X) → R) x : R) (0 : R)})

Tactic:
isClosed_iInter fun f =>
      isClosed_iInter fun _ => isClosed_eq (map_continuous f) continuous_const

Premises used: continuous_const, isClosed_eq, ContinuousMapClass.map_continuous, isClosed_iInter
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : T2Space R
I : Ideal C(X, R)
⊢ IsClosed.{u_1} (X := X) (⋂ i ∈ I, {x : X | Eq.{u_2 + 1} (α := R) ((i : (a : X) → R) x : R) (0 : R)})

Tactic:
exact
    isClosed_iInter fun f =>
      isClosed_iInter fun _ => isClosed_eq (map_continuous f) continuous_const

Premises used: continuous_const, isClosed_eq, ContinuousMapClass.map_continuous, isClosed_iInter
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : Nontrivial R
⊢ Eq.{u_1 + 1} (α := Set X) (setOfIdeal.{u_1, u_2} (R := R) ⊤) Set.univ

Tactic:
Set.univ_subset_iff.mp fun _ _ => mem_setOfIdeal.mpr ⟨1, Submodule.mem_top, one_ne_zero⟩

Premises used: Iff.mpr, Set.univ_subset_iff, And.intro, Exists.intro, Iff.mp, ContinuousMap.mem_setOfIdeal, one_ne_zero, OfNat.ofNat, Submodule.mem_top
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
f : C(X, R)
⊢ Membership.mem (γ := Ideal C(X, R)) (idealOfSet R ∅) f ↔ Membership.mem (γ := Ideal C(X, R)) ⊥ f

Tactic:
simp only [mem_idealOfSet, Set.compl_empty, Set.mem_univ, forall_true_left, Ideal.mem_bot,
      DFunLike.ext_iff, zero_apply]

Premises used: Ideal.mem_bot, forall_true_left, ContinuousMap.mem_idealOfSet, DFunLike.ext_iff, ContinuousMap.zero_apply, Set.compl_empty, Set.mem_univ
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
x : X
f : C(X, R)
⊢ Membership.mem (γ := Ideal C(X, R)) (idealOfSet R {x}ᶜ) f ↔ Eq.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)

Tactic:
simp only [mem_idealOfSet, compl_compl, Set.mem_singleton_iff, forall_eq]

Premises used: compl_compl, ContinuousMap.mem_idealOfSet, forall_eq, Set.mem_singleton_iff
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
⊢ GaloisConnection (α := Ideal C(X, R)) setOfIdeal (idealOfSet R)

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

Premises used: Iff.intro, GaloisConnection
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
refine_1 :
  ∀ (I : Ideal C(X, R)) (s : Set X) (h : setOfIdeal I ≤ s) (f : C(X, R)) (hf : f ∈ I),
    Membership.mem (γ := Submodule C(X, R) C(X, R)) (idealOfSet R s) f
refine_2 : ∀ (I : Ideal C(X, R)) (s : Set X) (h : I ≤ idealOfSet R s) (x : X) (hx : x ∈ setOfIdeal I), x ∈ s
⊢ GaloisConnection (α := Ideal C(X, R)) setOfIdeal (idealOfSet R)

Tactic:
refine fun I s => ⟨fun h f hf => ?_, fun h x hx => ?_⟩
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
I : Ideal C(X, R)
s : Set X
h : setOfIdeal I ≤ s
f : C(X, R)
hf : f ∈ I
refine_1 : ∀ (h' : f ∉ idealOfSet R s), False
⊢ Membership.mem (γ := Submodule C(X, R) C(X, R)) (idealOfSet R s) f

Tactic:
by_contra h'
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : 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
refine_1 : ∀ (x : X) (hx : x ∈ sᶜ) (hfx : Ne.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)), False
⊢ False

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

Premises used: ContinuousMap.notMem_idealOfSet, Iff.mp
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : 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 : Ne.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)
⊢ False

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

Premises used: mt, ContinuousMap.notMem_setOfIdeal, Iff.mp
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : 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 : Ne.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)
⊢ False

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

Premises used: mt, ContinuousMap.notMem_setOfIdeal, Iff.mp
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : IsTopologicalSemiring R
I : Ideal C(X, R)
s : Set X
h : I ≤ idealOfSet R s
x : X
hx : x ∈ setOfIdeal I
refine_2 : ∀ (f : C(X, R)) (hf : f ∈ I) (hfx : Ne.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)), x ∈ s
⊢ x ∈ s

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

Premises used: Iff.mp, ContinuousMap.mem_setOfIdeal
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : 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 : Ne.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)
refine_2 : ∀ (hx' : x ∉ s), False
⊢ x ∈ s

Tactic:
by_contra hx'
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : 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 : Ne.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)
hx' : x ∉ s
⊢ False

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

Premises used: Iff.mpr, ContinuousMap.notMem_idealOfSet, And.intro, Exists.intro
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
R : Type u_2
inst : TopologicalSpace X
inst_1 : Semiring R
inst_2 : TopologicalSpace R
inst_3 : 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 : Ne.{u_2 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)
hx' : x ∉ s
⊢ False

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

Premises used: Iff.mpr, ContinuousMap.notMem_idealOfSet, And.intro, Exists.intro
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
inst : TopologicalSpace X
f : C(X, ℝ≥0)
c : ℝ≥0
hc : 0 < c
x : X
hx : Membership.mem (γ := Set X) {x : X | c ≤ (f : (a : X) → ℝ≥0) x} x
⊢ Eq (α := ℝ≥0)
    (({ toFun := ((⇑f : (a : X) → ℝ≥0) ⊔ (⇑(const X c) : (a : X) → ℝ≥0))⁻¹, continuous_toFun := ⋯ : C(X, ℝ≥0) } * f :
          (a : X) → ℝ≥0)
        x :
      ℝ≥0)
    (1 x : ℝ≥0)

Tactic:
simpa only [coe_const, mul_apply, coe_mk, Pi.inv_apply, Pi.sup_apply,
      Function.const_apply, sup_eq_left.mpr (Set.mem_setOf.mp hx), ne_eq, Pi.one_apply]
      using inv_mul_cancel₀ (hc.trans_le hx).ne'

Premises used: Function.const_apply, Iff.mpr, Pi.one_apply, sup_eq_left, ne_eq, Set.mem_setOf, LT.lt.ne', Pi.sup_apply, LT.lt.trans_le, ContinuousMap.coe_mk, Iff.mp, ContinuousMap.coe_const, inv_mul_cancel₀, ContinuousMap.mul_apply, Pi.inv_apply
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
⊢ Eq (α := Ideal C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) I.closure

Tactic:
le_antisymm ?_
      ((idealOfSet_closed 𝕜 <| setOfIdeal I).closure_subset_iff.mpr fun f hf x hx =>
        notMem_setOfIdeal.mp hx hf)

Premises used: Iff.mpr, ContinuousMap.idealOfSet_closed, ContinuousMap.notMem_setOfIdeal, IsClosed.closure_subset_iff, ContinuousMap.setOfIdeal, le_antisymm, Iff.mp
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
refine : LE.le (α := Ideal C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) I.closure
⊢ Eq (α := Ideal C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) I.closure

Tactic:
refine le_antisymm ?_
      ((idealOfSet_closed 𝕜 <| setOfIdeal I).closure_subset_iff.mpr fun f hf x hx =>
        notMem_setOfIdeal.mp hx hf)

Premises used: Iff.mpr, ContinuousMap.idealOfSet_closed, ContinuousMap.notMem_setOfIdeal, IsClosed.closure_subset_iff, ContinuousMap.setOfIdeal, le_antisymm, Iff.mp
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
⊢ LE.le (α := Ideal C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) I.closure

Tactic:
(fun f hf => Metric.mem_closure_iff.mpr fun ε hε => ?_)

Premises used: Iff.mpr, Set.Mem, setOf, Metric.mem_closure_iff, closure, Set.sInter
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
refine :
  ∀ (f : C(X, 𝕜)) (hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f) (ε : ℝ)
    (hε : ε > 0), ∃ b ∈ (↑I : Set C(X, 𝕜)), dist f b < ε
⊢ LE.le (α := Ideal C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) I.closure

Tactic:
refine (fun f hf => Metric.mem_closure_iff.mpr fun ε hε => ?_)

Premises used: Iff.mpr, Metric.mem_closure_iff
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f
ε : ℝ
hε : ε > 0
⊢ 0 ≤ ε

Tactic:
hε.lt.le

Premises used: GT.gt.lt, LT.lt.le
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f
ε : ℝ
hε : ε > 0
lift : ∀ (ε : ℝ≥0) (hε : (↑ε : ℝ) > 0), ∃ b ∈ (↑I : Set C(X, 𝕜)), dist f b < (↑ε : ℝ)
⊢ ∃ b ∈ (↑I : Set C(X, 𝕜)), dist f b < ε

Tactic:
lift ε to ℝ≥0 using hε.lt.le

Premises used: GT.gt.lt, LT.lt.le
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f
ε : ℝ≥0
hε : (↑ε : ℝ) > 0
⊢ 0 < ε

Tactic:
replace hε := show (0 : ℝ≥0) < ε from hε
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x : X | ε / 2 ≤ nnnorm.{u_2} (E := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)}
⊢ IsClosed t

Tactic:
have ht : IsClosed t := isClosed_le continuous_const (map_continuous f).nnnorm
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x : X | ε / 2 ≤ nnnorm.{u_2} (E := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)}
ht : IsClosed t
⊢ Disjoint t (setOfIdeal I)ᶜ

Tactic:
Set.subset_compl_iff_disjoint_left.mp fun x hx => ?_

Premises used: Set.subset_compl_iff_disjoint_left, Iff.mp
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x : X | ε / 2 ≤ nnnorm.{u_2} (E := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)}
ht : IsClosed t
refine : ∀ (x : X) (hx : x ∈ (setOfIdeal I)ᶜ), x ∈ tᶜ
⊢ Disjoint t (setOfIdeal I)ᶜ

Tactic:
refine Set.subset_compl_iff_disjoint_left.mp fun x hx => ?_

Premises used: Set.subset_compl_iff_disjoint_left, Iff.mp
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x : X | ε / 2 ≤ nnnorm.{u_2} (E := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)}
ht : IsClosed t
x : X
hx : x ∈ (setOfIdeal I)ᶜ
⊢ x ∈ tᶜ

Tactic:
simpa only [t, Set.mem_setOf, Set.mem_compl_iff, not_le] using
      (nnnorm_eq_zero.mpr (mem_idealOfSet.mp hf hx)).trans_lt (half_pos hε)

Premises used: not_le, Iff.mpr, ContinuousMap.mem_idealOfSet, half_pos, Set.mem_setOf, nnnorm_eq_zero, Eq.trans_lt, Iff.mp, Set.mem_compl_iff
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x : X | ε / 2 ≤ nnnorm.{u_2} (E := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)}
ht : IsClosed t
⊢ Disjoint t (setOfIdeal I)ᶜ

Tactic:
have htI : Disjoint t (setOfIdeal I)ᶜ := by
    refine Set.subset_compl_iff_disjoint_left.mp fun x hx => ?_
    simpa only [t, Set.mem_setOf, Set.mem_compl_iff, not_le] using
      (nnnorm_eq_zero.mpr (mem_idealOfSet.mp hf hx)).trans_lt (half_pos hε)
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x : X | ε / 2 ≤ nnnorm.{u_2} (E := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
this :
  ∃ (g : C(X, ℝ≥0)),
    comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g ∈ I ∧
      (∀ (x : X), LE.le (α := ℝ≥0) ((g : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)) ∧
        Set.EqOn (β := ℝ≥0) (⇑g : (a : X) → ℝ≥0) 1 t
obtain :
  ∀ (g : C(X, ℝ≥0)) (hgI : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g ∈ I)
    (hg : ∀ (x : X), LE.le (α := ℝ≥0) ((g : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0))
    (hgt : Set.EqOn (β := ℝ≥0) (⇑g : (a : X) → ℝ≥0) 1 t), ∃ b ∈ (↑I : Set C(X, 𝕜)), nndist f b < ε
⊢ ∃ b ∈ (↑I : Set C(X, 𝕜)), nndist f b < ε

Tactic:
obtain ⟨g, hgI, hg, hgt⟩ := this
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x : X | ε / 2 ≤ nnnorm.{u_2} (E := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
g : C(X, ℝ≥0)
hgI : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g ∈ I
hg : ∀ (x : X), LE.le (α := ℝ≥0) ((g : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
hgt : Set.EqOn (β := ℝ≥0) (⇑g : (a : X) → ℝ≥0) 1 t
⊢ ∃ b ∈ (↑I : Set C(X, 𝕜)), nndist f b < ε

Tactic:
⟨f * (algebraMapCLM ℝ≥0 𝕜 : C(ℝ≥0, 𝕜)).comp g, I.mul_mem_left f hgI, ?_⟩

Premises used: HMul.hMul, algebraMapCLM, ContinuousMap.comp, NNReal, toContinuousMap, And.intro, Exists.intro, Ideal.mul_mem_left
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x : X | ε / 2 ≤ nnnorm.{u_2} (E := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
g : C(X, ℝ≥0)
hgI : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g ∈ I
hg : ∀ (x : X), LE.le (α := ℝ≥0) ((g : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
hgt : Set.EqOn (β := ℝ≥0) (⇑g : (a : X) → ℝ≥0) 1 t
refine : nndist f (f * comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g) < ε
⊢ ∃ b ∈ (↑I : Set C(X, 𝕜)), nndist f b < ε

Tactic:
refine ⟨f * (algebraMapCLM ℝ≥0 𝕜 : C(ℝ≥0, 𝕜)).comp g, I.mul_mem_left f hgI, ?_⟩
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x : X | ε / 2 ≤ nnnorm.{u_2} (E := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
g : C(X, ℝ≥0)
hgI : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g ∈ I
hg : ∀ (x : X), LE.le (α := ℝ≥0) ((g : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
hgt : Set.EqOn (β := ℝ≥0) (⇑g : (a : X) → ℝ≥0) 1 t
rw : ‖f - f * comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g‖₊ < ε
⊢ nndist f (f * comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g) < ε

Tactic:
rw [nndist_eq_nnnorm]

Premises used: nndist_eq_nnnorm
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x : X | ε / 2 ≤ nnnorm.{u_2} (E := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
g : C(X, ℝ≥0)
hgI : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g ∈ I
hg : ∀ (x : X), LE.le (α := ℝ≥0) ((g : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
hgt : Set.EqOn (β := ℝ≥0) (⇑g : (a : X) → ℝ≥0) 1 t
⊢ ‖f - f * comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g‖₊ < ε

Tactic:
(nnnorm_lt_iff _ hε).2 fun x => ?_

Premises used: Iff.mpr, ContinuousMap.nnnorm_lt_iff
-- Module: Mathlib.Topology.ContinuousMap.Ideals
Goal:
X : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
inst_3 : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : Membership.mem (γ := Submodule C(X, 𝕜) C(X, 𝕜)) (idealOfSet 𝕜 (setOfIdeal I)) f
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x : X | ε / 2 ≤ nnnorm.{u_2} (E := 𝕜) ((f : (a : X) → 𝕜) x : 𝕜)}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
g : C(X, ℝ≥0)
hgI : comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g ∈ I
hg : ∀ (x : X), LE.le (α := ℝ≥0) ((g : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
hgt : Set.EqOn (β := ℝ≥0) (⇑g : (a : X) → ℝ≥0) 1 t
refine :
  ∀ (x : X), nnnorm.{u_2} (E := 𝕜) ((f - f * comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g : (a : X) → 𝕜) x : 𝕜) < ε
⊢ ‖f - f * comp (↑(algebraMapCLM ℝ≥0 𝕜) : C(ℝ≥0, 𝕜)) g‖₊ < ε

Tactic:
refine (nnnorm_lt_iff _ hε).2 fun x => ?_

Premises used: Iff.mpr, ContinuousMap.nnnorm_lt_iff