case refine'_1
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
⊢ Set.Finite (Set.range orderOf)

case refine'_2
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
he : Set.Finite (Set.range orderOf)
⊢ exponent G ≠ 0
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
⊢ exponent G ≠ 0 ↔ Set.Finite (Set.range orderOf)
refine' ⟨fun he => _, fun he => _⟩
case refine'_1
G : Type u
inst✝ : Monoid G
h✝ : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
h : ¬Set.Finite (Set.range orderOf)
⊢ False
case refine'_1
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
⊢ Set.Finite (Set.range orderOf)
by_contra h
case refine'_1.intro.intro.intro
G : Type u
inst✝ : Monoid G
h✝ : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
h : ¬Set.Finite (Set.range orderOf)
t : G
het : exponent G < orderOf t
⊢ False
case refine'_1
G : Type u
inst✝ : Monoid G
h✝ : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
h : ¬Set.Finite (Set.range orderOf)
⊢ False
obtain ⟨m, ⟨t, rfl⟩, het⟩ := Set.Infinite.exists_gt h (exponent G)
no goals
case refine'_1.intro.intro.intro
G : Type u
inst✝ : Monoid G
h✝ : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
h : ¬Set.Finite (Set.range orderOf)
t : G
het : exponent G < orderOf t
⊢ False
exact pow_ne_one_of_lt_orderOf' he het (pow_exponent_eq_one t)
case refine'_2.intro
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
⊢ exponent G ≠ 0
case refine'_2
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
he : Set.Finite (Set.range orderOf)
⊢ exponent G ≠ 0
lift Set.range (orderOf (G := G)) to Finset ℕ using he with t ht
case refine'_2.intro
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
htpos : 0 < Finset.prod t id
⊢ exponent G ≠ 0
case refine'_2.intro
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
⊢ exponent G ≠ 0
have htpos : 0 < t.prod id := by
  refine' Finset.prod_pos fun a ha => _
  rw [← Finset.mem_coe, ht] at ha
  obtain ⟨k, rfl⟩ := ha
  exact h k
case refine'_2.intro
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
htpos : 0 < Finset.prod t id
⊢ exponent G ∣ Finset.prod t id
case refine'_2.intro
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
htpos : 0 < Finset.prod t id
⊢ exponent G ≠ 0
suffices exponent G ∣ t.prod id by
  intro h
  rw [h, zero_dvd_iff] at this
  exact htpos.ne' this
case refine'_2.intro
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
htpos : 0 < Finset.prod t id
g : G
⊢ g ^ Finset.prod t id = 1
case refine'_2.intro
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
htpos : 0 < Finset.prod t id
⊢ exponent G ∣ Finset.prod t id
refine' exponent_dvd_of_forall_pow_eq_one _ _ fun g => _
case refine'_2.intro
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
htpos : 0 < Finset.prod t id
g : G
⊢ orderOf g ∣ Finset.prod t id
case refine'_2.intro
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
htpos : 0 < Finset.prod t id
g : G
⊢ g ^ Finset.prod t id = 1
rw [pow_eq_mod_orderOf, Nat.mod_eq_zero_of_dvd, pow_zero g]
case refine'_2.intro.ha
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
htpos : 0 < Finset.prod t id
g : G
⊢ Function.minimalPeriod (fun x => g * x) 1 ∈ t
case refine'_2.intro
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
htpos : 0 < Finset.prod t id
g : G
⊢ orderOf g ∣ Finset.prod t id
apply Finset.dvd_prod_of_mem
case refine'_2.intro.ha
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
htpos : 0 < Finset.prod t id
g : G
⊢ Function.minimalPeriod (fun x => g * x) 1 ∈ Set.range orderOf
case refine'_2.intro.ha
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
htpos : 0 < Finset.prod t id
g : G
⊢ Function.minimalPeriod (fun x => g * x) 1 ∈ t
rw [← Finset.mem_coe, ht]
no goals
case refine'_2.intro.ha
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
htpos : 0 < Finset.prod t id
g : G
⊢ Function.minimalPeriod (fun x => g * x) 1 ∈ Set.range orderOf
exact Set.mem_range_self g
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
a : ℕ
ha : a ∈ t
⊢ 0 < id a
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
⊢ 0 < Finset.prod t id
refine' Finset.prod_pos fun a ha => _
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
a : ℕ
ha : a ∈ Set.range orderOf
⊢ 0 < id a
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
a : ℕ
ha : a ∈ t
⊢ 0 < id a
rw [← Finset.mem_coe, ht] at ha
case intro
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
k : G
⊢ 0 < id (orderOf k)
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
a : ℕ
ha : a ∈ Set.range orderOf
⊢ 0 < id a
obtain ⟨k, rfl⟩ := ha
no goals
case intro
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
k : G
⊢ 0 < id (orderOf k)
exact h k
G : Type u
inst✝ : Monoid G
h✝ : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
htpos : 0 < Finset.prod t id
this : exponent G ∣ Finset.prod t id
h : exponent G = 0
⊢ False
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
htpos : 0 < Finset.prod t id
this : exponent G ∣ Finset.prod t id
⊢ exponent G ≠ 0
intro h
G : Type u
inst✝ : Monoid G
h✝ : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
htpos : 0 < Finset.prod t id
this : Finset.prod t id = 0
h : exponent G = 0
⊢ False
G : Type u
inst✝ : Monoid G
h✝ : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
htpos : 0 < Finset.prod t id
this : exponent G ∣ Finset.prod t id
h : exponent G = 0
⊢ False
rw [h, zero_dvd_iff] at this
no goals
G : Type u
inst✝ : Monoid G
h✝ : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
htpos : 0 < Finset.prod t id
this : Finset.prod t id = 0
h : exponent G = 0
⊢ False
exact htpos.ne' this