awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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
⊢ 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)
have 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))
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]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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
⊢ 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))
have 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))
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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
⊢ 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))
have 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)
Tactic: rw [sum_pair zero_ne_one, sub_zero, ψ.map_one, χ.map_one, sub_self, mul_zero, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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)
⊢ 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))
have 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)
Tactic: rw [sum_pair zero_ne_one, sub_zero, ψ.map_one, χ.map_one, sub_self, mul_zero, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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)
⊢ 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))
have 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)
Tactic: rw [sum_pair zero_ne_one, sub_zero, ψ.map_one, χ.map_one, sub_self, mul_zero, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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)
⊢ 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))
have 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)
Tactic: rw [sum_pair zero_ne_one, sub_zero, ψ.map_one, χ.map_one, sub_self, mul_zero, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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)
⊢ 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))
have 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)
Tactic: rw [sum_pair zero_ne_one, sub_zero, ψ.map_one, χ.map_one, sub_self, mul_zero, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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)
⊢ 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))
have e_a₅ : 0 = 0 + 0 * HSub.hSub (α := R) (β := R) ((ψ : (a : F) → R) (HSub.hSub (α := F) 1 1) : R) (1 : R)
Tactic: rw [sum_pair zero_ne_one, sub_zero, ψ.map_one, χ.map_one, sub_self, mul_zero, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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)
⊢ 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))
have e_a₆ : 0 = HAdd.hAdd (α := R) 0 0
Tactic: rw [sum_pair zero_ne_one, sub_zero, ψ.map_one, χ.map_one, sub_self, mul_zero, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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
⊢ 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))
have e_a₇ : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [sum_pair zero_ne_one, sub_zero, ψ.map_one, χ.map_one, sub_self, mul_zero, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
Goal:
F : Type u_1
R : Type u_2
inst : Field F
inst_1 : Fintype F
inst_2 : CommRing R
⊢ jacobiSum (MulChar.trivial F R) (MulChar.trivial F R) = HSub.hSub (α := R) (↑(Fintype.card F) : R) 2
have 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
Tactic: rw [jacobiSum_eq_sum_sdiff]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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
⊢ HMul.hMul (α := R) (β := R) ((MulChar.trivial F R : (a : F) → R) x : R)
      ((MulChar.trivial F R : (a : F) → R) (1 - x) : R) =
    1
have hc : IsUnit (x * (1 - x))
Tactic: rw [← map_mul, MulChar.trivial_apply, if_pos]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (hypothesis)
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
⊢ IsUnit (x * (1 - x))
have hx₁ : x ≠ 0 ∧ x ≠ 1
Tactic: simp only [mem_sdiff, mem_univ, mem_insert, mem_singleton, not_or, ← ne_eq, true_and] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (hypothesis)
Goal:
F : Type u_1
R : Type u_2
inst : Field F
inst_1 : Fintype F
inst_2 : CommRing 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) =
    HSub.hSub (α := R) (↑(Fintype.card F) : R) 2
have 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
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
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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
⊢ (↑(card (α := F) (univ \ {0, 1})) : R) = HSub.hSub (α := R) (↑(Fintype.card F) : R) 2
have rw : (↑(card.{u_1} (α := F) univ - card (α := F) {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]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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
⊢ (↑(card (α := F) (univ \ {0, 1})) : R) = HSub.hSub (α := R) (↑(Fintype.card F) : R) 2
have rw₁ : (↑(Fintype.card F - card (α := F) {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]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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
⊢ (↑(card (α := F) (univ \ {0, 1})) : R) = HSub.hSub (α := R) (↑(Fintype.card F) : R) 2
have rw₂ : (↑(Fintype.card F - 2) : 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]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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
⊢ (↑(card (α := F) (univ \ {0, 1})) : R) = HSub.hSub (α := R) (↑(Fintype.card F) : R) 2
have rw₃ : HSub.hSub (α := R) (↑(Fintype.card F) : R) (↑(HAdd.hAdd (α := ℕ) 1 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]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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
⊢ (↑(card (α := F) (univ \ {0, 1})) : R) = HSub.hSub (α := R) (↑(Fintype.card F) : R) 2
have rw₄ : HSub.hSub (α := R) (↑(Fintype.card F) : R) 2 = 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]
-- Lean 4 proof step from Mathlib.NumberTheory.JacobiSum.Basic (goal)
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
⊢ ∑ 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
have calc : (↑(card (α := F) (univ \ {0, 1})) : 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]