awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
inst_1 : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : Nonempty α
h_1 : Nonempty.{u_1 + 1} (↑s : Type u_1)
φ : β → Filter α := fun (b : β) ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ (a : (↑s : Type u_1)), φ (f (↑a : α))
x : (↑s : Type u_1)
⊢ pure (↑x : α) ≤ φ (f (↑x : α))

Tactic:
have : (pure x : Filter α) ≤ φ (f x) := le_principal_iff.mpr ⟨x.2, le_refl (f x)⟩
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
inst_1 : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : Nonempty α
h_1 : Nonempty.{u_1 + 1} (↑s : Type u_1)
φ : β → Filter α := fun (b : β) ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ (a : (↑s : Type u_1)), φ (f (↑a : α))
x : (↑s : Type u_1)
this : pure (↑x : α) ≤ φ (f (↑x : α))
⊢ (φ (f (↑x : α))).NeBot

Tactic:
neBot_of_le this

Premises used: Filter.neBot_of_le
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
inst_1 : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : Nonempty α
h_1 : Nonempty.{u_1 + 1} (↑s : Type u_1)
φ : β → Filter α := fun (b : β) ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ (a : (↑s : Type u_1)), φ (f (↑a : α))
x : (↑s : Type u_1)
this : pure (↑x : α) ≤ φ (f (↑x : α))
⊢ (φ (f (↑x : α))).NeBot

Tactic:
exact neBot_of_le this

Premises used: Filter.neBot_of_le
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
inst_1 : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : Nonempty α
h_1 : Nonempty.{u_1 + 1} (↑s : Type u_1)
φ : β → Filter α := fun (b : β) ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ (a : (↑s : Type u_1)), φ (f (↑a : α))
⊢ ℱ.NeBot

Tactic:
have : ℱ.NeBot := by
    apply iInf_neBot_of_directed _ _
    · change Directed GE.ge (fun x ↦ (φ ∘ (fun (a : s) ↦ f ↑a)) x)
      exact Directed.mono_comp GE.ge (fun x y hxy ↦
        principal_mono.mpr (inter_subset_inter_right _ (preimage_mono <| Iic_subset_Iic.mpr hxy)))
        (Std.Total.directed _)
    · intro x
      have : (pure x : Filter α) ≤ φ (f x) := le_principal_iff.mpr ⟨x.2, le_refl (f x)⟩
      exact neBot_of_le this
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
inst_1 : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : Nonempty α
h_1 : Nonempty.{u_1 + 1} (↑s : Type u_1)
φ : β → Filter α := fun (b : β) ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ (a : (↑s : Type u_1)), φ (f (↑a : α))
this : ℱ.NeBot
⊢ ℱ ≤ 𝓟 s

Tactic:
have hℱs : ℱ ≤ 𝓟 s :=
    iInf_le_of_le (Classical.choice inferInstance) (principal_mono.mpr <| inter_subset_left)
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
inst_1 : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : Nonempty α
h_1 : Nonempty.{u_1 + 1} (↑s : Type u_1)
φ : β → Filter α := fun (b : β) ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ (a : (↑s : Type u_1)), φ (f (↑a : α))
this : ℱ.NeBot
hℱs : ℱ ≤ 𝓟 s
x : α
hx : x ∈ s
⊢ {x_1 : α | (fun (y : α) ↦ f y ≤ f x) x_1} ∈ φ (f (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) : α))

Tactic:
apply inter_subset_right

Premises used: Set.inter_subset_right
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
inst_1 : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : Nonempty α
h_1 : Nonempty.{u_1 + 1} (↑s : Type u_1)
φ : β → Filter α := fun (b : β) ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ (a : (↑s : Type u_1)), φ (f (↑a : α))
this : ℱ.NeBot
hℱs : ℱ ≤ 𝓟 s
⊢ ∀ (x : α) (hx : x ∈ s), ∀ᶠ (y : α) in ℱ, f y ≤ f x

Tactic:
have hℱ (x) (hx : x ∈ s) : ∀ᶠ y in ℱ, f y ≤ f x :=
    mem_iInf_of_mem ⟨x, hx⟩ (by apply inter_subset_right)
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
inst_1 : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : Nonempty α
h_1 : Nonempty.{u_1 + 1} (↑s : Type u_1)
φ : β → Filter α := fun (b : β) ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ (a : (↑s : Type u_1)), φ (f (↑a : α))
this : ℱ.NeBot
hℱs : ℱ ≤ 𝓟 s
hℱ : ∀ (x : α) (hx : x ∈ s), ∀ᶠ (y : α) in ℱ, f y ≤ f x
obtain : ∀ (a : α) (ha : a ∈ s) (h : ClusterPt a ℱ), ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x

Tactic:
obtain ⟨a, ha, h⟩ := hs hℱs
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
inst_1 : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h_1 : Nonempty α
h_2 : Nonempty.{u_1 + 1} (↑s : Type u_1)
φ : β → Filter α := fun (b : β) ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ (a : (↑s : Type u_1)), φ (f (↑a : α))
this : ℱ.NeBot
hℱs : ℱ ≤ 𝓟 s
hℱ : ∀ (x : α) (hx : x ∈ s), ∀ᶠ (y : α) in ℱ, f y ≤ f x
a : α
ha : a ∈ s
h : ClusterPt a ℱ
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x

Tactic:
⟨a, ha, fun x hx ↦ le_of_not_gt fun hxa ↦ ?_⟩

Premises used: le_of_not_gt, And.intro, Exists.intro
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
inst_1 : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h_1 : Nonempty α
h_2 : Nonempty.{u_1 + 1} (↑s : Type u_1)
φ : β → Filter α := fun (b : β) ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ (a : (↑s : Type u_1)), φ (f (↑a : α))
this : ℱ.NeBot
hℱs : ℱ ≤ 𝓟 s
hℱ : ∀ (x : α) (hx : x ∈ s), ∀ᶠ (y : α) in ℱ, f y ≤ f x
a : α
ha : a ∈ s
h : ClusterPt a ℱ
refine : ∀ (x : α) (hx : x ∈ s) (hxa : f x < f a), False
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x

Tactic:
refine ⟨a, ha, fun x hx ↦ le_of_not_gt fun hxa ↦ ?_⟩
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
inst_1 : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h_1 : Nonempty α
h_2 : Nonempty.{u_1 + 1} (↑s : Type u_1)
φ : β → Filter α := fun (b : β) ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ (a : (↑s : Type u_1)), φ (f (↑a : α))
this_1 : ℱ.NeBot
hℱs : ℱ ≤ 𝓟 s
hℱ : ∀ (x : α) (hx : x ∈ s), ∀ᶠ (y : α) in ℱ, f y ≤ f x
a : α
ha : a ∈ s
h : ClusterPt a ℱ
x : α
hx : x ∈ s
hxa : f x < f a
h_3 : (𝓝 a ⊓ ℱ).NeBot := h
this : ∀ᶠ (x : α) in 𝓝 a ⊓ ℱ, False
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : False), False
⊢ False

Tactic:
rwa [eventually_const] at this

Premises used: Filter.eventually_const
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
inst_1 : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h_1 : Nonempty α
h_2 : Nonempty.{u_1 + 1} (↑s : Type u_1)
φ : β → Filter α := fun (b : β) ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ (a : (↑s : Type u_1)), φ (f (↑a : α))
this : ℱ.NeBot
hℱs : ℱ ≤ 𝓟 s
hℱ : ∀ (x : α) (hx : x ∈ s), ∀ᶠ (y : α) in ℱ, f y ≤ f x
a : α
ha : a ∈ s
h : ClusterPt a ℱ
x : α
hx : x ∈ s
hxa : f x < f a
h_3 : (𝓝 a ⊓ ℱ).NeBot := h
suffices : ∀ᶠ (x : α) in 𝓝 a ⊓ ℱ, False
⊢ False

Tactic:
suffices ∀ᶠ _ in 𝓝 a ⊓ ℱ, False by rwa [eventually_const] at this
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
inst_1 : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h_1 : Nonempty α
h_2 : Nonempty.{u_1 + 1} (↑s : Type u_1)
φ : β → Filter α := fun (b : β) ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ (a : (↑s : Type u_1)), φ (f (↑a : α))
this : ℱ.NeBot
hℱs : ℱ ≤ 𝓟 s
hℱ : ∀ (x : α) (hx : x ∈ s), ∀ᶠ (y : α) in ℱ, f y ≤ f x
a : α
ha : a ∈ s
h : ClusterPt a ℱ
x : α
hx : x ∈ s
hxa : f x < f a
h_3 : (𝓝 a ⊓ ℱ).NeBot := h
⊢ ∀ (a : α), f a > f x → f a ≤ f x → False

Tactic:
fun y h₁ h₂ ↦ not_le_of_gt h₁ h₂

Premises used: not_le_of_gt
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
inst_1 : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h_1 : Nonempty α
h_2 : Nonempty.{u_1 + 1} (↑s : Type u_1)
φ : β → Filter α := fun (b : β) ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ (a : (↑s : Type u_1)), φ (f (↑a : α))
this : ℱ.NeBot
hℱs : ℱ ≤ 𝓟 s
hℱ : ∀ (x : α) (hx : x ∈ s), ∀ᶠ (y : α) in ℱ, f y ≤ f x
a : α
ha : a ∈ s
h : ClusterPt a ℱ
x : α
hx : x ∈ s
hxa : f x < f a
h_3 : (𝓝 a ⊓ ℱ).NeBot := h
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x_1 : α |
        Membership.mem (γ := Set α)
            {x_2 : α | (fun (x_3 : α) ↦ ((fun (x1 : α) (x2 : β) ↦ f x1 > x2) x_3 (f x) : Prop)) x_2} x_1 →
          Membership.mem (γ := Set α)
            {x_2 : α |
              Membership.mem (γ := Set α) {x_3 : α | (fun (x_4 : α) ↦ f x_4 ≤ f x) x_3} x_2 →
                Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ False) x} x_2}
            x_1}
      a
h₂ : ∀ (a : α), f a > f x → f a ≤ f x → False
⊢ ∀ᶠ (x : α) in 𝓝 a ⊓ ℱ, False

Tactic:
filter_upwards [(hf a ha (f x) hxa).filter_mono (inf_le_inf_left _ hℱs),
    (hℱ x hx).filter_mono (inf_le_right : 𝓝 a ⊓ ℱ ≤ ℱ)] using fun y h₁ h₂ ↦ not_le_of_gt h₁ h₂

Premises used: Filter.Eventually.filter_mono, inf_le_right, inf_le_inf_left, not_le_of_gt
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
inst_1 : LinearOrder β
inst_2 : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : s = ∅
inl : BddBelow.{u_2} (α := β) ∅
⊢ BddBelow (f '' s)

Tactic:
simp only [h, Set.image_empty]

Premises used: Set.image_empty
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
inst_1 : LinearOrder β
inst_2 : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : s = ∅
⊢ BddBelow.{u_2} (α := β) ∅

Tactic:
bddBelow_empty

Premises used: bddBelow_empty
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
inst_1 : LinearOrder β
inst_2 : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : s = ∅
⊢ BddBelow.{u_2} (α := β) ∅

Tactic:
exact bddBelow_empty

Premises used: bddBelow_empty
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
inst_1 : LinearOrder β
inst_2 : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : s.Nonempty
inr : ∀ a ∈ s, ∀ (has : IsMinOn f s a), BddBelow (f '' s)
⊢ BddBelow (f '' s)

Tactic:
obtain ⟨a, _, has⟩ := LowerSemicontinuousOn.exists_isMinOn h hs hf

Premises used: LowerSemicontinuousOn.exists_isMinOn
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
inst_1 : LinearOrder β
inst_2 : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : s.Nonempty
a : α
left : a ∈ s
has : IsMinOn f s a
⊢ BddBelow (f '' s)

Tactic:
has.bddBelow

Premises used: IsMinOn.bddBelow
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
inst_1 : LinearOrder β
inst_2 : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : s.Nonempty
a : α
left : a ∈ s
has : IsMinOn f s a
⊢ BddBelow (f '' s)

Tactic:
exact has.bddBelow

Premises used: IsMinOn.bddBelow
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
inst_1 : LinearOrder β
inst_2 : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
⊢ s = ∅ ∨ s.Nonempty

Tactic:
cases s.eq_empty_or_nonempty with
  | inl h =>
      simp only [h, Set.image_empty]
      exact bddBelow_empty
  | inr h =>
      obtain ⟨a, _, has⟩ := LowerSemicontinuousOn.exists_isMinOn h hs hf
      exact has.bddBelow

Premises used: bddBelow_empty, Set.eq_empty_or_nonempty, Set.image_empty
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s : Set α
y : β
inst_1 : Zero β
inst_2 : Preorder β
hs : IsOpen[inst] s
hy : 0 ≤ y
x : α
z : β
hz : s.indicator (fun (_x : α) ↦ y) x > z
pos : ∀ (h : x ∈ s), ∀ᶠ (x' : α) in 𝓝 x, (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z
neg : ∀ (h : x ∉ s), ∀ᶠ (x' : α) in 𝓝 x, (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z

Tactic:
by_cases h : x ∈ s
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s : Set α
y : β
inst_1 : Zero β
inst_2 : Preorder β
hs : IsOpen[inst] s
hy : 0 ≤ y
x : α
z : β
hz : s.indicator (fun (_x : α) ↦ y) x > z
h : x ∈ s
⊢ z < y

Tactic:
simp [h] at hz
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s : Set α
y : β
inst_1 : Zero β
inst_2 : Preorder β
hs : IsOpen[inst] s
hy : 0 ≤ y
x : α
z : β
hz : s.indicator (fun (_x : α) ↦ y) x > z
h : x ∉ s
⊢ z < 0

Tactic:
simp [h] at hz
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s : Set α
y : β
inst_1 : Zero β
inst_2 : Preorder β
hs : IsOpen[inst] s
hy : 0 ≤ y
x : α
z : β
h : x ∈ s
hz : z < y
h₁ : ∀ a ∈ s, s.indicator (fun (_x : α) ↦ y) a > z
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z

Tactic:
filter_upwards [hs.mem_nhds h]

Premises used: IsOpen.mem_nhds
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s : Set α
y : β
inst_1 : Zero β
inst_2 : Preorder β
hs : IsOpen[inst] s
hy : 0 ≤ y
x : α
z : β
h : x ∈ s
hz : z < y
⊢ ∀ a ∈ s, s.indicator (fun (_x : α) ↦ y) a > z

Tactic:
simp +contextual [hz]
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s : Set α
y : β
inst_1 : Zero β
inst_2 : Preorder β
hs : IsOpen[inst] s
hy : 0 ≤ y
x : α
z : β
h : x ∉ s
hz : z < 0
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z

Tactic:
Filter.Eventually.of_forall fun x' => ?_

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s : Set α
y : β
inst_1 : Zero β
inst_2 : Preorder β
hs : IsOpen[inst] s
hy : 0 ≤ y
x : α
z : β
h : x ∉ s
hz : z < 0
neg : ∀ (x' : α), (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z

Tactic:
refine Filter.Eventually.of_forall fun x' => ?_

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s : Set α
y : β
inst_1 : Zero β
inst_2 : Preorder β
hs : IsOpen[inst] s
hy : 0 ≤ y
x : α
z : β
h : x ∉ s
hz : z < 0
x' : α
pos : ∀ (h' : x' ∈ s), (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z
neg : ∀ (h' : x' ∉ s), (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z
⊢ (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z

Tactic:
by_cases h' : x' ∈ s
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s : Set α
y : β
inst_1 : Zero β
inst_2 : Preorder β
hs : IsOpen[inst] s
hy : 0 ≤ y
x : α
z : β
h : x ∉ s
hz : z < 0
x' : α
h' : x' ∈ s
⊢ (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z

Tactic:
simp [h', hz.trans_le hy, hz]

Premises used: LT.lt.trans_le
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s : Set α
y : β
inst_1 : Zero β
inst_2 : Preorder β
hs : IsOpen[inst] s
hy : 0 ≤ y
x : α
z : β
h : x ∉ s
hz : z < 0
x' : α
h' : x' ∉ s
⊢ (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z

Tactic:
simp [h', hz.trans_le hy, hz]

Premises used: LT.lt.trans_le
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s t : Set α
y : β
inst_1 : Zero β
inst_2 : Preorder β
hs : IsOpen[inst] s
hy : 0 ≤ y
⊢ LowerSemicontinuousOn.{u_1, u_2} (β := β) (s.indicator fun (_x : α) ↦ y) t

Tactic:
(hs.lowerSemicontinuous_indicator hy).lowerSemicontinuousOn t

Premises used: IsOpen.lowerSemicontinuous_indicator, LowerSemicontinuous.lowerSemicontinuousOn
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s : Set α
x : α
y : β
inst_1 : Zero β
inst_2 : Preorder β
hs : IsOpen[inst] s
hy : 0 ≤ y
⊢ LowerSemicontinuousAt.{u_1, u_2} (β := β) (s.indicator fun (_x : α) ↦ y) x

Tactic:
(hs.lowerSemicontinuous_indicator hy).lowerSemicontinuousAt x

Premises used: IsOpen.lowerSemicontinuous_indicator, LowerSemicontinuous.lowerSemicontinuousAt
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s t : Set α
x : α
y : β
inst_1 : Zero β
inst_2 : Preorder β
hs : IsOpen[inst] s
hy : 0 ≤ y
⊢ LowerSemicontinuousWithinAt.{u_1, u_2} (β := β) (s.indicator fun (_x : α) ↦ y) t x

Tactic:
(hs.lowerSemicontinuous_indicator hy).lowerSemicontinuousWithinAt t x

Premises used: IsOpen.lowerSemicontinuous_indicator, LowerSemicontinuous.lowerSemicontinuousWithinAt
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s : Set α
y : β
inst_1 : Zero β
inst_2 : Preorder β
hs : IsClosed[inst] s
hy : y ≤ 0
x : α
z : β
hz : s.indicator (fun (_x : α) ↦ y) x > z
pos : ∀ (h : x ∈ s), ∀ᶠ (x' : α) in 𝓝 x, (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z
neg : ∀ (h : x ∉ s), ∀ᶠ (x' : α) in 𝓝 x, (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z

Tactic:
by_cases h : x ∈ s
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s : Set α
y : β
inst_1 : Zero β
inst_2 : Preorder β
hs : IsClosed[inst] s
hy : y ≤ 0
x : α
z : β
hz : s.indicator (fun (_x : α) ↦ y) x > z
h : x ∈ s
⊢ z < y

Tactic:
simp [h] at hz
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s : Set α
y : β
inst_1 : Zero β
inst_2 : Preorder β
hs : IsClosed[inst] s
hy : y ≤ 0
x : α
z : β
hz : s.indicator (fun (_x : α) ↦ y) x > z
h : x ∉ s
⊢ z < 0

Tactic:
simp [h] at hz
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s : Set α
y : β
inst_1 : Zero β
inst_2 : Preorder β
hs : IsClosed[inst] s
hy : y ≤ 0
x : α
z : β
h : x ∈ s
hz : z < y
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z

Tactic:
Filter.Eventually.of_forall fun x' => ?_

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s : Set α
y : β
inst_1 : Zero β
inst_2 : Preorder β
hs : IsClosed[inst] s
hy : y ≤ 0
x : α
z : β
h : x ∈ s
hz : z < y
pos : ∀ (x' : α), (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z

Tactic:
refine Filter.Eventually.of_forall fun x' => ?_

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s : Set α
y : β
inst_1 : Zero β
inst_2 : Preorder β
hs : IsClosed[inst] s
hy : y ≤ 0
x : α
z : β
h : x ∈ s
hz : z < y
x' : α
pos : ∀ (h' : x' ∈ s), (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z
neg : ∀ (h' : x' ∉ s), (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z
⊢ (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z

Tactic:
by_cases h' : x' ∈ s
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s : Set α
y : β
inst_1 : Zero β
inst_2 : Preorder β
hs : IsClosed[inst] s
hy : y ≤ 0
x : α
z : β
h : x ∈ s
hz : z < y
x' : α
h' : x' ∈ s
⊢ (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z

Tactic:
simp [h', hz, hz.trans_le hy]

Premises used: LT.lt.trans_le
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s : Set α
y : β
inst_1 : Zero β
inst_2 : Preorder β
hs : IsClosed[inst] s
hy : y ≤ 0
x : α
z : β
h : x ∈ s
hz : z < y
x' : α
h' : x' ∉ s
⊢ (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z

Tactic:
simp [h', hz, hz.trans_le hy]

Premises used: LT.lt.trans_le
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s : Set α
y : β
inst_1 : Zero β
inst_2 : Preorder β
hs : IsClosed[inst] s
hy : y ≤ 0
x : α
z : β
h : x ∉ s
hz : z < 0
h₁ : ∀ a ∈ sᶜ, s.indicator (fun (_x : α) ↦ y) a > z
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z

Tactic:
filter_upwards [hs.isOpen_compl.mem_nhds h]

Premises used: IsClosed.isOpen_compl, IsOpen.mem_nhds
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s : Set α
y : β
inst_1 : Zero β
inst_2 : Preorder β
hs : IsClosed[inst] s
hy : y ≤ 0
x : α
z : β
h : x ∉ s
hz : z < 0
⊢ ∀ a ∈ sᶜ, s.indicator (fun (_x : α) ↦ y) a > z

Tactic:
simp +contextual [hz]
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s t : Set α
y : β
inst_1 : Zero β
inst_2 : Preorder β
hs : IsClosed[inst] s
hy : y ≤ 0
⊢ LowerSemicontinuousOn.{u_1, u_2} (β := β) (s.indicator fun (_x : α) ↦ y) t

Tactic:
(hs.lowerSemicontinuous_indicator hy).lowerSemicontinuousOn t

Premises used: IsClosed.lowerSemicontinuous_indicator, LowerSemicontinuous.lowerSemicontinuousOn
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s : Set α
x : α
y : β
inst_1 : Zero β
inst_2 : Preorder β
hs : IsClosed[inst] s
hy : y ≤ 0
⊢ LowerSemicontinuousAt.{u_1, u_2} (β := β) (s.indicator fun (_x : α) ↦ y) x

Tactic:
(hs.lowerSemicontinuous_indicator hy).lowerSemicontinuousAt x

Premises used: IsClosed.lowerSemicontinuous_indicator, LowerSemicontinuous.lowerSemicontinuousAt
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s t : Set α
x : α
y : β
inst_1 : Zero β
inst_2 : Preorder β
hs : IsClosed[inst] s
hy : y ≤ 0
⊢ LowerSemicontinuousWithinAt.{u_1, u_2} (β := β) (s.indicator fun (_x : α) ↦ y) t x

Tactic:
(hs.lowerSemicontinuous_indicator hy).lowerSemicontinuousWithinAt t x

Premises used: IsClosed.lowerSemicontinuous_indicator, LowerSemicontinuous.lowerSemicontinuousWithinAt
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
inst_1 : Preorder β
⊢ LowerSemicontinuous f ↔ ∀ (y : β), IsOpen[inst] (f ⁻¹' Ioi y)

Tactic:
⟨fun H y => isOpen_iff_mem_nhds.2 fun x hx => H x y hx, fun H _x y y_lt =>
    IsOpen.mem_nhds (H y) y_lt⟩

Premises used: Iff.mpr, IsOpen.mem_nhds, Iff.intro, isOpen_iff_mem_nhds
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
inst_1 : Preorder β
hf : LowerSemicontinuous f
y : β
⊢ IsOpen[inst] (f ⁻¹' Ioi y)

Tactic:
lowerSemicontinuous_iff_isOpen_preimage.1 hf y

Premises used: Iff.mp, lowerSemicontinuous_iff_isOpen_preimage