mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case coe.inr.inr
a : ℝ
a_pos : 0 < a
⊢ (↑(↑a).abs)⁻¹ = (↑a)⁻¹

Tactic:
]

Goal state after:
case coe.inr.inr
a : ℝ
a_pos : 0 < a
⊢ (↑(↑a).abs)⁻¹ = (↑a)⁻¹
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0
hf : Summable f
i i' : α
⊢ (if i' = i then 0 else f i') ≤ f i'

Tactic:
]

Goal state after:
α : Type u_1
f : α → ℝ≥0
hf : Summable f
i i' : α
⊢ (if i' = i then 0 else f i') ≤ f i'
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x : α
⊢ (∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝[univ] x, f x' ⊆ t) → f x ⊆ t) ↔
    ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝 x, f x' ⊆ t) → f x ⊆ t

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x : α
⊢ (∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝[univ] x, f x' ⊆ t) → f x ⊆ t) ↔
    ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝 x, f x' ⊆ t) → f x ⊆ t
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case coe.inl
a : ℝ
a_neg : a < 0
⊢ ↑a⁻¹ = ↑a⁻¹

Tactic:
]

Goal state after:
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case coe.inr.inr
a : ℝ
a_pos : 0 < a
⊢ ↑|a|⁻¹ = ↑a⁻¹

Tactic:
]

Goal state after:
case coe.inr.inr
a : ℝ
a_pos : 0 < a
⊢ ↑|a|⁻¹ = ↑a⁻¹
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x : α
s : Set α
⊢ (∀ (x_1 : Set β), (∃ᶠ (x' : α) in 𝓝[s] x, x_1ᶜ ∉ 𝓝ˢ (f x')) → x_1ᶜ ∉ 𝓝ˢ (f x)) ↔
    ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x : α
s : Set α
⊢ (∀ (x_1 : Set β), (∃ᶠ (x' : α) in 𝓝[s] x, x_1ᶜ ∉ 𝓝ˢ (f x')) → x_1ᶜ ∉ 𝓝ˢ (f x)) ↔
    ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case coe
a : ℝ
h : 0 ≤ ↑a
⊢ 0 ≤ a

Tactic:
]

Goal state after:
case coe
a : ℝ
h : 0 ≤ ↑a
⊢ 0 ≤ a
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case coe
a : ℝ
h : ↑a ≤ 0
⊢ a ≤ 0

Tactic:
]

Goal state after:
case coe
a : ℝ
h : ↑a ≤ 0
⊢ a ≤ 0
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
β : Type u_4
i : β → α
hi : Injective i
f : α → ℝ≥0
hf : Summable f
⊢ tsum ((fun i ↦ ↑(f i)) ∘ i) ≤ ∑' (i : α), ↑(f i)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_4
i : β → α
hi : Injective i
f : α → ℝ≥0
hf : Summable f
⊢ tsum ((fun i ↦ ↑(f i)) ∘ i) ≤ ∑' (i : α), ↑(f i)
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a : ℝ
h : 0 < ↑a
h' : ↑a ≠ ⊤
⊢ 0 < ↑a⁻¹

Tactic:
]

Goal state after:
a : ℝ
h : 0 < ↑a
h' : ↑a ≠ ⊤
⊢ 0 < ↑a⁻¹
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x : α
⊢ (∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝[univ] x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty) ↔
    ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝 x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x : α
⊢ (∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝[univ] x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty) ↔
    ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝 x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a : ℝ
h : ↑a < 0
h' : ↑a ≠ ⊥
⊢ ↑a⁻¹ < 0

Tactic:
]

Goal state after:
a : ℝ
h : ↑a < 0
h' : ↑a ≠ ⊥
⊢ ↑a⁻¹ < 0
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
hf : HasOpenCGraph f
hg : HasOpenCGraph g
this : {x | x.2 ∈ f x.1 ∩ g x.1} = {x | x.2 ∈ f x.1} ∩ {x | x.2 ∈ g x.1}
⊢ IsOpen[instTopologicalSpaceProd] ({x | x.2 ∈ f x.1} ∩ {x | x.2 ∈ g x.1})

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
hf : HasOpenCGraph f
hg : HasOpenCGraph g
this : {x | x.2 ∈ f x.1 ∩ g x.1} = {x | x.2 ∈ f x.1} ∩ {x | x.2 ∈ g x.1}
⊢ IsOpen[instTopologicalSpaceProd] ({x | x.2 ∈ f x.1} ∩ {x | x.2 ∈ g x.1})
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: ⊢ StrictAntiOn (fun x ↦ x⁻¹) (Ioi 0)

Tactic:
intro a a_0 b b_0 a_b

Goal state after:
a : EReal
a_0 : a ∈ Ioi 0
b : EReal
b_0 : b ∈ Ioi 0
a_b : a < b
⊢ (fun x ↦ x⁻¹) b < (fun x ↦ x⁻¹) a
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: β : Type u_2
f : β → ℝ≥0
hf : Summable f
g : β → ℝ≥0
hgf : ∀ (b : β), (fun i ↦ ↑(g i)) b ≤ (fun i ↦ ↑(f i)) b
⊢ Summable g

Tactic:
]

Goal state after:
β : Type u_2
f : β → ℝ≥0
hf : Summable f
g : β → ℝ≥0
hgf : ∀ (b : β), (fun i ↦ ↑(g i)) b ≤ (fun i ↦ ↑(f i)) b
⊢ Summable g
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: b✝ : EReal
a : ℝ
a_0 : 0 < ↑a
b : ℝ
b_0 : 0 < ↑b
a_b : ↑a < ↑b
⊢ b⁻¹ < a⁻¹

Tactic:
]

Goal state after:
b✝ : EReal
a : ℝ
a_0 : 0 < ↑a
b : ℝ
b_0 : 0 < ↑b
a_b : ↑a < ↑b
⊢ b⁻¹ < a⁻¹
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: m n : ℕ
⊢ ↑(m / n) ≤ ↑m / ↑n

Tactic:
]

Goal state after:
m n : ℕ
⊢ ↑(m / n) ≤ ↑m / ↑n
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a : EReal
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a : EReal
⊢ a / 0 = 0

Tactic:
change a * 0⁻¹ = 0
  rw [inv_zero, mul_zero a]

Goal state after:
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a : EReal
h₁ : a ≠ ⊥
h₂ : a ≠ ⊤
h₃ : ↑a.toReal ≠ 0
⊢ ↑a.toReal / ↑a.toReal = 1

Tactic:
]

Goal state after:
a : EReal
h₁ : a ≠ ⊥
h₂ : a ≠ ⊤
h₃ : ↑a.toReal ≠ 0
⊢ ↑a.toReal / ↑a.toReal = 1
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a : EReal
h₁ : a ≠ ⊥
h₂ : a ≠ ⊤
h₃ : ↑a.toReal ≠ 0
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
⊢ a * (b * c⁻¹) = a * (b * c⁻¹)

Tactic:
]

Goal state after:
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
⊢ a * c / b = a * c / b

Tactic:
]

Goal state after:
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
⊢ b * (a / c) = b * (a / c)

Tactic:
]

Goal state after:
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
⊢ a * (b⁻¹ * c⁻¹) = a * (b⁻¹ * c⁻¹)

Tactic:
]

Goal state after:
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c d : EReal
⊢ c / d * (a / b) = c / d * (a / b)

Tactic:
]

Goal state after:
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b : EReal
h₁ : b ≠ ⊥
h₂ : b ≠ ⊤
h₃ : b ≠ 0
⊢ a = a

Tactic:
]

Goal state after:
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
h₁ : c ≠ ⊥
h₂ : c ≠ ⊤
h₃ : c ≠ 0
⊢ a / b = a / b

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
f : α → ℝ
hf : Summable f
⊢ Summable fun i ↦ (f i).toNNReal

Tactic:
]

Goal state after:
α : Type u_1
f : α → ℝ
hf : Summable f
⊢ Summable fun i ↦ (f i).toNNReal
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case refine_1
a b c : EReal
hbot : b ≠ ⊥
htop : b ≠ ⊤
hzero : b ≠ 0
h : c / b = a
⊢ b * a = b * a

Tactic:
]

Goal state after:
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case refine_2
a b c : EReal
hbot : b ≠ ⊥
htop : b ≠ ⊤
hzero : b ≠ 0
h : c = a * b
⊢ a = a

Tactic:
]

Goal state after:
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: b : EReal
h : 0 < b
h' : b ≠ ⊤
a a' : EReal
a_lt_a' : a < a'
hyp : a / b = a' / b
⊢ a' = a'

Tactic:
]

Goal state after:
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
⊢ a * (-b)⁻¹ ≤ a' * (-b)⁻¹

Tactic:
]

Goal state after:
b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
⊢ a * (-b)⁻¹ ≤ a' * (-b)⁻¹
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: b : EReal
h : b < 0
h' : b ≠ ⊥
a a' : EReal
a_lt_a' : a < a'
hyp : a' / b = a / b
⊢ a' = a'

Tactic:
]

Goal state after:
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
h : b > 0
h' : b ≠ ⊤
⊢ b * (a / b) ≤ c / b ↔ a * b ≤ c

Tactic:
]

Goal state after:
a b c : EReal
h : b > 0
h' : b ≠ ⊤
⊢ b * (a / b) ≤ c / b ↔ a * b ≤ c
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
h : b > 0
h' : b ≠ ⊤
⊢ b * a / b ≤ c / b ↔ b * a ≤ c

Tactic:
]

Goal state after:
a b c : EReal
h : b > 0
h' : b ≠ ⊤
⊢ b * a / b ≤ c / b ↔ b * a ≤ c
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ a / b ≤ b * (c / b) ↔ a ≤ b * c

Tactic:
]

Goal state after:
a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ a / b ≤ b * (c / b) ↔ a ≤ b * c
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ a / b ≤ c * b / b ↔ a ≤ c * b

Tactic:
]

Goal state after:
a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ a / b ≤ c * b / b ↔ a ≤ c * b
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → β
inst✝ : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
x✝² : Nonempty α
x✝¹ : Nonempty ↑s
φ : β → Filter α := fun b ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
this✝ : ℱ.NeBot
hℱs : ℱ ≤ 𝓟 s
hℱ : ∀ x ∈ s, ∀ᶠ (y : α) in ℱ, f y ≤ f x
a : α
ha : a ∈ s
h : ClusterPt a ℱ
x : α
hx : x ∈ s
hxa : f x < f a
x✝ : (𝓝 a ⊓ ℱ).NeBot := h
this : False
⊢ False

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → β
inst✝ : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
x✝² : Nonempty α
x✝¹ : Nonempty ↑s
φ : β → Filter α := fun b ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
this✝ : ℱ.NeBot
hℱs : ℱ ≤ 𝓟 s
hℱ : ∀ x ∈ s, ∀ᶠ (y : α) in ℱ, f y ≤ f x
a : α
ha : a ∈ s
h : ClusterPt a ℱ
x : α
hx : x ∈ s
hxa : f x < f a
x✝ : (𝓝 a ⊓ ℱ).NeBot := h
this : False
⊢ False
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ b * (a / b) < c / b ↔ a * b < c

Tactic:
]

Goal state after:
a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ b * (a / b) < c / b ↔ a * b < c
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ b * a / b < c / b ↔ b * a < c

Tactic:
]

Goal state after:
a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ b * a / b < c / b ↔ b * a < c
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
h : 0 < c
h' : c ≠ ⊤
⊢ b / c < c * (a / c) ↔ b < a * c

Tactic:
]

Goal state after:
a b c : EReal
h : 0 < c
h' : c ≠ ⊤
⊢ b / c < c * (a / c) ↔ b < a * c
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
h : 0 < c
h' : c ≠ ⊤
⊢ b / c < c * a / c ↔ b < c * a

Tactic:
]

Goal state after:
a b c : EReal
h : 0 < c
h' : c ≠ ⊤
⊢ b / c < c * a / c ↔ b < c * a
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case inl.inl
c : EReal
hc : 0 ≤ c
ha : 0 ≤ 0
h : c < 0
⊢ ∃ a' ∈ Ioo 0 0, c < a' * ⊤

Tactic:
]

Goal state after:
case inl.inl
c : EReal
hc : 0 ≤ c
ha : 0 ≤ 0
h : c < 0
⊢ ∃ a' ∈ Ioo 0 0, c < a' * ⊤
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case right
a c : EReal
ha✝ : 0 ≤ a
hc : 0 ≤ c
h : c < ⊤
ha : 0 < a
a' : EReal
a0' : 0 < a'
aa' : a' < a
⊢ c < a' * ⊤

Tactic:
]

Goal state after:
case right
a c : EReal
ha✝ : 0 ≤ a
hc : 0 ≤ c
h : c < ⊤
ha : 0 < a
a' : EReal
a0' : 0 < a'
aa' : a' < a
⊢ c < a' * ⊤
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case right
a c : EReal
ha✝ : 0 ≤ a
hc : 0 ≤ c
h : c < ⊤
ha : 0 < a
a' : EReal
a0' : 0 < a'
aa' : a' < a
⊢ c < ⊤

Tactic:
]

Goal state after:
case right
a c : EReal
ha✝ : 0 ≤ a
hc : 0 ≤ c
h : c < ⊤
ha : 0 < a
a' : EReal
a0' : 0 < a'
aa' : a' < a
⊢ c < ⊤
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n ↦ ∑ x ∈ Finset.range n, d x
N n : ℕ
hN :
  ∑ k ∈ Finset.Ico N n, d k < ε ∧
    ∑ x ∈ Finset.range N, d x - (∑ k ∈ Finset.range N, d k + ∑ k ∈ Finset.Ico N n, d k) < ε
hn : N ≤ n
⊢ edist (f n) (f N) < ↑ε

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n ↦ ∑ x ∈ Finset.range n, d x
N n : ℕ
hN :
  ∑ k ∈ Finset.Ico N n, d k < ε ∧
    ∑ x ∈ Finset.range N, d x - (∑ k ∈ Finset.range N, d k + ∑ k ∈ Finset.Ico N n, d k) < ε
hn : N ≤ n
⊢ edist (f n) (f N) < ↑ε
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n ↦ ∑ x ∈ Finset.range n, d x
N n : ℕ
hN :
  ∑ k ∈ Finset.Ico N n, d k < ε ∧
    ∑ x ∈ Finset.range N, d x - (∑ k ∈ Finset.range N, d k + ∑ k ∈ Finset.Ico N n, d k) < ε
hn : N ≤ n
⊢ edist (f N) (f n) < ↑ε

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n ↦ ∑ x ∈ Finset.range n, d x
N n : ℕ
hN :
  ∑ k ∈ Finset.Ico N n, d k < ε ∧
    ∑ x ∈ Finset.range N, d x - (∑ k ∈ Finset.range N, d k + ∑ k ∈ Finset.Ico N n, d k) < ε
hn : N ≤ n
⊢ edist (f N) (f n) < ↑ε
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case inl
b c : EReal
h₁ : ⊤ ≠ 0 ∨ b ≠ ⊤
h₂ : 0 < b
hc : ⊤ * b < c
⊢ ∃ a' ∈ Ioo ⊤ ⊤, a' * b < c

Tactic:
]

Goal state after:
case inl
b c : EReal
h₁ : ⊤ ≠ 0 ∨ b ≠ ⊤
h₂ : 0 < b
hc : ⊤ * b < c
⊢ ∃ a' ∈ Ioo ⊤ ⊤, a' * b < c
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ (fun i ↦ ↑(d i)) n
hd : Summable d
⊢ CauchySeq f

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ (fun i ↦ ↑(d i)) n
hd : Summable d
⊢ CauchySeq f
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case inl
b c : EReal
h₁ : ⊤ ≠ 0 ∨ b ≠ ⊤
h₂ : 0 < b
hc : ⊤ < c
⊢ ∃ a' ∈ Ioo ⊤ ⊤, a' * b < c

Tactic:
]

Goal state after:
case inl
b c : EReal
h₁ : ⊤ ≠ 0 ∨ b ≠ ⊤
h₂ : 0 < b
hc : ⊤ < c
⊢ ∃ a' ∈ Ioo ⊤ ⊤, a' * b < c
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: ⊢ (Ioo ⊥ ⊤).OrdConnected

Tactic:
]

Goal state after:
⊢ (Ioo ⊥ ⊤).OrdConnected
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : n ≤ m
⊢ ∑ k ∈ Finset.range (m - n), d (n + k) ≤ ∑' (m : ℕ), d (n + m)

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : n ≤ m
⊢ ∑ k ∈ Finset.range (m - n), d (n + k) ≤ ∑' (m : ℕ), d (n + m)
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: a : ℝ
ha : ↑a ≠ ⊤
h'a : ↑a ≠ ⊥
⊢ Tendsto (toReal ∘ Real.toEReal) (𝓝 a) (𝓝 (↑a).toReal)

Tactic:
]

Goal state after:
a : ℝ
ha : ↑a ≠ ⊤
h'a : ↑a ≠ ⊥
⊢ Tendsto (toReal ∘ Real.toEReal) (𝓝 a) (𝓝 (↑a).toReal)
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: ⊢ (Ici 0).OrdConnected

Tactic:
]

Goal state after:
⊢ (Ici 0).OrdConnected
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: ⊢ IsClosed (Ici 0)

Tactic:
]

Goal state after:
⊢ IsClosed (Ici 0)
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: case inr
α : Type u_4
s : Set α
hinf : s.Infinite
this : Infinite ↑s
⊢ ∞ = ∞

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_4
⊢ ∑' (x : ↑univ), 1 = ↑(ENat.card α)

Tactic:
]

Goal state after:
α : Type u_4
⊢ ∑' (x : ↑univ), 1 = ↑(ENat.card α)
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_4
c : ℝ≥0∞
⊢ ∑' (x : ↑univ), c = ↑(ENat.card α) * c

Tactic:
]

Goal state after:
α : Type u_4
c : ℝ≥0∞
⊢ ∑' (x : ↑univ), c = ↑(ENat.card α) * c
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case inr.inr.inl.inl
a c : EReal
a_top : a < ⊤
h₁ : a ≠ 0 ∨ ⊤ ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < ⊤
hc : ⊥ < c
b0 : 0 < ⊤
a0 : a < 0
a' : EReal
aa' : a < a'
a0' : a' < 0
⊢ ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c

Tactic:
]

Goal state after:
case inr.inr.inl.inl
a c : EReal
a_top : a < ⊤
h₁ : a ≠ 0 ∨ ⊤ ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < ⊤
hc : ⊥ < c
b0 : 0 < ⊤
a0 : a < 0
a' : EReal
aa' : a < a'
a0' : a' < 0
⊢ ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case inr.inr.inl.inr.inl
c : EReal
b0 : 0 < ⊤
a_top : 0 < ⊤
h₁ : False
h₂ : 0 ≠ ⊤ ∨ 0 < ⊤
hc : 0 * ⊤ < c
⊢ ∃ a' ∈ Ioo 0 ⊤, a' * ⊤ < c

Tactic:
]

Goal state after:
case inr.inr.inl.inr.inl
c : EReal
b0 : 0 < ⊤
a_top : 0 < ⊤
h₁ : False
h₂ : 0 ≠ ⊤ ∨ 0 < ⊤
hc : 0 * ⊤ < c
⊢ ∃ a' ∈ Ioo 0 ⊤, a' * ⊤ < c
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case inr.inr.inl.inr.inr
a c : EReal
a_top : a < ⊤
h₁ : a ≠ 0 ∨ ⊤ ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < ⊤
hc : ⊤ < c
b0 : 0 < ⊤
a0 : 0 < a
⊢ ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c

Tactic:
]

Goal state after:
case inr.inr.inl.inr.inr
a c : EReal
a_top : a < ⊤
h₁ : a ≠ 0 ∨ ⊤ ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < ⊤
hc : ⊤ < c
b0 : 0 < ⊤
a0 : 0 < a
⊢ ∃ a' ∈ Ioo a ⊤, a' * ⊤ < c
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
γ : Type u_4
inst✝ : LinearOrder γ
f : α → γ
⊢ (∀ (y : γ), IsOpen[inst✝¹] (f ⁻¹' Ioi y)) ↔ ∀ (y : γ), IsClosed[inst✝¹] (f ⁻¹' Iic y)

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
γ : Type u_4
inst✝ : LinearOrder γ
f : α → γ
⊢ (∀ (y : γ), IsOpen[inst✝¹] (f ⁻¹' Ioi y)) ↔ ∀ (y : γ), IsClosed[inst✝¹] (f ⁻¹' Iic y)
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
x : α
γ : Type u_4
inst✝ : CompleteLinearOrder γ
f : α → γ
⊢ f x ≤ liminf f (𝓝[univ] x) ↔ f x ≤ liminf f (𝓝[univ] x)

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
γ : Type u_4
inst✝ : LinearOrder γ
f : α → γ
hfs : ∀ (b : γ), ∃ v, IsClosed[inst✝¹] v ∧ s ∩ f ⁻¹' Iic b = s ∩ v
ks : IsCompact s
c : γ
⊢ IsCompact (s ∩ f ⁻¹' Iic c)

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
γ : Type u_4
inst✝ : LinearOrder γ
f : α → γ
hfs : ∀ (b : γ), ∃ v, IsClosed[inst✝¹] v ∧ s ∩ f ⁻¹' Iic b = s ∩ v
ks : IsCompact s
c : γ
⊢ IsCompact (s ∩ f ⁻¹' Iic c)
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
γ : Type u_4
inst✝ : LinearOrder γ
ι : Type u_5
f : ι → α → γ
ks : IsCompact s
I : Set ι
c : γ
hfi : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
x✝ : ∃ u, ∀ x ∈ s, ∃ i ∈ u, c < f (↑i) x
u : Finset ↑I
hu : ∀ x ∈ s, ∃ i ∈ u, c < f (↑i) x
⊢ ∀ (x : α), x ∉ s ∩ ⋂ i ∈ I, f i ⁻¹' Iic c

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
γ : Type u_4
inst✝ : LinearOrder γ
ι : Type u_5
f : ι → α → γ
ks : IsCompact s
I : Set ι
c : γ
hfi : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
x✝ : ∃ u, ∀ x ∈ s, ∃ i ∈ u, c < f (↑i) x
u : Finset ↑I
hu : ∀ x ∈ s, ∃ i ∈ u, c < f (↑i) x
⊢ ∀ (x : α), x ∉ s ∩ ⋂ i ∈ I, f i ⁻¹' Iic c
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_1
f : α → ℝ
l : Filter α
⊢ (∀ (x : ℝ), ∀ᶠ (a : α) in l, ↑x < ↑(f a)) ↔ ∀ (i : ℝ), True → ∀ᶠ (x : α) in l, f x ∈ Ioi i

Tactic:
]

Goal state after:
α : Type u_1
f : α → ℝ
l : Filter α
⊢ (∀ (x : ℝ), ∀ᶠ (a : α) in l, ↑x < ↑(f a)) ↔ ∀ (i : ℝ), True → ∀ᶠ (x : α) in l, f x ∈ Ioi i
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_1
f : α → ℝ
l : Filter α
⊢ (∀ (x : ℝ), ∀ᶠ (a : α) in l, ↑(f a) < ↑x) ↔ ∀ (i : ℝ), True → ∀ᶠ (x : α) in l, f x ∈ Iio i

Tactic:
]

Goal state after:
α : Type u_1
f : α → ℝ
l : Filter α
⊢ (∀ (x : ℝ), ∀ᶠ (a : α) in l, ↑(f a) < ↑x) ↔ ∀ (i : ℝ), True → ∀ᶠ (x : α) in l, f x ∈ Iio i
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : Set α → ℝ≥0∞ := fun s ↦ ⨅ f, ⨅ (_ : s ⊆ ⋃ i, f i), ∑' (i : ℕ), m (f i)
⊢ μ ∅ ≤ 0

Tactic:
]

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : Set α → ℝ≥0∞ := fun s ↦ ⨅ f, ⨅ (_ : s ⊆ ⋃ i, f i), ∑' (i : ℕ), m (f i)
⊢ μ ∅ ≤ 0
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : Set α → ℝ≥0∞ := fun s ↦ ⨅ f, ⨅ (_ : s ⊆ ⋃ i, f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : ∑' (i : ℕ), μ (s i) < ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), ↑(ε' i) < ↑ε
⊢ μ (⋃ i, s i) ≤ ∑' (i : ℕ), μ (s i) + ∑' (i : ℕ), ↑(ε' i)

Tactic:
]

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : Set α → ℝ≥0∞ := fun s ↦ ⨅ f, ⨅ (_ : s ⊆ ⋃ i, f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : ∑' (i : ℕ), μ (s i) < ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), ↑(ε' i) < ↑ε
⊢ μ (⋃ i, s i) ≤ ∑' (i : ℕ), μ (s i) + ∑' (i : ℕ), ↑(ε' i)
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : Set α → ℝ≥0∞ := fun s ↦ ⨅ f, ⨅ (_ : s ⊆ ⋃ i, f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : ∑' (i : ℕ), μ (s i) < ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), ↑(ε' i) < ↑ε
⊢ μ (⋃ i, s i) ≤ ∑' (a : ℕ), (μ (s a) + ↑(ε' a))

Tactic:
]

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : Set α → ℝ≥0∞ := fun s ↦ ⨅ f, ⨅ (_ : s ⊆ ⋃ i, f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : ∑' (i : ℕ), μ (s i) < ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), ↑(ε' i) < ↑ε
⊢ μ (⋃ i, s i) ≤ ∑' (a : ℕ), (μ (s a) + ↑(ε' a))
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: ⊢ Tendsto (toReal ∘ Real.toEReal) atTop atTop

Tactic:
]

Goal state after:
⊢ Tendsto (toReal ∘ Real.toEReal) atTop atTop
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: ⊢ Tendsto (toReal ∘ Real.toEReal) atBot atBot

Tactic:
]

Goal state after:
⊢ Tendsto (toReal ∘ Real.toEReal) atBot atBot
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case pos
x✝ : EReal
h_top : ¬x✝ = ⊤
x : EReal
hx : x ∈ {⊤}ᶜ
h_bot : x = ⊥
⊢ ∃ i, True ∧ ∀ ⦃x : EReal⦄, x ∈ Iio ↑i → ENNReal.ofReal x.toReal = (fun x ↦ ENNReal.ofReal x.toReal) ⊥

Tactic:
]

Goal state after:
case pos
x✝ : EReal
h_top : ¬x✝ = ⊤
x : EReal
hx : x ∈ {⊤}ᶜ
h_bot : x = ⊥
⊢ ∃ i, True ∧ ∀ ⦃x : EReal⦄, x ∈ Iio ↑i → ENNReal.ofReal x.toReal = (fun x ↦ ENNReal.ofReal x.toReal) ⊥
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case mp
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : 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

Tactic:
⟨x, y⟩

Goal state after:
case mp
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
hf : ∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x
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
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
⊢ liminf u f + liminf v f ≤ liminf (u + v) f

Tactic:
by
  refine add_le_of_forall_lt fun a a_u b b_v ↦ (le_liminf_iff).2 fun c c_ab ↦ ?_
  filter_upwards [eventually_lt_of_lt_liminf a_u, eventually_lt_of_lt_liminf b_v] with x a_x b_x
  exact c_ab.trans (add_lt_add a_x b_x)

Goal state after: