ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : LinearOrderedField α<VAR>inst✝² : ConditionallyCompleteLinearOrderedField β<VAR>inst✝¹ : ConditionallyCompleteLinearOrderedField γ<VAR>inst✝ : Archimedean α<VAR>q : ℚ<VAR>x : β<VAR>h : x ∈ cutMap β ↑q<GOAL>x ≤ ↑q
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : LinearOrderedField α<VAR>inst✝² : ConditionallyCompleteLinearOrderedField β<VAR>inst✝¹ : ConditionallyCompleteLinearOrderedField γ<VAR>inst✝ : Archimedean α<VAR>q : ℚ<VAR>w : β<VAR>h : w < ↑q<GOAL>∃ a ∈ cutMap β ↑q, w < a
<VAR>G : Type u<VAR>M : Type v<VAR>α : Type w<VAR>s✝ : Set α<VAR>m : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace G<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>μ : Measure α<VAR>inst✝ : SMulInvariantMeasure G α μ<VAR>c : G<VAR>s : Set α<GOAL>s ∈ c • ae μ ↔ s ∈ ae μ
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁴ : EuclideanDomain R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : IsDomain S<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : Field L<VAR>inst✝⁹ : Algebra R K<VAR>inst✝⁸ : IsFractionRing R K<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : FiniteDimensional K L<VAR>inst✝⁵ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>bS : Basis ι R S<GOAL>0 < normBound abv bS
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁴ : EuclideanDomain R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : IsDomain S<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : Field L<VAR>inst✝⁹ : Algebra R K<VAR>inst✝⁸ : IsFractionRing R K<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : FiniteDimensional K L<VAR>inst✝⁵ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>bS : Basis ι R S<VAR>i j k : ι<VAR>hijk : (Algebra.leftMulMatrix bS) (bS i) j k ≠ 0<GOAL>0 < normBound abv bS
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁴ : EuclideanDomain R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : IsDomain S<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : Field L<VAR>inst✝⁹ : Algebra R K<VAR>inst✝⁸ : IsFractionRing R K<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : FiniteDimensional K L<VAR>inst✝⁵ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>bS : Basis ι R S<VAR>i j k : ι<VAR>hijk : (Algebra.leftMulMatrix bS) (bS i) j k ≠ 0<GOAL>0 < ↑(Fintype.card ι).factorial * (↑(Fintype.card ι) * (Finset.image (fun ijk => abv ((Algebra.leftMulMatrix bS) (bS ijk.1) ijk.2.1 ijk.2.2)) Finset.univ).max' ⋯) ^ Fintype.card ι
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁴ : EuclideanDomain R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : IsDomain S<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : Field L<VAR>inst✝⁹ : Algebra R K<VAR>inst✝⁸ : IsFractionRing R K<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : FiniteDimensional K L<VAR>inst✝⁵ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>bS : Basis ι R S<VAR>i j k : ι<VAR>hijk : (Algebra.leftMulMatrix bS) (bS i) j k ≠ 0<GOAL>0 < (↑(Fintype.card ι) * (Finset.image (fun ijk => abv ((Algebra.leftMulMatrix bS) (bS ijk.1) ijk.2.1 ijk.2.2)) Finset.univ).max' ⋯) ^ Fintype.card ι
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁴ : EuclideanDomain R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : IsDomain S<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : Field L<VAR>inst✝⁹ : Algebra R K<VAR>inst✝⁸ : IsFractionRing R K<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : FiniteDimensional K L<VAR>inst✝⁵ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>bS : Basis ι R S<VAR>i j k : ι<VAR>hijk : (Algebra.leftMulMatrix bS) (bS i) j k ≠ 0<GOAL>0 < (Finset.image (fun ijk => abv ((Algebra.leftMulMatrix bS) (bS ijk.1) ijk.2.1 ijk.2.2)) Finset.univ).max' ⋯
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁴ : EuclideanDomain R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : IsDomain S<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : Field L<VAR>inst✝⁹ : Algebra R K<VAR>inst✝⁸ : IsFractionRing R K<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : FiniteDimensional K L<VAR>inst✝⁵ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>bS : Basis ι R S<VAR>i j k : ι<VAR>hijk : (Algebra.leftMulMatrix bS) (bS i) j k ≠ 0<GOAL>abv ((Algebra.leftMulMatrix bS) (bS i) j k) ∈ Finset.image (fun ijk => abv ((Algebra.leftMulMatrix bS) (bS ijk.1) ijk.2.1 ijk.2.2)) Finset.univ
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L : Filter 𝕜<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>derivWithin (fun y => -f y) s x = -derivWithin f s x
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>x : CliffordAlgebra Q<GOAL>(reverse ∘ₗ involute.toLinearMap) x = (involute.toLinearMap ∘ₗ reverse) x
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>x : CliffordAlgebra Q<GOAL>reverse (involute x) = involute (reverse x)
<VAR>R : Type u_1<VAR>σ : Type u_2<VAR>inst✝ : CommRing R<VAR>r : R<VAR>I : Ideal R<VAR>i : R<VAR>hi : i ∈ I<GOAL>((Ideal.Quotient.mk (Ideal.map C I)).comp C) i = 0
<VAR>R : Type u_1<VAR>σ : Type u_2<VAR>inst✝ : CommRing R<VAR>r : R<VAR>I : Ideal R<VAR>i : R<VAR>hi : i ∈ I<GOAL>C i ∈ Ideal.map C I
<VAR>p : ℕ<VAR>inst✝¹¹ : Fact (Nat.Prime p)<VAR>R : Type u₁<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : CharP R p<VAR>P✝ : Type u₃<VAR>inst✝⁸ : CommSemiring P✝<VAR>inst✝⁷ : CharP P✝ p<VAR>inst✝⁶ : PerfectRing P✝ p<VAR>inst✝⁵ : PerfectRing R p<VAR>S : Type u₂<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : CharP S p<VAR>P : Type u₃<VAR>inst✝² : CommSemiring P<VAR>inst✝¹ : CharP P p<VAR>inst✝ : PerfectRing P p<VAR>π : P →+* S<VAR>m : PerfectionMap p π<VAR>f : R →+* S<GOAL>(fun f => π.comp f) ((fun f => (↑m.equiv.symm).comp ((Perfection.lift p R S) f)) f) = f
<VAR>p : ℕ<VAR>inst✝¹¹ : Fact (Nat.Prime p)<VAR>R : Type u₁<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : CharP R p<VAR>P✝ : Type u₃<VAR>inst✝⁸ : CommSemiring P✝<VAR>inst✝⁷ : CharP P✝ p<VAR>inst✝⁶ : PerfectRing P✝ p<VAR>inst✝⁵ : PerfectRing R p<VAR>S : Type u₂<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : CharP S p<VAR>P : Type u₃<VAR>inst✝² : CommSemiring P<VAR>inst✝¹ : CharP P p<VAR>inst✝ : PerfectRing P p<VAR>π : P →+* S<VAR>m : PerfectionMap p π<VAR>f : R →+* S<GOAL>(Perfection.coeff S p 0).comp ((Perfection.lift p R S) f) = f
<VAR>p : ℕ<VAR>inst✝¹¹ : Fact (Nat.Prime p)<VAR>R : Type u₁<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : CharP R p<VAR>P✝ : Type u₃<VAR>inst✝⁸ : CommSemiring P✝<VAR>inst✝⁷ : CharP P✝ p<VAR>inst✝⁶ : PerfectRing P✝ p<VAR>inst✝⁵ : PerfectRing R p<VAR>S : Type u₂<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : CharP S p<VAR>P : Type u₃<VAR>inst✝² : CommSemiring P<VAR>inst✝¹ : CharP P p<VAR>inst✝ : PerfectRing P p<VAR>π : P →+* S<VAR>m : PerfectionMap p π<VAR>f : R →+* P<GOAL>(fun f => (↑m.equiv.symm).comp ((Perfection.lift p R S) f)) ((fun f => π.comp f) f) = f
<VAR>M : Type u_1<VAR>inst✝ : NonAssocSemiring M<VAR>n : ℕ<VAR>x✝ : M<GOAL>↑n * x✝ = x✝ * ↑n
<VAR>M : Type u_1<VAR>inst✝ : NonAssocSemiring M<VAR>n : ℕ<VAR>x✝¹ x✝ : M<GOAL>↑n * (x✝¹ * x✝) = ↑n * x✝¹ * x✝
<VAR>M : Type u_1<VAR>inst✝ : NonAssocSemiring M<VAR>n : ℕ<VAR>x✝¹ x✝ : M<GOAL>x✝¹ * ↑n * x✝ = x✝¹ * (↑n * x✝)
<VAR>M : Type u_1<VAR>inst✝ : NonAssocSemiring M<VAR>n : ℕ<VAR>x✝¹ x✝ : M<GOAL>x✝¹ * x✝ * ↑n = x✝¹ * (x✝ * ↑n)
<VAR>h : Decidable (Dom 1)<GOAL>toWithTop 1 = 1
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x : (P F).W α<GOAL>WEquiv x x
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x : (P F).W α<GOAL>∀ (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (f : (P F).last.B a → (P F).W α), WEquiv ((P F).wMk a f' f) ((P F).wMk a f' f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>G : Type u_7<VAR>inst✝ : NormedLatticeAddCommGroup G<VAR>g : α →ₛ G<VAR>hp : AEEqFun.mk ↑g ⋯ ∈ Lp G p μ<VAR>hf : 0 ≤ᶠ[ae μ] ↑g<GOAL>∃ f', 0 ≤ f' ∧ ↑↑↑⟨⟨AEEqFun.mk ↑g ⋯, hp⟩, ⋯⟩ =ᶠ[ae μ] ↑f'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>G : Type u_7<VAR>inst✝ : NormedLatticeAddCommGroup G<VAR>g : α →ₛ G<VAR>hp : AEEqFun.mk ↑g ⋯ ∈ Lp G p μ<VAR>hf : 0 ≤ᶠ[ae μ] ↑g<GOAL>↑g =ᶠ[ae μ] ↑(g ⊔ 0)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>c x y : P<VAR>R : ℝ<VAR>hR : R ≠ 0<VAR>hx : x ≠ c<VAR>hy : y ≠ c<GOAL>inversion c R x ∈ perpBisector c (inversion c R y) ↔ dist x y = dist y c
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>c x y : P<VAR>R : ℝ<VAR>hR : R ≠ 0<VAR>hx : x ≠ c<VAR>hy : y ≠ c<GOAL>R ^ 2 / dist x c = R ^ 2 / (dist x c * dist y c) * dist x y ↔ dist x y = dist y c
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>c x y : P<VAR>R : ℝ<VAR>hR : R ≠ 0<VAR>hx : x ≠ c<VAR>hy : y ≠ c<VAR>hx' : dist x c ≠ 0<GOAL>R ^ 2 / dist x c = R ^ 2 / (dist x c * dist y c) * dist x y ↔ dist x y = dist y c
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>c x y : P<VAR>R : ℝ<VAR>hR : R ≠ 0<VAR>hx : x ≠ c<VAR>hy : y ≠ c<VAR>hx' : dist x c ≠ 0<VAR>hy' : dist y c ≠ 0<GOAL>R ^ 2 / dist x c = R ^ 2 / (dist x c * dist y c) * dist x y ↔ dist x y = dist y c
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : _root_.RCLike 𝕜<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>c : Core 𝕜 F<VAR>x : F<GOAL>im ⟪x, x⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : _root_.RCLike 𝕜<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>c : Core 𝕜 F<VAR>x : F<GOAL>I * ((starRingEnd 𝕜) ⟪x, x⟫_𝕜 - ⟪x, x⟫_𝕜) / 2 = ↑0
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹³ : Ring R<VAR>inst✝¹² : StrongRankCondition R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>inst✝⁹ : Free R M<VAR>inst✝⁸ : AddCommGroup M'<VAR>inst✝⁷ : Module R M'<VAR>inst✝⁶ : Free R M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Free R M₁<VAR>W : Type v<VAR>inst✝² : AddCommGroup W<VAR>inst✝¹ : Module R W<VAR>inst✝ : Free R W<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hVW : Module.rank R M = n • Module.rank R W<GOAL>Finite R M ↔ Finite R W
<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>X Y : C<VAR>i : IsIso 0<GOAL>𝟙 X = 0 ∧ 𝟙 Y = 0
<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>X Y : C<VAR>i : IsIso 0<GOAL>0 ≫ inv 0 = 0 ∧ 𝟙 Y = 0
<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>X Y : C<VAR>i : IsIso 0<GOAL>0 ≫ inv 0 = 0 ∧ inv 0 ≫ 0 = 0
<VAR>a b : ℝ<VAR>nb ne : ℕ<VAR>pb : IsInt b (Int.negOfNat nb)<VAR>pe' : IsNat (a ^ Int.negOfNat nb) ne<GOAL>IsNat (a ^ b) ne
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ t : Set α<VAR>inst✝ : Countable ι<VAR>s : ι → Set α<VAR>h : ∀ (i : ι), NullMeasurableSet (s i) μ<VAR>hd : Pairwise (AEDisjoint μ on s)<GOAL>∃ t, (∀ (i : ι), t i ⊆ s i) ∧ (∀ (i : ι), s i =ᶠ[ae μ] t i) ∧ (∀ (i : ι), MeasurableSet (t i)) ∧ Pairwise (Disjoint on t)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ t✝ : Set α<VAR>inst✝ : Countable ι<VAR>s : ι → Set α<VAR>h : ∀ (i : ι), NullMeasurableSet (s i) μ<VAR>hd : Pairwise (AEDisjoint μ on s)<VAR>t : ι → Set α<VAR>ht_sub : ∀ (i : ι), t i ⊆ s i<VAR>htm : ∀ (i : ι), MeasurableSet (t i)<VAR>ht_eq : ∀ (i : ι), t i =ᶠ[ae μ] s i<GOAL>∃ t, (∀ (i : ι), t i ⊆ s i) ∧ (∀ (i : ι), s i =ᶠ[ae μ] t i) ∧ (∀ (i : ι), MeasurableSet (t i)) ∧ Pairwise (Disjoint on t)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ t✝ : Set α<VAR>inst✝ : Countable ι<VAR>s : ι → Set α<VAR>h : ∀ (i : ι), NullMeasurableSet (s i) μ<VAR>hd : Pairwise (AEDisjoint μ on s)<VAR>t : ι → Set α<VAR>ht_sub : ∀ (i : ι), t i ⊆ s i<VAR>htm : ∀ (i : ι), MeasurableSet (t i)<VAR>ht_eq : ∀ (i : ι), t i =ᶠ[ae μ] s i<VAR>u : ι → Set α<VAR>hum : ∀ (i : ι), MeasurableSet (u i)<VAR>hu₀ : ∀ (i : ι), μ (u i) = 0<VAR>hud : Pairwise (Disjoint on fun i => s i \ u i)<GOAL>∃ t, (∀ (i : ι), t i ⊆ s i) ∧ (∀ (i : ι), s i =ᶠ[ae μ] t i) ∧ (∀ (i : ι), MeasurableSet (t i)) ∧ Pairwise (Disjoint on t)
<VAR>G : Type u_1<VAR>inst✝¹ : CommGroup G<VAR>inst✝ : Group.FG G<GOAL>Nat.card G ∣ Monoid.exponent G ^ Group.rank G
<VAR>G : Type u_1<VAR>inst✝¹ : CommGroup G<VAR>inst✝ : Group.FG G<VAR>S : Finset G<VAR>hS1 : S.card = Group.rank G<VAR>hS2 : closure ↑S = ⊤<GOAL>Nat.card G ∣ Monoid.exponent G ^ Group.rank G
<VAR>G : Type u_1<VAR>inst✝¹ : CommGroup G<VAR>inst✝ : Group.FG G<VAR>S : Finset G<VAR>hS1 : S.card = Group.rank G<VAR>hS2 : closure ↑S = ⊤<GOAL>Nat.card G ∣ ∏ _x : { x // x ∈ S }, Monoid.exponent G
<VAR>G : Type u_1<VAR>inst✝¹ : CommGroup G<VAR>inst✝ : Group.FG G<VAR>S : Finset G<VAR>hS1 : S.card = Group.rank G<VAR>hS2 : closure ↑S = ⊤<VAR>f : ((g : { x // x ∈ S }) → ↥(zpowers ↑g)) →* G := noncommPiCoprod ⋯<GOAL>Nat.card G ∣ ∏ _x : { x // x ∈ S }, Monoid.exponent G
<VAR>G : Type u_1<VAR>inst✝¹ : CommGroup G<VAR>inst✝ : Group.FG G<VAR>S : Finset G<VAR>hS1 : S.card = Group.rank G<VAR>hS2 : closure ↑S = ⊤<VAR>f : ((g : { x // x ∈ S }) → ↥(zpowers ↑g)) →* G := noncommPiCoprod ⋯<VAR>hf : Function.Surjective ⇑f<GOAL>Nat.card G ∣ ∏ _x : { x // x ∈ S }, Monoid.exponent G
<VAR>G : Type u_1<VAR>inst✝¹ : CommGroup G<VAR>inst✝ : Group.FG G<VAR>S : Finset G<VAR>hS1 : S.card = Group.rank G<VAR>hS2 : closure ↑S = ⊤<VAR>f : ((g : { x // x ∈ S }) → ↥(zpowers ↑g)) →* G := noncommPiCoprod ⋯<VAR>hf : Nat.card G ∣ Nat.card ((g : { x // x ∈ S }) → ↥(zpowers ↑g))<GOAL>Nat.card G ∣ ∏ _x : { x // x ∈ S }, Monoid.exponent G
<VAR>G : Type u_1<VAR>inst✝¹ : CommGroup G<VAR>inst✝ : Group.FG G<VAR>S : Finset G<VAR>hS1 : S.card = Group.rank G<VAR>hS2 : closure ↑S = ⊤<VAR>f : ((g : { x // x ∈ S }) → ↥(zpowers ↑g)) →* G := noncommPiCoprod ⋯<VAR>hf : Nat.card G ∣ ∏ a : { x // x ∈ S }, Nat.card ↥(zpowers ↑a)<GOAL>Nat.card G ∣ ∏ _x : { x // x ∈ S }, Monoid.exponent G
<VAR>G : Type u_1<VAR>inst✝¹ : CommGroup G<VAR>inst✝ : Group.FG G<VAR>S : Finset G<VAR>hS1 : S.card = Group.rank G<VAR>hS2 : closure ↑S = ⊤<VAR>f : ((g : { x // x ∈ S }) → ↥(zpowers ↑g)) →* G := noncommPiCoprod ⋯<VAR>hf : Nat.card G ∣ ∏ a : { x // x ∈ S }, Nat.card ↥(zpowers ↑a)<VAR>g : { x // x ∈ S }<VAR>x✝ : g ∈ Finset.univ<GOAL>Nat.card ↥(zpowers ↑g) ∣ Monoid.exponent G
<VAR>G : Type u_1<VAR>inst✝¹ : CommGroup G<VAR>inst✝ : Group.FG G<VAR>S : Finset G<VAR>hS1 : S.card = Group.rank G<VAR>hS2 : closure ↑S = ⊤<VAR>f : ((g : { x // x ∈ S }) → ↥(zpowers ↑g)) →* G := noncommPiCoprod ⋯<VAR>hf : Nat.card G ∣ ∏ a : { x // x ∈ S }, Nat.card ↥(zpowers ↑a)<VAR>g : { x // x ∈ S }<VAR>x✝ : g ∈ Finset.univ<GOAL>orderOf ↑g ∣ Monoid.exponent G
<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>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁸ : DecidableEq α'<VAR>inst✝⁷ : DecidableEq β'<VAR>inst✝⁶ : DecidableEq γ<VAR>inst✝⁵ : DecidableEq γ'<VAR>inst✝⁴ : DecidableEq δ<VAR>inst✝³ : DecidableEq δ'<VAR>inst✝² : DecidableEq ε<VAR>inst✝¹ : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>inst✝ : DecidableEq β<GOAL>image2 f (↑s) (↑t ∪ ↑t') = image2 f ↑s ↑t ∪ image2 f ↑s ↑t'
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : Affine R<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>x y : R<GOAL>-f y - (map W f).toAffine.a₁ * f x - (map W f).toAffine.a₃ = f (-y - W.a₁ * x - W.a₃)
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{?u.146934, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₁.LeftHomologyData<VAR>inst✝² : Epi φ.τ₁<VAR>inst✝¹ : IsIso φ.τ₂<VAR>inst✝ : Mono φ.τ₃<VAR>i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂<GOAL>S₂.LeftHomologyData
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{?u.146934, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₁.LeftHomologyData<VAR>inst✝² : Epi φ.τ₁<VAR>inst✝¹ : IsIso φ.τ₂<VAR>inst✝ : Mono φ.τ₃<VAR>i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂<VAR>wi : i ≫ S₂.g = 0<GOAL>S₂.LeftHomologyData
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{?u.146934, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₁.LeftHomologyData<VAR>inst✝² : Epi φ.τ₁<VAR>inst✝¹ : IsIso φ.τ₂<VAR>inst✝ : Mono φ.τ₃<VAR>i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂<VAR>wi : i ≫ S₂.g = 0<VAR>hi : IsLimit (KernelFork.ofι i wi)<GOAL>S₂.LeftHomologyData
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{?u.146934, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₁.LeftHomologyData<VAR>inst✝² : Epi φ.τ₁<VAR>inst✝¹ : IsIso φ.τ₂<VAR>inst✝ : Mono φ.τ₃<VAR>i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂<VAR>wi : i ≫ S₂.g = 0<VAR>hi : IsLimit (KernelFork.ofι i wi)<VAR>f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)<GOAL>S₂.LeftHomologyData
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{?u.146934, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₁.LeftHomologyData<VAR>inst✝² : Epi φ.τ₁<VAR>inst✝¹ : IsIso φ.τ₂<VAR>inst✝ : Mono φ.τ₃<VAR>i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂<VAR>wi : i ≫ S₂.g = 0<VAR>hi : IsLimit (KernelFork.ofι i wi)<VAR>f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)<VAR>hf' : φ.τ₁ ≫ f' = h.f'<GOAL>S₂.LeftHomologyData
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{?u.146934, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₁.LeftHomologyData<VAR>inst✝² : Epi φ.τ₁<VAR>inst✝¹ : IsIso φ.τ₂<VAR>inst✝ : Mono φ.τ₃<VAR>i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂<VAR>wi : i ≫ S₂.g = 0<VAR>hi : IsLimit (KernelFork.ofι i wi)<VAR>f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)<VAR>hf' : φ.τ₁ ≫ f' = h.f'<VAR>wπ : f' ≫ h.π = 0<GOAL>S₂.LeftHomologyData
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{?u.146934, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₁.LeftHomologyData<VAR>inst✝² : Epi φ.τ₁<VAR>inst✝¹ : IsIso φ.τ₂<VAR>inst✝ : Mono φ.τ₃<VAR>i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂<VAR>wi : i ≫ S₂.g = 0<VAR>hi : IsLimit (KernelFork.ofι i wi)<VAR>f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)<VAR>hf' : φ.τ₁ ≫ f' = h.f'<VAR>wπ : f' ≫ h.π = 0<VAR>hπ : IsColimit (CokernelCofork.ofπ h.π wπ)<GOAL>S₂.LeftHomologyData
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s t : Finset ι<VAR>i j : ι<VAR>v r r' : ι → F<VAR>hvs : Set.InjOn v ↑s<GOAL>((interpolate s v) r).degree ≤ ↑(s.card - 1)
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s t : Finset ι<VAR>i j : ι<VAR>v r r' : ι → F<VAR>hvs : Set.InjOn v ↑s<GOAL>(s.sup fun b => (C (r b) * Lagrange.basis s v b).degree) ≤ ↑(s.card - 1)
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s t : Finset ι<VAR>i j : ι<VAR>v r r' : ι → F<VAR>hvs : Set.InjOn v ↑s<GOAL>∀ b ∈ s, (C (r b) * Lagrange.basis s v b).degree ≤ ↑(s.card - 1)
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s t : Finset ι<VAR>i✝ j : ι<VAR>v r r' : ι → F<VAR>hvs : Set.InjOn v ↑s<VAR>i : ι<VAR>hi : i ∈ s<GOAL>(C (r i) * Lagrange.basis s v i).degree ≤ ↑(s.card - 1)
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s t : Finset ι<VAR>i✝ j : ι<VAR>v r r' : ι → F<VAR>hvs : Set.InjOn v ↑s<VAR>i : ι<VAR>hi : i ∈ s<GOAL>(C (r i)).degree + ↑(s.card - 1) ≤ ↑(s.card - 1)
<VAR>α : Type u_1<VAR>inst✝¹ : Lattice α<VAR>inst✝ : Group α<VAR>a✝ b a : α<GOAL>mabs a⁻¹ = mabs a
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>inst✝ : DecidableEq α<VAR>f g : Π₀ (_a : α), ℕ<GOAL>toMultiset f < toMultiset g ↔ f < g
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : Fintype ι'<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module ℝ F<VAR>v : ι → E<GOAL>parallelepiped v = (convexHull ℝ) (∑ i : ι, {0, v i})
<VAR>G : Type u_1<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : SFinite μ<VAR>s : Set G<VAR>inst✝² : MeasurableInv G<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : ν.IsMulLeftInvariant<VAR>hν : ν ≠ 0<GOAL>μ ≪ ν
<VAR>G : Type u_1<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : SFinite μ<VAR>s✝ : Set G<VAR>inst✝² : MeasurableInv G<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : ν.IsMulLeftInvariant<VAR>hν : ν ≠ 0<VAR>s : Set G<VAR>sm : MeasurableSet s<VAR>hνs : ν s = 0<GOAL>μ s = 0
<VAR>G : Type u_1<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : SFinite μ<VAR>s✝ : Set G<VAR>inst✝² : MeasurableInv G<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : ν.IsMulLeftInvariant<VAR>hν : ν ≠ 0<VAR>s : Set G<VAR>sm : MeasurableSet s<VAR>hνs : ν s = 0<VAR>h1 : μ s * ∫⁻ (y : G), 1 y ∂ν = ∫⁻ (x : G), ν ((fun z => z * x) ⁻¹' s) * 1 x⁻¹ ∂μ<GOAL>μ s = 0
<VAR>G : Type u_1<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : SFinite μ<VAR>s✝ : Set G<VAR>inst✝² : MeasurableInv G<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : ν.IsMulLeftInvariant<VAR>hν : ν ≠ 0<VAR>s : Set G<VAR>sm : MeasurableSet s<VAR>hνs : ν s = 0<VAR>h1 : μ s = 0<GOAL>μ s = 0