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
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 : ℕ), ‖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∞))
have 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∞))
Tactic: use ‖p 1‖ ⊔ 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 : ℕ), ‖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∞))
have 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∞)
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 : ℕ), ‖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∞)
have 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 : ℝ)
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 : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C
n : ℕ
hr : r = 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 : ℝ)
have 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 : ℝ)
Tactic: rw [hr]
-- 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 : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C
n : ℕ
hr : r = 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 : ℝ)
have 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 : ℝ)
Tactic: cases n
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 : ℕ), ‖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 : ℝ)
⊢ 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 : ℝ)
have 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 : ℝ)
Tactic: cases n
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 : ℕ), ‖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 ≤
      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 : ℝ)
have 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 : ℝ)
Tactic: right
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (hypothesis)
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 ≤
    C / (↑r : ℝ)
have hr₁ : 0 < (↑r : ℝ)
Tactic: rw [← NNReal.coe_pos] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (hypothesis)
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 ≤
    C / (↑r : ℝ)
have 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
Tactic: specialize h (n + 1)
Cleared hypotheses: h
-- 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 : ℝ
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
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) * (↑r : ℝ) ^ n ≤
    C / (↑r : ℝ)
have 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
Tactic: rw [le_div_iff₀ hr]
-- 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 : ℝ
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
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) * (↑r : ℝ) ^ n *
      (↑r : ℝ) ≤
    C
have 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
Tactic: rwa [pow_succ, ← mul_assoc] at h
Cleared hypotheses: h
-- 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 : ℝ
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
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) * (↑r : ℝ) ^ n *
      (↑r : ℝ) ≤
    C
have 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
Tactic: rwa [pow_succ, ← mul_assoc] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (hypothesis)
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 : ℕ
⊢ 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 : ℝ)
have x : 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
-- 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 (E →L[𝕜] F)
z : F
⊢ (p.unshift z).radius = p.radius (𝕜 := 𝕜) (E := E) (F := E →L[𝕜] F)
have rw : (p.unshift z).shift.radius (𝕜 := 𝕜) (E := E) (F := E →L[𝕜] F) = p.radius (𝕜 := 𝕜) (E := E) (F := E →L[𝕜] F)
Tactic: rw [← radius_shift, unshift_shift]
-- 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 (E →L[𝕜] F)
z : F
rw : (p.unshift z).shift.radius (𝕜 := 𝕜) (E := E) (F := E →L[𝕜] F) = p.radius (𝕜 := 𝕜) (E := E) (F := E →L[𝕜] F)
⊢ (p.unshift z).radius = p.radius (𝕜 := 𝕜) (E := E) (F := E →L[𝕜] F)
have rw₁ : p.radius (𝕜 := 𝕜) (E := E) (F := E →L[𝕜] F) = p.radius (𝕜 := 𝕜) (E := E) (F := E →L[𝕜] F)
Tactic: rw [← radius_shift, unshift_shift]
-- 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 𝕜 E F
f : F →L[𝕜] G
⊢ p.radius ≤ radius (f.compFormalMultilinearSeries p)
have refine : ∀ (r : ℝ≥0) (hr : (↑r : ℝ≥0∞) < p.radius), (↑r : ℝ≥0∞) ≤ radius (f.compFormalMultilinearSeries p)
Tactic: refine ENNReal.le_of_forall_nnreal_lt fun r hr => ?_
-- 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 𝕜 E F
f : F →L[𝕜] G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
⊢ (↑r : ℝ≥0∞) ≤ radius (f.compFormalMultilinearSeries p)
have h : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖f.compFormalMultilinearSeries p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ 1
Tactic: apply le_radius_of_isBigO
-- 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 𝕜 E F
f : F →L[𝕜] G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖f.compFormalMultilinearSeries p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ 1
have apply : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖f.compFormalMultilinearSeries p n‖ * (↑r : ℝ) ^ n) fun (n : ℕ) ↦
  ‖p n‖ * (↑r : ℝ) ^ n
Tactic: apply (IsBigO.trans_isLittleO _ (p.isLittleO_one_of_lt_radius hr)).isBigO
-- 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 𝕜 E F
f : F →L[𝕜] G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖f.compFormalMultilinearSeries p n‖ * (↑r : ℝ) ^ n) fun (n : ℕ) ↦
    ‖p n‖ * (↑r : ℝ) ^ n
have refine : IsBigOWith (E := ℝ) (F := ℝ) ‖f‖ atTop (fun (n : ℕ) ↦ ‖f.compFormalMultilinearSeries p n‖) fun (n : ℕ) ↦ ‖p n‖
Tactic: refine IsBigO.mul (@IsBigOWith.isBigO _ _ _ _ _ ‖f‖ _ _ _ ?_) (isBigO_refl _ _)
-- 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 𝕜 E F
f : F →L[𝕜] G
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
⊢ IsBigOWith (E := ℝ) (F := ℝ) ‖f‖ atTop (fun (n : ℕ) ↦ ‖f.compFormalMultilinearSeries p n‖) fun (n : ℕ) ↦ ‖p n‖
have refine : ∀ (n : ℕ), ‖‖f.compFormalMultilinearSeries p n‖‖ ≤ ‖f‖ * ‖‖p n‖‖
Tactic: refine IsBigOWith.of_bound (Eventually.of_forall fun n => ?_)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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
i : E ≃L[𝕜] F
x : E
⊢ p.leftInv i x 0 = ContinuousMultilinearMap.uncurry0 𝕜 F x
have rw : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin 0) ↦ F) E)
  (ContinuousMultilinearMap.uncurry0 𝕜 F x) (ContinuousMultilinearMap.uncurry0 𝕜 F x)
Tactic: rw [leftInv]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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
i : E ≃L[𝕜] F
x : E
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin 1) ↦ F) E) (p.leftInv i x 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 F E) :
        (a : F →L[𝕜] E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ F) E)
      (↑i.symm : F →L[𝕜] E))
have rw : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin 1) ↦ F) E)
  ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 F E) :
        (a : F →L[𝕜] E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ F) E)
      (↑i.symm : F →L[𝕜] E) :
    ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin 1) ↦ F) E)
  ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 F E) :
        (a : F →L[𝕜] E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ F) E)
      (↑i.symm : F →L[𝕜] E) :
    ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin 1) ↦ F) E)
Tactic: rw [leftInv]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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
i : E ≃L[𝕜] F
x : E
⊢ p.removeZero.leftInv i x = p.leftInv i x
have h : ∀ (n : ℕ), p.removeZero.leftInv i x n = p.leftInv i x n
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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
i : E ≃L[𝕜] F
x : E
n : ℕ
⊢ p.removeZero.leftInv i x n = p.leftInv i x n
have h : ∀ (n : ℕ) (IH : ∀ m < n, p.removeZero.leftInv i x m = p.leftInv i x m), p.removeZero.leftInv i x n = p.leftInv i x n
Tactic: induction n using Nat.strongRec' with | _ n IH
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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
i : E ≃L[𝕜] F
x : E
n_1 n : ℕ
IH : ∀ m < n + 2, p.removeZero.leftInv i x m = p.leftInv i x m
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (n + 2)) ↦ F) E)
    (p.removeZero.leftInv i x (n + 2)) (p.leftInv i x (n + 2))
have simp : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (n + 2)) ↦ F) E)
  (∑ c : { c : Composition (n + 2) // c.length < n + 2 },
    ContinuousMultilinearMap.compAlongComposition (p.removeZero.compContinuousLinearMap (↑i.symm : F →L[𝕜] E))
      (↑c : Composition (n + 2)) (p.removeZero.leftInv i x (↑c : Composition (n + 2)).length))
  (∑ c : { c : Composition (n + 2) // c.length < n + 2 },
    ContinuousMultilinearMap.compAlongComposition (p.compContinuousLinearMap (↑i.symm : F →L[𝕜] E))
      (↑c : Composition (n + 2)) (p.leftInv i x (↑c : Composition (n + 2)).length))
Tactic: simp only [leftInv, neg_inj]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Inverse (goal)
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
i : E ≃L[𝕜] F
x : E
n_1 n : ℕ
IH : ∀ m < n + 2, p.removeZero.leftInv i x m = p.leftInv i x m
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_3, u_2} 𝕜 (fun (i : Fin (n + 2)) ↦ F) E)
    (∑ c : { c : Composition (n + 2) // c.length < n + 2 },
      ContinuousMultilinearMap.compAlongComposition (p.removeZero.compContinuousLinearMap (↑i.symm : F →L[𝕜] E))
        (↑c : Composition (n + 2)) (p.removeZero.leftInv i x (↑c : Composition (n + 2)).length))
    (∑ c : { c : Composition (n + 2) // c.length < n + 2 },
      ContinuousMultilinearMap.compAlongComposition (p.compContinuousLinearMap (↑i.symm : F →L[𝕜] E))
        (↑c : Composition (n + 2)) (p.leftInv i x (↑c : Composition (n + 2)).length))
have refine : ∀ (c : { c : Composition (n + 2) // c.length < n + 2 })
  (cuniv : Membership.mem (γ := Finset { c : Composition (n + 2) // c.length < n + 2 }) univ c),
  ContinuousMultilinearMap.compAlongComposition (p.removeZero.compContinuousLinearMap (↑i.symm : F →L[𝕜] E))
      (↑c : Composition (n + 2)) (p.removeZero.leftInv i x (↑c : Composition (n + 2)).length) =
    ContinuousMultilinearMap.compAlongComposition (p.compContinuousLinearMap (↑i.symm : F →L[𝕜] E))
      (↑c : Composition (n + 2)) (p.leftInv i x (↑c : Composition (n + 2)).length)
Tactic: refine Finset.sum_congr rfl fun c cuniv => ?_