ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>LinearOrderedCancelAddCommMonoid α<VAR>Nontrivial α<VAR>DenselyOrdered α<VAR>ExistsAddOfLE α<VAR>Finite ι<VAR>x y : ι → α<VAR>h : ∀ (i : ι), x i < y i<GOAL>∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>x : { x // 0 < x }<GOAL>↑x⁻¹ = (↑x)⁻¹
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>x : { x // 0 < x }<VAR>n : ℤ<GOAL>↑(x ^ n) = ↑x ^ n
<VAR>G : Type u_3<VAR>P : Type u_4<VAR>LE G<VAR>LE P<VAR>VAdd G P<VAR>self : IsOrderedVAdd G P<VAR>c d : G<GOAL>c ≤ d → ∀ (a : P), c +ᵥ a ≤ d +ᵥ a
<VAR>G : Type u_3<VAR>P : Type u_4<VAR>LE G<VAR>LE P<VAR>VAdd G P<VAR>self : IsOrderedVAdd G P<VAR>a b : P<GOAL>a ≤ b → ∀ (c : G), c +ᵥ a ≤ c +ᵥ b
<VAR>G : Type u_3<VAR>P : Type u_4<VAR>LE G<VAR>LE P<VAR>SMul G P<VAR>self : IsOrderedSMul G P<VAR>a b : P<GOAL>a ≤ b → ∀ (c : G), c • a ≤ c • b
<VAR>G : Type u_3<VAR>P : Type u_4<VAR>LE G<VAR>LE P<VAR>SMul G P<VAR>self : IsOrderedSMul G P<VAR>c d : G<GOAL>c ≤ d → ∀ (a : P), c • a ≤ d • a
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>Preorder G<VAR>Preorder P<VAR>VAdd G P<VAR>IsOrderedVAdd G P<VAR>a b : G<VAR>c d : P<VAR>hab : a ≤ b<VAR>hcd : c ≤ d<GOAL>a +ᵥ c ≤ b +ᵥ d
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>Preorder G<VAR>Preorder P<VAR>SMul G P<VAR>IsOrderedSMul G P<VAR>a b : G<VAR>c d : P<VAR>hab : a ≤ b<VAR>hcd : c ≤ d<GOAL>a • c ≤ b • d
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>γ : Type u_3<VAR>Preorder G<VAR>Preorder P<VAR>Preorder γ<VAR>VAdd G P<VAR>IsOrderedVAdd G P<VAR>f : γ → G<VAR>g : γ → P<VAR>hf : Monotone f<VAR>hg : Monotone g<GOAL>Monotone fun x => f x +ᵥ g x
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>γ : Type u_3<VAR>Preorder G<VAR>Preorder P<VAR>Preorder γ<VAR>SMul G P<VAR>IsOrderedSMul G P<VAR>f : γ → G<VAR>g : γ → P<VAR>hf : Monotone f<VAR>hg : Monotone g<GOAL>Monotone fun x => f x • g x
<VAR>G : Type u_3<VAR>P : Type u_4<VAR>VAdd G P<VAR>self : IsCancelVAdd G P<VAR>a : G<VAR>b c : P<GOAL>a +ᵥ b = a +ᵥ c → b = c
<VAR>G : Type u_3<VAR>P : Type u_4<VAR>VAdd G P<VAR>self : IsCancelVAdd G P<VAR>a b : G<VAR>c : P<GOAL>a +ᵥ c = b +ᵥ c → a = b
<VAR>G : Type u_3<VAR>P : Type u_4<VAR>SMul G P<VAR>self : IsCancelSMul G P<VAR>a : G<VAR>b c : P<GOAL>a • b = a • c → b = c
<VAR>G : Type u_3<VAR>P : Type u_4<VAR>SMul G P<VAR>self : IsCancelSMul G P<VAR>a b : G<VAR>c : P<GOAL>a • c = b • c → a = b
<VAR>G : Type u_3<VAR>P : Type u_4<VAR>LE G<VAR>LE P<VAR>VAdd G P<VAR>self : IsOrderedCancelVAdd G P<VAR>a b : G<VAR>c : P<GOAL>a +ᵥ c ≤ b +ᵥ c → a ≤ b
<VAR>G : Type u_3<VAR>P : Type u_4<VAR>LE G<VAR>LE P<VAR>VAdd G P<VAR>self : IsOrderedCancelVAdd G P<VAR>a : G<VAR>b c : P<GOAL>a +ᵥ b ≤ a +ᵥ c → b ≤ c
<VAR>G : Type u_3<VAR>P : Type u_4<VAR>LE G<VAR>LE P<VAR>SMul G P<VAR>self : IsOrderedCancelSMul G P<VAR>a b : G<VAR>c : P<GOAL>a • c ≤ b • c → a ≤ b
<VAR>G : Type u_3<VAR>P : Type u_4<VAR>LE G<VAR>LE P<VAR>SMul G P<VAR>self : IsOrderedCancelSMul G P<VAR>a : G<VAR>b c : P<GOAL>a • b ≤ a • c → b ≤ c
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>LE G<VAR>Preorder P<VAR>VAdd G P<VAR>IsOrderedCancelVAdd G P<VAR>a b : G<VAR>c d : P<VAR>h₁ : a ≤ b<VAR>h₂ : c < d<GOAL>a +ᵥ c < b +ᵥ d
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>LE G<VAR>Preorder P<VAR>SMul G P<VAR>IsOrderedCancelSMul G P<VAR>a b : G<VAR>c d : P<VAR>h₁ : a ≤ b<VAR>h₂ : c < d<GOAL>a • c < b • d
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>Preorder G<VAR>Preorder P<VAR>SMul G P<VAR>IsOrderedCancelSMul G P<VAR>a b : G<VAR>c d : P<VAR>h₁ : a < b<VAR>h₂ : c ≤ d<GOAL>a • c < b • d
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>Preorder G<VAR>Preorder P<VAR>VAdd G P<VAR>IsOrderedCancelVAdd G P<VAR>a b : G<VAR>c d : P<VAR>h₁ : a < b<VAR>h₂ : c ≤ d<GOAL>a +ᵥ c < b +ᵥ d
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>EuclideanDomain R<VAR>OrderedSemiring S<VAR>abv : AbsoluteValue R S<VAR>self : abv.IsEuclidean<VAR>x y : R<GOAL>abv x < abv y ↔ x ≺ y
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>EuclideanDomain R<VAR>OrderedSemiring S<VAR>abv : AbsoluteValue R S<VAR>x y : R<VAR>h : abv.IsEuclidean<GOAL>abv x < abv y ↔ x ≺ y
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>EuclideanDomain R<VAR>OrderedSemiring S<VAR>abv : AbsoluteValue R S<VAR>h : abv.IsEuclidean<VAR>a : R<VAR>b : R<VAR>hb : b ≠ 0<GOAL>abv (a % b) < abv b
<VAR>R : Type u_5<VAR>S : Type u_6<VAR>Semiring R<VAR>OrderedSemiring S<VAR>self : AbsoluteValue R S<VAR>x : R<GOAL>self.toFun x = 0 ↔ x = 0
<VAR>R : Type u_5<VAR>S : Type u_6<VAR>Semiring R<VAR>OrderedSemiring S<VAR>self : AbsoluteValue R S<VAR>x y : R<GOAL>self.toFun (x + y) ≤ self.toFun x + self.toFun y
<VAR>R : Type u_5<VAR>S : Type u_6<VAR>Semiring R<VAR>OrderedSemiring S<VAR>self : AbsoluteValue R S<VAR>x : R<GOAL>0 ≤ self.toFun x
<VAR>R : Type u_5<VAR>S : Type u_6<VAR>Semiring R<VAR>OrderedSemiring S<VAR>f : R →ₙ* S<VAR>h₁ : ∀ (x : R), 0 ≤ f.toFun x<VAR>h₂ : ∀ (x : R), f.toFun x = 0 ↔ x = 0<VAR>h₃ : ∀ (x y : R), f.toFun (x + y) ≤ f.toFun x + f.toFun y<GOAL>⇑{ toMulHom := f, nonneg' := h₁, eq_zero' := h₂, add_le' := h₃ } = ⇑f
<VAR>R : Type u_5<VAR>S : Type u_6<VAR>Semiring R<VAR>OrderedSemiring S<VAR>f g : AbsoluteValue R S<GOAL>(∀ (x : R), f x = g x) → f = g
<VAR>R : Type u_5<VAR>S : Type u_6<VAR>Semiring R<VAR>OrderedSemiring S<VAR>abv : AbsoluteValue R S<GOAL>⇑abv.toMulHom = ⇑abv
<VAR>R : Type u_5<VAR>S : Type u_6<VAR>Semiring R<VAR>OrderedSemiring S<VAR>abv : AbsoluteValue R S<VAR>x : R<GOAL>0 ≤ abv x
<VAR>R : Type u_5<VAR>S : Type u_6<VAR>Semiring R<VAR>OrderedSemiring S<VAR>abv : AbsoluteValue R S<VAR>x : R<GOAL>abv x = 0 ↔ x = 0
<VAR>R : Type u_5<VAR>S : Type u_6<VAR>Semiring R<VAR>OrderedSemiring S<VAR>abv : AbsoluteValue R S<VAR>x y : R<GOAL>abv (x + y) ≤ abv x + abv y
<VAR>R : Type u_5<VAR>S : Type u_6<VAR>Semiring R<VAR>OrderedSemiring S<VAR>abv : AbsoluteValue R S<VAR>x y : R<GOAL>abv (x * y) = abv x * abv y
<VAR>R : Type u_5<VAR>S : Type u_6<VAR>Semiring R<VAR>OrderedSemiring S<VAR>abv : AbsoluteValue R S<VAR>x : R<GOAL>abv x ≠ 0 ↔ x ≠ 0
<VAR>R : Type u_5<VAR>S : Type u_6<VAR>Semiring R<VAR>OrderedSemiring S<VAR>abv : AbsoluteValue R S<VAR>x : R<VAR>hx : x ≠ 0<GOAL>0 < abv x
<VAR>R : Type u_5<VAR>S : Type u_6<VAR>Semiring R<VAR>OrderedSemiring S<VAR>abv : AbsoluteValue R S<VAR>x : R<GOAL>0 < abv x ↔ x ≠ 0
<VAR>R : Type u_5<VAR>S : Type u_6<VAR>Semiring R<VAR>OrderedSemiring S<VAR>abv : AbsoluteValue R S<VAR>x : R<VAR>hx : x ≠ 0<GOAL>abv x ≠ 0
<VAR>R : Type u_5<VAR>S : Type u_6<VAR>Semiring R<VAR>OrderedSemiring S<VAR>abv : AbsoluteValue R S<VAR>h : IsLeftRegular (abv 1)<GOAL>abv 1 = 1
<VAR>R : Type u_5<VAR>S : Type u_6<VAR>Semiring R<VAR>OrderedSemiring S<VAR>abv : AbsoluteValue R S<GOAL>abv 0 = 0
<VAR>R : Type u_5<VAR>S : Type u_6<VAR>Ring R<VAR>OrderedSemiring S<VAR>abv : AbsoluteValue R S<VAR>a b c : R<GOAL>abv (a - c) ≤ abv (a - b) + abv (b - c)
<VAR>R : Type u_5<VAR>S : Type u_6<VAR>Ring R<VAR>OrderedSemiring S<VAR>abv : AbsoluteValue R S<VAR>a b : R<GOAL>abv (a - b) = 0 ↔ a = b
<VAR>R : Type u_5<VAR>S : Type u_6<VAR>Semiring R<VAR>OrderedRing S<VAR>abv : AbsoluteValue R S<VAR>IsDomain S<VAR>Nontrivial R<GOAL>abv 1 = 1
<VAR>R : Type u_5<VAR>S : Type u_6<VAR>Semiring R<VAR>OrderedRing S<VAR>abv : AbsoluteValue R S<VAR>IsDomain S<VAR>Nontrivial R<GOAL>⇑abv.toMonoidWithZeroHom = ⇑abv
<VAR>R : Type u_5<VAR>S : Type u_6<VAR>Semiring R<VAR>OrderedRing S<VAR>abv : AbsoluteValue R S<VAR>IsDomain S<VAR>Nontrivial R<GOAL>⇑abv.toMonoidHom = ⇑abv
<VAR>R : Type u_5<VAR>S : Type u_6<VAR>Semiring R<VAR>OrderedRing S<VAR>abv : AbsoluteValue R S<VAR>IsDomain S<VAR>Nontrivial R<VAR>a : R<VAR>n : ℕ<GOAL>abv (a ^ n) = abv a ^ n
<VAR>R : Type u_5<VAR>S : Type u_6<VAR>Ring R<VAR>OrderedRing S<VAR>abv : AbsoluteValue R S<VAR>a b : R<GOAL>abv a - abv b ≤ abv (a - b)
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>OrderedCommRing S<VAR>Ring R<VAR>abv : AbsoluteValue R S<VAR>NoZeroDivisors S<VAR>a : R<GOAL>abv (-a) = abv a
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>OrderedCommRing S<VAR>Ring R<VAR>abv : AbsoluteValue R S<VAR>NoZeroDivisors S<VAR>a b : R<GOAL>abv (a - b) = abv (b - a)
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>OrderedCommRing S<VAR>Ring R<VAR>abv : AbsoluteValue R S<VAR>NoZeroDivisors S<VAR>a b : R<GOAL>abv a - abv b ≤ abv (a + b)
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>OrderedCommRing S<VAR>Ring R<VAR>abv : AbsoluteValue R S<VAR>NoZeroDivisors S<VAR>a b : R<GOAL>abv (a - b) ≤ abv a + abv b
<VAR>S : Type u_6<VAR>LinearOrderedRing S<VAR>a : S<GOAL>AbsoluteValue.abs a = |a|
<VAR>R : Type u_5<VAR>S : Type u_6<VAR>Ring R<VAR>LinearOrderedCommRing S<VAR>abv : AbsoluteValue R S<VAR>a b : R<GOAL>|abv a - abv b| ≤ abv (a - b)
<VAR>S : Type u_5<VAR>OrderedSemiring S<VAR>R : Type u_6<VAR>Semiring R<VAR>f : R → S<VAR>self : IsAbsoluteValue f<VAR>x : R<GOAL>f x = 0 ↔ x = 0
<VAR>S : Type u_5<VAR>OrderedSemiring S<VAR>R : Type u_6<VAR>Semiring R<VAR>f : R → S<VAR>self : IsAbsoluteValue f<VAR>x y : R<GOAL>f (x * y) = f x * f y
<VAR>S : Type u_5<VAR>OrderedSemiring S<VAR>R : Type u_6<VAR>Semiring R<VAR>f : R → S<VAR>self : IsAbsoluteValue f<VAR>x y : R<GOAL>f (x + y) ≤ f x + f y
<VAR>S : Type u_5<VAR>OrderedSemiring S<VAR>R : Type u_6<VAR>Semiring R<VAR>f : R → S<VAR>self : IsAbsoluteValue f<VAR>x : R<GOAL>0 ≤ f x
<VAR>S : Type u_5<VAR>OrderedSemiring S<VAR>R : Type u_6<VAR>Semiring R<VAR>abv : R → S<VAR>IsAbsoluteValue abv<VAR>x : R<GOAL>0 ≤ abv x
<VAR>S : Type u_5<VAR>OrderedSemiring S<VAR>R : Type u_6<VAR>Semiring R<VAR>abv : R → S<VAR>IsAbsoluteValue abv<VAR>x : R<GOAL>abv x = 0 ↔ x = 0
<VAR>S : Type u_5<VAR>OrderedSemiring S<VAR>R : Type u_6<VAR>Semiring R<VAR>abv : R → S<VAR>IsAbsoluteValue abv<VAR>x y : R<GOAL>abv (x + y) ≤ abv x + abv y
<VAR>S : Type u_5<VAR>OrderedSemiring S<VAR>R : Type u_6<VAR>Semiring R<VAR>abv : R → S<VAR>IsAbsoluteValue abv<VAR>x y : R<GOAL>abv (x * y) = abv x * abv y
<VAR>S : Type u_5<VAR>OrderedSemiring S<VAR>R : Type u_6<VAR>Semiring R<VAR>abv : R → S<VAR>IsAbsoluteValue abv<GOAL>∀ (a : R), (IsAbsoluteValue.toAbsoluteValue abv) a = abv a
<VAR>S : Type u_5<VAR>OrderedSemiring S<VAR>R : Type u_6<VAR>Semiring R<VAR>abv : R → S<VAR>IsAbsoluteValue abv<GOAL>abv 0 = 0
<VAR>S : Type u_5<VAR>OrderedSemiring S<VAR>R : Type u_6<VAR>Semiring R<VAR>abv : R → S<VAR>IsAbsoluteValue abv<VAR>a : R<GOAL>0 < abv a ↔ a ≠ 0
<VAR>S : Type u_5<VAR>OrderedRing S<VAR>R : Type u_6<VAR>Semiring R<VAR>abv : R → S<VAR>IsAbsoluteValue abv<VAR>IsDomain S<VAR>Nontrivial R<GOAL>abv 1 = 1
<VAR>S : Type u_5<VAR>OrderedRing S<VAR>R : Type u_6<VAR>Semiring R<VAR>IsDomain S<VAR>Nontrivial R<VAR>abv : R → S<VAR>IsAbsoluteValue abv<VAR>a : R<VAR>n : ℕ<GOAL>abv (a ^ n) = abv a ^ n
<VAR>S : Type u_5<VAR>OrderedRing S<VAR>R : Type u_6<VAR>Ring R<VAR>abv : R → S<VAR>IsAbsoluteValue abv<VAR>a b c : R<GOAL>abv (a - c) ≤ abv (a - b) + abv (b - c)
<VAR>S : Type u_5<VAR>OrderedRing S<VAR>R : Type u_6<VAR>Ring R<VAR>abv : R → S<VAR>IsAbsoluteValue abv<VAR>a b : R<GOAL>abv a - abv b ≤ abv (a - b)
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>OrderedCommRing S<VAR>NoZeroDivisors S<VAR>Ring R<VAR>abv : R → S<VAR>IsAbsoluteValue abv<VAR>a : R<GOAL>abv (-a) = abv a
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>OrderedCommRing S<VAR>NoZeroDivisors S<VAR>Ring R<VAR>abv : R → S<VAR>IsAbsoluteValue abv<VAR>a b : R<GOAL>abv (a - b) = abv (b - a)
<VAR>S : Type u_5<VAR>LinearOrderedCommRing S<VAR>R : Type u_6<VAR>Ring R<VAR>abv : R → S<VAR>IsAbsoluteValue abv<VAR>a b : R<GOAL>|abv a - abv b| ≤ abv (a - b)
<VAR>S : Type u_5<VAR>LinearOrderedSemifield S<VAR>R : Type u_6<VAR>Semiring R<VAR>Nontrivial R<VAR>abv : R → S<VAR>IsAbsoluteValue abv<GOAL>abv 1 = 1
<VAR>S : Type u_5<VAR>LinearOrderedSemifield S<VAR>R : Type u_6<VAR>DivisionSemiring R<VAR>abv : R → S<VAR>IsAbsoluteValue abv<VAR>a : R<GOAL>abv a⁻¹ = (abv a)⁻¹
<VAR>S : Type u_5<VAR>LinearOrderedSemifield S<VAR>R : Type u_6<VAR>DivisionSemiring R<VAR>abv : R → S<VAR>IsAbsoluteValue abv<VAR>a b : R<GOAL>abv (a / b) = abv a / abv b
<VAR>M : Type u_2<VAR>α : Type u_3<VAR>SMul M α<VAR>Preorder α<VAR>CovariantClass M α HSMul.hSMul LE.le<VAR>m : M<GOAL>Monotone (HSMul.hSMul m)
<VAR>M : Type u_2<VAR>α : Type u_3<VAR>SMul M α<VAR>Preorder α<VAR>CovariantClass M α HSMul.hSMul LE.le<VAR>m : M<VAR>a b : α<VAR>h : a ≤ b<GOAL>m • a ≤ m • b
<VAR>M : Type u_2<VAR>α : Type u_3<VAR>SMul M α<VAR>SemilatticeInf α<VAR>CovariantClass M α HSMul.hSMul LE.le<VAR>m : M<VAR>a₁ a₂ : α<GOAL>m • (a₁ ⊓ a₂) ≤ m • a₁ ⊓ m • a₂
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>α : Type u_3<VAR>SMul M α<VAR>CompleteLattice α<VAR>CovariantClass M α HSMul.hSMul LE.le<VAR>m : M<VAR>t : ι → α<GOAL>m • iInf t ≤ ⨅ i, m • t i
<VAR>M : Type u_2<VAR>α : Type u_3<VAR>SMul M α<VAR>Preorder α<VAR>CovariantClass M α HSMul.hSMul LT.lt<VAR>m : M<GOAL>StrictMono (HSMul.hSMul m)
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>Preorder M<VAR>CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>x y : { x // 0 < x }<GOAL>↑(x + y) = ↑x + ↑y
<VAR>R : Type u_2<VAR>StrictOrderedSemiring R<VAR>x y : { x // 0 < x }<GOAL>↑(x * y) = ↑x * ↑y
<VAR>R : Type u_2<VAR>StrictOrderedSemiring R<VAR>x : { x // 0 < x }<VAR>n : ℕ<GOAL>↑(x ^ n) = ↑x ^ n
<VAR>R : Type u_2<VAR>StrictOrderedSemiring R<GOAL>↑1 = 1
<VAR>A : Type u_1<VAR>AddMonoid A<VAR>self : Finset.HasAntidiagonal A<VAR>n : A<VAR>a : A × A<GOAL>a ∈ Finset.antidiagonal n ↔ a.1 + a.2 = n
<VAR>A : Type u_2<VAR>AddMonoid A<VAR>H1 : Finset.HasAntidiagonal A<VAR>H2 : Finset.HasAntidiagonal A<GOAL>Finset.antidiagonal = Finset.antidiagonal
<VAR>A : Type u_1<VAR>AddCommMonoid A<VAR>Finset.HasAntidiagonal A<VAR>n : A<VAR>xy : A × A<GOAL>xy.swap ∈ Finset.antidiagonal n ↔ xy ∈ Finset.antidiagonal n
<VAR>A : Type u_1<VAR>AddCommMonoid A<VAR>Finset.HasAntidiagonal A<VAR>n : A<GOAL>Finset.map (Equiv.prodComm A A).toEmbedding (Finset.antidiagonal n) = Finset.antidiagonal n
<VAR>A : Type u_1<VAR>AddCommMonoid A<VAR>Finset.HasAntidiagonal A<VAR>n : A<GOAL>Finset.map { toFun := Prod.swap, inj' := ⋯ } (Finset.antidiagonal n) = Finset.antidiagonal n
<VAR>A : Type u_1<VAR>AddCancelMonoid A<VAR>Finset.HasAntidiagonal A<VAR>p q : A × A<VAR>n : A<VAR>hp : p ∈ Finset.antidiagonal n<VAR>hq : q ∈ Finset.antidiagonal n<GOAL>p = q ↔ p.1 = q.1
<VAR>A : Type u_1<VAR>AddCancelMonoid A<VAR>Finset.HasAntidiagonal A<VAR>n : A<VAR>p q : { x // x ∈ Finset.antidiagonal n }<VAR>h : (↑p).1 = (↑q).1<GOAL>p = q
<VAR>A : Type u_1<VAR>AddCancelCommMonoid A<VAR>Finset.HasAntidiagonal A<VAR>p q : A × A<VAR>n : A<VAR>hp : p ∈ Finset.antidiagonal n<VAR>hq : q ∈ Finset.antidiagonal n<GOAL>p = q ↔ p.2 = q.2
<VAR>A : Type u_1<VAR>CanonicallyOrderedAddCommMonoid A<VAR>Finset.HasAntidiagonal A<GOAL>Finset.antidiagonal 0 = {(0, 0)}
<VAR>A : Type u_1<VAR>CanonicallyOrderedAddCommMonoid A<VAR>Finset.HasAntidiagonal A<VAR>n : A<VAR>kl : A × A<VAR>hlk : kl ∈ Finset.antidiagonal n<GOAL>kl.1 ≤ n
<VAR>A : Type u_1<VAR>CanonicallyOrderedAddCommMonoid A<VAR>Finset.HasAntidiagonal A<VAR>n : A<VAR>kl : A × A<VAR>hlk : kl ∈ Finset.antidiagonal n<GOAL>kl.2 ≤ n
<VAR>A : Type u_1<VAR>CanonicallyOrderedAddCommMonoid A<VAR>Sub A<VAR>OrderedSub A<VAR>ContravariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Finset.HasAntidiagonal A<VAR>n m : A<VAR>DecidablePred fun x => x = m<VAR>Decidable (m ≤ n)<GOAL>Finset.filter (fun x => x.1 = m) (Finset.antidiagonal n) = if m ≤ n then {(m, n - m)} else ∅
<VAR>A : Type u_1<VAR>CanonicallyOrderedAddCommMonoid A<VAR>Sub A<VAR>OrderedSub A<VAR>ContravariantClass A A (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Finset.HasAntidiagonal A<VAR>n m : A<VAR>DecidablePred fun x => x = m<VAR>Decidable (m ≤ n)<GOAL>Finset.filter (fun x => x.2 = m) (Finset.antidiagonal n) = if m ≤ n then {(n - m, m)} else ∅
<VAR>A : Type u_1<VAR>AddMonoid A<VAR>Finset.HasAntidiagonal A<VAR>x : (n : A) × { x // x ∈ Finset.antidiagonal n }<GOAL>Finset.sigmaAntidiagonalEquivProd x = ↑x.snd
<VAR>A : Type u_1<VAR>AddMonoid A<VAR>Finset.HasAntidiagonal A<VAR>x : A × A<GOAL>(Finset.sigmaAntidiagonalEquivProd.symm x).fst = x.1 + x.2
<VAR>A : Type u_1<VAR>AddMonoid A<VAR>Finset.HasAntidiagonal A<VAR>x : A × A<GOAL>↑(Finset.sigmaAntidiagonalEquivProd.symm x).snd = x
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>n : ℤ<VAR>a : α<VAR>ha : 1 < a<VAR>hn : 0 < n<GOAL>1 < a ^ n
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>n : ℤ<VAR>a : α<VAR>ha : 0 < a<VAR>hn : 0 < n<GOAL>0 < n • a
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a : α<VAR>ha : 0 < a<GOAL>StrictMono fun n => n • a
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>a : α<VAR>ha : 1 < a<GOAL>StrictMono fun n => a ^ n
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>a : α<VAR>ha : 0 ≤ a<GOAL>Monotone fun n => n • a
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>a : α<VAR>ha : 1 ≤ a<GOAL>Monotone fun n => a ^ n
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>m n : ℤ<VAR>a : α<VAR>ha : 0 ≤ a<VAR>h : m ≤ n<GOAL>m • a ≤ n • a
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>m n : ℤ<VAR>a : α<VAR>ha : 1 ≤ a<VAR>h : m ≤ n<GOAL>a ^ m ≤ a ^ n
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>m n : ℤ<VAR>a : α<VAR>ha : 1 < a<VAR>h : m < n<GOAL>a ^ m < a ^ n
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>m n : ℤ<VAR>a : α<VAR>ha : 0 < a<VAR>h : m < n<GOAL>m • a < n • a
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>m n : ℤ<VAR>a : α<VAR>ha : 0 < a<GOAL>m • a ≤ n • a ↔ m ≤ n
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>m n : ℤ<VAR>a : α<VAR>ha : 1 < a<GOAL>a ^ m ≤ a ^ n ↔ m ≤ n
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>m n : ℤ<VAR>a : α<VAR>ha : 0 < a<GOAL>m • a < n • a ↔ m < n
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>m n : ℤ<VAR>a : α<VAR>ha : 1 < a<GOAL>a ^ m < a ^ n ↔ m < n
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>n : ℤ<VAR>hn : 0 < n<GOAL>StrictMono fun x => n • x
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>n : ℤ<VAR>hn : 0 < n<GOAL>StrictMono fun x => x ^ n
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>n : ℤ<VAR>hn : 0 ≤ n<GOAL>Monotone fun x => x ^ n
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>n : ℤ<VAR>hn : 0 ≤ n<GOAL>Monotone fun x => n • x
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>n : ℤ<VAR>a b : α<VAR>hn : 0 ≤ n<VAR>h : a ≤ b<GOAL>n • a ≤ n • b
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>n : ℤ<VAR>a b : α<VAR>hn : 0 ≤ n<VAR>h : a ≤ b<GOAL>a ^ n ≤ b ^ n
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>n : ℤ<VAR>a b : α<VAR>hn : 0 < n<VAR>h : a < b<GOAL>n • a < n • b
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>n : ℤ<VAR>a b : α<VAR>hn : 0 < n<VAR>h : a < b<GOAL>a ^ n < b ^ n
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>n : ℤ<VAR>a b : α<VAR>hn : 0 < n<GOAL>n • a ≤ n • b ↔ a ≤ b
<VAR>α : Type u_1<VAR>LinearOrderedCommGroup α<VAR>n : ℤ<VAR>a b : α<VAR>hn : 0 < n<GOAL>a ^ n ≤ b ^ n ↔ a ≤ b
<VAR>α : Type u_1<VAR>LinearOrderedCommGroup α<VAR>n : ℤ<VAR>a b : α<VAR>hn : 0 < n<GOAL>a ^ n < b ^ n ↔ a < b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>n : ℤ<VAR>a b : α<VAR>hn : 0 < n<GOAL>n • a < n • b ↔ a < b
<VAR>α : Type u_1<VAR>LinearOrderedCommGroup α<VAR>n : ℤ<VAR>hn : n ≠ 0<GOAL>Function.Injective fun x => x ^ n
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>n : ℤ<VAR>hn : n ≠ 0<GOAL>Function.Injective fun x => n • x
<VAR>α : Type u_1<VAR>LinearOrderedCommGroup α<VAR>n : ℤ<VAR>a b : α<VAR>hn : n ≠ 0<GOAL>a ^ n = b ^ n ↔ a = b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>n : ℤ<VAR>a b : α<VAR>hn : n ≠ 0<GOAL>n • a = n • b ↔ a = b
<VAR>a : ℤ<GOAL>|a| = ↑a.natAbs
<VAR>n : ℤ<GOAL>↑n.natAbs = |n|
<VAR>b : ℤ<GOAL>b ≤ b ^ 2
<VAR>n : ℕ<GOAL>|↑n| = ↑n
<VAR>i j : ℤ<GOAL>(i - j).natAbs ≠ 0 ↔ i ≠ j
<VAR>z : ℤ<VAR>h₀ : z ≠ 0<GOAL>1 ≤ |z|
<VAR>a b : ℤ<VAR>H1 : 0 ≤ a<VAR>H2 : a < |b|<GOAL>a / b = 0
<VAR>a b : ℤ<GOAL>a % |b| = a % b
<VAR>a : ℤ<VAR>b : ℤ<VAR>H : b ≠ 0<GOAL>a % b < |b|
<VAR>a b : ℤ<GOAL>|a / b| ≤ |a|
<VAR>a : ℤ<GOAL>a.sign = a / |a|
<VAR>G : Type u_1<VAR>AddGroup G<VAR>a : G<VAR>n : ℤ<GOAL>|n| • a = 0 ↔ n • a = 0
<VAR>G : Type u_1<VAR>Group G<VAR>a : G<VAR>n : ℤ<GOAL>a ^ |n| = 1 ↔ a ^ n = 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 : α<GOAL>max a 1 / max a⁻¹ 1 = 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>max a 0 - max (-a) 0 = 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>max (-a) 0 = -a + max 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 : α<GOAL>max a⁻¹ 1 = a⁻¹ * max a 1
<VAR>α : Type u_1<VAR>LinearOrderedCommGroup α<VAR>a b : α<GOAL>min 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>LinearOrderedCommGroup α<VAR>a b : α<GOAL>max a⁻¹ b⁻¹ = (min a b)⁻¹
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b : α<GOAL>max (-a) (-b) = -min a b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b c : α<GOAL>min (a - c) (b - c) = min a b - c
<VAR>α : Type u_1<VAR>LinearOrderedCommGroup α<VAR>a b c : α<GOAL>min (a / c) (b / c) = min a b / c
<VAR>α : Type u_1<VAR>LinearOrderedCommGroup α<VAR>a b c : α<GOAL>max (a / c) (b / c) = max a b / c
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b c : α<GOAL>max (a - c) (b - c) = max a b - c
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b c : α<GOAL>min (a - b) (a - c) = a - max b c
<VAR>α : Type u_1<VAR>LinearOrderedCommGroup α<VAR>a b c : α<GOAL>min (a / b) (a / c) = a / max b c
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b c : α<GOAL>max (a - b) (a - c) = a - min b c
<VAR>α : Type u_1<VAR>LinearOrderedCommGroup α<VAR>a b c : α<GOAL>max (a / b) (a / c) = a / min b c
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b c d : α<GOAL>max a b - max c d ≤ max (a - c) (b - d)
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b c d : α<GOAL>|max a b - max c d| ≤ max |a - c| |b - d|
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b c d : α<GOAL>|min a b - min c d| ≤ max |a - c| |b - d|
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b c : α<GOAL>|max a c - max b c| ≤ |a - b|
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>a : α<VAR>m n : ℤ<VAR>ha : 1 ≤ a<VAR>h : m ≤ n<GOAL>a ^ m ≤ a ^ n
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>a : α<VAR>n : ℤ<VAR>ha : 1 ≤ a<VAR>hn : n ≤ 0<GOAL>a ^ n ≤ 1
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>a : α<VAR>n : ℤ<VAR>ha : 1 ≤ a<VAR>hn : 0 ≤ n<GOAL>1 ≤ a ^ n
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>a : ℕ<VAR>h : 0 < a<VAR>n : ℤ<GOAL>0 < ↑a ^ n
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>a : ℕ<VAR>h : 0 < a<VAR>n : ℤ<GOAL>↑a ^ n ≠ 0
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>a : α<VAR>ha : 1 < a<VAR>n : ℤ<GOAL>0 < n → 1 < a ^ n
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>a : α<VAR>hx : 1 < a<GOAL>StrictMono fun x => a ^ x
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>a : α<VAR>h₀ : 0 < a<VAR>h₁ : a < 1<GOAL>StrictAnti fun x => a ^ x
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>a : α<VAR>m n : ℤ<VAR>hx : 1 < a<GOAL>a ^ m < a ^ n ↔ m < n
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>a : α<VAR>m n : ℤ<VAR>hx : 1 < a<GOAL>a ^ m ≤ a ^ n ↔ m ≤ n
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>a b : α<VAR>ha : 0 ≤ a<VAR>hb : 1 ≤ b<VAR>k : ℕ<GOAL>a / b ^ k ≤ a
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>a : α<VAR>h₀ : 0 < a<VAR>h₁ : a ≠ 1<GOAL>Function.Injective fun x => a ^ x
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>a : α<VAR>m n : ℤ<VAR>h₀ : 0 < a<VAR>h₁ : a ≠ 1<GOAL>a ^ m = a ^ n ↔ m = n
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>x : α<VAR>hx : 1 ≤ x<VAR>a b c : ℤ<VAR>h : min a b ≤ c<GOAL>x ^ (-c) ≤ max (x ^ (-a)) (x ^ (-b))
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>x : α<VAR>hx : 1 < x<VAR>a b c : ℤ<GOAL>x ^ (-c) ≤ max (x ^ (-a)) (x ^ (-b)) ↔ min a b ≤ c
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>n : ℤ<VAR>hn : Even n<VAR>a : α<GOAL>0 ≤ a ^ n
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a : α<GOAL>0 ≤ a ^ 2
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a : α<GOAL>0 ≤ a ^ (-2)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a : α<VAR>n : ℤ<VAR>hn : Even n<VAR>ha : a ≠ 0<GOAL>0 < a ^ n
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a : α<VAR>ha : a ≠ 0<GOAL>0 < a ^ 2
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a : α<VAR>n : ℤ<VAR>hn : Even n<VAR>h : n ≠ 0<GOAL>0 < a ^ n ↔ a ≠ 0
<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