awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
R : Type u_2
inst : Field F
inst_1 : Fintype F
inst_2 : CommRing R
inst_3 : IsDomain R
χ φ : MulChar F R
h : χ * φ ≠ 1
ψ : AddChar F R
sum_eq :
  ∀ (t : F),
    Membership.mem (γ := Finset F) (univ \ {0}) t →
      HMul.hMul (α := R) (β := R)
          (∑ x : F, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((φ : (a : F) → R) (t - x) : R) : R)
          ((ψ : (a : F) → R) t : R) =
        HMul.hMul (α := R) (β := R)
          (∑ y : F, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) (t * y) : R) ((φ : (a : F) → R) (t - t * y) : R) : R)
          ((ψ : (a : F) → R) t : R)
conv :
  gaussSum (χ * φ) ψ * jacobiSum χ φ =
    ∑ t ∈ univ \ {0},
      HMul.hMul (α := R) (β := R)
        (∑ x : F,
            HMul.hMul (α := R) ((χ : (a : F) → R) t : R)
              (HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) ((φ : (a : F) → R) t : R) ((χ : (a : F) → R) x : R))
                ((φ : (a : F) → R) (1 - x) : R)) :
          R)
        ((ψ : (a : F) → R) t : R)
⊢ gaussSum (χ * φ) ψ * jacobiSum χ φ =
    ∑ x ∈ univ \ {0},
      HMul.hMul (α := R) (β := R)
        (∑ x_1 : F,
            HMul.hMul (α := R) ((χ : (a : F) → R) x : R)
              (HMul.hMul (α := R) ((χ : (a : F) → R) x_1 : R)
                (HMul.hMul (α := R) (β := R) ((φ : (a : F) → R) x : R) ((φ : (a : F) → R) (1 - x_1) : R))) :
          R)
        ((ψ : (a : F) → R) x : R)

Tactic:
conv => enter [2, 2, t, 1, 2, x, 2]; rw [← mul_assoc, mul_comm (χ x) (φ t)]

Premises used: mul_assoc
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
R : Type u_2
inst : Field F
inst_1 : Fintype F
inst_2 : CommRing R
inst_3 : IsDomain R
χ φ : MulChar F R
h : χ * φ ≠ 1
ψ : AddChar F R
sum_eq :
  ∀ (t : F),
    Membership.mem (γ := Finset F) (univ \ {0}) t →
      HMul.hMul (α := R) (β := R)
          (∑ x : F, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((φ : (a : F) → R) (t - x) : R) : R)
          ((ψ : (a : F) → R) t : R) =
        HMul.hMul (α := R) (β := R)
          (∑ y : F, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) (t * y) : R) ((φ : (a : F) → R) (t - t * y) : R) : R)
          ((ψ : (a : F) → R) t : R)
simp_rw :
  gaussSum (χ * φ) ψ * jacobiSum χ φ =
    ∑ x ∈ univ \ {0},
      HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) x : R) ((ψ : (a : F) → R) x : R) *
        ∑ i : F, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) i : R) ((φ : (a : F) → R) (1 - i) : R)
⊢ gaussSum (χ * φ) ψ * jacobiSum χ φ =
    ∑ t ∈ univ \ {0},
      HMul.hMul (α := R) (β := R)
        (∑ x : F,
            HMul.hMul (α := R) ((χ : (a : F) → R) t : R)
              (HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) ((φ : (a : F) → R) t : R) ((χ : (a : F) → R) x : R))
                ((φ : (a : F) → R) (1 - x) : R)) :
          R)
        ((ψ : (a : F) → R) t : R)

Tactic:
simp_rw [← mul_assoc, ← MulChar.mul_apply, mul_assoc, ← mul_sum, mul_right_comm]

Premises used: Finset.mul_sum, mul_assoc, MulChar.mul_apply, mul_right_comm
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
R : Type u_2
inst : Field F
inst_1 : Fintype F
inst_2 : CommRing R
inst_3 : IsDomain R
χ φ : MulChar F R
h : χ * φ ≠ 1
ψ : AddChar F R
sum_eq :
  ∀ (t : F),
    Membership.mem (γ := Finset F) (univ \ {0}) t →
      HMul.hMul (α := R) (β := R)
          (∑ x : F, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((φ : (a : F) → R) (t - x) : R) : R)
          ((ψ : (a : F) → R) t : R) =
        HMul.hMul (α := R) (β := R)
          (∑ y : F, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) (t * y) : R) ((φ : (a : F) → R) (t - t * y) : R) : R)
          ((ψ : (a : F) → R) t : R)
rw :
  gaussSum (χ * φ) ψ * jacobiSum χ φ =
    ∑ x ∈ univ \ {0},
      HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) x : R) ((ψ : (a : F) → R) x : R) * jacobiSum χ φ
rw₁ :
  gaussSum (χ * φ) ψ * jacobiSum χ φ =
    (∑ i ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) i : R) ((ψ : (a : F) → R) i : R)) *
      jacobiSum χ φ
rw₂ :
  (∑ a : F, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) a : R) ((ψ : (a : F) → R) a : R)) * jacobiSum χ φ =
    (∑ i ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) i : R) ((ψ : (a : F) → R) i : R)) *
      jacobiSum χ φ
rw₃ :
  (∑ x ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) x : R) ((ψ : (a : F) → R) x : R) +
        HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) 0 : R) ((ψ : (a : F) → R) 0 : R)) *
      jacobiSum χ φ =
    (∑ i ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) i : R) ((ψ : (a : F) → R) i : R)) *
      jacobiSum χ φ
rw₄ :
  (∑ x ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) x : R) ((ψ : (a : F) → R) x : R) +
        HMul.hMul (α := R) (β := R) (0 : R) ((ψ : (a : F) → R) 0 : R)) *
      jacobiSum χ φ =
    (∑ i ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) i : R) ((ψ : (a : F) → R) i : R)) *
      jacobiSum χ φ
rw₅ :
  HAdd.hAdd (α := R)
        (∑ x ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) x : R) ((ψ : (a : F) → R) x : R)) 0 *
      jacobiSum χ φ =
    (∑ i ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) i : R) ((ψ : (a : F) → R) i : R)) *
      jacobiSum χ φ
rw₆ rw₇ :
  (∑ x ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) x : R) ((ψ : (a : F) → R) x : R)) *
      jacobiSum χ φ =
    (∑ i ∈ univ \ {0}, HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) i : R) ((ψ : (a : F) → R) i : R)) *
      jacobiSum χ φ
⊢ gaussSum (χ * φ) ψ * jacobiSum χ φ =
    ∑ x ∈ univ \ {0},
      HMul.hMul (α := R) (β := R) ((χ * φ : (a : F) → R) x : R) ((ψ : (a : F) → R) x : R) *
        ∑ i : F, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) i : R) ((φ : (a : F) → R) (1 - i) : R)

Tactic:
rw [← jacobiSum, ← sum_mul, gaussSum, sum_eq_sum_diff_singleton_add (mem_univ (0 : F)),
    (χ * φ).map_zero, zero_mul, add_zero]

Premises used: Finset.mem_univ, HMul.hMul, MulZeroClass.zero_mul, Finset.sum_eq_sum_diff_singleton_add, jacobiSum, gaussSum, add_zero, OfNat.ofNat, MulChar.map_zero, Finset.sum_mul
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
F' : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : Field F'
h : Ne.{u_2 + 1} (α := F') (↑(Fintype.card F) : F') 0
χ φ : MulChar F F'
hχφ : χ * φ ≠ 1
ψ : AddChar F F'
hψ : AddChar.IsPrimitive.{u_1, u_2} (R := F) (R' := F') ψ
rw : gaussSum (χ * φ) ψ * jacobiSum χ φ = gaussSum χ ψ * gaussSum φ ψ
⊢ jacobiSum χ φ = gaussSum χ ψ * gaussSum φ ψ / gaussSum (χ * φ) ψ

Tactic:
rw [eq_div_iff <| gaussSum_ne_zero_of_nontrivial h hχφ hψ, mul_comm]

Premises used: mul_comm, gaussSum_ne_zero_of_nontrivial, eq_div_iff
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
F' : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : Field F'
h : Ne.{u_2 + 1} (α := F') (↑(Fintype.card F) : F') 0
χ φ : MulChar F F'
hχφ : χ * φ ≠ 1
ψ : AddChar F F'
hψ : AddChar.IsPrimitive.{u_1, u_2} (R := F) (R' := F') ψ
⊢ gaussSum (χ * φ) ψ * jacobiSum χ φ = gaussSum χ ψ * gaussSum φ ψ

Tactic:
jacobiSum_mul_nontrivial hχφ ψ

Premises used: jacobiSum_mul_nontrivial
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
F' : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : Field F'
h : Ne.{u_2 + 1} (α := F') (↑(Fintype.card F) : F') 0
χ φ : MulChar F F'
hχφ : χ * φ ≠ 1
ψ : AddChar F F'
hψ : AddChar.IsPrimitive.{u_1, u_2} (R := F) (R' := F') ψ
⊢ gaussSum (χ * φ) ψ * jacobiSum χ φ = gaussSum χ ψ * gaussSum φ ψ

Tactic:
exact jacobiSum_mul_nontrivial hχφ ψ

Premises used: jacobiSum_mul_nontrivial
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
F' : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
obtain :
  ∀ (n : ℕ+) (hp : Nat.Prime (ringChar F)) (hc : Fintype.card F = ringChar F ^ (↑n : ℕ)),
    jacobiSum χ φ * jacobiSum χ⁻¹ φ⁻¹ = (↑(Fintype.card F) : F')
⊢ jacobiSum χ φ * jacobiSum χ⁻¹ φ⁻¹ = (↑(Fintype.card F) : F')

Tactic:
obtain ⟨n, hp, hc⟩ := FiniteField.card F (ringChar F)

Premises used: FiniteField.card, ringChar
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
F' : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n : ℕ) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
⊢ Function.Injective (α := F') (β := FF') (⇑(algebraMap F' FF' : F' →+* FF') : (a : F') → FF')

Tactic:
have hinj := (algebraMap F' FF').injective
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
F' : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n : ℕ) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective (α := F') (β := FF') (⇑(algebraMap F' FF' : F' →+* FF') : (a : F') → FF')
a :
  Eq (α := FF') (((algebraMap F' FF' : F' →+* FF') : (a : F') → FF') (jacobiSum χ φ * jacobiSum χ⁻¹ φ⁻¹) : FF')
    (((algebraMap F' FF' : F' →+* FF') : (a : F') → FF') (↑(Fintype.card F) : F') : FF')
⊢ jacobiSum χ φ * jacobiSum χ⁻¹ φ⁻¹ = (↑(Fintype.card F) : F')

Tactic:
apply hinj
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
F' : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n : ℕ) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective (α := F') (β := FF') (⇑(algebraMap F' FF' : F' →+* FF') : (a : F') → FF')
a :
  jacobiSum (χ.ringHomComp (algebraMap F' FF')) (φ.ringHomComp (algebraMap F' FF')) *
      jacobiSum (χ⁻¹.ringHomComp (algebraMap F' FF')) (φ⁻¹.ringHomComp (algebraMap F' FF')) =
    ((algebraMap F' FF' : F' →+* FF') : (a : F') → FF') (↑(Fintype.card F) : F')
⊢ Eq (α := FF') (((algebraMap F' FF' : F' →+* FF') : (a : F') → FF') (jacobiSum χ φ * jacobiSum χ⁻¹ φ⁻¹) : FF')
    (((algebraMap F' FF' : F' →+* FF') : (a : F') → FF') (↑(Fintype.card F) : F') : FF')

Tactic:
rw [map_mul, ← jacobiSum_ringHomComp, ← jacobiSum_ringHomComp]

Premises used: map_mul, jacobiSum_ringHomComp
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
F' : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n : ℕ) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective (α := F') (β := FF') (⇑(algebraMap F' FF' : F' →+* FF') : (a : F') → FF')
rw : (χ * φ).ringHomComp (algebraMap F' FF') ≠ 1
⊢ χ' * φ' ≠ 1

Tactic:
rw [← ringHomComp_mul]

Premises used: MulChar.ringHomComp_mul
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
F' : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n : ℕ) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective (α := F') (β := FF') (⇑(algebraMap F' FF' : F' →+* FF') : (a : F') → FF')
⊢ (χ * φ).ringHomComp (algebraMap F' FF') ≠ 1

Tactic:
(MulChar.ringHomComp_ne_one_iff hinj).mpr hχφ

Premises used: Iff.mpr, MulChar.ringHomComp_ne_one_iff
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
F' : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n : ℕ) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective (α := F') (β := FF') (⇑(algebraMap F' FF' : F' →+* FF') : (a : F') → FF')
⊢ (χ * φ).ringHomComp (algebraMap F' FF') ≠ 1

Tactic:
exact (MulChar.ringHomComp_ne_one_iff hinj).mpr hχφ

Premises used: Iff.mpr, MulChar.ringHomComp_ne_one_iff
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
F' : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n : ℕ) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective (α := F') (β := FF') (⇑(algebraMap F' FF' : F' →+* FF') : (a : F') → FF')
⊢ χ' * φ' ≠ 1

Tactic:
have Hχφ : χ' * φ' ≠ 1 := by
    rw [← ringHomComp_mul]
    exact (MulChar.ringHomComp_ne_one_iff hinj).mpr hχφ
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
F' : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n : ℕ) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective (α := F') (β := FF') (⇑(algebraMap F' FF' : F' →+* FF') : (a : F') → FF')
Hχφ : χ' * φ' ≠ 1
rwa : (χ' * φ')⁻¹ ≠ 1
rwa₁ rwa₂ rwa₃ rwa₄ : χ' * φ' ≠ 1
⊢ χ'⁻¹ * φ'⁻¹ ≠ 1

Tactic:
rwa [← mul_inv, inv_ne_one]

Premises used: inv_ne_one, mul_inv
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
F' : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n : ℕ) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective (α := F') (β := FF') (⇑(algebraMap F' FF' : F' →+* FF') : (a : F') → FF')
Hχφ : χ' * φ' ≠ 1
⊢ χ'⁻¹ * φ'⁻¹ ≠ 1

Tactic:
have Hχφ' : χ'⁻¹ * φ'⁻¹ ≠ 1 := by
    rwa [← mul_inv, inv_ne_one]
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
F' : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n : ℕ) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective (α := F') (β := FF') (⇑(algebraMap F' FF' : F' →+* FF') : (a : F') → FF')
Hχφ : χ' * φ' ≠ 1
Hχφ' : χ'⁻¹ * φ'⁻¹ ≠ 1
⊢ χ' ≠ 1

Tactic:
have Hχ : χ' ≠ 1 := (MulChar.ringHomComp_ne_one_iff hinj).mpr hχ
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
F' : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n : ℕ) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective (α := F') (β := FF') (⇑(algebraMap F' FF' : F' →+* FF') : (a : F') → FF')
Hχφ : χ' * φ' ≠ 1
Hχφ' : χ'⁻¹ * φ'⁻¹ ≠ 1
Hχ : χ' ≠ 1
⊢ φ' ≠ 1

Tactic:
have Hφ : φ' ≠ 1 := (MulChar.ringHomComp_ne_one_iff hinj).mpr hφ
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
F' : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n : ℕ) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective (α := F') (β := FF') (⇑(algebraMap F' FF' : F' →+* FF') : (a : F') → FF')
Hχφ : χ' * φ' ≠ 1
Hχφ' : χ'⁻¹ * φ'⁻¹ ≠ 1
Hχ : χ' ≠ 1
Hφ : φ' ≠ 1
H : Eq.{u_2 + 1} (α := FF') (↑(Fintype.card F) : FF') 0
⊢ Eq.{u_2 + 1} (α := FF') (↑(ringChar F) : FF') 0

Tactic:
simp only [hc, Nat.cast_pow, ne_eq, PNat.ne_zero, not_false_eq_true, pow_eq_zero_iff] at H

Premises used: pow_eq_zero_iff, PNat.ne_zero, ne_eq, Nat.cast_pow, not_false_eq_true
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
F' : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n : ℕ) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective (α := F') (β := FF') (⇑(algebraMap F' FF' : F' →+* FF') : (a : F') → FF')
Hχφ : χ' * φ' ≠ 1
Hχφ' : χ'⁻¹ * φ'⁻¹ ≠ 1
Hχ : χ' ≠ 1
Hφ : φ' ≠ 1
H : Eq.{u_2 + 1} (α := FF') (↑(ringChar F) : FF') 0
⊢ False

Tactic:
h <| (Algebra.ringChar_eq F' FF').trans <| CharP.ringChar_of_prime_eq_zero hp H

Premises used: Algebra.ringChar_eq, CharP.ringChar_of_prime_eq_zero, Eq.trans
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
F' : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n : ℕ) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective (α := F') (β := FF') (⇑(algebraMap F' FF' : F' →+* FF') : (a : F') → FF')
Hχφ : χ' * φ' ≠ 1
Hχφ' : χ'⁻¹ * φ'⁻¹ ≠ 1
Hχ : χ' ≠ 1
Hφ : φ' ≠ 1
H : Eq.{u_2 + 1} (α := FF') (↑(ringChar F) : FF') 0
⊢ False

Tactic:
exact h <| (Algebra.ringChar_eq F' FF').trans <| CharP.ringChar_of_prime_eq_zero hp H

Premises used: Algebra.ringChar_eq, CharP.ringChar_of_prime_eq_zero, Eq.trans
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
F' : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n : ℕ) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective (α := F') (β := FF') (⇑(algebraMap F' FF' : F' →+* FF') : (a : F') → FF')
Hχφ : χ' * φ' ≠ 1
Hχφ' : χ'⁻¹ * φ'⁻¹ ≠ 1
Hχ : χ' ≠ 1
Hφ : φ' ≠ 1
⊢ Ne.{u_2 + 1} (α := FF') (↑(Fintype.card F) : FF') 0

Tactic:
have Hcard : (Fintype.card F : FF') ≠ 0 := by
    intro H
    simp only [hc, Nat.cast_pow, ne_eq, PNat.ne_zero, not_false_eq_true, pow_eq_zero_iff] at H
    exact h <| (Algebra.ringChar_eq F' FF').trans <| CharP.ringChar_of_prime_eq_zero hp H
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
F' : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n : ℕ) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective (α := F') (β := FF') (⇑(algebraMap F' FF' : F' →+* FF') : (a : F') → FF')
Hχφ : χ' * φ' ≠ 1
Hχφ' : χ'⁻¹ * φ'⁻¹ ≠ 1
Hχ : χ' ≠ 1
Hφ : φ' ≠ 1
Hcard : Ne.{u_2 + 1} (α := FF') (↑(Fintype.card F) : FF') 0
⊢ gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ ≠ 0

Tactic:
have H := (gaussSum_mul_gaussSum_eq_card Hχφ ψ.prim).trans_ne Hcard
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
F' : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n : ℕ) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective (α := F') (β := FF') (⇑(algebraMap F' FF' : F' →+* FF') : (a : F') → FF')
Hχφ : χ' * φ' ≠ 1
Hχφ' : χ'⁻¹ * φ'⁻¹ ≠ 1
Hχ : χ' ≠ 1
Hφ : φ' ≠ 1
Hcard : Ne.{u_2 + 1} (α := FF') (↑(Fintype.card F) : FF') 0
H : gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ ≠ 0
⊢ Function.Injective (β := FF') fun (x : FF') ↦ gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ * x

Tactic:
mul_right_injective₀ H

Premises used: mul_right_injective₀
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
F' : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ (↑n : ℕ)
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n : ℕ) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective (α := F') (β := FF') (⇑(algebraMap F' FF' : F' →+* FF') : (a : F') → FF')
Hχφ : χ' * φ' ≠ 1
Hχφ' : χ'⁻¹ * φ'⁻¹ ≠ 1
Hχ : χ' ≠ 1
Hφ : φ' ≠ 1
Hcard : Ne.{u_2 + 1} (α := FF') (↑(Fintype.card F) : FF') 0
H : gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ ≠ 0
a :
  Eq.{u_2 + 1} (α := FF')
    ((fun (x : FF') ↦ gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ * x)
      (jacobiSum (χ.ringHomComp (algebraMap F' FF')) (φ.ringHomComp (algebraMap F' FF')) *
        jacobiSum (χ⁻¹.ringHomComp (algebraMap F' FF')) (φ⁻¹.ringHomComp (algebraMap F' FF'))))
    ((fun (x : FF') ↦ gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ * x)
      (((algebraMap F' FF' : F' →+* FF') : (a : F') → FF') (↑(Fintype.card F) : F')))
⊢ jacobiSum (χ.ringHomComp (algebraMap F' FF')) (φ.ringHomComp (algebraMap F' FF')) *
      jacobiSum (χ⁻¹.ringHomComp (algebraMap F' FF')) (φ⁻¹.ringHomComp (algebraMap F' FF')) =
    ((algebraMap F' FF' : F' →+* FF') : (a : F') → FF') (↑(Fintype.card F) : F')

Tactic:
apply_fun (gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ * ·)
    using mul_right_injective₀ H

Premises used: HMul.hMul, mul_right_injective₀, AddChar.PrimitiveAddChar.char, Inv.inv, gaussSum