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

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

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

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

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

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