ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>n : ℕ<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>x : 𝕜<GOAL>‖iteratedFDeriv 𝕜 n f x‖ = ‖iteratedDeriv n f x‖
<VAR>n : ℕ<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f g : (Fin n → ℂ) → E<VAR>c : Fin n → ℂ<VAR>R : Fin n → ℝ<VAR>hf : TorusIntegrable f c R<VAR>hg : TorusIntegrable g c R<GOAL>(∯ (x : Fin n → ℂ) in T(c, R), f x - g x) = (∯ (x : Fin n → ℂ) in T(c, R), f x) - ∯ (x : Fin n → ℂ) in T(c, R), g x
<VAR>X : Type u_1<VAR>a b : FreeAbelianGroup X<GOAL>(a + b).support ⊆ a.support ∪ b.support
<VAR>X : Type u_1<VAR>a b : FreeAbelianGroup X<GOAL>(toFinsupp a + toFinsupp b).support ⊆ (toFinsupp a).support ∪ (toFinsupp b).support
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝¹⁶ : Category.{u_5, u_1} C<VAR>inst✝¹⁵ : HasZeroObject C<VAR>inst✝¹⁴ : HasShift C ℤ<VAR>inst✝¹³ : Preadditive C<VAR>inst✝¹² : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝¹¹ : Pretriangulated C<VAR>inst✝¹⁰ : Category.{?u.49293, u_2} D<VAR>inst✝⁹ : HasZeroObject D<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : Preadditive D<VAR>inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝⁵ : Pretriangulated D<VAR>inst✝⁴ : Category.{u_4, u_3} A<VAR>inst✝³ : Abelian A<VAR>F : C ⥤ A<VAR>inst✝² inst✝¹ : F.IsHomological<VAR>inst✝ : F.ShiftSequence ℤ<VAR>T T' : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>hT' : T' ∈ distinguishedTriangles<VAR>φ : T ⟶ T'<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<GOAL>F.shiftMap T.mor₃ n₀ n₁ ⋯ ≫ (F.shift n₁).map T.mor₁ = 0
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝³ : NonUnitalSemiring R<VAR>inst✝² : NonUnitalSemiring S<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : NonUnitalRingHomClass F R S<VAR>f : F<VAR>x : R<VAR>hx : IsQuasiregular x<GOAL>IsQuasiregular (f x)
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝³ : NonUnitalSemiring R<VAR>inst✝² : NonUnitalSemiring S<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : NonUnitalRingHomClass F R S<VAR>f : F<VAR>x : R<VAR>hx : ∃ y, y + x + x * y = 0 ∧ x + y + y * x = 0<GOAL>∃ y, y + f x + f x * y = 0 ∧ f x + y + y * f x = 0
<VAR>Fq F : Type<VAR>inst✝² : Field Fq<VAR>inst✝¹ : Field F<VAR>inst✝ : DecidableEq (RatFunc Fq)<VAR>p : Fq[X]<VAR>hp : p ≠ 0<GOAL>inftyValuationDef Fq ((algebraMap Fq[X] (RatFunc Fq)) p) = ↑(Multiplicative.ofAdd ↑p.natDegree)
<VAR>Fq F : Type<VAR>inst✝² : Field Fq<VAR>inst✝¹ : Field F<VAR>inst✝ : DecidableEq (RatFunc Fq)<VAR>p : Fq[X]<VAR>hp : p ≠ 0<VAR>hp' : (algebraMap Fq[X] (RatFunc Fq)) p ≠ 0<GOAL>inftyValuationDef Fq ((algebraMap Fq[X] (RatFunc Fq)) p) = ↑(Multiplicative.ofAdd ↑p.natDegree)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : Fintype ι'<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module ℝ F<VAR>v : ι → E<VAR>e : ι' ≃ ι<VAR>K : (ι' → ℝ) ≃ (ι → ℝ) := Equiv.piCongrLeft' (fun _a => ℝ) e<VAR>this : Icc 0 1 = ⇑K '' Icc 0 1<GOAL>(fun t => ∑ i : ι', t i • (v ∘ ⇑e) i) '' Icc 0 1 = (fun t => ∑ i : ι, t i • v i) '' Icc 0 1
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : Fintype ι'<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module ℝ F<VAR>v : ι → E<VAR>e : ι' ≃ ι<VAR>K : (ι' → ℝ) ≃ (ι → ℝ) := Equiv.piCongrLeft' (fun _a => ℝ) e<VAR>this : Icc 0 1 = ⇑K '' Icc 0 1<GOAL>(fun t => ∑ i : ι', t i • (v ∘ ⇑e) i) '' Icc 0 1 = (fun t => ∑ i : ι, t i • v i) ∘ ⇑K '' Icc 0 1
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : Fintype ι'<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module ℝ F<VAR>v : ι → E<VAR>e : ι' ≃ ι<VAR>K : (ι' → ℝ) ≃ (ι → ℝ) := Equiv.piCongrLeft' (fun _a => ℝ) e<VAR>this : Icc 0 1 = ⇑K '' Icc 0 1<VAR>x : E<GOAL>x ∈ (fun t => ∑ i : ι', t i • (v ∘ ⇑e) i) '' Icc 0 1 ↔ x ∈ (fun t => ∑ i : ι, t i • v i) ∘ ⇑K '' Icc 0 1
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : Fintype ι'<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module ℝ F<VAR>v : ι → E<VAR>e : ι' ≃ ι<VAR>K : (ι' → ℝ) ≃ (ι → ℝ) := Equiv.piCongrLeft' (fun _a => ℝ) e<VAR>this✝ : Icc 0 1 = ⇑K '' Icc 0 1<VAR>x : E<VAR>this : ∀ (z : ι' → ℝ), ∑ i : ι, z (e.symm i) • v (e (e.symm i)) = ∑ i : ι', z i • v (e i)<GOAL>x ∈ (fun t => ∑ i : ι', t i • (v ∘ ⇑e) i) '' Icc 0 1 ↔ x ∈ (fun t => ∑ i : ι, t i • v i) ∘ ⇑K '' Icc 0 1
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : Fintype ι'<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module ℝ F<VAR>v : ι → E<VAR>e : ι' ≃ ι<VAR>K : (ι' → ℝ) ≃ (ι → ℝ) := Equiv.piCongrLeft' (fun _a => ℝ) e<VAR>this✝ : Icc 0 1 = ⇑K '' Icc 0 1<VAR>x : E<VAR>this : ∀ (z : ι' → ℝ), ∑ x : ι, z (e.symm x) • v x = ∑ i : ι', z i • v (e i)<GOAL>x ∈ (fun t => ∑ i : ι', t i • (v ∘ ⇑e) i) '' Icc 0 1 ↔ x ∈ (fun t => ∑ i : ι, t i • v i) ∘ ⇑K '' Icc 0 1
<VAR>X✝ X Y Z : LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>e : X ≅ Y<VAR>x : ↑X.toTopCat<GOAL>Hom.stalkMap e.inv (e.hom.val.base x) ≫ Hom.stalkMap e.hom x = X.presheaf.stalkSpecializes ⋯
<VAR>X✝ X Y Z : LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>e : X ≅ Y<VAR>x : ↑X.toTopCat<GOAL>X.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap (𝟙 X) x = X.presheaf.stalkSpecializes ⋯
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>inst✝ : Fintype ι<VAR>p : ι → P<VAR>hi : AffineIndependent k p<VAR>n : ℕ<VAR>hc : Fintype.card ι = n + 1<GOAL>finrank k ↥(vectorSpan k (Set.range p)) = n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalGroup α<VAR>f g : β → α<VAR>a a₁ a₂ : α<VAR>hg : Multipliable g<VAR>hfg : Multipliable fun b => f b / g b<GOAL>Multipliable f
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : X → Y<VAR>y : Y<VAR>hf : Tendsto f (coLindelof X) (𝓝 y)<VAR>hfc : Continuous f<VAR>l : Filter Y<VAR>hne : l.NeBot<VAR>inst✝ : CountableInterFilter l<VAR>hle : l ≤ 𝓟 (insert y (range f))<VAR>hy : ¬ClusterPt y l<GOAL>∃ x ∈ insert y (range f), ClusterPt x l
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : X → Y<VAR>y : Y<VAR>hf : Tendsto f (coLindelof X) (𝓝 y)<VAR>hfc : Continuous f<VAR>l : Filter Y<VAR>hne : l.NeBot<VAR>inst✝ : CountableInterFilter l<VAR>hle : l ≤ 𝓟 (insert y (range f))<VAR>hy : ∃ x, ∃ (_ : x ∈ 𝓝 y), ∃ x_1, ∃ (_ : x_1 ∈ l), Disjoint x x_1<GOAL>∃ x ∈ insert y (range f), ClusterPt x l
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t✝ : Set X<VAR>f : X → Y<VAR>y : Y<VAR>hf : Tendsto f (coLindelof X) (𝓝 y)<VAR>hfc : Continuous f<VAR>l : Filter Y<VAR>hne : l.NeBot<VAR>inst✝ : CountableInterFilter l<VAR>hle : l ≤ 𝓟 (insert y (range f))<VAR>s : Set Y<VAR>hsy : s ∈ 𝓝 y<VAR>t : Set Y<VAR>htl : t ∈ l<VAR>hd : Disjoint s t<GOAL>∃ x ∈ insert y (range f), ClusterPt x l
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t✝ : Set X<VAR>f : X → Y<VAR>y : Y<VAR>hf : Tendsto f (coLindelof X) (𝓝 y)<VAR>hfc : Continuous f<VAR>l : Filter Y<VAR>hne : l.NeBot<VAR>inst✝ : CountableInterFilter l<VAR>hle : l ≤ 𝓟 (insert y (range f))<VAR>s : Set Y<VAR>hsy : s ∈ 𝓝 y<VAR>t : Set Y<VAR>htl : t ∈ l<VAR>hd : Disjoint s t<VAR>K : Set X<VAR>hKc : IsLindelof K<VAR>hKs : Kᶜ ⊆ f ⁻¹' s<GOAL>∃ x ∈ insert y (range f), ClusterPt x l
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t✝ : Set X<VAR>f : X → Y<VAR>y : Y<VAR>hf : Tendsto f (coLindelof X) (𝓝 y)<VAR>hfc : Continuous f<VAR>l : Filter Y<VAR>hne : l.NeBot<VAR>inst✝ : CountableInterFilter l<VAR>hle : l ≤ 𝓟 (insert y (range f))<VAR>s : Set Y<VAR>hsy : s ∈ 𝓝 y<VAR>t : Set Y<VAR>htl : t ∈ l<VAR>hd : Disjoint s t<VAR>K : Set X<VAR>hKc : IsLindelof K<VAR>hKs : Kᶜ ⊆ f ⁻¹' s<VAR>this : f '' K ∈ l<GOAL>∃ x ∈ insert y (range f), ClusterPt x l
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t✝ : Set X<VAR>f : X → Y<VAR>y✝ : Y<VAR>hf : Tendsto f (coLindelof X) (𝓝 y✝)<VAR>hfc : Continuous f<VAR>l : Filter Y<VAR>hne : l.NeBot<VAR>inst✝ : CountableInterFilter l<VAR>hle : l ≤ 𝓟 (insert y✝ (range f))<VAR>s : Set Y<VAR>hsy : s ∈ 𝓝 y✝<VAR>t : Set Y<VAR>htl : t ∈ l<VAR>hd : Disjoint s t<VAR>K : Set X<VAR>hKc : IsLindelof K<VAR>hKs : Kᶜ ⊆ f ⁻¹' s<VAR>this : f '' K ∈ l<VAR>y : Y<VAR>hy : y ∈ f '' K<VAR>hyl : ClusterPt y l<GOAL>∃ x ∈ insert y✝ (range f), ClusterPt x l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : T0Space α<VAR>s : Set α<VAR>h : IsComplete s<VAR>a : α<VAR>ha : ClusterPt a (𝓟 s)<VAR>f : Filter α := 𝓝[s] a<GOAL>a ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : T0Space α<VAR>s : Set α<VAR>h : IsComplete s<VAR>a : α<VAR>ha : ClusterPt a (𝓟 s)<VAR>f : Filter α := 𝓝[s] a<VAR>this : Cauchy f<GOAL>a ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : T0Space α<VAR>s : Set α<VAR>h : IsComplete s<VAR>a : α<VAR>ha : ClusterPt a (𝓟 s)<VAR>f : Filter α := 𝓝[s] a<VAR>this : Cauchy f<VAR>y : α<VAR>ys : y ∈ s<VAR>fy : f ≤ 𝓝 y<GOAL>a ∈ s
<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 : α →ₘ[μ] β<GOAL>MeasureTheory.Integrable (↑f) μ ↔ f.Integrable
<VAR>x₀ : ℝ<VAR>a b : ℕ<VAR>f : ℝ → ℝ<VAR>hab : a ≤ b<VAR>hf : AntitoneOn f (Icc ↑a ↑b)<GOAL>∫ (x : ℝ) in ↑a..↑b, f x ≤ ∑ x ∈ Finset.Ico a b, f ↑x
<VAR>x₀ : ℝ<VAR>a b : ℕ<VAR>f : ℝ → ℝ<VAR>hab : a ≤ b<VAR>hf : AntitoneOn f (Icc ↑a ↑b)<GOAL>∫ (x : ℝ) in ↑a..↑(b - a) + ↑a, f x ≤ ∑ x ∈ Finset.Ico a (b - a + a), f ↑x
<VAR>x₀ : ℝ<VAR>a b : ℕ<VAR>f : ℝ → ℝ<VAR>hab : a ≤ b<VAR>hf : AntitoneOn f (Icc ↑a ↑b)<GOAL>∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x ≤ ∑ x ∈ Finset.Ico (0 + a) (b - a + a), f ↑x
<VAR>x₀ : ℝ<VAR>a b : ℕ<VAR>f : ℝ → ℝ<VAR>hab : a ≤ b<VAR>hf : AntitoneOn f (Icc ↑a ↑b)<GOAL>∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x ≤ ∑ x ∈ Finset.range (b - a), f ↑(a + x)
<VAR>x₀ : ℝ<VAR>a b : ℕ<VAR>f : ℝ → ℝ<VAR>hab : a ≤ b<VAR>hf : AntitoneOn f (Icc ↑a ↑b)<GOAL>∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x ≤ ∑ x ∈ Finset.range (b - a), f (↑a + ↑x)
<VAR>x₀ : ℝ<VAR>a b : ℕ<VAR>f : ℝ → ℝ<VAR>hab : a ≤ b<VAR>hf : AntitoneOn f (Icc ↑a ↑b)<GOAL>AntitoneOn f (Icc (↑a) (↑a + ↑(b - a)))
<VAR>G : Type u<VAR>inst✝ : CommMonoid G<VAR>h : ∀ (g : G), 0 < orderOf g<VAR>h✝ : ExponentExists G<GOAL>exponent G = sSup (Set.range fun g => orderOf g)
<VAR>G : Type u<VAR>inst✝ : CommMonoid G<VAR>h : ∀ (g : G), 0 < orderOf g<VAR>h✝ : ¬ExponentExists G<GOAL>exponent G = sSup (Set.range fun g => orderOf g)
<VAR>L : Type u_1<VAR>inst✝³ : SemilatticeSup L<VAR>inst✝² : TopologicalSpace L<VAR>inst✝¹ : ContinuousSup L<VAR>X : Type u_2<VAR>inst✝ : TopologicalSpace X<VAR>f : ℕ → X → L<VAR>n : ℕ<VAR>s : Set X<VAR>x : X<VAR>hf : ∀ k ≤ n, ContinuousWithinAt (f k) s x<GOAL>ContinuousWithinAt ((partialSups f) n) s x
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : TopologicalSpace F<VAR>proj : Z → B<VAR>e : Pretrivialization F proj<VAR>x✝ : Z<VAR>s : Set B<VAR>x : B<VAR>y : F<GOAL>(x, y) ∈ ↑e.symm ⁻¹' (proj ⁻¹' s) ∩ e.baseSet ×ˢ univ ↔ (x, y) ∈ (s ∩ e.baseSet) ×ˢ univ
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : TopologicalSpace F<VAR>proj : Z → B<VAR>e : Pretrivialization F proj<VAR>x✝ : Z<VAR>s : Set B<VAR>x : B<VAR>y : F<GOAL>x ∈ e.baseSet → (proj (↑e.symm (x, y)) ∈ s ↔ x ∈ s)
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : TopologicalSpace F<VAR>proj : Z → B<VAR>e : Pretrivialization F proj<VAR>x✝ : Z<VAR>s : Set B<VAR>x : B<VAR>y : F<VAR>h : x ∈ e.baseSet<GOAL>proj (↑e.symm (x, y)) ∈ s ↔ x ∈ s
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>M₂ : Type u_5<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>χ : L → R<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>hf : Injective ⇑f<GOAL>LieSubmodule.comap f (weightSpace M₂ χ) = weightSpace M χ
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>M₂ : Type u_5<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>χ : L → R<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>hf : Injective ⇑f<VAR>m : M<VAR>hm : m ∈ LieSubmodule.comap f (weightSpace M₂ χ)<GOAL>m ∈ weightSpace M χ
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>M₂ : Type u_5<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>χ : L → R<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>hf : Injective ⇑f<GOAL>weightSpace M χ ≤ LieSubmodule.comap f (weightSpace M₂ χ)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t u : Multiset α<VAR>h : t ≤ s<GOAL>u + s = u ∪ t ↔ u.Disjoint s ∧ s = t
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t u : Multiset α<VAR>h : t ≤ s<GOAL>u + s = u ∪ t ↔ u + s = u ∪ s ∧ s = t
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>ha : Polynomial.eval a F = 0<GOAL>‖a - a‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : MulAction G α<VAR>inst✝² : MulAction G β<VAR>inst✝¹ : SMul α β<VAR>inst✝ : IsScalarTower G α β<VAR>a : α<VAR>b : β<VAR>h : Injective fun x => x • b<GOAL>stabilizer G (a • b) = stabilizer G a
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : MulAction G α<VAR>inst✝² : MulAction G β<VAR>inst✝¹ : SMul α β<VAR>inst✝ : IsScalarTower G α β<VAR>a✝ : α<VAR>b : β<VAR>h : Injective fun x => x • b<VAR>a : G<VAR>ha : a ∈ stabilizer G (a✝ • b)<GOAL>a ∈ stabilizer G a✝
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>K : Submodule 𝕜 E<VAR>u v : E<VAR>hu : u ∈ K<VAR>hv : v ∈ Kᗮ<GOAL>⟪v, u⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>K : Submodule 𝕜 E<VAR>u v : E<VAR>hu : u ∈ K<VAR>hv : v ∈ Kᗮ<GOAL>⟪u, v⟫_𝕜 = 0
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : R<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>↑(basicOpen (f ^ n)) = ↑(basicOpen f)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝⁵ : TopologicalSpace X<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>inst✝⁴ : TopologicalSpace M₂<VAR>inst✝³ : T2Space M₂<VAR>inst✝² : Mul M₁<VAR>inst✝¹ : Mul M₂<VAR>inst✝ : ContinuousMul M₂<GOAL>IsClosed {f | ∀ (x y : M₁), f (x * y) = f x * f y}
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝⁵ : TopologicalSpace X<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>inst✝⁴ : TopologicalSpace M₂<VAR>inst✝³ : T2Space M₂<VAR>inst✝² : Mul M₁<VAR>inst✝¹ : Mul M₂<VAR>inst✝ : ContinuousMul M₂<GOAL>IsClosed (⋂ i, ⋂ i_1, {x | x (i * i_1) = x i * x i_1})
<VAR>p : ℕ<VAR>hp : Nat.blt 1 p = true<VAR>h : Nat.ble 1 (sMod' (2 ^ p - 1) (p - 2)) = true<GOAL>¬LucasLehmerTest p
<VAR>p : ℕ<VAR>hp : 1 < p<VAR>h : Nat.ble 1 (sMod' (2 ^ p - 1) (p - 2)) = true<GOAL>¬LucasLehmerTest p
<VAR>p : ℕ<VAR>hp : 1 < p<VAR>h : sMod' (2 ^ p - 1) (p - 2) ≠ 0<GOAL>¬LucasLehmerTest p
<VAR>p : ℕ<VAR>hp : 1 < p<VAR>h : sMod' (2 ^ p - 1) (p - 2) ≠ 0<GOAL>¬↑(sMod' (2 ^ p - 1) (p - 2)) = 0
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a✝ b✝ : ℝ<VAR>f✝ g : ℝ → E<VAR>μ✝ : Measure ℝ<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>μ : Measure ℝ<GOAL>‖∫ (x : ℝ) in a..b, f x ∂μ‖ = ‖∫ (x : ℝ) in Ι a b, f x ∂μ‖
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a✝ b✝ : ℝ<VAR>f✝ g : ℝ → E<VAR>μ✝ : Measure ℝ<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>μ : Measure ℝ<GOAL>‖if a ≤ b then 1 else -1‖ * ‖∫ (x : ℝ) in Ι a b, f x ∂μ‖ = ‖∫ (x : ℝ) in Ι a b, f x ∂μ‖
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y P Q : C<VAR>t : BinaryFan P Q<VAR>I : IsLimit t<VAR>s : Cone (pair Q P)<VAR>m : s.pt ⟶ t.swap.pt<VAR>w : ∀ (j : Discrete WalkingPair), m ≫ t.swap.π.app j = s.π.app j<GOAL>m = (fun s => I.lift (BinaryFan.swap s)) s
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y P Q : C<VAR>t : BinaryFan P Q<VAR>I : IsLimit t<VAR>s : Cone (pair Q P)<VAR>m : s.pt ⟶ t.swap.pt<VAR>w : ∀ (j : Discrete WalkingPair), m ≫ t.swap.π.app j = s.π.app j<VAR>h : (∀ (j : Discrete WalkingPair), m ≫ t.π.app j = (BinaryFan.swap s).π.app j) → m = I.lift (BinaryFan.swap s)<GOAL>m = (fun s => I.lift (BinaryFan.swap s)) s
<VAR>a✝ b c d m n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>a n : ℕ<GOAL>a ^ (n + 1) = 0 ↔ a = 0 ∧ n + 1 ≠ 0
<VAR>a✝ b c d m n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>a n : ℕ<GOAL>a = 0 ∧ n ≠ 0 ∨ a = 0 ↔ a = 0 ∧ n + 1 ≠ 0
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>p : α → Prop<GOAL>Continuous p ↔ IsOpen {x | p x}
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>p : α → Prop<GOAL>(∀ (x : α), p x → ∀ᶠ (x : α) in 𝓝 x, p x) ↔ ∀ x ∈ {x | p x}, {x | p x} ∈ 𝓝 x
<VAR>J : Type w<VAR>C✝ : Type u<VAR>inst✝² : Category.{v, u} C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>B : C<VAR>objs : J → C<VAR>arrows : (j : J) → B ⟶ objs j<VAR>inst✝ : HasWidePushout B objs arrows<VAR>X : C<VAR>f : B ⟶ X<VAR>fs : (j : J) → objs j ⟶ X<VAR>w : ∀ (j : J), arrows j ≫ fs j = f<VAR>g : widePushout B objs arrows ⟶ X<VAR>j : J<GOAL>arrows j ≫ (fun j => ι arrows j ≫ g) j = head arrows ≫ g
<VAR>J : Type w<VAR>C✝ : Type u<VAR>inst✝² : Category.{v, u} C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>B : C<VAR>objs : J → C<VAR>arrows : (j : J) → B ⟶ objs j<VAR>inst✝ : HasWidePushout B objs arrows<VAR>X : C<VAR>f : B ⟶ X<VAR>fs : (j : J) → objs j ⟶ X<VAR>w : ∀ (j : J), arrows j ≫ fs j = f<VAR>g : widePushout B objs arrows ⟶ X<VAR>j : J<GOAL>(arrows j ≫ ι arrows j) ≫ g = head arrows ≫ g
<VAR>J : Type w<VAR>C✝ : Type u<VAR>inst✝² : Category.{v, u} C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>B : C<VAR>objs : J → C<VAR>arrows : (j : J) → B ⟶ objs j<VAR>inst✝ : HasWidePushout B objs arrows<VAR>X : C<VAR>f : B ⟶ X<VAR>fs : (j : J) → objs j ⟶ X<VAR>w : ∀ (j : J), arrows j ≫ fs j = f<VAR>g : widePushout B objs arrows ⟶ X<GOAL>g = desc (head arrows ≫ g) (fun j => ι arrows j ≫ g) ⋯
<VAR>J : Type w<VAR>C✝ : Type u<VAR>inst✝² : Category.{v, u} C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>B : C<VAR>objs : J → C<VAR>arrows : (j : J) → B ⟶ objs j<VAR>inst✝ : HasWidePushout B objs arrows<VAR>X : C<VAR>f : B ⟶ X<VAR>fs : (j : J) → objs j ⟶ X<VAR>w : ∀ (j : J), arrows j ≫ fs j = f<VAR>g : widePushout B objs arrows ⟶ X<GOAL>∀ (j : J), ι arrows j ≫ g = ι arrows j ≫ g
<VAR>J : Type w<VAR>C✝ : Type u<VAR>inst✝² : Category.{v, u} C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>B : C<VAR>objs : J → C<VAR>arrows : (j : J) → B ⟶ objs j<VAR>inst✝ : HasWidePushout B objs arrows<VAR>X : C<VAR>f : B ⟶ X<VAR>fs : (j : J) → objs j ⟶ X<VAR>w : ∀ (j : J), arrows j ≫ fs j = f<VAR>g : widePushout B objs arrows ⟶ X<GOAL>head arrows ≫ g = head arrows ≫ g
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : Lattice α<VAR>inst✝¹ : Lattice β<VAR>inst✝ : Lattice γ<GOAL>(fun f => ⇑f) (LatticeHom.id α).withTopWithBot = (fun f => ⇑f) (BoundedLatticeHom.id (WithTop (WithBot α)))
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : Lattice α<VAR>inst✝¹ : Lattice β<VAR>inst✝ : Lattice γ<GOAL>⇑(LatticeHom.id α).withBot.toSupHom = id
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : Lattice α<VAR>inst✝¹ : Lattice β<VAR>inst✝ : Lattice γ<GOAL>⇑(LatticeHom.id (WithBot α)).toSupHom = id
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>p : α × Bool<VAR>l : List (α × Bool)<GOAL>Step (p :: l ++ L₁) (p :: l ++ L₂) ↔ Step L₁ L₂
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CommMonoid β<VAR>s t : Multiset α<VAR>a✝ : α<VAR>m : Multiset ι<VAR>f g : ι → α<VAR>n : ℕ<VAR>a : α<GOAL>(replicate n a).prod = a ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>f : β → γ<VAR>g✝ : γ → α<VAR>η : Kernel β γ<VAR>κ : Kernel α β<VAR>a : α<VAR>g : γ → ℝ≥0∞<VAR>hg : Measurable g<GOAL>∫⁻ (c : γ), g c ∂(η ∘ₖ κ) a = ∫⁻ (b : β), ∫⁻ (c : γ), g c ∂η b ∂κ a
<VAR>α : Type u_1<VAR>inst✝³ : Lattice α<VAR>inst✝² : Group α<VAR>a✝ b : α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>1 ≤ mabs a
<VAR>α : Type u_1<VAR>inst✝³ : Lattice α<VAR>inst✝² : Group α<VAR>a✝ b : α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>1 ≤ mabs a ^ 2
<VAR>α : Type u_1<VAR>inst✝³ : Lattice α<VAR>inst✝² : Group α<VAR>a✝ b : α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>1 ≤ (a ⊔ a⁻¹) * a⁻¹ ⊔ a ^ 2 ⊔ 1
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCancelCommMonoid G<VAR>x : k[G]<VAR>a : G<GOAL>x * of' k G a /ᵒᶠ a = x
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCancelCommMonoid G<VAR>x : k[G]<VAR>a x✝ : G<GOAL>(x * of' k G a /ᵒᶠ a) x✝ = x x✝
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCancelCommMonoid G<VAR>x : k[G]<VAR>a x✝ : G<GOAL>∀ (a_1 : G), a_1 + a = a + x✝ ↔ a_1 = x✝
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCancelCommMonoid G<VAR>x : k[G]<VAR>a x✝ c : G<GOAL>c + a = a + x✝ ↔ c = x✝
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCancelCommMonoid G<VAR>x : k[G]<VAR>a x✝ c : G<GOAL>a + c = a + x✝ ↔ c = x✝