mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ IsBounded r ⊤ ↔ ∃ t, ∀ (x : α), r x t

Tactic:
simp [IsBounded]

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

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

Tactic:
simp [IsBounded]

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
⊢ (∃ s, BddAbove (u '' s) ∧ ∀ᶠ (x : β) in f, x ∈ s) → IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u

Tactic:
rintro ⟨s, ⟨b, hb⟩, hs⟩

Goal state after:
case mpr
α : 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)
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
Module: Mathlib.Topology.Order.MonotoneConvergence

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : SupConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
ha : IsLUB (range f) a
⊢ Tendsto f atTop (𝓝 a)

Tactic:
suffices Tendsto (rangeFactorization f) atTop atTop from
    (SupConvergenceClass.tendsto_coe_atTop_isLUB _ _ ha).comp this

Goal state after:
α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : SupConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
ha : IsLUB (range f) a
⊢ Tendsto (rangeFactorization f) atTop atTop
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β → γ
Kα Kβ : ℝ≥0
hα : ∀ (b : β), LipschitzWith Kα fun a ↦ f a b
hβ : ∀ (a : α), LipschitzWith Kβ (f a)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
⊢ edist (f a₁ b₁) (f a₂ b₁) + edist (f a₂ b₁) (f a₂ b₂) ≤ ↑Kα * edist (a₁, b₁) (a₂, b₂) + ↑Kβ * edist (a₁, b₁) (a₂, b₂)

Tactic:
exact
    add_le_add (le_trans (hα _ _ _) <| mul_right_mono <| le_max_left _ _)
      (le_trans (hβ _ _ _) <| mul_right_mono <| le_max_right _ _)

Goal state after:
Module: Mathlib.Order.LiminfLimsup

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

Tactic:
sup_comm,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
u : β → α
a : α
⊢ (⨆ s ∈ f, ⨅ a ∈ s, u a) ⊔ a = ⨆ s ∈ f, ⨅ a_1 ∈ s, a ⊔ u a_1
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ y > x, ∀ᶠ (a : α) in f, u a < y
h' : ∀ y > x, ∃ z, x < z ∧ z < y
y : β
x_y : x < y
⊢ limsup u f < y

Tactic:
rcases h' y x_y with ⟨z, x_z, z_y⟩

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ y > x, ∀ᶠ (a : α) in f, u a < y
h' : ∀ y > x, ∃ z, x < z ∧ z < y
y : β
x_y : x < y
z : β
x_z : x < z
z_y : z < y
⊢ limsup u f < y
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot.coe
a✝ : ℝ
h : ⊥ ≠ 0 ∧ ↑a✝ ≠ 0
⊢ ⊥ * ↑a✝ ≠ 0

Tactic:
rcases lt_or_gt_of_ne h.2 with (h | h)

Goal state after:
case bot.coe.inl
a✝ : ℝ
h✝ : ⊥ ≠ 0 ∧ ↑a✝ ≠ 0
h : ↑a✝ < 0
⊢ ⊥ * ↑a✝ ≠ 0

case bot.coe.inr
a✝ : ℝ
h✝ : ⊥ ≠ 0 ∧ ↑a✝ ≠ 0
h : 0 < ↑a✝
⊢ ⊥ * ↑a✝ ≠ 0
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top.coe
a✝ : ℝ
h : ⊤ ≠ 0 ∧ ↑a✝ ≠ 0
⊢ ⊤ * ↑a✝ ≠ 0

Tactic:
rcases lt_or_gt_of_ne h.2 with (h | h)

Goal state after:
case top.coe.inl
a✝ : ℝ
h✝ : ⊤ ≠ 0 ∧ ↑a✝ ≠ 0
h : ↑a✝ < 0
⊢ ⊤ * ↑a✝ ≠ 0

case top.coe.inr
a✝ : ℝ
h✝ : ⊤ ≠ 0 ∧ ↑a✝ ≠ 0
h : 0 < ↑a✝
⊢ ⊤ * ↑a✝ ≠ 0
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: case inr
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst✝ : L.NeBot
f : β ↪ γ
c : γ
hc : c ∉ range ⇑f
⊢ c ∈ (L.map f).support ↔ c ∈ ⇑f '' L.support

Tactic:
· exact ⟨fun hc' ↦ have := hc'.exists; by grind, by grind⟩

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
v : α → β
l : β → γ
u : γ → β
gc : GaloisConnection l u
hlv : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ l (v x)
hv_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
c : γ
hc : ∀ᶠ (n : γ) in map (fun x ↦ l (v x)) f, n ≤ c
⊢ l (limsup v f) ≤ c

Tactic:
Filter.eventually_map

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
v : α → β
l : β → γ
u : γ → β
gc : GaloisConnection l u
hlv : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ l (v x)
hv_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
c : γ
hc : ∀ᶠ (a : α) in f, l (v a) ≤ c
⊢ l (limsup v f) ≤ c
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
f : β → α
s : Finset β
hf : ∀ b ∉ s, f b = 1
inst✝ : L.HasSupport
⊢ Multipliable f L

Tactic:
by
  classical
  exact (hasProd_prod_support_of_ne_finset_one (fun b _ hb ↦ hf b hb)).multipliable

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

Goal state before:
pp: α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝⁴ : CommGroup α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalGroup α
f : β → α
a₁ : α
inst✝¹ : L.LeAtTop
hf : HasProd f a₁ L
b : β
inst✝ : DecidableEq β
a : α
⊢ HasProd (Function.update f b a) (a / f b * a₁) L

Tactic:
convert! (hasProd_ite_eq b (a / f b) (L := L)).mul hf with b'

Goal state after:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝⁴ : CommGroup α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalGroup α
f : β → α
a₁ : α
inst✝¹ : L.LeAtTop
hf : HasProd f a₁ L
b : β
inst✝ : DecidableEq β
a : α
b' : β
⊢ Function.update f b a b' = (if b' = b then a / f b else 1) * f b'
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : CommMonoid α
inst✝⁵ : TopologicalSpace α
L : SummationFilter β
inst✝⁴ : CommMonoid γ
inst✝³ : TopologicalSpace γ
inst✝² : T2Space γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
⊢ Multipliable f L → Multipliable (⇑g ∘ f) L ∧ ∏'[L] (i : β), g (f i) ∈ Set.range ⇑g

Tactic:
intro hf
    constructor
    · exact hf.map g hg.continuous
    · by_cases hL : L.NeBot
      · exact ⟨_, hf.map_tprod g hg.continuous⟩
      · by_cases hfs : (mulSupport fun x ↦ g (f x)).Finite
        · simp [tprod_bot hL, finprod_eq_prod _ hfs, ← _root_.map_prod]
        · exact ⟨1, by simp [tprod_bot hL, finprod_of_infinite_mulSupport hfs]⟩

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

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : T2Space M
f : ℕ → M
hf : Multipliable f
h : Tendsto (fun n ↦ ∏ i ∈ range n, f i) atTop (𝓝 m)
⊢ HasProd f m

Tactic:
tendsto_nhds_unique h hf.hasProd.tendsto_prod_nat

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : T2Space M
f : ℕ → M
hf : Multipliable f
h : Tendsto (fun n ↦ ∏ i ∈ range n, f i) atTop (𝓝 m)
⊢ HasProd f (∏' (b : ℕ), f b)
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁷ : CommGroup α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedMonoid α
inst✝⁴ : TopologicalSpace α
inst✝³ : IsTopologicalGroup α
inst✝² : OrderClosedTopology α
g : ι → α
inst✝¹ : L.LeAtTop
inst✝ : L.NeBot
hsum : Multipliable g L
hg : ∀ (i : ι), 1 ≤ g i
i : ι
hi : 1 < g i
⊢ 1 < ∏'[L] (i : ι), g i

Tactic:
by
  rw [← tprod_one (L := L)]
  exact multipliable_one.tprod_lt_tprod hg hi hsum

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

Goal state before:
pp: α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : e ∈ 𝓝 1
⊢ ∃ s, ∀ (t : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e

Tactic:
let : UniformSpace G := IsTopologicalGroup.rightUniformSpace G

Goal state after:
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : e ∈ 𝓝 1
this : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
⊢ ∃ s, ∀ (t : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : e ∈ 𝓝 1
⊢ ∃ s, ∀ (t : Set α), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e

Tactic:
let : UniformSpace G := IsTopologicalGroup.rightUniformSpace G

Goal state after:
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : e ∈ 𝓝 1
this : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
⊢ ∃ s, ∀ (t : Set α), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: case neg
β : Type u_2
L : SummationFilter β
inst✝⁶ : L.LeAtTop
inst✝⁵ : L.NeBot
α : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : CommMonoid α
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : DecidableEq β
f : β → α
a a' : α
hf : HasProd f a L
b : β
x : α
hf' : HasProd (update f b x) a' L
b' : β
hb' : ¬b' = b
⊢ f b' * 1 = update f b x b' * 1

Tactic:
simp only [Function.update_apply, hb', if_false]

Goal state after:
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
⊢ (x :: lxy).length = (lxy ++ [y]).length

Tactic:
length_cons,

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
⊢ lxy.length + 1 = (lxy ++ [y]).length
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
⊢ ⨅ l, (zipWith d (x :: l) (l ++ [z])).sum ≤
    (zipWith d (x :: lxy) (lxy ++ [y])).sum + (zipWith d (y :: lyz) (lyz ++ [z])).sum

Tactic:
calc
      ⨅ l, (zipWith d (x::l) (l ++ [z])).sum ≤
          (zipWith d (x::lxy ++ y::lyz) ((lxy ++ y::lyz) ++ [z])).sum :=
        ciInf_le (OrderBot.bddBelow _) (lxy ++ y::lyz)
      _ = (zipWith d (x::lxy) (lxy ++ [y])).sum + (zipWith d (y::lyz) (lyz ++ [z])).sum := by
        rw [← sum_append, ← zipWith_append, cons_append, ← @singleton_append _ y, append_assoc,
          append_assoc, append_assoc]
        rw [length_cons, length_append, length_singleton]

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
⊢ FrechetUrysohnSpace X

Tactic:
by
  refine ⟨fun s x hx ↦ ?_⟩
  rw [hf.closure_eq_preimage_closure_image, mem_preimage, mem_closure_iff_seq_limit] at hx
  rcases hx with ⟨u, hus, hu⟩
  choose v hv hvu using hus
  refine ⟨v, hv, ?_⟩
  simpa only [hf.tendsto_nhds_iff, Function.comp_def, hvu]

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

Goal state before:
pp: case h
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])
⊢ d x y ≤ 2 * L.sum

Tactic:
have hL_len : length L = length l + 1 := by simp [L]

Goal state after:
case h
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
⊢ d x y ≤ 2 * L.sum
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

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

Tactic:
simpa only [pkg.extend_coe hf] using h

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

Goal state before:
pp: α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ (((𝓤 α).lift' gen).lift' fun s ↦ s ○ s) ≤ (𝓤 α).lift' gen

Tactic:
exact comp_gen

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:
rw [extend, if_pos hf]

Goal state after:
α : Type u
inst✝² : UniformSpace α
β : Type v
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
hf : UniformContinuous f
a : α
⊢ ⋯.extend f (pureCauchy a) = f a
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: case pos
α : Type u
inst✝² : UniformSpace α
β : Type v
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace β
f : α → β
hf : UniformContinuous f
⊢ UniformContinuous (extend f)

Tactic:
rw [extend, if_pos hf]

Goal state after:
case pos
α : Type u
inst✝² : UniformSpace α
β : Type v
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace β
f : α → β
hf : UniformContinuous f
⊢ UniformContinuous (⋯.extend f)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case neg
a : ℝ≥0∞
a_infty : ¬a = ∞
⊢ Continuous fun x ↦ x - a

Tactic:
rw [show (fun x => x - a) = (fun p : ℝ≥0∞ × ℝ≥0∞ => p.fst - p.snd) ∘ fun x => ⟨x, a⟩ by rfl]

Goal state after:
case neg
a : ℝ≥0∞
a_infty : ¬a = ∞
⊢ Continuous ((fun p ↦ p.1 - p.2) ∘ fun x ↦ (x, a))
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
x : ↑(Ici a)
⊢ projIci a ↑x = x

Tactic:
cases x; apply projIci_of_mem

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

Goal state before:
pp: case neg
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 := fun x y ↦ if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : 1 / 2 ∈ Ioo 0 1
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ ↑(d x y)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
x₁ x₂ x₃ x₄ : X
H : ¬∃ n, (x₁, x₄) ∉ U n
⊢ d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))

Tactic:
· exact (dif_neg H).trans_le zero_le

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

Goal state before:
pp: case refine_2
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 := fun x y ↦ if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : ↑0 < ↑(1 / 2) ∧ ↑(1 / 2) < ↑1
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ ↑(d x y)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
hd_le : ∀ (x y : X), ↑(d x y) ≤ 2 * dist x y
n : ℕ
x✝ : True
x : X × X
hx : x ∉ U n
⊢ (1 / 2) ^ n ≤ d x.1 x.2

Tactic:
hle_d

Goal state after:
case refine_2
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 := fun x y ↦ if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : ↑0 < ↑(1 / 2) ∧ ↑(1 / 2) < ↑1
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ ↑(d x y)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
hd_le : ∀ (x y : X), ↑(d x y) ≤ 2 * dist x y
n : ℕ
x✝ : True
x : X × X
hx : x ∉ U n
⊢ (x.1, x.2) ∉ U n
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: G : Type u_4
inst✝ : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖(u m)⁻¹ * u n‖ < C
this : ∀ (n : ℕ), ‖u n‖ ≤ C + ‖u 0‖
⊢ BddAbove (Set.range fun n ↦ ‖u n‖)

Tactic:
bddAbove_def

Goal state after:
G : Type u_4
inst✝ : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖(u m)⁻¹ * u n‖ < C
this : ∀ (n : ℕ), ‖u n‖ ≤ C + ‖u 0‖
⊢ ∃ x, ∀ y ∈ Set.range fun n ↦ ‖u n‖, y ≤ x
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
f : α → Prop
h : MeasurableSet (f ⁻¹' {True})
x : Prop
⊢ MeasurableSet (f ⁻¹' {x})

Tactic:
by_cases hx : x

Goal state after:
case pos
α : Type u_1
mα : MeasurableSpace α
f : α → Prop
h : MeasurableSet (f ⁻¹' {True})
x : Prop
hx : x
⊢ MeasurableSet (f ⁻¹' {x})

case neg
α : Type u_1
mα : MeasurableSpace α
f : α → Prop
h : MeasurableSet (f ⁻¹' {True})
x : Prop
hx : ¬x
⊢ MeasurableSet (f ⁻¹' {x})
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
⊢ sign (x * y) = sign x * sign y

Tactic:
rcases lt_trichotomy x 0 with (hx | hx | hx)

Goal state after:
case inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : x < 0
⊢ sign (x * y) = sign x * sign y

case inr.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : x = 0
⊢ sign (x * y) = sign x * sign y

case inr.inr
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : 0 < x
⊢ sign (x * y) = sign x * sign y
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case coe_coe
x✝ y✝ : ℝ
⊢ sign (↑x✝ * ↑y✝) = sign ↑x✝ * sign ↑y✝

Tactic:
simp only [← coe_mul, sign_coe, _root_.sign_mul]

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

Goal state before:
pp: case mp.zero
x y : EReal
h : ↑(sign x) * ↑x.abs ≤ ↑(sign y) * ↑y.abs
hs : sign x = sign y
hy : sign y = zero
⊢ sign x = neg ∧ zero = neg ∧ y.abs ≤ x.abs ∨ sign x = zero ∧ zero = zero ∨ sign x = pos ∧ zero = pos ∧ x.abs ≤ y.abs

Tactic:
hs,

Goal state after:
case mp.zero
x y : EReal
h : ↑(sign y) * ↑x.abs ≤ ↑(sign y) * ↑y.abs
hs : sign x = sign y
hy : sign y = zero
⊢ sign y = neg ∧ zero = neg ∧ y.abs ≤ x.abs ∨ sign y = zero ∧ zero = zero ∨ sign y = pos ∧ zero = pos ∧ x.abs ≤ y.abs
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case mp.neg
x y : EReal
h : ↑(sign x) * ↑x.abs ≤ ↑(sign y) * ↑y.abs
hs : sign x = sign y
hy : sign y = neg
⊢ sign x = neg ∧ neg = neg ∧ y.abs ≤ x.abs ∨ sign x = zero ∧ neg = zero ∨ sign x = pos ∧ neg = pos ∧ x.abs ≤ y.abs

Tactic:
hs,

Goal state after:
case mp.neg
x y : EReal
h : ↑(sign y) * ↑x.abs ≤ ↑(sign y) * ↑y.abs
hs : sign x = sign y
hy : sign y = neg
⊢ sign y = neg ∧ neg = neg ∧ y.abs ≤ x.abs ∨ sign y = zero ∧ neg = zero ∨ sign y = pos ∧ neg = pos ∧ x.abs ≤ y.abs
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case mp.pos
x y : EReal
h : ↑(sign x) * ↑x.abs ≤ ↑(sign y) * ↑y.abs
hs : sign x = sign y
hy : sign y = pos
⊢ sign x = neg ∧ pos = neg ∧ y.abs ≤ x.abs ∨ sign x = zero ∧ pos = zero ∨ sign x = pos ∧ pos = pos ∧ x.abs ≤ y.abs

Tactic:
hs,

Goal state after:
case mp.pos
x y : EReal
h : ↑(sign y) * ↑x.abs ≤ ↑(sign y) * ↑y.abs
hs : sign x = sign y
hy : sign y = pos
⊢ sign y = neg ∧ pos = neg ∧ y.abs ≤ x.abs ∨ sign y = zero ∧ pos = zero ∨ sign y = pos ∧ pos = pos ∧ x.abs ≤ y.abs
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_4
s : Set α
c : ℝ≥0∞
⊢ ∑' (x : ↑s), c = ↑s.encard * c

Tactic:
simp [← tsum_set_one, ← ENNReal.tsum_mul_right]

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
γ : Type u_4
inst✝ : LinearOrder γ
ι : Type u_5
f : ι → α → γ
ks : IsCompact s
I : Set ι
c : γ
hfi : ∀ i ∈ I, LowerSemicontinuousOn (f i) s
x✝ : ∃ u, ∀ x ∈ s, ∃ i ∈ u, c < f (↑i) x
u : Finset ↑I
hu : ∀ x ∈ s, ∃ i ∈ u, c < f (↑i) x
⊢ s ∩ ⋂ i ∈ I, f i ⁻¹' Iic c = ∅

Tactic:
· rw [Set.eq_empty_iff_forall_notMem]
    simp only [mem_inter_iff, mem_iInter, mem_preimage, mem_Iic, not_and, not_forall,
      exists_prop, not_le]
    grind

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁵ : DivisionSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
x : 𝕜
⊢ Tendsto (fun n ↦ ↑n / (↑n + x)) atTop (𝓝 1)

Tactic:
convert! Tendsto.congr' ((eventually_ne_atTop 0).mp (Eventually.of_forall fun n hn ↦ _)) _

Goal state after:
case convert_2
𝕜 : Type u_4
inst✝⁵ : DivisionSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
x : 𝕜
⊢ ℕ → 𝕜

case convert_5
𝕜 : Type u_4
inst✝⁵ : DivisionSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
x : 𝕜
n : ℕ
hn : n ≠ 0
⊢ ?convert_2 n = ↑n / (↑n + x)

case convert_6
𝕜 : Type u_4
inst✝⁵ : DivisionSemiring 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
x : 𝕜
⊢ Tendsto ?convert_2 atTop (𝓝 1)
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case mpr
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
⊢ (∀ (x : α × γ), (x.1 ∈ s → x.2 < f x.1) → ∀ᶠ (a : α × γ) in 𝓝 x, a.1 ∈ s → a.2 < f a.1) →
    ∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x

Tactic:
intro hf x _ y hy
    exact ((Continuous.prodMk_left y).tendsto x).eventually (hf (x, y) (fun _ => hy))

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

Goal state before:
pp: α : Type u_3
f : Filter α
u : α → EReal
inst✝ : f.NeBot
c : EReal
h₁ : c ≤ 0
h₂ : c ≠ ⊥
⊢ limsup (fun x ↦ c * u x) f = c * liminf u f

Tactic:
simpa [limsup_neg] using
    limsup_const_mul_of_nonneg_of_ne_top (u := -u) (c := -c) (by aesop) (by aesop)

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : Semiring α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : ExistsAddOfLE α
inst✝ : Archimedean α
r : α
h : 1 < r
⊢ Tendsto (fun n ↦ r ^ n) atTop atTop

Tactic:
obtain ⟨r, r0, rfl⟩ := exists_pos_add_of_lt' h
  rw [add_comm]
  exact tendsto_add_one_pow_atTop_atTop_of_pos r0

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: r : ℝ≥0∞
hr : r < 1
⊢ Tendsto (fun n ↦ r ^ n) atTop (𝓝 0)

Tactic:
rcases ENNReal.lt_iff_exists_coe.1 hr with ⟨r, rfl, hr'⟩

Goal state after:
r : ℝ≥0
hr' hr : ↑r < 1
⊢ Tendsto (fun n ↦ ↑r ^ n) atTop (𝓝 0)