awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.RadiusLiminf
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this :
  ∀ (r : ℝ≥0) {n : ℕ},
    0 < n → ((↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ↔ ‖p n‖₊ * r ^ n ≤ 1)
⊢ liminf (fun (n : ℕ) ↦ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop ≤ p.radius

Tactic:
ENNReal.le_of_forall_nnreal_lt fun r hr => ?_

Premises used: ENNReal.le_of_forall_nnreal_lt
-- Module: Mathlib.Analysis.Analytic.RadiusLiminf
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this :
  ∀ (r : ℝ≥0) {n : ℕ},
    0 < n → ((↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ↔ ‖p n‖₊ * r ^ n ≤ 1)
a :
  ∀ (r : ℝ≥0) (hr : (↑r : ℝ≥0∞) < liminf (fun (n : ℕ) ↦ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop),
    (↑r : ℝ≥0∞) ≤ p.radius
⊢ liminf (fun (n : ℕ) ↦ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop ≤ p.radius

Tactic:
refine ENNReal.le_of_forall_nnreal_lt fun r hr => ?_

Premises used: ENNReal.le_of_forall_nnreal_lt
-- Module: Mathlib.Analysis.Analytic.RadiusLiminf
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this :
  ∀ (r : ℝ≥0) {n : ℕ},
    0 < n → ((↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
⊢ ∃ (a : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) a ∧ ∀ᶠ (n : ℕ) in atTop, |‖p n‖ * (↑r : ℝ) ^ n| ≤ a ^ n

Tactic:
have := ((TFAE_exists_lt_isLittleO_pow (fun n => ‖p n‖ * r ^ n) 1).out 1 7).1
      (p.isLittleO_of_lt_radius hr)
-- Module: Mathlib.Analysis.Analytic.RadiusLiminf
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this_1 :
  ∀ (r : ℝ≥0) {n : ℕ},
    0 < n → ((↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
this : ∃ (a : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) a ∧ ∀ᶠ (n : ℕ) in atTop, |‖p n‖ * (↑r : ℝ) ^ n| ≤ a ^ n
a :
  ∀ (a : ℝ) (ha : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) a)
    (H : ∀ᶠ (n : ℕ) in atTop, |‖p n‖ * (↑r : ℝ) ^ n| ≤ a ^ n),
    (↑r : ℝ≥0∞) ≤ liminf (fun (n : ℕ) ↦ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop
⊢ (↑r : ℝ≥0∞) ≤ liminf (fun (n : ℕ) ↦ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop

Tactic:
obtain ⟨a, ha, H⟩ := this
-- Module: Mathlib.Analysis.Analytic.RadiusLiminf
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this :
  ∀ (r : ℝ≥0) {n : ℕ},
    0 < n → ((↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) a
H : ∀ᶠ (n : ℕ) in atTop, |‖p n‖ * (↑r : ℝ) ^ n| ≤ a ^ n
a₁ :
  autoParam
    (IsCoboundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦
      1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞))
    le_liminf_of_le._auto_1
a₂ : ∀ᶠ (n : ℕ) in atTop, (↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)
⊢ (↑r : ℝ≥0∞) ≤ liminf (fun (n : ℕ) ↦ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop

Tactic:
apply le_liminf_of_le

Premises used: Filter.le_liminf_of_le
-- Module: Mathlib.Analysis.Analytic.RadiusLiminf
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this :
  ∀ (r : ℝ≥0) {n : ℕ},
    0 < n → ((↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) a
H : ∀ᶠ (n : ℕ) in atTop, |‖p n‖ * (↑r : ℝ) ^ n| ≤ a ^ n
⊢ ∀ᶠ (b : ℝ≥0∞) in map (fun (n : ℕ) ↦ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop, (↑r : ℝ≥0∞) ≤ b

Tactic:
H.mp ((eventually_gt_atTop 0).mono fun n hn₀ hn => (this _ hn₀).2 (NNReal.coe_le_coe.1 ?_))

Premises used: Iff.mpr, Set.Mem, Filter.Eventually, setOf, Set.Subset, Filter.Eventually.mono, Filter.Eventually.mp, Set.preimage, ENNReal, Iff.mp, OfNat.ofNat, NNReal.coe_le_coe, WithTop, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.Analytic.RadiusLiminf
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this :
  ∀ (r : ℝ≥0) {n : ℕ},
    0 < n → ((↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) a
H : ∀ᶠ (n : ℕ) in atTop, |‖p n‖ * (↑r : ℝ) ^ n| ≤ a ^ n
a₁ : ∀ (n : ℕ) (hn₀ : 0 < n) (hn : |‖p n‖ * (↑r : ℝ) ^ n| ≤ a ^ n), (↑(‖p n‖₊ * r ^ n) : ℝ) ≤ (↑1 : ℝ)
⊢ ∀ᶠ (b : ℝ≥0∞) in map (fun (n : ℕ) ↦ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop, (↑r : ℝ≥0∞) ≤ b

Tactic:
refine
        H.mp ((eventually_gt_atTop 0).mono fun n hn₀ hn => (this _ hn₀).2 (NNReal.coe_le_coe.1 ?_))

Premises used: Iff.mpr, Filter.Eventually.mono, Filter.Eventually.mp, Iff.mp, OfNat.ofNat, NNReal.coe_le_coe, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.Analytic.RadiusLiminf
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this :
  ∀ (r : ℝ≥0) {n : ℕ},
    0 < n → ((↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) a
H : ∀ᶠ (n : ℕ) in atTop, |‖p n‖ * (↑r : ℝ) ^ n| ≤ a ^ n
n : ℕ
hn₀ : 0 < n
hn : |‖p n‖ * (↑r : ℝ) ^ n| ≤ a ^ n
⊢ ‖p n‖ * (↑r : ℝ) ^ n ≤ 1

Tactic:
(le_abs_self _).trans (hn.trans (pow_le_one₀ ha.1.le ha.2.le))

Premises used: le_abs_self, LT.lt.le, And.right, And.left, LE.le.trans, pow_le_one₀
-- Module: Mathlib.Analysis.Analytic.RadiusLiminf
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this :
  ∀ (r : ℝ≥0) {n : ℕ},
    0 < n → ((↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) a
H : ∀ᶠ (n : ℕ) in atTop, |‖p n‖ * (↑r : ℝ) ^ n| ≤ a ^ n
n : ℕ
hn₀ : 0 < n
hn : |‖p n‖ * (↑r : ℝ) ^ n| ≤ a ^ n
⊢ ‖p n‖ * (↑r : ℝ) ^ n ≤ 1

Tactic:
exact (le_abs_self _).trans (hn.trans (pow_le_one₀ ha.1.le ha.2.le))

Premises used: le_abs_self, LT.lt.le, And.right, And.left, LE.le.trans, pow_le_one₀
-- Module: Mathlib.Analysis.Analytic.RadiusLiminf
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this :
  ∀ (r : ℝ≥0) {n : ℕ},
    0 < n → ((↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < liminf (fun (n : ℕ) ↦ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop
⊢ (↑r : ℝ≥0∞) ≤ p.radius

Tactic:
p.le_radius_of_isBigO <| .of_norm_eventuallyLE ?_

Premises used: Asymptotics.IsBigO.of_norm_eventuallyLE, FormalMultilinearSeries.le_radius_of_isBigO
-- Module: Mathlib.Analysis.Analytic.RadiusLiminf
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this :
  ∀ (r : ℝ≥0) {n : ℕ},
    0 < n → ((↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < liminf (fun (n : ℕ) ↦ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop
a : EventuallyLE (β := ℝ) atTop (fun (x : ℕ) ↦ ‖‖p x‖ * (↑r : ℝ) ^ x‖) fun (x : ℕ) ↦ 1
⊢ (↑r : ℝ≥0∞) ≤ p.radius

Tactic:
refine p.le_radius_of_isBigO <| .of_norm_eventuallyLE ?_

Premises used: FormalMultilinearSeries.le_radius_of_isBigO
-- Module: Mathlib.Analysis.Analytic.RadiusLiminf
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this :
  ∀ (r : ℝ≥0) {n : ℕ},
    0 < n → ((↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < liminf (fun (n : ℕ) ↦ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop
h :
  ∀ (n : ℕ) (hn : (↑r : ℝ≥0∞) < 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) (hn₀ : 0 < n),
    ‖‖p n‖ * (↑r : ℝ) ^ n‖ ≤ 1
⊢ EventuallyLE (β := ℝ) atTop (fun (x : ℕ) ↦ ‖‖p x‖ * (↑r : ℝ) ^ x‖) fun (x : ℕ) ↦ 1

Tactic:
filter_upwards [eventually_lt_of_lt_liminf hr, eventually_gt_atTop 0] with n hn hn₀

Premises used: Filter.eventually_lt_of_lt_liminf, OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.Analytic.RadiusLiminf
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this :
  ∀ (r : ℝ≥0) {n : ℕ},
    0 < n → ((↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < liminf (fun (n : ℕ) ↦ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop
n : ℕ
hn : (↑r : ℝ≥0∞) < 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)
hn₀ : 0 < n
⊢ ‖‖p n‖ * (↑r : ℝ) ^ n‖ ≤ 1

Tactic:
simpa using NNReal.coe_le_coe.2 ((this _ hn₀).1 hn.le)

Premises used: Iff.mpr, LT.lt.le, Iff.mp, NNReal.coe_le_coe
-- Module: Mathlib.Analysis.Analytic.RadiusLiminf
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
⊢ p.radius⁻¹ = limsup (fun (n : ℕ) ↦ (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop

Tactic:
simpa [ENNReal.inv_liminf] using congr($(p.radius_eq_liminf)⁻¹)

Premises used: ENNReal.inv_liminf, FormalMultilinearSeries.radius_eq_liminf
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
p : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F
h :
  IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝 0) (fun (y : E) ↦ (p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    fun (y : E) ↦ ‖y‖ ^ (n + 1)
y : E
by_contra! : ∀ (hy : Ne.{u_3 + 1} (α := F) ((p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) (0 : F)), False
⊢ Eq.{u_3 + 1} (α := F) ((p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) (0 : F)

Tactic:
by_contra! hy
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
p : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F
h :
  IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝 0) (fun (y : E) ↦ (p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    fun (y : E) ↦ ‖y‖ ^ (n + 1)
y : E
hy : Ne.{u_3 + 1} (α := F) ((p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) (0 : F)
⊢ IsBigO.{u_1, u_1, u_3} (E := 𝕜) (F := F) (𝓝 0) (fun (c : 𝕜) ↦ c ^ n) fun (c : 𝕜) ↦
    HSMul.hSMul (β := F) (c ^ n) ((p : (a : (i : Fin n) → E) → F) fun (i : Fin n) ↦ y : F)

Tactic:
.of_norm_norm ?_

Premises used: Asymptotics.IsBigO.of_norm_norm
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
p : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F
h :
  IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝 0) (fun (y : E) ↦ (p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    fun (y : E) ↦ ‖y‖ ^ (n + 1)
y : E
hy : Ne.{u_3 + 1} (α := F) ((p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) (0 : F)
refine :
  IsBigO (E := ℝ) (F := ℝ) (𝓝 0) (fun (x : 𝕜) ↦ ‖x ^ n‖) fun (x : 𝕜) ↦
    ‖HSMul.hSMul (β := F) (x ^ n) ((p : (a : (i : Fin n) → E) → F) fun (i : Fin n) ↦ y : F)‖
⊢ IsBigO.{u_1, u_1, u_3} (E := 𝕜) (F := F) (𝓝 0) (fun (c : 𝕜) ↦ c ^ n) fun (c : 𝕜) ↦
    HSMul.hSMul (β := F) (c ^ n) ((p : (a : (i : Fin n) → E) → F) fun (i : Fin n) ↦ y : F)

Tactic:
refine .of_norm_norm ?_
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
p : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F
h :
  IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝 0) (fun (y : E) ↦ (p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    fun (y : E) ↦ ‖y‖ ^ (n + 1)
y : E
hy : Ne.{u_3 + 1} (α := F) ((p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) (0 : F)
simp :
  IsBigO (E := ℝ) (F := ℝ) (𝓝 0) (fun (x : 𝕜) ↦ ‖x ^ n‖) fun (x : 𝕜) ↦
    norm.{u_3} (E := F) ((p : (a : (i : Fin n) → E) → F) fun (i : Fin n) ↦ y : F) * ‖x ^ n‖
⊢ IsBigO (E := ℝ) (F := ℝ) (𝓝 0) (fun (x : 𝕜) ↦ ‖x ^ n‖) fun (x : 𝕜) ↦
    ‖HSMul.hSMul (β := F) (x ^ n) ((p : (a : (i : Fin n) → E) → F) fun (i : Fin n) ↦ y : F)‖

Tactic:
simp only [norm_smul, mul_comm (‖_ ^ _‖)]

Premises used: Norm.norm, norm_smul, HPow.hPow, mul_comm
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
p : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F
h :
  IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝 0) (fun (y : E) ↦ (p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    fun (y : E) ↦ ‖y‖ ^ (n + 1)
y : E
hy : Ne.{u_3 + 1} (α := F) ((p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) (0 : F)
⊢ norm.{u_3} (E := F) ((p : (a : (i : Fin n) → E) → F) fun (i : Fin n) ↦ y : F) ≠ 0

Tactic:
simpa
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
p : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F
h :
  IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝 0) (fun (y : E) ↦ (p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    fun (y : E) ↦ ‖y‖ ^ (n + 1)
y : E
hy : Ne.{u_3 + 1} (α := F) ((p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) (0 : F)
⊢ IsBigO (E := ℝ) (F := ℝ) (𝓝 0) (fun (x : 𝕜) ↦ ‖x ^ n‖) fun (x : 𝕜) ↦
    norm.{u_3} (E := F) ((p : (a : (i : Fin n) → E) → F) fun (i : Fin n) ↦ y : F) * ‖x ^ n‖

Tactic:
exact .const_mul_right (by simpa) (isBigO_refl ..)
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
p : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F
h :
  IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝 0) (fun (y : E) ↦ (p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    fun (y : E) ↦ ‖y‖ ^ (n + 1)
y : E
hy : Ne.{u_3 + 1} (α := F) ((p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) (0 : F)
⊢ Eq (α := (c : 𝕜) → F)
    (fun (c : 𝕜) ↦ HSMul.hSMul (β := F) (c ^ n) ((p : (a : (i : Fin n) → E) → F) fun (i : Fin n) ↦ y : F)) fun (c : 𝕜) ↦
    (p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ c • y

Tactic:
simp [p.map_smul_univ]

Premises used: ContinuousMultilinearMap.map_smul_univ
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
p : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F
h :
  IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝 0) (fun (y : E) ↦ (p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    fun (y : E) ↦ ‖y‖ ^ (n + 1)
y : E
hy : Ne.{u_3 + 1} (α := F) ((p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) (0 : F)
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (c : 𝕜) ↦ c • y

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
p : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F
h :
  IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝 0) (fun (y : E) ↦ (p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    fun (y : E) ↦ ‖y‖ ^ (n + 1)
y : E
hy : Ne.{u_3 + 1} (α := F) ((p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) (0 : F)
⊢ IsBigO (E := ℝ) (F := 𝕜) (𝓝 0) (fun (c : 𝕜) ↦ ‖c • y‖ ^ (n + 1)) fun (c : 𝕜) ↦ c ^ (n + 1)

Tactic:
.of_norm_right ?_

Premises used: Asymptotics.IsBigO.of_norm_right
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
p : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F
h :
  IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝 0) (fun (y : E) ↦ (p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    fun (y : E) ↦ ‖y‖ ^ (n + 1)
y : E
hy : Ne.{u_3 + 1} (α := F) ((p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) (0 : F)
refine : IsBigO (E := ℝ) (F := ℝ) (𝓝 0) (fun (c : 𝕜) ↦ ‖c • y‖ ^ (n + 1)) fun (x : 𝕜) ↦ ‖x ^ (n + 1)‖
⊢ IsBigO (E := ℝ) (F := 𝕜) (𝓝 0) (fun (c : 𝕜) ↦ ‖c • y‖ ^ (n + 1)) fun (c : 𝕜) ↦ c ^ (n + 1)

Tactic:
refine .of_norm_right ?_
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
p : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F
h :
  IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝 0) (fun (y : E) ↦ (p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    fun (y : E) ↦ ‖y‖ ^ (n + 1)
y : E
hy : Ne.{u_3 + 1} (α := F) ((p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) (0 : F)
simp : IsBigO (E := ℝ) (F := ℝ) (𝓝 0) (fun (c : 𝕜) ↦ ‖y‖ ^ (n + 1) * ‖c‖ ^ (n + 1)) fun (x : 𝕜) ↦ ‖x‖ ^ (n + 1)
⊢ IsBigO (E := ℝ) (F := ℝ) (𝓝 0) (fun (c : 𝕜) ↦ ‖c • y‖ ^ (n + 1)) fun (x : 𝕜) ↦ ‖x ^ (n + 1)‖

Tactic:
simp only [norm_smul, mul_pow, mul_comm _ ‖y‖, norm_pow]

Premises used: Norm.norm, norm_smul, norm_pow, mul_comm, mul_pow
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
p : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F
h :
  IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝 0) (fun (y : E) ↦ (p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    fun (y : E) ↦ ‖y‖ ^ (n + 1)
y : E
hy : Ne.{u_3 + 1} (α := F) ((p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) (0 : F)
⊢ IsBigO (E := ℝ) (F := ℝ) (𝓝 0) (fun (c : 𝕜) ↦ ‖y‖ ^ (n + 1) * ‖c‖ ^ (n + 1)) fun (x : 𝕜) ↦ ‖x‖ ^ (n + 1)

Tactic:
.const_mul_left (isBigO_refl ..) _

Premises used: Asymptotics.IsBigO.const_mul_left, Asymptotics.isBigO_refl
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
p : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F
h :
  IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝 0) (fun (y : E) ↦ (p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    fun (y : E) ↦ ‖y‖ ^ (n + 1)
y : E
hy : Ne.{u_3 + 1} (α := F) ((p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) (0 : F)
⊢ IsBigO (E := ℝ) (F := ℝ) (𝓝 0) (fun (c : 𝕜) ↦ ‖y‖ ^ (n + 1) * ‖c‖ ^ (n + 1)) fun (x : 𝕜) ↦ ‖x‖ ^ (n + 1)

Tactic:
exact .const_mul_left (isBigO_refl ..) _
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
p : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F
h :
  IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝 0) (fun (y : E) ↦ (p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    fun (y : E) ↦ ‖y‖ ^ (n + 1)
y : E
hy : Ne.{u_3 + 1} (α := F) ((p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) (0 : F)
⊢ n < n + 1

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
p : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F
h :
  IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝 0) (fun (y : E) ↦ (p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    fun (y : E) ↦ ‖y‖ ^ (n + 1)
y : E
hy : Ne.{u_3 + 1} (α := F) ((p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) (0 : F)
⊢ IsLittleO (E := 𝕜) (F := 𝕜) (𝓝 0) (fun (c : 𝕜) ↦ c ^ n) fun (c : 𝕜) ↦ c ^ n

Tactic:
have : (fun c : 𝕜 ↦ c ^ n) =o[𝓝 0] (fun c : 𝕜 ↦ c ^ n) := calc
    (fun c : 𝕜 ↦ c ^ n) =O[𝓝 0] fun c ↦ c ^ n • p fun i ↦ y := by
      refine .of_norm_norm ?_
      simp only [norm_smul, mul_comm (‖_ ^ _‖)]
      exact .const_mul_right (by simpa) (isBigO_refl ..)
    _ = fun c ↦ p fun _ ↦ c • y := by simp [p.map_smul_univ]
    _ =O[𝓝 0] fun c ↦ ‖c • y‖ ^ (n + 1) :=
      h.comp_tendsto <| Continuous.tendsto' (by fun_prop) _ _ (zero_smul _ _)
    _ =O[𝓝 0] fun c ↦ c ^ (n + 1) := by
      refine .of_norm_right ?_
      simp only [norm_smul, mul_pow, mul_comm _ ‖y‖, norm_pow]
      exact .const_mul_left (isBigO_refl ..) _
    _ =o[𝓝 0] (· ^ n) := isLittleO_pow_pow (by simp)
-- Module: Mathlib.Analysis.Analytic.Uniqueness
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
p : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F
h :
  IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝 0) (fun (y : E) ↦ (p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    fun (y : E) ↦ ‖y‖ ^ (n + 1)
y : E
hy : Ne.{u_3 + 1} (α := F) ((p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) (0 : F)
this : IsLittleO (E := 𝕜) (F := 𝕜) (𝓝 0) (fun (c : 𝕜) ↦ c ^ n) fun (c : 𝕜) ↦ c ^ n
⊢ False

Tactic:
isLittleO_irrefl (.mono ?_ fun _ ↦ pow_ne_zero n) this

Premises used: Asymptotics.isLittleO_irrefl, Filter.Frequently.mono