Theorem: Lean4Axiomatic.Integer.Impl.Difference.sgn_negative (Lean4Axiomatic/Integer/Impl/Difference/Sign.lean)

State before:
ℕ : Type
inst✝ : Natural ℕ
a : Difference ℕ
⊢ Negative a ↔ a.sgn ≃ -1
Tactic:
revert a
State after:
ℕ : Type
inst✝ : Natural ℕ
⊢ ∀ {a : Difference ℕ}, Negative a ↔ a.sgn ≃ -1

State before:
ℕ : Type
inst✝ : Natural ℕ
⊢ ∀ {a : Difference ℕ}, Negative a ↔ a.sgn ≃ -1
Tactic:
intro (n——m)
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ Negative (n——m) ↔ (n——m).sgn ≃ -1

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ Negative (n——m) ↔ (n——m).sgn ≃ -1
Tactic:
apply Iff.intro
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)

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
State after:
no goals

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
State after:
no goals

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ Negative (n——m) → (n——m).sgn ≃ -1
Tactic:
intro (_ : Negative (n——m))
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Negative (n——m)
⊢ (n——m).sgn ≃ -1

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)›
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Negative (n——m)
this : n < m
⊢ (n——m).sgn ≃ -1

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
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Negative (n——m)
this✝ : n < m
this : compare n m = Ordering.lt
⊢ (n——m).sgn ≃ -1

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
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

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
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

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
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

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
State after:
no goals

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (n——m).sgn ≃ -1 → Negative (n——m)
Tactic:
intro (_ : sgn (n——m) ≃ -1)
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : (n——m).sgn ≃ -1
⊢ Negative (n——m)

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›
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : (n——m).sgn ≃ -1
this : ord_sgn (compare n m) ≃ -1
⊢ Negative (n——m)

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
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)

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
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)

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
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)

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
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)

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
State after:
no goals