ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing A'<VAR>inst✝³ : CommRing A''<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R A''<VAR>a b : R<VAR>hx : AlgebraicIndependent R x<GOAL>Injective ⇑(Finsupp.total ι A R x)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing A'<VAR>inst✝³ : CommRing A''<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R A''<VAR>a b : R<VAR>hx : AlgebraicIndependent R x<VAR>this : Finsupp.total ι A R x = (aeval x).toLinearMap ∘ₗ Finsupp.total ι (MvPolynomial ι R) R X<GOAL>Injective ⇑((aeval x).toLinearMap ∘ₗ Finsupp.total ι (MvPolynomial ι R) R X)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing A'<VAR>inst✝³ : CommRing A''<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R A''<VAR>a b : R<VAR>hx : AlgebraicIndependent R x<VAR>this : Finsupp.total ι A R x = (aeval x).toLinearMap ∘ₗ Finsupp.total ι (MvPolynomial ι R) R X<GOAL>Injective ⇑(Finsupp.total ι (MvPolynomial ι R) R X)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing A'<VAR>inst✝³ : CommRing A''<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R A''<VAR>a b : R<VAR>hx : AlgebraicIndependent R x<VAR>this : Finsupp.total ι A R x = (aeval x).toLinearMap ∘ₗ Finsupp.total ι (MvPolynomial ι R) R X<GOAL>LinearIndependent R X
<VAR>k : ℤ<VAR>N : ℕ<VAR>hk : 3 ≤ k<VAR>a : Fin 2 → ZMod N<VAR>τ : ℍ<GOAL>MDifferentiableAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (⇑(eisensteinSeries_SIF a k)) τ
<VAR>k : ℤ<VAR>N : ℕ<VAR>hk : 3 ≤ k<VAR>a : Fin 2 → ZMod N<VAR>τ : ℍ<GOAL>DifferentiableAt ℂ (⇑(eisensteinSeries_SIF a k) ∘ ↑ofComplex) ↑τ
<VAR>k : ℤ<VAR>N : ℕ<VAR>hk : 3 ≤ k<VAR>a : Fin 2 → ZMod N<VAR>τ : ℍ<GOAL>DifferentiableOn ℂ (⇑(eisensteinSeries_SIF a k) ∘ ↑ofComplex) {b | 0 < b.im}
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : SetLike σ M<VAR>inst✝¹ : AddSubmonoidClass σ M<VAR>ℳ : ι → σ<VAR>inst✝ : Decomposition ℳ<VAR>p : M → Prop<VAR>h_zero : p 0<VAR>h_homogeneous : ∀ {i : ι} (m : ↥(ℳ i)), p ↑m<VAR>h_add : ∀ (m m' : M), p m → p m' → p (m + m')<GOAL>∀ (m : M), p m
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : SetLike σ M<VAR>inst✝¹ : AddSubmonoidClass σ M<VAR>ℳ : ι → σ<VAR>inst✝ : Decomposition ℳ<VAR>p : M → Prop<VAR>h_zero : p 0<VAR>h_homogeneous : ∀ {i : ι} (m : ↥(ℳ i)), p ↑m<VAR>h_add : ∀ (m m' : M), p m → p m' → p (m + m')<VAR>ℳ' : ι → AddSubmonoid M := fun i => { carrier := ↑(ℳ i), add_mem' := ⋯, zero_mem' := ⋯ }<GOAL>∀ (m : M), p m
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : SetLike σ M<VAR>inst✝¹ : AddSubmonoidClass σ M<VAR>ℳ : ι → σ<VAR>inst✝ : Decomposition ℳ<VAR>p : M → Prop<VAR>h_zero : p 0<VAR>h_homogeneous : ∀ {i : ι} (m : ↥(ℳ i)), p ↑m<VAR>h_add : ∀ (m m' : M), p m → p m' → p (m + m')<VAR>ℳ' : ι → AddSubmonoid M := fun i => { carrier := ↑(ℳ i), add_mem' := ⋯, zero_mem' := ⋯ }<VAR>t : Decomposition ℳ'<GOAL>∀ (m : M), p m
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : SetLike σ M<VAR>inst✝¹ : AddSubmonoidClass σ M<VAR>ℳ : ι → σ<VAR>inst✝ : Decomposition ℳ<VAR>p : M → Prop<VAR>h_zero : p 0<VAR>h_homogeneous : ∀ {i : ι} (m : ↥(ℳ i)), p ↑m<VAR>h_add : ∀ (m m' : M), p m → p m' → p (m + m')<VAR>ℳ' : ι → AddSubmonoid M := fun i => { carrier := ↑(ℳ i), add_mem' := ⋯, zero_mem' := ⋯ }<VAR>t : Decomposition ℳ'<VAR>mem : ∀ (m : M), m ∈ iSup ℳ'<GOAL>∀ (m : M), p m
<VAR>C : Type u'<VAR>inst✝⁴ : Category.{v', u'} C<VAR>J : GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>inst✝³ : Presheaf.IsLocallyInjective J α<VAR>inst✝² : Presheaf.IsLocallySurjective J α<VAR>inst✝¹ : J.WEqualsLocallyBijective AddCommGrp<VAR>inst✝ : HasWeakSheafify J AddCommGrp<VAR>P : PresheafOfModules R₀<VAR>F : SheafOfModules R<VAR>g : P ⟶ (restrictScalars α).obj ((SheafOfModules.forget R).obj F)<GOAL>(SheafOfModules.toSheaf R).map ((sheafificationHomEquiv α).symm g) = ((sheafificationAdjunction J AddCommGrp).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F)).symm g.hom
<VAR>C : Type u'<VAR>inst✝⁴ : Category.{v', u'} C<VAR>J : GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>inst✝³ : Presheaf.IsLocallyInjective J α<VAR>inst✝² : Presheaf.IsLocallySurjective J α<VAR>inst✝¹ : J.WEqualsLocallyBijective AddCommGrp<VAR>inst✝ : HasWeakSheafify J AddCommGrp<VAR>P : PresheafOfModules R₀<VAR>F : SheafOfModules R<VAR>f : (sheafification α).obj P ⟶ F<GOAL>(SheafOfModules.toSheaf R).map ((sheafificationHomEquiv α).symm ((sheafificationHomEquiv α) f)) = ((sheafificationAdjunction J AddCommGrp).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F)).symm ((sheafificationHomEquiv α) f).hom
<VAR>C : Type u'<VAR>inst✝⁴ : Category.{v', u'} C<VAR>J : GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>inst✝³ : Presheaf.IsLocallyInjective J α<VAR>inst✝² : Presheaf.IsLocallySurjective J α<VAR>inst✝¹ : J.WEqualsLocallyBijective AddCommGrp<VAR>inst✝ : HasWeakSheafify J AddCommGrp<VAR>P : PresheafOfModules R₀<VAR>F : SheafOfModules R<VAR>f : (sheafification α).obj P ⟶ F<GOAL>((sheafificationAdjunction J AddCommGrp).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F)) ((SheafOfModules.toSheaf R).map ((sheafificationHomEquiv α).symm ((sheafificationHomEquiv α) f))) = ((sheafificationAdjunction J AddCommGrp).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F)) (((sheafificationAdjunction J AddCommGrp).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F)).symm ((sheafificationHomEquiv α) f).hom)
<VAR>C : Type u'<VAR>inst✝⁴ : Category.{v', u'} C<VAR>J : GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>inst✝³ : Presheaf.IsLocallyInjective J α<VAR>inst✝² : Presheaf.IsLocallySurjective J α<VAR>inst✝¹ : J.WEqualsLocallyBijective AddCommGrp<VAR>inst✝ : HasWeakSheafify J AddCommGrp<VAR>P : PresheafOfModules R₀<VAR>F : SheafOfModules R<VAR>f : (sheafification α).obj P ⟶ F<GOAL>(sheafificationAdjunction J AddCommGrp).unit.app P.presheaf ≫ (sheafToPresheaf J AddCommGrp).map ((SheafOfModules.toSheaf R).map f) = ((sheafificationHomEquiv α) f).hom
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t : Set α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hf' : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤<GOAL>(⨍⁻ (x : α), f x ∂μ).toReal = ⨍ (x : α), (f x).toReal ∂μ
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : ChosenFiniteProducts C<VAR>X Y Z : C<GOAL>(α_ X Y Z).hom ≫ snd X (Y ⊗ Z) ≫ snd Y Z = snd (X ⊗ Y) Z
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : ChosenFiniteProducts C<VAR>X Y Z : C<GOAL>Limits.BinaryFan.snd (product (product X Y).cone.pt Z).cone = snd (X ⊗ Y) Z
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<GOAL>HasFDerivAt (fun p => jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<VAR>T : ℝ<VAR>hT : 0 < T<VAR>hτ' : T < τ.im<GOAL>HasFDerivAt (fun p => jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<VAR>T : ℝ<VAR>hT : 0 < T<VAR>hτ' : T < τ.im<VAR>S : ℝ<VAR>hz : |z.im| < S<GOAL>HasFDerivAt (fun p => jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<VAR>T : ℝ<VAR>hT : 0 < T<VAR>hτ' : T < τ.im<VAR>S : ℝ<VAR>hz : |z.im| < S<VAR>V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}<GOAL>HasFDerivAt (fun p => jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<VAR>T : ℝ<VAR>hT : 0 < T<VAR>hτ' : T < τ.im<VAR>S : ℝ<VAR>hz : |z.im| < S<VAR>V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}<VAR>hVo : IsOpen V<GOAL>HasFDerivAt (fun p => jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<VAR>T : ℝ<VAR>hT : 0 < T<VAR>hτ' : T < τ.im<VAR>S : ℝ<VAR>hz : |z.im| < S<VAR>V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}<VAR>hVo : IsOpen V<VAR>hVmem : (z, τ) ∈ V<GOAL>HasFDerivAt (fun p => jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<VAR>T : ℝ<VAR>hT : 0 < T<VAR>hτ' : T < τ.im<VAR>S : ℝ<VAR>hz : |z.im| < S<VAR>V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}<VAR>hVo : IsOpen V<VAR>hVmem : (z, τ) ∈ V<VAR>hVp : IsPreconnected V<GOAL>HasFDerivAt (fun p => jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<VAR>T : ℝ<VAR>hT : 0 < T<VAR>hτ' : T < τ.im<VAR>S : ℝ<VAR>hz : |z.im| < S<VAR>V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}<VAR>hVo : IsOpen V<VAR>hVmem : (z, τ) ∈ V<VAR>hVp : IsPreconnected V<VAR>f : ℤ → ℂ × ℂ → ℂ := fun n p => jacobiTheta₂_term n p.1 p.2<VAR>f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun n p => jacobiTheta₂_term_fderiv n p.1 p.2<GOAL>HasFDerivAt (fun p => jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<VAR>T : ℝ<VAR>hT : 0 < T<VAR>hτ' : T < τ.im<VAR>S : ℝ<VAR>hz : |z.im| < S<VAR>V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}<VAR>hVo : IsOpen V<VAR>hVmem : (z, τ) ∈ V<VAR>hVp : IsPreconnected V<VAR>f : ℤ → ℂ × ℂ → ℂ := fun n p => jacobiTheta₂_term n p.1 p.2<VAR>f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun n p => jacobiTheta₂_term_fderiv n p.1 p.2<VAR>hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p<GOAL>HasFDerivAt (fun p => jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<VAR>T : ℝ<VAR>hT : 0 < T<VAR>hτ' : T < τ.im<VAR>S : ℝ<VAR>hz : |z.im| < S<VAR>V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}<VAR>hVo : IsOpen V<VAR>hVmem : (z, τ) ∈ V<VAR>hVp : IsPreconnected V<VAR>f : ℤ → ℂ × ℂ → ℂ := fun n p => jacobiTheta₂_term n p.1 p.2<VAR>f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun n p => jacobiTheta₂_term_fderiv n p.1 p.2<VAR>hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p<VAR>u : ℤ → ℝ := fun n => 3 * π * ↑|n| ^ 2 * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))<GOAL>HasFDerivAt (fun p => jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<VAR>T : ℝ<VAR>hT : 0 < T<VAR>hτ' : T < τ.im<VAR>S : ℝ<VAR>hz : |z.im| < S<VAR>V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}<VAR>hVo : IsOpen V<VAR>hVmem : (z, τ) ∈ V<VAR>hVp : IsPreconnected V<VAR>f : ℤ → ℂ × ℂ → ℂ := fun n p => jacobiTheta₂_term n p.1 p.2<VAR>f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun n p => jacobiTheta₂_term_fderiv n p.1 p.2<VAR>hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p<VAR>u : ℤ → ℝ := fun n => 3 * π * ↑|n| ^ 2 * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))<VAR>hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n<GOAL>HasFDerivAt (fun p => jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<VAR>T : ℝ<VAR>hT : 0 < T<VAR>hτ' : T < τ.im<VAR>S : ℝ<VAR>hz : |z.im| < S<VAR>V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}<VAR>hVo : IsOpen V<VAR>hVmem : (z, τ) ∈ V<VAR>hVp : IsPreconnected V<VAR>f : ℤ → ℂ × ℂ → ℂ := fun n p => jacobiTheta₂_term n p.1 p.2<VAR>f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun n p => jacobiTheta₂_term_fderiv n p.1 p.2<VAR>hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p<VAR>u : ℤ → ℝ := fun n => 3 * π * ↑|n| ^ 2 * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))<VAR>hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n<VAR>hu_sum : Summable u<GOAL>HasFDerivAt (fun p => jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<VAR>T : ℝ<VAR>hT : 0 < T<VAR>hτ' : T < τ.im<VAR>S : ℝ<VAR>hz : |z.im| < S<VAR>V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}<VAR>hVo : IsOpen V<VAR>hVmem : (z, τ) ∈ V<VAR>hVp : IsPreconnected V<VAR>f : ℤ → ℂ × ℂ → ℂ := fun n p => jacobiTheta₂_term n p.1 p.2<VAR>f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun n p => jacobiTheta₂_term_fderiv n p.1 p.2<VAR>hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p<VAR>u : ℤ → ℝ := fun n => 3 * π * ↑|n| ^ 2 * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))<VAR>hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n<VAR>hu_sum : Summable u<VAR>hf_sum : Summable fun n => f n (z, τ)<GOAL>HasFDerivAt (fun p => jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ γ₁ γ₂ : Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n + a = n'<GOAL>(leftShiftAddEquiv K L n a n' hn') (-γ) = -γ.leftShift a n' hn'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>K : Type u_3<VAR>inst✝ : DivisionRing K<VAR>a✝ b✝ c✝ d a b c : K<GOAL>a / c - b / c = (a - b) / c
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>f : Filter α<GOAL>Cauchy f ↔ f ≠ ⊥ ∧ ∀ ε > 0, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, edist x y < ε
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>f : Filter α<GOAL>Cauchy f ↔ f.NeBot ∧ ∀ ε > 0, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, edist x y < ε
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : CommSemiring R₁<VAR>inst✝¹ : AddCommMonoid M₁<VAR>inst✝ : Module R₁ M₁<VAR>I₁ I₂ I : R₁ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M<VAR>H : B.IsAlt<VAR>x y : M₁<VAR>h : (B x) y = 0<GOAL>(B y) x = 0
<VAR>α : Type u_1<VAR>inst✝² : Group α<VAR>inst✝¹ : LinearOrder α<VAR>a✝¹ b✝ : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a✝ b c a : α<GOAL>1 ≤ a * mabs a
<VAR>α : Type u_1<VAR>inst✝² : Group α<VAR>inst✝¹ : LinearOrder α<VAR>a✝¹ b✝ : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a✝ b c a : α<GOAL>a * a⁻¹ ≤ a * mabs a
<VAR>R : Type u<VAR>inst✝¹⁸ : CommRing R<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>P : Type w₂<VAR>Q : Type w₃<VAR>inst✝¹⁷ : LieRing L<VAR>inst✝¹⁶ : LieAlgebra R L<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : Module R M<VAR>inst✝¹³ : LieRingModule L M<VAR>inst✝¹² : LieModule R L M<VAR>inst✝¹¹ : AddCommGroup N<VAR>inst✝¹⁰ : Module R N<VAR>inst✝⁹ : LieRingModule L N<VAR>inst✝⁸ : LieModule R L N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>inst✝⁵ : LieRingModule L P<VAR>inst✝⁴ : LieModule R L P<VAR>inst✝³ : AddCommGroup Q<VAR>inst✝² : Module R Q<VAR>inst✝¹ : LieRingModule L Q<VAR>inst✝ : LieModule R L Q<VAR>x : L<VAR>m : M<VAR>n : N<GOAL>(hasBracketAux x) (m ⊗ₜ[R] n) = ⁅x, m⁆ ⊗ₜ[R] n + m ⊗ₜ[R] ⁅x, n⁆
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>M : Type v₁<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : Module R S<VAR>inst✝² : Module S A<VAR>inst✝¹ : Module R A<VAR>inst✝ : IsScalarTower R S A<VAR>s : Set S<VAR>hs : span R s = ⊤<VAR>t : Set A<VAR>k : S<VAR>x : A<VAR>hx : x ∈ span R (s • t)<GOAL>k • x ∈ span R (s • t)
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>M : Type v₁<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : Module R S<VAR>inst✝² : Module S A<VAR>inst✝¹ : Module R A<VAR>inst✝ : IsScalarTower R S A<VAR>s : Set S<VAR>hs : span R s = ⊤<VAR>t : Set A<VAR>k : S<VAR>x : A<VAR>hx : x ∈ restrictScalars R (span S t)<GOAL>k • x ∈ restrictScalars R (span S t)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Group G<VAR>inst✝ : Fintype G<VAR>x : G<VAR>n : ℕ<GOAL>x ^ card G = 1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f✝ g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>f : X → ℝ<VAR>hfi : Integrable f μ<VAR>h_meas : NullMeasurableSet {x | 0 ≤ f x} μ<GOAL>∫ (x : X), ‖f x‖ ∂μ = ∫ (x : X) in {x | 0 ≤ f x}, ‖f x‖ ∂μ + ∫ (x : X) in {x | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f✝ g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>f : X → ℝ<VAR>hfi : Integrable f μ<VAR>h_meas : NullMeasurableSet {x | 0 ≤ f x} μ<GOAL>∫ (x : X) in {x | 0 ≤ f x}, ‖f x‖ ∂μ = ∫ (x : X) in {x | 0 ≤ f x}, f x ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f✝ g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>f : X → ℝ<VAR>hfi : Integrable f μ<VAR>h_meas : NullMeasurableSet {x | 0 ≤ f x} μ<VAR>x : X<VAR>hx : x ∈ {x | 0 ≤ f x}<GOAL>‖f x‖ = f x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f✝ g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>f : X → ℝ<VAR>hfi : Integrable f μ<VAR>h_meas : NullMeasurableSet {x | 0 ≤ f x} μ<VAR>x : X<VAR>hx : x ∈ {x | 0 ≤ f x}<GOAL>0 ≤ f x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f✝ g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>f : X → ℝ<VAR>hfi : Integrable f μ<VAR>h_meas : NullMeasurableSet {x | 0 ≤ f x} μ<GOAL>∫ (x : X) in {x | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ = -∫ (x : X) in {x | 0 ≤ f x}ᶜ, f x ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f✝ g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>f : X → ℝ<VAR>hfi : Integrable f μ<VAR>h_meas : NullMeasurableSet {x | 0 ≤ f x} μ<GOAL>∫ (x : X) in {x | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ = ∫ (a : X) in {x | 0 ≤ f x}ᶜ, -f a ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f✝ g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>f : X → ℝ<VAR>hfi : Integrable f μ<VAR>h_meas : NullMeasurableSet {x | 0 ≤ f x} μ<VAR>x : X<VAR>hx : x ∈ {x | 0 ≤ f x}ᶜ<GOAL>‖f x‖ = -f x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f✝ g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>f : X → ℝ<VAR>hfi : Integrable f μ<VAR>h_meas : NullMeasurableSet {x | 0 ≤ f x} μ<VAR>x : X<VAR>hx : x ∈ {x | 0 ≤ f x}ᶜ<GOAL>f x ≤ 0
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f✝ g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>f : X → ℝ<VAR>hfi : Integrable f μ<VAR>h_meas : NullMeasurableSet {x | 0 ≤ f x} μ<VAR>x : X<VAR>hx : ¬0 ≤ f x<GOAL>f x ≤ 0
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f✝ g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>f : X → ℝ<VAR>hfi : Integrable f μ<VAR>h_meas : NullMeasurableSet {x | 0 ≤ f x} μ<GOAL>∫ (x : X) in {x | 0 ≤ f x}, f x ∂μ - ∫ (x : X) in {x | 0 ≤ f x}ᶜ, f x ∂μ = ∫ (x : X) in {x | 0 ≤ f x}, f x ∂μ - ∫ (x : X) in {x | f x ≤ 0}, f x ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f✝ g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>f : X → ℝ<VAR>hfi : Integrable f μ<VAR>h_meas : NullMeasurableSet {x | 0 ≤ f x} μ<GOAL>∫ (x : X) in {x | 0 ≤ f x}, f x ∂μ - ∫ (x : X) in {a | ¬0 ≤ f a}, f x ∂μ = ∫ (x : X) in {x | 0 ≤ f x}, f x ∂μ - ∫ (x : X) in {x | f x < 0}, f x ∂μ
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>hσ : Finite σ<VAR>p : Polynomial (MvPolynomial σ R)<VAR>hp : ((optionEquivLeft R σ).symm p).IsHomogeneous n<VAR>i j : ℕ<VAR>h : i + j = n<GOAL>(p.coeff i).IsHomogeneous j
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>hσ : Finite σ<VAR>p : Polynomial (MvPolynomial σ R)<VAR>hp : ((optionEquivLeft R σ).symm p).IsHomogeneous n<VAR>i j : ℕ<VAR>h : i + j = n<VAR>k : ℕ<VAR>e : σ ≃ Fin k<GOAL>(p.coeff i).IsHomogeneous j
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ✝ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>hσ : Finite σ<VAR>p : Polynomial (MvPolynomial σ R)<VAR>hp : ((optionEquivLeft R σ).symm p).IsHomogeneous n<VAR>i j : ℕ<VAR>h : i + j = n<VAR>k : ℕ<VAR>e : σ ≃ Fin k<VAR>e' : Option σ ≃ Fin (k + 1) := e.optionCongr.trans (_root_.finSuccEquiv k).symm<VAR>F : MvPolynomial σ R ≃ₐ[R] MvPolynomial (Fin k) R := renameEquiv R e<VAR>F' : MvPolynomial (Option σ) R ≃ₐ[R] MvPolynomial (Fin (k + 1)) R := renameEquiv R e'<VAR>φ : MvPolynomial (Fin (k + 1)) R := F' ((optionEquivLeft R σ).symm p)<GOAL>(p.coeff i).IsHomogeneous j
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ✝ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>hσ : Finite σ<VAR>p : Polynomial (MvPolynomial σ R)<VAR>hp : ((optionEquivLeft R σ).symm p).IsHomogeneous n<VAR>i j : ℕ<VAR>h : i + j = n<VAR>k : ℕ<VAR>e : σ ≃ Fin k<VAR>e' : Option σ ≃ Fin (k + 1) := e.optionCongr.trans (_root_.finSuccEquiv k).symm<VAR>F : MvPolynomial σ R ≃ₐ[R] MvPolynomial (Fin k) R := renameEquiv R e<VAR>F' : MvPolynomial (Option σ) R ≃ₐ[R] MvPolynomial (Fin (k + 1)) R := renameEquiv R e'<VAR>φ : MvPolynomial (Fin (k + 1)) R := F' ((optionEquivLeft R σ).symm p)<VAR>hφ : φ.IsHomogeneous n<GOAL>(p.coeff i).IsHomogeneous j
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ✝ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>hσ : Finite σ<VAR>p : Polynomial (MvPolynomial σ R)<VAR>hp : ((optionEquivLeft R σ).symm p).IsHomogeneous n<VAR>i j : ℕ<VAR>h : i + j = n<VAR>k : ℕ<VAR>e : σ ≃ Fin k<VAR>e' : Option σ ≃ Fin (k + 1) := e.optionCongr.trans (_root_.finSuccEquiv k).symm<VAR>F : MvPolynomial σ R ≃ₐ[R] MvPolynomial (Fin k) R := renameEquiv R e<VAR>F' : MvPolynomial (Option σ) R ≃ₐ[R] MvPolynomial (Fin (k + 1)) R := renameEquiv R e'<VAR>φ : MvPolynomial (Fin (k + 1)) R := F' ((optionEquivLeft R σ).symm p)<VAR>hφ : φ.IsHomogeneous n<GOAL>(F (p.coeff i)).IsHomogeneous j