awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Tactic.NormNum.NatFactorial
Goal:
n x : ℕ
h₁ : IsNat n x
a : ℕ
h₂ : ascFactorial 1 x = a
⊢ n ! = (↑a : ℕ)

Tactic:
simp only [h₁.out, cast_id, ← h₂, one_ascFactorial]

Premises used: Nat.cast_id, Nat.one_ascFactorial, Mathlib.Meta.NormNum.IsNat.out
-- Module: Mathlib.Tactic.NormNum.NatFactorial
Goal:
n x l y : ℕ
h₁ : IsNat n x
h₂ : IsNat l y
a : ℕ
p : x.ascFactorial y = a
out : n.ascFactorial l = (↑a : ℕ)
⊢ IsNat (n.ascFactorial l) a

Tactic:
constructor
-- Module: Mathlib.Tactic.NormNum.NatFactorial
Goal:
n x l y : ℕ
h₁ : IsNat n x
h₂ : IsNat l y
a : ℕ
p : x.ascFactorial y = a
⊢ n.ascFactorial l = (↑a : ℕ)

Tactic:
simp [h₁.out, h₂.out, ← p]

Premises used: Mathlib.Meta.NormNum.IsNat.out
-- Module: Mathlib.Tactic.NormNum.NatFactorial
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
out : n.descFactorial l = (↑a : ℕ)
⊢ IsNat (n.descFactorial l) a

Tactic:
constructor
-- Module: Mathlib.Tactic.NormNum.NatFactorial
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
⊢ n.descFactorial l = (↑a : ℕ)

Tactic:
simpa [h₁.out, h₂.out, ← p, h₃] using Nat.add_descFactorial_eq_ascFactorial _ _

Premises used: Nat.add_descFactorial_eq_ascFactorial, Mathlib.Meta.NormNum.IsNat.out
-- Module: Mathlib.Tactic.NormNum.NatFactorial
Goal:
n x l y z : ℕ
h₁ : IsNat n x
h₂ : IsNat l y
h₃ : y = z + x + 1
out : n.descFactorial l = (↑0 : ℕ)
⊢ IsNat (n.descFactorial l) 0

Tactic:
constructor
-- Module: Mathlib.Tactic.NormNum.NatFactorial
Goal:
n x l y z : ℕ
h₁ : IsNat n x
h₂ : IsNat l y
h₃ : y = z + x + 1
⊢ n.descFactorial l = (↑0 : ℕ)

Tactic:
simp [h₁.out, h₂.out, h₃]

Premises used: Mathlib.Meta.NormNum.IsNat.out
-- Module: Mathlib.Tactic.NormNum.NatFib
Goal:
⊢ IsFibAux 0 0 1

Tactic:
⟨fib_zero, fib_one⟩

Premises used: Nat.fib_one, And.intro, Mathlib.Meta.NormNum.IsFibAux, Nat.fib_zero
-- Module: Mathlib.Tactic.NormNum.NatFib
Goal:
⊢ IsFibAux 1 1 1

Tactic:
⟨fib_one, fib_two⟩

Premises used: Nat.fib_one, Nat.fib_two, And.intro, Mathlib.Meta.NormNum.IsFibAux
-- Module: Mathlib.Tactic.NormNum.NatFib
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'
rw₄ rw₅ : a * (2 * b - a) = a * (2 * b - a)
⊢ fib n' = a'

Tactic:
rw [← hn, fib_two_mul, H.1, H.2, ← h1]

Premises used: Nat.fib_two_mul, And.right, And.left
-- Module: Mathlib.Tactic.NormNum.NatFib
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'
rw₇ rw₈ : b' = b'
⊢ fib (n' + 1) = b'

Tactic:
rw [← hn, fib_two_mul_add_one, H.1, H.2, pow_two, pow_two, add_comm, h2]

Premises used: pow_two, add_comm, Nat.fib_two_mul_add_one, And.right, And.left
-- Module: Mathlib.Tactic.NormNum.NatFib
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'
rw₇ rw₈ : a' = a'
⊢ fib n' = a'

Tactic:
rw [← hn, fib_two_mul_add_one, H.1, H.2, pow_two, pow_two, add_comm, h1]

Premises used: pow_two, add_comm, Nat.fib_two_mul_add_one, And.right, And.left
-- Module: Mathlib.Tactic.NormNum.NatFib
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'
rw₄ rw₅ : b' = b'
⊢ fib (n' + 1) = b'

Tactic:
rw [← hn, fib_two_mul_add_two, H.1, H.2, h2]

Premises used: And.right, And.left, Nat.fib_two_mul_add_two
-- Module: Mathlib.Tactic.NormNum.NatFib
Goal:
n a b n' a' : ℕ
H : IsFibAux n a b
hn : 2 * n = n'
h : a * (2 * b - a) = a'
⊢ fib n' = a'

Tactic:
(isFibAux_two_mul H hn h rfl).1

Premises used: And.left, Mathlib.Meta.NormNum.isFibAux_two_mul, rfl
-- Module: Mathlib.Tactic.NormNum.NatFib
Goal:
n a b n' a' : ℕ
H : IsFibAux n a b
hn : 2 * n + 1 = n'
h : a * a + b * b = a'
⊢ fib n' = a'

Tactic:
(isFibAux_two_mul_add_one H hn h rfl).1

Premises used: Mathlib.Meta.NormNum.isFibAux_two_mul_add_one, And.left, rfl
-- Module: Mathlib.Tactic.NormNum.NatLog
Goal:
n : ℕ
⊢ Nat.log 0 n = 0

Tactic:
Nat.log_zero_left n

Premises used: Nat.log_zero_left
-- Module: Mathlib.Tactic.NormNum.NatLog
Goal:
n : ℕ
⊢ Nat.log 1 n = 0

Tactic:
Nat.log_one_left n

Premises used: Nat.log_one_left
-- Module: Mathlib.Tactic.NormNum.NatLog
Goal:
b n : ℕ
hl : n.blt b = true
⊢ n < b

Tactic:
rw [Nat.blt_eq] at hl

Premises used: Nat.blt_eq
-- Module: Mathlib.Tactic.NormNum.NatLog
Goal:
b n : ℕ
hl : n < b
⊢ Nat.log b n = 0

Tactic:
simp [hl]
-- Module: Mathlib.Tactic.NormNum.NatLog
Goal:
b n k : ℕ
hl : (b ^ k).ble n = true
hh : n.blt (b ^ (k + 1)) = true
⊢ Nat.log b n = k

Tactic:
Nat.log_eq_of_pow_le_of_lt_pow (Nat.le_of_ble_eq_true hl) (Nat.le_of_ble_eq_true hh)

Premises used: Nat.le_of_ble_eq_true, Nat.log_eq_of_pow_le_of_lt_pow
-- Module: Mathlib.Tactic.NormNum.NatLog
Goal:
b n : ℕ
hb : b.ble 1 = true
⊢ Nat.clog b n = 0

Tactic:
Nat.clog_of_left_le_one (Nat.le_of_ble_eq_true hb) n

Premises used: Nat.le_of_ble_eq_true, Nat.clog_of_left_le_one
-- Module: Mathlib.Tactic.NormNum.NatLog
Goal:
b n : ℕ
hn : n.ble 1 = true
⊢ Nat.clog b n = 0

Tactic:
Nat.clog_of_right_le_one (Nat.le_of_ble_eq_true hn) b

Premises used: Nat.le_of_ble_eq_true, Nat.clog_of_right_le_one
-- Module: Mathlib.Tactic.NormNum.NatLog
Goal:
b m n : ℕ
hb : Nat.blt 1 b = true
h₁ : (b ^ m).blt n = true
h₂ : n.ble (b ^ (m + 1)) = true
⊢ 1 < b

Tactic:
rw [Nat.blt_eq] at hb

Premises used: Nat.blt_eq
-- Module: Mathlib.Tactic.NormNum.NatLog
Goal:
b m n : ℕ
hb : Nat.blt 1 b = true
h₁ : (b ^ m).blt n = true
h₂ : n.ble (b ^ (m + 1)) = true
hb₁ : 1 < b
⊢ (b ^ m).blt n = true

Tactic:
rw [Nat.blt_eq] at hb

Premises used: Nat.blt_eq
-- Module: Mathlib.Tactic.NormNum.NatLog
Goal:
b m n : ℕ
hb : Nat.blt 1 b = true
h₁ : (b ^ m).blt n = true
h₂ : n.ble (b ^ (m + 1)) = true
hb₁ : 1 < b
h₃ : (b ^ m).blt n = true
⊢ n.ble (b ^ (m + 1)) = true

Tactic:
rw [Nat.blt_eq] at hb

Premises used: Nat.blt_eq
-- Module: Mathlib.Tactic.NormNum.NatLog
Goal:
b m n : ℕ
hb : 1 < b
h₁ : (b ^ m).blt n = true
h₂ : n.ble (b ^ (m + 1)) = true
⊢ m < Nat.clog b n

Tactic:
rw [Nat.blt_eq, ← Nat.lt_clog_iff_pow_lt hb] at h₁

Premises used: Nat.lt_clog_iff_pow_lt, Nat.blt_eq
-- Module: Mathlib.Tactic.NormNum.NatLog
Goal:
b m n : ℕ
hb : 1 < b
h₁ : (b ^ m).blt n = true
h₂ : n.ble (b ^ (m + 1)) = true
h₃ : m < Nat.clog b n
⊢ n.ble (b ^ (m + 1)) = true

Tactic:
rw [Nat.blt_eq, ← Nat.lt_clog_iff_pow_lt hb] at h₁

Premises used: Nat.lt_clog_iff_pow_lt, Nat.blt_eq
-- Module: Mathlib.Tactic.NormNum.NatLog
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

Tactic:
rw [Nat.ble_eq, ← Nat.clog_le_iff_le_pow hb] at h₂

Premises used: Nat.ble_eq, Nat.clog_le_iff_le_pow
-- Module: Mathlib.Tactic.NormNum.NatLog
Goal:
b m n : ℕ
hb : 1 < b
h₁ : m < Nat.clog b n
h₂ : Nat.clog b n ≤ m + 1
⊢ Nat.clog b n = m + 1

Tactic:
lia
-- Module: Mathlib.Tactic.NormNum.NatLog
Goal:
eb en : Q(ℕ)
b : ℕ := Expr.natLit! eb
n : ℕ := Expr.natLit! en
h_1 : ¬b ≤ 1
h_2 : ¬n ≤ 1
h : Nat.clog b n = 0
⊢ 1 < b

Tactic:
lia
-- Module: Mathlib.Tactic.NormNum.NatLog
Goal:
eb en : Q(ℕ)
b : ℕ := Expr.natLit! eb
n : ℕ := Expr.natLit! en
h_1 : ¬b ≤ 1
h_2 : ¬n ≤ 1
h : Nat.clog b n = 0
⊢ 1 < n

Tactic:
lia
-- Module: Mathlib.Tactic.NormNum.NatSqrt
Goal:
x y r : ℕ
hr : y * y + r = x
hle : r.ble (2 * y) = true
rw : (HPow.hPow (β := ℕ) y 2 + r).sqrt = y
⊢ x.sqrt = y

Tactic:
rw [← hr, ← pow_two]

Premises used: pow_two
-- Module: Mathlib.Tactic.NormNum.NatSqrt
Goal:
x y r : ℕ
hr : y * y + r = x
hle : r.ble (2 * y) = true
⊢ r.ble (y + y) = true

Tactic:
rw [two_mul] at hle

Premises used: two_mul
-- Module: Mathlib.Tactic.NormNum.NatSqrt
Goal:
x y r : ℕ
hr : y * y + r = x
hle : r.ble (y + y) = true
⊢ (HPow.hPow (β := ℕ) y 2 + r).sqrt = y

Tactic:
Nat.sqrt_add_eq' _ (Nat.le_of_ble_eq_true hle)

Premises used: Nat.le_of_ble_eq_true, Nat.sqrt_add_eq'
-- Module: Mathlib.Tactic.NormNum.NatSqrt
Goal:
x y r : ℕ
hr : y * y + r = x
hle : r.ble (y + y) = true
⊢ (HPow.hPow (β := ℕ) y 2 + r).sqrt = y

Tactic:
exact Nat.sqrt_add_eq' _ (Nat.le_of_ble_eq_true hle)

Premises used: Nat.le_of_ble_eq_true, Nat.sqrt_add_eq'
-- Module: Mathlib.Tactic.NormNum.OfScientific
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 : α) _)
rwa₂ rwa₃ rwa₄ rwa₅ :
  (↑(mkRat (↑(OfNat.ofNat x) : ℤ) (HPow.hPow (α := ℕ) (β := ℕ) 10 (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 : α) _)

Tactic:
rwa [← Rat.cast_ofScientific, ← Rat.ofScientific_eq_ofScientific, Rat.ofScientific_true_def]

Premises used: Rat.ofScientific_true_def, Rat.cast_ofScientific, Rat.ofScientific_eq_ofScientific
-- Module: Mathlib.Tactic.NormNum.OfScientific
Goal:
α : Type u_1
inst : DivisionRing α
n n_1 x : ℕ
h : x = n.mul (HPow.hPow (α := ℕ) 10 n_1)
rw : Eq.{u_1 + 1} (α := α) (↑(Rat.ofScientific (OfNat.ofNat (↑n : ℕ)) false (OfNat.ofNat (↑n_1 : ℕ))) : α) (↑x : α)
⊢ Eq.{u_1 + 1} (α := α) (OfScientific.ofScientific (↑n : ℕ) false (↑n_1 : ℕ)) (↑x : α)

Tactic:
rw [← Rat.cast_ofScientific, ← Rat.ofScientific_eq_ofScientific]

Premises used: Rat.cast_ofScientific, Rat.ofScientific_eq_ofScientific
-- Module: Mathlib.Tactic.NormNum.OfScientific
Goal:
α : Type u_1
inst : DivisionRing α
n n_1 x : ℕ
h : x = n.mul (HPow.hPow (α := ℕ) 10 n_1)
simp :
  (↑((↑(OfNat.ofNat n) : ℚ) * HPow.hPow (α := ℚ) (β := ℕ) 10 (OfNat.ofNat n_1)) : α) =
    (↑n : α) * HPow.hPow (α := α) 10 n_1
⊢ Eq.{u_1 + 1} (α := α) (↑(Rat.ofScientific (OfNat.ofNat (↑n : ℕ)) false (OfNat.ofNat (↑n_1 : ℕ))) : α) (↑x : α)

Tactic:
simp only [Nat.cast_id, Rat.ofScientific_false_def, Nat.cast_mul, Nat.cast_pow,
      Nat.cast_ofNat, h, Nat.mul_eq]

Premises used: Nat.cast_ofNat, Nat.cast_id, Nat.cast_mul, Nat.mul_eq, Rat.ofScientific_false_def, Nat.cast_pow
-- Module: Mathlib.Tactic.NormNum.OfScientific
Goal:
α : Type u_1
inst : DivisionRing α
n n_1 x : ℕ
h : x = n.mul (HPow.hPow (α := ℕ) 10 n_1)
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  Eq.{u_1 + 1} (α := α) (↑(OfNat.ofNat n * HPow.hPow (α := ℕ) (β := ℕ) 10 (OfNat.ofNat n_1)) : α)
    (↑(n * HPow.hPow (α := ℕ) 10 n_1) : α)
⊢ (↑((↑(OfNat.ofNat n) : ℚ) * HPow.hPow (α := ℚ) (β := ℕ) 10 (OfNat.ofNat n_1)) : α) =
    (↑n : α) * HPow.hPow (α := α) 10 n_1

Tactic:
norm_cast
-- Module: Mathlib.Tactic.NormNum.Pow
Goal:
a : ℕ
⊢ a.pow 0 = 1

Tactic:
rfl

Premises used: Nat.pow, rfl
-- Module: Mathlib.Tactic.NormNum.Pow
Goal:
a : ℕ
⊢ a.pow 1 = a

Tactic:
Nat.pow_one _

Premises used: Nat.pow_one
-- Module: Mathlib.Tactic.NormNum.Pow
Goal:
b : ℕ
⊢ Nat.pow 0 b.succ = 0

Tactic:
rfl

Premises used: Nat.pow, rfl
-- Module: Mathlib.Tactic.NormNum.Pow
Goal:
b : ℕ
⊢ Nat.pow 1 b = 1

Tactic:
Nat.one_pow _

Premises used: Nat.one_pow
-- Module: Mathlib.Tactic.NormNum.Pow
Goal:
a b c : ℕ
p : IsNatPowT (a.pow 1 = a) a b c
⊢ a.pow b = c

Tactic:
p.run' (Nat.pow_one _)

Premises used: Mathlib.Meta.NormNum.IsNatPowT.run', Nat.pow_one
-- Module: Mathlib.Tactic.NormNum.Pow
Goal:
a b c : ℕ
p : Prop
b' c' : ℕ
h1 : IsNatPowT p a b c
h2 : IsNatPowT (a.pow b = c) a b' c'
⊢ IsNatPowT p a b' c'

Tactic:
⟨h2.run' ∘ h1.run'⟩

Premises used: Function.comp, Mathlib.Meta.NormNum.IsNatPowT.run', Mathlib.Meta.NormNum.IsNatPowT.mk
-- Module: Mathlib.Tactic.NormNum.Pow
Goal:
a b c : ℕ
h1 : a.pow b = c
⊢ a.pow (2 * b) = c.mul c

Tactic:
simp [two_mul, pow_add, ← h1]

Premises used: two_mul, pow_add
-- Module: Mathlib.Tactic.NormNum.Pow
Goal:
a b c : ℕ
h1 : a.pow b = c
⊢ a.pow (2 * b + 1) = c.mul (c.mul a)

Tactic:
simp [two_mul, pow_add, mul_assoc, ← h1]

Premises used: mul_assoc, two_mul, pow_add
-- Module: Mathlib.Tactic.NormNum.Pow
Goal:
a_1 b_1 c : ℕ
a_2 b_2 : Q(ℕ)
depth : ℕ
a b₀ c₀ b : Q(ℕ)
p : Q(Prop)
hp : «$p» =Q Eq «$c₀»
b' : ℕ := Expr.natLit! b
d : ℕ := HShiftRight.hShiftRight (β := ℕ) depth 1
hi : Q(ℕ)
⊢ «$p» =Q Eq «$c₀»

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

Tactic:
exact hp
-- Module: Mathlib.Tactic.NormNum.Pow
Goal:
a b c : ℕ
h1 : a.pow b = c
⊢ (Int.ofNat a).pow b = Int.ofNat c

Tactic:
simp [← h1]
-- Module: Mathlib.Tactic.NormNum.Pow
Goal:
a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' = b
hc : c' * c' = c
rw : Int.ofNat a ^ b' * Int.ofNat a ^ b' = Int.ofNat (a.pow b' * a.pow b')
⊢ (Int.negOfNat a).pow b = Int.ofNat c

Tactic:
rw [← hb, Int.negOfNat_eq, Int.pow_eq, pow_mul, neg_pow_two, ← pow_mul, two_mul, pow_add, ← hc,
    ← h1]

Premises used: Int.pow_eq, two_mul, pow_add, neg_pow_two, pow_mul, Int.negOfNat_eq
-- Module: Mathlib.Tactic.NormNum.Pow
Goal:
a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' = b
hc : c' * c' = c
⊢ Int.ofNat a ^ b' * Int.ofNat a ^ b' = Int.ofNat (a.pow b' * a.pow b')

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Pow
Goal:
a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' + 1 = b
hc : c' * (c' * a) = c
rw : Int.ofNat a ^ b' * Int.ofNat a ^ b' * -Int.ofNat a = -Int.ofNat (a.pow b' * (a.pow b' * a))
⊢ (Int.negOfNat a).pow b = Int.negOfNat c

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]

Premises used: Int.pow_eq, pow_succ, two_mul, pow_add, neg_pow_two, pow_mul, Int.negOfNat_eq
-- Module: Mathlib.Tactic.NormNum.Pow
Goal:
a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' + 1 = b
hc : c' * (c' * a) = c
⊢ Int.ofNat a ^ b' * Int.ofNat a ^ b' * -Int.ofNat a = -Int.ofNat (a.pow b' * (a.pow b' * a))

Tactic:
simp [mul_comm, mul_left_comm]

Premises used: mul_left_comm, mul_comm
-- Module: Mathlib.Tactic.NormNum.Pow
Goal:
α : Type u_1
inst : Semiring α
n n_1 : ℕ
⊢ HPow.hPow (α := α) (β := ℕ) (↑n : α) (↑n_1 : ℕ) = (↑(n.pow n_1) : α)

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Pow
Goal:
α : Type u_1
inst : Ring α
n : ℤ
n_1 : ℕ
⊢ HPow.hPow (α := α) (β := ℕ) (↑n : α) (↑n_1 : ℕ) = (↑(n.pow n_1) : α)

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Pow
Goal:
α : Type u_1
inst : Ring α
an : ℤ
ad b : ℕ
inv : Invertible (α := α) (↑ad : α)
have :
  ∀ (this : Invertible (HPow.hPow (α := α) (↑ad : α) b)),
    IsRat (HMul.hMul (α := α) (↑an : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑ad : α) _) ^ b)
      (an ^ b) (ad ^ b)
⊢ IsRat (HMul.hMul (α := α) (↑an : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑ad : α) _) ^ b)
    (an ^ b) (ad ^ b)

Tactic:
have := invertiblePow (ad:α) b
-- Module: Mathlib.Tactic.NormNum.Pow
Goal:
α : Type u_1
inst : Ring α
an : ℤ
ad b : ℕ
inv : Invertible (α := α) (↑ad : α)
this : Invertible (HPow.hPow (α := α) (↑ad : α) b)
rw :
  ∀ (this : Invertible (α := α) (↑(ad ^ b) : α)),
    IsRat (HMul.hMul (α := α) (↑an : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑ad : α) _) ^ b)
      (an ^ b) (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

Premises used: Nat.cast_pow
-- Module: Mathlib.Tactic.NormNum.Pow
Goal:
α : Type u_1
inst : Ring α
an : ℤ
ad b : ℕ
inv : Invertible (α := α) (↑ad : α)
this : Invertible (α := α) (↑(ad ^ b) : α)
eq :
  HMul.hMul (α := α) (↑an : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑ad : α) _) ^ b =
    HMul.hMul (α := α) (↑(an ^ b) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(ad ^ b) : α) _)
⊢ IsRat (HMul.hMul (α := α) (↑an : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑ad : α) _) ^ b)
    (an ^ b) (ad ^ b)

Tactic:
use this
-- Module: Mathlib.Tactic.NormNum.Pow
Goal:
α : Type u_1
inst : Ring α
an : ℤ
ad b : ℕ
inv : Invertible (α := α) (↑ad : α)
this : Invertible (α := α) (↑(ad ^ b) : α)
⊢ HMul.hMul (α := α) (↑an : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑ad : α) _) ^ b =
    HMul.hMul (α := α) (↑(an ^ b) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(ad ^ b) : α) _)

Tactic:
simp [invOf_pow, Commute.mul_pow]

Premises used: Commute.mul_pow, invOf_pow
-- Module: Mathlib.Tactic.NormNum.Pow
Goal:
α : Type u_1
inst : Semiring α
an ad b : ℕ
inv : Invertible (α := α) (↑ad : α)
have :
  ∀ (this : Invertible (HPow.hPow (α := α) (↑ad : α) b)),
    IsNNRat (HMul.hMul (α := α) (↑an : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑ad : α) _) ^ b)
      (an ^ b) (ad ^ b)
⊢ IsNNRat (HMul.hMul (α := α) (↑an : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑ad : α) _) ^ b)
    (an ^ b) (ad ^ b)

Tactic:
have := invertiblePow (ad:α) b
-- Module: Mathlib.Tactic.NormNum.Pow
Goal:
α : Type u_1
inst : Semiring α
an ad b : ℕ
inv : Invertible (α := α) (↑ad : α)
this : Invertible (HPow.hPow (α := α) (↑ad : α) b)
rw :
  ∀ (this : Invertible (α := α) (↑(ad ^ b) : α)),
    IsNNRat (HMul.hMul (α := α) (↑an : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑ad : α) _) ^ b)
      (an ^ b) (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

Premises used: Nat.cast_pow
-- Module: Mathlib.Tactic.NormNum.Pow
Goal:
α : Type u_1
inst : Semiring α
an ad b : ℕ
inv : Invertible (α := α) (↑ad : α)
this : Invertible (α := α) (↑(ad ^ b) : α)
eq :
  HMul.hMul (α := α) (↑an : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑ad : α) _) ^ b =
    HMul.hMul (α := α) (↑(an ^ b) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(ad ^ b) : α) _)
⊢ IsNNRat (HMul.hMul (α := α) (↑an : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑ad : α) _) ^ b)
    (an ^ b) (ad ^ b)

Tactic:
use this
-- Module: Mathlib.Tactic.NormNum.Pow
Goal:
α : Type u_1
inst : Semiring α
an ad b : ℕ
inv : Invertible (α := α) (↑ad : α)
this : Invertible (α := α) (↑(ad ^ b) : α)
⊢ HMul.hMul (α := α) (↑an : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑ad : α) _) ^ b =
    HMul.hMul (α := α) (↑(an ^ b) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑(ad ^ b) : α) _)

Tactic:
simp [invOf_pow, Commute.mul_pow, Nat.cast_commute]

Premises used: Commute.mul_pow, invOf_pow, Nat.cast_commute
-- Module: Mathlib.Tactic.NormNum.Pow
Goal:
α : Type u_1
inst : DivisionSemiring α
a : α
b : ℤ
nb ne : ℕ
pb : IsNat b nb
pe' : IsNat (a ^ nb) ne
rwa : IsNat (HPow.hPow (β := ℤ) a (↑nb : ℤ)) ne
rwa₁ rwa₂ rwa₃ rwa₄ : IsNat (a ^ nb) ne
⊢ IsNat (a ^ b) ne

Tactic:
rwa [pb.out, zpow_natCast]

Premises used: zpow_natCast, Mathlib.Meta.NormNum.IsNat.out
-- Module: Mathlib.Tactic.NormNum.Pow
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
rwa₂ : IsNat (HPow.hPow (β := ℤ) a (↑nb : ℤ))⁻¹ ne
rwa₃ rwa₄ rwa₅ rwa₆ : IsNat (a ^ nb)⁻¹ ne
⊢ IsNat (a ^ b) ne

Tactic:
rwa [pb.out, Int.cast_negOfNat, zpow_neg, zpow_natCast]

Premises used: zpow_natCast, zpow_neg, Int.cast_negOfNat, Mathlib.Meta.NormNum.IsInt.out
-- Module: Mathlib.Tactic.NormNum.Pow
Goal:
α : Type u_1
inst : DivisionRing α
a : α
b : ℤ
nb ne : ℕ
pb : IsNat b nb
pe' : IsInt (a ^ nb) (Int.negOfNat ne)
rwa : IsInt (HPow.hPow (β := ℤ) a (↑nb : ℤ)) (Int.negOfNat ne)
rwa₁ rwa₂ rwa₃ rwa₄ : IsInt (a ^ nb) (Int.negOfNat ne)
⊢ IsInt (a ^ b) (Int.negOfNat ne)

Tactic:
rwa [pb.out, zpow_natCast]

Premises used: zpow_natCast, Mathlib.Meta.NormNum.IsNat.out
-- Module: Mathlib.Tactic.NormNum.Pow
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)
rwa₂ : IsInt (HPow.hPow (β := ℤ) a (↑nb : ℤ))⁻¹ (Int.negOfNat ne)
rwa₃ rwa₄ rwa₅ rwa₆ : IsInt (a ^ nb)⁻¹ (Int.negOfNat ne)
⊢ IsInt (a ^ b) (Int.negOfNat ne)

Tactic:
rwa [pb.out, Int.cast_negOfNat, zpow_neg, zpow_natCast]

Premises used: zpow_natCast, zpow_neg, Int.cast_negOfNat, Mathlib.Meta.NormNum.IsInt.out
-- Module: Mathlib.Tactic.NormNum.Pow
Goal:
α : Type u_1
inst : DivisionSemiring α
a : α
b : ℤ
nb num den : ℕ
pb : IsNat b nb
pe' : IsNNRat (a ^ nb) num den
rwa : IsNNRat (HPow.hPow (β := ℤ) a (↑nb : ℤ)) num den
rwa₁ rwa₂ rwa₃ rwa₄ : IsNNRat (a ^ nb) num den
⊢ IsNNRat (a ^ b) num den

Tactic:
rwa [pb.out, zpow_natCast]

Premises used: zpow_natCast, Mathlib.Meta.NormNum.IsNat.out
-- Module: Mathlib.Tactic.NormNum.Pow
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
rwa₂ : IsNNRat (HPow.hPow (β := ℤ) a (↑nb : ℤ))⁻¹ num den
rwa₃ rwa₄ rwa₅ rwa₆ : IsNNRat (a ^ nb)⁻¹ num den
⊢ IsNNRat (a ^ b) num den

Tactic:
rwa [pb.out, Int.cast_negOfNat, zpow_neg, zpow_natCast]

Premises used: zpow_natCast, zpow_neg, Int.cast_negOfNat, Mathlib.Meta.NormNum.IsInt.out
-- Module: Mathlib.Tactic.NormNum.Pow
Goal:
α : Type u_1
inst : DivisionRing α
a : α
b : ℤ
nb : ℕ
num : ℤ
den : ℕ
pb : IsNat b nb
pe' : IsRat (a ^ nb) num den
rwa : IsRat (HPow.hPow (β := ℤ) a (↑nb : ℤ)) num den
rwa₁ rwa₂ rwa₃ rwa₄ : IsRat (a ^ nb) num den
⊢ IsRat (a ^ b) num den

Tactic:
rwa [pb.out, zpow_natCast]

Premises used: zpow_natCast, Mathlib.Meta.NormNum.IsNat.out
-- Module: Mathlib.Tactic.NormNum.Pow
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
rwa₂ : IsRat (HPow.hPow (β := ℤ) a (↑nb : ℤ))⁻¹ num den
rwa₃ rwa₄ rwa₅ rwa₆ : IsRat (a ^ nb)⁻¹ num den
⊢ IsRat (a ^ b) num den

Tactic:
rwa [pb.out, Int.cast_negOfNat, zpow_neg, zpow_natCast]

Premises used: zpow_natCast, zpow_neg, Int.cast_negOfNat, Mathlib.Meta.NormNum.IsInt.out
-- Module: Mathlib.Tactic.NormNum.PowMod
Goal:
a m b c : ℕ
p : IsNatPowModT ((a.pow 1).mod m = a.mod m) a b m c
⊢ (a.pow b).mod m = c

Tactic:
p.run' (congr_arg (fun x => x % m) (Nat.pow_one a))

Premises used: Mathlib.Meta.NormNum.IsNatPowModT.run', congr_arg, HMod.hMod, Nat.pow_one
-- Module: Mathlib.Tactic.NormNum.PowMod
Goal:
p : Prop
a b m c b' c' : ℕ
h1 : IsNatPowModT p a b m c
h2 : IsNatPowModT ((a.pow b).mod m = c) a b' m c'
⊢ IsNatPowModT p a b' m c'

Tactic:
⟨h2.run' ∘ h1.run'⟩

Premises used: Function.comp, Mathlib.Meta.NormNum.IsNatPowModT.run', Mathlib.Meta.NormNum.IsNatPowModT.mk