internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Rational.pow_substL
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₁ p₂ : ℚ
a : ℤ
inst✝¹ : AP (p₁ ≄ 0)
inst✝ : AP (p₂ ≄ 0)
x✝ : p₁ ≃ p₂
⊢ p₁ ^ a ≃ p₂ ^ a
Tactic:
have Exists.intro (n : ℕ) (Exists.intro (m : ℕ) (_ : 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₁ p₂ : ℚ
a : ℤ
inst✝¹ : AP (p₁ ≄ 0)
inst✝ : AP (p₂ ≄ 0)
x✝ : p₁ ≃ p₂
n m : ℕ
h✝ : a ≃ Coe.coe n - Coe.coe m
⊢ p₁ ^ a ≃ p₂ ^ a
Theorem: Lean4Axiomatic.Rational.pow_substL
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₁ p₂ : ℚ
a : ℤ
inst✝¹ : AP (p₁ ≄ 0)
inst✝ : AP (p₂ ≄ 0)
x✝ : p₁ ≃ p₂
n m : ℕ
h✝ : a ≃ Coe.coe n - Coe.coe m
⊢ p₁ ^ a ≃ p₂ ^ a
Tactic:
calc
  _ = p₁^a           := rfl
  _ ≃ p₁^((n:ℤ) - m) := pow_substR ‹a ≃ n - m›
  _ ≃ p₁^n / p₁^m    := pow_diff
  _ ≃ p₂^n / p₁^m    := div_substL (Natural.pow_substL ‹p₁ ≃ p₂›)
  _ ≃ p₂^n / p₂^m    := div_substR (Natural.pow_substL ‹p₁ ≃ p₂›)
  _ ≃ p₂^((n:ℤ) - m) := eqv_symm pow_diff
  _ ≃ p₂^a           := pow_substR (Rel.symm ‹a ≃ n - m›)
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.pow_preserves_nonzero
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 : ℚ
a : ℤ
inst✝ : AP (p ≄ 0)
⊢ p ^ a ≄ 0
Tactic:
intro (_ : p^a ≃ 0)
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 : ℚ
a : ℤ
inst✝ : AP (p ≄ 0)
x✝ : p ^ a ≃ 0
⊢ False
Theorem: Lean4Axiomatic.Rational.pow_preserves_nonzero
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 : ℚ
a : ℤ
inst✝ : AP (p ≄ 0)
x✝ : p ^ a ≃ 0
⊢ False
Tactic:
have Exists.intro (n : ℕ) (Exists.intro (m : ℕ) (_ : 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 : ℚ
a : ℤ
inst✝ : AP (p ≄ 0)
x✝ : p ^ a ≃ 0
n m : ℕ
h✝ : a ≃ Coe.coe n - Coe.coe m
⊢ False
Theorem: Lean4Axiomatic.Rational.pow_preserves_nonzero
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 : ℚ
a : ℤ
inst✝ : AP (p ≄ 0)
x✝ : p ^ a ≃ 0
n m : ℕ
h✝ : a ≃ Coe.coe n - Coe.coe m
⊢ False
Tactic:
have : p^n / p^m ≃ 0 := calc
  _ = p^n / p^m     := rfl
  _ ≃ p^((n:ℤ) - m) := eqv_symm pow_diff
  _ ≃ p^a           := pow_substR (Rel.symm ‹a ≃ n - m›)
  _ ≃ 0             := ‹p^a ≃ 0›
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 : ℚ
a : ℤ
inst✝ : AP (p ≄ 0)
x✝ : p ^ a ≃ 0
n m : ℕ
h✝ : a ≃ Coe.coe n - Coe.coe m
this : p ^ n / p ^ m ≃ 0
⊢ False
Theorem: Lean4Axiomatic.Rational.pow_preserves_nonzero
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 : ℚ
a : ℤ
inst✝ : AP (p ≄ 0)
x✝ : p ^ a ≃ 0
n m : ℕ
h✝ : a ≃ Coe.coe n - Coe.coe m
this : p ^ n / p ^ m ≃ 0
⊢ False
Tactic:
have : p^n ≃ 0 := div_eqv_0.mp this
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 : ℚ
a : ℤ
inst✝ : AP (p ≄ 0)
x✝ : p ^ a ≃ 0
n m : ℕ
h✝ : a ≃ Coe.coe n - Coe.coe m
this✝ : p ^ n / p ^ m ≃ 0
this : p ^ n ≃ 0
⊢ False
Theorem: Lean4Axiomatic.Rational.pow_preserves_nonzero
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 : ℚ
a : ℤ
inst✝ : AP (p ≄ 0)
x✝ : p ^ a ≃ 0
n m : ℕ
h✝ : a ≃ Coe.coe n - Coe.coe m
this✝ : p ^ n / p ^ m ≃ 0
this : p ^ n ≃ 0
⊢ False
Tactic:
have : p^n ≄ 0 := Natural.pow_preserves_nonzero_base ‹AP (p ≄ 0)›.ev
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 : ℚ
a : ℤ
inst✝ : AP (p ≄ 0)
x✝ : p ^ a ≃ 0
n m : ℕ
h✝ : a ≃ Coe.coe n - Coe.coe m
this✝¹ : p ^ n / p ^ m ≃ 0
this✝ : p ^ n ≃ 0
this : p ^ n ≄ 0
⊢ False
Theorem: Lean4Axiomatic.Rational.pow_preserves_nonzero
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 : ℚ
a : ℤ
inst✝ : AP (p ≄ 0)
x✝ : p ^ a ≃ 0
n m : ℕ
h✝ : a ≃ Coe.coe n - Coe.coe m
this✝¹ : p ^ n / p ^ m ≃ 0
this✝ : p ^ n ≃ 0
this : p ^ n ≄ 0
⊢ False
Tactic:
exact absurd ‹p^n ≃ 0› ‹p^n ≄ 0›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.pow_compatL_add
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 : ℤ
⊢ p ^ (a + b) ≃ p ^ a * p ^ b
Tactic:
have Exists.intro (n : ℕ) (Exists.intro (m : ℕ) (_ : 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 : ℚ
inst✝ : AP (p ≄ 0)
a b : ℤ
n m : ℕ
h✝ : a ≃ Coe.coe n - Coe.coe m
⊢ p ^ (a + b) ≃ p ^ a * p ^ b
Theorem: Lean4Axiomatic.Rational.pow_compatL_add
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 : ℕ
h✝ : a ≃ Coe.coe n - Coe.coe m
⊢ p ^ (a + b) ≃ p ^ a * p ^ b
Tactic:
have Exists.intro (k : ℕ) (Exists.intro (j : ℕ) (_ : b ≃ k - j)) :=
  Integer.as_diff b
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 : ℕ
h✝¹ : a ≃ Coe.coe n - Coe.coe m
k j : ℕ
h✝ : b ≃ Coe.coe k - Coe.coe j
⊢ p ^ (a + b) ≃ p ^ a * p ^ b
Theorem: Lean4Axiomatic.Rational.pow_compatL_add
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 : ℕ
h✝¹ : a ≃ Coe.coe n - Coe.coe m
k j : ℕ
h✝ : b ≃ Coe.coe k - Coe.coe j
⊢ p ^ (a + b) ≃ p ^ a * p ^ b
Tactic:
have : a + b ≃ (n + k : ℕ) - (m + j : ℕ) := calc
  _ = a + b                     := rfl
  _ ≃ (n - m) + b               := AA.substL ‹a ≃ n - m›
  _ ≃ (n - m) + (k - j)         := AA.substR ‹b ≃ k - j›
  _ ≃ (n + k) - (m + j)         := Integer.sub_xchg_add
  _ ≃ (n + k : ℕ) - (m + j)     := AA.substL (Rel.symm AA.compat₂)
  _ ≃ (n + k : ℕ) - (m + j : ℕ) := AA.substR (Rel.symm AA.compat₂)
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 : ℕ
h✝¹ : a ≃ Coe.coe n - Coe.coe m
k j : ℕ
h✝ : b ≃ Coe.coe k - Coe.coe j
this : a + b ≃ Coe.coe (n + k) - Coe.coe (m + j)
⊢ p ^ (a + b) ≃ p ^ a * p ^ b
Theorem: Lean4Axiomatic.Rational.pow_compatL_add
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 : ℕ
h✝¹ : a ≃ Coe.coe n - Coe.coe m
k j : ℕ
h✝ : b ≃ Coe.coe k - Coe.coe j
this : a + b ≃ Coe.coe (n + k) - Coe.coe (m + j)
⊢ p ^ (a + b) ≃ p ^ a * p ^ b
Tactic:
have pow_lift {x y : ℕ} {z : ℤ} : z ≃ x - y → p^x / p^y ≃ p^z := by
  intro (_ : z ≃ x - y)
  calc
    _ = p^x / p^y     := rfl
    _ ≃ p^((x:ℤ) - y) := eqv_symm pow_diff
    _ ≃ p^z           := pow_substR (Rel.symm ‹z ≃ 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 : ℕ
h✝¹ : a ≃ Coe.coe n - Coe.coe m
k j : ℕ
h✝ : b ≃ Coe.coe k - Coe.coe j
this : a + b ≃ Coe.coe (n + k) - Coe.coe (m + j)
pow_lift : ∀ {x y : ℕ} {z : ℤ}, z ≃ Coe.coe x - Coe.coe y → p ^ x / p ^ y ≃ p ^ z
⊢ p ^ (a + b) ≃ p ^ a * p ^ b
Theorem: Lean4Axiomatic.Rational.pow_compatL_add
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 : ℕ
h✝¹ : a ≃ Coe.coe n - Coe.coe m
k j : ℕ
h✝ : b ≃ Coe.coe k - Coe.coe j
this : a + b ≃ Coe.coe (n + k) - Coe.coe (m + j)
pow_lift : ∀ {x y : ℕ} {z : ℤ}, z ≃ Coe.coe x - Coe.coe y → p ^ x / p ^ y ≃ p ^ z
⊢ p ^ (a + b) ≃ p ^ a * p ^ b
Tactic:
calc
  _ = p^(a + b)                         := rfl
  _ ≃ p^(((n + k : ℕ):ℤ) - (m + j : ℕ)) := pow_substR ‹a+b ≃ (n+k:ℕ)-(m+j:ℕ)›
  _ ≃ p^(n + k) / p^(m + j)             := pow_diff
  _ ≃ (p^n * p^k) / p^(m + j)           := div_substL Natural.pow_compatL_add
  _ ≃ (p^n * p^k) / (p^m * p^j)         := div_substR Natural.pow_compatL_add
  _ ≃ (p^n / p^m) * (p^k / p^j)         := Rel.symm div_mul_swap
  _ ≃ p^a * (p^k / p^j)                 := mul_substL (pow_lift ‹a ≃ n - m›)
  _ ≃ p^a * p^b                         := mul_substR (pow_lift ‹b ≃ k - j›)
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.pow_compatL_add
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 : ℕ
h✝¹ : a ≃ Coe.coe n - Coe.coe m
k j : ℕ
h✝ : b ≃ Coe.coe k - Coe.coe j
this : a + b ≃ Coe.coe (n + k) - Coe.coe (m + j)
x y : ℕ
z : ℤ
⊢ z ≃ Coe.coe x - Coe.coe y → p ^ x / p ^ y ≃ p ^ z
Tactic:
intro (_ : z ≃ 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 : ℕ
h✝¹ : a ≃ Coe.coe n - Coe.coe m
k j : ℕ
h✝ : b ≃ Coe.coe k - Coe.coe j
this : a + b ≃ Coe.coe (n + k) - Coe.coe (m + j)
x y : ℕ
z : ℤ
x✝ : z ≃ Coe.coe x - Coe.coe y
⊢ p ^ x / p ^ y ≃ p ^ z
Theorem: Lean4Axiomatic.Rational.pow_compatL_add
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 : ℕ
h✝¹ : a ≃ Coe.coe n - Coe.coe m
k j : ℕ
h✝ : b ≃ Coe.coe k - Coe.coe j
this : a + b ≃ Coe.coe (n + k) - Coe.coe (m + j)
x y : ℕ
z : ℤ
x✝ : z ≃ Coe.coe x - Coe.coe y
⊢ p ^ x / p ^ y ≃ p ^ z
Tactic:
calc
  _ = p^x / p^y     := rfl
  _ ≃ p^((x:ℤ) - y) := eqv_symm pow_diff
  _ ≃ p^z           := pow_substR (Rel.symm ‹z ≃ x - y›)
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 : ℤ
⊢ (p ^ a) ^ b ≃ p ^ (a * b)
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 : ℚ
inst✝ : AP (p ≄ 0)
a b : ℤ
n m : ℕ
a_eqv : a ≃ Coe.coe n - Coe.coe m
⊢ (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
⊢ (p ^ a) ^ b ≃ p ^ (a * b)
Tactic:
have Exists.intro (k : ℕ) (Exists.intro (j : ℕ) (b_eqv : b ≃ k - j)) :=
  Integer.as_diff b
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
⊢ (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
⊢ (p ^ a) ^ b ≃ p ^ (a * b)
Tactic:
have pow_expand : (p^a)^b ≃ ((p^n)^k/(p^m)^k) / ((p^n)^j/(p^m)^j) := calc
  _ = (p^a)^b                               := rfl
  _ ≃ (p^((n:ℤ)-m))^b                       := pow_substL (pow_substR a_eqv)
  _ ≃ (p^n/p^m)^b                           := pow_substL pow_diff
  _ ≃ (p^n/p^m)^((k:ℤ)-j)                   := pow_substR b_eqv
  _ ≃ (p^n/p^m)^k / (p^n/p^m)^j             := pow_diff
  _ ≃ ((p^n)^k/(p^m)^k) / (p^n/p^m)^j       := div_substL pow_distribR_div
  _ ≃ ((p^n)^k/(p^m)^k) / ((p^n)^j/(p^m)^j) := div_substR pow_distribR_div
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)
⊢ (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)
⊢ (p ^ a) ^ b ≃ p ^ (a * b)
Tactic:
have pow_combine {w x y z : ℕ} : (p^w)^x*(p^y)^z ≃ p^(w*x + y*z) := calc
  _ = (p^w)^x*(p^y)^z := rfl
  _ ≃ p^(w*x)*(p^y)^z := mul_substL Natural.pow_flatten
  _ ≃ p^(w*x)*p^(y*z) := mul_substR Natural.pow_flatten
  _ ≃ p^(w*x + y*z)   := Rel.symm Natural.pow_compatL_add
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)
⊢ (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)
⊢ (p ^ a) ^ b ≃ p ^ (a * b)
Tactic:
have multi_compat {w x y z : ℕ} : ((w*x + y*z : ℕ):ℤ) ≃ (w:ℤ)*x + y*z := calc
  _ = ((w*x + y*z : ℕ):ℤ)           := rfl
  _ ≃ ((w*x : ℕ):ℤ) + ((y*z : ℕ):ℤ) := AA.compat₂
  _ ≃ (w:ℤ)*x + ((y*z : ℕ):ℤ)       := AA.substL AA.compat₂
  _ ≃ (w:ℤ)*x + y*z                 := AA.substR AA.compat₂
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
⊢ (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
⊢ (p ^ a) ^ b ≃ p ^ (a * b)
Tactic:
have diff_expand
    {w x y z : ℤ} : (w-x) * (y-z) ≃ (w*y + x*z) - (x*y + w*z)
    := by
  let wy := w*y; let wz := w*z; let xy := x*y; let xz := x*z
  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:
ℕ ℤ : 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)