mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a b : E
⊢ |‖a‖ - ‖b‖| ≤ ‖a⁻¹ * b‖

Tactic:
simpa using

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
a b : E
⊢ |‖a‖ - ‖b‖| ≤ ‖a⁻¹ * b‖
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a b : E
⊢ ‖a‖ - ‖b‖ ≤ ‖a * b‖

Tactic:
simpa using

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
a b : E
⊢ ‖a‖ ≤ ‖a * b‖ + ‖b‖
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖x‖ = 0
⊢ ‖x * y‖ ≤ ‖y‖

Tactic:
simpa using

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖x‖ = 0
⊢ ‖x * y‖ ≤ ‖y‖
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖x‖ = 0
⊢ ‖y‖ ≤ ‖x * y‖

Tactic:
simpa using

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖x‖ = 0
⊢ ‖y‖ ≤ ‖x * y‖
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖y‖ = 0
⊢ ‖x * y‖ ≤ ‖x‖

Tactic:
simpa using

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖y‖ = 0
⊢ ‖x * y‖ ≤ ‖x‖
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖y‖ = 0
⊢ ‖x‖ ≤ ‖x * y‖

Tactic:
simpa using

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖y‖ = 0
⊢ ‖x‖ ≤ ‖x * y‖
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖y‖ = 0
⊢ ‖x‖ ≤ ‖x * y‖

Tactic:
simpa [h] using norm_le_mul_norm_add x y

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
u v w : E
⊢ ‖u / w‖ - ‖v / w‖ ≤ ‖u / v‖

Tactic:
simpa using

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
u v w : E
⊢ ‖u / w‖ ≤ ‖u / v‖ + ‖v / w‖
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_8
inst✝ : SeminormedGroup E
u v : E
⊢ ‖u * v‖ - ‖u / v‖ ≤ 2 * ‖v‖

Tactic:
simpa using

Goal state after:
E : Type u_8
inst✝ : SeminormedGroup E
u v : E
⊢ ‖u * v‖ ≤ ‖u / v‖ + (‖v‖ + ‖v‖)
Module: Mathlib.Topology.MetricSpace.Cauchy

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
b : ℕ → ℝ
hb : ∀ (n : ℕ), 0 < b n
⊢ ∃ f, StrictMono f ∧ ∀ (n m : ℕ), m ≥ f n → dist (u m) (u (f n)) < b n

Tactic:
rw [cauchySeq_iff] at hu
  have hu' : ∀ k, ∀ᶠ (n : ℕ) in atTop, ∀ m ≥ n, dist (u m) (u n) < b k := by
    intro k
    rw [eventually_atTop]
    obtain ⟨N, hN⟩ := hu (b k) (hb k)
    exact ⟨N, fun m hm r hr => hN r (hm.trans hr) m hm⟩
  exact Filter.extraction_forall_of_eventually hu'

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
n : ℕ
⊢ ‖a ^ (n + 1)‖ ≤ ↑(n + 1) * ‖a‖

Tactic:
simpa using

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
a : E
n : ℕ
⊢ ‖a ^ n * a‖ ≤ ↑n * ‖a‖ + ‖a‖
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a b : E
⊢ ‖a / b‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ

Tactic:
simpa using

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
a b : E
⊢ ‖a / b‖₊ ≤ ‖a‖₊ + ‖b‖₊
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
x✝ : ∃ x, ‖x‖₊ ≠ 0
x : E
hx : ‖x‖₊ ≠ 0
⊢ ¬‖x⁻¹ * 1‖₊ = 0

Tactic:
simpa using

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
x✝ : ∃ x, ‖x‖₊ ≠ 0
x : E
hx : ‖x‖₊ ≠ 0
⊢ ¬‖x‖₊ = 0
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
⊢ IndiscreteTopology E ↔ ∀ (x : E), ‖x‖₊ = 0

Tactic:
simpa using

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
⊢ IndiscreteTopology E ↔ ∀ (x : E), ‖x‖₊ = 0
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
⊢ IndiscreteTopology E ↔ ∀ (x : E), ‖x‖ = 0

Tactic:
simpa using

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
⊢ IndiscreteTopology E ↔ ∀ (x : E), ‖x‖ = 0
Module: Mathlib.Topology.EMetricSpace.Diam

Goal state before:
pp: X : Type u_2
s t : Set X
inst✝ : PseudoEMetricSpace X
h : (s ∩ t).Nonempty
x : X
xs : x ∈ s
xt : x ∈ t
⊢ ediam (s ∪ t) ≤ ediam s + ediam t

Tactic:
simpa using

Goal state after:
X : Type u_2
s t : Set X
inst✝ : PseudoEMetricSpace X
h : (s ∩ t).Nonempty
x : X
xs : x ∈ s
xt : x ∈ t
⊢ ediam (s ∪ t) ≤ ediam s + ediam t
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst✝³] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := {t | t ∈ Icc a b ∧ Icc a t ⊆ s}
a_mem : a ∈ A
bdd_A : BddAbove A
t₁ : α := sSup A
t₁_mem : t₁ ∈ Icc a b
ht₁ : Icc a t₁ ⊆ s
t₁a : a ≤ t₁
t₁b : t₁ ≤ b
this : t₁ = b
⊢ Icc a b ⊆ s

Tactic:
simpa using

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst✝³] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := {t | t ∈ Icc a b ∧ Icc a t ⊆ s}
a_mem : a ∈ A
bdd_A : BddAbove A
t₁ : α := sSup A
t₁_mem : t₁ ∈ Icc a b
ht₁ : Icc a t₁ ⊆ s
t₁a : a ≤ t₁
t₁b : t₁ ≤ b
this : t₁ = b
⊢ Icc a b ⊆ s
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
f : Filter E
⊢ Disjoint (𝓝 1) f ↔ ∃ δ > 0, ∀ᶠ (y : E) in f, δ ≤ ‖y‖

Tactic:
simpa using

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
f : Filter E
⊢ Disjoint (𝓝 1) f ↔ ∃ δ, 0 < δ ∧ ∀ᶠ (y : E) in f, δ ≤ ‖y‖
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
⊢ ‖a⁻¹ * b‖ = ‖a / b‖

Tactic:
rw [← dist_eq_norm_inv_mul, dist_eq_norm_div]

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
h : ‖a⁻¹ * b‖ ≤ r
⊢ ↑n * ‖a⁻¹ * b‖ ≤ n • r

Tactic:
simpa using

Goal state after:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
n : ℕ
h : ‖a⁻¹ * b‖ ≤ r
⊢ ↑n * ‖a⁻¹ * b‖ ≤ ↑n * r
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
f : E → F
x : E
y : F
⊢ Tendsto f (𝓝 x) (𝓝 y) ↔ ∀ ε > 0, ∃ δ > 0, ∀ (x' : E), ‖x' / x‖ < δ → ‖f x' / y‖ < ε

Tactic:
simpa using

Goal state after:
E : Type u_5
F : Type u_6
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
f : E → F
x : E
y : F
⊢ Tendsto f (𝓝 x) (𝓝 y) ↔ ∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ (x' : E), ‖x' / x‖ < δ → ‖f x' / y‖ < ε
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
x : E
⊢ (𝓝 x).HasBasis (fun ε ↦ 0 < ε) fun ε ↦ {y | ‖y / x‖ < ε}

Tactic:
simpa using

Goal state after:
E : Type u_5
inst✝ : SeminormedCommGroup E
x : E
⊢ (𝓝 x).HasBasis (fun ε ↦ 0 < ε) fun ε ↦ {y | ‖y / x‖ < ε}
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
⊢ (𝓤 E).HasBasis (fun ε ↦ 0 < ε) fun ε ↦ {p | ‖p.1 / p.2‖ < ε}

Tactic:
simpa using

Goal state after:
E : Type u_5
inst✝ : SeminormedCommGroup E
⊢ (𝓤 E).HasBasis (fun ε ↦ 0 < ε) fun ε ↦ {p | ‖p.1 / p.2‖ < ε}
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : NormedGroup E
a : E
⊢ a = 1 ∨ 0 < ‖a‖

Tactic:
simpa using

Goal state after:
E : Type u_5
inst✝ : NormedGroup E
a : E
⊢ a = 1 ∨ ¬a = 1
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case h
R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsDedekindDomain R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : Algebra S R
inst✝³ : Algebra.IsIntegral S R
inst✝² : IsDomain S
inst✝¹ : Module.IsTorsionFree S R
p : Ideal S
inst✝ : p.IsMaximal
hp : p ≠ 0
h : map (algebraMap S R) p ≠ 0
hF : Fintype ↑{v | v.asIdeal ∣ map (algebraMap S R) p} := ⋯.fintype
v : HeightOneSpectrum R
hv : v ∈ mulSupport fun v ↦ v.maxPowDividing (map (algebraMap S R) p)
⊢ v ∈ ↑{v | v.asIdeal ∣ map (algebraMap S R) p}.toFinset

Tactic:
simpa using

Goal state after:
case h
R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsDedekindDomain R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : Algebra S R
inst✝³ : Algebra.IsIntegral S R
inst✝² : IsDomain S
inst✝¹ : Module.IsTorsionFree S R
p : Ideal S
inst✝ : p.IsMaximal
hp : p ≠ 0
h : map (algebraMap S R) p ≠ 0
hF : Fintype ↑{v | v.asIdeal ∣ map (algebraMap S R) p} := ⋯.fintype
v : HeightOneSpectrum R
hv : v ∈ mulSupport fun v ↦ v.maxPowDividing (map (algebraMap S R) p)
⊢ v.asIdeal ∣ map (algebraMap S R) p
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
⊢ ∏ᶠ (p : HeightOneSpectrum R), p.asIdeal ^ multiplicity p.asIdeal I = I

Tactic:
simpa using

Goal state after:
R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
⊢ ∏ᶠ (p : HeightOneSpectrum R), p.asIdeal ^ multiplicity p.asIdeal I = I
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
s : Set α
hs : x ∈ s ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ Bornology.IsBounded (s ∩ ball x 1) ∧ s ∩ ball x 1 ⊆ s

Tactic:
simpa using

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
s : Set α
hs : x ∈ s ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ Bornology.IsBounded (s ∩ ball x 1)
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
r : R
n : ℕ
hn : -r ≤ ↑n
⊢ ↑(-↑n) ≤ r

Tactic:
simpa using

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
r : R
n : ℕ
hn : -r ≤ ↑n
⊢ -r ≤ ↑n
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
c : α
x✝² x✝¹ : ℝ
hr : x✝² ≤ x✝¹
x✝ : α
⊢ x✝ ∈ (closedBall c x✝¹)ᶜ → x✝ ∈ (closedBall c x✝²)ᶜ

Tactic:
simpa using

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
c : α
x✝² x✝¹ : ℝ
hr : x✝² ≤ x✝¹
x✝ : α
⊢ x✝¹ < dist x✝ c → x✝² < dist x✝ c
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
c : α
x✝² x✝¹ : ℝ
hr : x✝² ≤ x✝¹
x✝ : α
⊢ x✝ ∈ (ball c x✝¹)ᶜ → x✝ ∈ (ball c x✝²)ᶜ

Tactic:
simpa using

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
c : α
x✝² x✝¹ : ℝ
hr : x✝² ≤ x✝¹
x✝ : α
⊢ x✝¹ ≤ dist x✝ c → x✝² ≤ dist x✝ c
Module: Mathlib.Topology.MetricSpace.Bounded

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

Tactic:
simpa using

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
c : α
⊢ comap (dist c) atTop = cobounded α
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
k : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f univ x
⊢ ∃ t, k ⊆ t ∧ IsOpen[inst✝] t ∧ Bornology.IsBounded (f '' t)

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
k : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f univ x
⊢ ∃ t, k ⊆ t ∧ IsOpen[inst✝] t ∧ Bornology.IsBounded (f '' t)
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

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

Tactic:
simpa using

Goal state after:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
hr : r < 0
hf : Tendsto f l atTop
⊢ Tendsto (fun x ↦ f x * r) l atBot
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

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

Tactic:
simpa using

Goal state after:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
hr : r < 0
hf : Tendsto f l atBot
⊢ Tendsto (fun x ↦ f x * r) l atTop
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

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

Tactic:
simpa using

Goal state after:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝³ : AddCommGroup R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
f : α → ℕ
hr : r < 0
hf : Tendsto f l atTop
⊢ Tendsto (fun x ↦ f x • r) l atBot
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

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

Tactic:
simpa using

Goal state after:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝³ : AddCommGroup R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
f : α → ℤ
hr : r < 0
hf : Tendsto f l atTop
⊢ Tendsto (fun x ↦ f x • r) l atBot
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

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

Tactic:
simpa using

Goal state after:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝³ : AddCommGroup R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
f : α → ℤ
hr : r < 0
hf : Tendsto f l atBot
⊢ Tendsto (fun x ↦ f x • r) l atTop
Module: Mathlib.Analysis.Normed.Group.Int

Goal state before:
pp: α : Type u_1
m n : ℤ
⊢ |↑m - ↑n| = |-↑m + ↑n|

Tactic:
rw [abs_sub_comm, neg_add_eq_sub]

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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : SeminormedCommGroup α
a : α
n : ℕ
⊢ ‖a ^ ↑n‖ ≤ ‖↑n‖ * ‖a‖

Tactic:
simpa using

Goal state after:
case inl
α : Type u_1
inst✝ : SeminormedCommGroup α
a : α
n : ℕ
⊢ ‖a ^ n‖ ≤ ↑n * ‖a‖
Module: Mathlib.Analysis.Normed.Group.Int

Goal state before:
pp: case inr
α : Type u_1
inst✝ : SeminormedCommGroup α
a : α
n : ℕ
⊢ ‖a ^ (-↑n)‖ ≤ ‖-↑n‖ * ‖a‖

Tactic:
simpa using

Goal state after:
case inr
α : Type u_1
inst✝ : SeminormedCommGroup α
a : α
n : ℕ
⊢ ‖a ^ n‖ ≤ ↑n * ‖a‖
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
s : Set α
inst✝ : PseudoMetricSpace α
t : Set α
x : α
xs : x ∈ s
xt : x ∈ t
⊢ diam (s ∪ t) ≤ diam s + diam t

Tactic:
simpa using

Goal state after:
α : Type u
s : Set α
inst✝ : PseudoMetricSpace α
t : Set α
x : α
xs : x ∈ s
xt : x ∈ t
⊢ diam (s ∪ t) ≤ diam s + diam t
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s n)
h's : ∀ (n : ℕ), Bornology.IsBounded (s n)
h : ∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty
h' : Tendsto (fun n ↦ diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N ↦ ⋯.some
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
⊢ CauchySeq u

Tactic:
apply cauchySeq_of_le_tendsto_0 _ _ h'

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s n)
h's : ∀ (n : ℕ), Bornology.IsBounded (s n)
h : ∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty
h' : Tendsto (fun n ↦ diam (s n)) atTop (𝓝 0)
u : ℕ → α := ⋯
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
⊢ ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ diam (s N)
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
⊢ 1 ≤ g / a ^ k

Tactic:
simpa using

Goal state after:
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 ^ k ≤ g
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:
simpa using

Goal state after:
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
Module: Mathlib.Topology.Algebra.Ring.Real

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

Tactic:
simpa using

Goal state after:
ε : ℝ
ε0 : ε > 0
x✝¹ x✝ : ℝ
h : dist x✝¹ x✝ < ε
⊢ |x✝¹ - x✝| < ε
Module: Mathlib.Topology.Instances.Rat

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

Tactic:
simpa using

Goal state after:
⊢ Pairwise fun x y ↦ 1 ≤ dist x y
Module: Mathlib.Topology.Instances.Rat

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

Tactic:
simpa using

Goal state after:
ε : ℝ
ε0 : ε > 0
x✝¹ x✝ : ℚ
h : dist x✝¹ x✝ < ε
⊢ |↑x✝¹ - ↑x✝| < ε
Module: Mathlib.Topology.Instances.Rat

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

Tactic:
simpa using

Goal state after:
ε : ℝ
ε0 : ε > 0
x✝¹ x✝ : ℚ
h : dist x✝¹ x✝ < ε
⊢ ||↑x✝¹| - |↑x✝|| ≤ |↑x✝¹ - ↑x✝|
Module: Mathlib.Topology.Instances.Rat

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

Tactic:
simpa using

Goal state after:
a b : ℚ
⊢ TotallyBounded (Icc a b)
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:
simpa using

Goal state after:
α : 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 ≤ b
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
k₀ : κ
s : Finset κ
k₀_notin_s : k₀ ∉ s
ih : (∀ k ∈ s, IsBoundedUnder r f (u k)) → IsBoundedUnder r f (∑ k ∈ s, u k)
h : IsBoundedUnder r f (u k₀) ∧ ∀ x ∈ s, IsBoundedUnder r f (u x)
⊢ IsBoundedUnder r f (∑ k ∈ Finset.cons k₀ s k₀_notin_s, u k)

Tactic:
simpa using

Goal state after:
α : 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
k₀ : κ
s : Finset κ
k₀_notin_s : k₀ ∉ s
ih : (∀ k ∈ s, IsBoundedUnder r f (u k)) → IsBoundedUnder r f (∑ k ∈ s, u k)
h : IsBoundedUnder r f (u k₀) ∧ ∀ x ∈ s, IsBoundedUnder r f (u x)
⊢ IsBoundedUnder r f (u k₀ + ∑ k ∈ s, u k)
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x : ℝ
x✝ : EReal
h : ↑x + x✝ ≤ ↑x + ⊥
⊢ x✝ ≤ ⊥

Tactic:
simpa using

Goal state after:
x : ℝ
x✝ : EReal
h : ↑x + x✝ ≤ ↑x + ⊥
⊢ x✝ = ⊥
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x y z : ℝ
h : ↑x + ↑y ≤ ↑x + ↑z
⊢ ↑y ≤ ↑z

Tactic:
simpa using

Goal state after:
x y z : ℝ
h : ↑x + ↑y ≤ ↑x + ↑z
⊢ y ≤ z
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x y : EReal
h : x < y
z : ℝ
⊢ ↑z + x < ↑z + y

Tactic:
simpa using

Goal state after:
x y : EReal
h : x < y
z : ℝ
⊢ x + ↑z < y + ↑z
Module: Mathlib.Topology.Order.MonotoneConvergence

Goal state before:
pp: case left
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : Preorder α
inst✝³ : OrderClosedTopology α
inst✝² : Preorder β
inst✝¹ : IsDirectedOrder β
inst✝ : Nonempty β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atTop (𝓝 a)
b : β
⊢ f b ≤ a

Tactic:
exact hf.ge_of_tendsto ha b

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: ι : Type u_6
α : Type u_7
β : Type u_8
inst✝ : ConditionallyCompleteLattice β
v : ι → α
u : α → β
f : Filter ι
g : Filter α
hv : Tendsto v f g
hvf : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (map v f) u
hg : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) g u
⊢ limsup u (map v f) ≤ limsup u g

Tactic:
exact limsup_le_limsup_of_le hv

Goal state after:
Module: Mathlib.Order.LiminfLimsup

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

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
⊢ ∀ (b : α), (∀ (x : α), x ≤ b) → b = ⊤
Module: Mathlib.Order.LiminfLimsup

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

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
⊢ ∀ (b : α), (∀ (x : α), b ≤ x) → b = ⊥
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: motive : EReal → Sort u_1
coe : (x : ℝ≥0∞) → motive ↑x
neg_coe : (x : ℝ≥0∞) → 0 < x → motive (-↑x)
x : EReal
hx : ¬0 ≤ x
⊢ 0 < -x

Tactic:
simpa using

Goal state after:
motive : EReal → Sort u_1
coe : (x : ℝ≥0∞) → motive ↑x
neg_coe : (x : ℝ≥0∞) → 0 < x → motive (-↑x)
x : EReal
hx : ¬0 ≤ x
⊢ x < 0
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
p : β → Prop
u : β → α
⊢ (blimsup u f fun x ↦ ¬p x) ⊔ blimsup u f p = limsup u f

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
p : β → Prop
u : β → α
⊢ (blimsup u f fun x ↦ ¬p x) ⊔ blimsup u f p = limsup u f
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
Kf : ℝ≥0
hf : LipschitzWith Kf f
g : α → γ
Kg : ℝ≥0
hg : LipschitzWith Kg g
x y : α
⊢ edist ((fun x ↦ (f x, g x)) x) ((fun x ↦ (f x, g x)) y) ≤ ↑(max Kf Kg) * edist x y

Tactic:
rw [ENNReal.coe_mono.map_max, Prod.edist_eq, max_mul]

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
Kf : ℝ≥0
hf : LipschitzWith Kf f
g : α → γ
Kg : ℝ≥0
hg : LipschitzWith Kg g
x y : α
⊢ max (edist ((fun x ↦ (f x, g x)) x).1 ((fun x ↦ (f x, g x)) y).1)
      (edist ((fun x ↦ (f x, g x)) x).2 ((fun x ↦ (f x, g x)) y).2) ≤
    max (↑Kf * edist x y) (↑Kg * edist x y)