awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ (diagonal d).blockDiag k i j = diagonal (fun (i : m) ↦ d (i, k)) i j
have inl : (diagonal d).blockDiag k i i = diagonal (fun (i : m) ↦ d (i, k)) i i
Tactic: obtain rfl | hij := Decidable.eq_or_ne i j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ (diagonal d).blockDiag k i j = diagonal (fun (i : m) ↦ d (i, k)) i j
have inr : ∀ (hij : 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
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ (diagonal d).blockDiag k i i = diagonal (fun (i : m) ↦ d (i, k)) i i
have inl : diagonal d (i, k) (i, k) = diagonal (fun (i : m) ↦ d (i, k)) i i
Tactic: rw [blockDiag_apply, diagonal_apply_eq, diagonal_apply_eq]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ (diagonal d).blockDiag k i i = diagonal (fun (i : m) ↦ d (i, k)) i i
have inl₁ : d (i, k) = diagonal (fun (i : m) ↦ d (i, k)) i i
Tactic: rw [blockDiag_apply, diagonal_apply_eq, diagonal_apply_eq]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ (diagonal d).blockDiag k i i = diagonal (fun (i : m) ↦ d (i, k)) i i
have inl₂ : d (i, k) = d (i, k)
Tactic: rw [blockDiag_apply, diagonal_apply_eq, diagonal_apply_eq]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ (diagonal d).blockDiag k i j = diagonal (fun (i : m) ↦ d (i, k)) i j
have rw : (i, k) = (j, k) → i = j
Tactic: rw [blockDiag_apply, diagonal_apply_ne _ hij, diagonal_apply_ne _ (mt _ hij)]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ (blockDiagonal' (m' := m') (n' := n') M).map f = blockDiagonal' (m' := m') (n' := n') fun (k : o) ↦ (M k).map f
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ (blockDiagonal' (m' := m') (n' := n') M).map f i j =
    blockDiagonal' (m' := m') (n' := n') (fun (k : o) ↦ (M k).map f) i j
have 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 sorry (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 sorry (j.snd (β := fun (i : o) ↦ n' i))))
  else 0
Tactic: simp only [map_apply, blockDiagonal'_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ 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
have 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 sorry (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 sorry (j.snd (β := fun (i : o) ↦ n' i))))
  else 0)
Tactic: rw [apply_dite f, hf]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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)
⊢ 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
have 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 sorry (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 sorry (j.snd (β := fun (i : o) ↦ n' i))))
  else 0)
Tactic: rw [apply_dite f, hf]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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) α
⊢ (blockDiagonal' (m' := m') (n' := n') M)ᵀ = blockDiagonal' (m' := n') (n' := m') fun (k : o) ↦ (M k)ᵀ
have 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)
Tactic: ext ⟨ii, ix⟩ ⟨ji, jx⟩
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ (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)
have a : Eq.{u_12 + 1} (α := α) (if h : ji = ii then M ji jx (cast sorry ix) else 0) (if h : ii = ji then M ii (cast sorry jx) ix else 0)
Tactic: simp only [transpose_apply, blockDiagonal'_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ 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)
have pos : ∀ (h : ji = ii) (h_1 : ii = ji), M ji jx (cast sorry ix) = M ii (cast sorry jx) ix
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ 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)
have neg : ∀ (h : ji = ii), ¬ii = ji → M ji jx (cast sorry ix) = 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ 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)
have pos₁ : ¬ji = ii → ∀ (h : ii = ji), 0 = M ii (cast sorry jx) ix
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ 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)
have neg₁ : ¬ji = ii → ¬ii = ji → Eq.{u_12 + 1} (α := α) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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) α
⊢ (blockDiagonal' (m' := m') (n' := n') M)ᴴ = blockDiagonal' (m' := n') (n' := m') fun (k : o) ↦ (M k)ᴴ
have 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)
Tactic: simp only [conjTranspose, blockDiagonal'_transpose]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst : DecidableEq o
inst_1 : Zero α
⊢ Eq (α := Matrix ((i : o) × m' i) ((i : o) × n' i) α) (blockDiagonal' (m' := m') (n' := n') 0) 0
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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 → α
⊢ 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)))
have 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'))
Tactic: ext ⟨i, k⟩ ⟨j, k'⟩
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ 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'))
have 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 sorry 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 only [blockDiagonal'_apply, diagonal]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ 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') :
      α)
have 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 sorry 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: obtain rfl | hij := Decidable.eq_or_ne i j
Cleared hypotheses: j, k'
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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') :
        α)
⊢ 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') :
      α)
have 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 sorry 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
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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 α
⊢ 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)
have 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)
Tactic: rw [blockDiagonal'_diagonal]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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) α
⊢ blockDiagonal' (m' := m') (n' := n') (M + N) =
    blockDiagonal' (m' := m') (n' := n') M + blockDiagonal' (m' := m') (n' := n') N
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ blockDiagonal' (m' := m') (n' := n') (M + N) i j =
    (blockDiagonal' (m' := m') (n' := n') M + blockDiagonal' (m' := m') (n' := n') N) i j
have 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 sorry (j.snd (β := fun (i : o) ↦ n' i))) +
      N (i.fst (β := fun (i : o) ↦ m' i)) (i.snd (β := fun (i : o) ↦ m' i)) (cast sorry (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 sorry (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 sorry (j.snd (β := fun (i : o) ↦ n' i)))
    else 0)
Tactic: simp only [blockDiagonal'_apply, Pi.add_apply, add_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ (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)
have 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 sorry (j.snd (β := fun (i : o) ↦ n' i))) +
      N (i.fst (β := fun (i : o) ↦ m' i)) (i.snd (β := fun (i : o) ↦ m' i)) (cast sorry (j.snd (β := fun (i : o) ↦ n' i))) =
    M (i.fst (β := fun (i : o) ↦ m' i)) (i.snd (β := fun (i : o) ↦ m' i)) (cast sorry (j.snd (β := fun (i : o) ↦ n' i))) +
      N (i.fst (β := fun (i : o) ↦ m' i)) (i.snd (β := fun (i : o) ↦ m' i)) (cast sorry (j.snd (β := fun (i : o) ↦ n' i)))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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)))
⊢ (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)
have neg : ¬i.fst (β := fun (i : o) ↦ m' i) = j.fst (β := fun (i : o) ↦ n' i) → 0 = HAdd.hAdd (α := α) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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) α
⊢ (blockDiagonal' (m' := m') (n' := p') fun (k : o) ↦ M k * N k) =
    blockDiagonal' (m' := m') (n' := n') M * blockDiagonal' (m' := n') (n' := p') N
have 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)
Tactic: ext ⟨k, i⟩ ⟨k', j⟩