awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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)
⊢ J(a | 2 * b) = J(a | 2 * b / 2)
have neg₃ : J(a % 2 | 2) * J(a | b) = J(a | b)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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)
⊢ J(a | 2 * b) = J(a | 2 * b / 2)
have neg₄ : J(1 | 2) * J(a | b) = J(a | b)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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)
⊢ J(a | 2 * b) = J(a | 2 * b / 2)
have neg₅ : 1 * J(a | b) = J(a | b)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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)
⊢ J(a | 2 * b) = J(a | 2 * b / 2)
have neg₆ : J(a | b) = J(a | b)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : b = 1
⊢ J(a | b) = 1
have pos : J(a | 1) = 1
Tactic: rw [hb1, one_right]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ J(a | b) = 1
have pos₁ : Eq (α := ℤ) 1 1
Tactic: rw [hb1, one_right]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ J(a | b) = 0
have pos : J(a % (↑b : ℤ) | b) = 0
Tactic: rw [mod_left, hab, zero_left (lt_of_le_of_ne (Nat.pos_of_ne_zero hb0) (Ne.symm hb1))]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ J(a | b) = 0
have pos₁ : J(0 | b) = 0
Tactic: rw [mod_left, hab, zero_left (lt_of_le_of_ne (Nat.pos_of_ne_zero hb0) (Ne.symm hb1))]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ J(a | b) = 0
have pos₂ : Eq (α := ℤ) 0 0
Tactic: rw [mod_left, hab, zero_left (lt_of_le_of_ne (Nat.pos_of_ne_zero hb0) (Ne.symm hb1))]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ J(a | b) = fastJacobiSymAux (a % (↑b : ℤ)).natAbs b false ⋯
have neg : b % 2 = 1
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))]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ J(a | b) = fastJacobiSymAux (a % (↑b : ℤ)).natAbs b false ⋯
have neg₁ : b > 1
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))]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
⊢ J(a | b) = fastJacobiSym a b
have h : ∀ (b : ℕ) (IH : ∀ m < b, J(a | m) = fastJacobiSym a m), 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)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
⊢ legendreSym = fastLegendreSym
have h : ∀ (p : ℕ) (x : Fact (Nat.Prime p)) (a : ℤ), legendreSym p a = fastLegendreSym p a
Tactic: ext p _ a
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
⊢ legendreSym p a = fastLegendreSym p a
have h : J(a | p) = fastLegendreSym p a
Tactic: rw [legendreSym.to_jacobiSym, fastLegendreSym]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
p : ℕ
h_1 : Fact (Nat.Prime p)
a : ℤ
h : J(a | p) = fastLegendreSym p a
⊢ legendreSym p a = fastLegendreSym p a
have h₁ : J(a | p) = J(a | p)
Tactic: rw [legendreSym.to_jacobiSym, fastLegendreSym]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
⊢ quadraticCharFun F a = 1
have simp : ¬IsSquare a → Eq (α := ℤ) (-1) 1
Tactic: simp only [quadraticCharFun, ha, if_false, ite_eq_left_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
⊢ quadraticCharFun F a = if a ^ (Fintype.card F / 2) = 1 then 1 else -1
have simp : Eq (α := ℤ) (if IsSquare a then 1 else -1) (if a ^ (Fintype.card F / 2) = 1 then 1 else -1)
Tactic: simp only [quadraticCharFun, ha, if_false]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a b : F
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
have pos : ∀ (ha : a = 0), quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
have neg : ∀ (ha : ¬a = 0), quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a b : F
ha : a = 0
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
have pos : quadraticCharFun F (0 * b) = quadraticCharFun F 0 * quadraticCharFun F b
Tactic: rw [ha, zero_mul, quadraticCharFun_zero, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
have pos₁ : quadraticCharFun F 0 = quadraticCharFun F 0 * quadraticCharFun F b
Tactic: rw [ha, zero_mul, quadraticCharFun_zero, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
have pos₂ : 0 = 0 * quadraticCharFun F b
Tactic: rw [ha, zero_mul, quadraticCharFun_zero, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
have pos₃ : Eq (α := ℤ) 0 0
Tactic: rw [ha, zero_mul, quadraticCharFun_zero, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a b : F
ha : ¬a = 0
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
have pos : ∀ (hb : b = 0), quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
Tactic: by_cases hb : b = 0
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
have neg : ∀ (hb : ¬b = 0), quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
Tactic: by_cases hb : b = 0
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
have pos : quadraticCharFun F (a * 0) = quadraticCharFun F a * quadraticCharFun F 0
Tactic: rw [hb, mul_zero, quadraticCharFun_zero, mul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
have pos₁ : quadraticCharFun F 0 = quadraticCharFun F a * quadraticCharFun F 0
Tactic: rw [hb, mul_zero, quadraticCharFun_zero, mul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
have pos₂ : 0 = quadraticCharFun F a * 0
Tactic: rw [hb, mul_zero, quadraticCharFun_zero, mul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
have pos₃ : Eq (α := ℤ) 0 0
Tactic: rw [hb, mul_zero, quadraticCharFun_zero, mul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (hypothesis)
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
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
have hab : a * b ≠ 0
Tactic: have hab := mul_ne_zero ha hb
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
have pos : ∀ (hF : ringChar F = 2), quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
Tactic: by_cases hF : ringChar F = 2
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
have neg : ∀ (hF : ¬ringChar F = 2), quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
Tactic: by_cases hF : ringChar F = 2
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
have pos : quadraticCharFun F (a * b) = 1 * 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]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
have pos₁ : quadraticCharFun F (a * b) = HMul.hMul (α := ℤ) 1 1
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]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
have pos₂ : 1 = HMul.hMul (α := ℤ) 1 1
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]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
have pos₃ : Eq (α := ℤ) 1 1
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]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
have 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)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
⊢ (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)
have 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)
Tactic: rcases FiniteField.pow_dichotomy hF hb with hb' | hb'
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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)
⊢ (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)
have 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)
Tactic: rcases FiniteField.pow_dichotomy hF hb with hb' | hb'
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (hypothesis)
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)
have h : Ne.{u_1 + 1} (α := F) (-1) 1
Tactic: have h := Ring.neg_one_ne_one_of_char_ne_two hF
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
⊢ (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)
have neg : 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 [hb', mul_neg, mul_one, h, if_false]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
⊢ Eq (α := ℤ) (if -a ^ (Fintype.card F / 2) = 1 then 1 else -1) (-if a ^ (Fintype.card F / 2) = 1 then 1 else -1)
have 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)
Tactic: rcases FiniteField.pow_dichotomy hF ha with ha' | ha'
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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)
⊢ Eq (α := ℤ) (if -a ^ (Fintype.card F / 2) = 1 then 1 else -1) (-if a ^ (Fintype.card F / 2) = 1 then 1 else -1)
have 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)
Tactic: rcases FiniteField.pow_dichotomy hF ha with ha' | ha'
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a : F
ha : ¬IsUnit a
⊢ quadraticCharFun F a = 0
have rw : quadraticCharFun F 0 = 0
Tactic: rw [of_not_not (mt Ne.isUnit ha)]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Fintype F
inst_2 : DecidableEq F
a : F
ha : a ≠ 0
⊢ HPow.hPow (α := ℤ) (β := ℕ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) 2 = 1
have rwa : HMul.hMul (α := ℤ) (β := ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) = 1
Tactic: rwa [pow_two, ← map_mul, ← pow_two, quadraticChar_sq_one']
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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
⊢ HPow.hPow (α := ℤ) (β := ℕ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) 2 = 1
have rwa₁ : Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (a * a) : ℤ) (1 : ℤ)
Tactic: rwa [pow_two, ← map_mul, ← pow_two, quadraticChar_sq_one']
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (goal)
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 : ℤ)
⊢ HPow.hPow (α := ℤ) (β := ℕ) ((quadraticChar F : (a : F) → ℤ) a : ℤ) 2 = 1
have rwa₂ : Eq (α := ℤ) ((quadraticChar F : (a : F) → ℤ) (HPow.hPow (β := ℕ) a 2) : ℤ) (1 : ℤ)
Tactic: rwa [pow_two, ← map_mul, ← pow_two, quadraticChar_sq_one']