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

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
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
cases' n with n n
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
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
suffices a ^ (n : ℤ) ∈ s by exact this
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
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
rw [zpow_ofNat]
no goals
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
exact hs.toIsSubring.toIsSubmonoid.pow_mem h
no goals
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
exact this
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
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
rw [zpow_negSucc]
no goals
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
exact hs.inv_mem (hs.toIsSubring.toIsSubmonoid.pow_mem h)