-- Mathlib/GroupTheory/Subgroup/Saturated.lean
theorem saturated_iff_zpow {H : Subgroup G} :
    Saturated H ↔ ∀ (n : ℤ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H

Proof state:
case mp
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : H.Saturated
n : ℤ
g : G
hgn : g ^ n ∈ H
⊢ n = 0 ∨ g ∈ H

Tactic:
cases n with
| ofNat n =>
  simp only [Int.natCast_eq_zero, Int.ofNat_eq_coe, zpow_natCast] at hgn ⊢
  exact hH hgn
| negSucc n =>
  suffices g ^ (n + 1) ∈ H by
    refine (hH this).imp ?_ id
    simp only [IsEmpty.forall_iff, Nat.succ_ne_zero]
  simpa only [inv_mem_iff, zpow_negSucc] using hgn

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : H.Saturated
g : G
n : ℕ
hgn : g ^ Int.negSucc n ∈ H
this : g ^ (n + 1) ∈ H
⊢ n + 1 = 0 → Int.negSucc n = 0

Tactic:
simp only [IsEmpty.forall_iff, Nat.succ_ne_zero]

Result:
no goals

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

Tactic:
intro h n g hgn

Result:
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

Proof state:
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

Tactic:
apply h hgn

Result:
no goals

Proof state:
case mp.ofNat
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : H.Saturated
g : G
n : ℕ
hgn : g ^ n ∈ H
⊢ n = 0 ∨ g ∈ H

Tactic:
exact hH hgn

Result:
no goals

Proof state:
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

Tactic:
specialize h n g

Result:
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

Proof state:
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

Tactic:
simp only [Int.natCast_eq_zero, zpow_natCast] at h

Result:
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

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

Tactic:
constructor

Result:
case mp
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.Saturated → ∀ (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) → H.Saturated

Proof state:
case mp.negSucc
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : H.Saturated
g : G
n : ℕ
hgn : g ^ Int.negSucc n ∈ H
⊢ g ^ (n + 1) ∈ H

Tactic:
simpa only [inv_mem_iff, zpow_negSucc] using hgn

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : H.Saturated
g : G
n : ℕ
hgn : g ^ Int.negSucc n ∈ H
this : g ^ (n + 1) ∈ H
⊢ Int.negSucc n = 0 ∨ g ∈ H

Tactic:
refine (hH this).imp ?_ id

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : H.Saturated
g : G
n : ℕ
hgn : g ^ Int.negSucc n ∈ H
this : g ^ (n + 1) ∈ H
⊢ n + 1 = 0 → Int.negSucc n = 0

Proof state:
case mp.ofNat
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : H.Saturated
g : G
n : ℕ
hgn : g ^ Int.ofNat n ∈ H
⊢ Int.ofNat n = 0 ∨ g ∈ H

Tactic:
simp only [Int.natCast_eq_zero, Int.ofNat_eq_coe, zpow_natCast] at hgn ⊢

Result:
case mp.ofNat
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : H.Saturated
g : G
n : ℕ
hgn : g ^ n ∈ H
⊢ n = 0 ∨ g ∈ H

Proof state:
case mp.negSucc
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : H.Saturated
g : G
n : ℕ
hgn : g ^ Int.negSucc n ∈ H
⊢ Int.negSucc n = 0 ∨ g ∈ H

Tactic:
suffices g ^ (n + 1) ∈ H by
  refine (hH this).imp ?_ id
  simp only [IsEmpty.forall_iff, Nat.succ_ne_zero]

Result:
case mp.negSucc
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : H.Saturated
g : G
n : ℕ
hgn : g ^ Int.negSucc n ∈ H
⊢ g ^ (n + 1) ∈ H

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

Tactic:
intros hH n g hgn

Result:
case mp
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : H.Saturated
n : ℤ
g : G
hgn : g ^ n ∈ H
⊢ n = 0 ∨ g ∈ H