ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁶ : EuclideanDomain R<VAR>inst✝¹⁵ : CommRing S<VAR>inst✝¹⁴ : IsDomain S<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra R K<VAR>inst✝¹⁰ : IsFractionRing R K<VAR>inst✝⁹ : Algebra K L<VAR>inst✝⁸ : FiniteDimensional K L<VAR>inst✝⁷ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁶ : IsScalarTower R K L<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>inst✝¹ : Infinite R<VAR>inst✝ : DecidableEq R<GOAL>¬∏ m ∈ finsetApprox bS adm, m = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁶ : EuclideanDomain R<VAR>inst✝¹⁵ : CommRing S<VAR>inst✝¹⁴ : IsDomain S<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra R K<VAR>inst✝¹⁰ : IsFractionRing R K<VAR>inst✝⁹ : Algebra K L<VAR>inst✝⁸ : FiniteDimensional K L<VAR>inst✝⁷ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁶ : IsScalarTower R K L<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>inst✝¹ : Infinite R<VAR>inst✝ : DecidableEq R<GOAL>∀ (x : R), ¬(x ∈ finsetApprox bS adm ∧ x = 0)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁶ : EuclideanDomain R<VAR>inst✝¹⁵ : CommRing S<VAR>inst✝¹⁴ : IsDomain S<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra R K<VAR>inst✝¹⁰ : IsFractionRing R K<VAR>inst✝⁹ : Algebra K L<VAR>inst✝⁸ : FiniteDimensional K L<VAR>inst✝⁷ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁶ : IsScalarTower R K L<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>inst✝¹ : Infinite R<VAR>inst✝ : DecidableEq R<VAR>hx : 0 ∈ finsetApprox bS adm<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>M₀ : Type u_6<VAR>G : Type u_7<VAR>R : Type u_8<VAR>inst✝² : AddMonoid M<VAR>inst✝¹ : AddMonoid N<VAR>inst✝ : LinearOrder N<VAR>f : M → N<VAR>h0 : f 0 ≤ 0<VAR>hadd : ∀ (x y : M), f (x + y) ≤ max (f x) (f y)<VAR>hd : M<VAR>tl : List M<VAR>IH : f tl.sum ≤ foldr max 0 (map f tl)<GOAL>f (hd :: tl).sum ≤ foldr max 0 (map f (hd :: tl))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>M₀ : Type u_6<VAR>G : Type u_7<VAR>R : Type u_8<VAR>inst✝² : AddMonoid M<VAR>inst✝¹ : AddMonoid N<VAR>inst✝ : LinearOrder N<VAR>f : M → N<VAR>h0 : f 0 ≤ 0<VAR>hadd : ∀ (x y : M), f (x + y) ≤ max (f x) (f y)<VAR>hd : M<VAR>tl : List M<VAR>IH : f tl.sum ≤ foldr (fun x y => max (f x) y) 0 tl<GOAL>f (hd + tl.sum) ≤ max (f hd) (foldr (fun x y => max (f x) y) 0 tl)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>x : X<VAR>y : Y<GOAL>𝓝 (x, y) = map Prod.swap (𝓝 (y, x))
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>x : X<VAR>y : Y<GOAL>map (fun p => (p.2, p.1)) (𝓝 y ×ˢ 𝓝 x) = map Prod.swap (𝓝 y ×ˢ 𝓝 x)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝¹ : OrderedCancelCommMonoid M<VAR>f g : ι → M<VAR>s t : Finset ι<VAR>inst✝ : DecidableEq ι<GOAL>∏ i ∈ s \ t, f i < ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i < ∏ i ∈ t, f i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝¹ : OrderedCancelCommMonoid M<VAR>f g : ι → M<VAR>s t : Finset ι<VAR>inst✝ : DecidableEq ι<GOAL>Disjoint (t \ s) (s ∩ t)
<VAR>𝓕 : Type u_1<VAR>α✝ : Type u_2<VAR>E✝ : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : SeminormedCommGroup E✝<VAR>inst✝² : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E✝<VAR>r r₁ r₂ : ℝ<VAR>α : Type u_5<VAR>E : Type u_6<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : PseudoEMetricSpace α<VAR>K Kf Kg : ℝ≥0<VAR>f g : α → E<VAR>s : Set α<VAR>x : α<VAR>hf : AntilipschitzWith Kf f<VAR>hg : LipschitzWith Kg (g / f)<VAR>hK : Kg < Kf⁻¹<GOAL>AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ g
<VAR>f : StieltjesFunction<VAR>a b : ℝ<GOAL>f.measure (Icc a b) = ofReal (↑f b - leftLim (↑f) a)
<VAR>f : StieltjesFunction<VAR>a b : ℝ<VAR>hab : a ≤ b<GOAL>f.measure (Icc a b) = ofReal (↑f b - leftLim (↑f) a)
<VAR>f : StieltjesFunction<VAR>a b : ℝ<VAR>hab : b < a<GOAL>f.measure (Icc a b) = ofReal (↑f b - leftLim (↑f) a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>u v : α → ℝ<GOAL>IsBigOWith c l (fun x => ‖f' x‖) g ↔ IsBigOWith c l f' g
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>hs : 0 ∈ s<GOAL>balancedCore 𝕜 s = ⋂ r, ⋂ (_ : 1 ≤ ‖r‖), r • s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>hs : 0 ∈ s<GOAL>balancedCoreAux 𝕜 s ⊆ balancedCore 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>hs : 0 ∈ s<GOAL>0 ∈ balancedCoreAux 𝕜 s
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f : X → ↑F X<VAR>P : PFunctor.{u}<VAR>α : Type u_2<VAR>g : α → ↑P α<VAR>x : α<GOAL>(M.corec g x).dest = P.map (M.corec g) (g x)
<VAR>α : Type u_1<VAR>f g h σ τ : Perm α<VAR>hστ : σ.Disjoint τ<VAR>a : α<GOAL>(σ * τ) a = a ↔ σ a = a ∧ τ a = a
<VAR>α : Type u_1<VAR>f g h✝ σ τ : Perm α<VAR>hστ : σ.Disjoint τ<VAR>a : α<VAR>h : (σ * τ) a = a<GOAL>σ a = a ∧ τ a = a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>h0 : 0 ∈ balancedCoreAux 𝕜 s<VAR>a : 𝕜<VAR>ha : ‖a‖ ≤ 1<VAR>y : E<VAR>hy : y ∈ balancedCoreAux 𝕜 s<GOAL>(fun x => a • x) y ∈ balancedCoreAux 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>h0 : 0 ∈ balancedCoreAux 𝕜 s<VAR>y : E<VAR>hy : y ∈ balancedCoreAux 𝕜 s<VAR>ha : ‖0‖ ≤ 1<GOAL>(fun x => 0 • x) y ∈ balancedCoreAux 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>h0 : 0 ∈ balancedCoreAux 𝕜 s<VAR>a : 𝕜<VAR>ha : ‖a‖ ≤ 1<VAR>y : E<VAR>hy : y ∈ balancedCoreAux 𝕜 s<VAR>h : a ≠ 0<GOAL>(fun x => a • x) y ∈ balancedCoreAux 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>h0 : 0 ∈ balancedCoreAux 𝕜 s<VAR>a : 𝕜<VAR>ha : ‖a‖ ≤ 1<VAR>y : E<VAR>hy : ∀ (r : 𝕜), 1 ≤ ‖r‖ → y ∈ r • s<VAR>h : a ≠ 0<GOAL>∀ (r : 𝕜), 1 ≤ ‖r‖ → (fun x => a • x) y ∈ r • s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>h0 : 0 ∈ balancedCoreAux 𝕜 s<VAR>a : 𝕜<VAR>ha : ‖a‖ ≤ 1<VAR>y : E<VAR>hy : ∀ (r : 𝕜), 1 ≤ ‖r‖ → y ∈ r • s<VAR>h : a ≠ 0<VAR>r : 𝕜<VAR>hr : 1 ≤ ‖r‖<GOAL>(fun x => a • x) y ∈ r • s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>h0 : 0 ∈ balancedCoreAux 𝕜 s<VAR>a : 𝕜<VAR>ha : ‖a‖ ≤ 1<VAR>y : E<VAR>hy : ∀ (r : 𝕜), 1 ≤ ‖r‖ → y ∈ r • s<VAR>h : a ≠ 0<VAR>r : 𝕜<VAR>hr : 1 ≤ ‖r‖<VAR>h'' : 1 ≤ ‖a⁻¹ • r‖<GOAL>(fun x => a • x) y ∈ r • s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>h0 : 0 ∈ balancedCoreAux 𝕜 s<VAR>a : 𝕜<VAR>ha : ‖a‖ ≤ 1<VAR>y : E<VAR>hy : ∀ (r : 𝕜), 1 ≤ ‖r‖ → y ∈ r • s<VAR>h : a ≠ 0<VAR>r : 𝕜<VAR>hr : 1 ≤ ‖r‖<VAR>h'' : 1 ≤ ‖a⁻¹ • r‖<VAR>h' : y ∈ (a⁻¹ • r) • s<GOAL>(fun x => a • x) y ∈ r • s
<VAR>J : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝² : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>inst✝ : Category.{v₄, u₄} D<VAR>F : J ⥤ C<VAR>G : C ⥤ D<VAR>A : Cocone F<VAR>X✝ Y✝ : J<VAR>f✝ : X✝ ⟶ Y✝<GOAL>(F ⋙ G).map f✝ ≫ (fun j => G.map (A.ι.app j)) Y✝ = (fun j => G.map (A.ι.app j)) X✝ ≫ ((const J).obj (G.obj A.pt)).map f✝
<VAR>J : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝² : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>inst✝ : Category.{v₄, u₄} D<VAR>F : J ⥤ C<VAR>G : C ⥤ D<VAR>A : Cocone F<VAR>X✝ Y✝ : J<VAR>f✝ : X✝ ⟶ Y✝<GOAL>G.map (F.map f✝ ≫ A.ι.app Y✝) = (fun j => G.map (A.ι.app j)) X✝ ≫ ((const J).obj (G.obj A.pt)).map f✝
<VAR>J : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝² : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>inst✝ : Category.{v₄, u₄} D<VAR>F : J ⥤ C<VAR>G : C ⥤ D<VAR>X✝ Y✝ : Cocone F<VAR>f : X✝ ⟶ Y✝<VAR>j✝ : J<GOAL>((fun A => { pt := G.obj A.pt, ι := { app := fun j => G.map (A.ι.app j), naturality := ⋯ } }) X✝).ι.app j✝ ≫ G.map f.hom = ((fun A => { pt := G.obj A.pt, ι := { app := fun j => G.map (A.ι.app j), naturality := ⋯ } }) Y✝).ι.app j✝
<VAR>a b c : Cardinal.{u_1}<VAR>hc : ℵ₀ ≤ c<VAR>h1 : a < c<VAR>h2 : b < c<VAR>h : ℵ₀ ≤ max a b<GOAL>max a b + max a b < c
<VAR>a b c : Cardinal.{u_1}<VAR>hc : ℵ₀ ≤ c<VAR>h1 : a < c<VAR>h2 : b < c<VAR>h : ℵ₀ ≤ max a b<GOAL>max a b < c
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>θ : Real.Angle<VAR>f : V ≃ₗᵢ[ℝ] ℂ<VAR>hf : (map (Fin 2) f.toLinearEquiv) o = Complex.orientation<VAR>x : V<GOAL>f ((o.rotation θ) x) = ↑θ.expMapCircle * f x
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.13544, u_1} C<VAR>W₁ W₂ : MorphismProperty C<VAR>data : W₁.FunctorialFactorizationData W₂<VAR>J : Type u_2<VAR>inst✝ : Category.{?u.13627, u_2} J<VAR>f : Arrow (J ⥤ C)<VAR>j : J<GOAL>data.mapZ { left := f.left.map (𝟙 j), right := f.right.map (𝟙 j), w := ⋯ } = 𝟙 (data.factorizationData (f.hom.app j)).Z
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.13544, u_1} C<VAR>W₁ W₂ : MorphismProperty C<VAR>data : W₁.FunctorialFactorizationData W₂<VAR>J : Type u_2<VAR>inst✝ : Category.{?u.13627, u_2} J<VAR>f : Arrow (J ⥤ C)<VAR>j : J<GOAL>data.mapZ { left := f.left.map (𝟙 j), right := f.right.map (𝟙 j), w := ⋯ } = data.mapZ (𝟙 (Arrow.mk (f.hom.app j)))
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.13544, u_1} C<VAR>W₁ W₂ : MorphismProperty C<VAR>data : W₁.FunctorialFactorizationData W₂<VAR>J : Type u_2<VAR>inst✝ : Category.{?u.13627, u_2} J<VAR>f : Arrow (J ⥤ C)<VAR>X✝ Y✝ Z✝ : J<VAR>x✝¹ : X✝ ⟶ Y✝<VAR>x✝ : Y✝ ⟶ Z✝<GOAL>data.mapZ { left := f.left.map (x✝¹ ≫ x✝), right := f.right.map (x✝¹ ≫ x✝), w := ⋯ } = data.mapZ { left := f.left.map x✝¹, right := f.right.map x✝¹, w := ⋯ } ≫ data.mapZ { left := f.left.map x✝, right := f.right.map x✝, w := ⋯ }
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.13544, u_1} C<VAR>W₁ W₂ : MorphismProperty C<VAR>data : W₁.FunctorialFactorizationData W₂<VAR>J : Type u_2<VAR>inst✝ : Category.{?u.13627, u_2} J<VAR>f : Arrow (J ⥤ C)<VAR>X✝ Y✝ Z✝ : J<VAR>x✝¹ : X✝ ⟶ Y✝<VAR>x✝ : Y✝ ⟶ Z✝<GOAL>data.mapZ { left := f.left.map (x✝¹ ≫ x✝), right := f.right.map (x✝¹ ≫ x✝), w := ⋯ } = data.mapZ ({ left := f.left.map x✝¹, right := f.right.map x✝¹, w := ⋯ } ≫ { left := f.left.map x✝, right := f.right.map x✝, w := ⋯ })
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.13544, u_1} C<VAR>W₁ W₂ : MorphismProperty C<VAR>data : W₁.FunctorialFactorizationData W₂<VAR>J : Type u_2<VAR>inst✝ : Category.{?u.13627, u_2} J<VAR>X✝ Y✝ : Arrow (J ⥤ C)<VAR>τ : X✝ ⟶ Y✝<VAR>x✝¹ x✝ : J<VAR>α : x✝¹ ⟶ x✝<GOAL>data.mapZ { left := X✝.left.map α, right := X✝.right.map α, w := ⋯ } ≫ data.mapZ { left := τ.left.app x✝, right := τ.right.app x✝, w := ⋯ } = data.mapZ { left := τ.left.app x✝¹, right := τ.right.app x✝¹, w := ⋯ } ≫ data.mapZ { left := Y✝.left.map α, right := Y✝.right.map α, w := ⋯ }
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.13544, u_1} C<VAR>W₁ W₂ : MorphismProperty C<VAR>data : W₁.FunctorialFactorizationData W₂<VAR>J : Type u_2<VAR>inst✝ : Category.{?u.13627, u_2} J<VAR>X✝ Y✝ : Arrow (J ⥤ C)<VAR>τ : X✝ ⟶ Y✝<VAR>x✝¹ x✝ : J<VAR>α : x✝¹ ⟶ x✝<GOAL>data.mapZ ({ left := X✝.left.map α, right := X✝.right.map α, w := ⋯ } ≫ { left := τ.left.app x✝, right := τ.right.app x✝, w := ⋯ }) = data.mapZ ({ left := τ.left.app x✝¹, right := τ.right.app x✝¹, w := ⋯ } ≫ { left := Y✝.left.map α, right := Y✝.right.map α, w := ⋯ })
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.13544, u_1} C<VAR>W₁ W₂ : MorphismProperty C<VAR>data : W₁.FunctorialFactorizationData W₂<VAR>J : Type u_2<VAR>inst✝ : Category.{?u.13627, u_2} J<VAR>f : Arrow (J ⥤ C)<VAR>j : J<GOAL>data.mapZ { left := 𝟙 (f.left.obj j), right := 𝟙 (f.right.obj j), w := ⋯ } = 𝟙 (data.factorizationData (f.hom.app j)).Z
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.13544, u_1} C<VAR>W₁ W₂ : MorphismProperty C<VAR>data : W₁.FunctorialFactorizationData W₂<VAR>J : Type u_2<VAR>inst✝ : Category.{?u.13627, u_2} J<VAR>f : Arrow (J ⥤ C)<VAR>j : J<GOAL>data.mapZ { left := 𝟙 (f.left.obj j), right := 𝟙 (f.right.obj j), w := ⋯ } = data.mapZ (𝟙 (Arrow.mk (f.hom.app j)))
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.13544, u_1} C<VAR>W₁ W₂ : MorphismProperty C<VAR>data : W₁.FunctorialFactorizationData W₂<VAR>J : Type u_2<VAR>inst✝ : Category.{?u.13627, u_2} J<VAR>X✝ Y✝ Z✝ : Arrow (J ⥤ C)<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<VAR>j : J<GOAL>data.mapZ { left := f.left.app j ≫ g.left.app j, right := f.right.app j ≫ g.right.app j, w := ⋯ } = data.mapZ { left := f.left.app j, right := f.right.app j, w := ⋯ } ≫ data.mapZ { left := g.left.app j, right := g.right.app j, w := ⋯ }
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.13544, u_1} C<VAR>W₁ W₂ : MorphismProperty C<VAR>data : W₁.FunctorialFactorizationData W₂<VAR>J : Type u_2<VAR>inst✝ : Category.{?u.13627, u_2} J<VAR>X✝ Y✝ Z✝ : Arrow (J ⥤ C)<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<VAR>j : J<GOAL>data.mapZ { left := f.left.app j ≫ g.left.app j, right := f.right.app j ≫ g.right.app j, w := ⋯ } = data.mapZ ({ left := f.left.app j, right := f.right.app j, w := ⋯ } ≫ { left := g.left.app j, right := g.right.app j, w := ⋯ })
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι✝ : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s : Set E<VAR>i j : ι✝<VAR>c : R<VAR>t✝ : Finset ι✝<VAR>w✝ : ι✝ → R<VAR>z : ι✝ → E<VAR>ι : Type u_8<VAR>t : Finset ι<VAR>p : ι → E<VAR>w : ι → R<VAR>hw₂ : ∑ i ∈ t, w i = 1<GOAL>(affineCombination R t p) w = t.centerMass w p
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι✝ : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s : Set E<VAR>i j : ι✝<VAR>c : R<VAR>t✝ : Finset ι✝<VAR>w✝ : ι✝ → R<VAR>z : ι✝ → E<VAR>ι : Type u_8<VAR>t : Finset ι<VAR>p : ι → E<VAR>w : ι → R<VAR>hw₂ : ∑ i ∈ t, w i = 1<GOAL>∑ i ∈ t, w i • (p i -ᵥ 0) = ∑ i ∈ t, w i • p i
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>A B : T.Algebra<VAR>h : A.A ≅ B.A<VAR>w : autoParam (T.map h.hom ≫ B.a = A.a ≫ h.hom) _auto✝<GOAL>T.map h.inv ≫ A.a = B.a ≫ h.inv
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>A B : T.Algebra<VAR>h : A.A ≅ B.A<VAR>w : autoParam (T.map h.hom ≫ B.a = A.a ≫ h.hom) _auto✝<GOAL>T.map (h.inv ≫ h.hom) ≫ B.a = B.a
<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>X Y Z : C<VAR>f✝ : Y ⟶ X<VAR>S✝ R : Sieve X<VAR>f : Y ⟶ X<VAR>g : Z ⟶ Y<VAR>S : Sieve X<GOAL>pullback (g ≫ f) S = pullback g (pullback f S)
<VAR>z w : ℍ<VAR>r R : ℝ<VAR>a : { x // 0 < x }<VAR>y₁ y₂ : ℍ<GOAL>dist (a • y₁) (a • y₂) = dist y₁ y₂
<VAR>z w : ℍ<VAR>r R : ℝ<VAR>a : { x // 0 < x }<VAR>y₁ y₂ : ℍ<GOAL>2 * arsinh (dist (↑a • ↑y₁) (↑a • ↑y₂) / (2 * √(↑a * y₁.im * (↑a * y₂.im)))) = 2 * arsinh (dist ↑y₁ ↑y₂ / (2 * √(y₁.im * y₂.im)))
<VAR>z w : ℍ<VAR>r R : ℝ<VAR>a : { x // 0 < x }<VAR>y₁ y₂ : ℍ<GOAL>dist (↑a • ↑y₁) (↑a • ↑y₂) / (2 * √(↑a * y₁.im * (↑a * y₂.im))) = dist ↑y₁ ↑y₂ / (2 * √(y₁.im * y₂.im))
<VAR>z w : ℍ<VAR>r R : ℝ<VAR>a : { x // 0 < x }<VAR>y₁ y₂ : ℍ<GOAL>|↑a| * dist ↑y₁ ↑y₂ / (|↑a| * (2 * √(y₁.im * y₂.im))) = dist ↑y₁ ↑y₂ / (2 * √(y₁.im * y₂.im))
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>m n : ℕ<VAR>hm : p m<VAR>hn : p n<VAR>heq : count p m = count p n<GOAL>m = n
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>m n : ℕ<VAR>hm : p m<VAR>hn : p n<VAR>heq : count p m = count p n<VAR>h : m ≠ n<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>k m : ℕ<VAR>hkm : k ≠ m<VAR>x y : R<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>(C x * X ^ k + C y * X ^ m).support = {k, m}
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>k m : ℕ<VAR>hkm : k ≠ m<VAR>x y : R<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>{k, m} ⊆ (C x * X ^ k + C y * X ^ m).support
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>f g : E →ₗ.[R] F<VAR>h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y<GOAL>g ≤ f.sup g h
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>f g : E →ₗ.[R] F<VAR>h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y<VAR>z₁ : ↥g.domain<VAR>z₂ : ↥(f.sup g h).domain<VAR>hz : ↑z₁ = ↑z₂<GOAL>↑g z₁ = ↑(f.sup g h) z₂
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>f g : E →ₗ.[R] F<VAR>h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y<VAR>z₁ : ↥g.domain<VAR>z₂ : ↥(f.sup g h).domain<VAR>hz : ↑z₁ = ↑z₂<GOAL>↑f 0 + ↑g z₁ = ↑(f.sup g h) z₂
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>f g : E →ₗ.[R] F<VAR>h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y<VAR>z₁ : ↥g.domain<VAR>z₂ : ↥(f.sup g h).domain<VAR>hz : ↑z₁ = ↑z₂<GOAL>↑0 + ↑z₁ = ↑z₂
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>(Ico a b).card = ↑b - ↑a
<GOAL>Pairwise fun x y => 1 ≤ dist ↑x ↑y
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>hs : IsCompact s<VAR>ht : IsClosed t<VAR>hst : Disjoint s t<GOAL>∃ r, 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>t : Set α<VAR>Φ : α → β<VAR>ht : IsClosed t<VAR>hs : IsCompact ∅<VAR>hst : Disjoint ∅ t<GOAL>∃ r, 0 < r ∧ ∀ x ∈ ∅, ∀ y ∈ t, ↑r < edist x y
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>hs : IsCompact s<VAR>ht : IsClosed t<VAR>hst : Disjoint s t<VAR>hne : s.Nonempty<GOAL>∃ r, 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x✝ y : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>hs : IsCompact s<VAR>ht : IsClosed t<VAR>hst : Disjoint s t<VAR>hne : s.Nonempty<VAR>x : α<VAR>hx : x ∈ s<VAR>h : IsMinOn (fun x => infEdist x ?m.37155) s x<GOAL>∃ r, 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x✝ y : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>hs : IsCompact s<VAR>ht : IsClosed t<VAR>hst : Disjoint s t<VAR>hne : s.Nonempty<VAR>x : α<VAR>hx : x ∈ s<VAR>h : IsMinOn (fun x => infEdist x ?m.37155) s x<VAR>this : 0 < infEdist x t<GOAL>∃ r, 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x✝ y : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>hs : IsCompact s<VAR>ht : IsClosed t<VAR>hst : Disjoint s t<VAR>hne : s.Nonempty<VAR>x : α<VAR>hx : x ∈ s<VAR>h : IsMinOn (fun x => infEdist x ?m.37155) s x<VAR>this : 0 < infEdist x t<VAR>r : ℝ≥0<VAR>h₀ : 0 < ↑r<VAR>hr : ↑r < infEdist x t<GOAL>∃ r, 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y
<VAR>α : Type u_1<VAR>n : Nat<VAR>a : α<VAR>l : List α<GOAL>leftpad n a l = leftpadTR n a l
<VAR>α✝ : Type u<VAR>u : Level<VAR>α : Type u_1<VAR>inst✝ : DivisionRing α<VAR>n : ℤ<VAR>d : ℕ<VAR>h : ↑d ≠ 0<VAR>this : Invertible ↑d<GOAL>Rat.rawCast n d = ↑n * ⅟↑d
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : SFinite ν<VAR>f : β × α → γ<VAR>hf : AEMeasurable f (ν.prod μ)<GOAL>AEMeasurable (fun z => f z.swap) (μ.prod ν)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : SFinite ν<VAR>f : β × α → γ<VAR>hf : AEMeasurable f (map Prod.swap (μ.prod ν))<GOAL>AEMeasurable (fun z => f z.swap) (μ.prod ν)