case mp
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Saturated H → ∀ (n : ℤ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H

case mpr
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∀ (n : ℤ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H) → Saturated H
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Saturated H ↔ ∀ (n : ℤ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H
constructor
case mp
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : Saturated H
n : ℤ
g : G
hgn : g ^ n ∈ H
⊢ n = 0 ∨ g ∈ H
case mp
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Saturated H → ∀ (n : ℤ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H
intros hH n g hgn
case mp.ofNat
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : Saturated H
n✝ : ℤ
g : G
hgn✝ : g ^ n✝ ∈ H
n : ℕ
hgn : g ^ Int.ofNat n ∈ H
⊢ Int.ofNat n = 0 ∨ g ∈ H

case mp.negSucc
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : Saturated H
n✝ : ℤ
g : G
hgn✝ : g ^ n✝ ∈ H
n : ℕ
hgn : g ^ Int.negSucc n ∈ H
⊢ Int.negSucc n = 0 ∨ g ∈ H
case mp
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : Saturated H
n : ℤ
g : G
hgn : g ^ n ∈ H
⊢ n = 0 ∨ g ∈ H
induction' n with n n
case mp.ofNat
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : Saturated H
n✝ : ℤ
g : G
hgn✝ : g ^ n✝ ∈ H
n : ℕ
hgn : g ^ n ∈ H
⊢ n = 0 ∨ g ∈ H
case mp.ofNat
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : Saturated H
n✝ : ℤ
g : G
hgn✝ : g ^ n✝ ∈ H
n : ℕ
hgn : g ^ Int.ofNat n ∈ H
⊢ Int.ofNat n = 0 ∨ g ∈ H
simp only [Int.coe_nat_eq_zero, Int.ofNat_eq_coe, zpow_ofNat] at hgn⊢
no goals
case mp.ofNat
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : Saturated H
n✝ : ℤ
g : G
hgn✝ : g ^ n✝ ∈ H
n : ℕ
hgn : g ^ n ∈ H
⊢ n = 0 ∨ g ∈ H
exact hH hgn
case mp.negSucc
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : Saturated H
n✝ : ℤ
g : G
hgn✝ : g ^ n✝ ∈ H
n : ℕ
hgn : g ^ Int.negSucc n ∈ H
⊢ g ^ (n + 1) ∈ H
case mp.negSucc
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : Saturated H
n✝ : ℤ
g : G
hgn✝ : g ^ n✝ ∈ H
n : ℕ
hgn : g ^ Int.negSucc n ∈ H
⊢ Int.negSucc n = 0 ∨ g ∈ H
suffices g ^ (n + 1) ∈ H by
  refine' (hH this).imp _ id
  simp only [IsEmpty.forall_iff, Nat.succ_ne_zero]
no goals
case mp.negSucc
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : Saturated H
n✝ : ℤ
g : G
hgn✝ : g ^ n✝ ∈ H
n : ℕ
hgn : g ^ Int.negSucc n ∈ H
⊢ g ^ (n + 1) ∈ H
simpa only [inv_mem_iff, zpow_negSucc] using hgn
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : Saturated H
n✝ : ℤ
g : G
hgn✝ : g ^ n✝ ∈ H
n : ℕ
hgn : g ^ Int.negSucc n ∈ H
this : g ^ (n + 1) ∈ H
⊢ n + 1 = 0 → Int.negSucc n = 0
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : Saturated H
n✝ : ℤ
g : G
hgn✝ : g ^ n✝ ∈ H
n : ℕ
hgn : g ^ Int.negSucc n ∈ H
this : g ^ (n + 1) ∈ H
⊢ Int.negSucc n = 0 ∨ g ∈ H
refine' (hH this).imp _ id
no goals
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : Saturated H
n✝ : ℤ
g : G
hgn✝ : g ^ n✝ ∈ H
n : ℕ
hgn : g ^ Int.negSucc n ∈ H
this : g ^ (n + 1) ∈ H
⊢ n + 1 = 0 → Int.negSucc n = 0
simp only [IsEmpty.forall_iff, Nat.succ_ne_zero]
case mpr
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : ∀ (n : ℤ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H
n : ℕ
g : G
hgn : g ^ n ∈ H
⊢ n = 0 ∨ g ∈ H
case mpr
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∀ (n : ℤ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H) → Saturated H
intro h n g hgn
case mpr
G : Type u_1
inst✝ : Group G
H : Subgroup G
n : ℕ
g : G
hgn : g ^ n ∈ H
h : g ^ ↑n ∈ H → ↑n = 0 ∨ g ∈ H
⊢ n = 0 ∨ g ∈ H
case mpr
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : ∀ (n : ℤ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H
n : ℕ
g : G
hgn : g ^ n ∈ H
⊢ n = 0 ∨ g ∈ H
specialize h n g
case mpr
G : Type u_1
inst✝ : Group G
H : Subgroup G
n : ℕ
g : G
hgn : g ^ n ∈ H
h : g ^ n ∈ H → n = 0 ∨ g ∈ H
⊢ n = 0 ∨ g ∈ H
case mpr
G : Type u_1
inst✝ : Group G
H : Subgroup G
n : ℕ
g : G
hgn : g ^ n ∈ H
h : g ^ ↑n ∈ H → ↑n = 0 ∨ g ∈ H
⊢ n = 0 ∨ g ∈ H
simp only [Int.coe_nat_eq_zero, zpow_ofNat] at h
no goals
case mpr
G : Type u_1
inst✝ : Group G
H : Subgroup G
n : ℕ
g : G
hgn : g ^ n ∈ H
h : g ^ n ∈ H → n = 0 ∨ g ∈ H
⊢ n = 0 ∨ g ∈ H
apply h hgn