Theorem: Lean4Axiomatic.Integer.le_neg_flip (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 ↔ -b ≤ -a
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 → -b ≤ -a

case mpr
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
⊢ -b ≤ -a → 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 → -b ≤ -a
Tactic:
case mp =>
  intro (_ : a ≤ b)
  show -b ≤ -a
  have : a < b ∨ a ≃ b := le_iff_lt_or_eqv.mp ‹a ≤ b›
  match this with
  | Or.inl (_ : a < b) =>
    have : -b < -a := lt_neg_flip.mp ‹a < b›
    have : -b ≤ -a := le_iff_lt_or_eqv.mpr (Or.inl this)
    exact this
  | Or.inr (_ : a ≃ b) =>
    have : -b ≃ -a := AA.subst₁ (Rel.symm ‹a ≃ b›)
    have : -b ≤ -a := le_iff_lt_or_eqv.mpr (Or.inr this)
    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 : ℤ
⊢ -b ≤ -a → a ≤ b
Tactic:
case mpr =>
  intro (_ : -b ≤ -a)
  show a ≤ b
  have : -b < -a ∨ -b ≃ -a := le_iff_lt_or_eqv.mp ‹-b ≤ -a›
  match this with
  | Or.inl (_ : -b < -a) =>
    have : a < b := lt_neg_flip.mpr ‹-b < -a›
    have : a ≤ b := le_iff_lt_or_eqv.mpr (Or.inl this)
    exact this
  | Or.inr (_ : -b ≃ -a) =>
    have : a ≃ b := AA.inject (Rel.symm ‹-b ≃ -a›)
    have : a ≤ b := le_iff_lt_or_eqv.mpr (Or.inr this)
    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 → -b ≤ -a
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
⊢ -b ≤ -a

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

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 : a < b ∨ a ≃ b
⊢ -b ≤ -a
Tactic:
match this with
| Or.inl (_ : a < b) =>
  have : -b < -a := lt_neg_flip.mp ‹a < b›
  have : -b ≤ -a := le_iff_lt_or_eqv.mpr (Or.inl this)
  exact this
| Or.inr (_ : a ≃ b) =>
  have : -b ≃ -a := AA.subst₁ (Rel.symm ‹a ≃ b›)
  have : -b ≤ -a := le_iff_lt_or_eqv.mpr (Or.inr this)
  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 : ℤ
x✝ : a ≤ b
this : a < b ∨ a ≃ b
h✝ : a < b
⊢ -b ≤ -a
Tactic:
have : -b < -a := lt_neg_flip.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
this✝ : a < b ∨ a ≃ b
h✝ : a < b
this : -b < -a
⊢ -b ≤ -a

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✝ : a < b ∨ a ≃ b
h✝ : a < b
this : -b < -a
⊢ -b ≤ -a
Tactic:
have : -b ≤ -a := le_iff_lt_or_eqv.mpr (Or.inl this)
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✝¹ : a < b ∨ a ≃ b
h✝ : a < b
this✝ : -b < -a
this : -b ≤ -a
⊢ -b ≤ -a

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✝¹ : a < b ∨ a ≃ b
h✝ : a < b
this✝ : -b < -a
this : -b ≤ -a
⊢ -b ≤ -a
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 : ℤ
x✝ : a ≤ b
this : a < b ∨ a ≃ b
h✝ : a ≃ b
⊢ -b ≤ -a
Tactic:
have : -b ≃ -a := AA.subst₁ (Rel.symm ‹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✝ : a < b ∨ a ≃ b
h✝ : a ≃ b
this : -b ≃ -a
⊢ -b ≤ -a

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✝ : a < b ∨ a ≃ b
h✝ : a ≃ b
this : -b ≃ -a
⊢ -b ≤ -a
Tactic:
have : -b ≤ -a := le_iff_lt_or_eqv.mpr (Or.inr this)
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✝¹ : a < b ∨ a ≃ b
h✝ : a ≃ b
this✝ : -b ≃ -a
this : -b ≤ -a
⊢ -b ≤ -a

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✝¹ : a < b ∨ a ≃ b
h✝ : a ≃ b
this✝ : -b ≃ -a
this : -b ≤ -a
⊢ -b ≤ -a
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 : ℤ
⊢ -b ≤ -a → a ≤ b
Tactic:
intro (_ : -b ≤ -a)
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : -b ≤ -a
⊢ 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✝ : -b ≤ -a
⊢ a ≤ b
Tactic:
have : -b < -a ∨ -b ≃ -a := le_iff_lt_or_eqv.mp ‹-b ≤ -a›
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : -b ≤ -a
this : -b < -a ∨ -b ≃ -a
⊢ 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✝ : -b ≤ -a
this : -b < -a ∨ -b ≃ -a
⊢ a ≤ b
Tactic:
match this with
| Or.inl (_ : -b < -a) =>
  have : a < b := lt_neg_flip.mpr ‹-b < -a›
  have : a ≤ b := le_iff_lt_or_eqv.mpr (Or.inl this)
  exact this
| Or.inr (_ : -b ≃ -a) =>
  have : a ≃ b := AA.inject (Rel.symm ‹-b ≃ -a›)
  have : a ≤ b := le_iff_lt_or_eqv.mpr (Or.inr this)
  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 : ℤ
x✝ : -b ≤ -a
this : -b < -a ∨ -b ≃ -a
h✝ : -b < -a
⊢ a ≤ b
Tactic:
have : a < b := lt_neg_flip.mpr ‹-b < -a›
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : -b ≤ -a
this✝ : -b < -a ∨ -b ≃ -a
h✝ : -b < -a
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✝ : -b ≤ -a
this✝ : -b < -a ∨ -b ≃ -a
h✝ : -b < -a
this : a < b
⊢ a ≤ b
Tactic:
have : a ≤ b := le_iff_lt_or_eqv.mpr (Or.inl this)
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : -b ≤ -a
this✝¹ : -b < -a ∨ -b ≃ -a
h✝ : -b < -a
this✝ : 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✝ : -b ≤ -a
this✝¹ : -b < -a ∨ -b ≃ -a
h✝ : -b < -a
this✝ : a < b
this : 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 : ℤ
x✝ : -b ≤ -a
this : -b < -a ∨ -b ≃ -a
h✝ : -b ≃ -a
⊢ a ≤ b
Tactic:
have : a ≃ b := AA.inject (Rel.symm ‹-b ≃ -a›)
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : -b ≤ -a
this✝ : -b < -a ∨ -b ≃ -a
h✝ : -b ≃ -a
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✝ : -b ≤ -a
this✝ : -b < -a ∨ -b ≃ -a
h✝ : -b ≃ -a
this : a ≃ b
⊢ a ≤ b
Tactic:
have : a ≤ b := le_iff_lt_or_eqv.mpr (Or.inr this)
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : -b ≤ -a
this✝¹ : -b < -a ∨ -b ≃ -a
h✝ : -b ≃ -a
this✝ : 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✝ : -b ≤ -a
this✝¹ : -b < -a ∨ -b ≃ -a
h✝ : -b ≃ -a
this✝ : a ≃ b
this : a ≤ b
⊢ a ≤ b
Tactic:
exact this
State after:
no goals