ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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 E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : IsPurelyInseparable F E<VAR>ι : Type u_1<VAR>v : ι → K<VAR>hsep : ∀ (i : ι), IsSeparable F (v i)<VAR>h : LinearIndependent F v<VAR>q : ℕ<VAR>h✝ : ExpChar F q<VAR>this : ExpChar K q<VAR>l : ι →₀ E<VAR>hl : (Finsupp.total ι K E v) l = 0<VAR>i : ι<VAR>f : ι → ℕ<VAR>hf : ∀ (i : ι), l i ^ q ^ f i ∈ (algebraMap F E).range<GOAL>l i = 0 i
<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 E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : IsPurelyInseparable F E<VAR>ι : Type u_1<VAR>v : ι → K<VAR>hsep : ∀ (i : ι), IsSeparable F (v i)<VAR>h : LinearIndependent F v<VAR>q : ℕ<VAR>h✝ : ExpChar F q<VAR>this : ExpChar K q<VAR>l : ι →₀ E<VAR>hl : (Finsupp.total ι K E v) l = 0<VAR>i : ι<VAR>f : ι → ℕ<VAR>hf : ∀ (i : ι), l i ^ q ^ f i ∈ (algebraMap F E).range<VAR>n : ℕ := l.support.sup f<GOAL>l i = 0 i
<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 E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : IsPurelyInseparable F E<VAR>ι : Type u_1<VAR>v : ι → K<VAR>hsep : ∀ (i : ι), IsSeparable F (v i)<VAR>h : LinearIndependent F v<VAR>q : ℕ<VAR>h✝ : ExpChar F q<VAR>this✝ : ExpChar K q<VAR>l : ι →₀ E<VAR>hl : (Finsupp.total ι K E v) l = 0<VAR>i : ι<VAR>f : ι → ℕ<VAR>hf : ∀ (i : ι), l i ^ q ^ f i ∈ (algebraMap F E).range<VAR>n : ℕ := l.support.sup f<VAR>this : q ^ n ≠ 0<GOAL>l i = 0 i
<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 E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : IsPurelyInseparable F E<VAR>ι : Type u_1<VAR>v : ι → K<VAR>hsep : ∀ (i : ι), IsSeparable F (v i)<VAR>h : LinearIndependent F v<VAR>q : ℕ<VAR>h✝ : ExpChar F q<VAR>this✝ : ExpChar K q<VAR>l : ι →₀ E<VAR>hl : (Finsupp.total ι K E v) l = 0<VAR>i : ι<VAR>f : ι → ℕ<VAR>n : ℕ := l.support.sup f<VAR>this : q ^ n ≠ 0<VAR>lF : ι → F<VAR>hlF : ∀ (i : ι), (algebraMap F E) (lF i) = l i ^ q ^ n<GOAL>l i = 0 i
<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 E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : IsPurelyInseparable F E<VAR>ι : Type u_1<VAR>v : ι → K<VAR>hsep : ∀ (i : ι), IsSeparable F (v i)<VAR>h : LinearIndependent F v<VAR>q : ℕ<VAR>h✝ : ExpChar F q<VAR>this✝ : ExpChar K q<VAR>l : ι →₀ E<VAR>hl : (Finsupp.total ι K E v) l = 0<VAR>i : ι<VAR>f : ι → ℕ<VAR>n : ℕ := l.support.sup f<VAR>this : q ^ n ≠ 0<VAR>lF : ι → F<VAR>hlF : ∀ (i : ι), (algebraMap F E) (lF i) = l i ^ q ^ n<VAR>lF₀ : ι →₀ F := Finsupp.onFinset l.support lF ⋯<GOAL>l i = 0 i
<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 E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : IsPurelyInseparable F E<VAR>ι : Type u_1<VAR>v : ι → K<VAR>hsep : ∀ (i : ι), IsSeparable F (v i)<VAR>q : ℕ<VAR>h✝ : ExpChar F q<VAR>this✝ : ExpChar K q<VAR>l : ι →₀ E<VAR>hl : (Finsupp.total ι K E v) l = 0<VAR>i : ι<VAR>f : ι → ℕ<VAR>n : ℕ := l.support.sup f<VAR>this : q ^ n ≠ 0<VAR>lF : ι → F<VAR>hlF : ∀ (i : ι), (algebraMap F E) (lF i) = l i ^ q ^ n<VAR>lF₀ : ι →₀ F := Finsupp.onFinset l.support lF ⋯<VAR>h : lF₀ = 0<GOAL>l i = 0 i
<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 E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : IsPurelyInseparable F E<VAR>ι : Type u_1<VAR>v : ι → K<VAR>hsep : ∀ (i : ι), IsSeparable F (v i)<VAR>q : ℕ<VAR>h✝ : ExpChar F q<VAR>this✝ : ExpChar K q<VAR>l : ι →₀ E<VAR>hl : (Finsupp.total ι K E v) l = 0<VAR>i : ι<VAR>f : ι → ℕ<VAR>n : ℕ := l.support.sup f<VAR>this : q ^ n ≠ 0<VAR>lF : ι → F<VAR>hlF : ∀ (i : ι), (algebraMap F E) (lF i) = l i ^ q ^ n<VAR>lF₀ : ι →₀ F := Finsupp.onFinset l.support lF ⋯<VAR>h : lF₀ = 0<GOAL>(algebraMap F E) (lF i) = 0
<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 E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : IsPurelyInseparable F E<VAR>ι : Type u_1<VAR>v : ι → K<VAR>hsep : ∀ (i : ι), IsSeparable F (v i)<VAR>q : ℕ<VAR>h✝ : ExpChar F q<VAR>this✝ : ExpChar K q<VAR>l : ι →₀ E<VAR>hl : (Finsupp.total ι K E v) l = 0<VAR>i : ι<VAR>f : ι → ℕ<VAR>n : ℕ := l.support.sup f<VAR>this : q ^ n ≠ 0<VAR>lF : ι → F<VAR>hlF : ∀ (i : ι), (algebraMap F E) (lF i) = l i ^ q ^ n<VAR>lF₀ : ι →₀ F := Finsupp.onFinset l.support lF ⋯<VAR>h : lF₀ = 0<GOAL>lF i = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<VAR>p : ℝ≥0∞<VAR>hf : Memℒp f p μ<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<GOAL>Integrable (fun x => ‖f x‖ ^ p.toReal) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<VAR>p : ℝ≥0∞<VAR>hf : Memℒp f p μ<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<GOAL>Memℒp (fun x => ‖f x‖ ^ p.toReal) 1 μ
<VAR>m n : ℤ<GOAL>Odd n.natAbs ↔ Odd n
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>s t u v : Set α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TotallyDisconnectedSpace β<VAR>f✝ : α → β<VAR>S : Set α<VAR>hS : IsPreconnected S<VAR>T : Set β<VAR>inst✝ : DiscreteTopology ↑T<VAR>f : α → β<VAR>hc : ContinuousOn f S<VAR>hTm : MapsTo f S T<VAR>hne : T.Nonempty<GOAL>∃ y ∈ T, EqOn f (const α y) S
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>s t u v : Set α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TotallyDisconnectedSpace β<VAR>f✝ : α → β<VAR>T : Set β<VAR>inst✝ : DiscreteTopology ↑T<VAR>f : α → β<VAR>hne : T.Nonempty<VAR>hS : IsPreconnected ∅<VAR>hc : ContinuousOn f ∅<VAR>hTm : MapsTo f ∅ T<GOAL>∃ y ∈ T, EqOn f (const α y) ∅
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>s t u v : Set α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TotallyDisconnectedSpace β<VAR>f✝ : α → β<VAR>S : Set α<VAR>hS : IsPreconnected S<VAR>T : Set β<VAR>inst✝ : DiscreteTopology ↑T<VAR>f : α → β<VAR>hc : ContinuousOn f S<VAR>hTm : MapsTo f S T<VAR>hne : T.Nonempty<VAR>x : α<VAR>hx : x ∈ S<GOAL>∃ y ∈ T, EqOn f (const α y) S
<VAR>α : Type u_1<VAR>ι : Sort u_3<VAR>β : Sort u_2<VAR>S : ι → Set α<VAR>f : (i : ι) → ↑(S i) → β<VAR>hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩<VAR>T : Set α<VAR>hT : T ⊆ iUnion S<VAR>hT' : T = iUnion S<VAR>c : ↑T<VAR>ci : (i : ι) → ↑(S i)<VAR>hci : ∀ (i : ι), ↑(ci i) = ↑c<VAR>cβ : β<VAR>h : ∀ (i : ι), f i (ci i) = cβ<GOAL>iUnionLift S f hf T hT c = cβ
<VAR>α : Type u_1<VAR>ι : Sort u_3<VAR>β : Sort u_2<VAR>S : ι → Set α<VAR>f : (i : ι) → ↑(S i) → β<VAR>hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩<VAR>T : Set α<VAR>hT : T ⊆ iUnion S<VAR>hT' : T = iUnion S<VAR>c : ↑T<VAR>ci : (i : ι) → ↑(S i)<VAR>hci : ∀ (i : ι), ↑(ci i) = ↑c<VAR>cβ : β<VAR>h : ∀ (i : ι), f i (ci i) = cβ<VAR>i : ι<VAR>hi : ↑c ∈ S i<GOAL>iUnionLift S f hf T hT c = cβ
<VAR>α : Type u_1<VAR>ι : Sort u_3<VAR>β : Sort u_2<VAR>S : ι → Set α<VAR>f : (i : ι) → ↑(S i) → β<VAR>hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩<VAR>T : Set α<VAR>hT : T ⊆ iUnion S<VAR>hT' : T = iUnion S<VAR>c : ↑T<VAR>ci : (i : ι) → ↑(S i)<VAR>hci : ∀ (i : ι), ↑(ci i) = ↑c<VAR>cβ : β<VAR>h : ∀ (i : ι), f i (ci i) = cβ<VAR>i : ι<VAR>hi : ↑c ∈ S i<VAR>this : ci i = ⟨↑c, hi⟩<GOAL>iUnionLift S f hf T hT c = cβ
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Multiset α<GOAL>(Finset.Ico s t).card = ∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s) - 1
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>W X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>t : PushoutCocone f g<GOAL>t.ι.app WalkingSpan.zero = f ≫ t.inl
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>W X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>t : PushoutCocone f g<VAR>w : (span f g).map fst ≫ t.ι.app WalkingSpan.left = t.ι.app WalkingSpan.zero ≫ ((Functor.const WalkingSpan).obj t.pt).map fst<GOAL>t.ι.app WalkingSpan.zero = f ≫ t.inl
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>W X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>t : PushoutCocone f g<VAR>w : f ≫ t.inl = t.ι.app WalkingSpan.zero ≫ 𝟙 t.pt<GOAL>t.ι.app WalkingSpan.zero = f ≫ t.inl
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁵ : CommRing R<VAR>M N : Matrix m m R<VAR>b : m → α<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : Fintype m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>inst✝ : LinearOrder m<VAR>h : M.BlockTriangular id<VAR>this : DecidableEq R<GOAL>M.det = ∏ i : m, M i i
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : DecidableEq L<VAR>inst✝⁶ : Algebra R K<VAR>inst✝⁵ : IsFractionRing R K<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra R L<VAR>inst✝¹ : IsScalarTower R K L<VAR>inst✝ : IsDomain R<VAR>I : FractionalIdeal R⁰ (FractionRing R)<VAR>hI : I ≠ 0<GOAL>I.num ∈ (Ideal R)⁰
<VAR>E : Type uE<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<GOAL>(𝓝[range ↑I] ↑(extChartAt I c) c).HasBasis (fun x => True) fun f => closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I
<VAR>E : Type uE<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<GOAL>∀ (i : ℝ), 0 < i ∧ closedBall (↑(extChartAt I c) c) i ∩ range ↑I ⊆ (extChartAt I c).target → ∃ i', True ∧ closedBall (↑(extChartAt I c) c) i'.rOut ∩ range ↑I ⊆ closedBall (↑(extChartAt I c) c) i ∩ range ↑I
<VAR>E : Type uE<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<GOAL>∀ (i' : SmoothBumpFunction I c), True → closedBall (↑(extChartAt I c) c) i'.rOut ∩ range ↑I ∈ 𝓝[range ↑I] ↑(extChartAt I c) c
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : SemilatticeSup α<VAR>a✝ b✝ c d a b : α<GOAL>a ⊔ b = b ⊔ a
<VAR>M : Type u_1<VAR>G : Type u_2<VAR>inst✝ : Monoid M<VAR>u : Mˣ<VAR>x : M<GOAL>↑u * x = ↑u * x * ↑u⁻¹ * ↑u
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>n : ℕ<VAR>x : α<GOAL>(l ++ [x]).rtake (n + 1) = l.rtake n ++ [x]
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : CommGroupWithZero G₀<VAR>a✝ b✝ c d a b : G₀<VAR>hc : c ≠ 0<GOAL>c / a / (c / b) = b / a
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>h : q.degree ≤ p.degree ∧ p ≠ 0<VAR>hq : q.Monic<VAR>hp : p.leadingCoeff ≠ 0<VAR>hq0 : q ≠ 0<GOAL>↑q.natDegree ≤ ↑p.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>h : q.degree ≤ p.degree ∧ p ≠ 0<VAR>hq : q.Monic<VAR>hp : p.leadingCoeff ≠ 0<VAR>hq0 : q ≠ 0<GOAL>q.degree ≤ p.degree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>h : q.degree ≤ p.degree ∧ p ≠ 0<VAR>hq : q.Monic<VAR>hp : p.leadingCoeff ≠ 0<VAR>hq0 : q ≠ 0<VAR>hlt : q.natDegree ≤ p.natDegree<GOAL>p.degree = (q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).degree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>h : q.degree ≤ p.degree ∧ p ≠ 0<VAR>hq : q.Monic<VAR>hp : p.leadingCoeff ≠ 0<VAR>hq0 : q ≠ 0<VAR>hlt : q.natDegree ≤ p.natDegree<GOAL>p.leadingCoeff = (q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).leadingCoeff
<VAR>x✝ y z x : ℝ<VAR>hx : x ≠ 0<VAR>p : ℝ<GOAL>HasStrictDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x
<VAR>x✝ y z x : ℝ<VAR>hx✝ : x ≠ 0<VAR>p : ℝ<VAR>hx : x < 0<GOAL>HasStrictDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x
<VAR>x✝ y z x : ℝ<VAR>hx✝ : x ≠ 0<VAR>p : ℝ<VAR>hx : 0 < x<GOAL>HasStrictDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>x : R<VAR>n : ℕ<GOAL>eval x (↑n * p) = ↑n * eval x p
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>s : KernelFork f<GOAL>s.π.app one = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>n : ℕ<VAR>a : ⨂[R]^n M<GOAL>(cast R M ⋯) (GradedMonoid.GMul.mul a GradedMonoid.GOne.one) = a
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>n : ℕ<VAR>a : ⨂[R]^n M<GOAL>(cast R M ⋯) (mulEquiv (a ⊗ₜ[R] (tprod R) Fin.elim0)) = a
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<GOAL>ModuleCat.ofHom (dOne A) ≫ ModuleCat.ofHom (dTwo A) = 0
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>h1 : ↑(oneCochainsLequiv A) ≫ ModuleCat.ofHom (dOne A) = (inhomogeneousCochains A).d 1 2 ≫ ↑(twoCochainsLequiv A)<GOAL>ModuleCat.ofHom (dOne A) ≫ ModuleCat.ofHom (dTwo A) = 0
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>h1 : ↑(oneCochainsLequiv A) ≫ ModuleCat.ofHom (dOne A) = (inhomogeneousCochains A).d 1 2 ≫ ↑(twoCochainsLequiv A)<VAR>h2 : ↑(twoCochainsLequiv A) ≫ ModuleCat.ofHom (dTwo A) = (inhomogeneousCochains A).d 2 3 ≫ ↑(threeCochainsLequiv A)<GOAL>ModuleCat.ofHom (dOne A) ≫ ModuleCat.ofHom (dTwo A) = 0
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>h1 : (oneCochainsLequiv A).toModuleIso.hom ≫ ModuleCat.ofHom (dOne A) = (inhomogeneousCochains A).d 1 2 ≫ (twoCochainsLequiv A).toModuleIso.hom<VAR>h2 : (twoCochainsLequiv A).toModuleIso.hom ≫ ModuleCat.ofHom (dTwo A) = (inhomogeneousCochains A).d 2 3 ≫ (threeCochainsLequiv A).toModuleIso.hom<GOAL>ModuleCat.ofHom (dOne A) ≫ ModuleCat.ofHom (dTwo A) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>x : α<GOAL>(pure x).HasBasis (fun x => True) fun x_1 => {x}
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s : Set α<GOAL>∀ u ∈ {U | IsOpen U}, IsOpen u
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s : Set α<GOAL>∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v ∈ {U | IsOpen U}, a ∈ v ∧ v ⊆ u
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>J : C<VAR>hP : PreservesFiniteColimits (preadditiveYonedaObj J)<GOAL>Injective J
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>J : C<VAR>hP : PreservesFiniteColimits (preadditiveYonedaObj J)<GOAL>(preadditiveYonedaObj J).PreservesEpimorphisms
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>h0 : p ≠ 0<VAR>h_top : ¬p = ⊤<GOAL>eLpNorm 0 p μ = 0
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>inst✝ : IsStrictOrder α r<VAR>f : (fun x x_1 => x > x_1) ↪r r<VAR>k : ℕ<GOAL>¬Acc r (f k)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>inst✝ : IsStrictOrder α r<VAR>f : (fun x x_1 => x > x_1) ↪r r<VAR>k : ℕ<GOAL>Nonempty { f_1 // f k ∈ Set.range ⇑f_1 }
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} C₁<VAR>inst✝² : Category.{v₂, u₂} C₂<VAR>inst✝¹ : Category.{v₃, u₃} C₃<VAR>inst✝ : Category.{v₄, u₄} C₄<VAR>T : C₁ ⥤ C₂<VAR>L : C₁ ⥤ C₃<VAR>R : C₂ ⥤ C₄<VAR>B : C₃ ⥤ C₄<VAR>w : TwoSquare T L R B<VAR>X₂ X₂' : C₂<VAR>X₃ : C₃<VAR>g : R.obj X₂ ⟶ B.obj X₃<VAR>g' : R.obj X₂' ⟶ B.obj X₃<VAR>γ : X₂' ⟶ X₂<VAR>hγ : R.map γ ≫ g = g'<VAR>A : w.CostructuredArrowDownwards g<GOAL>R.map (γ ≫ A.left.hom) ≫ w.app A.left.right ≫ B.map A.hom.right = g'
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} C₁<VAR>inst✝² : Category.{v₂, u₂} C₂<VAR>inst✝¹ : Category.{v₃, u₃} C₃<VAR>inst✝ : Category.{v₄, u₄} C₄<VAR>T : C₁ ⥤ C₂<VAR>L : C₁ ⥤ C₃<VAR>R : C₂ ⥤ C₄<VAR>B : C₃ ⥤ C₄<VAR>w : TwoSquare T L R B<VAR>X₂ X₂' : C₂<VAR>X₃ : C₃<VAR>g : R.obj X₂ ⟶ B.obj X₃<VAR>g' : R.obj X₂' ⟶ B.obj X₃<VAR>γ : X₂' ⟶ X₂<VAR>hγ : R.map γ ≫ g = g'<VAR>A A' : w.CostructuredArrowDownwards g<VAR>φ : A ⟶ A'<GOAL>(γ ≫ A.left.hom) ≫ T.map φ.left.right = γ ≫ A'.left.hom
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} C₁<VAR>inst✝² : Category.{v₂, u₂} C₂<VAR>inst✝¹ : Category.{v₃, u₃} C₃<VAR>inst✝ : Category.{v₄, u₄} C₄<VAR>T : C₁ ⥤ C₂<VAR>L : C₁ ⥤ C₃<VAR>R : C₂ ⥤ C₄<VAR>B : C₃ ⥤ C₄<VAR>w : TwoSquare T L R B<VAR>X₂ X₂' : C₂<VAR>X₃ : C₃<VAR>g : R.obj X₂ ⟶ B.obj X₃<VAR>g' : R.obj X₂' ⟶ B.obj X₃<VAR>γ : X₂' ⟶ X₂<VAR>hγ : R.map γ ≫ g = g'<VAR>A A' : w.CostructuredArrowDownwards g<VAR>φ : A ⟶ A'<GOAL>L.map φ.left.right ≫ A'.hom.right = A.hom.right
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} C₁<VAR>inst✝² : Category.{v₂, u₂} C₂<VAR>inst✝¹ : Category.{v₃, u₃} C₃<VAR>inst✝ : Category.{v₄, u₄} C₄<VAR>T : C₁ ⥤ C₂<VAR>L : C₁ ⥤ C₃<VAR>R : C₂ ⥤ C₄<VAR>B : C₃ ⥤ C₄<VAR>w : TwoSquare T L R B<VAR>X₂ X₂' : C₂<VAR>X₃ : C₃<VAR>g : R.obj X₂ ⟶ B.obj X₃<VAR>g' : R.obj X₂' ⟶ B.obj X₃<VAR>γ : X₂' ⟶ X₂<VAR>hγ : R.map γ ≫ g = g'<VAR>A A' : w.CostructuredArrowDownwards g<VAR>φ : A ⟶ A'<GOAL>L.map φ.left.right ≫ A'.hom.right = ((StructuredArrow.pre (R.obj X₂) L B).map ((Comma.mapRight (Functor.fromPUnit (R.obj X₂)) w).map (StructuredArrow.homMk φ.left.right ⋯)) ≫ A'.hom).right
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>M : R[X] → Prop<VAR>f : R[X]<VAR>f0 : f.natDegree ≠ 0<VAR>h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)<VAR>h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)<VAR>h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)<GOAL>f.natDegree = 0 ∨ M f
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>M : R[X] → Prop<VAR>f : R[X]<VAR>f0 : f.natDegree ≠ 0<VAR>h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)<VAR>h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)<VAR>h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)<GOAL>∀ (a : R), (C a).natDegree = 0 ∨ M (C a)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>M : R[X] → Prop<VAR>f : R[X]<VAR>f0 : f.natDegree ≠ 0<VAR>h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)<VAR>h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)<VAR>h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)<GOAL>∀ (p q : R[X]), p.natDegree = 0 ∨ M p → q.natDegree = 0 ∨ M q → (p + q).natDegree = 0 ∨ M (p + q)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>M : R[X] → Prop<VAR>f : R[X]<VAR>f0 : f.natDegree ≠ 0<VAR>h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)<VAR>h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)<VAR>h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)<GOAL>∀ (n : ℕ) (a : R), (C a * X ^ n).natDegree = 0 ∨ M (C a * X ^ n) → (C a * X ^ (n + 1)).natDegree = 0 ∨ M (C a * X ^ (n + 1))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>a a₁ a₂ b b₁ b₂ c d : α<GOAL>Ico a b \ Iio c = Ico (max a c) b
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>f : R →+* S₁<VAR>g : σ → S₁<GOAL>∀ {p : MvPolynomial σ R}, eval₂ f g (p * q) = eval₂ f g p * eval₂ f g q
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>f : R →+* S₁<VAR>g : σ → S₁<GOAL>∀ (a : R) {p : MvPolynomial σ R}, eval₂ f g (p * C a) = eval₂ f g p * eval₂ f g (C a)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>f : R →+* S₁<VAR>g : σ → S₁<GOAL>∀ (p q : MvPolynomial σ R), (∀ {p_1 : MvPolynomial σ R}, eval₂ f g (p_1 * p) = eval₂ f g p_1 * eval₂ f g p) → (∀ {p : MvPolynomial σ R}, eval₂ f g (p * q) = eval₂ f g p * eval₂ f g q) → ∀ {p_1 : MvPolynomial σ R}, eval₂ f g (p_1 * (p + q)) = eval₂ f g p_1 * eval₂ f g (p + q)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>f : R →+* S₁<VAR>g : σ → S₁<GOAL>∀ (p : MvPolynomial σ R) (n : σ), (∀ {p_1 : MvPolynomial σ R}, eval₂ f g (p_1 * p) = eval₂ f g p_1 * eval₂ f g p) → ∀ {p_1 : MvPolynomial σ R}, eval₂ f g (p_1 * (p * X n)) = eval₂ f g p_1 * eval₂ f g (p * X n)
<VAR>a✝ b✝ c✝ d m n a b c : ℤ<VAR>az : ¬a = 0<GOAL>a * b / a ∣ a * b * c / a
<VAR>a✝ b✝ c✝ d m n a b c : ℤ<VAR>az : ¬a = 0<GOAL>b ∣ b * c
<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✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : AddCommMonoid N₂<VAR>inst✝¹⁴ : Module R N₂<VAR>inst✝¹³ : Semiring R₁<VAR>inst✝¹² : Semiring R₂<VAR>inst✝¹¹ : SMulCommClass R R N₂<VAR>inst✝¹⁰ : Semiring S₁<VAR>inst✝⁹ : Semiring S₂<VAR>inst✝⁸ : Module S₁ N₂<VAR>inst✝⁷ : Module S₂ N₂<VAR>inst✝⁶ : SMulCommClass S₁ R N₂<VAR>inst✝⁵ : SMulCommClass S₂ R N₂<VAR>inst✝⁴ : SMulCommClass S₂ S₁ N₂<VAR>σ₁ : R₁ →+* S₁<VAR>σ₂ : R₂ →+* S₂<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype m<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : DecidableEq m<VAR>M : Matrix n m N₂<VAR>x : n → S₁<VAR>y : m → S₂<VAR>x✝³ : n<VAR>x✝² : x✝³ ∈ univ<VAR>x✝¹ : m<VAR>x✝ : x✝¹ ∈ univ<GOAL>(RingHom.id S₂) (y x✝¹) •> (RingHom.id S₁) (x x✝³) •> M x✝³ x✝¹ = x x✝³ •> y x✝¹ •> M x✝³ x✝¹