ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommSemiring S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommSemiring P<VAR>N : Submonoid S<VAR>T : Type u_4<VAR>inst✝⁵ : CommSemiring T<VAR>inst✝⁴ : Algebra R T<VAR>inst✝³ : Algebra S T<VAR>inst✝² : IsScalarTower R S T<VAR>inst✝¹ : IsLocalization M S<VAR>inst✝ : IsLocalization N T<VAR>x : T<VAR>y : S<VAR>s : ↥N<VAR>eq₁ : x * (algebraMap S T) ↑(y, s).2 = (algebraMap S T) (y, s).1<GOAL>∃ y, x * (algebraMap R T) ↑y.2 = (algebraMap R T) y.1
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommSemiring S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommSemiring P<VAR>N : Submonoid S<VAR>T : Type u_4<VAR>inst✝⁵ : CommSemiring T<VAR>inst✝⁴ : Algebra R T<VAR>inst✝³ : Algebra S T<VAR>inst✝² : IsScalarTower R S T<VAR>inst✝¹ : IsLocalization M S<VAR>inst✝ : IsLocalization N T<VAR>x : T<VAR>y : S<VAR>s : ↥N<VAR>eq₁ : x * (algebraMap S T) ↑(y, s).2 = (algebraMap S T) (y, s).1<VAR>z : R<VAR>t : ↥M<VAR>eq₂ : y * (algebraMap R S) ↑(z, t).2 = (algebraMap R S) (z, t).1<GOAL>∃ y, x * (algebraMap R T) ↑y.2 = (algebraMap R T) y.1
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommSemiring S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommSemiring P<VAR>N : Submonoid S<VAR>T : Type u_4<VAR>inst✝⁵ : CommSemiring T<VAR>inst✝⁴ : Algebra R T<VAR>inst✝³ : Algebra S T<VAR>inst✝² : IsScalarTower R S T<VAR>inst✝¹ : IsLocalization M S<VAR>inst✝ : IsLocalization N T<VAR>x : T<VAR>y : S<VAR>s : ↥N<VAR>eq₁ : x * (algebraMap S T) ↑(y, s).2 = (algebraMap S T) (y, s).1<VAR>z : R<VAR>t : ↥M<VAR>eq₂ : y * (algebraMap R S) ↑(z, t).2 = (algebraMap R S) (z, t).1<VAR>z' : R<VAR>t' : ↥M<VAR>eq₃ : ↑s * (algebraMap R S) ↑(z', t').2 = (algebraMap R S) (z', t').1<GOAL>∃ y, x * (algebraMap R T) ↑y.2 = (algebraMap R T) y.1
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>f : ι → Subgroup G<VAR>hs : ∀ i ∈ s, (f i).FiniteIndex<GOAL>(⨅ i ∈ s, f i).FiniteIndex
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>f : ι → Subgroup G<VAR>hs : ∀ i ∈ s, (f i).FiniteIndex<GOAL>(⨅ x, f ↑x).FiniteIndex
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Abelian C<VAR>inst✝¹ : HasExt C<VAR>X Y Z T : C<VAR>n : ℕ<VAR>inst✝ : HasDerivedCategory C<VAR>X₁ X₂ : C<VAR>α β : Ext (X₁ ⊞ X₂) Y n<VAR>h₁ : (mk₀ biprod.inl).comp α ⋯ = (mk₀ biprod.inl).comp β ⋯<VAR>h₂ : (mk₀ biprod.inr).comp α ⋯ = (mk₀ biprod.inr).comp β ⋯<VAR>this : HasDerivedCategory C := HasDerivedCategory.standard C<GOAL>α = β
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Abelian C<VAR>inst✝¹ : HasExt C<VAR>X Y Z T : C<VAR>n : ℕ<VAR>inst✝ : HasDerivedCategory C<VAR>X₁ X₂ : C<VAR>α β : Ext (X₁ ⊞ X₂) Y n<VAR>this : HasDerivedCategory C := HasDerivedCategory.standard C<VAR>h₂ : ((mk₀ biprod.inr).comp α ⋯).hom = ((mk₀ biprod.inr).comp β ⋯).hom<VAR>h₁ : ((mk₀ biprod.inl).comp α ⋯).hom = ((mk₀ biprod.inl).comp β ⋯).hom<GOAL>α.hom = β.hom
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Abelian C<VAR>inst✝¹ : HasExt C<VAR>X Y Z T : C<VAR>n : ℕ<VAR>inst✝ : HasDerivedCategory C<VAR>X₁ X₂ : C<VAR>α β : Ext (X₁ ⊞ X₂) Y n<VAR>this : HasDerivedCategory C := HasDerivedCategory.standard C<VAR>h₁ : (DerivedCategory.singleFunctor C 0).map biprod.inl ≫ α.hom = (DerivedCategory.singleFunctor C 0).map biprod.inl ≫ β.hom<VAR>h₂ : (DerivedCategory.singleFunctor C 0).map biprod.inr ≫ α.hom = (DerivedCategory.singleFunctor C 0).map biprod.inr ≫ β.hom<GOAL>α.hom = β.hom
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Abelian C<VAR>inst✝¹ : HasExt C<VAR>X Y Z T : C<VAR>n : ℕ<VAR>inst✝ : HasDerivedCategory C<VAR>X₁ X₂ : C<VAR>α β : Ext (X₁ ⊞ X₂) Y n<VAR>this : HasDerivedCategory C := HasDerivedCategory.standard C<VAR>h₁ : (DerivedCategory.singleFunctor C 0).map biprod.inl ≫ α.hom = (DerivedCategory.singleFunctor C 0).map biprod.inl ≫ β.hom<VAR>h₂ : (DerivedCategory.singleFunctor C 0).map biprod.inr ≫ α.hom = (DerivedCategory.singleFunctor C 0).map biprod.inr ≫ β.hom<GOAL>BinaryCofan.inl ((DerivedCategory.singleFunctor C 0).mapBinaryBicone (BinaryBiproduct.bicone X₁ X₂)).toCocone ≫ α.hom = BinaryCofan.inl ((DerivedCategory.singleFunctor C 0).mapBinaryBicone (BinaryBiproduct.bicone X₁ X₂)).toCocone ≫ β.hom
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Abelian C<VAR>inst✝¹ : HasExt C<VAR>X Y Z T : C<VAR>n : ℕ<VAR>inst✝ : HasDerivedCategory C<VAR>X₁ X₂ : C<VAR>α β : Ext (X₁ ⊞ X₂) Y n<VAR>this : HasDerivedCategory C := HasDerivedCategory.standard C<VAR>h₁ : (DerivedCategory.singleFunctor C 0).map biprod.inl ≫ α.hom = (DerivedCategory.singleFunctor C 0).map biprod.inl ≫ β.hom<VAR>h₂ : (DerivedCategory.singleFunctor C 0).map biprod.inr ≫ α.hom = (DerivedCategory.singleFunctor C 0).map biprod.inr ≫ β.hom<GOAL>BinaryCofan.inr ((DerivedCategory.singleFunctor C 0).mapBinaryBicone (BinaryBiproduct.bicone X₁ X₂)).toCocone ≫ α.hom = BinaryCofan.inr ((DerivedCategory.singleFunctor C 0).mapBinaryBicone (BinaryBiproduct.bicone X₁ X₂)).toCocone ≫ β.hom
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>n : ℕ<VAR>l : List α<VAR>h : l.Nodup<VAR>this : Pairwise (fun x x_1 => x ≠ x_1) l.sublists'<GOAL>(sublistsLen n l).Nodup
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : Mono f<GOAL>(imageMonoIsoSource f).hom ≫ f = image.ι f
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : Mono f<GOAL>(imageMonoIsoSource f).hom ≫ (imageMonoIsoSource f).inv ≫ image.ι f = image.ι f
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>d₁ : l₁.Nodup<VAR>d₂ : l₂.Nodup<GOAL>l₁ ~ l₂ ↔ ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>d₁ : l₁.Nodup<VAR>d₂ : l₂.Nodup<VAR>H : ∀ (a : α), a ∈ l₁ ↔ a ∈ l₂<GOAL>l₁ ~ l₂
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>𝒜✝ ℬ✝ : Finset (Finset α)<VAR>s : Finset α<VAR>𝒜 ℬ : Finset (Finset α)<GOAL>∑ s : Finset α, ↑((𝒜 ∪ ℬ).truncatedSup s).card / ((↑(card α) - ↑s.card) * ↑((card α).choose s.card)) + ∑ s : Finset α, ↑((𝒜 ⊼ ℬ).truncatedSup s).card / ((↑(card α) - ↑s.card) * ↑((card α).choose s.card)) = ∑ s : Finset α, ↑(𝒜.truncatedSup s).card / ((↑(card α) - ↑s.card) * ↑((card α).choose s.card)) + ∑ s : Finset α, ↑(ℬ.truncatedSup s).card / ((↑(card α) - ↑s.card) * ↑((card α).choose s.card))
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>𝒜✝ ℬ✝ : Finset (Finset α)<VAR>s : Finset α<VAR>𝒜 ℬ : Finset (Finset α)<GOAL>∀ s ∈ univ, ↑((𝒜 ∪ ℬ).truncatedSup s).card / ((↑(card α) - ↑s.card) * ↑((card α).choose s.card)) + ↑((𝒜 ⊼ ℬ).truncatedSup s).card / ((↑(card α) - ↑s.card) * ↑((card α).choose s.card)) = ↑(𝒜.truncatedSup s).card / ((↑(card α) - ↑s.card) * ↑((card α).choose s.card)) + ↑(ℬ.truncatedSup s).card / ((↑(card α) - ↑s.card) * ↑((card α).choose s.card))
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>𝒜✝ ℬ✝ : Finset (Finset α)<VAR>s : Finset α<VAR>𝒜 ℬ : Finset (Finset α)<GOAL>∀ s ∈ univ, True
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>s✝ t✝ : Set α<VAR>a✝ b✝ : α<VAR>inst✝ : LinearOrder γ<VAR>a b : γ<VAR>s t : Set γ<VAR>ha : IsLeast s a<VAR>hb : IsLeast t b<GOAL>min a b ∈ s ∪ t
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Abelian C<VAR>inst✝¹ : HasProjectiveResolutions C<VAR>inst✝ : EnoughProjectives C<VAR>Z : C<VAR>n : ℕ<GOAL>HomologicalComplex.ExactAt (ofComplex Z) (n + 1)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Abelian C<VAR>inst✝¹ : HasProjectiveResolutions C<VAR>inst✝ : EnoughProjectives C<VAR>Z : C<VAR>n : ℕ<GOAL>(HomologicalComplex.sc' (ofComplex Z) (n + 1 + 1) (n + 1) n).Exact
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Abelian C<VAR>inst✝¹ : HasProjectiveResolutions C<VAR>inst✝ : EnoughProjectives C<VAR>Z : C<VAR>n : ℕ<GOAL>(ShortComplex.mk ((ChainComplex.of (fun n => (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z)) (d (d (Projective.π Z))) ⋯ (fun S => ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) n).X₃) (fun n => (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z)) (d (d (Projective.π Z))) ⋯ (fun S => ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) n).g) ⋯).d (n + 1 + 1) (n + 1)) ((ChainComplex.of (fun n => (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z)) (d (d (Projective.π Z))) ⋯ (fun S => ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) n).X₃) (fun n => (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z)) (d (d (Projective.π Z))) ⋯ (fun S => ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) n).g) ⋯).d (n + 1) n) ⋯).Exact
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Abelian C<VAR>inst✝¹ : HasProjectiveResolutions C<VAR>inst✝ : EnoughProjectives C<VAR>Z : C<VAR>n : ℕ<GOAL>(ShortComplex.mk (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z)) (d (d (Projective.π Z))) ⋯ (fun S => ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) (n + 1)).g (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z)) (d (d (Projective.π Z))) ⋯ (fun S => ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) n).g ⋯).Exact
<VAR>R : Type u<VAR>M : Type v<VAR>M'✝ : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'✝<VAR>inst✝ : Module R M'✝<VAR>I J : Ideal R<VAR>N P : Submodule R M<VAR>S : Set R<VAR>T : Set M<VAR>M' : Submodule R M<VAR>s : Set R<VAR>hs : Ideal.span s = ⊤<VAR>x : M<VAR>H : ∀ (r : ↑s), ∃ n, ↑r ^ n • x ∈ M'<GOAL>x ∈ M'
<VAR>R : Type u<VAR>M : Type v<VAR>M'✝ : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'✝<VAR>inst✝ : Module R M'✝<VAR>I J : Ideal R<VAR>N P : Submodule R M<VAR>S : Set R<VAR>T : Set M<VAR>M' : Submodule R M<VAR>s : Set R<VAR>hs : Ideal.span s = ⊤<VAR>x : M<VAR>H : ∀ (r : ↑s), ∃ n, ↑r ^ n • x ∈ M'<VAR>s' : Finset R<VAR>hs₁ : ↑s' ⊆ s<VAR>hs₂ : Ideal.span ↑s' = ⊤<GOAL>x ∈ M'
<VAR>R : Type u<VAR>M : Type v<VAR>M'✝ : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'✝<VAR>inst✝ : Module R M'✝<VAR>I J : Ideal R<VAR>N P : Submodule R M<VAR>S : Set R<VAR>T : Set M<VAR>M' : Submodule R M<VAR>s : Set R<VAR>hs : Ideal.span s = ⊤<VAR>x : M<VAR>s' : Finset R<VAR>hs₁ : ↑s' ⊆ s<VAR>hs₂ : Ideal.span ↑s' = ⊤<VAR>H : ∀ (r : { x // x ∈ s' }), ∃ n, ↑r ^ n • x ∈ M'<GOAL>x ∈ M'
<VAR>R : Type u<VAR>M : Type v<VAR>M'✝ : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'✝<VAR>inst✝ : Module R M'✝<VAR>I J : Ideal R<VAR>N✝ P : Submodule R M<VAR>S : Set R<VAR>T : Set M<VAR>M' : Submodule R M<VAR>s : Set R<VAR>hs : Ideal.span s = ⊤<VAR>x : M<VAR>s' : Finset R<VAR>hs₁ : ↑s' ⊆ s<VAR>hs₂ : Ideal.span ↑s' = ⊤<VAR>n₁ : { x // x ∈ s' } → ℕ<VAR>n₂ : ∀ (r : { x // x ∈ s' }), ↑r ^ n₁ r • x ∈ M'<VAR>N : ℕ := s'.attach.sup n₁<GOAL>x ∈ M'
<VAR>R : Type u<VAR>M : Type v<VAR>M'✝ : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'✝<VAR>inst✝ : Module R M'✝<VAR>I J : Ideal R<VAR>N✝ P : Submodule R M<VAR>S : Set R<VAR>T : Set M<VAR>M' : Submodule R M<VAR>s : Set R<VAR>hs : Ideal.span s = ⊤<VAR>x : M<VAR>s' : Finset R<VAR>hs₁ : ↑s' ⊆ s<VAR>hs₂ : Ideal.span ↑s' = ⊤<VAR>n₁ : { x // x ∈ s' } → ℕ<VAR>n₂ : ∀ (r : { x // x ∈ s' }), ↑r ^ n₁ r • x ∈ M'<VAR>N : ℕ := s'.attach.sup n₁<VAR>hs' : Ideal.span ((fun x => x ^ N) '' ↑s') = ⊤<GOAL>x ∈ M'
<VAR>R : Type u<VAR>M : Type v<VAR>M'✝ : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'✝<VAR>inst✝ : Module R M'✝<VAR>I J : Ideal R<VAR>N✝ P : Submodule R M<VAR>S : Set R<VAR>T : Set M<VAR>M' : Submodule R M<VAR>s : Set R<VAR>hs : Ideal.span s = ⊤<VAR>x : M<VAR>s' : Finset R<VAR>hs₁ : ↑s' ⊆ s<VAR>hs₂ : Ideal.span ↑s' = ⊤<VAR>n₁ : { x // x ∈ s' } → ℕ<VAR>n₂ : ∀ (r : { x // x ∈ s' }), ↑r ^ n₁ r • x ∈ M'<VAR>N : ℕ := s'.attach.sup n₁<VAR>hs' : Ideal.span ((fun x => x ^ N) '' ↑s') = ⊤<GOAL>∀ (r : ↑((fun x => x ^ N) '' ↑s')), ↑r • x ∈ M'
<VAR>R : Type u<VAR>M : Type v<VAR>M'✝ : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'✝<VAR>inst✝ : Module R M'✝<VAR>I J : Ideal R<VAR>N✝ P : Submodule R M<VAR>S : Set R<VAR>T : Set M<VAR>M' : Submodule R M<VAR>s : Set R<VAR>hs : Ideal.span s = ⊤<VAR>x : M<VAR>s' : Finset R<VAR>hs₁ : ↑s' ⊆ s<VAR>hs₂ : Ideal.span ↑s' = ⊤<VAR>n₁ : { x // x ∈ s' } → ℕ<VAR>n₂ : ∀ (r : { x // x ∈ s' }), ↑r ^ n₁ r • x ∈ M'<VAR>N : ℕ := s'.attach.sup n₁<VAR>hs' : Ideal.span ((fun x => x ^ N) '' ↑s') = ⊤<VAR>r : R<VAR>hr : r ∈ ↑s'<GOAL>↑⟨(fun x => x ^ N) r, ⋯⟩ • x ∈ M'
<VAR>R : Type u<VAR>M : Type v<VAR>M'✝ : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'✝<VAR>inst✝ : Module R M'✝<VAR>I J : Ideal R<VAR>N✝ P : Submodule R M<VAR>S : Set R<VAR>T : Set M<VAR>M' : Submodule R M<VAR>s : Set R<VAR>hs : Ideal.span s = ⊤<VAR>x : M<VAR>s' : Finset R<VAR>hs₁ : ↑s' ⊆ s<VAR>hs₂ : Ideal.span ↑s' = ⊤<VAR>n₁ : { x // x ∈ s' } → ℕ<VAR>n₂ : ∀ (r : { x // x ∈ s' }), ↑r ^ n₁ r • x ∈ M'<VAR>N : ℕ := s'.attach.sup n₁<VAR>hs' : Ideal.span ((fun x => x ^ N) '' ↑s') = ⊤<VAR>r : R<VAR>hr : r ∈ ↑s'<GOAL>↑⟨(fun x => x ^ N) r, ⋯⟩ • x = r ^ (N - n₁ ⟨r, hr⟩) • ↑⟨r, hr⟩ ^ n₁ ⟨r, hr⟩ • x
<VAR>R : Type u<VAR>M : Type v<VAR>M'✝ : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'✝<VAR>inst✝ : Module R M'✝<VAR>I J : Ideal R<VAR>N✝ P : Submodule R M<VAR>S : Set R<VAR>T : Set M<VAR>M' : Submodule R M<VAR>s : Set R<VAR>hs : Ideal.span s = ⊤<VAR>x : M<VAR>s' : Finset R<VAR>hs₁ : ↑s' ⊆ s<VAR>hs₂ : Ideal.span ↑s' = ⊤<VAR>n₁ : { x // x ∈ s' } → ℕ<VAR>n₂ : ∀ (r : { x // x ∈ s' }), ↑r ^ n₁ r • x ∈ M'<VAR>N : ℕ := s'.attach.sup n₁<VAR>hs' : Ideal.span ((fun x => x ^ N) '' ↑s') = ⊤<VAR>r : R<VAR>hr : r ∈ ↑s'<GOAL>r ^ N • x = r ^ (N - n₁ ⟨r, hr⟩ + n₁ ⟨r, hr⟩) • x
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.RightHomologyData<VAR>A : C<VAR>hg : S.g = 0<GOAL>IsIso h.ι
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.RightHomologyData<VAR>A : C<VAR>hg : S.g = 0<VAR>φ : h.Q ⟶ (KernelFork.ofι h.ι ⋯).pt<VAR>hφ : φ ≫ Fork.ι (KernelFork.ofι h.ι ⋯) = 𝟙 h.Q<GOAL>IsIso h.ι
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.RightHomologyData<VAR>A : C<VAR>hg : S.g = 0<VAR>φ : h.Q ⟶ (KernelFork.ofι h.ι ⋯).pt<VAR>hφ : φ ≫ h.ι = 𝟙 h.Q<GOAL>IsIso h.ι
<VAR>s : Finset ℕ<VAR>m n✝ p✝ n p : ℕ<VAR>hn : Squarefree n<GOAL>n.factorization p ≤ 1
<VAR>s : Finset ℕ<VAR>m n p✝ p : ℕ<VAR>hn : Squarefree 0<GOAL>(factorization 0) p ≤ 1
<VAR>s : Finset ℕ<VAR>m n✝ p✝ n p : ℕ<VAR>hn : Squarefree n<VAR>hn' : n ≠ 0<GOAL>n.factorization p ≤ 1
<VAR>s : Finset ℕ<VAR>m n✝ p✝ n p : ℕ<VAR>hn : ∀ (x : ℕ), multiplicity x n ≤ 1 ∨ IsUnit x<VAR>hn' : n ≠ 0<GOAL>n.factorization p ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ✝ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f✝ g✝ s t✝ : ι → α<VAR>a b : α<VAR>γ : Type u_9<VAR>f : β → γ<VAR>g : γ → α<VAR>t : Set β<GOAL>⨆ c ∈ f '' t, g c = ⨆ b ∈ t, g (f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ✝ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f✝ g✝ s t✝ : ι → α<VAR>a b : α<VAR>γ : Type u_9<VAR>f : β → γ<VAR>g : γ → α<VAR>t : Set β<GOAL>sSup (g ∘ f '' t) = sSup ((fun b => g (f b)) '' t)
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁶ : LinearOrder α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : ClosedIicTopology α<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : One α<VAR>f : β → α<VAR>hf : Continuous f<VAR>h : HasCompactMulSupport f<GOAL>∃ x, ∀ (y : β), f x ≤ f y
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁶ : LinearOrder α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : ClosedIicTopology α<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : One α<VAR>f : β → α<VAR>hf : Continuous f<VAR>h : HasCompactMulSupport f<VAR>x : β<VAR>hx : f x ∈ lowerBounds (range f)<GOAL>∃ x, ∀ (y : β), f x ≤ f y
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁶ : LinearOrder α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : ClosedIicTopology α<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : One α<VAR>f : β → α<VAR>hf : Continuous f<VAR>h : HasCompactMulSupport f<VAR>x : β<VAR>hx : ∀ (i : β), f x ≤ f i<GOAL>∃ x, ∀ (y : β), f x ≤ f y
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → G<VAR>hf : f =ᶠ[ae μ] 0<GOAL>∫ (a : α), f a ∂μ = 0
<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>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>n : ℕ<VAR>h : a ∈ closedBall b r<GOAL>a ^ n ∈ closedBall (b ^ n) (n • r)
<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>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>n : ℕ<VAR>h : ‖a / b‖ ≤ r<GOAL>‖(a / b) ^ n‖ ≤ n • r
<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>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>n : ℕ<VAR>h : ‖a / b‖ ≤ r<GOAL>↑n * ‖a / b‖ ≤ n • r
<VAR>α : Type u<VAR>J : Type w<VAR>inst✝³ : SmallCategory J<VAR>inst✝² : FinCategory J<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : OrderBot α<VAR>x y : α<GOAL>colimit (pair x y) = Finset.univ.sup (pair x y).obj
<VAR>α : Type u<VAR>J : Type w<VAR>inst✝³ : SmallCategory J<VAR>inst✝² : FinCategory J<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : OrderBot α<VAR>x y : α<GOAL>x ⊔ (y ⊔ ⊥) = x ⊔ y
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s t : Finset α<VAR>P : Finpartition univ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hP₁ : P.IsEquipartition<VAR>hP₃ : P.parts.card ≤ bound (ε / 8) ⌈4 / ε⌉₊<VAR>ht : t ∈ (regularityReduced P G (ε / 8) (ε / 4)).cliqueFinset 3<GOAL>triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(G.cliqueFinset 3).card
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s t : Finset α<VAR>P : Finpartition univ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hP₁ : P.IsEquipartition<VAR>hP₃ : P.parts.card ≤ bound (ε / 8) ⌈4 / ε⌉₊<VAR>ht : ∃ a b c, (regularityReduced P G (ε / 8) (ε / 4)).Adj a b ∧ (regularityReduced P G (ε / 8) (ε / 4)).Adj a c ∧ (regularityReduced P G (ε / 8) (ε / 4)).Adj b c ∧ t = {a, b, c}<GOAL>triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(G.cliqueFinset 3).card
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s✝ : Finset α<VAR>P : Finpartition univ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hP₁ : P.IsEquipartition<VAR>hP₃ : P.parts.card ≤ bound (ε / 8) ⌈4 / ε⌉₊<VAR>x y z : α<VAR>s : Finset α<VAR>hX : s ∈ P.parts<VAR>Y : Finset α<VAR>hY : Y ∈ P.parts<VAR>xX : x ∈ s<VAR>yY : y ∈ Y<VAR>nXY : s ≠ Y<VAR>uXY : G.IsUniform (ε / 8) s Y<VAR>dXY : ε / 4 ≤ ↑(G.edgeDensity s Y)<VAR>X' : Finset α<VAR>hX' : X' ∈ P.parts<VAR>Z : Finset α<VAR>hZ : Z ∈ P.parts<VAR>xX' : x ∈ X'<VAR>zZ : z ∈ Z<VAR>nXZ : X' ≠ Z<VAR>uXZ : G.IsUniform (ε / 8) X' Z<VAR>dXZ : ε / 4 ≤ ↑(G.edgeDensity X' Z)<VAR>Y' : Finset α<VAR>hY' : Y' ∈ P.parts<VAR>Z' : Finset α<VAR>hZ' : Z' ∈ P.parts<VAR>yY' : y ∈ Y'<VAR>zZ' : z ∈ Z'<VAR>nYZ : Y' ≠ Z'<VAR>uYZ : G.IsUniform (ε / 8) Y' Z'<VAR>dYZ : ε / 4 ≤ ↑(G.edgeDensity Y' Z')<GOAL>triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(G.cliqueFinset 3).card
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s✝ : Finset α<VAR>P : Finpartition univ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hP₁ : P.IsEquipartition<VAR>hP₃ : P.parts.card ≤ bound (ε / 8) ⌈4 / ε⌉₊<VAR>x y z : α<VAR>s : Finset α<VAR>hX : s ∈ P.parts<VAR>Y : Finset α<VAR>hY : Y ∈ P.parts<VAR>xX : x ∈ s<VAR>yY : y ∈ Y<VAR>nXY : s ≠ Y<VAR>uXY : G.IsUniform (ε / 8) s Y<VAR>dXY : ε / 4 ≤ ↑(G.edgeDensity s Y)<VAR>Z : Finset α<VAR>hZ : Z ∈ P.parts<VAR>zZ : z ∈ Z<VAR>Y' : Finset α<VAR>hY' : Y' ∈ P.parts<VAR>Z' : Finset α<VAR>hZ' : Z' ∈ P.parts<VAR>yY' : y ∈ Y'<VAR>zZ' : z ∈ Z'<VAR>nYZ : Y' ≠ Z'<VAR>uYZ : G.IsUniform (ε / 8) Y' Z'<VAR>dYZ : ε / 4 ≤ ↑(G.edgeDensity Y' Z')<VAR>hX' : s ∈ P.parts<VAR>xX' : x ∈ s<VAR>nXZ : s ≠ Z<VAR>uXZ : G.IsUniform (ε / 8) s Z<VAR>dXZ : ε / 4 ≤ ↑(G.edgeDensity s Z)<GOAL>triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(G.cliqueFinset 3).card
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s✝ : Finset α<VAR>P : Finpartition univ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hP₁ : P.IsEquipartition<VAR>hP₃ : P.parts.card ≤ bound (ε / 8) ⌈4 / ε⌉₊<VAR>x y z : α<VAR>s : Finset α<VAR>hX : s ∈ P.parts<VAR>Y : Finset α<VAR>hY : Y ∈ P.parts<VAR>xX : x ∈ s<VAR>yY : y ∈ Y<VAR>nXY : s ≠ Y<VAR>uXY : G.IsUniform (ε / 8) s Y<VAR>dXY : ε / 4 ≤ ↑(G.edgeDensity s Y)<VAR>Z : Finset α<VAR>hZ : Z ∈ P.parts<VAR>zZ : z ∈ Z<VAR>Z' : Finset α<VAR>hZ' : Z' ∈ P.parts<VAR>zZ' : z ∈ Z'<VAR>hX' : s ∈ P.parts<VAR>xX' : x ∈ s<VAR>nXZ : s ≠ Z<VAR>uXZ : G.IsUniform (ε / 8) s Z<VAR>dXZ : ε / 4 ≤ ↑(G.edgeDensity s Z)<VAR>hY' : Y ∈ P.parts<VAR>yY' : y ∈ Y<VAR>nYZ : Y ≠ Z'<VAR>uYZ : G.IsUniform (ε / 8) Y Z'<VAR>dYZ : ε / 4 ≤ ↑(G.edgeDensity Y Z')<GOAL>triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(G.cliqueFinset 3).card
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s✝ : Finset α<VAR>P : Finpartition univ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hP₁ : P.IsEquipartition<VAR>hP₃ : P.parts.card ≤ bound (ε / 8) ⌈4 / ε⌉₊<VAR>x y z : α<VAR>s : Finset α<VAR>hX : s ∈ P.parts<VAR>Y : Finset α<VAR>hY : Y ∈ P.parts<VAR>xX : x ∈ s<VAR>yY : y ∈ Y<VAR>nXY : s ≠ Y<VAR>uXY : G.IsUniform (ε / 8) s Y<VAR>dXY : ε / 4 ≤ ↑(G.edgeDensity s Y)<VAR>Z : Finset α<VAR>hZ : Z ∈ P.parts<VAR>zZ : z ∈ Z<VAR>hX' : s ∈ P.parts<VAR>xX' : x ∈ s<VAR>nXZ : s ≠ Z<VAR>uXZ : G.IsUniform (ε / 8) s Z<VAR>dXZ : ε / 4 ≤ ↑(G.edgeDensity s Z)<VAR>hY' : Y ∈ P.parts<VAR>yY' : y ∈ Y<VAR>hZ' : Z ∈ P.parts<VAR>zZ' : z ∈ Z<VAR>nYZ : Y ≠ Z<VAR>uYZ : G.IsUniform (ε / 8) Y Z<VAR>dYZ : ε / 4 ≤ ↑(G.edgeDensity Y Z)<GOAL>triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 ≤ ↑(G.cliqueFinset 3).card