awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
ι : Sort u_4
δ' : Type u_6
inst_1 : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝 x, BddAbove.{u_6} (α := δ') (range fun (i : ι) ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) univ x
⊢ LowerSemicontinuousWithinAt.{u_1, u_6} (β := δ') (fun (x' : α) ↦ ⨆ (i : ι), f i x') univ x
have bdd₁ : ∀ᶠ (y : α) in 𝓝[univ] x, BddAbove.{u_6} (α := δ') (range fun (i : ι) ↦ f i y)
Tactic: rw [← nhdsWithin_univ] at bdd
Cleared hypotheses: bdd, h
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
ι : Type u_4
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt (β := ℝ≥0∞) (fun (x' : α) ↦ ∑' (i : ι), f i x') s x
have simp_rw : LowerSemicontinuousWithinAt (β := ℝ≥0∞) (fun (x' : α) ↦ ⨆ (s : Finset ι), ∑ i ∈ s, f i x') s x
Tactic: simp_rw [ENNReal.tsum_eq_iSup_sum]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
ι : Type u_4
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt (β := ℝ≥0∞) (fun (x' : α) ↦ ⨆ (s : Finset ι), ∑ i ∈ s, f i x') s x
have refine : ∀ (b : Finset ι), LowerSemicontinuousWithinAt (β := ℝ≥0∞) (fun (x' : α) ↦ ∑ i ∈ b, f i x') s x
Tactic: refine lowerSemicontinuousWithinAt_iSup fun b => ?_
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
ι : Type u_4
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuousAt (f i) x
⊢ LowerSemicontinuousAt (β := ℝ≥0∞) (fun (x' : α) ↦ ∑' (i : ι), f i x') x
have simp_rw : ∀ (h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) univ x),
  LowerSemicontinuousWithinAt (β := ℝ≥0∞) (fun (x' : α) ↦ ∑' (i : ι), f i x') univ x
Tactic: simp_rw [← lowerSemicontinuousWithinAt_univ_iff] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
γ : Type u_4
inst_1 : LinearOrder γ
f : α → γ
⊢ UpperSemicontinuous f ↔ ∀ (y : γ), IsClosed[inst] (f ⁻¹' Ici y)
have rw : (∀ (y : γ), IsOpen[inst] (f ⁻¹' Iio y)) ↔ ∀ (y : γ), IsClosed[inst] (f ⁻¹' Ici y)
Tactic: rw [upperSemicontinuous_iff_isOpen_preimage]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_4
inst : TopologicalSpace α
β : Type u_5
f : α → β
s : Set α
a : α
inst_1 : PartialOrder β
inst_2 : CommGroup β
inst_3 : IsOrderedMonoid β
⊢ LowerSemicontinuousWithinAt f⁻¹ s a ↔ UpperSemicontinuousWithinAt f s a
have rw : (∀ (x : β), x⁻¹ < f⁻¹ a → ∀ᶠ (x' : α) in 𝓝[s] a, x⁻¹ < f⁻¹ x') ↔ ∀ (y : β), f a < y → ∀ᶠ (x' : α) in 𝓝[s] a, f x' < y
Tactic: rw [lowerSemicontinuousWithinAt_iff, inv_surjective.forall, upperSemicontinuousWithinAt_iff]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
γ : Type u_5
inst_1 : AddCommMonoid γ
inst_2 : LinearOrder γ
inst_3 : IsOrderedAddMonoid γ
inst_4 : TopologicalSpace γ
inst_5 : OrderTopology γ
f g : α → γ
hf : UpperSemicontinuousAt f x
hg : UpperSemicontinuousAt g x
hcont : ContinuousAt (Y := γ) (fun (p : γ × γ) ↦ p.1 + p.2) (f x, g x)
⊢ UpperSemicontinuousAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ f z + g z) x
have simp_rw : ∀ (hf : UpperSemicontinuousWithinAt f univ x) (hg : UpperSemicontinuousWithinAt g univ x),
  UpperSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ f z + g z) univ x
Tactic: simp_rw [← upperSemicontinuousWithinAt_univ_iff] at *
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
ι : Type u_4
γ : Type u_5
inst_1 : AddCommMonoid γ
inst_2 : LinearOrder γ
inst_3 : IsOrderedAddMonoid γ
inst_4 : TopologicalSpace γ
inst_5 : OrderTopology γ
inst_6 : ContinuousAdd γ
f : ι → α → γ
a : Finset ι
ha : ∀ i ∈ a, UpperSemicontinuousAt (f i) x
⊢ UpperSemicontinuousAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ a, f i z) x
have simp_rw : ∀ (ha : ∀ i ∈ a, UpperSemicontinuousWithinAt (f i) univ x),
  UpperSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ a, f i z) univ x
Tactic: simp_rw [← upperSemicontinuousWithinAt_univ_iff] at *
Cleared hypotheses: ha
-- 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 γ
f : α → γ
⊢ ContinuousWithinAt f s x ↔ LowerSemicontinuousWithinAt f s x ∧ UpperSemicontinuousWithinAt f s x
have refine : LowerSemicontinuousWithinAt f s x ∧ UpperSemicontinuousWithinAt f s x → ContinuousWithinAt f s x
Tactic: refine ⟨fun h => ⟨h.lowerSemicontinuousWithinAt, h.upperSemicontinuousWithinAt⟩, ?_⟩
-- 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 γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
⊢ f ⁻¹' v ∈ 𝓝[s] x
have pos : ∀ (Hl : ∃ (l : γ), l < f x), f ⁻¹' v ∈ 𝓝[s] x
Tactic: by_cases! Hl : ∃ 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 γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
pos : ∀ (Hl : ∃ (l : γ), l < f x), f ⁻¹' v ∈ 𝓝[s] x
⊢ f ⁻¹' v ∈ 𝓝[s] x
have neg : ∀ (Hl : ∀ (l : γ), f x ≤ l), f ⁻¹' v ∈ 𝓝[s] x
Tactic: by_cases! Hl : ∃ 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 γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ (l : γ), l < f x
⊢ f ⁻¹' v ∈ 𝓝[s] x
have pos : ∀ (l : γ) (lfx : l < f x) (hl : Ioc l (f x) ⊆ v), f ⁻¹' v ∈ 𝓝[s] x
Tactic: rcases exists_Ioc_subset_of_mem_nhds hv Hl with ⟨l, lfx, hl⟩
-- 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 γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ (l : γ), l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
⊢ f ⁻¹' v ∈ 𝓝[s] x
have pos : ∀ (Hu : ∃ (u : γ), f x < u), f ⁻¹' v ∈ 𝓝[s] x
Tactic: by_cases! Hu : ∃ u, f x < u
-- 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 γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ (l : γ), l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
pos : ∀ (Hu : ∃ (u : γ), f x < u), f ⁻¹' v ∈ 𝓝[s] x
⊢ f ⁻¹' v ∈ 𝓝[s] x
have neg : ∀ (Hu : ∀ (u : γ), u ≤ f x), f ⁻¹' v ∈ 𝓝[s] x
Tactic: by_cases! Hu : ∃ u, f x < u
-- 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 γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ (l : γ), l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∃ (u : γ), f x < u
⊢ f ⁻¹' v ∈ 𝓝[s] x
have pos : ∀ (u : γ) (fxu : f x < u) (hu : Ico (f x) u ⊆ v), f ⁻¹' v ∈ 𝓝[s] x
Tactic: rcases exists_Ico_subset_of_mem_nhds hv Hu with ⟨u, fxu, hu⟩
-- 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 γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ (l : γ), l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∃ (u : γ), f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
⊢ f ⁻¹' v ∈ 𝓝[s] x
have h : ∀ (a : α) (lfa : f a > l) (fau : f a < u), a ∈ f ⁻¹' v
Tactic: filter_upwards [h₁ l lfx, h₂ u fxu] with a lfa fau
-- 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 γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ (l : γ), l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∃ (u : γ), f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
a : α
lfa : f a > l
fau : f a < u
⊢ a ∈ f ⁻¹' v
have h : ∀ (h : f a ≤ f x), a ∈ f ⁻¹' v
Tactic: rcases le_or_gt (f a) (f x) with h | 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 γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ (l : γ), l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∃ (u : γ), f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
a : α
lfa : f a > l
fau : f a < u
h : ∀ (h : f a ≤ f x), a ∈ f ⁻¹' v
⊢ a ∈ f ⁻¹' v
have h₃ : ∀ (h : f x < f a), a ∈ f ⁻¹' v
Tactic: rcases le_or_gt (f a) (f x) with h | 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 γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ (l : γ), l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∀ (u : γ), u ≤ f x
⊢ f ⁻¹' v ∈ 𝓝[s] x
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x' : α) ↦ ((fun (x1 : α) (x2 : γ) ↦ f x1 > x2) x' l : Prop)) x} x →
        x ∈ f ⁻¹' v}
    a
Tactic: filter_upwards [h₁ l lfx] with a lfa using hl ⟨lfa, Hu (f a)⟩
-- 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 γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ (l : γ), l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∀ (u : γ), u ≤ f x
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x' : α) ↦ ((fun (x1 : α) (x2 : γ) ↦ f x1 > x2) x' l : Prop)) x} x →
          x ∈ f ⁻¹' v}
      a
⊢ f ⁻¹' v ∈ 𝓝[s] x
have h₃ : ∀ (a : α), f a > l → a ∈ f ⁻¹' v
Tactic: filter_upwards [h₁ l lfx] with a lfa using hl ⟨lfa, Hu (f a)⟩
-- 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 γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (l : γ), f x ≤ l
⊢ f ⁻¹' v ∈ 𝓝[s] x
have pos : ∀ (Hu : ∃ (u : γ), f x < u), f ⁻¹' v ∈ 𝓝[s] x
Tactic: by_cases! Hu : ∃ u, f x < u
-- 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 γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (l : γ), f x ≤ l
pos : ∀ (Hu : ∃ (u : γ), f x < u), f ⁻¹' v ∈ 𝓝[s] x
⊢ f ⁻¹' v ∈ 𝓝[s] x
have neg : ∀ (Hu : ∀ (u : γ), u ≤ f x), f ⁻¹' v ∈ 𝓝[s] x
Tactic: by_cases! Hu : ∃ u, f x < u
-- 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 γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (l : γ), f x ≤ l
Hu : ∃ (u : γ), f x < u
⊢ f ⁻¹' v ∈ 𝓝[s] x
have pos : ∀ (u : γ) (fxu : f x < u) (hu : Ico (f x) u ⊆ v), f ⁻¹' v ∈ 𝓝[s] x
Tactic: rcases exists_Ico_subset_of_mem_nhds hv Hu with ⟨u, fxu, hu⟩
-- 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 γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (l : γ), f x ≤ l
Hu : ∃ (u : γ), f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
⊢ f ⁻¹' v ∈ 𝓝[s] x
have h : ∀ (a : α) (lfa : f a < u), a ∈ f ⁻¹' v
Tactic: filter_upwards [h₂ u fxu] with a lfa
-- 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 γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (l : γ), f x ≤ l
Hu : ∃ (u : γ), f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
a : α
lfa : f a < u
⊢ a ∈ f ⁻¹' v
have h : f a ∈ Ico (f x) u
Tactic: apply hu
-- 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 γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (l : γ), f x ≤ l
Hu : ∀ (u : γ), u ≤ f x
⊢ f ⁻¹' v ∈ 𝓝[s] x
have neg : ∀ (x : α), f x ∈ v
Tactic: apply Filter.Eventually.of_forall
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (l : γ), f x ≤ l
Hu : ∀ (u : γ), u ≤ f x
a : α
⊢ f a ∈ v
have this : f a = f x
Tactic: have : f a = f x := le_antisymm (Hu _) (Hl _)
-- 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 γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (l : γ), f x ≤ l
Hu : ∀ (u : γ), u ≤ f x
a : α
this : f a = f x
⊢ f a ∈ v
have neg : f x ∈ v
Tactic: rw [this]
-- 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 γ
f : α → γ
⊢ ContinuousAt f x ↔ LowerSemicontinuousAt f x ∧ UpperSemicontinuousAt f x
have simp_rw : ContinuousWithinAt f univ x ↔ LowerSemicontinuousAt f x ∧ UpperSemicontinuousAt f x
Tactic: simp_rw [← continuousWithinAt_univ, ← lowerSemicontinuousWithinAt_univ_iff, ←
    upperSemicontinuousWithinAt_univ_iff, continuousWithinAt_iff_lower_upperSemicontinuousWithinAt]
-- 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 γ
f : α → γ
simp_rw : ContinuousWithinAt f univ x ↔ LowerSemicontinuousAt f x ∧ UpperSemicontinuousAt f x
⊢ ContinuousAt f x ↔ LowerSemicontinuousAt f x ∧ UpperSemicontinuousAt f x
have simp_rw₁ : ContinuousWithinAt f univ x ↔ LowerSemicontinuousWithinAt f univ x ∧ UpperSemicontinuousAt f x
Tactic: simp_rw [← continuousWithinAt_univ, ← lowerSemicontinuousWithinAt_univ_iff, ←
    upperSemicontinuousWithinAt_univ_iff, continuousWithinAt_iff_lower_upperSemicontinuousWithinAt]
-- 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 γ
f : α → γ
simp_rw : ContinuousWithinAt f univ x ↔ LowerSemicontinuousAt f x ∧ UpperSemicontinuousAt f x
simp_rw₁ : ContinuousWithinAt f univ x ↔ LowerSemicontinuousWithinAt f univ x ∧ UpperSemicontinuousAt f x
⊢ ContinuousAt f x ↔ LowerSemicontinuousAt f x ∧ UpperSemicontinuousAt f x
have simp_rw₂ : ContinuousWithinAt f univ x ↔ LowerSemicontinuousWithinAt f univ x ∧ UpperSemicontinuousWithinAt f univ x
Tactic: simp_rw [← continuousWithinAt_univ, ← lowerSemicontinuousWithinAt_univ_iff, ←
    upperSemicontinuousWithinAt_univ_iff, continuousWithinAt_iff_lower_upperSemicontinuousWithinAt]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
γ : Type u_4
inst_1 : LinearOrder γ
inst_2 : TopologicalSpace γ
inst_3 : OrderTopology γ
f : α → γ
⊢ ContinuousOn f s ↔ LowerSemicontinuousOn f s ∧ UpperSemicontinuousOn f s
have simp : (∀ x ∈ s, LowerSemicontinuousWithinAt f s x ∧ UpperSemicontinuousWithinAt f s x) ↔
  LowerSemicontinuousOn f s ∧ UpperSemicontinuousOn f s
Tactic: simp only [ContinuousOn, continuousWithinAt_iff_lower_upperSemicontinuousWithinAt]
-- 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 : OrderTopology γ
f : α → γ
⊢ Continuous[inst, inst_2] f ↔ LowerSemicontinuous f ∧ UpperSemicontinuous f
have simp_rw : ContinuousOn f univ ↔ LowerSemicontinuous f ∧ UpperSemicontinuous f
Tactic: simp_rw [← continuousOn_univ, continuousOn_iff_lower_upperSemicontinuousOn,
    lowerSemicontinuousOn_univ_iff, upperSemicontinuousOn_univ_iff]
-- 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 : OrderTopology γ
f : α → γ
simp_rw : ContinuousOn f univ ↔ LowerSemicontinuous f ∧ UpperSemicontinuous f
⊢ Continuous[inst, inst_2] f ↔ LowerSemicontinuous f ∧ UpperSemicontinuous f
have simp_rw₁ : LowerSemicontinuousOn f univ ∧ UpperSemicontinuousOn f univ ↔ LowerSemicontinuous f ∧ UpperSemicontinuous f
Tactic: simp_rw [← continuousOn_univ, continuousOn_iff_lower_upperSemicontinuousOn,
    lowerSemicontinuousOn_univ_iff, upperSemicontinuousOn_univ_iff]
-- 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 : OrderTopology γ
f : α → γ
simp_rw : ContinuousOn f univ ↔ LowerSemicontinuous f ∧ UpperSemicontinuous f
simp_rw₁ : LowerSemicontinuousOn f univ ∧ UpperSemicontinuousOn f univ ↔ LowerSemicontinuous f ∧ UpperSemicontinuous f
⊢ Continuous[inst, inst_2] f ↔ LowerSemicontinuous f ∧ UpperSemicontinuous f
have simp_rw₂ : LowerSemicontinuous f ∧ UpperSemicontinuousOn f univ ↔ LowerSemicontinuous f ∧ UpperSemicontinuous f
Tactic: simp_rw [← continuousOn_univ, continuousOn_iff_lower_upperSemicontinuousOn,
    lowerSemicontinuousOn_univ_iff, upperSemicontinuousOn_univ_iff]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Defs (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
r r' : α → β → Prop
s : Set α
a : α
h : SemicontinuousWithinAt r s a
has : a ∈ s
hfg : ∀ᶠ (x : α) in 𝓝[s] a, ∀ (y : β), r x y ↔ r' x y
b : β
hb : r' a b
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, r' x' b
have hfg₁ : ∀ᶠ (x : α) in 𝓝[s] a, r x = r' x
Tactic: simp_rw [← propext_iff, ← funext_iff] at hfg
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Defs (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
r r' : α → β → Prop
s : Set α
a : α
h : SemicontinuousWithinAt r s a
has : a ∈ s
b : β
hb : r' a b
hfg : ∀ᶠ (x : α) in 𝓝[s] a, r x = r' x
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, r' x' b
have hb₁ : r a b
Tactic: rw [← Filter.EventuallyEq.eq_of_nhdsWithin hfg has] at hb
Cleared hypotheses: hb, hfg
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
r r' : α → β → Prop
s : Set α
a : α
h : SemicontinuousWithinAt r s a
has : a ∈ s
b : β
hb : r a b
hfg : ∀ᶠ (x : α) in 𝓝[s] a, r x = r' x
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, r' x' b
have h₁ : ∀ (x : α) (hx : r x = r' x) (hxb : r x b), r' x b
Tactic: filter_upwards [hfg, h b hb] with x hx hxb
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
r : α → β → Prop
s : Set α
⊢ Semicontinuous (s.restrict (π := fun (a : α) ↦ β → Prop) r) ↔ SemicontinuousOn r s
have rw : (∀ (x : α) (h : x ∈ s),
    SemicontinuousAt (s.restrict (π := fun (a : α) ↦ β → Prop) r) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h)) ↔
  ∀ x ∈ s, SemicontinuousWithinAt r s x
Tactic: rw [SemicontinuousOn, Semicontinuous, SetCoe.forall]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
r : α → β → Prop
s : Set α
⊢ (∀ (x : α) (h : x ∈ s),
      SemicontinuousAt (s.restrict (π := fun (a : α) ↦ β → Prop) r) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h)) ↔
    ∀ x ∈ s, SemicontinuousWithinAt r s x
have refine : ∀ (a : α) (ha : a ∈ s) (b : β),
  s.restrict (π := fun (a : α) ↦ β → Prop) r (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha) b →
    ((∀ᶠ (x' : (↑s : Type u_1)) in 𝓝 (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha),
        s.restrict (π := fun (a : α) ↦ β → Prop) r x' b) ↔
      ∀ᶠ (x' : α) in 𝓝[s] a, r x' b)
Tactic: refine forall₂_congr fun a ha ↦ forall₂_congr fun b _ ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace γ
inst_2 : Preorder β
f g : α → β
x : α
s t : Set α
y z : β
⊢ (Semicontinuous fun (x1 : α) (x2 : β) ↦ ¬f x1 ≤ x2) ↔ ∀ (x : α) (y : β), (∃ᶠ (x' : α) in 𝓝 x, f x' ≤ y) → f x ≤ y
have simp_rw : (∀ (x : α), SemicontinuousAt (fun (x1 : α) (x2 : β) ↦ ¬f x1 ≤ x2) x) ↔
  ∀ (x : α) (y : β), (∃ᶠ (x' : α) in 𝓝 x, f x' ≤ y) → f x ≤ y
Tactic: simp_rw [Semicontinuous, SemicontinuousAt, ← not_frequently, not_imp_not]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace γ
inst_2 : Preorder β
f g : α → β
x : α
s t : Set α
y z : β
simp_rw :
  (∀ (x : α), SemicontinuousAt (fun (x1 : α) (x2 : β) ↦ ¬f x1 ≤ x2) x) ↔
    ∀ (x : α) (y : β), (∃ᶠ (x' : α) in 𝓝 x, f x' ≤ y) → f x ≤ y
⊢ (Semicontinuous fun (x1 : α) (x2 : β) ↦ ¬f x1 ≤ x2) ↔ ∀ (x : α) (y : β), (∃ᶠ (x' : α) in 𝓝 x, f x' ≤ y) → f x ≤ y
have simp_rw₁ : (∀ (x : α) (y : β), ¬f x ≤ y → ∀ᶠ (x' : α) in 𝓝 x, ¬f x' ≤ y) ↔
  ∀ (x : α) (y : β), (∃ᶠ (x' : α) in 𝓝 x, f x' ≤ y) → f x ≤ y
Tactic: simp_rw [Semicontinuous, SemicontinuousAt, ← not_frequently, not_imp_not]