Theorem: Nat.lt_of_mul_lt_mul_left (Algdata/Init/Nat.lean)

State before:
a b c : Nat
⊢ a * b < a * c → b < c
Tactic:
intro h
State after:
a b c : Nat
h : a * b < a * c
⊢ b < c

State before:
a b c : Nat
h : a * b < a * c
⊢ b < c
Tactic:
apply Nat.lt_of_not_le
State after:
case a
a b c : Nat
h : a * b < a * c
⊢ ¬c ≤ b

State before:
case a
a b c : Nat
h : a * b < a * c
⊢ ¬c ≤ b
Tactic:
intro hcontra
State after:
case a
a b c : Nat
h : a * b < a * c
hcontra : c ≤ b
⊢ False

State before:
case a
a b c : Nat
h : a * b < a * c
hcontra : c ≤ b
⊢ False
Tactic:
have := Nat.mul_le_mul_left a hcontra
State after:
case a
a b c : Nat
h : a * b < a * c
hcontra : c ≤ b
this : a * c ≤ a * b
⊢ False

State before:
case a
a b c : Nat
h : a * b < a * c
hcontra : c ≤ b
this : a * c ≤ a * b
⊢ False
Tactic:
exact absurd h (Nat.not_lt_of_le this)
State after:
no goals