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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
g : γ → β
hg : Injective g
f : β → α
hf : mulSupport f ⊆ Set.range g
this : mulSupport f = g '' mulSupport (f ∘ g)
hf_fin : ¬(mulSupport f).Finite
hf_fin' : ¬(mulSupport (f ∘ g)).Finite
⊢ (if h : ∃ a, HasProd (f ∘ g) a then if HasProd (f ∘ g) 1 then 1 else Exists.choose ⋯ else 1) =
    if h : ∃ a, HasProd (fun b ↦ f b) a then if HasProd (fun b ↦ f b) 1 then 1 else Exists.choose ⋯ else 1

Tactic:
simp [hg.hasProd_iff (mulSupport_subset_iff'.1 hf)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : CommMonoid α
inst✝⁵ : TopologicalSpace α
L : SummationFilter β
inst✝⁴ : T2Space α
inst✝³ : ContinuousMul α
inst✝² : DecidableEq β
inst✝¹ : L.LeAtTop
inst✝ : L.NeBot
f : β → α
b : β
hf : Multipliable (update f b 1) L
n : β
⊢ f n = (if n = b then f n else 1) * update f b 1 n

Tactic:
split_ifs with h <;> simp [h]

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

Goal state before:
pp: ⊢ comap Real.toNNReal atTop = atTop

Tactic:
refine le_antisymm ?_ tendsto_real_toNNReal_atTop.le_comap

Goal state after:
⊢ comap Real.toNNReal atTop ≤ atTop
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: f : ℕ → ℝ≥0
k : ℕ
a : ℝ≥0
⊢ HasSum (fun n ↦ f (n + k)) a ↔ HasSum f (a + ∑ i ∈ Finset.range k, f i)

Tactic:
rw [← hasSum_coe, hasSum_nat_add_iff (f := fun n => toReal (f n)) k]; norm_cast

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

Goal state before:
pp: β : Type u_2
inst✝² : PseudoMetricSpace β
α : Type u_4
inst✝¹ : MetricSpace α
K : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K f
f_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : Function.Surjective f
x₀ : β
r : ℝ
⊢ IsCompact (closedBall x₀ r)

Tactic:
let K := f ⁻¹' closedBall x₀ r

Goal state after:
β : Type u_2
inst✝² : PseudoMetricSpace β
α : Type u_4
inst✝¹ : MetricSpace α
K✝ : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K✝ f
f_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
⊢ IsCompact (closedBall x₀ r)
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h : α ≃ᵢ β
s : Set β
⊢ Metric.diam (⇑h.symm '' s) = Metric.diam s

Tactic:
diam_image

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h : α ≃ᵢ β
s : Set β
⊢ Metric.diam s = Metric.diam s
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}

pp: case neg
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}
⊢ 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:
case neg
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}
⊢ l ∈ ⋃ i, closure[inst✝¹] {x i}
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
a✝ : α
hfx : f a✝ ≠ ∞
⊢ g a✝ ≠ ∞ → (f a✝).toReal = (g a✝).toReal → f a✝ = g a✝

Tactic:
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✝ ≠ ∞
⊢ (f a✝).toReal = (g a✝).toReal → f a✝ = g a✝
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: ι : Type u_2
κ : Type u_3
G : Type u_6
inst✝ : SeminormedGroup G
f : ι → κ → G
s : Set κ
l : Filter ι
⊢ TendstoUniformlyOn f 1 l s ↔ ∀ ε > 0, ∀ᶠ (i : ι) in l, ∀ x ∈ s, ‖f i x‖ < ε

Tactic:
by
  simp only [tendstoUniformlyOn_iff, Pi.one_apply, dist_one_left]

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

Goal state before:
pp: case inr.refine_1
x : ℝ≥0∞
xt : x ≠ ∞
x0 : 0 < x
⊢ ∀ (i : ℝ≥0∞ × ℝ≥0∞), i.1 < x ∧ x < i.2 → ∃ i', i' ≠ 0 ∧ Icc (x - i') (x + i') ⊆ Ioo i.1 i.2

Tactic:
rintro ⟨a, b⟩ ⟨ha, hb⟩
      rcases exists_between (tsub_pos_of_lt ha) with ⟨ε, ε0, hε⟩
      rcases lt_iff_exists_add_pos_lt.1 hb with ⟨δ, δ0, hδ⟩
      refine ⟨min ε δ, (lt_min ε0 (coe_pos.2 δ0)).ne', Icc_subset_Ioo ?_ ?_⟩
      · exact lt_tsub_comm.2 ((min_le_left _ _).trans_lt hε)
      · grw [min_le_right]
        exact hδ

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

Goal state before:
pp: ι : Type u_2
κ : Type u_3
G : Type u_6
inst✝ : SeminormedGroup G
f : ι → κ → G
s : Set κ
l : Filter ι
⊢ UniformCauchySeqOn f l s ↔ TendstoUniformlyOnFilter (fun n z ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) (𝓟 s)

Tactic:
uniformCauchySeqOn_iff_uniformCauchySeqOnFilter,

Goal state after:
ι : Type u_2
κ : Type u_3
G : Type u_6
inst✝ : SeminormedGroup G
f : ι → κ → G
s : Set κ
l : Filter ι
⊢ UniformCauchySeqOnFilter f l (𝓟 s) ↔ TendstoUniformlyOnFilter (fun n z ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) (𝓟 s)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

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

Tactic:
filter_upwards [h ε hε] with n hn

Goal state after:
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, a - f x ≤ ε
ε : ℝ≥0∞
hε : ε > 0
n : α
hn : a - f n ≤ ε
⊢ f n ∈ Icc (a - ε) (a + ε)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

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

Tactic:
filter_upwards [h ε hε] with n hn

Goal state after:
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)
ε : ℝ≥0∞
hε : ε > 0
n : α
hn : f n ∈ Icc (a - ε) (a + ε)
⊢ a - f n ≤ ε
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: case refine_3
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 ≤ l.length
hMs : IsGreatest s M
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
⊢ d (l ++ [y])[M] y ≤ L.sum

Tactic:
rcases hMl.eq_or_lt with (rfl | hMl)

Goal state after:
case refine_3.inl
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
hMl : l.length ≤ l.length
hMs : IsGreatest s l.length
hM_lt : l.length < L.length
hM_ltx : l.length < (x :: l).length
hM_lty : l.length < (l ++ [y]).length
⊢ d (l ++ [y])[l.length] y ≤ L.sum

case refine_3.inr
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 ≤ l.length
hMs : IsGreatest s M
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
hMl : M < l.length
⊢ d (l ++ [y])[M] y ≤ L.sum
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ι : Type u_4
f : Filter ι
u v : ι → ℝ≥0∞
a : ℝ≥0∞
a_u : a < liminf u f
b : ℝ≥0∞
b_v : b < liminf v f
c : ℝ≥0∞
c_ab : c < a * b
x : ι
a_x : a < u x
b_x : b < v x
⊢ c < (u * v) x

Tactic:
exact c_ab.trans (mul_lt_mul a_x b_x)

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✝³ : SeminormedGroup E
inst✝² : SeminormedGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
x✝ : ∃ K, AntilipschitzWith K ⇑f
K : ℝ≥0
hK : AntilipschitzWith K ⇑f
x : E
⊢ (↑K + 1)⁻¹ * ↑K ≤ 1

Tactic:
by simp [field]

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

Goal state before:
pp: E : Type u_2
inst✝³ : SeminormedGroup E
X : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : DiscreteTopology X
inst✝ : ProperSpace E
e : X → E
he : Topology.IsClosedEmbedding e
⊢ Tendsto (norm ∘ e) Filter.cofinite atTop

Tactic:
← Filter.cocompact_eq_cofinite X

Goal state after:
E : Type u_2
inst✝³ : SeminormedGroup E
X : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : DiscreteTopology X
inst✝ : ProperSpace E
e : X → E
he : Topology.IsClosedEmbedding e
⊢ Tendsto (norm ∘ e) (cocompact X) atTop
Module: Mathlib.Analysis.Normed.Ring.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NonUnitalSeminormedRing α
x : α × α
⊢ Tendsto (fun e ↦ ‖e.1 * e.2 - (fun p ↦ p.1 * p.2) x‖) (𝓝 x) (𝓝 0)

Tactic:
have : ∀ e : α × α,
            ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖ := by
          intro e
          calc
            ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * (e.2 - x.2) + (e.1 - x.1) * x.2‖ := by
              rw [mul_sub, sub_mul, sub_add_sub_cancel]
            _ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖ :=
              norm_add_le_of_le (norm_mul_le _ _) (norm_mul_le _ _)
        refine squeeze_zero (fun e => norm_nonneg _) this ?_
        convert!
          ((continuous_fst.tendsto x).norm.mul
                ((continuous_snd.tendsto x).sub tendsto_const_nhds).norm).add
            (((continuous_fst.tendsto x).sub tendsto_const_nhds).norm.mul tendsto_const_nhds)
        simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
⊢ diam (⇑f '' univ) = ↑(ratio f) * diam univ

Tactic:
diam_image

Goal state after:
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
⊢ ↑(ratio f) * diam univ = ↑(ratio f) * diam univ
Module: Mathlib.Algebra.Order.AddTorsor

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

Tactic:
rw [@lt_iff_le_not_ge] at h₂

Goal state after:
G : Type u_1
P : Type u_2
inst✝³ : LE G
inst✝² : Preorder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a ≤ b
h₂ : c ≤ d ∧ ¬d ≤ c
hbdc : b • d ≤ b • c
h : d ≤ c
⊢ False
Module: Mathlib.Analysis.Normed.MulAction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : NonUnitalSeminormedRing α
x₁ x₂ : αᵐᵒᵖ
y : α
⊢ dist (x₁ • y) (x₂ • y) ≤ dist x₁ x₂ * dist y 0

Tactic:
simpa [mul_sub, dist_eq_norm, mul_comm] using! norm_mul_le y (x₁ - x₂).unop

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
h : dist p (s • x) < ‖s‖ * ε
⊢ dist (s • s⁻¹ • p) (s • x) < ‖s‖ * ε

Tactic:
simpa [smul_smul, hs] using h

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

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

Tactic:
simpa [smul_smul, hs] using h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : s.Countable
h : ∀ b ∈ s, MeasurableSet (f b)
⊢ MeasurableSet (⋃ x, f ↑x)

Tactic:
have := hs.to_subtype

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : s.Countable
h : ∀ b ∈ s, MeasurableSet (f b)
this : Countable ↑s
⊢ MeasurableSet (⋃ x, f ↑x)
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: E : Type u_6
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
y : E
hy : y ≠ 0
⊢ dist (x + r • ‖y‖⁻¹ • y) (x - r • ‖y‖⁻¹ • y) ≤ diam (sphere x r)

Tactic:
by
      apply dist_le_diam_of_mem isBounded_sphere <;> simp [norm_smul, hy, abs_of_nonneg hr]

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
inst✝⁷ : NormedField 𝕜
inst✝⁶ : SeminormedAddCommGroup E✝
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E✝
inst✝³ : NormedSpace 𝕜 F
ι : Type u_6
E : ι → Type u_7
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
a : 𝕜
f : (i : ι) → E i
⊢ ‖a • f‖ ≤ ‖a‖ * ‖f‖

Tactic:
simp_rw [← coe_nnnorm, ← NNReal.coe_mul, NNReal.coe_le_coe, Pi.nnnorm_def,
      NNReal.mul_finset_sup]
    exact Finset.sup_mono_fun fun _ _ => norm_smul_le a _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : MeasurableSpace β
f : β → α
h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})
s : Set α
x✝ : MeasurableSet s
y : α
hy : y ∈ s
⊢ MeasurableSet (f ⁻¹' {y})

Tactic:
by_cases hyf : y ∈ range f

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : MeasurableSpace β
f : β → α
h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})
s : Set α
x✝ : MeasurableSet s
y : α
hy : y ∈ s
hyf : y ∈ range f
⊢ MeasurableSet (f ⁻¹' {y})

case neg
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : MeasurableSpace β
f : β → α
h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})
s : Set α
x✝ : MeasurableSet s
y : α
hy : y ∈ s
hyf : y ∉ range f
⊢ MeasurableSet (f ⁻¹' {y})
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ ((map f) ⊤) s = ((restrict (range f)) ⊤) s

Tactic:
rw [map_apply, restrict_apply, ← image_preimage_eq_inter_range, top_apply', top_apply',
      Set.image_eq_empty]

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : n ≤ m
⊢ dist (f n) (f m) ≤ ∑' (m : ℕ), d (n + m)

Tactic:
refine le_trans (dist_le_Ico_sum_of_dist_le hnm fun _ _ ↦ hf _) ?_

Goal state after:
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : n ≤ m
⊢ ∑ i ∈ Ico n m, d i ≤ ∑' (m : ℕ), d (n + m)
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: f : ℕ → ℝ≥0∞
r : ℝ≥0∞
⊢ HasSum f r ↔ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)

Tactic:
by
  refine ⟨HasSum.tendsto_sum_nat, fun h => ?_⟩
  rw [← iSup_eq_of_tendsto _ h, ← ENNReal.tsum_eq_iSup_nat]
  · exact ENNReal.summable.hasSum
  · exact fun s t hst => Finset.sum_le_sum_of_subset (Finset.range_subset_range.2 hst)

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

Goal state before:
pp: case e'_3
α : Type u_4
f : α → ℝ≥0
hf : ∑' (x : α), (fun i ↦ ↑(f i)) x ≠ ∞
x✝ : Finset α
⊢ ∑' (b : { x // x ∉ x✝ }), (fun i ↦ ↑(f i)) ↑b = ↑(∑' (b : { x // x ∉ x✝ }), f ↑b)

Tactic:
rw [ENNReal.coe_tsum]

Goal state after:
case e'_3
α : Type u_4
f : α → ℝ≥0
hf : ∑' (x : α), (fun i ↦ ↑(f i)) x ≠ ∞
x✝ : Finset α
⊢ Summable fun b ↦ f ↑b
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
r : α → β → Prop
s : Set α
⊢ Semicontinuous (s.domRestrict r) ↔ SemicontinuousOn r s

Tactic:
rw [SemicontinuousOn, Semicontinuous, SetCoe.forall]
  refine forall₂_congr fun a ha ↦ forall₂_congr fun b _ ↦ ?_
  simp only [nhdsWithin_eq_map_subtype_coe ha, eventually_map, domRestrict]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace γ
inst✝ : Preorder β
f g : α → β
x : α
s t : Set α
y z : β
⊢ (Semicontinuous fun x1 x2 ↦ ¬f x1 ≤ x2) ↔ ∀ (x : α) (y : β), (∃ᶠ (x' : α) in 𝓝 x, f x' ≤ y) → f x ≤ y

Tactic:
by
  simp_rw [Semicontinuous, SemicontinuousAt, ← not_frequently, not_imp_not]

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

Goal state before:
pp: ⊢ ↑0⁻¹ = 0

Tactic:
GroupWithZero.inv_zero,

Goal state after:
⊢ ↑0 = 0
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n ↦ ∑ x ∈ Finset.range n, d x
N n : ℕ
hN : dist (∑ x ∈ Finset.range n, d x) (∑ x ∈ Finset.range N, d x) < ↑ε
hn : N ≤ n
⊢ edist (f n) (f N) < ↑ε

Tactic:
rw [dist_nndist, NNReal.nndist_eq, ← Finset.sum_range_add_sum_Ico _ hn, add_tsub_cancel_left,
    NNReal.coe_lt_coe, max_lt_iff] at hN

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n ↦ ∑ x ∈ Finset.range n, d x
N n : ℕ
hN :
  ∑ k ∈ Finset.Ico N n, d k < ε ∧
    ∑ x ∈ Finset.range N, d x - (∑ k ∈ Finset.range N, d k + ∑ k ∈ Finset.Ico N n, d k) < ε
hn : N ≤ n
⊢ edist (f n) (f N) < ↑ε
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : n ≤ m
⊢ ∑ i ∈ Finset.Ico n m, d i ≤ ∑' (m : ℕ), d (n + m)

Tactic:
rw [Finset.sum_Ico_eq_sum_range]

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : n ≤ m
⊢ ∑ k ∈ Finset.range (m - n), d (n + k) ≤ ∑' (m : ℕ), d (n + m)
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝⁶ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_5
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : (g ∘ f) x > y
h : ∀ (l : γ), f x ≤ l
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, (fun x1 x2 ↦ (g ∘ f) x1 > x2) x' y

Tactic:
exact Filter.Eventually.of_forall fun a => hy.trans_le (gmon (h (f a)))

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

Goal state before:
pp: case hl
𝕜 : Type u_4
inst✝⁵ : Semifield 𝕜
inst✝⁴ : CharZero 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ ?f₁ =ᶠ[atTop] fun k ↦ (a + c * ↑k) / (b + d * ↑k)

pp: case h
𝕜 : Type u_4
inst✝⁵ : Semifield 𝕜
inst✝⁴ : CharZero 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ Tendsto ?f₁ atTop (𝓝 (c / d))

pp: case f₁
𝕜 : Type u_4
inst✝⁵ : Semifield 𝕜
inst✝⁴ : CharZero 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ ℕ → 𝕜

Tactic:
case f₁ => exact fun k ↦ (a * (↑k)⁻¹ + c) / (b * (↑k)⁻¹ + d)

Goal state after:
case hl
𝕜 : Type u_4
inst✝⁵ : Semifield 𝕜
inst✝⁴ : CharZero 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ (fun k ↦ (a * (↑k)⁻¹ + c) / (b * (↑k)⁻¹ + d)) =ᶠ[atTop] fun k ↦ (a + c * ↑k) / (b + d * ↑k)

case h
𝕜 : Type u_4
inst✝⁵ : Semifield 𝕜
inst✝⁴ : CharZero 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ Tendsto (fun k ↦ (a * (↑k)⁻¹ + c) / (b * (↑k)⁻¹ + d)) atTop (𝓝 (c / d))
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: a : ℝ
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊤, ↑a)

Tactic:
by
  simp only [ContinuousAt, tendsto_nhds_top_iff_real, top_add_coe]
  refine fun r ↦ ((lt_mem_nhds (coe_lt_top (r - (a - 1)))).prod_nhds
    (lt_mem_nhds <| EReal.coe_lt_coe_iff.2 <| sub_one_lt _)).mono fun _ h ↦ ?_
  simpa only [← coe_add, _root_.sub_add_cancel] using add_lt_add h.1 h.2

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

Goal state before:
pp: case neg
𝕜 : Type u_4
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : Tendsto (abs ∘ fun n ↦ r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : ¬1 = |r|
⊢ False

Tactic:
apply @not_tendsto_nhds_of_tendsto_atTop 𝕜 ℕ _ _ _ _ atTop _ (fun n ↦ |r| ^ n) _ 0 _
      · refine (pow_right_strictMono₀ <| lt_of_le_of_ne (le_of_not_gt hr_le)
          hr).monotone.tendsto_atTop_atTop (fun b ↦ ?_)
        obtain ⟨n, hn⟩ := (pow_unbounded_of_one_lt b (lt_of_le_of_ne (le_of_not_gt hr_le) hr))
        exact ⟨n, le_of_lt hn⟩
      · simpa only [← abs_pow]

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

Goal state before:
pp: n : ℕ
⊢ ∑ i ∈ Finset.range n, (1 / 2) ^ i ≤ 2

Tactic:
have : ∀ i, 0 ≤ (1 / (2 : ℝ)) ^ i := by
    intro i
    apply pow_nonneg
    norm_num

Goal state after:
n : ℕ
this : ∀ (i : ℕ), 0 ≤ (1 / 2) ^ i
⊢ ∑ i ∈ Finset.range n, (1 / 2) ^ i ≤ 2
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case h.refine_1
x : ℝ
p : EReal × EReal
p2_gt_1 : 1 < p.2
p1_gt_x : ↑x < p.1
p1_pos : 0 < p.1
this : p.1 ≤ p.1 * p.2
⊢ ↑x < p.1 * p.2

Tactic:
exact lt_of_lt_of_le p1_gt_x this

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

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
⊢ ⨆ (_ : t.Nonempty), m t = m t

Tactic:
rcases t.eq_empty_or_nonempty with h | h <;> simp [h, Set.not_nonempty_empty, m_empty]

Goal state after: