K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
s : Set K
x : K
⊢ x ∈ (closure s).toSubring.toSubsemiring.toSubmonoid.toSubsemigroup.carrier ↔
    ∃ y, y ∈ Subring.closure s ∧ ∃ z, z ∈ Subring.closure s ∧ y / z = x
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
s : Set K
x : K
⊢ x ∈ closure s ↔ ∃ y, y ∈ Subring.closure s ∧ ∃ z, z ∈ Subring.closure s ∧ y / z = x
change x ∈ (closure s).carrier ↔ ∃ y ∈ Subring.closure s, ∃ z ∈ Subring.closure s, y / z = x
no goals
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
s : Set K
x : K
⊢ x ∈ (closure s).toSubring.toSubsemiring.toSubmonoid.toSubsemigroup.carrier ↔
    ∃ y, y ∈ Subring.closure s ∧ ∃ z, z ∈ Subring.closure s ∧ y / z = x
simp only [closure, exists_prop, Set.mem_setOf_eq]