awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
Goal:
α_1 : Type u_1
inst : TopologicalSpace α_1
α : Type u_1
inst_1 : TopologicalSpace α
inst_2 : QuasiSeparatedSpace α
s_1 : Set (Set α)
a : Set α
s : Set (Set α)
ha : a ∉ s
hs : s.Finite
ih :
  ∀ (ho : ∀ t ∈ s, IsOpen[inst_1] t ∨ IsClosed[inst_1] t) (hc : ∀ t ∈ s, IsCompact t) (h : ∀ t ∈ s, IsOpen[inst_1] t)
    (hne : s.Nonempty), IsCompact (⋂₀ s)
ho : ∀ t ∈ insert a s, IsOpen[inst_1] t ∨ IsClosed[inst_1] t
hc : ∀ t ∈ insert a s, IsCompact t
h : ∀ t ∈ insert a s, IsOpen[inst_1] t
⊢ ∀ (hne : (insert a s).Nonempty), IsCompact (⋂₀ insert a s)
have insert : ∀ (ha : a ∉ ∅) (hs : Set.Finite.{u_1} (α := Set α) ∅)
  (ih :
    ∀ (ho : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) ∅ t → IsOpen[inst_1] t ∨ IsClosed[inst_1] t)
      (hc : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) ∅ t → IsCompact t)
      (h : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) ∅ t → IsOpen[inst_1] t)
      (hne : Set.Nonempty.{u_1} (α := Set α) ∅), IsCompact.{u_1} (X := α) (⋂₀ ∅))
  (ho : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) (insert a ∅) t → IsOpen[inst_1] t ∨ IsClosed[inst_1] t)
  (hc : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) (insert a ∅) t → IsCompact t)
  (h : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) (insert a ∅) t → IsOpen[inst_1] t)
  (hne : Set.Nonempty (α := Set α) (insert a ∅)), IsCompact (X := α) (⋂₀ insert a ∅)
Tactic: obtain (rfl | hne) := s.eq_empty_or_nonempty
Cleared hypotheses: s, ha, hs, ih, ho, hc, h
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
Goal:
α_1 : Type u_1
inst : TopologicalSpace α_1
α : Type u_1
inst_1 : TopologicalSpace α
inst_2 : QuasiSeparatedSpace α
s_1 : Set (Set α)
a : Set α
s : Set (Set α)
ha : a ∉ s
hs : s.Finite
ih :
  ∀ (ho : ∀ t ∈ s, IsOpen[inst_1] t ∨ IsClosed[inst_1] t) (hc : ∀ t ∈ s, IsCompact t) (h : ∀ t ∈ s, IsOpen[inst_1] t)
    (hne : s.Nonempty), IsCompact (⋂₀ s)
ho : ∀ t ∈ Insert.insert a s, IsOpen[inst_1] t ∨ IsClosed[inst_1] t
hc : ∀ t ∈ Insert.insert a s, IsCompact t
h : ∀ t ∈ Insert.insert a s, IsOpen[inst_1] t
insert :
  ∀ (ha : a ∉ ∅) (hs : Set.Finite.{u_1} (α := Set α) ∅)
    (ih :
      ∀ (ho : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) ∅ t → IsOpen[inst_1] t ∨ IsClosed[inst_1] t)
        (hc : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) ∅ t → IsCompact t)
        (h : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) ∅ t → IsOpen[inst_1] t)
        (hne : Set.Nonempty.{u_1} (α := Set α) ∅), IsCompact.{u_1} (X := α) (⋂₀ ∅))
    (ho :
      ∀ (t : Set α), Membership.mem (γ := Set (Set α)) (Insert.insert a ∅) t → IsOpen[inst_1] t ∨ IsClosed[inst_1] t)
    (hc : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) (Insert.insert a ∅) t → IsCompact t)
    (h : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) (Insert.insert a ∅) t → IsOpen[inst_1] t)
    (hne : Set.Nonempty (α := Set α) (Insert.insert a ∅)), IsCompact (X := α) (⋂₀ Insert.insert a ∅)
⊢ ∀ (hne : (Insert.insert a s).Nonempty), IsCompact (⋂₀ Insert.insert a s)
have insert₁ : ∀ (hne : s.Nonempty) (hne : (Insert.insert a s).Nonempty), IsCompact (⋂₀ Insert.insert a s)
Tactic: obtain (rfl | hne) := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSeparatedSpace α
inst_2 : CompactSpace α
s : Set (Set α)
hf : s.Finite
ho : ∀ t ∈ s, IsOpen[inst] t ∨ IsClosed[inst] t
hc : ∀ t ∈ s, IsCompact t
⊢ IsCompact (⋂₀ s)
have inl : ∀ (hf : Set.Finite.{u_1} (α := Set α) ∅)
  (ho : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) ∅ t → IsOpen[inst] t ∨ IsClosed[inst] t)
  (hc : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) ∅ t → IsCompact t), IsCompact.{u_1} (X := α) (⋂₀ ∅)
Tactic: obtain (rfl | hne) := s.eq_empty_or_nonempty
Cleared hypotheses: s, hf, ho, hc
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSeparatedSpace α
inst_2 : CompactSpace α
s : Set (Set α)
hf : s.Finite
ho : ∀ t ∈ s, IsOpen[inst] t ∨ IsClosed[inst] t
hc : ∀ t ∈ s, IsCompact t
inl :
  ∀ (hf : Set.Finite.{u_1} (α := Set α) ∅)
    (ho : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) ∅ t → IsOpen[inst] t ∨ IsClosed[inst] t)
    (hc : ∀ (t : Set α), Membership.mem (γ := Set (Set α)) ∅ t → IsCompact t), IsCompact.{u_1} (X := α) (⋂₀ ∅)
⊢ IsCompact (⋂₀ s)
have inr : ∀ (hne : s.Nonempty), IsCompact (⋂₀ s)
Tactic: obtain (rfl | hne) := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ ∃ a ∈ s, IsMinOn f s a
have simp : ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x
Tactic: simp only [isMinOn_iff]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (hypothesis)
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
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x
have x : Nonempty α
Tactic: have _ : Nonempty α := Exists.nonempty ne_s
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (hypothesis)
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 α
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x
have x : Nonempty.{u_1 + 1} (↑s : Type u_1)
Tactic: have _ : Nonempty s := Nonempty.to_subtype ne_s
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
have apply : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) fun (a : (↑s : Type u_1)) ↦ φ (f (↑a : α))
Tactic: apply iInf_neBot_of_directed _ _
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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 : α))
apply : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) fun (a : (↑s : Type u_1)) ↦ φ (f (↑a : α))
⊢ ℱ.NeBot
have apply₁ : ∀ (i : (↑s : Type u_1)), (φ (f (↑i : α))).NeBot
Tactic: apply iInf_neBot_of_directed _ _
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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 : α))
⊢ Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) fun (a : (↑s : Type u_1)) ↦ φ (f (↑a : α))
have change : Directed (α := Filter α) GE.ge fun (x : (↑s : Type u_1)) ↦ (φ ∘ fun (a : (↑s : Type u_1)) ↦ f (↑a : α)) x
Tactic: change Directed GE.ge (fun x ↦ (φ ∘ (fun (a : s) ↦ f ↑a)) x)
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (hypothesis)
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)
⊢ (φ (f (↑x : α))).NeBot
have this : pure (↑x : α) ≤ φ (f (↑x : α))
Tactic: have : (pure x : Filter α) ≤ φ (f x) := le_principal_iff.mpr ⟨x.2, le_refl (f x)⟩
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (hypothesis)
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 : α))
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x
have this : ℱ.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
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (hypothesis)
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
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x
have hℱs : ℱ ≤ 𝓟 s
Tactic: have hℱs : ℱ ≤ 𝓟 s :=
    iInf_le_of_le (Classical.choice inferInstance) (principal_mono.mpr <| inter_subset_left)
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (hypothesis)
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
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x
have hℱ : ∀ (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)
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x
have obtain : ∀ (a : α) (ha : a ∈ s) (h : ClusterPt a ℱ), ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x
Tactic: obtain ⟨a, ha, h⟩ := hs hℱs
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
have refine : ∀ (x : α) (hx : x ∈ s) (hxa : f x < f a), False
Tactic: refine ⟨a, ha, fun x hx ↦ le_of_not_gt fun hxa ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ False
have rwa : ∀ (this : False), False
Tactic: rwa [eventually_const] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ False
have suffices : ∀ᶠ (x : α) in 𝓝 a ⊓ ℱ, False
Tactic: suffices ∀ᶠ _ in 𝓝 a ⊓ ℱ, False by rwa [eventually_const] at this
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ ∀ᶠ (x : α) in 𝓝 a ⊓ ℱ, False
have 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
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₂
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ ∀ᶠ (x : α) in 𝓝 a ⊓ ℱ, False
have h₂ : ∀ (a : α), f a > f x → f a ≤ f x → 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₂
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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 (f '' s)
have inl : BddBelow.{u_2} (α := β) ∅
Tactic: simp only [h, Set.image_empty]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ BddBelow (f '' s)
have inr : ∀ a ∈ s, ∀ (has : IsMinOn f s a), BddBelow (f '' s)
Tactic: obtain ⟨a, _, has⟩ := LowerSemicontinuousOn.exists_isMinOn h hs hf
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (hypothesis)
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
⊢ BddBelow (f '' s)
have x : 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
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z
have pos : ∀ (h : x ∈ s), ∀ᶠ (x' : α) in 𝓝 x, (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z
Tactic: by_cases h : x ∈ s
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z
have neg : ∀ (h : x ∉ s), ∀ᶠ (x' : α) in 𝓝 x, (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z
Tactic: by_cases h : x ∈ s
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (hypothesis)
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
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z
have hz₁ : z < y
Tactic: simp [h] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (hypothesis)
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
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z
have hz₁ : z < 0
Tactic: simp [h] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z
have h₁ : ∀ a ∈ s, s.indicator (fun (_x : α) ↦ y) a > z
Tactic: filter_upwards [hs.mem_nhds h]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
have neg : ∀ (x' : α), (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z
Tactic: refine Filter.Eventually.of_forall fun x' => ?_
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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' : α
⊢ (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z
have pos : ∀ (h' : x' ∈ s), (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z
Tactic: by_cases h' : x' ∈ s
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z
have neg : ∀ (h' : x' ∉ s), (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z
Tactic: by_cases h' : x' ∈ s
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z
have pos : ∀ (h : x ∈ s), ∀ᶠ (x' : α) in 𝓝 x, (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z
Tactic: by_cases h : x ∈ s
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z
have neg : ∀ (h : x ∉ s), ∀ᶠ (x' : α) in 𝓝 x, (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z
Tactic: by_cases h : x ∈ s
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (hypothesis)
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
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z
have hz₁ : z < y
Tactic: simp [h] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (hypothesis)
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
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z
have hz₁ : z < 0
Tactic: simp [h] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
have pos : ∀ (x' : α), (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z
Tactic: refine Filter.Eventually.of_forall fun x' => ?_
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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' : α
⊢ (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z
have pos : ∀ (h' : x' ∈ s), (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z
Tactic: by_cases h' : x' ∈ s
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z
have neg : ∀ (h' : x' ∉ s), (fun (x1 : α) (x2 : β) ↦ s.indicator (fun (_x : α) ↦ y) x1 > x2) x' z
Tactic: by_cases h' : x' ∈ s