ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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.map f (weightSpace M χ) = weightSpace M₂ χ ⊓ f.range
<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₂ χ ⊓ f.range ≤ LieSubmodule.map f (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 : f m ∈ ↑↑(weightSpace M₂ χ)<GOAL>f m ∈ LieSubmodule.map f (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 : f m ∈ ↑↑(weightSpace M₂ χ)<GOAL>∃ m_1, f m_1 ∈ weightSpace M₂ χ ∧ f m_1 = f m
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a b : α<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>h : Associates.mk a ⊓ Associates.mk b ≠ 1<GOAL>∃ p, Prime p ∧ p ∣ a ∧ p ∣ b
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a b : α<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>h : Associates.mk a ⊓ Associates.mk b ≠ 1<VAR>hz : (Associates.mk a).factors ⊓ (Associates.mk b).factors ≠ 0<GOAL>∃ p, Prime p ∧ p ∣ a ∧ p ∣ b
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a b : α<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>h : Associates.mk a ⊓ Associates.mk b ≠ 1<VAR>hz : ↑(factors' a ⊓ factors' b) ≠ 0<GOAL>∃ p, Prime p ∧ p ∣ a ∧ p ∣ b
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a b : α<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>h : Associates.mk a ⊓ Associates.mk b ≠ 1<VAR>hz : ↑(factors' a ⊓ factors' b) ≠ 0<VAR>p0 : Associates α<VAR>p0_irr : Irreducible p0<VAR>p0_mem : ⟨p0, p0_irr⟩ ∈ factors' a ⊓ factors' b<GOAL>∃ p, Prime p ∧ p ∣ a ∧ p ∣ b
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a b : α<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>h : Associates.mk a ⊓ Associates.mk b ≠ 1<VAR>hz : ↑(factors' a ⊓ factors' b) ≠ 0<VAR>p0 : Associates α<VAR>p0_irr : Irreducible p0<VAR>p0_mem : ⟨p0, p0_irr⟩ ∈ factors' a ∩ factors' b<GOAL>∃ p, Prime p ∧ p ∣ a ∧ p ∣ b
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a b : α<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>h : Associates.mk a ⊓ Associates.mk b ≠ 1<VAR>hz : ↑(factors' a ⊓ factors' b) ≠ 0<VAR>p : α<VAR>p0_irr : Irreducible (Associates.mk p)<VAR>p0_mem : ⟨Associates.mk p, p0_irr⟩ ∈ factors' a ∩ factors' b<GOAL>∃ p, Prime p ∧ p ∣ a ∧ p ∣ b
<VAR>n : ℕ∞<VAR>p : ℝ[X]<GOAL>ContDiff ℝ n fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x
<VAR>n : ℕ∞<VAR>p : ℝ[X]<VAR>m : ℕ<GOAL>ContDiff ℝ ↑m fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x
<VAR>E : Type u_1<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>x y : E<VAR>h : SameRay ℝ x y<GOAL>‖x + y‖ = ‖x‖ + ‖y‖
<VAR>E : Type u_1<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>u : E<VAR>a b : ℝ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>h : SameRay ℝ (a • u) (b • u)<GOAL>‖a • u + b • u‖ = ‖a • u‖ + ‖b • u‖
<VAR>r s : ℝ<VAR>hrs : r.IsConjExponent s<VAR>j k : ℤ<VAR>h : r > 0<GOAL>j ∈ {x | ∃ k, beattySeq r k = x} ∨ ∃ k, ↑k < ↑j / r ∧ (↑j + 1) / r ≤ ↑k + 1
<VAR>r s : ℝ<VAR>hrs : r.IsConjExponent s<VAR>j k : ℤ<VAR>h : r > 0<VAR>h✝ : (↑⌈(↑j + 1) / r⌉ - 1) * r < ↑j<GOAL>j ∈ {x | ∃ k, beattySeq r k = x} ∨ ∃ k, ↑k < ↑j / r ∧ (↑j + 1) / r ≤ ↑k + 1
<VAR>r s : ℝ<VAR>hrs : r.IsConjExponent s<VAR>j k : ℤ<VAR>h : r > 0<VAR>h✝ : (↑⌈(↑j + 1) / r⌉ - 1) * r ≥ ↑j<GOAL>j ∈ {x | ∃ k, beattySeq r k = x} ∨ ∃ k, ↑k < ↑j / r ∧ (↑j + 1) / r ≤ ↑k + 1
<VAR>Ω : Type u_1<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : TopologicalSpace Ω<VAR>inst✝² : HasOuterApproxClosed Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ ν : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>h : ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), ↑(f x) ∂μ = ∫⁻ (x : Ω), ↑(f x) ∂ν<VAR>F : Set Ω<VAR>F_closed : IsClosed F<GOAL>μ F = ν F
<VAR>Ω : Type u_1<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : TopologicalSpace Ω<VAR>inst✝² : HasOuterApproxClosed Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ ν : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>h : ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), ↑(f x) ∂μ = ∫⁻ (x : Ω), ↑(f x) ∂ν<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>ν_finite : IsFiniteMeasure ν<GOAL>μ F = ν F
<VAR>Ω : Type u_1<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : TopologicalSpace Ω<VAR>inst✝² : HasOuterApproxClosed Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ ν : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>h : ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), ↑(f x) ∂μ = ∫⁻ (x : Ω), ↑(f x) ∂ν<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>ν_finite : IsFiniteMeasure ν<VAR>obs_μ : Tendsto (fun n => ∫⁻ (x : Ω), ↑((F_closed.apprSeq n) x) ∂μ) atTop (𝓝 (μ F))<GOAL>μ F = ν F
<VAR>Ω : Type u_1<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : TopologicalSpace Ω<VAR>inst✝² : HasOuterApproxClosed Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ ν : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>h : ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), ↑(f x) ∂μ = ∫⁻ (x : Ω), ↑(f x) ∂ν<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>ν_finite : IsFiniteMeasure ν<VAR>obs_μ : Tendsto (fun n => ∫⁻ (x : Ω), ↑((F_closed.apprSeq n) x) ∂μ) atTop (𝓝 (μ F))<VAR>obs_ν : Tendsto (fun n => ∫⁻ (x : Ω), ↑((F_closed.apprSeq n) x) ∂ν) atTop (𝓝 (ν F))<GOAL>μ F = ν F
<VAR>Ω : Type u_1<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : TopologicalSpace Ω<VAR>inst✝² : HasOuterApproxClosed Ω<VAR>inst✝¹ : OpensMeasurableSpace Ω<VAR>μ ν : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>h : ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), ↑(f x) ∂μ = ∫⁻ (x : Ω), ↑(f x) ∂ν<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>ν_finite : IsFiniteMeasure ν<VAR>obs_ν : Tendsto (fun n => ∫⁻ (x : Ω), ↑((F_closed.apprSeq n) x) ∂ν) atTop (𝓝 (ν F))<VAR>obs_μ : Tendsto (fun n => ∫⁻ (x : Ω), ↑((F_closed.apprSeq n) x) ∂ν) atTop (𝓝 (μ F))<GOAL>μ F = ν F
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>W U V : Submodule R M<GOAL>U.dualAnnihilator ⊔ V.dualAnnihilator ≤ (U ⊓ V).dualAnnihilator
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>W U V : Submodule R M<GOAL>U ⊓ V ≤ U.dualAnnihilator.dualCoannihilator ⊓ V.dualAnnihilator.dualCoannihilator
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module R M₁<VAR>inst✝² : StrongRankCondition R<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>p : ι → Submodule R M<VAR>hp : Independent p<GOAL>#{ i // p i ≠ ⊥ } ≤ ↑(finrank R M)
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module R M₁<VAR>inst✝² : StrongRankCondition R<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>p : ι → Submodule R M<VAR>hp : Independent p<GOAL>lift.{v, w} #{ i // p i ≠ ⊥ } ≤ lift.{v, w} ↑(finrank R M)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>p₁ p₂ : P<VAR>v : V<GOAL>v ∈ vectorSpan k {p₁, p₂} ↔ ∃ r, r • (p₂ -ᵥ p₁) = v
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : CosimplicialObject C<VAR>X✝ Y✝ : Augmented C<VAR>η : X✝ ⟶ Y✝<GOAL>η.left ≫ Y✝.hom.app [0] = X✝.hom.app [0] ≫ η.right.app [0]
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : CosimplicialObject C<VAR>X✝ Y✝ : Augmented C<VAR>η : X✝ ⟶ Y✝<GOAL>η.left ≫ Y✝.hom.app [0] = (X✝.hom ≫ η.right).app [0]
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : CosimplicialObject C<VAR>X✝ Y✝ : Augmented C<VAR>η : X✝ ⟶ Y✝<GOAL>η.left ≫ Y✝.hom.app [0] = ((const C).map η.left ≫ Y✝.hom).app [0]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MulOneClass α<VAR>inst✝¹ : LT α<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>h : a < a * b<GOAL>a * 1 < a * b
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<GOAL>(∀ (m : ℕ), m < n + 1 → p m) ↔ (∀ (m : ℕ), m < n → p m) ∧ p n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : ConditionallyCompleteLinearOrder β<VAR>f : Filter α<VAR>F : ι → α → β<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>h₁ : autoParam (∀ i ∈ s, IsCoboundedUnder (fun x x_1 => x ≤ x_1) f (F i)) _auto✝<VAR>h₂ : autoParam (∀ i ∈ s, IsBoundedUnder (fun x x_1 => x ≤ x_1) f (F i)) _auto✝<GOAL>limsup (fun a => s.sup' hs fun i => F i a) f = s.sup' hs fun i => limsup (F i) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : ConditionallyCompleteLinearOrder β<VAR>f : Filter α<VAR>F : ι → α → β<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>h₁ : autoParam (∀ i ∈ s, IsCoboundedUnder (fun x x_1 => x ≤ x_1) f (F i)) _auto✝<VAR>h₂ : autoParam (∀ i ∈ s, IsBoundedUnder (fun x x_1 => x ≤ x_1) f (F i)) _auto✝<VAR>bddsup : IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun a => s.sup' hs fun i => F i a<GOAL>limsup (fun a => s.sup' hs fun i => F i a) f = s.sup' hs fun i => limsup (F i) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : ConditionallyCompleteLinearOrder β<VAR>f : Filter α<VAR>F : ι → α → β<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>h₁ : autoParam (∀ i ∈ s, IsCoboundedUnder (fun x x_1 => x ≤ x_1) f (F i)) _auto✝<VAR>h₂ : autoParam (∀ i ∈ s, IsBoundedUnder (fun x x_1 => x ≤ x_1) f (F i)) _auto✝<VAR>bddsup : IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun a => s.sup' hs fun i => F i a<GOAL>limsup (fun a => s.sup' hs fun i => F i a) f ≤ s.sup' hs fun i => limsup (F i) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : ConditionallyCompleteLinearOrder β<VAR>f : Filter α<VAR>F : ι → α → β<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>h₁ : autoParam (∀ i ∈ s, IsCoboundedUnder (fun x x_1 => x ≤ x_1) f (F i)) _auto✝<VAR>h₂ : autoParam (∀ i ∈ s, IsBoundedUnder (fun x x_1 => x ≤ x_1) f (F i)) _auto✝<VAR>bddsup : IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun a => s.sup' hs fun i => F i a<GOAL>(s.sup' hs fun i => limsup (F i) f) ≤ limsup (fun a => s.sup' hs fun i => F i a) f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace W<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝ : T2Space Y<VAR>compactlyGenerated : ∀ (s : Set Y), IsClosed s ↔ ∀ ⦃K : Set Y⦄, IsCompact K → IsClosed (s ∩ K)<GOAL>IsProperMap f ↔ Continuous f ∧ Tendsto f (cocompact X) (cocompact Y)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace W<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝ : T2Space Y<VAR>compactlyGenerated : ∀ (s : Set Y), IsClosed s ↔ ∀ ⦃K : Set Y⦄, IsCompact K → IsClosed (s ∩ K)<GOAL>(Continuous f ∧ ∀ ⦃K : Set Y⦄, IsCompact K → IsCompact (f ⁻¹' K)) ↔ Continuous f ∧ ∀ (i : Set Y), IsCompact i → (f ⁻¹' i)ᶜ ∈ cocompact X
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace W<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝ : T2Space Y<VAR>compactlyGenerated : ∀ (s : Set Y), IsClosed s ↔ ∀ ⦃K : Set Y⦄, IsCompact K → IsClosed (s ∩ K)<VAR>f_cont : Continuous f<VAR>H : ∀ (i : Set Y), IsCompact i → (f ⁻¹' i)ᶜ ∈ cocompact X<VAR>K : Set Y<VAR>hK : IsCompact K<GOAL>IsCompact (f ⁻¹' K)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace W<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝ : T2Space Y<VAR>compactlyGenerated : ∀ (s : Set Y), IsClosed s ↔ ∀ ⦃K : Set Y⦄, IsCompact K → IsClosed (s ∩ K)<VAR>f_cont : Continuous f<VAR>H : ∀ (i : Set Y), IsCompact i → (f ⁻¹' i)ᶜ ∈ cocompact X<VAR>K : Set Y<VAR>hK : IsCompact K<VAR>K' : Set X<VAR>hK' : IsCompact K'<VAR>hK'y : K'ᶜ ⊆ (f ⁻¹' K)ᶜ<GOAL>IsCompact (f ⁻¹' K)
<VAR>p : ℝ<VAR>n : ℕ<VAR>hp_pos : 0 < p<VAR>hp_le_one : p ≤ 1<GOAL>0 ≤ (1 - p) ^ n * p
<VAR>p : ℝ<VAR>n : ℕ<VAR>hp_pos : 0 < p<VAR>hp_le_one : p ≤ 1<VAR>this : 0 ≤ 1 - p<GOAL>0 ≤ (1 - p) ^ n * p
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x✝ y z : X<VAR>s✝ : Set X<VAR>f g : X → Y<VAR>t s : Set (SeparationQuotient X)<VAR>x : X<GOAL>Filter.map mk (𝓝[mk ⁻¹' s] x) = 𝓝[s] mk x
<VAR>z : ℤ<GOAL>¬z * z % ↑4 = 2 % ↑4
<VAR>z : ℤ<GOAL>¬↑(z * z) = ↑2
<VAR>α✝ : Type u_1<VAR>inst✝¹ : DecidableEq α✝<VAR>s✝ s'✝ : Cycle α✝<VAR>α : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s s' : Cycle α<VAR>hs : s.Nodup<VAR>hs' : s'.Nodup<GOAL>s.formPerm hs = s'.formPerm hs' ↔ s = s' ∨ s.Subsingleton ∧ s'.Subsingleton
<VAR>α✝ : Type u_1<VAR>inst✝¹ : DecidableEq α✝<VAR>s✝ s'✝ : Cycle α✝<VAR>α : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s s' : Cycle α<VAR>hs : s.Nodup<VAR>hs' : s'.Nodup<GOAL>s.formPerm hs = s'.formPerm hs' ↔ s = s' ∨ s.length ≤ 1 ∧ s'.length ≤ 1
<VAR>α✝ : Type u_1<VAR>inst✝¹ : DecidableEq α✝<VAR>s✝ s'✝ : Cycle α✝<VAR>α : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s s' : Cycle α<GOAL>∀ {hs : s.Nodup} {hs' : s'.Nodup}, s.formPerm hs = s'.formPerm hs' ↔ s = s' ∨ s.length ≤ 1 ∧ s'.length ≤ 1
<VAR>α✝ : Type u_1<VAR>inst✝¹ : DecidableEq α✝<VAR>s✝ s'✝ : Cycle α✝<VAR>α : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s s' : Cycle α<GOAL>∀ (a₁ a₂ : List α) {hs : Nodup (Quotient.mk'' a₁)} {hs' : Nodup (Quotient.mk'' a₂)}, formPerm (Quotient.mk'' a₁) hs = formPerm (Quotient.mk'' a₂) hs' ↔ Quotient.mk'' a₁ = Quotient.mk'' a₂ ∨ length (Quotient.mk'' a₁) ≤ 1 ∧ length (Quotient.mk'' a₂) ≤ 1
<VAR>α✝ : Type u_1<VAR>inst✝¹ : DecidableEq α✝<VAR>s✝ s'✝ : Cycle α✝<VAR>α : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s s' : Cycle α<VAR>l l' : List α<GOAL>∀ {hs : Nodup (Quotient.mk'' l)} {hs' : Nodup (Quotient.mk'' l')}, formPerm (Quotient.mk'' l) hs = formPerm (Quotient.mk'' l') hs' ↔ Quotient.mk'' l = Quotient.mk'' l' ∨ length (Quotient.mk'' l) ≤ 1 ∧ length (Quotient.mk'' l') ≤ 1
<VAR>α✝ : Type u_1<VAR>inst✝¹ : DecidableEq α✝<VAR>s✝ s'✝ : Cycle α✝<VAR>α : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s s' : Cycle α<VAR>l l' : List α<GOAL>∀ {hs : l.Nodup} {hs' : l'.Nodup}, l.formPerm = l'.formPerm ↔ l ~r l' ∨ l.length ≤ 1 ∧ l'.length ≤ 1
<VAR>α✝ : Type u_1<VAR>inst✝¹ : DecidableEq α✝<VAR>s✝ s'✝ : Cycle α✝<VAR>α : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s s' : Cycle α<VAR>l l' : List α<VAR>hs : l.Nodup<VAR>hs' : l'.Nodup<GOAL>l.formPerm = l'.formPerm ↔ l ~r l' ∨ l.length ≤ 1 ∧ l'.length ≤ 1
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>n : ℕ<VAR>hn : Odd n<VAR>a : K<VAR>ha : ∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a<GOAL>Irreducible (X ^ n - C a)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>sm : SplitMono f<VAR>F : C ⥤ D<GOAL>F.map f ≫ F.map sm.retraction = 𝟙 (F.obj X)
<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>ι : Type v<VAR>hι : Nonempty ι<VAR>hs : IsCompact s<VAR>t : ι → Set X<VAR>htc : ∀ (i : ι), IsClosed (t i)<VAR>hst : s ∩ ⋂ i, t i = ∅<VAR>hdt : Directed (fun x x_1 => x ⊇ x_1) t<GOAL>s ⊆ ⋃ i, (compl ∘ t) i
<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>ι : Type v<VAR>hι : Nonempty ι<VAR>hs : IsCompact s<VAR>t✝ : ι → Set X<VAR>htc : ∀ (i : ι), IsClosed (t✝ i)<VAR>hst : s ∩ ⋂ i, t✝ i = ∅<VAR>hdt : Directed (fun x x_1 => x ⊇ x_1) t✝<VAR>t : ι<VAR>ht : s ⊆ (compl ∘ t✝) t<GOAL>s ∩ t✝ t = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteLattice α<VAR>f : Filter β<VAR>u : β → α<GOAL>IsCoboundedUnder (fun x x_1 => x ≥ x_1) f u
<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>f : Filter α<VAR>inst✝⁴ : f.NeBot<VAR>R : Type u_7<VAR>inst✝³ : Preorder R<VAR>κ : Type u_8<VAR>inst✝² : AddCommMonoid R<VAR>inst✝¹ : CovariantClass R R (fun a b => a + b) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass R R (fun a b => b + a) fun x x_1 => x ≤ x_1<VAR>u : κ → α → R<VAR>s : Finset κ<GOAL>(∀ k ∈ s, IsBoundedUnder (fun x x_1 => x ≤ x_1) f (u k)) → IsBoundedUnder (fun x x_1 => x ≤ x_1) f (∑ k ∈ s, u k)
<VAR>R : Type u_1<VAR>inst✝⁸ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>N : Type u_3<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R N<VAR>P : Type u_4<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R P<VAR>T : Type u_5<VAR>inst✝¹ : AddCommGroup T<VAR>inst✝ : Module (AdicCompletion I R) T<VAR>f g : AdicCompletion I M →ₗ[AdicCompletion I R] T<VAR>h : ∀ (a : AdicCauchySequence I M), f ((mk I M) a) = g ((mk I M) a)<VAR>x : AdicCompletion I M<GOAL>f x = g x
<VAR>a k : ℕ<VAR>h0 : 0 < a<VAR>h1 : a < k<VAR>n : ℕ<GOAL>π' (k + n) ≤ (filter Prime (range k)).card + (filter Prime (Ico k (k + n))).card
<VAR>a k : ℕ<VAR>h0 : 0 < a<VAR>h1 : a < k<VAR>n : ℕ<GOAL>(filter Prime (Ico 0 k) ∪ filter Prime (Ico k (k + n))).card ≤ (filter Prime (Ico 0 k)).card + (filter Prime (Ico k (k + n))).card
<VAR>a k : ℕ<VAR>h0 : 0 < a<VAR>h1 : a < k<VAR>n : ℕ<GOAL>(filter Prime (range k)).card + (filter Prime (Ico k (k + n))).card ≤ π' k + (filter Prime (Ico k (k + n))).card
<VAR>a k : ℕ<VAR>h0 : 0 < a<VAR>h1 : a < k<VAR>n : ℕ<GOAL>π' k + (filter Prime (Ico k (k + n))).card ≤ π' k + (filter a.Coprime (Ico k (k + n))).card
<VAR>a k : ℕ<VAR>h0 : 0 < a<VAR>h1 : a < k<VAR>n : ℕ<GOAL>filter Prime (Ico k (k + n)) ⊆ filter a.Coprime (Ico k (k + n))
<VAR>a k : ℕ<VAR>h0 : 0 < a<VAR>h1 : a < k<VAR>n : ℕ<GOAL>∀ ⦃x : ℕ⦄, k ≤ x → x < k + n → Prime x → (k ≤ x ∧ x < k + n) ∧ a.Coprime x
<VAR>a k : ℕ<VAR>h0 : 0 < a<VAR>h1 : a < k<VAR>n : ℕ<GOAL>π' k + (filter a.Coprime (Ico k (k + n))).card ≤ π' k + φ a * (n / a + 1)
<VAR>a k : ℕ<VAR>h0 : 0 < a<VAR>h1 : a < k<VAR>n : ℕ<GOAL>(filter a.Coprime (Ico k (k + n))).card ≤ φ a * (n / a + 1)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>inst✝¹ : Nonempty ↥s<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>p : P<GOAL>orthogonalProjectionFn s p ∈ mk' p s.directionᗮ
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>inst✝¹ : Nonempty ↥s<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>p : P<GOAL>↑s ∩ ↑(mk' p s.directionᗮ) ⊆ ↑(mk' p s.directionᗮ)
<VAR>n a : ℕ<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>pp : Periodic p a<GOAL>card (filter p (Ico n (n + a))) = count p a
<VAR>n a : ℕ<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>pp : Periodic p a<GOAL>Multiset.count True (map p (Ico n (n + a))) = Multiset.count True (map (p ∘ fun x => x % a) (Ico n (n + a)))
<VAR>n a : ℕ<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>pp : Periodic p a<GOAL>p = p ∘ fun x => x % a
<VAR>n✝ a : ℕ<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>pp : Periodic p a<VAR>n : ℕ<GOAL>p n = (p ∘ fun x => x % a) n
<VAR>α✝ β✝ : Type u_1<VAR>a✝¹ : α✝ → PGame<VAR>a✝ : β✝ → PGame<VAR>o : (PGame.mk α✝ β✝ a✝¹ a✝).Numeric<VAR>j : (PGame.mk α✝ β✝ a✝¹ a✝).RightMoves<GOAL>((PGame.mk α✝ β✝ a✝¹ a✝).moveRight j).Numeric
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>r : R<VAR>f : R[X]<GOAL>(taylor r) X = X + C r
<VAR>α : Type v<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>n : ℕ<VAR>m : M<VAR>a : α<GOAL>m ^ (n + period m a) • a = m ^ n • a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>hns : n ≤ s.card<GOAL>∃ t ⊆ s, t.card = n
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Semiring α<VAR>i j : n<VAR>c : α<VAR>i' j' : n<VAR>inst✝ : Fintype n<VAR>a : n<VAR>M : Matrix n n α<GOAL>(M * stdBasisMatrix i j c) a j = M a i * c
<VAR>M : Type u_1<VAR>S T : Set M<VAR>a✝ b✝ c : M<VAR>inst✝ : Mul M<VAR>h : IsMulCentral c<VAR>a b : M<GOAL>a * b * c = a * c * b
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>n G : Type v<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>M✝ : Matrix n n R<VAR>p✝ : ℕ<VAR>inst✝ : Fact (Nat.Prime p✝)<VAR>M : Matrix n n R<VAR>a✝ : Nontrivial R<VAR>t : R[T;T⁻¹] := T 1<VAR>t_inv : R[T;T⁻¹] := T (-1)<VAR>p : R[T;T⁻¹] := ((scalar n) t - M.map ⇑LaurentPolynomial.C).det<VAR>q : R[T;T⁻¹] := (1 - (scalar n) t * M.map ⇑LaurentPolynomial.C).det<GOAL>M.charpoly.reverse = M.charpolyRev
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>n G : Type v<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>M✝ : Matrix n n R<VAR>p✝ : ℕ<VAR>inst✝ : Fact (Nat.Prime p✝)<VAR>M : Matrix n n R<VAR>a✝ : Nontrivial R<VAR>t : R[T;T⁻¹] := T 1<VAR>t_inv : R[T;T⁻¹] := T (-1)<VAR>p : R[T;T⁻¹] := ((scalar n) t - M.map ⇑LaurentPolynomial.C).det<VAR>q : R[T;T⁻¹] := (1 - (scalar n) t * M.map ⇑LaurentPolynomial.C).det<VAR>ht : t_inv * t = 1<GOAL>M.charpoly.reverse = M.charpolyRev
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>n G : Type v<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>M✝ : Matrix n n R<VAR>p✝ : ℕ<VAR>inst✝ : Fact (Nat.Prime p✝)<VAR>M : Matrix n n R<VAR>a✝ : Nontrivial R<VAR>t : R[T;T⁻¹] := T 1<VAR>t_inv : R[T;T⁻¹] := T (-1)<VAR>p : R[T;T⁻¹] := ((scalar n) t - M.map ⇑LaurentPolynomial.C).det<VAR>q : R[T;T⁻¹] := (1 - (scalar n) t * M.map ⇑LaurentPolynomial.C).det<VAR>ht : t_inv * t = 1<VAR>hp : toLaurentAlg M.charpoly = p<GOAL>M.charpoly.reverse = M.charpolyRev