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
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
val✝¹ : n
val✝ : l
⊢ (fromBlocks A B C D).map f (Sum.inl val✝¹) (Sum.inl val✝) =
    fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) (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
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
val✝¹ : n
val✝ : m
⊢ (fromBlocks A B C D).map f (Sum.inl val✝¹) (Sum.inr val✝) =
    fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) (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
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
val✝¹ : o
val✝ : l
⊢ (fromBlocks A B C D).map f (Sum.inr val✝¹) (Sum.inl val✝) =
    fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) (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
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
val✝¹ : o
val✝ : m
⊢ (fromBlocks A B C D).map f (Sum.inr val✝¹) (Sum.inr val✝) =
    fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) (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
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
val✝¹ : n
val✝ : l
⊢ (fromBlocks A B C D).map f (Sum.inl val✝¹) (Sum.inl val✝) =
    fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) (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
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
val✝¹ : n
val✝ : m
⊢ (fromBlocks A B C D).map f (Sum.inl val✝¹) (Sum.inr val✝) =
    fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) (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
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
val✝¹ : o
val✝ : l
⊢ (fromBlocks A B C D).map f (Sum.inr val✝¹) (Sum.inl val✝) =
    fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) (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
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
val✝¹ : o
val✝ : m
⊢ (fromBlocks A B C D).map f (Sum.inr val✝¹) (Sum.inr val✝) =
    fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) (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
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
j : n ⊕ o
val✝ : l
⊢ (fromBlocks A B C D)ᵀ (Sum.inl val✝) j = fromBlocks Aᵀ Cᵀ Bᵀ 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
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
j : n ⊕ o
val✝ : m
⊢ (fromBlocks A B C D)ᵀ (Sum.inr val✝) j = fromBlocks Aᵀ Cᵀ Bᵀ 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
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
j : n ⊕ o
val✝ : l
⊢ (fromBlocks A B C D)ᵀ (Sum.inl val✝) j = fromBlocks Aᵀ Cᵀ Bᵀ 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
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
j : n ⊕ o
val✝ : m
⊢ (fromBlocks A B C D)ᵀ (Sum.inr val✝) j = fromBlocks Aᵀ Cᵀ Bᵀ 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
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : l
val✝ : n
⊢ (fromBlocks A B C D)ᵀ (Sum.inl val✝¹) (Sum.inl val✝) = fromBlocks Aᵀ Cᵀ Bᵀ 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
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : l
val✝ : o
⊢ (fromBlocks A B C D)ᵀ (Sum.inl val✝¹) (Sum.inr val✝) = fromBlocks Aᵀ Cᵀ Bᵀ 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
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : m
val✝ : n
⊢ (fromBlocks A B C D)ᵀ (Sum.inr val✝¹) (Sum.inl val✝) = fromBlocks Aᵀ Cᵀ Bᵀ 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
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : m
val✝ : o
⊢ (fromBlocks A B C D)ᵀ (Sum.inr val✝¹) (Sum.inr val✝) = fromBlocks Aᵀ Cᵀ Bᵀ 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
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : l
val✝ : n
⊢ (fromBlocks A B C D)ᵀ (Sum.inl val✝¹) (Sum.inl val✝) = fromBlocks Aᵀ Cᵀ Bᵀ 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
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : l
val✝ : o
⊢ (fromBlocks A B C D)ᵀ (Sum.inl val✝¹) (Sum.inr val✝) = fromBlocks Aᵀ Cᵀ Bᵀ 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
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : m
val✝ : n
⊢ (fromBlocks A B C D)ᵀ (Sum.inr val✝¹) (Sum.inl val✝) = fromBlocks Aᵀ Cᵀ Bᵀ 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
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val✝¹ : m
val✝ : o
⊢ (fromBlocks A B C D)ᵀ (Sum.inr val✝¹) (Sum.inr val✝) = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ (Sum.inr val✝¹) (Sum.inr val✝)
Module: Mathlib.LinearAlgebra.Basis.Prod

Goal state before:
pp: case fst
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i : ι ⊕ ι'
⊢ ((b.prod b') i).1 = (Sum.elim (⇑(LinearMap.inl R M M') ∘ ⇑b) (⇑(LinearMap.inr R M M') ∘ ⇑b') i).1

pp: case snd
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i : ι ⊕ ι'
⊢ ((b.prod b') i).2 = (Sum.elim (⇑(LinearMap.inl R M M') ∘ ⇑b) (⇑(LinearMap.inr R M M') ∘ ⇑b') i).2

Tactic:
<;>

Goal state after:
case fst
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i : ι ⊕ ι'
⊢ ((b.prod b') i).1 = (Sum.elim (⇑(LinearMap.inl R M M') ∘ ⇑b) (⇑(LinearMap.inr R M M') ∘ ⇑b') i).1

case snd
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i : ι ⊕ ι'
⊢ ((b.prod b') i).2 = (Sum.elim (⇑(LinearMap.inl R M M') ∘ ⇑b) (⇑(LinearMap.inr R M M') ∘ ⇑b') i).2
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
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val✝ : o
⊢ (fromBlocks A B C D).submatrix Sum.swap f (Sum.inl val✝) j = (fromBlocks C D A B).submatrix id f (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
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val✝ : n
⊢ (fromBlocks A B C D).submatrix Sum.swap f (Sum.inr val✝) j = (fromBlocks C D A B).submatrix id f (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
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val✝ : o
⊢ (fromBlocks A B C D).submatrix Sum.swap f (Sum.inl val✝) j = (fromBlocks C D A B).submatrix id f (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
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val✝ : n
⊢ (fromBlocks A B C D).submatrix Sum.swap f (Sum.inr val✝) j = (fromBlocks C D A B).submatrix id f (Sum.inr val✝) j
Module: Mathlib.LinearAlgebra.Basis.Prod

Goal state before:
pp: case fst.inl
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
val✝ : ι
⊢ ((b.prod b') (Sum.inl val✝)).1 =
    (Sum.elim (⇑(LinearMap.inl R M M') ∘ ⇑b) (⇑(LinearMap.inr R M M') ∘ ⇑b') (Sum.inl val✝)).1

pp: case fst.inr
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
val✝ : ι'
⊢ ((b.prod b') (Sum.inr val✝)).1 =
    (Sum.elim (⇑(LinearMap.inl R M M') ∘ ⇑b) (⇑(LinearMap.inr R M M') ∘ ⇑b') (Sum.inr val✝)).1

pp: case snd.inl
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
val✝ : ι
⊢ ((b.prod b') (Sum.inl val✝)).2 =
    (Sum.elim (⇑(LinearMap.inl R M M') ∘ ⇑b) (⇑(LinearMap.inr R M M') ∘ ⇑b') (Sum.inl val✝)).2

pp: case snd.inr
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
val✝ : ι'
⊢ ((b.prod b') (Sum.inr val✝)).2 =
    (Sum.elim (⇑(LinearMap.inl R M M') ∘ ⇑b) (⇑(LinearMap.inr R M M') ∘ ⇑b') (Sum.inr val✝)).2

Tactic:
<;>

Goal state after:
case fst.inl
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
val✝ : ι
⊢ ((b.prod b') (Sum.inl val✝)).1 =
    (Sum.elim (⇑(LinearMap.inl R M M') ∘ ⇑b) (⇑(LinearMap.inr R M M') ∘ ⇑b') (Sum.inl val✝)).1

case fst.inr
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
val✝ : ι'
⊢ ((b.prod b') (Sum.inr val✝)).1 =
    (Sum.elim (⇑(LinearMap.inl R M M') ∘ ⇑b) (⇑(LinearMap.inr R M M') ∘ ⇑b') (Sum.inr val✝)).1

case snd.inl
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
val✝ : ι
⊢ ((b.prod b') (Sum.inl val✝)).2 =
    (Sum.elim (⇑(LinearMap.inl R M M') ∘ ⇑b) (⇑(LinearMap.inr R M M') ∘ ⇑b') (Sum.inl val✝)).2

case snd.inr
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
val✝ : ι'
⊢ ((b.prod b') (Sum.inr val✝)).2 =
    (Sum.elim (⇑(LinearMap.inl R M M') ∘ ⇑b) (⇑(LinearMap.inr R M M') ∘ ⇑b') (Sum.inr val✝)).2
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
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val✝ : o
⊢ fromBlocks A B C D (Sum.inr val✝) (f j) = fromBlocks C D A B (Sum.inl val✝) (f j)

pp: case inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val✝ : n
⊢ fromBlocks A B C D (Sum.inl val✝) (f j) = fromBlocks C D A B (Sum.inr val✝) (f 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
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val✝ : o
⊢ fromBlocks A B C D (Sum.inr val✝) (f j) = fromBlocks C D A B (Sum.inl val✝) (f j)

case inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val✝ : n
⊢ fromBlocks A B C D (Sum.inl val✝) (f j) = fromBlocks C D A B (Sum.inr val✝) (f 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
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val✝¹ : o
val✝ : l
⊢ fromBlocks A B C D (Sum.inr val✝¹) (Sum.inl val✝) = fromBlocks C D A B (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
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val✝¹ : o
val✝ : m
⊢ fromBlocks A B C D (Sum.inr val✝¹) (Sum.inr val✝) = fromBlocks C D A B (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
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val✝¹ : n
val✝ : l
⊢ fromBlocks A B C D (Sum.inl val✝¹) (Sum.inl val✝) = fromBlocks C D A B (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
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val✝¹ : n
val✝ : m
⊢ fromBlocks A B C D (Sum.inl val✝¹) (Sum.inr val✝) = fromBlocks C D A B (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
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val✝¹ : o
val✝ : l
⊢ fromBlocks A B C D (Sum.inr val✝¹) (Sum.inl val✝) = fromBlocks C D A B (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
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val✝¹ : o
val✝ : m
⊢ fromBlocks A B C D (Sum.inr val✝¹) (Sum.inr val✝) = fromBlocks C D A B (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
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val✝¹ : n
val✝ : l
⊢ fromBlocks A B C D (Sum.inl val✝¹) (Sum.inl val✝) = fromBlocks C D A B (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
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val✝¹ : n
val✝ : m
⊢ fromBlocks A B C D (Sum.inl val✝¹) (Sum.inr val✝) = fromBlocks C D A B (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
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val✝ : m
⊢ (fromBlocks A B C D).submatrix f Sum.swap i (Sum.inl val✝) = (fromBlocks B A D C).submatrix f id i (Sum.inl val✝)

pp: case inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val✝ : l
⊢ (fromBlocks A B C D).submatrix f Sum.swap i (Sum.inr val✝) = (fromBlocks B A D C).submatrix f id i (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
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val✝ : m
⊢ (fromBlocks A B C D).submatrix f Sum.swap i (Sum.inl val✝) = (fromBlocks B A D C).submatrix f id i (Sum.inl val✝)

case inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val✝ : l
⊢ (fromBlocks A B C D).submatrix f Sum.swap i (Sum.inr val✝) = (fromBlocks B A D C).submatrix f id i (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
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val✝ : m
⊢ fromBlocks A B C D (f i) (Sum.inr val✝) = fromBlocks B A D C (f i) (Sum.inl val✝)

pp: case inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val✝ : l
⊢ fromBlocks A B C D (f i) (Sum.inl val✝) = fromBlocks B A D C (f i) (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
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val✝ : m
⊢ fromBlocks A B C D (f i) (Sum.inr val✝) = fromBlocks B A D C (f i) (Sum.inl val✝)

case inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val✝ : l
⊢ fromBlocks A B C D (f i) (Sum.inl val✝) = fromBlocks B A D C (f i) (Sum.inr val✝)
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
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val✝¹ : m
val✝ : n
⊢ fromBlocks A B C D (Sum.inl val✝) (Sum.inr val✝¹) = fromBlocks B A D C (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
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val✝¹ : m
val✝ : o
⊢ fromBlocks A B C D (Sum.inr val✝) (Sum.inr val✝¹) = fromBlocks B A D C (Sum.inr val✝) (Sum.inl val✝¹)

pp: case inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val✝¹ : l
val✝ : n
⊢ fromBlocks A B C D (Sum.inl val✝) (Sum.inl val✝¹) = fromBlocks B A D C (Sum.inl val✝) (Sum.inr val✝¹)

pp: case inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val✝¹ : l
val✝ : o
⊢ fromBlocks A B C D (Sum.inr val✝) (Sum.inl val✝¹) = fromBlocks B A D C (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
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val✝¹ : m
val✝ : n
⊢ fromBlocks A B C D (Sum.inl val✝) (Sum.inr val✝¹) = fromBlocks B A D C (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
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val✝¹ : m
val✝ : o
⊢ fromBlocks A B C D (Sum.inr val✝) (Sum.inr val✝¹) = fromBlocks B A D C (Sum.inr val✝) (Sum.inl val✝¹)

case inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val✝¹ : l
val✝ : n
⊢ fromBlocks A B C D (Sum.inl val✝) (Sum.inl val✝¹) = fromBlocks B A D C (Sum.inl val✝) (Sum.inr val✝¹)

case inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val✝¹ : l
val✝ : o
⊢ fromBlocks A B C D (Sum.inr val✝) (Sum.inl val✝¹) = fromBlocks B A D C (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
α : Type u_12
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
j : l ⊕ m
val✝ : n
⊢ (x • fromBlocks A B C D) (Sum.inl val✝) j = fromBlocks (x • A) (x • B) (x • C) (x • 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
α : Type u_12
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
j : l ⊕ m
val✝ : o
⊢ (x • fromBlocks A B C D) (Sum.inr val✝) j = fromBlocks (x • A) (x • B) (x • C) (x • 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
α : Type u_12
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
j : l ⊕ m
val✝ : n
⊢ (x • fromBlocks A B C D) (Sum.inl val✝) j = fromBlocks (x • A) (x • B) (x • C) (x • 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
α : Type u_12
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
j : l ⊕ m
val✝ : o
⊢ (x • fromBlocks A B C D) (Sum.inr val✝) j = fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inr val✝) j