awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Matrix.ColumnRowPartitioned (goal)
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
a :
  ∀ (val : m₁) (val_1 : n₁),
    (B₁₁.fromRows B₂₁).fromCols (B₁₂.fromRows B₂₂) (Sum.inl val) (Sum.inl val_1) =
      fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inl val) (Sum.inl val_1)
a₁ :
  ∀ (val : m₁) (val_1 : n₂),
    (B₁₁.fromRows B₂₁).fromCols (B₁₂.fromRows B₂₂) (Sum.inl val) (Sum.inr val_1) =
      fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inl val) (Sum.inr val_1)
a₂ :
  ∀ (val : m₂) (val_1 : n₁),
    (B₁₁.fromRows B₂₁).fromCols (B₁₂.fromRows B₂₂) (Sum.inr val) (Sum.inl val_1) =
      fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inr val) (Sum.inl val_1)
⊢ (B₁₁.fromRows B₂₁).fromCols (B₁₂.fromRows B₂₂) = fromBlocks B₁₁ B₁₂ B₂₁ B₂₂
have a₃ : ∀ (val : m₂) (val_1 : n₂),
  (B₁₁.fromRows B₂₁).fromCols (B₁₂.fromRows B₂₂) (Sum.inr val) (Sum.inr val_1) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inr val) (Sum.inr val_1)
Tactic: ext (_ | _) (_ | _)
-- Lean 4 proof step from Mathlib.Data.Matrix.ColumnRowPartitioned (goal)
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
⊢ (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) = fromBlocks B₁₁ B₁₂ B₂₁ B₂₂
have a : ∀ (val : m₁) (val_1 : n₁),
  (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) (Sum.inl val) (Sum.inl val_1) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inl val) (Sum.inl val_1)
Tactic: ext (_ | _) (_ | _)
-- Lean 4 proof step from Mathlib.Data.Matrix.ColumnRowPartitioned (goal)
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
a :
  ∀ (val : m₁) (val_1 : n₁),
    (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) (Sum.inl val) (Sum.inl val_1) =
      fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inl val) (Sum.inl val_1)
⊢ (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) = fromBlocks B₁₁ B₁₂ B₂₁ B₂₂
have a₁ : ∀ (val : m₁) (val_1 : n₂),
  (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) (Sum.inl val) (Sum.inr val_1) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inl val) (Sum.inr val_1)
Tactic: ext (_ | _) (_ | _)
-- Lean 4 proof step from Mathlib.Data.Matrix.ColumnRowPartitioned (goal)
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
a :
  ∀ (val : m₁) (val_1 : n₁),
    (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) (Sum.inl val) (Sum.inl val_1) =
      fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inl val) (Sum.inl val_1)
a₁ :
  ∀ (val : m₁) (val_1 : n₂),
    (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) (Sum.inl val) (Sum.inr val_1) =
      fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inl val) (Sum.inr val_1)
⊢ (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) = fromBlocks B₁₁ B₁₂ B₂₁ B₂₂
have a₂ : ∀ (val : m₂) (val_1 : n₁),
  (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) (Sum.inr val) (Sum.inl val_1) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inr val) (Sum.inl val_1)
Tactic: ext (_ | _) (_ | _)
-- Lean 4 proof step from Mathlib.Data.Matrix.ColumnRowPartitioned (goal)
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
a :
  ∀ (val : m₁) (val_1 : n₁),
    (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) (Sum.inl val) (Sum.inl val_1) =
      fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inl val) (Sum.inl val_1)
a₁ :
  ∀ (val : m₁) (val_1 : n₂),
    (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) (Sum.inl val) (Sum.inr val_1) =
      fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inl val) (Sum.inr val_1)
a₂ :
  ∀ (val : m₂) (val_1 : n₁),
    (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) (Sum.inr val) (Sum.inl val_1) =
      fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inr val) (Sum.inl val_1)
⊢ (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) = fromBlocks B₁₁ B₁₂ B₂₁ B₂₂
have a₃ : ∀ (val : m₂) (val_1 : n₂),
  (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) (Sum.inr val) (Sum.inr val_1) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inr val) (Sum.inr val_1)
Tactic: ext (_ | _) (_ | _)
-- Lean 4 proof step from Mathlib.Data.Matrix.ColumnRowPartitioned (goal)
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst : Semiring R
inst_1 : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
v : n → R
⊢ A₁.fromRows A₂ *ᵥ v = Sum.elim (A₁ *ᵥ v) (A₂ *ᵥ v)
have h : ∀ (val : m₁), (A₁.fromRows A₂ *ᵥ v) (Sum.inl val) = Sum.elim (A₁ *ᵥ v) (A₂ *ᵥ v) (Sum.inl val)
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.Data.Matrix.ColumnRowPartitioned (goal)
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst : Semiring R
inst_1 : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
v : n → R
h : ∀ (val : m₁), (A₁.fromRows A₂ *ᵥ v) (Sum.inl val) = Sum.elim (A₁ *ᵥ v) (A₂ *ᵥ v) (Sum.inl val)
⊢ A₁.fromRows A₂ *ᵥ v = Sum.elim (A₁ *ᵥ v) (A₂ *ᵥ v)
have h₁ : ∀ (val : m₂), (A₁.fromRows A₂ *ᵥ v) (Sum.inr val) = Sum.elim (A₁ *ᵥ v) (A₂ *ᵥ v) (Sum.inr val)
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.Data.Matrix.ColumnRowPartitioned (goal)
Goal:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
inst_1 : Fintype m
B₁ : Matrix m n₁ R
B₂ : Matrix m n₂ R
v : m → R
⊢ v ᵥ* B₁.fromCols B₂ = Sum.elim (v ᵥ* B₁) (v ᵥ* B₂)
have h : ∀ (val : n₁), (v ᵥ* B₁.fromCols B₂) (Sum.inl val) = Sum.elim (v ᵥ* B₁) (v ᵥ* B₂) (Sum.inl val)
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.Data.Matrix.ColumnRowPartitioned (goal)
Goal:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
inst_1 : Fintype m
B₁ : Matrix m n₁ R
B₂ : Matrix m n₂ R
v : m → R
h : ∀ (val : n₁), (v ᵥ* B₁.fromCols B₂) (Sum.inl val) = Sum.elim (v ᵥ* B₁) (v ᵥ* B₂) (Sum.inl val)
⊢ v ᵥ* B₁.fromCols B₂ = Sum.elim (v ᵥ* B₁) (v ᵥ* B₂)
have h₁ : ∀ (val : n₂), (v ᵥ* B₁.fromCols B₂) (Sum.inr val) = Sum.elim (v ᵥ* B₁) (v ᵥ* B₂) (Sum.inr val)
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.Data.Matrix.ColumnRowPartitioned (goal)
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst : Semiring R
inst_1 : Fintype m₁
inst_2 : Fintype m₂
B₁ : Matrix m₁ n R
B₂ : Matrix m₂ n R
v₁ : m₁ → R
v₂ : m₂ → R
⊢ Sum.elim v₁ v₂ ᵥ* B₁.fromRows B₂ = v₁ ᵥ* B₁ + v₂ ᵥ* B₂
have h : ∀ (x : n), (Sum.elim v₁ v₂ ᵥ* B₁.fromRows B₂) x = (v₁ ᵥ* B₁ + v₂ ᵥ* B₂) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.ColumnRowPartitioned (goal)
Goal:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
inst_1 : Fintype n₁
inst_2 : Fintype n₂
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
v₁ : n₁ → R
v₂ : n₂ → R
⊢ A₁.fromCols A₂ *ᵥ Sum.elim v₁ v₂ = A₁ *ᵥ v₁ + A₂ *ᵥ v₂
have h : ∀ (x : m), (A₁.fromCols A₂ *ᵥ Sum.elim v₁ v₂) x = (A₁ *ᵥ v₁ + A₂ *ᵥ v₂) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.ColumnRowPartitioned (goal)
Goal:
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst : Semiring R
inst_1 : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B : Matrix n m R
⊢ A₁.fromRows A₂ * B = (A₁ * B).fromRows (A₂ * B)
have a : ∀ (val : m₁) (j : m), (A₁.fromRows A₂ * B) (Sum.inl val) j = (A₁ * B).fromRows (A₂ * B) (Sum.inl val) j
Tactic: ext (_ | _) _
-- Lean 4 proof step from Mathlib.Data.Matrix.ColumnRowPartitioned (goal)
Goal:
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst : Semiring R
inst_1 : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B : Matrix n m R
a : ∀ (val : m₁) (j : m), (A₁.fromRows A₂ * B) (Sum.inl val) j = (A₁ * B).fromRows (A₂ * B) (Sum.inl val) j
⊢ A₁.fromRows A₂ * B = (A₁ * B).fromRows (A₂ * B)
have a₁ : ∀ (val : m₂) (j : m), (A₁.fromRows A₂ * B) (Sum.inr val) j = (A₁ * B).fromRows (A₂ * B) (Sum.inr val) j
Tactic: ext (_ | _) _
-- Lean 4 proof step from Mathlib.Data.Matrix.ColumnRowPartitioned (goal)
Goal:
R : Type u_1
m : Type u_2
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
inst_1 : Fintype n
A : Matrix m n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
⊢ A * B₁.fromCols B₂ = (A * B₁).fromCols (A * B₂)
have a : ∀ (i : m) (val : n₁), (A * B₁.fromCols B₂) i (Sum.inl val) = (A * B₁).fromCols (A * B₂) i (Sum.inl val)
Tactic: ext _ (_ | _)
-- Lean 4 proof step from Mathlib.Data.Matrix.ColumnRowPartitioned (goal)
Goal:
R : Type u_1
m : Type u_2
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
inst_1 : Fintype n
A : Matrix m n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
a : ∀ (i : m) (val : n₁), (A * B₁.fromCols B₂) i (Sum.inl val) = (A * B₁).fromCols (A * B₂) i (Sum.inl val)
⊢ A * B₁.fromCols B₂ = (A * B₁).fromCols (A * B₂)
have a₁ : ∀ (i : m) (val : n₂), (A * B₁.fromCols B₂) i (Sum.inr val) = (A * B₁).fromCols (A * B₂) i (Sum.inr val)
Tactic: ext _ (_ | _)
-- Lean 4 proof step from Mathlib.Data.Matrix.ColumnRowPartitioned (goal)
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst : Semiring R
⊢ Eq (α := Matrix (m₁ ⊕ m₂) n R) (fromRows 0 0) 0
have a : ∀ (val : m₁) (j : n),
  Eq.{u_1 + 1} (α := R) (fromRows.{u_1, u_3, u_4, u_5} (m₂ := m₂) 0 0 (Sum.inl val) j) (0 (Sum.inl val) j)
Tactic: ext (_ | _) _
-- Lean 4 proof step from Mathlib.Data.Matrix.ColumnRowPartitioned (goal)
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst : Semiring R
a :
  ∀ (val : m₁) (j : n),
    Eq.{u_1 + 1} (α := R) (fromRows.{u_1, u_3, u_4, u_5} (m₂ := m₂) 0 0 (Sum.inl val) j) (0 (Sum.inl val) j)
⊢ Eq (α := Matrix (m₁ ⊕ m₂) n R) (fromRows 0 0) 0
have a₁ : ∀ (val : m₂) (j : n),
  Eq.{u_1 + 1} (α := R) (fromRows.{u_1, u_3, u_4, u_5} (m₁ := m₁) 0 0 (Sum.inr val) j) (0 (Sum.inr val) j)
Tactic: ext (_ | _) _
-- Lean 4 proof step from Mathlib.Data.Matrix.ColumnRowPartitioned (goal)
Goal:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
⊢ Eq (α := Matrix m (n₁ ⊕ n₂) R) (fromCols 0 0) 0
have a : ∀ (i : m) (val : n₁),
  Eq.{u_1 + 1} (α := R) (fromCols.{u_1, u_2, u_6, u_7} (n₂ := n₂) 0 0 i (Sum.inl val)) (0 i (Sum.inl val))
Tactic: ext _ (_ | _)
-- Lean 4 proof step from Mathlib.Data.Matrix.ColumnRowPartitioned (goal)
Goal:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
a :
  ∀ (i : m) (val : n₁),
    Eq.{u_1 + 1} (α := R) (fromCols.{u_1, u_2, u_6, u_7} (n₂ := n₂) 0 0 i (Sum.inl val)) (0 i (Sum.inl val))
⊢ Eq (α := Matrix m (n₁ ⊕ n₂) R) (fromCols 0 0) 0
have a₁ : ∀ (i : m) (val : n₂),
  Eq.{u_1 + 1} (α := R) (fromCols.{u_1, u_2, u_6, u_7} (n₁ := n₁) 0 0 i (Sum.inr val)) (0 i (Sum.inr val))
Tactic: ext _ (_ | _)
-- Lean 4 proof step from Mathlib.Data.Matrix.ColumnRowPartitioned (goal)
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
inst_1 : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
⊢ A₁.fromRows A₂ * B₁.fromCols B₂ = fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂)
have a : ∀ (val : m₁) (val_1 : n₁),
  (A₁.fromRows A₂ * B₁.fromCols B₂) (Sum.inl val) (Sum.inl val_1) =
    fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂) (Sum.inl val) (Sum.inl val_1)
Tactic: ext (_ | _) (_ | _)
-- Lean 4 proof step from Mathlib.Data.Matrix.ColumnRowPartitioned (goal)
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
inst_1 : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
a :
  ∀ (val : m₁) (val_1 : n₁),
    (A₁.fromRows A₂ * B₁.fromCols B₂) (Sum.inl val) (Sum.inl val_1) =
      fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂) (Sum.inl val) (Sum.inl val_1)
⊢ A₁.fromRows A₂ * B₁.fromCols B₂ = fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂)
have a₁ : ∀ (val : m₁) (val_1 : n₂),
  (A₁.fromRows A₂ * B₁.fromCols B₂) (Sum.inl val) (Sum.inr val_1) =
    fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂) (Sum.inl val) (Sum.inr val_1)
Tactic: ext (_ | _) (_ | _)
-- Lean 4 proof step from Mathlib.Data.Matrix.ColumnRowPartitioned (goal)
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
inst_1 : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
a :
  ∀ (val : m₁) (val_1 : n₁),
    (A₁.fromRows A₂ * B₁.fromCols B₂) (Sum.inl val) (Sum.inl val_1) =
      fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂) (Sum.inl val) (Sum.inl val_1)
a₁ :
  ∀ (val : m₁) (val_1 : n₂),
    (A₁.fromRows A₂ * B₁.fromCols B₂) (Sum.inl val) (Sum.inr val_1) =
      fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂) (Sum.inl val) (Sum.inr val_1)
⊢ A₁.fromRows A₂ * B₁.fromCols B₂ = fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂)
have a₂ : ∀ (val : m₂) (val_1 : n₁),
  (A₁.fromRows A₂ * B₁.fromCols B₂) (Sum.inr val) (Sum.inl val_1) =
    fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂) (Sum.inr val) (Sum.inl val_1)
Tactic: ext (_ | _) (_ | _)
-- Lean 4 proof step from Mathlib.Data.Matrix.ColumnRowPartitioned (goal)
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
inst_1 : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
a :
  ∀ (val : m₁) (val_1 : n₁),
    (A₁.fromRows A₂ * B₁.fromCols B₂) (Sum.inl val) (Sum.inl val_1) =
      fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂) (Sum.inl val) (Sum.inl val_1)
a₁ :
  ∀ (val : m₁) (val_1 : n₂),
    (A₁.fromRows A₂ * B₁.fromCols B₂) (Sum.inl val) (Sum.inr val_1) =
      fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂) (Sum.inl val) (Sum.inr val_1)
a₂ :
  ∀ (val : m₂) (val_1 : n₁),
    (A₁.fromRows A₂ * B₁.fromCols B₂) (Sum.inr val) (Sum.inl val_1) =
      fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂) (Sum.inr val) (Sum.inl val_1)
⊢ A₁.fromRows A₂ * B₁.fromCols B₂ = fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂)
have a₃ : ∀ (val : m₂) (val_1 : n₂),
  (A₁.fromRows A₂ * B₁.fromCols B₂) (Sum.inr val) (Sum.inr val_1) =
    fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂) (Sum.inr val) (Sum.inr val_1)
Tactic: ext (_ | _) (_ | _)
-- Lean 4 proof step from Mathlib.Data.Matrix.ColumnRowPartitioned (goal)
Goal:
R : Type u_1
m : Type u_2
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
inst_1 : Fintype n₁
inst_2 : Fintype n₂
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
B₁ : Matrix n₁ n R
B₂ : Matrix n₂ n R
⊢ A₁.fromCols A₂ * B₁.fromRows B₂ = A₁ * B₁ + A₂ * B₂
have a : ∀ (i : m) (j : n), (A₁.fromCols A₂ * B₁.fromRows B₂) i j = (A₁ * B₁ + A₂ * B₂) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.ColumnRowPartitioned (goal)
Goal:
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
inst_1 : Fintype m₁
inst_2 : Fintype m₂
A₁ : Matrix m m₁ R
A₂ : Matrix m m₂ R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
⊢ A₁.fromCols A₂ * fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ = (A₁ * B₁₁ + A₂ * B₂₁).fromCols (A₁ * B₁₂ + A₂ * B₂₂)
have a : ∀ (i : m) (val : n₁),
  (A₁.fromCols A₂ * fromBlocks B₁₁ B₁₂ B₂₁ B₂₂) i (Sum.inl val) =
    (A₁ * B₁₁ + A₂ * B₂₁).fromCols (A₁ * B₁₂ + A₂ * B₂₂) i (Sum.inl val)
Tactic: ext _ (_ | _)
-- Lean 4 proof step from Mathlib.Data.Matrix.ColumnRowPartitioned (goal)
Goal:
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
inst_1 : Fintype m₁
inst_2 : Fintype m₂
A₁ : Matrix m m₁ R
A₂ : Matrix m m₂ R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
a :
  ∀ (i : m) (val : n₁),
    (A₁.fromCols A₂ * fromBlocks B₁₁ B₁₂ B₂₁ B₂₂) i (Sum.inl val) =
      (A₁ * B₁₁ + A₂ * B₂₁).fromCols (A₁ * B₁₂ + A₂ * B₂₂) i (Sum.inl val)
⊢ A₁.fromCols A₂ * fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ = (A₁ * B₁₁ + A₂ * B₂₁).fromCols (A₁ * B₁₂ + A₂ * B₂₂)
have a₁ : ∀ (i : m) (val : n₂),
  (A₁.fromCols A₂ * fromBlocks B₁₁ B₁₂ B₂₁ B₂₂) i (Sum.inr val) =
    (A₁ * B₁₁ + A₂ * B₂₁).fromCols (A₁ * B₁₂ + A₂ * B₂₂) i (Sum.inr val)
Tactic: ext _ (_ | _)
-- Lean 4 proof step from Mathlib.Data.Matrix.ColumnRowPartitioned (goal)
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
inst_1 : Fintype n₁
inst_2 : Fintype n₂
A₁ : Matrix n₁ n R
A₂ : Matrix n₂ n R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
⊢ fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ * A₁.fromRows A₂ = (B₁₁ * A₁ + B₁₂ * A₂).fromRows (B₂₁ * A₁ + B₂₂ * A₂)
have a : ∀ (val : m₁) (j : n),
  (fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ * A₁.fromRows A₂) (Sum.inl val) j =
    (B₁₁ * A₁ + B₁₂ * A₂).fromRows (B₂₁ * A₁ + B₂₂ * A₂) (Sum.inl val) j
Tactic: ext (_ | _) _
-- Lean 4 proof step from Mathlib.Data.Matrix.ColumnRowPartitioned (goal)
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst : Semiring R
inst_1 : Fintype n₁
inst_2 : Fintype n₂
A₁ : Matrix n₁ n R
A₂ : Matrix n₂ n R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
a :
  ∀ (val : m₁) (j : n),
    (fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ * A₁.fromRows A₂) (Sum.inl val) j =
      (B₁₁ * A₁ + B₁₂ * A₂).fromRows (B₂₁ * A₁ + B₂₂ * A₂) (Sum.inl val) j
⊢ fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ * A₁.fromRows A₂ = (B₁₁ * A₁ + B₁₂ * A₂).fromRows (B₂₁ * A₁ + B₂₂ * A₂)
have a₁ : ∀ (val : m₂) (j : n),
  (fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ * A₁.fromRows A₂) (Sum.inr val) j =
    (B₁₁ * A₁ + B₁₂ * A₂).fromRows (B₂₁ * A₁ + B₂₂ * A₂) (Sum.inr val) j
Tactic: ext (_ | _) _
-- Lean 4 proof step from Mathlib.Data.Matrix.ColumnRowPartitioned (goal)
Goal:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst : Star R
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
⊢ (A₁.fromCols A₂)ᴴ = A₁ᴴ.fromRows A₂ᴴ
have a : ∀ (val : n₁) (j : m), (A₁.fromCols A₂)ᴴ (Sum.inl val) j = A₁ᴴ.fromRows A₂ᴴ (Sum.inl val) j
Tactic: ext (_ | _) _
-- Lean 4 proof step from Mathlib.Data.Matrix.ColumnRowPartitioned (goal)
Goal:
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst : Star R
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
a : ∀ (val : n₁) (j : m), (A₁.fromCols A₂)ᴴ (Sum.inl val) j = A₁ᴴ.fromRows A₂ᴴ (Sum.inl val) j
⊢ (A₁.fromCols A₂)ᴴ = A₁ᴴ.fromRows A₂ᴴ
have a₁ : ∀ (val : n₂) (j : m), (A₁.fromCols A₂)ᴴ (Sum.inr val) j = A₁ᴴ.fromRows A₂ᴴ (Sum.inr val) j
Tactic: ext (_ | _) _
-- Lean 4 proof step from Mathlib.Data.Matrix.ColumnRowPartitioned (goal)
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst : Star R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
⊢ (A₁.fromRows A₂)ᴴ = A₁ᴴ.fromCols A₂ᴴ
have a : ∀ (i : n) (val : m₁), (A₁.fromRows A₂)ᴴ i (Sum.inl val) = A₁ᴴ.fromCols A₂ᴴ i (Sum.inl val)
Tactic: ext _ (_ | _)
-- Lean 4 proof step from Mathlib.Data.Matrix.ColumnRowPartitioned (goal)
Goal:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst : Star R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
a : ∀ (i : n) (val : m₁), (A₁.fromRows A₂)ᴴ i (Sum.inl val) = A₁ᴴ.fromCols A₂ᴴ i (Sum.inl val)
⊢ (A₁.fromRows A₂)ᴴ = A₁ᴴ.fromCols A₂ᴴ
have a₁ : ∀ (i : n) (val : m₂), (A₁.fromRows A₂)ᴴ i (Sum.inr val) = A₁ᴴ.fromCols A₂ᴴ i (Sum.inr val)
Tactic: ext _ (_ | _)
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
Goal:
I : Type u_1
J : Type u_2
R : Type u_5
inst : DecidableEq I
inst_1 : DecidableEq J
inst_2 : Zero R
inst_3 : One R
⊢ Eq (α := Matrix (I × J) (I × J) R) ((comp I I J J R : (a : Matrix I I (Matrix J J R)) → Matrix (I × J) (I × J) R) 1) 1
have a : ∀ (i j : I × J),
  Eq.{u_5 + 1} (α := R) ((comp I I J J R : (a : Matrix I I (Matrix J J R)) → Matrix (I × J) (I × J) R) 1 i j : R)
    (1 i j : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
Goal:
I : Type u_1
J : Type u_2
R : Type u_5
inst : DecidableEq I
inst_1 : DecidableEq J
inst_2 : Zero R
inst_3 : One R
i j : I × J
⊢ Eq.{u_5 + 1} (α := R) ((comp I I J J R : (a : Matrix I I (Matrix J J R)) → Matrix (I × J) (I × J) R) 1 i j : R)
    (1 i j : R)
have a : if i = j then Eq.{u_5 + 1} (α := R) ((if i.1 = j.1 then 1 else 0) i.2 j.2) 1
else Eq.{u_5 + 1} (α := R) ((if i.1 = j.1 then 1 else 0) i.2 j.2) 0
Tactic: simp only [comp, Equiv.coe_fn_mk, one_apply, apply_ite]
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst : DecidableEq I
inst_1 : DecidableEq J
inst_2 : DecidableEq K
inst_3 : DecidableEq L
inst_4 : Zero R
i : I
j : J
k : K
l : L
r : R
⊢ (comp I J K L R : (a : Matrix I J (Matrix K L R)) → Matrix (I × K) (J × L) R) (single i j (single k l r)) =
    single (i, k) (j, l) r
have a : ∀ (i' : I) (k' : K) (j' : J) (l' : L),
  (comp I J K L R : (a : Matrix I J (Matrix K L R)) → Matrix (I × K) (J × L) R) (single i j (single k l r)) (i', k')
      (j', l') =
    single (i, k) (j, l) r (i', k') (j', l')
Tactic: ext ⟨i', k'⟩ ⟨j', l'⟩
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst : DecidableEq I
inst_1 : DecidableEq J
inst_2 : DecidableEq K
inst_3 : DecidableEq L
inst_4 : Zero R
i : I
j : J
k : K
l : L
r : R
i' : I
k' : K
j' : J
l' : L
⊢ (comp I J K L R : (a : Matrix I J (Matrix K L R)) → Matrix (I × K) (J × L) R) (single i j (single k l r)) (i', k')
      (j', l') =
    single (i, k) (j, l) r (i', k') (j', l')
have a : single i j (single k l r) i' j' k' l' = single (i, k) (j, l) r (i', k') (j', l')
Tactic: dsimp [comp_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst : DecidableEq I
inst_1 : DecidableEq J
inst_2 : DecidableEq K
inst_3 : DecidableEq L
inst_4 : Zero R
i : I
j : J
k : K
l : L
r : R
i' : I
k' : K
j' : J
l' : L
⊢ single i j (single k l r) i' j' k' l' = single (i, k) (j, l) r (i', k') (j', l')
have a : ∀ (hi : i ≠ i'), single i j (single k l r) i' j' k' l' = single (i, k) (j, l) r (i', k') (j', l')
Tactic: obtain hi | rfl := ne_or_eq i i'
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst : DecidableEq I
inst_1 : DecidableEq J
inst_2 : DecidableEq K
inst_3 : DecidableEq L
inst_4 : Zero R
i : I
j : J
k : K
l : L
r : R
i' : I
k' : K
j' : J
l' : L
a : ∀ (hi : i ≠ i'), single i j (single k l r) i' j' k' l' = single (i, k) (j, l) r (i', k') (j', l')
⊢ single i j (single k l r) i' j' k' l' = single (i, k) (j, l) r (i', k') (j', l')
have a₁ : single i j (single k l r) i j' k' l' = single (i, k) (j, l) r (i, k') (j', l')
Tactic: obtain hi | rfl := ne_or_eq i i'
Cleared hypotheses: i'
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst : DecidableEq I
inst_1 : DecidableEq J
inst_2 : DecidableEq K
inst_3 : DecidableEq L
inst_4 : Zero R
i : I
j : J
k : K
l : L
r : R
i' : I
k' : K
j' : J
l' : L
hi : i ≠ i'
⊢ single i j (single k l r) i' j' k' l' = single (i, k) (j, l) r (i', k') (j', l')
have a : 0 k' l' = single (i, k) (j, l) r (i', k') (j', l')
Tactic: rw [single_apply_of_row_ne hi,
      single_apply_of_row_ne (ne_of_apply_ne Prod.fst hi), Matrix.zero_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst : DecidableEq I
inst_1 : DecidableEq J
inst_2 : DecidableEq K
inst_3 : DecidableEq L
inst_4 : Zero R
i : I
j : J
k : K
l : L
r : R
i' : I
k' : K
j' : J
l' : L
hi : i ≠ i'
a : 0 k' l' = single (i, k) (j, l) r (i', k') (j', l')
⊢ single i j (single k l r) i' j' k' l' = single (i, k) (j, l) r (i', k') (j', l')
have a₁ : Eq.{u_5 + 1} (α := R) (0 k' l') 0
Tactic: rw [single_apply_of_row_ne hi,
      single_apply_of_row_ne (ne_of_apply_ne Prod.fst hi), Matrix.zero_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Composition (goal)
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst : DecidableEq I
inst_1 : DecidableEq J
inst_2 : DecidableEq K
inst_3 : DecidableEq L
inst_4 : Zero R
i : I
j : J
k : K
l : L
r : R
i' : I
k' : K
j' : J
l' : L
hi : i ≠ i'
a : 0 k' l' = single (i, k) (j, l) r (i', k') (j', l')
a₁ : Eq.{u_5 + 1} (α := R) (0 k' l') 0
⊢ single i j (single k l r) i' j' k' l' = single (i, k) (j, l) r (i', k') (j', l')
have a₂ : Eq.{u_5 + 1} (α := R) 0 0
Tactic: rw [single_apply_of_row_ne hi,
      single_apply_of_row_ne (ne_of_apply_ne Prod.fst hi), Matrix.zero_apply]