awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
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 : E × E | ‖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
refine_1 : Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 a)
refine_2 : ∀ (n : ℕ), v n ∈ s
refine_3 : ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
⊢ ∃ (v : ℕ → E),
    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:
refine ⟨v, ?_, ?_, hn₀ _ (n₀.le_add_left _), ?_⟩
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
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 : E × E | ‖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
apply : ∀ (n : ℕ), w n = ∏ i ∈ range (n + 1), v i
⊢ Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 a)

Tactic:
apply hw.congr (fun n ↦ ?_)

Premises used: Filter.Tendsto.congr
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
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 : E × E | ‖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 : ℕ
rw : w n = (∏ k ∈ range n, v (k + 1)) * v 0
⊢ w n = ∏ i ∈ range (n + 1), v i

Tactic:
rw [Finset.prod_range_succ']

Premises used: Finset.prod_range_succ'
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
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 : E × E | ‖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 : ℕ
⊢ (v 0)⁻¹ * w 0 = 1

Tactic:
simp [v]
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
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 : E × E | ‖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 : ℕ
apply : ∀ (k : ℕ) (hk : k < n), (v 0)⁻¹ * w (k + 1) = (v 0)⁻¹ * w k * v (k + 1)
⊢ ∏ k ∈ range n, v (k + 1) = (v 0)⁻¹ * w n

Tactic:
apply prod_range_induction _ _ (by simp [v]) _ (fun k hk ↦ ?_)

Premises used: Finset.prod_range_induction
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
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 : E × E | ‖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 : ℕ
hk : k < n
simp : (w 0)⁻¹ * w (k + 1) = (w 0)⁻¹ * w k * ((w k)⁻¹ * w (k + 1))
⊢ (v 0)⁻¹ * w (k + 1) = (v 0)⁻¹ * w k * v (k + 1)

Tactic:
simp only [↓reduceIte, Nat.add_eq_zero_iff, one_ne_zero, and_false, add_tsub_cancel_right, v]

Premises used: reduceIte, and_false, add_tsub_cancel_right, one_ne_zero, Nat.add_eq_zero_iff
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
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 : E × E | ‖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 : ℕ
hk : k < n
⊢ (w 0)⁻¹ * w (k + 1) = (w 0)⁻¹ * w k * ((w k)⁻¹ * w (k + 1))

Tactic:
group
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
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 : E × E | ‖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:
have : ∏ k ∈ range n, v (k + 1) = (v 0)⁻¹ * w n := by
      apply prod_range_induction _ _ (by simp [v]) _ (fun k hk ↦ ?_)
      simp only [↓reduceIte, Nat.add_eq_zero_iff, one_ne_zero, and_false, add_tsub_cancel_right, v]
      group
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
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 : E × E | ‖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 : ℕ
this : ∏ k ∈ range n, v (k + 1) = (v 0)⁻¹ * w n
⊢ w n = (∏ k ∈ range n, v (k + 1)) * v 0

Tactic:
simp [this]
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
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 : E × E | ‖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
refine_2 : w 0 ∈ s
⊢ v 0 ∈ s

Tactic:
change w 0 ∈ s

Premises used: OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
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 : E × E | ‖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
⊢ w 0 ∈ s

Tactic:
apply u_in
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
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 : E × E | ‖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 : ℕ
⊢ v (n + 1) ∈ s

Tactic:
s.mul_mem (s.inv_mem (u_in _)) (u_in _)

Premises used: Set.Mem, Subgroup.inv_mem, Subgroup.mul_mem, ite
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
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 : E × E | ‖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 : ℕ
⊢ v (n + 1) ∈ s

Tactic:
exact s.mul_mem (s.inv_mem (u_in _)) (u_in _)

Premises used: Subgroup.inv_mem, Subgroup.mul_mem
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
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 : E × E | ‖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
l : ℕ
hl : 0 < l
⊢ ∃ (k : ℕ), l = k + 1

Tactic:
Nat.exists_eq_succ_of_ne_zero hl.ne'

Premises used: LT.lt.ne', Nat.exists_eq_succ_of_ne_zero
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
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 : E × E | ‖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
l : ℕ
hl : 0 < l
refine_3 : ∀ (k : ℕ) (hl : 0 < k + 1), ‖v (k + 1)‖ < b (k + 1)
⊢ ‖v l‖ < b l

Tactic:
obtain ⟨k, rfl⟩ : ∃ k, l = k + 1 := Nat.exists_eq_succ_of_ne_zero hl.ne'

Premises used: LT.lt.ne', Nat.exists_eq_succ_of_ne_zero, rfl
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
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 : E × E | ‖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
k : ℕ
hl : 0 < k + 1
refine_3 : ‖(v (k + 1))⁻¹‖ < b (k + 1)
⊢ ‖v (k + 1)‖ < b (k + 1)

Tactic:
rw [← norm_inv']

Premises used: norm_inv'
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
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 : E × E | ‖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
k : ℕ
hl : 0 < k + 1
refine_3 : ‖(w (k + 1))⁻¹ * w k‖ < b (k + 1)
⊢ ‖(v (k + 1))⁻¹‖ < b (k + 1)

Tactic:
simp only [Nat.add_eq_zero_iff, one_ne_zero, and_false, ↓reduceIte, add_tsub_cancel_right,
      mul_inv_rev, inv_inv, v]

Premises used: inv_inv, reduceIte, mul_inv_rev, and_false, add_tsub_cancel_right, one_ne_zero, Nat.add_eq_zero_iff
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
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 : E × E | ‖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
k : ℕ
hl : 0 < k + 1
⊢ ‖(w (k + 1))⁻¹ * w k‖ < b (k + 1)

Tactic:
apply hφ
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
F : Type u_5
inst : SeminormedCommGroup E
inst_1 : SeminormedCommGroup F
j : E →* F
b : F
hb : b ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑j.range : Set F)
f : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < f n
obtain :
  ∀ (v : ℕ → F) (sum_v : Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 b)) (v_in : ∀ (n : ℕ), v n ∈ j.range)
    (hv₀ : ‖(v 0)⁻¹ * b‖ < f 0) (hv_pos : ∀ (n : ℕ), 0 < n → ‖v n‖ < f n),
    ∃ (a : ℕ → E),
      Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), (j : (a : E) → F) (a i)) atTop (𝓝 b) ∧
        ‖HMul.hMul (α := F) (((j : (a : E) → F) (a 0))⁻¹ : F) b‖ < f 0 ∧
          ∀ (n : ℕ), 0 < n → norm.{u_5} (E := F) ((j : (a : E) → F) (a n) : F) < f n
⊢ ∃ (a : ℕ → E),
    Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), (j : (a : E) → F) (a i)) atTop (𝓝 b) ∧
      ‖HMul.hMul (α := F) (((j : (a : E) → F) (a 0))⁻¹ : F) b‖ < f 0 ∧
        ∀ (n : ℕ), 0 < n → norm.{u_5} (E := F) ((j : (a : E) → F) (a n) : F) < f n

Tactic:
obtain ⟨v, sum_v, v_in, hv₀, hv_pos⟩ := controlled_prod_of_mem_closure hb b_pos

Premises used: controlled_prod_of_mem_closure
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
F : Type u_5
inst : SeminormedCommGroup E
inst_1 : SeminormedCommGroup F
j : E →* F
b : F
hb : b ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑j.range : Set F)
f : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < f n
v : ℕ → F
sum_v : Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 b)
v_in : ∀ (n : ℕ), v n ∈ j.range
hv₀ : ‖(v 0)⁻¹ * b‖ < f 0
hv_pos : ∀ (n : ℕ), 0 < n → ‖v n‖ < f n
choose :
  ∀ (g : (n : ℕ) → E) (hg : ∀ (n : ℕ), (j : (a : E) → F) (g n) = v n),
    ∃ (a : ℕ → E),
      Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), (j : (a : E) → F) (a i)) atTop (𝓝 b) ∧
        ‖HMul.hMul (α := F) (((j : (a : E) → F) (a 0))⁻¹ : F) b‖ < f 0 ∧
          ∀ (n : ℕ), 0 < n → norm.{u_5} (E := F) ((j : (a : E) → F) (a n) : F) < f n
⊢ ∃ (a : ℕ → E),
    Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), (j : (a : E) → F) (a i)) atTop (𝓝 b) ∧
      ‖HMul.hMul (α := F) (((j : (a : E) → F) (a 0))⁻¹ : F) b‖ < f 0 ∧
        ∀ (n : ℕ), 0 < n → norm.{u_5} (E := F) ((j : (a : E) → F) (a n) : F) < f n

Tactic:
choose g hg using v_in
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
F : Type u_5
inst : SeminormedCommGroup E
inst_1 : SeminormedCommGroup F
j : E →* F
b : F
hb : b ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑j.range : Set F)
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 : (n : ℕ) → E
hg : ∀ (n : ℕ), (j : (a : E) → F) (g n) = v n
⊢ Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), (j : (a : E) → F) (g i)) atTop (𝓝 b)

Tactic:
simpa [← hg] using sum_v
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
F : Type u_5
inst : SeminormedCommGroup E
inst_1 : SeminormedCommGroup F
j : E →* F
b : F
hb : b ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑j.range : Set F)
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 : (n : ℕ) → E
hg : ∀ (n : ℕ), (j : (a : E) → F) (g n) = v n
⊢ ‖HMul.hMul (α := F) (((j : (a : E) → F) (g 0))⁻¹ : F) b‖ < f 0

Tactic:
simpa [hg 0] using hv₀

Premises used: OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
F : Type u_5
inst : SeminormedCommGroup E
inst_1 : SeminormedCommGroup F
j : E →* F
b : F
hb : b ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑j.range : Set F)
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 : (n : ℕ) → E
hg : ∀ (n : ℕ), (j : (a : E) → F) (g n) = v n
n : ℕ
hn : 0 < n
⊢ norm.{u_5} (E := F) ((j : (a : E) → F) (g n) : F) < f n

Tactic:
simpa [hg] using hv_pos n hn
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
F : Type u_5
inst : SeminormedCommGroup E
inst_1 : SeminormedCommGroup F
j : E →* F
b : F
hb : b ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑j.range : Set F)
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 : (n : ℕ) → E
hg : ∀ (n : ℕ), (j : (a : E) → F) (g n) = v n
⊢ ∃ (a : ℕ → E),
    Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), (j : (a : E) → F) (a i)) atTop (𝓝 b) ∧
      ‖HMul.hMul (α := F) (((j : (a : E) → F) (a 0))⁻¹ : F) b‖ < f 0 ∧
        ∀ (n : ℕ), 0 < n → norm.{u_5} (E := F) ((j : (a : E) → F) (a n) : F) < f n

Tactic:
exact
    ⟨g, by simpa [← hg] using sum_v, by simpa [hg 0] using hv₀,
      fun n hn => by simpa [hg] using hv_pos n hn⟩
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : NormedGroup E
⊢ Tendsto (α := E) norm (𝓝[≠] 1) (𝓝[>] 0)

Tactic:
tendsto_norm_one.inf <| tendsto_principal_principal.2 fun _ hx ↦ norm_pos_iff'.2 hx

Premises used: Iff.mpr, Set.Mem, nhdsWithin, norm_pos_iff', setOf, tendsto_norm_one, Filter.Tendsto.inf, Filter.tendsto_principal_principal
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : NormedGroup E
a : E
apply : Tendsto (β := ℝ) (fun (a_1 : E) ↦ ‖a_1⁻¹ * a‖) (𝓟 {a}ᶜ) (𝓟 (Set.Ioi 0))
⊢ Tendsto (β := ℝ) (fun (x : E) ↦ ‖x⁻¹ * a‖) (𝓝[≠] a) (𝓝[>] 0)

Tactic:
apply (tendsto_norm_inv_mul_self a).inf

Premises used: tendsto_norm_inv_mul_self, Filter.Tendsto.inf
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : NormedGroup E
a : E
apply : ∀ (_x : E) (hx : Membership.mem (γ := Set E) {a}ᶜ _x), _x⁻¹ * a ≠ 1
⊢ Tendsto (β := ℝ) (fun (a_1 : E) ↦ ‖a_1⁻¹ * a‖) (𝓟 {a}ᶜ) (𝓟 (Set.Ioi 0))

Tactic:
apply tendsto_principal_principal.2 (fun _x hx => norm_pos_iff'.2 ?_)

Premises used: Iff.mpr, norm_pos_iff', Filter.tendsto_principal_principal
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : NormedGroup E
a _x : E
hx : Membership.mem (γ := Set E) {a}ᶜ _x
⊢ _x⁻¹ * a ≠ 1

Tactic:
simpa [inv_mul_eq_one] using hx

Premises used: inv_mul_eq_one
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : NormedGroup E
⊢ Eq (α := Filter E) (comap norm (𝓝[>] 0)) (𝓝[≠] 1)

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

Premises used: Set.compl_def, nhdsWithin, comap_norm_nhds_one, Set.preimage
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_7
inst : NormedCommGroup E
a : E
simp_rw : Tendsto (β := ℝ) (fun (x : E) ↦ ‖x⁻¹ * a‖) (𝓝[≠] a) (𝓝[>] 0)
⊢ Tendsto (β := ℝ) (fun (x : E) ↦ ‖x / a‖) (𝓝[≠] a) (𝓝[>] 0)

Tactic:
simp_rw [← norm_inv_mul]

Premises used: norm_inv_mul
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_7
inst : NormedCommGroup E
a : E
⊢ Tendsto (β := ℝ) (fun (x : E) ↦ ‖x⁻¹ * a‖) (𝓝[≠] a) (𝓝[>] 0)

Tactic:
tendsto_norm_inv_mul_self_nhdsNE a

Premises used: tendsto_norm_inv_mul_self_nhdsNE
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_7
inst : NormedCommGroup E
a : E
⊢ Tendsto (β := ℝ) (fun (x : E) ↦ ‖x⁻¹ * a‖) (𝓝[≠] a) (𝓝[>] 0)

Tactic:
exact tendsto_norm_inv_mul_self_nhdsNE a

Premises used: tendsto_norm_inv_mul_self_nhdsNE
-- Module: Mathlib.Analysis.Normed.Group.ControlledClosure
Goal:
G : Type u_1
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
H : Type u_2
inst_2 : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : AddSubgroup H
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : f.SurjectiveOnWith K C
h : H
h_in : h ∈ K.topologicalClosure
pos : ∀ (hyp_h : h = 0), ∃ (g : G), (f : (a : G) → H) g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖
neg : ∀ (hyp_h : ¬h = 0), ∃ (g : G), (f : (a : G) → H) g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖
⊢ ∃ (g : G), (f : (a : G) → H) g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖

Tactic:
by_cases hyp_h : h = 0
-- Module: Mathlib.Analysis.Normed.Group.ControlledClosure
Goal:
G : Type u_1
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
H : Type u_2
inst_2 : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : AddSubgroup H
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : f.SurjectiveOnWith K C
h : H
h_in : h ∈ K.topologicalClosure
hyp_h : h = 0
pos : ∃ (g : G), Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) g : H) (0 : H) ∧ ‖g‖ ≤ (C + ε) * norm.{u_2} (E := H) 0
⊢ ∃ (g : G), (f : (a : G) → H) g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖

Tactic:
rw [hyp_h]