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

Goal state before:
pp: R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousSMul R A
⊢ Continuous[inst✝², inst✝¹] fun r ↦ r • 1

Tactic:
]

Goal state after:
R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousSMul R A
⊢ Continuous[inst✝², inst✝¹] fun r ↦ r • 1
Module: Mathlib.Data.Nat.Cast.Order.Field

Goal state before:
pp: case zero
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
m : ℕ
⊢ 0 ≤ 0

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Field

Goal state before:
pp: case succ
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
m n✝ : ℕ
⊢ m / (n✝ + 1) * (n✝ + 1) ≤ m

pp: case succ
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
m n✝ : ℕ
⊢ 0 < ↑(n✝ + 1)

Tactic:
]

Goal state after:
case succ
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
m n✝ : ℕ
⊢ m / (n✝ + 1) * (n✝ + 1) ≤ m

case succ
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
m n✝ : ℕ
⊢ 0 < ↑(n✝ + 1)
Module: Mathlib.Data.Nat.Cast.Order.Field

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n : ℕ
⊢ 0 < (↑n + 1)⁻¹

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n : ℕ
⊢ 0 < (↑n + 1)⁻¹
Module: Mathlib.Topology.Algebra.Algebra

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
A : Type u_2
inst✝⁷ : Semiring A
inst✝⁶ : TopologicalSpace A
B : Type u_3
inst✝⁵ : Semiring B
inst✝⁴ : TopologicalSpace B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsSemitopologicalSemiring A
inst✝ : IsSemitopologicalSemiring B
f : A →A[R] B
hf' : DenseRange ⇑f
s : Subalgebra R A
hs : ↑s.topologicalClosure = ↑⊤
⊢ ↑(map (↑f) s).topologicalClosure = ↑⊤

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
A : Type u_2
inst✝⁷ : Semiring A
inst✝⁶ : TopologicalSpace A
B : Type u_3
inst✝⁵ : Semiring B
inst✝⁴ : TopologicalSpace B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsSemitopologicalSemiring A
inst✝ : IsSemitopologicalSemiring B
f : A →A[R] B
hf' : DenseRange ⇑f
s : Subalgebra R A
hs : ↑s.topologicalClosure = ↑⊤
⊢ ↑(map (↑f) s).topologicalClosure = ↑⊤
Module: Mathlib.Topology.Algebra.Algebra

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : Semiring A
inst✝¹ : TopologicalSpace A
inst✝ : Algebra R A
f : A →A[R] A
⊢ f = ContinuousAlgHom.id R A ↔ f = ContinuousAlgHom.id R A

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Field

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : AddRightMono α
n : ℕ
⊢ (↑n)⁻¹ ≤ 1

Tactic:
]

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : AddRightMono α
n : ℕ
⊢ (↑n)⁻¹ ≤ 1
Module: Mathlib.Data.Nat.Cast.Order.Field

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : AddLeftMono α
n : ℕ
⊢ 0 ≤ 1 / ↑n

Tactic:
]

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : AddLeftMono α
n : ℕ
⊢ 0 ≤ 1 / ↑n
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
ha : 0 < a
⊢ 1 = 1

pp: case hc
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
ha : 0 < a
⊢ 0 < a

Tactic:
]

Goal state after:
case hc
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
ha : 0 < a
⊢ 0 < a
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
ha : a < 0
⊢ -1 = -1

pp: case hc
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
ha : a < 0
⊢ a < 0

Tactic:
]

Goal state after:
case hc
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
ha : a < 0
⊢ 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
s : Subalgebra R A
B : Type u_2
inst✝³ : TopologicalSpace B
inst✝² : Ring B
inst✝¹ : IsSemitopologicalRing B
inst✝ : Algebra R B
f : B →ₐ[R] A
f' : B ≃ₜ A
w : ⇑f = ⇑f'
⊢ ⇑f' ⁻¹' ↑s.topologicalClosure = closure[inst✝³] (⇑f' ⁻¹' ↑s)

Tactic:
]

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
s : Subalgebra R A
B : Type u_2
inst✝³ : TopologicalSpace B
inst✝² : Ring B
inst✝¹ : IsSemitopologicalRing B
inst✝ : Algebra R B
f : B →ₐ[R] A
f' : B ≃ₜ A
w : ⇑f = ⇑f'
⊢ ⇑f' ⁻¹' ↑s.topologicalClosure = closure[inst✝³] (⇑f' ⁻¹' ↑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:
]

Goal state after:
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
h : (if a < 0 then -1 else 0) = 1
hn : ¬0 < a
⊢ False
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:
]

Goal state after:
α : 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
Module: Mathlib.Data.Sign.Defs

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

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : (if 0 < a then 1 else if a < 0 then -1 else 0) = 0
⊢ a = 0
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0
r : ℝ≥0
hr : HasSum f r
⊢ ↑r = ↑r

Tactic:
]

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

Goal state before:
pp: β : Type u_2
f : β → ℝ≥0
a : ℝ≥0
ha : ↑a = ∑' (b : β), ↑(f b)
⊢ HasSum (fun a ↦ ↑(f a)) (∑' (b : β), ↑(f b))

Tactic:
]

Goal state after:
β : Type u_2
f : β → ℝ≥0
a : ℝ≥0
ha : ↑a = ∑' (b : β), ↑(f b)
⊢ HasSum (fun a ↦ ↑(f a)) (∑' (b : β), ↑(f b))
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0∞
ι : Type u_4
s : ι → Finset α
hs : ∀ (t : Finset α), ∃ i, t ⊆ s i
⊢ ⨆ s, ∑ a ∈ s, f a = ⨆ i, ∑ a ∈ s i, f a

Tactic:
]

Goal state after:
α : Type u_1
f : α → ℝ≥0∞
ι : Type u_4
s : ι → Finset α
hs : ∀ (t : Finset α), ∃ i, t ⊆ s i
⊢ ⨆ s, ∑ a ∈ s, f a = ⨆ i, ∑ a ∈ s i, f a
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
ι : Type u_4
f : α → ℝ≥0∞
t : ι → Set α
h : univ.PairwiseDisjoint t
⊢ ∑' (x : ↑(⋃ i, t i)), f ↑x = ∑' (x : ↑univ) (x_1 : ↑(t ↑x)), f ↑x_1

Tactic:
]

Goal state after:
α : Type u_1
ι : Type u_4
f : α → ℝ≥0∞
t : ι → Set α
h : univ.PairwiseDisjoint t
⊢ ∑' (x : ↑(⋃ i, t i)), f ↑x = ∑' (x : ↑univ) (x_1 : ↑(t ↑x)), f ↑x_1
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: ⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
f : α → ℝ≥0∞
t : ι → Set α
h : univ.PairwiseDisjoint t
⊢ ∑' (x : ↑(⋃ i, t i)), f ↑x = ∑' (x : ↑(⋃ x, t x)), f ↑x

Tactic:
]

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

Goal state before:
pp: x : ℝ
⊢ ↑↑(Real.nnabs x) = ↑↑(Real.nnabs x)

Tactic:
]

Goal state after:
x : ℝ
⊢ ↑↑(Real.nnabs x) = ↑↑(Real.nnabs x)
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: ι : Type u_4
s : Finset ι
f : ι → ℝ≥0∞
⊢ ∑' (x : ι), (↑s).indicator f x + ∑' (x : ι), (↑s)ᶜ.indicator f x = ∑' (i : ι), f i

Tactic:
]

Goal state after:
ι : Type u_4
s : Finset ι
f : ι → ℝ≥0∞
⊢ ∑' (x : ι), (↑s).indicator f x + ∑' (x : ι), (↑s)ᶜ.indicator f x = ∑' (i : ι), f i
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: x : ℝ
⊢ ENNReal.ofReal |x| = ENNReal.ofReal |x|

Tactic:
]

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

Goal state before:
pp: α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
h : ∀ b < a, ∃ I, b < ∑ i ∈ I, f i
⊢ a ≤ ∑' (i : α), f i

Tactic:
refine le_of_forall_lt fun b hb ↦ ?_

Goal state after:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
h : ∀ b < a, ∃ I, b < ∑ i ∈ I, f i
b : ℝ≥0∞
hb : b < a
⊢ b < ∑' (i : α), f i
Module: Mathlib.Data.EReal.Inv

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

Tactic:
]

Goal state after:
case symm
x✝ y✝ : EReal
h : (x✝ * y✝).abs = x✝.abs * y✝.abs
⊢ (x✝ * y✝).abs = x✝.abs * y✝.abs
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ ∞ = ∞

pp: case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ (↑x✝).abs ≠ 0

Tactic:
]

Goal state after:
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ (↑x✝).abs ≠ 0
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ ¬x✝ = 0

Tactic:
]

Goal state after:
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ ¬x✝ = 0
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: case neg
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
hf : ¬∑' (i : α), f i = 0
⊢ ∑' (i : α), a * f i = a * ∑' (i : α), f i

Tactic:
]

Goal state after:
case neg
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
hf : ¬∑' (i : α), f i = 0
⊢ ∑' (i : α), a * f i = a * ∑' (i : α), f i
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:
]

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.Data.EReal.Inv

Goal state before:
pp: x : ℝ
⊢ -sign x = -sign x

Tactic:
]

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

Goal state before:
pp: case symm
x✝ y✝ : EReal
h : sign (x✝ * y✝) = sign x✝ * sign y✝
⊢ sign (x✝ * y✝) = sign x✝ * sign y✝

Tactic:
]

Goal state after:
case symm
x✝ y✝ : EReal
h : sign (x✝ * y✝) = sign x✝ * sign y✝
⊢ sign (x✝ * y✝) = sign x✝ * sign y✝
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: f : ℕ → ℝ≥0∞
r : ℝ≥0∞
h : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
⊢ HasSum f (∑' (i : ℕ), f i)

pp: f : ℕ → ℝ≥0∞
r : ℝ≥0∞
h : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
⊢ Monotone fun n ↦ ∑ i ∈ Finset.range n, f i

Tactic:
]

Goal state after:
f : ℕ → ℝ≥0∞
r : ℝ≥0∞
h : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
⊢ HasSum f (∑' (i : ℕ), f i)

f : ℕ → ℝ≥0∞
r : ℝ≥0∞
h : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
⊢ Monotone fun n ↦ ∑ i ∈ Finset.range n, f i
Module: Mathlib.Data.EReal.Inv

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

Tactic:
]

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

Goal state before:
pp: f : ℕ → ℝ≥0∞
⊢ HasSum f (∑' (n : ℕ), f n)

Tactic:
]

Goal state after:
f : ℕ → ℝ≥0∞
⊢ HasSum f (∑' (n : ℕ), f n)
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: x : ℝ
⊢ ↑x = ↑x

Tactic:
]

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

Goal state before:
pp: x : EReal
⊢ x = x

Tactic:
]

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

Goal state before:
pp: case mp
x y : EReal
habs : x.abs = y.abs
hsign : sign x = sign y
⊢ ↑(sign y) * ↑y.abs = ↑(sign y) * ↑y.abs

Tactic:
]

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

Goal state before:
pp: α : Type u_4
f : α → ℝ≥0∞
hf : ∑' (x : α), f x ≠ ∞
f_ne_top : ∀ (n : α), f n ≠ ∞
h_f_coe : f = fun n ↦ ↑(f n).toNNReal
⊢ Tendsto (fun n ↦ (f n).toNNReal) cofinite (𝓝 0)

Tactic:
]

Goal state after:
α : Type u_4
f : α → ℝ≥0∞
hf : ∑' (x : α), f x ≠ ∞
f_ne_top : ∀ (n : α), f n ≠ ∞
h_f_coe : f = fun n ↦ ↑(f n).toNNReal
⊢ Tendsto (fun n ↦ (f n).toNNReal) cofinite (𝓝 0)
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: f : ℕ → ℝ≥0∞
hf : ∑' (x : ℕ), f x ≠ ∞
⊢ Tendsto f cofinite (𝓝 0)

Tactic:
]

Goal state after:
f : ℕ → ℝ≥0∞
hf : ∑' (x : ℕ), f x ≠ ∞
⊢ Tendsto f cofinite (𝓝 0)
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case mp
x y : EReal
h : ↑(sign x) * ↑x.abs ≤ ↑(sign y) * ↑y.abs
hs : sign x = sign y
⊢ sign x = neg ∧ sign y = neg ∧ y.abs ≤ x.abs ∨
    sign x = zero ∧ sign y = zero ∨ sign x = pos ∧ sign y = pos ∧ x.abs ≤ y.abs

Tactic:
]

Goal state after:
case mp
x y : EReal
h : ↑(sign x) * ↑x.abs ≤ ↑(sign y) * ↑y.abs
hs : sign x = sign y
⊢ sign x = neg ∧ sign y = neg ∧ y.abs ≤ x.abs ∨
    sign x = zero ∧ sign y = zero ∨ sign x = pos ∧ sign y = pos ∧ x.abs ≤ y.abs
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: case e'_3
α : Type u_4
f : α → ℝ≥0
hf : ∑' (x : α), (fun i ↦ ↑(f i)) x ≠ ∞
x✝ : Finset α
⊢ ∑' (b : { x // x ∉ x✝ }), (fun i ↦ ↑(f i)) ↑b = ∑' (a : { x // x ∉ x✝ }), ↑(f ↑a)

pp: case e'_3
α : Type u_4
f : α → ℝ≥0
hf : ∑' (x : α), (fun i ↦ ↑(f i)) x ≠ ∞
x✝ : Finset α
⊢ Summable fun b ↦ f ↑b

Tactic:
]

Goal state after:
case e'_3
α : Type u_4
f : α → ℝ≥0
hf : ∑' (x : α), (fun i ↦ ↑(f i)) x ≠ ∞
x✝ : Finset α
⊢ Summable fun b ↦ f ↑b
Module: Mathlib.Data.EReal.Inv

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

Tactic:
]

Goal state after:
case mp.zero
x y : EReal
h : ↑zero * ↑x.abs ≤ ↑zero * ↑y.abs
hs : sign x = sign y
hy : sign y = zero
⊢ zero = neg ∧ zero = neg ∧ y.abs ≤ x.abs ∨ zero = zero ∧ zero = zero ∨ zero = pos ∧ zero = pos ∧ x.abs ≤ y.abs
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 ∨ neg = zero ∧ neg = zero ∨ neg = pos ∧ neg = pos ∧ x.abs ≤ y.abs

Tactic:
]

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
⊢ neg = neg ∧ neg = neg ∧ y.abs ≤ x.abs ∨ neg = zero ∧ neg = zero ∨ neg = pos ∧ neg = pos ∧ x.abs ≤ y.abs
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝ : Fintype ι
f : α → ℝ≥0∞
t : ι → Set α
⊢ ∑' (x : ↑(⋃ i, t i)), f ↑x ≤ ∑' (b : ι) (x : ↑(t b)), f ↑x

Tactic:
]

Goal state after:
α : Type u_1
ι : Type u_4
inst✝ : Fintype ι
f : α → ℝ≥0∞
t : ι → Set α
⊢ ∑' (x : ↑(⋃ i, t i)), f ↑x ≤ ∑' (b : ι) (x : ↑(t b)), f ↑x
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 = neg ∧ pos = neg ∧ y.abs ≤ x.abs ∨ pos = zero ∧ pos = zero ∨ pos = pos ∧ pos = pos ∧ x.abs ≤ y.abs

Tactic:
]

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
⊢ pos = neg ∧ pos = neg ∧ y.abs ≤ x.abs ∨ pos = zero ∧ pos = zero ∨ pos = pos ∧ pos = pos ∧ x.abs ≤ y.abs
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: f : ℕ → ℝ≥0∞
hf : f 0 = ∞ ∨ ∑' (b : ℕ), f (b + 1) = ∞
hf0 : f 0 ≠ ∞
⊢ ∑' (n : ℕ), f (n + 1) = ∞

Tactic:
]

Goal state after:
f : ℕ → ℝ≥0∞
hf : f 0 = ∞ ∨ ∑' (b : ℕ), f (b + 1) = ∞
hf0 : f 0 ≠ ∞
⊢ ∑' (n : ℕ), f (n + 1) = ∞
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r r' : α → β → Prop
s : Set α
a : α
h : SemicontinuousWithinAt r s a
has : a ∈ s
b : β
hb : r a b
hfg : ∀ᶠ (x : α) in 𝓝[s] a, r x = r' x
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, r' x' b

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r r' : α → β → Prop
s : Set α
a : α
h : SemicontinuousWithinAt r s a
has : a ∈ s
b : β
hb : r a b
hfg : ∀ᶠ (x : α) in 𝓝[s] a, r x = r' x
⊢ ∀ᶠ (x' : α) in 𝓝[s] a, r' x' b
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: ι : Type u_4
a : ι → ℝ≥0∞
c : ℝ≥0∞
c_ne_top : c ≠ ∞
tsum_le_c : ∑' (i : ι), a i ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
hf : {i | ε ≤ a i}.Finite
⊢ ↑(#hf.toFinset) * ε = ↑(#hf.toFinset) * ε

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
s : Set α
⊢ (∀ (x : α) (h : x ∈ s), SemicontinuousAt (s.domRestrict r) ⟨x, h⟩) ↔ ∀ x ∈ s, SemicontinuousWithinAt r s x

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
s : Set α
⊢ (∀ (x : α) (h : x ∈ s), SemicontinuousAt (s.domRestrict r) ⟨x, h⟩) ↔ ∀ x ∈ s, SemicontinuousWithinAt r s x
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0
⊢ ∑' (a : α), ↑(f a) ≠ ∞ ↔ Summable f

Tactic:
]

Goal state after:
α : Type u_1
f : α → ℝ≥0
⊢ ∑' (a : α), ↑(f a) ≠ ∞ ↔ Summable f
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case mpr.inr.inl
x y : EReal
h : sign x = neg ∧ sign y = neg ∧ y.abs ≤ x.abs
⊢ ↑(sign x) * ↑x.abs ≤ ↑(sign y) * ↑y.abs

Tactic:
]

Goal state after:
case mpr.inr.inl
x y : EReal
h : sign x = neg ∧ sign y = neg ∧ y.abs ≤ x.abs
⊢ ↑(sign x) * ↑x.abs ≤ ↑(sign y) * ↑y.abs
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case mpr.inr.inr.inl
x y : EReal
h : sign x = zero ∧ sign y = zero
⊢ ↑(sign x) * ↑x.abs ≤ ↑(sign y) * ↑y.abs

Tactic:
]

Goal state after:
case mpr.inr.inr.inl
x y : EReal
h : sign x = zero ∧ sign y = zero
⊢ ↑(sign x) * ↑x.abs ≤ ↑(sign y) * ↑y.abs
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: case pos
β : Type u_2
f : β → ℝ≥0
h : Summable f
⊢ ∑' (b : β), f b = tsum f

Tactic:
]

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

Goal state before:
pp: case mpr.inr.inr.inr
x y : EReal
h : sign x = pos ∧ sign y = pos ∧ x.abs ≤ y.abs
⊢ ↑(sign x) * ↑x.abs ≤ ↑(sign y) * ↑y.abs

Tactic:
]

Goal state after:
case mpr.inr.inr.inr
x y : EReal
h : sign x = pos ∧ sign y = pos ∧ x.abs ≤ y.abs
⊢ ↑(sign x) * ↑x.abs ≤ ↑(sign y) * ↑y.abs
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: x y z : EReal
⊢ (x * y * z).abs = (x * (y * z)).abs ∧ sign (x * y * z) = sign (x * (y * z))

Tactic:
]

Goal state after:
x y z : EReal
⊢ (x * y * z).abs = (x * (y * z)).abs ∧ sign (x * y * z) = sign (x * (y * z))
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:
]

Goal state after:
α : Type u_1
f : α → ℝ≥0
h : Summable fun a ↦ ↑(f a)
⊢ (support f).Countable
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
h : b ≤ a
hc : c ≤ 0
⊢ -c * b ≤ -c * a

Tactic:
]

Goal state after:
a b c : EReal
h : b ≤ a
hc : c ≤ 0
⊢ -c * b ≤ -c * a
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
h : b ≤ a
hc : 0 ≤ -c
⊢ -c * b ≤ -c * a

Tactic:
]

Goal state after:
a b c : EReal
h : b ≤ a
hc : 0 ≤ -c
⊢ -c * b ≤ -c * a
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

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

Tactic:
]

Goal state after:
f : ℕ → ℝ≥0
r : ℝ≥0
⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, ↑(f i)) atTop (𝓝 ↑r) ↔ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case h
a✝ : EReal
n : ℕ
a : ℝ
ha : ↑a ≠ ⊤
m : ℕ
an_m : a * ↑n ≤ ↑m
⊢ a * ↑n ≤ ↑m

Tactic:
]

Goal state after:
case h
a✝ : EReal
n : ℕ
a : ℝ
ha : ↑a ≠ ⊤
m : ℕ
an_m : a * ↑n ≤ ↑m
⊢ a * ↑n ≤ ↑m
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

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

Tactic:
intro h
    refine ((tendsto_atTop_of_monotone ?_).resolve_right h).comp ?_
    exacts [Finset.sum_mono_set _, tendsto_finset_range]

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

Goal state before:
pp: ⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: case bot
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case bot
⊢ (-⊥)⁻¹ = -⊥⁻¹

Tactic:
rw [neg_bot, inv_top, inv_bot, neg_zero]

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

Goal state before:
pp: case coe
a✝ : ℝ
⊢ ↑(-a✝)⁻¹ = ↑(-a✝⁻¹)

Tactic:
]

Goal state after:
case coe
a✝ : ℝ
⊢ ↑(-a✝)⁻¹ = ↑(-a✝⁻¹)
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case top
⊢ 0 = 0

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: a : EReal
h : a ≠ ⊥
h' : a ≠ ⊤
⊢ ↑a.toReal = ↑a.toReal

Tactic:
]

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

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

Tactic:
by
  rw [← not_iff_not, Classical.not_not, not_summable_iff_tendsto_nat_atTop]

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

Goal state before:
pp: case symm
a b : EReal
h : (a * b)⁻¹ = a⁻¹ * b⁻¹
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹

Tactic:
]

Goal state after:
case symm
a b : EReal
h : (a * b)⁻¹ = a⁻¹ * b⁻¹
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case top_pos
x : ℝ
x_pos : 0 < x
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case top_neg
x : ℝ
x_neg : x < 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case pos_bot
x : ℝ
x_pos : 0 < x
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case coe_coe
x y : ℝ
⊢ (↑x)⁻¹ * (↑y)⁻¹ = (↑x)⁻¹ * (↑y)⁻¹

Tactic:
]

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

Goal state before:
pp: case neg_bot
x : ℝ
x_neg : x < 0
⊢ 0 = 0

Tactic:
]

Goal state after:
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 β), IsOpen[inst✝] x_1ᶜ → (f x ∩ x_1ᶜ).Nonempty → ∀ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ x_1ᶜ).Nonempty) ↔
    ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ t) → f x ⊆ t

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x : α
s : Set α
⊢ (∀ (x_1 : Set β), IsOpen[inst✝] x_1ᶜ → (f x ∩ x_1ᶜ).Nonempty → ∀ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ x_1ᶜ).Nonempty) ↔
    ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝[s] 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.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: f : ℕ → ℝ≥0
⊢ Tendsto (fun a ↦ ↑(∑' (k : ℕ), f (k + a))) atTop (𝓝 ↑0)

Tactic:
]

Goal state after:
f : ℕ → ℝ≥0
⊢ Tendsto (fun a ↦ ↑(∑' (k : ℕ), f (k + a))) atTop (𝓝 ↑0)
Module: Mathlib.Topology.Semicontinuity.Defs

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

Tactic:
]

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