-- Mathlib/Analysis/Analytic/Composition.lean
theorem compPartialSumTargetSet_image_compPartialSumSource (m M N : ℕ)
    (i : Σ n, Composition n) (hi : i ∈ compPartialSumTargetSet m M N) :
    ∃ (j : _) (hj : j ∈ compPartialSumSource m M N), compChangeOfVariables m M N j hj = i

Proof state:
case mk.refine_2
m M N n : ℕ
c : Composition n
hi : ⟨n, c⟩ ∈ compPartialSumTargetSet m M N
⊢ (ofFn fun a => c.blocks.get a) = c.blocks

Tactic:
conv_rhs => rw [← List.ofFn_get c.blocks]

Result:
no goals

Proof state:
case mk.refine_1
m M N n : ℕ
c : Composition n
hi : m ≤ c.length ∧ c.length < M ∧ ∀ (j : Fin c.length), c.blocksFun j < N
⊢ ∀ (a : Fin c.length), 1 ≤ c.blocksFun a

Tactic:
exact fun a => c.one_le_blocks' _

Result:
no goals

Proof state:
case mk.refine_2
m M N n : ℕ
c : Composition n
hi : ⟨n, c⟩ ∈ compPartialSumTargetSet m M N
⊢ compChangeOfVariables m M N ⟨c.length, c.blocksFun⟩ ⋯ = ⟨n, c⟩

Tactic:
dsimp [compChangeOfVariables]

Result:
case mk.refine_2
m M N n : ℕ
c : Composition n
hi : ⟨n, c⟩ ∈ compPartialSumTargetSet m M N
⊢ ⟨∑ j : Fin c.length, c.blocksFun j, { blocks := ofFn fun a => c.blocksFun a, blocks_pos := ⋯, blocks_sum := ⋯ }⟩ =
    ⟨n, c⟩

Proof state:
m M N : ℕ
i : (n : ℕ) × Composition n
hi : i ∈ compPartialSumTargetSet m M N
⊢ ∃ j, ∃ (hj : j ∈ compPartialSumSource m M N), compChangeOfVariables m M N j hj = i

Tactic:
rcases i with ⟨n, c⟩

Result:
case mk
m M N n : ℕ
c : Composition n
hi : ⟨n, c⟩ ∈ compPartialSumTargetSet m M N
⊢ ∃ j, ∃ (hj : j ∈ compPartialSumSource m M N), compChangeOfVariables m M N j hj = ⟨n, c⟩

Proof state:
case mk.refine_2
m M N n : ℕ
c : Composition n
hi : ⟨n, c⟩ ∈ compPartialSumTargetSet m M N
⊢ ⟨∑ j : Fin c.length, c.blocksFun j, { blocks := ofFn fun a => c.blocksFun a, blocks_pos := ⋯, blocks_sum := ⋯ }⟩ =
    ⟨n, c⟩

Tactic:
rw [Composition.sigma_eq_iff_blocks_eq]

Result:
case mk.refine_2
m M N n : ℕ
c : Composition n
hi : ⟨n, c⟩ ∈ compPartialSumTargetSet m M N
⊢ ⟨∑ j : Fin c.length, c.blocksFun j,
          { blocks := ofFn fun a => c.blocksFun a, blocks_pos := ⋯, blocks_sum := ⋯ }⟩.snd.blocks =
    ⟨n, c⟩.snd.blocks

Proof state:
case mk.refine_1
m M N n : ℕ
c : Composition n
hi : ⟨n, c⟩ ∈ compPartialSumTargetSet m M N
⊢ ⟨c.length, c.blocksFun⟩ ∈ compPartialSumSource m M N

Tactic:
simp only [compPartialSumTargetSet, Set.mem_setOf_eq] at hi

Result:
case mk.refine_1
m M N n : ℕ
c : Composition n
hi : m ≤ c.length ∧ c.length < M ∧ ∀ (j : Fin c.length), c.blocksFun j < N
⊢ ⟨c.length, c.blocksFun⟩ ∈ compPartialSumSource m M N

Proof state:
case mk.refine_1
m M N n : ℕ
c : Composition n
hi : m ≤ c.length ∧ c.length < M ∧ ∀ (j : Fin c.length), c.blocksFun j < N
⊢ ⟨c.length, c.blocksFun⟩ ∈ compPartialSumSource m M N

Tactic:
simp only [mem_compPartialSumSource_iff, hi.left, hi.right, true_and, and_true]

Result:
case mk.refine_1
m M N n : ℕ
c : Composition n
hi : m ≤ c.length ∧ c.length < M ∧ ∀ (j : Fin c.length), c.blocksFun j < N
⊢ ∀ (a : Fin c.length), 1 ≤ c.blocksFun a

Proof state:
case mk
m M N n : ℕ
c : Composition n
hi : ⟨n, c⟩ ∈ compPartialSumTargetSet m M N
⊢ ∃ j, ∃ (hj : j ∈ compPartialSumSource m M N), compChangeOfVariables m M N j hj = ⟨n, c⟩

Tactic:
refine ⟨⟨c.length, c.blocksFun⟩, ?_, ?_⟩

Result:
case mk.refine_1
m M N n : ℕ
c : Composition n
hi : ⟨n, c⟩ ∈ compPartialSumTargetSet m M N
⊢ ⟨c.length, c.blocksFun⟩ ∈ compPartialSumSource m M N

case mk.refine_2
m M N n : ℕ
c : Composition n
hi : ⟨n, c⟩ ∈ compPartialSumTargetSet m M N
⊢ compChangeOfVariables m M N ⟨c.length, c.blocksFun⟩ ?mk.refine_1 = ⟨n, c⟩

Proof state:
case mk.refine_2
m M N n : ℕ
c : Composition n
hi : ⟨n, c⟩ ∈ compPartialSumTargetSet m M N
⊢ ⟨∑ j : Fin c.length, c.blocksFun j,
          { blocks := ofFn fun a => c.blocksFun a, blocks_pos := ⋯, blocks_sum := ⋯ }⟩.snd.blocks =
    ⟨n, c⟩.snd.blocks

Tactic:
simp only [Composition.blocksFun, Composition.blocks, Subtype.coe_eta]

Result:
case mk.refine_2
m M N n : ℕ
c : Composition n
hi : ⟨n, c⟩ ∈ compPartialSumTargetSet m M N
⊢ (ofFn fun a => c.blocks.get a) = c.blocks