internlm/Lean-Github huggingface dataset:
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
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›
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)
this : 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 : ℤ
x✝ : a ≤ b
this✝ : Decidable (a ≃ b)
this : a < b ∨ a ≃ b
⊢ a < b ∨ a ≃ b
Tactic:
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 ∨ 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 : 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›
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
this : 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
this : a ≤ b
⊢ a ≤ b
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.le_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 : ℤ
⊢ a ≤ b ↔ -b ≤ -a
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 → -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
Theorem: Lean4Axiomatic.Integer.le_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 : ℤ
⊢ 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.le_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 : ℤ
⊢ -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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.le_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 : ℤ
⊢ a ≤ b → -b ≤ -a
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
⊢ -b ≤ -a
Theorem: Lean4Axiomatic.Integer.le_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 : ℤ
x✝ : a ≤ b
⊢ -b ≤ -a
Tactic:
have : a < b ∨ a ≃ b := le_iff_lt_or_eqv.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 : ℤ
x✝ : a ≤ b
this : a < b ∨ a ≃ b
⊢ -b ≤ -a
Theorem: Lean4Axiomatic.Integer.le_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 : ℤ
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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.le_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 : ℤ
x✝ : a ≤ b
this : a < b ∨ a ≃ b
h✝ : a < b
⊢ -b ≤ -a
Tactic:
have : -b < -a := lt_neg_flip.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 : ℤ
x✝ : a ≤ b
this✝ : a < b ∨ a ≃ b
h✝ : a < b
this : -b < -a
⊢ -b ≤ -a
Theorem: Lean4Axiomatic.Integer.le_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 : ℤ
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)
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✝¹ : a < b ∨ a ≃ b
h✝ : a < b
this✝ : -b < -a
this : -b ≤ -a
⊢ -b ≤ -a
Theorem: Lean4Axiomatic.Integer.le_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 : ℤ
x✝ : a ≤ b
this✝¹ : a < b ∨ a ≃ b
h✝ : a < b
this✝ : -b < -a
this : -b ≤ -a
⊢ -b ≤ -a
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.le_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 : ℤ
x✝ : a ≤ b
this : a < b ∨ a ≃ b
h✝ : a ≃ b
⊢ -b ≤ -a
Tactic:
have : -b ≃ -a := AA.subst₁ (Rel.symm ‹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✝ : a < b ∨ a ≃ b
h✝ : a ≃ b
this : -b ≃ -a
⊢ -b ≤ -a
Theorem: Lean4Axiomatic.Integer.le_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 : ℤ
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)
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✝¹ : a < b ∨ a ≃ b
h✝ : a ≃ b
this✝ : -b ≃ -a
this : -b ≤ -a
⊢ -b ≤ -a
Theorem: Lean4Axiomatic.Integer.le_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 : ℤ
x✝ : a ≤ b
this✝¹ : a < b ∨ a ≃ b
h✝ : a ≃ b
this✝ : -b ≃ -a
this : -b ≤ -a
⊢ -b ≤ -a
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.le_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 : ℤ
⊢ -b ≤ -a → a ≤ b
Tactic:
intro (_ : -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 : ℤ
x✝ : -b ≤ -a
⊢ a ≤ b
Theorem: Lean4Axiomatic.Integer.le_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 : ℤ
x✝ : -b ≤ -a
⊢ a ≤ b
Tactic:
have : -b < -a ∨ -b ≃ -a := le_iff_lt_or_eqv.mp ‹-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 : ℤ
x✝ : -b ≤ -a
this : -b < -a ∨ -b ≃ -a
⊢ a ≤ b
Theorem: Lean4Axiomatic.Integer.le_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 : ℤ
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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.le_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 : ℤ
x✝ : -b ≤ -a
this : -b < -a ∨ -b ≃ -a
h✝ : -b < -a
⊢ a ≤ b
Tactic:
have : a < b := lt_neg_flip.mpr ‹-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 : ℤ
x✝ : -b ≤ -a
this✝ : -b < -a ∨ -b ≃ -a
h✝ : -b < -a
this : a < b
⊢ a ≤ b
Theorem: Lean4Axiomatic.Integer.le_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 : ℤ
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)
Proof 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
Theorem: Lean4Axiomatic.Integer.le_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 : ℤ
x✝ : -b ≤ -a
this✝¹ : -b < -a ∨ -b ≃ -a
h✝ : -b < -a
this✝ : a < b
this : a ≤ b
⊢ a ≤ b
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.le_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 : ℤ
x✝ : -b ≤ -a
this : -b < -a ∨ -b ≃ -a
h✝ : -b ≃ -a
⊢ a ≤ b
Tactic:
have : a ≃ b := AA.inject (Rel.symm ‹-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 : ℤ
x✝ : -b ≤ -a
this✝ : -b < -a ∨ -b ≃ -a
h✝ : -b ≃ -a
this : a ≃ b
⊢ a ≤ b
Theorem: Lean4Axiomatic.Integer.le_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 : ℤ
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)
Proof 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
Theorem: Lean4Axiomatic.Integer.le_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 : ℤ
x✝ : -b ≤ -a
this✝¹ : -b < -a ∨ -b ≃ -a
h✝ : -b ≃ -a
this✝ : a ≃ b
this : a ≤ b
⊢ a ≤ b
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.le_gt_false
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 → False
Tactic:
intro (_ : 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 : ℤ
x✝¹ : a ≤ b
x✝ : a > b
⊢ False
Theorem: Lean4Axiomatic.Integer.le_gt_false
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
x✝ : a > b
⊢ False
Tactic:
have : a < b ∨ a ≃ b := le_iff_lt_or_eqv.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 : ℤ
x✝¹ : a ≤ b
x✝ : a > b
this : a < b ∨ a ≃ b
⊢ False
Theorem: Lean4Axiomatic.Integer.le_gt_false
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
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
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
x✝ : a > b
this : a < b ∨ a ≃ b
notTwo : ¬AA.TwoOfThree (a < b) (a ≃ b) (a > b)
⊢ False
Theorem: Lean4Axiomatic.Integer.le_gt_false
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
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›
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
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
Theorem: Lean4Axiomatic.Integer.le_gt_false
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
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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.lt_ge_false
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 → False
Tactic:
intro (_ : b > a) (_ : 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 : ℤ
x✝¹ : b > a
x✝ : b ≤ a
⊢ False
Theorem: Lean4Axiomatic.Integer.lt_ge_false
Proof 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
x✝ : b ≤ a
⊢ False
Tactic:
exact le_gt_false ‹b ≤ a› ‹b > a›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.lt_inc
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a : ℤ
⊢ a < a + 1
Tactic:
apply lt_iff_neg_diff.mpr
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a : ℤ
⊢ Negative (a - (a + 1))
Theorem: Lean4Axiomatic.Integer.lt_inc
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a : ℤ
⊢ Negative (a - (a + 1))
Tactic:
have : a - (a + 1) ≃ -1 := calc
  a - (a + 1)   ≃ _ := sub_defn
  a + -(a + 1)  ≃ _ := AA.substR neg_compat_add
  a + (-a + -1) ≃ _ := Rel.symm AA.assoc
  (a + -a) + -1 ≃ _ := AA.substL AA.inverseR
  (0 : ℤ) + -1  ≃ _ := AA.identL
  (-1)          ≃ _ := 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 + 1) ≃ -1
⊢ Negative (a - (a + 1))
Theorem: Lean4Axiomatic.Integer.lt_inc
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 + 1) ≃ -1
⊢ Negative (a - (a + 1))
Tactic:
apply AA.substFn (Rel.symm ‹a - (a + 1) ≃ -1›)
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 + 1) ≃ -1
⊢ Negative (-1)
Theorem: Lean4Axiomatic.Integer.lt_inc
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 + 1) ≃ -1
⊢ Negative (-1)
Tactic:
exact neg_one_negative
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.zero_lt_one
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
⊢ 0 < 1
Tactic:
have : (0 : ℤ) < 0 + 1 := lt_inc
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
this : 0 < 0 + 1
⊢ 0 < 1
Theorem: Lean4Axiomatic.Integer.zero_lt_one
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
this : 0 < 0 + 1
⊢ 0 < 1
Tactic:
have : (0 : ℤ) < 1 := lt_substR_eqv AA.identL this
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
this✝ : 0 < 0 + 1
this : 0 < 1
⊢ 0 < 1
Theorem: Lean4Axiomatic.Integer.zero_lt_one
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
this✝ : 0 < 0 + 1
this : 0 < 1
⊢ 0 < 1
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.neg_one_lt_zero
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
⊢ -1 < 0
Tactic:
have : (-1 : ℤ) < -1 + 1 := lt_inc
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
this : -1 < -1 + 1
⊢ -1 < 0
Theorem: Lean4Axiomatic.Integer.neg_one_lt_zero
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
this : -1 < -1 + 1
⊢ -1 < 0
Tactic:
have : (-1 : ℤ) < 0 := lt_substR_eqv AA.inverseL this
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
this✝ : -1 < -1 + 1
this : -1 < 0
⊢ -1 < 0
Theorem: Lean4Axiomatic.Integer.neg_one_lt_zero
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
this✝ : -1 < -1 + 1
this : -1 < 0
⊢ -1 < 0
Tactic:
exact this
Proof state after:
no goals