[GOAL]
α : Type u_1
inst✝ : DecidableEq α
x y : α
⊢ optionCongr (swap x y) = swap (some x) (some y)
[PROOFSTEP]
ext (_ | i)
[GOAL]
case H.none.a
α : Type u_1
inst✝ : DecidableEq α
x y a✝ : α
⊢ a✝ ∈ ↑(optionCongr (swap x y)) none ↔ a✝ ∈ ↑(swap (some x) (some y)) none
[PROOFSTEP]
simp [swap_apply_of_ne_of_ne]
[GOAL]
case H.some.a
α : Type u_1
inst✝ : DecidableEq α
x y i a✝ : α
⊢ a✝ ∈ ↑(optionCongr (swap x y)) (some i) ↔ a✝ ∈ ↑(swap (some x) (some y)) (some i)
[PROOFSTEP]
by_cases hx : i = x
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
x y i a✝ : α
hx : i = x
⊢ a✝ ∈ ↑(optionCongr (swap x y)) (some i) ↔ a✝ ∈ ↑(swap (some x) (some y)) (some i)
case neg
α : Type u_1
inst✝ : DecidableEq α
x y i a✝ : α
hx : ¬i = x
⊢ a✝ ∈ ↑(optionCongr (swap x y)) (some i) ↔ a✝ ∈ ↑(swap (some x) (some y)) (some i)
[PROOFSTEP]
simp [hx, swap_apply_of_ne_of_ne]
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
x y i a✝ : α
hx : ¬i = x
⊢ a✝ ∈ ↑(optionCongr (swap x y)) (some i) ↔ a✝ ∈ ↑(swap (some x) (some y)) (some i)
[PROOFSTEP]
by_cases hy : i = y
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
x y i a✝ : α
hx : ¬i = x
hy : i = y
⊢ a✝ ∈ ↑(optionCongr (swap x y)) (some i) ↔ a✝ ∈ ↑(swap (some x) (some y)) (some i)
[PROOFSTEP]
simp [hx, hy, swap_apply_of_ne_of_ne]
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
x y i a✝ : α
hx : ¬i = x
hy : ¬i = y
⊢ a✝ ∈ ↑(optionCongr (swap x y)) (some i) ↔ a✝ ∈ ↑(swap (some x) (some y)) (some i)
[PROOFSTEP]
simp [hx, hy, swap_apply_of_ne_of_ne]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
e : Perm α
⊢ ↑Perm.sign (optionCongr e) = ↑Perm.sign e
[PROOFSTEP]
refine Perm.swap_induction_on e ?_ ?_
[GOAL]
case refine_1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
e : Perm α
⊢ ↑Perm.sign (optionCongr 1) = ↑Perm.sign 1
[PROOFSTEP]
simp [Perm.one_def]
[GOAL]
case refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
e : Perm α
⊢ ∀ (f : Perm α) (x y : α),
    x ≠ y →
      ↑Perm.sign (optionCongr f) = ↑Perm.sign f → ↑Perm.sign (optionCongr (swap x y * f)) = ↑Perm.sign (swap x y * f)
[PROOFSTEP]
intro f x y hne h
[GOAL]
case refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
e f : Perm α
x y : α
hne : x ≠ y
h : ↑Perm.sign (optionCongr f) = ↑Perm.sign f
⊢ ↑Perm.sign (optionCongr (swap x y * f)) = ↑Perm.sign (swap x y * f)
[PROOFSTEP]
simp [h, hne, Perm.mul_def, ← Equiv.optionCongr_trans]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
⊢ optionCongr (removeNone σ) = swap none (↑σ none) * σ
[PROOFSTEP]
ext1 x
[GOAL]
case H
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x : Option α
⊢ ↑(optionCongr (removeNone σ)) x = ↑(swap none (↑σ none) * σ) x
[PROOFSTEP]
have : Option.map (⇑(removeNone σ)) x = (swap none (σ none)) (σ x) :=
  by
  cases' x with x
  · simp
  · cases h : σ (some _)
    · simp [removeNone_none _ h]
    · have hn : σ (some x) ≠ none := by simp [h]
      have hσn : σ (some x) ≠ σ none := σ.injective.ne (by simp)
      simp [removeNone_some _ ⟨_, h⟩, ← h, swap_apply_of_ne_of_ne hn hσn]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x : Option α
⊢ Option.map (↑(removeNone σ)) x = ↑(swap none (↑σ none)) (↑σ x)
[PROOFSTEP]
cases' x with x
[GOAL]
case none
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
⊢ Option.map (↑(removeNone σ)) none = ↑(swap none (↑σ none)) (↑σ none)
[PROOFSTEP]
simp
[GOAL]
case some
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x : α
⊢ Option.map (↑(removeNone σ)) (some x) = ↑(swap none (↑σ none)) (↑σ (some x))
[PROOFSTEP]
cases h : σ (some _)
[GOAL]
case some.none
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x : α
h : ↑σ (some x) = none
⊢ Option.map (↑(removeNone σ)) (some x) = ↑(swap none (↑σ none)) none
[PROOFSTEP]
simp [removeNone_none _ h]
[GOAL]
case some.some
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x val✝ : α
h : ↑σ (some x) = some val✝
⊢ Option.map (↑(removeNone σ)) (some x) = ↑(swap none (↑σ none)) (some val✝)
[PROOFSTEP]
have hn : σ (some x) ≠ none := by simp [h]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x val✝ : α
h : ↑σ (some x) = some val✝
⊢ ↑σ (some x) ≠ none
[PROOFSTEP]
simp [h]
[GOAL]
case some.some
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x val✝ : α
h : ↑σ (some x) = some val✝
hn : ↑σ (some x) ≠ none
⊢ Option.map (↑(removeNone σ)) (some x) = ↑(swap none (↑σ none)) (some val✝)
[PROOFSTEP]
have hσn : σ (some x) ≠ σ none := σ.injective.ne (by simp)
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x val✝ : α
h : ↑σ (some x) = some val✝
hn : ↑σ (some x) ≠ none
⊢ some x ≠ none
[PROOFSTEP]
simp
[GOAL]
case some.some
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x val✝ : α
h : ↑σ (some x) = some val✝
hn : ↑σ (some x) ≠ none
hσn : ↑σ (some x) ≠ ↑σ none
⊢ Option.map (↑(removeNone σ)) (some x) = ↑(swap none (↑σ none)) (some val✝)
[PROOFSTEP]
simp [removeNone_some _ ⟨_, h⟩, ← h, swap_apply_of_ne_of_ne hn hσn]
[GOAL]
case H
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x : Option α
this : Option.map (↑(removeNone σ)) x = ↑(swap none (↑σ none)) (↑σ x)
⊢ ↑(optionCongr (removeNone σ)) x = ↑(swap none (↑σ none) * σ) x
[PROOFSTEP]
simpa using this
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
⊢ (fun i => swap none i.fst * optionCongr i.snd) ((fun σ => (↑σ none, removeNone σ)) σ) = σ
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
x✝ : Option α × Perm α
x : Option α
σ : Perm α
⊢ (fun σ => (↑σ none, removeNone σ)) ((fun i => swap none i.fst * optionCongr i.snd) (x, σ)) = (x, σ)
[PROOFSTEP]
have : removeNone (swap none x * σ.optionCongr) = σ := Equiv.optionCongr_injective (by simp [← mul_assoc])
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
x✝ : Option α × Perm α
x : Option α
σ : Perm α
⊢ optionCongr (removeNone (swap none x * optionCongr σ)) = optionCongr σ
[PROOFSTEP]
simp [← mul_assoc]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
x✝ : Option α × Perm α
x : Option α
σ : Perm α
this : removeNone (swap none x * optionCongr σ) = σ
⊢ (fun σ => (↑σ none, removeNone σ)) ((fun i => swap none i.fst * optionCongr i.snd) (x, σ)) = (x, σ)
[PROOFSTEP]
simp [← Perm.eq_inv_iff_eq, this]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
e : Perm α
i : Option α
⊢ ↑(↑decomposeOption.symm (none, e)) i = Option.map (↑e) i
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
e : Perm α
⊢ ↑sign (↑decomposeOption.symm (none, e)) = ↑sign e
[PROOFSTEP]
simp
