α : Type u_1
β : Type ?u.56876
γ : Type ?u.56879
inst✝ : Mul α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ get (a * b)
      (_ : ∃ h, ((fun b_1 => (fun y => map y ((fun x => b) ())) (get ((fun x x_1 => x * x_1) <$> a) b_1)) h).Dom) =
    get a (_ : a.Dom) * get b (_ : b.Dom)
α : Type u_1
β : Type ?u.56876
γ : Type ?u.56879
inst✝ : Mul α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ get (a * b)
      (_ : ∃ h, ((fun b_1 => (fun y => map y ((fun x => b) ())) (get ((fun x x_1 => x * x_1) <$> a) b_1)) h).Dom) =
    ma * mb
simp [← ha.2, ← hb.2]
no goals
α : Type u_1
β : Type ?u.56876
γ : Type ?u.56879
inst✝ : Mul α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ get (a * b)
      (_ : ∃ h, ((fun b_1 => (fun y => map y ((fun x => b) ())) (get ((fun x x_1 => x * x_1) <$> a) b_1)) h).Dom) =
    get a (_ : a.Dom) * get b (_ : b.Dom)
rfl