-- Mathlib/GroupTheory/OrderOfElement.lean
theorem infinite_not_isOfFinOrder {x : G} (h : ¬IsOfFinOrder x) :
    { y : G | ¬IsOfFinOrder y }.Infinite

Proof state:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
this : s.Infinite
⊢ {y | ¬IsOfFinOrder y}.Infinite

Tactic:
exact this.mono hs

Result:
no goals

Proof state:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
h : ¬s.Infinite
⊢ IsOfFinOrder x

Tactic:
have : ¬Injective fun n : ℕ => x ^ n := by
  have := Set.not_injOn_infinite_finite_image (Set.Ioi_infinite 0) (Set.not_infinite.mp h)
  contrapose! this
  exact Set.injOn_of_injective this

Result:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
h : ¬s.Infinite
this : ¬Injective fun n => x ^ n
⊢ IsOfFinOrder x

Proof state:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
h : ¬s.Infinite
this : Injective fun n => x ^ n
⊢ Set.InjOn (fun n => x ^ n) (Set.Ioi 0)

Tactic:
exact Set.injOn_of_injective this

Result:
no goals

Proof state:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
h : ¬s.Infinite
⊢ ¬Injective fun n => x ^ n

Tactic:
have := Set.not_injOn_infinite_finite_image (Set.Ioi_infinite 0) (Set.not_infinite.mp h)

Result:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
h : ¬s.Infinite
this : ¬Set.InjOn (fun n => x ^ n) (Set.Ioi 0)
⊢ ¬Injective fun n => x ^ n

Proof state:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
⊢ s.Infinite

Tactic:
contrapose! h

Result:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
h : ¬s.Infinite
⊢ IsOfFinOrder x

Proof state:
case intro.intro
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
n : ℕ
hn : 0 < n
contra : IsOfFinOrder (x ^ n)
⊢ False

Tactic:
apply h

Result:
case intro.intro
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
n : ℕ
hn : 0 < n
contra : IsOfFinOrder (x ^ n)
⊢ IsOfFinOrder x

Proof state:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
h : ¬s.Infinite
this : ¬Set.InjOn (fun n => x ^ n) (Set.Ioi 0)
⊢ ¬Injective fun n => x ^ n

Tactic:
contrapose! this

Result:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
h : ¬s.Infinite
this : Injective fun n => x ^ n
⊢ Set.InjOn (fun n => x ^ n) (Set.Ioi 0)

Proof state:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
⊢ {y | ¬IsOfFinOrder y}.Infinite

Tactic:
have hs : s ⊆ { y : G | ¬IsOfFinOrder y } := by
  rintro - ⟨n, hn : 0 < n, rfl⟩ (contra : IsOfFinOrder (x ^ n))
  apply h
  rw [isOfFinOrder_iff_pow_eq_one] at contra ⊢
  obtain ⟨m, hm, hm'⟩ := contra
  exact ⟨n * m, mul_pos hn hm, by rwa [pow_mul]⟩

Result:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
⊢ {y | ¬IsOfFinOrder y}.Infinite

Proof state:
case intro.intro
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
n : ℕ
hn : 0 < n
contra : IsOfFinOrder (x ^ n)
⊢ IsOfFinOrder x

Tactic:
rw [isOfFinOrder_iff_pow_eq_one] at contra ⊢

Result:
case intro.intro
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
n : ℕ
hn : 0 < n
contra : ∃ n_1, 0 < n_1 ∧ (x ^ n) ^ n_1 = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1

Proof state:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
⊢ s ⊆ {y | ¬IsOfFinOrder y}

Tactic:
rintro - ⟨n, hn : 0 < n, rfl⟩ (contra : IsOfFinOrder (x ^ n))

Result:
case intro.intro
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
n : ℕ
hn : 0 < n
contra : IsOfFinOrder (x ^ n)
⊢ False

Proof state:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
⊢ {y | ¬IsOfFinOrder y}.Infinite

Tactic:
suffices s.Infinite by exact this.mono hs

Result:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
⊢ s.Infinite

Proof state:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
h : ¬s.Infinite
this : ¬Injective fun n => x ^ n
⊢ IsOfFinOrder x

Tactic:
rwa [injective_pow_iff_not_isOfFinOrder, Classical.not_not] at this

Result:
no goals

Proof state:
case intro.intro
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
n : ℕ
hn : 0 < n
contra : ∃ n_1, 0 < n_1 ∧ (x ^ n) ^ n_1 = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1

Tactic:
obtain ⟨m, hm, hm'⟩ := contra

Result:
case intro.intro.intro.intro
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
n : ℕ
hn : 0 < n
m : ℕ
hm : 0 < m
hm' : (x ^ n) ^ m = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1

Proof state:
case intro.intro.intro.intro
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
n : ℕ
hn : 0 < n
m : ℕ
hm : 0 < m
hm' : (x ^ n) ^ m = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1

Tactic:
exact ⟨n * m, mul_pos hn hm, by rwa [pow_mul]⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
n : ℕ
hn : 0 < n
m : ℕ
hm : 0 < m
hm' : (x ^ n) ^ m = 1
⊢ x ^ (n * m) = 1

Tactic:
rwa [pow_mul]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
⊢ {y | ¬IsOfFinOrder y}.Infinite

Tactic:
let s := { n | 0 < n }.image fun n : ℕ => x ^ n

Result:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
⊢ {y | ¬IsOfFinOrder y}.Infinite