awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Tactic.NormNum.IsSquare (goal)
Goal:
a : ℚ
n d : ℕ
hn : ¬IsSquare n
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ ¬IsSquare a
have rw : ¬(IsSquare (α := ℤ) (↑n : ℤ) ∧ IsSquare (HDiv.hDiv (α := ℚ) (↑(↑n : ℤ) : ℚ) (↑(↑d : ℤ) : ℚ)).den)
Tactic: rw [ha.to_eq rfl rfl, Rat.isSquare_iff, ← Int.cast_natCast n, ← Int.cast_natCast d,
    Rat.num_div_eq_of_coprime]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.IsSquare (goal)
Goal:
a : ℚ
n d : ℕ
hn : ¬IsSquare n
hnd : n.Coprime d
ha : IsNNRat a n d
rw : ¬(IsSquare (α := ℤ) (↑n : ℤ) ∧ IsSquare (HDiv.hDiv (α := ℚ) (↑(↑n : ℤ) : ℚ) (↑(↑d : ℤ) : ℚ)).den)
⊢ ¬IsSquare a
have hb0 : LT.lt (α := ℤ) 0 (↑d : ℤ)
Tactic: rw [ha.to_eq rfl rfl, Rat.isSquare_iff, ← Int.cast_natCast n, ← Int.cast_natCast d,
    Rat.num_div_eq_of_coprime]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.IsSquare (goal)
Goal:
a : ℚ
n d : ℕ
hn : ¬IsSquare n
hnd : n.Coprime d
ha : IsNNRat a n d
rw : ¬(IsSquare (α := ℤ) (↑n : ℤ) ∧ IsSquare (HDiv.hDiv (α := ℚ) (↑(↑n : ℤ) : ℚ) (↑(↑d : ℤ) : ℚ)).den)
hb0 : LT.lt (α := ℤ) 0 (↑d : ℤ)
⊢ ¬IsSquare a
have h : (Int.natAbs (↑n : ℤ)).Coprime (Int.natAbs (↑d : ℤ))
Tactic: rw [ha.to_eq rfl rfl, Rat.isSquare_iff, ← Int.cast_natCast n, ← Int.cast_natCast d,
    Rat.num_div_eq_of_coprime]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.IsSquare (goal)
Goal:
a : ℚ
n d : ℕ
hn : ¬IsSquare n
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ LT.lt (α := ℤ) 0 (↑d : ℤ)
have hb0 : ∀ (hnd : LE.le (α := ℤ) (↑d : ℤ) 0), n.gcd d ≠ 1
Tactic: contrapose! hnd
Cleared hypotheses: hnd
-- Lean 4 proof step from Mathlib.Tactic.NormNum.IsSquare (hypothesis)
Goal:
a : ℚ
n d : ℕ
hn : ¬IsSquare n
ha : IsNNRat a n d
hnd : LE.le (α := ℤ) (↑d : ℤ) 0
⊢ n.gcd d ≠ 1
have this : n ≠ 1
Tactic: have : n ≠ 1 := by rintro rfl; simp at hn
-- Lean 4 proof step from Mathlib.Tactic.NormNum.IsSquare (goal)
Goal:
a : ℚ
n d : ℕ
hd : ¬IsSquare d
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ ¬IsSquare a
have rw : ¬(IsSquare (HDiv.hDiv (α := ℚ) (↑(↑n : ℤ) : ℚ) (↑(↑d : ℤ) : ℚ)).num ∧ IsSquare (α := ℤ) (↑d : ℤ))
Tactic: rw [ha.to_eq rfl rfl, Rat.isSquare_iff, ← Int.cast_natCast n, ← Int.cast_natCast d,
    ← Int.isSquare_natCast_iff (n := Rat.den _), Rat.den_div_eq_of_coprime]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.IsSquare (goal)
Goal:
a : ℚ
n d : ℕ
hd : ¬IsSquare d
hnd : n.Coprime d
ha : IsNNRat a n d
rw : ¬(IsSquare (HDiv.hDiv (α := ℚ) (↑(↑n : ℤ) : ℚ) (↑(↑d : ℤ) : ℚ)).num ∧ IsSquare (α := ℤ) (↑d : ℤ))
⊢ ¬IsSquare a
have hb0 : LT.lt (α := ℤ) 0 (↑d : ℤ)
Tactic: rw [ha.to_eq rfl rfl, Rat.isSquare_iff, ← Int.cast_natCast n, ← Int.cast_natCast d,
    ← Int.isSquare_natCast_iff (n := Rat.den _), Rat.den_div_eq_of_coprime]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.IsSquare (goal)
Goal:
a : ℚ
n d : ℕ
hd : ¬IsSquare d
hnd : n.Coprime d
ha : IsNNRat a n d
rw : ¬(IsSquare (HDiv.hDiv (α := ℚ) (↑(↑n : ℤ) : ℚ) (↑(↑d : ℤ) : ℚ)).num ∧ IsSquare (α := ℤ) (↑d : ℤ))
hb0 : LT.lt (α := ℤ) 0 (↑d : ℤ)
⊢ ¬IsSquare a
have h : (Int.natAbs (↑n : ℤ)).Coprime (Int.natAbs (↑d : ℤ))
Tactic: rw [ha.to_eq rfl rfl, Rat.isSquare_iff, ← Int.cast_natCast n, ← Int.cast_natCast d,
    ← Int.isSquare_natCast_iff (n := Rat.den _), Rat.den_div_eq_of_coprime]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.IsSquare (goal)
Goal:
a : ℚ
n d : ℕ
hd : ¬IsSquare d
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ LT.lt (α := ℤ) 0 (↑d : ℤ)
have hb0 : ∀ (hnd : LE.le (α := ℤ) (↑d : ℤ) 0), n.gcd d ≠ 1
Tactic: contrapose! hnd
Cleared hypotheses: hnd
-- Lean 4 proof step from Mathlib.Tactic.NormNum.IsSquare (goal)
Goal:
a : ℚ
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
ha : IsRat a (Int.negOfNat n) d
⊢ ¬IsSquare a
have rw : ¬IsSquare (-HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ))
Tactic: rw [ha.neg_to_eq rfl rfl]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.IsSquare (goal)
Goal:
a : ℚ
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
ha : IsRat a (Int.negOfNat n) d
q : ℚ
hq : -HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) = q * q
⊢ False
have refine : -HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) < q * q
Tactic: refine absurd hq (ne_of_lt ?_)
-- Lean 4 proof step from Mathlib.Tactic.NormNum.IsSquare (goal)
Goal:
a : ℚ
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
ha : IsRat a (Int.negOfNat n) d
q : ℚ
hq : -HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) = q * q
⊢ -HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) < 0
have rw : 0 < HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)
Tactic: rw [Left.neg_neg_iff]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.IsSquare (goal)
Goal:
a : ℚ
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
ha : IsRat a (Int.negOfNat n) d
q : ℚ
hq : -HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) = q * q
⊢ 0 < HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)
have ha₁ : LT.lt (α := ℚ) 0 (↑n : ℚ)
Tactic: apply div_pos
-- Lean 4 proof step from Mathlib.Tactic.NormNum.IsSquare (goal)
Goal:
a : ℚ
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
ha : IsRat a (Int.negOfNat n) d
q : ℚ
hq : -HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) = q * q
ha₁ : LT.lt (α := ℚ) 0 (↑n : ℚ)
⊢ 0 < HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)
have hb : LT.lt (α := ℚ) 0 (↑d : ℚ)
Tactic: apply div_pos
-- Lean 4 proof step from Mathlib.Tactic.NormNum.IsSquare (goal)
Goal:
a : ℚ
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
ha : IsRat a (Int.negOfNat n) d
q : ℚ
hq : -HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) = q * q
⊢ -HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) < q * q
have d₁ : -HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) < 0
Tactic: calc
    -(n / d : ℚ) < 0 := by rw [Left.neg_neg_iff]; apply div_pos <;> simpa [Nat.pos_iff_ne_zero]
    _ ≤ q * q := mul_self_nonneg _
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a : ℕ
⊢ jacobiSymNat a 0 = 1
have rw : jacobiSym (↑a : ℤ) 0 = 1
Tactic: rw [jacobiSymNat, jacobiSym.zero_right]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a : ℕ
rw : jacobiSym (↑a : ℤ) 0 = 1
⊢ jacobiSymNat a 0 = 1
have rw₁ : Eq (α := ℤ) 1 1
Tactic: rw [jacobiSymNat, jacobiSym.zero_right]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a : ℕ
⊢ jacobiSymNat a 1 = 1
have rw : jacobiSym (↑a : ℤ) 1 = 1
Tactic: rw [jacobiSymNat, jacobiSym.one_right]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a : ℕ
rw : jacobiSym (↑a : ℤ) 1 = 1
⊢ jacobiSymNat a 1 = 1
have rw₁ : Eq (α := ℤ) 1 1
Tactic: rw [jacobiSymNat, jacobiSym.one_right]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
b : ℕ
hb : (b / 2).beq 0 = false
⊢ jacobiSymNat 0 b = 0
have rw : 1 < b
Tactic: rw [jacobiSymNat, Nat.cast_zero, jacobiSym.zero_left ?_]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
b : ℕ
hb : (b / 2).beq 0 = false
⊢ 1 < b
have by : 1 < HMul.hMul (α := ℕ) 2 1
Tactic: calc
    1 < 2 * 1       := by decide
    _ ≤ 2 * (b / 2) :=
      Nat.mul_le_mul_left _ (Nat.succ_le_of_lt (Nat.pos_of_ne_zero (Nat.ne_of_beq_eq_false hb)))
    _ ≤ b           := Nat.mul_div_le b 2
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
b : ℕ
⊢ jacobiSymNat 1 b = 1
have rw : jacobiSym (↑1 : ℤ) b = 1
Tactic: rw [jacobiSymNat, Nat.cast_one, jacobiSym.one_left]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
b : ℕ
rw : jacobiSym (↑1 : ℤ) b = 1
⊢ jacobiSymNat 1 b = 1
have rw₁ : jacobiSym 1 b = 1
Tactic: rw [jacobiSymNat, Nat.cast_one, jacobiSym.one_left]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
b : ℕ
rw : jacobiSym (↑1 : ℤ) b = 1
rw₁ : jacobiSym 1 b = 1
⊢ jacobiSymNat 1 b = 1
have rw₂ : Eq (α := ℤ) 1 1
Tactic: rw [jacobiSymNat, Nat.cast_one, jacobiSym.one_left]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a : ℤ
b ab' : ℕ
ab r b' : ℤ
hb' : (↑b : ℤ) = b'
hab : a % b' = ab
h : (↑ab' : ℤ) = ab
hr : jacobiSymNat ab' b = r
⊢ jacobiSym a b = r
have rw : jacobiSym a b = jacobiSymNat ab' b
Tactic: rw [← hr, jacobiSymNat, jacobiSym.mod_left, hb', hab, ← h]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a : ℤ
b ab' : ℕ
ab r b' : ℤ
hb' : (↑b : ℤ) = b'
hab : a % b' = ab
h : (↑ab' : ℤ) = ab
hr : jacobiSymNat ab' b = r
rw : jacobiSym a b = jacobiSymNat ab' b
⊢ jacobiSym a b = r
have rw₁ : jacobiSym a b = jacobiSym (↑ab' : ℤ) b
Tactic: rw [← hr, jacobiSymNat, jacobiSym.mod_left, hb', hab, ← h]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a : ℤ
b ab' : ℕ
ab r b' : ℤ
hb' : (↑b : ℤ) = b'
hab : a % b' = ab
h : (↑ab' : ℤ) = ab
hr : jacobiSymNat ab' b = r
rw : jacobiSym a b = jacobiSymNat ab' b
rw₁ : jacobiSym a b = jacobiSym (↑ab' : ℤ) b
⊢ jacobiSym a b = r
have rw₂ : jacobiSym (a % (↑b : ℤ)) b = jacobiSym (↑ab' : ℤ) b
Tactic: rw [← hr, jacobiSymNat, jacobiSym.mod_left, hb', hab, ← h]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a : ℤ
b ab' : ℕ
ab r b' : ℤ
hb' : (↑b : ℤ) = b'
hab : a % b' = ab
h : (↑ab' : ℤ) = ab
hr : jacobiSymNat ab' b = r
rw : jacobiSym a b = jacobiSymNat ab' b
rw₁ : jacobiSym a b = jacobiSym (↑ab' : ℤ) b
rw₂ : jacobiSym (a % (↑b : ℤ)) b = jacobiSym (↑ab' : ℤ) b
⊢ jacobiSym a b = r
have rw₃ : jacobiSym (a % b') b = jacobiSym (↑ab' : ℤ) b
Tactic: rw [← hr, jacobiSymNat, jacobiSym.mod_left, hb', hab, ← h]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a : ℤ
b ab' : ℕ
ab r b' : ℤ
hb' : (↑b : ℤ) = b'
hab : a % b' = ab
h : (↑ab' : ℤ) = ab
hr : jacobiSymNat ab' b = r
rw : jacobiSym a b = jacobiSymNat ab' b
rw₁ : jacobiSym a b = jacobiSym (↑ab' : ℤ) b
rw₂ : jacobiSym (a % (↑b : ℤ)) b = jacobiSym (↑ab' : ℤ) b
rw₃ : jacobiSym (a % b') b = jacobiSym (↑ab' : ℤ) b
⊢ jacobiSym a b = r
have rw₄ : jacobiSym ab b = jacobiSym (↑ab' : ℤ) b
Tactic: rw [← hr, jacobiSymNat, jacobiSym.mod_left, hb', hab, ← h]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a : ℤ
b ab' : ℕ
ab r b' : ℤ
hb' : (↑b : ℤ) = b'
hab : a % b' = ab
h : (↑ab' : ℤ) = ab
hr : jacobiSymNat ab' b = r
rw : jacobiSym a b = jacobiSymNat ab' b
rw₁ : jacobiSym a b = jacobiSym (↑ab' : ℤ) b
rw₂ : jacobiSym (a % (↑b : ℤ)) b = jacobiSym (↑ab' : ℤ) b
rw₃ : jacobiSym (a % b') b = jacobiSym (↑ab' : ℤ) b
rw₄ : jacobiSym ab b = jacobiSym (↑ab' : ℤ) b
⊢ jacobiSym a b = r
have rw₅ : jacobiSym (↑ab' : ℤ) b = jacobiSym (↑ab' : ℤ) b
Tactic: rw [← hr, jacobiSymNat, jacobiSym.mod_left, hb', hab, ← h]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a b ab : ℕ
r : ℤ
hab : a % b = ab
hr : jacobiSymNat ab b = r
⊢ jacobiSymNat a b = r
have rw : jacobiSym (HMod.hMod (α := ℤ) (↑a : ℤ) (↑b : ℤ)) b = jacobiSym (↑(a % b) : ℤ) b
Tactic: rw [← hr, jacobiSymNat, jacobiSymNat, _root_.jacobiSym.mod_left a b, ← hab]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a b : ℕ
hb₀ : (b / 2).beq 0 = false
ha : a % 2 = 0
hb₁ : b % 2 = 0
⊢ jacobiSymNat a b = 0
have refine : ∀ (hf : Int.gcd (↑a : ℤ) (↑b : ℤ) = 1), False
Tactic: refine jacobiSym.eq_zero_iff.mpr
    ⟨ne_of_gt ((Nat.pos_of_ne_zero (Nat.ne_of_beq_eq_false hb₀)).trans_le (Nat.div_le_self b 2)),
      fun hf => ?_⟩
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (hypothesis)
Goal:
a b : ℕ
hb₀ : (b / 2).beq 0 = false
ha : a % 2 = 0
hb₁ : b % 2 = 0
hf : Int.gcd (↑a : ℤ) (↑b : ℤ) = 1
⊢ False
have h : 2 ∣ a.gcd b
Tactic: have h : 2 ∣ a.gcd b := Nat.dvd_gcd (Nat.dvd_of_mod_eq_zero ha) (Nat.dvd_of_mod_eq_zero hb₁)
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (hypothesis)
Goal:
a b : ℕ
hb₀ : (b / 2).beq 0 = false
ha : a % 2 = 0
hb₁ : b % 2 = 0
hf : Int.gcd (↑a : ℤ) (↑b : ℤ) = 1
h : 2 ∣ a.gcd b
⊢ False
have h₁ : 2 ∣ Int.gcd (↑a : ℤ) (↑b : ℤ)
Tactic: change 2 ∣ (a : ℤ).gcd b at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (hypothesis)
Goal:
a b : ℕ
hb₀ : (b / 2).beq 0 = false
ha : a % 2 = 0
hb₁ : b % 2 = 0
hf : Int.gcd (↑a : ℤ) (↑b : ℤ) = 1
h : 2 ∣ Int.gcd (↑a : ℤ) (↑b : ℤ)
⊢ False
have h₁ : Even (α := ℕ) 1
Tactic: rw [hf, ← even_iff_two_dvd] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
⊢ legendreSym 2 (↑a : ℤ) = 1
have simp : legendreSym 2 (↑1 : ℤ) = 1
Tactic: simp only [legendreSym.mod 2 a, Int.ofNat_mod_ofNat, ha]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (hypothesis)
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
⊢ jacobiSymNat a b = r
have ha' : legendreSym 2 (↑a : ℤ) = 1
Tactic: have ha' : legendreSym 2 a = 1 := by
    simp only [legendreSym.mod 2 a, Int.ofNat_mod_ofNat, ha]
    decide
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 (↑a : ℤ) = 1
⊢ jacobiSymNat a b = r
have inl : ∀ (hc : b / 2 = 0) (hr : jacobiSymNat a 0 = r), jacobiSymNat a b = r
Tactic: rcases eq_or_ne c 0 with (rfl | hc')
Cleared hypotheses: c, hc, hr
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 (↑a : ℤ) = 1
inl : ∀ (hc : b / 2 = 0) (hr : jacobiSymNat a 0 = r), jacobiSymNat a b = r
⊢ jacobiSymNat a b = r
have inr : ∀ (hc' : c ≠ 0), jacobiSymNat a b = r
Tactic: rcases eq_or_ne c 0 with (rfl | hc')
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a b : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
ha' : legendreSym 2 (↑a : ℤ) = 1
hc : b / 2 = 0
hr : jacobiSymNat a 0 = r
⊢ jacobiSymNat a b = r
have inl : jacobiSymNat a b = jacobiSymNat a 0
Tactic: rw [← hr, Nat.eq_zero_of_dvd_of_div_eq_zero (Nat.dvd_of_mod_eq_zero hb) hc]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a b : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
ha' : legendreSym 2 (↑a : ℤ) = 1
hc : b / 2 = 0
hr : jacobiSymNat a 0 = r
inl : jacobiSymNat a b = jacobiSymNat a 0
⊢ jacobiSymNat a b = r
have inl₁ : jacobiSymNat a 0 = jacobiSymNat a 0
Tactic: rw [← hr, Nat.eq_zero_of_dvd_of_div_eq_zero (Nat.dvd_of_mod_eq_zero hb) hc]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (hypothesis)
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 (↑a : ℤ) = 1
hc' : c ≠ 0
⊢ jacobiSymNat a b = r
have this : NeZero c
Tactic: haveI : NeZero c := ⟨hc'⟩
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 (↑a : ℤ) = 1
hc' : c ≠ 0
this : NeZero c
⊢ jacobiSymNat a b = r
have inr : jacobiSymNat a (b % 2 + 2 * (b / 2)) = r
Tactic: rwa [← Nat.mod_add_div b 2, hb, hc, Nat.zero_add, jacobiSymNat, jacobiSym.mul_right,
      ← jacobiSym.legendreSym.to_jacobiSym, ha', one_mul]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 (↑a : ℤ) = 1
hc' : c ≠ 0
this : NeZero c
inr : jacobiSymNat a (b % 2 + 2 * (b / 2)) = r
⊢ jacobiSymNat a b = r
have inr₁ : jacobiSymNat a (0 + 2 * (b / 2)) = r
Tactic: rwa [← Nat.mod_add_div b 2, hb, hc, Nat.zero_add, jacobiSymNat, jacobiSym.mul_right,
      ← jacobiSym.legendreSym.to_jacobiSym, ha', one_mul]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 (↑a : ℤ) = 1
hc' : c ≠ 0
this : NeZero c
inr : jacobiSymNat a (b % 2 + 2 * (b / 2)) = r
inr₁ : jacobiSymNat a (0 + 2 * (b / 2)) = r
⊢ jacobiSymNat a b = r
have inr₂ : jacobiSymNat a (0 + 2 * c) = r
Tactic: rwa [← Nat.mod_add_div b 2, hb, hc, Nat.zero_add, jacobiSymNat, jacobiSym.mul_right,
      ← jacobiSym.legendreSym.to_jacobiSym, ha', one_mul]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 (↑a : ℤ) = 1
hc' : c ≠ 0
this : NeZero c
inr : jacobiSymNat a (b % 2 + 2 * (b / 2)) = r
inr₁ : jacobiSymNat a (0 + 2 * (b / 2)) = r
inr₂ : jacobiSymNat a (0 + 2 * c) = r
⊢ jacobiSymNat a b = r
have inr₃ : jacobiSymNat a (2 * c) = r
Tactic: rwa [← Nat.mod_add_div b 2, hb, hc, Nat.zero_add, jacobiSymNat, jacobiSym.mul_right,
      ← jacobiSym.legendreSym.to_jacobiSym, ha', one_mul]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 (↑a : ℤ) = 1
hc' : c ≠ 0
this : NeZero c
inr : jacobiSymNat a (b % 2 + 2 * (b / 2)) = r
inr₁ : jacobiSymNat a (0 + 2 * (b / 2)) = r
inr₂ : jacobiSymNat a (0 + 2 * c) = r
inr₃ : jacobiSymNat a (2 * c) = r
⊢ jacobiSymNat a b = r
have inr₄ : jacobiSym (↑a : ℤ) (2 * c) = r
Tactic: rwa [← Nat.mod_add_div b 2, hb, hc, Nat.zero_add, jacobiSymNat, jacobiSym.mul_right,
      ← jacobiSym.legendreSym.to_jacobiSym, ha', one_mul]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 (↑a : ℤ) = 1
hc' : c ≠ 0
this : NeZero c
inr : jacobiSymNat a (b % 2 + 2 * (b / 2)) = r
inr₁ : jacobiSymNat a (0 + 2 * (b / 2)) = r
inr₂ : jacobiSymNat a (0 + 2 * c) = r
inr₃ : jacobiSymNat a (2 * c) = r
inr₄ : jacobiSym (↑a : ℤ) (2 * c) = r
⊢ jacobiSymNat a b = r
have inr₅ : jacobiSym (↑a : ℤ) 2 * jacobiSym (↑a : ℤ) c = r
Tactic: rwa [← Nat.mod_add_div b 2, hb, hc, Nat.zero_add, jacobiSymNat, jacobiSym.mul_right,
      ← jacobiSym.legendreSym.to_jacobiSym, ha', one_mul]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 (↑a : ℤ) = 1
hc' : c ≠ 0
this : NeZero c
inr : jacobiSymNat a (b % 2 + 2 * (b / 2)) = r
inr₁ : jacobiSymNat a (0 + 2 * (b / 2)) = r
inr₂ : jacobiSymNat a (0 + 2 * c) = r
inr₃ : jacobiSymNat a (2 * c) = r
inr₄ : jacobiSym (↑a : ℤ) (2 * c) = r
inr₅ : jacobiSym (↑a : ℤ) 2 * jacobiSym (↑a : ℤ) c = r
⊢ jacobiSymNat a b = r
have inr₆ : legendreSym 2 (↑a : ℤ) * jacobiSym (↑a : ℤ) c = r
Tactic: rwa [← Nat.mod_add_div b 2, hb, hc, Nat.zero_add, jacobiSymNat, jacobiSym.mul_right,
      ← jacobiSym.legendreSym.to_jacobiSym, ha', one_mul]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 (↑a : ℤ) = 1
hc' : c ≠ 0
this : NeZero c
inr : jacobiSymNat a (b % 2 + 2 * (b / 2)) = r
inr₁ : jacobiSymNat a (0 + 2 * (b / 2)) = r
inr₂ : jacobiSymNat a (0 + 2 * c) = r
inr₃ : jacobiSymNat a (2 * c) = r
inr₄ : jacobiSym (↑a : ℤ) (2 * c) = r
inr₅ : jacobiSym (↑a : ℤ) 2 * jacobiSym (↑a : ℤ) c = r
inr₆ : legendreSym 2 (↑a : ℤ) * jacobiSym (↑a : ℤ) c = r
⊢ jacobiSymNat a b = r
have inr₇ : 1 * jacobiSym (↑a : ℤ) c = r
Tactic: rwa [← Nat.mod_add_div b 2, hb, hc, Nat.zero_add, jacobiSymNat, jacobiSym.mul_right,
      ← jacobiSym.legendreSym.to_jacobiSym, ha', one_mul]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 (↑a : ℤ) = 1
hc' : c ≠ 0
this : NeZero c
inr : jacobiSymNat a (b % 2 + 2 * (b / 2)) = r
inr₁ : jacobiSymNat a (0 + 2 * (b / 2)) = r
inr₂ : jacobiSymNat a (0 + 2 * c) = r
inr₃ : jacobiSymNat a (2 * c) = r
inr₄ : jacobiSym (↑a : ℤ) (2 * c) = r
inr₅ : jacobiSym (↑a : ℤ) 2 * jacobiSym (↑a : ℤ) c = r
inr₆ : legendreSym 2 (↑a : ℤ) * jacobiSym (↑a : ℤ) c = r
inr₇ : 1 * jacobiSym (↑a : ℤ) c = r
⊢ jacobiSymNat a b = r
have inr₈ : jacobiSym (↑a : ℤ) c = r
Tactic: rwa [← Nat.mod_add_div b 2, hb, hc, Nat.zero_add, jacobiSymNat, jacobiSym.mul_right,
      ← jacobiSym.legendreSym.to_jacobiSym, ha', one_mul]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a b c : ℕ
r : ℤ
ha : a % 4 = 0
hb : b % 2 = 1
hc : a / 4 = c
hr : jacobiSymNat c b = r
⊢ jacobiSymNat a b = r
have simp : jacobiSym (↑a : ℤ) b = jacobiSym (HDiv.hDiv (α := ℤ) (↑a : ℤ) 4) b
Tactic: simp only [jacobiSymNat, ← hr, ← hc, Int.natCast_ediv, Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ jacobiSymNat a b = r
have simp : jacobiSym (↑a : ℤ) b = jacobiSym (HDiv.hDiv (α := ℤ) (↑a : ℤ) 2) b
Tactic: simp only [jacobiSymNat, ← hr, ← hc, Int.natCast_ediv, Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ jacobiSym (↑a : ℤ) b = jacobiSym (HDiv.hDiv (α := ℤ) (↑a : ℤ) 2) b
have rw : b % 2 = 1
Tactic: rw [← jacobiSym.even_odd (mod_cast ha), if_neg (by simp [hb])]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ b % 2 = 1
have h : Dvd.dvd (α := ℕ) 2 8
Tactic: rw [← Nat.mod_mod_of_dvd, hb]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ jacobiSymNat a b = r
have simp : jacobiSym (↑a : ℤ) b = jacobiSym (HDiv.hDiv (α := ℤ) (↑a : ℤ) 2) b
Tactic: simp only [jacobiSymNat, ← hr, ← hc, Int.natCast_ediv, Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ jacobiSym (↑a : ℤ) b = jacobiSym (HDiv.hDiv (α := ℤ) (↑a : ℤ) 2) b
have rw : b % 2 = 1
Tactic: rw [← jacobiSym.even_odd (mod_cast ha), if_neg (by simp [hb])]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ b % 2 = 1
have h : Dvd.dvd (α := ℕ) 2 8
Tactic: rw [← Nat.mod_mod_of_dvd, hb]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ jacobiSymNat a b = -r
have simp : jacobiSym (↑a : ℤ) b = -jacobiSym (HDiv.hDiv (α := ℤ) (↑a : ℤ) 2) b
Tactic: simp only [jacobiSymNat, ← hr, ← hc, Int.natCast_ediv, Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ jacobiSym (↑a : ℤ) b = -jacobiSym (HDiv.hDiv (α := ℤ) (↑a : ℤ) 2) b
have rw : b % 2 = 1
Tactic: rw [← jacobiSym.even_odd (mod_cast ha), if_pos (by simp [hb])]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ b % 2 = 1
have h : Dvd.dvd (α := ℕ) 2 8
Tactic: rw [← Nat.mod_mod_of_dvd, hb]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ jacobiSymNat a b = -r
have simp : jacobiSym (↑a : ℤ) b = -jacobiSym (HDiv.hDiv (α := ℤ) (↑a : ℤ) 2) b
Tactic: simp only [jacobiSymNat, ← hr, ← hc, Int.natCast_ediv, Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ jacobiSym (↑a : ℤ) b = -jacobiSym (HDiv.hDiv (α := ℤ) (↑a : ℤ) 2) b
have rw : b % 2 = 1
Tactic: rw [← jacobiSym.even_odd (mod_cast ha), if_pos (by simp [hb])]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ b % 2 = 1
have h : Dvd.dvd (α := ℕ) 2 8
Tactic: rw [← Nat.mod_mod_of_dvd, hb]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a b : ℕ
r : ℤ
ha : a % 4 = 1
hb : b % 2 = 1
hr : jacobiSymNat b a = r
⊢ jacobiSymNat a b = r
have rwa : jacobiSym (↑a : ℤ) b = r
Tactic: rwa [jacobiSymNat, jacobiSym.quadratic_reciprocity_one_mod_four ha (Nat.odd_iff.mpr hb)]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a b : ℕ
r : ℤ
ha : a % 4 = 1
hb : b % 2 = 1
hr : jacobiSymNat b a = r
rwa : jacobiSym (↑a : ℤ) b = r
⊢ jacobiSymNat a b = r
have rwa₁ : jacobiSym (↑b : ℤ) a = r
Tactic: rwa [jacobiSymNat, jacobiSym.quadratic_reciprocity_one_mod_four ha (Nat.odd_iff.mpr hb)]