ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : TopCat<VAR>H₁ : X ≅ Y<VAR>ℱ : Presheaf C X<VAR>𝒢 : Presheaf C Y<VAR>H₂ : (pushforward C H₁.hom).obj ℱ ⟶ 𝒢<VAR>U : (Opens ↑X)ᵒᵖ<GOAL>U = (Opens.map H₁.hom).op.obj (op ((Opens.map H₁.inv).obj (unop U)))
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : TopCat<VAR>H₁ : X ≅ Y<VAR>ℱ : Presheaf C X<VAR>𝒢 : Presheaf C Y<VAR>H₂ : (pushforward C H₁.hom).obj ℱ ⟶ 𝒢<VAR>U : (Opens ↑X)ᵒᵖ<GOAL>(((presheafEquivOfIso C H₁).toAdjunction.homEquiv ℱ 𝒢) H₂).app U = ℱ.map (eqToHom ⋯) ≫ H₂.app (op ((Opens.map H₁.inv).obj (unop U)))
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : TopCat<VAR>H₁ : X ≅ Y<VAR>ℱ : Presheaf C X<VAR>𝒢 : Presheaf C Y<VAR>H₂ : (pushforward C H₁.hom).obj ℱ ⟶ 𝒢<VAR>U : (Opens ↑X)ᵒᵖ<GOAL>ℱ.map ((Opens.mapMapIso H₁).symm.op.unit.app U ≫ ((Opens.map H₁.hom).map ((Opens.mapMapIso H₁).symm.op.counitInv.app (op ((Opens.map H₁.inv).obj (unop U)))).unop).op ≫ (Opens.mapMapIso H₁).symm.op.unitInv.app (op ((Opens.map H₁.hom).obj ((Opens.map H₁.inv).obj (unop U))))) ≫ H₂.app (op ((Opens.map H₁.inv).obj (unop U))) = ℱ.map (eqToHom ⋯) ≫ H₂.app (op ((Opens.map H₁.inv).obj (unop U)))
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>a b c : α<GOAL>Associated (gcd (b * a) (c * a)) (gcd b c * a)
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a✝ a₁ a₂ b✝ b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>a b : E<GOAL>‖a / b‖ = ‖b / a‖
<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>K : Type u_9<VAR>V : Type u_10<VAR>V₂ : Type u_11<VAR>inst✝⁴ : Semifield K<VAR>inst✝³ : AddCommMonoid V<VAR>inst✝² : Module K V<VAR>inst✝¹ : AddCommMonoid V₂<VAR>inst✝ : Module K V₂<VAR>f : V →ₗ[K] V₂<VAR>p : Submodule K V₂<VAR>a : K<GOAL>comap (a • f) p = ⨅ (_ : a ≠ 0), comap f p
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L : Filter 𝕜<VAR>h : HasDerivAtFilter f f' x L<GOAL>HasDerivAtFilter (fun x => -f x) (-f') x L
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : PredOrder α<VAR>a b : α<VAR>ha : ¬IsMin a<GOAL>Ioc (pred a) b = Icc a 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>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : MeasurableSMul G α<VAR>inst✝³ : SMulInvariantMeasure G α μ<VAR>inst✝² : Countable G<VAR>ν : Measure α<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>h : IsFundamentalDomain G s μ<VAR>f : α → E<VAR>t : Set α<VAR>hf : IntegrableOn f t μ<GOAL>∑' (g : G), ∫ (x : α) in t ∩ g⁻¹ • s, f x ∂μ = ∑' (g : G), ∫ (x : α) in g⁻¹ • (g • t ∩ s), f x ∂μ
<VAR>G : Type u<VAR>inst✝² : Group G<VAR>inst✝¹ : Finite G<VAR>h2 : ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'], Nat.card G' < Nat.card G → ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'<VAR>inst✝ : ⊥.Normal<VAR>h1 : (Nat.card ↥⊥).Coprime ⊥.index<VAR>h3 : ∀ (H : Subgroup G), ¬⊥.IsComplement' H<GOAL>False
<VAR>α : Sort u<VAR>β✝ : Sort v<VAR>γ : Sort w<VAR>inst✝ : Unique α<VAR>β : α → Sort u_1<VAR>f : (i : α) → β i<VAR>i : α<GOAL>uniqueElim ((fun f => f default) f) i = f i
<VAR>α : Sort u<VAR>β✝ : Sort v<VAR>γ : Sort w<VAR>inst✝ : Unique α<VAR>β : α → Sort u_1<VAR>f : (i : α) → β i<GOAL>uniqueElim ((fun f => f default) f) default = f default
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : StrongRankCondition R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module.Free R M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module.Free R M'<VAR>inst✝² : AddCommGroup M₁<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Module.Free R M₁<VAR>h : ¬Module.Finite R M<GOAL>finrank R M = 0
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : StrongRankCondition R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module.Free R M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module.Free R M'<VAR>inst✝² : AddCommGroup M₁<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Module.Free R M₁<VAR>h : ¬Module.Finite R M<GOAL>Module.rank R M = 0 ∨ ¬Module.Finite R M
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>a b : α<VAR>m : Sym2 α<GOAL>image Sym2.mk s.diag ∪ image Sym2.mk s.offDiag = s.sym2
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Nontrivial R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module.Finite R M<VAR>f : M →ₗ[R] M<VAR>inst✝ : StrongRankCondition R<GOAL>f.charpoly.natDegree = finrank R M
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : Mul M<VAR>s✝ : Set M<VAR>inst✝ : Add A<VAR>t : Set A<VAR>S : Subsemigroup M<VAR>s : Set M<VAR>p : (x : M) → x ∈ closure s → Prop<VAR>mem : ∀ (x : M) (h : x ∈ s), p x ⋯<VAR>mul : ∀ (x : M) (hx : x ∈ closure s) (y : M) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) ⋯<VAR>x : M<VAR>hx : x ∈ closure s<GOAL>p x hx
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : Mul M<VAR>s✝ : Set M<VAR>inst✝ : Add A<VAR>t : Set A<VAR>S : Subsemigroup M<VAR>s : Set M<VAR>p : (x : M) → x ∈ closure s → Prop<VAR>mem : ∀ (x : M) (h : x ∈ s), p x ⋯<VAR>mul : ∀ (x : M) (hx : x ∈ closure s) (y : M) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) ⋯<VAR>x : M<VAR>hx : x ∈ closure s<GOAL>∃ (x_1 : x ∈ closure s), p x x_1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : Zero α<VAR>inst✝¹ : Zero β<VAR>inst✝ : SMulWithZero α β<VAR>s : Set α<VAR>t✝ t : Set β<GOAL>0 • t ⊆ 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>r : R<VAR>N : ℕ<GOAL>reflect N (C r) = C r * X ^ N
<VAR>M : Type u_1<VAR>inst✝⁵ : CommMonoid M<VAR>inst✝⁴ : TopologicalSpace M<VAR>m m' : M<VAR>G : Type u_2<VAR>inst✝³ : CommGroup G<VAR>g g' : G<VAR>inst✝² : UniformSpace G<VAR>inst✝¹ : UniformGroup G<VAR>inst✝ : CompleteSpace G<VAR>f : ℕ → G<GOAL>Multipliable f ↔ ∀ e ∈ 𝓝 1, ∃ N, ∀ t ⊆ {n | N ≤ n}, ∏' (n : ↑t), f ↑n ∈ e
<VAR>a b c d m n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>n : ℕ<VAR>h : a ≤ n + n<GOAL>(n ^ 2 + a).sqrt = n
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s✝ s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>s : Set (Set X)<GOAL>(∀ t ∈ s, IsClosed t) → IsClosed (⋂₀ s)
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>ac : a < c<VAR>bd : b < d<GOAL>a * b < c * d
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>ac : a < c<VAR>bd : b < d<VAR>a' : ℝ≥0<VAR>aa' : a < ↑a'<VAR>a'c : ↑a' < c<GOAL>a * b < c * d
<VAR>b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>bd : b < d<VAR>a' : ℝ≥0<VAR>a'c : ↑a' < c<VAR>a : ℝ≥0<VAR>ac : ↑a < c<VAR>aa' : ↑a < ↑a'<GOAL>↑a * b < c * d
<VAR>b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>bd : b < d<VAR>a' : ℝ≥0<VAR>a'c : ↑a' < c<VAR>a : ℝ≥0<VAR>ac : ↑a < c<VAR>aa' : ↑a < ↑a'<VAR>b' : ℝ≥0<VAR>bb' : b < ↑b'<VAR>b'd : ↑b' < d<GOAL>↑a * b < c * d
<VAR>c d : ℝ≥0∞<VAR>r p q a' : ℝ≥0<VAR>a'c : ↑a' < c<VAR>a : ℝ≥0<VAR>ac : ↑a < c<VAR>aa' : ↑a < ↑a'<VAR>b' : ℝ≥0<VAR>b'd : ↑b' < d<VAR>b : ℝ≥0<VAR>bd : ↑b < d<VAR>bb' : ↑b < ↑b'<GOAL>↑a * ↑b < c * d
<VAR>c d : ℝ≥0∞<VAR>r p q a' : ℝ≥0<VAR>a'c : ↑a' < c<VAR>a : ℝ≥0<VAR>ac : ↑a < c<VAR>b' : ℝ≥0<VAR>b'd : ↑b' < d<VAR>b : ℝ≥0<VAR>bd : ↑b < d<VAR>aa' : a < a'<VAR>bb' : b < b'<GOAL>↑(a * b) < c * d
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a✝ : α<VAR>n : ℕ<VAR>a b : α<VAR>h : a < b<VAR>h' : 0 < b<GOAL>⌊a⌋₊ < ⌈b⌉₊
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a✝ : α<VAR>n : ℕ<VAR>a b : α<VAR>h : a < b<VAR>h' : 0 < b<VAR>ha : 0 ≤ a<GOAL>⌊a⌋₊ < ⌈b⌉₊
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a✝ : α<VAR>n : ℕ<VAR>a b : α<VAR>h : a < b<VAR>h' : 0 < b<VAR>ha : a < 0<GOAL>⌊a⌋₊ < ⌈b⌉₊
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x y : α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>hf : f.IsCycle<GOAL>orderOf f = f.support.card
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x y : α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>hf : f.IsCycle<GOAL>Fintype.card ↥(Subgroup.zpowers f) = Fintype.card { x // x ∈ f.support }
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℝ<VAR>c_one : 1 < c<GOAL>∀ᵐ (ω : Ω), (fun n => ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n => ↑⌊c ^ n⌋₊
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℝ<VAR>c_one : 1 < c<VAR>ω : Ω<VAR>hω : (fun n => ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a) =o[atTop] fun n => ↑⌊c ^ n⌋₊<GOAL>(fun n => ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n => ↑⌊c ^ n⌋₊
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℝ<VAR>c_one : 1 < c<VAR>ω : Ω<VAR>hω : (fun n => ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a) =o[atTop] fun n => ↑⌊c ^ n⌋₊<VAR>A : Tendsto (fun n => ⌊c ^ n⌋₊) atTop atTop<GOAL>(fun n => ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n => ↑⌊c ^ n⌋₊
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℝ<VAR>c_one : 1 < c<VAR>ω : Ω<VAR>hω : (fun n => ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a) =o[atTop] fun n => ↑⌊c ^ n⌋₊<VAR>A : Tendsto (fun n => ⌊c ^ n⌋₊) atTop atTop<GOAL>(fun n => ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) = fun x => (∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) ↑i) a) + ((fun n => (∫ (a : Ω), (∑ i ∈ range n, truncation (X i) ↑i) a) - ↑n * ∫ (a : Ω), X 0 a) ∘ fun n => ⌊c ^ n⌋₊) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<GOAL>∅.encard = 0
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : Y ⟶ (coextendScalars f).obj X<VAR>x y : ↑((restrictScalars f).obj Y)<GOAL>(g (x + y)) 1 = (g x) 1 + (g y) 1
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : Y ⟶ (coextendScalars f).obj X<VAR>r : R<VAR>y : ↑Y<GOAL>(g (f r • y)) 1 = r • (g y) 1
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : Y ⟶ (coextendScalars f).obj X<VAR>r : R<VAR>y : ↑Y<GOAL>(g (f r • y)) 1 = (g y) (r • 1)
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : Y ⟶ (coextendScalars f).obj X<VAR>r : R<VAR>y : ↑Y<GOAL>(f r • g y) 1 = (g y) (↑f.toMonoidWithZeroHom r)
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : Y ⟶ (coextendScalars f).obj X<VAR>r : R<VAR>y : ↑Y<GOAL>(f r • g y).toFun 1 = (g y) (↑f.toMonoidWithZeroHom r)
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : Y ⟶ (coextendScalars f).obj X<VAR>r : R<VAR>y : ↑Y<GOAL>(g y).toFun (f r) = (g y) (↑f.toMonoidWithZeroHom r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : CommGroup α<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformGroup α<VAR>f g : β → α<VAR>a a₁ a₂ : α<VAR>inst✝ : CompleteSpace α<GOAL>Multipliable f ↔ ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : (i : ι) → DecidableEq (β i)<VAR>γ : ι → Type u_4<VAR>inst✝⁴ : (i : ι) → DecidableEq (γ i)<VAR>inst✝³ : (i : ι) → Zero (β i)<VAR>inst✝² : (i : ι) → Zero (γ i)<VAR>inst✝¹ : Zero α<VAR>inst✝ : (i : ι) → SMulWithZero α (β i)<VAR>k : α<VAR>x : (i : ι) → β i<VAR>i : ι<GOAL>(fun i c => k • c) i 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : CommMonoid M<VAR>x y z a b : M<GOAL>(a * b) ^ 0 = a ^ 0 * b ^ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : CommMonoid M<VAR>x y z a b : M<VAR>n : ℕ<GOAL>(a * b) ^ (n + 1) = a ^ (n + 1) * b ^ (n + 1)
<VAR>α : Type u_1<VAR>inst✝¹ : OrderedSemiring α<VAR>inst✝ : Nontrivial α<VAR>x : ↑(Ico 0 1)<GOAL>x = 0 ↔ ↑x = 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : InvolutiveInv α<VAR>s✝ t s : Set α<GOAL>Nat.card ↑s⁻¹ = Nat.card ↑s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : NoMaxOrder α<VAR>a : α<GOAL>Bounded (fun x x_1 => x < x_1) (s ∩ {b | a < b}) ↔ Bounded (fun x x_1 => x < x_1) s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : NoMaxOrder α<VAR>a : α<GOAL>Bounded (fun x x_1 => x ≤ x_1) (s ∩ {b | a < b}) ↔ Bounded (fun x x_1 => x ≤ x_1) s
<VAR>G : Type u<VAR>M : Type v<VAR>α : Type w<VAR>s✝ : Set α<VAR>m : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace G<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>μ : Measure α<VAR>inst✝ : SMulInvariantMeasure G α μ<VAR>c : G<VAR>s t : Set α<GOAL>c • s =ᶠ[ae μ] c • t ↔ s =ᶠ[ae μ] t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : Fintype α<VAR>s : Set α<VAR>inst✝¹ : Fintype ↑s<VAR>inst✝ : Fintype ↑sᶜ<GOAL>card ↑sᶜ = card α - card ↑s
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ : ℝ<VAR>s : Set α<VAR>x : α<VAR>δ : ℝ<GOAL>thickening δ ∅ = ∅
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝⁴ : LinearOrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : DenselyOrdered 𝕜<VAR>inst✝ : NoZeroSMulDivisors 𝕜 E<VAR>A B : Set E<VAR>x : E<GOAL>x ∈ extremePoints 𝕜 A ↔ x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝⁴ : LinearOrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : DenselyOrdered 𝕜<VAR>inst✝ : NoZeroSMulDivisors 𝕜 E<VAR>A B : Set E<VAR>x : E<VAR>hxA : x ∈ A<VAR>x₁ : E<VAR>h₁ : x₁ ∈ A<VAR>x₂ : E<VAR>h₂ : x₂ ∈ A<GOAL>x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x ↔ x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x
<VAR>B : Type u₁<VAR>inst✝² : Bicategory B<VAR>C : Type u₂<VAR>inst✝¹ : Bicategory C<VAR>D : Type u₃<VAR>inst✝ : Bicategory D<VAR>F✝ : Pseudofunctor B C<VAR>F : OplaxFunctor B C<VAR>F' : F.PseudoCore<VAR>a✝ b✝ c✝ : B<VAR>f : a✝ ⟶ b✝<VAR>g h : b✝ ⟶ c✝<VAR>η : g ⟶ h<GOAL>F.map₂ (f ◁ η) = (F'.mapCompIso f g).hom ≫ F.map f ◁ F.map₂ η ≫ (F'.mapCompIso f h).inv
<VAR>B : Type u₁<VAR>inst✝² : Bicategory B<VAR>C : Type u₂<VAR>inst✝¹ : Bicategory C<VAR>D : Type u₃<VAR>inst✝ : Bicategory D<VAR>F✝ : Pseudofunctor B C<VAR>F : OplaxFunctor B C<VAR>F' : F.PseudoCore<VAR>a✝ b✝ c✝ : B<VAR>f✝ g✝ : a✝ ⟶ b✝<VAR>η : f✝ ⟶ g✝<VAR>h : b✝ ⟶ c✝<GOAL>F.map₂ (η ▷ h) = (F'.mapCompIso f✝ h).hom ≫ F.map₂ η ▷ F.map h ≫ (F'.mapCompIso g✝ h).inv
<VAR>B : Type u₁<VAR>inst✝² : Bicategory B<VAR>C : Type u₂<VAR>inst✝¹ : Bicategory C<VAR>D : Type u₃<VAR>inst✝ : Bicategory D<VAR>F✝ : Pseudofunctor B C<VAR>F : OplaxFunctor B C<VAR>F' : F.PseudoCore<VAR>a✝ b✝ c✝ d✝ : B<VAR>f : a✝ ⟶ b✝<VAR>g : b✝ ⟶ c✝<VAR>h : c✝ ⟶ d✝<GOAL>F.map₂ (α_ f g h).hom = (F'.mapCompIso (f ≫ g) h).hom ≫ (F'.mapCompIso f g).hom ▷ F.map h ≫ (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>f : α → E<VAR>hf : LocallyIntegrable f μ<GOAL>∀ᵐ (x : α) ∂μ, Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>f : α → E<VAR>hf : LocallyIntegrable f μ<VAR>u : ℕ → Set α<VAR>u_open : ∀ (n : ℕ), IsOpen (u n)<VAR>u_univ : ⋃ n, u n = univ<VAR>hu : ∀ (n : ℕ), IntegrableOn f (u n) μ<GOAL>∀ᵐ (x : α) ∂μ, Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>f : α → E<VAR>hf : LocallyIntegrable f μ<VAR>u : ℕ → Set α<VAR>u_open : ∀ (n : ℕ), IsOpen (u n)<VAR>u_univ : ⋃ n, u n = univ<VAR>hu : ∀ (n : ℕ), IntegrableOn f (u n) μ<VAR>this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖(u n).indicator f y - (u n).indicator f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)<GOAL>∀ᵐ (x : α) ∂μ, Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>f : α → E<VAR>hf : LocallyIntegrable f μ<VAR>u : ℕ → Set α<VAR>u_open : ∀ (n : ℕ), IsOpen (u n)<VAR>u_univ : ⋃ n, u n = univ<VAR>hu : ∀ (n : ℕ), IntegrableOn f (u n) μ<VAR>this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖(u n).indicator f y - (u n).indicator f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)<VAR>x : α<VAR>hx : ∀ (i : ℕ), Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖(u i).indicator f y - (u i).indicator f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)<GOAL>Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>f : α → E<VAR>hf : LocallyIntegrable f μ<VAR>u : ℕ → Set α<VAR>u_open : ∀ (n : ℕ), IsOpen (u n)<VAR>u_univ : ⋃ n, u n = univ<VAR>hu : ∀ (n : ℕ), IntegrableOn f (u n) μ<VAR>this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖(u n).indicator f y - (u n).indicator f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)<VAR>x : α<VAR>hx : ∀ (i : ℕ), Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖(u i).indicator f y - (u i).indicator f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)<VAR>n : ℕ<VAR>hn : x ∈ u n<GOAL>Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>f : α → E<VAR>hf : LocallyIntegrable f μ<VAR>u : ℕ → Set α<VAR>u_open : ∀ (n : ℕ), IsOpen (u n)<VAR>u_univ : ⋃ n, u n = univ<VAR>hu : ∀ (n : ℕ), IntegrableOn f (u n) μ<VAR>this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖(u n).indicator f y - (u n).indicator f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)<VAR>x : α<VAR>hx : ∀ (i : ℕ), Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖(u i).indicator f y - (u i).indicator f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)<VAR>n : ℕ<VAR>hn : x ∈ u n<GOAL>(fun a => (∫⁻ (y : α) in a, ↑‖(u n).indicator f y - (u n).indicator f x‖₊ ∂μ) / μ a) =ᶠ[v.filterAt x] fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / μ a
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>f : α → E<VAR>hf : LocallyIntegrable f μ<VAR>u : ℕ → Set α<VAR>u_open : ∀ (n : ℕ), IsOpen (u n)<VAR>u_univ : ⋃ n, u n = univ<VAR>hu : ∀ (n : ℕ), IntegrableOn f (u n) μ<VAR>this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖(u n).indicator f y - (u n).indicator f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)<VAR>x : α<VAR>hx : ∀ (i : ℕ), Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖(u i).indicator f y - (u i).indicator f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)<VAR>n : ℕ<VAR>hn : x ∈ u n<VAR>a : Set α<VAR>ha : a ⊆ u n<VAR>h'a : MeasurableSet a<GOAL>(∫⁻ (y : α) in a, ↑‖(u n).indicator f y - (u n).indicator f x‖₊ ∂μ) / μ a = (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / μ a
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>f : α → E<VAR>hf : LocallyIntegrable f μ<VAR>u : ℕ → Set α<VAR>u_open : ∀ (n : ℕ), IsOpen (u n)<VAR>u_univ : ⋃ n, u n = univ<VAR>hu : ∀ (n : ℕ), IntegrableOn f (u n) μ<VAR>this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖(u n).indicator f y - (u n).indicator f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)<VAR>x : α<VAR>hx : ∀ (i : ℕ), Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖(u i).indicator f y - (u i).indicator f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)<VAR>n : ℕ<VAR>hn : x ∈ u n<VAR>a : Set α<VAR>ha : a ⊆ u n<VAR>h'a : MeasurableSet a<GOAL>∫⁻ (y : α) in a, ↑‖(u n).indicator f y - (u n).indicator f x‖₊ ∂μ = ∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ