awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
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
⊢ ‖u‖ₑ ≠ ∞

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
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
inr : (↑(r / ‖u‖₊) : ℝ≥0∞) ≤ radius (p.compContinuousLinearMap u)
⊢ (↑r : ℝ≥0∞) ≤ radius (p.compContinuousLinearMap u) * ‖u‖ₑ

Tactic:
rw [← ENNReal.div_le_iff (by simpa using h_zero) (by simp), enorm_eq_nnnorm, ← coe_div h_zero.ne']

Premises used: LT.lt.ne', ENNReal.div_le_iff, enorm_eq_nnnorm, ENNReal.coe_div
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
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
inr :
  ∀ (C : ℝ) (hC_pos : C > 0) (hC : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C),
    (↑(r / ‖u‖₊) : ℝ≥0∞) ≤ radius (p.compContinuousLinearMap u)
⊢ (↑(r / ‖u‖₊) : ℝ≥0∞) ≤ radius (p.compContinuousLinearMap u)

Tactic:
obtain ⟨C, hC_pos, hC⟩ := p.norm_mul_pow_le_of_lt_radius hr

Premises used: FormalMultilinearSeries.norm_mul_pow_le_of_lt_radius
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
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
⊢ (↑(r / ‖u‖₊) : ℝ≥0∞) ≤ radius (p.compContinuousLinearMap u)

Tactic:
le_radius_of_bound _ C fun n ↦ ?_

Premises used: FormalMultilinearSeries.le_radius_of_bound
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
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
inr : ∀ (n : ℕ), ‖p.compContinuousLinearMap u n‖ * (↑(r / ‖u‖₊) : ℝ) ^ n ≤ C
⊢ (↑(r / ‖u‖₊) : ℝ≥0∞) ≤ radius (p.compContinuousLinearMap u)

Tactic:
refine le_radius_of_bound _ C fun n ↦ ?_

Premises used: FormalMultilinearSeries.le_radius_of_bound
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
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 : ℕ
hbc : ‖p.compContinuousLinearMap u n‖ ≤ ‖p n‖ * ‖u‖ ^ n
⊢ ‖p.compContinuousLinearMap u n‖ * (↑(r / ‖u‖₊) : ℝ) ^ n ≤ ‖p n‖ * ‖u‖ ^ n * (↑(r / ‖u‖₊) : ℝ) ^ n

Tactic:
gcongr
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
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‖ ≤ ‖p n‖ * ‖u‖ ^ n

Tactic:
nnnorm_compContinuousLinearMap_le p u n

Premises used: FormalMultilinearSeries.nnnorm_compContinuousLinearMap_le
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
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‖ ≤ ‖p n‖ * ‖u‖ ^ n

Tactic:
exact nnnorm_compContinuousLinearMap_le p u n

Premises used: FormalMultilinearSeries.nnnorm_compContinuousLinearMap_le
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
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 : ℕ
simp : ‖p n‖ * (‖u‖ ^ n * ((↑r : ℝ) ^ n / ‖u‖ ^ n)) = ‖p n‖ * (↑r : ℝ) ^ n
⊢ ‖p n‖ * ‖u‖ ^ n * (↑(r / ‖u‖₊) : ℝ) ^ n = ‖p n‖ * (↑r : ℝ) ^ n

Tactic:
simp only [NNReal.coe_div, coe_nnnorm, div_pow, mul_assoc]

Premises used: NNReal.coe_div, mul_assoc, coe_nnnorm, div_pow
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
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 : ℕ
hb : ‖u‖ ^ n ≠ 0
⊢ ‖p n‖ * (‖u‖ ^ n * ((↑r : ℝ) ^ n / ‖u‖ ^ n)) = ‖p n‖ * (↑r : ℝ) ^ n

Tactic:
rw [mul_div_cancel₀]

Premises used: mul_div_cancel₀
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
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 : ℕ
hb :
  ∀ (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‖ ^ n ≠ 0
⊢ ‖u‖ ^ n ≠ 0

Tactic:
rw [← NNReal.coe_pos] at h_zero

Premises used: NNReal.coe_pos
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
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‖ ^ n ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
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 n‖ * (↑r : ℝ) ^ n ≤ C

Tactic:
hC n
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
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
u₂ : ‖p n‖ * ‖u‖ ^ n * (↑(r / ‖u‖₊) : ℝ) ^ n = ‖p n‖ * (↑r : ℝ) ^ n
⊢ ‖p.compContinuousLinearMap u n‖ * (↑(r / ‖u‖₊) : ℝ) ^ n ≤ C

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

Premises used: NNNorm.nnnorm, FormalMultilinearSeries.compContinuousLinearMap, HDiv.hDiv
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
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)
inr : ∀ (h : Nontrivial E), p.radius ≤ radius (p.compContinuousLinearMap u.toContinuousLinearMap)
⊢ p.radius ≤ radius (p.compContinuousLinearMap u.toContinuousLinearMap)

Tactic:
obtain (h | h) := subsingleton_or_nontrivial E

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
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
h : Subsingleton E
⊢ p.radius ≤ radius (p.compContinuousLinearMap u.toContinuousLinearMap)

Tactic:
simp [Subsingleton.elim u.toContinuousLinearMap 0]

Premises used: Subsingleton.elim, OfNat.ofNat, LinearIsometry.toContinuousLinearMap
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
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
h : Nontrivial E
⊢ p.radius ≤ radius (p.compContinuousLinearMap u.toContinuousLinearMap)

Tactic:
simpa [u.norm_toContinuousLinearMap]
      using div_le_radius_compContinuousLinearMap p u.toContinuousLinearMap

Premises used: LinearIsometry.norm_toContinuousLinearMap, FormalMultilinearSeries.div_le_radius_compContinuousLinearMap, LinearIsometry.toContinuousLinearMap
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
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)‖ₑ ≤
    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
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
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

Tactic:
simp only [compContinuousLinearMap_comp, ContinuousLinearEquiv.coe_comp_coe_symm,
    compContinuousLinearMap_id] at this

Premises used: ContinuousLinearEquiv.coe_comp_coe_symm, FormalMultilinearSeries.compContinuousLinearMap_id, FormalMultilinearSeries.compContinuousLinearMap_comp
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
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
⊢ ‖(↑u.symm : F →L[𝕜] E)‖ₑ ≠ ∞

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
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
rwa rwa₁ rwa₂ 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
⊢ 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

Premises used: ENNReal.div_le_iff'
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
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

Tactic:
le_antisymm ?_ <| le_radius_compContinuousLinearMap _ _

Premises used: FormalMultilinearSeries.le_radius_compContinuousLinearMap, le_antisymm
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
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
refine : radius (p.compContinuousLinearMap u.toLinearIsometry.toContinuousLinearMap) ≤ p.radius
⊢ radius (p.compContinuousLinearMap u.toLinearIsometry.toContinuousLinearMap) = p.radius

Tactic:
refine le_antisymm ?_ <| le_radius_compContinuousLinearMap _ _

Premises used: FormalMultilinearSeries.le_radius_compContinuousLinearMap, le_antisymm
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
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
⊢ Nontrivial F

Tactic:
have _ : Nontrivial F := u.symm.toEquiv.nontrivial
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
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 : E ≃L[𝕜] F) : E →L[𝕜] F)) ≤
    ‖(↑(↑u : E ≃L[𝕜] F).symm : F →L[𝕜] E)‖ₑ * p.radius

Tactic:
radius_compContinuousLinearMap_le p u.toContinuousLinearEquiv

Premises used: FormalMultilinearSeries.radius_compContinuousLinearMap_le, LinearIsometryEquiv.toContinuousLinearEquiv
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
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_1 : Nontrivial F
h : p.radius = ‖(↑(↑u : E ≃L[𝕜] F).symm : F →L[𝕜] E)‖ₑ * p.radius
⊢ radius (p.compContinuousLinearMap u.toLinearIsometry.toContinuousLinearMap) ≤ p.radius

Tactic:
convert! radius_compContinuousLinearMap_le p u.toContinuousLinearEquiv

Premises used: FormalMultilinearSeries.radius_compContinuousLinearMap_le, LinearIsometryEquiv.toContinuousLinearEquiv
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
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
⊢ (↑(↑u : E ≃L[𝕜] F).symm : F →L[𝕜] E) = u.symm.toLinearIsometry.toContinuousLinearMap

Tactic:
have : u.toContinuousLinearEquiv.symm.toContinuousLinearMap =
    u.symm.toLinearIsometry.toContinuousLinearMap := rfl
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
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
this : (↑(↑u : E ≃L[𝕜] F).symm : F →L[𝕜] E) = u.symm.toLinearIsometry.toContinuousLinearMap
⊢ p.radius = ‖(↑(↑u : E ≃L[𝕜] F).symm : F →L[𝕜] E)‖ₑ * p.radius

Tactic:
simp [this]
-- Module: Mathlib.Analysis.Analytic.ConvergenceRadius
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 →L[𝕜] F
hu_iso : Isometry.{u_2, u_3} (α := E) (β := F) (⇑u : (a : E) → F)
hu_surj : Function.Surjective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑u : (a : E) → F)
⊢ radius (p.compContinuousLinearMap u) = p.radius

Tactic:
let v : E ≃ₗᵢ[𝕜] F :=
    { LinearEquiv.ofBijective u.toLinearMap ⟨hu_iso.injective, hu_surj⟩ with
      norm_map' := hu_iso.norm_map_of_map_zero (map_zero u) }
  radius_compContinuousLinearMap_linearIsometryEquiv_eq p v

Premises used: map_zero, ContinuousLinearMap.toLinearMap, FormalMultilinearSeries.radius_compContinuousLinearMap_linearIsometryEquiv_eq, Isometry.injective, LinearIsometryEquiv.mk, Isometry.norm_map_of_map_zero, And.intro, LinearEquiv.ofBijective, LinearIsometry.toContinuousLinearMap
-- 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
inst_5 : Nontrivial E
p : FormalMultilinearSeries 𝕜 E F
⊢ radius (p.compContinuousLinearMap (-ContinuousLinearMap.id 𝕜 E)) = p.radius

Tactic:
radius_compContinuousLinearMap_linearIsometryEquiv_eq _ (.neg 𝕜)

Premises used: FormalMultilinearSeries.radius_compContinuousLinearMap_linearIsometryEquiv_eq, LinearIsometryEquiv.neg, LinearIsometry.toContinuousLinearMap
-- 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
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∞))
⊢ p.shift.radius (𝕜 := 𝕜) (E := E) (F := E →L[𝕜] F) = p.radius

Tactic:
simp only [radius, shift, Nat.succ_eq_add_one, ContinuousMultilinearMap.curryRight_norm]

Premises used: Nat.succ_eq_add_one, ContinuousMultilinearMap.curryRight_norm, FormalMultilinearSeries.radius, FormalMultilinearSeries.shift
-- 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
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∞)
⊢ 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:
congr
-- 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
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∞))
⊢ 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:
ext r