awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
a : ℚ
n d : ℕ
hn : ¬IsSquare n
ha : IsNNRat a n d
hnd : LE.le (α := ℤ) (↑d : ℤ) 0
this : n ≠ 1
⊢ n.gcd d ≠ 1

Tactic:
simp_all
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
a : ℚ
n d : ℕ
hn : ¬IsSquare n
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ (Int.natAbs (↑n : ℤ)).Coprime (Int.natAbs (↑d : ℤ))

Tactic:
simpa
-- Module: Mathlib.Tactic.NormNum.IsSquare
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 : ℤ)
h : (Int.natAbs (↑n : ℤ)).Coprime (Int.natAbs (↑d : ℤ))
⊢ ¬IsSquare a

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]

Premises used: Int.cast_natCast, Mathlib.Meta.NormNum.IsNNRat.to_eq, Rat.isSquare_iff, Rat.den_div_eq_of_coprime, Int.isSquare_natCast_iff, rfl
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
a : ℚ
n d : ℕ
hd : ¬IsSquare d
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ ¬(IsSquare (HDiv.hDiv (α := ℚ) (↑(↑n : ℤ) : ℚ) (↑(↑d : ℤ) : ℚ)).num ∧ IsSquare (α := ℤ) (↑d : ℤ))

Tactic:
simp [hd]
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
a : ℚ
n d : ℕ
hd : ¬IsSquare d
hnd : n.Coprime d
ha : IsNNRat a n d
hb0 : ∀ (hnd : LE.le (α := ℤ) (↑d : ℤ) 0), n.gcd d ≠ 1
⊢ LT.lt (α := ℤ) 0 (↑d : ℤ)

Tactic:
contrapose! hnd
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
a : ℚ
n d : ℕ
hd : ¬IsSquare d
ha : IsNNRat a n d
hnd : LE.le (α := ℤ) (↑d : ℤ) 0
⊢ n.gcd d ≠ 1

Tactic:
simp_all
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
a : ℚ
n d : ℕ
hd : ¬IsSquare d
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ (Int.natAbs (↑n : ℤ)).Coprime (Int.natAbs (↑d : ℤ))

Tactic:
simpa
-- Module: Mathlib.Tactic.NormNum.IsSquare
Goal:
a : ℚ
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
ha : IsRat a (Int.negOfNat n) d
rw : ¬IsSquare (-HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ))
⊢ ¬IsSquare a

Tactic:
rw [ha.neg_to_eq rfl rfl]

Premises used: rfl, Mathlib.Meta.NormNum.IsRat.neg_to_eq
-- Module: Mathlib.Tactic.NormNum.IsSquare
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

Tactic:
absurd hq (ne_of_lt ?_)

Premises used: absurd, ne_of_lt
-- Module: Mathlib.Tactic.NormNum.IsSquare
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
refine : -HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) < q * q
⊢ False

Tactic:
refine absurd hq (ne_of_lt ?_)

Premises used: absurd, ne_of_lt
-- Module: Mathlib.Tactic.NormNum.IsSquare
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
rw : 0 < HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)
⊢ -HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) < 0

Tactic:
rw [Left.neg_neg_iff]

Premises used: Left.neg_neg_iff
-- Module: Mathlib.Tactic.NormNum.IsSquare
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 : ℚ)
hb : LT.lt (α := ℚ) 0 (↑d : ℚ)
⊢ 0 < HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)

Tactic:
apply div_pos

Premises used: div_pos
-- Module: Mathlib.Tactic.NormNum.IsSquare
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
⊢ LT.lt (α := ℚ) 0 (↑n : ℚ)

Tactic:
simpa [Nat.pos_iff_ne_zero]

Premises used: Nat.pos_iff_ne_zero
-- Module: Mathlib.Tactic.NormNum.IsSquare
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
⊢ LT.lt (α := ℚ) 0 (↑d : ℚ)

Tactic:
simpa [Nat.pos_iff_ne_zero]

Premises used: Nat.pos_iff_ne_zero
-- Module: Mathlib.Tactic.NormNum.IsSquare
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 ≤ q * q

Tactic:
mul_self_nonneg _

Premises used: mul_self_nonneg
-- Module: Mathlib.Tactic.NormNum.IsSquare
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
d₁ : -HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) < 0
⊢ -HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) < q * q

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 _

Premises used: mul_self_nonneg, HDiv.hDiv, Nat.cast
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a : ℕ
rw : jacobiSym (↑a : ℤ) 0 = 1
rw₁ rw₂ : Eq (α := ℤ) 1 1
⊢ jacobiSymNat a 0 = 1

Tactic:
rw [jacobiSymNat, jacobiSym.zero_right]

Premises used: Mathlib.Meta.NormNum.jacobiSymNat, jacobiSym.zero_right
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a : ℕ
rw : jacobiSym (↑a : ℤ) 1 = 1
rw₁ rw₂ : Eq (α := ℤ) 1 1
⊢ jacobiSymNat a 1 = 1

Tactic:
rw [jacobiSymNat, jacobiSym.one_right]

Premises used: jacobiSym.one_right, Mathlib.Meta.NormNum.jacobiSymNat
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
b : ℕ
hb : (b / 2).beq 0 = false
rw : 1 < b
⊢ jacobiSymNat 0 b = 0

Tactic:
rw [jacobiSymNat, Nat.cast_zero, jacobiSym.zero_left ?_]

Premises used: jacobiSym.zero_left, Mathlib.Meta.NormNum.jacobiSymNat, Nat.cast_zero
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
b : ℕ
hb : (b / 2).beq 0 = false
⊢ 1 < HMul.hMul (α := ℕ) 2 1

Tactic:
decide
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
b : ℕ
hb : (b / 2).beq 0 = false
⊢ HMul.hMul (α := ℕ) 2 1 ≤ 2 * (b / 2)

Tactic:
Nat.mul_le_mul_left _ (Nat.succ_le_of_lt (Nat.pos_of_ne_zero (Nat.ne_of_beq_eq_false hb)))

Premises used: Nat.ne_of_beq_eq_false, Nat.succ_le_of_lt, Nat.mul_le_mul_left, Nat.pos_of_ne_zero
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
b : ℕ
hb : (b / 2).beq 0 = false
⊢ 2 * (b / 2) ≤ b

Tactic:
Nat.mul_div_le b 2

Premises used: Nat.mul_div_le, OfNat.ofNat
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
b : ℕ
hb : (b / 2).beq 0 = false
by : 1 < HMul.hMul (α := ℕ) 2 1
⊢ 1 < b

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

Premises used: Nat.ne_of_beq_eq_false, Nat.succ_le_of_lt, HDiv.hDiv, Nat.mul_le_mul_left, Nat.pos_of_ne_zero, Nat.mul_div_le, OfNat.ofNat
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
b : ℕ
rw : jacobiSym (↑1 : ℤ) b = 1
rw₁ : jacobiSym 1 b = 1
rw₂ rw₃ : Eq (α := ℤ) 1 1
⊢ jacobiSymNat 1 b = 1

Tactic:
rw [jacobiSymNat, Nat.cast_one, jacobiSym.one_left]

Premises used: jacobiSym.one_left, Mathlib.Meta.NormNum.jacobiSymNat, Nat.cast_one
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
p : ℕ
pp : Fact (Nat.Prime p)
a r : ℤ
hr rwa rwa₁ rwa₂ rwa₃ : IsInt (jacobiSym a p) r
⊢ IsInt (legendreSym p a) r

Tactic:
rwa [@jacobiSym.legendreSym.to_jacobiSym p pp a]

Premises used: jacobiSym.legendreSym.to_jacobiSym
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
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
rw₅ rw₆ : jacobiSym (↑ab' : ℤ) b = jacobiSym (↑ab' : ℤ) b
⊢ jacobiSym a b = r

Tactic:
rw [← hr, jacobiSymNat, jacobiSym.mod_left, hb', hab, ← h]

Premises used: jacobiSym.mod_left, Mathlib.Meta.NormNum.jacobiSymNat
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b ab : ℕ
r : ℤ
hab : a % b = ab
hr : jacobiSymNat ab b = r
rw : jacobiSym (HMod.hMod (α := ℤ) (↑a : ℤ) (↑b : ℤ)) b = jacobiSym (↑(a % b) : ℤ) b
⊢ jacobiSymNat a b = r

Tactic:
rw [← hr, jacobiSymNat, jacobiSymNat, _root_.jacobiSym.mod_left a b, ← hab]

Premises used: jacobiSym.mod_left, Nat.cast, Mathlib.Meta.NormNum.jacobiSymNat
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b ab : ℕ
r : ℤ
hab : a % b = ab
hr : jacobiSymNat ab b = r
⊢ jacobiSym (HMod.hMod (α := ℤ) (↑a : ℤ) (↑b : ℤ)) b = jacobiSym (↑(a % b) : ℤ) b

Tactic:
rfl
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b : ℕ
hb₀ : (b / 2).beq 0 = false
ha : a % 2 = 0
hb₁ : b % 2 = 0
⊢ jacobiSymNat a b = 0

Tactic:
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 => ?_⟩

Premises used: Iff.mpr, Nat.ne_of_beq_eq_false, ne_of_gt, Nat.div_le_self, Nat.pos_of_ne_zero, Mathlib.Meta.NormNum.jacobiSymNat, LT.lt.trans_le, And.intro, jacobiSym.eq_zero_iff, OfNat.ofNat
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b : ℕ
hb₀ : (b / 2).beq 0 = false
ha : a % 2 = 0
hb₁ : b % 2 = 0
refine : ∀ (hf : Int.gcd (↑a : ℤ) (↑b : ℤ) = 1), False
⊢ jacobiSymNat a b = 0

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 => ?_⟩

Premises used: Iff.mpr, Nat.ne_of_beq_eq_false, ne_of_gt, Nat.div_le_self, Nat.pos_of_ne_zero, LT.lt.trans_le, And.intro, jacobiSym.eq_zero_iff, OfNat.ofNat
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b : ℕ
hb₀ : (b / 2).beq 0 = false
ha : a % 2 = 0
hb₁ : b % 2 = 0
hf : Int.gcd (↑a : ℤ) (↑b : ℤ) = 1
⊢ 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₁)
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
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
⊢ 2 ∣ Int.gcd (↑a : ℤ) (↑b : ℤ)

Tactic:
change 2 ∣ (a : ℤ).gcd b at h

Premises used: Int.gcd, Nat.cast
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
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 : ℤ)
⊢ Even (α := ℕ) 1

Tactic:
rw [hf, ← even_iff_two_dvd] at h

Premises used: even_iff_two_dvd
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b : ℕ
hb₀ : (b / 2).beq 0 = false
ha : a % 2 = 0
hb₁ : b % 2 = 0
hf : Int.gcd (↑a : ℤ) (↑b : ℤ) = 1
h : Even (α := ℕ) 1
⊢ False

Tactic:
Nat.not_even_one h

Premises used: Nat.not_even_one
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b : ℕ
hb₀ : (b / 2).beq 0 = false
ha : a % 2 = 0
hb₁ : b % 2 = 0
hf : Int.gcd (↑a : ℤ) (↑b : ℤ) = 1
h : Even (α := ℕ) 1
⊢ False

Tactic:
exact Nat.not_even_one h

Premises used: Nat.not_even_one
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
simp : legendreSym 2 (↑1 : ℤ) = 1
⊢ legendreSym 2 (↑a : ℤ) = 1

Tactic:
simp only [legendreSym.mod 2 a, Int.ofNat_mod_ofNat, ha]

Premises used: legendreSym.mod, Nat.cast, Int.ofNat_mod_ofNat, OfNat.ofNat
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
⊢ legendreSym 2 (↑1 : ℤ) = 1

Tactic:
decide
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
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

Tactic:
have ha' : legendreSym 2 a = 1 := by
    simp only [legendreSym.mod 2 a, Int.ofNat_mod_ofNat, ha]
    decide
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
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
inr : ∀ (hc' : c ≠ 0), jacobiSymNat a b = r
⊢ jacobiSymNat a b = r

Tactic:
rcases eq_or_ne c 0 with (rfl | hc')

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
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
inl₁ inl₂ : jacobiSymNat a 0 = jacobiSymNat a 0
⊢ jacobiSymNat a b = r

Tactic:
rw [← hr, Nat.eq_zero_of_dvd_of_div_eq_zero (Nat.dvd_of_mod_eq_zero hb) hc]

Premises used: Nat.dvd_of_mod_eq_zero, Nat.eq_zero_of_dvd_of_div_eq_zero
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
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
⊢ NeZero c

Tactic:
haveI : NeZero c := ⟨hc'⟩
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
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
inr₈ inr₉ inr₁₀ inr₁₁ : jacobiSym (↑a : ℤ) c = r
⊢ jacobiSymNat a b = 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]

Premises used: jacobiSym.mul_right, jacobiSym.legendreSym.to_jacobiSym, Nat.mod_add_div, Mathlib.Meta.NormNum.jacobiSymNat, Nat.zero_add, OfNat.ofNat, one_mul
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b c : ℕ
r : ℤ
ha : a % 4 = 0
hb : b % 2 = 1
hc : a / 4 = c
hr : jacobiSymNat c b = r
simp : jacobiSym (↑a : ℤ) b = jacobiSym (HDiv.hDiv (α := ℤ) (↑a : ℤ) 4) b
⊢ jacobiSymNat a b = r

Tactic:
simp only [jacobiSymNat, ← hr, ← hc, Int.natCast_ediv, Nat.cast_ofNat]

Premises used: Nat.cast_ofNat, Int.natCast_ediv, Mathlib.Meta.NormNum.jacobiSymNat
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b c : ℕ
r : ℤ
ha : a % 4 = 0
hb : b % 2 = 1
hc : a / 4 = c
hr : jacobiSymNat c b = r
⊢ jacobiSym (↑a : ℤ) b = jacobiSym (HDiv.hDiv (α := ℤ) (↑a : ℤ) 4) b

Tactic:
(jacobiSym.div_four_left (mod_cast ha) hb).symm

Premises used: jacobiSym.div_four_left, Eq.symm
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b c : ℕ
r : ℤ
ha : a % 4 = 0
hb : b % 2 = 1
hc : a / 4 = c
hr : jacobiSymNat c b = r
⊢ jacobiSym (↑a : ℤ) b = jacobiSym (HDiv.hDiv (α := ℤ) (↑a : ℤ) 4) b

Tactic:
exact (jacobiSym.div_four_left (mod_cast ha) hb).symm

Premises used: jacobiSym.div_four_left, Eq.symm
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
simp : jacobiSym (↑a : ℤ) b = jacobiSym (HDiv.hDiv (α := ℤ) (↑a : ℤ) 2) b
⊢ jacobiSymNat a b = r

Tactic:
simp only [jacobiSymNat, ← hr, ← hc, Int.natCast_ediv, Nat.cast_ofNat]

Premises used: Nat.cast_ofNat, Int.natCast_ediv, Mathlib.Meta.NormNum.jacobiSymNat
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ ¬(b % 8 = 3 ∨ b % 8 = 5)

Tactic:
simp [hb]
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
rw : b % 2 = 1
⊢ jacobiSym (↑a : ℤ) b = jacobiSym (HDiv.hDiv (α := ℤ) (↑a : ℤ) 2) b

Tactic:
rw [← jacobiSym.even_odd (mod_cast ha), if_neg (by simp [hb])]

Premises used: if_neg, jacobiSym.even_odd
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
h : Dvd.dvd (α := ℕ) 2 8
⊢ b % 2 = 1

Tactic:
rw [← Nat.mod_mod_of_dvd, hb]

Premises used: Nat.mod_mod_of_dvd
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ Dvd.dvd (α := ℕ) 2 8

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
simp : jacobiSym (↑a : ℤ) b = jacobiSym (HDiv.hDiv (α := ℤ) (↑a : ℤ) 2) b
⊢ jacobiSymNat a b = r

Tactic:
simp only [jacobiSymNat, ← hr, ← hc, Int.natCast_ediv, Nat.cast_ofNat]

Premises used: Nat.cast_ofNat, Int.natCast_ediv, Mathlib.Meta.NormNum.jacobiSymNat
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ ¬(b % 8 = 3 ∨ b % 8 = 5)

Tactic:
simp [hb]
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
rw : b % 2 = 1
⊢ jacobiSym (↑a : ℤ) b = jacobiSym (HDiv.hDiv (α := ℤ) (↑a : ℤ) 2) b

Tactic:
rw [← jacobiSym.even_odd (mod_cast ha), if_neg (by simp [hb])]

Premises used: if_neg, jacobiSym.even_odd
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
h : Dvd.dvd (α := ℕ) 2 8
⊢ b % 2 = 1

Tactic:
rw [← Nat.mod_mod_of_dvd, hb]

Premises used: Nat.mod_mod_of_dvd
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ Dvd.dvd (α := ℕ) 2 8

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
simp : jacobiSym (↑a : ℤ) b = -jacobiSym (HDiv.hDiv (α := ℤ) (↑a : ℤ) 2) b
⊢ jacobiSymNat a b = -r

Tactic:
simp only [jacobiSymNat, ← hr, ← hc, Int.natCast_ediv, Nat.cast_ofNat]

Premises used: Nat.cast_ofNat, Int.natCast_ediv, Mathlib.Meta.NormNum.jacobiSymNat
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ b % 8 = 3 ∨ b % 8 = 5

Tactic:
simp [hb]
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
rw : b % 2 = 1
⊢ jacobiSym (↑a : ℤ) b = -jacobiSym (HDiv.hDiv (α := ℤ) (↑a : ℤ) 2) b

Tactic:
rw [← jacobiSym.even_odd (mod_cast ha), if_pos (by simp [hb])]

Premises used: if_pos, jacobiSym.even_odd
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
h : Dvd.dvd (α := ℕ) 2 8
⊢ b % 2 = 1

Tactic:
rw [← Nat.mod_mod_of_dvd, hb]

Premises used: Nat.mod_mod_of_dvd
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ Dvd.dvd (α := ℕ) 2 8

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
simp : jacobiSym (↑a : ℤ) b = -jacobiSym (HDiv.hDiv (α := ℤ) (↑a : ℤ) 2) b
⊢ jacobiSymNat a b = -r

Tactic:
simp only [jacobiSymNat, ← hr, ← hc, Int.natCast_ediv, Nat.cast_ofNat]

Premises used: Nat.cast_ofNat, Int.natCast_ediv, Mathlib.Meta.NormNum.jacobiSymNat
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ b % 8 = 3 ∨ b % 8 = 5

Tactic:
simp [hb]
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
rw : b % 2 = 1
⊢ jacobiSym (↑a : ℤ) b = -jacobiSym (HDiv.hDiv (α := ℤ) (↑a : ℤ) 2) b

Tactic:
rw [← jacobiSym.even_odd (mod_cast ha), if_pos (by simp [hb])]

Premises used: if_pos, jacobiSym.even_odd
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
h : Dvd.dvd (α := ℕ) 2 8
⊢ b % 2 = 1

Tactic:
rw [← Nat.mod_mod_of_dvd, hb]

Premises used: Nat.mod_mod_of_dvd
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ Dvd.dvd (α := ℕ) 2 8

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b : ℕ
r : ℤ
ha : a % 4 = 1
hb : b % 2 = 1
hr : jacobiSymNat b a = r
rwa : jacobiSym (↑a : ℤ) b = r
rwa₁ rwa₂ rwa₃ rwa₄ : jacobiSym (↑b : ℤ) a = r
⊢ jacobiSymNat a b = r

Tactic:
rwa [jacobiSymNat, jacobiSym.quadratic_reciprocity_one_mod_four ha (Nat.odd_iff.mpr hb)]

Premises used: Iff.mpr, jacobiSym.quadratic_reciprocity_one_mod_four, Mathlib.Meta.NormNum.jacobiSymNat, Nat.odd_iff
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b ab : ℕ
r : ℤ
ha : a % 4 = 1
hb : b % 2 = 1
hab : b % a = ab
hr : jacobiSymNat ab a = r
⊢ jacobiSymNat a b = r

Tactic:
jacobiSymNat.qr₁ _ _ _ ha hb <| jacobiSymNat.mod_left _ _ ab r hab hr

Premises used: Mathlib.Meta.NormNum.jacobiSymNat.mod_left, Mathlib.Meta.NormNum.jacobiSymNat.qr₁
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 4 = 1
hr : jacobiSymNat b a = r
rwa : jacobiSym (↑a : ℤ) b = r
rwa₁ rwa₂ rwa₃ rwa₄ : jacobiSym (↑b : ℤ) a = r
⊢ jacobiSymNat a b = r

Tactic:
rwa [jacobiSymNat, ← jacobiSym.quadratic_reciprocity_one_mod_four hb (Nat.odd_iff.mpr ha)]

Premises used: Iff.mpr, jacobiSym.quadratic_reciprocity_one_mod_four, Mathlib.Meta.NormNum.jacobiSymNat, Nat.odd_iff
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b ab : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 4 = 1
hab : b % a = ab
hr : jacobiSymNat ab a = r
⊢ jacobiSymNat a b = r

Tactic:
jacobiSymNat.qr₁' _ _ _ ha hb <| jacobiSymNat.mod_left _ _ ab r hab hr

Premises used: Mathlib.Meta.NormNum.jacobiSymNat.mod_left, Mathlib.Meta.NormNum.jacobiSymNat.qr₁'
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b : ℕ
r : ℤ
ha : a % 4 = 3
hb : b % 4 = 3
hr : jacobiSymNat b a = r
rwa : jacobiSym (↑a : ℤ) b = -r
rwa₁ : -jacobiSym (↑b : ℤ) a = -r
rwa₂ rwa₃ rwa₄ rwa₅ : jacobiSym (↑b : ℤ) a = r
⊢ jacobiSymNat a b = -r

Tactic:
rwa [jacobiSymNat, jacobiSym.quadratic_reciprocity_three_mod_four ha hb, neg_inj]

Premises used: Mathlib.Meta.NormNum.jacobiSymNat, neg_inj, jacobiSym.quadratic_reciprocity_three_mod_four
-- Module: Mathlib.Tactic.NormNum.LegendreSymbol
Goal:
a b ab : ℕ
r : ℤ
ha : a % 4 = 3
hb : b % 4 = 3
hab : b % a = ab
hr : jacobiSymNat ab a = r
⊢ jacobiSymNat a b = -r

Tactic:
jacobiSymNat.qr₃ _ _ _ ha hb <| jacobiSymNat.mod_left _ _ ab r hab hr

Premises used: Mathlib.Meta.NormNum.jacobiSymNat.mod_left, Mathlib.Meta.NormNum.jacobiSymNat.qr₃
-- Module: Mathlib.Tactic.NormNum.NatFactorial
Goal:
n l m a b : ℕ
h₁ : n.ascFactorial l = a
h₂ : (n + l).ascFactorial m = b
rw : n.ascFactorial (l + m) = n.ascFactorial l * (n + l).ascFactorial m
⊢ n.ascFactorial (l + m) = a * b

Tactic:
rw [← h₁, ← h₂]
-- Module: Mathlib.Tactic.NormNum.NatFactorial
Goal:
n l m a b : ℕ
h₁ : n.ascFactorial l = a
h₂ : (n + l).ascFactorial m = b
symm : n.ascFactorial l * (n + l).ascFactorial m = n.ascFactorial (l + m)
⊢ n.ascFactorial (l + m) = n.ascFactorial l * (n + l).ascFactorial m

Tactic:
symm
-- Module: Mathlib.Tactic.NormNum.NatFactorial
Goal:
n l m a b : ℕ
h₁ : n.ascFactorial l = a
h₂ : (n + l).ascFactorial m = b
⊢ n.ascFactorial l * (n + l).ascFactorial m = n.ascFactorial (l + m)

Tactic:
apply ascFactorial_mul_ascFactorial

Premises used: Nat.ascFactorial_mul_ascFactorial
-- Module: Mathlib.Tactic.NormNum.NatFactorial
Goal:
«$n» «$l» «$en» «$el» «$m» : ℕ
«$em» : ℕ := «$el» / 2
«$r» : ℕ
«$er» : ℕ := «$el» - «$em»
«$this» : «$el» = «$em» + «$er»
«$nm» : ℕ
«$enm» : ℕ := «$en» + «$em»
«$a» «$ea» : ℕ
«$a_prf» : «$en».ascFactorial «$em» = «$ea»
«$b» «$eb» : ℕ
«$b_prf» : «$enm».ascFactorial «$er» = «$eb»
«$eab» : ℕ := «$ea» * «$eb»
⊢ «$en».ascFactorial («$em» + «$er») = «$ea» * «$eb»

Tactic:
asc_factorial_aux «$en» «$em» «$er» «$ea» «$eb» «$a_prf» «$b_prf»

Premises used: Mathlib.Meta.NormNum.asc_factorial_aux
-- Module: Mathlib.Tactic.NormNum.NatFactorial
Goal:
«$n» «$l» «$en» «$el» «$m» : ℕ
«$em» : ℕ := «$el» / 2
«$r» : ℕ
«$er» : ℕ := «$el» - «$em»
«$this» : «$el» = «$em» + «$er»
«$nm» : ℕ
«$enm» : ℕ := «$en» + «$em»
«$a» «$ea» : ℕ
«$a_prf» : «$en».ascFactorial «$em» = «$ea»
«$b» «$eb» : ℕ
«$b_prf» : «$enm».ascFactorial «$er» = «$eb»
«$eab» : ℕ := «$ea» * «$eb»
⊢ «$en».ascFactorial «$el» = «$eab»

Tactic:
convert! asc_factorial_aux «$en» «$em» «$er» «$ea» «$eb» «$a_prf» «$b_prf»

Premises used: Mathlib.Meta.NormNum.asc_factorial_aux
-- Module: Mathlib.Tactic.NormNum.NatFactorial
Goal:
n x : ℕ
h₁ : IsNat n x
a : ℕ
h₂ : ascFactorial 1 x = a
out : n ! = (↑a : ℕ)
⊢ IsNat n ! a

Tactic:
constructor