case inl
α✝ : Type ?u.76176
β : Type ?u.76179
γ : Type ?u.76182
δ : Type ?u.76185
α : Type u_1
inst✝ : Monoid α
x : α
n : ℕ
hn✝ : n ≠ 1
hn : n < 1
⊢ Irreducible (x ^ n) → IsUnit x

case inr
α✝ : Type ?u.76176
β : Type ?u.76179
γ : Type ?u.76182
δ : Type ?u.76185
α : Type u_1
inst✝ : Monoid α
x : α
n : ℕ
hn✝ : n ≠ 1
hn : 1 < n
⊢ Irreducible (x ^ n) → IsUnit x
α✝ : Type ?u.76176
β : Type ?u.76179
γ : Type ?u.76182
δ : Type ?u.76185
α : Type u_1
inst✝ : Monoid α
x : α
n : ℕ
hn : n ≠ 1
⊢ Irreducible (x ^ n) → IsUnit x
obtain hn | hn := hn.lt_or_lt
case inr
α✝ : Type ?u.76176
β : Type ?u.76179
γ : Type ?u.76182
δ : Type ?u.76185
α : Type u_1
inst✝ : Monoid α
x : α
n : ℕ
hn✝ : n ≠ 1
hn : 1 < n
h : Irreducible (x ^ n)
⊢ IsUnit x
case inr
α✝ : Type ?u.76176
β : Type ?u.76179
γ : Type ?u.76182
δ : Type ?u.76185
α : Type u_1
inst✝ : Monoid α
x : α
n : ℕ
hn✝ : n ≠ 1
hn : 1 < n
⊢ Irreducible (x ^ n) → IsUnit x
intro h
case inr.intro
α✝ : Type ?u.76176
β : Type ?u.76179
γ : Type ?u.76182
δ : Type ?u.76185
α : Type u_1
inst✝ : Monoid α
x : α
k : ℕ
hn✝ : 1 + k + 1 ≠ 1
hn : 1 < 1 + k + 1
h : Irreducible (x ^ (1 + k + 1))
⊢ IsUnit x
case inr
α✝ : Type ?u.76176
β : Type ?u.76179
γ : Type ?u.76182
δ : Type ?u.76185
α : Type u_1
inst✝ : Monoid α
x : α
n : ℕ
hn✝ : n ≠ 1
hn : 1 < n
h : Irreducible (x ^ n)
⊢ IsUnit x
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_lt hn
case inr.intro
α✝ : Type ?u.76176
β : Type ?u.76179
γ : Type ?u.76182
δ : Type ?u.76185
α : Type u_1
inst✝ : Monoid α
x : α
k : ℕ
hn✝ : 1 + k + 1 ≠ 1
hn : 1 < 1 + k + 1
h : Irreducible (x * x ^ (k + 1))
⊢ IsUnit x
case inr.intro
α✝ : Type ?u.76176
β : Type ?u.76179
γ : Type ?u.76182
δ : Type ?u.76185
α : Type u_1
inst✝ : Monoid α
x : α
k : ℕ
hn✝ : 1 + k + 1 ≠ 1
hn : 1 < 1 + k + 1
h : Irreducible (x ^ (1 + k + 1))
⊢ IsUnit x
rw [pow_succ, add_comm] at h
no goals
case inr.intro
α✝ : Type ?u.76176
β : Type ?u.76179
γ : Type ?u.76182
δ : Type ?u.76185
α : Type u_1
inst✝ : Monoid α
x : α
k : ℕ
hn✝ : 1 + k + 1 ≠ 1
hn : 1 < 1 + k + 1
h : Irreducible (x * x ^ (k + 1))
⊢ IsUnit x
exact (or_iff_left_of_imp isUnit_pow_succ_iff.mp).mp (of_irreducible_mul h)
no goals
case inl
α✝ : Type ?u.76176
β : Type ?u.76179
γ : Type ?u.76182
δ : Type ?u.76185
α : Type u_1
inst✝ : Monoid α
x : α
n : ℕ
hn✝ : n ≠ 1
hn : n < 1
⊢ Irreducible (x ^ n) → IsUnit x
simp only [Nat.lt_one_iff.mp hn, IsEmpty.forall_iff, not_irreducible_one, pow_zero]