case intro.intro
G : Type u
A : Type v
x✝ y : G
a b : A
n✝ m : ℕ
inst✝² : Monoid G
inst✝¹ : AddMonoid A
η : Type u_1
Gs : η → Type u_2
inst✝ : (i : η) → Monoid (Gs i)
x : (i : η) → Gs i
h : IsOfFinOrder x
n : ℕ
npos : 0 < n
hn : x ^ n = 1
⊢ ∀ (i : η), IsOfFinOrder (x i)
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝² : Monoid G
inst✝¹ : AddMonoid A
η : Type u_1
Gs : η → Type u_2
inst✝ : (i : η) → Monoid (Gs i)
x : (i : η) → Gs i
h : IsOfFinOrder x
⊢ ∀ (i : η), IsOfFinOrder (x i)
rcases(isOfFinOrder_iff_pow_eq_one _).mp h with ⟨n, npos, hn⟩
no goals
case intro.intro
G : Type u
A : Type v
x✝ y : G
a b : A
n✝ m : ℕ
inst✝² : Monoid G
inst✝¹ : AddMonoid A
η : Type u_1
Gs : η → Type u_2
inst✝ : (i : η) → Monoid (Gs i)
x : (i : η) → Gs i
h : IsOfFinOrder x
n : ℕ
npos : 0 < n
hn : x ^ n = 1
⊢ ∀ (i : η), IsOfFinOrder (x i)
exact fun _ => (isOfFinOrder_iff_pow_eq_one _).mpr ⟨n, npos, (congr_fun hn.symm _).symm⟩