awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a b : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 4 = 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 hb (Nat.odd_iff.mpr ha)]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a b : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 4 = 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 hb (Nat.odd_iff.mpr ha)]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a b : ℕ
r : ℤ
ha : a % 4 = 3
hb : b % 4 = 3
hr : jacobiSymNat b a = r
⊢ jacobiSymNat a b = -r
have rwa : jacobiSym (↑a : ℤ) b = -r
Tactic: rwa [jacobiSymNat, jacobiSym.quadratic_reciprocity_three_mod_four ha hb, neg_inj]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
Goal:
a b : ℕ
r : ℤ
ha : a % 4 = 3
hb : b % 4 = 3
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_three_mod_four ha hb, neg_inj]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.LegendreSymbol (goal)
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
⊢ jacobiSymNat a b = -r
have rwa₂ : jacobiSym (↑b : ℤ) a = r
Tactic: rwa [jacobiSymNat, jacobiSym.quadratic_reciprocity_three_mod_four ha hb, neg_inj]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.NatFactorial (goal)
Goal:
n l m a b : ℕ
h₁ : n.ascFactorial l = a
h₂ : (n + l).ascFactorial m = b
⊢ n.ascFactorial (l + m) = a * b
have rw : n.ascFactorial (l + m) = n.ascFactorial l * (n + l).ascFactorial m
Tactic: rw [← h₁, ← h₂]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.NatFactorial (goal)
Goal:
n l m a b : ℕ
h₁ : n.ascFactorial l = a
h₂ : (n + l).ascFactorial m = b
⊢ n.ascFactorial (l + m) = n.ascFactorial l * (n + l).ascFactorial m
have symm : n.ascFactorial l * (n + l).ascFactorial m = n.ascFactorial (l + m)
Tactic: symm
-- Lean 4 proof step from Mathlib.Tactic.NormNum.NatFactorial (goal)
Goal:
n x : ℕ
h₁ : IsNat n x
a : ℕ
h₂ : ascFactorial 1 x = a
⊢ IsNat n ! a
have out : n ! = (↑a : ℕ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Tactic.NormNum.NatFactorial (goal)
Goal:
n x l y : ℕ
h₁ : IsNat n x
h₂ : IsNat l y
a : ℕ
p : x.ascFactorial y = a
⊢ IsNat (n.ascFactorial l) a
have out : n.ascFactorial l = (↑a : ℕ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Tactic.NormNum.NatFactorial (goal)
Goal:
n x l y z : ℕ
h₁ : IsNat n x
h₂ : IsNat l y
h₃ : x = z + y
a : ℕ
p : (z + 1).ascFactorial y = a
⊢ IsNat (n.descFactorial l) a
have out : n.descFactorial l = (↑a : ℕ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Tactic.NormNum.NatFactorial (goal)
Goal:
n x l y z : ℕ
h₁ : IsNat n x
h₂ : IsNat l y
h₃ : y = z + x + 1
⊢ IsNat (n.descFactorial l) 0
have out : n.descFactorial l = (↑0 : ℕ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Tactic.NormNum.NatFib (goal)
Goal:
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n = n'
h1 : a * (2 * b - a) = a'
h2 : a * a + b * b = b'
⊢ fib n' = a'
have rw : fib (2 * n) = a'
Tactic: rw [← hn, fib_two_mul, H.1, H.2, ← h1]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.NatFib (goal)
Goal:
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n = n'
h1 : a * (2 * b - a) = a'
h2 : a * a + b * b = b'
rw : fib (2 * n) = a'
⊢ fib n' = a'
have rw₁ : fib n * (2 * fib (n + 1) - fib n) = a'
Tactic: rw [← hn, fib_two_mul, H.1, H.2, ← h1]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.NatFib (goal)
Goal:
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n = n'
h1 : a * (2 * b - a) = a'
h2 : a * a + b * b = b'
rw : fib (2 * n) = a'
rw₁ : fib n * (2 * fib (n + 1) - fib n) = a'
⊢ fib n' = a'
have rw₂ : a * (2 * fib (n + 1) - a) = a'
Tactic: rw [← hn, fib_two_mul, H.1, H.2, ← h1]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.NatFib (goal)
Goal:
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n = n'
h1 : a * (2 * b - a) = a'
h2 : a * a + b * b = b'
rw : fib (2 * n) = a'
rw₁ : fib n * (2 * fib (n + 1) - fib n) = a'
rw₂ : a * (2 * fib (n + 1) - a) = a'
rw₃ : a * (2 * b - a) = a'
⊢ fib n' = a'
have rw₄ : a * (2 * b - a) = a * (2 * b - a)
Tactic: rw [← hn, fib_two_mul, H.1, H.2, ← h1]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.NatFib (goal)
Goal:
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n = n'
h1 : a * (2 * b - a) = a'
h2 : a * a + b * b = b'
⊢ fib (n' + 1) = b'
have rw : fib (2 * n + 1) = b'
Tactic: rw [← hn, fib_two_mul_add_one, H.1, H.2, pow_two, pow_two, add_comm, h2]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.NatFib (goal)
Goal:
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n = n'
h1 : a * (2 * b - a) = a'
h2 : a * a + b * b = b'
rw : fib (2 * n + 1) = b'
⊢ fib (n' + 1) = b'
have rw₁ : HPow.hPow (β := ℕ) (fib (n + 1)) 2 + HPow.hPow (β := ℕ) (fib n) 2 = b'
Tactic: rw [← hn, fib_two_mul_add_one, H.1, H.2, pow_two, pow_two, add_comm, h2]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.NatFib (goal)
Goal:
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n = n'
h1 : a * (2 * b - a) = a'
h2 : a * a + b * b = b'
rw : fib (2 * n + 1) = b'
rw₁ : HPow.hPow (β := ℕ) (fib (n + 1)) 2 + HPow.hPow (β := ℕ) (fib n) 2 = b'
⊢ fib (n' + 1) = b'
have rw₂ : HPow.hPow (β := ℕ) (fib (n + 1)) 2 + HPow.hPow (β := ℕ) a 2 = b'
Tactic: rw [← hn, fib_two_mul_add_one, H.1, H.2, pow_two, pow_two, add_comm, h2]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.NatFib (goal)
Goal:
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n = n'
h1 : a * (2 * b - a) = a'
h2 : a * a + b * b = b'
rw : fib (2 * n + 1) = b'
rw₁ : HPow.hPow (β := ℕ) (fib (n + 1)) 2 + HPow.hPow (β := ℕ) (fib n) 2 = b'
rw₂ : HPow.hPow (β := ℕ) (fib (n + 1)) 2 + HPow.hPow (β := ℕ) a 2 = b'
⊢ fib (n' + 1) = b'
have rw₃ : HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) a 2 = b'
Tactic: rw [← hn, fib_two_mul_add_one, H.1, H.2, pow_two, pow_two, add_comm, h2]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.NatFib (goal)
Goal:
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n = n'
h1 : a * (2 * b - a) = a'
h2 : a * a + b * b = b'
rw : fib (2 * n + 1) = b'
rw₁ : HPow.hPow (β := ℕ) (fib (n + 1)) 2 + HPow.hPow (β := ℕ) (fib n) 2 = b'
rw₂ : HPow.hPow (β := ℕ) (fib (n + 1)) 2 + HPow.hPow (β := ℕ) a 2 = b'
rw₃ : HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) a 2 = b'
⊢ fib (n' + 1) = b'
have rw₄ : b * b + HPow.hPow (β := ℕ) a 2 = b'
Tactic: rw [← hn, fib_two_mul_add_one, H.1, H.2, pow_two, pow_two, add_comm, h2]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.NatFib (goal)
Goal:
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n = n'
h1 : a * (2 * b - a) = a'
h2 : a * a + b * b = b'
rw : fib (2 * n + 1) = b'
rw₁ : HPow.hPow (β := ℕ) (fib (n + 1)) 2 + HPow.hPow (β := ℕ) (fib n) 2 = b'
rw₂ : HPow.hPow (β := ℕ) (fib (n + 1)) 2 + HPow.hPow (β := ℕ) a 2 = b'
rw₃ : HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) a 2 = b'
rw₄ : b * b + HPow.hPow (β := ℕ) a 2 = b'
⊢ fib (n' + 1) = b'
have rw₅ : b * b + a * a = b'
Tactic: rw [← hn, fib_two_mul_add_one, H.1, H.2, pow_two, pow_two, add_comm, h2]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.NatFib (goal)
Goal:
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n = n'
h1 : a * (2 * b - a) = a'
h2 : a * a + b * b = b'
rw : fib (2 * n + 1) = b'
rw₁ : HPow.hPow (β := ℕ) (fib (n + 1)) 2 + HPow.hPow (β := ℕ) (fib n) 2 = b'
rw₂ : HPow.hPow (β := ℕ) (fib (n + 1)) 2 + HPow.hPow (β := ℕ) a 2 = b'
rw₃ : HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) a 2 = b'
rw₄ : b * b + HPow.hPow (β := ℕ) a 2 = b'
rw₅ : b * b + a * a = b'
rw₆ : a * a + b * b = b'
⊢ fib (n' + 1) = b'
have rw₇ : b' = b'
Tactic: rw [← hn, fib_two_mul_add_one, H.1, H.2, pow_two, pow_two, add_comm, h2]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.NatFib (goal)
Goal:
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n + 1 = n'
h1 : a * a + b * b = a'
h2 : b * (2 * a + b) = b'
⊢ fib n' = a'
have rw : fib (2 * n + 1) = a'
Tactic: rw [← hn, fib_two_mul_add_one, H.1, H.2, pow_two, pow_two, add_comm, h1]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.NatFib (goal)
Goal:
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n + 1 = n'
h1 : a * a + b * b = a'
h2 : b * (2 * a + b) = b'
rw : fib (2 * n + 1) = a'
⊢ fib n' = a'
have rw₁ : HPow.hPow (β := ℕ) (fib (n + 1)) 2 + HPow.hPow (β := ℕ) (fib n) 2 = a'
Tactic: rw [← hn, fib_two_mul_add_one, H.1, H.2, pow_two, pow_two, add_comm, h1]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.NatFib (goal)
Goal:
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n + 1 = n'
h1 : a * a + b * b = a'
h2 : b * (2 * a + b) = b'
rw : fib (2 * n + 1) = a'
rw₁ : HPow.hPow (β := ℕ) (fib (n + 1)) 2 + HPow.hPow (β := ℕ) (fib n) 2 = a'
⊢ fib n' = a'
have rw₂ : HPow.hPow (β := ℕ) (fib (n + 1)) 2 + HPow.hPow (β := ℕ) a 2 = a'
Tactic: rw [← hn, fib_two_mul_add_one, H.1, H.2, pow_two, pow_two, add_comm, h1]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.NatFib (goal)
Goal:
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n + 1 = n'
h1 : a * a + b * b = a'
h2 : b * (2 * a + b) = b'
rw : fib (2 * n + 1) = a'
rw₁ : HPow.hPow (β := ℕ) (fib (n + 1)) 2 + HPow.hPow (β := ℕ) (fib n) 2 = a'
rw₂ : HPow.hPow (β := ℕ) (fib (n + 1)) 2 + HPow.hPow (β := ℕ) a 2 = a'
⊢ fib n' = a'
have rw₃ : HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) a 2 = a'
Tactic: rw [← hn, fib_two_mul_add_one, H.1, H.2, pow_two, pow_two, add_comm, h1]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.NatFib (goal)
Goal:
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n + 1 = n'
h1 : a * a + b * b = a'
h2 : b * (2 * a + b) = b'
rw : fib (2 * n + 1) = a'
rw₁ : HPow.hPow (β := ℕ) (fib (n + 1)) 2 + HPow.hPow (β := ℕ) (fib n) 2 = a'
rw₂ : HPow.hPow (β := ℕ) (fib (n + 1)) 2 + HPow.hPow (β := ℕ) a 2 = a'
rw₃ : HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) a 2 = a'
⊢ fib n' = a'
have rw₄ : b * b + HPow.hPow (β := ℕ) a 2 = a'
Tactic: rw [← hn, fib_two_mul_add_one, H.1, H.2, pow_two, pow_two, add_comm, h1]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.NatFib (goal)
Goal:
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n + 1 = n'
h1 : a * a + b * b = a'
h2 : b * (2 * a + b) = b'
rw : fib (2 * n + 1) = a'
rw₁ : HPow.hPow (β := ℕ) (fib (n + 1)) 2 + HPow.hPow (β := ℕ) (fib n) 2 = a'
rw₂ : HPow.hPow (β := ℕ) (fib (n + 1)) 2 + HPow.hPow (β := ℕ) a 2 = a'
rw₃ : HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) a 2 = a'
rw₄ : b * b + HPow.hPow (β := ℕ) a 2 = a'
⊢ fib n' = a'
have rw₅ : b * b + a * a = a'
Tactic: rw [← hn, fib_two_mul_add_one, H.1, H.2, pow_two, pow_two, add_comm, h1]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.NatFib (goal)
Goal:
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n + 1 = n'
h1 : a * a + b * b = a'
h2 : b * (2 * a + b) = b'
rw : fib (2 * n + 1) = a'
rw₁ : HPow.hPow (β := ℕ) (fib (n + 1)) 2 + HPow.hPow (β := ℕ) (fib n) 2 = a'
rw₂ : HPow.hPow (β := ℕ) (fib (n + 1)) 2 + HPow.hPow (β := ℕ) a 2 = a'
rw₃ : HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) a 2 = a'
rw₄ : b * b + HPow.hPow (β := ℕ) a 2 = a'
rw₅ : b * b + a * a = a'
rw₆ : a * a + b * b = a'
⊢ fib n' = a'
have rw₇ : a' = a'
Tactic: rw [← hn, fib_two_mul_add_one, H.1, H.2, pow_two, pow_two, add_comm, h1]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.NatFib (goal)
Goal:
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n + 1 = n'
h1 : a * a + b * b = a'
h2 : b * (2 * a + b) = b'
⊢ fib (n' + 1) = b'
have rw : fib (2 * n + 1 + 1) = b'
Tactic: rw [← hn, fib_two_mul_add_two, H.1, H.2, h2]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.NatFib (goal)
Goal:
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n + 1 = n'
h1 : a * a + b * b = a'
h2 : b * (2 * a + b) = b'
rw : fib (2 * n + 1 + 1) = b'
⊢ fib (n' + 1) = b'
have rw₁ : fib (n + 1) * (2 * fib n + fib (n + 1)) = b'
Tactic: rw [← hn, fib_two_mul_add_two, H.1, H.2, h2]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.NatFib (goal)
Goal:
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n + 1 = n'
h1 : a * a + b * b = a'
h2 : b * (2 * a + b) = b'
rw : fib (2 * n + 1 + 1) = b'
rw₁ : fib (n + 1) * (2 * fib n + fib (n + 1)) = b'
⊢ fib (n' + 1) = b'
have rw₂ : fib (n + 1) * (2 * a + fib (n + 1)) = b'
Tactic: rw [← hn, fib_two_mul_add_two, H.1, H.2, h2]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.NatFib (goal)
Goal:
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n + 1 = n'
h1 : a * a + b * b = a'
h2 : b * (2 * a + b) = b'
rw : fib (2 * n + 1 + 1) = b'
rw₁ : fib (n + 1) * (2 * fib n + fib (n + 1)) = b'
rw₂ : fib (n + 1) * (2 * a + fib (n + 1)) = b'
rw₃ : b * (2 * a + b) = b'
⊢ fib (n' + 1) = b'
have rw₄ : b' = b'
Tactic: rw [← hn, fib_two_mul_add_two, H.1, H.2, h2]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.NatLog (hypothesis)
Goal:
b n : ℕ
hl : n.blt b = true
⊢ Nat.log b n = 0
have hl₁ : n < b
Tactic: rw [Nat.blt_eq] at hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Tactic.NormNum.NatLog (hypothesis)
Goal:
b m n : ℕ
hb : Nat.blt 1 b = true
h₁ : (b ^ m).blt n = true
h₂ : n.ble (b ^ (m + 1)) = true
⊢ Nat.clog b n = m + 1
have hb₁ : 1 < b
Tactic: rw [Nat.blt_eq] at hb
Cleared hypotheses: hb, h₁, h₂
-- Lean 4 proof step from Mathlib.Tactic.NormNum.NatLog (hypothesis)
Goal:
b m n : ℕ
hb : 1 < b
h₁ : (b ^ m).blt n = true
h₂ : n.ble (b ^ (m + 1)) = true
⊢ Nat.clog b n = m + 1
have h₃ : m < Nat.clog b n
Tactic: rw [Nat.blt_eq, ← Nat.lt_clog_iff_pow_lt hb] at h₁
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Tactic.NormNum.NatLog (hypothesis)
Goal:
b m n : ℕ
hb : 1 < b
h₁ : m < Nat.clog b n
h₂ : n.ble (b ^ (m + 1)) = true
⊢ Nat.clog b n = m + 1
have h₃ : Nat.clog b n ≤ m + 1
Tactic: rw [Nat.ble_eq, ← Nat.clog_le_iff_le_pow hb] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Tactic.NormNum.NatSqrt (goal)
Goal:
x y r : ℕ
hr : y * y + r = x
hle : r.ble (2 * y) = true
⊢ x.sqrt = y
have rw : (HPow.hPow (β := ℕ) y 2 + r).sqrt = y
Tactic: rw [← hr, ← pow_two]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.NatSqrt (hypothesis)
Goal:
x y r : ℕ
hr : y * y + r = x
hle : r.ble (2 * y) = true
⊢ (HPow.hPow (β := ℕ) y 2 + r).sqrt = y
have hle₁ : r.ble (y + y) = true
Tactic: rw [two_mul] at hle
Cleared hypotheses: hle
-- Lean 4 proof step from Mathlib.Tactic.NormNum.OfScientific (goal)
Goal:
α : Type u_1
inst : DivisionRing α
x x_1 num denom : ℕ
inv : Invertible (α := α) (↑denom : α)
eq :
  (↑(mkRat (↑x : ℤ) (HPow.hPow (α := ℕ) 10 x_1)) : α) =
    HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : α) _)
⊢ OfScientific.ofScientific x true x_1 =
    HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : α) _)
have rwa : (↑(OfScientific.ofScientific x true x_1) : α) =
  HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : α) _)
Tactic: rwa [← Rat.cast_ofScientific, ← Rat.ofScientific_eq_ofScientific, Rat.ofScientific_true_def]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.OfScientific (goal)
Goal:
α : Type u_1
inst : DivisionRing α
x x_1 num denom : ℕ
inv : Invertible (α := α) (↑denom : α)
eq :
  (↑(mkRat (↑x : ℤ) (HPow.hPow (α := ℕ) 10 x_1)) : α) =
    HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : α) _)
rwa :
  (↑(OfScientific.ofScientific x true x_1) : α) =
    HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : α) _)
⊢ OfScientific.ofScientific x true x_1 =
    HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : α) _)
have rwa₁ : (↑(Rat.ofScientific (OfNat.ofNat x) true (OfNat.ofNat x_1)) : α) =
  HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : α) _)
Tactic: rwa [← Rat.cast_ofScientific, ← Rat.ofScientific_eq_ofScientific, Rat.ofScientific_true_def]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.OfScientific (goal)
Goal:
α : Type u_1
inst : DivisionRing α
x x_1 num denom : ℕ
inv : Invertible (α := α) (↑denom : α)
eq :
  (↑(mkRat (↑x : ℤ) (HPow.hPow (α := ℕ) 10 x_1)) : α) =
    HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : α) _)
rwa :
  (↑(OfScientific.ofScientific x true x_1) : α) =
    HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : α) _)
rwa₁ :
  (↑(Rat.ofScientific (OfNat.ofNat x) true (OfNat.ofNat x_1)) : α) =
    HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : α) _)
⊢ OfScientific.ofScientific x true x_1 =
    HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : α) _)
have rwa₂ : (↑(mkRat (↑(OfNat.ofNat x) : ℤ) (HPow.hPow (α := ℕ) (β := ℕ) 10 (OfNat.ofNat x_1))) : α) =
  HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : α) _)
Tactic: rwa [← Rat.cast_ofScientific, ← Rat.ofScientific_eq_ofScientific, Rat.ofScientific_true_def]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.OfScientific (goal)
Goal:
α : Type u_1
inst : DivisionRing α
n n_1 x : ℕ
h : x = n.mul (HPow.hPow (α := ℕ) 10 n_1)
⊢ Eq.{u_1 + 1} (α := α) (OfScientific.ofScientific (↑n : ℕ) false (↑n_1 : ℕ)) (↑x : α)
have rw : Eq.{u_1 + 1} (α := α) (↑(Rat.ofScientific (OfNat.ofNat (↑n : ℕ)) false (OfNat.ofNat (↑n_1 : ℕ))) : α) (↑x : α)
Tactic: rw [← Rat.cast_ofScientific, ← Rat.ofScientific_eq_ofScientific]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.OfScientific (goal)
Goal:
α : Type u_1
inst : DivisionRing α
n n_1 x : ℕ
h : x = n.mul (HPow.hPow (α := ℕ) 10 n_1)
⊢ Eq.{u_1 + 1} (α := α) (↑(Rat.ofScientific (OfNat.ofNat (↑n : ℕ)) false (OfNat.ofNat (↑n_1 : ℕ))) : α) (↑x : α)
have simp : (↑((↑(OfNat.ofNat n) : ℚ) * HPow.hPow (α := ℚ) (β := ℕ) 10 (OfNat.ofNat n_1)) : α) =
  (↑n : α) * HPow.hPow (α := α) 10 n_1
Tactic: simp only [Nat.cast_id, Rat.ofScientific_false_def, Nat.cast_mul, Nat.cast_pow,
      Nat.cast_ofNat, h, Nat.mul_eq]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.OfScientific (goal)
Goal:
α : Type u_1
inst : DivisionRing α
n n_1 x : ℕ
h : x = n.mul (HPow.hPow (α := ℕ) 10 n_1)
⊢ (↑((↑(OfNat.ofNat n) : ℚ) * HPow.hPow (α := ℚ) (β := ℕ) 10 (OfNat.ofNat n_1)) : α) =
    (↑n : α) * HPow.hPow (α := α) 10 n_1
have norm_cast : Eq.{u_1 + 1} (α := α) (↑(OfNat.ofNat n * HPow.hPow (α := ℕ) (β := ℕ) 10 (OfNat.ofNat n_1)) : α)
  (↑(n * HPow.hPow (α := ℕ) 10 n_1) : α)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Pow (goal)
Goal:
a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' = b
hc : c' * c' = c
⊢ (Int.negOfNat a).pow b = Int.ofNat c
have rw : Int.ofNat a ^ b' * Int.ofNat a ^ b' = Int.ofNat (a.pow b' * a.pow b')
Tactic: rw [← hb, Int.negOfNat_eq, Int.pow_eq, pow_mul, neg_pow_two, ← pow_mul, two_mul, pow_add, ← hc,
    ← h1]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Pow (goal)
Goal:
a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' + 1 = b
hc : c' * (c' * a) = c
⊢ (Int.negOfNat a).pow b = Int.negOfNat c
have rw : Int.ofNat a ^ b' * Int.ofNat a ^ b' * -Int.ofNat a = -Int.ofNat (a.pow b' * (a.pow b' * a))
Tactic: rw [← hb, Int.negOfNat_eq, Int.negOfNat_eq, Int.pow_eq, pow_succ, pow_mul, neg_pow_two, ← pow_mul,
    two_mul, pow_add, ← hc, ← h1]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Pow (goal)
Goal:
α : Type u_1
inst : Ring α
an : ℤ
ad b : ℕ
inv : Invertible (α := α) (↑ad : α)
⊢ IsRat (HMul.hMul (α := α) (↑an : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑ad : α) _) ^ b)
    (an ^ b) (ad ^ b)
have have : ∀ (this : Invertible (HPow.hPow (α := α) (↑ad : α) b)),
  IsRat (HMul.hMul (α := α) (↑an : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑ad : α) _) ^ b)
    (an ^ b) (ad ^ b)
Tactic: have := invertiblePow (ad:α) b
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Pow (goal)
Goal:
α : Type u_1
inst : Ring α
an : ℤ
ad b : ℕ
inv : Invertible (α := α) (↑ad : α)
this : Invertible (HPow.hPow (α := α) (↑ad : α) b)
⊢ IsRat (HMul.hMul (α := α) (↑an : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑ad : α) _) ^ b)
    (an ^ b) (ad ^ b)
have rw : ∀ (this : Invertible (α := α) (↑(ad ^ b) : α)),
  IsRat (HMul.hMul (α := α) (↑an : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑ad : α) _) ^ b)
    (an ^ b) (ad ^ b)
Tactic: rw [← Nat.cast_pow] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Pow (goal)
Goal:
α : Type u_1
inst : Ring α
an : ℤ
ad b : ℕ
inv : Invertible (α := α) (↑ad : α)
this : Invertible (α := α) (↑(ad ^ b) : α)
⊢ IsRat (HMul.hMul (α := α) (↑an : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑ad : α) _) ^ b)
    (an ^ b) (ad ^ b)
have eq : HMul.hMul (α := α) (↑an : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑ad : α) _) ^ b =
  HMul.hMul (α := α) (↑(an ^ b) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(ad ^ b) : α) _)
Tactic: use this
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Pow (goal)
Goal:
α : Type u_1
inst : Semiring α
an ad b : ℕ
inv : Invertible (α := α) (↑ad : α)
⊢ IsNNRat (HMul.hMul (α := α) (↑an : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑ad : α) _) ^ b)
    (an ^ b) (ad ^ b)
have have : ∀ (this : Invertible (HPow.hPow (α := α) (↑ad : α) b)),
  IsNNRat (HMul.hMul (α := α) (↑an : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑ad : α) _) ^ b)
    (an ^ b) (ad ^ b)
Tactic: have := invertiblePow (ad:α) b
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Pow (goal)
Goal:
α : Type u_1
inst : Semiring α
an ad b : ℕ
inv : Invertible (α := α) (↑ad : α)
this : Invertible (HPow.hPow (α := α) (↑ad : α) b)
⊢ IsNNRat (HMul.hMul (α := α) (↑an : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑ad : α) _) ^ b)
    (an ^ b) (ad ^ b)
have rw : ∀ (this : Invertible (α := α) (↑(ad ^ b) : α)),
  IsNNRat (HMul.hMul (α := α) (↑an : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑ad : α) _) ^ b)
    (an ^ b) (ad ^ b)
Tactic: rw [← Nat.cast_pow] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Pow (goal)
Goal:
α : Type u_1
inst : Semiring α
an ad b : ℕ
inv : Invertible (α := α) (↑ad : α)
this : Invertible (α := α) (↑(ad ^ b) : α)
⊢ IsNNRat (HMul.hMul (α := α) (↑an : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑ad : α) _) ^ b)
    (an ^ b) (ad ^ b)
have eq : HMul.hMul (α := α) (↑an : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑ad : α) _) ^ b =
  HMul.hMul (α := α) (↑(an ^ b) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(ad ^ b) : α) _)
Tactic: use this
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Pow (goal)
Goal:
α : Type u_1
inst : DivisionSemiring α
a : α
b : ℤ
nb ne : ℕ
pb : IsNat b nb
pe' : IsNat (a ^ nb) ne
⊢ IsNat (a ^ b) ne
have rwa : IsNat (HPow.hPow (β := ℤ) a (↑nb : ℤ)) ne
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 ne : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsNat (a ^ nb)⁻¹ ne
⊢ IsNat (a ^ b) ne
have rwa : IsNat (HPow.hPow (β := ℤ) a (↑(Int.negOfNat nb) : ℤ)) 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 ne : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsNat (a ^ nb)⁻¹ ne
rwa : IsNat (HPow.hPow (β := ℤ) a (↑(Int.negOfNat nb) : ℤ)) ne
⊢ IsNat (a ^ b) ne
have rwa₁ : IsNat (HPow.hPow (β := ℤ) a (-(↑nb : ℤ))) 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 ne : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsNat (a ^ nb)⁻¹ ne
rwa : IsNat (HPow.hPow (β := ℤ) a (↑(Int.negOfNat nb) : ℤ)) ne
rwa₁ : IsNat (HPow.hPow (β := ℤ) a (-(↑nb : ℤ))) ne
⊢ IsNat (a ^ b) ne
have rwa₂ : IsNat (HPow.hPow (β := ℤ) a (↑nb : ℤ))⁻¹ 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 : IsNat b nb
pe' : IsInt (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, zpow_natCast]