Theorem: Subgroup.mem_closure_singleton' (AlgebraI/Subgroups.lean)

State before:
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
⊢ y ∈ closure {x} ↔ ∃ n < orderOf x, x ^ n = y
Tactic:
simp only [← zpowers_eq_closure, exists_prop]
State after:
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
⊢ y ∈ zpowers x ↔ ∃ n < orderOf x, x ^ n = y

State before:
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
⊢ y ∈ zpowers x ↔ ∃ n < orderOf x, x ^ n = y
Tactic:
constructor <;>
rintro ⟨i, hi⟩
State after:
case mp.intro
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
⊢ ∃ n < orderOf x, x ^ n = y

case mpr.intro
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℕ
hi : i < orderOf x ∧ x ^ i = y
⊢ y ∈ zpowers x

State before:
case mp.intro
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
⊢ ∃ n, 0 ≤ n ∧ n < ↑(orderOf x) ∧ x ^ n = y
Tactic:
have ho : 0 < (orderOf x : ℤ) := by
  rwa [Int.coe_nat_pos, pos_iff_ne_zero, Ne.def, orderOf_eq_zero_iff, Classical.not_not]
State after:
case mp.intro
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
ho : 0 < ↑(orderOf x)
⊢ ∃ n, 0 ≤ n ∧ n < ↑(orderOf x) ∧ x ^ n = y

State before:
case mp.intro
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
ho : 0 < ↑(orderOf x)
⊢ ∃ n, 0 ≤ n ∧ n < ↑(orderOf x) ∧ x ^ n = y
Tactic:
refine' ⟨i % orderOf x, Int.emod_nonneg _ ho.ne', Int.emod_lt_of_pos _ ho, _⟩
State after:
case mp.intro
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
ho : 0 < ↑(orderOf x)
⊢ x ^ (i % ↑(orderOf x)) = y

State before:
case mp.intro
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
ho : 0 < ↑(orderOf x)
⊢ x ^ (i % ↑(orderOf x)) = y
Tactic:
rw [← hi, l1_2_20_i _ _ _ _ h]
State after:
case mp.intro
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
ho : 0 < ↑(orderOf x)
⊢ i % ↑(orderOf x) ≡ i [ZMOD ↑(orderOf x)]

State before:
case mp.intro
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
ho : 0 < ↑(orderOf x)
⊢ i % ↑(orderOf x) ≡ i [ZMOD ↑(orderOf x)]
Tactic:
exact Int.mod_modEq _ _
State after:
no goals

State before:
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
this : ∃ n, 0 ≤ n ∧ n < ↑(orderOf x) ∧ x ^ n = y
⊢ ∃ n < orderOf x, x ^ n = y
Tactic:
obtain ⟨n, hnonneg, hlt, heq⟩ := this
State after:
case intro.intro.intro
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
n : ℤ
hnonneg : 0 ≤ n
hlt : n < ↑(orderOf x)
heq : x ^ n = y
⊢ ∃ n < orderOf x, x ^ n = y

State before:
case intro.intro.intro
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
n : ℤ
hnonneg : 0 ≤ n
hlt : n < ↑(orderOf x)
heq : x ^ n = y
⊢ ∃ n < orderOf x, x ^ n = y
Tactic:
refine' ⟨n.natAbs, _, _⟩
State after:
case intro.intro.intro.refine'_1
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
n : ℤ
hnonneg : 0 ≤ n
hlt : n < ↑(orderOf x)
heq : x ^ n = y
⊢ Int.natAbs n < orderOf x

case intro.intro.intro.refine'_2
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
n : ℤ
hnonneg : 0 ≤ n
hlt : n < ↑(orderOf x)
heq : x ^ n = y
⊢ x ^ Int.natAbs n = y

State before:
case intro.intro.intro.refine'_1
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
n : ℤ
hnonneg : 0 ≤ n
hlt : n < ↑(orderOf x)
heq : x ^ n = y
⊢ Int.natAbs n < orderOf x
Tactic:
rwa [← Int.ofNat_lt, Int.natAbs_of_nonneg hnonneg]
State after:
no goals

State before:
case intro.intro.intro.refine'_2
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
n : ℤ
hnonneg : 0 ≤ n
hlt : n < ↑(orderOf x)
heq : x ^ n = y
⊢ x ^ Int.natAbs n = y
Tactic:
rwa [← zpow_ofNat, Int.natAbs_of_nonneg hnonneg]
State after:
no goals

State before:
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
⊢ 0 < ↑(orderOf x)
Tactic:
rwa [Int.coe_nat_pos, pos_iff_ne_zero, Ne.def, orderOf_eq_zero_iff, Classical.not_not]
State after:
no goals

State before:
case mpr.intro
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℕ
hi : i < orderOf x ∧ x ^ i = y
⊢ y ∈ zpowers x
Tactic:
use i
State after:
case h
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℕ
hi : i < orderOf x ∧ x ^ i = y
⊢ (fun x_1 => x ^ x_1) ↑i = y

State before:
case h
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℕ
hi : i < orderOf x ∧ x ^ i = y
⊢ (fun x_1 => x ^ x_1) ↑i = y
Tactic:
simp only [zpow_ofNat, hi.2]
State after:
no goals