awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
⊢ ∀ᶠ (x : ℝ≥0∞) in map u f, (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) x 0

Tactic:
simp
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
apply : ∀ (b_1 : ℝ≥0∞), (∀ᶠ (n : ι) in f, b_1 ≤ u n) → b_1 ≤ b
⊢ liminf u f ≤ b

Tactic:
apply liminf_le_of_le ⟨0, by simp⟩

Premises used: Exists.intro, OfNat.ofNat, Filter.liminf_le_of_le
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
y : ℝ≥0∞
h : ∀ᶠ (n : ι) in f, y ≤ u n
obtain : ∀ (i : ι) (hi : y ≤ u i ∧ u i ≤ b), y ≤ b
⊢ y ≤ b

Tactic:
obtain ⟨i, hi⟩ := (Eventually.and h le_b).exists

Premises used: Filter.Eventually.and, Filter.Eventually.exists
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
y : ℝ≥0∞
h : ∀ᶠ (n : ι) in f, y ≤ u n
i : ι
hi : y ≤ u i ∧ u i ≤ b
⊢ y ≤ b

Tactic:
hi.1.trans hi.2

Premises used: And.right, And.left, LE.le.trans
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
y : ℝ≥0∞
h : ∀ᶠ (n : ι) in f, y ≤ u n
i : ι
hi : y ≤ u i ∧ u i ≤ b
⊢ y ≤ b

Tactic:
exact hi.1.trans hi.2

Premises used: And.right, And.left, LE.le.trans
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
⊢ liminf u f ≤ b

Tactic:
have liminf_le : f.liminf u ≤ b := by
    apply liminf_le_of_le ⟨0, by simp⟩
    intro y h
    obtain ⟨i, hi⟩ := (Eventually.and h le_b).exists
    exact hi.1.trans hi.2
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
liminf_le : liminf u f ≤ b
h : ∀ (i : ι) (i_le_b : u i ≤ b), (u i).toReal = b.truncateToReal (u i)
⊢ ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)

Tactic:
filter_upwards [le_b] with i i_le_b
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
liminf_le : liminf u f ≤ b
i : ι
i_le_b : u i ≤ b
⊢ (u i).toReal = b.truncateToReal (u i)

Tactic:
simp only [truncateToReal_eq_toReal b_ne_top i_le_b]

Premises used: ENNReal.truncateToReal_eq_toReal
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
liminf_le : liminf u f ≤ b
⊢ ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)

Tactic:
have aux : ∀ᶠ i in f, (u i).toReal = ENNReal.truncateToReal b (u i) := by
    filter_upwards [le_b] with i i_le_b
    simp only [truncateToReal_eq_toReal b_ne_top i_le_b]
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
liminf_le : liminf u f ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
rw rw₁ : (liminf u f).toReal = (liminf u f).toReal
⊢ (liminf u f).toReal = b.truncateToReal (liminf u f)

Tactic:
rw [truncateToReal_eq_toReal b_ne_top liminf_le]

Premises used: ENNReal.truncateToReal_eq_toReal
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
liminf_le : liminf u f ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
⊢ (liminf u f).toReal = b.truncateToReal (liminf u f)

Tactic:
have aux' : (f.liminf u).toReal = ENNReal.truncateToReal b (f.liminf u) := by
    rw [truncateToReal_eq_toReal b_ne_top liminf_le]
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
liminf_le : liminf u f ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
aux' : (liminf u f).toReal = b.truncateToReal (liminf u f)
simp_rw : liminf (fun (a : ι) ↦ b.truncateToReal (u a)) f = b.truncateToReal (liminf u f)
⊢ liminf (fun (i : ι) ↦ (u i).toReal) f = (liminf u f).toReal

Tactic:
simp_rw [liminf_congr aux, aux']

Premises used: Filter.liminf_congr
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
liminf_le : liminf u f ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
aux' : (liminf u f).toReal = b.truncateToReal (liminf u f)
⊢ ∀ᶠ (x : ℝ≥0∞) in map u f, (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≤ x2) x b

Tactic:
simpa only [eventually_map] using le_b

Premises used: Filter.eventually_map
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
liminf_le : liminf u f ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
aux' : (liminf u f).toReal = b.truncateToReal (liminf u f)
⊢ ∀ (x : ℝ≥0∞), (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) x 0

Tactic:
simp
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
liminf_le : liminf u f ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
aux' : (liminf u f).toReal = b.truncateToReal (liminf u f)
⊢ b.truncateToReal (liminf u f) = liminf (b.truncateToReal ∘ u) f

Tactic:
have key := Monotone.map_liminf_of_continuousAt (F := f) (monotone_truncateToReal b_ne_top) u
          (continuous_truncateToReal b_ne_top).continuousAt
          (IsBoundedUnder.isCoboundedUnder_ge ⟨b, by simpa only [eventually_map] using le_b⟩)
          ⟨0, Eventually.of_forall (by simp)⟩
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
liminf_le : liminf u f ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
aux' : (liminf u f).toReal = b.truncateToReal (liminf u f)
key : b.truncateToReal (liminf u f) = liminf (b.truncateToReal ∘ u) f
rw : liminf (fun (a : ι) ↦ b.truncateToReal (u a)) f = liminf (b.truncateToReal ∘ u) f
⊢ liminf (fun (a : ι) ↦ b.truncateToReal (u a)) f = b.truncateToReal (liminf u f)

Tactic:
rw [key]
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
liminf_le : liminf u f ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
aux' : (liminf u f).toReal = b.truncateToReal (liminf u f)
key : b.truncateToReal (liminf u f) = liminf (b.truncateToReal ∘ u) f
⊢ liminf (fun (a : ι) ↦ b.truncateToReal (u a)) f = liminf (b.truncateToReal ∘ u) f

Tactic:
rfl
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
h : ∀ (i : ι) (i_le_b : u i ≤ b), (u i).toReal = b.truncateToReal (u i)
⊢ ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)

Tactic:
filter_upwards [le_b] with i i_le_b
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
i : ι
i_le_b : u i ≤ b
⊢ (u i).toReal = b.truncateToReal (u i)

Tactic:
simp only [truncateToReal_eq_toReal b_ne_top i_le_b]

Premises used: ENNReal.truncateToReal_eq_toReal
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
⊢ ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)

Tactic:
have aux : ∀ᶠ i in f, (u i).toReal = ENNReal.truncateToReal b (u i) := by
    filter_upwards [le_b] with i i_le_b
    simp only [truncateToReal_eq_toReal b_ne_top i_le_b]
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
⊢ ∀ (a : ℝ≥0∞), (∀ᶠ (x : ℝ≥0∞) in map u f, (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≤ x2) 0 a

Tactic:
simp
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
rw rw₁ : (limsup u f).toReal = (limsup u f).toReal
⊢ (limsup u f).toReal = b.truncateToReal (limsup u f)

Tactic:
rw [truncateToReal_eq_toReal b_ne_top (limsup_le_of_le ⟨0, by simp⟩ le_b)]

Premises used: Filter.limsup_le_of_le, Exists.intro, ENNReal.truncateToReal_eq_toReal, OfNat.ofNat
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
⊢ (limsup u f).toReal = b.truncateToReal (limsup u f)

Tactic:
have aux' : (f.limsup u).toReal = ENNReal.truncateToReal b (f.limsup u) := by
    rw [truncateToReal_eq_toReal b_ne_top (limsup_le_of_le ⟨0, by simp⟩ le_b)]
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
aux' : (limsup u f).toReal = b.truncateToReal (limsup u f)
simp_rw : limsup (fun (a : ι) ↦ b.truncateToReal (u a)) f = b.truncateToReal (limsup u f)
⊢ limsup (fun (i : ι) ↦ (u i).toReal) f = (limsup u f).toReal

Tactic:
simp_rw [limsup_congr aux, aux']

Premises used: Filter.limsup_congr
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
aux' : (limsup u f).toReal = b.truncateToReal (limsup u f)
⊢ ∀ᶠ (x : ℝ≥0∞) in map u f, (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≤ x2) x b

Tactic:
simpa only [eventually_map] using le_b

Premises used: Filter.eventually_map
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
aux' : (limsup u f).toReal = b.truncateToReal (limsup u f)
⊢ ∀ (x : ℝ≥0∞), (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) x 0

Tactic:
simp
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
aux' : (limsup u f).toReal = b.truncateToReal (limsup u f)
⊢ b.truncateToReal (limsup u f) = limsup (b.truncateToReal ∘ u) f

Tactic:
have key := Monotone.map_limsup_of_continuousAt (F := f) (monotone_truncateToReal b_ne_top) u
          (continuous_truncateToReal b_ne_top).continuousAt
          ⟨b, by simpa only [eventually_map] using le_b⟩
          (IsBoundedUnder.isCoboundedUnder_le ⟨0, Eventually.of_forall (by simp)⟩)
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
aux' : (limsup u f).toReal = b.truncateToReal (limsup u f)
key : b.truncateToReal (limsup u f) = limsup (b.truncateToReal ∘ u) f
rw : limsup (fun (a : ι) ↦ b.truncateToReal (u a)) f = limsup (b.truncateToReal ∘ u) f
⊢ limsup (fun (a : ι) ↦ b.truncateToReal (u a)) f = b.truncateToReal (limsup u f)

Tactic:
rw [key]
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
aux' : (limsup u f).toReal = b.truncateToReal (limsup u f)
key : b.truncateToReal (limsup u f) = limsup (b.truncateToReal ∘ u) f
⊢ limsup (fun (a : ι) ↦ b.truncateToReal (u a)) f = limsup (b.truncateToReal ∘ u) f

Tactic:
rfl
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0
hf : IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
⊢ (↑(limsup u f) : ℝ≥0∞) = limsup (fun (i : ι) ↦ (↑(u i) : ℝ≥0∞)) f

Tactic:
eq_of_forall_nnreal_le_iff fun r ↦ ?_

Premises used: ENNReal.eq_of_forall_nnreal_le_iff
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0
hf : IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
refine : ∀ (r : ℝ≥0), (↑r : ℝ≥0∞) ≤ (↑(limsup u f) : ℝ≥0∞) ↔ (↑r : ℝ≥0∞) ≤ limsup (fun (i : ι) ↦ (↑(u i) : ℝ≥0∞)) f
⊢ (↑(limsup u f) : ℝ≥0∞) = limsup (fun (i : ι) ↦ (↑(u i) : ℝ≥0∞)) f

Tactic:
refine eq_of_forall_nnreal_le_iff fun r ↦ ?_

Premises used: ENNReal.eq_of_forall_nnreal_le_iff
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0
hf : IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
r : ℝ≥0
rw : (∀ y < r, ∃ᶠ (a : ι) in f, y < u a) ↔ ∀ y < (↑r : ℝ≥0∞), ∃ᶠ (a : ι) in f, y < (↑(u a) : ℝ≥0∞)
⊢ (↑r : ℝ≥0∞) ≤ (↑(limsup u f) : ℝ≥0∞) ↔ (↑r : ℝ≥0∞) ≤ limsup (fun (i : ι) ↦ (↑(u i) : ℝ≥0∞)) f

Tactic:
rw [coe_le_coe, le_limsup_iff, le_limsup_iff]

Premises used: Filter.le_limsup_iff, ENNReal.coe_le_coe
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0
hf : IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
r : ℝ≥0
⊢ (∀ y < r, ∃ᶠ (a : ι) in f, y < u a) ↔ ∀ y < (↑r : ℝ≥0∞), ∃ᶠ (a : ι) in f, y < (↑(u a) : ℝ≥0∞)

Tactic:
simp [forall_ennreal]

Premises used: ENNReal.forall_ennreal
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) f u
⊢ (↑(liminf u f) : ℝ≥0∞) = liminf (fun (i : ι) ↦ (↑(u i) : ℝ≥0∞)) f

Tactic:
eq_of_forall_nnreal_le_iff fun r ↦ ?_

Premises used: ENNReal.eq_of_forall_nnreal_le_iff
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) f u
refine : ∀ (r : ℝ≥0), (↑r : ℝ≥0∞) ≤ (↑(liminf u f) : ℝ≥0∞) ↔ (↑r : ℝ≥0∞) ≤ liminf (fun (i : ι) ↦ (↑(u i) : ℝ≥0∞)) f
⊢ (↑(liminf u f) : ℝ≥0∞) = liminf (fun (i : ι) ↦ (↑(u i) : ℝ≥0∞)) f

Tactic:
refine eq_of_forall_nnreal_le_iff fun r ↦ ?_

Premises used: ENNReal.eq_of_forall_nnreal_le_iff
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) f u
r : ℝ≥0
rw : (∀ y < r, ∀ᶠ (a : ι) in f, y < u a) ↔ ∀ y < (↑r : ℝ≥0∞), ∀ᶠ (a : ι) in f, y < (↑(u a) : ℝ≥0∞)
⊢ (↑r : ℝ≥0∞) ≤ (↑(liminf u f) : ℝ≥0∞) ↔ (↑r : ℝ≥0∞) ≤ liminf (fun (i : ι) ↦ (↑(u i) : ℝ≥0∞)) f

Tactic:
rw [coe_le_coe, le_liminf_iff, le_liminf_iff]

Premises used: ENNReal.coe_le_coe, Filter.le_liminf_iff
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) f u
r : ℝ≥0
⊢ (∀ y < r, ∀ᶠ (a : ι) in f, y < u a) ↔ ∀ y < (↑r : ℝ≥0∞), ∀ᶠ (a : ι) in f, y < (↑(u a) : ℝ≥0∞)

Tactic:
simp [forall_ennreal]

Premises used: ENNReal.forall_ennreal
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
⊢ ∀ (x : ι), f x ≤ (f + g) x

Tactic:
simp
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
refine : liminf (f + g) u ≤ liminf f u
⊢ liminf (f + g) u = liminf f u

Tactic:
refine le_antisymm ?_ <| liminf_le_liminf <| .of_forall <| by simp

Premises used: le_antisymm, Filter.liminf_le_liminf
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
⊢ IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) u (f + g)

Tactic:
isBoundedDefault
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
refine : ∀ (b : ℝ≥0∞) (hb : ∀ᶠ (n : ι) in u, b ≤ (f + g) n), b ≤ liminf f u
⊢ liminf (f + g) u ≤ liminf f u

Tactic:
refine liminf_le_of_le (by isBoundedDefault) fun b hb ↦ ?_

Premises used: Filter.liminf_le_of_le
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
b : ℝ≥0∞
hb : ∀ᶠ (n : ι) in u, b ≤ (f + g) n
rw : ∀ y < b, ∀ᶠ (a : ι) in u, y ≤ f a
⊢ b ≤ liminf f u

Tactic:
rw [Filter.le_liminf_iff']

Premises used: Filter.le_liminf_iff'
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
b : ℝ≥0∞
hb : ∀ᶠ (n : ι) in u, b ≤ (f + g) n
a : ℝ≥0∞
hab : a < b
h : ∀ (i : ι) (hfg : b ≤ (f + g) i) (hg : g i ≤ min (b - a) 1), a ≤ f i
⊢ ∀ᶠ (a_1 : ι) in u, a ≤ f a_1

Tactic:
filter_upwards [hb, ENNReal.tendsto_nhds_zero.1 hg _ <| lt_min (tsub_pos_of_lt hab) one_pos]
    with i hfg hg

Premises used: lt_min, Iff.mp, ENNReal.tendsto_nhds_zero, one_pos, tsub_pos_of_lt
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg_1 : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
b : ℝ≥0∞
hb : ∀ᶠ (n : ι) in u, b ≤ (f + g) n
a : ℝ≥0∞
hab : a < b
i : ι
hfg : b ≤ (f + g) i
hg : g i ≤ min (b - a) 1
⊢ min (b - a) 1 < ∞

Tactic:
simp
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg_1 : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
b : ℝ≥0∞
hb : ∀ᶠ (n : ι) in u, b ≤ (f + g) n
a : ℝ≥0∞
hab : a < b
i : ι
hfg : b ≤ (f + g) i
hg : g i ≤ min (b - a) 1
⊢ a ≤ f i

Tactic:
exact ENNReal.le_of_add_le_add_right (hg.trans_lt <| by simp).ne <|
    (add_le_of_le_tsub_left_of_le hab.le <| hg.trans <| min_le_left ..).trans hfg

Premises used: LT.lt.le, ENNReal.le_of_add_le_add_right, min_le_left, add_le_of_le_tsub_left_of_le, LE.le.trans, LE.le.trans_lt, LT.lt.ne
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
u : Filter ι
f : ι → ℝ≥0∞
hf : Tendsto f u (𝓝 0)
g : ι → ℝ≥0∞
rw : liminf (g + f) u = liminf g u
rw₁ rw₂ : liminf g u = liminf g u
⊢ liminf (f + g) u = liminf g u

Tactic:
rw [add_comm, liminf_add_of_right_tendsto_zero hf]

Premises used: add_comm, ENNReal.liminf_add_of_right_tendsto_zero
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
refine : limsup (f + g) u ≤ limsup f u
⊢ limsup (f + g) u = limsup f u

Tactic:
refine le_antisymm ?_ <| limsup_le_limsup <| .of_forall <| by simp

Premises used: le_antisymm, Filter.limsup_le_limsup
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
⊢ IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≤ x2) u f

Tactic:
isBoundedDefault
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
refine : ∀ (b : ℝ≥0∞) (hb : ∀ᶠ (n : ι) in u, f n ≤ b), limsup (f + g) u ≤ b
⊢ limsup (f + g) u ≤ limsup f u

Tactic:
refine le_limsup_of_le (by isBoundedDefault) fun b hb ↦ ?_

Premises used: Filter.le_limsup_of_le
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
b : ℝ≥0∞
hb : ∀ᶠ (n : ι) in u, f n ≤ b
rw : ∀ y > b, ∀ᶠ (a : ι) in u, (f + g) a ≤ y
⊢ limsup (f + g) u ≤ b

Tactic:
rw [Filter.limsup_le_iff']

Premises used: Filter.limsup_le_iff'
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
b : ℝ≥0∞
hb : ∀ᶠ (n : ι) in u, f n ≤ b
a : ℝ≥0∞
hba : a > b
h : ∀ (i : ι) (hf : f i ≤ b) (hg : g i ≤ a - b), (f + g) i ≤ a
⊢ ∀ᶠ (a_1 : ι) in u, (f + g) a_1 ≤ a

Tactic:
filter_upwards [hb, ENNReal.tendsto_nhds_zero.1 hg _ <| tsub_pos_of_lt hba] with i hf hg

Premises used: Iff.mp, ENNReal.tendsto_nhds_zero, tsub_pos_of_lt
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg_1 : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
b : ℝ≥0∞
hb : ∀ᶠ (n : ι) in u, f n ≤ b
a : ℝ≥0∞
hba : a > b
i : ι
hf : f i ≤ b
hg : g i ≤ a - b
⊢ f i + g i ≤ b + g i

Tactic:
gcongr
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg_1 : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
b : ℝ≥0∞
hb : ∀ᶠ (n : ι) in u, f n ≤ b
a : ℝ≥0∞
hba : a > b
i : ι
hf : f i ≤ b
hg : g i ≤ a - b
⊢ b + g i ≤ a

Tactic:
add_le_of_le_tsub_left_of_le hba.le hg

Premises used: LT.lt.le, add_le_of_le_tsub_left_of_le
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg_1 : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
b : ℝ≥0∞
hb : ∀ᶠ (n : ι) in u, f n ≤ b
a : ℝ≥0∞
hba : a > b
i : ι
hf : f i ≤ b
hg : g i ≤ a - b
calc : f i + g i ≤ b + g i
⊢ (f + g) i ≤ a

Tactic:
calc f i + g i
    _ ≤ b + g i := by gcongr
    _ ≤ a := add_le_of_le_tsub_left_of_le hba.le hg

Premises used: LT.lt.le, add_le_of_le_tsub_left_of_le
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
u : Filter ι
f : ι → ℝ≥0∞
hf : Tendsto f u (𝓝 0)
g : ι → ℝ≥0∞
rw : limsup (g + f) u = limsup g u
rw₁ rw₂ : limsup g u = limsup g u
⊢ limsup (f + g) u = limsup g u

Tactic:
rw [add_comm, limsup_add_of_right_tendsto_zero hf]

Premises used: add_comm, ENNReal.limsup_add_of_right_tendsto_zero
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_4
β : Type u_5
inst : PseudoEMetricSpace α
inst_1 : EMetricSpace β
inst_2 : CompleteSpace β
s : Set α
hs : Dense s
f : (↑s : Type u_4) → β
K : ℝ≥0
hf : LipschitzWith K f
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
    (hs.extend (s := s) f)

Tactic:
have : Continuous (hs.extend f) := (hs.uniformContinuous_extend hf.uniformContinuous).continuous
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_4
β : Type u_5
inst : PseudoEMetricSpace α
inst_1 : EMetricSpace β
inst_2 : CompleteSpace β
s : Set α
hs : Dense s
f : (↑s : Type u_4) → β
K : ℝ≥0
hf : LipschitzWith K f
this :
  Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
    (hs.extend (s := s) f)
⊢ Continuous[instTopologicalSpaceProd, _] fun (b : α × α) ↦ edist (hs.extend (s := s) f b.1) (hs.extend (s := s) f b.2)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_4
β : Type u_5
inst : PseudoEMetricSpace α
inst_1 : EMetricSpace β
inst_2 : CompleteSpace β
s : Set α
hs : Dense s
f : (↑s : Type u_4) → β
K : ℝ≥0
hf : LipschitzWith K f
this :
  Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
    (hs.extend (s := s) f)
apply : Continuous[instTopologicalSpaceProd, _] fun (b : α × α) ↦ (↑K : ℝ≥0∞) * edist b.1 b.2
⊢ IsClosed[instTopologicalSpaceProd]
    {p : α × α | edist (hs.extend (s := s) f p.1) (hs.extend (s := s) f p.2) ≤ (↑K : ℝ≥0∞) * edist p.1 p.2}

Tactic:
apply isClosed_le (by fun_prop)

Premises used: isClosed_le
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_4
β : Type u_5
inst : PseudoEMetricSpace α
inst_1 : EMetricSpace β
inst_2 : CompleteSpace β
s : Set α
hs : Dense s
f : (↑s : Type u_4) → β
K : ℝ≥0
hf : LipschitzWith K f
this :
  Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
    (hs.extend (s := s) f)
⊢ (↑K : ℝ≥0∞) ≠ ∞

Tactic:
simp