awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
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
a : ∀ (i : n) (j : m₁), (-A₁.fromCols A₂) i (Sum.inl j) = (-A₁).fromCols (-A₂) i (Sum.inl j)
a₁ : ∀ (i : n) (j : m₂), (-A₁.fromCols A₂) i (Sum.inr j) = (-A₁).fromCols (-A₂) i (Sum.inr j)
⊢ -A₁.fromCols A₂ = (-A₁).fromCols (-A₂)

Tactic:
ext i (j | j)
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
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)

Tactic:
simp
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
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:
simp
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
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
a :
  ∀ (val : m₁) (val_1 : n₁),
    (B₁₁.fromRows B₂₁).fromCols (B₁₂.fromRows B₂₂) (Sum.inl val) (Sum.inl val_1) =
      fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inl val) (Sum.inl val_1)
a₁ :
  ∀ (val : m₁) (val_1 : n₂),
    (B₁₁.fromRows B₂₁).fromCols (B₁₂.fromRows B₂₂) (Sum.inl val) (Sum.inr val_1) =
      fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inl val) (Sum.inr val_1)
a₂ :
  ∀ (val : m₂) (val_1 : n₁),
    (B₁₁.fromRows B₂₁).fromCols (B₁₂.fromRows B₂₂) (Sum.inr val) (Sum.inl val_1) =
      fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inr val) (Sum.inl val_1)
a₃ :
  ∀ (val : m₂) (val_1 : n₂),
    (B₁₁.fromRows B₂₁).fromCols (B₁₂.fromRows B₂₂) (Sum.inr val) (Sum.inr val_1) =
      fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inr val) (Sum.inr val_1)
⊢ (B₁₁.fromRows B₂₁).fromCols (B₁₂.fromRows B₂₂) = fromBlocks B₁₁ B₁₂ B₂₁ B₂₂

Tactic:
ext (_ | _) (_ | _)
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
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_1 : n₁
⊢ (B₁₁.fromRows B₂₁).fromCols (B₁₂.fromRows B₂₂) (Sum.inl val) (Sum.inl val_1) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inl val) (Sum.inl val_1)

Tactic:
simp
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
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_1 : n₂
⊢ (B₁₁.fromRows B₂₁).fromCols (B₁₂.fromRows B₂₂) (Sum.inl val) (Sum.inr val_1) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inl val) (Sum.inr val_1)

Tactic:
simp
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
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_1 : n₁
⊢ (B₁₁.fromRows B₂₁).fromCols (B₁₂.fromRows B₂₂) (Sum.inr val) (Sum.inl val_1) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inr val) (Sum.inl val_1)

Tactic:
simp
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
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_1 : n₂
⊢ (B₁₁.fromRows B₂₁).fromCols (B₁₂.fromRows B₂₂) (Sum.inr val) (Sum.inr val_1) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inr val) (Sum.inr val_1)

Tactic:
simp
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
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
a :
  ∀ (val : m₁) (val_1 : n₁),
    (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) (Sum.inl val) (Sum.inl val_1) =
      fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inl val) (Sum.inl val_1)
a₁ :
  ∀ (val : m₁) (val_1 : n₂),
    (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) (Sum.inl val) (Sum.inr val_1) =
      fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inl val) (Sum.inr val_1)
a₂ :
  ∀ (val : m₂) (val_1 : n₁),
    (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) (Sum.inr val) (Sum.inl val_1) =
      fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inr val) (Sum.inl val_1)
a₃ :
  ∀ (val : m₂) (val_1 : n₂),
    (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) (Sum.inr val) (Sum.inr val_1) =
      fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inr val) (Sum.inr val_1)
⊢ (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) = fromBlocks B₁₁ B₁₂ B₂₁ B₂₂

Tactic:
ext (_ | _) (_ | _)
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
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_1 : n₁
⊢ (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) (Sum.inl val) (Sum.inl val_1) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inl val) (Sum.inl val_1)

Tactic:
simp
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
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_1 : n₂
⊢ (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) (Sum.inl val) (Sum.inr val_1) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inl val) (Sum.inr val_1)

Tactic:
simp
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
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_1 : n₁
⊢ (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) (Sum.inr val) (Sum.inl val_1) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inr val) (Sum.inl val_1)

Tactic:
simp
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
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_1 : n₂
⊢ (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) (Sum.inr val) (Sum.inr val_1) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inr val) (Sum.inr val_1)

Tactic:
simp
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst : Semiring R
inst_1 : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
v : n → R
h : ∀ (val : m₁), (A₁.fromRows A₂ *ᵥ v) (Sum.inl val) = Sum.elim (A₁ *ᵥ v) (A₂ *ᵥ v) (Sum.inl val)
h₁ : ∀ (val : m₂), (A₁.fromRows A₂ *ᵥ v) (Sum.inr val) = Sum.elim (A₁ *ᵥ v) (A₂ *ᵥ v) (Sum.inr val)
⊢ A₁.fromRows A₂ *ᵥ v = Sum.elim (A₁ *ᵥ v) (A₂ *ᵥ v)

Tactic:
ext (_ | _)
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst : Semiring R
inst_1 : 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)

Tactic:
rfl
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst : Semiring R
inst_1 : 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:
rfl
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
inst_1 : Fintype m
B₁ : Matrix m n₁ R
B₂ : Matrix m n₂ R
v : m → R
h : ∀ (val : n₁), (v ᵥ* B₁.fromCols B₂) (Sum.inl val) = Sum.elim (v ᵥ* B₁) (v ᵥ* B₂) (Sum.inl val)
h₁ : ∀ (val : n₂), (v ᵥ* B₁.fromCols B₂) (Sum.inr val) = Sum.elim (v ᵥ* B₁) (v ᵥ* B₂) (Sum.inr val)
⊢ v ᵥ* B₁.fromCols B₂ = Sum.elim (v ᵥ* B₁) (v ᵥ* B₂)

Tactic:
ext (_ | _)
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
inst_1 : 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)

Tactic:
rfl
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
inst_1 : 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:
rfl
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst : Semiring R
inst_1 : Fintype m₁
inst_2 : Fintype m₂
B₁ : Matrix m₁ n R
B₂ : Matrix m₂ n R
v₁ : m₁ → R
v₂ : m₂ → R
h : ∀ (x : n), (Sum.elim v₁ v₂ ᵥ* B₁.fromRows B₂) x = (v₁ ᵥ* B₁ + v₂ ᵥ* B₂) x
⊢ Sum.elim v₁ v₂ ᵥ* B₁.fromRows B₂ = v₁ ᵥ* B₁ + v₂ ᵥ* B₂

Tactic:
ext
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst : Semiring R
inst_1 : Fintype m₁
inst_2 : Fintype m₂
B₁ : Matrix m₁ n R
B₂ : Matrix m₂ n R
v₁ : m₁ → R
v₂ : m₂ → R
x : n
⊢ (Sum.elim v₁ v₂ ᵥ* B₁.fromRows B₂) x = (v₁ ᵥ* B₁ + v₂ ᵥ* B₂) x

Tactic:
simp [Matrix.vecMul, fromRows, dotProduct]

Premises used: dotProduct, Matrix.vecMul, Matrix.fromRows
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst : Semiring R
inst_1 : Fintype m₁
inst_2 : Fintype m₂
B₁ : Matrix m₁ n R
B₂ : Matrix m₂ n R
v : m₁ ⊕ m₂ → R
⊢ v ᵥ* B₁.fromRows B₂ = v ∘ Sum.inl ᵥ* B₁ + v ∘ Sum.inr ᵥ* B₂

Tactic:
simp [← sumElim_vecMul_fromRows]

Premises used: Matrix.sumElim_vecMul_fromRows
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
inst_1 : Fintype n₁
inst_2 : Fintype n₂
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
v₁ : n₁ → R
v₂ : n₂ → R
h : ∀ (x : m), (A₁.fromCols A₂ *ᵥ Sum.elim v₁ v₂) x = (A₁ *ᵥ v₁ + A₂ *ᵥ v₂) x
⊢ A₁.fromCols A₂ *ᵥ Sum.elim v₁ v₂ = A₁ *ᵥ v₁ + A₂ *ᵥ v₂

Tactic:
ext
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
inst_1 : Fintype n₁
inst_2 : Fintype n₂
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
v₁ : n₁ → R
v₂ : n₂ → R
x : m
⊢ (A₁.fromCols A₂ *ᵥ Sum.elim v₁ v₂) x = (A₁ *ᵥ v₁ + A₂ *ᵥ v₂) x

Tactic:
simp [Matrix.mulVec, fromCols]

Premises used: Matrix.fromCols, Matrix.mulVec
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
inst_1 : Fintype n₁
inst_2 : Fintype n₂
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
v : n₁ ⊕ n₂ → R
⊢ A₁.fromCols A₂ *ᵥ v = A₁ *ᵥ v ∘ Sum.inl + A₂ *ᵥ v ∘ Sum.inr

Tactic:
simp [← fromCols_mulVec_sumElim]

Premises used: Matrix.fromCols_mulVec_sumElim
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst : Semiring R
inst_1 : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B : Matrix n m R
a : ∀ (val : m₁) (j : m), (A₁.fromRows A₂ * B) (Sum.inl val) j = (A₁ * B).fromRows (A₂ * B) (Sum.inl val) j
a₁ : ∀ (val : m₂) (j : m), (A₁.fromRows A₂ * B) (Sum.inr val) j = (A₁ * B).fromRows (A₂ * B) (Sum.inr val) j
⊢ A₁.fromRows A₂ * B = (A₁ * B).fromRows (A₂ * B)

Tactic:
ext (_ | _) _
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst : Semiring R
inst_1 : 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

Tactic:
simp [mul_apply]

Premises used: Matrix.mul_apply
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst : Semiring R
inst_1 : 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:
simp [mul_apply]

Premises used: Matrix.mul_apply
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
inst_1 : Fintype n
A : Matrix m n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
a : ∀ (i : m) (val : n₁), (A * B₁.fromCols B₂) i (Sum.inl val) = (A * B₁).fromCols (A * B₂) i (Sum.inl val)
a₁ : ∀ (i : m) (val : n₂), (A * B₁.fromCols B₂) i (Sum.inr val) = (A * B₁).fromCols (A * B₂) i (Sum.inr val)
⊢ A * B₁.fromCols B₂ = (A * B₁).fromCols (A * B₂)

Tactic:
ext _ (_ | _)
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
inst_1 : 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)

Tactic:
simp [mul_apply]

Premises used: Matrix.mul_apply
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
inst_1 : 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:
simp [mul_apply]

Premises used: Matrix.mul_apply
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst : Semiring R
a :
  ∀ (val : m₁) (j : n),
    Eq.{u_1 + 1} (α := R) (fromRows.{u_1, u_3, u_4, u_5} (m₂ := m₂) 0 0 (Sum.inl val) j) (0 (Sum.inl val) j)
a₁ :
  ∀ (val : m₂) (j : n),
    Eq.{u_1 + 1} (α := R) (fromRows.{u_1, u_3, u_4, u_5} (m₁ := m₁) 0 0 (Sum.inr val) j) (0 (Sum.inr val) j)
⊢ Eq (α := Matrix (m₁ ⊕ m₂) n R) (fromRows 0 0) 0

Tactic:
ext (_ | _) _
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst : Semiring R
val : m₁
j : n
⊢ Eq.{u_1 + 1} (α := R) (fromRows.{u_1, u_3, u_4, u_5} (m₂ := m₂) 0 0 (Sum.inl val) j) (0 (Sum.inl val) j)

Tactic:
simp
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst : Semiring R
val : m₂
j : n
⊢ Eq.{u_1 + 1} (α := R) (fromRows.{u_1, u_3, u_4, u_5} (m₁ := m₁) 0 0 (Sum.inr val) j) (0 (Sum.inr val) j)

Tactic:
simp
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
a :
  ∀ (i : m) (val : n₁),
    Eq.{u_1 + 1} (α := R) (fromCols.{u_1, u_2, u_6, u_7} (n₂ := n₂) 0 0 i (Sum.inl val)) (0 i (Sum.inl val))
a₁ :
  ∀ (i : m) (val : n₂),
    Eq.{u_1 + 1} (α := R) (fromCols.{u_1, u_2, u_6, u_7} (n₁ := n₁) 0 0 i (Sum.inr val)) (0 i (Sum.inr val))
⊢ Eq (α := Matrix m (n₁ ⊕ n₂) R) (fromCols 0 0) 0

Tactic:
ext _ (_ | _)
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
i : m
val : n₁
⊢ Eq.{u_1 + 1} (α := R) (fromCols.{u_1, u_2, u_6, u_7} (n₂ := n₂) 0 0 i (Sum.inl val)) (0 i (Sum.inl val))

Tactic:
simp
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
i : m
val : n₂
⊢ Eq.{u_1 + 1} (α := R) (fromCols.{u_1, u_2, u_6, u_7} (n₁ := n₁) 0 0 i (Sum.inr val)) (0 i (Sum.inr val))

Tactic:
simp
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
inst_1 : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
a :
  ∀ (val : m₁) (val_1 : n₁),
    (A₁.fromRows A₂ * B₁.fromCols B₂) (Sum.inl val) (Sum.inl val_1) =
      fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂) (Sum.inl val) (Sum.inl val_1)
a₁ :
  ∀ (val : m₁) (val_1 : n₂),
    (A₁.fromRows A₂ * B₁.fromCols B₂) (Sum.inl val) (Sum.inr val_1) =
      fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂) (Sum.inl val) (Sum.inr val_1)
a₂ :
  ∀ (val : m₂) (val_1 : n₁),
    (A₁.fromRows A₂ * B₁.fromCols B₂) (Sum.inr val) (Sum.inl val_1) =
      fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂) (Sum.inr val) (Sum.inl val_1)
a₃ :
  ∀ (val : m₂) (val_1 : n₂),
    (A₁.fromRows A₂ * B₁.fromCols B₂) (Sum.inr val) (Sum.inr val_1) =
      fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂) (Sum.inr val) (Sum.inr val_1)
⊢ A₁.fromRows A₂ * B₁.fromCols B₂ = fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂)

Tactic:
ext (_ | _) (_ | _)
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
inst_1 : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
val : m₁
val_1 : n₁
⊢ (A₁.fromRows A₂ * B₁.fromCols B₂) (Sum.inl val) (Sum.inl val_1) =
    fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂) (Sum.inl val) (Sum.inl val_1)

Tactic:
simp
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
inst_1 : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
val : m₁
val_1 : n₂
⊢ (A₁.fromRows A₂ * B₁.fromCols B₂) (Sum.inl val) (Sum.inr val_1) =
    fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂) (Sum.inl val) (Sum.inr val_1)

Tactic:
simp
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
inst_1 : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
val : m₂
val_1 : n₁
⊢ (A₁.fromRows A₂ * B₁.fromCols B₂) (Sum.inr val) (Sum.inl val_1) =
    fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂) (Sum.inr val) (Sum.inl val_1)

Tactic:
simp
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
inst_1 : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
val : m₂
val_1 : n₂
⊢ (A₁.fromRows A₂ * B₁.fromCols B₂) (Sum.inr val) (Sum.inr val_1) =
    fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂) (Sum.inr val) (Sum.inr val_1)

Tactic:
simp
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
inst_1 : Fintype n₁
inst_2 : Fintype n₂
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
B₁ : Matrix n₁ n R
B₂ : Matrix n₂ n R
a : ∀ (i : m) (j : n), (A₁.fromCols A₂ * B₁.fromRows B₂) i j = (A₁ * B₁ + A₂ * B₂) i j
⊢ A₁.fromCols A₂ * B₁.fromRows B₂ = A₁ * B₁ + A₂ * B₂

Tactic:
ext
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
inst_1 : Fintype n₁
inst_2 : Fintype n₂
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
B₁ : Matrix n₁ n R
B₂ : Matrix n₂ n R
i : m
j : n
⊢ (A₁.fromCols A₂ * B₁.fromRows B₂) i j = (A₁ * B₁ + A₂ * B₂) i j

Tactic:
simp [mul_apply]

Premises used: Matrix.mul_apply
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
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_1 : Fintype m₁
inst_2 : 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
a :
  ∀ (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)
a₁ :
  ∀ (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)
⊢ A₁.fromCols A₂ * fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ = (A₁ * B₁₁ + A₂ * B₂₁).fromCols (A₁ * B₁₂ + A₂ * B₂₂)

Tactic:
ext _ (_ | _)
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
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_1 : Fintype m₁
inst_2 : 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)

Tactic:
simp [mul_apply]

Premises used: Matrix.mul_apply
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
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_1 : Fintype m₁
inst_2 : 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:
simp [mul_apply]

Premises used: Matrix.mul_apply
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
inst_1 : Fintype n₁
inst_2 : Fintype n₂
A₁ : Matrix n₁ n R
A₂ : Matrix n₂ n R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
a :
  ∀ (val : m₁) (j : n),
    (fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ * A₁.fromRows A₂) (Sum.inl val) j =
      (B₁₁ * A₁ + B₁₂ * A₂).fromRows (B₂₁ * A₁ + B₂₂ * A₂) (Sum.inl val) j
a₁ :
  ∀ (val : m₂) (j : n),
    (fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ * A₁.fromRows A₂) (Sum.inr val) j =
      (B₁₁ * A₁ + B₁₂ * A₂).fromRows (B₂₁ * A₁ + B₂₂ * A₂) (Sum.inr val) j
⊢ fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ * A₁.fromRows A₂ = (B₁₁ * A₁ + B₁₂ * A₂).fromRows (B₂₁ * A₁ + B₂₂ * A₂)

Tactic:
ext (_ | _) _
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
inst_1 : Fintype n₁
inst_2 : Fintype n₂
A₁ : Matrix n₁ n R
A₂ : Matrix n₂ n R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val : m₁
j : n
⊢ (fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ * A₁.fromRows A₂) (Sum.inl val) j =
    (B₁₁ * A₁ + B₁₂ * A₂).fromRows (B₂₁ * A₁ + B₂₂ * A₂) (Sum.inl val) j

Tactic:
simp [mul_apply]

Premises used: Matrix.mul_apply
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
inst_1 : Fintype n₁
inst_2 : Fintype n₂
A₁ : Matrix n₁ n R
A₂ : Matrix n₂ n R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val : m₂
j : n
⊢ (fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ * A₁.fromRows A₂) (Sum.inr val) j =
    (B₁₁ * A₁ + B₁₂ * A₂).fromRows (B₂₁ * A₁ + B₂₂ * A₂) (Sum.inr val) j

Tactic:
simp [mul_apply]

Premises used: Matrix.mul_apply
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst : CommRing R
inst_1 : Fintype n₁
inst_2 : Fintype n₂
inst_3 : Fintype n
inst_4 : DecidableEq n
inst_5 : DecidableEq n₁
inst_6 : DecidableEq n₂
e : n ≃ n₁ ⊕ n₂
A₁ : Matrix n n₁ R
A₂ : Matrix n n₂ R
B₁ : Matrix n₁ n R
B₂ : Matrix n₂ n R
⊢ A₁.fromCols A₂ * B₁.fromRows B₂ = 1 ↔ B₁.fromRows B₂ * A₁.fromCols A₂ = 1

Tactic:
mul_eq_one_comm_of_equiv e

Premises used: Matrix.mul_eq_one_comm_of_equiv
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
n : Type u_5
inst : CommRing R
inst_1 : Fintype n
inst_2 : DecidableEq n
p : n → Prop
inst_3 : DecidablePred p
A₁ : Matrix n { i : n // p i } R
A₂ : Matrix n { i : n // ¬p i } R
B₁ : Matrix { i : n // p i } n R
B₂ : Matrix { i : n // ¬p i } n R
⊢ A₁.fromCols A₂ * B₁.fromRows B₂ = 1 ↔ B₁.fromRows B₂ * A₁.fromCols A₂ = 1

Tactic:
fromCols_mul_fromRows_eq_one_comm (Equiv.sumCompl p).symm A₁ A₂ B₁ B₂

Premises used: Matrix.fromCols_mul_fromRows_eq_one_comm, Equiv.sumCompl, Equiv.symm
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst : Star R
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
a : ∀ (val : n₁) (j : m), (A₁.fromCols A₂)ᴴ (Sum.inl val) j = A₁ᴴ.fromRows A₂ᴴ (Sum.inl val) j
a₁ : ∀ (val : n₂) (j : m), (A₁.fromCols A₂)ᴴ (Sum.inr val) j = A₁ᴴ.fromRows A₂ᴴ (Sum.inr val) j
⊢ (A₁.fromCols A₂)ᴴ = A₁ᴴ.fromRows A₂ᴴ

Tactic:
ext (_ | _) _
-- Module: Mathlib.Data.Matrix.ColumnRowPartitioned
Goal:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst : Star R
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
val : n₁
j : m
⊢ (A₁.fromCols A₂)ᴴ (Sum.inl val) j = A₁ᴴ.fromRows A₂ᴴ (Sum.inl val) j

Tactic:
simp