Theorem: Lean4Axiomatic.Rational.Impl.Generic.on_diff_subst_pow (Lean4Axiomatic/Rational/Impl/Generic/Exponentiation.lean)

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

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

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

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

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

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

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

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

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₂)
this : n₁ + m₂ ≃ m₁ + n₂
⊢ p ^ n₁ / p ^ m₁ ≃ p ^ n₂ / p ^ m₂
Tactic:
have pow_add_subst : p^(n₁ + m₂) ≃ p^(m₁ + n₂) := Natural.pow_substR this
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₂
pow_add_subst : p ^ (n₁ + m₂) ≃ p ^ (m₁ + n₂)
⊢ p ^ n₁ / p ^ m₁ ≃ p ^ n₂ / p ^ m₂

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₂)
this : n₁ + m₂ ≃ m₁ + n₂
pow_add_subst : p ^ (n₁ + m₂) ≃ p ^ (m₁ + n₂)
⊢ p ^ n₁ / p ^ m₁ ≃ p ^ n₂ / p ^ m₂
Tactic:
have : (p^n₁ / p^m₁) / (p^n₂ / p^m₂) ≃ 1 := calc
  _ = (p^n₁ / p^m₁) / (p^n₂ / p^m₂) := rfl
  _ ≃ (p^n₁ * p^m₂) / (p^m₁ * p^n₂) := div_div_div
  _ ≃ p^(n₁ + m₂) / (p^m₁ * p^n₂)   := div_substL pow_add_n₁m₂
  _ ≃ p^(n₁ + m₂) / p^(m₁ + n₂)     := div_substR pow_add_m₁n₂
  _ ≃ p^(m₁ + n₂) / p^(m₁ + n₂)     := div_substL pow_add_subst
  _ ≃ 1                             := div_same
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₂
pow_add_subst : p ^ (n₁ + m₂) ≃ p ^ (m₁ + n₂)
this : p ^ n₁ / p ^ m₁ / (p ^ n₂ / p ^ m₂) ≃ 1
⊢ p ^ n₁ / p ^ m₁ ≃ p ^ n₂ / p ^ m₂

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₂)
this✝ : n₁ + m₂ ≃ m₁ + n₂
pow_add_subst : p ^ (n₁ + m₂) ≃ p ^ (m₁ + n₂)
this : p ^ n₁ / p ^ m₁ / (p ^ n₂ / p ^ m₂) ≃ 1
⊢ p ^ n₁ / p ^ m₁ ≃ p ^ n₂ / p ^ m₂
Tactic:
have : p^n₁ / p^m₁ ≃ p^n₂ / p^m₂ := div_eqv_1.mp this
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₂
pow_add_subst : p ^ (n₁ + m₂) ≃ p ^ (m₁ + n₂)
this✝ : p ^ n₁ / p ^ m₁ / (p ^ n₂ / p ^ m₂) ≃ 1
this : p ^ n₁ / p ^ m₁ ≃ p ^ n₂ / p ^ m₂
⊢ p ^ n₁ / p ^ m₁ ≃ p ^ n₂ / p ^ m₂

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₂)
this✝¹ : n₁ + m₂ ≃ m₁ + n₂
pow_add_subst : p ^ (n₁ + m₂) ≃ p ^ (m₁ + n₂)
this✝ : p ^ n₁ / p ^ m₁ / (p ^ n₂ / p ^ m₂) ≃ 1
this : p ^ n₁ / p ^ m₁ ≃ p ^ n₂ / p ^ m₂
⊢ p ^ n₁ / p ^ m₁ ≃ p ^ n₂ / p ^ m₂
Tactic:
exact this
State after:
no goals