ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>_mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>mβ : MeasurableSpace β<VAR>mβ' : MeasurableSpace β'<VAR>f' : Ω → β<VAR>g' : Ω → β'<VAR>hfg : IndepFun f g μ<VAR>hf : f =ᶠ[ae μ] f'<VAR>hg : g =ᶠ[ae μ] g'<GOAL>f =ᶠ[ae μ] 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>_mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>mβ : MeasurableSpace β<VAR>mβ' : MeasurableSpace β'<VAR>f' : Ω → β<VAR>g' : Ω → β'<VAR>hfg : IndepFun f g μ<VAR>hf : f =ᶠ[ae μ] f'<VAR>hg : g =ᶠ[ae μ] g'<GOAL>g =ᶠ[ae μ] g'
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>B✝ B' I✝ J D X : Set α<VAR>e f : α<VAR>M : Matroid α<VAR>I B : Set α<VAR>hI : M.Indep I<VAR>hInotmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | M.Indep I}<VAR>hB : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | M.Indep I}<GOAL>∃ x ∈ B \ I, M.Indep (insert x I)
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>B✝ B' I✝ J D X : Set α<VAR>e f : α<VAR>M : Matroid α<VAR>I B : Set α<VAR>hI : M.Indep I<VAR>hB : M.Indep B ∧ ∀ ⦃y : Set α⦄, M.Indep y → B ⊆ y → B = y<VAR>hInotmax : ∃ x, M.Indep x ∧ I ⊆ x ∧ ¬I = x<GOAL>∃ x ∈ B \ I, M.Indep (insert x I)
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>B✝ B' I✝ J D X : Set α<VAR>e f : α<VAR>M : Matroid α<VAR>I B : Set α<VAR>hI : M.Indep I<VAR>hB : M.Indep B ∧ ∀ ⦃y : Set α⦄, M.Indep y → B ⊆ y → B = y<VAR>hInotmax : ∃ x, M.Indep x ∧ I ⊆ x ∧ ¬I = x<VAR>hIb : M.Base I<GOAL>False
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>B✝ B' I✝ J D X : Set α<VAR>e f : α<VAR>M : Matroid α<VAR>I B : Set α<VAR>hI : M.Indep I<VAR>hB : M.Indep B ∧ ∀ ⦃y : Set α⦄, M.Indep y → B ⊆ y → B = y<VAR>hInotmax : ∃ x, M.Indep x ∧ I ⊆ x ∧ ¬I = x<GOAL>M.Base B
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra S R<VAR>inst✝⁷ : Module S M<VAR>inst✝⁶ : IsScalarTower S R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R' M'<VAR>inst✝² : Algebra R R'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : IsScalarTower R R' M'<VAR>f : M →ₗ[R] M'<VAR>p : R[X]<VAR>q : PolynomialModule R M<GOAL>(map R' f) (p • q) = Polynomial.map (algebraMap R R') p • (map R' f) q
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra S R<VAR>inst✝⁷ : Module S M<VAR>inst✝⁶ : IsScalarTower S R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R' M'<VAR>inst✝² : Algebra R R'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : IsScalarTower R R' M'<VAR>f : M →ₗ[R] M'<VAR>p : R[X]<VAR>q : PolynomialModule R M<GOAL>(map R' f) (p • 0) = Polynomial.map (algebraMap R R') p • (map R' f) 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra S R<VAR>inst✝⁷ : Module S M<VAR>inst✝⁶ : IsScalarTower S R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R' M'<VAR>inst✝² : Algebra R R'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : IsScalarTower R R' M'<VAR>f : M →ₗ[R] M'<VAR>p : R[X]<VAR>q : PolynomialModule R M<GOAL>∀ (f_1 g : PolynomialModule R M), (map R' f) (p • f_1) = Polynomial.map (algebraMap R R') p • (map R' f) f_1 → (map R' f) (p • g) = Polynomial.map (algebraMap R R') p • (map R' f) g → (map R' f) (p • (f_1 + g)) = Polynomial.map (algebraMap R R') p • (map R' f) (f_1 + g)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra S R<VAR>inst✝⁷ : Module S M<VAR>inst✝⁶ : IsScalarTower S R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R' M'<VAR>inst✝² : Algebra R R'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : IsScalarTower R R' M'<VAR>f : M →ₗ[R] M'<VAR>p : R[X]<VAR>q : PolynomialModule R M<GOAL>∀ (a : ℕ) (b : M), (map R' f) (p • (single R a) b) = Polynomial.map (algebraMap R R') p • (map R' f) ((single R a) b)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra S R<VAR>inst✝⁷ : Module S M<VAR>inst✝⁶ : IsScalarTower S R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R' M'<VAR>inst✝² : Algebra R R'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : IsScalarTower R R' M'<VAR>f : M →ₗ[R] M'<VAR>p : R[X]<VAR>q : PolynomialModule R M<VAR>i : ℕ<VAR>m : M<GOAL>(map R' f) (p • (single R i) m) = Polynomial.map (algebraMap R R') p • (map R' f) ((single R i) m)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra S R<VAR>inst✝⁷ : Module S M<VAR>inst✝⁶ : IsScalarTower S R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R' M'<VAR>inst✝² : Algebra R R'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : IsScalarTower R R' M'<VAR>f : M →ₗ[R] M'<VAR>q : PolynomialModule R M<VAR>i : ℕ<VAR>m : M<VAR>p✝ q✝ : R[X]<VAR>e₁ : (map R' f) (p✝ • (single R i) m) = Polynomial.map (algebraMap R R') p✝ • (map R' f) ((single R i) m)<VAR>e₂ : (map R' f) (q✝ • (single R i) m) = Polynomial.map (algebraMap R R') q✝ • (map R' f) ((single R i) m)<GOAL>(map R' f) ((p✝ + q✝) • (single R i) m) = Polynomial.map (algebraMap R R') (p✝ + q✝) • (map R' f) ((single R i) m)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra S R<VAR>inst✝⁷ : Module S M<VAR>inst✝⁶ : IsScalarTower S R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R' M'<VAR>inst✝² : Algebra R R'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : IsScalarTower R R' M'<VAR>f : M →ₗ[R] M'<VAR>q : PolynomialModule R M<VAR>i : ℕ<VAR>m : M<VAR>n✝ : ℕ<VAR>a✝ : R<GOAL>(map R' f) ((monomial n✝) a✝ • (single R i) m) = Polynomial.map (algebraMap R R') ((monomial n✝) a✝) • (map R' f) ((single R i) m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>h : a ∉ s<GOAL>(insert a s).card = s.card + 1
<VAR>s : ℂ<GOAL>(fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π
<VAR>s : ℂ<VAR>h1 : AnalyticOn ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ<GOAL>(fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π
<VAR>s : ℂ<VAR>h1 : AnalyticOn ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ<VAR>h2 : AnalyticOn ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ<VAR>h3 : Tendsto ofReal' (𝓝[≠] 1) (𝓝[≠] 1)<GOAL>(fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π
<VAR>s : ℂ<VAR>h1 : AnalyticOn ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ<VAR>h2 : AnalyticOn ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ<VAR>h3 : Tendsto ofReal' (𝓝[≠] 1) (𝓝[≠] 1)<GOAL>∃ᶠ (x : ℝ) in 𝓝[≠] 1, (Gamma ↑x)⁻¹ * (Gamma (↑x + 1 / 2))⁻¹ = (Gamma (2 * ↑x))⁻¹ * 2 ^ (2 * ↑x - 1) / ↑√π
<VAR>s : ℂ<VAR>h1 : AnalyticOn ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ<VAR>h2 : AnalyticOn ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ<VAR>h3 : Tendsto ofReal' (𝓝[≠] 1) (𝓝[≠] 1)<GOAL>∀ᶠ (x : ℝ) in 𝓝 1, (Gamma ↑x)⁻¹ * (Gamma (↑x + 1 / 2))⁻¹ = (Gamma (2 * ↑x))⁻¹ * 2 ^ (2 * ↑x - 1) / ↑√π
<VAR>s : ℂ<VAR>h1 : AnalyticOn ℂ (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ<VAR>h2 : AnalyticOn ℂ (fun z => (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ<VAR>h3 : Tendsto ofReal' (𝓝[≠] 1) (𝓝[≠] 1)<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>(Gamma ↑t)⁻¹ * (Gamma (↑t + 1 / 2))⁻¹ = (Gamma (2 * ↑t))⁻¹ * 2 ^ (2 * ↑t - 1) / ↑√π
<VAR>α : Type u_1<VAR>g : GenContFract α<VAR>n : ℕ<GOAL>g.TerminatedAt n ↔ g.s.TerminatedAt n
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝² : LinearOrderedCommSemiring R<VAR>inst✝¹ : ExistsAddOfLE R<VAR>s : Finset ι<VAR>f g : ι → R<VAR>inst✝ : Nontrivial R<GOAL>(∑ i ∈ s, f i * g i) ^ 2 ≤ (∑ i ∈ s, f i ^ 2) * ∑ i ∈ s, g i ^ 2
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝² : LinearOrderedCommSemiring R<VAR>inst✝¹ : ExistsAddOfLE R<VAR>s : Finset ι<VAR>f g : ι → R<VAR>inst✝ : Nontrivial R<VAR>h' : 0 = ∑ i ∈ ?m.33436, g (?m.34208 i) ^ 2<GOAL>(∑ i ∈ s, f i * g i) ^ 2 ≤ (∑ i ∈ s, f i ^ 2) * ∑ i ∈ s, g i ^ 2
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝² : LinearOrderedCommSemiring R<VAR>inst✝¹ : ExistsAddOfLE R<VAR>s : Finset ι<VAR>f g : ι → R<VAR>inst✝ : Nontrivial R<VAR>h' : 0 < ∑ i ∈ ?m.33436, g (?m.34208 i) ^ 2<GOAL>(∑ i ∈ s, f i * g i) ^ 2 ≤ (∑ i ∈ s, f i ^ 2) * ∑ i ∈ s, g i ^ 2
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝² : LinearOrderedCommSemiring R<VAR>inst✝¹ : ExistsAddOfLE R<VAR>s : Finset ι<VAR>f g : ι → R<VAR>inst✝ : Nontrivial R<VAR>h' : 0 < ∑ i ∈ s, g i ^ 2<GOAL>(∑ i ∈ s, f i * g i) ^ 2 ≤ (∑ i ∈ s, f i ^ 2) * ∑ i ∈ s, g i ^ 2
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝² : LinearOrderedCommSemiring R<VAR>inst✝¹ : ExistsAddOfLE R<VAR>s : Finset ι<VAR>f g : ι → R<VAR>inst✝ : Nontrivial R<VAR>h' : 0 < ∑ i ∈ s, g i ^ 2<GOAL>(∑ i ∈ s, g i ^ 2) * (∑ j ∈ s, f j * g j) ^ 2 + (∑ i ∈ s, g i ^ 2) * (∑ i ∈ s, f i * g i) ^ 2 ≤ (∑ i ∈ s, g i ^ 2) * (∑ j ∈ s, f j * g j) ^ 2 + (∑ i ∈ s, g i ^ 2) * ((∑ i ∈ s, f i ^ 2) * ∑ i ∈ s, g i ^ 2)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>P : Karoubi (SimplicialObject C)<VAR>n : ℕ<GOAL>((AlternatingFaceMapComplex.obj (KaroubiFunctorCategoryEmbedding.obj P)).d (n + 1) n).f = P.p.app (op [n + 1]) ≫ (AlternatingFaceMapComplex.obj P.X).d (n + 1) n
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>P : Karoubi (SimplicialObject C)<VAR>n : ℕ<GOAL>∑ x : Fin (n + 2), (-1) ^ ↑x • (SimplicialObject.δ (KaroubiFunctorCategoryEmbedding.obj P) x).f = ∑ x : Fin (n + 2), (-1) ^ ↑x • P.p.app (op [n + 1]) ≫ P.X.δ x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f : α → β<VAR>ι : Sort u_2<VAR>t₁ t₂ : TopologicalSpace α<VAR>t₃ : TopologicalSpace β<VAR>h₁ : t₂ ≤ t₁<VAR>h₂ : Continuous f<GOAL>Continuous f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f : α → β<VAR>ι : Sort u_2<VAR>t₁ t₂ : TopologicalSpace α<VAR>t₃ : TopologicalSpace β<VAR>h₁ : t₂ ≤ t₁<VAR>h₂ : t₁ ≤ induced f t₃<GOAL>t₂ ≤ induced f t₃
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hX : autoParam (X ⊆ M.E) _auto✝<VAR>hB : M.Base B<VAR>hBX : B ⊆ X<GOAL>M.Basis B X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hX : autoParam (X ⊆ M.E) _auto✝<VAR>hB : M.Base B<VAR>hBX : B ⊆ X<GOAL>∀ (J : Set α), M.Indep J → B ⊆ J → J ⊆ X → B = J
<VAR>R : Type u_3<VAR>S : Type u_1<VAR>M : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Field S<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S M<VAR>inst✝¹ : IsScalarTower R S M<VAR>B : BilinForm S M<VAR>hB : B.Nondegenerate<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>N : Submodule R M<VAR>hN : Submodule.span S ↑N = ⊤<VAR>x y : ↥(B.dualSubmodule N)<VAR>e : (B.dualSubmoduleToDual N) x = (B.dualSubmoduleToDual N) y<GOAL>↑x = ↑y
<VAR>R : Type u_3<VAR>S : Type u_1<VAR>M : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Field S<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S M<VAR>inst✝¹ : IsScalarTower R S M<VAR>B : BilinForm S M<VAR>hB : B.Nondegenerate<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>N : Submodule R M<VAR>hN : Submodule.span S ↑N = ⊤<VAR>x y : ↥(B.dualSubmodule N)<VAR>e : (B.dualSubmoduleToDual N) x = (B.dualSubmoduleToDual N) y<GOAL>B ↑x = B ↑y
<VAR>R : Type u_3<VAR>S : Type u_1<VAR>M : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Field S<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S M<VAR>inst✝¹ : IsScalarTower R S M<VAR>B : BilinForm S M<VAR>hB : B.Nondegenerate<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>N : Submodule R M<VAR>hN : Submodule.span S ↑N = ⊤<VAR>x y : ↥(B.dualSubmodule N)<VAR>e : (B.dualSubmoduleToDual N) x = (B.dualSubmoduleToDual N) y<GOAL>Set.EqOn ⇑(B ↑x) ⇑(B ↑y) ↑N
<VAR>R : Type u_3<VAR>S : Type u_1<VAR>M : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Field S<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S M<VAR>inst✝¹ : IsScalarTower R S M<VAR>B : BilinForm S M<VAR>hB : B.Nondegenerate<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>N : Submodule R M<VAR>hN : Submodule.span S ↑N = ⊤<VAR>x y : ↥(B.dualSubmodule N)<VAR>e : (B.dualSubmoduleToDual N) x = (B.dualSubmoduleToDual N) y<VAR>z : M<VAR>hz : z ∈ ↑N<GOAL>(B ↑x) z = (B ↑y) z
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n m : ℕ<VAR>hpos : 0 < n<VAR>hm : m ∣ n<VAR>hdiff : m ≠ n<GOAL>X ^ m - 1 ∣ ∏ i ∈ n.properDivisors, cyclotomic i R
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n m : ℕ<VAR>hpos : 0 < n<VAR>hdiff : m ≠ n<VAR>hm : m ∈ n.properDivisors<GOAL>X ^ m - 1 ∣ ∏ i ∈ n.properDivisors, cyclotomic i R
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n m : ℕ<VAR>hpos : 0 < n<VAR>hdiff : m ≠ n<VAR>hm : m ∈ n.properDivisors<GOAL>X ^ m - 1 ∣ (∏ x ∈ n.properDivisors \ m.divisors, cyclotomic x R) * (X ^ m - 1)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : Zero α<VAR>s : Finset ι<VAR>f : (i : ι) → i ∈ s → α<VAR>i✝ : ι<VAR>a b : (i : ι) → i ∈ s → α<VAR>h : (fun f => indicator s f) a = (fun f => indicator s f) b<VAR>i : ι<VAR>hi : i ∈ s<GOAL>a i hi = b i hi
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : Zero α<VAR>s : Finset ι<VAR>f : (i : ι) → i ∈ s → α<VAR>i✝ : ι<VAR>a b : (i : ι) → i ∈ s → α<VAR>h : (fun f => indicator s f) a = (fun f => indicator s f) b<VAR>i : ι<VAR>hi : i ∈ s<GOAL>(indicator s a) i = (indicator s b) i
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>F_obj : C → D<VAR>e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)<VAR>he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), (e X Y') (h ≫ g) = (e X Y) h ≫ G.map g<VAR>X' X : C<VAR>Y : D<VAR>f : X' ⟶ X<VAR>g : X ⟶ G.obj Y<GOAL>(e X' Y).symm (f ≫ g) = (leftAdjointOfEquiv e he).map f ≫ (e X Y).symm g
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>F_obj : C → D<VAR>e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)<VAR>he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), (e X Y') (h ≫ g) = (e X Y) h ≫ G.map g<VAR>X' X : C<VAR>Y : D<VAR>f : X' ⟶ X<VAR>g : X ⟶ G.obj Y<VAR>this : ∀ {X : C} {Y Y' : D} (f : X ⟶ G.obj Y) (g : Y ⟶ Y'), (e X Y').symm (f ≫ G.map g) = (e X Y).symm f ≫ g<GOAL>(e X' Y).symm (f ≫ g) = (leftAdjointOfEquiv e he).map f ≫ (e X Y).symm g
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>F_obj : C → D<VAR>e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)<VAR>he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), (e X Y') (h ≫ g) = (e X Y) h ≫ G.map g<VAR>X' X : C<VAR>Y : D<VAR>f : X' ⟶ X<VAR>g : X ⟶ G.obj Y<VAR>this : ∀ {X : C} {Y Y' : D} (f : X ⟶ G.obj Y) (g : Y ⟶ Y'), (e X Y').symm (f ≫ G.map g) = (e X Y).symm f ≫ g<GOAL>(e X' Y) ((e X' Y).symm (f ≫ g)) = (e X' Y) ((e X' Y).symm ((f ≫ (e X (F_obj X)) (𝟙 (F_obj X))) ≫ G.map ((e X Y).symm g)))
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>F_obj : C → D<VAR>e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)<VAR>he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), (e X Y') (h ≫ g) = (e X Y) h ≫ G.map g<VAR>X' X : C<VAR>Y : D<VAR>f : X' ⟶ X<VAR>g : X ⟶ G.obj Y<VAR>this : ∀ {X : C} {Y Y' : D} (f : X ⟶ G.obj Y) (g : Y ⟶ Y'), (e X Y').symm (f ≫ G.map g) = (e X Y).symm f ≫ g<GOAL>f ≫ g = f ≫ (e X (F_obj X)) (𝟙 (F_obj X)) ≫ G.map ((e X Y).symm g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : CountableOrCountablyGenerated α β<VAR>ρ : Measure (β × Ω)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>f : β × Ω → ℝ≥0∞<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>t : Set Ω<VAR>ht : MeasurableSet t<GOAL>∫⁻ (b : β) in s, (ρ.condKernel b) t ∂ρ.fst = ρ (s ×ˢ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : CountableOrCountablyGenerated α β<VAR>ρ : Measure (β × Ω)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>f : β × Ω → ℝ≥0∞<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>t : Set Ω<VAR>ht : MeasurableSet t<VAR>this : ρ (s ×ˢ t) = (ρ.fst ⊗ₘ ρ.condKernel) (s ×ˢ t)<GOAL>∫⁻ (b : β) in s, (ρ.condKernel b) t ∂ρ.fst = ρ (s ×ˢ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : CountableOrCountablyGenerated α β<VAR>ρ : Measure (β × Ω)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>f : β × Ω → ℝ≥0∞<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>t : Set Ω<VAR>ht : MeasurableSet t<VAR>this : ρ (s ×ˢ t) = (ρ.fst ⊗ₘ ρ.condKernel) (s ×ˢ t)<GOAL>∫⁻ (b : β) in s, (ρ.condKernel b) t ∂ρ.fst = ∫⁻ (a : β), (ρ.condKernel a) (Prod.mk a ⁻¹' s ×ˢ t) ∂ρ.fst
<VAR>α : Type u<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : LT α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c d : α<GOAL>a * b⁻¹ < c ↔ a < b * c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>p : α × α → Prop<VAR>h : ∀ᶠ (i : α × α) in f ×ˢ f, p i<GOAL>∀ᶠ (i : α) in f, p (i, i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s✝ : Set α<VAR>t✝ : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>p : α × α → Prop<VAR>h : ∀ᶠ (i : α × α) in f ×ˢ f, p i<VAR>t : α → Prop<VAR>ht : ∀ᶠ (x : α) in f, t x<VAR>s : α → Prop<VAR>hs : ∀ᶠ (y : α) in f, s y<VAR>hst : ∀ {x : α}, t x → ∀ {y : α}, s y → p (x, y)<GOAL>∀ᶠ (i : α) in f, p (i, i)
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>inst✝³ : LinearOrder α✝<VAR>inst✝² : LocallyFiniteOrder α✝<VAR>a✝¹ b✝ : α✝<VAR>α : Type u_3<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LocallyFiniteOrderBot α<VAR>a b a✝ : α<GOAL>a✝ ∈ filter (fun x => x < b) (Iio a) ↔ a✝ ∈ Iio (min a b)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>α : Type u_5<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedRing 𝕜'<VAR>inst✝¹ : NormedAlgebra 𝕜 𝕜'<VAR>inst✝ : NormOneClass 𝕜'<VAR>x : 𝕜<GOAL>‖(algebraMap 𝕜 𝕜') x‖ = ‖x‖
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E B I X R J : Set α<GOAL>¬M.RkPos ↔ M = loopyOn M.E
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>N : ℕ<VAR>toFinsupp✝ : AddMonoidAlgebra R ℕ<VAR>a✝ : ℕ<GOAL>a✝ ∈ (reflect N { toFinsupp := toFinsupp✝ }).support ↔ a✝ ∈ image ⇑(revAt N) { toFinsupp := toFinsupp✝ }.support
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝ : CompleteLattice α<VAR>f : ι → α<VAR>h : WellFounded fun x x_1 => x > x_1<VAR>s : Set α<VAR>hs : SetIndependent s<GOAL>s.Finite
<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>a : G<VAR>b : α<VAR>n : ℕ<GOAL>a ^ n • b = b ↔ minimalPeriod (fun x => a • x) b ∣ n
<VAR>N k : ℕ<GOAL>(N.smoothNumbersUpTo k).card ≤ 2 ^ k.primesBelow.card * N.sqrt
<VAR>N k : ℕ<GOAL>2 ^ k.primesBelow.card * N.sqrt = (k.primesBelow.powerset ×ˢ (Finset.range N.sqrt.succ).erase 0).card
<VAR>R✝ : Type u<VAR>A✝ : Type v<VAR>B : Type w<VAR>inst✝⁷ : CommSemiring R✝<VAR>inst✝⁶ : Semiring A✝<VAR>inst✝⁵ : Algebra R✝ A✝<VAR>inst✝⁴ : Semiring B<VAR>inst✝³ : Algebra R✝ B<VAR>S✝ : Subalgebra R✝ A✝<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>S : Subalgebra R A<GOAL>(algebraMap (↥S) A).rangeS = S.toSubsemiring
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>z1 z2 : ℤ_[p]<VAR>h : ‖z1 + z2‖ < ‖z2‖<VAR>hne : ¬‖z1‖ = ‖z2‖<GOAL>‖z1 + z2‖ ≥ ‖z2‖
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>z1 z2 : ℤ_[p]<VAR>h : ‖z1 + z2‖ < ‖z2‖<VAR>hne : ¬‖z1‖ = ‖z2‖<GOAL>max ‖z1‖ ‖z2‖ ≥ ‖z2‖
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : Add α<VAR>a✝ b✝ c d : WithTop α<VAR>x y : α<VAR>inst✝ : LT α<VAR>a b : WithTop α<GOAL>a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤
<VAR>Γ : Type u_1<VAR>inst✝⁵ : PartialOrder Γ<VAR>R : Type u_2<VAR>V : Type u_3<VAR>W : Type u_4<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module R V<VAR>inst✝¹ : AddCommGroup W<VAR>inst✝ : Module R W<VAR>a₁✝ a₂✝ : HVertexOperator Γ R V W<VAR>h : a₁✝.coeff = a₂✝.coeff<VAR>v : V<VAR>n : Γ<GOAL>((of R).symm (a₁✝ v)).coeff n = ((of R).symm (a₂✝ v)).coeff n
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝² : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝¹ : Ring R<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x y z : R<VAR>h : v y < v x<GOAL>v (x - y) = v x
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝² : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝¹ : Ring R<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x y z : R<VAR>h : v y < v x<GOAL>v (-y) < v x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>E : Type u_3<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g✝ : α → E<VAR>f : α → ℝ≥0<VAR>g : α → E<VAR>hf : AEMeasurable f μ<VAR>hfg : Integrable (f • g) μ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>↑(μ.withDensityᵥ (f • g)) s = ↑((μ.withDensity fun x => ↑(f x)).withDensityᵥ g) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>E : Type u_3<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g✝ : α → E<VAR>f : α → ℝ≥0<VAR>g : α → E<VAR>hf : AEMeasurable f μ<VAR>hfg : Integrable (f • g) μ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∫ (x : α) in s, (f • g) x ∂μ = ∫ (x : α) in s, f x • g x ∂μ
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x✝ y✝ : α<VAR>Φ : α → β<VAR>bs : Bornology.IsBounded s<VAR>bt : Bornology.IsBounded t<VAR>x : α<VAR>xs : x ∈ s<VAR>y : α<VAR>yt : y ∈ t<GOAL>hausdorffDist s t ≤ diam (s ∪ t)
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x✝ y✝ : α<VAR>Φ : α → β<VAR>bs : Bornology.IsBounded s<VAR>bt : Bornology.IsBounded t<VAR>x : α<VAR>xs : x ∈ s<VAR>y : α<VAR>yt : y ∈ t<GOAL>∀ x ∈ s, ∃ y ∈ t, dist x y ≤ diam (s ∪ t)
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x✝ y✝ : α<VAR>Φ : α → β<VAR>bs : Bornology.IsBounded s<VAR>bt : Bornology.IsBounded t<VAR>x : α<VAR>xs : x ∈ s<VAR>y : α<VAR>yt : y ∈ t<GOAL>∀ x ∈ t, ∃ y ∈ s, dist x y ≤ diam (s ∪ t)
<VAR>R : Type u<VAR>n : Type w<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>J A B : Matrix n n R<VAR>hA : A ∈ skewAdjointMatricesSubmodule J<VAR>hB : B ∈ skewAdjointMatricesSubmodule J<GOAL>⁅A, B⁆ ∈ skewAdjointMatricesSubmodule J
<VAR>R : Type u<VAR>n : Type w<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>J A B : Matrix n n R<VAR>hA : J.IsSkewAdjoint A<VAR>hB : J.IsSkewAdjoint B<GOAL>J.IsSkewAdjoint ⁅A, B⁆