-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem neZero' {n : ℕ} [NeZero n] (hζ : IsPrimitiveRoot ζ n) : NeZero ((n : ℕ) : R)

Proof state:
case pos.intro
R : Type u_4
ζ : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
p : ℕ := ringChar R
hfin : FiniteMultiplicity p n
m : ℕ
hm : n = p ^ multiplicity p n * m ∧ ¬p ∣ m
hp : p ∣ n
k : ℕ
hk : multiplicity p n = k.succ
this : NeZero p
⊢ NeZero ↑n

Tactic:
have hpri : Fact p.Prime := CharP.char_is_prime_of_pos R p

Result:
case pos.intro
R : Type u_4
ζ : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
p : ℕ := ringChar R
hfin : FiniteMultiplicity p n
m : ℕ
hm : n = p ^ multiplicity p n * m ∧ ¬p ∣ m
hp : p ∣ n
k : ℕ
hk : multiplicity p n = k.succ
this : NeZero p
hpri : Fact (Nat.Prime p)
⊢ NeZero ↑n

Proof state:
R : Type u_4
ζ : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
⊢ NeZero ↑n

Tactic:
let p := ringChar R

Result:
R : Type u_4
ζ : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
p : ℕ := ringChar R
⊢ NeZero ↑n

Proof state:
case pos.intro
R : Type u_4
ζ : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
p : ℕ := ringChar R
hfin : FiniteMultiplicity p n
m : ℕ
hm : n = p ^ multiplicity p n * m ∧ ¬p ∣ m
hp : p ∣ n
k : ℕ
hk : multiplicity p n = k.succ
this✝ : NeZero p
hpri : Fact (Nat.Prime p)
this : (frobenius R p) (ζ ^ (p ^ k * m)) = (frobenius R p) 1
⊢ False

Tactic:
have hpos : 0 < p ^ k * m :=
  mul_pos (pow_pos hpri.1.pos _) <| Nat.pos_of_ne_zero (fun H ↦ hm.2 <| H ▸ p.dvd_zero)

Result:
case pos.intro
R : Type u_4
ζ : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
p : ℕ := ringChar R
hfin : FiniteMultiplicity p n
m : ℕ
hm : n = p ^ multiplicity p n * m ∧ ¬p ∣ m
hp : p ∣ n
k : ℕ
hk : multiplicity p n = k.succ
this✝ : NeZero p
hpri : Fact (Nat.Prime p)
this : (frobenius R p) (ζ ^ (p ^ k * m)) = (frobenius R p) 1
hpos : 0 < p ^ k * m
⊢ False

Proof state:
case pos.intro
R : Type u_4
ζ : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
p : ℕ := ringChar R
hfin : FiniteMultiplicity p n
m : ℕ
hm : n = p ^ multiplicity p n * m ∧ ¬p ∣ m
hp : p ∣ n
k : ℕ
hk : multiplicity p n = k.succ
⊢ NeZero ↑n

Tactic:
have : NeZero p := NeZero.of_pos (Nat.pos_of_dvd_of_pos hp (NeZero.pos n))

Result:
case pos.intro
R : Type u_4
ζ : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
p : ℕ := ringChar R
hfin : FiniteMultiplicity p n
m : ℕ
hm : n = p ^ multiplicity p n * m ∧ ¬p ∣ m
hp : p ∣ n
k : ℕ
hk : multiplicity p n = k.succ
this : NeZero p
⊢ NeZero ↑n

Proof state:
case pos
R : Type u_4
ζ : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
p : ℕ := ringChar R
hfin : FiniteMultiplicity p n
m : ℕ
hm : n = p ^ multiplicity p n * m ∧ ¬p ∣ m
hp : p ∣ n
⊢ NeZero ↑n

Tactic:
obtain ⟨k, hk⟩ := Nat.exists_eq_succ_of_ne_zero (multiplicity_pos_of_dvd hp).ne'

Result:
case pos.intro
R : Type u_4
ζ : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
p : ℕ := ringChar R
hfin : FiniteMultiplicity p n
m : ℕ
hm : n = p ^ multiplicity p n * m ∧ ¬p ∣ m
hp : p ∣ n
k : ℕ
hk : multiplicity p n = k.succ
⊢ NeZero ↑n

Proof state:
case pos.intro
R : Type u_4
ζ : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
p : ℕ := ringChar R
hfin : FiniteMultiplicity p n
m : ℕ
hm : n = p ^ multiplicity p n * m ∧ ¬p ∣ m
hp : p ∣ n
k : ℕ
hk : multiplicity p n = k.succ
this✝ : NeZero p
hpri : Fact (Nat.Prime p)
this : (frobenius R p) (ζ ^ (p ^ k * m)) = (frobenius R p) 1
hpos : 0 < p ^ k * m
⊢ False

Tactic:
refine hζ.pow_ne_one_of_pos_of_lt hpos ?_ (frobenius_inj R p this)

Result:
case pos.intro
R : Type u_4
ζ : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
p : ℕ := ringChar R
hfin : FiniteMultiplicity p n
m : ℕ
hm : n = p ^ multiplicity p n * m ∧ ¬p ∣ m
hp : p ∣ n
k : ℕ
hk : multiplicity p n = k.succ
this✝ : NeZero p
hpri : Fact (Nat.Prime p)
this : (frobenius R p) (ζ ^ (p ^ k * m)) = (frobenius R p) 1
hpos : 0 < p ^ k * m
⊢ p ^ k * m < n

Proof state:
case pos.intro
R : Type u_4
ζ : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
p : ℕ := ringChar R
hfin : FiniteMultiplicity p n
m : ℕ
hm : n = p ^ multiplicity p n * m ∧ ¬p ∣ m
hp : p ∣ n
k : ℕ
hk : multiplicity p n = k.succ
this✝ : NeZero p
hpri : Fact (Nat.Prime p)
this : (frobenius R p) (ζ ^ (p ^ k * m)) = (frobenius R p) 1
hpos : 0 < p ^ k * m
⊢ p ^ k * m < p ^ k * m * p

Tactic:
exact lt_mul_of_one_lt_right hpos hpri.1.one_lt

Result:
no goals

Proof state:
R : Type u_4
ζ : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
p : ℕ := ringChar R
⊢ NeZero ↑n

Tactic:
have hfin := Nat.finiteMultiplicity_iff.2 ⟨CharP.char_ne_one R p, NeZero.pos n⟩

Result:
R : Type u_4
ζ : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
p : ℕ := ringChar R
hfin : FiniteMultiplicity p n
⊢ NeZero ↑n

Proof state:
R : Type u_4
ζ : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
p : ℕ := ringChar R
hfin : FiniteMultiplicity p n
⊢ NeZero ↑n

Tactic:
obtain ⟨m, hm⟩ := hfin.exists_eq_pow_mul_and_not_dvd

Result:
case intro
R : Type u_4
ζ : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
p : ℕ := ringChar R
hfin : FiniteMultiplicity p n
m : ℕ
hm : n = p ^ multiplicity p n * m ∧ ¬p ∣ m
⊢ NeZero ↑n

Proof state:
case pos.intro
R : Type u_4
ζ : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
p : ℕ := ringChar R
hfin : FiniteMultiplicity p n
m : ℕ
hm : n = p ^ multiplicity p n * m ∧ ¬p ∣ m
hp : p ∣ n
k : ℕ
hk : multiplicity p n = k.succ
this : NeZero p
hpri : Fact (Nat.Prime p)
⊢ NeZero ↑n

Tactic:
have := hζ.pow_eq_one

Result:
case pos.intro
R : Type u_4
ζ : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
p : ℕ := ringChar R
hfin : FiniteMultiplicity p n
m : ℕ
hm : n = p ^ multiplicity p n * m ∧ ¬p ∣ m
hp : p ∣ n
k : ℕ
hk : multiplicity p n = k.succ
this✝ : NeZero p
hpri : Fact (Nat.Prime p)
this : ζ ^ n = 1
⊢ NeZero ↑n

Proof state:
case pos.intro
R : Type u_4
ζ : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
p : ℕ := ringChar R
hfin : FiniteMultiplicity p n
m : ℕ
hm : n = p ^ multiplicity p n * m ∧ ¬p ∣ m
hp : p ∣ n
k : ℕ
hk : multiplicity p n = k.succ
this✝ : NeZero p
hpri : Fact (Nat.Prime p)
this : (frobenius R p) (ζ ^ (p ^ k * m)) = (frobenius R p) 1
hpos : 0 < p ^ k * m
⊢ p ^ k * m < n

Tactic:
rw [hm.1, hk, pow_succ', mul_assoc, mul_comm p]

Result:
case pos.intro
R : Type u_4
ζ : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
p : ℕ := ringChar R
hfin : FiniteMultiplicity p n
m : ℕ
hm : n = p ^ multiplicity p n * m ∧ ¬p ∣ m
hp : p ∣ n
k : ℕ
hk : multiplicity p n = k.succ
this✝ : NeZero p
hpri : Fact (Nat.Prime p)
this : (frobenius R p) (ζ ^ (p ^ k * m)) = (frobenius R p) 1
hpos : 0 < p ^ k * m
⊢ p ^ k * m < p ^ k * m * p

Proof state:
case neg
R : Type u_4
ζ : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
p : ℕ := ringChar R
hfin : FiniteMultiplicity p n
m : ℕ
hm : n = p ^ multiplicity p n * m ∧ ¬p ∣ m
hp : ¬p ∣ n
⊢ NeZero ↑n

Tactic:
exact NeZero.of_not_dvd R hp

Result:
no goals