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

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ Negative (n——m) ↔ n < m
Tactic:
have neg_diff {k : ℕ} : 0——k ≃ -1 * coe k := by
  apply Rel.symm
  calc
    (-1) * coe k ≃ _ := Rel.refl
    (-1) * k——0  ≃ _ := mul_neg_one
    (-(k——0))    ≃ _ := Rel.refl
    0——k         ≃ _ := Rel.refl
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
⊢ Negative (n——m) ↔ n < m

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
⊢ Negative (n——m) ↔ n < m
Tactic:
apply Iff.intro
State after:
case mp
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
⊢ Negative (n——m) → n < m

case mpr
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
⊢ n < m → Negative (n——m)

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
⊢ Negative (n——m) → n < m
Tactic:
case mp =>
  intro (_ : Negative (n——m))
  show n < m
  apply Natural.lt_defn_add.mpr
  show ∃ (k : ℕ), Positive k ∧ m ≃ n + k
  have
    (NonzeroWithSign.intro (k : ℕ) (_ : Positive k) (_ : n——m ≃ -1 * coe k))
      := Generic.negative_iff_sign_neg1.mp ‹Negative (n——m)›
  have : n——m ≃ 0——k := Rel.trans ‹n——m ≃ -1 * coe k› (Rel.symm neg_diff)
  have : n + k ≃ 0 + m := ‹n——m ≃ 0——k›
  have : m ≃ n + k := calc
    m     ≃ _ := Rel.symm AA.identL
    0 + m ≃ _ := Rel.symm ‹n + k ≃ 0 + m›
    n + k ≃ _ := Rel.refl
  exact Exists.intro k (And.intro ‹Positive k› ‹m ≃ n + k›)
State after:
no goals

State before:
ℕ : Type
inst✝ : Natural ℕ
n m k : ℕ
⊢ 0——k ≃ -1 * coe k
Tactic:
apply Rel.symm
State after:
case a
ℕ : Type
inst✝ : Natural ℕ
n m k : ℕ
⊢ -1 * coe k ≃ 0——k

State before:
case a
ℕ : Type
inst✝ : Natural ℕ
n m k : ℕ
⊢ -1 * coe k ≃ 0——k
Tactic:
calc
  (-1) * coe k ≃ _ := Rel.refl
  (-1) * k——0  ≃ _ := mul_neg_one
  (-(k——0))    ≃ _ := Rel.refl
  0——k         ≃ _ := Rel.refl
State after:
no goals

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
⊢ Negative (n——m) → n < m
Tactic:
intro (_ : Negative (n——m))
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : Negative (n——m)
⊢ n < m

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : Negative (n——m)
⊢ n < m
Tactic:
apply Natural.lt_defn_add.mpr
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : Negative (n——m)
⊢ ∃ k, Positive k ∧ m ≃ n + k

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : Negative (n——m)
⊢ ∃ k, Positive k ∧ m ≃ n + k
Tactic:
have
  (NonzeroWithSign.intro (k : ℕ) (_ : Positive k) (_ : n——m ≃ -1 * coe k))
    := Generic.negative_iff_sign_neg1.mp ‹Negative (n——m)›
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : Negative (n——m)
k : ℕ
pos✝ : Positive k
eqv✝ : n——m ≃ -1 * coe k
⊢ ∃ k, Positive k ∧ m ≃ n + k

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : Negative (n——m)
k : ℕ
pos✝ : Positive k
eqv✝ : n——m ≃ -1 * coe k
⊢ ∃ k, Positive k ∧ m ≃ n + k
Tactic:
have : n——m ≃ 0——k := Rel.trans ‹n——m ≃ -1 * coe k› (Rel.symm neg_diff)
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : Negative (n——m)
k : ℕ
pos✝ : Positive k
eqv✝ : n——m ≃ -1 * coe k
this : n——m ≃ 0——k
⊢ ∃ k, Positive k ∧ m ≃ n + k

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : Negative (n——m)
k : ℕ
pos✝ : Positive k
eqv✝ : n——m ≃ -1 * coe k
this : n——m ≃ 0——k
⊢ ∃ k, Positive k ∧ m ≃ n + k
Tactic:
have : n + k ≃ 0 + m := ‹n——m ≃ 0——k›
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : Negative (n——m)
k : ℕ
pos✝ : Positive k
eqv✝ : n——m ≃ -1 * coe k
this✝ : n——m ≃ 0——k
this : n + k ≃ 0 + m
⊢ ∃ k, Positive k ∧ m ≃ n + k

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : Negative (n——m)
k : ℕ
pos✝ : Positive k
eqv✝ : n——m ≃ -1 * coe k
this✝ : n——m ≃ 0——k
this : n + k ≃ 0 + m
⊢ ∃ k, Positive k ∧ m ≃ n + k
Tactic:
have : m ≃ n + k := calc
  m     ≃ _ := Rel.symm AA.identL
  0 + m ≃ _ := Rel.symm ‹n + k ≃ 0 + m›
  n + k ≃ _ := Rel.refl
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : Negative (n——m)
k : ℕ
pos✝ : Positive k
eqv✝ : n——m ≃ -1 * coe k
this✝¹ : n——m ≃ 0——k
this✝ : n + k ≃ 0 + m
this : m ≃ n + k
⊢ ∃ k, Positive k ∧ m ≃ n + k

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : Negative (n——m)
k : ℕ
pos✝ : Positive k
eqv✝ : n——m ≃ -1 * coe k
this✝¹ : n——m ≃ 0——k
this✝ : n + k ≃ 0 + m
this : m ≃ n + k
⊢ ∃ k, Positive k ∧ m ≃ n + k
Tactic:
exact Exists.intro k (And.intro ‹Positive k› ‹m ≃ n + k›)
State after:
no goals

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
⊢ n < m → Negative (n——m)
Tactic:
intro (_ : n < m)
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : n < m
⊢ Negative (n——m)

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : n < m
⊢ Negative (n——m)
Tactic:
apply Generic.negative_iff_sign_neg1.mpr
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : n < m
⊢ NonzeroWithSign (n——m) (-1)

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : n < m
⊢ NonzeroWithSign (n——m) (-1)
Tactic:
have (Exists.intro k (And.intro (_ : Positive k) (_ : m ≃ n + k))) :=
  Natural.lt_defn_add.mp ‹n < m›
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : n < m
k : ℕ
left✝ : Positive k
right✝ : m ≃ n + k
⊢ NonzeroWithSign (n——m) (-1)

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : n < m
k : ℕ
left✝ : Positive k
right✝ : m ≃ n + k
⊢ NonzeroWithSign (n——m) (-1)
Tactic:
apply NonzeroWithSign.intro k ‹Positive k›
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : n < m
k : ℕ
left✝ : Positive k
right✝ : m ≃ n + k
⊢ n——m ≃ -1 * coe k

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : n < m
k : ℕ
left✝ : Positive k
right✝ : m ≃ n + k
⊢ n——m ≃ -1 * coe k
Tactic:
have : 0——k ≃ -1 * coe k := neg_diff
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : n < m
k : ℕ
left✝ : Positive k
right✝ : m ≃ n + k
this : 0——k ≃ -1 * coe k
⊢ n——m ≃ -1 * coe k

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : n < m
k : ℕ
left✝ : Positive k
right✝ : m ≃ n + k
this : 0——k ≃ -1 * coe k
⊢ n——m ≃ 0——k
Tactic:
show n + k ≃ 0 + m
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : n < m
k : ℕ
left✝ : Positive k
right✝ : m ≃ n + k
this : 0——k ≃ -1 * coe k
⊢ n + k ≃ 0 + m

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : n < m
k : ℕ
left✝ : Positive k
right✝ : m ≃ n + k
this : 0——k ≃ -1 * coe k
⊢ n + k ≃ 0 + m
Tactic:
calc
  n + k ≃ _ := Rel.symm ‹m ≃ n + k›
  m     ≃ _ := Rel.symm AA.identL
  0 + m ≃ _ := Rel.refl
State after:
no goals