ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Ring Fq<VAR>d m : ℕ<VAR>hm : Fintype.card Fq ^ d ≤ m<VAR>b : Fq[X]<VAR>A : Fin m.succ → Fq[X]<VAR>hA : ∀ (i : Fin m.succ), (A i).degree < b.degree<VAR>hb : b ≠ 0<VAR>f : Fin m.succ → Fin d → Fq := fun i j => (A i).coeff (b.natDegree - ↑j.succ)<VAR>this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)<VAR>i₀ i₁ : Fin m.succ<VAR>i_ne : i₀ ≠ i₁<VAR>i_eq : f i₀ = f i₁<VAR>j : ℕ<VAR>hj : b.natDegree - d ≤ j<VAR>hbj : ↑j < ↑b.natDegree<GOAL>(A i₁).coeff j = (A i₀).coeff j
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Ring Fq<VAR>d m : ℕ<VAR>hm : Fintype.card Fq ^ d ≤ m<VAR>b : Fq[X]<VAR>A : Fin m.succ → Fq[X]<VAR>hA : ∀ (i : Fin m.succ), (A i).degree < b.degree<VAR>hb : b ≠ 0<VAR>f : Fin m.succ → Fin d → Fq := fun i j => (A i).coeff (b.natDegree - ↑j.succ)<VAR>this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)<VAR>i₀ i₁ : Fin m.succ<VAR>i_ne : i₀ ≠ i₁<VAR>i_eq : f i₀ = f i₁<VAR>j : ℕ<VAR>hj : b.natDegree - d ≤ j<VAR>hbj✝ : ↑j < ↑b.natDegree<VAR>hbj : j < b.natDegree<GOAL>(A i₁).coeff j = (A i₀).coeff j
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Ring Fq<VAR>d m : ℕ<VAR>hm : Fintype.card Fq ^ d ≤ m<VAR>b : Fq[X]<VAR>A : Fin m.succ → Fq[X]<VAR>hA : ∀ (i : Fin m.succ), (A i).degree < b.degree<VAR>hb : b ≠ 0<VAR>f : Fin m.succ → Fin d → Fq := fun i j => (A i).coeff (b.natDegree - ↑j.succ)<VAR>this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)<VAR>i₀ i₁ : Fin m.succ<VAR>i_ne : i₀ ≠ i₁<VAR>i_eq : f i₀ = f i₁<VAR>j : ℕ<VAR>hj✝ : b.natDegree - d ≤ j<VAR>hbj✝ : ↑j < ↑b.natDegree<VAR>hbj : j < b.natDegree<VAR>hj : b.natDegree - j.succ < d<GOAL>(A i₁).coeff j = (A i₀).coeff j
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Ring Fq<VAR>d m : ℕ<VAR>hm : Fintype.card Fq ^ d ≤ m<VAR>b : Fq[X]<VAR>A : Fin m.succ → Fq[X]<VAR>hA : ∀ (i : Fin m.succ), (A i).degree < b.degree<VAR>hb : b ≠ 0<VAR>f : Fin m.succ → Fin d → Fq := fun i j => (A i).coeff (b.natDegree - ↑j.succ)<VAR>this✝ : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)<VAR>i₀ i₁ : Fin m.succ<VAR>i_ne : i₀ ≠ i₁<VAR>i_eq : f i₀ = f i₁<VAR>j : ℕ<VAR>hj✝ : b.natDegree - d ≤ j<VAR>hbj✝ : ↑j < ↑b.natDegree<VAR>hbj : j < b.natDegree<VAR>hj : b.natDegree - j.succ < d<VAR>this : j = b.natDegree - (b.natDegree - j.succ).succ<GOAL>(A i₁).coeff j = (A i₀).coeff j
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>h : IsUnit A.det<VAR>n : ℕ<GOAL>A ^ (↑n + 1) = A ^ ↑n * A
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>h : IsUnit A.det<VAR>n : ℕ<GOAL>A ^ (-(↑n + 1) + 1) = (A ^ n)⁻¹
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>h : IsUnit A.det<VAR>n : ℕ<GOAL>(A ^ n)⁻¹ = (A * A ^ n)⁻¹ * A
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>h : IsUnit A.det<VAR>n : ℕ<GOAL>(A * A ^ n)⁻¹ * A = A ^ (-(↑n + 1)) * A
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ η : Kernel α α<VAR>μ : Measure α<VAR>inst✝ : IsSFiniteKernel κ<VAR>hκ : κ.Invariant μ<VAR>hη : η.Invariant μ<GOAL>(κ ∘ₖ η).Invariant μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ η : Kernel α α<VAR>μ : Measure α<VAR>inst✝ : IsSFiniteKernel κ<VAR>hκ : κ.Invariant μ<VAR>hη : η.Invariant μ<VAR>h✝ : IsEmpty α<GOAL>(κ ∘ₖ η).Invariant μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ η : Kernel α α<VAR>μ : Measure α<VAR>inst✝ : IsSFiniteKernel κ<VAR>hκ : κ.Invariant μ<VAR>hη : η.Invariant μ<VAR>hα : Nonempty α<GOAL>(κ ∘ₖ η).Invariant μ
<VAR>X : LocallyRingedSpace<VAR>r : ↑(Γ.obj (op X))<VAR>x✝ : ↑X.toTopCat<GOAL>x✝ ∈ X.toΓSpecFun ⁻¹' (basicOpen r).carrier ↔ x✝ ∈ (X.toRingedSpace.basicOpen r).carrier
<VAR>X : LocallyRingedSpace<VAR>r : ↑(Γ.obj (op X))<VAR>x✝ : ↑X.toTopCat<GOAL>x✝ ∈ X.toΓSpecFun ⁻¹' (basicOpen r).carrier ↔ IsUnit ((X.toRingedSpace.presheaf.germ ⟨x✝, ⋯⟩) r)
<GOAL>ConvexOn ℝ (Ioi 0) (log ∘ Gamma)
<VAR>x : ℝ<VAR>hx : x ∈ Ioi 0<VAR>y : ℝ<VAR>hy : y ∈ Ioi 0<VAR>a b : ℝ<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>(log ∘ Gamma) (a • x + b • y) ≤ a • (log ∘ Gamma) x + b • (log ∘ Gamma) y
<VAR>x : ℝ<VAR>hx : x ∈ Ioi 0<VAR>y : ℝ<VAR>hy : y ∈ Ioi 0<VAR>a : ℝ<VAR>ha : 0 < a<VAR>hb : 0 < 1 - a<VAR>hab : a + (1 - a) = 1<GOAL>(log ∘ Gamma) (a • x + (1 - a) • y) ≤ a • (log ∘ Gamma) x + (1 - a) • (log ∘ Gamma) y
<VAR>x : ℝ<VAR>hx : x ∈ Ioi 0<VAR>y : ℝ<VAR>hy : y ∈ Ioi 0<VAR>a : ℝ<VAR>ha : 0 < a<VAR>hb : 0 < 1 - a<VAR>hab : a + (1 - a) = 1<GOAL>log (Gamma (a * x + (1 - a) * y)) ≤ a * log (Gamma x) + (1 - a) * log (Gamma y)
<VAR>x y a : ℝ<VAR>ha : 0 < a<VAR>hb : 0 < 1 - a<VAR>hab : a + (1 - a) = 1<VAR>hx : 0 < x<VAR>hy : 0 < y<GOAL>log (Gamma (a * x + (1 - a) * y)) ≤ a * log (Gamma x) + (1 - a) * log (Gamma y)
<VAR>x y a : ℝ<VAR>ha : 0 < a<VAR>hb : 0 < 1 - a<VAR>hab : a + (1 - a) = 1<VAR>hx : 0 < x<VAR>hy : 0 < y<GOAL>log (Gamma (a * x + (1 - a) * y)) ≤ log (Gamma x ^ a * Gamma y ^ (1 - a))
<VAR>x y a : ℝ<VAR>ha : 0 < a<VAR>hb : 0 < 1 - a<VAR>hab : a + (1 - a) = 1<VAR>hx : 0 < x<VAR>hy : 0 < y<GOAL>Gamma x ^ a ≠ 0
<VAR>x y a : ℝ<VAR>ha : 0 < a<VAR>hb : 0 < 1 - a<VAR>hab : a + (1 - a) = 1<VAR>hx : 0 < x<VAR>hy : 0 < y<GOAL>Gamma y ^ (1 - a) ≠ 0
<VAR>x y a : ℝ<VAR>ha : 0 < a<VAR>hb : 0 < 1 - a<VAR>hab : a + (1 - a) = 1<VAR>hx : 0 < x<VAR>hy : 0 < y<GOAL>0 < Gamma y
<VAR>x y a : ℝ<VAR>ha : 0 < a<VAR>hb : 0 < 1 - a<VAR>hab : a + (1 - a) = 1<VAR>hx : 0 < x<VAR>hy : 0 < y<GOAL>0 < Gamma x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h : c ≤ max a b<GOAL>Ico a b ∪ Ici c = Ici (min a c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>hab : a ≤ b<VAR>h : c ≤ b<GOAL>Ico a b ∪ Ici c = Ici (min a c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>hab : b ≤ a<VAR>h : c ≤ a<GOAL>Ico a b ∪ Ici c = Ici (min a c)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝² : Category.{u_3, u_1} A<VAR>inst✝¹ : Category.{u_4, u_2} B<VAR>F : A ⥤ B<VAR>G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A<VAR>adj₁ : G₁ ⊣ sheafToPresheaf J A<VAR>G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B<VAR>adj₂ : G₂ ⊣ sheafToPresheaf J B<VAR>inst✝ : J.HasSheafCompose F<VAR>P : Cᵒᵖ ⥤ A<GOAL>adj₂.unit.app (P ⋙ F) ≫ (sheafToPresheaf J B).map ((adj₂.homEquiv (((whiskeringRight Cᵒᵖ A B).obj F).obj P) ((G₁ ⋙ sheafCompose J F).obj P)).symm (whiskerRight (adj₁.unit.app P) F)) = whiskerRight (adj₁.unit.app P) F
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>inst✝¹ : CompleteLattice β<VAR>m : MeasurableSpace α<VAR>γ : Type u_3<VAR>inst✝ : CompleteLattice γ<VAR>f : α → β<VAR>μ : Measure α<VAR>g : β ≃o γ<GOAL>g (essSup f μ) = essSup (fun x => g (f x)) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>inst✝¹ : CompleteLattice β<VAR>m : MeasurableSpace α<VAR>γ : Type u_3<VAR>inst✝ : CompleteLattice γ<VAR>f : α → β<VAR>μ : Measure α<VAR>g : β ≃o γ<GOAL>IsBoundedUnder (fun x x_1 => x ≤ x_1) (ae μ) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>inst✝¹ : CompleteLattice β<VAR>m : MeasurableSpace α<VAR>γ : Type u_3<VAR>inst✝ : CompleteLattice γ<VAR>f : α → β<VAR>μ : Measure α<VAR>g : β ≃o γ<GOAL>IsCoboundedUnder (fun x x_1 => x ≤ x_1) (ae μ) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>inst✝¹ : CompleteLattice β<VAR>m : MeasurableSpace α<VAR>γ : Type u_3<VAR>inst✝ : CompleteLattice γ<VAR>f : α → β<VAR>μ : Measure α<VAR>g : β ≃o γ<GOAL>IsBoundedUnder (fun x x_1 => x ≤ x_1) (ae μ) fun x => g (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>inst✝¹ : CompleteLattice β<VAR>m : MeasurableSpace α<VAR>γ : Type u_3<VAR>inst✝ : CompleteLattice γ<VAR>f : α → β<VAR>μ : Measure α<VAR>g : β ≃o γ<GOAL>IsCoboundedUnder (fun x x_1 => x ≤ x_1) (ae μ) fun x => g (f x)
<VAR>α β : Type u<VAR>a b c : Cardinal.{u_1}<GOAL>a ^ (b * c) = (a ^ b) ^ c
<VAR>α β : Type u<VAR>a b c : Cardinal.{u_1}<GOAL>a ^ (c * b) = (a ^ b) ^ c
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝² : Semiring α<VAR>inst✝¹ : LinearOrder α<VAR>a b c d : α<VAR>inst✝ : PosMulStrictMono α<VAR>h : ∀ (n : ℕ), 0 ≤ a * b ^ n<GOAL>a = 0 ∨ 0 < a ∧ 0 ≤ b
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝² : Semiring α<VAR>inst✝¹ : LinearOrder α<VAR>a b c d : α<VAR>inst✝ : PosMulStrictMono α<VAR>h : ∀ (n : ℕ), 0 ≤ a * b ^ n<VAR>this : 0 ≤ a<GOAL>a = 0 ∨ 0 < a ∧ 0 ≤ b
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝² : Semiring α<VAR>inst✝¹ : LinearOrder α<VAR>a b c d : α<VAR>inst✝ : PosMulStrictMono α<VAR>h : ∀ (n : ℕ), 0 ≤ a * b ^ n<VAR>this : 0 ≤ a<VAR>ha : 0 < a<GOAL>0 ≤ a * b
<VAR>X : Type u_1<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : T2Space X<VAR>inst✝² : LocallyCompactSpace X<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : CompleteSpace E<VAR>ι : Type u_3<VAR>F : ι → C(X, E)<VAR>hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖<GOAL>Summable F
<VAR>X : Type u_1<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : T2Space X<VAR>inst✝² : LocallyCompactSpace X<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : CompleteSpace E<VAR>ι : Type u_3<VAR>F : ι → C(X, E)<VAR>hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖<VAR>K : Set X<VAR>hK : IsCompact K<GOAL>∃ f, Tendsto (fun i => restrict K (∑ b ∈ i, F b)) atTop (𝓝 f)
<VAR>X : Type u_1<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : T2Space X<VAR>inst✝² : LocallyCompactSpace X<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : CompleteSpace E<VAR>ι : Type u_3<VAR>F : ι → C(X, E)<VAR>hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖<VAR>K : Compacts X<GOAL>∃ f, Tendsto (fun i => restrict (↑K) (∑ b ∈ i, F b)) atTop (𝓝 f)
<VAR>X : Type u_1<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : T2Space X<VAR>inst✝² : LocallyCompactSpace X<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : CompleteSpace E<VAR>ι : Type u_3<VAR>F : ι → C(X, E)<VAR>hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖<VAR>K : Compacts X<VAR>A : ∀ (s : Finset ι), restrict (↑K) (∑ i ∈ s, F i) = ∑ i ∈ s, restrict (↑K) (F i)<GOAL>∃ f, Tendsto (fun i => restrict (↑K) (∑ b ∈ i, F b)) atTop (𝓝 f)
<VAR>x y : ℂ<GOAL>abs (cexp x) = abs (cexp y) ↔ x.re = y.re
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : CommSemiring R₁<VAR>inst✝⁴ : AddCommMonoid M₁<VAR>inst✝³ : Module R₁ M₁<VAR>inst✝² : CommSemiring R₂<VAR>inst✝¹ : AddCommMonoid M₂<VAR>inst✝ : Module R₂ M₂<VAR>I₁ : R₁ →+* R<VAR>I₂ : R₂ →+* R<VAR>I₁' : R₁ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M<VAR>h : ∀ (x : M₁), B x = 0 → x = 0<VAR>x : M₁<VAR>hB : ∀ (y : M₂), (B x) y = 0<GOAL>x = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : CommSemiring R₁<VAR>inst✝⁴ : AddCommMonoid M₁<VAR>inst✝³ : Module R₁ M₁<VAR>inst✝² : CommSemiring R₂<VAR>inst✝¹ : AddCommMonoid M₂<VAR>inst✝ : Module R₂ M₂<VAR>I₁ : R₁ →+* R<VAR>I₂ : R₂ →+* R<VAR>I₁' : R₁ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M<VAR>h : ∀ (x : M₁), B x = 0 → x = 0<VAR>x : M₁<VAR>hB : ∀ (y : M₂), (B x) y = 0<VAR>h' : B x = 0<GOAL>x = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S M<VAR>inst✝¹ : SMul S R<VAR>inst✝ : IsScalarTower S R M<VAR>p✝ q : Submodule R M<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>p : ι → Submodule R M<VAR>x : M<GOAL>x ∈ s.inf p ↔ ∀ i ∈ s, x ∈ p i
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c✝ d x✝ y z : P<VAR>r R✝ : ℝ<VAR>c x : P<VAR>R : ℝ<GOAL>dist c (inversion c R x) = R ^ 2 / dist c x
<VAR>G : Type u_1<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Fintype G<VAR>A✝ B : Finset (G × G)<VAR>a b c d x y : G<VAR>n : ℕ<VAR>ε✝ ε : ℝ<VAR>hε : 0 < ε<VAR>hG : cornersTheoremBound (ε / 3) ≤ n<VAR>A : Finset ℕ<VAR>hAn : A ⊆ range n<VAR>hAε : ε * ↑n ≤ ↑A.card<VAR>hA : ThreeAPFree ↑A<GOAL>False
<VAR>G : Type u_1<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Fintype G<VAR>A✝ B : Finset (G × G)<VAR>a b c d x y : G<VAR>n : ℕ<VAR>ε✝ ε : ℝ<VAR>hε : 0 < ε<VAR>hG : cornersTheoremBound (ε / 3) ≤ n<VAR>A : Finset ℕ<VAR>hAn : ↑A ⊆ Set.Iio n<VAR>hAε : ε * ↑n ≤ ↑A.card<VAR>hA : ThreeAPFree ↑A<GOAL>False
<VAR>G : Type u_1<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Fintype G<VAR>A✝ B : Finset (G × G)<VAR>a b c d x y : G<VAR>n : ℕ<VAR>ε✝ ε : ℝ<VAR>hε : 0 < ε<VAR>hG : cornersTheoremBound (ε / 3) ≤ n<VAR>A : Finset ℕ<VAR>hAn : ↑A ⊆ Set.Iio n<VAR>hAε : ε * ↑n ≤ ↑A.card<VAR>hA : ThreeAPFree ↑A<VAR>this : ↑A = Fin.val '' (Nat.cast '' ↑A)<GOAL>False
<VAR>G : Type u_1<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Fintype G<VAR>A✝ B : Finset (G × G)<VAR>a b c d x y : G<VAR>n : ℕ<VAR>ε✝ ε : ℝ<VAR>hε : 0 < ε<VAR>hG : cornersTheoremBound (ε / 3) ≤ n<VAR>A : Finset ℕ<VAR>hAn : ↑A ⊆ Set.Iio n<VAR>hAε : ε * ↑n ≤ ↑A.card<VAR>hA : ThreeAPFree (Fin.val '' (Nat.cast '' ↑A))<VAR>this : ↑A = Fin.val '' (Nat.cast '' ↑A)<GOAL>False
<VAR>G : Type u_1<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Fintype G<VAR>A✝ B : Finset (G × G)<VAR>a b c d x y : G<VAR>n : ℕ<VAR>ε✝ ε : ℝ<VAR>hε : 0 < ε<VAR>hG : cornersTheoremBound (ε / 3) ≤ n<VAR>A : Finset ℕ<VAR>hAn : ↑A ⊆ Set.Iio n<VAR>hAε : ε * ↑n ≤ ↑A.card<VAR>hA : ThreeAPFree (Fin.val '' (Nat.cast '' ↑A))<VAR>this✝ : ↑A = Fin.val '' (Nat.cast '' ↑A)<VAR>this : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val<GOAL>False
<VAR>G : Type u_1<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Fintype G<VAR>A✝ B : Finset (G × G)<VAR>a b c d x y : G<VAR>n : ℕ<VAR>ε✝ ε : ℝ<VAR>hε : 0 < ε<VAR>hG : cornersTheoremBound (ε / 3) ≤ n<VAR>A : Finset ℕ<VAR>hAn : ↑A ⊆ Set.Iio n<VAR>hAε : ε * ↑n ≤ ↑A.card<VAR>hA : ThreeAPFree (Fin.val '' (Nat.cast '' ↑A))<VAR>this✝¹ : ↑A = Fin.val '' (Nat.cast '' ↑A)<VAR>this✝ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val<VAR>this : ThreeAPFree ((fun x => ↑x) '' ↑A)<GOAL>False
<VAR>G : Type u_1<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Fintype G<VAR>A✝ B : Finset (G × G)<VAR>a b c d x y : G<VAR>n : ℕ<VAR>ε✝ ε : ℝ<VAR>hε : 0 < ε<VAR>hG : cornersTheoremBound (ε / 3) ≤ n<VAR>A : Finset ℕ<VAR>hAn : ↑A ⊆ Set.Iio n<VAR>hAε : ε * ↑n ≤ ↑A.card<VAR>hA : ThreeAPFree (Fin.val '' (Nat.cast '' ↑A))<VAR>this✝¹ : ↑A = Fin.val '' (Nat.cast '' ↑A)<VAR>this✝ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val<VAR>this : ThreeAPFree ↑(image (fun x => ↑x) A)<GOAL>False
<VAR>G : Type u_1<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Fintype G<VAR>A✝ B : Finset (G × G)<VAR>a b c d x y : G<VAR>n : ℕ<VAR>ε✝ ε : ℝ<VAR>hε : 0 < ε<VAR>hG : cornersTheoremBound (ε / 3) ≤ n<VAR>A : Finset ℕ<VAR>hAn : ↑A ⊆ Set.Iio n<VAR>hAε : ε * ↑n ≤ ↑A.card<VAR>hA : ThreeAPFree (Fin.val '' (Nat.cast '' ↑A))<VAR>this✝¹ : ↑A = Fin.val '' (Nat.cast '' ↑A)<VAR>this✝ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val<VAR>this : ThreeAPFree ↑(image (fun x => ↑x) A)<GOAL>ε / 3 * ↑(Fintype.card (Fin (2 * n + 1))) ≤ ↑(image (fun x => ↑x) A).card
<VAR>n : ℕ<VAR>α : Type u_1<VAR>l : List α<VAR>c : Composition l.length<VAR>i : ℕ<GOAL>map length (l.splitWrtComposition c) = c.blocks
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{u}<GOAL>(∀ (i : Ordinal.{u}) (h : i < o), f i h < o.bsup f) → (o.bsup f).cof ≤ o.card
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{u}<GOAL>(∀ (i : Ordinal.{u}) (h : i < o), f i h < o.bsup f) → (o.bsup f).cof ≤ Cardinal.lift.{u, u} o.card
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x✝ y z : E<VAR>δ ε a b r : ℝ<VAR>ha : 0 ≤ a<VAR>hr : 0 < r<VAR>this : EqOn (fun x => ‖x‖) id (Ioo a b)<VAR>x : E<GOAL>x ∈ (fun x => ‖x‖) ⁻¹' Ioo (a * r) (b * r) ↔ x ∈ ball 0 (b * r) \ closedBall 0 (a * r)
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>s✝ : Finset ι<VAR>f✝ : ι → α<VAR>β : ι → Type u_5<VAR>s : Finset ι<VAR>g : (i : ι) → Finset (β i)<VAR>f : Sigma β → α<VAR>hs : s.SupIndep fun i => (g i).sup fun b => f ⟨i, b⟩<VAR>hg : ∀ i ∈ s, (g i).SupIndep fun b => f ⟨i, b⟩<VAR>t : Finset ((i : ι) × β i)<VAR>ht : t ⊆ s.sigma g<VAR>i : ι<VAR>b : β i<VAR>hi : ⟨i, b⟩ ∈ s.sigma g<VAR>hit : ⟨i, b⟩ ∉ t<GOAL>Disjoint (f ⟨i, b⟩) (t.sup f)
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>s✝ : Finset ι<VAR>f✝ : ι → α<VAR>β : ι → Type u_5<VAR>s : Finset ι<VAR>g : (i : ι) → Finset (β i)<VAR>f : Sigma β → α<VAR>hs : s.SupIndep fun i => (g i).sup fun b => f ⟨i, b⟩<VAR>hg : ∀ i ∈ s, (g i).SupIndep fun b => f ⟨i, b⟩<VAR>t : Finset ((i : ι) × β i)<VAR>ht : t ⊆ s.sigma g<VAR>i : ι<VAR>b : β i<VAR>hi : ⟨i, b⟩ ∈ s.sigma g<VAR>hit : ⟨i, b⟩ ∉ t<GOAL>∀ ⦃i_1 : (i : ι) × β i⦄, i_1 ∈ t → Disjoint (f ⟨i, b⟩) (f i_1)
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>s✝ : Finset ι<VAR>f✝ : ι → α<VAR>β : ι → Type u_5<VAR>s : Finset ι<VAR>g : (i : ι) → Finset (β i)<VAR>f : Sigma β → α<VAR>hs : s.SupIndep fun i => (g i).sup fun b => f ⟨i, b⟩<VAR>hg : ∀ i ∈ s, (g i).SupIndep fun b => f ⟨i, b⟩<VAR>t : Finset ((i : ι) × β i)<VAR>ht : t ⊆ s.sigma g<VAR>i : ι<VAR>b : β i<VAR>hi : ⟨i, b⟩ ∈ s.sigma g<VAR>hit : ⟨i, b⟩ ∉ t<VAR>j : ι<VAR>c : β j<VAR>hj : ⟨j, c⟩ ∈ t<GOAL>Disjoint (f ⟨i, b⟩) (f ⟨j, c⟩)
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>s✝ : Finset ι<VAR>f✝ : ι → α<VAR>β : ι → Type u_5<VAR>s : Finset ι<VAR>g : (i : ι) → Finset (β i)<VAR>f : Sigma β → α<VAR>hs : s.SupIndep fun i => (g i).sup fun b => f ⟨i, b⟩<VAR>hg : ∀ i ∈ s, (g i).SupIndep fun b => f ⟨i, b⟩<VAR>t : Finset ((i : ι) × β i)<VAR>ht : t ⊆ s.sigma g<VAR>i : ι<VAR>b : β i<VAR>hi : ⟨i, b⟩ ∈ s.sigma g<VAR>hit : ⟨i, b⟩ ∉ t<VAR>j : ι<VAR>c : β j<VAR>hj : ⟨j, c⟩ ∈ t<VAR>hbc : ⟨i, b⟩ ≠ ⟨j, c⟩<GOAL>Disjoint (f ⟨i, b⟩) (f ⟨j, c⟩)
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>s✝ : Finset ι<VAR>f✝ : ι → α<VAR>β : ι → Type u_5<VAR>s : Finset ι<VAR>g : (i : ι) → Finset (β i)<VAR>f : Sigma β → α<VAR>hs : s.SupIndep fun i => (g i).sup fun b => f ⟨i, b⟩<VAR>hg : ∀ i ∈ s, (g i).SupIndep fun b => f ⟨i, b⟩<VAR>t : Finset ((i : ι) × β i)<VAR>ht : t ⊆ s.sigma g<VAR>i : ι<VAR>b : β i<VAR>hi : ⟨i, b⟩ ∈ s.sigma g<VAR>hit : ⟨i, b⟩ ∉ t<VAR>j : ι<VAR>c : β j<VAR>hbc : ⟨i, b⟩ ≠ ⟨j, c⟩<VAR>hj : ⟨j, c⟩ ∈ s.sigma g<GOAL>Disjoint (f ⟨i, b⟩) (f ⟨j, c⟩)
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>s✝ : Finset ι<VAR>f✝ : ι → α<VAR>β : ι → Type u_5<VAR>s : Finset ι<VAR>g : (i : ι) → Finset (β i)<VAR>f : Sigma β → α<VAR>hs : s.SupIndep fun i => (g i).sup fun b => f ⟨i, b⟩<VAR>hg : ∀ i ∈ s, (g i).SupIndep fun b => f ⟨i, b⟩<VAR>t : Finset ((i : ι) × β i)<VAR>ht : t ⊆ s.sigma g<VAR>i : ι<VAR>b : β i<VAR>hi : ⟨i, b⟩.fst ∈ s ∧ ⟨i, b⟩.snd ∈ g ⟨i, b⟩.fst<VAR>hit : ⟨i, b⟩ ∉ t<VAR>j : ι<VAR>c : β j<VAR>hbc : ⟨i, b⟩ ≠ ⟨j, c⟩<VAR>hj : ⟨j, c⟩.fst ∈ s ∧ ⟨j, c⟩.snd ∈ g ⟨j, c⟩.fst<GOAL>Disjoint (f ⟨i, b⟩) (f ⟨j, c⟩)
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>s✝ : Finset ι<VAR>f✝ : ι → α<VAR>β : ι → Type u_5<VAR>s : Finset ι<VAR>g : (i : ι) → Finset (β i)<VAR>f : Sigma β → α<VAR>hs : s.SupIndep fun i => (g i).sup fun b => f ⟨i, b⟩<VAR>hg : ∀ i ∈ s, (g i).SupIndep fun b => f ⟨i, b⟩<VAR>t : Finset ((i : ι) × β i)<VAR>ht : t ⊆ s.sigma g<VAR>i : ι<VAR>b : β i<VAR>hi : ⟨i, b⟩.fst ∈ s ∧ ⟨i, b⟩.snd ∈ g ⟨i, b⟩.fst<VAR>hit : ⟨i, b⟩ ∉ t<VAR>c : β i<VAR>hbc : ⟨i, b⟩ ≠ ⟨i, c⟩<VAR>hj : ⟨i, c⟩.fst ∈ s ∧ ⟨i, c⟩.snd ∈ g ⟨i, c⟩.fst<GOAL>Disjoint (f ⟨i, b⟩) (f ⟨i, c⟩)
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>s✝ : Finset ι<VAR>f✝ : ι → α<VAR>β : ι → Type u_5<VAR>s : Finset ι<VAR>g : (i : ι) → Finset (β i)<VAR>f : Sigma β → α<VAR>hs : s.SupIndep fun i => (g i).sup fun b => f ⟨i, b⟩<VAR>hg : ∀ i ∈ s, (g i).SupIndep fun b => f ⟨i, b⟩<VAR>t : Finset ((i : ι) × β i)<VAR>ht : t ⊆ s.sigma g<VAR>i : ι<VAR>b : β i<VAR>hi : ⟨i, b⟩.fst ∈ s ∧ ⟨i, b⟩.snd ∈ g ⟨i, b⟩.fst<VAR>hit : ⟨i, b⟩ ∉ t<VAR>j : ι<VAR>c : β j<VAR>hbc : ⟨i, b⟩ ≠ ⟨j, c⟩<VAR>hj : ⟨j, c⟩.fst ∈ s ∧ ⟨j, c⟩.snd ∈ g ⟨j, c⟩.fst<VAR>hij : i ≠ j<GOAL>Disjoint (f ⟨i, b⟩) (f ⟨j, c⟩)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Denumerable α<VAR>inst✝ : Denumerable β<GOAL>ofNat (ℕ × ℕ) = unpair
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Denumerable α<VAR>inst✝ : Denumerable β<VAR>x✝ : ℕ<GOAL>ofNat (ℕ × ℕ) x✝ = unpair x✝
<VAR>x y z : ℤ<GOAL>x * x + y * y = z * z ↔ y * y + x * x = z * z
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>c : 𝕜<VAR>f : ↥(lpMeas F 𝕜 m p μ)<GOAL>↑↑(lpMeasToLpTrim F 𝕜 p μ hm (c • f)) =ᶠ[ae (μ.trim hm)] ↑↑(c • lpMeasToLpTrim F 𝕜 p μ hm f)
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>c : 𝕜<VAR>f : ↥(lpMeas F 𝕜 m p μ)<GOAL>↑↑(lpMeasToLpTrim F 𝕜 p μ hm (c • f)) =ᶠ[ae (μ.trim hm)] c • ↑↑(lpMeasToLpTrim F 𝕜 p μ hm f)
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>c : 𝕜<VAR>f : ↥(lpMeas F 𝕜 m p μ)<GOAL>StronglyMeasurable (c • ↑↑(lpMeasToLpTrim F 𝕜 p μ hm f))