Theorem: Lean4Axiomatic.Rational.pow_compatL_add (Lean4Axiomatic/Rational/Exponentiation.lean)

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
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

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
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

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₂)
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

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›)
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

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›)
State after:
no goals

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)
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

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›)
State after:
no goals