ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>f g : ↥A<GOAL>2⁻¹ • (↑f + ↑g - |↑g - ↑f|) ∈ A.topologicalClosure
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>s : Set α<VAR>inst✝ : NoMaxOrder α<VAR>a b : α<VAR>h : a < b<GOAL>frontier (Ioc a b) = {a, b}
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : WeierstrassCurve R<VAR>A : Type v<VAR>inst✝ : CommRing A<VAR>φ : R →+* A<VAR>C C' : VariableChange R<GOAL>{ u := (Units.map ↑φ) (C.u * C'.u), r := φ (C.r * ↑C'.u ^ 2 + C'.r), s := φ (↑C'.u * C.s + C'.s), t := φ (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) } = { u := (Units.map ↑φ) C.u * (Units.map ↑φ) C'.u, r := φ C.r * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.r, s := ↑((Units.map ↑φ) C'.u) * φ C.s + φ C'.s, t := φ C.t * ↑((Units.map ↑φ) C'.u) ^ 3 + φ C.r * φ C'.s * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.t }
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : DivisionRing α<VAR>inst✝¹ : DivisionRing β<VAR>inst✝ : RingHomClass F α β<VAR>f : F<VAR>q : ℚ<GOAL>f ↑q = ↑q
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>T : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace T<VAR>K✝ : Set X<VAR>U✝ : Set Y<VAR>f : C(X, Y)<VAR>K : Set X<VAR>hK : IsCompact K<VAR>U : Set Z<VAR>hU : IsOpen U<GOAL>IsOpen {x | MapsTo (⇑(x.comp f)) K U}
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>a : α<VAR>s t : Multiset α<VAR>f g : α → Multiset β<GOAL>(s.bind fun x => 0) = 0
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : CommMonoid M<VAR>x y : M<VAR>hu : IsUnit (x * y)<GOAL>IsUnit (y * x)
<VAR>n m : SimplexCategory<VAR>f : n ⟶ m<GOAL>Mono f ↔ Function.Injective ⇑(Hom.toOrderHom f)
<VAR>n m : SimplexCategory<VAR>f : n ⟶ m<GOAL>Mono (skeletalEquivalence.functor.map f) ↔ Function.Injective ⇑(Hom.toOrderHom f)
<VAR>n m : SimplexCategory<VAR>f : n ⟶ m<GOAL>Mono (skeletalFunctor.map f) ↔ Function.Injective ⇑(Hom.toOrderHom f)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>inst✝ : Finite ↑(commutatorSet G)<VAR>hG : ¬(center G).index = 0<VAR>this : (center G).FiniteIndex<GOAL>Nat.card ↥(_root_.commutator G) ∣ (center G).index ^ ((center G).index * Nat.card ↑(commutatorSet G) + 1)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>inst✝ : Finite ↑(commutatorSet G)<VAR>hG : ¬(center G).index = 0<VAR>this : (center G).FiniteIndex<GOAL>Nat.card ↥((center G).subgroupOf (_root_.commutator G)) * ((center G).subgroupOf (_root_.commutator G)).index ∣ (center G).index ^ ((center G).index * Nat.card ↑(commutatorSet G)) * (center G).index
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>inst✝ : Finite ↑(commutatorSet G)<VAR>hG : ¬(center G).index = 0<VAR>this : (center G).FiniteIndex<VAR>h1 : (center G).relindex (_root_.commutator G) ∣ (center G).index<GOAL>Nat.card ↥((center G).subgroupOf (_root_.commutator G)) * ((center G).subgroupOf (_root_.commutator G)).index ∣ (center G).index ^ ((center G).index * Nat.card ↑(commutatorSet G)) * (center G).index
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>inst✝ : Finite ↑(commutatorSet G)<VAR>hG : ¬(center G).index = 0<VAR>this : (center G).FiniteIndex<VAR>h1 : (center G).relindex (_root_.commutator G) ∣ (center G).index<GOAL>Nat.card ↥((center G).subgroupOf (_root_.commutator G)) ∣ (center G).index ^ ((center G).index * Nat.card ↑(commutatorSet G))
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>inst✝ : Finite ↑(commutatorSet G)<VAR>hG : ¬(center G).index = 0<VAR>this✝ : (center G).FiniteIndex<VAR>h1 : (center G).relindex (_root_.commutator G) ∣ (center G).index<VAR>this : ((center G).subgroupOf (_root_.commutator G)).FiniteIndex<GOAL>Nat.card ↥((center G).subgroupOf (_root_.commutator G)) ∣ (center G).index ^ ((center G).index * Nat.card ↑(commutatorSet G))
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>inst✝ : Finite ↑(commutatorSet G)<VAR>hG : ¬(center G).index = 0<VAR>this✝ : (center G).FiniteIndex<VAR>h1 : (center G).relindex (_root_.commutator G) ∣ (center G).index<VAR>this : ((center G).subgroupOf (_root_.commutator G)).FiniteIndex<VAR>h2 : Group.rank ↥((center G).subgroupOf (_root_.commutator G)) ≤ ((center G).subgroupOf (_root_.commutator G)).index * Group.rank ↥(_root_.commutator G)<GOAL>Nat.card ↥((center G).subgroupOf (_root_.commutator G)) ∣ (center G).index ^ ((center G).index * Nat.card ↑(commutatorSet G))
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>inst✝ : Finite ↑(commutatorSet G)<VAR>hG : ¬(center G).index = 0<VAR>this✝ : (center G).FiniteIndex<VAR>h1 : (center G).relindex (_root_.commutator G) ∣ (center G).index<VAR>this : ((center G).subgroupOf (_root_.commutator G)).FiniteIndex<VAR>h2 : Group.rank ↥((center G).subgroupOf (_root_.commutator G)) ≤ ((center G).subgroupOf (_root_.commutator G)).index * Group.rank ↥(_root_.commutator G)<VAR>h3 : (center G).relindex (_root_.commutator G) * Group.rank ↥(_root_.commutator G) ≤ (center G).index * Nat.card ↑(commutatorSet G)<GOAL>Nat.card ↥((center G).subgroupOf (_root_.commutator G)) ∣ (center G).index ^ ((center G).index * Nat.card ↑(commutatorSet G))
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>inst✝ : Finite ↑(commutatorSet G)<VAR>hG : ¬(center G).index = 0<VAR>this✝ : (center G).FiniteIndex<VAR>h1 : (center G).relindex (_root_.commutator G) ∣ (center G).index<VAR>this : ((center G).subgroupOf (_root_.commutator G)).FiniteIndex<VAR>h2 : Group.rank ↥((center G).subgroupOf (_root_.commutator G)) ≤ ((center G).subgroupOf (_root_.commutator G)).index * Group.rank ↥(_root_.commutator G)<VAR>h3 : (center G).relindex (_root_.commutator G) * Group.rank ↥(_root_.commutator G) ≤ (center G).index * Nat.card ↑(commutatorSet G)<GOAL>Nat.card ↥((center G).subgroupOf (_root_.commutator G)) ∣ (center G).index ^ Group.rank ↥((center G).subgroupOf (_root_.commutator G))
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>inst✝ : Finite ↑(commutatorSet G)<VAR>hG : ¬(center G).index = 0<VAR>this✝ : (center G).FiniteIndex<VAR>h1 : (center G).relindex (_root_.commutator G) ∣ (center G).index<VAR>this : ((center G).subgroupOf (_root_.commutator G)).FiniteIndex<VAR>h2 : Group.rank ↥((center G).subgroupOf (_root_.commutator G)) ≤ ((center G).subgroupOf (_root_.commutator G)).index * Group.rank ↥(_root_.commutator G)<VAR>h3 : (center G).relindex (_root_.commutator G) * Group.rank ↥(_root_.commutator G) ≤ (center G).index * Nat.card ↑(commutatorSet G)<GOAL>∀ (g : ↥((center G).subgroupOf (_root_.commutator G))), g ^ (center G).index = 1
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>inst✝ : Finite ↑(commutatorSet G)<VAR>hG : ¬(center G).index = 0<VAR>this✝ : (center G).FiniteIndex<VAR>h1 : (center G).relindex (_root_.commutator G) ∣ (center G).index<VAR>this : ((center G).subgroupOf (_root_.commutator G)).FiniteIndex<VAR>h2 : Group.rank ↥((center G).subgroupOf (_root_.commutator G)) ≤ ((center G).subgroupOf (_root_.commutator G)).index * Group.rank ↥(_root_.commutator G)<VAR>h3 : (center G).relindex (_root_.commutator G) * Group.rank ↥(_root_.commutator G) ≤ (center G).index * Nat.card ↑(commutatorSet G)<VAR>g : ↥((center G).subgroupOf (_root_.commutator G))<GOAL>g ^ (center G).index = 1
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>inst✝ : Finite ↑(commutatorSet G)<VAR>hG : ¬(center G).index = 0<VAR>this✝¹ : (center G).FiniteIndex<VAR>h1 : (center G).relindex (_root_.commutator G) ∣ (center G).index<VAR>this✝ : ((center G).subgroupOf (_root_.commutator G)).FiniteIndex<VAR>h2 : Group.rank ↥((center G).subgroupOf (_root_.commutator G)) ≤ ((center G).subgroupOf (_root_.commutator G)).index * Group.rank ↥(_root_.commutator G)<VAR>h3 : (center G).relindex (_root_.commutator G) * Group.rank ↥(_root_.commutator G) ≤ (center G).index * Nat.card ↑(commutatorSet G)<VAR>g : ↥((center G).subgroupOf (_root_.commutator G))<VAR>this : ↑↑g ∈ (MonoidHom.transferCenterPow G).ker<GOAL>g ^ (center G).index = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝¹ : Mul R<VAR>inst✝ : StarMul R<VAR>x : R<GOAL>IsSelfAdjoint (x * star x)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>n : ℕ<VAR>b : Basis (Fin n) R M<GOAL>b.flag (Fin.last n) = ⊤
<VAR>f : StieltjesFunction<VAR>l : ℝ<VAR>hf : Tendsto (↑f) atBot (𝓝 l)<VAR>x : ℝ<GOAL>f.measure (Iic x) = ofReal (↑f x - l)
<VAR>f : StieltjesFunction<VAR>l : ℝ<VAR>hf : Tendsto (↑f) atBot (𝓝 l)<VAR>x : ℝ<GOAL>Tendsto (fun x_1 => f.measure (Ioc x_1 x)) atBot (𝓝 (ofReal (↑f x - l)))
<VAR>f : StieltjesFunction<VAR>l : ℝ<VAR>hf : Tendsto (↑f) atBot (𝓝 l)<VAR>x : ℝ<GOAL>Tendsto (fun x_1 => ofReal (↑f x - ↑f x_1)) atBot (𝓝 (ofReal (↑f x - l)))
<VAR>X : TopCat<VAR>p₀ : ↑X<VAR>inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)<VAR>C : Type v<VAR>inst✝² : Category.{u, v} C<VAR>A : C<VAR>inst✝¹ : HasTerminal C<VAR>inst✝ : HasColimits C<VAR>x y : C<VAR>f : x ⟶ y<VAR>U : (OpenNhds p₀)ᵒᵖ<GOAL>colimit.ι (((whiskeringLeft (OpenNhds p₀)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion p₀).op).obj ((skyscraperPresheafFunctor p₀).obj x)) U ≫ (skyscraperPresheafFunctor p₀ ⋙ Presheaf.stalkFunctor C p₀).map f ≫ (fun c => (skyscraperPresheafStalkOfSpecializes p₀ c ⋯).hom) y = colimit.ι (((whiskeringLeft (OpenNhds p₀)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion p₀).op).obj ((skyscraperPresheafFunctor p₀).obj x)) U ≫ (fun c => (skyscraperPresheafStalkOfSpecializes p₀ c ⋯).hom) x ≫ (𝟭 C).map f
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝ : DivisionRing K<VAR>ι : Type v<VAR>hι : Infinite ι<GOAL>Module.rank K (ι → K) = #(ι → K)
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝ : DivisionRing K<VAR>ι : Type v<VAR>hι : Infinite ι<VAR>ιK : Type (max u v)<VAR>bK : Basis ιK K (ι → K)<GOAL>Module.rank K (ι → K) = #(ι → K)
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝ : DivisionRing K<VAR>ι : Type v<VAR>hι : Infinite ι<VAR>ιK : Type (max u v)<VAR>bK : Basis ιK K (ι → K)<VAR>e : ℕ ↪ ι<GOAL>Module.rank K (ι → K) = #(ι → K)
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝ : DivisionRing K<VAR>ι : Type v<VAR>hι : Infinite ι<VAR>ιK : Type (max u v)<VAR>bK : Basis ιK K (ι → K)<VAR>e : ℕ ↪ ι<VAR>this : lift.{max u v, u} (Module.rank K (ℕ → K)) ≤ lift.{u, max u v} (Module.rank K (ι → K))<GOAL>Module.rank K (ι → K) = #(ι → K)
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝ : DivisionRing K<VAR>ι : Type v<VAR>hι : Infinite ι<VAR>ιK : Type (max u v)<VAR>bK : Basis ιK K (ι → K)<VAR>e : ℕ ↪ ι<VAR>this : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)<GOAL>Module.rank K (ι → K) = #(ι → K)
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝ : DivisionRing K<VAR>ι : Type v<VAR>hι : Infinite ι<VAR>ιK : Type (max u v)<VAR>bK : Basis ιK K (ι → K)<VAR>e : ℕ ↪ ι<VAR>this : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)<VAR>key : lift.{v, u} (max ℵ₀ #K) ≤ Module.rank K (ι → K)<GOAL>Module.rank K (ι → K) = #(ι → K)
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝ : DivisionRing K<VAR>ι : Type v<VAR>hι : Infinite ι<VAR>ιK : Type (max u v)<VAR>bK : Basis ιK K (ι → K)<VAR>e : ℕ ↪ ι<VAR>this : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)<VAR>key : ℵ₀ ≤ Module.rank K (ι → K) ∧ lift.{v, u} #K ≤ Module.rank K (ι → K)<GOAL>Module.rank K (ι → K) = #(ι → K)
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝ : DivisionRing K<VAR>ι : Type v<VAR>hι : Infinite ι<VAR>ιK : Type (max u v)<VAR>bK : Basis ιK K (ι → K)<VAR>e : ℕ ↪ ι<VAR>this✝ : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)<VAR>key : ℵ₀ ≤ Module.rank K (ι → K) ∧ lift.{v, u} #K ≤ Module.rank K (ι → K)<VAR>this : Infinite ιK<GOAL>Module.rank K (ι → K) = #(ι → K)
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝ : DivisionRing K<VAR>ι : Type v<VAR>hι : Infinite ι<VAR>ιK : Type (max u v)<VAR>bK : Basis ιK K (ι → K)<VAR>e : ℕ ↪ ι<VAR>this✝ : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)<VAR>key : ℵ₀ ≤ Module.rank K (ι → K) ∧ lift.{v, u} #K ≤ Module.rank K (ι → K)<VAR>this : Infinite ιK<GOAL>lift.{v, u} #K ≤ Module.rank K (ι → K)
<VAR>C✝ : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C✝<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>F : D ⥤ E<VAR>hF : F.FullyFaithful<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.29894, u_1} C<VAR>X✝ Y✝ : C ⥤ D<VAR>f : ((CategoryTheory.whiskeringRight C D E).obj F).obj X✝ ⟶ ((CategoryTheory.whiskeringRight C D E).obj F).obj Y✝<VAR>x✝¹ x✝ : C<VAR>g : x✝¹ ⟶ x✝<GOAL>X✝.map g ≫ (fun X => hF.preimage (f.app X)) x✝ = (fun X => hF.preimage (f.app X)) x✝¹ ≫ Y✝.map g
<VAR>C✝ : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C✝<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>F : D ⥤ E<VAR>hF : F.FullyFaithful<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.29894, u_1} C<VAR>X✝ Y✝ : C ⥤ D<VAR>f : ((CategoryTheory.whiskeringRight C D E).obj F).obj X✝ ⟶ ((CategoryTheory.whiskeringRight C D E).obj F).obj Y✝<VAR>x✝¹ x✝ : C<VAR>g : x✝¹ ⟶ x✝<GOAL>F.map (X✝.map g ≫ (fun X => hF.preimage (f.app X)) x✝) = F.map ((fun X => hF.preimage (f.app X)) x✝¹ ≫ Y✝.map g)
<VAR>C✝ : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C✝<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>F : D ⥤ E<VAR>hF : F.FullyFaithful<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.29894, u_1} C<VAR>X✝ Y✝ : C ⥤ D<VAR>f : ((CategoryTheory.whiskeringRight C D E).obj F).obj X✝ ⟶ ((CategoryTheory.whiskeringRight C D E).obj F).obj Y✝<VAR>x✝¹ x✝ : C<VAR>g : x✝¹ ⟶ x✝<GOAL>F.map (X✝.map g ≫ hF.preimage (f.app x✝)) = F.map (hF.preimage (f.app x✝¹) ≫ Y✝.map g)
<VAR>C✝ : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C✝<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>F : D ⥤ E<VAR>hF : F.FullyFaithful<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.29894, u_1} C<VAR>X✝ Y✝ : C ⥤ D<VAR>f : ((CategoryTheory.whiskeringRight C D E).obj F).obj X✝ ⟶ ((CategoryTheory.whiskeringRight C D E).obj F).obj Y✝<VAR>x✝¹ x✝ : C<VAR>g : x✝¹ ⟶ x✝<GOAL>F.map (X✝.map g) ≫ f.app x✝ = f.app x✝¹ ≫ F.map (Y✝.map g)
<VAR>T : Type uT<VAR>g : ContextFreeGrammar T<VAR>s : List (Symbol T g.NT)<VAR>hgs : g.reverse.Derives [Symbol.nonterminal g.reverse.initial] s<GOAL>g.Derives [Symbol.nonterminal g.initial] s.reverse
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹¹ : TopologicalSpace X<VAR>inst✝¹⁰ : MeasurableSpace X<VAR>inst✝⁹ : BorelSpace X<VAR>inst✝⁸ : R1Space X<VAR>inst✝⁷ : TopologicalSpace Y<VAR>inst✝⁶ : MeasurableSpace Y<VAR>inst✝⁵ : BorelSpace Y<VAR>inst✝⁴ : R1Space Y<VAR>μ : Measure X<VAR>ν : Measure Y<VAR>inst✝³ : μ.InnerRegularCompactLTTop<VAR>inst✝² : IsLocallyFiniteMeasure ν<VAR>E : Type u_4<VAR>inst✝¹ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>inst✝ : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<GOAL>Continuous fun gf => (compMeasurePreserving ⇑↑gf.2 ⋯) gf.1
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹¹ : TopologicalSpace X<VAR>inst✝¹⁰ : MeasurableSpace X<VAR>inst✝⁹ : BorelSpace X<VAR>inst✝⁸ : R1Space X<VAR>inst✝⁷ : TopologicalSpace Y<VAR>inst✝⁶ : MeasurableSpace Y<VAR>inst✝⁵ : BorelSpace Y<VAR>inst✝⁴ : R1Space Y<VAR>μ : Measure X<VAR>ν : Measure Y<VAR>inst✝³ : μ.InnerRegularCompactLTTop<VAR>inst✝² : IsLocallyFiniteMeasure ν<VAR>E : Type u_4<VAR>inst✝¹ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>inst✝ : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>hp₀ : p ≠ 0<GOAL>Continuous fun gf => (compMeasurePreserving ⇑↑gf.2 ⋯) gf.1
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹¹ : TopologicalSpace X<VAR>inst✝¹⁰ : MeasurableSpace X<VAR>inst✝⁹ : BorelSpace X<VAR>inst✝⁸ : R1Space X<VAR>inst✝⁷ : TopologicalSpace Y<VAR>inst✝⁶ : MeasurableSpace Y<VAR>inst✝⁵ : BorelSpace Y<VAR>inst✝⁴ : R1Space Y<VAR>μ : Measure X<VAR>ν : Measure Y<VAR>inst✝³ : μ.InnerRegularCompactLTTop<VAR>inst✝² : IsLocallyFiniteMeasure ν<VAR>E : Type u_4<VAR>inst✝¹ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>inst✝ : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>hp₀ : p ≠ 0<GOAL>∀ a ∈ ↑(simpleFunc E p ν), Continuous fun y => (compMeasurePreserving ⇑↑(a, y).2 ⋯) (a, y).1
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹¹ : TopologicalSpace X<VAR>inst✝¹⁰ : MeasurableSpace X<VAR>inst✝⁹ : BorelSpace X<VAR>inst✝⁸ : R1Space X<VAR>inst✝⁷ : TopologicalSpace Y<VAR>inst✝⁶ : MeasurableSpace Y<VAR>inst✝⁵ : BorelSpace Y<VAR>inst✝⁴ : R1Space Y<VAR>μ : Measure X<VAR>ν : Measure Y<VAR>inst✝³ : μ.InnerRegularCompactLTTop<VAR>inst✝² : IsLocallyFiniteMeasure ν<VAR>E : Type u_4<VAR>inst✝¹ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>inst✝ : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>hp₀ : p ≠ 0<VAR>f : ↥(simpleFunc E p ν)<GOAL>Continuous fun y => (compMeasurePreserving ⇑↑(↑f, y).2 ⋯) (↑f, y).1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K : ℝ≥0<VAR>f : α → β<VAR>s : Set α<VAR>hf : AntilipschitzWith K (s.restrict f)<VAR>g : β → α<VAR>t : Set β<VAR>g_maps : MapsTo g t s<VAR>g_inv : RightInvOn g f t<VAR>x y : ↑t<GOAL>edist (t.restrict g x) (t.restrict g y) ≤ ↑K * edist x y
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → E →L[ℝ] F<VAR>h_add : FinMeasAdditive μ T<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<GOAL>setToSimpleFunc T (map Neg.neg f) = -setToSimpleFunc T f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → E →L[ℝ] F<VAR>h_add : FinMeasAdditive μ T<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<GOAL>∑ x ∈ f.range, (T (↑f ⁻¹' {x})) (-x) = ∑ x ∈ f.range, -(T (↑f ⁻¹' {x})) x
<VAR>l : ℝ<VAR>h : Tendsto (fun n => ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)<GOAL>Tendsto (fun k => ∑ i ∈ range k, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 (π / 4))
<VAR>l : ℝ<VAR>h : Tendsto (fun n => ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)<VAR>abel : Tendsto (fun x => ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) (𝓝[<] 1) (𝓝 l)<GOAL>Tendsto (fun k => ∑ i ∈ range k, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 (π / 4))
<VAR>l : ℝ<VAR>h : Tendsto (fun n => ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)<VAR>abel : Tendsto (fun x => ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) (𝓝[<] 1) (𝓝 l)<VAR>m : 𝓝[<] 1 ≤ 𝓝 1<GOAL>Tendsto (fun k => ∑ i ∈ range k, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 (π / 4))
<VAR>l : ℝ<VAR>h : Tendsto (fun n => ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)<VAR>abel : Tendsto (fun x => ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) (𝓝[<] 1) (𝓝 l)<VAR>m : 𝓝[<] 1 ≤ 𝓝 1<VAR>q : Tendsto (fun x => x ^ 2) (𝓝[<] 1) (𝓝[<] 1)<GOAL>Tendsto (fun k => ∑ i ∈ range k, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 (π / 4))
<VAR>l : ℝ<VAR>h : Tendsto (fun n => ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)<VAR>m : 𝓝[<] 1 ≤ 𝓝 1<VAR>q : Tendsto (fun x => x ^ 2) (𝓝[<] 1) (𝓝[<] 1)<VAR>abel : Tendsto (fun x => ((fun x => ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x => x ^ 2) x * x) (𝓝[<] 1) (𝓝 (l * 1))<GOAL>Tendsto (fun k => ∑ i ∈ range k, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 (π / 4))
<VAR>l : ℝ<VAR>h : Tendsto (fun n => ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)<VAR>m : 𝓝[<] 1 ≤ 𝓝 1<VAR>q : Tendsto (fun x => x ^ 2) (𝓝[<] 1) (𝓝[<] 1)<VAR>abel : Tendsto (fun x => ((fun x => ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x => x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)<GOAL>Tendsto (fun k => ∑ i ∈ range k, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 (π / 4))
<VAR>l : ℝ<VAR>h : Tendsto (fun n => ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)<VAR>m : 𝓝[<] 1 ≤ 𝓝 1<VAR>q : Tendsto (fun x => x ^ 2) (𝓝[<] 1) (𝓝[<] 1)<VAR>abel : Tendsto arctan (𝓝[<] 1) (𝓝 l)<GOAL>Tendsto (fun k => ∑ i ∈ range k, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 (π / 4))
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>n : ℕ<VAR>w : ℂ<GOAL>((cauchyPowerSeries f c R n) fun x => w) = (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>n : ℕ<VAR>w : ℂ<GOAL>(w ^ n • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z) = (2 * ↑π * I)⁻¹ • w ^ n • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z
<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Fact (p % 2 = 1)<VAR>a : ℕ<VAR>ha2✝ : a % 2 = 1<VAR>hap : ↑a ≠ 0<VAR>ha2 : ↑a = ↑1<GOAL>↑(filter (fun x => p / 2 < (↑a * ↑x).val) (Ico 1 (p / 2).succ)).card - ↑(∑ x ∈ Ico 1 (p / 2).succ, x * a / p) = 0
<VAR>a✝¹ b✝¹ c✝ d m n a✝ b✝ c a b : ℤ<GOAL>a < b ∨ b ≤ a
<VAR>a✝¹ b✝¹ c✝ d m n a✝ b✝ c a b : ℤ<GOAL>a < b ∨ ¬a < b
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝³ : Monoid M<VAR>inst✝² : AddMonoid N<VAR>G : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group G<VAR>inst✝ : AddGroup H<VAR>P : Subgroup G<GOAL>P.FG ↔ (toAddSubgroup P).FG
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → CanonicallyOrderedAddCommMonoid (α i)<VAR>inst✝³ : (i : ι) → Sub (α i)<VAR>inst✝² : ∀ (i : ι), OrderedSub (α i)<VAR>f g : Π₀ (i : ι), α i<VAR>i : ι<VAR>a b : α i<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)<GOAL>(f - g).support ⊆ f.support
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : LinearOrder α<VAR>inst✝⁵ : OrderTopology α<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝⁴ : Finite ι<VAR>inst✝³ : (i : ι) → LinearOrder (π i)<VAR>inst✝² : (i : ι) → TopologicalSpace (π i)<VAR>inst✝¹ : ∀ (i : ι), OrderTopology (π i)<VAR>a b x : (i : ι) → π i<VAR>a' b' x' : ι → α<VAR>inst✝ : Nonempty ι<VAR>ha : ∀ (i : ι), a i < x i<VAR>hb : ∀ (i : ι), x i < b i<GOAL>Ioo a b ∈ 𝓝 x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : LinearOrder α<VAR>inst✝⁵ : OrderTopology α<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝⁴ : Finite ι<VAR>inst✝³ : (i : ι) → LinearOrder (π i)<VAR>inst✝² : (i : ι) → TopologicalSpace (π i)<VAR>inst✝¹ : ∀ (i : ι), OrderTopology (π i)<VAR>a b x : (i : ι) → π i<VAR>a' b' x' : ι → α<VAR>inst✝ : Nonempty ι<VAR>ha : ∀ (i : ι), a i < x i<VAR>hb : ∀ (i : ι), x i < b i<VAR>i : ι<VAR>x✝ : i ∈ univ<GOAL>Ioo (a i) (b i) ∈ 𝓝 (x i)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : LinearOrder β<VAR>inst✝ : NoMaxOrder β<VAR>u : ℕ → β<VAR>hu : Tendsto u atTop atTop<VAR>N : ℕ<GOAL>∃ n ≥ N, ∀ k < n, u k < u n