awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonAssocSemiring α
f : l ≃. m
i : l
j : n
M : Matrix m n α
none :
  ∀ (h : Eq.{u_3 + 1} (α := Option m) ((f : (a : l) → Option m) i : Option m) (Option.none : Option m)),
    Eq.{u_5 + 1} (α := α) (∑ j_1 : m, (if Membership.mem (γ := Option m) Option.none j_1 then 1 else 0) * M j_1 j : α)
      (Option.rec (motive := fun (x : Option m) ↦ α) 0 (fun (val : m) ↦ M val j) Option.none : α)
⊢ Eq.{u_5 + 1} (α := α)
    (∑ j_1 : m,
        (if Membership.mem (γ := Option m) ((f : (a : l) → Option m) i : Option m) j_1 then 1 else 0) * M j_1 j :
      α)
    (Option.rec (motive := fun (x : Option m) ↦ α) 0 (fun (val : m) ↦ M val j) ((f : (a : l) → Option m) i) : α)
have some : ∀ (fi : m) (h : (f : (a : l) → Option m) i = some fi),
  Eq.{u_5 + 1} (α := α) (∑ j_1 : m, (if j_1 ∈ some fi then 1 else 0) * M j_1 j : α)
    (Option.rec (motive := fun (x : Option m) ↦ α) 0 (fun (val : m) ↦ M val j) (some fi) : α)
Tactic: rcases h : f i with - | fi
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonAssocSemiring α
f : l ≃. m
i : l
j : n
M : Matrix m n α
fi : m
h : (f : (a : l) → Option m) i = some fi
⊢ Eq.{u_5 + 1} (α := α) (∑ j_1 : m, (if j_1 ∈ some fi then 1 else 0) * M j_1 j : α)
    (Option.rec (motive := fun (x : Option m) ↦ α) 0 (fun (val : m) ↦ M val j) (some fi) : α)
have some : (if fi ∈ some fi then 1 else 0) * M fi j =
  Option.rec (motive := fun (x : Option m) ↦ α) 0 (fun (val : m) ↦ M val j) (some fi)
Tactic: rw [Finset.sum_eq_single fi]
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonAssocSemiring α
f : l ≃. m
i : l
j : n
M : Matrix m n α
fi : m
h : (f : (a : l) → Option m) i = Option.some fi
some :
  (if fi ∈ Option.some fi then 1 else 0) * M fi j =
    Option.rec (motive := fun (x : Option m) ↦ α) 0 (fun (val : m) ↦ M val j) (Option.some fi)
⊢ Eq.{u_5 + 1} (α := α) (∑ j_1 : m, (if j_1 ∈ Option.some fi then 1 else 0) * M j_1 j : α)
    (Option.rec (motive := fun (x : Option m) ↦ α) 0 (fun (val : m) ↦ M val j) (Option.some fi) : α)
have some₁ : ∀ (b : m), Membership.mem (γ := Finset m) Finset.univ b → b ≠ fi → (if b ∈ Option.some fi then 1 else 0) * M b j = 0
Tactic: rw [Finset.sum_eq_single fi]
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonAssocSemiring α
f : l ≃. m
i : l
j : n
M : Matrix m n α
fi : m
h : (f : (a : l) → Option m) i = Option.some fi
some :
  (if fi ∈ Option.some fi then 1 else 0) * M fi j =
    Option.rec (motive := fun (x : Option m) ↦ α) 0 (fun (val : m) ↦ M val j) (Option.some fi)
some₁ :
  ∀ (b : m), Membership.mem (γ := Finset m) Finset.univ b → b ≠ fi → (if b ∈ Option.some fi then 1 else 0) * M b j = 0
⊢ Eq.{u_5 + 1} (α := α) (∑ j_1 : m, (if j_1 ∈ Option.some fi then 1 else 0) * M j_1 j : α)
    (Option.rec (motive := fun (x : Option m) ↦ α) 0 (fun (val : m) ↦ M val j) (Option.some fi) : α)
have some₂ : fi ∉ Finset.univ → (if fi ∈ Option.some fi then 1 else 0) * M fi j = 0
Tactic: rw [Finset.sum_eq_single fi]
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : NonAssocSemiring α
inst_2 : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
⊢ HMul.hMul (β := Matrix m n α) M f.toMatrix i j =
    Option.casesOn (motive := fun (x : Option m) ↦ α) ((f.symm : (a : n) → Option m) j) 0 (M i)
have dsimp : Eq.{u_5 + 1} (α := α)
  (∑ j_1 : m, M i j_1 * if Membership.mem (γ := Option n) ((f : (a : m) → Option n) j_1 : Option n) j then 1 else 0 : α)
  (Option.rec (motive := fun (x : Option m) ↦ α) 0 (fun (val : m) ↦ M i val) ((f.symm : (a : n) → Option m) j) : α)
Tactic: dsimp [Matrix.mul_apply, toMatrix_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : NonAssocSemiring α
inst_2 : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
⊢ Eq.{u_5 + 1} (α := α)
    (∑ j_1 : m, M i j_1 * if Membership.mem (γ := Option n) ((f : (a : m) → Option n) j_1 : Option n) j then 1 else 0 :
      α)
    (Option.rec (motive := fun (x : Option m) ↦ α) 0 (fun (val : m) ↦ M i val) ((f.symm : (a : n) → Option m) j) : α)
have none : ∀ (h : Eq.{u_3 + 1} (α := Option m) ((f.symm : (a : n) → Option m) j : Option m) (none : Option m)),
  Eq.{u_5 + 1} (α := α)
    (∑ j_1 : m, M i j_1 * if Membership.mem (γ := Option n) ((f : (a : m) → Option n) j_1 : Option n) j then 1 else 0 :
      α)
    (Option.rec (motive := fun (x : Option m) ↦ α) 0 (fun (val : m) ↦ M i val) none : α)
Tactic: rcases h : f.symm j with - | fj
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : NonAssocSemiring α
inst_2 : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
none :
  ∀ (h : Eq.{u_3 + 1} (α := Option m) ((f.symm : (a : n) → Option m) j : Option m) (Option.none : Option m)),
    Eq.{u_5 + 1} (α := α)
      (∑ j_1 : m,
          M i j_1 * if Membership.mem (γ := Option n) ((f : (a : m) → Option n) j_1 : Option n) j then 1 else 0 :
        α)
      (Option.rec (motive := fun (x : Option m) ↦ α) 0 (fun (val : m) ↦ M i val) Option.none : α)
⊢ Eq.{u_5 + 1} (α := α)
    (∑ j_1 : m, M i j_1 * if Membership.mem (γ := Option n) ((f : (a : m) → Option n) j_1 : Option n) j then 1 else 0 :
      α)
    (Option.rec (motive := fun (x : Option m) ↦ α) 0 (fun (val : m) ↦ M i val) ((f.symm : (a : n) → Option m) j) : α)
have some : ∀ (fj : m) (h : (f.symm : (a : n) → Option m) j = some fj),
  Eq.{u_5 + 1} (α := α)
    (∑ j_1 : m, M i j_1 * if Membership.mem (γ := Option n) ((f : (a : m) → Option n) j_1 : Option n) j then 1 else 0 :
      α)
    (Option.rec (motive := fun (x : Option m) ↦ α) 0 (fun (val : m) ↦ M i val) (some fj) : α)
Tactic: rcases h : f.symm j with - | fj
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : NonAssocSemiring α
inst_2 : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
fj : m
h : (f.symm : (a : n) → Option m) j = some fj
⊢ Eq.{u_5 + 1} (α := α)
    (∑ j_1 : m, M i j_1 * if Membership.mem (γ := Option n) ((f : (a : m) → Option n) j_1 : Option n) j then 1 else 0 :
      α)
    (Option.rec (motive := fun (x : Option m) ↦ α) 0 (fun (val : m) ↦ M i val) (some fj) : α)
have some : (M i fj * if Membership.mem (γ := Option n) ((f : (a : m) → Option n) fj : Option n) j then 1 else 0) =
  Option.rec (motive := fun (x : Option m) ↦ α) 0 (fun (val : m) ↦ M i val) (some fj)
Tactic: rw [Finset.sum_eq_single fj]
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : NonAssocSemiring α
inst_2 : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
fj : m
h : (f.symm : (a : n) → Option m) j = Option.some fj
some :
  (M i fj * if Membership.mem (γ := Option n) ((f : (a : m) → Option n) fj : Option n) j then 1 else 0) =
    Option.rec (motive := fun (x : Option m) ↦ α) 0 (fun (val : m) ↦ M i val) (Option.some fj)
⊢ Eq.{u_5 + 1} (α := α)
    (∑ j_1 : m, M i j_1 * if Membership.mem (γ := Option n) ((f : (a : m) → Option n) j_1 : Option n) j then 1 else 0 :
      α)
    (Option.rec (motive := fun (x : Option m) ↦ α) 0 (fun (val : m) ↦ M i val) (Option.some fj) : α)
have some₁ : ∀ (b : m),
  Membership.mem (γ := Finset m) Finset.univ b →
    b ≠ fj → (M i b * if Membership.mem (γ := Option n) ((f : (a : m) → Option n) b : Option n) j then 1 else 0) = 0
Tactic: rw [Finset.sum_eq_single fj]
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : NonAssocSemiring α
inst_2 : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
fj : m
h : (f.symm : (a : n) → Option m) j = Option.some fj
some :
  (M i fj * if Membership.mem (γ := Option n) ((f : (a : m) → Option n) fj : Option n) j then 1 else 0) =
    Option.rec (motive := fun (x : Option m) ↦ α) 0 (fun (val : m) ↦ M i val) (Option.some fj)
some₁ :
  ∀ (b : m),
    Membership.mem (γ := Finset m) Finset.univ b →
      b ≠ fj → (M i b * if Membership.mem (γ := Option n) ((f : (a : m) → Option n) b : Option n) j then 1 else 0) = 0
⊢ Eq.{u_5 + 1} (α := α)
    (∑ j_1 : m, M i j_1 * if Membership.mem (γ := Option n) ((f : (a : m) → Option n) j_1 : Option n) j then 1 else 0 :
      α)
    (Option.rec (motive := fun (x : Option m) ↦ α) 0 (fun (val : m) ↦ M i val) (Option.some fj) : α)
have some₂ : fj ∉ Finset.univ →
  (M i fj * if Membership.mem (γ := Option n) ((f : (a : m) → Option n) fj : Option n) j then 1 else 0) = 0
Tactic: rw [Finset.sum_eq_single fj]
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Zero α
inst_3 : One α
f : m ≃. n
⊢ Eq (α := Matrix n m α) f.symm.toMatrix f.toMatrixᵀ
have a : ∀ (i : n) (j : m), Eq.{u_5 + 1} (α := α) (f.symm.toMatrix i j) (f.toMatrixᵀ i j)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Zero α
inst_3 : One α
f : m ≃. n
i : n
j : m
⊢ Eq.{u_5 + 1} (α := α) (f.symm.toMatrix i j) (f.toMatrixᵀ i j)
have a : Eq.{u_5 + 1} (α := α) (if Membership.mem (γ := Option n) ((f : (a : m) → Option n) j : Option n) i then 1 else 0 : α)
  ((of : (a : n → m → α) → Matrix n m α)
      (fun (x : n) (y : m) ↦ if Membership.mem (γ := Option n) ((f : (a : m) → Option n) y : Option n) x then 1 else 0)
      i j :
    α)
Tactic: simp only [transpose, mem_iff_mem f, toMatrix_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : Zero α
inst_2 : One α
⊢ Eq (α := Matrix n n α) (PEquiv.refl n).toMatrix 1
have a : ∀ (i j : n), Eq.{u_5 + 1} (α := α) ((PEquiv.refl n).toMatrix i j) (1 i j)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : Zero α
inst_2 : One α
f : m ≃ n
i : m
⊢ Eq (α := n → α) (f.toPEquiv.toMatrix i) (Pi.single (M := fun (a : n) ↦ α) ((f : (a : m) → n) i) 1)
have h : ∀ (x : n),
  Eq.{u_5 + 1} (α := α) (f.toPEquiv.toMatrix i x : α) (Pi.single (M := fun (a : n) ↦ α) ((f : (a : m) → n) i) 1 x : α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Zero α
inst_3 : One α
f : m ≃ n
j : n
⊢ Eq (α := m → α) (f.toPEquiv.toMatrixᵀ j) (Pi.single (M := fun (a : m) ↦ α) ((f.symm : (a : n) → m) j) 1)
have h : ∀ (x : m),
  Eq.{u_5 + 1} (α := α) (f.toPEquiv.toMatrixᵀ j x : α)
    (Pi.single (M := fun (a : m) ↦ α) ((f.symm : (a : n) → m) j) 1 x : α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonAssocSemiring α
f : l ≃ m
M : Matrix m n α
⊢ HMul.hMul (α := Matrix l m α) f.toPEquiv.toMatrix M = M.submatrix (⇑f : (a : l) → m) id
have a : ∀ (i : l) (j : n), HMul.hMul (α := Matrix l m α) f.toPEquiv.toMatrix M i j = M.submatrix (⇑f : (a : l) → m) id i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonAssocSemiring α
f : l ≃ m
M : Matrix m n α
i : l
j : n
⊢ HMul.hMul (α := Matrix l m α) f.toPEquiv.toMatrix M i j = M.submatrix (⇑f : (a : l) → m) id i j
have a : (Option.casesOn (motive := fun (x : Option m) ↦ α) ((f.toPEquiv : (a : l) → Option m) i) 0 fun (fi : m) ↦ M fi j) =
  M.submatrix (⇑f : (a : l) → m) id i j
Tactic: rw [toMatrix_mul_apply, Equiv.toPEquiv_apply, submatrix_apply, id]
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonAssocSemiring α
f : l ≃ m
M : Matrix m n α
i : l
j : n
a :
  (Option.casesOn (motive := fun (x : Option m) ↦ α) ((f.toPEquiv : (a : l) → Option m) i) 0 fun (fi : m) ↦ M fi j) =
    M.submatrix (⇑f : (a : l) → m) id i j
⊢ HMul.hMul (α := Matrix l m α) f.toPEquiv.toMatrix M i j = M.submatrix (⇑f : (a : l) → m) id i j
have a₁ : (Option.casesOn.{u_5 + 1, u_3} (α := m) (motive := fun (x : Option m) ↦ α) (some ((f : (a : l) → m) i) : Option m)
    (0 : α) fun (fi : m) ↦ M fi j) =
  M.submatrix (⇑f : (a : l) → m) id i j
Tactic: rw [toMatrix_mul_apply, Equiv.toPEquiv_apply, submatrix_apply, id]
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonAssocSemiring α
f : l ≃ m
M : Matrix m n α
i : l
j : n
a :
  (Option.casesOn (motive := fun (x : Option m) ↦ α) ((f.toPEquiv : (a : l) → Option m) i) 0 fun (fi : m) ↦ M fi j) =
    M.submatrix (⇑f : (a : l) → m) id i j
a₁ :
  (Option.casesOn.{u_5 + 1, u_3} (α := m) (motive := fun (x : Option m) ↦ α) (some ((f : (a : l) → m) i) : Option m)
      (0 : α) fun (fi : m) ↦ M fi j) =
    M.submatrix (⇑f : (a : l) → m) id i j
⊢ HMul.hMul (α := Matrix l m α) f.toPEquiv.toMatrix M i j = M.submatrix (⇑f : (a : l) → m) id i j
have a₂ : (Option.casesOn.{u_5 + 1, u_3} (α := m) (motive := fun (x : Option m) ↦ α) (some ((f : (a : l) → m) i) : Option m)
    (0 : α) fun (fi : m) ↦ M fi j) =
  M ((f : (a : l) → m) i) (id j)
Tactic: rw [toMatrix_mul_apply, Equiv.toPEquiv_apply, submatrix_apply, id]
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonAssocSemiring α
f : l ≃ m
M : Matrix m n α
i : l
j : n
a :
  (Option.casesOn (motive := fun (x : Option m) ↦ α) ((f.toPEquiv : (a : l) → Option m) i) 0 fun (fi : m) ↦ M fi j) =
    M.submatrix (⇑f : (a : l) → m) id i j
a₁ :
  (Option.casesOn.{u_5 + 1, u_3} (α := m) (motive := fun (x : Option m) ↦ α) (some ((f : (a : l) → m) i) : Option m)
      (0 : α) fun (fi : m) ↦ M fi j) =
    M.submatrix (⇑f : (a : l) → m) id i j
a₂ :
  (Option.casesOn.{u_5 + 1, u_3} (α := m) (motive := fun (x : Option m) ↦ α) (some ((f : (a : l) → m) i) : Option m)
      (0 : α) fun (fi : m) ↦ M fi j) =
    M ((f : (a : l) → m) i) (id j)
⊢ HMul.hMul (α := Matrix l m α) f.toPEquiv.toMatrix M i j = M.submatrix (⇑f : (a : l) → m) id i j
have a₃ : (Option.casesOn.{u_5 + 1, u_3} (α := m) (motive := fun (x : Option m) ↦ α) (some ((f : (a : l) → m) i) : Option m)
    (0 : α) fun (fi : m) ↦ M fi j) =
  M ((f : (a : l) → m) i) j
Tactic: rw [toMatrix_mul_apply, Equiv.toPEquiv_apply, submatrix_apply, id]
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : DecidableEq n
inst_2 : NonAssocSemiring α
M : Matrix l m α
f : m ≃ n
i : l
j : n
⊢ HMul.hMul (β := Matrix m n α) M f.toPEquiv.toMatrix i j = M.submatrix id (⇑f.symm : (a : n) → m) i j
have rw : Option.casesOn (motive := fun (x : Option m) ↦ α) ((f.toPEquiv.symm : (a : n) → Option m) j) 0 (M i) =
  M.submatrix id (⇑f.symm : (a : n) → m) i j
Tactic: rw [PEquiv.mul_toMatrix_apply, ← Equiv.toPEquiv_symm, Equiv.toPEquiv_apply,
      Matrix.submatrix_apply, id]
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : DecidableEq n
inst_2 : NonAssocSemiring α
M : Matrix l m α
f : m ≃ n
i : l
j : n
rw :
  Option.casesOn (motive := fun (x : Option m) ↦ α) ((f.toPEquiv.symm : (a : n) → Option m) j) 0 (M i) =
    M.submatrix id (⇑f.symm : (a : n) → m) i j
⊢ HMul.hMul (β := Matrix m n α) M f.toPEquiv.toMatrix i j = M.submatrix id (⇑f.symm : (a : n) → m) i j
have rw₁ : Option.casesOn (motive := fun (x : Option m) ↦ α) ((f.symm.toPEquiv : (a : n) → Option m) j) 0 (M i) =
  M.submatrix id (⇑f.symm : (a : n) → m) i j
Tactic: rw [PEquiv.mul_toMatrix_apply, ← Equiv.toPEquiv_symm, Equiv.toPEquiv_apply,
      Matrix.submatrix_apply, id]
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : DecidableEq n
inst_2 : NonAssocSemiring α
M : Matrix l m α
f : m ≃ n
i : l
j : n
rw :
  Option.casesOn (motive := fun (x : Option m) ↦ α) ((f.toPEquiv.symm : (a : n) → Option m) j) 0 (M i) =
    M.submatrix id (⇑f.symm : (a : n) → m) i j
rw₁ :
  Option.casesOn (motive := fun (x : Option m) ↦ α) ((f.symm.toPEquiv : (a : n) → Option m) j) 0 (M i) =
    M.submatrix id (⇑f.symm : (a : n) → m) i j
⊢ HMul.hMul (β := Matrix m n α) M f.toPEquiv.toMatrix i j = M.submatrix id (⇑f.symm : (a : n) → m) i j
have rw₂ : Option.casesOn.{u_5 + 1, u_3} (α := m) (motive := fun (x : Option m) ↦ α) (some ((f.symm : (a : n) → m) j) : Option m)
    (0 : α) (M i) =
  M.submatrix id (⇑f.symm : (a : n) → m) i j
Tactic: rw [PEquiv.mul_toMatrix_apply, ← Equiv.toPEquiv_symm, Equiv.toPEquiv_apply,
      Matrix.submatrix_apply, id]
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : DecidableEq n
inst_2 : NonAssocSemiring α
M : Matrix l m α
f : m ≃ n
i : l
j : n
rw :
  Option.casesOn (motive := fun (x : Option m) ↦ α) ((f.toPEquiv.symm : (a : n) → Option m) j) 0 (M i) =
    M.submatrix id (⇑f.symm : (a : n) → m) i j
rw₁ :
  Option.casesOn (motive := fun (x : Option m) ↦ α) ((f.symm.toPEquiv : (a : n) → Option m) j) 0 (M i) =
    M.submatrix id (⇑f.symm : (a : n) → m) i j
rw₂ :
  Option.casesOn.{u_5 + 1, u_3} (α := m) (motive := fun (x : Option m) ↦ α) (some ((f.symm : (a : n) → m) j) : Option m)
      (0 : α) (M i) =
    M.submatrix id (⇑f.symm : (a : n) → m) i j
⊢ HMul.hMul (β := Matrix m n α) M f.toPEquiv.toMatrix i j = M.submatrix id (⇑f.symm : (a : n) → m) i j
have rw₃ : Option.casesOn.{u_5 + 1, u_3} (α := m) (motive := fun (x : Option m) ↦ α) (some ((f.symm : (a : n) → m) j) : Option m)
    (0 : α) (M i) =
  M (id i) ((f.symm : (a : n) → m) j)
Tactic: rw [PEquiv.mul_toMatrix_apply, ← Equiv.toPEquiv_symm, Equiv.toPEquiv_apply,
      Matrix.submatrix_apply, id]
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : DecidableEq n
inst_2 : NonAssocSemiring α
M : Matrix l m α
f : m ≃ n
i : l
j : n
rw :
  Option.casesOn (motive := fun (x : Option m) ↦ α) ((f.toPEquiv.symm : (a : n) → Option m) j) 0 (M i) =
    M.submatrix id (⇑f.symm : (a : n) → m) i j
rw₁ :
  Option.casesOn (motive := fun (x : Option m) ↦ α) ((f.symm.toPEquiv : (a : n) → Option m) j) 0 (M i) =
    M.submatrix id (⇑f.symm : (a : n) → m) i j
rw₂ :
  Option.casesOn.{u_5 + 1, u_3} (α := m) (motive := fun (x : Option m) ↦ α) (some ((f.symm : (a : n) → m) j) : Option m)
      (0 : α) (M i) =
    M.submatrix id (⇑f.symm : (a : n) → m) i j
rw₃ :
  Option.casesOn.{u_5 + 1, u_3} (α := m) (motive := fun (x : Option m) ↦ α) (some ((f.symm : (a : n) → m) j) : Option m)
      (0 : α) (M i) =
    M (id i) ((f.symm : (a : n) → m) j)
⊢ HMul.hMul (β := Matrix m n α) M f.toPEquiv.toMatrix i j = M.submatrix id (⇑f.symm : (a : n) → m) i j
have rw₄ : Option.casesOn.{u_5 + 1, u_3} (α := m) (motive := fun (x : Option m) ↦ α) (some ((f.symm : (a : n) → m) j) : Option m)
    (0 : α) (M i) =
  M i ((f.symm : (a : n) → m) j)
Tactic: rw [PEquiv.mul_toMatrix_apply, ← Equiv.toPEquiv_symm, Equiv.toPEquiv_apply,
      Matrix.submatrix_apply, id]
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : NonAssocSemiring α
σ : m ≃ n
a : n → α
⊢ σ.toPEquiv.toMatrix *ᵥ a = a ∘ (⇑σ : (a : m) → n)
have h : ∀ (j : m), (σ.toPEquiv.toMatrix *ᵥ a) j = (a ∘ (⇑σ : (a : m) → n)) j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : Fintype m
inst_2 : NonAssocSemiring α
σ : m ≃ n
a : m → α
⊢ a ᵥ* σ.toPEquiv.toMatrix = a ∘ (⇑σ.symm : (a : n) → m)
have h : ∀ (j : n), (a ᵥ* σ.toPEquiv.toMatrix) j = (a ∘ (⇑σ.symm : (a : n) → m)) j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : Fintype m
inst_2 : NonAssocSemiring α
σ : m ≃ n
a : m → α
⊢ a ᵥ* σ.toPEquiv.toMatrix = a ∘ (⇑σ.symm : (a : n) → m)
have h : ∀ (j : n), (a ᵥ* σ.toPEquiv.toMatrix) j = (a ∘ (⇑σ.symm : (a : n) → m)) j
Tactic: classical
  ext j
  simp [toMatrix, σ.apply_eq_iff_eq_symm_apply, vecMul, dotProduct]
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : NonAssocSemiring α
f : l ≃. m
g : m ≃. n
⊢ (f.trans g).toMatrix = HMul.hMul (α := Matrix l m α) (β := Matrix m n α) f.toMatrix g.toMatrix
have a : ∀ (i : l) (j : n),
  (f.trans g).toMatrix i j = HMul.hMul (α := Matrix l m α) (β := Matrix m n α) f.toMatrix g.toMatrix i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : NonAssocSemiring α
f : l ≃. m
g : m ≃. n
i : l
j : n
⊢ (f.trans g).toMatrix i j = HMul.hMul (α := Matrix l m α) (β := Matrix m n α) f.toMatrix g.toMatrix i j
have a : Eq.{u_5 + 1} (α := α) ((f.trans g).toMatrix i j : α)
  (Option.casesOn (motive := fun (x : Option m) ↦ α) ((f : (a : l) → Option m) i) 0 fun (fi : m) ↦ g.toMatrix fi j : α)
Tactic: rw [toMatrix_mul_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : NonAssocSemiring α
f : l ≃. m
g : m ≃. n
i : l
j : n
⊢ Eq.{u_5 + 1} (α := α) ((f.trans g).toMatrix i j : α)
    (Option.casesOn (motive := fun (x : Option m) ↦ α) ((f : (a : l) → Option m) i) 0 fun (fi : m) ↦ g.toMatrix fi j :
      α)
have a : Eq.{u_5 + 1} (α := α)
  (if
        Membership.mem (γ := Option n)
          (Option.bind.{u_3, u_4} (α := m) ((f : (a : l) → Option m) i) (⇑g : (a : m) → Option n)) j then
      1
    else 0 :
    α)
  (Option.rec (motive := fun (x : Option m) ↦ α) 0
      (fun (val : m) ↦ if Membership.mem (γ := Option n) ((g : (a : m) → Option n) val : Option n) j then 1 else 0)
      ((f : (a : l) → Option m) i) :
    α)
Tactic: dsimp +instances [toMatrix, PEquiv.trans]
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : NonAssocSemiring α
f : l ≃. m
g : m ≃. n
i : l
j : n
⊢ Eq.{u_5 + 1} (α := α)
    (if
          Membership.mem (γ := Option n)
            (Option.bind.{u_3, u_4} (α := m) ((f : (a : l) → Option m) i) (⇑g : (a : m) → Option n)) j then
        1
      else 0 :
      α)
    (Option.rec (motive := fun (x : Option m) ↦ α) 0
        (fun (val : m) ↦ if Membership.mem (γ := Option n) ((g : (a : m) → Option n) val : Option n) j then 1 else 0)
        ((f : (a : l) → Option m) i) :
      α)
have a : Eq.{u_5 + 1} (α := α)
  (if Membership.mem (γ := Option n) (Option.bind.{u_3, u_4} (α := m) none (⇑g : (a : m) → Option n)) j then 1 else 0 :
    α)
  (Option.rec (motive := fun (x : Option m) ↦ α) 0
      (fun (val : m) ↦ if Membership.mem (γ := Option n) ((g : (a : m) → Option n) val : Option n) j then 1 else 0)
      none :
    α)
Tactic: cases f i