ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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 F' : C ⥤ D<VAR>G : D ⥤ E<VAR>obj : C → D<VAR>map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)<VAR>F_obj : C → E<VAR>map✝¹ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)<VAR>map_id✝¹ : ∀ (X : C), { obj := F_obj, map := map✝¹ }.map (𝟙 X) = 𝟙 ({ obj := F_obj, map := map✝¹ }.obj X)<VAR>map_comp✝¹ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), { obj := F_obj, map := map✝¹ }.map (f ≫ g) = { obj := F_obj, map := map✝¹ }.map f ≫ { obj := F_obj, map := map✝¹ }.map g<VAR>inst✝¹ : { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.Faithful<VAR>G_obj : D → E<VAR>map✝ : {X Y : D} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)<VAR>map_id✝ : ∀ (X : D), { obj := G_obj, map := map✝ }.map (𝟙 X) = 𝟙 ({ obj := G_obj, map := map✝ }.obj X)<VAR>map_comp✝ : ∀ {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z), { obj := G_obj, map := map✝ }.map (f ≫ g) = { obj := G_obj, map := map✝ }.map f ≫ { obj := G_obj, map := map✝ }.map g<VAR>inst✝ : { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.Faithful<VAR>h_obj : ∀ (X : C), { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj (obj X) = { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj X<VAR>h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq ({ obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map (map f)) ({ obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map f)<GOAL>{ obj := fun X => { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj ({ obj := obj, map := map, map_id := ⋯, map_comp := ⋯ }.obj X), map := fun {X Y} f => { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map ({ obj := obj, map := map, map_id := ⋯, map_comp := ⋯ }.map f), map_id := ⋯, map_comp := ⋯ } = { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }
<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 F' : C ⥤ D<VAR>G : D ⥤ E<VAR>obj : C → D<VAR>map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)<VAR>F_obj : C → E<VAR>map✝¹ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)<VAR>map_id✝¹ : ∀ (X : C), { obj := F_obj, map := map✝¹ }.map (𝟙 X) = 𝟙 ({ obj := F_obj, map := map✝¹ }.obj X)<VAR>map_comp✝¹ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), { obj := F_obj, map := map✝¹ }.map (f ≫ g) = { obj := F_obj, map := map✝¹ }.map f ≫ { obj := F_obj, map := map✝¹ }.map g<VAR>inst✝¹ : { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.Faithful<VAR>G_obj : D → E<VAR>map✝ : {X Y : D} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)<VAR>map_id✝ : ∀ (X : D), { obj := G_obj, map := map✝ }.map (𝟙 X) = 𝟙 ({ obj := G_obj, map := map✝ }.obj X)<VAR>map_comp✝ : ∀ {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z), { obj := G_obj, map := map✝ }.map (f ≫ g) = { obj := G_obj, map := map✝ }.map f ≫ { obj := G_obj, map := map✝ }.map g<VAR>inst✝ : { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.Faithful<VAR>h_obj : ∀ (X : C), { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj (obj X) = { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj X<VAR>h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq ({ obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map (map f)) ({ obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map f)<VAR>this : F_obj = G_obj ∘ obj<GOAL>{ obj := fun X => { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj ({ obj := obj, map := map, map_id := ⋯, map_comp := ⋯ }.obj X), map := fun {X Y} f => { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map ({ obj := obj, map := map, map_id := ⋯, map_comp := ⋯ }.map f), map_id := ⋯, map_comp := ⋯ } = { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }
<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 F' : C ⥤ D<VAR>G : D ⥤ E<VAR>obj : C → D<VAR>map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)<VAR>G_obj : D → E<VAR>map✝¹ : {X Y : D} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)<VAR>map_id✝¹ : ∀ (X : D), { obj := G_obj, map := map✝¹ }.map (𝟙 X) = 𝟙 ({ obj := G_obj, map := map✝¹ }.obj X)<VAR>map_comp✝¹ : ∀ {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z), { obj := G_obj, map := map✝¹ }.map (f ≫ g) = { obj := G_obj, map := map✝¹ }.map f ≫ { obj := G_obj, map := map✝¹ }.map g<VAR>inst✝¹ : { obj := G_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.Faithful<VAR>map✝ : {X Y : C} → (X ⟶ Y) → ((G_obj ∘ obj) X ⟶ (G_obj ∘ obj) Y)<VAR>map_id✝ : ∀ (X : C), { obj := G_obj ∘ obj, map := map✝ }.map (𝟙 X) = 𝟙 ({ obj := G_obj ∘ obj, map := map✝ }.obj X)<VAR>map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), { obj := G_obj ∘ obj, map := map✝ }.map (f ≫ g) = { obj := G_obj ∘ obj, map := map✝ }.map f ≫ { obj := G_obj ∘ obj, map := map✝ }.map g<VAR>inst✝ : { obj := G_obj ∘ obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.Faithful<VAR>h_obj : ∀ (X : C), { obj := G_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj (obj X) = { obj := G_obj ∘ obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X<VAR>h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq ({ obj := G_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map (map f)) ({ obj := G_obj ∘ obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f)<GOAL>(fun {X Y} f => { obj := G_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map ({ obj := obj, map := map, map_id := ⋯, map_comp := ⋯ }.map f)) = map✝
<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 F' : C ⥤ D<VAR>G : D ⥤ E<VAR>obj : C → D<VAR>map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)<VAR>G_obj : D → E<VAR>map✝¹ : {X Y : D} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)<VAR>map_id✝¹ : ∀ (X : D), { obj := G_obj, map := map✝¹ }.map (𝟙 X) = 𝟙 ({ obj := G_obj, map := map✝¹ }.obj X)<VAR>map_comp✝¹ : ∀ {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z), { obj := G_obj, map := map✝¹ }.map (f ≫ g) = { obj := G_obj, map := map✝¹ }.map f ≫ { obj := G_obj, map := map✝¹ }.map g<VAR>inst✝¹ : { obj := G_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.Faithful<VAR>map✝ : {X Y : C} → (X ⟶ Y) → ((G_obj ∘ obj) X ⟶ (G_obj ∘ obj) Y)<VAR>map_id✝ : ∀ (X : C), { obj := G_obj ∘ obj, map := map✝ }.map (𝟙 X) = 𝟙 ({ obj := G_obj ∘ obj, map := map✝ }.obj X)<VAR>map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), { obj := G_obj ∘ obj, map := map✝ }.map (f ≫ g) = { obj := G_obj ∘ obj, map := map✝ }.map f ≫ { obj := G_obj ∘ obj, map := map✝ }.map g<VAR>inst✝ : { obj := G_obj ∘ obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.Faithful<VAR>h_obj : ∀ (X : C), { obj := G_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj (obj X) = { obj := G_obj ∘ obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X<VAR>h_map✝ : ∀ {X Y : C} {f : X ⟶ Y}, HEq ({ obj := G_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map (map f)) ({ obj := G_obj ∘ obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f)<VAR>h_map : ∀ {X Y : C} {f : X ⟶ Y}, map✝¹ (map f) = map✝ f<GOAL>(fun {X Y} f => { obj := G_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map ({ obj := obj, map := map, map_id := ⋯, map_comp := ⋯ }.map f)) = map✝
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Bornology M<VAR>inst✝ : SMul M α<VAR>s t : Set α<VAR>hs : Absorbent M s<VAR>ht : t.Finite<GOAL>Absorbs M s t
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Bornology M<VAR>inst✝ : SMul M α<VAR>s t : Set α<VAR>hs : Absorbent M s<VAR>ht : t.Finite<GOAL>Absorbs M s (⋃ x ∈ t, {x})
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p q : R[X]<VAR>h : (X - C a) * (p /ₘ (X - C a)) = p<GOAL>eval a p = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p q : R[X]<VAR>h : eval a p = 0<GOAL>(X - C a) * (p /ₘ (X - C a)) = p
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<VAR>ℱ : Filter ι<VAR>f : X → α<GOAL>Tendsto (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ (𝓝 ((UniformOnFun.ofFun 𝔖) f)) ↔ Tendsto ((⋃₀ 𝔖).restrict ∘ F) ℱ (𝓝 ((⋃₀ 𝔖).restrict f))
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<VAR>ℱ : Filter ι<VAR>f : X → α<GOAL>Tendsto (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ (𝓝 ((UniformOnFun.ofFun 𝔖) f)) ↔ Tendsto F ℱ (𝓝 f)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<VAR>ℱ : Filter ι<VAR>f : X → α<GOAL>(∀ i ∈ 𝔖, Tendsto ((⇑UniformFun.ofFun ∘ i.restrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ∘ ⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ (𝓝 ((⇑UniformFun.ofFun ∘ i.restrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ((UniformOnFun.ofFun 𝔖) f)))) ↔ ∀ i ∈ 𝔖, Tendsto (i.restrict ∘ F) ℱ (𝓝 (i.restrict f))
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<VAR>ℱ : Filter ι<VAR>f : X → α<VAR>K : Set X<VAR>hK : K ∈ 𝔖<GOAL>Tendsto ((⇑UniformFun.ofFun ∘ K.restrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ∘ ⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ (𝓝 ((⇑UniformFun.ofFun ∘ K.restrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ((UniformOnFun.ofFun 𝔖) f))) ↔ Tendsto (K.restrict ∘ F) ℱ (𝓝 (K.restrict f))
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<VAR>ℱ : Filter ι<VAR>f : X → α<VAR>K : Set X<VAR>hK : K ∈ 𝔖<VAR>this : CompactSpace ↑K<GOAL>Tendsto ((⇑UniformFun.ofFun ∘ K.restrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ∘ ⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ (𝓝 ((⇑UniformFun.ofFun ∘ K.restrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ((UniformOnFun.ofFun 𝔖) f))) ↔ Tendsto (K.restrict ∘ F) ℱ (𝓝 (K.restrict f))
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<VAR>ℱ : Filter ι<VAR>f : X → α<VAR>K : Set X<VAR>hK : K ∈ 𝔖<VAR>this : CompactSpace ↑K<GOAL>Tendsto ((⇑UniformFun.ofFun ∘ K.restrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ∘ ⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ (𝓝 ((⇑UniformFun.ofFun ∘ K.restrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ((UniformOnFun.ofFun 𝔖) f))) ↔ Tendsto (⇑UniformFun.ofFun ∘ K.restrict ∘ F) ℱ (𝓝 (UniformFun.ofFun (K.restrict f)))
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionRing α<VAR>p q : ℚ<VAR>n : ℕ<GOAL>↑↑n = ↑n
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>pb : PowerBasis K L<GOAL>pb.equivAdjoinSimple.symm pb.gen = AdjoinSimple.gen K pb.gen
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : SMulCommClass ℝ 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace E<VAR>f g : ↥(Lp E 1 μ)<GOAL>integralCLM (f - g) = integralCLM f - integralCLM g
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : CommRing B<VAR>inst✝¹⁵ : Field L<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : Algebra B L<VAR>inst✝¹² : Algebra A B<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : IsScalarTower A B L<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsFractionRing A K<VAR>inst✝⁵ : IsIntegralClosure B A L<VAR>inst✝⁴ : IsFractionRing B L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : IsDedekindDomain B<VAR>I J : FractionalIdeal B⁰ L<VAR>hI : I ≠ 0<VAR>hJ : J ≠ 0<GOAL>dual A K (dual A K I) = I
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>a x y : G<VAR>h : SemiconjBy a x y<VAR>n : ℕ<GOAL>SemiconjBy a (x ^ ↑n) (y ^ ↑n)
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>a x y : G<VAR>h : SemiconjBy a x y<VAR>n : ℕ<GOAL>SemiconjBy a (x ^ Int.negSucc n) (y ^ Int.negSucc n)
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>a x y : G<VAR>h : SemiconjBy a x y<VAR>n : ℕ<GOAL>SemiconjBy a (x ^ (n + 1)) (y ^ (n + 1))
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα : α.IsNonZero<GOAL>β (coroot α) = ↑(↑(chainBotCoeff (⇑α) β) - ↑(chainTopCoeff (⇑α) β))
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα : α.IsNonZero<GOAL>↑(↑(chainTopCoeff (⇑α) β + chainBotCoeff (⇑α) β) - 2 * ↑(chainTopCoeff (⇑α) β)) = ↑(↑(chainBotCoeff (⇑α) β) - ↑(chainTopCoeff (⇑α) β))
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>k n : ℕ<VAR>f : ContinuousMultilinearMap 𝕜 (fun i => G) G'<VAR>s : Finset (Fin n)<VAR>hk : s.card = k<VAR>z : G<GOAL>‖f.restr s hk z‖ ≤ ‖f‖ * ‖z‖ ^ (n - k)
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>k n : ℕ<VAR>f : ContinuousMultilinearMap 𝕜 (fun i => G) G'<VAR>s : Finset (Fin n)<VAR>hk : s.card = k<VAR>z : G<GOAL>0 ≤ ‖f‖ * ‖z‖ ^ (n - k)
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>y z : E<GOAL>‖I • y - 2 • z‖ * ‖I • y - 2 • z‖ = 2 * (‖I • y - z‖ * ‖I • y - z‖ + ‖z‖ * ‖z‖) - ‖I • y‖ * ‖I • y‖
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>y z : E<GOAL>‖I • y‖ * ‖I • y‖ + ‖I • y - 2 • z‖ * ‖I • y - 2 • z‖ = 2 * (‖I • y - z‖ * ‖I • y - z‖ + ‖z‖ * ‖z‖)
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>y z : E<VAR>h₀ : ‖I • y - z + z‖ * ‖I • y - z + z‖ + ‖I • y - z - z‖ * ‖I • y - z - z‖ = 2 * (‖I • y - z‖ * ‖I • y - z‖ + ‖z‖ * ‖z‖)<GOAL>‖I • y‖ * ‖I • y‖ + ‖I • y - 2 • z‖ * ‖I • y - 2 • z‖ = 2 * (‖I • y - z‖ * ‖I • y - z‖ + ‖z‖ * ‖z‖)
<VAR>f : ℕ → ℂ<VAR>n : ℕ<VAR>s : ℂ<GOAL>HasDerivAt (fun z => term f z n) (-term (logMul f) s n) s
<VAR>f : ℕ → ℂ<VAR>s : ℂ<GOAL>HasDerivAt (fun z => term f z 0) (-term (logMul f) s 0) s
<VAR>f : ℕ → ℂ<VAR>n : ℕ<VAR>s : ℂ<VAR>hn : n ≠ 0<GOAL>HasDerivAt (fun z => term f z n) (-term (logMul f) s n) s
<VAR>f : ℕ → ℂ<VAR>n : ℕ<VAR>s : ℂ<VAR>hn : n ≠ 0<GOAL>HasDerivAt (fun z => f n * ↑n ^ (-z)) (f n * (-log ↑n * ↑n ^ (-s))) s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>m : ℝ≥0∞ → ℝ≥0∞<VAR>c : ℝ≥0<VAR>hc : c ≠ 0<GOAL>mkMetric (c • m) = c • mkMetric m
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>f : LocallyConstant ↑C ℤ<VAR>hf : (LocallyConstant.comapₗ ℤ { toFun := CC'₁ C hsC ho, continuous_toFun := ⋯ }) f - (LocallyConstant.comapₗ ℤ { toFun := CC'₀ C ho, continuous_toFun := ⋯ }) f = 0<GOAL>∃ y, (πs C o) y = f
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>f : LocallyConstant ↑C ℤ<VAR>hf : ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₁ C hsC ho, continuous_toFun := ⋯ }) f) = ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₀ C ho, continuous_toFun := ⋯ }) f)<GOAL>∃ y, (πs C o) y = f
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>f : LocallyConstant ↑C ℤ<VAR>hf : ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₁ C hsC ho, continuous_toFun := ⋯ }) f) = ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₀ C ho, continuous_toFun := ⋯ }) f)<VAR>C₀C : ↑(C0 C ho) → ↑C := fun x => ⟨↑x, ⋯⟩<GOAL>∃ y, (πs C o) y = f
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>f : LocallyConstant ↑C ℤ<VAR>hf : ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₁ C hsC ho, continuous_toFun := ⋯ }) f) = ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₀ C ho, continuous_toFun := ⋯ }) f)<VAR>C₀C : ↑(C0 C ho) → ↑C := fun x => ⟨↑x, ⋯⟩<VAR>h₀ : Continuous C₀C<GOAL>∃ y, (πs C o) y = f
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>f : LocallyConstant ↑C ℤ<VAR>hf : ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₁ C hsC ho, continuous_toFun := ⋯ }) f) = ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₀ C ho, continuous_toFun := ⋯ }) f)<VAR>C₀C : ↑(C0 C ho) → ↑C := fun x => ⟨↑x, ⋯⟩<VAR>h₀ : Continuous C₀C<VAR>C₁C : ↑(π (C1 C ho) fun x => ord I x < o) → ↑C := fun x => ⟨SwapTrue o ↑x, ⋯⟩<GOAL>∃ y, (πs C o) y = f
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>f : LocallyConstant ↑C ℤ<VAR>hf : ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₁ C hsC ho, continuous_toFun := ⋯ }) f) = ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₀ C ho, continuous_toFun := ⋯ }) f)<VAR>C₀C : ↑(C0 C ho) → ↑C := fun x => ⟨↑x, ⋯⟩<VAR>h₀ : Continuous C₀C<VAR>C₁C : ↑(π (C1 C ho) fun x => ord I x < o) → ↑C := fun x => ⟨SwapTrue o ↑x, ⋯⟩<VAR>h₁ : Continuous C₁C<GOAL>∃ y, (πs C o) y = f
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>f : LocallyConstant ↑C ℤ<VAR>hf : ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₁ C hsC ho, continuous_toFun := ⋯ }) f) = ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₀ C ho, continuous_toFun := ⋯ }) f)<VAR>C₀C : ↑(C0 C ho) → ↑C := fun x => ⟨↑x, ⋯⟩<VAR>h₀ : Continuous C₀C<VAR>C₁C : ↑(π (C1 C ho) fun x => ord I x < o) → ↑C := fun x => ⟨SwapTrue o ↑x, ⋯⟩<VAR>h₁ : Continuous C₁C<GOAL>(π C fun x => ord I x < o) ⊆ C0 C ho ∪ π (C1 C ho) fun x => ord I x < o
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>f : LocallyConstant ↑C ℤ<VAR>hf : ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₁ C hsC ho, continuous_toFun := ⋯ }) f) = ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₀ C ho, continuous_toFun := ⋯ }) f)<VAR>C₀C : ↑(C0 C ho) → ↑C := fun x => ⟨↑x, ⋯⟩<VAR>h₀ : Continuous C₀C<VAR>C₁C : ↑(π (C1 C ho) fun x => ord I x < o) → ↑C := fun x => ⟨SwapTrue o ↑x, ⋯⟩<VAR>h₁ : Continuous C₁C<GOAL>∀ (x : I → Bool) (hx : x ∈ C0 C ho ∩ π (C1 C ho) fun x => ord I x < o), (LocallyConstant.comap { toFun := C₀C, continuous_toFun := h₀ } f) ⟨x, ⋯⟩ = (LocallyConstant.comap { toFun := C₁C, continuous_toFun := h₁ } f) ⟨x, ⋯⟩
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>f : LocallyConstant ↑C ℤ<VAR>hf : ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₁ C hsC ho, continuous_toFun := ⋯ }) f) = ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₀ C ho, continuous_toFun := ⋯ }) f)<VAR>C₀C : ↑(C0 C ho) → ↑C := fun x => ⟨↑x, ⋯⟩<VAR>h₀ : Continuous C₀C<VAR>C₁C : ↑(π (C1 C ho) fun x => ord I x < o) → ↑C := fun x => ⟨SwapTrue o ↑x, ⋯⟩<VAR>h₁ : Continuous C₁C<GOAL>(πs C o) (LocallyConstant.piecewise' ?refine_1 ⋯ ⋯ (LocallyConstant.comap { toFun := C₀C, continuous_toFun := h₀ } f) (LocallyConstant.comap { toFun := C₁C, continuous_toFun := h₁ } f) ?refine_2) = f
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁶ : NormedAddCommGroup E<VAR>inst✝¹⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹³ : TopologicalSpace M<VAR>inst✝¹² : ChartedSpace H M<VAR>inst✝¹¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹⁰ : NormedAddCommGroup E'<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁷ : TopologicalSpace M'<VAR>inst✝⁶ : ChartedSpace H' M'<VAR>inst✝⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>c : M'<VAR>x : M<GOAL>ContMDiffAt I I' n (fun x => c) x