awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 α
a :
  ∀ (i : (i : o) × m' i) (j : (i : o) × n' i),
    Eq.{u_12 + 1} (α := α) (blockDiagonal' (m' := m') (n' := n') 0 i j) (0 i j)
⊢ Eq (α := Matrix ((i : o) × m' i) ((i : o) × n' i) α) (blockDiagonal' (m' := m') (n' := n') 0) 0

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
inst : DecidableEq o
inst_1 : Zero α
i : (i : o) × m' i
j : (i : o) × n' i
⊢ Eq.{u_12 + 1} (α := α) (blockDiagonal' (m' := m') (n' := n') 0 i j) (0 i j)

Tactic:
simp [blockDiagonal'_apply]

Premises used: Matrix.blockDiagonal'_apply
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst : DecidableEq o
inst_1 : Zero α
inst_2 : (i : o) → DecidableEq (m' i)
d : (i : o) → m' i → α
a :
  ∀ (i : o) (k : m' i) (j : o) (k' : m' j),
    Eq.{u_12 + 1} (α := α)
      (blockDiagonal' (m' := m') (n' := m') (fun (k : o) ↦ diagonal (d k)) (Sigma.mk (β := fun (i : o) ↦ m' i) i k)
        (Sigma.mk (β := fun (i : o) ↦ m' i) j k'))
      (diagonal (fun (ik : (i : o) × m' i) ↦ d (ik.fst (β := fun (i : o) ↦ m' i)) (ik.snd (β := fun (i : o) ↦ m' i)))
        (Sigma.mk (β := fun (i : o) ↦ m' i) i k) (Sigma.mk (β := fun (i : o) ↦ m' i) j k'))
⊢ Eq (α := Matrix ((i : o) × m' i) ((i : o) × m' i) α)
    (blockDiagonal' (m' := m') (n' := m') fun (k : o) ↦ diagonal (d k))
    (diagonal fun (ik : (i : o) × m' i) ↦ d (ik.fst (β := fun (i : o) ↦ m' i)) (ik.snd (β := fun (i : o) ↦ m' i)))

Tactic:
ext ⟨i, k⟩ ⟨j, k'⟩
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst : DecidableEq o
inst_1 : Zero α
inst_2 : (i : o) → DecidableEq (m' i)
d : (i : o) → m' i → α
i : o
k : m' i
j : o
k' : m' j
a :
  Eq.{u_12 + 1} (α := α)
    (if h : i = j then
        (of : (a : m' i → m' i → α) → Matrix (m' i) (m' i) α) (fun (i_1 j : m' i) ↦ if i_1 = j then d i i_1 else 0) k
          (cast ⋯ k')
      else 0 :
      α)
    ((of : (a : (i : o) × m' i → (i : o) × m' i → α) → Matrix ((i : o) × m' i) ((i : o) × m' i) α)
        (fun (i j : (i : o) × m' i) ↦
          if i = j then d (i.fst (β := fun (i : o) ↦ m' i)) (i.snd (β := fun (i : o) ↦ m' i)) else 0)
        (Sigma.mk (β := fun (i : o) ↦ m' i) i k) (Sigma.mk (β := fun (i : o) ↦ m' i) j k') :
      α)
⊢ Eq.{u_12 + 1} (α := α)
    (blockDiagonal' (m' := m') (n' := m') (fun (k : o) ↦ diagonal (d k)) (Sigma.mk (β := fun (i : o) ↦ m' i) i k)
      (Sigma.mk (β := fun (i : o) ↦ m' i) j k'))
    (diagonal (fun (ik : (i : o) × m' i) ↦ d (ik.fst (β := fun (i : o) ↦ m' i)) (ik.snd (β := fun (i : o) ↦ m' i)))
      (Sigma.mk (β := fun (i : o) ↦ m' i) i k) (Sigma.mk (β := fun (i : o) ↦ m' i) j k'))

Tactic:
simp only [blockDiagonal'_apply, diagonal]

Premises used: Matrix.blockDiagonal'_apply, Matrix.diagonal
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst : DecidableEq o
inst_1 : Zero α
inst_2 : (i : o) → DecidableEq (m' i)
d : (i : o) → m' i → α
i : o
k : m' i
j : o
k' : m' j
a :
  ∀ (k' : m' i),
    Eq.{u_12 + 1} (α := α)
      (if h : i = i then
          (of : (a : m' i → m' i → α) → Matrix (m' i) (m' i) α) (fun (i_1 j : m' i) ↦ if i_1 = j then d i i_1 else 0) k
            (cast ⋯ k')
        else 0 :
        α)
      ((of : (a : (i : o) × m' i → (i : o) × m' i → α) → Matrix ((i : o) × m' i) ((i : o) × m' i) α)
          (fun (i j : (i : o) × m' i) ↦
            if i = j then d (i.fst (β := fun (i : o) ↦ m' i)) (i.snd (β := fun (i : o) ↦ m' i)) else 0)
          (Sigma.mk (β := fun (i : o) ↦ m' i) i k) (Sigma.mk (β := fun (i : o) ↦ m' i) i k') :
        α)
a₁ :
  ∀ (hij : i ≠ j),
    Eq.{u_12 + 1} (α := α)
      (if h : i = j then
          (of : (a : m' i → m' i → α) → Matrix (m' i) (m' i) α) (fun (i_1 j : m' i) ↦ if i_1 = j then d i i_1 else 0) k
            (cast ⋯ k')
        else 0 :
        α)
      ((of : (a : (i : o) × m' i → (i : o) × m' i → α) → Matrix ((i : o) × m' i) ((i : o) × m' i) α)
          (fun (i j : (i : o) × m' i) ↦
            if i = j then d (i.fst (β := fun (i : o) ↦ m' i)) (i.snd (β := fun (i : o) ↦ m' i)) else 0)
          (Sigma.mk (β := fun (i : o) ↦ m' i) i k) (Sigma.mk (β := fun (i : o) ↦ m' i) j k') :
        α)
⊢ Eq.{u_12 + 1} (α := α)
    (if h : i = j then
        (of : (a : m' i → m' i → α) → Matrix (m' i) (m' i) α) (fun (i_1 j : m' i) ↦ if i_1 = j then d i i_1 else 0) k
          (cast ⋯ k')
      else 0 :
      α)
    ((of : (a : (i : o) × m' i → (i : o) × m' i → α) → Matrix ((i : o) × m' i) ((i : o) × m' i) α)
        (fun (i j : (i : o) × m' i) ↦
          if i = j then d (i.fst (β := fun (i : o) ↦ m' i)) (i.snd (β := fun (i : o) ↦ m' i)) else 0)
        (Sigma.mk (β := fun (i : o) ↦ m' i) i k) (Sigma.mk (β := fun (i : o) ↦ m' i) j k') :
      α)

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

Premises used: Decidable.eq_or_ne, rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst : DecidableEq o
inst_1 : Zero α
inst_2 : (i : o) → DecidableEq (m' i)
d : (i : o) → m' i → α
i : o
k k' : m' i
⊢ Eq.{u_12 + 1} (α := α)
    (if h : i = i then
        (of : (a : m' i → m' i → α) → Matrix (m' i) (m' i) α) (fun (i_1 j : m' i) ↦ if i_1 = j then d i i_1 else 0) k
          (cast ⋯ k')
      else 0 :
      α)
    ((of : (a : (i : o) × m' i → (i : o) × m' i → α) → Matrix ((i : o) × m' i) ((i : o) × m' i) α)
        (fun (i j : (i : o) × m' i) ↦
          if i = j then d (i.fst (β := fun (i : o) ↦ m' i)) (i.snd (β := fun (i : o) ↦ m' i)) else 0)
        (Sigma.mk (β := fun (i : o) ↦ m' i) i k) (Sigma.mk (β := fun (i : o) ↦ m' i) i k') :
      α)

Tactic:
simp
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst : DecidableEq o
inst_1 : Zero α
inst_2 : (i : o) → DecidableEq (m' i)
d : (i : o) → m' i → α
i : o
k : m' i
j : o
k' : m' j
hij : i ≠ j
⊢ Eq.{u_12 + 1} (α := α)
    (if h : i = j then
        (of : (a : m' i → m' i → α) → Matrix (m' i) (m' i) α) (fun (i_1 j : m' i) ↦ if i_1 = j then d i i_1 else 0) k
          (cast ⋯ k')
      else 0 :
      α)
    ((of : (a : (i : o) × m' i → (i : o) × m' i → α) → Matrix ((i : o) × m' i) ((i : o) × m' i) α)
        (fun (i j : (i : o) × m' i) ↦
          if i = j then d (i.fst (β := fun (i : o) ↦ m' i)) (i.snd (β := fun (i : o) ↦ m' i)) else 0)
        (Sigma.mk (β := fun (i : o) ↦ m' i) i k) (Sigma.mk (β := fun (i : o) ↦ m' i) j k') :
      α)

Tactic:
simp [hij]
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst : DecidableEq o
inst_1 : Zero α
inst_2 : (i : o) → DecidableEq (m' i)
inst_3 : One α
rw rw₁ :
  Eq (α := Matrix ((i : o) × m' i) ((i : o) × m' i) α) (diagonal fun (ik : (i : o) × m' i) ↦ 1)
    (diagonal fun (x : (i : o) × m' i) ↦ 1)
⊢ Eq (α := Matrix ((i : o) × m' i) ((i : o) × m' i) α)
    (blockDiagonal' (m' := m') (n' := m') fun (i : o) ↦ diagonal fun (x : m' i) ↦ 1)
    (diagonal fun (x : (i : o) × m' i) ↦ 1)

Tactic:
rw [blockDiagonal'_diagonal]

Premises used: Matrix.blockDiagonal'_diagonal
-- 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 : AddZeroClass α
M N : (i : o) → Matrix.{u_7, u_8, u_12} (m' i) (n' i) α
a :
  ∀ (i : (i : o) × m' i) (j : (i : o) × n' i),
    blockDiagonal' (m' := m') (n' := n') (M + N) i j =
      (blockDiagonal' (m' := m') (n' := n') M + blockDiagonal' (m' := m') (n' := n') N) i j
⊢ blockDiagonal' (m' := m') (n' := n') (M + N) =
    blockDiagonal' (m' := m') (n' := n') M + blockDiagonal' (m' := m') (n' := n') N

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
inst : DecidableEq o
inst_1 : AddZeroClass α
M N : (i : o) → Matrix.{u_7, u_8, u_12} (m' i) (n' i) α
i : (i : o) × m' i
j : (i : o) × n' i
a :
  (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))) +
        N (i.fst (β := fun (i : o) ↦ m' i)) (i.snd (β := fun (i : o) ↦ m' i)) (cast ⋯ (j.snd (β := fun (i : o) ↦ n' i)))
    else 0) =
    HAdd.hAdd (α := α)
      (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
        N (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 + N) i j =
    (blockDiagonal' (m' := m') (n' := n') M + blockDiagonal' (m' := m') (n' := n') N) i j

Tactic:
simp only [blockDiagonal'_apply, Pi.add_apply, add_apply]

Premises used: Matrix.blockDiagonal'_apply, Matrix.add_apply, Pi.add_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 : AddZeroClass α
M N : (i : o) → Matrix.{u_7, u_8, u_12} (m' i) (n' i) α
i : (i : o) × m' i
j : (i : o) × n' i
pos :
  ∀ (h : i.fst (β := fun (i : o) ↦ m' i) = j.fst (β := fun (i : o) ↦ n' i)),
    M (i.fst (β := fun (i : o) ↦ m' i)) (i.snd (β := fun (i : o) ↦ m' i)) (cast ⋯ (j.snd (β := fun (i : o) ↦ n' i))) +
        N (i.fst (β := fun (i : o) ↦ m' i)) (i.snd (β := fun (i : o) ↦ m' i))
          (cast ⋯ (j.snd (β := fun (i : o) ↦ n' i))) =
      M (i.fst (β := fun (i : o) ↦ m' i)) (i.snd (β := fun (i : o) ↦ m' i)) (cast ⋯ (j.snd (β := fun (i : o) ↦ n' i))) +
        N (i.fst (β := fun (i : o) ↦ m' i)) (i.snd (β := fun (i : o) ↦ m' i)) (cast ⋯ (j.snd (β := fun (i : o) ↦ n' i)))
neg : ¬i.fst (β := fun (i : o) ↦ m' i) = j.fst (β := fun (i : o) ↦ n' i) → 0 = HAdd.hAdd (α := α) 0 0
⊢ (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))) +
        N (i.fst (β := fun (i : o) ↦ m' i)) (i.snd (β := fun (i : o) ↦ m' i)) (cast ⋯ (j.snd (β := fun (i : o) ↦ n' i)))
    else 0) =
    HAdd.hAdd (α := α)
      (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
        N (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:
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 : AddZeroClass α
M N : (i : o) → Matrix.{u_7, u_8, u_12} (m' i) (n' i) α
i : (i : o) × m' i
j : (i : o) × n' i
h : i.fst (β := fun (i : o) ↦ m' i) = j.fst (β := fun (i : o) ↦ n' i)
⊢ M (i.fst (β := fun (i : o) ↦ m' i)) (i.snd (β := fun (i : o) ↦ m' i)) (cast ⋯ (j.snd (β := fun (i : o) ↦ n' i))) +
      N (i.fst (β := fun (i : o) ↦ m' i)) (i.snd (β := fun (i : o) ↦ m' i)) (cast ⋯ (j.snd (β := fun (i : o) ↦ n' i))) =
    M (i.fst (β := fun (i : o) ↦ m' i)) (i.snd (β := fun (i : o) ↦ m' i)) (cast ⋯ (j.snd (β := fun (i : o) ↦ n' i))) +
      N (i.fst (β := fun (i : o) ↦ m' i)) (i.snd (β := fun (i : o) ↦ m' i)) (cast ⋯ (j.snd (β := fun (i : o) ↦ n' i)))

Tactic:
simp
-- 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 : AddZeroClass α
M N : (i : o) → Matrix.{u_7, u_8, u_12} (m' i) (n' i) α
i : (i : o) × m' i
j : (i : o) × n' i
h : ¬i.fst (β := fun (i : o) ↦ m' i) = j.fst (β := fun (i : o) ↦ n' i)
⊢ 0 = HAdd.hAdd (α := α) 0 0

Tactic:
simp
-- 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 : AddGroup α
M : (i : o) → Matrix.{u_7, u_8, u_12} (m' i) (n' i) α
⊢ blockDiagonal' (m' := m') (n' := n') (-M) = -blockDiagonal' (m' := m') (n' := n') M

Tactic:
map_neg (blockDiagonal'AddMonoidHom m' n' α) M

Premises used: map_neg, Matrix.blockDiagonal'AddMonoidHom, 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
inst : DecidableEq o
inst_1 : AddGroup α
M N : (i : o) → Matrix.{u_7, u_8, u_12} (m' i) (n' i) α
⊢ blockDiagonal' (m' := m') (n' := n') (M - N) =
    blockDiagonal' (m' := m') (n' := n') M - blockDiagonal' (m' := m') (n' := n') N

Tactic:
map_sub (blockDiagonal'AddMonoidHom m' n' α) M N

Premises used: map_sub, Matrix.blockDiagonal'AddMonoidHom, Matrix.blockDiagonal'
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst : DecidableEq o
inst_1 : NonUnitalNonAssocSemiring α
inst_2 : (i : o) → Fintype (n' i)
inst_3 : Fintype o
M : (i : o) → Matrix.{u_7, u_8, u_12} (m' i) (n' i) α
N : (i : o) → Matrix.{u_8, u_9, u_12} (n' i) (p' i) α
a :
  ∀ (k : o) (i : m' k) (k' : o) (j : p' k'),
    blockDiagonal' (m' := m') (n' := p') (fun (k : o) ↦ M k * N k) (Sigma.mk (β := fun (i : o) ↦ m' i) k i)
        (Sigma.mk (β := fun (i : o) ↦ p' i) k' j) =
      (blockDiagonal' (m' := m') (n' := n') M * blockDiagonal' (m' := n') (n' := p') N)
        (Sigma.mk (β := fun (i : o) ↦ m' i) k i) (Sigma.mk (β := fun (i : o) ↦ p' i) k' j)
⊢ (blockDiagonal' (m' := m') (n' := p') fun (k : o) ↦ M k * N k) =
    blockDiagonal' (m' := m') (n' := n') M * blockDiagonal' (m' := n') (n' := p') N

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

Tactic:
simp only [blockDiagonal'_apply, mul_apply, ← Finset.univ_sigma_univ, Finset.sum_sigma]

Premises used: Matrix.blockDiagonal'_apply, Finset.sum_sigma, Matrix.mul_apply, Finset.univ_sigma_univ
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst : DecidableEq o
inst_1 : NonUnitalNonAssocSemiring α
inst_2 : (i : o) → Fintype (n' i)
inst_3 : Fintype o
M : (i : o) → Matrix.{u_7, u_8, u_12} (m' i) (n' i) α
N : (i : o) → Matrix.{u_8, u_9, u_12} (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
a :
  Eq.{u_12 + 1} (α := α) (if h : k = k' then ∑ j_1 : n' k, M k i j_1 * N k j_1 (cast ⋯ j) else 0)
    (∑ x : n' k,
      HMul.hMul (α := α) (if h : k = k then M k i (cast ⋯ x) else 0) (if h : k = k' then N k x (cast ⋯ j) else 0))
a₁ :
  ∀ (x : o),
    x ≠ k →
      Eq.{u_12 + 1} (α := α)
        (∑ x_1 : n' x,
          HMul.hMul (α := α) (if h : k = x then M k i (cast ⋯ x_1) else 0)
            (if h : x = k' then N x x_1 (cast ⋯ j) else 0))
        0
⊢ Eq.{u_12 + 1} (α := α) (if h : k = k' then ∑ j_1 : n' k, M k i j_1 * N k j_1 (cast ⋯ j) else 0)
    (∑ x : o,
      ∑ x_1 : n' x,
        HMul.hMul (α := α) (if h : k = x then M k i (cast ⋯ x_1) else 0) (if h : x = k' then N x x_1 (cast ⋯ j) else 0))

Tactic:
rw [Fintype.sum_eq_single k]

Premises used: Fintype.sum_eq_single
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst : DecidableEq o
inst_1 : NonUnitalNonAssocSemiring α
inst_2 : (i : o) → Fintype (n' i)
inst_3 : Fintype o
M : (i : o) → Matrix.{u_7, u_8, u_12} (m' i) (n' i) α
N : (i : o) → Matrix.{u_8, u_9, u_12} (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
a :
  Eq.{u_12 + 1} (α := α) (if h : k = k' then ∑ j_1 : n' k, M k i j_1 * N k j_1 (cast ⋯ j) else 0)
    (∑ x : n' k, M k i (cast ⋯ x) * if h : k = k' then N k x (cast ⋯ j) else 0)
⊢ Eq.{u_12 + 1} (α := α) (if h : k = k' then ∑ j_1 : n' k, M k i j_1 * N k j_1 (cast ⋯ j) else 0)
    (∑ x : n' k,
      HMul.hMul (α := α) (if h : k = k then M k i (cast ⋯ x) else 0) (if h : k = k' then N k x (cast ⋯ j) else 0))

Tactic:
simp only [dif_pos]

Premises used: dif_pos
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst : DecidableEq o
inst_1 : NonUnitalNonAssocSemiring α
inst_2 : (i : o) → Fintype (n' i)
inst_3 : Fintype o
M : (i : o) → Matrix.{u_7, u_8, u_12} (m' i) (n' i) α
N : (i : o) → Matrix.{u_8, u_9, u_12} (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
pos :
  ∀ (h : k = k'),
    Eq.{u_12 + 1} (α := α) (∑ j_1 : n' k, M k i j_1 * N k j_1 (cast ⋯ j))
      (∑ x : n' k, M k i (cast ⋯ x) * N k x (cast ⋯ j))
neg : ¬k = k' → Eq.{u_12 + 1} (α := α) 0 (∑ x : n' k, M k i (cast ⋯ x) * 0)
⊢ Eq.{u_12 + 1} (α := α) (if h : k = k' then ∑ j_1 : n' k, M k i j_1 * N k j_1 (cast ⋯ j) else 0)
    (∑ x : n' k, M k i (cast ⋯ x) * if h : k = k' then N k x (cast ⋯ j) 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
p' : o → Type u_9
α : Type u_12
inst : DecidableEq o
inst_1 : NonUnitalNonAssocSemiring α
inst_2 : (i : o) → Fintype (n' i)
inst_3 : Fintype o
M : (i : o) → Matrix.{u_7, u_8, u_12} (m' i) (n' i) α
N : (i : o) → Matrix.{u_8, u_9, u_12} (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
h : k = k'
⊢ Eq.{u_12 + 1} (α := α) (∑ j_1 : n' k, M k i j_1 * N k j_1 (cast ⋯ j))
    (∑ x : n' k, M k i (cast ⋯ x) * N k x (cast ⋯ j))

Tactic:
simp
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst : DecidableEq o
inst_1 : NonUnitalNonAssocSemiring α
inst_2 : (i : o) → Fintype (n' i)
inst_3 : Fintype o
M : (i : o) → Matrix.{u_7, u_8, u_12} (m' i) (n' i) α
N : (i : o) → Matrix.{u_8, u_9, u_12} (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
h : ¬k = k'
⊢ Eq.{u_12 + 1} (α := α) 0 (∑ x : n' k, M k i (cast ⋯ x) * 0)

Tactic:
simp
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst : DecidableEq o
inst_1 : NonUnitalNonAssocSemiring α
inst_2 : (i : o) → Fintype (n' i)
inst_3 : Fintype o
M : (i : o) → Matrix.{u_7, u_8, u_12} (m' i) (n' i) α
N : (i : o) → Matrix.{u_8, u_9, u_12} (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
j' : o
hj' : j' ≠ k
x : n' j'
h : Membership.mem (γ := Finset (n' j')) Finset.univ x
rw : HMul.hMul (α := α) 0 (if h : j' = k' then N j' x (cast ⋯ j) else 0) = 0
rw₁ rw₂ : Eq.{u_12 + 1} (α := α) 0 0
⊢ HMul.hMul (α := α) (if h : k = j' then M k i (cast ⋯ x) else 0) (if h : j' = k' then N j' x (cast ⋯ j) else 0) = 0

Tactic:
rw [dif_neg hj'.symm, zero_mul]

Premises used: MulZeroClass.zero_mul, Ne.symm, dif_neg
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst : DecidableEq o
inst_1 : NonUnitalNonAssocSemiring α
inst_2 : (i : o) → Fintype (n' i)
inst_3 : Fintype o
M : (i : o) → Matrix.{u_7, u_8, u_12} (m' i) (n' i) α
N : (i : o) → Matrix.{u_8, u_9, u_12} (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
j' : o
hj' : j' ≠ k
⊢ Eq.{u_12 + 1} (α := α)
    (∑ x : n' j',
      HMul.hMul (α := α) (if h : k = j' then M k i (cast ⋯ x) else 0) (if h : j' = k' then N j' x (cast ⋯ j) else 0))
    0

Tactic:
exact Finset.sum_eq_zero fun _ _ => by rw [dif_neg hj'.symm, zero_mul]

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.Data.Matrix.Block
Goal:
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst : DecidableEq o
inst_1 : (i : o) → DecidableEq (m' i)
inst_2 : Fintype o
inst_3 : (i : o) → Fintype (m' i)
inst_4 : Semiring α
M : (i : o) → Matrix.{u_7, u_7, u_12} (m' i) (m' i) α
n : ℕ
⊢ blockDiagonal' (m' := m') (n' := m') (M ^ n) = blockDiagonal' (m' := m') (n' := m') M ^ n

Tactic:
map_pow (blockDiagonal'RingHom m' α) M n

Premises used: map_pow, Matrix.blockDiagonal', Matrix.blockDiagonal'RingHom
-- 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
R : Type u_14
inst_1 : Zero α
inst_2 : SMulZeroClass R α
x : R
M : (i : o) → Matrix.{u_7, u_8, u_12} (m' i) (n' i) α
a :
  ∀ (i : (i : o) × m' i) (j : (i : o) × n' i),
    blockDiagonal' (m' := m') (n' := n') (x • M) i j = (x • blockDiagonal' (m' := m') (n' := n') M) i j
⊢ blockDiagonal' (m' := m') (n' := n') (x • M) = x • blockDiagonal' (m' := m') (n' := n') M

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
inst : DecidableEq o
R : Type u_14
inst_1 : Zero α
inst_2 : SMulZeroClass R α
x : R
M : (i : o) → Matrix.{u_7, u_8, u_12} (m' i) (n' i) α
i : (i : o) × m' i
j : (i : o) × n' i
a :
  (if h : i.fst (β := fun (i : o) ↦ m' i) = j.fst (β := fun (i : o) ↦ n' i) then
      x •
        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) =
    HSMul.hSMul (β := α) x
      (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)
⊢ blockDiagonal' (m' := m') (n' := n') (x • M) i j = (x • blockDiagonal' (m' := m') (n' := n') M) i j

Tactic:
simp only [blockDiagonal'_apply, Pi.smul_apply, smul_apply]

Premises used: Matrix.blockDiagonal'_apply, Matrix.smul_apply, Pi.smul_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
R : Type u_14
inst_1 : Zero α
inst_2 : SMulZeroClass R α
x : R
M : (i : o) → Matrix.{u_7, u_8, u_12} (m' i) (n' i) α
i : (i : o) × m' i
j : (i : o) × n' i
pos :
  ∀ (h : i.fst (β := fun (i : o) ↦ m' i) = j.fst (β := fun (i : o) ↦ n' i)),
    x •
        M (i.fst (β := fun (i : o) ↦ m' i)) (i.snd (β := fun (i : o) ↦ m' i))
          (cast ⋯ (j.snd (β := fun (i : o) ↦ n' i))) =
      x •
        M (i.fst (β := fun (i : o) ↦ m' i)) (i.snd (β := fun (i : o) ↦ m' i)) (cast ⋯ (j.snd (β := fun (i : o) ↦ n' i)))
neg : ¬i.fst (β := fun (i : o) ↦ m' i) = j.fst (β := fun (i : o) ↦ n' i) → 0 = HSMul.hSMul (β := α) x 0
⊢ (if h : i.fst (β := fun (i : o) ↦ m' i) = j.fst (β := fun (i : o) ↦ n' i) then
      x •
        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) =
    HSMul.hSMul (β := α) x
      (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)

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
R : Type u_14
inst_1 : Zero α
inst_2 : SMulZeroClass R α
x : R
M : (i : o) → Matrix.{u_7, u_8, u_12} (m' i) (n' i) α
i : (i : o) × m' i
j : (i : o) × n' i
h : i.fst (β := fun (i : o) ↦ m' i) = j.fst (β := fun (i : o) ↦ n' i)
⊢ x • M (i.fst (β := fun (i : o) ↦ m' i)) (i.snd (β := fun (i : o) ↦ m' i)) (cast ⋯ (j.snd (β := fun (i : o) ↦ n' i))) =
    x • M (i.fst (β := fun (i : o) ↦ m' i)) (i.snd (β := fun (i : o) ↦ m' i)) (cast ⋯ (j.snd (β := fun (i : o) ↦ n' i)))

Tactic:
simp
-- 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
R : Type u_14
inst_1 : Zero α
inst_2 : SMulZeroClass R α
x : R
M : (i : o) → Matrix.{u_7, u_8, u_12} (m' i) (n' i) α
i : (i : o) × m' i
j : (i : o) × n' i
h : ¬i.fst (β := fun (i : o) ↦ m' i) = j.fst (β := fun (i : o) ↦ n' i)
⊢ 0 = HSMul.hSMul (β := α) x 0

Tactic:
simp