case refl
n : ℕ
c : Composition n
n₁ : ℕ
c₁ : Composition n₁
i₁ : Fin (length c₁)
c₂ : Composition n₁
i₂ : Fin (length c₂)
hc : c₁.blocks = c₂.blocks
hi : ↑i₁ = ↑i₂
⊢ blocksFun c₁ i₁ = blocksFun c₂ i₂
n : ℕ
c : Composition n
n₁ n₂ : ℕ
c₁ : Composition n₁
c₂ : Composition n₂
i₁ : Fin (length c₁)
i₂ : Fin (length c₂)
hn : n₁ = n₂
hc : c₁.blocks = c₂.blocks
hi : ↑i₁ = ↑i₂
⊢ blocksFun c₁ i₁ = blocksFun c₂ i₂
cases hn
case refl
n : ℕ
c : Composition n
n₁ : ℕ
c₁ : Composition n₁
i₁ : Fin (length c₁)
c₂ : Composition n₁
i₂ : Fin (length c₂)
hc : c₁ = c₂
hi : ↑i₁ = ↑i₂
⊢ blocksFun c₁ i₁ = blocksFun c₂ i₂
case refl
n : ℕ
c : Composition n
n₁ : ℕ
c₁ : Composition n₁
i₁ : Fin (length c₁)
c₂ : Composition n₁
i₂ : Fin (length c₂)
hc : c₁.blocks = c₂.blocks
hi : ↑i₁ = ↑i₂
⊢ blocksFun c₁ i₁ = blocksFun c₂ i₂
rw [← Composition.ext_iff] at hc
case refl.refl
n : ℕ
c : Composition n
n₁ : ℕ
c₁ : Composition n₁
i₁ i₂ : Fin (length c₁)
hi : ↑i₁ = ↑i₂
⊢ blocksFun c₁ i₁ = blocksFun c₁ i₂
case refl
n : ℕ
c : Composition n
n₁ : ℕ
c₁ : Composition n₁
i₁ : Fin (length c₁)
c₂ : Composition n₁
i₂ : Fin (length c₂)
hc : c₁ = c₂
hi : ↑i₁ = ↑i₂
⊢ blocksFun c₁ i₁ = blocksFun c₂ i₂
cases hc
case refl.refl.e_a
n : ℕ
c : Composition n
n₁ : ℕ
c₁ : Composition n₁
i₁ i₂ : Fin (length c₁)
hi : ↑i₁ = ↑i₂
⊢ i₁ = i₂
case refl.refl
n : ℕ
c : Composition n
n₁ : ℕ
c₁ : Composition n₁
i₁ i₂ : Fin (length c₁)
hi : ↑i₁ = ↑i₂
⊢ blocksFun c₁ i₁ = blocksFun c₁ i₂
congr
no goals
case refl.refl.e_a
n : ℕ
c : Composition n
n₁ : ℕ
c₁ : Composition n₁
i₁ i₂ : Fin (length c₁)
hi : ↑i₁ = ↑i₂
⊢ i₁ = i₂
rwa [Fin.ext_iff]