Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus.
On Mac, use
Cmd instead of
Ctrl .
/-
Copyright (c) 2020 Robert Y. Lewis. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Robert Y. Lewis
Ported by: Scott Morrison
-/
import Std.Tactic.Simpa
import Std.Tactic.Lint.Basic
import Mathlib.Algebra.Order.Ring.Defs
import Mathlib.Algebra.Order.Monoid.Lemmas
import Mathlib.Init.Data.Int.Order
import Mathlib.Algebra.Order.ZeroLEOne
import Mathlib.Algebra.GroupPower.Order
/-!
# Lemmas for `linarith`.
Those in the `Linarith` namespace should stay here.
Those outside the `Linarith` namespace may be deleted as they are ported to mathlib4.
-/
namespace Linarith
theorem lt_irrefl { α : Type u } [ Preorder α ] { a : α } : ¬ a < a := _root_.lt_irrefl : ∀ {α : Type ?u.29} [inst : Preorder α a : α ), ¬ a < a a
theorem eq_of_eq_of_eq { α } [ OrderedSemiring : Type ?u.43 → Type ?u.43 α ] { a b : α } ( ha : a = 0 ) ( hb : b = 0 ) : a + b = 0 := by
simp [*]
theorem le_of_eq_of_le { α } [ OrderedSemiring : Type ?u.816 → Type ?u.816 α ] { a b : α } ( ha : a = 0 ) ( hb : b ≤ 0 ) : a + b ≤ 0 := by
simp [*]
theorem lt_of_eq_of_lt { α } [ OrderedSemiring : Type ?u.1901 → Type ?u.1901 α ] { a b : α } ( ha : a = 0 ) ( hb : b < 0 ) : a + b < 0 := by
simp [*]
theorem le_of_le_of_eq { α } [ OrderedSemiring : Type ?u.2951 → Type ?u.2951 α ] { a b : α } ( ha : a ≤ 0 ) ( hb : b = 0 ) : a + b ≤ 0 := by
simp [*]
theorem lt_of_lt_of_eq { α } [ OrderedSemiring : Type ?u.4032 → Type ?u.4032 α ] { a b : α } ( ha : a < 0 ) ( hb : b = 0 ) : a + b < 0 := by
simp [*]
theorem mul_neg { α } [ StrictOrderedRing : Type ?u.5078 → Type ?u.5078 α ] { a b : α } ( ha : a < 0 ) ( hb : 0 < b ) : b * a < 0 :=
have : (- b )* a > 0 := mul_pos_of_neg_of_neg ( neg_neg_of_pos hb ) ha
neg_of_neg_pos : ∀ {α : Type ?u.5848} [inst : AddGroup α inst_1 : LT α inst_2 : CovariantClass α α (fun x x_1 => x + x_1 ) fun x x_1 => x < x_1 a : α }, 0 < - a a < 0 ( by simpa )
theorem mul_nonpos { α } [ OrderedRing : Type ?u.7170 → Type ?u.7170 α ] { a b : α } ( ha : a ≤ 0 ) ( hb : 0 < b ) : b * a ≤ 0 :=
have : (- b )* a ≥ 0 := mul_nonneg_of_nonpos_of_nonpos : ∀ {α : Type ?u.8113} [inst : OrderedRing α a b : α }, a ≤ 0 b ≤ 0 0 ≤ a * b ( le_of_lt : ∀ {α : Type ?u.8155} [inst : Preorder α a b : α }, a < b a ≤ b ( neg_neg_of_pos hb )) ha
by simpa
-- used alongside `mul_neg` and `mul_nonpos`, so has the same argument pattern for uniformity
@[ nolint unusedArguments ]
theorem mul_eq { α } [ OrderedSemiring : Type ?u.9535 → Type ?u.9535 α ] { a b : α } ( ha : a = 0 ) ( _ : 0 < b ) : b * a = 0 := by
simp [*]
lemma eq_of_not_lt_of_not_gt { α } [ LinearOrder : Type ?u.10394 → Type ?u.10394 α ] ( a b : α ) ( h1 : ¬ a < b ) ( h2 : ¬ b < a ) : a = b :=
le_antisymm ( le_of_not_gt h2 ) ( le_of_not_gt h1 )
-- used in the `nlinarith` normalization steps. The `_` argument is for uniformity.
@[ nolint unusedArguments ]
lemma mul_zero_eq : ∀ {α : Type u_1} {R : α → α → Prop inst : Semiring α a b : α }, R a 0 b = 0 a * b = 0 mul_zero_eq { α } { R : α → α → Prop } [ Semiring α ] { a b : α } ( _ : R a 0 ) ( h : b = 0 ) :
a * b = 0 :=
by simp [ h ]
-- used in the `nlinarith` normalization steps. The `_` argument is for uniformity.
@[ nolint unusedArguments ]
lemma zero_mul_eq : ∀ {α : Type u_1} {R : α → α → Prop inst : Semiring α a b : α }, a = 0 R b 0 a * b = 0 zero_mul_eq { α } { R : α → α → Prop } [ Semiring α ] { a b : α } ( h : a = 0 ) ( _ : R b 0 ) :
a * b = 0 :=
by simp [ h ]
end Linarith
section
open Function
-- These lemmas can be removed when their originals are ported.
theorem lt_zero_of_zero_gt : ∀ {α : Type u_1} [inst : Zero α inst_1 : LT α a : α }, 0 > a a < 0 lt_zero_of_zero_gt [ Zero α ] [ LT α ] { a : α } ( h : 0 > a ) : a < 0 := h
theorem le_zero_of_zero_ge : ∀ {α : Type u_1} [inst : Zero α inst_1 : LE α a : α }, 0 ≥ a a ≤ 0 le_zero_of_zero_ge [ Zero α ] [ LE α ] { a : α } ( h : 0 ≥ a ) : a ≤ 0 := h