[GOAL]
F : Type u_1
inst✝ : Field F
S✝ S : Set F
hS : IsSubfield S
x y : F
hx : x ∈ S
hy : y ∈ S
⊢ x / y ∈ S
[PROOFSTEP]
rw [div_eq_mul_inv]
[GOAL]
F : Type u_1
inst✝ : Field F
S✝ S : Set F
hS : IsSubfield S
x y : F
hx : x ∈ S
hy : y ∈ S
⊢ x * y⁻¹ ∈ S
[PROOFSTEP]
exact hS.toIsSubring.toIsSubmonoid.mul_mem hx (hS.inv_mem hy)
[GOAL]
F : Type u_1
inst✝ : Field F
S : Set F
a : F
n : ℤ
s : Set F
hs : IsSubfield s
h : a ∈ s
⊢ a ^ n ∈ s
[PROOFSTEP]
cases' n with n n
[GOAL]
case ofNat
F : Type u_1
inst✝ : Field F
S : Set F
a : F
s : Set F
hs : IsSubfield s
h : a ∈ s
n : ℕ
⊢ a ^ Int.ofNat n ∈ s
[PROOFSTEP]
suffices a ^ (n : ℤ) ∈ s by exact this
[GOAL]
F : Type u_1
inst✝ : Field F
S : Set F
a : F
s : Set F
hs : IsSubfield s
h : a ∈ s
n : ℕ
this : a ^ ↑n ∈ s
⊢ a ^ Int.ofNat n ∈ s
[PROOFSTEP]
exact this
[GOAL]
case ofNat
F : Type u_1
inst✝ : Field F
S : Set F
a : F
s : Set F
hs : IsSubfield s
h : a ∈ s
n : ℕ
⊢ a ^ ↑n ∈ s
[PROOFSTEP]
rw [zpow_ofNat]
[GOAL]
case ofNat
F : Type u_1
inst✝ : Field F
S : Set F
a : F
s : Set F
hs : IsSubfield s
h : a ∈ s
n : ℕ
⊢ a ^ n ∈ s
[PROOFSTEP]
exact hs.toIsSubring.toIsSubmonoid.pow_mem h
[GOAL]
case negSucc
F : Type u_1
inst✝ : Field F
S : Set F
a : F
s : Set F
hs : IsSubfield s
h : a ∈ s
n : ℕ
⊢ a ^ Int.negSucc n ∈ s
[PROOFSTEP]
rw [zpow_negSucc]
[GOAL]
case negSucc
F : Type u_1
inst✝ : Field F
S : Set F
a : F
s : Set F
hs : IsSubfield s
h : a ∈ s
n : ℕ
⊢ (a ^ (n + 1))⁻¹ ∈ s
[PROOFSTEP]
exact hs.inv_mem (hs.toIsSubring.toIsSubmonoid.pow_mem h)
[GOAL]
F : Type u_1
inst✝¹ : Field F
S : Set F
K : Type u_2
inst✝ : Field K
f : F →+* K
s : Set K
hs : IsSubfield s
src✝ : IsSubring (↑f ⁻¹' s) := RingHom.isSubring_preimage f hs.toIsSubring
a : F
ha : ↑f a ∈ s
⊢ ↑f a⁻¹ ∈ s
[PROOFSTEP]
rw [map_inv₀]
[GOAL]
F : Type u_1
inst✝¹ : Field F
S : Set F
K : Type u_2
inst✝ : Field K
f : F →+* K
s : Set K
hs : IsSubfield s
src✝ : IsSubring (↑f ⁻¹' s) := RingHom.isSubring_preimage f hs.toIsSubring
a : F
ha : ↑f a ∈ s
⊢ (↑f a)⁻¹ ∈ s
[PROOFSTEP]
exact hs.inv_mem ha
[GOAL]
F : Type u_1
inst✝¹ : Field F
S : Set F
K : Type u_2
inst✝ : Field K
f : F →+* K
⊢ IsSubfield (Set.range ↑f)
[PROOFSTEP]
rw [← Set.image_univ]
[GOAL]
F : Type u_1
inst✝¹ : Field F
S : Set F
K : Type u_2
inst✝ : Field K
f : F →+* K
⊢ IsSubfield (↑f '' Set.univ)
[PROOFSTEP]
apply Image.isSubfield _ Univ.isSubfield
[GOAL]
F : Type u_1
inst✝ : Field F
S : Set F
⊢ ∀ {a b : F}, a ∈ closure S → b ∈ closure S → a * b ∈ closure S
[PROOFSTEP]
rintro _ _ ⟨p, hp, q, hq, hq0, rfl⟩ ⟨r, hr, s, hs, hs0, rfl⟩
[GOAL]
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
[PROOFSTEP]
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⟩
[GOAL]
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
[PROOFSTEP]
intro a b ha hb
[GOAL]
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
[PROOFSTEP]
rcases id ha with ⟨p, hp, q, hq, rfl⟩
[GOAL]
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
[PROOFSTEP]
rcases id hb with ⟨r, hr, s, hs, rfl⟩
[GOAL]
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
[PROOFSTEP]
by_cases hq0 : q = 0
[GOAL]
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
[PROOFSTEP]
rwa [hq0, div_zero, zero_add]
[GOAL]
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
[PROOFSTEP]
by_cases hs0 : s = 0
[GOAL]
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
[PROOFSTEP]
rwa [hs0, div_zero, add_zero]
[GOAL]
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
[PROOFSTEP]
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⟩
[GOAL]
F : Type u_1
inst✝ : Field F
S : Set F
src✝ : IsSubmonoid (closure S) := isSubmonoid
⊢ ∀ {a : F}, a ∈ closure S → -a ∈ closure S
[PROOFSTEP]
rintro _ ⟨p, hp, q, hq, rfl⟩
[GOAL]
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
[PROOFSTEP]
exact ⟨-p, Ring.closure.isSubring.toIsAddSubgroup.neg_mem hp, q, hq, neg_div q p⟩
[GOAL]
F : Type u_1
inst✝ : Field F
S : Set F
src✝ : IsSubmonoid (closure S) := isSubmonoid
⊢ ∀ {x : F}, x ∈ closure S → x⁻¹ ∈ closure S
[PROOFSTEP]
rintro _ ⟨p, hp, q, hq, rfl⟩
[GOAL]
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
[PROOFSTEP]
exact ⟨q, hq, p, hp, (inv_div _ _).symm⟩
[GOAL]
F : Type u_1
inst✝ : Field F
S T : Set F
hT : IsSubfield T
H : S ⊆ T
⊢ closure S ⊆ T
[PROOFSTEP]
rintro _ ⟨p, hp, q, hq, hq0, rfl⟩
[GOAL]
case intro.intro.intro.intro.refl
F : Type u_1
inst✝ : Field F
S T : Set F
hT : IsSubfield T
H : S ⊆ T
p : F
hp : p ∈ Ring.closure S
q : F
hq : q ∈ Ring.closure S
⊢ p / q ∈ T
[PROOFSTEP]
exact hT.div_mem (Ring.closure_subset hT.toIsSubring H hp) (Ring.closure_subset hT.toIsSubring H hq)
