case H
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x : Option α
⊢ ↑(optionCongr (removeNone σ)) x = ↑(swap none (↑σ none) * σ) x
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
⊢ optionCongr (removeNone σ) = swap none (↑σ none) * σ
ext1 x
no goals
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
simpa using this
case none
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
⊢ Option.map (↑(removeNone σ)) none = ↑(swap none (↑σ none)) (↑σ none)

case some
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x : α
⊢ Option.map (↑(removeNone σ)) (some x) = ↑(swap none (↑σ none)) (↑σ (some x))
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x : Option α
⊢ Option.map (↑(removeNone σ)) x = ↑(swap none (↑σ none)) (↑σ x)
cases' x with x
no goals
case none
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
⊢ Option.map (↑(removeNone σ)) none = ↑(swap none (↑σ none)) (↑σ none)
simp
case some.none
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x : α
h : ↑σ (some x) = none
⊢ Option.map (↑(removeNone σ)) (some x) = ↑(swap none (↑σ none)) none

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✝)
case some
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x : α
⊢ Option.map (↑(removeNone σ)) (some x) = ↑(swap none (↑σ none)) (↑σ (some x))
cases h : σ (some _)
no goals
case some.none
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x : α
h : ↑σ (some x) = none
⊢ Option.map (↑(removeNone σ)) (some x) = ↑(swap none (↑σ none)) none
simp [removeNone_none _ h]
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✝)
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✝)
have hn : σ (some x) ≠ none := by simp [h]
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✝)
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✝)
have hσn : σ (some x) ≠ σ none := σ.injective.ne (by simp)
no goals
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✝)
simp [removeNone_some _ ⟨_, h⟩, ← h, swap_apply_of_ne_of_ne hn hσn]
no goals
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x val✝ : α
h : ↑σ (some x) = some val✝
⊢ ↑σ (some x) ≠ none
simp [h]
no goals
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x val✝ : α
h : ↑σ (some x) = some val✝
hn : ↑σ (some x) ≠ none
⊢ some x ≠ none
simp