awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Matrix.PEquiv
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 α
h : Eq.{u_3 + 1} (α := Option m) ((f : (a : l) → Option m) i : Option m) (none : Option m)
⊢ Eq.{u_5 + 1} (α := α) (∑ j_1 : m, (if Membership.mem (γ := Option m) 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) none : α)

Tactic:
simp
-- Module: Mathlib.Data.Matrix.PEquiv
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
some₂ : fi ∉ Finset.univ → (if fi ∈ Option.some fi then 1 else 0) * M fi 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) : α)

Tactic:
rw [Finset.sum_eq_single fi]

Premises used: Finset.sum_eq_single
-- Module: Mathlib.Data.Matrix.PEquiv
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
⊢ (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:
simp +contextual [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Data.Matrix.PEquiv
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
⊢ ∀ (b : m), Membership.mem (γ := Finset m) Finset.univ b → b ≠ fi → (if b ∈ some fi then 1 else 0) * M b j = 0

Tactic:
simp +contextual [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Data.Matrix.PEquiv
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
⊢ fi ∉ Finset.univ → (if fi ∈ some fi then 1 else 0) * M fi j = 0

Tactic:
simp +contextual [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Data.Matrix.PEquiv
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
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) : α)
⊢ 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)

Tactic:
dsimp [Matrix.mul_apply, toMatrix_apply]

Premises used: Matrix.mul_apply, PEquiv.toMatrix_apply
-- Module: Mathlib.Data.Matrix.PEquiv
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 : α)
some :
  ∀ (fj : m) (h : (f.symm : (a : n) → Option m) j = 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) : α)
⊢ 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:
rcases h : f.symm j with - | fj

Premises used: DFunLike.coe, PEquiv.symm
-- Module: Mathlib.Data.Matrix.PEquiv
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
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:
simp [h, ← f.eq_some_iff]

Premises used: PEquiv.eq_some_iff
-- Module: Mathlib.Data.Matrix.PEquiv
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
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
⊢ 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) : α)

Tactic:
rw [Finset.sum_eq_single fj]

Premises used: Finset.sum_eq_single
-- Module: Mathlib.Data.Matrix.PEquiv
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
⊢ (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:
simp [h, ← f.eq_some_iff]

Premises used: PEquiv.eq_some_iff
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
l : Type u_2
m : Type u_3
n_1 : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : NonAssocSemiring α
inst_2 : DecidableEq n_1
M : Matrix l m α
f : m ≃. n_1
i : l
j : n_1
fj : m
h : (f.symm : (a : n_1) → Option m) j = some fj
b : m
n : b ≠ fj
⊢ (M i b * if Membership.mem (γ := Option n_1) ((f : (a : m) → Option n_1) b : Option n_1) j then 1 else 0) = 0

Tactic:
simp [h, ← f.eq_some_iff, n.symm]

Premises used: Ne.symm, PEquiv.eq_some_iff
-- Module: Mathlib.Data.Matrix.PEquiv
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
⊢ 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:
simp
-- Module: Mathlib.Data.Matrix.PEquiv
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
a : ∀ (i : n) (j : m), Eq.{u_5 + 1} (α := α) (f.symm.toMatrix i j) (f.toMatrixᵀ i j)
⊢ Eq (α := Matrix n m α) f.symm.toMatrix f.toMatrixᵀ

Tactic:
ext
-- Module: Mathlib.Data.Matrix.PEquiv
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
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 :
      α)
⊢ Eq.{u_5 + 1} (α := α) (f.symm.toMatrix i j) (f.toMatrixᵀ i j)

Tactic:
simp only [transpose, mem_iff_mem f, toMatrix_apply]

Premises used: PEquiv.mem_iff_mem, Matrix.transpose, PEquiv.toMatrix_apply
-- Module: Mathlib.Data.Matrix.PEquiv
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} (α := α) (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:
congr
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : Zero α
inst_2 : One α
a : ∀ (i j : n), Eq.{u_5 + 1} (α := α) ((PEquiv.refl n).toMatrix i j) (1 i j)
⊢ Eq (α := Matrix n n α) (PEquiv.refl n).toMatrix 1

Tactic:
ext
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : Zero α
inst_2 : One α
i j : n
⊢ Eq.{u_5 + 1} (α := α) ((PEquiv.refl n).toMatrix i j) (1 i j)

Tactic:
simp [toMatrix_apply, one_apply]

Premises used: Matrix.one_apply, PEquiv.toMatrix_apply
-- Module: Mathlib.Data.Matrix.PEquiv
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
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 : α)
⊢ Eq (α := n → α) (f.toPEquiv.toMatrix i) (Pi.single (M := fun (a : n) ↦ α) ((f : (a : m) → n) i) 1)

Tactic:
ext
-- Module: Mathlib.Data.Matrix.PEquiv
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
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:
simp [toMatrix_apply, Pi.single_apply, eq_comm]

Premises used: Pi.single_apply, eq_comm, PEquiv.toMatrix_apply
-- Module: Mathlib.Data.Matrix.PEquiv
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
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 : α)
⊢ Eq (α := m → α) (f.toPEquiv.toMatrixᵀ j) (Pi.single (M := fun (a : m) ↦ α) ((f.symm : (a : n) → m) j) 1)

Tactic:
ext
-- Module: Mathlib.Data.Matrix.PEquiv
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
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:
simp [toMatrix_apply, Pi.single_apply, eq_comm, ← Equiv.apply_eq_iff_eq_symm_apply]

Premises used: Pi.single_apply, eq_comm, PEquiv.toMatrix_apply, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Data.Matrix.PEquiv
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 α
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
⊢ HMul.hMul (α := Matrix l m α) f.toPEquiv.toMatrix M = M.submatrix (⇑f : (a : l) → m) id

Tactic:
ext i j
-- Module: Mathlib.Data.Matrix.PEquiv
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)
a₃ 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
⊢ HMul.hMul (α := Matrix l m α) f.toPEquiv.toMatrix M i j = M.submatrix (⇑f : (a : l) → m) id i j

Tactic:
rw [toMatrix_mul_apply, Equiv.toPEquiv_apply, submatrix_apply, id]

Premises used: Equiv.toPEquiv_apply, id, Matrix.submatrix_apply, PEquiv.toMatrix_mul_apply
-- Module: Mathlib.Data.Matrix.PEquiv
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)
rw₄ 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)
⊢ HMul.hMul (β := Matrix m n α) M f.toPEquiv.toMatrix i j = 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]

Premises used: Equiv.toPEquiv_apply, PEquiv.mul_toMatrix_apply, id, Equiv.toPEquiv_symm, Matrix.submatrix_apply
-- Module: Mathlib.Data.Matrix.PEquiv
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 → α
h : ∀ (j : m), (σ.toPEquiv.toMatrix *ᵥ a) j = (a ∘ (⇑σ : (a : m) → n)) j
⊢ σ.toPEquiv.toMatrix *ᵥ a = a ∘ (⇑σ : (a : m) → n)

Tactic:
ext j
-- Module: Mathlib.Data.Matrix.PEquiv
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 → α
j : m
⊢ (σ.toPEquiv.toMatrix *ᵥ a) j = (a ∘ (⇑σ : (a : m) → n)) j

Tactic:
simp [toMatrix, mulVec, dotProduct]

Premises used: dotProduct, PEquiv.toMatrix, Matrix.mulVec
-- Module: Mathlib.Data.Matrix.PEquiv
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 → α
h : ∀ (j : n), (a ᵥ* σ.toPEquiv.toMatrix) j = (a ∘ (⇑σ.symm : (a : n) → m)) j
⊢ a ᵥ* σ.toPEquiv.toMatrix = a ∘ (⇑σ.symm : (a : n) → m)

Tactic:
ext j
-- Module: Mathlib.Data.Matrix.PEquiv
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 → α
j : n
⊢ (a ᵥ* σ.toPEquiv.toMatrix) j = (a ∘ (⇑σ.symm : (a : n) → m)) j

Tactic:
simp [toMatrix, σ.apply_eq_iff_eq_symm_apply, vecMul, dotProduct]

Premises used: dotProduct, Matrix.vecMul, PEquiv.toMatrix, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Data.Matrix.PEquiv
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 → α
h : ∀ (j : n), (a ᵥ* σ.toPEquiv.toMatrix) j = (a ∘ (⇑σ.symm : (a : n) → m)) j
⊢ a ᵥ* σ.toPEquiv.toMatrix = a ∘ (⇑σ.symm : (a : n) → m)

Tactic:
classical
  ext j
  simp [toMatrix, σ.apply_eq_iff_eq_symm_apply, vecMul, dotProduct]

Premises used: dotProduct, Matrix.vecMul, PEquiv.toMatrix, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Data.Matrix.PEquiv
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
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
⊢ (f.trans g).toMatrix = HMul.hMul (α := Matrix l m α) (β := Matrix m n α) f.toMatrix g.toMatrix

Tactic:
ext i j
-- Module: Mathlib.Data.Matrix.PEquiv
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
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 :
      α)
⊢ (f.trans g).toMatrix i j = HMul.hMul (α := Matrix l m α) (β := Matrix m n α) f.toMatrix g.toMatrix i j

Tactic:
rw [toMatrix_mul_apply]

Premises used: PEquiv.toMatrix_mul_apply
-- Module: Mathlib.Data.Matrix.PEquiv
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
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) :
      α)
⊢ 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:
dsimp +instances [toMatrix, PEquiv.trans]

Premises used: PEquiv.toMatrix, PEquiv.trans
-- Module: Mathlib.Data.Matrix.PEquiv
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
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 :
      α)
a₁ :
  ∀ (val : m),
    Eq.{u_5 + 1} (α := α)
      (if Membership.mem (γ := Option n) ((some val).bind (⇑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)
          (some val) :
        α)
⊢ 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:
cases f i

Premises used: DFunLike.coe
-- Module: Mathlib.Data.Matrix.PEquiv
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) 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:
simp
-- Module: Mathlib.Data.Matrix.PEquiv
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
val : m
⊢ Eq.{u_5 + 1} (α := α)
    (if Membership.mem (γ := Option n) ((some val).bind (⇑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)
        (some val) :
      α)

Tactic:
simp
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : Zero α
inst_2 : One α
⊢ Eq (α := Matrix m n α) (toMatrix ⊥) 0

Tactic:
rfl

Premises used: PEquiv.toMatrix, rfl, ite
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : MulZeroOneClass α
inst_2 : Nontrivial α
f g : m ≃. n
⊢ Eq (α := Matrix m n α) f.toMatrix g.toMatrix → f = g

Tactic:
not_imp_not.1 ?_

Premises used: Iff.mp, not_imp_not
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : MulZeroOneClass α
inst_2 : Nontrivial α
f g : m ≃. n
refine : ¬f = g → ¬Eq (α := Matrix m n α) f.toMatrix g.toMatrix
⊢ Eq (α := Matrix m n α) f.toMatrix g.toMatrix → f = g

Tactic:
refine not_imp_not.1 ?_

Premises used: Iff.mp, not_imp_not
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : MulZeroOneClass α
inst_2 : Nontrivial α
f g : m ≃. n
simp :
  ∀ (x : m),
    ¬Eq.{u_4 + 1} (α := Option n) ((f : (a : m) → Option n) x : Option n) ((g : (a : m) → Option n) x : Option n) →
      ∃ (x : m) (x_1 : n),
        ¬Eq.{u_5 + 1} (α := α)
            (if Membership.mem (γ := Option n) ((f : (a : m) → Option n) x : Option n) x_1 then 1 else 0)
            (if Membership.mem (γ := Option n) ((g : (a : m) → Option n) x : Option n) x_1 then 1 else 0)
⊢ ¬f = g → ¬Eq (α := Matrix m n α) f.toMatrix g.toMatrix

Tactic:
simp only [Matrix.ext_iff.symm, toMatrix_apply, PEquiv.ext_iff, not_forall, exists_imp]

Premises used: PEquiv.ext_iff, Matrix.ext_iff, PEquiv.toMatrix_apply, exists_imp, Classical.not_forall, Iff.symm
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : MulZeroOneClass α
inst_2 : Nontrivial α
f g : m ≃. n
i : m
hi : ¬Eq.{u_4 + 1} (α := Option n) ((f : (a : m) → Option n) i : Option n) ((g : (a : m) → Option n) i : Option n)
h :
  ∃ (x : n),
    ¬Eq.{u_5 + 1} (α := α) (if Membership.mem (γ := Option n) ((f : (a : m) → Option n) i : Option n) x then 1 else 0)
        (if Membership.mem (γ := Option n) ((g : (a : m) → Option n) i : Option n) x then 1 else 0)
⊢ ∃ (x : m) (x_1 : n),
    ¬Eq.{u_5 + 1} (α := α) (if Membership.mem (γ := Option n) ((f : (a : m) → Option n) x : Option n) x_1 then 1 else 0)
        (if Membership.mem (γ := Option n) ((g : (a : m) → Option n) x : Option n) x_1 then 1 else 0)

Tactic:
use i