ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedSemiring α<VAR>LinearOrderedSemiring β<VAR>s : Set ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hg : ∀ i ∈ s, 0 ≤ g i<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>LinearOrderedSemiring α<VAR>LinearOrderedSemiring β<VAR>s : Set ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hg : ∀ i ∈ s, 0 ≤ g i<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>LinearOrderedSemiring α<VAR>LinearOrderedSemiring β<VAR>f : ι → α<VAR>g₁ g₂ : ι → β<VAR>hg₁ : 0 ≤ g₁<VAR>hg₂ : 0 ≤ 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>LinearOrderedSemiring α<VAR>LinearOrderedSemiring β<VAR>f : ι → α<VAR>g₁ g₂ : ι → β<VAR>hg₁ : 0 ≤ g₁<VAR>hg₂ : 0 ≤ 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>LinearOrderedSemiring α<VAR>LinearOrderedSemiring β<VAR>f : ι → α<VAR>g : ι → β<VAR>hg : 0 ≤ 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>LinearOrderedSemiring α<VAR>LinearOrderedSemiring β<VAR>f : ι → α<VAR>g : ι → β<VAR>hg : 0 ≤ 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>LinearOrderedSemifield α<VAR>LinearOrderedSemifield β<VAR>s : Set ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hf : ∀ i ∈ s, 0 < f i<GOAL>MonovaryOn f⁻¹ g s ↔ AntivaryOn f g s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedSemifield α<VAR>LinearOrderedSemifield β<VAR>s : Set ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hf : ∀ i ∈ s, 0 < f i<GOAL>AntivaryOn f⁻¹ g s ↔ MonovaryOn f g s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedSemifield α<VAR>LinearOrderedSemifield β<VAR>s : Set ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hg : ∀ i ∈ s, 0 < g i<GOAL>MonovaryOn f g⁻¹ s ↔ AntivaryOn f g s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedSemifield α<VAR>LinearOrderedSemifield β<VAR>s : Set ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hg : ∀ i ∈ s, 0 < g i<GOAL>AntivaryOn f g⁻¹ s ↔ MonovaryOn f g s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedSemifield α<VAR>LinearOrderedSemifield β<VAR>s : Set ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hf : ∀ i ∈ s, 0 < f i<VAR>hg : ∀ i ∈ s, 0 < g i<GOAL>MonovaryOn f⁻¹ g⁻¹ s ↔ MonovaryOn f g s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedSemifield α<VAR>LinearOrderedSemifield β<VAR>s : Set ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hf : ∀ i ∈ s, 0 < f i<VAR>hg : ∀ i ∈ s, 0 < g i<GOAL>AntivaryOn f⁻¹ g⁻¹ s ↔ AntivaryOn f g s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedSemifield α<VAR>LinearOrderedSemifield β<VAR>f : ι → α<VAR>g : ι → β<VAR>hf : StrongLT 0 f<GOAL>Monovary f⁻¹ g ↔ Antivary f g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedSemifield α<VAR>LinearOrderedSemifield β<VAR>f : ι → α<VAR>g : ι → β<VAR>hf : StrongLT 0 f<GOAL>Antivary f⁻¹ g ↔ Monovary f g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedSemifield α<VAR>LinearOrderedSemifield β<VAR>f : ι → α<VAR>g : ι → β<VAR>hg : StrongLT 0 g<GOAL>Monovary f g⁻¹ ↔ Antivary f g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedSemifield α<VAR>LinearOrderedSemifield β<VAR>f : ι → α<VAR>g : ι → β<VAR>hg : StrongLT 0 g<GOAL>Antivary f g⁻¹ ↔ Monovary f g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedSemifield α<VAR>LinearOrderedSemifield β<VAR>f : ι → α<VAR>g : ι → β<VAR>hf : StrongLT 0 f<VAR>hg : StrongLT 0 g<GOAL>Monovary f⁻¹ g⁻¹ ↔ Monovary f g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedSemifield α<VAR>LinearOrderedSemifield β<VAR>f : ι → α<VAR>g : ι → β<VAR>hf : StrongLT 0 f<VAR>hg : StrongLT 0 g<GOAL>Antivary f⁻¹ g⁻¹ ↔ Antivary f g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedSemifield α<VAR>LinearOrderedSemifield β<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₂ : AntivaryOn f₂ g s<GOAL>MonovaryOn (f₁ / f₂) g s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedSemifield α<VAR>LinearOrderedSemifield β<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₂ : MonovaryOn f₂ g s<GOAL>AntivaryOn (f₁ / f₂) g s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedSemifield α<VAR>LinearOrderedSemifield β<VAR>f₁ f₂ : ι → α<VAR>g : ι → β<VAR>hf₁ : 0 ≤ f₁<VAR>hf₂ : StrongLT 0 f₂<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>LinearOrderedSemifield α<VAR>LinearOrderedSemifield β<VAR>f₁ f₂ : ι → α<VAR>g : ι → β<VAR>hf₁ : 0 ≤ f₁<VAR>hf₂ : StrongLT 0 f₂<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>LinearOrderedSemifield α<VAR>LinearOrderedSemifield β<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₂ : AntivaryOn f g₂ s<GOAL>MonovaryOn f (g₁ / g₂) s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedSemifield α<VAR>LinearOrderedSemifield β<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₂ : MonovaryOn f g₂ s<GOAL>AntivaryOn f (g₁ / g₂) s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedSemifield α<VAR>LinearOrderedSemifield β<VAR>f : ι → α<VAR>g₁ g₂ : ι → β<VAR>hg₁ : 0 ≤ g₁<VAR>hg₂ : StrongLT 0 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>LinearOrderedSemifield α<VAR>LinearOrderedSemifield β<VAR>f : ι → α<VAR>g₁ g₂ : ι → β<VAR>hg₁ : 0 ≤ g₁<VAR>hg₂ : StrongLT 0 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>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>OrderedSMul α β<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<GOAL>MonovaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → 0 ≤ (f j - f i) • (g j - g i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>OrderedSMul α β<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<GOAL>AntivaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f j - f i) • (g j - g i) ≤ 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>OrderedSMul α β<VAR>f : ι → α<VAR>g : ι → β<GOAL>Monovary f g ↔ ∀ (i j : ι), 0 ≤ (f j - f i) • (g j - g i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>OrderedSMul α β<VAR>f : ι → α<VAR>g : ι → β<GOAL>Antivary f g ↔ ∀ (i j : ι), (f j - f i) • (g j - g i) ≤ 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>OrderedSMul α β<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<GOAL>MonovaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i • g j + f j • g i ≤ f i • g i + f j • g j
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>OrderedSMul α β<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<GOAL>AntivaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i • g i + f j • g j ≤ f i • g j + f j • g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>OrderedSMul α β<VAR>f : ι → α<VAR>g : ι → β<GOAL>Monovary f g ↔ ∀ (i j : ι), f i • g j + f j • g i ≤ f i • g i + f j • g j
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>OrderedSMul α β<VAR>f : ι → α<VAR>g : ι → β<GOAL>Antivary f g ↔ ∀ (i j : ι), f i • g i + f j • g j ≤ f i • g j + f j • g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>f g : ι → α<VAR>s : Set ι<GOAL>MonovaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → 0 ≤ (f j - f i) * (g j - g i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>f g : ι → α<VAR>s : Set ι<GOAL>AntivaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f j - f i) * (g j - g i) ≤ 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>f g : ι → α<GOAL>Monovary f g ↔ ∀ (i j : ι), 0 ≤ (f j - f i) * (g j - g i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>f g : ι → α<GOAL>Antivary f g ↔ ∀ (i j : ι), (f j - f i) * (g j - g i) ≤ 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>f g : ι → α<VAR>s : Set ι<GOAL>MonovaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i * g j + f j * g i ≤ f i * g i + f j * g j
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>f g : ι → α<VAR>s : Set ι<GOAL>AntivaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i * g i + f j * g j ≤ f i * g j + f j * g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>f g : ι → α<GOAL>Monovary f g ↔ ∀ (i j : ι), f i * g j + f j * g i ≤ f i * g i + f j * g j
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrderedRing α<VAR>f g : ι → α<GOAL>Antivary f g ↔ ∀ (i j : ι), f i * g i + f j * g j ≤ f i * g j + f j * g i
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>DecidableEq ι<VAR>AddCommMonoid μ<VAR>Finset.HasAntidiagonal μ<VAR>DecidableEq μ<VAR>s : Finset ι<VAR>n : μ<VAR>f : ι →₀ μ<GOAL>f ∈ s.finsuppAntidiag n ↔ s.sum ⇑f = n ∧ f.support ⊆ s
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>DecidableEq ι<VAR>AddCommMonoid μ<VAR>Finset.HasAntidiagonal μ<VAR>DecidableEq μ<VAR>s : Finset ι<VAR>n : μ<VAR>f : ι →₀ μ<GOAL>f ∈ s.finsuppAntidiag n ↔ (f.sum fun x x => x) = n ∧ f.support ⊆ s
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>DecidableEq ι<VAR>AddCommMonoid μ<VAR>Finset.HasAntidiagonal μ<VAR>DecidableEq μ<GOAL>∅.finsuppAntidiag 0 = {0}
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>DecidableEq ι<VAR>AddCommMonoid μ<VAR>Finset.HasAntidiagonal μ<VAR>DecidableEq μ<VAR>n : μ<VAR>hn : n ≠ 0<GOAL>∅.finsuppAntidiag n = ∅
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>DecidableEq ι<VAR>AddCommMonoid μ<VAR>Finset.HasAntidiagonal μ<VAR>DecidableEq μ<VAR>n : μ<GOAL>∅.finsuppAntidiag n = if n = 0 then {0} else ∅
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>DecidableEq ι<VAR>AddCommMonoid μ<VAR>Finset.HasAntidiagonal μ<VAR>DecidableEq μ<VAR>a : ι<VAR>s : Finset ι<VAR>h : a ∉ s<VAR>n : μ<VAR>f : ι →₀ μ<GOAL>f ∈ (insert a s).finsuppAntidiag n ↔ ∃ m ∈ Finset.antidiagonal n, ∃ g, f = g.update a m.1 ∧ g ∈ s.finsuppAntidiag m.2
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>DecidableEq ι<VAR>AddCommMonoid μ<VAR>Finset.HasAntidiagonal μ<VAR>DecidableEq μ<VAR>a : ι<VAR>s : Finset ι<VAR>h : a ∉ s<VAR>n : μ<GOAL>(insert a s).finsuppAntidiag n = (Finset.antidiagonal n).biUnion fun p => Finset.map { toFun := fun f => (↑f).update a p.1, inj' := ⋯ } (s.finsuppAntidiag p.2).attach
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>DecidableEq ι<VAR>AddCommMonoid μ<VAR>Finset.HasAntidiagonal μ<VAR>DecidableEq μ<VAR>AddCommMonoid μ'<VAR>Finset.HasAntidiagonal μ'<VAR>DecidableEq μ'<VAR>e : μ ≃+ μ'<VAR>s : Finset ι<VAR>n : μ<GOAL>Finset.map (Finsupp.mapRange.addEquiv e).toEmbedding (s.finsuppAntidiag n) ⊆ s.finsuppAntidiag (e n)
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>DecidableEq ι<VAR>AddCommMonoid μ<VAR>Finset.HasAntidiagonal μ<VAR>DecidableEq μ<VAR>AddCommMonoid μ'<VAR>Finset.HasAntidiagonal μ'<VAR>DecidableEq μ'<VAR>e : μ ≃+ μ'<VAR>s : Finset ι<VAR>n : μ<GOAL>Finset.map (Finsupp.mapRange.addEquiv e).toEmbedding (s.finsuppAntidiag n) = s.finsuppAntidiag (e n)
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>DecidableEq ι<VAR>DecidableEq μ<VAR>CanonicallyOrderedAddCommMonoid μ<VAR>Finset.HasAntidiagonal μ<VAR>s : Finset ι<GOAL>s.finsuppAntidiag 0 = {0}
<VAR>α : Type u<VAR>self : OrderedAddCommGroup α<VAR>a b : α<GOAL>a ≤ b → ∀ (c : α), c + a ≤ c + b
<VAR>α : Type u<VAR>self : OrderedCommGroup α<VAR>a b : α<GOAL>a ≤ b → ∀ (c : α), c * a ≤ c * b
<VAR>α : Type u<VAR>OrderedAddCommGroup α<GOAL>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
<VAR>α : Type u<VAR>OrderedCommGroup α<GOAL>ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
<VAR>α : Type u<VAR>OrderedAddCommGroup α<GOAL>ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
<VAR>α : Type u<VAR>OrderedCommGroup α<GOAL>ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
<VAR>α : Type u<VAR>LinearOrderedCommGroup α<VAR>a b : α<VAR>h : a < b<VAR>c : α<GOAL>c * a < c * b
<VAR>α : Type u<VAR>LinearOrderedAddCommGroup α<VAR>a b : α<VAR>h : a < b<VAR>c : α<GOAL>c + a < c + b
<VAR>α : Type u<VAR>LinearOrderedAddCommGroup α<VAR>a : α<VAR>h : -a = a<GOAL>a = 0
<VAR>α : Type u<VAR>LinearOrderedCommGroup α<VAR>a : α<VAR>h : a⁻¹ = a<GOAL>a = 1
<VAR>α : Type u<VAR>LinearOrderedCommGroup α<VAR>Nontrivial α<GOAL>∃ a, 1 < a
<VAR>α : Type u<VAR>LinearOrderedAddCommGroup α<VAR>Nontrivial α<GOAL>∃ a, 0 < a
<VAR>α : Type u<VAR>LinearOrderedCommGroup α<VAR>a : α<GOAL>a⁻¹ ≤ a ↔ 1 ≤ a
<VAR>α : Type u<VAR>LinearOrderedAddCommGroup α<VAR>a : α<GOAL>-a ≤ a ↔ 0 ≤ a
<VAR>α : Type u<VAR>LinearOrderedCommGroup α<VAR>a : α<GOAL>a⁻¹ < a ↔ 1 < a
<VAR>α : Type u<VAR>LinearOrderedAddCommGroup α<VAR>a : α<GOAL>-a < a ↔ 0 < a
<VAR>α : Type u<VAR>LinearOrderedAddCommGroup α<VAR>a : α<GOAL>a ≤ -a ↔ a ≤ 0
<VAR>α : Type u<VAR>LinearOrderedCommGroup α<VAR>a : α<GOAL>a ≤ a⁻¹ ↔ a ≤ 1
<VAR>α : Type u<VAR>LinearOrderedCommGroup α<VAR>a : α<GOAL>a < a⁻¹ ↔ a < 1
<VAR>α : Type u<VAR>LinearOrderedAddCommGroup α<VAR>a : α<GOAL>a < -a ↔ a < 0
<VAR>α : Type u<VAR>OrderedCommGroup α<VAR>a b : α<GOAL>a ≤ b → b⁻¹ ≤ a⁻¹
<VAR>α : Type u<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>a ≤ b → -b ≤ -a
<VAR>α : Type u<VAR>OrderedAddCommGroup α<VAR>a b : α<GOAL>a < b → -b < -a
<VAR>α : Type u<VAR>OrderedCommGroup α<VAR>a b : α<GOAL>a < b → b⁻¹ < a⁻¹
<VAR>α : Type u<VAR>OrderedCommGroup α<VAR>a : α<GOAL>1 < a → a⁻¹ < 1
<VAR>α : Type u<VAR>OrderedAddCommGroup α<VAR>a : α<GOAL>0 < a → -a < 0
<VAR>α : Type u<VAR>OrderedAddCommGroup α<VAR>a : α<GOAL>0 ≤ a → -a ≤ 0
<VAR>α : Type u<VAR>OrderedCommGroup α<VAR>a : α<GOAL>1 ≤ a → a⁻¹ ≤ 1
<VAR>α : Type u<VAR>OrderedCommGroup α<VAR>a : α<GOAL>a ≤ 1 → 1 ≤ a⁻¹
<VAR>α : Type u<VAR>OrderedAddCommGroup α<VAR>a : α<GOAL>a ≤ 0 → 0 ≤ -a
<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>StrictMono fun x => x ^ n
<VAR>α : Type u_1<VAR>n : ℕ<VAR>f : α → ℕ<VAR>Preorder α<VAR>hn : n ≠ 0<VAR>hf : StrictMono f<GOAL>StrictMono fun x => f x ^ n
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>s : Set α<VAR>a ε : α<VAR>h : IsGLB s a<VAR>hε : 0 < ε<GOAL>∃ b ∈ s, a ≤ b ∧ b < a + ε
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>s : Set α<VAR>a ε : α<VAR>h : IsGLB s a<VAR>h₂ : a ∉ s<VAR>hε : 0 < ε<GOAL>∃ b ∈ s, a < b ∧ b < a + ε
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>s : Set α<VAR>a ε : α<VAR>h : IsLUB s a<VAR>hε : 0 < ε<GOAL>∃ b ∈ s, a - ε < b ∧ b ≤ a
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>s : Set α<VAR>a ε : α<VAR>h : IsLUB s a<VAR>h₂ : a ∉ s<VAR>hε : 0 < ε<GOAL>∃ b ∈ s, a - ε < b ∧ b < a
<VAR>μ : Type u_2<VAR>AddCommMonoid μ<VAR>Finset.HasAntidiagonal μ<VAR>DecidableEq μ<VAR>n : μ<VAR>d : ℕ<VAR>f : Fin d → μ<GOAL>f ∈ Finset.finAntidiagonal d n ↔ ∑ i : Fin d, f i = n
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>DecidableEq ι<VAR>AddCommMonoid μ<VAR>Finset.HasAntidiagonal μ<VAR>DecidableEq μ<VAR>s : Finset ι<VAR>n : μ<VAR>f : ι → μ<GOAL>f ∈ s.piAntidiag n ↔ s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>DecidableEq ι<VAR>AddCommMonoid μ<VAR>Finset.HasAntidiagonal μ<VAR>DecidableEq μ<GOAL>∅.piAntidiag 0 = {0}
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>DecidableEq ι<VAR>AddCommMonoid μ<VAR>Finset.HasAntidiagonal μ<VAR>DecidableEq μ<VAR>n : μ<VAR>hn : n ≠ 0<GOAL>∅.piAntidiag n = ∅
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>DecidableEq ι<VAR>AddCommMonoid μ<VAR>Finset.HasAntidiagonal μ<VAR>DecidableEq μ<VAR>n : μ<GOAL>∅.piAntidiag n = if n = 0 then {0} else ∅
<VAR>μ : Type u_2<VAR>AddCommMonoid μ<VAR>Finset.HasAntidiagonal μ<VAR>DecidableEq μ<VAR>n : μ<GOAL>(Equiv.boolArrowEquivProd μ).finsetCongr (Finset.univ.piAntidiag n) = Finset.antidiagonal n
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>DecidableEq ι<VAR>AddCancelCommMonoid μ<VAR>Finset.HasAntidiagonal μ<VAR>DecidableEq μ<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>n : μ<GOAL>(↑(Finset.antidiagonal n)).PairwiseDisjoint fun p => Finset.map (addRightEmbedding fun j => if j = i then p.1 else 0) (s.piAntidiag p.2)
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>DecidableEq ι<VAR>AddCancelCommMonoid μ<VAR>Finset.HasAntidiagonal μ<VAR>DecidableEq μ<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>n : μ<GOAL>(Finset.cons i s hi).piAntidiag n = (Finset.antidiagonal n).disjiUnion (fun p => Finset.map (addRightEmbedding fun t => if t = i then p.1 else 0) (s.piAntidiag p.2)) ⋯
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>DecidableEq ι<VAR>AddCancelCommMonoid μ<VAR>Finset.HasAntidiagonal μ<VAR>DecidableEq μ<VAR>i : ι<VAR>s : Finset ι<VAR>DecidableEq (ι → μ)<VAR>hi : i ∉ s<VAR>n : μ<GOAL>(insert i s).piAntidiag n = (Finset.antidiagonal n).biUnion fun p => Finset.image (fun f j => f j + if j = i then p.1 else 0) (s.piAntidiag p.2)
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>DecidableEq ι<VAR>CanonicallyOrderedAddCommMonoid μ<VAR>Finset.HasAntidiagonal μ<VAR>DecidableEq μ<VAR>s : Finset ι<GOAL>s.piAntidiag 0 = {0}
<VAR>n k : ℕ<GOAL>Finset.univ.piAntidiag n = Finset.Nat.antidiagonalTuple k n
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>DecidableEq (ι → ℕ)<VAR>s : Finset ι<VAR>m : ℕ<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>SMul.smul n (s.piAntidiag m) = Finset.filter (fun f => ∀ i ∈ s, n ∣ f i) (s.piAntidiag (n * m))
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>m : ℕ<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>Finset.map { toFun := fun x => n • x, inj' := ⋯ } (s.piAntidiag m) = Finset.filter (fun f => ∀ i ∈ s, n ∣ f i) (s.piAntidiag (n * m))
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>Fintype ι<VAR>m : ℕ<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>SMul.smul n (Finset.univ.piAntidiag m) = Finset.filter (fun f => ∀ (i : ι), n ∣ f i) (Finset.univ.piAntidiag (n * m))
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>Fintype ι<VAR>m : ℕ<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>Finset.map { toFun := fun x => n • x, inj' := ⋯ } (Finset.univ.piAntidiag m) = Finset.filter (fun f => ∀ (i : ι), n ∣ f i) (Finset.univ.piAntidiag (n * m))
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>n : ℕ<GOAL>Finset.map { toFun := fun m a => Multiset.count a ↑m, inj' := ⋯ } (s.sym n) = s.piAntidiag n
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<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>∀ (a : αᵒᵈ), (RelIso.symm (OrderIso.neg α)) a = -OrderDual.ofDual a
<VAR>α : Type u<VAR>Group α<VAR>LE α<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>∀ (a : αᵒᵈ), (RelIso.symm (OrderIso.inv α)) a = (OrderDual.ofDual a)⁻¹
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<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>∀ (a : α), (OrderIso.neg α) a = OrderDual.toDual (-a)
<VAR>α : Type u<VAR>Group α<VAR>LE α<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>∀ (a : α), (OrderIso.inv α) a = OrderDual.toDual a⁻¹
<VAR>α : Type u<VAR>Group α<VAR>LE α<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 ↔ b⁻¹ ≤ a
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<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 ↔ -b ≤ a
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<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 ↔ b ≤ -a
<VAR>α : Type u<VAR>Group α<VAR>LE α<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⁻¹ ↔ b ≤ a⁻¹
<VAR>α : Type u<VAR>Group α<VAR>LE α<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_1 : αᵒᵈ), (RelIso.symm (OrderIso.divLeft a)) a_1 = (OrderDual.ofDual a_1)⁻¹ * a
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<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_1 : αᵒᵈ), (RelIso.symm (OrderIso.subLeft a)) a_1 = -OrderDual.ofDual a_1 + a
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<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_1 : α), (OrderIso.subLeft a) a_1 = OrderDual.toDual (a - a_1)
<VAR>α : Type u<VAR>Group α<VAR>LE α<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_1 : α), (OrderIso.divLeft a) a_1 = OrderDual.toDual (a / a_1)
<VAR>α : Type u<VAR>Group α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>(OrderIso.mulRight a).toEquiv = Equiv.mulRight a
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a x : α<GOAL>(OrderIso.addRight a) x = x + a
<VAR>α : Type u<VAR>Group α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a x : α<GOAL>(OrderIso.mulRight a) x = x * a
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>(OrderIso.addRight a).toEquiv = Equiv.addRight a
<VAR>α : Type u<VAR>Group α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>(OrderIso.mulRight a).symm = OrderIso.mulRight a⁻¹
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>(OrderIso.addRight a).symm = OrderIso.addRight (-a)
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>(RelIso.symm (OrderIso.subRight a)) b = b + a
<VAR>α : Type u<VAR>Group α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>(OrderIso.divRight a) b = b / a
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>(OrderIso.subRight a) b = b - a
<VAR>α : Type u<VAR>Group α<VAR>LE α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>(RelIso.symm (OrderIso.divRight a)) b = b * a
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>(OrderIso.addLeft a).toEquiv = Equiv.addLeft a
<VAR>α : Type u<VAR>Group α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>(OrderIso.mulLeft a).toEquiv = Equiv.mulLeft a
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a x : α<GOAL>(OrderIso.addLeft a) x = a + x
<VAR>α : Type u<VAR>Group α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a x : α<GOAL>(OrderIso.mulLeft a) x = a * x