-- Mathlib/NumberTheory/MulChar/Lemmas.lean
/-- The values of a multiplicative character `χ` such that `χ^n = 1` are contained in `ℤ[μ]` when
`μ` is a primitive `n`th root of unity. -/
lemma apply_mem_algebraAdjoin_of_pow_eq_one {χ : MulChar F R} {n : ℕ} [NeZero n] (hχ : χ ^ n = 1)
    {μ : R} (hμ : IsPrimitiveRoot μ n) (a : F) :
    χ a ∈ Algebra.adjoin ℤ {μ}

Proof state:
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Finite F
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
χ : MulChar F R
n : ℕ
inst✝ : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
⊢ χ a ∈ Algebra.adjoin ℤ {μ}

Tactic:
rcases eq_or_ne a 0 with rfl | h

Result:
case inl
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Finite F
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
χ : MulChar F R
n : ℕ
inst✝ : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
⊢ χ 0 ∈ Algebra.adjoin ℤ {μ}

case inr
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Finite F
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
χ : MulChar F R
n : ℕ
inst✝ : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
h : a ≠ 0
⊢ χ a ∈ Algebra.adjoin ℤ {μ}

Proof state:
case inr
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Finite F
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
χ : MulChar F R
n : ℕ
inst✝ : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
h : a ≠ 0
⊢ χ a ∈ Algebra.adjoin ℤ {μ}

Tactic:
obtain ⟨ζ, hζ₁, hζ₂⟩ := apply_mem_rootsOfUnity_of_pow_eq_one hχ h

Result:
case inr.intro.intro
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Finite F
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
χ : MulChar F R
n : ℕ
inst✝ : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
h : a ≠ 0
ζ : Rˣ
hζ₁ : ζ ∈ rootsOfUnity n R
hζ₂ : ↑ζ = χ a
⊢ χ a ∈ Algebra.adjoin ℤ {μ}

Proof state:
case inr.intro.intro.intro.intro
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Finite F
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
χ : MulChar F R
n : ℕ
inst✝ : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
h : a ≠ 0
ζ : Rˣ
hζ₁ : ↑ζ ^ n = ↑1
hζ₂ : ↑ζ = χ a
k : ℕ
left✝ : k < n
hk : μ ^ k = ↑ζ
⊢ χ a ∈ Algebra.adjoin ℤ {μ}

Tactic:
exact hζ₂ ▸ hk ▸ Subalgebra.pow_mem _ (Algebra.self_mem_adjoin_singleton ℤ μ) k

Result:
no goals

Proof state:
case inr.intro.intro
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Finite F
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
χ : MulChar F R
n : ℕ
inst✝ : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
h : a ≠ 0
ζ : Rˣ
hζ₁ : ↑ζ ^ n = ↑1
hζ₂ : ↑ζ = χ a
⊢ χ a ∈ Algebra.adjoin ℤ {μ}

Tactic:
obtain ⟨k, _, hk⟩ := IsPrimitiveRoot.eq_pow_of_pow_eq_one hμ hζ₁

Result:
case inr.intro.intro.intro.intro
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Finite F
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
χ : MulChar F R
n : ℕ
inst✝ : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
h : a ≠ 0
ζ : Rˣ
hζ₁ : ↑ζ ^ n = ↑1
hζ₂ : ↑ζ = χ a
k : ℕ
left✝ : k < n
hk : μ ^ k = ↑ζ
⊢ χ a ∈ Algebra.adjoin ℤ {μ}

Proof state:
case inr.intro.intro
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Finite F
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
χ : MulChar F R
n : ℕ
inst✝ : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
h : a ≠ 0
ζ : Rˣ
hζ₁ : ζ ∈ rootsOfUnity n R
hζ₂ : ↑ζ = χ a
⊢ χ a ∈ Algebra.adjoin ℤ {μ}

Tactic:
rw [mem_rootsOfUnity, Units.ext_iff, Units.val_pow_eq_pow_val] at hζ₁

Result:
case inr.intro.intro
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Finite F
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
χ : MulChar F R
n : ℕ
inst✝ : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
h : a ≠ 0
ζ : Rˣ
hζ₁ : ↑ζ ^ n = ↑1
hζ₂ : ↑ζ = χ a
⊢ χ a ∈ Algebra.adjoin ℤ {μ}

Proof state:
case inl
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Finite F
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
χ : MulChar F R
n : ℕ
inst✝ : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
⊢ χ 0 ∈ Algebra.adjoin ℤ {μ}

Tactic:
exact χ.map_zero ▸ Subalgebra.zero_mem _

Result:
no goals