Theorem: Lean4Axiomatic.Integer.mul_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 : ℤ
⊢ Positive c → c * a < c * b → a < b
Tactic:
intro (_ : Positive c) (_ : 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✝¹ : Positive 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✝¹ : 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›
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

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

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

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

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

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