no goals
α : Type u
a✝ : α
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : IsCyclic H
f : G →* H
hf : MonoidHom.ker f ≤ center G
a b : G
x : H
y : G
hxy : ↑f y = x
hx : ∀ (a : { x // x ∈ MonoidHom.range f }), a ∈ zpowers { val := x, property := (_ : ∃ y, ↑f y = x) }
m : ℤ
hm :
  (fun x x_1 => x ^ x_1) { val := x, property := (_ : ∃ y, ↑f y = x) } m =
    { val := ↑f a, property := (_ : ∃ y, ↑f y = ↑f a) }
n : ℤ
hn :
  (fun x x_1 => x ^ x_1) { val := x, property := (_ : ∃ y, ↑f y = x) } n =
    { val := ↑f b, property := (_ : ∃ y, ↑f y = ↑f b) }
⊢ x ^ m = ↑f a
simpa [Subtype.ext_iff] using hm
no goals
α : Type u
a✝ : α
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : IsCyclic H
f : G →* H
hf : MonoidHom.ker f ≤ center G
a b : G
x : H
y : G
hxy : ↑f y = x
hx : ∀ (a : { x // x ∈ MonoidHom.range f }), a ∈ zpowers { val := x, property := (_ : ∃ y, ↑f y = x) }
m : ℤ
hm✝ :
  (fun x x_1 => x ^ x_1) { val := x, property := (_ : ∃ y, ↑f y = x) } m =
    { val := ↑f a, property := (_ : ∃ y, ↑f y = ↑f a) }
n : ℤ
hn :
  (fun x x_1 => x ^ x_1) { val := x, property := (_ : ∃ y, ↑f y = x) } n =
    { val := ↑f b, property := (_ : ∃ y, ↑f y = ↑f b) }
hm : x ^ m = ↑f a
⊢ x ^ n = ↑f b
simpa [Subtype.ext_iff] using hn
no goals
α : Type u
a✝ : α
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : IsCyclic H
f : G →* H
hf : MonoidHom.ker f ≤ center G
a b : G
x : H
y : G
hxy : ↑f y = x
hx : ∀ (a : { x // x ∈ MonoidHom.range f }), a ∈ zpowers { val := x, property := (_ : ∃ y, ↑f y = x) }
m : ℤ
hm✝ :
  (fun x x_1 => x ^ x_1) { val := x, property := (_ : ∃ y, ↑f y = x) } m =
    { val := ↑f a, property := (_ : ∃ y, ↑f y = ↑f a) }
n : ℤ
hn✝ :
  (fun x x_1 => x ^ x_1) { val := x, property := (_ : ∃ y, ↑f y = x) } n =
    { val := ↑f b, property := (_ : ∃ y, ↑f y = ↑f b) }
hm : x ^ m = ↑f a
hn : x ^ n = ↑f b
⊢ y ^ (-m) * a ∈ MonoidHom.ker f
rw [f.mem_ker, f.map_mul, f.map_zpow, hxy, zpow_neg x m, hm, inv_mul_self]
no goals
α : Type u
a✝ : α
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : IsCyclic H
f : G →* H
hf : MonoidHom.ker f ≤ center G
a b : G
x : H
y : G
hxy : ↑f y = x
hx : ∀ (a : { x // x ∈ MonoidHom.range f }), a ∈ zpowers { val := x, property := (_ : ∃ y, ↑f y = x) }
m : ℤ
hm✝ :
  (fun x x_1 => x ^ x_1) { val := x, property := (_ : ∃ y, ↑f y = x) } m =
    { val := ↑f a, property := (_ : ∃ y, ↑f y = ↑f a) }
n : ℤ
hn✝ :
  (fun x x_1 => x ^ x_1) { val := x, property := (_ : ∃ y, ↑f y = x) } n =
    { val := ↑f b, property := (_ : ∃ y, ↑f y = ↑f b) }
hm : x ^ m = ↑f a
hn : x ^ n = ↑f b
ha : y ^ (-m) * a ∈ center G
⊢ y ^ (-n) * b ∈ MonoidHom.ker f
rw [f.mem_ker, f.map_mul, f.map_zpow, hxy, zpow_neg x n, hn, inv_mul_self]
no goals
α : Type u
a✝ : α
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : IsCyclic H
f : G →* H
hf : MonoidHom.ker f ≤ center G
a b : G
x : H
y : G
hxy : ↑f y = x
hx : ∀ (a : { x // x ∈ MonoidHom.range f }), a ∈ zpowers { val := x, property := (_ : ∃ y, ↑f y = x) }
m : ℤ
hm✝ :
  (fun x x_1 => x ^ x_1) { val := x, property := (_ : ∃ y, ↑f y = x) } m =
    { val := ↑f a, property := (_ : ∃ y, ↑f y = ↑f a) }
n : ℤ
hn✝ :
  (fun x x_1 => x ^ x_1) { val := x, property := (_ : ∃ y, ↑f y = x) } n =
    { val := ↑f b, property := (_ : ∃ y, ↑f y = ↑f b) }
hm : x ^ m = ↑f a
hn : x ^ n = ↑f b
ha : y ^ (-m) * a ∈ center G
hb : y ^ (-n) * b ∈ center G
⊢ a * b = y ^ m * (y ^ (-m) * a * y ^ n) * (y ^ (-n) * b)
simp [mul_assoc]
no goals
α : Type u
a✝ : α
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : IsCyclic H
f : G →* H
hf : MonoidHom.ker f ≤ center G
a b : G
x : H
y : G
hxy : ↑f y = x
hx : ∀ (a : { x // x ∈ MonoidHom.range f }), a ∈ zpowers { val := x, property := (_ : ∃ y, ↑f y = x) }
m : ℤ
hm✝ :
  (fun x x_1 => x ^ x_1) { val := x, property := (_ : ∃ y, ↑f y = x) } m =
    { val := ↑f a, property := (_ : ∃ y, ↑f y = ↑f a) }
n : ℤ
hn✝ :
  (fun x x_1 => x ^ x_1) { val := x, property := (_ : ∃ y, ↑f y = x) } n =
    { val := ↑f b, property := (_ : ∃ y, ↑f y = ↑f b) }
hm : x ^ m = ↑f a
hn : x ^ n = ↑f b
ha : y ^ (-m) * a ∈ center G
hb : y ^ (-n) * b ∈ center G
⊢ y ^ m * (y ^ (-m) * a * y ^ n) * (y ^ (-n) * b) = y ^ m * (y ^ n * (y ^ (-m) * a)) * (y ^ (-n) * b)
rw [mem_center_iff.1 ha]
no goals
α : Type u
a✝ : α
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : IsCyclic H
f : G →* H
hf : MonoidHom.ker f ≤ center G
a b : G
x : H
y : G
hxy : ↑f y = x
hx : ∀ (a : { x // x ∈ MonoidHom.range f }), a ∈ zpowers { val := x, property := (_ : ∃ y, ↑f y = x) }
m : ℤ
hm✝ :
  (fun x x_1 => x ^ x_1) { val := x, property := (_ : ∃ y, ↑f y = x) } m =
    { val := ↑f a, property := (_ : ∃ y, ↑f y = ↑f a) }
n : ℤ
hn✝ :
  (fun x x_1 => x ^ x_1) { val := x, property := (_ : ∃ y, ↑f y = x) } n =
    { val := ↑f b, property := (_ : ∃ y, ↑f y = ↑f b) }
hm : x ^ m = ↑f a
hn : x ^ n = ↑f b
ha : y ^ (-m) * a ∈ center G
hb : y ^ (-n) * b ∈ center G
⊢ y ^ m * (y ^ n * (y ^ (-m) * a)) * (y ^ (-n) * b) = y ^ m * y ^ n * y ^ (-m) * (a * (y ^ (-n) * b))
simp [mul_assoc]
no goals
α : Type u
a✝ : α
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : IsCyclic H
f : G →* H
hf : MonoidHom.ker f ≤ center G
a b : G
x : H
y : G
hxy : ↑f y = x
hx : ∀ (a : { x // x ∈ MonoidHom.range f }), a ∈ zpowers { val := x, property := (_ : ∃ y, ↑f y = x) }
m : ℤ
hm✝ :
  (fun x x_1 => x ^ x_1) { val := x, property := (_ : ∃ y, ↑f y = x) } m =
    { val := ↑f a, property := (_ : ∃ y, ↑f y = ↑f a) }
n : ℤ
hn✝ :
  (fun x x_1 => x ^ x_1) { val := x, property := (_ : ∃ y, ↑f y = x) } n =
    { val := ↑f b, property := (_ : ∃ y, ↑f y = ↑f b) }
hm : x ^ m = ↑f a
hn : x ^ n = ↑f b
ha : y ^ (-m) * a ∈ center G
hb : y ^ (-n) * b ∈ center G
⊢ y ^ m * y ^ n * y ^ (-m) * (a * (y ^ (-n) * b)) = y ^ m * y ^ n * y ^ (-m) * (y ^ (-n) * b * a)
rw [mem_center_iff.1 hb]
no goals
α : Type u
a✝ : α
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : IsCyclic H
f : G →* H
hf : MonoidHom.ker f ≤ center G
a b : G
x : H
y : G
hxy : ↑f y = x
hx : ∀ (a : { x // x ∈ MonoidHom.range f }), a ∈ zpowers { val := x, property := (_ : ∃ y, ↑f y = x) }
m : ℤ
hm✝ :
  (fun x x_1 => x ^ x_1) { val := x, property := (_ : ∃ y, ↑f y = x) } m =
    { val := ↑f a, property := (_ : ∃ y, ↑f y = ↑f a) }
n : ℤ
hn✝ :
  (fun x x_1 => x ^ x_1) { val := x, property := (_ : ∃ y, ↑f y = x) } n =
    { val := ↑f b, property := (_ : ∃ y, ↑f y = ↑f b) }
hm : x ^ m = ↑f a
hn : x ^ n = ↑f b
ha : y ^ (-m) * a ∈ center G
hb : y ^ (-n) * b ∈ center G
⊢ y ^ m * y ^ n * y ^ (-m) * (y ^ (-n) * b * a) = b * a
group