Lemmas for the linear_combination tactic

These should not be used directly in user code.

Addition

theorem Mathlib.Tactic.LinearCombination.add_eq_eq {α : Type u_1} {a₁ a₂ b₁ b₂ : α} [Add α] (p₁ : a₁ = b₁) (p₂ : a₂ = b₂) : a₁ + a₂ = b₁ + b₂

theorem Mathlib.Tactic.LinearCombination.add_le_eq {α : Type u_1} {a₁ a₂ b₁ b₂ : α} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] (p₁ : a₁ ≤ b₁) (p₂ : a₂ = b₂) : a₁ + a₂ ≤ b₁ + b₂

theorem Mathlib.Tactic.LinearCombination.add_eq_le {α : Type u_1} {a₁ a₂ b₁ b₂ : α} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] (p₁ : a₁ = b₁) (p₂ : a₂ ≤ b₂) : a₁ + a₂ ≤ b₁ + b₂

theorem Mathlib.Tactic.LinearCombination.add_lt_eq {α : Type u_1} {a₁ a₂ b₁ b₂ : α} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] (p₁ : a₁ < b₁) (p₂ : a₂ = b₂) : a₁ + a₂ < b₁ + b₂

theorem Mathlib.Tactic.LinearCombination.add_eq_lt {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {a₁ b₁ a₂ b₂ : α} (p₁ : a₁ = b₁) (p₂ : a₂ < b₂) : a₁ + a₂ < b₁ + b₂

Multiplication

theorem Mathlib.Tactic.LinearCombination.mul_eq_const {α : Type u_1} {a b : α} [Mul α] (p : a = b) (c : α) : a * c = b * c

theorem Mathlib.Tactic.LinearCombination.mul_le_const {α : Type u_1} {b c : α} [Semiring α] [PartialOrder α] [IsOrderedRing α] (p : b ≤ c) {a : α} (ha : 0 ≤ a) : b * a ≤ c * a

theorem Mathlib.Tactic.LinearCombination.mul_lt_const {α : Type u_1} {b c : α} [Semiring α] [PartialOrder α] [IsStrictOrderedRing α] (p : b < c) {a : α} (ha : 0 < a) : b * a < c * a

theorem Mathlib.Tactic.LinearCombination.mul_lt_const_weak {α : Type u_1} {b c : α} [Semiring α] [PartialOrder α] [IsOrderedRing α] (p : b < c) {a : α} (ha : 0 ≤ a) : b * a ≤ c * a

theorem Mathlib.Tactic.LinearCombination.mul_const_eq {α : Type u_1} {b c : α} [Mul α] (p : b = c) (a : α) : a * b = a * c

theorem Mathlib.Tactic.LinearCombination.mul_const_le {α : Type u_1} {b c : α} [Semiring α] [PartialOrder α] [IsOrderedRing α] (p : b ≤ c) {a : α} (ha : 0 ≤ a) : a * b ≤ a * c

theorem Mathlib.Tactic.LinearCombination.mul_const_lt {α : Type u_1} {b c : α} [Semiring α] [PartialOrder α] [IsStrictOrderedRing α] (p : b < c) {a : α} (ha : 0 < a) : a * b < a * c

theorem Mathlib.Tactic.LinearCombination.mul_const_lt_weak {α : Type u_1} {b c : α} [Semiring α] [PartialOrder α] [IsOrderedRing α] (p : b < c) {a : α} (ha : 0 ≤ a) : a * b ≤ a * c

Scalar multiplication

theorem Mathlib.Tactic.LinearCombination.smul_eq_const {α : Type u_1} {K : Type u_2} {t s : K} [SMul K α] (p : t = s) (c : α) : t • c = s • c

theorem Mathlib.Tactic.LinearCombination.smul_le_const {α : Type u_1} {K : Type u_2} {t s : K} [Ring K] [PartialOrder K] [IsOrderedRing K] [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [Module K α] [OrderedSMul K α] (p : t ≤ s) {a : α} (ha : 0 ≤ a) : t • a ≤ s • a

theorem Mathlib.Tactic.LinearCombination.smul_lt_const {α : Type u_1} {K : Type u_2} {t s : K} [Ring K] [PartialOrder K] [IsOrderedRing K] [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [Module K α] [OrderedSMul K α] (p : t < s) {a : α} (ha : 0 < a) : t • a < s • a

theorem Mathlib.Tactic.LinearCombination.smul_lt_const_weak {α : Type u_1} {K : Type u_2} {t s : K} [Ring K] [PartialOrder K] [IsOrderedRing K] [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [Module K α] [OrderedSMul K α] (p : t < s) {a : α} (ha : 0 ≤ a) : t • a ≤ s • a

theorem Mathlib.Tactic.LinearCombination.smul_const_eq {α : Type u_1} {b c : α} {K : Type u_2} [SMul K α] (p : b = c) (s : K) : s • b = s • c

theorem Mathlib.Tactic.LinearCombination.smul_const_le {α : Type u_1} {b c : α} {K : Type u_2} [Semiring K] [PartialOrder K] [AddCommMonoid α] [PartialOrder α] [Module K α] [OrderedSMul K α] (p : b ≤ c) {s : K} (hs : 0 ≤ s) : s • b ≤ s • c

theorem Mathlib.Tactic.LinearCombination.smul_const_lt {α : Type u_1} {b c : α} {K : Type u_2} [Semiring K] [PartialOrder K] [AddCommMonoid α] [PartialOrder α] [Module K α] [OrderedSMul K α] (p : b < c) {s : K} (hs : 0 < s) : s • b < s • c

theorem Mathlib.Tactic.LinearCombination.smul_const_lt_weak {α : Type u_1} {b c : α} {K : Type u_2} [Semiring K] [PartialOrder K] [AddCommMonoid α] [PartialOrder α] [Module K α] [OrderedSMul K α] (p : b < c) {s : K} (hs : 0 ≤ s) : s • b ≤ s • c

Division

theorem Mathlib.Tactic.LinearCombination.div_eq_const {α : Type u_1} {a b : α} [Div α] (p : a = b) (c : α) : a / c = b / c

theorem Mathlib.Tactic.LinearCombination.div_le_const {α : Type u_1} {b c : α} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] (p : b ≤ c) {a : α} (ha : 0 ≤ a) : b / a ≤ c / a

theorem Mathlib.Tactic.LinearCombination.div_lt_const {α : Type u_1} {b c : α} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] (p : b < c) {a : α} (ha : 0 < a) : b / a < c / a

theorem Mathlib.Tactic.LinearCombination.div_lt_const_weak {α : Type u_1} {b c : α} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] (p : b < c) {a : α} (ha : 0 ≤ a) : b / a ≤ c / a

Lemmas constructing the reduction of a goal to a specified built-up hypothesis

theorem Mathlib.Tactic.LinearCombination.eq_of_eq {α : Type u_1} {a a' b b' : α} [Add α] [IsRightCancelAdd α] (p : a = b) (H : a' + b = b' + a) : a' = b'

theorem Mathlib.Tactic.LinearCombination.le_of_le {α : Type u_1} {a a' b b' : α} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] (p : a ≤ b) (H : a' + b ≤ b' + a) : a' ≤ b'

theorem Mathlib.Tactic.LinearCombination.le_of_eq {α : Type u_1} {a a' b b' : α} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] (p : a = b) (H : a' + b ≤ b' + a) : a' ≤ b'

theorem Mathlib.Tactic.LinearCombination.le_of_lt {α : Type u_1} {a a' b b' : α} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] (p : a < b) (H : a' + b ≤ b' + a) : a' ≤ b'

theorem Mathlib.Tactic.LinearCombination.lt_of_le {α : Type u_1} {a a' b b' : α} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] (p : a ≤ b) (H : a' + b < b' + a) : a' < b'

theorem Mathlib.Tactic.LinearCombination.lt_of_eq {α : Type u_1} {a a' b b' : α} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] (p : a = b) (H : a' + b < b' + a) : a' < b'

theorem Mathlib.Tactic.LinearCombination.lt_of_lt {α : Type u_1} {a a' b b' : α} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] (p : a < b) (H : a' + b ≤ b' + a) : a' < b'

theorem Mathlib.Tactic.LinearCombination.eq_rearrange {G : Type u_3} [AddGroup G] {a b : G} : a - b = 0 → a = b

Alias of the forward direction of sub_eq_zero.

theorem Mathlib.Tactic.LinearCombination.le_rearrange {α : Type u_3} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a b : α} (h : a - b ≤ 0) : a ≤ b

theorem Mathlib.Tactic.LinearCombination.lt_rearrange {α : Type u_3} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a b : α} (h : a - b < 0) : a < b

theorem Mathlib.Tactic.LinearCombination.eq_of_add_pow {α : Type u_1} {a a' b b' : α} [Ring α] [NoZeroDivisors α] (n : ℕ) (p : a = b) (H : (a' - b') ^ n - (a - b) = 0) : a' = b'

Lookup functions for lemmas by operation and relation(s)

def Mathlib.Ineq.addRelRelData : Ineq → Ineq → Lean.Name

Given two (in)equalities, look up the lemma to add them.

inductive Mathlib.Ineq.WithStrictness : Type

Finite inductive type extending Mathlib.Ineq: a type of inequality (eq, le or lt), together with, in the case of lt, a boolean, typically representing the strictness (< or ≤) of some other inequality.

• eq : Ineq.WithStrictness
• le : Ineq.WithStrictness
• lt (strict : Bool) : Ineq.WithStrictness

def Mathlib.Ineq.mulRelConstData : Ineq.WithStrictness → Lean.Name

Given an (in)equality, look up the lemma to left-multiply it by a constant. If relevant, also take into account the degree of positivity which can be proved of the constant: strict or non-strict.

def Mathlib.Ineq.mulConstRelData : Ineq.WithStrictness → Lean.Name

Given an (in)equality, look up the lemma to right-multiply it by a constant. If relevant, also take into account the degree of positivity which can be proved of the constant: strict or non-strict.

def Mathlib.Ineq.smulRelConstData : Ineq.WithStrictness → Lean.Name

Given an (in)equality, look up the lemma to left-scalar-multiply it by a constant (scalar). If relevant, also take into account the degree of positivity which can be proved of the constant: strict or non-strict.

def Mathlib.Ineq.smulConstRelData : Ineq.WithStrictness → Lean.Name

Given an (in)equality, look up the lemma to right-scalar-multiply it by a constant (vector). If relevant, also take into account the degree of positivity which can be proved of the constant: strict or non-strict.

def Mathlib.Ineq.divRelConstData : Ineq.WithStrictness → Lean.Name

Given an (in)equality, look up the lemma to divide it by a constant. If relevant, also take into account the degree of positivity which can be proved of the constant: strict or non-strict.

def Mathlib.Ineq.relImpRelData : Ineq → Ineq → Option (Lean.Name × Ineq)

Given two (in)equalities P and Q, look up the lemma to deduce Q from P, and the relation appearing in the side condition produced by this lemma.

def Mathlib.Ineq.rearrangeData : Ineq → Lean.Name

Given an (in)equality, look up the lemma to move everything to the LHS.