ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁵ : AddCommGroup F'<VAR>inst✝⁴ : Module 𝕜 F'<VAR>inst✝³ : TopologicalSpace F'<VAR>inst✝² : TopologicalAddGroup F'<VAR>inst✝¹ : ContinuousSMul 𝕜 F'<VAR>inst✝ : CompleteSpace 𝕜<VAR>n : ℕ<GOAL>IsOpen (⋃ i, ⋃ (_ : i.card = n), {x | LinearIndependent 𝕜 fun (x_1 : ↑↑i) => ↑x ↑x_1})
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁵ : AddCommGroup F'<VAR>inst✝⁴ : Module 𝕜 F'<VAR>inst✝³ : TopologicalSpace F'<VAR>inst✝² : TopologicalAddGroup F'<VAR>inst✝¹ : ContinuousSMul 𝕜 F'<VAR>inst✝ : CompleteSpace 𝕜<VAR>n : ℕ<VAR>t : Finset E<VAR>x✝ : t ∈ fun i => i.card = n<GOAL>IsOpen {x | LinearIndependent 𝕜 fun (x_1 : ↑↑t) => ↑x ↑x_1}
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁵ : AddCommGroup F'<VAR>inst✝⁴ : Module 𝕜 F'<VAR>inst✝³ : TopologicalSpace F'<VAR>inst✝² : TopologicalAddGroup F'<VAR>inst✝¹ : ContinuousSMul 𝕜 F'<VAR>inst✝ : CompleteSpace 𝕜<VAR>n : ℕ<VAR>t : Finset E<VAR>x✝ : t ∈ fun i => i.card = n<VAR>this : Continuous fun f x => f ↑x<GOAL>IsOpen {x | LinearIndependent 𝕜 fun (x_1 : ↑↑t) => ↑x ↑x_1}
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Ring B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : FunLike F A B<VAR>inst✝ : AlgHomClass F R A B<VAR>φ : F<VAR>a : A<VAR>r : R<VAR>h : r ∈ resolventSet R a<GOAL>r ∈ resolventSet R (φ a)
<VAR>s : ℝ<VAR>h : 0 < s<GOAL>IntegrableOn (fun x => rexp (-x) * x ^ (s - 1)) (Ioi 0) volume
<VAR>s : ℝ<VAR>h : 0 < s<GOAL>IntegrableOn (fun x => rexp (-x) * x ^ (s - 1)) (Ioc 0 1) volume ∧ IntegrableOn (fun x => rexp (-x) * x ^ (s - 1)) (Ioi 1) volume
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>m : Matrix n n R[X]<VAR>k : ℕ<VAR>i j : n<GOAL>(matPolyEquiv m).coeff k i j = (m i j).coeff k
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>m : Matrix n n R[X]<VAR>k : ℕ<VAR>i j : n<GOAL>(matPolyEquiv 0).coeff k i j = (0 i j).coeff k
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>m : Matrix n n R[X]<VAR>k : ℕ<VAR>i j : n<GOAL>∀ (p q : Matrix n n R[X]), (matPolyEquiv p).coeff k i j = (p i j).coeff k → (matPolyEquiv q).coeff k i j = (q i j).coeff k → (matPolyEquiv (p + q)).coeff k i j = ((p + q) i j).coeff k
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>m : Matrix n n R[X]<VAR>k : ℕ<VAR>i j : n<GOAL>∀ (i_1 j_1 : n) (x : R[X]), (matPolyEquiv (stdBasisMatrix i_1 j_1 x)).coeff k i j = (stdBasisMatrix i_1 j_1 x i j).coeff k
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>hXm : AEStronglyMeasurable X μ<VAR>hX : ¬Memℒp X 2 μ<GOAL>evariance X μ = ⊤
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>hXm : AEStronglyMeasurable X μ<VAR>hX : ¬Memℒp X 2 μ<VAR>h : ¬evariance X μ = ⊤<GOAL>False
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>hXm : AEStronglyMeasurable X μ<VAR>hX : ¬Memℒp X 2 μ<VAR>h : evariance X μ < ⊤<GOAL>False
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>hXm : AEStronglyMeasurable X μ<VAR>hX : ¬Memℒp X 2 μ<VAR>h : evariance X μ < ⊤<VAR>this : Memℒp (fun ω => X ω - ∫ (x : Ω), X x ∂μ) 2 μ<GOAL>False
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>hXm : AEStronglyMeasurable X μ<VAR>hX : ¬Memℒp X 2 μ<VAR>h : evariance X μ < ⊤<VAR>this : Memℒp (fun ω => X ω - ∫ (x : Ω), X x ∂μ) 2 μ<GOAL>Memℒp X 2 μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>hXm : AEStronglyMeasurable X μ<VAR>hX : ¬Memℒp X 2 μ<VAR>h : evariance X μ < ⊤<VAR>this : Memℒp (fun ω => X ω - ∫ (x : Ω), X x ∂μ) 2 μ<GOAL>X = (fun ω => X ω - ∫ (x : Ω), X x ∂μ) + fun x => ∫ (x : Ω), X x ∂μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>hXm : AEStronglyMeasurable X μ<VAR>hX : ¬Memℒp X 2 μ<VAR>h : evariance X μ < ⊤<VAR>this : Memℒp (fun ω => X ω - ∫ (x : Ω), X x ∂μ) 2 μ<VAR>ω : Ω<GOAL>X ω = ((fun ω => X ω - ∫ (x : Ω), X x ∂μ) + fun x => ∫ (x : Ω), X x ∂μ) ω
<VAR>b u v w : Ordinal.{u_1}<VAR>hb : 1 < b<VAR>hv : v ≠ 0<VAR>hvb : v < b<VAR>hw : w < b ^ u<GOAL>log b (b ^ u * v + w) = u
<VAR>b u v w : Ordinal.{u_1}<VAR>hb : 1 < b<VAR>hv : v ≠ 0<VAR>hvb : v < b<VAR>hw : w < b ^ u<VAR>hne' : b ^ u * v + w ≠ 0<GOAL>log b (b ^ u * v + w) = u
<VAR>b u v w : Ordinal.{u_1}<VAR>hb : 1 < b<VAR>hv : v ≠ 0<VAR>hvb : v < b<VAR>hw : w < b ^ u<VAR>hne' : b ^ u * v + w ≠ 0<VAR>hne : log b (b ^ u * v + w) ≠ u<GOAL>False
<VAR>b u v w : Ordinal.{u_1}<VAR>hb : 1 < b<VAR>hv : v ≠ 0<VAR>hvb : v < b<VAR>hw : w < b ^ u<VAR>hne' : b ^ u * v + w ≠ 0<VAR>hne : log b (b ^ u * v + w) ≠ u<VAR>h : log b (b ^ u * v + w) < u<GOAL>False
<VAR>b u v w : Ordinal.{u_1}<VAR>hb : 1 < b<VAR>hv : v ≠ 0<VAR>hvb : v < b<VAR>hw : w < b ^ u<VAR>hne' : b ^ u * v + w ≠ 0<VAR>hne : log b (b ^ u * v + w) ≠ u<VAR>h : log b (b ^ u * v + w) > u<GOAL>False
<VAR>R : Type uR<VAR>inst✝³ : Semiring R<VAR>S : Type uS<VAR>inst✝² : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra S A<VAR>r✝ r : R → R → Prop<VAR>x y : R<VAR>w : r x y<GOAL>(mkRingHom r) x = (mkRingHom r) y
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>α : X ≅ Y<VAR>Z : C<VAR>β : Y ≅ Z<VAR>f : Aut X<GOAL>(α ≪≫ β).conjAut f = β.conjAut (α.conjAut f)
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>inst✝⁶ : Category.{?u.67329, u_1} C<VAR>inst✝⁵ : Category.{?u.67333, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>inst✝⁴ : AddMonoid M<VAR>inst✝³ : HasShift C M<VAR>G : Type u_4<VAR>inst✝² : AddGroup G<VAR>inst✝¹ : HasShift C G<VAR>inst✝ : F.ShiftSequence M<VAR>n m mn : M<VAR>hnm : m + n = mn<VAR>a a' a'' : M<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<VAR>X : C<GOAL>mn + a = a''
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>inst✝⁶ : Category.{u_6, u_1} C<VAR>inst✝⁵ : Category.{u_5, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>inst✝⁴ : AddMonoid M<VAR>inst✝³ : HasShift C M<VAR>G : Type u_4<VAR>inst✝² : AddGroup G<VAR>inst✝¹ : HasShift C G<VAR>inst✝ : F.ShiftSequence M<VAR>n m mn : M<VAR>hnm : m + n = mn<VAR>a a' a'' : M<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<VAR>X : C<GOAL>(F.shiftIso n a a' ha').hom.app ((shiftFunctor C m).obj X) ≫ (F.shiftIso m a' a'' ha'').hom.app X = (F.shift a).map ((shiftFunctorAdd' C m n mn hnm).inv.app X) ≫ (F.shiftIso mn a a'' ⋯).hom.app X
<VAR>x y : ℂ<GOAL>sin x + sin y = 2 * sin ((x + y) / 2) * cos ((x - y) / 2)
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>e' : PartialHomeomorph Y Z<VAR>s : Set Y<VAR>hs : IsOpen s<GOAL>e.trans (ofSet s hs) = e.restr (e.source ∩ ↑e ⁻¹' s)
<VAR>N : ℕ<VAR>hN : N ≠ 0<VAR>χ : DirichletCharacter ℂ N<VAR>s : ℂ<GOAL>LSeriesSummable (fun n => χ ↑n) s ↔ 1 < s.re
<VAR>N : ℕ<VAR>hN : N ≠ 0<VAR>χ : DirichletCharacter ℂ N<VAR>s : ℂ<VAR>H : LSeriesSummable (fun n => χ ↑n) s<GOAL>1 < s.re
<VAR>N : ℕ<VAR>hN : N ≠ 0<VAR>χ : DirichletCharacter ℂ N<VAR>s : ℂ<VAR>H : LSeriesSummable (fun n => χ ↑n) s<VAR>h : s.re ≤ 1<GOAL>False
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Semiring α<VAR>inst✝ : StarRing α<VAR>M : Matrix n n α<VAR>d : ℕ<GOAL>M = (↑d)ᴴ ↔ M = ↑d
<VAR>α : Type u<VAR>a : α<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>g : G<VAR>hg : ∀ (x : G), x ∈ zpowers g<VAR>g' : G'<VAR>f₁ f₂ : G →* G'<GOAL>f₁ = f₂ ↔ f₁ g = f₂ g
<VAR>α : Type u<VAR>a : α<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>g : G<VAR>hg : ∀ (x : G), x ∈ zpowers g<VAR>g' : G'<VAR>f₁ f₂ : G →* G'<GOAL>(∀ (x : G), f₁ x = f₂ x) ↔ f₁ g = f₂ g
<VAR>α : Type u<VAR>a : α<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>g : G<VAR>hg : ∀ (x : G), x ∈ zpowers g<VAR>g' : G'<VAR>f₁ f₂ : G →* G'<VAR>H : f₁ g = f₂ g<VAR>x : G<GOAL>f₁ x = f₂ x
<VAR>α : Type u<VAR>a : α<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>g : G<VAR>hg : ∀ (x : G), x ∈ zpowers g<VAR>g' : G'<VAR>f₁ f₂ : G →* G'<VAR>H : f₁ g = f₂ g<VAR>x : G<VAR>n : ℤ<VAR>hn : g ^ n = x<GOAL>f₁ x = f₂ x
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>h : ↑|discr K| < (2 * (π / 4) ^ NrComplexPlaces K * (↑(finrank ℚ K) ^ finrank ℚ K / ↑(finrank ℚ K).factorial)) ^ 2<GOAL>IsPrincipalIdealRing (𝓞 K)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>h : ↑|discr K| < (2 * (π / 4) ^ NrComplexPlaces K * (↑(finrank ℚ K) ^ finrank ℚ K / ↑(finrank ℚ K).factorial)) ^ 2<VAR>this : 0 < finrank ℚ K<GOAL>IsPrincipalIdealRing (𝓞 K)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>h : (4 / π) ^ NrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|) < 2<VAR>this : 0 < finrank ℚ K<GOAL>IsPrincipalIdealRing (𝓞 K)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>h : (4 / π) ^ NrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|) < 2<VAR>this : 0 < finrank ℚ K<GOAL>∃ x, ∀ (y : ClassGroup (𝓞 K)), y = x
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>h : (4 / π) ^ NrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|) < 2<VAR>this : 0 < finrank ℚ K<VAR>C : ClassGroup (𝓞 K)<GOAL>C = 1
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>h : (4 / π) ^ NrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|) < 2<VAR>this : 0 < finrank ℚ K<VAR>I : ↥(Ideal (𝓞 K))⁰<VAR>hI : ↑(Ideal.absNorm ↑I) ≤ (4 / π) ^ NrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)<GOAL>ClassGroup.mk0 I = 1
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>h : (4 / π) ^ NrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|) < 2<VAR>this✝ : 0 < finrank ℚ K<VAR>I : ↥(Ideal (𝓞 K))⁰<VAR>hI : ↑(Ideal.absNorm ↑I) ≤ (4 / π) ^ NrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)<VAR>this : Ideal.absNorm ↑I = 1<GOAL>ClassGroup.mk0 I = 1
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>h : (4 / π) ^ NrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|) < 2<VAR>this✝ : 0 < finrank ℚ K<VAR>I : ↥(Ideal (𝓞 K))⁰<VAR>hI : ↑(Ideal.absNorm ↑I) ≤ (4 / π) ^ NrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)<VAR>this : Ideal.absNorm ↑I = 1<GOAL>Submodule.IsPrincipal ⊤
<VAR>α : Sort u_1<VAR>σ : α → Sort u_2<VAR>P Q R : Prop<VAR>inst✝¹ : Decidable P<VAR>inst✝ : Decidable Q<VAR>a b c : α<VAR>A : P → α<VAR>B : ¬P → α<GOAL>(∃ h, a ≠ b) ↔ ¬P ∧ a ≠ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Set α<VAR>hs : s ≠ Set.univ<VAR>f : α → ↑s<VAR>hf : Injective f<VAR>h : Fintype α<GOAL>False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹⁰ : LinearOrderedCommRing 𝕜<VAR>inst✝⁹ : LinearOrderedCommRing E<VAR>inst✝⁸ : LinearOrderedAddCommGroup F<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜 F<VAR>inst✝⁵ : Module E F<VAR>inst✝⁴ : IsScalarTower 𝕜 E F<VAR>inst✝³ : SMulCommClass 𝕜 E F<VAR>inst✝² : OrderedSMul 𝕜 E<VAR>inst✝¹ : OrderedSMul 𝕜 F<VAR>inst✝ : OrderedSMul E F<VAR>s : Set 𝕜<VAR>f : 𝕜 → E<VAR>g : 𝕜 → F<VAR>hf : ConvexOn 𝕜 s f<VAR>hg : ConvexOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x<VAR>hfg : MonovaryOn f g s<GOAL>ConvexOn 𝕜 s (f • g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹⁰ : LinearOrderedCommRing 𝕜<VAR>inst✝⁹ : LinearOrderedCommRing E<VAR>inst✝⁸ : LinearOrderedAddCommGroup F<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜 F<VAR>inst✝⁵ : Module E F<VAR>inst✝⁴ : IsScalarTower 𝕜 E F<VAR>inst✝³ : SMulCommClass 𝕜 E F<VAR>inst✝² : OrderedSMul 𝕜 E<VAR>inst✝¹ : OrderedSMul 𝕜 F<VAR>inst✝ : OrderedSMul E F<VAR>s : Set 𝕜<VAR>f : 𝕜 → E<VAR>g : 𝕜 → F<VAR>hf : ConvexOn 𝕜 s f<VAR>hg : ConvexOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x<VAR>hfg : MonovaryOn f g s<VAR>x : 𝕜<VAR>hx : x ∈ s<VAR>y : 𝕜<VAR>hy : y ∈ s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>(f • g) (a • x + b • y) ≤ a • (f • g) x + b • (f • g) y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹⁰ : LinearOrderedCommRing 𝕜<VAR>inst✝⁹ : LinearOrderedCommRing E<VAR>inst✝⁸ : LinearOrderedAddCommGroup F<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜 F<VAR>inst✝⁵ : Module E F<VAR>inst✝⁴ : IsScalarTower 𝕜 E F<VAR>inst✝³ : SMulCommClass 𝕜 E F<VAR>inst✝² : OrderedSMul 𝕜 E<VAR>inst✝¹ : OrderedSMul 𝕜 F<VAR>inst✝ : OrderedSMul E F<VAR>s : Set 𝕜<VAR>f : 𝕜 → E<VAR>g : 𝕜 → F<VAR>hf : ConvexOn 𝕜 s f<VAR>hg : ConvexOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x<VAR>hfg : MonovaryOn f g s<VAR>x : 𝕜<VAR>hx : x ∈ s<VAR>y : 𝕜<VAR>hy : y ∈ s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>f (a * x + b * y) • g (a * x + b * y) ≤ a • f x • g x + b • f y • g y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹⁰ : LinearOrderedCommRing 𝕜<VAR>inst✝⁹ : LinearOrderedCommRing E<VAR>inst✝⁸ : LinearOrderedAddCommGroup F<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜 F<VAR>inst✝⁵ : Module E F<VAR>inst✝⁴ : IsScalarTower 𝕜 E F<VAR>inst✝³ : SMulCommClass 𝕜 E F<VAR>inst✝² : OrderedSMul 𝕜 E<VAR>inst✝¹ : OrderedSMul 𝕜 F<VAR>inst✝ : OrderedSMul E F<VAR>s : Set 𝕜<VAR>f : 𝕜 → E<VAR>g : 𝕜 → F<VAR>hf : ConvexOn 𝕜 s f<VAR>hg : ConvexOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x<VAR>hfg : MonovaryOn f g s<VAR>x : 𝕜<VAR>hx : x ∈ s<VAR>y : 𝕜<VAR>hy : y ∈ s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>(a • f x + b • f y) • (a • g x + b • g y) ≤ a • f x • g x + b • f y • g y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹⁰ : LinearOrderedCommRing 𝕜<VAR>inst✝⁹ : LinearOrderedCommRing E<VAR>inst✝⁸ : LinearOrderedAddCommGroup F<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜 F<VAR>inst✝⁵ : Module E F<VAR>inst✝⁴ : IsScalarTower 𝕜 E F<VAR>inst✝³ : SMulCommClass 𝕜 E F<VAR>inst✝² : OrderedSMul 𝕜 E<VAR>inst✝¹ : OrderedSMul 𝕜 F<VAR>inst✝ : OrderedSMul E F<VAR>s : Set 𝕜<VAR>f : 𝕜 → E<VAR>g : 𝕜 → F<VAR>hf : ConvexOn 𝕜 s f<VAR>hg : ConvexOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x<VAR>hfg : MonovaryOn f g s<VAR>x : 𝕜<VAR>hx : x ∈ s<VAR>y : 𝕜<VAR>hy : y ∈ s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>(a • f x + b • f y) • (a • g x + b • g y) = (a * a) • f x • g x + (b * b) • f y • g y + (a * b) • (f x • g y + f y • g x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹⁰ : LinearOrderedCommRing 𝕜<VAR>inst✝⁹ : LinearOrderedCommRing E<VAR>inst✝⁸ : LinearOrderedAddCommGroup F<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜 F<VAR>inst✝⁵ : Module E F<VAR>inst✝⁴ : IsScalarTower 𝕜 E F<VAR>inst✝³ : SMulCommClass 𝕜 E F<VAR>inst✝² : OrderedSMul 𝕜 E<VAR>inst✝¹ : OrderedSMul 𝕜 F<VAR>inst✝ : OrderedSMul E F<VAR>s : Set 𝕜<VAR>f : 𝕜 → E<VAR>g : 𝕜 → F<VAR>hf : ConvexOn 𝕜 s f<VAR>hg : ConvexOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x<VAR>hfg : MonovaryOn f g s<VAR>x : 𝕜<VAR>hx : x ∈ s<VAR>y : 𝕜<VAR>hy : y ∈ s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>(a • f x) • a • g x + (b • f y) • a • g x + ((a • f x) • b • g y + (b • f y) • b • g y) = (a * a) • f x • g x + (b * b) • f y • g y + ((a * b) • f x • g y + (a * b) • f y • g x)
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>π₁ π₂ : TaggedPrepartition I<VAR>h₁ : π₁.IsPartition<VAR>h₂ : π₂.IsPartition<GOAL>integralSum f vol π₁ - integralSum f vol π₂ = ∑ J ∈ (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes, ((vol J) (f ((π₁.infPrepartition π₂.toPrepartition).tag J)) - (vol J) (f ((π₂.infPrepartition π₁.toPrepartition).tag J)))
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>π₁ π₂ : TaggedPrepartition I<VAR>h₁ : π₁.IsPartition<VAR>h₂ : π₂.IsPartition<GOAL>∑ J ∈ (π₁.infPrepartition π₂.toPrepartition).boxes, (vol J) (f ((π₁.infPrepartition π₂.toPrepartition).tag J)) - ∑ J ∈ (π₂.infPrepartition π₁.toPrepartition).boxes, (vol J) (f ((π₂.infPrepartition π₁.toPrepartition).tag J)) = ∑ x ∈ (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes, (vol x) (f ((π₁.infPrepartition π₂.toPrepartition).tag x)) - ∑ x ∈ (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes, (vol x) (f ((π₂.infPrepartition π₁.toPrepartition).tag x))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>φ : α → β<VAR>θ : α → γ<VAR>ψ : β → δ<VAR>ρ : γ → δ<VAR>H : ψ ∘ φ = ρ ∘ θ<VAR>F : Filter α<GOAL>map ψ (map φ F) = map ρ (map θ F)
<VAR>k G✝ : Type u<VAR>inst✝⁴ : CommRing k<VAR>inst✝³ : Group G✝<VAR>A : Rep k G✝<VAR>G M : Type<VAR>inst✝² : Group G<VAR>inst✝¹ : CommGroup M<VAR>inst✝ : MulDistribMulAction G M<VAR>f : ↥(oneCoboundaries (Rep.ofMulDistribMulAction G M))<GOAL>IsMulOneCoboundary (⇑Additive.ofMul ∘ ↑↑f)
<VAR>k G✝ : Type u<VAR>inst✝⁴ : CommRing k<VAR>inst✝³ : Group G✝<VAR>A : Rep k G✝<VAR>G M : Type<VAR>inst✝² : Group G<VAR>inst✝¹ : CommGroup M<VAR>inst✝ : MulDistribMulAction G M<VAR>f : ↥(oneCoboundaries (Rep.ofMulDistribMulAction G M))<VAR>x : CoeSort.coe (Rep.ofMulDistribMulAction G M)<VAR>hx : (dZero (Rep.ofMulDistribMulAction G M)) x = ↑↑f<GOAL>IsMulOneCoboundary (⇑Additive.ofMul ∘ ↑↑f)
<VAR>d : ℤ<VAR>a : Solution₁ d<VAR>hax : 0 < a.x<VAR>hay : 0 < a.y<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>0 < (a ^ n).y
<VAR>d : ℤ<VAR>a : Solution₁ d<VAR>hax : 0 < a.x<VAR>hay : 0 < a.y<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>0 < (a ^ n.pred.succ).y
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>hST : IsComplement S T<VAR>hHT : IsComplement (↑H) T<VAR>hSK : IsComplement S ↑K<VAR>g : G<VAR>k : ↥K<GOAL>hSK.equiv (g * ↑k) = ((hSK.equiv g).1, (hSK.equiv g).2 * k)
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>hST : IsComplement S T<VAR>hHT : IsComplement (↑H) T<VAR>hSK : IsComplement S ↑K<VAR>g : G<VAR>k : ↥K<VAR>this : (hSK.equiv (g * ↑k)).1 = (hSK.equiv g).1<GOAL>hSK.equiv (g * ↑k) = ((hSK.equiv g).1, (hSK.equiv g).2 * k)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a✝ b : α<VAR>hst : { ofColex := s } ≤ { ofColex := t }<VAR>hts : { ofColex := t } ≤ { ofColex := s }<VAR>a : α<VAR>has : a ∈ s<GOAL>a ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a✝ b : α<VAR>hst : { ofColex := s } ≤ { ofColex := t }<VAR>hts : { ofColex := t } ≤ { ofColex := s }<VAR>a : α<VAR>has : a ∈ s<VAR>hat : a ∉ t<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a✝ b : α<VAR>hst : { ofColex := s } ≤ { ofColex := t }<VAR>hts : { ofColex := t } ≤ { ofColex := s }<VAR>a : α<VAR>has : a ∈ s<VAR>hat : a ∉ t<VAR>_b : α<VAR>hb₁ : _b ∈ s<VAR>hb₂ : _b ∉ s<VAR>right✝ : a ≤ _b<GOAL>False
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>w x y z : P<VAR>h₁ : Wbtw R w x z<VAR>h₂ : Wbtw R x y z<GOAL>Wbtw R w x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>w x y z : P<VAR>h₁ : Wbtw R z x w<VAR>h₂ : Wbtw R z y x<GOAL>Wbtw R y x w
<VAR>A : Type u_1<VAR>B✝ : Type u_2<VAR>inst✝⁴ : Field A<VAR>inst✝³ : Ring B✝<VAR>inst✝² : Algebra A B✝<VAR>x✝ : B✝<VAR>B : Type u_3<VAR>inst✝¹ : CommRing B<VAR>inst✝ : Algebra A B<VAR>x : B<VAR>hx : IsIntegral A x<VAR>a : A<GOAL>minpoly A (x + (algebraMap A B) a) = (minpoly A x).comp (X - C a)
<VAR>A : Type u_1<VAR>B✝ : Type u_2<VAR>inst✝⁴ : Field A<VAR>inst✝³ : Ring B✝<VAR>inst✝² : Algebra A B✝<VAR>x✝ : B✝<VAR>B : Type u_3<VAR>inst✝¹ : CommRing B<VAR>inst✝ : Algebra A B<VAR>x : B<VAR>hx : IsIntegral A x<VAR>a : A<GOAL>(Polynomial.aeval (x + (algebraMap A B) a)) ((minpoly A x).comp (X - C a)) = 0
<VAR>A : Type u_1<VAR>B✝ : Type u_2<VAR>inst✝⁴ : Field A<VAR>inst✝³ : Ring B✝<VAR>inst✝² : Algebra A B✝<VAR>x✝ : B✝<VAR>B : Type u_3<VAR>inst✝¹ : CommRing B<VAR>inst✝ : Algebra A B<VAR>x : B<VAR>hx : IsIntegral A x<VAR>a : A<VAR>q : A[X]<VAR>qmo : q.Monic<VAR>hq : (Polynomial.aeval (x + (algebraMap A B) a)) q = 0<GOAL>((minpoly A x).comp (X - C a)).degree ≤ q.degree
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝¹¹ : Group G<VAR>inst✝¹⁰ : Group H<VAR>inst✝⁹ : MulAction G α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : MulAction H β<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>s t✝ : Set α<VAR>μ : Measure α<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : MeasurableSMul G α<VAR>inst✝² : SMulInvariantMeasure G α μ<VAR>inst✝¹ : Countable G<VAR>ν : Measure α<VAR>inst✝ : Finite G<VAR>h : IsFundamentalDomain G s μ<VAR>t : Set α<VAR>ht : ∀ (g : G), g • t =ᶠ[ae μ] t<VAR>this : Fintype G<GOAL>μ t = Nat.card G • μ (t ∩ s)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝¹¹ : Group G<VAR>inst✝¹⁰ : Group H<VAR>inst✝⁹ : MulAction G α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : MulAction H β<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>s t✝ : Set α<VAR>μ : Measure α<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : MeasurableSMul G α<VAR>inst✝² : SMulInvariantMeasure G α μ<VAR>inst✝¹ : Countable G<VAR>ν : Measure α<VAR>inst✝ : Finite G<VAR>h : IsFundamentalDomain G s μ<VAR>t : Set α<VAR>ht : ∀ (g : G), g • t =ᶠ[ae μ] t<VAR>this : Fintype G<GOAL>∑' (g : G), μ (g • t ∩ s) = Nat.card G • μ (t ∩ s)