awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : Fintype l
inst_1 : Fintype m
inst_2 : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : l ⊕ m → α
val : o
⊢ (fromBlocks A B C D *ᵥ x) (Sum.inr val) =
    Sum.elim (A *ᵥ x ∘ Sum.inl + B *ᵥ x ∘ Sum.inr) (C *ᵥ x ∘ Sum.inl + D *ᵥ x ∘ Sum.inr) (Sum.inr val)

Tactic:
simp [mulVec, dotProduct]

Premises used: dotProduct, Matrix.mulVec
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : Fintype n
inst_1 : Fintype o
inst_2 : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : n ⊕ o → α
h :
  ∀ (i : l ⊕ m),
    (x ᵥ* fromBlocks A B C D) i = Sum.elim (x ∘ Sum.inl ᵥ* A + x ∘ Sum.inr ᵥ* C) (x ∘ Sum.inl ᵥ* B + x ∘ Sum.inr ᵥ* D) i
⊢ x ᵥ* fromBlocks A B C D = Sum.elim (x ∘ Sum.inl ᵥ* A + x ∘ Sum.inr ᵥ* C) (x ∘ Sum.inl ᵥ* B + x ∘ Sum.inr ᵥ* D)

Tactic:
ext i
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : Fintype n
inst_1 : Fintype o
inst_2 : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : n ⊕ o → α
i : l ⊕ m
h :
  ∀ (val : l),
    (x ᵥ* fromBlocks A B C D) (Sum.inl val) =
      Sum.elim (x ∘ Sum.inl ᵥ* A + x ∘ Sum.inr ᵥ* C) (x ∘ Sum.inl ᵥ* B + x ∘ Sum.inr ᵥ* D) (Sum.inl val)
h₁ :
  ∀ (val : m),
    (x ᵥ* fromBlocks A B C D) (Sum.inr val) =
      Sum.elim (x ∘ Sum.inl ᵥ* A + x ∘ Sum.inr ᵥ* C) (x ∘ Sum.inl ᵥ* B + x ∘ Sum.inr ᵥ* D) (Sum.inr val)
⊢ (x ᵥ* fromBlocks A B C D) i = Sum.elim (x ∘ Sum.inl ᵥ* A + x ∘ Sum.inr ᵥ* C) (x ∘ Sum.inl ᵥ* B + x ∘ Sum.inr ᵥ* D) i

Tactic:
cases i
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : Fintype n
inst_1 : Fintype o
inst_2 : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : n ⊕ o → α
val : l
⊢ (x ᵥ* fromBlocks A B C D) (Sum.inl val) =
    Sum.elim (x ∘ Sum.inl ᵥ* A + x ∘ Sum.inr ᵥ* C) (x ∘ Sum.inl ᵥ* B + x ∘ Sum.inr ᵥ* D) (Sum.inl val)

Tactic:
simp [vecMul, dotProduct]

Premises used: dotProduct, Matrix.vecMul
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : Fintype n
inst_1 : Fintype o
inst_2 : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : n ⊕ o → α
val : m
⊢ (x ᵥ* fromBlocks A B C D) (Sum.inr val) =
    Sum.elim (x ∘ Sum.inl ᵥ* A + x ∘ Sum.inr ᵥ* C) (x ∘ Sum.inl ᵥ* B + x ∘ Sum.inr ᵥ* D) (Sum.inr val)

Tactic:
simp [vecMul, dotProduct]

Premises used: dotProduct, Matrix.vecMul
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
α : Type u_12
inst : DecidableEq m
inst_1 : Zero α
d : m → α
p : m → Prop
a : ∀ (i j : { a : m // p a }), (diagonal d).toBlock p p i j = diagonal (fun (i : Subtype p) ↦ d (↑i : m)) i j
⊢ (diagonal d).toBlock p p = diagonal fun (i : Subtype p) ↦ d (↑i : m)

Tactic:
ext i j
-- Module: Mathlib.Data.Matrix.Block
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
neg : ∀ (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

Tactic:
by_cases h : i = j
-- Module: Mathlib.Data.Matrix.Block
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 }
h : i = j
⊢ (diagonal d).toBlock p p i j = diagonal (fun (i : Subtype p) ↦ d (↑i : m)) i j

Tactic:
simp [h]
-- Module: Mathlib.Data.Matrix.Block
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 }
h : ¬i = j
⊢ (diagonal d).toBlock p p i j = diagonal (fun (i : Subtype p) ↦ d (↑i : m)) i j

Tactic:
simp [h, Subtype.val_injective.ne h]

Premises used: Subtype.val_injective, Function.Injective.ne
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
α : Type u_12
inst : DecidableEq m
inst_1 : Zero α
d : m → α
p q : m → Prop
hpq : Disjoint p q
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)
⊢ (diagonal d).toBlock p q = 0

Tactic:
ext ⟨i, hi⟩ ⟨j, hj⟩
-- Module: Mathlib.Data.Matrix.Block
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
⊢ i ≠ j

Tactic:
have : i ≠ j := fun heq => hpq.le_bot i ⟨hi, heq.symm ▸ hj⟩
-- Module: Mathlib.Data.Matrix.Block
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
this : i ≠ 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:
simp [diagonal_apply_ne d this]

Premises used: Matrix.diagonal_apply_ne
-- Module: Mathlib.Data.Matrix.Block
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 → α
a : ∀ (i j : l ⊕ m), fromBlocks (diagonal d₁) 0 0 (diagonal d₂) i j = diagonal (Sum.elim d₁ d₂) i j
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) = diagonal (Sum.elim d₁ d₂)

Tactic:
ext i j
-- Module: Mathlib.Data.Matrix.Block
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
a₁ : ∀ (val : m), fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inr val) j = diagonal (Sum.elim d₁ d₂) (Sum.inr val) j
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) i j = diagonal (Sum.elim d₁ d₂) i j

Tactic:
rcases i with ⟨⟩
-- Module: Mathlib.Data.Matrix.Block
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)
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)
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inl val) j = diagonal (Sum.elim d₁ d₂) (Sum.inl val) j

Tactic:
rcases j with ⟨⟩
-- Module: Mathlib.Data.Matrix.Block
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)
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)
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) (Sum.inr val) j = diagonal (Sum.elim d₁ d₂) (Sum.inr val) j

Tactic:
rcases j with ⟨⟩
-- Module: Mathlib.Data.Matrix.Block
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 → α
val 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:
simp [diagonal]

Premises used: Matrix.diagonal
-- Module: Mathlib.Data.Matrix.Block
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 → α
val : l
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:
simp [diagonal]

Premises used: Matrix.diagonal
-- Module: Mathlib.Data.Matrix.Block
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 → α
val : m
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:
simp [diagonal]

Premises used: Matrix.diagonal
-- Module: Mathlib.Data.Matrix.Block
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 → α
val 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:
simp [diagonal]

Premises used: Matrix.diagonal
-- Module: Mathlib.Data.Matrix.Block
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 → α
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 : α)
⊢ 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))

Tactic:
funext i j
-- Module: Mathlib.Data.Matrix.Block
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 → α
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:
simp only [Sum.inl.injEq, of_apply, diagonal_apply]

Premises used: Sum.inl.injEq, Matrix.of_apply, Matrix.diagonal_apply
-- Module: Mathlib.Data.Matrix.Block
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 → α
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 : α)
⊢ 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))

Tactic:
funext i j
-- Module: Mathlib.Data.Matrix.Block
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 → α
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:
simp only [Sum.inr.injEq, of_apply, diagonal_apply]

Premises used: Sum.inr.injEq, Matrix.of_apply, Matrix.diagonal_apply
-- Module: Mathlib.Data.Matrix.Block
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 → α
⊢ (diagonal v).toBlocks₁₂ = 0

Tactic:
rfl

Premises used: Matrix.toBlocks₁₂, Matrix.diagonal, rfl, ite
-- Module: Mathlib.Data.Matrix.Block
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 → α
⊢ (diagonal v).toBlocks₂₁ = 0

Tactic:
rfl

Premises used: Matrix.toBlocks₂₁, Matrix.diagonal, rfl, ite
-- Module: Mathlib.Data.Matrix.Block
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 α
a : ∀ (i j : l ⊕ m), Eq.{u_12 + 1} (α := α) (fromBlocks 1 0 0 1 i j) (1 i j)
⊢ Eq (α := Matrix (l ⊕ m) (l ⊕ m) α) (fromBlocks 1 0 0 1) 1

Tactic:
ext i j
-- Module: Mathlib.Data.Matrix.Block
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)
a₁ : ∀ (val : m), Eq.{u_12 + 1} (α := α) (fromBlocks (n := l) 1 0 0 1 (Sum.inr val) j) (1 (Sum.inr val) j)
⊢ Eq.{u_12 + 1} (α := α) (fromBlocks 1 0 0 1 i j) (1 i j)

Tactic:
rcases i with ⟨⟩
-- Module: Mathlib.Data.Matrix.Block
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))
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))
⊢ Eq.{u_12 + 1} (α := α) (fromBlocks (o := m) 1 0 0 1 (Sum.inl val) j) (1 (Sum.inl val) j)

Tactic:
rcases j with ⟨⟩
-- Module: Mathlib.Data.Matrix.Block
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))
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))
⊢ Eq.{u_12 + 1} (α := α) (fromBlocks (n := l) 1 0 0 1 (Sum.inr val) j) (1 (Sum.inr val) j)

Tactic:
rcases j with ⟨⟩
-- Module: Mathlib.Data.Matrix.Block
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 α
val 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:
simp [one_apply]

Premises used: Matrix.one_apply
-- Module: Mathlib.Data.Matrix.Block
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 α
val : l
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:
simp [one_apply]

Premises used: Matrix.one_apply
-- Module: Mathlib.Data.Matrix.Block
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 α
val : m
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:
simp [one_apply]

Premises used: Matrix.one_apply
-- Module: Mathlib.Data.Matrix.Block
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 α
val 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:
simp [one_apply]

Premises used: Matrix.one_apply
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
α : Type u_12
inst : DecidableEq m
inst_1 : Zero α
inst_2 : One α
p : m → Prop
⊢ Eq (α := Matrix.{u_2, u_2, u_12} { a : m // p a } { a : m // p a } α) (toBlock 1 p p) 1

Tactic:
toBlock_diagonal_self _ p

Premises used: Matrix.toBlock_diagonal_self
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
α : Type u_12
inst : DecidableEq m
inst_1 : Zero α
inst_2 : One α
p q : m → Prop
hpq : Disjoint p q
⊢ Eq (α := Matrix.{u_2, u_2, u_12} { a : m // p a } { a : m // q a } α) (toBlock 1 p q) 0

Tactic:
toBlock_diagonal_disjoint _ hpq

Premises used: Matrix.toBlock_diagonal_disjoint
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : DecidableEq o
inst_1 : Zero α
M : o → Matrix m n α
i : m
k : o
j : n
k' : o
⊢ blockDiagonal M (i, k) (j, k') = if k = k' then M k i j else 0

Tactic:
rfl

Premises used: Matrix.blockDiagonal, rfl, ite
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : DecidableEq o
inst_1 : Zero α
M : o → Matrix m n α
ik : m × o
jk : n × o
⊢ blockDiagonal M ik jk = if ik.2 = jk.2 then M ik.2 ik.1 jk.1 else 0

Tactic:
rfl

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

Tactic:
if_pos rfl

Premises used: Matrix.blockDiagonal, if_pos, rfl, ite
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : DecidableEq o
inst_1 : Zero α
M : o → Matrix m n α
i : m
j : n
k k' : o
h : k ≠ k'
⊢ blockDiagonal M (i, k) (j, k') = 0

Tactic:
if_neg h

Premises used: Matrix.blockDiagonal, if_neg, ite
-- Module: Mathlib.Data.Matrix.Block
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
a : ∀ (i : m × o) (j : n × o), (blockDiagonal M).map f i j = blockDiagonal (fun (k : o) ↦ (M k).map f) i j
⊢ (blockDiagonal M).map f = blockDiagonal fun (k : o) ↦ (M k).map f

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Block
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 : 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
⊢ (blockDiagonal M).map f i j = blockDiagonal (fun (k : o) ↦ (M k).map f) i j

Tactic:
simp only [map_apply, blockDiagonal_apply]

Premises used: Matrix.map_apply, Matrix.blockDiagonal_apply
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
β : 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
a₁ 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
⊢ 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:
rw [apply_ite f, hf]

Premises used: apply_ite
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : DecidableEq o
inst_1 : Zero α
M : o → Matrix m n α
a : ∀ (i : n × o) (j : m × o), (blockDiagonal M)ᵀ i j = blockDiagonal (fun (k : o) ↦ (M k)ᵀ) i j
⊢ (blockDiagonal M)ᵀ = blockDiagonal fun (k : o) ↦ (M k)ᵀ

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : DecidableEq o
inst_1 : Zero α
M : o → Matrix m n α
i : n × o
j : m × o
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
⊢ (blockDiagonal M)ᵀ i j = blockDiagonal (fun (k : o) ↦ (M k)ᵀ) i j

Tactic:
simp only [transpose_apply, blockDiagonal_apply, eq_comm]

Premises used: eq_comm, Matrix.transpose_apply, Matrix.blockDiagonal_apply
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : DecidableEq o
inst_1 : 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
neg : ∀ (h : ¬i.2 = j.2), Eq.{u_12 + 1} (α := α) 0 0
⊢ (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:
split_ifs with h
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : DecidableEq o
inst_1 : Zero α
M : o → Matrix m n α
i : n × o
j : m × o
h : i.2 = j.2
pos pos₁ : M j.2 j.1 i.1 = M j.2 j.1 i.1
⊢ M i.2 j.1 i.1 = M j.2 j.1 i.1

Tactic:
rw [h]
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : DecidableEq o
inst_1 : Zero α
M : o → Matrix m n α
i : n × o
j : m × o
h : ¬i.2 = j.2
⊢ Eq.{u_12 + 1} (α := α) 0 0

Tactic:
rfl
-- Module: Mathlib.Data.Matrix.Block
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 α
simp :
  Eq (α := Matrix (n × o) (m × o) α) (map (blockDiagonal fun (k : o) ↦ (M k)ᵀ) star)
    (blockDiagonal fun (k : o) ↦ (M k)ᵀ.map star)
⊢ (blockDiagonal M)ᴴ = blockDiagonal fun (k : o) ↦ (M k)ᴴ

Tactic:
simp only [conjTranspose, blockDiagonal_transpose]

Premises used: Matrix.blockDiagonal_transpose, Matrix.conjTranspose
-- Module: Mathlib.Data.Matrix.Block
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 α
rw rw₁ :
  Eq (α := Matrix (n × o) (m × o) α) (blockDiagonal fun (k : o) ↦ (M k)ᵀ.map star)
    (blockDiagonal fun (k : o) ↦ (M k)ᵀ.map star)
⊢ Eq (α := Matrix (n × o) (m × o) α) (map (blockDiagonal fun (k : o) ↦ (M k)ᵀ) star)
    (blockDiagonal fun (k : o) ↦ (M k)ᵀ.map star)

Tactic:
rw [blockDiagonal_map _ star (star_zero α)]

Premises used: Matrix.blockDiagonal_map, star_zero, Star.star
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : DecidableEq o
inst_1 : Zero α
a : ∀ (i : m × o) (j : n × o), Eq.{u_12 + 1} (α := α) (blockDiagonal 0 i j) (0 i j)
⊢ Eq (α := Matrix (m × o) (n × o) α) (blockDiagonal 0) 0

Tactic:
ext
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : DecidableEq o
inst_1 : Zero α
i : m × o
j : n × o
⊢ Eq.{u_12 + 1} (α := α) (blockDiagonal 0 i j) (0 i j)

Tactic:
simp [blockDiagonal_apply]

Premises used: Matrix.blockDiagonal_apply
-- Module: Mathlib.Data.Matrix.Block
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 → α
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'))
⊢ Eq (α := Matrix (m × o) (m × o) α) (blockDiagonal fun (k : o) ↦ diagonal (d k))
    (diagonal fun (ik : m × o) ↦ d ik.2 ik.1)

Tactic:
ext ⟨i, k⟩ ⟨j, k'⟩
-- Module: Mathlib.Data.Matrix.Block
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
a : (if k = k' ∧ i = j then d k i else 0) = if i = j ∧ k = k' then d k i else 0
⊢ 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:
simp only [blockDiagonal_apply, diagonal_apply, Prod.mk_inj, ← ite_and]

Premises used: Prod.mk_inj, Matrix.diagonal_apply, ite_and, Matrix.blockDiagonal_apply
-- Module: Mathlib.Data.Matrix.Block
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
a : (k = k' ∧ i = j) = (i = j ∧ k = k')
⊢ (if k = k' ∧ i = j then d k i else 0) = if i = j ∧ k = k' then d k i else 0

Tactic:
congr 1
-- Module: Mathlib.Data.Matrix.Block
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
a a₁ : (i = j ∧ k = k') = (i = j ∧ k = k')
⊢ (k = k' ∧ i = j) = (i = j ∧ k = k')

Tactic:
rw [and_comm]

Premises used: and_comm
-- Module: Mathlib.Data.Matrix.Block
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 α
rw rw₁ : Eq (α := Matrix (m × o) (m × o) α) (diagonal fun (ik : m × o) ↦ 1) (diagonal fun (x : m × o) ↦ 1)
⊢ Eq (α := Matrix (m × o) (m × o) α) (blockDiagonal fun (x : o) ↦ diagonal fun (x : m) ↦ 1)
    (diagonal fun (x : m × o) ↦ 1)

Tactic:
rw [blockDiagonal_diagonal]

Premises used: Matrix.blockDiagonal_diagonal
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst : DecidableEq o
inst_1 : AddZeroClass α
M N : o → Matrix m n α
a : ∀ (i : m × o) (j : n × o), blockDiagonal (M + N) i j = (blockDiagonal M + blockDiagonal N) i j
⊢ blockDiagonal (M + N) = blockDiagonal M + blockDiagonal N

Tactic:
ext