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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PartialOrder α
h : ∀ {a b : α}, a < b → IsCompact (Icc a b)
a✝ : α
hab : a✝ ≤ a✝
⊢ IsCompact (Icc a✝ a✝)

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : ClosedIicTopology α
inst✝ : Nonempty β
f : β → α
hf : Continuous[inst✝², inst✝³] f
hlim : Tendsto f (cocompact β) atTop
⊢ ∃ x, ∀ (y : β), f x ≤ f y

Tactic:
inhabit β

Goal state after:
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : ClosedIicTopology α
inst✝ : Nonempty β
f : β → α
hf : Continuous[inst✝², inst✝³] f
hlim : Tendsto f (cocompact β) atTop
inhabited_h : Inhabited β
⊢ ∃ x, ∀ (y : β), f x ≤ f y
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a b : E
⊢ ‖1⁻¹ * (a / b)‖ = ‖(b / a)⁻¹ * 1‖

Tactic:
simp

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

Goal state before:
pp: case pos
α : Type u_2
E : Type u_5
inst✝ : SeminormedGroup E
s t : Set α
f : α → E
x : α
h✝¹ : x ∈ t
h✝ : x ∈ s
⊢ ‖(f x)⁻¹ * f x‖ = ‖f x / f x‖

Tactic:
simp

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

Goal state before:
pp: case neg
α : Type u_2
E : Type u_5
inst✝ : SeminormedGroup E
s t : Set α
f : α → E
x : α
h✝¹ : x ∈ t
h✝ : x ∉ s
⊢ ‖1⁻¹ * f x‖ = ‖1 / f x‖

Tactic:
simp

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

Goal state before:
pp: case pos
α : Type u_2
E : Type u_5
inst✝ : SeminormedGroup E
s t : Set α
f : α → E
x : α
h✝¹ : x ∉ t
h✝ : x ∈ s
⊢ ‖(f x)⁻¹‖ = ‖f x / 1‖

Tactic:
simp

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

Goal state before:
pp: case neg
α : Type u_2
E : Type u_5
inst✝ : SeminormedGroup E
s t : Set α
f : α → E
x : α
h✝¹ : x ∉ t
h✝ : x ∉ s
⊢ ‖1⁻¹‖ = ‖1 / 1‖

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst✝²] (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty
S : Set α := s ∩ Icc a b
ha : a ∈ S
Sbd : BddAbove S
c : α := sSup (s ∩ Icc a b)
c_mem : c ∈ S
c_le : c ≤ b
hc : c = b
⊢ b ∈ s

pp: case inr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst✝²] (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty
S : Set α := s ∩ Icc a b
ha : a ∈ S
Sbd : BddAbove S
c : α := sSup (s ∩ Icc a b)
c_mem : c ∈ S
c_le : c ≤ b
hc : c < b
⊢ b ∈ s

Tactic:
· exact hc ▸ c_mem.1

Goal state after:
case inr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst✝²] (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty
S : Set α := s ∩ Icc a b
ha : a ∈ S
Sbd : BddAbove S
c : α := sSup (s ∩ Icc a b)
c_mem : c ∈ S
c_le : c ≤ b
hc : c < b
⊢ b ∈ s
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
r : ℝ
a : E
⊢ a ∈ ball 1 r ↔ a ∈ {x | ‖x‖ < r}

Tactic:
simp

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
r : ℝ
⊢ a ∈ sphere 1 r ↔ ‖a‖ = r

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst✝²] (s ∩ Icc a b)
hb : b ∈ s
hgt : ∀ x ∈ s ∩ Ioc a b, ∀ y ∈ Iio x, (s ∩ Ico y x).Nonempty
⊢ Icc a b ⊆ s

Tactic:
intro y hy
  have : IsClosed (s ∩ Icc y b) := by
    suffices s ∩ Icc y b = s ∩ Icc a b ∩ Icc y b from this ▸ hs.inter isClosed_Icc
    grind [Icc_subset_Icc_left, inter_eq_self_of_subset_right, inter_assoc]
  exact IsClosed.mem_of_ge_of_forall_exists_lt this hb hy.2 fun x hx ↦
    hgt x ⟨hx.1, Ioc_subset_Ioc_left hy.1 hx.2⟩ y hx.2.1

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
⊢ (fun ε ↦ {y | ‖y‖ < ε}) = fun ε ↦ {y | ‖y⁻¹ * 1‖ < ε}

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Diam

Goal state before:
pp: case none
X : Type u_2
inst✝ : PseudoEMetricSpace X
ι : Type u_3
s : ι → Set X
⊢ ediam (⋃ i ∈ none, s i) = ⨆ i ∈ none, ediam (s i)

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Diam

Goal state before:
pp: case some
X : Type u_2
inst✝ : PseudoEMetricSpace X
ι : Type u_3
s : ι → Set X
val✝ : ι
⊢ ediam (⋃ i ∈ some val✝, s i) = ⨆ i ∈ some val✝, ediam (s i)

Tactic:
simp

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ ‖a ^ 0‖ ≤ ↑0 * ‖a‖

Tactic:
simp

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

Goal state before:
pp: E : Type u_8
inst✝¹ : TopologicalSpace E
inst✝ : ESeminormedMonoid E
hbot : (𝓝[≠] 1).NeBot
c : ℝ≥0∞
hc : c ≠ 0
⊢ ‖1‖ₑ = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I J I' J' : FractionalIdeal R⁰ K
H✝ : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
H : Submodule.map ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I = ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I
⊢ ↑(J' + spanSingleton R⁰ (I'.divMod I J') * I) ≤ ↑J' ⊔ ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I

Tactic:
simp

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

Goal state before:
pp: case refine_4
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I J I' J' : FractionalIdeal R⁰ K
H✝ : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
H : Submodule.map ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I = ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I
⊢ ↑I' ≤ ↑J' ⊔ ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I

Tactic:
exact le_trans (divMod_spec h' hJ' hI).ge (by simp)

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a : E
r : ℝ
x : E
⊢ x ∈ {x | x / a ∈ ball 1 r} ↔ ‖x / a‖ < r

Tactic:
simp

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a : E
r : ℝ
x : E
⊢ x ∈ {x | x / a ∈ closedBall 1 r} ↔ ‖x / a‖ ≤ r

Tactic:
simp

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a : E
r : ℝ
x : E
⊢ x ∈ {x | x / a ∈ sphere 1 r} ↔ ‖x / a‖ = r

Tactic:
simp

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ ‖a * b / a‖ < r ↔ ‖b‖ < r

Tactic:
simp

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ ‖a * b / a‖ ≤ r ↔ ‖b‖ ≤ r

Tactic:
simp

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
c : E
⊢ ‖b * c * (a * c)⁻¹‖ ≤ r ↔ ‖b * a⁻¹‖ ≤ r

Tactic:
simp

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
c : E
⊢ ‖b * c * (a * c)⁻¹‖ < r ↔ ‖b * a⁻¹‖ < r

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I J I' J' : FractionalIdeal R⁰ K
H✝ : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
H : Submodule.map ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I = ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I
⊢ ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I ≤ ↑(J' + spanSingleton R⁰ (I'.divMod I J') * I)

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
c : α
x✝ : Set α
⊢ (∃ r, x✝ ⊆ closedBall c r) ↔ ∃ i, True ∧ (closedBall c i)ᶜ ⊆ x✝ᶜ

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
c : α
x✝ : Set α
⊢ (∃ r, x✝ ⊆ ball c r) ↔ ∃ i, True ∧ (ball c i)ᶜ ⊆ x✝ᶜ

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
c : α
⊢ comap (dist c) atTop = cobounded α

Tactic:
simpa only [dist_comm _ c] using comap_dist_right_atTop c

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : IsDirectedOrder α
k : α
⊢ ∀ (c : α), 0 ≤ c → c ≤ c - k + k

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
⊢ Tendsto (fun x ↦ f x * r) l atTop

Tactic:
by
  refine tendsto_atTop.2 fun b => ?_
  obtain ⟨n : ℕ, hn : 1 ≤ n • r⟩ := Archimedean.arch 1 hr
  have hn' : 1 ≤ (n : R) * r := by rwa [nsmul_eq_mul] at hn
  filter_upwards [tendsto_atTop.1 hf (max b 0 * n)] with x hx
  calc
    b ≤ max b 0 * 1 := by
    { rw [mul_one]
      exact le_max_left _ _ }
    _ ≤ max b 0 * (n * r) := by gcongr
    _ = max b 0 * n * r := by rw [mul_assoc]
    _ ≤ f x * r := by gcongr

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

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

Tactic:
simp

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

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
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:
rw [closedBall_eq_empty.2 hr, Icc_eq_empty_of_lt]
    calc ⌊(x : ℝ) + r⌋₊ ≤ ⌊(x : ℝ)⌋₊ := floor_mono <| by linarith
    _ < ⌈↑x - r⌉₊ := by
      rw [floor_natCast, Nat.lt_ceil]
      linarith

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

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

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

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

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : InfConvergenceClass α
f : ι → α
a : α
h_anti : Antitone f
ha : IsGLB (range f) a
⊢ Tendsto f atTop (𝓝 a)

Tactic:
by convert! tendsto_atBot_isLUB h_anti.dual ha.dual using 1

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: ⊢ (-⊤).toReal = -⊤.toReal

Tactic:
simp

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

Goal state before:
pp: ⊢ (-⊥).toReal = -⊥.toReal

Tactic:
simp

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
⊢ ⊥ ∈ {a | ∀ᶠ (n : α) in ⊥, n ≤ a}

Tactic:
simp

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
⊢ ⊤ ∈ {a | ∀ᶠ (n : α) in ⊥, a ≤ n}

Tactic:
simp

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

Goal state before:
pp: case bot
⊢ ⊥ - ⊥ ≤ 0

Tactic:
simp

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

Goal state before:
pp: case coe
a✝ : ℝ
⊢ ↑a✝ - ↑a✝ ≤ 0

Tactic:
simp

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

Goal state before:
pp: case top
⊢ ⊤ - ⊤ ≤ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: case hinf
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
x y : α
r : ℝ≥0∞
h : LipschitzWith K f
hK : K ≠ 0
hr : edist x y < r
⊢ ↑K ≠ ∞

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
f : Filter α
inst✝ : f.NeBot
hc : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f
hb : IsBounded (fun x1 x2 ↦ x1 ≤ x2) f
⊢ ClusterPt f.limsSup f

Tactic:
by_cases! hn : Nontrivial α
  · by_cases! htop : ∀ x, x ≤ f.limsSup
    · let : OrderTop α := { top := f.limsSup, le_top := htop }
      exact nhds_top_basis.clusterPt_iff_frequently |>.mpr fun a => frequently_lt_of_lt_limsSup hc
    · by_cases! hbot : ∀ x, f.limsSup ≤ x
      · let : OrderBot α := { bot := f.limsSup, bot_le := hbot }
        refine nhds_bot_basis.clusterPt_iff_frequently |>.mpr fun a h => ?_
        exact lt_mem_sets_of_limsSup_lt hb h |>.frequently
      · refine (nhds_basis_Ioo' hbot htop).clusterPt_iff_frequently |>.mpr fun a ⟨hl, hg⟩ => ?_
        exact frequently_lt_of_lt_limsSup hc hl |>.and_eventually <| lt_mem_sets_of_limsSup_lt hb hg
  · simp_all [ClusterPt, Filter.eq_top_of_neBot]

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

Goal state before:
pp: case neg
x y : ℝ
hy : 0 ≤ ↑y
hxy : ¬x ≤ y
⊢ ENNReal.ofReal x - ENNReal.ofReal y = (↑x).toENNReal - (↑y).toENNReal

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β → γ
K₁ K₂ : ℝ≥0
s : Set α
t : Set β
hf₁ : ∀ b ∈ t, LipschitzOnWith K₁ (fun x ↦ f x b) s
hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t
⊢ Metric.ediam (image2 f s t) ≤ ↑K₁ * Metric.ediam s + ↑K₂ * Metric.ediam t

Tactic:
simp only [Metric.ediam_le_iff, forall_mem_image2]
  intro a₁ ha₁ b₁ hb₁ a₂ ha₂ b₂ hb₂
  refine (edist_triangle _ (f a₂ b₁) _).trans ?_
  exact
    add_le_add
      ((hf₁ b₁ hb₁ ha₁ ha₂).trans <| mul_right_mono <| Metric.edist_le_ediam_of_mem ha₁ ha₂)
      ((hf₂ a₂ ha₂ hb₁ hb₂).trans <| mul_right_mono <| Metric.edist_le_ediam_of_mem hb₁ hb₂)

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
h : x ∉ {x | {n | p n ∧ x ∈ s n}.Infinite}
⊢ x ∉ {x}ᶜ

Tactic:
simp

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

Goal state before:
pp: x y z t : EReal
h : x ≤ y
h' : z < t
hx_top : x ≠ ⊤
hy_bot : y ≠ ⊥
hy_top : y = ⊤
⊢ 0 ≠ ⊥

Tactic:
simp

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

Goal state before:
pp: x z t : EReal
h' : z < t
hx_top : x ≠ ⊤
y : ℝ
h : x ≤ ↑y
hy_bot : ↑y ≠ ⊥
hy_top : ¬↑y = ⊤
hxy : x = ↑y
htz_top : ¬t - z = ⊤
⊢ 0 ≠ ⊥

Tactic:
simp

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

Goal state before:
pp: case top_zero
⊢ (⊤ * 0).toReal = ⊤.toReal * toReal 0

Tactic:
simp

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

Goal state before:
pp: case zero_bot
⊢ (0 * ⊥).toReal = toReal 0 * ⊥.toReal

Tactic:
simp

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

Goal state before:
pp: case top_top
⊢ (⊤ * ⊤).toReal = ⊤.toReal * ⊤.toReal

Tactic:
simp

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

Goal state before:
pp: case top_bot
⊢ (⊤ * ⊥).toReal = ⊤.toReal * ⊥.toReal

Tactic:
simp

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

Goal state before:
pp: case bot_bot
⊢ (⊥ * ⊥).toReal = ⊥.toReal * ⊥.toReal

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Encodable.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
C : Set α → Prop
H0 : C ∅
H1 : ∀ (b : β), C (f b)
n : ℕ
b : β
⊢ ⋃ b_1 ∈ some b, f b_1 = f b

Tactic:
simp

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

Goal state before:
pp: case top_top
⊢ 0 < ⊤ * ⊤ ↔ 0 < ⊤ ∧ 0 < ⊤ ∨ ⊤ < 0 ∧ ⊤ < 0

Tactic:
simp

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

Goal state before:
pp: case top_zero
⊢ 0 < ⊤ * 0 ↔ 0 < ⊤ ∧ 0 < 0 ∨ ⊤ < 0 ∧ 0 < 0

Tactic:
simp

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

Goal state before:
pp: case top_bot
⊢ 0 < ⊤ * ⊥ ↔ 0 < ⊤ ∧ 0 < ⊥ ∨ ⊤ < 0 ∧ ⊥ < 0

Tactic:
simp

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

Goal state before:
pp: case zero_bot
⊢ 0 < 0 * ⊥ ↔ 0 < 0 ∧ 0 < ⊥ ∨ 0 < 0 ∧ ⊥ < 0

Tactic:
simp

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

Goal state before:
pp: case bot_bot
⊢ 0 < ⊥ * ⊥ ↔ 0 < ⊥ ∧ 0 < ⊥ ∨ ⊥ < 0 ∧ ⊥ < 0

Tactic:
simp

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

Goal state before:
pp: β : Type u_2
L : SummationFilter β
h : L.filter ≤ atTop
b : β
⊢ ∀ (a : Finset β), {b} ⊆ a → b ∈ a

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst✝ : L.LeAtTop
b : β
⊢ (fun x ↦ x ∈ L.support) b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst✝ : L.LeAtTop
⊢ ∀ᶠ (s : Finset β) in L.filter, ↑s ⊆ L.support

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst✝ : L.LeAtTop
f : γ ↪ β
⊢ (L.comap f).support = univ

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst✝ : L.LeAtTop
f : γ ↪ β
⊢ (L.comap f).filter ≤ atTop

Tactic:
by rw [← support_eq_univ_iff]; simp

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

Goal state before:
pp: case top_top
⊢ ⊤ * ⊤ = ⊤ ↔ ⊤ = ⊥ ∧ ⊤ < 0 ∨ ⊤ < 0 ∧ ⊤ = ⊥ ∨ ⊤ = ⊤ ∧ 0 < ⊤ ∨ 0 < ⊤ ∧ ⊤ = ⊤

Tactic:
simp

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

Goal state before:
pp: case top_zero
⊢ ⊤ * 0 = ⊤ ↔ ⊤ = ⊥ ∧ 0 < 0 ∨ ⊤ < 0 ∧ 0 = ⊥ ∨ ⊤ = ⊤ ∧ 0 < 0 ∨ 0 < ⊤ ∧ 0 = ⊤

Tactic:
simp

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

Goal state before:
pp: case top_bot
⊢ ⊤ * ⊥ = ⊤ ↔ ⊤ = ⊥ ∧ ⊥ < 0 ∨ ⊤ < 0 ∧ ⊥ = ⊥ ∨ ⊤ = ⊤ ∧ 0 < ⊥ ∨ 0 < ⊤ ∧ ⊥ = ⊤

Tactic:
simp

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

Goal state before:
pp: γ : Type u_3
β : Type u_4
f : γ ↪ β
s : Set (Finset γ)
t : Finset β
ht : ∀ (b : Finset β), t ⊆ b → b.preimage ⇑f ⋯ ∈ s
⊢ InjOn (⇑f) (⇑f ⁻¹' ↑t)

Tactic:
simp

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

Goal state before:
pp: case zero_bot
⊢ 0 * ⊥ = ⊤ ↔ 0 = ⊥ ∧ ⊥ < 0 ∨ 0 < 0 ∧ ⊥ = ⊥ ∨ 0 = ⊤ ∧ 0 < ⊥ ∨ 0 < 0 ∧ ⊥ = ⊤

Tactic:
simp

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

Goal state before:
pp: case bot_bot
⊢ ⊥ * ⊥ = ⊤ ↔ ⊥ = ⊥ ∧ ⊥ < 0 ∨ ⊥ < 0 ∧ ⊥ = ⊥ ∨ ⊥ = ⊤ ∧ 0 < ⊥ ∨ 0 < ⊥ ∧ ⊥ = ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
j0 : Subtype p
hj0 : BddBelow (range fun i ↦ f ↑i)
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
this : ∀ (j : Subtype p), Nonempty ↑(s ↑j)
A : ⋃ j, ⋂ i, Iic (f ↑i) = ⋃ j, ⋂ i, Iic (f ↑i)
⊢ ∀ (j : Subtype p), ⋂ i, Iic (f ↑i) = Iic (⨅ i, f ↑i)

Tactic:
intro j

Goal state after:
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
j0 : Subtype p
hj0 : BddBelow (range fun i ↦ f ↑i)
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
this : ∀ (j : Subtype p), Nonempty ↑(s ↑j)
A : ⋃ j, ⋂ i, Iic (f ↑i) = ⋃ j, ⋂ i, Iic (f ↑i)
j : Subtype p
⊢ ⋂ i, Iic (f ↑i) = Iic (⨅ i, f ↑i)