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

State before:
ℕ : Type
inst✝ : Natural ℕ
s a b : Difference ℕ
⊢ a.sgn ≃ s → b.sgn ≃ s → (a + b).sgn ≃ s
Tactic:
revert a
State after:
ℕ : Type
inst✝ : Natural ℕ
s b : Difference ℕ
⊢ ∀ {a : Difference ℕ}, a.sgn ≃ s → b.sgn ≃ s → (a + b).sgn ≃ s

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

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
State after:
ℕ : Type
inst✝ : Natural ℕ
s : Difference ℕ
n m : ℕ
⊢ ∀ {b : Difference ℕ}, (n——m).sgn ≃ s → b.sgn ≃ s → (n——m + b).sgn ≃ s

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

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

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

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

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

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

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

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

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