Theorem: Smt.Reconstruct.Arith.combineSigns₂ (Smt/Reconstruct/Arith/ArithMulSign/Lemmas.lean)

State before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
⊢ a > 0 → b < 0 → b * a < 0
Tactic:
intros h₁ h₂
State after:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
h₁ : a > 0
h₂ : b < 0
⊢ b * a < 0

State before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
h₁ : a > 0
h₂ : b < 0
⊢ b * a < 0
Tactic:
have h := mul_lt_mul_of_pos_right h₂ h₁
State after:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
h₁ : a > 0
h₂ : b < 0
h : b * a < 0 * a
⊢ b * a < 0

State before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
h₁ : a > 0
h₂ : b < 0
h : b * a < 0 * a
⊢ b * a < 0
Tactic:
simp at h
State after:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
h₁ : a > 0
h₂ : b < 0
h : b * a < 0
⊢ b * a < 0

State before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
h₁ : a > 0
h₂ : b < 0
h : b * a < 0
⊢ b * a < 0
Tactic:
exact h
State after:
no goals