Theorem: Smt.Reconstruct.Arith.arithMulTangentMprLower (Smt/Reconstruct/Arith/TangentPlane/Theorems.lean)

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
h₁ : x ≤ a
h₂ : y ≥ b
⊢ x * y ≤ b * x + a * y - a * b
Tactic:
nlinarith
State after:
no goals

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
h₁ : x ≥ a
h₂ : y ≤ b
⊢ x * y ≤ b * x + a * y - a * b
Tactic:
nlinarith
State after:
no goals