Theorem: Lean4Axiomatic.Rational.Impl.Generic.pow_diff (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
p : ℚ
n m : ℕ
inst✝ : AP (p ≄ 0)
⊢ p ^ (Coe.coe n - Coe.coe m) ≃ p ^ n / p ^ m
Tactic:
let ctx := ind_ctx (ℚ := ℚ)
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
p : ℚ
n m : ℕ
inst✝ : AP (p ≄ 0)
ctx : Integer.Induction.Context fun x => (p : ℚ) → [inst : AP (p ≄ 0)] → ℚ :=
  Lean4Axiomatic.Rational.Impl.Generic.ind_ctx
⊢ p ^ (Coe.coe n - Coe.coe 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
p : ℚ
n m : ℕ
inst✝ : AP (p ≄ 0)
ctx : Integer.Induction.Context fun x => (p : ℚ) → [inst : AP (p ≄ 0)] → ℚ :=
  Lean4Axiomatic.Rational.Impl.Generic.ind_ctx
⊢ p ^ (Coe.coe n - Coe.coe m) ≃ p ^ n / p ^ m
Tactic:
have : ctx.rec_diff ((n:ℤ) - m) ≃ ctx.on_diff n m := ctx.rec_diff_eval
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
p : ℚ
n m : ℕ
inst✝ : AP (p ≄ 0)
ctx : Integer.Induction.Context fun x => (p : ℚ) → [inst : AP (p ≄ 0)] → ℚ :=
  Lean4Axiomatic.Rational.Impl.Generic.ind_ctx
this :
  ctx.rec_diff (Coe.coe n - Coe.coe m) ≃
    Integer.Induction.Context.on_diff (motive := fun x => (p : ℚ) → [inst : AP (p ≄ 0)] → ℚ) n m
⊢ p ^ (Coe.coe n - Coe.coe 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
p : ℚ
n m : ℕ
inst✝ : AP (p ≄ 0)
ctx : Integer.Induction.Context fun x => (p : ℚ) → [inst : AP (p ≄ 0)] → ℚ :=
  Lean4Axiomatic.Rational.Impl.Generic.ind_ctx
this :
  ctx.rec_diff (Coe.coe n - Coe.coe m) ≃
    Integer.Induction.Context.on_diff (motive := fun x => (p : ℚ) → [inst : AP (p ≄ 0)] → ℚ) n m
⊢ p ^ (Coe.coe n - Coe.coe m) ≃ p ^ n / p ^ m
Tactic:
have rec_eval
  : (x : ℚ) → [AP (x ≄ 0)] → ctx.rec_diff ((n:ℤ) - m) x ≃ ctx.on_diff n m x
  := 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
p : ℚ
n m : ℕ
inst✝ : AP (p ≄ 0)
ctx : Integer.Induction.Context fun x => (p : ℚ) → [inst : AP (p ≄ 0)] → ℚ :=
  Lean4Axiomatic.Rational.Impl.Generic.ind_ctx
this :
  ctx.rec_diff (Coe.coe n - Coe.coe m) ≃
    Integer.Induction.Context.on_diff (motive := fun x => (p : ℚ) → [inst : AP (p ≄ 0)] → ℚ) n m
rec_eval :
  ∀ (x : ℚ) [inst : AP (x ≄ 0)],
    ctx.rec_diff (Coe.coe n - Coe.coe m) x ≃
      Integer.Induction.Context.on_diff (motive := fun x => (p : ℚ) → [inst : AP (p ≄ 0)] → ℚ) n m x
⊢ p ^ (Coe.coe n - Coe.coe 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
p : ℚ
n m : ℕ
inst✝ : AP (p ≄ 0)
ctx : Integer.Induction.Context fun x => (p : ℚ) → [inst : AP (p ≄ 0)] → ℚ :=
  Lean4Axiomatic.Rational.Impl.Generic.ind_ctx
this :
  ctx.rec_diff (Coe.coe n - Coe.coe m) ≃
    Integer.Induction.Context.on_diff (motive := fun x => (p : ℚ) → [inst : AP (p ≄ 0)] → ℚ) n m
rec_eval :
  ∀ (x : ℚ) [inst : AP (x ≄ 0)],
    ctx.rec_diff (Coe.coe n - Coe.coe m) x ≃
      Integer.Induction.Context.on_diff (motive := fun x => (p : ℚ) → [inst : AP (p ≄ 0)] → ℚ) n m x
⊢ p ^ (Coe.coe n - Coe.coe m) ≃ p ^ n / p ^ m
Tactic:
calc
  _ = p^((n:ℤ) - m)              := rfl
  _ = _pow p ((n:ℤ) - m)         := rfl
  _ = ctx.rec_diff ((n:ℤ) - m) p := rfl
  _ ≃ ctx.on_diff n m p          := rec_eval p
  _ = on_diff_pow n m p          := rfl
  _ = p^n / p^m                  := rfl
State after:
no goals