awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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 : α → β
⊢ (fromBlocks A B C D).map f = fromBlocks (A.map f) (B.map f) (C.map f) (D.map f)
have 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
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ (fromBlocks A B C D).map f i j = fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) i j
have 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
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
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
⊢ (fromBlocks A B C D).map f i j = fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) i j
have 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
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
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
⊢ (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
have 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)
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
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)
⊢ (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
have 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)
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
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
⊢ (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
have 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)
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
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)
⊢ (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
have 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)
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
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 α
⊢ (fromBlocks A B C D)ᵀ = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ
have a : ∀ (i : l ⊕ m) (j : n ⊕ o), (fromBlocks A B C D)ᵀ i j = fromBlocks Aᵀ Cᵀ Bᵀ 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
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
⊢ (fromBlocks A B C D)ᵀ i j = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ i j
have a : ∀ (val : l), (fromBlocks A B C D)ᵀ (Sum.inl val) j = fromBlocks Aᵀ Cᵀ Bᵀ 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
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
⊢ (fromBlocks A B C D)ᵀ i j = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ i j
have a₁ : ∀ (val : m), (fromBlocks A B C D)ᵀ (Sum.inr val) j = fromBlocks Aᵀ Cᵀ Bᵀ 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
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
⊢ (fromBlocks A B C D)ᵀ (Sum.inl val) j = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ (Sum.inl val) j
have 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)
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
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)
⊢ (fromBlocks A B C D)ᵀ (Sum.inl val) j = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ (Sum.inl val) j
have 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)
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
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
⊢ (fromBlocks A B C D)ᵀ (Sum.inr val) j = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ (Sum.inr val) j
have 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)
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
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)
⊢ (fromBlocks A B C D)ᵀ (Sum.inr val) j = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ (Sum.inr val) j
have 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)
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
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
⊢ (fromBlocks A B C D).submatrix Sum.swap f = (fromBlocks C D A B).submatrix id f
have 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
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ (fromBlocks A B C D).submatrix Sum.swap f i j = (fromBlocks C D A B).submatrix id f i j
have 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
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ (fromBlocks A B C D).submatrix Sum.swap f i j = (fromBlocks C D A B).submatrix id f i j
have 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
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ (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
have a : fromBlocks A B C D (Sum.inr val) (f j) = fromBlocks C D A B (Sum.inl val) (f j)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ (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
have a : fromBlocks A B C D (Sum.inl val) (f j) = fromBlocks C D A B (Sum.inr val) (f j)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ fromBlocks A B C D (Sum.inr val) (f j) = fromBlocks C D A B (Sum.inl val) (f j)
have 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)
Tactic: cases f j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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)
⊢ fromBlocks A B C D (Sum.inr val) (f j) = fromBlocks C D A B (Sum.inl val) (f j)
have 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)
Tactic: cases f j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ fromBlocks A B C D (Sum.inl val) (f j) = fromBlocks C D A B (Sum.inr val) (f j)
have 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)
Tactic: cases f j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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)
⊢ fromBlocks A B C D (Sum.inl val) (f j) = fromBlocks C D A B (Sum.inr val) (f j)
have 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)
Tactic: cases f j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ (fromBlocks A B C D).submatrix f Sum.swap = (fromBlocks B A D C).submatrix f id
have 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
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ (fromBlocks A B C D).submatrix f Sum.swap i j = (fromBlocks B A D C).submatrix f id i j
have 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)
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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)
⊢ (fromBlocks A B C D).submatrix f Sum.swap i j = (fromBlocks B A D C).submatrix f id i j
have 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)
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ (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)
have a : fromBlocks A B C D (f i) (Sum.inr val) = fromBlocks B A D C (f i) (Sum.inl val)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ (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)
have a : fromBlocks A B C D (f i) (Sum.inl val) = fromBlocks B A D C (f i) (Sum.inr val)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ fromBlocks A B C D (f i) (Sum.inr val) = fromBlocks B A D C (f i) (Sum.inl val)
have 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)
Tactic: cases f i
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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)
⊢ fromBlocks A B C D (f i) (Sum.inr val) = fromBlocks B A D C (f i) (Sum.inl val)
have 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)
Tactic: cases f i
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ fromBlocks A B C D (f i) (Sum.inl val) = fromBlocks B A D C (f i) (Sum.inr val)
have 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)
Tactic: cases f i
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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)
⊢ fromBlocks A B C D (f i) (Sum.inl val) = fromBlocks B A D C (f i) (Sum.inr val)
have 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)
Tactic: cases f i
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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 α
⊢ x • fromBlocks A B C D = fromBlocks (x • A) (x • B) (x • C) (x • D)
have 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
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
⊢ (x • fromBlocks A B C D) i j = fromBlocks (x • A) (x • B) (x • C) (x • D) i j
have 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
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
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
⊢ (x • fromBlocks A B C D) i j = fromBlocks (x • A) (x • B) (x • C) (x • D) i j
have 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
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
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
⊢ (x • fromBlocks A B C D) (Sum.inl val) j = fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inl val) j
have 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)
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
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)
⊢ (x • fromBlocks A B C D) (Sum.inl val) j = fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inl val) j
have 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)
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
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
⊢ (x • fromBlocks A B C D) (Sum.inr val) j = fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inr val) j
have 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)
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
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)
⊢ (x • fromBlocks A B C D) (Sum.inr val) j = fromBlocks (x • A) (x • B) (x • C) (x • D) (Sum.inr val) j
have 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)
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
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
⊢ -fromBlocks A B C D = fromBlocks (-A) (-B) (-C) (-D)
have a : ∀ (i : n ⊕ o) (j : l ⊕ m), (-fromBlocks A B C D) i j = fromBlocks (-A) (-B) (-C) (-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
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
i : n ⊕ o
j : l ⊕ m
⊢ (-fromBlocks A B C D) i j = fromBlocks (-A) (-B) (-C) (-D) i j
have a : ∀ (val : n), (-fromBlocks A B C D) (Sum.inl val) j = fromBlocks (-A) (-B) (-C) (-D) (Sum.inl val) j
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
i : n ⊕ o
j : l ⊕ m
a : ∀ (val : n), (-fromBlocks A B C D) (Sum.inl val) j = fromBlocks (-A) (-B) (-C) (-D) (Sum.inl val) j
⊢ (-fromBlocks A B C D) i j = fromBlocks (-A) (-B) (-C) (-D) i j
have a₁ : ∀ (val : o), (-fromBlocks A B C D) (Sum.inr val) j = fromBlocks (-A) (-B) (-C) (-D) (Sum.inr val) j
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
j : l ⊕ m
val : n
⊢ (-fromBlocks A B C D) (Sum.inl val) j = fromBlocks (-A) (-B) (-C) (-D) (Sum.inl val) j
have a : ∀ (val_1 : l),
  (-fromBlocks A B C D) (Sum.inl val) (Sum.inl val_1) = fromBlocks (-A) (-B) (-C) (-D) (Sum.inl val) (Sum.inl val_1)
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
j : l ⊕ m
val : n
a :
  ∀ (val_1 : l),
    (-fromBlocks A B C D) (Sum.inl val) (Sum.inl val_1) = fromBlocks (-A) (-B) (-C) (-D) (Sum.inl val) (Sum.inl val_1)
⊢ (-fromBlocks A B C D) (Sum.inl val) j = fromBlocks (-A) (-B) (-C) (-D) (Sum.inl val) j
have a₁ : ∀ (val_1 : m),
  (-fromBlocks A B C D) (Sum.inl val) (Sum.inr val_1) = fromBlocks (-A) (-B) (-C) (-D) (Sum.inl val) (Sum.inr val_1)
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Matrix.Block (goal)
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
j : l ⊕ m
val : o
⊢ (-fromBlocks A B C D) (Sum.inr val) j = fromBlocks (-A) (-B) (-C) (-D) (Sum.inr val) j
have a : ∀ (val_1 : l),
  (-fromBlocks A B C D) (Sum.inr val) (Sum.inl val_1) = fromBlocks (-A) (-B) (-C) (-D) (Sum.inr val) (Sum.inl val_1)
Tactic: cases j
Cleared hypotheses: j