-- Mathlib/Data/Matrix/Composition.lean
theorem comp_stdBasisMatrix_stdBasisMatrix
    [DecidableEq I] [DecidableEq J] [DecidableEq K] [DecidableEq L] [Zero R] (i j k l r) :
    comp I J K L R (stdBasisMatrix i j (stdBasisMatrix k l r))
      = stdBasisMatrix (i, k) (j, l) r

Proof state:
case a.mk.mk.inr.inr
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
k' : K
l' : L
⊢ stdBasisMatrix i j (stdBasisMatrix k l r) i j k' l' = stdBasisMatrix (i, k) (j, l) r (i, k') (j, l')

Tactic:
rw [StdBasisMatrix.apply_same]

Result:
case a.mk.mk.inr.inr
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
k' : K
l' : L
⊢ stdBasisMatrix k l r k' l' = stdBasisMatrix (i, k) (j, l) r (i, k') (j, l')

Proof state:
case a.mk.mk.inr.inr.inr.inl
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
l' : L
hj : l ≠ l'
⊢ stdBasisMatrix k l r k l' = stdBasisMatrix (i, k) (j, l) r (i, k) (j, l')

Tactic:
rw [StdBasisMatrix.apply_of_col_ne _ _ hj,
  StdBasisMatrix.apply_of_col_ne _ _ (ne_of_apply_ne Prod.snd hj)]

Result:
no goals

Proof state:
case a.mk.mk
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
i' : I
k' : K
j' : J
l' : L
⊢ (comp I J K L R) (stdBasisMatrix i j (stdBasisMatrix k l r)) (i', k') (j', l') =
    stdBasisMatrix (i, k) (j, l) r (i', k') (j', l')

Tactic:
dsimp [comp_apply]

Result:
case a.mk.mk
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
i' : I
k' : K
j' : J
l' : L
⊢ stdBasisMatrix i j (stdBasisMatrix k l r) i' j' k' l' = stdBasisMatrix (i, k) (j, l) r (i', k') (j', l')

Proof state:
case a.mk.mk.inr.inr.inr.inr
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
⊢ stdBasisMatrix k l r k l = stdBasisMatrix (i, k) (j, l) r (i, k) (j, l)

Tactic:
rw [StdBasisMatrix.apply_same, StdBasisMatrix.apply_same]

Result:
no goals

Proof state:
case a.mk.mk
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
i' : I
k' : K
j' : J
l' : L
⊢ stdBasisMatrix i j (stdBasisMatrix k l r) i' j' k' l' = stdBasisMatrix (i, k) (j, l) r (i', k') (j', l')

Tactic:
obtain hi | rfl := ne_or_eq i i'

Result:
case a.mk.mk.inl
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
i' : I
k' : K
j' : J
l' : L
hi : i ≠ i'
⊢ stdBasisMatrix i j (stdBasisMatrix k l r) i' j' k' l' = stdBasisMatrix (i, k) (j, l) r (i', k') (j', l')

case a.mk.mk.inr
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
k' : K
j' : J
l' : L
⊢ stdBasisMatrix i j (stdBasisMatrix k l r) i j' k' l' = stdBasisMatrix (i, k) (j, l) r (i, k') (j', l')

Proof state:
case a.mk.mk.inr.inr.inl
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
k' : K
l' : L
hk : k ≠ k'
⊢ stdBasisMatrix k l r k' l' = stdBasisMatrix (i, k) (j, l) r (i, k') (j, l')

Tactic:
rw [StdBasisMatrix.apply_of_row_ne hk,
  StdBasisMatrix.apply_of_row_ne (ne_of_apply_ne Prod.snd hk)]

Result:
no goals

Proof state:
case a.mk.mk.inr.inl
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
k' : K
j' : J
l' : L
hj : j ≠ j'
⊢ stdBasisMatrix i j (stdBasisMatrix k l r) i j' k' l' = stdBasisMatrix (i, k) (j, l) r (i, k') (j', l')

Tactic:
rw [StdBasisMatrix.apply_of_col_ne _ _ hj,
  StdBasisMatrix.apply_of_col_ne _ _ (ne_of_apply_ne Prod.fst hj), Matrix.zero_apply]

Result:
no goals

Proof state:
case a.mk.mk.inr.inr
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
k' : K
l' : L
⊢ stdBasisMatrix k l r k' l' = stdBasisMatrix (i, k) (j, l) r (i, k') (j, l')

Tactic:
obtain hk | rfl := ne_or_eq k k'

Result:
case a.mk.mk.inr.inr.inl
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
k' : K
l' : L
hk : k ≠ k'
⊢ stdBasisMatrix k l r k' l' = stdBasisMatrix (i, k) (j, l) r (i, k') (j, l')

case a.mk.mk.inr.inr.inr
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
l' : L
⊢ stdBasisMatrix k l r k l' = stdBasisMatrix (i, k) (j, l) r (i, k) (j, l')

Proof state:
case a.mk.mk.inr.inr.inr
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
l' : L
⊢ stdBasisMatrix k l r k l' = stdBasisMatrix (i, k) (j, l) r (i, k) (j, l')

Tactic:
obtain hj | rfl := ne_or_eq l l'

Result:
case a.mk.mk.inr.inr.inr.inl
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
l' : L
hj : l ≠ l'
⊢ stdBasisMatrix k l r k l' = stdBasisMatrix (i, k) (j, l) r (i, k) (j, l')

case a.mk.mk.inr.inr.inr.inr
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
⊢ stdBasisMatrix k l r k l = stdBasisMatrix (i, k) (j, l) r (i, k) (j, l)

Proof state:
case a.mk.mk.inl
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
i' : I
k' : K
j' : J
l' : L
hi : i ≠ i'
⊢ stdBasisMatrix i j (stdBasisMatrix k l r) i' j' k' l' = stdBasisMatrix (i, k) (j, l) r (i', k') (j', l')

Tactic:
rw [StdBasisMatrix.apply_of_row_ne hi,
  StdBasisMatrix.apply_of_row_ne (ne_of_apply_ne Prod.fst hi), Matrix.zero_apply]

Result:
no goals