awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) α
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)
have a : Eq.{u_12 + 1} (α := α) (if h : k = k' then ∑ j_1 : n' k, M k i j_1 * N k j_1 (cast sorry j) else 0)
  (∑ x : o,
    ∑ x_1 : n' x,
      HMul.hMul (α := α) (if h : k = x then M k i (cast sorry x_1) else 0) (if h : x = k' then N x x_1 (cast sorry j) else 0))
Tactic: simp only [blockDiagonal'_apply, mul_apply, ← Finset.univ_sigma_univ, Finset.sum_sigma]
-- 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) α
k : o
i : m' k
k' : o
j : p' k'
⊢ 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))
have a : Eq.{u_12 + 1} (α := α) (if h : k = k' then ∑ j_1 : n' k, M k i j_1 * N k j_1 (cast sorry j) else 0)
  (∑ x : n' k,
    HMul.hMul (α := α) (if h : k = k then M k i (cast sorry x) else 0) (if h : k = k' then N k x (cast sorry j) else 0))
Tactic: rw [Fintype.sum_eq_single k]
-- 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) α
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))
⊢ 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))
have a₁ : ∀ (x : o),
  x ≠ k →
    Eq.{u_12 + 1} (α := α)
      (∑ x_1 : n' x,
        HMul.hMul (α := α) (if h : k = x then M k i (cast sorry x_1) else 0) (if h : x = k' then N x x_1 (cast sorry j) else 0))
      0
Tactic: rw [Fintype.sum_eq_single k]
-- 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) α
k : o
i : m' k
k' : o
j : p' k'
⊢ 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))
have a : Eq.{u_12 + 1} (α := α) (if h : k = k' then ∑ j_1 : n' k, M k i j_1 * N k j_1 (cast sorry j) else 0)
  (∑ x : n' k, M k i (cast sorry x) * if h : k = k' then N k x (cast sorry j) else 0)
Tactic: simp only [dif_pos]
-- 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) α
k : o
i : m' k
k' : o
j : p' k'
⊢ 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)
have pos : ∀ (h : k = k'),
  Eq.{u_12 + 1} (α := α) (∑ j_1 : n' k, M k i j_1 * N k j_1 (cast sorry j))
    (∑ x : n' k, M k i (cast sorry x) * N k x (cast sorry j))
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) α
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))
⊢ 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)
have neg : ¬k = k' → Eq.{u_12 + 1} (α := α) 0 (∑ x : n' k, M k i (cast sorry x) * 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) α
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
⊢ 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
have rw : HMul.hMul (α := α) 0 (if h : j' = k' then N j' x (cast sorry j) else 0) = 0
Tactic: rw [dif_neg hj'.symm, zero_mul]
-- 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) α
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
⊢ 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
have rw₁ : Eq.{u_12 + 1} (α := α) 0 0
Tactic: rw [dif_neg hj'.symm, zero_mul]
-- 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
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) α
⊢ blockDiagonal' (m' := m') (n' := n') (x • M) = x • blockDiagonal' (m' := m') (n' := n') M
have 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
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
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
⊢ blockDiagonal' (m' := m') (n' := n') (x • M) i j = (x • blockDiagonal' (m' := m') (n' := n') M) i j
have 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 sorry (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 sorry (j.snd (β := fun (i : o) ↦ n' i)))
    else 0)
Tactic: simp only [blockDiagonal'_apply, Pi.smul_apply, smul_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
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
⊢ (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)
have 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 sorry (j.snd (β := fun (i : o) ↦ n' i))) =
    x • M (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
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)))
⊢ (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)
have neg : ¬i.fst (β := fun (i : o) ↦ m' i) = j.fst (β := fun (i : o) ↦ n' i) → 0 = HSMul.hSMul (β := α) x 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst : Zero α
inst_1 : DecidableEq o
inst_2 : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i j : m' k
⊢ (diagonal d).blockDiag' (m' := m') (n' := m') k i j =
    diagonal (fun (i : m' k) ↦ d (Sigma.mk (β := fun (i : o) ↦ m' i) k i)) i j
have inl : (diagonal d).blockDiag' (m' := m') (n' := m') k i i =
  diagonal (fun (i : m' k) ↦ d (Sigma.mk (β := fun (i : o) ↦ m' i) k i)) 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:
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst : Zero α
inst_1 : DecidableEq o
inst_2 : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i j : m' k
inl :
  (diagonal d).blockDiag' (m' := m') (n' := m') k i i =
    diagonal (fun (i : m' k) ↦ d (Sigma.mk (β := fun (i : o) ↦ m' i) k i)) i i
⊢ (diagonal d).blockDiag' (m' := m') (n' := m') k i j =
    diagonal (fun (i : m' k) ↦ d (Sigma.mk (β := fun (i : o) ↦ m' i) k i)) i j
have inr : ∀ (hij : i ≠ j),
  (diagonal d).blockDiag' (m' := m') (n' := m') k i j =
    diagonal (fun (i : m' k) ↦ d (Sigma.mk (β := fun (i : o) ↦ m' i) k i)) i j
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 : Zero α
inst_1 : DecidableEq o
inst_2 : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i : m' k
⊢ (diagonal d).blockDiag' (m' := m') (n' := m') k i i =
    diagonal (fun (i : m' k) ↦ d (Sigma.mk (β := fun (i : o) ↦ m' i) k i)) i i
have inl : diagonal d (Sigma.mk (β := fun (i : o) ↦ m' i) k i) (Sigma.mk (β := fun (i : o) ↦ m' i) k i) =
  diagonal (fun (i : m' k) ↦ d (Sigma.mk (β := fun (i : o) ↦ m' i) k i)) i i
Tactic: rw [blockDiag'_apply, diagonal_apply_eq, diagonal_apply_eq]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst : Zero α
inst_1 : DecidableEq o
inst_2 : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i : m' k
inl :
  diagonal d (Sigma.mk (β := fun (i : o) ↦ m' i) k i) (Sigma.mk (β := fun (i : o) ↦ m' i) k i) =
    diagonal (fun (i : m' k) ↦ d (Sigma.mk (β := fun (i : o) ↦ m' i) k i)) i i
⊢ (diagonal d).blockDiag' (m' := m') (n' := m') k i i =
    diagonal (fun (i : m' k) ↦ d (Sigma.mk (β := fun (i : o) ↦ m' i) k i)) i i
have inl₁ : d (Sigma.mk (β := fun (i : o) ↦ m' i) k i) = diagonal (fun (i : m' k) ↦ d (Sigma.mk (β := fun (i : o) ↦ m' i) k i)) i i
Tactic: rw [blockDiag'_apply, diagonal_apply_eq, diagonal_apply_eq]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst : Zero α
inst_1 : DecidableEq o
inst_2 : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i : m' k
inl :
  diagonal d (Sigma.mk (β := fun (i : o) ↦ m' i) k i) (Sigma.mk (β := fun (i : o) ↦ m' i) k i) =
    diagonal (fun (i : m' k) ↦ d (Sigma.mk (β := fun (i : o) ↦ m' i) k i)) i i
inl₁ :
  d (Sigma.mk (β := fun (i : o) ↦ m' i) k i) =
    diagonal (fun (i : m' k) ↦ d (Sigma.mk (β := fun (i : o) ↦ m' i) k i)) i i
⊢ (diagonal d).blockDiag' (m' := m') (n' := m') k i i =
    diagonal (fun (i : m' k) ↦ d (Sigma.mk (β := fun (i : o) ↦ m' i) k i)) i i
have inl₂ : d (Sigma.mk (β := fun (i : o) ↦ m' i) k i) = d (Sigma.mk (β := fun (i : o) ↦ m' i) k i)
Tactic: rw [blockDiag'_apply, diagonal_apply_eq, diagonal_apply_eq]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst : Zero α
inst_1 : DecidableEq o
inst_2 : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i j : m' k
hij : i ≠ j
⊢ (diagonal d).blockDiag' (m' := m') (n' := m') k i j =
    diagonal (fun (i : m' k) ↦ d (Sigma.mk (β := fun (i : o) ↦ m' i) k i)) i j
have rw : ∀ (h : Sigma.mk (β := fun (i : o) ↦ m' i) k i = Sigma.mk (β := fun (i : o) ↦ m' i) k j), i = j
Tactic: rw [blockDiag'_apply, diagonal_apply_ne _ hij, diagonal_apply_ne _ (mt (fun h => ?_) hij)]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst : Zero α
inst_1 : DecidableEq o
inst_2 : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i j : m' k
hij : i ≠ j
h : Sigma.mk (β := fun (i : o) ↦ m' i) k i = Sigma.mk (β := fun (i : o) ↦ m' i) k j
⊢ i = j
have refl : ∀ (hij : i ≠ i), i = i
Tactic: cases h
Cleared hypotheses: j, hij, h
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
R : Type u_10
inst : CommRing R
m : Type u_14
n : Type u_15
k : Type u_16
inst_1 : Fintype n
p : m → Prop
q : k → Prop
A : Matrix m n R
B : Matrix n k R
⊢ (A * B).toBlock p q =
    HMul.hMul (α := Matrix.{u_14, u_15, u_10} { a : m // p a } { a : n // ⊤ a } R) (β :=
      Matrix.{u_15, u_16, u_10} { a : n // ⊤ a } { a : k // q a } R) (A.toBlock p ⊤) (B.toBlock ⊤ q)
have a : ∀ (i : { a : m // p a }) (k_1 : { a : k // q a }),
  (A * B).toBlock p q i k_1 =
    HMul.hMul (α := Matrix.{u_14, u_15, u_10} { a : m // p a } { a : n // ⊤ a } R) (β :=
      Matrix.{u_15, u_16, u_10} { a : n // ⊤ a } { a : k // q a } R) (A.toBlock p ⊤) (B.toBlock ⊤ q) i k_1
Tactic: ext i k
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
R : Type u_10
inst : CommRing R
m : Type u_14
n : Type u_15
k_1 : Type u_16
inst_1 : Fintype n
p : m → Prop
q : k_1 → Prop
A : Matrix m n R
B : Matrix n k_1 R
i : { a : m // p a }
k : { a : k_1 // q a }
⊢ (A * B).toBlock p q i k =
    HMul.hMul (α := Matrix.{u_14, u_15, u_10} { a : m // p a } { a : n // ⊤ a } R) (β :=
      Matrix.{u_15, u_16, u_10} { a : n // ⊤ a } { a : k_1 // q a } R) (A.toBlock p ⊤) (B.toBlock ⊤ q) i k
have a : Eq.{u_10 + 1} (α := R) (∑ j : n, A (↑i : m) j * B j (↑k : k_1))
  (∑ x : { a : n // ⊤ a }, A (↑i : m) (↑x : n) * B (↑x : n) (↑k : k_1))
Tactic: simp only [toBlock_apply, mul_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
R : Type u_10
inst : CommRing R
m : Type u_14
n : Type u_15
k_1 : Type u_16
inst_1 : Fintype n
p : m → Prop
q : k_1 → Prop
A : Matrix m n R
B : Matrix n k_1 R
i : { a : m // p a }
k : { a : k_1 // q a }
⊢ Eq.{u_10 + 1} (α := R) (∑ j : n, A (↑i : m) j * B j (↑k : k_1))
    (∑ x : { a : n // ⊤ a }, A (↑i : m) (↑x : n) * B (↑x : n) (↑k : k_1))
have a : ∀ (x : n), Membership.mem (γ := Finset n) Finset.univ x ↔ ⊤ x
Tactic: rw [Finset.sum_subtype]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
R : Type u_10
inst : CommRing R
m : Type u_14
n : Type u_15
k : Type u_16
inst_1 : Fintype n
p : m → Prop
q : n → Prop
inst_2 : DecidablePred q
r : k → Prop
A : Matrix m n R
B : Matrix n k R
⊢ (A * B).toBlock p r =
    A.toBlock p q * B.toBlock q r +
      HMul.hMul (α := Matrix.{u_14, u_15, u_10} { a : m // p a } { a : n // ¬q a } R) (β :=
        Matrix.{u_15, u_16, u_10} { a : n // ¬q a } { a : k // r a } R) (A.toBlock p fun (i : n) ↦ ¬q i)
        (B.toBlock (fun (i : n) ↦ ¬q i) r)
have a : ∀ (i : { a : m // p a }) (k_1 : { a : k // r a }),
  (A * B).toBlock p r i k_1 =
    (A.toBlock p q * B.toBlock q r +
        HMul.hMul (α := Matrix.{u_14, u_15, u_10} { a : m // p a } { a : n // ¬q a } R) (β :=
          Matrix.{u_15, u_16, u_10} { a : n // ¬q a } { a : k // r a } R) (A.toBlock p fun (i : n) ↦ ¬q i)
          (B.toBlock (fun (i : n) ↦ ¬q i) r))
      i k_1
Tactic: ext i k
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
R : Type u_10
inst : CommRing R
m : Type u_14
n : Type u_15
k_1 : Type u_16
inst_1 : Fintype n
p : m → Prop
q : n → Prop
inst_2 : DecidablePred q
r : k_1 → Prop
A : Matrix m n R
B : Matrix n k_1 R
i : { a : m // p a }
k : { a : k_1 // r a }
⊢ (A * B).toBlock p r i k =
    (A.toBlock p q * B.toBlock q r +
        HMul.hMul (α := Matrix.{u_14, u_15, u_10} { a : m // p a } { a : n // ¬q a } R) (β :=
          Matrix.{u_15, u_16, u_10} { a : n // ¬q a } { a : k_1 // r a } R) (A.toBlock p fun (i : n) ↦ ¬q i)
          (B.toBlock (fun (i : n) ↦ ¬q i) r))
      i k
have a : ∑ j : n, A (↑i : m) j * B j (↑k : k_1) =
  (A.toBlock p q * B.toBlock q r +
      HMul.hMul (α := Matrix.{u_14, u_15, u_10} { a : m // p a } { a : n // ¬q a } R) (β :=
        Matrix.{u_15, u_16, u_10} { a : n // ¬q a } { a : k_1 // r a } R) (A.toBlock p fun (i : n) ↦ ¬q i)
        (B.toBlock (fun (i : n) ↦ ¬q i) r))
    i k
Tactic: simp only [toBlock_apply, mul_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
R : Type u_10
inst : CommRing R
m : Type u_14
n : Type u_15
k : Type u_16
inst_1 : Fintype n
p : m → Prop
q : n → Prop
inst_2 : DecidablePred q
r : k → Prop
A : Matrix m n R
B : Matrix n k R
⊢ (A * B).toBlock p r =
    A.toBlock p q * B.toBlock q r +
      HMul.hMul (α := Matrix.{u_14, u_15, u_10} { a : m // p a } { a : n // ¬q a } R) (β :=
        Matrix.{u_15, u_16, u_10} { a : n // ¬q a } { a : k // r a } R) (A.toBlock p fun (i : n) ↦ ¬q i)
        (B.toBlock (fun (i : n) ↦ ¬q i) r)
have a : ∀ (i : { a : m // p a }) (k_1 : { a : k // r a }),
  (A * B).toBlock p r i k_1 =
    (A.toBlock p q * B.toBlock q r +
        HMul.hMul (α := Matrix.{u_14, u_15, u_10} { a : m // p a } { a : n // ¬q a } R) (β :=
          Matrix.{u_15, u_16, u_10} { a : n // ¬q a } { a : k // r a } R) (A.toBlock p fun (i : n) ↦ ¬q i)
          (B.toBlock (fun (i : n) ↦ ¬q i) r))
      i k_1
Tactic: classical
    ext i k
    simp only [toBlock_apply, mul_apply]
    exact (Fintype.sum_subtype_add_sum_subtype q fun x => A (↑i) x * B x ↑k).symm
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
R : Type u_10
inst : CommRing R
m : Type u_14
n : Type u_15
k : Type u_16
inst_1 : Fintype n
p : m → Prop
q : n → Prop
inst_2 : DecidablePred q
r : k → Prop
A : Matrix m n R
B : Matrix n k R
a :
  ∀ (i : { a : m // p a }) (k_1 : { a : k // r a }),
    (A * B).toBlock p r i k_1 =
      (A.toBlock p q * B.toBlock q r +
          HMul.hMul (α := Matrix.{u_14, u_15, u_10} { a : m // p a } { a : n // ¬q a } R) (β :=
            Matrix.{u_15, u_16, u_10} { a : n // ¬q a } { a : k // r a } R) (A.toBlock p fun (i : n) ↦ ¬q i)
            (B.toBlock (fun (i : n) ↦ ¬q i) r))
        i k_1
⊢ (A * B).toBlock p r =
    A.toBlock p q * B.toBlock q r +
      HMul.hMul (α := Matrix.{u_14, u_15, u_10} { a : m // p a } { a : n // ¬q a } R) (β :=
        Matrix.{u_15, u_16, u_10} { a : n // ¬q a } { a : k // r a } R) (A.toBlock p fun (i : n) ↦ ¬q i)
        (B.toBlock (fun (i : n) ↦ ¬q i) r)
have a₁ : ∀ (i : { a : m // p a }) (k_1 : { a : k // r a }),
  ∑ j : n, A (↑i : m) j * B j (↑k_1 : k) =
    (A.toBlock p q * B.toBlock q r +
        HMul.hMul (α := Matrix.{u_14, u_15, u_10} { a : m // p a } { a : n // ¬q a } R) (β :=
          Matrix.{u_15, u_16, u_10} { a : n // ¬q a } { a : k // r a } R) (A.toBlock p fun (i : n) ↦ ¬q i)
          (B.toBlock (fun (i : n) ↦ ¬q i) r))
      i k_1
Tactic: classical
    ext i k
    simp only [toBlock_apply, mul_apply]
    exact (Fintype.sum_subtype_add_sum_subtype q fun x => A (↑i) x * B x ↑k).symm
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
m : Type u_2
n : Type u_3
R : Type u_14
inst : Zero R
inst_1 : DecidableEq m
d : m → Matrix n n R
⊢ Eq (α := Matrix (m × n) (m × n) R)
    ((comp m m n n R : (a : Matrix m m (Matrix n n R)) → Matrix (m × n) (m × n) R) (diagonal d) :
      Matrix (m × n) (m × n) R)
    ((reindex (Equiv.prodComm n m) (Equiv.prodComm n m) : (a : Matrix (n × m) (n × m) R) → Matrix (m × n) (m × n) R)
        (blockDiagonal d) :
      Matrix (m × n) (m × n) R)
have a : ∀ (i j : m × n),
  Eq.{u_14 + 1} (α := R)
    ((comp m m n n R : (a : Matrix m m (Matrix n n R)) → Matrix (m × n) (m × n) R) (diagonal d) i j : R)
    ((reindex (Equiv.prodComm n m) (Equiv.prodComm n m) : (a : Matrix (n × m) (n × m) R) → Matrix (m × n) (m × n) R)
        (blockDiagonal d) i j :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
n : ℕ
⊢ (A n).diag = 2
have h : ∀ (x : Fin n), (A n).diag x = 2 x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
⊢ A n i j ≤ 0
have simp : LE.le (α := ℤ) (if i = j then 2 else if (↑i : ℕ) + 1 = (↑j : ℕ) ∨ (↑j : ℕ) + 1 = (↑i : ℕ) then -1 else 0) 0
Tactic: simp only [A, Matrix.of_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
⊢ LE.le (α := ℤ) (if i = j then 2 else if (↑i : ℕ) + 1 = (↑j : ℕ) ∨ (↑j : ℕ) + 1 = (↑i : ℕ) then -1 else 0) 0
have pos : i = j → LE.le (α := ℤ) 2 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
pos : i = j → LE.le (α := ℤ) 2 0
⊢ LE.le (α := ℤ) (if i = j then 2 else if (↑i : ℕ) + 1 = (↑j : ℕ) ∨ (↑j : ℕ) + 1 = (↑i : ℕ) then -1 else 0) 0
have pos₁ : ¬i = j → (↑i : ℕ) + 1 = (↑j : ℕ) ∨ (↑j : ℕ) + 1 = (↑i : ℕ) → LE.le (α := ℤ) (-1) 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.Cartan (goal)
Goal:
n : ℕ
i j : Fin n
h : i ≠ j
pos : i = j → LE.le (α := ℤ) 2 0
pos₁ : ¬i = j → (↑i : ℕ) + 1 = (↑j : ℕ) ∨ (↑j : ℕ) + 1 = (↑i : ℕ) → LE.le (α := ℤ) (-1) 0
⊢ LE.le (α := ℤ) (if i = j then 2 else if (↑i : ℕ) + 1 = (↑j : ℕ) ∨ (↑j : ℕ) + 1 = (↑i : ℕ) then -1 else 0) 0
have neg : ¬i = j → ¬((↑i : ℕ) + 1 = (↑j : ℕ) ∨ (↑j : ℕ) + 1 = (↑i : ℕ)) → LE.le (α := ℤ) 0 0
Tactic: split_ifs