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

State before:
ℕ : Type
inst✝ : Natural ℕ
a : Difference ℕ
⊢ AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
Tactic:
revert a
State after:
ℕ : Type
inst✝ : Natural ℕ
⊢ ∀ (a : Difference ℕ), AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)

State before:
ℕ : Type
inst✝ : Natural ℕ
⊢ ∀ (a : Difference ℕ), AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
Tactic:
intro (n——m)
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ AA.ExactlyOneOfThree (n——m ≃ 0) (Positive (n——m)) (Negative (n——m))

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ AA.ExactlyOneOfThree (n——m ≃ 0) (Positive (n——m)) (Negative (n——m))
Tactic:
have natOrderTri : AA.ExactlyOneOfThree (n < m) (n ≃ m) (n > m) :=
  Natural.trichotomy n m
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
natOrderTri : AA.ExactlyOneOfThree (n < m) (n ≃ m) (n > m)
⊢ AA.ExactlyOneOfThree (n——m ≃ 0) (Positive (n——m)) (Negative (n——m))

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
natOrderTri : AA.ExactlyOneOfThree (n < m) (n ≃ m) (n > m)
⊢ AA.ExactlyOneOfThree (n——m ≃ 0) (Positive (n——m)) (Negative (n——m))
Tactic:
apply AA.ExactlyOneOfThree.mk
State after:
case atLeastOne
ℕ : 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))

case atMostOne
ℕ : 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))

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:
case atLeastOne =>
  show AA.OneOfThree (n——m ≃ 0) (Positive (n——m)) (Negative (n——m))
  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)›
State after:
no goals

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:
case atMostOne =>
  intro (h : AA.TwoOfThree (n——m ≃ 0) (Positive (n——m)) (Negative (n——m)))
  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›
  show False
  have notTwoOfThree : ¬ AA.TwoOfThree (n < m) (n ≃ m) (n > m) :=
    natOrderTri.atMostOne
  exact absurd twoOfThree notTwoOfThree
State after:
no goals

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

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

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

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

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

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

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

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

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

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

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