internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Integer.lt_neg_flip
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
this✝ : -a - -b ≃ b - a
x✝ : -b < -a
this : Positive (-a - -b)
⊢ Positive (b - a)
Tactic:
exact AA.substFn ‹-a - -b ≃ b - a› ‹Positive (-a - -b)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.lt_trans
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
⊢ a < b → b < c → a < c
Tactic:
intro (_ : a < b) (_ : b < c)
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : a < b
x✝ : b < c
⊢ a < c
Theorem: Lean4Axiomatic.Integer.lt_trans
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : a < b
x✝ : b < c
⊢ a < c
Tactic:
have : Positive (b - a) := gt_iff_pos_diff.mp ‹a < b›
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : a < b
x✝ : b < c
this : Positive (b - a)
⊢ a < c
Theorem: Lean4Axiomatic.Integer.lt_trans
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : a < b
x✝ : b < c
this : Positive (b - a)
⊢ a < c
Tactic:
have : Positive (c - b) := gt_iff_pos_diff.mp ‹b < c›
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : a < b
x✝ : b < c
this✝ : Positive (b - a)
this : Positive (c - b)
⊢ a < c
Theorem: Lean4Axiomatic.Integer.lt_trans
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : a < b
x✝ : b < c
this✝ : Positive (b - a)
this : Positive (c - b)
⊢ a < c
Tactic:
apply gt_iff_pos_diff.mpr
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : a < b
x✝ : b < c
this✝ : Positive (b - a)
this : Positive (c - b)
⊢ Positive (c - a)
Theorem: Lean4Axiomatic.Integer.lt_trans
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : a < b
x✝ : b < c
this✝ : Positive (b - a)
this : Positive (c - b)
⊢ Positive (c - a)
Tactic:
have : Positive ((c - b) + (b - a)) :=
  add_preserves_positive ‹Positive (c - b)› ‹Positive (b - a)›
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : a < b
x✝ : b < c
this✝¹ : Positive (b - a)
this✝ : Positive (c - b)
this : Positive (c - b + (b - a))
⊢ Positive (c - a)
Theorem: Lean4Axiomatic.Integer.lt_trans
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : a < b
x✝ : b < c
this✝¹ : Positive (b - a)
this✝ : Positive (c - b)
this : Positive (c - b + (b - a))
⊢ Positive (c - a)
Tactic:
have : (c - b) + (b - a) ≃ c - a := calc
  (c - b) + (b - a)   ≃ _ := AA.substL sub_defn
  (c + -b) + (b - a)  ≃ _ := AA.substR sub_defn
  (c + -b) + (b + -a) ≃ _ := AA.assoc
  c + (-b + (b + -a)) ≃ _ := AA.substR (Rel.symm AA.assoc)
  c + ((-b + b) + -a) ≃ _ := AA.substR (AA.substL AA.inverseL)
  c + (0 + -a)        ≃ _ := AA.substR AA.identL
  c + -a              ≃ _ := Rel.symm sub_defn
  c - a               ≃ _ := Rel.refl
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : a < b
x✝ : b < c
this✝² : Positive (b - a)
this✝¹ : Positive (c - b)
this✝ : Positive (c - b + (b - a))
this : c - b + (b - a) ≃ c - a
⊢ Positive (c - a)
Theorem: Lean4Axiomatic.Integer.lt_trans
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : a < b
x✝ : b < c
this✝² : Positive (b - a)
this✝¹ : Positive (c - b)
this✝ : Positive (c - b + (b - a))
this : c - b + (b - a) ≃ c - a
⊢ Positive (c - a)
Tactic:
have : Positive (c - a) :=
  AA.substFn ‹(c - b) + (b - a) ≃ c - a› ‹Positive ((c - b) + (b - a))›
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : a < b
x✝ : b < c
this✝³ : Positive (b - a)
this✝² : Positive (c - b)
this✝¹ : Positive (c - b + (b - a))
this✝ : c - b + (b - a) ≃ c - a
this : Positive (c - a)
⊢ Positive (c - a)
Theorem: Lean4Axiomatic.Integer.lt_trans
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : a < b
x✝ : b < c
this✝³ : Positive (b - a)
this✝² : Positive (c - b)
this✝¹ : Positive (c - b + (b - a))
this✝ : c - b + (b - a) ≃ c - a
this : Positive (c - a)
⊢ Positive (c - a)
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.order_trichotomy
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
⊢ AA.ExactlyOneOfThree (a < b) (a ≃ b) (a > b)
Tactic:
have abTri
  : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
  := Signed.trichotomy (a - b)
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
⊢ AA.ExactlyOneOfThree (a < b) (a ≃ b) (a > b)
Theorem: Lean4Axiomatic.Integer.order_trichotomy
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
⊢ AA.ExactlyOneOfThree (a < b) (a ≃ b) (a > b)
Tactic:
apply AA.ExactlyOneOfThree.mk
Proof state after:
case atLeastOne
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
⊢ AA.OneOfThree (a < b) (a ≃ b) (a > b)

case atMostOne
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
⊢ ¬AA.TwoOfThree (a < b) (a ≃ b) (a > b)
Theorem: Lean4Axiomatic.Integer.order_trichotomy
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
⊢ AA.OneOfThree (a < b) (a ≃ b) (a > b)
Tactic:
case atLeastOne =>
  show AA.OneOfThree (a < b) (a ≃ b) (a > b)
  match abTri.atLeastOne with
  | AA.OneOfThree.first (_ : a - b ≃ 0) =>
    have : a ≃ b := zero_diff_iff_eqv.mp ‹a - b ≃ 0›
    exact AA.OneOfThree.second ‹a ≃ b›
  | AA.OneOfThree.second (_ : Positive (a - b)) =>
    have : a > b := gt_iff_pos_diff.mpr ‹Positive (a - b)›
    exact AA.OneOfThree.third ‹a > b›
  | AA.OneOfThree.third (_ : Negative (a - b)) =>
    have : a < b := lt_iff_neg_diff.mpr ‹Negative (a - b)›
    exact AA.OneOfThree.first ‹a < b›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.order_trichotomy
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
⊢ ¬AA.TwoOfThree (a < b) (a ≃ b) (a > b)
Tactic:
case atMostOne =>
  intro (_ : AA.TwoOfThree (a < b) (a ≃ b) (a > b))
  show False
  let ab := a - b
  have abTwo : AA.TwoOfThree (ab ≃ 0) (Positive ab) (Negative ab) :=
    match ‹AA.TwoOfThree (a < b) (a ≃ b) (a > b)› with
    | AA.TwoOfThree.oneAndTwo (_ : a < b) (_ : a ≃ b) =>
      have : Negative ab := lt_iff_neg_diff.mp ‹a < b›
      have : ab ≃ 0 := zero_diff_iff_eqv.mpr ‹a ≃ b›
      AA.TwoOfThree.oneAndThree ‹ab ≃ 0› ‹Negative ab›
    | AA.TwoOfThree.oneAndThree (_ : a < b) (_ : a > b) =>
      have : Negative ab := lt_iff_neg_diff.mp ‹a < b›
      have : Positive ab := gt_iff_pos_diff.mp ‹a > b›
      AA.TwoOfThree.twoAndThree ‹Positive ab› ‹Negative ab›
    | AA.TwoOfThree.twoAndThree (_ : a ≃ b) (_ : a > b) =>
      have : ab ≃ 0 := zero_diff_iff_eqv.mpr ‹a ≃ b›
      have : Positive ab := gt_iff_pos_diff.mp ‹a > b›
      AA.TwoOfThree.oneAndTwo ‹ab ≃ 0› ‹Positive ab›
  have abNotTwo
    : ¬ AA.TwoOfThree (ab ≃ 0) (Positive ab) (Negative ab)
    := abTri.atMostOne
  exact absurd abTwo abNotTwo
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.order_trichotomy
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
⊢ AA.OneOfThree (a < b) (a ≃ b) (a > b)
Tactic:
match abTri.atLeastOne with
| AA.OneOfThree.first (_ : a - b ≃ 0) =>
  have : a ≃ b := zero_diff_iff_eqv.mp ‹a - b ≃ 0›
  exact AA.OneOfThree.second ‹a ≃ b›
| AA.OneOfThree.second (_ : Positive (a - b)) =>
  have : a > b := gt_iff_pos_diff.mpr ‹Positive (a - b)›
  exact AA.OneOfThree.third ‹a > b›
| AA.OneOfThree.third (_ : Negative (a - b)) =>
  have : a < b := lt_iff_neg_diff.mpr ‹Negative (a - b)›
  exact AA.OneOfThree.first ‹a < b›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.order_trichotomy
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
a✝ : a - b ≃ 0
⊢ AA.OneOfThree (a < b) (a ≃ b) (a > b)
Tactic:
have : a ≃ b := zero_diff_iff_eqv.mp ‹a - b ≃ 0›
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
a✝ : a - b ≃ 0
this : a ≃ b
⊢ AA.OneOfThree (a < b) (a ≃ b) (a > b)
Theorem: Lean4Axiomatic.Integer.order_trichotomy
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
a✝ : a - b ≃ 0
this : a ≃ b
⊢ AA.OneOfThree (a < b) (a ≃ b) (a > b)
Tactic:
exact AA.OneOfThree.second ‹a ≃ b›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.order_trichotomy
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
b✝ : Positive (a - b)
⊢ AA.OneOfThree (a < b) (a ≃ b) (a > b)
Tactic:
have : a > b := gt_iff_pos_diff.mpr ‹Positive (a - b)›
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
b✝ : Positive (a - b)
this : a > b
⊢ AA.OneOfThree (a < b) (a ≃ b) (a > b)
Theorem: Lean4Axiomatic.Integer.order_trichotomy
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
b✝ : Positive (a - b)
this : a > b
⊢ AA.OneOfThree (a < b) (a ≃ b) (a > b)
Tactic:
exact AA.OneOfThree.third ‹a > b›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.order_trichotomy
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
c✝ : Negative (a - b)
⊢ AA.OneOfThree (a < b) (a ≃ b) (a > b)
Tactic:
have : a < b := lt_iff_neg_diff.mpr ‹Negative (a - b)›
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
c✝ : Negative (a - b)
this : a < b
⊢ AA.OneOfThree (a < b) (a ≃ b) (a > b)
Theorem: Lean4Axiomatic.Integer.order_trichotomy
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
c✝ : Negative (a - b)
this : a < b
⊢ AA.OneOfThree (a < b) (a ≃ b) (a > b)
Tactic:
exact AA.OneOfThree.first ‹a < b›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.order_trichotomy
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
⊢ ¬AA.TwoOfThree (a < b) (a ≃ b) (a > b)
Tactic:
intro (_ : AA.TwoOfThree (a < b) (a ≃ b) (a > b))
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
x✝ : AA.TwoOfThree (a < b) (a ≃ b) (a > b)
⊢ False
Theorem: Lean4Axiomatic.Integer.order_trichotomy
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
x✝ : AA.TwoOfThree (a < b) (a ≃ b) (a > b)
⊢ False
Tactic:
let ab := a - b
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
x✝ : AA.TwoOfThree (a < b) (a ≃ b) (a > b)
ab : ℤ := a - b
⊢ False
Theorem: Lean4Axiomatic.Integer.order_trichotomy
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
x✝ : AA.TwoOfThree (a < b) (a ≃ b) (a > b)
ab : ℤ := a - b
⊢ False
Tactic:
have abTwo : AA.TwoOfThree (ab ≃ 0) (Positive ab) (Negative ab) :=
  match ‹AA.TwoOfThree (a < b) (a ≃ b) (a > b)› with
  | AA.TwoOfThree.oneAndTwo (_ : a < b) (_ : a ≃ b) =>
    have : Negative ab := lt_iff_neg_diff.mp ‹a < b›
    have : ab ≃ 0 := zero_diff_iff_eqv.mpr ‹a ≃ b›
    AA.TwoOfThree.oneAndThree ‹ab ≃ 0› ‹Negative ab›
  | AA.TwoOfThree.oneAndThree (_ : a < b) (_ : a > b) =>
    have : Negative ab := lt_iff_neg_diff.mp ‹a < b›
    have : Positive ab := gt_iff_pos_diff.mp ‹a > b›
    AA.TwoOfThree.twoAndThree ‹Positive ab› ‹Negative ab›
  | AA.TwoOfThree.twoAndThree (_ : a ≃ b) (_ : a > b) =>
    have : ab ≃ 0 := zero_diff_iff_eqv.mpr ‹a ≃ b›
    have : Positive ab := gt_iff_pos_diff.mp ‹a > b›
    AA.TwoOfThree.oneAndTwo ‹ab ≃ 0› ‹Positive ab›
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
x✝ : AA.TwoOfThree (a < b) (a ≃ b) (a > b)
ab : ℤ := a - b
abTwo : AA.TwoOfThree (ab ≃ 0) (Positive ab) (Negative ab)
⊢ False
Theorem: Lean4Axiomatic.Integer.order_trichotomy
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
x✝ : AA.TwoOfThree (a < b) (a ≃ b) (a > b)
ab : ℤ := a - b
abTwo : AA.TwoOfThree (ab ≃ 0) (Positive ab) (Negative ab)
⊢ False
Tactic:
have abNotTwo
  : ¬ AA.TwoOfThree (ab ≃ 0) (Positive ab) (Negative ab)
  := abTri.atMostOne
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
x✝ : AA.TwoOfThree (a < b) (a ≃ b) (a > b)
ab : ℤ := a - b
abTwo : AA.TwoOfThree (ab ≃ 0) (Positive ab) (Negative ab)
abNotTwo : ¬AA.TwoOfThree (ab ≃ 0) (Positive ab) (Negative ab)
⊢ False
Theorem: Lean4Axiomatic.Integer.order_trichotomy
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
x✝ : AA.TwoOfThree (a < b) (a ≃ b) (a > b)
ab : ℤ := a - b
abTwo : AA.TwoOfThree (ab ≃ 0) (Positive ab) (Negative ab)
abNotTwo : ¬AA.TwoOfThree (ab ≃ 0) (Positive ab) (Negative ab)
⊢ False
Tactic:
exact absurd abTwo abNotTwo
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.le_refl
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a : ℤ
⊢ a ≤ a
Tactic:
apply le_iff_add_nat.mpr
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a : ℤ
⊢ ∃ k, a ≃ a + coe k
Theorem: Lean4Axiomatic.Integer.le_refl
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a : ℤ
⊢ ∃ k, a ≃ a + coe k
Tactic:
have : a ≃ a + coe (0 : ℕ) := calc
  a               ≃ _ := Rel.symm AA.identR
  a + 0           ≃ _ := Rel.refl
  a + coe (0 : ℕ) ≃ _ := Rel.refl
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a : ℤ
this : a ≃ a + coe 0
⊢ ∃ k, a ≃ a + coe k
Theorem: Lean4Axiomatic.Integer.le_refl
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a : ℤ
this : a ≃ a + coe 0
⊢ ∃ k, a ≃ a + coe k
Tactic:
exact Exists.intro 0 ‹a ≃ a + coe (0 : ℕ)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.le_iff_lt_or_eqv
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
⊢ a ≤ b ↔ a < b ∨ a ≃ b
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
⊢ a ≤ b → a < b ∨ a ≃ b

case mpr
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
⊢ a < b ∨ a ≃ b → a ≤ b
Theorem: Lean4Axiomatic.Integer.le_iff_lt_or_eqv
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
⊢ a ≤ b → a < b ∨ a ≃ b
Tactic:
case mp =>
  intro (_ : a ≤ b)
  show a < b ∨ a ≃ b
  have : Decidable (a ≃ b) := eqv? a b
  have : a < b ∨ a ≃ b := match this with
  | isTrue (_ : a ≃ b) =>
    Or.inr ‹a ≃ b›
  | isFalse (_ : a ≄ b) =>
    have : a < b := lt_iff_le_neqv.mpr (And.intro ‹a ≤ b› ‹a ≄ b›)
    Or.inl ‹a < b›
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.le_iff_lt_or_eqv
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
⊢ a < b ∨ a ≃ b → a ≤ b
Tactic:
case mpr =>
  intro (_ : a < b ∨ a ≃ b)
  show a ≤ b
  have : a ≤ b := match ‹a < b ∨ a ≃ b› with
  | Or.inl (_ : a < b) =>
    have (And.intro (_ : a ≤ b) _) := lt_iff_le_neqv.mp ‹a < b›
    ‹a ≤ b›
  | Or.inr (_ : a ≃ b) =>
    have : a ≤ a := le_refl
    have : a ≤ b := AA.substRFn ‹a ≃ b› ‹a ≤ a›
    ‹a ≤ b›
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.le_iff_lt_or_eqv
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
⊢ a ≤ b → a < b ∨ a ≃ b
Tactic:
intro (_ : a ≤ b)
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : a ≤ b
⊢ a < b ∨ a ≃ b
Theorem: Lean4Axiomatic.Integer.le_iff_lt_or_eqv
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : a ≤ b
⊢ a < b ∨ a ≃ b
Tactic:
have : Decidable (a ≃ b) := eqv? a b
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : a ≤ b
this : Decidable (a ≃ b)
⊢ a < b ∨ a ≃ b