awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
m : Type u_2
α : Type u_12
inst : DecidableEq m
inst_1 : Zero α
d : m → α
p : m → Prop
⊢ (diagonal d).toBlock p p = diagonal fun (i : Subtype p) ↦ d (↑i : m)
have a : ∀ (i j : { a : m // p a }), (diagonal d).toBlock p p i j = diagonal (fun (i : Subtype p) ↦ d (↑i : m)) i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
m : Type u_2
α : Type u_12
inst : DecidableEq m
inst_1 : Zero α
d : m → α
p : m → Prop
i j : { a : m // p a }
⊢ (diagonal d).toBlock p p i j = diagonal (fun (i : Subtype p) ↦ d (↑i : m)) i j
have pos : ∀ (h : i = j), (diagonal d).toBlock p p i j = diagonal (fun (i : Subtype p) ↦ d (↑i : m)) i j
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
m : Type u_2
α : Type u_12
inst : DecidableEq m
inst_1 : Zero α
d : m → α
p : m → Prop
i j : { a : m // p a }
pos : ∀ (h : i = j), (diagonal d).toBlock p p i j = diagonal (fun (i : Subtype p) ↦ d (↑i : m)) i j
⊢ (diagonal d).toBlock p p i j = diagonal (fun (i : Subtype p) ↦ d (↑i : m)) i j
have neg : ∀ (h : ¬i = j), (diagonal d).toBlock p p i j = diagonal (fun (i : Subtype p) ↦ d (↑i : m)) i j
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
m : Type u_2
α : Type u_12
inst : DecidableEq m
inst_1 : Zero α
d : m → α
p q : m → Prop
hpq : Disjoint p q
⊢ (diagonal d).toBlock p q = 0
have a : ∀ (i : m) (hi : p i) (j : m) (hj : q j),
  (diagonal d).toBlock p q (Subtype.mk (p := fun (a : m) ↦ p a) i hi) (Subtype.mk (p := fun (a : m) ↦ q a) j hj) =
    0 (Subtype.mk (p := fun (a : m) ↦ p a) i hi) (Subtype.mk (p := fun (a : m) ↦ q a) j hj)
Tactic: ext ⟨i, hi⟩ ⟨j, hj⟩
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (hypothesis)
Goal:
m : Type u_2
α : Type u_12
inst : DecidableEq m
inst_1 : Zero α
d : m → α
p q : m → Prop
hpq : Disjoint p q
i : m
hi : p i
j : m
hj : q j
⊢ (diagonal d).toBlock p q (Subtype.mk (p := fun (a : m) ↦ p a) i hi) (Subtype.mk (p := fun (a : m) ↦ q a) j hj) =
    0 (Subtype.mk (p := fun (a : m) ↦ p a) i hi) (Subtype.mk (p := fun (a : m) ↦ q a) j hj)
have this : i ≠ j
Tactic: have : i ≠ j := fun heq => hpq.le_bot i ⟨hi, heq.symm ▸ hj⟩
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
l : Type u_1
m : Type u_2
α : Type u_12
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : Zero α
d₁ : l → α
d₂ : m → α
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) = diagonal (Sum.elim d₁ d₂)
have a : ∀ (i j : l ⊕ m), fromBlocks (diagonal d₁) 0 0 (diagonal d₂) i j = diagonal (Sum.elim d₁ d₂) i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
l : Type u_1
m : Type u_2
α : Type u_12
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : Zero α
d₁ : l → α
d₂ : m → α
i j : l ⊕ m
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) i j = diagonal (Sum.elim d₁ d₂) i j
have a : ∀ (val : l), fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inl val) j = diagonal (Sum.elim d₁ d₂) (Sum.inl val) j
Tactic: rcases i with ⟨⟩
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
l : Type u_1
m : Type u_2
α : Type u_12
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : Zero α
d₁ : l → α
d₂ : m → α
i j : l ⊕ m
a : ∀ (val : l), fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inl val) j = diagonal (Sum.elim d₁ d₂) (Sum.inl val) j
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) i j = diagonal (Sum.elim d₁ d₂) i j
have a₁ : ∀ (val : m), fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inr val) j = diagonal (Sum.elim d₁ d₂) (Sum.inr val) j
Tactic: rcases i with ⟨⟩
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
l : Type u_1
m : Type u_2
α : Type u_12
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : Zero α
d₁ : l → α
d₂ : m → α
j : l ⊕ m
val : l
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inl val) j = diagonal (Sum.elim d₁ d₂) (Sum.inl val) j
have a : ∀ (val_1 : l),
  fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inl val) (Sum.inl val_1) =
    diagonal (Sum.elim d₁ d₂) (Sum.inl val) (Sum.inl val_1)
Tactic: rcases j with ⟨⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
l : Type u_1
m : Type u_2
α : Type u_12
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : Zero α
d₁ : l → α
d₂ : m → α
j : l ⊕ m
val : l
a :
  ∀ (val_1 : l),
    fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inl val) (Sum.inl val_1) =
      diagonal (Sum.elim d₁ d₂) (Sum.inl val) (Sum.inl val_1)
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inl val) j = diagonal (Sum.elim d₁ d₂) (Sum.inl val) j
have a₁ : ∀ (val_1 : m),
  fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inl val) (Sum.inr val_1) =
    diagonal (Sum.elim d₁ d₂) (Sum.inl val) (Sum.inr val_1)
Tactic: rcases j with ⟨⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
l : Type u_1
m : Type u_2
α : Type u_12
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : Zero α
d₁ : l → α
d₂ : m → α
j : l ⊕ m
val : m
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inr val) j = diagonal (Sum.elim d₁ d₂) (Sum.inr val) j
have a : ∀ (val_1 : l),
  fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inr val) (Sum.inl val_1) =
    diagonal (Sum.elim d₁ d₂) (Sum.inr val) (Sum.inl val_1)
Tactic: rcases j with ⟨⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
l : Type u_1
m : Type u_2
α : Type u_12
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : Zero α
d₁ : l → α
d₂ : m → α
j : l ⊕ m
val : m
a :
  ∀ (val_1 : l),
    fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inr val) (Sum.inl val_1) =
      diagonal (Sum.elim d₁ d₂) (Sum.inr val) (Sum.inl val_1)
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inr val) j = diagonal (Sum.elim d₁ d₂) (Sum.inr val) j
have a₁ : ∀ (val_1 : m),
  fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inr val) (Sum.inr val_1) =
    diagonal (Sum.elim d₁ d₂) (Sum.inr val) (Sum.inr val_1)
Tactic: rcases j with ⟨⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
l : Type u_1
m : Type u_2
α : Type u_12
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : Zero α
v : l ⊕ m → α
⊢ Eq (α := Matrix l l α) ((of : (a : l → l → α) → Matrix l l α) fun (i j : l) ↦ diagonal v (Sum.inl i) (Sum.inl j))
    (diagonal fun (i : l) ↦ v (Sum.inl i))
have h : ∀ (i j : l),
  Eq.{u_12 + 1} (α := α)
    ((of : (a : l → l → α) → Matrix l l α) (fun (i j : l) ↦ diagonal v (Sum.inl i) (Sum.inl j)) i j : α)
    (diagonal (fun (i : l) ↦ v (Sum.inl i)) i j : α)
Tactic: funext i j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
l : Type u_1
m : Type u_2
α : Type u_12
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : Zero α
v : l ⊕ m → α
⊢ Eq (α := Matrix m m α) ((of : (a : m → m → α) → Matrix m m α) fun (i j : m) ↦ diagonal v (Sum.inr i) (Sum.inr j))
    (diagonal fun (i : m) ↦ v (Sum.inr i))
have h : ∀ (i j : m),
  Eq.{u_12 + 1} (α := α)
    ((of : (a : m → m → α) → Matrix m m α) (fun (i j : m) ↦ diagonal v (Sum.inr i) (Sum.inr j)) i j : α)
    (diagonal (fun (i : m) ↦ v (Sum.inr i)) i j : α)
Tactic: funext i j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
l : Type u_1
m : Type u_2
α : Type u_12
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : Zero α
inst_3 : One α
⊢ Eq (α := Matrix (l ⊕ m) (l ⊕ m) α) (fromBlocks 1 0 0 1) 1
have a : ∀ (i j : l ⊕ m), Eq.{u_12 + 1} (α := α) (fromBlocks 1 0 0 1 i j) (1 i j)
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
l : Type u_1
m : Type u_2
α : Type u_12
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : Zero α
inst_3 : One α
i j : l ⊕ m
⊢ Eq.{u_12 + 1} (α := α) (fromBlocks 1 0 0 1 i j) (1 i j)
have a : ∀ (val : l), Eq.{u_12 + 1} (α := α) (fromBlocks (o := m) 1 0 0 1 (Sum.inl val) j) (1 (Sum.inl val) j)
Tactic: rcases i with ⟨⟩
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
l : Type u_1
m : Type u_2
α : Type u_12
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : Zero α
inst_3 : One α
i j : l ⊕ m
a : ∀ (val : l), Eq.{u_12 + 1} (α := α) (fromBlocks (o := m) 1 0 0 1 (Sum.inl val) j) (1 (Sum.inl val) j)
⊢ Eq.{u_12 + 1} (α := α) (fromBlocks 1 0 0 1 i j) (1 i j)
have a₁ : ∀ (val : m), Eq.{u_12 + 1} (α := α) (fromBlocks (n := l) 1 0 0 1 (Sum.inr val) j) (1 (Sum.inr val) j)
Tactic: rcases i with ⟨⟩
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
l : Type u_1
m : Type u_2
α : Type u_12
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : Zero α
inst_3 : One α
j : l ⊕ m
val : l
⊢ Eq.{u_12 + 1} (α := α) (fromBlocks (o := m) 1 0 0 1 (Sum.inl val) j) (1 (Sum.inl val) j)
have a : ∀ (val_1 : l),
  Eq.{u_12 + 1} (α := α) (fromBlocks.{u_1, u_2, u_1, u_2, u_12} (m := m) (o := m) 1 0 0 1 (Sum.inl val) (Sum.inl val_1))
    (1 (Sum.inl val) (Sum.inl val_1))
Tactic: rcases j with ⟨⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
l : Type u_1
m : Type u_2
α : Type u_12
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : Zero α
inst_3 : One α
j : l ⊕ m
val : l
a :
  ∀ (val_1 : l),
    Eq.{u_12 + 1} (α := α)
      (fromBlocks.{u_1, u_2, u_1, u_2, u_12} (m := m) (o := m) 1 0 0 1 (Sum.inl val) (Sum.inl val_1))
      (1 (Sum.inl val) (Sum.inl val_1))
⊢ Eq.{u_12 + 1} (α := α) (fromBlocks (o := m) 1 0 0 1 (Sum.inl val) j) (1 (Sum.inl val) j)
have a₁ : ∀ (val_1 : m),
  Eq.{u_12 + 1} (α := α) (fromBlocks (l := l) (o := m) 1 0 0 1 (Sum.inl val) (Sum.inr val_1))
    (1 (Sum.inl val) (Sum.inr val_1))
Tactic: rcases j with ⟨⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
l : Type u_1
m : Type u_2
α : Type u_12
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : Zero α
inst_3 : One α
j : l ⊕ m
val : m
⊢ Eq.{u_12 + 1} (α := α) (fromBlocks (n := l) 1 0 0 1 (Sum.inr val) j) (1 (Sum.inr val) j)
have a : ∀ (val_1 : l),
  Eq.{u_12 + 1} (α := α) (fromBlocks (m := m) (n := l) 1 0 0 1 (Sum.inr val) (Sum.inl val_1))
    (1 (Sum.inr val) (Sum.inl val_1))
Tactic: rcases j with ⟨⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
l : Type u_1
m : Type u_2
α : Type u_12
inst : DecidableEq l
inst_1 : DecidableEq m
inst_2 : Zero α
inst_3 : One α
j : l ⊕ m
val : m
a :
  ∀ (val_1 : l),
    Eq.{u_12 + 1} (α := α) (fromBlocks (m := m) (n := l) 1 0 0 1 (Sum.inr val) (Sum.inl val_1))
      (1 (Sum.inr val) (Sum.inl val_1))
⊢ Eq.{u_12 + 1} (α := α) (fromBlocks (n := l) 1 0 0 1 (Sum.inr val) j) (1 (Sum.inr val) j)
have a₁ : ∀ (val_1 : m),
  Eq.{u_12 + 1} (α := α) (fromBlocks.{u_1, u_2, u_1, u_2, u_12} (l := l) (n := l) 1 0 0 1 (Sum.inr val) (Sum.inr val_1))
    (1 (Sum.inr val) (Sum.inr val_1))
Tactic: rcases j with ⟨⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
β : Type u_13
inst : DecidableEq o
inst_1 : Zero α
inst_2 : Zero β
M : o → Matrix m n α
f : α → β
hf : f 0 = 0
⊢ (blockDiagonal M).map f = blockDiagonal fun (k : o) ↦ (M k).map f
have a : ∀ (i : m × o) (j : n × o), (blockDiagonal M).map f i j = blockDiagonal (fun (k : o) ↦ (M k).map f) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
β : Type u_13
inst : DecidableEq o
inst_1 : Zero α
inst_2 : Zero β
M : o → Matrix m n α
f : α → β
hf : f 0 = 0
i : m × o
j : n × o
⊢ (blockDiagonal M).map f i j = blockDiagonal (fun (k : o) ↦ (M k).map f) i j
have a : f (if i.2 = j.2 then M i.2 i.1 j.1 else 0) = if i.2 = j.2 then f (M i.2 i.1 j.1) else 0
Tactic: simp only [map_apply, blockDiagonal_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
β : Type u_13
inst : DecidableEq o
inst_1 : Zero α
inst_2 : Zero β
M : o → Matrix m n α
f : α → β
hf : f 0 = 0
i : m × o
j : n × o
⊢ f (if i.2 = j.2 then M i.2 i.1 j.1 else 0) = if i.2 = j.2 then f (M i.2 i.1 j.1) else 0
have a : (if i.2 = j.2 then f (M i.2 i.1 j.1) else f 0) = if i.2 = j.2 then f (M i.2 i.1 j.1) else 0
Tactic: rw [apply_ite f, hf]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
β : Type u_13
inst : DecidableEq o
inst_1 : Zero α
inst_2 : Zero β
M : o → Matrix m n α
f : α → β
hf : f 0 = 0
i : m × o
j : n × o
a : (if i.2 = j.2 then f (M i.2 i.1 j.1) else f 0) = if i.2 = j.2 then f (M i.2 i.1 j.1) else 0
⊢ f (if i.2 = j.2 then M i.2 i.1 j.1 else 0) = if i.2 = j.2 then f (M i.2 i.1 j.1) else 0
have a₁ : (if i.2 = j.2 then f (M i.2 i.1 j.1) else 0) = if i.2 = j.2 then f (M i.2 i.1 j.1) else 0
Tactic: rw [apply_ite f, hf]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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)ᵀ = blockDiagonal fun (k : o) ↦ (M k)ᵀ
have a : ∀ (i : n × o) (j : m × o), (blockDiagonal M)ᵀ i j = blockDiagonal (fun (k : o) ↦ (M k)ᵀ) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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 α
i : n × o
j : m × o
⊢ (blockDiagonal M)ᵀ i j = blockDiagonal (fun (k : o) ↦ (M k)ᵀ) i j
have a : (if i.2 = j.2 then M i.2 j.1 i.1 else 0) = if i.2 = j.2 then M j.2 j.1 i.1 else 0
Tactic: simp only [transpose_apply, blockDiagonal_apply, eq_comm]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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 α
i : n × o
j : m × o
⊢ (if i.2 = j.2 then M i.2 j.1 i.1 else 0) = if i.2 = j.2 then M j.2 j.1 i.1 else 0
have pos : ∀ (h : i.2 = j.2), M i.2 j.1 i.1 = M j.2 j.1 i.1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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 α
i : n × o
j : m × o
pos : ∀ (h : i.2 = j.2), M i.2 j.1 i.1 = M j.2 j.1 i.1
⊢ (if i.2 = j.2 then M i.2 j.1 i.1 else 0) = if i.2 = j.2 then M j.2 j.1 i.1 else 0
have neg : ∀ (h : ¬i.2 = j.2), Eq.{u_12 + 1} (α := α) 0 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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 α
i : n × o
j : m × o
h : i.2 = j.2
⊢ M i.2 j.1 i.1 = M j.2 j.1 i.1
have pos : M j.2 j.1 i.1 = M j.2 j.1 i.1
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
inst : DecidableEq o
α : Type u_14
inst_1 : AddMonoid α
inst_2 : StarAddMonoid α
M : o → Matrix m n α
⊢ (blockDiagonal M)ᴴ = blockDiagonal fun (k : o) ↦ (M k)ᴴ
have simp : Eq (α := Matrix (n × o) (m × o) α) (map (blockDiagonal fun (k : o) ↦ (M k)ᵀ) star)
  (blockDiagonal fun (k : o) ↦ (M k)ᵀ.map star)
Tactic: simp only [conjTranspose, blockDiagonal_transpose]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
inst : DecidableEq o
α : Type u_14
inst_1 : AddMonoid α
inst_2 : StarAddMonoid α
M : o → Matrix m n α
⊢ Eq (α := Matrix (n × o) (m × o) α) (map (blockDiagonal fun (k : o) ↦ (M k)ᵀ) star)
    (blockDiagonal fun (k : o) ↦ (M k)ᵀ.map star)
have rw : Eq (α := Matrix (n × o) (m × o) α) (blockDiagonal fun (k : o) ↦ (M k)ᵀ.map star)
  (blockDiagonal fun (k : o) ↦ (M k)ᵀ.map star)
Tactic: rw [blockDiagonal_map _ star (star_zero α)]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : DecidableEq o
inst_1 : Zero α
⊢ Eq (α := Matrix (m × o) (n × o) α) (blockDiagonal 0) 0
have a : ∀ (i : m × o) (j : n × o), Eq.{u_12 + 1} (α := α) (blockDiagonal 0 i j) (0 i j)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
m : Type u_2
o : Type u_4
α : Type u_12
inst : DecidableEq o
inst_1 : Zero α
inst_2 : DecidableEq m
d : o → m → α
⊢ Eq (α := Matrix (m × o) (m × o) α) (blockDiagonal fun (k : o) ↦ diagonal (d k))
    (diagonal fun (ik : m × o) ↦ d ik.2 ik.1)
have a : ∀ (i : m) (k : o) (j : m) (k' : o),
  Eq.{u_12 + 1} (α := α) (blockDiagonal (fun (k : o) ↦ diagonal (d k)) (i, k) (j, k'))
    (diagonal (fun (ik : m × o) ↦ d ik.2 ik.1) (i, k) (j, k'))
Tactic: ext ⟨i, k⟩ ⟨j, k'⟩
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
m : Type u_2
o : Type u_4
α : Type u_12
inst : DecidableEq o
inst_1 : Zero α
inst_2 : DecidableEq m
d : o → m → α
i : m
k : o
j : m
k' : o
⊢ Eq.{u_12 + 1} (α := α) (blockDiagonal (fun (k : o) ↦ diagonal (d k)) (i, k) (j, k'))
    (diagonal (fun (ik : m × o) ↦ d ik.2 ik.1) (i, k) (j, k'))
have a : (if k = k' ∧ i = j then d k i else 0) = if i = j ∧ k = k' then d k i else 0
Tactic: simp only [blockDiagonal_apply, diagonal_apply, Prod.mk_inj, ← ite_and]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
m : Type u_2
o : Type u_4
α : Type u_12
inst : DecidableEq o
inst_1 : Zero α
inst_2 : DecidableEq m
d : o → m → α
i : m
k : o
j : m
k' : o
⊢ (if k = k' ∧ i = j then d k i else 0) = if i = j ∧ k = k' then d k i else 0
have a : (k = k' ∧ i = j) = (i = j ∧ k = k')
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
m : Type u_2
o : Type u_4
α : Type u_12
inst : DecidableEq o
inst_1 : Zero α
inst_2 : DecidableEq m
d : o → m → α
i : m
k : o
j : m
k' : o
⊢ (k = k' ∧ i = j) = (i = j ∧ k = k')
have a : (i = j ∧ k = k') = (i = j ∧ k = k')
Tactic: rw [and_comm]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
Goal:
m : Type u_2
o : Type u_4
α : Type u_12
inst : DecidableEq o
inst_1 : Zero α
inst_2 : DecidableEq m
inst_3 : One α
⊢ Eq (α := Matrix (m × o) (m × o) α) (blockDiagonal fun (x : o) ↦ diagonal fun (x : m) ↦ 1)
    (diagonal fun (x : m × o) ↦ 1)
have rw : Eq (α := Matrix (m × o) (m × o) α) (diagonal fun (ik : m × o) ↦ 1) (diagonal fun (x : m × o) ↦ 1)
Tactic: rw [blockDiagonal_diagonal]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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 α
⊢ blockDiagonal (M + N) = blockDiagonal M + blockDiagonal N
have a : ∀ (i : m × o) (j : n × o), blockDiagonal (M + N) i j = (blockDiagonal M + blockDiagonal N) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ blockDiagonal (M + N) i j = (blockDiagonal M + blockDiagonal N) i j
have 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
Tactic: simp only [blockDiagonal_apply, Pi.add_apply, add_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ (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
have 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
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ (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
have neg : ¬i.2 = j.2 → 0 = HAdd.hAdd (α := α) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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 α
⊢ (blockDiagonal fun (k : o) ↦ M k * N k) = blockDiagonal M * blockDiagonal N
have 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')
Tactic: ext ⟨i, k⟩ ⟨j, k'⟩
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ blockDiagonal (fun (k : o) ↦ M k * N k) (i, k) (j, k') = (blockDiagonal M * blockDiagonal N) (i, k) (j, k')
have 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)
Tactic: simp only [blockDiagonal_apply, mul_apply, ← Finset.univ_product_univ, Finset.sum_product]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ 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)
have 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)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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)
⊢ 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)
have 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)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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 α
⊢ blockDiagonal (x • M) = x • blockDiagonal M
have a : ∀ (i : m × o) (j : n × o), blockDiagonal (x • M) i j = (x • blockDiagonal M) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ blockDiagonal (x • M) i j = (x • blockDiagonal M) i j
have 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
Tactic: simp only [blockDiagonal_apply, Pi.smul_apply, smul_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ (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
have pos : i.2 = j.2 → x • M i.2 i.1 j.1 = x • M i.2 i.1 j.1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ (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
have neg : ¬i.2 = j.2 → 0 = HSMul.hSMul (β := α) x 0
Tactic: split_ifs