mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.InfiniteSum.Real

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a : α
h : Summable fun n ↦ dist (f n) (f n.succ)
ha : Tendsto f atTop (𝓝 a)
⊢ dist (f 0) a ≤ ∑' (n : ℕ), dist (f n) (f n.succ)

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a : α
h : Summable fun n ↦ dist (f n) (f n.succ)
ha : Tendsto f atTop (𝓝 a)
⊢ dist (f 0) a ≤ ∑' (n : ℕ), dist (f n) (f n.succ)
Module: Mathlib.Topology.Algebra.InfiniteSum.Real

Goal state before:
pp: f : ℕ → ℝ≥0
⊢ (¬Summable fun i ↦ ↑(f i)) ↔ Tendsto (fun n ↦ ∑ i ∈ range n, (fun i ↦ ↑(f i)) i) atTop atTop

Tactic:
simpa using

Goal state after:
f : ℕ → ℝ≥0
⊢ (¬Summable fun i ↦ ↑(f i)) ↔ Tendsto (fun n ↦ ∑ i ∈ range n, ↑(f i)) atTop atTop
Module: Mathlib.Topology.Algebra.InfiniteSum.Real

Goal state before:
pp: α : Type u_4
β : α → Type u_3
f : (x : α) × β x → ℝ≥0
⊢ (Summable fun i ↦ ↑(f i)) ↔
    (∀ (x : α), Summable fun y ↦ (fun i ↦ ↑(f i)) ⟨x, y⟩) ∧ Summable fun x ↦ ∑' (y : β x), (fun i ↦ ↑(f i)) ⟨x, y⟩

Tactic:
simpa using

Goal state after:
α : Type u_4
β : α → Type u_3
f : (x : α) × β x → ℝ≥0
⊢ (Summable fun i ↦ ↑(f i)) ↔ (∀ (x : α), Summable fun y ↦ ↑(f ⟨x, y⟩)) ∧ Summable fun x ↦ ∑' (y : β x), ↑(f ⟨x, y⟩)
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: case pos
δ : Type u_4
X : δ → Type u_6
inst✝¹ : (i : δ) → MeasurableSpace (X i)
inst✝ : DecidableEq δ
is : List δ
j : δ
hj : j ∈ j :: is
⊢ Measurable fun v ↦ v.elim hj

Tactic:
simpa using

Goal state after:
case pos
δ : Type u_4
X : δ → Type u_6
inst✝¹ : (i : δ) → MeasurableSpace (X i)
inst✝ : DecidableEq δ
is : List δ
j : δ
hj : j ∈ j :: is
⊢ Measurable fun v ↦ v.1
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
p : α → Prop
h : Measurable p
⊢ MeasurableSet {a | p a}

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
p : α → Prop
h : Measurable p
⊢ MeasurableSet {a | p a}
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case inl
z : ℤ
hz : Odd z
⊢ 0 ^ z = 0

pp: case inr
s : SignType
z : ℤ
hz : Odd z
hs : s ≠ 0
⊢ s ^ z = s

Tactic:
· rw [zero_zpow]
    rintro rfl
    simp at hz

Goal state after:
case inr
s : SignType
z : ℤ
hz : Odd z
hs : s ≠ 0
⊢ s ^ z = s
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
h : (if a < 0 then -1 else 0) = 1
hn : ¬0 < a
⊢ False

Tactic:
split_ifs at h

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsSemitopologicalSemiring A
x : A
s : Subalgebra R A
hs : IsClosed[inst✝³] ↑s
hx : x ∈ s
⊢ {x} ⊆ ↑s

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsSemitopologicalSemiring A
x : A
s : Subalgebra R A
hs : IsClosed[inst✝³] ↑s
hx : x ∈ s
⊢ x ∈ s
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
h : (if 0 < a then 1 else if a < 0 then -1 else 0) = -1
⊢ a < 0

Tactic:
split_ifs at h

Goal state after:
case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
h✝¹ : ¬0 < a
h✝ : a < 0
h : -1 = -1
⊢ a < 0
Module: Mathlib.Topology.Algebra.Algebra

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsSemitopologicalSemiring A
x : A
⊢ IsClosed[inst✝³] (range Subtype.val)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsSemitopologicalSemiring A
x : A
⊢ IsClosed[inst✝³] ↑(elemental R x)
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0
r : ℝ≥0
⊢ HasSum (fun a ↦ ↑(f a)) ↑r ↔ HasSum f r

Tactic:
by
  simp only [HasSum, ← ofNNReal_finsetSum, tendsto_coe]

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

Goal state before:
pp: α : Type u_4
inst✝ : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
A : Tendsto (fun n ↦ ↑n * c) atTop (𝓝 (∞ * c))
n : ℕ
s : Finset α
hs : #s = n
⊢ ↑n * c ≤ ∑' (x : α), c

Tactic:
simpa using

Goal state after:
α : Type u_4
inst✝ : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
A : Tendsto (fun n ↦ ↑n * c) atTop (𝓝 (∞ * c))
n : ℕ
s : Finset α
hs : #s = n
⊢ ↑n * c ≤ ∑' (x : α), c
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_4
inst✝ : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
A : Tendsto (fun n ↦ ↑n * c) atTop (𝓝 (∞ * c))
B : ∀ (n : ℕ), ↑n * c ≤ ∑' (x : α), c
⊢ ∑' (x : α), c = ∞

Tactic:
simpa using

Goal state after:
α : Type u_4
inst✝ : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
A : Tendsto (fun n ↦ ↑n * c) atTop (𝓝 (∞ * c))
B : ∀ (n : ℕ), ↑n * c ≤ ∑' (x : α), c
⊢ ∑' (x : α), c = ∞
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case neg_left
x✝ y✝ : EReal
h : (x✝ * y✝).abs = x✝.abs * y✝.abs
⊢ (x✝ * y✝).abs = (-x✝).abs * y✝.abs

Tactic:
EReal.abs_neg

Goal state after:
case neg_left
x✝ y✝ : EReal
h : (x✝ * y✝).abs = x✝.abs * y✝.abs
⊢ (x✝ * y✝).abs = x✝.abs * y✝.abs
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0∞
R : Type u_4
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
a : R
⊢ ∑' (i : α), a • f i = a • ∑' (i : α), f i

Tactic:
simpa using

Goal state after:
α : Type u_1
f : α → ℝ≥0∞
R : Type u_4
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
a : R
⊢ ∑' (i : α), a • f i = a • ∑' (i : α), f i
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_4
f : α → ℝ≥0∞
hf : ∑' (i : α), f i ≠ ∞
⊢ Summable (ENNReal.toNNReal ∘ f)

Tactic:
simpa using

Goal state after:
α : Type u_4
f : α → ℝ≥0∞
hf : ∑' (i : α), f i ≠ ∞
⊢ ∑' (b : α), f b ≠ ∞
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0∞
s t : Set α
⊢ ∑' (x : ↑(⋃ b, bif b then s else t)), f ↑x ≤ ∑' (x : ↑s), f ↑x + ∑' (x : ↑t), f ↑x

Tactic:
simpa using

Goal state after:
α : Type u_1
f : α → ℝ≥0∞
s t : Set α
⊢ ∑' (x : ↑(⋃ b, bif b then s else t)), f ↑x ≤ ∑' (x : ↑s), f ↑x + ∑' (x : ↑t), f ↑x
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case mp.neg
x y : EReal
h : ↑neg * ↑x.abs ≤ ↑neg * ↑y.abs
hs : sign x = sign y
hy : sign y = neg
⊢ neg = neg ∧ neg = neg ∧ y.abs ≤ x.abs

Tactic:
simpa using

Goal state after:
case mp.neg
x y : EReal
h : ↑neg * ↑x.abs ≤ ↑neg * ↑y.abs
hs : sign x = sign y
hy : sign y = neg
⊢ y.abs ≤ x.abs
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case mp.pos
x y : EReal
h : ↑pos * ↑x.abs ≤ ↑pos * ↑y.abs
hs : sign x = sign y
hy : sign y = pos
⊢ pos = pos ∧ pos = pos ∧ x.abs ≤ y.abs

Tactic:
simpa using

Goal state after:
case mp.pos
x y : EReal
h : ↑pos * ↑x.abs ≤ ↑pos * ↑y.abs
hs : sign x = sign y
hy : sign y = pos
⊢ x.abs ≤ y.abs
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
h : Semicontinuous r
b : β
⊢ IsOpen[inst✝] {x | r x b}

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
h : Semicontinuous r
b : β
⊢ ∀ (x : α), r x b → {x | r x b} ∈ 𝓝 x
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0
h : Summable fun a ↦ ↑(f a)
⊢ (support f).Countable

Tactic:
simpa using

Goal state after:
α : Type u_1
f : α → ℝ≥0
h : Summable fun a ↦ ↑(f a)
⊢ {x | ¬f x = 0}.Countable
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: case mpr
α : Type u_1
β : α → Type u_4
f : (x : α) × β x → ℝ≥0
h₁ : ∀ (x : α), Summable fun y ↦ f ⟨x, y⟩
h₂ : Summable fun x ↦ ∑' (y : β x), f ⟨x, y⟩
⊢ Summable f

Tactic:
simpa using

Goal state after:
case mpr
α : Type u_1
β : α → Type u_4
f : (x : α) × β x → ℝ≥0
h₁ : ∀ (x : α), Summable fun y ↦ f ⟨x, y⟩
h₂ : Summable fun x ↦ ∑' (y : β x), f ⟨x, y⟩
⊢ ∑' (a : α) (b : β a), ↑(f ⟨a, b⟩) ≠ ∞
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
g : α → ℝ≥0
hg : Summable g
i : α
hi : 0 < g i
⊢ 0 < ∑' (b : α), g b

Tactic:
simpa using

Goal state after:
α : Type u_1
g : α → ℝ≥0
hg : Summable g
i : α
hi : 0 < g i
⊢ 0 < ∑' (b : α), g b
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
h : HasOpenCGraph f
x : α
b : β
hb : b ∈ f x
⊢ IsOpen[inst✝¹] {x' | b ∈ f x'}

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
h : HasOpenCGraph f
x : α
b : β
hb : b ∈ f x
⊢ IsOpen[inst✝¹] {x' | b ∈ f x'}
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
h : HasOpenCGraph f
x : α
b : β
hb : b ∈ f x
hopen : IsOpen[inst✝¹] {x' | b ∈ f x'}
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun x b ↦ b ∈ f x) x' b

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
h : HasOpenCGraph f
x : α
b : β
hb : b ∈ f x
hopen : IsOpen[inst✝¹] {x' | b ∈ f x'}
⊢ {x | b ∈ f x} ∈ 𝓝 x
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0
h : ∑' (i : α), (fun i ↦ ↑(f i)) i ≠ ∞
⊢ (support fun i ↦ ↑(f i)).Countable

Tactic:
simpa using

Goal state after:
α : Type u_1
f : α → ℝ≥0
h : ∑' (i : α), (fun i ↦ ↑(f i)) i ≠ ∞
⊢ {x | ¬f x = 0}.Countable
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
⊢ b * (a / b) = a

Tactic:
@mul_div_cancel a b hbot htop hzero

Goal state after:
case refine_2
a b c : EReal
hbot : b ≠ ⊥
htop : b ≠ ⊤
hzero : b ≠ 0
h : c = a * b
⊢ a = a
Module: Mathlib.Data.EReal.Inv

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

Tactic:
nth_rw 1 [← @mul_div_cancel c b (ne_bot_of_gt h) h' h.ne']
  rw [mul_div b c b, mul_comm b]
  exact StrictMono.le_iff_le (strictMono_div_right_of_pos h h')

Goal state after:
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)
⊢ edist (f 0) a ≤ ∑' (m : ℕ), d m

Tactic:
simpa using

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)
⊢ edist (f 0) a ≤ ∑' (m : ℕ), d m
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

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

Tactic:
simpa using

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:
simpa using

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

Goal state before:
pp: α : 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
H : s ∩ ⋂ i ∈ I, f i ⁻¹' Iic c = ∅
this : ∀ i ∈ I, IsClosed[instTopologicalSpaceSubtype] (s ↓∩ (fun i ↦ f i ⁻¹' Iic c) i)
⊢ ∃ u, ∀ x ∈ s, ∃ i ∈ u, c < f (↑i) x

Tactic:
simpa using

Goal state after:
α : 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
H : s ∩ ⋂ i ∈ I, f i ⁻¹' Iic c = ∅
this : ∀ i ∈ I, IsClosed[instTopologicalSpaceSubtype] (s ↓∩ (fun i ↦ f i ⁻¹' Iic c) i)
⊢ ∃ u, ∀ x ∈ s, ∃ a, (∃ (x : a ∈ I), ⟨a, ⋯⟩ ∈ u) ∧ c < f a x
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: ⊢ 𝓝[≠] ⊥ = map Real.toEReal atBot

Tactic:
by
  apply (nhdsWithin_hasBasis nhds_bot_basis_Iic _).ext (atBot_basis.map Real.toEReal)
  · simp only [EReal.image_coe_Iic,
      true_and]
    intro x hx
    by_cases hx_top : x = ⊤
    · simp [hx_top]
    lift x to ℝ using ⟨hx_top, hx.ne_bot⟩
    refine ⟨x, fun x ⟨h1, h2⟩ ↦ ?_⟩
    simp [h2, h1.ne_bot]
  · simp only [EReal.image_coe_Iic, true_implies]
    refine fun x ↦ ⟨x, ⟨EReal.bot_lt_coe x, fun x ⟨(h1 : x ≤ _), h2⟩ ↦ ?_⟩⟩
    simp [h1, Ne.bot_lt' fun a ↦ h2 a.symm]

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
hε : 0 < ε
hb : ∑' (i : ℕ), μ (s i) < ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), ↑(ε' i) < ↑ε
i : ℕ
⊢ ↑(ε' i) ≠ 0

Tactic:
simpa using

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 : ℕ
⊢ ¬ε' i = 0
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:
simpa using

Goal state after:
case pos
x✝ : EReal
h_top : ¬x✝ = ⊤
x : EReal
hx : x ∈ {⊤}ᶜ
h_bot : x = ⊥
⊢ ∃ i, ∀ ⦃x : EReal⦄, x < ↑i → x.toReal ≤ 0
Module: Mathlib.Analysis.SpecificLimits.Basic

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

Tactic:
simpa using

Goal state after:
𝕜 : Type u_4
inst✝⁴ : DivisionSemiring 𝕜
inst✝³ : CharZero 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : ContinuousSMul ℚ≥0 𝕜
inst✝ : ContinuousMul 𝕜
C : 𝕜
⊢ Tendsto (fun n ↦ C * (↑n)⁻¹) atTop (𝓝 0)
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case inr.a
α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
⊢ ∀ y > limsup u f * c, ∀ᶠ (a : α) in f, u a * c < y

Tactic:
simpa using

Goal state after:
case inr.a
α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
⊢ ∀ (y : EReal), limsup u f < y / c → ∀ᶠ (a : α) in f, u a < y / c
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case a
α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
⊢ ∀ y < limsup u f * c, ∃ᶠ (a : α) in f, y < u a * c

Tactic:
simpa using

Goal state after:
case a
α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
⊢ ∀ (y : EReal), y / c < limsup u f → ∃ᶠ (a : α) in f, y / c < u a
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:
simpa using

Goal state after:
α : 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
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:
simpa using

Goal state after:
α : 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
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:
simpa using

Goal state after:
α : 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
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case inl
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h✝ : f.NeBot
u_0 : 0 ≤ limsup u f
h₁ : 0 < limsup u f ∨ limsup v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ 0 < limsup v f
a : EReal
a_u : a > limsup u f
b : EReal
b_v : b > limsup v f
c : EReal
c_ab : c > a * b
x : α
x_a : u x < a
x_b : v x < b
v_0 : 0 x ≤ v x
hux : u x < 0
⊢ 0 ≤ a * b

Tactic:
exact mul_nonneg (u_0.trans a_u.le) (v_0.trans x_b.le)

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

Goal state before:
pp: case h
𝕜 : 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 * (↑k)⁻¹ + c) / (b * (↑k)⁻¹ + d)) atTop (𝓝 (c / d))

Tactic:
apply Filter.Tendsto.div _ _ hd

Goal state after:
𝕜 : 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 * (↑k)⁻¹ + c) atTop (𝓝 c)

𝕜 : 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 ↦ b * (↑k)⁻¹ + d) atTop (𝓝 d)
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: a r : ℝ
x✝ : EReal × EReal
h : ↑(r - (a - 1)) < x✝.1 ∧ ↑(a - 1) < x✝.2
⊢ ↑r < x✝.1 + x✝.2

Tactic:
simpa using

Goal state after:
a r : ℝ
x✝ : EReal × EReal
h : ↑(r - (a - 1)) < x✝.1 ∧ ↑(a - 1) < x✝.2
⊢ ↑r < x✝.1 + x✝.2
Module: Mathlib.Topology.Instances.EReal.Lemmas

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

Tactic:
simpa using

Goal state after:
a : ℝ
⊢ Tendsto (fun p ↦ p.1 + p.2) (𝓝 (↑a, ⊤)) (𝓝 (↑a + ⊤))
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: r : ℝ
x✝ : EReal × EReal
h : ↑0 < x✝.1 ∧ ↑r < x✝.2
⊢ ↑r < x✝.1 + x✝.2

Tactic:
simpa using

Goal state after:
r : ℝ
x✝ : EReal × EReal
h : ↑0 < x✝.1 ∧ ↑r < x✝.2
⊢ ↑r < x✝.1 + x✝.2
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: a r : ℝ
x✝ : EReal × EReal
h : x✝.1 < ↑(r - (a + 1)) ∧ x✝.2 < ↑(a + 1)
⊢ x✝.1 + x✝.2 < ↑r

Tactic:
simpa using

Goal state after:
a r : ℝ
x✝ : EReal × EReal
h : x✝.1 < ↑(r - (a + 1)) ∧ x✝.2 < ↑(a + 1)
⊢ x✝.1 + x✝.2 < ↑r
Module: Mathlib.Topology.Instances.EReal.Lemmas

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

Tactic:
simpa using

Goal state after:
a : ℝ
⊢ Tendsto (fun p ↦ p.1 + p.2) (𝓝 (↑a, ⊥)) (𝓝 (⊥ + ↑a))
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: r : ℝ
x✝ : EReal × EReal
h : x✝.1 < ↑0 ∧ x✝.2 < ↑r
⊢ x✝.1 + x✝.2 < ↑r

Tactic:
simpa using

Goal state after:
r : ℝ
x✝ : EReal × EReal
h : x✝.1 < ↑0 ∧ x✝.2 < ↑r
⊢ x✝.1 + x✝.2 < ↑r
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case pos
α : 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₂
H : f z ≤ f x
⊢ min (f z) (f x) ∈ u

Tactic:
simpa using

Goal state after:
case pos
α : 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₂
H : f z ≤ f x
⊢ f z ∈ u
Module: Mathlib.Analysis.SpecificLimits.Basic

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

Tactic:
simpa using

Goal state after:
r : ℝ≥0
h : Tendsto (fun n ↦ r ^ n) atTop (𝓝 0)
⊢ r < 1
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case pos
α : 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
H : g z ≤ g x
⊢ min (g z) (g x) ∈ v

Tactic:
simpa using

Goal state after:
case pos
α : 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
H : g z ≤ g x
⊢ g z ∈ v
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case refine_2
r : ℝ≥0∞
r_gt_one : 1 < r
obs : r⁻¹ < 1 → Tendsto (fun x ↦ (r⁻¹ ^ x)⁻¹) atTop (𝓝 ∞)
⊢ Tendsto (fun n ↦ r ^ n) atTop (𝓝 ∞)

Tactic:
simpa using

Goal state after:
case refine_2
r : ℝ≥0∞
r_gt_one : 1 < r
obs : r⁻¹ < 1 → Tendsto (fun x ↦ (r⁻¹ ^ x)⁻¹) atTop (𝓝 ∞)
⊢ Tendsto (fun n ↦ r ^ n) atTop (𝓝 ∞)