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

Goal state before:
pp: α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
u : Set α
hu : u ∈ 𝓝 x
⊢ ∀ᶠ (r : ℝ) in 𝓝 0, closedBall x r ⊆ u

Tactic:
obtain ⟨ε, εpos, hε⟩ : ∃ ε, 0 < ε ∧ closedBall x ε ⊆ u := nhds_basis_closedBall.mem_iff.1 hu

Goal state after:
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
u : Set α
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
⊢ ∀ᶠ (r : ℝ) in 𝓝 0, closedBall x r ⊆ u
Module: Mathlib.Topology.MetricSpace.Basic

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : PseudoMetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ toUniformSpace = toUniformSpace

Tactic:
by
  dsimp +instances [replaceDist]

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : PseudoMetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ toBornology = toBornology

Tactic:
by
  dsimp +instances [replaceDist]

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

Goal state before:
pp: α✝ : Type u_1
s✝ t : Set α✝
inst✝⁵ : Bornology α✝
inst✝⁴ : Preorder α✝
inst✝³ : IsOrderBornology α✝
ι : Type u_2
α : ι → Type u_3
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : (i : ι) → Bornology (α i)
inst✝ : ∀ (i : ι), IsOrderBornology (α i)
s : Set ((i : ι) → α i)
⊢ IsBounded s ↔ BddBelow s ∧ BddAbove s

Tactic:
by
    simp_rw [← forall_isBounded_image_eval_iff, bddBelow_pi, bddAbove_pi, ← forall_and,
      isBounded_iff_bddBelow_bddAbove]

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✝ : SecondCountableTopology α
hf : MonotoneOn f s
a✝ : Nontrivial α
t : Set β := {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : β → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
H : (x '' t).Countable
this : InjOn x t
⊢ {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}.Countable

Tactic:
exact countable_of_injective_of_countable_image this H

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

Goal state before:
pp: case refine_1
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : CompactIccSpace α
s : Set α
hs : s ∈ atBot ⊔ atTop
h✝ : IsEmpty α
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ s

pp: case refine_2
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : CompactIccSpace α
s : Set α
hs : s ∈ atBot ⊔ atTop
h✝ : Nonempty α
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ s

Tactic:
· exact ⟨∅, isCompact_empty, fun x _ ↦ (IsEmpty.false x).elim⟩

Goal state after:
case refine_2
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : CompactIccSpace α
s : Set α
hs : s ∈ atBot ⊔ atTop
h✝ : Nonempty α
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ s
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: case refine_1
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTop α
inst✝ : CompactIccSpace α
x✝ : Set α
hs : x✝ ∈ atBot
h✝ : IsEmpty α
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ x✝

pp: case refine_2
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTop α
inst✝ : CompactIccSpace α
x✝ : Set α
hs : x✝ ∈ atBot
h✝ : Nonempty α
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ x✝

Tactic:
· exact ⟨∅, isCompact_empty, fun x _ ↦ (IsEmpty.false x).elim⟩

Goal state after:
case refine_2
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTop α
inst✝ : CompactIccSpace α
x✝ : Set α
hs : x✝ ∈ atBot
h✝ : Nonempty α
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ x✝
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 β
  exact hf.exists_forall_le' default (hlim.eventually <| eventually_ge_atTop _)

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)
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty
S : Set α := s ∩ Icc a b
ha : a ∈ S
⊢ b ∈ s

Tactic:
have Sbd : BddAbove S := ⟨b, fun z hz => hz.2.2⟩

Goal state after:
α : 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
⊢ b ∈ s
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}
⊢ Icc a a ⊆ s

Tactic:
by simp [ha]

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

Goal state before:
pp: X : Type u_2
s t : Set X
x y : X
inst✝ : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
a : X
ha : a ∈ s
b : X
hb : b ∈ t
⊢ edist a x + edist x y + edist y b ≤ ediam s + edist x y + ediam t

Tactic:
by
        gcongr
        exacts [edist_le_ediam_of_mem ha xs, edist_le_ediam_of_mem yt hb]

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 only [nsmul_eq_mul] using mul_le_mul_of_nonneg_left h n.cast_nonneg

Goal state after:
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 hf.atBot_zsmul_const (neg_pos.2 hr)

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

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

Tactic:
← Rat.norm_cast_real,

Goal state after:
m : ℤ
⊢ ‖↑↑m‖ = ‖m‖
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
s : Set β
inst✝ : DecidablePred fun x ↦ x ∈ s
v : β → α
⊢ ∀ᶠ (a : β) in f, a ∈ s → s.piecewise u v a = u a

Tactic:
filter_upwards with _ h using by simp [h]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
s : Set β
inst✝ : DecidablePred fun x ↦ x ∈ s
v : β → α
⊢ ∀ᶠ (a : β) in f, a ∉ s → s.piecewise u v a = v a

Tactic:
filter_upwards with _ h using by simp [h]

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

Goal state before:
pp: case pos
α : 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
hn : Nontrivial α
⊢ ClusterPt f.limsSup f

Tactic:
by_cases! htop : ∀ x, x ≤ f.limsSup

Goal state after:
case pos
α : 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
hn : Nontrivial α
htop : ∀ (x : α), x ≤ f.limsSup
⊢ ClusterPt f.limsSup f

case neg
α : 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
hn : Nontrivial α
htop : ∃ x, f.limsSup < x
⊢ ClusterPt f.limsSup f
Module: Mathlib.Data.EReal.Operations

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

Tactic:
· exact ne_bot_of_le_ne_bot (by simp) (sub_pos.mpr h').le

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

Goal state before:
pp: case refine_1
β : Type u_2
L : SummationFilter β
h : ∀ (x : β), ∀ᶠ (s : Finset β) in L.filter, x ∈ s
s : Set (Finset β)
hs : s ∈ atTop
t : Finset β
ht : ∀ (b : Finset β), t ⊆ b → b ∈ s
⊢ s ∈ L.filter

Tactic:
have := (Filter.biInter_finset_mem t).mpr fun b hb ↦ h b

Goal state after:
case refine_1
β : Type u_2
L : SummationFilter β
h : ∀ (x : β), ∀ᶠ (s : Finset β) in L.filter, x ∈ s
s : Set (Finset β)
hs : s ∈ atTop
t : Finset β
ht : ∀ (b : Finset β), t ⊆ b → b ∈ s
this : ⋂ i ∈ t, {x | (fun s ↦ i ∈ s) x} ∈ L.filter
⊢ s ∈ L.filter
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: case a
R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun x1 x2 ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) F
⊢ f F.limsSup ≤ liminf f F

Tactic:
rw [limsSup, f_decr.map_csInf_of_continuousAt f_cont bdd_above cobdd]

Goal state after:
case a
R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun x1 x2 ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) F
⊢ sSup (f '' {a | ∀ᶠ (n : R) in F, n ≤ a}) ≤ liminf f F
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case pos
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : UniformSpace G
inst✝ : IsUniformGroup G
f : ℕ → G
vanish : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Set ℕ), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
e : Set G
he : e ∈ 𝓝 1
s : Finset ℕ
hs : ∀ (t : Set ℕ), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
t : Set ℕ
h : s.Nonempty
ht : t ⊆ {n | s.max' h + 1 ≤ n}
⊢ ∀ ⦃a : ℕ⦄, a ∈ t → a ∉ ↑s

pp: case neg
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : UniformSpace G
inst✝ : IsUniformGroup G
f : ℕ → G
vanish : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Set ℕ), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
e : Set G
he : e ∈ 𝓝 1
s : Finset ℕ
hs : ∀ (t : Set ℕ), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
t : Set ℕ
h : ¬s.Nonempty
ht : t ⊆ {n | 0 ≤ n}
⊢ ∀ ⦃a : ℕ⦄, a ∈ t → a ∉ ↑s

Tactic:
· exact fun m hmt hms ↦ (s.le_max' _ hms).not_gt (Nat.succ_le_iff.mp <| ht hmt)

Goal state after:
case neg
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : UniformSpace G
inst✝ : IsUniformGroup G
f : ℕ → G
vanish : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Set ℕ), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
e : Set G
he : e ∈ 𝓝 1
s : Finset ℕ
hs : ∀ (t : Set ℕ), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
t : Set ℕ
h : ¬s.Nonempty
ht : t ⊆ {n | 0 ≤ n}
⊢ ∀ ⦃a : ℕ⦄, a ∈ t → a ∉ ↑s
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℤ → M
hf : HasProd f m
⊢ HasProd (fun n ↦ f ↑n * f (-↑n)) (m * f 0)

Tactic:
by
  -- Note this is much easier to prove if you assume more about the target space, but we have to
  -- work hard to prove it under the very minimal assumptions here.
  apply (hf.mul (hasProd_ite_eq (0 : ℤ) (f 0))).hasProd_of_prod_eq fun u ↦ ?_
  refine ⟨u.image Int.natAbs, fun v' hv' ↦ ?_⟩
  let u1 := v'.image fun x : ℕ ↦ (x : ℤ)
  let u2 := v'.image fun x : ℕ ↦ -(x : ℤ)
  have A : u ⊆ u1 ∪ u2 := by
    intro x hx
    simp only [u1, u2, mem_union, mem_image]
    rcases le_total 0 x with (h'x | h'x)
    · refine Or.inl ⟨_, hv' <| mem_image.mpr ⟨x, hx, rfl⟩, ?_⟩
      simp only [Int.natCast_natAbs, abs_eq_self, h'x]
    · refine Or.inr ⟨_, hv' <| mem_image.mpr ⟨x, hx, rfl⟩, ?_⟩
      simp only [abs_of_nonpos h'x, Int.natCast_natAbs, neg_neg]
  exact ⟨_, A, calc
    (∏ x ∈ u1 ∪ u2, (f x * if x = 0 then f 0 else 1)) =
        (∏ x ∈ u1 ∪ u2, f x) * ∏ x ∈ u1 ∩ u2, f x := by
      rw [prod_mul_distrib]
      congr 1
      refine (prod_subset_one_on_sdiff inter_subset_union ?_ ?_).symm
      · intro x hx
        suffices x ≠ 0 by simp only [this, if_false]
        rintro rfl
        simp [u1, u2] at hx
      · intro x hx
        simp only [u1, u2, mem_inter, mem_image] at hx
        suffices x = 0 by simp only [this, if_true]
        lia
    _ = (∏ x ∈ u1, f x) * ∏ x ∈ u2, f x := prod_union_inter
    _ = (∏ b ∈ v', f b) * ∏ b ∈ v', f (-b) := by simp [u1, u2]
    _ = ∏ b ∈ v', (f b * f (-b)) := prod_mul_distrib.symm⟩

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

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

Tactic:
by_cases hn : n = 0
  · simp [hn]
  · exact iSup_pow_of_ne_zero hn _

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

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

Tactic:
by_cases hn : n = 0
  · simp [hn]
  · exact iSup_pow_of_ne_zero hn _

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
g : β → α
h : Isometry f
hg : RightInverse g f
x y : β
⊢ edist (g x) (g y) = edist x y

Tactic:
← h,

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
g : β → α
h : Isometry f
hg : RightInverse g f
x y : β
⊢ edist (f (g x)) (f (g y)) = edist x y
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
f_cont : SeqContinuous f
K : Set X
K_cpt : IsSeqCompact K
⊢ IsSeqCompact (f '' K)

Tactic:
intro ys

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
f_cont : SeqContinuous f
K : Set X
K_cpt : IsSeqCompact K
ys : ℕ → Y
⊢ (∀ (n : ℕ), ys n ∈ f '' K) → ∃ a ∈ f '' K, ∃ φ, StrictMono φ ∧ Tendsto (ys ∘ φ) atTop (𝓝 a)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: x : ℝ≥0∞
xt : x ≠ ∞
⊢ (𝓝 x).HasBasis (fun x ↦ x ≠ 0) fun ε ↦ Icc (x - ε) (x + ε)

Tactic:
by
  rcases eq_zero_or_pos x with rfl | x0
  · simp_rw [zero_tsub, zero_add, ← bot_eq_zero, Icc_bot, ← bot_lt_iff_ne_bot]
    exact nhds_bot_basis_Iic
  · refine (nhds_basis_Ioo' ⟨_, x0⟩ ⟨_, xt.lt_top⟩).to_hasBasis ?_ fun ε ε0 => ?_
    · rintro ⟨a, b⟩ ⟨ha, hb⟩
      rcases exists_between (tsub_pos_of_lt ha) with ⟨ε, ε0, hε⟩
      rcases lt_iff_exists_add_pos_lt.1 hb with ⟨δ, δ0, hδ⟩
      refine ⟨min ε δ, (lt_min ε0 (coe_pos.2 δ0)).ne', Icc_subset_Ioo ?_ ?_⟩
      · exact lt_tsub_comm.2 ((min_le_left _ _).trans_lt hε)
      · grw [min_le_right]
        exact hδ
    · exact ⟨(x - ε, x + ε), ⟨ENNReal.sub_lt_self xt x0.ne' ε0,
        lt_add_right xt ε0⟩, Ioo_subset_Icc_self⟩

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

Goal state before:
pp: case refine_1
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, a - f x ≤ ε
ε : ℝ≥0∞
hε : ε > 0
⊢ ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)

Tactic:
filter_upwards [h ε hε] with n hn
    refine ⟨?_, (hfa n).trans (le_add_right le_rfl)⟩
    rw [tsub_le_iff_right] at hn ⊢
    rwa [add_comm]

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

Goal state before:
pp: case neg
α : Type uα
inst✝² : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
hf : ¬UniformContinuous f
⊢ UniformContinuous (pkg.extend f)

Tactic:
unfold AbstractCompletion.extend
    rw [if_neg hf]
    exact uniformContinuous_of_const fun a b => by congr 1

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

Goal state before:
pp: β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
⊢ Tendsto f atTop (𝓝 0) ↔ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n < ε

Tactic:
by
  rw [ENNReal.tendsto_atTop_zero_iff_le_of_antitone hf]
  constructor <;> intro h ε hε
  · obtain ⟨n, hn⟩ := h (min 1 (ε / 2))
      (lt_min_iff.mpr ⟨zero_lt_one, (ENNReal.div_pos_iff.mpr ⟨hε.ne', by finiteness⟩)⟩)
    · refine ⟨n, hn.trans_lt ?_⟩
      by_cases hε_top : ε = ∞
      · simp [hε_top]
      refine (min_le_right _ _).trans_lt ?_
      rw [ENNReal.div_lt_iff (Or.inr hε.ne') (Or.inr hε_top)]
      conv_lhs => rw [← mul_one ε]
      gcongr; simp
  · obtain ⟨n, hn⟩ := h ε hε
    exact ⟨n, hn.le⟩

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

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
⊢ map Prod.swap ((𝓤 α).lift' gen) ≤ (𝓤 α).lift' gen

Tactic:
let f := fun s : SetRel α α =>
        { p : CauchyFilter α × CauchyFilter α | s ∈ (p.2.val ×ˢ p.1.val : Filter (α × α)) }

Goal state after:
α : Type u
inst✝ : UniformSpace α
f : SetRel α α → Set (CauchyFilter α × CauchyFilter α) := fun s ↦ {p | s ∈ ↑p.2 ×ˢ ↑p.1}
⊢ map Prod.swap ((𝓤 α).lift' gen) ≤ (𝓤 α).lift' gen
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
b : ℝ≥0∞
hb : ∀ᶠ (n : ι) in u, f n ≤ b
a : ℝ≥0∞
hba : a > b
⊢ ∀ᶠ (a_1 : ι) in u, (f + g) a_1 ≤ a

Tactic:
filter_upwards [hb, ENNReal.tendsto_nhds_zero.1 hg _ <| tsub_pos_of_lt hba] with i hf hg

Goal state after:
ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg✝ : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
b : ℝ≥0∞
hb : ∀ᶠ (n : ι) in u, f n ≤ b
a : ℝ≥0∞
hba : a > b
i : ι
hf : f i ≤ b
hg : g i ≤ a - b
⊢ (f + g) i ≤ a
Module: Mathlib.Topology.MetricSpace.Lipschitz

Goal state before:
pp: case refine_2
α : Type u
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : ι → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun x ↦ f x i) (g i) s
x : α
hx : x ∈ s
⊢ f x = (fun x i ↦ g i x) x

Tactic:
· ext1 i
    exact (hg i).2 hx

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : PseudoMetricSpace α
inst✝⁵ : PseudoMetricSpace β
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMul α β
inst✝¹ : IsBoundedSMul α β
X : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace X
s : Set X
F : ι → X → α
G : ι → X → β
f : X → α
g : X → β
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hG : ∀ x ∈ s, Tendsto (fun y ↦ (g y.2, G y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 β)
hf : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (f y) 0
hg : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (g y) 0
H : ∀ x ∈ s, Tendsto (fun y ↦ ((f y.2, g y.2), F y.1 y.2, G y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 (α × β))
x : X
hx : x ∈ s
C : ℝ
hC : ∀ᶠ (a : X) in 𝓝[s] x, dist (f a) 0 ≤ C ∧ dist (g a) 0 ≤ C
n : ι
y : X
hFn : dist (f y) (F n y) < 1
hGn : dist (g y) (G n y) < 1
hfg : dist (f y) 0 ≤ C ∧ dist (g y) 0 ≤ C
⊢ (dist (f y) 0 < C + 1 ∧ dist (g y) 0 < C + 1) ∧ dist (F n y) 0 < C + 1 ∧ dist (G n y) 0 < C + 1

Tactic:
dist_triangle_left (F n y) 0 (f y),

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : PseudoMetricSpace α
inst✝⁵ : PseudoMetricSpace β
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMul α β
inst✝¹ : IsBoundedSMul α β
X : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace X
s : Set X
F : ι → X → α
G : ι → X → β
f : X → α
g : X → β
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hG : ∀ x ∈ s, Tendsto (fun y ↦ (g y.2, G y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 β)
hf : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (f y) 0
hg : ∀ x ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[s] x) fun y ↦ dist (g y) 0
H : ∀ x ∈ s, Tendsto (fun y ↦ ((f y.2, g y.2), F y.1 y.2, G y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 (α × β))
x : X
hx : x ∈ s
C : ℝ
hC : ∀ᶠ (a : X) in 𝓝[s] x, dist (f a) 0 ≤ C ∧ dist (g a) 0 ≤ C
n : ι
y : X
hFn : dist (f y) (F n y) < 1
hGn : dist (g y) (G n y) < 1
hfg : dist (f y) 0 ≤ C ∧ dist (g y) 0 ≤ C
⊢ (dist (f y) 0 < C + 1 ∧ dist (g y) 0 < C + 1) ∧ dist (f y) (F n y) + dist (f y) 0 < C + 1 ∧ dist (G n y) 0 < C + 1
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
Kf Kg : ℝ≥0
f g : α → E
s : Set α
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
⊢ LipschitzOnWith (Kf + Kg) (fun x ↦ f x / g x) s

Tactic:
simpa only [div_eq_mul_inv] using! hf.mul hg.inv

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

Goal state before:
pp: α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
Kf Kg : ℝ≥0
f g : α → E
hf : LipschitzWith Kf f
hg : LipschitzWith Kg g
⊢ LipschitzWith (Kf + Kg) fun x ↦ f x / g x

Tactic:
simpa only [div_eq_mul_inv] using! hf.mul hg.inv

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

Goal state before:
pp: α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
f g : α → E
s : Set α
hf : LocallyLipschitzOn s f
hg : LocallyLipschitzOn s g
⊢ LocallyLipschitzOn s fun x ↦ f x / g x

Tactic:
simpa only [div_eq_mul_inv] using! hf.mul hg.inv

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

Goal state before:
pp: α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
f g : α → E
hf : LocallyLipschitz f
hg : LocallyLipschitz g
⊢ LocallyLipschitz fun x ↦ f x / g x

Tactic:
simpa only [div_eq_mul_inv] using! hf.mul hg.inv

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

Goal state before:
pp: α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
Kf Kg : ℝ≥0
f g : α → E
hf : AntilipschitzWith Kf f
hg : LipschitzWith Kg g
hK : Kg < Kf⁻¹
this : PseudoMetricSpace α := PseudoEMetricSpace.toPseudoMetricSpace ⋯
x y : α
⊢ ↑(Kf⁻¹ - Kg) * dist x y ≤ dist (f x * g x) (f y * g y)

Tactic:
NNReal.coe_sub hK.le,

Goal state after:
α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
Kf Kg : ℝ≥0
f g : α → E
hf : AntilipschitzWith Kf f
hg : LipschitzWith Kg g
hK : Kg < Kf⁻¹
this : PseudoMetricSpace α := PseudoEMetricSpace.toPseudoMetricSpace ⋯
x y : α
⊢ (↑Kf⁻¹ - ↑Kg) * dist x y ≤ dist (f x * g x) (f y * g y)
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: x y : ℝ
hy : 0 ≤ y
⊢ ‖x‖₊ * y.toNNReal = ‖x * y‖₊

Tactic:
rw [mul_comm, mul_comm x, toNNReal_mul_nnnorm x hy]

Goal state after:
Module: Mathlib.Algebra.Order.AddTorsor

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝³ : Preorder G
inst✝² : Preorder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a < b
h₂ : c ≤ d
⊢ a • d < b • d

Tactic:
refine lt_of_le_not_ge (IsOrderedSMul.smul_le_smul_right a b (le_of_lt h₁) d) ?_

Goal state after:
G : Type u_1
P : Type u_2
inst✝³ : Preorder G
inst✝² : Preorder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a < b
h₂ : c ≤ d
⊢ ¬b • d ≤ a • d
Module: Mathlib.Data.ENNReal.Action

Goal state before:
pp: a b c d : ℝ≥0∞
r✝ p q : ℝ≥0
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra ℝ≥0∞ A
r : ℝ≥0
x : A
⊢ r • x = ((algebraMap ℝ≥0∞ A).comp ofNNRealHom) r * x

Tactic:
by simp [← Algebra.smul_def (r : ℝ≥0∞) x, smul_def]

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: 𝕜 : Type u_4
val✝ : NontriviallyNormedField 𝕜
x : ℝ
h : x ∈ upperBounds (Set.range fun k ↦ ‖k‖)
⊢ False

Tactic:
obtain ⟨k, hk⟩ := NormedField.exists_lt_norm 𝕜 x

Goal state after:
𝕜 : Type u_4
val✝ : NontriviallyNormedField 𝕜
x : ℝ
h : x ∈ upperBounds (Set.range fun k ↦ ‖k‖)
k : 𝕜
hk : x < ‖k‖
⊢ False