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

State before:
ℕ ℤ : Type
inst✝¹³ : Natural ℕ
inst✝¹² : Integer ℤ
ℚ : Type
inst✝¹¹ : Core ℚ
inst✝¹⁰ : Addition ℚ
inst✝⁹ : Multiplication ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Reciprocation ℚ
inst✝⁵ : Division ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Order ℚ
inst✝² : Metric ℚ
inst✝¹ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
p : ℚ
n : ℕ
inst✝ : AP (p ≄ 0)
⊢ (p ^ n)⁻¹ ≃ p⁻¹ ^ n
Tactic:
apply Natural.ind_on n
State after:
case zero
ℕ ℤ : Type
inst✝¹³ : Natural ℕ
inst✝¹² : Integer ℤ
ℚ : Type
inst✝¹¹ : Core ℚ
inst✝¹⁰ : Addition ℚ
inst✝⁹ : Multiplication ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Reciprocation ℚ
inst✝⁵ : Division ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Order ℚ
inst✝² : Metric ℚ
inst✝¹ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
p : ℚ
n : ℕ
inst✝ : AP (p ≄ 0)
⊢ (p ^ 0)⁻¹ ≃ p⁻¹ ^ 0

case step
ℕ ℤ : Type
inst✝¹³ : Natural ℕ
inst✝¹² : Integer ℤ
ℚ : Type
inst✝¹¹ : Core ℚ
inst✝¹⁰ : Addition ℚ
inst✝⁹ : Multiplication ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Reciprocation ℚ
inst✝⁵ : Division ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Order ℚ
inst✝² : Metric ℚ
inst✝¹ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
p : ℚ
n : ℕ
inst✝ : AP (p ≄ 0)
⊢ ∀ (m : ℕ), (p ^ m)⁻¹ ≃ p⁻¹ ^ m → (p ^ step m)⁻¹ ≃ p⁻¹ ^ step m

State before:
ℕ ℤ : Type
inst✝¹³ : Natural ℕ
inst✝¹² : Integer ℤ
ℚ : Type
inst✝¹¹ : Core ℚ
inst✝¹⁰ : Addition ℚ
inst✝⁹ : Multiplication ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Reciprocation ℚ
inst✝⁵ : Division ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Order ℚ
inst✝² : Metric ℚ
inst✝¹ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
p : ℚ
n : ℕ
inst✝ : AP (p ≄ 0)
⊢ (p ^ 0)⁻¹ ≃ p⁻¹ ^ 0
Tactic:
case zero =>
  show (p^(0:ℕ))⁻¹ ≃ (p⁻¹)^(0:ℕ)
  calc
    _ = (p^(0:ℕ))⁻¹ := rfl
    _ ≃ 1⁻¹         := recip_subst pow_zero
    _ ≃ 1           := recip_sqrt1
    _ ≃ (p⁻¹)^(0:ℕ) := eqv_symm pow_zero
State after:
no goals

State before:
ℕ ℤ : Type
inst✝¹³ : Natural ℕ
inst✝¹² : Integer ℤ
ℚ : Type
inst✝¹¹ : Core ℚ
inst✝¹⁰ : Addition ℚ
inst✝⁹ : Multiplication ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Reciprocation ℚ
inst✝⁵ : Division ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Order ℚ
inst✝² : Metric ℚ
inst✝¹ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
p : ℚ
n : ℕ
inst✝ : AP (p ≄ 0)
⊢ ∀ (m : ℕ), (p ^ m)⁻¹ ≃ p⁻¹ ^ m → (p ^ step m)⁻¹ ≃ p⁻¹ ^ step m
Tactic:
case step =>
  intro (n' : ℕ) (ih : (p^n')⁻¹ ≃ (p⁻¹)^n')
  show (p^(step n'))⁻¹ ≃ (p⁻¹)^(step n')
  calc
    _ ≃ (p^(step n'))⁻¹ := eqv_refl
    _ ≃ (p^n' * p)⁻¹    := recip_subst pow_step
    _ ≃ (p^n')⁻¹ * p⁻¹  := recip_compat_mul
    _ ≃ (p⁻¹)^n' * p⁻¹  := mul_substL ih
    _ ≃ (p⁻¹)^(step n') := eqv_symm pow_step
State after:
no goals

State before:
ℕ ℤ : Type
inst✝¹³ : Natural ℕ
inst✝¹² : Integer ℤ
ℚ : Type
inst✝¹¹ : Core ℚ
inst✝¹⁰ : Addition ℚ
inst✝⁹ : Multiplication ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Reciprocation ℚ
inst✝⁵ : Division ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Order ℚ
inst✝² : Metric ℚ
inst✝¹ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
p : ℚ
n : ℕ
inst✝ : AP (p ≄ 0)
⊢ (p ^ 0)⁻¹ ≃ p⁻¹ ^ 0
Tactic:
calc
  _ = (p^(0:ℕ))⁻¹ := rfl
  _ ≃ 1⁻¹         := recip_subst pow_zero
  _ ≃ 1           := recip_sqrt1
  _ ≃ (p⁻¹)^(0:ℕ) := eqv_symm pow_zero
State after:
no goals

State before:
ℕ ℤ : Type
inst✝¹³ : Natural ℕ
inst✝¹² : Integer ℤ
ℚ : Type
inst✝¹¹ : Core ℚ
inst✝¹⁰ : Addition ℚ
inst✝⁹ : Multiplication ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Reciprocation ℚ
inst✝⁵ : Division ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Order ℚ
inst✝² : Metric ℚ
inst✝¹ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
p : ℚ
n : ℕ
inst✝ : AP (p ≄ 0)
⊢ ∀ (m : ℕ), (p ^ m)⁻¹ ≃ p⁻¹ ^ m → (p ^ step m)⁻¹ ≃ p⁻¹ ^ step m
Tactic:
intro (n' : ℕ) (ih : (p^n')⁻¹ ≃ (p⁻¹)^n')
State after:
ℕ ℤ : Type
inst✝¹³ : Natural ℕ
inst✝¹² : Integer ℤ
ℚ : Type
inst✝¹¹ : Core ℚ
inst✝¹⁰ : Addition ℚ
inst✝⁹ : Multiplication ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Reciprocation ℚ
inst✝⁵ : Division ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Order ℚ
inst✝² : Metric ℚ
inst✝¹ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
p : ℚ
n : ℕ
inst✝ : AP (p ≄ 0)
n' : ℕ
ih : (p ^ n')⁻¹ ≃ p⁻¹ ^ n'
⊢ (p ^ step n')⁻¹ ≃ p⁻¹ ^ step n'

State before:
ℕ ℤ : Type
inst✝¹³ : Natural ℕ
inst✝¹² : Integer ℤ
ℚ : Type
inst✝¹¹ : Core ℚ
inst✝¹⁰ : Addition ℚ
inst✝⁹ : Multiplication ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Reciprocation ℚ
inst✝⁵ : Division ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Order ℚ
inst✝² : Metric ℚ
inst✝¹ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
p : ℚ
n : ℕ
inst✝ : AP (p ≄ 0)
n' : ℕ
ih : (p ^ n')⁻¹ ≃ p⁻¹ ^ n'
⊢ (p ^ step n')⁻¹ ≃ p⁻¹ ^ step n'
Tactic:
calc
  _ ≃ (p^(step n'))⁻¹ := eqv_refl
  _ ≃ (p^n' * p)⁻¹    := recip_subst pow_step
  _ ≃ (p^n')⁻¹ * p⁻¹  := recip_compat_mul
  _ ≃ (p⁻¹)^n' * p⁻¹  := mul_substL ih
  _ ≃ (p⁻¹)^(step n') := eqv_symm pow_step
State after:
no goals