awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
hap : Ne (α := ZMod p) (↑a : ZMod p) 0
⊢ Ne (α := ZMod p) (↑(p / 2)! : ZMod p) 0
have rw : p / 2 < p
Tactic: rw [Ne, CharP.cast_eq_zero_iff (ZMod p) p, hp.1.dvd_factorial, not_le]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (hypothesis)
Goal:
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
hp : p ≠ 2
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
⊢ 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})
have hp₁ : Odd p
Tactic: replace hp : Odd p := h.out.odd_of_ne_two hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
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)
have 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)
Tactic: rw [legendreSym.eq_pow, gauss_lemma_aux p ha0]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
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)
⊢ 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)
have 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)
Tactic: rw [legendreSym.eq_pow, gauss_lemma_aux p ha0]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (hypothesis)
Goal:
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
hp : Odd p
⊢ 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})
have 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)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
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)
⊢ 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})
have 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})
Tactic: cases legendreSym.eq_one_or_neg_one p ha0
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
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})
⊢ 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})
have 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})
Tactic: cases legendreSym.eq_one_or_neg_one p ha0
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
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
⊢ 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})
have 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})
Tactic: cases neg_one_pow_eq_or ℤ #{x ∈ Ico 1 (p / 2).succ | p / 2 < (a * x.cast : ZMod p).val}
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
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})
⊢ 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})
have 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})
Tactic: cases neg_one_pow_eq_or ℤ #{x ∈ Ico 1 (p / 2).succ | p / 2 < (a * x.cast : ZMod p).val}
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
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
⊢ 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})
have 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})
Tactic: cases neg_one_pow_eq_or ℤ #{x ∈ Ico 1 (p / 2).succ | p / 2 < (a * x.cast : ZMod p).val}
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
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})
⊢ 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})
have 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})
Tactic: cases neg_one_pow_eq_or ℤ #{x ∈ Ico 1 (p / 2).succ | p / 2 < (a * x.cast : ZMod p).val}
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
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, val (n := p) (↑(a * x) : ZMod p)) : ZMod 2)
      (↑(∑ x ∈ Ico 1 (p / 2).succ, a * x / p) : ZMod 2)
have 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)
Tactic: simp only [val_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
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)).valMinAbs +
            (↑(if (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val ≤ p / 2 then 0 else p) : ℤ)) :
        ZMod 2))
have 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))
Tactic: simp only [(val_eq_ite_valMinAbs _).symm]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
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)
⊢ 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)
have 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)
Tactic: rw [Finset.sum_eq_multiset_sum, Ico_map_valMinAbs_natAbs_eq_Ico_map_id p a hap, ←
              Finset.sum_eq_multiset_sum]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
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)
⊢ 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)
have 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)
Tactic: rw [Finset.sum_eq_multiset_sum, Ico_map_valMinAbs_natAbs_eq_Ico_map_id p a hap, ←
              Finset.sum_eq_multiset_sum]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
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)
⊢ 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)
have 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)
Tactic: rw [Finset.sum_eq_multiset_sum, Ico_map_valMinAbs_natAbs_eq_Ico_map_id p a hap, ←
              Finset.sum_eq_multiset_sum]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (hypothesis)
Goal:
a b c : ℕ
hb0 : 0 < b
hc : a / b ≤ c
x : ℕ
⊢ x ∈ Ico 1 (a / b).succ ↔ x ∈ {x ∈ Ico 1 c.succ | x * b ≤ a}
have this : x * b ≤ a → x ≤ c
Tactic: have : x * b ≤ a → x ≤ c := fun h => le_trans (by rwa [le_div_iff_mul_le hb0]) hc
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
Goal:
a b c : ℕ
hb0 : 0 < b
hc : a / b ≤ c
x : ℕ
this : x * b ≤ a → x ≤ c
⊢ x ∈ Ico 1 (a / b).succ ↔ x ∈ {x ∈ Ico 1 c.succ | x * b ≤ a}
have simp : x * b ≤ a → 1 ≤ x → x ≤ c
Tactic: simp [le_div_iff_mul_le hb0]