internlm/Lean-Github huggingface dataset:
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof 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'
Proof 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
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof 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')
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof 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
Proof 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
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof 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'
Proof 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
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof 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
Proof 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
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof 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'
Proof 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
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof 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')
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof 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
Proof 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
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof 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'
Proof 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
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof 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
Proof 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
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof 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'
Proof 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
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof 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')
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof 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
Proof 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
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof 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'
Proof 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
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof 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
Proof 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
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof 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'
Proof 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
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof 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')
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof 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
Proof 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
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof 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'
Proof 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
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof 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
Proof 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
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof 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'
Proof 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
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof 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')
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof 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
Proof 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
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof 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'
Proof 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
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof 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
Proof 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
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof 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'
Proof 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
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof 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')
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof 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
Proof 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
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof 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'
Proof 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
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof 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
Proof 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
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof 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'
Proof 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
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof 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')
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpLower
Proof 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
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.arithMulTangentMprLower
Proof 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
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.arithMulTangentMprLower
Proof 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
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof 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
Proof 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
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof 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
Proof 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
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof 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
    have xaNeg' := le_of_lt xaNeg
    simp at xaNeg'
    have ybNeg' := le_of_lt ybNeg
    simp at ybNeg'
    exact Or.inl (And.intro xaNeg' ybNeg')
  | Or.inl xaNeg,           Or.inr (Or.inl ybZero) => by
    have xaNeg' := le_of_lt xaNeg
    simp at xaNeg'
    have ybZero' := le_of_eq ybZero
    simp at ybZero'
    exact Or.inl (And.intro xaNeg' ybZero')
  | Or.inl xaNeg,           Or.inr (Or.inr ybPos)  => by nlinarith
  | Or.inr (Or.inl xaZero), Or.inl ybNeg           => by
    have xaZero' := le_of_eq xaZero
    simp at xaZero'
    have ybNeg' := le_of_lt ybNeg
    simp at ybNeg'
    exact Or.inl (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' := le_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' := ge_of_eq xaZero
    simp at xaZero'
    have ybPos' := le_of_lt ybPos
    simp at ybPos'
    exact Or.inr (And.intro xaZero' ybPos')
  | Or.inr (Or.inr xaPos),  Or.inl ybNeg           => by nlinarith
  | Or.inr (Or.inr xaPos),  Or.inr (Or.inl ybZero) => by
    have xaPos' := le_of_lt xaPos
    simp at xaPos'
    have ybZero' := ge_of_eq ybZero
    simp at ybZero'
    exact Or.inr (And.intro xaPos' ybZero')
  | Or.inr (Or.inr xaPos),  Or.inr (Or.inr ybPos)  => by
    have xaPos' := le_of_lt xaPos
    simp at xaPos'
    have ybPos' := le_of_lt ybPos
    simp at ybPos'
    exact Or.inr (And.intro xaPos' ybPos')
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof 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
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof 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:
have xaNeg' := le_of_lt xaNeg
Proof 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
ybNeg : y - b < 0
xaNeg' : x - a ≤ 0
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof 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
xaNeg' : x - a ≤ 0
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Tactic:
simp at xaNeg'
Proof 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
ybNeg : y - b < 0
xaNeg' : x ≤ a
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof 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
xaNeg' : x ≤ a
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Tactic:
have ybNeg' := le_of_lt ybNeg
Proof 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
ybNeg : y - b < 0
xaNeg' : x ≤ a
ybNeg' : y - b ≤ 0
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof 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
xaNeg' : x ≤ a
ybNeg' : y - b ≤ 0
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Tactic:
simp at ybNeg'
Proof 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
ybNeg : y - b < 0
xaNeg' : x ≤ a
ybNeg' : y ≤ b
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof 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
xaNeg' : x ≤ a
ybNeg' : y ≤ b
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Tactic:
exact Or.inl (And.intro xaNeg' ybNeg')
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof 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
Proof 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
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof 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'
Proof 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
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof 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' := le_of_eq ybZero
Proof 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
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof 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'
Proof 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
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Theorem: Smt.Reconstruct.Arith.arithMulTangentMpUpper
Proof 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
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
Tactic:
exact Or.inl (And.intro xaNeg' ybZero')
Proof state after:
no goals