mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
α : Type u_12
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : n
val✝ : l
⊢ (x • fromBlocks A B C D) (Sum.inl val✝¹) (Sum.inl val✝) =
    fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inl val✝¹) (Sum.inl val✝)

pp: case inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
α : Type u_12
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : n
val✝ : m
⊢ (x • fromBlocks A B C D) (Sum.inl val✝¹) (Sum.inr val✝) =
    fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inl val✝¹) (Sum.inr val✝)

pp: case inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
α : Type u_12
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : o
val✝ : l
⊢ (x • fromBlocks A B C D) (Sum.inr val✝¹) (Sum.inl val✝) =
    fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inr val✝¹) (Sum.inl val✝)

pp: case inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
α : Type u_12
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : o
val✝ : m
⊢ (x • fromBlocks A B C D) (Sum.inr val✝¹) (Sum.inr val✝) =
    fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inr val✝¹) (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
α : Type u_12
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : n
val✝ : l
⊢ (x • fromBlocks A B C D) (Sum.inl val✝¹) (Sum.inl val✝) =
    fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inl val✝¹) (Sum.inl val✝)

case inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
α : Type u_12
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : n
val✝ : m
⊢ (x • fromBlocks A B C D) (Sum.inl val✝¹) (Sum.inr val✝) =
    fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inl val✝¹) (Sum.inr val✝)

case inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
α : Type u_12
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : o
val✝ : l
⊢ (x • fromBlocks A B C D) (Sum.inr val✝¹) (Sum.inl val✝) =
    fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inr val✝¹) (Sum.inl val✝)

case inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
α : Type u_12
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : o
val✝ : m
⊢ (x • fromBlocks A B C D) (Sum.inr val✝¹) (Sum.inr val✝) =
    fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inr val✝¹) (Sum.inr val✝)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
inst✝ : Neg R
A : Matrix n l R
B : Matrix n m R
C : Matrix o l R
D : Matrix o m R
j : l ⊕ m
val✝ : n
⊢ (-fromBlocks A B C D) (Sum.inl val✝) j = fromBlocks (-A) (-B) (-C) (-D) (Sum.inl val✝) j

pp: case inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
inst✝ : Neg R
A : Matrix n l R
B : Matrix n m R
C : Matrix o l R
D : Matrix o m R
j : l ⊕ m
val✝ : o
⊢ (-fromBlocks A B C D) (Sum.inr val✝) j = fromBlocks (-A) (-B) (-C) (-D) (Sum.inr val✝) j

Tactic:
<;>

Goal state after:
case inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
inst✝ : Neg R
A : Matrix n l R
B : Matrix n m R
C : Matrix o l R
D : Matrix o m R
j : l ⊕ m
val✝ : n
⊢ (-fromBlocks A B C D) (Sum.inl val✝) j = fromBlocks (-A) (-B) (-C) (-D) (Sum.inl val✝) j

case inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
inst✝ : Neg R
A : Matrix n l R
B : Matrix n m R
C : Matrix o l R
D : Matrix o m R
j : l ⊕ m
val✝ : o
⊢ (-fromBlocks A B C D) (Sum.inr val✝) j = fromBlocks (-A) (-B) (-C) (-D) (Sum.inr val✝) j
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
inst✝ : Neg R
A : Matrix n l R
B : Matrix n m R
C : Matrix o l R
D : Matrix o m R
val✝¹ : n
val✝ : l
⊢ (-fromBlocks A B C D) (Sum.inl val✝¹) (Sum.inl val✝) = fromBlocks (-A) (-B) (-C) (-D) (Sum.inl val✝¹) (Sum.inl val✝)

pp: case inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
inst✝ : Neg R
A : Matrix n l R
B : Matrix n m R
C : Matrix o l R
D : Matrix o m R
val✝¹ : n
val✝ : m
⊢ (-fromBlocks A B C D) (Sum.inl val✝¹) (Sum.inr val✝) = fromBlocks (-A) (-B) (-C) (-D) (Sum.inl val✝¹) (Sum.inr val✝)

pp: case inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
inst✝ : Neg R
A : Matrix n l R
B : Matrix n m R
C : Matrix o l R
D : Matrix o m R
val✝¹ : o
val✝ : l
⊢ (-fromBlocks A B C D) (Sum.inr val✝¹) (Sum.inl val✝) = fromBlocks (-A) (-B) (-C) (-D) (Sum.inr val✝¹) (Sum.inl val✝)

pp: case inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
inst✝ : Neg R
A : Matrix n l R
B : Matrix n m R
C : Matrix o l R
D : Matrix o m R
val✝¹ : o
val✝ : m
⊢ (-fromBlocks A B C D) (Sum.inr val✝¹) (Sum.inr val✝) = fromBlocks (-A) (-B) (-C) (-D) (Sum.inr val✝¹) (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
inst✝ : Neg R
A : Matrix n l R
B : Matrix n m R
C : Matrix o l R
D : Matrix o m R
val✝¹ : n
val✝ : l
⊢ (-fromBlocks A B C D) (Sum.inl val✝¹) (Sum.inl val✝) = fromBlocks (-A) (-B) (-C) (-D) (Sum.inl val✝¹) (Sum.inl val✝)

case inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
inst✝ : Neg R
A : Matrix n l R
B : Matrix n m R
C : Matrix o l R
D : Matrix o m R
val✝¹ : n
val✝ : m
⊢ (-fromBlocks A B C D) (Sum.inl val✝¹) (Sum.inr val✝) = fromBlocks (-A) (-B) (-C) (-D) (Sum.inl val✝¹) (Sum.inr val✝)

case inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
inst✝ : Neg R
A : Matrix n l R
B : Matrix n m R
C : Matrix o l R
D : Matrix o m R
val✝¹ : o
val✝ : l
⊢ (-fromBlocks A B C D) (Sum.inr val✝¹) (Sum.inl val✝) = fromBlocks (-A) (-B) (-C) (-D) (Sum.inr val✝¹) (Sum.inl val✝)

case inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
inst✝ : Neg R
A : Matrix n l R
B : Matrix n m R
C : Matrix o l R
D : Matrix o m R
val✝¹ : o
val✝ : m
⊢ (-fromBlocks A B C D) (Sum.inr val✝¹) (Sum.inr val✝) = fromBlocks (-A) (-B) (-C) (-D) (Sum.inr val✝¹) (Sum.inr val✝)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Zero α
j : l ⊕ m
val✝ : n
⊢ fromBlocks 0 0 0 0 (Sum.inl val✝) j = 0 (Sum.inl val✝) j

pp: case inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Zero α
j : l ⊕ m
val✝ : o
⊢ fromBlocks 0 0 0 0 (Sum.inr val✝) j = 0 (Sum.inr val✝) j

Tactic:
<;>

Goal state after:
case inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Zero α
j : l ⊕ m
val✝ : n
⊢ fromBlocks 0 0 0 0 (Sum.inl val✝) j = 0 (Sum.inl val✝) j

case inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Zero α
j : l ⊕ m
val✝ : o
⊢ fromBlocks 0 0 0 0 (Sum.inr val✝) j = 0 (Sum.inr val✝) j
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Zero α
val✝¹ : n
val✝ : l
⊢ fromBlocks 0 0 0 0 (Sum.inl val✝¹) (Sum.inl val✝) = 0 (Sum.inl val✝¹) (Sum.inl val✝)

pp: case inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Zero α
val✝¹ : n
val✝ : m
⊢ fromBlocks 0 0 0 0 (Sum.inl val✝¹) (Sum.inr val✝) = 0 (Sum.inl val✝¹) (Sum.inr val✝)

pp: case inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Zero α
val✝¹ : o
val✝ : l
⊢ fromBlocks 0 0 0 0 (Sum.inr val✝¹) (Sum.inl val✝) = 0 (Sum.inr val✝¹) (Sum.inl val✝)

pp: case inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Zero α
val✝¹ : o
val✝ : m
⊢ fromBlocks 0 0 0 0 (Sum.inr val✝¹) (Sum.inr val✝) = 0 (Sum.inr val✝¹) (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Zero α
val✝¹ : n
val✝ : l
⊢ fromBlocks 0 0 0 0 (Sum.inl val✝¹) (Sum.inl val✝) = 0 (Sum.inl val✝¹) (Sum.inl val✝)

case inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Zero α
val✝¹ : n
val✝ : m
⊢ fromBlocks 0 0 0 0 (Sum.inl val✝¹) (Sum.inr val✝) = 0 (Sum.inl val✝¹) (Sum.inr val✝)

case inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Zero α
val✝¹ : o
val✝ : l
⊢ fromBlocks 0 0 0 0 (Sum.inr val✝¹) (Sum.inl val✝) = 0 (Sum.inr val✝¹) (Sum.inl val✝)

case inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Zero α
val✝¹ : o
val✝ : m
⊢ fromBlocks 0 0 0 0 (Sum.inr val✝¹) (Sum.inr val✝) = 0 (Sum.inr val✝¹) (Sum.inr val✝)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Add α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix n l α
B' : Matrix n m α
C' : Matrix o l α
D' : Matrix o m α
j : l ⊕ m
val✝ : n
⊢ (fromBlocks A B C D + fromBlocks A' B' C' D') (Sum.inl val✝) j =
    fromBlocks (A + A') (B + B') (C + C') (D + D') (Sum.inl val✝) j

pp: case inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Add α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix n l α
B' : Matrix n m α
C' : Matrix o l α
D' : Matrix o m α
j : l ⊕ m
val✝ : o
⊢ (fromBlocks A B C D + fromBlocks A' B' C' D') (Sum.inr val✝) j =
    fromBlocks (A + A') (B + B') (C + C') (D + D') (Sum.inr val✝) j

Tactic:
<;>

Goal state after:
case inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Add α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix n l α
B' : Matrix n m α
C' : Matrix o l α
D' : Matrix o m α
j : l ⊕ m
val✝ : n
⊢ (fromBlocks A B C D + fromBlocks A' B' C' D') (Sum.inl val✝) j =
    fromBlocks (A + A') (B + B') (C + C') (D + D') (Sum.inl val✝) j

case inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Add α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix n l α
B' : Matrix n m α
C' : Matrix o l α
D' : Matrix o m α
j : l ⊕ m
val✝ : o
⊢ (fromBlocks A B C D + fromBlocks A' B' C' D') (Sum.inr val✝) j =
    fromBlocks (A + A') (B + B') (C + C') (D + D') (Sum.inr val✝) j
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
α : Type u_12
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix l p α
B' : Matrix l q α
C' : Matrix m p α
D' : Matrix m q α
j : p ⊕ q
val✝ : n
⊢ (fromBlocks A B C D * fromBlocks A' B' C' D') (Sum.inl val✝) j =
    fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D') (Sum.inl val✝) j

pp: case inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
α : Type u_12
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix l p α
B' : Matrix l q α
C' : Matrix m p α
D' : Matrix m q α
j : p ⊕ q
val✝ : o
⊢ (fromBlocks A B C D * fromBlocks A' B' C' D') (Sum.inr val✝) j =
    fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D') (Sum.inr val✝) j

Tactic:
<;>

Goal state after:
case inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
α : Type u_12
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix l p α
B' : Matrix l q α
C' : Matrix m p α
D' : Matrix m q α
j : p ⊕ q
val✝ : n
⊢ (fromBlocks A B C D * fromBlocks A' B' C' D') (Sum.inl val✝) j =
    fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D') (Sum.inl val✝) j

case inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
α : Type u_12
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix l p α
B' : Matrix l q α
C' : Matrix m p α
D' : Matrix m q α
j : p ⊕ q
val✝ : o
⊢ (fromBlocks A B C D * fromBlocks A' B' C' D') (Sum.inr val✝) j =
    fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D') (Sum.inr val✝) j
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case zero.inl.inl
m : Type u_2
n : Type u_3
α : Type u_12
inst✝⁴ : Semiring α
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
A : Matrix n n α
D : Matrix m m α
i j : n
⊢ (fromBlocks A 0 0 D ^ 0) (Sum.inl i) (Sum.inl j) = fromBlocks (A ^ 0) 0 0 (D ^ 0) (Sum.inl i) (Sum.inl j)

pp: case zero.inl.inr
m : Type u_2
n : Type u_3
α : Type u_12
inst✝⁴ : Semiring α
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
A : Matrix n n α
D : Matrix m m α
i : n
j : m
⊢ (fromBlocks A 0 0 D ^ 0) (Sum.inl i) (Sum.inr j) = fromBlocks (A ^ 0) 0 0 (D ^ 0) (Sum.inl i) (Sum.inr j)

pp: case zero.inr.inl
m : Type u_2
n : Type u_3
α : Type u_12
inst✝⁴ : Semiring α
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
A : Matrix n n α
D : Matrix m m α
i : m
j : n
⊢ (fromBlocks A 0 0 D ^ 0) (Sum.inr i) (Sum.inl j) = fromBlocks (A ^ 0) 0 0 (D ^ 0) (Sum.inr i) (Sum.inl j)

pp: case zero.inr.inr
m : Type u_2
n : Type u_3
α : Type u_12
inst✝⁴ : Semiring α
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
A : Matrix n n α
D : Matrix m m α
i j : m
⊢ (fromBlocks A 0 0 D ^ 0) (Sum.inr i) (Sum.inr j) = fromBlocks (A ^ 0) 0 0 (D ^ 0) (Sum.inr i) (Sum.inr j)

Tactic:
<;>

Goal state after:
case zero.inl.inl
m : Type u_2
n : Type u_3
α : Type u_12
inst✝⁴ : Semiring α
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
A : Matrix n n α
D : Matrix m m α
i j : n
⊢ (fromBlocks A 0 0 D ^ 0) (Sum.inl i) (Sum.inl j) = fromBlocks (A ^ 0) 0 0 (D ^ 0) (Sum.inl i) (Sum.inl j)

case zero.inl.inr
m : Type u_2
n : Type u_3
α : Type u_12
inst✝⁴ : Semiring α
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
A : Matrix n n α
D : Matrix m m α
i : n
j : m
⊢ (fromBlocks A 0 0 D ^ 0) (Sum.inl i) (Sum.inr j) = fromBlocks (A ^ 0) 0 0 (D ^ 0) (Sum.inl i) (Sum.inr j)

case zero.inr.inl
m : Type u_2
n : Type u_3
α : Type u_12
inst✝⁴ : Semiring α
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
A : Matrix n n α
D : Matrix m m α
i : m
j : n
⊢ (fromBlocks A 0 0 D ^ 0) (Sum.inr i) (Sum.inl j) = fromBlocks (A ^ 0) 0 0 (D ^ 0) (Sum.inr i) (Sum.inl j)

case zero.inr.inr
m : Type u_2
n : Type u_3
α : Type u_12
inst✝⁴ : Semiring α
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
A : Matrix n n α
D : Matrix m m α
i j : m
⊢ (fromBlocks A 0 0 D ^ 0) (Sum.inr i) (Sum.inr j) = fromBlocks (A ^ 0) 0 0 (D ^ 0) (Sum.inr i) (Sum.inr j)
Module: Mathlib.LinearAlgebra.Basis.SMul

Goal state before:
pp: case pos
ι : Type u_1
R₂ : Type u_3
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : CommSemiring R₂
inst✝ : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i j : ι
h : j = i
⊢ ↑(w j)⁻¹ • 1 = ↑(w i)⁻¹ • 1

pp: case neg
ι : Type u_1
R₂ : Type u_3
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : CommSemiring R₂
inst✝ : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i j : ι
h : ¬j = i
⊢ ↑(w j)⁻¹ • 0 = ↑(w i)⁻¹ • 0

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
R₂ : Type u_3
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : CommSemiring R₂
inst✝ : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i j : ι
h : j = i
⊢ ↑(w j)⁻¹ • 1 = ↑(w i)⁻¹ • 1

case neg
ι : Type u_1
R₂ : Type u_3
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : CommSemiring R₂
inst✝ : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i j : ι
h : ¬j = i
⊢ ↑(w j)⁻¹ • 0 = ↑(w i)⁻¹ • 0
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : l ⊕ m → α
val✝ : n
⊢ (fromBlocks A B C D *ᵥ x) (Sum.inl val✝) =
    Sum.elim (A *ᵥ x ∘ Sum.inl + B *ᵥ x ∘ Sum.inr) (C *ᵥ x ∘ Sum.inl + D *ᵥ x ∘ Sum.inr) (Sum.inl val✝)

pp: case inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : l ⊕ m → α
val✝ : o
⊢ (fromBlocks A B C D *ᵥ x) (Sum.inr val✝) =
    Sum.elim (A *ᵥ x ∘ Sum.inl + B *ᵥ x ∘ Sum.inr) (C *ᵥ x ∘ Sum.inl + D *ᵥ x ∘ Sum.inr) (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : l ⊕ m → α
val✝ : n
⊢ (fromBlocks A B C D *ᵥ x) (Sum.inl val✝) =
    Sum.elim (A *ᵥ x ∘ Sum.inl + B *ᵥ x ∘ Sum.inr) (C *ᵥ x ∘ Sum.inl + D *ᵥ x ∘ Sum.inr) (Sum.inl val✝)

case inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : l ⊕ m → α
val✝ : o
⊢ (fromBlocks A B C D *ᵥ x) (Sum.inr val✝) =
    Sum.elim (A *ᵥ x ∘ Sum.inl + B *ᵥ x ∘ Sum.inr) (C *ᵥ x ∘ Sum.inl + D *ᵥ x ∘ Sum.inr) (Sum.inr val✝)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : n ⊕ o → α
val✝ : l
⊢ (x ᵥ* fromBlocks A B C D) (Sum.inl val✝) =
    Sum.elim (x ∘ Sum.inl ᵥ* A + x ∘ Sum.inr ᵥ* C) (x ∘ Sum.inl ᵥ* B + x ∘ Sum.inr ᵥ* D) (Sum.inl val✝)

pp: case inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : n ⊕ o → α
val✝ : m
⊢ (x ᵥ* fromBlocks A B C D) (Sum.inr val✝) =
    Sum.elim (x ∘ Sum.inl ᵥ* A + x ∘ Sum.inr ᵥ* C) (x ∘ Sum.inl ᵥ* B + x ∘ Sum.inr ᵥ* D) (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : n ⊕ o → α
val✝ : l
⊢ (x ᵥ* fromBlocks A B C D) (Sum.inl val✝) =
    Sum.elim (x ∘ Sum.inl ᵥ* A + x ∘ Sum.inr ᵥ* C) (x ∘ Sum.inl ᵥ* B + x ∘ Sum.inr ᵥ* D) (Sum.inl val✝)

case inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : n ⊕ o → α
val✝ : m
⊢ (x ᵥ* fromBlocks A B C D) (Sum.inr val✝) =
    Sum.elim (x ∘ Sum.inl ᵥ* A + x ∘ Sum.inr ᵥ* C) (x ∘ Sum.inl ᵥ* B + x ∘ Sum.inr ᵥ* D) (Sum.inr val✝)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
j : l ⊕ m
val✝ : l
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inl val✝) j = diagonal (Sum.elim d₁ d₂) (Sum.inl val✝) j

pp: case inr
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
j : l ⊕ m
val✝ : m
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inr val✝) j = diagonal (Sum.elim d₁ d₂) (Sum.inr val✝) j

Tactic:
<;>

Goal state after:
case inl
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
j : l ⊕ m
val✝ : l
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inl val✝) j = diagonal (Sum.elim d₁ d₂) (Sum.inl val✝) j

case inr
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
j : l ⊕ m
val✝ : m
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inr val✝) j = diagonal (Sum.elim d₁ d₂) (Sum.inr val✝) j
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl.inl
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
val✝¹ val✝ : l
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inl val✝¹) (Sum.inl val✝) =
    diagonal (Sum.elim d₁ d₂) (Sum.inl val✝¹) (Sum.inl val✝)

pp: case inl.inr
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
val✝¹ : l
val✝ : m
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inl val✝¹) (Sum.inr val✝) =
    diagonal (Sum.elim d₁ d₂) (Sum.inl val✝¹) (Sum.inr val✝)

pp: case inr.inl
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
val✝¹ : m
val✝ : l
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inr val✝¹) (Sum.inl val✝) =
    diagonal (Sum.elim d₁ d₂) (Sum.inr val✝¹) (Sum.inl val✝)

pp: case inr.inr
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
val✝¹ val✝ : m
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inr val✝¹) (Sum.inr val✝) =
    diagonal (Sum.elim d₁ d₂) (Sum.inr val✝¹) (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl.inl
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
val✝¹ val✝ : l
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inl val✝¹) (Sum.inl val✝) =
    diagonal (Sum.elim d₁ d₂) (Sum.inl val✝¹) (Sum.inl val✝)

case inl.inr
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
val✝¹ : l
val✝ : m
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inl val✝¹) (Sum.inr val✝) =
    diagonal (Sum.elim d₁ d₂) (Sum.inl val✝¹) (Sum.inr val✝)

case inr.inl
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
val✝¹ : m
val✝ : l
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inr val✝¹) (Sum.inl val✝) =
    diagonal (Sum.elim d₁ d₂) (Sum.inr val✝¹) (Sum.inl val✝)

case inr.inr
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
val✝¹ val✝ : m
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inr val✝¹) (Sum.inr val✝) =
    diagonal (Sum.elim d₁ d₂) (Sum.inr val✝¹) (Sum.inr val✝)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl
l : Type u_1
m : Type u_2
α : Type u_12
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
j : l ⊕ m
val✝ : l
⊢ fromBlocks 1 0 0 1 (Sum.inl val✝) j = 1 (Sum.inl val✝) j

pp: case inr
l : Type u_1
m : Type u_2
α : Type u_12
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
j : l ⊕ m
val✝ : m
⊢ fromBlocks 1 0 0 1 (Sum.inr val✝) j = 1 (Sum.inr val✝) j

Tactic:
<;>

Goal state after:
case inl
l : Type u_1
m : Type u_2
α : Type u_12
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
j : l ⊕ m
val✝ : l
⊢ fromBlocks 1 0 0 1 (Sum.inl val✝) j = 1 (Sum.inl val✝) j

case inr
l : Type u_1
m : Type u_2
α : Type u_12
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Zero α
inst✝ : One α
j : l ⊕ m
val✝ : m
⊢ fromBlocks 1 0 0 1 (Sum.inr val✝) j = 1 (Sum.inr val✝) j