α : Type u_1
β : Type ?u.59915
γ : Type ?u.59918
inst✝ : Div α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1, a_1 ∈ a ∧ ∃ a, a ∈ b ∧ a_1 / a = ma / mb
α : Type u_1
β : Type ?u.59915
γ : Type ?u.59918
inst✝ : Div α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma / mb ∈ a / b
simp [div_def]
no goals
α : Type u_1
β : Type ?u.59915
γ : Type ?u.59918
inst✝ : Div α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1, a_1 ∈ a ∧ ∃ a, a ∈ b ∧ a_1 / a = ma / mb
aesop