awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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)
⊢ (-fromBlocks A B C D) (Sum.inr val) j = fromBlocks (-A) (-B) (-C) (-D) (Sum.inr val) j
have 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)
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : Zero α
⊢ Eq (α := Matrix (n ⊕ o) (l ⊕ m) α) (fromBlocks 0 0 0 0) 0
have a : ∀ (i : n ⊕ o) (j : l ⊕ m), Eq.{u_12 + 1} (α := α) (fromBlocks 0 0 0 0 i j) (0 i j)
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ Eq.{u_12 + 1} (α := α) (fromBlocks 0 0 0 0 i j) (0 i j)
have 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)
Tactic: rcases i with ⟨⟩
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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)
⊢ Eq.{u_12 + 1} (α := α) (fromBlocks 0 0 0 0 i j) (0 i j)
have 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)
Tactic: rcases i with ⟨⟩
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ 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)
have 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))
Tactic: rcases j with ⟨⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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))
⊢ 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)
have 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))
Tactic: rcases j with ⟨⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ 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)
have 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))
Tactic: rcases j with ⟨⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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))
⊢ 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)
have 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))
Tactic: rcases j with ⟨⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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 α
⊢ fromBlocks A B C D + fromBlocks A' B' C' D' = fromBlocks (A + A') (B + B') (C + C') (D + D')
have 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
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ (fromBlocks A B C D + fromBlocks A' B' C' D') i j = fromBlocks (A + A') (B + B') (C + C') (D + D') i j
have 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
Tactic: rcases i with ⟨⟩
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ (fromBlocks A B C D + fromBlocks A' B' C' D') i j = fromBlocks (A + A') (B + B') (C + C') (D + D') i j
have 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
Tactic: rcases i with ⟨⟩
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ (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
have 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)
Tactic: rcases j with ⟨⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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)
⊢ (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
have 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)
Tactic: rcases j with ⟨⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ (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
have 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)
Tactic: rcases j with ⟨⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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)
⊢ (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
have 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)
Tactic: rcases j with ⟨⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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 α
⊢ 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')
have 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
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ (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
have 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
Tactic: rcases i with ⟨⟩
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ (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
have 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
Tactic: rcases i with ⟨⟩
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ (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
have 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)
Tactic: rcases j with ⟨⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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)
⊢ (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
have 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)
Tactic: rcases j with ⟨⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ (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
have 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)
Tactic: rcases j with ⟨⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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)
⊢ (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
have 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)
Tactic: rcases j with ⟨⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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 α
⊢ HPow.hPow (β := ℕ) (fromBlocks A 0 0 D) 0 = fromBlocks (HPow.hPow (β := ℕ) A 0) 0 0 (HPow.hPow (β := ℕ) D 0)
have 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)
Tactic: ext (i | i) (j | j)
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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)
⊢ HPow.hPow (β := ℕ) (fromBlocks A 0 0 D) 0 = fromBlocks (HPow.hPow (β := ℕ) A 0) 0 0 (HPow.hPow (β := ℕ) D 0)
have 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)
Tactic: ext (i | i) (j | j)
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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)
⊢ HPow.hPow (β := ℕ) (fromBlocks A 0 0 D) 0 = fromBlocks (HPow.hPow (β := ℕ) A 0) 0 0 (HPow.hPow (β := ℕ) D 0)
have 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)
Tactic: ext (i | i) (j | j)
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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)
⊢ HPow.hPow (β := ℕ) (fromBlocks A 0 0 D) 0 = fromBlocks (HPow.hPow (β := ℕ) A 0) 0 0 (HPow.hPow (β := ℕ) D 0)
have 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)
Tactic: ext (i | i) (j | j)
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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 : ℕ
⊢ fromBlocks A 0 0 D ^ k = fromBlocks (A ^ k) 0 0 (D ^ k)
have zero : HPow.hPow (β := ℕ) (fromBlocks A 0 0 D) 0 = fromBlocks (HPow.hPow (β := ℕ) A 0) 0 0 (HPow.hPow (β := ℕ) D 0)
Tactic: induction k with
  | zero => ext (i | i) (j | j) <;> simp [one_apply]
  | succ n ih =>
    simp [ih, pow_succ, fromBlocks_multiply]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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)
⊢ fromBlocks A 0 0 D ^ k = fromBlocks (A ^ k) 0 0 (D ^ k)
have 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))
Tactic: induction k with
  | zero => ext (i | i) (j | j) <;> simp [one_apply]
  | succ n ih =>
    simp [ih, pow_succ, fromBlocks_multiply]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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 → α
⊢ fromBlocks A B C D *ᵥ x = Sum.elim (A *ᵥ x ∘ Sum.inl + B *ᵥ x ∘ Sum.inr) (C *ᵥ x ∘ Sum.inl + D *ᵥ x ∘ Sum.inr)
have 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
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ (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
have 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)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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)
⊢ (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
have 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)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : Fintype n
inst_1 : Fintype o
inst_2 : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : n ⊕ o → α
⊢ x ᵥ* fromBlocks A B C D = Sum.elim (x ∘ Sum.inl ᵥ* A + x ∘ Sum.inr ᵥ* C) (x ∘ Sum.inl ᵥ* B + x ∘ Sum.inr ᵥ* D)
have h : ∀ (i : l ⊕ m),
  (x ᵥ* fromBlocks A B C D) i = Sum.elim (x ∘ Sum.inl ᵥ* A + x ∘ Sum.inr ᵥ* C) (x ∘ Sum.inl ᵥ* B + x ∘ Sum.inr ᵥ* D) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : Fintype n
inst_1 : Fintype o
inst_2 : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : n ⊕ o → α
i : l ⊕ m
⊢ (x ᵥ* fromBlocks A B C D) i = Sum.elim (x ∘ Sum.inl ᵥ* A + x ∘ Sum.inr ᵥ* C) (x ∘ Sum.inl ᵥ* B + x ∘ Sum.inr ᵥ* D) i
have h : ∀ (val : l),
  (x ᵥ* fromBlocks A B C D) (Sum.inl val) =
    Sum.elim (x ∘ Sum.inl ᵥ* A + x ∘ Sum.inr ᵥ* C) (x ∘ Sum.inl ᵥ* B + x ∘ Sum.inr ᵥ* D) (Sum.inl val)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : Fintype n
inst_1 : Fintype o
inst_2 : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : n ⊕ o → α
i : l ⊕ m
h :
  ∀ (val : l),
    (x ᵥ* fromBlocks A B C D) (Sum.inl val) =
      Sum.elim (x ∘ Sum.inl ᵥ* A + x ∘ Sum.inr ᵥ* C) (x ∘ Sum.inl ᵥ* B + x ∘ Sum.inr ᵥ* D) (Sum.inl val)
⊢ (x ᵥ* fromBlocks A B C D) i = Sum.elim (x ∘ Sum.inl ᵥ* A + x ∘ Sum.inr ᵥ* C) (x ∘ Sum.inl ᵥ* B + x ∘ Sum.inr ᵥ* D) i
have h₁ : ∀ (val : m),
  (x ᵥ* fromBlocks A B C D) (Sum.inr val) =
    Sum.elim (x ∘ Sum.inl ᵥ* A + x ∘ Sum.inr ᵥ* C) (x ∘ Sum.inl ᵥ* B + x ∘ Sum.inr ᵥ* D) (Sum.inr val)
Tactic: cases i
Cleared hypotheses: i