F : Type u_1
inst✝ : Field F
S : Set F
src✝ : IsSubmonoid (closure S) := isSubmonoid
a b : F
ha : a ∈ closure S
hb : b ∈ closure S
⊢ a + b ∈ closure S
F : Type u_1
inst✝ : Field F
S : Set F
src✝ : IsSubmonoid (closure S) := isSubmonoid
⊢ ∀ {a b : F}, a ∈ closure S → b ∈ closure S → a + b ∈ closure S
intro a b ha hb
case intro.intro.intro.intro
F : Type u_1
inst✝ : Field F
S : Set F
src✝ : IsSubmonoid (closure S) := isSubmonoid
b : F
hb : b ∈ closure S
p : F
hp : p ∈ Ring.closure S
q : F
hq : q ∈ Ring.closure S
ha : p / q ∈ closure S
⊢ p / q + b ∈ closure S
F : Type u_1
inst✝ : Field F
S : Set F
src✝ : IsSubmonoid (closure S) := isSubmonoid
a b : F
ha : a ∈ closure S
hb : b ∈ closure S
⊢ a + b ∈ closure S
rcases id ha with ⟨p, hp, q, hq, rfl⟩
case intro.intro.intro.intro.intro.intro.intro.intro
F : Type u_1
inst✝ : Field F
S : Set F
src✝ : IsSubmonoid (closure S) := isSubmonoid
p : F
hp : p ∈ Ring.closure S
q : F
hq : q ∈ Ring.closure S
ha : p / q ∈ closure S
r : F
hr : r ∈ Ring.closure S
s : F
hs : s ∈ Ring.closure S
hb : r / s ∈ closure S
⊢ p / q + r / s ∈ closure S
case intro.intro.intro.intro
F : Type u_1
inst✝ : Field F
S : Set F
src✝ : IsSubmonoid (closure S) := isSubmonoid
b : F
hb : b ∈ closure S
p : F
hp : p ∈ Ring.closure S
q : F
hq : q ∈ Ring.closure S
ha : p / q ∈ closure S
⊢ p / q + b ∈ closure S
rcases id hb with ⟨r, hr, s, hs, rfl⟩
case pos
F : Type u_1
inst✝ : Field F
S : Set F
src✝ : IsSubmonoid (closure S) := isSubmonoid
p : F
hp : p ∈ Ring.closure S
q : F
hq : q ∈ Ring.closure S
ha : p / q ∈ closure S
r : F
hr : r ∈ Ring.closure S
s : F
hs : s ∈ Ring.closure S
hb : r / s ∈ closure S
hq0 : q = 0
⊢ p / q + r / s ∈ closure S

case neg
F : Type u_1
inst✝ : Field F
S : Set F
src✝ : IsSubmonoid (closure S) := isSubmonoid
p : F
hp : p ∈ Ring.closure S
q : F
hq : q ∈ Ring.closure S
ha : p / q ∈ closure S
r : F
hr : r ∈ Ring.closure S
s : F
hs : s ∈ Ring.closure S
hb : r / s ∈ closure S
hq0 : ¬q = 0
⊢ p / q + r / s ∈ closure S
case intro.intro.intro.intro.intro.intro.intro.intro
F : Type u_1
inst✝ : Field F
S : Set F
src✝ : IsSubmonoid (closure S) := isSubmonoid
p : F
hp : p ∈ Ring.closure S
q : F
hq : q ∈ Ring.closure S
ha : p / q ∈ closure S
r : F
hr : r ∈ Ring.closure S
s : F
hs : s ∈ Ring.closure S
hb : r / s ∈ closure S
⊢ p / q + r / s ∈ closure S
by_cases hq0 : q = 0
case pos
F : Type u_1
inst✝ : Field F
S : Set F
src✝ : IsSubmonoid (closure S) := isSubmonoid
p : F
hp : p ∈ Ring.closure S
q : F
hq : q ∈ Ring.closure S
ha : p / q ∈ closure S
r : F
hr : r ∈ Ring.closure S
s : F
hs : s ∈ Ring.closure S
hb : r / s ∈ closure S
hq0 : ¬q = 0
hs0 : s = 0
⊢ p / q + r / s ∈ closure S

case neg
F : Type u_1
inst✝ : Field F
S : Set F
src✝ : IsSubmonoid (closure S) := isSubmonoid
p : F
hp : p ∈ Ring.closure S
q : F
hq : q ∈ Ring.closure S
ha : p / q ∈ closure S
r : F
hr : r ∈ Ring.closure S
s : F
hs : s ∈ Ring.closure S
hb : r / s ∈ closure S
hq0 : ¬q = 0
hs0 : ¬s = 0
⊢ p / q + r / s ∈ closure S
case neg
F : Type u_1
inst✝ : Field F
S : Set F
src✝ : IsSubmonoid (closure S) := isSubmonoid
p : F
hp : p ∈ Ring.closure S
q : F
hq : q ∈ Ring.closure S
ha : p / q ∈ closure S
r : F
hr : r ∈ Ring.closure S
s : F
hs : s ∈ Ring.closure S
hb : r / s ∈ closure S
hq0 : ¬q = 0
⊢ p / q + r / s ∈ closure S
by_cases hs0 : s = 0
no goals
case neg
F : Type u_1
inst✝ : Field F
S : Set F
src✝ : IsSubmonoid (closure S) := isSubmonoid
p : F
hp : p ∈ Ring.closure S
q : F
hq : q ∈ Ring.closure S
ha : p / q ∈ closure S
r : F
hr : r ∈ Ring.closure S
s : F
hs : s ∈ Ring.closure S
hb : r / s ∈ closure S
hq0 : ¬q = 0
hs0 : ¬s = 0
⊢ p / q + r / s ∈ closure S
exact ⟨p * s + q * r,
  IsAddSubmonoid.add_mem Ring.closure.isSubring.toIsAddSubgroup.toIsAddSubmonoid
    (Ring.closure.isSubring.toIsSubmonoid.mul_mem hp hs)
    (Ring.closure.isSubring.toIsSubmonoid.mul_mem hq hr),
  q * s, Ring.closure.isSubring.toIsSubmonoid.mul_mem hq hs, (div_add_div p r hq0 hs0).symm⟩
no goals
case pos
F : Type u_1
inst✝ : Field F
S : Set F
src✝ : IsSubmonoid (closure S) := isSubmonoid
p : F
hp : p ∈ Ring.closure S
q : F
hq : q ∈ Ring.closure S
ha : p / q ∈ closure S
r : F
hr : r ∈ Ring.closure S
s : F
hs : s ∈ Ring.closure S
hb : r / s ∈ closure S
hq0 : q = 0
⊢ p / q + r / s ∈ closure S
rwa [hq0, div_zero, zero_add]
no goals
case pos
F : Type u_1
inst✝ : Field F
S : Set F
src✝ : IsSubmonoid (closure S) := isSubmonoid
p : F
hp : p ∈ Ring.closure S
q : F
hq : q ∈ Ring.closure S
ha : p / q ∈ closure S
r : F
hr : r ∈ Ring.closure S
s : F
hs : s ∈ Ring.closure S
hb : r / s ∈ closure S
hq0 : ¬q = 0
hs0 : s = 0
⊢ p / q + r / s ∈ closure S
rwa [hs0, div_zero, add_zero]
case intro.intro.intro.intro
F : Type u_1
inst✝ : Field F
S : Set F
src✝ : IsSubmonoid (closure S) := isSubmonoid
p : F
hp : p ∈ Ring.closure S
q : F
hq : q ∈ Ring.closure S
⊢ -(p / q) ∈ closure S
F : Type u_1
inst✝ : Field F
S : Set F
src✝ : IsSubmonoid (closure S) := isSubmonoid
⊢ ∀ {a : F}, a ∈ closure S → -a ∈ closure S
rintro _ ⟨p, hp, q, hq, rfl⟩
no goals
case intro.intro.intro.intro
F : Type u_1
inst✝ : Field F
S : Set F
src✝ : IsSubmonoid (closure S) := isSubmonoid
p : F
hp : p ∈ Ring.closure S
q : F
hq : q ∈ Ring.closure S
⊢ -(p / q) ∈ closure S
exact ⟨-p, Ring.closure.isSubring.toIsAddSubgroup.neg_mem hp, q, hq, neg_div q p⟩
case intro.intro.intro.intro
F : Type u_1
inst✝ : Field F
S : Set F
src✝ : IsSubmonoid (closure S) := isSubmonoid
p : F
hp : p ∈ Ring.closure S
q : F
hq : q ∈ Ring.closure S
⊢ (p / q)⁻¹ ∈ closure S
F : Type u_1
inst✝ : Field F
S : Set F
src✝ : IsSubmonoid (closure S) := isSubmonoid
⊢ ∀ {x : F}, x ∈ closure S → x⁻¹ ∈ closure S
rintro _ ⟨p, hp, q, hq, rfl⟩
no goals
case intro.intro.intro.intro
F : Type u_1
inst✝ : Field F
S : Set F
src✝ : IsSubmonoid (closure S) := isSubmonoid
p : F
hp : p ∈ Ring.closure S
q : F
hq : q ∈ Ring.closure S
⊢ (p / q)⁻¹ ∈ closure S
exact ⟨q, hq, p, hp, (inv_div _ _).symm⟩