internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Rational.Impl.Generic.on_diff_subst_pow
Proof 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
n₁ m₁ n₂ m₂ : ℕ
x✝¹ : Coe.coe n₁ - Coe.coe m₁ ≃ Coe.coe n₂ - Coe.coe m₂
p : ℚ
x✝ : AP (p ≄ 0)
pow_add_n₁m₂ : p ^ n₁ * p ^ m₂ ≃ p ^ (n₁ + m₂)
pow_add_m₁n₂ : p ^ m₁ * p ^ n₂ ≃ p ^ (m₁ + n₂)
this✝¹ : Coe.coe n₁ + Coe.coe m₂ ≃ Coe.coe n₂ + Coe.coe m₁
this✝ : Coe.coe (n₁ + m₂) ≃ Coe.coe (m₁ + n₂)
this : n₁ + m₂ ≃ m₁ + n₂
⊢ p ^ n₁ / p ^ m₁ ≃ p ^ n₂ / p ^ m₂
Tactic:
have pow_add_subst : p^(n₁ + m₂) ≃ p^(m₁ + n₂) := Natural.pow_substR this
Proof 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
n₁ m₁ n₂ m₂ : ℕ
x✝¹ : Coe.coe n₁ - Coe.coe m₁ ≃ Coe.coe n₂ - Coe.coe m₂
p : ℚ
x✝ : AP (p ≄ 0)
pow_add_n₁m₂ : p ^ n₁ * p ^ m₂ ≃ p ^ (n₁ + m₂)
pow_add_m₁n₂ : p ^ m₁ * p ^ n₂ ≃ p ^ (m₁ + n₂)
this✝¹ : Coe.coe n₁ + Coe.coe m₂ ≃ Coe.coe n₂ + Coe.coe m₁
this✝ : Coe.coe (n₁ + m₂) ≃ Coe.coe (m₁ + n₂)
this : n₁ + m₂ ≃ m₁ + n₂
pow_add_subst : p ^ (n₁ + m₂) ≃ p ^ (m₁ + n₂)
⊢ p ^ n₁ / p ^ m₁ ≃ p ^ n₂ / p ^ m₂
Theorem: Lean4Axiomatic.Rational.Impl.Generic.on_diff_subst_pow
Proof 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
n₁ m₁ n₂ m₂ : ℕ
x✝¹ : Coe.coe n₁ - Coe.coe m₁ ≃ Coe.coe n₂ - Coe.coe m₂
p : ℚ
x✝ : AP (p ≄ 0)
pow_add_n₁m₂ : p ^ n₁ * p ^ m₂ ≃ p ^ (n₁ + m₂)
pow_add_m₁n₂ : p ^ m₁ * p ^ n₂ ≃ p ^ (m₁ + n₂)
this✝¹ : Coe.coe n₁ + Coe.coe m₂ ≃ Coe.coe n₂ + Coe.coe m₁
this✝ : Coe.coe (n₁ + m₂) ≃ Coe.coe (m₁ + n₂)
this : n₁ + m₂ ≃ m₁ + n₂
pow_add_subst : p ^ (n₁ + m₂) ≃ p ^ (m₁ + n₂)
⊢ p ^ n₁ / p ^ m₁ ≃ p ^ n₂ / p ^ m₂
Tactic:
have : (p^n₁ / p^m₁) / (p^n₂ / p^m₂) ≃ 1 := calc
  _ = (p^n₁ / p^m₁) / (p^n₂ / p^m₂) := rfl
  _ ≃ (p^n₁ * p^m₂) / (p^m₁ * p^n₂) := div_div_div
  _ ≃ p^(n₁ + m₂) / (p^m₁ * p^n₂)   := div_substL pow_add_n₁m₂
  _ ≃ p^(n₁ + m₂) / p^(m₁ + n₂)     := div_substR pow_add_m₁n₂
  _ ≃ p^(m₁ + n₂) / p^(m₁ + n₂)     := div_substL pow_add_subst
  _ ≃ 1                             := div_same
Proof 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
n₁ m₁ n₂ m₂ : ℕ
x✝¹ : Coe.coe n₁ - Coe.coe m₁ ≃ Coe.coe n₂ - Coe.coe m₂
p : ℚ
x✝ : AP (p ≄ 0)
pow_add_n₁m₂ : p ^ n₁ * p ^ m₂ ≃ p ^ (n₁ + m₂)
pow_add_m₁n₂ : p ^ m₁ * p ^ n₂ ≃ p ^ (m₁ + n₂)
this✝² : Coe.coe n₁ + Coe.coe m₂ ≃ Coe.coe n₂ + Coe.coe m₁
this✝¹ : Coe.coe (n₁ + m₂) ≃ Coe.coe (m₁ + n₂)
this✝ : n₁ + m₂ ≃ m₁ + n₂
pow_add_subst : p ^ (n₁ + m₂) ≃ p ^ (m₁ + n₂)
this : p ^ n₁ / p ^ m₁ / (p ^ n₂ / p ^ m₂) ≃ 1
⊢ p ^ n₁ / p ^ m₁ ≃ p ^ n₂ / p ^ m₂
Theorem: Lean4Axiomatic.Rational.Impl.Generic.on_diff_subst_pow
Proof 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
n₁ m₁ n₂ m₂ : ℕ
x✝¹ : Coe.coe n₁ - Coe.coe m₁ ≃ Coe.coe n₂ - Coe.coe m₂
p : ℚ
x✝ : AP (p ≄ 0)
pow_add_n₁m₂ : p ^ n₁ * p ^ m₂ ≃ p ^ (n₁ + m₂)
pow_add_m₁n₂ : p ^ m₁ * p ^ n₂ ≃ p ^ (m₁ + n₂)
this✝² : Coe.coe n₁ + Coe.coe m₂ ≃ Coe.coe n₂ + Coe.coe m₁
this✝¹ : Coe.coe (n₁ + m₂) ≃ Coe.coe (m₁ + n₂)
this✝ : n₁ + m₂ ≃ m₁ + n₂
pow_add_subst : p ^ (n₁ + m₂) ≃ p ^ (m₁ + n₂)
this : p ^ n₁ / p ^ m₁ / (p ^ n₂ / p ^ m₂) ≃ 1
⊢ p ^ n₁ / p ^ m₁ ≃ p ^ n₂ / p ^ m₂
Tactic:
have : p^n₁ / p^m₁ ≃ p^n₂ / p^m₂ := div_eqv_1.mp this
Proof 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
n₁ m₁ n₂ m₂ : ℕ
x✝¹ : Coe.coe n₁ - Coe.coe m₁ ≃ Coe.coe n₂ - Coe.coe m₂
p : ℚ
x✝ : AP (p ≄ 0)
pow_add_n₁m₂ : p ^ n₁ * p ^ m₂ ≃ p ^ (n₁ + m₂)
pow_add_m₁n₂ : p ^ m₁ * p ^ n₂ ≃ p ^ (m₁ + n₂)
this✝³ : Coe.coe n₁ + Coe.coe m₂ ≃ Coe.coe n₂ + Coe.coe m₁
this✝² : Coe.coe (n₁ + m₂) ≃ Coe.coe (m₁ + n₂)
this✝¹ : n₁ + m₂ ≃ m₁ + n₂
pow_add_subst : p ^ (n₁ + m₂) ≃ p ^ (m₁ + n₂)
this✝ : p ^ n₁ / p ^ m₁ / (p ^ n₂ / p ^ m₂) ≃ 1
this : p ^ n₁ / p ^ m₁ ≃ p ^ n₂ / p ^ m₂
⊢ p ^ n₁ / p ^ m₁ ≃ p ^ n₂ / p ^ m₂
Theorem: Lean4Axiomatic.Rational.Impl.Generic.on_diff_subst_pow
Proof 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
n₁ m₁ n₂ m₂ : ℕ
x✝¹ : Coe.coe n₁ - Coe.coe m₁ ≃ Coe.coe n₂ - Coe.coe m₂
p : ℚ
x✝ : AP (p ≄ 0)
pow_add_n₁m₂ : p ^ n₁ * p ^ m₂ ≃ p ^ (n₁ + m₂)
pow_add_m₁n₂ : p ^ m₁ * p ^ n₂ ≃ p ^ (m₁ + n₂)
this✝³ : Coe.coe n₁ + Coe.coe m₂ ≃ Coe.coe n₂ + Coe.coe m₁
this✝² : Coe.coe (n₁ + m₂) ≃ Coe.coe (m₁ + n₂)
this✝¹ : n₁ + m₂ ≃ m₁ + n₂
pow_add_subst : p ^ (n₁ + m₂) ≃ p ^ (m₁ + n₂)
this✝ : p ^ n₁ / p ^ m₁ / (p ^ n₂ / p ^ m₂) ≃ 1
this : p ^ n₁ / p ^ m₁ ≃ p ^ n₂ / p ^ m₂
⊢ p ^ n₁ / p ^ m₁ ≃ p ^ n₂ / p ^ m₂
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Generic.pow_diff
Proof 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 : ℚ
n m : ℕ
inst✝ : AP (p ≄ 0)
⊢ p ^ (Coe.coe n - Coe.coe m) ≃ p ^ n / p ^ m
Tactic:
let ctx := ind_ctx (ℚ := ℚ)
Proof 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 : ℚ
n m : ℕ
inst✝ : AP (p ≄ 0)
ctx : Integer.Induction.Context fun x => (p : ℚ) → [inst : AP (p ≄ 0)] → ℚ :=
  Lean4Axiomatic.Rational.Impl.Generic.ind_ctx
⊢ p ^ (Coe.coe n - Coe.coe m) ≃ p ^ n / p ^ m
Theorem: Lean4Axiomatic.Rational.Impl.Generic.pow_diff
Proof 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 : ℚ
n m : ℕ
inst✝ : AP (p ≄ 0)
ctx : Integer.Induction.Context fun x => (p : ℚ) → [inst : AP (p ≄ 0)] → ℚ :=
  Lean4Axiomatic.Rational.Impl.Generic.ind_ctx
⊢ p ^ (Coe.coe n - Coe.coe m) ≃ p ^ n / p ^ m
Tactic:
have : ctx.rec_diff ((n:ℤ) - m) ≃ ctx.on_diff n m := ctx.rec_diff_eval
Proof 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 : ℚ
n m : ℕ
inst✝ : AP (p ≄ 0)
ctx : Integer.Induction.Context fun x => (p : ℚ) → [inst : AP (p ≄ 0)] → ℚ :=
  Lean4Axiomatic.Rational.Impl.Generic.ind_ctx
this :
  ctx.rec_diff (Coe.coe n - Coe.coe m) ≃
    Integer.Induction.Context.on_diff (motive := fun x => (p : ℚ) → [inst : AP (p ≄ 0)] → ℚ) n m
⊢ p ^ (Coe.coe n - Coe.coe m) ≃ p ^ n / p ^ m
Theorem: Lean4Axiomatic.Rational.Impl.Generic.pow_diff
Proof 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 : ℚ
n m : ℕ
inst✝ : AP (p ≄ 0)
ctx : Integer.Induction.Context fun x => (p : ℚ) → [inst : AP (p ≄ 0)] → ℚ :=
  Lean4Axiomatic.Rational.Impl.Generic.ind_ctx
this :
  ctx.rec_diff (Coe.coe n - Coe.coe m) ≃
    Integer.Induction.Context.on_diff (motive := fun x => (p : ℚ) → [inst : AP (p ≄ 0)] → ℚ) n m
⊢ p ^ (Coe.coe n - Coe.coe m) ≃ p ^ n / p ^ m
Tactic:
have rec_eval
  : (x : ℚ) → [AP (x ≄ 0)] → ctx.rec_diff ((n:ℤ) - m) x ≃ ctx.on_diff n m x
  := this
Proof 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 : ℚ
n m : ℕ
inst✝ : AP (p ≄ 0)
ctx : Integer.Induction.Context fun x => (p : ℚ) → [inst : AP (p ≄ 0)] → ℚ :=
  Lean4Axiomatic.Rational.Impl.Generic.ind_ctx
this :
  ctx.rec_diff (Coe.coe n - Coe.coe m) ≃
    Integer.Induction.Context.on_diff (motive := fun x => (p : ℚ) → [inst : AP (p ≄ 0)] → ℚ) n m
rec_eval :
  ∀ (x : ℚ) [inst : AP (x ≄ 0)],
    ctx.rec_diff (Coe.coe n - Coe.coe m) x ≃
      Integer.Induction.Context.on_diff (motive := fun x => (p : ℚ) → [inst : AP (p ≄ 0)] → ℚ) n m x
⊢ p ^ (Coe.coe n - Coe.coe m) ≃ p ^ n / p ^ m
Theorem: Lean4Axiomatic.Rational.Impl.Generic.pow_diff
Proof 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 : ℚ
n m : ℕ
inst✝ : AP (p ≄ 0)
ctx : Integer.Induction.Context fun x => (p : ℚ) → [inst : AP (p ≄ 0)] → ℚ :=
  Lean4Axiomatic.Rational.Impl.Generic.ind_ctx
this :
  ctx.rec_diff (Coe.coe n - Coe.coe m) ≃
    Integer.Induction.Context.on_diff (motive := fun x => (p : ℚ) → [inst : AP (p ≄ 0)] → ℚ) n m
rec_eval :
  ∀ (x : ℚ) [inst : AP (x ≄ 0)],
    ctx.rec_diff (Coe.coe n - Coe.coe m) x ≃
      Integer.Induction.Context.on_diff (motive := fun x => (p : ℚ) → [inst : AP (p ≄ 0)] → ℚ) n m x
⊢ p ^ (Coe.coe n - Coe.coe m) ≃ p ^ n / p ^ m
Tactic:
calc
  _ = p^((n:ℤ) - m)              := rfl
  _ = _pow p ((n:ℤ) - m)         := rfl
  _ = ctx.rec_diff ((n:ℤ) - m) p := rfl
  _ ≃ ctx.on_diff n m p          := rec_eval p
  _ = on_diff_pow n m p          := rfl
  _ = p^n / p^m                  := rfl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Generic.pow_substR
Proof 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₂)
Proof 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₂
Theorem: Lean4Axiomatic.Rational.Impl.Generic.pow_substR
Proof 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 (ℚ := ℚ)
Proof 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₂
Theorem: Lean4Axiomatic.Rational.Impl.Generic.pow_substR
Proof 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₂›
Proof 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₂
Theorem: Lean4Axiomatic.Rational.Impl.Generic.pow_substR
Proof 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
Proof 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₂
Theorem: Lean4Axiomatic.Rational.Impl.Generic.pow_substR
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.le_subst_step
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ : ℕ
⊢ n₁ ≤ n₂ → step n₁ ≤ step n₂
Tactic:
intro (_ : n₁ ≤ n₂)
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ : ℕ
x✝ : n₁ ≤ n₂
⊢ step n₁ ≤ step n₂
Theorem: Lean4Axiomatic.Natural.le_subst_step
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ : ℕ
x✝ : n₁ ≤ n₂
⊢ step n₁ ≤ step n₂
Tactic:
have ⟨d, (_ : n₁ + d ≃ n₂)⟩ := le_defn.mp ‹n₁ ≤ n₂›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ : ℕ
x✝ : n₁ ≤ n₂
d : ℕ
h✝ : n₁ + d ≃ n₂
⊢ step n₁ ≤ step n₂
Theorem: Lean4Axiomatic.Natural.le_subst_step
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ : ℕ
x✝ : n₁ ≤ n₂
d : ℕ
h✝ : n₁ + d ≃ n₂
⊢ step n₁ ≤ step n₂
Tactic:
apply le_defn.mpr
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ : ℕ
x✝ : n₁ ≤ n₂
d : ℕ
h✝ : n₁ + d ≃ n₂
⊢ ∃ k, step n₁ + k ≃ step n₂
Theorem: Lean4Axiomatic.Natural.le_subst_step
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ : ℕ
x✝ : n₁ ≤ n₂
d : ℕ
h✝ : n₁ + d ≃ n₂
⊢ ∃ k, step n₁ + k ≃ step n₂
Tactic:
exists d
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ : ℕ
x✝ : n₁ ≤ n₂
d : ℕ
h✝ : n₁ + d ≃ n₂
⊢ step n₁ + d ≃ step n₂
Theorem: Lean4Axiomatic.Natural.le_subst_step
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ : ℕ
x✝ : n₁ ≤ n₂
d : ℕ
h✝ : n₁ + d ≃ n₂
⊢ step n₁ + d ≃ step n₂
Tactic:
calc
  step n₁ + d   ≃ _ := step_add
  step (n₁ + d) ≃ _ := AA.subst₁ ‹n₁ + d ≃ n₂›
  step n₂       ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.le_inject_step
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ : ℕ
⊢ step n₁ ≤ step n₂ → n₁ ≤ n₂
Tactic:
intro (_ : step n₁ ≤ step n₂)
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ : ℕ
x✝ : step n₁ ≤ step n₂
⊢ n₁ ≤ n₂
Theorem: Lean4Axiomatic.Natural.le_inject_step
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ : ℕ
x✝ : step n₁ ≤ step n₂
⊢ n₁ ≤ n₂
Tactic:
have ⟨d, (_ : step n₁ + d ≃ step n₂)⟩ := le_defn.mp ‹step n₁ ≤ step n₂›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ : ℕ
x✝ : step n₁ ≤ step n₂
d : ℕ
h✝ : step n₁ + d ≃ step n₂
⊢ n₁ ≤ n₂
Theorem: Lean4Axiomatic.Natural.le_inject_step
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ : ℕ
x✝ : step n₁ ≤ step n₂
d : ℕ
h✝ : step n₁ + d ≃ step n₂
⊢ n₁ ≤ n₂
Tactic:
apply le_defn.mpr
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ : ℕ
x✝ : step n₁ ≤ step n₂
d : ℕ
h✝ : step n₁ + d ≃ step n₂
⊢ ∃ k, n₁ + k ≃ n₂
Theorem: Lean4Axiomatic.Natural.le_inject_step
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ : ℕ
x✝ : step n₁ ≤ step n₂
d : ℕ
h✝ : step n₁ + d ≃ step n₂
⊢ ∃ k, n₁ + k ≃ n₂
Tactic:
exists d
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ : ℕ
x✝ : step n₁ ≤ step n₂
d : ℕ
h✝ : step n₁ + d ≃ step n₂
⊢ n₁ + d ≃ n₂
Theorem: Lean4Axiomatic.Natural.le_inject_step
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ : ℕ
x✝ : step n₁ ≤ step n₂
d : ℕ
h✝ : step n₁ + d ≃ step n₂
⊢ n₁ + d ≃ n₂
Tactic:
have : step (n₁ + d) ≃ step n₂ := calc
  step (n₁ + d) ≃ _ := Rel.symm step_add
  step n₁ + d   ≃ _ := ‹step n₁ + d ≃ step n₂›
  step n₂       ≃ _ := Rel.refl
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ : ℕ
x✝ : step n₁ ≤ step n₂
d : ℕ
h✝ : step n₁ + d ≃ step n₂
this : step (n₁ + d) ≃ step n₂
⊢ n₁ + d ≃ n₂
Theorem: Lean4Axiomatic.Natural.le_inject_step
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ : ℕ
x✝ : step n₁ ≤ step n₂
d : ℕ
h✝ : step n₁ + d ≃ step n₂
this : step (n₁ + d) ≃ step n₂
⊢ n₁ + d ≃ n₂
Tactic:
exact AA.inject ‹step (n₁ + d) ≃ step n₂›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.le_subst_eqv
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
⊢ n₁ ≃ n₂ → n₁ ≤ m → n₂ ≤ m
Tactic:
intro (_ : n₁ ≃ n₂) (_ : n₁ ≤ m)
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : n₁ ≤ m
⊢ n₂ ≤ m
Theorem: Lean4Axiomatic.Natural.le_subst_eqv
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : n₁ ≤ m
⊢ n₂ ≤ m
Tactic:
have ⟨d, (_ : n₁ + d ≃ m)⟩ := le_defn.mp ‹n₁ ≤ m›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : n₁ ≤ m
d : ℕ
h✝ : n₁ + d ≃ m
⊢ n₂ ≤ m
Theorem: Lean4Axiomatic.Natural.le_subst_eqv
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : n₁ ≤ m
d : ℕ
h✝ : n₁ + d ≃ m
⊢ n₂ ≤ m
Tactic:
apply le_defn.mpr
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : n₁ ≤ m
d : ℕ
h✝ : n₁ + d ≃ m
⊢ ∃ k, n₂ + k ≃ m
Theorem: Lean4Axiomatic.Natural.le_subst_eqv
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : n₁ ≤ m
d : ℕ
h✝ : n₁ + d ≃ m
⊢ ∃ k, n₂ + k ≃ m
Tactic:
exists d
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : n₁ ≤ m
d : ℕ
h✝ : n₁ + d ≃ m
⊢ n₂ + d ≃ m
Theorem: Lean4Axiomatic.Natural.le_subst_eqv
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : n₁ ≤ m
d : ℕ
h✝ : n₁ + d ≃ m
⊢ n₂ + d ≃ m
Tactic:
calc
  n₂ + d ≃ _ := Rel.symm (AA.substL ‹n₁ ≃ n₂›)
  n₁ + d ≃ _ := ‹n₁ + d ≃ m›
  m      ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.trans_eqv_le_le
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
⊢ n ≃ m → m ≤ k → n ≤ k
Tactic:
intro (_ : n ≃ m) (_ : m ≤ k)
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n ≃ m
x✝ : m ≤ k
⊢ n ≤ k
Theorem: Lean4Axiomatic.Natural.trans_eqv_le_le
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n ≃ m
x✝ : m ≤ k
⊢ n ≤ k
Tactic:
exact le_subst_eqv (Rel.symm ‹n ≃ m›) ‹m ≤ k›
Proof state after:
no goals