awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Tactic.NormNum.PowMod
Goal:
a b m c : ℕ
h1 : (a.pow b).mod m = c
simp : (a ^ b * a ^ b).mod m = ((a ^ b).mod m * (a ^ b).mod m).mod m
⊢ (a.pow (2 * b)).mod m = (c.mul c).mod m

Tactic:
simp only [two_mul, Nat.pow_eq, pow_add, ← h1, Nat.mul_eq]

Premises used: Nat.pow_eq, two_mul, pow_add, Nat.mul_eq
-- Module: Mathlib.Tactic.NormNum.PowMod
Goal:
a b m c : ℕ
h1 : (a.pow b).mod m = c
⊢ (a ^ b * a ^ b).mod m = ((a ^ b).mod m * (a ^ b).mod m).mod m

Tactic:
Nat.mul_mod ..

Premises used: Nat.mul_mod
-- Module: Mathlib.Tactic.NormNum.PowMod
Goal:
a b m c : ℕ
h1 : (a.pow b).mod m = c
⊢ (a ^ b * a ^ b).mod m = ((a ^ b).mod m * (a ^ b).mod m).mod m

Tactic:
exact Nat.mul_mod ..

Premises used: Nat.mul_mod
-- Module: Mathlib.Tactic.NormNum.PowMod
Goal:
a : ℕ
⊢ (a.pow 0).mod 0 = 1

Tactic:
simp [Nat.mod, Nat.modCore]

Premises used: Nat.modCore, Nat.mod
-- Module: Mathlib.Tactic.NormNum.PowMod
Goal:
a : ℕ
⊢ (a.pow 0).mod 1 = 0

Tactic:
simp [Nat.mod, Nat.modCore_eq]

Premises used: Nat.modCore_eq, Nat.mod
-- Module: Mathlib.Tactic.NormNum.PowMod
Goal:
a m : ℕ
⊢ (a.pow 0).mod m.succ.succ = 1

Tactic:
rfl
-- Module: Mathlib.Tactic.NormNum.PowMod
Goal:
a m : ℕ
rw rw₁ : a.mod m = a.mod m
⊢ (a.pow 1).mod m = a.mod m

Tactic:
rw [natPow_one]

Premises used: Mathlib.Meta.NormNum.natPow_one
-- Module: Mathlib.Tactic.NormNum.PowMod
Goal:
a b m : ℕ
rw : a ^ (2 * b) * HPow.hPow (β := ℕ) a 1 % m = a ^ b % m * (a ^ b % m * a % m) % m
rw₁ : a ^ (b + b) * HPow.hPow (β := ℕ) a 1 % m = a ^ b % m * (a ^ b % m * a % m) % m
rw₂ : a ^ b * a ^ b * HPow.hPow (β := ℕ) a 1 % m = a ^ b % m * (a ^ b % m * a % m) % m
rw₃ : a ^ b * a ^ b * a % m = a ^ b % m * (a ^ b % m * a % m) % m
rw₄ : a ^ b * a ^ b * a % m = a ^ b % m * (a ^ b % m % m * (a % m) % m) % m
rw₅ : a ^ b * a ^ b * a % m = a ^ b % m * (a ^ b % m * (a % m) % m) % m
rw₆ : a ^ b * a ^ b * a % m = a ^ b % m * (a ^ b * a % m) % m
rw₇ : a ^ b * a ^ b * a % m = a ^ b * (a ^ b * a) % m
rw₈ rw₉ : a ^ b * (a ^ b * a) % m = a ^ b * (a ^ b * a) % m
⊢ a ^ (2 * b + 1) % m = a ^ b % m * (a ^ b % m * a % m) % m

Tactic:
rw [pow_add, two_mul, pow_add, pow_one, Nat.mul_mod (a ^ b % m) a, Nat.mod_mod,
      ← Nat.mul_mod (a ^ b) a, ← Nat.mul_mod, mul_assoc]

Premises used: Nat.mod_mod, mul_assoc, two_mul, pow_add, Nat.mul_mod, HMod.hMod, HPow.hPow, pow_one
-- Module: Mathlib.Tactic.NormNum.PowMod
Goal:
a_1 b_1 m_1 : Q(ℕ)
depth : ℕ
a m b₀ c₀ b : Q(ℕ)
p : Q(Prop)
hp : «$p» =Q Eq «$c₀»
b' : ℕ := Expr.natLit! b
m' : ℕ := Expr.natLit! m
d : ℕ := HShiftRight.hShiftRight (β := ℕ) depth 1
hi : Q(ℕ)
⊢ «$p» =Q Eq «$c₀»

Tactic:
hp
-- Module: Mathlib.Tactic.NormNum.PowMod
Goal:
a_1 b_1 m_1 : Q(ℕ)
depth : ℕ
a m b₀ c₀ b : Q(ℕ)
p : Q(Prop)
hp : «$p» =Q Eq «$c₀»
b' : ℕ := Expr.natLit! b
m' : ℕ := Expr.natLit! m
d : ℕ := HShiftRight.hShiftRight (β := ℕ) depth 1
hi : Q(ℕ)
⊢ «$p» =Q Eq «$c₀»

Tactic:
exact hp
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
a b n : ℕ
h : a * b = n
h₁ : a.ble 1 = false
h₂ : b.ble 1 = false
⊢ ¬Nat.Prime n

Tactic:
not_prime_of_mul_eq h (ble_eq_false.mp h₁).ne' (ble_eq_false.mp h₂).ne'

Premises used: Nat.not_prime_of_mul_eq, Mathlib.Meta.NormNum.ble_eq_false, LT.lt.ne', Iff.mp
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k : ℕ
h : MinFacHelper n k
⊢ 2 < n.minFac

Tactic:
have : 2 < minFac n := h.1.trans_le h.2.2
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k : ℕ
h : MinFacHelper n k
this : 2 < n.minFac
inl : ∀ (h : MinFacHelper 0 k) (this : 2 < minFac 0), LT.lt (α := ℕ) 1 0
inr : ∀ (h : n > 0), 1 < n
⊢ 1 < n

Tactic:
obtain rfl | h := n.eq_zero_or_pos

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
k : ℕ
h : MinFacHelper 0 k
this : 2 < minFac 0
⊢ LT.lt (α := ℕ) 1 0

Tactic:
contradiction
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k : ℕ
h_1 : MinFacHelper n k
this : 2 < n.minFac
h : n > 0
inr : ∀ (h : MinFacHelper (succ 0) k) (this : 2 < (succ 0).minFac) (h : succ 0 > 0), 1 < succ 0
inr₁ : ∀ (h : succ 0 < n), 1 < n
⊢ 1 < n

Tactic:
rcases (succ_le_of_lt h).eq_or_lt with rfl | h

Premises used: LE.le.eq_or_lt, Nat.succ_le_of_lt, rfl
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
k : ℕ
h_1 : MinFacHelper (succ 0) k
this : 2 < (succ 0).minFac
h : succ 0 > 0
⊢ 1 < succ 0

Tactic:
simp_all
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k : ℕ
h_1 : MinFacHelper n k
this : 2 < n.minFac
h_2 : n > 0
h : succ 0 < n
⊢ 1 < n

Tactic:
h
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k : ℕ
h_1 : MinFacHelper n k
this : 2 < n.minFac
h_2 : n > 0
h : succ 0 < n
⊢ 1 < n

Tactic:
exact h
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
⊢ 2 < 3

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
⊢ 3 % 2 = 1

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
refine : 3 ≤ n.minFac
⊢ MinFacHelper n 3

Tactic:
refine ⟨by simp, by simp, ?_⟩
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
⊢ 3 ≤ n.minFac

Tactic:
(le_minFac'.mpr fun p hp hpn ↦ ?_).resolve_left (Nat.ne_of_gt (Nat.le_of_ble_eq_true h1))

Premises used: Iff.mpr, Nat.le_of_ble_eq_true, Or.resolve_left, Nat.le_minFac', Nat.ne_of_gt
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
refine : ∀ (p : ℕ) (hp : 2 ≤ p) (hpn : p ∣ n), 3 ≤ p
⊢ 3 ≤ n.minFac

Tactic:
refine (le_minFac'.mpr fun p hp hpn ↦ ?_).resolve_left (Nat.ne_of_gt (Nat.le_of_ble_eq_true h1))

Premises used: Iff.mpr, Nat.le_of_ble_eq_true, Or.resolve_left, Nat.le_minFac', Nat.ne_of_gt
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
p : ℕ
hp : 2 ≤ p
hpn : p ∣ n
inl : ∀ (hp : LE.le (α := ℕ) 2 2) (hpn : 2 ∣ n), 3 ≤ 2
inr : ∀ (h : 2 < p), 3 ≤ p
⊢ 3 ≤ p

Tactic:
rcases hp.eq_or_lt with rfl | h

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
hp : LE.le (α := ℕ) 2 2
hpn : 2 ∣ n
⊢ 3 ≤ 2

Tactic:
simp [(Nat.dvd_iff_mod_eq_zero ..).1 hpn] at h2

Premises used: Nat.dvd_iff_mod_eq_zero, Iff.mp
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
p : ℕ
hp : 2 ≤ p
hpn : p ∣ n
h : 2 < p
⊢ 3 ≤ p

Tactic:
h

Premises used: Nat.lt
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
p : ℕ
hp : 2 ≤ p
hpn : p ∣ n
h : 2 < p
⊢ 3 ≤ p

Tactic:
exact h
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
rw : MinFacHelper n (k + 2)
⊢ MinFacHelper n k'

Tactic:
rw [← e]
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
⊢ MinFacHelper n (k + 2)

Tactic:
⟨Nat.lt_add_right _ h.1, ?_, ?_⟩

Premises used: Mathlib.Meta.NormNum.MinFacHelper, And.left, And.intro, Nat.lt_add_right
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
refine_1 : (k + 2) % 2 = 1
refine_2 : k + 2 ≤ n.minFac
⊢ MinFacHelper n (k + 2)

Tactic:
refine ⟨Nat.lt_add_right _ h.1, ?_, ?_⟩
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
refine_1 : k % 2 = 1
⊢ (k + 2) % 2 = 1

Tactic:
rw [add_mod, mod_self, add_zero, mod_mod]

Premises used: Nat.mod_self, Nat.mod_mod, Nat.add_mod, add_zero
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
⊢ k % 2 = 1

Tactic:
h.2.1

Premises used: And.right, And.left
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
⊢ k % 2 = 1

Tactic:
exact h.2.1

Premises used: And.right, And.left
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
refine_2 : ∀ (e : n.minFac + 2 = k') (h : MinFacHelper n n.minFac) (np : n.minFac ≠ n.minFac), n.minFac + 2 ≤ n.minFac
refine_2₁ : ∀ (h2 : k < n.minFac), k + 2 ≤ n.minFac
⊢ k + 2 ≤ n.minFac

Tactic:
rcases h.2.2.eq_or_lt with rfl | h2

Premises used: LE.le.eq_or_lt, And.right, rfl
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k' : ℕ
e : n.minFac + 2 = k'
h : MinFacHelper n n.minFac
np : n.minFac ≠ n.minFac
⊢ n.minFac + 2 ≤ n.minFac

Tactic:
(np rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k' : ℕ
e : n.minFac + 2 = k'
h : MinFacHelper n n.minFac
np : n.minFac ≠ n.minFac
⊢ n.minFac + 2 ≤ n.minFac

Tactic:
exact (np rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
h2 : k < n.minFac
refine_2 : ∀ (h2 : k.succ = n.minFac), k + 2 ≤ n.minFac
refine_2₁ : ∀ (h2 : k.succ < n.minFac), k + 2 ≤ n.minFac
⊢ k + 2 ≤ n.minFac

Tactic:
rcases (succ_le_of_lt h2).eq_or_lt with h2|h2

Premises used: LE.le.eq_or_lt, Nat.succ_le_of_lt
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
h2_1 : k < n.minFac
h2 : k.succ = n.minFac
⊢ k + 2 ≤ n.minFac

Tactic:
((h.1.trans_le h.2.2).ne ?_).elim

Premises used: False.elim, And.right, And.left, LT.lt.trans_le, LT.lt.ne
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
h2_1 : k < n.minFac
h2 : k.succ = n.minFac
refine_2 : 2 = n.minFac
⊢ k + 2 ≤ n.minFac

Tactic:
refine ((h.1.trans_le h.2.2).ne ?_).elim

Premises used: False.elim, And.right, And.left, LT.lt.trans_le, LT.lt.ne
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
h2_1 : k < n.minFac
h2 : k.succ = n.minFac
rw : n.minFac % 2 = 0
rw₁ : k.succ % 2 = 0
rw₂ : (k + 1) % 2 = 0
rw₃ : (k % 2 + HMod.hMod (α := ℕ) 1 2) % 2 = 0
rw₄ rw₅ : (1 + HMod.hMod (α := ℕ) 1 2) % 2 = 0
⊢ 2 ∣ n.minFac

Tactic:
rw [Nat.dvd_iff_mod_eq_zero, ← h2, succ_eq_add_one, add_mod, h.2.1]

Premises used: Nat.succ_eq_add_one, And.right, And.left, Nat.dvd_iff_mod_eq_zero, Nat.add_mod
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
h2_1 : k < n.minFac
h2 : k.succ = n.minFac
⊢ 2 ∣ n.minFac

Tactic:
have h3 : 2 ∣ minFac n := by
      rw [Nat.dvd_iff_mod_eq_zero, ← h2, succ_eq_add_one, add_mod, h.2.1]
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
h2_1 : k < n.minFac
h2 : k.succ = n.minFac
h3 : 2 ∣ n.minFac
⊢ 2 = n.minFac

Tactic:
simpa [dvd_prime <| minFac_prime h.one_lt.ne'] using h3

Premises used: Nat.dvd_prime, LT.lt.ne', Nat.minFac_prime, Mathlib.Meta.NormNum.MinFacHelper.one_lt
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
h2_1 : k < n.minFac
h2 : k.succ < n.minFac
⊢ k + 2 ≤ n.minFac

Tactic:
h2

Premises used: Nat.lt
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
h2_1 : k < n.minFac
h2 : k.succ < n.minFac
⊢ k + 2 ≤ n.minFac

Tactic:
exact h2
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k k' : ℕ
e : k + 2 = k'
nk : ¬Nat.Prime k
h : MinFacHelper n k
⊢ MinFacHelper n k'

Tactic:
minFacHelper_1 e h fun h2 ↦ ?_

Premises used: Mathlib.Meta.NormNum.minFacHelper_1
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k k' : ℕ
e : k + 2 = k'
nk : ¬Nat.Prime k
h : MinFacHelper n k
refine : ∀ (h2 : n.minFac = k), False
⊢ MinFacHelper n k'

Tactic:
refine minFacHelper_1 e h fun h2 ↦ ?_

Premises used: Mathlib.Meta.NormNum.minFacHelper_1
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k k' : ℕ
e : k + 2 = k'
nk : ¬Nat.Prime k
h : MinFacHelper n k
h2 : n.minFac = k
⊢ ¬Nat.Prime n.minFac

Tactic:
rw [← h2] at nk
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k k' : ℕ
e : k + 2 = k'
nk : ¬Nat.Prime k
h : MinFacHelper n k
h2 : n.minFac = k
nk₁ : ¬Nat.Prime n.minFac
⊢ MinFacHelper n k

Tactic:
rw [← h2] at nk
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k k' : ℕ
e : k + 2 = k'
nk : ¬Nat.Prime k
h : MinFacHelper n k
h2 : n.minFac = k
nk₁ : ¬Nat.Prime n.minFac
h₁ : MinFacHelper n k
⊢ n.minFac = k

Tactic:
rw [← h2] at nk
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k k' : ℕ
e : k + 2 = k'
nk : ¬Nat.Prime n.minFac
h : MinFacHelper n k
h2 : n.minFac = k
⊢ False

Tactic:
nk <| minFac_prime h.one_lt.ne'

Premises used: LT.lt.ne', Nat.minFac_prime, Mathlib.Meta.NormNum.MinFacHelper.one_lt
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k k' : ℕ
e : k + 2 = k'
nk : ¬Nat.Prime n.minFac
h : MinFacHelper n k
h2 : n.minFac = k
⊢ False

Tactic:
exact nk <| minFac_prime h.one_lt.ne'

Premises used: LT.lt.ne', Nat.minFac_prime, Mathlib.Meta.NormNum.MinFacHelper.one_lt
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k k' : ℕ
e : k + 2 = k'
nk : (n % k).beq 0 = false
h : MinFacHelper n k
⊢ MinFacHelper n k'

Tactic:
minFacHelper_1 e h fun h2 ↦ ?_

Premises used: Mathlib.Meta.NormNum.minFacHelper_1
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k k' : ℕ
e : k + 2 = k'
nk : (n % k).beq 0 = false
h : MinFacHelper n k
refine : ∀ (h2 : n.minFac = k), False
⊢ MinFacHelper n k'

Tactic:
refine minFacHelper_1 e h fun h2 ↦ ?_

Premises used: Mathlib.Meta.NormNum.minFacHelper_1
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k k' : ℕ
e : k + 2 = k'
nk : (n % k).beq 0 = false
h : MinFacHelper n k
h2 : n.minFac = k
⊢ ¬n % k = 0

Tactic:
have nk := Nat.ne_of_beq_eq_false nk
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k k' : ℕ
e : k + 2 = k'
nk_1 : (n % k).beq 0 = false
h : MinFacHelper n k
h2 : n.minFac = k
nk : ¬n % k = 0
⊢ ¬n.minFac ∣ n

Tactic:
rw [← Nat.dvd_iff_mod_eq_zero, ← h2] at nk

Premises used: Nat.dvd_iff_mod_eq_zero
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k k' : ℕ
e : k + 2 = k'
nk_1 : (n % k).beq 0 = false
h : MinFacHelper n k
h2 : n.minFac = k
nk : ¬n.minFac ∣ n
⊢ False

Tactic:
nk <| minFac_dvd n

Premises used: Nat.minFac_dvd
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k k' : ℕ
e : k + 2 = k'
nk_1 : (n % k).beq 0 = false
h : MinFacHelper n k
h2 : n.minFac = k
nk : ¬n.minFac ∣ n
⊢ False

Tactic:
exact nk <| minFac_dvd n

Premises used: Nat.minFac_dvd
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
a : ℕ
h : a % 2 = 0
rw : a.minFac = 2
rw₁ : 2 ∣ a
rw₂ : a % 2 = 0
rw₃ rw₄ : Eq (α := ℕ) 0 0
⊢ a.minFac = (↑2 : ℕ)

Tactic:
rw [cast_ofNat, minFac_eq_two_iff, Nat.dvd_iff_mod_eq_zero, h]

Premises used: Nat.cast_ofNat, Nat.minFac_eq_two_iff, Nat.dvd_iff_mod_eq_zero
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k : ℕ
h1 : MinFacHelper n k
h2 : 0 = n % k
⊢ k ∣ n

Tactic:
rw [eq_comm, ← Nat.dvd_iff_mod_eq_zero] at h2

Premises used: eq_comm, Nat.dvd_iff_mod_eq_zero
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k : ℕ
h1 : MinFacHelper n k
h2 : k ∣ n
⊢ IsNat n.minFac k

Tactic:
⟨le_antisymm (minFac_le_of_dvd h1.1.le h2) h1.2.2⟩

Premises used: Nat.minFac_le_of_dvd, Mathlib.Meta.NormNum.IsNat.mk, LT.lt.le, le_antisymm, And.right, And.left
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k : ℕ
h1 : MinFacHelper n k
h2 : k ∣ n
⊢ IsNat n.minFac k

Tactic:
exact ⟨le_antisymm (minFac_le_of_dvd h1.1.le h2) h1.2.2⟩
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k : ℕ
h1 : MinFacHelper n k
h2 : (k * k).ble n = false
⊢ IsNat n.minFac n

Tactic:
⟨(Nat.prime_def_minFac.mp ?_).2⟩

Premises used: Mathlib.Meta.NormNum.IsNat.mk, And.right, Iff.mp, Nat.prime_def_minFac
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k : ℕ
h1 : MinFacHelper n k
h2 : (k * k).ble n = false
refine : Nat.Prime n
⊢ IsNat n.minFac n

Tactic:
refine ⟨(Nat.prime_def_minFac.mp ?_).2⟩
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k : ℕ
h1 : MinFacHelper n k
h2 : (k * k).ble n = false
rw : 2 ≤ n ∧ ∀ (m : ℕ), 2 ≤ m → m ≤ n.sqrt → ¬m ∣ n
⊢ Nat.Prime n

Tactic:
rw [Nat.prime_def_le_sqrt]

Premises used: Nat.prime_def_le_sqrt
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k : ℕ
h1 : MinFacHelper n k
h2 : (k * k).ble n = false
⊢ 2 ≤ n ∧ ∀ (m : ℕ), 2 ≤ m → m ≤ n.sqrt → ¬m ∣ n

Tactic:
⟨h1.one_lt, fun m hm hmn h2mn ↦ ?_⟩

Premises used: And.intro, Mathlib.Meta.NormNum.MinFacHelper.one_lt
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k : ℕ
h1 : MinFacHelper n k
h2 : (k * k).ble n = false
refine : ∀ (m : ℕ) (hm : 2 ≤ m) (hmn : m ≤ n.sqrt) (h2mn : m ∣ n), False
⊢ 2 ≤ n ∧ ∀ (m : ℕ), 2 ≤ m → m ≤ n.sqrt → ¬m ∣ n

Tactic:
refine ⟨h1.one_lt, fun m hm hmn h2mn ↦ ?_⟩
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k : ℕ
h1 : MinFacHelper n k
h2 : (k * k).ble n = false
m : ℕ
hm : 2 ≤ m
hmn : m ≤ n.sqrt
h2mn : m ∣ n
⊢ False

Tactic:
lt_irrefl m <| calc
      m ≤ sqrt n   := hmn
      _ < k        := sqrt_lt.mpr (ble_eq_false.mp h2)
      _ ≤ n.minFac := h1.2.2
      _ ≤ m        := Nat.minFac_le_of_dvd hm h2mn

Premises used: Iff.mpr, Nat.sqrt_lt, Trans.trans, lt_irrefl, Mathlib.Meta.NormNum.ble_eq_false, Nat.minFac_le_of_dvd, And.right, Iff.mp
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n k : ℕ
h1 : MinFacHelper n k
h2 : (k * k).ble n = false
m : ℕ
hm : 2 ≤ m
hmn : m ≤ n.sqrt
h2mn : m ∣ n
⊢ False

Tactic:
exact lt_irrefl m <| calc
      m ≤ sqrt n   := hmn
      _ < k        := sqrt_lt.mpr (ble_eq_false.mp h2)
      _ ≤ n.minFac := h1.2.2
      _ ≤ m        := Nat.minFac_le_of_dvd hm h2mn

Premises used: Iff.mpr, Nat.sqrt_lt, lt_irrefl, Mathlib.Meta.NormNum.ble_eq_false, Nat.minFac_le_of_dvd, Nat.minFac, Nat.sqrt, And.right, Iff.mp
-- Module: Mathlib.Tactic.NormNum.Prime
Goal:
n n' : ℕ
h : IsNat n n'
⊢ ¬Nat.Prime n' → ¬Nat.Prime n

Tactic:
isNat.natElim h

Premises used: Mathlib.Meta.NormNum.isNat.natElim
-- Module: Mathlib.Tactic.NormNum.RealSqrt
Goal:
x : ℝ
nx ny : ℕ
h : IsNat x nx
hy : ny * ny = nx
⊢ √x = (↑ny : ℝ)

Tactic:
simp [h.out, ← hy]

Premises used: Mathlib.Meta.NormNum.IsNat.out
-- Module: Mathlib.Tactic.NormNum.RealSqrt
Goal:
x : ℝ≥0
nx ny : ℕ
h : IsNat x nx
hy : ny * ny = nx
⊢ Eq (α := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) ((↑ny : ℝ≥0) : ℝ≥0)

Tactic:
simp [h.out, ← hy]

Premises used: Mathlib.Meta.NormNum.IsNat.out
-- Module: Mathlib.Tactic.NormNum.RealSqrt
Goal:
x : ℝ≥0
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
h : IsNNRat x n d
obtain :
  ∀ (inv : Invertible (α := ℝ≥0) (↑d : ℝ≥0)),
    IsNNRat (α := ℝ≥0)
      ((sqrt : (a : ℝ≥0) → ℝ≥0)
          (HMul.hMul (α := ℝ≥0) (↑n : ℝ≥0) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ≥0) _)) :
        ℝ≥0)
      sn sd
⊢ IsNNRat (α := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) sn sd

Tactic:
obtain ⟨_, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Tactic.NormNum.RealSqrt
Goal:
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv : Invertible (α := ℝ≥0) (↑d : ℝ≥0)
⊢ IsNNRat (α := ℝ≥0)
    ((sqrt : (a : ℝ≥0) → ℝ≥0)
        (HMul.hMul (α := ℝ≥0) (↑n : ℝ≥0) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ≥0) _)) :
      ℝ≥0)
    sn sd

Tactic:
⟨?_, ?out⟩

Premises used: Mathlib.Meta.NormNum.IsNNRat.mk
-- Module: Mathlib.Tactic.NormNum.RealSqrt
Goal:
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv : Invertible (α := ℝ≥0) (↑d : ℝ≥0)
refine : Invertible (α := ℝ≥0) (↑sd : ℝ≥0)
out :
  (sqrt : (a : ℝ≥0) → ℝ≥0)
      (HMul.hMul (α := ℝ≥0) (↑n : ℝ≥0) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ≥0) _)) =
    HMul.hMul (α := ℝ≥0) (↑sn : ℝ≥0) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑sd : ℝ≥0) _)
⊢ IsNNRat (α := ℝ≥0)
    ((sqrt : (a : ℝ≥0) → ℝ≥0)
        (HMul.hMul (α := ℝ≥0) (↑n : ℝ≥0) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ≥0) _)) :
      ℝ≥0)
    sn sd

Tactic:
refine ⟨?_, ?out⟩
-- Module: Mathlib.Tactic.NormNum.RealSqrt
Goal:
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv : Invertible (α := ℝ≥0) (↑d : ℝ≥0)
h : Ne (α := ℝ≥0) (↑sd : ℝ≥0) 0
⊢ Invertible (α := ℝ≥0) (↑sd : ℝ≥0)

Tactic:
apply invertibleOfNonzero

Premises used: invertibleOfNonzero
-- Module: Mathlib.Tactic.NormNum.RealSqrt
Goal:
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv : Invertible (α := ℝ≥0) (↑d : ℝ≥0)
h : Ne (α := ℝ≥0) (↑d : ℝ≥0) 0
⊢ Ne (α := ℝ≥0) (↑sd : ℝ≥0) 0

Tactic:
rw [← mul_self_ne_zero, ← Nat.cast_mul, hd]

Premises used: Nat.cast_mul, mul_self_ne_zero
-- Module: Mathlib.Tactic.NormNum.RealSqrt
Goal:
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv : Invertible (α := ℝ≥0) (↑d : ℝ≥0)
⊢ Ne (α := ℝ≥0) (↑d : ℝ≥0) 0

Tactic:
Invertible.ne_zero _

Premises used: Invertible.ne_zero
-- Module: Mathlib.Tactic.NormNum.RealSqrt
Goal:
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv : Invertible (α := ℝ≥0) (↑d : ℝ≥0)
⊢ Ne (α := ℝ≥0) (↑d : ℝ≥0) 0

Tactic:
exact Invertible.ne_zero _

Premises used: Invertible.ne_zero
-- Module: Mathlib.Tactic.NormNum.RealSqrt
Goal:
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv : Invertible (α := ℝ≥0) (↑d : ℝ≥0)
⊢ (sqrt : (a : ℝ≥0) → ℝ≥0)
      (HMul.hMul (α := ℝ≥0) (↑n : ℝ≥0) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ≥0) _)) =
    HMul.hMul (α := ℝ≥0) (↑sn : ℝ≥0) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑sd : ℝ≥0) _)

Tactic:
simp [← hn, ← hd, NNReal.sqrt_mul]

Premises used: NNReal.sqrt_mul
-- Module: Mathlib.Tactic.NormNum.RealSqrt
Goal:
x : ℝ
nx : ℕ
h : IsInt x (Int.negOfNat nx)
⊢ √x = (↑0 : ℝ)

Tactic:
simp [Real.sqrt_eq_zero', h.out]

Premises used: Real.sqrt_eq_zero', Mathlib.Meta.NormNum.IsInt.out
-- Module: Mathlib.Tactic.NormNum.RealSqrt
Goal:
x : ℝ
num denom : ℕ
h : IsRat x (Int.negOfNat num) denom
⊢ IsNat (√x) 0

Tactic:
⟨?_⟩

Premises used: Mathlib.Meta.NormNum.IsNat.mk
-- Module: Mathlib.Tactic.NormNum.RealSqrt
Goal:
x : ℝ
num denom : ℕ
h : IsRat x (Int.negOfNat num) denom
refine : √x = (↑0 : ℝ)
⊢ IsNat (√x) 0

Tactic:
refine ⟨?_⟩
-- Module: Mathlib.Tactic.NormNum.RealSqrt
Goal:
x : ℝ
num denom : ℕ
h : IsRat x (Int.negOfNat num) denom
obtain :
  ∀ (inv : Invertible (α := ℝ) (↑denom : ℝ)),
    √(HMul.hMul (α := ℝ) (↑(Int.negOfNat num) : ℝ)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : ℝ) _)) =
      (↑0 : ℝ)
⊢ √x = (↑0 : ℝ)

Tactic:
obtain ⟨inv, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Tactic.NormNum.RealSqrt
Goal:
num denom : ℕ
inv : Invertible (α := ℝ) (↑denom : ℝ)
⊢ 0 ≤ HMul.hMul (α := ℝ) (↑(↑num : ℚ) : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : ℝ) _)

Tactic:
have h₁ : 0 ≤ (num : ℚ) * ⅟(denom : ℝ) :=
    mul_nonneg (Nat.cast_nonneg' _) (invOf_nonneg.2 <| Nat.cast_nonneg' _)
-- Module: Mathlib.Tactic.NormNum.RealSqrt
Goal:
num denom : ℕ
inv : Invertible (α := ℝ) (↑denom : ℝ)
h₁ : 0 ≤ HMul.hMul (α := ℝ) (↑(↑num : ℚ) : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : ℝ) _)
⊢ √(HMul.hMul (α := ℝ) (↑(Int.negOfNat num) : ℝ)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : ℝ) _)) =
    (↑0 : ℝ)

Tactic:
simpa [Nat.cast_zero, Real.sqrt_eq_zero', Int.cast_negOfNat, neg_mul, neg_nonpos] using h₁

Premises used: neg_nonpos, neg_mul, Nat.cast_zero, Int.cast_negOfNat, Real.sqrt_eq_zero'
-- Module: Mathlib.Tactic.NormNum.RealSqrt
Goal:
x : ℝ
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
h : IsNNRat x n d
obtain :
  ∀ (inv : Invertible (α := ℝ) (↑d : ℝ)),
    IsNNRat (√(HMul.hMul (α := ℝ) (↑n : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ) _))) sn sd
⊢ IsNNRat (√x) sn sd

Tactic:
obtain ⟨_, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Tactic.NormNum.RealSqrt
Goal:
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv : Invertible (α := ℝ) (↑d : ℝ)
⊢ IsNNRat (√(HMul.hMul (α := ℝ) (↑n : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ) _))) sn sd

Tactic:
⟨?_, ?out⟩

Premises used: Mathlib.Meta.NormNum.IsNNRat.mk
-- Module: Mathlib.Tactic.NormNum.RealSqrt
Goal:
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv : Invertible (α := ℝ) (↑d : ℝ)
refine : Invertible (α := ℝ) (↑sd : ℝ)
out :
  √(HMul.hMul (α := ℝ) (↑n : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ) _)) =
    HMul.hMul (α := ℝ) (↑sn : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑sd : ℝ) _)
⊢ IsNNRat (√(HMul.hMul (α := ℝ) (↑n : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ) _))) sn sd

Tactic:
refine ⟨?_, ?out⟩
-- Module: Mathlib.Tactic.NormNum.RealSqrt
Goal:
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv : Invertible (α := ℝ) (↑d : ℝ)
h : Ne (α := ℝ) (↑sd : ℝ) 0
⊢ Invertible (α := ℝ) (↑sd : ℝ)

Tactic:
apply invertibleOfNonzero

Premises used: invertibleOfNonzero