case none
α : Type u_2
β : Type u_1
γ : Type ?u.6621
e : Option α ≃ Option β
x : α
h : ↑e (some x) = none
⊢ some (↑(removeNone e) x) = ↑e none ↔ ↑e.symm none = some x

case some
α : Type u_2
β : Type u_1
γ : Type ?u.6621
e : Option α ≃ Option β
x : α
a : β
h : ↑e (some x) = some a
⊢ some (↑(removeNone e) x) = ↑e none ↔ ↑e.symm none = some x
α : Type u_2
β : Type u_1
γ : Type ?u.6621
e : Option α ≃ Option β
x : α
⊢ some (↑(removeNone e) x) = ↑e none ↔ ↑e.symm none = some x
cases' h : e (some x) with a
case none
α : Type u_2
β : Type u_1
γ : Type ?u.6621
e : Option α ≃ Option β
x : α
h : ↑e (some x) = none
⊢ ↑e none = ↑e none ↔ ↑e.symm none = some x
case none
α : Type u_2
β : Type u_1
γ : Type ?u.6621
e : Option α ≃ Option β
x : α
h : ↑e (some x) = none
⊢ some (↑(removeNone e) x) = ↑e none ↔ ↑e.symm none = some x
rw [removeNone_none _ h]
no goals
case none
α : Type u_2
β : Type u_1
γ : Type ?u.6621
e : Option α ≃ Option β
x : α
h : ↑e (some x) = none
⊢ ↑e none = ↑e none ↔ ↑e.symm none = some x
simpa using (congr_arg e.symm h).symm
case some
α : Type u_2
β : Type u_1
γ : Type ?u.6621
e : Option α ≃ Option β
x : α
a : β
h : ↑e (some x) = some a
⊢ ↑e (some x) = ↑e none ↔ ↑e.symm none = some x
case some
α : Type u_2
β : Type u_1
γ : Type ?u.6621
e : Option α ≃ Option β
x : α
a : β
h : ↑e (some x) = some a
⊢ some (↑(removeNone e) x) = ↑e none ↔ ↑e.symm none = some x
rw [removeNone_some _ ⟨a, h⟩]
case some
α : Type u_2
β : Type u_1
γ : Type ?u.6621
e : Option α ≃ Option β
x : α
a : β
h : ↑e (some x) = some a
h1 : ↑e.symm (↑e (some x)) = ↑e.symm (some a)
⊢ ↑e (some x) = ↑e none ↔ ↑e.symm none = some x
case some
α : Type u_2
β : Type u_1
γ : Type ?u.6621
e : Option α ≃ Option β
x : α
a : β
h : ↑e (some x) = some a
⊢ ↑e (some x) = ↑e none ↔ ↑e.symm none = some x
have h1 := congr_arg e.symm h
case some
α : Type u_2
β : Type u_1
γ : Type ?u.6621
e : Option α ≃ Option β
x : α
a : β
h : ↑e (some x) = some a
h1 : some x = ↑e.symm (some a)
⊢ ↑e (some x) = ↑e none ↔ ↑e.symm none = some x
case some
α : Type u_2
β : Type u_1
γ : Type ?u.6621
e : Option α ≃ Option β
x : α
a : β
h : ↑e (some x) = some a
h1 : ↑e.symm (↑e (some x)) = ↑e.symm (some a)
⊢ ↑e (some x) = ↑e none ↔ ↑e.symm none = some x
rw [symm_apply_apply] at h1
case some
α : Type u_2
β : Type u_1
γ : Type ?u.6621
e : Option α ≃ Option β
x : α
a : β
h : ↑e (some x) = some a
h1 : some x = ↑e.symm (some a)
⊢ ¬↑e.symm none = some x
case some
α : Type u_2
β : Type u_1
γ : Type ?u.6621
e : Option α ≃ Option β
x : α
a : β
h : ↑e (some x) = some a
h1 : some x = ↑e.symm (some a)
⊢ ↑e (some x) = ↑e none ↔ ↑e.symm none = some x
simp only [false_iff_iff, apply_eq_iff_eq]
no goals
case some
α : Type u_2
β : Type u_1
γ : Type ?u.6621
e : Option α ≃ Option β
x : α
a : β
h : ↑e (some x) = some a
h1 : some x = ↑e.symm (some a)
⊢ ¬↑e.symm none = some x
simp [h1, apply_eq_iff_eq]