Theorem: Lean4Axiomatic.Rational.pow_scompatL_abs (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 : ℕ
⊢ abs (p ^ n) ≃ abs 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 : ℕ
⊢ abs (p ^ 0) ≃ abs 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 : ℕ
⊢ ∀ (m : ℕ), abs (p ^ m) ≃ abs p ^ m → abs (p ^ step m) ≃ abs 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 : ℕ
⊢ abs (p ^ 0) ≃ abs p ^ 0
Tactic:
case zero =>
  show abs (p^0) ≃ (abs p)^0
  have : sgn (1:ℚ) ≃ 1 := sgn_one
  have : abs (1:ℚ) ≃ 1 := abs_positive this
  calc
    _ ≃ abs (p^0) := eqv_refl
    _ ≃ abs 1     := abs_subst pow_zero
    _ ≃ 1         := ‹abs (1:ℚ) ≃ 1›
    _ ≃ (abs 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 : ℕ
⊢ ∀ (m : ℕ), abs (p ^ m) ≃ abs p ^ m → abs (p ^ step m) ≃ abs p ^ step m
Tactic:
case step =>
  intro (n' : ℕ) (ih : abs (p^n') ≃ (abs p)^n')
  show abs (p^(step n')) ≃ (abs p)^(step n')
  calc
    _ ≃ abs (p^(step n'))  := eqv_refl
    _ ≃ abs (p^n' * p)     := abs_subst pow_step
    _ ≃ abs (p^n') * abs p := abs_compat_mul
    _ ≃ (abs p)^n' * abs p := mul_substL ih
    _ ≃ (abs 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 : ℕ
⊢ abs (p ^ 0) ≃ abs p ^ 0
Tactic:
have : sgn (1:ℚ) ≃ 1 := sgn_one
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 : ℕ
this : sgn 1 ≃ 1
⊢ abs (p ^ 0) ≃ abs p ^ 0

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 : ℕ
this : sgn 1 ≃ 1
⊢ abs (p ^ 0) ≃ abs p ^ 0
Tactic:
have : abs (1:ℚ) ≃ 1 := abs_positive this
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 : ℕ
this✝ : sgn 1 ≃ 1
this : abs 1 ≃ 1
⊢ abs (p ^ 0) ≃ abs p ^ 0

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 : ℕ
this✝ : sgn 1 ≃ 1
this : abs 1 ≃ 1
⊢ abs (p ^ 0) ≃ abs p ^ 0
Tactic:
calc
  _ ≃ abs (p^0) := eqv_refl
  _ ≃ abs 1     := abs_subst pow_zero
  _ ≃ 1         := ‹abs (1:ℚ) ≃ 1›
  _ ≃ (abs 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 : ℕ
⊢ ∀ (m : ℕ), abs (p ^ m) ≃ abs p ^ m → abs (p ^ step m) ≃ abs p ^ step m
Tactic:
intro (n' : ℕ) (ih : abs (p^n') ≃ (abs 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 n' : ℕ
ih : abs (p ^ n') ≃ abs p ^ n'
⊢ abs (p ^ step n') ≃ abs 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 n' : ℕ
ih : abs (p ^ n') ≃ abs p ^ n'
⊢ abs (p ^ step n') ≃ abs p ^ step n'
Tactic:
calc
  _ ≃ abs (p^(step n'))  := eqv_refl
  _ ≃ abs (p^n' * p)     := abs_subst pow_step
  _ ≃ abs (p^n') * abs p := abs_compat_mul
  _ ≃ (abs p)^n' * abs p := mul_substL ih
  _ ≃ (abs p)^(step n')  := eqv_symm pow_step
State after:
no goals