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
A B : Matrix (n ⊕ o) (l ⊕ m) α
h :
  A.toBlocks₁₁ = B.toBlocks₁₁ ∧ A.toBlocks₁₂ = B.toBlocks₁₂ ∧ A.toBlocks₂₁ = B.toBlocks₂₁ ∧ A.toBlocks₂₂ = B.toBlocks₂₂
h₁₁ : A.toBlocks₁₁ = B.toBlocks₁₁
h₁₂ : A.toBlocks₁₂ = B.toBlocks₁₂
h₂₁ : A.toBlocks₂₁ = B.toBlocks₂₁
h₂₂ : A.toBlocks₂₂ = B.toBlocks₂₂
rw : fromBlocks A.toBlocks₁₁ A.toBlocks₁₂ A.toBlocks₂₁ A.toBlocks₂₂ = B
rw₁ :
  fromBlocks A.toBlocks₁₁ A.toBlocks₁₂ A.toBlocks₂₁ A.toBlocks₂₂ =
    fromBlocks B.toBlocks₁₁ B.toBlocks₁₂ B.toBlocks₂₁ B.toBlocks₂₂
rw₂ :
  fromBlocks B.toBlocks₁₁ A.toBlocks₁₂ A.toBlocks₂₁ A.toBlocks₂₂ =
    fromBlocks B.toBlocks₁₁ B.toBlocks₁₂ B.toBlocks₂₁ B.toBlocks₂₂
rw₃ :
  fromBlocks B.toBlocks₁₁ B.toBlocks₁₂ A.toBlocks₂₁ A.toBlocks₂₂ =
    fromBlocks B.toBlocks₁₁ B.toBlocks₁₂ B.toBlocks₂₁ B.toBlocks₂₂
rw₄ :
  fromBlocks B.toBlocks₁₁ B.toBlocks₁₂ B.toBlocks₂₁ A.toBlocks₂₂ =
    fromBlocks B.toBlocks₁₁ B.toBlocks₁₂ B.toBlocks₂₁ B.toBlocks₂₂
rw₅ rw₆ :
  fromBlocks B.toBlocks₁₁ B.toBlocks₁₂ B.toBlocks₂₁ B.toBlocks₂₂ =
    fromBlocks B.toBlocks₁₁ B.toBlocks₁₂ B.toBlocks₂₁ B.toBlocks₂₂
⊢ A = B

Tactic:
rw [← fromBlocks_toBlocks A, ← fromBlocks_toBlocks B, h₁₁, h₁₂, h₂₁, h₂₂]

Premises used: Matrix.fromBlocks_toBlocks
-- 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
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix n l α
B' : Matrix n m α
C' : Matrix o l α
D' : Matrix o m α
⊢ fromBlocks A B C D = fromBlocks A' B' C' D' ↔ A = A' ∧ B = B' ∧ C = C' ∧ D = D'

Tactic:
ext_iff_blocks

Premises used: Matrix.fromBlocks, Matrix.ext_iff_blocks, Matrix.toBlocks₁₂, Matrix.toBlocks₂₁, Matrix.toBlocks₁₁, Matrix.toBlocks₂₂, Sum.elim
-- 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
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
a : ∀ (i : n ⊕ o) (j : l ⊕ m), (fromBlocks A B C D).map f i j = fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) i j
⊢ (fromBlocks A B C D).map f = fromBlocks (A.map f) (B.map f) (C.map f) (D.map f)

Tactic:
ext i j
-- 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
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
i : n ⊕ o
j : l ⊕ m
a :
  ∀ (val : n),
    (fromBlocks A B C D).map f (Sum.inl val) j = fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) (Sum.inl val) j
a₁ :
  ∀ (val : o),
    (fromBlocks A B C D).map f (Sum.inr val) j = fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) (Sum.inr val) j
⊢ (fromBlocks A B C D).map f i j = fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) i j

Tactic:
rcases i with ⟨⟩
-- 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
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
j : l ⊕ m
val : n
a :
  ∀ (val_1 : l),
    (fromBlocks A B C D).map f (Sum.inl val) (Sum.inl val_1) =
      fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) (Sum.inl val) (Sum.inl val_1)
a₁ :
  ∀ (val_1 : m),
    (fromBlocks A B C D).map f (Sum.inl val) (Sum.inr val_1) =
      fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) (Sum.inl val) (Sum.inr val_1)
⊢ (fromBlocks A B C D).map f (Sum.inl val) j = fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) (Sum.inl val) j

Tactic:
rcases j with ⟨⟩
-- 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
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
j : l ⊕ m
val : o
a :
  ∀ (val_1 : l),
    (fromBlocks A B C D).map f (Sum.inr val) (Sum.inl val_1) =
      fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) (Sum.inr val) (Sum.inl val_1)
a₁ :
  ∀ (val_1 : m),
    (fromBlocks A B C D).map f (Sum.inr val) (Sum.inr val_1) =
      fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) (Sum.inr val) (Sum.inr val_1)
⊢ (fromBlocks A B C D).map f (Sum.inr val) j = fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) (Sum.inr val) j

Tactic:
rcases j with ⟨⟩
-- 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
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
val : n
val_1 : l
⊢ (fromBlocks A B C D).map f (Sum.inl val) (Sum.inl val_1) =
    fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) (Sum.inl val) (Sum.inl val_1)

Tactic:
simp [fromBlocks]

Premises used: Matrix.fromBlocks
-- 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
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
val : n
val_1 : m
⊢ (fromBlocks A B C D).map f (Sum.inl val) (Sum.inr val_1) =
    fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) (Sum.inl val) (Sum.inr val_1)

Tactic:
simp [fromBlocks]

Premises used: Matrix.fromBlocks
-- 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
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
val : o
val_1 : l
⊢ (fromBlocks A B C D).map f (Sum.inr val) (Sum.inl val_1) =
    fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) (Sum.inr val) (Sum.inl val_1)

Tactic:
simp [fromBlocks]

Premises used: Matrix.fromBlocks
-- 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
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
val : o
val_1 : m
⊢ (fromBlocks A B C D).map f (Sum.inr val) (Sum.inr val_1) =
    fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) (Sum.inr val) (Sum.inr val_1)

Tactic:
simp [fromBlocks]

Premises used: Matrix.fromBlocks
-- 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
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
a : ∀ (i : l ⊕ m) (j : n ⊕ o), (fromBlocks A B C D)ᵀ i j = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ i j
⊢ (fromBlocks A B C D)ᵀ = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ

Tactic:
ext i j
-- 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
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
i : l ⊕ m
j : n ⊕ o
a : ∀ (val : l), (fromBlocks A B C D)ᵀ (Sum.inl val) j = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ (Sum.inl val) j
a₁ : ∀ (val : m), (fromBlocks A B C D)ᵀ (Sum.inr val) j = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ (Sum.inr val) j
⊢ (fromBlocks A B C D)ᵀ i j = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ i j

Tactic:
rcases i with ⟨⟩
-- 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
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
j : n ⊕ o
val : l
a :
  ∀ (val_1 : n),
    (fromBlocks A B C D)ᵀ (Sum.inl val) (Sum.inl val_1) = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ (Sum.inl val) (Sum.inl val_1)
a₁ :
  ∀ (val_1 : o),
    (fromBlocks A B C D)ᵀ (Sum.inl val) (Sum.inr val_1) = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ (Sum.inl val) (Sum.inr val_1)
⊢ (fromBlocks A B C D)ᵀ (Sum.inl val) j = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ (Sum.inl val) j

Tactic:
rcases j with ⟨⟩
-- 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
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
j : n ⊕ o
val : m
a :
  ∀ (val_1 : n),
    (fromBlocks A B C D)ᵀ (Sum.inr val) (Sum.inl val_1) = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ (Sum.inr val) (Sum.inl val_1)
a₁ :
  ∀ (val_1 : o),
    (fromBlocks A B C D)ᵀ (Sum.inr val) (Sum.inr val_1) = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ (Sum.inr val) (Sum.inr val_1)
⊢ (fromBlocks A B C D)ᵀ (Sum.inr val) j = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ (Sum.inr val) j

Tactic:
rcases j with ⟨⟩
-- 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
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val : l
val_1 : n
⊢ (fromBlocks A B C D)ᵀ (Sum.inl val) (Sum.inl val_1) = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ (Sum.inl val) (Sum.inl val_1)

Tactic:
simp [fromBlocks]

Premises used: Matrix.fromBlocks
-- 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
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val : l
val_1 : o
⊢ (fromBlocks A B C D)ᵀ (Sum.inl val) (Sum.inr val_1) = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ (Sum.inl val) (Sum.inr val_1)

Tactic:
simp [fromBlocks]

Premises used: Matrix.fromBlocks
-- 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
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val : m
val_1 : n
⊢ (fromBlocks A B C D)ᵀ (Sum.inr val) (Sum.inl val_1) = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ (Sum.inr val) (Sum.inl val_1)

Tactic:
simp [fromBlocks]

Premises used: Matrix.fromBlocks
-- 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
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val : m
val_1 : o
⊢ (fromBlocks A B C D)ᵀ (Sum.inr val) (Sum.inr val_1) = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ (Sum.inr val) (Sum.inr val_1)

Tactic:
simp [fromBlocks]

Premises used: Matrix.fromBlocks
-- 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 : Star α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
⊢ (fromBlocks A B C D)ᴴ = fromBlocks Aᴴ Cᴴ Bᴴ Dᴴ

Tactic:
simp only [conjTranspose, fromBlocks_transpose, fromBlocks_map]

Premises used: Matrix.fromBlocks_transpose, Matrix.fromBlocks_map, Matrix.conjTranspose
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
a : ∀ (i : o ⊕ n) (j : p), (fromBlocks A B C D).submatrix Sum.swap f i j = (fromBlocks C D A B).submatrix id f i j
⊢ (fromBlocks A B C D).submatrix Sum.swap f = (fromBlocks C D A B).submatrix id f

Tactic:
ext i j
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
i : o ⊕ n
j : p
a :
  ∀ (val : o),
    (fromBlocks A B C D).submatrix Sum.swap f (Sum.inl val) j = (fromBlocks C D A B).submatrix id f (Sum.inl val) j
a₁ :
  ∀ (val : n),
    (fromBlocks A B C D).submatrix Sum.swap f (Sum.inr val) j = (fromBlocks C D A B).submatrix id f (Sum.inr val) j
⊢ (fromBlocks A B C D).submatrix Sum.swap f i j = (fromBlocks C D A B).submatrix id f i j

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
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val : o
a : fromBlocks A B C D (Sum.inr val) (f j) = fromBlocks C D A B (Sum.inl val) (f j)
⊢ (fromBlocks A B C D).submatrix Sum.swap f (Sum.inl val) j = (fromBlocks C D A B).submatrix id f (Sum.inl val) j

Tactic:
dsimp
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val : n
a : fromBlocks A B C D (Sum.inl val) (f j) = fromBlocks C D A B (Sum.inr val) (f j)
⊢ (fromBlocks A B C D).submatrix Sum.swap f (Sum.inr val) j = (fromBlocks C D A B).submatrix id f (Sum.inr val) j

Tactic:
dsimp
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val : o
a : ∀ (val_1 : l), fromBlocks A B C D (Sum.inr val) (Sum.inl val_1) = fromBlocks C D A B (Sum.inl val) (Sum.inl val_1)
a₁ : ∀ (val_1 : m), fromBlocks A B C D (Sum.inr val) (Sum.inr val_1) = fromBlocks C D A B (Sum.inl val) (Sum.inr val_1)
⊢ fromBlocks A B C D (Sum.inr val) (f j) = fromBlocks C D A B (Sum.inl val) (f j)

Tactic:
cases f j
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val : n
a : ∀ (val_1 : l), fromBlocks A B C D (Sum.inl val) (Sum.inl val_1) = fromBlocks C D A B (Sum.inr val) (Sum.inl val_1)
a₁ : ∀ (val_1 : m), fromBlocks A B C D (Sum.inl val) (Sum.inr val_1) = fromBlocks C D A B (Sum.inr val) (Sum.inr val_1)
⊢ fromBlocks A B C D (Sum.inl val) (f j) = fromBlocks C D A B (Sum.inr val) (f j)

Tactic:
cases f j
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val : o
val_1 : l
⊢ fromBlocks A B C D (Sum.inr val) (Sum.inl val_1) = fromBlocks C D A B (Sum.inl val) (Sum.inl val_1)

Tactic:
rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val : o
val_1 : m
⊢ fromBlocks A B C D (Sum.inr val) (Sum.inr val_1) = fromBlocks C D A B (Sum.inl val) (Sum.inr val_1)

Tactic:
rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val : n
val_1 : l
⊢ fromBlocks A B C D (Sum.inl val) (Sum.inl val_1) = fromBlocks C D A B (Sum.inr val) (Sum.inl val_1)

Tactic:
rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val : n
val_1 : m
⊢ fromBlocks A B C D (Sum.inl val) (Sum.inr val_1) = fromBlocks C D A B (Sum.inr val) (Sum.inr val_1)

Tactic:
rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
a : ∀ (i : p) (j : m ⊕ l), (fromBlocks A B C D).submatrix f Sum.swap i j = (fromBlocks B A D C).submatrix f id i j
⊢ (fromBlocks A B C D).submatrix f Sum.swap = (fromBlocks B A D C).submatrix f id

Tactic:
ext i j
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
j : m ⊕ l
a :
  ∀ (val : m),
    (fromBlocks A B C D).submatrix f Sum.swap i (Sum.inl val) = (fromBlocks B A D C).submatrix f id i (Sum.inl val)
a₁ :
  ∀ (val : l),
    (fromBlocks A B C D).submatrix f Sum.swap i (Sum.inr val) = (fromBlocks B A D C).submatrix f id i (Sum.inr val)
⊢ (fromBlocks A B C D).submatrix f Sum.swap i j = (fromBlocks B A D C).submatrix f id i j

Tactic:
cases j
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val : m
a : fromBlocks A B C D (f i) (Sum.inr val) = fromBlocks B A D C (f i) (Sum.inl val)
⊢ (fromBlocks A B C D).submatrix f Sum.swap i (Sum.inl val) = (fromBlocks B A D C).submatrix f id i (Sum.inl val)

Tactic:
dsimp
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val : l
a : fromBlocks A B C D (f i) (Sum.inl val) = fromBlocks B A D C (f i) (Sum.inr val)
⊢ (fromBlocks A B C D).submatrix f Sum.swap i (Sum.inr val) = (fromBlocks B A D C).submatrix f id i (Sum.inr val)

Tactic:
dsimp
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val : m
a : ∀ (val_1 : n), fromBlocks A B C D (Sum.inl val_1) (Sum.inr val) = fromBlocks B A D C (Sum.inl val_1) (Sum.inl val)
a₁ : ∀ (val_1 : o), fromBlocks A B C D (Sum.inr val_1) (Sum.inr val) = fromBlocks B A D C (Sum.inr val_1) (Sum.inl val)
⊢ fromBlocks A B C D (f i) (Sum.inr val) = fromBlocks B A D C (f i) (Sum.inl val)

Tactic:
cases f i
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val : l
a : ∀ (val_1 : n), fromBlocks A B C D (Sum.inl val_1) (Sum.inl val) = fromBlocks B A D C (Sum.inl val_1) (Sum.inr val)
a₁ : ∀ (val_1 : o), fromBlocks A B C D (Sum.inr val_1) (Sum.inl val) = fromBlocks B A D C (Sum.inr val_1) (Sum.inr val)
⊢ fromBlocks A B C D (f i) (Sum.inl val) = fromBlocks B A D C (f i) (Sum.inr val)

Tactic:
cases f i
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val : m
val_1 : n
⊢ fromBlocks A B C D (Sum.inl val_1) (Sum.inr val) = fromBlocks B A D C (Sum.inl val_1) (Sum.inl val)

Tactic:
rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val : m
val_1 : o
⊢ fromBlocks A B C D (Sum.inr val_1) (Sum.inr val) = fromBlocks B A D C (Sum.inr val_1) (Sum.inl val)

Tactic:
rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val : l
val_1 : n
⊢ fromBlocks A B C D (Sum.inl val_1) (Sum.inl val) = fromBlocks B A D C (Sum.inl val_1) (Sum.inr val)

Tactic:
rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val : l
val_1 : o
⊢ fromBlocks A B C D (Sum.inr val_1) (Sum.inl val) = fromBlocks B A D C (Sum.inr val_1) (Sum.inr val)

Tactic:
rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_14
m : Type u_15
n : Type u_16
o : Type u_17
α : Type u_18
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
⊢ (fromBlocks A B C D).submatrix Sum.swap Sum.swap = fromBlocks D C B A

Tactic:
simp
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
n : Type u_3
α : Type u_12
M : Matrix m n α
p : m → Prop
q : n → Prop
i : { a : m // p a }
j : { a : n // q a }
⊢ M.toBlock p q i j = M (↑i : m) (↑j : n)

Tactic:
rfl

Premises used: Matrix.submatrix, Matrix.toBlock, rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
α : Type u_12
M : Matrix m m α
p : m → Prop
⊢ M.toSquareBlockProp p =
    (of : (a : { a : m // p a } → { a : m // p a } → α) → Matrix { a : m // p a } { a : m // p a } α)
      fun (i j : { a : m // p a }) ↦ M (↑i : m) (↑j : m)

Tactic:
rfl

Premises used: Matrix.submatrix, Matrix.toBlock, Matrix.toSquareBlockProp, rfl
-- Module: Mathlib.Data.Matrix.Block
Goal:
m : Type u_2
α : Type u_12
β : Type u_13
M : Matrix m m α
b : m → β
k : β
⊢ M.toSquareBlock b k =
    (of : (a : { a : m // b a = k } → { a : m // b a = k } → α) → Matrix { a : m // b a = k } { a : m // b a = k } α)
      fun (i j : { a : m // b a = k }) ↦ M (↑i : m) (↑j : m)

Tactic:
rfl

Premises used: Matrix.submatrix, Matrix.toBlock, Matrix.toSquareBlockProp, rfl, Matrix.toSquareBlock
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
α : Type u_12
inst : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
a : ∀ (i : n ⊕ o) (j : l ⊕ m), (x • fromBlocks A B C D) i j = fromBlocks (x • A) (x • B) (x • C) (x • D) i j
⊢ x • fromBlocks A B C D = fromBlocks (x • A) (x • B) (x • C) (x • D)

Tactic:
ext i j
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
α : Type u_12
inst : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
i : n ⊕ o
j : l ⊕ m
a : ∀ (val : n), (x • fromBlocks A B C D) (Sum.inl val) j = fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inl val) j
a₁ : ∀ (val : o), (x • fromBlocks A B C D) (Sum.inr val) j = fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inr val) j
⊢ (x • fromBlocks A B C D) i j = fromBlocks (x • A) (x • B) (x • C) (x • D) i j

Tactic:
rcases i with ⟨⟩
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
α : Type u_12
inst : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
j : l ⊕ m
val : n
a :
  ∀ (val_1 : l),
    (x • fromBlocks A B C D) (Sum.inl val) (Sum.inl val_1) =
      fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inl val) (Sum.inl val_1)
a₁ :
  ∀ (val_1 : m),
    (x • fromBlocks A B C D) (Sum.inl val) (Sum.inr val_1) =
      fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inl val) (Sum.inr val_1)
⊢ (x • fromBlocks A B C D) (Sum.inl val) j = fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inl val) j

Tactic:
rcases j with ⟨⟩
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
α : Type u_12
inst : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
j : l ⊕ m
val : o
a :
  ∀ (val_1 : l),
    (x • fromBlocks A B C D) (Sum.inr val) (Sum.inl val_1) =
      fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inr val) (Sum.inl val_1)
a₁ :
  ∀ (val_1 : m),
    (x • fromBlocks A B C D) (Sum.inr val) (Sum.inr val_1) =
      fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inr val) (Sum.inr val_1)
⊢ (x • fromBlocks A B C D) (Sum.inr val) j = fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inr val) j

Tactic:
rcases j with ⟨⟩
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
α : Type u_12
inst : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val : n
val_1 : l
⊢ (x • fromBlocks A B C D) (Sum.inl val) (Sum.inl val_1) =
    fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inl val) (Sum.inl val_1)

Tactic:
simp [fromBlocks]

Premises used: Matrix.fromBlocks
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
α : Type u_12
inst : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val : n
val_1 : m
⊢ (x • fromBlocks A B C D) (Sum.inl val) (Sum.inr val_1) =
    fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inl val) (Sum.inr val_1)

Tactic:
simp [fromBlocks]

Premises used: Matrix.fromBlocks
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
α : Type u_12
inst : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val : o
val_1 : l
⊢ (x • fromBlocks A B C D) (Sum.inr val) (Sum.inl val_1) =
    fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inr val) (Sum.inl val_1)

Tactic:
simp [fromBlocks]

Premises used: Matrix.fromBlocks
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
α : Type u_12
inst : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
val : o
val_1 : m
⊢ (x • fromBlocks A B C D) (Sum.inr val) (Sum.inr val_1) =
    fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inr val) (Sum.inr val_1)

Tactic:
simp [fromBlocks]

Premises used: Matrix.fromBlocks
-- Module: Mathlib.Data.Matrix.Block
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
inst : Neg R
A : Matrix n l R
B : Matrix n m R
C : Matrix o l R
D : Matrix o m R
a : ∀ (i : n ⊕ o) (j : l ⊕ m), (-fromBlocks A B C D) i j = fromBlocks (-A) (-B) (-C) (-D) i j
⊢ -fromBlocks A B C D = fromBlocks (-A) (-B) (-C) (-D)

Tactic:
ext i j