case none.none
α : Type u_1
β : Type u_2
γ : Type ?u.3190
e : Option α ≃ Option β
x : α
h1 : ↑e.symm (some (removeNone_aux e x)) = none
h2 : ↑e (some x) = none
⊢ some (removeNone_aux e.symm (removeNone_aux e x)) = some x

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

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

case some.some
α : Type u_1
β : Type u_2
γ : Type ?u.3190
e : Option α ≃ Option β
x val✝¹ : α
h1 : ↑e.symm (some (removeNone_aux e x)) = some val✝¹
val✝ : β
h2 : ↑e (some x) = some val✝
⊢ some (removeNone_aux e.symm (removeNone_aux e x)) = some x
α : Type u_1
β : Type u_2
γ : Type ?u.3190
e : Option α ≃ Option β
x : α
⊢ some (removeNone_aux e.symm (removeNone_aux e x)) = some x
cases h1 : e.symm (some (removeNone_aux e x)) <;> cases h2 : e (some x)
case none.none
α : Type u_1
β : Type u_2
γ : Type ?u.3190
e : Option α ≃ Option β
x : α
h1 : ↑e.symm (some (removeNone_aux e x)) = none
h2 : ↑e (some x) = none
⊢ ↑e.symm none = some x
case none.none
α : Type u_1
β : Type u_2
γ : Type ?u.3190
e : Option α ≃ Option β
x : α
h1 : ↑e.symm (some (removeNone_aux e x)) = none
h2 : ↑e (some x) = none
⊢ some (removeNone_aux e.symm (removeNone_aux e x)) = some x
rw [removeNone_aux_none _ h1]
no goals
case none.none
α : Type u_1
β : Type u_2
γ : Type ?u.3190
e : Option α ≃ Option β
x : α
h1 : ↑e.symm (some (removeNone_aux e x)) = none
h2 : ↑e (some x) = none
⊢ ↑e.symm none = some x
exact (e.eq_symm_apply.mpr h2).symm
case none.some
α : Type u_1
β : Type u_2
γ : Type ?u.3190
e : Option α ≃ Option β
x : α
h1 : ↑e.symm (↑e (some x)) = none
val✝ : β
h2 : ↑e (some x) = some val✝
⊢ some (removeNone_aux e.symm (removeNone_aux e x)) = some x
case none.some
α : Type u_1
β : Type u_2
γ : Type ?u.3190
e : Option α ≃ Option β
x : α
h1 : ↑e.symm (some (removeNone_aux e x)) = none
val✝ : β
h2 : ↑e (some x) = some val✝
⊢ some (removeNone_aux e.symm (removeNone_aux e x)) = some x
rw [removeNone_aux_some _ ⟨_, h2⟩] at h1
no goals
case none.some
α : Type u_1
β : Type u_2
γ : Type ?u.3190
e : Option α ≃ Option β
x : α
h1 : ↑e.symm (↑e (some x)) = none
val✝ : β
h2 : ↑e (some x) = some val✝
⊢ some (removeNone_aux e.symm (removeNone_aux e x)) = some x
simp at h1
case some.none
α : Type u_1
β : Type u_2
γ : Type ?u.3190
e : Option α ≃ Option β
x val✝ : α
h1 : ↑e.symm (↑e none) = some val✝
h2 : ↑e (some x) = none
⊢ some (removeNone_aux e.symm (removeNone_aux e x)) = some x
case some.none
α : Type u_1
β : Type u_2
γ : Type ?u.3190
e : Option α ≃ Option β
x val✝ : α
h1 : ↑e.symm (some (removeNone_aux e x)) = some val✝
h2 : ↑e (some x) = none
⊢ some (removeNone_aux e.symm (removeNone_aux e x)) = some x
rw [removeNone_aux_none _ h2] at h1
no goals
case some.none
α : Type u_1
β : Type u_2
γ : Type ?u.3190
e : Option α ≃ Option β
x val✝ : α
h1 : ↑e.symm (↑e none) = some val✝
h2 : ↑e (some x) = none
⊢ some (removeNone_aux e.symm (removeNone_aux e x)) = some x
simp at h1
case some.some
α : Type u_1
β : Type u_2
γ : Type ?u.3190
e : Option α ≃ Option β
x val✝¹ : α
h1 : ↑e.symm (some (removeNone_aux e x)) = some val✝¹
val✝ : β
h2 : ↑e (some x) = some val✝
⊢ ↑e.symm (some (removeNone_aux e x)) = some x
case some.some
α : Type u_1
β : Type u_2
γ : Type ?u.3190
e : Option α ≃ Option β
x val✝¹ : α
h1 : ↑e.symm (some (removeNone_aux e x)) = some val✝¹
val✝ : β
h2 : ↑e (some x) = some val✝
⊢ some (removeNone_aux e.symm (removeNone_aux e x)) = some x
rw [removeNone_aux_some _ ⟨_, h1⟩]
case some.some
α : Type u_1
β : Type u_2
γ : Type ?u.3190
e : Option α ≃ Option β
x val✝¹ : α
h1 : ↑e.symm (some (removeNone_aux e x)) = some val✝¹
val✝ : β
h2 : ↑e (some x) = some val✝
⊢ ↑e.symm (↑e (some x)) = some x
case some.some
α : Type u_1
β : Type u_2
γ : Type ?u.3190
e : Option α ≃ Option β
x val✝¹ : α
h1 : ↑e.symm (some (removeNone_aux e x)) = some val✝¹
val✝ : β
h2 : ↑e (some x) = some val✝
⊢ ↑e.symm (some (removeNone_aux e x)) = some x
rw [removeNone_aux_some _ ⟨_, h2⟩]
no goals
case some.some
α : Type u_1
β : Type u_2
γ : Type ?u.3190
e : Option α ≃ Option β
x val✝¹ : α
h1 : ↑e.symm (some (removeNone_aux e x)) = some val✝¹
val✝ : β
h2 : ↑e (some x) = some val✝
⊢ ↑e.symm (↑e (some x)) = some x
simp