mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case refine_4
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I J I' J' : FractionalIdeal R⁰ K
H✝ : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
H : Submodule.map ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I = ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I
⊢ ⊤ ≤ Submodule.comap (↑I').subtype (↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I) ⊔ Submodule.comap (↑I').subtype ↑J'

Tactic:
← Submodule.map_le_map_iff_of_injective I'.coeToSubmodule.injective_subtype,

Goal state after:
case refine_4
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I J I' J' : FractionalIdeal R⁰ K
H✝ : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
H : Submodule.map ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I = ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I
⊢ Submodule.map (↑I').subtype ⊤ ≤
    Submodule.map (↑I').subtype
      (Submodule.comap (↑I').subtype (↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I) ⊔ Submodule.comap (↑I').subtype ↑J')
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
x : E
f : Filter E
⊢ Disjoint (𝓝 x) f ↔ ∃ δ > 0, ∀ᶠ (y : E) in f, δ ≤ ‖y⁻¹ * x‖

Tactic:
simp [NormedGroup.nhds_basis_norm_lt x |>.disjoint_iff_left, compl_ofPred, eventually_iff]

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

Goal state before:
pp: ⊢ cocompact ℤ = atBot ⊔ atTop

Tactic:
cocompact_eq_atBot_atTop

Goal state after:
⊢ atBot ⊔ atTop = atBot ⊔ atTop
Module: Mathlib.Topology.Algebra.Order.Archimedean

Goal state before:
pp: case inr
G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
S : Subgroup G
hS : ∀ ε > 1, ∃ g ∈ S, g ∈ Ioo 1 ε
h✝ : Nontrivial G
a b : G
hlt : a < b
g : G
hgS : g ∈ S
hg0 : 1 < g
hg : g < b / a
⊢ ∃ c ∈ ↑S, c ∈ Ioo a b

Tactic:
rcases (existsUnique_add_zpow_mem_Ioc hg0 1 a).exists with ⟨m, hm⟩

Goal state after:
case inr
G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
S : Subgroup G
hS : ∀ ε > 1, ∃ g ∈ S, g ∈ Ioo 1 ε
h✝ : Nontrivial G
a b : G
hlt : a < b
g : G
hgS : g ∈ S
hg0 : 1 < g
hg : g < b / a
m : ℤ
hm : 1 * g ^ m ∈ Ioc a (a * g)
⊢ ∃ c ∈ ↑S, c ∈ Ioo a b
Module: Mathlib.GroupTheory.Archimedean

Goal state before:
pp: case ha
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
hex : ∀ g > 1, ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ n, (↑H ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬(↑H ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ ↑H
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
hxmin : ∀ (x : G), x ∈ H ∧ 1 < x → ∃ x_1, ∃ (_ : x_1 ∈ H ∧ 1 < x_1), x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 1 < y
m : ℕ
hm : a ^ m < y
hya : y ≤ a ^ (m + 1)
hnm : n ≤ m
⊢ 1 ≤ a

Tactic:
exact h₀.le

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝⁴ : Preorder α
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
f : Filter ι
u v : ι → α
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∀ᶠ (x : ι) in f, v x ≤ V
⊢ ∀ᶠ (x : ι) in f, (u * v) x ≤ U * V

Tactic:
filter_upwards [hU, hV, h₃] with x x_U x_V v_0

Goal state after:
α : Type u_1
ι : Type u_4
inst✝⁴ : Preorder α
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
f : Filter ι
u v : ι → α
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∀ᶠ (x : ι) in f, v x ≤ V
x : ι
x_U : u x ≤ U
x_V : v x ≤ V
v_0 : 0 x ≤ v x
⊢ (u * v) x ≤ U * V
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : LE α
inst✝ : LE β
e : α ≃o β
l : Filter γ
u : γ → α
a : α
⊢ (∀ᶠ (x : β) in map (fun x ↦ e (u x)) l, (fun x1 x2 ↦ x1 ≤ x2) x (e a)) ↔
    ∀ᶠ (x : α) in map u l, (fun x1 x2 ↦ x1 ≤ x2) x a

Tactic:
by simp only [eventually_map, e.le_iff_le]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
⊢ blimsup u f p = limsup u (f ⊓ 𝓟 {x | p x})

Tactic:
simp only [blimsup_eq, limsup_eq, eventually_inf_principal, mem_ofPred_eq]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
s : Set α
⊢ ediam (f '' s) ≤ ↑K * ediam s

Tactic:
apply Metric.ediam_le

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
s : Set α
⊢ ∀ x ∈ f '' s, ∀ y ∈ f '' s, edist x y ≤ ↑K * ediam s
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case inl
x : ℝ≥0
⊢ ↑↑x = ↑↑(↑x).toNNReal - ↑↑0

Tactic:
Real.toNNReal_coe,

Goal state after:
case inl
x : ℝ≥0
⊢ ↑↑x = ↑↑x - ↑↑0
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x : EReal
h : 0 < x
⊢ ⊤ * x = ⊤

Tactic:
by
  rw [EReal.mul_comm]
  exact mul_top_of_pos h

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

Goal state before:
pp: x y : EReal
⊢ -y * x = -(y * x)

Tactic:
exact y.neg_mul x

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

Goal state before:
pp: a b c : EReal
ha : 0 ≤ a
hb : 0 ≤ b
⊢ (a + b) * c = a * c + b * c

Tactic:
lift a to ℝ≥0∞ using ha

Goal state after:
b c : EReal
hb : 0 ≤ b
a : ℝ≥0∞
⊢ (↑a + b) * c = ↑a * c + b * c
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 α
⊢ e ∈ 𝓝 1 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e

Tactic:
he

Goal state after:
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, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁵ : CommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedMonoid α
inst✝² : CanonicallyOrderedMul α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
hf : Multipliable f
⊢ ¬∏' (i : ι), f i = 1 ↔ ∃ x, f x ≠ 1

Tactic:
hf.tprod_eq_one_iff,

Goal state after:
ι : Type u_1
α : Type u_3
inst✝⁵ : CommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedMonoid α
inst✝² : CanonicallyOrderedMul α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
hf : Multipliable f
⊢ (¬∀ (x : ι), f x = 1) ↔ ∃ x, f x ≠ 1
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: case pos
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
H : Multipliable f
e : Set G
⊢ e ∈ 𝓝 1 → e ∈ Filter.map (fun s ↦ ∏' (a : { x // x ∉ s }), f ↑a) atTop

Tactic:
he

Goal state after:
case pos
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
H : Multipliable f
e : Set G
he : e ∈ 𝓝 1
⊢ e ∈ Filter.map (fun s ↦ ∏' (a : { x // x ∉ s }), f ↑a) atTop
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
⊢ e ∈ 𝓝 1 → e ∈ Filter.map f cofinite

Tactic:
he

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
⊢ e ∈ Filter.map f cofinite
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
h : Summable fun x ↦ f x.1 * g x.2
⊢ Summable fun n ↦ ∑ k ∈ range (n + 1), f k * g (n - k)

Tactic:
simp_rw [← Nat.sum_antidiagonal_eq_sum_range_succ fun k l ↦ f k * g l]

Goal state after:
α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
h : Summable fun x ↦ f x.1 * g x.2
⊢ Summable fun n ↦ ∑ ij ∈ antidiagonal n, f ij.1 * g ij.2
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x ↦ f x.1 * g x.2
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ k ∈ range (n + 1), f k * g (n - k)

Tactic:
simp_rw [← Nat.sum_antidiagonal_eq_sum_range_succ fun k l ↦ f k * g l]

Goal state after:
α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x ↦ f x.1 * g x.2
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ ij ∈ antidiagonal n, f ij.1 * g ij.2
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁵ : CommSemiring α
inst✝⁴ : TopologicalSpace α
f : ι → α
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderBot ι
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
hsum : Summable fun i ↦ f i * ∏ j < i, (1 + f j)
hprod : Multipliable fun x ↦ 1 + f x
⊢ ∏' (i : ι), (1 + f i) = 1 + ∑' (i : ι), f i * ∏ j < i, (1 + f j)

Tactic:
rcases isEmpty_or_nonempty ι with _ | _

Goal state after:
case inl
ι : Type u_1
α : Type u_3
inst✝⁵ : CommSemiring α
inst✝⁴ : TopologicalSpace α
f : ι → α
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderBot ι
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
hsum : Summable fun i ↦ f i * ∏ j < i, (1 + f j)
hprod : Multipliable fun x ↦ 1 + f x
h✝ : IsEmpty ι
⊢ ∏' (i : ι), (1 + f i) = 1 + ∑' (i : ι), f i * ∏ j < i, (1 + f j)

case inr
ι : Type u_1
α : Type u_3
inst✝⁵ : CommSemiring α
inst✝⁴ : TopologicalSpace α
f : ι → α
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderBot ι
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
hsum : Summable fun i ↦ f i * ∏ j < i, (1 + f j)
hprod : Multipliable fun x ↦ 1 + f x
h✝ : Nonempty ι
⊢ ∏' (i : ι), (1 + f i) = 1 + ∑' (i : ι), f i * ∏ j < i, (1 + f j)
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₄))
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
⊢ M < L.length

Tactic:
hL_len,

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₄))
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
⊢ M < l.length + 1
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: E : Type u_4
inst✝ : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑s
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
⊢ {x | dist x a < b 0} ∈ 𝓝 a

Tactic:
exact Metric.ball_mem_nhds _ (b_pos _)

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

Goal state before:
pp: E : Type u_4
inst✝ : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑s
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun n ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
⊢ ∃ v,
    Tendsto (fun n ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧
      (∀ (n : ℕ), v n ∈ s) ∧ ‖(v 0)⁻¹ * a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n

Tactic:
have hw : Tendsto w atTop (𝓝 a) := lim_z.comp φ_extr.tendsto_atTop

Goal state after:
E : Type u_4
inst✝ : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑s
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun n ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
⊢ ∃ v,
    Tendsto (fun n ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧
      (∀ (n : ℕ), v n ∈ s) ∧ ‖(v 0)⁻¹ * a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝² : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
hf : ¬UniformContinuous f
a b : pkg.space
⊢ f (⋯.some a) = f (⋯.some b)

Tactic:
by congr 1

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

Goal state before:
pp: E : Type u_7
inst✝ : NormedCommGroup E
a : E
⊢ Tendsto (fun x ↦ ‖x⁻¹ * a‖) (𝓝[≠] a) (𝓝[>] 0)

Tactic:
exact tendsto_norm_inv_mul_self_nhdsNE a

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PseudoEMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
s : β → α
⊢ (∀ ε > 0, ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε) ↔
    ∃ b, (∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N) ∧ Tendsto b atTop (𝓝 0)

Tactic:
by
  constructor
  · intro hs
    /- `s` is Cauchy sequence. Let `b n` be the diameter of the set `s '' Set.Ici n`. -/
    refine ⟨fun N => Metric.ediam (s '' Ici N), fun n m N hn hm => ?_, ?_⟩
    -- Prove that it bounds the distances of points in the Cauchy sequence
    · exact Metric.edist_le_ediam_of_mem (mem_image_of_mem _ hn) (mem_image_of_mem _ hm)
    -- Prove that it tends to `0`, by using the Cauchy property of `s`
    · refine ENNReal.tendsto_nhds_zero.2 fun ε ε0 => ?_
      rcases hs ε ε0 with ⟨N, hN⟩
      refine (eventually_ge_atTop N).mono fun n hn => Metric.ediam_le ?_
      rintro _ ⟨k, hk, rfl⟩ _ ⟨l, hl, rfl⟩
      exact (hN _ (hn.trans hk) _ (hn.trans hl)).le
  · rintro ⟨b, ⟨b_bound, b_lim⟩⟩ ε εpos
    have : ∀ᶠ n in atTop, b n < ε := b_lim.eventually (gt_mem_nhds εpos)
    rcases this.exists with ⟨N, hN⟩
    refine ⟨N, fun m hm n hn => ?_⟩
    calc edist (s m) (s n) ≤ b N := b_bound m n N hm hn
    _ < ε := hN

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

Goal state before:
pp: F : Type u_3
inst✝¹ : SeminormedCommGroup F
E : Type u_5
inst✝ : SeminormedCommGroup E
K : ℝ≥0
f : E → F
hf : AntilipschitzWith K f
x y : E
⊢ ‖x⁻¹ * y‖ ≤ ↑K * ‖(f x)⁻¹ * f y‖

Tactic:
simp [← dist_eq_norm_inv_mul, hf.le_mul_dist x y]

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
x : α
r' : ℝ
y : α
hy : y ∈ ball x r'
⊢ ↑(ratio f) * dist y x < ↑(ratio f) * r'

Tactic:
by gcongr; exacts [ratio_pos _, hy]

Goal state after:
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
⊢ False

Tactic:
have h : d ≤ c := IsOrderedCancelSMul.le_of_smul_le_smul_left b d c hbdc

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
hbdc : b • d ≤ b • c
h : d ≤ c
⊢ False
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: ι : Type u_4
α : Type u_5
inst✝ : NormedCommRing α
s : Finset ι
hs : s.Nonempty
f : ι → α
⊢ ∏ i ∈ s, ‖f i‖ = ↑(∏ i ∈ s, ‖f i‖₊)

Tactic:
simp [NNReal.coe_prod]

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

Goal state before:
pp: ι : Type u_4
α : Type u_5
inst✝¹ : NormedCommRing α
inst✝ : NormOneClass α
s : Finset ι
f : ι → α
⊢ ∏ i ∈ s, ‖f i‖ = ↑(∏ i ∈ s, ‖f i‖₊)

Tactic:
simp [NNReal.coe_prod]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
g : β → α
hg : Function.Surjective g
S : Set α
hS : MeasurableSet (g ⁻¹' S)
⊢ MeasurableSet S

Tactic:
measurableSet_comap

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
g : β → α
hg : Function.Surjective g
S : Set α
hS : ∃ s', MeasurableSet s' ∧ g ⁻¹' s' = g ⁻¹' S
⊢ MeasurableSet S
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 (⋃ b ∈ s, f b)

Tactic:
biUnion_eq_iUnion

Goal state after:
α : 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)
Module: Mathlib.MeasureTheory.OuterMeasure.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_2
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
I : Set ι
μ : F
hI : I.Countable
s : ι → Set α
this : Countable ↑I
⊢ μ (⋃ i ∈ I, s i) ≤ ∑' (i : ↑I), μ (s ↑i)

Tactic:
biUnion_eq_iUnion

Goal state after:
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
I : Set ι
μ : F
hI : I.Countable
s : ι → Set α
this : Countable ↑I
⊢ μ (⋃ x, s ↑x) ≤ ∑' (i : ↑I), μ (s ↑i)
Module: Mathlib.MeasureTheory.OuterMeasure.Basic

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s : Set α
hs : s.Countable
⊢ μ s = 0 ↔ ∀ x ∈ s, μ {x} = 0

Tactic:
rw [← measure_biUnion_null_iff hs, biUnion_of_singleton]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
h : (s ×ˢ t).Nonempty
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t

Tactic:
rcases h with ⟨⟨x, y⟩, hx, hy⟩

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
x : α
y : β
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ t
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: a b : SignType
⊢ (match a * b with
    | zero => ⟨0, fin3Equiv._proof_7⟩
    | pos => ⟨1, fin3Equiv._proof_8⟩
    | neg => ⟨2, fin3Equiv._proof_9⟩) =
    (match a with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩) *
      match b with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩

Tactic:
cases a <;> cases b <;> rfl

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

Goal state before:
pp: α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
h : sign a = 1
⊢ 0 < a

Tactic:
by_contra hn

Goal state after:
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
h : sign a = 1
hn : ¬0 < a
⊢ False
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ sign (⊤ * ↑x✝) = sign ⊤ * sign ↑x✝

Tactic:
rw [top_mul_coe_of_pos h, sign_top, one_mul, sign_pos (EReal.coe_pos.2 h)]

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

Goal state before:
pp: f : ℕ → ℝ≥0∞
hf : ∑' (x : ℕ), f x ≠ ∞
⊢ Tendsto f cofinite (𝓝 0)

Tactic:
exact tendsto_cofinite_zero_of_tsum_ne_top hf

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x : α
s : Set α
⊢ LowerHemicontinuousWithinAt f s x ↔ ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ t) → f x ⊆ t

Tactic:
lowerHemicontinuousWithinAt_iff,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x : α
s : Set α
⊢ (∀ (u : Set β), IsOpen[inst✝] u → (f x ∩ u).Nonempty → ∀ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ u).Nonempty) ↔
    ∀ (t : Set β), IsClosed[inst✝] t → (∃ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ t) → f x ⊆ t
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
f g : α → ℝ≥0
sf sg : ℝ≥0
i : α
h : ∀ (a : α), f a ≤ g a
hi : f i < g i
hf : HasSum f sf
hg : HasSum g sg
A : ∀ (a : α), ↑(f a) ≤ ↑(g a)
⊢ sf < sg

Tactic:
have : (sf : ℝ) < sg := hasSum_lt A (NNReal.coe_lt_coe.2 hi) (hasSum_coe.2 hf) (hasSum_coe.2 hg)

Goal state after:
α : Type u_1
f g : α → ℝ≥0
sf sg : ℝ≥0
i : α
h : ∀ (a : α), f a ≤ g a
hi : f i < g i
hf : HasSum f sf
hg : HasSum g sg
A : ∀ (a : α), ↑(f a) ≤ ↑(g a)
this : ↑sf < ↑sg
⊢ sf < sg
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: f : ℕ → ℝ≥0
hf : ∑' (i : ℕ), (fun i ↦ ↑(f i)) i ≠ ∞
⊢ Tendsto (fun i ↦ ∑' (k : ℕ), (fun i ↦ ↑(f i)) (k + i)) atTop (𝓝 0)

Tactic:
replace hf : Summable f := tsum_coe_ne_top_iff_summable.1 hf

Goal state after:
f : ℕ → ℝ≥0
hf : Summable f
⊢ Tendsto (fun i ↦ ∑' (k : ℕ), (fun i ↦ ↑(f i)) (k + i)) atTop (𝓝 0)
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: x : EReal
h_top : x = ⊤
n : ℕ
y : EReal
hy : ↑↑n < y
⊢ ↑n < y.toENNReal

Tactic:
exact toENNReal_coe (x := n) ▸ toENNReal_lt_toENNReal (coe_ennreal_nonneg _) hy

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

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁴ : DivisionSemiring 𝕜
inst✝³ : CharZero 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : ContinuousSMul ℚ≥0 𝕜
inst✝ : ContinuousMul 𝕜
C : 𝕜
⊢ Tendsto (fun n ↦ C / ↑n) atTop (𝓝 0)

Tactic:
by
  simpa only [mul_zero, div_eq_mul_inv] using
    (tendsto_const_nhds (x := C)).mul tendsto_inv_atTop_nhds_zero_nat

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

Goal state before:
pp: case inr
r : ℝ≥0∞
hr : 1 ≤ r
⊢ ∑' (n : ℕ), r ^ n = ∞

Tactic:
ENNReal.tsum_eq_iSup_nat,

Goal state after:
case inr
r : ℝ≥0∞
hr : 1 ≤ r
⊢ ⨆ i, ∑ a ∈ Finset.range i, r ^ a = ∞
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

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

Tactic:
simp [h, Set.not_nonempty_empty, m_empty]

Goal state after: