-- Mathlib/GroupTheory/Exponent.lean
theorem exponent_ne_zero_iff_range_orderOf_finite (h : ∀ g : G, 0 < orderOf g) :
    exponent G ≠ 0 ↔ (Set.range (orderOf : G → ℕ)).Finite

Proof state:
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 ↔ (↑t).Finite)
htpos : 0 < t.prod id
⊢ ∀ (g : G), orderOf g ∣ t.prod id

Tactic:
intro g

Result:
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 ↔ (↑t).Finite)
htpos : 0 < t.prod id
g : G
⊢ orderOf g ∣ t.prod id

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

Tactic:
by_contra h

Result:
case refine_1
G : Type u
inst✝ : Monoid G
h✝ : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
h : ¬(Set.range orderOf).Finite
⊢ False

Proof state:
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 ↔ (↑t).Finite)
htpos : 0 < t.prod id
⊢ exponent G ≠ 0

Tactic:
suffices exponent G ∣ t.prod id by
  intro h
  rw [h, zero_dvd_iff] at this
  exact htpos.ne' this

Result:
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 ↔ (↑t).Finite)
htpos : 0 < t.prod id
⊢ exponent G ∣ t.prod id

Proof state:
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
⊢ exponent G ≠ 0 ↔ (Set.range orderOf).Finite

Tactic:
refine ⟨fun he => ?_, fun he => ?_⟩

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

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

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

Tactic:
lift Set.range (orderOf (G := G)) to Finset ℕ using he with t ht

Result:
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 ↔ (↑t).Finite)
⊢ exponent G ≠ 0

Proof state:
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 ↔ (↑t).Finite)
⊢ 0 < t.prod id

Tactic:
refine Finset.prod_pos fun a ha => ?_

Result:
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 ↔ (↑t).Finite)
a : ℕ
ha : a ∈ t
⊢ 0 < id a

Proof state:
case refine_1
G : Type u
inst✝ : Monoid G
h✝ : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
h : ¬(Set.range orderOf).Finite
⊢ False

Tactic:
obtain ⟨m, ⟨t, rfl⟩, het⟩ := Set.Infinite.exists_gt h (exponent G)

Result:
case refine_1.intro.intro.intro
G : Type u
inst✝ : Monoid G
h✝ : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
h : ¬(Set.range orderOf).Finite
t : G
het : exponent G < orderOf t
⊢ False

Proof state:
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 ↔ (↑t).Finite)
⊢ exponent G ≠ 0

Tactic:
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

Result:
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 ↔ (↑t).Finite)
htpos : 0 < t.prod id
⊢ exponent G ≠ 0

Proof state:
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 ↔ (↑t).Finite)
k : G
⊢ 0 < id (orderOf k)

Tactic:
exact h k

Result:
no goals

Proof state:
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 ↔ (↑t).Finite)
a : ℕ
ha : a ∈ t
⊢ 0 < id a

Tactic:
rw [← Finset.mem_coe, ht] at ha

Result:
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 ↔ (↑t).Finite)
a : ℕ
ha : a ∈ Set.range orderOf
⊢ 0 < id a

Proof state:
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 ↔ (↑t).Finite)
htpos : 0 < t.prod id
g : G
⊢ orderOf g ∣ t.prod id

Tactic:
apply Finset.dvd_prod_of_mem id (?_ : orderOf g ∈ _)

Result:
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 ↔ (↑t).Finite)
htpos : 0 < t.prod id
g : G
⊢ orderOf g ∈ t

Proof state:
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 ↔ (↑t).Finite)
htpos : 0 < t.prod id
this : t.prod id = 0
h : exponent G = 0
⊢ False

Tactic:
exact htpos.ne' this

Result:
no goals

Proof state:
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 ↔ (↑t).Finite)
htpos : 0 < t.prod id
g : G
⊢ orderOf g ∈ Set.range orderOf

Tactic:
exact Set.mem_range_self g

Result:
no goals

Proof state:
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 ↔ (↑t).Finite)
a : ℕ
ha : a ∈ Set.range orderOf
⊢ 0 < id a

Tactic:
obtain ⟨k, rfl⟩ := ha

Result:
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 ↔ (↑t).Finite)
k : G
⊢ 0 < id (orderOf k)

Proof state:
case refine_1.intro.intro.intro
G : Type u
inst✝ : Monoid G
h✝ : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
h : ¬(Set.range orderOf).Finite
t : G
het : exponent G < orderOf t
⊢ False

Tactic:
exact pow_ne_one_of_lt_orderOf he het (pow_exponent_eq_one t)

Result:
no goals