internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Rational.pow_pos_substL_gt_nonneg
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Rational.pow_pos_substL_gt_nonneg
Proof 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›
Proof 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
Theorem: Lean4Axiomatic.Rational.pow_pos_substL_gt_nonneg
Proof 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›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.pow_pos_substL_gt_nonneg
Proof 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›
Proof 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
Theorem: Lean4Axiomatic.Rational.pow_pos_substL_gt_nonneg
Proof 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›)
Proof 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
Theorem: Lean4Axiomatic.Rational.pow_pos_substL_gt_nonneg
Proof 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›
Proof 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
Theorem: Lean4Axiomatic.Rational.pow_pos_substL_gt_nonneg
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Rational.pow_pos_substL_gt_nonneg
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Rational.pow_pos_substL_gt_nonneg
Proof 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›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.pow_scompatL_recip
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Rational.pow_scompatL_recip
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.pow_scompatL_recip
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.pow_scompatL_recip
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.pow_scompatL_recip
Proof 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')
Proof 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'
Theorem: Lean4Axiomatic.Rational.pow_scompatL_recip
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.pow_scompatL_abs
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Rational.pow_scompatL_abs
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.pow_scompatL_abs
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.pow_scompatL_abs
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Rational.pow_scompatL_abs
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Rational.pow_scompatL_abs
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.pow_scompatL_abs
Proof 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')
Proof 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'
Theorem: Lean4Axiomatic.Rational.pow_scompatL_abs
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.pow_substL
Proof state before:
ℕ ℤ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
ℚ : 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
inst✝² : Exponentiation ℚ
p₁ p₂ : ℚ
a : ℤ
inst✝¹ : AP (p₁ ≄ 0)
inst✝ : AP (p₂ ≄ 0)
⊢ p₁ ≃ p₂ → p₁ ^ a ≃ p₂ ^ a
Tactic:
intro (_ : p₁ ≃ p₂)
Proof state after:
ℕ ℤ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
ℚ : 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
inst✝² : Exponentiation ℚ
p₁ p₂ : ℚ
a : ℤ
inst✝¹ : AP (p₁ ≄ 0)
inst✝ : AP (p₂ ≄ 0)
x✝ : p₁ ≃ p₂
⊢ p₁ ^ a ≃ p₂ ^ a