ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>M : Mon_ C<GOAL>(tensor_μ C (𝟙_ C, M.X) (𝟙_ C, M.X) ≫ (λ_ (𝟙_ C)).hom ▷ (M.X ⊗ M.X) ≫ 𝟙_ C ◁ M.mul) ≫ (λ_ M.X).hom = ((λ_ M.X).hom ⊗ (λ_ M.X).hom) ≫ 𝟙 (M.X ⊗ M.X) ≫ M.mul
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>M : Mon_ C<GOAL>tensor_μ C (𝟙_ C, M.X) (𝟙_ C, M.X) ≫ (λ_ (𝟙_ C)).hom ▷ (M.X ⊗ M.X) ≫ (λ_ (M.X ⊗ M.X)).hom ≫ M.mul = ((λ_ M.X).hom ⊗ (λ_ M.X).hom) ≫ 𝟙 (M.X ⊗ M.X) ≫ M.mul
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>M : Mon_ C<GOAL>((λ_ M.X).hom ⊗ (λ_ M.X).hom) ≫ M.mul = ((λ_ M.X).hom ⊗ (λ_ M.X).hom) ≫ 𝟙 (M.X ⊗ M.X) ≫ M.mul
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>inst✝² : Semiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>I : Ideal R<VAR>f : F<GOAL>map f I = ⊥ ↔ I ≤ RingHom.ker f
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>r : R<VAR>f : R[X]<VAR>x : R<GOAL>(taylor r) (C x) = C x
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁✝ l₂✝ : List α<VAR>inst✝ : Inhabited α<VAR>l₁ l₂ : List α<GOAL>l₁.length ≤ (l₁ ++ l₂).length
<VAR>R : Type u<VAR>L : Type v<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>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>I₁ I₂ : LieIdeal R L<GOAL>map I₁.incl (comap I₁.incl I₂) = I₁ ⊓ I₂
<VAR>R : Type u<VAR>L : Type v<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>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>I₁ I₂ : LieIdeal R L<GOAL>map I₁.incl (comap I₁.incl I₂) = I₁.incl.idealRange ⊓ I₂
<VAR>R : Type u<VAR>L : Type v<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>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>I₁ I₂ : LieIdeal R L<GOAL>I₁.incl.IsIdealMorphism
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<GOAL>↑(f.extend I).symm ⁻¹' (s ∩ t) ∩ range ↑I = ↑(f.extend I).symm ⁻¹' s ∩ range ↑I ∩ ↑(f.extend I).symm ⁻¹' t
<VAR>n : ℕ<GOAL>eulerMascheroniConstant < eulerMascheroniSeq' n
<VAR>n : ℕ<GOAL>eulerMascheroniConstant ≤ eulerMascheroniSeq' n.succ
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype o<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Fintype m<VAR>e₁ e₂ : m ≃ n<VAR>A : Matrix m m R<GOAL>((reindex e₁ e₂) A).rank = A.rank
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a✝ b c d : G<VAR>n✝ : ℤ<VAR>a : G<VAR>m n : ℤ<GOAL>a ^ m * a ^ n = a ^ n * a ^ m
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a : α<VAR>x✝ : ℤ<GOAL>x✝ ∈ Int.cast ⁻¹' Iic a ↔ x✝ ∈ Iic ⌊a⌋
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι✝ → Type u_5<VAR>s✝ s₁ s₂ : Finset ι✝<VAR>i : ι✝<VAR>a : α<VAR>f✝ g : ι✝ → α<VAR>ι : Type u_6<VAR>s : Finset ι<VAR>f : ι → ℕ<VAR>n : ℕ<VAR>hf : ∀ i ∈ s, n ∣ f i<GOAL>(∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι✝ → Type u_5<VAR>s✝ s₁ s₂ : Finset ι✝<VAR>i : ι✝<VAR>a : α<VAR>f✝ g : ι✝ → α<VAR>ι : Type u_6<VAR>s : Finset ι<VAR>f : ι → ℕ<VAR>hf : ∀ i ∈ s, 0 ∣ f i<GOAL>(∑ i ∈ s, f i) / 0 = ∑ i ∈ s, f i / 0
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι✝ → Type u_5<VAR>s✝ s₁ s₂ : Finset ι✝<VAR>i : ι✝<VAR>a : α<VAR>f✝ g : ι✝ → α<VAR>ι : Type u_6<VAR>s : Finset ι<VAR>f : ι → ℕ<VAR>n : ℕ<VAR>hf : ∀ i ∈ s, n ∣ f i<VAR>hn : n > 0<GOAL>(∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι✝ → Type u_5<VAR>s✝ s₁ s₂ : Finset ι✝<VAR>i : ι✝<VAR>a : α<VAR>f✝ g : ι✝ → α<VAR>ι : Type u_6<VAR>s : Finset ι<VAR>f : ι → ℕ<VAR>n : ℕ<VAR>hf : ∀ i ∈ s, n ∣ f i<VAR>hn : n > 0<GOAL>∑ i ∈ s, f i = ∑ i ∈ s, f i / n * n
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι✝ → Type u_5<VAR>s✝¹ s₁ s₂ : Finset ι✝<VAR>i : ι✝<VAR>a : α<VAR>f✝ g : ι✝ → α<VAR>ι : Type u_6<VAR>s✝ : Finset ι<VAR>f : ι → ℕ<VAR>n : ℕ<VAR>hf : ∀ i ∈ s✝, n ∣ f i<VAR>hn : n > 0<VAR>s : ι<VAR>hs : s ∈ s✝<GOAL>f s = f s / n * n
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : BorelSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ : ι → α → ℝ<VAR>a : E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : MetrizableSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : μ.IsOpenPosMeasure<VAR>hs : IsCompact s<VAR>c : α → ℝ<VAR>hc : ContinuousOn c s<VAR>h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀<VAR>hnc : ∀ x ∈ s, 0 ≤ c x<VAR>hnc₀ : 0 < c x₀<VAR>h₀ : x₀ ∈ closure (interior s)<VAR>hmg : IntegrableOn g s μ<VAR>hcg : ContinuousWithinAt g s x₀<GOAL>Tendsto (fun n => (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ • ∫ (x : α) in s, c x ^ n • g x ∂μ) atTop (𝓝 (g x₀))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : BorelSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ : ι → α → ℝ<VAR>a : E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : MetrizableSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : μ.IsOpenPosMeasure<VAR>hs : IsCompact s<VAR>c : α → ℝ<VAR>hc : ContinuousOn c s<VAR>h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀<VAR>hnc : ∀ x ∈ s, 0 ≤ c x<VAR>hnc₀ : 0 < c x₀<VAR>h₀ : x₀ ∈ closure (interior s)<VAR>hmg : IntegrableOn g s μ<VAR>hcg : ContinuousWithinAt g s x₀<VAR>this : x₀ ∈ s<GOAL>Tendsto (fun n => (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ • ∫ (x : α) in s, c x ^ n • g x ∂μ) atTop (𝓝 (g x₀))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : BorelSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ : ι → α → ℝ<VAR>a : E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : MetrizableSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : μ.IsOpenPosMeasure<VAR>hs : IsCompact s<VAR>c : α → ℝ<VAR>hc : ContinuousOn c s<VAR>h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀<VAR>hnc : ∀ x ∈ s, 0 ≤ c x<VAR>hnc₀ : 0 < c x₀<VAR>h₀ : x₀ ∈ closure (interior s)<VAR>hmg : IntegrableOn g s μ<VAR>hcg : ContinuousWithinAt g s x₀<VAR>this : x₀ ∈ s<GOAL>∀ (u : Set α), IsOpen u → x₀ ∈ u → 0 < μ (u ∩ s)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : BorelSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ : ι → α → ℝ<VAR>a : E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : MetrizableSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : μ.IsOpenPosMeasure<VAR>hs : IsCompact s<VAR>c : α → ℝ<VAR>hc : ContinuousOn c s<VAR>h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀<VAR>hnc : ∀ x ∈ s, 0 ≤ c x<VAR>hnc₀ : 0 < c x₀<VAR>h₀ : x₀ ∈ closure (interior s)<VAR>hmg : IntegrableOn g s μ<VAR>hcg : ContinuousWithinAt g s x₀<VAR>this : x₀ ∈ s<VAR>u : Set α<VAR>u_open : IsOpen u<VAR>x₀_u : x₀ ∈ u<GOAL>0 < μ (u ∩ s)
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝ : IsDedekindDomain S<VAR>hp0 : map f p ≠ ⊥<VAR>hP : P.IsPrime<VAR>hP0 : P ≠ ⊥<GOAL>ramificationIdx f p P = Multiset.count P (normalizedFactors (map f p))
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝ : IsDedekindDomain S<VAR>hp0 : map f p ≠ ⊥<VAR>hP : P.IsPrime<VAR>hP0 : P ≠ ⊥<VAR>hPirr : Irreducible P<GOAL>ramificationIdx f p P = Multiset.count P (normalizedFactors (map f p))
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝ : IsDedekindDomain S<VAR>hp0 : map f p ≠ ⊥<VAR>hP : P.IsPrime<VAR>hP0 : P ≠ ⊥<VAR>hPirr : Irreducible P<GOAL>¬Multiset.count P (normalizedFactors (map f p)) + 1 ≤ Multiset.count P (normalizedFactors (map f p))
<VAR>X : Type u_1<VAR>x : X<GOAL>(toFreeAbelianGroup.comp (singleAddHom x)) 1 = ((smulAddHom ℤ (FreeAbelianGroup X)).flip (of x)) 1
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z✝ z : K<GOAL>‖z‖ * ‖z‖ = normSq z
<VAR>Ω : Type u_1<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁴ : SMul R ℝ≥0<VAR>inst✝³ : SMul R ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝ : TopologicalSpace Ω<VAR>c : ℝ≥0<VAR>μ : FiniteMeasure Ω<VAR>f : Ω →ᵇ ℝ≥0<GOAL>(c • μ).testAgainstNN f = c • μ.testAgainstNN f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x : F<VAR>r : ℝ<VAR>hx : x ≠ 0<VAR>hr : r < 0<GOAL>⟪x, r • x⟫_ℝ / (‖x‖ * ‖r • x‖) = -1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x : F<VAR>r : ℝ<VAR>hx : x ≠ 0<VAR>hr : r < 0<GOAL>r * (‖x‖ * ‖x‖) ≠ 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedHeytingAlgebra α<VAR>a✝ b✝ c✝ d✝ a b c d : α<GOAL>d ≤ a ⊔ b ⇨ c ↔ d ≤ (a ⇨ c) ⊓ (b ⇨ c)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedHeytingAlgebra α<VAR>a✝ b✝ c✝ d✝ a b c d : α<GOAL>a ≤ d ⇨ c ∧ b ≤ d ⇨ c ↔ d ≤ a ⇨ c ∧ d ≤ b ⇨ c
<VAR>n m : ℕ<VAR>i j : Fin n<GOAL>i.rev ≤ j ↔ j.rev ≤ i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>c : α → Bool<VAR>f g : α →. σ<VAR>hc : Computable c<VAR>hf : Partrec f<VAR>hg : Partrec g<VAR>cf : Code<VAR>ef : cf.eval = fun n => (↑(decode n)).bind fun a => Part.map encode (f a)<VAR>cg : Code<VAR>eg : cg.eval = fun n => (↑(decode n)).bind fun a => Part.map encode (g a)<VAR>a : α<GOAL>(((bif c a then cf else cg).eval (encode a)).bind fun b => ↑(decode (a, b).2)) = bif c a then f a else g a
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>x : ↥U<GOAL>hU.fromSpec.val.base (hU.primeIdealOf x) = ↑x
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>x : ↥U<GOAL>(Spec.map (X.presheaf.map (eqToHom ⋯).op) ≫ (↑U).isoSpec.inv ≫ U.ι).val.base (((↑U).isoSpec.hom ≫ Spec.map (X.presheaf.map (eqToHom ⋯).op)).val.base x) = ↑x
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>x : ↥U<GOAL>(((↑U).isoSpec.hom ≫ Spec.map (X.presheaf.map (eqToHom ⋯).op)) ≫ Spec.map (X.presheaf.map (eqToHom ⋯).op) ≫ (↑U).isoSpec.inv ≫ U.ι).val.base x = ↑x
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>x : ↥U<GOAL>U.ι.val.base x = ↑x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>N' : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : AddCommGroup N'<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R N'<VAR>f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N<VAR>m : M<GOAL>(((foldl 0 (LinearMap.mk₂ R (fun m f i => (f (i + 1)).curryLeft m) ⋯ ⋯ ⋯ ⋯) ⋯) f) ((ι R) m) 0) 0 = (f 1) ![m]
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>N' : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : AddCommGroup N'<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R N'<VAR>f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N<VAR>m : M<GOAL>(f (0 + 1)) (Matrix.vecCons m 0) = (f 1) ![m]
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>N' : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : AddCommGroup N'<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R N'<VAR>f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N<VAR>m : M<GOAL>Matrix.vecCons m 0 = ![m]
<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<VAR>n : ℕ<VAR>hn : n ≤ chainLength α β<VAR>hα : ¬α.IsZero<GOAL>rootSpace H (-(n • ⇑α) + ⇑(chainTop (⇑α) β)) ≠ ⊥
<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<VAR>n : ℕ<VAR>hn : n ≤ chainLength α β<VAR>hα : ¬α.IsZero<VAR>x : L<VAR>hx : x ∈ weightSpace L ⇑(chainTop (⇑α) β)<VAR>x_ne0 : x ≠ 0<GOAL>rootSpace H (-(n • ⇑α) + ⇑(chainTop (⇑α) β)) ≠ ⊥
<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<VAR>n : ℕ<VAR>hn : n ≤ chainLength α β<VAR>hα : ¬α.IsZero<VAR>x : L<VAR>hx : x ∈ weightSpace L ⇑(chainTop (⇑α) β)<VAR>x_ne0 : x ≠ 0<VAR>h e f : L<VAR>isSl2 : IsSl2Triple h e f<VAR>he : e ∈ rootSpace H ⇑α<VAR>hf : f ∈ rootSpace H (-⇑α)<GOAL>rootSpace H (-(n • ⇑α) + ⇑(chainTop (⇑α) β)) ≠ ⊥
<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<VAR>n : ℕ<VAR>hn : n ≤ chainLength α β<VAR>hα : ¬α.IsZero<VAR>x : L<VAR>hx : x ∈ weightSpace L ⇑(chainTop (⇑α) β)<VAR>x_ne0 : x ≠ 0<VAR>e f : L<VAR>he : e ∈ rootSpace H ⇑α<VAR>hf : f ∈ rootSpace H (-⇑α)<VAR>isSl2 : IsSl2Triple (↑(coroot α)) e f<GOAL>rootSpace H (-(n • ⇑α) + ⇑(chainTop (⇑α) β)) ≠ ⊥
<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<VAR>n : ℕ<VAR>hn : n ≤ chainLength α β<VAR>hα : ¬α.IsZero<VAR>x : L<VAR>hx : x ∈ weightSpace L ⇑(chainTop (⇑α) β)<VAR>x_ne0 : x ≠ 0<VAR>e f : L<VAR>he : e ∈ rootSpace H ⇑α<VAR>hf : f ∈ rootSpace H (-⇑α)<VAR>isSl2 : IsSl2Triple (↑(coroot α)) e f<VAR>prim : isSl2.HasPrimitiveVectorWith x ↑(chainLength α β)<GOAL>rootSpace H (-(n • ⇑α) + ⇑(chainTop (⇑α) β)) ≠ ⊥
<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<VAR>n : ℕ<VAR>hn : n ≤ chainLength α β<VAR>hα : ¬α.IsZero<VAR>x : L<VAR>hx : x ∈ weightSpace L ⇑(chainTop (⇑α) β)<VAR>x_ne0 : x ≠ 0<VAR>e f : L<VAR>he : e ∈ rootSpace H ⇑α<VAR>hf : f ∈ rootSpace H (-⇑α)<VAR>isSl2 : IsSl2Triple (↑(coroot α)) e f<VAR>prim : isSl2.HasPrimitiveVectorWith x ↑(chainLength α β)<GOAL>∃ x, ∃ (_ : x ∈ rootSpace H (n • -⇑α + ⇑(chainTop (⇑α) β))), ¬x = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : _root_.RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>inst✝² : NormedSpace ℝ E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f g : G → E<VAR>f' g' : G →L[ℝ] E<VAR>s : Set G<VAR>x : G<VAR>n : ℕ∞<VAR>hf : DifferentiableWithinAt ℝ f s x<VAR>hg : DifferentiableWithinAt ℝ g s x<VAR>hne : f x ≠ g x<GOAL>DifferentiableWithinAt ℝ (fun y => ‖f y - g y‖) s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>s : Finset α<VAR>a : α<VAR>inst✝ : LinearOrder β<VAR>c : β<GOAL>c ≥ fold min b f s ↔ b ≤ c ∨ ∃ x ∈ s, f x ≤ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>s : Finset α<VAR>a : α<VAR>inst✝ : LinearOrder β<VAR>c : β<GOAL>∀ {x y z : β}, x ≥ min y z ↔ x ≥ y ∨ x ≥ z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>s : Finset α<VAR>a : α<VAR>inst✝ : LinearOrder β<VAR>c x y z : β<GOAL>min y z ≤ x ↔ x ≥ y ∨ x ≥ z
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>S : Set (Set X)<VAR>hc : S.Countable<VAR>hcomp : ∀ (s : ↑S), IsSigmaCompact ↑s<GOAL>IsSigmaCompact (⋃₀ S)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>S : Set (Set X)<VAR>hc : S.Countable<VAR>hcomp : ∀ (s : ↑S), IsSigmaCompact ↑s<VAR>this : Countable ↑S<GOAL>IsSigmaCompact (⋃₀ S)
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>s t : Set A<GOAL>Subalgebra.toSubmodule (adjoin R (s ∪ t)) = Subalgebra.toSubmodule (adjoin R s) * Subalgebra.toSubmodule (adjoin R t)
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>s t : Set A<GOAL>span R ↑(Submonoid.closure (s ∪ t)) = span R (↑(Submonoid.closure s) * ↑(Submonoid.closure t))
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>s t : Set A<VAR>z : A<GOAL>z ∈ ↑(Submonoid.closure (s ∪ t)) ↔ z ∈ ↑(Submonoid.closure s) * ↑(Submonoid.closure t)
<GOAL>∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S] [inst_4 : Algebra R T], (algebraMap R T).FinitePresentation → Algebra.TensorProduct.includeLeftRingHom.FinitePresentation
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>s : Set E<VAR>hs : IsOpen s<GOAL>∃ f, support f = s ∧ ContDiff ℝ ⊤ f ∧ range f ⊆ Icc 0 1
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>hs : IsOpen ∅<GOAL>∃ f, support f = ∅ ∧ ContDiff ℝ ⊤ f ∧ range f ⊆ Icc 0 1
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>s : Set E<VAR>hs : IsOpen s<VAR>h's : s.Nonempty<GOAL>∃ f, support f = s ∧ ContDiff ℝ ⊤ f ∧ range f ⊆ Icc 0 1
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>s : Set E<VAR>hs : IsOpen s<VAR>h's : s.Nonempty<VAR>ι : Type u_1 := { f // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ⊤ f ∧ range f ⊆ Icc 0 1 }<GOAL>∃ f, support f = s ∧ ContDiff ℝ ⊤ f ∧ range f ⊆ Icc 0 1
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>s : Set E<VAR>hs : IsOpen s<VAR>h's : s.Nonempty<VAR>ι : Type u_1 := { f // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ⊤ f ∧ range f ⊆ Icc 0 1 }<VAR>T : Set ι<VAR>T_count : T.Countable<VAR>hT : ⋃ f ∈ T, support ↑f = s<GOAL>∃ f, support f = s ∧ ContDiff ℝ ⊤ f ∧ range f ⊆ Icc 0 1
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>s : Set E<VAR>hs : IsOpen s<VAR>h's : s.Nonempty<VAR>ι : Type u_1 := { f // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ⊤ f ∧ range f ⊆ Icc 0 1 }<VAR>T : Set ι<VAR>T_count : T.Countable<VAR>hT : ⋃ f ∈ T, support ↑f = s<VAR>g0 : ℕ → ι<VAR>hg : T = range g0<VAR>g : ℕ → E → ℝ := fun n => ↑(g0 n)<GOAL>∃ f, support f = s ∧ ContDiff ℝ ⊤ f ∧ range f ⊆ Icc 0 1
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>s : Set E<VAR>hs : IsOpen s<VAR>h's : s.Nonempty<VAR>ι : Type u_1 := { f // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ⊤ f ∧ range f ⊆ Icc 0 1 }<VAR>T : Set ι<VAR>T_count : T.Countable<VAR>hT : ⋃ f ∈ T, support ↑f = s<VAR>g0 : ℕ → ι<VAR>hg : T = range g0<VAR>g : ℕ → E → ℝ := fun n => ↑(g0 n)<VAR>g_s : ∀ (n : ℕ), support (g n) ⊆ s<GOAL>∃ f, support f = s ∧ ContDiff ℝ ⊤ f ∧ range f ⊆ Icc 0 1
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>s : Set E<VAR>hs : IsOpen s<VAR>h's : s.Nonempty<VAR>ι : Type u_1 := { f // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ⊤ f ∧ range f ⊆ Icc 0 1 }<VAR>T : Set ι<VAR>T_count : T.Countable<VAR>hT : ⋃ f ∈ T, support ↑f = s<VAR>g0 : ℕ → ι<VAR>hg : T = range g0<VAR>g : ℕ → E → ℝ := fun n => ↑(g0 n)<VAR>g_s : ∀ (n : ℕ), support (g n) ⊆ s<VAR>s_g : ∀ x ∈ s, ∃ n, x ∈ support (g n)<GOAL>∃ f, support f = s ∧ ContDiff ℝ ⊤ f ∧ range f ⊆ Icc 0 1
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>s : Set E<VAR>hs : IsOpen s<VAR>h's : s.Nonempty<VAR>ι : Type u_1 := { f // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ⊤ f ∧ range f ⊆ Icc 0 1 }<VAR>T : Set ι<VAR>T_count : T.Countable<VAR>hT : ⋃ f ∈ T, support ↑f = s<VAR>g0 : ℕ → ι<VAR>hg : T = range g0<VAR>g : ℕ → E → ℝ := fun n => ↑(g0 n)<VAR>g_s : ∀ (n : ℕ), support (g n) ⊆ s<VAR>s_g : ∀ x ∈ s, ∃ n, x ∈ support (g n)<VAR>g_smooth : ∀ (n : ℕ), ContDiff ℝ ⊤ (g n)<GOAL>∃ f, support f = s ∧ ContDiff ℝ ⊤ f ∧ range f ⊆ Icc 0 1
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>s : Set E<VAR>hs : IsOpen s<VAR>h's : s.Nonempty<VAR>ι : Type u_1 := { f // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ⊤ f ∧ range f ⊆ Icc 0 1 }<VAR>T : Set ι<VAR>T_count : T.Countable<VAR>hT : ⋃ f ∈ T, support ↑f = s<VAR>g0 : ℕ → ι<VAR>hg : T = range g0<VAR>g : ℕ → E → ℝ := fun n => ↑(g0 n)<VAR>g_s : ∀ (n : ℕ), support (g n) ⊆ s<VAR>s_g : ∀ x ∈ s, ∃ n, x ∈ support (g n)<VAR>g_smooth : ∀ (n : ℕ), ContDiff ℝ ⊤ (g n)<VAR>g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)<GOAL>∃ f, support f = s ∧ ContDiff ℝ ⊤ f ∧ range f ⊆ Icc 0 1