mathlib-initiative/mathlib-tactics huggingface dataset:
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:
by

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
⊢ sign a = 0 ↔ a = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
⊢ 0 ≤ sign a ↔ 0 ≤ a

Tactic:
by

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

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
⊢ sign a ≤ 0 ↔ a ≤ 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0
r : ℝ≥0
hr : HasSum f r
⊢ ↑(tsum f) = ∑' (a : α), ↑(f a)

Tactic:
by

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

Goal state before:
pp: β : Type u_2
f : β → ℝ≥0
⊢ ∑' (b : β), ↑(f b) ≠ ∞ ↔ Summable f

Tactic:
by

Goal state after:
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
⊢ ∑' (a : α), f a = ⨆ i, ∑ a ∈ s i, f a

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ sign a = sign b ∨ sign a = -sign b

Tactic:
by

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

Goal state before:
pp: x : EReal
⊢ x.abs = 0 ↔ x = 0

Tactic:
by

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

Goal state before:
pp: ⊢ EReal.abs 0 = 0

Tactic:
by

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 = ∑' (i : ι) (x : ↑(t i)), f ↑x

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ ↑(↑x).abs = ↑|x|

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ (-↑x).abs = (↑x).abs

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddLeftStrictMono α
a : α
⊢ sign (-a) = -sign a

Tactic:
by

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:
by

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

Goal state before:
pp: α : Type u_1
a : α → ℝ≥0∞
tsum_ne_top : ∑' (i : α), a i ≠ ∞
j : α
⊢ a j < ∞

Tactic:
by

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

Goal state before:
pp: α : Type u_4
inst✝ : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
⊢ Tendsto (fun n ↦ ↑n * c) atTop (𝓝 (∞ * c))

Tactic:
by

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 : ℕ
⊢ ↑n * c ≤ ∑' (x : α), c

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddRightStrictMono α
a : α
⊢ sign (-a) = -sign a

Tactic:
by

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

Goal state before:
pp: α : Type u_4
inst✝ : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
⊢ ∑' (x : α), c = ∞

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: n : ℤ
⊢ n.sign = ↑(SignType.sign n)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
hf : ¬∑' (i : α), f i = 0
⊢ Tendsto (fun s ↦ ∑ j ∈ s, a * f j) atTop (𝓝 (a * ∑' (i : α), f i))

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ sign (-↑x) = -sign ↑x

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: α : Type u_4
a : α
f : α → ℝ≥0∞
x✝ : α
h : x✝ ≠ a
⊢ ⨆ (_ : a = x✝), f x✝ = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_4
a : α
f : α → ℝ≥0∞
⊢ ⨆ (_ : a = a), f a = f a

Tactic:
by

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

Goal state before:
pp: x y : EReal
⊢ sign (x * y) = sign x * sign y

Tactic:
by

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

Goal state before:
pp: ⊢ ↑(sign ⊥) * ↑⊥.abs = ⊥

Tactic:
by

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

Goal state before:
pp: ⊢ ↑(sign ⊤) * ↑⊤.abs = ⊤

Tactic:
by

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

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

Tactic:
by

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 (𝓝 (∑' (n : ℕ), f n))

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ ↑(sign ↑x) * ↑(↑x).abs = ↑x

Tactic:
by

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

Goal state before:
pp: x : EReal
⊢ ↑x.abs * ↑(sign x) = x

Tactic:
by

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

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

Tactic:
by

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 x) * ↑x.abs = y

Tactic:
← y.sign_mul_abs,

Goal state after:
case mp
x y : EReal
habs : x.abs = y.abs
hsign : sign x = sign y
⊢ ↑(sign x) * ↑x.abs = ↑(sign y) * ↑y.abs
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: x y : EReal
⊢ x.abs = y.abs ∧ sign x = sign y ↔ x = y

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_4
f : α → ℝ≥0∞
hf : ∑' (x : α), f x ≠ ∞
⊢ Tendsto (fun s ↦ ∑' (b : { x // x ∉ s }), f ↑b) atTop (𝓝 0)

Tactic:
by

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

Goal state before:
pp: f g : ℕ → ℝ≥0∞
h₁ : ∑' (i : ℕ), g i ≠ ∞
h₂ : g ≤ f
this : ∀ (i : ℕ), f i - g i + g i = f i
⊢ ∑' (i : ℕ), (f i - g i) + ∑' (i : ℕ), g i = ∑' (i : ℕ), f i

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
g : β → ℝ≥0∞
⊢ ∑' (y : β), g y = ∑' (y : β), g (f (surjInv hf y))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
f : α → ℝ≥0∞
s : Set ι
t : ι → Set α
⊢ ⋃ i ∈ s, t i = ⋃ i, t ↑i

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
x : α
s : Set α
⊢ SemicontinuousWithinAt r s x ↔ ∀ (y : β), (∃ᶠ (x' : α) in 𝓝[s] x, ¬r x' y) → ¬r x y

Tactic:
by

Goal state after:
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 ≤ ∑ i, ∑' (x : ↑(t i)), f ↑x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
s : Set α
⊢ SemicontinuousOn r s ↔ ∀ x ∈ s, ∀ (y : β), (∃ᶠ (x' : α) in 𝓝[s] x, ¬r x' y) → ¬r x y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
x : α
⊢ SemicontinuousAt r x ↔ ∀ (y : β), (∃ᶠ (x' : α) in 𝓝 x, ¬r x' y) → ¬r x y

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
⊢ Semicontinuous r ↔ ∀ (x : α) (y : β), (∃ᶠ (x' : α) in 𝓝 x, ¬r x' y) → ¬r x y

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ι : Type u_4
a : ι → ℝ≥0∞
tsum_ne_top : ∑' (i : ι), a i ≠ ∞
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
⊢ {i | ε ≤ a i}.Finite

Tactic:
by

Goal state after:
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
hfg : ∀ᶠ (x : α) in 𝓝[s] a, ∀ (y : β), r x y ↔ r' x y
⊢ SemicontinuousWithinAt r' s a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
x : α
⊢ SemicontinuousWithinAt r univ x ↔ SemicontinuousAt r x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
⊢ SemicontinuousOn r univ ↔ Semicontinuous r

Tactic:
by

Goal state after:
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) * ε = ∑ _i ∈ hf.toFinset, ε

Tactic:
by

Goal state after:
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) ≤ c / ε

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
s : Set α
⊢ Semicontinuous (s.domRestrict r) ↔ SemicontinuousOn r s

Tactic:
by

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

Goal state before:
pp: β : Type u_2
γ : Type u_3
f : β → ℝ≥0∞
g : β → γ
⊢ ∑' (x : γ) (b : ↑(g ⁻¹' {x})), f ↑b = ∑' (i : β), f i

Tactic:
by

Goal state after:
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:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0∞
hsum : ∑' (x : α), f x ≠ ∞
⊢ HasSum (fun x ↦ (f x).toReal) (∑' (x : α), (f x).toReal)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
x : α
s : Set α
r' : α → β → Prop
h : SemicontinuousWithinAt r s x
h' : SemicontinuousWithinAt r' s x
⊢ SemicontinuousWithinAt (r ⊔ r') s x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
x : α
r' : α → β → Prop
h : SemicontinuousAt r x
h' : SemicontinuousAt r' x
⊢ SemicontinuousAt (r ⊔ r') x

Tactic:
by

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

Goal state before:
pp: x y : EReal
⊢ x ≤ y ↔
    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:
by

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

Goal state before:
pp: β : Type u_2
f : β → ℝ≥0
⊢ ∑' (b : β), f b = (∑' (b : β), ↑(f b)).toNNReal

Tactic:
by

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

Goal state before:
pp: x y z : EReal
⊢ x * y * z = x * (y * z)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace γ
inst✝ : Preorder β
f g : α → β
x : α
s t : Set α
y z : β
⊢ (Semicontinuous fun x1 x2 ↦ ¬f x1 ≤ x2) ↔ ∀ (x : α) (y : β), (∃ᶠ (x' : α) in 𝓝 x, f x' ≤ y) → f x ≤ y

Tactic:
by

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

Goal state before:
pp: β : Type u_2
f g : β → ℝ≥0
r : ℝ≥0
hgf : ∀ (b : β), g b ≤ f b
hfr : HasSum f r
⊢ ∑' (b : β), ↑(g b) ≤ ↑r

Tactic:
by

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

Goal state before:
pp: ⊢ Covariant { x // 0 < x } EReal (fun x y ↦ ↑x * y) fun x1 x2 ↦ x1 ≤ x2

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : Preorder β
f g : α → β
s : Set α
a : α
h : LowerSemicontinuousWithinAt f s a
has : a ∈ s
hfg : f =ᶠ[𝓝[s] a] g
⊢ ∀ᶠ (x : α) in 𝓝[s] a, ∀ (y : β), f x > y ↔ g x > y

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder β
f : α → β
x : α
s : Set α
⊢ LowerSemicontinuousWithinAt f s x ↔ ∀ (y : β), (∃ᶠ (x' : α) in 𝓝[s] x, f x' ≤ y) → f x ≤ y

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder β
f : α → β
s : Set α
⊢ LowerSemicontinuousOn f s ↔ ∀ x ∈ s, ∀ (y : β), (∃ᶠ (x' : α) in 𝓝[s] x, f x' ≤ y) → f x ≤ y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder β
f : α → β
x : α
⊢ LowerSemicontinuousAt f x ↔ ∀ (y : β), (∃ᶠ (x' : α) in 𝓝 x, f x' ≤ y) → f x ≤ y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder β
f : α → β
⊢ LowerSemicontinuous f ↔ ∀ (x : α) (y : β), (∃ᶠ (x' : α) in 𝓝 x, f x' ≤ y) → f x ≤ y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder β
f : α → β
x : α
s : Set α
⊢ UpperSemicontinuousWithinAt f s x ↔ ∀ (y : β), (∃ᶠ (x' : α) in 𝓝[s] x, f x' ≥ y) → f x ≥ y

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder β
f : α → β
s : Set α
⊢ UpperSemicontinuousOn f s ↔ ∀ x ∈ s, ∀ (y : β), (∃ᶠ (x' : α) in 𝓝[s] x, f x' ≥ y) → f x ≥ y

Tactic:
by

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

Goal state before:
pp: a✝ : EReal
n : ℕ
a : ℝ
ha : ↑a ≠ ⊤
⊢ ∃ m, ↑a * ↑n ≤ ↑m

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder β
f : α → β
x : α
⊢ UpperSemicontinuousAt f x ↔ ∀ (y : β), (∃ᶠ (x' : α) in 𝓝 x, f x' ≥ y) → f x ≥ y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder β
f : α → β
⊢ UpperSemicontinuous f ↔ ∀ (x : α) (y : β), (∃ᶠ (x' : α) in 𝓝 x, f x' ≥ y) → f x ≥ y

Tactic:
by

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

Goal state before:
pp: x y : EReal
⊢ min (-x) (-y) = -max x y

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x y : EReal
⊢ max (-x) (-y) = -min x y

Tactic:
by

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 : α
⊢ LowerHemicontinuousAt f x ↔
    ∀ (u : Set β), IsOpen[inst✝] u → (f x ∩ u).Nonempty → ∀ᶠ (x' : α) in 𝓝 x, (f x' ∩ u).Nonempty

Tactic:
by

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

Goal state before:
pp: ⊢ 0⁻¹ = 0

Tactic:
by

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

Goal state before:
pp: ⊢ 1⁻¹ = 1

Tactic:
by

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

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

Goal state before:
pp: a : EReal
⊢ (-a)⁻¹ = -a⁻¹

Tactic:
by

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

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

Goal state before:
pp: a : EReal
h : a ≠ ⊥
h' : a ≠ ⊤
⊢ a⁻¹⁻¹ = a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
s : Set α
a : α
h : LowerHemicontinuousWithinAt f s a
has : a ∈ s
hfg : f =ᶠ[𝓝[s] a] g
⊢ ∀ᶠ (x : α) in 𝓝[s] a, ∀ (y : Set β), IsOpen[inst✝] y ∧ (f x ∩ y).Nonempty ↔ IsOpen[inst✝] y ∧ (g x ∩ y).Nonempty

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℝ≥0
c : ℝ≥0
h : ∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ c
⊢ Summable f

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0
hf : Summable f
s : Set α
⊢ Summable (s.indicator f)

Tactic:
by

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

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

Tactic:
by

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 α
⊢ LowerHemicontinuousWithinAt f s x ↔ ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ t) → f x ⊆ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f g : α → ℝ≥0
sf sg : ℝ≥0
i : α
h : ∀ (a : α), f a ≤ g a
hi : f i < g i
hf : HasSum f sf
hg : HasSum g sg
⊢ sf < sg

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: a : EReal
⊢ ↑(sign a) * (↑a.abs)⁻¹ = a⁻¹

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0∞
hf : ∀ (a : α), f a ≠ ∞
⊢ (∑' (a : α), f a).toReal = ∑' (a : α), (f a).toReal

Tactic:
by

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 : α
⊢ LowerHemicontinuousAt f x ↔ ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝 x, f x' ⊆ t) → f x ⊆ t

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after: