ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>q : α → Prop<VAR>inst✝ : DecidablePred q<VAR>s : Multiset α<GOAL>filter p (filter q s) = filter q (filter p s)
<VAR>b n : ℕ<VAR>h : 1 < b<VAR>hn : b ≤ n<GOAL>(if h : b ≤ n ∧ 1 < b then log b (n / b) + 1 else 0) = log b (n / b) + 1
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>h e f : L<VAR>m : M<VAR>μ : R<VAR>t : IsSl2Triple h e f<VAR>P : t.HasPrimitiveVectorWith m μ<VAR>inst✝³ : IsNoetherian R M<VAR>inst✝² : NoZeroSMulDivisors R M<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : CharZero R<GOAL>∃ n, μ = ↑n
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>h e f : L<VAR>m : M<VAR>μ : R<VAR>t : IsSl2Triple h e f<VAR>P : t.HasPrimitiveVectorWith m μ<VAR>inst✝³ : IsNoetherian R M<VAR>inst✝² : NoZeroSMulDivisors R M<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : CharZero R<GOAL>∃ n, ((toEnd R L M) f ^ n) m = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>h e f : L<VAR>m : M<VAR>μ : R<VAR>t : IsSl2Triple h e f<VAR>P : t.HasPrimitiveVectorWith m μ<VAR>inst✝³ : IsNoetherian R M<VAR>inst✝² : NoZeroSMulDivisors R M<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : CharZero R<VAR>hs : (range fun n => μ - 2 * ↑n).Infinite<GOAL>∃ n, ((toEnd R L M) f ^ n) m = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>h e f : L<VAR>m : M<VAR>μ : R<VAR>t : IsSl2Triple h e f<VAR>P : t.HasPrimitiveVectorWith m μ<VAR>inst✝³ : IsNoetherian R M<VAR>inst✝² : NoZeroSMulDivisors R M<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : CharZero R<VAR>hs : (range fun n => μ - 2 * ↑n).Infinite<VAR>contra : ∀ (n : ℕ), ((toEnd R L M) f ^ n) m ≠ 0<GOAL>False
<VAR>q : ℚ<VAR>x y : ℝ<VAR>h : Irrational x<VAR>m : ℤ<VAR>hm : m ≠ 0<GOAL>Irrational (x * ↑m)
<VAR>q : ℚ<VAR>x y : ℝ<VAR>h : Irrational x<VAR>m : ℤ<VAR>hm : m ≠ 0<GOAL>Irrational (x * ↑↑m)
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : LinearOrder α<VAR>s : Set α<VAR>a : α<VAR>f : ι → α<GOAL>⋃ i, Iio (f i) = univ ↔ ¬BddAbove (range f)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁶ : AddCommMonoid ι<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝¹ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>𝔭 : Ideal A<VAR>inst✝ : 𝔭.IsPrime<VAR>f : AtPrime 𝒜 𝔭<GOAL>IsUnit (val f) ↔ IsUnit f
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁶ : AddCommMonoid ι<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝¹ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>𝔭 : Ideal A<VAR>inst✝ : 𝔭.IsPrime<VAR>f : AtPrime 𝒜 𝔭<VAR>h1 : IsUnit (val f)<GOAL>IsUnit f
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁶ : AddCommMonoid ι<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝¹ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>𝔭 : Ideal A<VAR>inst✝ : 𝔭.IsPrime<VAR>f : AtPrime 𝒜 𝔭<VAR>b : at 𝔭.primeCompl<VAR>eq0 : val f * b = 1<VAR>eq1 : b * val f = 1<GOAL>IsUnit f
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁶ : AddCommMonoid ι<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝¹ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>𝔭 : Ideal A<VAR>inst✝ : 𝔭.IsPrime<VAR>b : at 𝔭.primeCompl<VAR>f : NumDenSameDeg 𝒜 𝔭.primeCompl<VAR>eq0 : (mk f).val * b = 1<VAR>eq1 : b * (mk f).val = 1<GOAL>IsUnit (mk f)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁶ : AddCommMonoid ι<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝¹ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>𝔭 : Ideal A<VAR>inst✝ : 𝔭.IsPrime<VAR>f : NumDenSameDeg 𝒜 𝔭.primeCompl<VAR>b : A<VAR>s : ↥𝔭.primeCompl<VAR>eq0 : (mk f).val * IsLocalization.mk' (at 𝔭.primeCompl) b s = 1<VAR>eq1 : IsLocalization.mk' (at 𝔭.primeCompl) b s * (mk f).val = 1<GOAL>IsUnit (mk f)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁶ : AddCommMonoid ι<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝¹ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>𝔭 : Ideal A<VAR>inst✝ : 𝔭.IsPrime<VAR>f : NumDenSameDeg 𝒜 𝔭.primeCompl<VAR>b : A<VAR>s : ↥𝔭.primeCompl<VAR>eq0 : ∃ c, ↑c * (↑f.num * b) = ↑c * ↑(⟨↑f.den, ⋯⟩ * s)<VAR>eq1 : IsLocalization.mk' (at 𝔭.primeCompl) b s * (mk f).val = 1<GOAL>IsUnit (mk f)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁶ : AddCommMonoid ι<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝¹ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>𝔭 : Ideal A<VAR>inst✝ : 𝔭.IsPrime<VAR>f : NumDenSameDeg 𝒜 𝔭.primeCompl<VAR>b : A<VAR>s : ↥𝔭.primeCompl<VAR>eq1 : IsLocalization.mk' (at 𝔭.primeCompl) b s * (mk f).val = 1<VAR>c : ↥𝔭.primeCompl<VAR>hc : ↑c * (↑f.num * b) = ↑c * (↑f.den * ↑s)<GOAL>IsUnit (mk f)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁶ : AddCommMonoid ι<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝¹ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>𝔭 : Ideal A<VAR>inst✝ : 𝔭.IsPrime<VAR>f : NumDenSameDeg 𝒜 𝔭.primeCompl<VAR>b : A<VAR>s : ↥𝔭.primeCompl<VAR>eq1 : IsLocalization.mk' (at 𝔭.primeCompl) b s * (mk f).val = 1<VAR>c : ↥𝔭.primeCompl<VAR>hc : ↑c * (↑f.num * b) = ↑c * (↑f.den * ↑s)<VAR>this : ↑f.num ∉ 𝔭<GOAL>IsUnit (mk f)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁶ : AddCommMonoid ι<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝¹ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>𝔭 : Ideal A<VAR>inst✝ : 𝔭.IsPrime<VAR>f : NumDenSameDeg 𝒜 𝔭.primeCompl<VAR>b : A<VAR>s : ↥𝔭.primeCompl<VAR>eq1 : IsLocalization.mk' (at 𝔭.primeCompl) b s * (mk f).val = 1<VAR>c : ↥𝔭.primeCompl<VAR>hc : ↑c * (↑f.num * b) = ↑c * (↑f.den * ↑s)<VAR>this : ↑f.num ∉ 𝔭<GOAL>mk f * Quotient.mk'' { deg := f.deg, num := f.den, den := f.num, den_mem := this } = 1
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁶ : AddCommMonoid ι<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝¹ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>𝔭 : Ideal A<VAR>inst✝ : 𝔭.IsPrime<VAR>f : NumDenSameDeg 𝒜 𝔭.primeCompl<VAR>b : A<VAR>s : ↥𝔭.primeCompl<VAR>eq1 : IsLocalization.mk' (at 𝔭.primeCompl) b s * (mk f).val = 1<VAR>c : ↥𝔭.primeCompl<VAR>hc : ↑c * (↑f.num * b) = ↑c * (↑f.den * ↑s)<VAR>this : ↑f.num ∉ 𝔭<GOAL>Localization.mk ↑(f * { deg := f.deg, num := f.den, den := f.num, den_mem := this }).num ⟨↑(f * { deg := f.deg, num := f.den, den := f.num, den_mem := this }).den, ⋯⟩ = val 1
<VAR>X Y Z : SemiNormedGrp<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>w : f ≫ g = 0<VAR>e : explicitCokernel f ⟶ Z<VAR>he : explicitCokernelπ f ≫ e = g<GOAL>e = explicitCokernelDesc w
<VAR>X Y Z : SemiNormedGrp<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>w : f ≫ g = 0<VAR>e : explicitCokernel f ⟶ Z<VAR>he : explicitCokernelπ f ≫ e = g<GOAL>∀ (j : WalkingParallelPair), (cokernelCocone f).ι.app j ≫ e = (Cofork.ofπ g ⋯).ι.app j
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n : ℕ<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>f : ofMulAction k G (Fin (n + 1) → G) ⟶ A<VAR>x : Fin n → G<GOAL>f.hom ((diagonalSucc k G n).inv.hom (Finsupp.single 1 1 ⊗ₜ[k] Finsupp.single x 1)) = f.hom (Finsupp.single (Fin.partialProd x) 1)
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>μ : Measure E<VAR>F : Type u_3<VAR>inst✝⁴ : MeasurableSpace F<VAR>ν : Measure F<VAR>X : Ω → E<VAR>Y : Ω → F<VAR>inst✝³ : IsFiniteMeasure ℙ<VAR>inst✝² : SigmaFinite μ<VAR>inst✝¹ : SigmaFinite ν<VAR>inst✝ : HasPDF (fun ω => (X ω, Y ω)) ℙ (μ.prod ν)<GOAL>IndepFun X Y ℙ ↔ pdf (fun ω => (X ω, Y ω)) ℙ (μ.prod ν) =ᶠ[ae (μ.prod ν)] fun z => pdf X ℙ μ z.1 * pdf Y ℙ ν z.2
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>μ : Measure E<VAR>F : Type u_3<VAR>inst✝⁴ : MeasurableSpace F<VAR>ν : Measure F<VAR>X : Ω → E<VAR>Y : Ω → F<VAR>inst✝³ : IsFiniteMeasure ℙ<VAR>inst✝² : SigmaFinite μ<VAR>inst✝¹ : SigmaFinite ν<VAR>inst✝ : HasPDF (fun ω => (X ω, Y ω)) ℙ (μ.prod ν)<VAR>this : HasPDF X ℙ μ<GOAL>IndepFun X Y ℙ ↔ pdf (fun ω => (X ω, Y ω)) ℙ (μ.prod ν) =ᶠ[ae (μ.prod ν)] fun z => pdf X ℙ μ z.1 * pdf Y ℙ ν z.2
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>μ : Measure E<VAR>F : Type u_3<VAR>inst✝⁴ : MeasurableSpace F<VAR>ν : Measure F<VAR>X : Ω → E<VAR>Y : Ω → F<VAR>inst✝³ : IsFiniteMeasure ℙ<VAR>inst✝² : SigmaFinite μ<VAR>inst✝¹ : SigmaFinite ν<VAR>inst✝ : HasPDF (fun ω => (X ω, Y ω)) ℙ (μ.prod ν)<VAR>this✝ : HasPDF X ℙ μ<VAR>this : HasPDF Y ℙ ν<GOAL>IndepFun X Y ℙ ↔ pdf (fun ω => (X ω, Y ω)) ℙ (μ.prod ν) =ᶠ[ae (μ.prod ν)] fun z => pdf X ℙ μ z.1 * pdf Y ℙ ν z.2
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>μ : Measure E<VAR>F : Type u_3<VAR>inst✝⁴ : MeasurableSpace F<VAR>ν : Measure F<VAR>X : Ω → E<VAR>Y : Ω → F<VAR>inst✝³ : IsFiniteMeasure ℙ<VAR>inst✝² : SigmaFinite μ<VAR>inst✝¹ : SigmaFinite ν<VAR>inst✝ : HasPDF (fun ω => (X ω, Y ω)) ℙ (μ.prod ν)<VAR>this✝ : HasPDF X ℙ μ<VAR>this : HasPDF Y ℙ ν<VAR>h₀ : (map X ℙ).prod (map Y ℙ) = (μ.prod ν).withDensity fun z => pdf X ℙ μ z.1 * pdf Y ℙ ν z.2<GOAL>IndepFun X Y ℙ ↔ pdf (fun ω => (X ω, Y ω)) ℙ (μ.prod ν) =ᶠ[ae (μ.prod ν)] fun z => pdf X ℙ μ z.1 * pdf Y ℙ ν z.2
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>μ : Measure E<VAR>F : Type u_3<VAR>inst✝⁴ : MeasurableSpace F<VAR>ν : Measure F<VAR>X : Ω → E<VAR>Y : Ω → F<VAR>inst✝³ : IsFiniteMeasure ℙ<VAR>inst✝² : SigmaFinite μ<VAR>inst✝¹ : SigmaFinite ν<VAR>inst✝ : HasPDF (fun ω => (X ω, Y ω)) ℙ (μ.prod ν)<VAR>this✝ : HasPDF X ℙ μ<VAR>this : HasPDF Y ℙ ν<VAR>h₀ : (map X ℙ).prod (map Y ℙ) = (μ.prod ν).withDensity fun z => pdf X ℙ μ z.1 * pdf Y ℙ ν z.2<GOAL>AEMeasurable (fun z => pdf X ℙ μ z.1 * pdf Y ℙ ν z.2) (μ.prod ν)
<VAR>ss : List String<GOAL>(join ss).data = (List.map data ss).join
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ g f : Perm α<VAR>h : f ≠ 1<GOAL>1 < f.support.card
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ g f : Perm α<VAR>h : f ≠ 1<GOAL>∃ a b, ¬(f a = a ∨ f b = b ∨ a = b)
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ g f : Perm α<VAR>h : ∀ (a b : α), f a = a ∨ f b = b ∨ a = b<GOAL>f = 1
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ g f : Perm α<VAR>a : α<VAR>h : f (f a) = f a ∨ f a = a ∨ f a = a<GOAL>f a = 1 a
<VAR>B : Type u₁<VAR>inst✝² : Bicategory B<VAR>C : Type u₂<VAR>inst✝¹ : Bicategory C<VAR>D : Type u₃<VAR>inst✝ : Bicategory D<VAR>F✝ F : Pseudofunctor B C<VAR>a b : B<VAR>f : a ⟶ b<GOAL>(F.mapComp f (𝟙 b)).inv = F.map f ◁ (F.mapId b).hom ≫ (ρ_ (F.map f)).hom ≫ F.map₂ (ρ_ f).inv
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>A : Matrix α β ℤ<VAR>v : β → ℤ<VAR>hn : m < n<VAR>hm : 0 < m<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<GOAL>↑S.card < ↑T.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>A : Matrix α β ℤ<VAR>v : β → ℤ<VAR>hn : m < n<VAR>hm : 0 < m<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<GOAL>∏ i : α, (P i - N i + 1) < ↑((B + 1) ^ 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>h : j ≠ i<GOAL>(stdBasisMatrix i j c).trace = 0
<VAR>R : Type u_1<VAR>inst✝⁴ : StrictOrderedCommRing R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>x y : M<GOAL>SameRay R (-x) (-y) ↔ SameRay R x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>ι : Sort u_4<VAR>f : ι → ℝ≥0∞<VAR>a : ℝ≥0∞<GOAL>iSup f * a = ⨆ i, f i * a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>ι : Sort u_4<VAR>f : ι → ℝ≥0∞<VAR>a : ℝ≥0∞<GOAL>⨆ i, a * f i = ⨆ i, f i * a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>ι : Sort u_4<VAR>f : ι → ℝ≥0∞<VAR>a : ℝ≥0∞<GOAL>(fun i => a * f i) = fun i => f i * a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>ι : Sort u_4<VAR>f : ι → ℝ≥0∞<VAR>a : ℝ≥0∞<VAR>x✝ : ι<GOAL>a * f x✝ = f x✝ * a
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>n : ℕ<VAR>v : Fin n → R<GOAL>(vandermonde v).det ≠ 0 ↔ ∀ ⦃a₁ a₂ : Fin n⦄, v a₁ = v a₂ → a₁ = a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Fintype α<VAR>s : Finset α<VAR>hs : s.card = Fintype.card α<GOAL>univ.card ≤ s.card
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → 𝕜<VAR>x : 𝕜<VAR>h : MeromorphicAt f⁻¹ x<GOAL>MeromorphicAt f x
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>inst✝¹ : Inhabited Γ<VAR>inst✝ : Inhabited Γ'<VAR>F : PointedMap Γ Γ'<VAR>f : Γ → Γ<VAR>f' : Γ' → Γ'<VAR>H : ∀ (x : Γ), F.f (f x) = f' (F.f x)<VAR>n : ℕ<VAR>L : ListBlank Γ<GOAL>map F (modifyNth f n L) = modifyNth f' n (map F L)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k₁ k₂ : ℕ<VAR>hk : k₁ ≤ k₂<GOAL>(TruncatedWittVector.truncate hk).comp ((zmodEquivTrunc p k₂).toRingHom.comp (PadicInt.toZModPow k₂)) = (zmodEquivTrunc p k₁).toRingHom.comp (PadicInt.toZModPow k₁)
<VAR>f : ℕ → ℂ<VAR>n : ℕ<GOAL>(f * δ) n = (f 1 • δ) n
<VAR>f : ℕ → ℂ<VAR>n : ℕ<GOAL>(if n = 1 then f n else 0) = if n = 1 then f 1 else 0
<VAR>α : Type u_1<VAR>M : α → Type u_2<VAR>u : Ultrafilter α<VAR>L : Language<VAR>inst✝ : (a : α) → L.Structure (M a)<VAR>β : Type u_3<VAR>x : β → (a : α) → M a<VAR>t : L.Term β<GOAL>Term.realize (fun i => Quotient.mk' (x i)) t = Quotient.mk' fun a => Term.realize (fun i => x i a) t
<VAR>α : Type u_1<VAR>M : α → Type u_2<VAR>u : Ultrafilter α<VAR>L : Language<VAR>inst✝ : (a : α) → L.Structure (M a)<VAR>β : Type u_3<VAR>x : β → (a : α) → M a<VAR>t : L.Term β<GOAL>(fun a => Term.realize (fun i => x i a) t) = Term.realize x t
<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℂ F<VAR>f : E → F<VAR>s : Set E<VAR>hd : DifferentiableOn ℂ f s<GOAL>IsOpen {z | s ∈ 𝓝 z ∧ IsMaxOn (norm ∘ f) s z}
<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℂ F<VAR>f : E → F<VAR>s : Set E<VAR>hd : DifferentiableOn ℂ f s<VAR>z : E<VAR>hz : z ∈ {z | s ∈ 𝓝 z ∧ IsMaxOn (norm ∘ f) s z}<GOAL>Filter.Eventually (IsMaxOn (norm ∘ f) s) (𝓝 z)
<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℂ F<VAR>f : E → F<VAR>s : Set E<VAR>z : E<VAR>hz : z ∈ {z | s ∈ 𝓝 z ∧ IsMaxOn (norm ∘ f) s z}<VAR>hd : ∀ᶠ (w : E) in 𝓝 z, DifferentiableAt ℂ f w<GOAL>Filter.Eventually (IsMaxOn (norm ∘ f) s) (𝓝 z)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x y z : V<VAR>p : P<GOAL>z +ᵥ p ∈ affineSegment R (x +ᵥ p) (y +ᵥ p) ↔ z ∈ affineSegment R x y
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>I : Ideal R<VAR>H : I.IsPrime<VAR>hk : RingHom.ker f ≤ I<GOAL>(map f I).IsPrime
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>I : Ideal R<VAR>H : I.IsPrime<VAR>hk : RingHom.ker f ≤ I<VAR>h : map f I = ⊤<GOAL>⊤ ≤ I
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>I : Ideal R<VAR>H : I.IsPrime<VAR>hk : RingHom.ker f ≤ I<VAR>x y : S<GOAL>x * y ∈ map f I → x ∈ map f I ∨ y ∈ map f I
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : α → β<VAR>g : β → γ<VAR>hf : UniformContinuous f<VAR>hg : UniformContinuous g<GOAL>mk ∘ g ∘ f = (map g ∘ map f) ∘ mk
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Category.{?u.132496, u_2} D<VAR>inst✝³ : Preadditive C<VAR>inst✝² : Preadditive D<VAR>S : ShortComplex C<VAR>inst✝¹ : Balanced C<VAR>hS : S.Exact<VAR>h : S.RightHomologyData<VAR>inst✝ : Epi S.g<GOAL>IsIso h.g'
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Category.{?u.132496, u_2} D<VAR>inst✝³ : Preadditive C<VAR>inst✝² : Preadditive D<VAR>S : ShortComplex C<VAR>inst✝¹ : Balanced C<VAR>hS : S.Exact<VAR>h : S.RightHomologyData<VAR>inst✝ : Epi S.g<VAR>this : Mono h.g'<GOAL>IsIso h.g'
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Category.{?u.132496, u_2} D<VAR>inst✝³ : Preadditive C<VAR>inst✝² : Preadditive D<VAR>S : ShortComplex C<VAR>inst✝¹ : Balanced C<VAR>hS : S.Exact<VAR>h : S.RightHomologyData<VAR>inst✝ : Epi S.g<VAR>this✝ : Mono h.g'<VAR>this : Epi h.g'<GOAL>IsIso h.g'
<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✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : SeminormedAddCommGroup V<VAR>inst✝⁶ : SeminormedAddCommGroup W<VAR>inst✝⁵ : NormedSpace 𝕜 V<VAR>inst✝⁴ : NormedSpace 𝕜 W<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : PseudoMetricSpace Q<VAR>inst✝¹ : NormedAddTorsor V P<VAR>inst✝ : NormedAddTorsor W Q<VAR>φ : P →ᵃⁱ[𝕜] Q<VAR>s : Set P<GOAL>intrinsicClosure 𝕜 (⇑φ '' s) = ⇑φ '' intrinsicClosure 𝕜 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✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : SeminormedAddCommGroup V<VAR>inst✝⁶ : SeminormedAddCommGroup W<VAR>inst✝⁵ : NormedSpace 𝕜 V<VAR>inst✝⁴ : NormedSpace 𝕜 W<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : PseudoMetricSpace Q<VAR>inst✝¹ : NormedAddTorsor V P<VAR>inst✝ : NormedAddTorsor W Q<VAR>φ : P →ᵃⁱ[𝕜] Q<GOAL>intrinsicClosure 𝕜 (⇑φ '' ∅) = ⇑φ '' intrinsicClosure 𝕜 ∅
<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✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : SeminormedAddCommGroup V<VAR>inst✝⁶ : SeminormedAddCommGroup W<VAR>inst✝⁵ : NormedSpace 𝕜 V<VAR>inst✝⁴ : NormedSpace 𝕜 W<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : PseudoMetricSpace Q<VAR>inst✝¹ : NormedAddTorsor V P<VAR>inst✝ : NormedAddTorsor W Q<VAR>φ : P →ᵃⁱ[𝕜] Q<VAR>s : Set P<VAR>hs : s.Nonempty<GOAL>intrinsicClosure 𝕜 (⇑φ '' s) = ⇑φ '' intrinsicClosure 𝕜 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✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : SeminormedAddCommGroup V<VAR>inst✝⁶ : SeminormedAddCommGroup W<VAR>inst✝⁵ : NormedSpace 𝕜 V<VAR>inst✝⁴ : NormedSpace 𝕜 W<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : PseudoMetricSpace Q<VAR>inst✝¹ : NormedAddTorsor V P<VAR>inst✝ : NormedAddTorsor W Q<VAR>φ : P →ᵃⁱ[𝕜] Q<VAR>s : Set P<VAR>hs : s.Nonempty<VAR>this : Nonempty ↑s<GOAL>intrinsicClosure 𝕜 (⇑φ '' s) = ⇑φ '' intrinsicClosure 𝕜 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✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : SeminormedAddCommGroup V<VAR>inst✝⁶ : SeminormedAddCommGroup W<VAR>inst✝⁵ : NormedSpace 𝕜 V<VAR>inst✝⁴ : NormedSpace 𝕜 W<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : PseudoMetricSpace Q<VAR>inst✝¹ : NormedAddTorsor V P<VAR>inst✝ : NormedAddTorsor W Q<VAR>φ : P →ᵃⁱ[𝕜] Q<VAR>s : Set P<VAR>hs : s.Nonempty<VAR>this : Nonempty ↑s<VAR>f : ↥(affineSpan 𝕜 s) ≃ₜ ↥(map φ.toAffineMap (affineSpan 𝕜 s)) := (isometryEquivMap φ (affineSpan 𝕜 s)).toHomeomorph<GOAL>intrinsicClosure 𝕜 (⇑φ '' s) = ⇑φ '' intrinsicClosure 𝕜 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✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : SeminormedAddCommGroup V<VAR>inst✝⁶ : SeminormedAddCommGroup W<VAR>inst✝⁵ : NormedSpace 𝕜 V<VAR>inst✝⁴ : NormedSpace 𝕜 W<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : PseudoMetricSpace Q<VAR>inst✝¹ : NormedAddTorsor V P<VAR>inst✝ : NormedAddTorsor W Q<VAR>φ : P →ᵃⁱ[𝕜] Q<VAR>s : Set P<VAR>hs : s.Nonempty<VAR>this✝ : Nonempty ↑s<VAR>f : ↥(affineSpan 𝕜 s) ≃ₜ ↥(map φ.toAffineMap (affineSpan 𝕜 s)) := (isometryEquivMap φ (affineSpan 𝕜 s)).toHomeomorph<VAR>this : ⇑φ.toAffineMap ∘ Subtype.val ∘ ⇑f.symm = Subtype.val<GOAL>intrinsicClosure 𝕜 (⇑φ '' s) = ⇑φ '' intrinsicClosure 𝕜 s
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : StrictOrderedCommRing R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x z : P<VAR>t : R<VAR>ht0 : 0 ≤ t<VAR>ht1 : t ≤ 1<GOAL>SameRay R ((lineMap x z) t -ᵥ x) (z -ᵥ (lineMap x z) t)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : StrictOrderedCommRing R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x z : P<VAR>t : R<VAR>ht0 : 0 ≤ t<VAR>ht1 : t ≤ 1<GOAL>SameRay R (t • (z -ᵥ x) +ᵥ x -ᵥ x) (z -ᵥ (t • (z -ᵥ x) +ᵥ x))
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : StrictOrderedCommRing R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x z : P<VAR>t : R<VAR>ht0 : 0 ≤ t<VAR>ht1 : t ≤ 1<VAR>ht0' : 0 < t<VAR>ht1' : t < 1<GOAL>SameRay R (t • (z -ᵥ x) +ᵥ x -ᵥ x) (z -ᵥ (t • (z -ᵥ x) +ᵥ x))
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : StrictOrderedCommRing R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x z : P<VAR>t : R<VAR>ht0 : 0 ≤ t<VAR>ht1 : t ≤ 1<VAR>ht0' : 0 < t<VAR>ht1' : t < 1<GOAL>(1 - t) • (t • (z -ᵥ x) +ᵥ x -ᵥ x) = t • (z -ᵥ (t • (z -ᵥ x) +ᵥ x))
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : StrictOrderedCommRing R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x z : P<VAR>t : R<VAR>ht0 : 0 ≤ t<VAR>ht1 : t ≤ 1<VAR>ht0' : 0 < t<VAR>ht1' : t < 1<GOAL>((1 - t) * t) • (z -ᵥ x) = (t - t * t) • (z -ᵥ x)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>f : α ≃. β<VAR>a : α<VAR>h : (f a).isSome = true<GOAL>f.symm ((f a).get h) = some a
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>i j k : ι<VAR>hi : c.prev j = i<VAR>hk : c.next j = k<VAR>inst✝¹ : K.HasHomology j<VAR>inst✝ : (K.sc' i j k).HasHomology<GOAL>(K.sc' i j k).pOpcycles ≫ ShortComplex.opcyclesMap ((natIsoSc' C c i j k hi hk).inv.app K) = K.pOpcycles j