case a.h
n : Type ?u.166573
p : Type ?u.166576
q : Type ?u.166579
l : Type u_1
R : Type u₂
inst✝⁷ : DecidableEq n
inst✝⁶ : DecidableEq p
inst✝⁵ : DecidableEq q
inst✝⁴ : DecidableEq l
inst✝³ : CommRing R
inst✝² : Fintype p
inst✝¹ : Fintype q
inst✝ : Fintype l
i j : (Unit ⊕ l) ⊕ l
⊢ indefiniteDiagonal (Unit ⊕ l) l R i j =
    ↑(reindexLieEquiv (Equiv.sumAssoc Unit l l).symm) (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) i j
n : Type ?u.166573
p : Type ?u.166576
q : Type ?u.166579
l : Type u_1
R : Type u₂
inst✝⁷ : DecidableEq n
inst✝⁶ : DecidableEq p
inst✝⁵ : DecidableEq q
inst✝⁴ : DecidableEq l
inst✝³ : CommRing R
inst✝² : Fintype p
inst✝¹ : Fintype q
inst✝ : Fintype l
⊢ indefiniteDiagonal (Unit ⊕ l) l R =
    ↑(reindexLieEquiv (Equiv.sumAssoc Unit l l).symm) (fromBlocks 1 0 0 (indefiniteDiagonal l l R))
ext (i j)
no goals
case a.h
n : Type ?u.166573
p : Type ?u.166576
q : Type ?u.166579
l : Type u_1
R : Type u₂
inst✝⁷ : DecidableEq n
inst✝⁶ : DecidableEq p
inst✝⁵ : DecidableEq q
inst✝⁴ : DecidableEq l
inst✝³ : CommRing R
inst✝² : Fintype p
inst✝¹ : Fintype q
inst✝ : Fintype l
i j : (Unit ⊕ l) ⊕ l
⊢ indefiniteDiagonal (Unit ⊕ l) l R i j =
    ↑(reindexLieEquiv (Equiv.sumAssoc Unit l l).symm) (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) i j
rcases i with ⟨⟨i₁ | i₂⟩ | i₃⟩ <;> rcases j with ⟨⟨j₁ | j₂⟩ | j₃⟩ <;>
  simp only [indefiniteDiagonal, Matrix.diagonal_apply, Equiv.sumAssoc_apply_inl_inl,
    Matrix.reindexLieEquiv_apply, Matrix.submatrix_apply, Equiv.symm_symm, Matrix.reindex_apply,
    Sum.elim_inl, if_true, eq_self_iff_true, Matrix.one_apply_eq, Matrix.fromBlocks_apply₁₁,
    DMatrix.zero_apply, Equiv.sumAssoc_apply_inl_inr, if_false, Matrix.fromBlocks_apply₁₂,
    Matrix.fromBlocks_apply₂₁, Matrix.fromBlocks_apply₂₂, Equiv.sumAssoc_apply_inr,
    Sum.elim_inr, Sum.inl_injective.eq_iff, Sum.inr_injective.eq_iff] <;>
  congr 1