awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
a b c : ℕ
hb0 : 0 < b
hc : a / b ≤ c
x : ℕ
h rwa rwa₁ rwa₂ rwa₃ : x * b ≤ a
⊢ x ≤ a / b

Tactic:
rwa [le_div_iff_mul_le hb0]

Premises used: Nat.le_div_iff_mul_le
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
a b c : ℕ
hb0 : 0 < b
hc : a / b ≤ c
x : ℕ
⊢ 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
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
a b c : ℕ
hb0 : 0 < b
hc : a / b ≤ c
x : ℕ
this : x * b ≤ a → x ≤ c
simp : x * b ≤ a → 1 ≤ x → x ≤ c
⊢ x ∈ Ico 1 (a / b).succ ↔ x ∈ {x ∈ Ico 1 c.succ | x * b ≤ a}

Tactic:
simp [le_div_iff_mul_le hb0]

Premises used: Nat.le_div_iff_mul_le
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
a b c : ℕ
hb0 : 0 < b
hc : a / b ≤ c
x : ℕ
this : x * b ≤ a → x ≤ c
inl : x * b ≤ a → ∀ (this : ¬x * b ≤ a), 1 ≤ x → x ≤ c
inr inr₁ inr₂ : x * b ≤ a → ∀ (this : x ≤ c), 1 ≤ x → x ≤ c
⊢ x * b ≤ a → 1 ≤ x → x ≤ c

Tactic:
tauto
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p q : ℕ
hp0 : p = 0
⊢ ∑ a ∈ Ico 1 (p / 2).succ, a * q / p = #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q})

Tactic:
simp [hp0]
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p q : ℕ
hp0 : ¬p = 0
x : ℕ
hx : x ∈ Ico 1 (p / 2).succ
⊢ x ≤ p / 2

Tactic:
have := le_of_lt_succ (mem_Ico.mp hx).2
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p q : ℕ
hp0 : ¬p = 0
x : ℕ
hx : x ∈ Ico 1 (p / 2).succ
this : x ≤ p / 2
⊢ x * q / p ≤ p / 2 * q / p

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p q : ℕ
hp0 : ¬p = 0
⊢ ∑ a ∈ Ico 1 (p / 2).succ, #({x ∈ Ico 1 (q / 2).succ | x * p ≤ a * q}) =
    #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q})

Tactic:
simp only [card_eq_sum_ones, sum_filter, sum_product]

Premises used: Finset.card_eq_sum_ones, Finset.sum_filter, Finset.sum_product
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : Ne (α := ZMod p) (↑q : ZMod p) 0
x : ℕ × ℕ
fst snd : ℕ
⊢ (fst, snd) ∈ {x ∈ Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ | x.2 * q ≤ x.1 * p} ↔
    Membership.mem (α := ℕ × ℕ) ({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})
      ((Equiv.prodComm ℕ ℕ : (a : ℕ × ℕ) → ℕ × ℕ) (fst, snd) : ℕ × ℕ)

Tactic:
simp +contextual only [mem_filter, Prod.swap_prod_mk,
          mem_product, Equiv.prodComm_apply, and_assoc, and_left_comm]

Premises used: and_left_comm, Equiv.prodComm_apply, Prod.swap_prod_mk, and_assoc, Finset.mem_filter, Finset.mem_product
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : Ne (α := ZMod p) (↑q : ZMod p) 0
⊢ #({x ∈ Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ | x.2 * q ≤ x.1 * p}) =
    #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})

Tactic:
have hswap :
    #{x ∈ Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ | x.2 * q ≤ x.1 * p} =
      #{x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p} :=
    card_equiv (Equiv.prodComm _ _)
      (fun ⟨_, _⟩ => by
        simp +contextual only [mem_filter, Prod.swap_prod_mk,
          mem_product, Equiv.prodComm_apply, and_assoc, and_left_comm])
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : Ne (α := ZMod p) (↑q : ZMod p) 0
hswap :
  #({x ∈ Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ | x.2 * q ≤ x.1 * p}) =
    #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})
apply :
  ∀ (x : ℕ × ℕ) (hx : x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ) (hpq : x.2 * p ≤ x.1 * q) (hqp : x.1 * q ≤ x.2 * p),
    False
⊢ Disjoint ({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q})
    ({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})

Tactic:
apply disjoint_filter.2 fun x hx hpq hqp => ?_

Premises used: Iff.mpr, Finset.disjoint_filter
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : Ne (α := ZMod p) (↑q : ZMod p) 0
hswap :
  #({x ∈ Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ | x.2 * q ≤ x.1 * p}) =
    #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})
x : ℕ × ℕ
hx : x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ
hpq : x.2 * p ≤ x.1 * q
hqp : x.1 * q ≤ x.2 * p
⊢ x.1 ≤ p / 2

Tactic:
grind
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : Ne (α := ZMod p) (↑q : ZMod p) 0
hswap :
  #({x ∈ Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ | x.2 * q ≤ x.1 * p}) =
    #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})
x : ℕ × ℕ
hx : x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ
hpq : x.2 * p ≤ x.1 * q
hqp : x.1 * q ≤ x.2 * p
⊢ LT.lt (α := ℕ) 1 2

Tactic:
decide
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : Ne (α := ZMod p) (↑q : ZMod p) 0
hswap :
  #({x ∈ Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ | x.2 * q ≤ x.1 * p}) =
    #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})
x : ℕ × ℕ
hx : x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ
hpq : x.2 * p ≤ x.1 * q
hqp : x.1 * q ≤ x.2 * p
⊢ x.1 < p

Tactic:
have hxp : x.1 < p := lt_of_le_of_lt (b := p / 2)
      (by grind) (Nat.div_lt_self hp.1.pos (by decide))
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : Ne (α := ZMod p) (↑q : ZMod p) 0
hswap :
  #({x ∈ Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ | x.2 * q ≤ x.1 * p}) =
    #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})
x : ℕ × ℕ
hx : x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ
hpq : x.2 * p ≤ x.1 * q
hqp : x.1 * q ≤ x.2 * p
hxp : x.1 < p
⊢ Eq (α := ZMod p) (↑x.1 : ZMod p) 0

Tactic:
simpa [hq0] using congr_arg ((↑) : ℕ → ZMod p) (le_antisymm hpq hqp)

Premises used: Nat.cast, congr_arg, le_antisymm
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : Ne (α := ZMod p) (↑q : ZMod p) 0
hswap :
  #({x ∈ Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ | x.2 * q ≤ x.1 * p}) =
    #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})
x : ℕ × ℕ
hx : x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ
hpq : x.2 * p ≤ x.1 * q
hqp : x.1 * q ≤ x.2 * p
hxp : x.1 < p
⊢ Eq (α := ZMod p) (↑x.1 : ZMod p) 0

Tactic:
have : (x.1 : ZMod p) = 0 := by
      simpa [hq0] using congr_arg ((↑) : ℕ → ZMod p) (le_antisymm hpq hqp)
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : Ne (α := ZMod p) (↑q : ZMod p) 0
hswap :
  #({x ∈ Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ | x.2 * q ≤ x.1 * p}) =
    #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})
x : ℕ × ℕ
hx : x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ
hpq : x.2 * p ≤ x.1 * q
hqp : x.1 * q ≤ x.2 * p
hxp : x.1 < p
this : Eq (α := ZMod p) (↑x.1 : ZMod p) 0
⊢ val (n := p) (↑x.1 : ZMod p) = val (n := p) 0

Tactic:
apply_fun ZMod.val at this

Premises used: ZMod.val
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : Ne (α := ZMod p) (↑q : ZMod p) 0
hswap :
  #({x ∈ Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ | x.2 * q ≤ x.1 * p}) =
    #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})
x : ℕ × ℕ
hx : x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ
hpq : x.2 * p ≤ x.1 * q
hqp : x.1 * q ≤ x.2 * p
hxp : x.1 < p
this : val (n := p) (↑x.1 : ZMod p) = val (n := p) 0
⊢ x.1 = 0

Tactic:
rw [val_cast_of_lt hxp, val_zero] at this

Premises used: ZMod.val_cast_of_lt, ZMod.val_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : Ne (α := ZMod p) (↑q : ZMod p) 0
hswap :
  #({x ∈ Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ | x.2 * q ≤ x.1 * p}) =
    #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})
x : ℕ × ℕ
hx : x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ
hpq : x.2 * p ≤ x.1 * q
hqp : x.1 * q ≤ x.2 * p
hxp : x.1 < p
this : x.1 = 0
⊢ False

Tactic:
simp only [this, nonpos_iff_eq_zero, mem_Ico, one_ne_zero, false_and, mem_product] at hx

Premises used: false_and, one_ne_zero, Finset.mem_product, nonpos_iff_eq_zero, Finset.mem_Ico
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : Ne (α := ZMod p) (↑q : ZMod p) 0
hswap :
  #({x ∈ Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ | x.2 * q ≤ x.1 * p}) =
    #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})
⊢ Disjoint ({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q})
    ({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})

Tactic:
have hdisj :
    Disjoint {x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q}
      {x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p} := by
    apply disjoint_filter.2 fun x hx hpq hqp => ?_
    have hxp : x.1 < p := lt_of_le_of_lt (b := p / 2)
      (by grind) (Nat.div_lt_self hp.1.pos (by decide))
    have : (x.1 : ZMod p) = 0 := by
      simpa [hq0] using congr_arg ((↑) : ℕ → ZMod p) (le_antisymm hpq hqp)
    apply_fun ZMod.val at this
    rw [val_cast_of_lt hxp, val_zero] at this
    simp only [this, nonpos_iff_eq_zero, mem_Ico, one_ne_zero, false_and, mem_product] at hx
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : Ne (α := ZMod p) (↑q : ZMod p) 0
hswap :
  #({x ∈ Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ | x.2 * q ≤ x.1 * p}) =
    #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})
hdisj :
  Disjoint ({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q})
    ({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})
x : ℕ × ℕ
⊢ x.2 * p ≤ x.1 * q ∨ x.1 * q ≤ x.2 * p

Tactic:
have := le_total (x.2 * p) (x.1 * q)
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : Ne (α := ZMod p) (↑q : ZMod p) 0
hswap :
  #({x ∈ Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ | x.2 * q ≤ x.1 * p}) =
    #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})
hdisj :
  Disjoint ({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q})
    ({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})
x : ℕ × ℕ
this : x.2 * p ≤ x.1 * q ∨ x.1 * q ≤ x.2 * p
simp :
  ((1 ≤ x.1 ∧ x.1 < (p / 2).succ) ∧ 1 ≤ x.2 ∧ x.2 < (q / 2).succ) ∧ x.2 * p ≤ x.1 * q ∨
      ((1 ≤ x.1 ∧ x.1 < (p / 2).succ) ∧ 1 ≤ x.2 ∧ x.2 < (q / 2).succ) ∧ x.1 * q ≤ x.2 * p ↔
    (1 ≤ x.1 ∧ x.1 < (p / 2).succ) ∧ 1 ≤ x.2 ∧ x.2 < (q / 2).succ
⊢ x ∈
      {x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q} ∪
        {x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p} ↔
    x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ

Tactic:
simp only [mem_union, mem_filter, mem_Ico, mem_product]

Premises used: Finset.mem_filter, Finset.mem_union, Finset.mem_product, Finset.mem_Ico
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : Ne (α := ZMod p) (↑q : ZMod p) 0
hswap :
  #({x ∈ Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ | x.2 * q ≤ x.1 * p}) =
    #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})
hdisj :
  Disjoint ({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q})
    ({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})
⊢ {x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q} ∪
      {x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p} =
    Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ

Tactic:
have hunion :
      {x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q} ∪
        {x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p} =
      Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ :=
    Finset.ext fun x => by
      have := le_total (x.2 * p) (x.1 * q)
      simp only [mem_union, mem_filter, mem_Ico, mem_product]
      tauto
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : Ne (α := ZMod p) (↑q : ZMod p) 0
hswap :
  #({x ∈ Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ | x.2 * q ≤ x.1 * p}) =
    #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})
hdisj :
  Disjoint ({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q})
    ({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})
hunion :
  {x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q} ∪
      {x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p} =
    Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ
rw : #(Ico 1 (p / 2).succ) * #(Ico 1 (q / 2).succ) = p / 2 * (q / 2)
⊢ HAdd.hAdd (α := ℕ) (∑ a ∈ Ico 1 (p / 2).succ, a * q / p) (∑ a ∈ Ico 1 (q / 2).succ, a * p / q) = p / 2 * (q / 2)

Tactic:
rw [sum_Ico_eq_card_lt, sum_Ico_eq_card_lt, hswap, ← card_union_of_disjoint hdisj, hunion,
    card_product]

Premises used: _private.0.ZMod.sum_Ico_eq_card_lt, Finset.card_product, Finset.card_union_of_disjoint
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : Ne (α := ZMod p) (↑q : ZMod p) 0
hswap :
  #({x ∈ Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ | x.2 * q ≤ x.1 * p}) =
    #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})
hdisj :
  Disjoint ({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q})
    ({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})
hunion :
  {x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q} ∪
      {x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p} =
    Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ
⊢ #(Ico 1 (p / 2).succ) * #(Ico 1 (q / 2).succ) = p / 2 * (q / 2)

Tactic:
simp only [card_Ico, succ_sub_succ_eq_sub, Nat.sub_zero]

Premises used: Nat.card_Ico, Nat.sub_zero, Nat.succ_sub_succ_eq_sub
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℕ
ha1 : a % 2 = 1
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
⊢ Fact (p % 2 = 1)

Tactic:
haveI hp' : Fact (p % 2 = 1) := ⟨(Nat.Prime.mod_two_eq_one_iff_ne_two Fact.out).mpr hp⟩
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℕ
ha1 : a % 2 = 1
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
hp' : Fact (p % 2 = 1)
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : ¬Eq (α := ZMod p) (↑a : ZMod p) 0
⊢ Ne (α := ZMod p) (↑(↑a : ℤ) : ZMod p) 0

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℕ
ha1 : a % 2 = 1
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
hp' : Fact (p % 2 = 1)
⊢ Ne (α := ZMod p) (↑(↑a : ℤ) : ZMod p) 0

Tactic:
have ha0' : ((a : ℤ) : ZMod p) ≠ 0 := by norm_cast
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℕ
ha1 : a % 2 = 1
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
hp' : Fact (p % 2 = 1)
ha0' : Ne (α := ZMod p) (↑(↑a : ℤ) : ZMod p) 0
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : Eq (α := ZMod p) (↑a : ZMod p) (↑a : ZMod p)
⊢ Eq (α := ZMod p) (↑(↑a : ℤ) : ZMod p) (↑a : ZMod p)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℕ
ha1 : a % 2 = 1
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
hp' : Fact (p % 2 = 1)
ha0' : Ne (α := ZMod p) (↑(↑a : ℤ) : ZMod p) 0
rw : legendreSym p (↑a : ℤ) = HPow.hPow (α := ℤ) (-1) (HMod.hMod (α := ℕ) (∑ x ∈ Ico 1 (p / 2).succ, x * a / p) 2)
rw₁ :
  HPow.hPow (α := ℤ) (-1)
      #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑(↑a : ℤ) : ZMod p) (↑x : ZMod p)).val}) =
    HPow.hPow (α := ℤ) (-1) (HMod.hMod (α := ℕ) (∑ x ∈ Ico 1 (p / 2).succ, x * a / p) 2)
rw₂ :
  HPow.hPow (α := ℤ) (-1)
      (#({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑(↑a : ℤ) : ZMod p) (↑x : ZMod p)).val}) % 2) =
    HPow.hPow (α := ℤ) (-1) (HMod.hMod (α := ℕ) (∑ x ∈ Ico 1 (p / 2).succ, x * a / p) 2)
rw₃ :
  HPow.hPow (α := ℤ) (-1)
      (#({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val}) % 2) =
    HPow.hPow (α := ℤ) (-1) (HMod.hMod (α := ℕ) (∑ x ∈ Ico 1 (p / 2).succ, x * a / p) 2)
rw₄ rw₅ :
  HPow.hPow (α := ℤ) (-1) (HMod.hMod (α := ℕ) (∑ x ∈ Ico 1 (p / 2).succ, x * a / p) 2) =
    HPow.hPow (α := ℤ) (-1) (HMod.hMod (α := ℕ) (∑ x ∈ Ico 1 (p / 2).succ, x * a / p) 2)
⊢ legendreSym p (↑a : ℤ) = HPow.hPow (α := ℤ) (β := ℕ) (-1) (∑ x ∈ Ico 1 (p / 2).succ, x * a / p)

Tactic:
rw [neg_one_pow_eq_pow_mod_two, gauss_lemma hp ha0', neg_one_pow_eq_pow_mod_two,
    (by norm_cast : ((a : ℤ) : ZMod p) = (a : ZMod p)),
    show _ = _ from eisenstein_lemma_aux p ha1 ha0]

Premises used: neg_one_pow_eq_pow_mod_two, ZMod.gauss_lemma, ZMod.eisenstein_lemma_aux
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
⊢ J(a | 0) = 1

Tactic:
simp only [jacobiSym, primeFactorsList_zero, List.prod_nil, List.pmap]

Premises used: List.pmap, List.prod_nil, Nat.primeFactorsList_zero, jacobiSym
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
⊢ J(a | 1) = 1

Tactic:
simp only [jacobiSym, primeFactorsList_one, List.prod_nil, List.pmap]

Premises used: List.pmap, Nat.primeFactorsList_one, List.prod_nil, jacobiSym
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
p : ℕ
fp : Fact (Nat.Prime p)
a : ℤ
⊢ legendreSym p a = J(a | p)

Tactic:
simp only [jacobiSym, primeFactorsList_prime fp.1, List.prod_cons, List.prod_nil, mul_one,
    List.pmap]

Premises used: Nat.primeFactorsList_prime, List.pmap, List.prod_nil, mul_one, List.prod_cons, Fact.out, jacobiSym
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
rw :
  HMul.hMul (α := ℤ)
      (List.prod (List.pmap (P := Nat.Prime) (fun (p : ℕ) (pp : Nat.Prime p) ↦ legendreSym p a) b₁.primeFactorsList ⋯))
      (List.prod
        (List.pmap (P := Nat.Prime) (fun (p : ℕ) (pp : Nat.Prime p) ↦ legendreSym p a) b₂.primeFactorsList ⋯)) =
    J(a | b₁) * J(a | b₂)
rw₁ : ∀ a ∈ b₁.primeFactorsList ++ b₂.primeFactorsList, Nat.Prime a
⊢ J(a | b₁ * b₂) = J(a | b₁) * J(a | b₂)

Tactic:
rw [jacobiSym, ((perm_primeFactorsList_mul hb₁ hb₂).pmap _).prod_eq, List.pmap_append,
    List.prod_append]

Premises used: List.prod_append, List.Perm.prod_eq, List.pmap_append, List.Perm.pmap, Nat.perm_primeFactorsList_mul, jacobiSym
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ ∀ a ∈ b₁.primeFactorsList ++ b₂.primeFactorsList, Nat.Prime a

Tactic:
fun p hp =>
      (List.mem_append.mp hp).elim prime_of_mem_primeFactorsList prime_of_mem_primeFactorsList

Premises used: Nat.prime_of_mem_primeFactorsList, List.mem_append, Iff.mp, Or.elim
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ ∀ a ∈ b₁.primeFactorsList ++ b₂.primeFactorsList, Nat.Prime a

Tactic:
exact fun p hp =>
      (List.mem_append.mp hp).elim prime_of_mem_primeFactorsList prime_of_mem_primeFactorsList

Premises used: Nat.prime_of_mem_primeFactorsList, List.mem_append, Iff.mp, Or.elim
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ HMul.hMul (α := ℤ)
      (List.prod (List.pmap (P := Nat.Prime) (fun (p : ℕ) (pp : Nat.Prime p) ↦ legendreSym p a) b₁.primeFactorsList ⋯))
      (List.prod
        (List.pmap (P := Nat.Prime) (fun (p : ℕ) (pp : Nat.Prime p) ↦ legendreSym p a) b₂.primeFactorsList ⋯)) =
    J(a | b₁) * J(a | b₂)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b₁ b₂ : ℕ
inst : NeZero b₁
inst_1 : NeZero b₂
⊢ J(a | b₁ * b₂) = J(a | b₁) * J(a | b₂)

Tactic:
mul_right' a (NeZero.ne b₁) (NeZero.ne b₂)

Premises used: jacobiSym.mul_right', NeZero.ne
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
rw : {0, -1, 1} = (↑(MonoidHom.mrange (F := SignType →* ℤ) (↑SignType.castHom : SignType →* ℤ)) : Set ℤ)
⊢ {0, 1, -1} = (↑(MonoidHom.mrange (F := SignType →* ℤ) (↑SignType.castHom : SignType →* ℤ)) : Set ℤ)

Tactic:
rw [Set.pair_comm]

Premises used: Set.pair_comm
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
⊢ {0, -1, 1} = (↑(MonoidHom.mrange (F := SignType →* ℤ) (↑SignType.castHom : SignType →* ℤ)) : Set ℤ)

Tactic:
(SignType.range_eq SignType.castHom).symm

Premises used: SignType.cast, SignType.range_eq, setOf, SignType.castHom, Set.range, Eq.symm, DFunLike.coe, Int.neg, Int.negOfNat
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
⊢ {0, -1, 1} = (↑(MonoidHom.mrange (F := SignType →* ℤ) (↑SignType.castHom : SignType →* ℤ)) : Set ℤ)

Tactic:
exact (SignType.range_eq SignType.castHom).symm

Premises used: SignType.range_eq, SignType.castHom, Eq.symm, DFunLike.coe
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
x : ℤ
ha' :
  Membership.mem (γ := List ℤ)
    (List.pmap (P := Nat.Prime) (fun (p : ℕ) (pp : Nat.Prime p) ↦ legendreSym p a) b.primeFactorsList ⋯) x
rcases :
  ∀ (p : ℕ) (hp : p ∈ b.primeFactorsList)
    (ha' :
      Membership.mem (γ := List ℤ)
        (List.pmap (P := Nat.Prime) (fun (p : ℕ) (pp : Nat.Prime p) ↦ legendreSym p a) b.primeFactorsList ⋯)
        (legendreSym p a)),
    Membership.mem (γ := Submonoid ℤ)
      (Submonoid.copy (MonoidHom.mrange (F := SignType →* ℤ) (↑SignType.castHom : SignType →* ℤ)) {0, 1, -1} ⋯)
      (legendreSym p a)
⊢ Membership.mem (γ := Submonoid ℤ)
    (Submonoid.copy (MonoidHom.mrange (F := SignType →* ℤ) (↑SignType.castHom : SignType →* ℤ)) {0, 1, -1} ⋯) x

Tactic:
rcases List.mem_pmap.mp ha' with ⟨p, hp, rfl⟩

Premises used: List.mem_pmap, Iff.mp, rfl
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b p : ℕ
hp : p ∈ b.primeFactorsList
ha' :
  Membership.mem (γ := List ℤ)
    (List.pmap (P := Nat.Prime) (fun (p : ℕ) (pp : Nat.Prime p) ↦ legendreSym p a) b.primeFactorsList ⋯)
    (legendreSym p a)
⊢ Fact (Nat.Prime p)

Tactic:
haveI : Fact p.Prime := ⟨prime_of_mem_primeFactorsList hp⟩
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b p : ℕ
hp : p ∈ b.primeFactorsList
ha' :
  Membership.mem (γ := List ℤ)
    (List.pmap (P := Nat.Prime) (fun (p : ℕ) (pp : Nat.Prime p) ↦ legendreSym p a) b.primeFactorsList ⋯)
    (legendreSym p a)
this : Fact (Nat.Prime p)
⊢ Membership.mem (γ := Submonoid ℤ)
    (Submonoid.copy (MonoidHom.mrange (F := SignType →* ℤ) (↑SignType.castHom : SignType →* ℤ)) {0, 1, -1} ⋯)
    (legendreSym p a)

Tactic:
quadraticChar_isQuadratic (ZMod p) a

Premises used: Int.cast, Set.insert, quadraticChar_isQuadratic, Set.Mem, setOf, legendreSym, ZMod, Set.singleton
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b p : ℕ
hp : p ∈ b.primeFactorsList
ha' :
  Membership.mem (γ := List ℤ)
    (List.pmap (P := Nat.Prime) (fun (p : ℕ) (pp : Nat.Prime p) ↦ legendreSym p a) b.primeFactorsList ⋯)
    (legendreSym p a)
this : Fact (Nat.Prime p)
⊢ Membership.mem (γ := Submonoid ℤ)
    (Submonoid.copy (MonoidHom.mrange (F := SignType →* ℤ) (↑SignType.castHom : SignType →* ℤ)) {0, 1, -1} ⋯)
    (legendreSym p a)

Tactic:
exact quadraticChar_isQuadratic (ZMod p) a

Premises used: Int.cast, quadraticChar_isQuadratic, ZMod
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
b : ℕ
z : ℤ
hz :
  Membership.mem (γ := List ℤ)
    (List.pmap (P := Nat.Prime) (fun (p : ℕ) (pp : Nat.Prime p) ↦ legendreSym p 1) b.primeFactorsList ⋯) z
let : ∀ (p : ℕ) (hp : p ∈ b.primeFactorsList) (he : legendreSym p 1 = z), z = 1
⊢ z = 1

Tactic:
let ⟨p, hp, he⟩ := List.mem_pmap.1 hz