ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type w'<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>P : Type u_1<VAR>inst✝¹ : L.Structure P<VAR>Q : Type u_2<VAR>inst✝ : L.Structure Q<VAR>toEmbedding✝¹ : M ↪ N<VAR>map_fun'✝¹ : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding✝¹.toFun (funMap f x) = funMap f (toEmbedding✝¹.toFun ∘ x)<VAR>map_rel'✝¹ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding✝¹.toFun ∘ x) ↔ RelMap r x<VAR>toEmbedding✝ : M ↪ N<VAR>map_fun'✝ : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding✝.toFun (funMap f x) = funMap f (toEmbedding✝.toFun ∘ x)<VAR>map_rel'✝ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding✝.toFun ∘ x) ↔ RelMap r x<VAR>h : ⇑{ toEmbedding := toEmbedding✝¹, map_fun' := map_fun'✝¹, map_rel' := map_rel'✝¹ } = ⇑{ toEmbedding := toEmbedding✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }<VAR>x : M<GOAL>toEmbedding✝¹ x = toEmbedding✝ x
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<GOAL>Disjoint Weight.ker (lieIdealSubalgebra K (↥H) (corootSpace ⇑α)).toSubmodule
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<GOAL>Weight.ker ⊓ (lieIdealSubalgebra K (↥H) (corootSpace ⇑α)).toSubmodule = ⊥
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>x : ↥H<VAR>x✝ : x ∈ Weight.ker ⊓ (lieIdealSubalgebra K (↥H) (corootSpace ⇑α)).toSubmodule<VAR>hαx : x ∈ ↑Weight.ker<VAR>hx : x ∈ ↑(lieIdealSubalgebra K (↥H) (corootSpace ⇑α)).toSubmodule<GOAL>x = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>x : ↥H<VAR>x✝ : x ∈ Weight.ker ⊓ (lieIdealSubalgebra K (↥H) (corootSpace ⇑α)).toSubmodule<VAR>hx : x ∈ ↑(lieIdealSubalgebra K (↥H) (corootSpace ⇑α)).toSubmodule<VAR>hαx : α x = 0<GOAL>x = 0
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁✝ : ι → Type v₁<VAR>β₂✝ : ι → Type v₂<VAR>inst✝⁵ : DecidableEq ι<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝⁴ : (i : ι) → Zero (β₁ i)<VAR>inst✝³ : (i : ι) → Zero (β₂ i)<VAR>inst✝² : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)<VAR>inst✝¹ : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)<VAR>inst✝ : CommMonoid γ<VAR>f : (i : ι) → β₁ i → β₂ i<VAR>hf : ∀ (i : ι), f i 0 = 0<VAR>g : Π₀ (i : ι), β₁ i<VAR>h : (i : ι) → β₂ i → γ<VAR>h0 : ∀ (i : ι), h i 0 = 1<GOAL>(mapRange f hf g).prod h = g.prod fun i b => h i (f i b)
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁✝ : ι → Type v₁<VAR>β₂✝ : ι → Type v₂<VAR>inst✝⁵ : DecidableEq ι<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝⁴ : (i : ι) → Zero (β₁ i)<VAR>inst✝³ : (i : ι) → Zero (β₂ i)<VAR>inst✝² : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)<VAR>inst✝¹ : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)<VAR>inst✝ : CommMonoid γ<VAR>f : (i : ι) → β₁ i → β₂ i<VAR>hf : ∀ (i : ι), f i 0 = 0<VAR>g : Π₀ (i : ι), β₁ i<VAR>h : (i : ι) → β₂ i → γ<VAR>h0 : ∀ (i : ι), h i 0 = 1<GOAL>(mk g.support fun i => f (↑i) (g ↑i)).prod h = g.prod fun i b => h i (f i b)
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁✝ : ι → Type v₁<VAR>β₂✝ : ι → Type v₂<VAR>inst✝⁵ : DecidableEq ι<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝⁴ : (i : ι) → Zero (β₁ i)<VAR>inst✝³ : (i : ι) → Zero (β₂ i)<VAR>inst✝² : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)<VAR>inst✝¹ : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)<VAR>inst✝ : CommMonoid γ<VAR>f : (i : ι) → β₁ i → β₂ i<VAR>hf : ∀ (i : ι), f i 0 = 0<VAR>g : Π₀ (i : ι), β₁ i<VAR>h : (i : ι) → β₂ i → γ<VAR>h0 : ∀ (i : ι), h i 0 = 1<GOAL>∀ x ∈ g.support, x ∉ (mk g.support fun i => f (↑i) (g ↑i)).support → h x ((mk g.support fun i => f (↑i) (g ↑i)) x) = 1
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁✝ : ι → Type v₁<VAR>β₂✝ : ι → Type v₂<VAR>inst✝⁵ : DecidableEq ι<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝⁴ : (i : ι) → Zero (β₁ i)<VAR>inst✝³ : (i : ι) → Zero (β₂ i)<VAR>inst✝² : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)<VAR>inst✝¹ : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)<VAR>inst✝ : CommMonoid γ<VAR>f : (i : ι) → β₁ i → β₂ i<VAR>hf : ∀ (i : ι), f i 0 = 0<VAR>g : Π₀ (i : ι), β₁ i<VAR>h : (i : ι) → β₂ i → γ<VAR>h0 : ∀ (i : ι), h i 0 = 1<GOAL>∏ x ∈ g.support, h x ((mk g.support fun i => f (↑i) (g ↑i)) x) = g.prod fun i b => h i (f i b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s✝ : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : β × γ → ℝ≥0∞<VAR>hf : Measurable f<VAR>s : Set β<VAR>t : Set γ<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<GOAL>∫⁻ (z : β × γ) in s ×ˢ t, f z ∂(κ ⊗ₖ η) a = ∫⁻ (x : β) in s, ∫⁻ (y : γ) in t, f (x, y) ∂η (a, x) ∂κ a
<VAR>α : Type u_1<VAR>inst✝ : CancelCommMonoid α<VAR>s : Submonoid α<VAR>a₁ b₁ : α<VAR>a₂ b₂ b : ↥s<VAR>c d : α<VAR>h : (fun a => mk a b) c = (fun a => mk a b) d<GOAL>c = d
<VAR>α : Type u_1<VAR>s t u : Set α<GOAL>val ⁻¹' t = val ⁻¹' u ↔ s ∩ t = s ∩ u
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>a b : α<VAR>n : ℕ<GOAL>a = b ↔ n + 1 = 0 ∨ a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Finite α<VAR>p q : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred q<VAR>e : { x // p x } ≃ { x // q x }<VAR>x : α<VAR>hx : ¬p x<GOAL>¬q (e.extendSubtype x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Finite α<VAR>p q : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred q<VAR>e : { x // p x } ≃ { x // q x }<VAR>x : α<VAR>hx : ¬p x<GOAL>e.extendSubtype x = ↑(e.toCompl ⟨x, hx⟩)
<VAR>a✝ b✝ c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>a b : ℕ<GOAL>a % b + a / b * b = a
<VAR>a✝ b✝ c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>a b : ℕ<GOAL>a % b + b * (a / b) = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t t₁ t₂ : Set α<VAR>hs : s₁ ⊆ s₂<VAR>hsμ : μ s₂ ≤ μ s₁<VAR>ht : t₁ ⊆ t₂<VAR>htμ : μ t₂ ≤ μ t₁<GOAL>μ (s₁ ∪ t₁) = μ (s₂ ∪ t₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t t₁ t₂ : Set α<VAR>hs : s₁ ⊆ s₂<VAR>hsμ : μ s₂ ≤ μ s₁<VAR>ht : t₁ ⊆ t₂<VAR>htμ : μ t₂ ≤ μ t₁<GOAL>μ (⋃ b, bif b then s₁ else t₁) = μ (⋃ b, bif b then s₂ else t₂)
<VAR>b o : Ordinal.{u_1}<VAR>hb : 1 < b<GOAL>o / b ^ log b o < b
<VAR>b o : Ordinal.{u_1}<VAR>hb : 1 < b<GOAL>o < b ^ succ (log b o)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>t : Set (ProjectiveSpectrum 𝒜)<GOAL>vanishingIdeal (closure t) = vanishingIdeal t
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>t : Set (ProjectiveSpectrum 𝒜)<VAR>this : (vanishingIdeal (zeroLocus 𝒜 ↑(vanishingIdeal t).toIdeal)).toIdeal = (vanishingIdeal t).toIdeal<GOAL>vanishingIdeal (closure t) = vanishingIdeal t
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>t : Set (ProjectiveSpectrum 𝒜)<VAR>this : (vanishingIdeal (zeroLocus 𝒜 ↑(vanishingIdeal t).toIdeal)).toIdeal = (vanishingIdeal t).toIdeal<GOAL>(vanishingIdeal (closure t)).toIdeal = (vanishingIdeal t).toIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>t : Set (ProjectiveSpectrum 𝒜)<VAR>this : (vanishingIdeal (closure t)).toIdeal = (vanishingIdeal t).toIdeal<GOAL>(vanishingIdeal (closure t)).toIdeal = (vanishingIdeal t).toIdeal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : TopologicalSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : SecondCountableTopologyEither α E<VAR>inst✝⁵ : CompactSpace α<VAR>inst✝⁴ : IsFiniteMeasure μ<VAR>𝕜 : Type u_5<VAR>inst✝³ : Fact (1 ≤ p)<VAR>β : Type u_6<VAR>inst✝² : μ.IsOpenPosMeasure<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<VAR>g : β → C(α, E)<VAR>f : C(α, E)<VAR>hg : Summable g<VAR>hg2 : HasSum (⇑(toLp p μ 𝕜) ∘ g) ((toLp p μ 𝕜) f)<GOAL>HasSum g f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : TopologicalSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : SecondCountableTopologyEither α E<VAR>inst✝⁵ : CompactSpace α<VAR>inst✝⁴ : IsFiniteMeasure μ<VAR>𝕜 : Type u_5<VAR>inst✝³ : Fact (1 ≤ p)<VAR>β : Type u_6<VAR>inst✝² : μ.IsOpenPosMeasure<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<VAR>g : β → C(α, E)<VAR>f : C(α, E)<VAR>hg : Summable g<VAR>hg2 : HasSum (⇑(toLp p μ 𝕜) ∘ g) ((toLp p μ 𝕜) f)<GOAL>f = ∑' (b : β), g b
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : StrictConcaveOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hfd : HasDerivAt f f' x<GOAL>slope f x y < f'
<VAR>J K : Type v<VAR>inst✝² : SmallCategory J<VAR>inst✝¹ : SmallCategory K<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>D : DiagramOfCocones F<VAR>Q : (j : J) → IsColimit (D.obj j)<VAR>c : Cocone (uncurry.obj F)<VAR>j : J<VAR>k k' : K<VAR>f : k ⟶ k'<GOAL>(F.obj j).map f ≫ c.ι.app (j, k') = c.ι.app (j, k) ≫ 𝟙 c.pt
<VAR>J K : Type v<VAR>inst✝² : SmallCategory J<VAR>inst✝¹ : SmallCategory K<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>D : DiagramOfCocones F<VAR>Q : (j : J) → IsColimit (D.obj j)<VAR>c : Cocone (uncurry.obj F)<VAR>j : J<VAR>k k' : K<VAR>f : k ⟶ k'<GOAL>(F.obj j).map f ≫ c.ι.app (j, k') = c.ι.app (j, k)
<VAR>J K : Type v<VAR>inst✝² : SmallCategory J<VAR>inst✝¹ : SmallCategory K<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>D : DiagramOfCocones F<VAR>Q : (j : J) → IsColimit (D.obj j)<VAR>c : Cocone (uncurry.obj F)<VAR>j : J<VAR>k k' : K<VAR>f : k ⟶ k'<GOAL>((F.map (𝟙 j)).app k ≫ (F.obj j).map f) ≫ c.ι.app (j, k') = c.ι.app (j, k)
<VAR>J K : Type v<VAR>inst✝² : SmallCategory J<VAR>inst✝¹ : SmallCategory K<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>D : DiagramOfCocones F<VAR>Q : (j : J) → IsColimit (D.obj j)<VAR>c : Cocone (uncurry.obj F)<VAR>j : J<VAR>k k' : K<VAR>f : k ⟶ k'<GOAL>(uncurry.obj F).map (𝟙 j, f) ≫ c.ι.app (j, k') = c.ι.app (j, k)
<VAR>J K : Type v<VAR>inst✝² : SmallCategory J<VAR>inst✝¹ : SmallCategory K<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>D : DiagramOfCocones F<VAR>Q : (j : J) → IsColimit (D.obj j)<VAR>c : Cocone (uncurry.obj F)<VAR>j j' : J<VAR>f : j ⟶ j'<VAR>k : K<GOAL>(D.obj j).ι.app k ≫ (D.map f).hom ≫ (Q j').desc { pt := c.pt, ι := { app := fun k => c.ι.app (j', k), naturality := ⋯ } } = (D.obj j).ι.app k ≫ (Q j).desc { pt := c.pt, ι := { app := fun k => c.ι.app (j, k), naturality := ⋯ } } ≫ 𝟙 c.pt
<VAR>J K : Type v<VAR>inst✝² : SmallCategory J<VAR>inst✝¹ : SmallCategory K<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>D : DiagramOfCocones F<VAR>Q : (j : J) → IsColimit (D.obj j)<VAR>c : Cocone (uncurry.obj F)<VAR>j j' : J<VAR>f : j ⟶ j'<VAR>k : K<GOAL>(F.map f).app k ≫ c.ι.app (j', k) = c.ι.app (j, k)
<VAR>J K : Type v<VAR>inst✝² : SmallCategory J<VAR>inst✝¹ : SmallCategory K<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>D : DiagramOfCocones F<VAR>Q : (j : J) → IsColimit (D.obj j)<VAR>c : Cocone (uncurry.obj F)<VAR>j j' : J<VAR>f : j ⟶ j'<VAR>k : K<VAR>this : (uncurry.obj F).map (f, 𝟙 k) ≫ c.ι.app (j', k) = c.ι.app (j, k) ≫ ((Functor.const (J × K)).obj c.pt).map (f, 𝟙 k)<GOAL>(F.map f).app k ≫ c.ι.app (j', k) = c.ι.app (j, k)
<VAR>J K : Type v<VAR>inst✝² : SmallCategory J<VAR>inst✝¹ : SmallCategory K<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>D : DiagramOfCocones F<VAR>Q : (j : J) → IsColimit (D.obj j)<VAR>c : Cocone (uncurry.obj F)<VAR>j j' : J<VAR>f : j ⟶ j'<VAR>k : K<VAR>this : ((F.map f).app k ≫ (F.obj j').map (𝟙 k)) ≫ c.ι.app (j', k) = c.ι.app (j, k) ≫ 𝟙 c.pt<GOAL>(F.map f).app k ≫ c.ι.app (j', k) = c.ι.app (j, k)
<VAR>J K : Type v<VAR>inst✝² : SmallCategory J<VAR>inst✝¹ : SmallCategory K<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>D : DiagramOfCocones F<VAR>Q : (j : J) → IsColimit (D.obj j)<VAR>c : Cocone (uncurry.obj F)<VAR>j j' : J<VAR>f : j ⟶ j'<VAR>k : K<VAR>this : (F.map f).app k ≫ c.ι.app (j', k) = c.ι.app (j, k)<GOAL>(F.map f).app k ≫ c.ι.app (j', k) = c.ι.app (j, k)
<VAR>p✝ n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁹ : CommRing A<VAR>inst✝⁸ : CommRing B<VAR>inst✝⁷ : Algebra A B<VAR>inst✝⁶ : IsCyclotomicExtension {n} A B<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : CommRing L<VAR>inst✝³ : IsDomain L<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : IsCyclotomicExtension {n} K L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>inst✝ : FiniteDimensional K L<VAR>p q : ℕ<VAR>x y : L<VAR>hx : IsPrimitiveRoot x p<VAR>hy : IsPrimitiveRoot y q<VAR>hirr : Irreducible (cyclotomic (p.lcm q) K)<GOAL>φ (p.lcm q) ≤ FiniteDimensional.finrank K L
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁹ : CommRing A<VAR>inst✝⁸ : CommRing B<VAR>inst✝⁷ : Algebra A B<VAR>inst✝⁶ : IsCyclotomicExtension {n} A B<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : CommRing L<VAR>inst✝³ : IsDomain L<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : IsCyclotomicExtension {n} K L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>inst✝ : FiniteDimensional K L<VAR>q : ℕ<VAR>x y : L<VAR>hy : IsPrimitiveRoot y q<VAR>hx : IsPrimitiveRoot x 0<VAR>hirr : Irreducible (cyclotomic (Nat.lcm 0 q) K)<GOAL>φ (Nat.lcm 0 q) ≤ FiniteDimensional.finrank K L
<VAR>p✝ n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁹ : CommRing A<VAR>inst✝⁸ : CommRing B<VAR>inst✝⁷ : Algebra A B<VAR>inst✝⁶ : IsCyclotomicExtension {n} A B<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : CommRing L<VAR>inst✝³ : IsDomain L<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : IsCyclotomicExtension {n} K L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>inst✝ : FiniteDimensional K L<VAR>p q : ℕ<VAR>x y : L<VAR>hx : IsPrimitiveRoot x p<VAR>hy : IsPrimitiveRoot y q<VAR>hirr : Irreducible (cyclotomic (p.lcm q) K)<VAR>hppos : p > 0<GOAL>φ (p.lcm q) ≤ FiniteDimensional.finrank K L
<VAR>p✝ n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁹ : CommRing A<VAR>inst✝⁸ : CommRing B<VAR>inst✝⁷ : Algebra A B<VAR>inst✝⁶ : IsCyclotomicExtension {n} A B<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : CommRing L<VAR>inst✝³ : IsDomain L<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : IsCyclotomicExtension {n} K L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>inst✝ : FiniteDimensional K L<VAR>p : ℕ<VAR>x y : L<VAR>hx : IsPrimitiveRoot x p<VAR>hppos : p > 0<VAR>hy : IsPrimitiveRoot y 0<VAR>hirr : Irreducible (cyclotomic (p.lcm 0) K)<GOAL>φ (p.lcm 0) ≤ FiniteDimensional.finrank K L
<VAR>p✝ n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁹ : CommRing A<VAR>inst✝⁸ : CommRing B<VAR>inst✝⁷ : Algebra A B<VAR>inst✝⁶ : IsCyclotomicExtension {n} A B<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : CommRing L<VAR>inst✝³ : IsDomain L<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : IsCyclotomicExtension {n} K L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>inst✝ : FiniteDimensional K L<VAR>p q : ℕ<VAR>x y : L<VAR>hx : IsPrimitiveRoot x p<VAR>hy : IsPrimitiveRoot y q<VAR>hirr : Irreducible (cyclotomic (p.lcm q) K)<VAR>hppos : p > 0<VAR>hqpos : q > 0<GOAL>φ (p.lcm q) ≤ FiniteDimensional.finrank K L
<VAR>p✝ n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁹ : CommRing A<VAR>inst✝⁸ : CommRing B<VAR>inst✝⁷ : Algebra A B<VAR>inst✝⁶ : IsCyclotomicExtension {n} A B<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : CommRing L<VAR>inst✝³ : IsDomain L<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : IsCyclotomicExtension {n} K L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>inst✝ : FiniteDimensional K L<VAR>p q : ℕ<VAR>x y : L<VAR>hx : IsPrimitiveRoot x p<VAR>hy : IsPrimitiveRoot y q<VAR>hirr : Irreducible (cyclotomic (p.lcm q) K)<VAR>hppos : p > 0<VAR>hqpos : q > 0<VAR>z : L := x ^ (p / p.factorizationLCMLeft q) * y ^ (q / p.factorizationLCMRight q)<VAR>k : ℕ+ := PNat.lcm ⟨p, hppos⟩ ⟨q, hqpos⟩<GOAL>φ (p.lcm q) ≤ FiniteDimensional.finrank K L
<VAR>p✝ n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁹ : CommRing A<VAR>inst✝⁸ : CommRing B<VAR>inst✝⁷ : Algebra A B<VAR>inst✝⁶ : IsCyclotomicExtension {n} A B<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : CommRing L<VAR>inst✝³ : IsDomain L<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : IsCyclotomicExtension {n} K L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>inst✝ : FiniteDimensional K L<VAR>p q : ℕ<VAR>x y : L<VAR>hx : IsPrimitiveRoot x p<VAR>hy : IsPrimitiveRoot y q<VAR>hirr : Irreducible (cyclotomic (p.lcm q) K)<VAR>hppos : p > 0<VAR>hqpos : q > 0<VAR>z : L := x ^ (p / p.factorizationLCMLeft q) * y ^ (q / p.factorizationLCMRight q)<VAR>k : ℕ+ := PNat.lcm ⟨p, hppos⟩ ⟨q, hqpos⟩<VAR>this : IsPrimitiveRoot z ↑k<GOAL>φ (p.lcm q) ≤ FiniteDimensional.finrank K L
<VAR>p✝ n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁹ : CommRing A<VAR>inst✝⁸ : CommRing B<VAR>inst✝⁷ : Algebra A B<VAR>inst✝⁶ : IsCyclotomicExtension {n} A B<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : CommRing L<VAR>inst✝³ : IsDomain L<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : IsCyclotomicExtension {n} K L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>inst✝ : FiniteDimensional K L<VAR>p q : ℕ<VAR>x y : L<VAR>hx : IsPrimitiveRoot x p<VAR>hy : IsPrimitiveRoot y q<VAR>hirr : Irreducible (cyclotomic (p.lcm q) K)<VAR>hppos : p > 0<VAR>hqpos : q > 0<VAR>z : L := x ^ (p / p.factorizationLCMLeft q) * y ^ (q / p.factorizationLCMRight q)<VAR>k : ℕ+ := PNat.lcm ⟨p, hppos⟩ ⟨q, hqpos⟩<VAR>this✝ : IsPrimitiveRoot z ↑k<VAR>this : IsCyclotomicExtension {k} K ↥(adjoin K {z})<GOAL>φ (p.lcm q) ≤ FiniteDimensional.finrank K L
<VAR>p✝ n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁹ : CommRing A<VAR>inst✝⁸ : CommRing B<VAR>inst✝⁷ : Algebra A B<VAR>inst✝⁶ : IsCyclotomicExtension {n} A B<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : CommRing L<VAR>inst✝³ : IsDomain L<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : IsCyclotomicExtension {n} K L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>inst✝ : FiniteDimensional K L<VAR>p q : ℕ<VAR>x y : L<VAR>hx : IsPrimitiveRoot x p<VAR>hy : IsPrimitiveRoot y q<VAR>hirr : Irreducible (cyclotomic (p.lcm q) K)<VAR>hppos : p > 0<VAR>hqpos : q > 0<VAR>z : L := x ^ (p / p.factorizationLCMLeft q) * y ^ (q / p.factorizationLCMRight q)<VAR>k : ℕ+ := PNat.lcm ⟨p, hppos⟩ ⟨q, hqpos⟩<VAR>this✝ : IsPrimitiveRoot z ↑k<VAR>this : IsCyclotomicExtension {k} K ↥(adjoin K {z})<GOAL>φ (p.lcm q) = FiniteDimensional.finrank K ↥(Subalgebra.toSubmodule (adjoin K {z}))
<VAR>p✝ n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁹ : CommRing A<VAR>inst✝⁸ : CommRing B<VAR>inst✝⁷ : Algebra A B<VAR>inst✝⁶ : IsCyclotomicExtension {n} A B<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : CommRing L<VAR>inst✝³ : IsDomain L<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : IsCyclotomicExtension {n} K L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>inst✝ : FiniteDimensional K L<VAR>p q : ℕ<VAR>x y : L<VAR>hx : IsPrimitiveRoot x p<VAR>hy : IsPrimitiveRoot y q<VAR>hppos : p > 0<VAR>hqpos : q > 0<VAR>z : L := x ^ (p / p.factorizationLCMLeft q) * y ^ (q / p.factorizationLCMRight q)<VAR>k : ℕ+ := PNat.lcm ⟨p, hppos⟩ ⟨q, hqpos⟩<VAR>hirr : Irreducible (cyclotomic (↑k) K)<VAR>this✝ : IsPrimitiveRoot z ↑k<VAR>this : IsCyclotomicExtension {k} K ↥(adjoin K {z})<GOAL>φ (p.lcm q) = FiniteDimensional.finrank K ↥(Subalgebra.toSubmodule (adjoin K {z}))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>mδ : MeasurableSpace δ<VAR>f : β → γ<VAR>g : γ → α<VAR>κ : Kernel α β<VAR>inst✝ : IsSFiniteKernel κ<VAR>hf : Measurable f<VAR>a : α<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>((Kernel.sum fun n => (κ.seq n).map f hf) a) s = ((κ.map f hf) a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>mδ : MeasurableSpace δ<VAR>f : β → γ<VAR>g : γ → α<VAR>κ : Kernel α β<VAR>inst✝ : IsSFiniteKernel κ<VAR>hf : Measurable f<VAR>a : α<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>∑' (i : ℕ), (((κ.seq i).map f hf) a) s = ∑' (i : ℕ), ((κ.seq i) a) (f ⁻¹' s)
<VAR>α : Type u_1<VAR>inst✝ : EMetricSpace α<VAR>cs : CompleteSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>x : α<VAR>hx : edist x (f x) ≠ ⊤<GOAL>edist x (efixedPoint f hf x hx) ≤ edist x (f x) / (1 - ↑K)
<VAR>α : Type u_1<VAR>inst✝ : EMetricSpace α<VAR>cs : CompleteSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>x : α<VAR>hx : edist x (f x) ≠ ⊤<GOAL>edist x (f x) = edist x (f x) * ↑K ^ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : CommSemigroup G<VAR>a b c : G<GOAL>a * (b * c) = b * (c * a)
<VAR>u v : Level<VAR>n : ℕ<VAR>pn : NormNum.IsNat n 0<GOAL>Multiset.range n = 0
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>s : Set (α × α)<GOAL>idRel ⊆ s ↔ ∀ (a : α), (a, a) ∈ s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁷ : MeasurableSpace X<VAR>μ : Measure X<VAR>𝕜 : Type u_5<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : NormedSpace ℝ E<VAR>L : E ≃L[𝕜] F<VAR>φ : X → E<GOAL>∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁷ : MeasurableSpace X<VAR>μ : Measure X<VAR>𝕜 : Type u_5<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : NormedSpace ℝ E<VAR>L : E ≃L[𝕜] F<VAR>φ : X → E<VAR>this : CompleteSpace E ↔ CompleteSpace F<GOAL>∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)