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
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)
n : ℕ
h : HPow.hPow (α := ℝ≥0) 2 n / HPow.hPow (α := ℝ≥0) 4 (n + 1) = 1 / 4 * (1 / 2) ^ 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

Tactic:
rw [(this _).tsum_eq, add_tsub_cancel_right]

Premises used: HasSum.tsum_eq, add_tsub_cancel_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
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)
n : ℕ
⊢ 4 = HMul.hMul (α := ℝ≥0) 2 2

Tactic:
norm_num
-- 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)
n : ℕ
⊢ HPow.hPow (α := ℝ≥0) 2 n / HPow.hPow (α := ℝ≥0) 4 (n + 1) = 1 / 4 * (1 / 2) ^ n

Tactic:
simp [field, pow_succ, mul_pow, show (4 : ℝ≥0) = 2 * 2 by norm_num]

Premises used: pow_succ, 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
r : ℝ≥0
hr :
  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∞) ≤ radius (q.comp p)

Tactic:
le_radius_of_bound_nnreal _
      (∑' i : Σ n, Composition n, ‖compAlongComposition q p i.snd‖₊ * r ^ i.fst) fun n => ?_

Premises used: HMul.hMul, NNNorm.nnnorm, FormalMultilinearSeries.compAlongComposition, Sigma.fst, HPow.hPow, tsum, Sigma.snd, SummationFilter.unconditional, FormalMultilinearSeries.le_radius_of_bound_nnreal
-- 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
r : ℝ≥0
hr :
  Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
le_radius_of_bound_nnreal :
  ∀ (n : ℕ),
    ‖q.comp p n‖₊ * r ^ n ≤
      ∑' (i : (n : ℕ) × Composition n),
        ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
          r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
⊢ (↑r : ℝ≥0∞) ≤ radius (q.comp p)

Tactic:
refine
    le_radius_of_bound_nnreal _
      (∑' i : Σ n, Composition n, ‖compAlongComposition q p i.snd‖₊ * r ^ i.fst) fun n => ?_

Premises used: HMul.hMul, NNNorm.nnnorm, FormalMultilinearSeries.compAlongComposition, Sigma.fst, HPow.hPow, tsum, Sigma.snd, SummationFilter.unconditional, FormalMultilinearSeries.le_radius_of_bound_nnreal
-- 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
r : ℝ≥0
hr :
  Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
n : ℕ
rw : ‖q.comp p n‖₊ * r ^ n ≤ (∑ i : Composition n, ‖q.compAlongComposition p i‖₊) * r ^ n
⊢ ‖q.comp p n‖₊ * r ^ n ≤ ∑' (c : Composition n), ‖q.compAlongComposition p c‖₊ * r ^ n

Tactic:
rw [tsum_fintype, ← Finset.sum_mul]

Premises used: tsum_fintype, Finset.sum_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
r : ℝ≥0
hr :
  Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
n : ℕ
⊢ ‖q.comp p n‖₊ * r ^ n ≤ (∑ i : Composition n, ‖q.compAlongComposition p i‖₊) * r ^ n

Tactic:
mul_le_mul' (nnnorm_sum_le _ _) le_rfl

Premises used: le_rfl, nnnorm_sum_le, 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
r : ℝ≥0
hr :
  Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
n : ℕ
⊢ ‖q.comp p n‖₊ * r ^ n ≤ (∑ i : Composition n, ‖q.compAlongComposition p i‖₊) * r ^ n

Tactic:
exact mul_le_mul' (nnnorm_sum_le _ _) le_rfl

Premises used: le_rfl, nnnorm_sum_le, 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
r : ℝ≥0
hr :
  Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
n : ℕ
⊢ LE.le (α := ℝ≥0) (∑' (c : Composition n), ‖q.compAlongComposition p c‖₊ * r ^ n)
    (∑' (i : (n : ℕ) × Composition n),
      ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
        r ^ i.fst (β := fun (n : ℕ) ↦ Composition n))

Tactic:
NNReal.tsum_comp_le_tsum_of_inj hr sigma_mk_injective

Premises used: NNReal.tsum_comp_le_tsum_of_inj, sigma_mk_injective
-- 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
r : ℝ≥0
hr :
  Summable (α := ℝ≥0) fun (i : (n : ℕ) × Composition n) ↦
    ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
      r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
n : ℕ
q₁ : ‖q.comp p n‖₊ * r ^ n ≤ ∑' (c : Composition n), ‖q.compAlongComposition p c‖₊ * r ^ n
⊢ ‖q.comp p n‖₊ * r ^ n ≤
    ∑' (i : (n : ℕ) × Composition n),
      ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
        r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)

Tactic:
calc
    ‖FormalMultilinearSeries.comp q p n‖₊ * r ^ n ≤
        ∑' c : Composition n, ‖compAlongComposition q p c‖₊ * r ^ n := by
      rw [tsum_fintype, ← Finset.sum_mul]
      exact mul_le_mul' (nnnorm_sum_le _ _) le_rfl
    _ ≤ ∑' i : Σ n : ℕ, Composition n, ‖compAlongComposition q p i.snd‖₊ * r ^ i.fst :=
      NNReal.tsum_comp_le_tsum_of_inj hr sigma_mk_injective

Premises used: NNReal.tsum_comp_le_tsum_of_inj, Composition, FormalMultilinearSeries.comp, sigma_mk_injective
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
m M N : ℕ
i : (n : ℕ) × (Fin n → ℕ)
⊢ i ∈ compPartialSumSource m M N ↔
    (m ≤ i.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) ∧ i.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) < M) ∧
      ∀ (a : Fin (i.fst (β := fun (n : ℕ) ↦ Fin n → ℕ))),
        1 ≤ i.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) a ∧ i.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) a < N

Tactic:
simp only [compPartialSumSource, Finset.mem_Ico, Fintype.mem_piFinset, Finset.mem_sigma]

Premises used: Fintype.mem_piFinset, FormalMultilinearSeries.compPartialSumSource, Finset.mem_sigma, Finset.mem_Ico
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
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 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
m M N : ℕ
i : (n : ℕ) × (Fin n → ℕ)
hi : i ∈ compPartialSumSource m M N
rcases :
  (n : ℕ) →
    (f : Fin n → ℕ) →
      (hi : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f ∈ compPartialSumSource m M N) → (n : ℕ) × Composition n
⊢ (n : ℕ) × Composition n

Tactic:
rcases i with ⟨n, f⟩
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
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 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
m M N n : ℕ
f : Fin n → ℕ
hi : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f ∈ compPartialSumSource m M N
⊢ (m ≤ Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f) ∧
      Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f) < M) ∧
    ∀ (a : Fin (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f))),
      LE.le (α := ℕ) (1 : ℕ)
          (Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f) a : ℕ) ∧
        Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f) a < N

Tactic:
rw [mem_compPartialSumSource_iff] at hi

Premises used: FormalMultilinearSeries.mem_compPartialSumSource_iff
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
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 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
m M N n : ℕ
f : Fin n → ℕ
hi :
  (m ≤ Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f) ∧
      Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f) < M) ∧
    ∀ (a : Fin (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f))),
      LE.le (α := ℕ) (1 : ℕ)
          (Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f) a : ℕ) ∧
        Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f) a < N
⊢ Eq (α := ℕ) (sum (ofFn (n := n) fun (a : Fin n) ↦ f a)) (∑ j : Fin n, f j)

Tactic:
simp [sum_ofFn]

Premises used: List.sum_ofFn
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
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 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
m M N n : ℕ
f : Fin n → ℕ
hi :
  (m ≤ Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f) ∧
      Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f) < M) ∧
    ∀ (a : Fin (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f))),
      LE.le (α := ℕ) (1 : ℕ)
          (Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f) a : ℕ) ∧
        Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f) a < N
refine : ∀ {i : ℕ} (hi' : Membership.mem (γ := List ℕ) (ofFn (n := n) fun (a : Fin n) ↦ f a) i), 0 < i
⊢ (n : ℕ) × Composition n

Tactic:
refine ⟨∑ j, f j, ofFn fun a => f a, fun {i} hi' => ?_, by simp [sum_ofFn]⟩
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
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 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
m M N n : ℕ
f : Fin n → ℕ
hi :
  (m ≤ Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f) ∧
      Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f) < M) ∧
    ∀ (a : Fin (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f))),
      LE.le (α := ℕ) (1 : ℕ)
          (Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f) a : ℕ) ∧
        Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f) a < N
i : ℕ
hi' : Membership.mem (γ := List ℕ) (ofFn (n := n) fun (a : Fin n) ↦ f a) i
rwa : ∀ (hi' : Membership.mem (γ := Set ℕ) (Set.range fun (a : Fin n) ↦ f a) i), ∃ (j : Fin n), f j = i
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (hi' : ∃ (y : Fin n), f y = i), ∃ (j : Fin n), f j = i
⊢ ∃ (j : Fin n), f j = i

Tactic:
rwa [mem_ofFn', Set.mem_range] at hi'

Premises used: Set.mem_range, List.mem_ofFn'
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
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 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
m M N n : ℕ
f : Fin n → ℕ
hi :
  (m ≤ Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f) ∧
      Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f) < M) ∧
    ∀ (a : Fin (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f))),
      LE.le (α := ℕ) (1 : ℕ)
          (Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f) a : ℕ) ∧
        Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f) a < N
i : ℕ
hi' : Membership.mem (γ := List ℕ) (ofFn (n := n) fun (a : Fin n) ↦ f a) i
obtain : ∀ (j : Fin n) (hi' : Membership.mem (γ := List ℕ) (ofFn (n := n) fun (a : Fin n) ↦ f a) (f j)), 0 < f j
⊢ 0 < i

Tactic:
obtain ⟨j, rfl⟩ : ∃ j : Fin n, f j = i := by rwa [mem_ofFn', Set.mem_range] at hi'

Premises used: Fin, rfl
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
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 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
m M N n : ℕ
f : Fin n → ℕ
hi :
  (m ≤ Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f) ∧
      Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f) < M) ∧
    ∀ (a : Fin (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f))),
      LE.le (α := ℕ) (1 : ℕ)
          (Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f) a : ℕ) ∧
        Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f) a < N
j : Fin n
hi' : Membership.mem (γ := List ℕ) (ofFn (n := n) fun (a : Fin n) ↦ f a) (f j)
⊢ 0 < f j

Tactic:
(hi.2 j).1

Premises used: And.right, And.left, Nat.lt
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
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 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
m M N n : ℕ
f : Fin n → ℕ
hi :
  (m ≤ Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f) ∧
      Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f) < M) ∧
    ∀ (a : Fin (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f))),
      LE.le (α := ℕ) (1 : ℕ)
          (Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f) a : ℕ) ∧
        Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f) a < N
j : Fin n
hi' : Membership.mem (γ := List ℕ) (ofFn (n := n) fun (a : Fin n) ↦ f a) (f j)
⊢ 0 < f j

Tactic:
exact (hi.2 j).1

Premises used: And.right, And.left
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
m M N : ℕ
i : (n : ℕ) × (Fin n → ℕ)
hi : i ∈ compPartialSumSource m M N
rcases :
  ∀ (k : ℕ) (blocks_fun : Fin k → ℕ)
    (hi : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun ∈ compPartialSumSource m M N),
    (compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) hi).snd (β := fun (n : ℕ) ↦
          Composition n).length =
      Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun)
⊢ (compChangeOfVariables m M N i hi).snd (β := fun (n : ℕ) ↦ Composition n).length =
    i.fst (β := fun (n : ℕ) ↦ Fin n → ℕ)

Tactic:
rcases i with ⟨k, blocks_fun⟩
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
m M N k : ℕ
blocks_fun : Fin k → ℕ
hi : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun ∈ compPartialSumSource m M N
dsimp :
  { blocks := ofFn (n := k) fun (a : Fin k) ↦ blocks_fun a, blocks_pos := ⋯, blocks_sum := ⋯ :
        Composition (∑ j : Fin k, blocks_fun j) }.length =
    k
⊢ (compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) hi).snd (β := fun (n : ℕ) ↦
        Composition n).length =
    Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun)

Tactic:
dsimp [compChangeOfVariables]

Premises used: FormalMultilinearSeries.compChangeOfVariables
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
m M N k : ℕ
blocks_fun : Fin k → ℕ
hi : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun ∈ compPartialSumSource m M N
⊢ { blocks := ofFn (n := k) fun (a : Fin k) ↦ blocks_fun a, blocks_pos := ⋯, blocks_sum := ⋯ :
        Composition (∑ j : Fin k, blocks_fun j) }.length =
    k

Tactic:
simp only [Composition.length, length_ofFn]

Premises used: Composition.length, List.length_ofFn
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
m M N : ℕ
i : (n : ℕ) × (Fin n → ℕ)
hi : i ∈ compPartialSumSource m M N
j : Fin (i.fst (β := fun (n : ℕ) ↦ Fin n → ℕ))
rcases :
  ∀ (n : ℕ) (f : Fin n → ℕ) (hi : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f ∈ compPartialSumSource m M N)
    (j : Fin (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f))),
    (compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f) hi).snd (β := fun (n : ℕ) ↦
            Composition n).blocksFun
        (⟨(↑j : ℕ), ⋯⟩ :
          Fin
            (compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f) hi).snd (β := fun (n : ℕ) ↦
                Composition n).length) =
      Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f) j
⊢ (compChangeOfVariables m M N i hi).snd (β := fun (n : ℕ) ↦ Composition n).blocksFun
      (⟨(↑j : ℕ), ⋯⟩ : Fin (compChangeOfVariables m M N i hi).snd (β := fun (n : ℕ) ↦ Composition n).length) =
    i.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) j

Tactic:
rcases i with ⟨n, f⟩
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
m M N n : ℕ
f : Fin n → ℕ
hi : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f ∈ compPartialSumSource m M N
j : Fin (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f))
dsimp :
  getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (ofFn (n := n) fun (a : Fin n) ↦ f a) (↑j : ℕ) ⋯ = f j
⊢ (compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f) hi).snd (β := fun (n : ℕ) ↦
          Composition n).blocksFun
      (⟨(↑j : ℕ), ⋯⟩ :
        Fin
          (compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f) hi).snd (β := fun (n : ℕ) ↦
              Composition n).length) =
    Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f) j

Tactic:
dsimp [Composition.blocksFun, Composition.blocks, compChangeOfVariables]

Premises used: Composition.blocks, Composition.blocksFun, FormalMultilinearSeries.compChangeOfVariables