Theorem: Lean4Axiomatic.Rational.pow_substL (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₁ p₂ : ℚ
a : ℤ
inst✝¹ : AP (p₁ ≄ 0)
inst✝ : AP (p₂ ≄ 0)
⊢ p₁ ≃ p₂ → p₁ ^ a ≃ p₂ ^ a
Tactic:
intro (_ : p₁ ≃ p₂)
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₂
⊢ p₁ ^ a ≃ p₂ ^ a

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

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