ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a : α<VAR>n : ℤ<VAR>hn : Odd n<GOAL>a ^ n ≤ 0 ↔ a ≤ 0
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a : α<VAR>n : ℤ<VAR>hn : Odd n<GOAL>0 < a ^ n ↔ 0 < a
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>p : ℤ<VAR>hp : Even p<VAR>a : α<GOAL>|a| ^ p = a ^ p
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a : α<VAR>H : 1 < a<VAR>n : ℕ<GOAL>↑n ≤ (a ^ n - 1) / (a - 1)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a : α<VAR>H : 1 < a<VAR>n : ℕ<GOAL>↑n ≤ a ^ n / (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>DenselyOrdered α<VAR>a b : α<VAR>h : ∀ (ε : α), ε < 0 → a + ε ≤ b<GOAL>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>DenselyOrdered α<VAR>a b : α<VAR>h : ∀ (ε : α), ε < 1 → a * ε ≤ b<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>DenselyOrdered α<VAR>a b : α<VAR>h : ∀ (ε : α), 0 < ε → a - ε ≤ b<GOAL>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>DenselyOrdered α<VAR>a b : α<VAR>h : ∀ (ε : α), 1 < ε → a / ε ≤ b<GOAL>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>DenselyOrdered α<VAR>a b : α<GOAL>a ≤ b ↔ ∀ (ε : α), 1 < ε → 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>DenselyOrdered α<VAR>a b : α<GOAL>a ≤ b ↔ ∀ (ε : α), 0 < ε → 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>DenselyOrdered α<VAR>a b : α<GOAL>a ≤ b ↔ ∀ (ε : α), ε < 1 → 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>DenselyOrdered α<VAR>a b : α<GOAL>a ≤ b ↔ ∀ (ε : α), ε < 0 → a + ε ≤ b
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>self : AddCommGroup.PositiveCone α<VAR>a : α<GOAL>self.pos a ↔ self.nonneg a ∧ ¬self.nonneg (-a)
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>self : AddCommGroup.PositiveCone α<VAR>a b : α<GOAL>self.nonneg a → self.nonneg b → self.nonneg (a + b)
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>self : AddCommGroup.PositiveCone α<VAR>a : α<GOAL>self.nonneg a → self.nonneg (-a) → a = 0
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>self : AddCommGroup.PositiveCone α<GOAL>self.nonneg 0
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>self : AddCommGroup.TotalPositiveCone α<VAR>a : α<GOAL>self.nonneg a ∨ self.nonneg (-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 b c : α<GOAL>c * (a ⊔ b) = c * a ⊔ c * b
<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 b c : α<GOAL>c + a ⊔ b = (c + a) ⊔ (c + b)
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>(a ⊔ b) * c = a * c ⊔ b * c
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>a ⊔ b + c = (a + c) ⊔ (b + c)
<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 b c : α<GOAL>c * (a ⊓ b) = c * a ⊓ c * b
<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 b c : α<GOAL>c + a ⊓ b = (c + a) ⊓ (c + b)
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>a ⊓ b + c = (a + c) ⊓ (b + c)
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>(a ⊓ b) * c = a * c ⊓ b * c
<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 b : α<GOAL>(a ⊔ b)⁻¹ = a⁻¹ ⊓ b⁻¹
<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 b : α<GOAL>-(a ⊔ b) = -a ⊓ -b
<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 b : α<GOAL>(a ⊓ b)⁻¹ = a⁻¹ ⊔ b⁻¹
<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 b : α<GOAL>-(a ⊓ b) = -a ⊔ -b
<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 b c : α<GOAL>c - a ⊔ b = (c - a) ⊓ (c - b)
<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 b c : α<GOAL>c / (a ⊔ b) = c / a ⊓ c / b
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>a ⊔ b - c = (a - c) ⊔ (b - c)
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>(a ⊔ b) / c = a / c ⊔ b / c
<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 b c : α<GOAL>c / (a ⊓ b) = c / a ⊔ c / b
<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 b c : α<GOAL>c - a ⊓ b = (c - a) ⊔ (c - b)
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>(a ⊓ b) / c = a / c ⊓ b / c
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>a ⊓ b - c = (a - c) ⊓ (b - c)
<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 : α<VAR>ha : 1 ≤ a ^ 2<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>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>ha : 0 ≤ 2 • a<GOAL>0 ≤ a
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddCommGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a ⊓ b + a ⊔ b = a + b
<VAR>α : Type u_1<VAR>Lattice α<VAR>CommGroup α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>(a ⊓ b) * (a ⊔ b) = a * b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommGroup α<VAR>OrderedCommGroup β<VAR>s : Set ι<VAR>f : ι → α<VAR>g : ι → β<GOAL>MonovaryOn f⁻¹ g s ↔ AntivaryOn f g s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>OrderedAddCommGroup β<VAR>s : Set ι<VAR>f : ι → α<VAR>g : ι → β<GOAL>MonovaryOn (-f) g s ↔ AntivaryOn f g s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommGroup α<VAR>OrderedCommGroup β<VAR>s : Set ι<VAR>f : ι → α<VAR>g : ι → β<GOAL>AntivaryOn f⁻¹ g s ↔ MonovaryOn f g s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>OrderedAddCommGroup β<VAR>s : Set ι<VAR>f : ι → α<VAR>g : ι → β<GOAL>AntivaryOn (-f) g s ↔ MonovaryOn f g s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommGroup α<VAR>OrderedCommGroup β<VAR>s : Set ι<VAR>f : ι → α<VAR>g : ι → β<GOAL>MonovaryOn f g⁻¹ s ↔ AntivaryOn f g s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>OrderedAddCommGroup β<VAR>s : Set ι<VAR>f : ι → α<VAR>g : ι → β<GOAL>MonovaryOn f (-g) s ↔ AntivaryOn f g s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommGroup α<VAR>OrderedCommGroup β<VAR>s : Set ι<VAR>f : ι → α<VAR>g : ι → β<GOAL>AntivaryOn f g⁻¹ s ↔ MonovaryOn f g s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>OrderedAddCommGroup β<VAR>s : Set ι<VAR>f : ι → α<VAR>g : ι → β<GOAL>AntivaryOn f (-g) s ↔ MonovaryOn f g s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommGroup α<VAR>OrderedCommGroup β<VAR>s : Set ι<VAR>f : ι → α<VAR>g : ι → β<GOAL>MonovaryOn f⁻¹ g⁻¹ s ↔ MonovaryOn f g s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>OrderedAddCommGroup β<VAR>s : Set ι<VAR>f : ι → α<VAR>g : ι → β<GOAL>MonovaryOn (-f) (-g) s ↔ MonovaryOn f g s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommGroup α<VAR>OrderedCommGroup β<VAR>s : Set ι<VAR>f : ι → α<VAR>g : ι → β<GOAL>AntivaryOn f⁻¹ g⁻¹ s ↔ AntivaryOn f g s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>OrderedAddCommGroup β<VAR>s : Set ι<VAR>f : ι → α<VAR>g : ι → β<GOAL>AntivaryOn (-f) (-g) s ↔ AntivaryOn f g s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>OrderedAddCommGroup β<VAR>f : ι → α<VAR>g : ι → β<GOAL>Monovary (-f) g ↔ Antivary f g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommGroup α<VAR>OrderedCommGroup β<VAR>f : ι → α<VAR>g : ι → β<GOAL>Monovary f⁻¹ g ↔ Antivary f g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>OrderedAddCommGroup β<VAR>f : ι → α<VAR>g : ι → β<GOAL>Antivary (-f) g ↔ Monovary f g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommGroup α<VAR>OrderedCommGroup β<VAR>f : ι → α<VAR>g : ι → β<GOAL>Antivary f⁻¹ g ↔ Monovary f g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>OrderedAddCommGroup β<VAR>f : ι → α<VAR>g : ι → β<GOAL>Monovary f (-g) ↔ Antivary f g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommGroup α<VAR>OrderedCommGroup β<VAR>f : ι → α<VAR>g : ι → β<GOAL>Monovary f g⁻¹ ↔ Antivary f g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>OrderedAddCommGroup β<VAR>f : ι → α<VAR>g : ι → β<GOAL>Antivary f (-g) ↔ Monovary f g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommGroup α<VAR>OrderedCommGroup β<VAR>f : ι → α<VAR>g : ι → β<GOAL>Antivary f g⁻¹ ↔ Monovary f g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommGroup α<VAR>OrderedCommGroup β<VAR>f : ι → α<VAR>g : ι → β<GOAL>Monovary f⁻¹ g⁻¹ ↔ Monovary f g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>OrderedAddCommGroup β<VAR>f : ι → α<VAR>g : ι → β<GOAL>Monovary (-f) (-g) ↔ Monovary f g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>OrderedAddCommGroup β<VAR>f : ι → α<VAR>g : ι → β<GOAL>Antivary (-f) (-g) ↔ Antivary f g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommGroup α<VAR>OrderedCommGroup β<VAR>f : ι → α<VAR>g : ι → β<GOAL>Antivary f⁻¹ g⁻¹ ↔ Antivary f g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommGroup α<VAR>OrderedCommGroup β<VAR>s : Set ι<VAR>f₁ f₂ : ι → α<VAR>g : ι → β<VAR>h₁ : MonovaryOn f₁ g s<VAR>h₂ : MonovaryOn f₂ g s<GOAL>MonovaryOn (f₁ * f₂) g s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>OrderedAddCommGroup β<VAR>s : Set ι<VAR>f₁ f₂ : ι → α<VAR>g : ι → β<VAR>h₁ : MonovaryOn f₁ g s<VAR>h₂ : MonovaryOn f₂ g s<GOAL>MonovaryOn (f₁ + f₂) g s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>OrderedAddCommGroup β<VAR>s : Set ι<VAR>f₁ f₂ : ι → α<VAR>g : ι → β<VAR>h₁ : AntivaryOn f₁ g s<VAR>h₂ : AntivaryOn f₂ g s<GOAL>AntivaryOn (f₁ + f₂) g s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommGroup α<VAR>OrderedCommGroup β<VAR>s : Set ι<VAR>f₁ f₂ : ι → α<VAR>g : ι → β<VAR>h₁ : AntivaryOn f₁ g s<VAR>h₂ : AntivaryOn f₂ g s<GOAL>AntivaryOn (f₁ * f₂) g s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommGroup α<VAR>OrderedCommGroup β<VAR>s : Set ι<VAR>f₁ f₂ : ι → α<VAR>g : ι → β<VAR>h₁ : MonovaryOn f₁ g s<VAR>h₂ : AntivaryOn f₂ g s<GOAL>MonovaryOn (f₁ / f₂) g s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>OrderedAddCommGroup β<VAR>s : Set ι<VAR>f₁ f₂ : ι → α<VAR>g : ι → β<VAR>h₁ : MonovaryOn f₁ g s<VAR>h₂ : AntivaryOn f₂ g s<GOAL>MonovaryOn (f₁ - f₂) g s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>OrderedAddCommGroup β<VAR>s : Set ι<VAR>f₁ f₂ : ι → α<VAR>g : ι → β<VAR>h₁ : AntivaryOn f₁ g s<VAR>h₂ : MonovaryOn f₂ g s<GOAL>AntivaryOn (f₁ - f₂) g s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommGroup α<VAR>OrderedCommGroup β<VAR>s : Set ι<VAR>f₁ f₂ : ι → α<VAR>g : ι → β<VAR>h₁ : AntivaryOn f₁ g s<VAR>h₂ : MonovaryOn f₂ g s<GOAL>AntivaryOn (f₁ / f₂) g s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommGroup α<VAR>OrderedCommGroup β<VAR>s : Set ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : MonovaryOn f g s<VAR>n : ℕ<GOAL>MonovaryOn (f ^ n) g s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>OrderedAddCommGroup β<VAR>s : Set ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : MonovaryOn f g s<VAR>n : ℕ<GOAL>MonovaryOn (n • f) g s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>OrderedAddCommGroup β<VAR>s : Set ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : AntivaryOn f g s<VAR>n : ℕ<GOAL>AntivaryOn (n • f) g s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommGroup α<VAR>OrderedCommGroup β<VAR>s : Set ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : AntivaryOn f g s<VAR>n : ℕ<GOAL>AntivaryOn (f ^ n) g s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommGroup α<VAR>OrderedCommGroup β<VAR>f₁ f₂ : ι → α<VAR>g : ι → β<VAR>h₁ : Monovary f₁ g<VAR>h₂ : Monovary f₂ g<GOAL>Monovary (f₁ * f₂) g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>OrderedAddCommGroup β<VAR>f₁ f₂ : ι → α<VAR>g : ι → β<VAR>h₁ : Monovary f₁ g<VAR>h₂ : Monovary f₂ g<GOAL>Monovary (f₁ + f₂) g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommGroup α<VAR>OrderedCommGroup β<VAR>f₁ f₂ : ι → α<VAR>g : ι → β<VAR>h₁ : Antivary f₁ g<VAR>h₂ : Antivary f₂ g<GOAL>Antivary (f₁ * f₂) g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>OrderedAddCommGroup β<VAR>f₁ f₂ : ι → α<VAR>g : ι → β<VAR>h₁ : Antivary f₁ g<VAR>h₂ : Antivary f₂ g<GOAL>Antivary (f₁ + f₂) g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommGroup α<VAR>OrderedCommGroup β<VAR>f₁ f₂ : ι → α<VAR>g : ι → β<VAR>h₁ : Monovary f₁ g<VAR>h₂ : Antivary f₂ g<GOAL>Monovary (f₁ / f₂) g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>OrderedAddCommGroup β<VAR>f₁ f₂ : ι → α<VAR>g : ι → β<VAR>h₁ : Monovary f₁ g<VAR>h₂ : Antivary f₂ g<GOAL>Monovary (f₁ - f₂) g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>OrderedAddCommGroup β<VAR>f₁ f₂ : ι → α<VAR>g : ι → β<VAR>h₁ : Antivary f₁ g<VAR>h₂ : Monovary f₂ g<GOAL>Antivary (f₁ - f₂) g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommGroup α<VAR>OrderedCommGroup β<VAR>f₁ f₂ : ι → α<VAR>g : ι → β<VAR>h₁ : Antivary f₁ g<VAR>h₂ : Monovary f₂ g<GOAL>Antivary (f₁ / f₂) g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>OrderedAddCommGroup β<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : Monovary f g<VAR>n : ℕ<GOAL>Monovary (n • f) g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommGroup α<VAR>OrderedCommGroup β<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : Monovary f g<VAR>n : ℕ<GOAL>Monovary (f ^ n) g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommGroup α<VAR>OrderedCommGroup β<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : Antivary f g<VAR>n : ℕ<GOAL>Antivary (f ^ n) g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>OrderedAddCommGroup β<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : Antivary f g<VAR>n : ℕ<GOAL>Antivary (n • f) g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>LinearOrderedAddCommGroup β<VAR>s : Set ι<VAR>f : ι → α<VAR>g₁ g₂ : ι → β<VAR>h₁ : MonovaryOn f g₁ s<VAR>h₂ : MonovaryOn f g₂ s<GOAL>MonovaryOn f (g₁ + g₂) s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommGroup α<VAR>LinearOrderedCommGroup β<VAR>s : Set ι<VAR>f : ι → α<VAR>g₁ g₂ : ι → β<VAR>h₁ : MonovaryOn f g₁ s<VAR>h₂ : MonovaryOn f g₂ s<GOAL>MonovaryOn f (g₁ * g₂) s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommGroup α<VAR>LinearOrderedCommGroup β<VAR>s : Set ι<VAR>f : ι → α<VAR>g₁ g₂ : ι → β<VAR>h₁ : AntivaryOn f g₁ s<VAR>h₂ : AntivaryOn f g₂ s<GOAL>AntivaryOn f (g₁ * g₂) s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>LinearOrderedAddCommGroup β<VAR>s : Set ι<VAR>f : ι → α<VAR>g₁ g₂ : ι → β<VAR>h₁ : AntivaryOn f g₁ s<VAR>h₂ : AntivaryOn f g₂ s<GOAL>AntivaryOn f (g₁ + g₂) s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommGroup α<VAR>LinearOrderedCommGroup β<VAR>s : Set ι<VAR>f : ι → α<VAR>g₁ g₂ : ι → β<VAR>h₁ : MonovaryOn f g₁ s<VAR>h₂ : AntivaryOn f g₂ s<GOAL>MonovaryOn f (g₁ / g₂) s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>LinearOrderedAddCommGroup β<VAR>s : Set ι<VAR>f : ι → α<VAR>g₁ g₂ : ι → β<VAR>h₁ : MonovaryOn f g₁ s<VAR>h₂ : AntivaryOn f g₂ s<GOAL>MonovaryOn f (g₁ - g₂) s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommGroup α<VAR>LinearOrderedCommGroup β<VAR>s : Set ι<VAR>f : ι → α<VAR>g₁ g₂ : ι → β<VAR>h₁ : AntivaryOn f g₁ s<VAR>h₂ : MonovaryOn f g₂ s<GOAL>AntivaryOn f (g₁ / g₂) s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>LinearOrderedAddCommGroup β<VAR>s : Set ι<VAR>f : ι → α<VAR>g₁ g₂ : ι → β<VAR>h₁ : AntivaryOn f g₁ s<VAR>h₂ : MonovaryOn f g₂ s<GOAL>AntivaryOn f (g₁ - g₂) s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>LinearOrderedAddCommGroup β<VAR>s : Set ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : MonovaryOn f g s<VAR>n : ℕ<GOAL>MonovaryOn f (n • g) s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommGroup α<VAR>LinearOrderedCommGroup β<VAR>s : Set ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : MonovaryOn f g s<VAR>n : ℕ<GOAL>MonovaryOn f (g ^ n) s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommGroup α<VAR>LinearOrderedCommGroup β<VAR>s : Set ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : AntivaryOn f g s<VAR>n : ℕ<GOAL>AntivaryOn f (g ^ n) s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>LinearOrderedAddCommGroup β<VAR>s : Set ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : AntivaryOn f g s<VAR>n : ℕ<GOAL>AntivaryOn f (n • g) s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommGroup α<VAR>LinearOrderedCommGroup β<VAR>f : ι → α<VAR>g₁ g₂ : ι → β<VAR>h₁ : Monovary f g₁<VAR>h₂ : Monovary f g₂<GOAL>Monovary f (g₁ * g₂)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>LinearOrderedAddCommGroup β<VAR>f : ι → α<VAR>g₁ g₂ : ι → β<VAR>h₁ : Monovary f g₁<VAR>h₂ : Monovary f g₂<GOAL>Monovary f (g₁ + g₂)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommGroup α<VAR>LinearOrderedCommGroup β<VAR>f : ι → α<VAR>g₁ g₂ : ι → β<VAR>h₁ : Antivary f g₁<VAR>h₂ : Antivary f g₂<GOAL>Antivary f (g₁ * g₂)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>LinearOrderedAddCommGroup β<VAR>f : ι → α<VAR>g₁ g₂ : ι → β<VAR>h₁ : Antivary f g₁<VAR>h₂ : Antivary f g₂<GOAL>Antivary f (g₁ + g₂)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>LinearOrderedAddCommGroup β<VAR>f : ι → α<VAR>g₁ g₂ : ι → β<VAR>h₁ : Monovary f g₁<VAR>h₂ : Antivary f g₂<GOAL>Monovary f (g₁ - g₂)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommGroup α<VAR>LinearOrderedCommGroup β<VAR>f : ι → α<VAR>g₁ g₂ : ι → β<VAR>h₁ : Monovary f g₁<VAR>h₂ : Antivary f g₂<GOAL>Monovary f (g₁ / g₂)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommGroup α<VAR>LinearOrderedCommGroup β<VAR>f : ι → α<VAR>g₁ g₂ : ι → β<VAR>h₁ : Antivary f g₁<VAR>h₂ : Monovary f g₂<GOAL>Antivary f (g₁ / g₂)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>LinearOrderedAddCommGroup β<VAR>f : ι → α<VAR>g₁ g₂ : ι → β<VAR>h₁ : Antivary f g₁<VAR>h₂ : Monovary f g₂<GOAL>Antivary f (g₁ - g₂)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>LinearOrderedAddCommGroup β<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : Monovary f g<VAR>n : ℕ<GOAL>Monovary f (n • g)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommGroup α<VAR>LinearOrderedCommGroup β<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : Monovary f g<VAR>n : ℕ<GOAL>Monovary f (g ^ n)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedCommGroup α<VAR>LinearOrderedCommGroup β<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : Antivary f g<VAR>n : ℕ<GOAL>Antivary f (g ^ n)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommGroup α<VAR>LinearOrderedAddCommGroup β<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : Antivary f g<VAR>n : ℕ<GOAL>Antivary f (n • g)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedSemiring α<VAR>OrderedSemiring β<VAR>s : Set ι<VAR>f₁ f₂ : ι → α<VAR>g : ι → β<VAR>hf₁ : ∀ i ∈ s, 0 ≤ f₁ i<VAR>hf₂ : ∀ i ∈ s, 0 ≤ f₂ i<VAR>h₁ : MonovaryOn f₁ g s<VAR>h₂ : MonovaryOn f₂ g s<GOAL>MonovaryOn (f₁ * f₂) g s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedSemiring α<VAR>OrderedSemiring β<VAR>s : Set ι<VAR>f₁ f₂ : ι → α<VAR>g : ι → β<VAR>hf₁ : ∀ i ∈ s, 0 ≤ f₁ i<VAR>hf₂ : ∀ i ∈ s, 0 ≤ f₂ i<VAR>h₁ : AntivaryOn f₁ g s<VAR>h₂ : AntivaryOn f₂ g s<GOAL>AntivaryOn (f₁ * f₂) g s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedSemiring α<VAR>OrderedSemiring β<VAR>s : Set ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hf : ∀ i ∈ s, 0 ≤ f i<VAR>hfg : MonovaryOn f g s<VAR>n : ℕ<GOAL>MonovaryOn (f ^ n) g s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedSemiring α<VAR>OrderedSemiring β<VAR>s : Set ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hf : ∀ i ∈ s, 0 ≤ f i<VAR>hfg : AntivaryOn f g s<VAR>n : ℕ<GOAL>AntivaryOn (f ^ n) g s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedSemiring α<VAR>OrderedSemiring β<VAR>f₁ f₂ : ι → α<VAR>g : ι → β<VAR>hf₁ : 0 ≤ f₁<VAR>hf₂ : 0 ≤ f₂<VAR>h₁ : Monovary f₁ g<VAR>h₂ : Monovary f₂ g<GOAL>Monovary (f₁ * f₂) g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedSemiring α<VAR>OrderedSemiring β<VAR>f₁ f₂ : ι → α<VAR>g : ι → β<VAR>hf₁ : 0 ≤ f₁<VAR>hf₂ : 0 ≤ f₂<VAR>h₁ : Antivary f₁ g<VAR>h₂ : Antivary f₂ g<GOAL>Antivary (f₁ * f₂) g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedSemiring α<VAR>OrderedSemiring β<VAR>f : ι → α<VAR>g : ι → β<VAR>hf : 0 ≤ f<VAR>hfg : Monovary f g<VAR>n : ℕ<GOAL>Monovary (f ^ n) g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedSemiring α<VAR>OrderedSemiring β<VAR>f : ι → α<VAR>g : ι → β<VAR>hf : 0 ≤ f<VAR>hfg : Antivary f g<VAR>n : ℕ<GOAL>Antivary (f ^ n) g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedSemiring α<VAR>LinearOrderedSemiring β<VAR>s : Set ι<VAR>f : ι → α<VAR>g₁ g₂ : ι → β<VAR>hg₁ : ∀ i ∈ s, 0 ≤ g₁ i<VAR>hg₂ : ∀ i ∈ s, 0 ≤ g₂ i<VAR>h₁ : MonovaryOn f g₁ s<VAR>h₂ : MonovaryOn f g₂ s<GOAL>MonovaryOn f (g₁ * g₂) s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedSemiring α<VAR>LinearOrderedSemiring β<VAR>s : Set ι<VAR>f : ι → α<VAR>g₁ g₂ : ι → β<VAR>hg₁ : ∀ i ∈ s, 0 ≤ g₁ i<VAR>hg₂ : ∀ i ∈ s, 0 ≤ g₂ i<VAR>h₁ : AntivaryOn f g₁ s<VAR>h₂ : AntivaryOn f g₂ s<GOAL>AntivaryOn f (g₁ * g₂) s