Theorem: Lean4Axiomatic.Rational.pow_pos_substL_gt_nonneg (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 q : ℚ
n : ℕ
⊢ n > 0 → p > q ∧ q ≥ 0 → p ^ n > q ^ n ∧ q ^ n ≥ 0
Tactic:
intro (_ : n > 0) (And.intro (_ : p > q) (_ : q ≥ 0))
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 q : ℚ
n : ℕ
x✝ : n > 0
left✝ : p > q
right✝ : q ≥ 0
⊢ p ^ n > q ^ n ∧ q ^ n ≥ 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 q : ℚ
n : ℕ
x✝ : n > 0
left✝ : p > q
right✝ : q ≥ 0
⊢ p ^ n > q ^ n ∧ q ^ n ≥ 0
Tactic:
revert ‹n > 0›
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 q : ℚ
n : ℕ
left✝ : p > q
right✝ : q ≥ 0
⊢ n > 0 → p ^ n > q ^ n ∧ q ^ n ≥ 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 q : ℚ
n : ℕ
left✝ : p > q
right✝ : q ≥ 0
⊢ n > 0 → p ^ n > q ^ n ∧ q ^ n ≥ 0
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 q : ℚ
n : ℕ
left✝ : p > q
right✝ : q ≥ 0
⊢ 0 > 0 → p ^ 0 > q ^ 0 ∧ q ^ 0 ≥ 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 q : ℚ
n : ℕ
left✝ : p > q
right✝ : q ≥ 0
⊢ ∀ (m : ℕ), (m > 0 → p ^ m > q ^ m ∧ q ^ m ≥ 0) → step m > 0 → p ^ step m > q ^ step m ∧ q ^ step m ≥ 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 q : ℚ
n : ℕ
left✝ : p > q
right✝ : q ≥ 0
⊢ 0 > 0 → p ^ 0 > q ^ 0 ∧ q ^ 0 ≥ 0
Tactic:
case zero =>
  intro (_ : (0:ℕ) > 0)
  show p^0 > q^0 ∧ q^0 ≥ 0
  have : (0:ℕ) ≯ 0 := Natural.lt_zero
  exact absurd ‹(0:ℕ) > 0› ‹(0:ℕ) ≯ 0›
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 q : ℚ
n : ℕ
left✝ : p > q
right✝ : q ≥ 0
⊢ ∀ (m : ℕ), (m > 0 → p ^ m > q ^ m ∧ q ^ m ≥ 0) → step m > 0 → p ^ step m > q ^ step m ∧ q ^ step m ≥ 0
Tactic:
case step =>
  intro (n' : ℕ) (ih : n' > 0 → p^n' > q^n' ∧ q^n' ≥ 0) (_ : step n' > 0)
  show p^(step n') > q^(step n') ∧ q^(step n') ≥ 0
  have : n' ≃ 0 ∨ n' > 0 := Natural.gt_split ‹step n' > 0›
  match this with
  | Or.inl (_ : n' ≃ 0) =>
    have pow_step_zero {x : ℚ} : x^(step n') ≃ x := calc
      _ ≃ x^(step n') := eqv_refl
      _ ≃ x^n' * x    := pow_step
      _ ≃ x^0 * x     := mul_substL (Natural.pow_substR ‹n' ≃ 0›)
      _ ≃ 1 * x       := mul_substL pow_zero
      _ ≃ x           := mul_identL
    have : p^(step n') > q^(step n') := calc
      _ ≃ p^(step n') := eqv_refl
      _ ≃ p           := pow_step_zero
      _ > q           := ‹p > q›
      _ ≃ q^(step n') := eqv_symm pow_step_zero
    have : q^(step n') ≥ 0 := calc
      _ ≃ q^(step n') := eqv_refl
      _ ≃ q           := pow_step_zero
      _ ≥ 0           := ‹q ≥ 0›
    exact And.intro ‹p^(step n') > q^(step n')› ‹q^(step n') ≥ 0›
  | Or.inr (_ : n' > 0) =>
    have (And.intro (_ : p^n' > q^n') (_ : q^n' ≥ 0)) := ih ‹n' > 0›
    have : p ≥ q := ge_cases.mpr (Or.inl ‹p > q›)
    have : p > 0 := trans_gt_ge_gt ‹p > q› ‹q ≥ 0›
    have : p^(step n') > q^(step n') := calc
      _ ≃ p^(step n') := eqv_refl
      _ ≃ p^n' * p    := pow_step
      _ > q^n' * p    := lt_substL_mul_pos ‹p > 0› ‹p^n' > q^n'›
      _ ≥ q^n' * q    := le_substR_mul_nonneg ‹q^n' ≥ 0› ‹p ≥ q›
      _ ≃ q^(step n') := eqv_symm pow_step
    have : q^(step n') ≥ 0 := calc
      _ ≃ q^(step n') := eqv_refl
      _ ≃ q^n' * q    := pow_step
      _ ≥ 0 * q       := le_substL_mul_nonneg ‹q ≥ 0› ‹q^n' ≥ 0›
      _ ≃ 0           := mul_absorbL
    exact And.intro ‹p^(step n') > q^(step n')› ‹q^(step n') ≥ 0›
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 q : ℚ
n : ℕ
left✝ : p > q
right✝ : q ≥ 0
⊢ 0 > 0 → p ^ 0 > q ^ 0 ∧ q ^ 0 ≥ 0
Tactic:
intro (_ : (0:ℕ) > 0)
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 q : ℚ
n : ℕ
left✝ : p > q
right✝ : q ≥ 0
x✝ : 0 > 0
⊢ p ^ 0 > q ^ 0 ∧ q ^ 0 ≥ 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 q : ℚ
n : ℕ
left✝ : p > q
right✝ : q ≥ 0
x✝ : 0 > 0
⊢ p ^ 0 > q ^ 0 ∧ q ^ 0 ≥ 0
Tactic:
have : (0:ℕ) ≯ 0 := Natural.lt_zero
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 q : ℚ
n : ℕ
left✝ : p > q
right✝ : q ≥ 0
x✝ : 0 > 0
this : 0 ≯ 0
⊢ p ^ 0 > q ^ 0 ∧ q ^ 0 ≥ 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 q : ℚ
n : ℕ
left✝ : p > q
right✝ : q ≥ 0
x✝ : 0 > 0
this : 0 ≯ 0
⊢ p ^ 0 > q ^ 0 ∧ q ^ 0 ≥ 0
Tactic:
exact absurd ‹(0:ℕ) > 0› ‹(0:ℕ) ≯ 0›
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 q : ℚ
n : ℕ
left✝ : p > q
right✝ : q ≥ 0
⊢ ∀ (m : ℕ), (m > 0 → p ^ m > q ^ m ∧ q ^ m ≥ 0) → step m > 0 → p ^ step m > q ^ step m ∧ q ^ step m ≥ 0
Tactic:
intro (n' : ℕ) (ih : n' > 0 → p^n' > q^n' ∧ q^n' ≥ 0) (_ : step n' > 0)
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 q : ℚ
n : ℕ
left✝ : p > q
right✝ : q ≥ 0
n' : ℕ
ih : n' > 0 → p ^ n' > q ^ n' ∧ q ^ n' ≥ 0
x✝ : step n' > 0
⊢ p ^ step n' > q ^ step n' ∧ q ^ step n' ≥ 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 q : ℚ
n : ℕ
left✝ : p > q
right✝ : q ≥ 0
n' : ℕ
ih : n' > 0 → p ^ n' > q ^ n' ∧ q ^ n' ≥ 0
x✝ : step n' > 0
⊢ p ^ step n' > q ^ step n' ∧ q ^ step n' ≥ 0
Tactic:
have : n' ≃ 0 ∨ n' > 0 := Natural.gt_split ‹step n' > 0›
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 q : ℚ
n : ℕ
left✝ : p > q
right✝ : q ≥ 0
n' : ℕ
ih : n' > 0 → p ^ n' > q ^ n' ∧ q ^ n' ≥ 0
x✝ : step n' > 0
this : n' ≃ 0 ∨ n' > 0
⊢ p ^ step n' > q ^ step n' ∧ q ^ step n' ≥ 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 q : ℚ
n : ℕ
left✝ : p > q
right✝ : q ≥ 0
n' : ℕ
ih : n' > 0 → p ^ n' > q ^ n' ∧ q ^ n' ≥ 0
x✝ : step n' > 0
this : n' ≃ 0 ∨ n' > 0
⊢ p ^ step n' > q ^ step n' ∧ q ^ step n' ≥ 0
Tactic:
match this with
| Or.inl (_ : n' ≃ 0) =>
  have pow_step_zero {x : ℚ} : x^(step n') ≃ x := calc
    _ ≃ x^(step n') := eqv_refl
    _ ≃ x^n' * x    := pow_step
    _ ≃ x^0 * x     := mul_substL (Natural.pow_substR ‹n' ≃ 0›)
    _ ≃ 1 * x       := mul_substL pow_zero
    _ ≃ x           := mul_identL
  have : p^(step n') > q^(step n') := calc
    _ ≃ p^(step n') := eqv_refl
    _ ≃ p           := pow_step_zero
    _ > q           := ‹p > q›
    _ ≃ q^(step n') := eqv_symm pow_step_zero
  have : q^(step n') ≥ 0 := calc
    _ ≃ q^(step n') := eqv_refl
    _ ≃ q           := pow_step_zero
    _ ≥ 0           := ‹q ≥ 0›
  exact And.intro ‹p^(step n') > q^(step n')› ‹q^(step n') ≥ 0›
| Or.inr (_ : n' > 0) =>
  have (And.intro (_ : p^n' > q^n') (_ : q^n' ≥ 0)) := ih ‹n' > 0›
  have : p ≥ q := ge_cases.mpr (Or.inl ‹p > q›)
  have : p > 0 := trans_gt_ge_gt ‹p > q› ‹q ≥ 0›
  have : p^(step n') > q^(step n') := calc
    _ ≃ p^(step n') := eqv_refl
    _ ≃ p^n' * p    := pow_step
    _ > q^n' * p    := lt_substL_mul_pos ‹p > 0› ‹p^n' > q^n'›
    _ ≥ q^n' * q    := le_substR_mul_nonneg ‹q^n' ≥ 0› ‹p ≥ q›
    _ ≃ q^(step n') := eqv_symm pow_step
  have : q^(step n') ≥ 0 := calc
    _ ≃ q^(step n') := eqv_refl
    _ ≃ q^n' * q    := pow_step
    _ ≥ 0 * q       := le_substL_mul_nonneg ‹q ≥ 0› ‹q^n' ≥ 0›
    _ ≃ 0           := mul_absorbL
  exact And.intro ‹p^(step n') > q^(step n')› ‹q^(step n') ≥ 0›
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 q : ℚ
n : ℕ
left✝ : p > q
right✝ : q ≥ 0
n' : ℕ
ih : n' > 0 → p ^ n' > q ^ n' ∧ q ^ n' ≥ 0
x✝ : step n' > 0
this : n' ≃ 0 ∨ n' > 0
h✝ : n' ≃ 0
⊢ p ^ step n' > q ^ step n' ∧ q ^ step n' ≥ 0
Tactic:
have pow_step_zero {x : ℚ} : x^(step n') ≃ x := calc
  _ ≃ x^(step n') := eqv_refl
  _ ≃ x^n' * x    := pow_step
  _ ≃ x^0 * x     := mul_substL (Natural.pow_substR ‹n' ≃ 0›)
  _ ≃ 1 * x       := mul_substL pow_zero
  _ ≃ x           := mul_identL
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 q : ℚ
n : ℕ
left✝ : p > q
right✝ : q ≥ 0
n' : ℕ
ih : n' > 0 → p ^ n' > q ^ n' ∧ q ^ n' ≥ 0
x✝ : step n' > 0
this : n' ≃ 0 ∨ n' > 0
h✝ : n' ≃ 0
pow_step_zero : ∀ {x : ℚ}, x ^ step n' ≃ x
⊢ p ^ step n' > q ^ step n' ∧ q ^ step n' ≥ 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 q : ℚ
n : ℕ
left✝ : p > q
right✝ : q ≥ 0
n' : ℕ
ih : n' > 0 → p ^ n' > q ^ n' ∧ q ^ n' ≥ 0
x✝ : step n' > 0
this : n' ≃ 0 ∨ n' > 0
h✝ : n' ≃ 0
pow_step_zero : ∀ {x : ℚ}, x ^ step n' ≃ x
⊢ p ^ step n' > q ^ step n' ∧ q ^ step n' ≥ 0
Tactic:
have : p^(step n') > q^(step n') := calc
  _ ≃ p^(step n') := eqv_refl
  _ ≃ p           := pow_step_zero
  _ > q           := ‹p > q›
  _ ≃ q^(step n') := eqv_symm pow_step_zero
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 q : ℚ
n : ℕ
left✝ : p > q
right✝ : q ≥ 0
n' : ℕ
ih : n' > 0 → p ^ n' > q ^ n' ∧ q ^ n' ≥ 0
x✝ : step n' > 0
this✝ : n' ≃ 0 ∨ n' > 0
h✝ : n' ≃ 0
pow_step_zero : ∀ {x : ℚ}, x ^ step n' ≃ x
this : p ^ step n' > q ^ step n'
⊢ p ^ step n' > q ^ step n' ∧ q ^ step n' ≥ 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 q : ℚ
n : ℕ
left✝ : p > q
right✝ : q ≥ 0
n' : ℕ
ih : n' > 0 → p ^ n' > q ^ n' ∧ q ^ n' ≥ 0
x✝ : step n' > 0
this✝ : n' ≃ 0 ∨ n' > 0
h✝ : n' ≃ 0
pow_step_zero : ∀ {x : ℚ}, x ^ step n' ≃ x
this : p ^ step n' > q ^ step n'
⊢ p ^ step n' > q ^ step n' ∧ q ^ step n' ≥ 0
Tactic:
have : q^(step n') ≥ 0 := calc
  _ ≃ q^(step n') := eqv_refl
  _ ≃ q           := pow_step_zero
  _ ≥ 0           := ‹q ≥ 0›
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 q : ℚ
n : ℕ
left✝ : p > q
right✝ : q ≥ 0
n' : ℕ
ih : n' > 0 → p ^ n' > q ^ n' ∧ q ^ n' ≥ 0
x✝ : step n' > 0
this✝¹ : n' ≃ 0 ∨ n' > 0
h✝ : n' ≃ 0
pow_step_zero : ∀ {x : ℚ}, x ^ step n' ≃ x
this✝ : p ^ step n' > q ^ step n'
this : q ^ step n' ≥ 0
⊢ p ^ step n' > q ^ step n' ∧ q ^ step n' ≥ 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 q : ℚ
n : ℕ
left✝ : p > q
right✝ : q ≥ 0
n' : ℕ
ih : n' > 0 → p ^ n' > q ^ n' ∧ q ^ n' ≥ 0
x✝ : step n' > 0
this✝¹ : n' ≃ 0 ∨ n' > 0
h✝ : n' ≃ 0
pow_step_zero : ∀ {x : ℚ}, x ^ step n' ≃ x
this✝ : p ^ step n' > q ^ step n'
this : q ^ step n' ≥ 0
⊢ p ^ step n' > q ^ step n' ∧ q ^ step n' ≥ 0
Tactic:
exact And.intro ‹p^(step n') > q^(step n')› ‹q^(step n') ≥ 0›
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 q : ℚ
n : ℕ
left✝ : p > q
right✝ : q ≥ 0
n' : ℕ
ih : n' > 0 → p ^ n' > q ^ n' ∧ q ^ n' ≥ 0
x✝ : step n' > 0
this : n' ≃ 0 ∨ n' > 0
h✝ : n' > 0
⊢ p ^ step n' > q ^ step n' ∧ q ^ step n' ≥ 0
Tactic:
have (And.intro (_ : p^n' > q^n') (_ : q^n' ≥ 0)) := ih ‹n' > 0›
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 q : ℚ
n : ℕ
left✝¹ : p > q
right✝¹ : q ≥ 0
n' : ℕ
ih : n' > 0 → p ^ n' > q ^ n' ∧ q ^ n' ≥ 0
x✝ : step n' > 0
this : n' ≃ 0 ∨ n' > 0
h✝ : n' > 0
left✝ : p ^ n' > q ^ n'
right✝ : q ^ n' ≥ 0
⊢ p ^ step n' > q ^ step n' ∧ q ^ step n' ≥ 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 q : ℚ
n : ℕ
left✝¹ : p > q
right✝¹ : q ≥ 0
n' : ℕ
ih : n' > 0 → p ^ n' > q ^ n' ∧ q ^ n' ≥ 0
x✝ : step n' > 0
this : n' ≃ 0 ∨ n' > 0
h✝ : n' > 0
left✝ : p ^ n' > q ^ n'
right✝ : q ^ n' ≥ 0
⊢ p ^ step n' > q ^ step n' ∧ q ^ step n' ≥ 0
Tactic:
have : p ≥ q := ge_cases.mpr (Or.inl ‹p > q›)
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 q : ℚ
n : ℕ
left✝¹ : p > q
right✝¹ : q ≥ 0
n' : ℕ
ih : n' > 0 → p ^ n' > q ^ n' ∧ q ^ n' ≥ 0
x✝ : step n' > 0
this✝ : n' ≃ 0 ∨ n' > 0
h✝ : n' > 0
left✝ : p ^ n' > q ^ n'
right✝ : q ^ n' ≥ 0
this : p ≥ q
⊢ p ^ step n' > q ^ step n' ∧ q ^ step n' ≥ 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 q : ℚ
n : ℕ
left✝¹ : p > q
right✝¹ : q ≥ 0
n' : ℕ
ih : n' > 0 → p ^ n' > q ^ n' ∧ q ^ n' ≥ 0
x✝ : step n' > 0
this✝ : n' ≃ 0 ∨ n' > 0
h✝ : n' > 0
left✝ : p ^ n' > q ^ n'
right✝ : q ^ n' ≥ 0
this : p ≥ q
⊢ p ^ step n' > q ^ step n' ∧ q ^ step n' ≥ 0
Tactic:
have : p > 0 := trans_gt_ge_gt ‹p > q› ‹q ≥ 0›
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 q : ℚ
n : ℕ
left✝¹ : p > q
right✝¹ : q ≥ 0
n' : ℕ
ih : n' > 0 → p ^ n' > q ^ n' ∧ q ^ n' ≥ 0
x✝ : step n' > 0
this✝¹ : n' ≃ 0 ∨ n' > 0
h✝ : n' > 0
left✝ : p ^ n' > q ^ n'
right✝ : q ^ n' ≥ 0
this✝ : p ≥ q
this : p > 0
⊢ p ^ step n' > q ^ step n' ∧ q ^ step n' ≥ 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 q : ℚ
n : ℕ
left✝¹ : p > q
right✝¹ : q ≥ 0
n' : ℕ
ih : n' > 0 → p ^ n' > q ^ n' ∧ q ^ n' ≥ 0
x✝ : step n' > 0
this✝¹ : n' ≃ 0 ∨ n' > 0
h✝ : n' > 0
left✝ : p ^ n' > q ^ n'
right✝ : q ^ n' ≥ 0
this✝ : p ≥ q
this : p > 0
⊢ p ^ step n' > q ^ step n' ∧ q ^ step n' ≥ 0
Tactic:
have : p^(step n') > q^(step n') := calc
  _ ≃ p^(step n') := eqv_refl
  _ ≃ p^n' * p    := pow_step
  _ > q^n' * p    := lt_substL_mul_pos ‹p > 0› ‹p^n' > q^n'›
  _ ≥ q^n' * q    := le_substR_mul_nonneg ‹q^n' ≥ 0› ‹p ≥ q›
  _ ≃ q^(step n') := eqv_symm pow_step
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 q : ℚ
n : ℕ
left✝¹ : p > q
right✝¹ : q ≥ 0
n' : ℕ
ih : n' > 0 → p ^ n' > q ^ n' ∧ q ^ n' ≥ 0
x✝ : step n' > 0
this✝² : n' ≃ 0 ∨ n' > 0
h✝ : n' > 0
left✝ : p ^ n' > q ^ n'
right✝ : q ^ n' ≥ 0
this✝¹ : p ≥ q
this✝ : p > 0
this : p ^ step n' > q ^ step n'
⊢ p ^ step n' > q ^ step n' ∧ q ^ step n' ≥ 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 q : ℚ
n : ℕ
left✝¹ : p > q
right✝¹ : q ≥ 0
n' : ℕ
ih : n' > 0 → p ^ n' > q ^ n' ∧ q ^ n' ≥ 0
x✝ : step n' > 0
this✝² : n' ≃ 0 ∨ n' > 0
h✝ : n' > 0
left✝ : p ^ n' > q ^ n'
right✝ : q ^ n' ≥ 0
this✝¹ : p ≥ q
this✝ : p > 0
this : p ^ step n' > q ^ step n'
⊢ p ^ step n' > q ^ step n' ∧ q ^ step n' ≥ 0
Tactic:
have : q^(step n') ≥ 0 := calc
  _ ≃ q^(step n') := eqv_refl
  _ ≃ q^n' * q    := pow_step
  _ ≥ 0 * q       := le_substL_mul_nonneg ‹q ≥ 0› ‹q^n' ≥ 0›
  _ ≃ 0           := mul_absorbL
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 q : ℚ
n : ℕ
left✝¹ : p > q
right✝¹ : q ≥ 0
n' : ℕ
ih : n' > 0 → p ^ n' > q ^ n' ∧ q ^ n' ≥ 0
x✝ : step n' > 0
this✝³ : n' ≃ 0 ∨ n' > 0
h✝ : n' > 0
left✝ : p ^ n' > q ^ n'
right✝ : q ^ n' ≥ 0
this✝² : p ≥ q
this✝¹ : p > 0
this✝ : p ^ step n' > q ^ step n'
this : q ^ step n' ≥ 0
⊢ p ^ step n' > q ^ step n' ∧ q ^ step n' ≥ 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 q : ℚ
n : ℕ
left✝¹ : p > q
right✝¹ : q ≥ 0
n' : ℕ
ih : n' > 0 → p ^ n' > q ^ n' ∧ q ^ n' ≥ 0
x✝ : step n' > 0
this✝³ : n' ≃ 0 ∨ n' > 0
h✝ : n' > 0
left✝ : p ^ n' > q ^ n'
right✝ : q ^ n' ≥ 0
this✝² : p ≥ q
this✝¹ : p > 0
this✝ : p ^ step n' > q ^ step n'
this : q ^ step n' ≥ 0
⊢ p ^ step n' > q ^ step n' ∧ q ^ step n' ≥ 0
Tactic:
exact And.intro ‹p^(step n') > q^(step n')› ‹q^(step n') ≥ 0›
State after:
no goals