ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type v'<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : StarRing R<VAR>inst✝¹⁴ : NonUnitalSemiring A<VAR>inst✝¹³ : StarRing A<VAR>inst✝¹² : Module R A<VAR>inst✝¹¹ : IsScalarTower R A A<VAR>inst✝¹⁰ : SMulCommClass R A A<VAR>inst✝⁹ : StarModule R A<VAR>inst✝⁸ : NonUnitalSemiring B<VAR>inst✝⁷ : StarRing B<VAR>inst✝⁶ : Module R B<VAR>inst✝⁵ : IsScalarTower R B B<VAR>inst✝⁴ : SMulCommClass R B B<VAR>inst✝³ : StarModule R B<VAR>inst✝² : FunLike F A B<VAR>inst✝¹ : NonUnitalAlgHomClass F R A B<VAR>inst✝ : NonUnitalStarAlgHomClass F R A B<VAR>S : NonUnitalStarSubalgebra R A<VAR>s : Set A<VAR>z : A<GOAL>(∀ x ∈ s, x * z = z * x) → ((∀ x ∈ star s, x * z = z * x) ↔ ∀ x ∈ s, star x * z = z * star x)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>g : Perm α<GOAL>∀ {f : Perm α}, f ∈ g.cycleFactorsFinset → (g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f}
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>g f✝ : Perm α<GOAL>fun {g} => ∀ {f : Perm α}, f ∈ g.cycleFactorsFinset → (g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f}
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>g f✝ : Perm α<GOAL>∀ (σ : Perm α), σ.IsCycle → fun {g} => ∀ {f : Perm α}, f ∈ g.cycleFactorsFinset → (g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f}
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>g f✝ : Perm α<GOAL>∀ (σ τ : Perm α), σ.Disjoint τ → σ.IsCycle → (fun {g} => ∀ {f : Perm α}, f ∈ g.cycleFactorsFinset → (g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f}) → (fun {g} => ∀ {f : Perm α}, f ∈ g.cycleFactorsFinset → (g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f}) → fun {g} => ∀ {f : Perm α}, f ∈ g.cycleFactorsFinset → (g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f}
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<GOAL>m ≤ n.sqrt ↔ m ^ 2 ≤ n
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<GOAL>W.negAddY P Q = (-addU P Q) ^ 3
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Field K<VAR>R₁ : Type u_4<VAR>inst✝³ : CommRing R₁<VAR>inst✝² : IsDomain R₁<VAR>inst✝¹ : Algebra R₁ K<VAR>inst✝ : IsFractionRing R₁ K<VAR>I✝ J✝ I J : FractionalIdeal R₁⁰ K<VAR>h : I * J = 1<GOAL>J = I⁻¹
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Field K<VAR>R₁ : Type u_4<VAR>inst✝³ : CommRing R₁<VAR>inst✝² : IsDomain R₁<VAR>inst✝¹ : Algebra R₁ K<VAR>inst✝ : IsFractionRing R₁ K<VAR>I✝ J✝ I J : FractionalIdeal R₁⁰ K<VAR>h : I * J = 1<VAR>hI : I ≠ 0<GOAL>J = I⁻¹
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Field K<VAR>R₁ : Type u_4<VAR>inst✝³ : CommRing R₁<VAR>inst✝² : IsDomain R₁<VAR>inst✝¹ : Algebra R₁ K<VAR>inst✝ : IsFractionRing R₁ K<VAR>I✝ J✝ I J : FractionalIdeal R₁⁰ K<VAR>h : I * J = 1<VAR>hI : I ≠ 0<GOAL>I * (1 / I) = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Field K<VAR>R₁ : Type u_4<VAR>inst✝³ : CommRing R₁<VAR>inst✝² : IsDomain R₁<VAR>inst✝¹ : Algebra R₁ K<VAR>inst✝ : IsFractionRing R₁ K<VAR>I✝ J✝ I J : FractionalIdeal R₁⁰ K<VAR>h : I * J = 1<VAR>hI : I ≠ 0<GOAL>I * (1 / I) ≤ 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Field K<VAR>R₁ : Type u_4<VAR>inst✝³ : CommRing R₁<VAR>inst✝² : IsDomain R₁<VAR>inst✝¹ : Algebra R₁ K<VAR>inst✝ : IsFractionRing R₁ K<VAR>I✝ J✝ I J : FractionalIdeal R₁⁰ K<VAR>h : I * J = 1<VAR>hI : I ≠ 0<GOAL>1 ≤ I * (1 / I)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Field K<VAR>R₁ : Type u_4<VAR>inst✝³ : CommRing R₁<VAR>inst✝² : IsDomain R₁<VAR>inst✝¹ : Algebra R₁ K<VAR>inst✝ : IsFractionRing R₁ K<VAR>I✝ J✝ I J : FractionalIdeal R₁⁰ K<VAR>h : I * J = 1<VAR>hI : I ≠ 0<GOAL>I * J ≤ I * (I * J / I)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Field K<VAR>R₁ : Type u_4<VAR>inst✝³ : CommRing R₁<VAR>inst✝² : IsDomain R₁<VAR>inst✝¹ : Algebra R₁ K<VAR>inst✝ : IsFractionRing R₁ K<VAR>I✝ J✝ I J : FractionalIdeal R₁⁰ K<VAR>h : I * J = 1<VAR>hI : I ≠ 0<GOAL>J ≤ I * J / I
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Field K<VAR>R₁ : Type u_4<VAR>inst✝³ : CommRing R₁<VAR>inst✝² : IsDomain R₁<VAR>inst✝¹ : Algebra R₁ K<VAR>inst✝ : IsFractionRing R₁ K<VAR>I✝ J✝ I J : FractionalIdeal R₁⁰ K<VAR>h : I * J = 1<VAR>hI : I ≠ 0<GOAL>∀ x ∈ J, ∀ y ∈ I, x * y ∈ I * J
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Field K<VAR>R₁ : Type u_4<VAR>inst✝³ : CommRing R₁<VAR>inst✝² : IsDomain R₁<VAR>inst✝¹ : Algebra R₁ K<VAR>inst✝ : IsFractionRing R₁ K<VAR>I✝ J✝ I J : FractionalIdeal R₁⁰ K<VAR>h : I * J = 1<VAR>hI : I ≠ 0<VAR>y : K<VAR>hy : y ∈ J<VAR>x : K<VAR>hx : x ∈ I<GOAL>y * x ∈ I * J
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Field K<VAR>R₁ : Type u_4<VAR>inst✝³ : CommRing R₁<VAR>inst✝² : IsDomain R₁<VAR>inst✝¹ : Algebra R₁ K<VAR>inst✝ : IsFractionRing R₁ K<VAR>I✝ J✝ I J : FractionalIdeal R₁⁰ K<VAR>h : I * J = 1<VAR>hI : I ≠ 0<VAR>y : K<VAR>hy : y ∈ J<VAR>x : K<VAR>hx : x ∈ I<GOAL>x * y ∈ I * J
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>c : ℂ<VAR>R θ : ℝ<GOAL>circleMap c R θ = c ↔ R = 0
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : TopologicalSpace L<VAR>inst✝³ : TopologicalSpace X<VAR>ι : Type u_3<VAR>inst✝² : SemilatticeSup L<VAR>inst✝¹ : OrderBot L<VAR>inst✝ : ContinuousSup L<VAR>s : Finset ι<VAR>f : ι → X → L<VAR>t : Set X<VAR>x : X<VAR>hs : ∀ i ∈ s, ContinuousAt (f i) x<GOAL>ContinuousAt (s.sup f) x
<VAR>X : Type u_1<VAR>inst✝⁶ : MeasurableSpace X<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : OpensMeasurableSpace X<VAR>μ : Measure X<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : SecondCountableTopology E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>f : X →ᵇ E<GOAL>∫⁻ (x : X), ↑‖f x‖₊ ∂μ ≤ ↑‖f‖₊ * μ Set.univ
<VAR>R : Type u<VAR>inst✝² : Ring R<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsFiltered J<VAR>F : J ⥤ ModuleCatMax R<VAR>r s : R<VAR>x : ↑(M F)<GOAL>(r + s) • x = r • x + s • x
<VAR>R : Type u<VAR>inst✝² : Ring R<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsFiltered J<VAR>F : J ⥤ ModuleCatMax R<VAR>r s : R<VAR>x : ↑(M F)<GOAL>∀ (a : (j : J) × ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙ forget AddMonCat).obj j), (r + s) • Quot.mk (Types.Quot.Rel ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙ forget AddMonCat)) a = r • Quot.mk (Types.Quot.Rel ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙ forget AddMonCat)) a + s • Quot.mk (Types.Quot.Rel ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙ forget AddMonCat)) a
<VAR>R : Type u<VAR>inst✝² : Ring R<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsFiltered J<VAR>F : J ⥤ ModuleCatMax R<VAR>r s : R<VAR>j : J<VAR>x : ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙ forget AddMonCat).obj j<GOAL>(r + s) • Quot.mk (Types.Quot.Rel ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙ forget AddMonCat)) ⟨j, x⟩ = r • Quot.mk (Types.Quot.Rel ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙ forget AddMonCat)) ⟨j, x⟩ + s • Quot.mk (Types.Quot.Rel ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙ forget AddMonCat)) ⟨j, x⟩
<VAR>R : Type u<VAR>inst✝² : Ring R<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsFiltered J<VAR>F : J ⥤ ModuleCatMax R<VAR>r s : R<VAR>j : J<VAR>x : ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙ forget AddMonCat).obj j<GOAL>M.mk F ⟨⟨j, x⟩.fst, r • ⟨j, x⟩.snd + s • ⟨j, x⟩.snd⟩ = AddMonCat.FilteredColimits.M.mk (((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⟨j, ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat).map (𝟙 j)) ⟨j, r • ⟨j, x⟩.snd⟩.snd + ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat).map (𝟙 j)) ⟨j, s • ⟨j, x⟩.snd⟩.snd⟩
<VAR>R : Type u<VAR>inst✝² : Ring R<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsFiltered J<VAR>F : J ⥤ ModuleCatMax R<VAR>r s : R<VAR>j : J<VAR>x : ((((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⋙ forget AddMonCat).obj j<GOAL>M.mk F ⟨j, r • x + s • x⟩ = AddMonCat.FilteredColimits.M.mk (((F ⋙ forget₂ (ModuleCat R) AddCommGrp) ⋙ forget₂ AddCommGrp AddGrp) ⋙ forget₂ AddGrp AddMonCat) ⟨j, ((forget₂ AddGrp AddMonCat).map ((forget₂ AddCommGrp AddGrp).map (LinearMap.toAddMonoidHom (𝟙 (F.obj j))))) (r • x) + ((forget₂ AddGrp AddMonCat).map ((forget₂ AddCommGrp AddGrp).map (LinearMap.toAddMonoidHom (𝟙 (F.obj j))))) (s • 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 S<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Algebra S R<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : Module S N<VAR>inst✝¹ : IsScalarTower S R N<VAR>inst✝ : Invertible 2<VAR>f g : M →ₗ[R] R<VAR>x✝¹ x✝ : M<GOAL>((associated (linMulLin f g)) x✝¹) x✝ = ((⅟2 • ((mul R R).compl₁₂ f g + (mul R R).compl₁₂ g f)) 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 S<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Algebra S R<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : Module S N<VAR>inst✝¹ : IsScalarTower S R N<VAR>inst✝ : Invertible 2<VAR>f g : M →ₗ[R] R<VAR>x✝¹ x✝ : M<GOAL>⅟2 * ((f x✝¹ + f x✝) * (g x✝¹ + g x✝) - f x✝¹ * g x✝¹ - f x✝ * g x✝) = ⅟2 * (f x✝¹ * g x✝) + ⅟2 * (g x✝¹ * f x✝)
<VAR>P : TopCat → Prop<VAR>α : Type w<VAR>inst✝¹ : Finite α<VAR>X : α → CompHausLike P<VAR>inst✝ : HasExplicitFiniteCoproduct X<VAR>B : CompHausLike P<VAR>π : (a : α) → X a ⟶ B<VAR>a : α<VAR>x : (forget (CompHausLike P)).obj (X a)<GOAL>(ι X a ≫ desc X π) x = (π a) x
<VAR>n : ℕ<GOAL>map { toFun := fun d => (n / d, d), inj' := ⋯ } n.divisors = n.divisorsAntidiagonal
<VAR>n : ℕ<GOAL>map (Equiv.prodComm ℕ ℕ).toEmbedding (map { toFun := fun d => (n / d, d), inj' := ⋯ } n.divisors) = map (Equiv.prodComm ℕ ℕ).toEmbedding n.divisorsAntidiagonal
<VAR>n : ℕ<VAR>a✝ : ℕ × ℕ<GOAL>a✝ ∈ map (Equiv.prodComm ℕ ℕ).toEmbedding (map { toFun := fun d => (n / d, d), inj' := ⋯ } n.divisors) ↔ a✝ ∈ map (Equiv.prodComm ℕ ℕ).toEmbedding n.divisorsAntidiagonal
<VAR>n : ℕ<VAR>a✝ : ℕ × ℕ<GOAL>a✝ ∈ map ({ toFun := fun d => (n / d, d), inj' := ⋯ }.trans (Equiv.prodComm ℕ ℕ).toEmbedding) n.divisors ↔ a✝ ∈ map { toFun := fun d => (d, n / d), inj' := ⋯ } n.divisors
<VAR>N : ℕ<VAR>inst✝ : NeZero N<VAR>j : ℤ<GOAL>↑(toCircle ↑j) = cexp (2 * ↑π * I * ↑j / ↑N)
<VAR>N : ℕ<VAR>inst✝ : NeZero N<VAR>j : ℤ<GOAL>cexp (↑(2 * π / 1 * (↑j / ↑N)) * I) = cexp (2 * ↑π * I * ↑j / ↑N)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>k : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>ι : Type u_8<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>r s : R<VAR>x y : M<GOAL>-r • x + r • x = 0
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : Ring 𝕜<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module 𝕜 V<VAR>inst✝¹ : TopologicalSpace P<VAR>inst✝ : AddTorsor V P<VAR>s t : Set P<VAR>x : P<VAR>hs : IsClosed (Subtype.val ⁻¹' s)<GOAL>intrinsicClosure 𝕜 s = s
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : Ring 𝕜<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module 𝕜 V<VAR>inst✝¹ : TopologicalSpace P<VAR>inst✝ : AddTorsor V P<VAR>s t : Set P<VAR>x : P<VAR>hs : IsClosed (Subtype.val ⁻¹' s)<GOAL>s ⊆ range Subtype.val
<VAR>a x✝ z x : ℂ<GOAL>|x⁻¹.arg| = |x.arg|
<VAR>a x✝ z x : ℂ<GOAL>|if x.arg = π then π else -x.arg| = |x.arg|
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>N : Type w<VAR>inst✝⁷ : Semiring 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>inst✝ : IsNoetherian R M<VAR>f : ℕ →o Submodule R M<GOAL>EventuallyConst (⇑f) atTop
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>N : Type w<VAR>inst✝⁷ : Semiring 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>inst✝ : IsNoetherian R M<VAR>f : ℕ →o Submodule R M<GOAL>∃ i, ∀ (j : ℕ), i ≤ j → f i = f j
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀ : Type u_4<VAR>R : Type u_5<VAR>inst✝¹ : MulZeroClass M₀<VAR>inst✝ : NoZeroDivisors M₀<VAR>f g : ι → M₀<VAR>x : ι<GOAL>(x ∈ support fun x => f x * g x) ↔ x ∈ support f ∩ support g
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>hb : b ≠ ⊤<VAR>h : a < b<GOAL>a.toNNReal < b.toNNReal
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>P✝ : Cᵒᵖ ⥤ Type (max v u)<VAR>X✝¹ : C<VAR>R✝ : Presieve X✝¹<VAR>S✝ : Sieve X✝¹<VAR>inst✝¹ : R✝.hasPullbacks<VAR>P : Cᵒᵖ ⥤ Type w<VAR>X✝ : C<VAR>R : Presieve X✝<VAR>S : Sieve X✝<VAR>B : C<VAR>I : Type<VAR>X : I → C<VAR>π : (i : I) → X i ⟶ B<VAR>inst✝ : (Presieve.ofArrows X π).hasPullbacks<VAR>z₁ z₂ : SecondObj P X π<VAR>h : ∀ (ij : I × I), Pi.π (fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij z₁ = Pi.π (fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij z₂<GOAL>z₁ = z₂
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>P✝ : Cᵒᵖ ⥤ Type (max v u)<VAR>X✝¹ : C<VAR>R✝ : Presieve X✝¹<VAR>S✝ : Sieve X✝¹<VAR>inst✝¹ : R✝.hasPullbacks<VAR>P : Cᵒᵖ ⥤ Type w<VAR>X✝ : C<VAR>R : Presieve X✝<VAR>S : Sieve X✝<VAR>B : C<VAR>I : Type<VAR>X : I → C<VAR>π : (i : I) → X i ⟶ B<VAR>inst✝ : (Presieve.ofArrows X π).hasPullbacks<VAR>z₁ z₂ : SecondObj P X π<VAR>h : ∀ (ij : I × I), Pi.π (fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij z₁ = Pi.π (fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij z₂<GOAL>∀ (j : Discrete (I × I)), limit.π (Discrete.functor fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) j z₁ = limit.π (Discrete.functor fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) j z₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>K : Type u_5<VAR>inst✝ : Zero β<VAR>f : α →ₛ β<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>a : α<GOAL>↑(f.restrict s) a = s.indicator (↑f) a
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : TopologicalSpace N<VAR>inst✝² : TopologicalAddGroup N<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>f✝ g f : ContinuousMultilinearMap R (fun x => M) N<VAR>v : ι → M<VAR>i j : ι<VAR>hv : v i = v j<VAR>hne : i ≠ j<GOAL>(∑ σ : Equiv.Perm ι, Equiv.Perm.sign σ • domDomCongr σ f).toFun v = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : TopologicalSpace N<VAR>inst✝² : TopologicalAddGroup N<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>f g x✝² x✝¹ : ContinuousMultilinearMap R (fun x => M) N<VAR>x✝ : ι → M<GOAL>({ toFun := fun f => { toContinuousMultilinearMap := ∑ σ : Equiv.Perm ι, Equiv.Perm.sign σ • domDomCongr σ f, map_eq_zero_of_eq' := ⋯ }, map_zero' := ⋯ }.toFun (x✝² + x✝¹)) x✝ = ({ toFun := fun f => { toContinuousMultilinearMap := ∑ σ : Equiv.Perm ι, Equiv.Perm.sign σ • domDomCongr σ f, map_eq_zero_of_eq' := ⋯ }, map_zero' := ⋯ }.toFun x✝² + { toFun := fun f => { toContinuousMultilinearMap := ∑ σ : Equiv.Perm ι, Equiv.Perm.sign σ • domDomCongr σ f, map_eq_zero_of_eq' := ⋯ }, map_zero' := ⋯ }.toFun x✝¹) x✝
<VAR>p : ℂ<GOAL>(Summable fun n => 1 / ↑n ^ p) ↔ 1 < p.re
<VAR>p : ℂ<GOAL>(Summable fun x => ‖1 / ↑(x + 1) ^ p‖) ↔ Summable fun n => 1 / ↑(n + 1) ^ p.re
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : OrderedSemiring α<VAR>l : Filter β<VAR>f g : β → α<VAR>hf : Tendsto f l atTop<VAR>hg : Tendsto g l atTop<GOAL>Tendsto (fun x => f x * g x) l atTop
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : OrderedSemiring α<VAR>l : Filter β<VAR>f g : β → α<VAR>hf : Tendsto f l atTop<VAR>hg : Tendsto g l atTop<GOAL>g ≤ᶠ[l] fun x => f x * g x
<VAR>x y : ℝ<VAR>hy₀ : 0 ≤ y<VAR>hy₁ : y ≤ π<VAR>hxy : x = cos y<GOAL>arccos x = y
<VAR>R : Type u_1<VAR>inst✝ : CommSemigroup R<VAR>a b : R<GOAL>IsRegular (a * b) ↔ IsRegular a ∧ IsRegular b
<VAR>R : Type u_1<VAR>inst✝ : CommSemigroup R<VAR>a b : R<GOAL>IsRegular (a * b) ↔ IsRegular (a * b) ∧ IsRegular (b * a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : α → M<VAR>s : Set α<VAR>hf : (s ∩ mulSupport f).Finite<GOAL>s ∩ mulSupport f = ↑hf.toFinset ∩ mulSupport f
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : Conservative f μ<VAR>hs : NullMeasurableSet s μ<GOAL>∀ᵐ (x : α) ∂μ, ∀ (k : ℕ), f^[k] x ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : Conservative f μ<VAR>hs : NullMeasurableSet s μ<VAR>k : ℕ<GOAL>∀ᵐ (a : α) ∂μ, f^[k] a ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] a ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : Conservative f μ<VAR>hs : NullMeasurableSet s μ<VAR>k : ℕ<VAR>x : α<VAR>hx : x ∈ f^[k] ⁻¹' s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ f^[k] ⁻¹' s<VAR>hk : f^[k] x ∈ s<GOAL>∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : Conservative f μ<VAR>hs : NullMeasurableSet s μ<VAR>k : ℕ<VAR>x : α<VAR>hx : x ∈ f^[k] ⁻¹' s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ f^[k] ⁻¹' s<VAR>hk : f^[k] x ∈ s<GOAL>∃ᶠ (a : ℕ) in atTop, f^[a + k] x ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : Conservative f μ<VAR>hs : NullMeasurableSet s μ<VAR>k : ℕ<VAR>x : α<VAR>hx : x ∈ f^[k] ⁻¹' s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ f^[k] ⁻¹' s<VAR>hk : f^[k] x ∈ s<VAR>n : ℕ<VAR>hn : f^[n] x ∈ f^[k] ⁻¹' s<GOAL>f^[n + k] x ∈ s
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>m : α → β → γ<VAR>f✝ f₁ f₂ : Filter α<VAR>g✝ g₁ g₂ : Filter β<VAR>h h₁ h₂ : Filter γ<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>u : Set γ<VAR>v : Set δ<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>f : Filter α<VAR>g : Filter β<GOAL>map₂ Prod.mk f g = f ×ˢ g
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.203992, u_1} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>inst✝³ : HasKernels C<VAR>inst✝² : HasCokernels C<VAR>inst✝¹ : HasKernels Cᵒᵖ<VAR>inst✝ : HasCokernels Cᵒᵖ<GOAL>∀ {X Y : (ShortComplex C)ᵒᵖ} (f : X ⟶ Y), (leftHomologyFunctor C).op.map f ≫ ((fun S => (Opposite.unop S).rightHomologyOpIso.symm) Y).hom = ((fun S => (Opposite.unop S).rightHomologyOpIso.symm) X).hom ≫ (opFunctor C ⋙ rightHomologyFunctor Cᵒᵖ).map f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t u : Set α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>e : α ≃ᵐ β<VAR>s : Set β<GOAL>⇑e.symm '' s = ⇑e ⁻¹' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<VAR>g : α → α<VAR>h : Function.Commute f g<GOAL>minimalPeriod (f ∘ g) x ∣ (minimalPeriod f x).lcm (minimalPeriod g x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<VAR>g : α → α<VAR>h : Function.Commute f g<GOAL>IsPeriodicPt (f ∘ g) ((minimalPeriod f x).lcm (minimalPeriod g x)) x
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>ι✝ : Type w<VAR>ι'✝ : Type w'<VAR>inst✝² : StrongRankCondition R<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>b : Basis ι R M<VAR>ι' : Type u_2<VAR>inst✝ : Fintype ι'<VAR>v : ι' → M<VAR>hv : LinearIndependent R v<GOAL>Fintype.card ι' ≤ Fintype.card ι
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>ι✝ : Type w<VAR>ι'✝ : Type w'<VAR>inst✝² : StrongRankCondition R<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>b : Basis ι R M<VAR>ι' : Type u_2<VAR>inst✝ : Fintype ι'<VAR>v : ι' → M<VAR>hv : LinearIndependent R v<VAR>this : Nontrivial R := nontrivial_of_invariantBasisNumber R<GOAL>Fintype.card ι' ≤ Fintype.card ι
<VAR>s : Finset ℕ<VAR>m n✝ p n d : ℕ<VAR>h : n.minSqFac = some d<GOAL>Prime d
<VAR>s : Finset ℕ<VAR>m n✝ p n d : ℕ<VAR>h : n.minSqFac = some d<VAR>this : n.MinSqFacProp n.minSqFac<GOAL>Prime d
<VAR>s : Finset ℕ<VAR>m n✝ p n d : ℕ<VAR>h : n.minSqFac = some d<VAR>this : n.MinSqFacProp (some d)<GOAL>Prime d
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F G : C ⥤ C<VAR>adj : F ⊣ G<VAR>V₁ V₂ : Coalgebra G<VAR>f : V₁ ⟶ V₂<GOAL>F.map f.f ≫ (adj.homEquiv V₂.V V₂.V).symm V₂.str = (adj.homEquiv V₁.V V₁.V).symm V₁.str ≫ f.f
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ✝ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁷ : DecidableEq α'<VAR>inst✝⁶ : DecidableEq β'<VAR>inst✝⁵ : DecidableEq γ✝<VAR>inst✝⁴ : DecidableEq γ'<VAR>inst✝³ : DecidableEq δ<VAR>inst✝² : DecidableEq δ'<VAR>inst✝¹ : DecidableEq ε<VAR>inst✝ : DecidableEq ε'<VAR>f✝ f'✝ : α → β → γ✝<VAR>g✝ g'✝ : α → β → γ✝ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u✝ u' : Finset γ✝<VAR>a a' : α<VAR>b b' : β<VAR>c : γ✝<VAR>γ : Type u_14<VAR>u : Finset γ<VAR>f : α → δ → ε<VAR>g : β → γ → δ<VAR>f' : α → γ → δ'<VAR>g' : β → δ' → ε<VAR>h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)<GOAL>image2 f (↑s) (image2 g ↑t ↑u) = image2 g' (↑t) (image2 f' ↑s ↑u)
<VAR>R✝ : Type u_1<VAR>R : Type u_2<VAR>V : Type u_3<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Module R V<VAR>k : ℕ<VAR>f : LaurentSeries V<VAR>x✝ : ℤ<VAR>h_lt : x✝ < order f - ↑k<GOAL>Ring.choose (x✝ + ↑k) k • f.coeff (x✝ + ↑k) = 0
<VAR>R✝ : Type u_1<VAR>R : Type u_2<VAR>V : Type u_3<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Module R V<VAR>k : ℕ<VAR>f g : LaurentSeries V<VAR>x✝ : ℤ<GOAL>((fun f => ofSuppBddBelow (fun n => Ring.choose (n + ↑k) k • f.coeff (n + ↑k)) ⋯) (f + g)).coeff x✝ = ((fun f => ofSuppBddBelow (fun n => Ring.choose (n + ↑k) k • f.coeff (n + ↑k)) ⋯) f + (fun f => ofSuppBddBelow (fun n => Ring.choose (n + ↑k) k • f.coeff (n + ↑k)) ⋯) g).coeff x✝