awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
s : Set E
hx : x ∈ s
hs : s ≠ univ
y : E
hys : y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] sᶜ
hyd : infDist x sᶜ = dist x y
hys₁ : y ∈ (interior s)ᶜ
⊢ infDist x sᶜ = dist x y

Tactic:
rw [closure_compl] at hys

Premises used: closure_compl
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
s : Set E
hx : x ∈ s
hs : s ≠ univ
y : E
hys : y ∈ (interior s)ᶜ
hyd : infDist x sᶜ = dist x y
⊢ ∃ y ∈ frontier s, infDist x sᶜ = dist x y

Tactic:
⟨y, ⟨Metric.closedBall_infDist_compl_subset_closure hx <|
    Metric.mem_closedBall.2 <| ge_of_eq ?_, hys⟩, hyd⟩

Premises used: Iff.mpr, ge_of_eq, And.intro, Exists.intro, Metric.mem_closedBall, Metric.closedBall_infDist_compl_subset_closure
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
s : Set E
hx : x ∈ s
hs : s ≠ univ
y : E
hys : y ∈ (interior s)ᶜ
hyd : infDist x sᶜ = dist x y
refine : infDist x sᶜ = dist y x
⊢ ∃ y ∈ frontier s, infDist x sᶜ = dist x y

Tactic:
refine ⟨y, ⟨Metric.closedBall_infDist_compl_subset_closure hx <|
    Metric.mem_closedBall.2 <| ge_of_eq ?_, hys⟩, hyd⟩
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
s : Set E
hx : x ∈ s
hs : s ≠ univ
y : E
hys : y ∈ (interior s)ᶜ
hyd rwa rwa₁ rwa₂ rwa₃ : infDist x sᶜ = dist x y
⊢ infDist x sᶜ = dist y x

Tactic:
rwa [dist_comm]

Premises used: dist_comm
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
rw : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K
⊢ x ∈ interior K ∪ frontier K

Tactic:
rw [← closure_eq_interior_union_frontier]

Premises used: closure_eq_interior_union_frontier
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
⊢ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K

Tactic:
subset_closure hx

Premises used: subset_closure
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
⊢ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K

Tactic:
exact subset_closure hx

Premises used: subset_closure
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
inl : ∀ (hx' : x ∈ interior K), ∃ y ∈ frontier K, infDist x Kᶜ = dist x y
inr : ∀ (hx' : x ∈ frontier K), ∃ y ∈ frontier K, infDist x Kᶜ = dist x y
⊢ ∃ y ∈ frontier K, infDist x Kᶜ = dist x y

Tactic:
obtain hx' | hx' : x ∈ interior K ∪ frontier K := by
    rw [← closure_eq_interior_union_frontier]
    exact subset_closure hx

Premises used: frontier, interior
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
hx' : x ∈ interior K
⊢ ∃ (i : ℝ), 0 < i ∧ closedBall x i ⊆ K

Tactic:
rw [mem_interior_iff_mem_nhds, Metric.nhds_basis_closedBall.mem_iff] at hx'

Premises used: mem_interior_iff_mem_nhds, Filter.HasBasis.mem_iff, Metric.nhds_basis_closedBall
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
hx' : ∃ (i : ℝ), 0 < i ∧ closedBall x i ⊆ K
inl : ∀ (r : ℝ) (hr₀ : 0 < r) (hrK : closedBall x r ⊆ K), ∃ y ∈ frontier K, infDist x Kᶜ = dist x y
⊢ ∃ y ∈ frontier K, infDist x Kᶜ = dist x y

Tactic:
rcases hx' with ⟨r, hr₀, hrK⟩
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
r : ℝ
hr₀ : 0 < r
hrK : closedBall x r ⊆ K
⊢ FiniteDimensional ℝ E

Tactic:
have : FiniteDimensional ℝ E :=
      .of_isCompact_closedBall ℝ hr₀
        (hK.of_isClosed_subset Metric.isClosed_closedBall hrK)
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
r : ℝ
hr₀ : 0 < r
hrK : closedBall x r ⊆ K
this : FiniteDimensional ℝ E
⊢ ∃ y ∈ frontier K, infDist x Kᶜ = dist x y

Tactic:
exists_mem_frontier_infDist_compl_eq_dist hx hK.ne_univ

Premises used: IsCompact.ne_univ, exists_mem_frontier_infDist_compl_eq_dist
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
r : ℝ
hr₀ : 0 < r
hrK : closedBall x r ⊆ K
this : FiniteDimensional ℝ E
⊢ ∃ y ∈ frontier K, infDist x Kᶜ = dist x y

Tactic:
exact exists_mem_frontier_infDist_compl_eq_dist hx hK.ne_univ
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
hx' : x ∈ frontier K
⊢ ∃ y ∈ frontier K, infDist x Kᶜ = dist x y

Tactic:
⟨x, hx', ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
hx' : x ∈ frontier K
inr : infDist x Kᶜ = dist x x
⊢ ∃ y ∈ frontier K, infDist x Kᶜ = dist x y

Tactic:
refine ⟨x, hx', ?_⟩
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
hx' : x ∈ frontier K
⊢ x ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K ∩
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Kᶜ

Tactic:
rw [frontier_eq_closure_inter_closure] at hx'

Premises used: frontier_eq_closure_inter_closure
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
hx' :
  x ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K ∩
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Kᶜ
inr : 0 = dist x x
inr₁ inr₂ : Eq (α := ℝ) 0 0
⊢ infDist x Kᶜ = dist x x

Tactic:
rw [Metric.infDist_zero_of_mem_closure hx'.2, dist_self]

Premises used: dist_self, And.right, Metric.infDist_zero_of_mem_closure
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
f : α → E
⊢ (Summable (α := ℝ) fun (x : α) ↦ ‖f x‖) ↔ Summable f

Tactic:
⟨Summable.of_norm, fun hf ↦ ?_⟩

Premises used: Summable.of_norm, Iff.intro
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
f : α → E
refine : ∀ (hf : Summable f), Summable (α := ℝ) fun (x : α) ↦ ‖f x‖
⊢ (Summable (α := ℝ) fun (x : α) ↦ ‖f x‖) ↔ Summable f

Tactic:
refine ⟨Summable.of_norm, fun hf ↦ ?_⟩
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
f : α → E
hf : Summable f
this : ∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable (α := ℝ) fun (x : α) ↦ ‖g x‖
obtain : ∀ (v : Basis (Fin (finrank ℝ E)) ℝ E), Summable (α := ℝ) fun (x : α) ↦ ‖f x‖
⊢ Summable (α := ℝ) fun (x : α) ↦ ‖f x‖

Tactic:
obtain v := Module.finBasis ℝ E

Premises used: Real, Module.finBasis
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
f : α → E
hf : Summable f
this : ∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable (α := ℝ) fun (x : α) ↦ ‖g x‖
v : Basis (Fin (finrank ℝ E)) ℝ E
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := v.equivFunL
⊢ Summable (α := ℝ) fun (x : α) ↦
    norm (E := Fin (finrank ℝ E) → ℝ) ((e : (a : E) → Fin (finrank ℝ E) → ℝ) (f x) : Fin (finrank ℝ E) → ℝ)

Tactic:
have H : Summable fun x => ‖e (f x)‖ := this (e.summable.2 hf)
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
f : α → E
hf : Summable f
this : ∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable (α := ℝ) fun (x : α) ↦ ‖g x‖
v : Basis (Fin (finrank ℝ E)) ℝ E
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := v.equivFunL
H :
  Summable (α := ℝ) fun (x : α) ↦
    norm (E := Fin (finrank ℝ E) → ℝ) ((e : (a : E) → Fin (finrank ℝ E) → ℝ) (f x) : Fin (finrank ℝ E) → ℝ)
⊢ Summable (α := ℝ) fun (x : α) ↦ ‖f x‖

Tactic:
.of_norm_bounded (H.mul_left ↑‖(e.symm : (Fin (finrank ℝ E) → ℝ) →L[ℝ] E)‖₊) fun i ↦ ?_

Premises used: Summable.mul_left, Summable.of_norm_bounded
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
f : α → E
hf : Summable f
this : ∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable (α := ℝ) fun (x : α) ↦ ‖g x‖
v : Basis (Fin (finrank ℝ E)) ℝ E
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := v.equivFunL
H :
  Summable (α := ℝ) fun (x : α) ↦
    norm (E := Fin (finrank ℝ E) → ℝ) ((e : (a : E) → Fin (finrank ℝ E) → ℝ) (f x) : Fin (finrank ℝ E) → ℝ)
refine :
  ∀ (i : α),
    ‖‖f i‖‖ ≤
      (↑‖(↑e.symm : (Fin (finrank ℝ E) → ℝ) →L[ℝ] E)‖₊ : ℝ) *
        norm (E := Fin (finrank ℝ E) → ℝ) ((e : (a : E) → Fin (finrank ℝ E) → ℝ) (f i) : Fin (finrank ℝ E) → ℝ)
⊢ Summable (α := ℝ) fun (x : α) ↦ ‖f x‖

Tactic:
refine .of_norm_bounded (H.mul_left ↑‖(e.symm : (Fin (finrank ℝ E) → ℝ) →L[ℝ] E)‖₊) fun i ↦ ?_
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
f : α → E
hf : Summable f
this : ∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable (α := ℝ) fun (x : α) ↦ ‖g x‖
v : Basis (Fin (finrank ℝ E)) ℝ E
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := v.equivFunL
H :
  Summable (α := ℝ) fun (x : α) ↦
    norm (E := Fin (finrank ℝ E) → ℝ) ((e : (a : E) → Fin (finrank ℝ E) → ℝ) (f x) : Fin (finrank ℝ E) → ℝ)
i : α
⊢ ‖‖f i‖‖ ≤
    (↑‖(↑e.symm : (Fin (finrank ℝ E) → ℝ) →L[ℝ] E)‖₊ : ℝ) *
      norm (E := Fin (finrank ℝ E) → ℝ) ((e : (a : E) → Fin (finrank ℝ E) → ℝ) (f i) : Fin (finrank ℝ E) → ℝ)

Tactic:
simpa using (e.symm : (Fin (finrank ℝ E) → ℝ) →L[ℝ] E).le_opNorm (e <| f i)

Premises used: ContinuousLinearEquiv.symm, ContinuousLinearMap.le_opNorm, DFunLike.coe, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
f : α → E
hf : Summable f
suffices : ∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable (α := ℝ) fun (x : α) ↦ ‖g x‖
⊢ Summable (α := ℝ) fun (x : α) ↦ ‖f x‖

Tactic:
suffices ∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable fun x => ‖g x‖ by
    obtain v := Module.finBasis ℝ E
    set e := v.equivFunL
    have H : Summable fun x => ‖e (f x)‖ := this (e.summable.2 hf)
    refine .of_norm_bounded (H.mul_left ↑‖(e.symm : (Fin (finrank ℝ E) → ℝ) →L[ℝ] E)‖₊) fun i ↦ ?_
    simpa using (e.symm : (Fin (finrank ℝ E) → ℝ) →L[ℝ] E).le_opNorm (e <| f i)
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
α : Type u_1
N : ℕ
g : α → Fin N → ℝ
hg : Summable g
⊢ ∀ (i : Fin N), Summable (α := ℝ) fun (x : α) ↦ ‖g x i‖

Tactic:
have : ∀ i, Summable fun x => ‖g x i‖ := fun i => (Pi.summable.1 hg i).abs
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
α : Type u_1
N : ℕ
g : α → Fin N → ℝ
hg : Summable g
this : ∀ (i : Fin N), Summable (α := ℝ) fun (x : α) ↦ ‖g x i‖
⊢ Summable (α := ℝ) fun (x : α) ↦ ‖g x‖

Tactic:
.of_norm_bounded (summable_sum fun i (_ : i ∈ Finset.univ) => this i) fun x => ?_

Premises used: summable_sum, Summable.of_norm_bounded
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
α : Type u_1
N : ℕ
g : α → Fin N → ℝ
hg : Summable g
this : ∀ (i : Fin N), Summable (α := ℝ) fun (x : α) ↦ ‖g x i‖
refine : ∀ (x : α), ‖‖g x‖‖ ≤ ∑ i : Fin N, ‖g x i‖
⊢ Summable (α := ℝ) fun (x : α) ↦ ‖g x‖

Tactic:
refine .of_norm_bounded (summable_sum fun i (_ : i ∈ Finset.univ) => this i) fun x => ?_
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
α : Type u_1
N : ℕ
g : α → Fin N → ℝ
hg : Summable g
this : ∀ (i : Fin N), Summable (α := ℝ) fun (x : α) ↦ ‖g x i‖
x : α
rw : ∀ (i : Fin N), ‖g x i‖ ≤ ∑ i : Fin N, ‖g x i‖
rw₁ : LE.le (α := ℝ) 0 (∑ i : Fin N, ‖g x i‖)
⊢ ‖‖g x‖‖ ≤ ∑ i : Fin N, ‖g x i‖

Tactic:
rw [norm_norm, pi_norm_le_iff_of_nonneg]

Premises used: pi_norm_le_iff_of_nonneg, norm_norm
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
α : Type u_1
N : ℕ
g : α → Fin N → ℝ
hg : Summable g
this : ∀ (i : Fin N), Summable (α := ℝ) fun (x : α) ↦ ‖g x i‖
x : α
⊢ ∀ (i : Fin N), ‖g x i‖ ≤ ∑ i : Fin N, ‖g x i‖

Tactic:
fun i => Finset.single_le_sum (f := fun i => ‖g x i‖) (fun i _ => ?_) (Finset.mem_univ i)

Premises used: Finset.mem_univ, Finset.single_le_sum
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
α : Type u_1
N : ℕ
g : α → Fin N → ℝ
hg : Summable g
this : ∀ (i : Fin N), Summable (α := ℝ) fun (x : α) ↦ ‖g x i‖
x : α
refine :
  ∀ (i i : Fin N), Membership.mem (γ := Finset (Fin N)) Finset.univ i → LE.le (α := ℝ) 0 ((fun (i : Fin N) ↦ ‖g x i‖) i)
⊢ ∀ (i : Fin N), ‖g x i‖ ≤ ∑ i : Fin N, ‖g x i‖

Tactic:
refine fun i => Finset.single_le_sum (f := fun i => ‖g x i‖) (fun i _ => ?_) (Finset.mem_univ i)

Premises used: Finset.mem_univ, Finset.single_le_sum
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
α : Type u_1
N : ℕ
g : α → Fin N → ℝ
hg : Summable g
this : ∀ (i : Fin N), Summable (α := ℝ) fun (x : α) ↦ ‖g x i‖
x : α
i_1 i : Fin N
h : Membership.mem (γ := Finset (Fin N)) Finset.univ i
⊢ LE.le (α := ℝ) 0 ((fun (i : Fin N) ↦ ‖g x i‖) i)

Tactic:
norm_nonneg (g x i)

Premises used: norm_nonneg
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
α : Type u_1
N : ℕ
g : α → Fin N → ℝ
hg : Summable g
this : ∀ (i : Fin N), Summable (α := ℝ) fun (x : α) ↦ ‖g x i‖
x : α
i_1 i : Fin N
h : Membership.mem (γ := Finset (Fin N)) Finset.univ i
⊢ LE.le (α := ℝ) 0 ((fun (i : Fin N) ↦ ‖g x i‖) i)

Tactic:
exact norm_nonneg (g x i)

Premises used: norm_nonneg
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
α : Type u_1
N : ℕ
g : α → Fin N → ℝ
hg : Summable g
this : ∀ (i : Fin N), Summable (α := ℝ) fun (x : α) ↦ ‖g x i‖
x : α
⊢ LE.le (α := ℝ) 0 (∑ i : Fin N, ‖g x i‖)

Tactic:
Finset.sum_nonneg fun _ _ => norm_nonneg _

Premises used: Finset.sum_nonneg, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
α : Type u_1
N : ℕ
g : α → Fin N → ℝ
hg : Summable g
this : ∀ (i : Fin N), Summable (α := ℝ) fun (x : α) ↦ ‖g x i‖
x : α
⊢ LE.le (α := ℝ) 0 (∑ i : Fin N, ‖g x i‖)

Tactic:
exact Finset.sum_nonneg fun _ _ => norm_nonneg _

Premises used: Finset.sum_nonneg, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
c : ℝ
f : ℕ → E
h : ∀ (n : ℕ), ∑ i ∈ Finset.range n, ‖f i‖ ≤ c
⊢ Summable f

Tactic:
summable_norm_iff.mp <| summable_of_sum_range_le (fun _ ↦ norm_nonneg _) h

Premises used: Iff.mp, summable_norm_iff, summable_of_sum_range_le, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
ι : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : FiniteDimensional ℝ F
f : ι → E
g : ι → F
hg : Summable g
h : f =O[cofinite] g
⊢ Summable f

Tactic:
summable_of_isBigO hg.norm h.norm_right

Premises used: Summable.norm, summable_of_isBigO, Asymptotics.IsBigO.norm_right
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
ι : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : CompleteSpace F
f : E → F
hf : f =O[𝓝 0] id
g : ι → E
hg : Summable g
⊢ Summable (f ∘ g)

Tactic:
.of_norm <| hf.comp_summable_norm hg.norm

Premises used: Summable.of_norm, Asymptotics.IsBigO.comp_summable_norm, Summable.norm
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : FiniteDimensional ℝ F
f : ℕ → E
g : ℕ → F
hg : Summable g
h : f =O[atTop] g
⊢ Summable f

Tactic:
summable_of_isBigO_nat hg.norm h.norm_right

Premises used: Summable.norm, Asymptotics.IsBigO.norm_right, summable_of_isBigO_nat
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormOneClass F
inst_2 : NormMulClass F
k : ℕ
r : F
hr : ‖r‖ < 1
u : ℕ → F
hu : IsBigO (F := F) atTop u fun (n : ℕ) ↦ (↑(n ^ k) : F)
rcases : ∀ (r' : ℝ) (hrr' : ‖r‖ < r') (h : r' < 1), Summable (α := ℝ) fun (n : ℕ) ↦ ‖u n * r ^ n‖
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖u n * r ^ n‖

Tactic:
rcases exists_between hr with ⟨r', hrr', h⟩

Premises used: exists_between
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormOneClass F
inst_2 : NormMulClass F
k : ℕ
r : F
hr : ‖r‖ < 1
u : ℕ → F
hu : IsBigO (F := F) atTop u fun (n : ℕ) ↦ (↑(n ^ k) : F)
r' : ℝ
hrr' : ‖r‖ < r'
h : r' < 1
apply : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖u n * r ^ n‖) fun (x : ℕ) ↦ ‖r' ^ x‖
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖u n * r ^ n‖

Tactic:
apply summable_of_isBigO_nat (summable_geometric_of_lt_one ((norm_nonneg _).trans hrr'.le) h).norm

Premises used: LT.lt.le, Summable.norm, LE.le.trans, summable_geometric_of_lt_one, norm_nonneg, summable_of_isBigO_nat
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormOneClass F
inst_2 : NormMulClass F
k : ℕ
r : F
hr : ‖r‖ < 1
u : ℕ → F
hu : IsBigO (F := F) atTop u fun (n : ℕ) ↦ (↑(n ^ k) : F)
r' : ℝ
hrr' : ‖r‖ < r'
h : r' < 1
apply : ∀ᶠ (x : ℕ) in atTop, ‖‖u x * r ^ x‖‖ ≤ norm (E := ℝ) 1 * ‖‖u x‖ * ‖r‖ ^ x‖
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖u n * r ^ n‖) fun (n : ℕ) ↦ ‖u n‖ * ‖r‖ ^ n

Tactic:
apply (IsBigOWith.of_bound (c := ‖(1 : ℝ)‖) ?_).isBigO

Premises used: Asymptotics.IsBigOWith.isBigO, Asymptotics.IsBigOWith.of_bound
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormOneClass F
inst_2 : NormMulClass F
k : ℕ
r : F
hr : ‖r‖ < 1
u : ℕ → F
hu : IsBigO (F := F) atTop u fun (n : ℕ) ↦ (↑(n ^ k) : F)
r' : ℝ
hrr' : ‖r‖ < r'
h : r' < 1
h₁ : ∀ (n : ℕ) (hn : ‖r ^ n‖ ≤ ‖r‖ ^ n), ‖‖u n * r ^ n‖‖ ≤ norm (E := ℝ) 1 * ‖‖u n‖ * ‖r‖ ^ n‖
⊢ ∀ᶠ (x : ℕ) in atTop, ‖‖u x * r ^ x‖‖ ≤ norm (E := ℝ) 1 * ‖‖u x‖ * ‖r‖ ^ x‖

Tactic:
filter_upwards [eventually_norm_pow_le r] with n hn

Premises used: eventually_norm_pow_le
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormOneClass F
inst_2 : NormMulClass F
k : ℕ
r : F
hr : ‖r‖ < 1
u : ℕ → F
hu : IsBigO (F := F) atTop u fun (n : ℕ) ↦ (↑(n ^ k) : F)
r' : ℝ
hrr' : ‖r‖ < r'
h : r' < 1
n : ℕ
hn : ‖r ^ n‖ ≤ ‖r‖ ^ n
⊢ ‖‖u n * r ^ n‖‖ ≤ norm (E := ℝ) 1 * ‖‖u n‖ * ‖r‖ ^ n‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormOneClass F
inst_2 : NormMulClass F
k : ℕ
r : F
hr : ‖r‖ < 1
u : ℕ → F
hu : IsBigO (F := F) atTop u fun (n : ℕ) ↦ (↑(n ^ k) : F)
r' : ℝ
hrr' : ‖r‖ < r'
h : r' < 1
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖u n‖ * ‖r‖ ^ n) fun (n : ℕ) ↦ ‖HPow.hPow (α := F) (↑n : F) k‖ * ‖r‖ ^ n

Tactic:
simpa [Nat.cast_pow] using
      (isBigO_norm_left.mpr (isBigO_norm_right.mpr hu)).mul (isBigO_refl (fun n ↦ (‖r‖ ^ n)) atTop)

Premises used: Iff.mpr, Norm.norm, Asymptotics.isBigO_norm_right, Asymptotics.IsBigO.mul, Filter.atTop, Asymptotics.isBigO_norm_left, HPow.hPow, Nat.cast_pow, Asymptotics.isBigO_refl
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormOneClass F
inst_2 : NormMulClass F
k : ℕ
r : F
hr : ‖r‖ < 1
u : ℕ → F
hu : IsBigO (F := F) atTop u fun (n : ℕ) ↦ (↑(n ^ k) : F)
r' : ℝ
hrr' : ‖r‖ < r'
h : r' < 1
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℕ) ↦ ‖HPow.hPow (α := F) (↑x : F) k * r ^ x‖) fun (x : ℕ) ↦ ‖r' ^ x‖

Tactic:
isBigO_norm_right.mpr
          (isBigO_norm_left.mpr
            (isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt k hrr').isBigO)

Premises used: Iff.mpr, Asymptotics.isBigO_norm_right, Asymptotics.IsLittleO.isBigO, Asymptotics.isBigO_norm_left, isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormOneClass F
inst_2 : NormMulClass F
k : ℕ
r : F
hr : ‖r‖ < 1
u : ℕ → F
hu : IsBigO (F := F) atTop u fun (n : ℕ) ↦ (↑(n ^ k) : F)
r' : ℝ
hrr' : ‖r‖ < r'
h : r' < 1
h₁ : ∀ (x : ℕ), ‖HPow.hPow (α := F) (↑x : F) k‖ * ‖r‖ ^ x = ‖HPow.hPow (α := F) (↑x : F) k * r ^ x‖
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖HPow.hPow (α := F) (↑n : F) k‖ * ‖r‖ ^ n) fun (n : ℕ) ↦ ‖r' ^ n‖

Tactic:
convert!
        isBigO_norm_right.mpr
          (isBigO_norm_left.mpr
            (isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt k hrr').isBigO)

Premises used: Iff.mpr, Asymptotics.isBigO_norm_right, Asymptotics.IsLittleO.isBigO, Asymptotics.isBigO_norm_left, isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormOneClass F
inst_2 : NormMulClass F
k : ℕ
r : F
hr : ‖r‖ < 1
u : ℕ → F
hu : IsBigO (F := F) atTop u fun (n : ℕ) ↦ (↑(n ^ k) : F)
r' : ℝ
hrr' : ‖r‖ < r'
h : r' < 1
x : ℕ
⊢ ‖HPow.hPow (α := F) (↑x : F) k‖ * ‖r‖ ^ x = ‖HPow.hPow (α := F) (↑x : F) k * r ^ x‖

Tactic:
simp only [norm_pow, norm_mul]

Premises used: norm_pow, norm_mul
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
F : Type u_1
inst : NormedRing F
inst_1 : NormOneClass F
inst_2 : NormMulClass F
k : ℕ
r : F
hr : ‖r‖ < 1
u : ℕ → F
hu : IsBigO (F := F) atTop u fun (n : ℕ) ↦ (↑(n ^ k) : F)
r' : ℝ
hrr' : ‖r‖ < r'
h : r' < 1
fun : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖u n * r ^ n‖) fun (n : ℕ) ↦ ‖u n‖ * ‖r‖ ^ n
fun₁ :
  IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖u n‖ * ‖r‖ ^ n) fun (n : ℕ) ↦ ‖HPow.hPow (α := F) (↑n : F) k‖ * ‖r‖ ^ n
fun₂ : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖HPow.hPow (α := F) (↑n : F) k‖ * ‖r‖ ^ n) fun (n : ℕ) ↦ ‖r' ^ n‖
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖u n * r ^ n‖) fun (x : ℕ) ↦ ‖r' ^ x‖

Tactic:
calc
  fun n ↦ ‖(u n) * r ^ n‖
  _ =O[atTop] fun n ↦ ‖u n‖ * ‖r‖ ^ n := by
      apply (IsBigOWith.of_bound (c := ‖(1 : ℝ)‖) ?_).isBigO
      filter_upwards [eventually_norm_pow_le r] with n hn
      simp
  _ =O[atTop] fun n ↦ ‖((n : F) ^ k)‖ * ‖r‖ ^ n := by
      simpa [Nat.cast_pow] using
      (isBigO_norm_left.mpr (isBigO_norm_right.mpr hu)).mul (isBigO_refl (fun n ↦ (‖r‖ ^ n)) atTop)
  _ =O[atTop] fun n ↦ ‖r' ^ n‖ := by
      convert!
        isBigO_norm_right.mpr
          (isBigO_norm_left.mpr
            (isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt k hrr').isBigO)
      simp only [norm_pow, norm_mul]

Premises used: Norm.norm, HMul.hMul, Filter.atTop, HPow.hPow