case inl
α✝ : Type ?u.8538
β✝ : Type ?u.8541
γ : Type ?u.8544
α : Type u_1
β : Type u_2
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
h : a.Dom
⊢ Option.elim (toOption a) b f = f (get a h)

case inr
α✝ : Type ?u.8538
β✝ : Type ?u.8541
γ : Type ?u.8544
α : Type u_1
β : Type u_2
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
h : ¬a.Dom
⊢ Option.elim (toOption a) b f = b
α✝ : Type ?u.8538
β✝ : Type ?u.8541
γ : Type ?u.8544
α : Type u_1
β : Type u_2
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
⊢ Option.elim (toOption a) b f = if h : a.Dom then f (get a h) else b
split_ifs with h
case inl
α✝ : Type ?u.8538
β✝ : Type ?u.8541
γ : Type ?u.8544
α : Type u_1
β : Type u_2
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
h : a.Dom
⊢ Option.elim (Option.some (get a h)) b f = f (get a h)
case inl
α✝ : Type ?u.8538
β✝ : Type ?u.8541
γ : Type ?u.8544
α : Type u_1
β : Type u_2
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
h : a.Dom
⊢ Option.elim (toOption a) b f = f (get a h)
rw [h.toOption]
no goals
case inl
α✝ : Type ?u.8538
β✝ : Type ?u.8541
γ : Type ?u.8544
α : Type u_1
β : Type u_2
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
h : a.Dom
⊢ Option.elim (Option.some (get a h)) b f = f (get a h)
rfl
case inr
α✝ : Type ?u.8538
β✝ : Type ?u.8541
γ : Type ?u.8544
α : Type u_1
β : Type u_2
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
h : ¬a.Dom
⊢ Option.elim Option.none b f = b
case inr
α✝ : Type ?u.8538
β✝ : Type ?u.8541
γ : Type ?u.8544
α : Type u_1
β : Type u_2
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
h : ¬a.Dom
⊢ Option.elim (toOption a) b f = b
rw [Part.toOption_eq_none_iff.2 h]
no goals
case inr
α✝ : Type ?u.8538
β✝ : Type ?u.8541
γ : Type ?u.8544
α : Type u_1
β : Type u_2
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
h : ¬a.Dom
⊢ Option.elim Option.none b f = b
rfl