-- Mathlib/GroupTheory/Perm/Option.lean
theorem map_equiv_removeNone {α : Type*} [DecidableEq α] (σ : Perm (Option α)) :
    (removeNone σ).optionCongr = swap none (σ none) * σ

Proof state:
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x : Option α
⊢ Option.map (⇑(removeNone σ)) x = (swap none (σ none)) (σ x)

Tactic:
obtain - | x := x

Result:
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))

Proof state:
case H
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x : Option α
this : Option.map (⇑(removeNone σ)) x = (swap none (σ none)) (σ x)
⊢ (removeNone σ).optionCongr x = (swap none (σ none) * σ) x

Tactic:
simpa using this

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x val✝ : α
h : σ (some x) = some val✝
⊢ σ (some x) ≠ none

Tactic:
simp [h]

Result:
no goals

Proof state:
case some.none
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x : α
h : σ (some x) = none
⊢ Option.map (⇑(removeNone σ)) (some x) = (swap none (σ none)) none

Tactic:
simp [removeNone_none _ h]

Result:
no goals

Proof state:
case none
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
⊢ Option.map (⇑(removeNone σ)) none = (swap none (σ none)) (σ none)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
⊢ (removeNone σ).optionCongr = swap none (σ none) * σ

Tactic:
ext1 x

Result:
case H
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x : Option α
⊢ (removeNone σ).optionCongr x = (swap none (σ none) * σ) x

Proof state:
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✝)

Tactic:
simp [removeNone_some _ ⟨_, h⟩, ← h, swap_apply_of_ne_of_ne hn hσn]

Result:
no goals

Proof state:
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✝)

Tactic:
have hσn : σ (some x) ≠ σ none := σ.injective.ne (by simp)

Result:
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✝)

Proof state:
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✝)

Tactic:
have hn : σ (some x) ≠ none := by simp [h]

Result:
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✝)

Proof state:
case some
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x : α
⊢ Option.map (⇑(removeNone σ)) (some x) = (swap none (σ none)) (σ (some x))

Tactic:
cases h : σ (some _)

Result:
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✝)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x val✝ : α
h : σ (some x) = some val✝
hn : σ (some x) ≠ none
⊢ some x ≠ none

Tactic:
simp

Result:
no goals