awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 < 0
⊢ ∀ᶠ (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.isOpen_compl.mem_nhds h]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : β) ↦ (fun (x : α) ↦ f (M x) x) x1 > x2) x' b
have 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
Tactic: apply Filter.Eventually.mp <| hfy (M x) (M_mem x hx) x hx b hb
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ ∀ᶠ (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
have 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
Tactic: apply eventually_nhdsWithin_of_forall
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
γ : Type u_4
inst_1 : LinearOrder γ
f : α → γ
⊢ LowerSemicontinuous f ↔ ∀ (y : γ), IsClosed[inst] (f ⁻¹' Iic y)
have rw : (∀ (y : γ), IsOpen[inst] (f ⁻¹' Ioi y)) ↔ ∀ (y : γ), IsClosed[inst] (f ⁻¹' Iic y)
Tactic: rw [lowerSemicontinuous_iff_isOpen_preimage]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst_1 : CompleteLinearOrder γ
f : α → γ
⊢ LowerSemicontinuousWithinAt f s x ↔ f x ≤ liminf f (𝓝[s] x)
have mp : LowerSemicontinuousWithinAt f s x → f x ≤ liminf f (𝓝[s] x)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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)
⊢ LowerSemicontinuousWithinAt f s x ↔ f x ≤ liminf f (𝓝[s] x)
have mpr : f x ≤ liminf f (𝓝[s] x) → LowerSemicontinuousWithinAt f s x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ f x ≤ liminf f (𝓝[s] x)
have mp : ∀ (hf : liminf f (𝓝[s] x) < f x), False
Tactic: by_contra! hf
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ False
have mp : ∀ (z : γ) (ltz : z > liminf f (𝓝[s] x)) (y : γ) (ylt : y < f x) (h₁ : ∀ x < z, ∀ y_1 > y, x < y_1), False
Tactic: obtain ⟨z, ltz, y, ylt, h₁⟩ := hf.exists_disjoint_Iio_Ioi
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
γ : Type u_4
inst_1 : CompleteLinearOrder γ
f : α → γ
⊢ LowerSemicontinuousAt f x ↔ f x ≤ liminf f (𝓝 x)
have rw : LowerSemicontinuousWithinAt f univ x ↔ f x ≤ liminf f (𝓝 x)
Tactic: rw [← lowerSemicontinuousWithinAt_univ_iff, lowerSemicontinuousWithinAt_iff_le_liminf,
    ← nhdsWithin_univ]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
γ : Type u_4
inst_1 : CompleteLinearOrder γ
f : α → γ
rw : LowerSemicontinuousWithinAt f univ x ↔ f x ≤ liminf f (𝓝 x)
⊢ LowerSemicontinuousAt f x ↔ f x ≤ liminf f (𝓝 x)
have rw₁ : f x ≤ liminf f (𝓝[univ] x) ↔ f x ≤ liminf f (𝓝 x)
Tactic: rw [← lowerSemicontinuousWithinAt_univ_iff, lowerSemicontinuousWithinAt_iff_le_liminf,
    ← nhdsWithin_univ]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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)
⊢ LowerSemicontinuousAt f x ↔ f x ≤ liminf f (𝓝 x)
have rw₂ : f x ≤ liminf f (𝓝[univ] x) ↔ f x ≤ liminf f (𝓝[univ] x)
Tactic: rw [← lowerSemicontinuousWithinAt_univ_iff, lowerSemicontinuousWithinAt_iff_le_liminf,
    ← nhdsWithin_univ]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
γ : Type u_4
inst_1 : LinearOrder γ
f : α → γ
hfs : LowerSemicontinuousOn f s
ks : IsCompact s
c : γ
⊢ IsCompact (s ∩ f ⁻¹' Iic c)
have rw : ∀ (hfs : ∀ (b : γ), ∃ (v : Set α), IsClosed[inst] v ∧ s ∩ f ⁻¹' Iic b = s ∩ v) (ks : IsCompact s) (c : γ),
  IsCompact (s ∩ f ⁻¹' Iic c)
Tactic: rw [lowerSemicontinuousOn_iff_preimage_Iic] at hfs
Cleared hypotheses: hfs, ks, c
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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 : γ
⊢ IsCompact (s ∩ f ⁻¹' Iic c)
have obtain : ∀ (v : Set α) (hv : IsClosed[inst] v) (hv' : s ∩ f ⁻¹' Iic c = s ∩ v), IsCompact (s ∩ f ⁻¹' Iic c)
Tactic: obtain ⟨v, hv, hv'⟩ := hfs c
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
have refine_1 : ∀ (H : 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⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ s ∩ ⋂ i ∈ I, f i ⁻¹' Iic c = ∅ ↔ ∃ (u : Finset (↑I : Type u_5)), ∀ x ∈ s, ∃ i ∈ u, c < f (↑i : ι) x
have 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 = ∅
Tactic: refine ⟨fun H ↦ ?_, fun ⟨u, hu⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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 = ∅
⊢ ∃ (u : Finset (↑I : Type u_5)), ∀ x ∈ s, ∃ i ∈ u, c < f (↑i : ι) x
have refine_1 : ∀ i ∈ I, IsClosed[instTopologicalSpaceSubtype] (s ↓∩ (fun (i : ι) ↦ f i ⁻¹' Iic c) i)
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
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ s ∩ ⋂ i ∈ I, f i ⁻¹' Iic c = ∅
have refine_2 : ∀ (x : α), x ∉ s ∩ ⋂ i ∈ I, f i ⁻¹' Iic c
Tactic: rw [Set.eq_empty_iff_forall_notMem]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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 : α), x ∉ s ∩ ⋂ i ∈ I, f i ⁻¹' Iic c
have refine_2 : ∀ x ∈ s, ∃ x_1 ∈ I, c < f x_1 x
Tactic: simp only [mem_inter_iff, mem_iInter, mem_preimage, mem_Iic, not_and, not_forall,
      exists_prop, not_le]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ LowerSemicontinuousOn f s ↔ IsClosed[instTopologicalSpaceProd] {p : α × γ | p.1 ∈ s ∧ f p.1 ≤ p.2}
have 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
Tactic: simp_rw [lowerSemicontinuousOn_iff, lowerSemicontinuousWithinAt_iff,
    eventually_nhdsWithin_iff, ← isOpen_compl_iff, compl_setOf, isOpen_iff_eventually, mem_setOf,
    not_and, not_le]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ (∀ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ (∀ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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 : α × γ), (x.1 ∈ s → x.2 < f x.1) → ∀ᶠ (a : α × γ) in 𝓝 x, a.1 ∈ s → a.2 < f a.1
have 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
Tactic: ⟨x, y⟩
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ ∀ᶠ (a : α × γ) in 𝓝 (x, y), a.1 ∈ s → a.2 < f a.1
have pos : ∀ (hx : x ∈ s), ∀ᶠ (a : α × γ) in 𝓝 (x, y), a.1 ∈ s → a.2 < f a.1
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ ∀ᶠ (a : α × γ) in 𝓝 (x, y), a.1 ∈ s → a.2 < f a.1
have neg : ∀ (hx : x ∉ s), ∀ᶠ (a : α × γ) in 𝓝 (x, y), a.1 ∈ s → a.2 < f a.1
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ ∀ᶠ (a : α × γ) in 𝓝 (x, y), a.1 ∈ s → a.2 < f a.1
have 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
Tactic: have ⟨y', hy', z, hz, h₁⟩ := (h hx).exists_disjoint_Iio_Ioi
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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 : α × γ
⊢ (a.1 ∈ s → z < f a.1) ∧ a.2 < y' → a.1 ∈ s → a.2 < f a.1
have h₂ : ∀ (h₂ : a.1 ∈ s → z < f a.1) (h₃ : a.2 < y'), a.1 ∈ s → a.2 < f a.1
Tactic: ⟨h₂, h₃⟩
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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 : α × γ) in 𝓝 (x, y), a.1 ∈ s → a.2 < f a.1
have 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
Tactic: filter_upwards [(hf x hx z hz).prodMk_nhds (eventually_lt_nhds hy')]
        with _ ⟨h₂, h₃⟩ h₄ using h₁ _ h₃ _ <| h₂ h₄
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ ∀ᶠ (a : α × γ) in 𝓝 (x, y), a.1 ∈ s → a.2 < f a.1
have h₃ : ∀ (a : α × γ), (a.1 ∈ s → z < f a.1) ∧ a.2 < 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₄
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ ∀ᶠ (a : α × γ) in 𝓝 (x, y), a.1 ∈ s → a.2 < f a.1
have h₄ : ∀ (a : α × γ) (h₂ : a.1 ∈ s → z < f a.1) (h₃ : a.2 < y') (h₄ : 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₄
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
⊢ ∀ᶠ (a : α × γ) in 𝓝 (x, y), a.1 ∈ s → a.2 < f a.1
have h₁ : ∀ (a : α × γ),
  Membership.mem (γ := Set (α × γ))
    {x : α × γ |
      Membership.mem (γ := Set (α × γ)) {x : α × γ | (fun (x : α × γ) ↦ x.1 ∈ sᶜ) x} x →
        Membership.mem (γ := Set (α × γ)) {x : α × γ | (fun (a : α × γ) ↦ a.1 ∈ s → a.2 < f a.1) x} x}
    a
Tactic: filter_upwards [(continuous_fst.tendsto _).eventually (hs.isOpen_compl.eventually_mem hx)]
        with _ h₁ h₂ using (h₁ h₂).elim
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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
h₁ :
  ∀ (a : α × γ),
    Membership.mem (γ := Set (α × γ))
      {x : α × γ |
        Membership.mem (γ := Set (α × γ)) {x : α × γ | (fun (x : α × γ) ↦ x.1 ∈ sᶜ) x} x →
          Membership.mem (γ := Set (α × γ)) {x : α × γ | (fun (a : α × γ) ↦ a.1 ∈ s → a.2 < f a.1) x} x}
      a
⊢ ∀ᶠ (a : α × γ) in 𝓝 (x, y), a.1 ∈ s → a.2 < f a.1
have h₂ : ∀ (a : α × γ), a.1 ∈ sᶜ → a.1 ∈ s → a.2 < f a.1
Tactic: filter_upwards [(continuous_fst.tendsto _).eventually (hs.isOpen_compl.eventually_mem hx)]
        with _ h₁ h₂ using (h₁ h₂).elim
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
δ : Type u_5
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : (g ∘ f) x > y
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : δ) ↦ (g ∘ f) x1 > x2) x' y
have pos : ∀ (h : ∃ (l : γ), l < f x), ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : δ) ↦ (g ∘ f) x1 > x2) x' y
Tactic: by_cases! h : ∃ l, l < f x
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
δ : Type u_5
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : (g ∘ f) x > y
pos : ∀ (h : ∃ (l : γ), l < f x), ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : δ) ↦ (g ∘ f) x1 > x2) x' y
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : δ) ↦ (g ∘ f) x1 > x2) x' y
have neg : ∀ (h : ∀ (l : γ), f x ≤ l), ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : δ) ↦ (g ∘ f) x1 > x2) x' y
Tactic: by_cases! h : ∃ l, l < f x
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
δ : Type u_5
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : (g ∘ f) x > y
h : ∃ (l : γ), l < f x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : δ) ↦ (g ∘ f) x1 > x2) x' y
have pos : ∀ (z : γ) (zlt : z < f x) (hz : Ioc z (f x) ⊆ g ⁻¹' Ioi y),
  ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : δ) ↦ (g ∘ f) x1 > x2) x' y
Tactic: obtain ⟨z, zlt, hz⟩ : ∃ z < f x, Ioc z (f x) ⊆ g ⁻¹' Ioi y :=
      exists_Ioc_subset_of_mem_nhds (hg (Ioi_mem_nhds hy)) h
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
δ : Type u_5
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : (g ∘ f) x > y
h : ∃ (l : γ), l < f x
z : γ
zlt : z < f x
hz : Ioc z (f x) ⊆ g ⁻¹' Ioi y
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : δ) ↦ (g ∘ f) x1 > x2) x' y
have h₁ : ∀ (a : α) (ha : f a > z), (g ∘ f) a > y
Tactic: filter_upwards [hf z zlt] with a ha
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
δ : Type u_5
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousAt f x
gmon : Monotone g
⊢ LowerSemicontinuousAt (g ∘ f) x
have simp : ∀ (hf : LowerSemicontinuousWithinAt f univ x), LowerSemicontinuousWithinAt (g ∘ f) univ x
Tactic: simp only [← lowerSemicontinuousWithinAt_univ_iff] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst_1 : AddCommMonoid γ
inst_2 : LinearOrder γ
inst_3 : IsOrderedAddMonoid γ
inst_4 : TopologicalSpace γ
inst_5 : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (Y := γ) (fun (p : γ × γ) ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun (z : α) ↦ f z + g z) x > y
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : γ) ↦ (fun (z : α) ↦ f z + g z) x1 > x2) x' y
have obtain : ∀ (u v : Set γ) (u_open : IsOpen[inst_4] u) (xu : f x ∈ u) (v_open : IsOpen[inst_4] v) (xv : g x ∈ v)
  (h : u ×ˢ v ⊆ {p : γ × γ | y < p.1 + p.2}),
  ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : γ) ↦ (fun (z : α) ↦ f z + g z) x1 > x2) x' y
Tactic: obtain ⟨u, v, u_open, xu, v_open, xv, h⟩ :
    ∃ u v : Set γ,
      IsOpen u ∧ f x ∈ u ∧ IsOpen v ∧ g x ∈ v ∧ u ×ˢ v ⊆ { p : γ × γ | y < p.fst + p.snd } :=
    mem_nhds_prod_iff'.1 (hcont (isOpen_Ioi.mem_nhds hy))