awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
hap : Ne (α := ZMod p) (↑a : ZMod p) 0
x : ℕ
h : x ∈ Ico 1 (p / 2).succ
pos :
  (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val ≤ p / 2 →
    (↑(HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val : ZMod p) =
      1 * HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)
neg :
  ¬(HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val ≤ p / 2 →
    (↑(HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val : ZMod p) =
      -1 * -HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)
⊢ (↑(HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val : ZMod p) =
    (if (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val ≤ p / 2 then 1 else -1) *
      if (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val ≤ p / 2 then
        HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)
      else -HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
hap : Ne (α := ZMod p) (↑a : ZMod p) 0
x : ℕ
h : x ∈ Ico 1 (p / 2).succ
h_1 : (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val ≤ p / 2
⊢ (↑(HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val : ZMod p) =
    1 * HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)

Tactic:
simp
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
hap : Ne (α := ZMod p) (↑a : ZMod p) 0
x : ℕ
h : x ∈ Ico 1 (p / 2).succ
h_1 : ¬(HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val ≤ p / 2
⊢ (↑(HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val : ZMod p) =
    -1 * -HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)

Tactic:
simp
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
hap : Ne (α := ZMod p) (↑a : ZMod p) 0
rw :
  HMul.hMul (α := ZMod p)
        (∏ x ∈ Ico 1 (p / 2).succ with (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val ≤ p / 2, 1)
        (∏ x ∈ Ico 1 (p / 2).succ with ¬(HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val ≤ p / 2, -1) *
      ∏ x ∈ Ico 1 (p / 2).succ, (↑(HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).valMinAbs.natAbs : ZMod p) =
    HPow.hPow (α := ZMod p) (-1)
        #({x ∈ Ico 1 (p / 2).succ | ¬(HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val ≤ p / 2}) *
      ∏ x ∈ Ico 1 (p / 2).succ, (↑(HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).valMinAbs.natAbs : ZMod p)
⊢ ∏ x ∈ Ico 1 (p / 2).succ,
      HMul.hMul (α := ZMod p) (if (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val ≤ p / 2 then 1 else -1)
        (↑(HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).valMinAbs.natAbs : ZMod p) =
    HPow.hPow (α := ZMod p) (-1)
        #({x ∈ Ico 1 (p / 2).succ | ¬(HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val ≤ p / 2}) *
      ∏ x ∈ Ico 1 (p / 2).succ, (↑(HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).valMinAbs.natAbs : ZMod p)

Tactic:
rw [prod_mul_distrib, Finset.prod_ite]

Premises used: Finset.prod_mul_distrib, Finset.prod_ite
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
hap : Ne (α := ZMod p) (↑a : ZMod p) 0
⊢ HMul.hMul (α := ZMod p)
        (∏ x ∈ Ico 1 (p / 2).succ with (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val ≤ p / 2, 1)
        (∏ x ∈ Ico 1 (p / 2).succ with ¬(HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val ≤ p / 2, -1) *
      ∏ x ∈ Ico 1 (p / 2).succ, (↑(HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).valMinAbs.natAbs : ZMod p) =
    HPow.hPow (α := ZMod p) (-1)
        #({x ∈ Ico 1 (p / 2).succ | ¬(HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val ≤ p / 2}) *
      ∏ x ∈ Ico 1 (p / 2).succ, (↑(HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).valMinAbs.natAbs : ZMod p)

Tactic:
simp
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
hap : Ne (α := ZMod p) (↑a : ZMod p) 0
rw :
  HPow.hPow (α := ZMod p) (-1)
        #({x ∈ Ico 1 (p / 2).succ | ¬(HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val ≤ p / 2}) *
      (↑(∏ i ∈ Ico 1 (p / 2).succ, (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑i : ZMod p)).valMinAbs.natAbs) : ZMod p) =
    HPow.hPow (α := ZMod p) (-1)
        #({x ∈ Ico 1 (p / 2).succ | ¬(HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val ≤ p / 2}) *
      (↑(p / 2)! : ZMod p)
rw₁ :
  HPow.hPow (α := ZMod p) (-1)
        #({x ∈ Ico 1 (p / 2).succ | ¬(HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val ≤ p / 2}) *
      (↑(Multiset.prod
            (Multiset.map (fun (i : ℕ) ↦ (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑i : ZMod p)).valMinAbs.natAbs)
              (Ico 1 (p / 2).succ).val)) :
        ZMod p) =
    HPow.hPow (α := ZMod p) (-1)
        #({x ∈ Ico 1 (p / 2).succ | ¬(HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val ≤ p / 2}) *
      (↑(p / 2)! : ZMod p)
rw₂ :
  HPow.hPow (α := ZMod p) (-1)
        #({x ∈ Ico 1 (p / 2).succ | ¬(HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val ≤ p / 2}) *
      (↑(Multiset.prod (Multiset.map (fun (a : ℕ) ↦ a) (Ico 1 (p / 2).succ).val)) : ZMod p) =
    HPow.hPow (α := ZMod p) (-1)
        #({x ∈ Ico 1 (p / 2).succ | ¬(HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val ≤ p / 2}) *
      (↑(p / 2)! : ZMod p)
rw₃ :
  HPow.hPow (α := ZMod p) (-1)
        #({x ∈ Ico 1 (p / 2).succ | ¬(HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val ≤ p / 2}) *
      (↑(∏ x ∈ Ico 1 (p / 2).succ, x) : ZMod p) =
    HPow.hPow (α := ZMod p) (-1)
        #({x ∈ Ico 1 (p / 2).succ | ¬(HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val ≤ p / 2}) *
      (↑(p / 2)! : ZMod p)
rw₄ rw₅ :
  HPow.hPow (α := ZMod p) (-1)
        #({x ∈ Ico 1 (p / 2).succ | ¬(HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val ≤ p / 2}) *
      (↑(p / 2)! : ZMod p) =
    HPow.hPow (α := ZMod p) (-1)
        #({x ∈ Ico 1 (p / 2).succ | ¬(HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val ≤ p / 2}) *
      (↑(p / 2)! : ZMod p)
⊢ HPow.hPow (α := ZMod p) (-1)
        #({x ∈ Ico 1 (p / 2).succ | ¬(HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val ≤ p / 2}) *
      ∏ x ∈ Ico 1 (p / 2).succ, (↑(HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).valMinAbs.natAbs : ZMod p) =
    HPow.hPow (α := ZMod p) (-1)
        #({x ∈ Ico 1 (p / 2).succ | ¬(HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val ≤ p / 2}) *
      (↑(p / 2)! : ZMod p)

Tactic:
rw [← prod_natCast, Finset.prod_eq_multiset_prod,
        Ico_map_valMinAbs_natAbs_eq_Ico_map_id p a hap, ← Finset.prod_eq_multiset_prod,
        prod_Ico_id_eq_factorial]

Premises used: Int.cast, Finset.prod_Ico_id_eq_factorial, ZMod.Ico_map_valMinAbs_natAbs_eq_Ico_map_id, Finset.prod_eq_multiset_prod, Finset.prod_natCast
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
hap : Ne (α := ZMod p) (↑a : ZMod p) 0
rw : p / 2 < p
⊢ Ne (α := ZMod p) (↑(p / 2)! : ZMod p) 0

Tactic:
rw [Ne, CharP.cast_eq_zero_iff (ZMod p) p, hp.1.dvd_factorial, not_le]

Premises used: not_le, Nat.Prime.dvd_factorial, Ne, ZMod, CharP.cast_eq_zero_iff, Fact.out
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
hap : Ne (α := ZMod p) (↑a : ZMod p) 0
⊢ LT.lt (α := ℕ) 1 2

Tactic:
decide
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
hap : Ne (α := ZMod p) (↑a : ZMod p) 0
⊢ p / 2 < p

Tactic:
exact Nat.div_lt_self hp.1.pos (by decide)

Premises used: Nat.div_lt_self, Nat.Prime.pos, Fact.out
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
hap : Ne (α := ZMod p) (↑a : ZMod p) 0
⊢ HPow.hPow (α := ZMod p) (↑a : ZMod p) (p / 2) * (↑(p / 2)! : ZMod p) =
    HMul.hMul (α := ZMod p)
      (↑(HPow.hPow (α := ℤ) (-1)
            #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val})) :
        ZMod p)
      (↑(p / 2)! : ZMod p)

Tactic:
simpa using gauss_lemma_aux₁ p hap

Premises used: _private.0.ZMod.gauss_lemma_aux₁
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
hp : p ≠ 2
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
⊢ Odd p

Tactic:
replace hp : Odd p := h.out.odd_of_ne_two hp
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
hp : Odd p
rw :
  HPow.hPow (α := ZMod p) (↑a : ZMod p) (p / 2) =
    (↑(HPow.hPow (α := ℤ) (-1)
          #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val})) :
      ZMod p)
rw₁ rw₂ :
  Eq (α := ZMod p)
    (↑(HPow.hPow (α := ℤ) (-1)
          #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val})) :
      ZMod p)
    (↑(HPow.hPow (α := ℤ) (-1)
          #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val})) :
      ZMod p)
⊢ Eq (α := ZMod p) (↑(legendreSym p a) : ZMod p)
    (↑(HPow.hPow (α := ℤ) (-1)
          #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val})) :
      ZMod p)

Tactic:
rw [legendreSym.eq_pow, gauss_lemma_aux p ha0]

Premises used: legendreSym.eq_pow, ZMod.gauss_lemma_aux
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
hp : Odd p
⊢ Eq (α := ZMod p) (↑(legendreSym p a) : ZMod p)
    (↑(HPow.hPow (α := ℤ) (-1)
          #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val})) :
      ZMod p)

Tactic:
have : (legendreSym p a : ZMod p) =
      (((-1) ^ #{x ∈ Ico 1 (p / 2).succ | p / 2 < (a * x.cast : ZMod p).val} : ℤ) : ZMod p) := by
    rw [legendreSym.eq_pow, gauss_lemma_aux p ha0]
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
hp : Odd p
this :
  Eq (α := ZMod p) (↑(legendreSym p a) : ZMod p)
    (↑(HPow.hPow (α := ℤ) (-1)
          #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val})) :
      ZMod p)
inl :
  legendreSym p a = 1 →
    legendreSym p a =
      HPow.hPow (α := ℤ) (-1)
        #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val})
inr :
  legendreSym p a = -1 →
    legendreSym p a =
      HPow.hPow (α := ℤ) (-1)
        #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val})
⊢ legendreSym p a =
    HPow.hPow (α := ℤ) (-1)
      #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val})

Tactic:
cases legendreSym.eq_one_or_neg_one p ha0

Premises used: legendreSym.eq_one_or_neg_one
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
hp : Odd p
this :
  Eq (α := ZMod p) (↑(legendreSym p a) : ZMod p)
    (↑(HPow.hPow (α := ℤ) (-1)
          #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val})) :
      ZMod p)
h_1 : legendreSym p a = 1
inl :
  HPow.hPow (α := ℤ) (-1)
        #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val}) =
      1 →
    legendreSym p a =
      HPow.hPow (α := ℤ) (-1)
        #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val})
inl₁ :
  HPow.hPow (α := ℤ) (-1)
        #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val}) =
      -1 →
    legendreSym p a =
      HPow.hPow (α := ℤ) (-1)
        #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val})
⊢ legendreSym p a =
    HPow.hPow (α := ℤ) (-1)
      #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val})

Tactic:
cases neg_one_pow_eq_or ℤ #{x ∈ Ico 1 (p / 2).succ | p / 2 < (a * x.cast : ZMod p).val}

Premises used: Int.cast, HMul.hMul, Finset.Ico, HDiv.hDiv, Int, LT.lt, Finset.card, neg_one_pow_eq_or, OfNat.ofNat, Finset.filter, Nat.succ, ZMod.val
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
hp : Odd p
this :
  Eq (α := ZMod p) (↑(legendreSym p a) : ZMod p)
    (↑(HPow.hPow (α := ℤ) (-1)
          #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val})) :
      ZMod p)
h_1 : legendreSym p a = -1
inr :
  HPow.hPow (α := ℤ) (-1)
        #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val}) =
      1 →
    legendreSym p a =
      HPow.hPow (α := ℤ) (-1)
        #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val})
inr₁ :
  HPow.hPow (α := ℤ) (-1)
        #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val}) =
      -1 →
    legendreSym p a =
      HPow.hPow (α := ℤ) (-1)
        #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val})
⊢ legendreSym p a =
    HPow.hPow (α := ℤ) (-1)
      #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val})

Tactic:
cases neg_one_pow_eq_or ℤ #{x ∈ Ico 1 (p / 2).succ | p / 2 < (a * x.cast : ZMod p).val}

Premises used: Int.cast, HMul.hMul, Finset.Ico, HDiv.hDiv, Int, LT.lt, Finset.card, neg_one_pow_eq_or, OfNat.ofNat, Finset.filter, Nat.succ, ZMod.val
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
hp : Odd p
this :
  Eq (α := ZMod p) (↑(legendreSym p a) : ZMod p)
    (↑(HPow.hPow (α := ℤ) (-1)
          #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val})) :
      ZMod p)
h_1 : legendreSym p a = 1
h_2 :
  HPow.hPow (α := ℤ) (-1)
      #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val}) =
    1
⊢ legendreSym p a =
    HPow.hPow (α := ℤ) (-1)
      #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val})

Tactic:
simp_all [ne_neg_self hp one_ne_zero, (ne_neg_self hp one_ne_zero).symm]

Premises used: ZMod.ne_neg_self, Ne.symm, one_ne_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
hp : Odd p
this :
  Eq (α := ZMod p) (↑(legendreSym p a) : ZMod p)
    (↑(HPow.hPow (α := ℤ) (-1)
          #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val})) :
      ZMod p)
h_1 : legendreSym p a = 1
h_2 :
  HPow.hPow (α := ℤ) (-1)
      #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val}) =
    -1
⊢ legendreSym p a =
    HPow.hPow (α := ℤ) (-1)
      #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val})

Tactic:
simp_all [ne_neg_self hp one_ne_zero, (ne_neg_self hp one_ne_zero).symm]

Premises used: ZMod.ne_neg_self, Ne.symm, one_ne_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
hp : Odd p
this :
  Eq (α := ZMod p) (↑(legendreSym p a) : ZMod p)
    (↑(HPow.hPow (α := ℤ) (-1)
          #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val})) :
      ZMod p)
h_1 : legendreSym p a = -1
h_2 :
  HPow.hPow (α := ℤ) (-1)
      #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val}) =
    1
⊢ legendreSym p a =
    HPow.hPow (α := ℤ) (-1)
      #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val})

Tactic:
simp_all [ne_neg_self hp one_ne_zero, (ne_neg_self hp one_ne_zero).symm]

Premises used: ZMod.ne_neg_self, Ne.symm, one_ne_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
hp : Odd p
this :
  Eq (α := ZMod p) (↑(legendreSym p a) : ZMod p)
    (↑(HPow.hPow (α := ℤ) (-1)
          #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val})) :
      ZMod p)
h_1 : legendreSym p a = -1
h_2 :
  HPow.hPow (α := ℤ) (-1)
      #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val}) =
    -1
⊢ legendreSym p a =
    HPow.hPow (α := ℤ) (-1)
      #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val})

Tactic:
simp_all [ne_neg_self hp one_ne_zero, (ne_neg_self hp one_ne_zero).symm]

Premises used: ZMod.ne_neg_self, Ne.symm, one_ne_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp2_1 : Fact (p % 2 = 1)
a : ℕ
hap : Ne (α := ZMod p) (↑a : ZMod p) 0
hp2 : Eq (α := ZMod 2) (↑p : ZMod 2) (↑1 : ZMod 2)
⊢ Eq (α := ZMod 2) (↑(∑ x ∈ Ico 1 (p / 2).succ, a * x) : ZMod 2)
    (↑(∑ x ∈ Ico 1 (p / 2).succ, (a * x % p + p * (a * x / p))) : ZMod 2)

Tactic:
simp only [mod_add_div]

Premises used: Nat.mod_add_div
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp2_1 : Fact (p % 2 = 1)
a : ℕ
hap : Ne (α := ZMod p) (↑a : ZMod p) 0
hp2 : Eq (α := ZMod 2) (↑p : ZMod 2) (↑1 : ZMod 2)
simp :
  (↑(∑ x ∈ Ico 1 (p / 2).succ, (a * x % p + p * (a * x / p))) : ZMod 2) =
    HAdd.hAdd (α := ZMod 2) (↑(∑ x ∈ Ico 1 (p / 2).succ, a * x % p) : ZMod 2)
      (↑(∑ x ∈ Ico 1 (p / 2).succ, a * x / p) : ZMod 2)
⊢ (↑(∑ x ∈ Ico 1 (p / 2).succ, (a * x % p + p * (a * x / p))) : ZMod 2) =
    HAdd.hAdd (α := ZMod 2) (↑(∑ x ∈ Ico 1 (p / 2).succ, val (n := p) (↑(a * x) : ZMod p)) : ZMod 2)
      (↑(∑ x ∈ Ico 1 (p / 2).succ, a * x / p) : ZMod 2)

Tactic:
simp only [val_natCast]

Premises used: ZMod.val_natCast
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp2_1 : Fact (p % 2 = 1)
a : ℕ
hap : Ne (α := ZMod p) (↑a : ZMod p) 0
hp2 : Eq (α := ZMod 2) (↑p : ZMod 2) (↑1 : ZMod 2)
⊢ (↑(∑ x ∈ Ico 1 (p / 2).succ, (a * x % p + p * (a * x / p))) : ZMod 2) =
    HAdd.hAdd (α := ZMod 2) (↑(∑ x ∈ Ico 1 (p / 2).succ, a * x % p) : ZMod 2)
      (↑(∑ x ∈ Ico 1 (p / 2).succ, a * x / p) : ZMod 2)

Tactic:
simp [sum_add_distrib, ← mul_sum, Nat.cast_add, Nat.cast_mul, Nat.cast_sum, hp2]

Premises used: Finset.mul_sum, Finset.sum_add_distrib, Nat.cast_add, Nat.cast_sum, Nat.cast_mul
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp2_1 : Fact (p % 2 = 1)
a : ℕ
hap : Ne (α := ZMod p) (↑a : ZMod p) 0
hp2 : Eq (α := ZMod 2) (↑p : ZMod 2) (↑1 : ZMod 2)
simp :
  Eq (α := ZMod 2) (↑(∑ x ∈ Ico 1 (p / 2).succ, val (n := p) (↑(a * x) : ZMod p)) : ZMod 2)
    (∑ x ∈ Ico 1 (p / 2).succ, (↑(↑(HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val : ℤ) : ZMod 2))
⊢ Eq (α := ZMod 2) (↑(∑ x ∈ Ico 1 (p / 2).succ, val (n := p) (↑(a * x) : ZMod p)) : ZMod 2)
    (∑ x ∈ Ico 1 (p / 2).succ,
      (↑((HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).valMinAbs +
            (↑(if (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val ≤ p / 2 then 0 else p) : ℤ)) :
        ZMod 2))

Tactic:
simp only [(val_eq_ite_valMinAbs _).symm]

Premises used: ZMod.val_eq_ite_valMinAbs, Eq.symm
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp2_1 : Fact (p % 2 = 1)
a : ℕ
hap : Ne (α := ZMod p) (↑a : ZMod p) 0
hp2 : Eq (α := ZMod 2) (↑p : ZMod 2) (↑1 : ZMod 2)
⊢ Eq (α := ZMod 2) (↑(∑ x ∈ Ico 1 (p / 2).succ, val (n := p) (↑(a * x) : ZMod p)) : ZMod 2)
    (∑ x ∈ Ico 1 (p / 2).succ, (↑(↑(HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val : ℤ) : ZMod 2))

Tactic:
simp [Nat.cast_sum]

Premises used: Nat.cast_sum
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp2_1 : Fact (p % 2 = 1)
a : ℕ
hap : Ne (α := ZMod p) (↑a : ZMod p) 0
hp2 : Eq (α := ZMod 2) (↑p : ZMod 2) (↑1 : ZMod 2)
⊢ ∑ x ∈ Ico 1 (p / 2).succ,
      (↑((HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).valMinAbs +
            (↑(if (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val ≤ p / 2 then 0 else p) : ℤ)) :
        ZMod 2) =
    HAdd.hAdd (α := ZMod 2)
      (↑(#({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val})) : ZMod 2)
      (↑(∑ x ∈ Ico 1 (p / 2).succ, (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).valMinAbs.natAbs) : ZMod 2)

Tactic:
simp [add_comm, sum_add_distrib, Finset.sum_ite, hp2, Nat.cast_sum]

Premises used: Finset.sum_add_distrib, add_comm, Nat.cast_sum, Finset.sum_ite
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp2_1 : Fact (p % 2 = 1)
a : ℕ
hap : Ne (α := ZMod p) (↑a : ZMod p) 0
hp2 : Eq (α := ZMod 2) (↑p : ZMod 2) (↑1 : ZMod 2)
rw :
  HAdd.hAdd (α := ZMod 2)
      (↑(#({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val})) : ZMod 2)
      (↑(Multiset.sum
            (Multiset.map (fun (x : ℕ) ↦ (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).valMinAbs.natAbs)
              (Ico 1 (p / 2).succ).val)) :
        ZMod 2) =
    HAdd.hAdd (α := ZMod 2)
      (↑(#({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val})) : ZMod 2)
      (↑(∑ x ∈ Ico 1 (p / 2).succ, x) : ZMod 2)
rw₁ :
  HAdd.hAdd (α := ZMod 2)
      (↑(#({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val})) : ZMod 2)
      (↑(Multiset.sum (Multiset.map (fun (a : ℕ) ↦ a) (Ico 1 (p / 2).succ).val)) : ZMod 2) =
    HAdd.hAdd (α := ZMod 2)
      (↑(#({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val})) : ZMod 2)
      (↑(∑ x ∈ Ico 1 (p / 2).succ, x) : ZMod 2)
rw₂ rw₃ :
  HAdd.hAdd (α := ZMod 2)
      (↑(#({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val})) : ZMod 2)
      (↑(∑ x ∈ Ico 1 (p / 2).succ, x) : ZMod 2) =
    HAdd.hAdd (α := ZMod 2)
      (↑(#({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val})) : ZMod 2)
      (↑(∑ x ∈ Ico 1 (p / 2).succ, x) : ZMod 2)
⊢ HAdd.hAdd (α := ZMod 2)
      (↑(#({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val})) : ZMod 2)
      (↑(∑ x ∈ Ico 1 (p / 2).succ, (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).valMinAbs.natAbs) : ZMod 2) =
    HAdd.hAdd (α := ZMod 2)
      (↑(#({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val})) : ZMod 2)
      (↑(∑ x ∈ Ico 1 (p / 2).succ, x) : ZMod 2)

Tactic:
rw [Finset.sum_eq_multiset_sum, Ico_map_valMinAbs_natAbs_eq_Ico_map_id p a hap, ←
              Finset.sum_eq_multiset_sum]

Premises used: Nat.cast, Finset.sum_eq_multiset_sum, ZMod.Ico_map_valMinAbs_natAbs_eq_Ico_map_id
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Fact (p % 2 = 1)
a : ℕ
ha2_1 : a % 2 = 1
hap : Ne (α := ZMod p) (↑a : ZMod p) 0
ha2 : Eq (α := ZMod 2) (↑a : ZMod 2) (↑1 : ZMod 2)
⊢ HSub.hSub (α := ZMod 2)
      (↑(#({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val})) : ZMod 2)
      (↑(∑ x ∈ Ico 1 (p / 2).succ, x * a / p) : ZMod 2) =
    0

Tactic:
simpa [add_left_comm, sub_eq_add_neg, ← mul_sum, mul_comm, ha2, Nat.cast_sum,
      add_neg_eq_iff_eq_add.symm, add_assoc] using
      Eq.symm (eisenstein_lemma_aux₁ p hap)

Premises used: Finset.mul_sum, add_left_comm, add_assoc, sub_eq_add_neg, Nat.cast_sum, mul_comm, _private.0.ZMod.eisenstein_lemma_aux₁, Eq.symm, Iff.symm, add_neg_eq_iff_eq_add
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
a b c : ℕ
hb0 : 0 < b
hc : a / b ≤ c
⊢ a / b = #(Ico 1 (a / b).succ)

Tactic:
simp