awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
R : Type u_2
inst : CommRing F
inst_1 : Nontrivial F
inst_2 : Fintype F
inst_3 : DecidableEq F
inst_4 : CommRing R
χ ψ : MulChar F R
rw :
  HAdd.hAdd (α := R) (∑ x : F, (χ : (a : F) → R) x) (∑ i : F, (ψ : (a : F) → R) i) - ∑ x : F, 1 +
      HSub.hSub (α := R)
        (∑ x : F,
          HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
            HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R))
        0 =
    HAdd.hAdd (α := R) (∑ x : F, (χ : (a : F) → R) x) (∑ x : F, (ψ : (a : F) → R) x) - ∑ x : F, 1 +
      HSub.hSub (α := R)
        (∑ x : F,
          HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
            HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R))
        (∑ x ∈ {0, 1},
          HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
            HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R))
⊢ HAdd.hAdd (α := R) (∑ x : F, (χ : (a : F) → R) x)
          (∑ x : F, (ψ : (a : F) → R) ((Equiv.subLeft 1 : (a : F) → F) x : F)) -
        ∑ x : F, 1 +
      ∑ x : F,
        HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
          HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R) =
    HAdd.hAdd (α := R) (∑ x : F, (χ : (a : F) → R) x) (∑ x : F, (ψ : (a : F) → R) x) - (↑(Fintype.card F) : R) +
      ∑ x ∈ univ \ {0, 1},
        HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
          HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R)

Tactic:
rw [(Equiv.subLeft 1).sum_comp ψ, Fintype.card_eq_sum_ones, Nat.cast_sum, Nat.cast_one,
    sum_sdiff_eq_sub (subset_univ _), ← sub_zero (_ - _ + _), add_sub_assoc]

Premises used: add_sub_assoc, Equiv.subLeft, sub_zero, Equiv.sum_comp, Finset.sum_sdiff_eq_sub, HSub.hSub, Fintype.card_eq_sum_ones, Nat.cast_sum, HAdd.hAdd, OfNat.ofNat, Nat.cast_one, DFunLike.coe, Finset.subset_univ
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
R : Type u_2
inst : CommRing F
inst_1 : Nontrivial F
inst_2 : Fintype F
inst_3 : DecidableEq F
inst_4 : CommRing R
χ ψ : MulChar F R
e_a :
  Eq.{u_2 + 1} (α := R) 0
    (∑ x ∈ {0, 1},
      HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
        HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R))
⊢ HAdd.hAdd (α := R) (∑ x : F, (χ : (a : F) → R) x) (∑ i : F, (ψ : (a : F) → R) i) - ∑ x : F, 1 +
      HSub.hSub (α := R)
        (∑ x : F,
          HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
            HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R))
        0 =
    HAdd.hAdd (α := R) (∑ x : F, (χ : (a : F) → R) x) (∑ x : F, (ψ : (a : F) → R) x) - ∑ x : F, 1 +
      HSub.hSub (α := R)
        (∑ x : F,
          HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
            HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R))
        (∑ x ∈ {0, 1},
          HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
            HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R))

Tactic:
congr
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
R : Type u_2
inst : CommRing F
inst_1 : Nontrivial F
inst_2 : Fintype F
inst_3 : DecidableEq F
inst_4 : CommRing R
χ ψ : MulChar F R
e_a :
  0 =
    HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) 0 : R) (1 : R) *
        HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (HSub.hSub (α := F) 1 0) : R) (1 : R) +
      HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) 1 : R) (1 : R) *
        HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (HSub.hSub (α := F) 1 1) : R) (1 : R)
e_a₁ :
  0 =
    HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) 0 : R) (1 : R) *
        HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) 1 : R) (1 : R) +
      HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) 1 : R) (1 : R) *
        HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (HSub.hSub (α := F) 1 1) : R) (1 : R)
e_a₂ :
  0 =
    HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) 0 : R) (1 : R) * HSub.hSub (α := R) 1 1 +
      HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) 1 : R) (1 : R) *
        HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (HSub.hSub (α := F) 1 1) : R) (1 : R)
e_a₃ :
  0 =
    HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) 0 : R) (1 : R) * HSub.hSub (α := R) 1 1 +
      HSub.hSub (α := R) 1 1 * HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (HSub.hSub (α := F) 1 1) : R) (1 : R)
e_a₄ :
  0 =
    HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) 0 : R) (1 : R) * 0 +
      0 * HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (HSub.hSub (α := F) 1 1) : R) (1 : R)
e_a₅ : 0 = 0 + 0 * HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (HSub.hSub (α := F) 1 1) : R) (1 : R)
e_a₆ : 0 = HAdd.hAdd (α := R) 0 0
e_a₇ e_a₈ : Eq.{u_2 + 1} (α := R) 0 0
⊢ Eq.{u_2 + 1} (α := R) 0
    (∑ x ∈ {0, 1},
      HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) x : R) (1 : R) *
        HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (1 - x) : R) (1 : R))

Tactic:
rw [sum_pair zero_ne_one, sub_zero, ψ.map_one, χ.map_one, sub_self, mul_zero, zero_mul, add_zero]

Premises used: MulChar.map_one, Finset.sum_pair, sub_self, sub_zero, MulZeroClass.zero_mul, zero_ne_one, MulZeroClass.mul_zero, add_zero
-- 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
rw :
  ∑ x ∈ univ \ {0, 1},
      HMul.hMul (α := R) (β := R) ((MulChar.trivial F R : (a : F) → R) x : R)
        ((MulChar.trivial F R : (a : F) → R) (1 - x) : R) =
    HSub.hSub (α := R) (↑(Fintype.card F) : R) 2
⊢ jacobiSum (MulChar.trivial F R) (MulChar.trivial F R) = HSub.hSub (α := R) (↑(Fintype.card F) : R) 2

Tactic:
rw [jacobiSum_eq_sum_sdiff]

Premises used: jacobiSum_eq_sum_sdiff
-- 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
x : F
hx : Membership.mem (γ := Finset F) (univ \ {0, 1}) x
hc : IsUnit (x * (1 - x))
⊢ HMul.hMul (α := R) (β := R) ((MulChar.trivial F R : (a : F) → R) x : R)
      ((MulChar.trivial F R : (a : F) → R) (1 - x) : R) =
    1

Tactic:
rw [← map_mul, MulChar.trivial_apply, if_pos]

Premises used: if_pos, map_mul, MulChar.trivial_apply
-- 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
x : F
hx : Membership.mem (γ := Finset F) (univ \ {0, 1}) x
⊢ x ≠ 0 ∧ x ≠ 1

Tactic:
simp only [mem_sdiff, mem_univ, mem_insert, mem_singleton, not_or, ← ne_eq, true_and] at hx

Premises used: Finset.mem_univ, Finset.mem_singleton, Finset.mem_insert, ne_eq, not_or, Finset.mem_sdiff, true_and
-- 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
x : F
hx : x ≠ 0 ∧ x ≠ 1
⊢ IsUnit (x * (1 - x))

Tactic:
simpa only [isUnit_iff_ne_zero, mul_ne_zero_iff, ne_eq, sub_eq_zero, @eq_comm _ _ x] using hx

Premises used: sub_eq_zero, isUnit_iff_ne_zero, eq_comm, ne_eq, mul_ne_zero_iff
-- 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
⊢ ∀ (x : F),
    Membership.mem (γ := Finset F) (univ \ {0, 1}) x →
      HMul.hMul (α := R) (β := R) ((MulChar.trivial F R : (a : F) → R) x : R)
          ((MulChar.trivial F R : (a : F) → R) (1 - x) : R) =
        1

Tactic:
have : ∀ x ∈ univ \ {0, 1}, (MulChar.trivial F R) x * (MulChar.trivial F R) (1 - x) = 1 := by
    intro x hx
    rw [← map_mul, MulChar.trivial_apply, if_pos]
    simp only [mem_sdiff, mem_univ, mem_insert, mem_singleton, not_or, ← ne_eq, true_and] at hx
    simpa only [isUnit_iff_ne_zero, mul_ne_zero_iff, ne_eq, sub_eq_zero, @eq_comm _ _ x] using hx
-- 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
this :
  ∀ (x : F),
    Membership.mem (γ := Finset F) (univ \ {0, 1}) x →
      HMul.hMul (α := R) (β := R) ((MulChar.trivial F R : (a : F) → R) x : R)
          ((MulChar.trivial F R : (a : F) → R) (1 - x) : R) =
        1
⊢ Eq.{u_2 + 1} (α := R)
    (∑ x ∈ univ \ {0, 1},
      HMul.hMul (α := R) (β := R) ((MulChar.trivial F R : (a : F) → R) x : R)
        ((MulChar.trivial F R : (a : F) → R) (1 - x) : R))
    (∑ x ∈ univ \ {0, 1}, 1)

Tactic:
sum_congr rfl this

Premises used: Finset.sum_congr, rfl
-- 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
this :
  ∀ (x : F),
    Membership.mem (γ := Finset F) (univ \ {0, 1}) x →
      HMul.hMul (α := R) (β := R) ((MulChar.trivial F R : (a : F) → R) x : R)
          ((MulChar.trivial F R : (a : F) → R) (1 - x) : R) =
        1
⊢ Eq.{u_2 + 1} (α := R) (∑ x ∈ univ \ {0, 1}, 1) (↑(card (α := F) (univ \ {0, 1})) : R)

Tactic:
(cast_card _).symm

Premises used: Eq.symm, Finset.cast_card
-- 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
this :
  ∀ (x : F),
    Membership.mem (γ := Finset F) (univ \ {0, 1}) x →
      HMul.hMul (α := R) (β := R) ((MulChar.trivial F R : (a : F) → R) x : R)
          ((MulChar.trivial F R : (a : F) → R) (1 - x) : R) =
        1
rw : (↑(card.{u_1} (α := F) univ - card (α := F) {0, 1}) : R) = HSub.hSub (α := R) (↑(Fintype.card F) : R) 2
rw₁ : (↑(Fintype.card F - card (α := F) {0, 1}) : R) = HSub.hSub (α := R) (↑(Fintype.card F) : R) 2
rw₂ : (↑(Fintype.card F - 2) : R) = HSub.hSub (α := R) (↑(Fintype.card F) : R) 2
rw₃ :
  HSub.hSub (α := R) (↑(Fintype.card F) : R) (↑(HAdd.hAdd (α := ℕ) 1 1) : R) =
    HSub.hSub (α := R) (↑(Fintype.card F) : R) 2
rw₄ rw₅ : HSub.hSub (α := R) (↑(Fintype.card F) : R) 2 = HSub.hSub (α := R) (↑(Fintype.card F) : R) 2
⊢ (↑(card (α := F) (univ \ {0, 1})) : R) = HSub.hSub (α := R) (↑(Fintype.card F) : R) 2

Tactic:
rw [card_sdiff_of_subset (subset_univ _), card_univ, card_pair zero_ne_one,
      Nat.cast_sub <| Nat.add_one_le_of_lt Fintype.one_lt_card, Nat.cast_two]

Premises used: Finset.card_univ, Fintype.one_lt_card, Nat.cast_sub, Finset.card_sdiff_of_subset, zero_ne_one, Nat.add_one_le_of_lt, Finset.card_pair, Nat.cast_two, Finset.subset_univ
-- 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
this :
  ∀ (x : F),
    Membership.mem (γ := Finset F) (univ \ {0, 1}) x →
      HMul.hMul (α := R) (β := R) ((MulChar.trivial F R : (a : F) → R) x : R)
          ((MulChar.trivial F R : (a : F) → R) (1 - x) : R) =
        1
calc : (↑(card (α := F) (univ \ {0, 1})) : R) = HSub.hSub (α := R) (↑(Fintype.card F) : R) 2
⊢ ∑ x ∈ univ \ {0, 1},
      HMul.hMul (α := R) (β := R) ((MulChar.trivial F R : (a : F) → R) x : R)
        ((MulChar.trivial F R : (a : F) → R) (1 - x) : R) =
    HSub.hSub (α := R) (↑(Fintype.card F) : R) 2

Tactic:
calc ∑ x ∈ univ \ {0, 1}, (MulChar.trivial F R) x * (MulChar.trivial F R) (1 - x)
  _ = ∑ _ ∈ univ \ {0, 1}, 1 := sum_congr rfl this
  _ = #(univ \ {0, 1}) := (cast_card _).symm
  _ = Fintype.card F - 2 := by
    rw [card_sdiff_of_subset (subset_univ _), card_univ, card_pair zero_ne_one,
      Nat.cast_sub <| Nat.add_one_le_of_lt Fintype.one_lt_card, Nat.cast_two]

Premises used: Finset.univ, Fintype.card, Insert.insert, SDiff.sdiff, Singleton.singleton, OfNat.ofNat, Eq.symm, Finset.cast_card, Finset.sum_congr, rfl
-- 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
rw rw₁ rw₂ :
  ∑ x ∈ univ \ {0, 1},
      HMul.hMul (α := R) (β := R) ((MulChar.trivial F R : (a : F) → R) x : R)
        ((MulChar.trivial F R : (a : F) → R) (1 - x) : R) =
    HSub.hSub (α := R) (↑(Fintype.card F) : R) 2
rw₃ :
  ∀
    (this :
      ∀ (x : F),
        Membership.mem (γ := Finset F) (univ \ {0, 1}) x →
          HMul.hMul (α := R) (β := R) ((MulChar.trivial F R : (a : F) → R) x : R)
              ((MulChar.trivial F R : (a : F) → R) (1 - x) : R) =
            1),
    ∑ x ∈ univ \ {0, 1},
        HMul.hMul (α := R) (β := R) ((MulChar.trivial F R : (a : F) → R) x : R)
          ((MulChar.trivial F R : (a : F) → R) (1 - x) : R) =
      HSub.hSub (α := R) (↑(Fintype.card F) : R) 2
⊢ jacobiSum (MulChar.trivial F R) (MulChar.trivial F R) = HSub.hSub (α := R) (↑(Fintype.card F) : R) 2

Tactic:
classical
  rw [jacobiSum_eq_sum_sdiff]
  have : ∀ x ∈ univ \ {0, 1}, (MulChar.trivial F R) x * (MulChar.trivial F R) (1 - x) = 1 := by
    intro x hx
    rw [← map_mul, MulChar.trivial_apply, if_pos]
    simp only [mem_sdiff, mem_univ, mem_insert, mem_singleton, not_or, ← ne_eq, true_and] at hx
    simpa only [isUnit_iff_ne_zero, mul_ne_zero_iff, ne_eq, sub_eq_zero, @eq_comm _ _ x] using hx
  calc ∑ x ∈ univ \ {0, 1}, (MulChar.trivial F R) x * (MulChar.trivial F R) (1 - x)
  _ = ∑ _ ∈ univ \ {0, 1}, 1 := sum_congr rfl this
  _ = #(univ \ {0, 1}) := (cast_card _).symm
  _ = Fintype.card F - 2 := by
    rw [card_sdiff_of_subset (subset_univ _), card_univ, card_pair zero_ne_one,
      Nat.cast_sub <| Nat.add_one_le_of_lt Fintype.one_lt_card, Nat.cast_two]

Premises used: Finset.univ, Fintype.card, Insert.insert, SDiff.sdiff, jacobiSum_eq_sum_sdiff, Singleton.singleton, OfNat.ofNat, Eq.symm, Finset.cast_card
-- 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
⊢ jacobiSum.{u_1, u_2} (R := F) 1 1 = HSub.hSub (α := R) (↑(Fintype.card F) : R) 2

Tactic:
jacobiSum_trivial_trivial

Premises used: jacobiSum_trivial_trivial
-- 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
h :
  ∀ (x : F),
    Membership.mem (γ := Finset F) (univ \ {0, 1}) x →
      HSub.hSub (α := R) (β := R) ((1 : (a : F) → R) x : R) (1 : R) *
          HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) (1 - x) : R) (1 : R) =
        0
⊢ Eq.{u_2 + 1} (α := R)
    (∑ x ∈ univ \ {0, 1},
      HSub.hSub (α := R) (β := R) ((1 : (a : F) → R) x : R) (1 : R) *
        HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) (1 - x) : R) (1 : R))
    0

Tactic:
apply Finset.sum_eq_zero

Premises used: Finset.sum_eq_zero
-- 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
⊢ ∀ (x : F),
    Membership.mem (γ := Finset F) (univ \ {0, 1}) x →
      HSub.hSub (α := R) (β := R) ((1 : (a : F) → R) x : R) (1 : R) *
          HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) (1 - x) : R) (1 : R) =
        0

Tactic:
simp +contextual only [mem_sdiff, mem_univ, mem_insert, mem_singleton,
      not_or, ← isUnit_iff_ne_zero, true_and, MulChar.one_apply, sub_self, zero_mul,
      implies_true]

Premises used: Finset.mem_univ, Finset.mem_singleton, sub_self, MulZeroClass.zero_mul, Finset.mem_insert, isUnit_iff_ne_zero, not_or, Finset.mem_sdiff, MulChar.one_apply, implies_true, true_and
-- 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
⊢ Eq.{u_2 + 1} (α := R)
    (∑ x ∈ univ \ {0, 1},
      HSub.hSub (α := R) (β := R) ((1 : (a : F) → R) x : R) (1 : R) *
        HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) (1 - x) : R) (1 : R))
    0

Tactic:
have : ∑ x ∈ univ \ {0, 1}, ((1 : MulChar F R) x - 1) * (χ (1 - x) - 1) = 0 := by
    apply Finset.sum_eq_zero
    simp +contextual only [mem_sdiff, mem_univ, mem_insert, mem_singleton,
      not_or, ← isUnit_iff_ne_zero, true_and, MulChar.one_apply, sub_self, zero_mul,
      implies_true]
-- 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
this :
  Eq.{u_2 + 1} (α := R)
    (∑ x ∈ univ \ {0, 1},
      HSub.hSub (α := R) (β := R) ((1 : (a : F) → R) x : R) (1 : R) *
        HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) (1 - x) : R) (1 : R))
    0
⊢ jacobiSum 1 χ = -1

Tactic:
simp only [jacobiSum_eq_aux, MulChar.sum_one_eq_card_units, MulChar.sum_eq_zero_of_ne_one hχ,
    add_zero, Fintype.card_eq_card_units_add_one (α := F), Nat.cast_add, Nat.cast_one,
    sub_add_cancel_left, this]

Premises used: MulChar.sum_one_eq_card_units, sub_add_cancel_left, _private.0.jacobiSum_eq_aux, Nat.cast_add, Fintype.card_eq_card_units_add_one, add_zero, Nat.cast_one, MulChar.sum_eq_zero_of_ne_one
-- 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
have :
  Eq.{u_2 + 1} (α := R)
    (∑ x ∈ univ \ {0, 1},
      HSub.hSub (α := R) (β := R) ((1 : (a : F) → R) x : R) (1 : R) *
        HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) (1 - x) : R) (1 : R))
    0
have₁ :
  ∀
    (this :
      Eq.{u_2 + 1} (α := R)
        (∑ x ∈ univ \ {0, 1},
          HSub.hSub (α := R) (β := R) ((1 : (a : F) → R) x : R) (1 : R) *
            HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) (1 - x) : R) (1 : R))
        0),
    jacobiSum 1 χ = -1
have₂ :
  Eq.{u_2 + 1} (α := R)
    (∑ x ∈ univ \ {0, 1},
      HSub.hSub (α := R) (β := R) ((1 : (a : F) → R) x : R) (1 : R) *
        HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) (1 - x) : R) (1 : R))
    0
have₃ have₄ :
  ∀
    (this :
      Eq.{u_2 + 1} (α := R)
        (∑ x ∈ univ \ {0, 1},
          HSub.hSub (α := R) (β := R) ((1 : (a : F) → R) x : R) (1 : R) *
            HSub.hSub (α := R) (β := R) ((χ : (a : F) → R) (1 - x) : R) (1 : R))
        0),
    jacobiSum 1 χ = -1
⊢ jacobiSum 1 χ = -1

Tactic:
classical
  have : ∑ x ∈ univ \ {0, 1}, ((1 : MulChar F R) x - 1) * (χ (1 - x) - 1) = 0 := by
    apply Finset.sum_eq_zero
    simp +contextual only [mem_sdiff, mem_univ, mem_insert, mem_singleton,
      not_or, ← isUnit_iff_ne_zero, true_and, MulChar.one_apply, sub_self, zero_mul,
      implies_true]
  simp only [jacobiSum_eq_aux, MulChar.sum_one_eq_card_units, MulChar.sum_eq_zero_of_ne_one hχ,
    add_zero, Fintype.card_eq_card_units_add_one (α := F), Nat.cast_add, Nat.cast_one,
    sub_add_cancel_left, this]

Premises used: MulChar.sum_one_eq_card_units, sub_add_cancel_left, _private.0.jacobiSum_eq_aux, Nat.cast_add, add_zero, Nat.cast_one, MulChar.sum_eq_zero_of_ne_one
-- 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
h : ∀ (x : F), HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((χ⁻¹ : (a : F) → R) (1 - x) : R)
| Eq.{u_2 + 1} (α := R)
    (∑ x : F, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((χ⁻¹ : (a : F) → R) (1 - x) : R) : R)
    (-(χ : (a : F) → R) (-1) : R)

Tactic:
enter [1, 2, x]
-- 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
x : F
h : ((χ : (a : F) → R) (x / (1 - x)) : R)
| HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((χ⁻¹ : (a : F) → R) (1 - x) : R)

Tactic:
rw [MulChar.inv_apply', ← map_mul, ← div_eq_mul_inv]

Premises used: div_eq_mul_inv, map_mul, MulChar.inv_apply'
-- 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
h : ∀ (x : F), ((χ : (a : F) → R) (x / (1 - x)) : R)
| Eq.{u_2 + 1} (α := R)
    (∑ x : F, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((χ⁻¹ : (a : F) → R) (1 - x) : R) : R)
    (-(χ : (a : F) → R) (-1) : R)

Tactic:
enter [1, 2, x]; rw [MulChar.inv_apply', ← map_mul, ← div_eq_mul_inv]

Premises used: div_eq_mul_inv, map_mul, MulChar.inv_apply'
-- 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
conv : Eq.{u_2 + 1} (α := R) (∑ x : F, (χ : (a : F) → R) (x / (1 - x)) : R) (-(χ : (a : F) → R) (-1) : R)
⊢ Eq.{u_2 + 1} (α := R)
    (∑ x : F, HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((χ⁻¹ : (a : F) → R) (1 - x) : R) : R)
    (-(χ : (a : F) → R) (-1) : R)

Tactic:
conv => enter [1, 2, x]; rw [MulChar.inv_apply', ← map_mul, ← div_eq_mul_inv]

Premises used: div_eq_mul_inv, map_mul, MulChar.inv_apply'
-- 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
rw : Eq.{u_2 + 1} (α := R) (∑ x ∈ univ \ {1}, (χ : (a : F) → R) (x / (1 - x)) : R) (-(χ : (a : F) → R) (-1) : R)
⊢ Eq.{u_2 + 1} (α := R) (∑ x : F, (χ : (a : F) → R) (x / (1 - x)) : R) (-(χ : (a : F) → R) (-1) : R)

Tactic:
rw [sum_eq_sum_diff_singleton_add (mem_univ (1 : F)), sub_self, div_zero, χ.map_zero, add_zero]

Premises used: Finset.mem_univ, sub_self, Finset.sum_eq_sum_diff_singleton_add, add_zero, OfNat.ofNat, MulChar.map_zero, div_zero
-- 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
⊢ Eq.{u_2 + 1} (α := R) (∑ x ∈ univ \ {1}, (χ : (a : F) → R) (x / (1 - x))) (∑ x ∈ univ \ {-1}, (χ : (a : F) → R) x)

Tactic:
sum_bij' (fun a _ ↦ a / (1 - a)) (fun b _ ↦ b / (1 + b)) (fun x hx ↦ ?_)
      (fun y hy ↦ ?_) (fun x hx ↦ ?_) (fun y hy ↦ ?_) (fun _ _ ↦ rfl)

Premises used: HSub.hSub, HDiv.hDiv, HAdd.hAdd, Finset.sum_bij', OfNat.ofNat, rfl
-- 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
refine_1 :
  ∀ (x : F) (hx : Membership.mem (γ := Finset F) (univ \ {1}) x),
    Membership.mem (γ := Finset F) (univ \ {-1})
      ((fun (a : F) (x : Membership.mem (γ := Finset F) (univ \ {1}) a) ↦ a / (1 - a)) x hx)
refine_2 :
  ∀ (y : F) (hy : Membership.mem (γ := Finset F) (univ \ {-1}) y),
    Membership.mem (γ := Finset F) (univ \ {1})
      ((fun (b : F) (x : Membership.mem (γ := Finset F) (univ \ {-1}) b) ↦ b / (1 + b)) y hy)
refine_3 :
  ∀ (x : F) (hx : Membership.mem (γ := Finset F) (univ \ {1}) x),
    (fun (b : F) (x : Membership.mem (γ := Finset F) (univ \ {-1}) b) ↦ b / (1 + b))
        ((fun (a : F) (x : Membership.mem (γ := Finset F) (univ \ {1}) a) ↦ a / (1 - a)) x hx) ⋯ =
      x
refine_4 :
  ∀ (y : F) (hy : Membership.mem (γ := Finset F) (univ \ {-1}) y),
    (fun (a : F) (x : Membership.mem (γ := Finset F) (univ \ {1}) a) ↦ a / (1 - a))
        ((fun (b : F) (x : Membership.mem (γ := Finset F) (univ \ {-1}) b) ↦ b / (1 + b)) y hy) ⋯ =
      y
⊢ Eq.{u_2 + 1} (α := R) (∑ x ∈ univ \ {1}, (χ : (a : F) → R) (x / (1 - x))) (∑ x ∈ univ \ {-1}, (χ : (a : F) → R) x)

Tactic:
refine sum_bij' (fun a _ ↦ a / (1 - a)) (fun b _ ↦ b / (1 + b)) (fun x hx ↦ ?_)
      (fun y hy ↦ ?_) (fun x hx ↦ ?_) (fun y hy ↦ ?_) (fun _ _ ↦ rfl)

Premises used: HSub.hSub, HDiv.hDiv, HAdd.hAdd, Finset.sum_bij', OfNat.ofNat, rfl
-- 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
x : F
hx : Membership.mem (γ := Finset F) (univ \ {1}) x
refine_1 : ∀ (hx : ¬x = 1), ¬x / (1 - x) = -1
⊢ Membership.mem (γ := Finset F) (univ \ {-1})
    ((fun (a : F) (x : Membership.mem (γ := Finset F) (univ \ {1}) a) ↦ a / (1 - a)) x hx)

Tactic:
simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hx ⊢

Premises used: Finset.mem_univ, Finset.mem_singleton, Finset.mem_sdiff, true_and
-- 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
x : F
hx : ¬x = 1
refine_1 : ¬Eq.{u_1 + 1} (α := F) 1 0
⊢ ¬x / (1 - x) = -1

Tactic:
rw [div_eq_iff <| sub_ne_zero.mpr ((ne_eq ..).symm ▸ hx).symm, mul_sub, mul_one,
        neg_one_mul, sub_neg_eq_add, right_eq_add, neg_eq_zero]

Premises used: Iff.mpr, mul_sub, sub_ne_zero, neg_one_mul, neg_eq_zero, div_eq_iff, mul_one, right_eq_add, sub_neg_eq_add