-- Mathlib/NumberTheory/JacobiSum/Basic.lean
private
lemma MulChar.exists_apply_sub_one_mul_apply_sub_one {n : ℕ} [NeZero n] {χ ψ : MulChar F R}
    {μ : R} (hχ : χ ^ n = 1) (hψ : ψ ^ n = 1) (hμ : IsPrimitiveRoot μ n) (x : F) :
    ∃ z ∈ Algebra.adjoin ℤ {μ}, (χ x - 1) * (ψ (1 - x) - 1) = z * (μ - 1) ^ 2

Proof state:
case inr.inl
F : Type u_1
R : Type u_2
inst✝⁴ : Fintype F
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
hx₀ : 1 ≠ 0
⊢ ∃ z ∈ Algebra.adjoin ℤ {μ}, (χ 1 - 1) * (ψ (1 - 1) - 1) = z * (μ - 1) ^ 2

Tactic:
exact ⟨0, Subalgebra.zero_mem _, by rw [χ.map_one, sub_self, zero_mul, zero_mul]⟩

Result:
no goals

Proof state:
case inr.inr.intro.intro.intro.intro
F : Type u_1
R : Type u_2
inst✝⁴ : Fintype F
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
x : F
hx₀ : x ≠ 0
hx₁ : x ≠ 1
z₁ : R
hz₁ : z₁ ∈ Algebra.adjoin ℤ {μ}
Hz₁ : χ x - 1 = z₁ * (μ - 1)
z₂ : R
hz₂ : z₂ ∈ Algebra.adjoin ℤ {μ}
Hz₂ : ψ (1 - x) - 1 = z₂ * (μ - 1)
⊢ ∃ z ∈ Algebra.adjoin ℤ {μ}, z₁ * (μ - 1) * (z₂ * (μ - 1)) = z * ((μ - 1) * (μ - 1))

Tactic:
exact ⟨z₁ * z₂, Subalgebra.mul_mem _ hz₁ hz₂, mul_mul_mul_comm ..⟩

Result:
no goals

Proof state:
F : Type u_1
R : Type u_2
inst✝⁴ : Fintype F
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
x : F
⊢ ∃ z ∈ Algebra.adjoin ℤ {μ}, (χ x - 1) * (ψ (1 - x) - 1) = z * (μ - 1) ^ 2

Tactic:
rcases eq_or_ne x 0 with rfl | hx₀

Result:
case inl
F : Type u_1
R : Type u_2
inst✝⁴ : Fintype F
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
⊢ ∃ z ∈ Algebra.adjoin ℤ {μ}, (χ 0 - 1) * (ψ (1 - 0) - 1) = z * (μ - 1) ^ 2

case inr
F : Type u_1
R : Type u_2
inst✝⁴ : Fintype F
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
x : F
hx₀ : x ≠ 0
⊢ ∃ z ∈ Algebra.adjoin ℤ {μ}, (χ x - 1) * (ψ (1 - x) - 1) = z * (μ - 1) ^ 2

Proof state:
case inl
F : Type u_1
R : Type u_2
inst✝⁴ : Fintype F
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
⊢ ∃ z ∈ Algebra.adjoin ℤ {μ}, (χ 0 - 1) * (ψ (1 - 0) - 1) = z * (μ - 1) ^ 2

Tactic:
exact ⟨0, Subalgebra.zero_mem _, by rw [sub_zero, ψ.map_one, sub_self, mul_zero, zero_mul]⟩

Result:
no goals

Proof state:
case inr.inr.intro.intro
F : Type u_1
R : Type u_2
inst✝⁴ : Fintype F
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
x : F
hx₀ : x ≠ 0
hx₁ : x ≠ 1
z₁ : R
hz₁ : z₁ ∈ Algebra.adjoin ℤ {μ}
Hz₁ : χ x - 1 = z₁ * (μ - 1)
⊢ ∃ z ∈ Algebra.adjoin ℤ {μ}, (χ x - 1) * (ψ (1 - x) - 1) = z * (μ - 1) ^ 2

Tactic:
obtain ⟨z₂, hz₂, Hz₂⟩ :=
  MulChar.exists_apply_sub_one_eq_mul_sub_one hψ hμ (sub_ne_zero_of_ne hx₁.symm)

Result:
case inr.inr.intro.intro.intro.intro
F : Type u_1
R : Type u_2
inst✝⁴ : Fintype F
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
x : F
hx₀ : x ≠ 0
hx₁ : x ≠ 1
z₁ : R
hz₁ : z₁ ∈ Algebra.adjoin ℤ {μ}
Hz₁ : χ x - 1 = z₁ * (μ - 1)
z₂ : R
hz₂ : z₂ ∈ Algebra.adjoin ℤ {μ}
Hz₂ : ψ (1 - x) - 1 = z₂ * (μ - 1)
⊢ ∃ z ∈ Algebra.adjoin ℤ {μ}, (χ x - 1) * (ψ (1 - x) - 1) = z * (μ - 1) ^ 2

Proof state:
case inr.inr
F : Type u_1
R : Type u_2
inst✝⁴ : Fintype F
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
x : F
hx₀ : x ≠ 0
hx₁ : x ≠ 1
⊢ ∃ z ∈ Algebra.adjoin ℤ {μ}, (χ x - 1) * (ψ (1 - x) - 1) = z * (μ - 1) ^ 2

Tactic:
obtain ⟨z₁, hz₁, Hz₁⟩ := MulChar.exists_apply_sub_one_eq_mul_sub_one hχ hμ hx₀

Result:
case inr.inr.intro.intro
F : Type u_1
R : Type u_2
inst✝⁴ : Fintype F
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
x : F
hx₀ : x ≠ 0
hx₁ : x ≠ 1
z₁ : R
hz₁ : z₁ ∈ Algebra.adjoin ℤ {μ}
Hz₁ : χ x - 1 = z₁ * (μ - 1)
⊢ ∃ z ∈ Algebra.adjoin ℤ {μ}, (χ x - 1) * (ψ (1 - x) - 1) = z * (μ - 1) ^ 2

Proof state:
case inr.inr.intro.intro.intro.intro
F : Type u_1
R : Type u_2
inst✝⁴ : Fintype F
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
x : F
hx₀ : x ≠ 0
hx₁ : x ≠ 1
z₁ : R
hz₁ : z₁ ∈ Algebra.adjoin ℤ {μ}
Hz₁ : χ x - 1 = z₁ * (μ - 1)
z₂ : R
hz₂ : z₂ ∈ Algebra.adjoin ℤ {μ}
Hz₂ : ψ (1 - x) - 1 = z₂ * (μ - 1)
⊢ ∃ z ∈ Algebra.adjoin ℤ {μ}, (χ x - 1) * (ψ (1 - x) - 1) = z * (μ - 1) ^ 2

Tactic:
rewrite [Hz₁, Hz₂, sq]

Result:
case inr.inr.intro.intro.intro.intro
F : Type u_1
R : Type u_2
inst✝⁴ : Fintype F
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
x : F
hx₀ : x ≠ 0
hx₁ : x ≠ 1
z₁ : R
hz₁ : z₁ ∈ Algebra.adjoin ℤ {μ}
Hz₁ : χ x - 1 = z₁ * (μ - 1)
z₂ : R
hz₂ : z₂ ∈ Algebra.adjoin ℤ {μ}
Hz₂ : ψ (1 - x) - 1 = z₂ * (μ - 1)
⊢ ∃ z ∈ Algebra.adjoin ℤ {μ}, z₁ * (μ - 1) * (z₂ * (μ - 1)) = z * ((μ - 1) * (μ - 1))

Proof state:
F : Type u_1
R : Type u_2
inst✝⁴ : Fintype F
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
⊢ (χ 0 - 1) * (ψ (1 - 0) - 1) = 0 * (μ - 1) ^ 2

Tactic:
rw [sub_zero, ψ.map_one, sub_self, mul_zero, zero_mul]

Result:
no goals

Proof state:
case inr
F : Type u_1
R : Type u_2
inst✝⁴ : Fintype F
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
x : F
hx₀ : x ≠ 0
⊢ ∃ z ∈ Algebra.adjoin ℤ {μ}, (χ x - 1) * (ψ (1 - x) - 1) = z * (μ - 1) ^ 2

Tactic:
rcases eq_or_ne x 1 with rfl | hx₁

Result:
case inr.inl
F : Type u_1
R : Type u_2
inst✝⁴ : Fintype F
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
hx₀ : 1 ≠ 0
⊢ ∃ z ∈ Algebra.adjoin ℤ {μ}, (χ 1 - 1) * (ψ (1 - 1) - 1) = z * (μ - 1) ^ 2

case inr.inr
F : Type u_1
R : Type u_2
inst✝⁴ : Fintype F
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
x : F
hx₀ : x ≠ 0
hx₁ : x ≠ 1
⊢ ∃ z ∈ Algebra.adjoin ℤ {μ}, (χ x - 1) * (ψ (1 - x) - 1) = z * (μ - 1) ^ 2

Proof state:
F : Type u_1
R : Type u_2
inst✝⁴ : Fintype F
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
hx₀ : 1 ≠ 0
⊢ (χ 1 - 1) * (ψ (1 - 1) - 1) = 0 * (μ - 1) ^ 2

Tactic:
rw [χ.map_one, sub_self, zero_mul, zero_mul]

Result:
no goals