awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
α : Type v
inst : CommRing α
inst_1 : Fintype m
inst_2 : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
rw : ((↑h.unit : Matrix m m α)⁻¹ * N * (↑h.unit : Matrix m m α)).trace = N.trace
⊢ (M⁻¹ * N * M).trace = N.trace
have rw₁ : ((↑h.unit⁻¹ : Matrix m m α) * N * (↑h.unit : Matrix m m α)).trace = N.trace
Tactic: rw [← h.unit_spec, ← coe_units_inv, trace_units_conj']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
m : Type u
α : Type v
inst : CommRing α
inst_1 : Fintype m
inst_2 : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
rw : ((↑h.unit : Matrix m m α)⁻¹ * N * (↑h.unit : Matrix m m α)).trace = N.trace
rw₁ : ((↑h.unit⁻¹ : Matrix m m α) * N * (↑h.unit : Matrix m m α)).trace = N.trace
⊢ (M⁻¹ * N * M).trace = N.trace
have rw₂ : N.trace = N.trace
Tactic: rw [← h.unit_spec, ← coe_units_inv, trace_units_conj']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
m : ℕ
n' : Type uₙ
v : n' → α
B : Fin m → n' → α
i : Fin m.succ
j : n'
⊢ vecCons v B i j = vecCons (v j) (fun (i : Fin m) ↦ B i j) i
have refine_1 : vecCons v B 0 j = vecCons (n := m) (v j) (fun (i : Fin m) ↦ B i j) 0
Tactic: refine Fin.cases ?_ ?_ i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
m : ℕ
n' : Type uₙ
v : n' → α
B : Fin m → n' → α
i : Fin m.succ
j : n'
refine_1 : vecCons v B 0 j = vecCons (n := m) (v j) (fun (i : Fin m) ↦ B i j) 0
⊢ vecCons v B i j = vecCons (v j) (fun (i : Fin m) ↦ B i j) i
have refine_2 : ∀ (i : Fin m), vecCons v B i.succ j = vecCons (v j) (fun (i : Fin m) ↦ B i j) i.succ
Tactic: refine Fin.cases ?_ ?_ i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
m : ℕ
ι : Type u_1
x : α
u : Fin m → α
⊢ replicateCol ι (vecCons x u) =
    (of : (a : Fin m.succ → ι → α) → Matrix (Fin m.succ) ι α) (vecCons (fun (x_1 : ι) ↦ x) (replicateCol ι u))
have a : ∀ (i : Fin m.succ) (j : ι),
  replicateCol ι (vecCons x u) i j =
    (of : (a : Fin m.succ → ι → α) → Matrix (Fin m.succ) ι α) (vecCons (fun (x_1 : ι) ↦ x) (replicateCol ι u)) i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
m : ℕ
ι : Type u_1
x : α
u : Fin m → α
i : Fin m.succ
j : ι
⊢ replicateCol ι (vecCons x u) i j =
    (of : (a : Fin m.succ → ι → α) → Matrix (Fin m.succ) ι α) (vecCons (fun (x_1 : ι) ↦ x) (replicateCol ι u)) i j
have a : replicateCol ι (vecCons x u) 0 j =
  (of : (a : Fin m.succ → ι → α) → Matrix (Fin m.succ) ι α) (vecCons (fun (x_1 : ι) ↦ x) (replicateCol ι u)) 0 j
Tactic: refine Fin.cases ?_ ?_ i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
m : ℕ
ι : Type u_1
x : α
u : Fin m → α
i : Fin m.succ
j : ι
a :
  replicateCol ι (vecCons x u) 0 j =
    (of : (a : Fin m.succ → ι → α) → Matrix (Fin m.succ) ι α) (vecCons (fun (x_1 : ι) ↦ x) (replicateCol ι u)) 0 j
⊢ replicateCol ι (vecCons x u) i j =
    (of : (a : Fin m.succ → ι → α) → Matrix (Fin m.succ) ι α) (vecCons (fun (x_1 : ι) ↦ x) (replicateCol ι u)) i j
have a₁ : ∀ (i : Fin m),
  replicateCol ι (vecCons x u) i.succ j =
    (of : (a : Fin m.succ → ι → α) → Matrix (Fin m.succ) ι α) (vecCons (fun (x_1 : ι) ↦ x) (replicateCol ι u)) i.succ j
Tactic: refine Fin.cases ?_ ?_ i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
m : ℕ
n' : Type uₙ
v : n' → α
A : Matrix (Fin m) n' α
⊢ Eq (α := Matrix n' (Fin m.succ) α) ((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A))ᵀ
    ((of : (a : n' → Fin m.succ → α) → Matrix n' (Fin m.succ) α) fun (i : n') ↦ vecCons (v i) (Aᵀ i))
have a : ∀ (i : n') (j : Fin m.succ),
  Eq.{u + 1} (α := α) (((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A))ᵀ i j : α)
    ((of : (a : n' → Fin m.succ → α) → Matrix n' (Fin m.succ) α) (fun (i : n') ↦ vecCons (v i) (Aᵀ i)) i j : α)
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
m : ℕ
n' : Type uₙ
v : n' → α
A : Matrix (Fin m) n' α
i : n'
j : Fin m.succ
⊢ Eq.{u + 1} (α := α) (((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A))ᵀ i j : α)
    ((of : (a : n' → Fin m.succ → α) → Matrix n' (Fin m.succ) α) (fun (i : n') ↦ vecCons (v i) (Aᵀ i)) i j : α)
have a : Eq.{u + 1} (α := α)
  (transpose (m := Fin m.succ) ((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A)) i 0 : α)
  ((of : (a : n' → Fin m.succ → α) → Matrix n' (Fin m.succ) α) (fun (i : n') ↦ vecCons (v i) (Aᵀ i)) i 0 : α)
Tactic: refine Fin.cases ?_ ?_ j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
m : ℕ
n' : Type uₙ
v : n' → α
A : Matrix (Fin m) n' α
i : n'
j : Fin m.succ
a :
  Eq.{u + 1} (α := α)
    (transpose (m := Fin m.succ) ((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A)) i 0 : α)
    ((of : (a : n' → Fin m.succ → α) → Matrix n' (Fin m.succ) α) (fun (i : n') ↦ vecCons (v i) (Aᵀ i)) i 0 : α)
⊢ Eq.{u + 1} (α := α) (((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A))ᵀ i j : α)
    ((of : (a : n' → Fin m.succ → α) → Matrix n' (Fin m.succ) α) (fun (i : n') ↦ vecCons (v i) (Aᵀ i)) i j : α)
have a₁ : ∀ (i_1 : Fin m),
  Eq.{u + 1} (α := α) (((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A))ᵀ i i_1.succ : α)
    ((of : (a : n' → Fin m.succ → α) → Matrix n' (Fin m.succ) α) (fun (i : n') ↦ vecCons (v i) (Aᵀ i)) i i_1.succ : α)
Tactic: refine Fin.cases ?_ ?_ j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
n : ℕ
m' : Type uₘ
A : Matrix m' (Fin n.succ) α
⊢ vecTail ((Equiv.symm of : (a : Matrix (Fin n.succ) m' α) → Fin n.succ → m' → α) Aᵀ) = (vecTail ∘ A)ᵀ
have h : ∀ (i : Fin n) (j : m'),
  vecTail ((Equiv.symm of : (a : Matrix (Fin n.succ) m' α) → Fin n.succ → m' → α) Aᵀ) i j = (vecTail ∘ A)ᵀ i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
m : ℕ
n' : Type uₙ
o' : Type uₒ
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n'
v : n' → α
A : Fin m → n' → α
B : Matrix n' o' α
⊢ HMul.hMul (α := Matrix (Fin m.succ) n' α)
      ((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A) : Matrix (Fin m.succ) n' α) B =
    (of : (a : Fin m.succ → o' → α) → Matrix (Fin m.succ) o' α)
      (vecCons (v ᵥ* B)
        ((Equiv.symm of : (a : Matrix (Fin m) o' α) → Fin m → o' → α)
          (HMul.hMul (α := Matrix (Fin m) n' α)
            ((of : (a : Fin m → n' → α) → Matrix (Fin m) n' α) A : Matrix (Fin m) n' α) B)))
have a : ∀ (i : Fin m.succ) (j : o'),
  HMul.hMul (α := Matrix (Fin m.succ) n' α)
      ((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A) : Matrix (Fin m.succ) n' α) B i j =
    (of : (a : Fin m.succ → o' → α) → Matrix (Fin m.succ) o' α)
      (vecCons (v ᵥ* B)
        ((Equiv.symm of : (a : Matrix (Fin m) o' α) → Fin m → o' → α)
          (HMul.hMul (α := Matrix (Fin m) n' α)
            ((of : (a : Fin m → n' → α) → Matrix (Fin m) n' α) A : Matrix (Fin m) n' α) B)))
      i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
m : ℕ
n' : Type uₙ
o' : Type uₒ
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n'
v : n' → α
A : Fin m → n' → α
B : Matrix n' o' α
i : Fin m.succ
j : o'
⊢ HMul.hMul (α := Matrix (Fin m.succ) n' α)
      ((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A) : Matrix (Fin m.succ) n' α) B i j =
    (of : (a : Fin m.succ → o' → α) → Matrix (Fin m.succ) o' α)
      (vecCons (v ᵥ* B)
        ((Equiv.symm of : (a : Matrix (Fin m) o' α) → Fin m → o' → α)
          (HMul.hMul (α := Matrix (Fin m) n' α)
            ((of : (a : Fin m → n' → α) → Matrix (Fin m) n' α) A : Matrix (Fin m) n' α) B)))
      i j
have a : HMul.hMul (α := Matrix (Fin m.succ) n' α)
    ((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A) : Matrix (Fin m.succ) n' α) B 0 j =
  (of : (a : Fin m.succ → o' → α) → Matrix (Fin m.succ) o' α)
    (vecCons (v ᵥ* B)
      ((Equiv.symm of : (a : Matrix (Fin m) o' α) → Fin m → o' → α)
        (HMul.hMul (α := Matrix (Fin m) n' α)
          ((of : (a : Fin m → n' → α) → Matrix (Fin m) n' α) A : Matrix (Fin m) n' α) B)))
    0 j
Tactic: refine Fin.cases ?_ ?_ i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
m : ℕ
n' : Type uₙ
o' : Type uₒ
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n'
v : n' → α
A : Fin m → n' → α
B : Matrix n' o' α
i : Fin m.succ
j : o'
a :
  HMul.hMul (α := Matrix (Fin m.succ) n' α)
      ((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A) : Matrix (Fin m.succ) n' α) B 0 j =
    (of : (a : Fin m.succ → o' → α) → Matrix (Fin m.succ) o' α)
      (vecCons (v ᵥ* B)
        ((Equiv.symm of : (a : Matrix (Fin m) o' α) → Fin m → o' → α)
          (HMul.hMul (α := Matrix (Fin m) n' α)
            ((of : (a : Fin m → n' → α) → Matrix (Fin m) n' α) A : Matrix (Fin m) n' α) B)))
      0 j
⊢ HMul.hMul (α := Matrix (Fin m.succ) n' α)
      ((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A) : Matrix (Fin m.succ) n' α) B i j =
    (of : (a : Fin m.succ → o' → α) → Matrix (Fin m.succ) o' α)
      (vecCons (v ᵥ* B)
        ((Equiv.symm of : (a : Matrix (Fin m) o' α) → Fin m → o' → α)
          (HMul.hMul (α := Matrix (Fin m) n' α)
            ((of : (a : Fin m → n' → α) → Matrix (Fin m) n' α) A : Matrix (Fin m) n' α) B)))
      i j
have a₁ : ∀ (i : Fin m),
  HMul.hMul (α := Matrix (Fin m.succ) n' α)
      ((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A) : Matrix (Fin m.succ) n' α) B i.succ
      j =
    (of : (a : Fin m.succ → o' → α) → Matrix (Fin m.succ) o' α)
      (vecCons (v ᵥ* B)
        ((Equiv.symm of : (a : Matrix (Fin m) o' α) → Fin m → o' → α)
          (HMul.hMul (α := Matrix (Fin m) n' α)
            ((of : (a : Fin m → n' → α) → Matrix (Fin m) n' α) A : Matrix (Fin m) n' α) B)))
      i.succ j
Tactic: refine Fin.cases ?_ ?_ i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
n : ℕ
o' : Type uₒ
inst : NonUnitalNonAssocSemiring α
x : α
v : Fin n → α
B : Fin n.succ → o' → α
⊢ vecCons x v ᵥ* (of : (a : Fin n.succ → o' → α) → Matrix (Fin n.succ) o' α) B =
    x • vecHead B + v ᵥ* (of : (a : Fin n → o' → α) → Matrix (Fin n) o' α) (vecTail B)
have h : ∀ (i : o'),
  (vecCons x v ᵥ* (of : (a : Fin n.succ → o' → α) → Matrix (Fin n.succ) o' α) B) i =
    HAdd.hAdd (β := o' → α) (x • vecHead B) (v ᵥ* (of : (a : Fin n → o' → α) → Matrix (Fin n) o' α) (vecTail B)) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
n : ℕ
o' : Type uₒ
inst : NonUnitalNonAssocSemiring α
v : Fin n.succ → α
w : o' → α
B : Fin n → o' → α
⊢ v ᵥ* (of : (a : Fin n.succ → o' → α) → Matrix (Fin n.succ) o' α) (vecCons w B) =
    vecHead v • w + vecTail v ᵥ* (of : (a : Fin n → o' → α) → Matrix (Fin n) o' α) B
have h : ∀ (i : o'),
  (v ᵥ* (of : (a : Fin n.succ → o' → α) → Matrix (Fin n.succ) o' α) (vecCons w B)) i =
    HAdd.hAdd (β := o' → α) (vecHead v • w) (vecTail v ᵥ* (of : (a : Fin n → o' → α) → Matrix (Fin n) o' α) B) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
m : ℕ
n' : Type uₙ
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n'
v : n' → α
A : Fin m → n' → α
w : n' → α
⊢ Eq (α := Fin m.succ → α) ((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A) *ᵥ w)
    (vecCons (v ⬝ᵥ w) ((of : (a : Fin m → n' → α) → Matrix (Fin m) n' α) A *ᵥ w))
have h : ∀ (i : Fin m.succ),
  ((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A) *ᵥ w) i =
    vecCons (v ⬝ᵥ w) ((of : (a : Fin m → n' → α) → Matrix (Fin m) n' α) A *ᵥ w) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
m : ℕ
n' : Type uₙ
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n'
v : n' → α
A : Fin m → n' → α
w : n' → α
i : Fin m.succ
⊢ ((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A) *ᵥ w) i =
    vecCons (v ⬝ᵥ w) ((of : (a : Fin m → n' → α) → Matrix (Fin m) n' α) A *ᵥ w) i
have h : mulVec (m := Fin m.succ) ((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A)) w 0 =
  vecCons (n := m) (v ⬝ᵥ w) ((of : (a : Fin m → n' → α) → Matrix (Fin m) n' α) A *ᵥ w) 0
Tactic: refine Fin.cases ?_ ?_ i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
m : ℕ
n' : Type uₙ
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n'
v : n' → α
A : Fin m → n' → α
w : n' → α
i : Fin m.succ
h :
  mulVec (m := Fin m.succ) ((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A)) w 0 =
    vecCons (n := m) (v ⬝ᵥ w) ((of : (a : Fin m → n' → α) → Matrix (Fin m) n' α) A *ᵥ w) 0
⊢ ((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A) *ᵥ w) i =
    vecCons (v ⬝ᵥ w) ((of : (a : Fin m → n' → α) → Matrix (Fin m) n' α) A *ᵥ w) i
have h₁ : ∀ (i : Fin m),
  ((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A) *ᵥ w) i.succ =
    vecCons (v ⬝ᵥ w) ((of : (a : Fin m → n' → α) → Matrix (Fin m) n' α) A *ᵥ w) i.succ
Tactic: refine Fin.cases ?_ ?_ i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
n : ℕ
m' : Type uₘ
α : Type u_1
inst : NonUnitalCommSemiring α
A : m' → Fin n.succ → α
x : α
v : Fin n → α
⊢ (of : (a : m' → Fin n.succ → α) → Matrix m' (Fin n.succ) α) A *ᵥ vecCons x v =
    x • vecHead ∘ A + (of : (a : m' → Fin n → α) → Matrix m' (Fin n) α) (vecTail ∘ A) *ᵥ v
have h : ∀ (i : m'),
  ((of : (a : m' → Fin n.succ → α) → Matrix m' (Fin n.succ) α) A *ᵥ vecCons x v) i =
    HAdd.hAdd (β := m' → α) (x • vecHead ∘ A) ((of : (a : m' → Fin n → α) → Matrix m' (Fin n) α) (vecTail ∘ A) *ᵥ v) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
m : ℕ
n' : Type uₙ
inst : NonUnitalNonAssocSemiring α
x : α
v : Fin m → α
w : n' → α
⊢ vecMulVec (vecCons x v) w = vecCons (x • w) (vecMulVec v w)
have a : ∀ (i : Fin m.succ) (j : n'), vecMulVec (vecCons x v) w i j = vecCons (x • w) (vecMulVec v w) i j
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
m : ℕ
n' : Type uₙ
inst : NonUnitalNonAssocSemiring α
x : α
v : Fin m → α
w : n' → α
i : Fin m.succ
j : n'
⊢ vecMulVec (vecCons x v) w i j = vecCons (x • w) (vecMulVec v w) i j
have a : vecMulVec (vecCons x v) w 0 j = vecCons (x • w) (vecMulVec v w) 0 j
Tactic: refine Fin.cases ?_ ?_ i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
m : ℕ
n' : Type uₙ
inst : NonUnitalNonAssocSemiring α
x : α
v : Fin m → α
w : n' → α
i : Fin m.succ
j : n'
a : vecMulVec (vecCons x v) w 0 j = vecCons (x • w) (vecMulVec v w) 0 j
⊢ vecMulVec (vecCons x v) w i j = vecCons (x • w) (vecMulVec v w) i j
have a₁ : ∀ (i : Fin m), vecMulVec (vecCons x v) w i.succ j = vecCons (x • w) (vecMulVec v w) i.succ j
Tactic: refine Fin.cases ?_ ?_ i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
A : Matrix m' n' α
i : m'
row : Fin m → m'
col : o' → n'
⊢ A.submatrix (vecCons i row) col = vecCons (fun (j : o') ↦ A i (col j)) (A.submatrix row col)
have a : ∀ (i_1 : Fin m.succ) (j : o'),
  A.submatrix (vecCons i row) col i_1 j = vecCons (fun (j : o') ↦ A i (col j)) (A.submatrix row col) i_1 j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
A : Matrix m' n' α
i_1 : m'
row : Fin m → m'
col : o' → n'
i : Fin m.succ
j : o'
⊢ A.submatrix (vecCons i_1 row) col i j = vecCons (fun (j : o') ↦ A i_1 (col j)) (A.submatrix row col) i j
have a : A.submatrix (vecCons i_1 row) col 0 j = vecCons (fun (j : o') ↦ A i_1 (col j)) (A.submatrix row col) 0 j
Tactic: refine Fin.cases ?_ ?_ i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
A : Matrix m' n' α
i_1 : m'
row : Fin m → m'
col : o' → n'
i : Fin m.succ
j : o'
a : A.submatrix (vecCons i_1 row) col 0 j = vecCons (fun (j : o') ↦ A i_1 (col j)) (A.submatrix row col) 0 j
⊢ A.submatrix (vecCons i_1 row) col i j = vecCons (fun (j : o') ↦ A i_1 (col j)) (A.submatrix row col) i j
have a₁ : ∀ (i : Fin m),
  A.submatrix (vecCons i_1 row) col i.succ j = vecCons (fun (j : o') ↦ A i_1 (col j)) (A.submatrix row col) i.succ j
Tactic: refine Fin.cases ?_ ?_ i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
inst : Zero α
inst_1 : One α
⊢ Eq.{u + 1} (α := Matrix (Fin 2) (Fin 2) α) (1 : Matrix (Fin 2) (Fin 2) α) (!![1, 0; 0, 1] : Matrix (Fin 2) (Fin 2) α)
have a : ∀ (i j : Fin 2), Eq.{u + 1} (α := α) (1 i j : α) (!![1, 0; 0, 1] i j : α)
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
inst : Zero α
inst_1 : One α
i j : Fin 2
⊢ Eq.{u + 1} (α := α) (1 i j : α) (!![1, 0; 0, 1] i j : α)
have a : Eq.{u + 1} (α := α) (1 ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) j : α) (!![1, 0; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) j : α)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
inst : Zero α
inst_1 : One α
i j : Fin 2
a : Eq.{u + 1} (α := α) (1 ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j : α) (!![1, 0; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j : α)
⊢ Eq.{u + 1} (α := α) (1 i j : α) (!![1, 0; 0, 1] i j : α)
have a₁ : Eq.{u + 1} (α := α) (1 ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) j : α) (!![1, 0; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) j : α)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
inst : Zero α
inst_1 : One α
j : Fin 2
⊢ Eq.{u + 1} (α := α) (1 ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j : α) (!![1, 0; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j : α)
have a : Eq.{u + 1} (α := α) (1 ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) : α)
  (!![1, 0; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) : α)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
inst : Zero α
inst_1 : One α
j : Fin 2
a :
  Eq.{u + 1} (α := α) (1 ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : α)
    (!![1, 0; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : α)
⊢ Eq.{u + 1} (α := α) (1 ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j : α) (!![1, 0; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j : α)
have a₁ : Eq.{u + 1} (α := α) (1 ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) : α)
  (!![1, 0; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) : α)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
inst : Zero α
inst_1 : One α
j : Fin 2
⊢ Eq.{u + 1} (α := α) (1 ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j : α) (!![1, 0; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j : α)
have a : Eq.{u + 1} (α := α) (1 ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) : α)
  (!![1, 0; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) : α)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
inst : Zero α
inst_1 : One α
j : Fin 2
a :
  Eq.{u + 1} (α := α) (1 ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : α)
    (!![1, 0; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : α)
⊢ Eq.{u + 1} (α := α) (1 ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j : α) (!![1, 0; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j : α)
have a₁ : Eq.{u + 1} (α := α) (1 ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) : α)
  (!![1, 0; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) : α)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
inst : Zero α
inst_1 : One α
⊢ Eq.{u + 1} (α := Matrix (Fin 3) (Fin 3) α) (1 : Matrix (Fin 3) (Fin 3) α)
    (!![1, 0, 0; 0, 1, 0; 0, 0, 1] : Matrix (Fin 3) (Fin 3) α)
have a : ∀ (i j : Fin 3), Eq.{u + 1} (α := α) (1 i j : α) (!![1, 0, 0; 0, 1, 0; 0, 0, 1] i j : α)
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
inst : Zero α
inst_1 : One α
i j : Fin 3
⊢ Eq.{u + 1} (α := α) (1 i j : α) (!![1, 0, 0; 0, 1, 0; 0, 0, 1] i j : α)
have a : Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨0, sorry⟩) j : α)
  (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨0, sorry⟩) j : α)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
inst : Zero α
inst_1 : One α
i j : Fin 3
a :
  Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) j : α)
    (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) j : α)
⊢ Eq.{u + 1} (α := α) (1 i j : α) (!![1, 0, 0; 0, 1, 0; 0, 0, 1] i j : α)
have a₁ : Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨1, sorry⟩) j : α)
  (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨1, sorry⟩) j : α)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
inst : Zero α
inst_1 : One α
i j : Fin 3
a :
  Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) j : α)
    (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) j : α)
a₁ :
  Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) j : α)
    (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) j : α)
⊢ Eq.{u + 1} (α := α) (1 i j : α) (!![1, 0, 0; 0, 1, 0; 0, 0, 1] i j : α)
have a₂ : Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨2, sorry⟩) j : α)
  (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨2, sorry⟩) j : α)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
inst : Zero α
inst_1 : One α
j : Fin 3
⊢ Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) j : α)
    (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) j : α)
have a : Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 3) ↦ i) ⟨0, sorry⟩) : α)
  (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 3) ↦ i) ⟨0, sorry⟩) : α)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
inst : Zero α
inst_1 : One α
j : Fin 3
a :
  Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) : α)
    (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) : α)
⊢ Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) j : α)
    (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) j : α)
have a₁ : Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 3) ↦ i) ⟨1, sorry⟩) : α)
  (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 3) ↦ i) ⟨1, sorry⟩) : α)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u
inst : Zero α
inst_1 : One α
j : Fin 3
a :
  Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) : α)
    (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) : α)
a₁ :
  Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) : α)
    (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) : α)
⊢ Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) j : α)
    (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) j : α)
have a₂ : Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 3) ↦ i) ⟨2, sorry⟩) : α)
  (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 3) ↦ i) ⟨2, sorry⟩) : α)
Tactic: fin_cases j
Cleared hypotheses: j