ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α β : TypeVec.{u_1} n<VAR>F' : TypeVec.{u_1} n → Type u<VAR>inst✝¹ : MvFunctor F'<VAR>inst✝ : LawfulMvFunctor F'<VAR>R : β ⊗ β ⟹ repeat n Prop<VAR>x : F' α<VAR>f g : α ⟹ β<VAR>h : α ⟹ Subtype_ R<VAR>hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag<GOAL>(f ⊚ TypeVec.id) <$$> x = f <$$> x ∧ (prod.snd ⊚ subtypeVal R) <$$> h <$$> x = g <$$> x
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α β : TypeVec.{u_1} n<VAR>F' : TypeVec.{u_1} n → Type u<VAR>inst✝¹ : MvFunctor F'<VAR>inst✝ : LawfulMvFunctor F'<VAR>R : β ⊗ β ⟹ repeat n Prop<VAR>x : F' α<VAR>f g : α ⟹ β<VAR>h : α ⟹ Subtype_ R<VAR>hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag<GOAL>(f ⊚ TypeVec.id) <$$> x = f <$$> x ∧ (g ⊚ TypeVec.id) <$$> x = g <$$> x
<VAR>x : ℝ<VAR>hx : 0 ≤ x<GOAL>(↑(Real.log x)).re = (log ↑x).re
<VAR>x : ℝ<VAR>hx : 0 ≤ x<GOAL>(↑(Real.log x)).im = (log ↑x).im
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α →. σ<VAR>h : Nat.Partrec fun n => (↑(decode₂ α n)).bind fun a => Part.map encode (f a)<GOAL>Partrec fun a => Part.map encode (f a)
<VAR>X : Type u_1<VAR>inst✝ : EMetricSpace X<VAR>s✝ t✝ : Set X<VAR>x y : X<VAR>ι : Type u_2<VAR>I : Set ι<VAR>hI : I.Finite<VAR>s : ι → Set X<VAR>t : Set X<GOAL>IsMetricSeparated (⋃ i ∈ I, s i) t ↔ ∀ i ∈ I, IsMetricSeparated (s i) t
<VAR>X : Type u_1<VAR>inst✝ : EMetricSpace X<VAR>s✝ t✝ : Set X<VAR>x y : X<VAR>ι : Type u_2<VAR>I✝ : Set ι<VAR>hI✝ : I✝.Finite<VAR>s : ι → Set X<VAR>t : Set X<VAR>i : ι<VAR>I : Set ι<VAR>x✝¹ : i ∉ I<VAR>x✝ : I.Finite<VAR>hI : IsMetricSeparated (⋃ i ∈ I, s i) t ↔ ∀ i ∈ I, IsMetricSeparated (s i) t<GOAL>IsMetricSeparated (⋃ i_1 ∈ insert i I, s i_1) t ↔ ∀ i_1 ∈ insert i I, IsMetricSeparated (s i_1) t
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIcoMod hp a b ≤ toIocMod hp a b
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIocDiv hp a b • p ≤ toIcoDiv hp a b • p
<VAR>ι : Sort u_1<VAR>f : ι → ℕ<VAR>s : Set ℕ<GOAL>(⨅ i, ↑(f i)).toNat = ⨅ i, f i
<VAR>ι : Sort u_1<VAR>f : ι → ℕ<VAR>s : Set ℕ<VAR>h✝ : IsEmpty ι<GOAL>(⨅ i, ↑(f i)).toNat = ⨅ i, f i
<VAR>ι : Sort u_1<VAR>f : ι → ℕ<VAR>s : Set ℕ<VAR>h✝ : Nonempty ι<GOAL>(⨅ i, ↑(f i)).toNat = ⨅ i, f i
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_4, u_1} C<VAR>inst✝⁴ : Category.{u_3, u_2} D<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : S.RightHomologyData<VAR>F : C ⥤ D<VAR>inst✝¹ : F.PreservesZeroMorphisms<VAR>inst✝ : h.IsPreservedBy F<GOAL>(h.map F).g' = F.map h.g'
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝³ : Monoid N<VAR>hnontriv : Nontrivial ι<VAR>G : Type u_4<VAR>inst✝² : Group G<VAR>H : ι → Type u_5<VAR>inst✝¹ : (i : ι) → Group (H i)<VAR>f : (i : ι) → H i →* G<VAR>hcard : 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)<VAR>α : Type u_6<VAR>inst✝ : MulAction G α<VAR>X : ι → Set α<VAR>hXnonempty : ∀ (i : ι), (X i).Nonempty<VAR>hXdisj : Pairwise fun i j => Disjoint (X i) (X j)<VAR>hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i<GOAL>Function.Injective ⇑(lift f)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<GOAL>TendstoUniformly F f p ↔ TendstoUniformlyOnFilter F f p ⊤
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ γ₁ γ₂ : Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n + a = n'<VAR>p q : ℤ<VAR>hpq : p + n = q<GOAL>((γ.leftShift a n' hn').rightShift a n hn').v p q hpq = ((a * n' + a * (a - 1) / 2).negOnePow • γ.shift a).v p q hpq
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ γ₁ γ₂ : Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n + a = n'<VAR>p q : ℤ<VAR>hpq : p + n = q<GOAL>((a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫ γ.v (p + a) (q + a) ⋯) ≫ (L.shiftFunctorObjXIso a q (q + a) ⋯).inv = (a * n' + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) ⋯
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ γ₁ γ₂ : Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n + a = n'<VAR>p q : ℤ<VAR>hpq : p + n = q<GOAL>((a * n' + a * (a - 1) / 2).negOnePow • 𝟙 (K.X (p + a)) ≫ γ.v (p + a) (q + a) ⋯) ≫ 𝟙 (L.X (q + a)) = (a * n' + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) ⋯
<VAR>α : Type u_1<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : MonoidWithZero α<VAR>inst✝¹ : NoZeroDivisors α<VAR>inst✝ : Nontrivial α<VAR>n : ℕ<VAR>n_pos : 0 < n<VAR>m : ℕ<VAR>x✝ : Nat.succ 0 ≤ m<VAR>hm : ⊤ ^ m = ⊤<GOAL>⊤ ^ (m + 1) = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : Monoid M<VAR>G : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Nontrivial R<GOAL>FiniteType R (MonoidAlgebra R G) ↔ Group.FG G
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>H₁ : S₁.HomologyData<VAR>H₂ : S₂.HomologyData<VAR>h₀ : S₁.X₁ ⟶ S₂.X₁<VAR>h₀_f : h₀ ≫ S₂.f = 0<VAR>h₁ : S₁.X₂ ⟶ S₂.X₁<VAR>h₂ : S₁.X₃ ⟶ S₂.X₂<VAR>h₃ : S₁.X₃ ⟶ S₂.X₃<VAR>g_h₃ : S₁.g ≫ h₃ = 0<GOAL>homologyMap' (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) H₁ H₂ = 0
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>x ⊓ y ⊓ z ⊔ 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 \ z) ⊓ y
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>(x ⊔ y \ z) ⊓ y = x ⊓ y ⊔ y \ z
<VAR>α : Type u_1<VAR>a b : ℂ<VAR>ha : a ≠ 0<GOAL>(fun x => x ^ b) =ᶠ[𝓝 a] fun x => cexp (Complex.log x * b)
<VAR>α : Type u_1<VAR>a b : ℂ<VAR>ha : a ≠ 0<GOAL>∀ᶠ (x : ℂ) in 𝓝 a, x ≠ 0
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁶ : CommSemiring K<VAR>inst✝⁵ : CommSemiring L<VAR>inst✝⁴ : CommSemiring M<VAR>i : K →+* L<VAR>j : K →+* M<VAR>f : L →+* M<VAR>p : ℕ<VAR>inst✝³ : ExpChar K p<VAR>inst✝² : ExpChar L p<VAR>inst✝¹ : ExpChar M p<VAR>inst✝ : PerfectRing L p<VAR>x : K<VAR>h : x ∈ pNilradical K p<GOAL>x ∈ ker i
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁶ : CommSemiring K<VAR>inst✝⁵ : CommSemiring L<VAR>inst✝⁴ : CommSemiring M<VAR>i : K →+* L<VAR>j : K →+* M<VAR>f : L →+* M<VAR>p : ℕ<VAR>inst✝³ : ExpChar K p<VAR>inst✝² : ExpChar L p<VAR>inst✝¹ : ExpChar M p<VAR>inst✝ : PerfectRing L p<VAR>x : K<VAR>h✝ : x ∈ pNilradical K p<VAR>n : ℕ<VAR>h : x ^ p ^ n = 0<GOAL>x ∈ ker i
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁶ : CommSemiring K<VAR>inst✝⁵ : CommSemiring L<VAR>inst✝⁴ : CommSemiring M<VAR>i : K →+* L<VAR>j : K →+* M<VAR>f : L →+* M<VAR>p : ℕ<VAR>inst✝³ : ExpChar K p<VAR>inst✝² : ExpChar L p<VAR>inst✝¹ : ExpChar M p<VAR>inst✝ : PerfectRing L p<VAR>x : K<VAR>h✝ : x ∈ pNilradical K p<VAR>n : ℕ<VAR>h : (iterateFrobeniusEquiv L p n).symm (i (x ^ p ^ n)) = (iterateFrobeniusEquiv L p n).symm (i 0)<GOAL>x ∈ ker i
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰✝ : X.OpenCover<VAR>f✝ : X ⟶ Z<VAR>g✝ : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰✝.J), HasPullback (𝒰✝.map i ≫ f✝) g✝<VAR>s : PullbackCone f✝ g✝<VAR>𝒰 : Z.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>i : (openCoverOfLeft (𝒰.pullbackCover f) f g).J<VAR>Xᵢ : Scheme := pullback f (𝒰.map i)<VAR>Yᵢ : Scheme := pullback g (𝒰.map i)<VAR>W : Scheme := pullback (pullback.snd g (𝒰.map i)) (pullback.snd f (𝒰.map i))<GOAL>((openCoverOfLeft (𝒰.pullbackCover f) f g).obj i).OpenCover
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰✝ : X.OpenCover<VAR>f✝ : X ⟶ Z<VAR>g✝ : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰✝.J), HasPullback (𝒰✝.map i ≫ f✝) g✝<VAR>s : PullbackCone f✝ g✝<VAR>𝒰 : Z.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>i : (openCoverOfLeft (𝒰.pullbackCover f) f g).J<VAR>Xᵢ : Scheme := pullback f (𝒰.map i)<VAR>Yᵢ : Scheme := pullback g (𝒰.map i)<VAR>W : Scheme := pullback (pullback.snd g (𝒰.map i)) (pullback.snd f (𝒰.map i))<VAR>this : IsLimit (PullbackCone.mk (pullback.snd (pullback.snd g (𝒰.map i)) (pullback.snd f (𝒰.map i))) (pullback.fst (pullback.snd g (𝒰.map i)) (pullback.snd f (𝒰.map i)) ≫ pullback.fst g (𝒰.map i)) ⋯)<GOAL>((openCoverOfLeft (𝒰.pullbackCover f) f g).obj i).OpenCover
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>β : Sort u_1<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F G : C ⥤ D<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>hobj : ∀ (X : C), F.obj X = G.obj X<VAR>hmap : ∀ {X Y : C} (f : X ⟶ Y), HEq (F.map f) (G.map f)<GOAL>HEq (F.map (f ≫ g)) (G.map (f ≫ g))
<VAR>l r : List Char<VAR>it : Iterator<VAR>h : ValidFor l r it<GOAL>it.hasPrev = true ↔ l ≠ []
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝ : Fintype ι<VAR>f : ι → ℝ<VAR>hf : f ∈ stdSimplex ℝ ι<GOAL>f ∈ closedBall 0 1
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝ : Fintype ι<VAR>f : ι → ℝ<VAR>hf : f ∈ stdSimplex ℝ ι<GOAL>∀ (b : ι), dist (f b) (0 b) ≤ 1
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝ : Fintype ι<VAR>f : ι → ℝ<VAR>hf : f ∈ stdSimplex ℝ ι<VAR>x : ι<GOAL>dist (f x) (0 x) ≤ 1
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝ : Fintype ι<VAR>f : ι → ℝ<VAR>hf : f ∈ stdSimplex ℝ ι<VAR>x : ι<GOAL>f x ≤ 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : OrderedSMul α β<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<GOAL>Monovary f (⇑OrderDual.toDual ∘ g) ↔ ∀ (i j : ι), (f j - f i) • (g j - g i) ≤ 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : OrderedSMul α β<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<GOAL>(∀ (i j : ι), 0 ≤ (f j - f i) • ((⇑OrderDual.toDual ∘ g) j - (⇑OrderDual.toDual ∘ g) i)) ↔ ∀ (i j : ι), (f j - f i) • (g j - g i) ≤ 0
<VAR>α✝ β✝ : Type u<VAR>inst✝ : (P : Prop) → Decidable P<VAR>α β γ : Type u<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<VAR>a✝ : γ<GOAL>a✝ ∈ image₂ f s t ↔ a✝ ∈ Seq.seq (f <$> s) fun x => t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>x y : ℝ<VAR>hy : 0 ≤ y<GOAL>‖x‖₊ * y.toNNReal = ‖x * y‖₊
<VAR>q : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>x : ℝ<GOAL>Irrational (↑n * x) ↔ n ≠ 0 ∧ Irrational x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedHeytingAlgebra α<VAR>a b c d : α<VAR>h : Codisjoint a b<GOAL>a ⇨ a ⊓ b = b
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : Group H<VAR>inst✝⁴ : MulAction G α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MulAction H β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>ν : Measure β<VAR>h : IsFundamentalDomain G s μ<VAR>f : α ≃ β<VAR>hf : QuasiMeasurePreserving (⇑f.symm) ν μ<VAR>e : H ≃ G<VAR>hef : ∀ (g : H), Semiconj (⇑f) (fun x => e g • x) fun x => g • x<GOAL>IsFundamentalDomain H (⇑f '' s) ν
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : Group H<VAR>inst✝⁴ : MulAction G α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MulAction H β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>ν : Measure β<VAR>h : IsFundamentalDomain G s μ<VAR>f : α ≃ β<VAR>hf : QuasiMeasurePreserving (⇑f.symm) ν μ<VAR>e : H ≃ G<VAR>hef : ∀ (g : H), Semiconj (⇑f) (fun x => e g • x) fun x => g • x<GOAL>IsFundamentalDomain H (⇑f.symm ⁻¹' s) ν
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : Group H<VAR>inst✝⁴ : MulAction G α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MulAction H β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>ν : Measure β<VAR>h : IsFundamentalDomain G s μ<VAR>f : α ≃ β<VAR>hf : QuasiMeasurePreserving (⇑f.symm) ν μ<VAR>e : H ≃ G<VAR>hef : ∀ (g : H), Semiconj (⇑f) (fun x => e g • x) fun x => g • x<VAR>g : G<VAR>x : β<GOAL>f.symm ((fun x => e.symm g • x) x) = (fun x => g • x) (f.symm x)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : Group H<VAR>inst✝⁴ : MulAction G α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MulAction H β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>ν : Measure β<VAR>h : IsFundamentalDomain G s μ<VAR>f : α ≃ β<VAR>hf : QuasiMeasurePreserving (⇑f.symm) ν μ<VAR>e : H ≃ G<VAR>hef : ∀ (g : H), Semiconj (⇑f) (fun x => e g • x) fun x => g • x<VAR>g : G<VAR>x : α<GOAL>f.symm ((fun x => e.symm g • x) (f x)) = (fun x => g • x) (f.symm (f x))
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : Nonempty ι<VAR>U : Set E<VAR>hU : U ∈ p.basisSets<GOAL>∃ V ∈ 𝓝 0, ∃ W ∈ AddGroupFilterBasis.toFilterBasis.sets, V • W ⊆ U
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : Nonempty ι<VAR>U : Set E<VAR>hU✝ : U ∈ p.basisSets<VAR>s : Finset ι<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hU : U = (s.sup p).ball 0 r<GOAL>∃ V ∈ 𝓝 0, ∃ W ∈ AddGroupFilterBasis.toFilterBasis.sets, V • W ⊆ U
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : Nonempty ι<VAR>U : Set E<VAR>hU✝ : U ∈ p.basisSets<VAR>s : Finset ι<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hU : U = (s.sup p).ball 0 r<GOAL>∃ W ∈ AddGroupFilterBasis.toFilterBasis.sets, Metric.ball 0 √r • W ⊆ U
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : Nonempty ι<VAR>U : Set E<VAR>hU✝ : U ∈ p.basisSets<VAR>s : Finset ι<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hU : U = (s.sup p).ball 0 r<GOAL>Metric.ball 0 √r • (s.sup p).ball 0 √r ⊆ U
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : Nonempty ι<VAR>U : Set E<VAR>hU✝ : U ∈ p.basisSets<VAR>s : Finset ι<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hU : U = (s.sup p).ball 0 r<GOAL>(s.sup p).ball 0 (√r * √r) ⊆ U
<VAR>F : Type u_1<VAR>α✝ : Type u_2<VAR>β✝ : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>inst✝ : DecidableEq β<VAR>s : Finset α<VAR>f : α → Finset β<VAR>x : β<GOAL>x ∈ s.sup f ↔ ∃ v ∈ s, x ∈ (f v).val
<VAR>F : Type u_1<VAR>α✝ : Type u_2<VAR>β✝ : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>inst✝ : DecidableEq β<VAR>s : Finset α<VAR>f : α → Finset β<VAR>x : β<GOAL>x ∈ s.sup f ↔ x ∈ s.sup fun x => (f x).val.toFinset
<VAR>α : Type u<VAR>n : ℕ<GOAL>Pairwise (fun x x_1 => x < x_1) (range n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t : Set α<GOAL>s₁ ∩ s₂ ⊆ s₂
<VAR>R : Type u_1<VAR>inst✝³ : Ring R<VAR>S : Type u_2<VAR>inst✝² : AddCommGroup S<VAR>inst✝¹ : Pow S ℕ<VAR>inst✝ : Module R S<VAR>p q : R[X]<VAR>x : S<GOAL>(-p).smeval x = -p.smeval x
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_1<VAR>p : α → Prop<VAR>α✝ : Type u_1<VAR>q : α✝ → Prop<VAR>f : α → α✝<VAR>inst✝¹ : Functor m<VAR>inst✝ : LawfulFunctor m<VAR>x : m α<VAR>hx✝ : SatisfiesM p x<VAR>hf : ∀ {a : α}, p a → q (f a)<VAR>x' : m { a // p a }<VAR>hx : Subtype.val <$> x' = x<GOAL>Subtype.val <$> (fun x => match x with | ⟨a, h⟩ => ⟨f a, ⋯⟩) <$> x' = f <$> Subtype.val <$> x'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : DivisionMonoid α<VAR>a b c d : α<VAR>h : a * b⁻¹ = 1<GOAL>a = b
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝ : Preadditive D<VAR>X : C<VAR>P Q : Cᵒᵖ ⥤ D<VAR>x✝ : (J.Cover X)ᵒᵖ<GOAL>(J.diagramNatTrans 0 X).app x✝ = NatTrans.app 0 x✝
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝ : Preadditive D<VAR>X : C<VAR>P Q : Cᵒᵖ ⥤ D<VAR>x✝ : (J.Cover X)ᵒᵖ<VAR>i : ((unop x✝).index Q).L<GOAL>(J.diagramNatTrans 0 X).app x✝ ≫ Multiequalizer.ι ((unop x✝).index Q) i = NatTrans.app 0 x✝ ≫ Multiequalizer.ι ((unop x✝).index Q) i
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝ : Preadditive D<VAR>X : C<VAR>P Q : Cᵒᵖ ⥤ D<VAR>x✝ : (J.Cover X)ᵒᵖ<VAR>i : ((unop x✝).index Q).L<GOAL>Multiequalizer.lift ((unop x✝).index Q) (multiequalizer ((unop x✝).index P)) (fun i => Multiequalizer.ι ((unop x✝).index P) i ≫ 0) ⋯ ≫ Multiequalizer.ι ((unop x✝).index Q) i = 0 ≫ Multiequalizer.ι ((unop x✝).index Q) i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Finset α<VAR>hs : s.Nonempty<VAR>a✝ a : α<VAR>ha : a ∈ s<GOAL>∀ (x : α), x ∈ (uniformOfFinset s ⋯).support ↔ x ∈ ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : TopologicalSpace α<VAR>f✝ g : β → α<VAR>a a₁ a₂ : α<VAR>b : β<VAR>f : β → α<GOAL>∏' (x : ↑{b}), f ↑x = f b
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>Z X Y P : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C<VAR>h₁₁ : X₁₁ ⟶ X₁₂<VAR>h₂₁ : X₂₁ ⟶ X₂₂<VAR>h₃₁ : X₃₁ ⟶ X₃₂<VAR>v₁₁ : X₁₁ ⟶ X₂₁<VAR>v₁₂ : X₁₂ ⟶ X₂₂<VAR>v₁₃ : X₁₂ ⟶ X₃₂<VAR>v₂₁ : X₂₁ ⟶ X₃₁<VAR>s : IsPushout h₁₁ (v₁₁ ≫ v₂₁) v₁₃ h₃₁<VAR>t : IsPushout h₁₁ v₁₁ v₁₂ h₂₁<GOAL>h₁₁ ≫ v₁₃ = v₁₁ ≫ v₂₁ ≫ h₃₁
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K : Set (E →L[𝕜] F)<VAR>inst✝ : CompleteSpace F<VAR>hf : Continuous (Function.uncurry f)<GOAL>MeasurableSet {p | DifferentiableAt 𝕜 (f p.1) p.2}
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K : Set (E →L[𝕜] F)<VAR>inst✝ : CompleteSpace F<VAR>hf : Continuous (Function.uncurry f)<VAR>this : IsComplete univ<GOAL>MeasurableSet {p | DifferentiableAt 𝕜 (f p.1) p.2}
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K : Set (E →L[𝕜] F)<VAR>inst✝ : CompleteSpace F<VAR>hf : Continuous (Function.uncurry f)<VAR>this : IsComplete univ<VAR>x✝ : α × E<GOAL>DifferentiableAt 𝕜 (f x✝.1) x✝.2 ↔ DifferentiableAt 𝕜 (f x✝.1) x✝.2 ∧ fderiv 𝕜 (f x✝.1) x✝.2 ∈ univ
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<GOAL>edgeDensity r s t + edgeDensity (fun x y => ¬r x y) s t = 1
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<GOAL>↑(interedges r s t).card + ↑(interedges (fun x y => ¬r x y) s t).card = ↑s.card * ↑t.card
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<GOAL>↑s.card * ↑t.card ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>f g : α → β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>s t : Set α<GOAL>AEStronglyMeasurable f (μ.restrict (s ∪ t)) ↔ AEStronglyMeasurable f (μ.restrict s) ∧ AEStronglyMeasurable f (μ.restrict t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>X✝ Y✝ Z✝ : Pointed<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<GOAL>{ obj := fun X => { x // x ≠ X.point }, map := fun {X Y} f => PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val }.map (f ≫ g) = { obj := fun X => { x // x ≠ X.point }, map := fun {X Y} f => PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val }.map f ≫ { obj := fun X => { x // x ≠ X.point }, map := fun {X Y} f => PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val }.map g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>X✝ Y✝ Z✝ : Pointed<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<GOAL>∀ (a : { obj := fun X => { x // x ≠ X.point }, map := fun {X Y} f => PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val }.obj X✝) (b : { obj := fun X => { x // x ≠ X.point }, map := fun {X Y} f => PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val }.obj Z✝), b ∈ { obj := fun X => { x // x ≠ X.point }, map := fun {X Y} f => PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val }.map (f ≫ g) a ↔ b ∈ ({ obj := fun X => { x // x ≠ X.point }, map := fun {X Y} f => PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val }.map f ≫ { obj := fun X => { x // x ≠ X.point }, map := fun {X Y} f => PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val }.map g) a