-- Mathlib/NumberTheory/JacobiSum/Basic.lean
theorem jacobiSum_trivial_trivial :
    jacobiSum (MulChar.trivial F R) (MulChar.trivial F R) = Fintype.card F - 2

Proof state:
F : Type u_1
R : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : CommRing R
this : ∀ x ∈ univ \ {0, 1}, (MulChar.trivial F R) x * (MulChar.trivial F R) (1 - x) = 1
⊢ ∑ x ∈ univ \ {0, 1}, (MulChar.trivial F R) x * (MulChar.trivial F R) (1 - x) = ↑(Fintype.card F) - 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 (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]

Result:
no goals

Proof state:
F : Type u_1
R : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : CommRing R
this : ∀ x ∈ univ \ {0, 1}, (MulChar.trivial F R) x * (MulChar.trivial F R) (1 - x) = 1
⊢ ↑(#(univ \ {0, 1})) = ↑(Fintype.card F) - 2

Tactic:
rw [card_sdiff (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]

Result:
no goals

Proof state:
case hc
F : Type u_1
R : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : 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

Result:
no goals

Proof state:
F : Type u_1
R : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : CommRing R
⊢ jacobiSum (MulChar.trivial F R) (MulChar.trivial F R) = ↑(Fintype.card F) - 2

Tactic:
rw [jacobiSum_eq_sum_sdiff]

Result:
F : Type u_1
R : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : CommRing R
⊢ ∑ x ∈ univ \ {0, 1}, (MulChar.trivial F R) x * (MulChar.trivial F R) (1 - x) = ↑(Fintype.card F) - 2

Proof state:
case hc
F : Type u_1
R : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : CommRing R
x : F
hx : x ∈ univ \ {0, 1}
⊢ IsUnit (x * (1 - x))

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

Result:
case hc
F : Type u_1
R : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : CommRing R
x : F
hx : x ≠ 0 ∧ x ≠ 1
⊢ IsUnit (x * (1 - x))

Proof state:
F : Type u_1
R : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : CommRing R
⊢ ∑ x ∈ univ \ {0, 1}, (MulChar.trivial F R) x * (MulChar.trivial F R) (1 - x) = ↑(Fintype.card F) - 2

Tactic:
have : ∀ x ∈ univ \ {0, 1}, (MulChar.trivial F R) x * (MulChar.trivial F R) (1 - x) = 1 := by
  intros 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

Result:
F : Type u_1
R : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : CommRing R
this : ∀ x ∈ univ \ {0, 1}, (MulChar.trivial F R) x * (MulChar.trivial F R) (1 - x) = 1
⊢ ∑ x ∈ univ \ {0, 1}, (MulChar.trivial F R) x * (MulChar.trivial F R) (1 - x) = ↑(Fintype.card F) - 2

Proof state:
F : Type u_1
R : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : CommRing R
⊢ ∀ x ∈ univ \ {0, 1}, (MulChar.trivial F R) x * (MulChar.trivial F R) (1 - x) = 1

Tactic:
intros x hx

Result:
F : Type u_1
R : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : CommRing R
x : F
hx : x ∈ univ \ {0, 1}
⊢ (MulChar.trivial F R) x * (MulChar.trivial F R) (1 - x) = 1

Proof state:
F : Type u_1
R : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : CommRing R
⊢ jacobiSum (MulChar.trivial F R) (MulChar.trivial F R) = ↑(Fintype.card F) - 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
  intros 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 (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]

Result:
no goals

Proof state:
F : Type u_1
R : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : CommRing R
x : F
hx : x ∈ univ \ {0, 1}
⊢ (MulChar.trivial F R) x * (MulChar.trivial F R) (1 - x) = 1

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

Result:
case hc
F : Type u_1
R : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : CommRing R
x : F
hx : x ∈ univ \ {0, 1}
⊢ IsUnit (x * (1 - x))