mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b c : ℝ≥0∞
hc✝ : c < a * b
a' : ℝ≥0∞
hc : c / b < a'
ha' : a' < a
⊢ ∃ a' < a, c < a' * b

Tactic:
exact ⟨_, ha', (ENNReal.div_lt_iff (.inl <| by rintro rfl; simp at *)
    (.inr <| by rintro rfl; simp at *)).1 hc⟩

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
s : Set α
inst✝ : PseudoEMetricSpace β
f : α → β
a : α
b : β
⊢ Tendsto f (𝓝[s] a) (𝓝 b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ {x : α}, x ∈ s → edist x a < δ → edist (f x) b < ε

Tactic:
rw [← nhdsWithin_univ b, tendsto_nhdsWithin_nhdsWithin]

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
s : Set α
inst✝ : PseudoEMetricSpace β
f : α → β
a : α
b : β
⊢ (∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → edist x a < δ → f x ∈ univ ∧ edist (f x) b < ε) ↔
    ∀ ε > 0, ∃ δ > 0, ∀ {x : α}, x ∈ s → edist x a < δ → edist (f x) b < ε
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x : ℝ≥0∞
hx : 1 ≤ x
m : ℤ
hn : -m ≤ 0
⊢ 0 ≤ m

Tactic:
by simpa using hn

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

Goal state before:
pp: α✝ : Type u
β✝ : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α✝
γ : Type w
inst✝ : EMetricSpace γ
α : Type u_2
β : Type u_3
e : TopologicalSpace α
n : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
m : WeakPseudoEMetricSpace β
hα : PseudoEMetricSpace α := PseudoEMetricSpace.ofEDist (fun x y ↦ edist (f x) (f y)) ⋯ ⋯ ⋯
hβ : PseudoEMetricSpace β := PseudoEMetricSpace.ofEDist edist ⋯ ⋯ ⋯
⊢ (uniformSpaceOfEDist (fun x y ↦ edist (f x) (f y)) ⋯ ⋯ ⋯).toTopologicalSpace ≤ e

Tactic:
rw [(isInducing_iff f).mp hf]

Goal state after:
α✝ : Type u
β✝ : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α✝
γ : Type w
inst✝ : EMetricSpace γ
α : Type u_2
β : Type u_3
e : TopologicalSpace α
n : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
m : WeakPseudoEMetricSpace β
hα : PseudoEMetricSpace α := PseudoEMetricSpace.ofEDist (fun x y ↦ edist (f x) (f y)) ⋯ ⋯ ⋯
hβ : PseudoEMetricSpace β := PseudoEMetricSpace.ofEDist edist ⋯ ⋯ ⋯
⊢ (uniformSpaceOfEDist (fun x y ↦ edist (f x) (f y)) ⋯ ⋯ ⋯).toTopologicalSpace ≤ TopologicalSpace.induced f n
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α✝ : Type u
β✝ : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α✝
γ : Type w
inst✝ : EMetricSpace γ
α : Type u_2
β : Type u_3
e : TopologicalSpace α
n : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
m : WeakPseudoEMetricSpace β
x : α
r : ℝ≥0∞
u : Set β
hu : IsOpen[n] u
uy : Subtype.val ⁻¹' u = Metric.eball (f x) ∞ ↓∩ Metric.eball (f x) r
⊢ IsOpen[instTopologicalSpaceSubtype] (Metric.eball x ∞ ↓∩ Metric.eball x r)

Tactic:
rw [(isInducing_iff f).mp hf]

Goal state after:
α✝ : Type u
β✝ : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α✝
γ : Type w
inst✝ : EMetricSpace γ
α : Type u_2
β : Type u_3
e : TopologicalSpace α
n : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
m : WeakPseudoEMetricSpace β
x : α
r : ℝ≥0∞
u : Set β
hu : IsOpen[n] u
uy : Subtype.val ⁻¹' u = Metric.eball (f x) ∞ ↓∩ Metric.eball (f x) r
⊢ IsOpen[instTopologicalSpaceSubtype] (Metric.eball x ∞ ↓∩ Metric.eball x r)
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
g : κ → ℝ≥0∞
hf : ∃ i, f i ≠ ∞
hg : ∃ j, g j ≠ ∞
ha : ∀ (i : ι) (j : κ), a ≤ f i * g j
⊢ a ≤ (⨅ i, f i) * ⨅ j, g j

Tactic:
by
  rw [← iInf_ne_top_subtype]
  have := nonempty_subtype.2 hf
  have := hg.nonempty
  replace hg : ⨅ j, g j ≠ ∞ := by simpa using hg
  rw [iInf_mul fun h ↦ (hg h).elim, le_iInf_iff]
  rintro ⟨i, hi⟩
  simpa [mul_iInf fun h ↦ (hi h).elim] using ha i

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x₁ y₁ x₂ y₂ : α
⊢ dist x₁ y₁ ≤ dist x₁ x₂ + dist y₁ y₂ + dist x₂ y₂

Tactic:
rw [add_right_comm, dist_comm y₁]
  apply dist_triangle4

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

Goal state before:
pp: a : ℝ≥0∞
⊢ a⁻¹.toNNReal = a.toNNReal⁻¹

Tactic:
cases a with
  | top => simp
  | coe a =>
    rcases eq_or_ne a 0 with (rfl | ha); · simp
    rw [← coe_inv ha, toNNReal_coe, toNNReal_coe]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε : ℝ
h : y ∈ ball x ε
⊢ dist y x ≤ ε - (ε - dist y x)

Tactic:
rw [sub_sub_self]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : PseudoMetricSpace β
f : α → β
a : α
b : β
⊢ Tendsto f (𝓝[s] a) (𝓝 b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → dist (f x) b < ε

Tactic:
rw [← nhdsWithin_univ b, tendsto_nhdsWithin_nhdsWithin]

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : PseudoMetricSpace β
f : α → β
a : α
b : β
⊢ (∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → f x ∈ univ ∧ dist (f x) b < ε) ↔
    ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → dist (f x) b < ε
Module: Mathlib.Topology.Metrizable.Basic

Goal state before:
pp: ι : Type u_1
X✝ : Type u_2
Y : Type u_3
A : ι → Type u_4
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : Finite ι
inst✝³ : (i : ι) → TopologicalSpace (A i)
X : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : LindelofSpace X
inst✝ : PseudoMetrizableSpace X
this✝ : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
V : ℕ → SetRel X X
hVb : (𝓤 X).HasAntitoneBasis V
hVs : ∀ (n : ℕ), (V n).IsSymm
U : ℕ → Set X
hUc : ∀ (n : ℕ), (U n).Countable
hUu : ∀ (n : ℕ), ⋃ x ∈ U n, ball x (V n) = univ
x : X
⊢ ∃ᶠ (x : X) in 𝓝 x, x ∈ iUnion U

Tactic:
nhds_eq_comap_uniformity,

Goal state after:
ι : Type u_1
X✝ : Type u_2
Y : Type u_3
A : ι → Type u_4
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : Finite ι
inst✝³ : (i : ι) → TopologicalSpace (A i)
X : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : LindelofSpace X
inst✝ : PseudoMetrizableSpace X
this✝ : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
V : ℕ → SetRel X X
hVb : (𝓤 X).HasAntitoneBasis V
hVs : ∀ (n : ℕ), (V n).IsSymm
U : ℕ → Set X
hUc : ∀ (n : ℕ), (U n).Countable
hUu : ∀ (n : ℕ), ⋃ x ∈ U n, ball x (V n) = univ
x : X
⊢ ∃ᶠ (x : X) in Filter.comap (Prod.mk x) (𝓤 X), x ∈ iUnion U
Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions

Goal state before:
pp: case pos
c : ℝ
c_pos : 0 < c
⊢ ball 0 c = Ico 0 c.toNNReal

pp: case neg
c : ℝ
c_pos : c ≤ 0
⊢ ball 0 c = Ico 0 c.toNNReal

Tactic:
· convert! NNReal.ball_zero_eq_Ico' (NNReal.mk c c_pos.le)
    simp [Real.toNNReal, c_pos.le]

Goal state after:
case neg
c : ℝ
c_pos : c ≤ 0
⊢ ball 0 c = Ico 0 c.toNNReal
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : a < b
⊢ frontier (Ioo a b) = {a, b}

Tactic:
frontier,

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : a < b
⊢ closure[inst✝³] (Ioo a b) \ interior (Ioo a b) = {a, b}
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a b : α
h : a < b
⊢ frontier (Ico a b) = {a, b}

Tactic:
frontier,

Goal state after:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a b : α
h : a < b
⊢ closure[inst✝⁴] (Ico a b) \ interior (Ico a b) = {a, b}
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMaxOrder α
a b : α
h : a < b
⊢ frontier (Ioc a b) = {a, b}

Tactic:
frontier,

Goal state after:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMaxOrder α
a b : α
h : a < b
⊢ closure[inst✝⁴] (Ioc a b) \ interior (Ioc a b) = {a, b}
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
a b : α
s✝ : Set α
x : α
inst✝ : Nontrivial α
s : Set α
hs : s ∈ 𝓝[≠] x
⊢ s.Nonempty

Tactic:
obtain ⟨u, u_open, xu, us⟩ : ∃ u : Set α, IsOpen u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ s := mem_nhdsWithin.1 hs

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
a b : α
s✝ : Set α
x : α
inst✝ : Nontrivial α
s : Set α
hs : s ∈ 𝓝[≠] x
u : Set α
u_open : IsOpen[inst✝⁴] u
xu : x ∈ u
us : u ∩ {x}ᶜ ⊆ s
⊢ s.Nonempty
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
s : Set α
x : α
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : Tendsto f (𝓝[s] x) (𝓝 (f x))
this✝ : (𝓝[s] x).NeBot
b : α
hb : b ∈ s
hxb✝ : x ≤ b
hxb : x < b
this : s ∩ Iio b ∈ 𝓝[s] x
y : α
hy : y ∈ s ∩ Iio b
⊢ f y ≤ f b

Tactic:
exact hf hy.1 hb (le_of_lt hy.2)

Goal state after:
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: case refine_2
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : CompactIccSpace α
s : Set α
hs : s ∈ atBot ⊔ atTop
h✝ : Nonempty α
t : α
ht : ∀ b ≤ t, b ∈ s
u : α
hu : ∀ (b : α), u ≤ b → b ∈ s
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ s

Tactic:
refine ⟨Icc t u, isCompact_Icc, fun x hx ↦ ?_⟩

Goal state after:
case refine_2
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : CompactIccSpace α
s : Set α
hs : s ∈ atBot ⊔ atTop
h✝ : Nonempty α
t : α
ht : ∀ b ≤ t, b ∈ s
u : α
hu : ∀ (b : α), u ≤ b → b ∈ s
x : α
hx : x ∈ (Icc t u)ᶜ
⊢ x ∈ s
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
y : E
ε : ℝ
a : E
⊢ a ∈ ball y ε ↔ a ∈ {x | ‖x⁻¹ * y‖ < ε}

Tactic:
simp [dist_eq_norm_inv_mul]

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a b : E
r : ℝ
⊢ b ∈ sphere a r ↔ ‖b⁻¹ * a‖ = r

Tactic:
simp [dist_eq_norm_inv_mul]

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
x✝¹ : ℝ
x✝ : E × E
⊢ ‖x✝.1⁻¹ * x✝.2‖ = dist x✝.1 x✝.2

Tactic:
simp [dist_eq_norm_inv_mul]

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a : E
r : ℝ
⊢ {x | x / a ∈ closedBall 1 r} = closedBall a r

Tactic:
ext x
  rw [mem_closedBall_iff_norm'']
  simp

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
x : E
⊢ (𝓝 x).HasBasis (fun ε ↦ 0 < ε) fun ε ↦ {y | ‖y / x‖ < ε}

Tactic:
simpa [norm_inv_mul] using NormedGroup.nhds_basis_norm_lt x

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

Goal state before:
pp: x : ℤ
r : ℝ
⊢ closedBall x r = Icc ⌈↑x - r⌉ ⌊↑x + r⌋

Tactic:
rw [← preimage_closedBall, Real.closedBall_eq_Icc, preimage_Icc]

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

Goal state before:
pp: α : Type u
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
⊢ ediam univ = ∞ ↔ ¬Bornology.IsBounded univ

Tactic:
isBounded_iff_ediam_ne_top,

Goal state after:
α : Type u
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
⊢ ediam univ = ∞ ↔ ¬ediam univ ≠ ∞
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
inst✝² : PseudoMetricSpace α
inst✝¹ : ProperSpace α
inst✝ : NoncompactSpace α
⊢ diam univ = 0

Tactic:
by
  simp [diam]

Goal state after:
Module: Mathlib.GroupTheory.Archimedean

Goal state before:
pp: 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)
g : G
hg : g > 1
⊢ ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))

Tactic:
by
    rcases existsUnique_mul_zpow_mem_Ico h₀ 1 (g / a) with ⟨m, ⟨hm, hm'⟩, -⟩
    simp only [one_mul, div_le_iff_le_mul, div_mul_cancel, ← zpow_add_one] at hm hm'
    lift m to ℕ
    · rw [← Int.lt_add_one_iff, ← zpow_lt_zpow_iff_right h₀, zpow_zero]
      exact hg.trans_le hm
    · simp only [← Nat.cast_succ, zpow_natCast] at hm hm'
      exact ⟨m, hm', hm⟩

Goal state after:
Module: Mathlib.GroupTheory.Archimedean

Goal state before:
pp: case inr
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
⊢ False

Tactic:
refine disjoint_left.1 hd (div_mem hxH hyH) ⟨one_lt_div'.2 hxy, div_lt_iff_lt_mul'.2 ?_⟩
    calc x ≤ a ^ (n + 1) := hxn
    _ ≤ a ^ (m + 1) := by grw [hnm]; exact h₀.le
    _ = a ^ m * a := pow_succ _ _
    _ < y * a := by gcongr

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

Goal state before:
pp: case inl
x : ℕ
r : ℝ
hr : 0 ≤ r
⊢ closedBall x r = Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊

Tactic:
rw [← preimage_closedBall, Real.closedBall_eq_Icc, preimage_Icc]

Goal state after:
case inl
x : ℕ
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ ↑x + r
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:
simp only [eventually_map, e.le_iff_le]

Goal state after:
Module: Mathlib.Topology.Order.MonotoneConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SupConvergenceClass α
inst✝ : SupConvergenceClass β
a : α
b : β
s : Set (α × β)
h : IsLUB (range (s.domRestrict fst)) (a, b).1 ∧ IsLUB (range (s.domRestrict snd)) (a, b).2
A : Tendsto (fun x ↦ (↑x).1) atTop (𝓝 a)
B : Tendsto (fun x ↦ (↑x).2) atTop (𝓝 b)
⊢ Tendsto Subtype.val atTop (𝓝 (a, b))

Tactic:
exact A.prodMk_nhds B

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

Goal state before:
pp: x y : EReal
hy : y ≠ ⊥
hy' : y ≠ ⊤
⊢ x + y ≠ ⊤ ↔ x ≠ ⊤

Tactic:
cases x <;> simp [add_ne_top_iff_ne_top₂, hy, hy']

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
u : β → α
⊢ ⨅ i ∈ f, sSup (u '' id i) = ⨅ s ∈ f, ⨆ a ∈ s, u a

Tactic:
by simp only [sSup_image, id]

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:
by
  apply Metric.ediam_le
  rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩
  exact hf.edist_le_mul_of_le (Metric.edist_le_ediam_of_mem hx hy)

Goal state after:
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: case neg
α : Type u_2
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
f : Filter α
inst✝ : f.NeBot
hc : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f
hb : IsBounded (fun x1 x2 ↦ x1 ≤ x2) f
hn : Nontrivial α
htop : ∃ x, f.limsSup < x
⊢ ClusterPt f.limsSup f

Tactic:
by_cases! hbot : ∀ x, f.limsSup ≤ x

Goal state after:
case pos
α : Type u_2
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
f : Filter α
inst✝ : f.NeBot
hc : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f
hb : IsBounded (fun x1 x2 ↦ x1 ≤ x2) f
hn : Nontrivial α
htop : ∃ x, f.limsSup < x
hbot : ∀ (x : α), f.limsSup ≤ x
⊢ ClusterPt f.limsSup f

case neg
α : Type u_2
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
f : Filter α
inst✝ : f.NeBot
hc : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f
hb : IsBounded (fun x1 x2 ↦ x1 ≤ x2) f
hn : Nontrivial α
htop : ∃ x, f.limsSup < x
hbot : ∃ x, x < f.limsSup
⊢ ClusterPt f.limsSup f
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : CompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : FirstCountableTopology α
inst✝¹ : OrderTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
h : u =ᶠ[f] ⊥
⊢ limsup u f = ⊥

Tactic:
rw [limsup_congr h]
    exact limsup_const_bot

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

Goal state before:
pp: a b c : EReal
h₁ : b ≠ ⊥ ∨ c ≠ ⊤
h₂ : b ≠ ⊤ ∨ c ≠ ⊥
⊢ a - b ≤ c ↔ a ≤ c + b

Tactic:
by
  suffices a + (-b) ≤ c ↔ a ≤ c - (-b) by simpa [sub_eq_add_neg]
  refine (le_sub_iff_add_le ?_ ?_).symm <;> simpa

Goal state after:
Module: Mathlib.Order.LiminfLimsup

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

Tactic:
simp only [blimsup_eq, eventually_cofinite, not_forall, sInf_eq_sInter, exists_prop]

Goal state after:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
⊢ ⋂₀ {a | {x | p x ∧ ¬s x ⊆ a}.Finite} = {x | {n | p n ∧ x ∈ s n}.Infinite}
Module: Mathlib.Data.EReal.Operations

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

Tactic:
contrapose! h
  exact sub_le_of_le_add h

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Finset

Goal state before:
pp: case neg
α : Type u_3
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
h✝¹ : Nonempty α
h✝ : ¬IsDirectedOrder α
h : ¬atTop.NeBot
⊢ Tendsto Finset.Iic atTop atTop

Tactic:
simp [not_ne_iff.mp <| Filter.neBot_iff.not.mp h]

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

Goal state before:
pp: β : Type u_4
inst✝² : Finite β
L : SummationFilter β
inst✝¹ : L.LeAtTop
inst✝ : L.NeBot
this : Fintype β
⊢ atTop = pure Finset.univ

Tactic:
rw [(isTop_iff_eq_top.mpr rfl).atTop_eq (a := Finset.univ), ← Finset.top_eq_univ,
      Ici_top, principal_singleton]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case neg
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
j0 : Subtype p
hj0 : BddBelow (range fun i ↦ f ↑i)
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
this : ∀ (j : Subtype p), Nonempty ↑(s ↑j)
A : ⋃ j, ⋂ i, Iic (f ↑i) = ⋃ j, ⋂ i, Iic (f ↑i)
j : Subtype p
Hj : j ∉ m
⊢ liminfReparam f s p j ∈ m

Tactic:
simp only [m, liminfReparam, if_neg Hj]

Goal state after:
case neg
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
j0 : Subtype p
hj0 : BddBelow (range fun i ↦ f ↑i)
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
this : ∀ (j : Subtype p), Nonempty ↑(s ↑j)
A : ⋃ j, ⋂ i, Iic (f ↑i) = ⋃ j, ⋂ i, Iic (f ↑i)
j : Subtype p
Hj : j ∉ m
⊢ ⋯.choose (Nat.find ⋯) ∈ {j | BddBelow (range fun i ↦ f ↑i)}
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f g : β → α
a₁ a₂ : α
hf : HasProd f a₁ L
hg : HasProd g a₂ L
⊢ HasProd (fun b ↦ f b / g b) (a₁ / a₂) L

Tactic:
simp only [div_eq_mul_inv]

Goal state after:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f g : β → α
a₁ a₂ : α
hf : HasProd f a₁ L
hg : HasProd g a₂ L
⊢ HasProd (fun b ↦ f b * (g b)⁻¹) (a₁ * a₂⁻¹) L
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁵ : CommMonoidWithZero α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder α
inst✝² : ZeroLEOneClass α
inst✝¹ : PosMulMono α
inst✝ : ClosedIciTopology α
f : ι → α
hf : ∀ (i : ι), 0 ≤ f i
h : Multipliable f L
hbot : L.NeBot
⊢ 0 ≤ ∏'[L] (x : ι), f x

pp: case neg
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁵ : CommMonoidWithZero α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder α
inst✝² : ZeroLEOneClass α
inst✝¹ : PosMulMono α
inst✝ : ClosedIciTopology α
f : ι → α
hf : ∀ (i : ι), 0 ≤ f i
h : Multipliable f L
hbot : ¬L.NeBot
⊢ 0 ≤ ∏'[L] (x : ι), f x

Tactic:
· exact h.hasProd.nonneg hf

Goal state after:
case neg
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁵ : CommMonoidWithZero α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder α
inst✝² : ZeroLEOneClass α
inst✝¹ : PosMulMono α
inst✝ : ClosedIciTopology α
f : ι → α
hf : ∀ (i : ι), 0 ≤ f i
h : Multipliable f L
hbot : ¬L.NeBot
⊢ 0 ≤ ∏'[L] (x : ι), f x
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
L : SummationFilter α
inst✝¹ : ContinuousInv₀ K
inst✝ : ContinuousMul K
a b : K
hf : HasProd f a L
hg : HasProd g b L
hb : b ≠ 0
⊢ HasProd (fun x ↦ f x / g x) (a / b) L

Tactic:
simp only [div_eq_mul_inv]

Goal state after:
α : Type u_1
K : Type u_4
inst✝³ : CommGroupWithZero K
inst✝² : TopologicalSpace K
f g : α → K
L : SummationFilter α
inst✝¹ : ContinuousInv₀ K
inst✝ : ContinuousMul K
a b : K
hf : HasProd f a L
hg : HasProd g b L
hb : b ≠ 0
⊢ HasProd (fun x ↦ f x * (g x)⁻¹) (a * b⁻¹) L
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:
by split_ifs with h <;> simp [h]

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

Goal state before:
pp: x : ℝ≥0
⊢ Filter.map toReal (𝓝[>] x) = 𝓝[>] ↑x

Tactic:
rw [isEmbedding_coe.map_nhdsWithin_eq, image_coe_Ioi]

Goal state after:
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 α
h✝ : Nonempty ι
x : α
hx :
  Tendsto (fun x ↦ 1 + ∑ i ∈ x, f i * ∏ j ∈ x with j < i, (1 + f j)) (SummationFilter.unconditional ι).filter (nhds x)
a : α
ha : HasSum (fun i ↦ f i * ∏ j < i, (1 + f j)) a
⊢ Tendsto (fun x ↦ ∑ i ≤ x, f i * ∏ j ≤ x with j < i, (1 + f j)) atTop (nhds a)

Tactic:
convert! ha.comp tendsto_finset_Iic_atTop_atTop using 2 with s

Goal state after:
ι : Type u_1
α : Type u_3
inst✝⁵ : CommSemiring α
inst✝⁴ : TopologicalSpace α
f : ι → α
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderBot ι
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
h✝ : Nonempty ι
x : α
hx :
  Tendsto (fun x ↦ 1 + ∑ i ∈ x, f i * ∏ j ∈ x with j < i, (1 + f j)) (SummationFilter.unconditional ι).filter (nhds x)
a : α
ha : HasSum (fun i ↦ f i * ∏ j < i, (1 + f j)) a
s : ι
⊢ ∑ i ≤ s, f i * ∏ j ≤ s with j < i, (1 + f j) = ((fun s ↦ ∑ b ∈ s, (fun i ↦ f i * ∏ j < i, (1 + f j)) b) ∘ Iic) s