mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
a : α
⊢ Tendsto f (𝓝 a) (𝓝 (f a)) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, edist x a < δ → edist (f x) (f a) < ε

Tactic:
tendsto_nhds_nhds

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
a : α
⊢ (∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, edist x a < δ → edist (f x) (f a) < ε) ↔
    ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, edist x a < δ → edist (f x) (f a) < ε
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x y : ℝ
hy : 0 ≤ y
⊢ ENNReal.ofReal (x / y) ≤ ENNReal.ofReal x / ENNReal.ofReal y

Tactic:
div_eq_mul_inv,

Goal state after:
x y : ℝ
hy : 0 ≤ y
⊢ ENNReal.ofReal (x * y⁻¹) ≤ ENNReal.ofReal x * (ENNReal.ofReal y)⁻¹
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x y : ℝ
hy : 0 < y
⊢ ENNReal.ofReal (x / y) = ENNReal.ofReal x / ENNReal.ofReal y

Tactic:
div_eq_mul_inv,

Goal state after:
x y : ℝ
hy : 0 < y
⊢ ENNReal.ofReal (x * y⁻¹) = ENNReal.ofReal x / ENNReal.ofReal y
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x y : ℝ
hy : 0 < y
⊢ ENNReal.ofReal (x * y⁻¹) = ENNReal.ofReal x / ENNReal.ofReal y

Tactic:
div_eq_mul_inv,

Goal state after:
x y : ℝ
hy : 0 < y
⊢ ENNReal.ofReal (x * y⁻¹) = ENNReal.ofReal x * (ENNReal.ofReal y)⁻¹
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x y : ℝ
hy : 0 < y
⊢ ENNReal.ofReal (x * y⁻¹) = ENNReal.ofReal x * (ENNReal.ofReal y)⁻¹

Tactic:
ofReal_mul' (inv_nonneg.2 hy.le),

Goal state after:
x y : ℝ
hy : 0 < y
⊢ ENNReal.ofReal x * ENNReal.ofReal y⁻¹ = ENNReal.ofReal x * (ENNReal.ofReal y)⁻¹
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
⊢ (a / b).toNNReal = a.toNNReal / b.toNNReal

Tactic:
div_eq_mul_inv,

Goal state after:
a b : ℝ≥0∞
⊢ (a * b⁻¹).toNNReal = a.toNNReal / b.toNNReal
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
⊢ (a / b).toReal = a.toReal / b.toReal

Tactic:
div_eq_mul_inv,

Goal state after:
a b : ℝ≥0∞
⊢ (a * b⁻¹).toReal = a.toReal / b.toReal
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
c : ℝ≥0
⊢ ↑(nndist x y) < ↑c ↔ nndist x y < c

Tactic:
ENNReal.coe_lt_coe

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
c : ℝ≥0
⊢ nndist x y < c ↔ nndist x y < c
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
a : α
⊢ Tendsto f (𝓝 a) (𝓝 (f a)) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, dist x a < δ → dist (f x) (f a) < ε

Tactic:
tendsto_nhds_nhds

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
a : α
⊢ (∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, dist x a < δ → dist (f x) (f a) < ε) ↔
    ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, dist x a < δ → dist (f x) (f a) < ε
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
h : 0 ≤ ε
y : α
⊢ y ∈ closedEBall x (ENNReal.ofReal ε) ↔ y ∈ closedBall x ε

Tactic:
simp [edist_le_ofReal h]

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
p : HeightOneSpectrum R
hps : p ∈ s
⊢ J * ∏ x ∈ s \ {p}, x.asIdeal ≠ 0

Tactic:
mul_ne_zero_iff,

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
p : HeightOneSpectrum R
hps : p ∈ s
⊢ J ≠ 0 ∧ ∏ x ∈ s \ {p}, x.asIdeal ≠ 0
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✝
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
a c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : 1 ≠ 0
H : Ideal.span {↑c.den} * a.num ≤ c.num * Ideal.span {↑a.den}
⊢ Ideal.span {↑c.den} * a.num ≠ 0

Tactic:
by simpa using FractionalIdeal.num_eq_zero_iff.not.mpr ha

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: case inr.inl
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
x✝ : (b : β) → X b
h : 0 < 0 ∨ Nonempty β
this : Nonempty β := Or.resolve_left h (lt_irrefl 0)
inhabited_h : Inhabited β
x : (x : β) → X x
hx : ∀ (b : β), dist (x b) (x✝ b) ≤ 0
⊢ x ∈ Function.eval default ⁻¹' sphere (x✝ default) 0

Tactic:
exact le_antisymm (hx default) dist_nonneg

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
s : Set α
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : SecondCountableTopology β
hf : MonotoneOn f s
x : α
xs : x ∈ s
hx : x ∈ s → ∀ (z : β), f x < z → ∃ y ∈ s, x < y ∧ f y < z
u : β
hu : u > f x
v : α
vs : v ∈ s
xv : x < v
fvu : f v < u
this : s ∩ Ioo x v ∈ 𝓝[s ∩ Ioi x] x
y : α
hy : y ∈ s ∩ Ioo x v
⊢ f y < u

Tactic:
exact (hf hy.1 vs hy.2.2.le).trans_lt fvu

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

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 : ‖y‖ = 0
⊢ ‖x / y‖ = ‖x‖

Tactic:
div_eq_mul_inv,

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 / y‖ = ‖x‖

Tactic:
rw [div_eq_mul_inv, norm_mul_eq_norm_left]
  rwa [norm_inv']

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
r : ℝ
hr : r ≠ 0
x : ↑(sphere 1 r)
⊢ ‖↑x‖ ≠ 0

Tactic:
norm_eq_of_mem_sphere' x

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
r : ℝ
hr : r ≠ 0
x : ↑(sphere 1 r)
⊢ r ≠ 0
Module: Mathlib.Topology.EMetricSpace.Diam

Goal state before:
pp: α : Type u_1
X : Type u_2
inst✝ : PseudoEMetricSpace X
d : ℝ≥0∞
f : α → X
s : Set α
⊢ ediam (f '' s) ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) ≤ d

Tactic:
simp only [ediam_le_iff, forall_mem_image]

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 : α
⊢ map (fun a ↦ a + -k) atTop = atTop

Tactic:
apply map_add_atTop_eq

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

Goal state before:
pp: α : Type u
s : Set α
inst✝ : PseudoMetricSpace α
h : ¬Bornology.IsBounded s
⊢ (ediam s).toReal = 0

Tactic:
ediam_of_unbounded h,

Goal state after:
α : Type u
s : Set α
inst✝ : PseudoMetricSpace α
h : ¬Bornology.IsBounded s
⊢ ∞.toReal = 0
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:
rw [‹OrderTopology β›.topology_eq_generate_intervals, continuous_generateFrom_iff]
  rintro s ⟨a, rfl | rfl⟩
  · rw [e.preimage_Ioi]
    apply isOpen_lt'
  · rw [e.preimage_Iio]
    apply isOpen_gt'

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
h : LipschitzWith K f
x y : α
⊢ (↑K)⁻¹ * edist (f x) (f y) ≤ edist x y

Tactic:
rw [mul_comm, ← div_eq_mul_inv]

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
h : LipschitzWith K f
x y : α
⊢ edist (f x) (f y) / ↑K ≤ edist x y
Module: Mathlib.Topology.EMetricSpace.Lipschitz

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

Tactic:
by rw [← mul_assoc, ENNReal.coe_mul]

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

Goal state before:
pp: x y : EReal
hy : 0 ≤ y
⊢ (x - y).toENNReal = x.toENNReal - y.toENNReal

Tactic:
induction x <;> induction y <;> try {· simp_all [zero_tsub, ENNReal.sub_top]}

Goal state after:
case coe.coe
a✝¹ a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (↑a✝¹ - ↑a✝).toENNReal = (↑a✝¹).toENNReal - (↑a✝).toENNReal
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
u : β → α
a : α
⊢ ⨆ i ∈ f, ⨅ i_1 ∈ i, u i_1 ⊔ a = ⨆ s ∈ f, ⨅ a_1 ∈ s, a ⊔ u a_1

Tactic:
sup_comm (a := a)

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

Goal state before:
pp: a b c : EReal
ha : 0 ≤ a
ha' : a ≠ ⊤
⊢ a * (b - c) = a * b - a * c

Tactic:
rw [sub_eq_add_neg, left_distrib_of_nonneg_of_ne_top ha ha']
  simp [← neg_mul, sub_eq_add_neg]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_6
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
hu_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
hgu : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ g (u x)
hgu_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ g (u x)
hf : u = fun i ↦ g.symm (g (u i))
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ g.symm (g (u x))

Tactic:
simp_rw [g.symm_apply_apply]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_6
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
hu_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
hgu : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ g (u x)
hgu_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ g (u x)
hf : u = fun i ↦ g.symm (g (u i))
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ u x
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
L : SummationFilter β
f : β → α
inst✝¹ : T2Space α
inst✝ : L.NeBot
a₁ a₂ : α
⊢ HasProd f a₁ L → HasProd f a₂ L → a₁ = a₂

Tactic:
by
  exact tendsto_nhds_unique

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
⊢ HasProd (fun x ↦ 1) 1 L

Tactic:
by simp [HasProd, tendsto_const_nhds]

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

Goal state before:
pp: case e'_5
α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝⁴ : CommGroup α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalGroup α
f : β → α
a : α
inst✝¹ : L.LeAtTop
inst✝ : DecidableEq β
hf : HasProd f a L
b n : β
⊢ (if n = b then 1 else f n) = update f b 1 n

Tactic:
rw [Function.update_apply]

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

Goal state before:
pp: case neg
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst✝⁶ : CommMonoid α
inst✝⁵ : CommMonoid α'
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst✝¹ : FunLike G α α'
inst✝ : MonoidHomClass G α α'
hge : IsClosedEmbedding ⇑g
hL : L.NeBot
h : ¬Multipliable f L
⊢ g (∏'[L] (i : ι), f i) = ∏'[L] (i : ι), g (f i)

Tactic:
rw [tprod_eq_one_of_not_multipliable h, tprod_eq_one_of_not_multipliable, map_one]
      contrapose h
      -- need to show `g ∘ f` multipliable implies `g` multipliable
      simp only [Multipliable, HasProd] at h ⊢
      obtain ⟨b, hb⟩ := h
      obtain ⟨a, ha⟩ : b ∈ Set.range g :=
        hge.isClosed_range.mem_of_tendsto hb (.of_forall <| by simp [← _root_.map_prod])
      use a
      simp [hge.tendsto_nhds_iff, Function.comp_def, ha, hb]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : CommGroup α
inst✝¹ : IsUniformGroup α
f g : β → α
inst✝ : CompleteSpace α
hf : Multipliable f
h : ∀ (b : β), g b = 1 ∨ g b = f b
e : Set α
he : e ∈ 𝓝 1
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
t : Finset β
ht : Disjoint t s
b : β
hbt : b ∈ t
hb : b ∉ {b ∈ t | g b = f b}
⊢ g b = 1

Tactic:
simp only [Finset.mem_filter, and_iff_right hbt] at hb

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : CommGroup α
inst✝¹ : IsUniformGroup α
f g : β → α
inst✝ : CompleteSpace α
hf : Multipliable f
h : ∀ (b : β), g b = 1 ∨ g b = f b
e : Set α
he : e ∈ 𝓝 1
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
t : Finset β
ht : Disjoint t s
b : β
hbt : b ∈ t
hb : ¬g b = f b
⊢ g b = 1
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case neg
G : Type u_2
inst✝³ : CommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
f : ℕ → G
hf : ¬Multipliable f
n : ℕ
⊢ ¬Multipliable fun k ↦ f (k + n)

Tactic:
multipliable_nat_add_iff n

Goal state after:
case neg
G : Type u_2
inst✝³ : CommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
f : ℕ → G
hf : ¬Multipliable f
n : ℕ
⊢ ¬Multipliable f
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case refine_1.negSucc
M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
m : M
f : ℤ → M
hf : HasProd f m
this : Injective Int.negSucc
u : Finset ℤ
v' : Finset ℕ
hv' : u.preimage Nat.cast ⋯ ∪ u.preimage Int.negSucc ⋯ ⊆ v'
a✝ : ℕ
hx : Int.negSucc a✝ ∈ u
⊢ (∃ a ∈ v', ↑a = Int.negSucc a✝) ∨ ∃ a ∈ v', Int.negSucc a = Int.negSucc a✝

Tactic:
· exact Or.inr ⟨_, hv' (by simpa using Or.inr hx), rfl⟩

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : TopologicalSpace α
f : ι → α
a : α
h : HasSum (fun x ↦ ∏ i ∈ x, f i) a
⊢ HasProd (fun x ↦ 1 + f x) a

Tactic:
simp_rw [HasProd, prod_one_add]
  exact h.comp tendsto_finset_powerset_atTop_atTop

Goal state after:
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: ι : Sort u_1
inst✝ : Nonempty ι
n : ℕ
f : ι → ℝ≥0
⊢ (⨆ i, ↑(f i)) ^ n = ⨆ i, ↑(f i) ^ n

Tactic:
exact mod_cast NNReal.iSup_pow f n

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x y : α
⊢ (↑K)⁻¹ * edist x y ≤ edist (f x) (f y)

Tactic:
rw [mul_comm, ← div_eq_mul_inv]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x y : α
⊢ edist x y / ↑K ≤ edist (f x) (f y)
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
x y z : X
lxy lyz : List X
⊢ (zipWith d (x :: lxy ++ y :: lyz) (lxy ++ y :: lyz ++ [z])).sum =
    (zipWith d (x :: lxy) (lxy ++ [y])).sum + (zipWith d (y :: lyz) (lyz ++ [z])).sum

Tactic:
rw [← sum_append, ← zipWith_append, cons_append, ← @singleton_append _ y, append_assoc,
          append_assoc, append_assoc]

Goal state after:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
x y z : X
lxy lyz : List X
⊢ (x :: lxy).length = (lxy ++ [y]).length
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: E : Type u_4
inst✝ : SeminormedGroup E
⊢ Tendsto (fun a ↦ ‖a‖) (𝓝 1) (𝓝 0)

Tactic:
simpa using tendsto_norm_inv_mul_self (1 : E)

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

Goal state before:
pp: α : Type uα
inst✝⁴ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝³ : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
γ : Type uγ
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace γ
inst✝ : T0Space γ
f : β → γ
g : α → β
hf : UniformContinuous f
hg : UniformContinuous g
a : α
⊢ (pkg'.extend f ∘ pkg.map pkg' g) (pkg.coe a) = pkg.extend (f ∘ g) (pkg.coe a)

Tactic:
pkg.extend_coe (hf.comp hg),

Goal state after:
α : Type uα
inst✝⁴ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝³ : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
γ : Type uγ
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace γ
inst✝ : T0Space γ
f : β → γ
g : α → β
hf : UniformContinuous f
hg : UniformContinuous g
a : α
⊢ (pkg'.extend f ∘ pkg.map pkg' g) (pkg.coe a) = (f ∘ g) a
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ 0 ∨ b ≠ ∞
hb : b ≠ 0 ∨ a ≠ ∞
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))

Tactic:
by
  have ht : ∀ b : ℝ≥0∞, b ≠ 0 →
      Tendsto (fun p : ℝ≥0∞ × ℝ≥0∞ => p.1 * p.2) (𝓝 (∞, b)) (𝓝 ∞) := fun b hb => by
    refine tendsto_nhds_top_iff_nnreal.2 fun n => ?_
    rcases lt_iff_exists_nnreal_btwn.1 (pos_iff_ne_zero.2 hb) with ⟨ε, hε, hεb⟩
    have : ∀ᶠ c : ℝ≥0∞ × ℝ≥0∞ in 𝓝 (∞, b), ↑n / ↑ε < c.1 ∧ ↑ε < c.2 :=
      (lt_mem_nhds <| div_lt_top coe_ne_top hε.ne').prod_nhds (lt_mem_nhds hεb)
    refine this.mono fun c hc => ?_
    exact (ENNReal.div_mul_cancel hε.ne' coe_ne_top).symm.trans_lt (mul_lt_mul hc.1 hc.2)
  induction a with
  | top => simp only [ne_eq, or_false, not_true_eq_false] at hb; simp [ht b hb, top_mul hb]
  | coe a =>
    induction b with
    | top =>
      simp only [ne_eq, or_false, not_true_eq_false] at ha
      simpa [Function.comp_def, mul_comm, mul_top ha]
        using (ht a ha).comp (continuous_swap.tendsto (ofNNReal a, ∞))
    | coe b =>
      simp only [nhds_coe_coe, ← coe_mul, tendsto_coe, tendsto_map'_iff, Function.comp_def,
        tendsto_mul]

Goal state after:
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case inl.refine_1
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i ↦ ↑(Real.nnabs (x i))) l ≠ ∞
hbdd : ¬IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
q : ℚ
hq : R < ↑q
⊢ ∃ᶠ (i : ι) in l, x i < ↑q

Tactic:
refine fun hcon => hR ?_

Goal state after:
case inl.refine_1
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i ↦ ↑(Real.nnabs (x i))) l ≠ ∞
hbdd : ¬IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
q : ℚ
hq : R < ↑q
hcon : ∀ᶠ (x_1 : ι) in l, ¬(fun i ↦ x i < ↑q) x_1
⊢ ∀ᶠ (x_1 : ι) in l, ¬(fun n ↦ x n < R) x_1
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case inr.refine_2
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i ↦ ↑(Real.nnabs (x i))) l ≠ ∞
hbdd : ¬IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
q : ℚ
hq : ↑q < R
⊢ ∃ᶠ (i : ι) in l, ↑q < x i

Tactic:
refine fun hcon => hR ?_

Goal state after:
case inr.refine_2
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i ↦ ↑(Real.nnabs (x i))) l ≠ ∞
hbdd : ¬IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
q : ℚ
hq : ↑q < R
hcon : ∀ᶠ (x_1 : ι) in l, ¬(fun i ↦ ↑q < x i) x_1
⊢ ∀ᶠ (x_1 : ι) in l, ¬(fun n ↦ R < x n) x_1
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
⊢ ∃ U, (∀ (n : ℕ), (U n).IsSymm) ∧ (∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m) ∧ (𝓤 X).HasAntitoneBasis U

Tactic:
by
    rcases UniformSpace.has_seq_basis X with ⟨V, hB, hV_symm⟩
    rcases hB.subbasis_with_rel fun m =>
        hB.tendsto_smallSets.eventually
          (eventually_uniformity_iterate_comp_subset (hB.mem m) 2) with
      ⟨φ, -, hφ_comp, hφB⟩
    exact ⟨V ∘ φ, fun n => hV_symm _, hφ_comp, hφB⟩

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
⊢ LipschitzOnWith K f s ↔ ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ ↑K * dist x y

Tactic:
simp only [LipschitzOnWith, edist_nndist, dist_nndist]

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → ↑(nndist (f x) (f y)) ≤ ↑K * ↑(nndist x y)) ↔
    ∀ x ∈ s, ∀ y ∈ s, ↑(nndist (f x) (f y)) ≤ ↑K * ↑(nndist x y)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ι : Type u_4
u : Filter ι
f : ι → ℝ≥0∞
hf : Tendsto f u (𝓝 0)
g : ι → ℝ≥0∞
⊢ liminf (f + g) u = liminf g u

Tactic:
by
  rw [add_comm, liminf_add_of_right_tendsto_zero hf]

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

Goal state before:
pp: G : Type v
inst✝³ : Group G
inst✝² : PseudoEMetricSpace G
inst✝¹ : IsIsometricSMul G G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
a b c : G
⊢ edist (a / b) (a / c) = edist b c

Tactic:
div_eq_mul_inv,

Goal state after:
G : Type v
inst✝³ : Group G
inst✝² : PseudoEMetricSpace G
inst✝¹ : IsIsometricSMul G G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
a b c : G
⊢ edist (a * b⁻¹) (a / c) = edist b c
Module: Mathlib.Topology.MetricSpace.IsometricSMul

Goal state before:
pp: G : Type v
inst✝³ : Group G
inst✝² : PseudoEMetricSpace G
inst✝¹ : IsIsometricSMul G G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
a b c : G
⊢ edist (a * b⁻¹) (a / c) = edist b c

Tactic:
div_eq_mul_inv,

Goal state after:
G : Type v
inst✝³ : Group G
inst✝² : PseudoEMetricSpace G
inst✝¹ : IsIsometricSMul G G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
a b c : G
⊢ edist (a * b⁻¹) (a * c⁻¹) = edist b c
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
a b : E
⊢ dist a (a / b) = ‖b‖

Tactic:
div_eq_mul_inv,

Goal state after:
E : Type u_2
inst✝ : SeminormedCommGroup E
a b : E
⊢ dist a (a * b⁻¹) = ‖b‖
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝ : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
⊢ ‖w - z‖ * (‖z‖⁻¹ * ‖w‖⁻¹) = ‖w - z‖ / (‖z‖ * ‖w‖)

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u_2
inst✝ : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
⊢ ‖w - z‖ * (‖z‖⁻¹ * ‖w‖⁻¹) = ‖w - z‖ * (‖z‖ * ‖w‖)⁻¹
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
s : Set α
⊢ ediam s ≤ ediam (⇑f '' s) / ↑(ratio f)

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
s : Set α
⊢ ediam s ≤ ediam (⇑f '' s) * (↑(ratio f))⁻¹
Module: Mathlib.Analysis.Normed.Ring.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NonUnitalSeminormedRing α
x e : α × α
⊢ ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * (e.2 - x.2) + (e.1 - x.1) * x.2‖

Tactic:
mul_sub,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NonUnitalSeminormedRing α
x e : α × α
⊢ ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * e.2 - e.1 * x.2 + (e.1 - x.1) * x.2‖
Module: Mathlib.Analysis.Normed.MulAction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : SeminormedRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
x y : β
⊢ dist (s • x) (s • y) = ‖s‖ * dist x y

Tactic:
by
  simp_rw [dist_eq_norm, (norm_smul s (x - y)).symm, smul_sub]

Goal state after: