ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>𝕜 : Type u_5<VAR>inst✝ : RCLike 𝕜<VAR>f : α → 𝕜<VAR>hf : Integrable f μ<GOAL>Integrable (fun x => RCLike.re (f x)) μ
<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>𝕜 : Type u_5<VAR>inst✝ : RCLike 𝕜<VAR>f : α → 𝕜<VAR>hf : Memℒp f 1 μ<GOAL>Memℒp (fun x => RCLike.re (f x)) 1 μ
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℕ<GOAL>(W.preΨ' n).coeff ((n ^ 2 - if Even n then 4 else 1) / 2) = ↑(if Even n then n / 2 else n)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℕ<GOAL>↑(if Even n then n / 2 else n) = ↑(WeierstrassCurve.expCoeff n)
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasZeroMorphisms D<VAR>F : C ⥤ D<VAR>X Y : C<VAR>inst✝² : HasBinaryBiproduct X Y<VAR>inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)<VAR>inst✝ : F.PreservesZeroMorphisms<GOAL>F.biprodComparison' X Y ≫ F.biprodComparison X Y = 𝟙 (F.obj X ⊞ F.obj Y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a✝ b✝ c✝ d : G<VAR>n : ℤ<VAR>a b c : G<GOAL>a * c / (b * c) = a / b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a✝ b✝ c✝ d : G<VAR>n : ℤ<VAR>a b c : G<GOAL>a * c / c / b = a / b
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.76698, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S : ShortComplex C<VAR>s : S.Splitting<GOAL>S.g ≫ s.s = 𝟙 S.X₂ - s.r ≫ S.f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<GOAL>s.encard = 1 ↔ ∃ x, s = {x}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>h : s.encard = 1<GOAL>∃ x, s = {x}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>h : s.encard = 1<VAR>x : α<VAR>hx : x ∈ s<GOAL>∃ x, s = {x}
<VAR>a b p q : ℝ<VAR>h : p.IsConjExponent q<GOAL>(ENNReal.ofReal p)⁻¹ + (ENNReal.ofReal q)⁻¹ = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>a : α<VAR>n : ℕ<GOAL>toMultiset (single a n) = n • {a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>a : α<VAR>n : ℕ<GOAL>0 • {a} = 0
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>A : Set Y<VAR>u : Y → β → α<VAR>hA : UniformEquicontinuous (u ∘ Subtype.val)<VAR>hu : Continuous u<GOAL>UniformEquicontinuous (u ∘ Subtype.val)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>A : Set Y<VAR>u : Y → β → α<VAR>hA : UniformEquicontinuousOn (u ∘ Subtype.val) univ<VAR>hu : Continuous u<GOAL>UniformEquicontinuousOn (u ∘ Subtype.val) univ
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>ha : a ≠ ⊤<VAR>hb : b ≠ ⊤<VAR>h : a.toNNReal < b.toNNReal<GOAL>a < b
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>Q : AffineSubspace k P<VAR>p₀ p₁ : P<VAR>c : k<VAR>h₀ : p₀ ∈ Q<VAR>h₁ : p₁ ∈ Q<GOAL>(lineMap p₀ p₁) c ∈ Q
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>Q : AffineSubspace k P<VAR>p₀ p₁ : P<VAR>c : k<VAR>h₀ : p₀ ∈ Q<VAR>h₁ : p₁ ∈ Q<GOAL>c • (p₁ -ᵥ p₀) +ᵥ p₀ ∈ Q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>hf : MapsTo f s t<VAR>f_inj : InjOn f s<GOAL>s.encard ≤ t.encard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>hf : MapsTo f s t<VAR>f_inj : InjOn f s<GOAL>(f '' s).encard ≤ t.encard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>hf : MapsTo f s t<VAR>f_inj : InjOn f s<GOAL>f '' s ⊆ t
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : AddCommMonoid M<VAR>w : σ → M<VAR>i : σ<GOAL>IsWeightedHomogeneous w (X i) (w i)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : AddCommMonoid M<VAR>w : σ → M<VAR>i : σ<GOAL>(weight w) (Finsupp.single i 1) = w i
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁵ : Fintype l<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>inst✝² : Unique ι<VAR>inst✝¹ : SeminormedAddCommGroup α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>A : Matrix m n α<GOAL>‖A‖ ≤ r ↔ ∀ (i : m) (j : n), ‖A i j‖ ≤ r
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>hS : S ∈ rightTransversals ↑H<VAR>g : G<GOAL>(g * (↑(toFun hS g))⁻¹)⁻¹ = ↑(toFun hS g) * g⁻¹
<VAR>x✝ y✝ z : ℝ<VAR>n✝ : ℕ<VAR>x : ℝ<VAR>hx : x ≠ 0<VAR>y : ℝ<VAR>n : ℕ<GOAL>x ^ (y + ↑n) = x ^ y * x ^ n
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : AddCommMonoid N<VAR>n : ℕ<VAR>f : ℕ × ℕ → M<GOAL>∏ p ∈ antidiagonal n, f p.swap = ∏ p ∈ antidiagonal n, f p
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : AddCommMonoid N<VAR>n : ℕ<VAR>f : ℕ × ℕ → M<GOAL>∏ x ∈ antidiagonal n, f ({ toFun := Prod.swap, inj' := ⋯ } x).swap = ∏ p ∈ antidiagonal n, f p
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>x ⊓ y ⊓ z ⊔ x ⊓ y \ z = x ⊓ (y ⊓ z) ⊔ x ⊓ y \ z
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>x ⊓ (y ⊓ z) ⊔ x ⊓ y \ z = x ⊓ (y ⊓ z ⊔ y \ z)
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>x ⊓ (y ⊓ z ⊔ y \ z) = x ⊓ y
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>x ⊓ x ⊓ (y ⊓ z ⊓ y \ z) = ⊥
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>inst✝² : NonAssocSemiring R<VAR>M : Submonoid R<VAR>inst✝¹ : NonAssocSemiring S✝<VAR>inst✝ : NonAssocSemiring T<VAR>ι : Sort u_1<VAR>hι : Nonempty ι<VAR>S : ι → Subsemiring R<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : R<GOAL>x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>inst✝² : NonAssocSemiring R<VAR>M : Submonoid R<VAR>inst✝¹ : NonAssocSemiring S✝<VAR>inst✝ : NonAssocSemiring T<VAR>ι : Sort u_1<VAR>hι : Nonempty ι<VAR>S : ι → Subsemiring R<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : R<GOAL>x ∈ ⨆ i, S i → ∃ i, x ∈ S i
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>inst✝² : NonAssocSemiring R<VAR>M : Submonoid R<VAR>inst✝¹ : NonAssocSemiring S✝<VAR>inst✝ : NonAssocSemiring T<VAR>ι : Sort u_1<VAR>hι : Nonempty ι<VAR>S : ι → Subsemiring R<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : R<VAR>U : Subsemiring R := Subsemiring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubmonoid) ⋯ (⨆ i, (S i).toAddSubmonoid) ⋯<GOAL>x ∈ ⨆ i, S i → ∃ i, x ∈ S i
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>inst✝² : NonAssocSemiring R<VAR>M : Submonoid R<VAR>inst✝¹ : NonAssocSemiring S✝<VAR>inst✝ : NonAssocSemiring T<VAR>ι : Sort u_1<VAR>hι : Nonempty ι<VAR>S : ι → Subsemiring R<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : R<VAR>U : Subsemiring R := Subsemiring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubmonoid) ⋯ (⨆ i, (S i).toAddSubmonoid) ⋯<GOAL>⨆ i, S i ≤ U
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α✝ → α✝ → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>f : Ordinal.{max u v} → Ordinal.{max u w}<VAR>H : IsNormal f<VAR>o : Ordinal.{u}<VAR>α : Type u<VAR>r : α → α → Prop<VAR>x✝ : IsWellOrder α r<VAR>g : (a : Ordinal.{u}) → a < type r → Ordinal.{max u v}<VAR>h : type r ≠ 0<GOAL>f ((type r).bsup g) = (type r).bsup fun a h => f (g a h)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α✝ → α✝ → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>f : Ordinal.{max u v} → Ordinal.{max u w}<VAR>H : IsNormal f<VAR>o : Ordinal.{u}<VAR>α : Type u<VAR>r : α → α → Prop<VAR>x✝ : IsWellOrder α r<VAR>g : (a : Ordinal.{u}) → a < type r → Ordinal.{max u v}<VAR>h : type r ≠ 0<VAR>this : Nonempty α<GOAL>f ((type r).bsup g) = (type r).bsup fun a h => f (g a h)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>s t : Set α<VAR>a b x✝ y✝ : α<VAR>inst✝ : DecidableEq α<VAR>hab : a ≠ b<VAR>x : α<VAR>hx : x ∈ {a, b}<VAR>y : α<VAR>hy : y ∈ {a, b}<GOAL>(swap a b).SameCycle x y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>s t : Set α<VAR>a b x✝ y✝ : α<VAR>inst✝ : DecidableEq α<VAR>hab : a ≠ b<VAR>x : α<VAR>hx : x = a ∨ x = b<VAR>y : α<VAR>hy : y = a ∨ y = b<GOAL>(swap a b).SameCycle x y
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>a b : R<VAR>h : gcd a b = 0<GOAL>a = 0 ∧ b = 0
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<GOAL>gcd 0 0 = 0
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ g : Perm α<VAR>ht : g.IsThreeCycle<GOAL>_root_.orderOf g = 3
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>T : Type u_3<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>g : S →+* T<VAR>f : R →+* S<GOAL>f.SurjectiveOnStalks ↔ ∀ (I : Ideal S) (x : I.IsMaximal), Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f I) I f ⋯)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>T : Type u_3<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>g : S →+* T<VAR>f : R →+* S<VAR>H : ∀ (I : Ideal S) (x : I.IsMaximal), Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f I) I f ⋯)<VAR>I : Ideal S<VAR>hI : I.IsPrime<GOAL>Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f I) I f ⋯)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>T : Type u_3<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>g : S →+* T<VAR>f : R →+* S<VAR>I : Ideal S<VAR>hI : I.IsPrime<VAR>H : ∀ (I : Ideal S), I.IsMaximal → ∀ (s : S), ∃ x r, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x<GOAL>∀ (s : S), ∃ x r, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>T : Type u_3<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>g : S →+* T<VAR>f : R →+* S<VAR>I : Ideal S<VAR>hI : I.IsPrime<VAR>H : ∀ (I : Ideal S), I.IsMaximal → ∀ (s : S), ∃ x r, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x<VAR>s : S<GOAL>∃ x r, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>M✝ : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>T : Type u_3<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>g : S →+* T<VAR>f : R →+* S<VAR>I : Ideal S<VAR>hI : I.IsPrime<VAR>H : ∀ (I : Ideal S), I.IsMaximal → ∀ (s : S), ∃ x r, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x<VAR>s : S<VAR>M : Ideal S<VAR>hM : M.IsMaximal<VAR>hIM : I ≤ M<GOAL>∃ x r, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x
<VAR>d x y : ℤ<GOAL>IsPell { re := x, im := y } ↔ { re := x, im := y } * star { re := x, im := y } = 1
<VAR>d x y : ℤ<GOAL>x * x - y * (d * y) = 1 ↔ x * x + -(y * (d * y)) = 1
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s : Set α<VAR>x a : α<VAR>x✝ : x ∈ a • s<VAR>b : α<VAR>hb : b ∈ s<VAR>Eq : (fun x => a • x) b = x<GOAL>a⁻¹ * x ∈ s
<VAR>R : Type u<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>n : ℕ<GOAL>C a * X ^ (n + 1) = (monomial (n + 1)) a
<VAR>J : Type v<VAR>inst✝² : SmallCategory J<VAR>inst✝¹ : IsCofiltered J<VAR>F : J ⥤ Profinite<VAR>C : Cone F<VAR>α : Type u_1<VAR>inst✝ : Finite α<VAR>hC : IsLimit C<VAR>f : LocallyConstant (↑C.pt.toTop) α<GOAL>∃ j g, LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (C.π.app j) g
<VAR>J : Type v<VAR>inst✝² : SmallCategory J<VAR>inst✝¹ : IsCofiltered J<VAR>F : J ⥤ Profinite<VAR>C : Cone F<VAR>α : Type u_1<VAR>inst✝ : Finite α<VAR>hC : IsLimit C<VAR>f : LocallyConstant (↑C.pt.toTop) α<VAR>val✝ : Fintype α<GOAL>∃ j g, LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (C.π.app j) g
<VAR>J : Type v<VAR>inst✝² : SmallCategory J<VAR>inst✝¹ : IsCofiltered J<VAR>F : J ⥤ Profinite<VAR>C : Cone F<VAR>α : Type u_1<VAR>inst✝ : Finite α<VAR>hC : IsLimit C<VAR>f : LocallyConstant (↑C.pt.toTop) α<VAR>val✝ : Fintype α<VAR>ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1<VAR>ff : α → LocallyConstant (↑C.pt.toTop) (Fin 2) := (LocallyConstant.map ι f).flip<GOAL>∃ j g, LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (C.π.app j) g
<VAR>J : Type v<VAR>inst✝² : SmallCategory J<VAR>inst✝¹ : IsCofiltered J<VAR>F : J ⥤ Profinite<VAR>C : Cone F<VAR>α : Type u_1<VAR>inst✝ : Finite α<VAR>hC : IsLimit C<VAR>f : LocallyConstant (↑C.pt.toTop) α<VAR>val✝ : Fintype α<VAR>ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1<VAR>ff : α → LocallyConstant (↑C.pt.toTop) (Fin 2) := (LocallyConstant.map ι f).flip<VAR>hff : ∀ (a : α), ∃ j g, ff a = LocallyConstant.comap (C.π.app j) g<GOAL>∃ j g, LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (C.π.app j) g
<VAR>J : Type v<VAR>inst✝² : SmallCategory J<VAR>inst✝¹ : IsCofiltered J<VAR>F : J ⥤ Profinite<VAR>C : Cone F<VAR>α : Type u_1<VAR>inst✝ : Finite α<VAR>hC : IsLimit C<VAR>f : LocallyConstant (↑C.pt.toTop) α<VAR>val✝ : Fintype α<VAR>ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1<VAR>ff : α → LocallyConstant (↑C.pt.toTop) (Fin 2) := (LocallyConstant.map ι f).flip<VAR>j : α → J<VAR>g : (a : α) → LocallyConstant (↑(F.obj (j a)).toTop) (Fin 2)<VAR>h : ∀ (a : α), ff a = LocallyConstant.comap (C.π.app (j a)) (g a)<VAR>G : Finset J := Finset.image j Finset.univ<GOAL>∃ j g, LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (C.π.app j) g
<VAR>J : Type v<VAR>inst✝² : SmallCategory J<VAR>inst✝¹ : IsCofiltered J<VAR>F : J ⥤ Profinite<VAR>C : Cone F<VAR>α : Type u_1<VAR>inst✝ : Finite α<VAR>hC : IsLimit C<VAR>f : LocallyConstant (↑C.pt.toTop) α<VAR>val✝ : Fintype α<VAR>ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1<VAR>ff : α → LocallyConstant (↑C.pt.toTop) (Fin 2) := (LocallyConstant.map ι f).flip<VAR>j : α → J<VAR>g : (a : α) → LocallyConstant (↑(F.obj (j a)).toTop) (Fin 2)<VAR>h : ∀ (a : α), ff a = LocallyConstant.comap (C.π.app (j a)) (g a)<VAR>G : Finset J := Finset.image j Finset.univ<VAR>j0 : J<VAR>hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)<GOAL>∃ j g, LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (C.π.app j) g
<VAR>J : Type v<VAR>inst✝² : SmallCategory J<VAR>inst✝¹ : IsCofiltered J<VAR>F : J ⥤ Profinite<VAR>C : Cone F<VAR>α : Type u_1<VAR>inst✝ : Finite α<VAR>hC : IsLimit C<VAR>f : LocallyConstant (↑C.pt.toTop) α<VAR>val✝ : Fintype α<VAR>ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1<VAR>ff : α → LocallyConstant (↑C.pt.toTop) (Fin 2) := (LocallyConstant.map ι f).flip<VAR>j : α → J<VAR>g : (a : α) → LocallyConstant (↑(F.obj (j a)).toTop) (Fin 2)<VAR>h : ∀ (a : α), ff a = LocallyConstant.comap (C.π.app (j a)) (g a)<VAR>G : Finset J := Finset.image j Finset.univ<VAR>j0 : J<VAR>hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)<VAR>hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ<GOAL>∃ j g, LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (C.π.app j) g
<VAR>J : Type v<VAR>inst✝² : SmallCategory J<VAR>inst✝¹ : IsCofiltered J<VAR>F : J ⥤ Profinite<VAR>C : Cone F<VAR>α : Type u_1<VAR>inst✝ : Finite α<VAR>hC : IsLimit C<VAR>f : LocallyConstant (↑C.pt.toTop) α<VAR>val✝ : Fintype α<VAR>ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1<VAR>ff : α → LocallyConstant (↑C.pt.toTop) (Fin 2) := (LocallyConstant.map ι f).flip<VAR>j : α → J<VAR>g : (a : α) → LocallyConstant (↑(F.obj (j a)).toTop) (Fin 2)<VAR>h : ∀ (a : α), ff a = LocallyConstant.comap (C.π.app (j a)) (g a)<VAR>G : Finset J := Finset.image j Finset.univ<VAR>j0 : J<VAR>hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)<VAR>hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ<VAR>fs : (a : α) → j0 ⟶ j a := fun a => ⋯.some<VAR>gg : α → LocallyConstant (↑(F.obj j0).toTop) (Fin 2) := fun a => LocallyConstant.comap (F.map (fs a)) (g a)<VAR>ggg : LocallyConstant (↑(F.obj j0).toTop) (α → Fin 2) := LocallyConstant.unflip gg<VAR>a : α<VAR>x : ↑C.pt.toTop<GOAL>(LocallyConstant.comap (C.π.app (j a)) (g a)) x = (g a) ((C.π.app j0 ≫ F.map (fs a)) x)
<VAR>J : Type v<VAR>inst✝² : SmallCategory J<VAR>inst✝¹ : IsCofiltered J<VAR>F : J ⥤ Profinite<VAR>C : Cone F<VAR>α : Type u_1<VAR>inst✝ : Finite α<VAR>hC : IsLimit C<VAR>f : LocallyConstant (↑C.pt.toTop) α<VAR>val✝ : Fintype α<VAR>ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1<VAR>ff : α → LocallyConstant (↑C.pt.toTop) (Fin 2) := (LocallyConstant.map ι f).flip<VAR>j : α → J<VAR>g : (a : α) → LocallyConstant (↑(F.obj (j a)).toTop) (Fin 2)<VAR>h : ∀ (a : α), ff a = LocallyConstant.comap (C.π.app (j a)) (g a)<VAR>G : Finset J := Finset.image j Finset.univ<VAR>j0 : J<VAR>hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)<VAR>hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ<VAR>fs : (a : α) → j0 ⟶ j a := fun a => ⋯.some<VAR>gg : α → LocallyConstant (↑(F.obj j0).toTop) (Fin 2) := fun a => LocallyConstant.comap (F.map (fs a)) (g a)<VAR>ggg : LocallyConstant (↑(F.obj j0).toTop) (α → Fin 2) := LocallyConstant.unflip gg<VAR>a : α<VAR>x : ↑C.pt.toTop<GOAL>(LocallyConstant.comap (C.π.app (j a)) (g a)) x = (g a) ((C.π.app (j a)) x)
<VAR>X Y B : CompHaus<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<VAR>Z : CompHaus<VAR>a b : Z ⟶ pullback f g<VAR>z : (forget CompHaus).obj Z<VAR>hfst : (a ≫ fst f g) z = (b ≫ fst f g) z<VAR>hsnd : (a ≫ snd f g) z = (b ≫ snd f g) z<GOAL>a z = b z
<VAR>X Y B : CompHaus<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<VAR>Z : CompHaus<VAR>a b : Z ⟶ pullback f g<VAR>z : (forget CompHaus).obj Z<VAR>hfst : (a ≫ fst f g) z = (b ≫ fst f g) z<VAR>hsnd : (a ≫ snd f g) z = (b ≫ snd f g) z<GOAL>↑(a z) = ↑(b z)
<VAR>X Y B : CompHaus<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<VAR>Z : CompHaus<VAR>a b : Z ⟶ pullback f g<VAR>z : (forget CompHaus).obj Z<VAR>hfst : (a ≫ fst f g) z = (b ≫ fst f g) z<VAR>hsnd : (a ≫ snd f g) z = (b ≫ snd f g) z<GOAL>(↑(a z)).1 = (↑(b z)).1
<VAR>X Y B : CompHaus<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<VAR>Z : CompHaus<VAR>a b : Z ⟶ pullback f g<VAR>z : (forget CompHaus).obj Z<VAR>hfst : (a ≫ fst f g) z = (b ≫ fst f g) z<VAR>hsnd : (a ≫ snd f g) z = (b ≫ snd f g) z<GOAL>(↑(a z)).2 = (↑(b z)).2
<VAR>α : Type u<VAR>a : α<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : IsSimpleGroup α<VAR>inst✝ : Fintype α<GOAL>Nat.Prime (Fintype.card α)
<VAR>α : Type u<VAR>a : α<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : IsSimpleGroup α<VAR>inst✝ : Fintype α<VAR>h0 : 0 < Fintype.card α<GOAL>Nat.Prime (Fintype.card α)
<VAR>α : Type u<VAR>a : α<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : IsSimpleGroup α<VAR>inst✝ : Fintype α<VAR>h0 : 0 < Fintype.card α<VAR>g : α<VAR>hg : ∀ (x : α), x ∈ Subgroup.zpowers g<GOAL>Nat.Prime (Fintype.card α)
<VAR>α : Type u<VAR>a : α<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : IsSimpleGroup α<VAR>inst✝ : Fintype α<VAR>h0 : 0 < Fintype.card α<VAR>g : α<VAR>hg : ∀ (x : α), x ∈ Subgroup.zpowers g<GOAL>2 ≤ Fintype.card α ∧ ∀ (m : ℕ), m ∣ Fintype.card α → m = 1 ∨ m = Fintype.card α
<VAR>α : Type u<VAR>a : α<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : IsSimpleGroup α<VAR>inst✝ : Fintype α<VAR>h0 : 0 < Fintype.card α<VAR>g : α<VAR>hg : ∀ (x : α), x ∈ Subgroup.zpowers g<VAR>n : ℕ<VAR>hn : n ∣ Fintype.card α<GOAL>n = 1 ∨ n = Fintype.card α
<VAR>α : Type u<VAR>a : α<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : IsSimpleGroup α<VAR>inst✝ : Fintype α<VAR>h0 : 0 < Fintype.card α<VAR>g : α<VAR>hg : ∀ (x : α), x ∈ Subgroup.zpowers g<VAR>n : ℕ<VAR>hn : n ∣ Fintype.card α<GOAL>Subgroup.zpowers (g ^ n) = ⊤ → n = 1
<VAR>α : Type u<VAR>a : α<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : IsSimpleGroup α<VAR>inst✝ : Fintype α<VAR>h0 : 0 < Fintype.card α<VAR>g : α<VAR>hg : ∀ (x : α), x ∈ Subgroup.zpowers g<VAR>n : ℕ<VAR>hn : n ∣ Fintype.card α<GOAL>Subgroup.zpowers (g ^ n) = ⊥ → n = Fintype.card α
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝² : Category.{uD', uD} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>f : J → C<VAR>inst✝ : HasBiproduct f<VAR>b : Bicone f<VAR>hb : b.IsBilimit<GOAL>(hb.isLimit.conePointUniqueUpToIso (isLimit f)).inv = desc b.ι
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝² : Category.{uD', uD} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>f : J → C<VAR>inst✝ : HasBiproduct f<VAR>b : Bicone f<VAR>hb : b.IsBilimit<VAR>j : J<VAR>j' : Discrete J<GOAL>(ι f j ≫ (hb.isLimit.conePointUniqueUpToIso (isLimit f)).inv) ≫ b.toCone.π.app j' = (ι f j ≫ desc b.ι) ≫ b.toCone.π.app j'
<VAR>a b : Cardinal.{u_1}<VAR>h' : a ≠ 0<VAR>h : ℵ₀ ≤ b<GOAL>a * b = max a b
<VAR>a b : Cardinal.{u_1}<VAR>h' : a ≠ 0<VAR>h : ℵ₀ ≤ b<GOAL>b * a = max b a
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ s : Set E<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>t u : Set E<VAR>h'u : μ u ≠ 0<VAR>t_bound : t ⊆ closedBall 0 1<GOAL>Tendsto (fun r => μ (s ∩ ({x} + r • t)) / μ ({x} + r • u)) (𝓝[>] 0) (𝓝 0)
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ s : Set E<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>t u : Set E<VAR>h'u : μ u ≠ 0<VAR>t_bound : t ⊆ closedBall 0 1<VAR>A : Tendsto (fun r => μ (s ∩ ({x} + r • t)) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<GOAL>Tendsto (fun r => μ (s ∩ ({x} + r • t)) / μ ({x} + r • u)) (𝓝[>] 0) (𝓝 0)
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ s : Set E<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>t u : Set E<VAR>h'u : μ u ≠ 0<VAR>t_bound : t ⊆ closedBall 0 1<VAR>A : Tendsto (fun r => μ (s ∩ ({x} + r • t)) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>B : Tendsto (fun r => μ (closedBall x r) / μ ({x} + r • u)) (𝓝[>] 0) (𝓝 (μ (closedBall x 1) / μ ({x} + u)))<GOAL>Tendsto (fun r => μ (s ∩ ({x} + r • t)) / μ ({x} + r • u)) (𝓝[>] 0) (𝓝 0)