-- Mathlib/Analysis/Analytic/Composition.lean
theorem compChangeOfVariables_sum {α : Type*} [AddCommMonoid α] (m M N : ℕ)
    (f : (Σ n : ℕ, Fin n → ℕ) → α) (g : (Σ n, Composition n) → α)
    (h : ∀ (e) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)) :
    ∑ e ∈ compPartialSumSource m M N, f e = ∑ e ∈ compPartialSumTarget m M N, g e

Proof state:
case hi.mk
α : 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✝ : ⟨k, blocks_fun⟩ ∈ compPartialSumSource m M N
H : (m ≤ k ∧ k < M) ∧ ∀ (a : Fin k), 1 ≤ blocks_fun a ∧ blocks_fun a < N
⊢ ∀ (j : Fin (ofFn fun a => blocks_fun a).length),
    { blocks := ofFn fun a => blocks_fun a, blocks_pos := ⋯, blocks_sum := ⋯ }.blocksFun j < N

Tactic:
intro j

Result:
case hi.mk
α : 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✝ : ⟨k, blocks_fun⟩ ∈ compPartialSumSource m M N
H : (m ≤ k ∧ k < M) ∧ ∀ (a : Fin k), 1 ≤ blocks_fun a ∧ blocks_fun a < N
j : Fin (ofFn fun a => blocks_fun a).length
⊢ { blocks := ofFn fun a => blocks_fun a, blocks_pos := ⋯, blocks_sum := ⋯ }.blocksFun j < N

Proof state:
case h
α : 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)
⊢ ∀ (a : (n : ℕ) × (Fin n → ℕ)) (ha : a ∈ compPartialSumSource m M N), f a = g (compChangeOfVariables m M N a ha)

Tactic:
rintro ⟨k, blocks_fun⟩ H

Result:
case h.mk
α : 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 : ⟨k, blocks_fun⟩ ∈ compPartialSumSource m M N
⊢ f ⟨k, blocks_fun⟩ = g (compChangeOfVariables m M N ⟨k, blocks_fun⟩ H)

Proof state:
case i_inj
α : 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)
⊢ ∀ (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:
rintro ⟨k, blocks_fun⟩ H ⟨k', blocks_fun'⟩ H' heq

Result:
case i_inj.mk.mk
α : 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 : ⟨k, blocks_fun⟩ ∈ compPartialSumSource m M N
k' : ℕ
blocks_fun' : Fin k' → ℕ
H' : ⟨k', blocks_fun'⟩ ∈ compPartialSumSource m M N
heq : compChangeOfVariables m M N ⟨k, blocks_fun⟩ H = compChangeOfVariables m M N ⟨k', blocks_fun'⟩ H'
⊢ ⟨k, blocks_fun⟩ = ⟨k', blocks_fun'⟩

Proof state:
case hi.mk
α : 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✝ : ⟨k, blocks_fun⟩ ∈ compPartialSumSource m M N
H :
  (m ≤ ⟨k, blocks_fun⟩.fst ∧ ⟨k, blocks_fun⟩.fst < M) ∧
    ∀ (a : Fin ⟨k, blocks_fun⟩.fst), 1 ≤ ⟨k, blocks_fun⟩.snd a ∧ ⟨k, blocks_fun⟩.snd a < N
⊢ compChangeOfVariables m M N ⟨k, blocks_fun⟩ H✝ ∈ compPartialSumTarget m M N

Tactic:
simp only at H

Result:
case hi.mk
α : 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✝ : ⟨k, blocks_fun⟩ ∈ compPartialSumSource m M N
H : (m ≤ k ∧ k < M) ∧ ∀ (a : Fin k), 1 ≤ blocks_fun a ∧ blocks_fun a < N
⊢ compChangeOfVariables m M N ⟨k, blocks_fun⟩ H✝ ∈ compPartialSumTarget m M N

Proof state:
α : 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 : ⟨k, blocks_fun⟩ ∈ compPartialSumSource m M N
k' : ℕ
blocks_fun' : Fin k' → ℕ
H' : ⟨k', blocks_fun'⟩ ∈ compPartialSumSource m M N
heq : compChangeOfVariables m M N ⟨k, blocks_fun⟩ H = compChangeOfVariables m M N ⟨k', blocks_fun'⟩ H'
this : ⟨k, blocks_fun⟩.fst = (compChangeOfVariables m M N ⟨k, blocks_fun⟩ H).snd.length
⊢ k = k'

Tactic:
rwa [heq, compChangeOfVariables_length] at this

Result:
no goals

Proof state:
case h.mk
α : 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 : ⟨k, blocks_fun⟩ ∈ compPartialSumSource m M N
⊢ f ⟨k, blocks_fun⟩ = g (compChangeOfVariables m M N ⟨k, blocks_fun⟩ H)

Tactic:
rw [h]

Result:
no goals