awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℤ
rw : legendreSym p (-1 * a) = HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑p : ZMod 4) : ℤ) (legendreSym p a)
rw₁ :
  legendreSym p (-1) * legendreSym p a =
    HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑p : ZMod 4) : ℤ) (legendreSym p a)
rw₂ rw₃ :
  HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑p : ZMod 4) : ℤ) (legendreSym p a) =
    HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑p : ZMod 4) : ℤ) (legendreSym p a)
⊢ legendreSym p (-a) = HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑p : ZMod 4) : ℤ) (legendreSym p a)

Tactic:
rw [neg_eq_neg_one_mul, legendreSym.mul p (-1) a, legendreSym.at_neg_one hp]

Premises used: neg_eq_neg_one_mul, legendreSym.at_neg_one, legendreSym.mul, OfNat.ofNat, Neg.neg
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
rw : Fintype.card (ZMod p) % 4 ≠ 3 ↔ p % 4 ≠ 3
rw₁ rw₂ : p % 4 ≠ 3 ↔ p % 4 ≠ 3
⊢ IsSquare (α := ZMod p) (-1) ↔ p % 4 ≠ 3

Tactic:
rw [FiniteField.isSquare_neg_one_iff, card p]

Premises used: FiniteField.isSquare_neg_one_iff, ZMod.card
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
y : ZMod p
hy : HPow.hPow (β := ℕ) y 2 = -1
⊢ p % 4 ≠ 3

Tactic:
exists_sq_eq_neg_one_iff.1 ⟨y, hy ▸ pow_two y⟩

Premises used: ZMod.exists_sq_eq_neg_one_iff, Exists.intro, Iff.mp
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ZMod p
hy : y ≠ 0
hxy : HPow.hPow (β := ℕ) x 2 = -HPow.hPow (β := ℕ) y 2
⊢ HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) y 2 = -HPow.hPow (β := ℕ) y 2 / HPow.hPow (β := ℕ) y 2

Tactic:
apply_fun fun z => z / y ^ 2 at hxy

Premises used: HDiv.hDiv, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ZMod p
hy : y ≠ 0
hxy : HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) y 2 = -HPow.hPow (β := ℕ) y 2 / HPow.hPow (β := ℕ) y 2
rwa :
  ∀ (hxy : HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) y 2 = -(HPow.hPow (β := ℕ) y 2 / HPow.hPow (β := ℕ) y 2)),
    HPow.hPow (β := ℕ) (x / y) 2 = -1
rwa₁ :
  ∀ (hxy : HPow.hPow (β := ℕ) (x / y) 2 = -(HPow.hPow (β := ℕ) y 2 / HPow.hPow (β := ℕ) y 2)),
    HPow.hPow (β := ℕ) (x / y) 2 = -1
rwa₂ : ∀ (hxy : HPow.hPow (β := ℕ) (x / y) 2 = -HPow.hPow (β := ℕ) (y / y) 2), HPow.hPow (β := ℕ) (x / y) 2 = -1
rwa₃ : ∀ (hxy : HPow.hPow (β := ℕ) (x / y) 2 = -HPow.hPow (α := ZMod p) (β := ℕ) 1 2), HPow.hPow (β := ℕ) (x / y) 2 = -1
rwa₄ rwa₅ rwa₆ rwa₇ : ∀ (hxy : HPow.hPow (β := ℕ) (x / y) 2 = -1), HPow.hPow (β := ℕ) (x / y) 2 = -1
⊢ HPow.hPow (β := ℕ) (x / y) 2 = -1

Tactic:
rwa [neg_div, ← div_pow, ← div_pow, div_self hy, one_pow] at hxy

Premises used: one_pow, neg_div, div_pow, div_self
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ZMod p
hx : x ≠ 0
hxy : HPow.hPow (β := ℕ) x 2 = -HPow.hPow (β := ℕ) y 2
⊢ p % 4 ≠ 3

Tactic:
mod_four_ne_three_of_sq_eq_neg_sq' hx (neg_eq_iff_eq_neg.mpr hxy).symm

Premises used: Iff.mpr, neg_eq_iff_eq_neg, Eq.symm, ZMod.mod_four_ne_three_of_sq_eq_neg_sq'
-- Module: Mathlib.NumberTheory.LegendreSymbol.Complex
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
⊢ ringChar ℂ ≠ ringChar F

Tactic:
simpa only [ringChar.eq_zero] using (CharP.ringChar_ne_zero_of_finite F).symm

Premises used: Ne.symm, CharP.ringChar_ne_zero_of_finite, ringChar.eq_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.Complex
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
⊢ ringChar ℂ ≠ ringChar F

Tactic:
ringChar_ne F

Premises used: _private.0.AddChar.ringChar_ne
-- Module: Mathlib.NumberTheory.LegendreSymbol.Complex
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
⊢ ringChar ℂ ≠ ringChar F

Tactic:
exact ringChar_ne F

Premises used: _private.0.AddChar.ringChar_ne
-- Module: Mathlib.NumberTheory.LegendreSymbol.Complex
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
ch : PrimitiveAddChar F ℂ := primitiveChar F ℂ ⋯
refine : CyclotomicField (↑ch.n : ℕ) ℂ →* ℂ
⊢ AddChar F ℂ

Tactic:
refine MonoidHom.compAddChar ?_ ch.char

Premises used: AddChar.PrimitiveAddChar.char, MonoidHom.compAddChar
-- Module: Mathlib.NumberTheory.LegendreSymbol.Complex
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
ch : PrimitiveAddChar F ℂ := primitiveChar F ℂ ⋯
⊢ CyclotomicField (↑ch.n : ℕ) ℂ →* ℂ

Tactic:
exact (IsCyclotomicExtension.algEquiv {(ch.n : ℕ)} ℂ (CyclotomicField ch.n ℂ) ℂ).toMonoidHom

Premises used: PNat.val, IsCyclotomicExtension.algEquiv, AddChar.PrimitiveAddChar.n, AlgEquiv.toMulEquiv, MulEquiv.toMonoidHom, CyclotomicField, Complex, Singleton.singleton
-- Module: Mathlib.NumberTheory.LegendreSymbol.Complex
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
⊢ IsPrimitive (primitiveChar_to_Complex F)

Tactic:
IsPrimitive.compMulHom_of_isPrimitive (PrimitiveAddChar.prim _) ?_

Premises used: AddChar.FiniteField.primitiveChar_to_Complex, AddChar.PrimitiveAddChar.prim, AddChar.IsPrimitive.compMulHom_of_isPrimitive
-- Module: Mathlib.NumberTheory.LegendreSymbol.Complex
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
refine :
  Function.Injective (α := CyclotomicField (↑(PrimitiveAddChar.n (primitiveChar F ℂ ⋯)) : ℕ) ℂ) (β := ℂ)
    (⇑(MulEquiv.toMonoidHom
          (AlgEquiv.toMulEquiv
            (IsCyclotomicExtension.algEquiv {(↑(PrimitiveAddChar.n (primitiveChar F ℂ ⋯)) : ℕ)} ℂ
              (CyclotomicField (↑(PrimitiveAddChar.n (primitiveChar F ℂ ⋯)) : ℕ) ℂ) ℂ))) :
      (a : CyclotomicField (↑(primitiveChar F ℂ ⋯).n : ℕ) ℂ) → ℂ)
⊢ IsPrimitive (primitiveChar_to_Complex F)

Tactic:
refine IsPrimitive.compMulHom_of_isPrimitive (PrimitiveAddChar.prim _) ?_

Premises used: AddChar.PrimitiveAddChar.prim, AddChar.IsPrimitive.compMulHom_of_isPrimitive
-- Module: Mathlib.NumberTheory.LegendreSymbol.Complex
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
nn : ℕ+ := PrimitiveAddChar.n (primitiveChar F ℂ ⋯)
⊢ Function.Injective (α := CyclotomicField (↑(PrimitiveAddChar.n (primitiveChar F ℂ ⋯)) : ℕ) ℂ) (β := ℂ)
    (⇑(MulEquiv.toMonoidHom
          (AlgEquiv.toMulEquiv
            (IsCyclotomicExtension.algEquiv {(↑(PrimitiveAddChar.n (primitiveChar F ℂ ⋯)) : ℕ)} ℂ
              (CyclotomicField (↑(PrimitiveAddChar.n (primitiveChar F ℂ ⋯)) : ℕ) ℂ) ℂ))) :
      (a : CyclotomicField (↑(primitiveChar F ℂ ⋯).n : ℕ) ℂ) → ℂ)

Tactic:
(IsCyclotomicExtension.algEquiv {(nn : ℕ)} ℂ (CyclotomicField nn ℂ) ℂ).injective

Premises used: PNat.val, IsCyclotomicExtension.algEquiv, Set.Mem, setOf, CyclotomicField, AlgEquiv.injective, Complex, Singleton.singleton
-- Module: Mathlib.NumberTheory.LegendreSymbol.Complex
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
nn : ℕ+ := PrimitiveAddChar.n (primitiveChar F ℂ ⋯)
⊢ Function.Injective (α := CyclotomicField (↑(PrimitiveAddChar.n (primitiveChar F ℂ ⋯)) : ℕ) ℂ) (β := ℂ)
    (⇑(MulEquiv.toMonoidHom
          (AlgEquiv.toMulEquiv
            (IsCyclotomicExtension.algEquiv {(↑(PrimitiveAddChar.n (primitiveChar F ℂ ⋯)) : ℕ)} ℂ
              (CyclotomicField (↑(PrimitiveAddChar.n (primitiveChar F ℂ ⋯)) : ℕ) ℂ) ℂ))) :
      (a : CyclotomicField (↑(primitiveChar F ℂ ⋯).n : ℕ) ℂ) → ℂ)

Tactic:
exact (IsCyclotomicExtension.algEquiv {(nn : ℕ)} ℂ (CyclotomicField nn ℂ) ℂ).injective

Premises used: PNat.val, IsCyclotomicExtension.algEquiv, CyclotomicField, AlgEquiv.injective, Complex, Singleton.singleton
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
⊢ ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2

Tactic:
grind
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
⊢ ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2

Tactic:
have he : ∀ {x}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2 := by grind
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
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
x : ℕ
hx : x ∈ Ico 1 (p / 2).succ
⊢ LT.lt (α := ℕ) 1 2

Tactic:
decide
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
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
⊢ ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p

Tactic:
have hep : ∀ {x}, x ∈ Ico 1 (p / 2).succ → x < p := fun hx =>
    lt_of_le_of_lt (he hx).2 (Nat.div_lt_self hp.1.pos (by decide))
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
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
⊢ ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x

Tactic:
have hpe : ∀ {x}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x := fun hx hpx =>
    not_lt_of_ge (le_of_dvd (Nat.pos_of_ne_zero (he hx).1) hpx) (hep hx)
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
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
x : ℕ
hx : x ∈ Ico 1 (p / 2).succ
⊢ (a * (↑x : ZMod p)).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ

Tactic:
simp [hap, CharP.cast_eq_zero_iff (ZMod p) p, hpe hx, one_le_iff_ne_zero, natAbs_valMinAbs_le _]

Premises used: ZMod, ZMod.natAbs_valMinAbs_le, Nat.one_le_iff_ne_zero, CharP.cast_eq_zero_iff
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
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
⊢ ∀ x ∈ Ico 1 (p / 2).succ, (a * (↑x : ZMod p)).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ

Tactic:
have hmem : ∀ (x : ℕ) (_ : x ∈ Ico 1 (p / 2).succ),
      (a * x : ZMod p).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ := by
    intro x hx
    simp [hap, CharP.cast_eq_zero_iff (ZMod p) p, hpe hx, one_le_iff_ne_zero, natAbs_valMinAbs_le _]
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
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
⊢ ∃ (x : ℕ) (_ : x ∈ Ico 1 (p / 2).succ), (a * (↑x : ZMod p)).valMinAbs.natAbs = b

Tactic:
⟨(b / a : ZMod p).valMinAbs.natAbs, mem_Ico.mpr ⟨?_, ?_⟩, ?_⟩

Premises used: Iff.mpr, ZMod.valMinAbs, HDiv.hDiv, Nat.cast, And.intro, Int.natAbs, Exists.intro, Finset.mem_Ico
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
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
refine_1 : 1 ≤ ((↑b : ZMod p) / a).valMinAbs.natAbs
refine_2 : ((↑b : ZMod p) / a).valMinAbs.natAbs < (p / 2).succ
refine_3 : (a * (↑((↑b : ZMod p) / a).valMinAbs.natAbs : ZMod p)).valMinAbs.natAbs = b
⊢ ∃ (x : ℕ) (_ : x ∈ Ico 1 (p / 2).succ), (a * (↑x : ZMod p)).valMinAbs.natAbs = b

Tactic:
refine ⟨(b / a : ZMod p).valMinAbs.natAbs, mem_Ico.mpr ⟨?_, ?_⟩, ?_⟩
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
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
refine_1 : ((↑b : ZMod p) / a).valMinAbs.natAbs ≠ 0
⊢ 1 ≤ ((↑b : ZMod p) / a).valMinAbs.natAbs

Tactic:
apply Nat.pos_of_ne_zero

Premises used: Nat.pos_of_ne_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
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 ≠ 0

Tactic:
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]

Premises used: inv_eq_zero, or_self_iff, Ne, ZMod.valMinAbs_eq_zero, mul_eq_zero, div_eq_mul_inv, ZMod, Int.natAbs_eq_zero, CharP.cast_eq_zero_iff, not_false_iff
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
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
refine_2 : ((↑b : ZMod p) / a).valMinAbs.natAbs ≤ p / 2
⊢ ((↑b : ZMod p) / a).valMinAbs.natAbs < (p / 2).succ

Tactic:
apply lt_succ_of_le

Premises used: Nat.lt_succ_of_le
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
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

Tactic:
apply natAbs_valMinAbs_le

Premises used: ZMod.natAbs_valMinAbs_le
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
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
refine_3 :
  (a * if ((↑b : ZMod p) / a).val ≤ p / 2 then (↑b : ZMod p) / a else -((↑b : ZMod p) / a)).valMinAbs.natAbs = b
⊢ (a * (↑((↑b : ZMod p) / a).valMinAbs.natAbs : ZMod p)).valMinAbs.natAbs = b

Tactic:
rw [natCast_natAbs_valMinAbs]

Premises used: ZMod.natCast_natAbs_valMinAbs
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
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
neg : ¬((↑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

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
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
pos₄ pos₅ : b = b
⊢ (a * ((↑b : ZMod p) / a)).valMinAbs.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]

Premises used: ZMod.valMinAbs_def_pos, ZMod.val_cast_of_lt, if_pos, mul_div_cancel₀, And.right, Nat.le_of_lt_succ, Iff.mp, Int.natAbs_natCast, Finset.mem_Ico
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
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
neg₆ neg₇ : b = b
⊢ (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]

Premises used: ZMod.valMinAbs_def_pos, ZMod.val_cast_of_lt, ZMod.natAbs_valMinAbs_neg, if_pos, mul_div_cancel₀, And.right, Nat.le_of_lt_succ, Iff.mp, Int.natAbs_natCast, mul_neg, Finset.mem_Ico
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
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),
    ∃ (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]
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
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
hsurj :
  ∀ (b : ℕ) (hb : b ∈ Ico 1 (p / 2).succ),
    ∃ (x : ℕ) (_ : x ∈ Ico 1 (p / 2).succ), (a * (↑x : ZMod p)).valMinAbs.natAbs = b
⊢ 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)

Tactic:
Multiset.map_eq_map_of_bij_of_nodup _ _ (Finset.nodup _) (Finset.nodup _)
    (fun x _ => (a * x : ZMod p).valMinAbs.natAbs) hmem
    (inj_on_of_surj_on_of_card_le _ hmem hsurj le_rfl) hsurj (fun _ _ => rfl)

Premises used: le_rfl, HMul.hMul, ZMod.valMinAbs, Finset.inj_on_of_surj_on_of_card_le, Finset.nodup, Nat.cast, Multiset.map_eq_map_of_bij_of_nodup, Int.natAbs, rfl
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
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
hsurj :
  ∀ (b : ℕ) (hb : b ∈ Ico 1 (p / 2).succ),
    ∃ (x : ℕ) (_ : x ∈ Ico 1 (p / 2).succ), (a * (↑x : ZMod p)).valMinAbs.natAbs = b
⊢ 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)

Tactic:
exact Multiset.map_eq_map_of_bij_of_nodup _ _ (Finset.nodup _) (Finset.nodup _)
    (fun x _ => (a * x : ZMod p).valMinAbs.natAbs) hmem
    (inj_on_of_surj_on_of_card_le _ hmem hsurj le_rfl) hsurj (fun _ _ => rfl)
-- 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) (↑a : ZMod p) (p / 2) * (↑(p / 2)! : ZMod p) = (↑(a ^ (p / 2) * (↑(p / 2)! : ℤ)) : ZMod p)
⊢ HPow.hPow (α := ZMod p) (↑a : ZMod p) (p / 2) * (↑(p / 2)! : ZMod p) =
    (↑(∏ x ∈ Ico 1 (p / 2).succ, a * (↑x : ℤ)) : ZMod p)

Tactic:
rw [prod_mul_distrib, ← prod_natCast, prod_Ico_id_eq_factorial, prod_const, card_Ico,
        Nat.add_one_sub_one]

Premises used: Nat.add_one_sub_one, Finset.prod_mul_distrib, Finset.prod_const, Finset.prod_Ico_id_eq_factorial, Nat.card_Ico, Finset.prod_natCast
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
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) = (↑(a ^ (p / 2) * (↑(p / 2)! : ℤ)) : 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
⊢ Eq (α := ZMod p) (↑(∏ x ∈ Ico 1 (p / 2).succ, a * (↑x : ℤ)) : ZMod p)
    (∏ x ∈ Ico 1 (p / 2).succ, (↑(HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val : 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
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)
⊢ (↑(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)

Tactic:
simp only [natCast_natAbs_valMinAbs]

Premises used: ZMod.natCast_natAbs_valMinAbs