ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p q : R[X]<VAR>hp : p.Monic<VAR>hq : q.Monic<VAR>h : q.natDegree ≠ 0<GOAL>(p.comp q).Monic
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p : R[X]<VAR>hp : p.Monic<VAR>r : R<GOAL>(p.comp (Polynomial.X + Polynomial.C r)).Monic
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p : R[X]<VAR>hp : p.Monic<VAR>r : R<GOAL>(p.comp (Polynomial.X - Polynomial.C r)).Monic
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>c : R[X]ˣ<VAR>p : R[X]<GOAL>(↑c).coeff 0 • p = ↑c * p
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p q : R[X]<GOAL>p.comp q = 0 ↔ p = 0 ∨ Polynomial.eval (q.coeff 0) p = 0 ∧ q = Polynomial.C (q.coeff 0)
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Nontrivial S<VAR>Semiring S<VAR>Algebra R S<VAR>p q : R[X]<VAR>h : IsCoprime p q<VAR>s : S<GOAL>(Polynomial.aeval s) p ≠ 0 ∨ (Polynomial.aeval s) q ≠ 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>a b : R<VAR>h : IsUnit (a - b)<GOAL>IsCoprime (Polynomial.X - Polynomial.C a) (Polynomial.X - Polynomial.C b)
<VAR>K : Type u_1<VAR>Field K<VAR>I : Type v<VAR>s : I → K<VAR>H : Function.Injective s<GOAL>Pairwise (IsCoprime on fun i => Polynomial.X - Polynomial.C (s i))
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>p q : R[X]<VAR>x : R<VAR>hpq : p * q ≠ 0<GOAL>Polynomial.rootMultiplicity x (p * q) = Polynomial.rootMultiplicity x p + Polynomial.rootMultiplicity x q
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>DecidableEq R<VAR>p : R[X]<GOAL>p ≠ 0 → ∃ s, ↑(Multiset.card s) ≤ p.degree ∧ ∀ (a : R), Multiset.count a s = Polynomial.rootMultiplicity a p
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>CommRing S<VAR>IsDomain S<VAR>φ : R →+* S<VAR>f : R[X]<VAR>hf : IsUnit f.leadingCoeff<VAR>H : IsUnit (Polynomial.map φ f)<GOAL>IsUnit f
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>IsDomain R<VAR>CommRing S<VAR>IsDomain S<VAR>φ : R →+* S<VAR>f : R[X]<VAR>h_mon : f.Monic<VAR>h_irr : Irreducible (Polynomial.map φ f)<GOAL>Irreducible f
<VAR>α : Type u_1<VAR>self : CanonicallyOrderedAddCommMonoid α<VAR>a b : α<GOAL>a ≤ b → ∃ c, b = a + c
<VAR>α : Type u_1<VAR>self : CanonicallyOrderedAddCommMonoid α<VAR>a b : α<GOAL>a ≤ a + b
<VAR>α : Type u_1<VAR>self : CanonicallyOrderedCommMonoid α<VAR>a b : α<GOAL>a ≤ a * b
<VAR>α : Type u_1<VAR>self : CanonicallyOrderedCommMonoid α<VAR>a b : α<GOAL>a ≤ b → ∃ c, b = a * c
<VAR>α : Type u<VAR>CanonicallyOrderedCommMonoid α<VAR>a c : α<GOAL>a ≤ a * c
<VAR>α : Type u<VAR>CanonicallyOrderedAddCommMonoid α<VAR>a c : α<GOAL>a ≤ a + c
<VAR>α : Type u<VAR>CanonicallyOrderedAddCommMonoid α<VAR>a b : α<GOAL>a ≤ b + a
<VAR>α : Type u<VAR>CanonicallyOrderedCommMonoid α<VAR>a b : α<GOAL>a ≤ b * a
<VAR>α : Type u<VAR>CanonicallyOrderedCommMonoid α<VAR>a b : α<GOAL>a ≤ a * b
<VAR>α : Type u<VAR>CanonicallyOrderedAddCommMonoid α<VAR>a b : α<GOAL>a ≤ a + b
<VAR>α : Type u<VAR>CanonicallyOrderedCommMonoid α<VAR>a b c : α<GOAL>a * b ≤ c → a ≤ c
<VAR>α : Type u<VAR>CanonicallyOrderedAddCommMonoid α<VAR>a b c : α<GOAL>a + b ≤ c → a ≤ c
<VAR>α : Type u<VAR>CanonicallyOrderedAddCommMonoid α<VAR>a b c : α<GOAL>a + b ≤ c → b ≤ c
<VAR>α : Type u<VAR>CanonicallyOrderedCommMonoid α<VAR>a b c : α<GOAL>a * b ≤ c → b ≤ c
<VAR>α : Type u<VAR>CanonicallyOrderedCommMonoid α<VAR>a b c : α<GOAL>a ≤ b → a ≤ b * c
<VAR>α : Type u<VAR>CanonicallyOrderedAddCommMonoid α<VAR>a b c : α<GOAL>a ≤ b → a ≤ b + c
<VAR>α : Type u<VAR>CanonicallyOrderedAddCommMonoid α<VAR>a b c : α<GOAL>a ≤ c → a ≤ b + c
<VAR>α : Type u<VAR>CanonicallyOrderedCommMonoid α<VAR>a b c : α<GOAL>a ≤ c → a ≤ b * c
<VAR>α : Type u<VAR>CanonicallyOrderedCommMonoid α<VAR>a b : α<GOAL>a ≤ b ↔ ∃ c, b = a * c
<VAR>α : Type u<VAR>CanonicallyOrderedAddCommMonoid α<VAR>a b : α<GOAL>a ≤ b ↔ ∃ c, b = a + c
<VAR>α : Type u<VAR>CanonicallyOrderedAddCommMonoid α<VAR>a b : α<GOAL>a ≤ b ↔ ∃ c, b = c + a
<VAR>α : Type u<VAR>CanonicallyOrderedCommMonoid α<VAR>a b : α<GOAL>a ≤ b ↔ ∃ c, b = c * a
<VAR>α : Type u<VAR>CanonicallyOrderedCommMonoid α<VAR>a : α<GOAL>1 ≤ a
<VAR>α : Type u<VAR>CanonicallyOrderedAddCommMonoid α<VAR>a : α<GOAL>0 ≤ a
<VAR>α : Type u<VAR>CanonicallyOrderedCommMonoid α<GOAL>⊥ = 1
<VAR>α : Type u<VAR>CanonicallyOrderedAddCommMonoid α<GOAL>⊥ = 0
<VAR>α : Type u<VAR>CanonicallyOrderedAddCommMonoid α<VAR>a b : α<GOAL>a + b = 0 ↔ a = 0 ∧ b = 0
<VAR>α : Type u<VAR>CanonicallyOrderedCommMonoid α<VAR>a b : α<GOAL>a * b = 1 ↔ a = 1 ∧ b = 1
<VAR>α : Type u<VAR>CanonicallyOrderedCommMonoid α<VAR>a : α<GOAL>a ≤ 1 ↔ a = 1
<VAR>α : Type u<VAR>CanonicallyOrderedAddCommMonoid α<VAR>a : α<GOAL>a ≤ 0 ↔ a = 0
<VAR>α : Type u<VAR>CanonicallyOrderedAddCommMonoid α<VAR>a : α<GOAL>0 < a ↔ a ≠ 0
<VAR>α : Type u<VAR>CanonicallyOrderedCommMonoid α<VAR>a : α<GOAL>1 < a ↔ a ≠ 1
<VAR>α : Type u<VAR>CanonicallyOrderedAddCommMonoid α<VAR>a : α<GOAL>a = 0 ∨ 0 < a
<VAR>α : Type u<VAR>CanonicallyOrderedCommMonoid α<VAR>a : α<GOAL>a = 1 ∨ 1 < a
<VAR>α : Type u<VAR>CanonicallyOrderedAddCommMonoid α<VAR>a b : α<GOAL>0 < a + b ↔ 0 < a ∨ 0 < b
<VAR>α : Type u<VAR>CanonicallyOrderedCommMonoid α<VAR>a b : α<GOAL>1 < a * b ↔ 1 < a ∨ 1 < b
<VAR>α : Type u<VAR>CanonicallyOrderedAddCommMonoid α<VAR>a b : α<VAR>h : a < b<GOAL>∃ c x, a + c = b
<VAR>α : Type u<VAR>CanonicallyOrderedCommMonoid α<VAR>a b : α<VAR>h : a < b<GOAL>∃ c x, a * c = b
<VAR>α : Type u<VAR>CanonicallyOrderedAddCommMonoid α<VAR>a b c : α<VAR>h : a ≤ c<GOAL>a ≤ b + c
<VAR>α : Type u<VAR>CanonicallyOrderedCommMonoid α<VAR>a b c : α<VAR>h : a ≤ c<GOAL>a ≤ b * c
<VAR>α : Type u<VAR>CanonicallyOrderedCommMonoid α<VAR>a b c : α<VAR>h : a ≤ b<GOAL>a ≤ b * c
<VAR>α : Type u<VAR>CanonicallyOrderedAddCommMonoid α<VAR>a b c : α<VAR>h : a ≤ b<GOAL>a ≤ b + c
<VAR>α : Type u<VAR>CanonicallyOrderedCommMonoid α<VAR>a b : α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<GOAL>a < b ↔ ∃ c, c > 1 ∧ b = a * c
<VAR>α : Type u<VAR>CanonicallyOrderedAddCommMonoid α<VAR>a b : α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<GOAL>a < b ↔ ∃ c, c > 0 ∧ b = a + c
<VAR>M : Type u_1<VAR>CanonicallyOrderedAddCommMonoid M<VAR>n m : M<VAR>h : n < m<GOAL>0 < m
<VAR>M : Type u_1<VAR>a : M<VAR>CanonicallyOrderedAddCommMonoid M<VAR>NeZero a<GOAL>0 < a
<VAR>M : Type u_1<VAR>CanonicallyOrderedAddCommMonoid M<VAR>x y : M<VAR>h : x < y<GOAL>NeZero y
<VAR>α : Type u<VAR>CanonicallyLinearOrderedAddCommMonoid α<VAR>a b c : α<GOAL>min a (b + c) = min a (min a b + min a c)
<VAR>α : Type u<VAR>CanonicallyLinearOrderedCommMonoid α<VAR>a b c : α<GOAL>min a (b * c) = min a (min a b * min a c)
<VAR>α : Type u<VAR>CanonicallyLinearOrderedAddCommMonoid α<VAR>a b c : α<GOAL>min (a + b) c = min (min a c + min b c) c
<VAR>α : Type u<VAR>CanonicallyLinearOrderedCommMonoid α<VAR>a b c : α<GOAL>min (a * b) c = min (min a c * min b c) c
<VAR>α : Type u<VAR>CanonicallyLinearOrderedAddCommMonoid α<VAR>a : α<GOAL>min 0 a = 0
<VAR>α : Type u<VAR>CanonicallyLinearOrderedCommMonoid α<VAR>a : α<GOAL>min 1 a = 1
<VAR>α : Type u<VAR>CanonicallyLinearOrderedCommMonoid α<VAR>a : α<GOAL>min a 1 = 1
<VAR>α : Type u<VAR>CanonicallyLinearOrderedAddCommMonoid α<VAR>a : α<GOAL>min a 0 = 0
<VAR>α : Type u<VAR>CanonicallyLinearOrderedCommMonoid α<GOAL>⊥ = 1
<VAR>α : Type u<VAR>CanonicallyLinearOrderedAddCommMonoid α<GOAL>⊥ = 0
<VAR>M : Type u_1<VAR>Monoid M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<GOAL>↑(Submonoid.oneLE M) = Set.Ici 1
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>↑(AddSubmonoid.nonneg M) = Set.Ici 0
<VAR>M : Type u_1<VAR>Monoid M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : M<GOAL>a ∈ Submonoid.oneLE M ↔ 1 ≤ a
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : M<GOAL>a ∈ AddSubmonoid.nonneg M ↔ 0 ≤ a
<VAR>α : Type u_2<VAR>MulZeroOneClass α<VAR>PartialOrder α<VAR>PosMulStrictMono α<VAR>ZeroLEOneClass α<VAR>NeZero 1<GOAL>↑(Submonoid.pos α) = Set.Ioi 0
<VAR>α : Type u_2<VAR>MulZeroOneClass α<VAR>PartialOrder α<VAR>PosMulStrictMono α<VAR>ZeroLEOneClass α<VAR>NeZero 1<VAR>a : α<GOAL>a ∈ Submonoid.pos α ↔ 0 < a
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b : α<VAR>h : a ≤ b<GOAL>a + (b - a) = b
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b : α<VAR>h : a ≤ b<GOAL>b - a + a = b
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>h : b ≤ c<VAR>h2 : a ≤ c - b<GOAL>a + b ≤ c
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>h : a ≤ c<VAR>h2 : b ≤ c - a<GOAL>a + b ≤ c
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>h : c ≤ b<GOAL>a - c ≤ b - c ↔ a ≤ b
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>h1 : c ≤ a<VAR>h2 : c ≤ b<GOAL>a - c = b - c ↔ a = b
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>h₁ : a ≤ b<VAR>h₂ : a ≤ c<GOAL>b - a = c - a → b = c
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>h : c ≤ b<VAR>h2 : a - c < b - c<GOAL>a < b
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>hab : b ≤ a<VAR>hcb : c ≤ b<GOAL>a - b + (b - c) = a - c
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>h : c ≤ b<GOAL>a - c - (b - c) = a - b
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>hc : AddLECancellable c<VAR>h : c ≤ b<GOAL>a = b - c ↔ a + c = b
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>hb : AddLECancellable b<VAR>h : b ≤ a<GOAL>a - b = c ↔ a = c + b
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>b c : α<VAR>hc : AddLECancellable c<VAR>h : c ≤ b<VAR>a : α<GOAL>a + b - c = a + (b - c)
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>hb : AddLECancellable b<VAR>h : b ≤ a<GOAL>a - b + c = a + c - b
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>hbc : AddLECancellable (b - c)<VAR>h₁ : b ≤ a<VAR>h₂ : c ≤ b<GOAL>a - (b - c) = a - b + c
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c d : α<VAR>hb : AddLECancellable b<VAR>hd : AddLECancellable d<VAR>hba : b ≤ a<VAR>hdc : d ≤ c<GOAL>a - b + (c - d) = a + c - (b + d)
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ha : AddLECancellable a<VAR>h : a ≤ c<GOAL>b ≤ c - a ↔ a + b ≤ c
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ha : AddLECancellable a<VAR>h : a ≤ c<GOAL>b ≤ c - a ↔ b + a ≤ c
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>hb : AddLECancellable b<VAR>hba : b ≤ a<GOAL>a - b < c ↔ a < b + c
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>hb : AddLECancellable b<VAR>hba : b ≤ a<GOAL>a - b < c ↔ a < c + b
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>hb : AddLECancellable b<VAR>hc : AddLECancellable c<VAR>h₁ : b ≤ a<VAR>h₂ : c ≤ a<GOAL>a - b < c ↔ a - c < b
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ha : AddLECancellable a<VAR>hc : AddLECancellable c<VAR>h₁ : a ≤ b<VAR>h₂ : c ≤ b<GOAL>a ≤ b - c ↔ c ≤ b - a
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>hc : AddLECancellable c<VAR>h : c ≤ b<GOAL>a < b - c ↔ a + c < b
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>hc : AddLECancellable c<VAR>h : c ≤ b<GOAL>a < b - c ↔ c + a < b
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>hab : AddLECancellable (a - b)<VAR>h₁ : b ≤ a<VAR>h₂ : c ≤ a<VAR>h₃ : a - b = a - c<GOAL>b = c
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>hb : AddLECancellable b<VAR>hca : c ≤ a<VAR>h : a - b < a - c<GOAL>c < b
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>hab : AddLECancellable (a - b)<VAR>h₁ : b ≤ a<VAR>h : c < b<GOAL>a - b < a - c
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>hc : AddLECancellable c<VAR>h : c ≤ a<VAR>h2 : a < b<GOAL>a - c < b - c
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>hb : AddLECancellable b<VAR>hab : AddLECancellable (a - b)<VAR>h₁ : b ≤ a<VAR>h₂ : c ≤ a<GOAL>a - b < a - c ↔ c < b
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>hac : AddLECancellable (a - c)<VAR>h : c ≤ a<GOAL>a + b - (a - c) = b + c
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b : α<VAR>hba : AddLECancellable (b - a)<VAR>h : a ≤ b<GOAL>b - (b - a) = a
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>hab : AddLECancellable (a - b)<VAR>h : b ≤ a<GOAL>a - c - (a - b) = b - c
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : c ≤ b<GOAL>a = b - c ↔ a + c = b
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : b ≤ a<GOAL>a - b = c ↔ a = c + b
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>b c : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : c ≤ b<VAR>a : α<GOAL>a + b - c = a + (b - c)
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : b ≤ a<GOAL>a - b + c = a + c - b
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h₁ : b ≤ a<VAR>h₂ : c ≤ b<GOAL>a - (b - c) = a - b + c
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c d : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hba : b ≤ a<VAR>hdc : d ≤ c<GOAL>a - b + (c - d) = a + c - (b + d)
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : a ≤ c<GOAL>b ≤ c - a ↔ a + b ≤ c
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : a ≤ c<GOAL>b ≤ c - a ↔ b + a ≤ c
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hbc : b ≤ a<GOAL>a - b < c ↔ a < b + c
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hbc : b ≤ a<GOAL>a - b < c ↔ a < c + b
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h₁ : b ≤ a<VAR>h₂ : c ≤ a<GOAL>a - b < c ↔ a - c < b
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h₁ : a ≤ b<VAR>h₂ : c ≤ b<GOAL>a ≤ b - c ↔ c ≤ b - a
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : c ≤ b<GOAL>a < b - c ↔ a + c < b
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : c ≤ b<GOAL>a < b - c ↔ c + a < b
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>hca : c ≤ a<VAR>h : a - b < a - c<GOAL>c < b
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>b ≤ a → c < b → a - b < a - c
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : c ≤ a<VAR>h2 : a < b<GOAL>a - c < b - c
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h₁ : b ≤ a<VAR>h₂ : c ≤ a<VAR>h₃ : a - b = a - c<GOAL>b = c
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>h₁ : b ≤ a<VAR>h₂ : c ≤ a<GOAL>a - b < a - c ↔ c < b
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : c ≤ a<GOAL>a + b - (a - c) = b + c
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : a ≤ b<GOAL>b - (b - a) = a
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : b ≤ a<GOAL>a - c - (a - b) = b - c
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>PartialOrder α<VAR>ExistsAddOfLE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Sub α<VAR>OrderedSub α<VAR>a b c : α<VAR>ContravariantClass α α HAdd.hAdd LE.le<VAR>h : c ≤ b<GOAL>a - (b - c) = a + c - b
<VAR>α : Type u_1<VAR>CanonicallyOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>a b : α<GOAL>a + (b - a) = b ↔ a ≤ b
<VAR>α : Type u_1<VAR>CanonicallyOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>a b : α<GOAL>b - a + a = b ↔ a ≤ b
<VAR>α : Type u_1<VAR>CanonicallyOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>a b : α<GOAL>a - b = 0 ↔ a ≤ b
<VAR>α : Type u_1<VAR>CanonicallyOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>a : α<GOAL>a - a = 0
<VAR>α : Type u_1<VAR>CanonicallyOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>a b : α<GOAL>a - b ≤ a
<VAR>α : Type u_1<VAR>CanonicallyOrderedAddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>a : α<GOAL>0 - a = 0