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

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
⊢ x * y ≤ b * x + a * y - a * b → x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
intro h
State after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
have h₁ : (x - a) * (y - b) ≤ 0 := by linarith
State after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
exact
  match lt_trichotomy (x - a) 0, lt_trichotomy (y - b) 0 with
  | Or.inl xaNeg,           Or.inl ybNeg           => by nlinarith
  | Or.inl xaNeg,           Or.inr (Or.inl ybZero) => by
    have xaNeg' := le_of_lt xaNeg
    simp at xaNeg'
    have ybZero' := ge_of_eq ybZero
    simp at ybZero'
    exact Or.inl (And.intro xaNeg' ybZero')
  | Or.inl xaNeg,           Or.inr (Or.inr ybPos)  => by
    have xaNeg' := le_of_lt xaNeg
    simp at xaNeg'
    have ybPos' := le_of_lt ybPos
    simp at ybPos'
    exact Or.inl (And.intro xaNeg' ybPos')
  | Or.inr (Or.inl xaZero), Or.inl ybNeg           => by
    have xaZero' := ge_of_eq xaZero
    simp at xaZero'
    have ybNeg' := le_of_lt ybNeg
    simp at ybNeg'
    exact Or.inr (And.intro xaZero' ybNeg')
  | Or.inr (Or.inl xaZero), Or.inr (Or.inl ybZero) => by
    have xaZero' := le_of_eq xaZero
    simp at xaZero'
    have ybZero' := ge_of_eq ybZero
    simp at ybZero'
    exact Or.inl (And.intro xaZero' ybZero')
  | Or.inr (Or.inl xaZero), Or.inr (Or.inr ybPos)  => by
    have xaZero' := le_of_eq xaZero
    simp at xaZero'
    have ybPos' := le_of_lt ybPos
    simp at ybPos'
    exact Or.inl (And.intro xaZero' ybPos')
  | Or.inr (Or.inr xaPos),  Or.inl ybNeg           => by
    have xaPos' := le_of_lt xaPos
    simp at xaPos'
    have ybNeg' := le_of_lt ybNeg
    simp at ybNeg'
    exact Or.inr (And.intro xaPos' ybNeg')
  | Or.inr (Or.inr xaPos),  Or.inr (Or.inl ybZero) => by
    have xaPos' := le_of_lt xaPos
    simp at xaPos'
    have ybZero' := le_of_eq ybZero
    simp at ybZero'
    exact Or.inr (And.intro xaPos' ybZero')
  | Or.inr (Or.inr xaPos),  Or.inr (Or.inr ybPos)  => by nlinarith
State after:
no goals

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
⊢ (x - a) * (y - b) ≤ 0
Tactic:
linarith
State after:
no goals

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaNeg : x - a < 0
ybNeg : y - b < 0
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
nlinarith
State after:
no goals

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaNeg : x - a < 0
ybZero : y - b = 0
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
have xaNeg' := le_of_lt xaNeg
State after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaNeg : x - a < 0
ybZero : y - b = 0
xaNeg' : x - a ≤ 0
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaNeg : x - a < 0
ybZero : y - b = 0
xaNeg' : x - a ≤ 0
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
simp at xaNeg'
State after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaNeg : x - a < 0
ybZero : y - b = 0
xaNeg' : x ≤ a
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaNeg : x - a < 0
ybZero : y - b = 0
xaNeg' : x ≤ a
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
have ybZero' := ge_of_eq ybZero
State after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaNeg : x - a < 0
ybZero : y - b = 0
xaNeg' : x ≤ a
ybZero' : y - b ≥ 0
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaNeg : x - a < 0
ybZero : y - b = 0
xaNeg' : x ≤ a
ybZero' : y - b ≥ 0
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
simp at ybZero'
State after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaNeg : x - a < 0
ybZero : y - b = 0
xaNeg' : x ≤ a
ybZero' : b ≤ y
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaNeg : x - a < 0
ybZero : y - b = 0
xaNeg' : x ≤ a
ybZero' : b ≤ y
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
exact Or.inl (And.intro xaNeg' ybZero')
State after:
no goals

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaNeg : x - a < 0
ybPos : 0 < y - b
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
have xaNeg' := le_of_lt xaNeg
State after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaNeg : x - a < 0
ybPos : 0 < y - b
xaNeg' : x - a ≤ 0
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaNeg : x - a < 0
ybPos : 0 < y - b
xaNeg' : x - a ≤ 0
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
simp at xaNeg'
State after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaNeg : x - a < 0
ybPos : 0 < y - b
xaNeg' : x ≤ a
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaNeg : x - a < 0
ybPos : 0 < y - b
xaNeg' : x ≤ a
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
have ybPos' := le_of_lt ybPos
State after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaNeg : x - a < 0
ybPos : 0 < y - b
xaNeg' : x ≤ a
ybPos' : 0 ≤ y - b
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaNeg : x - a < 0
ybPos : 0 < y - b
xaNeg' : x ≤ a
ybPos' : 0 ≤ y - b
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
simp at ybPos'
State after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaNeg : x - a < 0
ybPos : 0 < y - b
xaNeg' : x ≤ a
ybPos' : b ≤ y
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaNeg : x - a < 0
ybPos : 0 < y - b
xaNeg' : x ≤ a
ybPos' : b ≤ y
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
exact Or.inl (And.intro xaNeg' ybPos')
State after:
no goals

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaZero : x - a = 0
ybNeg : y - b < 0
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
have xaZero' := ge_of_eq xaZero
State after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaZero : x - a = 0
ybNeg : y - b < 0
xaZero' : x - a ≥ 0
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaZero : x - a = 0
ybNeg : y - b < 0
xaZero' : x - a ≥ 0
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
simp at xaZero'
State after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaZero : x - a = 0
ybNeg : y - b < 0
xaZero' : a ≤ x
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaZero : x - a = 0
ybNeg : y - b < 0
xaZero' : a ≤ x
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
have ybNeg' := le_of_lt ybNeg
State after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaZero : x - a = 0
ybNeg : y - b < 0
xaZero' : a ≤ x
ybNeg' : y - b ≤ 0
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaZero : x - a = 0
ybNeg : y - b < 0
xaZero' : a ≤ x
ybNeg' : y - b ≤ 0
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
simp at ybNeg'
State after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaZero : x - a = 0
ybNeg : y - b < 0
xaZero' : a ≤ x
ybNeg' : y ≤ b
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaZero : x - a = 0
ybNeg : y - b < 0
xaZero' : a ≤ x
ybNeg' : y ≤ b
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
exact Or.inr (And.intro xaZero' ybNeg')
State after:
no goals

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaZero : x - a = 0
ybZero : y - b = 0
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
have xaZero' := le_of_eq xaZero
State after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaZero : x - a = 0
ybZero : y - b = 0
xaZero' : x - a ≤ 0
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaZero : x - a = 0
ybZero : y - b = 0
xaZero' : x - a ≤ 0
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
simp at xaZero'
State after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaZero : x - a = 0
ybZero : y - b = 0
xaZero' : x ≤ a
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaZero : x - a = 0
ybZero : y - b = 0
xaZero' : x ≤ a
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
have ybZero' := ge_of_eq ybZero
State after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaZero : x - a = 0
ybZero : y - b = 0
xaZero' : x ≤ a
ybZero' : y - b ≥ 0
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaZero : x - a = 0
ybZero : y - b = 0
xaZero' : x ≤ a
ybZero' : y - b ≥ 0
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
simp at ybZero'
State after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaZero : x - a = 0
ybZero : y - b = 0
xaZero' : x ≤ a
ybZero' : b ≤ y
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaZero : x - a = 0
ybZero : y - b = 0
xaZero' : x ≤ a
ybZero' : b ≤ y
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
exact Or.inl (And.intro xaZero' ybZero')
State after:
no goals

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaZero : x - a = 0
ybPos : 0 < y - b
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
have xaZero' := le_of_eq xaZero
State after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaZero : x - a = 0
ybPos : 0 < y - b
xaZero' : x - a ≤ 0
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaZero : x - a = 0
ybPos : 0 < y - b
xaZero' : x - a ≤ 0
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
simp at xaZero'
State after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaZero : x - a = 0
ybPos : 0 < y - b
xaZero' : x ≤ a
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaZero : x - a = 0
ybPos : 0 < y - b
xaZero' : x ≤ a
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
have ybPos' := le_of_lt ybPos
State after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaZero : x - a = 0
ybPos : 0 < y - b
xaZero' : x ≤ a
ybPos' : 0 ≤ y - b
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaZero : x - a = 0
ybPos : 0 < y - b
xaZero' : x ≤ a
ybPos' : 0 ≤ y - b
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
simp at ybPos'
State after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaZero : x - a = 0
ybPos : 0 < y - b
xaZero' : x ≤ a
ybPos' : b ≤ y
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaZero : x - a = 0
ybPos : 0 < y - b
xaZero' : x ≤ a
ybPos' : b ≤ y
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
exact Or.inl (And.intro xaZero' ybPos')
State after:
no goals

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaPos : 0 < x - a
ybNeg : y - b < 0
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
have xaPos' := le_of_lt xaPos
State after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaPos : 0 < x - a
ybNeg : y - b < 0
xaPos' : 0 ≤ x - a
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaPos : 0 < x - a
ybNeg : y - b < 0
xaPos' : 0 ≤ x - a
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
simp at xaPos'
State after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaPos : 0 < x - a
ybNeg : y - b < 0
xaPos' : a ≤ x
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaPos : 0 < x - a
ybNeg : y - b < 0
xaPos' : a ≤ x
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
have ybNeg' := le_of_lt ybNeg
State after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaPos : 0 < x - a
ybNeg : y - b < 0
xaPos' : a ≤ x
ybNeg' : y - b ≤ 0
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaPos : 0 < x - a
ybNeg : y - b < 0
xaPos' : a ≤ x
ybNeg' : y - b ≤ 0
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
simp at ybNeg'
State after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaPos : 0 < x - a
ybNeg : y - b < 0
xaPos' : a ≤ x
ybNeg' : y ≤ b
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaPos : 0 < x - a
ybNeg : y - b < 0
xaPos' : a ≤ x
ybNeg' : y ≤ b
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
exact Or.inr (And.intro xaPos' ybNeg')
State after:
no goals

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaPos : 0 < x - a
ybZero : y - b = 0
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
have xaPos' := le_of_lt xaPos
State after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaPos : 0 < x - a
ybZero : y - b = 0
xaPos' : 0 ≤ x - a
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaPos : 0 < x - a
ybZero : y - b = 0
xaPos' : 0 ≤ x - a
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
simp at xaPos'
State after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaPos : 0 < x - a
ybZero : y - b = 0
xaPos' : a ≤ x
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaPos : 0 < x - a
ybZero : y - b = 0
xaPos' : a ≤ x
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
have ybZero' := le_of_eq ybZero
State after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaPos : 0 < x - a
ybZero : y - b = 0
xaPos' : a ≤ x
ybZero' : y - b ≤ 0
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaPos : 0 < x - a
ybZero : y - b = 0
xaPos' : a ≤ x
ybZero' : y - b ≤ 0
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
simp at ybZero'
State after:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaPos : 0 < x - a
ybZero : y - b = 0
xaPos' : a ≤ x
ybZero' : y ≤ b
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaPos : 0 < x - a
ybZero : y - b = 0
xaPos' : a ≤ x
ybZero' : y ≤ b
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
exact Or.inr (And.intro xaPos' ybZero')
State after:
no goals

State before:
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaPos : 0 < x - a
ybPos : 0 < y - b
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
Tactic:
nlinarith
State after:
no goals