case pos
α : Type u_2
β : Type u_1
γ : Type ?u.25409
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (Part.bind o f).Dom
h : o.Dom
⊢ toOption (Part.bind o f) = Option.elim (toOption o) Option.none fun a => toOption (f a)

case neg
α : Type u_2
β : Type u_1
γ : Type ?u.25409
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (Part.bind o f).Dom
h : ¬o.Dom
⊢ toOption (Part.bind o f) = Option.elim (toOption o) Option.none fun a => toOption (f a)
α : Type u_2
β : Type u_1
γ : Type ?u.25409
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (Part.bind o f).Dom
⊢ toOption (Part.bind o f) = Option.elim (toOption o) Option.none fun a => toOption (f a)
by_cases h : o.Dom
case pos
α : Type u_2
β : Type u_1
γ : Type ?u.25409
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (Part.bind o f).Dom
h : o.Dom
⊢ toOption (f (get o h)) = Option.elim (Option.some (get o h)) Option.none fun a => toOption (f a)
case pos
α : Type u_2
β : Type u_1
γ : Type ?u.25409
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (Part.bind o f).Dom
h : o.Dom
⊢ toOption (Part.bind o f) = Option.elim (toOption o) Option.none fun a => toOption (f a)
simp_rw [h.toOption, h.bind]
no goals
case pos
α : Type u_2
β : Type u_1
γ : Type ?u.25409
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (Part.bind o f).Dom
h : o.Dom
⊢ toOption (f (get o h)) = Option.elim (Option.some (get o h)) Option.none fun a => toOption (f a)
rfl
case neg
α : Type u_2
β : Type u_1
γ : Type ?u.25409
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (Part.bind o f).Dom
h : ¬o.Dom
⊢ toOption (Part.bind o f) = Option.elim Option.none Option.none fun a => toOption (f a)
case neg
α : Type u_2
β : Type u_1
γ : Type ?u.25409
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (Part.bind o f).Dom
h : ¬o.Dom
⊢ toOption (Part.bind o f) = Option.elim (toOption o) Option.none fun a => toOption (f a)
rw [Part.toOption_eq_none_iff.2 h]
no goals
case neg
α : Type u_2
β : Type u_1
γ : Type ?u.25409
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (Part.bind o f).Dom
h : ¬o.Dom
⊢ toOption (Part.bind o f) = Option.elim Option.none Option.none fun a => toOption (f a)
exact Part.toOption_eq_none_iff.2 fun ho => h ho.of_bind