[GOAL]
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Semiring α
f : l ≃. m
M : Matrix m n α
i : l
j : n
⊢ (toMatrix f * M) i j = Option.casesOn (↑f i) 0 fun fi => M fi j
[PROOFSTEP]
dsimp [toMatrix, Matrix.mul_apply]
[GOAL]
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Semiring α
f : l ≃. m
M : Matrix m n α
i : l
j : n
⊢ (Finset.sum Finset.univ fun j_1 => (if j_1 ∈ ↑f i then 1 else 0) * M j_1 j) = Option.rec 0 (fun val => M val j) (↑f i)
[PROOFSTEP]
cases' h : f i with fi
[GOAL]
case none
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Semiring α
f : l ≃. m
M : Matrix m n α
i : l
j : n
h : ↑f i = none
⊢ (Finset.sum Finset.univ fun j_1 => (if j_1 ∈ none then 1 else 0) * M j_1 j) = Option.rec 0 (fun val => M val j) none
[PROOFSTEP]
simp [h]
[GOAL]
case some
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Semiring α
f : l ≃. m
M : Matrix m n α
i : l
j : n
fi : m
h : ↑f i = some fi
⊢ (Finset.sum Finset.univ fun j_1 => (if j_1 ∈ some fi then 1 else 0) * M j_1 j) =
    Option.rec 0 (fun val => M val j) (some fi)
[PROOFSTEP]
rw [Finset.sum_eq_single fi]
[GOAL]
case some
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Semiring α
f : l ≃. m
M : Matrix m n α
i : l
j : n
fi : m
h : ↑f i = some fi
⊢ (if fi ∈ some fi then 1 else 0) * M fi j = Option.rec 0 (fun val => M val j) (some fi)
[PROOFSTEP]
simp (config := { contextual := true }) [h, eq_comm]
[GOAL]
case some.h₀
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Semiring α
f : l ≃. m
M : Matrix m n α
i : l
j : n
fi : m
h : ↑f i = some fi
⊢ ∀ (b : m), b ∈ Finset.univ → b ≠ fi → (if b ∈ some fi then 1 else 0) * M b j = 0
[PROOFSTEP]
simp (config := { contextual := true }) [h, eq_comm]
[GOAL]
case some.h₁
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Semiring α
f : l ≃. m
M : Matrix m n α
i : l
j : n
fi : m
h : ↑f i = some fi
⊢ ¬fi ∈ Finset.univ → (if fi ∈ some fi then 1 else 0) * M fi j = 0
[PROOFSTEP]
simp (config := { contextual := true }) [h, eq_comm]
[GOAL]
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
f : m ≃. n
⊢ toMatrix (PEquiv.symm f) = (toMatrix f)ᵀ
[PROOFSTEP]
ext
[GOAL]
case a.h
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
f : m ≃. n
i✝ : n
x✝ : m
⊢ toMatrix (PEquiv.symm f) i✝ x✝ = (toMatrix f)ᵀ i✝ x✝
[PROOFSTEP]
simp only [transpose, mem_iff_mem f, toMatrix_apply]
[GOAL]
case a.h
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
f : m ≃. n
i✝ : n
x✝ : m
⊢ (if i✝ ∈ ↑f x✝ then 1 else 0) = ↑of (fun x y => if x ∈ ↑f y then 1 else 0) i✝ x✝
[PROOFSTEP]
congr
[GOAL]
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
⊢ toMatrix (PEquiv.refl n) = 1
[PROOFSTEP]
ext
[GOAL]
case a.h
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
i✝ x✝ : n
⊢ toMatrix (PEquiv.refl n) i✝ x✝ = OfNat.ofNat 1 i✝ x✝
[PROOFSTEP]
simp [toMatrix_apply, one_apply]
[GOAL]
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
⊢ (M * toMatrix f) i j = Option.casesOn (↑(PEquiv.symm f) j) 0 fun fj => M i fj
[PROOFSTEP]
dsimp [toMatrix, Matrix.mul_apply]
[GOAL]
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
⊢ (Finset.sum Finset.univ fun j_1 => M i j_1 * if j ∈ ↑f j_1 then 1 else 0) =
    Option.rec 0 (fun val => M i val) (↑(PEquiv.symm f) j)
[PROOFSTEP]
cases' h : f.symm j with fj
[GOAL]
case none
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
h : ↑(PEquiv.symm f) j = none
⊢ (Finset.sum Finset.univ fun j_1 => M i j_1 * if j ∈ ↑f j_1 then 1 else 0) = Option.rec 0 (fun val => M i val) none
[PROOFSTEP]
simp [h, ← f.eq_some_iff]
[GOAL]
case some
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
fj : m
h : ↑(PEquiv.symm f) j = some fj
⊢ (Finset.sum Finset.univ fun j_1 => M i j_1 * if j ∈ ↑f j_1 then 1 else 0) =
    Option.rec 0 (fun val => M i val) (some fj)
[PROOFSTEP]
rw [Finset.sum_eq_single fj]
[GOAL]
case some
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
fj : m
h : ↑(PEquiv.symm f) j = some fj
⊢ (M i fj * if j ∈ ↑f fj then 1 else 0) = Option.rec 0 (fun val => M i val) (some fj)
[PROOFSTEP]
simp [h, ← f.eq_some_iff]
[GOAL]
case some.h₀
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
fj : m
h : ↑(PEquiv.symm f) j = some fj
⊢ ∀ (b : m), b ∈ Finset.univ → b ≠ fj → (M i b * if j ∈ ↑f b then 1 else 0) = 0
[PROOFSTEP]
rintro b - n
[GOAL]
case some.h₀
k : Type u_1
l : Type u_2
m : Type u_3
n✝ : Type u_4
α : Type v
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n✝
M : Matrix l m α
f : m ≃. n✝
i : l
j : n✝
fj : m
h : ↑(PEquiv.symm f) j = some fj
b : m
n : b ≠ fj
⊢ (M i b * if j ∈ ↑f b then 1 else 0) = 0
[PROOFSTEP]
simp [h, ← f.eq_some_iff, n.symm]
[GOAL]
case some.h₁
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
fj : m
h : ↑(PEquiv.symm f) j = some fj
⊢ ¬fj ∈ Finset.univ → (M i fj * if j ∈ ↑f fj then 1 else 0) = 0
[PROOFSTEP]
simp
[GOAL]
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Semiring α
f : m ≃ m
M : Matrix m n α
⊢ toMatrix (Equiv.toPEquiv f) * M = fun i => M (↑f i)
[PROOFSTEP]
ext i j
[GOAL]
case h.h
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Semiring α
f : m ≃ m
M : Matrix m n α
i : m
j : n
⊢ (toMatrix (Equiv.toPEquiv f) * M) i j = M (↑f i) j
[PROOFSTEP]
rw [mul_matrix_apply, Equiv.toPEquiv_apply]
[GOAL]
k : Type u_1
l : Type u_2
m✝ : Type u_3
n✝ : Type u_4
α✝ : Type v
m : Type u_5
n : Type u_6
α : Type u_7
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Semiring α
f : n ≃ n
M : Matrix m n α
i : m
j : n
⊢ (M * toMatrix (Equiv.toPEquiv f)) i j = submatrix M id (↑f.symm) i j
[PROOFSTEP]
rw [PEquiv.matrix_mul_apply, ← Equiv.toPEquiv_symm, Equiv.toPEquiv_apply, Matrix.submatrix_apply, id.def]
[GOAL]
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
f : l ≃. m
g : m ≃. n
⊢ toMatrix (PEquiv.trans f g) = toMatrix f * toMatrix g
[PROOFSTEP]
ext i j
[GOAL]
case a.h
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
f : l ≃. m
g : m ≃. n
i : l
j : n
⊢ toMatrix (PEquiv.trans f g) i j = (toMatrix f * toMatrix g) i j
[PROOFSTEP]
rw [mul_matrix_apply]
[GOAL]
case a.h
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
f : l ≃. m
g : m ≃. n
i : l
j : n
⊢ toMatrix (PEquiv.trans f g) i j = Option.casesOn (↑f i) 0 fun fi => toMatrix g fi j
[PROOFSTEP]
dsimp [toMatrix, PEquiv.trans]
[GOAL]
case a.h
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
f : l ≃. m
g : m ≃. n
i : l
j : n
⊢ (if j ∈ Option.bind (↑f i) ↑g then 1 else 0) = Option.rec 0 (fun val => if j ∈ ↑g val then 1 else 0) (↑f i)
[PROOFSTEP]
cases f i
[GOAL]
case a.h.none
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
f : l ≃. m
g : m ≃. n
i : l
j : n
⊢ (if j ∈ Option.bind none ↑g then 1 else 0) = Option.rec 0 (fun val => if j ∈ ↑g val then 1 else 0) none
[PROOFSTEP]
simp
[GOAL]
case a.h.some
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
f : l ≃. m
g : m ≃. n
i : l
j : n
val✝ : m
⊢ (if j ∈ Option.bind (some val✝) ↑g then 1 else 0) = Option.rec 0 (fun val => if j ∈ ↑g val then 1 else 0) (some val✝)
[PROOFSTEP]
simp
[GOAL]
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
⊢ Function.Injective toMatrix
[PROOFSTEP]
classical
intro f g
refine' not_imp_not.1 _
simp only [Matrix.ext_iff.symm, toMatrix_apply, PEquiv.ext_iff, not_forall, exists_imp]
intro i hi
use i
cases' hf : f i with fi
· cases' hg : g i with gi
  · rw [hf, hg] at hi 
    exact (hi rfl).elim
  · use gi
    simp
· use fi
  simp [hf.symm, Ne.symm hi]
[GOAL]
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
⊢ Function.Injective toMatrix
[PROOFSTEP]
intro f g
[GOAL]
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
⊢ toMatrix f = toMatrix g → f = g
[PROOFSTEP]
refine' not_imp_not.1 _
[GOAL]
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
⊢ ¬f = g → ¬toMatrix f = toMatrix g
[PROOFSTEP]
simp only [Matrix.ext_iff.symm, toMatrix_apply, PEquiv.ext_iff, not_forall, exists_imp]
[GOAL]
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
⊢ ∀ (x : m), ¬↑f x = ↑g x → ∃ x x_1, ¬(if x_1 ∈ ↑f x then 1 else 0) = if x_1 ∈ ↑g x then 1 else 0
[PROOFSTEP]
intro i hi
[GOAL]
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬↑f i = ↑g i
⊢ ∃ x x_1, ¬(if x_1 ∈ ↑f x then 1 else 0) = if x_1 ∈ ↑g x then 1 else 0
[PROOFSTEP]
use i
[GOAL]
case h
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬↑f i = ↑g i
⊢ ∃ x, ¬(if x ∈ ↑f i then 1 else 0) = if x ∈ ↑g i then 1 else 0
[PROOFSTEP]
cases' hf : f i with fi
[GOAL]
case h.none
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬↑f i = ↑g i
hf : ↑f i = none
⊢ ∃ x, ¬(if x ∈ none then 1 else 0) = if x ∈ ↑g i then 1 else 0
[PROOFSTEP]
cases' hg : g i with gi
[GOAL]
case h.none.none
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬↑f i = ↑g i
hf : ↑f i = none
hg : ↑g i = none
⊢ ∃ x, ¬(if x ∈ none then 1 else 0) = if x ∈ none then 1 else 0
[PROOFSTEP]
rw [hf, hg] at hi 
[GOAL]
case h.none.none
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬none = none
hf : ↑f i = none
hg : ↑g i = none
⊢ ∃ x, ¬(if x ∈ none then 1 else 0) = if x ∈ none then 1 else 0
[PROOFSTEP]
exact (hi rfl).elim
[GOAL]
case h.none.some
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬↑f i = ↑g i
hf : ↑f i = none
gi : n
hg : ↑g i = some gi
⊢ ∃ x, ¬(if x ∈ none then 1 else 0) = if x ∈ some gi then 1 else 0
[PROOFSTEP]
use gi
[GOAL]
case h
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬↑f i = ↑g i
hf : ↑f i = none
gi : n
hg : ↑g i = some gi
⊢ ¬(if gi ∈ none then 1 else 0) = if gi ∈ some gi then 1 else 0
[PROOFSTEP]
simp
[GOAL]
case h.some
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬↑f i = ↑g i
fi : n
hf : ↑f i = some fi
⊢ ∃ x, ¬(if x ∈ some fi then 1 else 0) = if x ∈ ↑g i then 1 else 0
[PROOFSTEP]
use fi
[GOAL]
case h
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝² : DecidableEq n
inst✝¹ : MonoidWithZero α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬↑f i = ↑g i
fi : n
hf : ↑f i = some fi
⊢ ¬(if fi ∈ some fi then 1 else 0) = if fi ∈ ↑g i then 1 else 0
[PROOFSTEP]
simp [hf.symm, Ne.symm hi]
[GOAL]
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j : n
⊢ toMatrix (Equiv.toPEquiv (Equiv.swap i j)) =
    1 - toMatrix (single i i) - toMatrix (single j j) + toMatrix (single i j) + toMatrix (single j i)
[PROOFSTEP]
ext
[GOAL]
case a.h
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
⊢ toMatrix (Equiv.toPEquiv (Equiv.swap i j)) i✝ x✝ =
    (1 - toMatrix (single i i) - toMatrix (single j j) + toMatrix (single i j) + toMatrix (single j i)) i✝ x✝
[PROOFSTEP]
dsimp [toMatrix, single, Equiv.swap_apply_def, Equiv.toPEquiv, one_apply]
[GOAL]
case a.h
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
⊢ (if x✝ ∈ some (if i✝ = i then j else if i✝ = j then i else i✝) then 1 else 0) =
    ((((if i✝ = x✝ then 1 else 0) - if x✝ ∈ if i✝ = i then some i else none then 1 else 0) -
          if x✝ ∈ if i✝ = j then some j else none then 1 else 0) +
        if x✝ ∈ if i✝ = i then some j else none then 1 else 0) +
      if x✝ ∈ if i✝ = j then some i else none then 1 else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁴ : i✝ = i
h✝³ : x✝ ∈ some j
h✝² : i✝ = x✝
h✝¹ : x✝ ∈ some i
h✝ : i✝ = j
⊢ 1 = 1 - 1 - 1 + 1 + 1
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : i✝ = i
h✝⁴ : x✝ ∈ some j
h✝³ : i✝ = x✝
h✝² : x✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : x✝ ∈ none
⊢ 1 = 1 - 1 - 1 + 1 + 1
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : i✝ = i
h✝⁴ : x✝ ∈ some j
h✝³ : i✝ = x✝
h✝² : x✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : ¬x✝ ∈ none
⊢ 1 = 1 - 1 - 0 + 1 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁴ : i✝ = i
h✝³ : x✝ ∈ some j
h✝² : i✝ = x✝
h✝¹ : ¬x✝ ∈ some i
h✝ : i✝ = j
⊢ 1 = 1 - 0 - 1 + 1 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : i✝ = i
h✝⁴ : x✝ ∈ some j
h✝³ : i✝ = x✝
h✝² : ¬x✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : x✝ ∈ none
⊢ 1 = 1 - 0 - 1 + 1 + 1
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : i✝ = i
h✝⁴ : x✝ ∈ some j
h✝³ : i✝ = x✝
h✝² : ¬x✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : ¬x✝ ∈ none
⊢ 1 = 1 - 0 - 0 + 1 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁴ : i✝ = i
h✝³ : x✝ ∈ some j
h✝² : ¬i✝ = x✝
h✝¹ : x✝ ∈ some i
h✝ : i✝ = j
⊢ 1 = 0 - 1 - 1 + 1 + 1
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : i✝ = i
h✝⁴ : x✝ ∈ some j
h✝³ : ¬i✝ = x✝
h✝² : x✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : x✝ ∈ none
⊢ 1 = 0 - 1 - 1 + 1 + 1
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : i✝ = i
h✝⁴ : x✝ ∈ some j
h✝³ : ¬i✝ = x✝
h✝² : x✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : ¬x✝ ∈ none
⊢ 1 = 0 - 1 - 0 + 1 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁴ : i✝ = i
h✝³ : x✝ ∈ some j
h✝² : ¬i✝ = x✝
h✝¹ : ¬x✝ ∈ some i
h✝ : i✝ = j
⊢ 1 = 0 - 0 - 1 + 1 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : i✝ = i
h✝⁴ : x✝ ∈ some j
h✝³ : ¬i✝ = x✝
h✝² : ¬x✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : x✝ ∈ none
⊢ 1 = 0 - 0 - 1 + 1 + 1
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : i✝ = i
h✝⁴ : x✝ ∈ some j
h✝³ : ¬i✝ = x✝
h✝² : ¬x✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : ¬x✝ ∈ none
⊢ 1 = 0 - 0 - 0 + 1 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁴ : i✝ = i
h✝³ : ¬x✝ ∈ some j
h✝² : i✝ = x✝
h✝¹ : x✝ ∈ some i
h✝ : i✝ = j
⊢ 0 = 1 - 1 - 0 + 0 + 1
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : i✝ = i
h✝⁴ : ¬x✝ ∈ some j
h✝³ : i✝ = x✝
h✝² : x✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : x✝ ∈ none
⊢ 0 = 1 - 1 - 1 + 0 + 1
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : i✝ = i
h✝⁴ : ¬x✝ ∈ some j
h✝³ : i✝ = x✝
h✝² : x✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : ¬x✝ ∈ none
⊢ 0 = 1 - 1 - 0 + 0 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁴ : i✝ = i
h✝³ : ¬x✝ ∈ some j
h✝² : i✝ = x✝
h✝¹ : ¬x✝ ∈ some i
h✝ : i✝ = j
⊢ 0 = 1 - 0 - 0 + 0 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : i✝ = i
h✝⁴ : ¬x✝ ∈ some j
h✝³ : i✝ = x✝
h✝² : ¬x✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : x✝ ∈ none
⊢ 0 = 1 - 0 - 1 + 0 + 1
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : i✝ = i
h✝⁴ : ¬x✝ ∈ some j
h✝³ : i✝ = x✝
h✝² : ¬x✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : ¬x✝ ∈ none
⊢ 0 = 1 - 0 - 0 + 0 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁴ : i✝ = i
h✝³ : ¬x✝ ∈ some j
h✝² : ¬i✝ = x✝
h✝¹ : x✝ ∈ some i
h✝ : i✝ = j
⊢ 0 = 0 - 1 - 0 + 0 + 1
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : i✝ = i
h✝⁴ : ¬x✝ ∈ some j
h✝³ : ¬i✝ = x✝
h✝² : x✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : x✝ ∈ none
⊢ 0 = 0 - 1 - 1 + 0 + 1
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : i✝ = i
h✝⁴ : ¬x✝ ∈ some j
h✝³ : ¬i✝ = x✝
h✝² : x✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : ¬x✝ ∈ none
⊢ 0 = 0 - 1 - 0 + 0 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁴ : i✝ = i
h✝³ : ¬x✝ ∈ some j
h✝² : ¬i✝ = x✝
h✝¹ : ¬x✝ ∈ some i
h✝ : i✝ = j
⊢ 0 = 0 - 0 - 0 + 0 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : i✝ = i
h✝⁴ : ¬x✝ ∈ some j
h✝³ : ¬i✝ = x✝
h✝² : ¬x✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : x✝ ∈ none
⊢ 0 = 0 - 0 - 1 + 0 + 1
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : i✝ = i
h✝⁴ : ¬x✝ ∈ some j
h✝³ : ¬i✝ = x✝
h✝² : ¬x✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : ¬x✝ ∈ none
⊢ 0 = 0 - 0 - 0 + 0 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : x✝ ∈ some i
h✝² : i✝ = x✝
h✝¹ : x✝ ∈ none
h✝ : x✝ ∈ some j
⊢ 1 = 1 - 1 - 1 + 1 + 1
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : x✝ ∈ some i
h✝² : i✝ = x✝
h✝¹ : x✝ ∈ none
h✝ : ¬x✝ ∈ some j
⊢ 1 = 1 - 1 - 0 + 1 + 1
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : x✝ ∈ some i
h✝² : i✝ = x✝
h✝¹ : ¬x✝ ∈ none
h✝ : x✝ ∈ some j
⊢ 1 = 1 - 0 - 1 + 0 + 1
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : x✝ ∈ some i
h✝² : i✝ = x✝
h✝¹ : ¬x✝ ∈ none
h✝ : ¬x✝ ∈ some j
⊢ 1 = 1 - 0 - 0 + 0 + 1
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : x✝ ∈ some i
h✝² : ¬i✝ = x✝
h✝¹ : x✝ ∈ none
h✝ : x✝ ∈ some j
⊢ 1 = 0 - 1 - 1 + 1 + 1
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : x✝ ∈ some i
h✝² : ¬i✝ = x✝
h✝¹ : x✝ ∈ none
h✝ : ¬x✝ ∈ some j
⊢ 1 = 0 - 1 - 0 + 1 + 1
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : x✝ ∈ some i
h✝² : ¬i✝ = x✝
h✝¹ : ¬x✝ ∈ none
h✝ : x✝ ∈ some j
⊢ 1 = 0 - 0 - 1 + 0 + 1
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : x✝ ∈ some i
h✝² : ¬i✝ = x✝
h✝¹ : ¬x✝ ∈ none
h✝ : ¬x✝ ∈ some j
⊢ 1 = 0 - 0 - 0 + 0 + 1
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : ¬x✝ ∈ some i
h✝² : i✝ = x✝
h✝¹ : x✝ ∈ none
h✝ : x✝ ∈ some j
⊢ 0 = 1 - 1 - 1 + 1 + 0
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : ¬x✝ ∈ some i
h✝² : i✝ = x✝
h✝¹ : x✝ ∈ none
h✝ : ¬x✝ ∈ some j
⊢ 0 = 1 - 1 - 0 + 1 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : ¬x✝ ∈ some i
h✝² : i✝ = x✝
h✝¹ : ¬x✝ ∈ none
h✝ : x✝ ∈ some j
⊢ 0 = 1 - 0 - 1 + 0 + 0
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : ¬x✝ ∈ some i
h✝² : i✝ = x✝
h✝¹ : ¬x✝ ∈ none
h✝ : ¬x✝ ∈ some j
⊢ 0 = 1 - 0 - 0 + 0 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : ¬x✝ ∈ some i
h✝² : ¬i✝ = x✝
h✝¹ : x✝ ∈ none
h✝ : x✝ ∈ some j
⊢ 0 = 0 - 1 - 1 + 1 + 0
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : ¬x✝ ∈ some i
h✝² : ¬i✝ = x✝
h✝¹ : x✝ ∈ none
h✝ : ¬x✝ ∈ some j
⊢ 0 = 0 - 1 - 0 + 1 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : ¬x✝ ∈ some i
h✝² : ¬i✝ = x✝
h✝¹ : ¬x✝ ∈ none
h✝ : x✝ ∈ some j
⊢ 0 = 0 - 0 - 1 + 0 + 0
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : ¬x✝ ∈ some i
h✝² : ¬i✝ = x✝
h✝¹ : ¬x✝ ∈ none
h✝ : ¬x✝ ∈ some j
⊢ 0 = 0 - 0 - 0 + 0 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁴ : ¬i✝ = i
h✝³ : ¬i✝ = j
h✝² : x✝ ∈ some i✝
h✝¹ : i✝ = x✝
h✝ : x✝ ∈ none
⊢ 1 = 1 - 1 - 1 + 1 + 1
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁴ : ¬i✝ = i
h✝³ : ¬i✝ = j
h✝² : x✝ ∈ some i✝
h✝¹ : i✝ = x✝
h✝ : ¬x✝ ∈ none
⊢ 1 = 1 - 0 - 0 + 0 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁴ : ¬i✝ = i
h✝³ : ¬i✝ = j
h✝² : x✝ ∈ some i✝
h✝¹ : ¬i✝ = x✝
h✝ : x✝ ∈ none
⊢ 1 = 0 - 1 - 1 + 1 + 1
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁴ : ¬i✝ = i
h✝³ : ¬i✝ = j
h✝² : x✝ ∈ some i✝
h✝¹ : ¬i✝ = x✝
h✝ : ¬x✝ ∈ none
⊢ 1 = 0 - 0 - 0 + 0 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁴ : ¬i✝ = i
h✝³ : ¬i✝ = j
h✝² : ¬x✝ ∈ some i✝
h✝¹ : i✝ = x✝
h✝ : x✝ ∈ none
⊢ 0 = 1 - 1 - 1 + 1 + 1
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁴ : ¬i✝ = i
h✝³ : ¬i✝ = j
h✝² : ¬x✝ ∈ some i✝
h✝¹ : i✝ = x✝
h✝ : ¬x✝ ∈ none
⊢ 0 = 1 - 0 - 0 + 0 + 0
[PROOFSTEP]
simp_all
[GOAL]
case pos
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁴ : ¬i✝ = i
h✝³ : ¬i✝ = j
h✝² : ¬x✝ ∈ some i✝
h✝¹ : ¬i✝ = x✝
h✝ : x✝ ∈ none
⊢ 0 = 0 - 1 - 1 + 1 + 1
[PROOFSTEP]
simp_all
[GOAL]
case neg
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Ring α
i j i✝ x✝ : n
h✝⁴ : ¬i✝ = i
h✝³ : ¬i✝ = j
h✝² : ¬x✝ ∈ some i✝
h✝¹ : ¬i✝ = x✝
h✝ : ¬x✝ ∈ none
⊢ 0 = 0 - 0 - 0 + 0 + 0
[PROOFSTEP]
simp_all
[GOAL]
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq k
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
a : m
b : n
c : k
⊢ toMatrix (single a b) * toMatrix (single b c) = toMatrix (single a c)
[PROOFSTEP]
rw [← toMatrix_trans, single_trans_single]
[GOAL]
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : DecidableEq k
inst✝¹ : DecidableEq m
inst✝ : Semiring α
b₁ b₂ : n
hb : b₁ ≠ b₂
a : m
c : k
⊢ toMatrix (single a b₁) * toMatrix (single b₂ c) = 0
[PROOFSTEP]
rw [← toMatrix_trans, single_trans_single_of_ne hb, toMatrix_bot]
[GOAL]
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type v
inst✝⁵ : Fintype n
inst✝⁴ : Fintype k
inst✝³ : DecidableEq n
inst✝² : DecidableEq k
inst✝¹ : DecidableEq m
inst✝ : Semiring α
a : m
b : n
c : k
M : Matrix k l α
⊢ toMatrix (single a b) * (toMatrix (single b c) * M) = toMatrix (single a c) * M
[PROOFSTEP]
rw [← Matrix.mul_assoc, single_mul_single]
