ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℕ<VAR>a b : α<VAR>n : ℕ<VAR>inst✝ : DecidableEq α<VAR>h : a ≠ b<GOAL>(f a + (f b).succ).choose (f a) + (f a + (f b).succ).choose (f a).succ = (f a + (f b).succ).choose (f a).succ + (f a + (f b).succ).choose (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>hβ : Nonempty β<GOAL>range (const α) = {f | ∀ (x y : α), f x = f y}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>hβ : Nonempty β<VAR>f : α → β<VAR>hf : f ∈ {f | ∀ (x y : α), f x = f y}<GOAL>∃ a, const α a = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>hβ : Nonempty β<VAR>f : α → β<VAR>hf : f ∈ {f | ∀ (x y : α), f x = f y}<VAR>h : IsEmpty α<GOAL>∃ a, const α a = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>hβ : Nonempty β<VAR>f : α → β<VAR>hf : f ∈ {f | ∀ (x y : α), f x = f y}<VAR>a : α<GOAL>∃ a, const α a = f
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>H1 : b ∣ a<VAR>H2 : a / b = c<GOAL>a = c * b
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : CommSemiring k<VAR>inst✝² : Group G<VAR>inst✝¹ : Fintype G<VAR>inst✝ : Invertible ↑(Fintype.card G)<VAR>g : G<GOAL>Finsupp.single g 1 * average k G = average k G
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : CommSemiring k<VAR>inst✝² : Group G<VAR>inst✝¹ : Fintype G<VAR>inst✝ : Invertible ↑(Fintype.card G)<VAR>g : G<GOAL>⅟↑(Fintype.card G) • ∑ x : G, single (g * x) 1 = ⅟↑(Fintype.card G) • ∑ x : G, single x 1
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : CommSemiring k<VAR>inst✝² : Group G<VAR>inst✝¹ : Fintype G<VAR>inst✝ : Invertible ↑(Fintype.card G)<VAR>g : G<VAR>f : G → MonoidAlgebra k G := fun x => Finsupp.single x 1<GOAL>⅟↑(Fintype.card G) • ∑ x : G, f (g * x) = ⅟↑(Fintype.card G) • ∑ x : G, f x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : CommSemiring A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module A M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsScalarTower R A M<VAR>d✝ : Derivation R A M<VAR>a : A<VAR>d : Derivation R A M<VAR>f : R[X]<GOAL>(d.compAEval a) f = derivative f • (AEval.of R M a) (d a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : CommSemiring A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module A M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsScalarTower R A M<VAR>d✝ : Derivation R A M<VAR>a : A<VAR>d : Derivation R A M<VAR>f : R[X]<GOAL>(d.compAEval a) f = ((mkDerivation R) ((AEval.of R M a) (d a))) f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : CommSemiring A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module A M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsScalarTower R A M<VAR>d✝ : Derivation R A M<VAR>a : A<VAR>d : Derivation R A M<VAR>f : R[X]<GOAL>d.compAEval a = (mkDerivation R) ((AEval.of R M a) (d a))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : CommSemiring A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module A M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsScalarTower R A M<VAR>d✝ : Derivation R A M<VAR>a : A<VAR>d : Derivation R A M<VAR>f : R[X]<GOAL>(d.compAEval a) X = ((mkDerivation R) ((AEval.of R M a) (d a))) X
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : Algebra.IsAlgebraic F E<GOAL>finSepDegree F E = Cardinal.toNat (sepDegree F E)
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>this : Algebra.IsAlgebraic (↥(separableClosure F E)) E<GOAL>finSepDegree F E = Cardinal.toNat (sepDegree F E)
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>this : Algebra.IsAlgebraic (↥(separableClosure F E)) E<VAR>h : finSepDegree F E = finSepDegree F ↥(separableClosure F E) * finSepDegree (↥(separableClosure F E)) E<GOAL>finSepDegree F E = Cardinal.toNat (sepDegree F E)
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>this✝ : Algebra.IsAlgebraic (↥(separableClosure F E)) E<VAR>h : finSepDegree F E = finSepDegree F ↥(separableClosure F E) * finSepDegree (↥(separableClosure F E)) E<VAR>this : Algebra.IsSeparable F ↥(separableClosure F E)<GOAL>finSepDegree F E = Cardinal.toNat (sepDegree F E)
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>this✝¹ : Algebra.IsAlgebraic (↥(separableClosure F E)) E<VAR>h : finSepDegree F E = finSepDegree F ↥(separableClosure F E) * finSepDegree (↥(separableClosure F E)) E<VAR>this✝ : Algebra.IsSeparable F ↥(separableClosure F E)<VAR>this : IsPurelyInseparable (↥(separableClosure F E)) E<GOAL>finSepDegree F E = Cardinal.toNat (sepDegree F E)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v, u₁} C<VAR>C' : Type u₂<VAR>inst✝ : Category.{v, u₂} C'<VAR>D : GlueData C<VAR>i j : D.J<GOAL>D.t' i i j = (pullbackSymmetry (D.f i i) (D.f i j)).hom
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v, u₁} C<VAR>C' : Type u₂<VAR>inst✝ : Category.{v, u₂} C'<VAR>D : GlueData C<VAR>i j : D.J<VAR>eq₁ : D.t' i i j ≫ pullback.snd (D.f i j) (D.f i i) = pullback.fst (D.f i i) (D.f i j) ≫ D.t i i<GOAL>D.t' i i j = (pullbackSymmetry (D.f i i) (D.f i j)).hom
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v, u₁} C<VAR>C' : Type u₂<VAR>inst✝ : Category.{v, u₂} C'<VAR>D : GlueData C<VAR>i j : D.J<VAR>eq₁ : D.t' i i j ≫ pullback.snd (D.f i j) (D.f i i) = pullback.fst (D.f i i) (D.f i j) ≫ D.t i i<VAR>eq₂ : pullback.fst (D.f i i) (D.f i j) = (pullback.snd (D.f i i) (D.f i j) ≫ D.f i j) ≫ inv (D.f i i)<GOAL>D.t' i i j = (pullbackSymmetry (D.f i i) (D.f i j)).hom
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v, u₁} C<VAR>C' : Type u₂<VAR>inst✝ : Category.{v, u₂} C'<VAR>D : GlueData C<VAR>i j : D.J<VAR>eq₁ : D.t' i i j ≫ pullback.snd (D.f i j) (D.f i i) = (pullback.snd (D.f i i) (D.f i j) ≫ D.f i j) ≫ inv (D.f i i)<VAR>eq₂ : pullback.fst (D.f i i) (D.f i j) = (pullback.snd (D.f i i) (D.f i j) ≫ D.f i j) ≫ inv (D.f i i)<GOAL>D.t' i i j = (pullbackSymmetry (D.f i i) (D.f i j)).hom
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v, u₁} C<VAR>C' : Type u₂<VAR>inst✝ : Category.{v, u₂} C'<VAR>D : GlueData C<VAR>i j : D.J<VAR>eq₁ : D.t' i i j ≫ pullback.snd (D.f i j) (D.f i i) = (pullback.snd (D.f i i) (D.f i j) ≫ D.f i j) ≫ inv (D.f i i)<VAR>eq₂ : pullback.fst (D.f i i) (D.f i j) = (pullback.snd (D.f i i) (D.f i j) ≫ D.f i j) ≫ inv (D.f i i)<VAR>eq₃ : (D.t' i i j ≫ pullback.snd (D.f i j) (D.f i i)) ≫ D.f i i = pullback.snd (D.f i i) (D.f i j) ≫ D.f i j<GOAL>D.t' i i j = (pullbackSymmetry (D.f i i) (D.f i j)).hom
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v, u₁} C<VAR>C' : Type u₂<VAR>inst✝ : Category.{v, u₂} C'<VAR>D : GlueData C<VAR>i j : D.J<VAR>eq₁ : D.t' i i j ≫ pullback.snd (D.f i j) (D.f i i) = (pullback.snd (D.f i i) (D.f i j) ≫ D.f i j) ≫ inv (D.f i i)<VAR>eq₂ : pullback.fst (D.f i i) (D.f i j) = (pullback.snd (D.f i i) (D.f i j) ≫ D.f i j) ≫ inv (D.f i i)<VAR>eq₃ : (D.t' i i j ≫ pullback.fst (D.f i j) (D.f i i)) ≫ D.f i j = pullback.snd (D.f i i) (D.f i j) ≫ D.f i j<GOAL>D.t' i i j = (pullbackSymmetry (D.f i i) (D.f i j)).hom
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : 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>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype n'<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis n' R M₂<VAR>J J₂ : Matrix n n R<VAR>J' : Matrix n' n' R<VAR>A : Matrix n' n R<VAR>A' : Matrix n n' R<VAR>A₁ A₂ : Matrix n n R<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : DecidableEq n'<GOAL>A₁ ∈ skewAdjointMatricesSubmodule J ↔ J.IsSkewAdjoint A₁
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : 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>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype n'<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis n' R M₂<VAR>J J₂ : Matrix n n R<VAR>J' : Matrix n' n' R<VAR>A : Matrix n' n R<VAR>A' : Matrix n n' R<VAR>A₁ A₂ : Matrix n n R<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : DecidableEq n'<GOAL>(-J).IsAdjointPair J A₁ A₁ ↔ J.IsSkewAdjoint A₁
<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✝ g f : α → E<VAR>s t : Set α<VAR>hd : AEDisjoint μ s t<VAR>ht : NullMeasurableSet t μ<VAR>hs₀ : μ s ≠ 0<VAR>ht₀ : μ t ≠ 0<VAR>hsμ : μ s ≠ ⊤<VAR>htμ : μ t ≠ ⊤<VAR>hfs : IntegrableOn f s μ<VAR>hft : IntegrableOn f t μ<GOAL>⨍ (x : α) in s ∪ t, f x ∂μ ∈ openSegment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in t, f x ∂μ)
<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✝ g f : α → E<VAR>s t : Set α<VAR>hd : AEDisjoint μ s t<VAR>ht : NullMeasurableSet t μ<VAR>ht₀ : μ t ≠ 0<VAR>hsμ : μ s ≠ ⊤<VAR>htμ : μ t ≠ ⊤<VAR>hfs : IntegrableOn f s μ<VAR>hft : IntegrableOn f t μ<VAR>hs₀ : 0 < (μ s).toReal<GOAL>⨍ (x : α) in s ∪ t, f x ∂μ ∈ openSegment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in t, f x ∂μ)
<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✝ g f : α → E<VAR>s t : Set α<VAR>hd : AEDisjoint μ s t<VAR>ht : NullMeasurableSet t μ<VAR>hsμ : μ s ≠ ⊤<VAR>htμ : μ t ≠ ⊤<VAR>hfs : IntegrableOn f s μ<VAR>hft : IntegrableOn f t μ<VAR>hs₀ : 0 < (μ s).toReal<VAR>ht₀ : 0 < (μ t).toReal<GOAL>⨍ (x : α) in s ∪ t, f x ∂μ ∈ openSegment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in t, f x ∂μ)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Abelian C<VAR>inst✝¹ : HasExt C<VAR>X Y Z T : C<VAR>n : ℕ<VAR>inst✝ : HasDerivedCategory C<VAR>α β : Ext X Y n<GOAL>(α + β).hom = α.hom + β.hom
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Abelian C<VAR>inst✝¹ : HasExt C<VAR>X Y Z T : C<VAR>n : ℕ<VAR>inst✝ : HasDerivedCategory C<VAR>α β : Ext X Y n<VAR>α' : Ext (X ⊞ X) Y n := (mk₀ biprod.fst).comp α ⋯<GOAL>(α + β).hom = α.hom + β.hom
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Abelian C<VAR>inst✝¹ : HasExt C<VAR>X Y Z T : C<VAR>n : ℕ<VAR>inst✝ : HasDerivedCategory C<VAR>α β : Ext X Y n<VAR>α' : Ext (X ⊞ X) Y n := (mk₀ biprod.fst).comp α ⋯<VAR>β' : Ext (X ⊞ X) Y n := (mk₀ biprod.snd).comp β ⋯<GOAL>(α + β).hom = α.hom + β.hom
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Abelian C<VAR>inst✝¹ : HasExt C<VAR>X Y Z T : C<VAR>n : ℕ<VAR>inst✝ : HasDerivedCategory C<VAR>α β : Ext X Y n<VAR>α' : Ext (X ⊞ X) Y n := (mk₀ biprod.fst).comp α ⋯<VAR>β' : Ext (X ⊞ X) Y n := (mk₀ biprod.snd).comp β ⋯<VAR>eq₁ : α + β = (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).comp (α' + β') ⋯<GOAL>(α + β).hom = α.hom + β.hom
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Abelian C<VAR>inst✝¹ : HasExt C<VAR>X Y Z T : C<VAR>n : ℕ<VAR>inst✝ : HasDerivedCategory C<VAR>α β : Ext X Y n<VAR>α' : Ext (X ⊞ X) Y n := (mk₀ biprod.fst).comp α ⋯<VAR>β' : Ext (X ⊞ X) Y n := (mk₀ biprod.snd).comp β ⋯<VAR>eq₁ : α + β = (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).comp (α' + β') ⋯<VAR>eq₂ : α' + β' = homEquiv.symm (α'.hom + β'.hom)<GOAL>(α + β).hom = α.hom + β.hom
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Abelian C<VAR>inst✝¹ : HasExt C<VAR>X Y Z T : C<VAR>n : ℕ<VAR>inst✝ : HasDerivedCategory C<VAR>α β : Ext X Y n<VAR>α' : Ext (X ⊞ X) Y n := (mk₀ biprod.fst).comp α ⋯<VAR>β' : Ext (X ⊞ X) Y n := (mk₀ biprod.snd).comp β ⋯<VAR>eq₁ : α + β = (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).comp (α' + β') ⋯<VAR>eq₂ : α' + β' = homEquiv.symm (α'.hom + β'.hom)<GOAL>(mk₀ (biprod.lift (𝟙 X) (𝟙 X))).hom.comp α'.hom ⋯ + (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).hom.comp β'.hom ⋯ = α.hom + β.hom
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>v : E<VAR>L : ℝ →L[ℝ] E := ContinuousLinearMap.smulRight 1 v<GOAL>∀ᵐ (p : E) ∂μ, LineDifferentiableAt ℝ f p v
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>v : E<VAR>L : ℝ →L[ℝ] E := ContinuousLinearMap.smulRight 1 v<GOAL>∀ (p : E), ∀ᵐ (t : ℝ), LineDifferentiableAt ℝ f (p + t • v) v
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>v : E<VAR>L : ℝ →L[ℝ] E := ContinuousLinearMap.smulRight 1 v<VAR>p : E<GOAL>∀ᵐ (t : ℝ), LineDifferentiableAt ℝ f (p + t • v) v
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>v : E<VAR>L : ℝ →L[ℝ] E := ContinuousLinearMap.smulRight 1 v<VAR>p : E<VAR>this : ∀ᵐ (s : ℝ), DifferentiableAt ℝ (fun t => f (p + t • v)) s<GOAL>∀ᵐ (t : ℝ), LineDifferentiableAt ℝ f (p + t • v) v
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>v : E<VAR>L : ℝ →L[ℝ] E := ContinuousLinearMap.smulRight 1 v<VAR>p : E<VAR>this : ∀ᵐ (s : ℝ), DifferentiableAt ℝ (fun t => f (p + t • v)) s<VAR>s : ℝ<VAR>hs : DifferentiableAt ℝ (fun t => f (p + t • v)) s<GOAL>LineDifferentiableAt ℝ f (p + s • v) v
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>v : E<VAR>L : ℝ →L[ℝ] E := ContinuousLinearMap.smulRight 1 v<VAR>p : E<VAR>this : ∀ᵐ (s : ℝ), DifferentiableAt ℝ (fun t => f (p + t • v)) s<VAR>s : ℝ<VAR>hs : DifferentiableAt ℝ (fun t => f (p + t • v)) s<VAR>h's : DifferentiableAt ℝ (fun t => f (p + t • v)) (s + 0)<GOAL>LineDifferentiableAt ℝ f (p + s • v) v
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>v : E<VAR>L : ℝ →L[ℝ] E := ContinuousLinearMap.smulRight 1 v<VAR>p : E<VAR>this✝ : ∀ᵐ (s : ℝ), DifferentiableAt ℝ (fun t => f (p + t • v)) s<VAR>s : ℝ<VAR>hs : DifferentiableAt ℝ (fun t => f (p + t • v)) s<VAR>h's : DifferentiableAt ℝ (fun t => f (p + t • v)) (s + 0)<VAR>this : DifferentiableAt ℝ (fun t => s + t) 0<GOAL>LineDifferentiableAt ℝ f (p + s • v) v
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>v : E<VAR>L : ℝ →L[ℝ] E := ContinuousLinearMap.smulRight 1 v<VAR>p : E<VAR>this✝ : ∀ᵐ (s : ℝ), DifferentiableAt ℝ (fun t => f (p + t • v)) s<VAR>s : ℝ<VAR>hs : DifferentiableAt ℝ (fun t => f (p + t • v)) s<VAR>h's : DifferentiableAt ℝ (fun t => f (p + t • v)) (s + 0)<VAR>this : DifferentiableAt ℝ (fun t => s + t) 0<GOAL>DifferentiableAt ℝ (fun t => f (p + s • v + t • v)) 0
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>v : E<VAR>L : ℝ →L[ℝ] E := ContinuousLinearMap.smulRight 1 v<VAR>p : E<VAR>this✝ : ∀ᵐ (s : ℝ), DifferentiableAt ℝ (fun t => f (p + t • v)) s<VAR>s : ℝ<VAR>hs : DifferentiableAt ℝ (fun t => f (p + t • v)) s<VAR>h's : DifferentiableAt ℝ (fun t => f (p + t • v)) (s + 0)<VAR>this : DifferentiableAt ℝ (fun t => s + t) 0<VAR>t : ℝ<GOAL>f (p + s • v + t • v) = ((fun t => f (p + t • v)) ∘ HAdd.hAdd s) t
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>inst✝ : Finite I<VAR>e : I → R<VAR>he : OrthogonalIdempotents e<GOAL>Function.Surjective ⇑(Pi.ringHom fun i => Ideal.Quotient.mk (Ideal.span {1 - e i}))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>inst✝ : Finite I<VAR>e : I → R<VAR>he : OrthogonalIdempotents e<GOAL>Pairwise fun i j => IsCoprime (Ideal.span {1 - e i}) (Ideal.span {1 - e j})
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>inst✝ : Finite I<VAR>e : I → R<VAR>he : OrthogonalIdempotents e<VAR>i j : I<VAR>hij : i ≠ j<GOAL>IsCoprime (Ideal.span {1 - e i}) (Ideal.span {1 - e j})
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>inst✝ : Finite I<VAR>e : I → R<VAR>he : OrthogonalIdempotents e<VAR>i j : I<VAR>hij : i ≠ j<GOAL>IsCoprime (1 - e i) (1 - e j)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : MonoidalCategory C<VAR>X Y : C<GOAL>(α_ (𝟙_ C) X Y).hom ≫ (λ_ (X ⊗ Y)).hom = (λ_ X).hom ⊗ 𝟙 Y
<VAR>α : Type u<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>x : α<GOAL>lfpApprox f ⊥ (succ #α).ord = lfp f
<VAR>α : Type u<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>x : α<GOAL>lfpApprox f ⊥ (succ #α).ord ≤ lfp f
<VAR>α : Type u<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>x : α<GOAL>lfp f ≤ lfpApprox f ⊥ (succ #α).ord
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : LocalRing R<VAR>J : Ideal R<VAR>hJ : J ≠ ⊤<GOAL>J ≤ maximalIdeal R
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : LocalRing R<VAR>J : Ideal R<VAR>hJ : J ≠ ⊤<VAR>M : Ideal R<VAR>hM1 : M.IsMaximal<VAR>hM2 : J ≤ M<GOAL>J ≤ maximalIdeal R
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : DistribLattice α<VAR>a b✝ c✝ : α<VAR>h : ∀ ⦃b c : α⦄, b ⊔ c = a → b = a ∨ c = a<VAR>b c : α<GOAL>a ≤ b ⊔ c → a ≤ b ∨ a ≤ c
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : DistribLattice α<VAR>a b✝ c✝ : α<VAR>h : ∀ ⦃b c : α⦄, b ⊔ c = a → b = a ∨ c = a<VAR>b c : α<GOAL>a ⊓ b ⊔ a ⊓ c = a → a ⊓ b = a ∨ a ⊓ c = a
<VAR>p : ℕ<VAR>fp : Fact (Nat.Prime p)<VAR>a : ℤ<GOAL>legendreSym p a = J(a | p)
<VAR>α : Type u_1<VAR>a✝ b✝ c✝ d : α<VAR>inst✝¹ : MulZeroClass α<VAR>inst✝ : PartialOrder α<VAR>h✝ : CovariantClass { x // 0 < x } α (fun x y => y * ↑x) fun x x_1 => x ≤ x_1<VAR>a : { x // 0 ≤ x }<VAR>b c : α<VAR>h : b ≤ c<GOAL>b * ↑a ≤ c * ↑a
<VAR>α : Type u_1<VAR>a✝ b✝ c✝ d : α<VAR>inst✝¹ : MulZeroClass α<VAR>inst✝ : PartialOrder α<VAR>h✝ : CovariantClass { x // 0 < x } α (fun x y => y * ↑x) fun x x_1 => x ≤ x_1<VAR>a : { x // 0 ≤ x }<VAR>b c : α<VAR>h : b ≤ c<VAR>ha : 0 = ↑a<GOAL>b * ↑a ≤ c * ↑a
<VAR>α : Type u_1<VAR>a✝ b✝ c✝ d : α<VAR>inst✝¹ : MulZeroClass α<VAR>inst✝ : PartialOrder α<VAR>h✝ : CovariantClass { x // 0 < x } α (fun x y => y * ↑x) fun x x_1 => x ≤ x_1<VAR>a : { x // 0 ≤ x }<VAR>b c : α<VAR>h : b ≤ c<VAR>ha : 0 < ↑a<GOAL>b * ↑a ≤ c * ↑a
<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>inst✝ : HasTerminal C<VAR>X : C<VAR>f : ⊤_ C ⟶ X<GOAL>f = default
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>f : N →ₗ[R] P<VAR>Q : QuadraticMap R M N<VAR>b : R<VAR>x : M<GOAL>(fun x => f (Q x)) (b • x) = (b * b) • (fun x => f (Q x)) x
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>f : N →ₗ[R] P<VAR>Q : QuadraticMap R M N<VAR>B : BilinMap R M N<VAR>h : ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y<VAR>x y : M<GOAL>(fun x => f (Q x)) (x + y) = (fun x => f (Q x)) x + (fun x => f (Q x)) y + ((LinearMap.compr₂ B f) x) y
<VAR>R S T : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : CommRing T<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra R T<GOAL>(pullbackSpecIso R S T).hom ≫ Spec.map (ofHom includeLeftRingHom) = pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T)))
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y Z : Mon_ C<VAR>M N P : Bimod X Y<VAR>f : M ⟶ N<VAR>g : N ⟶ P<VAR>Q : Bimod Y Z<GOAL>(whiskerRight (f ≫ g) Q).hom = (whiskerRight f Q ≫ whiskerRight g Q).hom
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y Z : Mon_ C<VAR>M N P : Bimod X Y<VAR>f : M ⟶ N<VAR>g : N ⟶ P<VAR>Q : Bimod Y Z<GOAL>coequalizer.π (M.actRight ▷ Q.X) ((α_ M.X Y.X Q.X).hom ≫ M.X ◁ Q.actLeft) ≫ (whiskerRight (f ≫ g) Q).hom = coequalizer.π (M.actRight ▷ Q.X) ((α_ M.X Y.X Q.X).hom ≫ M.X ◁ Q.actLeft) ≫ (whiskerRight f Q ≫ whiskerRight g Q).hom