-- Mathlib/GroupTheory/Exponent.lean
theorem exponent_eq_iSup_orderOf (h : ∀ g : G, 0 < orderOf g) :
    exponent G = ⨆ g : G, orderOf g

Proof state:
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
⊢ exponent G = ⨆ g, orderOf g

Tactic:
rw [iSup]

Result:
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
⊢ exponent G = sSup (Set.range fun g => orderOf g)

Proof state:
case H
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
⊢ ∀ a ∈ Set.range fun g => orderOf g, a ≤ exponent G

Tactic:
simp_rw [Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff]

Result:
case H
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
⊢ ∀ (a : G), orderOf a ≤ exponent G

Proof state:
case H'
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
x : ℕ
hx : x < exponent G
⊢ ∃ a ∈ Set.range fun g => orderOf g, x < a

Tactic:
obtain ⟨g, hg⟩ := exists_orderOf_eq_exponent he

Result:
case H'.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
x : ℕ
hx : x < exponent G
g : G
hg : orderOf g = exponent G
⊢ ∃ a ∈ Set.range fun g => orderOf g, x < a

Proof state:
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G = 0
⊢ exponent G = sSup (Set.range fun g => orderOf g)

Tactic:
rw [he, Set.Infinite.Nat.sSup_eq_zero <| (exponent_eq_zero_iff_range_orderOf_infinite h).1 he]

Result:
no goals

Proof state:
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ¬ExponentExists G
⊢ exponent G = sSup (Set.range fun g => orderOf g)

Tactic:
rw [← exponent_eq_zero_iff] at he

Result:
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G = 0
⊢ exponent G = sSup (Set.range fun g => orderOf g)

Proof state:
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
⊢ exponent G = sSup (Set.range fun g => orderOf g)

Tactic:
by_cases ExponentExists G

Result:
case pos
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
h✝ : ExponentExists G
⊢ exponent G = sSup (Set.range fun g => orderOf g)

case neg
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
h✝ : ¬ExponentExists G
⊢ exponent G = sSup (Set.range fun g => orderOf g)

Proof state:
case H'
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
⊢ ∀ w < exponent G, ∃ a ∈ Set.range fun g => orderOf g, w < a

Tactic:
intro x hx

Result:
case H'
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
x : ℕ
hx : x < exponent G
⊢ ∃ a ∈ Set.range fun g => orderOf g, x < a

Proof state:
case pos
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
h✝ : ExponentExists G
⊢ exponent G = sSup (Set.range fun g => orderOf g)

case neg
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
h✝ : ¬ExponentExists G
⊢ exponent G = sSup (Set.range fun g => orderOf g)

Tactic:
case neg he =>
  rw [← exponent_eq_zero_iff] at he
  rw [he, Set.Infinite.Nat.sSup_eq_zero <| (exponent_eq_zero_iff_range_orderOf_infinite h).1 he]

Result:
case pos
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
h✝ : ExponentExists G
⊢ exponent G = sSup (Set.range fun g => orderOf g)

Proof state:
case H'.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
x : ℕ
g : G
hx : x < orderOf g
hg : orderOf g = exponent G
⊢ ∃ a ∈ Set.range fun g => orderOf g, x < a

Tactic:
simp_rw [Set.mem_range, exists_exists_eq_and]

Result:
case H'.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
x : ℕ
g : G
hx : x < orderOf g
hg : orderOf g = exponent G
⊢ ∃ a, x < orderOf a

Proof state:
case H'.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
x : ℕ
g : G
hx : x < orderOf g
hg : orderOf g = exponent G
⊢ ∃ a, x < orderOf a

Tactic:
exact ⟨g, hx⟩

Result:
no goals

Proof state:
case H'.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
x : ℕ
hx : x < exponent G
g : G
hg : orderOf g = exponent G
⊢ ∃ a ∈ Set.range fun g => orderOf g, x < a

Tactic:
rw [← hg] at hx

Result:
case H'.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
x : ℕ
g : G
hx : x < orderOf g
hg : orderOf g = exponent G
⊢ ∃ a ∈ Set.range fun g => orderOf g, x < a

Proof state:
case H
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
⊢ ∀ (a : G), orderOf a ≤ exponent G

Tactic:
exact orderOf_le_exponent he

Result:
no goals

Proof state:
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
⊢ exponent G = sSup (Set.range fun g => orderOf g)

Tactic:
rw [csSup_eq_of_forall_le_of_forall_lt_exists_gt (Set.range_nonempty _)]

Result:
case H
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
⊢ ∀ a ∈ Set.range fun g => orderOf g, a ≤ exponent G

case H'
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
⊢ ∀ w < exponent G, ∃ a ∈ Set.range fun g => orderOf g, w < a