internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sign_trichotomy
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
natOrderTri : AA.ExactlyOneOfThree (n < m) (n ≃ m) (n > m)
⊢ AA.OneOfThree (n——m ≃ 0) (Positive (n——m)) (Negative (n——m))
Tactic:
match natOrderTri.atLeastOne with
| AA.OneOfThree.first (_ : n < m) =>
  have : Negative (n——m) := neg_diff_lt.mpr ‹n < m›
  exact AA.OneOfThree.third ‹Negative (n——m)›
| AA.OneOfThree.second (_ : n ≃ m) =>
  have : n——m ≃ 0 := zero_diff_eqv.mpr ‹n ≃ m›
  exact AA.OneOfThree.first ‹n——m ≃ 0›
| AA.OneOfThree.third (_ : n > m) =>
  have : Positive (n——m) := pos_diff_gt.mpr ‹n > m›
  exact AA.OneOfThree.second ‹Positive (n——m)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sign_trichotomy
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
natOrderTri : AA.ExactlyOneOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
⊢ AA.OneOfThree (n——m ≃ 0) (Positive (n——m)) (Negative (n——m))
Tactic:
have : Negative (n——m) := neg_diff_lt.mpr ‹n < m›
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
natOrderTri : AA.ExactlyOneOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
this : Negative (n——m)
⊢ AA.OneOfThree (n——m ≃ 0) (Positive (n——m)) (Negative (n——m))
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sign_trichotomy
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
natOrderTri : AA.ExactlyOneOfThree (n < m) (n ≃ m) (n > m)
a✝ : n < m
this : Negative (n——m)
⊢ AA.OneOfThree (n——m ≃ 0) (Positive (n——m)) (Negative (n——m))
Tactic:
exact AA.OneOfThree.third ‹Negative (n——m)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sign_trichotomy
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
natOrderTri : AA.ExactlyOneOfThree (n < m) (n ≃ m) (n > m)
b✝ : n ≃ m
⊢ AA.OneOfThree (n——m ≃ 0) (Positive (n——m)) (Negative (n——m))
Tactic:
have : n——m ≃ 0 := zero_diff_eqv.mpr ‹n ≃ m›
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
natOrderTri : AA.ExactlyOneOfThree (n < m) (n ≃ m) (n > m)
b✝ : n ≃ m
this : n——m ≃ 0
⊢ AA.OneOfThree (n——m ≃ 0) (Positive (n——m)) (Negative (n——m))
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sign_trichotomy
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
natOrderTri : AA.ExactlyOneOfThree (n < m) (n ≃ m) (n > m)
b✝ : n ≃ m
this : n——m ≃ 0
⊢ AA.OneOfThree (n——m ≃ 0) (Positive (n——m)) (Negative (n——m))
Tactic:
exact AA.OneOfThree.first ‹n——m ≃ 0›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sign_trichotomy
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
natOrderTri : AA.ExactlyOneOfThree (n < m) (n ≃ m) (n > m)
c✝ : n > m
⊢ AA.OneOfThree (n——m ≃ 0) (Positive (n——m)) (Negative (n——m))
Tactic:
have : Positive (n——m) := pos_diff_gt.mpr ‹n > m›
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
natOrderTri : AA.ExactlyOneOfThree (n < m) (n ≃ m) (n > m)
c✝ : n > m
this : Positive (n——m)
⊢ AA.OneOfThree (n——m ≃ 0) (Positive (n——m)) (Negative (n——m))
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sign_trichotomy
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
natOrderTri : AA.ExactlyOneOfThree (n < m) (n ≃ m) (n > m)
c✝ : n > m
this : Positive (n——m)
⊢ AA.OneOfThree (n——m ≃ 0) (Positive (n——m)) (Negative (n——m))
Tactic:
exact AA.OneOfThree.second ‹Positive (n——m)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sign_trichotomy
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
natOrderTri : AA.ExactlyOneOfThree (n < m) (n ≃ m) (n > m)
⊢ ¬AA.TwoOfThree (n——m ≃ 0) (Positive (n——m)) (Negative (n——m))
Tactic:
intro (h : AA.TwoOfThree (n——m ≃ 0) (Positive (n——m)) (Negative (n——m)))
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
natOrderTri : AA.ExactlyOneOfThree (n < m) (n ≃ m) (n > m)
h : AA.TwoOfThree (n——m ≃ 0) (Positive (n——m)) (Negative (n——m))
⊢ False
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sign_trichotomy
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
natOrderTri : AA.ExactlyOneOfThree (n < m) (n ≃ m) (n > m)
h : AA.TwoOfThree (n——m ≃ 0) (Positive (n——m)) (Negative (n——m))
⊢ False
Tactic:
have twoOfThree : AA.TwoOfThree (n < m) (n ≃ m) (n > m) := match h with
| AA.TwoOfThree.oneAndTwo (_ : n——m ≃ 0) (_ : Positive (n——m)) =>
  have : n ≃ m := zero_diff_eqv.mp ‹n——m ≃ 0›
  have : n > m := pos_diff_gt.mp ‹Positive (n——m)›
  AA.TwoOfThree.twoAndThree ‹n ≃ m› ‹n > m›
| AA.TwoOfThree.oneAndThree (_ : n——m ≃ 0) (_ : Negative (n——m)) =>
  have : n < m := neg_diff_lt.mp ‹Negative (n——m)›
  have : n ≃ m := zero_diff_eqv.mp ‹n——m ≃ 0›
  AA.TwoOfThree.oneAndTwo ‹n < m› ‹n ≃ m›
| AA.TwoOfThree.twoAndThree (_ : Positive (n——m)) (_ : Negative (n——m)) =>
  have : n < m := neg_diff_lt.mp ‹Negative (n——m)›
  have : n > m := pos_diff_gt.mp ‹Positive (n——m)›
  AA.TwoOfThree.oneAndThree ‹n < m› ‹n > m›
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
natOrderTri : AA.ExactlyOneOfThree (n < m) (n ≃ m) (n > m)
h : AA.TwoOfThree (n——m ≃ 0) (Positive (n——m)) (Negative (n——m))
twoOfThree : AA.TwoOfThree (n < m) (n ≃ m) (n > m)
⊢ False
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sign_trichotomy
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
natOrderTri : AA.ExactlyOneOfThree (n < m) (n ≃ m) (n > m)
h : AA.TwoOfThree (n——m ≃ 0) (Positive (n——m)) (Negative (n——m))
twoOfThree : AA.TwoOfThree (n < m) (n ≃ m) (n > m)
⊢ False
Tactic:
have notTwoOfThree : ¬ AA.TwoOfThree (n < m) (n ≃ m) (n > m) :=
  natOrderTri.atMostOne
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
natOrderTri : AA.ExactlyOneOfThree (n < m) (n ≃ m) (n > m)
h : AA.TwoOfThree (n——m ≃ 0) (Positive (n——m)) (Negative (n——m))
twoOfThree : AA.TwoOfThree (n < m) (n ≃ m) (n > m)
notTwoOfThree : ¬AA.TwoOfThree (n < m) (n ≃ m) (n > m)
⊢ False
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sign_trichotomy
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
natOrderTri : AA.ExactlyOneOfThree (n < m) (n ≃ m) (n > m)
h : AA.TwoOfThree (n——m ≃ 0) (Positive (n——m)) (Negative (n——m))
twoOfThree : AA.TwoOfThree (n < m) (n ≃ m) (n > m)
notTwoOfThree : ¬AA.TwoOfThree (n < m) (n ≃ m) (n > m)
⊢ False
Tactic:
exact absurd twoOfThree notTwoOfThree
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_zero
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a : Difference ℕ
⊢ a ≃ 0 ↔ a.sgn ≃ 0
Tactic:
revert a
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
⊢ ∀ {a : Difference ℕ}, a ≃ 0 ↔ a.sgn ≃ 0
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_zero
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
⊢ ∀ {a : Difference ℕ}, a ≃ 0 ↔ a.sgn ≃ 0
Tactic:
intro (n——m)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ n——m ≃ 0 ↔ (n——m).sgn ≃ 0
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_zero
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ n——m ≃ 0 ↔ (n——m).sgn ≃ 0
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ n——m ≃ 0 → (n——m).sgn ≃ 0

case mpr
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (n——m).sgn ≃ 0 → n——m ≃ 0
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_zero
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ n——m ≃ 0 → (n——m).sgn ≃ 0
Tactic:
case mp =>
  intro (_ : n——m ≃ 0)
  show sgn (n——m) ≃ 0
  have : n ≃ m := zero_diff_eqv.mp ‹n——m ≃ 0›
  have : compare n m = Ordering.eq := Natural.compare_eq.mpr this
  have : ord_sgn (compare n m) ≃ ord_sgn Ordering.eq :=
    ord_sgn_subst (ℤ := Difference ℕ) this
  have : ord_sgn (compare n m) ≃ (0:Difference ℕ) := this
  have : sgn (n——m) ≃ 0 := this
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_zero
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (n——m).sgn ≃ 0 → n——m ≃ 0
Tactic:
case mpr =>
  intro (_ : sgn (n——m) ≃ 0)
  show n——m ≃ 0
  have : ord_sgn (compare n m) ≃ (0:Difference ℕ) := ‹sgn (n——m) ≃ 0›
  have : ord_sgn (compare n m) ≃ ord_sgn Ordering.eq := this
  have : compare n m = Ordering.eq := ord_sgn_inject this
  have : n ≃ m := Natural.compare_eq.mp this
  have : n——m ≃ 0 := zero_diff_eqv.mpr this
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_zero
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ n——m ≃ 0 → (n——m).sgn ≃ 0
Tactic:
intro (_ : n——m ≃ 0)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : n——m ≃ 0
⊢ (n——m).sgn ≃ 0
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_zero
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : n——m ≃ 0
⊢ (n——m).sgn ≃ 0
Tactic:
have : n ≃ m := zero_diff_eqv.mp ‹n——m ≃ 0›
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : n——m ≃ 0
this : n ≃ m
⊢ (n——m).sgn ≃ 0
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_zero
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : n——m ≃ 0
this : n ≃ m
⊢ (n——m).sgn ≃ 0
Tactic:
have : compare n m = Ordering.eq := Natural.compare_eq.mpr this
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : n——m ≃ 0
this✝ : n ≃ m
this : compare n m = Ordering.eq
⊢ (n——m).sgn ≃ 0
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_zero
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : n——m ≃ 0
this✝ : n ≃ m
this : compare n m = Ordering.eq
⊢ (n——m).sgn ≃ 0
Tactic:
have : ord_sgn (compare n m) ≃ ord_sgn Ordering.eq :=
  ord_sgn_subst (ℤ := Difference ℕ) this
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : n——m ≃ 0
this✝¹ : n ≃ m
this✝ : compare n m = Ordering.eq
this : ord_sgn (compare n m) ≃ ord_sgn Ordering.eq
⊢ (n——m).sgn ≃ 0
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_zero
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : n——m ≃ 0
this✝¹ : n ≃ m
this✝ : compare n m = Ordering.eq
this : ord_sgn (compare n m) ≃ ord_sgn Ordering.eq
⊢ (n——m).sgn ≃ 0
Tactic:
have : ord_sgn (compare n m) ≃ (0:Difference ℕ) := this
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : n——m ≃ 0
this✝² : n ≃ m
this✝¹ : compare n m = Ordering.eq
this✝ : ord_sgn (compare n m) ≃ ord_sgn Ordering.eq
this : ord_sgn (compare n m) ≃ 0
⊢ (n——m).sgn ≃ 0
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_zero
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : n——m ≃ 0
this✝² : n ≃ m
this✝¹ : compare n m = Ordering.eq
this✝ : ord_sgn (compare n m) ≃ ord_sgn Ordering.eq
this : ord_sgn (compare n m) ≃ 0
⊢ (n——m).sgn ≃ 0
Tactic:
have : sgn (n——m) ≃ 0 := this
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : n——m ≃ 0
this✝³ : n ≃ m
this✝² : compare n m = Ordering.eq
this✝¹ : ord_sgn (compare n m) ≃ ord_sgn Ordering.eq
this✝ : ord_sgn (compare n m) ≃ 0
this : (n——m).sgn ≃ 0
⊢ (n——m).sgn ≃ 0
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_zero
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : n——m ≃ 0
this✝³ : n ≃ m
this✝² : compare n m = Ordering.eq
this✝¹ : ord_sgn (compare n m) ≃ ord_sgn Ordering.eq
this✝ : ord_sgn (compare n m) ≃ 0
this : (n——m).sgn ≃ 0
⊢ (n——m).sgn ≃ 0
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_zero
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (n——m).sgn ≃ 0 → n——m ≃ 0
Tactic:
intro (_ : sgn (n——m) ≃ 0)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : (n——m).sgn ≃ 0
⊢ n——m ≃ 0
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_zero
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : (n——m).sgn ≃ 0
⊢ n——m ≃ 0
Tactic:
have : ord_sgn (compare n m) ≃ (0:Difference ℕ) := ‹sgn (n——m) ≃ 0›
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : (n——m).sgn ≃ 0
this : ord_sgn (compare n m) ≃ 0
⊢ n——m ≃ 0
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_zero
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : (n——m).sgn ≃ 0
this : ord_sgn (compare n m) ≃ 0
⊢ n——m ≃ 0
Tactic:
have : ord_sgn (compare n m) ≃ ord_sgn Ordering.eq := this
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : (n——m).sgn ≃ 0
this✝ : ord_sgn (compare n m) ≃ 0
this : ord_sgn (compare n m) ≃ ord_sgn Ordering.eq
⊢ n——m ≃ 0
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_zero
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : (n——m).sgn ≃ 0
this✝ : ord_sgn (compare n m) ≃ 0
this : ord_sgn (compare n m) ≃ ord_sgn Ordering.eq
⊢ n——m ≃ 0
Tactic:
have : compare n m = Ordering.eq := ord_sgn_inject this
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : (n——m).sgn ≃ 0
this✝¹ : ord_sgn (compare n m) ≃ 0
this✝ : ord_sgn (compare n m) ≃ ord_sgn Ordering.eq
this : compare n m = Ordering.eq
⊢ n——m ≃ 0
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_zero
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : (n——m).sgn ≃ 0
this✝¹ : ord_sgn (compare n m) ≃ 0
this✝ : ord_sgn (compare n m) ≃ ord_sgn Ordering.eq
this : compare n m = Ordering.eq
⊢ n——m ≃ 0
Tactic:
have : n ≃ m := Natural.compare_eq.mp this
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : (n——m).sgn ≃ 0
this✝² : ord_sgn (compare n m) ≃ 0
this✝¹ : ord_sgn (compare n m) ≃ ord_sgn Ordering.eq
this✝ : compare n m = Ordering.eq
this : n ≃ m
⊢ n——m ≃ 0
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_zero
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : (n——m).sgn ≃ 0
this✝² : ord_sgn (compare n m) ≃ 0
this✝¹ : ord_sgn (compare n m) ≃ ord_sgn Ordering.eq
this✝ : compare n m = Ordering.eq
this : n ≃ m
⊢ n——m ≃ 0
Tactic:
have : n——m ≃ 0 := zero_diff_eqv.mpr this
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : (n——m).sgn ≃ 0
this✝³ : ord_sgn (compare n m) ≃ 0
this✝² : ord_sgn (compare n m) ≃ ord_sgn Ordering.eq
this✝¹ : compare n m = Ordering.eq
this✝ : n ≃ m
this : n——m ≃ 0
⊢ n——m ≃ 0
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_zero
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : (n——m).sgn ≃ 0
this✝³ : ord_sgn (compare n m) ≃ 0
this✝² : ord_sgn (compare n m) ≃ ord_sgn Ordering.eq
this✝¹ : compare n m = Ordering.eq
this✝ : n ≃ m
this : n——m ≃ 0
⊢ n——m ≃ 0
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_positive
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a : Difference ℕ
⊢ Positive a ↔ a.sgn ≃ 1
Tactic:
revert a
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
⊢ ∀ {a : Difference ℕ}, Positive a ↔ a.sgn ≃ 1
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_positive
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
⊢ ∀ {a : Difference ℕ}, Positive a ↔ a.sgn ≃ 1
Tactic:
intro (n——m)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ Positive (n——m) ↔ (n——m).sgn ≃ 1
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_positive
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ Positive (n——m) ↔ (n——m).sgn ≃ 1
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ Positive (n——m) → (n——m).sgn ≃ 1

case mpr
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (n——m).sgn ≃ 1 → Positive (n——m)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_positive
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ Positive (n——m) → (n——m).sgn ≃ 1
Tactic:
case mp =>
  intro (_ : Positive (n——m))
  show sgn (n——m) ≃ 1
  have : n > m := pos_diff_gt.mp ‹Positive (n——m)›
  have : compare n m = Ordering.gt := Natural.compare_gt.mpr this
  have : ord_sgn (compare n m) ≃ ord_sgn Ordering.gt :=
    ord_sgn_subst (ℤ := Difference ℕ) this
  have : ord_sgn (compare n m) ≃ (1:Difference ℕ) := this
  have : sgn (n——m) ≃ 1 := this
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_positive
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (n——m).sgn ≃ 1 → Positive (n——m)
Tactic:
case mpr =>
  intro (_ : sgn (n——m) ≃ 1)
  show Positive (n——m)
  have : ord_sgn (compare n m) ≃ (1:Difference ℕ) := ‹sgn (n——m) ≃ 1›
  have : ord_sgn (compare n m) ≃ ord_sgn Ordering.gt := this
  have : compare n m = Ordering.gt := ord_sgn_inject this
  have : n > m := Natural.compare_gt.mp this
  have : Positive (n——m) := pos_diff_gt.mpr this
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_positive
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ Positive (n——m) → (n——m).sgn ≃ 1
Tactic:
intro (_ : Positive (n——m))
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Positive (n——m)
⊢ (n——m).sgn ≃ 1
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_positive
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Positive (n——m)
⊢ (n——m).sgn ≃ 1
Tactic:
have : n > m := pos_diff_gt.mp ‹Positive (n——m)›
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Positive (n——m)
this : n > m
⊢ (n——m).sgn ≃ 1
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_positive
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Positive (n——m)
this : n > m
⊢ (n——m).sgn ≃ 1
Tactic:
have : compare n m = Ordering.gt := Natural.compare_gt.mpr this
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Positive (n——m)
this✝ : n > m
this : compare n m = Ordering.gt
⊢ (n——m).sgn ≃ 1
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_positive
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Positive (n——m)
this✝ : n > m
this : compare n m = Ordering.gt
⊢ (n——m).sgn ≃ 1
Tactic:
have : ord_sgn (compare n m) ≃ ord_sgn Ordering.gt :=
  ord_sgn_subst (ℤ := Difference ℕ) this
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Positive (n——m)
this✝¹ : n > m
this✝ : compare n m = Ordering.gt
this : ord_sgn (compare n m) ≃ ord_sgn Ordering.gt
⊢ (n——m).sgn ≃ 1
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_positive
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Positive (n——m)
this✝¹ : n > m
this✝ : compare n m = Ordering.gt
this : ord_sgn (compare n m) ≃ ord_sgn Ordering.gt
⊢ (n——m).sgn ≃ 1
Tactic:
have : ord_sgn (compare n m) ≃ (1:Difference ℕ) := this
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Positive (n——m)
this✝² : n > m
this✝¹ : compare n m = Ordering.gt
this✝ : ord_sgn (compare n m) ≃ ord_sgn Ordering.gt
this : ord_sgn (compare n m) ≃ 1
⊢ (n——m).sgn ≃ 1
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_positive
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Positive (n——m)
this✝² : n > m
this✝¹ : compare n m = Ordering.gt
this✝ : ord_sgn (compare n m) ≃ ord_sgn Ordering.gt
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✝ : Positive (n——m)
this✝³ : n > m
this✝² : compare n m = Ordering.gt
this✝¹ : ord_sgn (compare n m) ≃ ord_sgn Ordering.gt
this✝ : ord_sgn (compare n m) ≃ 1
this : (n——m).sgn ≃ 1
⊢ (n——m).sgn ≃ 1
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_positive
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Positive (n——m)
this✝³ : n > m
this✝² : compare n m = Ordering.gt
this✝¹ : ord_sgn (compare n m) ≃ ord_sgn Ordering.gt
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_positive
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (n——m).sgn ≃ 1 → Positive (n——m)
Tactic:
intro (_ : sgn (n——m) ≃ 1)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : (n——m).sgn ≃ 1
⊢ Positive (n——m)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_positive
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : (n——m).sgn ≃ 1
⊢ Positive (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
⊢ Positive (n——m)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_positive
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : (n——m).sgn ≃ 1
this : ord_sgn (compare n m) ≃ 1
⊢ Positive (n——m)
Tactic:
have : ord_sgn (compare n m) ≃ ord_sgn Ordering.gt := 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.gt
⊢ Positive (n——m)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_positive
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.gt
⊢ Positive (n——m)
Tactic:
have : compare n m = Ordering.gt := 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.gt
this : compare n m = Ordering.gt
⊢ Positive (n——m)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_positive
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.gt
this : compare n m = Ordering.gt
⊢ Positive (n——m)
Tactic:
have : n > m := Natural.compare_gt.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.gt
this✝ : compare n m = Ordering.gt
this : n > m
⊢ Positive (n——m)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_positive
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.gt
this✝ : compare n m = Ordering.gt
this : n > m
⊢ Positive (n——m)
Tactic:
have : Positive (n——m) := pos_diff_gt.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.gt
this✝¹ : compare n m = Ordering.gt
this✝ : n > m
this : Positive (n——m)
⊢ Positive (n——m)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_positive
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.gt
this✝¹ : compare n m = Ordering.gt
this✝ : n > m
this : Positive (n——m)
⊢ Positive (n——m)
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_negative
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a : Difference ℕ
⊢ Negative a ↔ a.sgn ≃ -1
Tactic:
revert a
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
⊢ ∀ {a : Difference ℕ}, Negative a ↔ a.sgn ≃ -1
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_negative
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
⊢ ∀ {a : Difference ℕ}, Negative a ↔ a.sgn ≃ -1
Tactic:
intro (n——m)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ Negative (n——m) ↔ (n——m).sgn ≃ -1
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_negative
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ Negative (n——m) ↔ (n——m).sgn ≃ -1
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ Negative (n——m) → (n——m).sgn ≃ -1

case mpr
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (n——m).sgn ≃ -1 → Negative (n——m)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_negative
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ Negative (n——m) → (n——m).sgn ≃ -1
Tactic:
case mp =>
  intro (_ : Negative (n——m))
  show sgn (n——m) ≃ -1
  have : n < m := neg_diff_lt.mp ‹Negative (n——m)›
  have : compare n m = Ordering.lt := Natural.compare_lt.mpr this
  have : ord_sgn (compare n m) ≃ ord_sgn Ordering.lt :=
    ord_sgn_subst (ℤ := Difference ℕ) this
  have : ord_sgn (compare n m) ≃ (-1:Difference ℕ) := this
  have : sgn (n——m) ≃ -1 := this
  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:
case mpr =>
  intro (_ : sgn (n——m) ≃ -1)
  show Negative (n——m)
  have : ord_sgn (compare n m) ≃ (-1:Difference ℕ) := ‹sgn (n——m) ≃ -1›
  have : ord_sgn (compare n m) ≃ ord_sgn Ordering.lt := this
  have : compare n m = Ordering.lt := ord_sgn_inject this
  have : n < m := Natural.compare_lt.mp this
  have : Negative (n——m) := neg_diff_lt.mpr this
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_negative
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ Negative (n——m) → (n——m).sgn ≃ -1
Tactic:
intro (_ : Negative (n——m))
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Negative (n——m)
⊢ (n——m).sgn ≃ -1
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_negative
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Negative (n——m)
⊢ (n——m).sgn ≃ -1
Tactic:
have : n < m := neg_diff_lt.mp ‹Negative (n——m)›
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Negative (n——m)
this : n < m
⊢ (n——m).sgn ≃ -1