awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Pow (goal)
Goal:
α : Type u_1
inst : DivisionRing α
a : α
b : ℤ
nb ne : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsInt (a ^ nb)⁻¹ (Int.negOfNat ne)
⊢ IsInt (a ^ b) (Int.negOfNat ne)
have rwa : IsInt (HPow.hPow (β := ℤ) a (↑(Int.negOfNat nb) : ℤ)) (Int.negOfNat ne)
Tactic: rwa [pb.out, Int.cast_negOfNat, zpow_neg, zpow_natCast]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Pow (goal)
Goal:
α : Type u_1
inst : DivisionRing α
a : α
b : ℤ
nb ne : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsInt (a ^ nb)⁻¹ (Int.negOfNat ne)
rwa : IsInt (HPow.hPow (β := ℤ) a (↑(Int.negOfNat nb) : ℤ)) (Int.negOfNat ne)
⊢ IsInt (a ^ b) (Int.negOfNat ne)
have rwa₁ : IsInt (HPow.hPow (β := ℤ) a (-(↑nb : ℤ))) (Int.negOfNat ne)
Tactic: rwa [pb.out, Int.cast_negOfNat, zpow_neg, zpow_natCast]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Pow (goal)
Goal:
α : Type u_1
inst : DivisionRing α
a : α
b : ℤ
nb ne : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsInt (a ^ nb)⁻¹ (Int.negOfNat ne)
rwa : IsInt (HPow.hPow (β := ℤ) a (↑(Int.negOfNat nb) : ℤ)) (Int.negOfNat ne)
rwa₁ : IsInt (HPow.hPow (β := ℤ) a (-(↑nb : ℤ))) (Int.negOfNat ne)
⊢ IsInt (a ^ b) (Int.negOfNat ne)
have rwa₂ : IsInt (HPow.hPow (β := ℤ) a (↑nb : ℤ))⁻¹ (Int.negOfNat ne)
Tactic: rwa [pb.out, Int.cast_negOfNat, zpow_neg, zpow_natCast]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Pow (goal)
Goal:
α : Type u_1
inst : DivisionSemiring α
a : α
b : ℤ
nb num den : ℕ
pb : IsNat b nb
pe' : IsNNRat (a ^ nb) num den
⊢ IsNNRat (a ^ b) num den
have rwa : IsNNRat (HPow.hPow (β := ℤ) a (↑nb : ℤ)) num den
Tactic: rwa [pb.out, zpow_natCast]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Pow (goal)
Goal:
α : Type u_1
inst : DivisionSemiring α
a : α
b : ℤ
nb num den : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsNNRat (a ^ nb)⁻¹ num den
⊢ IsNNRat (a ^ b) num den
have rwa : IsNNRat (HPow.hPow (β := ℤ) a (↑(Int.negOfNat nb) : ℤ)) num den
Tactic: rwa [pb.out, Int.cast_negOfNat, zpow_neg, zpow_natCast]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Pow (goal)
Goal:
α : Type u_1
inst : DivisionSemiring α
a : α
b : ℤ
nb num den : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsNNRat (a ^ nb)⁻¹ num den
rwa : IsNNRat (HPow.hPow (β := ℤ) a (↑(Int.negOfNat nb) : ℤ)) num den
⊢ IsNNRat (a ^ b) num den
have rwa₁ : IsNNRat (HPow.hPow (β := ℤ) a (-(↑nb : ℤ))) num den
Tactic: rwa [pb.out, Int.cast_negOfNat, zpow_neg, zpow_natCast]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Pow (goal)
Goal:
α : Type u_1
inst : DivisionSemiring α
a : α
b : ℤ
nb num den : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsNNRat (a ^ nb)⁻¹ num den
rwa : IsNNRat (HPow.hPow (β := ℤ) a (↑(Int.negOfNat nb) : ℤ)) num den
rwa₁ : IsNNRat (HPow.hPow (β := ℤ) a (-(↑nb : ℤ))) num den
⊢ IsNNRat (a ^ b) num den
have rwa₂ : IsNNRat (HPow.hPow (β := ℤ) a (↑nb : ℤ))⁻¹ num den
Tactic: rwa [pb.out, Int.cast_negOfNat, zpow_neg, zpow_natCast]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Pow (goal)
Goal:
α : Type u_1
inst : DivisionRing α
a : α
b : ℤ
nb : ℕ
num : ℤ
den : ℕ
pb : IsNat b nb
pe' : IsRat (a ^ nb) num den
⊢ IsRat (a ^ b) num den
have rwa : IsRat (HPow.hPow (β := ℤ) a (↑nb : ℤ)) num den
Tactic: rwa [pb.out, zpow_natCast]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Pow (goal)
Goal:
α : Type u_1
inst : DivisionRing α
a : α
b : ℤ
nb : ℕ
num : ℤ
den : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsRat (a ^ nb)⁻¹ num den
⊢ IsRat (a ^ b) num den
have rwa : IsRat (HPow.hPow (β := ℤ) a (↑(Int.negOfNat nb) : ℤ)) num den
Tactic: rwa [pb.out, Int.cast_negOfNat, zpow_neg, zpow_natCast]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Pow (goal)
Goal:
α : Type u_1
inst : DivisionRing α
a : α
b : ℤ
nb : ℕ
num : ℤ
den : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsRat (a ^ nb)⁻¹ num den
rwa : IsRat (HPow.hPow (β := ℤ) a (↑(Int.negOfNat nb) : ℤ)) num den
⊢ IsRat (a ^ b) num den
have rwa₁ : IsRat (HPow.hPow (β := ℤ) a (-(↑nb : ℤ))) num den
Tactic: rwa [pb.out, Int.cast_negOfNat, zpow_neg, zpow_natCast]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Pow (goal)
Goal:
α : Type u_1
inst : DivisionRing α
a : α
b : ℤ
nb : ℕ
num : ℤ
den : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsRat (a ^ nb)⁻¹ num den
rwa : IsRat (HPow.hPow (β := ℤ) a (↑(Int.negOfNat nb) : ℤ)) num den
rwa₁ : IsRat (HPow.hPow (β := ℤ) a (-(↑nb : ℤ))) num den
⊢ IsRat (a ^ b) num den
have rwa₂ : IsRat (HPow.hPow (β := ℤ) a (↑nb : ℤ))⁻¹ num den
Tactic: rwa [pb.out, Int.cast_negOfNat, zpow_neg, zpow_natCast]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.PowMod (goal)
Goal:
a b m c : ℕ
h1 : (a.pow b).mod m = c
⊢ (a.pow (2 * b)).mod m = (c.mul c).mod m
have simp : (a ^ b * a ^ b).mod m = ((a ^ b).mod m * (a ^ b).mod m).mod m
Tactic: simp only [two_mul, Nat.pow_eq, pow_add, ← h1, Nat.mul_eq]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.PowMod (goal)
Goal:
a m : ℕ
⊢ (a.pow 1).mod m = a.mod m
have rw : a.mod m = a.mod m
Tactic: rw [natPow_one]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.PowMod (goal)
Goal:
a b m : ℕ
⊢ a ^ (2 * b + 1) % m = a ^ b % m * (a ^ b % m * a % m) % m
have rw : a ^ (2 * b) * HPow.hPow (β := ℕ) a 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]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.PowMod (goal)
Goal:
a b m : ℕ
rw : a ^ (2 * b) * HPow.hPow (β := ℕ) a 1 % m = a ^ b % m * (a ^ b % m * a % m) % m
⊢ a ^ (2 * b + 1) % m = a ^ b % m * (a ^ b % m * a % m) % m
have rw₁ : a ^ (b + b) * HPow.hPow (β := ℕ) a 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]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.PowMod (goal)
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
⊢ a ^ (2 * b + 1) % m = a ^ b % m * (a ^ b % m * a % m) % m
have rw₂ : a ^ b * a ^ b * HPow.hPow (β := ℕ) a 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]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.PowMod (goal)
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
⊢ a ^ (2 * b + 1) % m = a ^ b % m * (a ^ b % m * a % m) % m
have rw₃ : a ^ b * a ^ b * a % 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]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.PowMod (goal)
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
⊢ a ^ (2 * b + 1) % m = a ^ b % m * (a ^ b % m * a % m) % m
have rw₄ : a ^ b * a ^ b * a % m = a ^ b % m * (a ^ b % m % m * (a % m) % 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]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.PowMod (goal)
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
⊢ a ^ (2 * b + 1) % m = a ^ b % m * (a ^ b % m * a % m) % m
have rw₅ : a ^ b * a ^ b * a % m = a ^ b % m * (a ^ b % m * (a % m) % 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]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.PowMod (goal)
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
⊢ a ^ (2 * b + 1) % m = a ^ b % m * (a ^ b % m * a % m) % m
have rw₆ : a ^ b * a ^ b * a % m = a ^ b % m * (a ^ b * 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]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.PowMod (goal)
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
⊢ a ^ (2 * b + 1) % m = a ^ b % m * (a ^ b % m * a % m) % m
have rw₇ : a ^ b * a ^ b * a % m = a ^ b * (a ^ b * a) % 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]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.PowMod (goal)
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
⊢ a ^ (2 * b + 1) % m = a ^ b % m * (a ^ b % m * a % m) % m
have rw₈ : a ^ b * (a ^ b * a) % m = a ^ b * (a ^ b * a) % 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]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Prime (hypothesis)
Goal:
n k : ℕ
h : MinFacHelper n k
⊢ 1 < n
have this : 2 < n.minFac
Tactic: have : 2 < minFac n := h.1.trans_le h.2.2
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Prime (goal)
Goal:
n k : ℕ
h : MinFacHelper n k
this : 2 < n.minFac
⊢ 1 < n
have inl : ∀ (h : MinFacHelper 0 k) (this : 2 < minFac 0), LT.lt (α := ℕ) 1 0
Tactic: obtain rfl | h := n.eq_zero_or_pos
Cleared hypotheses: n, h, this
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Prime (goal)
Goal:
n k : ℕ
h : MinFacHelper n k
this : 2 < n.minFac
inl : ∀ (h : MinFacHelper 0 k) (this : 2 < minFac 0), LT.lt (α := ℕ) 1 0
⊢ 1 < n
have inr : ∀ (h : n > 0), 1 < n
Tactic: obtain rfl | h := n.eq_zero_or_pos
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Prime (goal)
Goal:
n k : ℕ
h_1 : MinFacHelper n k
this : 2 < n.minFac
h : n > 0
⊢ 1 < n
have inr : ∀ (h : MinFacHelper (succ 0) k) (this : 2 < (succ 0).minFac) (h : succ 0 > 0), 1 < succ 0
Tactic: rcases (succ_le_of_lt h).eq_or_lt with rfl | h
Cleared hypotheses: n, h_1, this, h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Prime (goal)
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
⊢ 1 < n
have inr₁ : ∀ (h : succ 0 < n), 1 < n
Tactic: rcases (succ_le_of_lt h).eq_or_lt with rfl | h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Prime (goal)
Goal:
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
⊢ MinFacHelper n 3
have refine : 3 ≤ n.minFac
Tactic: refine ⟨by simp, by simp, ?_⟩
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Prime (goal)
Goal:
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
⊢ 3 ≤ n.minFac
have refine : ∀ (p : ℕ) (hp : 2 ≤ p) (hpn : p ∣ n), 3 ≤ p
Tactic: refine (le_minFac'.mpr fun p hp hpn ↦ ?_).resolve_left (Nat.ne_of_gt (Nat.le_of_ble_eq_true h1))
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Prime (goal)
Goal:
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
p : ℕ
hp : 2 ≤ p
hpn : p ∣ n
⊢ 3 ≤ p
have inl : ∀ (hp : LE.le (α := ℕ) 2 2) (hpn : 2 ∣ n), 3 ≤ 2
Tactic: rcases hp.eq_or_lt with rfl | h
Cleared hypotheses: p, hp, hpn
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Prime (goal)
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
⊢ 3 ≤ p
have inr : ∀ (h : 2 < p), 3 ≤ p
Tactic: rcases hp.eq_or_lt with rfl | h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Prime (goal)
Goal:
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
⊢ MinFacHelper n k'
have rw : MinFacHelper n (k + 2)
Tactic: rw [← e]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Prime (goal)
Goal:
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
⊢ MinFacHelper n (k + 2)
have refine_1 : (k + 2) % 2 = 1
Tactic: refine ⟨Nat.lt_add_right _ h.1, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Prime (goal)
Goal:
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
refine_1 : (k + 2) % 2 = 1
⊢ MinFacHelper n (k + 2)
have refine_2 : k + 2 ≤ n.minFac
Tactic: refine ⟨Nat.lt_add_right _ h.1, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Prime (goal)
Goal:
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
⊢ (k + 2) % 2 = 1
have refine_1 : k % 2 = 1
Tactic: rw [add_mod, mod_self, add_zero, mod_mod]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Prime (goal)
Goal:
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
⊢ k + 2 ≤ n.minFac
have refine_2 : ∀ (e : n.minFac + 2 = k') (h : MinFacHelper n n.minFac) (np : n.minFac ≠ n.minFac), n.minFac + 2 ≤ n.minFac
Tactic: rcases h.2.2.eq_or_lt with rfl | h2
Cleared hypotheses: k, e, h, np
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Prime (goal)
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
⊢ k + 2 ≤ n.minFac
have refine_2₁ : ∀ (h2 : k < n.minFac), k + 2 ≤ n.minFac
Tactic: rcases h.2.2.eq_or_lt with rfl | h2
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Prime (goal)
Goal:
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
h2 : k < n.minFac
⊢ k + 2 ≤ n.minFac
have refine_2 : ∀ (h2 : k.succ = n.minFac), k + 2 ≤ n.minFac
Tactic: rcases (succ_le_of_lt h2).eq_or_lt with h2|h2
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Prime (goal)
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
⊢ k + 2 ≤ n.minFac
have refine_2₁ : ∀ (h2 : k.succ < n.minFac), k + 2 ≤ n.minFac
Tactic: rcases (succ_le_of_lt h2).eq_or_lt with h2|h2
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Prime (goal)
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
have refine_2 : 2 = n.minFac
Tactic: refine ((h.1.trans_le h.2.2).ne ?_).elim
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Prime (goal)
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
have rw : n.minFac % 2 = 0
Tactic: rw [Nat.dvd_iff_mod_eq_zero, ← h2, succ_eq_add_one, add_mod, h.2.1]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Prime (goal)
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
⊢ 2 ∣ n.minFac
have rw₁ : k.succ % 2 = 0
Tactic: rw [Nat.dvd_iff_mod_eq_zero, ← h2, succ_eq_add_one, add_mod, h.2.1]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Prime (goal)
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
⊢ 2 ∣ n.minFac
have rw₃ : (k % 2 + HMod.hMod (α := ℕ) 1 2) % 2 = 0
Tactic: rw [Nat.dvd_iff_mod_eq_zero, ← h2, succ_eq_add_one, add_mod, h.2.1]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Prime (goal)
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
⊢ 2 ∣ n.minFac
have rw₄ : (1 + HMod.hMod (α := ℕ) 1 2) % 2 = 0
Tactic: rw [Nat.dvd_iff_mod_eq_zero, ← h2, succ_eq_add_one, add_mod, h.2.1]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Prime (hypothesis)
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
have h3 : 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]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Prime (goal)
Goal:
n k k' : ℕ
e : k + 2 = k'
nk : ¬Nat.Prime k
h : MinFacHelper n k
⊢ MinFacHelper n k'
have refine : ∀ (h2 : n.minFac = k), False
Tactic: refine minFacHelper_1 e h fun h2 ↦ ?_
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Prime (hypothesis)
Goal:
n k k' : ℕ
e : k + 2 = k'
nk : ¬Nat.Prime k
h : MinFacHelper n k
h2 : n.minFac = k
⊢ False
have nk₁ : ¬Nat.Prime n.minFac
Tactic: rw [← h2] at nk
Cleared hypotheses: nk, h, h2
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Prime (goal)
Goal:
n k k' : ℕ
e : k + 2 = k'
nk : (n % k).beq 0 = false
h : MinFacHelper n k
⊢ MinFacHelper n k'
have refine : ∀ (h2 : n.minFac = k), False
Tactic: refine minFacHelper_1 e h fun h2 ↦ ?_
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Prime (hypothesis)
Goal:
n k k' : ℕ
e : k + 2 = k'
nk : (n % k).beq 0 = false
h : MinFacHelper n k
h2 : n.minFac = k
⊢ False
have nk₁ : ¬n % k = 0
Tactic: have nk := Nat.ne_of_beq_eq_false nk
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Prime (hypothesis)
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
⊢ False
have nk₁ : ¬n.minFac ∣ n
Tactic: rw [← Nat.dvd_iff_mod_eq_zero, ← h2] at nk
Cleared hypotheses: nk
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Prime (goal)
Goal:
a : ℕ
h : a % 2 = 0
⊢ a.minFac = (↑2 : ℕ)
have rw : a.minFac = 2
Tactic: rw [cast_ofNat, minFac_eq_two_iff, Nat.dvd_iff_mod_eq_zero, h]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Prime (goal)
Goal:
a : ℕ
h : a % 2 = 0
rw : a.minFac = 2
⊢ a.minFac = (↑2 : ℕ)
have rw₁ : 2 ∣ a
Tactic: rw [cast_ofNat, minFac_eq_two_iff, Nat.dvd_iff_mod_eq_zero, h]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Prime (goal)
Goal:
a : ℕ
h : a % 2 = 0
rw : a.minFac = 2
rw₁ : 2 ∣ a
rw₂ : a % 2 = 0
⊢ a.minFac = (↑2 : ℕ)
have rw₃ : Eq (α := ℕ) 0 0
Tactic: rw [cast_ofNat, minFac_eq_two_iff, Nat.dvd_iff_mod_eq_zero, h]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Prime (hypothesis)
Goal:
n k : ℕ
h1 : MinFacHelper n k
h2 : 0 = n % k
⊢ IsNat n.minFac k
have h2₁ : k ∣ n
Tactic: rw [eq_comm, ← Nat.dvd_iff_mod_eq_zero] at h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Prime (goal)
Goal:
n k : ℕ
h1 : MinFacHelper n k
h2 : (k * k).ble n = false
⊢ IsNat n.minFac n
have refine : Nat.Prime n
Tactic: refine ⟨(Nat.prime_def_minFac.mp ?_).2⟩
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Prime (goal)
Goal:
n k : ℕ
h1 : MinFacHelper n k
h2 : (k * k).ble n = false
⊢ Nat.Prime n
have rw : 2 ≤ n ∧ ∀ (m : ℕ), 2 ≤ m → m ≤ n.sqrt → ¬m ∣ n
Tactic: rw [Nat.prime_def_le_sqrt]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Prime (goal)
Goal:
n k : ℕ
h1 : MinFacHelper n k
h2 : (k * k).ble n = false
⊢ 2 ≤ n ∧ ∀ (m : ℕ), 2 ≤ m → m ≤ n.sqrt → ¬m ∣ n
have refine : ∀ (m : ℕ) (hm : 2 ≤ m) (hmn : m ≤ n.sqrt) (h2mn : m ∣ n), False
Tactic: refine ⟨h1.one_lt, fun m hm hmn h2mn ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Tactic.NormNum.RealSqrt (goal)
Goal:
x : ℝ≥0
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
h : IsNNRat x n d
⊢ IsNNRat (α := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) sn sd
have 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
Tactic: obtain ⟨_, rfl⟩ := h
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.RealSqrt (goal)
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
have refine : Invertible (α := ℝ≥0) (↑sd : ℝ≥0)
Tactic: refine ⟨?_, ?out⟩
-- Lean 4 proof step from Mathlib.Tactic.NormNum.RealSqrt (goal)
Goal:
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv : Invertible (α := ℝ≥0) (↑d : ℝ≥0)
refine : Invertible (α := ℝ≥0) (↑sd : ℝ≥0)
⊢ IsNNRat (α := ℝ≥0)
    ((sqrt : (a : ℝ≥0) → ℝ≥0)
        (HMul.hMul (α := ℝ≥0) (↑n : ℝ≥0) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ≥0) _)) :
      ℝ≥0)
    sn sd
have 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) _)
Tactic: refine ⟨?_, ?out⟩
-- Lean 4 proof step from Mathlib.Tactic.NormNum.RealSqrt (goal)
Goal:
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv : Invertible (α := ℝ≥0) (↑d : ℝ≥0)
⊢ Invertible (α := ℝ≥0) (↑sd : ℝ≥0)
have h : Ne (α := ℝ≥0) (↑sd : ℝ≥0) 0
Tactic: apply invertibleOfNonzero
-- Lean 4 proof step from Mathlib.Tactic.NormNum.RealSqrt (goal)
Goal:
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv : Invertible (α := ℝ≥0) (↑d : ℝ≥0)
⊢ Ne (α := ℝ≥0) (↑sd : ℝ≥0) 0
have h : Ne (α := ℝ≥0) (↑d : ℝ≥0) 0
Tactic: rw [← mul_self_ne_zero, ← Nat.cast_mul, hd]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.RealSqrt (goal)
Goal:
x : ℝ
num denom : ℕ
h : IsRat x (Int.negOfNat num) denom
⊢ IsNat (√x) 0
have refine : √x = (↑0 : ℝ)
Tactic: refine ⟨?_⟩
-- Lean 4 proof step from Mathlib.Tactic.NormNum.RealSqrt (goal)
Goal:
x : ℝ
num denom : ℕ
h : IsRat x (Int.negOfNat num) denom
⊢ √x = (↑0 : ℝ)
have obtain : ∀ (inv : Invertible (α := ℝ) (↑denom : ℝ)),
  √(HMul.hMul (α := ℝ) (↑(Int.negOfNat num) : ℝ)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : ℝ) _)) =
    (↑0 : ℝ)
Tactic: obtain ⟨inv, rfl⟩ := h
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.RealSqrt (hypothesis)
Goal:
num denom : ℕ
inv : Invertible (α := ℝ) (↑denom : ℝ)
⊢ √(HMul.hMul (α := ℝ) (↑(Int.negOfNat num) : ℝ)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : ℝ) _)) =
    (↑0 : ℝ)
have h₁ : 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' _)
-- Lean 4 proof step from Mathlib.Tactic.NormNum.RealSqrt (goal)
Goal:
x : ℝ
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
h : IsNNRat x n d
⊢ IsNNRat (√x) sn sd
have obtain : ∀ (inv : Invertible (α := ℝ) (↑d : ℝ)),
  IsNNRat (√(HMul.hMul (α := ℝ) (↑n : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ) _))) sn sd
Tactic: obtain ⟨_, rfl⟩ := h
Cleared hypotheses: x, h