awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : b % 2 = 0
ha2 : a % 2 = 0
pos : 1 < a.gcd (↑b : ℤ)
⊢ J(a | b) = 0

Tactic:
refine eq_zero_iff.mpr ⟨hb0, ne_of_gt ?_⟩

Premises used: Iff.mpr, ne_of_gt, And.intro, jacobiSym.eq_zero_iff
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : b % 2 = 0
ha2 : a % 2 = 0
⊢ 1 < a.gcd (↑b : ℤ)

Tactic:
Nat.le_of_dvd (Int.gcd_pos_iff.mpr (mod_cast .inr hb0)) ?_

Premises used: Iff.mpr, congrArg, cast, Ne, Nat.cast, Int.gcd_pos_iff, congr, Nat.cast_inj._simp_1, congrFun', Or, Nat.cast_zero, OfNat.ofNat, Eq.symm, Nat.le_of_dvd, Eq, Not, Or.inr, Nat.lt, Eq.trans
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : b % 2 = 0
ha2 : a % 2 = 0
pos : Nat.succ 1 ∣ a.gcd (↑b : ℤ)
⊢ 1 < a.gcd (↑b : ℤ)

Tactic:
refine Nat.le_of_dvd (Int.gcd_pos_iff.mpr (mod_cast .inr hb0)) ?_

Premises used: Iff.mpr, Int.gcd_pos_iff, Nat.le_of_dvd
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : b % 2 = 0
ha2 : a % 2 = 0
⊢ Nat.succ 1 ∣ a.gcd (↑b : ℤ)

Tactic:
Nat.dvd_gcd (Int.ofNat_dvd_left.mp (Int.dvd_of_emod_eq_zero ha2)) ?_

Premises used: Int.gcd, Int.ofNat_dvd_left, Int.dvd_of_emod_eq_zero, Nat.dvd_gcd, Iff.mp
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : b % 2 = 0
ha2 : a % 2 = 0
pos : Nat.succ 1 ∣ Int.natAbs (↑b : ℤ)
⊢ Nat.succ 1 ∣ a.gcd (↑b : ℤ)

Tactic:
refine Nat.dvd_gcd (Int.ofNat_dvd_left.mp (Int.dvd_of_emod_eq_zero ha2)) ?_

Premises used: Int.ofNat_dvd_left, Int.dvd_of_emod_eq_zero, Nat.dvd_gcd, Iff.mp
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : b % 2 = 0
ha2 : a % 2 = 0
⊢ Nat.succ 1 ∣ Int.natAbs (↑b : ℤ)

Tactic:
Int.ofNat_dvd_left.mp (Int.dvd_of_emod_eq_zero (mod_cast hb2))

Premises used: congrArg, Int.ofNat_dvd_left, cast, Int.dvd_of_emod_eq_zero, Nat.cast, HMod.hMod, Iff.mp, Nat.cast_inj._simp_1, Nat.cast_zero, OfNat.ofNat, Eq.symm, Nat.succ, Eq, Eq.trans
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : b % 2 = 0
ha2 : a % 2 = 0
⊢ Nat.succ 1 ∣ Int.natAbs (↑b : ℤ)

Tactic:
exact Int.ofNat_dvd_left.mp (Int.dvd_of_emod_eq_zero (mod_cast hb2))

Premises used: Int.ofNat_dvd_left, Int.dvd_of_emod_eq_zero, Iff.mp
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : b % 2 = 0
ha2 : ¬a % 2 = 0
neg : J(a | b) = J(a | b / 2)
⊢ J(a | b) = fastJacobiSym a (b / 2)

Tactic:
rw [← IH (b / 2) (b.div_lt_self (Nat.pos_of_ne_zero hb0) one_lt_two)]

Premises used: HDiv.hDiv, Nat.div_lt_self, Nat.pos_of_ne_zero, one_lt_two, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : b % 2 = 0
ha2 : ¬a % 2 = 0
neg :
  ∀ (b : ℕ) (IH : ∀ m < 2 * b, J(a | m) = fastJacobiSym a m) (hb0 : ¬2 * b = 0) (hb2 : 2 * b % 2 = 0),
    J(a | 2 * b) = J(a | 2 * b / 2)
⊢ J(a | b) = J(a | b / 2)

Tactic:
obtain ⟨b, rfl⟩ := Nat.dvd_of_mod_eq_zero hb2

Premises used: Nat.dvd_of_mod_eq_zero, rfl
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
ha2 : ¬a % 2 = 0
b : ℕ
IH : ∀ m < 2 * b, J(a | m) = fastJacobiSym a m
hb0 : ¬2 * b = 0
hb2 : 2 * b % 2 = 0
⊢ Ne (α := ℕ) 2 0

Tactic:
decide
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
ha2 : ¬a % 2 = 0
b : ℕ
IH : ∀ m < 2 * b, J(a | m) = fastJacobiSym a m
hb0 : ¬2 * b = 0
hb2 : 2 * b % 2 = 0
⊢ LT.lt (α := ℕ) 0 2

Tactic:
decide
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
ha2 : ¬a % 2 = 0
b : ℕ
IH : ∀ m < 2 * b, J(a | m) = fastJacobiSym a m
hb0 : ¬2 * b = 0
hb2 : 2 * b % 2 = 0
neg : J(a | 2) * J(a | b) = J(a | 2 * b / 2)
neg₁ : J(a | 2) * J(a | b) = J(a | b)
neg₂ : J(a % (↑2 : ℤ) | 2) * J(a | b) = J(a | b)
neg₃ : J(a % 2 | 2) * J(a | b) = J(a | b)
neg₄ : J(1 | 2) * J(a | b) = J(a | b)
neg₅ : 1 * J(a | b) = J(a | b)
neg₆ neg₇ : J(a | b) = J(a | b)
⊢ J(a | 2 * b) = J(a | 2 * b / 2)

Tactic:
rw [mul_right' a (by decide) fun h ↦ hb0 (mul_eq_zero_of_right 2 h),
      b.mul_div_cancel_left (by decide), mod_left a 2, Nat.cast_ofNat,
      Int.emod_two_ne_zero.mp ha2, one_left, one_mul]

Premises used: Nat.cast_ofNat, Nat.mul_div_cancel_left, jacobiSym.mod_left, mul_eq_zero_of_right, jacobiSym.one_left, Int.emod_two_ne_zero, Iff.mp, jacobiSym.mul_right', OfNat.ofNat, one_mul
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : b = 1
pos : J(a | 1) = 1
pos₁ pos₂ : Eq (α := ℤ) 1 1
⊢ J(a | b) = 1

Tactic:
rw [hb1, one_right]

Premises used: jacobiSym.one_right
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : a % (↑b : ℤ) = 0
pos : J(a % (↑b : ℤ) | b) = 0
pos₁ : J(0 | b) = 0
pos₂ pos₃ : Eq (α := ℤ) 0 0
⊢ J(a | b) = 0

Tactic:
rw [mod_left, hab, zero_left (lt_of_le_of_ne (Nat.pos_of_ne_zero hb0) (Ne.symm hb1))]

Premises used: jacobiSym.mod_left, Ne.symm, jacobiSym.zero_left, Nat.pos_of_ne_zero, lt_of_le_of_ne
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : ¬a % (↑b : ℤ) = 0
neg : b % 2 = 1
neg₁ : b > 1
⊢ J(a | b) = fastJacobiSymAux (a % (↑b : ℤ)).natAbs b false ⋯

Tactic:
rw [fastJacobiSymAux.eq_jacobiSym, if_neg Bool.false_ne_true, mod_left a b,
      Int.natAbs_of_nonneg (a.emod_nonneg (mod_cast hb0))]

Premises used: jacobiSym.mod_left, _private.0.fastJacobiSymAux.eq_jacobiSym, Int.natAbs_of_nonneg, Bool.false_ne_true, if_neg, Int.emod_nonneg
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : ¬a % (↑b : ℤ) = 0
⊢ b % 2 = 1

Tactic:
Nat.mod_two_ne_zero.mp hb2

Premises used: Iff.mp, Nat.mod_two_ne_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : ¬a % (↑b : ℤ) = 0
⊢ b % 2 = 1

Tactic:
exact Nat.mod_two_ne_zero.mp hb2

Premises used: Iff.mp, Nat.mod_two_ne_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : ¬a % (↑b : ℤ) = 0
⊢ b > 1

Tactic:
lt_of_le_of_ne (Nat.one_le_iff_ne_zero.mpr hb0) (Ne.symm hb1)

Premises used: Iff.mpr, Ne.symm, Nat.one_le_iff_ne_zero, lt_of_le_of_ne
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : ¬a % (↑b : ℤ) = 0
⊢ b > 1

Tactic:
exact lt_of_le_of_ne (Nat.one_le_iff_ne_zero.mpr hb0) (Ne.symm hb1)

Premises used: Iff.mpr, Ne.symm, Nat.one_le_iff_ne_zero, lt_of_le_of_ne
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
h : ∀ (b : ℕ) (IH : ∀ m < b, J(a | m) = fastJacobiSym a m), J(a | b) = fastJacobiSym a b
⊢ J(a | b) = fastJacobiSym a b

Tactic:
induction b using Nat.strongRecOn with | ind b IH =>
  unfold fastJacobiSym
  split_ifs with hb0 hb2 ha2 hb1 hab
  · rw [hb0, zero_right]
  · refine eq_zero_iff.mpr ⟨hb0, ne_of_gt ?_⟩
    refine Nat.le_of_dvd (Int.gcd_pos_iff.mpr (mod_cast .inr hb0)) ?_
    refine Nat.dvd_gcd (Int.ofNat_dvd_left.mp (Int.dvd_of_emod_eq_zero ha2)) ?_
    exact Int.ofNat_dvd_left.mp (Int.dvd_of_emod_eq_zero (mod_cast hb2))
  · dsimp only
    rw [← IH (b / 2) (b.div_lt_self (Nat.pos_of_ne_zero hb0) one_lt_two)]
    obtain ⟨b, rfl⟩ := Nat.dvd_of_mod_eq_zero hb2
    rw [mul_right' a (by decide) fun h ↦ hb0 (mul_eq_zero_of_right 2 h),
      b.mul_div_cancel_left (by decide), mod_left a 2, Nat.cast_ofNat,
      Int.emod_two_ne_zero.mp ha2, one_left, one_mul]
  · rw [hb1, one_right]
  · rw [mod_left, hab, zero_left (lt_of_le_of_ne (Nat.pos_of_ne_zero hb0) (Ne.symm hb1))]
  · rw [fastJacobiSymAux.eq_jacobiSym, if_neg Bool.false_ne_true, mod_left a b,
      Int.natAbs_of_nonneg (a.emod_nonneg (mod_cast hb0))]
    · exact Nat.mod_two_ne_zero.mp hb2
    · exact lt_of_le_of_ne (Nat.one_le_iff_ne_zero.mpr hb0) (Ne.symm hb1)

Premises used: Iff.mpr, Nat.cast_ofNat, Nat.mul_div_cancel_left, jacobiSym.mod_left, Int.ofNat_dvd_left, Int.dvd_of_emod_eq_zero, _private.0.fastJacobiSymAux.eq_jacobiSym, jacobiSym.one_right, Int.natAbs_of_nonneg, jacobiSym.one_left, Int.gcd_pos_iff, jacobiSym.zero_right, Iff.mp, _private.0.fastJacobiSym, Bool.false_ne_true, OfNat.ofNat, Nat.le_of_dvd, if_neg, Int.emod_nonneg, one_mul, rfl
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
h : ∀ (p : ℕ) (x : Fact (Nat.Prime p)) (a : ℤ), legendreSym p a = fastLegendreSym p a
⊢ legendreSym = fastLegendreSym

Tactic:
ext p _ a
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
p : ℕ
h_1 : Fact (Nat.Prime p)
a : ℤ
h : J(a | p) = fastLegendreSym p a
h₁ h₂ : J(a | p) = J(a | p)
⊢ legendreSym p a = fastLegendreSym p a

Tactic:
rw [legendreSym.to_jacobiSym, fastLegendreSym]

Premises used: jacobiSym.legendreSym.to_jacobiSym, _private.0.fastLegendreSym
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a : F
⊢ Eq (α := ℤ) (if a = 0 then 0 else if IsSquare a then 1 else -1) 0 ↔ a = 0

Tactic:
grind
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
⊢ quadraticCharFun F 0 = 0

Tactic:
simp only [quadraticCharFun, if_true]

Premises used: if_true, quadraticCharFun
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
⊢ quadraticCharFun F 1 = 1

Tactic:
simp only [quadraticCharFun, one_ne_zero, IsSquare.one, if_true, if_false]

Premises used: if_true, if_false, quadraticCharFun, IsSquare.one, one_ne_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
hF : ringChar F = 2
a : F
ha : a ≠ 0
simp : ¬IsSquare a → Eq (α := ℤ) (-1) 1
⊢ quadraticCharFun F a = 1

Tactic:
simp only [quadraticCharFun, ha, if_false, ite_eq_left_iff]

Premises used: ite_eq_left_iff, if_false, quadraticCharFun
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
hF : ringChar F = 2
a : F
ha : a ≠ 0
⊢ ¬IsSquare a → Eq (α := ℤ) (-1) 1

Tactic:
fun h ↦ (h (FiniteField.isSquare_of_char_two hF a)).elim

Premises used: False.elim, FiniteField.isSquare_of_char_two
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
hF : ringChar F = 2
a : F
ha : a ≠ 0
⊢ ¬IsSquare a → Eq (α := ℤ) (-1) 1

Tactic:
exact fun h ↦ (h (FiniteField.isSquare_of_char_two hF a)).elim
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
simp : Eq (α := ℤ) (if IsSquare a then 1 else -1) (if a ^ (Fintype.card F / 2) = 1 then 1 else -1)
⊢ quadraticCharFun F a = if a ^ (Fintype.card F / 2) = 1 then 1 else -1

Tactic:
simp only [quadraticCharFun, ha, if_false]

Premises used: if_false, quadraticCharFun
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ Eq (α := ℤ) (if IsSquare a then 1 else -1) (if a ^ (Fintype.card F / 2) = 1 then 1 else -1)

Tactic:
simp_rw [FiniteField.isSquare_iff hF ha]

Premises used: FiniteField.isSquare_iff
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a b : F
pos : ∀ (ha : a = 0), quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
neg : ∀ (ha : ¬a = 0), quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a b : F
ha : a = 0
pos : quadraticCharFun F (0 * b) = quadraticCharFun F 0 * quadraticCharFun F b
pos₁ : quadraticCharFun F 0 = quadraticCharFun F 0 * quadraticCharFun F b
pos₂ : 0 = 0 * quadraticCharFun F b
pos₃ pos₄ : Eq (α := ℤ) 0 0
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b

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

Premises used: MulZeroClass.zero_mul, quadraticCharFun_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a b : F
ha : ¬a = 0
pos : ∀ (hb : b = 0), quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
neg : ∀ (hb : ¬b = 0), quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b

Tactic:
by_cases hb : b = 0
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a b : F
ha : ¬a = 0
hb : b = 0
pos : quadraticCharFun F (a * 0) = quadraticCharFun F a * quadraticCharFun F 0
pos₁ : quadraticCharFun F 0 = quadraticCharFun F a * quadraticCharFun F 0
pos₂ : 0 = quadraticCharFun F a * 0
pos₃ pos₄ : Eq (α := ℤ) 0 0
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b

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

Premises used: MulZeroClass.mul_zero, quadraticCharFun_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
⊢ a * b ≠ 0

Tactic:
have hab := mul_ne_zero ha hb
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
pos : ∀ (hF : ringChar F = 2), quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
neg : ∀ (hF : ¬ringChar F = 2), quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b

Tactic:
by_cases hF : ringChar F = 2

Premises used: ringChar
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ringChar F = 2
pos : quadraticCharFun F (a * b) = 1 * quadraticCharFun F b
pos₁ : quadraticCharFun F (a * b) = HMul.hMul (α := ℤ) 1 1
pos₂ : 1 = HMul.hMul (α := ℤ) 1 1
pos₃ pos₄ : Eq (α := ℤ) 1 1
⊢ 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]

Premises used: quadraticCharFun_eq_one_of_char_two, mul_one
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
neg :
  (if a ^ (Fintype.card F / 2) * b ^ (Fintype.card F / 2) = 1 then 1 else -1) =
    HMul.hMul (α := ℤ) (if a ^ (Fintype.card F / 2) = 1 then 1 else -1) (if b ^ (Fintype.card F / 2) = 1 then 1 else -1)
⊢ 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]

Premises used: quadraticCharFun_eq_pow_of_char_ne_two, mul_pow
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
neg :
  ∀ (hb' : b ^ (Fintype.card F / 2) = 1),
    (if a ^ (Fintype.card F / 2) * b ^ (Fintype.card F / 2) = 1 then 1 else -1) =
      HMul.hMul (α := ℤ) (if a ^ (Fintype.card F / 2) = 1 then 1 else -1)
        (if b ^ (Fintype.card F / 2) = 1 then 1 else -1)
neg₁ :
  ∀ (hb' : b ^ (Fintype.card F / 2) = -1),
    (if a ^ (Fintype.card F / 2) * b ^ (Fintype.card F / 2) = 1 then 1 else -1) =
      HMul.hMul (α := ℤ) (if a ^ (Fintype.card F / 2) = 1 then 1 else -1)
        (if b ^ (Fintype.card F / 2) = 1 then 1 else -1)
⊢ (if a ^ (Fintype.card F / 2) * b ^ (Fintype.card F / 2) = 1 then 1 else -1) =
    HMul.hMul (α := ℤ) (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'

Premises used: FiniteField.pow_dichotomy
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : 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) =
    HMul.hMul (α := ℤ) (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]

Premises used: if_true, mul_one
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : 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
⊢ Ne.{u_1 + 1} (α := F) (-1) 1

Tactic:
have h := Ring.neg_one_ne_one_of_char_ne_two hF
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : 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 : Ne.{u_1 + 1} (α := F) (-1) 1
neg : Eq (α := ℤ) (if -a ^ (Fintype.card F / 2) = 1 then 1 else -1) (-if a ^ (Fintype.card F / 2) = 1 then 1 else -1)
⊢ (if a ^ (Fintype.card F / 2) * b ^ (Fintype.card F / 2) = 1 then 1 else -1) =
    HMul.hMul (α := ℤ) (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]

Premises used: if_false, mul_one, mul_neg
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : 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 : Ne.{u_1 + 1} (α := F) (-1) 1
neg :
  ∀ (ha' : a ^ (Fintype.card F / 2) = 1),
    Eq (α := ℤ) (if -a ^ (Fintype.card F / 2) = 1 then 1 else -1) (-if a ^ (Fintype.card F / 2) = 1 then 1 else -1)
neg₁ :
  ∀ (ha' : a ^ (Fintype.card F / 2) = -1),
    Eq (α := ℤ) (if -a ^ (Fintype.card F / 2) = 1 then 1 else -1) (-if a ^ (Fintype.card F / 2) = 1 then 1 else -1)
⊢ Eq (α := ℤ) (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'

Premises used: FiniteField.pow_dichotomy
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : 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 : Ne.{u_1 + 1} (α := F) (-1) 1
ha' : a ^ (Fintype.card F / 2) = 1
⊢ Eq (α := ℤ) (if -a ^ (Fintype.card F / 2) = 1 then 1 else -1) (-if a ^ (Fintype.card F / 2) = 1 then 1 else -1)

Tactic:
simp only [ha', h, neg_neg, if_true, if_false]

Premises used: if_true, if_false, neg_neg
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : 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 : Ne.{u_1 + 1} (α := F) (-1) 1
ha' : a ^ (Fintype.card F / 2) = -1
⊢ Eq (α := ℤ) (if -a ^ (Fintype.card F / 2) = 1 then 1 else -1) (-if a ^ (Fintype.card F / 2) = 1 then 1 else -1)

Tactic:
simp only [ha', h, neg_neg, if_true, if_false]

Premises used: if_true, if_false, neg_neg
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a : F
ha : ¬IsUnit a
rw : quadraticCharFun F 0 = 0
⊢ quadraticCharFun F a = 0

Tactic:
rw [of_not_not (mt Ne.isUnit ha)]

Premises used: Ne.isUnit, mt, of_not_not
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a : F
ha : ¬IsUnit a
⊢ quadraticCharFun F 0 = 0

Tactic:
quadraticCharFun_zero

Premises used: quadraticCharFun_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a : F
ha : ¬IsUnit a
⊢ quadraticCharFun F 0 = 0

Tactic:
exact quadraticCharFun_zero

Premises used: quadraticCharFun_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a : F
⊢ Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (0 : ℤ) ↔ a = 0

Tactic:
quadraticCharFun_eq_zero_iff

Premises used: quadraticCharFun_eq_zero_iff, quadraticCharFun, ite
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
⊢ Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) 0 : ℤ) (0 : ℤ)

Tactic:
simp only [quadraticChar_apply, quadraticCharFun_zero]

Premises used: quadraticChar_apply, quadraticCharFun_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a : F
ha : a ≠ 0
⊢ Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) (1 : ℤ) ↔ IsSquare a

Tactic:
simp only [quadraticChar_apply, quadraticCharFun, ha, if_false, ite_eq_left_iff,
    imp_false, not_not, reduceCtorEq]

Premises used: reduceCtorEq, ite_eq_left_iff, Classical.not_not, imp_false, if_false, quadraticCharFun, quadraticChar_apply
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a : F
ha : a ≠ 0
⊢ Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (HPow.hPow (β := ℕ) a 2) : ℤ) (1 : ℤ)

Tactic:
simp only [quadraticChar_apply, quadraticCharFun, sq_eq_zero_iff, ha, IsSquare.sq, if_true,
    if_false]

Premises used: if_true, if_false, IsSquare.sq, quadraticCharFun, quadraticChar_apply, sq_eq_zero_iff
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a : F
ha : a ≠ 0
rwa : HMul.hMul (α := ℤ) (β := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) = 1
rwa₁ : Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (a * a) : ℤ) (1 : ℤ)
rwa₂ : Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (HPow.hPow (β := ℕ) a 2) : ℤ) (1 : ℤ)
rwa₃ : Eq (α := ℤ) 1 1
rwa₄ : a ≠ 0
rwa₅ : Eq (α := ℤ) 1 1
rwa₆ rwa₇ rwa₈ : a ≠ 0
⊢ HPow.hPow (α := ℤ) (β := ℕ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) 2 = 1

Tactic:
rwa [pow_two, ← map_mul, ← pow_two, quadraticChar_sq_one']

Premises used: pow_two, map_mul, quadraticChar_sq_one'