mathlib-initiative/mathlib-tactics huggingface dataset:
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 ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun i ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
n : ℕ
⊢ ∏ k ∈ range n, v (k + 1) = (v 0)⁻¹ * w n

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝¹ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝ : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
f : α → β
g : pkg.space → pkg'.space
hg : UniformContinuous g
h : ∀ (a : α), pkg'.coe (f a) = g (pkg.coe a)
⊢ ∀ (a : α), pkg.map pkg' f (pkg.coe a) = g (pkg.coe a)

Tactic:
by

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

Goal state before:
pp: β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
⊢ Tendsto f atTop (𝓝 0) ↔ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n < ε

Tactic:
by

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

Goal state before:
pp: h : ∞ ≠ ∞ ∨ ∞ ≠ ∞
⊢ Tendsto (fun p ↦ p.1 - p.2) (𝓝 (∞, ∞)) (𝓝 (∞ - ∞))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝⁴ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝³ : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
γ : Type uγ
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace γ
inst✝ : T0Space γ
f : β → γ
g : α → β
hf : UniformContinuous f
hg : UniformContinuous g
a : α
⊢ (pkg'.extend f ∘ pkg.map pkg' g) (pkg.coe a) = pkg.extend (f ∘ g) (pkg.coe a)

Tactic:
by

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

Goal state before:
pp: b : ℝ≥0
x✝ : ∞ ≠ ∞ ∨ ↑b ≠ ∞
⊢ Tendsto (fun p ↦ p.1 - p.2) (𝓝 (∞, ↑b)) (𝓝 (∞ - ↑b))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝² : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝¹ : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
f : α → β
γ : Type uγ
inst✝ : UniformSpace γ
pkg'' : AbstractCompletion.{vγ, uγ} γ
e : α ≃ᵤ β
⊢ pkg'.map pkg ⇑e.symm ∘ pkg.map pkg' ⇑e = id

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝² : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝¹ : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
f : α → β
γ : Type uγ
inst✝ : UniformSpace γ
pkg'' : AbstractCompletion.{vγ, uγ} γ
e : α ≃ᵤ β
⊢ pkg.map pkg' ⇑e ∘ pkg'.map pkg ⇑e.symm = id

Tactic:
by

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

Goal state before:
pp: a : ℝ≥0
x✝ : ↑a ≠ ∞ ∨ ∞ ≠ ∞
⊢ Tendsto (fun p ↦ p.1 - p.2) (𝓝 (↑a, ∞)) (𝓝 (↑a - ∞))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
⊢ pkg.compare pkg' ∘ pkg'.compare pkg = id

Tactic:
by

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

Goal state before:
pp: a b : ℝ≥0
x✝ : ↑a ≠ ∞ ∨ ↑b ≠ ∞
⊢ Tendsto (fun p ↦ p.1 - p.2) (𝓝 (↑a, ↑b)) (𝓝 (↑a - ↑b))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝² : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
γ : Type uγ
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
f : α → γ
cont_f : Continuous[inst✝².toTopologicalSpace, inst✝¹] f
h : ∀ (a : pkg.space), Tendsto f (comap pkg.coe (𝓝 a)) (𝓝 (⋯.extend f a))
x : α
⊢ (⋯.extend f ∘ pkg'.compare pkg) (pkg'.coe x) = f x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝² : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
γ : Type uγ
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
f : α → γ
cont_f : Continuous[inst✝².toTopologicalSpace, inst✝¹] f
⊢ (∀ (a : pkg.space), Tendsto f (comap pkg.coe (𝓝 a)) (𝓝 (⋯.extend f a))) → ⋯.extend f ∘ pkg'.compare pkg = ⋯.extend f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝³ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝² : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
γ : Type uγ
inst✝¹ : UniformSpace γ
f : α → β → γ
inst✝ : CompleteSpace γ
⊢ UniformContinuous₂ (pkg.extend₂ pkg' f)

Tactic:
by

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

Goal state before:
pp: a b✝ : ℝ≥0∞
ha : a ≠ 0 ∨ b✝ ≠ ∞
hb✝ : b✝ ≠ 0 ∨ a ≠ ∞
b : ℝ≥0∞
hb : b ≠ 0
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 (∞, b)) (𝓝 ∞)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
f : SetRel α α → Set (CauchyFilter α × CauchyFilter α) := fun s ↦ {p | s ∈ ↑p.2 ×ˢ ↑p.1}
⊢ map Prod.swap ((𝓤 α).lift' gen) = (𝓤 α).lift' f

Tactic:
by

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

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ 0 ∨ b ≠ ∞
hb : b ≠ 0 ∨ a ≠ ∞
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f : Filter α
m : α → ℝ≥0∞
a b : ℝ≥0∞
hm : Tendsto m f (𝓝 b)
hb : b ≠ 0 ∨ a ≠ ∞
this : a = 0
⊢ Tendsto (fun b ↦ a * m b) f (𝓝 (a * b))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f : Filter α
m : α → ℝ≥0∞
a b : ℝ≥0∞
hm : Tendsto m f (𝓝 a)
ha : a ≠ 0 ∨ b ≠ ∞
⊢ Tendsto (fun x ↦ m x * b) f (𝓝 (a * b))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
f : SetRel α α → Set (CauchyFilter α × CauchyFilter α) := fun s ↦ {p | s ∈ ↑p.2 ×ˢ ↑p.1}
h₁ : map Prod.swap ((𝓤 α).lift' gen) = (𝓤 α).lift' f
⊢ ((𝓤 α).lift fun s ↦ (𝓟 ∘ f) (Prod.swap ⁻¹' s)) ≤ (𝓤 α).lift' gen

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
⊢ map Prod.swap ((𝓤 α).lift' gen) ≤ (𝓤 α).lift' gen

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
⊢ (((𝓤 α).lift' gen).lift' fun s ↦ s ○ s) = (𝓤 α).lift' fun s ↦ gen s ○ gen s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
⊢ ((𝓤 α).lift' fun s ↦ gen (s ○ s)) = ((𝓤 α).lift' fun s ↦ s ○ s).lift' gen

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ Tendsto Prod.swap ((𝓤 α).lift' gen) ((𝓤 α).lift' gen)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ (((𝓤 α).lift' gen).lift' fun s ↦ s ○ s) ≤ (𝓤 α).lift' gen

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
s : Set (CauchyFilter α × CauchyFilter α)
⊢ s ∈ 𝓤 (CauchyFilter α) ↔ ∃ t ∈ 𝓤 α, ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
s : SetRel α α
x✝ : α × α
a₁ a₂ : α
⊢ (a₁, a₂) ∈ ((preimage fun x ↦ (pureCauchy x.1, pureCauchy x.2)) ∘ gen) s ↔ (a₁, a₂) ∈ id s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
s : Finset ι
h : ∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))
h' : ∀ i ∈ s, a i ≠ ∞
⊢ Tendsto (fun b ↦ ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a c))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
this : (preimage fun x ↦ (pureCauchy x.1, pureCauchy x.2)) ∘ gen = id
⊢ (𝓤 α).lift' ((preimage fun x ↦ (pureCauchy x.1, pureCauchy x.2)) ∘ gen) = 𝓤 α

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
f : CauchyFilter α
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ 𝓤 (CauchyFilter α)
t'' : Set (α × α)
ht''₁ : t'' ∈ 𝓤 α
ht''₂ : gen t'' ⊆ s
t' : Set (α × α)
ht'₁ : t' ∈ 𝓤 α
ht'₂ : t' ○ t' ⊆ t''
this✝ : t' ∈ ↑f ×ˢ ↑f
t : Set α
ht : t ∈ ↑f
h : t ×ˢ t ⊆ t'
x : α
hx : x ∈ t
this : t'' ∈ ↑f ×ˢ pure x
⊢ (f, pureCauchy x) ∈ gen t''

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ Continuous fun a ↦ a ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
f : CauchyFilter α
⊢ f ∈ closure (range pureCauchy)

Tactic:
by

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

Goal state before:
pp: ⊢ ContinuousOn (fun p ↦ p.1 - p.2) {p | p ≠ (∞, ∞)}

Tactic:
by

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

Goal state before:
pp: a : ℝ≥0∞
a_ne_top : a ≠ ∞
⊢ Continuous fun x ↦ a - x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
⊢ Nonempty (CauchyFilter α) ↔ Nonempty α

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : Filter α
hf : Cauchy f
f' : CauchyFilter α := ⟨f, hf⟩
this : map pureCauchy f ≤ (𝓤 (CauchyFilter α)).lift' (preimage (Prod.mk f'))
⊢ map pureCauchy f ≤ 𝓝 f'

Tactic:
by

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

Goal state before:
pp: a : ℝ≥0∞
⊢ ContinuousOn (fun x ↦ (a, x)) {x | x ≠ ∞}

Tactic:
by

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

Goal state before:
pp: a : ℝ≥0∞
⊢ ContinuousOn (fun x ↦ a - x) {x | x ≠ ∞}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝² : UniformSpace α
β : Type v
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
hf : UniformContinuous f
a : α
⊢ extend f (pureCauchy a) = f a

Tactic:
by

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
⊢ ∃ 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:
by

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

Goal state before:
pp: a : ℝ≥0∞
a_infty : ¬a = ∞
⊢ Continuous fun x ↦ (x, a)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝² : UniformSpace α
β : Type v
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace β
f : α → β
hf : ¬UniformContinuous f
a _b : CauchyFilter α
⊢ f ⋯.some = f ⋯.some

Tactic:
by

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

Goal state before:
pp: a : ℝ≥0∞
⊢ Continuous fun x ↦ x - a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝² : UniformSpace α
β : Type v
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace β
f : α → β
⊢ UniformContinuous (extend f)

Tactic:
by

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

Goal state before:
pp: x y : ℝ≥0∞
h : ∀ a < 1, a * x ≤ y
⊢ x ≤ y

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ Continuous fun x ↦ x ^ Int.negSucc n

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
f g : CauchyFilter α
a b : α
ha : ↑f ≤ 𝓝 a
hb : ↑g ≤ 𝓝 b
⊢ Inseparable a b ↔ Inseparable f g

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : T0Space α
f g : CauchyFilter α
⊢ (↑f).lim = (↑g).lim ↔ Inseparable f g

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f : Filter α
ma mb : α → ℝ≥0∞
a b : ℝ≥0∞
hma : Tendsto ma f (𝓝 a)
ha : a ≠ 0 ∨ b ≠ 0
hmb : Tendsto mb f (𝓝 b)
hb : b ≠ ∞ ∨ a ≠ ∞
⊢ Tendsto (fun a ↦ ma a / mb a) f (𝓝 (a / b))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α✝ : Type u_1
inst✝³ : UniformSpace α✝
β : Type u_2
inst✝² : UniformSpace β
γ : Type u_3
inst✝¹ : UniformSpace γ
α : Type u_4
inst✝ : UniformSpace α
⊢ UniformSpace (Completion α)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α✝ : Type u_1
inst✝³ : UniformSpace α✝
β : Type u_2
inst✝² : UniformSpace β
γ : Type u_3
inst✝¹ : UniformSpace γ
α : Type u_4
inst✝ : UniformSpace α
⊢ CompleteSpace (Completion α)

Tactic:
by

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

Goal state before:
pp: E : Type u_4
F : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
j : E →* F
b : F
hb : b ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑j.range
f : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < f n
v : ℕ → F
sum_v : Tendsto (fun n ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 b)
hv₀ : ‖(v 0)⁻¹ * b‖ < f 0
hv_pos : ∀ (n : ℕ), 0 < n → ‖v n‖ < f n
g : ℕ → E
hg : ∀ (n : ℕ), j (g n) = v n
⊢ Tendsto (fun n ↦ ∏ i ∈ range (n + 1), j (g i)) atTop (𝓝 b)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α✝ : Type u_1
inst✝³ : UniformSpace α✝
β : Type u_2
inst✝² : UniformSpace β
γ : Type u_3
inst✝¹ : UniformSpace γ
α : Type u_4
inst✝ : UniformSpace α
⊢ T0Space (Completion α)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f : Filter α
m : α → ℝ≥0∞
a b : ℝ≥0∞
hm : Tendsto m f (𝓝 b)
hb : b ≠ ∞ ∨ a ≠ ∞
⊢ Tendsto (fun b ↦ a / m b) f (𝓝 (a / b))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u_1
inst✝⁴ : UniformSpace α
β : Type u_2
inst✝³ : UniformSpace β
γ : Type u_3
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace γ
inst✝ : T0Space γ
f : β → γ
g : α → β
hf : UniformContinuous f
hg : UniformContinuous g
⊢ ∀ (a : α), (Completion.extension f ∘ Completion.map g) ↑a = Completion.extension (f ∘ g) ↑a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f : Filter α
m : α → ℝ≥0∞
a b : ℝ≥0∞
hm : Tendsto m f (𝓝 a)
ha : a ≠ 0 ∨ b ≠ 0
⊢ Tendsto (fun x ↦ m x / b) f (𝓝 (a / b))

Tactic:
by

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

Goal state before:
pp: s : Set ℝ≥0∞
s_count : s.Countable
s_dense : Dense s
hs : (∀ (x : ℝ≥0∞), IsBot x → x ∉ s) ∧ ∀ (x : ℝ≥0∞), IsTop x → x ∉ s
h : 0 ∈ s
⊢ IsBot 0

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α✝ : Type u_1
inst✝³ : UniformSpace α✝
β : Type u_2
inst✝² : UniformSpace β
γ : Type u_3
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
⊢ Completion (SeparationQuotient α) ≃ Completion α

Tactic:
by

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

Goal state before:
pp: s : Set ℝ≥0∞
s_count : s.Countable
s_dense : Dense s
hs : (∀ (x : ℝ≥0∞), IsBot x → x ∉ s) ∧ ∀ (x : ℝ≥0∞), IsTop x → x ∉ s
h : ∞ ∈ s
⊢ IsTop ∞

Tactic:
by

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

Goal state before:
pp: E : Type u_4
F : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
j : E →* F
b : F
hb : b ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑j.range
f : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < f n
v : ℕ → F
sum_v : Tendsto (fun n ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 b)
hv₀ : ‖(v 0)⁻¹ * b‖ < f 0
hv_pos : ∀ (n : ℕ), 0 < n → ‖v n‖ < f n
g : ℕ → E
hg : ∀ (n : ℕ), j (g n) = v n
⊢ ‖(j (g 0))⁻¹ * b‖ < f 0

Tactic:
by

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

Goal state before:
pp: ⊢ ∃ s, s.Countable ∧ Dense s ∧ 0 ∉ s ∧ ∞ ∉ s

Tactic:
by

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

Goal state before:
pp: ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : liminf (fun n ↦ ↑(Real.nnabs (x n))) l ≠ ∞
h : ∀ (R : ℝ), ∀ᶠ (x_1 : ι) in l, R ≤ x x_1
r : ℝ≥0
⊢ IsCobounded (fun x1 x2 ↦ x1 ≥ x2) (map (fun n ↦ ↑(Real.nnabs (x n))) l)

Tactic:
by

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

Goal state before:
pp: ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : liminf (fun n ↦ ↑(Real.nnabs (x n))) l ≠ ∞
⊢ ∃ R, ∃ᶠ (n : ι) in l, x n < R

Tactic:
by

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

Goal state before:
pp: ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : liminf (fun n ↦ ↑(Real.nnabs (x n))) l ≠ ∞
h : ∀ (R : ℝ), ∀ᶠ (x_1 : ι) in l, x x_1 ≤ R
r : ℝ≥0
⊢ IsCobounded (fun x1 x2 ↦ x1 ≥ x2) (map (fun n ↦ ↑(Real.nnabs (x n))) l)

Tactic:
by

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

Goal state before:
pp: ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : liminf (fun n ↦ ↑(Real.nnabs (x n))) l ≠ ∞
⊢ ∃ R, ∃ᶠ (n : ι) in l, R < x n

Tactic:
by

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

Goal state before:
pp: E : Type u_4
F : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
j : E →* F
b : F
hb : b ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑j.range
f : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < f n
v : ℕ → F
sum_v : Tendsto (fun n ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 b)
hv₀ : ‖(v 0)⁻¹ * b‖ < f 0
hv_pos : ∀ (n : ℕ), 0 < n → ‖v n‖ < f n
g : ℕ → E
hg : ∀ (n : ℕ), j (g n) = v n
n : ℕ
hn : 0 < n
⊢ ‖j (g n)‖ < f n

Tactic:
by

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

Goal state before:
pp: E : Type u_4
F : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
j : E →* F
b : F
hb : b ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑j.range
f : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < f n
⊢ ∃ a,
    Tendsto (fun n ↦ ∏ i ∈ range (n + 1), j (a i)) atTop (𝓝 b) ∧
      ‖(j (a 0))⁻¹ * b‖ < f 0 ∧ ∀ (n : ℕ), 0 < n → ‖j (a n)‖ < f n

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: E : Type u_4
inst✝ : NormedGroup E
⊢ comap norm (𝓝[>] 0) = 𝓝[≠] 1

Tactic:
simp [nhdsWithin, comap_norm_nhds_one, Set.preimage, Set.compl_def]

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

Goal state before:
pp: E : Type u_4
inst✝ : NormedGroup E
⊢ comap norm (𝓝[>] 0) = 𝓝[≠] 1

Tactic:
by

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:
by

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

Goal state before:
pp: ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i ↦ ↑(Real.nnabs (x i))) l ≠ ∞
hbdd : ¬IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun i ↦ |x i|
⊢ ∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i

Tactic:
by

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

Goal state before:
pp: ι : Type u_4
fi : Filter ι
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
x : ℝ≥0∞
hx : x ≠ ∞
⊢ Tendsto (fun n ↦ (f n).toReal) fi (𝓝 x.toReal) ↔ Tendsto f fi (𝓝 x)

Tactic:
by

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

Goal state before:
pp: ι : Type u_4
fi : Filter ι
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
⊢ Tendsto (fun n ↦ (f n).toReal) fi (𝓝 0) ↔ Tendsto f fi (𝓝 0)

Tactic:
by

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

Goal state before:
pp: β : Type u_2
inst✝ : EMetricSpace β
a : β
r : ℝ≥0∞
x y : ↑(eball a r)
⊢ edist a ↑x + edist a ↑y < r + r

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : PseudoEMetricSpace α
l : Filter β
f : β → α
y : α
⊢ Tendsto f l (𝓝 y) ↔ Tendsto (fun x ↦ edist (f x) y) l (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x : α
hx : x ≤ a
⊢ projIcc a b h x = ⟨a, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x : α
hx : b ≤ x
⊢ projIcc a b h x = ⟨b, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a x : α
⊢ projIci a x = ⟨a, ⋯⟩ ↔ x ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
b x : α
⊢ projIic b x = ⟨b, ⋯⟩ ↔ b ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b x : α
h : a < b
⊢ projIcc a b ⋯ x = ⟨a, ⋯⟩ ↔ x ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b x : α
h : a < b
⊢ projIcc a b ⋯ x = ⟨b, ⋯⟩ ↔ b ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a x : α
hx : x ∈ Ici a
⊢ projIci a x = ⟨x, hx⟩

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
b x : α
hx : x ∈ Iic b
⊢ projIic b x = ⟨x, hx⟩

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x : α
hx : x ∈ Icc a b
⊢ projIcc a b h x = ⟨x, hx⟩

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
x : ↑(Ici a)
⊢ projIci a ↑x = x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
b : α
x : ↑(Iic b)
⊢ projIic b ↑x = x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x : ↑(Icc a b)
⊢ projIcc a b h ↑x = x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a x : α
hx : x ∈ Ici a
y : α
hy : y ∈ Ici a
hxy : x < y
⊢ projIci a x < projIci a y

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
b x : α
hx : x ∈ Iic b
y : α
hy : y ∈ Iic b
hxy : x < y
⊢ projIic b x < projIic b y

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x : α
hx : x ∈ Icc a b
y : α
hy : y ∈ Icc a b
hxy : x < y
⊢ projIcc a b h x < projIcc a b h y

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a : α
f : ↑(Ici a) → β
⊢ range (IciExtend f) = range f

Tactic:
by

Goal state after: