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

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 : ℚ
inst✝ : AP (p ≄ 0)
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
⊢ p ^ a₁ ≃ p ^ a₂
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 : ℚ
inst✝ : AP (p ≄ 0)
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
ctx : Integer.Induction.Context fun x => (p : ℚ) → [inst : AP (p ≄ 0)] → ℚ :=
  Lean4Axiomatic.Rational.Impl.Generic.ind_ctx
⊢ p ^ a₁ ≃ p ^ a₂

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 : ℚ
inst✝ : AP (p ≄ 0)
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
ctx : Integer.Induction.Context fun x => (p : ℚ) → [inst : AP (p ≄ 0)] → ℚ :=
  Lean4Axiomatic.Rational.Impl.Generic.ind_ctx
⊢ p ^ a₁ ≃ p ^ a₂
Tactic:
have : ctx.rec_diff a₁ ≃ ctx.rec_diff a₂ := ctx.rec_diff_subst ‹a₁ ≃ a₂›
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 : ℚ
inst✝ : AP (p ≄ 0)
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
ctx : Integer.Induction.Context fun x => (p : ℚ) → [inst : AP (p ≄ 0)] → ℚ :=
  Lean4Axiomatic.Rational.Impl.Generic.ind_ctx
this : ctx.rec_diff a₁ ≃ ctx.rec_diff a₂
⊢ p ^ a₁ ≃ p ^ a₂

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 : ℚ
inst✝ : AP (p ≄ 0)
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
ctx : Integer.Induction.Context fun x => (p : ℚ) → [inst : AP (p ≄ 0)] → ℚ :=
  Lean4Axiomatic.Rational.Impl.Generic.ind_ctx
this : ctx.rec_diff a₁ ≃ ctx.rec_diff a₂
⊢ p ^ a₁ ≃ p ^ a₂
Tactic:
have rec_subst
  : (x : ℚ) → [AP (x ≄ 0)] → ctx.rec_diff a₁ x ≃ ctx.rec_diff a₂ 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 : ℚ
inst✝ : AP (p ≄ 0)
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
ctx : Integer.Induction.Context fun x => (p : ℚ) → [inst : AP (p ≄ 0)] → ℚ :=
  Lean4Axiomatic.Rational.Impl.Generic.ind_ctx
this : ctx.rec_diff a₁ ≃ ctx.rec_diff a₂
rec_subst : ∀ (x : ℚ) [inst : AP (x ≄ 0)], ctx.rec_diff a₁ x ≃ ctx.rec_diff a₂ x
⊢ p ^ a₁ ≃ p ^ a₂

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 : ℚ
inst✝ : AP (p ≄ 0)
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
ctx : Integer.Induction.Context fun x => (p : ℚ) → [inst : AP (p ≄ 0)] → ℚ :=
  Lean4Axiomatic.Rational.Impl.Generic.ind_ctx
this : ctx.rec_diff a₁ ≃ ctx.rec_diff a₂
rec_subst : ∀ (x : ℚ) [inst : AP (x ≄ 0)], ctx.rec_diff a₁ x ≃ ctx.rec_diff a₂ x
⊢ p ^ a₁ ≃ p ^ a₂
Tactic:
calc
  _ = p^a₁              := rfl
  _ = _pow p a₁         := rfl
  _ = ctx.rec_diff a₁ p := rfl
  _ ≃ ctx.rec_diff a₂ p := rec_subst p
  _ = _pow p a₂         := rfl
  _ = p^a₂              := rfl
State after:
no goals