Theorem: Lean4Axiomatic.Integer.add_cancelL_lt (Lean4Axiomatic/Integer/Order.lean)

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b c : ℤ
⊢ c + a < c + b → a < b
Tactic:
intro (_ : c + a < c + b)
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

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›
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

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
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)

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
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)

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›
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))

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))›
State after:
no goals