ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁸ : CommRing P<VAR>A : Type u_4<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : IsDomain A<VAR>K : Type u_5<VAR>B : Type u_6<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : Field K<VAR>L : Type u_7<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>g : A →+* L<VAR>z : K<VAR>x y : A<VAR>hy : y ∈ nonZeroDivisors A<VAR>h : mk' K x ⟨y, hy⟩ = z<GOAL>(algebraMap A K) x / (algebraMap A K) y = z
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : NormedAddCommGroup E''<VAR>inst✝¹² : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>inst✝⁸ : NormedSpace 𝕜 E''<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁶ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : μ.IsAddLeftInvariant<VAR>inst✝² : μ.IsNegInvariant<VAR>inst✝¹ : MeasurableNeg G<VAR>inst✝ : MeasurableAdd G<GOAL>(f ⋆[L, μ] g) x = ∫ (t : G), (L (f (x - t))) (g t) ∂μ
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : NormedAddCommGroup E''<VAR>inst✝¹² : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>inst✝⁸ : NormedSpace 𝕜 E''<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁶ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : μ.IsAddLeftInvariant<VAR>inst✝² : μ.IsNegInvariant<VAR>inst✝¹ : MeasurableNeg G<VAR>inst✝ : MeasurableAdd G<GOAL>(g ⋆[L.flip, μ] f) x = ∫ (t : G), (L (f (x - t))) (g t) ∂μ
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>f : Ordinal.{u_2} → Ordinal.{u_2}<VAR>c : Cardinal.{u_2}<VAR>hc : c.IsRegular<VAR>hc' : c ≠ ℵ₀<VAR>hf : ∀ i < c.ord, f i < c.ord<VAR>a : Ordinal.{u_2}<GOAL>ℵ₀ < c.ord.cof
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>f : Ordinal.{u_2} → Ordinal.{u_2}<VAR>c : Cardinal.{u_2}<VAR>hc : c.IsRegular<VAR>hc' : c ≠ ℵ₀<VAR>hf : ∀ i < c.ord, f i < c.ord<VAR>a : Ordinal.{u_2}<GOAL>ℵ₀ < c
<VAR>R : Type u_1<VAR>A : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : Semiring A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : TopologicalSpace A<VAR>inst✝ : TopologicalSemiring A<GOAL>Continuous ⇑(algebraMap R A) ↔ Continuous fun p => p.1 • p.2
<VAR>R : Type u_1<VAR>A : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : Semiring A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : TopologicalSpace A<VAR>inst✝ : TopologicalSemiring A<VAR>h : Continuous ⇑(algebraMap R A)<GOAL>Continuous fun p => p.1 • p.2
<VAR>R : Type u_1<VAR>A : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : Semiring A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : TopologicalSpace A<VAR>inst✝ : TopologicalSemiring A<VAR>h : Continuous ⇑(algebraMap R A)<GOAL>Continuous fun p => (algebraMap R A) p.1 * p.2
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝³ : Monoid N<VAR>hnontriv : Nontrivial ι<VAR>G : Type u_4<VAR>inst✝² : Group G<VAR>H : ι → Type u_5<VAR>inst✝¹ : (i : ι) → Group (H i)<VAR>f : (i : ι) → H i →* G<VAR>hcard✝ : 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)<VAR>α : Type u_6<VAR>inst✝ : MulAction G α<VAR>X : ι → Set α<VAR>hXnonempty : ∀ (i : ι), (X i).Nonempty<VAR>hXdisj : Pairwise fun i j => Disjoint (X i) (X j)<VAR>hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i<VAR>i j : ι<VAR>w : NeWord H i j<VAR>hcard : 3 ≤ #(H i)<VAR>hheadtail : i ≠ j<GOAL>(lift f) w.prod ≠ 1
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝³ : Monoid N<VAR>hnontriv : Nontrivial ι<VAR>G : Type u_4<VAR>inst✝² : Group G<VAR>H : ι → Type u_5<VAR>inst✝¹ : (i : ι) → Group (H i)<VAR>f : (i : ι) → H i →* G<VAR>hcard✝ : 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)<VAR>α : Type u_6<VAR>inst✝ : MulAction G α<VAR>X : ι → Set α<VAR>hXnonempty : ∀ (i : ι), (X i).Nonempty<VAR>hXdisj : Pairwise fun i j => Disjoint (X i) (X j)<VAR>hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i<VAR>i j : ι<VAR>w : NeWord H i j<VAR>hcard : 3 ≤ #(H i)<VAR>hheadtail : i ≠ j<VAR>h : H i<VAR>hn1 : h ≠ 1<VAR>hnh : h ≠ w.head⁻¹<GOAL>(lift f) w.prod ≠ 1
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝³ : Monoid N<VAR>hnontriv : Nontrivial ι<VAR>G : Type u_4<VAR>inst✝² : Group G<VAR>H : ι → Type u_5<VAR>inst✝¹ : (i : ι) → Group (H i)<VAR>f : (i : ι) → H i →* G<VAR>hcard✝ : 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)<VAR>α : Type u_6<VAR>inst✝ : MulAction G α<VAR>X : ι → Set α<VAR>hXnonempty : ∀ (i : ι), (X i).Nonempty<VAR>hXdisj : Pairwise fun i j => Disjoint (X i) (X j)<VAR>hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i<VAR>i j : ι<VAR>w : NeWord H i j<VAR>hcard : 3 ≤ #(H i)<VAR>hheadtail : i ≠ j<VAR>h : H i<VAR>hn1 : h ≠ 1<VAR>hnh : h ≠ w.head⁻¹<VAR>hnot1 : h * w.head ≠ 1<GOAL>(lift f) w.prod ≠ 1
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝³ : Monoid N<VAR>hnontriv : Nontrivial ι<VAR>G : Type u_4<VAR>inst✝² : Group G<VAR>H : ι → Type u_5<VAR>inst✝¹ : (i : ι) → Group (H i)<VAR>f : (i : ι) → H i →* G<VAR>hcard✝ : 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)<VAR>α : Type u_6<VAR>inst✝ : MulAction G α<VAR>X : ι → Set α<VAR>hXnonempty : ∀ (i : ι), (X i).Nonempty<VAR>hXdisj : Pairwise fun i j => Disjoint (X i) (X j)<VAR>hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i<VAR>i j : ι<VAR>w : NeWord H i j<VAR>hcard : 3 ≤ #(H i)<VAR>hheadtail : i ≠ j<VAR>h : H i<VAR>hn1 : h ≠ 1<VAR>hnh : h ≠ w.head⁻¹<VAR>hnot1 : h * w.head ≠ 1<VAR>w' : NeWord H i i := (w.mulHead h hnot1).append ⋯ (NeWord.singleton h⁻¹ ⋯)<GOAL>(lift f) w.prod ≠ 1
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝³ : Monoid N<VAR>hnontriv : Nontrivial ι<VAR>G : Type u_4<VAR>inst✝² : Group G<VAR>H : ι → Type u_5<VAR>inst✝¹ : (i : ι) → Group (H i)<VAR>f : (i : ι) → H i →* G<VAR>hcard✝ : 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)<VAR>α : Type u_6<VAR>inst✝ : MulAction G α<VAR>X : ι → Set α<VAR>hXnonempty : ∀ (i : ι), (X i).Nonempty<VAR>hXdisj : Pairwise fun i j => Disjoint (X i) (X j)<VAR>hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i<VAR>i j : ι<VAR>w : NeWord H i j<VAR>hcard : 3 ≤ #(H i)<VAR>hheadtail : i ≠ j<VAR>h : H i<VAR>hn1 : h ≠ 1<VAR>hnh : h ≠ w.head⁻¹<VAR>hnot1 : h * w.head ≠ 1<VAR>w' : NeWord H i i := (w.mulHead h hnot1).append ⋯ (NeWord.singleton h⁻¹ ⋯)<VAR>hw' : (lift f) w'.prod ≠ 1<GOAL>(lift f) w.prod ≠ 1
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B : Type u_3<VAR>B' : Type u_4<VAR>inst✝³ : Category.{u_5, u_1} A<VAR>inst✝² : Category.{u_7, u_2} A'<VAR>inst✝¹ : Category.{u_6, u_3} B<VAR>inst✝ : Category.{u_8, u_4} B'<VAR>eA : A ≌ A'<VAR>eB : B ≌ B'<VAR>e' : A' ≌ B'<VAR>F : A ⥤ B'<VAR>hF : eA.functor ⋙ e'.functor ≅ F<VAR>G : B ⥤ A<VAR>hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor<VAR>X : A<GOAL>(equivalence₁ hF).unitIso.hom.app X ≫ (equivalence₁ hF).inverse.map (eB.counitIso.inv.app (F.obj X)) = (equivalence₂UnitIso eB hF).hom.app X
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>B : Type u_3<VAR>B' : Type u_4<VAR>inst✝³ : Category.{u_5, u_1} A<VAR>inst✝² : Category.{u_7, u_2} A'<VAR>inst✝¹ : Category.{u_6, u_3} B<VAR>inst✝ : Category.{u_8, u_4} B'<VAR>eA : A ≌ A'<VAR>eB : B ≌ B'<VAR>e' : A' ≌ B'<VAR>F : A ⥤ B'<VAR>hF : eA.functor ⋙ e'.functor ≅ F<VAR>G : B ⥤ A<VAR>hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor<VAR>X : A<GOAL>eA.unitIso.hom.app X ≫ eA.inverse.map (e'.unitIso.hom.app (eA.functor.obj X)) ≫ eA.inverse.map (e'.inverse.map (hF.hom.app X)) ≫ (equivalence₁ hF).inverse.map (eB.counitIso.inv.app (F.obj X)) = eA.unitIso.hom.app X ≫ eA.inverse.map (e'.unitIso.hom.app (eA.functor.obj X)) ≫ eA.inverse.map (e'.inverse.map (hF.hom.app X)) ≫ eA.inverse.map (e'.inverse.map (eB.counitIso.inv.app (F.obj X)))
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : PseudoMetricSpace α✝<VAR>inst✝³ : PseudoMetricSpace β<VAR>inst✝² : PseudoMetricSpace γ<VAR>K✝¹ : ℝ≥0<VAR>f✝ : α✝ → β<VAR>α : Type u_4<VAR>inst✝¹ : MetricSpace α<VAR>K✝ : ℝ≥0<VAR>f : α → β<VAR>inst✝ : ProperSpace α<VAR>hK : AntilipschitzWith K✝ f<VAR>f_cont : Continuous f<VAR>hf : Function.Surjective f<VAR>x₀ : β<VAR>r : ℝ<VAR>K : Set α := f ⁻¹' closedBall x₀ r<GOAL>IsCompact (closedBall x₀ r)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : PseudoMetricSpace α✝<VAR>inst✝³ : PseudoMetricSpace β<VAR>inst✝² : PseudoMetricSpace γ<VAR>K✝¹ : ℝ≥0<VAR>f✝ : α✝ → β<VAR>α : Type u_4<VAR>inst✝¹ : MetricSpace α<VAR>K✝ : ℝ≥0<VAR>f : α → β<VAR>inst✝ : ProperSpace α<VAR>hK : AntilipschitzWith K✝ f<VAR>f_cont : Continuous f<VAR>hf : Function.Surjective f<VAR>x₀ : β<VAR>r : ℝ<VAR>K : Set α := f ⁻¹' closedBall x₀ r<VAR>A : IsClosed K<GOAL>IsCompact (closedBall x₀ r)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : PseudoMetricSpace α✝<VAR>inst✝³ : PseudoMetricSpace β<VAR>inst✝² : PseudoMetricSpace γ<VAR>K✝¹ : ℝ≥0<VAR>f✝ : α✝ → β<VAR>α : Type u_4<VAR>inst✝¹ : MetricSpace α<VAR>K✝ : ℝ≥0<VAR>f : α → β<VAR>inst✝ : ProperSpace α<VAR>hK : AntilipschitzWith K✝ f<VAR>f_cont : Continuous f<VAR>hf : Function.Surjective f<VAR>x₀ : β<VAR>r : ℝ<VAR>K : Set α := f ⁻¹' closedBall x₀ r<VAR>A : IsClosed K<VAR>B : IsBounded K<GOAL>IsCompact (closedBall x₀ r)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : PseudoMetricSpace α✝<VAR>inst✝³ : PseudoMetricSpace β<VAR>inst✝² : PseudoMetricSpace γ<VAR>K✝¹ : ℝ≥0<VAR>f✝ : α✝ → β<VAR>α : Type u_4<VAR>inst✝¹ : MetricSpace α<VAR>K✝ : ℝ≥0<VAR>f : α → β<VAR>inst✝ : ProperSpace α<VAR>hK : AntilipschitzWith K✝ f<VAR>f_cont : Continuous f<VAR>hf : Function.Surjective f<VAR>x₀ : β<VAR>r : ℝ<VAR>K : Set α := f ⁻¹' closedBall x₀ r<VAR>A : IsClosed K<VAR>B : IsBounded K<VAR>this : IsCompact K<GOAL>IsCompact (closedBall x₀ r)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : PseudoMetricSpace α✝<VAR>inst✝³ : PseudoMetricSpace β<VAR>inst✝² : PseudoMetricSpace γ<VAR>K✝¹ : ℝ≥0<VAR>f✝ : α✝ → β<VAR>α : Type u_4<VAR>inst✝¹ : MetricSpace α<VAR>K✝ : ℝ≥0<VAR>f : α → β<VAR>inst✝ : ProperSpace α<VAR>hK : AntilipschitzWith K✝ f<VAR>f_cont : Continuous f<VAR>hf : Function.Surjective f<VAR>x₀ : β<VAR>r : ℝ<VAR>K : Set α := f ⁻¹' closedBall x₀ r<VAR>A : IsClosed K<VAR>B : IsBounded K<VAR>this : IsCompact K<GOAL>closedBall x₀ r = f '' K
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>hb : 0 < b<VAR>h : a / b ≤ c<GOAL>a = a / b * b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>hb : 0 < b<VAR>h : a ≤ c * b<GOAL>c * b / b = c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>hμν : μ ≤ ν<VAR>inst✝ : SigmaFinite ν<GOAL>μ.rnDeriv ν ≤ᶠ[ae ν] 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>hμν : μ ≤ ν<VAR>inst✝ : SigmaFinite ν<VAR>s : Set α<VAR>x✝¹ : MeasurableSet s<VAR>x✝ : ν s < ⊤<GOAL>∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν ≤ ∫⁻ (x : α) in s, 1 x ∂ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>hμν : μ ≤ ν<VAR>inst✝ : SigmaFinite ν<VAR>s : Set α<VAR>x✝¹ : MeasurableSet s<VAR>x✝ : ν s < ⊤<GOAL>∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν ≤ ν s
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f : F[X]<VAR>x y : F<VAR>n : ℕ<VAR>hx : x ≠ 0<GOAL>(C x * (X - C y) ^ n).natSepDegree = if n = 0 then 0 else 1
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : Ring α<VAR>inst✝ : Ring β<VAR>f : α → β<VAR>hf✝ : IsRingHom f<VAR>x y : α<VAR>hf : IsRingHom f<GOAL>f (x - y) = f x - f y
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α✝<VAR>x✝ y : α✝<VAR>inst✝² : DecidableEq α✝<VAR>inst✝¹ : Fintype α✝<VAR>α : Type u_4<VAR>inst✝ : DecidableEq α<VAR>f : Perm α<VAR>hf : f.IsCycle<VAR>x : α<VAR>hx : f x ≠ x<VAR>hffx : f (f x) ≠ x<GOAL>(swap x (f x) * f) (f x) ≠ f x
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α✝<VAR>x✝ y✝ : α✝<VAR>inst✝² : DecidableEq α✝<VAR>inst✝¹ : Fintype α✝<VAR>α : Type u_4<VAR>inst✝ : DecidableEq α<VAR>f : Perm α<VAR>hf : f.IsCycle<VAR>x : α<VAR>hx : f x ≠ x<VAR>hffx : f (f x) ≠ x<VAR>y : α<VAR>hy : (swap x (f x) * f) y ≠ y<VAR>i : ℤ<VAR>hi : (f ^ i) x = y<GOAL>(f ^ (i - 1) * f ^ 1) x = y
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R✝ : Type u_3<VAR>M✝ : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁹ : CommSemiring R✝<VAR>inst✝⁸ : AddCommMonoid M✝<VAR>inst✝⁷ : Module R✝ M✝<VAR>inst✝⁶ : AddCommMonoid N<VAR>inst✝⁵ : Module R✝ N<VAR>ι : Type u_8<VAR>inst✝⁴ : Fintype ι<VAR>v✝ : Basis ι R✝ M✝<VAR>R : Type u_9<VAR>M : Type u_10<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Invertible 2<VAR>Q : QuadraticMap R M R<VAR>v : Basis ι R M<VAR>hv₂ : LinearMap.IsOrthoᵢ (associated Q) ⇑v<VAR>w : ι → R<GOAL>(Q.basisRepr v) w = (weightedSumSquares R fun i => Q (v i)) w
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R✝ : Type u_3<VAR>M✝ : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁹ : CommSemiring R✝<VAR>inst✝⁸ : AddCommMonoid M✝<VAR>inst✝⁷ : Module R✝ M✝<VAR>inst✝⁶ : AddCommMonoid N<VAR>inst✝⁵ : Module R✝ N<VAR>ι : Type u_8<VAR>inst✝⁴ : Fintype ι<VAR>v✝ : Basis ι R✝ M✝<VAR>R : Type u_9<VAR>M : Type u_10<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Invertible 2<VAR>Q : QuadraticMap R M R<VAR>v : Basis ι R M<VAR>hv₂ : LinearMap.IsOrthoᵢ (associated Q) ⇑v<VAR>w : ι → R<GOAL>∑ x : ι, (((associatedHom R) Q) (∑ i : ι, w i • v i)) (w x • v x) = ∑ i : ι, Q (v i) • (w i * w i)
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R✝ : Type u_3<VAR>M✝ : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁹ : CommSemiring R✝<VAR>inst✝⁸ : AddCommMonoid M✝<VAR>inst✝⁷ : Module R✝ M✝<VAR>inst✝⁶ : AddCommMonoid N<VAR>inst✝⁵ : Module R✝ N<VAR>ι : Type u_8<VAR>inst✝⁴ : Fintype ι<VAR>v✝ : Basis ι R✝ M✝<VAR>R : Type u_9<VAR>M : Type u_10<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Invertible 2<VAR>Q : QuadraticMap R M R<VAR>v : Basis ι R M<VAR>hv₂ : LinearMap.IsOrthoᵢ (associated Q) ⇑v<VAR>w : ι → R<VAR>j : ι<VAR>hj : j ∈ univ<GOAL>(((associatedHom R) Q) (∑ i : ι, w i • v i)) (w j • v j) = Q (v j) • (w j * w j)
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R✝ : Type u_3<VAR>M✝ : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁹ : CommSemiring R✝<VAR>inst✝⁸ : AddCommMonoid M✝<VAR>inst✝⁷ : Module R✝ M✝<VAR>inst✝⁶ : AddCommMonoid N<VAR>inst✝⁵ : Module R✝ N<VAR>ι : Type u_8<VAR>inst✝⁴ : Fintype ι<VAR>v✝ : Basis ι R✝ M✝<VAR>R : Type u_9<VAR>M : Type u_10<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Invertible 2<VAR>Q : QuadraticMap R M R<VAR>v : Basis ι R M<VAR>hv₂ : LinearMap.IsOrthoᵢ (associated Q) ⇑v<VAR>w : ι → R<VAR>j : ι<VAR>hj : j ∈ univ<GOAL>(((associatedHom R) Q) (w j • v j)) (w j • v j) = (((associatedHom R) Q) (v j)) (v j) • (w j * w j)
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R✝ : Type u_3<VAR>M✝ : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁹ : CommSemiring R✝<VAR>inst✝⁸ : AddCommMonoid M✝<VAR>inst✝⁷ : Module R✝ M✝<VAR>inst✝⁶ : AddCommMonoid N<VAR>inst✝⁵ : Module R✝ N<VAR>ι : Type u_8<VAR>inst✝⁴ : Fintype ι<VAR>v✝ : Basis ι R✝ M✝<VAR>R : Type u_9<VAR>M : Type u_10<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Invertible 2<VAR>Q : QuadraticMap R M R<VAR>v : Basis ι R M<VAR>hv₂ : LinearMap.IsOrthoᵢ (associated Q) ⇑v<VAR>w : ι → R<VAR>j : ι<VAR>hj : j ∈ univ<GOAL>∀ b ∈ univ, b ≠ j → (((associatedHom R) Q) (w b • v b)) (w j • v j) = 0
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : SeminormedRing α✝<VAR>α : Type u_5<VAR>inst✝¹ : NormedCommRing α<VAR>inst✝ : NormOneClass α<VAR>s : Finset ι<VAR>f : ι → α<GOAL>∏ i ∈ s, ‖f i‖ = (fun a => ↑a) (∏ i ∈ s, ‖f i‖₊)
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<GOAL>bernoulli' 2 = 1 / 6
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<GOAL>1 - ∑ k ∈ range 2, ↑(Nat.choose 2 k) / (↑2 - ↑k + 1) * bernoulli' k = 1 / 6
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ι : Type u_6<VAR>f✝ : α →. β<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>x : α<GOAL>x ∈ (res f s).core t ↔ x ∈ sᶜ ∪ f ⁻¹' t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ι : Type u_6<VAR>f✝ : α →. β<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>x : α<GOAL>x ∈ s → f x ∈ t ↔ x ∈ sᶜ ∪ f ⁻¹' t
<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✝¹ : Encodable ι<VAR>inst✝ : ∀ (i : ι), SigmaFinite (μ i)<VAR>s : (i : ι) → Set (α i)<GOAL>(map (TProd.elim' ⋯) (Measure.tprod (sortedUniv ι) μ)) (univ.pi s) = ∏ i : ι, (μ i) (s i)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝⁹ : Category.{u_4, u_1} C<VAR>inst✝⁸ : Category.{u_5, u_2} D<VAR>inst✝⁷ : Category.{u_6, u_3} E<VAR>inst✝⁶ : Preadditive C<VAR>inst✝⁵ : Preadditive D<VAR>inst✝⁴ : Preadditive E<VAR>F✝ : C ⥤ D<VAR>inst✝³ : F✝.Additive<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>inst✝² : G.Additive<VAR>inst✝¹ : (F ⋙ G).Additive<VAR>inst✝ : G.Faithful<VAR>x✝¹ x✝ : C<VAR>f₁ f₂ : x✝¹ ⟶ x✝<GOAL>G.map (F.map (f₁ + f₂)) = G.map (F.map f₁ + F.map f₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : SuccOrder α<VAR>inst✝¹ : IsSuccArchimedean α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>hf : Monotone f<VAR>m n : α<GOAL>⋃ i ∈ Ico m n, Ioc (f i) (f (succ i)) = Ioc (f m) (f n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : SuccOrder α<VAR>inst✝¹ : IsSuccArchimedean α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>hf : Monotone f<VAR>m n : α<VAR>hnm : n ≤ m<GOAL>⋃ i ∈ Ico m n, Ioc (f i) (f (succ i)) = Ioc (f m) (f n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : SuccOrder α<VAR>inst✝¹ : IsSuccArchimedean α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>hf : Monotone f<VAR>m n : α<VAR>hmn : m ≤ n<GOAL>⋃ i ∈ Ico m n, Ioc (f i) (f (succ i)) = Ioc (f m) (f n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : TopologicalSpace α<VAR>f g : β → α<VAR>a b : α<VAR>s✝ : Finset β<VAR>s : Set β<GOAL>HasProd (f ∘ Subtype.val) a ↔ HasProd (s.mulIndicator f) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : TopologicalSpace β<VAR>a : α<GOAL>𝓝[≤] a ⊔ 𝓝[>] a = 𝓝 a
<VAR>α β : NonemptyFinLinOrd<VAR>e : ↑α ≃o ↑β<VAR>x : (forget NonemptyFinLinOrd).obj α<GOAL>(↑e ≫ ↑e.symm) x = (𝟙 α) x
<VAR>α β : NonemptyFinLinOrd<VAR>e : ↑α ≃o ↑β<VAR>x : (forget NonemptyFinLinOrd).obj β<GOAL>(↑e.symm ≫ ↑e) x = (𝟙 β) x
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>x : adicCompletion K v<GOAL>x ∉ adicCompletionIntegers K v ↔ 1 < Valued.v x
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>x : adicCompletion K v<GOAL>¬Valued.v x ≤ 1 ↔ 1 < Valued.v x
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → F<VAR>hP : ¬W.Nonsingular P<GOAL>toAffine W P = 0
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>s : Set α<GOAL>(boundedBy m) s = (OuterMeasure.ofFunction m m_empty) s
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>s : Set α<VAR>this : (fun s => ⨆ (_ : s.Nonempty), m s) = m<GOAL>(boundedBy m) s = (OuterMeasure.ofFunction m m_empty) s
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : NormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁴ : NormedRing E<VAR>inst✝³ : StarRing E<VAR>inst✝² : CstarRing E<VAR>inst✝¹ : NormedAlgebra 𝕜 E<VAR>inst✝ : CompleteSpace E<VAR>u : ↥(unitary E)<VAR>a✝ : Nontrivial E<GOAL>spectrum 𝕜 ↑u ⊆ Metric.sphere 0 1
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : NormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁴ : NormedRing E<VAR>inst✝³ : StarRing E<VAR>inst✝² : CstarRing E<VAR>inst✝¹ : NormedAlgebra 𝕜 E<VAR>inst✝ : CompleteSpace E<VAR>u : ↥(unitary E)<VAR>a✝ : Nontrivial E<VAR>k : 𝕜<VAR>hk : k ∈ spectrum 𝕜 ↑u<GOAL>‖k‖ ≤ 1
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : NormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁴ : NormedRing E<VAR>inst✝³ : StarRing E<VAR>inst✝² : CstarRing E<VAR>inst✝¹ : NormedAlgebra 𝕜 E<VAR>inst✝ : CompleteSpace E<VAR>u : ↥(unitary E)<VAR>a✝ : Nontrivial E<VAR>k : 𝕜<VAR>hk : k ∈ spectrum 𝕜 ↑u<GOAL>1 ≤ ‖k‖
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g✝ : α → F'<VAR>s : Set α<VAR>fs gs : ℕ → α → F'<VAR>f g : α → F'<VAR>hfs_int : ∀ (n : ℕ), Integrable (fs n) μ<VAR>hgs_int : ∀ (n : ℕ), Integrable (gs n) μ<VAR>hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => fs n x) atTop (𝓝 (f x))<VAR>hgs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => gs n x) atTop (𝓝 (g x))<VAR>bound_fs : α → ℝ<VAR>h_int_bound_fs : Integrable bound_fs μ<VAR>bound_gs : α → ℝ<VAR>h_int_bound_gs : Integrable bound_gs μ<VAR>hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x<VAR>hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x<VAR>hfg : ∀ (n : ℕ), μ[fs n|m] =ᶠ[ae μ] μ[gs n|m]<VAR>hm : m ≤ m0<VAR>hμm this : SigmaFinite (μ.trim hm)<GOAL>μ[f|m] =ᶠ[ae μ] μ[g|m]
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g✝ : α → F'<VAR>s : Set α<VAR>fs gs : ℕ → α → F'<VAR>f g : α → F'<VAR>hfs_int : ∀ (n : ℕ), Integrable (fs n) μ<VAR>hgs_int : ∀ (n : ℕ), Integrable (gs n) μ<VAR>hfs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => fs n x) atTop (𝓝 (f x))<VAR>hgs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => gs n x) atTop (𝓝 (g x))<VAR>bound_fs : α → ℝ<VAR>h_int_bound_fs : Integrable bound_fs μ<VAR>bound_gs : α → ℝ<VAR>h_int_bound_gs : Integrable bound_gs μ<VAR>hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x<VAR>hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x<VAR>hfg : ∀ (n : ℕ), μ[fs n|m] =ᶠ[ae μ] μ[gs n|m]<VAR>hm : m ≤ m0<VAR>hμm this : SigmaFinite (μ.trim hm)<GOAL>↑↑(condexpL1 hm μ g) =ᶠ[ae μ] ↑↑(condexpL1 hm μ f)