awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
Goal:
p q : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Fact (Nat.Prime q)
hp : p % 4 = 3
hq : q % 4 = 3
nop : ∀ {n : ℕ} (hn : n % 4 = 3), HPow.hPow (α := ℤ) (-1) (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
hp₁ : p % 2 = 1
hp₂ : Eq (α := ℕ) 1 1
hp₃ : p % 4 = 3
hp₄ : Eq (α := ℕ) 1 1
hp₅ hp₆ hp₇ : p % 4 = 3
⊢ p ≠ 2

Tactic:
rwa [← Prime.mod_two_eq_one_iff_ne_two Fact.out, odd_of_mod_four_eq_three]

Premises used: Nat.Prime.mod_two_eq_one_iff_ne_two, Nat.odd_of_mod_four_eq_three, Fact.out
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
Goal:
p q : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Fact (Nat.Prime q)
hp : p % 4 = 3
hq : q % 4 = 3
nop : ∀ {n : ℕ} (hn : n % 4 = 3), HPow.hPow (α := ℤ) (-1) (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
hq₁ : q % 2 = 1
hq₂ : Eq (α := ℕ) 1 1
hq₃ : q % 4 = 3
hq₄ : Eq (α := ℕ) 1 1
hq₅ hq₆ hq₇ : q % 4 = 3
⊢ q ≠ 2

Tactic:
rwa [← Prime.mod_two_eq_one_iff_ne_two Fact.out, odd_of_mod_four_eq_three]

Premises used: Nat.Prime.mod_two_eq_one_iff_ne_two, Nat.odd_of_mod_four_eq_three, Fact.out
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
Goal:
p q : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Fact (Nat.Prime q)
hp1 : p % 4 = 1
hq1 : q ≠ 2
inl :
  ∀ [inst_2 : Fact (Nat.Prime p)] (hq1 : p ≠ 2),
    IsSquare (α := ZMod p) (↑p : ZMod p) ↔ IsSquare (α := ZMod p) (↑p : ZMod p)
inr : ∀ (h : p ≠ q), IsSquare (α := ZMod p) (↑q : ZMod p) ↔ IsSquare (α := ZMod q) (↑p : ZMod q)
⊢ IsSquare (α := ZMod p) (↑q : ZMod p) ↔ IsSquare (α := ZMod q) (↑p : ZMod q)

Tactic:
rcases eq_or_ne p q with rfl | h

Premises used: eq_or_ne, rfl
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp1 : p % 4 = 1
inst_1 : Fact (Nat.Prime p)
hq1 : p ≠ 2
⊢ IsSquare (α := ZMod p) (↑p : ZMod p) ↔ IsSquare (α := ZMod p) (↑p : ZMod p)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
Goal:
p q : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Fact (Nat.Prime q)
hp1 : p % 4 = 1
hq1 : q ≠ 2
h : p ≠ q
inr : legendreSym p (↑q : ℤ) = 1 ↔ IsSquare (α := ZMod q) (↑p : ZMod q)
inr₁ : legendreSym p (↑q : ℤ) = 1 ↔ legendreSym q (↑p : ℤ) = 1
inr₂ inr₃ : legendreSym p (↑q : ℤ) = 1 ↔ legendreSym p (↑q : ℤ) = 1
⊢ IsSquare (α := ZMod p) (↑q : ZMod p) ↔ IsSquare (α := ZMod q) (↑p : ZMod q)

Tactic:
rw [← eq_one_iff' p (prime_ne_zero p q h), ← eq_one_iff' q (prime_ne_zero q p h.symm),
      quadratic_reciprocity_one_mod_four hp1 hq1]

Premises used: Ne.symm, legendreSym.eq_one_iff', ZMod.prime_ne_zero, legendreSym.quadratic_reciprocity_one_mod_four
-- Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
Goal:
p q : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Fact (Nat.Prime q)
hp3 : p % 4 = 3
hq3 : q % 4 = 3
hpq : p ≠ q
rw : legendreSym p (↑q : ℤ) = 1 ↔ ¬IsSquare (α := ZMod q) (↑p : ZMod q)
rw₁ : legendreSym p (↑q : ℤ) = 1 ↔ legendreSym q (↑p : ℤ) = -1
rw₂ : legendreSym p (↑q : ℤ) = 1 ↔ -legendreSym p (↑q : ℤ) = -1
rw₃ rw₄ : legendreSym p (↑q : ℤ) = 1 ↔ legendreSym p (↑q : ℤ) = 1
⊢ IsSquare (α := ZMod p) (↑q : ZMod p) ↔ ¬IsSquare (α := ZMod q) (↑p : ZMod q)

Tactic:
rw [← eq_one_iff' p (prime_ne_zero p q hpq), ← eq_neg_one_iff' q,
    quadratic_reciprocity_three_mod_four hp3 hq3, neg_inj]

Premises used: legendreSym.quadratic_reciprocity_three_mod_four, legendreSym.eq_one_iff', neg_inj, ZMod.prime_ne_zero, legendreSym.eq_neg_one_iff'
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
⊢ ∀ (x y : ZMod 4),
    (match (motive := ZMod 4 → ℤ) x * y with
      | 0 => 0
      | 2 => 0
      | 1 => 1
      | 3 => -1) =
      HMul.hMul (α := ℤ) (β := ℤ)
        (match (motive := ZMod 4 → ℤ) x with
          | 0 => 0
          | 2 => 0
          | 1 => 1
          | 3 => -1 :
          ℤ)
        (match (motive := ZMod 4 → ℤ) y with
          | 0 => 0
          | 2 => 0
          | 1 => 1
          | 3 => -1 :
          ℤ)

Tactic:
decide
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
⊢ ∀ (a : ZMod 4),
    ¬IsUnit a →
      Eq (α := ℤ)
        (match (motive := ZMod 4 → ℤ) a with
          | 0 => 0
          | 2 => 0
          | 1 => 1
          | 3 => -1 :
          ℤ)
        (0 : ℤ)

Tactic:
decide
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
⊢ ∀ (a : ZMod 4),
    Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) a : ℤ) (0 : ℤ) ∨
      Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) a : ℤ) (1 : ℤ) ∨ Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) a : ℤ) (-1 : ℤ)

Tactic:
decide
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℕ
⊢ Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑n : ZMod 4) : ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(n % 4) : ZMod 4) : ℤ)

Tactic:
grind
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℤ
rw :
  Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(n % (↑4 : ℤ)) : ZMod 4) : ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(n % 4) : ZMod 4) : ℤ)
rw₁ rw₂ :
  Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(n % 4) : ZMod 4) : ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(n % 4) : ZMod 4) : ℤ)
⊢ Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑n : ZMod 4) : ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(n % 4) : ZMod 4) : ℤ)

Tactic:
rw [← ZMod.intCast_mod n 4, Nat.cast_ofNat]

Premises used: Nat.cast_ofNat, ZMod.intCast_mod, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℤ
⊢ ∀ (m : ℤ),
    0 ≤ m →
      m < 4 →
        Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) : ℤ) (if m % 2 = 0 then 0 else if m = 1 then 1 else -1 : ℤ)

Tactic:
decide
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℤ
⊢ ∀ (m : ℤ),
    0 ≤ m →
      m < 4 →
        Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) : ℤ) (if m % 2 = 0 then 0 else if m = 1 then 1 else -1 : ℤ)

Tactic:
have help : ∀ m : ℤ, 0 ≤ m → m < 4 → χ₄ m = if m % 2 = 0 then 0 else if m = 1 then 1 else -1 := by
    decide
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℤ
help :
  ∀ (m : ℤ),
    0 ≤ m →
      m < 4 →
        Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) : ℤ) (if m % 2 = 0 then 0 else if m = 1 then 1 else -1 : ℤ)
⊢ Dvd.dvd (α := ℤ) 2 4

Tactic:
lia
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℤ
help :
  ∀ (m : ℤ),
    0 ≤ m →
      m < 4 →
        Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) : ℤ) (if m % 2 = 0 then 0 else if m = 1 then 1 else -1 : ℤ)
rw :
  Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(n % (↑4 : ℤ)) : ZMod 4) : ℤ)
    (if n % 4 % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1 : ℤ)
⊢ Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑n : ZMod 4) : ℤ) (if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1 : ℤ)

Tactic:
rw [← Int.emod_emod_of_dvd n (by lia : (2 : ℤ) ∣ 4), ← ZMod.intCast_mod n 4]

Premises used: ZMod.intCast_mod, Int.emod_emod_of_dvd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℤ
help :
  ∀ (m : ℤ),
    0 ≤ m →
      m < 4 →
        Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) : ℤ) (if m % 2 = 0 then 0 else if m = 1 then 1 else -1 : ℤ)
⊢ Ne (α := ℤ) 4 0

Tactic:
lia
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℤ
help :
  ∀ (m : ℤ),
    0 ≤ m →
      m < 4 →
        Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) : ℤ) (if m % 2 = 0 then 0 else if m = 1 then 1 else -1 : ℤ)
⊢ Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(n % (↑4 : ℤ)) : ZMod 4) : ℤ)
    (if n % 4 % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1 : ℤ)

Tactic:
exact help (n % 4) (Int.emod_nonneg n (by lia)) (Int.emod_lt_abs n (by lia))

Premises used: HMod.hMod, OfNat.ofNat, Int.emod_nonneg
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℕ
⊢ Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑n : ZMod 4) : ℤ) (if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1 : ℤ)

Tactic:
mod_cast χ₄_int_eq_if_mod_four n

Premises used: Int.cast, Int.cast_natCast, ZMod.χ₄, congrArg, Int.cast_negSucc._simp_1, cast, Nat.cast, HMod.hMod, congr, Eq.refl, Nat.cast_inj._simp_1, ZMod.χ₄_int_eq_if_mod_four, Nat.cast_zero, Int.negSucc, ite_congr, OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, DFunLike.coe, Neg.neg, Eq.trans
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℕ
hn : n % 2 = 1
rw : (if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1) = HPow.hPow (α := ℤ) (-1) (n / 2)
⊢ (χ₄ : (a : ZMod 4) → ℤ) (↑n : ZMod 4) = HPow.hPow (α := ℤ) (-1) (n / 2)

Tactic:
rw [χ₄_nat_eq_if_mod_four]

Premises used: ZMod.χ₄_nat_eq_if_mod_four
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℕ
hn : n % 2 = 1
simp : (if n % 4 = 1 then 1 else -1) = HPow.hPow (α := ℤ) (-1) (n / 2)
⊢ (if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1) = HPow.hPow (α := ℤ) (-1) (n / 2)

Tactic:
simp only [hn, Nat.one_ne_zero, if_false]

Premises used: if_false, Nat.one_ne_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℕ
hn : n % 2 = 1
nth_rewrite : (if n % 4 = 1 then 1 else -1) = HPow.hPow (α := ℤ) (-1) ((4 * (n / 4) + n % 4) / 2)
⊢ (if n % 4 = 1 then 1 else -1) = HPow.hPow (α := ℤ) (-1) (n / 2)

Tactic:
nth_rewrite 3 [← Nat.div_add_mod n 4]

Premises used: Nat.div_add_mod, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℕ
hn : n % 2 = 1
⊢ 4 = HMul.hMul (α := ℕ) 2 2

Tactic:
lia
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℕ
hn : n % 2 = 1
rw : (if n % 4 = 1 then 1 else -1) = HPow.hPow (α := ℤ) (-1) (n % 4 / 2)
⊢ (if n % 4 = 1 then 1 else -1) = HPow.hPow (α := ℤ) (-1) ((HMul.hMul (α := ℕ) 2 2 * (n / 4) + n % 4) / 2)

Tactic:
rw [mul_assoc, add_comm, Nat.add_mul_div_left _ _ zero_lt_two, pow_add, pow_mul,
    neg_one_sq, one_pow, mul_one]

Premises used: one_pow, neg_one_sq, mul_assoc, pow_add, add_comm, pow_mul, Nat.add_mul_div_left, mul_one, zero_lt_two
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℕ
hn : n % 2 = 1
⊢ ∀ m < 4, m % 2 = 1 → (if m = 1 then 1 else -1) = HPow.hPow (α := ℤ) (-1) (m / 2)

Tactic:
decide
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℕ
hn : n % 2 = 1
⊢ ∀ m < 4, m % 2 = 1 → (if m = 1 then 1 else -1) = HPow.hPow (α := ℤ) (-1) (m / 2)

Tactic:
have help : ∀ m : ℕ, m < 4 → m % 2 = 1 → ite (m = 1) (1 : ℤ) (-1) = (-1) ^ (m / 2) := by decide
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℕ
hn : n % 2 = 1
help : ∀ m < 4, m % 2 = 1 → (if m = 1 then 1 else -1) = HPow.hPow (α := ℤ) (-1) (m / 2)
⊢ LT.lt (α := ℕ) 0 4

Tactic:
lia
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℕ
hn : n % 2 = 1
help : ∀ m < 4, m % 2 = 1 → (if m = 1 then 1 else -1) = HPow.hPow (α := ℤ) (-1) (m / 2)
⊢ Dvd.dvd (α := ℕ) 2 4

Tactic:
lia
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℕ
hn : n % 2 = 1
help : ∀ m < 4, m % 2 = 1 → (if m = 1 then 1 else -1) = HPow.hPow (α := ℤ) (-1) (m / 2)
⊢ (if n % 4 = 1 then 1 else -1) = HPow.hPow (α := ℤ) (-1) (n % 4 / 2)

Tactic:
exact help _ (Nat.mod_lt n (by lia)) <| (Nat.mod_mod_of_dvd n (by lia : 2 ∣ 4)).trans hn

Premises used: Nat.mod_lt, Nat.mod_mod_of_dvd, Eq.trans
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℕ
hn : n % 4 = 1
rw : Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑1 : ZMod 4) : ℤ) (1 : ℤ)
⊢ Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑n : ZMod 4) : ℤ) (1 : ℤ)

Tactic:
rw [χ₄_nat_mod_four, hn]

Premises used: ZMod.χ₄_nat_mod_four
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℕ
hn : n % 4 = 1
⊢ Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑1 : ZMod 4) : ℤ) (1 : ℤ)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℕ
hn : n % 4 = 3
rw : Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑3 : ZMod 4) : ℤ) (-1 : ℤ)
⊢ Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑n : ZMod 4) : ℤ) (-1 : ℤ)

Tactic:
rw [χ₄_nat_mod_four, hn]

Premises used: ZMod.χ₄_nat_mod_four
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℕ
hn : n % 4 = 3
⊢ Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑3 : ZMod 4) : ℤ) (-1 : ℤ)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℤ
hn : n % 4 = 1
rw : Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑1 : ZMod 4) : ℤ) (1 : ℤ)
⊢ Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑n : ZMod 4) : ℤ) (1 : ℤ)

Tactic:
rw [χ₄_int_mod_four, hn]

Premises used: ZMod.χ₄_int_mod_four
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℤ
hn : n % 4 = 1
⊢ Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑1 : ZMod 4) : ℤ) (1 : ℤ)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℤ
hn : n % 4 = 3
rw : Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑3 : ZMod 4) : ℤ) (-1 : ℤ)
⊢ Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑n : ZMod 4) : ℤ) (-1 : ℤ)

Tactic:
rw [χ₄_int_mod_four, hn]

Premises used: ZMod.χ₄_int_mod_four
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℤ
hn : n % 4 = 3
⊢ Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑3 : ZMod 4) : ℤ) (-1 : ℤ)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℕ
hn : n % 4 = 1
⊢ HPow.hPow (α := ℤ) (-1) (n / 2) = 1

Tactic:
χ₄_eq_neg_one_pow (Nat.odd_of_mod_four_eq_one hn) ▸ χ₄_nat_one_mod_four hn

Premises used: Nat.odd_of_mod_four_eq_one, Eq.rec, ZMod.χ₄_nat_one_mod_four, ZMod.χ₄_eq_neg_one_pow
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℕ
hn : n % 4 = 3
⊢ HPow.hPow (α := ℤ) (-1) (n / 2) = -1

Tactic:
χ₄_eq_neg_one_pow (Nat.odd_of_mod_four_eq_three hn) ▸ χ₄_nat_three_mod_four hn

Premises used: Eq.rec, ZMod.χ₄_nat_three_mod_four, Nat.odd_of_mod_four_eq_three, ZMod.χ₄_eq_neg_one_pow
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
⊢ ∀ (x y : ZMod 8),
    (match (motive := ZMod 8 → ℤ) x * y with
      | 0 => 0
      | 2 => 0
      | 4 => 0
      | 6 => 0
      | 1 => 1
      | 7 => 1
      | 3 => -1
      | 5 => -1) =
      HMul.hMul (α := ℤ) (β := ℤ)
        (match (motive := ZMod 8 → ℤ) x with
          | 0 => 0
          | 2 => 0
          | 4 => 0
          | 6 => 0
          | 1 => 1
          | 7 => 1
          | 3 => -1
          | 5 => -1 :
          ℤ)
        (match (motive := ZMod 8 → ℤ) y with
          | 0 => 0
          | 2 => 0
          | 4 => 0
          | 6 => 0
          | 1 => 1
          | 7 => 1
          | 3 => -1
          | 5 => -1 :
          ℤ)

Tactic:
decide
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
⊢ ∀ (a : ZMod 8),
    ¬IsUnit a →
      Eq (α := ℤ)
        (match (motive := ZMod 8 → ℤ) a with
          | 0 => 0
          | 2 => 0
          | 4 => 0
          | 6 => 0
          | 1 => 1
          | 7 => 1
          | 3 => -1
          | 5 => -1 :
          ℤ)
        (0 : ℤ)

Tactic:
decide
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
⊢ ∀ (a : ZMod 8),
    Eq (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) a : ℤ) (0 : ℤ) ∨
      Eq (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) a : ℤ) (1 : ℤ) ∨ Eq (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) a : ℤ) (-1 : ℤ)

Tactic:
decide
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℕ
rw rw₁ : Eq (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑(n % 8) : ZMod 8) : ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑(n % 8) : ZMod 8) : ℤ)
⊢ Eq (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑n : ZMod 8) : ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑(n % 8) : ZMod 8) : ℤ)

Tactic:
rw [← ZMod.natCast_mod n 8]

Premises used: ZMod.natCast_mod, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℤ
rw :
  Eq (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑(n % (↑8 : ℤ)) : ZMod 8) : ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑(n % 8) : ZMod 8) : ℤ)
rw₁ rw₂ :
  Eq (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑(n % 8) : ZMod 8) : ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑(n % 8) : ZMod 8) : ℤ)
⊢ Eq (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑n : ZMod 8) : ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑(n % 8) : ZMod 8) : ℤ)

Tactic:
rw [← ZMod.intCast_mod n 8, Nat.cast_ofNat]

Premises used: Nat.cast_ofNat, ZMod.intCast_mod, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℤ
⊢ ∀ (m : ℤ),
    0 ≤ m →
      m < 8 →
        Eq (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑m : ZMod 8) : ℤ)
          (if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1 : ℤ)

Tactic:
decide
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℤ
⊢ ∀ (m : ℤ),
    0 ≤ m →
      m < 8 →
        Eq (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑m : ZMod 8) : ℤ)
          (if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1 : ℤ)

Tactic:
have help :
    ∀ m : ℤ, 0 ≤ m → m < 8 → χ₈ m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1 := by
    decide
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℤ
help :
  ∀ (m : ℤ),
    0 ≤ m →
      m < 8 →
        Eq (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑m : ZMod 8) : ℤ)
          (if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1 : ℤ)
⊢ Dvd.dvd (α := ℤ) 2 8

Tactic:
lia
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℤ
help :
  ∀ (m : ℤ),
    0 ≤ m →
      m < 8 →
        Eq (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑m : ZMod 8) : ℤ)
          (if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1 : ℤ)
rw :
  Eq (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑(n % (↑8 : ℤ)) : ZMod 8) : ℤ)
    (if n % 8 % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 7 then 1 else -1 : ℤ)
⊢ Eq (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑n : ZMod 8) : ℤ)
    (if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 7 then 1 else -1 : ℤ)

Tactic:
rw [← Int.emod_emod_of_dvd n (by lia : (2 : ℤ) ∣ 8), ← ZMod.intCast_mod n 8]

Premises used: ZMod.intCast_mod, Int.emod_emod_of_dvd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℤ
help :
  ∀ (m : ℤ),
    0 ≤ m →
      m < 8 →
        Eq (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑m : ZMod 8) : ℤ)
          (if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1 : ℤ)
⊢ Ne (α := ℤ) 8 0

Tactic:
lia
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℤ
help :
  ∀ (m : ℤ),
    0 ≤ m →
      m < 8 →
        Eq (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑m : ZMod 8) : ℤ)
          (if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1 : ℤ)
⊢ Eq (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑(n % (↑8 : ℤ)) : ZMod 8) : ℤ)
    (if n % 8 % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 7 then 1 else -1 : ℤ)

Tactic:
exact help (n % 8) (Int.emod_nonneg n (by lia)) (Int.emod_lt_abs n (by lia))

Premises used: HMod.hMod, OfNat.ofNat, Int.emod_nonneg
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℕ
⊢ Eq (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑n : ZMod 8) : ℤ)
    (if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 7 then 1 else -1 : ℤ)

Tactic:
mod_cast χ₈_int_eq_if_mod_eight n

Premises used: Int.cast, Int.cast_natCast, ZMod.χ₈, congrArg, Int.cast_negSucc._simp_1, cast, Nat.cast, HMod.hMod, congr, Eq.refl, Nat.cast_inj._simp_1, congrFun', Or, Nat.cast_zero, Int.negSucc, ite_congr, OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, DFunLike.coe, Neg.neg, Eq.trans, ZMod.χ₈_int_eq_if_mod_eight
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
⊢ ∀ (x y : ZMod 8),
    (match (motive := ZMod 8 → ℤ) x * y with
      | 0 => 0
      | 2 => 0
      | 4 => 0
      | 6 => 0
      | 1 => 1
      | 3 => 1
      | 5 => -1
      | 7 => -1) =
      HMul.hMul (α := ℤ) (β := ℤ)
        (match (motive := ZMod 8 → ℤ) x with
          | 0 => 0
          | 2 => 0
          | 4 => 0
          | 6 => 0
          | 1 => 1
          | 3 => 1
          | 5 => -1
          | 7 => -1 :
          ℤ)
        (match (motive := ZMod 8 → ℤ) y with
          | 0 => 0
          | 2 => 0
          | 4 => 0
          | 6 => 0
          | 1 => 1
          | 3 => 1
          | 5 => -1
          | 7 => -1 :
          ℤ)

Tactic:
decide
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
⊢ ∀ (a : ZMod 8),
    ¬IsUnit a →
      Eq (α := ℤ)
        (match (motive := ZMod 8 → ℤ) a with
          | 0 => 0
          | 2 => 0
          | 4 => 0
          | 6 => 0
          | 1 => 1
          | 3 => 1
          | 5 => -1
          | 7 => -1 :
          ℤ)
        (0 : ℤ)

Tactic:
decide
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
⊢ ∀ (a : ZMod 8),
    Eq (α := ℤ) ((χ₈' : (a : ZMod 8) → ℤ) a : ℤ) (0 : ℤ) ∨
      Eq (α := ℤ) ((χ₈' : (a : ZMod 8) → ℤ) a : ℤ) (1 : ℤ) ∨ Eq (α := ℤ) ((χ₈' : (a : ZMod 8) → ℤ) a : ℤ) (-1 : ℤ)

Tactic:
decide
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℤ
⊢ ∀ (m : ℤ),
    0 ≤ m →
      m < 8 →
        Eq (α := ℤ) ((χ₈' : (a : ZMod 8) → ℤ) (↑m : ZMod 8) : ℤ)
          (if m % 2 = 0 then 0 else if m = 1 ∨ m = 3 then 1 else -1 : ℤ)

Tactic:
decide
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℤ
⊢ ∀ (m : ℤ),
    0 ≤ m →
      m < 8 →
        Eq (α := ℤ) ((χ₈' : (a : ZMod 8) → ℤ) (↑m : ZMod 8) : ℤ)
          (if m % 2 = 0 then 0 else if m = 1 ∨ m = 3 then 1 else -1 : ℤ)

Tactic:
have help :
    ∀ m : ℤ, 0 ≤ m → m < 8 → χ₈' m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 3 then 1 else -1 := by
    decide
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℤ
help :
  ∀ (m : ℤ),
    0 ≤ m →
      m < 8 →
        Eq (α := ℤ) ((χ₈' : (a : ZMod 8) → ℤ) (↑m : ZMod 8) : ℤ)
          (if m % 2 = 0 then 0 else if m = 1 ∨ m = 3 then 1 else -1 : ℤ)
⊢ Dvd.dvd (α := ℤ) 2 8

Tactic:
lia
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℤ
help :
  ∀ (m : ℤ),
    0 ≤ m →
      m < 8 →
        Eq (α := ℤ) ((χ₈' : (a : ZMod 8) → ℤ) (↑m : ZMod 8) : ℤ)
          (if m % 2 = 0 then 0 else if m = 1 ∨ m = 3 then 1 else -1 : ℤ)
rw :
  Eq (α := ℤ) ((χ₈' : (a : ZMod 8) → ℤ) (↑(n % (↑8 : ℤ)) : ZMod 8) : ℤ)
    (if n % 8 % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 3 then 1 else -1 : ℤ)
⊢ Eq (α := ℤ) ((χ₈' : (a : ZMod 8) → ℤ) (↑n : ZMod 8) : ℤ)
    (if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 3 then 1 else -1 : ℤ)

Tactic:
rw [← Int.emod_emod_of_dvd n (by lia : (2 : ℤ) ∣ 8), ← ZMod.intCast_mod n 8]

Premises used: ZMod.intCast_mod, Int.emod_emod_of_dvd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℤ
help :
  ∀ (m : ℤ),
    0 ≤ m →
      m < 8 →
        Eq (α := ℤ) ((χ₈' : (a : ZMod 8) → ℤ) (↑m : ZMod 8) : ℤ)
          (if m % 2 = 0 then 0 else if m = 1 ∨ m = 3 then 1 else -1 : ℤ)
⊢ Ne (α := ℤ) 8 0

Tactic:
lia
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℤ
help :
  ∀ (m : ℤ),
    0 ≤ m →
      m < 8 →
        Eq (α := ℤ) ((χ₈' : (a : ZMod 8) → ℤ) (↑m : ZMod 8) : ℤ)
          (if m % 2 = 0 then 0 else if m = 1 ∨ m = 3 then 1 else -1 : ℤ)
⊢ Eq (α := ℤ) ((χ₈' : (a : ZMod 8) → ℤ) (↑(n % (↑8 : ℤ)) : ZMod 8) : ℤ)
    (if n % 8 % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 3 then 1 else -1 : ℤ)

Tactic:
exact help (n % 8) (Int.emod_nonneg n (by lia)) (Int.emod_lt_abs n (by lia))

Premises used: HMod.hMod, OfNat.ofNat, Int.emod_nonneg
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
n : ℕ
⊢ Eq (α := ℤ) ((χ₈' : (a : ZMod 8) → ℤ) (↑n : ZMod 8) : ℤ)
    (if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 3 then 1 else -1 : ℤ)

Tactic:
mod_cast χ₈'_int_eq_if_mod_eight n

Premises used: ZMod.χ₈'_int_eq_if_mod_eight, Int.cast, Int.cast_natCast, congrArg, Int.cast_negSucc._simp_1, cast, Nat.cast, HMod.hMod, congr, Eq.refl, Nat.cast_inj._simp_1, congrFun', ZMod.χ₈', Or, Nat.cast_zero, Int.negSucc, ite_congr, OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, DFunLike.coe, Neg.neg, Eq.trans
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
⊢ ∀ (a : ZMod 8),
    (χ₈' : (a : ZMod 8) → ℤ) a =
      HMul.hMul (α := ℤ) (β := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) a.cast : ℤ) ((χ₈ : (a : ZMod 8) → ℤ) a : ℤ)

Tactic:
decide
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
a : ℤ
⊢ Dvd.dvd (α := ℕ) 4 8

Tactic:
lia
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
a : ℤ
rw :
  (χ₈' : (a : ZMod 8) → ℤ) (↑a : ZMod 8) =
    HMul.hMul (α := ℤ) (β := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (cast (n := 8) (↑a : ZMod 8)) : ℤ)
      ((χ₈ : (a : ZMod 8) → ℤ) (↑a : ZMod 8) : ℤ)
⊢ (χ₈' : (a : ZMod 8) → ℤ) (↑a : ZMod 8) =
    HMul.hMul (α := ℤ) (β := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑a : ZMod 4) : ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑a : ZMod 8) : ℤ)

Tactic:
rw [← @cast_intCast 8 (ZMod 4) _ 4 _ (by lia) a]

Premises used: ZMod.cast_intCast
-- Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar
Goal:
a : ℤ
⊢ (χ₈' : (a : ZMod 8) → ℤ) (↑a : ZMod 8) =
    HMul.hMul (α := ℤ) (β := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (cast (n := 8) (↑a : ZMod 8)) : ℤ)
      ((χ₈ : (a : ZMod 8) → ℤ) (↑a : ZMod 8) : ℤ)

Tactic:
χ₈'_eq_χ₄_mul_χ₈ a

Premises used: Int.cast, ZMod.χ₈'_eq_χ₄_mul_χ₈