awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.CocompactMap (goal)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), ∃ (r : ℝ), ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
s : Set F
hs : s ∈ cocompact F
ε : ℝ
hε : (closedBall 0 ε)ᶜ ⊆ s
r : ℝ
hr : ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
x : E
hx : r < ‖x‖
⊢ x ∈ f ⁻¹' s
have h₁ : Membership.mem (γ := Set F) (closedBall 0 ε)ᶜ (f x)
Tactic: apply hε
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Completeness (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
⊢ ∃ (f : ℕ → ℕ), StrictMono f ∧ Summable (α := ℝ) fun (i : ℕ) ↦ dist (u (f (i + 1))) (u (f i))
have obtain : ∀ (f : ℕ → ℕ) (hf₁ : StrictMono f) (hf₂ : ∀ (n m : ℕ), m ≥ f n → dist (u m) (u (f n)) < (1 / 2) ^ n),
  ∃ (f : ℕ → ℕ), StrictMono f ∧ Summable (α := ℝ) fun (i : ℕ) ↦ dist (u (f (i + 1))) (u (f i))
Tactic: obtain ⟨f, hf₁, hf₂⟩ := Metric.exists_subseq_bounded_of_cauchySeq u hu
    (fun n => (1 / (2 : ℝ)) ^ n) (fun n => by positivity)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Completeness (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : ∀ (n m : ℕ), m ≥ f n → dist (u m) (u (f n)) < (1 / 2) ^ n
⊢ ∃ (f : ℕ → ℕ), StrictMono f ∧ Summable (α := ℝ) fun (i : ℕ) ↦ dist (u (f (i + 1))) (u (f i))
have refine : Summable (α := ℝ) fun (i : ℕ) ↦ dist (u (f (i + 1))) (u (f i))
Tactic: refine ⟨f, hf₁, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Completeness (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : ∀ (n m : ℕ), m ≥ f n → dist (u m) (u (f n)) < (1 / 2) ^ n
⊢ Summable (α := ℝ) fun (i : ℕ) ↦ dist (u (f (i + 1))) (u (f i))
have refine : ∀ (b : ℕ), dist (u (f (b + 1))) (u (f b)) ≤ (1 / 2) ^ b
Tactic: refine Summable.of_nonneg_of_le (fun n => by positivity) ?_ summable_geometric_two
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Completeness (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
h :
  ∀ (u : ℕ → E),
    (Summable (α := ℝ) fun (x : ℕ) ↦ ‖u x‖) → ∃ (a : E), Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, u i) atTop (𝓝 a)
⊢ CompleteSpace E
have a : ∀ (u : ℕ → E), CauchySeq u → ∃ (a : E), Tendsto u atTop (𝓝 a)
Tactic: apply Metric.complete_of_cauchySeq_tendsto
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Completeness (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
h :
  ∀ (u : ℕ → E),
    (Summable (α := ℝ) fun (x : ℕ) ↦ ‖u x‖) → ∃ (a : E), Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, u i) atTop (𝓝 a)
u : ℕ → E
hu : CauchySeq u
⊢ ∃ (a : E), Tendsto u atTop (𝓝 a)
have a : ∀ (f : ℕ → ℕ) (hf₁ : StrictMono f) (hf₂ : Summable (α := ℝ) fun (i : ℕ) ↦ dist (u (f (i + 1))) (u (f i))),
  ∃ (a : E), Tendsto u atTop (𝓝 a)
Tactic: obtain ⟨f, hf₁, hf₂⟩ := Metric.exists_subseq_summable_dist_of_cauchySeq u hu
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Completeness (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
h :
  ∀ (u : ℕ → E),
    (Summable (α := ℝ) fun (x : ℕ) ↦ ‖u x‖) → ∃ (a : E), Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, u i) atTop (𝓝 a)
u : ℕ → E
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : Summable (α := ℝ) fun (i : ℕ) ↦ dist (u (f (i + 1))) (u (f i))
⊢ ∃ (a : E), Tendsto u atTop (𝓝 a)
have hf₃ : Summable (α := ℝ) fun (i : ℕ) ↦ ‖u (f (i + 1)) - u (f i)‖
Tactic: simp only [dist_eq_norm] at hf₂
Cleared hypotheses: hf₂
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Completeness (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
h :
  ∀ (u : ℕ → E),
    (Summable (α := ℝ) fun (x : ℕ) ↦ ‖u x‖) → ∃ (a : E), Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, u i) atTop (𝓝 a)
u : ℕ → E
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : Summable (α := ℝ) fun (i : ℕ) ↦ ‖u (f (i + 1)) - u (f i)‖
v : (n : ℕ) → E := fun (n : ℕ) ↦ u (f (n + 1)) - u (f n)
⊢ Eq.{u_1 + 1} (α := (n : ℕ) → E) (fun (n : ℕ) ↦ ∑ i ∈ range n, v i) fun (n : ℕ) ↦ u (f n) - u (f 0)
have h₁ : ∀ (n : ℕ), ∑ i ∈ range n, v i = u (f n) - u (f 0)
Tactic: ext n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Completeness (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
h :
  ∀ (u : ℕ → E),
    (Summable (α := ℝ) fun (x : ℕ) ↦ ‖u x‖) → ∃ (a : E), Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, u i) atTop (𝓝 a)
u : ℕ → E
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : Summable (α := ℝ) fun (i : ℕ) ↦ ‖u (f (i + 1)) - u (f i)‖
v : (n : ℕ) → E := fun (n : ℕ) ↦ u (f (n + 1)) - u (f n)
⊢ ∃ (a : E), Tendsto u atTop (𝓝 a)
have hv_sum : Eq.{u_1 + 1} (α := (n : ℕ) → E) (fun (n : ℕ) ↦ ∑ i ∈ range n, v i) fun (n : ℕ) ↦ u (f n) - u (f 0)
Tactic: have hv_sum : (fun n => (∑ i ∈ range n, v i)) = fun n => u (f n) - u (f 0) := by
    ext n
    exact sum_range_sub (u ∘ f) n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Completeness (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
h :
  ∀ (u : ℕ → E),
    (Summable (α := ℝ) fun (x : ℕ) ↦ ‖u x‖) → ∃ (a : E), Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, u i) atTop (𝓝 a)
u : ℕ → E
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : Summable (α := ℝ) fun (i : ℕ) ↦ ‖u (f (i + 1)) - u (f i)‖
v : (n : ℕ) → E := fun (n : ℕ) ↦ u (f (n + 1)) - u (f n)
hv_sum : Eq.{u_1 + 1} (α := (n : ℕ) → E) (fun (n : ℕ) ↦ ∑ i ∈ range n, v i) fun (n : ℕ) ↦ u (f n) - u (f 0)
⊢ ∃ (a : E), Tendsto u atTop (𝓝 a)
have a : ∀ (a : E) (ha : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, v i) atTop (𝓝 a)), ∃ (a : E), Tendsto u atTop (𝓝 a)
Tactic: obtain ⟨a, ha⟩ := h v hf₂
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Completeness (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
h :
  ∀ (u : ℕ → E),
    (Summable (α := ℝ) fun (x : ℕ) ↦ ‖u x‖) → ∃ (a : E), Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, u i) atTop (𝓝 a)
u : ℕ → E
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : Summable (α := ℝ) fun (i : ℕ) ↦ ‖u (f (i + 1)) - u (f i)‖
v : (n : ℕ) → E := fun (n : ℕ) ↦ u (f (n + 1)) - u (f n)
hv_sum : Eq.{u_1 + 1} (α := (n : ℕ) → E) (fun (n : ℕ) ↦ ∑ i ∈ range n, v i) fun (n : ℕ) ↦ u (f n) - u (f 0)
a : E
ha : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, v i) atTop (𝓝 a)
⊢ ∃ (a : E), Tendsto u atTop (𝓝 a)
have a₁ : Tendsto u atTop (𝓝 (a + u (f 0)))
Tactic: refine ⟨a + u (f 0), ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Completeness (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
h :
  ∀ (u : ℕ → E),
    (Summable (α := ℝ) fun (x : ℕ) ↦ ‖u x‖) → ∃ (a : E), Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, u i) atTop (𝓝 a)
u : ℕ → E
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : Summable (α := ℝ) fun (i : ℕ) ↦ ‖u (f (i + 1)) - u (f i)‖
v : (n : ℕ) → E := fun (n : ℕ) ↦ u (f (n + 1)) - u (f n)
hv_sum : Eq.{u_1 + 1} (α := (n : ℕ) → E) (fun (n : ℕ) ↦ ∑ i ∈ range n, v i) fun (n : ℕ) ↦ u (f n) - u (f 0)
a : E
ha : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, v i) atTop (𝓝 a)
⊢ Tendsto u atTop (𝓝 (a + u (f 0)))
have a₁ : Tendsto (u ∘ f) atTop (𝓝 (a + u (f 0)))
Tactic: refine tendsto_nhds_of_cauchySeq_of_subseq hu hf₁.tendsto_atTop ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Completeness (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
h :
  ∀ (u : ℕ → E),
    (Summable (α := ℝ) fun (x : ℕ) ↦ ‖u x‖) → ∃ (a : E), Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, u i) atTop (𝓝 a)
u : ℕ → E
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : Summable (α := ℝ) fun (i : ℕ) ↦ ‖u (f (i + 1)) - u (f i)‖
v : (n : ℕ) → E := fun (n : ℕ) ↦ u (f (n + 1)) - u (f n)
hv_sum : Eq.{u_1 + 1} (α := (n : ℕ) → E) (fun (n : ℕ) ↦ ∑ i ∈ range n, v i) fun (n : ℕ) ↦ u (f n) - u (f 0)
a : E
ha : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, v i) atTop (𝓝 a)
⊢ Tendsto (u ∘ f) atTop (𝓝 (a + u (f 0)))
have ha₁ : Tendsto (fun (n : ℕ) ↦ u (f n) - u (f 0)) atTop (𝓝 a)
Tactic: rw [hv_sum] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Completeness (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
h :
  ∀ (u : ℕ → E),
    (Summable (α := ℝ) fun (x : ℕ) ↦ ‖u x‖) → ∃ (a : E), Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, u i) atTop (𝓝 a)
u : ℕ → E
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : Summable (α := ℝ) fun (i : ℕ) ↦ ‖u (f (i + 1)) - u (f i)‖
v : (n : ℕ) → E := fun (n : ℕ) ↦ u (f (n + 1)) - u (f n)
hv_sum : Eq.{u_1 + 1} (α := (n : ℕ) → E) (fun (n : ℕ) ↦ ∑ i ∈ range n, v i) fun (n : ℕ) ↦ u (f n) - u (f 0)
a : E
ha : Tendsto (fun (n : ℕ) ↦ u (f n) - u (f 0)) atTop (𝓝 a)
⊢ Tendsto (u ∘ f) atTop (𝓝 (a + u (f 0)))
have h₁ : Tendsto (fun (n : ℕ) ↦ u (f n) - u (f 0) + u (f 0)) atTop (𝓝 (a + u (f 0)))
Tactic: have h₁ : Tendsto (fun n => u (f n) - u (f 0) + u (f 0)) atTop (𝓝 (a + u (f 0))) :=
    Tendsto.add_const _ ha
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Completeness (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
u : ℕ → E
hu : Summable (α := ℝ) fun (x : ℕ) ↦ ‖u x‖
⊢ ∃ (a : E), Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, u i) atTop (𝓝 a)
have refine : Summable (α := ℝ) fun (n : ℕ) ↦ dist.{u_1} (α := E) (∑ i ∈ range n, u i) (∑ i ∈ range n.succ, u i)
Tactic: refine cauchySeq_tendsto_of_complete <| cauchySeq_of_summable_dist ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Completion (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
x y : Completion E
⊢ dist x y = ‖-x + y‖
have hp : IsClosed.{u_1} (X := Completion E × Completion E) {x : Completion E × Completion E | dist x.1 x.2 = ‖-x.1 + x.2‖}
Tactic: induction x, y using Completion.induction_on₂
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Completion (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
x y : Completion E
hp : IsClosed.{u_1} (X := Completion E × Completion E) {x : Completion E × Completion E | dist x.1 x.2 = ‖-x.1 + x.2‖}
⊢ dist x y = ‖-x + y‖
have ih : ∀ (a b : E),
  dist (α := Completion E) (↑a : Completion E) (↑b : Completion E) =
    ‖HAdd.hAdd (α := Completion E) (-(↑a : Completion E)) (↑b : Completion E)‖
Tactic: induction x, y using Completion.induction_on₂
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Completion (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
⊢ IsClosed.{u_1} (X := Completion E × Completion E) {x : Completion E × Completion E | dist x.1 x.2 = ‖-x.1 + x.2‖}
have hp : Continuous (Y := ℝ) fun (x : Completion E × Completion E) ↦ ‖-x.1 + x.2‖
Tactic: refine isClosed_eq (Completion.uniformContinuous_extension₂ _).continuous ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Completion (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
a b : E
⊢ dist (α := Completion E) (↑a : Completion E) (↑b : Completion E) =
    ‖HAdd.hAdd (α := Completion E) (-(↑a : Completion E)) (↑b : Completion E)‖
have ih : dist (α := Completion E) (↑a : Completion E) (↑b : Completion E) =
  ‖HAdd.hAdd (α := Completion E) (↑(-a) : Completion E) (↑b : Completion E)‖
Tactic: rw [← Completion.coe_neg, ← Completion.coe_add, norm_coe, Completion.dist_eq,
        dist_eq_norm_neg_add]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Completion (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
a b : E
ih :
  dist (α := Completion E) (↑a : Completion E) (↑b : Completion E) =
    ‖HAdd.hAdd (α := Completion E) (↑(-a) : Completion E) (↑b : Completion E)‖
⊢ dist (α := Completion E) (↑a : Completion E) (↑b : Completion E) =
    ‖HAdd.hAdd (α := Completion E) (-(↑a : Completion E)) (↑b : Completion E)‖
have ih₁ : dist (α := Completion E) (↑a : Completion E) (↑b : Completion E) = norm (E := Completion E) (↑(-a + b) : Completion E)
Tactic: rw [← Completion.coe_neg, ← Completion.coe_add, norm_coe, Completion.dist_eq,
        dist_eq_norm_neg_add]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Completion (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
a b : E
ih :
  dist (α := Completion E) (↑a : Completion E) (↑b : Completion E) =
    ‖HAdd.hAdd (α := Completion E) (↑(-a) : Completion E) (↑b : Completion E)‖
ih₁ :
  dist (α := Completion E) (↑a : Completion E) (↑b : Completion E) = norm (E := Completion E) (↑(-a + b) : Completion E)
⊢ dist (α := Completion E) (↑a : Completion E) (↑b : Completion E) =
    ‖HAdd.hAdd (α := Completion E) (-(↑a : Completion E)) (↑b : Completion E)‖
have ih₂ : dist (α := Completion E) (↑a : Completion E) (↑b : Completion E) = ‖-a + b‖
Tactic: rw [← Completion.coe_neg, ← Completion.coe_add, norm_coe, Completion.dist_eq,
        dist_eq_norm_neg_add]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Completion (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
a b : E
ih :
  dist (α := Completion E) (↑a : Completion E) (↑b : Completion E) =
    ‖HAdd.hAdd (α := Completion E) (↑(-a) : Completion E) (↑b : Completion E)‖
ih₁ :
  dist (α := Completion E) (↑a : Completion E) (↑b : Completion E) = norm (E := Completion E) (↑(-a + b) : Completion E)
ih₂ : dist (α := Completion E) (↑a : Completion E) (↑b : Completion E) = ‖-a + b‖
⊢ dist (α := Completion E) (↑a : Completion E) (↑b : Completion E) =
    ‖HAdd.hAdd (α := Completion E) (-(↑a : Completion E)) (↑b : Completion E)‖
have ih₃ : dist a b = ‖-a + b‖
Tactic: rw [← Completion.coe_neg, ← Completion.coe_add, norm_coe, Completion.dist_eq,
        dist_eq_norm_neg_add]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Completion (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
a b : E
ih :
  dist (α := Completion E) (↑a : Completion E) (↑b : Completion E) =
    ‖HAdd.hAdd (α := Completion E) (↑(-a) : Completion E) (↑b : Completion E)‖
ih₁ :
  dist (α := Completion E) (↑a : Completion E) (↑b : Completion E) = norm (E := Completion E) (↑(-a + b) : Completion E)
ih₂ : dist (α := Completion E) (↑a : Completion E) (↑b : Completion E) = ‖-a + b‖
ih₃ : dist a b = ‖-a + b‖
⊢ dist (α := Completion E) (↑a : Completion E) (↑b : Completion E) =
    ‖HAdd.hAdd (α := Completion E) (-(↑a : Completion E)) (↑b : Completion E)‖
have ih₄ : ‖-a + b‖ = ‖-a + b‖
Tactic: rw [← Completion.coe_neg, ← Completion.coe_add, norm_coe, Completion.dist_eq,
        dist_eq_norm_neg_add]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Constructions (goal)
Goal:
ι : Type u_1
G : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedGroup (G i)
f : (i : ι) → G i
r : ℝ
inst_2 : Nonempty ι
⊢ ‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r
have pos : ∀ (hr : 0 ≤ r), ‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r
Tactic: by_cases hr : 0 ≤ r
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Constructions (goal)
Goal:
ι : Type u_1
G : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedGroup (G i)
f : (i : ι) → G i
r : ℝ
inst_2 : Nonempty ι
pos : ∀ (hr : 0 ≤ r), ‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r
⊢ ‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r
have neg : ∀ (hr : ¬0 ≤ r), ‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r
Tactic: by_cases hr : 0 ≤ r
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Constructions (goal)
Goal:
ι : Type u_1
G : ι → Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → NormedAddCommGroup (G i)
i : ι
y : G i
b : ι
⊢ ‖single (M := G) i y b‖₊ = single (M := fun (x : ι) ↦ ℝ≥0) i ‖y‖₊ b
have refine : ∀ (i : ι), Eq (α := ℝ≥0) ((fun (i : ι) (x : G i) ↦ ‖x‖₊) i 0) 0
Tactic: refine Pi.apply_single (fun i (x : G i) ↦ ‖x‖₊) ?_ i y b
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Constructions (hypothesis)
Goal:
ι : Type u_1
G : ι → Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → NormedAddCommGroup (G i)
i : ι
y : G i
⊢ ‖single (M := G) i y‖₊ = ‖y‖₊
have H : ∀ (b : ι), ‖single (M := G) i y b‖₊ = single (M := fun (x : ι) ↦ ℝ≥0) i ‖y‖₊ b
Tactic: have H : ∀ b, ‖single i y b‖₊ = single (M := fun _ ↦ ℝ≥0) i ‖y‖₊ b := by
    intro b
    refine Pi.apply_single (fun i (x : G i) ↦ ‖x‖₊) ?_ i y b
    simp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Continuity (goal)
Goal:
E : Type u_4
inst : SeminormedGroup E
x : E
⊢ Membership.mem (γ := Set E) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {1}) x ↔ ‖x‖ = 0
have rw : Membership.mem (γ := Set E) (closedBall 1 0) x ↔ ‖x‖ = 0
Tactic: rw [← closedBall_zero', mem_closedBall_one_iff, (norm_nonneg' x).ge_iff_eq']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Continuity (goal)
Goal:
E : Type u_4
inst : SeminormedGroup E
x : E
rw : Membership.mem (γ := Set E) (closedBall 1 0) x ↔ ‖x‖ = 0
⊢ Membership.mem (γ := Set E) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {1}) x ↔ ‖x‖ = 0
have rw₁ : ‖x‖ ≤ 0 ↔ ‖x‖ = 0
Tactic: rw [← closedBall_zero', mem_closedBall_one_iff, (norm_nonneg' x).ge_iff_eq']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Continuity (goal)
Goal:
E : Type u_4
inst : SeminormedGroup E
x : E
rw : Membership.mem (γ := Set E) (closedBall 1 0) x ↔ ‖x‖ = 0
rw₁ : ‖x‖ ≤ 0 ↔ ‖x‖ = 0
⊢ Membership.mem (γ := Set E) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {1}) x ↔ ‖x‖ = 0
have rw₂ : ‖x‖ = 0 ↔ ‖x‖ = 0
Tactic: rw [← closedBall_zero', mem_closedBall_one_iff, (norm_nonneg' x).ge_iff_eq']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Continuity (goal)
Goal:
ι : Type u_2
κ : Type u_3
G : Type u_6
inst : SeminormedGroup G
f : ι → κ → G
l : Filter ι
l' : Filter κ
⊢ UniformCauchySeqOnFilter f l l' ↔
    TendstoUniformlyOnFilter.{u_3, u_6, u_2} (β := G) (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) l'
have refine_1 : ∀ (hf : UniformCauchySeqOnFilter f l l') (u : Set (G × G)) (hu : u ∈ 𝓤 G),
  ∀ᶠ (n : Prod.{u_2, u_3} (ι × ι) κ) in (l ×ˢ l) ×ˢ l',
    (1 n.2, (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) n.1 n.2) ∈ u
Tactic: refine ⟨fun hf u hu => ?_, fun hf u hu => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Continuity (goal)
Goal:
ι : Type u_2
κ : Type u_3
G : Type u_6
inst : SeminormedGroup G
f : ι → κ → G
l : Filter ι
l' : Filter κ
refine_1 :
  ∀ (hf : UniformCauchySeqOnFilter f l l') (u : Set (G × G)) (hu : u ∈ 𝓤 G),
    ∀ᶠ (n : Prod.{u_2, u_3} (ι × ι) κ) in (l ×ˢ l) ×ˢ l',
      (1 n.2, (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) n.1 n.2) ∈ u
⊢ UniformCauchySeqOnFilter f l l' ↔
    TendstoUniformlyOnFilter.{u_3, u_6, u_2} (β := G) (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) l'
have refine_2 : ∀
  (hf :
    TendstoUniformlyOnFilter.{u_3, u_6, u_2} (β := G) (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) l')
  (u : Set (G × G)) (hu : u ∈ 𝓤 G), ∀ᶠ (m : Prod.{u_2, u_3} (ι × ι) κ) in (l ×ˢ l) ×ˢ l', (f m.1.1 m.2, f m.1.2 m.2) ∈ u
Tactic: refine ⟨fun hf u hu => ?_, fun hf u hu => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Continuity (goal)
Goal:
ι : Type u_2
κ : Type u_3
G : Type u_6
inst : SeminormedGroup G
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : UniformCauchySeqOnFilter f l l'
u : Set (G × G)
hu : u ∈ 𝓤 G
⊢ ∀ᶠ (n : Prod.{u_2, u_3} (ι × ι) κ) in (l ×ˢ l) ×ˢ l',
    (1 n.2, (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) n.1 n.2) ∈ u
have refine_1 : ∀ (ε : ℝ) (hε : 0 < ε)
  (H : ∀ (a b : G), Membership.mem (γ := SetRel G G) {p : G × G | dist p.1 p.2 < ε} (a, b) → (a, b) ∈ u),
  ∀ᶠ (n : Prod.{u_2, u_3} (ι × ι) κ) in (l ×ˢ l) ×ˢ l',
    (1 n.2, (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) n.1 n.2) ∈ u
Tactic: obtain ⟨ε, hε, H⟩ := uniformity_basis_dist.mem_uniformity_iff.mp hu
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Continuity (goal)
Goal:
ι : Type u_2
κ : Type u_3
G : Type u_6
inst : SeminormedGroup G
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : UniformCauchySeqOnFilter f l l'
u : Set (G × G)
hu : u ∈ 𝓤 G
ε : ℝ
hε : 0 < ε
H : ∀ (a b : G), Membership.mem (γ := SetRel G G) {p : G × G | dist p.1 p.2 < ε} (a, b) → (a, b) ∈ u
⊢ ∀ᶠ (n : Prod.{u_2, u_3} (ι × ι) κ) in (l ×ˢ l) ×ˢ l',
    (1 n.2, (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) n.1 n.2) ∈ u
have refine_1 : ∀ (x : Prod.{u_2, u_3} (ι × ι) κ)
  (hx : Membership.mem (γ := Set (G × G)) {p : G × G | dist p.1 p.2 < ε} (f x.1.1 x.2, f x.1.2 x.2)),
  Membership.mem (γ := SetRel G G) {p : G × G | dist p.1 p.2 < ε} (1, (f x.1.1 x.2)⁻¹ * f x.1.2 x.2)
Tactic: refine
      (hf { p : G × G | dist p.fst p.snd < ε } <| dist_mem_uniformity hε).mono fun x hx =>
        H 1 ((f x.fst.fst x.snd)⁻¹ * f x.fst.snd x.snd) ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Continuity (goal)
Goal:
ι : Type u_2
κ : Type u_3
G : Type u_6
inst : SeminormedGroup G
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : TendstoUniformlyOnFilter.{u_3, u_6, u_2} (β := G) (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) l'
u : Set (G × G)
hu : u ∈ 𝓤 G
⊢ ∀ᶠ (m : Prod.{u_2, u_3} (ι × ι) κ) in (l ×ˢ l) ×ˢ l', (f m.1.1 m.2, f m.1.2 m.2) ∈ u
have refine_2 : ∀ (ε : ℝ) (hε : 0 < ε)
  (H : ∀ (a b : G), Membership.mem (γ := SetRel G G) {p : G × G | dist p.1 p.2 < ε} (a, b) → (a, b) ∈ u),
  ∀ᶠ (m : Prod.{u_2, u_3} (ι × ι) κ) in (l ×ˢ l) ×ˢ l', (f m.1.1 m.2, f m.1.2 m.2) ∈ u
Tactic: obtain ⟨ε, hε, H⟩ := uniformity_basis_dist.mem_uniformity_iff.mp hu
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Continuity (goal)
Goal:
ι : Type u_2
κ : Type u_3
G : Type u_6
inst : SeminormedGroup G
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : TendstoUniformlyOnFilter.{u_3, u_6, u_2} (β := G) (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) l'
u : Set (G × G)
hu : u ∈ 𝓤 G
ε : ℝ
hε : 0 < ε
H : ∀ (a b : G), Membership.mem (γ := SetRel G G) {p : G × G | dist p.1 p.2 < ε} (a, b) → (a, b) ∈ u
⊢ ∀ᶠ (m : Prod.{u_2, u_3} (ι × ι) κ) in (l ×ˢ l) ×ˢ l', (f m.1.1 m.2, f m.1.2 m.2) ∈ u
have refine_2 : ∀ (x : Prod.{u_2, u_3} (ι × ι) κ)
  (hx :
    Membership.mem.{u_6, u_6} (γ := Set (G × G)) {p : G × G | dist p.1 p.2 < ε}
      (1 x.2, (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) x.1 x.2)),
  Membership.mem (γ := SetRel G G) {p : G × G | dist p.1 p.2 < ε} (f x.1.1 x.2, f x.1.2 x.2)
Tactic: refine
      (hf { p : G × G | dist p.fst p.snd < ε } <| dist_mem_uniformity hε).mono fun x hx =>
        H (f x.fst.fst x.snd) (f x.fst.snd x.snd) ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Continuity (goal)
Goal:
ι : Type u_2
κ : Type u_3
G : Type u_6
inst : SeminormedGroup G
f : ι → κ → G
s : Set κ
l : Filter ι
⊢ UniformCauchySeqOn f l s ↔
    TendstoUniformlyOn.{u_3, u_6, u_2} (β := G) (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) s
have rw : UniformCauchySeqOn f l s ↔
  TendstoUniformlyOnFilter.{u_3, u_6, u_2} (β := G) (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) (𝓟 s)
Tactic: rw [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter,
    uniformCauchySeqOn_iff_uniformCauchySeqOnFilter,
    SeminormedGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Continuity (goal)
Goal:
ι : Type u_2
κ : Type u_3
G : Type u_6
inst : SeminormedGroup G
f : ι → κ → G
s : Set κ
l : Filter ι
rw :
  UniformCauchySeqOn f l s ↔
    TendstoUniformlyOnFilter.{u_3, u_6, u_2} (β := G) (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) (𝓟 s)
⊢ UniformCauchySeqOn f l s ↔
    TendstoUniformlyOn.{u_3, u_6, u_2} (β := G) (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) s
have rw₁ : UniformCauchySeqOnFilter f l (𝓟 s) ↔
  TendstoUniformlyOnFilter.{u_3, u_6, u_2} (β := G) (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) (𝓟 s)
Tactic: rw [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter,
    uniformCauchySeqOn_iff_uniformCauchySeqOnFilter,
    SeminormedGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Continuity (goal)
Goal:
ι : Type u_2
κ : Type u_3
G : Type u_6
inst : SeminormedGroup G
f : ι → κ → G
s : Set κ
l : Filter ι
rw :
  UniformCauchySeqOn f l s ↔
    TendstoUniformlyOnFilter.{u_3, u_6, u_2} (β := G) (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) (𝓟 s)
rw₁ :
  UniformCauchySeqOnFilter f l (𝓟 s) ↔
    TendstoUniformlyOnFilter.{u_3, u_6, u_2} (β := G) (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) (𝓟 s)
⊢ UniformCauchySeqOn f l s ↔
    TendstoUniformlyOn.{u_3, u_6, u_2} (β := G) (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) s
have rw₂ : TendstoUniformlyOnFilter.{u_3, u_6, u_2} (β := G) (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) (𝓟 s) ↔
  TendstoUniformlyOnFilter.{u_3, u_6, u_2} (β := G) (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) (𝓟 s)
Tactic: rw [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter,
    uniformCauchySeqOn_iff_uniformCauchySeqOnFilter,
    SeminormedGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_one]