ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : Ring 𝕜<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module 𝕜 V<VAR>inst✝¹ : TopologicalSpace P<VAR>inst✝ : AddTorsor V P<VAR>s✝ t : Set P<VAR>x : P<VAR>s : Set P<GOAL>IsClosed (Subtype.val ⁻¹' intrinsicClosure 𝕜 s)
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : Ring 𝕜<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module 𝕜 V<VAR>inst✝¹ : TopologicalSpace P<VAR>inst✝ : AddTorsor V P<VAR>s✝ t✝ : Set P<VAR>x : P<VAR>s : Set P<VAR>t : AffineSubspace 𝕜 P<VAR>ht : t = affineSpan 𝕜 (intrinsicClosure 𝕜 s)<GOAL>IsClosed (Subtype.val ⁻¹' intrinsicClosure 𝕜 s)
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : Ring 𝕜<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module 𝕜 V<VAR>inst✝¹ : TopologicalSpace P<VAR>inst✝ : AddTorsor V P<VAR>s✝ t : Set P<VAR>x : P<VAR>s : Set P<VAR>ht : affineSpan 𝕜 s = affineSpan 𝕜 (intrinsicClosure 𝕜 s)<GOAL>IsClosed (Subtype.val ⁻¹' intrinsicClosure 𝕜 s)
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : Ring 𝕜<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module 𝕜 V<VAR>inst✝¹ : TopologicalSpace P<VAR>inst✝ : AddTorsor V P<VAR>s✝ t : Set P<VAR>x : P<VAR>s : Set P<VAR>ht : affineSpan 𝕜 s = affineSpan 𝕜 (intrinsicClosure 𝕜 s)<GOAL>IsClosed (closure (Subtype.val ⁻¹' s))
<VAR>t t' : Type u → Type u<VAR>eqv : (α : Type u) → t α ≃ t' α<VAR>inst✝⁵ : Traversable t<VAR>inst✝⁴ : LawfulTraversable t<VAR>F G : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : Applicative G<VAR>inst✝¹ : LawfulApplicative F<VAR>inst✝ : LawfulApplicative G<VAR>η : ApplicativeTransformation F G<VAR>α β γ : Type u<VAR>f : α → β<VAR>x : t' α<GOAL>Equiv.traverse eqv (pure ∘ f) x = pure (Equiv.map eqv f x)
<VAR>t t' : Type u → Type u<VAR>eqv : (α : Type u) → t α ≃ t' α<VAR>inst✝⁵ : Traversable t<VAR>inst✝⁴ : LawfulTraversable t<VAR>F G : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : Applicative G<VAR>inst✝¹ : LawfulApplicative F<VAR>inst✝ : LawfulApplicative G<VAR>η : ApplicativeTransformation F G<VAR>α β γ : Type u<VAR>f : α → β<VAR>x : t' α<GOAL>(eqv β) (id.mk (f <$> (eqv α).symm x)) = Equiv.map eqv f x
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>M N : Matrix m m R<GOAL>(M * N).det = (N * M).det
<VAR>α : Type u<VAR>l✝ l' l : List α<GOAL>l ∈ l.cyclicPermutations
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>f : LocallyConstant X Y<VAR>R : Type u_3<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : Semiring Y<VAR>inst✝¹ : Algebra R Y<VAR>inst✝ : TopologicalSemiring Y<VAR>r : R<VAR>x : X<GOAL>((↑↑{ toFun := toContinuousMap, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }).toFun ((algebraMap R (LocallyConstant X Y)) r)) x = ((algebraMap R C(X, Y)) r) x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.17959, u_1} C<VAR>inst✝ : Category.{?u.17963, u_2} D<VAR>F : C ⥤ Cat<VAR>X : Grothendieck F<GOAL>(F.map (𝟙 X).base).obj X.fiber = X.fiber
<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝ : CommMonoid α<VAR>k p : ℕ<VAR>f : ℕ → α<VAR>h : Prime p<GOAL>∏ x ∈ (p ^ k).divisors, f x = ∏ x ∈ range (k + 1), f (p ^ x)
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<GOAL>ContDiff 𝕜 0 f ↔ Continuous f
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<GOAL>ContDiffOn 𝕜 0 f univ ↔ ContinuousOn f univ
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>f : ℝ → E<VAR>c ca cb : E<VAR>l l' la la' lb lb' : Filter ℝ<VAR>lt : Filter ι<VAR>a b z : ℝ<VAR>u v ua ub va vb : ι → ℝ<VAR>inst✝³ : FTCFilter a la la'<VAR>inst✝² : FTCFilter b lb lb'<VAR>hf : IntervalIntegrable f volume a b<VAR>s t : Set ℝ<VAR>inst✝¹ : FTCFilter a (𝓝[s] a) la<VAR>inst✝ : FTCFilter b (𝓝[t] b) lb<VAR>hmeas_a : StronglyMeasurableAtFilter f la volume<VAR>hmeas_b : StronglyMeasurableAtFilter f lb volume<VAR>ha : Tendsto f (la ⊓ ae volume) (𝓝 ca)<VAR>hb : Tendsto f (lb ⊓ ae volume) (𝓝 cb)<GOAL>HasFDerivWithinAt (fun p => ∫ (x : ℝ) in p.1 ..p.2, f x) ((snd ℝ ℝ ℝ).smulRight cb - (fst ℝ ℝ ℝ).smulRight ca) (s ×ˢ t) (a, b)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>f : ℝ → E<VAR>c ca cb : E<VAR>l l' la la' lb lb' : Filter ℝ<VAR>lt : Filter ι<VAR>a b z : ℝ<VAR>u v ua ub va vb : ι → ℝ<VAR>inst✝³ : FTCFilter a la la'<VAR>inst✝² : FTCFilter b lb lb'<VAR>hf : IntervalIntegrable f volume a b<VAR>s t : Set ℝ<VAR>inst✝¹ : FTCFilter a (𝓝[s] a) la<VAR>inst✝ : FTCFilter b (𝓝[t] b) lb<VAR>hmeas_a : StronglyMeasurableAtFilter f la volume<VAR>hmeas_b : StronglyMeasurableAtFilter f lb volume<VAR>ha : Tendsto f (la ⊓ ae volume) (𝓝 ca)<VAR>hb : Tendsto f (lb ⊓ ae volume) (𝓝 cb)<GOAL>HasFDerivAtFilter (fun p => ∫ (x : ℝ) in p.1 ..p.2, f x) ((snd ℝ ℝ ℝ).smulRight cb - (fst ℝ ℝ ℝ).smulRight ca) (a, b) (𝓝[s] a ×ˢ 𝓝[t] b)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>f : ℝ → E<VAR>c ca cb : E<VAR>l l' la la' lb lb' : Filter ℝ<VAR>lt : Filter ι<VAR>a b z : ℝ<VAR>u v ua ub va vb : ι → ℝ<VAR>inst✝³ : FTCFilter a la la'<VAR>inst✝² : FTCFilter b lb lb'<VAR>hf : IntervalIntegrable f volume a b<VAR>s t : Set ℝ<VAR>inst✝¹ : FTCFilter a (𝓝[s] a) la<VAR>inst✝ : FTCFilter b (𝓝[t] b) lb<VAR>hmeas_a : StronglyMeasurableAtFilter f la volume<VAR>hmeas_b : StronglyMeasurableAtFilter f lb volume<VAR>ha : Tendsto f (la ⊓ ae volume) (𝓝 ca)<VAR>hb : Tendsto f (lb ⊓ ae volume) (𝓝 cb)<VAR>this : (fun t => ((∫ (x : ℝ) in t.1 ..t.2, f x) - ∫ (x : ℝ) in a..b, f x) - ((t.2 - b) • cb - (t.1 - a) • ca)) =o[𝓝[s] a ×ˢ 𝓝[t] b] fun t => ‖t.1 - a‖ + ‖t.2 - b‖<GOAL>HasFDerivAtFilter (fun p => ∫ (x : ℝ) in p.1 ..p.2, f x) ((snd ℝ ℝ ℝ).smulRight cb - (fst ℝ ℝ ℝ).smulRight ca) (a, b) (𝓝[s] a ×ˢ 𝓝[t] b)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>f : ℝ → E<VAR>c ca cb : E<VAR>l l' la la' lb lb' : Filter ℝ<VAR>lt : Filter ι<VAR>a b z : ℝ<VAR>u v ua ub va vb : ι → ℝ<VAR>inst✝³ : FTCFilter a la la'<VAR>inst✝² : FTCFilter b lb lb'<VAR>hf : IntervalIntegrable f volume a b<VAR>s t : Set ℝ<VAR>inst✝¹ : FTCFilter a (𝓝[s] a) la<VAR>inst✝ : FTCFilter b (𝓝[t] b) lb<VAR>hmeas_a : StronglyMeasurableAtFilter f la volume<VAR>hmeas_b : StronglyMeasurableAtFilter f lb volume<VAR>ha : Tendsto f (la ⊓ ae volume) (𝓝 ca)<VAR>hb : Tendsto f (lb ⊓ ae volume) (𝓝 cb)<VAR>this : (fun t => ((∫ (x : ℝ) in t.1 ..t.2, f x) - ∫ (x : ℝ) in a..b, f x) - ((t.2 - b) • cb - (t.1 - a) • ca)) =o[𝓝[s] a ×ˢ 𝓝[t] b] fun t => ‖t.1 - a‖ + ‖t.2 - b‖<GOAL>∀ (x : ℝ × ℝ), ((∫ (x : ℝ) in x.1 ..x.2, f x) - ∫ (x : ℝ) in a..b, f x) - ((x.2 - b) • cb - (x.1 - a) • ca) = ((∫ (x : ℝ) in x.1 ..x.2, f x) - ∫ (x : ℝ) in (a, b).1 ..(a, b).2, f x) - ((snd ℝ ℝ ℝ).smulRight cb - (fst ℝ ℝ ℝ).smulRight ca) (x - (a, b))
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>f : ℝ → E<VAR>c ca cb : E<VAR>l l' la la' lb lb' : Filter ℝ<VAR>lt : Filter ι<VAR>a b z : ℝ<VAR>u v ua ub va vb : ι → ℝ<VAR>inst✝³ : FTCFilter a la la'<VAR>inst✝² : FTCFilter b lb lb'<VAR>hf : IntervalIntegrable f volume a b<VAR>s t : Set ℝ<VAR>inst✝¹ : FTCFilter a (𝓝[s] a) la<VAR>inst✝ : FTCFilter b (𝓝[t] b) lb<VAR>hmeas_a : StronglyMeasurableAtFilter f la volume<VAR>hmeas_b : StronglyMeasurableAtFilter f lb volume<VAR>ha : Tendsto f (la ⊓ ae volume) (𝓝 ca)<VAR>hb : Tendsto f (lb ⊓ ae volume) (𝓝 cb)<VAR>this : (fun t => ((∫ (x : ℝ) in t.1 ..t.2, f x) - ∫ (x : ℝ) in a..b, f x) - ((t.2 - b) • cb - (t.1 - a) • ca)) =o[𝓝[s] a ×ˢ 𝓝[t] b] fun t => ‖t.1 - a‖ + ‖t.2 - b‖<GOAL>(fun t => ‖t.1 - a‖ + ‖t.2 - b‖) =O[𝓝[s] a ×ˢ 𝓝[t] b] fun x' => x' - (a, b)
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>s : Multiset R<GOAL>(map (fun r => X + C r) s).prod = ∑ j ∈ Finset.range (card s + 1), C (s.esymm j) * X ^ (card s - j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r p q : α → α → Prop<VAR>f g : ι → α<VAR>s t u : Set α<VAR>a b : α<GOAL>(insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, a ≠ b → r a b ∧ r b a
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : IsFiniteMeasure μ<VAR>c : F<VAR>hc_ne_zero : c ≠ 0<VAR>hq_ne_zero : q ≠ 0<GOAL>eLpNorm' (fun x => c) q μ = ↑‖c‖₊ * μ Set.univ ^ (1 / q)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : IsFiniteMeasure μ<VAR>c : F<VAR>hc_ne_zero : c ≠ 0<VAR>hq_ne_zero : q ≠ 0<GOAL>(↑‖c‖₊ ^ q) ^ (1 / q) * μ Set.univ ^ (1 / q) = ↑‖c‖₊ * μ Set.univ ^ (1 / q)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : IsFiniteMeasure μ<VAR>c : F<VAR>hc_ne_zero : c ≠ 0<VAR>hq_ne_zero : q ≠ 0<GOAL>↑‖c‖₊ ^ q ≠ ⊤
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.55203, u_1} C<VAR>inst✝ : Abelian C<VAR>X✝ Y✝ Z✝ : SimplicialObject C<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<GOAL>{ obj := obj, map := fun {X Y} f => map f }.map (f ≫ g) = { obj := obj, map := fun {X Y} f => map f }.map f ≫ { obj := obj, map := fun {X Y} f => map f }.map g
<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 a₁ a₂ : α<VAR>g : γ → β<VAR>f : β → α<VAR>hg : Injective g<GOAL>∏' (x : ↑(Set.range g)), f ↑x = ∏' (x : γ), f (g x)
<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 a₁ a₂ : α<VAR>g : γ → β<VAR>f : β → α<VAR>hg : Injective g<GOAL>∏' (x : ↑Set.univ), f (g ↑x) = ∏' (x : γ), f (g x)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P : Cubic R<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>φ : R →+* S<VAR>inst✝ : IsDomain S<GOAL>(map φ P).roots = (Polynomial.map φ P.toPoly).roots
<VAR>a b : ℤ<GOAL>Fintype.card ↑(Set.Icc a b) = (b + 1 - a).toNat
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : OrderedSMul α β<VAR>s : Finset ι<VAR>σ : Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : MonovaryOn f g ↑s<VAR>hσ : {x | σ x ≠ x} ⊆ ↑s<GOAL>∑ i ∈ s, f (σ i) • g i ≤ ∑ i ∈ s, f i • g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : OrderedSMul α β<VAR>s : Finset ι<VAR>σ : Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : MonovaryOn f g ↑s<VAR>hσ : {x | σ x ≠ x} ⊆ ↑s<GOAL>∑ i ∈ s, f (σ i) • g i = ∑ i ∈ s, f i • g (σ⁻¹ i)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>la : Filter α<VAR>lb : Filter β<VAR>f : α → Filter β<GOAL>Tendsto f la (𝓝 lb) ↔ ∀ s ∈ lb, ∀ᶠ (a : α) in la, s ∈ f a
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : CosimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 3)<VAR>j : Fin (n + 2)<VAR>H : i ≤ j.castSucc<GOAL>X.map (SimplexCategory.δ (i.castLT ⋯)) ≫ X.map (SimplexCategory.δ j.succ) = X.map (SimplexCategory.δ j) ≫ X.map (SimplexCategory.δ i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : NormedDivisionRing α<VAR>inst✝² : SeminormedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : BoundedSMul α β<VAR>s : α<VAR>x y : β<GOAL>edist (s • x) (s • y) = ‖s‖₊ • edist x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>ε : ℝ≥0∞<GOAL>ε * μ {x | ε ≤ f x} ≤ ∫⁻ (a : α), f a ∂μ
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>ι' : Type x'<VAR>inst✝³ : Semiring R<VAR>φ : ι → Type u_1<VAR>inst✝² : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝¹ : (i : ι) → Module R (φ i)<VAR>I : Set ι<VAR>p✝ q : (i : ι) → Submodule R (φ i)<VAR>x✝ : (i : ι) → φ i<VAR>inst✝ : DecidableEq ι<VAR>p : (i : ι) → Submodule R (φ i)<VAR>i : ι<VAR>x : φ i<VAR>hx : x ∈ p i<GOAL>x ∈ comap (single i) (pi Set.univ p)
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>ι' : Type x'<VAR>inst✝³ : Semiring R<VAR>φ : ι → Type u_1<VAR>inst✝² : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝¹ : (i : ι) → Module R (φ i)<VAR>I : Set ι<VAR>p✝ q : (i : ι) → Submodule R (φ i)<VAR>x✝ : (i : ι) → φ i<VAR>inst✝ : DecidableEq ι<VAR>p : (i : ι) → Submodule R (φ i)<VAR>i : ι<VAR>x : φ i<VAR>hx : x ∈ p i<GOAL>∀ i_1 ∈ Set.univ, (single i) x i_1 ∈ p i_1
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup E<VAR>hm : m ≤ m0<VAR>f : α → E<VAR>hf : StronglyMeasurable f<GOAL>∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ.trim hm = ∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup E<VAR>hm : m ≤ m0<VAR>f : α → E<VAR>hf : StronglyMeasurable f<GOAL>Measurable fun a => ↑‖f a‖₊ ^ q
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup E<VAR>hm : m ≤ m0<VAR>f : α → E<VAR>hf : StronglyMeasurable f<GOAL>Measurable fun a => ‖f a‖₊
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup E<VAR>hm : m ≤ m0<VAR>f : α → E<VAR>hf : StronglyMeasurable f<GOAL>StronglyMeasurable fun a => ‖f a‖₊
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hI : ¬M.Indep I<GOAL>M.Indep (insert e I) ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.closure I)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → α<VAR>g : ℕ → α → α<VAR>H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))<VAR>n k : ℕ<GOAL>Semiconj f^[n] (g k) (g (n + k))
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>x✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SMulInvariantMeasure G α μ<VAR>x y : G<VAR>s : Set α<VAR>hs : x • s =ᶠ[ae μ] s<VAR>hy : y ∈ Subgroup.zpowers x<GOAL>y • s =ᶠ[ae μ] s
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>x✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SMulInvariantMeasure G α μ<VAR>x y : G<VAR>s : Set α<VAR>hs : Subgroup.zpowers x ≤ MulAction.aestabilizer G μ s<VAR>hy : y ∈ Subgroup.zpowers x<GOAL>y • s =ᶠ[ae μ] s
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>x✝ : ↑(ModuleCat.of ℤ (LocallyConstant ↑(π C fun x => ord I x < o) ℤ))<GOAL>(ModuleCat.ofHom (πs C o) ≫ ModuleCat.ofHom (Linear_CC' C hsC ho)) x✝ = 0 x✝
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<GOAL>(ShortComplex.mk (ModuleCat.ofHom (πs C o)) (ModuleCat.ofHom (Linear_CC' C hsC ho)) ⋯).Exact
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<GOAL>∀ (x₂ : ↑(ShortComplex.mk (ModuleCat.ofHom (πs C o)) (ModuleCat.ofHom (Linear_CC' C hsC ho)) ⋯).X₂), (ShortComplex.mk (ModuleCat.ofHom (πs C o)) (ModuleCat.ofHom (Linear_CC' C hsC ho)) ⋯).g x₂ = 0 → ∃ x₁, (ShortComplex.mk (ModuleCat.ofHom (πs C o)) (ModuleCat.ofHom (Linear_CC' C hsC ho)) ⋯).f x₁ = x₂
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>f : ↑(ShortComplex.mk (ModuleCat.ofHom (πs C o)) (ModuleCat.ofHom (Linear_CC' C hsC ho)) ⋯).X₂<GOAL>(ShortComplex.mk (ModuleCat.ofHom (πs C o)) (ModuleCat.ofHom (Linear_CC' C hsC ho)) ⋯).g f = 0 → ∃ x₁, (ShortComplex.mk (ModuleCat.ofHom (πs C o)) (ModuleCat.ofHom (Linear_CC' C hsC ho)) ⋯).f x₁ = f
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H K : Subgroup G<VAR>ι : Sort u_5<VAR>S : ι → Subgroup G<VAR>x : G<GOAL>x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
<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>hPz : P z ≠ 0<GOAL>W.negY P / P z ^ 3 = W.toAffine.negY (P x / P z ^ 2) (P y / P z ^ 3)
<VAR>α : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p : Associates α<VAR>hp : ¬Irreducible p<VAR>s : FactorSet α<VAR>h : p ∈ s<GOAL>False
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>φ : R⟦X⟧<GOAL>(coeff R (n + 1)) (φ * X) = (coeff R n) φ
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>φ : R⟦X⟧<GOAL>(MvPowerSeries.coeff R (single () n + single () 1)) (φ * X) = (MvPowerSeries.coeff R (single () n)) φ
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>φ : R⟦X⟧<GOAL>(MvPowerSeries.coeff R (single () n)) φ = (MvPowerSeries.coeff R (single () n)) φ * 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t u : Set α<VAR>π : δ → Type u_6<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : (a : δ) → MeasurableSpace (π a)<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : DecidableEq δ<VAR>s : Finset δ<VAR>x : (i : δ) → π i<GOAL>Measurable (updateFinset x s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t u : Set α<VAR>π : δ → Type u_6<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : (a : δ) → MeasurableSpace (π a)<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : DecidableEq δ<VAR>s : Finset δ<VAR>x : (i : δ) → π i<GOAL>∀ (a : δ), Measurable fun x_1 => if hi : a ∈ s then x_1 ⟨a, hi⟩ else x a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t u : Set α<VAR>π : δ → Type u_6<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : (a : δ) → MeasurableSpace (π a)<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : DecidableEq δ<VAR>s : Finset δ<VAR>x : (i : δ) → π i<VAR>i : δ<GOAL>Measurable fun x_1 => if hi : i ∈ s then x_1 ⟨i, hi⟩ else x i
<VAR>d : ℤ<VAR>a₁ : Solution₁ d<VAR>h : IsFundamental a₁<VAR>a : Solution₁ d<VAR>hax : 1 < a.x<VAR>hay : 0 < a.y<GOAL>a.x * a₁.y ≤ a.y * a₁.x
<VAR>d : ℤ<VAR>a₁ : Solution₁ d<VAR>h : IsFundamental a₁<VAR>a : Solution₁ d<VAR>hax : 1 < a.x<VAR>hay : 0 < a.y<GOAL>0 ≤ a.y ^ 2 * (1 + d * a₁.y ^ 2) - (1 + d * a.y ^ 2) * a₁.y ^ 2
<VAR>d : ℤ<VAR>a₁ : Solution₁ d<VAR>h : IsFundamental a₁<VAR>a : Solution₁ d<VAR>hax : 1 < a.x<VAR>hay : 0 < a.y<GOAL>0 ≤ a.y ^ 2 - a₁.y ^ 2
<VAR>d : ℤ<VAR>a₁ : Solution₁ d<VAR>h : IsFundamental a₁<VAR>a : Solution₁ d<VAR>hax : 1 < a.x<VAR>hay : 0 < a.y<GOAL>a₁.y ≤ a.y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a : Ordinal.{u_4}<GOAL>0 • a = a * ↑0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>n : ℕ<VAR>a : Ordinal.{u_4}<GOAL>(n + 1) • a = a * ↑(n + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>n : ℕ<GOAL>0 ∉ map { toFun := succ, inj' := ⋯ } univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>n : ℕ<GOAL>univ = Finset.cons 0 (map { toFun := succ, inj' := ⋯ } univ) ⋯
<VAR>R✝ : Type u<VAR>inst✝¹¹ : CommRing R✝<VAR>W✝ : Affine R✝<VAR>R : Type r<VAR>inst✝¹⁰ : CommRing R<VAR>W : Affine R<VAR>S : Type s<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra S A<VAR>inst✝⁴ : IsScalarTower R S A<VAR>B : Type v<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra S B<VAR>inst✝ : IsScalarTower R S B<VAR>f : A →ₐ[S] B<GOAL>(baseChange W B).toAffine.polynomialX = Polynomial.map (mapRingHom ↑f) (baseChange W A).toAffine.polynomialX
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>w₁ : InfinitePlace K<VAR>B : ℕ<VAR>hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B<GOAL>Submodule.span ℝ ↑(unitLattice K) = ⊤
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>w₁ : InfinitePlace K<VAR>B : ℕ<VAR>hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B<GOAL>⊤ ≤ Submodule.span ℝ ↑(unitLattice K)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>w₁ : InfinitePlace K<VAR>B✝ : ℕ<VAR>hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B✝<VAR>B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }<GOAL>⊤ ≤ Submodule.span ℝ ↑(unitLattice K)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>w₁ : InfinitePlace K<VAR>B✝ : ℕ<VAR>hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B✝<VAR>B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }<VAR>v : { w // w ≠ w₀ } → { w // w ≠ w₀ } → ℝ := fun w => (logEmbedding K) ⋯.choose<GOAL>⊤ ≤ Submodule.span ℝ ↑(unitLattice K)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>w₁ : InfinitePlace K<VAR>B✝ : ℕ<VAR>hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B✝<VAR>B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }<VAR>v : { w // w ≠ w₀ } → { w // w ≠ w₀ } → ℝ := fun w => (logEmbedding K) ⋯.choose<GOAL>B.det v ≠ 0
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>w₁ : InfinitePlace K<VAR>B✝ : ℕ<VAR>hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B✝<VAR>B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }<VAR>v : { w // w ≠ w₀ } → { w // w ≠ w₀ } → ℝ := fun w => (logEmbedding K) ⋯.choose<GOAL>(B.toMatrix v).det ≠ 0
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>w₁ : InfinitePlace K<VAR>B✝ : ℕ<VAR>hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B✝<VAR>B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }<VAR>v : { w // w ≠ w₀ } → { w // w ≠ w₀ } → ℝ := fun w => (logEmbedding K) ⋯.choose<VAR>w : { w // w ≠ w₀ }<GOAL>∑ i ∈ univ.erase w, ‖B.toMatrix v i w‖ < ‖B.toMatrix v w w‖