ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>inst✝¹² : Group G<VAR>inst✝¹¹ : MeasurableSpace G<VAR>inst✝¹⁰ : TopologicalSpace G<VAR>inst✝⁹ : TopologicalGroup G<VAR>inst✝⁸ : BorelSpace G<VAR>inst✝⁷ : PolishSpace G<VAR>Γ : Subgroup G<VAR>inst✝⁶ : Countable ↥Γ<VAR>inst✝⁵ : Γ.Normal<VAR>inst✝⁴ : T2Space (G ⧸ Γ)<VAR>inst✝³ : SecondCountableTopology (G ⧸ Γ)<VAR>μ✝ : Measure (G ⧸ Γ)<VAR>ν : Measure G<VAR>inst✝² : SigmaFinite ν<VAR>inst✝¹ : ν.IsHaarMeasure<VAR>inst✝ : ν.IsMulRightInvariant<VAR>K : PositiveCompacts (G ⧸ Γ)<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν<VAR>h𝓕_finite : ν 𝓕 ≠ ⊤<VAR>c : ℝ≥0∞ := ν (QuotientGroup.mk ⁻¹' ↑K ∩ 𝓕)<VAR>c_ne_top : c ≠ ⊤<VAR>μ : Measure (G ⧸ Γ) := c • haarMeasure K<VAR>hμK : μ ↑K = c<GOAL>QuotientMeasureEqMeasurePreimage ν μ
<VAR>G : Type u_1<VAR>inst✝¹² : Group G<VAR>inst✝¹¹ : MeasurableSpace G<VAR>inst✝¹⁰ : TopologicalSpace G<VAR>inst✝⁹ : TopologicalGroup G<VAR>inst✝⁸ : BorelSpace G<VAR>inst✝⁷ : PolishSpace G<VAR>Γ : Subgroup G<VAR>inst✝⁶ : Countable ↥Γ<VAR>inst✝⁵ : Γ.Normal<VAR>inst✝⁴ : T2Space (G ⧸ Γ)<VAR>inst✝³ : SecondCountableTopology (G ⧸ Γ)<VAR>μ✝ : Measure (G ⧸ Γ)<VAR>ν : Measure G<VAR>inst✝² : SigmaFinite ν<VAR>inst✝¹ : ν.IsHaarMeasure<VAR>inst✝ : ν.IsMulRightInvariant<VAR>K : PositiveCompacts (G ⧸ Γ)<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν<VAR>h𝓕_finite : ν 𝓕 ≠ ⊤<VAR>c : ℝ≥0∞ := ν (QuotientGroup.mk ⁻¹' ↑K ∩ 𝓕)<VAR>c_ne_top : c ≠ ⊤<VAR>μ : Measure (G ⧸ Γ) := c • haarMeasure K<VAR>hμK : μ ↑K = c<VAR>this : SigmaFinite μ<GOAL>QuotientMeasureEqMeasurePreimage ν μ
<VAR>G : Type u_1<VAR>inst✝¹² : Group G<VAR>inst✝¹¹ : MeasurableSpace G<VAR>inst✝¹⁰ : TopologicalSpace G<VAR>inst✝⁹ : TopologicalGroup G<VAR>inst✝⁸ : BorelSpace G<VAR>inst✝⁷ : PolishSpace G<VAR>Γ : Subgroup G<VAR>inst✝⁶ : Countable ↥Γ<VAR>inst✝⁵ : Γ.Normal<VAR>inst✝⁴ : T2Space (G ⧸ Γ)<VAR>inst✝³ : SecondCountableTopology (G ⧸ Γ)<VAR>μ✝ : Measure (G ⧸ Γ)<VAR>ν : Measure G<VAR>inst✝² : SigmaFinite ν<VAR>inst✝¹ : ν.IsHaarMeasure<VAR>inst✝ : ν.IsMulRightInvariant<VAR>K : PositiveCompacts (G ⧸ Γ)<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν<VAR>h𝓕_finite : ν 𝓕 ≠ ⊤<VAR>c : ℝ≥0∞ := ν (QuotientGroup.mk ⁻¹' ↑K ∩ 𝓕)<VAR>c_ne_top : c ≠ ⊤<VAR>μ : Measure (G ⧸ Γ) := c • haarMeasure K<VAR>hμK : μ ↑K = c<VAR>this : SigmaFinite μ<GOAL>(interior ↑K).Nonempty
<VAR>G : Type u_1<VAR>inst✝¹² : Group G<VAR>inst✝¹¹ : MeasurableSpace G<VAR>inst✝¹⁰ : TopologicalSpace G<VAR>inst✝⁹ : TopologicalGroup G<VAR>inst✝⁸ : BorelSpace G<VAR>inst✝⁷ : PolishSpace G<VAR>Γ : Subgroup G<VAR>inst✝⁶ : Countable ↥Γ<VAR>inst✝⁵ : Γ.Normal<VAR>inst✝⁴ : T2Space (G ⧸ Γ)<VAR>inst✝³ : SecondCountableTopology (G ⧸ Γ)<VAR>μ✝ : Measure (G ⧸ Γ)<VAR>ν : Measure G<VAR>inst✝² : SigmaFinite ν<VAR>inst✝¹ : ν.IsHaarMeasure<VAR>inst✝ : ν.IsMulRightInvariant<VAR>K : PositiveCompacts (G ⧸ Γ)<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν<VAR>h𝓕_finite : ν 𝓕 ≠ ⊤<VAR>c : ℝ≥0∞ := ν (QuotientGroup.mk ⁻¹' ↑K ∩ 𝓕)<VAR>c_ne_top : c ≠ ⊤<VAR>μ : Measure (G ⧸ Γ) := c • haarMeasure K<VAR>hμK : μ ↑K = c<VAR>this : SigmaFinite μ<GOAL>μ ↑K = ν (QuotientGroup.mk ⁻¹' ↑K ∩ 𝓕)
<VAR>G : Type u_1<VAR>inst✝¹² : Group G<VAR>inst✝¹¹ : MeasurableSpace G<VAR>inst✝¹⁰ : TopologicalSpace G<VAR>inst✝⁹ : TopologicalGroup G<VAR>inst✝⁸ : BorelSpace G<VAR>inst✝⁷ : PolishSpace G<VAR>Γ : Subgroup G<VAR>inst✝⁶ : Countable ↥Γ<VAR>inst✝⁵ : Γ.Normal<VAR>inst✝⁴ : T2Space (G ⧸ Γ)<VAR>inst✝³ : SecondCountableTopology (G ⧸ Γ)<VAR>μ✝ : Measure (G ⧸ Γ)<VAR>ν : Measure G<VAR>inst✝² : SigmaFinite ν<VAR>inst✝¹ : ν.IsHaarMeasure<VAR>inst✝ : ν.IsMulRightInvariant<VAR>K : PositiveCompacts (G ⧸ Γ)<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν<VAR>h𝓕_finite : ν 𝓕 ≠ ⊤<VAR>c : ℝ≥0∞ := ν (QuotientGroup.mk ⁻¹' ↑K ∩ 𝓕)<VAR>c_ne_top : c ≠ ⊤<VAR>μ : Measure (G ⧸ Γ) := c • haarMeasure K<VAR>hμK : μ ↑K = c<VAR>this : SigmaFinite μ<GOAL>μ ↑K ≠ ⊤
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y : Mon_ (C ⥤ C)<VAR>f : X✝ ⟶ Y<VAR>X : C<GOAL>(ofMon X✝).η.app X ≫ __src✝.app X = (ofMon Y).η.app X
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y : Mon_ (C ⥤ C)<VAR>f : X✝ ⟶ Y<VAR>X : C<GOAL>Y.one.app X = (ofMon Y).η.app X
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : Mon_ (C ⥤ C)<VAR>f : X ⟶ Y<VAR>Z : C<GOAL>(ofMon X).μ.app Z ≫ __src✝.app Z = ((ofMon X).map (__src✝.app Z) ≫ __src✝.app ((ofMon Y).obj Z)) ≫ (ofMon Y).μ.app Z
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : Mon_ (C ⥤ C)<VAR>f : X ⟶ Y<VAR>Z : C<GOAL>(MonoidalCategory.tensorHom f.hom f.hom ≫ Y.mul).app Z = ((ofMon X).map (__src✝.app Z) ≫ __src✝.app ((ofMon Y).obj Z)) ≫ (ofMon Y).μ.app Z
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : Mon_ (C ⥤ C)<VAR>f : X ⟶ Y<VAR>Z : C<GOAL>(f.hom.app (X.X.obj Z) ≫ Y.X.map (f.hom.app Z)) ≫ Y.mul.app Z = ((ofMon X).map (f.hom.app Z) ≫ f.hom.app (Y.X.obj Z)) ≫ Y.mul.app Z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort u_6<VAR>s✝ t u : Set α<VAR>ms : Set (MeasurableSpace α)<VAR>s : Set α<GOAL>GenerateMeasurable (⋃₀ ((fun m => {t | MeasurableSet t}) '' ms)) s ↔ GenerateMeasurable {s | ∃ m ∈ ms, MeasurableSet s} s
<VAR>α : Type u_1<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c : α<GOAL>Ioo a a = 0
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace F<VAR>proj : Z → B<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace (TotalSpace F E)<VAR>e : Trivialization F proj<VAR>x z : Z<VAR>hz : z ∈ e.source<GOAL>𝓝 z = comap proj (𝓝 (proj z)) ⊓ comap (Prod.snd ∘ ↑e) (𝓝 (↑e z).2)
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace F<VAR>proj : Z → B<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace (TotalSpace F E)<VAR>e : Trivialization F proj<VAR>x z : Z<VAR>hz : z ∈ e.source<VAR>l : Filter Z<GOAL>l ≤ 𝓝 z ↔ l ≤ comap proj (𝓝 (proj z)) ⊓ comap (Prod.snd ∘ ↑e) (𝓝 (↑e z).2)
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace F<VAR>proj : Z → B<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace (TotalSpace F E)<VAR>e : Trivialization F proj<VAR>x z : Z<VAR>hz : z ∈ e.source<VAR>l : Filter Z<GOAL>l ≤ 𝓝 z ↔ Tendsto proj l (𝓝 (proj z)) ∧ Tendsto (Prod.snd ∘ ↑e) l (𝓝 (↑e z).2)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>ha : P.a = 0<VAR>hb : P.b = 0<VAR>hc : P.c ≠ 0<GOAL>P.toPoly.leadingCoeff = P.c
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β → β<VAR>op : α → α → α<VAR>inst✝² : Monoid α<VAR>inst✝¹ : Monoid β<VAR>inst✝ : FunLike F α β<VAR>s : Multiset α<VAR>comm : {x | x ∈ s}.Pairwise Commute<VAR>y : α<VAR>h : ∀ x ∈ s, Commute y x<GOAL>Commute y (s.noncommProd comm)
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β → β<VAR>op : α → α → α<VAR>inst✝² : Monoid α<VAR>inst✝¹ : Monoid β<VAR>inst✝ : FunLike F α β<VAR>y : α<VAR>a✝ : List α<VAR>comm : {x | x ∈ ⟦a✝⟧}.Pairwise Commute<VAR>h : ∀ x ∈ ⟦a✝⟧, Commute y x<GOAL>Commute y (noncommProd ⟦a✝⟧ comm)
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β → β<VAR>op : α → α → α<VAR>inst✝² : Monoid α<VAR>inst✝¹ : Monoid β<VAR>inst✝ : FunLike F α β<VAR>y : α<VAR>a✝ : List α<VAR>comm : {x | x ∈ ⟦a✝⟧}.Pairwise Commute<VAR>h : ∀ x ∈ ⟦a✝⟧, Commute y x<GOAL>Commute y a✝.prod
<VAR>R : Type u_1<VAR>inst✝⁸ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M'<VAR>ι : Type u_4<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>e✝ : Basis ι R M<VAR>A : Type u_5<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Module A M<VAR>e : Basis ι A M<VAR>f : M →ₗ[A] M<VAR>v : ι → M<GOAL>e.det (⇑f ∘ v) = LinearMap.det f * e.det v
<VAR>a b c : ℕ<GOAL>Ico 0 = range
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>s₁ s₂ s₃ s₄ : AList β<VAR>p₁₂ : s₁.entries ~ s₂.entries<VAR>p₃₄ : s₃.entries ~ s₄.entries<GOAL>(s₁ ∪ s₃).entries ~ (s₂ ∪ s₄).entries
<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∞<GOAL>∃ s, s.Countable ∧ Dense s ∧ 0 ∉ s ∧ ⊤ ∉ s
<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✝ s : Set ℝ≥0∞<VAR>s_count : s.Countable<VAR>s_dense : Dense s<VAR>hs : (∀ (x : ℝ≥0∞), IsBot x → x ∉ s) ∧ ∀ (x : ℝ≥0∞), IsTop x → x ∉ s<GOAL>∃ s, s.Countable ∧ Dense s ∧ 0 ∉ s ∧ ⊤ ∉ s
<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>R : Type u_1<VAR>inst✝ : Ring R<VAR>p : R[X]<VAR>n : ℕ<VAR>a : R<VAR>n✝ : ℕ<GOAL>(p.update n a).coeff n✝ = (p + C (a - p.coeff n) * X ^ n).coeff n✝
<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>R : Type u_1<VAR>inst✝ : Ring R<VAR>p : R[X]<VAR>n : ℕ<VAR>a : R<VAR>n✝ : ℕ<GOAL>(if n✝ = n then a else p.coeff n✝) = p.coeff n✝ + if n✝ = n then a - p.coeff n else 0
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝¹ : HasImage f<VAR>W : C<VAR>g h : image f ⟶ W<VAR>inst✝ : HasLimit (parallelPair g h)<VAR>w : factorThruImage f ≫ g = factorThruImage f ≫ h<VAR>q : equalizer g h ⟶ image f := equalizer.ι g h<VAR>e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w<GOAL>g = h
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝¹ : HasImage f<VAR>W : C<VAR>g h : image f ⟶ W<VAR>inst✝ : HasLimit (parallelPair g h)<VAR>w : factorThruImage f ≫ g = factorThruImage f ≫ h<VAR>q : equalizer g h ⟶ image f := equalizer.ι g h<VAR>e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w<VAR>F' : MonoFactorisation f := MonoFactorisation.mk (equalizer g h) (q ≫ ι f) e' ⋯<GOAL>g = h
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝¹ : HasImage f<VAR>W : C<VAR>g h : image f ⟶ W<VAR>inst✝ : HasLimit (parallelPair g h)<VAR>w : factorThruImage f ≫ g = factorThruImage f ≫ h<VAR>q : equalizer g h ⟶ image f := equalizer.ι g h<VAR>e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w<VAR>F' : MonoFactorisation f := MonoFactorisation.mk (equalizer g h) (q ≫ ι f) e' ⋯<VAR>v : image f ⟶ F'.I := lift F'<GOAL>g = h
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝¹ : HasImage f<VAR>W : C<VAR>g h : image f ⟶ W<VAR>inst✝ : HasLimit (parallelPair g h)<VAR>w : factorThruImage f ≫ g = factorThruImage f ≫ h<VAR>q : equalizer g h ⟶ image f := equalizer.ι g h<VAR>e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w<VAR>F' : MonoFactorisation f := MonoFactorisation.mk (equalizer g h) (q ≫ ι f) e' ⋯<VAR>v : image f ⟶ F'.I := lift F'<VAR>t₀ : v ≫ q ≫ ι f = ι f<GOAL>g = h
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝¹ : HasImage f<VAR>W : C<VAR>g h : image f ⟶ W<VAR>inst✝ : HasLimit (parallelPair g h)<VAR>w : factorThruImage f ≫ g = factorThruImage f ≫ h<VAR>q : equalizer g h ⟶ image f := equalizer.ι g h<VAR>e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w<VAR>F' : MonoFactorisation f := MonoFactorisation.mk (equalizer g h) (q ≫ ι f) e' ⋯<VAR>v : image f ⟶ F'.I := lift F'<VAR>t₀ : v ≫ q ≫ ι f = ι f<VAR>t : v ≫ q = 𝟙 (image f)<GOAL>g = h
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A<VAR>h₁₂ : a₁ + a₂ = a₁₂<VAR>h₂₃ : a₂ + a₃ = a₂₃<VAR>h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃<GOAL>a₁ + a₂₃ = a₁₂₃
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>a₁ a₂ a₃ : A<VAR>X : C<GOAL>(shiftFunctorAdd' C (a₁ + a₂) a₃ (a₁ + a₂ + a₃) ⋯).hom.app X ≫ (shiftFunctor C a₃).map ((shiftFunctorAdd' C a₁ a₂ (a₁ + a₂) ⋯).hom.app X) ≫ 𝟙 ((shiftFunctor C a₃).obj ((shiftFunctor C a₂).obj ((shiftFunctor C a₁).obj X))) = (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯).hom.app X ≫ (shiftFunctorAdd' C a₂ a₃ (a₂ + a₃) ⋯).hom.app ((shiftFunctor C a₁).obj X)
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>a₁ a₂ a₃ : A<VAR>X : C<GOAL>(shiftFunctorAdd C (a₁ + a₂) a₃).hom.app X ≫ (shiftFunctor C a₃).map ((shiftFunctorAdd C a₁ a₂).hom.app X) = (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯).hom.app X ≫ (shiftFunctorAdd C a₂ a₃).hom.app ((shiftFunctor C a₁).obj X)
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>a₁ a₂ a₃ : A<VAR>X : C<GOAL>(shiftFunctorAdd C (a₁ + a₂) a₃).hom.app X ≫ (shiftFunctor C a₃).map ((shiftFunctorAdd C a₁ a₂).hom.app X) = ((eqToHom ⋯).app X ≫ (shiftFunctorAdd C a₁ (a₂ + a₃)).hom.app X) ≫ (shiftFunctorAdd C a₂ a₃).hom.app ((shiftFunctor C a₁).obj X)
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>a₁ a₂ a₃ : A<VAR>X : C<GOAL>(shiftFunctorAdd C (a₁ + a₂) a₃).hom.app X ≫ (shiftFunctor C a₃).map ((shiftFunctorAdd C a₁ a₂).hom.app X) = (eqToHom ⋯ ≫ (shiftFunctorAdd C a₁ (a₂ + a₃)).hom.app X) ≫ (shiftFunctorAdd C a₂ a₃).hom.app ((shiftFunctor C a₁).obj X)
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>a₁ a₂ a₃ : A<VAR>X : C<GOAL>((shiftMonoidalFunctor C A).μIso { as := a₁ + a₂ } { as := a₃ }).inv.app X ≫ ((shiftMonoidalFunctor C A).obj { as := a₃ }).map (((shiftMonoidalFunctor C A).μIso { as := a₁ } { as := a₂ }).inv.app X) = (eqToHom ⋯ ≫ ((shiftMonoidalFunctor C A).μIso { as := a₁ } { as := a₂ + a₃ }).inv.app X) ≫ ((shiftMonoidalFunctor C A).μIso { as := a₂ } { as := a₃ }).inv.app (((shiftMonoidalFunctor C A).obj { as := a₁ }).obj X)
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>a₁ a₂ a₃ : A<VAR>X : C<GOAL>((shiftMonoidalFunctor C A).μIso { as := a₁ + a₂ } { as := a₃ }).inv.app X ≫ ((shiftMonoidalFunctor C A).μ (MonoidalCategory.tensorObj { as := a₁ } { as := a₂ }) { as := a₃ }).app X ≫ eqToHom ⋯ ≫ ((shiftMonoidalFunctor C A).μIso { as := a₁ } (MonoidalCategory.tensorObj { as := a₂ } { as := a₃ })).inv.app X ≫ ((shiftMonoidalFunctor C A).μIso { as := a₂ } { as := a₃ }).inv.app (((shiftMonoidalFunctor C A).obj { as := a₁ }).obj X) = (eqToHom ⋯ ≫ ((shiftMonoidalFunctor C A).μIso { as := a₁ } { as := a₂ + a₃ }).inv.app X) ≫ ((shiftMonoidalFunctor C A).μIso { as := a₂ } { as := a₃ }).inv.app (((shiftMonoidalFunctor C A).obj { as := a₁ }).obj X)
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>a₁ a₂ a₃ : A<VAR>X : C<GOAL>eqToHom ⋯ ≫ ((shiftMonoidalFunctor C A).μIso { as := a₁ } (MonoidalCategory.tensorObj { as := a₂ } { as := a₃ })).inv.app X ≫ ((shiftMonoidalFunctor C A).μIso { as := a₂ } { as := a₃ }).inv.app (((shiftMonoidalFunctor C A).obj { as := a₁ }).obj X) = eqToHom ⋯ ≫ ((shiftMonoidalFunctor C A).μIso { as := a₁ } { as := a₂ + a₃ }).inv.app X ≫ ((shiftMonoidalFunctor C A).μIso { as := a₂ } { as := a₃ }).inv.app (((shiftMonoidalFunctor C A).obj { as := a₁ }).obj X)
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup N<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>Q : QuadraticMap R M N<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra S R<VAR>inst✝³ : Module S M<VAR>inst✝² : IsScalarTower S R M<VAR>inst✝¹ : Module S N<VAR>inst✝ : IsScalarTower S R N<VAR>a : S<VAR>x y : M<GOAL>polar (⇑Q) (a • x) y = a • polar (⇑Q) x y
<VAR>a : ℤ<VAR>b : ℕ<VAR>h : IsInt a (Int.negOfNat b)<GOAL>-a = ↑b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>c : ℝ≥0∞<VAR>s : Set α<GOAL>(const α c).lintegral (μ.restrict s) = c * μ s
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>hST : IsComplement S T<VAR>hHT : IsComplement (↑H) T<VAR>hSK : IsComplement S ↑K<VAR>g : G<VAR>h1 : 1 ∈ T<GOAL>↑(hST.equiv g).2 = 1 ↔ g ∈ S
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>β✝ : Type u_4<VAR>β' : Type u_5<VAR>γ : Type u_6<VAR>γ' : Type u_7<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>f✝ : Ω → β✝<VAR>g : Ω → β'<VAR>β : Type u_8<VAR>m : MeasurableSpace β<VAR>inst✝² : CommMonoid β<VAR>inst✝¹ : MeasurableMul₂ β<VAR>f : ι → Ω → β<VAR>inst✝ : IsMarkovKernel κ<VAR>hf_Indep : iIndepFun (fun x => m) f κ μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>s : Finset ι<VAR>i : ι<VAR>hi : i ∉ s<GOAL>IndepFun (∏ j ∈ s, f j) (f i) κ μ
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>inst✝ : LinearOrder α<VAR>a : α<GOAL>Bounded (fun x x_1 => x ≤ x_1) (s ∩ {b | a ≤ b}) ↔ Bounded (fun x x_1 => x ≤ x_1) s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>inst✝ : LinearOrder α<VAR>a : α<GOAL>Bounded (fun x x_1 => x ≤ x_1) (s ∩ {b | a ≤ b}) → Bounded (fun x x_1 => x ≤ x_1) s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>inst✝ : LinearOrder α<VAR>a : α<GOAL>Bounded (fun x x_1 => x ≤ x_1) (s ∩ {b | a ≤ b}) → Bounded (fun x x_1 => x ≤ x_1) (s ∩ {b | a < b})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : DecidableEq β<VAR>b : β<VAR>a : α<GOAL>∏' (b' : β), Pi.mulSingle b a b' = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : DecidableEq β<VAR>b : β<VAR>a : α<GOAL>Pi.mulSingle b a b = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : DecidableEq β<VAR>b : β<VAR>a : α<GOAL>∀ (b' : β), b' ≠ b → Pi.mulSingle b a b' = 1
<GOAL>𝔠 ^ ℵ₀ = 𝔠
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝³ : Nonempty α<VAR>inst✝² : SemilatticeSup α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : NoMaxOrder β<VAR>f : α → β<VAR>h : Tendsto f atTop atTop<VAR>M : β<VAR>hM : M ∈ upperBounds (range f)<GOAL>False
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝³ : Nonempty α<VAR>inst✝² : SemilatticeSup α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : NoMaxOrder β<VAR>f : α → β<VAR>h : Tendsto f atTop atTop<VAR>M : β<VAR>hM : M ∈ upperBounds (range f)<VAR>a : α<VAR>ha : ∀ b ≥ a, b ∈ f ⁻¹' Ioi M<GOAL>False
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝³ : Nonempty α<VAR>inst✝² : SemilatticeSup α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : NoMaxOrder β<VAR>f : α → β<VAR>h : Tendsto f atTop atTop<VAR>M : β<VAR>hM : M ∈ upperBounds (range f)<VAR>a : α<VAR>ha : ∀ b ≥ a, b ∈ f ⁻¹' Ioi M<GOAL>M < M
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : HasShift C ℤ<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>T : Triangle Cᵒᵖ<GOAL>T ∈ distinguishedTriangles C ↔ Opposite.unop ((triangleOpEquivalence C).inverse.obj T) ∈ Pretriangulated.distinguishedTriangles
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>H : 1 = 0<GOAL>X.support = ∅
<VAR>n : ℕ<GOAL>catalan n = n.centralBinom / (n + 1)
<VAR>n : ℕ<GOAL>↑(catalan n) = ↑n.centralBinom / (↑n + 1)
<GOAL>↑(catalan 0) = ↑(Nat.centralBinom 0) / (↑0 + 1)
<VAR>d : ℕ<VAR>hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)<GOAL>↑(catalan d.succ) = ↑d.succ.centralBinom / (↑d.succ + 1)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : NonPreadditiveAbelian C<VAR>X Y : C<VAR>a b : X ⟶ Y<GOAL>-(a + b) = -a - b
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝² : SemilatticeSup α<VAR>inst✝¹ : OrderBot α<VAR>s s₁ s₂ : Finset β<VAR>f g : β → α<VAR>a : α<VAR>inst✝ : DecidableEq β<VAR>c : α<GOAL>(s₁ ∪ s₂).sup f ≤ c ↔ s₁.sup f ⊔ s₂.sup f ≤ c
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁵ : OrderedRing 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : AddCommGroup G<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y : E<GOAL>[x-[𝕜]y] = (fun θ => x + θ • (y - x)) '' Icc 0 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁵ : OrderedRing 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : AddCommGroup G<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y : E<VAR>a✝¹ : 𝕜<VAR>a✝ : a✝¹ ∈ Icc 0 1<GOAL>x + a✝¹ • (y - x) = (1 - a✝¹) • x + a✝¹ • y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁵ : OrderedRing 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : AddCommGroup G<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y : E<VAR>a✝¹ : 𝕜<VAR>a✝ : a✝¹ ∈ Icc 0 1<GOAL>x + (a✝¹ • y - a✝¹ • x) = x - a✝¹ • x + a✝¹ • y
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : RCLike 𝕜<VAR>F : Type u_2<VAR>inst✝³ : SeminormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : Module ℝ F<VAR>inst✝ : IsScalarTower ℝ 𝕜 F<VAR>fr : F →ₗ[ℝ] ℝ<VAR>x : F<GOAL>re (fr.extendTo𝕜' x) = fr x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : R<VAR>h : ‖x‖ < 1<GOAL>(1 + x) * ∑' (i : ℕ), x ^ i = 2 * ∑' (i : ℕ), x ^ i - 1
<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>inst✝ : CompactSpace X<VAR>U : X → Set X<VAR>hU : ∀ (x : X), U x ∈ 𝓝 x<GOAL>∃ t, ⋃ x ∈ t, U 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>inst✝ : CompactSpace X<VAR>U : X → Set X<VAR>hU : ∀ (x : X), U x ∈ 𝓝 x<VAR>t : Finset X<VAR>s : univ ⊆ ⋃ x ∈ t, U x<GOAL>∃ t, ⋃ x ∈ t, U x = ⊤
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>f : Arrow C<VAR>inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom<VAR>S : SplitEpi f.hom<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>WidePullback.lift (WidePullback.base fun x => f.hom) (fun i => if x : i = 0 then (WidePullback.base fun x => f.hom) ≫ S.section_ else WidePullback.π (fun x => f.hom) (i.pred x)) ⋯ ≫ WidePullback.π (fun x => f.hom) i.succ = WidePullback.π (fun x => f.hom) i
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>f : Arrow C<VAR>inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom<VAR>S : SplitEpi f.hom<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>(if x : i.succ = 0 then (WidePullback.base fun x => f.hom) ≫ S.section_ else WidePullback.π (fun x => f.hom) (i.succ.pred x)) = WidePullback.π (fun x => f.hom) i
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>inst✝¹ : Inhabited Γ<VAR>inst✝ : Inhabited Γ'<VAR>f : PointedMap Γ Γ'<VAR>l : ListBlank Γ<GOAL>(map f l).head = f.f l.head
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>inst✝¹ : Inhabited Γ<VAR>inst✝ : Inhabited Γ'<VAR>f : PointedMap Γ Γ'<VAR>l : ListBlank Γ<GOAL>(map f (cons l.head l.tail)).head = f.f l.head
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n✝ m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q a : MvPolynomial σ R<VAR>n : ℕ<GOAL>(a ^ n).totalDegree ≤ n * a.totalDegree
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n✝ m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q a : MvPolynomial σ R<VAR>n : ℕ<GOAL>(∏ _k ∈ Finset.range n, a).totalDegree ≤ ∑ _k ∈ Finset.range n, a.totalDegree
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n✝ m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q a : MvPolynomial σ R<VAR>n : ℕ<VAR>x✝¹ x✝ : σ →₀ ℕ<GOAL>((x✝¹ + x✝).sum fun x e => e) = (x✝¹.sum fun x e => e) + x✝.sum fun x e => e