-- Mathlib/Analysis/Analytic/Composition.lean
theorem sigma_pi_composition_eq_iff
    (u v : Σ c : Composition n, ∀ i : Fin c.length, Composition (c.blocksFun i)) :
    u = v ↔ (ofFn fun i => (u.2 i).blocks) = ofFn fun i => (v.2 i).blocks

Proof state:
n : ℕ
u v : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))
H : (ofFn fun i => (u.snd i).blocks) = ofFn fun i => (v.snd i).blocks
⊢ u = v

Tactic:
rcases u with ⟨a, b⟩

Result:
case mk
n : ℕ
v : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))
a : Composition n
b : (i : Fin a.length) → Composition (a.blocksFun i)
H : (ofFn fun i => (⟨a, b⟩.snd i).blocks) = ofFn fun i => (v.snd i).blocks
⊢ ⟨a, b⟩ = v

Proof state:
case mk
n : ℕ
v : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))
a : Composition n
b : (i : Fin a.length) → Composition (a.blocksFun i)
H : (ofFn fun i => (⟨a, b⟩.snd i).blocks) = ofFn fun i => (v.snd i).blocks
⊢ ⟨a, b⟩ = v

Tactic:
rcases v with ⟨a', b'⟩

Result:
case mk.mk
n : ℕ
a : Composition n
b : (i : Fin a.length) → Composition (a.blocksFun i)
a' : Composition n
b' : (i : Fin a'.length) → Composition (a'.blocksFun i)
H : (ofFn fun i => (⟨a, b⟩.snd i).blocks) = ofFn fun i => (⟨a', b'⟩.snd i).blocks
⊢ ⟨a, b⟩ = ⟨a', b'⟩

Proof state:
case blocks
n : ℕ
a : Composition n
b : (i : Fin a.length) → Composition (a.blocksFun i)
a' : Composition n
b' : (i : Fin a'.length) → Composition (a'.blocksFun i)
H : (ofFn fun i => (b i).blocks) = ofFn fun i => (b' i).blocks
this : (ofFn fun i => (b i).blocks.sum) = ofFn fun i => (b' i).blocks.sum
⊢ a.blocks = a'.blocks

Tactic:
simpa [Composition.blocks_sum, Composition.ofFn_blocksFun] using this

Result:
no goals

Proof state:
n : ℕ
a : Composition n
b : (i : Fin a.length) → Composition (a.blocksFun i)
a' : Composition n
b' : (i : Fin a'.length) → Composition (a'.blocksFun i)
H : (ofFn fun i => (b i).blocks) = ofFn fun i => (b' i).blocks
⊢ a = a'

Tactic:
ext1

Result:
case blocks
n : ℕ
a : Composition n
b : (i : Fin a.length) → Composition (a.blocksFun i)
a' : Composition n
b' : (i : Fin a'.length) → Composition (a'.blocksFun i)
H : (ofFn fun i => (b i).blocks) = ofFn fun i => (b' i).blocks
⊢ a.blocks = a'.blocks

Proof state:
case mk.mk.snd
n : ℕ
a : Composition n
b b' : (i : Fin a.length) → Composition (a.blocksFun i)
H : (ofFn fun i => (b i).blocks) = ofFn fun i => (b' i).blocks
⊢ HEq ⟨a, b⟩.snd ⟨a, b'⟩.snd

Tactic:
simp only [heq_eq_eq, ofFn_inj] at H ⊢

Result:
case mk.mk.snd
n : ℕ
a : Composition n
b b' : (i : Fin a.length) → Composition (a.blocksFun i)
H : (fun i => (b i).blocks) = fun i => (b' i).blocks
⊢ b = b'

Proof state:
case blocks
n : ℕ
a : Composition n
b : (i : Fin a.length) → Composition (a.blocksFun i)
a' : Composition n
b' : (i : Fin a'.length) → Composition (a'.blocksFun i)
H : (ofFn fun i => (b i).blocks) = ofFn fun i => (b' i).blocks
this : ofFn (sum ∘ fun i => (b i).blocks) = ofFn (sum ∘ fun i => (b' i).blocks)
⊢ a.blocks = a'.blocks

Tactic:
change
  (ofFn fun i : Fin (Composition.length a) => (b i).blocks.sum) =
    ofFn fun i : Fin (Composition.length a') => (b' i).blocks.sum at this

Result:
case blocks
n : ℕ
a : Composition n
b : (i : Fin a.length) → Composition (a.blocksFun i)
a' : Composition n
b' : (i : Fin a'.length) → Composition (a'.blocksFun i)
H : (ofFn fun i => (b i).blocks) = ofFn fun i => (b' i).blocks
this : (ofFn fun i => (b i).blocks.sum) = ofFn fun i => (b' i).blocks.sum
⊢ a.blocks = a'.blocks

Proof state:
case mk.mk.snd.h.blocks
n : ℕ
a : Composition n
b b' : (i : Fin a.length) → Composition (a.blocksFun i)
H : (fun i => (b i).blocks) = fun i => (b' i).blocks
i : Fin a.length
⊢ (b i).blocks = (b' i).blocks

Tactic:
exact congrFun H i

Result:
no goals

Proof state:
case mk.mk
n : ℕ
a : Composition n
b : (i : Fin a.length) → Composition (a.blocksFun i)
a' : Composition n
b' : (i : Fin a'.length) → Composition (a'.blocksFun i)
H : (ofFn fun i => (b i).blocks) = ofFn fun i => (b' i).blocks
⊢ ⟨a, b⟩ = ⟨a', b'⟩

Tactic:
obtain rfl : a = a' := by
  ext1
  have :
    map List.sum (ofFn fun i : Fin (Composition.length a) => (b i).blocks) =
      map List.sum (ofFn fun i : Fin (Composition.length a') => (b' i).blocks) := by
    rw [H]
  simp only [map_ofFn] at this
  change
    (ofFn fun i : Fin (Composition.length a) => (b i).blocks.sum) =
      ofFn fun i : Fin (Composition.length a') => (b' i).blocks.sum at this
  simpa [Composition.blocks_sum, Composition.ofFn_blocksFun] using this

Result:
case mk.mk
n : ℕ
a : Composition n
b b' : (i : Fin a.length) → Composition (a.blocksFun i)
H : (ofFn fun i => (b i).blocks) = ofFn fun i => (b' i).blocks
⊢ ⟨a, b⟩ = ⟨a, b'⟩

Proof state:
case mk.mk.fst
n : ℕ
a : Composition n
b b' : (i : Fin a.length) → Composition (a.blocksFun i)
H : (ofFn fun i => (b i).blocks) = ofFn fun i => (b' i).blocks
⊢ ⟨a, b⟩.fst = ⟨a, b'⟩.fst

Tactic:
rfl

Result:
no goals

Proof state:
case mk.mk.snd
n : ℕ
a : Composition n
b b' : (i : Fin a.length) → Composition (a.blocksFun i)
H : (fun i => (b i).blocks) = fun i => (b' i).blocks
⊢ b = b'

Tactic:
ext1 i

Result:
case mk.mk.snd.h
n : ℕ
a : Composition n
b b' : (i : Fin a.length) → Composition (a.blocksFun i)
H : (fun i => (b i).blocks) = fun i => (b' i).blocks
i : Fin a.length
⊢ b i = b' i

Proof state:
case mk.mk.snd.h
n : ℕ
a : Composition n
b b' : (i : Fin a.length) → Composition (a.blocksFun i)
H : (fun i => (b i).blocks) = fun i => (b' i).blocks
i : Fin a.length
⊢ b i = b' i

Tactic:
ext1

Result:
case mk.mk.snd.h.blocks
n : ℕ
a : Composition n
b b' : (i : Fin a.length) → Composition (a.blocksFun i)
H : (fun i => (b i).blocks) = fun i => (b' i).blocks
i : Fin a.length
⊢ (b i).blocks = (b' i).blocks

Proof state:
case mk.mk
n : ℕ
a : Composition n
b : (i : Fin a.length) → Composition (a.blocksFun i)
a' : Composition n
b' : (i : Fin a'.length) → Composition (a'.blocksFun i)
H : (ofFn fun i => (⟨a, b⟩.snd i).blocks) = ofFn fun i => (⟨a', b'⟩.snd i).blocks
⊢ ⟨a, b⟩ = ⟨a', b'⟩

Tactic:
dsimp at H

Result:
case mk.mk
n : ℕ
a : Composition n
b : (i : Fin a.length) → Composition (a.blocksFun i)
a' : Composition n
b' : (i : Fin a'.length) → Composition (a'.blocksFun i)
H : (ofFn fun i => (b i).blocks) = ofFn fun i => (b' i).blocks
⊢ ⟨a, b⟩ = ⟨a', b'⟩

Proof state:
case blocks
n : ℕ
a : Composition n
b : (i : Fin a.length) → Composition (a.blocksFun i)
a' : Composition n
b' : (i : Fin a'.length) → Composition (a'.blocksFun i)
H : (ofFn fun i => (b i).blocks) = ofFn fun i => (b' i).blocks
this : List.map sum (ofFn fun i => (b i).blocks) = List.map sum (ofFn fun i => (b' i).blocks)
⊢ a.blocks = a'.blocks

Tactic:
simp only [map_ofFn] at this

Result:
case blocks
n : ℕ
a : Composition n
b : (i : Fin a.length) → Composition (a.blocksFun i)
a' : Composition n
b' : (i : Fin a'.length) → Composition (a'.blocksFun i)
H : (ofFn fun i => (b i).blocks) = ofFn fun i => (b' i).blocks
this : ofFn (sum ∘ fun i => (b i).blocks) = ofFn (sum ∘ fun i => (b' i).blocks)
⊢ a.blocks = a'.blocks

Proof state:
n : ℕ
a : Composition n
b : (i : Fin a.length) → Composition (a.blocksFun i)
a' : Composition n
b' : (i : Fin a'.length) → Composition (a'.blocksFun i)
H : (ofFn fun i => (b i).blocks) = ofFn fun i => (b' i).blocks
⊢ List.map sum (ofFn fun i => (b i).blocks) = List.map sum (ofFn fun i => (b' i).blocks)

Tactic:
rw [H]

Result:
no goals