n : ℕ
c✝ : Composition n
c c' : (n : ℕ) × Composition n
H : c.snd.blocks = c'.snd.blocks
⊢ c = c'
n : ℕ
c✝ : Composition n
c c' : (n : ℕ) × Composition n
⊢ c = c' ↔ c.snd.blocks = c'.snd.blocks
refine' ⟨fun H => by rw [H], fun H => _⟩
case mk
n✝ : ℕ
c✝ : Composition n✝
c' : (n : ℕ) × Composition n
n : ℕ
c : Composition n
H : { fst := n, snd := c }.snd.blocks = c'.snd.blocks
⊢ { fst := n, snd := c } = c'
n : ℕ
c✝ : Composition n
c c' : (n : ℕ) × Composition n
H : c.snd.blocks = c'.snd.blocks
⊢ c = c'
rcases c with ⟨n, c⟩
case mk.mk
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n'
H : { fst := n, snd := c }.snd.blocks = { fst := n', snd := c' }.snd.blocks
⊢ { fst := n, snd := c } = { fst := n', snd := c' }
case mk
n✝ : ℕ
c✝ : Composition n✝
c' : (n : ℕ) × Composition n
n : ℕ
c : Composition n
H : { fst := n, snd := c }.snd.blocks = c'.snd.blocks
⊢ { fst := n, snd := c } = c'
rcases c' with ⟨n', c'⟩
case mk.mk
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n'
H : { fst := n, snd := c }.snd.blocks = { fst := n', snd := c' }.snd.blocks
this : n = n'
⊢ { fst := n, snd := c } = { fst := n', snd := c' }
case mk.mk
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n'
H : { fst := n, snd := c }.snd.blocks = { fst := n', snd := c' }.snd.blocks
⊢ { fst := n, snd := c } = { fst := n', snd := c' }
have : n = n' := by rw [← c.blocks_sum, ← c'.blocks_sum, H]
case mk.mk.refl
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n
H : { fst := n, snd := c }.snd.blocks = { fst := n, snd := c' }.snd.blocks
⊢ { fst := n, snd := c } = { fst := n, snd := c' }
case mk.mk
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n'
H : { fst := n, snd := c }.snd.blocks = { fst := n', snd := c' }.snd.blocks
this : n = n'
⊢ { fst := n, snd := c } = { fst := n', snd := c' }
induction this
case mk.mk.refl.e_snd
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n
H : { fst := n, snd := c }.snd.blocks = { fst := n, snd := c' }.snd.blocks
⊢ c = c'
case mk.mk.refl
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n
H : { fst := n, snd := c }.snd.blocks = { fst := n, snd := c' }.snd.blocks
⊢ { fst := n, snd := c } = { fst := n, snd := c' }
congr
case mk.mk.refl.e_snd.blocks
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n
H : { fst := n, snd := c }.snd.blocks = { fst := n, snd := c' }.snd.blocks
⊢ c.blocks = c'.blocks
case mk.mk.refl.e_snd
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n
H : { fst := n, snd := c }.snd.blocks = { fst := n, snd := c' }.snd.blocks
⊢ c = c'
ext1
no goals
case mk.mk.refl.e_snd.blocks
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n
H : { fst := n, snd := c }.snd.blocks = { fst := n, snd := c' }.snd.blocks
⊢ c.blocks = c'.blocks
exact H
no goals
n : ℕ
c✝ : Composition n
c c' : (n : ℕ) × Composition n
H : c = c'
⊢ c.snd.blocks = c'.snd.blocks
rw [H]
no goals
n✝ : ℕ
c✝ : Composition n✝
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n'
H : { fst := n, snd := c }.snd.blocks = { fst := n', snd := c' }.snd.blocks
⊢ n = n'
rw [← c.blocks_sum, ← c'.blocks_sum, H]