case refine'_1
G : Type u_1
G' : Type ?u.216540
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.216549
inst✝ : AddGroup A
H K : Subgroup G
k : Set G
x y : G
hy : y ∈ closure {x}
⊢ ∀ (x_1 : G), x_1 ∈ {x} → ∃ n, x ^ n = x_1

case refine'_2
G : Type u_1
G' : Type ?u.216540
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.216549
inst✝ : AddGroup A
H K : Subgroup G
k : Set G
x y : G
hy : y ∈ closure {x}
⊢ ∃ n, x ^ n = 1

case refine'_3
G : Type u_1
G' : Type ?u.216540
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.216549
inst✝ : AddGroup A
H K : Subgroup G
k : Set G
x y : G
hy : y ∈ closure {x}
⊢ ∀ (x_1 y : G), (∃ n, x ^ n = x_1) → (∃ n, x ^ n = y) → ∃ n, x ^ n = x_1 * y

case refine'_4
G : Type u_1
G' : Type ?u.216540
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.216549
inst✝ : AddGroup A
H K : Subgroup G
k : Set G
x y : G
hy : y ∈ closure {x}
⊢ ∀ (x_1 : G), (∃ n, x ^ n = x_1) → ∃ n, x ^ n = x_1⁻¹
G : Type u_1
G' : Type ?u.216540
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.216549
inst✝ : AddGroup A
H K : Subgroup G
k : Set G
x y : G
⊢ y ∈ closure {x} ↔ ∃ n, x ^ n = y
refine'
  ⟨fun hy => closure_induction hy _ _ _ _, fun ⟨n, hn⟩ =>
    hn ▸ zpow_mem (subset_closure <| mem_singleton x) n⟩
case refine'_4.intro
G : Type u_1
G' : Type ?u.216540
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.216549
inst✝ : AddGroup A
H K : Subgroup G
k : Set G
x y : G
hy : y ∈ closure {x}
n : ℤ
⊢ ∃ n_1, x ^ n_1 = (x ^ n)⁻¹
case refine'_4
G : Type u_1
G' : Type ?u.216540
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.216549
inst✝ : AddGroup A
H K : Subgroup G
k : Set G
x y : G
hy : y ∈ closure {x}
⊢ ∀ (x_1 : G), (∃ n, x ^ n = x_1) → ∃ n, x ^ n = x_1⁻¹
rintro _ ⟨n, rfl⟩
no goals
case refine'_4.intro
G : Type u_1
G' : Type ?u.216540
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.216549
inst✝ : AddGroup A
H K : Subgroup G
k : Set G
x y : G
hy : y ∈ closure {x}
n : ℤ
⊢ ∃ n_1, x ^ n_1 = (x ^ n)⁻¹
exact ⟨-n, zpow_neg x n⟩
case refine'_1
G : Type u_1
G' : Type ?u.216540
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.216549
inst✝ : AddGroup A
H K : Subgroup G
k : Set G
x y✝ : G
hy✝ : y✝ ∈ closure {x}
y : G
hy : y ∈ {x}
⊢ ∃ n, x ^ n = y
case refine'_1
G : Type u_1
G' : Type ?u.216540
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.216549
inst✝ : AddGroup A
H K : Subgroup G
k : Set G
x y : G
hy : y ∈ closure {x}
⊢ ∀ (x_1 : G), x_1 ∈ {x} → ∃ n, x ^ n = x_1
intro y hy
case refine'_1
G : Type u_1
G' : Type ?u.216540
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.216549
inst✝ : AddGroup A
H K : Subgroup G
k : Set G
x y✝ : G
hy✝ : y✝ ∈ closure {x}
y : G
hy : y ∈ {x}
⊢ ∃ n, x ^ n = x
case refine'_1
G : Type u_1
G' : Type ?u.216540
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.216549
inst✝ : AddGroup A
H K : Subgroup G
k : Set G
x y✝ : G
hy✝ : y✝ ∈ closure {x}
y : G
hy : y ∈ {x}
⊢ ∃ n, x ^ n = y
rw [eq_of_mem_singleton hy]
no goals
case refine'_1
G : Type u_1
G' : Type ?u.216540
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.216549
inst✝ : AddGroup A
H K : Subgroup G
k : Set G
x y✝ : G
hy✝ : y✝ ∈ closure {x}
y : G
hy : y ∈ {x}
⊢ ∃ n, x ^ n = x
exact ⟨1, zpow_one x⟩
no goals
case refine'_2
G : Type u_1
G' : Type ?u.216540
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.216549
inst✝ : AddGroup A
H K : Subgroup G
k : Set G
x y : G
hy : y ∈ closure {x}
⊢ ∃ n, x ^ n = 1
exact ⟨0, zpow_zero x⟩
case refine'_3.intro.intro
G : Type u_1
G' : Type ?u.216540
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.216549
inst✝ : AddGroup A
H K : Subgroup G
k : Set G
x y : G
hy : y ∈ closure {x}
n m : ℤ
⊢ ∃ n_1, x ^ n_1 = x ^ n * x ^ m
case refine'_3
G : Type u_1
G' : Type ?u.216540
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.216549
inst✝ : AddGroup A
H K : Subgroup G
k : Set G
x y : G
hy : y ∈ closure {x}
⊢ ∀ (x_1 y : G), (∃ n, x ^ n = x_1) → (∃ n, x ^ n = y) → ∃ n, x ^ n = x_1 * y
rintro _ _ ⟨n, rfl⟩ ⟨m, rfl⟩
no goals
case refine'_3.intro.intro
G : Type u_1
G' : Type ?u.216540
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.216549
inst✝ : AddGroup A
H K : Subgroup G
k : Set G
x y : G
hy : y ∈ closure {x}
n m : ℤ
⊢ ∃ n_1, x ^ n_1 = x ^ n * x ^ m
exact ⟨n + m, zpow_add x n m⟩