Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: case inl.inl.inl.inl
l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inl PUnit.unit)) =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm) (fromBlocks 1 0 0 (indefiniteDiagonal l l R))
      (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inl PUnit.unit))

pp: case inl.inl.inl.inr
l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
j₃ : l
⊢ indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inr j₃)) =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm) (fromBlocks 1 0 0 (indefiniteDiagonal l l R))
      (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inr j₃))

pp: case inl.inl.inr
l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
val✝ : l
⊢ indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inl PUnit.unit)) (Sum.inr val✝) =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm) (fromBlocks 1 0 0 (indefiniteDiagonal l l R))
      (Sum.inl (Sum.inl PUnit.unit)) (Sum.inr val✝)

pp: case inl.inr.inl.inl
l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
i₃ : l
⊢ indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inr i₃)) (Sum.inl (Sum.inl PUnit.unit)) =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm) (fromBlocks 1 0 0 (indefiniteDiagonal l l R))
      (Sum.inl (Sum.inr i₃)) (Sum.inl (Sum.inl PUnit.unit))

pp: case inl.inr.inl.inr
l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
i₃ j₃ : l
⊢ indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inr i₃)) (Sum.inl (Sum.inr j₃)) =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm) (fromBlocks 1 0 0 (indefiniteDiagonal l l R))
      (Sum.inl (Sum.inr i₃)) (Sum.inl (Sum.inr j₃))

pp: case inl.inr.inr
l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
i₃ val✝ : l
⊢ indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inr i₃)) (Sum.inr val✝) =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm) (fromBlocks 1 0 0 (indefiniteDiagonal l l R))
      (Sum.inl (Sum.inr i₃)) (Sum.inr val✝)

pp: case inr.inl.inl
l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
val✝ : l
⊢ indefiniteDiagonal (Unit ⊕ l) l R (Sum.inr val✝) (Sum.inl (Sum.inl PUnit.unit)) =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm) (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inr val✝)
      (Sum.inl (Sum.inl PUnit.unit))

pp: case inr.inl.inr
l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
val✝ j₃ : l
⊢ indefiniteDiagonal (Unit ⊕ l) l R (Sum.inr val✝) (Sum.inl (Sum.inr j₃)) =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm) (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inr val✝)
      (Sum.inl (Sum.inr j₃))

pp: case inr.inr
l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
val✝¹ val✝ : l
⊢ indefiniteDiagonal (Unit ⊕ l) l R (Sum.inr val✝¹) (Sum.inr val✝) =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm) (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inr val✝¹)
      (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl.inl.inl.inl
l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inl PUnit.unit)) =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm) (fromBlocks 1 0 0 (indefiniteDiagonal l l R))
      (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inl PUnit.unit))

case inl.inl.inl.inr
l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
j₃ : l
⊢ indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inr j₃)) =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm) (fromBlocks 1 0 0 (indefiniteDiagonal l l R))
      (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inr j₃))

case inl.inl.inr
l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
val✝ : l
⊢ indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inl PUnit.unit)) (Sum.inr val✝) =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm) (fromBlocks 1 0 0 (indefiniteDiagonal l l R))
      (Sum.inl (Sum.inl PUnit.unit)) (Sum.inr val✝)

case inl.inr.inl.inl
l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
i₃ : l
⊢ indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inr i₃)) (Sum.inl (Sum.inl PUnit.unit)) =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm) (fromBlocks 1 0 0 (indefiniteDiagonal l l R))
      (Sum.inl (Sum.inr i₃)) (Sum.inl (Sum.inl PUnit.unit))

case inl.inr.inl.inr
l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
i₃ j₃ : l
⊢ indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inr i₃)) (Sum.inl (Sum.inr j₃)) =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm) (fromBlocks 1 0 0 (indefiniteDiagonal l l R))
      (Sum.inl (Sum.inr i₃)) (Sum.inl (Sum.inr j₃))

case inl.inr.inr
l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
i₃ val✝ : l
⊢ indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inr i₃)) (Sum.inr val✝) =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm) (fromBlocks 1 0 0 (indefiniteDiagonal l l R))
      (Sum.inl (Sum.inr i₃)) (Sum.inr val✝)

case inr.inl.inl
l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
val✝ : l
⊢ indefiniteDiagonal (Unit ⊕ l) l R (Sum.inr val✝) (Sum.inl (Sum.inl PUnit.unit)) =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm) (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inr val✝)
      (Sum.inl (Sum.inl PUnit.unit))

case inr.inl.inr
l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
val✝ j₃ : l
⊢ indefiniteDiagonal (Unit ⊕ l) l R (Sum.inr val✝) (Sum.inl (Sum.inr j₃)) =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm) (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inr val✝)
      (Sum.inl (Sum.inr j₃))

case inr.inr
l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
val✝¹ val✝ : l
⊢ indefiniteDiagonal (Unit ⊕ l) l R (Sum.inr val✝¹) (Sum.inr val✝) =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm) (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inr val✝¹)
      (Sum.inr val✝)