ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>m : ℝ≥0∞ → ℝ≥0∞<VAR>μ : Measure X<VAR>ε : ℝ≥0∞<VAR>h₀ : 0 < ε<VAR>h : ∀ (s : Set X), diam s ≤ ε → μ s ≤ m (diam s)<GOAL>μ.toOuterMeasure ≤ OuterMeasure.mkMetric m
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>g✝ : P →ₗ[R] Q<VAR>f✝ : N →ₗ[R] P<VAR>f : M →ₗ[R] P<VAR>g : N →ₗ[R] Q<GOAL>rTensor Q f ∘ₗ lTensor M g = map f g
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : HasExt C<VAR>X Y Z T : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>n : ℕ<VAR>α : Ext Z T n<GOAL>(mk₀ f).comp ((mk₀ g).comp α ⋯) ⋯ = (mk₀ (f ≫ g)).comp α ⋯
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : HasExt C<VAR>X Y Z T : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>n : ℕ<VAR>α : Ext Z T n<GOAL>0 + 0 + n = n
<VAR>R : Type u_1<VAR>inst✝ : AddMonoidWithOne R<VAR>n : ℕ<GOAL>↑1 n = 1 n
<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>α : Type u_1<VAR>a : ℝ≥0∞<GOAL>a * a < ⊤ ↔ a < ⊤
<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>α : Type u_1<VAR>a : ℝ≥0∞<GOAL>a = 0 → a < ⊤
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>α : Type u_1<GOAL>0 < ⊤
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : Fintype l<VAR>inst✝ : CommRing R<VAR>A : Matrix (l ⊕ l) (l ⊕ l) R<VAR>hA : A ∈ symplecticGroup l R<GOAL>Aᵀ ∈ symplecticGroup l R
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : Fintype l<VAR>inst✝ : CommRing R<VAR>A : Matrix (l ⊕ l) (l ⊕ l) R<VAR>hA : A * J l R * Aᵀ = J l R<GOAL>Aᵀ * J l R * Aᵀᵀ = J l R
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : Fintype l<VAR>inst✝ : CommRing R<VAR>A : Matrix (l ⊕ l) (l ⊕ l) R<VAR>hA : A * J l R * Aᵀ = J l R<GOAL>Aᵀ * J l R * A = J l R
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : Fintype l<VAR>inst✝ : CommRing R<VAR>A : Matrix (l ⊕ l) (l ⊕ l) R<VAR>hA : A * J l R * Aᵀ = J l R<VAR>huA : IsUnit A.det<GOAL>Aᵀ * J l R * A = J l R
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : Fintype l<VAR>inst✝ : CommRing R<VAR>A : Matrix (l ⊕ l) (l ⊕ l) R<VAR>hA : A * J l R * Aᵀ = J l R<VAR>huA : IsUnit A.det<VAR>huAT : IsUnit Aᵀ.det<GOAL>Aᵀ * J l R * A = J l R
<VAR>s : ℝ<VAR>h : IntegrableOn (fun x => x ^ s) (Ioi 0) volume<GOAL>False
<VAR>s : ℝ<VAR>h : IntegrableOn (fun x => x ^ s) (Ioi 0) volume<VAR>hs : s ≤ -1<GOAL>False
<VAR>s : ℝ<VAR>h : IntegrableOn (fun x => x ^ s) (Ioi 0) volume<VAR>hs : -1 < s<GOAL>False
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝²² : NontriviallyNormedField R<VAR>inst✝²¹ : (x : B) → AddCommMonoid (E x)<VAR>inst✝²⁰ : (x : B) → Module R (E x)<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace R F<VAR>inst✝¹⁷ : TopologicalSpace B<VAR>inst✝¹⁶ : (x : B) → TopologicalSpace (E x)<VAR>𝕜₁ : Type u_5<VAR>𝕜₂ : Type u_6<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜₁<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>B' : Type u_7<VAR>inst✝¹³ : TopologicalSpace B'<VAR>inst✝¹² : NormedSpace 𝕜₁ F<VAR>inst✝¹¹ : (x : B) → Module 𝕜₁ (E x)<VAR>inst✝¹⁰ : TopologicalSpace (TotalSpace F E)<VAR>F' : Type u_8<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜₂ F'<VAR>E' : B' → Type u_9<VAR>inst✝⁷ : (x : B') → AddCommMonoid (E' x)<VAR>inst✝⁶ : (x : B') → Module 𝕜₂ (E' x)<VAR>inst✝⁵ : TopologicalSpace (TotalSpace F' E')<VAR>inst✝⁴ : FiberBundle F E<VAR>inst✝³ : VectorBundle 𝕜₁ F E<VAR>inst✝² : (x : B') → TopologicalSpace (E' x)<VAR>inst✝¹ : FiberBundle F' E'<VAR>inst✝ : VectorBundle 𝕜₂ F' E'<VAR>x₀ x : B<VAR>y₀ y : B'<VAR>ϕ : E x →SL[σ] E' y<VAR>hx : x ∈ (trivializationAt F E x₀).baseSet<VAR>hy : y ∈ (trivializationAt F' E' y₀).baseSet<VAR>x✝ : F<GOAL>(inCoordinates F E F' E' x₀ x y₀ y ϕ) x✝ = ((↑(Trivialization.continuousLinearEquivAt 𝕜₂ (trivializationAt F' E' y₀) y hy)).comp (ϕ.comp ↑(Trivialization.continuousLinearEquivAt 𝕜₁ (trivializationAt F E x₀) x hx).symm)) x✝
<VAR>R : Type u_1<VAR>inst✝ : NonUnitalSemiring R<VAR>u : (PreQuasiregular R)ˣ<GOAL>(↑u⁻¹).val + (↑u).val + (↑u).val * (↑u⁻¹).val = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>I : Ideal R<VAR>h : RingHom.ker f ≤ I<GOAL>map f I.radical = (map f I).radical
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>I : Ideal R<VAR>h : RingHom.ker f ≤ I<GOAL>map f (sInf {J | I ≤ J ∧ J.IsPrime}) = sInf {J | map f I ≤ J ∧ J.IsPrime}
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>I : Ideal R<VAR>h : RingHom.ker f ≤ I<VAR>this : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J<GOAL>map f (sInf {J | I ≤ J ∧ J.IsPrime}) = sInf {J | map f I ≤ J ∧ J.IsPrime}
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>I : Ideal R<VAR>h : RingHom.ker f ≤ I<VAR>this : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J<GOAL>{J | map f I ≤ J ∧ J.IsPrime} = map f '' {J | I ≤ J ∧ J.IsPrime}
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>I : Ideal R<VAR>h : RingHom.ker f ≤ I<VAR>this : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J<VAR>j : Ideal S<GOAL>{J | map f I ≤ J ∧ J.IsPrime} j → (map f '' {J | I ≤ J ∧ J.IsPrime}) j
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>I : Ideal R<VAR>h : RingHom.ker f ≤ I<VAR>this : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J<VAR>j : Ideal S<GOAL>(map f '' {J | I ≤ J ∧ J.IsPrime}) j → {J | map f I ≤ J ∧ J.IsPrime} j
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>a : α<GOAL>a ∈ {a}
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>a : α<GOAL>a ∈ a ::ₘ 0
<VAR>G : Type u<VAR>M : Type v<VAR>α : Type w<VAR>s✝ : Set α<VAR>m : MeasurableSpace α<VAR>inst✝⁴ : Group G<VAR>inst✝³ : MulAction G α<VAR>inst✝² : MeasurableSpace G<VAR>inst✝¹ : MeasurableSMul G α<VAR>c✝ : G<VAR>μ : Measure α<VAR>inst✝ : SMulInvariantMeasure G α μ<VAR>s : Set α<VAR>hs : NullMeasurableSet s μ<VAR>c : G<GOAL>NullMeasurableSet (c • s) μ
<VAR>α : Type u<VAR>β : Type u_1<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>s : Set (Set α)<VAR>this : TopologicalSpace α := generateFrom s<GOAL>IsTopologicalBasis ((fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s})
<VAR>α : Type u<VAR>β : Type u_1<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>s : Set (Set α)<VAR>this : TopologicalSpace α := generateFrom s<GOAL>∀ t₁ ∈ (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s}, ∀ t₂ ∈ (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s}, ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s}, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
<VAR>α : Type u<VAR>β : Type u_1<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>s : Set (Set α)<VAR>this : TopologicalSpace α := generateFrom s<GOAL>⋃₀ ((fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s}) = univ
<VAR>α : Type u<VAR>β : Type u_1<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>s : Set (Set α)<VAR>this : TopologicalSpace α := generateFrom s<GOAL>∀ s_1 ∈ (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s}, IsOpen s_1
<VAR>α : Type u<VAR>β : Type u_1<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>s : Set (Set α)<VAR>this : TopologicalSpace α := generateFrom s<VAR>t : Set α<VAR>ht : t ∈ s<GOAL>t ∈ (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s}
<VAR>a b c d : ℝ≥0∞<VAR>r p q x : ℝ≥0<VAR>hx : ↑x ≠ 0<VAR>y : ℝ≥0<VAR>hy : 1 < ↑y<GOAL>∃ n, ↑x ∈ Ioc (↑y ^ n) (↑y ^ (n + 1))
<VAR>a b c d : ℝ≥0∞<VAR>r p q x : ℝ≥0<VAR>hx : ↑x ≠ 0<VAR>y : ℝ≥0<VAR>hy : 1 < ↑y<VAR>A : y ≠ 0<GOAL>∃ n, ↑x ∈ Ioc (↑y ^ n) (↑y ^ (n + 1))
<VAR>a b c d : ℝ≥0∞<VAR>r p q x : ℝ≥0<VAR>hx : ↑x ≠ 0<VAR>y : ℝ≥0<VAR>hy : 1 < ↑y<VAR>A : y ≠ 0<VAR>n : ℤ<VAR>hn : y ^ n < x<VAR>h'n : x ≤ y ^ (n + 1)<GOAL>∃ n, ↑x ∈ Ioc (↑y ^ n) (↑y ^ (n + 1))
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v, u₁} C<VAR>C' : Type u₂<VAR>inst✝² : Category.{v, u₂} C'<VAR>D : GlueData C<VAR>F : C ⥤ C'<VAR>H : (i j k : D.J) → PreservesLimit (cospan (D.f i j) (D.f i k)) F<VAR>inst✝¹ : HasMulticoequalizer D.diagram<VAR>inst✝ : PreservesColimit D.diagram.multispan F<VAR>i : D.J<VAR>this : HasColimit (D.mapGlueData F).diagram.multispan<GOAL>colimit.ι (D.diagram.multispan ⋙ F) (WalkingMultispan.right i) ≫ (HasColimit.isoOfNatIso (D.diagramIso F)).hom = (D.mapGlueData F).ι i
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v, u₁} C<VAR>C' : Type u₂<VAR>inst✝² : Category.{v, u₂} C'<VAR>D : GlueData C<VAR>F : C ⥤ C'<VAR>H : (i j k : D.J) → PreservesLimit (cospan (D.f i j) (D.f i k)) F<VAR>inst✝¹ : HasMulticoequalizer D.diagram<VAR>inst✝ : PreservesColimit D.diagram.multispan F<VAR>i : D.J<VAR>this : HasColimit (D.mapGlueData F).diagram.multispan<GOAL>(D.diagramIso F).hom.app (WalkingMultispan.right i) ≫ colimit.ι (D.mapGlueData F).diagram.multispan (WalkingMultispan.right i) = (D.mapGlueData F).ι i
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v, u₁} C<VAR>C' : Type u₂<VAR>inst✝² : Category.{v, u₂} C'<VAR>D : GlueData C<VAR>F : C ⥤ C'<VAR>H : (i j k : D.J) → PreservesLimit (cospan (D.f i j) (D.f i k)) F<VAR>inst✝¹ : HasMulticoequalizer D.diagram<VAR>inst✝ : PreservesColimit D.diagram.multispan F<VAR>i : D.J<VAR>this : HasColimit (D.mapGlueData F).diagram.multispan<GOAL>colimit.ι (D.mapGlueData F).diagram.multispan (WalkingMultispan.right i) = (D.mapGlueData F).ι i
<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>f : ι → ℝ≥0<VAR>r : ℝ<GOAL>∏ i ∈ s, ↑(f i) ^ r = ↑(∏ i ∈ s, f i) ^ r
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p : R<VAR>k n m : ℕ<VAR>hn : IsPrimePow n<VAR>hm : m ∣ n<VAR>hm₁ : m ≠ 1<GOAL>IsPrimePow m
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p : R<VAR>k n m : ℕ<VAR>hn : ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n<VAR>hm : m ∣ n<VAR>hm₁ : m ≠ 1<GOAL>∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = m
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n p✝ : R<VAR>k✝ m : ℕ<VAR>hm₁ : m ≠ 1<VAR>p k : ℕ<VAR>hp : Nat.Prime p<VAR>_hk : 0 < k<VAR>hm : m ∣ p ^ k<GOAL>∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = m
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n p✝ : R<VAR>k✝ p k : ℕ<VAR>hp : Nat.Prime p<VAR>_hk : 0 < k<VAR>i : ℕ<VAR>hik : i ≤ k<VAR>hm₁ : p ^ i ≠ 1<VAR>hm : p ^ i ∣ p ^ k<GOAL>∃ p_1 k, Nat.Prime p_1 ∧ 0 < k ∧ p_1 ^ k = p ^ i
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n p✝ : R<VAR>k✝ p k : ℕ<VAR>hp : Nat.Prime p<VAR>_hk : 0 < k<VAR>i : ℕ<VAR>hik : i ≤ k<VAR>hm₁ : p ^ i ≠ 1<VAR>hm : p ^ i ∣ p ^ k<GOAL>0 < i
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n p✝ : R<VAR>k✝ p k : ℕ<VAR>hp : Nat.Prime p<VAR>_hk : 0 < k<VAR>i : ℕ<VAR>hik : i ≤ k<VAR>hm₁ : p ^ i ≠ 1<VAR>hm : p ^ i ∣ p ^ k<GOAL>i ≠ 0
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n p✝ : R<VAR>k✝ p k : ℕ<VAR>hp : Nat.Prime p<VAR>_hk : 0 < k<VAR>hik : 0 ≤ k<VAR>hm₁ : p ^ 0 ≠ 1<VAR>hm : p ^ 0 ∣ p ^ k<GOAL>False
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁶ : AddCommMonoid A<VAR>inst✝⁵ : AddCommMonoid B<VAR>inst✝⁴ : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i : ι<VAR>g : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝³ : Zero M<VAR>inst✝² : Zero M'<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DecidableEq α<VAR>f : α →₀ M<VAR>a : α<VAR>b : α → M → N<GOAL>(∏ a_1 ∈ f.support, if a_1 = a then b a_1 (f a_1) else 1) = if a ∈ f.support then b a (f a) else 1
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝² : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝¹ : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>inst✝ : ∀ (i : ι), SigmaFinite (μ i)<VAR>s : (i : ι) → Set (α i)<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<GOAL>(Measure.pi μ) (univ.pi s) = ∏ i : ι, (μ i) (s i)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝² : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝¹ : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>inst✝ : ∀ (i : ι), SigmaFinite (μ i)<VAR>s : (i : ι) → Set (α i)<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<GOAL>(Measure.pi μ) (univ.pi s) ≤ ∏ i : ι, (μ i) (s i)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝² : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝¹ : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>inst✝ : ∀ (i : ι), SigmaFinite (μ i)<VAR>s : (i : ι) → Set (α i)<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<GOAL>∏ i : ι, (μ i) (s i) ≤ (Measure.pi μ) (univ.pi s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>inst✝ : Subsingleton α<VAR>this : Fintype α := Fintype.ofSubsingleton a<GOAL>Nat.card α = 1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>S' : Type u_6<VAR>inst✝¹ : NonAssocRing R<VAR>inst✝ : NonAssocRing S<VAR>f : R ≃+* S<VAR>x✝ y x : R<GOAL>f x = -1 ↔ x = -1
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝ : MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>X : Ω → E<VAR>ℙ : Measure Ω<VAR>μ : autoParam (Measure E) _auto✝<VAR>hX : HasPDF X ℙ μ<GOAL>map X ℙ = withDensity μ (pdf X ℙ μ)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : PseudoEMetricSpace α<VAR>inst✝² : PseudoEMetricSpace β<VAR>inst✝¹ : PseudoEMetricSpace γ<VAR>f✝ : α → β<VAR>x✝ y✝ z : α<VAR>s : Set α<VAR>δ : Type u_2<VAR>inst✝ : PseudoEMetricSpace δ<VAR>f : α → β<VAR>g : γ → δ<VAR>hf : Isometry f<VAR>hg : Isometry g<VAR>x y : α × γ<GOAL>edist (Prod.map f g x) (Prod.map f g y) = edist x y
<VAR>α : Type u_1<VAR>inst✝² : Zero α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : DecidableRel fun x x_1 => x < x_1<VAR>a : α<GOAL>sign a = -1 ↔ a < 0
<VAR>α : Type u_1<VAR>inst✝² : Zero α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : DecidableRel fun x x_1 => x < x_1<VAR>a : α<VAR>h : sign a = -1<GOAL>a < 0
<VAR>α : Type u_1<VAR>inst✝² : Zero α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : DecidableRel fun x x_1 => x < x_1<VAR>a : α<VAR>h : (if 0 < a then 1 else if a < 0 then -1 else 0) = -1<GOAL>a < 0
<VAR>n : Nat<VAR>i : Fin (list n).length<GOAL>(list n).get i = cast ⋯ i
<VAR>R : Type u<VAR>S : Type v<VAR>a b c✝ d : R<VAR>n m : ℕ<VAR>inst✝² : Ring R<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : Ring S<VAR>c : S<GOAL>(X - C c).nextCoeff = -c
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v, u₁} C<VAR>inst✝⁴ : Preadditive C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v, u₂} D<VAR>inst✝² : Abelian D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>inst✝¹ : G.PreservesZeroMorphisms<VAR>i : F ⋙ G ≅ 𝟭 C<VAR>adj : G ⊣ F<VAR>inst✝ : PreservesFiniteLimits G<VAR>X✝ Y✝ : C<VAR>f : X✝ ⟶ Y✝<GOAL>HasKernel f
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v, u₁} C<VAR>inst✝⁴ : Preadditive C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v, u₂} D<VAR>inst✝² : Abelian D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>inst✝¹ : G.PreservesZeroMorphisms<VAR>i : F ⋙ G ≅ 𝟭 C<VAR>adj : G ⊣ F<VAR>inst✝ : PreservesFiniteLimits G<VAR>X✝ Y✝ : C<VAR>f : X✝ ⟶ Y✝<VAR>this : i.inv.app X✝ ≫ (F ⋙ G).map f ≫ i.hom.app Y✝ = (𝟭 C).map f<GOAL>HasKernel f
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v, u₁} C<VAR>inst✝⁴ : Preadditive C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v, u₂} D<VAR>inst✝² : Abelian D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>inst✝¹ : G.PreservesZeroMorphisms<VAR>i : F ⋙ G ≅ 𝟭 C<VAR>adj : G ⊣ F<VAR>inst✝ : PreservesFiniteLimits G<VAR>X✝ Y✝ : C<VAR>f : X✝ ⟶ Y✝<VAR>this : i.inv.app X✝ ≫ G.map (F.map f) ≫ i.hom.app Y✝ = f<GOAL>HasKernel f
<VAR>i j k : ℤ<GOAL>(↑(i.lcm j)).lcm k = i.lcm ↑(j.lcm k)
<VAR>i j k : ℤ<GOAL>(i.natAbs.lcm j.natAbs).lcm k.natAbs = i.natAbs.lcm (j.natAbs.lcm k.natAbs)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁶ : _root_.RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>inst✝² : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>V : ι → Submodule 𝕜 E<VAR>hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ<VAR>x : ⨁ (i : ι), ↥(V i)<VAR>i : ι<VAR>inst✝ : CompleteSpace ↥(V i)<GOAL>(orthogonalProjection (V i)) ((DirectSum.coeAddMonoidHom V) x) = x i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁶ : _root_.RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>inst✝² : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>V : ι → Submodule 𝕜 E<VAR>hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ<VAR>i : ι<VAR>inst✝ : CompleteSpace ↥(V i)<GOAL>(orthogonalProjection (V i)) ((DirectSum.coeAddMonoidHom V) 0) = 0 i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁶ : _root_.RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>inst✝² : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>V : ι → Submodule 𝕜 E<VAR>hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ<VAR>i : ι<VAR>inst✝ : CompleteSpace ↥(V i)<VAR>j : ι<VAR>x : ↥(V j)<GOAL>(orthogonalProjection (V i)) ((DirectSum.coeAddMonoidHom V) ((of (fun i => ↥(V i)) j) x)) = ((of (fun i => ↥(V i)) j) x) i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁶ : _root_.RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>inst✝² : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>V : ι → Submodule 𝕜 E<VAR>hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ<VAR>i : ι<VAR>inst✝ : CompleteSpace ↥(V i)<VAR>x y : ⨁ (i : ι), ↥(V i)<VAR>hx : (orthogonalProjection (V i)) ((DirectSum.coeAddMonoidHom V) x) = x i<VAR>hy : (orthogonalProjection (V i)) ((DirectSum.coeAddMonoidHom V) y) = y i<GOAL>(orthogonalProjection (V i)) ((DirectSum.coeAddMonoidHom V) (x + y)) = (x + y) i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>C : EReal<VAR>h : C ≠ ⊥<VAR>h' : C ≠ ⊤<GOAL>Tendsto (fun n => C / ↑n) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>C : EReal<VAR>h : C ≠ ⊥<VAR>h' : C ≠ ⊤<VAR>this : (fun n => C / ↑n) = fun n => ↑(C.toReal / ↑n)<GOAL>Tendsto (fun n => C / ↑n) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>C : EReal<VAR>h : C ≠ ⊥<VAR>h' : C ≠ ⊤<VAR>this : (fun n => C / ↑n) = fun n => ↑(C.toReal / ↑n)<GOAL>Tendsto (fun n => C.toReal / ↑n) atTop (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : InnerProductSpace 𝕜 F<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : CompleteSpace F<VAR>U : Submodule 𝕜 E<VAR>T : E →L[𝕜] E<VAR>hT : T.IsPositive<VAR>inst✝ : CompleteSpace ↥U<GOAL>(U.subtypeL.comp ((orthogonalProjection U).comp (T.comp (U.subtypeL.comp (orthogonalProjection U))))).IsPositive
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : InnerProductSpace 𝕜 F<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : CompleteSpace F<VAR>U : Submodule 𝕜 E<VAR>T : E →L[𝕜] E<VAR>hT : T.IsPositive<VAR>inst✝ : CompleteSpace ↥U<VAR>this : ((U.subtypeL.comp (orthogonalProjection U)).comp (T.comp (adjoint (U.subtypeL.comp (orthogonalProjection U))))).IsPositive<GOAL>(U.subtypeL.comp ((orthogonalProjection U).comp (T.comp (U.subtypeL.comp (orthogonalProjection U))))).IsPositive
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>σ : ι → Type u_7<VAR>τ : κ → Type u_8<VAR>inst✝² : (i : ι) → TopologicalSpace (σ i)<VAR>inst✝¹ : (k : κ) → TopologicalSpace (τ k)<VAR>inst✝ : TopologicalSpace X<VAR>fst✝ : ι<VAR>snd✝ : σ fst✝<GOAL>𝓝 ⟨fst✝, snd✝⟩ = Filter.map (mk ⟨fst✝, snd✝⟩.fst) (𝓝 ⟨fst✝, snd✝⟩.snd)
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>f : α → β → γ<VAR>l₁ : List α<VAR>l₂ : List β<VAR>z : γ<VAR>i : ℕ<GOAL>(zipWith f l₁ l₂).get? i = some z ↔ ∃ x y, l₁.get? i = some x ∧ l₂.get? i = some y ∧ f x y = z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<GOAL>Ioi a \ Ici b = Ioo a b
<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>μ : FiniteMeasure Ω<VAR>A : Set Ω<GOAL>(μ.restrict A).mass = μ A
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : Ring S<VAR>M : Type u_4<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>m✝ : Submodule R M<VAR>N : Type u_5<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>x✝¹ : Nontrivial M ∧ ∀ (x : M), x ≠ 0 → Function.Surjective ⇑(LinearMap.toSpanSingleton R M x)<VAR>left✝ : Nontrivial M<VAR>h : ∀ (x : M), x ≠ 0 → Function.Surjective ⇑(LinearMap.toSpanSingleton R M x)<VAR>m : Submodule R M<VAR>ne_bot : ¬m = ⊥<VAR>x : M<VAR>hxm : x ∈ m<VAR>hx0 : x ≠ 0<VAR>y : R<VAR>x✝ : (LinearMap.toSpanSingleton R M x) y ∈ ⊤<GOAL>(LinearMap.toSpanSingleton R M x) y ∈ m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>A✝ : Matrix n n α<VAR>inst✝³ : RCLike α<VAR>inst✝² : RCLike β<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n α<GOAL>A.IsHermitian ↔ (toEuclideanLin A).IsSymmetric
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>A✝ : Matrix n n α<VAR>inst✝³ : RCLike α<VAR>inst✝² : RCLike β<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n α<GOAL>A.IsHermitian ↔ ∀ (x₁ x₂ : n → α), ⟪(toEuclideanLin A) ((WithLp.equiv 2 (n → α)).symm x₁), (WithLp.equiv 2 (n → α)).symm x₂⟫_α = ⟪(WithLp.equiv 2 (n → α)).symm x₁, (toEuclideanLin A) ((WithLp.equiv 2 (n → α)).symm x₂)⟫_α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>A✝ : Matrix n n α<VAR>inst✝³ : RCLike α<VAR>inst✝² : RCLike β<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n α<GOAL>A.IsHermitian ↔ ∀ (x₁ x₂ : n → α), star x₁ ᵥ* Aᴴ ⬝ᵥ x₂ = star x₁ ᵥ* A ⬝ᵥ x₂
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝² : Semiring α<VAR>inst✝¹ : Semiring β<VAR>a b : α<VAR>m : ℕ<VAR>inst✝ : IsCancelAdd α<VAR>hab : a + b = 0<VAR>k : ℕ<VAR>ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0<GOAL>a ^ (2 * (k + 1) + 1) + b ^ (2 * (k + 1) + 1) = 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝² : Semiring α<VAR>inst✝¹ : Semiring β<VAR>a b : α<VAR>m : ℕ<VAR>inst✝ : IsCancelAdd α<VAR>hab : a + b = 0<VAR>k : ℕ<VAR>ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0<VAR>this : a ^ 2 = b ^ 2<GOAL>a ^ (2 * (k + 1) + 1) + b ^ (2 * (k + 1) + 1) = 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝² : Semiring α<VAR>inst✝¹ : Semiring β<VAR>a b : α<VAR>m : ℕ<VAR>inst✝ : IsCancelAdd α<VAR>hab : a + b = 0<VAR>k : ℕ<VAR>ih : a ^ (2 * k + 1) + b ^ (2 * k + 1) = 0<VAR>this : a ^ 2 = b ^ 2<GOAL>a ^ (2 * (k + 1) + 1) + b ^ (2 * (k + 1) + 1) + b ^ (2 * k + 1) * a ^ 2 = 0 + b ^ (2 * k + 1) * a ^ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n✝ d✝ k N : ℕ<VAR>x : Fin n✝ → ℕ<VAR>n d : ℕ<GOAL>∃ k ∈ range (n * (d - 1) ^ 2 + 1), ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(sphere n d k).card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n✝ d✝ k N : ℕ<VAR>x✝ : Fin n✝ → ℕ<VAR>n d : ℕ<VAR>x : Fin n → ℕ<VAR>hx : x ∈ box n d<GOAL>∑ i : Fin n, x i ^ 2 ∈ range (n * (d - 1) ^ 2 + 1)