Theorem: Smt.Reconstruct.Int.combine_signs₃ (Smt/Reconstruct/Int/Lemmas.lean)

State before:
a b c d : Int
⊢ a < 0 → b > 0 → b * a < 0
Tactic:
intros h₁ h₂
State after:
a b c d : Int
h₁ : a < 0
h₂ : b > 0
⊢ b * a < 0

State before:
a b c d : Int
h₁ : a < 0
h₂ : b > 0
⊢ b * a < 0
Tactic:
have h := Int.mul_lt_mul_of_pos_left h₁ h₂
State after:
a b c d : Int
h₁ : a < 0
h₂ : b > 0
h : b * a < b * 0
⊢ b * a < 0

State before:
a b c d : Int
h₁ : a < 0
h₂ : b > 0
h : b * a < b * 0
⊢ b * a < 0
Tactic:
simp at h
State after:
a b c d : Int
h₁ : a < 0
h₂ : b > 0
h : b * a < 0
⊢ b * a < 0

State before:
a b c d : Int
h₁ : a < 0
h₂ : b > 0
h : b * a < 0
⊢ b * a < 0
Tactic:
exact h
State after:
no goals