awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s ((u : (a : E) → F) x) r
y : E
hy1 : Membership.mem (γ := Set E) (insert x ((⇑u : (a : E) → F) ⁻¹' s)) (x + y)
hy2 : Membership.mem (γ := Set E) (Metric.eball 0 (r / ‖u‖ₑ)) y
convert_2 :
  ∀ (hy1 : y = 0 ∨ HAdd.hAdd (α := F) (β := F) ((u : (a : E) → F) x : F) ((u : (a : E) → F) y : F) ∈ s),
    Eq.{u_4 + 1} (α := F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F) (0 : F) ∨
      HAdd.hAdd (α := F) (β := F) ((u : (a : E) → F) x : F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F) ∈ s
⊢ HAdd.hAdd (α := F) (β := F) ((u : (a : E) → F) x : F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F) ∈
    insert (α := F) ((u : (a : E) → F) x : F) s

Tactic:
simp only [Set.mem_insert_iff, add_eq_left, Set.mem_preimage, map_add] at hy1 ⊢

Premises used: map_add, add_eq_left, Set.mem_insert_iff, Set.mem_preimage
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s ((u : (a : E) → F) x) r
y : E
hy2 : Membership.mem (γ := Set E) (Metric.eball 0 (r / ‖u‖ₑ)) y
hy1 : y = 0 ∨ HAdd.hAdd (α := F) (β := F) ((u : (a : E) → F) x : F) ((u : (a : E) → F) y : F) ∈ s
convert_2 :
  ∀ (hy1 : y = 0),
    Eq.{u_4 + 1} (α := F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F) (0 : F) ∨
      HAdd.hAdd (α := F) (β := F) ((u : (a : E) → F) x : F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F) ∈ s
convert_2₁ :
  ∀ (hy1 : HAdd.hAdd (α := F) (β := F) ((u : (a : E) → F) x : F) ((u : (a : E) → F) y : F) ∈ s),
    Eq.{u_4 + 1} (α := F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F) (0 : F) ∨
      HAdd.hAdd (α := F) (β := F) ((u : (a : E) → F) x : F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F) ∈ s
⊢ Eq.{u_4 + 1} (α := F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F) (0 : F) ∨
    HAdd.hAdd (α := F) (β := F) ((u : (a : E) → F) x : F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F) ∈ s

Tactic:
rcases hy1 with (hy1 | hy1)
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s ((u : (a : E) → F) x) r
y : E
hy2 : Membership.mem (γ := Set E) (Metric.eball 0 (r / ‖u‖ₑ)) y
hy1 : y = 0
⊢ Eq.{u_4 + 1} (α := F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F) (0 : F) ∨
    HAdd.hAdd (α := F) (β := F) ((u : (a : E) → F) x : F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F) ∈ s

Tactic:
simp [hy1]
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s ((u : (a : E) → F) x) r
y : E
hy2 : Membership.mem (γ := Set E) (Metric.eball 0 (r / ‖u‖ₑ)) y
hy1 : HAdd.hAdd (α := F) (β := F) ((u : (a : E) → F) x : F) ((u : (a : E) → F) y : F) ∈ s
⊢ Eq.{u_4 + 1} (α := F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F) (0 : F) ∨
    HAdd.hAdd (α := F) (β := F) ((u : (a : E) → F) x : F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F) ∈ s

Tactic:
simp [hy1]
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s ((u : (a : E) → F) x) r
y : E
hy1 : Membership.mem (γ := Set E) (insert x ((⇑u : (a : E) → F) ⁻¹' s)) (x + y)
hy2 : Membership.mem (γ := Set E) (Metric.eball 0 (r / ‖u‖ₑ)) y
convert_3 : ∀ (hy2 : ‖y‖ₑ < r / ‖u‖ₑ), enorm.{u_4} (E := F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F) < r
⊢ Membership.mem.{u_4, u_4} (α := F) (γ := Set F) (Metric.eball 0 r) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F)

Tactic:
simp only [Metric.eball, edist_zero_right, Set.mem_setOf_eq] at hy2 ⊢

Premises used: Set.mem_setOf_eq, Metric.eball, edist_zero_right
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s ((u : (a : E) → F) x) r
y : E
hy1 : Membership.mem (γ := Set E) (insert x ((⇑u : (a : E) → F) ⁻¹' s)) (x + y)
hy2 : ‖y‖ₑ < r / ‖u‖ₑ
⊢ enorm.{u_4} (E := F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F) < r

Tactic:
lt_of_le_of_lt (ContinuousLinearMap.le_opNorm_enorm _ _) (mul_lt_of_lt_div' hy2)

Premises used: lt_of_le_of_lt, ENNReal.mul_lt_of_lt_div', ContinuousLinearMap.le_opNorm_enorm
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s ((u : (a : E) → F) x) r
y : E
hy1 : Membership.mem (γ := Set E) (insert x ((⇑u : (a : E) → F) ⁻¹' s)) (x + y)
hy2 : ‖y‖ₑ < r / ‖u‖ₑ
⊢ enorm.{u_4} (E := F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F) < r

Tactic:
exact lt_of_le_of_lt (ContinuousLinearMap.le_opNorm_enorm _ _) (mul_lt_of_lt_div' hy2)

Premises used: lt_of_le_of_lt, ENNReal.mul_lt_of_lt_div', ContinuousLinearMap.le_opNorm_enorm
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f pf ((u : (a : E) → F) x) r
rw :
  ∀ (hf : HasFPowerSeriesWithinOnBall f pf Set.univ ((u : (a : E) → F) x) r),
    HasFPowerSeriesWithinOnBall (f ∘ (⇑u : (a : E) → F)) (pf.compContinuousLinearMap u) Set.univ x (r / ‖u‖ₑ)
⊢ HasFPowerSeriesOnBall (f ∘ (⇑u : (a : E) → F)) (pf.compContinuousLinearMap u) x (r / ‖u‖ₑ)

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf ⊢

Premises used: hasFPowerSeriesWithinOnBall_univ
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf Set.univ ((u : (a : E) → F) x) r
⊢ HasFPowerSeriesWithinOnBall (f ∘ (⇑u : (a : E) → F)) (pf.compContinuousLinearMap u) Set.univ x (r / ‖u‖ₑ)

Tactic:
hf.compContinuousLinearMap

Premises used: Set.Mem, Set.univ, setOf, HasFPowerSeriesWithinOnBall.compContinuousLinearMap, Set.preimage
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf Set.univ ((u : (a : E) → F) x) r
⊢ HasFPowerSeriesWithinOnBall (f ∘ (⇑u : (a : E) → F)) (pf.compContinuousLinearMap u) Set.univ x (r / ‖u‖ₑ)

Tactic:
exact hf.compContinuousLinearMap

Premises used: HasFPowerSeriesWithinOnBall.compContinuousLinearMap
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
x : E
hf : HasFPowerSeriesAt f pf ((u : (a : E) → F) x)
⊢ HasFPowerSeriesAt (f ∘ (⇑u : (a : E) → F)) (pf.compContinuousLinearMap u) x

Tactic:
let ⟨r, hr⟩ := hf
  ⟨r / ‖u‖ₑ, hr.compContinuousLinearMap⟩

Premises used: FormalMultilinearSeries.compContinuousLinearMap, HasFPowerSeriesOnBall.compContinuousLinearMap, Function.comp, HDiv.hDiv, ENorm.enorm, Exists.intro, HasFPowerSeriesAt, _private.0.HasFPowerSeriesAt.compContinuousLinearMap.match_1, DFunLike.coe
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
s : Set F
x : E
hf : HasFPowerSeriesWithinAt f pf s ((u : (a : E) → F) x)
⊢ HasFPowerSeriesWithinAt (f ∘ (⇑u : (a : E) → F)) (pf.compContinuousLinearMap u) ((⇑u : (a : E) → F) ⁻¹' s) x

Tactic:
let ⟨r, hr⟩ := hf
  ⟨r / ‖u‖ₑ, hr.compContinuousLinearMap⟩

Premises used: _private.0.HasFPowerSeriesWithinAt.compContinuousLinearMap.match_1, FormalMultilinearSeries.compContinuousLinearMap, Function.comp, HDiv.hDiv, ENorm.enorm, HasFPowerSeriesWithinOnBall.compContinuousLinearMap, Set.preimage, HasFPowerSeriesWithinAt, Exists.intro, DFunLike.coe
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
x : E
hf : AnalyticAt 𝕜 f ((u : (a : E) → F) x)
⊢ AnalyticAt 𝕜 (f ∘ (⇑u : (a : E) → F)) x

Tactic:
let ⟨p, hp⟩ := hf
  ⟨p.compContinuousLinearMap u, hp.compContinuousLinearMap⟩

Premises used: FormalMultilinearSeries.compContinuousLinearMap, Function.comp, AnalyticAt, Exists.intro, _private.0.AnalyticAt.compContinuousLinearMap.match_1, DFunLike.coe, HasFPowerSeriesAt.compContinuousLinearMap
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
s : Set F
x : E
hf : AnalyticWithinAt 𝕜 f s ((u : (a : E) → F) x)
⊢ AnalyticWithinAt 𝕜 (f ∘ (⇑u : (a : E) → F)) ((⇑u : (a : E) → F) ⁻¹' s) x

Tactic:
let ⟨p, hp⟩ := hf
  ⟨p.compContinuousLinearMap u, hp.compContinuousLinearMap⟩

Premises used: FormalMultilinearSeries.compContinuousLinearMap, Function.comp, AnalyticWithinAt, Set.preimage, Exists.intro, HasFPowerSeriesWithinAt.compContinuousLinearMap, DFunLike.coe, _private.0.AnalyticAtWithin.compContinuousLinearMap.match_1
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
s : Set F
hf : AnalyticOn 𝕜 f s
⊢ AnalyticOn.{u_2, u_3, u_5} 𝕜 (E := E) (f ∘ (⇑u : (a : E) → F)) ((⇑u : (a : E) → F) ⁻¹' s)

Tactic:
fun x hx =>
  AnalyticAtWithin.compContinuousLinearMap (hf (u x) hx)

Premises used: AnalyticAtWithin.compContinuousLinearMap, AnalyticOn, DFunLike.coe
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
s : Set F
hf : AnalyticOnNhd 𝕜 f s
⊢ AnalyticOnNhd.{u_2, u_3, u_5} 𝕜 (E := E) (f ∘ (⇑u : (a : E) → F)) ((⇑u : (a : E) → F) ⁻¹' s)

Tactic:
fun x hx =>
  AnalyticAt.compContinuousLinearMap (hf (u x) hx)

Premises used: AnalyticOnNhd, AnalyticAt.compContinuousLinearMap, DFunLike.coe
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : ContinuousAdd E
inst_8 : ContinuousAdd F
inst_9 : ContinuousConstSMul 𝕜 E
inst_10 : ContinuousConstSMul 𝕜 F
S : Type u_5
s : S
inst_11 : SetLike S F
inst_12 : AddSubmonoidClass S F
h_closed : IsClosed[inst_6] (↑s : Set F)
p : FormalMultilinearSeries 𝕜 E F
x : E
h : ∀ (k : ℕ), Membership.mem.{u_3, u_5} (α := F) s ((p k : (a : (i : Fin k) → E) → F) fun (x_1 : Fin k) ↦ x : F)
⊢ p.sum x ∈ s

Tactic:
tsum_mem h_closed h

Premises used: Set.Mem, tsum_mem, FormalMultilinearSeries.sum
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
inst_5 : TopologicalSpace E
inst_6 : TopologicalSpace F
inst_7 : ContinuousAdd E
inst_8 : ContinuousAdd F
inst_9 : ContinuousConstSMul 𝕜 E
inst_10 : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ Continuous[inst_5, inst_6] fun (x : E) ↦ ∑ k ∈ Finset.range n, (p k : (a : (i : Fin k) → E) → F) fun (x_1 : Fin k) ↦ x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
C : ℝ
r : ℝ≥0
h : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C
⊢ (↑r : ℝ≥0∞) ≤ p.radius

Tactic:
le_iSup_of_le r <| le_iSup_of_le C <| le_iSup (fun _ => (r : ℝ≥0∞)) h

Premises used: ENNReal.ofNNReal, le_iSup, FormalMultilinearSeries.radius, le_iSup_of_le
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
C r : ℝ≥0
h : ∀ (n : ℕ), ‖p n‖₊ * r ^ n ≤ C
⊢ (↑r : ℝ≥0∞) ≤ p.radius

Tactic:
p.le_radius_of_bound C fun n => mod_cast h n

Premises used: Norm.norm, HMul.hMul, cast, FormalMultilinearSeries.le_radius_of_bound, LE.le, HPow.hPow, Eq.refl, NNReal.toReal
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ 1
⊢ (↑r : ℝ≥0∞) ≤ p.radius

Tactic:
Exists.elim (isBigO_one_nat_atTop_iff.1 h) fun C hC =>
    p.le_radius_of_bound C fun n => (le_abs_self _).trans (hC n)

Premises used: Norm.norm, le_abs_self, HMul.hMul, FormalMultilinearSeries.le_radius_of_bound, Asymptotics.isBigO_one_nat_atTop_iff, HPow.hPow, Iff.mp, LE.le.trans, NNReal.toReal, Exists.elim
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
C : ℝ
h : ∀ᶠ (n : ℕ) in atTop, ‖p n‖ * (↑r : ℝ) ^ n ≤ C
n : ℕ
hn : ‖p n‖ * (↑r : ℝ) ^ n ≤ C
⊢ ‖‖p n‖ * (↑r : ℝ) ^ n‖ ≤ C * norm (E := ℝ) 1

Tactic:
simpa
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : Summable (α := ℝ≥0) fun (n : ℕ) ↦ ‖p n‖₊ * r ^ n
⊢ (↑r : ℝ≥0∞) ≤ p.radius

Tactic:
p.le_radius_of_bound_nnreal (∑' n, ‖p n‖₊ * r ^ n) fun _ => h.le_tsum' _

Premises used: HMul.hMul, NNNorm.nnnorm, Summable.le_tsum', HPow.hPow, tsum, SummationFilter.unconditional, FormalMultilinearSeries.le_radius_of_bound_nnreal
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : Summable (α := ℝ) fun (n : ℕ) ↦ (↑‖p n‖₊ : ℝ) * (↑r : ℝ) ^ n
⊢ Summable (α := ℝ≥0) fun (n : ℕ) ↦ ‖p n‖₊ * r ^ n

Tactic:
mod_cast h

Premises used: cast, NNReal.summable_coe._simp_1
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : Summable (α := ℝ) fun (n : ℕ) ↦ (↑‖p n‖₊ : ℝ) * (↑r : ℝ) ^ n
⊢ Summable (α := ℝ≥0) fun (n : ℕ) ↦ ‖p n‖₊ * r ^ n

Tactic:
exact mod_cast h
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
h : ∀ (r : ℝ≥0), IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ 1
⊢ p.radius = ∞

Tactic:
ENNReal.eq_top_of_forall_nnreal_le fun r => p.le_radius_of_isBigO (h r)

Premises used: ENNReal.eq_top_of_forall_nnreal_le, FormalMultilinearSeries.le_radius_of_isBigO
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
h : ∀ᶠ (n : ℕ) in atTop, p n = 0
r : ℝ≥0
n : ℕ
hn : p n = 0
⊢ Eq (α := ℝ) ((fun (_x : ℕ) ↦ (0 : ℝ)) n) ((fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) n)

Tactic:
simp [hn]
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (m + n)) ↦ E) F) (p (m + n)) 0
⊢ p.radius = ∞

Tactic:
p.radius_eq_top_of_eventually_eq_zero <|
    mem_atTop_sets.2 ⟨n, fun _ hk => tsub_add_cancel_of_le hk ▸ hn _⟩

Premises used: Iff.mpr, Filter.mem_atTop_sets, HSub.hSub, Eq.rec, tsub_add_cancel_of_le, Exists.intro, FormalMultilinearSeries.radius_eq_top_of_eventually_eq_zero
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
v : F
⊢ ∀ (m : ℕ),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (m + 1)) ↦ E) F)
      (constFormalMultilinearSeries 𝕜 E v (m + 1)) 0

Tactic:
simp [constFormalMultilinearSeries]

Premises used: constFormalMultilinearSeries
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
rw : radius.{u_1, u_2, u_3} (F := F) (constFormalMultilinearSeries 𝕜 E 0) = ∞
⊢ radius.{u_1, u_2, u_3} (𝕜 := 𝕜) (E := E) (F := F) 0 = ∞

Tactic:
rw [← constFormalMultilinearSeries_zero]

Premises used: constFormalMultilinearSeries_zero
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
⊢ radius.{u_1, u_2, u_3} (F := F) (constFormalMultilinearSeries 𝕜 E 0) = ∞

Tactic:
constFormalMultilinearSeries_radius

Premises used: FormalMultilinearSeries.constFormalMultilinearSeries_radius
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
⊢ radius.{u_1, u_2, u_3} (F := F) (constFormalMultilinearSeries 𝕜 E 0) = ∞

Tactic:
exact constFormalMultilinearSeries_radius

Premises used: FormalMultilinearSeries.constFormalMultilinearSeries_radius
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : (↑r : ℝ≥0∞) < p.radius
⊢ (∃ (a : ℝ),
      Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧
        IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
    ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n

Tactic:
have := (TFAE_exists_lt_isLittleO_pow (fun n => ‖p n‖ * (r : ℝ) ^ n) 1).out 1 4
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : (↑r : ℝ≥0∞) < p.radius
this :
  (∃ (a : ℝ),
      Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧
        IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
    ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
rw : ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
⊢ ∃ (a : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧
      IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x

Tactic:
rw [this]
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : (↑r : ℝ≥0∞) < p.radius
this :
  (∃ (a : ℝ),
      Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧
        IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
    ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
⊢ ∃ (i : ℝ≥0) (i_1 : ℝ) (_ : ∀ (n : ℕ), ‖p n‖ * (↑i : ℝ) ^ n ≤ i_1), (↑r : ℝ≥0∞) < (↑i : ℝ≥0∞)

Tactic:
simp only [radius, lt_iSup_iff] at h

Premises used: FormalMultilinearSeries.radius, lt_iSup_iff