mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: case mp
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
a : Matrix m n A
inst✝ : Nonempty l
⊢ mulRightLinearMap l R a = 0 → a = 0

pp: case mpr
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
a : Matrix m n A
inst✝ : Nonempty l
⊢ a = 0 → mulRightLinearMap l R a = 0

Tactic:
<;>

Goal state after:
case mp
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
a : Matrix m n A
inst✝ : Nonempty l
⊢ mulRightLinearMap l R a = 0 → a = 0

case mpr
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
a : Matrix m n A
inst✝ : Nonempty l
⊢ a = 0 → mulRightLinearMap l R a = 0
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Bool
a : List α
l : List (List α)
IH :
  ¬[] ∈ l →
    (∀ (m : List α), m ∈ l → IsChain (fun x y ↦ r x y = true) m) →
      IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) l → splitBy r l.flatten = l
hn : ¬a = [] ∧ ¬[] ∈ l
hc : ∀ (m : List α), m ∈ a :: l → IsChain (fun x y ↦ r x y = true) m
hc' : IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (a :: l)
⊢ splitBy r (a :: l).flatten = a :: l

Tactic:
flatten_cons,

Goal state after:
case cons
α : Type u_1
r : α → α → Bool
a : List α
l : List (List α)
IH :
  ¬[] ∈ l →
    (∀ (m : List α), m ∈ l → IsChain (fun x y ↦ r x y = true) m) →
      IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) l → splitBy r l.flatten = l
hn : ¬a = [] ∧ ¬[] ∈ l
hc : ∀ (m : List α), m ∈ a :: l → IsChain (fun x y ↦ r x y = true) m
hc' : IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (a :: l)
⊢ splitBy r (a ++ l.flatten) = a :: l
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A : Matrix m (n₁ ⊕ n₂) R
i : m
j : n₁
⊢ A.toCols₁.fromCols A.toCols₂ i (Sum.inl j) = A i (Sum.inl j)

pp: case inr
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A : Matrix m (n₁ ⊕ n₂) R
i : m
j : n₂
⊢ A.toCols₁.fromCols A.toCols₂ i (Sum.inr j) = A i (Sum.inr j)

Tactic:
<;>

Goal state after:
case inl
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A : Matrix m (n₁ ⊕ n₂) R
i : m
j : n₁
⊢ A.toCols₁.fromCols A.toCols₂ i (Sum.inl j) = A i (Sum.inl j)

case inr
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A : Matrix m (n₁ ⊕ n₂) R
i : m
j : n₂
⊢ A.toCols₁.fromCols A.toCols₂ i (Sum.inr j) = A i (Sum.inr j)
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A : Matrix (m₁ ⊕ m₂) n R
i : m₁
j : n
⊢ A.toRows₁.fromRows A.toRows₂ (Sum.inl i) j = A (Sum.inl i) j

pp: case inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A : Matrix (m₁ ⊕ m₂) n R
i : m₂
j : n
⊢ A.toRows₁.fromRows A.toRows₂ (Sum.inr i) j = A (Sum.inr i) j

Tactic:
<;>

Goal state after:
case inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A : Matrix (m₁ ⊕ m₂) n R
i : m₁
j : n
⊢ A.toRows₁.fromRows A.toRows₂ (Sum.inl i) j = A (Sum.inl i) j

case inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A : Matrix (m₁ ⊕ m₂) n R
i : m₂
j : n
⊢ A.toRows₁.fromRows A.toRows₂ (Sum.inr i) j = A (Sum.inr i) j
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
i : n₁
j : m
⊢ (A₁.fromCols A₂)ᵀ (Sum.inl i) j = A₁ᵀ.fromRows A₂ᵀ (Sum.inl i) j

pp: case inr
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
i : n₂
j : m
⊢ (A₁.fromCols A₂)ᵀ (Sum.inr i) j = A₁ᵀ.fromRows A₂ᵀ (Sum.inr i) j

Tactic:
<;>

Goal state after:
case inl
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
i : n₁
j : m
⊢ (A₁.fromCols A₂)ᵀ (Sum.inl i) j = A₁ᵀ.fromRows A₂ᵀ (Sum.inl i) j

case inr
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
i : n₂
j : m
⊢ (A₁.fromCols A₂)ᵀ (Sum.inr i) j = A₁ᵀ.fromRows A₂ᵀ (Sum.inr i) j
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
i : n
j : m₁
⊢ (A₁.fromRows A₂)ᵀ i (Sum.inl j) = A₁ᵀ.fromCols A₂ᵀ i (Sum.inl j)

pp: case inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
i : n
j : m₂
⊢ (A₁.fromRows A₂)ᵀ i (Sum.inr j) = A₁ᵀ.fromCols A₂ᵀ i (Sum.inr j)

Tactic:
<;>

Goal state after:
case inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
i : n
j : m₁
⊢ (A₁.fromRows A₂)ᵀ i (Sum.inl j) = A₁ᵀ.fromCols A₂ᵀ i (Sum.inl j)

case inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
i : n
j : m₂
⊢ (A₁.fromRows A₂)ᵀ i (Sum.inr j) = A₁ᵀ.fromCols A₂ᵀ i (Sum.inr j)
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
R' : Type u_8
f : R → R'
val✝ : m₁
j✝ : n
⊢ (A₁.fromRows A₂).map f (Sum.inl val✝) j✝ = (A₁.map f).fromRows (A₂.map f) (Sum.inl val✝) j✝

pp: case inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
R' : Type u_8
f : R → R'
val✝ : m₂
j✝ : n
⊢ (A₁.fromRows A₂).map f (Sum.inr val✝) j✝ = (A₁.map f).fromRows (A₂.map f) (Sum.inr val✝) j✝

Tactic:
<;>

Goal state after:
case inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
R' : Type u_8
f : R → R'
val✝ : m₁
j✝ : n
⊢ (A₁.fromRows A₂).map f (Sum.inl val✝) j✝ = (A₁.map f).fromRows (A₂.map f) (Sum.inl val✝) j✝

case inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
R' : Type u_8
f : R → R'
val✝ : m₂
j✝ : n
⊢ (A₁.fromRows A₂).map f (Sum.inr val✝) j✝ = (A₁.map f).fromRows (A₂.map f) (Sum.inr val✝) j✝
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
R' : Type u_8
f : R → R'
i✝ : m
val✝ : n₁
⊢ (A₁.fromCols A₂).map f i✝ (Sum.inl val✝) = (A₁.map f).fromCols (A₂.map f) i✝ (Sum.inl val✝)

pp: case inr
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
R' : Type u_8
f : R → R'
i✝ : m
val✝ : n₂
⊢ (A₁.fromCols A₂).map f i✝ (Sum.inr val✝) = (A₁.map f).fromCols (A₂.map f) i✝ (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
R' : Type u_8
f : R → R'
i✝ : m
val✝ : n₁
⊢ (A₁.fromCols A₂).map f i✝ (Sum.inl val✝) = (A₁.map f).fromCols (A₂.map f) i✝ (Sum.inl val✝)

case inr
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
R' : Type u_8
f : R → R'
i✝ : m
val✝ : n₂
⊢ (A₁.fromCols A₂).map f i✝ (Sum.inr val✝) = (A₁.map f).fromCols (A₂.map f) i✝ (Sum.inr val✝)
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Neg R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
i : m₁
j : n
⊢ (-A₁.fromRows A₂) (Sum.inl i) j = (-A₁).fromRows (-A₂) (Sum.inl i) j

pp: case inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Neg R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
i : m₂
j : n
⊢ (-A₁.fromRows A₂) (Sum.inr i) j = (-A₁).fromRows (-A₂) (Sum.inr i) j

Tactic:
<;>

Goal state after:
case inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Neg R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
i : m₁
j : n
⊢ (-A₁.fromRows A₂) (Sum.inl i) j = (-A₁).fromRows (-A₂) (Sum.inl i) j

case inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Neg R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
i : m₂
j : n
⊢ (-A₁.fromRows A₂) (Sum.inr i) j = (-A₁).fromRows (-A₂) (Sum.inr i) j
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Neg R
A₁ : Matrix n m₁ R
A₂ : Matrix n m₂ R
i : n
j : m₁
⊢ (-A₁.fromCols A₂) i (Sum.inl j) = (-A₁).fromCols (-A₂) i (Sum.inl j)

pp: case inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Neg R
A₁ : Matrix n m₁ R
A₂ : Matrix n m₂ R
i : n
j : m₂
⊢ (-A₁.fromCols A₂) i (Sum.inr j) = (-A₁).fromCols (-A₂) i (Sum.inr j)

Tactic:
<;>

Goal state after:
case inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Neg R
A₁ : Matrix n m₁ R
A₂ : Matrix n m₂ R
i : n
j : m₁
⊢ (-A₁.fromCols A₂) i (Sum.inl j) = (-A₁).fromCols (-A₂) i (Sum.inl j)

case inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Neg R
A₁ : Matrix n m₁ R
A₂ : Matrix n m₂ R
i : n
j : m₂
⊢ (-A₁.fromCols A₂) i (Sum.inr j) = (-A₁).fromCols (-A₂) i (Sum.inr j)
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl.inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝¹ : m₁
val✝ : n₁
⊢ (B₁₁.fromRows B₂₁).fromCols (B₁₂.fromRows B₂₂) (Sum.inl val✝¹) (Sum.inl val✝) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inl val✝¹) (Sum.inl val✝)

pp: case inl.inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝¹ : m₁
val✝ : n₂
⊢ (B₁₁.fromRows B₂₁).fromCols (B₁₂.fromRows B₂₂) (Sum.inl val✝¹) (Sum.inr val✝) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inl val✝¹) (Sum.inr val✝)

pp: case inr.inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝¹ : m₂
val✝ : n₁
⊢ (B₁₁.fromRows B₂₁).fromCols (B₁₂.fromRows B₂₂) (Sum.inr val✝¹) (Sum.inl val✝) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inr val✝¹) (Sum.inl val✝)

pp: case inr.inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝¹ : m₂
val✝ : n₂
⊢ (B₁₁.fromRows B₂₁).fromCols (B₁₂.fromRows B₂₂) (Sum.inr val✝¹) (Sum.inr val✝) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inr val✝¹) (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl.inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝¹ : m₁
val✝ : n₁
⊢ (B₁₁.fromRows B₂₁).fromCols (B₁₂.fromRows B₂₂) (Sum.inl val✝¹) (Sum.inl val✝) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inl val✝¹) (Sum.inl val✝)

case inl.inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝¹ : m₁
val✝ : n₂
⊢ (B₁₁.fromRows B₂₁).fromCols (B₁₂.fromRows B₂₂) (Sum.inl val✝¹) (Sum.inr val✝) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inl val✝¹) (Sum.inr val✝)

case inr.inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝¹ : m₂
val✝ : n₁
⊢ (B₁₁.fromRows B₂₁).fromCols (B₁₂.fromRows B₂₂) (Sum.inr val✝¹) (Sum.inl val✝) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inr val✝¹) (Sum.inl val✝)

case inr.inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝¹ : m₂
val✝ : n₂
⊢ (B₁₁.fromRows B₂₁).fromCols (B₁₂.fromRows B₂₂) (Sum.inr val✝¹) (Sum.inr val✝) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inr val✝¹) (Sum.inr val✝)
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl.inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝¹ : m₁
val✝ : n₁
⊢ (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) (Sum.inl val✝¹) (Sum.inl val✝) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inl val✝¹) (Sum.inl val✝)

pp: case inl.inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝¹ : m₁
val✝ : n₂
⊢ (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) (Sum.inl val✝¹) (Sum.inr val✝) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inl val✝¹) (Sum.inr val✝)

pp: case inr.inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝¹ : m₂
val✝ : n₁
⊢ (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) (Sum.inr val✝¹) (Sum.inl val✝) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inr val✝¹) (Sum.inl val✝)

pp: case inr.inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝¹ : m₂
val✝ : n₂
⊢ (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) (Sum.inr val✝¹) (Sum.inr val✝) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inr val✝¹) (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl.inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝¹ : m₁
val✝ : n₁
⊢ (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) (Sum.inl val✝¹) (Sum.inl val✝) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inl val✝¹) (Sum.inl val✝)

case inl.inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝¹ : m₁
val✝ : n₂
⊢ (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) (Sum.inl val✝¹) (Sum.inr val✝) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inl val✝¹) (Sum.inr val✝)

case inr.inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝¹ : m₂
val✝ : n₁
⊢ (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) (Sum.inr val✝¹) (Sum.inl val✝) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inr val✝¹) (Sum.inl val✝)

case inr.inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝¹ : m₂
val✝ : n₂
⊢ (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) (Sum.inr val✝¹) (Sum.inr val✝) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inr val✝¹) (Sum.inr val✝)
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝¹ : Semiring R
inst✝ : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
v : n → R
val✝ : m₁
⊢ (A₁.fromRows A₂ *ᵥ v) (Sum.inl val✝) = Sum.elim (A₁ *ᵥ v) (A₂ *ᵥ v) (Sum.inl val✝)

pp: case inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝¹ : Semiring R
inst✝ : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
v : n → R
val✝ : m₂
⊢ (A₁.fromRows A₂ *ᵥ v) (Sum.inr val✝) = Sum.elim (A₁ *ᵥ v) (A₂ *ᵥ v) (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝¹ : Semiring R
inst✝ : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
v : n → R
val✝ : m₁
⊢ (A₁.fromRows A₂ *ᵥ v) (Sum.inl val✝) = Sum.elim (A₁ *ᵥ v) (A₂ *ᵥ v) (Sum.inl val✝)

case inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝¹ : Semiring R
inst✝ : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
v : n → R
val✝ : m₂
⊢ (A₁.fromRows A₂ *ᵥ v) (Sum.inr val✝) = Sum.elim (A₁ *ᵥ v) (A₂ *ᵥ v) (Sum.inr val✝)
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst✝¹ : Semiring R
inst✝ : Fintype m
B₁ : Matrix m n₁ R
B₂ : Matrix m n₂ R
v : m → R
val✝ : n₁
⊢ (v ᵥ* B₁.fromCols B₂) (Sum.inl val✝) = Sum.elim (v ᵥ* B₁) (v ᵥ* B₂) (Sum.inl val✝)

pp: case inr
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst✝¹ : Semiring R
inst✝ : Fintype m
B₁ : Matrix m n₁ R
B₂ : Matrix m n₂ R
v : m → R
val✝ : n₂
⊢ (v ᵥ* B₁.fromCols B₂) (Sum.inr val✝) = Sum.elim (v ᵥ* B₁) (v ᵥ* B₂) (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst✝¹ : Semiring R
inst✝ : Fintype m
B₁ : Matrix m n₁ R
B₂ : Matrix m n₂ R
v : m → R
val✝ : n₁
⊢ (v ᵥ* B₁.fromCols B₂) (Sum.inl val✝) = Sum.elim (v ᵥ* B₁) (v ᵥ* B₂) (Sum.inl val✝)

case inr
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst✝¹ : Semiring R
inst✝ : Fintype m
B₁ : Matrix m n₁ R
B₂ : Matrix m n₂ R
v : m → R
val✝ : n₂
⊢ (v ᵥ* B₁.fromCols B₂) (Sum.inr val✝) = Sum.elim (v ᵥ* B₁) (v ᵥ* B₂) (Sum.inr val✝)
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝¹ : Semiring R
inst✝ : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B : Matrix n m R
val✝ : m₁
j✝ : m
⊢ (A₁.fromRows A₂ * B) (Sum.inl val✝) j✝ = (A₁ * B).fromRows (A₂ * B) (Sum.inl val✝) j✝

pp: case inr
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝¹ : Semiring R
inst✝ : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B : Matrix n m R
val✝ : m₂
j✝ : m
⊢ (A₁.fromRows A₂ * B) (Sum.inr val✝) j✝ = (A₁ * B).fromRows (A₂ * B) (Sum.inr val✝) j✝

Tactic:
<;>

Goal state after:
case inl
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝¹ : Semiring R
inst✝ : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B : Matrix n m R
val✝ : m₁
j✝ : m
⊢ (A₁.fromRows A₂ * B) (Sum.inl val✝) j✝ = (A₁ * B).fromRows (A₂ * B) (Sum.inl val✝) j✝

case inr
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝¹ : Semiring R
inst✝ : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B : Matrix n m R
val✝ : m₂
j✝ : m
⊢ (A₁.fromRows A₂ * B) (Sum.inr val✝) j✝ = (A₁ * B).fromRows (A₂ * B) (Sum.inr val✝) j✝
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl
R : Type u_1
m : Type u_2
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹ : Semiring R
inst✝ : Fintype n
A : Matrix m n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
i✝ : m
val✝ : n₁
⊢ (A * B₁.fromCols B₂) i✝ (Sum.inl val✝) = (A * B₁).fromCols (A * B₂) i✝ (Sum.inl val✝)

pp: case inr
R : Type u_1
m : Type u_2
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹ : Semiring R
inst✝ : Fintype n
A : Matrix m n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
i✝ : m
val✝ : n₂
⊢ (A * B₁.fromCols B₂) i✝ (Sum.inr val✝) = (A * B₁).fromCols (A * B₂) i✝ (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl
R : Type u_1
m : Type u_2
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹ : Semiring R
inst✝ : Fintype n
A : Matrix m n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
i✝ : m
val✝ : n₁
⊢ (A * B₁.fromCols B₂) i✝ (Sum.inl val✝) = (A * B₁).fromCols (A * B₂) i✝ (Sum.inl val✝)

case inr
R : Type u_1
m : Type u_2
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹ : Semiring R
inst✝ : Fintype n
A : Matrix m n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
i✝ : m
val✝ : n₂
⊢ (A * B₁.fromCols B₂) i✝ (Sum.inr val✝) = (A * B₁).fromCols (A * B₂) i✝ (Sum.inr val✝)
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Semiring R
val✝ : m₁
j✝ : n
⊢ fromRows 0 0 (Sum.inl val✝) j✝ = 0 (Sum.inl val✝) j✝

pp: case inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Semiring R
val✝ : m₂
j✝ : n
⊢ fromRows 0 0 (Sum.inr val✝) j✝ = 0 (Sum.inr val✝) j✝

Tactic:
<;>

Goal state after:
case inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Semiring R
val✝ : m₁
j✝ : n
⊢ fromRows 0 0 (Sum.inl val✝) j✝ = 0 (Sum.inl val✝) j✝

case inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Semiring R
val✝ : m₂
j✝ : n
⊢ fromRows 0 0 (Sum.inr val✝) j✝ = 0 (Sum.inr val✝) j✝
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst✝ : Semiring R
i✝ : m
val✝ : n₁
⊢ fromCols 0 0 i✝ (Sum.inl val✝) = 0 i✝ (Sum.inl val✝)

pp: case inr
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst✝ : Semiring R
i✝ : m
val✝ : n₂
⊢ fromCols 0 0 i✝ (Sum.inr val✝) = 0 i✝ (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst✝ : Semiring R
i✝ : m
val✝ : n₁
⊢ fromCols 0 0 i✝ (Sum.inl val✝) = 0 i✝ (Sum.inl val✝)

case inr
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst✝ : Semiring R
i✝ : m
val✝ : n₂
⊢ fromCols 0 0 i✝ (Sum.inr val✝) = 0 i✝ (Sum.inr val✝)
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A₁ : Matrix m m₁ R
A₂ : Matrix m m₂ R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
i✝ : m
val✝ : n₁
⊢ (A₁.fromCols A₂ * fromBlocks B₁₁ B₁₂ B₂₁ B₂₂) i✝ (Sum.inl val✝) =
    (A₁ * B₁₁ + A₂ * B₂₁).fromCols (A₁ * B₁₂ + A₂ * B₂₂) i✝ (Sum.inl val✝)

pp: case inr
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A₁ : Matrix m m₁ R
A₂ : Matrix m m₂ R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
i✝ : m
val✝ : n₂
⊢ (A₁.fromCols A₂ * fromBlocks B₁₁ B₁₂ B₂₁ B₂₂) i✝ (Sum.inr val✝) =
    (A₁ * B₁₁ + A₂ * B₂₁).fromCols (A₁ * B₁₂ + A₂ * B₂₂) i✝ (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A₁ : Matrix m m₁ R
A₂ : Matrix m m₂ R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
i✝ : m
val✝ : n₁
⊢ (A₁.fromCols A₂ * fromBlocks B₁₁ B₁₂ B₂₁ B₂₂) i✝ (Sum.inl val✝) =
    (A₁ * B₁₁ + A₂ * B₂₁).fromCols (A₁ * B₁₂ + A₂ * B₂₂) i✝ (Sum.inl val✝)

case inr
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A₁ : Matrix m m₁ R
A₂ : Matrix m m₂ R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
i✝ : m
val✝ : n₂
⊢ (A₁.fromCols A₂ * fromBlocks B₁₁ B₁₂ B₂₁ B₂₂) i✝ (Sum.inr val✝) =
    (A₁ * B₁₁ + A₂ * B₂₁).fromCols (A₁ * B₁₂ + A₂ * B₂₂) i✝ (Sum.inr val✝)