mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Interval.Set.OrdConnectedComponent

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
x : α
⊢ ¬(s.ordConnectedComponent x).Nonempty ↔ x ∉ s

Tactic:
nonempty_ordConnectedComponent

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x : α
⊢ x ∉ s ↔ x ∉ s
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: r₁ r₂ : ℝ≥0∞
h₁ : r₁ ≠ ∞
h₂ : r₂ ≠ ∞
⊢ (r₁ + r₂).toNNReal = r₁.toNNReal + r₂.toNNReal

Tactic:
by
  lift r₁ to ℝ≥0 using h₁
  lift r₂ to ℝ≥0 using h₂
  rfl

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

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0
⊢ (⨆ i, ↑(f i)).toNNReal = ⨆ i, f i

Tactic:
by_cases h : BddAbove (range f)

Goal state after:
case pos
ι : Sort u_1
f : ι → ℝ≥0
h : BddAbove (range f)
⊢ (⨆ i, ↑(f i)).toNNReal = ⨆ i, f i

case neg
ι : Sort u_1
f : ι → ℝ≥0
h : ¬BddAbove (range f)
⊢ (⨆ i, ↑(f i)).toNNReal = ⨆ i, f i
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x y : EReal
h : x ≤ y
⊢ x.toENNReal ≤ y.toENNReal

Tactic:
by
  induction x
  · simp
  · by_cases hy_top : y = ⊤
    · simp [hy_top]
    simp only [toENNReal, coe_ne_top, ↓reduceIte, toReal_coe, hy_top]
    exact ENNReal.ofReal_le_ofReal <| EReal.toReal_le_toReal h (coe_ne_bot _) hy_top
  · simp_all

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

Goal state before:
pp: m n : ℕ
⊢ ↑↑m = ↑↑n ↔ m = n

Tactic:
EReal.coe_eq_coe_iff,

Goal state after:
m n : ℕ
⊢ ↑m = ↑n ↔ m = n
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
htop : b ≠ ∞ ∨ a ≠ ∞
hzero : b ≠ 0 ∨ a ≠ 0
⊢ (a / b)⁻¹ = b / a

Tactic:
rw [← ENNReal.inv_ne_zero] at htop

Goal state after:
a b : ℝ≥0∞
htop : b⁻¹ ≠ 0 ∨ a ≠ ∞
hzero : b ≠ 0 ∨ a ≠ 0
⊢ (a / b)⁻¹ = b / a
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: 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
exps : HeightOneSpectrum R → ℤ
h_exps : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, exps v = 0
⊢ count K v (∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ exps v) = exps v

Tactic:
by
  convert! count_finsuppProd K v (Finsupp.mk h_exps.toFinset exps (fun _ ↦ h_exps.mem_toFinset))
  rw [finprod_eq_finsetProd_of_mulSupport_subset (s := h_exps.toFinset), Finsupp.prod]
  · rfl
  · rw [Finite.coe_toFinset]
    intro v hv h
    rw [mem_mulSupport, h, zpow_zero] at hv
    exact hv (Eq.refl 1)

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: 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
J : Ideal R
⊢ 0 ≤ count K v ↑J

Tactic:
by
  by_cases hJ : J = 0
  · simp only [hJ, Submodule.zero_eq_bot, coeIdeal_bot, count_zero, le_refl]
  · classical simp only [count_coe K v hJ, Nat.cast_nonneg]

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

Goal state before:
pp: case neg.inr.inr
ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ a * ⨆ i, f i = ⨆ i, a * f i

Tactic:
· exact (mulLeftOrderIso _ <| isUnit_iff.2 ⟨ha₀, ha⟩).map_iSup _

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:
by
  rw [add_right_comm, dist_comm y₁]
  apply dist_triangle4

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

Goal state before:
pp: case mp
α : Type u
inst✝ : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, 0 < i ∧ {p | dist p.1 p.2 < i} ⊆ s) → ∃ i, p i ∧ {p | dist p.1 p.2 ≤ f i} ⊆ s

Tactic:
rintro ⟨ε, ε₀, hε⟩
    rcases exists_between ε₀ with ⟨ε', hε'⟩
    rcases hf ε' hε'.1 with ⟨i, hi, H⟩
    exact ⟨i, hi, fun x (hx : _ ≤ _) => hε <| lt_of_le_of_lt (le_trans hx H) hε'.2⟩

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ ⋃ x ∈ t, closedEBall x ε = univ
⊢ SecondCountableTopology α

Tactic:
suffices SeparableSpace α from UniformSpace.secondCountable_of_separable α
  have : ∀ ε > 0, ∃ t : Set α, Set.Countable t ∧ univ ⊆ ⋃ x ∈ t, closedEBall x ε := by
    simpa only [univ_subset_iff] using hs
  rcases subset_countable_closure_of_almost_dense_set (univ : Set α) this with ⟨t, -, htc, ht⟩
  exact ⟨⟨t, htc, fun x => ht (mem_univ x)⟩⟩

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

Goal state before:
pp: a b : ℝ≥0
⊢ ↑a ≤ ↑b + dist a b

Tactic:
← sub_le_iff_le_add'

Goal state after:
a b : ℝ≥0
⊢ ↑a - ↑b ≤ dist a b
Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas

Goal state before:
pp: α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
u : Set α
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
this : Iic ε ∈ 𝓝 0
⊢ ∀ᶠ (r : ℝ) in 𝓝 0, closedBall x r ⊆ u

Tactic:
filter_upwards [this] with _ hr using Subset.trans (closedBall_subset_closedBall hr) hε

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
⊢ Ioc a b ⊆ closure[inst✝³] (interior (Ioc a b))

Tactic:
by
  rcases eq_or_ne a b with (rfl | h)
  · simp
  · calc
      Ioc a b ⊆ Icc a b := Ioc_subset_Icc_self
      _ = closure (Ioo a b) := (closure_Ioo h).symm
      _ ⊆ closure (interior (Ioc a b)) :=
        closure_mono (interior_maximal Ioo_subset_Ioc_self isOpen_Ioo)

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

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
s : Set α
a : α
hsa : a ∈ upperBounds s
hsf : a ∈ closure[inst✝²] s
⊢ IsLUB s a

Tactic:
rw [mem_closure_iff_clusterPt, ClusterPt, inf_comm] at hsf
  exact isLUB_of_mem_nhds hsa (mem_principal_self s)

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
⊢ IsClosed[inst✝³] (Ioo a b) ↔ b ≤ a

Tactic:
by
  refine ⟨fun h => le_of_not_gt fun hab => ?_, by simp_all⟩
  have := h.closure_eq
  rw [closure_Ioo hab.ne, Icc_eq_Ioo_same_iff] at this
  exact this hab.le

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

Goal state before:
pp: ι : Type u_1
E : Type u_2
F : Type u_3
inst✝² : Fintype ι
inst✝¹ : SeminormedGroup E
inst✝ : Fintype F
g : ι → E
f : F → ι
⊢ ‖g ∘ f‖ ≤ ‖g‖

Tactic:
rw [pi_norm_le_iff_of_nonneg' (by positivity)]

Goal state after:
ι : Type u_1
E : Type u_2
F : Type u_3
inst✝² : Fintype ι
inst✝¹ : SeminormedGroup E
inst✝ : Fintype F
g : ι → E
f : F → ι
⊢ ∀ (i : F), ‖(g ∘ f) i‖ ≤ ‖g‖
Module: Mathlib.Analysis.Normed.Group.Constructions

Goal state before:
pp: ι : Type u_1
G : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → NormedAddCommGroup (G i)
i : ι
y : G i
⊢ ∀ (b : ι), ‖single i y b‖₊ = single i ‖y‖₊ b

Tactic:
intro b

Goal state after:
ι : Type u_1
G : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → NormedAddCommGroup (G i)
i : ι
y : G i
b : ι
⊢ ‖single i y b‖₊ = single i ‖y‖₊ b
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: 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
a b c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : b ≠ 0
⊢ a + spanSingleton R⁰ (c.divMod b a) * b = c

Tactic:
by
  rw [divMod, dif_pos ⟨hac, ha, hb⟩]
  exact (IsDedekindDomain.exists_add_spanSingleton_mul_eq hac ha hb).choose_spec

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

Goal state before:
pp: case refine_2
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTop α
inst✝ : CompactIccSpace α
x✝ : Set α
hs : x✝ ∈ atBot
h✝ : Nonempty α
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ x✝

Tactic:
· obtain ⟨t, ht⟩ := mem_atBot_sets.mp hs
    refine ⟨Icc t ⊤, isCompact_Icc, fun _ hx ↦ ?_⟩
    exact (not_and_or.mp hx).casesOn (fun h ↦ ht _ (le_of_not_ge h)) (fun h ↦ (h le_top).elim)

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

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ BddBelow (f '' [[a, b]])

Tactic:
h.image_uIcc_eq_Icc

Goal state after:
case refine_1
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ BddBelow (Icc (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]])))
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ BddAbove (f '' [[a, b]])

Tactic:
h.image_uIcc_eq_Icc

Goal state after:
case refine_2
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ BddAbove (Icc (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]])))
Module: Mathlib.Topology.MetricSpace.ProperSpace

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
f : Filter α
hf : Cauchy f
⊢ ∃ x, f ≤ nhds x

Tactic:
obtain ⟨t, t_fset, ht⟩ : ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, dist x y < 1 :=
      (Metric.cauchy_iff.1 hf).2 1 zero_lt_one

Goal state after:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
f : Filter α
hf : Cauchy f
t : Set α
t_fset : t ∈ f
ht : ∀ x ∈ t, ∀ y ∈ t, dist x y < 1
⊢ ∃ x, f ≤ nhds x
Module: Mathlib.Topology.MetricSpace.Cauchy

Goal state before:
pp: α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : UniformCauchySeqOn F atTop s
ε : ℝ
hε : ε > 0
u : Set (α × α) := {a | dist a.1 a.2 < ε}
⊢ ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u

Tactic:
by simp [u]

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

Goal state before:
pp: case mp
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : UniformCauchySeqOn F atTop s
ε : ℝ
hε : ε > 0
u : Set (α × α) := {a | dist a.1 a.2 < ε}
hu : u ∈ 𝓤 α
⊢ ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε

Tactic:
rw [← Filter.eventually_atTop_prod_self' (p := fun m =>
      ∀ x ∈ s, dist (F m.fst x) (F m.snd x) < ε)]

Goal state after:
case mp
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : UniformCauchySeqOn F atTop s
ε : ℝ
hε : ε > 0
u : Set (α × α) := {a | dist a.1 a.2 < ε}
hu : u ∈ 𝓤 α
⊢ ∀ᶠ (x : β × β) in atTop, ∀ x_1 ∈ s, dist (F x.1 x_1) (F x.2 x_1) < ε
Module: Mathlib.Topology.MetricSpace.Cauchy

Goal state before:
pp: case h
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hab : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u
N : β
hN : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
⊢ ∀ (b : β × β), (N, N) ≤ b → ∀ x ∈ s, (F b.1 x, F b.2 x) ∈ u

Tactic:
intro b

Goal state after:
case h
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hab : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u
N : β
hN : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
b : β × β
⊢ (N, N) ≤ b → ∀ x ∈ s, (F b.1 x, F b.2 x) ∈ u
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
⊢ (𝓤 E).HasBasis (fun ε ↦ 0 < ε) fun ε ↦ {p | ‖p.1⁻¹ * p.2‖ < ε}

Tactic:
convert Metric.uniformity_basis_dist (α := E)
  simp [dist_eq_norm_inv_mul]

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

Goal state before:
pp: α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hab : a ≤ b
hfab : f a ≤ f b
hf_c : ContinuousOn f (Icc a b)
hf_i : InjOn f (Icc a b)
this : Fact (a ≤ b)
g : ↑(Icc a b) → δ := (Icc a b).domRestrict f
hgab : g ⊥ ≤ g ⊤
⊢ StrictMono g

Tactic:
exact Continuous.strictMono_of_inj_boundedOrder (f := g) hf_c.domRestrict hgab hf_i.injective

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

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

Tactic:
hm

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen[inst✝³] (⇑e ⁻¹' Iio a)

Tactic:
e.preimage_Iio

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen[inst✝³] (Iio (e.symm a))
Module: Mathlib.Topology.Order.MonotoneConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ SupConvergenceClass α

Tactic:
by
  refine ⟨fun a s ha => tendsto_order.2 ⟨fun b hb => ?_, fun b hb => ?_⟩⟩
  · rcases ha.exists_between hb with ⟨c, hcs, bc, bca⟩
    lift c to s using hcs
    exact (eventually_ge_atTop c).mono fun x hx => bc.trans_le hx
  · exact Eventually.of_forall fun x => (ha.1 x.2).trans_lt hb

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

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

Tactic:
obtain rfl : y.toENNReal = x := by simp [← hy]

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

Goal state before:
pp: case pos
x y : ℝ
hy : 0 ≤ ↑y
hxy : x ≤ y
⊢ 0 = (↑x).toENNReal - (↑y).toENNReal

Tactic:
exact (tsub_eq_zero_of_le <| toENNReal_le_toENNReal <| EReal.coe_le_coe_iff.mpr hxy).symm

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
hbot : f.NeBot
hlt : liminf u f < limsup u f
a : α
as : a ∈ s
la : liminf u f < a
au : a < limsup u f
b : α
bs : b ∈ s
ab : a < b
bu : b < limsup u f
⊢ False

Tactic:
have A : ∃ᶠ n in f, u n < a := frequently_lt_of_liminf_lt (IsBounded.isCobounded_ge h) la

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
hbot : f.NeBot
hlt : liminf u f < limsup u f
a : α
as : a ∈ s
la : liminf u f < a
au : a < limsup u f
b : α
bs : b ∈ s
ab : a < b
bu : b < limsup u f
A : ∃ᶠ (n : β) in f, u n < a
⊢ False
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x y z t : EReal
h : x ≤ y
h' : z < t
hx_top : x ≠ ⊤
hy_bot : y ≠ ⊥
⊢ x < t + (y - z)

Tactic:
add_sub_assoc',

Goal state after:
x y z t : EReal
h : x ≤ y
h' : z < t
hx_top : x ≠ ⊤
hy_bot : y ≠ ⊥
⊢ x < t + y - z
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftStrictMono α
x ε : α
u : ℕ → α
hu_bdd : IsBoundedUnder LE.le atTop u
hu : limsup u atTop ≤ x
hε : 0 < ε
h : ∀ᶠ (n : ℕ) in atTop, u n < x + ε
⊢ ∃ n, u ↑n < x + ε

Tactic:
simp only [eventually_atTop] at h

Goal state after:
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftStrictMono α
x ε : α
u : ℕ → α
hu_bdd : IsBoundedUnder LE.le atTop u
hu : limsup u atTop ≤ x
hε : 0 < ε
h : ∃ a, ∀ (b : ℕ), a ≤ b → u b < x + ε
⊢ ∃ n, u ↑n < x + ε
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftStrictMono α
x ε : α
u : ℕ → α
hu_bdd : IsBoundedUnder GE.ge atTop u
hu : x ≤ liminf u atTop
hε : ε < 0
h : ∀ᶠ (n : ℕ) in atTop, x + ε < u n
⊢ ∃ n, x + ε < u ↑n

Tactic:
simp only [eventually_atTop] at h

Goal state after:
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftStrictMono α
x ε : α
u : ℕ → α
hu_bdd : IsBoundedUnder GE.ge atTop u
hu : x ≤ liminf u atTop
hε : ε < 0
h : ∃ a, ∀ (b : ℕ), a ≤ b → x + ε < u b
⊢ ∃ n, x + ε < u ↑n
Module: Mathlib.Order.Filter.AtTopBot.Finset

Goal state before:
pp: α : Type u_3
β : Type u_4
s : Set (Finset α)
hs : s ∈ atTop
⊢ s ∈ map Finset.toLeft atTop

Tactic:
simp only [mem_atTop_sets, Filter.mem_map, Set.mem_preimage] at hs ⊢

Goal state after:
α : Type u_3
β : Type u_4
s : Set (Finset α)
hs : ∃ a, ∀ (b : Finset α), a ⊆ b → b ∈ s
⊢ ∃ a, ∀ (b : Finset (α ⊕ β)), a ⊆ b → b.toLeft ∈ s
Module: Mathlib.Order.Filter.AtTopBot.Finset

Goal state before:
pp: α : Type u_3
β : Type u_4
s : Set (Finset β)
hs : s ∈ atTop
⊢ s ∈ map Finset.toRight atTop

Tactic:
simp only [mem_atTop_sets, Filter.mem_map, Set.mem_preimage] at hs ⊢

Goal state after:
α : Type u_3
β : Type u_4
s : Set (Finset β)
hs : ∃ a, ∀ (b : Finset β), a ⊆ b → b ∈ s
⊢ ∃ a, ∀ (b : Finset (α ⊕ β)), a ⊆ b → b.toRight ∈ s
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : 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 : ι → α
H : ¬∃ j, s ↑j = ∅
H' : ∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i)
⊢ ∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i)

Tactic:
exact H'

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case neg.H
α : 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 : ι → α
H : ¬∃ j, s ↑j = ∅
H' : ∃ j, BddBelow (range fun i ↦ f ↑i)
⊢ ∃ j, BddBelow (range fun i ↦ f ↑i)

Tactic:
exact H'

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

Goal state before:
pp: case intro
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : TopologicalSpace M
α : Type u_3
β : Type u_4
inst✝¹ : Countable β
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))
s : β → α
val✝ : Encodable β
⊢ R (m (⨆ i, ⨆ b ∈ decode₂ β i, s b)) (∏' (b : β), m (s b))

Tactic:
← tprod_iSup_decode₂ _ m0 s

Goal state after:
case intro
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : TopologicalSpace M
α : Type u_3
β : Type u_4
inst✝¹ : Countable β
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))
s : β → α
val✝ : Encodable β
⊢ R (m (⨆ i, ⨆ b ∈ decode₂ β i, s b)) (∏' (i : ℕ), m (⨆ b ∈ decode₂ β i, s b))
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : CommGroup α
inst✝¹ : IsUniformGroup α
f : β → α
inst✝ : CompleteSpace α
⊢ Multipliable f ↔ ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Set β), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e

Tactic:
by
  rw [multipliable_iff_cauchySeq_finset, cauchySeq_finset_iff_tprod_vanishing]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : CommGroup α
inst✝¹ : IsUniformGroup α
f g : β → α
inst✝ : CompleteSpace α
hf : Multipliable f
h : ∀ (b : β), g b = 1 ∨ g b = f b
e : Set α
he : e ∈ 𝓝 1
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
t : Finset β
ht : Disjoint t s
⊢ ∀ x ∈ t, x ∉ {b ∈ t | g b = f b} → g x = 1

Tactic:
intro b

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : CommGroup α
inst✝¹ : IsUniformGroup α
f g : β → α
inst✝ : CompleteSpace α
hf : Multipliable f
h : ∀ (b : β), g b = 1 ∨ g b = f b
e : Set α
he : e ∈ 𝓝 1
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
t : Finset β
ht : Disjoint t s
b : β
⊢ b ∈ t → b ∉ {b ∈ t | g b = f b} → g b = 1
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: α : Type u_2
L : SummationFilter α
f : α → ℝ
y : ℝ
hf₀ : ∀ (n : α), 0 ≤ f n
hy : HasSum f y L
⊢ HasSum (fun x ↦ (f x).toNNReal) y.toNNReal L

Tactic:
rcases L.neBot_or_eq_bot with _ | hL

Goal state after:
case inl
α : Type u_2
L : SummationFilter α
f : α → ℝ
y : ℝ
hf₀ : ∀ (n : α), 0 ≤ f n
hy : HasSum f y L
h✝ : L.NeBot
⊢ HasSum (fun x ↦ (f x).toNNReal) y.toNNReal L

case inr
α : Type u_2
L : SummationFilter α
f : α → ℝ
y : ℝ
hf₀ : ∀ (n : α), 0 ≤ f n
hy : HasSum f y L
hL : L.filter = ⊥
⊢ HasSum (fun x ↦ (f x).toNNReal) y.toNNReal L
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: α : Type u_2
L : SummationFilter α
f : α → ℝ≥0
⊢ Summable (fun a ↦ ↑(f a)) L ↔ Summable f L

Tactic:
rcases L.neBot_or_eq_bot with _ | hL

Goal state after:
case inl
α : Type u_2
L : SummationFilter α
f : α → ℝ≥0
h✝ : L.NeBot
⊢ Summable (fun a ↦ ↑(f a)) L ↔ Summable f L

case inr
α : Type u_2
L : SummationFilter α
f : α → ℝ≥0
hL : L.filter = ⊥
⊢ Summable (fun a ↦ ↑(f a)) L ↔ Summable f L
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ≥0∞
⊢ ⇑h ⁻¹' Metric.closedEBall x r = Metric.closedEBall (h.symm x) r

Tactic:
by
  rw [← h.isometry.preimage_closedEBall (h.symm x) r, h.apply_symm_apply]

Goal state after: