mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Archimedean

Goal state before:
pp: case inr
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)
hbot : H ≠ ⊥
⊢ ∃ b, H = closure {b}

Tactic:
·

Goal state after:
case inr
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)
hbot : H ≠ ⊥
⊢ ∃ b, H = closure {b}
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case inr.inl
R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : HeightOneSpectrum R
I : Ideal R
hI : I ≠ ⊥
⊢ emultiplicity p.asIdeal (I ⊔ ⊥) = min (emultiplicity p.asIdeal I) (emultiplicity p.asIdeal ⊥)

pp: case inr.inr
R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ emultiplicity p.asIdeal (I ⊔ J) = min (emultiplicity p.asIdeal I) (emultiplicity p.asIdeal J)

Tactic:
·

Goal state after:
case inr.inl
R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : HeightOneSpectrum R
I : Ideal R
hI : I ≠ ⊥
⊢ emultiplicity p.asIdeal (I ⊔ ⊥) = min (emultiplicity p.asIdeal I) (emultiplicity p.asIdeal ⊥)
Module: Mathlib.Topology.Order.MonotoneContinuity

Goal state before:
pp: case refine_1
α : 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
has : a ∈ s
b : β
hb : b < f a
⊢ ∀ᶠ (b_1 : α) in 𝓝[≥] a, b < f b_1

pp: case refine_2
α : 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
has : a ∈ s
b : β
hb : b > f a
⊢ ∀ᶠ (b_1 : α) in 𝓝[≥] a, f b_1 < b

Tactic:
·

Goal state after:
case refine_1
α : 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
has : a ∈ s
b : β
hb : b < f a
⊢ ∀ᶠ (b_1 : α) in 𝓝[≥] a, b < f b_1
Module: Mathlib.Topology.Order.MonotoneContinuity

Goal state before:
pp: case refine_2
α : 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
has : a ∈ s
b : β
hb : b > f a
⊢ ∀ᶠ (b_1 : α) in 𝓝[≥] a, f b_1 < b

Tactic:
·

Goal state after:
case refine_2
α : 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
has : a ∈ s
b : β
hb : b > f a
⊢ ∀ᶠ (b_1 : α) in 𝓝[≥] a, f b_1 < b
Module: Mathlib.Topology.Algebra.Ring.Real

Goal state before:
pp: case none
α : Type u
β : Type v
γ : Type w
b : ℝ≥0∞
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (none, b)

pp: case some
α : Type u
β : Type v
γ : Type w
b : ℝ≥0∞
a : ℝ≥0
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (some a, b)

Tactic:
·

Goal state after:
case none
α : Type u
β : Type v
γ : Type w
b : ℝ≥0∞
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (none, b)
Module: Mathlib.Topology.Algebra.Ring.Real

Goal state before:
pp: case some.none
α : Type u
β : Type v
γ : Type w
a : ℝ≥0
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (some a, none)

pp: case some.some
α : Type u
β : Type v
γ : Type w
a b : ℝ≥0
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (some a, some b)

Tactic:
·

Goal state after:
case some.none
α : Type u
β : Type v
γ : Type w
a : ℝ≥0
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (some a, none)
Module: Mathlib.Topology.Order.MonotoneContinuity

Goal state before:
pp: case refine_1
α : 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
has : a ∈ s
b : β
hb : b < f a
⊢ ∀ᶠ (b_1 : α) in 𝓝[≥] a, b < f b_1

pp: case refine_2
α : 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
has : a ∈ s
b : β
hb : b > f a
⊢ ∀ᶠ (b_1 : α) in 𝓝[≥] a, f b_1 < b

Tactic:
·

Goal state after:
case refine_1
α : 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
has : a ∈ s
b : β
hb : b < f a
⊢ ∀ᶠ (b_1 : α) in 𝓝[≥] a, b < f b_1
Module: Mathlib.Topology.Order.MonotoneContinuity

Goal state before:
pp: case refine_2
α : 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
has : a ∈ s
b : β
hb : b > f a
⊢ ∀ᶠ (b_1 : α) in 𝓝[≥] a, f b_1 < b

Tactic:
·

Goal state after:
case refine_2
α : 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
has : a ∈ s
b : β
hb : b > f a
⊢ ∀ᶠ (b_1 : α) in 𝓝[≥] a, f b_1 < b
Module: Mathlib.Topology.Order.MonotoneContinuity

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen[inst✝³] (⇑e ⁻¹' Ioi a)

pp: case inr
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen[inst✝³] (⇑e ⁻¹' Iio a)

Tactic:
·

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen[inst✝³] (⇑e ⁻¹' Ioi a)
Module: Mathlib.Topology.Order.MonotoneContinuity

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen[inst✝³] (⇑e ⁻¹' Iio a)

Tactic:
·

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen[inst✝³] (⇑e ⁻¹' Iio a)
Module: Mathlib.Topology.Instances.Nat

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

pp: case inr
x : ℕ
r : ℝ
hr : r < 0
⊢ closedBall x r = Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊

Tactic:
·

Goal state after:
case inl
x : ℕ
r : ℝ
hr : 0 ≤ r
⊢ closedBall x r = Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊
Module: Mathlib.Topology.Instances.Nat

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

Tactic:
·

Goal state after:
case inr
x : ℕ
r : ℝ
hr : r < 0
⊢ closedBall x r = Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊
Module: Mathlib.Topology.Instances.Rat

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

Tactic:
by
      simpa only [abs_sub_comm, dist_eq, cast_neg, neg_sub_neg] using h

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

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

pp: α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ∞
⊢ ∑ a ∈ s, f a ≠ ∞

Tactic:
·

Goal state after:
α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ∞
⊢ ∀ x ∈ s, f x = ↑(f x).toNNReal
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 ≠ ∞

Tactic:
·

Goal state after:
α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ∞
⊢ ∑ a ∈ s, f a ≠ ∞
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: case cons.refine_1
ι : 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
⊢ f j ≠ ∞

pp: case cons.refine_2
ι : 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
⊢ f j ≠ 0

Tactic:
·

Goal state after:
case cons.refine_1
ι : 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
⊢ f j ≠ ∞
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: case cons.refine_2
ι : 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
⊢ f j ≠ 0

Tactic:
·

Goal state after:
case cons.refine_2
ι : 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
⊢ f j ≠ 0
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: case mp
α : 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

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

Tactic:
·

Goal state after:
case mp
α : 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
Module: Mathlib.Order.Filter.IsBounded

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

Tactic:
·

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
⊢ (∃ s, BddAbove (u '' s) ∧ ∀ᶠ (x : β) in f, x ∈ s) → IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot
h : ⊥ ≠ ⊥
⊢ ⊤ + ⊥ = ⊤

pp: case coe
a✝ : ℝ
h : ↑a✝ ≠ ⊥
⊢ ⊤ + ↑a✝ = ⊤

pp: case top
h : ⊤ ≠ ⊥
⊢ ⊤ + ⊤ = ⊤

Tactic:
·

Goal state after:
case bot
h : ⊥ ≠ ⊥
⊢ ⊤ + ⊥ = ⊤
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe
a✝ : ℝ
h : ↑a✝ ≠ ⊥
⊢ ⊤ + ↑a✝ = ⊤

pp: case top
h : ⊤ ≠ ⊥
⊢ ⊤ + ⊤ = ⊤

Tactic:
·

Goal state after:
case coe
a✝ : ℝ
h : ↑a✝ ≠ ⊥
⊢ ⊤ + ↑a✝ = ⊤
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top
h : ⊤ ≠ ⊥
⊢ ⊤ + ⊤ = ⊤

Tactic:
·

Goal state after:
case top
h : ⊤ ≠ ⊥
⊢ ⊤ + ⊤ = ⊤
Module: Mathlib.Data.EReal.Operations

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

pp: case mpr
x : EReal
h : x ≠ ⊥
⊢ ⊤ + x = ⊤

Tactic:
·

Goal state after:
case mp
x : EReal
h : ⊤ + x = ⊤
⊢ x ≠ ⊥
Module: Mathlib.Data.EReal.Operations

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

Tactic:
·

Goal state after:
case mpr
x : EReal
h : x ≠ ⊥
⊢ ⊤ + x = ⊤
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: case inl
α : 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
tbot : IsBot t
⊢ ∃ l, ∃ᶠ (x : α) in f, l ≤ x

pp: case inr
α : 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
⊢ ∃ l, ∃ᶠ (x : α) in f, l ≤ x

Tactic:
·

Goal state after:
case inl
α : 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
tbot : IsBot t
⊢ ∃ l, ∃ᶠ (x : α) in f, l ≤ x
Module: Mathlib.Order.Filter.IsBounded

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

pp: case inr
α : Type u_1
f : Filter α
inst✝ : LinearOrder α
l : α
freq_ge : ∃ᶠ (x : α) in f, l ≤ x
l' : α
hl' : l' < l
⊢ IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f

Tactic:
·

Goal state after:
case inl
α : Type u_1
f : Filter α
inst✝ : LinearOrder α
l : α
freq_ge : ∃ᶠ (x : α) in f, l ≤ x
lbot : IsBot l
⊢ IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝⁴ : Preorder α
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
f : Filter ι
u v : ι → α
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∀ᶠ (x : ι) in f, v x ≤ V
x : ι
x_U : u x ≤ U
x_V : v x ≤ V
⊢ 0 x ≤ v x → (u * v) x ≤ U * V

Tactic:
v_0

Goal state after:
α : Type u_1
ι : Type u_4
inst✝⁴ : Preorder α
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
f : Filter ι
u v : ι → α
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∀ᶠ (x : ι) in f, v x ≤ V
x : ι
x_U : u x ≤ U
x_V : v x ≤ V
v_0 : 0 x ≤ v x
⊢ (u * v) x ≤ U * V
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot.bot
hx hy : 0 ≤ ⊥
⊢ (⊥ + ⊥).toENNReal = ⊥.toENNReal + ⊥.toENNReal

Tactic:
·

Goal state after:
case bot.bot
hx hy : 0 ≤ ⊥
⊢ (⊥ + ⊥).toENNReal = ⊥.toENNReal + ⊥.toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot.coe
hx : 0 ≤ ⊥
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (⊥ + ↑a✝).toENNReal = ⊥.toENNReal + (↑a✝).toENNReal

Tactic:
·

Goal state after:
case bot.coe
hx : 0 ≤ ⊥
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (⊥ + ↑a✝).toENNReal = ⊥.toENNReal + (↑a✝).toENNReal
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
h' : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)

Tactic:
·

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
h' : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot.top
hx : 0 ≤ ⊥
hy : 0 ≤ ⊤
⊢ (⊥ + ⊤).toENNReal = ⊥.toENNReal + ⊤.toENNReal

Tactic:
·

Goal state after:
case bot.top
hx : 0 ≤ ⊥
hy : 0 ≤ ⊤
⊢ (⊥ + ⊤).toENNReal = ⊥.toENNReal + ⊤.toENNReal
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
h' : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)

Tactic:
·

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
h' : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe.bot
a✝ : ℝ
hx : 0 ≤ ↑a✝
hy : 0 ≤ ⊥
⊢ (↑a✝ + ⊥).toENNReal = (↑a✝).toENNReal + ⊥.toENNReal

Tactic:
·

Goal state after:
case coe.bot
a✝ : ℝ
hx : 0 ≤ ↑a✝
hy : 0 ≤ ⊥
⊢ (↑a✝ + ⊥).toENNReal = (↑a✝).toENNReal + ⊥.toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe.coe
a✝¹ : ℝ
hx : 0 ≤ ↑a✝¹
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (↑a✝¹ + ↑a✝).toENNReal = (↑a✝¹).toENNReal + (↑a✝).toENNReal

Tactic:
·

Goal state after:
case coe.coe
a✝¹ : ℝ
hx : 0 ≤ ↑a✝¹
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (↑a✝¹ + ↑a✝).toENNReal = (↑a✝¹).toENNReal + (↑a✝).toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe.top
a✝ : ℝ
hx : 0 ≤ ↑a✝
hy : 0 ≤ ⊤
⊢ (↑a✝ + ⊤).toENNReal = (↑a✝).toENNReal + ⊤.toENNReal

Tactic:
·

Goal state after:
case coe.top
a✝ : ℝ
hx : 0 ≤ ↑a✝
hy : 0 ≤ ⊤
⊢ (↑a✝ + ⊤).toENNReal = (↑a✝).toENNReal + ⊤.toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top.bot
hx : 0 ≤ ⊤
hy : 0 ≤ ⊥
⊢ (⊤ + ⊥).toENNReal = ⊤.toENNReal + ⊥.toENNReal

Tactic:
·

Goal state after:
case top.bot
hx : 0 ≤ ⊤
hy : 0 ≤ ⊥
⊢ (⊤ + ⊥).toENNReal = ⊤.toENNReal + ⊥.toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top.coe
hx : 0 ≤ ⊤
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (⊤ + ↑a✝).toENNReal = ⊤.toENNReal + (↑a✝).toENNReal

Tactic:
·

Goal state after:
case top.coe
hx : 0 ≤ ⊤
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (⊤ + ↑a✝).toENNReal = ⊤.toENNReal + (↑a✝).toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top.top
hx hy : 0 ≤ ⊤
⊢ (⊤ + ⊤).toENNReal = ⊤.toENNReal + ⊤.toENNReal

Tactic:
·

Goal state after:
case top.top
hx hy : 0 ≤ ⊤
⊢ (⊤ + ⊤).toENNReal = ⊤.toENNReal + ⊤.toENNReal
Module: Mathlib.Topology.Order.MonotoneConvergence

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
b : α
hb : b < a
⊢ ∀ᶠ (b_1 : { x // x ∈ s }) in atTop, b < ↑b_1

pp: case refine_2
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
b : α
hb : b > a
⊢ ∀ᶠ (b_1 : { x // x ∈ s }) in atTop, ↑b_1 < b

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
b : α
hb : b < a
⊢ ∀ᶠ (b_1 : { x // x ∈ s }) in atTop, b < ↑b_1
Module: Mathlib.Topology.Order.MonotoneConvergence

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
b : α
hb : b > a
⊢ ∀ᶠ (b_1 : { x // x ∈ s }) in atTop, ↑b_1 < b

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
b : α
hb : b > a
⊢ ∀ᶠ (b_1 : { x // x ∈ s }) in atTop, ↑b_1 < b
Module: Mathlib.Topology.Order.MonotoneConvergence

Goal state before:
pp: case inl
α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : SupConvergenceClass α
f : ι → α
h_mono : Monotone f
hbdd : BddAbove (range f)
h : atTop = ⊥
⊢ Tendsto f atTop (𝓝 (⨆ i, f i))

pp: case inr
α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : SupConvergenceClass α
f : ι → α
h_mono : Monotone f
hbdd : BddAbove (range f)
h : atTop ≠ ⊥
⊢ Tendsto f atTop (𝓝 (⨆ i, f i))

Tactic:
·

Goal state after:
case inl
α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : SupConvergenceClass α
f : ι → α
h_mono : Monotone f
hbdd : BddAbove (range f)
h : atTop = ⊥
⊢ Tendsto f atTop (𝓝 (⨆ i, f i))
Module: Mathlib.Topology.Order.MonotoneConvergence

Goal state before:
pp: case inr
α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : SupConvergenceClass α
f : ι → α
h_mono : Monotone f
hbdd : BddAbove (range f)
h : atTop ≠ ⊥
⊢ Tendsto f atTop (𝓝 (⨆ i, f i))

Tactic:
·

Goal state after:
case inr
α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : SupConvergenceClass α
f : ι → α
h_mono : Monotone f
hbdd : BddAbove (range f)
h : atTop ≠ ⊥
⊢ Tendsto f atTop (𝓝 (⨆ i, f i))
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot.bot
⊢ (⊥ + ⊥).toENNReal ≤ ⊥.toENNReal + ⊥.toENNReal

Tactic:
·

Goal state after:
case bot.bot
⊢ (⊥ + ⊥).toENNReal ≤ ⊥.toENNReal + ⊥.toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot.coe
a✝ : ℝ
⊢ (⊥ + ↑a✝).toENNReal ≤ ⊥.toENNReal + (↑a✝).toENNReal

Tactic:
·

Goal state after:
case bot.coe
a✝ : ℝ
⊢ (⊥ + ↑a✝).toENNReal ≤ ⊥.toENNReal + (↑a✝).toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot.top
⊢ (⊥ + ⊤).toENNReal ≤ ⊥.toENNReal + ⊤.toENNReal

Tactic:
·

Goal state after:
case bot.top
⊢ (⊥ + ⊤).toENNReal ≤ ⊥.toENNReal + ⊤.toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe.bot
a✝ : ℝ
⊢ (↑a✝ + ⊥).toENNReal ≤ (↑a✝).toENNReal + ⊥.toENNReal

Tactic:
·

Goal state after:
case coe.bot
a✝ : ℝ
⊢ (↑a✝ + ⊥).toENNReal ≤ (↑a✝).toENNReal + ⊥.toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℝ
⊢ (↑a✝¹ + ↑a✝).toENNReal ≤ (↑a✝¹).toENNReal + (↑a✝).toENNReal

Tactic:
·

Goal state after:
case coe.coe
a✝¹ a✝ : ℝ
⊢ (↑a✝¹ + ↑a✝).toENNReal ≤ (↑a✝¹).toENNReal + (↑a✝).toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe.top
a✝ : ℝ
⊢ (↑a✝ + ⊤).toENNReal ≤ (↑a✝).toENNReal + ⊤.toENNReal

Tactic:
·

Goal state after:
case coe.top
a✝ : ℝ
⊢ (↑a✝ + ⊤).toENNReal ≤ (↑a✝).toENNReal + ⊤.toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top.bot
⊢ (⊤ + ⊥).toENNReal ≤ ⊤.toENNReal + ⊥.toENNReal

Tactic:
·

Goal state after:
case top.bot
⊢ (⊤ + ⊥).toENNReal ≤ ⊤.toENNReal + ⊥.toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top.coe
a✝ : ℝ
⊢ (⊤ + ↑a✝).toENNReal ≤ ⊤.toENNReal + (↑a✝).toENNReal

Tactic:
·

Goal state after:
case top.coe
a✝ : ℝ
⊢ (⊤ + ↑a✝).toENNReal ≤ ⊤.toENNReal + (↑a✝).toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top.top
⊢ (⊤ + ⊤).toENNReal ≤ ⊤.toENNReal + ⊤.toENNReal

Tactic:
·

Goal state after:
case top.top
⊢ (⊤ + ⊤).toENNReal ≤ ⊤.toENNReal + ⊤.toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case inl
y z t : EReal
h2 : z < t
h1 : ⊥ < y
⊢ ⊥ + z < y + t

pp: case inr
x y z t : EReal
h1 : x < y
h2 : z < t
hx : x ≠ ⊥
⊢ x + z < y + t

Tactic:
·

Goal state after:
case inl
y z t : EReal
h2 : z < t
h1 : ⊥ < y
⊢ ⊥ + z < y + t
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case inr
x y z t : EReal
h1 : x < y
h2 : z < t
hx : x ≠ ⊥
⊢ x + z < y + t

Tactic:
·

Goal state after:
case inr
x y z t : EReal
h1 : x < y
h2 : z < t
hx : x ≠ ⊥
⊢ x + z < y + t
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case inl
x y z : EReal
h : x < y
h' : z ≤ z
hbot : z ≠ ⊥
htop : z = ⊤ → z = ⊤ → x = ⊥
⊢ x + z < y + z

pp: case inr
x y z t : EReal
h : x < y
h' : z ≤ t
hbot : t ≠ ⊥
htop : t = ⊤ → z = ⊤ → x = ⊥
hlt : z < t
⊢ x + z < y + t

Tactic:
·

Goal state after:
case inl
x y z : EReal
h : x < y
h' : z ≤ z
hbot : z ≠ ⊥
htop : z = ⊤ → z = ⊤ → x = ⊥
⊢ x + z < y + z