α : Type u_1
β : Type ?u.94362
γ : Type ?u.94365
inst✝ : Union α
a b : Part α
hab : (a ∪ b).Dom
⊢ get (Part.bind a fun y => map (fun x => y ∪ x) b) (_ : (Part.bind a fun y => map (fun x => y ∪ x) b).Dom) =
    get a (_ : a.Dom) ∪ get b (_ : b.Dom)
α : Type u_1
β : Type ?u.94362
γ : Type ?u.94365
inst✝ : Union α
a b : Part α
hab : (a ∪ b).Dom
⊢ get (a ∪ b) hab = get a (_ : a.Dom) ∪ get b (_ : b.Dom)
simp [union_def]
no goals
α : Type u_1
β : Type ?u.94362
γ : Type ?u.94365
inst✝ : Union α
a b : Part α
hab : (a ∪ b).Dom
⊢ get (Part.bind a fun y => map (fun x => y ∪ x) b) (_ : (Part.bind a fun y => map (fun x => y ∪ x) b).Dom) =
    get a (_ : a.Dom) ∪ get b (_ : b.Dom)
aesop