-- Mathlib/Logic/Equiv/Option.lean
theorem removeNone_aux_inv (x : α) : removeNone_aux e.symm (removeNone_aux e x) = x :=
  Option.some_injective _
    (by
      cases h1 : e.symm (some (removeNone_aux e x)) <;> cases h2 : e (some x)
      · rw [removeNone_aux_none _ h1]
        exact (e.eq_symm_apply.mpr h2).symm

      · rw [removeNone_aux_some _ ⟨_, h2⟩] at h1
        simp at h1

      · rw [removeNone_aux_none _ h2] at h1
        simp at h1

      · rw [removeNone_aux_some _ ⟨_, h1⟩]
        rw [removeNone_aux_some _ ⟨_, h2⟩]
        simp)

Proof state:
case some.some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x val✝¹ : α
h1 : e.symm (some (e.removeNone_aux x)) = some val✝¹
val✝ : β
h2 : e (some x) = some val✝
⊢ some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x

Tactic:
rw [removeNone_aux_some _ ⟨_, h1⟩]

Result:
case some.some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x val✝¹ : α
h1 : e.symm (some (e.removeNone_aux x)) = some val✝¹
val✝ : β
h2 : e (some x) = some val✝
⊢ e.symm (some (e.removeNone_aux x)) = some x

Proof state:
case some.some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x val✝¹ : α
h1 : e.symm (some (e.removeNone_aux x)) = some val✝¹
val✝ : β
h2 : e (some x) = some val✝
⊢ e.symm (some (e.removeNone_aux x)) = some x

Tactic:
rw [removeNone_aux_some _ ⟨_, h2⟩]

Result:
case some.some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x val✝¹ : α
h1 : e.symm (some (e.removeNone_aux x)) = some val✝¹
val✝ : β
h2 : e (some x) = some val✝
⊢ e.symm (e (some x)) = some x

Proof state:
case some.some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x val✝¹ : α
h1 : e.symm (some (e.removeNone_aux x)) = some val✝¹
val✝ : β
h2 : e (some x) = some val✝
⊢ e.symm (e (some x)) = some x

Tactic:
simp

Result:
no goals

Proof state:
case none.some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h1 : e.symm (e (some x)) = none
val✝ : β
h2 : e (some x) = some val✝
⊢ some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x

Tactic:
simp at h1

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
⊢ some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x

Tactic:
cases h1 : e.symm (some (removeNone_aux e x)) <;> cases h2 : e (some x)

Result:
case none.none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h1 : e.symm (some (e.removeNone_aux x)) = none
h2 : e (some x) = none
⊢ some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x

case none.some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h1 : e.symm (some (e.removeNone_aux x)) = none
val✝ : β
h2 : e (some x) = some val✝
⊢ some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x

case some.none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x val✝ : α
h1 : e.symm (some (e.removeNone_aux x)) = some val✝
h2 : e (some x) = none
⊢ some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x

case some.some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x val✝¹ : α
h1 : e.symm (some (e.removeNone_aux x)) = some val✝¹
val✝ : β
h2 : e (some x) = some val✝
⊢ some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x

Proof state:
case none.some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h1 : e.symm (some (e.removeNone_aux x)) = none
val✝ : β
h2 : e (some x) = some val✝
⊢ some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x

Tactic:
rw [removeNone_aux_some _ ⟨_, h2⟩] at h1

Result:
case none.some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h1 : e.symm (e (some x)) = none
val✝ : β
h2 : e (some x) = some val✝
⊢ some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x

Proof state:
case some.none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x val✝ : α
h1 : e.symm (e none) = some val✝
h2 : e (some x) = none
⊢ some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x

Tactic:
simp at h1

Result:
no goals

Proof state:
case some.none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x val✝ : α
h1 : e.symm (some (e.removeNone_aux x)) = some val✝
h2 : e (some x) = none
⊢ some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x

Tactic:
rw [removeNone_aux_none _ h2] at h1

Result:
case some.none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x val✝ : α
h1 : e.symm (e none) = some val✝
h2 : e (some x) = none
⊢ some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x

Proof state:
case none.none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h1 : e.symm (some (e.removeNone_aux x)) = none
h2 : e (some x) = none
⊢ e.symm none = some x

Tactic:
exact (e.eq_symm_apply.mpr h2).symm

Result:
no goals

Proof state:
case none.none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h1 : e.symm (some (e.removeNone_aux x)) = none
h2 : e (some x) = none
⊢ some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x

Tactic:
rw [removeNone_aux_none _ h1]

Result:
case none.none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h1 : e.symm (some (e.removeNone_aux x)) = none
h2 : e (some x) = none
⊢ e.symm none = some x