awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Matrix.Block
Goal:
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
i : n ⊕ o
j : l ⊕ m
a : ∀ (val : n), (-fromBlocks A B C D) (Sum.inl val) j = fromBlocks (-A) (-B) (-C) (-D) (Sum.inl val) j
a₁ : ∀ (val : o), (-fromBlocks A B C D) (Sum.inr val) j = fromBlocks (-A) (-B) (-C) (-D) (Sum.inr val) j
⊢ (-fromBlocks A B C D) i j = fromBlocks (-A) (-B) (-C) (-D) i j

Tactic:
cases i
-- Module: Mathlib.Data.Matrix.Block
Goal:
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
a :
  ∀ (val_1 : l),
    (-fromBlocks A B C D) (Sum.inl val) (Sum.inl val_1) = fromBlocks (-A) (-B) (-C) (-D) (Sum.inl val) (Sum.inl val_1)
a₁ :
  ∀ (val_1 : m),
    (-fromBlocks A B C D) (Sum.inl val) (Sum.inr val_1) = fromBlocks (-A) (-B) (-C) (-D) (Sum.inl val) (Sum.inr val_1)
⊢ (-fromBlocks A B C D) (Sum.inl val) j = fromBlocks (-A) (-B) (-C) (-D) (Sum.inl val) j

Tactic:
cases j
-- Module: Mathlib.Data.Matrix.Block
Goal:
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
a :
  ∀ (val_1 : l),
    (-fromBlocks A B C D) (Sum.inr val) (Sum.inl val_1) = fromBlocks (-A) (-B) (-C) (-D) (Sum.inr val) (Sum.inl val_1)
a₁ :
  ∀ (val_1 : m),
    (-fromBlocks A B C D) (Sum.inr val) (Sum.inr val_1) = fromBlocks (-A) (-B) (-C) (-D) (Sum.inr val) (Sum.inr val_1)
⊢ (-fromBlocks A B C D) (Sum.inr val) j = fromBlocks (-A) (-B) (-C) (-D) (Sum.inr val) j

Tactic:
cases j
-- Module: Mathlib.Data.Matrix.Block
Goal:
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_1 : l
⊢ (-fromBlocks A B C D) (Sum.inl val) (Sum.inl val_1) = fromBlocks (-A) (-B) (-C) (-D) (Sum.inl val) (Sum.inl val_1)

Tactic:
simp [fromBlocks]

Premises used: Matrix.fromBlocks
-- Module: Mathlib.Data.Matrix.Block
Goal:
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_1 : m
⊢ (-fromBlocks A B C D) (Sum.inl val) (Sum.inr val_1) = fromBlocks (-A) (-B) (-C) (-D) (Sum.inl val) (Sum.inr val_1)

Tactic:
simp [fromBlocks]

Premises used: Matrix.fromBlocks
-- Module: Mathlib.Data.Matrix.Block
Goal:
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_1 : l
⊢ (-fromBlocks A B C D) (Sum.inr val) (Sum.inl val_1) = fromBlocks (-A) (-B) (-C) (-D) (Sum.inr val) (Sum.inl val_1)

Tactic:
simp [fromBlocks]

Premises used: Matrix.fromBlocks
-- Module: Mathlib.Data.Matrix.Block
Goal:
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_1 : m
⊢ (-fromBlocks A B C D) (Sum.inr val) (Sum.inr val_1) = fromBlocks (-A) (-B) (-C) (-D) (Sum.inr val) (Sum.inr val_1)

Tactic:
simp [fromBlocks]

Premises used: Matrix.fromBlocks
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : Zero α
a : ∀ (i : n ⊕ o) (j : l ⊕ m), Eq.{u_12 + 1} (α := α) (fromBlocks 0 0 0 0 i j) (0 i j)
⊢ Eq (α := Matrix (n ⊕ o) (l ⊕ m) α) (fromBlocks 0 0 0 0) 0

Tactic:
ext i j
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : Zero α
i : n ⊕ o
j : l ⊕ m
a :
  ∀ (val : n),
    Eq.{u_12 + 1} (α := α) (fromBlocks.{u_1, u_2, u_3, u_4, u_12} (o := o) 0 0 0 0 (Sum.inl val) j) (0 (Sum.inl val) j)
a₁ :
  ∀ (val : o),
    Eq.{u_12 + 1} (α := α) (fromBlocks.{u_1, u_2, u_3, u_4, u_12} (n := n) 0 0 0 0 (Sum.inr val) j) (0 (Sum.inr val) j)
⊢ Eq.{u_12 + 1} (α := α) (fromBlocks 0 0 0 0 i j) (0 i j)

Tactic:
rcases i with ⟨⟩
-- Module: Mathlib.Data.Matrix.Block
Goal:
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
a :
  ∀ (val_1 : l),
    Eq.{u_12 + 1} (α := α)
      (fromBlocks.{u_1, u_2, u_3, u_4, u_12} (m := m) (o := o) 0 0 0 0 (Sum.inl val) (Sum.inl val_1))
      (0 (Sum.inl val) (Sum.inl val_1))
a₁ :
  ∀ (val_1 : m),
    Eq.{u_12 + 1} (α := α)
      (fromBlocks.{u_1, u_2, u_3, u_4, u_12} (l := l) (o := o) 0 0 0 0 (Sum.inl val) (Sum.inr val_1))
      (0 (Sum.inl val) (Sum.inr val_1))
⊢ Eq.{u_12 + 1} (α := α) (fromBlocks.{u_1, u_2, u_3, u_4, u_12} (o := o) 0 0 0 0 (Sum.inl val) j) (0 (Sum.inl val) j)

Tactic:
rcases j with ⟨⟩
-- Module: Mathlib.Data.Matrix.Block
Goal:
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
a :
  ∀ (val_1 : l),
    Eq.{u_12 + 1} (α := α)
      (fromBlocks.{u_1, u_2, u_3, u_4, u_12} (m := m) (n := n) 0 0 0 0 (Sum.inr val) (Sum.inl val_1))
      (0 (Sum.inr val) (Sum.inl val_1))
a₁ :
  ∀ (val_1 : m),
    Eq.{u_12 + 1} (α := α)
      (fromBlocks.{u_1, u_2, u_3, u_4, u_12} (l := l) (n := n) 0 0 0 0 (Sum.inr val) (Sum.inr val_1))
      (0 (Sum.inr val) (Sum.inr val_1))
⊢ Eq.{u_12 + 1} (α := α) (fromBlocks.{u_1, u_2, u_3, u_4, u_12} (n := n) 0 0 0 0 (Sum.inr val) j) (0 (Sum.inr val) j)

Tactic:
rcases j with ⟨⟩
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : Zero α
val : n
val_1 : l
⊢ Eq.{u_12 + 1} (α := α) (fromBlocks.{u_1, u_2, u_3, u_4, u_12} (m := m) (o := o) 0 0 0 0 (Sum.inl val) (Sum.inl val_1))
    (0 (Sum.inl val) (Sum.inl val_1))

Tactic:
rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : Zero α
val : n
val_1 : m
⊢ Eq.{u_12 + 1} (α := α) (fromBlocks.{u_1, u_2, u_3, u_4, u_12} (l := l) (o := o) 0 0 0 0 (Sum.inl val) (Sum.inr val_1))
    (0 (Sum.inl val) (Sum.inr val_1))

Tactic:
rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : Zero α
val : o
val_1 : l
⊢ Eq.{u_12 + 1} (α := α) (fromBlocks.{u_1, u_2, u_3, u_4, u_12} (m := m) (n := n) 0 0 0 0 (Sum.inr val) (Sum.inl val_1))
    (0 (Sum.inr val) (Sum.inl val_1))

Tactic:
rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : Zero α
val : o
val_1 : m
⊢ Eq.{u_12 + 1} (α := α) (fromBlocks.{u_1, u_2, u_3, u_4, u_12} (l := l) (n := n) 0 0 0 0 (Sum.inr val) (Sum.inr val_1))
    (0 (Sum.inr val) (Sum.inr val_1))

Tactic:
rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
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 α
a :
  ∀ (i : n ⊕ o) (j : l ⊕ m),
    (fromBlocks A B C D + fromBlocks A' B' C' D') i j = fromBlocks (A + A') (B + B') (C + C') (D + D') i j
⊢ fromBlocks A B C D + fromBlocks A' B' C' D' = fromBlocks (A + A') (B + B') (C + C') (D + D')

Tactic:
ext i j
-- Module: Mathlib.Data.Matrix.Block
Goal:
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 α
i : n ⊕ o
j : l ⊕ m
a :
  ∀ (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
a₁ :
  ∀ (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
⊢ (fromBlocks A B C D + fromBlocks A' B' C' D') i j = fromBlocks (A + A') (B + B') (C + C') (D + D') i j

Tactic:
rcases i with ⟨⟩
-- Module: Mathlib.Data.Matrix.Block
Goal:
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
a :
  ∀ (val_1 : l),
    (fromBlocks A B C D + fromBlocks A' B' C' D') (Sum.inl val) (Sum.inl val_1) =
      fromBlocks (A + A') (B + B') (C + C') (D + D') (Sum.inl val) (Sum.inl val_1)
a₁ :
  ∀ (val_1 : m),
    (fromBlocks A B C D + fromBlocks A' B' C' D') (Sum.inl val) (Sum.inr val_1) =
      fromBlocks (A + A') (B + B') (C + C') (D + D') (Sum.inl val) (Sum.inr val_1)
⊢ (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

Tactic:
rcases j with ⟨⟩
-- Module: Mathlib.Data.Matrix.Block
Goal:
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
a :
  ∀ (val_1 : l),
    (fromBlocks A B C D + fromBlocks A' B' C' D') (Sum.inr val) (Sum.inl val_1) =
      fromBlocks (A + A') (B + B') (C + C') (D + D') (Sum.inr val) (Sum.inl val_1)
a₁ :
  ∀ (val_1 : m),
    (fromBlocks A B C D + fromBlocks A' B' C' D') (Sum.inr val) (Sum.inr val_1) =
      fromBlocks (A + A') (B + B') (C + C') (D + D') (Sum.inr val) (Sum.inr val_1)
⊢ (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:
rcases j with ⟨⟩
-- Module: Mathlib.Data.Matrix.Block
Goal:
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 α
val : n
val_1 : l
⊢ (fromBlocks A B C D + fromBlocks A' B' C' D') (Sum.inl val) (Sum.inl val_1) =
    fromBlocks (A + A') (B + B') (C + C') (D + D') (Sum.inl val) (Sum.inl val_1)

Tactic:
rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
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 α
val : n
val_1 : m
⊢ (fromBlocks A B C D + fromBlocks A' B' C' D') (Sum.inl val) (Sum.inr val_1) =
    fromBlocks (A + A') (B + B') (C + C') (D + D') (Sum.inl val) (Sum.inr val_1)

Tactic:
rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
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 α
val : o
val_1 : l
⊢ (fromBlocks A B C D + fromBlocks A' B' C' D') (Sum.inr val) (Sum.inl val_1) =
    fromBlocks (A + A') (B + B') (C + C') (D + D') (Sum.inr val) (Sum.inl val_1)

Tactic:
rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
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 α
val : o
val_1 : m
⊢ (fromBlocks A B C D + fromBlocks A' B' C' D') (Sum.inr val) (Sum.inr val_1) =
    fromBlocks (A + A') (B + B') (C + C') (D + D') (Sum.inr val) (Sum.inr val_1)

Tactic:
rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
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_1 : Fintype m
inst_2 : 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 α
a :
  ∀ (i : n ⊕ o) (j : p ⊕ q),
    (fromBlocks A B C D * fromBlocks A' B' C' D') i j =
      fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D') i j
⊢ fromBlocks A B C D * fromBlocks A' B' C' D' =
    fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D')

Tactic:
ext i j
-- Module: Mathlib.Data.Matrix.Block
Goal:
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_1 : Fintype m
inst_2 : 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 α
i : n ⊕ o
j : p ⊕ q
a :
  ∀ (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
a₁ :
  ∀ (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
⊢ (fromBlocks A B C D * fromBlocks A' B' C' D') i j =
    fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D') i j

Tactic:
rcases i with ⟨⟩
-- Module: Mathlib.Data.Matrix.Block
Goal:
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_1 : Fintype m
inst_2 : 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
a :
  ∀ (val_1 : p),
    (fromBlocks A B C D * fromBlocks A' B' C' D') (Sum.inl val) (Sum.inl val_1) =
      fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D') (Sum.inl val) (Sum.inl val_1)
a₁ :
  ∀ (val_1 : q),
    (fromBlocks A B C D * fromBlocks A' B' C' D') (Sum.inl val) (Sum.inr val_1) =
      fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D') (Sum.inl val) (Sum.inr val_1)
⊢ (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

Tactic:
rcases j with ⟨⟩
-- Module: Mathlib.Data.Matrix.Block
Goal:
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_1 : Fintype m
inst_2 : 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
a :
  ∀ (val_1 : p),
    (fromBlocks A B C D * fromBlocks A' B' C' D') (Sum.inr val) (Sum.inl val_1) =
      fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D') (Sum.inr val) (Sum.inl val_1)
a₁ :
  ∀ (val_1 : q),
    (fromBlocks A B C D * fromBlocks A' B' C' D') (Sum.inr val) (Sum.inr val_1) =
      fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D') (Sum.inr val) (Sum.inr val_1)
⊢ (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:
rcases j with ⟨⟩
-- Module: Mathlib.Data.Matrix.Block
Goal:
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_1 : Fintype m
inst_2 : 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 α
val : n
val_1 : p
⊢ (fromBlocks A B C D * fromBlocks A' B' C' D') (Sum.inl val) (Sum.inl val_1) =
    fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D') (Sum.inl val) (Sum.inl val_1)

Tactic:
simp only [fromBlocks, mul_apply, of_apply,
      Sum.elim_inr, Fintype.sum_sum_type, Sum.elim_inl, add_apply]

Premises used: Matrix.fromBlocks, Matrix.add_apply, Fintype.sum_sum_type, Matrix.mul_apply, Matrix.of_apply, Sum.elim_inr, Sum.elim_inl
-- Module: Mathlib.Data.Matrix.Block
Goal:
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_1 : Fintype m
inst_2 : 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 α
val : n
val_1 : q
⊢ (fromBlocks A B C D * fromBlocks A' B' C' D') (Sum.inl val) (Sum.inr val_1) =
    fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D') (Sum.inl val) (Sum.inr val_1)

Tactic:
simp only [fromBlocks, mul_apply, of_apply,
      Sum.elim_inr, Fintype.sum_sum_type, Sum.elim_inl, add_apply]

Premises used: Matrix.fromBlocks, Matrix.add_apply, Fintype.sum_sum_type, Matrix.mul_apply, Matrix.of_apply, Sum.elim_inr, Sum.elim_inl
-- Module: Mathlib.Data.Matrix.Block
Goal:
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_1 : Fintype m
inst_2 : 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 α
val : o
val_1 : p
⊢ (fromBlocks A B C D * fromBlocks A' B' C' D') (Sum.inr val) (Sum.inl val_1) =
    fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D') (Sum.inr val) (Sum.inl val_1)

Tactic:
simp only [fromBlocks, mul_apply, of_apply,
      Sum.elim_inr, Fintype.sum_sum_type, Sum.elim_inl, add_apply]

Premises used: Matrix.fromBlocks, Matrix.add_apply, Fintype.sum_sum_type, Matrix.mul_apply, Matrix.of_apply, Sum.elim_inr, Sum.elim_inl
-- Module: Mathlib.Data.Matrix.Block
Goal:
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_1 : Fintype m
inst_2 : 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 α
val : o
val_1 : q
⊢ (fromBlocks A B C D * fromBlocks A' B' C' D') (Sum.inr val) (Sum.inr val_1) =
    fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D') (Sum.inr val) (Sum.inr val_1)

Tactic:
simp only [fromBlocks, mul_apply, of_apply,
      Sum.elim_inr, Fintype.sum_sum_type, Sum.elim_inl, add_apply]

Premises used: Matrix.fromBlocks, Matrix.add_apply, Fintype.sum_sum_type, Matrix.mul_apply, Matrix.of_apply, Sum.elim_inr, Sum.elim_inl
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
α : Type u_12
inst : Semiring α
inst_1 : Fintype n
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : DecidableEq m
A : Matrix n n α
D : Matrix m m α
zero :
  ∀ (i j : n),
    HPow.hPow (β := ℕ) (fromBlocks A 0 0 D) 0 (Sum.inl i) (Sum.inl j) =
      fromBlocks (HPow.hPow (β := ℕ) A 0) 0 0 (HPow.hPow (β := ℕ) D 0) (Sum.inl i) (Sum.inl j)
zero₁ :
  ∀ (i : n) (j : m),
    HPow.hPow (β := ℕ) (fromBlocks A 0 0 D) 0 (Sum.inl i) (Sum.inr j) =
      fromBlocks (HPow.hPow (β := ℕ) A 0) 0 0 (HPow.hPow (β := ℕ) D 0) (Sum.inl i) (Sum.inr j)
zero₂ :
  ∀ (i : m) (j : n),
    HPow.hPow (β := ℕ) (fromBlocks A 0 0 D) 0 (Sum.inr i) (Sum.inl j) =
      fromBlocks (HPow.hPow (β := ℕ) A 0) 0 0 (HPow.hPow (β := ℕ) D 0) (Sum.inr i) (Sum.inl j)
zero₃ :
  ∀ (i j : m),
    HPow.hPow (β := ℕ) (fromBlocks A 0 0 D) 0 (Sum.inr i) (Sum.inr j) =
      fromBlocks (HPow.hPow (β := ℕ) A 0) 0 0 (HPow.hPow (β := ℕ) D 0) (Sum.inr i) (Sum.inr j)
⊢ HPow.hPow (β := ℕ) (fromBlocks A 0 0 D) 0 = fromBlocks (HPow.hPow (β := ℕ) A 0) 0 0 (HPow.hPow (β := ℕ) D 0)

Tactic:
ext (i | i) (j | j)
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
α : Type u_12
inst : Semiring α
inst_1 : Fintype n
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : DecidableEq m
A : Matrix n n α
D : Matrix m m α
i j : n
⊢ HPow.hPow (β := ℕ) (fromBlocks A 0 0 D) 0 (Sum.inl i) (Sum.inl j) =
    fromBlocks (HPow.hPow (β := ℕ) A 0) 0 0 (HPow.hPow (β := ℕ) D 0) (Sum.inl i) (Sum.inl j)

Tactic:
simp [one_apply]

Premises used: Matrix.one_apply
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
α : Type u_12
inst : Semiring α
inst_1 : Fintype n
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : DecidableEq m
A : Matrix n n α
D : Matrix m m α
i : n
j : m
⊢ HPow.hPow (β := ℕ) (fromBlocks A 0 0 D) 0 (Sum.inl i) (Sum.inr j) =
    fromBlocks (HPow.hPow (β := ℕ) A 0) 0 0 (HPow.hPow (β := ℕ) D 0) (Sum.inl i) (Sum.inr j)

Tactic:
simp [one_apply]

Premises used: Matrix.one_apply
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
α : Type u_12
inst : Semiring α
inst_1 : Fintype n
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : DecidableEq m
A : Matrix n n α
D : Matrix m m α
i : m
j : n
⊢ HPow.hPow (β := ℕ) (fromBlocks A 0 0 D) 0 (Sum.inr i) (Sum.inl j) =
    fromBlocks (HPow.hPow (β := ℕ) A 0) 0 0 (HPow.hPow (β := ℕ) D 0) (Sum.inr i) (Sum.inl j)

Tactic:
simp [one_apply]

Premises used: Matrix.one_apply
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
α : Type u_12
inst : Semiring α
inst_1 : Fintype n
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : DecidableEq m
A : Matrix n n α
D : Matrix m m α
i j : m
⊢ HPow.hPow (β := ℕ) (fromBlocks A 0 0 D) 0 (Sum.inr i) (Sum.inr j) =
    fromBlocks (HPow.hPow (β := ℕ) A 0) 0 0 (HPow.hPow (β := ℕ) D 0) (Sum.inr i) (Sum.inr j)

Tactic:
simp [one_apply]

Premises used: Matrix.one_apply
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n_1 : Type u_3
α : Type u_12
inst : Semiring α
inst_1 : Fintype n_1
inst_2 : Fintype m
inst_3 : DecidableEq n_1
inst_4 : DecidableEq m
A : Matrix n_1 n_1 α
D : Matrix m m α
n : ℕ
ih : fromBlocks A 0 0 D ^ n = fromBlocks (A ^ n) 0 0 (D ^ n)
⊢ fromBlocks A 0 0 D ^ (n + 1) = fromBlocks (A ^ (n + 1)) 0 0 (D ^ (n + 1))

Tactic:
simp [ih, pow_succ, fromBlocks_multiply]

Premises used: pow_succ, Matrix.fromBlocks_multiply
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
α : Type u_12
inst : Semiring α
inst_1 : Fintype n
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : DecidableEq m
A : Matrix n n α
D : Matrix m m α
k : ℕ
zero : HPow.hPow (β := ℕ) (fromBlocks A 0 0 D) 0 = fromBlocks (HPow.hPow (β := ℕ) A 0) 0 0 (HPow.hPow (β := ℕ) D 0)
succ :
  ∀ (n_1 : ℕ) (ih : fromBlocks A 0 0 D ^ n_1 = fromBlocks (A ^ n_1) 0 0 (D ^ n_1)),
    fromBlocks A 0 0 D ^ (n_1 + 1) = fromBlocks (A ^ (n_1 + 1)) 0 0 (D ^ (n_1 + 1))
⊢ fromBlocks A 0 0 D ^ k = fromBlocks (A ^ k) 0 0 (D ^ k)

Tactic:
induction k with
  | zero => ext (i | i) (j | j) <;> simp [one_apply]
  | succ n ih =>
    simp [ih, pow_succ, fromBlocks_multiply]

Premises used: Matrix.one_apply, pow_succ, Matrix.fromBlocks_multiply, Matrix.zero
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : Fintype l
inst_1 : Fintype m
inst_2 : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : l ⊕ m → α
h :
  ∀ (i : n ⊕ o),
    (fromBlocks A B C D *ᵥ x) i = Sum.elim (A *ᵥ x ∘ Sum.inl + B *ᵥ x ∘ Sum.inr) (C *ᵥ x ∘ Sum.inl + D *ᵥ x ∘ Sum.inr) i
⊢ fromBlocks A B C D *ᵥ x = Sum.elim (A *ᵥ x ∘ Sum.inl + B *ᵥ x ∘ Sum.inr) (C *ᵥ x ∘ Sum.inl + D *ᵥ x ∘ Sum.inr)

Tactic:
ext i
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : Fintype l
inst_1 : Fintype m
inst_2 : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : l ⊕ m → α
i : n ⊕ o
h :
  ∀ (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)
h₁ :
  ∀ (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)
⊢ (fromBlocks A B C D *ᵥ x) i = Sum.elim (A *ᵥ x ∘ Sum.inl + B *ᵥ x ∘ Sum.inr) (C *ᵥ x ∘ Sum.inl + D *ᵥ x ∘ Sum.inr) i

Tactic:
cases i
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : Fintype l
inst_1 : Fintype m
inst_2 : 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)

Tactic:
simp [mulVec, dotProduct]

Premises used: dotProduct, Matrix.mulVec