ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝¹ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c c₁ c₂ : ℝ≥0<VAR>ε ε₁ ε₂ : ℝ<VAR>π₁✝ π₂✝ : TaggedPrepartition I<VAR>inst✝ : CompleteSpace F<VAR>h : Integrable I l f vol<VAR>π₁ π₂ : Prepartition I<VAR>hU : π₁.iUnion = π₂.iUnion<GOAL>Tendsto (integralSum f vol) (l.toFilteriUnion I π₁) (𝓝 (∑ J ∈ π₂.boxes, integral J l f vol))
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝¹ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c c₁ c₂ : ℝ≥0<VAR>ε ε₁ ε₂ : ℝ<VAR>π₁✝ π₂✝ : TaggedPrepartition I<VAR>inst✝ : CompleteSpace F<VAR>h : Integrable I l f vol<VAR>π₁ π₂ : Prepartition I<VAR>hU : π₁.iUnion = π₂.iUnion<GOAL>Tendsto (integralSum f vol) (l.toFilteriUnion I π₂) (𝓝 (∑ J ∈ π₂.boxes, integral J l f vol))
<VAR>α : Type u_1<VAR>inst✝ : HeytingAlgebra α<VAR>a b : α<GOAL>IsRegular ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u v s : Set α<GOAL>TotallyDisconnectedSpace ↑s ↔ IsTotallyDisconnected s
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup V<VAR>inst✝⁵ : NormedSpace ℝ V<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>inst✝ : SecondCountableTopology V<VAR>μ : Measure V<VAR>hf : Integrable f μ<VAR>hf' : Integrable (fun v => ‖v‖ * ‖f v‖) μ<VAR>w : W<GOAL>fderiv ℝ (fourierIntegral 𝐞 μ L.toLinearMap₂ f) w = fourierIntegral 𝐞 μ L.toLinearMap₂ (fourierSMulRight L f) w
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>A✝ : Matrix n n α<VAR>inst✝¹ : Star α<VAR>inst✝ : Star β<VAR>A : Matrix n n α<VAR>h : Aᵀ.IsHermitian<GOAL>A.IsHermitian
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>A✝ : Matrix n n α<VAR>inst✝¹ : Star α<VAR>inst✝ : Star β<VAR>A : Matrix n n α<VAR>h : Aᵀ.IsHermitian<GOAL>Aᵀᵀ.IsHermitian
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LocalRing R<VAR>inst✝ : IsNoetherianRing R<VAR>M : Submodule R ↥(maximalIdeal R)<GOAL>Submodule.map (maximalIdeal R).toCotangent M = ⊤ ↔ M = ⊤
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LocalRing R<VAR>inst✝ : IsNoetherianRing R<VAR>M : Submodule R ↥(maximalIdeal R)<VAR>H : Submodule.map (maximalIdeal R).toCotangent M = ⊤<GOAL>⊤ ≤ M
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LocalRing R<VAR>inst✝ : IsNoetherianRing R<VAR>M : Submodule R ↥(maximalIdeal R)<VAR>H : Submodule.map (maximalIdeal R).toCotangent M = ⊤<GOAL>Submodule.map (Submodule.subtype (maximalIdeal R)) ⊤ ≤ Submodule.map (Submodule.subtype (maximalIdeal R)) M
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LocalRing R<VAR>inst✝ : IsNoetherianRing R<VAR>M : Submodule R ↥(maximalIdeal R)<VAR>H : Submodule.map (maximalIdeal R).toCotangent M = ⊤<GOAL>maximalIdeal R ≤ Submodule.map (Submodule.subtype (maximalIdeal R)) M
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LocalRing R<VAR>inst✝ : IsNoetherianRing R<VAR>M : Submodule R ↥(maximalIdeal R)<VAR>H : Submodule.map (maximalIdeal R).toCotangent M = ⊤<GOAL>maximalIdeal R ≤ Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔ maximalIdeal R • maximalIdeal R
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : LocallyFiniteOrderBot α<VAR>a : α<GOAL>(Iio a).card = (Iic a).card - 1
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>a : ZMod n<GOAL>↑a.valMinAbs.natAbs = if a.val ≤ n / 2 then a else -a
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>a : ZMod n<VAR>this : ↑a.val - ↑n ≤ 0<GOAL>↑a.valMinAbs.natAbs = if a.val ≤ n / 2 then a else -a
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>a : ZMod n<VAR>this : ↑a.val - ↑n ≤ 0<GOAL>↑(if a.val ≤ n / 2 then ↑a.val else ↑a.val - ↑n).natAbs = if a.val ≤ n / 2 then a else -a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<GOAL>CompleteSpace (SeparationQuotient α) ↔ CompleteSpace α
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>inst✝ : SigmaCompactSpace X<VAR>K : CompactExhaustion X<VAR>s : Set X<VAR>hs : IsCompact s<GOAL>∃ n, s ⊆ interior (K n)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>inst✝ : SigmaCompactSpace X<VAR>K : CompactExhaustion X<VAR>s : Set X<VAR>hs : IsCompact s<GOAL>s ⊆ ⋃ i, (interior ∘ ⇑K) i
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>inst✝ : SigmaCompactSpace X<VAR>K : CompactExhaustion X<VAR>s : Set X<VAR>hs : IsCompact s<GOAL>Directed (fun x x_1 => x ⊆ x_1) (interior ∘ ⇑K)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F : C ⥤ Type w<VAR>fst✝ : C<VAR>snd✝¹ snd✝ : F.obj fst✝<VAR>h₂ : F.map (eqToHom ⋯) ⟨fst✝, snd✝¹⟩.snd = ⟨fst✝, snd✝⟩.snd<GOAL>⟨fst✝, snd✝¹⟩ = ⟨fst✝, snd✝⟩
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F : C ⥤ Type w<VAR>fst✝ : C<VAR>snd✝¹ snd✝ : F.obj fst✝<VAR>h₂ : snd✝¹ = snd✝<GOAL>⟨fst✝, snd✝¹⟩ = ⟨fst✝, snd✝⟩
<VAR>a x✝ z x : ℂ<VAR>h : ¬x = 0<GOAL>Real.tan x.arg = x.im / x.re
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>a✝ b✝ c a b : G<GOAL>a * b⁻¹ * b = a
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : AddCommMonoid B<VAR>inst✝² : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i : ι<VAR>g : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝¹ : Fintype α<VAR>inst✝ : AddCommMonoid M<VAR>f : α → M<GOAL>equivFunOnFinite.symm f = ∑ a : α, single a (f a)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : AddCommMonoid B<VAR>inst✝² : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i : ι<VAR>g : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝¹ : Fintype α<VAR>inst✝ : AddCommMonoid M<VAR>f : α → M<GOAL>∑ a : α, single a ((equivFunOnFinite.symm f) a) = ∑ a : α, single a (f a)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : Infinite R<VAR>σ : Type u_2<VAR>p : MvPolynomial σ R<GOAL>∀ (x : σ → R), (eval x) p = (eval x) p
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>n : ℤ<GOAL>↑n.natAbs = ↑|n|
<VAR>α : Type u_1<VAR>inst✝³ : Group α<VAR>inst✝² : LinearOrder α<VAR>a✝ b✝ : α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<GOAL>a⁻¹ < b ∧ a < b ↔ b⁻¹ < a ∧ a < b
<VAR>a b : ℤ<VAR>h : a * b = 0<VAR>hlt₁ : 0 < a<VAR>hlt₂ : 0 < b<GOAL>a = 0 ∨ b = 0
<VAR>a b : ℤ<VAR>h : a * b = 0<VAR>hlt₁ : 0 < a<VAR>hlt₂ : 0 < b<VAR>this : 0 < a * b<GOAL>a = 0 ∨ b = 0
<VAR>a b : ℤ<VAR>h : a * b = 0<VAR>hlt₁ : 0 < a<VAR>hlt₂ : 0 < b<VAR>this : 0 < 0<GOAL>a = 0 ∨ b = 0
<VAR>a b : ℤ<VAR>h : a * b = 0<VAR>hlt₁ : 0 < a<VAR>hgt₂ : b < 0<GOAL>a = 0 ∨ b = 0
<VAR>a b : ℤ<VAR>h : a * b = 0<VAR>hlt₁ : 0 < a<VAR>hgt₂ : b < 0<VAR>this : 0 > a * b<GOAL>a = 0 ∨ b = 0
<VAR>a b : ℤ<VAR>h : a * b = 0<VAR>hlt₁ : 0 < a<VAR>hgt₂ : b < 0<VAR>this : 0 > 0<GOAL>a = 0 ∨ b = 0
<VAR>a b : ℤ<VAR>h : a * b = 0<VAR>hgt₁ : a < 0<VAR>hlt₂ : 0 < b<GOAL>a = 0 ∨ b = 0
<VAR>a b : ℤ<VAR>h : a * b = 0<VAR>hgt₁ : a < 0<VAR>hlt₂ : 0 < b<VAR>this : 0 > a * b<GOAL>a = 0 ∨ b = 0
<VAR>a b : ℤ<VAR>h : a * b = 0<VAR>hgt₁ : a < 0<VAR>hlt₂ : 0 < b<VAR>this : 0 > 0<GOAL>a = 0 ∨ b = 0
<VAR>a b : ℤ<VAR>h : a * b = 0<VAR>hgt₁ : a < 0<VAR>hgt₂ : b < 0<GOAL>a = 0 ∨ b = 0
<VAR>a b : ℤ<VAR>h : a * b = 0<VAR>hgt₁ : a < 0<VAR>hgt₂ : b < 0<VAR>this : 0 < a * b<GOAL>a = 0 ∨ b = 0
<VAR>a b : ℤ<VAR>h : a * b = 0<VAR>hgt₁ : a < 0<VAR>hgt₂ : b < 0<VAR>this : 0 < 0<GOAL>a = 0 ∨ b = 0
<VAR>R✝ : Type u<VAR>S : Type u_1<VAR>σ✝ : Type v<VAR>M : Type w<VAR>inst✝⁵ : CommRing R✝<VAR>inst✝⁴ : CommRing S<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R✝ M<VAR>r✝ : R✝<VAR>R : Type u<VAR>σ : Type v<VAR>r : R<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Fintype σ<GOAL>Prime (C r) ↔ Prime r
<VAR>R✝ : Type u<VAR>S : Type u_1<VAR>σ✝ : Type v<VAR>M : Type w<VAR>inst✝⁵ : CommRing R✝<VAR>inst✝⁴ : CommRing S<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R✝ M<VAR>r✝ : R✝<VAR>R : Type u<VAR>σ : Type v<VAR>r : R<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Fintype σ<GOAL>Prime ((renameEquiv R (Fintype.equivFin σ)).toMulEquiv (C r)) ↔ Prime r
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddCommMonoid A<VAR>inst✝ : HasShift C A<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>i j : A<GOAL>(shiftFunctor C j).map ((shiftFunctor C i).map f) = (shiftComm X i j).hom ≫ (shiftFunctor C i).map ((shiftFunctor C j).map f) ≫ (shiftComm Y j i).hom
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddCommMonoid A<VAR>inst✝ : HasShift C A<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>i j : A<GOAL>(shiftFunctor C j).map ((shiftFunctor C i).map f) = (shiftFunctor C i ⋙ shiftFunctor C j).map f ≫ (shiftFunctorComm C i j).hom.app Y ≫ (shiftComm Y i j).symm.hom
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddCommMonoid A<VAR>inst✝ : HasShift C A<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>i j : A<GOAL>(shiftFunctor C j).map ((shiftFunctor C i).map f) = (shiftFunctor C j).map ((shiftFunctor C i).map f) ≫ (shiftFunctorComm C i j).hom.app Y ≫ (shiftFunctorComm C i j).inv.app Y
<VAR>b o : Ordinal.{u_2}<VAR>C : Ordinal.{u_2} → Sort u_1<VAR>ho : o ≠ 0<VAR>H0 : C 0<VAR>H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o<GOAL>b.CNFRec H0 H o = H o ho (b.CNFRec H0 H (o % b ^ log b o))
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG✝ : G.LocalInvariantProp G' P<VAR>hG : G.LocalInvariantProp G Q<VAR>hQ : ∀ (y : H), Q id univ y<GOAL>LiftProp Q id
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG✝ : G.LocalInvariantProp G' P<VAR>hG : G.LocalInvariantProp G Q<VAR>hQ : ∀ (y : H), Q id univ y<GOAL>∀ (x : M), Q (↑(chartAt H (id x)) ∘ id ∘ ↑(chartAt H x).symm) univ (↑(chartAt H x) x)
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>V₃ : Type u_6<VAR>P₃ : Type u_7<VAR>inst✝⁹ : Ring k<VAR>inst✝⁸ : AddCommGroup V₁<VAR>inst✝⁷ : Module k V₁<VAR>inst✝⁶ : AffineSpace V₁ P₁<VAR>inst✝⁵ : AddCommGroup V₂<VAR>inst✝⁴ : Module k V₂<VAR>inst✝³ : AffineSpace V₂ P₂<VAR>inst✝² : AddCommGroup V₃<VAR>inst✝¹ : Module k V₃<VAR>inst✝ : AffineSpace V₃ P₃<VAR>f : P₁ →ᵃ[k] P₂<VAR>s : Set P₁<VAR>e : P₁ ≃ᵃ[k] P₂<GOAL>affineSpan k s = ⊤ ↔ affineSpan k (⇑e '' s) = ⊤
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>V₃ : Type u_6<VAR>P₃ : Type u_7<VAR>inst✝⁹ : Ring k<VAR>inst✝⁸ : AddCommGroup V₁<VAR>inst✝⁷ : Module k V₁<VAR>inst✝⁶ : AffineSpace V₁ P₁<VAR>inst✝⁵ : AddCommGroup V₂<VAR>inst✝⁴ : Module k V₂<VAR>inst✝³ : AffineSpace V₂ P₂<VAR>inst✝² : AddCommGroup V₃<VAR>inst✝¹ : Module k V₃<VAR>inst✝ : AffineSpace V₃ P₃<VAR>f : P₁ →ᵃ[k] P₂<VAR>s : Set P₁<VAR>e : P₁ ≃ᵃ[k] P₂<GOAL>affineSpan k (⇑e '' s) = ⊤ → affineSpan k s = ⊤
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>V₃ : Type u_6<VAR>P₃ : Type u_7<VAR>inst✝⁹ : Ring k<VAR>inst✝⁸ : AddCommGroup V₁<VAR>inst✝⁷ : Module k V₁<VAR>inst✝⁶ : AffineSpace V₁ P₁<VAR>inst✝⁵ : AddCommGroup V₂<VAR>inst✝⁴ : Module k V₂<VAR>inst✝³ : AffineSpace V₂ P₂<VAR>inst✝² : AddCommGroup V₃<VAR>inst✝¹ : Module k V₃<VAR>inst✝ : AffineSpace V₃ P₃<VAR>f : P₁ →ᵃ[k] P₂<VAR>s : Set P₁<VAR>e : P₁ ≃ᵃ[k] P₂<VAR>h : affineSpan k (⇑e '' s) = ⊤<GOAL>affineSpan k s = ⊤
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>V₃ : Type u_6<VAR>P₃ : Type u_7<VAR>inst✝⁹ : Ring k<VAR>inst✝⁸ : AddCommGroup V₁<VAR>inst✝⁷ : Module k V₁<VAR>inst✝⁶ : AffineSpace V₁ P₁<VAR>inst✝⁵ : AddCommGroup V₂<VAR>inst✝⁴ : Module k V₂<VAR>inst✝³ : AffineSpace V₂ P₂<VAR>inst✝² : AddCommGroup V₃<VAR>inst✝¹ : Module k V₃<VAR>inst✝ : AffineSpace V₃ P₃<VAR>f : P₁ →ᵃ[k] P₂<VAR>s : Set P₁<VAR>e : P₁ ≃ᵃ[k] P₂<VAR>h : affineSpan k (⇑e '' s) = ⊤<VAR>this : s = ⇑e.symm '' (⇑e '' s)<GOAL>affineSpan k s = ⊤
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>V₃ : Type u_6<VAR>P₃ : Type u_7<VAR>inst✝⁹ : Ring k<VAR>inst✝⁸ : AddCommGroup V₁<VAR>inst✝⁷ : Module k V₁<VAR>inst✝⁶ : AffineSpace V₁ P₁<VAR>inst✝⁵ : AddCommGroup V₂<VAR>inst✝⁴ : Module k V₂<VAR>inst✝³ : AffineSpace V₂ P₂<VAR>inst✝² : AddCommGroup V₃<VAR>inst✝¹ : Module k V₃<VAR>inst✝ : AffineSpace V₃ P₃<VAR>f : P₁ →ᵃ[k] P₂<VAR>s : Set P₁<VAR>e : P₁ ≃ᵃ[k] P₂<VAR>h : affineSpan k (⇑e '' s) = ⊤<VAR>this : s = ⇑e.symm '' (⇑e '' s)<GOAL>affineSpan k (⇑e.symm '' (⇑e '' s)) = ⊤
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>p : ℕ<VAR>HF : CharP F p<VAR>f : F[X]<VAR>hf : Irreducible f<VAR>H : derivative f = 0<GOAL>f.Separable ∨ ¬f.Separable ∧ ∃ g, Irreducible g ∧ (expand F p) g = f
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>f : F[X]<VAR>hf : Irreducible f<VAR>H : derivative f = 0<VAR>HF : CharP F 0<GOAL>f.Separable ∨ ¬f.Separable ∧ ∃ g, Irreducible g ∧ (expand F 0) g = f
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>p : ℕ<VAR>HF : CharP F p<VAR>f : F[X]<VAR>hf : Irreducible f<VAR>H : derivative f = 0<VAR>hp : p > 0<GOAL>f.Separable ∨ ¬f.Separable ∧ ∃ g, Irreducible g ∧ (expand F p) g = f
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>p : ℕ<VAR>HF : CharP F p<VAR>f : F[X]<VAR>hf : Irreducible f<VAR>H : derivative f = 0<VAR>hp : p > 0<VAR>this : IsLocalRingHom ↑(expand F p)<GOAL>f.Separable ∨ ¬f.Separable ∧ ∃ g, Irreducible g ∧ (expand F p) g = f
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>a✝ : α<VAR>l✝ : List α<VAR>inst✝ : IsRefl α r<VAR>l : List α<VAR>h : Sorted r l<VAR>a b : Fin l.length<VAR>hab : a ≤ b<GOAL>r (l.get a) (l.get b)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>a✝ : α<VAR>l✝ : List α<VAR>inst✝ : IsRefl α r<VAR>l : List α<VAR>h : Sorted r l<VAR>a : Fin l.length<VAR>hab : a ≤ a<GOAL>r (l.get a) (l.get a)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>a✝ : α<VAR>l✝ : List α<VAR>inst✝ : IsRefl α r<VAR>l : List α<VAR>h : Sorted r l<VAR>a b : Fin l.length<VAR>hab : a ≤ b<VAR>hlt : a < b<GOAL>r (l.get a) (l.get b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : Zero M<VAR>f g : α →₀ M<VAR>x✝ : f.support = g.support ∧ ∀ x ∈ f.support, f x = g x<VAR>h₁ : f.support = g.support<VAR>h₂ : ∀ x ∈ f.support, f x = g x<VAR>a : α<GOAL>f a = g a
<VAR>m n a b c d✝ : ℤ<VAR>h : a ≡ b [ZMOD n]<VAR>d : ℕ<VAR>hd : a ^ d ≡ b ^ d [ZMOD n]<GOAL>a ^ (d + 1) ≡ b ^ (d + 1) [ZMOD n]
<VAR>m n a b c d✝ : ℤ<VAR>h : a ≡ b [ZMOD n]<VAR>d : ℕ<VAR>hd : a ^ d ≡ b ^ d [ZMOD n]<GOAL>a ^ d * a ≡ b ^ d * b [ZMOD n]
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>f : ℕ → R<GOAL>(ArithmeticFunction.prodPrimeFactors f).IsMultiplicative
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>f : ℕ → R<GOAL>(ArithmeticFunction.prodPrimeFactors f) 1 = 1 ∧ ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → m.Coprime n → (ArithmeticFunction.prodPrimeFactors f) (m * n) = (ArithmeticFunction.prodPrimeFactors f) m * (ArithmeticFunction.prodPrimeFactors f) n
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>f : ℕ → R<GOAL>∀ {m n : ℕ}, ¬m = 0 → ¬n = 0 → m.Coprime n → (ArithmeticFunction.prodPrimeFactors f) (m * n) = (ArithmeticFunction.prodPrimeFactors f) m * (ArithmeticFunction.prodPrimeFactors f) n
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>f : ℕ → R<VAR>x y : ℕ<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<VAR>hxy : x.Coprime y<GOAL>(ArithmeticFunction.prodPrimeFactors f) (x * y) = (ArithmeticFunction.prodPrimeFactors f) x * (ArithmeticFunction.prodPrimeFactors f) y
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>f : ℕ → R<VAR>x y : ℕ<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<VAR>hxy : x.Coprime y<VAR>hxy₀ : x * y ≠ 0<GOAL>(ArithmeticFunction.prodPrimeFactors f) (x * y) = (ArithmeticFunction.prodPrimeFactors f) x * (ArithmeticFunction.prodPrimeFactors f) y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f g : ↥(Lp β 1 μ)<GOAL>edist f g = ∫⁻ (a : α), edist (↑↑f a) (↑↑g a) ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f g : ↥(Lp β 1 μ)<GOAL>(if 1 = ⊤ then eLpNormEssSup (↑↑f - ↑↑g) μ else ∫⁻ (a : α), ↑‖↑↑f a - ↑↑g a‖₊ ∂μ) = ∫⁻ (a : α), edist (↑↑f a) (↑↑g a) ∂μ
<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>s : AffineSubspace ℝ P<VAR>ps : Set P<VAR>h : ps ⊆ ↑s<VAR>inst✝¹ : Nonempty ↥s<VAR>n : ℕ<VAR>inst✝ : FiniteDimensional ℝ ↥s.direction<VAR>hd : finrank ℝ ↥s.direction = n<VAR>hc : Cospherical ps<VAR>sx₁ sx₂ : Simplex ℝ P n<VAR>hsx₁ : Set.range sx₁.points ⊆ ps<VAR>hsx₂ : Set.range sx₂.points ⊆ ps<GOAL>sx₁.circumradius = sx₂.circumradius
<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>s : AffineSubspace ℝ P<VAR>ps : Set P<VAR>h : ps ⊆ ↑s<VAR>inst✝¹ : Nonempty ↥s<VAR>n : ℕ<VAR>inst✝ : FiniteDimensional ℝ ↥s.direction<VAR>hd : finrank ℝ ↥s.direction = n<VAR>hc : Cospherical ps<VAR>sx₁ sx₂ : Simplex ℝ P n<VAR>hsx₁ : Set.range sx₁.points ⊆ ps<VAR>hsx₂ : Set.range sx₂.points ⊆ ps<VAR>r : ℝ<VAR>hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r<GOAL>sx₁.circumradius = sx₂.circumradius
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP✝ : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>inst✝ : Nonempty α<VAR>hP : P.IsEquipartition<VAR>hP₇ : 7 ≤ P.parts.card<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPG : ¬P.IsUniform G ε<VAR>hε₀ : 0 ≤ ε<VAR>hε₁ : ε ≤ 1<GOAL>↑(P.energy G) + ε ^ 5 / 4 ≤ ↑((increment hP G ε).energy G)
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP✝ : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>inst✝ : Nonempty α<VAR>hP : P.IsEquipartition<VAR>hP₇ : 7 ≤ P.parts.card<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPG : ¬P.IsUniform G ε<VAR>hε₀ : 0 ≤ ε<VAR>hε₁ : ε ≤ 1<GOAL>(∑ x ∈ P.parts.offDiag, ↑(G.edgeDensity x.1 x.2) ^ 2 + ↑P.parts.card ^ 2 * (ε ^ 5 / 4)) / ↑P.parts.card ^ 2 ≤ (∑ x ∈ P.parts.offDiag.attach, (∑ i ∈ SzemerediRegularity.distinctPairs hP G ε x, ↑(G.edgeDensity i.1 i.2) ^ 2) / 16 ^ P.parts.card) / ↑P.parts.card ^ 2
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP✝ : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>inst✝ : Nonempty α<VAR>hP : P.IsEquipartition<VAR>hP₇ : 7 ≤ P.parts.card<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPG : ¬P.IsUniform G ε<VAR>hε₀ : 0 ≤ ε<VAR>hε₁ : ε ≤ 1<GOAL>∑ x ∈ P.parts.offDiag, ↑(G.edgeDensity x.1 x.2) ^ 2 + ↑P.parts.card ^ 2 * (ε ^ 5 / 4) ≤ ∑ x ∈ P.parts.offDiag.attach, (∑ i ∈ SzemerediRegularity.distinctPairs hP G ε x, ↑(G.edgeDensity i.1 i.2) ^ 2) / 16 ^ P.parts.card
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP✝ : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>inst✝ : Nonempty α<VAR>hP : P.IsEquipartition<VAR>hP₇ : 7 ≤ P.parts.card<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPG : ↑P.parts.offDiag.card * ε < ↑(P.nonUniforms G ε).card<VAR>hε₀ : 0 ≤ ε<VAR>hε₁ : ε ≤ 1<GOAL>∑ x ∈ P.parts.offDiag, ↑(G.edgeDensity x.1 x.2) ^ 2 + ↑P.parts.card ^ 2 * (ε ^ 5 / 4) ≤ ∑ x ∈ P.parts.offDiag.attach, (∑ i ∈ SzemerediRegularity.distinctPairs hP G ε x, ↑(G.edgeDensity i.1 i.2) ^ 2) / 16 ^ P.parts.card
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP✝ : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>inst✝ : Nonempty α<VAR>hP : P.IsEquipartition<VAR>hP₇ : 7 ≤ P.parts.card<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPG : ↑P.parts.offDiag.card * ε < ↑(P.nonUniforms G ε).card<VAR>hε₀ : 0 ≤ ε<VAR>hε₁ : ε ≤ 1<GOAL>↑P.parts.card ^ 2 * (ε ^ 5 / 4) ≤ ↑(P.nonUniforms G ε).card * (ε ^ 4 / 3) - ↑P.parts.offDiag.card * (ε ^ 5 / 25)
<VAR>n : ℕ<GOAL>(ack 0 n + 1) ^ 2 ≤ ack (0 + 3) n
<VAR>m : ℕ<GOAL>(ack (m + 1) 0 + 1) ^ 2 ≤ ack (m + 1 + 3) 0
<VAR>m : ℕ<GOAL>(ack m 1 + 1) ^ 2 ≤ ack (m + 3) 1
<VAR>m n : ℕ<GOAL>(ack (m + 1) (n + 1) + 1) ^ 2 ≤ ack (m + 1 + 3) (n + 1)
<VAR>m n : ℕ<GOAL>(ack m (ack (m + 1) n) + 1) ^ 2 ≤ ack (m + 3) (ack (m + 3 + 1) n)
<VAR>m n : ℕ<GOAL>m + 1 ≤ m + 3 + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : TopologicalSpace α<VAR>z : α<VAR>s : Set α<VAR>p : α → Prop<GOAL>(∃ᶠ (x : α) in 𝓝 z, x ∈ s ∧ p x) ↔ ∃ᶠ (x : α) in 𝓝 z, p x ∧ x ∈ s
<VAR>r r₁ r₂ : ℝ≥0<VAR>x y : ℝ<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℝ<VAR>hf : ∀ a ∈ s, 0 ≤ f a<GOAL>(∑ a ∈ s, f a).toNNReal = ∑ a ∈ s, (f a).toNNReal
<VAR>r r₁ r₂ : ℝ≥0<VAR>x y : ℝ<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℝ<VAR>hf : ∀ a ∈ s, 0 ≤ f a<GOAL>∑ i ∈ s, f i = ∑ a ∈ s, ↑(f a).toNNReal
<VAR>i : (toPGame 1).LeftMoves<GOAL>toLeftMovesToPGame.symm i = ⟨0, ⋯⟩
<VAR>α β : Type u<VAR>c : Cardinal.{u_1}<GOAL>1 ≤ c ↔ 0 < c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>xs ys : List α<VAR>n : ℕ<GOAL>map (⇑(Sym2.equivSym α)) xs.sym2 = List.sym 2 xs