Theorem: CyclotomicIntegers.equiv_zeta (FltRegular/NumberTheory/CyclotomicRing.lean)

State before:
p : ℕ
hpri : Fact p.Prime
⊢ (equiv p) (zeta p) = ⋯.toInteger
Tactic:
letI p' : ℕ+ := ⟨p, hpri.out.pos⟩
State after:
p : ℕ
hpri : Fact p.Prime
p' : ℕ+ := ⟨p, ⋯⟩
⊢ (equiv p) (zeta p) = ⋯.toInteger

State before:
p : ℕ
hpri : Fact p.Prime
p' : ℕ+ := ⟨p, ⋯⟩
⊢ (equiv p) (zeta p) = ⋯.toInteger
Tactic:
letI : Fact (Nat.Prime p') := hpri
State after:
p : ℕ
hpri : Fact p.Prime
p' : ℕ+ := ⟨p, ⋯⟩
this : Fact (↑p').Prime := hpri
⊢ (equiv p) (zeta p) = ⋯.toInteger

State before:
p : ℕ
hpri : Fact p.Prime
p' : ℕ+ := ⟨p, ⋯⟩
this : Fact (↑p').Prime := hpri
⊢ (equiv p) (zeta p) = ⋯.toInteger
Tactic:
rw [equiv_apply, zeta]
State after:
p : ℕ
hpri : Fact p.Prime
p' : ℕ+ := ⟨p, ⋯⟩
this : Fact (↑p').Prime := hpri
⊢ (AdjoinRoot.liftHom (cyclotomic p ℤ) ⋯.toInteger ⋯) (AdjoinRoot.root (cyclotomic p ℤ)) = ⋯.toInteger

State before:
p : ℕ
hpri : Fact p.Prime
p' : ℕ+ := ⟨p, ⋯⟩
this : Fact (↑p').Prime := hpri
⊢ (AdjoinRoot.liftHom (cyclotomic p ℤ) ⋯.toInteger ⋯) (AdjoinRoot.root (cyclotomic p ℤ)) = ⋯.toInteger
Tactic:
simp only [AdjoinRoot.liftHom_root, IsPrimitiveRoot.integralPowerBasis'_gen]
State after:
no goals