ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝²⁵ : CommRing R<VAR>inst✝²⁴ : CommRing S<VAR>inst✝²³ : Algebra R S<VAR>P : Generators R S<VAR>R' : Type ?u.595057<VAR>S' : Type ?u.595060<VAR>inst✝²² : CommRing R'<VAR>inst✝²¹ : CommRing S'<VAR>inst✝²⁰ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝¹⁹ : Algebra R R'<VAR>inst✝¹⁸ : Algebra S S'<VAR>inst✝¹⁷ : Algebra R S'<VAR>inst✝¹⁶ : IsScalarTower R R' S'<VAR>inst✝¹⁵ : IsScalarTower R S S'<VAR>R'' : Type ?u.597491<VAR>S'' : Type ?u.597494<VAR>inst✝¹⁴ : CommRing R''<VAR>inst✝¹³ : CommRing S''<VAR>inst✝¹² : Algebra R'' S''<VAR>P'' : Generators R'' S''<VAR>inst✝¹¹ : Algebra R R''<VAR>inst✝¹⁰ : Algebra S S''<VAR>inst✝⁹ : Algebra R S''<VAR>inst✝⁸ : IsScalarTower R R'' S''<VAR>inst✝⁷ : IsScalarTower R S S''<VAR>inst✝⁶ : Algebra R' R''<VAR>inst✝⁵ : Algebra S' S''<VAR>inst✝⁴ : Algebra R' S''<VAR>inst✝³ : IsScalarTower R' R'' S''<VAR>inst✝² : IsScalarTower R' S' S''<VAR>inst✝¹ : IsScalarTower R R' R''<VAR>inst✝ : IsScalarTower S S' S''<VAR>p : P.Ring<VAR>hp : p ∈ P.ker<VAR>x : ↥P.ker<GOAL>p * ↑x ∈ P.ker * P.ker
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>a✝ b✝ c a b : G<GOAL>a * b * b⁻¹ = a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>a b c : α<VAR>inst✝ : DecidableEq α<VAR>h : a < b<GOAL>insert a (Ioo a b) = Ico a b
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R✝ : Type u_2<VAR>inst✝² : Semiring k<VAR>inst✝¹ : MulOneClass G<VAR>R : Type u_3<VAR>inst✝ : Semiring R<VAR>f : k →+* R<VAR>g : G →* R<VAR>c : k<VAR>φ : MonoidAlgebra k G<GOAL>(liftNC ↑f ⇑g) (c • φ) = f c * (liftNC ↑f ⇑g) φ
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R✝ : Type u_2<VAR>inst✝² : Semiring k<VAR>inst✝¹ : MulOneClass G<VAR>R : Type u_3<VAR>inst✝ : Semiring R<VAR>f : k →+* R<VAR>g : G →* R<VAR>c : k<VAR>φ : MonoidAlgebra k G<GOAL>(liftNC ↑f ⇑g).comp ((smulAddHom k (MonoidAlgebra k G)) c) = (AddMonoidHom.mulLeft (f c)).comp (liftNC ↑f ⇑g)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R✝ : Type u_2<VAR>inst✝² : Semiring k<VAR>inst✝¹ : MulOneClass G<VAR>R : Type u_3<VAR>inst✝ : Semiring R<VAR>f : k →+* R<VAR>g : G →* R<VAR>c : k<VAR>φ : MonoidAlgebra k G<VAR>a : G<VAR>b : k<GOAL>(((liftNC ↑f ⇑g).comp ((smulAddHom k (MonoidAlgebra k G)) c)).comp (singleAddHom a)) b = (((AddMonoidHom.mulLeft (f c)).comp (liftNC ↑f ⇑g)).comp (singleAddHom a)) b
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R✝ : Type u_2<VAR>inst✝² : Semiring k<VAR>inst✝¹ : MulOneClass G<VAR>R : Type u_3<VAR>inst✝ : Semiring R<VAR>f : k →+* R<VAR>g : G →* R<VAR>c : k<VAR>φ : MonoidAlgebra k G<VAR>a : G<VAR>b : k<GOAL>(((liftNC ↑f ⇑g).comp ((smulAddHom k (G →₀ k)) c)).comp (singleAddHom a)) b = (((AddMonoidHom.mulLeft (f c)).comp (liftNC ↑f ⇑g)).comp (singleAddHom a)) b
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R✝ : Type u_2<VAR>inst✝² : Semiring k<VAR>inst✝¹ : MulOneClass G<VAR>R : Type u_3<VAR>inst✝ : Semiring R<VAR>f : k →+* R<VAR>g : G →* R<VAR>c : k<VAR>φ : MonoidAlgebra k G<VAR>a : G<VAR>b : k<GOAL>(liftNC ↑f ⇑g) (Finsupp.single a (c * b)) = f c * (liftNC ↑f ⇑g) (Finsupp.single a b)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R✝ : Type u_2<VAR>inst✝² : Semiring k<VAR>inst✝¹ : MulOneClass G<VAR>R : Type u_3<VAR>inst✝ : Semiring R<VAR>f : k →+* R<VAR>g : G →* R<VAR>c : k<VAR>φ : MonoidAlgebra k G<VAR>a : G<VAR>b : k<GOAL>↑f (c * b) * g a = f c * (↑f b * g a)
<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>f : M ≃[L] N<GOAL>f.symm.toEmbedding.comp f.toEmbedding = Embedding.refl L M
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>X Y : Center C<VAR>U : C<GOAL>(X.snd.β Y.fst).hom ▷ U ≫ (α_ Y.fst X.fst U).hom ≫ Y.fst ◁ (X.snd.β U).hom ≫ (α_ Y.fst U X.fst).inv ≫ (Y.snd.β U).hom ▷ X.fst ≫ (α_ U Y.fst X.fst).hom = ((α_ X.fst Y.fst U).hom ≫ X.fst ◁ (Y.snd.β U).hom ≫ (α_ X.fst U Y.fst).inv ≫ (X.snd.β U).hom ▷ Y.fst ≫ (α_ U X.fst Y.fst).hom) ≫ U ◁ (X.snd.β Y.fst).hom
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>X Y : Center C<VAR>U : C<GOAL>(X.snd.β Y.fst).hom ▷ U ≫ (α_ Y.fst X.fst U).hom ≫ Y.fst ◁ (X.snd.β U).hom ≫ (α_ Y.fst U X.fst).inv ≫ (Y.snd.β U).hom ▷ X.fst ≫ (α_ U Y.fst X.fst).hom = (α_ X.fst Y.fst U).hom ≫ X.fst ◁ (Y.snd.β U).hom ≫ (α_ X.fst U Y.fst).inv ≫ (X.snd.β U).hom ▷ Y.fst ≫ (α_ U X.fst Y.fst).hom ≫ U ◁ (X.snd.β Y.fst).hom
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>X Y : Center C<VAR>U : C<GOAL>X.fst ◁ (Y.snd.β U).hom ≫ ((α_ X.fst U Y.fst).inv ≫ (X.snd.β U).hom ▷ Y.fst ≫ (α_ U X.fst Y.fst).hom ≫ U ◁ (X.snd.β Y.fst).hom ≫ (α_ U Y.fst X.fst).inv) ≫ (α_ U Y.fst X.fst).hom = X.fst ◁ (Y.snd.β U).hom ≫ (α_ X.fst U Y.fst).inv ≫ (X.snd.β U).hom ▷ Y.fst ≫ (α_ U X.fst Y.fst).hom ≫ U ◁ (X.snd.β Y.fst).hom
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x : R<GOAL>Sbtw R 1 x 0 ↔ x ∈ Set.Ioo 0 1
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<GOAL>m < 1 + n ↔ m ≤ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>s t : Set α<VAR>a✝ b✝ x : α<VAR>inst✝ : IsAntisymm α r₂<VAR>h : ∀ (a b : α), r₁ a b → r₂ a b<VAR>a : α<VAR>ha : a ∈ maximals r₂ s<VAR>b : α<VAR>hb : b ∈ s<VAR>hab : r₁ a b<GOAL>r₁ b a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>s t : Set α<VAR>a✝ b✝ x : α<VAR>inst✝ : IsAntisymm α r₂<VAR>h : ∀ (a b : α), r₁ a b → r₂ a b<VAR>a : α<VAR>ha : a ∈ maximals r₂ s<VAR>b : α<VAR>hb : b ∈ s<VAR>hab : r₁ a b<VAR>this : a = b<GOAL>r₁ b a
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{?u.230, u_2} D<VAR>F : C ⥤ D<VAR>inst✝⁵ : F.PreservesEffectiveEpis<VAR>inst✝⁴ : F.ReflectsEffectiveEpis<VAR>inst✝³ : F.EffectivelyEnough<VAR>inst✝² : Preregular D<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>X✝ Y✝ Z✝ : C<VAR>f : X✝ ⟶ Y✝<VAR>g : Z✝ ⟶ Y✝<VAR>x✝ : EffectiveEpi g<GOAL>∃ W h, ∃ (_ : EffectiveEpi h), ∃ i, i ≫ g = h ≫ f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{?u.230, u_2} D<VAR>F : C ⥤ D<VAR>inst✝⁵ : F.PreservesEffectiveEpis<VAR>inst✝⁴ : F.ReflectsEffectiveEpis<VAR>inst✝³ : F.EffectivelyEnough<VAR>inst✝² : Preregular D<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>X✝ Y✝ Z✝ : C<VAR>f : X✝ ⟶ Y✝<VAR>g : Z✝ ⟶ Y✝<VAR>x✝ : EffectiveEpi g<VAR>W : D<VAR>f' : W ⟶ F.obj X✝<VAR>w✝ : EffectiveEpi f'<VAR>i : W ⟶ F.obj Z✝<VAR>w : i ≫ F.map g = f' ≫ F.map f<GOAL>∃ W h, ∃ (_ : EffectiveEpi h), ∃ i, i ≫ g = h ≫ f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{?u.230, u_2} D<VAR>F : C ⥤ D<VAR>inst✝⁵ : F.PreservesEffectiveEpis<VAR>inst✝⁴ : F.ReflectsEffectiveEpis<VAR>inst✝³ : F.EffectivelyEnough<VAR>inst✝² : Preregular D<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>X✝ Y✝ Z✝ : C<VAR>f : X✝ ⟶ Y✝<VAR>g : Z✝ ⟶ Y✝<VAR>x✝ : EffectiveEpi g<VAR>W : D<VAR>f' : W ⟶ F.obj X✝<VAR>w✝ : EffectiveEpi f'<VAR>i : W ⟶ F.obj Z✝<VAR>w : i ≫ F.map g = f' ≫ F.map f<GOAL>EffectiveEpi (F.map (F.preimage (F.effectiveEpiOver W ≫ f')))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{?u.230, u_2} D<VAR>F : C ⥤ D<VAR>inst✝⁵ : F.PreservesEffectiveEpis<VAR>inst✝⁴ : F.ReflectsEffectiveEpis<VAR>inst✝³ : F.EffectivelyEnough<VAR>inst✝² : Preregular D<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>X✝ Y✝ Z✝ : C<VAR>f : X✝ ⟶ Y✝<VAR>g : Z✝ ⟶ Y✝<VAR>x✝ : EffectiveEpi g<VAR>W : D<VAR>f' : W ⟶ F.obj X✝<VAR>w✝ : EffectiveEpi f'<VAR>i : W ⟶ F.obj Z✝<VAR>w : i ≫ F.map g = f' ≫ F.map f<GOAL>F.preimage (F.effectiveEpiOver W ≫ i) ≫ g = F.preimage (F.effectiveEpiOver W ≫ f') ≫ f
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x₀ x₁ : X<VAR>t : ↑I<GOAL>(if ↑t ≤ 1 / 2 then 2 * ↑t else 1) ∈ I
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹⁰ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>a b : OrthonormalBasis ι 𝕜 E<GOAL>‖a.toBasis.det ⇑b‖ = 1
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹⁰ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>a b : OrthonormalBasis ι 𝕜 E<VAR>this : (a.toBasis.toMatrix ⇑b).det * star (a.toBasis.toMatrix ⇑b).det = 1<GOAL>‖a.toBasis.det ⇑b‖ = 1
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹⁰ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>a b : OrthonormalBasis ι 𝕜 E<VAR>this : ↑‖(a.toBasis.toMatrix ⇑b).det‖ ^ 2 = 1<GOAL>‖a.toBasis.det ⇑b‖ = 1
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹⁰ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>a b : OrthonormalBasis ι 𝕜 E<VAR>this : ‖(a.toBasis.toMatrix ⇑b).det‖ ^ 2 = 1<GOAL>‖a.toBasis.det ⇑b‖ = 1
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroObject C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>i : X ≅ 0<VAR>j : Y ≅ 0<GOAL>IsIso f
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroObject C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>i : X ≅ 0<VAR>j : Y ≅ 0<GOAL>IsIso 0
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>hi : i ∈ t<GOAL>t.centerMass (fun j => if i = j then 1 else 0) z = z i
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>hi : i ∈ t<GOAL>∑ i_1 ∈ t, (if i = i_1 then 1 else 0) • z i_1 = z i
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>hi : i ∈ t<GOAL>(∑ i_1 ∈ t, if i = i_1 then 1 else 0) = 1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hf : Inducing f<VAR>s : Set X<VAR>x : X<GOAL>x ∈ closure s ↔ x ∈ f ⁻¹' closure (f '' s)
<VAR>α : Type u_1<VAR>inst✝¹ : AddCommGroup α<VAR>p a a₁ a₂ b b₁ b₂ c : α<VAR>n : ℕ<VAR>z : ℤ<VAR>inst✝ : NoZeroSMulDivisors ℤ α<VAR>hn : z ≠ 0<VAR>m : ℤ<GOAL>z • b - z • a = m • z • p ↔ b - a = m • p
<VAR>p q : ℚ<VAR>s t : Set ℚ<VAR>a✝ : SecondCountableTopology ℚ∞<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁴ : Norm E<VAR>inst✝¹³ : Norm F<VAR>inst✝¹² : Norm G<VAR>inst✝¹¹ : SeminormedAddCommGroup E'<VAR>inst✝¹⁰ : SeminormedAddCommGroup F'<VAR>inst✝⁹ : SeminormedAddCommGroup G'<VAR>inst✝⁸ : NormedAddCommGroup E''<VAR>inst✝⁷ : NormedAddCommGroup F''<VAR>inst✝⁶ : NormedAddCommGroup G''<VAR>inst✝⁵ : SeminormedRing R<VAR>inst✝⁴ : SeminormedAddGroup E'''<VAR>inst✝³ : SeminormedRing R'<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>inst✝¹ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝ : l.NeBot<VAR>d : E''<VAR>c : F''<GOAL>((fun _x => d) =o[l] fun _x => c) ↔ d = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁴ : Norm E<VAR>inst✝¹³ : Norm F<VAR>inst✝¹² : Norm G<VAR>inst✝¹¹ : SeminormedAddCommGroup E'<VAR>inst✝¹⁰ : SeminormedAddCommGroup F'<VAR>inst✝⁹ : SeminormedAddCommGroup G'<VAR>inst✝⁸ : NormedAddCommGroup E''<VAR>inst✝⁷ : NormedAddCommGroup F''<VAR>inst✝⁶ : NormedAddCommGroup G''<VAR>inst✝⁵ : SeminormedRing R<VAR>inst✝⁴ : SeminormedAddGroup E'''<VAR>inst✝³ : SeminormedRing R'<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>inst✝¹ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝ : l.NeBot<VAR>d : E''<VAR>c : F''<VAR>this : ¬Tendsto (Function.const α ‖c‖) l atTop<GOAL>((fun _x => d) =o[l] fun _x => c) ↔ d = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁴ : Norm E<VAR>inst✝¹³ : Norm F<VAR>inst✝¹² : Norm G<VAR>inst✝¹¹ : SeminormedAddCommGroup E'<VAR>inst✝¹⁰ : SeminormedAddCommGroup F'<VAR>inst✝⁹ : SeminormedAddCommGroup G'<VAR>inst✝⁸ : NormedAddCommGroup E''<VAR>inst✝⁷ : NormedAddCommGroup F''<VAR>inst✝⁶ : NormedAddCommGroup G''<VAR>inst✝⁵ : SeminormedRing R<VAR>inst✝⁴ : SeminormedAddGroup E'''<VAR>inst✝³ : SeminormedRing R'<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>inst✝¹ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝ : l.NeBot<VAR>d : E''<VAR>c : F''<VAR>this : ¬Tendsto (Function.const α ‖c‖) l atTop<GOAL>Tendsto (norm ∘ fun _x => c) l atTop → d = 0
<VAR>n : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<GOAL>ClosedEmbedding ⇑hA.cfcAux
<VAR>n : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<VAR>h0 : FiniteDimensional ℝ C(↑(spectrum ℝ A), ℝ)<GOAL>ClosedEmbedding ⇑hA.cfcAux
<VAR>n : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<VAR>h0 : FiniteDimensional ℝ C(↑(spectrum ℝ A), ℝ)<VAR>f : C(↑(spectrum ℝ A), ℝ)<VAR>hf : ↑hA.cfcAux f = 0<GOAL>f = 0
<VAR>n : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<VAR>h0 : FiniteDimensional ℝ C(↑(spectrum ℝ A), ℝ)<VAR>f : C(↑(spectrum ℝ A), ℝ)<VAR>hf : ↑hA.cfcAux f = 0<VAR>h2 : diagonal (RCLike.ofReal ∘ ⇑f ∘ fun i => ⟨hA.eigenvalues i, ⋯⟩) = 0<GOAL>f = 0
<VAR>n : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<VAR>h0 : FiniteDimensional ℝ C(↑(spectrum ℝ A), ℝ)<VAR>f : C(↑(spectrum ℝ A), ℝ)<VAR>hf : ↑hA.cfcAux f = 0<VAR>h2 : diagonal (RCLike.ofReal ∘ ⇑f ∘ fun i => ⟨hA.eigenvalues i, ⋯⟩) = 0<VAR>x : ↑(spectrum ℝ A)<GOAL>f x = 0 x
<VAR>n : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<VAR>h0 : FiniteDimensional ℝ C(↑(spectrum ℝ A), ℝ)<VAR>f : C(↑(spectrum ℝ A), ℝ)<VAR>hf : ↑hA.cfcAux f = 0<VAR>h2 : diagonal (RCLike.ofReal ∘ ⇑f ∘ fun i => ⟨hA.eigenvalues i, ⋯⟩) = 0<VAR>x : ↑(spectrum ℝ A)<GOAL>f x = 0
<VAR>n : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<VAR>h0 : FiniteDimensional ℝ C(↑(spectrum ℝ A), ℝ)<VAR>f : C(↑(spectrum ℝ A), ℝ)<VAR>hf : ↑hA.cfcAux f = 0<VAR>h2 : diagonal (RCLike.ofReal ∘ ⇑f ∘ fun i => ⟨hA.eigenvalues i, ⋯⟩) = 0<VAR>x : ℝ<VAR>hx : x ∈ spectrum ℝ A<GOAL>f ⟨x, hx⟩ = 0
<VAR>n : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<VAR>h0 : FiniteDimensional ℝ C(↑(spectrum ℝ A), ℝ)<VAR>f : C(↑(spectrum ℝ A), ℝ)<VAR>hf : ↑hA.cfcAux f = 0<VAR>h2 : diagonal (RCLike.ofReal ∘ ⇑f ∘ fun i => ⟨hA.eigenvalues i, ⋯⟩) = 0<VAR>i : n<VAR>hx : hA.eigenvalues i ∈ spectrum ℝ A<GOAL>f ⟨hA.eigenvalues i, hx⟩ = 0
<VAR>n : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<VAR>h0 : FiniteDimensional ℝ C(↑(spectrum ℝ A), ℝ)<VAR>f : C(↑(spectrum ℝ A), ℝ)<VAR>hf : ↑hA.cfcAux f = 0<VAR>h2 : diagonal (RCLike.ofReal ∘ ⇑f ∘ fun i => ⟨hA.eigenvalues i, ⋯⟩) = diagonal fun x => 0<VAR>i : n<VAR>hx : hA.eigenvalues i ∈ spectrum ℝ A<GOAL>f ⟨hA.eigenvalues i, hx⟩ = 0
<VAR>n : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<VAR>h0 : FiniteDimensional ℝ C(↑(spectrum ℝ A), ℝ)<VAR>f : C(↑(spectrum ℝ A), ℝ)<VAR>hf : ↑hA.cfcAux f = 0<VAR>h2 : diagonal (RCLike.ofReal ∘ ⇑f ∘ fun i => ⟨hA.eigenvalues i, ⋯⟩) = diagonal fun x => 0<VAR>i : n<VAR>hx : hA.eigenvalues i ∈ spectrum ℝ A<VAR>this : ∀ (i : n), (RCLike.ofReal ∘ ⇑f ∘ fun i => ⟨hA.eigenvalues i, ⋯⟩) i = 0<GOAL>f ⟨hA.eigenvalues i, hx⟩ = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s✝ t : Set α<VAR>f✝ g f : α → E<VAR>s : Set α<GOAL>⨍ (x : α) in s, f x ∂μ = ∫ (x : α), f x ∂(μ s)⁻¹ • μ.restrict s
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁶ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝³ : FunLike F M M₂<VAR>inst✝² : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>M' : Type u_9<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>q₁ q₁' : Submodule R M'<GOAL>p.prod q₁ ⊔ p'.prod q₁' = (p ⊔ p').prod (q₁ ⊔ q₁')
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁶ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝³ : FunLike F M M₂<VAR>inst✝² : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>M' : Type u_9<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>q₁ q₁' : Submodule R M'<GOAL>(p ⊔ p').prod (q₁ ⊔ q₁') ≤ p.prod q₁ ⊔ p'.prod q₁'
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁶ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝³ : FunLike F M M₂<VAR>inst✝² : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>M' : Type u_9<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>q₁ q₁' : Submodule R M'<GOAL>∀ (a : M) (b : M'), a ∈ p ⊔ p' → b ∈ q₁ ⊔ q₁' → (a, b) ∈ p.prod q₁ ⊔ p'.prod q₁'
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁶ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝³ : FunLike F M M₂<VAR>inst✝² : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>M' : Type u_9<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>q₁ q₁' : Submodule R M'<VAR>xx : M<VAR>yy : M'<VAR>hxx : xx ∈ p ⊔ p'<VAR>hyy : yy ∈ q₁ ⊔ q₁'<GOAL>(xx, yy) ∈ p.prod q₁ ⊔ p'.prod q₁'
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁶ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝³ : FunLike F M M₂<VAR>inst✝² : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>M' : Type u_9<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>q₁ q₁' : Submodule R M'<VAR>yy : M'<VAR>hyy : yy ∈ q₁ ⊔ q₁'<VAR>x : M<VAR>hx : x ∈ p<VAR>x' : M<VAR>hx' : x' ∈ p'<VAR>hxx : x + x' ∈ p ⊔ p'<GOAL>(x + x', yy) ∈ p.prod q₁ ⊔ p'.prod q₁'
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁶ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝³ : FunLike F M M₂<VAR>inst✝² : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>M' : Type u_9<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>q₁ q₁' : Submodule R M'<VAR>x : M<VAR>hx : x ∈ p<VAR>x' : M<VAR>hx' : x' ∈ p'<VAR>hxx : x + x' ∈ p ⊔ p'<VAR>y : M'<VAR>hy : y ∈ q₁<VAR>y' : M'<VAR>hy' : y' ∈ q₁'<VAR>hyy : y + y' ∈ q₁ ⊔ q₁'<GOAL>(x + x', y + y') ∈ p.prod q₁ ⊔ p'.prod q₁'