internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Rational.pow_flatten
Proof state before:
ℕ ℤ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
ℚ : Type
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Natural.Exponentiation ℕ fun x x_1 => x * x_1
inst✝¹ : Exponentiation ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
a b : ℤ
n m : ℕ
a_eqv : a ≃ Coe.coe n - Coe.coe m
k j : ℕ
b_eqv : b ≃ Coe.coe k - Coe.coe j
pow_expand : (p ^ a) ^ b ≃ (p ^ n) ^ k / (p ^ m) ^ k / ((p ^ n) ^ j / (p ^ m) ^ j)
pow_combine : ∀ {w x y z : ℕ}, (p ^ w) ^ x * (p ^ y) ^ z ≃ p ^ (w * x + y * z)
multi_compat : ∀ {w x y z : ℕ}, Coe.coe (w * x + y * z) ≃ Coe.coe w * Coe.coe x + Coe.coe y * Coe.coe z
diff_expand : ∀ {w x y z : ℤ}, (w - x) * (y - z) ≃ w * y + x * z - (x * y + w * z)
⊢ (p ^ a) ^ b ≃ p ^ (a * b)
Tactic:
have pow_reduce : ((n*k + m*j : ℕ):ℤ) - ((m*k + n*j : ℕ):ℤ) ≃ a * b := calc
  _ = ((n*k + m*j : ℕ):ℤ) - ((m*k + n*j : ℕ):ℤ) := rfl
  _ ≃ ((n:ℤ)*k + m*j) - ((m*k + n*j : ℕ):ℤ)     := AA.substL multi_compat
  _ ≃ ((n:ℤ)*k + m*j) - (m*k + n*j)             := AA.substR multi_compat
  _ ≃ ((n:ℤ) - m) * (k - j)                     := Rel.symm diff_expand
  _ ≃ a * (k - j)                               := AA.substL (Rel.symm a_eqv)
  _ ≃ a * b                                     := AA.substR (Rel.symm b_eqv)
Proof state after:
ℕ ℤ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
ℚ : Type
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Natural.Exponentiation ℕ fun x x_1 => x * x_1
inst✝¹ : Exponentiation ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
a b : ℤ
n m : ℕ
a_eqv : a ≃ Coe.coe n - Coe.coe m
k j : ℕ
b_eqv : b ≃ Coe.coe k - Coe.coe j
pow_expand : (p ^ a) ^ b ≃ (p ^ n) ^ k / (p ^ m) ^ k / ((p ^ n) ^ j / (p ^ m) ^ j)
pow_combine : ∀ {w x y z : ℕ}, (p ^ w) ^ x * (p ^ y) ^ z ≃ p ^ (w * x + y * z)
multi_compat : ∀ {w x y z : ℕ}, Coe.coe (w * x + y * z) ≃ Coe.coe w * Coe.coe x + Coe.coe y * Coe.coe z
diff_expand : ∀ {w x y z : ℤ}, (w - x) * (y - z) ≃ w * y + x * z - (x * y + w * z)
pow_reduce : Coe.coe (n * k + m * j) - Coe.coe (m * k + n * j) ≃ a * b
⊢ (p ^ a) ^ b ≃ p ^ (a * b)
Theorem: Lean4Axiomatic.Rational.pow_flatten
Proof state before:
ℕ ℤ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
ℚ : Type
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Natural.Exponentiation ℕ fun x x_1 => x * x_1
inst✝¹ : Exponentiation ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
a b : ℤ
n m : ℕ
a_eqv : a ≃ Coe.coe n - Coe.coe m
k j : ℕ
b_eqv : b ≃ Coe.coe k - Coe.coe j
pow_expand : (p ^ a) ^ b ≃ (p ^ n) ^ k / (p ^ m) ^ k / ((p ^ n) ^ j / (p ^ m) ^ j)
pow_combine : ∀ {w x y z : ℕ}, (p ^ w) ^ x * (p ^ y) ^ z ≃ p ^ (w * x + y * z)
multi_compat : ∀ {w x y z : ℕ}, Coe.coe (w * x + y * z) ≃ Coe.coe w * Coe.coe x + Coe.coe y * Coe.coe z
diff_expand : ∀ {w x y z : ℤ}, (w - x) * (y - z) ≃ w * y + x * z - (x * y + w * z)
pow_reduce : Coe.coe (n * k + m * j) - Coe.coe (m * k + n * j) ≃ a * b
⊢ (p ^ a) ^ b ≃ p ^ (a * b)
Tactic:
calc
  _ = (p^a)^b                                       := rfl
  _ ≃ ((p^n)^k/(p^m)^k) / ((p^n)^j/(p^m)^j)         := pow_expand
  _ ≃ ((p^n)^k*(p^m)^j) / ((p^m)^k*(p^n)^j)         := div_div_div
  _ ≃ p^(n*k + m*j) / ((p^m)^k*(p^n)^j)             := div_substL pow_combine
  _ ≃ p^(n*k + m*j) / p^(m*k + n*j)                 := div_substR pow_combine
  _ ≃ p^(((n*k + m*j : ℕ):ℤ) - ((m*k + n*j : ℕ):ℤ)) := eqv_symm pow_diff
  _ ≃ p^(a * b)                                     := pow_substR pow_reduce
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.pow_flatten
Proof state before:
ℕ ℤ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
ℚ : Type
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Natural.Exponentiation ℕ fun x x_1 => x * x_1
inst✝¹ : Exponentiation ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
a b : ℤ
n m : ℕ
a_eqv : a ≃ Coe.coe n - Coe.coe m
k j : ℕ
b_eqv : b ≃ Coe.coe k - Coe.coe j
pow_expand : (p ^ a) ^ b ≃ (p ^ n) ^ k / (p ^ m) ^ k / ((p ^ n) ^ j / (p ^ m) ^ j)
pow_combine : ∀ {w x y z : ℕ}, (p ^ w) ^ x * (p ^ y) ^ z ≃ p ^ (w * x + y * z)
multi_compat : ∀ {w x y z : ℕ}, Coe.coe (w * x + y * z) ≃ Coe.coe w * Coe.coe x + Coe.coe y * Coe.coe z
w x y z : ℤ
⊢ (w - x) * (y - z) ≃ w * y + x * z - (x * y + w * z)
Tactic:
let wy := w*y
Proof state after:
ℕ ℤ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
ℚ : Type
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Natural.Exponentiation ℕ fun x x_1 => x * x_1
inst✝¹ : Exponentiation ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
a b : ℤ
n m : ℕ
a_eqv : a ≃ Coe.coe n - Coe.coe m
k j : ℕ
b_eqv : b ≃ Coe.coe k - Coe.coe j
pow_expand : (p ^ a) ^ b ≃ (p ^ n) ^ k / (p ^ m) ^ k / ((p ^ n) ^ j / (p ^ m) ^ j)
pow_combine : ∀ {w x y z : ℕ}, (p ^ w) ^ x * (p ^ y) ^ z ≃ p ^ (w * x + y * z)
multi_compat : ∀ {w x y z : ℕ}, Coe.coe (w * x + y * z) ≃ Coe.coe w * Coe.coe x + Coe.coe y * Coe.coe z
w x y z : ℤ
wy : ℤ := w * y
⊢ (w - x) * (y - z) ≃ w * y + x * z - (x * y + w * z)
Theorem: Lean4Axiomatic.Rational.pow_flatten
Proof state before:
ℕ ℤ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
ℚ : Type
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Natural.Exponentiation ℕ fun x x_1 => x * x_1
inst✝¹ : Exponentiation ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
a b : ℤ
n m : ℕ
a_eqv : a ≃ Coe.coe n - Coe.coe m
k j : ℕ
b_eqv : b ≃ Coe.coe k - Coe.coe j
pow_expand : (p ^ a) ^ b ≃ (p ^ n) ^ k / (p ^ m) ^ k / ((p ^ n) ^ j / (p ^ m) ^ j)
pow_combine : ∀ {w x y z : ℕ}, (p ^ w) ^ x * (p ^ y) ^ z ≃ p ^ (w * x + y * z)
multi_compat : ∀ {w x y z : ℕ}, Coe.coe (w * x + y * z) ≃ Coe.coe w * Coe.coe x + Coe.coe y * Coe.coe z
w x y z : ℤ
wy : ℤ := w * y
⊢ (w - x) * (y - z) ≃ w * y + x * z - (x * y + w * z)
Tactic:
let wz := w*z
Proof state after:
ℕ ℤ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
ℚ : Type
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Natural.Exponentiation ℕ fun x x_1 => x * x_1
inst✝¹ : Exponentiation ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
a b : ℤ
n m : ℕ
a_eqv : a ≃ Coe.coe n - Coe.coe m
k j : ℕ
b_eqv : b ≃ Coe.coe k - Coe.coe j
pow_expand : (p ^ a) ^ b ≃ (p ^ n) ^ k / (p ^ m) ^ k / ((p ^ n) ^ j / (p ^ m) ^ j)
pow_combine : ∀ {w x y z : ℕ}, (p ^ w) ^ x * (p ^ y) ^ z ≃ p ^ (w * x + y * z)
multi_compat : ∀ {w x y z : ℕ}, Coe.coe (w * x + y * z) ≃ Coe.coe w * Coe.coe x + Coe.coe y * Coe.coe z
w x y z : ℤ
wy : ℤ := w * y
wz : ℤ := w * z
⊢ (w - x) * (y - z) ≃ w * y + x * z - (x * y + w * z)
Theorem: Lean4Axiomatic.Rational.pow_flatten
Proof state before:
ℕ ℤ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
ℚ : Type
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Natural.Exponentiation ℕ fun x x_1 => x * x_1
inst✝¹ : Exponentiation ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
a b : ℤ
n m : ℕ
a_eqv : a ≃ Coe.coe n - Coe.coe m
k j : ℕ
b_eqv : b ≃ Coe.coe k - Coe.coe j
pow_expand : (p ^ a) ^ b ≃ (p ^ n) ^ k / (p ^ m) ^ k / ((p ^ n) ^ j / (p ^ m) ^ j)
pow_combine : ∀ {w x y z : ℕ}, (p ^ w) ^ x * (p ^ y) ^ z ≃ p ^ (w * x + y * z)
multi_compat : ∀ {w x y z : ℕ}, Coe.coe (w * x + y * z) ≃ Coe.coe w * Coe.coe x + Coe.coe y * Coe.coe z
w x y z : ℤ
wy : ℤ := w * y
wz : ℤ := w * z
⊢ (w - x) * (y - z) ≃ w * y + x * z - (x * y + w * z)
Tactic:
let xy := x*y
Proof state after:
ℕ ℤ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
ℚ : Type
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Natural.Exponentiation ℕ fun x x_1 => x * x_1
inst✝¹ : Exponentiation ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
a b : ℤ
n m : ℕ
a_eqv : a ≃ Coe.coe n - Coe.coe m
k j : ℕ
b_eqv : b ≃ Coe.coe k - Coe.coe j
pow_expand : (p ^ a) ^ b ≃ (p ^ n) ^ k / (p ^ m) ^ k / ((p ^ n) ^ j / (p ^ m) ^ j)
pow_combine : ∀ {w x y z : ℕ}, (p ^ w) ^ x * (p ^ y) ^ z ≃ p ^ (w * x + y * z)
multi_compat : ∀ {w x y z : ℕ}, Coe.coe (w * x + y * z) ≃ Coe.coe w * Coe.coe x + Coe.coe y * Coe.coe z
w x y z : ℤ
wy : ℤ := w * y
wz : ℤ := w * z
xy : ℤ := x * y
⊢ (w - x) * (y - z) ≃ w * y + x * z - (x * y + w * z)
Theorem: Lean4Axiomatic.Rational.pow_flatten
Proof state before:
ℕ ℤ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
ℚ : Type
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Natural.Exponentiation ℕ fun x x_1 => x * x_1
inst✝¹ : Exponentiation ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
a b : ℤ
n m : ℕ
a_eqv : a ≃ Coe.coe n - Coe.coe m
k j : ℕ
b_eqv : b ≃ Coe.coe k - Coe.coe j
pow_expand : (p ^ a) ^ b ≃ (p ^ n) ^ k / (p ^ m) ^ k / ((p ^ n) ^ j / (p ^ m) ^ j)
pow_combine : ∀ {w x y z : ℕ}, (p ^ w) ^ x * (p ^ y) ^ z ≃ p ^ (w * x + y * z)
multi_compat : ∀ {w x y z : ℕ}, Coe.coe (w * x + y * z) ≃ Coe.coe w * Coe.coe x + Coe.coe y * Coe.coe z
w x y z : ℤ
wy : ℤ := w * y
wz : ℤ := w * z
xy : ℤ := x * y
⊢ (w - x) * (y - z) ≃ w * y + x * z - (x * y + w * z)
Tactic:
let xz := x*z
Proof state after:
ℕ ℤ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
ℚ : Type
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Natural.Exponentiation ℕ fun x x_1 => x * x_1
inst✝¹ : Exponentiation ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
a b : ℤ
n m : ℕ
a_eqv : a ≃ Coe.coe n - Coe.coe m
k j : ℕ
b_eqv : b ≃ Coe.coe k - Coe.coe j
pow_expand : (p ^ a) ^ b ≃ (p ^ n) ^ k / (p ^ m) ^ k / ((p ^ n) ^ j / (p ^ m) ^ j)
pow_combine : ∀ {w x y z : ℕ}, (p ^ w) ^ x * (p ^ y) ^ z ≃ p ^ (w * x + y * z)
multi_compat : ∀ {w x y z : ℕ}, Coe.coe (w * x + y * z) ≃ Coe.coe w * Coe.coe x + Coe.coe y * Coe.coe z
w x y z : ℤ
wy : ℤ := w * y
wz : ℤ := w * z
xy : ℤ := x * y
xz : ℤ := x * z
⊢ (w - x) * (y - z) ≃ w * y + x * z - (x * y + w * z)
Theorem: Lean4Axiomatic.Rational.pow_flatten
Proof state before:
ℕ ℤ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
ℚ : Type
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Natural.Exponentiation ℕ fun x x_1 => x * x_1
inst✝¹ : Exponentiation ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
a b : ℤ
n m : ℕ
a_eqv : a ≃ Coe.coe n - Coe.coe m
k j : ℕ
b_eqv : b ≃ Coe.coe k - Coe.coe j
pow_expand : (p ^ a) ^ b ≃ (p ^ n) ^ k / (p ^ m) ^ k / ((p ^ n) ^ j / (p ^ m) ^ j)
pow_combine : ∀ {w x y z : ℕ}, (p ^ w) ^ x * (p ^ y) ^ z ≃ p ^ (w * x + y * z)
multi_compat : ∀ {w x y z : ℕ}, Coe.coe (w * x + y * z) ≃ Coe.coe w * Coe.coe x + Coe.coe y * Coe.coe z
w x y z : ℤ
wy : ℤ := w * y
wz : ℤ := w * z
xy : ℤ := x * y
xz : ℤ := x * z
⊢ (w - x) * (y - z) ≃ w * y + x * z - (x * y + w * z)
Tactic:
calc
  _ = (w-x) * (y-z)           := rfl
  _ ≃ w * (y-z) - x * (y-z)   := AA.distribR
  _ ≃ (wy - wz) - x * (y-z)   := AA.substL AA.distribL
  _ ≃ (wy - wz) - (xy - xz)   := AA.substR AA.distribL
  _ ≃ (wy - wz) + -(xy - xz)  := Integer.sub_defn
  _ ≃ (wy - wz) + (xz - xy)   := AA.substR Integer.sub_neg_flip
  _ ≃ (wy + -wz) + (xz - xy)  := AA.substL Integer.sub_defn
  _ ≃ (wy + -wz) + (xz + -xy) := AA.substR Integer.sub_defn
  _ ≃ (wy + xz) + (-wz + -xy) := AA.expr_xxfxxff_lr_swap_rl
  _ ≃ (wy + xz) + (-xy + -wz) := AA.substR AA.comm
  _ ≃ (wy + xz) + -(xy + wz)  := AA.substR (Rel.symm Integer.neg_compat_add)
  _ ≃ (wy + xz) - (xy + wz)   := Rel.symm Integer.sub_defn
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.pow_distribR_mul
Proof state before:
ℕ ℤ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
ℚ : Type
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Multiplication ℚ
inst✝⁷ : Negation ℚ
inst✝⁶ : Reciprocation ℚ
inst✝⁵ : Division ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
inst✝² : Exponentiation ℚ
p q : ℚ
inst✝¹ : AP (p ≄ 0)
inst✝ : AP (q ≄ 0)
a : ℤ
⊢ (p * q) ^ a ≃ p ^ a * q ^ a
Tactic:
have Exists.intro (n : ℕ) (Exists.intro (m : ℕ) (a_eqv : a ≃ n - m)) :=
  Integer.as_diff a
Proof state after:
ℕ ℤ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
ℚ : Type
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Multiplication ℚ
inst✝⁷ : Negation ℚ
inst✝⁶ : Reciprocation ℚ
inst✝⁵ : Division ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
inst✝² : Exponentiation ℚ
p q : ℚ
inst✝¹ : AP (p ≄ 0)
inst✝ : AP (q ≄ 0)
a : ℤ
n m : ℕ
a_eqv : a ≃ Coe.coe n - Coe.coe m
⊢ (p * q) ^ a ≃ p ^ a * q ^ a
Theorem: Lean4Axiomatic.Rational.pow_distribR_mul
Proof state before:
ℕ ℤ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
ℚ : Type
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Multiplication ℚ
inst✝⁷ : Negation ℚ
inst✝⁶ : Reciprocation ℚ
inst✝⁵ : Division ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
inst✝² : Exponentiation ℚ
p q : ℚ
inst✝¹ : AP (p ≄ 0)
inst✝ : AP (q ≄ 0)
a : ℤ
n m : ℕ
a_eqv : a ≃ Coe.coe n - Coe.coe m
⊢ (p * q) ^ a ≃ p ^ a * q ^ a
Tactic:
calc
  _ = (p * q)^a                 := rfl
  _ ≃ (p * q)^((n:ℤ)-m)         := pow_substR a_eqv
  _ ≃ (p * q)^n / (p * q)^m     := pow_diff
  _ ≃ (p^n * q^n) / (p * q)^m   := div_substL Natural.pow_distribR_mul
  _ ≃ (p^n * q^n) / (p^m * q^m) := div_substR Natural.pow_distribR_mul
  _ ≃ (p^n / p^m) * (q^n / q^m) := eqv_symm div_mul_swap
  _ ≃ p^((n:ℤ)-m) * (q^n / q^m) := mul_substL (eqv_symm pow_diff)
  _ ≃ p^((n:ℤ)-m) * q^((n:ℤ)-m) := mul_substR (eqv_symm pow_diff)
  _ ≃ p^a * q^((n:ℤ)-m)         := mul_substL (pow_substR (Rel.symm a_eqv))
  _ ≃ p^a * q^a                 := mul_substR (pow_substR (Rel.symm a_eqv))
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Generic.on_diff_subst_pow
Proof state before:
ℕ ℤ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Integer.Induction ℤ
ℚ : Type
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
inst✝ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
n₁ m₁ n₂ m₂ : ℕ
⊢ Coe.coe n₁ - Coe.coe m₁ ≃ Coe.coe n₂ - Coe.coe m₂ → on_diff_pow n₁ m₁ ≃ on_diff_pow n₂ m₂
Tactic:
intro (_ : (n₁:ℤ) - m₁ ≃ n₂ - m₂)
Proof state after:
ℕ ℤ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Integer.Induction ℤ
ℚ : Type
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
inst✝ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
n₁ m₁ n₂ m₂ : ℕ
x✝ : Coe.coe n₁ - Coe.coe m₁ ≃ Coe.coe n₂ - Coe.coe m₂
⊢ on_diff_pow n₁ m₁ ≃ on_diff_pow n₂ m₂
Theorem: Lean4Axiomatic.Rational.Impl.Generic.on_diff_subst_pow
Proof state before:
ℕ ℤ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Integer.Induction ℤ
ℚ : Type
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
inst✝ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
n₁ m₁ n₂ m₂ : ℕ
x✝ : Coe.coe n₁ - Coe.coe m₁ ≃ Coe.coe n₂ - Coe.coe m₂
⊢ on_diff_pow n₁ m₁ ≃ on_diff_pow n₂ m₂
Tactic:
intro (p : ℚ) (_ : AP (p ≄ 0))
Proof state after:
ℕ ℤ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Integer.Induction ℤ
ℚ : Type
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
inst✝ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
n₁ m₁ n₂ m₂ : ℕ
x✝¹ : Coe.coe n₁ - Coe.coe m₁ ≃ Coe.coe n₂ - Coe.coe m₂
p : ℚ
x✝ : AP (p ≄ 0)
⊢ on_diff_pow n₁ m₁ p ≃ on_diff_pow n₂ m₂ p
Theorem: Lean4Axiomatic.Rational.Impl.Generic.on_diff_subst_pow
Proof state before:
ℕ ℤ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Integer.Induction ℤ
ℚ : Type
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
inst✝ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
n₁ m₁ n₂ m₂ : ℕ
x✝¹ : Coe.coe n₁ - Coe.coe m₁ ≃ Coe.coe n₂ - Coe.coe m₂
p : ℚ
x✝ : AP (p ≄ 0)
⊢ on_diff_pow n₁ m₁ p ≃ on_diff_pow n₂ m₂ p
Tactic:
show p^n₁ / p^m₁ ≃ p^n₂ / p^m₂
Proof state after:
ℕ ℤ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Integer.Induction ℤ
ℚ : Type
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
inst✝ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
n₁ m₁ n₂ m₂ : ℕ
x✝¹ : Coe.coe n₁ - Coe.coe m₁ ≃ Coe.coe n₂ - Coe.coe m₂
p : ℚ
x✝ : AP (p ≄ 0)
⊢ p ^ n₁ / p ^ m₁ ≃ p ^ n₂ / p ^ m₂
Theorem: Lean4Axiomatic.Rational.Impl.Generic.on_diff_subst_pow
Proof state before:
ℕ ℤ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Integer.Induction ℤ
ℚ : Type
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
inst✝ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
n₁ m₁ n₂ m₂ : ℕ
x✝¹ : Coe.coe n₁ - Coe.coe m₁ ≃ Coe.coe n₂ - Coe.coe m₂
p : ℚ
x✝ : AP (p ≄ 0)
⊢ p ^ n₁ / p ^ m₁ ≃ p ^ n₂ / p ^ m₂
Tactic:
have pow_add_n₁m₂ : p^n₁ * p^m₂ ≃ p^(n₁ + m₂) :=
  Rel.symm Natural.pow_compatL_add
Proof state after:
ℕ ℤ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Integer.Induction ℤ
ℚ : Type
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
inst✝ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
n₁ m₁ n₂ m₂ : ℕ
x✝¹ : Coe.coe n₁ - Coe.coe m₁ ≃ Coe.coe n₂ - Coe.coe m₂
p : ℚ
x✝ : AP (p ≄ 0)
pow_add_n₁m₂ : p ^ n₁ * p ^ m₂ ≃ p ^ (n₁ + m₂)
⊢ p ^ n₁ / p ^ m₁ ≃ p ^ n₂ / p ^ m₂
Theorem: Lean4Axiomatic.Rational.Impl.Generic.on_diff_subst_pow
Proof state before:
ℕ ℤ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Integer.Induction ℤ
ℚ : Type
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
inst✝ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
n₁ m₁ n₂ m₂ : ℕ
x✝¹ : Coe.coe n₁ - Coe.coe m₁ ≃ Coe.coe n₂ - Coe.coe m₂
p : ℚ
x✝ : AP (p ≄ 0)
pow_add_n₁m₂ : p ^ n₁ * p ^ m₂ ≃ p ^ (n₁ + m₂)
⊢ p ^ n₁ / p ^ m₁ ≃ p ^ n₂ / p ^ m₂
Tactic:
have pow_add_m₁n₂ : p^m₁ * p^n₂ ≃ p^(m₁ + n₂) :=
  Rel.symm Natural.pow_compatL_add
Proof state after:
ℕ ℤ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Integer.Induction ℤ
ℚ : Type
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
inst✝ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
n₁ m₁ n₂ m₂ : ℕ
x✝¹ : Coe.coe n₁ - Coe.coe m₁ ≃ Coe.coe n₂ - Coe.coe m₂
p : ℚ
x✝ : AP (p ≄ 0)
pow_add_n₁m₂ : p ^ n₁ * p ^ m₂ ≃ p ^ (n₁ + m₂)
pow_add_m₁n₂ : p ^ m₁ * p ^ n₂ ≃ p ^ (m₁ + n₂)
⊢ p ^ n₁ / p ^ m₁ ≃ p ^ n₂ / p ^ m₂
Theorem: Lean4Axiomatic.Rational.Impl.Generic.on_diff_subst_pow
Proof state before:
ℕ ℤ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Integer.Induction ℤ
ℚ : Type
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
inst✝ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
n₁ m₁ n₂ m₂ : ℕ
x✝¹ : Coe.coe n₁ - Coe.coe m₁ ≃ Coe.coe n₂ - Coe.coe m₂
p : ℚ
x✝ : AP (p ≄ 0)
pow_add_n₁m₂ : p ^ n₁ * p ^ m₂ ≃ p ^ (n₁ + m₂)
pow_add_m₁n₂ : p ^ m₁ * p ^ n₂ ≃ p ^ (m₁ + n₂)
⊢ p ^ n₁ / p ^ m₁ ≃ p ^ n₂ / p ^ m₂
Tactic:
have : (n₁:ℤ) + m₂ ≃ n₂ + m₁ :=
  Integer.sub_swap_add.mp ‹(n₁:ℤ) - m₁ ≃ n₂ - m₂›
Proof state after:
ℕ ℤ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Integer.Induction ℤ
ℚ : Type
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
inst✝ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
n₁ m₁ n₂ m₂ : ℕ
x✝¹ : Coe.coe n₁ - Coe.coe m₁ ≃ Coe.coe n₂ - Coe.coe m₂
p : ℚ
x✝ : AP (p ≄ 0)
pow_add_n₁m₂ : p ^ n₁ * p ^ m₂ ≃ p ^ (n₁ + m₂)
pow_add_m₁n₂ : p ^ m₁ * p ^ n₂ ≃ p ^ (m₁ + n₂)
this : Coe.coe n₁ + Coe.coe m₂ ≃ Coe.coe n₂ + Coe.coe m₁
⊢ p ^ n₁ / p ^ m₁ ≃ p ^ n₂ / p ^ m₂
Theorem: Lean4Axiomatic.Rational.Impl.Generic.on_diff_subst_pow
Proof state before:
ℕ ℤ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Integer.Induction ℤ
ℚ : Type
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
inst✝ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
n₁ m₁ n₂ m₂ : ℕ
x✝¹ : Coe.coe n₁ - Coe.coe m₁ ≃ Coe.coe n₂ - Coe.coe m₂
p : ℚ
x✝ : AP (p ≄ 0)
pow_add_n₁m₂ : p ^ n₁ * p ^ m₂ ≃ p ^ (n₁ + m₂)
pow_add_m₁n₂ : p ^ m₁ * p ^ n₂ ≃ p ^ (m₁ + n₂)
this : Coe.coe n₁ + Coe.coe m₂ ≃ Coe.coe n₂ + Coe.coe m₁
⊢ p ^ n₁ / p ^ m₁ ≃ p ^ n₂ / p ^ m₂
Tactic:
have : ((n₁ + m₂:ℕ):ℤ) ≃ ((m₁ + n₂:ℕ):ℤ) := calc
  _ = ((n₁ + m₂:ℕ):ℤ) := rfl
  _ ≃ (n₁:ℤ) + m₂     := AA.compat₂
  _ ≃ n₂ + m₁         := ‹(n₁:ℤ) + m₂ ≃ n₂ + m₁›
  _ ≃ m₁ + n₂         := AA.comm
  _ ≃ ((m₁ + n₂:ℕ):ℤ) := Rel.symm AA.compat₂
Proof state after:
ℕ ℤ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Integer.Induction ℤ
ℚ : Type
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
inst✝ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
n₁ m₁ n₂ m₂ : ℕ
x✝¹ : Coe.coe n₁ - Coe.coe m₁ ≃ Coe.coe n₂ - Coe.coe m₂
p : ℚ
x✝ : AP (p ≄ 0)
pow_add_n₁m₂ : p ^ n₁ * p ^ m₂ ≃ p ^ (n₁ + m₂)
pow_add_m₁n₂ : p ^ m₁ * p ^ n₂ ≃ p ^ (m₁ + n₂)
this✝ : Coe.coe n₁ + Coe.coe m₂ ≃ Coe.coe n₂ + Coe.coe m₁
this : Coe.coe (n₁ + m₂) ≃ Coe.coe (m₁ + n₂)
⊢ p ^ n₁ / p ^ m₁ ≃ p ^ n₂ / p ^ m₂
Theorem: Lean4Axiomatic.Rational.Impl.Generic.on_diff_subst_pow
Proof state before:
ℕ ℤ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Integer.Induction ℤ
ℚ : Type
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
inst✝ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
n₁ m₁ n₂ m₂ : ℕ
x✝¹ : Coe.coe n₁ - Coe.coe m₁ ≃ Coe.coe n₂ - Coe.coe m₂
p : ℚ
x✝ : AP (p ≄ 0)
pow_add_n₁m₂ : p ^ n₁ * p ^ m₂ ≃ p ^ (n₁ + m₂)
pow_add_m₁n₂ : p ^ m₁ * p ^ n₂ ≃ p ^ (m₁ + n₂)
this✝ : Coe.coe n₁ + Coe.coe m₂ ≃ Coe.coe n₂ + Coe.coe m₁
this : Coe.coe (n₁ + m₂) ≃ Coe.coe (m₁ + n₂)
⊢ p ^ n₁ / p ^ m₁ ≃ p ^ n₂ / p ^ m₂
Tactic:
have : n₁ + m₂ ≃ m₁ + n₂ := AA.inject this
Proof state after:
ℕ ℤ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Integer.Induction ℤ
ℚ : Type
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
inst✝ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
n₁ m₁ n₂ m₂ : ℕ
x✝¹ : Coe.coe n₁ - Coe.coe m₁ ≃ Coe.coe n₂ - Coe.coe m₂
p : ℚ
x✝ : AP (p ≄ 0)
pow_add_n₁m₂ : p ^ n₁ * p ^ m₂ ≃ p ^ (n₁ + m₂)
pow_add_m₁n₂ : p ^ m₁ * p ^ n₂ ≃ p ^ (m₁ + n₂)
this✝¹ : Coe.coe n₁ + Coe.coe m₂ ≃ Coe.coe n₂ + Coe.coe m₁
this✝ : Coe.coe (n₁ + m₂) ≃ Coe.coe (m₁ + n₂)
this : n₁ + m₂ ≃ m₁ + n₂
⊢ p ^ n₁ / p ^ m₁ ≃ p ^ n₂ / p ^ m₂