mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
g : γ → β
f : β → α
hg : Injective g
⊢ ∏' (x : ↑(Set.range g)), f ↑x = ∏' (x : γ), f (g x)

Tactic:
← Set.image_univ,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
g : γ → β
f : β → α
hg : Injective g
⊢ ∏' (x : ↑(g '' Set.univ)), f ↑x = ∏' (x : γ), f (g x)
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
g : γ → α
e : ↑(mulSupport f) ≃ ↑(mulSupport g)
he : ∀ (x : ↑(mulSupport f)), g ↑(e x) = f ↑x
⊢ mulSupport g ⊆ Set.range (Subtype.val ∘ ⇑e)

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoidWithZero α
inst✝² : TopologicalSpace α
L : SummationFilter β
inst✝¹ : Nonempty β
inst✝ : L.LeAtTop
b : β
⊢ 0 = 0

Tactic:
by simp

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

Goal state before:
pp: case inr
α : Type u_2
L : SummationFilter α
f : α → ℝ≥0
hL : L.filter = ⊥
⊢ Summable (fun a ↦ ↑(f a)) L ↔ Summable f L

Tactic:
simp [Summable, HasSum, hL]

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

Goal state before:
pp: α : Type u_2
L : SummationFilter α
f : α → ℝ≥0
x : ℝ≥0
⊢ (toRealHom x).toNNReal = x

Tactic:
by simp

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

Goal state before:
pp: f : ℕ → ℝ≥0
h_ant : Antitone f
⊢ BddBelow (range f)

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
g : β → α
hg : Function.RightInverse g f
⊢ LipschitzWith K g

Tactic:
by
  intro x y
  have := hf (g x) (g y)
  rwa [hg x, hg y] at this

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

Goal state before:
pp: ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
E : ι → Type u_3
inst✝¹ : (i : ι) → PseudoEMetricSpace (E i)
inst✝ : (i : ι) → Zero (E i)
i : ι
x y : E i
⊢ edist x y ≤ edist (Pi.single i x i) (Pi.single i y i)

Tactic:
by simp

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 : X
⊢ (zipWith d [x] ([] ++ [y])).sum = d x y

Tactic:
by simp

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
h : α ≃ᵢ β
⊢ range ⇑h = univ

Tactic:
by simp

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
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x y : X
⊢ ↑(d x y) ≤ 2 * dist x y

Tactic:
rw [dist_ofPreNNDist, ← NNReal.coe_two, ← NNReal.coe_mul, NNReal.mul_iInf, NNReal.coe_le_coe]

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
⊢ d x y ≤ ⨅ i, 2 * (zipWith d (x :: i) (i ++ [y])).sum
Module: Mathlib.Topology.Sequences

Goal state before:
pp: case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
x : ℕ → X
inst✝ : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), y n ∈ ⋃ i, closure[inst✝¹] {x i}
hy' : Tendsto y atTop (𝓝 l)
hm : ∃ m, ∃ᶠ (n : ℕ) in atTop, y n ∈ closure[inst✝¹] {x m}
⊢ l ∈ ⋃ i, closure[inst✝¹] {x i}

Tactic:
obtain ⟨m, pm⟩ := hm
    exact subset_iUnion _ m (isClosed_closure.mem_of_frequently_of_tendsto pm hy')

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
x : ℕ → X
inst✝ : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), y n ∈ ⋃ i, closure[inst✝¹] {x i}
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst✝¹] {x m}
j a : ℕ
⊢ (Iic a).Finite

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝ : SeminormedGroup E
f : α → E
a : Filter α
⊢ Tendsto (fun e ↦ ‖(f e)⁻¹ * 1‖) a (𝓝 0) ↔ Tendsto (fun x ↦ ‖f x‖) a (𝓝 0)

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝ : SeminormedGroup E
f : α → E
a : Filter α
⊢ Tendsto (fun e ↦ ‖(f e)⁻¹ * 1‖ₑ) a (𝓝 0) ↔ Tendsto (fun x ↦ ‖f x‖ₑ) a (𝓝 0)

Tactic:
by simp

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

Goal state before:
pp: E : Type u_4
inst✝ : SeminormedGroup E
x : E
⊢ ∀ᶠ (n : E) in 𝓝 x, ‖n⁻¹ * x‖ ∈ Set.Ici 0

Tactic:
by simp

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

Goal state before:
pp: E : Type u_4
inst✝ : SeminormedCommGroup E
x : E
⊢ ∀ᶠ (n : E) in 𝓝 x, ‖n / x‖ ∈ Set.Ici 0

Tactic:
by simp

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
h : 0 ∈ s
⊢ IsBot 0

Tactic:
by simp

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
h : ∞ ∈ s
⊢ IsTop ∞

Tactic:
by simp

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
⊢ ∀ᶠ (x : ℝ≥0∞) in map u f, (fun x1 x2 ↦ x1 ≥ x2) x 0

Tactic:
by simp

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
liminf_le : liminf u f ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
aux' : (liminf u f).toReal = b.truncateToReal (liminf u f)
⊢ ∀ (x : ℝ≥0∞), (fun x1 x2 ↦ x1 ≥ x2) x 0

Tactic:
by simp

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)
⊢ ∀ (a : ℝ≥0∞), (∀ᶠ (x : ℝ≥0∞) in map u f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) 0 a

Tactic:
by simp

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)
⊢ ∀ (x : ℝ≥0∞), (fun x1 x2 ↦ x2 ≤ x1) x 0

Tactic:
by simp

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

Goal state before:
pp: ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
⊢ ∀ (x : ι), f x ≤ (f + g) x

Tactic:
by simp

Goal state after:
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, b ≤ (f + g) n
a : ℝ≥0∞
hab : a < b
i : ι
hfg : b ≤ (f + g) i
hg : g i ≤ min (b - a) 1
⊢ min (b - a) 1 < ∞

Tactic:
by simp

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

Goal state before:
pp: case hbc
α : Type u
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : Nonempty ↑s
g : α → ℝ := ⋯
y z : α
hz : z ∈ s
t : ↑s
⊢ dist z ↑t ≤ dist y z + dist y ↑t

Tactic:
apply dist_triangle_left

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

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : EMetricSpace β
inst✝ : CompleteSpace β
s : Set α
hs : Dense s
f : ↑s → β
K : ℝ≥0
hf : LipschitzWith K f
this :
  Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
    (hs.extend f)
⊢ ↑K ≠ ∞

Tactic:
by simp

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 : α × β
⊢ x ∈ Metric.ball 0 (dist x 0 + 1)

Tactic:
by simp

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 α β
inst✝¹ : SMul αᵐᵒᵖ β
inst✝ : IsCentralScalar α β
x₁ x₂ : α
y : β
⊢ dist (MulOpposite.op x₁ • y) (MulOpposite.op x₂ • y) ≤ dist (MulOpposite.op x₁) (MulOpposite.op x₂) * dist y 0

Tactic:
simpa only [op_smul_eq_smul] using! dist_pair_smul x₁ x₂ y

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

Goal state before:
pp: 𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a₁ a₂ b₁ b₂ : E
r₁ r₂ : ℝ
a : Eᵐᵒᵖ
b c : E
⊢ dist (a • b) (a • c) = dist b c

Tactic:
by simp

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

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

Tactic:
rw [← dist_mul_right _ _ b, div_mul_cancel]

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

Goal state before:
pp: α : Type u_2
inst✝ : NormedDivisionRing α
a : α
⊢ ↑‖a⁻¹‖₊ = ↑‖a‖₊⁻¹

Tactic:
by simp

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

Goal state before:
pp: α : Type u_2
inst✝ : NontriviallyNormedField α
x : α
ε : ℝ
ε0 : ε > 0
⊢ ∃ b ∈ {x}ᶜ, dist x b < ε

Tactic:
rcases exists_norm_lt α ε0 with ⟨b, hb0, hbε⟩

Goal state after:
α : Type u_2
inst✝ : NontriviallyNormedField α
x : α
ε : ℝ
ε0 : ε > 0
b : α
hb0 : 0 < ‖b‖
hbε : ‖b‖ < ε
⊢ ∃ b ∈ {x}ᶜ, dist x b < ε
Module: Mathlib.Topology.MetricSpace.DilationEquiv

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
Z : Type u_3
inst✝³ : PseudoEMetricSpace X✝
inst✝² : PseudoEMetricSpace Y
inst✝¹ : PseudoEMetricSpace Z
X : Type u_4
inst✝ : PseudoEMetricSpace X
x✝¹ x✝ : X
⊢ edist ((Equiv.refl X).toFun x✝¹) ((Equiv.refl X).toFun x✝) = ↑1 * edist x✝¹ x✝

Tactic:
by simp

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

Goal state before:
pp: case pos
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∀ (x y : X), edist x y = 0 ∨ edist x y = ∞
hY : ∀ (x y : Y), edist x y = 0 ∨ edist x y = ∞
⊢ ratio (e.trans e') = ratio e * ratio e'

Tactic:
simp [Dilation.ratio_of_trivial, *]

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

Goal state before:
pp: x : ℝ≥0
y : ℝ≥0∞
hy : y < ∞
⊢ ↑x < ∞

Tactic:
by simp

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

Goal state before:
pp: x : ℝ≥0
y : ℝ≥0∞
hy : y ≠ ∞
⊢ ↑x ≠ ∞

Tactic:
by simp

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

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
x✝¹ x✝ : PUnit.{?u.6 + 1}
⊢ ‖x✝¹ * x✝‖ ≤ ‖x✝¹‖ * ‖x✝‖

Tactic:
by simp

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

Goal state before:
pp: G : Type u_1
inst✝² : SeminormedAddCommGroup G
inst✝¹ : One G
inst✝ : NormOneClass G
⊢ ‖0‖ ≠ ‖1‖

Tactic:
by simp

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

Goal state before:
pp: α : Type u_2
inst✝ : SeminormedRing α
⊢ ‖↑0‖ ≤ ↑0 * ‖1‖

Tactic:
by simp

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

Goal state before:
pp: α : Type u_2
inst✝ : SeminormedRing α
a : α
x✝ : [a] ≠ []
⊢ ‖[a].prod‖ ≤ (map norm [a]).prod

Tactic:
by simp

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

Goal state before:
pp: α : Type u_2
inst✝¹ : SeminormedRing α
inst✝ : NormOneClass α
⊢ ‖[].prod‖ ≤ (map norm []).prod

Tactic:
by simp

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

Goal state before:
pp: α : Type u_2
inst✝¹ : SeminormedRing α
inst✝ : NormOneClass α
a : α
n : ℕ
⊢ ‖a ^ Nat.zero‖₊ ≤ ‖a‖₊ ^ Nat.zero

Tactic:
by simp

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

Goal state before:
pp: α : Type u_2
inst✝¹ : SeminormedRing α
inst✝ : NormOneClass α
a : α
n : ℕ
⊢ ‖a ^ Nat.zero‖ ≤ ‖a‖ ^ Nat.zero

Tactic:
by simp

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

Goal state before:
pp: α : Type u_2
inst✝ : SeminormedRing α
a b c : α
ha : ‖a‖ ≤ 1
⊢ ‖c - a‖ + 1 * ‖1 - b‖ = ‖c - a‖ + ‖1 - b‖

Tactic:
by simp

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

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
R : Type u_5
inst✝ : Ring R
v : AbsoluteValue R ℝ
x : R
⊢ v (-x + x) = 0

Tactic:
by simp

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

Goal state before:
pp: α : Type u_5
inst✝¹ : Fintype α
ι : α → Type u
inst✝ : ∀ (a : α), Finite (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : IsEmpty ((a : α) → ι a)
a : α
ha : IsEmpty (ι a)
⊢ a ∈ Finset.univ ∧ ⨆ i, f a i = 0

Tactic:
by simp

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
y : β
h1 : dist y x ≤ ε
⊢ dist (s • y) (s • x) ≤ ‖s‖ * ε

Tactic:
simpa [dist_smul₀] using mul_le_mul_of_nonneg_left h1 (norm_nonneg s)

Goal state after:
Module: Mathlib.Data.Prod.TProd

Goal state before:
pp: ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
l : List ι
hnd : l.Nodup
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
⊢ TProd.elim' h ⁻¹' univ.pi t = Set.tprod l t

Tactic:
by
  have h2 : { i | i ∈ l } = univ := by
    ext i
    simp [h]
  rw [← h2, ← mk_preimage_tprod, preimage_preimage]
  simp only [TProd.mk_elim hnd h]
  dsimp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
r₁ r₂ : ℝ
h₀ : 0 ≤ r₁
hr : r₁ < r₂
q : ℚ
h : r₁ < ↑q ∧ ↑q < r₂
⊢ r₁ < ‖q‖ ∧ ‖q‖ < r₂

Tactic:
by rwa [← Rat.norm_cast_real, Real.norm_eq_abs, abs_of_pos (h₀.trans_lt h.1)]

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

Goal state before:
pp: K : Type u_4
val✝ : NontriviallyNormedField K
h : IsComplete (closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : k ∈ upperBounds (Set.range fun n ↦ ‖u n‖)
⊢ ‖u 0‖ ∈ Set.range fun n ↦ ‖u n‖

Tactic:
by simp

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

Goal state before:
pp: K : Type u_4
val✝ : NontriviallyNormedField K
h : IsComplete (closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : k ∈ upperBounds (Set.range fun n ↦ ‖u n‖)
kpos : 0 ≤ k
x : K
hx : k < ‖x‖
hu' : CauchySeq ((fun x_1 ↦ x_1 / x) ∘ u)
n✝ : ℕ
⊢ ‖u n✝‖ ∈ Set.range fun n ↦ ‖u n‖

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
⊢ MeasurableSet univᶜ

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.IterateAct

Goal state before:
pp: α : Type u_1
f : α → α
x✝¹ x✝ : IterateMulAct f
⊢ x✝¹ * x✝ = x✝ * x✝¹

Tactic:
ext; apply Nat.add_comm

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

Goal state before:
pp: α : Type u_1
⊢ ∀ t ∈ ∅, MeasurableSet t

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
⊢ ∀ t ∈ {univ}, MeasurableSet t

Tactic:
by simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
x : E
ε : ℝ
h : 0 < ε
⊢ ‖c • (x - x)‖ = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Real.ENatENNReal

Goal state before:
pp: n : ℕ∞
⊢ ↑n ≠ ∞ ↔ n ≠ ⊤

Tactic:
by simp

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

Goal state before:
pp: β : Type u_2
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSingletonClass β
x : β
⊢ {x} ⊆ measurableAtom x

Tactic:
by simp

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

Goal state before:
pp: G : Type u_6
H : Type u_7
inst✝² : SeminormedAddCommGroup G
inst✝¹ : SeminormedAddCommGroup H
inst✝ : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : s ∈ 𝓝 0
hbounded : Bornology.IsBounded (⇑f '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → ‖f a‖ < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < ↑n
hnpos : 0 < ↑n
hn₀ : n ≠ 0
x : G
hxδ : ‖x‖ < δ / ↑n
⊢ ‖(↑n)⁻¹‖ * C = (↑n)⁻¹ * C

Tactic:
by simp

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
ι : Sort u_3
f : ι → OuterMeasure α
s : Set α
⊢ (⨆ i, f i) s = (⨆ i, ⇑(f i)) s

Tactic:
by simp

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
β : Type u_2
m : OuterMeasure α
a : α
⊢ ∅.indicator (fun x ↦ 1) a = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
β : Type u_2
m : OuterMeasure α
ι : Type ?u.14
f : ι → OuterMeasure α
⊢ ∑' (i : ι), (f i) ∅ = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
m✝ : OuterMeasure α
β : Type ?u.15
f : α → β
m : OuterMeasure β
⊢ m (f '' ∅) = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
m : OuterMeasure α
s : Set α
⊢ ((restrict univ) m) s = m s

Tactic:
by simp

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
m : OuterMeasure α
s : Set α
⊢ ((restrict ∅) m) s = 0 s

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Instances

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsOrderedRing R
inst✝ : Nontrivial R
⊢ 0 ∈ Ico 0 1

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
p q : α → Prop
hp : Measurable p
hq : Measurable q
⊢ MeasurableSet {a | p a ↔ q a}

Tactic:
simp_rw [iff_iff_implies_and_implies]; exact hq.setOf.bihimp hp.setOf

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s : Set α
inst✝¹ : MeasurableSpace β
g : β → Finset α
inst✝ : Countable α
S : Finset α
⊢ MeasurableSet {↑S}

Tactic:
by simp

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

Goal state before:
pp: a : SignType
⊢ 0 < 3

Tactic:
by simp

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

Goal state before:
pp: s : SignType
n : ℕ
hn : Odd n
⊢ s ^ n = s

Tactic:
obtain ⟨k, rfl⟩ := hn

Goal state after:
s : SignType
k : ℕ
⊢ s ^ (2 * k + 1) = s
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: a : SignType
⊢ 1 < 3

Tactic:
by simp

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

Goal state before:
pp: a : SignType
⊢ 2 < 3

Tactic:
by simp

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

Goal state before:
pp: case inr
s : SignType
hs : s ≠ 0
k : ℤ
⊢ (s ^ 2) ^ k * s = s

Tactic:
zpow_two

Goal state after:
case inr
s : SignType
hs : s ≠ 0
k : ℤ
⊢ (s * s) ^ k * s = s
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: ⊢ Finset.univ = {0, -1, 1}

Tactic:
by
  decide

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

Goal state before:
pp: a : Fin 3
isLt✝ : 0 < 3
⊢ (fun a ↦
        match a with
        | zero => ⟨0, fin3Equiv._proof_7⟩
        | pos => ⟨1, fin3Equiv._proof_8⟩
        | neg => ⟨2, fin3Equiv._proof_9⟩)
      ((fun a ↦
          match a with
          | ⟨0, isLt⟩ => 0
          | ⟨1, isLt⟩ => 1
          | ⟨2, isLt⟩ => -1)
        ⟨0, isLt✝⟩) =
    ⟨0, isLt✝⟩

Tactic:
by simp

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

Goal state before:
pp: a : Fin 3
isLt✝ : 1 < 3
⊢ (fun a ↦
        match a with
        | zero => ⟨0, fin3Equiv._proof_7⟩
        | pos => ⟨1, fin3Equiv._proof_8⟩
        | neg => ⟨2, fin3Equiv._proof_9⟩)
      ((fun a ↦
          match a with
          | ⟨0, isLt⟩ => 0
          | ⟨1, isLt⟩ => 1
          | ⟨2, isLt⟩ => -1)
        ⟨1, isLt✝⟩) =
    ⟨1, isLt✝⟩

Tactic:
by simp

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

Goal state before:
pp: a : Fin 3
isLt✝ : 2 < 3
⊢ (fun a ↦
        match a with
        | zero => ⟨0, fin3Equiv._proof_7⟩
        | pos => ⟨1, fin3Equiv._proof_8⟩
        | neg => ⟨2, fin3Equiv._proof_9⟩)
      ((fun a ↦
          match a with
          | ⟨0, isLt⟩ => 0
          | ⟨1, isLt⟩ => 1
          | ⟨2, isLt⟩ => -1)
        ⟨2, isLt✝⟩) =
    ⟨2, isLt✝⟩

Tactic:
by simp

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

Goal state before:
pp: α : Type u
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
t : SignType
h : ∀ i ∈ s, sign (f i) = t
⊢ sign (∑ i ∈ s, f i) = t

Tactic:
cases t

Goal state after:
case zero
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, sign (f i) = zero
⊢ sign (∑ i ∈ s, f i) = zero

case neg
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, sign (f i) = neg
⊢ sign (∑ i ∈ s, f i) = neg

case pos
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, sign (f i) = pos
⊢ sign (∑ i ∈ s, f i) = pos
Module: Mathlib.Data.Nat.Cast.Order.Field

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
⊢ (↑0)⁻¹ ≤ 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Field

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n m : ℕ
h : n ≤ m
⊢ 1 / (↑m + 1) ≤ 1 / (↑n + 1)

Tactic:
refine one_div_le_one_div_of_le ?_ ?_
  · exact Nat.cast_add_one_pos _
  · simpa

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

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

Tactic:
neg_mul,

Goal state after:
case neg_left
x✝ y✝ : EReal
h : (x✝ * y✝).abs = x✝.abs * y✝.abs
⊢ (-(x✝ * y✝)).abs = (-x✝).abs * y✝.abs
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_4
a : α
f : α → ℝ≥0∞
⊢ ⨆ (_ : a = a), f a = f a

Tactic:
by simp

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

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

Tactic:
neg_mul,

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

Goal state before:
pp: ⊢ ↑(sign ⊥) * ↑⊥.abs = ⊥

Tactic:
by simp

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

Goal state before:
pp: ⊢ ↑(sign ⊤) * ↑⊤.abs = ⊤

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
f : α → ℝ≥0∞
s : Set ι
t : ι → Set α
⊢ ⋃ i ∈ s, t i = ⋃ i, t ↑i

Tactic:
by simp

Goal state after: