awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∃ (l : γ), l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₂z : g z > z₂
pos : ∀ (H : g z ≤ g x), min (g z) (g x) ∈ v
⊢ min (g z) (g x) ∈ v
have neg : ∀ (H : g x < g z), min (g z) (g x) ∈ v
Tactic: by_cases! H : g z ≤ g x
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (hypothesis)
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
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}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∃ (l : γ), l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₂z : g z > z₂
⊢ f z + g z > y
have A2 : min (g z) (g x) ∈ v
Tactic: have A2 : min (g z) (g x) ∈ v := by
        by_cases! H : g z ≤ g x
        · simpa [H] using h₂ ⟨h₂z, H⟩
        · simpa [H.le] using h₂ ⟨z₂lt, le_rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (hypothesis)
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
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}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∃ (l : γ), l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₂z : g z > z₂
A2 : min (g z) (g x) ∈ v
⊢ f z + g z > y
have this : (f x, min (g z) (g x)) ∈ u ×ˢ v
Tactic: have : (f x, min (g z) (g x)) ∈ u ×ˢ v := ⟨xu, A2⟩
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (hypothesis)
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
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}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ¬∃ (l : γ), l < g x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : γ) ↦ (fun (z : α) ↦ f z + g z) x1 > x2) x' y
have hx₃ : ∀ (x_1 : γ), g x ≤ x_1
Tactic: simp only [not_exists, not_lt] at hx₁ hx₂
Cleared hypotheses: hx₂
-- 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
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}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∀ (x_1 : γ), g x ≤ x_1
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : γ) ↦ (fun (z : α) ↦ f z + g z) x1 > x2) x' y
have neg : ∀ (x : α), (fun (x1 : α) (x2 : γ) ↦ (fun (z : α) ↦ f z + g z) x1 > x2) x y
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_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
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}
hx₁ : ∀ (x_1 : γ), f x ≤ x_1
hx₂ : ∀ (x_1 : γ), g x ≤ x_1
z : α
⊢ (fun (x1 : α) (x2 : γ) ↦ (fun (z : α) ↦ f z + g z) x1 > x2) z y
have this : (f x, g x) ∈ u ×ˢ v
Tactic: have : (f x, g x) ∈ u ×ˢ v := ⟨xu, xv⟩
-- 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 : LowerSemicontinuousAt f x
hg : LowerSemicontinuousAt g x
hcont : ContinuousAt (Y := γ) (fun (p : γ × γ) ↦ p.1 + p.2) (f x, g x)
⊢ LowerSemicontinuousAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ f z + g z) x
have simp_rw : ∀ (hf : LowerSemicontinuousWithinAt f univ x) (hg : LowerSemicontinuousWithinAt g univ x),
  LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ f z + g z) univ x
Tactic: simp_rw [← lowerSemicontinuousWithinAt_univ_iff] at *
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
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 : ι
s_1 : Finset ι
ia : a ∉ s_1
IH :
  ∀ (ha : ∀ i ∈ s_1, LowerSemicontinuousWithinAt (f i) s x),
    LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ s_1, f i z) s x
ha : ∀ i ∈ insert a s_1, LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ insert a s_1, f i z) s x
have insert : LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ f a z + ∑ i ∈ s_1, f i z) s x
Tactic: simp only [ia, Finset.sum_insert, not_false_iff]
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
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, LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ a, f i z) s x
have empty : ∀ (ha : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → LowerSemicontinuousWithinAt (f i) s x),
  LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ ∅, f i z) s x
Tactic: induction a using Finset.induction_on with
    | empty => exact lowerSemicontinuousWithinAt_const
    | insert _ _ ia IH =>
      simp only [ia, Finset.sum_insert, not_false_iff]
      exact
        LowerSemicontinuousWithinAt.add (ha _ (Finset.mem_insert_self ..))
          (IH fun j ja => ha j (Finset.mem_insert_of_mem ja))
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
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, LowerSemicontinuousWithinAt (f i) s x
empty :
  ∀ (ha : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → LowerSemicontinuousWithinAt (f i) s x),
    LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ ∅, f i z) s x
⊢ LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ a, f i z) s x
have insert : ∀ (a : ι) (s_1 : Finset ι) (ia : a ∉ s_1)
  (IH :
    ∀ (ha : ∀ i ∈ s_1, LowerSemicontinuousWithinAt (f i) s x),
      LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ s_1, f i z) s x)
  (ha : ∀ i ∈ insert a s_1, LowerSemicontinuousWithinAt (f i) s x),
  LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ insert a s_1, f i z) s x
Tactic: induction a using Finset.induction_on with
    | empty => exact lowerSemicontinuousWithinAt_const
    | insert _ _ ia IH =>
      simp only [ia, Finset.sum_insert, not_false_iff]
      exact
        LowerSemicontinuousWithinAt.add (ha _ (Finset.mem_insert_self ..))
          (IH fun j ja => ha j (Finset.mem_insert_of_mem ja))
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
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, LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ a, f i z) s x
have empty : ∀ (ha : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → LowerSemicontinuousWithinAt (f i) s x),
  LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ ∅, f i z) s x
Tactic: classical
    induction a using Finset.induction_on with
    | empty => exact lowerSemicontinuousWithinAt_const
    | insert _ _ ia IH =>
      simp only [ia, Finset.sum_insert, not_false_iff]
      exact
        LowerSemicontinuousWithinAt.add (ha _ (Finset.mem_insert_self ..))
          (IH fun j ja => ha j (Finset.mem_insert_of_mem ja))
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
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, LowerSemicontinuousWithinAt (f i) s x
empty :
  ∀ (ha : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → LowerSemicontinuousWithinAt (f i) s x),
    LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ ∅, f i z) s x
⊢ LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ a, f i z) s x
have insert : ∀ (a : ι) (s_1 : Finset ι) (ia : a ∉ s_1)
  (IH :
    ∀ (ha : ∀ i ∈ s_1, LowerSemicontinuousWithinAt (f i) s x),
      LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ s_1, f i z) s x)
  (ha : ∀ i ∈ insert a s_1, LowerSemicontinuousWithinAt (f i) s x),
  LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ insert a s_1, f i z) s x
Tactic: classical
    induction a using Finset.induction_on with
    | empty => exact lowerSemicontinuousWithinAt_const
    | insert _ _ ia IH =>
      simp only [ia, Finset.sum_insert, not_false_iff]
      exact
        LowerSemicontinuousWithinAt.add (ha _ (Finset.mem_insert_self ..))
          (IH fun j ja => ha j (Finset.mem_insert_of_mem ja))
Cleared hypotheses: a, ha
-- 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, LowerSemicontinuousAt (f i) x
⊢ LowerSemicontinuousAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ a, f i z) x
have simp_rw : ∀ (ha : ∀ i ∈ a, LowerSemicontinuousWithinAt (f i) univ x),
  LowerSemicontinuousWithinAt.{u_1, u_5} (β := γ) (fun (z : α) ↦ ∑ i ∈ a, f i z) univ x
Tactic: simp_rw [← lowerSemicontinuousWithinAt_univ_iff] at *
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_4
β : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder β
f g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : (fun (x : α) ↦ max (f x) (g x)) a > b
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, (fun (x1 : α) (x2 : β) ↦ (fun (x : α) ↦ max (f x) (g x)) x1 > x2) x' b
have simp : ∀ (hb : b < f a ∨ b < g a), ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∨ b < g x'
Tactic: simp only [lt_sup_iff] at hb ⊢
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_4
β : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder β
f g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < f a ∨ b < g a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∨ b < g x'
have inl : ∀ (hb : b < f a), ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∨ b < g x'
Tactic: rcases hb with hb | hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_4
β : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder β
f g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < f a ∨ b < g a
inl : ∀ (hb : b < f a), ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∨ b < g x'
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∨ b < g x'
have inr : ∀ (hb : b < g a), ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∨ b < g x'
Tactic: rcases hb with hb | hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_4
β : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder β
f g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < f a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∨ b < g x'
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x' : α) ↦ ((fun (x1 : α) (x2 : β) ↦ f x1 > x2) x' b : Prop)) x} x →
        Membership.mem (γ := Set α) {x : α | (fun (x' : α) ↦ b < f x' ∨ b < g x') x} x}
    a
Tactic: filter_upwards [hf b hb] with x using Or.intro_left _
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_4
β : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder β
f g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < f a
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x' : α) ↦ ((fun (x1 : α) (x2 : β) ↦ f x1 > x2) x' b : Prop)) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x' : α) ↦ b < f x' ∨ b < g x') x} x}
      a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∨ b < g x'
have h₁ : ∀ (a : α), f a > b → b < f a ∨ b < g a
Tactic: filter_upwards [hf b hb] with x using Or.intro_left _
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_4
β : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder β
f g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < g a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∨ b < g x'
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x' : α) ↦ ((fun (x1 : α) (x2 : β) ↦ g x1 > x2) x' b : Prop)) x} x →
        Membership.mem (γ := Set α) {x : α | (fun (x' : α) ↦ b < f x' ∨ b < g x') x} x}
    a
Tactic: filter_upwards [hg b hb] with x using Or.intro_right _
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_4
β : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder β
f g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : b < g a
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x' : α) ↦ ((fun (x1 : α) (x2 : β) ↦ g x1 > x2) x' b : Prop)) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x' : α) ↦ b < f x' ∨ b < g x') x} x}
      a
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∨ b < g x'
have h₁ : ∀ (a : α), g a > b → b < f a ∨ b < g a
Tactic: filter_upwards [hg b hb] with x using Or.intro_right _
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_4
β : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder β
f g : α → β
a : α
hf : LowerSemicontinuousAt f a
hg : LowerSemicontinuousAt g a
⊢ LowerSemicontinuousAt.{u_4, u_5} (β := β) (fun (x : α) ↦ max (f x) (g x)) a
have rw : ∀ (hf : LowerSemicontinuousWithinAt f univ a) (hg : LowerSemicontinuousWithinAt g univ a),
  LowerSemicontinuousWithinAt.{u_4, u_5} (β := β) (fun (x : α) ↦ max (f x) (g x)) univ a
Tactic: rw [← lowerSemicontinuousWithinAt_univ_iff] at *
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_4
β : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder β
f g : α → β
s : Set α
a : α
hf : LowerSemicontinuousWithinAt f s a
hg : LowerSemicontinuousWithinAt g s a
b : β
hb : (fun (x : α) ↦ min (f x) (g x)) a > b
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, (fun (x1 : α) (x2 : β) ↦ (fun (x : α) ↦ min (f x) (g x)) x1 > x2) x' b
have simp : ∀ (hb : b < f a ∧ b < g a), ∀ᶠ (x' : α) in 𝓝[s] a, b < f x' ∧ b < g x'
Tactic: simp only [lt_inf_iff] at hb ⊢
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_4
β : Type u_5
inst : TopologicalSpace α
inst_1 : LinearOrder β
f g : α → β
a : α
hf : LowerSemicontinuousAt f a
hg : LowerSemicontinuousAt g a
⊢ LowerSemicontinuousAt.{u_4, u_5} (β := β) (fun (x : α) ↦ min (f x) (g x)) a
have rw : ∀ (hf : LowerSemicontinuousWithinAt f univ a) (hg : LowerSemicontinuousWithinAt g univ a),
  LowerSemicontinuousWithinAt.{u_4, u_5} (β := β) (fun (x : α) ↦ min (f x) (g x)) univ a
Tactic: rw [← lowerSemicontinuousWithinAt_univ_iff] at *
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
ι : Sort u_4
δ' : Type u_6
inst_1 : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove.{u_6} (α := δ') (range fun (i : ι) ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt.{u_1, u_6} (β := δ') (fun (x' : α) ↦ ⨆ (i : ι), f i x') s x
have inl : IsEmpty ι → LowerSemicontinuousWithinAt.{u_1, u_6} (β := δ') (fun (x' : α) ↦ ⨆ (i : ι), f i x') s x
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
ι : Sort u_4
δ' : Type u_6
inst_1 : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove.{u_6} (α := δ') (range fun (i : ι) ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
inl : IsEmpty ι → LowerSemicontinuousWithinAt.{u_1, u_6} (β := δ') (fun (x' : α) ↦ ⨆ (i : ι), f i x') s x
⊢ LowerSemicontinuousWithinAt.{u_1, u_6} (β := δ') (fun (x' : α) ↦ ⨆ (i : ι), f i x') s x
have inr : Nonempty ι → LowerSemicontinuousWithinAt.{u_1, u_6} (β := δ') (fun (x' : α) ↦ ⨆ (i : ι), f i x') s x
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
ι : Sort u_4
δ' : Type u_6
inst_1 : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove.{u_6} (α := δ') (range fun (i : ι) ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h_1 : Nonempty ι
y : δ'
hy : (fun (x' : α) ↦ (⨆ (i : ι), f i x' : δ')) x > y
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : δ') ↦ (fun (x' : α) ↦ (⨆ (i : ι), f i x' : δ')) x1 > x2) x' y
have inr : ∀ (i : ι) (hi : y < f i x),
  ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : δ') ↦ (fun (x' : α) ↦ (⨆ (i : ι), f i x' : δ')) x1 > x2) x' y
Tactic: rcases exists_lt_of_lt_ciSup hy with ⟨i, hi⟩
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
ι : Sort u_4
δ' : Type u_6
inst_1 : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove.{u_6} (α := δ') (range fun (i : ι) ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h_1 : Nonempty ι
y : δ'
hy : (fun (x' : α) ↦ (⨆ (i : ι), f i x' : δ')) x > y
i : ι
hi : y < f i x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : δ') ↦ (fun (x' : α) ↦ (⨆ (i : ι), f i x' : δ')) x1 > x2) x' y
have h₁ : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x' : α) ↦ ((fun (x1 : α) (x2 : δ') ↦ f i x1 > x2) x' y : Prop)) x} x →
        Membership.mem (γ := Set α)
          {x : α |
            Membership.mem (γ := Set α) {x : α | (fun (y : α) ↦ BddAbove.{u_6} (α := δ') (range fun (i : ι) ↦ f i y)) x}
                x →
              Membership.mem (γ := Set α)
                {x : α |
                  (fun (x' : α) ↦
                      ((fun (x1 : α) (x2 : δ') ↦ (fun (x' : α) ↦ (⨆ (i : ι), f i x' : δ')) x1 > x2) x' y : Prop))
                    x}
                x}
          x}
    a
Tactic: filter_upwards [h i y hi, bdd] with y hy hy' using hy.trans_le (le_ciSup hy' i)
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
ι : Sort u_4
δ' : Type u_6
inst_1 : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove.{u_6} (α := δ') (range fun (i : ι) ↦ f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h_1 : Nonempty ι
y : δ'
hy : (fun (x' : α) ↦ (⨆ (i : ι), f i x' : δ')) x > y
i : ι
hi : y < f i x
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x' : α) ↦ ((fun (x1 : α) (x2 : δ') ↦ f i x1 > x2) x' y : Prop)) x}
            x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α)
                  {x : α | (fun (y : α) ↦ BddAbove.{u_6} (α := δ') (range fun (i : ι) ↦ f i y)) x} x →
                Membership.mem (γ := Set α)
                  {x : α |
                    (fun (x' : α) ↦
                        ((fun (x1 : α) (x2 : δ') ↦ (fun (x' : α) ↦ (⨆ (i : ι), f i x' : δ')) x1 > x2) x' y : Prop))
                      x}
                  x}
            x}
      a
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun (x1 : α) (x2 : δ') ↦ (fun (x' : α) ↦ (⨆ (i : ι), f i x' : δ')) x1 > x2) x' y
have h₂ : ∀ (a : α), f i a > y → BddAbove.{u_6} (α := δ') (range fun (i : ι) ↦ f i a) → ⨆ (i : ι), f i a > y
Tactic: filter_upwards [h i y hi, bdd] with y hy hy' using hy.trans_le (le_ciSup hy' i)
-- Lean 4 proof step from Mathlib.Topology.Semicontinuity.Basic (goal)
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 : ι), LowerSemicontinuousAt (f i) x
⊢ LowerSemicontinuousAt.{u_1, u_6} (β := δ') (fun (x' : α) ↦ ⨆ (i : ι), f i x') x
have simp_rw : ∀ (h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) univ x),
  LowerSemicontinuousWithinAt.{u_1, u_6} (β := δ') (fun (x' : α) ↦ ⨆ (i : ι), f i x') univ x
Tactic: simp_rw [← lowerSemicontinuousWithinAt_univ_iff] at *
Cleared hypotheses: h