awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
e_s :
  LE.le (α := ℝ≥0∞)
    (⨆ (C : ℝ),
      ⨆ (_ :
        ∀ (n : ℕ),
          norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) *
              (↑r : ℝ) ^ n ≤
            C),
        (↑r : ℝ≥0∞))
    (⨆ (C : ℝ), ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C), (↑r : ℝ≥0∞))
e_s₁ :
  LE.le (α := ℝ≥0∞) (⨆ (C : ℝ), ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C), (↑r : ℝ≥0∞))
    (⨆ (C : ℝ),
      ⨆ (_ :
        ∀ (n : ℕ),
          norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) *
              (↑r : ℝ) ^ n ≤
            C),
        (↑r : ℝ≥0∞))
⊢ Eq (α := ℝ≥0∞)
    (⨆ (C : ℝ),
      ⨆ (_ :
        ∀ (n : ℕ),
          norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) *
              (↑r : ℝ) ^ n ≤
            C),
        (↑r : ℝ≥0∞))
    (⨆ (C : ℝ), ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C), (↑r : ℝ≥0∞))

Tactic:
apply eq_of_le_of_ge

Premises used: eq_of_le_of_ge
-- 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
e_s :
  ∀ (i : ℝ),
    ∃ (i' : ℝ),
      LE.le (α := ℝ≥0∞)
        (⨆ (_ :
          ∀ (n : ℕ),
            norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) *
                (↑r : ℝ) ^ n ≤
              i),
          (↑r : ℝ≥0∞))
        (⨆ (_ : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ i'), (↑r : ℝ≥0∞))
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (C : ℝ),
      ⨆ (_ :
        ∀ (n : ℕ),
          norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) *
              (↑r : ℝ) ^ n ≤
            C),
        (↑r : ℝ≥0∞))
    (⨆ (C : ℝ), ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C), (↑r : ℝ≥0∞))

Tactic:
apply iSup_mono'

Premises used: iSup_mono'
-- 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 :
  LE.le (α := ℝ≥0∞)
    (⨆ (_ :
      ∀ (n : ℕ),
        norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) *
            (↑r : ℝ) ^ n ≤
          C),
      (↑r : ℝ≥0∞))
    (⨆ (_ :
      ∀ (n : ℕ),
        ‖p n‖ * (↑r : ℝ) ^ n ≤
          max (norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F) (p 0)) (C * (↑r : ℝ))),
      (↑r : ℝ≥0∞))
⊢ ∃ (i' : ℝ),
    LE.le (α := ℝ≥0∞)
      (⨆ (_ :
        ∀ (n : ℕ),
          norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) *
              (↑r : ℝ) ^ n ≤
            C),
        (↑r : ℝ≥0∞))
      (⨆ (_ : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ i'), (↑r : ℝ≥0∞))

Tactic:
use ‖p 0‖ ⊔ (C * r)

Premises used: HMul.hMul, OfNat.ofNat, 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
C : ℝ
h :
  ∀
    (i :
      ∀ (n : ℕ),
        norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) *
            (↑r : ℝ) ^ n ≤
          C),
    ∃ (_ :
      ∀ (n : ℕ),
        ‖p n‖ * (↑r : ℝ) ^ n ≤
          max (norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F) (p 0)) (C * (↑r : ℝ))),
      (↑r : ℝ≥0∞) ≤ (↑r : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (_ :
      ∀ (n : ℕ),
        norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) *
            (↑r : ℝ) ^ n ≤
          C),
      (↑r : ℝ≥0∞))
    (⨆ (_ :
      ∀ (n : ℕ),
        ‖p n‖ * (↑r : ℝ) ^ n ≤
          max (norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F) (p 0)) (C * (↑r : ℝ))),
      (↑r : ℝ≥0∞))

Tactic:
apply iSup_mono'

Premises used: iSup_mono'
-- 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 : ℕ),
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) * (↑r : ℝ) ^ n ≤
      C
h₁ :
  ∀ (n : ℕ),
    ‖p n‖ * (↑r : ℝ) ^ n ≤ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F) (p 0) ∨
      ‖p n‖ * (↑r : ℝ) ^ n ≤ C * (↑r : ℝ)
⊢ ∃ (_ :
    ∀ (n : ℕ),
      ‖p n‖ * (↑r : ℝ) ^ n ≤
        max (norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F) (p 0)) (C * (↑r : ℝ))),
    (↑r : ℝ≥0∞) ≤ (↑r : ℝ≥0∞)

Tactic:
simp only [le_refl, le_sup_iff, exists_prop, and_true]

Premises used: le_refl, and_true, exists_prop, le_sup_iff
-- 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 : ℕ),
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) * (↑r : ℝ) ^ n ≤
      C
n : ℕ
h₁ :
  norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F) (p 0) *
        HPow.hPow (β := ℕ) (↑r : ℝ) 0 ≤
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F) (p 0) ∨
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F) (p 0) *
        HPow.hPow (β := ℕ) (↑r : ℝ) 0 ≤
      C * (↑r : ℝ)
h₂ :
  ∀ (m : ℕ),
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (m + 1)) ↦ E) F) (p (m + 1)) *
          (↑r : ℝ) ^ (m + 1) ≤
        norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F) (p 0) ∨
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (m + 1)) ↦ E) F) (p (m + 1)) *
          (↑r : ℝ) ^ (m + 1) ≤
        C * (↑r : ℝ)
⊢ ‖p n‖ * (↑r : ℝ) ^ n ≤ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F) (p 0) ∨
    ‖p n‖ * (↑r : ℝ) ^ n ≤ C * (↑r : ℝ)

Tactic:
rcases n with - | m
-- 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 : ℕ),
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) * (↑r : ℝ) ^ n ≤
      C
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F) (p 0) *
        HPow.hPow (β := ℕ) (↑r : ℝ) 0 ≤
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F) (p 0) ∨
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F) (p 0) *
        HPow.hPow (β := ℕ) (↑r : ℝ) 0 ≤
      C * (↑r : ℝ)

Tactic:
simp
-- 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 : ℕ),
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) * (↑r : ℝ) ^ n ≤
      C
m : ℕ
h₁ :
  norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (m + 1)) ↦ E) F) (p (m + 1)) *
      (↑r : ℝ) ^ (m + 1) ≤
    C * (↑r : ℝ)
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (m + 1)) ↦ E) F) (p (m + 1)) *
        (↑r : ℝ) ^ (m + 1) ≤
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F) (p 0) ∨
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (m + 1)) ↦ E) F) (p (m + 1)) *
        (↑r : ℝ) ^ (m + 1) ≤
      C * (↑r : ℝ)

Tactic:
right
-- 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 : ℕ),
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) * (↑r : ℝ) ^ n ≤
      C
m : ℕ
h₁ :
  norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (m + 1)) ↦ E) F) (p (m + 1)) * (↑r : ℝ) ^ m *
      (↑r : ℝ) ≤
    C * (↑r : ℝ)
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (m + 1)) ↦ E) F) (p (m + 1)) *
      (↑r : ℝ) ^ (m + 1) ≤
    C * (↑r : ℝ)

Tactic:
rw [pow_succ, ← mul_assoc]

Premises used: pow_succ, mul_assoc
-- 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 : ℕ),
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) * (↑r : ℝ) ^ n ≤
      C
m : ℕ
h₁ :
  norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (m + 1)) ↦ E) F) (p (m + 1)) * (↑r : ℝ) ^ m ≤ C
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (m + 1)) ↦ E) F) (p (m + 1)) * (↑r : ℝ) ^ m *
      (↑r : ℝ) ≤
    C * (↑r : ℝ)

Tactic:
gcongr
-- 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 : ℕ),
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) * (↑r : ℝ) ^ n ≤
      C
m : ℕ
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (m + 1)) ↦ E) F) (p (m + 1)) * (↑r : ℝ) ^ m ≤ C

Tactic:
apply 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
r : ℝ≥0
e_s :
  ∀ (i : ℝ),
    ∃ (i' : ℝ),
      LE.le (α := ℝ≥0∞) (⨆ (_ : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ i), (↑r : ℝ≥0∞))
        (⨆ (_ :
          ∀ (n : ℕ),
            norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) *
                (↑r : ℝ) ^ n ≤
              i'),
          (↑r : ℝ≥0∞))
⊢ LE.le (α := ℝ≥0∞) (⨆ (C : ℝ), ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C), (↑r : ℝ≥0∞))
    (⨆ (C : ℝ),
      ⨆ (_ :
        ∀ (n : ℕ),
          norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) *
              (↑r : ℝ) ^ n ≤
            C),
        (↑r : ℝ≥0∞))

Tactic:
apply iSup_mono'

Premises used: iSup_mono'
-- 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 :
  LE.le (α := ℝ≥0∞) (⨆ (_ : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C), (↑r : ℝ≥0∞))
    (⨆ (_ :
      ∀ (n : ℕ),
        norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) *
            (↑r : ℝ) ^ n ≤
          max (norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)) (C / (↑r : ℝ))),
      (↑r : ℝ≥0∞))
⊢ ∃ (i' : ℝ),
    LE.le (α := ℝ≥0∞) (⨆ (_ : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C), (↑r : ℝ≥0∞))
      (⨆ (_ :
        ∀ (n : ℕ),
          norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) *
              (↑r : ℝ) ^ n ≤
            i'),
        (↑r : ℝ≥0∞))

Tactic:
use ‖p 1‖ ⊔ C / r

Premises used: OfNat.ofNat
-- 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 :
  ∀ (i : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C),
    ∃ (_ :
      ∀ (n : ℕ),
        norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) *
            (↑r : ℝ) ^ n ≤
          max (norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)) (C / (↑r : ℝ))),
      (↑r : ℝ≥0∞) ≤ (↑r : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (⨆ (_ : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C), (↑r : ℝ≥0∞))
    (⨆ (_ :
      ∀ (n : ℕ),
        norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) *
            (↑r : ℝ) ^ n ≤
          max (norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)) (C / (↑r : ℝ))),
      (↑r : ℝ≥0∞))

Tactic:
apply iSup_mono'

Premises used: iSup_mono'
-- 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 : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C
h₁ :
  ∀ (n : ℕ),
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) * (↑r : ℝ) ^ n ≤
        norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1) ∨
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) *
          (↑r : ℝ) ^ n ≤
        C / (↑r : ℝ)
⊢ ∃ (_ :
    ∀ (n : ℕ),
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) *
          (↑r : ℝ) ^ n ≤
        max (norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)) (C / (↑r : ℝ))),
    (↑r : ℝ≥0∞) ≤ (↑r : ℝ≥0∞)

Tactic:
simp only [le_refl, le_sup_iff, exists_prop, and_true]

Premises used: le_refl, and_true, exists_prop, le_sup_iff
-- 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 : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C
n : ℕ
hr : r = 0
h₁ :
  norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) * (↑0 : ℝ) ^ n ≤
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1) ∨
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) * (↑0 : ℝ) ^ n ≤
      C / (↑0 : ℝ)
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) * (↑r : ℝ) ^ n ≤
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1) ∨
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) * (↑r : ℝ) ^ n ≤
      C / (↑r : ℝ)

Tactic:
rw [hr]
-- 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 : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C
n : ℕ
hr : r = 0
h₁ :
  norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E) F)
          (p (HAdd.hAdd (α := ℕ) 0 1)) *
        HPow.hPow (β := ℕ) (↑0 : ℝ) 0 ≤
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1) ∨
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E) F)
          (p (HAdd.hAdd (α := ℕ) 0 1)) *
        HPow.hPow (β := ℕ) (↑0 : ℝ) 0 ≤
      C / (↑0 : ℝ)
h₂ :
  ∀ (n : ℕ),
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1 + 1)) ↦ E) F) (p (n + 1 + 1)) *
          (↑0 : ℝ) ^ (n + 1) ≤
        norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1) ∨
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1 + 1)) ↦ E) F) (p (n + 1 + 1)) *
          (↑0 : ℝ) ^ (n + 1) ≤
        C / (↑0 : ℝ)
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) * (↑0 : ℝ) ^ n ≤
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1) ∨
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) * (↑0 : ℝ) ^ n ≤
      C / (↑0 : ℝ)

Tactic:
cases n
-- 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 : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C
hr : r = 0
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E) F)
          (p (HAdd.hAdd (α := ℕ) 0 1)) *
        HPow.hPow (β := ℕ) (↑0 : ℝ) 0 ≤
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1) ∨
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ E) F)
          (p (HAdd.hAdd (α := ℕ) 0 1)) *
        HPow.hPow (β := ℕ) (↑0 : ℝ) 0 ≤
      C / (↑0 : ℝ)

Tactic:
simp
-- 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 : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C
hr : r = 0
n : ℕ
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1 + 1)) ↦ E) F) (p (n + 1 + 1)) *
        (↑0 : ℝ) ^ (n + 1) ≤
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1) ∨
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1 + 1)) ↦ E) F) (p (n + 1 + 1)) *
        (↑0 : ℝ) ^ (n + 1) ≤
      C / (↑0 : ℝ)

Tactic:
simp
-- 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 : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C
n : ℕ
hr : 0 < r
h₁ :
  norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) * (↑r : ℝ) ^ n ≤
    C / (↑r : ℝ)
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) * (↑r : ℝ) ^ n ≤
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1) ∨
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) * (↑r : ℝ) ^ n ≤
      C / (↑r : ℝ)

Tactic:
right
-- 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 : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C
n : ℕ
hr : 0 < r
⊢ 0 < (↑r : ℝ)

Tactic:
rw [← NNReal.coe_pos] at hr

Premises used: NNReal.coe_pos
-- 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 : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C
n : ℕ
hr : 0 < (↑r : ℝ)
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) *
      (↑r : ℝ) ^ (n + 1) ≤
    C

Tactic:
specialize h (n + 1)

Premises used: HAdd.hAdd, OfNat.ofNat
-- 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 : ℝ
n : ℕ
hr : 0 < (↑r : ℝ)
h :
  norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) *
      (↑r : ℝ) ^ (n + 1) ≤
    C
h₁ :
  norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) * (↑r : ℝ) ^ n *
      (↑r : ℝ) ≤
    C
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) * (↑r : ℝ) ^ n ≤
    C / (↑r : ℝ)

Tactic:
rw [le_div_iff₀ hr]

Premises used: le_div_iff₀
-- 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 : ℝ
n : ℕ
hr : 0 < (↑r : ℝ)
h :
  norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) *
      (↑r : ℝ) ^ (n + 1) ≤
    C
h₁ :
  ∀
    (h :
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) *
          ((↑r : ℝ) ^ n * (↑r : ℝ)) ≤
        C),
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) * (↑r : ℝ) ^ n *
        (↑r : ℝ) ≤
      C
h₂ h₃ h₄ h₅ :
  ∀
    (h :
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) *
            (↑r : ℝ) ^ n *
          (↑r : ℝ) ≤
        C),
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) * (↑r : ℝ) ^ n *
        (↑r : ℝ) ≤
      C
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) * (↑r : ℝ) ^ n *
      (↑r : ℝ) ≤
    C

Tactic:
rwa [pow_succ, ← mul_assoc] at h

Premises used: pow_succ, mul_assoc
-- 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 : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C
n : ℕ
⊢ r = 0 ∨ 0 < r

Tactic:
cases eq_zero_or_pos r with
    | inl hr =>
      rw [hr]
      cases n <;> simp
    | inr hr =>
      right
      rw [← NNReal.coe_pos] at hr
      specialize h (n + 1)
      rw [le_div_iff₀ hr]
      rwa [pow_succ, ← mul_assoc] at h

Premises used: pow_succ, mul_assoc, eq_zero_or_pos, HAdd.hAdd, NNReal.coe_pos, OfNat.ofNat