awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E × F → G
x : E
s : Set (E × F)
fa : AnalyticOn 𝕜 f s
⊢ AnalyticOn.{u_2, u_4, u_5} 𝕜 (F := G) (fun (y : F) ↦ f (x, y)) {y : F | (x, y) ∈ s}

Tactic:
fun y m ↦ (fa (x, y) m).curry_right

Premises used: AnalyticOn, Set.Mem, setOf, AnalyticWithinAt.curry_right, Prod.mk
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
i : ι
apply :
  ∀ (r' : ℝ≥0) (hr' : (↑r' : ℝ≥0∞) < radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)),
    (↑r' : ℝ≥0∞) ≤ (p i).radius
⊢ radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p) ≤ (p i).radius

Tactic:
apply le_of_forall_nnreal_lt (fun r' hr' ↦ ?_)

Premises used: ENNReal.le_of_forall_nnreal_lt
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
i : ι
r' : ℝ≥0
hr' : (↑r' : ℝ≥0∞) < radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)
⊢ ∃ C > 0, ∀ (n : ℕ), ‖pi (F := Fm) p n‖ * (↑r' : ℝ) ^ n ≤ C

Tactic:
norm_mul_pow_le_of_lt_radius _ hr'

Premises used: FormalMultilinearSeries.norm_mul_pow_le_of_lt_radius
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
i : ι
r' : ℝ≥0
hr' : (↑r' : ℝ≥0∞) < radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)
obtain : ∀ (C : ℝ) (hC : ∀ (n : ℕ), ‖pi (F := Fm) p n‖ * (↑r' : ℝ) ^ n ≤ C), (↑r' : ℝ≥0∞) ≤ (p i).radius
⊢ (↑r' : ℝ≥0∞) ≤ (p i).radius

Tactic:
obtain ⟨C, -, hC⟩ : ∃ C > 0, ∀ n, ‖pi p n‖ * ↑r' ^ n ≤ C := norm_mul_pow_le_of_lt_radius _ hr'

Premises used: FormalMultilinearSeries.norm_mul_pow_le_of_lt_radius
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
i : ι
r' : ℝ≥0
hr' : (↑r' : ℝ≥0∞) < radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)
C : ℝ
hC : ∀ (n : ℕ), ‖pi (F := Fm) p n‖ * (↑r' : ℝ) ^ n ≤ C
apply : ∀ (n : ℕ), ‖p i n‖ * (↑r' : ℝ) ^ n ≤ C
⊢ (↑r' : ℝ≥0∞) ≤ (p i).radius

Tactic:
apply le_radius_of_bound _ C (fun n ↦ ?_)

Premises used: FormalMultilinearSeries.le_radius_of_bound
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
i : ι
r' : ℝ≥0
hr' : (↑r' : ℝ≥0∞) < radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)
C : ℝ
hC : ∀ (n : ℕ), ‖pi (F := Fm) p n‖ * (↑r' : ℝ) ^ n ≤ C
n : ℕ
apply : ‖p i n‖ * (↑r' : ℝ) ^ n ≤ ‖pi (F := Fm) p n‖ * (↑r' : ℝ) ^ n
⊢ ‖p i n‖ * (↑r' : ℝ) ^ n ≤ C

Tactic:
apply le_trans _ (hC n)

Premises used: le_trans
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
i : ι
r' : ℝ≥0
hr' : (↑r' : ℝ≥0∞) < radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)
C : ℝ
hC : ∀ (n : ℕ), ‖pi (F := Fm) p n‖ * (↑r' : ℝ) ^ n ≤ C
n : ℕ
hbc : ‖p i n‖ ≤ ‖pi (F := Fm) p n‖
⊢ ‖p i n‖ * (↑r' : ℝ) ^ n ≤ ‖pi (F := Fm) p n‖ * (↑r' : ℝ) ^ n

Tactic:
gcongr
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
i : ι
r' : ℝ≥0
hr' : (↑r' : ℝ≥0∞) < radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)
C : ℝ
hC : ∀ (n : ℕ), ‖pi (F := Fm) p n‖ * (↑r' : ℝ) ^ n ≤ C
n : ℕ
hbc :
  ‖p i n‖ ≤
    norm (E := (i' : ι) → ContinuousMultilinearMap.{u_2, 0, u_3, u_10} 𝕜 (fun (i : Fin n) ↦ E) (Fm i')) fun (i : ι) ↦
      p i n
⊢ ‖p i n‖ ≤ ‖pi (F := Fm) p n‖

Tactic:
rw [pi, ContinuousMultilinearMap.opNorm_pi]

Premises used: ContinuousMultilinearMap.opNorm_pi, FormalMultilinearSeries.pi
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
i : ι
r' : ℝ≥0
hr' : (↑r' : ℝ≥0∞) < radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)
C : ℝ
hC : ∀ (n : ℕ), ‖pi (F := Fm) p n‖ * (↑r' : ℝ) ^ n ≤ C
n : ℕ
⊢ ‖p i n‖ ≤
    norm (E := (i' : ι) → ContinuousMultilinearMap.{u_2, 0, u_3, u_10} 𝕜 (fun (i : Fin n) ↦ E) (Fm i')) fun (i : ι) ↦
      p i n

Tactic:
norm_le_pi_norm (fun i ↦ p i n) i

Premises used: norm_le_pi_norm
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
i : ι
r' : ℝ≥0
hr' : (↑r' : ℝ≥0∞) < radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)
C : ℝ
hC : ∀ (n : ℕ), ‖pi (F := Fm) p n‖ * (↑r' : ℝ) ^ n ≤ C
n : ℕ
⊢ ‖p i n‖ ≤
    norm (E := (i' : ι) → ContinuousMultilinearMap.{u_2, 0, u_3, u_10} 𝕜 (fun (i : Fin n) ↦ E) (Fm i')) fun (i : ι) ↦
      p i n

Tactic:
exact norm_le_pi_norm (fun i ↦ p i n) i

Premises used: norm_le_pi_norm
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
h : ∀ (i : ι), r ≤ (p i).radius
apply :
  ∀ (r' : ℝ≥0) (hr' : (↑r' : ℝ≥0∞) < r), (↑r' : ℝ≥0∞) ≤ radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)
⊢ r ≤ radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)

Tactic:
apply le_of_forall_nnreal_lt (fun r' hr' ↦ ?_)

Premises used: ENNReal.le_of_forall_nnreal_lt
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
h : ∀ (i : ι), r ≤ (p i).radius
r' : ℝ≥0
hr' : (↑r' : ℝ≥0∞) < r
⊢ ∀ (i : ι), ∃ C > 0, ∀ (n : ℕ), ‖p i n‖ * (↑r' : ℝ) ^ n ≤ C

Tactic:
have I i : ∃ C > 0, ∀ n, ‖p i n‖ * (r' : ℝ) ^ n ≤ C :=
    norm_mul_pow_le_of_lt_radius _ (hr'.trans_le (h i))
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
h : ∀ (i : ι), r ≤ (p i).radius
r' : ℝ≥0
hr' : (↑r' : ℝ≥0∞) < r
I : ∀ (i : ι), ∃ C > 0, ∀ (n : ℕ), ‖p i n‖ * (↑r' : ℝ) ^ n ≤ C
choose :
  ∀ (C : (i : ι) → ℝ) (C_pos : ∀ (i : ι), C i > 0) (hC : ∀ (i : ι) (n : ℕ), ‖p i n‖ * (↑r' : ℝ) ^ n ≤ C i),
    (↑r' : ℝ≥0∞) ≤ radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)
⊢ (↑r' : ℝ≥0∞) ≤ radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)

Tactic:
choose C C_pos hC using I
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
h : ∀ (i : ι), r ≤ (p i).radius
r' : ℝ≥0
hr' : (↑r' : ℝ≥0∞) < r
C : (i : ι) → ℝ
C_pos : ∀ (i : ι), C i > 0
hC : ∀ (i : ι) (n : ℕ), ‖p i n‖ * (↑r' : ℝ) ^ n ≤ C i
⊢ ∃ D ≥ 0, ∀ (i : ι), C i ≤ D

Tactic:
⟨∑ i, C i, Finset.sum_nonneg (fun i _ ↦ (C_pos i).le),
      fun i ↦ Finset.single_le_sum (fun j _ ↦ (C_pos j).le) (Finset.mem_univ _)⟩

Premises used: Finset.mem_univ, Finset.univ, LT.lt.le, Finset.sum_nonneg, And.intro, Exists.intro, Finset.single_le_sum, Finset.sum
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
h : ∀ (i : ι), r ≤ (p i).radius
r' : ℝ≥0
hr' : (↑r' : ℝ≥0∞) < r
C : (i : ι) → ℝ
C_pos : ∀ (i : ι), C i > 0
hC : ∀ (i : ι) (n : ℕ), ‖p i n‖ * (↑r' : ℝ) ^ n ≤ C i
obtain :
  ∀ (D : ℝ) (D_nonneg : D ≥ 0) (hD : ∀ (i : ι), C i ≤ D),
    (↑r' : ℝ≥0∞) ≤ radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)
⊢ (↑r' : ℝ≥0∞) ≤ radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)

Tactic:
obtain ⟨D, D_nonneg, hD⟩ : ∃ D ≥ 0, ∀ i, C i ≤ D :=
    ⟨∑ i, C i, Finset.sum_nonneg (fun i _ ↦ (C_pos i).le),
      fun i ↦ Finset.single_le_sum (fun j _ ↦ (C_pos j).le) (Finset.mem_univ _)⟩
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
h : ∀ (i : ι), r ≤ (p i).radius
r' : ℝ≥0
hr' : (↑r' : ℝ≥0∞) < r
C : (i : ι) → ℝ
C_pos : ∀ (i : ι), C i > 0
hC : ∀ (i : ι) (n : ℕ), ‖p i n‖ * (↑r' : ℝ) ^ n ≤ C i
D : ℝ
D_nonneg : D ≥ 0
hD : ∀ (i : ι), C i ≤ D
apply : ∀ (n : ℕ), ‖pi (F := Fm) p n‖ * (↑r' : ℝ) ^ n ≤ D
⊢ (↑r' : ℝ≥0∞) ≤ radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)

Tactic:
apply le_radius_of_bound _ D (fun n ↦ ?_)

Premises used: FormalMultilinearSeries.le_radius_of_bound
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
h : ∀ (i : ι), r ≤ (p i).radius
r' : ℝ≥0
hr' : (↑r' : ℝ≥0∞) < r
C : (i : ι) → ℝ
C_pos : ∀ (i : ι), C i > 0
hC : ∀ (i : ι) (n : ℕ), ‖p i n‖ * (↑r' : ℝ) ^ n ≤ C i
D : ℝ
D_nonneg : D ≥ 0
hD : ∀ (i : ι), C i ≤ D
n : ℕ
inl : ∀ (hr' : (↑r' : ℝ) ^ n ≤ 0), ‖pi (F := Fm) p n‖ * (↑r' : ℝ) ^ n ≤ D
inr : ∀ (hr' : 0 < (↑r' : ℝ) ^ n), ‖pi (F := Fm) p n‖ * (↑r' : ℝ) ^ n ≤ D
⊢ ‖pi (F := Fm) p n‖ * (↑r' : ℝ) ^ n ≤ D

Tactic:
rcases le_or_gt ((r' : ℝ) ^ n) 0 with hr' | hr'

Premises used: le_or_gt, HPow.hPow, OfNat.ofNat, NNReal.toReal
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
h : ∀ (i : ι), r ≤ (p i).radius
r' : ℝ≥0
hr'_1 : (↑r' : ℝ≥0∞) < r
C : (i : ι) → ℝ
C_pos : ∀ (i : ι), C i > 0
hC : ∀ (i : ι) (n : ℕ), ‖p i n‖ * (↑r' : ℝ) ^ n ≤ C i
D : ℝ
D_nonneg : D ≥ 0
hD : ∀ (i : ι), C i ≤ D
n : ℕ
hr' : (↑r' : ℝ) ^ n ≤ 0
⊢ 0 ≤ ‖pi (F := Fm) p n‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
h : ∀ (i : ι), r ≤ (p i).radius
r' : ℝ≥0
hr'_1 : (↑r' : ℝ≥0∞) < r
C : (i : ι) → ℝ
C_pos : ∀ (i : ι), C i > 0
hC : ∀ (i : ι) (n : ℕ), ‖p i n‖ * (↑r' : ℝ) ^ n ≤ C i
D : ℝ
D_nonneg : D ≥ 0
hD : ∀ (i : ι), C i ≤ D
n : ℕ
hr' : (↑r' : ℝ) ^ n ≤ 0
⊢ ‖pi (F := Fm) p n‖ * (↑r' : ℝ) ^ n ≤ D

Tactic:
exact le_trans (mul_nonpos_of_nonneg_of_nonpos (by positivity) hr') D_nonneg

Premises used: mul_nonpos_of_nonneg_of_nonpos, le_trans
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
h : ∀ (i : ι), r ≤ (p i).radius
r' : ℝ≥0
hr'_1 : (↑r' : ℝ≥0∞) < r
C : (i : ι) → ℝ
C_pos : ∀ (i : ι), C i > 0
hC : ∀ (i : ι) (n : ℕ), ‖p i n‖ * (↑r' : ℝ) ^ n ≤ C i
D : ℝ
D_nonneg : D ≥ 0
hD : ∀ (i : ι), C i ≤ D
n : ℕ
hr' : 0 < (↑r' : ℝ) ^ n
⊢ 0 ≤ D / (↑r' : ℝ) ^ n

Tactic:
positivity
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
h : ∀ (i : ι), r ≤ (p i).radius
r' : ℝ≥0
hr'_1 : (↑r' : ℝ≥0∞) < r
C : (i : ι) → ℝ
C_pos : ∀ (i : ι), C i > 0
hC : ∀ (i : ι) (n : ℕ), ‖p i n‖ * (↑r' : ℝ) ^ n ≤ C i
D : ℝ
D_nonneg : D ≥ 0
hD : ∀ (i : ι), C i ≤ D
n : ℕ
hr' : 0 < (↑r' : ℝ) ^ n
inr : ∀ (i : ι), ‖p i n‖ ≤ D / (↑r' : ℝ) ^ n
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) ((i : ι) → Fm i))
        (ContinuousMultilinearMap.pi (M₁ := fun (i : Fin n) ↦ E) (M' := Fm) fun (i : ι) ↦ p i n :
          ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) ((i : ι) → Fm i)) *
      (↑r' : ℝ) ^ n ≤
    D

Tactic:
rw [← le_div_iff₀ hr', ContinuousMultilinearMap.opNorm_pi,
      pi_norm_le_iff_of_nonneg (by positivity)]

Premises used: pi_norm_le_iff_of_nonneg, ContinuousMultilinearMap.opNorm_pi, le_div_iff₀
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
h : ∀ (i : ι), r ≤ (p i).radius
r' : ℝ≥0
hr'_1 : (↑r' : ℝ≥0∞) < r
C : (i : ι) → ℝ
C_pos : ∀ (i : ι), C i > 0
hC : ∀ (i : ι) (n : ℕ), ‖p i n‖ * (↑r' : ℝ) ^ n ≤ C i
D : ℝ
D_nonneg : D ≥ 0
hD : ∀ (i : ι), C i ≤ D
n : ℕ
hr' : 0 < (↑r' : ℝ) ^ n
i : ι
⊢ ‖p i n‖ ≤ D / (↑r' : ℝ) ^ n

Tactic:
(le_div_iff₀ hr').2 ((hC i n).trans (hD i))

Premises used: Iff.mpr, LE.le.trans, le_div_iff₀
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
h : ∀ (i : ι), r ≤ (p i).radius
r' : ℝ≥0
hr'_1 : (↑r' : ℝ≥0∞) < r
C : (i : ι) → ℝ
C_pos : ∀ (i : ι), C i > 0
hC : ∀ (i : ι) (n : ℕ), ‖p i n‖ * (↑r' : ℝ) ^ n ≤ C i
D : ℝ
D_nonneg : D ≥ 0
hD : ∀ (i : ι), C i ≤ D
n : ℕ
hr' : 0 < (↑r' : ℝ) ^ n
i : ι
⊢ ‖p i n‖ ≤ D / (↑r' : ℝ) ^ n

Tactic:
exact (le_div_iff₀ hr').2 ((hC i n).trans (hD i))

Premises used: Iff.mpr, LE.le.trans, le_div_iff₀
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
⊢ radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p) ≤ ⨅ (i : ι), (p i).radius

Tactic:
simp [radius_pi_le]

Premises used: FormalMultilinearSeries.radius_pi_le
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
refine : ⨅ (i : ι), (p i).radius ≤ radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)
⊢ radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p) = ⨅ (i : ι), (p i).radius

Tactic:
refine le_antisymm (by simp [radius_pi_le]) ?_

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
apply :
  ∀ (r' : ℝ≥0) (hr' : (↑r' : ℝ≥0∞) < ⨅ (i : ι), (p i).radius),
    (↑r' : ℝ≥0∞) ≤ radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)
⊢ ⨅ (i : ι), (p i).radius ≤ radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)

Tactic:
apply le_of_forall_nnreal_lt (fun r' hr' ↦ ?_)

Premises used: ENNReal.le_of_forall_nnreal_lt
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
r' : ℝ≥0
hr' : (↑r' : ℝ≥0∞) < ⨅ (i : ι), (p i).radius
⊢ (↑r' : ℝ≥0∞) ≤ radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)

Tactic:
le_radius_pi (fun i ↦ le_iInf_iff.1 hr'.le i)

Premises used: le_iInf_iff, LT.lt.le, Iff.mp, FormalMultilinearSeries.le_radius_pi
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
r' : ℝ≥0
hr' : (↑r' : ℝ≥0∞) < ⨅ (i : ι), (p i).radius
⊢ (↑r' : ℝ≥0∞) ≤ radius (𝕜 := 𝕜) (E := E) (F := (i : ι) → Fm i) (pi (F := Fm) p)

Tactic:
exact le_radius_pi (fun i ↦ le_iInf_iff.1 hr'.le i)

Premises used: le_iInf_iff, LT.lt.le, Iff.mp, FormalMultilinearSeries.le_radius_pi
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
e : E
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
hf : ∀ (i : ι), HasFPowerSeriesWithinOnBall (f i) (p i) s e r
hr : 0 < r
apply : ∀ (i : ι), r ≤ (p i).radius
⊢ r ≤ FormalMultilinearSeries.radius (𝕜 := 𝕜) (E := E) (F := (x : ι) → Fm x) (FormalMultilinearSeries.pi (F := Fm) p)

Tactic:
apply FormalMultilinearSeries.le_radius_pi (fun i ↦ ?_)

Premises used: FormalMultilinearSeries.le_radius_pi
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
e : E
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
hf : ∀ (i : ι), HasFPowerSeriesWithinOnBall (f i) (p i) s e r
hr : 0 < r
i : ι
⊢ r ≤ (p i).radius

Tactic:
(hf i).r_le

Premises used: HasFPowerSeriesWithinOnBall.r_le
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
e : E
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
hf : ∀ (i : ι), HasFPowerSeriesWithinOnBall (f i) (p i) s e r
hr : 0 < r
i : ι
⊢ r ≤ (p i).radius

Tactic:
exact (hf i).r_le

Premises used: HasFPowerSeriesWithinOnBall.r_le
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_9
inst_3 : Fintype ι
e : E
Fm : ι → Type u_10
inst_4 : (i : ι) → NormedAddCommGroup (Fm i)
inst_5 : (i : ι) → NormedSpace.{u_2, u_10} 𝕜 (Fm i)
f : (i : ι) → E → Fm i
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries.{u_2, u_3, u_10} 𝕜 E (Fm i)
hf : ∀ (i : ι), HasFPowerSeriesOnBall (f i) (p i) e r
hr : 0 < r
simp_rw :
  ∀ (hf : ∀ (i : ι), HasFPowerSeriesWithinOnBall (f i) (p i) Set.univ e r),
    HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x)
      (FormalMultilinearSeries.pi (F := Fm) p) Set.univ e r
⊢ HasFPowerSeriesOnBall (𝕜 := 𝕜) (F := (x : ι) → Fm x) (fun (x : E) (x_1 : ι) ↦ f x_1 x)
    (FormalMultilinearSeries.pi (F := Fm) p) e r

Tactic:
simp_rw [← hasFPowerSeriesWithinOnBall_univ] at hf ⊢

Premises used: hasFPowerSeriesWithinOnBall_univ