internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Integer.le_widen_lt
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 + 1
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 + 1
Theorem: Lean4Axiomatic.Integer.le_widen_lt
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 + 1
Tactic:
have : b < b + 1 := lt_inc
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 : b < b + 1
⊢ a < b + 1
Theorem: Lean4Axiomatic.Integer.le_widen_lt
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 : b < b + 1
⊢ a < b + 1
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✝ : b < b + 1
this : a < b ∨ a ≃ b
⊢ a < b + 1
Theorem: Lean4Axiomatic.Integer.le_widen_lt
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✝ : b < b + 1
this : a < b ∨ a ≃ b
⊢ a < b + 1
Tactic:
have : a < b + 1 := match ‹a < b ∨ a ≃ b› with
| Or.inl (_ : a < b) => Rel.trans ‹a < b› ‹b < b + 1›
| Or.inr (_ : a ≃ b) => AA.substLFn (Rel.symm ‹a ≃ b›) ‹b < b + 1›
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✝¹ : b < b + 1
this✝ : a < b ∨ a ≃ b
this : a < b + 1
⊢ a < b + 1
Theorem: Lean4Axiomatic.Integer.le_widen_lt
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✝¹ : b < b + 1
this✝ : a < b ∨ a ≃ b
this : a < b + 1
⊢ a < b + 1
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.lt_sgn
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 ↔ sgn (a - b) ≃ -1
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 → sgn (a - b) ≃ -1

case mpr
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
⊢ sgn (a - b) ≃ -1 → a < b
Theorem: Lean4Axiomatic.Integer.lt_sgn
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 → sgn (a - b) ≃ -1
Tactic:
case mp =>
  intro (_ : a < b)
  show sgn (a - b) ≃ -1
  have : Negative (a - b) := lt_iff_neg_diff.mp ‹a < b›
  have : sgn (a - b) ≃ -1 := sgn_negative.mp this
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.lt_sgn
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
⊢ sgn (a - b) ≃ -1 → a < b
Tactic:
case mpr =>
  intro (_ : sgn (a - b) ≃ -1)
  show a < b
  have : Negative (a - b) := sgn_negative.mpr ‹sgn (a - b) ≃ -1›
  have : a < b := lt_iff_neg_diff.mpr this
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.lt_sgn
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 → sgn (a - b) ≃ -1
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
⊢ sgn (a - b) ≃ -1
Theorem: Lean4Axiomatic.Integer.lt_sgn
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
⊢ sgn (a - b) ≃ -1
Tactic:
have : Negative (a - b) := lt_iff_neg_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 : ℤ
x✝ : a < b
this : Negative (a - b)
⊢ sgn (a - b) ≃ -1
Theorem: Lean4Axiomatic.Integer.lt_sgn
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 : Negative (a - b)
⊢ sgn (a - b) ≃ -1
Tactic:
have : sgn (a - b) ≃ -1 := sgn_negative.mp 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✝ : Negative (a - b)
this : sgn (a - b) ≃ -1
⊢ sgn (a - b) ≃ -1
Theorem: Lean4Axiomatic.Integer.lt_sgn
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✝ : Negative (a - b)
this : sgn (a - b) ≃ -1
⊢ sgn (a - b) ≃ -1
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.lt_sgn
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
⊢ sgn (a - b) ≃ -1 → a < b
Tactic:
intro (_ : sgn (a - b) ≃ -1)
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : sgn (a - b) ≃ -1
⊢ a < b
Theorem: Lean4Axiomatic.Integer.lt_sgn
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : sgn (a - b) ≃ -1
⊢ a < b
Tactic:
have : Negative (a - b) := sgn_negative.mpr ‹sgn (a - b) ≃ -1›
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : sgn (a - b) ≃ -1
this : Negative (a - b)
⊢ a < b
Theorem: Lean4Axiomatic.Integer.lt_sgn
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : sgn (a - b) ≃ -1
this : Negative (a - b)
⊢ a < b
Tactic:
have : a < b := lt_iff_neg_diff.mpr 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✝ : sgn (a - b) ≃ -1
this✝ : Negative (a - b)
this : a < b
⊢ a < b
Theorem: Lean4Axiomatic.Integer.lt_sgn
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : sgn (a - b) ≃ -1
this✝ : Negative (a - b)
this : a < b
⊢ a < b
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.gt_sgn
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 ↔ sgn (a - b) ≃ 1
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 → sgn (a - b) ≃ 1

case mpr
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
⊢ sgn (a - b) ≃ 1 → a > b
Theorem: Lean4Axiomatic.Integer.gt_sgn
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 → sgn (a - b) ≃ 1
Tactic:
case mp =>
  intro (_ : a > b)
  show sgn (a - b) ≃ 1
  have : Positive (a - b) := gt_iff_pos_diff.mp ‹a > b›
  have : sgn (a - b) ≃ 1 := sgn_positive.mp this
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.gt_sgn
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
⊢ sgn (a - b) ≃ 1 → a > b
Tactic:
case mpr =>
  intro (_ : sgn (a - b) ≃ 1)
  show a > b
  have : Positive (a - b) := sgn_positive.mpr ‹sgn (a - b) ≃ 1›
  have : a > b := gt_iff_pos_diff.mpr this
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.gt_sgn
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 → sgn (a - b) ≃ 1
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
⊢ sgn (a - b) ≃ 1
Theorem: Lean4Axiomatic.Integer.gt_sgn
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
⊢ sgn (a - b) ≃ 1
Tactic:
have : Positive (a - b) := 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 : ℤ
x✝ : a > b
this : Positive (a - b)
⊢ sgn (a - b) ≃ 1
Theorem: Lean4Axiomatic.Integer.gt_sgn
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 : Positive (a - b)
⊢ sgn (a - b) ≃ 1
Tactic:
have : sgn (a - b) ≃ 1 := sgn_positive.mp 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✝ : Positive (a - b)
this : sgn (a - b) ≃ 1
⊢ sgn (a - b) ≃ 1
Theorem: Lean4Axiomatic.Integer.gt_sgn
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✝ : Positive (a - b)
this : sgn (a - b) ≃ 1
⊢ sgn (a - b) ≃ 1
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.gt_sgn
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
⊢ sgn (a - b) ≃ 1 → a > b
Tactic:
intro (_ : sgn (a - b) ≃ 1)
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : sgn (a - b) ≃ 1
⊢ a > b
Theorem: Lean4Axiomatic.Integer.gt_sgn
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : sgn (a - b) ≃ 1
⊢ a > b
Tactic:
have : Positive (a - b) := sgn_positive.mpr ‹sgn (a - b) ≃ 1›
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : sgn (a - b) ≃ 1
this : Positive (a - b)
⊢ a > b
Theorem: Lean4Axiomatic.Integer.gt_sgn
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : sgn (a - b) ≃ 1
this : Positive (a - b)
⊢ a > b
Tactic:
have : a > b := gt_iff_pos_diff.mpr 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✝ : sgn (a - b) ≃ 1
this✝ : Positive (a - b)
this : a > b
⊢ a > b
Theorem: Lean4Axiomatic.Integer.gt_sgn
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : sgn (a - b) ≃ 1
this✝ : Positive (a - b)
this : a > b
⊢ a > b
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.neg_one_neqv_zero
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
⊢ -1 ≄ 0
Tactic:
intro (_ : -1 ≃ (0:ℤ))
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : -1 ≃ 0
⊢ False
Theorem: Lean4Axiomatic.Integer.neg_one_neqv_zero
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : -1 ≃ 0
⊢ False
Tactic:
have : 1 ≃ (0:ℤ) := calc
  1      ≃ _ := Rel.symm AA.identR
  1 + 0  ≃ _ := AA.substR (Rel.symm ‹-1 ≃ (0:ℤ)›)
  1 + -1 ≃ _ := AA.inverseR
  0      ≃ _ := Rel.refl
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : -1 ≃ 0
this : 1 ≃ 0
⊢ False
Theorem: Lean4Axiomatic.Integer.neg_one_neqv_zero
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : -1 ≃ 0
this : 1 ≃ 0
⊢ False
Tactic:
have : (1:ℤ) ≄ 0 := one_neqv_zero
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : -1 ≃ 0
this✝ : 1 ≃ 0
this : 1 ≄ 0
⊢ False
Theorem: Lean4Axiomatic.Integer.neg_one_neqv_zero
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : -1 ≃ 0
this✝ : 1 ≃ 0
this : 1 ≄ 0
⊢ False
Tactic:
exact absurd ‹1 ≃ (0:ℤ)› ‹1 ≄ (0:ℤ)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.neg_one_neqv_one
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
⊢ -1 ≄ 1
Tactic:
intro (_ : -1 ≃ (1 : ℤ))
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : -1 ≃ 1
⊢ False
Theorem: Lean4Axiomatic.Integer.neg_one_neqv_one
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : -1 ≃ 1
⊢ False
Tactic:
have : step 0 ≃ 1 := Rel.symm Natural.literal_step
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : -1 ≃ 1
this : step 0 ≃ 1
⊢ False
Theorem: Lean4Axiomatic.Integer.neg_one_neqv_one
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : -1 ≃ 1
this : step 0 ≃ 1
⊢ False
Tactic:
have : (step 1 : ℤ) ≃ (0 : ℤ) := calc
  (step 1 : ℤ)           ≃ _ := AA.subst₁ (AA.subst₁ (Rel.symm AA.identR))
  (step (1 + 0) : ℤ)     ≃ _ := AA.subst₁ AA.scompatR
  ((1 + step 0 : ℕ) : ℤ) ≃ _ := AA.subst₁ (AA.substR ‹step 0 ≃ 1›)
  ((1 + 1 : ℕ) : ℤ)      ≃ _ := AA.compat₂
  (1 : ℤ) + (1 : ℤ)      ≃ _ := AA.substR (Rel.symm ‹-1 ≃ (1 : ℤ)›)
  1 + -1                 ≃ _ := AA.inverseR
  0                      ≃ _ := Rel.refl
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : -1 ≃ 1
this✝ : step 0 ≃ 1
this : coe (step 1) ≃ 0
⊢ False
Theorem: Lean4Axiomatic.Integer.neg_one_neqv_one
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : -1 ≃ 1
this✝ : step 0 ≃ 1
this : coe (step 1) ≃ 0
⊢ False
Tactic:
have : step 1 ≃ 0 := AA.inject ‹((step 1 : ℕ) : ℤ) ≃ ((0 : ℕ) : ℤ)›
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : -1 ≃ 1
this✝¹ : step 0 ≃ 1
this✝ : coe (step 1) ≃ 0
this : step 1 ≃ 0
⊢ False
Theorem: Lean4Axiomatic.Integer.neg_one_neqv_one
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : -1 ≃ 1
this✝¹ : step 0 ≃ 1
this✝ : coe (step 1) ≃ 0
this : step 1 ≃ 0
⊢ False
Tactic:
have : step 1 ≄ 0 := Natural.step_neqv_zero
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : -1 ≃ 1
this✝² : step 0 ≃ 1
this✝¹ : coe (step 1) ≃ 0
this✝ : step 1 ≃ 0
this : step 1 ≄ 0
⊢ False
Theorem: Lean4Axiomatic.Integer.neg_one_neqv_one
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : -1 ≃ 1
this✝² : step 0 ≃ 1
this✝¹ : coe (step 1) ≃ 0
this✝ : step 1 ≃ 0
this : step 1 ≄ 0
⊢ False
Tactic:
exact absurd ‹step 1 ≃ 0› ‹step 1 ≄ 0›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.signs_distinct
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a : ℤ
⊢ ¬AA.TwoOfThree (a ≃ 0) (a ≃ 1) (a ≃ -1)
Tactic:
intro (two : AA.TwoOfThree (a ≃ 0) (a ≃ 1) (a ≃ -1))
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a : ℤ
two : AA.TwoOfThree (a ≃ 0) (a ≃ 1) (a ≃ -1)
⊢ False
Theorem: Lean4Axiomatic.Integer.signs_distinct
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a : ℤ
two : AA.TwoOfThree (a ≃ 0) (a ≃ 1) (a ≃ -1)
⊢ False
Tactic:
match two with
| AA.TwoOfThree.oneAndTwo (_ : a ≃ 0) (_ : a ≃ 1) =>
  exact Rel.trans_failR ‹a ≃ 1› one_neqv_zero ‹a ≃ 0›
| AA.TwoOfThree.oneAndThree (_ : a ≃ 0) (_ : a ≃ -1) =>
  exact Rel.trans_failR ‹a ≃ -1› neg_one_neqv_zero ‹a ≃ 0›
| AA.TwoOfThree.twoAndThree (_ : a ≃ 1) (_ : a ≃ -1) =>
  exact Rel.trans_failR ‹a ≃ -1› neg_one_neqv_one ‹a ≃ 1›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.signs_distinct
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a : ℤ
two : AA.TwoOfThree (a ≃ 0) (a ≃ 1) (a ≃ -1)
a✝ : a ≃ 0
b✝ : a ≃ 1
⊢ False
Tactic:
exact Rel.trans_failR ‹a ≃ 1› one_neqv_zero ‹a ≃ 0›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.signs_distinct
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a : ℤ
two : AA.TwoOfThree (a ≃ 0) (a ≃ 1) (a ≃ -1)
a✝ : a ≃ 0
c✝ : a ≃ -1
⊢ False
Tactic:
exact Rel.trans_failR ‹a ≃ -1› neg_one_neqv_zero ‹a ≃ 0›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.signs_distinct
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a : ℤ
two : AA.TwoOfThree (a ≃ 0) (a ≃ 1) (a ≃ -1)
b✝ : a ≃ 1
c✝ : a ≃ -1
⊢ False
Tactic:
exact Rel.trans_failR ‹a ≃ -1› neg_one_neqv_one ‹a ≃ 1›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.neg_inject
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ : ℤ
⊢ -a₁ ≃ -a₂ → a₁ ≃ a₂
Tactic:
intro (_ : -a₁ ≃ -a₂)
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ : ℤ
x✝ : -a₁ ≃ -a₂
⊢ a₁ ≃ a₂
Theorem: Lean4Axiomatic.Integer.neg_inject
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ : ℤ
x✝ : -a₁ ≃ -a₂
⊢ a₁ ≃ a₂
Tactic:
calc
  a₁       ≃ _ := Rel.symm neg_involutive
  (-(-a₁)) ≃ _ := AA.subst₁ ‹-a₁ ≃ -a₂›
  (-(-a₂)) ≃ _ := neg_involutive
  a₂       ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.add_cancelL
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b₁ b₂ : ℤ
⊢ a + b₁ ≃ a + b₂ → b₁ ≃ b₂
Tactic:
intro (_ : a + b₁ ≃ a + b₂)
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b₁ b₂ : ℤ
x✝ : a + b₁ ≃ a + b₂
⊢ b₁ ≃ b₂
Theorem: Lean4Axiomatic.Integer.add_cancelL
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b₁ b₂ : ℤ
x✝ : a + b₁ ≃ a + b₂
⊢ b₁ ≃ b₂
Tactic:
have reduce {x y : ℤ} : -x + (x + y) ≃ y := calc
  _ = -x + (x + y) := rfl
  _ ≃ (-x + x) + y := Rel.symm AA.assoc
  _ ≃ 0 + y        := AA.substL AA.inverseL
  _ ≃ y            := AA.identL
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b₁ b₂ : ℤ
x✝ : a + b₁ ≃ a + b₂
reduce : ∀ {x y : ℤ}, -x + (x + y) ≃ y
⊢ b₁ ≃ b₂
Theorem: Lean4Axiomatic.Integer.add_cancelL
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b₁ b₂ : ℤ
x✝ : a + b₁ ≃ a + b₂
reduce : ∀ {x y : ℤ}, -x + (x + y) ≃ y
⊢ b₁ ≃ b₂
Tactic:
calc
  _ = b₁            := rfl
  _ ≃ -a + (a + b₁) := Rel.symm reduce
  _ ≃ -a + (a + b₂) := AA.substR ‹a + b₁ ≃ a + b₂›
  _ ≃ b₂            := reduce
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.add_cancelR
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ b : ℤ
⊢ a₁ + b ≃ a₂ + b → a₁ ≃ a₂
Tactic:
intro (_ : a₁ + b ≃ a₂ + b)
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ b : ℤ
x✝ : a₁ + b ≃ a₂ + b
⊢ a₁ ≃ a₂