Theorem: Pos.mul_lt_mul_of_lt_of_lt (Extra/Pos/Lemmas.lean)

State before:
x₁ y₁ x₂ y₂ : Pos
⊢ x₁ < y₁ → x₂ < y₂ → x₁ * x₂ < y₁ * y₂
Tactic:
by_toNat
State after:
x₁ y₁ x₂ y₂ : Pos
⊢ y₁.toNat > x₁.toNat → y₂.toNat > x₂.toNat → y₁.toNat * y₂.toNat > x₁.toNat * x₂.toNat

State before:
x₁ y₁ x₂ y₂ : Pos
⊢ y₁.toNat > x₁.toNat → y₂.toNat > x₂.toNat → y₁.toNat * y₂.toNat > x₁.toNat * x₂.toNat
Tactic:
exact Nat.mul_lt_mul_of_lt_of_lt
State after:
no goals