awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
s : Set α
inst_1 : Preorder β
⊢ LowerSemicontinuousOn f s ↔ ∀ (b : β), ∃ (u : Set α), IsOpen[inst] u ∧ s ∩ f ⁻¹' Ioi b = s ∩ u

Tactic:
simp only [← lowerSemicontinuous_restrict_iff, restrict_eq,
    lowerSemicontinuous_iff_isOpen_preimage, preimage_comp, isOpen_induced_iff,
    Subtype.preimage_coe_eq_preimage_coe_iff, eq_comm]

Premises used: Set.preimage_comp, eq_comm, lowerSemicontinuous_restrict_iff, Set.restrict_eq, lowerSemicontinuous_iff_isOpen_preimage, Subtype.preimage_coe_eq_preimage_coe_iff, isOpen_induced_iff
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s : Set α
ι : Type u_4
f : ι → α → β
inst_1 : Preorder β
I : Set ι
hfy : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
M : α → ι
M_mem : ∀ x ∈ s, M x ∈ I
M_max : ∀ x ∈ s, IsMaxOn.{u_4, u_2} (β := β) (fun (y : ι) ↦ f y x) I (M x)
x : α
hx : x ∈ s
b : β
hb : (fun (x : α) ↦ f (M x) x) x > b
apply :
  ∀ᶠ (x_1 : α) in 𝓝[s] x,
    (fun (x1 : α) (x2 : β) ↦ f (M x) x1 > x2) x_1 b → (fun (x1 : α) (x2 : β) ↦ (fun (x : α) ↦ f (M x) x) x1 > x2) x_1 b
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : β) ↦ (fun (x : α) ↦ f (M x) x) x1 > x2) x' b

Tactic:
apply Filter.Eventually.mp <| hfy (M x) (M_mem x hx) x hx b hb

Premises used: Filter.Eventually.mp
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s : Set α
ι : Type u_4
f : ι → α → β
inst_1 : Preorder β
I : Set ι
hfy : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
M : α → ι
M_mem : ∀ x ∈ s, M x ∈ I
M_max : ∀ x ∈ s, IsMaxOn.{u_4, u_2} (β := β) (fun (y : ι) ↦ f y x) I (M x)
x : α
hx : x ∈ s
b : β
hb : (fun (x : α) ↦ f (M x) x) x > b
h :
  ∀ x_1 ∈ s,
    (fun (x1 : α) (x2 : β) ↦ f (M x) x1 > x2) x_1 b → (fun (x1 : α) (x2 : β) ↦ (fun (x : α) ↦ f (M x) x) x1 > x2) x_1 b
⊢ ∀ᶠ (x_1 : α) in 𝓝[s] x,
    (fun (x1 : α) (x2 : β) ↦ f (M x) x1 > x2) x_1 b → (fun (x1 : α) (x2 : β) ↦ (fun (x : α) ↦ f (M x) x) x1 > x2) x_1 b

Tactic:
apply eventually_nhdsWithin_of_forall

Premises used: eventually_nhdsWithin_of_forall
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s : Set α
ι : Type u_4
f : ι → α → β
inst_1 : Preorder β
I : Set ι
hfy : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
M : α → ι
M_mem : ∀ x ∈ s, M x ∈ I
M_max : ∀ x ∈ s, IsMaxOn.{u_4, u_2} (β := β) (fun (y : ι) ↦ f y x) I (M x)
x : α
hx : x ∈ s
b : β
hb : (fun (x : α) ↦ f (M x) x) x > b
z : α
hz : z ∈ s
h : f (M x) z > b
⊢ (fun (x : α) ↦ f (M x) x) z > b

Tactic:
lt_of_lt_of_le h (M_max z hz (M_mem x hx))

Premises used: lt_of_lt_of_le
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s : Set α
ι : Type u_4
f : ι → α → β
inst_1 : Preorder β
I : Set ι
hfy : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
M : α → ι
M_mem : ∀ x ∈ s, M x ∈ I
M_max : ∀ x ∈ s, IsMaxOn.{u_4, u_2} (β := β) (fun (y : ι) ↦ f y x) I (M x)
x : α
hx : x ∈ s
b : β
hb : (fun (x : α) ↦ f (M x) x) x > b
z : α
hz : z ∈ s
h : f (M x) z > b
⊢ (fun (x : α) ↦ f (M x) x) z > b

Tactic:
exact lt_of_lt_of_le h (M_max z hz (M_mem x hx))

Premises used: lt_of_lt_of_le
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s : Set α
ι : Type u_4
f : ι → α → β
inst_1 : Preorder β
I : Set ι
hfy : ∀ i ∈ I, UpperSemicontinuousOn (f i) s
m : α → ι
m_mem : ∀ x ∈ s, m x ∈ I
m_min : ∀ x ∈ s, IsMinOn.{u_4, u_2} (β := β) (fun (i : ι) ↦ f i x) I (m x)
⊢ UpperSemicontinuousOn.{u_1, u_2} (β := β) (fun (x : α) ↦ f (m x) x) s

Tactic:
lowerSemicontinuousOn_of_forall_isMaxOn_and_mem (β := βᵒᵈ) hfy m_mem m_min

Premises used: OrderDual, lowerSemicontinuousOn_of_forall_isMaxOn_and_mem
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
γ : Type u_4
inst_1 : LinearOrder γ
f : α → γ
rw : (∀ (y : γ), IsOpen[inst] (f ⁻¹' Ioi y)) ↔ ∀ (y : γ), IsClosed[inst] (f ⁻¹' Iic y)
⊢ LowerSemicontinuous f ↔ ∀ (y : γ), IsClosed[inst] (f ⁻¹' Iic y)

Tactic:
rw [lowerSemicontinuous_iff_isOpen_preimage]

Premises used: lowerSemicontinuous_iff_isOpen_preimage
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
γ : Type u_4
inst_1 : LinearOrder γ
f : α → γ
⊢ (∀ (y : γ), IsOpen[inst] (f ⁻¹' Ioi y)) ↔ ∀ (y : γ), IsClosed[inst] (f ⁻¹' Iic y)

Tactic:
simp only [← isOpen_compl_iff, ← preimage_compl, compl_Iic]

Premises used: Set.compl_Iic, Set.preimage_compl, isOpen_compl_iff
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
γ : Type u_4
inst_1 : LinearOrder γ
f : α → γ
hf : LowerSemicontinuous f
y : γ
⊢ IsClosed[inst] (f ⁻¹' Iic y)

Tactic:
lowerSemicontinuous_iff_isClosed_preimage.1 hf y

Premises used: lowerSemicontinuous_iff_isClosed_preimage, Iff.mp
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
γ : Type u_4
inst_1 : LinearOrder γ
f : α → γ
⊢ LowerSemicontinuousOn f s ↔ ∀ (b : γ), ∃ (v : Set α), IsClosed[inst] v ∧ s ∩ f ⁻¹' Iic b = s ∩ v

Tactic:
simp only [← lowerSemicontinuous_restrict_iff, restrict_eq,
      lowerSemicontinuous_iff_isClosed_preimage, preimage_comp,
      isClosed_induced_iff, Subtype.preimage_coe_eq_preimage_coe_iff, eq_comm]

Premises used: lowerSemicontinuous_iff_isClosed_preimage, Set.preimage_comp, eq_comm, isClosed_induced_iff, lowerSemicontinuous_restrict_iff, Set.restrict_eq, Subtype.preimage_coe_eq_preimage_coe_iff
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
f : α → γ
h : ContinuousWithinAt f s x
⊢ LowerSemicontinuousWithinAt f s x

Tactic:
fun _y hy => h (Ioi_mem_nhds hy)

Premises used: Ioi_mem_nhds, Set.Mem, Filter.Eventually, setOf, Set.preimage, SemicontinuousWithinAt
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
f : α → γ
h : ContinuousAt f x
⊢ LowerSemicontinuousAt f x

Tactic:
fun _y hy => h (Ioi_mem_nhds hy)

Premises used: Ioi_mem_nhds, Set.Mem, Filter.Eventually, setOf, Set.preimage, SemicontinuousAt
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
f : α → γ
h : ContinuousOn f s
⊢ LowerSemicontinuousOn f s

Tactic:
fun x hx => (h x hx).lowerSemicontinuousWithinAt

Premises used: ContinuousWithinAt.lowerSemicontinuousWithinAt, SemicontinuousOn
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
f : α → γ
h : Continuous[inst, inst_2] f
⊢ LowerSemicontinuous f

Tactic:
fun _x => h.continuousAt.lowerSemicontinuousAt

Premises used: Continuous.continuousAt, Semicontinuous, ContinuousAt.lowerSemicontinuousAt
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst_1 : CompleteLinearOrder γ
f : α → γ
mp : LowerSemicontinuousWithinAt f s x → f x ≤ liminf f (𝓝[s] x)
mpr : f x ≤ liminf f (𝓝[s] x) → LowerSemicontinuousWithinAt f s x
⊢ LowerSemicontinuousWithinAt f s x ↔ f x ≤ liminf f (𝓝[s] x)

Tactic:
constructor
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst_1 : CompleteLinearOrder γ
f : α → γ
h : SemicontinuousWithinAt (fun (x1 : α) (x2 : γ) ↦ f x1 > x2) s x
mp : ∀ (hf : liminf f (𝓝[s] x) < f x), False
⊢ f x ≤ liminf f (𝓝[s] x)

Tactic:
by_contra! hf
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst_1 : CompleteLinearOrder γ
f : α → γ
h : SemicontinuousWithinAt (fun (x1 : α) (x2 : γ) ↦ f x1 > x2) s x
hf : liminf f (𝓝[s] x) < f x
mp : ∀ (z : γ) (ltz : z > liminf f (𝓝[s] x)) (y : γ) (ylt : y < f x) (h₁ : ∀ x < z, ∀ y_1 > y, x < y_1), False
⊢ False

Tactic:
obtain ⟨z, ltz, y, ylt, h₁⟩ := hf.exists_disjoint_Iio_Ioi

Premises used: LT.lt.exists_disjoint_Iio_Ioi
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst_1 : CompleteLinearOrder γ
f : α → γ
h : SemicontinuousWithinAt (fun (x1 : α) (x2 : γ) ↦ f x1 > x2) s x
hf : liminf f (𝓝[s] x) < f x
z : γ
ltz : z > liminf f (𝓝[s] x)
y : γ
ylt : y < f x
h₁ : ∀ x < z, ∀ y_1 > y, x < y_1
⊢ IsCoboundedUnder (fun (x1 x2 : γ) ↦ x1 ≥ x2) (𝓝[s] x) f

Tactic:
isBoundedDefault
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst_1 : CompleteLinearOrder γ
f : α → γ
h : SemicontinuousWithinAt (fun (x1 : α) (x2 : γ) ↦ f x1 > x2) s x
hf : liminf f (𝓝[s] x) < f x
z : γ
ltz : z > liminf f (𝓝[s] x)
y : γ
ylt : y < f x
h₁ : ∀ x < z, ∀ y_1 > y, x < y_1
⊢ False

Tactic:
exact ltz.not_ge
      (le_liminf_of_le (by isBoundedDefault) ((h y ylt).mono fun _ h₂ =>
        le_of_not_gt fun h₃ => (h₁ _ h₃ _ h₂).false))

Premises used: le_of_not_gt, Filter.Eventually.mono, LT.lt.false, LT.lt.not_ge, Filter.le_liminf_of_le
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst_1 : CompleteLinearOrder γ
f : α → γ
⊢ f x ≤ liminf f (𝓝[s] x) → LowerSemicontinuousWithinAt f s x

Tactic:
fun hf y ylt => eventually_lt_of_lt_liminf (ylt.trans_le hf)

Premises used: Filter.eventually_lt_of_lt_liminf, LT.lt.trans_le, SemicontinuousWithinAt
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst_1 : CompleteLinearOrder γ
f : α → γ
⊢ f x ≤ liminf f (𝓝[s] x) → LowerSemicontinuousWithinAt f s x

Tactic:
exact fun hf y ylt => eventually_lt_of_lt_liminf (ylt.trans_le hf)

Premises used: Filter.eventually_lt_of_lt_liminf
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
γ : Type u_4
inst_1 : CompleteLinearOrder γ
f : α → γ
rw : LowerSemicontinuousWithinAt f univ x ↔ f x ≤ liminf f (𝓝 x)
rw₁ : f x ≤ liminf f (𝓝[univ] x) ↔ f x ≤ liminf f (𝓝 x)
rw₂ rw₃ : f x ≤ liminf f (𝓝[univ] x) ↔ f x ≤ liminf f (𝓝[univ] x)
⊢ LowerSemicontinuousAt f x ↔ f x ≤ liminf f (𝓝 x)

Tactic:
rw [← lowerSemicontinuousWithinAt_univ_iff, lowerSemicontinuousWithinAt_iff_le_liminf,
    ← nhdsWithin_univ]

Premises used: nhdsWithin_univ, lowerSemicontinuousWithinAt_univ_iff, lowerSemicontinuousWithinAt_iff_le_liminf
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
γ : Type u_4
inst_1 : CompleteLinearOrder γ
f : α → γ
⊢ LowerSemicontinuous f ↔ ∀ (x : α), f x ≤ liminf f (𝓝 x)

Tactic:
simp only [← lowerSemicontinuousAt_iff_le_liminf, lowerSemicontinuous_iff]

Premises used: lowerSemicontinuousAt_iff_le_liminf, lowerSemicontinuous_iff
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
γ : Type u_4
inst_1 : CompleteLinearOrder γ
f : α → γ
⊢ LowerSemicontinuousOn f s ↔ ∀ x ∈ s, f x ≤ liminf f (𝓝[s] x)

Tactic:
simp only [← lowerSemicontinuousWithinAt_iff_le_liminf, lowerSemicontinuousOn_iff]

Premises used: lowerSemicontinuousWithinAt_iff_le_liminf, lowerSemicontinuousOn_iff
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
γ : Type u_4
inst_1 : LinearOrder γ
f : α → γ
hfs : LowerSemicontinuousOn f s
ks : IsCompact s
c : γ
rw :
  ∀ (hfs : ∀ (b : γ), ∃ (v : Set α), IsClosed[inst] v ∧ s ∩ f ⁻¹' Iic b = s ∩ v) (ks : IsCompact s) (c : γ),
    IsCompact (s ∩ f ⁻¹' Iic c)
⊢ IsCompact (s ∩ f ⁻¹' Iic c)

Tactic:
rw [lowerSemicontinuousOn_iff_preimage_Iic] at hfs

Premises used: lowerSemicontinuousOn_iff_preimage_Iic
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
γ : Type u_4
inst_1 : LinearOrder γ
f : α → γ
hfs : ∀ (b : γ), ∃ (v : Set α), IsClosed[inst] v ∧ s ∩ f ⁻¹' Iic b = s ∩ v
ks : IsCompact s
c : γ
obtain : ∀ (v : Set α) (hv : IsClosed[inst] v) (hv' : s ∩ f ⁻¹' Iic c = s ∩ v), IsCompact (s ∩ f ⁻¹' Iic c)
⊢ IsCompact (s ∩ f ⁻¹' Iic c)

Tactic:
obtain ⟨v, hv, hv'⟩ := hfs c
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
γ : Type u_4
inst_1 : LinearOrder γ
f : α → γ
hfs : ∀ (b : γ), ∃ (v : Set α), IsClosed[inst] v ∧ s ∩ f ⁻¹' Iic b = s ∩ v
ks : IsCompact s
c : γ
v : Set α
hv : IsClosed[inst] v
hv' : s ∩ f ⁻¹' Iic c = s ∩ v
⊢ IsCompact (s ∩ f ⁻¹' Iic c)

Tactic:
hv' ▸ ks.inter_right hv

Premises used: Eq.rec, IsCompact.inter_right, Eq.symm
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
γ : Type u_4
inst_1 : LinearOrder γ
f : α → γ
hfs : ∀ (b : γ), ∃ (v : Set α), IsClosed[inst] v ∧ s ∩ f ⁻¹' Iic b = s ∩ v
ks : IsCompact s
c : γ
v : Set α
hv : IsClosed[inst] v
hv' : s ∩ f ⁻¹' Iic c = s ∩ v
⊢ IsCompact (s ∩ f ⁻¹' Iic c)

Tactic:
exact hv' ▸ ks.inter_right hv
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
γ : Type u_4
inst_1 : LinearOrder γ
ι : Type u_5
f : ι → α → γ
ks : IsCompact s
I : Set ι
c : γ
hfi : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
⊢ s ∩ ⋂ i ∈ I, f i ⁻¹' Iic c = ∅ ↔ ∃ (u : Finset (↑I : Type u_5)), ∀ x ∈ s, ∃ i ∈ u, c < f (↑i : ι) x

Tactic:
⟨fun H ↦ ?_, fun ⟨u, hu⟩ ↦ ?_⟩

Premises used: Set.iInter, Inter.inter, Set.preimage, _private.0.LowerSemicontinuousOn.inter_biInter_preimage_Iic_eq_empty_iff_exists_finset.match_1, Iff.intro, Set.Iic, EmptyCollection.emptyCollection, Eq
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
γ : Type u_4
inst_1 : LinearOrder γ
ι : Type u_5
f : ι → α → γ
ks : IsCompact s
I : Set ι
c : γ
hfi : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
refine_1 : ∀ (H : s ∩ ⋂ i ∈ I, f i ⁻¹' Iic c = ∅), ∃ (u : Finset (↑I : Type u_5)), ∀ x ∈ s, ∃ i ∈ u, c < f (↑i : ι) x
refine_2 :
  (∃ (u : Finset (↑I : Type u_5)), ∀ x ∈ s, ∃ i ∈ u, c < f (↑i : ι) x) →
    ∀ (u : Finset (↑I : Type u_5)) (hu : ∀ x ∈ s, ∃ i ∈ u, c < f (↑i : ι) x), s ∩ ⋂ i ∈ I, f i ⁻¹' Iic c = ∅
⊢ s ∩ ⋂ i ∈ I, f i ⁻¹' Iic c = ∅ ↔ ∃ (u : Finset (↑I : Type u_5)), ∀ x ∈ s, ∃ i ∈ u, c < f (↑i : ι) x

Tactic:
refine ⟨fun H ↦ ?_, fun ⟨u, hu⟩ ↦ ?_⟩
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
γ : Type u_4
inst_1 : LinearOrder γ
ι : Type u_5
f : ι → α → γ
ks : IsCompact s
I : Set ι
c : γ
hfi : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
H : s ∩ ⋂ i ∈ I, f i ⁻¹' Iic c = ∅
this : ∀ i ∈ I, IsClosed[instTopologicalSpaceSubtype] (s ↓∩ (fun (i : ι) ↦ f i ⁻¹' Iic c) i)
⊢ ∃ (u : Finset (↑I : Type u_5)), ∀ x ∈ s, ∃ i ∈ u, c < f (↑i : ι) x

Tactic:
simpa [Set.eq_empty_iff_forall_notMem] using
        ks.elim_finite_subfamily_isClosed_subtype _ this H

Premises used: Set.eq_empty_iff_forall_notMem, IsCompact.elim_finite_subfamily_isClosed_subtype
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
γ : Type u_4
inst_1 : LinearOrder γ
ι : Type u_5
f : ι → α → γ
ks : IsCompact s
I : Set ι
c : γ
hfi : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
H : s ∩ ⋂ i ∈ I, f i ⁻¹' Iic c = ∅
refine_1 : ∀ i ∈ I, IsClosed[instTopologicalSpaceSubtype] (s ↓∩ (fun (i : ι) ↦ f i ⁻¹' Iic c) i)
⊢ ∃ (u : Finset (↑I : Type u_5)), ∀ x ∈ s, ∃ i ∈ u, c < f (↑i : ι) x

Tactic:
suffices ∀ i ∈ I, IsClosed (s ↓∩ (fun i ↦ f i ⁻¹' Iic c) i) by
      simpa [Set.eq_empty_iff_forall_notMem] using
        ks.elim_finite_subfamily_isClosed_subtype _ this H
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
γ : Type u_4
inst_1 : LinearOrder γ
ι : Type u_5
f : ι → α → γ
ks : IsCompact s
I : Set ι
c : γ
hfi : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
H : s ∩ ⋂ i ∈ I, f i ⁻¹' Iic c = ∅
⊢ ∀ i ∈ I, IsClosed[instTopologicalSpaceSubtype] (s ↓∩ (fun (i : ι) ↦ f i ⁻¹' Iic c) i)

Tactic:
fun i hi ↦ lowerSemicontinuous_restrict_iff.mpr (hfi i hi) |>.isClosed_preimage c

Premises used: Iff.mpr, Set.Mem, setOf, Set.preimage, lowerSemicontinuous_restrict_iff, LowerSemicontinuous.isClosed_preimage, Set.Iic, Set.restrict
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
γ : Type u_4
inst_1 : LinearOrder γ
ι : Type u_5
f : ι → α → γ
ks : IsCompact s
I : Set ι
c : γ
hfi : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
H : s ∩ ⋂ i ∈ I, f i ⁻¹' Iic c = ∅
⊢ ∀ i ∈ I, IsClosed[instTopologicalSpaceSubtype] (s ↓∩ (fun (i : ι) ↦ f i ⁻¹' Iic c) i)

Tactic:
exact fun i hi ↦ lowerSemicontinuous_restrict_iff.mpr (hfi i hi) |>.isClosed_preimage c

Premises used: Iff.mpr, lowerSemicontinuous_restrict_iff, LowerSemicontinuous.isClosed_preimage
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
γ : Type u_4
inst_1 : LinearOrder γ
ι : Type u_5
f : ι → α → γ
ks : IsCompact s
I : Set ι
c : γ
hfi : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
h : ∃ (u : Finset (↑I : Type u_5)), ∀ x ∈ s, ∃ i ∈ u, c < f (↑i : ι) x
u : Finset (↑I : Type u_5)
hu : ∀ x ∈ s, ∃ i ∈ u, c < f (↑i : ι) x
refine_2 : ∀ (x : α), x ∉ s ∩ ⋂ i ∈ I, f i ⁻¹' Iic c
⊢ s ∩ ⋂ i ∈ I, f i ⁻¹' Iic c = ∅

Tactic:
rw [Set.eq_empty_iff_forall_notMem]

Premises used: Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
γ : Type u_4
inst_1 : LinearOrder γ
ι : Type u_5
f : ι → α → γ
ks : IsCompact s
I : Set ι
c : γ
hfi : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
h : ∃ (u : Finset (↑I : Type u_5)), ∀ x ∈ s, ∃ i ∈ u, c < f (↑i : ι) x
u : Finset (↑I : Type u_5)
hu : ∀ x ∈ s, ∃ i ∈ u, c < f (↑i : ι) x
refine_2 : ∀ x ∈ s, ∃ x_1 ∈ I, c < f x_1 x
⊢ ∀ (x : α), x ∉ s ∩ ⋂ i ∈ I, f i ⁻¹' Iic c

Tactic:
simp only [mem_inter_iff, mem_iInter, mem_preimage, mem_Iic, not_and, not_forall,
      exists_prop, not_le]

Premises used: not_le, Set.mem_inter_iff, exists_prop, Set.mem_iInter, Set.mem_Iic, not_and, Classical.not_forall, Set.mem_preimage
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
γ : Type u_4
inst_1 : LinearOrder γ
ι : Type u_5
f : ι → α → γ
ks : IsCompact s
I : Set ι
c : γ
hfi : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
h : ∃ (u : Finset (↑I : Type u_5)), ∀ x ∈ s, ∃ i ∈ u, c < f (↑i : ι) x
u : Finset (↑I : Type u_5)
hu : ∀ x ∈ s, ∃ i ∈ u, c < f (↑i : ι) x
⊢ ∀ x ∈ s, ∃ x_1 ∈ I, c < f x_1 x

Tactic:
grind
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst] s
simp_rw :
  (∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x) ↔
    ∀ (x : α × γ), (x.1 ∈ s → x.2 < f x.1) → ∀ᶠ (a : α × γ) in 𝓝 x, a.1 ∈ s → a.2 < f a.1
⊢ LowerSemicontinuousOn f s ↔ IsClosed[instTopologicalSpaceProd] {p : α × γ | p.1 ∈ s ∧ f p.1 ≤ p.2}

Tactic:
simp_rw [lowerSemicontinuousOn_iff, lowerSemicontinuousWithinAt_iff,
    eventually_nhdsWithin_iff, ← isOpen_compl_iff, compl_setOf, isOpen_iff_eventually, mem_setOf,
    not_and, not_le]

Premises used: not_le, isOpen_iff_eventually, Set.mem_setOf, lowerSemicontinuousWithinAt_iff, eventually_nhdsWithin_iff, lowerSemicontinuousOn_iff, not_and, isOpen_compl_iff, Set.compl_setOf
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst] s
mp :
  (∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x) →
    ∀ (x : α × γ), (x.1 ∈ s → x.2 < f x.1) → ∀ᶠ (a : α × γ) in 𝓝 x, a.1 ∈ s → a.2 < f a.1
mpr :
  (∀ (x : α × γ), (x.1 ∈ s → x.2 < f x.1) → ∀ᶠ (a : α × γ) in 𝓝 x, a.1 ∈ s → a.2 < f a.1) →
    ∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x
⊢ (∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x) ↔
    ∀ (x : α × γ), (x.1 ∈ s → x.2 < f x.1) → ∀ᶠ (a : α × γ) in 𝓝 x, a.1 ∈ s → a.2 < f a.1

Tactic:
constructor
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst] s
hf : ∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x
mp : ∀ (x : α) (y : γ), ((x, y).1 ∈ s → (x, y).2 < f (x, y).1) → ∀ᶠ (a : α × γ) in 𝓝 (x, y), a.1 ∈ s → a.2 < f a.1
⊢ ∀ (x : α × γ), (x.1 ∈ s → x.2 < f x.1) → ∀ᶠ (a : α × γ) in 𝓝 x, a.1 ∈ s → a.2 < f a.1

Tactic:
⟨x, y⟩
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst] s
hf : ∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x
x : α
y : γ
h : (x, y).1 ∈ s → (x, y).2 < f (x, y).1
pos : ∀ (hx : x ∈ s), ∀ᶠ (a : α × γ) in 𝓝 (x, y), a.1 ∈ s → a.2 < f a.1
neg : ∀ (hx : x ∉ s), ∀ᶠ (a : α × γ) in 𝓝 (x, y), a.1 ∈ s → a.2 < f a.1
⊢ ∀ᶠ (a : α × γ) in 𝓝 (x, y), a.1 ∈ s → a.2 < f a.1

Tactic:
by_cases hx : x ∈ s
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst] s
hf : ∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x
x : α
y : γ
h : (x, y).1 ∈ s → (x, y).2 < f (x, y).1
hx : x ∈ s
pos :
  ∀ (y' : γ) (hy' : y' > (x, y).2) (z : γ) (hz : z < f (x, y).1) (h₁ : ∀ x < y', ∀ y > z, x < y),
    ∀ᶠ (a : α × γ) in 𝓝 (x, y), a.1 ∈ s → a.2 < f a.1
⊢ ∀ᶠ (a : α × γ) in 𝓝 (x, y), a.1 ∈ s → a.2 < f a.1

Tactic:
have ⟨y', hy', z, hz, h₁⟩ := (h hx).exists_disjoint_Iio_Ioi
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst] s
hf : ∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x
x : α
y : γ
h : (x, y).1 ∈ s → (x, y).2 < f (x, y).1
hx : x ∈ s
y' : γ
hy' : y' > (x, y).2
z : γ
hz : z < f (x, y).1
h₁ : ∀ x < y', ∀ y > z, x < y
a : α × γ
h₂ : ∀ (h₂ : a.1 ∈ s → z < f a.1) (h₃ : a.2 < y'), a.1 ∈ s → a.2 < f a.1
⊢ (a.1 ∈ s → z < f a.1) ∧ a.2 < y' → a.1 ∈ s → a.2 < f a.1

Tactic:
⟨h₂, h₃⟩
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst] s
hf : ∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x
x : α
y : γ
h : (x, y).1 ∈ s → (x, y).2 < f (x, y).1
hx : x ∈ s
y' : γ
hy' : y' > (x, y).2
z : γ
hz : z < f (x, y).1
h₁ : ∀ x < y', ∀ y > z, x < y
a : α × γ
h₂ : a.1 ∈ s → z < f a.1
h₃ : a.2 < y'
h₄ : a.1 ∈ s
⊢ a.2 < f a.1

Tactic:
h₁ _ h₃ _ <| h₂ h₄
-- Module: Mathlib.Topology.Semicontinuity.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst] s
hf : ∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x
x : α
y : γ
h : (x, y).1 ∈ s → (x, y).2 < f (x, y).1
hx : x ∈ s
y' : γ
hy' : y' > (x, y).2
z : γ
hz : z < f (x, y).1
h₁ : ∀ x < y', ∀ y > z, x < y
h₂ :
  ∀ (a : α × γ),
    Membership.mem (γ := Set (α × γ))
      {x : α × γ |
        Membership.mem (γ := Set (α × γ)) {x : α × γ | (fun (p : α × γ) ↦ (p.1 ∈ s → z < f p.1) ∧ p.2 < y') x} x →
          Membership.mem (γ := Set (α × γ)) {x : α × γ | (fun (a : α × γ) ↦ a.1 ∈ s → a.2 < f a.1) x} x}
      a
h₃ : ∀ (a : α × γ), (a.1 ∈ s → z < f a.1) ∧ a.2 < y' → a.1 ∈ s → a.2 < f a.1
h₄ : ∀ (a : α × γ) (h₂ : a.1 ∈ s → z < f a.1) (h₃ : a.2 < y') (h₄ : a.1 ∈ s), a.2 < f a.1
⊢ ∀ᶠ (a : α × γ) in 𝓝 (x, y), a.1 ∈ s → a.2 < f a.1

Tactic:
filter_upwards [(hf x hx z hz).prodMk_nhds (eventually_lt_nhds hy')]
        with _ ⟨h₂, h₃⟩ h₄ using h₁ _ h₃ _ <| h₂ h₄

Premises used: eventually_lt_nhds, Filter.Eventually.prodMk_nhds