awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
u : E →L[𝕜] F
h_zero : 0 < ‖u‖₊
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
C : ℝ
hC_pos : C > 0
hC : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C
n : ℕ
⊢ ‖p.compContinuousLinearMap u n‖ * (↑(r / ‖u‖₊) : ℝ) ^ n ≤ C
have u₁ : ‖p.compContinuousLinearMap u n‖ * (↑(r / ‖u‖₊) : ℝ) ^ n ≤ ‖p n‖ * ‖u‖ ^ n * (↑(r / ‖u‖₊) : ℝ) ^ n
Tactic: calc
    ‖p.compContinuousLinearMap u n‖ * ↑(r / ‖u‖₊) ^ n ≤ ‖p n‖ * ‖u‖ ^ n * ↑(r / ‖u‖₊) ^ n := by
      gcongr
      exact nnnorm_compContinuousLinearMap_le p u n
    _ = ‖p n‖ * r ^ n := by
      simp only [NNReal.coe_div, coe_nnnorm, div_pow, mul_assoc]
      rw [mul_div_cancel₀]
      rw [← NNReal.coe_pos] at h_zero
      positivity
    _ ≤ C := hC n
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
u : E →L[𝕜] F
h_zero : 0 < ‖u‖₊
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
C : ℝ
hC_pos : C > 0
hC : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C
n : ℕ
u₁ : ‖p.compContinuousLinearMap u n‖ * (↑(r / ‖u‖₊) : ℝ) ^ n ≤ ‖p n‖ * ‖u‖ ^ n * (↑(r / ‖u‖₊) : ℝ) ^ n
⊢ ‖p.compContinuousLinearMap u n‖ * (↑(r / ‖u‖₊) : ℝ) ^ n ≤ C
have u₂ : ‖p n‖ * ‖u‖ ^ n * (↑(r / ‖u‖₊) : ℝ) ^ n = ‖p n‖ * (↑r : ℝ) ^ n
Tactic: calc
    ‖p.compContinuousLinearMap u n‖ * ↑(r / ‖u‖₊) ^ n ≤ ‖p n‖ * ‖u‖ ^ n * ↑(r / ‖u‖₊) ^ n := by
      gcongr
      exact nnnorm_compContinuousLinearMap_le p u n
    _ = ‖p n‖ * r ^ n := by
      simp only [NNReal.coe_div, coe_nnnorm, div_pow, mul_assoc]
      rw [mul_div_cancel₀]
      rw [← NNReal.coe_pos] at h_zero
      positivity
    _ ≤ C := hC n
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
u : E →ₗᵢ[𝕜] F
⊢ p.radius ≤ radius (p.compContinuousLinearMap u.toContinuousLinearMap)
have inl : ∀ (h : Subsingleton E), p.radius ≤ radius (p.compContinuousLinearMap u.toContinuousLinearMap)
Tactic: obtain (h | h) := subsingleton_or_nontrivial E
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
u : E →ₗᵢ[𝕜] F
inl : ∀ (h : Subsingleton E), p.radius ≤ radius (p.compContinuousLinearMap u.toContinuousLinearMap)
⊢ p.radius ≤ radius (p.compContinuousLinearMap u.toContinuousLinearMap)
have inr : ∀ (h : Nontrivial E), p.radius ≤ radius (p.compContinuousLinearMap u.toContinuousLinearMap)
Tactic: obtain (h | h) := subsingleton_or_nontrivial E
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Nontrivial F
p : FormalMultilinearSeries 𝕜 F G
u : E ≃L[𝕜] F
⊢ radius (p.compContinuousLinearMap (↑u : E →L[𝕜] F)) ≤ ‖(↑u.symm : F →L[𝕜] E)‖ₑ * p.radius
have this : radius (p.compContinuousLinearMap (↑u : E →L[𝕜] F)) / ‖(↑u.symm : F →L[𝕜] E)‖ₑ ≤
  radius (compContinuousLinearMap (p.compContinuousLinearMap (↑u : E →L[𝕜] F)) (↑u.symm : F →L[𝕜] E))
Tactic: have := (p.compContinuousLinearMap u.toContinuousLinearMap).div_le_radius_compContinuousLinearMap
    u.symm.toContinuousLinearMap
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Nontrivial F
p : FormalMultilinearSeries 𝕜 F G
u : E ≃L[𝕜] F
this :
  radius (p.compContinuousLinearMap (↑u : E →L[𝕜] F)) / ‖(↑u.symm : F →L[𝕜] E)‖ₑ ≤
    radius (compContinuousLinearMap (p.compContinuousLinearMap (↑u : E →L[𝕜] F)) (↑u.symm : F →L[𝕜] E))
⊢ radius (p.compContinuousLinearMap (↑u : E →L[𝕜] F)) ≤ ‖(↑u.symm : F →L[𝕜] E)‖ₑ * p.radius
have this₁ : radius (p.compContinuousLinearMap (↑u : E →L[𝕜] F)) / ‖(↑u.symm : F →L[𝕜] E)‖ₑ ≤ p.radius
Tactic: simp only [compContinuousLinearMap_comp, ContinuousLinearEquiv.coe_comp_coe_symm,
    compContinuousLinearMap_id] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Nontrivial F
p : FormalMultilinearSeries 𝕜 F G
u : E ≃L[𝕜] F
this : radius (p.compContinuousLinearMap (↑u : E →L[𝕜] F)) / ‖(↑u.symm : F →L[𝕜] E)‖ₑ ≤ p.radius
⊢ radius (p.compContinuousLinearMap (↑u : E →L[𝕜] F)) ≤ ‖(↑u.symm : F →L[𝕜] E)‖ₑ * p.radius
have rwa : ∀ (this : radius (p.compContinuousLinearMap (↑u : E →L[𝕜] F)) ≤ ‖(↑u.symm : F →L[𝕜] E)‖ₑ * p.radius),
  radius (p.compContinuousLinearMap (↑u : E →L[𝕜] F)) ≤ ‖(↑u.symm : F →L[𝕜] E)‖ₑ * p.radius
Tactic: rwa [ENNReal.div_le_iff' (by simpa [DFunLike.ext_iff] using exists_ne 0) (by simp)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Nontrivial E
p : FormalMultilinearSeries 𝕜 F G
u : E ≃ₗᵢ[𝕜] F
⊢ radius (p.compContinuousLinearMap u.toLinearIsometry.toContinuousLinearMap) = p.radius
have refine : radius (p.compContinuousLinearMap u.toLinearIsometry.toContinuousLinearMap) ≤ p.radius
Tactic: refine le_antisymm ?_ <| le_radius_compContinuousLinearMap _ _
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Nontrivial E
p : FormalMultilinearSeries 𝕜 F G
u : E ≃ₗᵢ[𝕜] F
⊢ radius (p.compContinuousLinearMap u.toLinearIsometry.toContinuousLinearMap) ≤ p.radius
have x : Nontrivial F
Tactic: have _ : Nontrivial F := u.symm.toEquiv.nontrivial
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Nontrivial E
p : FormalMultilinearSeries 𝕜 F G
u : E ≃ₗᵢ[𝕜] F
h : Nontrivial F
⊢ radius (p.compContinuousLinearMap u.toLinearIsometry.toContinuousLinearMap) ≤ p.radius
have h : p.radius = ‖(↑(↑u : E ≃L[𝕜] F).symm : F →L[𝕜] E)‖ₑ * p.radius
Tactic: convert! radius_compContinuousLinearMap_le p u.toContinuousLinearEquiv
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Nontrivial E
p : FormalMultilinearSeries 𝕜 F G
u : E ≃ₗᵢ[𝕜] F
h : Nontrivial F
⊢ p.radius = ‖(↑(↑u : E ≃L[𝕜] F).symm : F →L[𝕜] E)‖ₑ * p.radius
have this : (↑(↑u : E ≃L[𝕜] F).symm : F →L[𝕜] E) = u.symm.toLinearIsometry.toContinuousLinearMap
Tactic: have : u.toContinuousLinearEquiv.symm.toContinuousLinearMap =
    u.symm.toLinearIsometry.toContinuousLinearMap := rfl
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
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
⊢ p.shift.radius (𝕜 := 𝕜) (E := E) (F := E →L[𝕜] F) = p.radius
have simp : Eq (α := ℝ≥0∞)
  (⨆ (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∞))
  (⨆ (r : ℝ≥0), ⨆ (C : ℝ), ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C), (↑r : ℝ≥0∞))
Tactic: simp only [radius, shift, Nat.succ_eq_add_one, ContinuousMultilinearMap.curryRight_norm]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
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
⊢ Eq (α := ℝ≥0∞)
    (⨆ (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∞))
    (⨆ (r : ℝ≥0), ⨆ (C : ℝ), ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C), (↑r : ℝ≥0∞))
have e_s : Eq (α := ℝ≥0 → ℝ≥0∞)
  (fun (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∞))
  fun (r : ℝ≥0) ↦ ⨆ (C : ℝ), ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C), (↑r : ℝ≥0∞)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
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
⊢ Eq (α := ℝ≥0 → ℝ≥0∞)
    (fun (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∞))
    fun (r : ℝ≥0) ↦ ⨆ (C : ℝ), ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C), (↑r : ℝ≥0∞)
have e_s : ∀ (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: ext r
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
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
⊢ 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∞))
have 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∞))
Tactic: apply eq_of_le_of_ge
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
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∞))
⊢ 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∞))
have 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∞))
Tactic: apply eq_of_le_of_ge
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
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
⊢ 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∞))
have 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∞))
Tactic: apply iSup_mono'
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
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 : ℝ
⊢ ∃ (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∞))
have 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∞))
Tactic: use ‖p 0‖ ⊔ (C * r)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
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 : ℝ
⊢ 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∞))
have 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∞)
Tactic: apply iSup_mono'
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
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 : ℕ),
      ‖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∞)
have 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 : ℝ)
Tactic: simp only [le_refl, le_sup_iff, exists_prop, and_true]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
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 : ℕ
⊢ ‖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 : ℝ)
have 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 : ℝ)
Tactic: rcases n with - | m
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
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 : ℝ)
⊢ ‖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 : ℝ)
have 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 : ℝ)
Tactic: rcases n with - | m
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
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 + 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 : ℝ)
have 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 : ℝ)
Tactic: right
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
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 + 1) ≤
    C * (↑r : ℝ)
have 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 : ℝ)
Tactic: rw [pow_succ, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
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 *
      (↑r : ℝ) ≤
    C * (↑r : ℝ)
have h₁ : norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (m + 1)) ↦ E) F) (p (m + 1)) * (↑r : ℝ) ^ m ≤ C
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
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
⊢ 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∞))
have 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∞))
Tactic: apply iSup_mono'