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

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

Tactic:
intro n

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

Goal state before:
pp: a b : EReal
⊢ -b ≤ - -a ↔ -b ≤ a

Tactic:
neg_neg

Goal state after:
a b : EReal
⊢ -b ≤ a ↔ -b ≤ a
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b : EReal
⊢ -a ≤ b ↔ -b ≤ a

Tactic:
by
  rw [← neg_le_neg_iff, neg_neg]

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

Goal state before:
pp: a b : EReal
⊢ - -b ≤ -a ↔ b ≤ -a

Tactic:
neg_neg

Goal state after:
a b : EReal
⊢ b ≤ -a ↔ b ≤ -a
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b : EReal
⊢ a ≤ -b ↔ b ≤ -a

Tactic:
by
  rw [← neg_le_neg_iff, neg_neg]

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

Goal state before:
pp: a b : EReal
⊢ -b < - -a ↔ -b < a

Tactic:
neg_neg

Goal state after:
a b : EReal
⊢ -b < a ↔ -b < a
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b : EReal
⊢ - -b < -a ↔ b < -a

Tactic:
neg_neg

Goal state after:
a b : EReal
⊢ b < -a ↔ b < -a
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x y : EReal
h1 : x ≠ ⊥ ∨ y ≠ ⊥
h2 : x ≠ ⊤ ∨ y ≠ ⊤
⊢ -x + - -y = -x + y

pp: x y : EReal
h1 : x ≠ ⊥ ∨ y ≠ ⊥
h2 : x ≠ ⊤ ∨ y ≠ ⊤
⊢ x ≠ ⊥ ∨ -y ≠ ⊤

pp: x y : EReal
h1 : x ≠ ⊥ ∨ y ≠ ⊥
h2 : x ≠ ⊤ ∨ y ≠ ⊤
⊢ x ≠ ⊤ ∨ -y ≠ ⊥

Tactic:
neg_neg

Goal state after:
x y : EReal
h1 : x ≠ ⊥ ∨ y ≠ ⊥
h2 : x ≠ ⊤ ∨ y ≠ ⊤
⊢ -x + y = -x + y

x y : EReal
h1 : x ≠ ⊥ ∨ y ≠ ⊥
h2 : x ≠ ⊤ ∨ y ≠ ⊤
⊢ x ≠ ⊥ ∨ -y ≠ ⊤

x y : EReal
h1 : x ≠ ⊥ ∨ y ≠ ⊥
h2 : x ≠ ⊤ ∨ y ≠ ⊤
⊢ x ≠ ⊤ ∨ -y ≠ ⊥
Module: Mathlib.Data.EReal.Operations

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

Tactic:
neg_neg

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

Goal state before:
pp: case inr
x : ℝ
h : x ≤ 0
⊢ ↑x = - -↑x

pp: case inr.hr
x : ℝ
h : x ≤ 0
⊢ 0 ≤ -x

Tactic:
neg_neg

Goal state after:
case inr
x : ℝ
h : x ≤ 0
⊢ ↑x = ↑x

case inr.hr
x : ℝ
h : x ≤ 0
⊢ 0 ≤ -x
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b c : EReal
h : a < b + c
⊢ a < b + - -c

Tactic:
neg_neg

Goal state after:
a b c : EReal
h : a < b + c
⊢ a < b + c
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
⊢ bliminf s cofinite p = {x | {n | p n ∧ x ∉ s n}.Finite}

Tactic:
by
  rw [← compl_inj_iff]
  simp only [bliminf_eq_iSup_biInf, compl_iInf, compl_iSup, ← blimsup_eq_iInf_biSup,
    cofinite.blimsup_set_eq]
  rfl

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

Goal state before:
pp: a b c : EReal
h : ∀ a' < a, ∀ b' < b, a' + b' ≤ c
⊢ a + b ≤ c

Tactic:
by
  refine le_of_forall_lt_imp_le_of_dense fun d hd ↦ ?_
  obtain ⟨a', ha', hd⟩ := exists_lt_add_left hd
  obtain ⟨b', hb', hd⟩ := exists_lt_add_right hd
  exact hd.le.trans (h _ ha' _ hb')

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

Goal state before:
pp: case neg_bot
x✝ : ℝ
h : x✝ < 0
⊢ (↑x✝ * ⊥).toReal = (↑x✝).toReal * ⊥.toReal

Tactic:
simp [coe_mul_bot_of_neg h]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
inst✝ : DenselyOrdered β
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, y ≤ u a
y : β
y_x : y < x
⊢ y < limsup u f

Tactic:
obtain ⟨z, y_z, z_x⟩ := exists_between y_x

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
inst✝ : DenselyOrdered β
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, y ≤ u a
y : β
y_x : y < x
z : β
y_z : y < z
z_x : z < x
⊢ y < limsup u f
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case neg_left
x✝ y✝ : EReal
h : -x✝ * y✝ = -(x✝ * y✝)
⊢ x✝ * y✝ = - -(x✝ * y✝)

Tactic:
neg_neg

Goal state after:
case neg_left
x✝ y✝ : EReal
h : -x✝ * y✝ = -(x✝ * y✝)
⊢ x✝ * y✝ = x✝ * y✝
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b : EReal
⊢ -a * b = ⊤ ↔ a = ⊥ ∧ 0 < b ∨ 0 < a ∧ b = ⊥ ∨ a = ⊤ ∧ b < 0 ∨ a < 0 ∧ b = ⊤

Tactic:
mul_eq_top,

Goal state after:
a b : EReal
⊢ -a = ⊥ ∧ b < 0 ∨ -a < 0 ∧ b = ⊥ ∨ -a = ⊤ ∧ 0 < b ∨ 0 < -a ∧ b = ⊤ ↔
    a = ⊥ ∧ 0 < b ∨ 0 < a ∧ b = ⊥ ∨ a = ⊤ ∧ b < 0 ∨ a < 0 ∧ b = ⊤
Module: Mathlib.Order.Filter.AtTopBot.BigOperators

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
s : Finset β
⊢ ∃ v, ∀ (v' : Finset α), v ⊆ v' → ∃ u', s ⊆ u' ∧ ∏ x ∈ u', f x = ∏ b ∈ v', f (g b)

pp: case a
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
s : Finset α
⊢ ∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', s ⊆ u' ∧ ∏ x ∈ u', f (g x) = ∏ b ∈ v', f b

Tactic:
· refine ⟨s.preimage g hg.injOn, fun t ht => ?_⟩
    refine ⟨t.image g ∪ s, Finset.subset_union_right, ?_⟩
    rw [← Finset.prod_image hg.injOn]
    refine (prod_subset subset_union_left ?_).symm
    simp only [Finset.mem_union, Finset.mem_image]
    refine fun y hy hyt => hf y (mt ?_ hyt)
    rintro ⟨x, rfl⟩
    exact ⟨x, ht (Finset.mem_preimage.2 <| hy.resolve_left hyt), rfl⟩

Goal state after:
case a
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
s : Finset α
⊢ ∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', s ⊆ u' ∧ ∏ x ∈ u', f (g x) = ∏ b ∈ v', f b
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
h✝ : ∀ s ∈ 𝓝 1, ∃ a, ∀ (b : Finset β × Finset β), a ≤ b → (∏ b ∈ b.2, f b) / ∏ b ∈ b.1, f b ∈ s
e : Set α
he : e ∈ 𝓝 1
s₁ s₂ : Finset β
h : ∀ (b : Finset β × Finset β), (s₁, s₂) ≤ b → (∏ b ∈ b.2, f b) / ∏ b ∈ b.1, f b ∈ e
⊢ ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e

Tactic:
use s₁ ∪ s₂

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
h✝ : ∀ s ∈ 𝓝 1, ∃ a, ∀ (b : Finset β × Finset β), a ≤ b → (∏ b ∈ b.2, f b) / ∏ b ∈ b.1, f b ∈ s
e : Set α
he : e ∈ 𝓝 1
s₁ s₂ : Finset β
h : ∀ (b : Finset β × Finset β), (s₁, s₂) ≤ b → (∏ b ∈ b.2, f b) / ∏ b ∈ b.1, f b ∈ e
⊢ ∀ (t : Finset β), Disjoint t (s₁ ∪ s₂) → ∏ b ∈ t, f b ∈ e
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
K : Type u_4
inst✝² : CommGroupWithZero K
inst✝¹ : TopologicalSpace K
f g : α → K
inst✝ : SeparatelyContinuousMul K
c : K
hc : HasProd f c
s : Finset α
hs : ∀ a ∈ s, f a ≠ 0
hs' : ∀ a ∉ s, f a = g a
t : Finset α
ht : s ⊆ t
⊢ (∏ i ∈ s, g i) * ∏ i ∈ t \ s, g i = ∏ i ∈ t, g i

Tactic:
rw [← prod_union disjoint_sdiff, union_sdiff_of_subset ht]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Set β
f : β → α
⊢ ∏' (x : ↑s), f ↑x = ∏' (x : β), s.mulIndicator f x

Tactic:
rw [← tprod_subtype_eq_of_mulSupport_subset Set.mulSupport_mulIndicator_subset, tprod_congr]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Set β
f : β → α
⊢ ∀ (b : ↑s), f ↑b = s.mulIndicator f ↑b
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: G : Type u_2
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
f : ℕ → G
⊢ (Multipliable fun n ↦ f ↑n) ↔ Multipliable f

Tactic:
rw [multipliable_pnat_iff_multipliable_succ, multipliable_nat_add_iff]

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

Goal state before:
pp: G : Type u_2
inst✝⁴ : CommGroup G
inst✝³ : UniformSpace G
inst✝² : IsUniformGroup G
inst✝¹ : CompleteSpace G
inst✝ : T2Space G
f : ℤ → G
hf2 : Multipliable f
h1 : Multipliable fun n ↦ f ↑n
h2 : Multipliable fun n ↦ f (-↑n)
h3 : Multipliable fun n ↦ f ↑↑n
⊢ Multipliable fun x ↦ f (-↑(x + 1))

Tactic:
multipliable_nat_add_iff 1 (f := (fun x ↦ f (-x)))

Goal state after:
G : Type u_2
inst✝⁴ : CommGroup G
inst✝³ : UniformSpace G
inst✝² : IsUniformGroup G
inst✝¹ : CompleteSpace G
inst✝ : T2Space G
f : ℤ → G
hf2 : Multipliable f
h1 : Multipliable fun n ↦ f ↑n
h2 : Multipliable fun n ↦ f (-↑n)
h3 : Multipliable fun n ↦ f ↑↑n
⊢ Multipliable fun x ↦ f (-↑x)
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
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x y : X
l : List X
this : IsTrans X fun x y ↦ d x y = 0
⊢ ∀ (n : ℕ), l.length = n → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum

Tactic:
intro n

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
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x y : X
l : List X
this : IsTrans X fun x y ↦ d x y = 0
n : ℕ
⊢ l.length = n → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝¹ : UniformSpace X
s : Set X
inst✝ : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
⊢ ∃ x ∈ s, l ≤ 𝓝 x

Tactic:
have hWV' : ∀ n, W n ⊆ V n := fun n ⟨x, y⟩ hx =>
    @hWV n (x, y) ⟨x, refl_mem_uniformity <| hW _, hx⟩

Goal state after:
X : Type u_1
inst✝¹ : UniformSpace X
s : Set X
inst✝ : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
⊢ ∃ x ∈ s, l ≤ 𝓝 x
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_1
l : Filter α
f g : α → ℝ≥0∞
hfi : ∀ᶠ (x : α) in l, f x ≠ ∞
hgi : ∀ᶠ (x : α) in l, g x ≠ ∞
hfg : (fun x ↦ (f x).toReal) =ᶠ[l] fun x ↦ (g x).toReal
⊢ f =ᶠ[l] g

Tactic:
filter_upwards [hfi, hgi, hfg] with _ hfx hgx _

Goal state after:
α : Type u_1
l : Filter α
f g : α → ℝ≥0∞
hfi : ∀ᶠ (x : α) in l, f x ≠ ∞
hgi : ∀ᶠ (x : α) in l, g x ≠ ∞
hfg : (fun x ↦ (f x).toReal) =ᶠ[l] fun x ↦ (g x).toReal
a✝¹ : α
hfx : f a✝¹ ≠ ∞
hgx : g a✝¹ ≠ ∞
a✝ : (f a✝¹).toReal = (g a✝¹).toReal
⊢ f a✝¹ = g 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)

pp: case neg
α : Type u
inst✝² : UniformSpace α
β : Type v
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace β
f : α → β
hf : ¬UniformContinuous f
⊢ UniformContinuous (extend f)

Tactic:
· rw [extend, if_pos hf]
    exact uniformContinuous_uniformly_extend isUniformInducing_pureCauchy denseRange_pureCauchy hf

Goal state after:
case neg
α : 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: n : ℕ
⊢ Continuous fun x ↦ x ^ Int.negSucc n

Tactic:
by simpa using (ENNReal.continuous_pow _).fun_inv

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

Goal state before:
pp: s : Set ℝ≥0∞
s_count : s.Countable
s_dense : Dense s
hs : (∀ (x : ℝ≥0∞), IsBot x → x ∉ s) ∧ ∀ (x : ℝ≥0∞), IsTop x → x ∉ s
⊢ ∃ s, s.Countable ∧ Dense s ∧ 0 ∉ s ∧ ∞ ∉ s

Tactic:
exact ⟨s, s_count, s_dense, fun h => hs.1 0 (by simp) h, fun h => hs.2 ∞ (by simp) h⟩

Goal state after:
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 : α → ℝ := fun y ↦ ⨅ x, f ↑x + ↑K * dist y ↑x
B : ∀ (y : α), BddBelow (range fun x ↦ f ↑x + ↑K * dist y ↑x)
E : EqOn f g s
x y : α
z : ↑s
⊢ g x - ↑K * dist x y ≤ f ↑z + ↑K * dist y ↑z

Tactic:
rw [sub_le_iff_le_add]

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
B : ∀ (y : α), BddBelow (range fun x ↦ f ↑x + ↑K * dist y ↑x)
E : EqOn f g s
x y : α
z : ↑s
⊢ g x ≤ f ↑z + ↑K * dist y ↑z + ↑K * dist x y
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
z x y : α
⊢ dist (x ⊔ z) (y ⊔ z) ≤ dist x y

Tactic:
dist_eq_norm,

Goal state after:
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
z x y : α
⊢ ‖x ⊔ z - y ⊔ z‖ ≤ dist x y
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₁ x₂ y : ℝ≥0
⊢ dist (x₁ • y) (x₂ • y) ≤ dist x₁ x₂ * dist y 0

Tactic:
convert! dist_pair_smul (x₁ : ℝ) x₂ (y : ℝ) using 1

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

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
f : E → F
K : ℝ≥0
h : LipschitzWith K f
hf : f 1 = 1
x : E
⊢ ‖f x‖ ≤ ↑K * ‖x‖

Tactic:
simpa only [dist_one_right, hf] using h.dist_le_mul x 1

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

Goal state before:
pp: α : Type u_2
inst✝ : NormedDivisionRing α
a : α
ha : a ≠ 0
⊢ ‖a⁻¹‖ₑ = ‖a‖ₑ⁻¹

Tactic:
by simp [enorm, ENNReal.coe_inv, ha]

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

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

Tactic:
dist_eq_norm,

Goal state after:
α : Type u_2
inst✝ : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
⊢ ‖z⁻¹ - w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
u v : ℕ → E
N : ℕ
huv : ∀ n ≥ N, u n = v n
hv : CauchySeq fun n ↦ ∏ k ∈ range (n + 1), v k
d : ℕ → E := fun n ↦ ∏ k ∈ range (n + 1), u k / v k
⊢ ∀ n ≥ N, d n = d N

Tactic:
intro n

Goal state after:
E : Type u_2
inst✝ : SeminormedCommGroup E
u v : ℕ → E
N : ℕ
huv : ∀ n ≥ N, u n = v n
hv : CauchySeq fun n ↦ ∏ k ∈ range (n + 1), v k
d : ℕ → E := fun n ↦ ∏ k ∈ range (n + 1), u k / v k
n : ℕ
⊢ n ≥ N → d n = d N
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: case mpr
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
this : ∃ ε > 0, ∀ (y : 𝕜), dist y 0 < ε → y = 0
⊢ ‖x‖ = 1

Tactic:
dist_eq_norm,

Goal state after:
case mpr
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
this : ∃ ε > 0, ∀ (y : 𝕜), ‖y - 0‖ < ε → y = 0
⊢ ‖x‖ = 1
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
⊢ ∀ (n : ℕ), ‖u n‖ ≤ C + ‖u 0‖

Tactic:
intro n

Goal state after:
G : Type u_4
inst✝ : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖(u m)⁻¹ * u n‖ < C
n : ℕ
⊢ ‖u n‖ ≤ C + ‖u 0‖
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝ : NontriviallyNormedField α
x : α
ε : ℝ
ε0 : ε > 0
b : α
hb0 : 0 < ‖b‖
hbε : ‖b‖ < ε
⊢ dist (x + b) x < ε

Tactic:
dist_eq_norm,

Goal state after:
α : Type u_2
inst✝ : NontriviallyNormedField α
x : α
ε : ℝ
ε0 : ε > 0
b : α
hb0 : 0 < ‖b‖
hbε : ‖b‖ < ε
⊢ ‖x + b - x‖ < ε
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:
dist_eq_norm,

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : SeminormedRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
x y : β
⊢ ‖s • x - s • y‖ = ‖s‖ * ‖x - y‖
Module: Mathlib.Analysis.Normed.MulAction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : IsBoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r‖ * (‖r⁻¹‖ * ‖r • x‖) = ‖r • x‖

Tactic:
rw [norm_inv, ← mul_assoc, mul_inv_cancel₀ (mt norm_eq_zero.1 h), one_mul]

Goal state after:
Module: Mathlib.Data.Finset.Update

Goal state before:
pp: case neg
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : (i_1 : ↥{i}) → π ↑i_1
j : ι
hj : ¬j = i
⊢ updateFinset x {i} y j = update x i (y ⟨i, ⋯⟩) j

Tactic:
· simp [hj, updateFinset]

Goal state after:
Module: Mathlib.Data.Finset.Update

Goal state before:
pp: case neg
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : π i
j : ι
hj : ¬j = i
⊢ update x i y j = updateFinset x {i} (uniqueElim y) j

Tactic:
· simp [hj, updateFinset]

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

Goal state before:
pp: case neg
𝕜 : Type u_4
h : NormedField 𝕜
H : ¬∃ x, x ≠ 0 ∧ ‖x‖ ≠ 1
⊢ (∃ ε > 0, ∀ (y : 𝕜), dist y 0 < ε → y = 0) ∨ Nonempty { h' // h'.toNormedField = h }

Tactic:
dist_eq_norm,

Goal state after:
case neg
𝕜 : Type u_4
h : NormedField 𝕜
H : ¬∃ x, x ≠ 0 ∧ ‖x‖ ≠ 1
⊢ (∃ ε > 0, ∀ (y : 𝕜), ‖y - 0‖ < ε → y = 0) ∨ Nonempty { h' // h'.toNormedField = h }
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (s₁ ∪ s₂)

Tactic:
by
  rw [union_eq_iUnion]
  exact .iUnion (Bool.forall_bool.2 ⟨h₂, h₁⟩)

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
x y : 𝕜
⊢ dist ((algebraMap 𝕜 𝕜') x) ((algebraMap 𝕜 𝕜') y) = dist x y

Tactic:
dist_eq_norm,

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
x y : 𝕜
⊢ ‖(algebraMap 𝕜 𝕜') x - (algebraMap 𝕜 𝕜') y‖ = dist x y
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
x y : 𝕜
⊢ ‖(algebraMap 𝕜 𝕜') x - (algebraMap 𝕜 𝕜') y‖ = dist x y

Tactic:
dist_eq_norm,

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
x y : 𝕜
⊢ ‖(algebraMap 𝕜 𝕜') x - (algebraMap 𝕜 𝕜') y‖ = ‖x - y‖
Module: Mathlib.MeasureTheory.OuterMeasure.Basic

Goal state before:
pp: case inr.refine_2
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ∞
n : ℕ
h' : Monotone s
x : α
this✝ : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
hnj : n < j
this : j - (n + 1) + n + 1 = j
⊢ j - (n + 1) + n < j

Tactic:
rw [← Nat.succ_le_iff, Nat.succ_eq_add_one, this]

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
h : (s.pi t).Nonempty
⊢ MeasurableSet (s.pi t) ↔ ∀ i ∈ s, MeasurableSet (t i)

Tactic:
by
  classical
    rcases h with ⟨f, hf⟩
    refine ⟨fun hst i hi => ?_, MeasurableSet.pi hs⟩
    convert! measurable_update f (a := i) hst
    rw [update_preimage_pi hi]
    exact fun j hj _ => hf j hj

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

Goal state before:
pp: case neg
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
hf : ¬∑' (i : α), f i = 0
this : Tendsto (fun s ↦ ∑ j ∈ s, a * f j) atTop (𝓝 (a * ∑' (i : α), f i))
⊢ ∑' (i : α), a * f i = a * ∑' (i : α), f i

Tactic:
exact HasSum.tsum_eq this

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

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

Tactic:
rw [← x.sign_mul_abs, ← y.sign_mul_abs] at h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x : α
⊢ LowerHemicontinuousAt f x ↔
    ∀ (u : Set β), IsOpen[inst✝] u → (f x ∩ u).Nonempty → ∀ᶠ (x' : α) in 𝓝 x, (f x' ∩ u).Nonempty

Tactic:
by
  simp +contextual [SemicontinuousAt]

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

Goal state before:
pp: case coe.inl
a : ℝ
a_neg : a < 0
⊢ (↑(- -a))⁻¹ = (↑a)⁻¹

Tactic:
neg_neg

Goal state after:
case coe.inl
a : ℝ
a_neg : a < 0
⊢ (↑a)⁻¹ = (↑a)⁻¹
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case coe.inl
a : ℝ
a_neg : a < 0
⊢ ↑(- -a)⁻¹ = ↑a⁻¹

Tactic:
neg_neg

Goal state after:
case coe.inl
a : ℝ
a_neg : a < 0
⊢ ↑a⁻¹ = ↑a⁻¹
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 ↦ _)) _
  · exact fun n : ℕ ↦ 1 / (1 + x / n)
  · simp [Nat.cast_ne_zero.mpr hn, add_div']
  · have : 𝓝 (1 : 𝕜) = 𝓝 (1 / (1 + x * (0 : 𝕜))) := by
      rw [mul_zero, add_zero, div_one]
    rw [this]
    refine tendsto_const_nhds.div (tendsto_const_nhds.add ?_) (by simp)
    simp_rw [div_eq_mul_inv]
    exact tendsto_const_nhds.mul tendsto_inv_atTop_nhds_zero_nat

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

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

Tactic:
← ENNReal.coe_zero

Goal state after:
r : ℝ≥0
hr' hr : ↑r < 1
⊢ Tendsto (fun n ↦ ↑r ^ n) atTop (𝓝 ↑0)
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: r : ℝ≥0
hr : r < 1
⊢ HasSum (fun a ↦ ↑r ^ a) (↑1 - ↑r)⁻¹

Tactic:
exact hasSum_geometric_of_lt_one r.coe_nonneg hr

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

Goal state before:
pp: ⊢ ∑' (m : ℕ), 2⁻¹ ^ (m + 1) = 1

Tactic:
ENNReal.tsum_geometric_add_one,

Goal state after:
⊢ 2⁻¹ * (1 - 2⁻¹)⁻¹ = 1
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case pos
x : EReal × EReal
y : EReal
hx₁ : ¬x.1 = ⊥
hx₂ : x.2 = ⊥
⊢ (fun x1 x2 ↦ (fun p ↦ p.1 + p.2) x1 > x2) x y →
    ∀ᶠ (x' : EReal × EReal) in 𝓝 x, (fun x1 x2 ↦ (fun p ↦ p.1 + p.2) x1 > x2) x' y

Tactic:
simp [hx₂]

Goal state after: