mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
⊢ a ≤ y

Tactic:
have hx' : x⁻¹ ≠ 0 := by rwa [Ne, inv_eq_zero]

Goal state after:
x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
⊢ a ≤ y
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
⊢ ⨅ r, f ↑r = ⨅ q, f ↑↑q

Tactic:
refine le_antisymm ?_ ?_
  · have : Nonempty { r' : ℚ // x < ↑r' } := by
      obtain ⟨r, hrx⟩ := exists_rat_gt x
      exact ⟨⟨r, hrx⟩⟩
    refine le_ciInf fun r => ?_
    obtain ⟨y, hxy, hyr⟩ := exists_rat_btwn r.prop
    refine ciInf_set_le hf (hxy.trans ?_)
    exact_mod_cast hyr
  · refine le_ciInf fun q => ?_
    have hq := q.prop
    rw [mem_Ioi] at hq
    obtain ⟨y, hxy, hyq⟩ := exists_rat_btwn hq
    refine (ciInf_le ?_ ?_).trans ?_
    · refine ⟨hf.some, fun z => ?_⟩
      rintro ⟨u, rfl⟩
      suffices hfu : f u ∈ f '' Ioi x from hf.choose_spec hfu
      exact ⟨u, u.prop, rfl⟩
    · exact ⟨y, hxy⟩
    · refine hf_mono (le_trans ?_ hyq.le)
      norm_cast

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono ⇑f
r : ℝ
hr : 0 < r
⊢ ∃ d, ↑(f ↑d) < r

Tactic:
by
  set s : NNReal := ⟨r, le_of_lt hr⟩
  have hs : 0 < s := hr
  exact NNReal.exists_lt_of_strictMono hf hs

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

Goal state before:
pp: a b c : ℝ≥0∞
hc : c ≠ ∞
⊢ c + a - (c + b) = a - b

Tactic:
add_comm c

Goal state after:
a b c : ℝ≥0∞
hc : c ≠ ∞
⊢ a + c - (b + c) = a - b
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ
⊢ Real.toEReal '' Ioi x = Ioo ↑x ⊤

Tactic:
by
  refine (image_comp WithBot.some WithTop.some _).trans ?_
  rw [WithTop.image_coe_Ioi, WithBot.image_coe_Ioo]
  rfl

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

Goal state before:
pp: r : ℝ≥0
b : ℝ≥0∞
hb : 1 ≤ ↑r * b
⊢ ∀ (p : ℝ≥0), b = ↑p → r⁻¹ ≤ p

Tactic:
rintro b rfl
      apply NNReal.inv_le_of_le_mul
      rwa [← coe_mul, ← coe_one, coe_le_coe] at hb

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

Goal state before:
pp: case neg
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 : FractionalIdeal R⁰ K
n : ℕ
h : count K v (I ^ n) = ↑n * count K v I
hI : ¬I = 0
⊢ (if I ^ n ≠ 0 ∧ I ≠ 0 then count K v (I ^ n) + count K v I else 0) = ↑(n + 1) * count K v I

Tactic:
if_pos (And.intro (pow_ne_zero n hI) hI),

Goal state after:
case neg
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 : FractionalIdeal R⁰ K
n : ℕ
h : count K v (I ^ n) = ↑n * count K v I
hI : ¬I = 0
⊢ count K v (I ^ n) + count K v I = ↑(n + 1) * count K v I
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a : ℝ≥0∞
⊢ ∀ ⦃b : ℝ≥0∞⦄, a < b → b⁻¹ < a⁻¹

Tactic:
b

Goal state after:
a b : ℝ≥0∞
⊢ a < b → b⁻¹ < a⁻¹
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
⊢ a ≤ b⁻¹ ↔ a * b ≤ 1

Tactic:
by
  rw [← one_div, ENNReal.le_div_iff_mul_le] <;>
    · right
      simp

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
⊢ edist x y ≤ edist x z + edist y z

Tactic:
by
  rw [edist_comm y]; apply edist_triangle

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

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝² : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
inst✝¹ : Subsingleton α
inst✝ : NeZero ε
⊢ IsEmpty ↑(sphere x ε)

Tactic:
by
  rw [sphere_eq_empty_of_subsingleton (NeZero.ne ε)]; infer_instance

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
⊢ closedBall x ε = ∅ ↔ ε < 0

Tactic:
by
  rw [← not_nonempty_iff_eq_empty, nonempty_closedBall, not_le]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
⊢ BoundedSpace α ↔ ∃ C, ∀ (a b : α), dist a b ≤ C

Tactic:
by
  rw [← isBounded_univ, Metric.isBounded_iff]
  simp

Goal state after:
Module: Mathlib.Data.NNReal.Basic

Goal state before:
pp: ι : Type u_2
s : Finset ι
f : ι → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
⊢ ↑(∑ a ∈ s, f a).toNNReal = ↑(∑ a ∈ s, (f a).toNNReal)

Tactic:
NNReal.coe_sum,

Goal state after:
ι : Type u_2
s : Finset ι
f : ι → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
⊢ ↑(∑ a ∈ s, f a).toNNReal = ∑ i ∈ s, ↑(f i).toNNReal
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ Inseparable x y ↔ nndist x y = 0

Tactic:
by
  rw [EMetric.inseparable_iff, edist_nndist, ENNReal.coe_eq_zero]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
ι : Sort u_2
c : ι → Set α
hs : IsCompact s
hc₁ : ∀ (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (c i)
hc₂ : s ⊆ ⋃ i, c i
⊢ ∃ δ > 0, ∀ x ∈ s, ∃ i, eball x δ ⊆ c i

Tactic:
simpa only [eball, UniformSpace.ball, preimage_ofPred_eq, edist_comm]
    using uniformity_basis_edist.lebesgue_number_lemma hs hc₁ hc₂

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝² : PseudoEMetricSpace α
X : β → Type u_2
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (X b)
f g : (b : β) → X b
⊢ edist f g = edist g f

Tactic:
by simp [edist_pi_def, edist_comm]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : DiscreteTopology α
a : α
⊢ ∀ (b : α), b ≤ a

Tactic:
b

Goal state after:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : DiscreteTopology α
a b : α
⊢ b ≤ a
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: case neg
γ : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : ClosedIicTopology α
f : γ → α
inst✝ : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst✝, inst✝³] f
h : ¬BddAbove (range fun x ↦ f ↑x)
⊢ ⨆ s, f ↑s = ⨆ i, f i

Tactic:
suffices ¬ BddAbove (range f) by simp [ciSup_of_not_bddAbove, this, h]
    contrapose h
    grind [h.mono]

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
β : Type u_3
inst✝² : LinearOrder β
inst✝¹ : DenselyOrdered α
inst✝ : FirstCountableTopology α
f : β → α
x y : α
hf : DenseRange f
hmono : Monotone f
hlt : x < y
⊢ ∃ u, StrictAnti u ∧ (∀ (n : ℕ), f (u n) ∈ Ioo x y) ∧ Tendsto (f ∘ u) atTop (𝓝 x)

Tactic:
simpa using! hf.exists_seq_strictMono_tendsto_of_lt (α := αᵒᵈ) (β := βᵒᵈ) hmono.dual
    (OrderDual.toDual_lt_toDual.2 hlt)

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
f : α → β
s : Set α
Cf : ContinuousWithinAt f s (sSup s)
Mf : MonotoneOn f s
fbot : f ⊥ = ⊥
h : s = ∅
⊢ f (sSup s) = sSup (f '' s)

pp: case inr
α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
f : α → β
s : Set α
Cf : ContinuousWithinAt f s (sSup s)
Mf : MonotoneOn f s
fbot : f ⊥ = ⊥
h : s.Nonempty
⊢ f (sSup s) = sSup (f '' s)

Tactic:
· simp [h, fbot]

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
f : α → β
s : Set α
Cf : ContinuousWithinAt f s (sSup s)
Mf : MonotoneOn f s
fbot : f ⊥ = ⊥
h : s.Nonempty
⊢ f (sSup s) = sSup (f '' s)
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : CompactIccSpace α
a : αᵒᵈ
⊢ ∀ {b : αᵒᵈ}, IsCompact (Icc a b)

Tactic:
b

Goal state after:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : CompactIccSpace α
a b : αᵒᵈ
⊢ IsCompact (Icc a b)
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝⁷ : TopologicalSpace α
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : OrderTopology α
inst✝⁴ : DenselyOrdered α
δ : Type u_1
inst✝³ : LinearOrder δ
inst✝² : TopologicalSpace δ
inst✝¹ : OrderClosedTopology δ
inst✝ : BoundedOrder α
f : α → δ
hf_c : Continuous[inst✝⁷, inst✝²] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a : α
⊢ ∀ ⦃b : α⦄, a < b → f a < f b

Tactic:
b

Goal state after:
α : Type u
inst✝⁷ : TopologicalSpace α
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : OrderTopology α
inst✝⁴ : DenselyOrdered α
δ : Type u_1
inst✝³ : LinearOrder δ
inst✝² : TopologicalSpace δ
inst✝¹ : OrderClosedTopology δ
inst✝ : BoundedOrder α
f : α → δ
hf_c : Continuous[inst✝⁷, inst✝²] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
⊢ a < b → f a < f b
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
hf_mono_st : StrictMonoOn f (Icc s t) ∨ StrictAntiOn f (Icc s t)
h : StrictAntiOn f (Icc s t)
this : Icc a b ⊆ Icc s t
⊢ False

Tactic:
replace : StrictAntiOn f (Icc a b) := StrictAntiOn.mono h this

Goal state after:
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
hf_mono_st : StrictMonoOn f (Icc s t) ∨ StrictAntiOn f (Icc s t)
h : StrictAntiOn f (Icc s t)
this : StrictAntiOn f (Icc a b)
⊢ False
Module: Mathlib.Topology.Algebra.Order.Archimedean

Goal state before:
pp: case inl
G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
S : Subgroup G
hS : ∀ ε > 1, ∃ g ∈ S, g ∈ Ioo 1 ε
h✝ : Subsingleton G
x : G
⊢ x ∈ ↑S

Tactic:
rw [Subsingleton.elim x 1]

Goal state after:
case inl
G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
S : Subgroup G
hS : ∀ ε > 1, ∃ g ∈ S, g ∈ Ioo 1 ε
h✝ : Subsingleton G
x : G
⊢ 1 ∈ ↑S
Module: Mathlib.Topology.Order.MonotoneContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b
⊢ ContinuousWithinAt f (Ici a) a

Tactic:
have has : a ∈ s := mem_of_mem_nhdsWithin self_mem_Ici hs
  refine tendsto_order.2 ⟨fun b hb => ?_, fun b hb => ?_⟩
  · filter_upwards [hs, @self_mem_nhdsWithin _ _ a (Ici a)] with _ hxs hxa using hb.trans_le
      ((h_mono.le_iff_le has hxs).2 hxa)
  · rcases hfs b hb with ⟨c, hcs, hac, hcb⟩
    rw [h_mono.lt_iff_lt has hcs] at hac
    filter_upwards [hs, Ico_mem_nhdsGE hac]
    rintro x hx ⟨_, hxc⟩
    exact ((h_mono.lt_iff_lt hx hcs).2 hxc).trans_le hcb

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

Goal state before:
pp: x : ℕ
r : ℝ
hr : r < 0
⊢ ⌊↑x⌋₊ < ⌈↑x - r⌉₊

Tactic:
rw [floor_natCast, Nat.lt_ceil]

Goal state after:
x : ℕ
r : ℝ
hr : r < 0
⊢ ↑x < ↑x - r
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ IsCobounded r ⊥ ↔ ∃ b, ∀ (x : α), r b x

Tactic:
simp [IsCobounded]

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
⊢ IsCobounded r (𝓟 s) ↔ ∃ b, ∀ (a : α), (∀ x ∈ s, r x a) → r b a

Tactic:
simp [IsCobounded]

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

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

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

Tactic:
· rcases eq_or_ne z ⊤ with (rfl | hz)
    · obtain rfl := htop rfl rfl
      simpa
    lift z to ℝ using ⟨hz, hbot⟩
    exact add_lt_add_right_coe h z

Goal state after:
case inr
x y z t : EReal
h : x < y
h' : z ≤ t
hbot : t ≠ ⊥
htop : t = ⊤ → z = ⊤ → x = ⊥
hlt : z < t
⊢ x + z < y + t
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
u : β → α
g : Filter β
a : α
ha : ∀ᶠ (n : β) in f, u n ≤ a
⊢ ∀ (i : α), (∀ᶠ (n : β) in g, u n ≤ i) → sInf {a | ∀ᶠ (n : β) in f ⊔ g, u n ≤ a} ≤ a ⊔ i

Tactic:
b

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
u : β → α
g : Filter β
a : α
ha : ∀ᶠ (n : β) in f, u n ≤ a
b : α
⊢ (∀ᶠ (n : β) in g, u n ≤ b) → sInf {a | ∀ᶠ (n : β) in f ⊔ g, u n ≤ a} ≤ a ⊔ b
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: 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
hbot : ∃ x, x < f.limsSup
⊢ ClusterPt f.limsSup f

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

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

Goal state before:
pp: case top
a b : EReal
h : a ≤ b + ⊤
⊢ a - ⊤ ≤ b

Tactic:
simp only [sub_top, bot_le]

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

Goal state before:
pp: a : EReal
⊢ ∀ {b : EReal}, a * b = 0 → a = 0 ∨ b = 0

Tactic:
b

Goal state after:
a b : EReal
⊢ a * b = 0 → a = 0 ∨ b = 0
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h✝ : f.NeBot
a : β
ha : ∀ᶠ (x : α) in f, v x ≤ a
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u

Tactic:
apply IsCoboundedUnder.of_frequently_le (a := a)

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h✝ : f.NeBot
a : β
ha : ∀ᶠ (x : α) in f, v x ≤ a
⊢ ∃ᶠ (x : α) in f, u x ≤ a
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: β : Type u_4
inst✝² : Finite β
L : SummationFilter β
inst✝¹ : L.LeAtTop
inst✝ : L.NeBot
this : Fintype β
hAtTop : atTop = pure Finset.univ
hL : L.filter ≤ atTop
hL' : ∅ ∉ L.filter
⊢ L = unconditional β

Tactic:
cases L with | mk F =>
  simp only [unconditional, hAtTop] at *
  congr 1
  refine eq_of_le_of_ge hL (pure_le_iff.mpr ?_)
  contrapose! hL'
  obtain ⟨s, hs, hs'⟩ := hL'
  simpa [inter_singleton_eq_empty.mpr hs'] using inter_mem hs (le_pure_iff.mp hL)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : CommMonoid α
inst✝⁴ : TopologicalSpace α
f : β → α
a : α
L : SummationFilter β
inst✝³ : CommMonoid γ
inst✝² : TopologicalSpace γ
hf : HasProd f a L
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : Continuous[inst✝⁴, inst✝²] ⇑g
this : (⇑g ∘ fun s ↦ ∏ b ∈ s, f b) = fun s ↦ ∏ b ∈ s, (⇑g ∘ f) b
⊢ Tendsto (⇑g ∘ fun s ↦ ∏ b ∈ s, f b) L.filter (𝓝 (g a))

Tactic:
exact (hg.tendsto a).comp hf

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

Goal state before:
pp: case refine_1.ofNat
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.ofNat a✝ ∈ u
⊢ (∃ a ∈ v', ↑a = Int.ofNat a✝) ∨ ∃ a ∈ v', Int.negSucc a = Int.ofNat a✝

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.inl ⟨_, hv' (by simpa using Or.inl hx), rfl⟩

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁴ : NonUnitalNonAssocSemiring α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalSemiring α
inst✝¹ : T2Space α
inst✝ : L.NeBot
f g : ι → α
a : α
hf : Summable f L
hg : Summable g L
h : ∀ (i : ι), SemiconjBy a (f i) (g i)
⊢ a * ∑'[L] (i : ι), f i = (∑'[L] (i : ι), g i) * a

Tactic:
← hf.tsum_mul_left a,

Goal state after:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁴ : NonUnitalNonAssocSemiring α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalSemiring α
inst✝¹ : T2Space α
inst✝ : L.NeBot
f g : ι → α
a : α
hf : Summable f L
hg : Summable g L
h : ∀ (i : ι), SemiconjBy a (f i) (g i)
⊢ ∑'[L] (i : ι), a * f i = (∑'[L] (i : ι), g i) * a
Module: Mathlib.Topology.MetricSpace.ProperSpace.Real

Goal state before:
pp: x : ℝ≥0
r : ℝ
⊢ IsCompact (Metric.closedBall x r)

Tactic:
have emb : IsClosedEmbedding ((↑) : ℝ≥0 → ℝ) := Isometry.isClosedEmbedding fun _ ↦ congrFun rfl
    exact emb.isCompact_preimage (K := Metric.closedBall x r) (isCompact_closedBall _ _)

Goal state after:
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:
rcases eq_zero_or_pos x with rfl | x0

Goal state after:
case inl
xt : 0 ≠ ∞
⊢ (𝓝 0).HasBasis (fun x ↦ x ≠ 0) fun ε ↦ Icc (0 - ε) (0 + ε)

case inr
x : ℝ≥0∞
xt : x ≠ ∞
x0 : 0 < x
⊢ (𝓝 x).HasBasis (fun x ↦ x ≠ 0) fun ε ↦ Icc (x - ε) (x + ε)
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝² : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝¹ : UniformSpace β
f : α → β
inst✝ : T2Space β
hf : UniformContinuous f
a : α
⊢ pkg.extend f (pkg.coe a) = f a

Tactic:
by
  rw [pkg.extend_def hf]
  exact pkg.isDenseInducing.extend_eq hf.continuous a

Goal state after:
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: case refine_1.succ
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
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun x y ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
hsne : s.Nonempty
M : ℕ
hMl : M + 1 ≤ l.length
hMs : IsGreatest s (M + 1)
hM_lt : M + 1 < L.length
hM_ltx : M + 1 < (x :: l).length
hM_lty : M + 1 < (l ++ [y]).length
⊢ d x (x :: l)[M + 1] ≤ L.sum

Tactic:
rw [Nat.succ_le_iff] at hMl
      have hMl' : length (take M l) = M := length_take.trans (min_eq_left hMl.le)
      refine (ihn _ hMl _ _ _ hMl').trans ?_
      convert! hMs.1.out
      rw [take_zipWith, take, take_add_one, getElem?_append_left hMl, getElem?_eq_getElem hMl,
        ← Option.coe_def, Option.toList_some, take_append_of_le_length hMl.le, getElem_cons_succ]

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

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
⊢ Nonempty (CauchyFilter α) ↔ Nonempty α

Tactic:
by
  constructor <;> rintro ⟨c⟩
  · have := eq_univ_iff_forall.1 isDenseEmbedding_pureCauchy.isDenseInducing.closure_range c
    obtain ⟨_, ⟨_, a, _⟩⟩ := mem_closure_iff.1 this _ isOpen_univ trivial
    exact ⟨a⟩
  · exact ⟨pureCauchy c⟩

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

Goal state before:
pp: α : Type u
inst✝² : UniformSpace α
β : Type v
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
hf : UniformContinuous f
a : α
⊢ ⋯.extend f (pureCauchy a) = f a

Tactic:
exact uniformly_extend_of_ind isUniformInducing_pureCauchy denseRange_pureCauchy hf _

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:
by
  simp only [LipschitzOnWith, edist_nndist, dist_nndist]
  norm_cast

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

Goal state before:
pp: ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst✝ : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
aux' : (limsup u f).toReal = b.truncateToReal (limsup u f)
⊢ limsup (fun i ↦ (u i).toReal) f = (limsup u f).toReal

Tactic:
limsup_congr aux,

Goal state after:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst✝ : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
aux' : (limsup u f).toReal = b.truncateToReal (limsup u f)
⊢ limsup (fun a ↦ b.truncateToReal (u a)) f = (limsup u f).toReal
Module: Mathlib.Topology.MetricSpace.Lipschitz

Goal state before:
pp: case inr
α : Type u
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty ↑s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s

Tactic:
let g := fun y : α => iInf fun x : s => f x + K * dist y x

Goal state after:
case inr
α : Type u
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty ↑s
g : α → ℝ := fun y ↦ ⨅ x, f ↑x + ↑K * dist y ↑x
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s
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:
dist_self_mul_right,

Goal state after:
E : Type u_2
inst✝ : SeminormedCommGroup E
a b : E
⊢ ‖b⁻¹‖ = ‖b‖
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
F : Type u_4
inst✝⁴ : PseudoEMetricSpace α✝
inst✝³ : PseudoEMetricSpace β✝
inst✝² : FunLike F α✝ β✝
α : Type ?u.16
β : Type ?u.18
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
r : ℝ≥0
hne : r ≠ 0
h : ∀ (x y : α), nndist (f x) (f y) = r * nndist x y
x y : α
⊢ edist (f x) (f y) = ↑r * edist x y

Tactic:
rw [edist_nndist, edist_nndist, ← ENNReal.coe_mul, h x y]

Goal state after: