-- Mathlib/NumberTheory/JacobiSum/Basic.lean
theorem jacobiSum_nontrivial_inv {χ : MulChar F R} (hχ : χ ≠ 1) : jacobiSum χ χ⁻¹ = -χ (-1)

Proof state:
case refine_3
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
x : F
hx✝ : x ∈ univ \ {1}
hx : ¬x = 1
⊢ (fun b x => b / (1 + b)) ((fun a x => a / (1 - a)) x hx✝) ⋯ = x

Tactic:
rw [eq_comm, ← sub_eq_zero] at hx

Result:
case refine_3
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
x : F
hx✝ : x ∈ univ \ {1}
hx : ¬1 - x = 0
⊢ (fun b x => b / (1 + b)) ((fun a x => a / (1 - a)) x hx✝) ⋯ = x

Proof state:
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
⊢ ∑ x : F, χ (x / (1 - x)) = -χ (-1)

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

Result:
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
⊢ ∑ x ∈ univ \ {1}, χ (x / (1 - x)) = -χ (-1)

Proof state:
case refine_1
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
x : F
hx : ¬x = 1
⊢ ¬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, self_eq_add_left, neg_eq_zero]

Result:
case refine_1
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
x : F
hx : ¬x = 1
⊢ ¬1 = 0

Proof state:
case refine_3
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
x : F
hx : x ∈ univ \ {1}
⊢ (fun b x => b / (1 + b)) ((fun a x => a / (1 - a)) x hx) ⋯ = x

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

Result:
case refine_3
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
x : F
hx✝ : x ∈ univ \ {1}
hx : ¬x = 1
⊢ (fun b x => b / (1 + b)) ((fun a x => a / (1 - a)) x hx✝) ⋯ = x

Proof state:
case refine_1
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
x : F
hx : ¬x = 1
⊢ ¬1 = 0

Tactic:
exact one_ne_zero

Result:
no goals

Proof state:
case refine_2
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
y : F
hy : ¬y = -1
⊢ ¬1 = 0

Tactic:
exact one_ne_zero

Result:
no goals

Proof state:
case refine_4
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
y : F
hy✝ : y ∈ univ \ {-1}
hy : ¬1 + y = 0
⊢ (fun a x => a / (1 - a)) ((fun b x => b / (1 + b)) y hy✝) ⋯ = y

Tactic:
field_simp

Result:
no goals

Proof state:
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
⊢ jacobiSum χ χ⁻¹ = -χ (-1)

Tactic:
rw [jacobiSum]

Result:
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
⊢ ∑ x : F, χ x * χ⁻¹ (1 - x) = -χ (-1)

Proof state:
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
this : ∑ x ∈ univ \ {1}, χ (x / (1 - x)) = ∑ x ∈ univ \ {-1}, χ x
⊢ ∑ x ∈ univ \ {1}, χ (x / (1 - x)) = -χ (-1)

Tactic:
rw [this, ← add_eq_zero_iff_eq_neg, ← sum_eq_sum_diff_singleton_add (mem_univ (-1 : F))]

Result:
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
this : ∑ x ∈ univ \ {1}, χ (x / (1 - x)) = ∑ x ∈ univ \ {-1}, χ x
⊢ ∑ x : F, χ x = 0

Proof state:
case refine_4
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
y : F
hy : y ∈ univ \ {-1}
⊢ (fun a x => a / (1 - a)) ((fun b x => b / (1 + b)) y hy) ⋯ = y

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

Result:
case refine_4
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
y : F
hy✝ : y ∈ univ \ {-1}
hy : ¬y = -1
⊢ (fun a x => a / (1 - a)) ((fun b x => b / (1 + b)) y hy✝) ⋯ = y

Proof state:
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
⊢ ∑ x ∈ univ \ {1}, χ (x / (1 - x)) = ∑ x ∈ univ \ {-1}, χ 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)

Result:
case refine_1
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
x : F
hx : x ∈ univ \ {1}
⊢ (fun a x => a / (1 - a)) x hx ∈ univ \ {-1}

case refine_2
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
y : F
hy : y ∈ univ \ {-1}
⊢ (fun b x => b / (1 + b)) y hy ∈ univ \ {1}

case refine_3
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
x : F
hx : x ∈ univ \ {1}
⊢ (fun b x => b / (1 + b)) ((fun a x => a / (1 - a)) x hx) ⋯ = x

case refine_4
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
y : F
hy : y ∈ univ \ {-1}
⊢ (fun a x => a / (1 - a)) ((fun b x => b / (1 + b)) y hy) ⋯ = y

Proof state:
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
this : ∑ x ∈ univ \ {1}, χ (x / (1 - x)) = ∑ x ∈ univ \ {-1}, χ x
⊢ ∑ x : F, χ x = 0

Tactic:
exact MulChar.sum_eq_zero_of_ne_one hχ

Result:
no goals

Proof state:
case refine_2
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
y : F
hy : y ∈ univ \ {-1}
⊢ (fun b x => b / (1 + b)) y hy ∈ univ \ {1}

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

Result:
case refine_2
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
y : F
hy : ¬y = -1
⊢ ¬y / (1 + y) = 1

Proof state:
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
⊢ ∑ x : F, χ x * χ⁻¹ (1 - x) = -χ (-1)

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

Result:
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
⊢ ∑ x : F, χ (x / (1 - x)) = -χ (-1)

Proof state:
case refine_3
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
x : F
hx✝ : x ∈ univ \ {1}
hx : ¬1 - x = 0
⊢ (fun b x => b / (1 + b)) ((fun a x => a / (1 - a)) x hx✝) ⋯ = x

Tactic:
field_simp

Result:
no goals

Proof state:
case refine_4
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
y : F
hy✝ : y ∈ univ \ {-1}
hy : ¬y = -1
⊢ (fun a x => a / (1 - a)) ((fun b x => b / (1 + b)) y hy✝) ⋯ = y

Tactic:
rw [eq_comm, neg_eq_iff_eq_neg, ← sub_eq_zero, sub_neg_eq_add] at hy

Result:
case refine_4
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
y : F
hy✝ : y ∈ univ \ {-1}
hy : ¬1 + y = 0
⊢ (fun a x => a / (1 - a)) ((fun b x => b / (1 + b)) y hy✝) ⋯ = y