Theorem: Lean4Axiomatic.Integer.le_iff_lt_or_eqv (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 ∨ a ≃ b
Tactic:
apply Iff.intro
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

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

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

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

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

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
this : Decidable (a ≃ b)
⊢ a < b ∨ a ≃ b
Tactic:
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›
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)
this : a < b ∨ a ≃ b
⊢ a < b ∨ a ≃ b

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
this✝ : Decidable (a ≃ b)
this : a < b ∨ a ≃ b
⊢ a < b ∨ a ≃ b
Tactic:
exact this
State after:
no goals

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 ∨ 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 ∨ a ≃ b
⊢ a ≤ b

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 : 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›
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
this : a ≤ b
⊢ a ≤ b

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
this : a ≤ b
⊢ a ≤ b
Tactic:
exact this
State after:
no goals