awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * (↑x : ZMod p)).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
⊢ 1 ≤ ((↑b : ZMod p) / a).valMinAbs.natAbs
have refine_1 : ((↑b : ZMod p) / a).valMinAbs.natAbs ≠ 0
Tactic: apply Nat.pos_of_ne_zero
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * (↑x : ZMod p)).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
⊢ ((↑b : ZMod p) / a).valMinAbs.natAbs < (p / 2).succ
have refine_2 : ((↑b : ZMod p) / a).valMinAbs.natAbs ≤ p / 2
Tactic: apply lt_succ_of_le
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * (↑x : ZMod p)).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
⊢ (a * (↑((↑b : ZMod p) / a).valMinAbs.natAbs : ZMod p)).valMinAbs.natAbs = b
have refine_3 : (a * if ((↑b : ZMod p) / a).val ≤ p / 2 then (↑b : ZMod p) / a else -((↑b : ZMod p) / a)).valMinAbs.natAbs = b
Tactic: rw [natCast_natAbs_valMinAbs]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * (↑x : ZMod p)).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
⊢ (a * if ((↑b : ZMod p) / a).val ≤ p / 2 then (↑b : ZMod p) / a else -((↑b : ZMod p) / a)).valMinAbs.natAbs = b
have pos : ((↑b : ZMod p) / a).val ≤ p / 2 → (a * ((↑b : ZMod p) / a)).valMinAbs.natAbs = b
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * (↑x : ZMod p)).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
pos : ((↑b : ZMod p) / a).val ≤ p / 2 → (a * ((↑b : ZMod p) / a)).valMinAbs.natAbs = b
⊢ (a * if ((↑b : ZMod p) / a).val ≤ p / 2 then (↑b : ZMod p) / a else -((↑b : ZMod p) / a)).valMinAbs.natAbs = b
have neg : ¬((↑b : ZMod p) / a).val ≤ p / 2 → (a * -((↑b : ZMod p) / a)).valMinAbs.natAbs = b
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * (↑x : ZMod p)).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
h : ((↑b : ZMod p) / a).val ≤ p / 2
⊢ (a * ((↑b : ZMod p) / a)).valMinAbs.natAbs = b
have pos : (valMinAbs (n := p) (↑b : ZMod p)).natAbs = b
Tactic: rw [mul_div_cancel₀ _ hap, valMinAbs_def_pos, val_cast_of_lt (hep hb),
          if_pos (le_of_lt_succ (mem_Ico.1 hb).2), Int.natAbs_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * (↑x : ZMod p)).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
h : ((↑b : ZMod p) / a).val ≤ p / 2
pos : (valMinAbs (n := p) (↑b : ZMod p)).natAbs = b
⊢ (a * ((↑b : ZMod p) / a)).valMinAbs.natAbs = b
have pos₁ : (if val (n := p) (↑b : ZMod p) ≤ p / 2 then (↑(val (n := p) (↑b : ZMod p)) : ℤ)
    else HSub.hSub (α := ℤ) (↑(val (n := p) (↑b : ZMod p)) : ℤ) (↑p : ℤ)).natAbs =
  b
Tactic: rw [mul_div_cancel₀ _ hap, valMinAbs_def_pos, val_cast_of_lt (hep hb),
          if_pos (le_of_lt_succ (mem_Ico.1 hb).2), Int.natAbs_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * (↑x : ZMod p)).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
h : ((↑b : ZMod p) / a).val ≤ p / 2
pos : (valMinAbs (n := p) (↑b : ZMod p)).natAbs = b
pos₁ :
  (if val (n := p) (↑b : ZMod p) ≤ p / 2 then (↑(val (n := p) (↑b : ZMod p)) : ℤ)
      else HSub.hSub (α := ℤ) (↑(val (n := p) (↑b : ZMod p)) : ℤ) (↑p : ℤ)).natAbs =
    b
⊢ (a * ((↑b : ZMod p) / a)).valMinAbs.natAbs = b
have pos₂ : (if b ≤ p / 2 then (↑b : ℤ) else HSub.hSub (α := ℤ) (↑b : ℤ) (↑p : ℤ)).natAbs = b
Tactic: rw [mul_div_cancel₀ _ hap, valMinAbs_def_pos, val_cast_of_lt (hep hb),
          if_pos (le_of_lt_succ (mem_Ico.1 hb).2), Int.natAbs_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * (↑x : ZMod p)).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
h : ((↑b : ZMod p) / a).val ≤ p / 2
pos : (valMinAbs (n := p) (↑b : ZMod p)).natAbs = b
pos₁ :
  (if val (n := p) (↑b : ZMod p) ≤ p / 2 then (↑(val (n := p) (↑b : ZMod p)) : ℤ)
      else HSub.hSub (α := ℤ) (↑(val (n := p) (↑b : ZMod p)) : ℤ) (↑p : ℤ)).natAbs =
    b
pos₂ : (if b ≤ p / 2 then (↑b : ℤ) else HSub.hSub (α := ℤ) (↑b : ℤ) (↑p : ℤ)).natAbs = b
⊢ (a * ((↑b : ZMod p) / a)).valMinAbs.natAbs = b
have pos₃ : Int.natAbs (↑b : ℤ) = b
Tactic: rw [mul_div_cancel₀ _ hap, valMinAbs_def_pos, val_cast_of_lt (hep hb),
          if_pos (le_of_lt_succ (mem_Ico.1 hb).2), Int.natAbs_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * (↑x : ZMod p)).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
h : ((↑b : ZMod p) / a).val ≤ p / 2
pos : (valMinAbs (n := p) (↑b : ZMod p)).natAbs = b
pos₁ :
  (if val (n := p) (↑b : ZMod p) ≤ p / 2 then (↑(val (n := p) (↑b : ZMod p)) : ℤ)
      else HSub.hSub (α := ℤ) (↑(val (n := p) (↑b : ZMod p)) : ℤ) (↑p : ℤ)).natAbs =
    b
pos₂ : (if b ≤ p / 2 then (↑b : ℤ) else HSub.hSub (α := ℤ) (↑b : ℤ) (↑p : ℤ)).natAbs = b
pos₃ : Int.natAbs (↑b : ℤ) = b
⊢ (a * ((↑b : ZMod p) / a)).valMinAbs.natAbs = b
have pos₄ : b = b
Tactic: rw [mul_div_cancel₀ _ hap, valMinAbs_def_pos, val_cast_of_lt (hep hb),
          if_pos (le_of_lt_succ (mem_Ico.1 hb).2), Int.natAbs_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * (↑x : ZMod p)).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
h : ¬((↑b : ZMod p) / a).val ≤ p / 2
⊢ (a * -((↑b : ZMod p) / a)).valMinAbs.natAbs = b
have neg : (-(a * ((↑b : ZMod p) / a))).valMinAbs.natAbs = b
Tactic: rw [mul_neg, mul_div_cancel₀ _ hap, natAbs_valMinAbs_neg, valMinAbs_def_pos,
          val_cast_of_lt (hep hb), if_pos (le_of_lt_succ (mem_Ico.1 hb).2), Int.natAbs_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * (↑x : ZMod p)).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
h : ¬((↑b : ZMod p) / a).val ≤ p / 2
neg : (-(a * ((↑b : ZMod p) / a))).valMinAbs.natAbs = b
⊢ (a * -((↑b : ZMod p) / a)).valMinAbs.natAbs = b
have neg₁ : (valMinAbs (n := p) (-(↑b : ZMod p))).natAbs = b
Tactic: rw [mul_neg, mul_div_cancel₀ _ hap, natAbs_valMinAbs_neg, valMinAbs_def_pos,
          val_cast_of_lt (hep hb), if_pos (le_of_lt_succ (mem_Ico.1 hb).2), Int.natAbs_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * (↑x : ZMod p)).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
h : ¬((↑b : ZMod p) / a).val ≤ p / 2
neg : (-(a * ((↑b : ZMod p) / a))).valMinAbs.natAbs = b
neg₁ : (valMinAbs (n := p) (-(↑b : ZMod p))).natAbs = b
⊢ (a * -((↑b : ZMod p) / a)).valMinAbs.natAbs = b
have neg₂ : (valMinAbs (n := p) (↑b : ZMod p)).natAbs = b
Tactic: rw [mul_neg, mul_div_cancel₀ _ hap, natAbs_valMinAbs_neg, valMinAbs_def_pos,
          val_cast_of_lt (hep hb), if_pos (le_of_lt_succ (mem_Ico.1 hb).2), Int.natAbs_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * (↑x : ZMod p)).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
h : ¬((↑b : ZMod p) / a).val ≤ p / 2
neg : (-(a * ((↑b : ZMod p) / a))).valMinAbs.natAbs = b
neg₁ : (valMinAbs (n := p) (-(↑b : ZMod p))).natAbs = b
neg₂ : (valMinAbs (n := p) (↑b : ZMod p)).natAbs = b
⊢ (a * -((↑b : ZMod p) / a)).valMinAbs.natAbs = b
have neg₃ : (if val (n := p) (↑b : ZMod p) ≤ p / 2 then (↑(val (n := p) (↑b : ZMod p)) : ℤ)
    else HSub.hSub (α := ℤ) (↑(val (n := p) (↑b : ZMod p)) : ℤ) (↑p : ℤ)).natAbs =
  b
Tactic: rw [mul_neg, mul_div_cancel₀ _ hap, natAbs_valMinAbs_neg, valMinAbs_def_pos,
          val_cast_of_lt (hep hb), if_pos (le_of_lt_succ (mem_Ico.1 hb).2), Int.natAbs_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * (↑x : ZMod p)).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
h : ¬((↑b : ZMod p) / a).val ≤ p / 2
neg : (-(a * ((↑b : ZMod p) / a))).valMinAbs.natAbs = b
neg₁ : (valMinAbs (n := p) (-(↑b : ZMod p))).natAbs = b
neg₂ : (valMinAbs (n := p) (↑b : ZMod p)).natAbs = b
neg₃ :
  (if val (n := p) (↑b : ZMod p) ≤ p / 2 then (↑(val (n := p) (↑b : ZMod p)) : ℤ)
      else HSub.hSub (α := ℤ) (↑(val (n := p) (↑b : ZMod p)) : ℤ) (↑p : ℤ)).natAbs =
    b
⊢ (a * -((↑b : ZMod p) / a)).valMinAbs.natAbs = b
have neg₄ : (if b ≤ p / 2 then (↑b : ℤ) else HSub.hSub (α := ℤ) (↑b : ℤ) (↑p : ℤ)).natAbs = b
Tactic: rw [mul_neg, mul_div_cancel₀ _ hap, natAbs_valMinAbs_neg, valMinAbs_def_pos,
          val_cast_of_lt (hep hb), if_pos (le_of_lt_succ (mem_Ico.1 hb).2), Int.natAbs_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * (↑x : ZMod p)).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
h : ¬((↑b : ZMod p) / a).val ≤ p / 2
neg : (-(a * ((↑b : ZMod p) / a))).valMinAbs.natAbs = b
neg₁ : (valMinAbs (n := p) (-(↑b : ZMod p))).natAbs = b
neg₂ : (valMinAbs (n := p) (↑b : ZMod p)).natAbs = b
neg₃ :
  (if val (n := p) (↑b : ZMod p) ≤ p / 2 then (↑(val (n := p) (↑b : ZMod p)) : ℤ)
      else HSub.hSub (α := ℤ) (↑(val (n := p) (↑b : ZMod p)) : ℤ) (↑p : ℤ)).natAbs =
    b
neg₄ : (if b ≤ p / 2 then (↑b : ℤ) else HSub.hSub (α := ℤ) (↑b : ℤ) (↑p : ℤ)).natAbs = b
⊢ (a * -((↑b : ZMod p) / a)).valMinAbs.natAbs = b
have neg₅ : Int.natAbs (↑b : ℤ) = b
Tactic: rw [mul_neg, mul_div_cancel₀ _ hap, natAbs_valMinAbs_neg, valMinAbs_def_pos,
          val_cast_of_lt (hep hb), if_pos (le_of_lt_succ (mem_Ico.1 hb).2), Int.natAbs_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * (↑x : ZMod p)).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
h : ¬((↑b : ZMod p) / a).val ≤ p / 2
neg : (-(a * ((↑b : ZMod p) / a))).valMinAbs.natAbs = b
neg₁ : (valMinAbs (n := p) (-(↑b : ZMod p))).natAbs = b
neg₂ : (valMinAbs (n := p) (↑b : ZMod p)).natAbs = b
neg₃ :
  (if val (n := p) (↑b : ZMod p) ≤ p / 2 then (↑(val (n := p) (↑b : ZMod p)) : ℤ)
      else HSub.hSub (α := ℤ) (↑(val (n := p) (↑b : ZMod p)) : ℤ) (↑p : ℤ)).natAbs =
    b
neg₄ : (if b ≤ p / 2 then (↑b : ℤ) else HSub.hSub (α := ℤ) (↑b : ℤ) (↑p : ℤ)).natAbs = b
neg₅ : Int.natAbs (↑b : ℤ) = b
⊢ (a * -((↑b : ZMod p) / a)).valMinAbs.natAbs = b
have neg₆ : b = b
Tactic: rw [mul_neg, mul_div_cancel₀ _ hap, natAbs_valMinAbs_neg, valMinAbs_def_pos,
          val_cast_of_lt (hep hb), if_pos (le_of_lt_succ (mem_Ico.1 hb).2), Int.natAbs_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * (↑x : ZMod p)).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
⊢ Eq (α := Multiset ℕ) (Multiset.map (fun (x : ℕ) ↦ (a * (↑x : ZMod p)).valMinAbs.natAbs) (Ico 1 (p / 2).succ).val)
    (Multiset.map (fun (a : ℕ) ↦ a) (Ico 1 (p / 2).succ).val)
have hsurj : ∀ (b : ℕ) (hb : b ∈ Ico 1 (p / 2).succ),
  ∃ (x : ℕ) (_ : x ∈ Ico 1 (p / 2).succ), (a * (↑x : ZMod p)).valMinAbs.natAbs = b
Tactic: have hsurj : ∀ (b : ℕ) (hb : b ∈ Ico 1 (p / 2).succ),
      ∃ x, ∃ _ : x ∈ Ico 1 (p / 2).succ, (a * x : ZMod p).valMinAbs.natAbs = b := by
    intro b hb
    refine ⟨(b / a : ZMod p).valMinAbs.natAbs, mem_Ico.mpr ⟨?_, ?_⟩, ?_⟩
    · apply Nat.pos_of_ne_zero
      simp only [div_eq_mul_inv, hap, CharP.cast_eq_zero_iff (ZMod p) p, hpe hb, not_false_iff,
        valMinAbs_eq_zero, inv_eq_zero, Int.natAbs_eq_zero, Ne, _root_.mul_eq_zero, or_self_iff]
    · apply lt_succ_of_le; apply natAbs_valMinAbs_le
    · rw [natCast_natAbs_valMinAbs]
      split_ifs
      · rw [mul_div_cancel₀ _ hap, valMinAbs_def_pos, val_cast_of_lt (hep hb),
          if_pos (le_of_lt_succ (mem_Ico.1 hb).2), Int.natAbs_natCast]
      · rw [mul_neg, mul_div_cancel₀ _ hap, natAbs_valMinAbs_neg, valMinAbs_def_pos,
          val_cast_of_lt (hep hb), if_pos (le_of_lt_succ (mem_Ico.1 hb).2), Int.natAbs_natCast]
-- 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
⊢ HPow.hPow (α := ZMod p) (↑a : ZMod p) (p / 2) * (↑(p / 2)! : ZMod p) =
    (↑(∏ x ∈ Ico 1 (p / 2).succ, a * (↑x : ℤ)) : ZMod p)
have rw : HPow.hPow (α := ZMod p) (↑a : ZMod p) (p / 2) * (↑(p / 2)! : ZMod p) = (↑(a ^ (p / 2) * (↑(p / 2)! : ℤ)) : ZMod p)
Tactic: rw [prod_mul_distrib, ← prod_natCast, prod_Ico_id_eq_factorial, prod_const, card_Ico,
        Nat.add_one_sub_one]
-- 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
x : ℕ
h : x ∈ Ico 1 (p / 2).succ
⊢ (↑(HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val : ZMod p) =
    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)
have simp : (↑(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: simp only [natCast_natAbs_valMinAbs]
-- 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
x : ℕ
h : x ∈ Ico 1 (p / 2).succ
⊢ (↑(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)
have 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)
Tactic: split_ifs
-- 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
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)
⊢ (↑(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)
have 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)
Tactic: split_ifs
-- 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
⊢ ∏ 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)
have 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)
Tactic: rw [prod_mul_distrib, Finset.prod_ite]
-- 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
⊢ 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}) *
    (↑(∏ 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)
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)
⊢ 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 (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)
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]