G : Type u
A : Type v
x y : G
a b : A
n✝ m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
n : ℕ
h : 0 < n
⊢ (if h : 1 ∈ periodicPts fun x_1 => x * x_1 then Nat.find h else 0) = n ↔
    IsPeriodicPt (fun x_1 => x * x_1) n 1 ∧ ∀ (m : ℕ), m < n → 0 < m → ¬IsPeriodicPt (fun x_1 => x * x_1) m 1
G : Type u
A : Type v
x y : G
a b : A
n✝ m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
n : ℕ
h : 0 < n
⊢ orderOf x = n ↔ x ^ n = 1 ∧ ∀ (m : ℕ), m < n → 0 < m → x ^ m ≠ 1
simp_rw [Ne, ← isPeriodicPt_mul_iff_pow_eq_one, orderOf, minimalPeriod]
case inl
G : Type u
A : Type v
x y : G
a b : A
n✝ m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
n : ℕ
h : 0 < n
h1 : 1 ∈ periodicPts fun x_1 => x * x_1
⊢ Nat.find h1 = n ↔
    IsPeriodicPt (fun x_1 => x * x_1) n 1 ∧ ∀ (m : ℕ), m < n → 0 < m → ¬IsPeriodicPt (fun x_1 => x * x_1) m 1

case inr
G : Type u
A : Type v
x y : G
a b : A
n✝ m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
n : ℕ
h : 0 < n
h1 : ¬1 ∈ periodicPts fun x_1 => x * x_1
⊢ 0 = n ↔ IsPeriodicPt (fun x_1 => x * x_1) n 1 ∧ ∀ (m : ℕ), m < n → 0 < m → ¬IsPeriodicPt (fun x_1 => x * x_1) m 1
G : Type u
A : Type v
x y : G
a b : A
n✝ m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
n : ℕ
h : 0 < n
⊢ (if h : 1 ∈ periodicPts fun x_1 => x * x_1 then Nat.find h else 0) = n ↔
    IsPeriodicPt (fun x_1 => x * x_1) n 1 ∧ ∀ (m : ℕ), m < n → 0 < m → ¬IsPeriodicPt (fun x_1 => x * x_1) m 1
split_ifs with h1
no goals
case inl
G : Type u
A : Type v
x y : G
a b : A
n✝ m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
n : ℕ
h : 0 < n
h1 : 1 ∈ periodicPts fun x_1 => x * x_1
⊢ Nat.find h1 = n ↔
    IsPeriodicPt (fun x_1 => x * x_1) n 1 ∧ ∀ (m : ℕ), m < n → 0 < m → ¬IsPeriodicPt (fun x_1 => x * x_1) m 1
classical
rw [find_eq_iff]
simp only [h, true_and]
push_neg
rfl
case inl
G : Type u
A : Type v
x y : G
a b : A
n✝ m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
n : ℕ
h : 0 < n
h1 : 1 ∈ periodicPts fun x_1 => x * x_1
⊢ ((n > 0 ∧ IsPeriodicPt (fun x_1 => x * x_1) n 1) ∧
      ∀ (n_1 : ℕ), n_1 < n → ¬(n_1 > 0 ∧ IsPeriodicPt (fun x_1 => x * x_1) n_1 1)) ↔
    IsPeriodicPt (fun x_1 => x * x_1) n 1 ∧ ∀ (m : ℕ), m < n → 0 < m → ¬IsPeriodicPt (fun x_1 => x * x_1) m 1
case inl
G : Type u
A : Type v
x y : G
a b : A
n✝ m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
n : ℕ
h : 0 < n
h1 : 1 ∈ periodicPts fun x_1 => x * x_1
⊢ Nat.find h1 = n ↔
    IsPeriodicPt (fun x_1 => x * x_1) n 1 ∧ ∀ (m : ℕ), m < n → 0 < m → ¬IsPeriodicPt (fun x_1 => x * x_1) m 1
rw [find_eq_iff]
case inl
G : Type u
A : Type v
x y : G
a b : A
n✝ m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
n : ℕ
h : 0 < n
h1 : 1 ∈ periodicPts fun x_1 => x * x_1
⊢ (IsPeriodicPt (fun x_1 => x * x_1) n 1 ∧
      ∀ (n_1 : ℕ), n_1 < n → ¬(n_1 > 0 ∧ IsPeriodicPt (fun x_1 => x * x_1) n_1 1)) ↔
    IsPeriodicPt (fun x_1 => x * x_1) n 1 ∧ ∀ (m : ℕ), m < n → 0 < m → ¬IsPeriodicPt (fun x_1 => x * x_1) m 1
case inl
G : Type u
A : Type v
x y : G
a b : A
n✝ m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
n : ℕ
h : 0 < n
h1 : 1 ∈ periodicPts fun x_1 => x * x_1
⊢ ((n > 0 ∧ IsPeriodicPt (fun x_1 => x * x_1) n 1) ∧
      ∀ (n_1 : ℕ), n_1 < n → ¬(n_1 > 0 ∧ IsPeriodicPt (fun x_1 => x * x_1) n_1 1)) ↔
    IsPeriodicPt (fun x_1 => x * x_1) n 1 ∧ ∀ (m : ℕ), m < n → 0 < m → ¬IsPeriodicPt (fun x_1 => x * x_1) m 1
simp only [h, true_and]
case inl
G : Type u
A : Type v
x y : G
a b : A
n✝ m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
n : ℕ
h : 0 < n
h1 : 1 ∈ periodicPts fun x_1 => x * x_1
⊢ (IsPeriodicPt (fun x_1 => x * x_1) n 1 ∧ ∀ (n_1 : ℕ), n_1 < n → n_1 > 0 → ¬IsPeriodicPt (fun x_1 => x * x_1) n_1 1) ↔
    IsPeriodicPt (fun x_1 => x * x_1) n 1 ∧ ∀ (m : ℕ), m < n → 0 < m → ¬IsPeriodicPt (fun x_1 => x * x_1) m 1
case inl
G : Type u
A : Type v
x y : G
a b : A
n✝ m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
n : ℕ
h : 0 < n
h1 : 1 ∈ periodicPts fun x_1 => x * x_1
⊢ (IsPeriodicPt (fun x_1 => x * x_1) n 1 ∧
      ∀ (n_1 : ℕ), n_1 < n → ¬(n_1 > 0 ∧ IsPeriodicPt (fun x_1 => x * x_1) n_1 1)) ↔
    IsPeriodicPt (fun x_1 => x * x_1) n 1 ∧ ∀ (m : ℕ), m < n → 0 < m → ¬IsPeriodicPt (fun x_1 => x * x_1) m 1
push_neg
no goals
case inl
G : Type u
A : Type v
x y : G
a b : A
n✝ m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
n : ℕ
h : 0 < n
h1 : 1 ∈ periodicPts fun x_1 => x * x_1
⊢ (IsPeriodicPt (fun x_1 => x * x_1) n 1 ∧ ∀ (n_1 : ℕ), n_1 < n → n_1 > 0 → ¬IsPeriodicPt (fun x_1 => x * x_1) n_1 1) ↔
    IsPeriodicPt (fun x_1 => x * x_1) n 1 ∧ ∀ (m : ℕ), m < n → 0 < m → ¬IsPeriodicPt (fun x_1 => x * x_1) m 1
rfl
case inr
G : Type u
A : Type v
x y : G
a b : A
n✝ m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
n : ℕ
h : 0 < n
h1 : ¬1 ∈ periodicPts fun x_1 => x * x_1
⊢ ¬(IsPeriodicPt (fun x_1 => x * x_1) n 1 ∧ ∀ (m : ℕ), m < n → 0 < m → ¬IsPeriodicPt (fun x_1 => x * x_1) m 1)
case inr
G : Type u
A : Type v
x y : G
a b : A
n✝ m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
n : ℕ
h : 0 < n
h1 : ¬1 ∈ periodicPts fun x_1 => x * x_1
⊢ 0 = n ↔ IsPeriodicPt (fun x_1 => x * x_1) n 1 ∧ ∀ (m : ℕ), m < n → 0 < m → ¬IsPeriodicPt (fun x_1 => x * x_1) m 1
rw [iff_false_left h.ne]
case inr.intro
G : Type u
A : Type v
x y : G
a b : A
n✝ m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
n : ℕ
h : 0 < n
h1 : ¬1 ∈ periodicPts fun x_1 => x * x_1
h' : IsPeriodicPt (fun x_1 => x * x_1) n 1
⊢ False
case inr
G : Type u
A : Type v
x y : G
a b : A
n✝ m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
n : ℕ
h : 0 < n
h1 : ¬1 ∈ periodicPts fun x_1 => x * x_1
⊢ ¬(IsPeriodicPt (fun x_1 => x * x_1) n 1 ∧ ∀ (m : ℕ), m < n → 0 < m → ¬IsPeriodicPt (fun x_1 => x * x_1) m 1)
rintro ⟨h', -⟩
no goals
case inr.intro
G : Type u
A : Type v
x y : G
a b : A
n✝ m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
n : ℕ
h : 0 < n
h1 : ¬1 ∈ periodicPts fun x_1 => x * x_1
h' : IsPeriodicPt (fun x_1 => x * x_1) n 1
⊢ False
exact h1 ⟨n, h, h'⟩