case none
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → isSome (↑f a₁) = true
x : α
hfx : ↑f x = none
⊢ (fun b => Option.recOn b a₂ fun b' => Option.recOn (↑(PEquiv.symm f) b') a₂ id) none = x

case some
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → isSome (↑f a₁) = true
x : α
val✝ : β
hfx : ↑f x = some val✝
⊢ (fun b => Option.recOn b a₂ fun b' => Option.recOn (↑(PEquiv.symm f) b') a₂ id) (some val✝) = x
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → isSome (↑f a₁) = true
x : α
⊢ (fun b => Option.recOn b a₂ fun b' => Option.recOn (↑(PEquiv.symm f) b') a₂ id) (↑f x) = x
cases hfx : f x
case none
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → isSome (↑f a₁) = true
x : α
hfx : ↑f x = none
this : x = a₂
⊢ (fun b => Option.recOn b a₂ fun b' => Option.recOn (↑(PEquiv.symm f) b') a₂ id) none = x
case none
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → isSome (↑f a₁) = true
x : α
hfx : ↑f x = none
⊢ (fun b => Option.recOn b a₂ fun b' => Option.recOn (↑(PEquiv.symm f) b') a₂ id) none = x
have : x = a₂ := not_imp_comm.1 (h x) (hfx.symm ▸ by simp)
no goals
case none
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → isSome (↑f a₁) = true
x : α
hfx : ↑f x = none
this : x = a₂
⊢ (fun b => Option.recOn b a₂ fun b' => Option.recOn (↑(PEquiv.symm f) b') a₂ id) none = x
simp [this]
no goals
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → isSome (↑f a₁) = true
x : α
hfx : ↑f x = none
⊢ ¬isSome none = true
simp
case some
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → isSome (↑f a₁) = true
x : α
val✝ : β
hfx : ↑f x = some val✝
⊢ Option.rec a₂ id (↑(PEquiv.symm f) val✝) = x
case some
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → isSome (↑f a₁) = true
x : α
val✝ : β
hfx : ↑f x = some val✝
⊢ (fun b => Option.recOn b a₂ fun b' => Option.recOn (↑(PEquiv.symm f) b') a₂ id) (some val✝) = x
dsimp only
case some
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → isSome (↑f a₁) = true
x : α
val✝ : β
hfx : ↑f x = some val✝
⊢ Option.rec a₂ id (some x) = x
case some
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → isSome (↑f a₁) = true
x : α
val✝ : β
hfx : ↑f x = some val✝
⊢ Option.rec a₂ id (↑(PEquiv.symm f) val✝) = x
rw [(eq_some_iff f).2 hfx]
no goals
case some
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → isSome (↑f a₁) = true
x : α
val✝ : β
hfx : ↑f x = some val✝
⊢ Option.rec a₂ id (some x) = x
rfl