awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Composition
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
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
b : Composition n
h : Membership.mem (γ := Finset (Composition n)) Finset.univ b
hb : b ≠ Composition.single n n_pos
this_1 : b.length ≠ 1
this : 0 < b.length
⊢ 1 < b.length

Tactic:
lia
-- Module: Mathlib.Analysis.Analytic.Composition
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
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
b : Composition n
h : Membership.mem (γ := Finset (Composition n)) Finset.univ b
hb : b ≠ Composition.single n n_pos
⊢ 1 < b.length

Tactic:
have A : 1 < b.length := by
        have : b.length ≠ 1 := by simpa [Composition.eq_single_iff_length] using hb
        have : 0 < b.length := Composition.length_pos_of_pos b n_pos
        lia
-- Module: Mathlib.Analysis.Analytic.Composition
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
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
b : Composition n
h_1 : Membership.mem (γ := Finset (Composition n)) Finset.univ b
hb : b ≠ Composition.single n n_pos
A : 1 < b.length
h :
  ∀ (v : (i : Fin n) → E),
    Eq.{u_3 + 1} (α := F)
      ((compAlongComposition (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p b : (a : (i : Fin n) → E) → F) v : F)
      ((0 : (a : (i : Fin n) → E) → F) v : F)
⊢ compAlongComposition (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p b = 0

Tactic:
ext v
-- Module: Mathlib.Analysis.Analytic.Composition
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
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
b : Composition n
h_1 : Membership.mem (γ := Finset (Composition n)) Finset.univ b
hb : b ≠ Composition.single n n_pos
A : 1 < b.length
v : (i : Fin n) → E
h :
  Eq (α := F)
    ((id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0) b.length : (a : (i : Fin b.length) → F) → F)
        (p.applyComposition b v) :
      F)
    ((0 : (a : (i : Fin n) → E) → F) v : F)
h₁ :
  Eq (α := F) ((0 : (a : (i : Fin b.length) → F) → F) (p.applyComposition b v) : F)
    ((0 : (a : (i : Fin n) → E) → F) v : F)
h₂ : Eq.{u_3 + 1} (α := F) (0 : F) ((0 : (a : (i : Fin n) → E) → F) v : F)
h₃ h₄ : Eq.{u_3 + 1} (α := F) 0 0
⊢ Eq.{u_3 + 1} (α := F)
    ((compAlongComposition (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p b : (a : (i : Fin n) → E) → F) v : F)
    ((0 : (a : (i : Fin n) → E) → F) v : F)

Tactic:
rw [compAlongComposition_apply, id_apply_of_one_lt _ _ _ A,
        ContinuousMultilinearMap.zero_apply, ContinuousMultilinearMap.zero_apply]

Premises used: FormalMultilinearSeries.compAlongComposition_apply, FormalMultilinearSeries.id_apply_of_one_lt, ContinuousMultilinearMap.zero_apply
-- Module: Mathlib.Analysis.Analytic.Composition
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
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
⊢ Composition.single n n_pos ∉ Finset.univ →
    compAlongComposition (id 𝕜 F ((p 0 : (a : (i : Fin 0) → E) → F) v0)) p (Composition.single n n_pos) = 0

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Composition
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
x : F
v0 : Fin 0 → E
h : x = (p 0 : (a : (i : Fin 0) → E) → F) v0
⊢ FormalMultilinearSeries.comp (id 𝕜 F x) p = p

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Analytic.Composition
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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
hq : 0 < q.radius
hp : 0 < p.radius
rcases :
  ∀ (rq : ℝ≥0) (rq_pos : 0 < (↑rq : ℝ≥0∞)) (hrq : (↑rq : ℝ≥0∞) < min 1 q.radius),
    ∃ r > 0,
      Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
        ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
          r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
⊢ ∃ r > 0,
    Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
      ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
        r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)

Tactic:
rcases ENNReal.lt_iff_exists_nnreal_btwn.1 (lt_min zero_lt_one hq) with ⟨rq, rq_pos, hrq⟩

Premises used: lt_min, ENNReal.lt_iff_exists_nnreal_btwn, zero_lt_one, Iff.mp
-- Module: Mathlib.Analysis.Analytic.Composition
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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
hq : 0 < q.radius
hp : 0 < p.radius
rq : ℝ≥0
rq_pos : 0 < (↑rq : ℝ≥0∞)
hrq : (↑rq : ℝ≥0∞) < min 1 q.radius
rcases :
  ∀ (rp : ℝ≥0) (rp_pos : 0 < (↑rp : ℝ≥0∞)) (hrp : (↑rp : ℝ≥0∞) < min 1 p.radius),
    ∃ r > 0,
      Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
        ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
          r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
⊢ ∃ r > 0,
    Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
      ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
        r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)

Tactic:
rcases ENNReal.lt_iff_exists_nnreal_btwn.1 (lt_min zero_lt_one hp) with ⟨rp, rp_pos, hrp⟩

Premises used: lt_min, ENNReal.lt_iff_exists_nnreal_btwn, zero_lt_one, Iff.mp
-- Module: Mathlib.Analysis.Analytic.Composition
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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
hq : 0 < q.radius
hp : 0 < p.radius
rq : ℝ≥0
rq_pos : 0 < (↑rq : ℝ≥0∞)
hrq : (↑rq : ℝ≥0∞) < min 1 q.radius
rp : ℝ≥0
rp_pos : 0 < (↑rp : ℝ≥0∞)
hrp : (↑rp : ℝ≥0∞) < min 1 p.radius
⊢ rp < 1 ∧ (↑rp : ℝ≥0∞) < p.radius

Tactic:
simp only [lt_min_iff, ENNReal.coe_lt_one_iff, ENNReal.coe_pos] at hrp hrq rp_pos rq_pos

Premises used: ENNReal.coe_pos, ENNReal.coe_lt_one_iff, lt_min_iff
-- Module: Mathlib.Analysis.Analytic.Composition
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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
hq : 0 < q.radius
hp : 0 < p.radius
rq : ℝ≥0
rq_pos : 0 < (↑rq : ℝ≥0∞)
hrq : (↑rq : ℝ≥0∞) < min 1 q.radius
rp : ℝ≥0
rp_pos : 0 < (↑rp : ℝ≥0∞)
hrp : (↑rp : ℝ≥0∞) < min 1 p.radius
hrp₁ : rp < 1 ∧ (↑rp : ℝ≥0∞) < p.radius
⊢ rq < 1 ∧ (↑rq : ℝ≥0∞) < q.radius

Tactic:
simp only [lt_min_iff, ENNReal.coe_lt_one_iff, ENNReal.coe_pos] at hrp hrq rp_pos rq_pos

Premises used: ENNReal.coe_pos, ENNReal.coe_lt_one_iff, lt_min_iff
-- Module: Mathlib.Analysis.Analytic.Composition
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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
hq : 0 < q.radius
hp : 0 < p.radius
rq : ℝ≥0
rq_pos : 0 < (↑rq : ℝ≥0∞)
hrq : (↑rq : ℝ≥0∞) < min 1 q.radius
rp : ℝ≥0
rp_pos : 0 < (↑rp : ℝ≥0∞)
hrp : (↑rp : ℝ≥0∞) < min 1 p.radius
hrp₁ : rp < 1 ∧ (↑rp : ℝ≥0∞) < p.radius
hrq₁ : rq < 1 ∧ (↑rq : ℝ≥0∞) < q.radius
⊢ 0 < rp

Tactic:
simp only [lt_min_iff, ENNReal.coe_lt_one_iff, ENNReal.coe_pos] at hrp hrq rp_pos rq_pos

Premises used: ENNReal.coe_pos, ENNReal.coe_lt_one_iff, lt_min_iff
-- Module: Mathlib.Analysis.Analytic.Composition
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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
hq : 0 < q.radius
hp : 0 < p.radius
rq : ℝ≥0
rq_pos : 0 < (↑rq : ℝ≥0∞)
hrq : (↑rq : ℝ≥0∞) < min 1 q.radius
rp : ℝ≥0
rp_pos : 0 < (↑rp : ℝ≥0∞)
hrp : (↑rp : ℝ≥0∞) < min 1 p.radius
hrp₁ : rp < 1 ∧ (↑rp : ℝ≥0∞) < p.radius
hrq₁ : rq < 1 ∧ (↑rq : ℝ≥0∞) < q.radius
rp_pos₁ : 0 < rp
⊢ 0 < rq

Tactic:
simp only [lt_min_iff, ENNReal.coe_lt_one_iff, ENNReal.coe_pos] at hrp hrq rp_pos rq_pos

Premises used: ENNReal.coe_pos, ENNReal.coe_lt_one_iff, lt_min_iff
-- Module: Mathlib.Analysis.Analytic.Composition
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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
hq : 0 < q.radius
hp : 0 < p.radius
rq rp : ℝ≥0
hrp : rp < 1 ∧ (↑rp : ℝ≥0∞) < p.radius
hrq : rq < 1 ∧ (↑rq : ℝ≥0∞) < q.radius
rp_pos : 0 < rp
rq_pos : 0 < rq
⊢ ∃ Cq > 0, ∀ (n : ℕ), ‖q n‖₊ * rq ^ n ≤ Cq

Tactic:
q.nnnorm_mul_pow_le_of_lt_radius hrq.2

Premises used: FormalMultilinearSeries.nnnorm_mul_pow_le_of_lt_radius, And.right
-- Module: Mathlib.Analysis.Analytic.Composition
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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
hq : 0 < q.radius
hp : 0 < p.radius
rq rp : ℝ≥0
hrp : rp < 1 ∧ (↑rp : ℝ≥0∞) < p.radius
hrq : rq < 1 ∧ (↑rq : ℝ≥0∞) < q.radius
rp_pos : 0 < rp
rq_pos : 0 < rq
obtain :
  ∀ (Cq : ℝ≥0) (_hCq0 : Cq > 0) (hCq : ∀ (n : ℕ), ‖q n‖₊ * rq ^ n ≤ Cq),
    ∃ r > 0,
      Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
        ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
          r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
⊢ ∃ r > 0,
    Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
      ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
        r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)

Tactic:
obtain ⟨Cq, _hCq0, hCq⟩ : ∃ Cq > 0, ∀ n, ‖q n‖₊ * rq ^ n ≤ Cq :=
    q.nnnorm_mul_pow_le_of_lt_radius hrq.2

Premises used: FormalMultilinearSeries.nnnorm_mul_pow_le_of_lt_radius, And.right
-- Module: Mathlib.Analysis.Analytic.Composition
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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
hq : 0 < q.radius
hp : 0 < p.radius
rq rp : ℝ≥0
hrp : rp < 1 ∧ (↑rp : ℝ≥0∞) < p.radius
hrq : rq < 1 ∧ (↑rq : ℝ≥0∞) < q.radius
rp_pos : 0 < rp
rq_pos : 0 < rq
Cq : ℝ≥0
_hCq0 : Cq > 0
hCq : ∀ (n : ℕ), ‖q n‖₊ * rq ^ n ≤ Cq
rcases : ∀ (Cp : ℝ≥0) (hCp : ∀ (n : ℕ), ‖p n‖₊ * rp ^ n ≤ Cp), ∃ Cp ≥ 1, ∀ (n : ℕ), ‖p n‖₊ * rp ^ n ≤ Cp
⊢ ∃ Cp ≥ 1, ∀ (n : ℕ), ‖p n‖₊ * rp ^ n ≤ Cp

Tactic:
rcases p.nnnorm_mul_pow_le_of_lt_radius hrp.2 with ⟨Cp, -, hCp⟩

Premises used: FormalMultilinearSeries.nnnorm_mul_pow_le_of_lt_radius, And.right
-- Module: Mathlib.Analysis.Analytic.Composition
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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
hq : 0 < q.radius
hp : 0 < p.radius
rq rp : ℝ≥0
hrp : rp < 1 ∧ (↑rp : ℝ≥0∞) < p.radius
hrq : rq < 1 ∧ (↑rq : ℝ≥0∞) < q.radius
rp_pos : 0 < rp
rq_pos : 0 < rq
Cq : ℝ≥0
_hCq0 : Cq > 0
hCq : ∀ (n : ℕ), ‖q n‖₊ * rq ^ n ≤ Cq
Cp : ℝ≥0
hCp : ∀ (n : ℕ), ‖p n‖₊ * rp ^ n ≤ Cp
⊢ ∃ Cp ≥ 1, ∀ (n : ℕ), ‖p n‖₊ * rp ^ n ≤ Cp

Tactic:
⟨max Cp 1, le_max_right _ _, fun n => (hCp n).trans (le_max_left _ _)⟩

Premises used: le_max_right, Max.max, And.intro, Exists.intro, LE.le.trans, OfNat.ofNat, le_max_left
-- Module: Mathlib.Analysis.Analytic.Composition
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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
hq : 0 < q.radius
hp : 0 < p.radius
rq rp : ℝ≥0
hrp : rp < 1 ∧ (↑rp : ℝ≥0∞) < p.radius
hrq : rq < 1 ∧ (↑rq : ℝ≥0∞) < q.radius
rp_pos : 0 < rp
rq_pos : 0 < rq
Cq : ℝ≥0
_hCq0 : Cq > 0
hCq : ∀ (n : ℕ), ‖q n‖₊ * rq ^ n ≤ Cq
Cp : ℝ≥0
hCp : ∀ (n : ℕ), ‖p n‖₊ * rp ^ n ≤ Cp
⊢ ∃ Cp ≥ 1, ∀ (n : ℕ), ‖p n‖₊ * rp ^ n ≤ Cp

Tactic:
exact ⟨max Cp 1, le_max_right _ _, fun n => (hCp n).trans (le_max_left _ _)⟩
-- Module: Mathlib.Analysis.Analytic.Composition
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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
hq : 0 < q.radius
hp : 0 < p.radius
rq rp : ℝ≥0
hrp : rp < 1 ∧ (↑rp : ℝ≥0∞) < p.radius
hrq : rq < 1 ∧ (↑rq : ℝ≥0∞) < q.radius
rp_pos : 0 < rp
rq_pos : 0 < rq
Cq : ℝ≥0
_hCq0 : Cq > 0
hCq : ∀ (n : ℕ), ‖q n‖₊ * rq ^ n ≤ Cq
obtain :
  ∀ (Cp : ℝ≥0) (hCp1 : Cp ≥ 1) (hCp : ∀ (n : ℕ), ‖p n‖₊ * rp ^ n ≤ Cp),
    ∃ r > 0,
      Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
        ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
          r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
⊢ ∃ r > 0,
    Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
      ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
        r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)

Tactic:
obtain ⟨Cp, hCp1, hCp⟩ : ∃ Cp ≥ 1, ∀ n, ‖p n‖₊ * rp ^ n ≤ Cp := by
    rcases p.nnnorm_mul_pow_le_of_lt_radius hrp.2 with ⟨Cp, -, hCp⟩
    exact ⟨max Cp 1, le_max_right _ _, fun n => (hCp n).trans (le_max_left _ _)⟩
-- Module: Mathlib.Analysis.Analytic.Composition
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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
hq : 0 < q.radius
hp : 0 < p.radius
rq rp : ℝ≥0
hrp : rp < 1 ∧ (↑rp : ℝ≥0∞) < p.radius
hrq : rq < 1 ∧ (↑rq : ℝ≥0∞) < q.radius
rp_pos : 0 < rp
rq_pos : 0 < rq
Cq : ℝ≥0
_hCq0 : Cq > 0
hCq : ∀ (n : ℕ), ‖q n‖₊ * rq ^ n ≤ Cq
Cp : ℝ≥0
hCp1 : Cp ≥ 1
hCp : ∀ (n : ℕ), ‖p n‖₊ * rp ^ n ≤ Cp
r0 : ℝ≥0 := (4 * Cp)⁻¹
⊢ 0 < r0

Tactic:
have r0_pos : 0 < r0 := inv_pos.2 (mul_pos zero_lt_four (zero_lt_one.trans_le hCp1))
-- Module: Mathlib.Analysis.Analytic.Composition
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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
hq : 0 < q.radius
hp : 0 < p.radius
rq rp : ℝ≥0
hrp : rp < 1 ∧ (↑rp : ℝ≥0∞) < p.radius
hrq : rq < 1 ∧ (↑rq : ℝ≥0∞) < q.radius
rp_pos : 0 < rp
rq_pos : 0 < rq
Cq : ℝ≥0
_hCq0 : Cq > 0
hCq : ∀ (n : ℕ), ‖q n‖₊ * rq ^ n ≤ Cq
Cp : ℝ≥0
hCp1 : Cp ≥ 1
hCp : ∀ (n : ℕ), ‖p n‖₊ * rp ^ n ≤ Cp
r0 : ℝ≥0 := (4 * Cp)⁻¹
r0_pos : 0 < r0
r : ℝ≥0 := rp * rq * r0
⊢ 0 < r

Tactic:
have r_pos : 0 < r := mul_pos (mul_pos rp_pos rq_pos) r0_pos
-- Module: Mathlib.Analysis.Analytic.Composition
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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
hq : 0 < q.radius
hp : 0 < p.radius
rq rp : ℝ≥0
hrp : rp < 1 ∧ (↑rp : ℝ≥0∞) < p.radius
hrq : rq < 1 ∧ (↑rq : ℝ≥0∞) < q.radius
rp_pos : 0 < rp
rq_pos : 0 < rq
Cq : ℝ≥0
_hCq0 : Cq > 0
hCq : ∀ (n : ℕ), ‖q n‖₊ * rq ^ n ≤ Cq
Cp : ℝ≥0
hCp1 : Cp ≥ 1
hCp : ∀ (n : ℕ), ‖p n‖₊ * rp ^ n ≤ Cp
r0 : ℝ≥0 := (4 * Cp)⁻¹
r0_pos : 0 < r0
r : ℝ≥0 := rp * rq * r0
r_pos : 0 < r
n : ℕ
c : Composition n
⊢ nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G) (q c.length) * rq ^ n ≤ Cq

Tactic:
have A := calc
      ‖q c.length‖₊ * rq ^ n ≤ ‖q c.length‖₊ * rq ^ c.length :=
        mul_le_mul' le_rfl (pow_le_pow_of_le_one rq.2 hrq.1.le c.length_le)
      _ ≤ Cq := hCq _
-- Module: Mathlib.Analysis.Analytic.Composition
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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
hq : 0 < q.radius
hp : 0 < p.radius
rq rp : ℝ≥0
hrp : rp < 1 ∧ (↑rp : ℝ≥0∞) < p.radius
hrq : rq < 1 ∧ (↑rq : ℝ≥0∞) < q.radius
rp_pos : 0 < rp
rq_pos : 0 < rq
Cq : ℝ≥0
_hCq0 : Cq > 0
hCq : ∀ (n : ℕ), ‖q n‖₊ * rq ^ n ≤ Cq
Cp : ℝ≥0
hCp1 : Cp ≥ 1
hCp : ∀ (n : ℕ), ‖p n‖₊ * rp ^ n ≤ Cp
r0 : ℝ≥0 := (4 * Cp)⁻¹
r0_pos : 0 < r0
r : ℝ≥0 := rp * rq * r0
r_pos : 0 < r
n : ℕ
c : Composition n
A :
  nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G) (q c.length) * rq ^ n ≤ Cq
⊢ (∏ i : Fin c.length,
        nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun i)) ↦ E) F)
          (p (c.blocksFun i))) *
      rp ^ n =
    ∏ i : Fin c.length,
      nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun i)) ↦ E) F)
          (p (c.blocksFun i)) *
        rp ^ c.blocksFun i

Tactic:
simp only [Finset.prod_mul_distrib, Finset.prod_pow_eq_pow_sum, c.sum_blocksFun]

Premises used: Finset.prod_mul_distrib, Composition.sum_blocksFun, Finset.prod_pow_eq_pow_sum
-- Module: Mathlib.Analysis.Analytic.Composition
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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
hq : 0 < q.radius
hp : 0 < p.radius
rq rp : ℝ≥0
hrp : rp < 1 ∧ (↑rp : ℝ≥0∞) < p.radius
hrq : rq < 1 ∧ (↑rq : ℝ≥0∞) < q.radius
rp_pos : 0 < rp
rq_pos : 0 < rq
Cq : ℝ≥0
_hCq0 : Cq > 0
hCq : ∀ (n : ℕ), ‖q n‖₊ * rq ^ n ≤ Cq
Cp : ℝ≥0
hCp1 : Cp ≥ 1
hCp : ∀ (n : ℕ), ‖p n‖₊ * rp ^ n ≤ Cp
r0 : ℝ≥0 := (4 * Cp)⁻¹
r0_pos : 0 < r0
r : ℝ≥0 := rp * rq * r0
r_pos : 0 < r
n : ℕ
c : Composition n
A :
  nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G) (q c.length) * rq ^ n ≤ Cq
⊢ ∏ _i : Fin c.length, Cp = Cp ^ c.length

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Composition
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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
hq : 0 < q.radius
hp : 0 < p.radius
rq rp : ℝ≥0
hrp : rp < 1 ∧ (↑rp : ℝ≥0∞) < p.radius
hrq : rq < 1 ∧ (↑rq : ℝ≥0∞) < q.radius
rp_pos : 0 < rp
rq_pos : 0 < rq
Cq : ℝ≥0
_hCq0 : Cq > 0
hCq : ∀ (n : ℕ), ‖q n‖₊ * rq ^ n ≤ Cq
Cp : ℝ≥0
hCp1 : Cp ≥ 1
hCp : ∀ (n : ℕ), ‖p n‖₊ * rp ^ n ≤ Cp
r0 : ℝ≥0 := (4 * Cp)⁻¹
r0_pos : 0 < r0
r : ℝ≥0 := rp * rq * r0
r_pos : 0 < r
n : ℕ
c : Composition n
A :
  nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G) (q c.length) * rq ^ n ≤ Cq
⊢ (∏ i : Fin c.length,
        nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun i)) ↦ E) F)
          (p (c.blocksFun i))) *
      rp ^ n ≤
    Cp ^ n

Tactic:
have B := calc
      (∏ i, ‖p (c.blocksFun i)‖₊) * rp ^ n = ∏ i, ‖p (c.blocksFun i)‖₊ * rp ^ c.blocksFun i := by
        simp only [Finset.prod_mul_distrib, Finset.prod_pow_eq_pow_sum, c.sum_blocksFun]
      _ ≤ ∏ _i : Fin c.length, Cp := Finset.prod_le_prod' fun i _ => hCp _
      _ = Cp ^ c.length := by simp
      _ ≤ Cp ^ n := pow_right_mono₀ hCp1 c.length_le
-- Module: Mathlib.Analysis.Analytic.Composition
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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
hq : 0 < q.radius
hp : 0 < p.radius
rq rp : ℝ≥0
hrp : rp < 1 ∧ (↑rp : ℝ≥0∞) < p.radius
hrq : rq < 1 ∧ (↑rq : ℝ≥0∞) < q.radius
rp_pos : 0 < rp
rq_pos : 0 < rq
Cq : ℝ≥0
_hCq0 : Cq > 0
hCq : ∀ (n : ℕ), ‖q n‖₊ * rq ^ n ≤ Cq
Cp : ℝ≥0
hCp1 : Cp ≥ 1
hCp : ∀ (n : ℕ), ‖p n‖₊ * rp ^ n ≤ Cp
r0 : ℝ≥0 := (4 * Cp)⁻¹
r0_pos : 0 < r0
r : ℝ≥0 := rp * rq * r0
r_pos : 0 < r
n : ℕ
c : Composition n
A :
  nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G) (q c.length) * rq ^ n ≤ Cq
B :
  (∏ i : Fin c.length,
        nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun i)) ↦ E) F)
          (p (c.blocksFun i))) *
      rp ^ n ≤
    Cp ^ n
grw grw₁ :
  (nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G) (q c.length) *
        ∏ i : Fin c.length,
          nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun i)) ↦ E) F)
            (p (c.blocksFun i))) *
      r ^ n ≤
    (nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G) (q c.length) *
        ∏ i : Fin c.length,
          nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun i)) ↦ E) F)
            (p (c.blocksFun i))) *
      r ^ n
⊢ ‖q.compAlongComposition p c‖₊ * r ^ n ≤
    (nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G) (q c.length) *
        ∏ i : Fin c.length,
          nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun i)) ↦ E) F)
            (p (c.blocksFun i))) *
      r ^ n

Tactic:
grw [q.compAlongComposition_nnnorm p c]

Premises used: FormalMultilinearSeries.compAlongComposition_nnnorm