ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N₁ N₂ : Bimod Y Z<VAR>f : N₁ ⟶ N₂<GOAL>(tensorRight Z.X).map (coequalizer.π (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft)) ≫ (M.tensorBimod N₁).actRight ≫ colimMap (parallelPairHom (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft) ((M.X ⊗ Y.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) = (tensorRight Z.X).map (coequalizer.π (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft)) ≫ colimMap (parallelPairHom (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft) ((M.X ⊗ Y.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) ▷ Z.X ≫ (M.tensorBimod N₂).actRight
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N₁ N₂ : Bimod Y Z<VAR>f : N₁ ⟶ N₂<GOAL>coequalizer.π (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) ▷ Z.X ≫ TensorBimod.actRight M N₁ ≫ colimMap (parallelPairHom (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft) ((M.X ⊗ Y.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) = coequalizer.π (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) ▷ Z.X ≫ colimMap (parallelPairHom (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft) ((M.X ⊗ Y.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) ▷ Z.X ≫ TensorBimod.actRight M N₂
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N₁ N₂ : Bimod Y Z<VAR>f : N₁ ⟶ N₂<GOAL>((α_ M.X N₁.X Z.X).hom ≫ M.X ◁ N₁.actRight ≫ coequalizer.π (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft)) ≫ colimMap (parallelPairHom (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft) ((M.X ⊗ Y.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) = coequalizer.π (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) ▷ Z.X ≫ colimMap (parallelPairHom (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft) ((M.X ⊗ Y.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) ▷ Z.X ≫ TensorBimod.actRight M N₂
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N₁ N₂ : Bimod Y Z<VAR>f : N₁ ⟶ N₂<GOAL>(α_ M.X N₁.X Z.X).hom ≫ M.X ◁ N₁.actRight ≫ M.X ◁ f.hom ≫ colimit.ι (parallelPair (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft)) WalkingParallelPair.one = coequalizer.π (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) ▷ Z.X ≫ colimMap (parallelPairHom (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft) ((M.X ⊗ Y.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) ▷ Z.X ≫ TensorBimod.actRight M N₂
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N₁ N₂ : Bimod Y Z<VAR>f : N₁ ⟶ N₂<GOAL>(α_ M.X N₁.X Z.X).hom ≫ M.X ◁ (f.hom ▷ Z.X ≫ N₂.actRight) ≫ colimit.ι (parallelPair (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft)) WalkingParallelPair.one = coequalizer.π (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) ▷ Z.X ≫ colimMap (parallelPairHom (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft) ((M.X ⊗ Y.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) ▷ Z.X ≫ TensorBimod.actRight M N₂
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N₁ N₂ : Bimod Y Z<VAR>f : N₁ ⟶ N₂<GOAL>(α_ M.X N₁.X Z.X).hom ≫ M.X ◁ (f.hom ▷ Z.X ≫ N₂.actRight) ≫ colimit.ι (parallelPair (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft)) WalkingParallelPair.one = ((M.X ◁ f.hom) ▷ Z.X ≫ colimit.ι (parallelPair (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft)) WalkingParallelPair.one ▷ Z.X) ≫ TensorBimod.actRight M N₂
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N₁ N₂ : Bimod Y Z<VAR>f : N₁ ⟶ N₂<GOAL>(α_ M.X N₁.X Z.X).hom ≫ M.X ◁ (f.hom ▷ Z.X ≫ N₂.actRight) ≫ colimit.ι (parallelPair (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft)) WalkingParallelPair.one = (M.X ◁ f.hom) ▷ Z.X ≫ (α_ M.X N₂.X Z.X).hom ≫ M.X ◁ N₂.actRight ≫ coequalizer.π (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft)
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>𝕝 : Type u_3<VAR>R : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>M : Type u_7<VAR>inst✝⁶ : CommSemiring 𝕜<VAR>inst✝⁵ : TopologicalSpace 𝕜<VAR>inst✝⁴ : ContinuousAdd 𝕜<VAR>inst✝³ : ContinuousConstSMul 𝕜 𝕜<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : TopologicalSpace E<VAR>V : Set E<VAR>hV : IsOpen (⇑(continuousLinearMapToWeakSpace 𝕜 E) '' V)<GOAL>IsOpen V
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>r : ℝ<GOAL>2 • o.oangle x (r • x) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f g : α → M<VAR>a b : α<VAR>s t : Set α<VAR>hs : (s ∩ mulSupport f).Finite<VAR>ht : (t ∩ mulSupport f).Finite<GOAL>(∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f g : α → M<VAR>a b : α<VAR>s t : Set α<VAR>hs : (s ∩ mulSupport f).Finite<VAR>ht : (t ∩ mulSupport f).Finite<GOAL>(∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ t ∩ mulSupport f), f i = (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f ∩ (t ∩ mulSupport f)), f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f g : α → M<VAR>a b : α<VAR>s t : Set α<VAR>hs : (s ∩ mulSupport f).Finite<VAR>ht : (t ∩ mulSupport f).Finite<GOAL>(fun i => ∏ᶠ (_ : i ∈ s ∩ t ∩ mulSupport f), f i) = fun i => ∏ᶠ (_ : i ∈ s ∩ mulSupport f ∩ (t ∩ mulSupport f)), f i
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>p : ℝ<VAR>hp : p ≠ 0<GOAL>(fun z => p * z ^ (p - 1) * (1 + ε z) - z ^ (p - 1) / log z ^ 2) ~[atTop] fun z => p * z ^ (p - 1)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>p : ℝ<VAR>hp : p ≠ 0<GOAL>(fun z => p * z ^ (p - 1) * (1 + ε z)) ~[atTop] fun z => p * z ^ (p - 1)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>p : ℝ<VAR>hp : p ≠ 0<GOAL>(fun z => -(z ^ (p - 1) / log z ^ 2)) =o[atTop] fun z => p * z ^ (p - 1)
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<GOAL>‖iteratedFDeriv 𝕜 n (fderiv 𝕜 f) x‖ = ‖iteratedFDeriv 𝕜 (n + 1) f x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>s : Finset α<VAR>h : ∀ x ∈ s, p x<GOAL>∀ (a : α), a ∈ map (Embedding.subtype p) (Finset.subtype p s) ↔ a ∈ s
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F₁ : Type u_3<VAR>F₂ : Type u_4<VAR>M : Type u_5<VAR>E₁ : B → Type u_6<VAR>E₂ : B → Type u_7<VAR>inst✝²⁹ : NontriviallyNormedField 𝕜<VAR>inst✝²⁸ : (x : B) → AddCommGroup (E₁ x)<VAR>inst✝²⁷ : (x : B) → Module 𝕜 (E₁ x)<VAR>inst✝²⁶ : NormedAddCommGroup F₁<VAR>inst✝²⁵ : NormedSpace 𝕜 F₁<VAR>inst✝²⁴ : TopologicalSpace (TotalSpace F₁ E₁)<VAR>inst✝²³ : (x : B) → TopologicalSpace (E₁ x)<VAR>inst✝²² : (x : B) → AddCommGroup (E₂ x)<VAR>inst✝²¹ : (x : B) → Module 𝕜 (E₂ x)<VAR>inst✝²⁰ : NormedAddCommGroup F₂<VAR>inst✝¹⁹ : NormedSpace 𝕜 F₂<VAR>inst✝¹⁸ : TopologicalSpace (TotalSpace F₂ E₂)<VAR>inst✝¹⁷ : (x : B) → TopologicalSpace (E₂ x)<VAR>inst✝¹⁶ : ∀ (x : B), TopologicalAddGroup (E₂ x)<VAR>inst✝¹⁵ : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)<VAR>EB : Type u_8<VAR>inst✝¹⁴ : NormedAddCommGroup EB<VAR>inst✝¹³ : NormedSpace 𝕜 EB<VAR>HB : Type u_9<VAR>inst✝¹² : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>inst✝¹¹ : TopologicalSpace B<VAR>inst✝¹⁰ : ChartedSpace HB B<VAR>EM : Type u_10<VAR>inst✝⁹ : NormedAddCommGroup EM<VAR>inst✝⁸ : NormedSpace 𝕜 EM<VAR>HM : Type u_11<VAR>inst✝⁷ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace HM M<VAR>inst✝⁴ : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝³ : FiberBundle F₁ E₁<VAR>inst✝² : VectorBundle 𝕜 F₁ E₁<VAR>inst✝¹ : FiberBundle F₂ E₂<VAR>inst✝ : VectorBundle 𝕜 F₂ E₂<VAR>e₁ e₁' : Trivialization F₁ TotalSpace.proj<VAR>e₂ e₂' : Trivialization F₂ TotalSpace.proj<VAR>y₀ y : LE₁E₂<GOAL>↑(chartAt (ModelProd HB (F₁ →L[𝕜] F₂)) y₀) y = (↑(chartAt HB y₀.proj) y.proj, inCoordinates F₁ E₁ F₂ E₂ y₀.proj y.proj y₀.proj y.proj y.snd)
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a c u v w : V<VAR>e : Sym2 V<VAR>h : G.Adj a a<GOAL>False
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Module α ℝ<VAR>inst✝ : OrderedSMul α ℝ<VAR>a : α<VAR>ha : a ≤ 0<VAR>s : Set ℝ<GOAL>sInf (a • s) = a • sSup s
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Module α ℝ<VAR>inst✝ : OrderedSMul α ℝ<VAR>a : α<VAR>ha : a ≤ 0<GOAL>sInf (a • ∅) = a • sSup ∅
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Module α ℝ<VAR>inst✝ : OrderedSMul α ℝ<VAR>a : α<VAR>ha : a ≤ 0<VAR>s : Set ℝ<VAR>hs : s.Nonempty<GOAL>sInf (a • s) = a • sSup s
<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>hρ : ρ ≪ μ<VAR>q : ℝ≥0<VAR>s : Set α<VAR>h : s ⊆ {x | ↑q < v.limRatioMeas hρ x}<VAR>t : Set α := {x | Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}<GOAL>↑q * μ s ≤ ρ s
<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>hρ : ρ ≪ μ<VAR>q : ℝ≥0<VAR>s : Set α<VAR>h : s ⊆ {x | ↑q < v.limRatioMeas hρ x}<VAR>t : Set α := {x | Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}<VAR>A : μ tᶜ = 0<GOAL>↑q * μ s ≤ ρ s
<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>hρ : ρ ≪ μ<VAR>q : ℝ≥0<VAR>s : Set α<VAR>h : s ⊆ {x | ↑q < v.limRatioMeas hρ x}<VAR>t : Set α := {x | Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}<VAR>A : μ tᶜ = 0<GOAL>(q • μ) (s ∩ t) ≤ ρ (s ∩ t)
<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>hρ : ρ ≪ μ<VAR>q : ℝ≥0<VAR>s : Set α<VAR>h : s ⊆ {x | ↑q < v.limRatioMeas hρ x}<VAR>t : Set α := {x | Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}<VAR>A : μ tᶜ = 0<GOAL>∀ x ∈ s ∩ t, ∃ᶠ (a : Set α) in v.filterAt x, (q • μ) a ≤ ρ 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>hρ : ρ ≪ μ<VAR>q : ℝ≥0<VAR>s : Set α<VAR>h : s ⊆ {x | ↑q < v.limRatioMeas hρ x}<VAR>t : Set α := {x | Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}<VAR>A : μ tᶜ = 0<VAR>x : α<VAR>hx : x ∈ s ∩ t<GOAL>∃ᶠ (a : Set α) in v.filterAt x, (q • μ) a ≤ ρ 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>hρ : ρ ≪ μ<VAR>q : ℝ≥0<VAR>s : Set α<VAR>h : s ⊆ {x | ↑q < v.limRatioMeas hρ x}<VAR>t : Set α := {x | Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}<VAR>A : μ tᶜ = 0<VAR>x : α<VAR>hx : x ∈ s ∩ t<VAR>I : ∀ᶠ (a : Set α) in v.filterAt x, ↑q < ρ a / μ a<GOAL>∃ᶠ (a : Set α) in v.filterAt x, (q • μ) a ≤ ρ 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>hρ : ρ ≪ μ<VAR>q : ℝ≥0<VAR>s : Set α<VAR>h : s ⊆ {x | ↑q < v.limRatioMeas hρ x}<VAR>t : Set α := {x | Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}<VAR>A : μ tᶜ = 0<VAR>x : α<VAR>hx : x ∈ s ∩ t<VAR>I : ∀ᶠ (a : Set α) in v.filterAt x, ↑q < ρ a / μ a<VAR>a : Set α<VAR>ha : ↑q < ρ a / μ a<GOAL>(q • μ) a ≤ ρ 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>hρ : ρ ≪ μ<VAR>q : ℝ≥0<VAR>s : Set α<VAR>h : s ⊆ {x | ↑q < v.limRatioMeas hρ x}<VAR>t : Set α := {x | Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}<VAR>A : μ tᶜ = 0<VAR>x : α<VAR>hx : x ∈ s ∩ t<VAR>I : ∀ᶠ (a : Set α) in v.filterAt x, ↑q < ρ a / μ a<VAR>a : Set α<VAR>ha : ↑q < ρ a / μ a<GOAL>↑q * μ a ≤ ρ a
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v s t : Finset α<VAR>i j : ℕ<VAR>hj : 0 < j<GOAL>j * (j - 1) * (i / j + 1) ^ 2 < (i + j) ^ 2
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v s t : Finset α<VAR>i j : ℕ<VAR>hj : 0 < j<VAR>this : j * (j - 1) < j ^ 2<GOAL>j * (j - 1) * (i / j + 1) ^ 2 < (i + j) ^ 2
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v s t : Finset α<VAR>i j : ℕ<VAR>hj : 0 < j<VAR>this : j * (j - 1) < j ^ 2<GOAL>j ^ 2 * (i / j).succ ^ 2 ≤ (i + j) ^ 2
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v s t : Finset α<VAR>i j : ℕ<VAR>hj : 0 < j<VAR>this : j * (j - 1) < j ^ 2<GOAL>(j * (i / j).succ) ^ 2 ≤ (i + j) ^ 2
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>∫ (x : ℝ) in -1 ..1, √(1 - x ^ 2) = ∫ (x : ℝ) in sin (-(π / 2))..sin (π / 2), √(1 - x ^ 2)
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>∫ (x : ℝ) in -(π / 2)..π / 2, √(1 - sin x ^ 2) * cos x = ∫ (x : ℝ) in -(π / 2)..π / 2, cos x ^ 2
<VAR>a b : ℝ<VAR>n : ℕ<VAR>x✝ : ℝ<VAR>h : x✝ ∈ Ι (-(π / 2)) (π / 2)<GOAL>√(1 - sin x✝ ^ 2) * cos x✝ = cos x✝ ^ 2
<VAR>a b : ℝ<VAR>n : ℕ<VAR>x✝ : ℝ<VAR>h : -(π / 2) < x✝ ∧ x✝ ≤ π / 2<GOAL>√(1 - sin x✝ ^ 2) * cos x✝ = cos x✝ ^ 2
<VAR>E : Type u_1<VAR>inst✝¹¹ : AddCommGroup E<VAR>inst✝¹⁰ : TopologicalSpace E<VAR>inst✝⁹ : TopologicalAddGroup E<VAR>inst✝⁸ : T2Space E<VAR>inst✝⁷ : Module ℝ E<VAR>inst✝⁶ : ContinuousSMul ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>G : Type u_3<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>inst✝ : FiniteDimensional ℝ G<VAR>f g : F → G<VAR>n : ℕ∞<VAR>hf : ContDiff ℝ n f<VAR>hg : ContDiff ℝ n g<VAR>h : ∀ (x : F), f x ≠ g x<GOAL>ContDiff ℝ n fun x => Dist.dist (toEuclidean (f x)) (toEuclidean (g x))
<VAR>E : Type u_1<VAR>inst✝¹¹ : AddCommGroup E<VAR>inst✝¹⁰ : TopologicalSpace E<VAR>inst✝⁹ : TopologicalAddGroup E<VAR>inst✝⁸ : T2Space E<VAR>inst✝⁷ : Module ℝ E<VAR>inst✝⁶ : ContinuousSMul ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>G : Type u_3<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>inst✝ : FiniteDimensional ℝ G<VAR>f g : F → G<VAR>n : ℕ∞<VAR>hf : ContDiff ℝ n f<VAR>hg : ContDiff ℝ n g<VAR>h : ∀ (x : F), f x ≠ g x<GOAL>ContDiff ℝ n fun y => toEuclidean (f y)
<VAR>E : Type u_1<VAR>inst✝¹¹ : AddCommGroup E<VAR>inst✝¹⁰ : TopologicalSpace E<VAR>inst✝⁹ : TopologicalAddGroup E<VAR>inst✝⁸ : T2Space E<VAR>inst✝⁷ : Module ℝ E<VAR>inst✝⁶ : ContinuousSMul ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>G : Type u_3<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>inst✝ : FiniteDimensional ℝ G<VAR>f g : F → G<VAR>n : ℕ∞<VAR>hf : ContDiff ℝ n f<VAR>hg : ContDiff ℝ n g<VAR>h : ∀ (x : F), f x ≠ g x<GOAL>ContDiff ℝ n fun y => toEuclidean (g y)
<VAR>E : Type u_1<VAR>inst✝¹¹ : AddCommGroup E<VAR>inst✝¹⁰ : TopologicalSpace E<VAR>inst✝⁹ : TopologicalAddGroup E<VAR>inst✝⁸ : T2Space E<VAR>inst✝⁷ : Module ℝ E<VAR>inst✝⁶ : ContinuousSMul ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>G : Type u_3<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>inst✝ : FiniteDimensional ℝ G<VAR>f g : F → G<VAR>n : ℕ∞<VAR>hf : ContDiff ℝ n f<VAR>hg : ContDiff ℝ n g<VAR>h : ∀ (x : F), f x ≠ g x<GOAL>∀ (x : F), toEuclidean (f x) ≠ toEuclidean (g x)
<VAR>n m : ℕ<VAR>P : MvPFunctor.{u} n<VAR>Q : Fin2 n → MvPFunctor.{u} m<VAR>α✝ β : TypeVec.{u} m<VAR>α : TypeVec.{u} n<VAR>r : ⦃i : Fin2 n⦄ → α i → α i → Prop<VAR>x y : ↑P α<VAR>a : P.A<VAR>f₀ f₁ : P.B a ⟹ α<VAR>xeq : x = ⟨a, f₀⟩<VAR>yeq : y = ⟨a, f₁⟩<VAR>h : ∀ (i : Fin2 n) (j : P.B a i), r (f₀ i j) (f₁ i j)<GOAL>LiftR r x y
<VAR>n m : ℕ<VAR>P : MvPFunctor.{u} n<VAR>Q : Fin2 n → MvPFunctor.{u} m<VAR>α✝ β : TypeVec.{u} m<VAR>α : TypeVec.{u} n<VAR>r : ⦃i : Fin2 n⦄ → α i → α i → Prop<VAR>x y : ↑P α<VAR>a : P.A<VAR>f₀ f₁ : P.B a ⟹ α<VAR>xeq : x = ⟨a, f₀⟩<VAR>yeq : y = ⟨a, f₁⟩<VAR>h : ∀ (i : Fin2 n) (j : P.B a i), r (f₀ i j) (f₁ i j)<GOAL>(fun i t => (↑t).1) <$$> ⟨a, fun i j => ⟨(f₀ i j, f₁ i j), ⋯⟩⟩ = x ∧ (fun i t => (↑t).2) <$$> ⟨a, fun i j => ⟨(f₀ i j, f₁ i j), ⋯⟩⟩ = y
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>L' : Type w₁<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>I J : LieIdeal R L<VAR>f : L' →ₗ⁅R⁆ L<VAR>k : ℕ<GOAL>map I.incl (derivedSeries R (↥↑I) k) = derivedSeriesOfIdeal R L k I
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>L' : Type w₁<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>I J : LieIdeal R L<VAR>f : L' →ₗ⁅R⁆ L<VAR>k : ℕ<GOAL>derivedSeriesOfIdeal R L k I ≤ I
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>ι : Type u_1<VAR>inst✝ : Unique ι<VAR>h : finrank K V = 1<VAR>v : V<VAR>hv : v ≠ 0<GOAL>Set.range ⇑(basisSingleton ι h v hv) = {v}
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a b : α<GOAL>a + b - ↑⌊a + b⌋ - (a - ↑⌊a⌋) - (b - ↑⌊b⌋) = ↑(⌊a⌋ + ⌊b⌋ - ⌊a + b⌋)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a b : α<GOAL>a + b + -↑⌊a + b⌋ + (↑⌊a⌋ + -a) + (↑⌊b⌋ + -b) = ↑⌊a⌋ + ↑⌊b⌋ + -↑⌊a + b⌋
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : α → β → γ<VAR>a : Option α<VAR>b : Option β<VAR>c✝ : Option γ<VAR>c : γ<GOAL>c ∈ map₂ f a b ↔ ∃ a' b', a' ∈ a ∧ b' ∈ b ∧ f a' b' = c
<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>c : F<GOAL>deriv (fun y => c - f y) x = -deriv f x
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>p : α → Bool<VAR>a : α<VAR>l : List α<VAR>h : p a = true<GOAL>count a (filter p l) = count a l
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>p : α → Bool<VAR>a : α<VAR>l : List α<VAR>h : p a = true<GOAL>countP (fun a_1 => decide ((a_1 == a) = true ∧ p a_1 = true)) l = countP (fun x => x == a) l
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>p : α → Bool<VAR>a : α<VAR>l : List α<VAR>h : p a = true<GOAL>(fun a_1 => decide ((a_1 == a) = true ∧ p a_1 = true)) = fun x => x == a