internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_negative
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Negative (n——m)
this : n < m
⊢ (n——m).sgn ≃ -1
Tactic:
have : compare n m = Ordering.lt := Natural.compare_lt.mpr this
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Negative (n——m)
this✝ : n < m
this : compare n m = Ordering.lt
⊢ (n——m).sgn ≃ -1
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_negative
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Negative (n——m)
this✝ : n < m
this : compare n m = Ordering.lt
⊢ (n——m).sgn ≃ -1
Tactic:
have : ord_sgn (compare n m) ≃ ord_sgn Ordering.lt :=
  ord_sgn_subst (ℤ := Difference ℕ) this
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Negative (n——m)
this✝¹ : n < m
this✝ : compare n m = Ordering.lt
this : ord_sgn (compare n m) ≃ ord_sgn Ordering.lt
⊢ (n——m).sgn ≃ -1
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_negative
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Negative (n——m)
this✝¹ : n < m
this✝ : compare n m = Ordering.lt
this : ord_sgn (compare n m) ≃ ord_sgn Ordering.lt
⊢ (n——m).sgn ≃ -1
Tactic:
have : ord_sgn (compare n m) ≃ (-1:Difference ℕ) := this
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Negative (n——m)
this✝² : n < m
this✝¹ : compare n m = Ordering.lt
this✝ : ord_sgn (compare n m) ≃ ord_sgn Ordering.lt
this : ord_sgn (compare n m) ≃ -1
⊢ (n——m).sgn ≃ -1
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_negative
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Negative (n——m)
this✝² : n < m
this✝¹ : compare n m = Ordering.lt
this✝ : ord_sgn (compare n m) ≃ ord_sgn Ordering.lt
this : ord_sgn (compare n m) ≃ -1
⊢ (n——m).sgn ≃ -1
Tactic:
have : sgn (n——m) ≃ -1 := this
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Negative (n——m)
this✝³ : n < m
this✝² : compare n m = Ordering.lt
this✝¹ : ord_sgn (compare n m) ≃ ord_sgn Ordering.lt
this✝ : ord_sgn (compare n m) ≃ -1
this : (n——m).sgn ≃ -1
⊢ (n——m).sgn ≃ -1
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_negative
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Negative (n——m)
this✝³ : n < m
this✝² : compare n m = Ordering.lt
this✝¹ : ord_sgn (compare n m) ≃ ord_sgn Ordering.lt
this✝ : ord_sgn (compare n m) ≃ -1
this : (n——m).sgn ≃ -1
⊢ (n——m).sgn ≃ -1
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_negative
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (n——m).sgn ≃ -1 → Negative (n——m)
Tactic:
intro (_ : sgn (n——m) ≃ -1)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : (n——m).sgn ≃ -1
⊢ Negative (n——m)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_negative
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : (n——m).sgn ≃ -1
⊢ Negative (n——m)
Tactic:
have : ord_sgn (compare n m) ≃ (-1:Difference ℕ) := ‹sgn (n——m) ≃ -1›
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : (n——m).sgn ≃ -1
this : ord_sgn (compare n m) ≃ -1
⊢ Negative (n——m)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_negative
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : (n——m).sgn ≃ -1
this : ord_sgn (compare n m) ≃ -1
⊢ Negative (n——m)
Tactic:
have : ord_sgn (compare n m) ≃ ord_sgn Ordering.lt := this
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : (n——m).sgn ≃ -1
this✝ : ord_sgn (compare n m) ≃ -1
this : ord_sgn (compare n m) ≃ ord_sgn Ordering.lt
⊢ Negative (n——m)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_negative
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : (n——m).sgn ≃ -1
this✝ : ord_sgn (compare n m) ≃ -1
this : ord_sgn (compare n m) ≃ ord_sgn Ordering.lt
⊢ Negative (n——m)
Tactic:
have : compare n m = Ordering.lt := ord_sgn_inject this
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : (n——m).sgn ≃ -1
this✝¹ : ord_sgn (compare n m) ≃ -1
this✝ : ord_sgn (compare n m) ≃ ord_sgn Ordering.lt
this : compare n m = Ordering.lt
⊢ Negative (n——m)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_negative
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : (n——m).sgn ≃ -1
this✝¹ : ord_sgn (compare n m) ≃ -1
this✝ : ord_sgn (compare n m) ≃ ord_sgn Ordering.lt
this : compare n m = Ordering.lt
⊢ Negative (n——m)
Tactic:
have : n < m := Natural.compare_lt.mp this
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : (n——m).sgn ≃ -1
this✝² : ord_sgn (compare n m) ≃ -1
this✝¹ : ord_sgn (compare n m) ≃ ord_sgn Ordering.lt
this✝ : compare n m = Ordering.lt
this : n < m
⊢ Negative (n——m)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_negative
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : (n——m).sgn ≃ -1
this✝² : ord_sgn (compare n m) ≃ -1
this✝¹ : ord_sgn (compare n m) ≃ ord_sgn Ordering.lt
this✝ : compare n m = Ordering.lt
this : n < m
⊢ Negative (n——m)
Tactic:
have : Negative (n——m) := neg_diff_lt.mpr this
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : (n——m).sgn ≃ -1
this✝³ : ord_sgn (compare n m) ≃ -1
this✝² : ord_sgn (compare n m) ≃ ord_sgn Ordering.lt
this✝¹ : compare n m = Ordering.lt
this✝ : n < m
this : Negative (n——m)
⊢ Negative (n——m)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_negative
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : (n——m).sgn ≃ -1
this✝³ : ord_sgn (compare n m) ≃ -1
this✝² : ord_sgn (compare n m) ≃ ord_sgn Ordering.lt
this✝¹ : compare n m = Ordering.lt
this✝ : n < m
this : Negative (n——m)
⊢ Negative (n——m)
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_preserves_sign
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
s a b : Difference ℕ
⊢ a.sgn ≃ s → b.sgn ≃ s → (a + b).sgn ≃ s
Tactic:
revert a
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
s b : Difference ℕ
⊢ ∀ {a : Difference ℕ}, a.sgn ≃ s → b.sgn ≃ s → (a + b).sgn ≃ s
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_preserves_sign
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
s b : Difference ℕ
⊢ ∀ {a : Difference ℕ}, a.sgn ≃ s → b.sgn ≃ s → (a + b).sgn ≃ s
Tactic:
intro (n——m)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
s b : Difference ℕ
n m : ℕ
⊢ (n——m).sgn ≃ s → b.sgn ≃ s → (n——m + b).sgn ≃ s
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_preserves_sign
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
s b : Difference ℕ
n m : ℕ
⊢ (n——m).sgn ≃ s → b.sgn ≃ s → (n——m + b).sgn ≃ s
Tactic:
revert b
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
s : Difference ℕ
n m : ℕ
⊢ ∀ {b : Difference ℕ}, (n——m).sgn ≃ s → b.sgn ≃ s → (n——m + b).sgn ≃ s
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_preserves_sign
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
s : Difference ℕ
n m : ℕ
⊢ ∀ {b : Difference ℕ}, (n——m).sgn ≃ s → b.sgn ≃ s → (n——m + b).sgn ≃ s
Tactic:
intro (k——j)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
s : Difference ℕ
n m k j : ℕ
⊢ (n——m).sgn ≃ s → (k——j).sgn ≃ s → (n——m + k——j).sgn ≃ s
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_preserves_sign
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
s : Difference ℕ
n m k j : ℕ
⊢ (n——m).sgn ≃ s → (k——j).sgn ≃ s → (n——m + k——j).sgn ≃ s
Tactic:
intro (_ : sgn (n——m) ≃ s) (_ : sgn (k——j) ≃ s)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
s : Difference ℕ
n m k j : ℕ
x✝¹ : (n——m).sgn ≃ s
x✝ : (k——j).sgn ≃ s
⊢ (n——m + k——j).sgn ≃ s
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_preserves_sign
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
s : Difference ℕ
n m k j : ℕ
x✝¹ : (n——m).sgn ≃ s
x✝ : (k——j).sgn ≃ s
⊢ (n——m + k——j).sgn ≃ s
Tactic:
have : ord_sgn (compare n m) ≃ s := ‹sgn (n——m) ≃ s›
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
s : Difference ℕ
n m k j : ℕ
x✝¹ : (n——m).sgn ≃ s
x✝ : (k——j).sgn ≃ s
this : ord_sgn (compare n m) ≃ s
⊢ (n——m + k——j).sgn ≃ s
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_preserves_sign
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
s : Difference ℕ
n m k j : ℕ
x✝¹ : (n——m).sgn ≃ s
x✝ : (k——j).sgn ≃ s
this : ord_sgn (compare n m) ≃ s
⊢ (n——m + k——j).sgn ≃ s
Tactic:
have : ord_sgn (compare k j) ≃ s := ‹sgn (k——j) ≃ s›
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
s : Difference ℕ
n m k j : ℕ
x✝¹ : (n——m).sgn ≃ s
x✝ : (k——j).sgn ≃ s
this✝ : ord_sgn (compare n m) ≃ s
this : ord_sgn (compare k j) ≃ s
⊢ (n——m + k——j).sgn ≃ s
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_preserves_sign
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
s : Difference ℕ
n m k j : ℕ
x✝¹ : (n——m).sgn ≃ s
x✝ : (k——j).sgn ≃ s
this✝ : ord_sgn (compare n m) ≃ s
this : ord_sgn (compare k j) ≃ s
⊢ (n——m + k——j).sgn ≃ s
Tactic:
have : ord_sgn (compare n m) ≃ ord_sgn (compare k j) :=
  Rel.trans ‹ord_sgn (compare n m) ≃ s› (Rel.symm this)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
s : Difference ℕ
n m k j : ℕ
x✝¹ : (n——m).sgn ≃ s
x✝ : (k——j).sgn ≃ s
this✝¹ : ord_sgn (compare n m) ≃ s
this✝ : ord_sgn (compare k j) ≃ s
this : ord_sgn (compare n m) ≃ ord_sgn (compare k j)
⊢ (n——m + k——j).sgn ≃ s
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_preserves_sign
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
s : Difference ℕ
n m k j : ℕ
x✝¹ : (n——m).sgn ≃ s
x✝ : (k——j).sgn ≃ s
this✝¹ : ord_sgn (compare n m) ≃ s
this✝ : ord_sgn (compare k j) ≃ s
this : ord_sgn (compare n m) ≃ ord_sgn (compare k j)
⊢ (n——m + k——j).sgn ≃ s
Tactic:
have : compare n m = compare k j := ord_sgn_inject this
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
s : Difference ℕ
n m k j : ℕ
x✝¹ : (n——m).sgn ≃ s
x✝ : (k——j).sgn ≃ s
this✝² : ord_sgn (compare n m) ≃ s
this✝¹ : ord_sgn (compare k j) ≃ s
this✝ : ord_sgn (compare n m) ≃ ord_sgn (compare k j)
this : compare n m = compare k j
⊢ (n——m + k——j).sgn ≃ s
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_preserves_sign
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
s : Difference ℕ
n m k j : ℕ
x✝¹ : (n——m).sgn ≃ s
x✝ : (k——j).sgn ≃ s
this✝² : ord_sgn (compare n m) ≃ s
this✝¹ : ord_sgn (compare k j) ≃ s
this✝ : ord_sgn (compare n m) ≃ ord_sgn (compare k j)
this : compare n m = compare k j
⊢ (n——m + k——j).sgn ≃ s
Tactic:
have : compare (n + k) (m + j) = compare k j :=
  Natural.add_preserves_compare this rfl
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
s : Difference ℕ
n m k j : ℕ
x✝¹ : (n——m).sgn ≃ s
x✝ : (k——j).sgn ≃ s
this✝³ : ord_sgn (compare n m) ≃ s
this✝² : ord_sgn (compare k j) ≃ s
this✝¹ : ord_sgn (compare n m) ≃ ord_sgn (compare k j)
this✝ : compare n m = compare k j
this : compare (n + k) (m + j) = compare k j
⊢ (n——m + k——j).sgn ≃ s
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_preserves_sign
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
s : Difference ℕ
n m k j : ℕ
x✝¹ : (n——m).sgn ≃ s
x✝ : (k——j).sgn ≃ s
this✝³ : ord_sgn (compare n m) ≃ s
this✝² : ord_sgn (compare k j) ≃ s
this✝¹ : ord_sgn (compare n m) ≃ ord_sgn (compare k j)
this✝ : compare n m = compare k j
this : compare (n + k) (m + j) = compare k j
⊢ (n——m + k——j).sgn ≃ s
Tactic:
have : sgn (n——m + k——j) ≃ s := calc
  sgn (n——m + k——j)                 ≃ _ := Rel.refl
  sgn ((n + k)——(m + j))            ≃ _ := Rel.refl
  ord_sgn (compare (n + k) (m + j)) ≃ _ := ord_sgn_subst this
  ord_sgn (compare k j)             ≃ _ := ‹ord_sgn (compare k j) ≃ s›
  s                                 ≃ _ := Rel.refl
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
s : Difference ℕ
n m k j : ℕ
x✝¹ : (n——m).sgn ≃ s
x✝ : (k——j).sgn ≃ s
this✝⁴ : ord_sgn (compare n m) ≃ s
this✝³ : ord_sgn (compare k j) ≃ s
this✝² : ord_sgn (compare n m) ≃ ord_sgn (compare k j)
this✝¹ : compare n m = compare k j
this✝ : compare (n + k) (m + j) = compare k j
this : (n——m + k——j).sgn ≃ s
⊢ (n——m + k——j).sgn ≃ s
Theorem: Lean4Axiomatic.Integer.Impl.Difference.add_preserves_sign
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
s : Difference ℕ
n m k j : ℕ
x✝¹ : (n——m).sgn ≃ s
x✝ : (k——j).sgn ≃ s
this✝⁴ : ord_sgn (compare n m) ≃ s
this✝³ : ord_sgn (compare k j) ≃ s
this✝² : ord_sgn (compare n m) ≃ ord_sgn (compare k j)
this✝¹ : compare n m = compare k j
this✝ : compare (n + k) (m + j) = compare k j
this : (n——m + k——j).sgn ≃ s
⊢ (n——m + k——j).sgn ≃ s
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.pow_substL
Proof state before:
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x₁ x₂ : α
m : ℕ
⊢ x₁ ≃ x₂ → x₁ ^ m ≃ x₂ ^ m
Tactic:
intro (_ : x₁ ≃ x₂)
Proof state after:
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x₁ x₂ : α
m : ℕ
x✝ : x₁ ≃ x₂
⊢ x₁ ^ m ≃ x₂ ^ m
Theorem: Lean4Axiomatic.Natural.pow_substL
Proof state before:
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x₁ x₂ : α
m : ℕ
x✝ : x₁ ≃ x₂
⊢ x₁ ^ m ≃ x₂ ^ m
Tactic:
apply ind_on (motive := λ y => x₁ ^ y ≃ x₂ ^ y) m
Proof state after:
case zero
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x₁ x₂ : α
m : ℕ
x✝ : x₁ ≃ x₂
⊢ x₁ ^ 0 ≃ x₂ ^ 0

case step
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x₁ x₂ : α
m : ℕ
x✝ : x₁ ≃ x₂
⊢ ∀ (m : ℕ), x₁ ^ m ≃ x₂ ^ m → x₁ ^ step m ≃ x₂ ^ step m
Theorem: Lean4Axiomatic.Natural.pow_substL
Proof state before:
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x₁ x₂ : α
m : ℕ
x✝ : x₁ ≃ x₂
⊢ x₁ ^ 0 ≃ x₂ ^ 0
Tactic:
case zero =>
  show x₁ ^ 0 ≃ x₂ ^ 0
  calc
    _ ≃ x₁ ^ 0 := Rel.refl
    _ ≃ 1      := pow_zero
    _ ≃ x₂ ^ 0 := Rel.symm pow_zero
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.pow_substL
Proof state before:
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x₁ x₂ : α
m : ℕ
x✝ : x₁ ≃ x₂
⊢ ∀ (m : ℕ), x₁ ^ m ≃ x₂ ^ m → x₁ ^ step m ≃ x₂ ^ step m
Tactic:
case step =>
  intro (m' : ℕ) (ih : x₁ ^ m' ≃ x₂ ^ m')
  show x₁ ^ step m' ≃ x₂ ^ step m'
  calc
    _ ≃ x₁ ^ step m' := Rel.refl
    _ ≃ x₁ ^ m' * x₁ := pow_step
    _ ≃ x₂ ^ m' * x₁ := AA.substL ih
    _ ≃ x₂ ^ m' * x₂ := AA.substR ‹x₁ ≃ x₂›
    _ ≃ x₂ ^ step m' := Rel.symm pow_step
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.pow_substL
Proof state before:
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x₁ x₂ : α
m : ℕ
x✝ : x₁ ≃ x₂
⊢ x₁ ^ 0 ≃ x₂ ^ 0
Tactic:
calc
  _ ≃ x₁ ^ 0 := Rel.refl
  _ ≃ 1      := pow_zero
  _ ≃ x₂ ^ 0 := Rel.symm pow_zero
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.pow_substL
Proof state before:
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x₁ x₂ : α
m : ℕ
x✝ : x₁ ≃ x₂
⊢ ∀ (m : ℕ), x₁ ^ m ≃ x₂ ^ m → x₁ ^ step m ≃ x₂ ^ step m
Tactic:
intro (m' : ℕ) (ih : x₁ ^ m' ≃ x₂ ^ m')
Proof state after:
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x₁ x₂ : α
m : ℕ
x✝ : x₁ ≃ x₂
m' : ℕ
ih : x₁ ^ m' ≃ x₂ ^ m'
⊢ x₁ ^ step m' ≃ x₂ ^ step m'
Theorem: Lean4Axiomatic.Natural.pow_substL
Proof state before:
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x₁ x₂ : α
m : ℕ
x✝ : x₁ ≃ x₂
m' : ℕ
ih : x₁ ^ m' ≃ x₂ ^ m'
⊢ x₁ ^ step m' ≃ x₂ ^ step m'
Tactic:
calc
  _ ≃ x₁ ^ step m' := Rel.refl
  _ ≃ x₁ ^ m' * x₁ := pow_step
  _ ≃ x₂ ^ m' * x₁ := AA.substL ih
  _ ≃ x₂ ^ m' * x₂ := AA.substR ‹x₁ ≃ x₂›
  _ ≃ x₂ ^ step m' := Rel.symm pow_step
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.pow_substR
Proof state before:
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x : α
n₁ n₂ : ℕ
⊢ n₁ ≃ n₂ → x ^ n₁ ≃ x ^ n₂
Tactic:
apply ind_on (motive := λ k => ∀ {j}, k ≃ j → x ^ k ≃ x ^ j) n₁
Proof state after:
case zero
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x : α
n₁ n₂ : ℕ
⊢ ∀ {j : ℕ}, 0 ≃ j → x ^ 0 ≃ x ^ j

case step
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x : α
n₁ n₂ : ℕ
⊢ ∀ (m : ℕ), (∀ {j : ℕ}, m ≃ j → x ^ m ≃ x ^ j) → ∀ {j : ℕ}, step m ≃ j → x ^ step m ≃ x ^ j
Theorem: Lean4Axiomatic.Natural.pow_substR
Proof state before:
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x : α
n₁ n₂ : ℕ
⊢ ∀ {j : ℕ}, 0 ≃ j → x ^ 0 ≃ x ^ j
Tactic:
case zero =>
  intro (n₂ : ℕ)
  show 0 ≃ n₂ → x ^ 0 ≃ x ^ n₂
  apply cases_on (motive := λ j => 0 ≃ j → x ^ 0 ≃ x ^ j) n₂
  case zero =>
    intro (_ : (0 : ℕ) ≃ 0)
    show x ^ 0 ≃ x ^ 0
    exact Rel.refl
  case step =>
    intro (n₂' : ℕ) (_ : 0 ≃ step n₂')
    show x ^ 0 ≃ x ^ step n₂'
    exact absurd ‹0 ≃ step n₂'› (Rel.symm step_neqv_zero)
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.pow_substR
Proof state before:
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x : α
n₁ n₂ : ℕ
⊢ ∀ (m : ℕ), (∀ {j : ℕ}, m ≃ j → x ^ m ≃ x ^ j) → ∀ {j : ℕ}, step m ≃ j → x ^ step m ≃ x ^ j
Tactic:
case step =>
  intro (n₁' : ℕ) (ih : ∀ {j}, n₁' ≃ j → x ^ n₁' ≃ x ^ j) (n₂ : ℕ)
  show step n₁' ≃ n₂ → x ^ step n₁' ≃ x ^ n₂
  apply cases_on (motive := λ j => step n₁' ≃ j → x ^ step n₁' ≃ x ^ j) n₂
  case zero =>
    intro (_ : step n₁' ≃ 0)
    show x ^ step n₁' ≃ x ^ 0
    exact absurd ‹step n₁' ≃ 0› step_neqv_zero
  case step =>
    intro (n₂' : ℕ) (_ : step n₁' ≃ step n₂')
    show x ^ step n₁' ≃ x ^ step n₂'
    have : n₁' ≃ n₂' := AA.inject ‹step n₁' ≃ step n₂'›
    calc
      _ ≃ x ^ step n₁' := Rel.refl
      _ ≃ x ^ n₁' * x  := pow_step
      _ ≃ x ^ n₂' * x  := AA.substL (ih ‹n₁' ≃ n₂'›)
      _ ≃ x ^ step n₂' := Rel.symm pow_step
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.pow_substR
Proof state before:
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x : α
n₁ n₂ : ℕ
⊢ ∀ {j : ℕ}, 0 ≃ j → x ^ 0 ≃ x ^ j
Tactic:
intro (n₂ : ℕ)
Proof state after:
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x : α
n₁ n₂✝ n₂ : ℕ
⊢ 0 ≃ n₂ → x ^ 0 ≃ x ^ n₂
Theorem: Lean4Axiomatic.Natural.pow_substR
Proof state before:
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x : α
n₁ n₂✝ n₂ : ℕ
⊢ 0 ≃ n₂ → x ^ 0 ≃ x ^ n₂
Tactic:
apply cases_on (motive := λ j => 0 ≃ j → x ^ 0 ≃ x ^ j) n₂
Proof state after:
case zero
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x : α
n₁ n₂✝ n₂ : ℕ
⊢ 0 ≃ 0 → x ^ 0 ≃ x ^ 0

case step
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x : α
n₁ n₂✝ n₂ : ℕ
⊢ ∀ (m : ℕ), 0 ≃ step m → x ^ 0 ≃ x ^ step m
Theorem: Lean4Axiomatic.Natural.pow_substR
Proof state before:
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x : α
n₁ n₂✝ n₂ : ℕ
⊢ 0 ≃ 0 → x ^ 0 ≃ x ^ 0
Tactic:
case zero =>
  intro (_ : (0 : ℕ) ≃ 0)
  show x ^ 0 ≃ x ^ 0
  exact Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.pow_substR
Proof state before:
ℕ : Type
inst✝⁸ : Core ℕ
inst✝⁷ : Induction ℕ
inst✝⁶ : Addition ℕ
inst✝⁵ : Sign ℕ
inst✝⁴ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝³ : EqvOp α
inst✝² : OfNat α 1
inst✝¹ : Exponentiation ℕ mul
inst✝ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
x : α
n₁ n₂✝ n₂ : ℕ
⊢ ∀ (m : ℕ), 0 ≃ step m → x ^ 0 ≃ x ^ step m
Tactic:
case step =>
  intro (n₂' : ℕ) (_ : 0 ≃ step n₂')
  show x ^ 0 ≃ x ^ step n₂'
  exact absurd ‹0 ≃ step n₂'› (Rel.symm step_neqv_zero)
Proof state after:
no goals