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

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)
α : Type u_1
inst✝ : DecidableEq α
x y : α
⊢ optionCongr (swap x y) = swap (some x) (some y)
ext (_ | i)
no goals
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
simp [swap_apply_of_ne_of_ne]
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)
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)
by_cases hx : i = x
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)
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)
simp [hx, swap_apply_of_ne_of_ne]
no goals
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)
by_cases hy : i = y <;> simp [hx, hy, swap_apply_of_ne_of_ne]