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 ι
d : ι → R
t : R
x : Matrix ι ι R
i j : ↥b.support
⊢ fromBlocks 0 0 0 (t • x) (Sum.inl i) (Sum.inl j) = ((RingHom.id R) t • fromBlocks 0 0 0 x) (Sum.inl i) (Sum.inl j)

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 ι
d : ι → R
t : R
x : Matrix ι ι R
i : ↥b.support
j : ι
⊢ fromBlocks 0 0 0 (t • x) (Sum.inl i) (Sum.inr j) = ((RingHom.id R) t • fromBlocks 0 0 0 x) (Sum.inl i) (Sum.inr j)

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 ι
d : ι → R
t : R
x : Matrix ι ι R
i : ι
j : ↥b.support
⊢ fromBlocks 0 0 0 (t • x) (Sum.inr i) (Sum.inl j) = ((RingHom.id R) t • fromBlocks 0 0 0 x) (Sum.inr i) (Sum.inl j)

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 ι
d : ι → R
t : R
x : Matrix ι ι R
i j : ι
⊢ fromBlocks 0 0 0 (t • x) (Sum.inr i) (Sum.inr j) = ((RingHom.id R) t • fromBlocks 0 0 0 x) (Sum.inr i) (Sum.inr j)

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 ι
d : ι → R
t : R
x : Matrix ι ι R
i j : ↥b.support
⊢ fromBlocks 0 0 0 (t • x) (Sum.inl i) (Sum.inl j) = ((RingHom.id R) t • fromBlocks 0 0 0 x) (Sum.inl i) (Sum.inl j)

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 ι
d : ι → R
t : R
x : Matrix ι ι R
i : ↥b.support
j : ι
⊢ fromBlocks 0 0 0 (t • x) (Sum.inl i) (Sum.inr j) = ((RingHom.id R) t • fromBlocks 0 0 0 x) (Sum.inl i) (Sum.inr j)

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 ι
d : ι → R
t : R
x : Matrix ι ι R
i : ι
j : ↥b.support
⊢ fromBlocks 0 0 0 (t • x) (Sum.inr i) (Sum.inl j) = ((RingHom.id R) t • fromBlocks 0 0 0 x) (Sum.inr i) (Sum.inl j)

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 ι
d : ι → R
t : R
x : Matrix ι ι R
i j : ι
⊢ fromBlocks 0 0 0 (t • x) (Sum.inr i) (Sum.inr j) = ((RingHom.id R) t • fromBlocks 0 0 0 x) (Sum.inr i) (Sum.inr j)