ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>s : Finset ι<VAR>σ : Equiv.Perm ι<VAR>f g : ι → α<VAR>hfg : AntivaryOn f g ↑s<VAR>hσ : {x | σ x ≠ x} ⊆ ↑s<GOAL>∑ i ∈ s, f i * g i < ∑ i ∈ s, f i * g (σ i) ↔ ¬AntivaryOn f (g ∘ ⇑σ) ↑s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>s : Finset ι<VAR>σ : Equiv.Perm ι<VAR>f g : ι → α<VAR>hfg : AntivaryOn f g ↑s<VAR>hσ : {x | σ x ≠ x} ⊆ ↑s<GOAL>∑ i ∈ s, f i * g i ≤ ∑ i ∈ s, f (σ i) * g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>s : Finset ι<VAR>σ : Equiv.Perm ι<VAR>f g : ι → α<VAR>hfg : AntivaryOn f g ↑s<VAR>hσ : {x | σ x ≠ x} ⊆ ↑s<GOAL>∑ i ∈ s, f (σ i) * g i = ∑ i ∈ s, f i * g i ↔ AntivaryOn (f ∘ ⇑σ) g ↑s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>s : Finset ι<VAR>σ : Equiv.Perm ι<VAR>f g : ι → α<VAR>hfg : AntivaryOn f g ↑s<VAR>hσ : {x | σ x ≠ x} ⊆ ↑s<GOAL>∑ i ∈ s, f i * g i < ∑ i ∈ s, f (σ i) * g i ↔ ¬AntivaryOn (f ∘ ⇑σ) g ↑s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>σ : Equiv.Perm ι<VAR>f g : ι → α<VAR>Fintype ι<VAR>hfg : Monovary f g<GOAL>∑ i : ι, f i * g (σ i) ≤ ∑ i : ι, f i * g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>σ : Equiv.Perm ι<VAR>f g : ι → α<VAR>Fintype ι<VAR>hfg : Monovary f g<GOAL>∑ i : ι, f i * g (σ i) = ∑ i : ι, f i * g i ↔ Monovary f (g ∘ ⇑σ)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>σ : Equiv.Perm ι<VAR>f g : ι → α<VAR>Fintype ι<VAR>hfg : Monovary f g<GOAL>∑ i : ι, f i * g (σ i) < ∑ i : ι, f i * g i ↔ ¬Monovary f (g ∘ ⇑σ)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>σ : Equiv.Perm ι<VAR>f g : ι → α<VAR>Fintype ι<VAR>hfg : Monovary f g<GOAL>∑ i : ι, f (σ i) * g i ≤ ∑ i : ι, f i * g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>σ : Equiv.Perm ι<VAR>f g : ι → α<VAR>Fintype ι<VAR>hfg : Monovary f g<GOAL>∑ i : ι, f (σ i) * g i = ∑ i : ι, f i * g i ↔ Monovary (f ∘ ⇑σ) g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>σ : Equiv.Perm ι<VAR>f g : ι → α<VAR>Fintype ι<VAR>hfg : Monovary f g<GOAL>∑ i : ι, f (σ i) * g i < ∑ i : ι, f i * g i ↔ ¬Monovary (f ∘ ⇑σ) g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>σ : Equiv.Perm ι<VAR>f g : ι → α<VAR>Fintype ι<VAR>hfg : Antivary f g<GOAL>∑ i : ι, f i * g i ≤ ∑ i : ι, f i * g (σ i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>σ : Equiv.Perm ι<VAR>f g : ι → α<VAR>Fintype ι<VAR>hfg : Antivary f g<GOAL>∑ i : ι, f i * g (σ i) = ∑ i : ι, f i * g i ↔ Antivary f (g ∘ ⇑σ)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>σ : Equiv.Perm ι<VAR>f g : ι → α<VAR>Fintype ι<VAR>hfg : Antivary f g<GOAL>∑ i : ι, f i • g i < ∑ i : ι, f i • g (σ i) ↔ ¬Antivary f (g ∘ ⇑σ)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>σ : Equiv.Perm ι<VAR>f g : ι → α<VAR>Fintype ι<VAR>hfg : Antivary f g<GOAL>∑ i : ι, f i * g i ≤ ∑ i : ι, f (σ i) * g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>σ : Equiv.Perm ι<VAR>f g : ι → α<VAR>Fintype ι<VAR>hfg : Antivary f g<GOAL>∑ i : ι, f (σ i) * g i = ∑ i : ι, f i * g i ↔ Antivary (f ∘ ⇑σ) g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>σ : Equiv.Perm ι<VAR>f g : ι → α<VAR>Fintype ι<VAR>hfg : Antivary f g<GOAL>∑ i : ι, f i * g i < ∑ i : ι, f (σ i) * g i ↔ ¬Antivary (f ∘ ⇑σ) g
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>A : ι → Type u_2<VAR>(i : ι) → SMul α (A i)<VAR>a : α<VAR>x : GradedMonoid A<GOAL>(a • x).fst = x.fst
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>A : ι → Type u_2<VAR>(i : ι) → SMul α (A i)<VAR>a : α<VAR>x : GradedMonoid A<GOAL>(a • x).snd = a • x.snd
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>A : ι → Type u_2<VAR>(i : ι) → SMul α (A i)<VAR>i : ι<VAR>c : α<VAR>a : A i<GOAL>c • GradedMonoid.mk i a = GradedMonoid.mk i (c • a)
<VAR>ι : Type u_1<VAR>A : ι → Type u_2<VAR>Zero ι<VAR>GradedMonoid.GOne A<GOAL>Sigma.fst 1 = 0
<VAR>ι : Type u_1<VAR>A : ι → Type u_2<VAR>Zero ι<VAR>GradedMonoid.GOne A<GOAL>Sigma.snd 1 = GradedMonoid.GOne.one
<VAR>ι : Type u_1<VAR>A : ι → Type u_2<VAR>Add ι<VAR>GradedMonoid.GMul A<VAR>x y : GradedMonoid A<GOAL>(x * y).fst = x.fst + y.fst
<VAR>ι : Type u_1<VAR>A : ι → Type u_2<VAR>Add ι<VAR>GradedMonoid.GMul A<VAR>x y : GradedMonoid A<GOAL>(x * y).snd = GradedMonoid.GMul.mul x.snd y.snd
<VAR>ι : Type u_1<VAR>A : ι → Type u_2<VAR>Add ι<VAR>GradedMonoid.GMul A<VAR>i j : ι<VAR>a : A i<VAR>b : A j<GOAL>GradedMonoid.mk i a * GradedMonoid.mk j b = GradedMonoid.mk (i + j) (GradedMonoid.GMul.mul a b)
<VAR>ι : Type u_1<VAR>A : ι → Type u_2<VAR>AddMonoid ι<VAR>GradedMonoid.GMul A<VAR>GradedMonoid.GOne A<VAR>a : GradedMonoid A<GOAL>GradedMonoid.mk (0 • a.fst) (GradedMonoid.GMonoid.gnpowRec 0 a.snd) = 1
<VAR>ι : Type u_1<VAR>A : ι → Type u_2<VAR>AddMonoid ι<VAR>GradedMonoid.GMul A<VAR>GradedMonoid.GOne A<VAR>n : ℕ<VAR>a : GradedMonoid A<GOAL>GradedMonoid.mk (n.succ • a.fst) (GradedMonoid.GMonoid.gnpowRec n.succ a.snd) = ⟨n • a.fst, GradedMonoid.GMonoid.gnpowRec n a.snd⟩ * a
<VAR>ι : Type u_1<VAR>A : ι → Type u_2<VAR>AddMonoid ι<VAR>self : GradedMonoid.GMonoid A<VAR>n : ℕ<VAR>a : GradedMonoid A<GOAL>GradedMonoid.mk (n.succ • a.fst) (GradedMonoid.GMonoid.gnpow n.succ a.snd) = ⟨n • a.fst, GradedMonoid.GMonoid.gnpow n a.snd⟩ * a
<VAR>ι : Type u_1<VAR>A : ι → Type u_2<VAR>AddMonoid ι<VAR>self : GradedMonoid.GMonoid A<VAR>a b c : GradedMonoid A<GOAL>a * b * c = a * (b * c)
<VAR>ι : Type u_1<VAR>A : ι → Type u_2<VAR>AddMonoid ι<VAR>self : GradedMonoid.GMonoid A<VAR>a : GradedMonoid A<GOAL>a * 1 = a
<VAR>ι : Type u_1<VAR>A : ι → Type u_2<VAR>AddMonoid ι<VAR>self : GradedMonoid.GMonoid A<VAR>a : GradedMonoid A<GOAL>1 * a = a
<VAR>ι : Type u_1<VAR>A : ι → Type u_2<VAR>AddMonoid ι<VAR>self : GradedMonoid.GMonoid A<VAR>a : GradedMonoid A<GOAL>GradedMonoid.mk (0 • a.fst) (GradedMonoid.GMonoid.gnpow 0 a.snd) = 1
<VAR>ι : Type u_1<VAR>A : ι → Type u_2<VAR>AddMonoid ι<VAR>GradedMonoid.GMonoid A<VAR>x : GradedMonoid A<VAR>n : ℕ<GOAL>(x ^ n).fst = n • x.fst
<VAR>ι : Type u_1<VAR>A : ι → Type u_2<VAR>AddMonoid ι<VAR>GradedMonoid.GMonoid A<VAR>x : GradedMonoid A<VAR>n : ℕ<GOAL>(x ^ n).snd = GradedMonoid.GMonoid.gnpow n x.snd
<VAR>ι : Type u_1<VAR>A : ι → Type u_2<VAR>AddMonoid ι<VAR>GradedMonoid.GMonoid A<VAR>i : ι<VAR>a : A i<VAR>n : ℕ<GOAL>GradedMonoid.mk i a ^ n = GradedMonoid.mk (n • i) (GradedMonoid.GMonoid.gnpow n a)
<VAR>ι : Type u_1<VAR>A : ι → Type u_2<VAR>AddCommMonoid ι<VAR>self : GradedMonoid.GCommMonoid A<VAR>a b : GradedMonoid A<GOAL>a * b = b * a
<VAR>ι : Type u_1<VAR>A : ι → Type u_2<VAR>AddZeroClass ι<VAR>GradedMonoid.GMul A<VAR>i : ι<VAR>a : A 0<VAR>b : A i<GOAL>GradedMonoid.mk i (a • b) = GradedMonoid.mk 0 a * GradedMonoid.mk i b
<VAR>ι : Type u_1<VAR>A : ι → Type u_2<VAR>AddZeroClass ι<VAR>GradedMonoid.GMul A<VAR>a b : A 0<GOAL>a • b = a * b
<VAR>ι : Type u_1<VAR>A : ι → Type u_2<VAR>AddMonoid ι<VAR>GradedMonoid.GMonoid A<VAR>a : A 0<VAR>n : ℕ<GOAL>GradedMonoid.mk 0 (a ^ n) = GradedMonoid.mk 0 a ^ n
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>AddMonoid ι<VAR>fι : α → ι<GOAL>[].dProdIndex fι = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>AddMonoid ι<VAR>a : α<VAR>l : List α<VAR>fι : α → ι<GOAL>(a :: l).dProdIndex fι = fι a + l.dProdIndex fι
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>AddMonoid ι<VAR>l : List α<VAR>fι : α → ι<GOAL>l.dProdIndex fι = (List.map fι l).sum
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>A : ι → Type u_3<VAR>AddMonoid ι<VAR>GradedMonoid.GMonoid A<VAR>fι : α → ι<VAR>fA : (a : α) → A (fι a)<GOAL>[].dProd fι fA = GradedMonoid.GOne.one
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>A : ι → Type u_3<VAR>AddMonoid ι<VAR>GradedMonoid.GMonoid A<VAR>fι : α → ι<VAR>fA : (a : α) → A (fι a)<VAR>a : α<VAR>l : List α<GOAL>(a :: l).dProd fι fA = GradedMonoid.GMul.mul (fA a) (l.dProd fι fA)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>A : ι → Type u_3<VAR>AddMonoid ι<VAR>GradedMonoid.GMonoid A<VAR>l : List α<VAR>fι : α → ι<VAR>fA : (a : α) → A (fι a)<GOAL>GradedMonoid.mk (l.dProdIndex fι) (l.dProd fι fA) = (List.map (fun a => GradedMonoid.mk (fι a) (fA a)) l).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>A : ι → Type u_3<VAR>AddMonoid ι<VAR>GradedMonoid.GMonoid A<VAR>l : List α<VAR>f : α → GradedMonoid A<GOAL>(List.map f l).prod = GradedMonoid.mk (l.dProdIndex fun i => (f i).fst) (l.dProd (fun i => (f i).fst) fun i => (f i).snd)
<VAR>ι : Type u_1<VAR>A : ι → Type u_3<VAR>AddMonoid ι<VAR>GradedMonoid.GMonoid A<VAR>n : ℕ<VAR>f : Fin n → GradedMonoid A<GOAL>(List.ofFn f).prod = GradedMonoid.mk ((List.finRange n).dProdIndex fun i => (f i).fst) ((List.finRange n).dProd (fun i => (f i).fst) fun i => (f i).snd)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>Zero ι<VAR>One R<GOAL>GradedMonoid.GOne.one = 1
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>Add ι<VAR>Mul R<GOAL>∀ {i j : ι} (x y : R), GradedMonoid.GMul.mul x y = x * y
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>AddMonoid ι<VAR>Monoid R<VAR>n : ℕ<GOAL>∀ (x : ι) (a : R), GradedMonoid.GMonoid.gnpow n a = a ^ n
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>α : Type u_3<VAR>AddMonoid ι<VAR>Monoid R<VAR>l : List α<VAR>fι : α → ι<VAR>fA : α → R<GOAL>l.dProd fι fA = (List.map fA l).prod
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>SetLike S R<VAR>One R<VAR>Zero ι<VAR>A : ι → S<VAR>self : SetLike.GradedOne A<GOAL>1 ∈ A 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>SetLike S R<VAR>One R<VAR>Zero ι<VAR>A : ι → S<VAR>SetLike.GradedOne A<GOAL>1 ∈ A 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>SetLike S R<VAR>One R<VAR>Zero ι<VAR>A : ι → S<VAR>SetLike.GradedOne A<GOAL>↑GradedMonoid.GOne.one = 1
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>SetLike S R<VAR>Mul R<VAR>Add ι<VAR>A : ι → S<VAR>self : SetLike.GradedMul A<VAR>i j : ι<VAR>gi gj : R<GOAL>gi ∈ A i → gj ∈ A j → gi * gj ∈ A (i + j)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>SetLike S R<VAR>Mul R<VAR>Add ι<VAR>A : ι → S<VAR>SetLike.GradedMul A<VAR>i j : ι<VAR>gi gj : R<VAR>hi : gi ∈ A i<VAR>hj : gj ∈ A j<GOAL>gi * gj ∈ A (i + j)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>SetLike S R<VAR>Mul R<VAR>Add ι<VAR>A : ι → S<VAR>SetLike.GradedMul A<VAR>i j : ι<VAR>x : ↥(A i)<VAR>y : ↥(A j)<GOAL>↑(GradedMonoid.GMul.mul x y) = ↑x * ↑y
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>SetLike S R<VAR>Monoid R<VAR>AddMonoid ι<VAR>A : ι → S<VAR>SetLike.GradedMonoid A<GOAL>↑(SetLike.GradeZero.submonoid A) = ↑(A 0)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>SetLike S R<VAR>Monoid R<VAR>AddMonoid ι<VAR>A : ι → S<VAR>SetLike.GradedMonoid A<GOAL>↑1 = 1
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>SetLike S R<VAR>Monoid R<VAR>AddMonoid ι<VAR>A : ι → S<VAR>SetLike.GradedMonoid A<VAR>a b : ↥(A 0)<GOAL>↑(a * b) = ↑a * ↑b
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>SetLike S R<VAR>Monoid R<VAR>AddMonoid ι<VAR>A : ι → S<VAR>SetLike.GradedMonoid A<VAR>a : ↥(A 0)<VAR>n : ℕ<GOAL>↑(a ^ n) = ↑a ^ n
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>SetLike S R<VAR>Monoid R<VAR>AddMonoid ι<VAR>A : ι → S<VAR>SetLike.GradedMonoid A<VAR>n : ℕ<VAR>r : R<VAR>i : ι<VAR>h : r ∈ A i<GOAL>r ^ n ∈ A (n • i)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>SetLike S R<VAR>Monoid R<VAR>AddMonoid ι<VAR>A : ι → S<VAR>SetLike.GradedMonoid A<VAR>ι' : Type u_4<VAR>l : List ι'<VAR>i : ι' → ι<VAR>r : ι' → R<VAR>h : ∀ j ∈ l, r j ∈ A (i j)<GOAL>(List.map r l).prod ∈ A (List.map i l).sum
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>SetLike S R<VAR>Monoid R<VAR>AddMonoid ι<VAR>A : ι → S<VAR>SetLike.GradedMonoid A<VAR>n : ℕ<VAR>i : Fin n → ι<VAR>r : Fin n → R<VAR>h : ∀ (j : Fin n), r j ∈ A (i j)<GOAL>(List.ofFn r).prod ∈ A (List.ofFn i).sum
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>SetLike S R<VAR>Monoid R<VAR>AddMonoid ι<VAR>A : ι → S<VAR>SetLike.GradedMonoid A<VAR>i : ι<VAR>x : ↥(A i)<VAR>n : ℕ<GOAL>↑(GradedMonoid.GMonoid.gnpow n x) = ↑x ^ n
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>α : Type u_3<VAR>S : Type u_4<VAR>SetLike S R<VAR>Monoid R<VAR>AddMonoid ι<VAR>A : ι → S<VAR>SetLike.GradedMonoid A<VAR>fι : α → ι<VAR>fA : (a : α) → ↥(A (fι a))<VAR>l : List α<GOAL>↑(l.dProd fι fA) = (List.map (fun a => ↑(fA a)) l).prod
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>α : Type u_3<VAR>S : Type u_4<VAR>SetLike S R<VAR>Monoid R<VAR>AddMonoid ι<VAR>A : ι → S<VAR>SetLike.GradedMonoid A<VAR>fι : α → ι<VAR>fA : (a : α) → ↥(A (fι a))<VAR>l : List α<GOAL>l.dProd fι fA = ⟨(List.map (fun a => ↑(fA a)) l).prod, ⋯⟩
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>SetLike S R<VAR>A : ι → S<VAR>i : ι<VAR>x : ↥(A i)<GOAL>SetLike.Homogeneous A ↑x
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>SetLike S R<VAR>Zero ι<VAR>One R<VAR>A : ι → S<VAR>SetLike.GradedOne A<GOAL>SetLike.Homogeneous A 1
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>SetLike S R<VAR>Add ι<VAR>Mul R<VAR>A : ι → S<VAR>SetLike.GradedMul A<VAR>a b : R<GOAL>SetLike.Homogeneous A a → SetLike.Homogeneous A b → SetLike.Homogeneous A (a * b)
<VAR>α : Type u<VAR>LE α<VAR>Semiring α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>a1 : 1 ≤ a<GOAL>a + 1 ≤ 2 * a
<VAR>α : Type u<VAR>Semiring α<VAR>Preorder α<VAR>a : α<VAR>ZeroLEOneClass α<VAR>PosMulMono α<VAR>H : 0 ≤ a<VAR>n : ℕ<GOAL>0 ≤ a ^ n
<VAR>α : Type u<VAR>Semiring α<VAR>Preorder α<VAR>a : α<VAR>ZeroLEOneClass α<VAR>PosMulMono α<VAR>MulPosMono α<VAR>ha₀ : 0 ≤ a<VAR>ha₁ : a ≤ 1<VAR>m n : ℕ<GOAL>m ≤ n → a ^ n ≤ a ^ m
<VAR>α : Type u<VAR>Semiring α<VAR>Preorder α<VAR>a : α<VAR>ZeroLEOneClass α<VAR>PosMulMono α<VAR>MulPosMono α<VAR>h₀ : 0 ≤ a<VAR>h₁ : a ≤ 1<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>a ^ n ≤ a
<VAR>α : Type u<VAR>Semiring α<VAR>Preorder α<VAR>a : α<VAR>ZeroLEOneClass α<VAR>PosMulMono α<VAR>MulPosMono α<VAR>h₀ : 0 ≤ a<VAR>h₁ : a ≤ 1<GOAL>a ^ 2 ≤ a
<VAR>α : Type u<VAR>Semiring α<VAR>Preorder α<VAR>a b : α<VAR>ZeroLEOneClass α<VAR>MulPosMono α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a2 : 2 ≤ a<VAR>b0 : 0 ≤ b<GOAL>a + (2 + b) ≤ a * (2 + b)
<VAR>α : Type u<VAR>Semiring α<VAR>Preorder α<VAR>a b : α<VAR>ZeroLEOneClass α<VAR>PosMulMono α<VAR>ha : 1 ≤ a<VAR>hb : 1 ≤ b<GOAL>1 ≤ a * b
<VAR>α : Type u<VAR>Semiring α<VAR>Preorder α<VAR>a : α<VAR>PosMulMono α<VAR>ha : 0 ≤ a<GOAL>Monotone fun x => a * x
<VAR>α : Type u<VAR>Semiring α<VAR>Preorder α<VAR>a : α<VAR>MulPosMono α<VAR>ha : 0 ≤ a<GOAL>Monotone fun x => x * a
<VAR>α : Type u<VAR>β : Type u_1<VAR>Semiring α<VAR>Preorder α<VAR>a : α<VAR>Preorder β<VAR>f : β → α<VAR>MulPosMono α<VAR>hf : Monotone f<VAR>ha : 0 ≤ a<GOAL>Monotone fun x => f x * a
<VAR>α : Type u<VAR>β : Type u_1<VAR>Semiring α<VAR>Preorder α<VAR>a : α<VAR>Preorder β<VAR>f : β → α<VAR>PosMulMono α<VAR>hf : Monotone f<VAR>ha : 0 ≤ a<GOAL>Monotone fun x => a * f x
<VAR>α : Type u<VAR>β : Type u_1<VAR>Semiring α<VAR>Preorder α<VAR>a : α<VAR>Preorder β<VAR>f : β → α<VAR>MulPosMono α<VAR>hf : Antitone f<VAR>ha : 0 ≤ a<GOAL>Antitone fun x => f x * a
<VAR>α : Type u<VAR>β : Type u_1<VAR>Semiring α<VAR>Preorder α<VAR>a : α<VAR>Preorder β<VAR>f : β → α<VAR>PosMulMono α<VAR>hf : Antitone f<VAR>ha : 0 ≤ a<GOAL>Antitone fun x => a * f x
<VAR>α : Type u<VAR>β : Type u_1<VAR>Semiring α<VAR>Preorder α<VAR>Preorder β<VAR>f g : β → α<VAR>PosMulMono α<VAR>MulPosMono α<VAR>hf : Monotone f<VAR>hg : Monotone g<VAR>hf₀ : ∀ (x : β), 0 ≤ f x<VAR>hg₀ : ∀ (x : β), 0 ≤ g x<GOAL>Monotone (f * g)
<VAR>α : Type u<VAR>Semiring α<VAR>Preorder α<VAR>a b : α<VAR>ZeroLEOneClass α<VAR>PosMulMono α<VAR>MulPosMono α<VAR>ha : a ≤ 1<VAR>hb' : 0 ≤ b<VAR>hb : b ≤ 1<GOAL>a * b ≤ 1
<VAR>α : Type u<VAR>Semiring α<VAR>Preorder α<VAR>a b : α<VAR>ZeroLEOneClass α<VAR>MulPosMono α<VAR>ha : 1 ≤ a<VAR>hb : 1 < b<GOAL>1 < a * b
<VAR>α : Type u<VAR>Semiring α<VAR>Preorder α<VAR>a b : α<VAR>ZeroLEOneClass α<VAR>PosMulMono α<VAR>ha : 1 < a<VAR>hb : 1 ≤ b<GOAL>1 < a * b
<VAR>α : Type u<VAR>Semiring α<VAR>Preorder α<VAR>a b : α<VAR>PosMulMono α<VAR>ha₀ : 0 ≤ a<VAR>ha : a < 1<VAR>hb : b ≤ 1<GOAL>a * b < 1
<VAR>α : Type u<VAR>Semiring α<VAR>Preorder α<VAR>a b : α<VAR>MulPosMono α<VAR>ha : a ≤ 1<VAR>hb₀ : 0 ≤ b<VAR>hb : b < 1<GOAL>a * b < 1
<VAR>α : Type u<VAR>Semiring α<VAR>Preorder α<VAR>a b c : α<VAR>ExistsAddOfLE α<VAR>PosMulMono α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : b ≤ a<VAR>hc : c ≤ 0<GOAL>c * a ≤ c * b
<VAR>α : Type u<VAR>Semiring α<VAR>Preorder α<VAR>a b c : α<VAR>ExistsAddOfLE α<VAR>MulPosMono α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : b ≤ a<VAR>hc : c ≤ 0<GOAL>a * c ≤ b * c
<VAR>α : Type u<VAR>Semiring α<VAR>Preorder α<VAR>a b : α<VAR>ExistsAddOfLE α<VAR>MulPosMono α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ha : a ≤ 0<VAR>hb : b ≤ 0<GOAL>0 ≤ a * b
<VAR>α : Type u<VAR>Semiring α<VAR>Preorder α<VAR>a b c d : α<VAR>ExistsAddOfLE α<VAR>MulPosMono α<VAR>PosMulMono α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hca : c ≤ a<VAR>hbd : b ≤ d<VAR>hc : 0 ≤ c<VAR>hb : b ≤ 0<GOAL>a * b ≤ c * d
<VAR>α : Type u<VAR>Semiring α<VAR>Preorder α<VAR>a b c d : α<VAR>ExistsAddOfLE α<VAR>PosMulMono α<VAR>MulPosMono α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hca : c ≤ a<VAR>hbd : b ≤ d<VAR>ha : 0 ≤ a<VAR>hd : d ≤ 0<GOAL>a * b ≤ c * d
<VAR>α : Type u<VAR>Semiring α<VAR>Preorder α<VAR>a b c d : α<VAR>ExistsAddOfLE α<VAR>MulPosMono α<VAR>PosMulMono α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hac : a ≤ c<VAR>hdb : d ≤ b<VAR>hc : c ≤ 0<VAR>hb : 0 ≤ b<GOAL>a * b ≤ c * d
<VAR>α : Type u<VAR>Semiring α<VAR>Preorder α<VAR>a b c d : α<VAR>ExistsAddOfLE α<VAR>MulPosMono α<VAR>PosMulMono α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hca : c ≤ a<VAR>hdb : d ≤ b<VAR>hc : c ≤ 0<VAR>hb : b ≤ 0<GOAL>a * b ≤ c * d
<VAR>α : Type u<VAR>Semiring α<VAR>Preorder α<VAR>a b c d : α<VAR>ExistsAddOfLE α<VAR>PosMulMono α<VAR>MulPosMono α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hca : c ≤ a<VAR>hdb : d ≤ b<VAR>ha : a ≤ 0<VAR>hd : d ≤ 0<GOAL>a * b ≤ c * d
<VAR>α : Type u<VAR>Semiring α<VAR>Preorder α<VAR>a b : α<VAR>ExistsAddOfLE α<VAR>MulPosMono α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hb : b ≤ 0<VAR>h : a ≤ 1<GOAL>b ≤ a * b
<VAR>α : Type u<VAR>Semiring α<VAR>Preorder α<VAR>a b : α<VAR>ExistsAddOfLE α<VAR>MulPosMono α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hb : b ≤ 0<VAR>h : 1 ≤ a<GOAL>a * b ≤ b
<VAR>α : Type u<VAR>Semiring α<VAR>Preorder α<VAR>a b : α<VAR>ExistsAddOfLE α<VAR>PosMulMono α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ha : a ≤ 0<VAR>h : b ≤ 1<GOAL>a ≤ a * b
<VAR>α : Type u<VAR>Semiring α<VAR>Preorder α<VAR>a b : α<VAR>ExistsAddOfLE α<VAR>PosMulMono α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ha : a ≤ 0<VAR>h : 1 ≤ b<GOAL>a * b ≤ a
<VAR>α : Type u<VAR>Semiring α<VAR>Preorder α<VAR>ExistsAddOfLE α<VAR>PosMulMono α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>ha : a ≤ 0<GOAL>Antitone fun x => a * x
<VAR>α : Type u<VAR>Semiring α<VAR>Preorder α<VAR>ExistsAddOfLE α<VAR>MulPosMono α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>ha : a ≤ 0<GOAL>Antitone fun x => x * a
<VAR>α : Type u<VAR>β : Type u_1<VAR>Semiring α<VAR>Preorder α<VAR>a : α<VAR>Preorder β<VAR>f : β → α<VAR>ExistsAddOfLE α<VAR>PosMulMono α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : Monotone f<VAR>ha : a ≤ 0<GOAL>Antitone fun x => a * f x
<VAR>α : Type u<VAR>β : Type u_1<VAR>Semiring α<VAR>Preorder α<VAR>a : α<VAR>Preorder β<VAR>f : β → α<VAR>ExistsAddOfLE α<VAR>MulPosMono α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : Monotone f<VAR>ha : a ≤ 0<GOAL>Antitone fun x => f x * a
<VAR>α : Type u<VAR>β : Type u_1<VAR>Semiring α<VAR>Preorder α<VAR>a : α<VAR>Preorder β<VAR>f : β → α<VAR>ExistsAddOfLE α<VAR>PosMulMono α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : Antitone f<VAR>ha : a ≤ 0<GOAL>Monotone fun x => a * f x
<VAR>α : Type u<VAR>β : Type u_1<VAR>Semiring α<VAR>Preorder α<VAR>a : α<VAR>Preorder β<VAR>f : β → α<VAR>ExistsAddOfLE α<VAR>MulPosMono α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : Antitone f<VAR>ha : a ≤ 0<GOAL>Monotone fun x => f x * a
<VAR>α : Type u<VAR>β : Type u_1<VAR>Semiring α<VAR>Preorder α<VAR>Preorder β<VAR>f g : β → α<VAR>ExistsAddOfLE α<VAR>PosMulMono α<VAR>MulPosMono α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : Antitone f<VAR>hg : Monotone g<VAR>hf₀ : ∀ (x : β), f x ≤ 0<VAR>hg₀ : ∀ (x : β), 0 ≤ g x<GOAL>Antitone (f * g)
<VAR>α : Type u<VAR>β : Type u_1<VAR>Semiring α<VAR>Preorder α<VAR>Preorder β<VAR>f g : β → α<VAR>ExistsAddOfLE α<VAR>PosMulMono α<VAR>MulPosMono α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : Monotone f<VAR>hg : Antitone g<VAR>hf₀ : ∀ (x : β), 0 ≤ f x<VAR>hg₀ : ∀ (x : β), g x ≤ 0<GOAL>Antitone (f * g)
<VAR>α : Type u<VAR>β : Type u_1<VAR>Semiring α<VAR>Preorder α<VAR>Preorder β<VAR>f g : β → α<VAR>ExistsAddOfLE α<VAR>PosMulMono α<VAR>MulPosMono α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : Antitone f<VAR>hg : Antitone g<VAR>hf₀ : ∀ (x : β), f x ≤ 0<VAR>hg₀ : ∀ (x : β), g x ≤ 0<GOAL>Monotone (f * g)
<VAR>α : Type u<VAR>Semiring α<VAR>Preorder α<VAR>ExistsAddOfLE α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a ≤ b ↔ ∃ c, c ≥ 0 ∧ b = a + c
<VAR>α : Type u<VAR>Semiring α<VAR>PartialOrder α<VAR>a : α<VAR>ZeroLEOneClass α<VAR>PosMulStrictMono α<VAR>H : 0 < a<VAR>n : ℕ<GOAL>0 < a ^ n
<VAR>α : Type u<VAR>Semiring α<VAR>PartialOrder α<VAR>a b : α<VAR>PosMulStrictMono α<VAR>MulPosMono α<VAR>h1 : 0 ≤ a<VAR>h2 : a < b<GOAL>a * a < b * b
<VAR>α : Type u<VAR>Semiring α<VAR>PartialOrder α<VAR>PosMulStrictMono α<VAR>MulPosMono α<GOAL>StrictMonoOn (fun x => x * x) {x | 0 ≤ x}
<VAR>α : Type u<VAR>Semiring α<VAR>PartialOrder α<VAR>a b c d : α<VAR>PosMulMono α<VAR>PosMulStrictMono α<VAR>MulPosStrictMono α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>h1 : a < c<VAR>h2 : b < d<VAR>h3 : 0 ≤ a<VAR>h4 : 0 ≤ b<GOAL>a * b < c * d
<VAR>α : Type u<VAR>Semiring α<VAR>PartialOrder α<VAR>a b : α<VAR>MulPosStrictMono α<VAR>hn : 0 < a<VAR>hm : 1 < b<GOAL>a < b * a