mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f = ⊥
h' : limsup v f ≠ ⊤
⊢ limsup (u + v) f = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: C : EReal
h : C ≠ ⊥
h' : C ≠ ⊤
⊢ (fun n ↦ C / ↑n) = fun n ↦ ↑(C.toReal / ↑n)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: C : EReal
h : C ≠ ⊥
h' : C ≠ ⊤
⊢ Tendsto (fun n ↦ C / ↑n) atTop (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: 𝕜 : Type u_4
inst✝³ : DivisionSemiring 𝕜
inst✝² : CharZero 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : ContinuousSMul ℚ≥0 𝕜
this : Tendsto (fun n ↦ 1 / ↑(n + 1)) atTop (𝓝 0)
⊢ Tendsto (fun n ↦ 1 / (↑n + 1)) atTop (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
a b : EReal
ha : limsup u f < a
hb : limsup v f ≤ b
⊢ limsup (u + v) f ≤ a + b

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
h : liminf u f = ⊤
h' : liminf v f ≠ ⊥
⊢ liminf (u + v) f = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: 𝕜 : Type u_4
A : Type u_5
inst✝⁷ : Semifield 𝕜
inst✝⁶ : CharZero 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : ContinuousSMul ℚ≥0 𝕜
inst✝³ : Semiring A
inst✝² : Algebra 𝕜 A
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousSMul 𝕜 A
⊢ Tendsto (⇑(algebraMap 𝕜 A) ∘ fun n ↦ (↑n)⁻¹) atTop (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
⊢ 0 < ?m.77

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
⊢ c ≠ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
⊢ 0 < ?m.121

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
⊢ limsup (fun x ↦ c * u x) f = c * limsup u f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁵ : DivisionSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
x : 𝕜
⊢ 𝓝 1 = 𝓝 (1 / (1 + x * 0))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
⊢ LowerSemicontinuousOn f s ↔ IsClosed[instTopologicalSpaceProd] {p | p.1 ∈ s ∧ f p.1 ≤ p.2}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : c ≤ 0
h₂ : c ≠ ⊥
⊢ 0 ≤ -c

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : c ≤ 0
h₂ : c ≠ ⊥
⊢ -c ≠ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : c ≤ 0
h₂ : c ≠ ⊥
⊢ limsup (fun x ↦ c * u x) f = c * liminf u f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
⊢ LowerSemicontinuous f ↔ IsClosed[instTopologicalSpaceProd] {p | f p.1 ≤ p.2}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
⊢ 0 ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
⊢ c ≠ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
⊢ liminf (fun x ↦ c * u x) f = c * liminf u f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁵ : DivisionSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
x : 𝕜
this : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
⊢ 1 + x * 0 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : c ≤ 0
h₂ : c ≠ ⊥
⊢ liminf (fun x ↦ c * u x) f = c * limsup u f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁵ : DivisionSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
x : 𝕜
⊢ Tendsto (fun n ↦ ↑n / (↑n + x)) atTop (𝓝 1)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝⁶ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_5
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : (g ∘ f) x > y
h : ∃ l, l < f x
z : γ
zlt : z < f x
hz : Ioc z (f x) ⊆ g ⁻¹' Ioi y
a : α
ha : f a > z
⊢ min (f x) (f a) ∈ Ioc z (f x)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
⊢ limsup u f * liminf v f ≤ limsup (u * v) f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝⁶ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_5
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
⊢ LowerSemicontinuousWithinAt (g ∘ f) s x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝⁶ : TopologicalSpace α
x : α
γ : Type u_4
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_5
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousAt f x
gmon : Monotone g
⊢ LowerSemicontinuousAt (g ∘ f) x

Tactic:
by

Goal state after:
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), 0 < ε → ∑' (i : ℕ), μ (s i) < ∞ → μ (⋃ i, s i) ≤ ∑' (i : ℕ), μ (s i) + ↑ε

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
t : ℕ → Set α
x✝ : ∀ (i : ℕ), P (t i)
h : s ⊆ ⋃ i, t i
⊢ s ⊆ iUnion t

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h₁ : limsup u f ≠ 0 ∨ limsup v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ limsup v f ≠ 0
⊢ limsup (u * v) f ≤ limsup u f * limsup v f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁵ : Semifield 𝕜
inst✝⁴ : CharZero 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ Tendsto (fun k ↦ (a + c * ↑k) / (b + d * ↑k)) atTop (𝓝 (c / d))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: m : ℕ
hm : 0 < m
⊢ ∀ᶠ (n : ℕ) in atTop, 0 ≤ (fun n ↦ ↑(n % m)) n

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
⊢ liminf u f * liminf v f ≤ liminf (u * v) f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
inst✝ : f.NeBot
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h₁ : limsup u f ≠ 0 ∨ liminf v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ liminf v f ≠ 0
⊢ 0 < limsup u f ∨ liminf v f ≠ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: m : ℕ
hm : 0 < m
⊢ Tendsto (fun n ↦ ↑(n % m) / ↑n) atTop (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
inst✝ : f.NeBot
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h₂ : limsup u f ≠ ⊤ ∨ liminf v f ≠ 0
h₁ : 0 < limsup u f ∨ liminf v f ≠ ⊤
⊢ limsup u f ≠ ⊤ ∨ 0 < liminf v f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: a c : ℝ
ha : a ≠ 0
⊢ Tendsto (fun x ↦ (a * x + c)⁻¹) atTop (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
inst✝ : f.NeBot
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h₁ : limsup u f ≠ 0 ∨ liminf v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ liminf v f ≠ 0
⊢ liminf (u * v) f ≤ limsup u f * liminf v f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: a b : ℝ
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (↑a, ↑b)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: α : Type u_4
G : Type u_5
inst✝ : GroupWithZero G
f g : α → G
l : Filter α
hg : Tendsto g l (𝓟 {0}ᶜ)
⊢ (fun x ↦ f x / g x * g x) =ᶠ[l] fun x ↦ f x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: a : ℝ
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊤, ↑a)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: a : ℝ
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (↑a, ⊤)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: ⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊤, ⊤)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: α : Type u_4
K : Type u_5
inst✝² : DivisionSemiring K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f g : α → K
l : Filter α
hg : Tendsto g l atTop
⊢ Set.Ioi 0 ⊆ {0}ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: a : ℝ
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊥, ↑a)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: a : ℝ
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (↑a, ⊥)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: ⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊥, ⊥)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: α : Type u_4
K : Type u_5
inst✝⁵ : Field K
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : TopologicalSpace K
inst✝¹ : OrderTopology K
inst✝ : ContinuousInv K
f g : α → K
l : Filter α
hf : Tendsto f l atTop
a : K
ha : 0 < a
hlim : Tendsto (fun x ↦ f x / g x) l (𝓝 a)
⊢ Tendsto (fun x ↦ g x / f x) l (𝓝 a⁻¹)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : Semiring α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : ExistsAddOfLE α
inst✝ : Archimedean α
r : α
h : 1 < r
⊢ Tendsto (fun n ↦ r ^ n) atTop atTop

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁶ : Semifield 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : ExistsAddOfLE 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h₁ : 0 ≤ r
h₂ : r < 1
hr : 0 = r
⊢ Tendsto (fun n ↦ r ^ (n + 1)) atTop (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁶ : Semifield 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : ExistsAddOfLE 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h₁ : 0 ≤ r
h₂ : r < 1
hr : 0 < r
this : Tendsto (fun n ↦ r⁻¹ ^ n) atTop atTop
n : ℕ
⊢ ((fun r ↦ r⁻¹) ∘ fun n ↦ r⁻¹ ^ n) n = r ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : Tendsto (abs ∘ fun n ↦ r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : 1 = |r|
⊢ Tendsto (fun n ↦ |r| ^ n) atTop (𝓝 0)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (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✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₁z : f z > z₁
h₂z : g z > z₂
⊢ min (f z) (f x) ∈ u

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
⊢ Tendsto (fun n ↦ r ^ n) atTop (𝓝 0) ↔ |r| < 1

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
⊢ (OuterMeasure.ofFunction m m_empty) s = ⨅ t, ⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ i, t i), ∑' (i : ℕ), m (t i)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
hn : 0 < n
h : ∀ k < n, c * u k < u (k + 1)
⊢ c ^ n * u 0 < u n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
h : ∀ k < n, c * u k ≤ u (k + 1)
⊢ c ^ n * u 0 ≤ u n

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
f : ℕ → Set α := fun i ↦ Nat.casesOn i s fun x ↦ ∅
⊢ ∀ (b' : ℕ), b' ≠ 0 → m (f b') = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
hn : 0 < n
h : ∀ k < n, u (k + 1) < c * u k
⊢ u n < c ^ n * u 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
h : ∀ k < n, u (k + 1) ≤ c * u k
⊢ u n ≤ c ^ n * u 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: r : ℝ≥0
hr : r < 1
⊢ Tendsto (fun a ↦ ↑(r ^ a)) atTop (𝓝 ↑0)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: r : ℝ≥0
h : Tendsto (fun n ↦ r ^ n) atTop (𝓝 0)
⊢ r < 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: r : ℝ≥0∞
hr : r < 1
⊢ Tendsto (fun n ↦ r ^ n) atTop (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: r : ℝ≥0∞
⊢ Tendsto (fun n ↦ r ^ n) atTop (𝓝 0) ↔ r < 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: r : ℝ≥0∞
⊢ Tendsto (fun n ↦ r ^ n) atTop (𝓝 ∞) ↔ 1 < r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: x r : ℝ≥0∞
ε : ℝ≥0
hr : r < 1
h : ∀ (n : ℕ), x ≤ ↑ε * r ^ n
⊢ x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: r : ℝ
h₁ : 0 ≤ r
h₂ : r < 1
this✝ : r ≠ 1
this : Tendsto (fun n ↦ (r ^ n - 1) * (r - 1)⁻¹) atTop (𝓝 ((0 - 1) * (r - 1)⁻¹))
⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, r ^ i) atTop (𝓝 (1 - r)⁻¹)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: ⊢ HasSum (fun n ↦ (1 / 2) ^ n) 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: n : ℕ
⊢ ∀ (i : ℕ), 0 ≤ (1 / 2) ^ i

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: n : ℕ
⊢ ∑ i ∈ Finset.range n, (1 / 2) ^ i ≤ 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: n : ℕ
⊢ Summable fun i ↦ if n ≤ i then 2⁻¹ ^ i else 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (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✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₁z : f z > z₁
h₂z : g z > z₂
A1 : min (f z) (f x) ∈ u
⊢ min (g z) (g x) ∈ v

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: n : ℕ
⊢ (∑' (i : ℕ), if n ≤ i then 2⁻¹ ^ i else 0) = 2 * 2⁻¹ ^ n

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ∞
⊢ (OuterMeasure.ofFunction m m_empty) (s ∪ t) =
    (OuterMeasure.ofFunction m m_empty) s + (OuterMeasure.ofFunction m m_empty) t

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type ?u.23
f : β → α
h : Monotone m ∨ Surjective f
⊢ m (f '' ∅) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: a : ℝ
⊢ HasSum (fun n ↦ a / 2 / 2 ^ n) a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: r : ℝ≥0
hr : r < 1
⊢ HasSum (fun n ↦ r ^ n) (1 - r)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: p : EReal × EReal
h : p.1 ≠ ⊤ ∨ p.2 ≠ ⊥
h' : p.1 ≠ ⊥ ∨ p.2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) p

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: r : ℝ≥0∞
hr : 1 ≤ r
a : ℝ≥0∞
ha : a < ∞
n : ℕ
hn : a < ↑n
⊢ ↑n = ∑ i ∈ Finset.range n, 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: r : ℝ≥0∞
hr : 1 ≤ r
a : ℝ≥0∞
ha : a < ∞
n : ℕ
hn : a < ↑n
⊢ ∑ i ∈ Finset.range n, 1 ≤ ∑ i ∈ Finset.range n, r ^ i

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case inr
r : ℝ≥0∞
hr : 1 ≤ r
a : ℝ≥0∞
ha : a < ∞
n : ℕ
hn : a < ↑n
⊢ ↑n ≤ ∑ a ∈ Finset.range n, r ^ a

Tactic:
calc
      (n : ℝ≥0∞) = ∑ i ∈ range n, 1 := by rw [sum_const, nsmul_one, card_range]
      _ ≤ ∑ i ∈ range n, r ^ i := by gcongr; apply one_le_pow₀ hr

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: r : ℝ≥0∞
⊢ ∑' (n : ℕ), r ^ n = (1 - r)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: r : ℝ≥0∞
⊢ ∑' (n : ℕ), r ^ (n + 1) = r * (1 - r)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: ⊢ ∑' (m : ℕ), 2 ^ (-1 - ↑m) = 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: ⊢ ∑' (n : ℕ), 2⁻¹ ^ n = 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: r : ℝ≥0∞
⊢ ∑' (n : ℕ), r ^ n < ∞ ↔ r < 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: r : ℝ≥0∞
hr : r < 1
ι : Type u_4
inst✝ : Encodable ι
⊢ ∑' (y : ℕ), r ^ y < ∞

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
⊢ (comap f) (OuterMeasure.ofFunction m m_empty) = OuterMeasure.ofFunction (fun s ↦ m (f '' s)) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
r C : ℝ≥0∞
hr : r < 1
hC : C ≠ ∞
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n
⊢ CauchySeq f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: ⊢ LowerSemicontinuous fun p ↦ p.1 + p.2

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
s : Set β
⊢ ((map f) (OuterMeasure.ofFunction m m_empty)) s ≤ m (f ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: a b : EReal
h : ContinuousAt (fun p ↦ p.1 * p.2) (a, b)
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (b, a)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
r C : ℝ≥0∞
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ edist (f n) a ≤ C * r ^ n / (1 - r)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: a b : EReal
h : ContinuousAt (fun p ↦ p.1 * p.2) (a, b)
⊢ (fun p ↦ p.1 * p.2) = (fun x ↦ -x) ∘ (fun p ↦ p.1 * p.2) ∘ fun p ↦ (-p.1, p.2)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
r C : ℝ≥0∞
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
⊢ edist (f 0) a ≤ C / (1 - r)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: a b : EReal
h : ContinuousAt (fun p ↦ p.1 * p.2) (a, b)
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (-a, b)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
hC : C ≠ ∞
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C / 2 ^ n
⊢ CauchySeq f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: a b : ℝ
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a, ↑b)

Tactic:
by

Goal state after: