-- Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean
theorem quadraticCharFun_mul (a b : F) :
    quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b

Proof state:
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b

Tactic:
rw [quadraticCharFun_eq_pow_of_char_ne_two hF ha, quadraticCharFun_eq_pow_of_char_ne_two hF hb,
  quadraticCharFun_eq_pow_of_char_ne_two hF hab, mul_pow]

Result:
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
⊢ (if a ^ (Fintype.card F / 2) * b ^ (Fintype.card F / 2) = 1 then 1 else -1) =
    (if a ^ (Fintype.card F / 2) = 1 then 1 else -1) * if b ^ (Fintype.card F / 2) = 1 then 1 else -1

Proof state:
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : a = 0
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b

Tactic:
rw [ha, zero_mul, quadraticCharFun_zero, zero_mul]

Result:
no goals

Proof state:
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : b = 0
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b

Tactic:
rw [hb, mul_zero, quadraticCharFun_zero, mul_zero]

Result:
no goals

Proof state:
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ringChar F = 2
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b

Tactic:
rw [quadraticCharFun_eq_one_of_char_two hF ha, quadraticCharFun_eq_one_of_char_two hF hb,
  quadraticCharFun_eq_one_of_char_two hF hab, mul_one]

Result:
no goals

Proof state:
case neg.inl
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
hb' : b ^ (Fintype.card F / 2) = 1
⊢ (if a ^ (Fintype.card F / 2) * b ^ (Fintype.card F / 2) = 1 then 1 else -1) =
    (if a ^ (Fintype.card F / 2) = 1 then 1 else -1) * if b ^ (Fintype.card F / 2) = 1 then 1 else -1

Tactic:
simp only [hb', mul_one, if_true]

Result:
no goals

Proof state:
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b

Tactic:
by_cases hF : ringChar F = 2

Result:
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ringChar F = 2
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b

case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b

Proof state:
case neg.inr
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
hb' : b ^ (Fintype.card F / 2) = -1
h : -1 ≠ 1
⊢ (if -a ^ (Fintype.card F / 2) = 1 then 1 else -1) = -if a ^ (Fintype.card F / 2) = 1 then 1 else -1

Tactic:
rcases FiniteField.pow_dichotomy hF ha with ha' | ha' <;>
  simp only [ha', h, neg_neg, if_true, if_false]

Result:
no goals

Proof state:
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
⊢ (if a ^ (Fintype.card F / 2) * b ^ (Fintype.card F / 2) = 1 then 1 else -1) =
    (if a ^ (Fintype.card F / 2) = 1 then 1 else -1) * if b ^ (Fintype.card F / 2) = 1 then 1 else -1

Tactic:
rcases FiniteField.pow_dichotomy hF hb with hb' | hb'

Result:
case neg.inl
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
hb' : b ^ (Fintype.card F / 2) = 1
⊢ (if a ^ (Fintype.card F / 2) * b ^ (Fintype.card F / 2) = 1 then 1 else -1) =
    (if a ^ (Fintype.card F / 2) = 1 then 1 else -1) * if b ^ (Fintype.card F / 2) = 1 then 1 else -1

case neg.inr
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
hb' : b ^ (Fintype.card F / 2) = -1
⊢ (if a ^ (Fintype.card F / 2) * b ^ (Fintype.card F / 2) = 1 then 1 else -1) =
    (if a ^ (Fintype.card F / 2) = 1 then 1 else -1) * if b ^ (Fintype.card F / 2) = 1 then 1 else -1

Proof state:
case neg.inr
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
hb' : b ^ (Fintype.card F / 2) = -1
⊢ (if a ^ (Fintype.card F / 2) * b ^ (Fintype.card F / 2) = 1 then 1 else -1) =
    (if a ^ (Fintype.card F / 2) = 1 then 1 else -1) * if b ^ (Fintype.card F / 2) = 1 then 1 else -1

Tactic:
have h := Ring.neg_one_ne_one_of_char_ne_two hF

Result:
case neg.inr
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
hb' : b ^ (Fintype.card F / 2) = -1
h : -1 ≠ 1
⊢ (if a ^ (Fintype.card F / 2) * b ^ (Fintype.card F / 2) = 1 then 1 else -1) =
    (if a ^ (Fintype.card F / 2) = 1 then 1 else -1) * if b ^ (Fintype.card F / 2) = 1 then 1 else -1

Proof state:
case neg.inr
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
hb' : b ^ (Fintype.card F / 2) = -1
h : -1 ≠ 1
⊢ (if a ^ (Fintype.card F / 2) * b ^ (Fintype.card F / 2) = 1 then 1 else -1) =
    (if a ^ (Fintype.card F / 2) = 1 then 1 else -1) * if b ^ (Fintype.card F / 2) = 1 then 1 else -1

Tactic:
simp only [hb', mul_neg, mul_one, h, if_false]

Result:
case neg.inr
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
hb' : b ^ (Fintype.card F / 2) = -1
h : -1 ≠ 1
⊢ (if -a ^ (Fintype.card F / 2) = 1 then 1 else -1) = -if a ^ (Fintype.card F / 2) = 1 then 1 else -1

Proof state:
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b

Tactic:
have hab := mul_ne_zero ha hb

Result:
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b

Tactic:
by_cases ha : a = 0

Result:
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : a = 0
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b

case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b

Proof state:
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b

Tactic:
by_cases hb : b = 0

Result:
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : b = 0
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b

case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b