awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this_1 : Nonempty (PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w))
this :
  ∀ (c : Set (PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w))),
    IsChain (fun (x1 x2 : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)) ↦ x1 ≤ x2) c →
      c.Nonempty → ∃ (ub : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)), ∀ v ∈ c, v ≤ ub
rcases :
  ∀ (v : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)) (hv : IsMax v),
    ∃ (v : ι → Set X),
      s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ (∀ (i : ι), closure (v i) ⊆ u i) ∧ ∀ (i : ι), IsCompact (closure (v i))
⊢ ∃ (v : ι → Set X),
    s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ (∀ (i : ι), closure (v i) ⊆ u i) ∧ ∀ (i : ι), IsCompact (closure (v i))

Tactic:
rcases zorn_le_nonempty this with ⟨v, hv⟩

Premises used: zorn_le_nonempty
-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this_1 : Nonempty (PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w))
this :
  ∀ (c : Set (PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w))),
    IsChain (fun (x1 x2 : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)) ↦ x1 ≤ x2) c →
      c.Nonempty → ∃ (ub : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)), ∀ v ∈ c, v ≤ ub
v : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)
hv : IsMax v
refine_2 :
  ∀ (this : ∀ (i : ι), i ∈ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) (i : ι),
    IsCompact (closure (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i))
refine_1 : ∀ (i : ι), i ∈ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
⊢ ∃ (v : ι → Set X),
    s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ (∀ (i : ι), closure (v i) ⊆ u i) ∧ ∀ (i : ι), IsCompact (closure (v i))

Tactic:
suffices ∀ i, i ∈ v.carrier from
    ⟨v, v.subset_iUnion, fun i => v.isOpen _, fun i => v.closure_subset (this i), ?_⟩
-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this_1 : Nonempty (PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w))
this_2 :
  ∀ (c : Set (PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w))),
    IsChain (fun (x1 x2 : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)) ↦ x1 ≤ x2) c →
      c.Nonempty → ∃ (ub : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)), ∀ v ∈ c, v ≤ ub
v : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)
hv : IsMax v
this : ∀ (i : ι), i ∈ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
i : ι
⊢ IsCompact (closure (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i))

Tactic:
v.pred_of_mem (this i)

Premises used: ShrinkingLemma.PartialRefinement.pred_of_mem
-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this_1 : Nonempty (PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w))
this_2 :
  ∀ (c : Set (PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w))),
    IsChain (fun (x1 x2 : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)) ↦ x1 ≤ x2) c →
      c.Nonempty → ∃ (ub : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)), ∀ v ∈ c, v ≤ ub
v : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)
hv : IsMax v
this : ∀ (i : ι), i ∈ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
i : ι
⊢ IsCompact (closure (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i))

Tactic:
exact v.pred_of_mem (this i)

Premises used: ShrinkingLemma.PartialRefinement.pred_of_mem
-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this_1 : Nonempty (PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w))
this :
  ∀ (c : Set (PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w))),
    IsChain (fun (x1 x2 : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)) ↦ x1 ≤ x2) c →
      c.Nonempty → ∃ (ub : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)), ∀ v ∈ c, v ≤ ub
v : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)
hv : IsMax v
i : ι
refine_1 : ∀ (hi : i ∉ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))), False
⊢ i ∈ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))

Tactic:
by_contra! hi
-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this_1 : Nonempty (PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w))
this :
  ∀ (c : Set (PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w))),
    IsChain (fun (x1 x2 : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)) ↦ x1 ≤ x2) c →
      c.Nonempty → ∃ (ub : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)), ∀ v ∈ c, v ≤ ub
v : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)
hv : IsMax v
i : ι
hi : i ∉ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
refine_1 :
  ∀ (v' : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)) (hlt : v < v'),
    IsCompact (closure (v'.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i)) → False
⊢ False

Tactic:
rcases exists_gt_t2space v hs i hi with ⟨v', hlt, _⟩

Premises used: exists_gt_t2space
-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this_1 : Nonempty (PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w))
this :
  ∀ (c : Set (PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w))),
    IsChain (fun (x1 x2 : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)) ↦ x1 ≤ x2) c →
      c.Nonempty → ∃ (ub : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)), ∀ v ∈ c, v ≤ ub
v : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)
hv : IsMax v
i : ι
hi : i ∉ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
v' : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)
hlt : v < v'
right : IsCompact (closure (v'.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i))
⊢ False

Tactic:
hv.not_lt hlt

Premises used: IsMax.not_lt
-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this_1 : Nonempty (PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w))
this :
  ∀ (c : Set (PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w))),
    IsChain (fun (x1 x2 : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)) ↦ x1 ≤ x2) c →
      c.Nonempty → ∃ (ub : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)), ∀ v ∈ c, v ≤ ub
v : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)
hv : IsMax v
i : ι
hi : i ∉ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
v' : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)
hlt : v < v'
right : IsCompact (closure (v'.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i))
⊢ False

Tactic:
exact hv.not_lt hlt

Premises used: IsMax.not_lt
-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
let :
  ∀ (v : ι → Set X) (hsv : s ⊆ iUnion v),
    (∀ (i : ι), IsOpen (v i)) →
      ∀ (hv : (∀ (i : ι), closure (v i) ⊆ u i) ∧ ∀ (i : ι), IsCompact (closure (v i))),
        ∃ (v : ι → Set X),
          s ⊆ iUnion v ∧ (∀ (i : ι), IsClosed (v i)) ∧ (∀ (i : ι), v i ⊆ u i) ∧ ∀ (i : ι), IsCompact (v i)
⊢ ∃ (v : ι → Set X), s ⊆ iUnion v ∧ (∀ (i : ι), IsClosed (v i)) ∧ (∀ (i : ι), v i ⊆ u i) ∧ ∀ (i : ι), IsCompact (v i)

Tactic:
let ⟨v, hsv, _, hv⟩ := exists_subset_iUnion_closure_subset_t2space hs uo uf us
-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
v : ι → Set X
hsv : s ⊆ iUnion v
left : ∀ (i : ι), IsOpen (v i)
hv : (∀ (i : ι), closure (v i) ⊆ u i) ∧ ∀ (i : ι), IsCompact (closure (v i))
h :
  s ⊆ ⋃ (i : ι), closure (v i) ∧
    (∀ (i : ι), IsClosed.{u_2} (X := X) ((fun (i : ι) ↦ closure (v i)) i)) ∧
      (∀ (i : ι), (fun (i : ι) ↦ closure (v i)) i ⊆ u i) ∧
        ∀ (i : ι), IsCompact.{u_2} (X := X) ((fun (i : ι) ↦ closure (v i)) i)
⊢ ∃ (v : ι → Set X), s ⊆ iUnion v ∧ (∀ (i : ι), IsClosed (v i)) ∧ (∀ (i : ι), v i ⊆ u i) ∧ ∀ (i : ι), IsCompact (v i)

Tactic:
use fun i => closure (v i)

Premises used: closure
-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
v : ι → Set X
hsv : s ⊆ iUnion v
left : ∀ (i : ι), IsOpen (v i)
hv : (∀ (i : ι), closure (v i) ⊆ u i) ∧ ∀ (i : ι), IsCompact (closure (v i))
⊢ s ⊆ ⋃ (i : ι), closure (v i) ∧
    (∀ (i : ι), IsClosed.{u_2} (X := X) ((fun (i : ι) ↦ closure (v i)) i)) ∧
      (∀ (i : ι), (fun (i : ι) ↦ closure (v i)) i ⊆ u i) ∧
        ∀ (i : ι), IsCompact.{u_2} (X := X) ((fun (i : ι) ↦ closure (v i)) i)

Tactic:
⟨?_, ?_, hv⟩

Premises used: And.intro
-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
v : ι → Set X
hsv : s ⊆ iUnion v
left : ∀ (i : ι), IsOpen (v i)
hv : (∀ (i : ι), closure (v i) ⊆ u i) ∧ ∀ (i : ι), IsCompact (closure (v i))
h : s ⊆ ⋃ (i : ι), closure (v i)
h₁ : ∀ (i : ι), IsClosed.{u_2} (X := X) ((fun (i : ι) ↦ closure (v i)) i)
⊢ s ⊆ ⋃ (i : ι), closure (v i) ∧
    (∀ (i : ι), IsClosed.{u_2} (X := X) ((fun (i : ι) ↦ closure (v i)) i)) ∧
      (∀ (i : ι), (fun (i : ι) ↦ closure (v i)) i ⊆ u i) ∧
        ∀ (i : ι), IsCompact.{u_2} (X := X) ((fun (i : ι) ↦ closure (v i)) i)

Tactic:
refine ⟨?_, ?_, hv⟩
-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
v : ι → Set X
hsv : s ⊆ iUnion v
left : ∀ (i : ι), IsOpen (v i)
hv : (∀ (i : ι), closure (v i) ⊆ u i) ∧ ∀ (i : ι), IsCompact (closure (v i))
⊢ s ⊆ ⋃ (i : ι), closure (v i)

Tactic:
Subset.trans hsv (iUnion_mono fun _ => subset_closure)

Premises used: Set.Subset.trans, subset_closure, Set.iUnion_mono
-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
v : ι → Set X
hsv : s ⊆ iUnion v
left : ∀ (i : ι), IsOpen (v i)
hv : (∀ (i : ι), closure (v i) ⊆ u i) ∧ ∀ (i : ι), IsCompact (closure (v i))
⊢ s ⊆ ⋃ (i : ι), closure (v i)

Tactic:
exact Subset.trans hsv (iUnion_mono fun _ => subset_closure)

Premises used: Set.Subset.trans, subset_closure, Set.iUnion_mono
-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
v : ι → Set X
hsv : s ⊆ iUnion v
left : ∀ (i : ι), IsOpen (v i)
hv : (∀ (i : ι), closure (v i) ⊆ u i) ∧ ∀ (i : ι), IsCompact (closure (v i))
⊢ ∀ (i : ι), IsClosed.{u_2} (X := X) ((fun (i : ι) ↦ closure (v i)) i)

Tactic:
simp only [isClosed_closure, implies_true]

Premises used: implies_true, isClosed_closure
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
b : β
y : (↑Y : Type u_2)
x : (↑X : Type u_1)
⊢ x ∈ sublevelLeft X f b (↑y : F) ↔ f (↑x : E) (↑y : F) ≤ b

Tactic:
simp [sublevelLeft]

Premises used: _private.0.Sion.sublevelLeft
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
u v : β
y : (↑Y : Type u_2)
h : u ≤ v
⊢ sublevelLeft X f u (↑y : F) ⊆ sublevelLeft X f v (↑y : F)

Tactic:
fun _ hxu ↦ le_trans hxu h

Premises used: _private.0.Sion.sublevelLeft, Set.Mem, setOf, Set.Subset, Set.preimage, Set.Iic, le_trans
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
a : E
b : β
y y' : (↑Y : Type u_2)
ha : ∀ x ∈ X, max (f a (↑y : F)) (f a (↑y' : F)) ≤ max (f x (↑y : F)) (f x (↑y' : F))
hb : b < max (f a (↑y : F)) (f a (↑y' : F))
rw : sublevelLeft X f b (↑y : F) ∩ sublevelLeft X f b (↑y' : F) ⊆ ∅
⊢ Disjoint (sublevelLeft X f b (↑y : F)) (sublevelLeft X f b (↑y' : F))

Tactic:
rw [Set.disjoint_iff]

Premises used: Set.disjoint_iff
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
a : E
b : β
y y' : (↑Y : Type u_2)
ha : ∀ x ∈ X, max (f a (↑y : F)) (f a (↑y' : F)) ≤ max (f x (↑y : F)) (f x (↑y' : F))
hb : b < max (f a (↑y : F)) (f a (↑y' : F))
x : E
hx : x ∈ X
hx1 : Subtype.mk (p := fun (x : E) ↦ x ∈ X) x hx ∈ sublevelLeft X f b (↑y : F)
hx2 : Subtype.mk (p := fun (x : E) ↦ x ∈ X) x hx ∈ sublevelLeft X f b (↑y' : F)
apply : max (f a (↑y : F)) (f a (↑y' : F)) ≤ b
⊢ Membership.mem (γ := Set (↑X : Type u_1)) ∅ (Subtype.mk (p := fun (x : E) ↦ x ∈ X) x hx)

Tactic:
apply hb.not_ge

Premises used: LT.lt.not_ge
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
a : E
b : β
y y' : (↑Y : Type u_2)
ha : ∀ x ∈ X, max (f a (↑y : F)) (f a (↑y' : F)) ≤ max (f x (↑y : F)) (f x (↑y' : F))
hb : b < max (f a (↑y : F)) (f a (↑y' : F))
x : E
hx : x ∈ X
hx1 : Subtype.mk (p := fun (x : E) ↦ x ∈ X) x hx ∈ sublevelLeft X f b (↑y : F)
hx2 : Subtype.mk (p := fun (x : E) ↦ x ∈ X) x hx ∈ sublevelLeft X f b (↑y' : F)
grw : max (f x (↑y : F)) (f x (↑y' : F)) ≤ b
⊢ max (f a (↑y : F)) (f a (↑y' : F)) ≤ b

Tactic:
grw [ha x hx]
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
a : E
b : β
y y' : (↑Y : Type u_2)
ha : ∀ x ∈ X, max (f a (↑y : F)) (f a (↑y' : F)) ≤ max (f x (↑y : F)) (f x (↑y' : F))
hb : b < max (f a (↑y : F)) (f a (↑y' : F))
x : E
hx : x ∈ X
hx1 : Subtype.mk (p := fun (x : E) ↦ x ∈ X) x hx ∈ sublevelLeft X f b (↑y : F)
hx2 : Subtype.mk (p := fun (x : E) ↦ x ∈ X) x hx ∈ sublevelLeft X f b (↑y' : F)
⊢ max (f x (↑y : F)) (f x (↑y' : F)) ≤ b

Tactic:
simpa using ⟨hx1, hx2⟩
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
y : (↑Y : Type u_2)
b : β
h : ∀ y ∈ Y, ∃ x ∈ X, f x y ≤ b
rcases : ∀ (y : F) (hy : y ∈ Y), (sublevelLeft X f b (↑(Subtype.mk (p := fun (x : F) ↦ x ∈ Y) y hy) : F)).Nonempty
⊢ (sublevelLeft X f b (↑y : F)).Nonempty

Tactic:
rcases y with ⟨y, hy⟩
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
b : β
h : ∀ y ∈ Y, ∃ x ∈ X, f x y ≤ b
y : F
hy : y ∈ Y
obtain :
  ∀ (x : E) (hx : x ∈ X) (hx_le : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X x),
    (sublevelLeft X f b (↑(Subtype.mk (p := fun (x : F) ↦ x ∈ Y) y hy) : F)).Nonempty
⊢ (sublevelLeft X f b (↑(Subtype.mk (p := fun (x : F) ↦ x ∈ Y) y hy) : F)).Nonempty

Tactic:
obtain ⟨x, hx, hx_le⟩ := LowerSemicontinuousOn.exists_isMinOn ne_X kX (hfy y hy)

Premises used: LowerSemicontinuousOn.exists_isMinOn
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
b : β
h : ∀ y ∈ Y, ∃ x ∈ X, f x y ≤ b
y : F
hy : y ∈ Y
x : E
hx : x ∈ X
hx_le : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X x
obtain :
  ∀ (x' : E) (hx' : x' ∈ X) (hx'b : f x' y ≤ b),
    (sublevelLeft X f b (↑(Subtype.mk (p := fun (x : F) ↦ x ∈ Y) y hy) : F)).Nonempty
⊢ (sublevelLeft X f b (↑(Subtype.mk (p := fun (x : F) ↦ x ∈ Y) y hy) : F)).Nonempty

Tactic:
obtain ⟨x', hx', hx'b⟩ := h y hy
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
b : β
h : ∀ y ∈ Y, ∃ x ∈ X, f x y ≤ b
y : F
hy : y ∈ Y
x : E
hx : x ∈ X
hx_le : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X x
x' : E
hx' : x' ∈ X
hx'b : f x' y ≤ b
⊢ (sublevelLeft X f b (↑(Subtype.mk (p := fun (x : F) ↦ x ∈ Y) y hy) : F)).Nonempty

Tactic:
⟨⟨x, hx⟩, le_trans (hx_le hx') hx'b⟩

Premises used: Subtype.mk, Set.Nonempty, Exists.intro, le_trans
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
b : β
h : ∀ y ∈ Y, ∃ x ∈ X, f x y ≤ b
y : F
hy : y ∈ Y
x : E
hx : x ∈ X
hx_le : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X x
x' : E
hx' : x' ∈ X
hx'b : f x' y ≤ b
⊢ (sublevelLeft X f b (↑(Subtype.mk (p := fun (x : F) ↦ x ∈ Y) y hy) : F)).Nonempty

Tactic:
exact ⟨⟨x, hx⟩, le_trans (hx_le hx') hx'b⟩
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
b : β
y : (↑Y : Type u_2)
⊢ LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x (↑y : F)) X

Tactic:
specialize hfy y.val y.prop

Premises used: Subtype.prop, Subtype.val
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
b : β
y : (↑Y : Type u_2)
hfy : LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x (↑y : F)) X
⊢ ∀ (y_1 : β),
    IsClosed.{u_1} (X := (↑X : Type u_1)) ((X.restrict (π := fun (a : E) ↦ β) fun (x : E) ↦ f x (↑y : F)) ⁻¹' Iic y_1)

Tactic:
rw [← lowerSemicontinuous_restrict_iff, lowerSemicontinuous_iff_isClosed_preimage] at hfy

Premises used: lowerSemicontinuous_iff_isClosed_preimage, lowerSemicontinuous_restrict_iff
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
b : β
y : (↑Y : Type u_2)
hfy :
  ∀ (y_1 : β),
    IsClosed.{u_1} (X := (↑X : Type u_1)) ((X.restrict (π := fun (a : E) ↦ β) fun (x : E) ↦ f x (↑y : F)) ⁻¹' Iic y_1)
⊢ IsClosed (sublevelLeft X f b (↑y : F))

Tactic:
hfy b

Premises used: _private.0.Sion.sublevelLeft, Set.restrict
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
b : β
y : (↑Y : Type u_2)
hfy :
  ∀ (y_1 : β),
    IsClosed.{u_1} (X := (↑X : Type u_1)) ((X.restrict (π := fun (a : E) ↦ β) fun (x : E) ↦ f x (↑y : F)) ⁻¹' Iic y_1)
⊢ IsClosed (sublevelLeft X f b (↑y : F))

Tactic:
exact hfy b
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
b : β
y : (↑Y : Type u_2)
⊢ IsPreconnected (sublevelLeft X f b (↑y : F))

Tactic:
(hfy' y.val y.prop).isPreconnected_preimage_subtype

Premises used: _private.0.Sion.sublevelLeft, Set.Mem, QuasiconvexOn.isPreconnected_preimage_subtype, setOf, Set.preimage, Subtype.prop, Set.Iic, Subtype.val
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : AddCommGroup F
inst_2 : Module ℝ F
hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) Y fun (y : F) ↦ f x y
b : β
y y' : (↑Y : Type u_2)
z : (↑(segment ℝ (↑y : F) (↑y' : F)) : Type u_2)
x : (↑X : Type u_1)
hx : x ∈ sublevelLeft X f b (↑z : F)
simp : min (f (↑x : E) (↑y : F)) (f (↑x : E) (↑y' : F)) ≤ b
⊢ x ∈ sublevelLeft X f b (↑y : F) ∪ sublevelLeft X f b (↑y' : F)

Tactic:
simp only [Set.mem_union, mem_sublevelLeft_iff, ← inf_le_iff]

Premises used: Set.mem_union, inf_le_iff, _private.0.Sion.mem_sublevelLeft_iff
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : AddCommGroup F
inst_2 : Module ℝ F
hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) Y fun (y : F) ↦ f x y
b : β
y y' : (↑Y : Type u_2)
z : (↑(segment ℝ (↑y : F) (↑y' : F)) : Type u_2)
x : (↑X : Type u_1)
hx : x ∈ sublevelLeft X f b (↑z : F)
⊢ Convex.{0, u_2} ℝ (E := F)
    {x_1 : F | x_1 ∈ Y ∧ min (f (↑x : E) (↑y : F)) (f (↑x : E) (↑y' : F)) ≤ (fun (y : F) ↦ f (↑x : E) y) x_1}

Tactic:
specialize hfx' x x.2 (f x y ⊓ f x y')

Premises used: Subtype.val, Min.min, Subtype.property