awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ (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) * rq ^ 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 ^ n) *
      r0 ^ n

Tactic:
ring
-- 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
⊢ nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G) (q c.length) * rq ^ 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 ^ n) *
      r0 ^ n ≤
    Cq * Cp ^ n * r0 ^ n

Tactic:
mul_le_mul' (mul_le_mul' A B) le_rfl

Premises used: le_rfl, mul_le_mul'
-- 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
simp : Cq * Cp ^ n * (4 * Cp)⁻¹ ^ n = Cq / HPow.hPow (α := ℝ≥0) 4 n
⊢ Cq * Cp ^ n * r0 ^ n = Cq / HPow.hPow (α := ℝ≥0) 4 n

Tactic:
simp only [r0]
-- 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
⊢ Cq * Cp ^ n * (4 * Cp)⁻¹ ^ n = Cq / HPow.hPow (α := ℝ≥0) 4 n

Tactic:
simp [field, mul_pow]

Premises used: mul_pow
-- 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
⊢ ∀ (i : (n : ℕ) × Composition n),
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
        r ^ i.fst (β := fun (n : ℕ) ↦ Composition n) ≤
      Cq / HPow.hPow (α := ℝ≥0) 4 (i.fst (β := fun (n : ℕ) ↦ Composition n))

Tactic:
have I :
    ∀ i : Σ n : ℕ, Composition n, ‖q.compAlongComposition p i.2‖₊ * r ^ i.1 ≤ Cq / 4 ^ i.1 := by
    rintro ⟨n, c⟩
    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 _
    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
    calc
      ‖q.compAlongComposition p c‖₊ * r ^ n ≤
          (‖q c.length‖₊ * ∏ i, ‖p (c.blocksFun i)‖₊) * r ^ n := by
        grw [q.compAlongComposition_nnnorm p c]
      _ = ‖q c.length‖₊ * rq ^ n * ((∏ i, ‖p (c.blocksFun i)‖₊) * rp ^ n) * r0 ^ n := by
        ring
      _ ≤ Cq * Cp ^ n * r0 ^ n := mul_le_mul' (mul_le_mul' A B) le_rfl
      _ = Cq / 4 ^ n := by
        simp only [r0]
        simp [field, mul_pow]
-- 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
I :
  ∀ (i : (n : ℕ) × Composition n),
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
        r ^ i.fst (β := fun (n : ℕ) ↦ Composition n) ≤
      Cq / HPow.hPow (α := ℝ≥0) 4 (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:
⟨r, r_pos, NNReal.summable_of_le I ?_⟩

Premises used: And.intro, Exists.intro, NNReal.summable_of_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
I :
  ∀ (i : (n : ℕ) × Composition n),
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
        r ^ i.fst (β := fun (n : ℕ) ↦ Composition n) ≤
      Cq / HPow.hPow (α := ℝ≥0) 4 (i.fst (β := fun (n : ℕ) ↦ Composition n))
refine :
  Summable (α := ℝ≥0) fun (b : (n : ℕ) × Composition n) ↦
    Cq / HPow.hPow (α := ℝ≥0) 4 (b.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:
refine ⟨r, r_pos, NNReal.summable_of_le I ?_⟩
-- 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
I :
  ∀ (i : (n : ℕ) × Composition n),
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
        r ^ i.fst (β := fun (n : ℕ) ↦ Composition n) ≤
      Cq / HPow.hPow (α := ℝ≥0) 4 (i.fst (β := fun (n : ℕ) ↦ Composition n))
⊢ Summable (α := ℝ≥0) fun (b : (n : ℕ) × Composition n) ↦
    Cq * (HPow.hPow (α := ℝ≥0) 4 (b.fst (β := fun (n : ℕ) ↦ Composition n)))⁻¹

Tactic:
Summable.mul_left _ ?_

Premises used: Summable.mul_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)⁻¹
r0_pos : 0 < r0
r : ℝ≥0 := rp * rq * r0
r_pos : 0 < r
I :
  ∀ (i : (n : ℕ) × Composition n),
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
        r ^ i.fst (β := fun (n : ℕ) ↦ Composition n) ≤
      Cq / HPow.hPow (α := ℝ≥0) 4 (i.fst (β := fun (n : ℕ) ↦ Composition n))
refine :
  Summable (α := ℝ≥0) fun (b : (n : ℕ) × Composition n) ↦
    (HPow.hPow (α := ℝ≥0) 4 (b.fst (β := fun (n : ℕ) ↦ Composition n)))⁻¹
⊢ Summable (α := ℝ≥0) fun (b : (n : ℕ) × Composition n) ↦
    Cq * (HPow.hPow (α := ℝ≥0) 4 (b.fst (β := fun (n : ℕ) ↦ Composition n)))⁻¹

Tactic:
refine Summable.mul_left _ ?_

Premises used: Summable.mul_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)⁻¹
r0_pos : 0 < r0
r : ℝ≥0 := rp * rq * r0
r_pos : 0 < r
I :
  ∀ (i : (n : ℕ) × Composition n),
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
        r ^ i.fst (β := fun (n : ℕ) ↦ Composition n) ≤
      Cq / HPow.hPow (α := ℝ≥0) 4 (i.fst (β := fun (n : ℕ) ↦ Composition n))
n : ℕ
⊢ HasSum (α := ℝ≥0) (fun (c : Composition n) ↦ (HPow.hPow (α := ℝ≥0) 4 n)⁻¹)
    (∑ b : Composition n, (HPow.hPow (α := ℝ≥0) 4 n)⁻¹)

Tactic:
hasSum_fintype fun c : Composition n => (4 ^ n : ℝ≥0)⁻¹

Premises used: hasSum_fintype, Inv.inv, HPow.hPow, OfNat.ofNat, SummationFilter.unconditional
-- 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
I :
  ∀ (i : (n : ℕ) × Composition n),
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
        r ^ i.fst (β := fun (n : ℕ) ↦ Composition n) ≤
      Cq / HPow.hPow (α := ℝ≥0) 4 (i.fst (β := fun (n : ℕ) ↦ Composition n))
n : ℕ
h : HPow.hPow (α := ℝ≥0) 2 (n - 1) / HPow.hPow (α := ℝ≥0) 4 n = ∑ b : Composition n, (HPow.hPow (α := ℝ≥0) 4 n)⁻¹
⊢ HasSum (fun (c : Composition n) ↦ (HPow.hPow (α := ℝ≥0) 4 n)⁻¹)
    (HPow.hPow (α := ℝ≥0) 2 (n - 1) / HPow.hPow (α := ℝ≥0) 4 n)

Tactic:
convert! hasSum_fintype fun c : Composition n => (4 ^ n : ℝ≥0)⁻¹

Premises used: hasSum_fintype, Inv.inv, HPow.hPow, OfNat.ofNat, SummationFilter.unconditional
-- 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
I :
  ∀ (i : (n : ℕ) × Composition n),
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
        r ^ i.fst (β := fun (n : ℕ) ↦ Composition n) ≤
      Cq / HPow.hPow (α := ℝ≥0) 4 (i.fst (β := fun (n : ℕ) ↦ Composition n))
n : ℕ
⊢ HPow.hPow (α := ℝ≥0) 2 (n - 1) / HPow.hPow (α := ℝ≥0) 4 n = ∑ b : Composition n, (HPow.hPow (α := ℝ≥0) 4 n)⁻¹

Tactic:
simp [Finset.card_univ, composition_card, div_eq_mul_inv]

Premises used: Finset.card_univ, composition_card, div_eq_mul_inv
-- 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
I :
  ∀ (i : (n : ℕ) × Composition n),
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
        r ^ i.fst (β := fun (n : ℕ) ↦ Composition n) ≤
      Cq / HPow.hPow (α := ℝ≥0) 4 (i.fst (β := fun (n : ℕ) ↦ Composition n))
⊢ ∀ (n : ℕ),
    HasSum (fun (c : Composition n) ↦ (HPow.hPow (α := ℝ≥0) 4 n)⁻¹)
      (HPow.hPow (α := ℝ≥0) 2 (n - 1) / HPow.hPow (α := ℝ≥0) 4 n)

Tactic:
have : ∀ n : ℕ, HasSum (fun c : Composition n => (4 ^ n : ℝ≥0)⁻¹) (2 ^ (n - 1) / 4 ^ n) := by
    intro n
    convert! hasSum_fintype fun c : Composition n => (4 ^ n : ℝ≥0)⁻¹
    simp [Finset.card_univ, composition_card, div_eq_mul_inv]
-- 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
I :
  ∀ (i : (n : ℕ) × Composition n),
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
        r ^ i.fst (β := fun (n : ℕ) ↦ Composition n) ≤
      Cq / HPow.hPow (α := ℝ≥0) 4 (i.fst (β := fun (n : ℕ) ↦ Composition n))
this :
  ∀ (n : ℕ),
    HasSum (fun (c : Composition n) ↦ (HPow.hPow (α := ℝ≥0) 4 n)⁻¹)
      (HPow.hPow (α := ℝ≥0) 2 (n - 1) / HPow.hPow (α := ℝ≥0) 4 n)
⊢ Summable (α := ℝ≥0) fun (b : (n : ℕ) × Composition n) ↦
    (HPow.hPow (α := ℝ≥0) 4 (b.fst (β := fun (n : ℕ) ↦ Composition n)))⁻¹

Tactic:
NNReal.summable_sigma.2 ⟨fun n => (this n).summable, (NNReal.summable_nat_add_iff 1).1 ?_⟩

Premises used: Iff.mpr, NNReal.summable_sigma, NNReal.summable_nat_add_iff, HasSum.summable, And.intro, Iff.mp, OfNat.ofNat
-- 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
I :
  ∀ (i : (n : ℕ) × Composition n),
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
        r ^ i.fst (β := fun (n : ℕ) ↦ Composition n) ≤
      Cq / HPow.hPow (α := ℝ≥0) 4 (i.fst (β := fun (n : ℕ) ↦ Composition n))
this :
  ∀ (n : ℕ),
    HasSum (fun (c : Composition n) ↦ (HPow.hPow (α := ℝ≥0) 4 n)⁻¹)
      (HPow.hPow (α := ℝ≥0) 2 (n - 1) / HPow.hPow (α := ℝ≥0) 4 n)
refine :
  Summable (α := ℝ≥0) fun (i : ℕ) ↦
    ∑' (y : Composition (i + 1)),
      (HPow.hPow (α := ℝ≥0) 4
          ((Sigma.mk (β := fun (x : ℕ) ↦ Composition x) (i + 1) y).fst (β := fun (n : ℕ) ↦ Composition n)))⁻¹
⊢ Summable (α := ℝ≥0) fun (b : (n : ℕ) × Composition n) ↦
    (HPow.hPow (α := ℝ≥0) 4 (b.fst (β := fun (n : ℕ) ↦ Composition n)))⁻¹

Tactic:
refine NNReal.summable_sigma.2 ⟨fun n => (this n).summable, (NNReal.summable_nat_add_iff 1).1 ?_⟩

Premises used: Iff.mpr, NNReal.summable_sigma, NNReal.summable_nat_add_iff, And.intro, Iff.mp, OfNat.ofNat
-- 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
I :
  ∀ (i : (n : ℕ) × Composition n),
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
        r ^ i.fst (β := fun (n : ℕ) ↦ Composition n) ≤
      Cq / HPow.hPow (α := ℝ≥0) 4 (i.fst (β := fun (n : ℕ) ↦ Composition n))
this :
  ∀ (n : ℕ),
    HasSum (fun (c : Composition n) ↦ (HPow.hPow (α := ℝ≥0) 4 n)⁻¹)
      (HPow.hPow (α := ℝ≥0) 2 (n - 1) / HPow.hPow (α := ℝ≥0) 4 n)
⊢ Summable (α := ℝ≥0) fun (i : ℕ) ↦ 1 / 4 * (1 / 2) ^ i

Tactic:
(NNReal.summable_geometric (NNReal.div_lt_one_of_lt one_lt_two)).mul_left (1 / 4)

Premises used: NNReal.div_lt_one_of_lt, NNReal.summable_geometric, HDiv.hDiv, Summable.mul_left, one_lt_two, OfNat.ofNat
-- 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
I :
  ∀ (i : (n : ℕ) × Composition n),
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
        r ^ i.fst (β := fun (n : ℕ) ↦ Composition n) ≤
      Cq / HPow.hPow (α := ℝ≥0) 4 (i.fst (β := fun (n : ℕ) ↦ Composition n))
this :
  ∀ (n : ℕ),
    HasSum (fun (c : Composition n) ↦ (HPow.hPow (α := ℝ≥0) 4 n)⁻¹)
      (HPow.hPow (α := ℝ≥0) 2 (n - 1) / HPow.hPow (α := ℝ≥0) 4 n)
h :
  ∀ (n : ℕ),
    ∑' (y : Composition (n + 1)),
        (HPow.hPow (α := ℝ≥0) 4
            ((Sigma.mk (β := fun (x : ℕ) ↦ Composition x) (n + 1) y).fst (β := fun (n : ℕ) ↦ Composition n)))⁻¹ =
      1 / 4 * (1 / 2) ^ n
⊢ Eq (α := ℕ → ℝ≥0)
    (fun (i : ℕ) ↦
      ∑' (y : Composition (i + 1)),
        (HPow.hPow (α := ℝ≥0) 4
            ((Sigma.mk (β := fun (x : ℕ) ↦ Composition x) (i + 1) y).fst (β := fun (n : ℕ) ↦ Composition n)))⁻¹)
    fun (i : ℕ) ↦ 1 / 4 * (1 / 2) ^ i

Tactic:
ext1 n