awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
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)
have 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)
Tactic: refine
    le_radius_of_bound_nnreal _
      (∑' i : Σ n, Composition n, ‖compAlongComposition q p i.snd‖₊ * r ^ i.fst) fun n => ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
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 ≤ ∑' (c : Composition n), ‖q.compAlongComposition p c‖₊ * r ^ n
have rw : ‖q.comp p n‖₊ * r ^ n ≤ (∑ i : Composition n, ‖q.compAlongComposition p i‖₊) * r ^ n
Tactic: rw [tsum_fintype, ← Finset.sum_mul]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
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 : (n : ℕ) × Composition n),
      ‖q.compAlongComposition p (i.snd (β := fun (n : ℕ) ↦ Composition n))‖₊ *
        r ^ i.fst (β := fun (n : ℕ) ↦ Composition n)
have q₁ : ‖q.comp p n‖₊ * r ^ n ≤ ∑' (c : Composition n), ‖q.compAlongComposition p c‖₊ * r ^ 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
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
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
⊢ (n : ℕ) × Composition n
have rcases : (n : ℕ) →
  (f : Fin n → ℕ) →
    (hi : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) n f ∈ compPartialSumSource m M N) → (n : ℕ) × Composition n
Tactic: rcases i with ⟨n, f⟩
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (hypothesis)
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
⊢ (n : ℕ) × Composition n
have 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
Tactic: rw [mem_compPartialSumSource_iff] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
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
⊢ (n : ℕ) × Composition n
have refine : ∀ {i : ℕ} (hi' : Membership.mem (γ := List ℕ) (ofFn (n := n) fun (a : Fin n) ↦ f a) i), 0 < i
Tactic: refine ⟨∑ j, f j, ofFn fun a => f a, fun {i} hi' => ?_, by simp [sum_ofFn]⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
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
⊢ ∃ (j : Fin n), f j = i
have rwa : ∀ (hi' : Membership.mem (γ := Set ℕ) (Set.range fun (a : Fin n) ↦ f a) i), ∃ (j : Fin n), f j = i
Tactic: rwa [mem_ofFn', Set.mem_range] at hi'
Cleared hypotheses: hi'
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
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
⊢ ∃ (j : Fin n), f j = i
have rwa₁ : ∀ (hi' : ∃ (y : Fin n), f y = i), ∃ (j : Fin n), f j = i
Tactic: rwa [mem_ofFn', Set.mem_range] at hi'
Cleared hypotheses: hi'
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
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
⊢ 0 < i
have obtain : ∀ (j : Fin n) (hi' : Membership.mem (γ := List ℕ) (ofFn (n := n) fun (a : Fin n) ↦ f a) (f j)), 0 < f j
Tactic: obtain ⟨j, rfl⟩ : ∃ j : Fin n, f j = i := by rwa [mem_ofFn', Set.mem_range] at hi'
Cleared hypotheses: i, hi'
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
m M N : ℕ
i : (n : ℕ) × (Fin n → ℕ)
hi : i ∈ compPartialSumSource m M N
⊢ (compChangeOfVariables m M N i hi).snd (β := fun (n : ℕ) ↦ Composition n).length =
    i.fst (β := fun (n : ℕ) ↦ Fin n → ℕ)
have 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)
Tactic: rcases i with ⟨k, blocks_fun⟩
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
m M N 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)
have dsimp : { blocks := ofFn (n := k) fun (a : Fin k) ↦ blocks_fun a, blocks_pos := sorry, blocks_sum := sorry :
      Composition (∑ j : Fin k, blocks_fun j) }.length =
  k
Tactic: dsimp [compChangeOfVariables]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
m M N : ℕ
i : (n : ℕ) × (Fin n → ℕ)
hi : i ∈ compPartialSumSource m M N
j : Fin (i.fst (β := fun (n : ℕ) ↦ Fin n → ℕ))
⊢ (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
have 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 : ℕ), sorry⟩ :
        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: rcases i with ⟨n, f⟩
Cleared hypotheses: i, hi, j
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
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))
⊢ (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
have dsimp : getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (ofFn (n := n) fun (a : Fin n) ↦ f a) (↑j : ℕ) sorry = f j
Tactic: dsimp [Composition.blocksFun, Composition.blocks, compChangeOfVariables]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
m M N : ℕ
i : (n : ℕ) × Composition n
hi : i ∈ compPartialSumTargetSet m M N
⊢ ∃ (j : (n : ℕ) × (Fin n → ℕ)) (hj : j ∈ compPartialSumSource m M N), compChangeOfVariables m M N j hj = i
have rcases : ∀ (n : ℕ) (c : Composition n) (hi : Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c ∈ compPartialSumTargetSet m M N),
  ∃ (j : (n : ℕ) × (Fin n → ℕ)) (hj : j ∈ compPartialSumSource m M N),
    compChangeOfVariables m M N j hj = Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c
Tactic: rcases i with ⟨n, c⟩
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
m M N n : ℕ
c : Composition n
hi : Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c ∈ compPartialSumTargetSet m M N
⊢ ∃ (j : (n : ℕ) × (Fin n → ℕ)) (hj : j ∈ compPartialSumSource m M N),
    compChangeOfVariables m M N j hj = Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c
have refine_1 : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) c.length c.blocksFun ∈ compPartialSumSource m M N
Tactic: refine ⟨⟨c.length, c.blocksFun⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
m M N n : ℕ
c : Composition n
hi : Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c ∈ compPartialSumTargetSet m M N
refine_1 : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) c.length c.blocksFun ∈ compPartialSumSource m M N
⊢ ∃ (j : (n : ℕ) × (Fin n → ℕ)) (hj : j ∈ compPartialSumSource m M N),
    compChangeOfVariables m M N j hj = Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c
have refine_2 : compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) c.length c.blocksFun) sorry =
  Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c
Tactic: refine ⟨⟨c.length, c.blocksFun⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
m M N n : ℕ
c : Composition n
hi : m ≤ c.length ∧ c.length < M ∧ ∀ (j : Fin c.length), c.blocksFun j < N
⊢ Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) c.length c.blocksFun ∈ compPartialSumSource m M N
have refine_1 : ∀ (a : Fin c.length), 1 ≤ c.blocksFun a
Tactic: simp only [mem_compPartialSumSource_iff, hi.left, hi.right, true_and, and_true]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
m M N n : ℕ
c : Composition n
hi : Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c ∈ compPartialSumTargetSet m M N
⊢ Sigma.mk (β := fun (n : ℕ) ↦ Composition n) (∑ j : Fin c.length, c.blocksFun j)
      { blocks := ofFn (n := c.length) fun (a : Fin c.length) ↦ c.blocksFun a, blocks_pos := ⋯, blocks_sum := ⋯ :
        Composition (∑ j : Fin c.length, c.blocksFun j) } =
    Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c
have refine_2 : (Sigma.mk (β := fun (n : ℕ) ↦ Composition n) (∑ j : Fin c.length, c.blocksFun j)
          { blocks := ofFn (n := c.length) fun (a : Fin c.length) ↦ c.blocksFun a, blocks_pos := sorry, blocks_sum := sorry :
            Composition (∑ j : Fin c.length, c.blocksFun j) }).snd
      (β := fun (n : ℕ) ↦ Composition n).blocks =
  (Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c).snd (β := fun (n : ℕ) ↦ Composition n).blocks
Tactic: rw [Composition.sigma_eq_iff_blocks_eq]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
m M N n : ℕ
c : Composition n
hi : Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c ∈ compPartialSumTargetSet m M N
⊢ (Sigma.mk (β := fun (n : ℕ) ↦ Composition n) (∑ j : Fin c.length, c.blocksFun j)
            { blocks := ofFn (n := c.length) fun (a : Fin c.length) ↦ c.blocksFun a, blocks_pos := ⋯, blocks_sum := ⋯ :
              Composition (∑ j : Fin c.length, c.blocksFun j) }).snd
        (β := fun (n : ℕ) ↦ Composition n).blocks =
    (Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c).snd (β := fun (n : ℕ) ↦ Composition n).blocks
have refine_2 : (ofFn (n := c.length) fun (a : Fin c.length) ↦ c.blocks.get a) = c.blocks
Tactic: simp only [Composition.blocksFun]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
m M N n : ℕ
c : Composition n
hi : Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c ∈ compPartialSumTargetSet m M N
| c.blocks
have rw : ofFn c.blocks.get
Tactic: rw [← List.ofFn_get c.blocks]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
m M N n : ℕ
c : Composition n
hi : Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c ∈ compPartialSumTargetSet m M N
⊢ (ofFn (n := c.length) fun (a : Fin c.length) ↦ c.blocks.get a) = c.blocks
have conv_rhs : (ofFn (n := c.length) fun (a : Fin c.length) ↦ c.blocks.get a) = c.blocks
Tactic: conv_rhs => rw [← List.ofFn_get c.blocks]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
m M N n : ℕ
c : Composition n
hi : Sigma.mk (β := fun (n : ℕ) ↦ Composition n) n c ∈ compPartialSumTargetSet m M N
conv_rhs : (ofFn (n := c.length) fun (a : Fin c.length) ↦ c.blocks.get a) = c.blocks
⊢ (ofFn (n := c.length) fun (a : Fin c.length) ↦ c.blocks.get a) = c.blocks
have refine_2 : (ofFn (n := c.length) fun (a : Fin c.length) ↦ c.blocks.get a) = ofFn c.blocks.get
Tactic: conv_rhs => rw [← List.ofFn_get c.blocks]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
α : Type u_6
inst : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
⊢ Eq.{u_6 + 1} (α := α) (∑ e ∈ compPartialSumSource m M N, f e) (∑ e ∈ compPartialSumTarget m M N, g e)
have hi : ∀ (a : (n : ℕ) × (Fin n → ℕ)) (ha : a ∈ compPartialSumSource m M N),
  compChangeOfVariables m M N a ha ∈ compPartialSumTarget m M N
Tactic: apply Finset.sum_bij (compChangeOfVariables m M N)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
α : Type u_6
inst : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
hi :
  ∀ (a : (n : ℕ) × (Fin n → ℕ)) (ha : a ∈ compPartialSumSource m M N),
    compChangeOfVariables m M N a ha ∈ compPartialSumTarget m M N
⊢ Eq.{u_6 + 1} (α := α) (∑ e ∈ compPartialSumSource m M N, f e) (∑ e ∈ compPartialSumTarget m M N, g e)
have i_inj : ∀ (a₁ : (n : ℕ) × (Fin n → ℕ)) (ha₁ : a₁ ∈ compPartialSumSource m M N) (a₂ : (n : ℕ) × (Fin n → ℕ))
  (ha₂ : a₂ ∈ compPartialSumSource m M N),
  compChangeOfVariables m M N a₁ ha₁ = compChangeOfVariables m M N a₂ ha₂ → a₁ = a₂
Tactic: apply Finset.sum_bij (compChangeOfVariables m M N)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
α : Type u_6
inst : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
hi :
  ∀ (a : (n : ℕ) × (Fin n → ℕ)) (ha : a ∈ compPartialSumSource m M N),
    compChangeOfVariables m M N a ha ∈ compPartialSumTarget m M N
i_inj :
  ∀ (a₁ : (n : ℕ) × (Fin n → ℕ)) (ha₁ : a₁ ∈ compPartialSumSource m M N) (a₂ : (n : ℕ) × (Fin n → ℕ))
    (ha₂ : a₂ ∈ compPartialSumSource m M N),
    compChangeOfVariables m M N a₁ ha₁ = compChangeOfVariables m M N a₂ ha₂ → a₁ = a₂
⊢ Eq.{u_6 + 1} (α := α) (∑ e ∈ compPartialSumSource m M N, f e) (∑ e ∈ compPartialSumTarget m M N, g e)
have i_surj : ∀ b ∈ compPartialSumTarget m M N,
  ∃ (a : (n : ℕ) × (Fin n → ℕ)) (ha : a ∈ compPartialSumSource m M N), compChangeOfVariables m M N a ha = b
Tactic: apply Finset.sum_bij (compChangeOfVariables m M N)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (hypothesis)
Goal:
α : Type u_6
inst : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
k : ℕ
blocks_fun : Fin k → ℕ
H : 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) H ∈ compPartialSumTarget m M N
have H₁ : (m ≤ Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) ∧
    Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) < M) ∧
  ∀ (a : Fin (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun))),
    LE.le (α := ℕ) (1 : ℕ)
        (Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) a : ℕ) ∧
      Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) a < N
Tactic: rw [mem_compPartialSumSource_iff] at H
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Composition (goal)
Goal:
α : Type u_6
inst : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
k : ℕ
blocks_fun : Fin k → ℕ
H_1 : Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun ∈ compPartialSumSource m M N
H :
  (m ≤ Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) ∧
      Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) < M) ∧
    ∀ (a : Fin (Sigma.fst (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun))),
      LE.le (α := ℕ) (1 : ℕ)
          (Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) a : ℕ) ∧
        Sigma.snd (β := fun (n : ℕ) ↦ Fin n → ℕ) (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) a < N
⊢ compChangeOfVariables m M N (Sigma.mk (β := fun (n : ℕ) ↦ Fin n → ℕ) k blocks_fun) H_1 ∈ compPartialSumTarget m M N
have hi : ∀ (j : Fin (length (α := ℕ) (ofFn (n := k) fun (a : Fin k) ↦ blocks_fun a))),
  { blocks := ofFn (n := k) fun (a : Fin k) ↦ blocks_fun a, blocks_pos := sorry, blocks_sum := sorry :
          Composition (∑ j : Fin k, blocks_fun j) }.blocksFun
      j <
    N
Tactic: simp only [mem_compPartialSumTarget_iff, Composition.length, H.left,
      length_ofFn, true_and, compChangeOfVariables]