Theorem: Lean4Axiomatic.Integer.le_gt_false (Lean4Axiomatic/Integer/Order.lean)

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 → False
Tactic:
intro (_ : a ≤ b) (_ : a > b)
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
x✝ : a > b
⊢ False

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
x✝ : a > b
⊢ False
Tactic:
have : a < b ∨ a ≃ b := le_iff_lt_or_eqv.mp ‹a ≤ b›
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
x✝ : a > b
this : a < b ∨ a ≃ b
⊢ False

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
x✝ : a > b
this : a < b ∨ a ≃ b
⊢ False
Tactic:
have notTwo : ¬AA.TwoOfThree (a < b) (a ≃ b) (a > b) :=
  (order_trichotomy a b).atMostOne
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
x✝ : a > b
this : a < b ∨ a ≃ b
notTwo : ¬AA.TwoOfThree (a < b) (a ≃ b) (a > b)
⊢ False

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
x✝ : a > b
this : a < b ∨ a ≃ b
notTwo : ¬AA.TwoOfThree (a < b) (a ≃ b) (a > b)
⊢ False
Tactic:
have two : AA.TwoOfThree (a < b) (a ≃ b) (a > b) :=
  match ‹a < b ∨ a ≃ b› with
  | Or.inl (_ : a < b) => AA.TwoOfThree.oneAndThree ‹a < b› ‹a > b›
  | Or.inr (_ : a ≃ b) => AA.TwoOfThree.twoAndThree ‹a ≃ b› ‹a > b›
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
x✝ : a > b
this : a < b ∨ a ≃ b
notTwo : ¬AA.TwoOfThree (a < b) (a ≃ b) (a > b)
two : AA.TwoOfThree (a < b) (a ≃ b) (a > b)
⊢ False

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
x✝ : a > b
this : a < b ∨ a ≃ b
notTwo : ¬AA.TwoOfThree (a < b) (a ≃ b) (a > b)
two : AA.TwoOfThree (a < b) (a ≃ b) (a > b)
⊢ False
Tactic:
exact absurd two notTwo
State after:
no goals