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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
inst✝¹ : PseudoMetricSpace β
inst✝ : ProperSpace β
f : β → α
hf : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst✝³] f
x₀ : β
h : Bornology.IsBounded {x | f x ≤ f x₀}
⊢ ∃ x, ∀ (y : β), f x ≤ f y

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Archimedean

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
a : G
a_min : a ∈ lowerBounds {g | g ∈ H ∧ 1 < g}
a_in : a ∈ H
a_pos : 1 < a
g : G
g_in : g ∈ H
k : ℤ
right✝ : ∀ (y : ℤ), (fun k ↦ a ^ k ≤ g ∧ g < a ^ (k + 1)) y → y = k
nonneg : a ^ k ≤ g
lt : g < a ^ (k + 1)
h : ¬g / a ^ k = 1
⊢ a ≤ g / a ^ k

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Archimedean

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
a : G
a_min : a ∈ lowerBounds {g | g ∈ H ∧ 1 < g}
a_in : a ∈ H
a_pos : 1 < a
g : G
g_in : g ∈ H
k : ℤ
right✝ : ∀ (y : ℤ), (fun k ↦ a ^ k ≤ g ∧ g < a ^ (k + 1)) y → y = k
nonneg : a ^ k ≤ g
lt : g < a ^ (k + 1)
h✝ : ¬g / a ^ k = 1
h : a ≤ g / a ^ k
⊢ g / a ^ k < a

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Archimedean

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
a : G
a_min : a ∈ lowerBounds {g | g ∈ H ∧ 1 < g}
a_in : a ∈ H
a_pos : 1 < a
g : G
g_in : g ∈ H
k : ℤ
right✝ : ∀ (y : ℤ), (fun k ↦ a ^ k ≤ g ∧ g < a ^ (k + 1)) y → y = k
nonneg : a ^ k ≤ g
lt : g < a ^ (k + 1)
⊢ g / a ^ k = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Archimedean

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
a : G
ha : IsLeast {g | g ∈ H ∧ 1 < g} a
⊢ H = closure {a}

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
S : Subgroup G
hS : ∀ ε > 1, ∃ g ∈ S, g ∈ Ioo 1 ε
⊢ Dense ↑S

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
S : Subgroup G
hbot : S ≠ ⊥
H : ¬∃ a, IsLeast {g | g ∈ S ∧ 1 < g} a
⊢ Dense ↑S

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Archimedean

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
g : G
hg : g > 1
⊢ ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
S : Subgroup G
⊢ Dense ↑S ∨ ∃ a, S = closure {a}

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Archimedean

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
hex : ∀ g > 1, ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))
⊢ ∃ n, (↑H ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁷ : CommGroup G
inst✝⁶ : LinearOrder G
inst✝⁵ : IsOrderedMonoid G
inst✝⁴ : TopologicalSpace G
inst✝³ : OrderTopology G
inst✝² : MulArchimedean G
inst✝¹ : Nontrivial G
inst✝ : DenselyOrdered G
s : Subgroup G
⊢ Xor (Dense ↑s) (∃ a, s = zpowers a)

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁷ : CommGroup G
inst✝⁶ : LinearOrder G
inst✝⁵ : IsOrderedMonoid G
inst✝⁴ : TopologicalSpace G
inst✝³ : OrderTopology G
inst✝² : MulArchimedean G
inst✝¹ : Nontrivial G
inst✝ : DenselyOrdered G
s : Subgroup G
⊢ Dense ↑s ↔ ∀ (a : G), s ≠ zpowers a

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Archimedean

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
hex : ∀ g > 1, ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ n, (↑H ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬(↑H ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ ↑H
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
hxmin : ∀ (x : G), x ∈ H ∧ 1 < x → ∃ x_1, ∃ (_ : x_1 ∈ H ∧ 1 < x_1), x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 1 < y
m : ℕ
hm : a ^ m < y
hya : y ≤ a ^ (m + 1)
hnm : n ≤ m
⊢ a ^ (n + 1) ≤ a ^ (m + 1)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Archimedean

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
hex : ∀ g > 1, ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ n, (↑H ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬(↑H ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ ↑H
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
hxmin : ∀ (x : G), x ∈ H ∧ 1 < x → ∃ x_1, ∃ (_ : x_1 ∈ H ∧ 1 < x_1), x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 1 < y
m : ℕ
hm : a ^ m < y
hya : y ≤ a ^ (m + 1)
hnm : n ≤ m
⊢ a ^ m * a < y * a

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Archimedean

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
⊢ ∃ b, IsLeast {g | g ∈ H ∧ 1 < g} b

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Archimedean

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
⊢ ∃ b, H = closure {b}

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Archimedean

Goal state before:
pp: H : AddSubgroup ℤ
this : Ioo 0 1 = ∅
⊢ Disjoint (↑H) (Ioo 0 1)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bornology.Real

Goal state before:
pp: ⊢ ∀ (r : ℝ), BddBelow (closedBall 0 r)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bornology.Real

Goal state before:
pp: ⊢ ∀ (r : ℝ), BddAbove (closedBall 0 r)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bornology.Real

Goal state before:
pp: r : ℝ
⊢ BddAbove (closedBall 0 r)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.Real

Goal state before:
pp: ⊢ CompleteSpace ℝ

Tactic:
by

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

Goal state before:
pp: ε : ℝ
ε0 : ε > 0
x✝¹ x✝ : ℝ
h : dist x✝¹ x✝ < ε
⊢ dist (-x✝¹) (-x✝) < ε

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
⊢ IsTopologicalAddGroup ℝ

Tactic:
by

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

Goal state before:
pp: ⊢ (range ofNNReal).OrdConnected

Tactic:
by

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

Goal state before:
pp: ⊢ IsOpen (range ofNNReal)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
⊢ ContinuousAdd ℝ≥0∞

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.MonotoneContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b
⊢ ContinuousWithinAt f (Ici a) a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.MonotoneContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b
⊢ ContinuousWithinAt f (Ici a) a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.MonotoneContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : closure[inst✝²] (f '' s) ∈ 𝓝[≥] f a
⊢ ContinuousWithinAt f (Ici a) a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ I ⊔ J ≠ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.MonotoneContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : DenselyOrdered β
f : α → β
h_mono : Monotone f
h_dense : DenseRange f
a : α
⊢ closure[inst✝²] (f '' univ) ∈ 𝓝 (f a)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.MonotoneContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
⊢ Continuous[inst✝³, inst✝²] ⇑e

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.Nat

Goal state before:
pp: x : ℕ
r : ℝ
hr : r < 0
⊢ ↑x + r ≤ ↑x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.Nat

Goal state before:
pp: x : ℕ
r : ℝ
hr : r < 0
⊢ ⌊↑x⌋₊ < ⌈↑x - r⌉₊

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.Nat

Goal state before:
pp: x : ℕ
r : ℝ
⊢ closedBall x r = Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.Nat

Goal state before:
pp: x : ℕ
r : ℝ
⊢ IsCompact (closedBall x r)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.Nat

Goal state before:
pp: ⊢ ∀ (r : ℝ), BddBelow (closedBall 0 r)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.Nat

Goal state before:
pp: ⊢ ∀ (r : ℝ), BddAbove (closedBall 0 r)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.Nat

Goal state before:
pp: ⊢ (cocompact ℕ).NeBot

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Rat

Goal state before:
pp: r₁ r₂ : ℚ
⊢ dist r₁ r₂ = ‖↑(-r₁ + r₂)‖

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.Rat

Goal state before:
pp: x y : ℕ
⊢ dist ↑x ↑y = dist x y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.Rat

Goal state before:
pp: ⊢ Pairwise fun x y ↦ 1 ≤ dist ↑x ↑y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.Rat

Goal state before:
pp: x y : ℤ
⊢ dist ↑x ↑y = dist x y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Rat

Goal state before:
pp: m : ℤ
⊢ ‖↑m‖ = ‖m‖

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.Rat

Goal state before:
pp: ⊢ UniformContinuous (Rat.cast ∘ fun p ↦ p.1 + p.2)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.Rat

Goal state before:
pp: ε : ℝ
ε0 : ε > 0
x✝¹ x✝ : ℚ
h : dist x✝¹ x✝ < ε
⊢ dist (-x✝¹) (-x✝) < ε

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.Rat

Goal state before:
pp: ε : ℝ
ε0 : ε > 0
x✝¹ x✝ : ℚ
h : dist x✝¹ x✝ < ε
⊢ dist |x✝¹| |x✝| ≤ dist x✝¹ x✝

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.Rat

Goal state before:
pp: a b : ℚ
⊢ TotallyBounded (Icc a b)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.Rat

Goal state before:
pp: ⊢ Continuous fun p ↦ max (↑p.1 - ↑p.2) 0

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.Rat

Goal state before:
pp: R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : MulAction ℚ R
inst✝² : MulAction ℚ≥0 R
inst✝¹ : IsScalarTower ℚ≥0 ℚ R
inst✝ : ContinuousSMul ℚ R
⊢ Continuous[instTopologicalSpaceProd, inst✝⁴] fun p ↦ p.1 • p.2

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.Rat

Goal state before:
pp: ⊢ Continuous fun p ↦ p.1 • ↑p.2

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: α : Type u_3
s : Finset α
f : α → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
⊢ ENNReal.ofReal (∏ i ∈ s, f i) = ∏ i ∈ s, ENNReal.ofReal (f i)

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: ι : Type u_3
α : Type u_4
f : ι → α → ℝ≥0∞
s : Finset α
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
⊢ ⨅ i, ∑ a ∈ s, f i a = ∑ a ∈ s, ⨅ i, f i a

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.BigOperators

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.BigOperators

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
⊢ ENNReal.ofReal (∑ i ∈ s, f i) = ∑ i ∈ s, ENNReal.ofReal (f i)

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: α : Type u_1
s : Finset α
hs : s.Nonempty
f g : α → ℝ≥0∞
Hlt : ∀ i ∈ s, f i < g i
⊢ ∑ i ∈ s, f i < ∑ i ∈ s, g i

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: α : Type u_1
s : Finset α
hs : s.Nonempty
f g : α → ℝ≥0∞
Hle : ∑ i ∈ s, f i ≤ ∑ i ∈ s, g i
⊢ ∃ i ∈ s, f i ≤ g i

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: ι : Type u_1
f : ι → ℝ≥0∞
s✝ : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
ih : ((↑s).Pairwise fun i j ↦ f i ≠ 0 ∨ f j ≠ ∞) → (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹
hf : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ f i ≠ 0 ∨ f j ≠ ∞
⊢ ↑s ⊆ ↑(Finset.cons i s hi)

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: ι : Type u_1
f : ι → ℝ≥0∞
s✝ : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
ih : ((↑s).Pairwise fun i j ↦ f i ≠ 0 ∨ f j ≠ ∞) → (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹
hf : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ f i ≠ 0 ∨ f j ≠ ∞
hi₀ : f i = 0
j : ι
hj : j ∈ s
⊢ i ∈ ↑(Finset.cons i s hi)

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: ι : Type u_1
f : ι → ℝ≥0∞
s✝ : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
ih : ((↑s).Pairwise fun i j ↦ f i ≠ 0 ∨ f j ≠ ∞) → (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹
hf : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ f i ≠ 0 ∨ f j ≠ ∞
hi₀ : f i = 0
j : ι
hj : j ∈ s
⊢ j ∈ ↑(Finset.cons i s hi)

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: ι : Type u_1
f : ι → ℝ≥0∞
s✝ : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
ih : ((↑s).Pairwise fun i j ↦ f i ≠ 0 ∨ f j ≠ ∞) → (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹
hf : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ f i ≠ 0 ∨ f j ≠ ∞
hi₀ : f i = ∞
j : ι
hj : j ∈ s
⊢ j ∈ ↑(Finset.cons i s hi)

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: ι : Type u_1
f : ι → ℝ≥0∞
s✝ : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
ih : ((↑s).Pairwise fun i j ↦ f i ≠ 0 ∨ f j ≠ ∞) → (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹
hf : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ f i ≠ 0 ∨ f j ≠ ∞
hi₀ : f i = ∞
j : ι
hj : j ∈ s
⊢ i ∈ ↑(Finset.cons i s hi)

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: ι : Type u_1
f : ι → ℝ≥0∞
s : Finset ι
hf : (↑s).Pairwise fun i j ↦ f i ≠ 0 ∨ f j ≠ ∞
⊢ (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: ι : Type u_1
f g : ι → ℝ≥0∞
s : Finset ι
hg : (↑s).Pairwise fun i j ↦ g i ≠ 0 ∨ g j ≠ ∞
⊢ ∏ i ∈ s, f i / g i = (∏ i ∈ s, f i) / ∏ i ∈ s, g i

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: ι : Type u_1
f g : ι → ℝ≥0∞
s : Finset ι
hg : ∀ i ∈ s, g i ≠ ∞
⊢ (↑s).Pairwise fun i j ↦ g i ≠ 0 ∨ g j ≠ ∞

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: ι : Type u_1
f g : ι → ℝ≥0∞
s : Finset ι
hg : ∀ i ∈ s, g i ≠ 0
⊢ (↑s).Pairwise fun i j ↦ g i ≠ 0 ∨ g j ≠ ∞

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: ι : Type u_1
α : Type u_2
s : Finset α
f : α → ι → ℝ≥0∞
hf : ∀ (i j : ι), ∃ k, ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
⊢ ∑ a ∈ s, ⨆ i, f a i = ⨆ i, ∑ a ∈ s, f a i

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ IsBounded r ⊥ ↔ Nonempty α

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ IsBounded r ⊤ ↔ ∃ t, ∀ (x : α), r x t

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
⊢ IsBounded r (𝓟 s) ↔ ∃ t, ∀ x ∈ s, r x t

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Preorder β
l : Filter α
u v : α → β
hu : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l u
hv : v ≤ᶠ[l] u
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l v

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
h : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
⊢ ∃ a, ∀ᶠ (x : β) in f, u x ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
b : α
hb : ∀ᶠ (x : α) in map u f, (fun x1 x2 ↦ x1 ≤ x2) x b
⊢ b ∈ upperBounds (u '' {a | u a ≤ b})

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
s : Set β
hs : ∀ᶠ (x : β) in f, x ∈ s
b : α
hb : b ∈ upperBounds (u '' s)
⊢ ∀ x ∈ s, u x ∈ {x | (fun x ↦ (fun x1 x2 ↦ x1 ≤ x2) x b) x}

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u ↔ ∃ s, BddAbove (u '' s) ∧ ∀ᶠ (x : β) in f, x ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
hu : BddAbove (range u)
⊢ BddAbove (u '' univ)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
f : α → β
l : Filter α
inst✝ : l.NeBot
hf : Tendsto f l atTop
⊢ ¬IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l f

Tactic:
by

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

Goal state before:
pp: x y : EReal
⊢ ⊥ < x + y ↔ ⊥ < x ∧ ⊥ < y

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) cofinite f
⊢ BddAbove (range f)

Tactic:
by

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

Goal state before:
pp: x : EReal
h : x ≠ ⊥
⊢ ⊤ + x = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: β : Type u_2
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : ℕ → β
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop f
⊢ BddAbove (range f)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ IsCobounded r ⊥ ↔ ∃ b, ∀ (x : α), r b x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ IsCobounded r ⊤ ↔ Nonempty α

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
⊢ IsCobounded r (𝓟 s) ↔ ∃ b, ∀ (a : α), (∀ x ∈ s, r x a) → r b a

Tactic:
by

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

Goal state before:
pp: x : EReal
⊢ ⊤ + x = ⊤ ↔ x ≠ ⊥

Tactic:
by

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

Goal state before:
pp: x : EReal
h : x ≠ ⊥
⊢ x + ⊤ = ⊤

Tactic:
by

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

Goal state before:
pp: x : EReal
⊢ x + ⊤ = ⊤ ↔ x ≠ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
f : Filter α
inst✝¹ : LinearOrder α
inst✝ : f.NeBot
t : α
ht : ∀ (a : α), (∀ᶠ (x : α) in f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) t a
t' : α
ht' : t' < t
ev : ∀ᶠ (x : α) in f, ¬(fun x ↦ t' ≤ x) x
⊢ ∀ᶠ (x : α) in f, (fun x1 x2 ↦ x1 ≤ x2) x t'

Tactic:
by

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

Goal state before:
pp: x y : EReal
hx : x ≠ ⊤
h'x : x ≠ ⊥
hy : y ≠ ⊤
h'y : y ≠ ⊥
⊢ (x + y).toReal = x.toReal + y.toReal

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
f : Filter α
inst✝¹ : LinearOrder α
inst✝ : f.NeBot
cobdd : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f
⊢ ∃ l, ∃ᶠ (x : α) in f, l ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
f : Filter α
inst✝ : LinearOrder α
l : α
freq_ge : ∃ᶠ (x : α) in f, l ≤ x
⊢ IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_5
f : Filter α
R : Type u_6
κ : Type u_7
inst✝ : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
h : ∀ k ∈ ∅, IsBoundedUnder r f (u k)
⊢ ∀ᶠ (x : R) in map 0 f, r x 0

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_5
f : Filter α
R : Type u_6
κ : Type u_7
inst✝ : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
s : Finset κ
h : ∀ k ∈ s, IsBoundedUnder r f (u k)
⊢ IsBoundedUnder r f (∑ k ∈ s, u k)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_5
f : Filter α
R : Type u_6
inst✝³ : Preorder R
inst✝² : Add R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
u v : α → R
u_bdd_le : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
v_bdd_le : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (u + v)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_5
R : Type u_6
inst✝⁴ : LinearOrder R
inst✝³ : Add R
f : Filter α
inst✝² : f.NeBot
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
u v : α → R
hu : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) f u
hv : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (u + v)

Tactic:
by

Goal state after: