internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Integer.lt_substR_eqv
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a₁ a₂ b : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : b < a₁
left✝ : b ≤ a₁
right✝ : b ≄ a₁
⊢ b < a₂
Tactic:
apply lt_iff_le_neqv.mpr
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a₁ a₂ b : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : b < a₁
left✝ : b ≤ a₁
right✝ : b ≄ a₁
⊢ b ≤ a₂ ∧ b ≄ a₂
Theorem: Lean4Axiomatic.Integer.lt_substR_eqv
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a₁ a₂ b : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : b < a₁
left✝ : b ≤ a₁
right✝ : b ≄ a₁
⊢ b ≤ a₂ ∧ b ≄ a₂
Tactic:
have : b ≤ a₂ := AA.substRFn ‹a₁ ≃ 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₁ a₂ b : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : b < a₁
left✝ : b ≤ a₁
right✝ : b ≄ a₁
this : b ≤ a₂
⊢ b ≤ a₂ ∧ b ≄ a₂
Theorem: Lean4Axiomatic.Integer.lt_substR_eqv
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a₁ a₂ b : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : b < a₁
left✝ : b ≤ a₁
right✝ : b ≄ a₁
this : b ≤ a₂
⊢ b ≤ a₂ ∧ b ≄ a₂
Tactic:
have : b ≄ a₂ := AA.neqv_substR ‹a₁ ≃ 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₁ a₂ b : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : b < a₁
left✝ : b ≤ a₁
right✝ : b ≄ a₁
this✝ : b ≤ a₂
this : b ≄ a₂
⊢ b ≤ a₂ ∧ b ≄ a₂
Theorem: Lean4Axiomatic.Integer.lt_substR_eqv
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a₁ a₂ b : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : b < a₁
left✝ : b ≤ a₁
right✝ : b ≄ a₁
this✝ : b ≤ a₂
this : b ≄ a₂
⊢ b ≤ a₂ ∧ b ≄ a₂
Tactic:
exact And.intro ‹b ≤ a₂› ‹b ≄ a₂›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.add_substL_lt
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
⊢ a < b → a + c < b + c
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 c : ℤ
x✝ : a < b
⊢ a + c < b + c
Theorem: Lean4Axiomatic.Integer.add_substL_lt
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝ : a < b
⊢ a + c < b + c
Tactic:
have : Positive (b - a) := 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 c : ℤ
x✝ : a < b
this : Positive (b - a)
⊢ a + c < b + c
Theorem: Lean4Axiomatic.Integer.add_substL_lt
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝ : a < b
this : Positive (b - a)
⊢ a + c < b + c
Tactic:
apply gt_iff_pos_diff.mpr
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝ : a < b
this : Positive (b - a)
⊢ Positive (b + c - (a + c))
Theorem: Lean4Axiomatic.Integer.add_substL_lt
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝ : a < b
this : Positive (b - a)
⊢ Positive (b + c - (a + c))
Tactic:
have : b - a ≃ b + c - (a + c) := Rel.symm sub_sums_sameR
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝ : a < b
this✝ : Positive (b - a)
this : b - a ≃ b + c - (a + c)
⊢ Positive (b + c - (a + c))
Theorem: Lean4Axiomatic.Integer.add_substL_lt
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝ : a < b
this✝ : Positive (b - a)
this : b - a ≃ b + c - (a + c)
⊢ Positive (b + c - (a + c))
Tactic:
exact AA.substFn ‹b - a ≃ b + c - (a + c)› ‹Positive (b - a)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.add_cancelL_lt
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
⊢ c + a < c + b → a < b
Tactic:
intro (_ : c + a < c + b)
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝ : c + a < c + b
⊢ a < b
Theorem: Lean4Axiomatic.Integer.add_cancelL_lt
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝ : c + a < c + b
⊢ a < b
Tactic:
have : Positive (c + b - (c + a)) := gt_iff_pos_diff.mp ‹c + a < c + b›
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝ : c + a < c + b
this : Positive (c + b - (c + a))
⊢ a < b
Theorem: Lean4Axiomatic.Integer.add_cancelL_lt
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝ : c + a < c + b
this : Positive (c + b - (c + a))
⊢ a < b
Tactic:
apply gt_iff_pos_diff.mpr
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝ : c + a < c + b
this : Positive (c + b - (c + a))
⊢ Positive (b - a)
Theorem: Lean4Axiomatic.Integer.add_cancelL_lt
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝ : c + a < c + b
this : Positive (c + b - (c + a))
⊢ Positive (b - a)
Tactic:
have : c + b - (c + a) ≃ b - a := calc
  c + b - (c + a) ≃ _ := AA.substL AA.comm
  b + c - (c + a) ≃ _ := AA.substR AA.comm
  b + c - (a + c) ≃ _ := sub_sums_sameR
  b - a ≃ _ := Rel.refl
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝ : c + a < c + b
this✝ : Positive (c + b - (c + a))
this : c + b - (c + a) ≃ b - a
⊢ Positive (b - a)
Theorem: Lean4Axiomatic.Integer.add_cancelL_lt
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝ : c + a < c + b
this✝ : Positive (c + b - (c + a))
this : c + b - (c + a) ≃ b - a
⊢ Positive (b - a)
Tactic:
apply AA.substFn ‹c + b - (c + 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 c : ℤ
x✝ : c + a < c + b
this✝ : Positive (c + b - (c + a))
this : c + b - (c + a) ≃ b - a
⊢ Positive (c + b - (c + a))
Theorem: Lean4Axiomatic.Integer.add_cancelL_lt
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝ : c + a < c + b
this✝ : Positive (c + b - (c + a))
this : c + b - (c + a) ≃ b - a
⊢ Positive (c + b - (c + a))
Tactic:
exact ‹Positive (c + b - (c + a))›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.mul_substL_lt
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
⊢ Positive c → a < b → a * c < b * c
Tactic:
intro (_ : Positive c) (_ : 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 c : ℤ
x✝¹ : Positive c
x✝ : a < b
⊢ a * c < b * c
Theorem: Lean4Axiomatic.Integer.mul_substL_lt
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : Positive c
x✝ : a < b
⊢ a * c < b * c
Tactic:
have : Positive (b - a) := 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 c : ℤ
x✝¹ : Positive c
x✝ : a < b
this : Positive (b - a)
⊢ a * c < b * c
Theorem: Lean4Axiomatic.Integer.mul_substL_lt
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : Positive c
x✝ : a < b
this : Positive (b - a)
⊢ a * c < b * c
Tactic:
apply gt_iff_pos_diff.mpr
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : Positive c
x✝ : a < b
this : Positive (b - a)
⊢ Positive (b * c - a * c)
Theorem: Lean4Axiomatic.Integer.mul_substL_lt
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : Positive c
x✝ : a < b
this : Positive (b - a)
⊢ Positive (b * c - a * c)
Tactic:
apply AA.substFn AA.distribR
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : Positive c
x✝ : a < b
this : Positive (b - a)
⊢ Positive (Hand.R.align HMul.hMul c (b - a))
Theorem: Lean4Axiomatic.Integer.mul_substL_lt
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : Positive c
x✝ : a < b
this : Positive (b - a)
⊢ Positive (Hand.R.align HMul.hMul c (b - a))
Tactic:
show Positive ((b - a) * c)
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : Positive c
x✝ : a < b
this : Positive (b - a)
⊢ Positive ((b - a) * c)
Theorem: Lean4Axiomatic.Integer.mul_substL_lt
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : Positive c
x✝ : a < b
this : Positive (b - a)
⊢ Positive ((b - a) * c)
Tactic:
exact mul_preserves_positive ‹Positive (b - a)› ‹Positive c›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.mul_cancelL_lt
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
⊢ Positive c → c * a < c * b → a < b
Tactic:
intro (_ : Positive c) (_ : c * a < c * b)
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : Positive c
x✝ : c * a < c * b
⊢ a < b
Theorem: Lean4Axiomatic.Integer.mul_cancelL_lt
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : Positive c
x✝ : c * a < c * b
⊢ a < b
Tactic:
have : Positive (c * b - c * a) := gt_iff_pos_diff.mp ‹c * a < c * b›
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : Positive c
x✝ : c * a < c * b
this : Positive (c * b - c * a)
⊢ a < b
Theorem: Lean4Axiomatic.Integer.mul_cancelL_lt
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : Positive c
x✝ : c * a < c * b
this : Positive (c * b - c * a)
⊢ a < b
Tactic:
apply gt_iff_pos_diff.mpr
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : Positive c
x✝ : c * a < c * b
this : Positive (c * b - c * a)
⊢ Positive (b - a)
Theorem: Lean4Axiomatic.Integer.mul_cancelL_lt
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : Positive c
x✝ : c * a < c * b
this : Positive (c * b - c * a)
⊢ Positive (b - a)
Tactic:
have : Positive (c * (b - a)) :=
  AA.substFn (Rel.symm AA.distribL) ‹Positive (c * b - c * a)›
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : Positive c
x✝ : c * a < c * b
this✝ : Positive (c * b - c * a)
this : Positive (c * (b - a))
⊢ Positive (b - a)
Theorem: Lean4Axiomatic.Integer.mul_cancelL_lt
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : Positive c
x✝ : c * a < c * b
this✝ : Positive (c * b - c * a)
this : Positive (c * (b - a))
⊢ Positive (b - a)
Tactic:
have : SameSign c (b - a) :=
  positive_mul_iff_same_sign.mp ‹Positive (c * (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 c : ℤ
x✝¹ : Positive c
x✝ : c * a < c * b
this✝¹ : Positive (c * b - c * a)
this✝ : Positive (c * (b - a))
this : SameSign c (b - a)
⊢ Positive (b - a)
Theorem: Lean4Axiomatic.Integer.mul_cancelL_lt
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : Positive c
x✝ : c * a < c * b
this✝¹ : Positive (c * b - c * a)
this✝ : Positive (c * (b - a))
this : SameSign c (b - a)
⊢ Positive (b - a)
Tactic:
have : Positive (b - a) :=
  same_sign_positive ‹SameSign c (b - a)› ‹Positive c›
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : Positive c
x✝ : c * a < c * b
this✝² : Positive (c * b - c * a)
this✝¹ : Positive (c * (b - a))
this✝ : SameSign c (b - a)
this : Positive (b - a)
⊢ Positive (b - a)
Theorem: Lean4Axiomatic.Integer.mul_cancelL_lt
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
x✝¹ : Positive c
x✝ : c * a < c * b
this✝² : Positive (c * b - c * a)
this✝¹ : Positive (c * (b - a))
this✝ : SameSign c (b - a)
this : Positive (b - a)
⊢ Positive (b - a)
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.lt_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:
have : -a - -b ≃ b - a := calc
  (-a) - -b    ≃ _ := sub_defn
  (-a) + -(-b) ≃ _ := AA.substR neg_involutive
  (-a) + b     ≃ _ := AA.comm
  b + -a       ≃ _ := Rel.symm sub_defn
  b - a        ≃ _ := Rel.refl
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
this : -a - -b ≃ b - a
⊢ a < b ↔ -b < -a
Theorem: Lean4Axiomatic.Integer.lt_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 : ℤ
this : -a - -b ≃ b - a
⊢ 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 : ℤ
this : -a - -b ≃ b - a
⊢ 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 : ℤ
this : -a - -b ≃ b - a
⊢ -b < -a → a < b
Theorem: Lean4Axiomatic.Integer.lt_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 : ℤ
this : -a - -b ≃ b - a
⊢ a < b → -b < -a
Tactic:
case mp =>
  intro (_ : a < b)
  show -b < -a
  have : Positive (b - a) := gt_iff_pos_diff.mp ‹a < b›
  apply gt_iff_pos_diff.mpr
  show Positive (-a - -b)
  exact AA.substFn (Rel.symm ‹-a - -b ≃ b - a›) ‹Positive (b - a)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.lt_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 : ℤ
this : -a - -b ≃ b - a
⊢ -b < -a → a < b
Tactic:
case mpr =>
  intro (_ : -b < -a)
  show a < b
  have : Positive (-a - -b) := gt_iff_pos_diff.mp ‹-b < -a›
  apply gt_iff_pos_diff.mpr
  show Positive (b - a)
  exact AA.substFn ‹-a - -b ≃ b - a› ‹Positive (-a - -b)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.lt_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 : ℤ
this : -a - -b ≃ b - a
⊢ 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 : ℤ
this : -a - -b ≃ b - a
x✝ : a < b
⊢ -b < -a
Theorem: Lean4Axiomatic.Integer.lt_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 : ℤ
this : -a - -b ≃ b - a
x✝ : a < b
⊢ -b < -a
Tactic:
have : Positive (b - a) := 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 : ℤ
this✝ : -a - -b ≃ b - a
x✝ : a < b
this : Positive (b - a)
⊢ -b < -a
Theorem: Lean4Axiomatic.Integer.lt_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 : ℤ
this✝ : -a - -b ≃ b - a
x✝ : a < b
this : Positive (b - a)
⊢ -b < -a
Tactic:
apply gt_iff_pos_diff.mpr
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
this✝ : -a - -b ≃ b - a
x✝ : a < b
this : Positive (b - a)
⊢ Positive (-a - -b)
Theorem: Lean4Axiomatic.Integer.lt_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 : ℤ
this✝ : -a - -b ≃ b - a
x✝ : a < b
this : Positive (b - a)
⊢ Positive (-a - -b)
Tactic:
exact AA.substFn (Rel.symm ‹-a - -b ≃ b - a›) ‹Positive (b - a)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.lt_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 : ℤ
this : -a - -b ≃ b - a
⊢ -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 : ℤ
this : -a - -b ≃ b - a
x✝ : -b < -a
⊢ a < b
Theorem: Lean4Axiomatic.Integer.lt_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 : ℤ
this : -a - -b ≃ b - a
x✝ : -b < -a
⊢ a < b
Tactic:
have : Positive (-a - -b) := gt_iff_pos_diff.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 : ℤ
this✝ : -a - -b ≃ b - a
x✝ : -b < -a
this : Positive (-a - -b)
⊢ a < b
Theorem: Lean4Axiomatic.Integer.lt_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 : ℤ
this✝ : -a - -b ≃ b - a
x✝ : -b < -a
this : Positive (-a - -b)
⊢ a < b
Tactic:
apply gt_iff_pos_diff.mpr
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
this✝ : -a - -b ≃ b - a
x✝ : -b < -a
this : Positive (-a - -b)
⊢ Positive (b - a)