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

State before:
p : ℕ
hpri : Fact p.Prime
n : CyclotomicIntegers p
hn : n ≠ 0
⊢ ∃ m, m ≠ 0 ∧ n ∣ ↑m
Tactic:
refine ⟨Algebra.norm ℤ ((equiv p) n), by simpa, ?_⟩
State after:
p : ℕ
hpri : Fact p.Prime
n : CyclotomicIntegers p
hn : n ≠ 0
⊢ n ∣ ↑((Algebra.norm ℤ) ((equiv p) n))

State before:
p : ℕ
hpri : Fact p.Prime
n : CyclotomicIntegers p
hn : n ≠ 0
⊢ n ∣ ↑((Algebra.norm ℤ) ((equiv p) n))
Tactic:
rw [← map_dvd_iff (equiv p), map_intCast]
State after:
p : ℕ
hpri : Fact p.Prime
n : CyclotomicIntegers p
hn : n ≠ 0
⊢ (equiv p) n ∣ ↑((Algebra.norm ℤ) ((equiv p) n))

State before:
p : ℕ
hpri : Fact p.Prime
n : CyclotomicIntegers p
hn : n ≠ 0
⊢ (equiv p) n ∣ ↑((Algebra.norm ℤ) ((equiv p) n))
Tactic:
convert RingOfIntegers.dvd_norm ℚ (equiv p n) using 1
State after:
case h.e'_4
p : ℕ
hpri : Fact p.Prime
n : CyclotomicIntegers p
hn : n ≠ 0
⊢ ↑((Algebra.norm ℤ) ((equiv p) n)) =
    (algebraMap (𝓞 ℚ) (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ((RingOfIntegers.norm ℚ) ((equiv p) n))

State before:
case h.e'_4
p : ℕ
hpri : Fact p.Prime
n : CyclotomicIntegers p
hn : n ≠ 0
⊢ ↑((Algebra.norm ℤ) ((equiv p) n)) =
    (algebraMap (𝓞 ℚ) (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ((RingOfIntegers.norm ℚ) ((equiv p) n))
Tactic:
ext1
State after:
case h.e'_4.h
p : ℕ
hpri : Fact p.Prime
n : CyclotomicIntegers p
hn : n ≠ 0
⊢ ↑↑((Algebra.norm ℤ) ((equiv p) n)) =
    ↑((algebraMap (𝓞 ℚ) (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ((RingOfIntegers.norm ℚ) ((equiv p) n)))

State before:
case h.e'_4.h
p : ℕ
hpri : Fact p.Prime
n : CyclotomicIntegers p
hn : n ≠ 0
⊢ ↑↑((Algebra.norm ℤ) ((equiv p) n)) =
    ↑((algebraMap (𝓞 ℚ) (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ((RingOfIntegers.norm ℚ) ((equiv p) n)))
Tactic:
exact DFunLike.congr_arg (algebraMap ℚ _) (Algebra.coe_norm_int (equiv p n))
State after:
no goals

State before:
p : ℕ
hpri : Fact p.Prime
n : CyclotomicIntegers p
hn : n ≠ 0
⊢ (Algebra.norm ℤ) ((equiv p) n) ≠ 0
Tactic:
simpa
State after:
no goals