[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Saturated H ↔ ∀ (n : ℤ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H
[PROOFSTEP]
constructor
[GOAL]
case mp
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Saturated H → ∀ (n : ℤ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H
[PROOFSTEP]
intros hH n g hgn
[GOAL]
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
[PROOFSTEP]
induction' n with n n
[GOAL]
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
[PROOFSTEP]
simp only [Int.coe_nat_eq_zero, Int.ofNat_eq_coe, zpow_ofNat] at hgn ⊢
[GOAL]
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
[PROOFSTEP]
exact hH hgn
[GOAL]
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
[PROOFSTEP]
suffices g ^ (n + 1) ∈ H by
  refine' (hH this).imp _ id
  simp only [IsEmpty.forall_iff, Nat.succ_ne_zero]
[GOAL]
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
[PROOFSTEP]
refine' (hH this).imp _ id
[GOAL]
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
[PROOFSTEP]
simp only [IsEmpty.forall_iff, Nat.succ_ne_zero]
[GOAL]
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
[PROOFSTEP]
simpa only [inv_mem_iff, zpow_negSucc] using hgn
[GOAL]
case mpr
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∀ (n : ℤ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H) → Saturated H
[PROOFSTEP]
intro h n g hgn
[GOAL]
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
[PROOFSTEP]
specialize h n g
[GOAL]
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
[PROOFSTEP]
simp only [Int.coe_nat_eq_zero, zpow_ofNat] at h 
[GOAL]
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
[PROOFSTEP]
apply h hgn
[GOAL]
A₁ : Type u_1
A₂ : Type u_2
inst✝² : AddCommGroup A₁
inst✝¹ : AddCommGroup A₂
inst✝ : NoZeroSMulDivisors ℕ A₂
f : A₁ →+ A₂
⊢ Saturated (AddMonoidHom.ker f)
[PROOFSTEP]
intro n g hg
[GOAL]
A₁ : Type u_1
A₂ : Type u_2
inst✝² : AddCommGroup A₁
inst✝¹ : AddCommGroup A₂
inst✝ : NoZeroSMulDivisors ℕ A₂
f : A₁ →+ A₂
n : ℕ
g : A₁
hg : n • g ∈ AddMonoidHom.ker f
⊢ n = 0 ∨ g ∈ AddMonoidHom.ker f
[PROOFSTEP]
simpa only [f.mem_ker, nsmul_eq_smul, f.map_nsmul, smul_eq_zero] using hg
