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 : 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: 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]
-- 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
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
⊢ jacobiSum (MulChar.trivial F R) (MulChar.trivial F R) = HSub.hSub (α := R) (↑(Fintype.card F) : R) 2
have 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
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]
-- 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
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
have 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
Tactic: apply Finset.sum_eq_zero
-- 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
inst_3 : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
⊢ jacobiSum 1 χ = -1
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
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]
-- 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
inst_3 : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
⊢ jacobiSum 1 χ = -1
have 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
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]
-- 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
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
⊢ jacobiSum 1 χ = -1
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
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]
-- 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
inst_3 : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
| 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)
have h : ∀ (x : F), HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((χ⁻¹ : (a : F) → R) (1 - x) : R)
Tactic: enter [1, 2, x]
-- 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
inst_3 : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
x : F
| HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) x : R) ((χ⁻¹ : (a : F) → R) (1 - x) : R)
have h : ((χ : (a : F) → R) (x / (1 - x)) : R)
Tactic: rw [MulChar.inv_apply', ← map_mul, ← div_eq_mul_inv]
-- 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
inst_3 : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
| 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)
have h : ∀ (x : F), ((χ : (a : F) → R) (x / (1 - x)) : R)
Tactic: enter [1, 2, x]; rw [MulChar.inv_apply', ← map_mul, ← div_eq_mul_inv]
-- 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
inst_3 : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
⊢ 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)
have conv : Eq.{u_2 + 1} (α := R) (∑ x : F, (χ : (a : F) → R) (x / (1 - x)) : R) (-(χ : (a : F) → R) (-1) : R)
Tactic: conv => enter [1, 2, x]; rw [MulChar.inv_apply', ← map_mul, ← div_eq_mul_inv]
-- 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
inst_3 : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
⊢ Eq.{u_2 + 1} (α := R) (∑ x : F, (χ : (a : F) → R) (x / (1 - x)) : R) (-(χ : (a : F) → R) (-1) : R)
have rw : Eq.{u_2 + 1} (α := R) (∑ x ∈ univ \ {1}, (χ : (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]
-- 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
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)
have 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)
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)
-- 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
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)
⊢ Eq.{u_2 + 1} (α := R) (∑ x ∈ univ \ {1}, (χ : (a : F) → R) (x / (1 - x))) (∑ x ∈ univ \ {-1}, (χ : (a : F) → R) x)
have 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)
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)
-- 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
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)
⊢ Eq.{u_2 + 1} (α := R) (∑ x ∈ univ \ {1}, (χ : (a : F) → R) (x / (1 - x))) (∑ x ∈ univ \ {-1}, (χ : (a : F) → R) x)
have 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) sorry =
    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)
-- 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
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
⊢ Eq.{u_2 + 1} (α := R) (∑ x ∈ univ \ {1}, (χ : (a : F) → R) (x / (1 - x))) (∑ x ∈ univ \ {-1}, (χ : (a : F) → R) x)
have 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) sorry =
    y
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)
-- 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
inst_3 : IsDomain R
χ : MulChar F R
hχ : χ ≠ 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)
have refine_1 : ∀ (hx : ¬x = 1), ¬x / (1 - x) = -1
Tactic: simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hx ⊢
Cleared hypotheses: 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
inst_3 : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
x : F
hx : ¬x = 1
⊢ ¬x / (1 - x) = -1
have refine_1 : ¬Eq.{u_1 + 1} (α := F) 1 0
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]
-- 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
inst_3 : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
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)
have refine_2 : ∀ (hy : ¬y = -1), ¬y / (1 + y) = 1
Tactic: simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hy ⊢
Cleared hypotheses: hy
-- 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
inst_3 : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
y : F
hy : ¬y = -1
⊢ ¬y / (1 + y) = 1
have refine_2 : ¬Eq.{u_1 + 1} (α := F) 1 0
Tactic: rw [div_eq_iff fun h ↦ hy <| eq_neg_of_add_eq_zero_right h, one_mul, right_eq_add]
-- 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
inst_3 : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
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
have hx₁ : ¬x = 1
Tactic: simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at 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
inst_3 : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
x : F
hx_1 : Membership.mem (γ := Finset F) (univ \ {1}) x
hx : ¬x = 1
⊢ (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_1) ⋯ =
    x
have hx₁ : ¬1 - x = 0
Tactic: rw [eq_comm, ← sub_eq_zero] 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
inst_3 : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
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
have hy₁ : ¬y = -1
Tactic: simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hy
-- 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
inst_3 : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
y : F
hy_1 : Membership.mem (γ := Finset F) (univ \ {-1}) y
hy : ¬y = -1
⊢ (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_1) ⋯ =
    y
have hy₁ : ¬1 + y = 0
Tactic: rw [eq_comm, neg_eq_iff_eq_neg, ← sub_eq_zero, sub_neg_eq_add] at hy
Cleared hypotheses: hy
-- 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
inst_3 : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
⊢ Eq.{u_2 + 1} (α := R) (∑ x ∈ univ \ {1}, (χ : (a : F) → R) (x / (1 - x)) : R) (-(χ : (a : F) → R) (-1) : R)
have this : Eq.{u_2 + 1} (α := R) (∑ x ∈ univ \ {1}, (χ : (a : F) → R) (x / (1 - x))) (∑ x ∈ univ \ {-1}, (χ : (a : F) → R) x)
Tactic: have : ∑ x ∈ univ \ {1}, χ (x / (1 - x)) = ∑ x ∈ univ \ {-1}, χ x := by
    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)
    · simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hx ⊢
      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]
      exact one_ne_zero
    · simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hy ⊢
      rw [div_eq_iff fun h ↦ hy <| eq_neg_of_add_eq_zero_right h, one_mul, right_eq_add]
      exact one_ne_zero
    · simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hx
      rw [eq_comm, ← sub_eq_zero] at hx
      simp [field]
    · simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hy
      rw [eq_comm, neg_eq_iff_eq_neg, ← sub_eq_zero, sub_neg_eq_add] at hy
      simp [field]
-- 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
inst_3 : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
this :
  Eq.{u_2 + 1} (α := R) (∑ x ∈ univ \ {1}, (χ : (a : F) → R) (x / (1 - x))) (∑ x ∈ univ \ {-1}, (χ : (a : F) → R) x)
⊢ Eq.{u_2 + 1} (α := R) (∑ x ∈ univ \ {1}, (χ : (a : F) → R) (x / (1 - x)) : R) (-(χ : (a : F) → R) (-1) : R)
have rw : Eq.{u_2 + 1} (α := R) (∑ x : F, (χ : (a : F) → R) x) 0
Tactic: rw [this, ← add_eq_zero_iff_eq_neg, ← sum_eq_sum_diff_singleton_add (mem_univ (-1 : F))]
-- 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
inst_3 : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
⊢ jacobiSum χ χ⁻¹ = -(χ : (a : F) → R) (-1)
have rw : 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: classical
  rw [jacobiSum]
  conv => enter [1, 2, x]; rw [MulChar.inv_apply', ← map_mul, ← div_eq_mul_inv]
  rw [sum_eq_sum_diff_singleton_add (mem_univ (1 : F)), sub_self, div_zero, χ.map_zero, add_zero]
  have : ∑ x ∈ univ \ {1}, χ (x / (1 - x)) = ∑ x ∈ univ \ {-1}, χ x := by
    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)
    · simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hx ⊢
      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]
      exact one_ne_zero
    · simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hy ⊢
      rw [div_eq_iff fun h ↦ hy <| eq_neg_of_add_eq_zero_right h, one_mul, right_eq_add]
      exact one_ne_zero
    · simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hx
      rw [eq_comm, ← sub_eq_zero] at hx
      simp [field]
    · simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hy
      rw [eq_comm, neg_eq_iff_eq_neg, ← sub_eq_zero, sub_neg_eq_add] at hy
      simp [field]
  rw [this, ← add_eq_zero_iff_eq_neg, ← sum_eq_sum_diff_singleton_add (mem_univ (-1 : F))]
  exact MulChar.sum_eq_zero_of_ne_one hχ
-- 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
inst_3 : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
rw rw₁ rw₂ :
  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)
⊢ jacobiSum χ χ⁻¹ = -(χ : (a : F) → R) (-1)
have rw₃ : Eq.{u_2 + 1} (α := R) (∑ x : F, (χ : (a : F) → R) (x / (1 - x)) : R) (-(χ : (a : F) → R) (-1) : R)
Tactic: classical
  rw [jacobiSum]
  conv => enter [1, 2, x]; rw [MulChar.inv_apply', ← map_mul, ← div_eq_mul_inv]
  rw [sum_eq_sum_diff_singleton_add (mem_univ (1 : F)), sub_self, div_zero, χ.map_zero, add_zero]
  have : ∑ x ∈ univ \ {1}, χ (x / (1 - x)) = ∑ x ∈ univ \ {-1}, χ x := by
    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)
    · simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hx ⊢
      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]
      exact one_ne_zero
    · simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hy ⊢
      rw [div_eq_iff fun h ↦ hy <| eq_neg_of_add_eq_zero_right h, one_mul, right_eq_add]
      exact one_ne_zero
    · simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hx
      rw [eq_comm, ← sub_eq_zero] at hx
      simp [field]
    · simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hy
      rw [eq_comm, neg_eq_iff_eq_neg, ← sub_eq_zero, sub_neg_eq_add] at hy
      simp [field]
  rw [this, ← add_eq_zero_iff_eq_neg, ← sum_eq_sum_diff_singleton_add (mem_univ (-1 : F))]
  exact MulChar.sum_eq_zero_of_ne_one hχ