ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>Group α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>h : a < 1<GOAL>1 < mabs a
<VAR>α : Type u_1<VAR>AddGroup α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>-|a| ≤ a
<VAR>α : Type u_1<VAR>Group α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>(mabs a)⁻¹ ≤ a
<VAR>α : Type u_1<VAR>Group α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>1 ≤ a * mabs a
<VAR>α : Type u_1<VAR>AddGroup α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>0 ≤ a + |a|
<VAR>α : Type u_1<VAR>Group α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>(mabs a)⁻¹ ≤ a⁻¹
<VAR>α : Type u_1<VAR>AddGroup α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>-|a| ≤ -a
<VAR>α : Type u_1<VAR>AddGroup α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>|a| ≠ 0 ↔ a ≠ 0
<VAR>α : Type u_1<VAR>Group α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<GOAL>mabs a ≠ 1 ↔ a ≠ 1
<VAR>α : Type u_1<VAR>AddGroup α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>|a| = 0 ↔ a = 0
<VAR>α : Type u_1<VAR>Group α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<GOAL>mabs a = 1 ↔ a = 1
<VAR>α : Type u_1<VAR>AddGroup α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>|a| ≤ 0 ↔ a = 0
<VAR>α : Type u_1<VAR>Group α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<GOAL>mabs a ≤ 1 ↔ a = 1
<VAR>α : Type u_1<VAR>Group α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>ha : a ≤ 1<VAR>hab : b ≤ a<GOAL>mabs a ≤ mabs b
<VAR>α : Type u_1<VAR>AddGroup α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ha : a ≤ 0<VAR>hab : b ≤ a<GOAL>|a| ≤ |b|
<VAR>α : Type u_1<VAR>AddGroup α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>|a| < b ↔ -b < a ∧ a < b
<VAR>α : Type u_1<VAR>Group α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<GOAL>mabs a < b ↔ b⁻¹ < a ∧ a < b
<VAR>α : Type u_1<VAR>Group α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>h : mabs a < b<GOAL>b⁻¹ < a
<VAR>α : Type u_1<VAR>AddGroup α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : |a| < b<GOAL>-b < a
<VAR>α : Type u_1<VAR>Group α<VAR>LinearOrder α<VAR>a b : α<GOAL>mabs a < b → a < b
<VAR>α : Type u_1<VAR>AddGroup α<VAR>LinearOrder α<VAR>a b : α<GOAL>|a| < b → a < b
<VAR>α : Type u_1<VAR>Group α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>max a b / min a b = mabs (a / b)
<VAR>α : Type u_1<VAR>AddGroup α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>max a b - min a b = |a - b|
<VAR>α : Type u_1<VAR>AddGroup α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>max a b - min a b = |b - a|
<VAR>α : Type u_1<VAR>Group α<VAR>LinearOrder α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>max a b / min a b = mabs (b / a)
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddCommGroup α<VAR>s : Set α<GOAL>LatticeOrderedAddCommGroup.IsSolid (LatticeOrderedAddCommGroup.solidClosure s)
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddCommGroup α<VAR>s t : Set α<VAR>hst : s ⊆ t<VAR>ht : LatticeOrderedAddCommGroup.IsSolid t<GOAL>LatticeOrderedAddCommGroup.solidClosure s ⊆ t
<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>(i : ι) → AddGroup (α i)<VAR>(i : ι) → Lattice (α i)<VAR>f : (i : ι) → α i<VAR>i : ι<GOAL>|f| i = |f i|
<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>(i : ι) → AddGroup (α i)<VAR>(i : ι) → Lattice (α i)<VAR>f : (i : ι) → α i<GOAL>|f| = fun i => |f i|
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>n : ℕ<VAR>a : α<GOAL>|n • a| = n • |a|
<VAR>α : Type u_1<VAR>LinearOrderedCommGroup α<VAR>n : ℕ<VAR>a : α<GOAL>mabs (a ^ n) = mabs a ^ n
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b : α<VAR>hab : a ≤ b<GOAL>|a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
<VAR>α : Type u_1<VAR>LinearOrderedCommGroup α<VAR>a b : α<VAR>hab : a ≤ b<GOAL>mabs (a * b) = mabs a * mabs b ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
<VAR>α : Type u_1<VAR>LinearOrderedCommGroup α<VAR>a b : α<GOAL>mabs (a * b) = mabs a * mabs b ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b : α<GOAL>|a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b : α<GOAL>|a| ≤ b ↔ -b ≤ a ∧ a ≤ b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b : α<GOAL>a ≤ |b| ↔ b ≤ -a ∨ a ≤ b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b : α<VAR>h : |a| ≤ b<GOAL>-b ≤ a
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b : α<VAR>h : |a| ≤ b<GOAL>a ≤ b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>β : Type u_2<VAR>MulOneClass β<VAR>Preorder β<VAR>CovariantClass β β (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass β β (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>f : α → β<VAR>a : α<VAR>h₁ : 1 ≤ f a<VAR>h₂ : 1 ≤ f (-a)<GOAL>f |a| ≤ f a * f (-a)
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>β : Type u_2<VAR>AddZeroClass β<VAR>Preorder β<VAR>CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass β β (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>f : α → β<VAR>a : α<VAR>h₁ : 0 ≤ f a<VAR>h₂ : 0 ≤ f (-a)<GOAL>f |a| ≤ f a + f (-a)
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>β : Type u_2<VAR>MulOneClass β<VAR>Preorder β<VAR>CovariantClass β β (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass β β (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>f : α → β<VAR>h : ∀ (x : α), 1 ≤ f x<VAR>a : α<GOAL>f |a| ≤ f a * f (-a)
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>β : Type u_2<VAR>AddZeroClass β<VAR>Preorder β<VAR>CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass β β (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>f : α → β<VAR>h : ∀ (x : α), 0 ≤ f x<VAR>a : α<GOAL>f |a| ≤ f a + f (-a)
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b : α<GOAL>|a + b| ≤ |a| + |b|
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b : α<GOAL>|a| ≤ |b| + |b + a|
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b : α<GOAL>|a - b| ≤ |a| + |b|
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b c : α<GOAL>|a - b| ≤ c ↔ a - b ≤ c ∧ b - a ≤ c
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b c : α<GOAL>|a - b| < c ↔ a - b < c ∧ b - a < c
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b c : α<VAR>h : |a - b| ≤ c<GOAL>b - c ≤ a
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b c : α<VAR>h : |a - b| ≤ c<GOAL>a - c ≤ b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b c : α<VAR>h : |a - b| < c<GOAL>b - c < a
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b c : α<VAR>h : |a - b| < c<GOAL>a - c < b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b : α<GOAL>|a| - |b| ≤ |a - b|
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b : α<GOAL>||a| - |b|| ≤ |a - b|
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b n : α<VAR>a_nonneg : 0 ≤ a<VAR>a_le_n : a ≤ n<VAR>b_nonneg : 0 ≤ b<VAR>b_le_n : b ≤ n<GOAL>|a - b| ≤ n
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b n : α<VAR>a_nonneg : 0 ≤ a<VAR>a_lt_n : a < n<VAR>b_nonneg : 0 ≤ b<VAR>b_lt_n : b < n<GOAL>|a - b| < n
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b : α<VAR>hb : 0 ≤ b<GOAL>|a| = b ↔ a = b ∨ a = -b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b c : α<VAR>hab : a ≤ b<VAR>hbc : b ≤ c<GOAL>|b| ≤ max |a| |c|
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b : α<GOAL>min |a| |b| ≤ |max a b|
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b : α<GOAL>min |a| |b| ≤ |min a b|
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b : α<GOAL>|max a b| ≤ max |a| |b|
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b : α<GOAL>|min a b| ≤ max |a| |b|
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b : α<VAR>h : |a - b| = 0<GOAL>a = b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b c : α<GOAL>|a - c| ≤ |a - b| + |b - c|
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b c : α<GOAL>|a + b + c| ≤ |a| + |b| + |c|
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b lb ub : α<VAR>hal : lb ≤ a<VAR>hau : a ≤ ub<VAR>hbl : lb ≤ b<VAR>hbu : b ≤ ub<GOAL>|a - b| ≤ ub - lb
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b : α<VAR>h : |a - b| ≤ 0<GOAL>a = b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b : α<GOAL>|a - b| ≤ 0 ↔ a = b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b : α<GOAL>0 < |a - b| ↔ a ≠ b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a : α<GOAL>|a| = a ↔ 0 ≤ a
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a : α<GOAL>|a| = -a ↔ a ≤ 0
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a : α<GOAL>|a| = a ∧ 0 ≤ a ∨ |a| = -a ∧ a < 0
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a : α<GOAL>max a 0 + max (-a) 0 = |a|
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>Zero M<VAR>SemilatticeSup M<VAR>f g : α → M<GOAL>(Function.support fun x => f x ⊔ g x) ⊆ Function.support f ∪ Function.support g
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>One M<VAR>SemilatticeSup M<VAR>f g : α → M<GOAL>(Function.mulSupport fun x => f x ⊔ g x) ⊆ Function.mulSupport f ∪ Function.mulSupport g
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>One M<VAR>SemilatticeInf M<VAR>f g : α → M<GOAL>(Function.mulSupport fun x => f x ⊓ g x) ⊆ Function.mulSupport f ∪ Function.mulSupport g
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>Zero M<VAR>SemilatticeInf M<VAR>f g : α → M<GOAL>(Function.support fun x => f x ⊓ g x) ⊆ Function.support f ∪ Function.support g
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>Zero M<VAR>LinearOrder M<VAR>f g : α → M<GOAL>(Function.support fun x => max (f x) (g x)) ⊆ Function.support f ∪ Function.support g
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>One M<VAR>LinearOrder M<VAR>f g : α → M<GOAL>(Function.mulSupport fun x => max (f x) (g x)) ⊆ Function.mulSupport f ∪ Function.mulSupport g
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>Zero M<VAR>LinearOrder M<VAR>f g : α → M<GOAL>(Function.support fun x => min (f x) (g x)) ⊆ Function.support f ∪ Function.support g
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>One M<VAR>LinearOrder M<VAR>f g : α → M<GOAL>(Function.mulSupport fun x => min (f x) (g x)) ⊆ Function.mulSupport f ∪ Function.mulSupport g
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>M : Type u_4<VAR>Zero M<VAR>ConditionallyCompleteLattice M<VAR>Nonempty ι<VAR>f : ι → α → M<GOAL>(Function.support fun x => ⨆ i, f i x) ⊆ ⋃ i, Function.support (f i)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>M : Type u_4<VAR>One M<VAR>ConditionallyCompleteLattice M<VAR>Nonempty ι<VAR>f : ι → α → M<GOAL>(Function.mulSupport fun x => ⨆ i, f i x) ⊆ ⋃ i, Function.mulSupport (f i)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>M : Type u_4<VAR>One M<VAR>ConditionallyCompleteLattice M<VAR>Nonempty ι<VAR>f : ι → α → M<GOAL>(Function.mulSupport fun x => ⨅ i, f i x) ⊆ ⋃ i, Function.mulSupport (f i)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>M : Type u_4<VAR>Zero M<VAR>ConditionallyCompleteLattice M<VAR>Nonempty ι<VAR>f : ι → α → M<GOAL>(Function.support fun x => ⨅ i, f i x) ⊆ ⋃ i, Function.support (f i)
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>LE M<VAR>One M<VAR>s : Set α<VAR>f : α → M<VAR>a : α<VAR>y : M<VAR>hfg : a ∈ s → f a ≤ y<VAR>hg : a ∉ s → 1 ≤ y<GOAL>s.mulIndicator f a ≤ y
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>LE M<VAR>Zero M<VAR>s : Set α<VAR>f : α → M<VAR>a : α<VAR>y : M<VAR>hfg : a ∈ s → f a ≤ y<VAR>hg : a ∉ s → 0 ≤ y<GOAL>s.indicator f a ≤ y
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>LE M<VAR>One M<VAR>s : Set α<VAR>f g : α → M<VAR>hfg : ∀ a ∈ s, f a ≤ g a<VAR>hg : ∀ a ∉ s, 1 ≤ g a<GOAL>s.mulIndicator f ≤ g
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>LE M<VAR>Zero M<VAR>s : Set α<VAR>f g : α → M<VAR>hfg : ∀ a ∈ s, f a ≤ g a<VAR>hg : ∀ a ∉ s, 0 ≤ g a<GOAL>s.indicator f ≤ g
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>LE M<VAR>Zero M<VAR>s : Set α<VAR>g : α → M<VAR>a : α<VAR>y : M<VAR>hfg : a ∈ s → y ≤ g a<VAR>hf : a ∉ s → y ≤ 0<GOAL>y ≤ s.indicator g a
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>LE M<VAR>One M<VAR>s : Set α<VAR>g : α → M<VAR>a : α<VAR>y : M<VAR>hfg : a ∈ s → y ≤ g a<VAR>hf : a ∉ s → y ≤ 1<GOAL>y ≤ s.mulIndicator g a
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>LE M<VAR>One M<VAR>s : Set α<VAR>f g : α → M<VAR>hfg : ∀ a ∈ s, f a ≤ g a<VAR>hf : ∀ a ∉ s, f a ≤ 1<GOAL>f ≤ s.mulIndicator g
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>LE M<VAR>Zero M<VAR>s : Set α<VAR>f g : α → M<VAR>hfg : ∀ a ∈ s, f a ≤ g a<VAR>hf : ∀ a ∉ s, f a ≤ 0<GOAL>f ≤ s.indicator g
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>Preorder M<VAR>One M<VAR>s : Set α<VAR>f : α → M<VAR>a : α<VAR>h : a ∈ s → 1 ≤ f a<GOAL>1 ≤ s.mulIndicator f a
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>Preorder M<VAR>Zero M<VAR>s : Set α<VAR>f : α → M<VAR>a : α<VAR>h : a ∈ s → 0 ≤ f a<GOAL>0 ≤ s.indicator f a
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>Preorder M<VAR>One M<VAR>s : Set α<VAR>f : α → M<VAR>h : ∀ a ∈ s, 1 ≤ f a<VAR>a : α<GOAL>1 ≤ s.mulIndicator f a
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>Preorder M<VAR>Zero M<VAR>s : Set α<VAR>f : α → M<VAR>h : ∀ a ∈ s, 0 ≤ f a<VAR>a : α<GOAL>0 ≤ s.indicator f a
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>Preorder M<VAR>One M<VAR>s : Set α<VAR>f : α → M<VAR>a : α<VAR>h : a ∈ s → f a ≤ 1<GOAL>s.mulIndicator f a ≤ 1
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>Preorder M<VAR>Zero M<VAR>s : Set α<VAR>f : α → M<VAR>a : α<VAR>h : a ∈ s → f a ≤ 0<GOAL>s.indicator f a ≤ 0
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>Preorder M<VAR>Zero M<VAR>s : Set α<VAR>f : α → M<VAR>h : ∀ a ∈ s, f a ≤ 0<VAR>a : α<GOAL>s.indicator f a ≤ 0
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>Preorder M<VAR>One M<VAR>s : Set α<VAR>f : α → M<VAR>h : ∀ a ∈ s, f a ≤ 1<VAR>a : α<GOAL>s.mulIndicator f a ≤ 1
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>Preorder M<VAR>Zero M<VAR>s : Set α<VAR>f g : α → M<VAR>a : α<VAR>h : f a ≤ g a<GOAL>s.indicator f a ≤ s.indicator g a
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>Preorder M<VAR>One M<VAR>s : Set α<VAR>f g : α → M<VAR>a : α<VAR>h : f a ≤ g a<GOAL>s.mulIndicator f a ≤ s.mulIndicator g a
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>Preorder M<VAR>Zero M<VAR>s t : Set α<VAR>f : α → M<VAR>h : s ⊆ t<VAR>hf : ∀ (a : α), 0 ≤ f a<VAR>a : α<GOAL>s.indicator f a ≤ t.indicator f a
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>Preorder M<VAR>One M<VAR>s t : Set α<VAR>f : α → M<VAR>h : s ⊆ t<VAR>hf : ∀ (a : α), 1 ≤ f a<VAR>a : α<GOAL>s.mulIndicator f a ≤ t.mulIndicator f a
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>Preorder M<VAR>One M<VAR>s : Set α<VAR>f : α → M<VAR>hf : ∀ x ∉ s, 1 ≤ f x<GOAL>s.mulIndicator f ≤ f
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>Preorder M<VAR>Zero M<VAR>s : Set α<VAR>f : α → M<VAR>hf : ∀ x ∉ s, 0 ≤ f x<GOAL>s.indicator f ≤ f
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>Zero M<VAR>LinearOrder M<VAR>s : Set α<VAR>f : α → M<GOAL>s.indicator f ≤ {a | 0 ≤ f a}.indicator f
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>Zero M<VAR>LinearOrder M<VAR>s : Set α<VAR>f : α → M<GOAL>{a | f a ≤ 0}.indicator f ≤ s.indicator f
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>M : Type u_4<VAR>CompleteLattice M<VAR>Zero M<VAR>h1 : ⊥ = 0<VAR>s : ι → Set α<VAR>f : α → M<VAR>x : α<GOAL>(⋃ i, s i).indicator f x = ⨆ i, (s i).indicator f x
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>M : Type u_4<VAR>CompleteLattice M<VAR>One M<VAR>h1 : ⊥ = 1<VAR>s : ι → Set α<VAR>f : α → M<VAR>x : α<GOAL>(⋃ i, s i).mulIndicator f x = ⨆ i, (s i).mulIndicator f x
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>M : Type u_4<VAR>CompleteLattice M<VAR>One M<VAR>Nonempty ι<VAR>h1 : ⊥ = 1<VAR>s : ι → Set α<VAR>f : α → M<VAR>x : α<GOAL>(⋂ i, s i).mulIndicator f x = ⨅ i, (s i).mulIndicator f x
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>M : Type u_4<VAR>CompleteLattice M<VAR>Zero M<VAR>Nonempty ι<VAR>h1 : ⊥ = 0<VAR>s : ι → Set α<VAR>f : α → M<VAR>x : α<GOAL>(⋂ i, s i).indicator f x = ⨅ i, (s i).indicator f x
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>CanonicallyOrderedAddCommMonoid M<VAR>s : Set α<VAR>f : α → M<GOAL>s.indicator f ≤ f
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>CanonicallyOrderedCommMonoid M<VAR>s : Set α<VAR>f : α → M<GOAL>s.mulIndicator f ≤ f
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>CanonicallyOrderedAddCommMonoid M<VAR>a : α<VAR>s : Set α<VAR>f g : α → M<VAR>hfg : a ∈ s → f a ≤ g a<GOAL>s.indicator f a ≤ g a
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>CanonicallyOrderedCommMonoid M<VAR>a : α<VAR>s : Set α<VAR>f g : α → M<VAR>hfg : a ∈ s → f a ≤ g a<GOAL>s.mulIndicator f a ≤ g a
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>CanonicallyOrderedCommMonoid M<VAR>s : Set α<VAR>f g : α → M<VAR>hfg : ∀ a ∈ s, f a ≤ g a<GOAL>s.mulIndicator f ≤ g
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>CanonicallyOrderedAddCommMonoid M<VAR>s : Set α<VAR>f g : α → M<VAR>hfg : ∀ a ∈ s, f a ≤ g a<GOAL>s.indicator f ≤ g
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>LinearOrderedAddCommGroup M<VAR>s t : Set α<VAR>f : α → M<VAR>x : α<GOAL>|(symmDiff s t).indicator f x| = |s.indicator f x - t.indicator f x|
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>LinearOrderedCommGroup M<VAR>s t : Set α<VAR>f : α → M<VAR>x : α<GOAL>mabs ((symmDiff s t).mulIndicator f x) = mabs (s.mulIndicator f x / t.mulIndicator f x)
<VAR>α : Type u_2<VAR>Ring α<VAR>self : Ring.PositiveCone α<GOAL>self.nonneg 1
<VAR>α : Type u_2<VAR>Ring α<VAR>self : Ring.PositiveCone α<VAR>a b : α<GOAL>self.pos a → self.pos b → self.pos (a * b)
<VAR>α : Type u_1<VAR>Ring α<VAR>Nontrivial α<VAR>C : Ring.PositiveCone α<GOAL>C.pos 1
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<GOAL>Monotone oneLePart
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<GOAL>Monotone posPart
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<GOAL>1⁺ᵐ = 1
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<GOAL>0⁺ = 0
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<GOAL>0⁻ = 0
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<GOAL>1⁻ᵐ = 1
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>a : α<GOAL>1 ≤ a⁺ᵐ
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>a : α<GOAL>0 ≤ a⁺
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>a : α<GOAL>1 ≤ a⁻ᵐ
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>a : α<GOAL>0 ≤ a⁻
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>a : α<GOAL>a ≤ a⁺
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>a : α<GOAL>a ≤ a⁺ᵐ
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>a : α<GOAL>-a ≤ a⁻
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>a : α<GOAL>a⁻¹ ≤ a⁻ᵐ
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>a : α<GOAL>a⁺ᵐ = a ↔ 1 ≤ a
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>a : α<GOAL>a⁺ = a ↔ 0 ≤ a
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>a : α<GOAL>a⁺ᵐ = 1 ↔ a ≤ 1
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>a : α<GOAL>a⁺ = 0 ↔ a ≤ 0
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>a : α<GOAL>a⁻ᵐ = a⁻¹ ↔ 1 ≤ a⁻¹
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>a : α<GOAL>a⁻ = -a ↔ 0 ≤ -a
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>a : α<GOAL>a⁻ᵐ = 1 ↔ a⁻¹ ≤ 1
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>a : α<GOAL>a⁻ = 0 ↔ -a ≤ 0
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>a : α<GOAL>a⁺ᵐ ≤ 1 ↔ a ≤ 1
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>a : α<GOAL>a⁺ ≤ 0 ↔ a ≤ 0
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>a : α<GOAL>a⁻ᵐ ≤ 1 ↔ a⁻¹ ≤ 1
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>a : α<GOAL>a⁻ ≤ 0 ↔ -a ≤ 0
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>a : α<VAR>ha : 0 < a<GOAL>0 < a⁺
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>a : α<VAR>ha : 1 < a<GOAL>1 < a⁺ᵐ
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>a : α<GOAL>a⁻¹⁺ᵐ = a⁻ᵐ
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>a : α<GOAL>(-a)⁺ = a⁻
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>a : α<GOAL>(-a)⁻ = a⁺
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>a : α<GOAL>a⁻¹⁻ᵐ = a⁺ᵐ
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>a : α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<GOAL>a⁻ᵐ = a⁻¹ ↔ a ≤ 1
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>a : α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>a⁻ = -a ↔ a ≤ 0
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>a : α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>a⁻ = 0 ↔ 0 ≤ a
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>a : α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<GOAL>a⁻ᵐ = 1 ↔ 1 ≤ a
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>a : α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ha : a < 0<GOAL>0 < a⁻
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>a : α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>ha : a < 1<GOAL>1 < a⁻ᵐ
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>a⁺ - a⁻ = a
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>a⁺ᵐ / a⁻ᵐ = a
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>a⁻ᵐ / a⁺ᵐ = a⁻¹
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>a⁻ - a⁺ = -a
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>Antitone negPart
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<GOAL>Antitone leOnePart
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>a⁻ = -(a ⊓ 0)
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>a⁻ᵐ = (a ⊓ 1)⁻¹
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>a⁺ + a⁻ = |a|