mathlib-initiative/mathlib-tactics huggingface dataset:
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:
;

Goal state after:
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
Module: Mathlib.Topology.Algebra.Ring.Real

Goal state before:
pp: ⊢ (Iio ∞).OrdConnected

Tactic:
;

Goal state after:
⊢ (Iio ∞).OrdConnected
Module: Mathlib.Topology.Algebra.Ring.Real

Goal state before:
pp: ⊢ IsOpen (Iio ∞)

Tactic:
;

Goal state after:
⊢ IsOpen (Iio ∞)
Module: Mathlib.Topology.Order.MonotoneContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : closure[inst✝²] (f '' s) ∈ 𝓝[≥] f a
b : β
hb : b > f a
b' : β
hb' : Ico (f a) b' ⊆ closure[inst✝²] (f '' s)
hab' : f a < b'
hbb' : b' ≤ b
⊢ ∃ c ∈ s, f c ∈ Ioo (f a) b

Tactic:
rcases exists_between hab' with ⟨c', hc'⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : closure[inst✝²] (f '' s) ∈ 𝓝[≥] f a
b : β
hb : b > f a
b' : β
hb' : Ico (f a) b' ⊆ closure[inst✝²] (f '' s)
hab' : f a < b'
hbb' : b' ≤ b
c' : β
hc' : f a < c' ∧ c' < b'
⊢ ∃ c ∈ s, f c ∈ Ioo (f a) b
Module: Mathlib.Topology.Instances.Rat

Goal state before:
pp: x y : ℕ
⊢ dist ↑x ↑y = dist ↑x ↑y

Tactic:
← Rat.dist_cast

Goal state after:
x y : ℕ
⊢ dist ↑↑x ↑↑y = dist ↑x ↑y
Module: Mathlib.Topology.Instances.Rat

Goal state before:
pp: x y : ℕ
⊢ dist ↑↑x ↑↑y = dist ↑x ↑y

Tactic:
;

Goal state after:
x y : ℕ
⊢ dist ↑↑x ↑↑y = dist ↑x ↑y
Module: Mathlib.Topology.Instances.Rat

Goal state before:
pp: x y : ℤ
⊢ dist ↑x ↑y = dist ↑x ↑y

Tactic:
← Rat.dist_cast

Goal state after:
x y : ℤ
⊢ dist ↑↑x ↑↑y = dist ↑x ↑y
Module: Mathlib.Topology.Instances.Rat

Goal state before:
pp: x y : ℤ
⊢ dist ↑↑x ↑↑y = dist ↑x ↑y

Tactic:
;

Goal state after:
x y : ℤ
⊢ dist ↑↑x ↑↑y = dist ↑x ↑y
Module: Mathlib.Analysis.Normed.Group.Rat

Goal state before:
pp: m : ℤ
⊢ ‖↑↑m‖ = ‖↑m‖

Tactic:
;

Goal state after:
m : ℤ
⊢ ‖↑↑m‖ = ‖↑m‖
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: α : Type u_3
s : Finset α
f : α → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
⊢ ENNReal.ofReal (∏ i ∈ s, f i) = ∏ i ∈ s, ENNReal.ofReal (f i)

Tactic:
ENNReal.ofReal,

Goal state after:
α : Type u_3
s : Finset α
f : α → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
⊢ ↑(∏ i ∈ s, f i).toNNReal = ∏ i ∈ s, ↑(f i).toNNReal
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
⊢ ENNReal.ofReal (∑ i ∈ s, f i) = ∑ i ∈ s, ENNReal.ofReal (f i)

Tactic:
ENNReal.ofReal,

Goal state after:
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
⊢ ↑(∑ i ∈ s, f i).toNNReal = ∑ i ∈ s, ↑(f i).toNNReal
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
b : α
hb : ∀ᶠ (x : α) in map u f, (fun x1 x2 ↦ x1 ≤ x2) x b
a : β
ha : a ∈ {a | u a ≤ b}
⊢ u a ≤ b

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
b : α
hb : ∀ᶠ (x : α) in map u f, (fun x1 x2 ↦ x1 ≤ x2) x b
a : β
ha : a ∈ {a | u a ≤ b}
⊢ u a ≤ b
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot
h : ⊥ ≠ ⊥
⊢ False

Tactic:
;

Goal state after:
case bot
h : ⊥ ≠ ⊥
⊢ False
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
c : γ
hc : ∀ᶠ (x : γ) in map (g ∘ f) l, (fun x1 x2 ↦ x1 ≤ x2) x c
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l f

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
c : γ
hc : ∀ᶠ (x : γ) in map (g ∘ f) l, (fun x1 x2 ↦ x1 ≤ x2) x c
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l f
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
s : Set α
h : BddAbove s
hs : s.Nonempty
⊢ sInf {a | ∀ x ∈ s, x ≤ a} = sSup s

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
s : Set α
h : BddAbove s
hs : s.Nonempty
⊢ sInf {a | ∀ x ∈ s, x ≤ a} = sSup s
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLattice α
u : β → α
inst✝ : Nonempty β
hu : BddAbove (range u)
⊢ limsup u ⊤ = ⨆ i, u i

Tactic:
by
  rw [limsup, map_top, limsSup_principal_eq_csSup hu (range_nonempty _), sSup_range]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
⊢ ⨅ i, ⨆ a ∈ Ici i, u a = ⨅ n, ⨆ i, ⨆ (_ : i ≥ n), u i

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
⊢ ⨅ i, ⨆ a ∈ Ici i, u a = ⨅ n, ⨆ i, ⨆ (_ : i ≥ n), u i
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
b : β
hb : u b ≠ ⊥ → (p b ↔ q b)
hu : u b = ⊥
⊢ p b → u b ≤ a ↔ q b → u b ≤ a

pp: case inr
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
b : β
hb : u b ≠ ⊥ → (p b ↔ q b)
hu : u b ≠ ⊥
⊢ p b → u b ≤ a ↔ q b → u b ≤ a

Tactic:
;

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
b : β
hb : u b ≠ ⊥ → (p b ↔ q b)
hu : u b = ⊥
⊢ p b → u b ≤ a ↔ q b → u b ≤ a

case inr
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
b : β
hb : u b ≠ ⊥ → (p b ↔ q b)
hu : u b ≠ ⊥
⊢ p b → u b ≤ a ↔ q b → u b ≤ a
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s t : Set α
f : α → β
hf : LocallyLipschitzOn t f
h : s ⊆ t
x : α
hx : x ∈ s
K : ℝ≥0
u : Set α
hu : u ∈ 𝓝[t] x
hfu : LipschitzOnWith K f u
⊢ ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Tactic:
;

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s t : Set α
f : α → β
hf : LocallyLipschitzOn t f
h : s ⊆ t
x : α
hx : x ∈ s
K : ℝ≥0
u : Set α
hu : u ∈ 𝓝[t] x
hfu : LipschitzOnWith K f u
⊢ ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
x y : α
r : ℝ≥0∞
h : LipschitzWith K f
hK : K ≠ 0
hr : edist x y < r
⊢ ↑K * edist x y < ↑K * r

Tactic:
;

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
x y : α
r : ℝ≥0∞
h : LipschitzWith K f
hK : K ≠ 0
hr : edist x y < r
⊢ ↑K * edist x y < ↑K * r
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: case hinf
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
x y : α
r : ℝ≥0∞
h : LipschitzWith K f
hK : K ≠ 0
hr : edist x y < r
⊢ ↑K ≠ ∞

Tactic:
;

Goal state after:
case hinf
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
x y : α
r : ℝ≥0∞
h : LipschitzWith K f
hK : K ≠ 0
hr : edist x y < r
⊢ ↑K ≠ ∞
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
K : ℝ≥0
f : α → α
hf : LipschitzWith K f
n : ℕ
⊢ LipschitzWith (K ^ n * K) f^[n + 1]

Tactic:
;

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
K : ℝ≥0
f : α → α
hf : LipschitzWith K f
n : ℕ
⊢ LipschitzWith (K ^ n * K) f^[n + 1]
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
⊢ (fun i ↦ ⨅ (_ : i ∈ f), a ⊔ ⨆ a ∈ i, u a) = fun s ↦ ⨅ (_ : s ∈ f), (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
⊢ (fun i ↦ ⨅ (_ : i ∈ f), a ⊔ ⨆ a ∈ i, u a) = fun s ↦ ⨅ (_ : s ∈ f), (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
s : Set β
⊢ ⨅ (_ : s ∈ f), a ⊔ ⨆ a ∈ s, u a = ⨅ (_ : s ∈ f), (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
s : Set β
⊢ ⨅ (_ : s ∈ f), a ⊔ ⨆ a ∈ s, u a = ⨅ (_ : s ∈ f), (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
s : Set β
⊢ (fun j ↦ a ⊔ ⨆ a ∈ s, u a) = fun x ↦ (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
s : Set β
⊢ (fun j ↦ a ⊔ ⨆ a ∈ s, u a) = fun x ↦ (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
s : Set β
hs : s ∈ f
⊢ a ⊔ ⨆ a ∈ s, u a = (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
s : Set β
hs : s ∈ f
⊢ a ⊔ ⨆ a ∈ s, u a = (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ ⨅ i ∈ f, (⨆ a ∈ i, u a) ⊓ aᶜ = ⨅ s ∈ f, ⨆ a_1 ∈ s, u a_1 ⊓ aᶜ

Tactic:
inf_comm,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ ⨅ i ∈ f, aᶜ ⊓ ⨆ a ∈ i, u a = ⨅ s ∈ f, ⨆ a_1 ∈ s, u a_1 ⊓ aᶜ
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ ⨅ i ∈ f, ⨆ i_1 ∈ i, aᶜ ⊓ u i_1 = ⨅ s ∈ f, ⨆ a_1 ∈ s, u a_1 ⊓ aᶜ

Tactic:
inf_comm

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
f : α → α
hf : LocallyLipschitz f
n : ℕ
⊢ LocallyLipschitz (f^[n] ∘ f)

Tactic:
;

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
f : α → α
hf : LocallyLipschitz f
n : ℕ
⊢ LocallyLipschitz (f^[n] ∘ f)
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot
a b : EReal
h : a = ⊥
⊢ a - ⊥ ≤ b

Tactic:
;

Goal state after:
case bot
a b : EReal
h : a = ⊥
⊢ a - ⊥ ≤ b
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b c : EReal
hc : c < b + a
⊢ ∃ b' < b, c < b' + a

Tactic:
;

Goal state after:
a b c : EReal
hc : c < b + a
⊢ ∃ b' < b, c < b' + a
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn (fun y ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith K (fun x ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < ↑δ
hδ : ↑δ * ↑(3 * K) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < ↑δ
A : s ∩ Metric.eball x ↑δ ∈ 𝓝[s] x
B : t ∩ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).1 ∈ s
hax : (a, b).1 ∈ Metric.eball x ↑δ
hbt : (a, b).2 ∈ t
hby : (a, b).2 ∈ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2}
⊢ ↑K * (↑δ + ↑δ) + ε / 2 + ↑K * ↑δ = ↑δ * (3 * ↑K) + ε / 2

Tactic:
;

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn (fun y ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith K (fun x ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < ↑δ
hδ : ↑δ * ↑(3 * K) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < ↑δ
A : s ∩ Metric.eball x ↑δ ∈ 𝓝[s] x
B : t ∩ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).1 ∈ s
hax : (a, b).1 ∈ Metric.eball x ↑δ
hbt : (a, b).2 ∈ t
hby : (a, b).2 ∈ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2}
⊢ ↑K * (↑δ + ↑δ) + ε / 2 + ↑K * ↑δ = ↑δ * (3 * ↑K) + ε / 2
Module: Mathlib.Order.Filter.AtTopBot.Finset

Goal state before:
pp: α : Type u_3
β : Type u_4
⊢ Tendsto Finset.toLeft atTop atTop

Tactic:
intro s hs
  simp only [mem_atTop_sets, Filter.mem_map, Set.mem_preimage] at hs ⊢
  obtain ⟨t, H⟩ := hs
  exact ⟨t.disjSum ∅, fun b hb ↦ H _ (by simpa [← Finset.coe_subset, Set.subset_def] using hb)⟩

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Infinite α
f : ℕ → β
l : Filter β
⊢ Tendsto (fun s ↦ f s.card) atTop l ↔ Tendsto f atTop l

Tactic:
← map_card_atTop (α := α),

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Infinite α
f : ℕ → β
l : Filter β
⊢ Tendsto (fun s ↦ f s.card) atTop l ↔ Tendsto f (map Finset.card atTop) l
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe_coe
x✝ y✝ : ℝ
⊢ -x✝ * y✝ = -(x✝ * y✝)

Tactic:
;

Goal state after:
case coe_coe
x✝ y✝ : ℝ
⊢ -x✝ * y✝ = -(x✝ * y✝)
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst✝ : L.LeAtTop
f : γ ↪ β
⊢ (L.comap f).support = univ

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst✝ : L.LeAtTop
f : γ ↪ β
⊢ (L.comap f).support = univ
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder β
inst✝² : Nonempty β
inst✝¹ : IsDirectedOrder β
inst✝ : IsCodirectedOrder β
⊢ (Filter.map (fun p ↦ Finset.Icc p.1 p.2) (atBot ×ˢ atTop)).NeBot

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : Preorder β
inst✝³ : LocallyFiniteOrder β
inst✝² : Nonempty β
inst✝¹ : IsDirectedOrder β
inst✝ : IsCodirectedOrder β
⊢ (Filter.map (fun p ↦ Finset.Icc p.1 p.2) (atBot ×ˢ atTop)).NeBot
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: n x : ℕ
⊢ x ∈ Finset.Iic n ↔ x ∈ Finset.range (n + 1)

Tactic:
;

Goal state after:
n x : ℕ
⊢ x ∈ Finset.Iic n ↔ x ∈ Finset.range (n + 1)
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
s : Set (Finset ℕ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → Finset.range (b + 1) ∈ s
b : ℕ
hb : a + 1 ≤ b
⊢ b = b - 1 + 1

Tactic:
;

Goal state after:
this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
s : Set (Finset ℕ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → Finset.range (b + 1) ∈ s
b : ℕ
hb : a + 1 ≤ b
⊢ b = b - 1 + 1
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
hL : L.filter.NeBot
⊢ L.NeBot

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
hL : L.filter.NeBot
⊢ L.NeBot
Module: Mathlib.Data.EReal.Operations

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

Tactic:
;

Goal state after:
a b c : EReal
ha : 0 ≤ a
hb : 0 ≤ b
⊢ (a + b) * c = c * a + c * b
Module: Mathlib.Data.EReal.Operations

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

Tactic:
;

Goal state after:
a b c : EReal
ha : 0 ≤ a
hb : 0 ≤ b
⊢ (a + b) * c = a * c + c * b
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
v : α → β
l : β → γ
u : γ → β
gc : GaloisConnection l u
hlv : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ l (v x)
hv_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
⊢ l (limsup v f) ≤ limsup (fun x ↦ l (v x)) f

Tactic:
refine le_limsSup_of_le hlv fun c hc => ?_

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
v : α → β
l : β → γ
u : γ → β
gc : GaloisConnection l u
hlv : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ l (v x)
hv_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
c : γ
hc : ∀ᶠ (n : γ) in map (fun x ↦ l (v x)) f, n ≤ c
⊢ l (limsup v f) ≤ c
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
i : ι
i_s : i ∈ s
bddsup : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ s.sup' ⋯ fun i ↦ F i a
⊢ ∃ i ∈ s, IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)

Tactic:
use i, i_s

Goal state after:
case right
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
i : ι
i_s : i ∈ s
bddsup : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ s.sup' ⋯ fun i ↦ F i a
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
bddsup : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ s.sup' hs fun i ↦ F i a
i : ι
i_s : i ∈ s
a : α
⊢ ∃ b ∈ s, F i a ≤ F b a

Tactic:
use i, i_s

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

Goal state before:
pp: case pos.convert_5
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport fun b ↦ f b) ∩ L.support).Finite
⊢ ∀ b ∈ L.support, b ∉ ⋯.toFinset → f b = 1

pp: case pos.convert_6
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport fun b ↦ f b) ∩ L.support).Finite
⊢ L.HasSupport

Tactic:
· grind [Set.Finite.mem_toFinset, mem_mulSupport]

Goal state after:
case pos.convert_6
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport fun b ↦ f b) ∩ L.support).Finite
⊢ L.HasSupport
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
L : SummationFilter β
inst✝ : IsEmpty β
⊢ HasProd f 1 L

Tactic:
by
  convert! hasProd_one

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
L : SummationFilter β
inst✝ : Subsingleton α
⊢ HasProd f 1 L

Tactic:
by
  convert! hasProd_one

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

Goal state before:
pp: case e'_5
α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝⁴ : CommGroup α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalGroup α
f : β → α
a : α
inst✝¹ : L.LeAtTop
inst✝ : DecidableEq β
hf : HasProd f a L
b : β
⊢ (fun n ↦ if n = b then 1 else f n) = update f b 1

pp: case e'_6
α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝⁴ : CommGroup α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalGroup α
f : β → α
a : α
inst✝¹ : L.LeAtTop
inst✝ : DecidableEq β
hf : HasProd f a L
b : β
⊢ a / f b = 1 / f b * a

Tactic:
· ext n
    rw [Function.update_apply]

Goal state after:
case e'_6
α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝⁴ : CommGroup α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalGroup α
f : β → α
a : α
inst✝¹ : L.LeAtTop
inst✝ : DecidableEq β
hf : HasProd f a L
b : β
⊢ a / f b = 1 / f b * a
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
L : SummationFilter β
inst✝ : L.HasSupport
h : HasFiniteMulSupport f
⊢ ∀ b ∉ Set.Finite.toFinset h, f b = 1

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
L : SummationFilter β
inst✝ : L.HasSupport
h : HasFiniteMulSupport f
⊢ ∀ b ∉ Set.Finite.toFinset h, f b = 1
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

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

Tactic:
refine (mul_one a).symm.trans (hf.update' b 1 ?_)

Goal state after:
β : Type u_2
L : SummationFilter β
inst✝⁶ : L.LeAtTop
inst✝⁵ : L.NeBot
α : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : CommMonoid α
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : DecidableEq β
f : β → α
a : α
hf : HasProd f a L
b : β
a' : α
hf' : HasProd (fun n ↦ if n = b then 1 else f n) a' L
⊢ HasProd (update f b 1) a' L
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

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

Tactic:
by
  refine (mul_one a).symm.trans (hf.update' b 1 ?_)
  convert! hf'
  apply update_apply

Goal state after: