awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : DecidableEq o
inst_1 : AddZeroClass α
M N : o → Matrix m n α
i : m × o
j : n × o
a :
  (if i.2 = j.2 then M i.2 i.1 j.1 + N i.2 i.1 j.1 else 0) =
    (if i.2 = j.2 then M i.2 i.1 j.1 else 0) + if i.2 = j.2 then N i.2 i.1 j.1 else 0
⊢ blockDiagonal (M + N) i j = (blockDiagonal M + blockDiagonal N) i j

Tactic:
simp only [blockDiagonal_apply, Pi.add_apply, add_apply]

Premises used: Matrix.add_apply, Pi.add_apply, Matrix.blockDiagonal_apply
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : DecidableEq o
inst_1 : AddZeroClass α
M N : o → Matrix m n α
i : m × o
j : n × o
pos : i.2 = j.2 → M i.2 i.1 j.1 + N i.2 i.1 j.1 = M i.2 i.1 j.1 + N i.2 i.1 j.1
neg : ¬i.2 = j.2 → 0 = HAdd.hAdd (α := α) 0 0
⊢ (if i.2 = j.2 then M i.2 i.1 j.1 + N i.2 i.1 j.1 else 0) =
    (if i.2 = j.2 then M i.2 i.1 j.1 else 0) + if i.2 = j.2 then N i.2 i.1 j.1 else 0

Tactic:
split_ifs
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : DecidableEq o
inst_1 : AddZeroClass α
M N : o → Matrix m n α
i : m × o
j : n × o
h : i.2 = j.2
⊢ M i.2 i.1 j.1 + N i.2 i.1 j.1 = M i.2 i.1 j.1 + N i.2 i.1 j.1

Tactic:
simp
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : DecidableEq o
inst_1 : AddZeroClass α
M N : o → Matrix m n α
i : m × o
j : n × o
h : ¬i.2 = j.2
⊢ 0 = HAdd.hAdd (α := α) 0 0

Tactic:
simp
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : DecidableEq o
inst_1 : AddGroup α
M : o → Matrix m n α
⊢ blockDiagonal (-M) = -blockDiagonal M

Tactic:
map_neg (blockDiagonalAddMonoidHom m n o α) M

Premises used: Matrix.blockDiagonal, Matrix.blockDiagonalAddMonoidHom, map_neg
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : DecidableEq o
inst_1 : AddGroup α
M N : o → Matrix m n α
⊢ blockDiagonal (M - N) = blockDiagonal M - blockDiagonal N

Tactic:
map_sub (blockDiagonalAddMonoidHom m n o α) M N

Premises used: map_sub, Matrix.blockDiagonal, Matrix.blockDiagonalAddMonoidHom
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
inst : DecidableEq o
inst_1 : Fintype n
inst_2 : Fintype o
inst_3 : NonUnitalNonAssocSemiring α
M : o → Matrix m n α
N : o → Matrix n p α
a :
  ∀ (i : m) (k : o) (j : p) (k' : o),
    blockDiagonal (fun (k : o) ↦ M k * N k) (i, k) (j, k') = (blockDiagonal M * blockDiagonal N) (i, k) (j, k')
⊢ (blockDiagonal fun (k : o) ↦ M k * N k) = blockDiagonal M * blockDiagonal N

Tactic:
ext ⟨i, k⟩ ⟨j, k'⟩
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
inst : DecidableEq o
inst_1 : Fintype n
inst_2 : Fintype o
inst_3 : NonUnitalNonAssocSemiring α
M : o → Matrix m n α
N : o → Matrix n p α
i : m
k : o
j : p
k' : o
a :
  Eq.{u_12 + 1} (α := α) (if k = k' then ∑ j_1 : n, M k i j_1 * N k j_1 j else 0)
    (∑ x : n, ∑ x_1 : o, (if k = x_1 then M k i x else 0) * if x_1 = k' then N x_1 x j else 0)
⊢ blockDiagonal (fun (k : o) ↦ M k * N k) (i, k) (j, k') = (blockDiagonal M * blockDiagonal N) (i, k) (j, k')

Tactic:
simp only [blockDiagonal_apply, mul_apply, ← Finset.univ_product_univ, Finset.sum_product]

Premises used: Matrix.mul_apply, Finset.univ_product_univ, Finset.sum_product, Matrix.blockDiagonal_apply
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
inst : DecidableEq o
inst_1 : Fintype n
inst_2 : Fintype o
inst_3 : NonUnitalNonAssocSemiring α
M : o → Matrix m n α
N : o → Matrix n p α
i : m
k : o
j : p
k' : o
pos :
  ∀ (h : k = k'),
    Eq.{u_12 + 1} (α := α) (∑ j_1 : n, M k i j_1 * N k j_1 j)
      (∑ x : n, ∑ x_1 : o, (if k = x_1 then M k i x else 0) * if x_1 = k' then N x_1 x j else 0)
neg :
  ∀ (h : ¬k = k'),
    Eq.{u_12 + 1} (α := α) 0 (∑ x : n, ∑ x_1 : o, (if k = x_1 then M k i x else 0) * if x_1 = k' then N x_1 x j else 0)
⊢ Eq.{u_12 + 1} (α := α) (if k = k' then ∑ j_1 : n, M k i j_1 * N k j_1 j else 0)
    (∑ x : n, ∑ x_1 : o, (if k = x_1 then M k i x else 0) * if x_1 = k' then N x_1 x j else 0)

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
inst : DecidableEq o
inst_1 : Fintype n
inst_2 : Fintype o
inst_3 : NonUnitalNonAssocSemiring α
M : o → Matrix m n α
N : o → Matrix n p α
i : m
k : o
j : p
k' : o
h : k = k'
⊢ Eq.{u_12 + 1} (α := α) (∑ j_1 : n, M k i j_1 * N k j_1 j)
    (∑ x : n, ∑ x_1 : o, (if k = x_1 then M k i x else 0) * if x_1 = k' then N x_1 x j else 0)

Tactic:
simp [h]
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
inst : DecidableEq o
inst_1 : Fintype n
inst_2 : Fintype o
inst_3 : NonUnitalNonAssocSemiring α
M : o → Matrix m n α
N : o → Matrix n p α
i : m
k : o
j : p
k' : o
h : ¬k = k'
⊢ Eq.{u_12 + 1} (α := α) 0 (∑ x : n, ∑ x_1 : o, (if k = x_1 then M k i x else 0) * if x_1 = k' then N x_1 x j else 0)

Tactic:
simp [h]
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
o : Type u_4
α : Type u_12
inst : DecidableEq o
inst_1 : DecidableEq m
inst_2 : Fintype o
inst_3 : Fintype m
inst_4 : Semiring α
M : o → Matrix m m α
n : ℕ
⊢ blockDiagonal (M ^ n) = blockDiagonal M ^ n

Tactic:
map_pow (blockDiagonalRingHom m o α) M n

Premises used: Matrix.blockDiagonal, map_pow, Matrix.blockDiagonalRingHom
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : DecidableEq o
R : Type u_14
inst_1 : Zero α
inst_2 : SMulZeroClass R α
x : R
M : o → Matrix m n α
a : ∀ (i : m × o) (j : n × o), blockDiagonal (x • M) i j = (x • blockDiagonal M) i j
⊢ blockDiagonal (x • M) = x • blockDiagonal M

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : DecidableEq o
R : Type u_14
inst_1 : Zero α
inst_2 : SMulZeroClass R α
x : R
M : o → Matrix m n α
i : m × o
j : n × o
a : (if i.2 = j.2 then x • M i.2 i.1 j.1 else 0) = x • if i.2 = j.2 then M i.2 i.1 j.1 else 0
⊢ blockDiagonal (x • M) i j = (x • blockDiagonal M) i j

Tactic:
simp only [blockDiagonal_apply, Pi.smul_apply, smul_apply]

Premises used: Matrix.smul_apply, Matrix.blockDiagonal_apply, Pi.smul_apply
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : DecidableEq o
R : Type u_14
inst_1 : Zero α
inst_2 : SMulZeroClass R α
x : R
M : o → Matrix m n α
i : m × o
j : n × o
pos : i.2 = j.2 → x • M i.2 i.1 j.1 = x • M i.2 i.1 j.1
neg : ¬i.2 = j.2 → 0 = HSMul.hSMul (β := α) x 0
⊢ (if i.2 = j.2 then x • M i.2 i.1 j.1 else 0) = x • if i.2 = j.2 then M i.2 i.1 j.1 else 0

Tactic:
split_ifs
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : DecidableEq o
R : Type u_14
inst_1 : Zero α
inst_2 : SMulZeroClass R α
x : R
M : o → Matrix m n α
i : m × o
j : n × o
h : i.2 = j.2
⊢ x • M i.2 i.1 j.1 = x • M i.2 i.1 j.1

Tactic:
simp
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : DecidableEq o
R : Type u_14
inst_1 : Zero α
inst_2 : SMulZeroClass R α
x : R
M : o → Matrix m n α
i : m × o
j : n × o
h : ¬i.2 = j.2
⊢ 0 = HSMul.hSMul (β := α) x 0

Tactic:
simp
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (m × o) (n × o) α
k : o
i : m
j : n
⊢ M.blockDiag k i j = M (i, k) (j, k)

Tactic:
rfl

Premises used: Matrix.blockDiag, rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
β : Type u_13
M : Matrix (m × o) (n × o) α
f : α → β
⊢ (M.map f).blockDiag = fun (k : o) ↦ (M.blockDiag k).map f

Tactic:
rfl

Premises used: Matrix.blockDiag, Matrix.map, rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (m × o) (n × o) α
k : o
⊢ Mᵀ.blockDiag k = (M.blockDiag k)ᵀ

Tactic:
ext fun _ _ => rfl

Premises used: Matrix.ext, rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_14
inst : Star α
M : Matrix (m × o) (n × o) α
k : o
⊢ Mᴴ.blockDiag k = (M.blockDiag k)ᴴ

Tactic:
ext fun _ _ => rfl

Premises used: Matrix.ext, rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : Zero α
⊢ Eq (α := (k : o) → Matrix m n α) (blockDiag 0) 0

Tactic:
rfl

Premises used: Matrix.blockDiag, rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
o : Type u_4
α : Type u_12
inst : Zero α
inst_1 : DecidableEq o
inst_2 : DecidableEq m
d : m × o → α
k : o
i j : m
inl : (diagonal d).blockDiag k i i = diagonal (fun (i : m) ↦ d (i, k)) i i
inr : ∀ (hij : i ≠ j), (diagonal d).blockDiag k i j = diagonal (fun (i : m) ↦ d (i, k)) i j
⊢ (diagonal d).blockDiag k i j = diagonal (fun (i : m) ↦ d (i, k)) i j

Tactic:
obtain rfl | hij := Decidable.eq_or_ne i j

Premises used: Decidable.eq_or_ne, rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
o : Type u_4
α : Type u_12
inst : Zero α
inst_1 : DecidableEq o
inst_2 : DecidableEq m
d : m × o → α
k : o
i : m
inl : diagonal d (i, k) (i, k) = diagonal (fun (i : m) ↦ d (i, k)) i i
inl₁ : d (i, k) = diagonal (fun (i : m) ↦ d (i, k)) i i
inl₂ inl₃ : d (i, k) = d (i, k)
⊢ (diagonal d).blockDiag k i i = diagonal (fun (i : m) ↦ d (i, k)) i i

Tactic:
rw [blockDiag_apply, diagonal_apply_eq, diagonal_apply_eq]

Premises used: Matrix.diagonal_apply_eq, Matrix.blockDiag_apply
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
o : Type u_4
α : Type u_12
inst : Zero α
inst_1 : DecidableEq o
inst_2 : DecidableEq m
d : m × o → α
k : o
i j : m
hij : i ≠ j
rw : (i, k) = (j, k) → i = j
⊢ (diagonal d).blockDiag k i j = diagonal (fun (i : m) ↦ d (i, k)) i j

Tactic:
rw [blockDiag_apply, diagonal_apply_ne _ hij, diagonal_apply_ne _ (mt _ hij)]

Premises used: mt, Matrix.blockDiag_apply, Matrix.diagonal_apply_ne
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
o : Type u_4
α : Type u_12
inst : Zero α
inst_1 : DecidableEq o
inst_2 : DecidableEq m
d : m × o → α
k : o
i j : m
hij : i ≠ j
⊢ (i, k) = (j, k) → i = j

Tactic:
Prod.fst_eq_iff.mpr

Premises used: Iff.mpr, Prod.fst_eq_iff
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
o : Type u_4
α : Type u_12
inst : Zero α
inst_1 : DecidableEq o
inst_2 : DecidableEq m
d : m × o → α
k : o
i j : m
hij : i ≠ j
⊢ (i, k) = (j, k) → i = j

Tactic:
exact Prod.fst_eq_iff.mpr

Premises used: Iff.mpr, Prod.fst_eq_iff
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : Zero α
inst_1 : DecidableEq o
M : o → Matrix m n α
⊢ (blockDiagonal M).blockDiag = M

Tactic:
funext fun _ => ext fun i j => blockDiagonal_apply_eq M i j _

Premises used: funext, Matrix.blockDiagonal_apply_eq, Matrix.ext
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : Zero α
inst_1 : DecidableEq o
⊢ Function.Injective (α := o → Matrix m n α) blockDiagonal

Tactic:
Function.LeftInverse.injective blockDiag_blockDiagonal

Premises used: Function.LeftInverse.injective, Matrix.blockDiag_blockDiagonal
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : Zero α
inst_1 : DecidableEq o
M N : o → Matrix m n α
⊢ blockDiagonal M = blockDiagonal N ↔ M = N

Tactic:
blockDiagonal_injective.eq_iff

Premises used: Matrix.blockDiagonal_injective, Function.Injective.eq_iff
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
o : Type u_4
α : Type u_12
inst : Zero α
inst_1 : DecidableEq o
inst_2 : DecidableEq m
inst_3 : One α
⊢ Eq (α := (k : o) → Matrix m m α) (blockDiag 1) 1

Tactic:
funext <| blockDiag_diagonal _

Premises used: Matrix.blockDiag_diagonal, funext
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : Add α
M N : Matrix (m × o) (n × o) α
⊢ (M + N).blockDiag = M.blockDiag + N.blockDiag

Tactic:
rfl

Premises used: Matrix.blockDiag, rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : AddGroup α
M : Matrix (m × o) (n × o) α
⊢ (-M).blockDiag = -M.blockDiag

Tactic:
map_neg (blockDiagAddMonoidHom m n o α) M

Premises used: Matrix.blockDiag, map_neg, Matrix.blockDiagAddMonoidHom
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : AddGroup α
M N : Matrix (m × o) (n × o) α
⊢ (M - N).blockDiag = M.blockDiag - N.blockDiag

Tactic:
map_sub (blockDiagAddMonoidHom m n o α) M N

Premises used: map_sub, Matrix.blockDiag, Matrix.blockDiagAddMonoidHom
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
R : Type u_14
inst : SMul R α
x : R
M : Matrix (m × o) (n × o) α
⊢ (x • M).blockDiag = x • M.blockDiag

Tactic:
rfl

Premises used: Matrix.blockDiag, rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst : DecidableEq o
inst_1 : Zero α
M : (i : o) → Matrix.{u_7, u_8, u_12} (m' i) (n' i) α
k : o
i : m' k
k' : o
j : n' k'
⊢ blockDiagonal' (m' := m') (n' := n') M (Sigma.mk (β := fun (i : o) ↦ m' i) k i)
      (Sigma.mk (β := fun (i : o) ↦ n' i) k' j) =
    if h : k = k' then M k i (cast ⋯ j) else 0

Tactic:
rfl

Premises used: dite, Matrix.blockDiagonal', rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : DecidableEq o
inst_1 : Zero α
M : o → Matrix m n α
k k' : o
i : m
j : n
⊢ blockDiagonal M (i, k) (j, k') =
    blockDiagonal' (m' := fun (i : o) ↦ m) (n' := fun (i : o) ↦ n) M (Sigma.mk (β := fun (i : o) ↦ m) k i)
      (Sigma.mk (β := fun (i : o) ↦ n) k' j)

Tactic:
rfl

Premises used: cast, dite, Matrix.blockDiagonal', rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : DecidableEq o
inst_1 : Zero α
M : o → Matrix m n α
⊢ (blockDiagonal' (m' := fun (i : o) ↦ m) (n' := fun (i : o) ↦ n) M).submatrix (Prod.toSigma ∘ Prod.swap)
      (Prod.toSigma ∘ Prod.swap) =
    blockDiagonal M

Tactic:
Matrix.ext fun ⟨_, _⟩ ⟨_, _⟩ => rfl

Premises used: Matrix.submatrix, Prod.toSigma, Matrix.blockDiagonal, Function.comp, Prod.mk, Prod.swap, Matrix.blockDiagonal', Eq, _private.0.Matrix.blockDiagonal'_submatrix_eq_blockDiagonal.match_1, Matrix.ext, rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst : DecidableEq o
inst_1 : Zero α
M : (i : o) → Matrix.{u_7, u_8, u_12} (m' i) (n' i) α
ik : (i : o) × m' i
jk : (i : o) × n' i
⊢ blockDiagonal' (m' := m') (n' := n') M ik jk =
    if h : ik.fst (β := fun (i : o) ↦ m' i) = jk.fst (β := fun (i : o) ↦ n' i) then
      M (ik.fst (β := fun (i : o) ↦ m' i)) (ik.snd (β := fun (i : o) ↦ m' i))
        (cast ⋯ (jk.snd (β := fun (i : o) ↦ n' i)))
    else 0

Tactic:
rfl

Premises used: dite, Matrix.blockDiagonal', rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst : DecidableEq o
inst_1 : Zero α
M : (i : o) → Matrix.{u_7, u_8, u_12} (m' i) (n' i) α
k : o
i : m' k
j : n' k
⊢ blockDiagonal' (m' := m') (n' := n') M (Sigma.mk (β := fun (i : o) ↦ m' i) k i)
      (Sigma.mk (β := fun (i : o) ↦ n' i) k j) =
    M k i j

Tactic:
dif_pos rfl

Premises used: cast, dif_pos, dite, Matrix.blockDiagonal', rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst : DecidableEq o
inst_1 : Zero α
M : (i : o) → Matrix.{u_7, u_8, u_12} (m' i) (n' i) α
k k' : o
i : m' k
j : n' k'
h : k ≠ k'
⊢ blockDiagonal' (m' := m') (n' := n') M (Sigma.mk (β := fun (i : o) ↦ m' i) k i)
      (Sigma.mk (β := fun (i : o) ↦ n' i) k' j) =
    0

Tactic:
dif_neg h

Premises used: dif_neg, dite, Matrix.blockDiagonal'
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
β : Type u_13
inst : DecidableEq o
inst_1 : Zero α
inst_2 : Zero β
M : (i : o) → Matrix.{u_7, u_8, u_12} (m' i) (n' i) α
f : α → β
hf : f 0 = 0
a :
  ∀ (i : (i : o) × m' i) (j : (i : o) × n' i),
    (blockDiagonal' (m' := m') (n' := n') M).map f i j =
      blockDiagonal' (m' := m') (n' := n') (fun (k : o) ↦ (M k).map f) i j
⊢ (blockDiagonal' (m' := m') (n' := n') M).map f = blockDiagonal' (m' := m') (n' := n') fun (k : o) ↦ (M k).map f

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
β : Type u_13
inst : DecidableEq o
inst_1 : Zero α
inst_2 : Zero β
M : (i : o) → Matrix.{u_7, u_8, u_12} (m' i) (n' i) α
f : α → β
hf : f 0 = 0
i : (i : o) × m' i
j : (i : o) × n' i
a :
  f
      (if h : i.fst (β := fun (i : o) ↦ m' i) = j.fst (β := fun (i : o) ↦ n' i) then
        M (i.fst (β := fun (i : o) ↦ m' i)) (i.snd (β := fun (i : o) ↦ m' i)) (cast ⋯ (j.snd (β := fun (i : o) ↦ n' i)))
      else 0) =
    if h : i.fst (β := fun (i : o) ↦ m' i) = j.fst (β := fun (i : o) ↦ n' i) then
      f
        (M (i.fst (β := fun (i : o) ↦ m' i)) (i.snd (β := fun (i : o) ↦ m' i))
          (cast ⋯ (j.snd (β := fun (i : o) ↦ n' i))))
    else 0
⊢ (blockDiagonal' (m' := m') (n' := n') M).map f i j =
    blockDiagonal' (m' := m') (n' := n') (fun (k : o) ↦ (M k).map f) i j

Tactic:
simp only [map_apply, blockDiagonal'_apply]

Premises used: Matrix.blockDiagonal'_apply, Matrix.map_apply
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
β : Type u_13
inst : DecidableEq o
inst_1 : Zero α
inst_2 : Zero β
M : (i : o) → Matrix.{u_7, u_8, u_12} (m' i) (n' i) α
f : α → β
hf : f 0 = 0
i : (i : o) × m' i
j : (i : o) × n' i
a :
  Eq.{u_13 + 1} (α := β)
    (if h : i.fst (β := fun (i : o) ↦ m' i) = j.fst (β := fun (i : o) ↦ n' i) then
      f
        (M (i.fst (β := fun (i : o) ↦ m' i)) (i.snd (β := fun (i : o) ↦ m' i))
          (cast ⋯ (j.snd (β := fun (i : o) ↦ n' i))))
    else f 0)
    (if h : i.fst (β := fun (i : o) ↦ m' i) = j.fst (β := fun (i : o) ↦ n' i) then
      f
        (M (i.fst (β := fun (i : o) ↦ m' i)) (i.snd (β := fun (i : o) ↦ m' i))
          (cast ⋯ (j.snd (β := fun (i : o) ↦ n' i))))
    else 0)
a₁ a₂ :
  Eq.{u_13 + 1} (α := β)
    (if h : i.fst (β := fun (i : o) ↦ m' i) = j.fst (β := fun (i : o) ↦ n' i) then
      f
        (M (i.fst (β := fun (i : o) ↦ m' i)) (i.snd (β := fun (i : o) ↦ m' i))
          (cast ⋯ (j.snd (β := fun (i : o) ↦ n' i))))
    else 0)
    (if h : i.fst (β := fun (i : o) ↦ m' i) = j.fst (β := fun (i : o) ↦ n' i) then
      f
        (M (i.fst (β := fun (i : o) ↦ m' i)) (i.snd (β := fun (i : o) ↦ m' i))
          (cast ⋯ (j.snd (β := fun (i : o) ↦ n' i))))
    else 0)
⊢ f
      (if h : i.fst (β := fun (i : o) ↦ m' i) = j.fst (β := fun (i : o) ↦ n' i) then
        M (i.fst (β := fun (i : o) ↦ m' i)) (i.snd (β := fun (i : o) ↦ m' i)) (cast ⋯ (j.snd (β := fun (i : o) ↦ n' i)))
      else 0) =
    if h : i.fst (β := fun (i : o) ↦ m' i) = j.fst (β := fun (i : o) ↦ n' i) then
      f
        (M (i.fst (β := fun (i : o) ↦ m' i)) (i.snd (β := fun (i : o) ↦ m' i))
          (cast ⋯ (j.snd (β := fun (i : o) ↦ n' i))))
    else 0

Tactic:
rw [apply_dite f, hf]

Premises used: apply_dite
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst : DecidableEq o
inst_1 : Zero α
M : (i : o) → Matrix.{u_7, u_8, u_12} (m' i) (n' i) α
a :
  ∀ (ii : o) (ix : n' ii) (ji : o) (jx : m' ji),
    (blockDiagonal' (m' := m') (n' := n') M)ᵀ (Sigma.mk (β := fun (i : o) ↦ n' i) ii ix)
        (Sigma.mk (β := fun (i : o) ↦ m' i) ji jx) =
      blockDiagonal' (m' := n') (n' := m') (fun (k : o) ↦ (M k)ᵀ) (Sigma.mk (β := fun (i : o) ↦ n' i) ii ix)
        (Sigma.mk (β := fun (i : o) ↦ m' i) ji jx)
⊢ (blockDiagonal' (m' := m') (n' := n') M)ᵀ = blockDiagonal' (m' := n') (n' := m') fun (k : o) ↦ (M k)ᵀ

Tactic:
ext ⟨ii, ix⟩ ⟨ji, jx⟩
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst : DecidableEq o
inst_1 : Zero α
M : (i : o) → Matrix.{u_7, u_8, u_12} (m' i) (n' i) α
ii : o
ix : n' ii
ji : o
jx : m' ji
a :
  Eq.{u_12 + 1} (α := α) (if h : ji = ii then M ji jx (cast ⋯ ix) else 0)
    (if h : ii = ji then M ii (cast ⋯ jx) ix else 0)
⊢ (blockDiagonal' (m' := m') (n' := n') M)ᵀ (Sigma.mk (β := fun (i : o) ↦ n' i) ii ix)
      (Sigma.mk (β := fun (i : o) ↦ m' i) ji jx) =
    blockDiagonal' (m' := n') (n' := m') (fun (k : o) ↦ (M k)ᵀ) (Sigma.mk (β := fun (i : o) ↦ n' i) ii ix)
      (Sigma.mk (β := fun (i : o) ↦ m' i) ji jx)

Tactic:
simp only [transpose_apply, blockDiagonal'_apply]

Premises used: Matrix.blockDiagonal'_apply, Matrix.transpose_apply
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst : DecidableEq o
inst_1 : Zero α
M : (i : o) → Matrix.{u_7, u_8, u_12} (m' i) (n' i) α
ii : o
ix : n' ii
ji : o
jx : m' ji
pos : ∀ (h : ji = ii) (h_1 : ii = ji), M ji jx (cast ⋯ ix) = M ii (cast ⋯ jx) ix
neg : ∀ (h : ji = ii), ¬ii = ji → M ji jx (cast ⋯ ix) = 0
pos₁ : ¬ji = ii → ∀ (h : ii = ji), 0 = M ii (cast ⋯ jx) ix
neg₁ : ¬ji = ii → ¬ii = ji → Eq.{u_12 + 1} (α := α) 0 0
⊢ Eq.{u_12 + 1} (α := α) (if h : ji = ii then M ji jx (cast ⋯ ix) else 0)
    (if h : ii = ji then M ii (cast ⋯ jx) ix else 0)

Tactic:
split_ifs
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst : DecidableEq o
inst_1 : Zero α
M : (i : o) → Matrix.{u_7, u_8, u_12} (m' i) (n' i) α
ii : o
ix : n' ii
ji : o
jx : m' ji
h : ji = ii
h_1 : ii = ji
⊢ M ji jx (cast ⋯ ix) = M ii (cast ⋯ jx) ix

Tactic:
grind
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst : DecidableEq o
inst_1 : Zero α
M : (i : o) → Matrix.{u_7, u_8, u_12} (m' i) (n' i) α
ii : o
ix : n' ii
ji : o
jx : m' ji
h : ji = ii
h_1 : ¬ii = ji
⊢ M ji jx (cast ⋯ ix) = 0

Tactic:
grind
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst : DecidableEq o
inst_1 : Zero α
M : (i : o) → Matrix.{u_7, u_8, u_12} (m' i) (n' i) α
ii : o
ix : n' ii
ji : o
jx : m' ji
h : ¬ji = ii
h_1 : ii = ji
⊢ 0 = M ii (cast ⋯ jx) ix

Tactic:
grind
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst : DecidableEq o
inst_1 : Zero α
M : (i : o) → Matrix.{u_7, u_8, u_12} (m' i) (n' i) α
ii : o
ix : n' ii
ji : o
jx : m' ji
h : ¬ji = ii
h_1 : ¬ii = ji
⊢ Eq.{u_12 + 1} (α := α) 0 0

Tactic:
grind
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
inst : DecidableEq o
α : Type u_14
inst_1 : AddMonoid α
inst_2 : StarAddMonoid α
M : (i : o) → Matrix.{u_7, u_8, u_14} (m' i) (n' i) α
simp :
  Eq (α := Matrix ((i : o) × n' i) ((i : o) × m' i) α)
    (map (blockDiagonal' (m' := n') (n' := m') fun (k : o) ↦ (M k)ᵀ) star)
    (blockDiagonal' (m' := n') (n' := m') fun (k : o) ↦ (M k)ᵀ.map star)
⊢ (blockDiagonal' (m' := m') (n' := n') M)ᴴ = blockDiagonal' (m' := n') (n' := m') fun (k : o) ↦ (M k)ᴴ

Tactic:
simp only [conjTranspose, blockDiagonal'_transpose]

Premises used: Matrix.blockDiagonal'_transpose, Matrix.conjTranspose
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
inst : DecidableEq o
α : Type u_14
inst_1 : AddMonoid α
inst_2 : StarAddMonoid α
M : (i : o) → Matrix.{u_7, u_8, u_14} (m' i) (n' i) α
⊢ Eq (α := Matrix ((i : o) × n' i) ((i : o) × m' i) α)
    (map (blockDiagonal' (m' := n') (n' := m') fun (k : o) ↦ (M k)ᵀ) star)
    (blockDiagonal' (m' := n') (n' := m') fun (k : o) ↦ (M k)ᵀ.map star)

Tactic:
blockDiagonal'_map _ star (star_zero α)

Premises used: Matrix.blockDiagonal'_map, star_zero, Star.star
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
inst : DecidableEq o
α : Type u_14
inst_1 : AddMonoid α
inst_2 : StarAddMonoid α
M : (i : o) → Matrix.{u_7, u_8, u_14} (m' i) (n' i) α
⊢ Eq (α := Matrix ((i : o) × n' i) ((i : o) × m' i) α)
    (map (blockDiagonal' (m' := n') (n' := m') fun (k : o) ↦ (M k)ᵀ) star)
    (blockDiagonal' (m' := n') (n' := m') fun (k : o) ↦ (M k)ᵀ.map star)

Tactic:
exact blockDiagonal'_map _ star (star_zero α)

Premises used: Matrix.blockDiagonal'_map, star_zero, Star.star