case a.h
k : Type ?u.26647
l : Type ?u.26650
m : Type ?u.26653
n : Type u_1
α : 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✝
k : Type ?u.26647
l : Type ?u.26650
m : Type ?u.26653
n : Type u_1
α : 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)
ext
case a.h
k : Type ?u.26647
l : Type ?u.26650
m : Type ?u.26653
n : Type u_1
α : 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
case a.h
k : Type ?u.26647
l : Type ?u.26650
m : Type ?u.26653
n : Type u_1
α : 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✝
dsimp [toMatrix, single, Equiv.swap_apply_def, Equiv.toPEquiv, one_apply]
no goals
case a.h
k : Type ?u.26647
l : Type ?u.26650
m : Type ?u.26653
n : Type u_1
α : 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
split_ifs <;> simp_all