internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Integer.gt_iff_pos_diff
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
k : ℕ
left✝ : Positive k
right✝ : a - b ≃ coe k
⊢ b ≤ a ∧ b ≄ a
Tactic:
have : a ≃ b + coe k := subR_moveR_addL.mp ‹a - b ≃ coe k›
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
k : ℕ
left✝ : Positive k
right✝ : a - b ≃ coe k
this : a ≃ b + coe k
⊢ b ≤ a ∧ b ≄ a
Theorem: Lean4Axiomatic.Integer.gt_iff_pos_diff
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
k : ℕ
left✝ : Positive k
right✝ : a - b ≃ coe k
this : a ≃ b + coe k
⊢ b ≤ a ∧ b ≄ a
Tactic:
have : b ≤ a := le_iff_add_nat.mpr (Exists.intro k ‹a ≃ b + coe k›)
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
k : ℕ
left✝ : Positive k
right✝ : a - b ≃ coe k
this✝ : a ≃ b + coe k
this : b ≤ a
⊢ b ≤ a ∧ b ≄ a
Theorem: Lean4Axiomatic.Integer.gt_iff_pos_diff
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
k : ℕ
left✝ : Positive k
right✝ : a - b ≃ coe k
this✝ : a ≃ b + coe k
this : b ≤ a
⊢ b ≤ a ∧ b ≄ a
Tactic:
have : k ≄ 0 := Signed.positive_defn.mp ‹Positive k›
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
k : ℕ
left✝ : Positive k
right✝ : a - b ≃ coe k
this✝¹ : a ≃ b + coe k
this✝ : b ≤ a
this : k ≄ 0
⊢ b ≤ a ∧ b ≄ a
Theorem: Lean4Axiomatic.Integer.gt_iff_pos_diff
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
k : ℕ
left✝ : Positive k
right✝ : a - b ≃ coe k
this✝¹ : a ≃ b + coe k
this✝ : b ≤ a
this : k ≄ 0
⊢ b ≤ a ∧ b ≄ a
Tactic:
have : (k:ℤ) ≄ ((0:ℕ):ℤ) := AA.subst₁ ‹k ≄ 0›
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
k : ℕ
left✝ : Positive k
right✝ : a - b ≃ coe k
this✝² : a ≃ b + coe k
this✝¹ : b ≤ a
this✝ : k ≄ 0
this : coe k ≄ coe 0
⊢ b ≤ a ∧ b ≄ a
Theorem: Lean4Axiomatic.Integer.gt_iff_pos_diff
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
k : ℕ
left✝ : Positive k
right✝ : a - b ≃ coe k
this✝² : a ≃ b + coe k
this✝¹ : b ≤ a
this✝ : k ≄ 0
this : coe k ≄ coe 0
⊢ b ≤ a ∧ b ≄ a
Tactic:
have : a - b ≄ 0 :=
  AA.neqv_substL (Rel.symm ‹a - b ≃ coe k›) ‹(coe k : ℤ) ≄ 0›
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
k : ℕ
left✝ : Positive k
right✝ : a - b ≃ coe k
this✝³ : a ≃ b + coe k
this✝² : b ≤ a
this✝¹ : k ≄ 0
this✝ : coe k ≄ coe 0
this : a - b ≄ 0
⊢ b ≤ a ∧ b ≄ a
Theorem: Lean4Axiomatic.Integer.gt_iff_pos_diff
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
k : ℕ
left✝ : Positive k
right✝ : a - b ≃ coe k
this✝³ : a ≃ b + coe k
this✝² : b ≤ a
this✝¹ : k ≄ 0
this✝ : coe k ≄ coe 0
this : a - b ≄ 0
⊢ b ≤ a ∧ b ≄ a
Tactic:
have : b ≄ a := Rel.symm (mt zero_diff_iff_eqv.mpr ‹a - b ≄ 0›)
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
k : ℕ
left✝ : Positive k
right✝ : a - b ≃ coe k
this✝⁴ : a ≃ b + coe k
this✝³ : b ≤ a
this✝² : k ≄ 0
this✝¹ : coe k ≄ coe 0
this✝ : a - b ≄ 0
this : b ≄ a
⊢ b ≤ a ∧ b ≄ a
Theorem: Lean4Axiomatic.Integer.gt_iff_pos_diff
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
k : ℕ
left✝ : Positive k
right✝ : a - b ≃ coe k
this✝⁴ : a ≃ b + coe k
this✝³ : b ≤ a
this✝² : k ≄ 0
this✝¹ : coe k ≄ coe 0
this✝ : a - b ≄ 0
this : b ≄ a
⊢ b ≤ a ∧ b ≄ a
Tactic:
exact And.intro ‹b ≤ a› ‹b ≄ a›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.lt_iff_neg_diff
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 ↔ Negative (a - b)
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 → Negative (a - b)

case mpr
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
⊢ Negative (a - b) → a < b
Theorem: Lean4Axiomatic.Integer.lt_iff_neg_diff
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 → Negative (a - b)
Tactic:
case mp =>
  intro (_ : a < b)
  show Negative (a - b)
  have : Positive (b - a) := gt_iff_pos_diff.mp ‹a < b›
  have : Positive (-(a - b)) :=
    AA.substFn (Rel.symm sub_neg_flip) ‹Positive (b - a)›
  have : Negative (a - b) :=
    negative_iff_negated_positive.mpr ‹Positive (-(a - b))›
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.lt_iff_neg_diff
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
⊢ Negative (a - b) → a < b
Tactic:
case mpr =>
  intro (_ : Negative (a - b))
  show a < b
  have : Negative (-(b - a)) :=
    AA.substFn (Rel.symm sub_neg_flip) ‹Negative (a - b)›
  have : Positive (b - a) :=
    positive_iff_negated_negative.mpr ‹Negative (-(b - a))›
  have : a < b := gt_iff_pos_diff.mpr ‹Positive (b - a)›
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.lt_iff_neg_diff
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 → Negative (a - b)
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
⊢ Negative (a - b)
Theorem: Lean4Axiomatic.Integer.lt_iff_neg_diff
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
⊢ Negative (a - b)
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 : ℤ
x✝ : a < b
this : Positive (b - a)
⊢ Negative (a - b)
Theorem: Lean4Axiomatic.Integer.lt_iff_neg_diff
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 (b - a)
⊢ Negative (a - b)
Tactic:
have : Positive (-(a - b)) :=
  AA.substFn (Rel.symm sub_neg_flip) ‹Positive (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✝ : a < b
this✝ : Positive (b - a)
this : Positive (-(a - b))
⊢ Negative (a - b)
Theorem: Lean4Axiomatic.Integer.lt_iff_neg_diff
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 (b - a)
this : Positive (-(a - b))
⊢ Negative (a - b)
Tactic:
have : Negative (a - b) :=
  negative_iff_negated_positive.mpr ‹Positive (-(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 (b - a)
this✝ : Positive (-(a - b))
this : Negative (a - b)
⊢ Negative (a - b)
Theorem: Lean4Axiomatic.Integer.lt_iff_neg_diff
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 (b - a)
this✝ : Positive (-(a - b))
this : Negative (a - b)
⊢ Negative (a - b)
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.lt_iff_neg_diff
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
⊢ Negative (a - b) → a < b
Tactic:
intro (_ : Negative (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✝ : Negative (a - b)
⊢ a < b
Theorem: Lean4Axiomatic.Integer.lt_iff_neg_diff
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Negative (a - b)
⊢ a < b
Tactic:
have : Negative (-(b - a)) :=
  AA.substFn (Rel.symm sub_neg_flip) ‹Negative (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✝ : Negative (a - b)
this : Negative (-(b - a))
⊢ a < b
Theorem: Lean4Axiomatic.Integer.lt_iff_neg_diff
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Negative (a - b)
this : Negative (-(b - a))
⊢ a < b
Tactic:
have : Positive (b - a) :=
  positive_iff_negated_negative.mpr ‹Negative (-(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✝ : Negative (a - b)
this✝ : Negative (-(b - a))
this : Positive (b - a)
⊢ a < b
Theorem: Lean4Axiomatic.Integer.lt_iff_neg_diff
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Negative (a - b)
this✝ : Negative (-(b - a))
this : Positive (b - a)
⊢ a < b
Tactic:
have : a < b := gt_iff_pos_diff.mpr ‹Positive (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✝ : Negative (a - b)
this✝¹ : Negative (-(b - a))
this✝ : Positive (b - a)
this : a < b
⊢ a < b
Theorem: Lean4Axiomatic.Integer.lt_iff_neg_diff
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Negative (a - b)
this✝¹ : Negative (-(b - a))
this✝ : Positive (b - a)
this : a < b
⊢ a < b
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.le_substL_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 : ℤ
⊢ a₁ ≃ a₂ → a₁ ≤ b → a₂ ≤ b
Tactic:
intro (_ : 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₁ a₂ b : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : a₁ ≤ b
⊢ a₂ ≤ b
Theorem: Lean4Axiomatic.Integer.le_substL_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✝ : a₁ ≤ b
⊢ a₂ ≤ b
Tactic:
have (Exists.intro (k : ℕ) (_ : b ≃ a₁ + coe k)) :=
  le_iff_add_nat.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₁ a₂ b : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : a₁ ≤ b
k : ℕ
h✝ : b ≃ a₁ + coe k
⊢ a₂ ≤ b
Theorem: Lean4Axiomatic.Integer.le_substL_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✝ : a₁ ≤ b
k : ℕ
h✝ : b ≃ a₁ + coe k
⊢ a₂ ≤ b
Tactic:
apply le_iff_add_nat.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✝ : a₁ ≤ b
k : ℕ
h✝ : b ≃ a₁ + coe k
⊢ ∃ k, b ≃ a₂ + coe k
Theorem: Lean4Axiomatic.Integer.le_substL_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✝ : a₁ ≤ b
k : ℕ
h✝ : b ≃ a₁ + coe k
⊢ ∃ k, b ≃ a₂ + coe k
Tactic:
have : b ≃ a₂ + coe k := Rel.trans ‹b ≃ a₁ + coe k› (AA.substL ‹a₁ ≃ 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✝ : a₁ ≤ b
k : ℕ
h✝ : b ≃ a₁ + coe k
this : b ≃ a₂ + coe k
⊢ ∃ k, b ≃ a₂ + coe k
Theorem: Lean4Axiomatic.Integer.le_substL_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✝ : a₁ ≤ b
k : ℕ
h✝ : b ≃ a₁ + coe k
this : b ≃ a₂ + coe k
⊢ ∃ k, b ≃ a₂ + coe k
Tactic:
exact Exists.intro k ‹b ≃ a₂ + coe k›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.le_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 : ℤ
⊢ a₁ ≃ a₂ → b ≤ a₁ → b ≤ a₂
Tactic:
intro (_ : 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₁
⊢ b ≤ a₂
Theorem: Lean4Axiomatic.Integer.le_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₁
⊢ b ≤ a₂
Tactic:
have (Exists.intro (k : ℕ) (_ : a₁ ≃ b + coe k)) :=
  le_iff_add_nat.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₁ a₂ b : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : b ≤ a₁
k : ℕ
h✝ : a₁ ≃ b + coe k
⊢ b ≤ a₂
Theorem: Lean4Axiomatic.Integer.le_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₁
k : ℕ
h✝ : a₁ ≃ b + coe k
⊢ b ≤ a₂
Tactic:
apply le_iff_add_nat.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₁
k : ℕ
h✝ : a₁ ≃ b + coe k
⊢ ∃ k, a₂ ≃ b + coe k
Theorem: Lean4Axiomatic.Integer.le_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₁
k : ℕ
h✝ : a₁ ≃ b + coe k
⊢ ∃ k, a₂ ≃ b + coe k
Tactic:
have : a₂ ≃ b + coe k := Rel.trans (Rel.symm ‹a₁ ≃ a₂›) ‹a₁ ≃ b + coe k›
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₁
k : ℕ
h✝ : a₁ ≃ b + coe k
this : a₂ ≃ b + coe k
⊢ ∃ k, a₂ ≃ b + coe k
Theorem: Lean4Axiomatic.Integer.le_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₁
k : ℕ
h✝ : a₁ ≃ b + coe k
this : a₂ ≃ b + coe k
⊢ ∃ k, a₂ ≃ b + coe k
Tactic:
exact Exists.intro k ‹a₂ ≃ b + coe k›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.lt_substL_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 : ℤ
⊢ a₁ ≃ a₂ → a₁ < b → a₂ < b
Tactic:
intro (_ : 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₁ a₂ b : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : a₁ < b
⊢ a₂ < b
Theorem: Lean4Axiomatic.Integer.lt_substL_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✝ : a₁ < b
⊢ a₂ < b
Tactic:
have (And.intro (_ : a₁ ≤ b) (_ : a₁ ≄ b)) := lt_iff_le_neqv.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₁ a₂ b : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : a₁ < b
left✝ : a₁ ≤ b
right✝ : a₁ ≄ b
⊢ a₂ < b
Theorem: Lean4Axiomatic.Integer.lt_substL_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✝ : a₁ < b
left✝ : a₁ ≤ b
right✝ : a₁ ≄ b
⊢ a₂ < b
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✝ : a₁ < b
left✝ : a₁ ≤ b
right✝ : a₁ ≄ b
⊢ a₂ ≤ b ∧ a₂ ≄ b
Theorem: Lean4Axiomatic.Integer.lt_substL_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✝ : a₁ < b
left✝ : a₁ ≤ b
right✝ : a₁ ≄ b
⊢ a₂ ≤ b ∧ a₂ ≄ b
Tactic:
have : a₂ ≤ b := AA.substLFn ‹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₁ a₂ b : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : a₁ < b
left✝ : a₁ ≤ b
right✝ : a₁ ≄ b
this : a₂ ≤ b
⊢ a₂ ≤ b ∧ a₂ ≄ b
Theorem: Lean4Axiomatic.Integer.lt_substL_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✝ : a₁ < b
left✝ : a₁ ≤ b
right✝ : a₁ ≄ b
this : a₂ ≤ b
⊢ a₂ ≤ b ∧ a₂ ≄ b
Tactic:
have : a₂ ≄ b := AA.neqv_substL ‹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₁ a₂ b : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : a₁ < b
left✝ : a₁ ≤ b
right✝ : a₁ ≄ b
this✝ : a₂ ≤ b
this : a₂ ≄ b
⊢ a₂ ≤ b ∧ a₂ ≄ b
Theorem: Lean4Axiomatic.Integer.lt_substL_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✝ : a₁ < b
left✝ : a₁ ≤ b
right✝ : a₁ ≄ b
this✝ : a₂ ≤ b
this : a₂ ≄ b
⊢ a₂ ≤ b ∧ a₂ ≄ b
Tactic:
exact And.intro ‹a₂ ≤ b› ‹a₂ ≄ b›
Proof state after:
no goals
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 : ℤ
⊢ a₁ ≃ a₂ → b < a₁ → b < a₂
Tactic:
intro (_ : 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₁
⊢ 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₁
⊢ b < a₂
Tactic:
have (And.intro (_ : b ≤ a₁) (_ : b ≄ a₁)) := lt_iff_le_neqv.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₁ a₂ b : ℤ
x✝¹ : a₁ ≃ a₂
x✝ : b < a₁
left✝ : b ≤ a₁
right✝ : b ≄ a₁
⊢ b < a₂