awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
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
v : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
si : Set X :=
  s ∩ (⋃ (j : ι), ⋃ (_ : j ≠ i), v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j)ᶜ
hsi :
  si =
    s ∩ ⋂ (i_1 : ι), ⋂ (_ : ¬i_1 = i), (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i
vi : Set X
hvi :
  IsOpen vi ∧
    si ⊆ vi ∧
      closure vi ⊆ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i ∧ IsCompact (closure vi)
refine_1 :
  ∀ (i_1 : ι),
    IsOpen
      (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) i vi
        i_1)
refine_2 :
  s ⊆
    ⋃ (i_1 : ι),
      update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) i vi
        i_1
⊢ ∃ (v' : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)),
    v < v' ∧ IsCompact (closure (v'.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i))
have refine_3 : ∀ {i_1 : ι},
  i_1 ∈ insert i (v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) →
    closure
        (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) i
          vi i_1) ⊆
      u i_1
Tactic: classical
  refine ⟨⟨update v i vi, insert i v.carrier, ?_, ?_, ?_, ?_, ?_⟩, ⟨?_, ?_⟩, ?_⟩
  · intro j
    rcases eq_or_ne j i with (rfl | hne) <;> simp [*, v.isOpen]
  · refine fun x hx => mem_iUnion.2 ?_
    by_cases! h : ∃ j ≠ i, x ∈ v j
    · rcases h with ⟨j, hji, hj⟩
      use j
      rwa [update_of_ne hji]
    · use i
      rw [update_self]
      apply hvi.2.1
      rw [hsi]
      exact ⟨hx, mem_iInter₂_of_mem h⟩
  · rintro j (rfl | hj)
    · rw [update_self]
      exact subset_trans hvi.2.2.1 <| PartialRefinement.subset v j
    · rw [update_of_ne (ne_of_mem_of_not_mem hj hi)]
      exact v.closure_subset hj
  · intro j hj
    rw [mem_insert_iff] at hj
    by_cases h : j = i
    · rw [← h]
      simp only [update_self]
      exact hvi.2.2.2
    · apply hj.elim
      · intro hji
        exact False.elim (h hji)
      · intro hjmemv
        rw [update_of_ne h]
        exact v.pred_of_mem hjmemv
  · intro j hj
    rw [mem_insert_iff, not_or] at hj
    rw [update_of_ne hj.1, v.apply_eq hj.2]
  · refine ⟨subset_insert _ _, fun j hj => ?_⟩
    exact (update_of_ne (ne_of_mem_of_not_mem hj hi) _ _).symm
  · exact fun hle => hi (hle.1 <| mem_insert _ _)
  · simp only [update_self]
    exact hvi.2.2.2
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (hypothesis)
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),
    s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ (∀ (i : ι), closure (v i) ⊆ u i) ∧ ∀ (i : ι), IsCompact (closure (v i))
have this : Nonempty (PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w))
Tactic: haveI : Nonempty (PartialRefinement u s (fun w => IsCompact (closure w))) :=
    ⟨⟨u, ∅, uo, us, False.elim, False.elim, fun _ => rfl⟩⟩
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (hypothesis)
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 : Nonempty (PartialRefinement u s 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))
have 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
Tactic: have : ∀ c : Set (PartialRefinement u s (fun w => IsCompact (closure w))),
      IsChain (· ≤ ·) c → c.Nonempty → ∃ ub, ∀ v ∈ c, v ≤ ub :=
    fun c hc ne => ⟨.chainSup c hc ne uf us, fun v hv => PartialRefinement.le_chainSup _ _ _ _ hv⟩
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
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 : ι → Set X),
    s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ (∀ (i : ι), closure (v i) ⊆ u i) ∧ ∀ (i : ι), IsCompact (closure (v i))
have 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))
Tactic: rcases zorn_le_nonempty this with ⟨v, hv⟩
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
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
⊢ ∃ (v : ι → Set X),
    s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ (∀ (i : ι), closure (v i) ⊆ u i) ∧ ∀ (i : ι), IsCompact (closure (v i))
have 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))
Tactic: suffices ∀ i, i ∈ v.carrier from
    ⟨v, v.subset_iUnion, fun i => v.isOpen _, fun i => v.closure_subset (this i), ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
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))
⊢ ∃ (v : ι → Set X),
    s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ (∀ (i : ι), closure (v i) ⊆ u i) ∧ ∀ (i : ι), IsCompact (closure (v i))
have refine_1 : ∀ (i : ι), i ∈ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
Tactic: suffices ∀ i, i ∈ v.carrier from
    ⟨v, v.subset_iUnion, fun i => v.isOpen _, fun i => v.closure_subset (this i), ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
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 : ι
⊢ i ∈ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
have refine_1 : ∀ (hi : i ∉ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))), False
Tactic: by_contra! hi
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
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))
⊢ False
have 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
Tactic: rcases exists_gt_t2space v hs i hi with ⟨v', hlt, _⟩
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
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), s ⊆ iUnion v ∧ (∀ (i : ι), IsClosed (v i)) ∧ (∀ (i : ι), v i ⊆ u i) ∧ ∀ (i : ι), IsCompact (v i)
have 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)
Tactic: let ⟨v, hsv, _, hv⟩ := exists_subset_iUnion_closure_subset_t2space hs uo uf us
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
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))
⊢ ∃ (v : ι → Set X), s ⊆ iUnion v ∧ (∀ (i : ι), IsClosed (v i)) ∧ (∀ (i : ι), v i ⊆ u i) ∧ ∀ (i : ι), IsCompact (v i)
have 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)
Tactic: use fun i => closure (v i)
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
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)
have h : s ⊆ ⋃ (i : ι), closure (v i)
Tactic: refine ⟨?_, ?_, hv⟩
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
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)
⊢ 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)
have h₁ : ∀ (i : ι), IsClosed.{u_2} (X := X) ((fun (i : ι) ↦ closure (v i)) i)
Tactic: refine ⟨?_, ?_, hv⟩
-- Lean 4 proof step from Mathlib.Topology.Sion (goal)
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))
⊢ Disjoint (sublevelLeft X f b (↑y : F)) (sublevelLeft X f b (↑y' : F))
have rw : sublevelLeft X f b (↑y : F) ∩ sublevelLeft X f b (↑y' : F) ⊆ ∅
Tactic: rw [Set.disjoint_iff]
-- Lean 4 proof step from Mathlib.Topology.Sion (goal)
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)
⊢ Membership.mem (γ := Set (↑X : Type u_1)) ∅ (Subtype.mk (p := fun (x : E) ↦ x ∈ X) x hx)
have apply : max (f a (↑y : F)) (f a (↑y' : F)) ≤ b
Tactic: apply hb.not_ge
-- Lean 4 proof step from Mathlib.Topology.Sion (goal)
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 a (↑y : F)) (f a (↑y' : F)) ≤ b
have grw : max (f x (↑y : F)) (f x (↑y' : F)) ≤ b
Tactic: grw [ha x hx]
-- Lean 4 proof step from Mathlib.Topology.Sion (goal)
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
⊢ (sublevelLeft X f b (↑y : F)).Nonempty
have rcases : ∀ (y : F) (hy : y ∈ Y), (sublevelLeft X f b (↑(Subtype.mk (p := fun (x : F) ↦ x ∈ Y) y hy) : F)).Nonempty
Tactic: rcases y with ⟨y, hy⟩
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Topology.Sion (goal)
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
⊢ (sublevelLeft X f b (↑(Subtype.mk (p := fun (x : F) ↦ x ∈ Y) y hy) : F)).Nonempty
have 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
Tactic: obtain ⟨x, hx, hx_le⟩ := LowerSemicontinuousOn.exists_isMinOn ne_X kX (hfy y hy)
-- Lean 4 proof step from Mathlib.Topology.Sion (goal)
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
⊢ (sublevelLeft X f b (↑(Subtype.mk (p := fun (x : F) ↦ x ∈ Y) y hy) : F)).Nonempty
have 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
Tactic: obtain ⟨x', hx', hx'b⟩ := h y hy
-- Lean 4 proof step from Mathlib.Topology.Sion (hypothesis)
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)
⊢ IsClosed (sublevelLeft X f b (↑y : F))
have hfy₁ : LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x (↑y : F)) X
Tactic: specialize hfy y.val y.prop
Cleared hypotheses: hfy
-- Lean 4 proof step from Mathlib.Topology.Sion (hypothesis)
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
⊢ IsClosed (sublevelLeft X f b (↑y : F))
have 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)
Tactic: rw [← lowerSemicontinuous_restrict_iff, lowerSemicontinuous_iff_isClosed_preimage] at hfy
Cleared hypotheses: hfy
-- Lean 4 proof step from Mathlib.Topology.Sion (goal)
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)
⊢ x ∈ sublevelLeft X f b (↑y : F) ∪ sublevelLeft X f b (↑y' : F)
have simp : min (f (↑x : E) (↑y : F)) (f (↑x : E) (↑y' : F)) ≤ b
Tactic: simp only [Set.mem_union, mem_sublevelLeft_iff, ← inf_le_iff]
-- Lean 4 proof step from Mathlib.Topology.Sion (hypothesis)
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)
⊢ min (f (↑x : E) (↑y : F)) (f (↑x : E) (↑y' : F)) ≤ b
have hfx'₁ : 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')
Cleared hypotheses: hfx'
-- Lean 4 proof step from Mathlib.Topology.Sion (hypothesis)
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
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)
hfx' :
  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}
⊢ min (f (↑x : E) (↑y : F)) (f (↑x : E) (↑y' : F)) ≤ b
have hfx'₁ : ∀ ⦃x_1 : F⦄,
  Membership.mem (γ := Set F)
      {x_2 : F | x_2 ∈ Y ∧ min (f (↑x : E) (↑y : F)) (f (↑x : E) (↑y' : F)) ≤ (fun (y : F) ↦ f (↑x : E) y) x_2} x_1 →
    ∀ ⦃y_1 : F⦄,
      Membership.mem (γ := Set F)
          {x_2 : F | x_2 ∈ Y ∧ min (f (↑x : E) (↑y : F)) (f (↑x : E) (↑y' : F)) ≤ (fun (y : F) ↦ f (↑x : E) y) x_2}
          y_1 →
        segment ℝ x_1 y_1 ⊆
          {x_2 : F | x_2 ∈ Y ∧ min (f (↑x : E) (↑y : F)) (f (↑x : E) (↑y' : F)) ≤ (fun (y : F) ↦ f (↑x : E) y) x_2}
Tactic: rw [convex_iff_segment_subset] at hfx'
Cleared hypotheses: hfx'
-- Lean 4 proof step from Mathlib.Topology.Sion (hypothesis)
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
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)
hfx' :
  ∀ ⦃x_1 : F⦄,
    Membership.mem (γ := Set F)
        {x_2 : F | x_2 ∈ Y ∧ min (f (↑x : E) (↑y : F)) (f (↑x : E) (↑y' : F)) ≤ (fun (y : F) ↦ f (↑x : E) y) x_2} x_1 →
      ∀ ⦃y_1 : F⦄,
        Membership.mem (γ := Set F)
            {x_2 : F | x_2 ∈ Y ∧ min (f (↑x : E) (↑y : F)) (f (↑x : E) (↑y' : F)) ≤ (fun (y : F) ↦ f (↑x : E) y) x_2}
            y_1 →
          segment ℝ x_1 y_1 ⊆
            {x_2 : F | x_2 ∈ Y ∧ min (f (↑x : E) (↑y : F)) (f (↑x : E) (↑y' : F)) ≤ (fun (y : F) ↦ f (↑x : E) y) x_2}
⊢ min (f (↑x : E) (↑y : F)) (f (↑x : E) (↑y' : F)) ≤ b
have hfx'₁ : Membership.mem (γ := Set 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} (↑z : F)
Tactic: specialize hfx' ⟨y.prop, inf_le_left⟩ ⟨y'.prop, inf_le_right⟩ z.prop
Cleared hypotheses: hfx'
-- Lean 4 proof step from Mathlib.Topology.Sion (goal)
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 : IsTopologicalAddGroup E
inst_4 : Module ℝ E
inst_5 : ContinuousSMul ℝ E
inst_6 : AddCommGroup F
inst_7 : Module ℝ F
hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) Y fun (y : F) ↦ f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
cY : Convex ℝ Y
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))
z : (↑(segment ℝ (↑y : F) (↑y' : F)) : Type u_2)
⊢ sublevelLeft X f b (↑z : F) ⊆ sublevelLeft X f b (↑y : F) ∨ sublevelLeft X f b (↑z : F) ⊆ sublevelLeft X f b (↑y' : F)
have apply : sublevelLeft X f b (↑(Subtype.mk (p := fun (x : F) ↦ x ∈ Y) (↑z : F) sorry) : F) ∩
    (sublevelLeft X f b (↑y : F) ∩ sublevelLeft X f b (↑y' : F)) =
  ∅
Tactic: apply isPreconnected_iff_subset_of_disjoint_closed.mp
    (isPreconnected_sublevelLeft hfy' b ⟨z, cY.segment_subset y.prop y'.prop z.prop⟩)
    _ _ (isClosed_sublevelLeft hfy b y) (isClosed_sublevelLeft hfy b y')
    (sublevelLeft_subset_union hfx' b y y' z)