case intro.intro.intro.intro.refl.intro.intro.intro.intro.refl
F : Type u_1
inst✝ : Field F
S : Set F
p : F
hp : p ∈ Ring.closure S
q : F
hq : q ∈ Ring.closure S
r : F
hr : r ∈ Ring.closure S
s : F
hs : s ∈ Ring.closure S
⊢ p / q * (r / s) ∈ closure S
F : Type u_1
inst✝ : Field F
S : Set F
⊢ ∀ {a b : F}, a ∈ closure S → b ∈ closure S → a * b ∈ closure S
rintro _ _ ⟨p, hp, q, hq, hq0, rfl⟩ ⟨r, hr, s, hs, hs0, rfl⟩
no goals
case intro.intro.intro.intro.refl.intro.intro.intro.intro.refl
F : Type u_1
inst✝ : Field F
S : Set F
p : F
hp : p ∈ Ring.closure S
q : F
hq : q ∈ Ring.closure S
r : F
hr : r ∈ Ring.closure S
s : F
hs : s ∈ Ring.closure S
⊢ p / q * (r / s) ∈ closure S
exact ⟨p * r, IsSubmonoid.mul_mem Ring.closure.isSubring.toIsSubmonoid hp hr, q * s,
  IsSubmonoid.mul_mem Ring.closure.isSubring.toIsSubmonoid hq hs,
  (div_mul_div_comm _ _ _ _).symm⟩