case H
α : Type u_1
β : Type u_2
γ : Type ?u.20498
o : Part α
h : o.Dom
f : α → Part β
b : β
⊢ b ∈ Part.bind o f ↔ b ∈ f (get o h)
α : Type u_1
β : Type u_2
γ : Type ?u.20498
o : Part α
h : o.Dom
f : α → Part β
⊢ Part.bind o f = f (get o h)
ext b
case H
α : Type u_1
β : Type u_2
γ : Type ?u.20498
o : Part α
h : o.Dom
f : α → Part β
b : β
⊢ (∃ a, a ∈ o ∧ b ∈ f a) ↔ b ∈ f (get o h)
case H
α : Type u_1
β : Type u_2
γ : Type ?u.20498
o : Part α
h : o.Dom
f : α → Part β
b : β
⊢ b ∈ Part.bind o f ↔ b ∈ f (get o h)
simp only [Part.mem_bind_iff, exists_prop]
case H
α : Type u_1
β : Type u_2
γ : Type ?u.20498
o : Part α
h : o.Dom
f : α → Part β
b : β
⊢ (∃ a, a ∈ o ∧ b ∈ f a) → b ∈ f (get o h)
case H
α : Type u_1
β : Type u_2
γ : Type ?u.20498
o : Part α
h : o.Dom
f : α → Part β
b : β
⊢ (∃ a, a ∈ o ∧ b ∈ f a) ↔ b ∈ f (get o h)
refine' ⟨_, fun hb => ⟨o.get h, Part.get_mem _, hb⟩⟩
case H.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.20498
o : Part α
h : o.Dom
f : α → Part β
b : β
a : α
ha : a ∈ o
hb : b ∈ f a
⊢ b ∈ f (get o h)
case H
α : Type u_1
β : Type u_2
γ : Type ?u.20498
o : Part α
h : o.Dom
f : α → Part β
b : β
⊢ (∃ a, a ∈ o ∧ b ∈ f a) → b ∈ f (get o h)
rintro ⟨a, ha, hb⟩
no goals
case H.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.20498
o : Part α
h : o.Dom
f : α → Part β
b : β
a : α
ha : a ∈ o
hb : b ∈ f a
⊢ b ∈ f (get o h)
rwa [Part.get_eq_of_mem ha]