ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : LE α<VAR>s t : UpperSet α<VAR>a : α<VAR>S : Set (UpperSet α)<GOAL>↑(sSup S).compl = ↑(⨆ s ∈ S, s.compl)
<VAR>G : Type u<VAR>inst✝ : Group G<GOAL>commutator G = Subgroup.closure (commutatorSet G)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>inst✝ : CompleteSpace E<VAR>c : E<GOAL>∫ (x : X) in s, c ∂μ = (μ s).toReal • c
<VAR>n : ℕ<VAR>c : Composition n<VAR>j : Fin n<GOAL>c.sizeUpTo ↑(c.index j) ≤ ↑j
<VAR>n : ℕ<VAR>c : Composition n<VAR>j : Fin n<VAR>H : ¬c.sizeUpTo ↑(c.index j) ≤ ↑j<GOAL>False
<VAR>n : ℕ<VAR>c : Composition n<VAR>j : Fin n<VAR>i : Fin c.length := c.index j<VAR>H : ↑j < c.sizeUpTo ↑i<GOAL>False
<VAR>n : ℕ<VAR>c : Composition n<VAR>j : Fin n<VAR>i : Fin c.length := c.index j<VAR>H : ↑j < c.sizeUpTo ↑i<VAR>i_pos : 0 < ↑i<GOAL>False
<VAR>n : ℕ<VAR>c : Composition n<VAR>j : Fin n<VAR>i : Fin c.length := c.index j<VAR>H : ↑j < c.sizeUpTo ↑i<VAR>i_pos : 0 < ↑i<VAR>i₁ : ℕ := (↑i).pred<GOAL>False
<VAR>n : ℕ<VAR>c : Composition n<VAR>j : Fin n<VAR>i : Fin c.length := c.index j<VAR>H : ↑j < c.sizeUpTo ↑i<VAR>i_pos : 0 < ↑i<VAR>i₁ : ℕ := (↑i).pred<VAR>i₁_lt_i : i₁ < ↑i<GOAL>False
<VAR>n : ℕ<VAR>c : Composition n<VAR>j : Fin n<VAR>i : Fin c.length := c.index j<VAR>H : ↑j < c.sizeUpTo ↑i<VAR>i_pos : 0 < ↑i<VAR>i₁ : ℕ := (↑i).pred<VAR>i₁_lt_i : i₁ < ↑i<VAR>i₁_succ : i₁ + 1 = ↑i<GOAL>False
<VAR>n : ℕ<VAR>c : Composition n<VAR>j : Fin n<VAR>i : Fin c.length := c.index j<VAR>H : ↑j < c.sizeUpTo ↑i<VAR>i_pos : 0 < ↑i<VAR>i₁ : ℕ := (↑i).pred<VAR>i₁_lt_i : i₁ < ↑i<VAR>i₁_succ : i₁ + 1 = ↑i<VAR>this : ¬(↑j < c.sizeUpTo (i₁ + 1) ∧ i₁ < c.length)<GOAL>False
<VAR>n : ℕ<VAR>c : Composition n<VAR>j : Fin n<VAR>i : Fin c.length := c.index j<VAR>H : ↑j < c.sizeUpTo ↑i<VAR>i_pos : 0 < ↑i<VAR>i₁ : ℕ := (↑i).pred<VAR>i₁_lt_i : i₁ < ↑i<VAR>i₁_succ : i₁ + 1 = ↑i<VAR>this : c.sizeUpTo ↑i ≤ ↑j<GOAL>False
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>f : E →ₗ[ℝ] E<VAR>s : Set E<GOAL>μ (⇑f '' s) = ENNReal.ofReal |LinearMap.det f| * μ s
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>f : E →ₗ[ℝ] E<VAR>s : Set E<VAR>hf : LinearMap.det f ≠ 0<GOAL>μ (⇑f '' s) = ENNReal.ofReal |LinearMap.det f| * μ s
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>f : E →ₗ[ℝ] E<VAR>s : Set E<VAR>hf : LinearMap.det f = 0<GOAL>μ (⇑f '' s) = ENNReal.ofReal |LinearMap.det f| * μ s
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>ai : R<VAR>au : a * ai = 1<GOAL>p.natDegree = (p * 1).natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>ai : R<VAR>au : a * ai = 1<GOAL>(p * 1).natDegree = (p * C a * C ai).natDegree
<VAR>X : Type u_1<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>μ : Measure X<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : X →ᵇ ℝ<VAR>c : ℝ<GOAL>∫ (x : X), (f + const X c) x ∂μ = ∫ (x : X), f x ∂μ + (μ Set.univ).toReal • c
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Computation α<VAR>f : α → Computation β<VAR>a : α<VAR>b : β<VAR>m n : ℕ<VAR>h1 : s.Results a m<VAR>h2 : (f a).Results b n<GOAL>(s.bind f).Results b (n + m)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Computation α<VAR>f : α → Computation β<VAR>a : α<VAR>b : β<VAR>m n : ℕ<VAR>h1 : s.Results a m<VAR>h2 : (f a).Results b n<VAR>this : a ∈ s<GOAL>(s.bind f).Results b (n + m)
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>hz : z ≤ y<VAR>hx : x ≤ y<VAR>H : Disjoint z (y \ x)<GOAL>z ⊔ y \ x ≤ x ⊔ y \ x
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>hz : z ≤ y<VAR>hx : x ≤ y<VAR>H : Disjoint z (y \ x)<GOAL>z ⊔ y \ x ≤ y
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>hz : z ≤ y<VAR>hx : x ≤ y<VAR>H : Disjoint z (y \ x)<GOAL>z ⊔ y ≤ y
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D✝ : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D✝<VAR>J : Type u<VAR>inst✝ : Category.{v, u} J<VAR>T : Comonad C<VAR>D : J ⥤ T.Coalgebra<VAR>c : Cocone (D ⋙ T.forget)<VAR>t : IsColimit c<VAR>s : Cocone D<VAR>j : J<GOAL>c.ι.app j ≫ t.desc (newCocone D c) ≫ T.map (t.desc (T.forget.mapCocone s)) = c.ι.app j ≫ t.desc (T.forget.mapCocone s) ≫ s.pt.a
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D✝ : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D✝<VAR>J : Type u<VAR>inst✝ : Category.{v, u} J<VAR>T : Comonad C<VAR>D : J ⥤ T.Coalgebra<VAR>c : Cocone (D ⋙ T.forget)<VAR>t : IsColimit c<VAR>s : Cocone D<VAR>j : J<GOAL>(D.obj j).a ≫ T.map ((T.forget.mapCocone s).ι.app j) = T.forget.map (s.ι.app j) ≫ s.pt.a
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D✝ : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D✝<VAR>J✝ : Type u<VAR>inst✝ : Category.{v, u} J✝<VAR>T : Comonad C<VAR>D : J✝ ⥤ T.Coalgebra<VAR>c : Cocone (D ⋙ T.forget)<VAR>t : IsColimit c<VAR>s : Cocone D<VAR>m : (liftedCocone D c t).pt ⟶ s.pt<VAR>J : ∀ (j : J✝), (liftedCocone D c t).ι.app j ≫ m = s.ι.app j<GOAL>m.f = ((fun s => { f := t.desc (T.forget.mapCocone s), h := ⋯ }) s).f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D✝ : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D✝<VAR>J✝ : Type u<VAR>inst✝ : Category.{v, u} J✝<VAR>T : Comonad C<VAR>D : J✝ ⥤ T.Coalgebra<VAR>c : Cocone (D ⋙ T.forget)<VAR>t : IsColimit c<VAR>s : Cocone D<VAR>m : (liftedCocone D c t).pt ⟶ s.pt<VAR>J : ∀ (j : J✝), (liftedCocone D c t).ι.app j ≫ m = s.ι.app j<GOAL>∀ (j : J✝), c.ι.app j ≫ m.f = c.ι.app j ≫ ((fun s => { f := t.desc (T.forget.mapCocone s), h := ⋯ }) s).f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D✝ : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D✝<VAR>J✝ : Type u<VAR>inst✝ : Category.{v, u} J✝<VAR>T : Comonad C<VAR>D : J✝ ⥤ T.Coalgebra<VAR>c : Cocone (D ⋙ T.forget)<VAR>t : IsColimit c<VAR>s : Cocone D<VAR>m : (liftedCocone D c t).pt ⟶ s.pt<VAR>J : ∀ (j : J✝), (liftedCocone D c t).ι.app j ≫ m = s.ι.app j<VAR>j : J✝<GOAL>c.ι.app j ≫ m.f = c.ι.app j ≫ ((fun s => { f := t.desc (T.forget.mapCocone s), h := ⋯ }) s).f
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>inst✝¹ : Category.{?u.66755, u_2} V<VAR>c : ComplexShape ι<VAR>inst✝ : HasZeroMorphisms V<VAR>X : (HomologicalComplex Vᵒᵖ c)ᵒᵖ<VAR>i✝ : ι<GOAL>((unopFunctor V c).map ((unopUnitIso V c).hom.app X) ≫ (unopCounitIso V c).hom.app ((unopFunctor V c).obj X)).f i✝ = (𝟙 ((unopFunctor V c).obj X)).f i✝
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>inst✝¹ : Category.{?u.66755, u_2} V<VAR>c : ComplexShape ι<VAR>inst✝ : HasZeroMorphisms V<VAR>X : (HomologicalComplex Vᵒᵖ c)ᵒᵖ<VAR>i✝ : ι<GOAL>((unopFunctor V c).map ((unopUnitIso V c).hom.app X)).f i✝ ≫ ((unopCounitIso V c).hom.app ((unopFunctor V c).obj X)).f i✝ = (𝟙 ((unopFunctor V c).obj X)).f i✝
<VAR>a b : ZNum<GOAL>(↑a.abs).gcd ↑b.abs = (↑a).gcd ↑b
<VAR>a b : ZNum<GOAL>(↑a).natAbs.gcd (↑b).natAbs = (↑a).gcd ↑b
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : SetLike σ A<VAR>inst✝³ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>s : Set A<VAR>h : ∀ x ∈ s, Homogeneous 𝒜 x<VAR>i : ι<VAR>r : A<VAR>hr : r ∈ span s<GOAL>↑(((decompose 𝒜) r) i) ∈ span s
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : SetLike σ A<VAR>inst✝³ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>s : Set A<VAR>h : ∀ x ∈ s, Homogeneous 𝒜 x<VAR>i : ι<VAR>r : A<VAR>hr : r ∈ LinearMap.range (Finsupp.total (↑s) A A Subtype.val)<GOAL>↑(((decompose 𝒜) r) i) ∈ span s
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : SetLike σ A<VAR>inst✝³ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>s : Set A<VAR>h : ∀ x ∈ s, Homogeneous 𝒜 x<VAR>i : ι<VAR>r : A<VAR>hr : ∃ y, (Finsupp.total (↑s) A A Subtype.val) y = r<GOAL>↑(((decompose 𝒜) r) i) ∈ span s
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : SetLike σ A<VAR>inst✝³ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>s✝ : Set A<VAR>h : ∀ x ∈ s✝, Homogeneous 𝒜 x<VAR>i : ι<VAR>s : ↑s✝ →₀ A<GOAL>↑(((decompose 𝒜) ((Finsupp.total (↑s✝) A A Subtype.val) s)) i) ∈ span s✝
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : SetLike σ A<VAR>inst✝³ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>s✝ : Set A<VAR>h : ∀ x ∈ s✝, Homogeneous 𝒜 x<VAR>i : ι<VAR>s : ↑s✝ →₀ A<GOAL>∑ i_1 ∈ s.support, ↑(((decompose 𝒜) (s i_1 • ↑i_1)) i) ∈ span s✝
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : SetLike σ A<VAR>inst✝³ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>s✝ : Set A<VAR>h : ∀ x ∈ s✝, Homogeneous 𝒜 x<VAR>i : ι<VAR>s : ↑s✝ →₀ A<GOAL>∀ c ∈ s.support, ↑(((decompose 𝒜) (s c • ↑c)) i) ∈ span s✝
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : SetLike σ A<VAR>inst✝³ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>s✝ : Set A<VAR>h : ∀ x ∈ s✝, Homogeneous 𝒜 x<VAR>i : ι<VAR>s : ↑s✝ →₀ A<VAR>z : ↑s✝<VAR>hz1 : z ∈ s.support<GOAL>↑(((decompose 𝒜) (s z • ↑z)) i) ∈ span s✝
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : SetLike σ A<VAR>inst✝³ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>s✝ : Set A<VAR>h : ∀ x ∈ s✝, Homogeneous 𝒜 x<VAR>i : ι<VAR>s : ↑s✝ →₀ A<VAR>z : ↑s✝<VAR>hz1 : z ∈ s.support<GOAL>↑(((decompose 𝒜) (s z * ↑z)) i) ∈ span s✝
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : SetLike σ A<VAR>inst✝³ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>s✝ : Set A<VAR>h : ∀ x ∈ s✝, Homogeneous 𝒜 x<VAR>i : ι<VAR>s : ↑s✝ →₀ A<VAR>z : ↑s✝<VAR>hz1 : z ∈ s.support<GOAL>Homogeneous 𝒜 ↑z
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : SetLike σ A<VAR>inst✝³ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>s✝ : Set A<VAR>h : ∀ x ∈ s✝, Homogeneous 𝒜 x<VAR>i : ι<VAR>s : ↑s✝ →₀ A<VAR>z : ↑s✝<VAR>hz1 : z ∈ s.support<GOAL>↑z ∈ span s✝
<VAR>x y : ℝ<VAR>hx : 0 < x<GOAL>0 ≤ log x ↔ 1 ≤ x
<VAR>α : Type u<VAR>e : Encoding α<GOAL>Function.Injective e.encode
<VAR>α : Type u<VAR>e : Encoding α<VAR>x✝¹ x✝ : α<VAR>h : e.encode x✝¹ = e.encode x✝<GOAL>some x✝¹ = some x✝
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>v : ↥K<GOAL>↑((orthogonalProjection K) ↑v) = ↑v
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>M : Type u_7<VAR>E : Type u_8<VAR>R : Type u_9<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : TopologicalSpace α'<VAR>inst✝³ : One β<VAR>inst✝² : One γ<VAR>inst✝¹ : One δ<VAR>g : β → γ<VAR>f : α → β<VAR>f₂ : α → γ<VAR>m : β → γ → δ<VAR>x : α<VAR>inst✝ : TopologicalSpace β<VAR>hf : Continuous f<VAR>k : Set α<VAR>hk : IsCompact k<VAR>h'f : mulSupport f ⊆ k<GOAL>IsCompact (range f)
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>M : Type u_7<VAR>E : Type u_8<VAR>R : Type u_9<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : TopologicalSpace α'<VAR>inst✝³ : One β<VAR>inst✝² : One γ<VAR>inst✝¹ : One δ<VAR>g : β → γ<VAR>f : α → β<VAR>f₂ : α → γ<VAR>m : β → γ → δ<VAR>x : α<VAR>inst✝ : TopologicalSpace β<VAR>hf : Continuous f<VAR>k : Set α<VAR>hk : IsCompact k<VAR>h'f : mulSupport f ⊆ k<VAR>h2 : range f = f '' k<GOAL>IsCompact (f '' k)
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>M : Type u_7<VAR>E : Type u_8<VAR>R : Type u_9<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : TopologicalSpace α'<VAR>inst✝³ : One β<VAR>inst✝² : One γ<VAR>inst✝¹ : One δ<VAR>g : β → γ<VAR>f : α → β<VAR>f₂ : α → γ<VAR>m : β → γ → δ<VAR>x : α<VAR>inst✝ : TopologicalSpace β<VAR>hf : Continuous f<VAR>k : Set α<VAR>hk : IsCompact k<VAR>h'f : mulSupport f ⊆ k<VAR>h2 : range f = insert 1 (f '' k)<GOAL>IsCompact (insert 1 (f '' k))
<VAR>α : Sort ?u.56697<VAR>β : Sort ?u.56701<VAR>p : α → Prop<VAR>q : β → Prop<VAR>e : α ≃ β<VAR>h : ∀ (a : α), p a ↔ q (e a)<VAR>a : β<GOAL>q a ↔ p (e.symm a)
<VAR>α : Sort ?u.56697<VAR>β : Sort ?u.56701<VAR>p : α → Prop<VAR>q : β → Prop<VAR>e : α ≃ β<VAR>h : ∀ (a : α), p a ↔ q (e a)<VAR>a : β<GOAL>a = e (e.symm a)
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>Ui Vj : Finset α<GOAL>(Ui, Vj) ∈ P.parts.offDiag.attach.biUnion (SzemerediRegularity.distinctPairs hP G ε) → (Ui, Vj) ∈ (increment hP G ε).parts.offDiag
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>Ui Vj : Finset α<GOAL>∀ (x x_1 : Finset α) (x_2 : x ∈ P.parts ∧ x_1 ∈ P.parts ∧ ¬x = x_1), Ui ∈ (chunk hP G ε ⋯).parts → Vj ∈ (chunk hP G ε ⋯).parts → (∃ a, ∃ (h : a ∈ P.parts), Ui ∈ (chunk hP G ε ⋯).parts) ∧ (∃ a, ∃ (h : a ∈ P.parts), Vj ∈ (chunk hP G ε ⋯).parts) ∧ ¬Ui = Vj
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>Ui Vj U V : Finset α<VAR>hUV : U ∈ P.parts ∧ V ∈ P.parts ∧ ¬U = V<VAR>hUi : Ui ∈ (chunk hP G ε ⋯).parts<VAR>hVj : Vj ∈ (chunk hP G ε ⋯).parts<GOAL>¬Ui = Vj
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>Ui U V : Finset α<VAR>hUV : U ∈ P.parts ∧ V ∈ P.parts ∧ ¬U = V<VAR>hUi : Ui ∈ (chunk hP G ε ⋯).parts<VAR>hVj : Ui ∈ (chunk hP G ε ⋯).parts<GOAL>False
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>Ui U V : Finset α<VAR>hUV : U ∈ P.parts ∧ V ∈ P.parts ∧ ¬U = V<VAR>hUi : Ui ∈ (chunk hP G ε ⋯).parts<VAR>hVj : Ui ∈ (chunk hP G ε ⋯).parts<VAR>i : α<VAR>hi : i ∈ Ui<GOAL>False
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>p₁ p₂ : P<VAR>h : ¬Collinear k {p₁, p₂, p₁}<GOAL>False
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P✝ : Cᵒᵖ ⥤ Type v<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>J J₂ : GrothendieckTopology C<VAR>P : Cᵒᵖ ⥤ Type v<VAR>U : Sieve X<VAR>B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y<VAR>hU : Presieve.IsSheafFor P U.arrows<VAR>hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), Presieve.IsSheafFor P (B hf).arrows<VAR>hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback g (B h)).arrows<VAR>s : Presieve.FamilyOfElements P (Sieve.bind U.arrows B).arrows<VAR>hs : s.Compatible<GOAL>∃! t, s.IsAmalgamation t
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P✝ : Cᵒᵖ ⥤ Type v<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>J J₂ : GrothendieckTopology C<VAR>P : Cᵒᵖ ⥤ Type v<VAR>U : Sieve X<VAR>B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y<VAR>hU : Presieve.IsSheafFor P U.arrows<VAR>hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), Presieve.IsSheafFor P (B hf).arrows<VAR>hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback g (B h)).arrows<VAR>s : Presieve.FamilyOfElements P (Sieve.bind U.arrows B).arrows<VAR>hs : s.Compatible<VAR>y : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → Presieve.FamilyOfElements P (B hf).arrows := fun Y f hf Z g hg => s (g ≫ f) ⋯<GOAL>∃! t, s.IsAmalgamation t
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P✝ : Cᵒᵖ ⥤ Type v<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>J J₂ : GrothendieckTopology C<VAR>P : Cᵒᵖ ⥤ Type v<VAR>U : Sieve X<VAR>B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y<VAR>hU : Presieve.IsSheafFor P U.arrows<VAR>hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), Presieve.IsSheafFor P (B hf).arrows<VAR>hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback g (B h)).arrows<VAR>s : Presieve.FamilyOfElements P (Sieve.bind U.arrows B).arrows<VAR>hs : s.Compatible<VAR>y : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → Presieve.FamilyOfElements P (B hf).arrows := fun Y f hf Z g hg => s (g ≫ f) ⋯<VAR>hy : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).Compatible<VAR>t : Presieve.FamilyOfElements P U.arrows := fun Y f hf => ⋯.amalgamate (y hf) ⋯<GOAL>∃! t, s.IsAmalgamation t
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P✝ : Cᵒᵖ ⥤ Type v<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>J J₂ : GrothendieckTopology C<VAR>P : Cᵒᵖ ⥤ Type v<VAR>U : Sieve X<VAR>B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y<VAR>hU : Presieve.IsSheafFor P U.arrows<VAR>hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), Presieve.IsSheafFor P (B hf).arrows<VAR>hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback g (B h)).arrows<VAR>s : Presieve.FamilyOfElements P (Sieve.bind U.arrows B).arrows<VAR>hs : s.Compatible<VAR>y : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → Presieve.FamilyOfElements P (B hf).arrows := fun Y f hf Z g hg => s (g ≫ f) ⋯<VAR>hy : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).Compatible<VAR>t : Presieve.FamilyOfElements P U.arrows := fun Y f hf => ⋯.amalgamate (y hf) ⋯<VAR>ht : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).IsAmalgamation (t f hf)<GOAL>∃! t, s.IsAmalgamation t
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>x y : α × β<VAR>h₁ : a₁ < a₂<VAR>h₂ : b₁ ≤ b₂<GOAL>(a₁, b₁) < (a₂, b₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>s t u : Finset α<VAR>a b : α<GOAL>_root_.Disjoint {a} {b} ↔ a ≠ b
<VAR>p : Char → Bool<VAR>x✝ : Substring<VAR>h✝ : x✝.Valid<VAR>w✝² w✝¹ w✝ : List Char<VAR>h : ValidFor w✝² w✝¹ w✝ x✝<GOAL>(x✝.dropWhile p).toString.data = List.dropWhile p x✝.toString.data
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : PresheafedSpace C<VAR>f : X ⟶ Z<VAR>hf : IsOpenImmersion f<VAR>g : Y ⟶ Z<VAR>s : PullbackCone f g<GOAL>pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd = s.snd
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : PresheafedSpace C<VAR>f : X ⟶ Z<VAR>hf : IsOpenImmersion f<VAR>g : Y ⟶ Z<VAR>s : PullbackCone f g<GOAL>(pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd).base = s.snd.base
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : PresheafedSpace C<VAR>f : X ⟶ Z<VAR>hf : IsOpenImmersion f<VAR>g : Y ⟶ Z<VAR>s : PullbackCone f g<VAR>x : (Opens ↑↑Y)ᵒᵖ<GOAL>((pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd).c ≫ whiskerRight (eqToHom ⋯) s.pt.presheaf).app x = s.snd.c.app x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : Monoid α<VAR>a : α<GOAL>Quot.out (Associates.mk a) ~ᵤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν s : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hs : s ⟂ₘ ν<VAR>hadd : μ = s + ν.withDensity f<VAR>this : μ.HaveLebesgueDecomposition ν<GOAL>s = μ.singularPart ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν s : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hs : s ⟂ₘ ν<VAR>hadd : μ = s + ν.withDensity f<VAR>this : μ.HaveLebesgueDecomposition ν<VAR>hmeas : Measurable (μ.rnDeriv ν)<VAR>hsing : μ.singularPart ν ⟂ₘ ν<VAR>hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)<GOAL>s = μ.singularPart ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν s : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f<VAR>this : μ.HaveLebesgueDecomposition ν<VAR>hmeas : Measurable (μ.rnDeriv ν)<VAR>hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)<VAR>S : Set α<VAR>hS₁ : MeasurableSet S<VAR>hS₂ : s S = 0<VAR>hS₃ : ν Sᶜ = 0<VAR>T : Set α<VAR>hT₁ : MeasurableSet T<VAR>hT₂ : (μ.singularPart ν) T = 0<VAR>hT₃ : ν Tᶜ = 0<GOAL>s = μ.singularPart ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν s : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f<VAR>this : μ.HaveLebesgueDecomposition ν<VAR>hmeas : Measurable (μ.rnDeriv ν)<VAR>hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)<VAR>S : Set α<VAR>hS₁ : MeasurableSet S<VAR>hS₂ : s S = 0<VAR>hS₃ : ν Sᶜ = 0<VAR>T : Set α<VAR>hT₁ : MeasurableSet T<VAR>hT₂ : (μ.singularPart ν) T = 0<VAR>hT₃ : ν Tᶜ = 0<VAR>hνinter : ν (S ∩ T)ᶜ = 0<GOAL>s = μ.singularPart ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν s : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f<VAR>this : μ.HaveLebesgueDecomposition ν<VAR>hmeas : Measurable (μ.rnDeriv ν)<VAR>hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)<VAR>S : Set α<VAR>hS₁ : MeasurableSet S<VAR>hS₂ : s S = 0<VAR>hS₃ : ν Sᶜ = 0<VAR>T : Set α<VAR>hT₁ : MeasurableSet T<VAR>hT₂ : (μ.singularPart ν) T = 0<VAR>hT₃ : ν Tᶜ = 0<VAR>hνinter : ν (S ∩ T)ᶜ = 0<VAR>heq : s.restrict (S ∩ T)ᶜ = (μ.singularPart ν).restrict (S ∩ T)ᶜ<GOAL>s = μ.singularPart ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν s : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f<VAR>this : μ.HaveLebesgueDecomposition ν<VAR>hmeas : Measurable (μ.rnDeriv ν)<VAR>hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)<VAR>S : Set α<VAR>hS₁ : MeasurableSet S<VAR>hS₂ : s S = 0<VAR>hS₃ : ν Sᶜ = 0<VAR>T : Set α<VAR>hT₁ : MeasurableSet T<VAR>hT₂ : (μ.singularPart ν) T = 0<VAR>hT₃ : ν Tᶜ = 0<VAR>hνinter : ν (S ∩ T)ᶜ = 0<VAR>heq : s.restrict (S ∩ T)ᶜ = (μ.singularPart ν).restrict (S ∩ T)ᶜ<VAR>heq' : ∀ (A : Set α), MeasurableSet A → s A = (s.restrict (S ∩ T)ᶜ) A<GOAL>s = μ.singularPart ν