Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

Goal state before:
pp: case inl.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : DecidableEq ι
i j k : ↥b.support
⊢ h i (Sum.inl j) (Sum.inl k) =
    Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun x ↦ ↑(P.pairingIn ℤ x ↑i)) (Sum.inl j) (Sum.inl k)

pp: case inl.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : DecidableEq ι
i j : ↥b.support
k : ι
⊢ h i (Sum.inl j) (Sum.inr k) =
    Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun x ↦ ↑(P.pairingIn ℤ x ↑i)) (Sum.inl j) (Sum.inr k)

pp: case inr.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : DecidableEq ι
i : ↥b.support
j : ι
k : ↥b.support
⊢ h i (Sum.inr j) (Sum.inl k) =
    Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun x ↦ ↑(P.pairingIn ℤ x ↑i)) (Sum.inr j) (Sum.inl k)

pp: case inr.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : DecidableEq ι
i : ↥b.support
j k : ι
⊢ h i (Sum.inr j) (Sum.inr k) =
    Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun x ↦ ↑(P.pairingIn ℤ x ↑i)) (Sum.inr j) (Sum.inr k)

Tactic:
<;>

Goal state after:
case inl.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : DecidableEq ι
i j k : ↥b.support
⊢ h i (Sum.inl j) (Sum.inl k) =
    Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun x ↦ ↑(P.pairingIn ℤ x ↑i)) (Sum.inl j) (Sum.inl k)

case inl.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : DecidableEq ι
i j : ↥b.support
k : ι
⊢ h i (Sum.inl j) (Sum.inr k) =
    Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun x ↦ ↑(P.pairingIn ℤ x ↑i)) (Sum.inl j) (Sum.inr k)

case inr.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : DecidableEq ι
i : ↥b.support
j : ι
k : ↥b.support
⊢ h i (Sum.inr j) (Sum.inl k) =
    Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun x ↦ ↑(P.pairingIn ℤ x ↑i)) (Sum.inr j) (Sum.inl k)

case inr.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : DecidableEq ι
i : ↥b.support
j k : ι
⊢ h i (Sum.inr j) (Sum.inr k) =
    Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun x ↦ ↑(P.pairingIn ℤ x ↑i)) (Sum.inr j) (Sum.inr k)