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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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