awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Type u_3
inst_3 : SeminormedAddCommGroup K
j : NormedAddGroupHom K H
hj : ∀ (x : K), norm.{u_2} (E := H) ((j : (a : K) → H) x : H) = ‖x‖
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : ∀ (k : K), ∃ (g : G), Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) g : H) ((j : (a : K) → H) k : H) ∧ ‖g‖ ≤ C * ‖k‖
h : H
h_in : h ∈ j.range
rcases :
  ∀ (k : K) (h_in : Membership.mem (α := H) j.range ((j : (a : K) → H) k : H)),
    ∃ (g : G),
      Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) g : H) ((j : (a : K) → H) k : H) ∧
        ‖g‖ ≤ C * norm.{u_2} (E := H) ((j : (a : K) → H) k : H)
⊢ ∃ (g : G), (f : (a : G) → H) g = h ∧ ‖g‖ ≤ C * ‖h‖

Tactic:
rcases (j.mem_range _).mp h_in with ⟨k, rfl⟩

Premises used: Iff.mp, NormedAddGroupHom.mem_range, rfl
-- 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 : Type u_3
inst_3 : SeminormedAddCommGroup K
j : NormedAddGroupHom K H
hj : ∀ (x : K), norm.{u_2} (E := H) ((j : (a : K) → H) x : H) = ‖x‖
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : ∀ (k : K), ∃ (g : G), Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) g : H) ((j : (a : K) → H) k : H) ∧ ‖g‖ ≤ C * ‖k‖
k : K
h_in : Membership.mem (α := H) j.range ((j : (a : K) → H) k : H)
rw : ∃ (g : G), Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) g : H) ((j : (a : K) → H) k : H) ∧ ‖g‖ ≤ C * ‖k‖
⊢ ∃ (g : G),
    Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) g : H) ((j : (a : K) → H) k : H) ∧
      ‖g‖ ≤ C * norm.{u_2} (E := H) ((j : (a : K) → H) k : H)

Tactic:
rw [hj]
-- 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 : Type u_3
inst_3 : SeminormedAddCommGroup K
j : NormedAddGroupHom K H
hj : ∀ (x : K), norm.{u_2} (E := H) ((j : (a : K) → H) x : H) = ‖x‖
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : ∀ (k : K), ∃ (g : G), Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) g : H) ((j : (a : K) → H) k : H) ∧ ‖g‖ ≤ C * ‖k‖
k : K
h_in : Membership.mem (α := H) j.range ((j : (a : K) → H) k : H)
⊢ ∃ (g : G), Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) g : H) ((j : (a : K) → H) k : H) ∧ ‖g‖ ≤ C * ‖k‖

Tactic:
hyp k
-- 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 : Type u_3
inst_3 : SeminormedAddCommGroup K
j : NormedAddGroupHom K H
hj : ∀ (x : K), norm.{u_2} (E := H) ((j : (a : K) → H) x : H) = ‖x‖
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : ∀ (k : K), ∃ (g : G), Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) g : H) ((j : (a : K) → H) k : H) ∧ ‖g‖ ≤ C * ‖k‖
k : K
h_in : Membership.mem (α := H) j.range ((j : (a : K) → H) k : H)
⊢ ∃ (g : G), Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) g : H) ((j : (a : K) → H) k : H) ∧ ‖g‖ ≤ C * ‖k‖

Tactic:
exact hyp k
-- 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 : Type u_3
inst_3 : SeminormedAddCommGroup K
j : NormedAddGroupHom K H
hj : ∀ (x : K), norm.{u_2} (E := H) ((j : (a : K) → H) x : H) = ‖x‖
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : ∀ (k : K), ∃ (g : G), Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) g : H) ((j : (a : K) → H) k : H) ∧ ‖g‖ ≤ C * ‖k‖
⊢ ∀ h ∈ j.range, ∃ (g : G), (f : (a : G) → H) g = h ∧ ‖g‖ ≤ C * ‖h‖

Tactic:
replace hyp : ∀ h ∈ j.range, ∃ g, f g = h ∧ ‖g‖ ≤ C * ‖h‖ := by
    intro h h_in
    rcases (j.mem_range _).mp h_in with ⟨k, rfl⟩
    rw [hj]
    exact hyp k
-- 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 : Type u_3
inst_3 : SeminormedAddCommGroup K
j : NormedAddGroupHom K H
hj : ∀ (x : K), norm.{u_2} (E := H) ((j : (a : K) → H) x : H) = ‖x‖
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : ∀ h ∈ j.range, ∃ (g : G), (f : (a : G) → H) g = h ∧ ‖g‖ ≤ C * ‖h‖
⊢ f.SurjectiveOnWith j.range.topologicalClosure (C + ε)

Tactic:
controlled_closure_of_complete hC hε hyp

Premises used: controlled_closure_of_complete
-- 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 : Type u_3
inst_3 : SeminormedAddCommGroup K
j : NormedAddGroupHom K H
hj : ∀ (x : K), norm.{u_2} (E := H) ((j : (a : K) → H) x : H) = ‖x‖
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : ∀ h ∈ j.range, ∃ (g : G), (f : (a : G) → H) g = h ∧ ‖g‖ ≤ C * ‖h‖
⊢ f.SurjectiveOnWith j.range.topologicalClosure (C + ε)

Tactic:
exact controlled_closure_of_complete hC hε hyp

Premises used: controlled_closure_of_complete
-- Module: Mathlib.Analysis.Normed.Group.Defs
Goal:
E : Type u_8
inst : NNNorm E
x : E
⊢ ‖x‖ₑ = (↑‖x‖₊ : ℝ≥0∞)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Defs
Goal:
E : Type u_8
inst : NNNorm E
x : E
⊢ ‖x‖ₑ.toNNReal = ‖x‖₊

Tactic:
rfl

Premises used: ENNReal.toNNReal, WithTop.untopD, WithTop.recTopCoe, rfl
-- Module: Mathlib.Analysis.Normed.Group.Defs
Goal:
E : Type u_8
inst : NNNorm E
x : E
r : ℝ≥0
⊢ (↑r : ℝ≥0∞) ≤ ‖x‖ₑ ↔ r ≤ ‖x‖₊

Tactic:
simp [enorm]

Premises used: ENorm.enorm
-- Module: Mathlib.Analysis.Normed.Group.Defs
Goal:
E : Type u_8
inst : NNNorm E
x : E
r : ℝ≥0
⊢ ‖x‖ₑ ≤ (↑r : ℝ≥0∞) ↔ ‖x‖₊ ≤ r

Tactic:
simp [enorm]

Premises used: ENorm.enorm
-- Module: Mathlib.Analysis.Normed.Group.Defs
Goal:
E : Type u_8
inst : NNNorm E
x : E
r : ℝ≥0
⊢ (↑r : ℝ≥0∞) < ‖x‖ₑ ↔ r < ‖x‖₊

Tactic:
simp [enorm]

Premises used: ENorm.enorm
-- Module: Mathlib.Analysis.Normed.Group.Defs
Goal:
E : Type u_8
inst : NNNorm E
x : E
r : ℝ≥0
⊢ ‖x‖ₑ < (↑r : ℝ≥0∞) ↔ ‖x‖₊ < r

Tactic:
simp [enorm]

Premises used: ENorm.enorm
-- Module: Mathlib.Analysis.Normed.Group.Defs
Goal:
E : Type u_8
inst : NNNorm E
x : E
⊢ ‖x‖ₑ ≠ ∞

Tactic:
simp [enorm]

Premises used: ENorm.enorm
-- Module: Mathlib.Analysis.Normed.Group.Defs
Goal:
E : Type u_8
inst : NNNorm E
x : E
⊢ ‖x‖ₑ < ∞

Tactic:
simp [enorm]

Premises used: ENorm.enorm
-- Module: Mathlib.Analysis.Normed.Group.Defs
Goal:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : Norm E
inst_1 : Group E
inst_2 : PseudoMetricSpace E
h₁ : ∀ (x : E), ‖x‖ = dist 1 x
h₂ : ∀ (x y z : E), dist x y ≤ dist (z * x) (z * y)
x y : E
rw : dist x y = dist 1 (x⁻¹ * y)
⊢ dist x y = ‖x⁻¹ * y‖

Tactic:
rw [h₁]
-- Module: Mathlib.Analysis.Normed.Group.Defs
Goal:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : Norm E
inst_1 : Group E
inst_2 : PseudoMetricSpace E
h₁ : ∀ (x : E), ‖x‖ = dist 1 x
h₂ : ∀ (x y z : E), dist x y ≤ dist (z * x) (z * y)
x y : E
a : dist x y ≤ dist 1 (x⁻¹ * y)
a₁ : dist 1 (x⁻¹ * y) ≤ dist x y
⊢ dist x y = dist 1 (x⁻¹ * y)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Normed.Group.Defs
Goal:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : Norm E
inst_1 : Group E
inst_2 : PseudoMetricSpace E
h₁ : ∀ (x : E), ‖x‖ = dist 1 x
h₂ : ∀ (x y z : E), dist x y ≤ dist (z * x) (z * y)
x y : E
⊢ dist x y ≤ dist 1 (x⁻¹ * y)

Tactic:
simpa only [div_eq_mul_inv, ← inv_mul_cancel x] using h₂ x y x⁻¹

Premises used: inv_mul_cancel, div_eq_mul_inv, Inv.inv
-- Module: Mathlib.Analysis.Normed.Group.Defs
Goal:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : Norm E
inst_1 : Group E
inst_2 : PseudoMetricSpace E
h₁ : ∀ (x : E), ‖x‖ = dist 1 x
h₂ : ∀ (x y z : E), dist x y ≤ dist (z * x) (z * y)
x y : E
⊢ dist 1 (x⁻¹ * y) ≤ dist x y

Tactic:
simpa only [mul_inv_cancel, mul_one, ← mul_assoc, one_mul] using h₂ 1 (x⁻¹ * y) x

Premises used: HMul.hMul, mul_assoc, Inv.inv, mul_inv_cancel, mul_one, OfNat.ofNat, one_mul
-- Module: Mathlib.Analysis.Normed.Group.Defs
Goal:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : Norm E
inst_1 : Group E
inst_2 : PseudoMetricSpace E
h₁ : ∀ (x : E), ‖x‖ = dist 1 x
h₂ : ∀ (x y z : E), dist (z * x) (z * y) ≤ dist x y
x y : E
rw : dist x y = dist 1 (x⁻¹ * y)
⊢ dist x y = ‖x⁻¹ * y‖

Tactic:
rw [h₁]
-- Module: Mathlib.Analysis.Normed.Group.Defs
Goal:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : Norm E
inst_1 : Group E
inst_2 : PseudoMetricSpace E
h₁ : ∀ (x : E), ‖x‖ = dist 1 x
h₂ : ∀ (x y z : E), dist (z * x) (z * y) ≤ dist x y
x y : E
a : dist x y ≤ dist 1 (x⁻¹ * y)
a₁ : dist 1 (x⁻¹ * y) ≤ dist x y
⊢ dist x y = dist 1 (x⁻¹ * y)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Normed.Group.Defs
Goal:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : Norm E
inst_1 : Group E
inst_2 : PseudoMetricSpace E
h₁ : ∀ (x : E), ‖x‖ = dist 1 x
h₂ : ∀ (x y z : E), dist (z * x) (z * y) ≤ dist x y
x y : E
⊢ dist x y ≤ dist 1 (x⁻¹ * y)

Tactic:
simpa only [mul_inv_cancel, mul_one, ← mul_assoc, one_mul] using h₂ 1 (x⁻¹ * y) x

Premises used: HMul.hMul, mul_assoc, Inv.inv, mul_inv_cancel, mul_one, OfNat.ofNat, one_mul
-- Module: Mathlib.Analysis.Normed.Group.Defs
Goal:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : Norm E
inst_1 : Group E
inst_2 : PseudoMetricSpace E
h₁ : ∀ (x : E), ‖x‖ = dist 1 x
h₂ : ∀ (x y z : E), dist (z * x) (z * y) ≤ dist x y
x y : E
⊢ dist 1 (x⁻¹ * y) ≤ dist x y

Tactic:
simpa only [div_eq_mul_inv, ← inv_mul_cancel x] using h₂ x y x⁻¹

Premises used: inv_mul_cancel, div_eq_mul_inv, Inv.inv
-- Module: Mathlib.Analysis.Normed.Group.Defs
Goal:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : Group E
f : GroupSeminorm E
x : E
⊢ Eq (α := ℝ) ((f : (a : E) → ℝ) (x⁻¹ * x) : ℝ) (0 : ℝ)

Tactic:
simp only [inv_mul_cancel, map_one_eq_zero]

Premises used: inv_mul_cancel, GroupSeminormClass.map_one_eq_zero
-- Module: Mathlib.Analysis.Normed.Group.Defs
Goal:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : Group E
f : GroupSeminorm E
x y : E
⊢ Eq (α := ℝ) ((f : (a : E) → ℝ) (y⁻¹ * x)⁻¹ : ℝ) ((f : (a : E) → ℝ) (y⁻¹ * x) : ℝ)

Tactic:
map_inv_eq_map f (y⁻¹ * x)

Premises used: HMul.hMul, GroupSeminormClass.map_inv_eq_map, Inv.inv
-- Module: Mathlib.Analysis.Normed.Group.Defs
Goal:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : Group E
f : GroupSeminorm E
x y : E
h : x⁻¹ * y = (y⁻¹ * x)⁻¹
⊢ Eq (α := ℝ) ((f : (a : E) → ℝ) (x⁻¹ * y) : ℝ) ((f : (a : E) → ℝ) (y⁻¹ * x) : ℝ)

Tactic:
convert! map_inv_eq_map f (y⁻¹ * x) using 2

Premises used: HMul.hMul, GroupSeminormClass.map_inv_eq_map, Inv.inv
-- Module: Mathlib.Analysis.Normed.Group.Defs
Goal:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : Group E
f : GroupSeminorm E
x y : E
⊢ x⁻¹ * y = (y⁻¹ * x)⁻¹

Tactic:
group
-- Module: Mathlib.Analysis.Normed.Group.Defs
Goal:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : Group E
f : GroupSeminorm E
x y z : E
⊢ (f : (a : E) → ℝ) (x⁻¹ * y * (y⁻¹ * z)) ≤
    HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : E) → ℝ) (x⁻¹ * y) : ℝ) ((f : (a : E) → ℝ) (y⁻¹ * z) : ℝ)

Tactic:
map_mul_le_add f (x⁻¹ * y) (y⁻¹ * z)

Premises used: HMul.hMul, Inv.inv, MulLEAddHomClass.map_mul_le_add
-- Module: Mathlib.Analysis.Normed.Group.Defs
Goal:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : Group E
f : GroupSeminorm E
x y z : E
h : x⁻¹ * z = x⁻¹ * y * (y⁻¹ * z)
⊢ (f : (a : E) → ℝ) (x⁻¹ * z) ≤
    HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : E) → ℝ) (x⁻¹ * y) : ℝ) ((f : (a : E) → ℝ) (y⁻¹ * z) : ℝ)

Tactic:
convert! map_mul_le_add f (x⁻¹ * y) (y⁻¹ * z) using 2

Premises used: HMul.hMul, Inv.inv, MulLEAddHomClass.map_mul_le_add
-- Module: Mathlib.Analysis.Normed.Group.Defs
Goal:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : Group E
f : GroupSeminorm E
x y z : E
⊢ x⁻¹ * z = x⁻¹ * y * (y⁻¹ * z)

Tactic:
group
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n
⊢ TendstoUniformlyOn.{u_2, u_3, u_1} (β := F) (fun (t : Finset α) (x : β) ↦ ∑ n ∈ t, f n x)
    (fun (x : β) ↦ ∑' (n : α), f n x) atTop s

Tactic:
tendstoUniformlyOn_iff.2 fun ε εpos => ?_

Premises used: Iff.mpr, Metric.tendstoUniformlyOn_iff
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n
refine :
  ∀ (ε : ℝ) (εpos : ε > 0),
    ∀ᶠ (n : Finset α) in atTop, ∀ x ∈ s, dist.{u_3} (α := F) (∑' (n : α), f n x) (∑ n ∈ n, f n x) < ε
⊢ TendstoUniformlyOn.{u_2, u_3, u_1} (β := F) (fun (t : Finset α) (x : β) ↦ ∑ n ∈ t, f n x)
    (fun (x : β) ↦ ∑' (n : α), f n x) atTop s

Tactic:
refine tendstoUniformlyOn_iff.2 fun ε εpos => ?_

Premises used: Iff.mpr, Metric.tendstoUniformlyOn_iff
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
h :
  ∀ (t : Finset α) (ht : ∑' (a : { x : α // x ∉ t }), u (↑a : α) < ε) (x : β) (hx : x ∈ s),
    dist.{u_3} (α := F) (∑' (n : α), f n x) (∑ n ∈ t, f n x) < ε
⊢ ∀ᶠ (n : Finset α) in atTop, ∀ x ∈ s, dist.{u_3} (α := F) (∑' (n : α), f n x) (∑ n ∈ n, f n x) < ε

Tactic:
filter_upwards [(tendsto_order.1 (tendsto_tsum_compl_atTop_zero u)).2 _ εpos] with t ht x hx

Premises used: tendsto_order, And.right, tendsto_tsum_compl_atTop_zero, Iff.mp
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
t : Finset α
ht : ∑' (a : { x : α // x ∉ t }), u (↑a : α) < ε
x : β
hx : x ∈ s
⊢ Summable (α := ℝ) fun (n : α) ↦ ‖f n x‖

Tactic:
have A : Summable fun n => ‖f n x‖ :=
    .of_nonneg_of_le (fun _ ↦ norm_nonneg _) (fun n => hfu n x hx) hu
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
t : Finset α
ht : ∑' (a : { x : α // x ∉ t }), u (↑a : α) < ε
x : β
hx : x ∈ s
A : Summable (α := ℝ) fun (n : α) ↦ ‖f n x‖
h : norm.{u_3} (E := F) (∑' (x_1 : { x : α // x ∉ t }), f (↑x_1 : α) x) < ε
⊢ dist.{u_3} (α := F) (∑' (n : α), f n x) (∑ n ∈ t, f n x) < ε

Tactic:
rw [dist_eq_norm, ← A.of_norm.sum_add_tsum_subtype_compl t, add_sub_cancel_left]

Premises used: Summable.sum_add_tsum_subtype_compl, dist_eq_norm, add_sub_cancel_left, Summable.of_norm
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
t : Finset α
ht : ∑' (a : { x : α // x ∉ t }), u (↑a : α) < ε
x : β
hx : x ∈ s
A : Summable (α := ℝ) fun (n : α) ↦ ‖f n x‖
apply : norm.{u_3} (E := F) (∑' (x_1 : { x : α // x ∉ t }), f (↑x_1 : α) x) ≤ ∑' (a : { x : α // x ∉ t }), u (↑a : α)
⊢ norm.{u_3} (E := F) (∑' (x_1 : { x : α // x ∉ t }), f (↑x_1 : α) x) < ε

Tactic:
apply lt_of_le_of_lt _ ht

Premises used: lt_of_le_of_lt
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
t : Finset α
ht : ∑' (a : { x : α // x ∉ t }), u (↑a : α) < ε
x : β
hx : x ∈ s
A : Summable (α := ℝ) fun (n : α) ↦ ‖f n x‖
apply : LE.le (α := ℝ) (∑' (i : { x : α // x ∉ t }), ‖f (↑i : α) x‖) (∑' (a : { x : α // x ∉ t }), u (↑a : α))
⊢ norm.{u_3} (E := F) (∑' (x_1 : { x : α // x ∉ t }), f (↑x_1 : α) x) ≤ ∑' (a : { x : α // x ∉ t }), u (↑a : α)

Tactic:
apply (norm_tsum_le_tsum_norm (A.subtype _)).trans

Premises used: Summable.subtype, norm_tsum_le_tsum_norm, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
t : Finset α
ht : ∑' (a : { x : α // x ∉ t }), u (↑a : α) < ε
x : β
hx : x ∈ s
A : Summable (α := ℝ) fun (n : α) ↦ ‖f n x‖
⊢ LE.le (α := ℝ) (∑' (i : { x : α // x ∉ t }), ‖f (↑i : α) x‖) (∑' (a : { x : α // x ∉ t }), u (↑a : α))

Tactic:
(A.subtype _).tsum_le_tsum (fun n => hfu _ _ hx) (hu.subtype _)

Premises used: Summable.subtype, Summable.tsum_le_tsum, Subtype.val
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
s : Set β
hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
t : Finset α
ht : ∑' (a : { x : α // x ∉ t }), u (↑a : α) < ε
x : β
hx : x ∈ s
A : Summable (α := ℝ) fun (n : α) ↦ ‖f n x‖
⊢ LE.le (α := ℝ) (∑' (i : { x : α // x ∉ t }), ‖f (↑i : α) x‖) (∑' (a : { x : α // x ∉ t }), u (↑a : α))

Tactic:
exact (A.subtype _).tsum_le_tsum (fun n => hfu _ _ hx) (hu.subtype _)

Premises used: Summable.subtype, Summable.tsum_le_tsum
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
Goal:
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
f : ℕ → β → F
u : ℕ → ℝ
hu : Summable u
s : Set β
hfu : ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ u n
⊢ TendstoUniformlyOn.{u_2, u_3, 0} (β := F) (fun (N : ℕ) (x : β) ↦ ∑ n ∈ Finset.range N, f n x)
    (fun (x : β) ↦ ∑' (n : ℕ), f n x) atTop s

Tactic:
fun v hv => tendsto_finset_range.eventually (tendstoUniformlyOn_tsum hu hfu v hv)

Premises used: Set.Mem, tendstoUniformlyOn_tsum, TendstoUniformlyOn, Filter.tendsto_finset_range, Filter.Tendsto.eventually
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
Goal:
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
s : Set β
hfu : ∀ᶠ (n : ι) in cofinite, ∀ x ∈ s, ‖f n x‖ ≤ u n
⊢ TendstoUniformlyOn.{u_2, u_3, u_4} (β := F) (fun (t : Finset ι) (x : β) ↦ ∑ n ∈ t, f n x)
    (fun (x : β) ↦ ∑' (n : ι), f n x) atTop s

Tactic:
tendstoUniformlyOn_iff.2 fun ε εpos => ?_

Premises used: Iff.mpr, Metric.tendstoUniformlyOn_iff
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
Goal:
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
s : Set β
hfu : ∀ᶠ (n : ι) in cofinite, ∀ x ∈ s, ‖f n x‖ ≤ u n
refine :
  ∀ (ε : ℝ) (εpos : ε > 0),
    ∀ᶠ (n : Finset ι) in atTop, ∀ x ∈ s, dist.{u_3} (α := F) (∑' (n : ι), f n x) (∑ n ∈ n, f n x) < ε
⊢ TendstoUniformlyOn.{u_2, u_3, u_4} (β := F) (fun (t : Finset ι) (x : β) ↦ ∑ n ∈ t, f n x)
    (fun (x : β) ↦ ∑' (n : ι), f n x) atTop s

Tactic:
refine tendstoUniformlyOn_iff.2 fun ε εpos => ?_

Premises used: Iff.mpr, Metric.tendstoUniformlyOn_iff
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
Goal:
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
s : Set β
hfu : ∀ᶠ (n : ι) in cofinite, ∀ x ∈ s, ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
⊢ ∀ᶠ (b : Finset ι) in atTop, ∑' (a : { x : ι // x ∉ b }), u (↑a : ι) < ε

Tactic:
have := (tendsto_order.1 (tendsto_tsum_compl_atTop_zero u)).2 _ εpos
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
Goal:
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
s : Set β
hfu : ∀ᶠ (n : ι) in cofinite, ∀ x ∈ s, ‖f n x‖ ≤ u n
ε : ℝ
εpos : ε > 0
this : ∀ᶠ (b : Finset ι) in atTop, ∑' (a : { x : ι // x ∉ b }), u (↑a : ι) < ε
simp :
  ∀ (εpos : 0 < ε) (this : ∃ (a : Finset ι), ∀ (b : Finset ι), a ⊆ b → ∑' (a : { x : ι // x ∉ b }), u (↑a : ι) < ε),
    ∃ (a : Finset ι), ∀ (b : Finset ι), a ⊆ b → ∀ x ∈ s, dist.{u_3} (α := F) (∑' (n : ι), f n x) (∑ n ∈ b, f n x) < ε
⊢ ∀ᶠ (n : Finset ι) in atTop, ∀ x ∈ s, dist.{u_3} (α := F) (∑' (n : ι), f n x) (∑ n ∈ n, f n x) < ε

Tactic:
simp only [gt_iff_lt,
    eventually_atTop, ge_iff_le, Finset.le_eq_subset] at *

Premises used: ge_iff_le, Finset.le_eq_subset, gt_iff_lt, Filter.eventually_atTop
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
Goal:
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
s : Set β
hfu : ∀ᶠ (n : ι) in cofinite, ∀ x ∈ s, ‖f n x‖ ≤ u n
ε : ℝ
εpos : 0 < ε
this : ∃ (a : Finset ι), ∀ (b : Finset ι), a ⊆ b → ∑' (a : { x : ι // x ∉ b }), u (↑a : ι) < ε
obtain :
  ∀ (t : Finset ι) (ht : ∀ (b : Finset ι), t ⊆ b → ∑' (a : { x : ι // x ∉ b }), u (↑a : ι) < ε),
    ∃ (a : Finset ι), ∀ (b : Finset ι), a ⊆ b → ∀ x ∈ s, dist.{u_3} (α := F) (∑' (n : ι), f n x) (∑ n ∈ b, f n x) < ε
⊢ ∃ (a : Finset ι), ∀ (b : Finset ι), a ⊆ b → ∀ x ∈ s, dist.{u_3} (α := F) (∑' (n : ι), f n x) (∑ n ∈ b, f n x) < ε

Tactic:
obtain ⟨t, ht⟩ := this
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
Goal:
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
s : Set β
hfu : ∀ᶠ (n : ι) in cofinite, ∀ x ∈ s, ‖f n x‖ ≤ u n
ε : ℝ
εpos : 0 < ε
t : Finset ι
ht : ∀ (b : Finset ι), t ⊆ b → ∑' (a : { x : ι // x ∉ b }), u (↑a : ι) < ε
rw :
  ∀ (hfu : ∃ (v : Set ι), Membership.mem (γ := Filter ι) cofinite v ∧ ∀ y ∈ v, ∀ x ∈ s, ‖f y x‖ ≤ u y) (ε : ℝ)
    (εpos : 0 < ε) (t : Finset ι) (ht : ∀ (b : Finset ι), t ⊆ b → ∑' (a : { x : ι // x ∉ b }), u (↑a : ι) < ε),
    ∃ (a : Finset ι), ∀ (b : Finset ι), a ⊆ b → ∀ x ∈ s, dist.{u_3} (α := F) (∑' (n : ι), f n x) (∑ n ∈ b, f n x) < ε
⊢ ∃ (a : Finset ι), ∀ (b : Finset ι), a ⊆ b → ∀ x ∈ s, dist.{u_3} (α := F) (∑' (n : ι), f n x) (∑ n ∈ b, f n x) < ε

Tactic:
rw [eventually_iff_exists_mem] at hfu

Premises used: Filter.eventually_iff_exists_mem
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
Goal:
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
s : Set β
hfu : ∃ (v : Set ι), Membership.mem (γ := Filter ι) cofinite v ∧ ∀ y ∈ v, ∀ x ∈ s, ‖f y x‖ ≤ u y
ε : ℝ
εpos : 0 < ε
t : Finset ι
ht : ∀ (b : Finset ι), t ⊆ b → ∑' (a : { x : ι // x ∉ b }), u (↑a : ι) < ε
obtain :
  ∀ (N : Set ι) (hN : Membership.mem (γ := Filter ι) cofinite N) (HN : ∀ y ∈ N, ∀ x ∈ s, ‖f y x‖ ≤ u y),
    ∃ (a : Finset ι), ∀ (b : Finset ι), a ⊆ b → ∀ x ∈ s, dist.{u_3} (α := F) (∑' (n : ι), f n x) (∑ n ∈ b, f n x) < ε
⊢ ∃ (a : Finset ι), ∀ (b : Finset ι), a ⊆ b → ∀ x ∈ s, dist.{u_3} (α := F) (∑' (n : ι), f n x) (∑ n ∈ b, f n x) < ε

Tactic:
obtain ⟨N, hN, HN⟩ := hfu
-- Module: Mathlib.Analysis.Normed.Group.FunctionSeries
Goal:
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
s : Set β
ε : ℝ
εpos : 0 < ε
t : Finset ι
ht : ∀ (b : Finset ι), t ⊆ b → ∑' (a : { x : ι // x ∉ b }), u (↑a : ι) < ε
N : Set ι
hN : Membership.mem (γ := Filter ι) cofinite N
HN : ∀ y ∈ N, ∀ x ∈ s, ‖f y x‖ ≤ u y
⊢ ∃ (a : Finset ι), ∀ (b : Finset ι), a ⊆ b → ∀ x ∈ s, dist.{u_3} (α := F) (∑' (n : ι), f n x) (∑ n ∈ b, f n x) < ε

Tactic:
⟨hN.toFinset ∪ t, fun n hn x hx => ?_⟩

Premises used: Set.Finite.toFinset, Exists.intro, Union.union