ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x✝ : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝¹ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>inst✝ : TopologicalSpace α<VAR>f : α →ᵤ[𝔖] β<VAR>x : α<VAR>hc : ContinuousAt ((toFun 𝔖) f) x<VAR>U : Set (β × β)<VAR>hU : U ∈ 𝓤 β<VAR>V : Set α<VAR>hV : V ∈ 𝔖<VAR>hVx : V ∈ 𝓝 x<GOAL>∀ᶠ (a : (α →ᵤ[𝔖] β) × α) in 𝓝 (f, x), (Prod.mk ((toFun 𝔖) (f, x).1 (f, x).2) ∘ fun fx => (toFun 𝔖) fx.1 fx.2) a ∈ U ○ U
<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>f : β × γ → α<VAR>s : Set β<VAR>t : Set γ<GOAL>⨆ x ∈ s ×ˢ t, f x = ⨆ a ∈ s, ⨆ b ∈ t, f (a, 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>f : β × γ → α<VAR>s : Set β<VAR>t : Set γ<GOAL>⨆ i, ⨆ j, ⨆ (_ : i ∈ s), ⨆ (_ : j ∈ t), f (i, j) = ⨆ a ∈ s, ⨆ b ∈ t, f (a, b)
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : MulAction G X<VAR>inst✝⁵ : MulAction G Y<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>h_proper : ProperSMul G X<VAR>inst✝ : T2Space G<VAR>f : X → G × X := fun x => (1, x)<VAR>proper_f : IsProperMap f<GOAL>T2Space X
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : MulAction G X<VAR>inst✝⁵ : MulAction G Y<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>h_proper : ProperSMul G X<VAR>inst✝ : T2Space G<VAR>f : X → G × X := fun x => (1, x)<VAR>proper_f : IsProperMap f<GOAL>IsClosed (diagonal X)
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : MulAction G X<VAR>inst✝⁵ : MulAction G Y<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>h_proper : ProperSMul G X<VAR>inst✝ : T2Space G<VAR>f : X → G × X := fun x => (1, x)<VAR>proper_f : IsProperMap f<VAR>g : G × X → X × X := fun gx => (gx.1 • gx.2, gx.2)<GOAL>IsClosed (diagonal X)
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : MulAction G X<VAR>inst✝⁵ : MulAction G Y<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>h_proper : ProperSMul G X<VAR>inst✝ : T2Space G<VAR>f : X → G × X := fun x => (1, x)<VAR>proper_f : IsProperMap f<VAR>g : G × X → X × X := fun gx => (gx.1 • gx.2, gx.2)<VAR>proper_g : IsProperMap g<GOAL>IsClosed (diagonal X)
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : MulAction G X<VAR>inst✝⁵ : MulAction G Y<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>h_proper : ProperSMul G X<VAR>inst✝ : T2Space G<VAR>f : X → G × X := fun x => (1, x)<VAR>proper_f : IsProperMap f<VAR>g : G × X → X × X := fun gx => (gx.1 • gx.2, gx.2)<VAR>proper_g : IsProperMap g<VAR>this : g ∘ f = fun x => (x, x)<VAR>range_gf : range (g ∘ f) = diagonal X<GOAL>IsClosed (range (g ∘ f))
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>n✝ : ℕ<GOAL>(divX 1).coeff n✝ = coeff 0 n✝
<VAR>R : Type u_1<VAR>inst✝³ : Ring R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddCommGroup X<VAR>inst✝ : Module R X<VAR>n : ℤ<VAR>x : OreLocalization S X<VAR>inst : Module ℤ (OreLocalization S X) := instModuleOfIsScalarTower<GOAL>n • x = n • x
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>W X Y Z X₁ X₂ X₃ Z₁ Z₂ : C<VAR>g₁ : Z₁ ⟶ X₁<VAR>g₂ : Z₁ ⟶ X₂<VAR>g₃ : Z₂ ⟶ X₂<VAR>g₄ : Z₂ ⟶ X₃<VAR>inst✝³ : HasPushout g₁ g₂<VAR>inst✝² : HasPushout g₃ g₄<VAR>inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄<VAR>inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)<GOAL>pushout.inl g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄ ≫ (pushoutAssoc g₁ g₂ g₃ g₄).hom = pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄)
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>W X Y Z X₁ X₂ X₃ Z₁ Z₂ : C<VAR>g₁ : Z₁ ⟶ X₁<VAR>g₂ : Z₁ ⟶ X₂<VAR>g₃ : Z₂ ⟶ X₂<VAR>g₄ : Z₂ ⟶ X₃<VAR>inst✝³ : HasPushout g₁ g₂<VAR>inst✝² : HasPushout g₃ g₄<VAR>inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄<VAR>inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)<GOAL>pushout.inl g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄ ≫ (pushoutAssoc g₁ g₂ g₃ g₄).hom = pushout.inl g₁ g₂ ≫ pushout.desc (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄)) (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>W X Y Z X₁ X₂ X₃ Z₁ Z₂ : C<VAR>g₁ : Z₁ ⟶ X₁<VAR>g₂ : Z₁ ⟶ X₂<VAR>g₃ : Z₂ ⟶ X₂<VAR>g₄ : Z₂ ⟶ X₃<VAR>inst✝³ : HasPushout g₁ g₂<VAR>inst✝² : HasPushout g₃ g₄<VAR>inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄<VAR>inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)<GOAL>pushout.inl g₁ g₂ ≫ pushout.desc (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄)) (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯ = pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄)
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type u<VAR>inst✝¹ : CommRing S<VAR>P : Type u<VAR>inst✝ : CommRing P<VAR>f : R →+* S<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>V : Opens ↑(PrimeSpectrum.Top S)<VAR>hUV : V.carrier ⊆ ⇑(PrimeSpectrum.comap f) ⁻¹' U.carrier<VAR>s : (x : ↥U) → Localizations R ↑x<VAR>hs : (isLocallyFraction R).pred s<VAR>p : ↑(PrimeSpectrum.Top S)<VAR>hpV : p ∈ V<VAR>W : Opens ↑(PrimeSpectrum.Top R)<VAR>m : ↑⟨(PrimeSpectrum.comap f) p, ⋯⟩ ∈ W<VAR>iWU : W ⟶ U<VAR>a b : R<VAR>q : ↑(PrimeSpectrum.Top S)<VAR>hqW : q ∈ ↑((Opens.comap (PrimeSpectrum.comap f)) W)<VAR>hqV : q ∈ ↑V<VAR>h_frac : b ∉ (↑⟨(PrimeSpectrum.comap f) q, hqW⟩).asIdeal ∧ (fun x => s ((fun x => ⟨↑x, ⋯⟩) x)) ⟨(PrimeSpectrum.comap f) q, hqW⟩ * (algebraMap R (Localizations R ↑⟨(PrimeSpectrum.comap f) q, hqW⟩)) b = (algebraMap R (Localizations R ↑⟨(PrimeSpectrum.comap f) q, hqW⟩)) a<GOAL>f b ∉ (↑⟨q, ⋯⟩).asIdeal ∧ (fun x => comapFun f U V hUV s ((fun x => ⟨↑x, ⋯⟩) x)) ⟨q, ⋯⟩ * (algebraMap S (Localizations S ↑⟨q, ⋯⟩)) (f b) = (algebraMap S (Localizations S ↑⟨q, ⋯⟩)) (f a)
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type u<VAR>inst✝¹ : CommRing S<VAR>P : Type u<VAR>inst✝ : CommRing P<VAR>f : R →+* S<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>V : Opens ↑(PrimeSpectrum.Top S)<VAR>hUV : V.carrier ⊆ ⇑(PrimeSpectrum.comap f) ⁻¹' U.carrier<VAR>s : (x : ↥U) → Localizations R ↑x<VAR>hs : (isLocallyFraction R).pred s<VAR>p : ↑(PrimeSpectrum.Top S)<VAR>hpV : p ∈ V<VAR>W : Opens ↑(PrimeSpectrum.Top R)<VAR>m : ↑⟨(PrimeSpectrum.comap f) p, ⋯⟩ ∈ W<VAR>iWU : W ⟶ U<VAR>a b : R<VAR>q : ↑(PrimeSpectrum.Top S)<VAR>hqW : q ∈ ↑((Opens.comap (PrimeSpectrum.comap f)) W)<VAR>hqV : q ∈ ↑V<VAR>h_frac : b ∉ (↑⟨(PrimeSpectrum.comap f) q, hqW⟩).asIdeal ∧ (fun x => s ((fun x => ⟨↑x, ⋯⟩) x)) ⟨(PrimeSpectrum.comap f) q, hqW⟩ * (algebraMap R (Localizations R ↑⟨(PrimeSpectrum.comap f) q, hqW⟩)) b = (algebraMap R (Localizations R ↑⟨(PrimeSpectrum.comap f) q, hqW⟩)) a<GOAL>(fun x => comapFun f U V hUV s ((fun x => ⟨↑x, ⋯⟩) x)) ⟨q, ⋯⟩ * (algebraMap S (Localizations S ↑⟨q, ⋯⟩)) (f b) = (algebraMap S (Localizations S ↑⟨q, ⋯⟩)) (f a)
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type u<VAR>inst✝¹ : CommRing S<VAR>P : Type u<VAR>inst✝ : CommRing P<VAR>f : R →+* S<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>V : Opens ↑(PrimeSpectrum.Top S)<VAR>hUV : V.carrier ⊆ ⇑(PrimeSpectrum.comap f) ⁻¹' U.carrier<VAR>s : (x : ↥U) → Localizations R ↑x<VAR>hs : (isLocallyFraction R).pred s<VAR>p : ↑(PrimeSpectrum.Top S)<VAR>hpV : p ∈ V<VAR>W : Opens ↑(PrimeSpectrum.Top R)<VAR>m : ↑⟨(PrimeSpectrum.comap f) p, ⋯⟩ ∈ W<VAR>iWU : W ⟶ U<VAR>a b : R<VAR>q : ↑(PrimeSpectrum.Top S)<VAR>hqW : q ∈ ↑((Opens.comap (PrimeSpectrum.comap f)) W)<VAR>hqV : q ∈ ↑V<VAR>h_frac : b ∉ (↑⟨(PrimeSpectrum.comap f) q, hqW⟩).asIdeal ∧ (fun x => s ((fun x => ⟨↑x, ⋯⟩) x)) ⟨(PrimeSpectrum.comap f) q, hqW⟩ * (algebraMap R (Localizations R ↑⟨(PrimeSpectrum.comap f) q, hqW⟩)) b = (algebraMap R (Localizations R ↑⟨(PrimeSpectrum.comap f) q, hqW⟩)) a<GOAL>(Localization.localRingHom ((PrimeSpectrum.comap f) q).asIdeal q.asIdeal f ⋯) (s ⟨(PrimeSpectrum.comap f) q, ⋯⟩) * (algebraMap S (Localizations S q)) (f b) = (algebraMap S (Localizations S q)) (f a)
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type u<VAR>inst✝¹ : CommRing S<VAR>P : Type u<VAR>inst✝ : CommRing P<VAR>f : R →+* S<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>V : Opens ↑(PrimeSpectrum.Top S)<VAR>hUV : V.carrier ⊆ ⇑(PrimeSpectrum.comap f) ⁻¹' U.carrier<VAR>s : (x : ↥U) → Localizations R ↑x<VAR>hs : (isLocallyFraction R).pred s<VAR>p : ↑(PrimeSpectrum.Top S)<VAR>hpV : p ∈ V<VAR>W : Opens ↑(PrimeSpectrum.Top R)<VAR>m : ↑⟨(PrimeSpectrum.comap f) p, ⋯⟩ ∈ W<VAR>iWU : W ⟶ U<VAR>a b : R<VAR>q : ↑(PrimeSpectrum.Top S)<VAR>hqW : q ∈ ↑((Opens.comap (PrimeSpectrum.comap f)) W)<VAR>hqV : q ∈ ↑V<VAR>h_frac : b ∉ (↑⟨(PrimeSpectrum.comap f) q, hqW⟩).asIdeal ∧ (fun x => s ((fun x => ⟨↑x, ⋯⟩) x)) ⟨(PrimeSpectrum.comap f) q, hqW⟩ * (algebraMap R (Localizations R ↑⟨(PrimeSpectrum.comap f) q, hqW⟩)) b = (algebraMap R (Localizations R ↑⟨(PrimeSpectrum.comap f) q, hqW⟩)) a<GOAL>(algebraMap S (Localization.AtPrime q.asIdeal)) (f a) = (algebraMap S (Localizations S q)) (f a)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<VAR>h : c ⊔ a ≤ c ⊔ b<GOAL>a \ c ≤ b \ c
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<VAR>h : c ⊔ a ≤ c ⊔ b<GOAL>(c ⊔ a) \ c ≤ (c ⊔ b) \ c
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Field L'<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra K L'<VAR>S : IntermediateField K L<VAR>F E✝ E'✝ : Subfield L<VAR>h : F ≤ E✝<VAR>h' : F ≤ E'✝<VAR>x : L<VAR>E E' : { E // F ≤ E }<GOAL>{ toFun := fun E => extendScalars ⋯, invFun := fun E => ⟨E.toSubfield, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } E ≤ { toFun := fun E => extendScalars ⋯, invFun := fun E => ⟨E.toSubfield, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } E' ↔ E ≤ E'
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Field L'<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra K L'<VAR>S : IntermediateField K L<VAR>F E✝ E'✝ : Subfield L<VAR>h : F ≤ E✝<VAR>h' : F ≤ E'✝<VAR>x : L<VAR>E E' : { E // F ≤ E }<GOAL>extendScalars ⋯ ≤ extendScalars ⋯ ↔ E ≤ E'
<VAR>α : Type u_1<VAR>m : Set (OuterMeasure α)<GOAL>sInf m = boundedBy (sInfGen m)
<VAR>α : Type u_1<VAR>m : Set (OuterMeasure α)<GOAL>sInf m ≤ boundedBy (sInfGen m)
<VAR>α : Type u_1<VAR>m : Set (OuterMeasure α)<GOAL>boundedBy (sInfGen m) ≤ sInf m
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>inst✝⁵ : MeasurableSpace E<VAR>inst✝⁴ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f✝ g : E → ℝ<VAR>s : Set E<VAR>μ : Measure E<VAR>inst✝¹ : μ.IsAddHaarMeasure<VAR>inst✝ : FiniteDimensional ℝ F<VAR>f : E → F<VAR>hf : LipschitzOnWith C f s<VAR>hs : MeasurableSet s<GOAL>∀ᵐ (x : E) ∂μ.restrict s, DifferentiableWithinAt ℝ f s x
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>inst✝⁵ : MeasurableSpace E<VAR>inst✝⁴ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f✝ g : E → ℝ<VAR>s : Set E<VAR>μ : Measure E<VAR>inst✝¹ : μ.IsAddHaarMeasure<VAR>inst✝ : FiniteDimensional ℝ F<VAR>f : E → F<VAR>hf : LipschitzOnWith C f s<VAR>hs : MeasurableSet s<GOAL>∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x
<VAR>f✝ : Ordinal.{u} → Ordinal.{u}<VAR>f : Ordinal.{u_1} → Ordinal.{u_1}<VAR>H : IsNormal f<VAR>a b : Ordinal.{u_1}<GOAL>f b < nfpFamily (fun x => f) a ↔ b < nfpFamily (fun x => f) a
<VAR>f✝ : Ordinal.{u} → Ordinal.{u}<VAR>f : Ordinal.{u_1} → Ordinal.{u_1}<VAR>H : IsNormal f<VAR>a b : Ordinal.{u_1}<GOAL>f b < nfpFamily (fun x => f) a ↔ Unit → f b < nfpFamily (fun x => f) a
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>inst✝¹ : Nonempty ↥s<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>p : P<GOAL>↑s ∩ ↑(mk' p s.directionᗮ) = {↑((orthogonalProjection s) p)}
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>inst✝¹ : Nonempty ↥s<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>p : P<GOAL>↑s ∩ ↑(mk' p s.directionᗮ) = {orthogonalProjectionFn s p}
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>Z : C<VAR>π : Y ⟶ Z<VAR>q : IsSplitCoequalizer f g π<VAR>F : C ⥤ D<GOAL>F.map f ≫ F.map π = F.map g ≫ F.map π
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>Z : C<VAR>π : Y ⟶ Z<VAR>q : IsSplitCoequalizer f g π<VAR>F : C ⥤ D<GOAL>F.map q.rightSection ≫ F.map π = 𝟙 (F.obj Z)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>Z : C<VAR>π : Y ⟶ Z<VAR>q : IsSplitCoequalizer f g π<VAR>F : C ⥤ D<GOAL>F.map q.leftSection ≫ F.map g = 𝟙 (F.obj Y)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>Z : C<VAR>π : Y ⟶ Z<VAR>q : IsSplitCoequalizer f g π<VAR>F : C ⥤ D<GOAL>F.map q.leftSection ≫ F.map f = F.map π ≫ F.map q.rightSection
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)<VAR>i j : ℕ<VAR>ih : i ≤ j → approx (⇑f) i ≤ approx (⇑f) j<VAR>a✝ : i.le j<GOAL>approx (⇑f) i ≤ approx (⇑f) (j + 1)
<VAR>θ : Angle<GOAL>toIocMod two_pi_pos (-π) θ.toReal = θ.toReal
<VAR>x✝ : ℝ<GOAL>toIocMod two_pi_pos (-π) (↑x✝).toReal = (↑x✝).toReal
<VAR>x✝ : ℝ<GOAL>toIocMod two_pi_pos (-π) (toIocMod two_pi_pos (-π) x✝) = toIocMod two_pi_pos (-π) x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>ι : Type u_4<VAR>inst✝¹ : Preorder ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>f g : ι → ℝ≥0∞<VAR>hf : Monotone f<VAR>hg : Monotone g<VAR>i j _k : ι<VAR>x✝ : i ≤ _k ∧ j ≤ _k<VAR>hi : i ≤ _k<VAR>hj : j ≤ _k<GOAL>f i + g j ≤ f _k + g _k
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j✝ k : J<VAR>s : Set (F.obj i)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>hFn : ∀ (j : J), Nonempty (F.obj j)<VAR>Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)<VAR>hs : s.Nonempty<VAR>j : J<GOAL>Nonempty ((F.toPreimages s).obj j)
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j✝ k : J<VAR>s : Set (F.obj i)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>hFn : ∀ (j : J), Nonempty (F.obj j)<VAR>Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)<VAR>hs : s.Nonempty<VAR>j : J<GOAL>∃ x, ∀ (i_1 : j ⟶ i), F.map i_1 x ∈ s
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j✝ k : J<VAR>s : Set (F.obj i)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>hFn : ∀ (j : J), Nonempty (F.obj j)<VAR>Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)<VAR>hs : s.Nonempty<VAR>j : J<VAR>h : IsEmpty (j ⟶ i)<GOAL>∃ x, ∀ (i_1 : j ⟶ i), F.map i_1 x ∈ s
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j✝ k : J<VAR>s : Set (F.obj i)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>hFn : ∀ (j : J), Nonempty (F.obj j)<VAR>Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)<VAR>hs : s.Nonempty<VAR>j : J<VAR>ji : j ⟶ i<GOAL>∃ x, ∀ (i_1 : j ⟶ i), F.map i_1 x ∈ s
<VAR>F : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>D : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁹ : Monoid A<VAR>inst✝¹⁸ : Monoid B<VAR>inst✝¹⁷ : Monoid C<VAR>inst✝¹⁶ : Monoid D<VAR>inst✝¹⁵ : CommGroup E<VAR>inst✝¹⁴ : TopologicalSpace A<VAR>inst✝¹³ : TopologicalSpace B<VAR>inst✝¹² : TopologicalSpace C<VAR>inst✝¹¹ : TopologicalSpace D<VAR>inst✝¹⁰ : TopologicalSpace E<VAR>inst✝⁹ : TopologicalGroup E<VAR>X : Type u_7<VAR>Y : Type u_8<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Group X<VAR>inst✝⁶ : TopologicalGroup X<VAR>inst✝⁵ : UniformSpace Y<VAR>inst✝⁴ : CommGroup Y<VAR>inst✝³ : UniformGroup Y<VAR>inst✝² : T0Space Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : LocallyCompactSpace X<VAR>V : ℕ → Set Y<VAR>hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)<VAR>hVo : (nhds 1).HasBasis (fun x => True) V<GOAL>LocallyCompactSpace (ContinuousMonoidHom X Y)
<VAR>F : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>D : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁹ : Monoid A<VAR>inst✝¹⁸ : Monoid B<VAR>inst✝¹⁷ : Monoid C<VAR>inst✝¹⁶ : Monoid D<VAR>inst✝¹⁵ : CommGroup E<VAR>inst✝¹⁴ : TopologicalSpace A<VAR>inst✝¹³ : TopologicalSpace B<VAR>inst✝¹² : TopologicalSpace C<VAR>inst✝¹¹ : TopologicalSpace D<VAR>inst✝¹⁰ : TopologicalSpace E<VAR>inst✝⁹ : TopologicalGroup E<VAR>X : Type u_7<VAR>Y : Type u_8<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Group X<VAR>inst✝⁶ : TopologicalGroup X<VAR>inst✝⁵ : UniformSpace Y<VAR>inst✝⁴ : CommGroup Y<VAR>inst✝³ : UniformGroup Y<VAR>inst✝² : T0Space Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : LocallyCompactSpace X<VAR>V : ℕ → Set Y<VAR>hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)<VAR>hVo : (nhds 1).HasBasis (fun x => True) V<VAR>U0 : Set X<VAR>hU0c : IsCompact U0<VAR>hU0o : U0 ∈ nhds 1<GOAL>LocallyCompactSpace (ContinuousMonoidHom X Y)
<VAR>F : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>D : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁹ : Monoid A<VAR>inst✝¹⁸ : Monoid B<VAR>inst✝¹⁷ : Monoid C<VAR>inst✝¹⁶ : Monoid D<VAR>inst✝¹⁵ : CommGroup E<VAR>inst✝¹⁴ : TopologicalSpace A<VAR>inst✝¹³ : TopologicalSpace B<VAR>inst✝¹² : TopologicalSpace C<VAR>inst✝¹¹ : TopologicalSpace D<VAR>inst✝¹⁰ : TopologicalSpace E<VAR>inst✝⁹ : TopologicalGroup E<VAR>X : Type u_7<VAR>Y : Type u_8<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Group X<VAR>inst✝⁶ : TopologicalGroup X<VAR>inst✝⁵ : UniformSpace Y<VAR>inst✝⁴ : CommGroup Y<VAR>inst✝³ : UniformGroup Y<VAR>inst✝² : T0Space Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : LocallyCompactSpace X<VAR>V : ℕ → Set Y<VAR>hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)<VAR>hVo : (nhds 1).HasBasis (fun x => True) V<VAR>U0 : Set X<VAR>hU0c : IsCompact U0<VAR>hU0o : U0 ∈ nhds 1<VAR>U_aux : ℕ → ↑{S | S ∈ nhds 1} := fun t => Nat.rec ⟨U0, hU0o⟩ (fun x S => let h := ⋯; ⟨Classical.choose h, ⋯⟩) t<GOAL>LocallyCompactSpace (ContinuousMonoidHom X Y)
<VAR>F : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>D : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁹ : Monoid A<VAR>inst✝¹⁸ : Monoid B<VAR>inst✝¹⁷ : Monoid C<VAR>inst✝¹⁶ : Monoid D<VAR>inst✝¹⁵ : CommGroup E<VAR>inst✝¹⁴ : TopologicalSpace A<VAR>inst✝¹³ : TopologicalSpace B<VAR>inst✝¹² : TopologicalSpace C<VAR>inst✝¹¹ : TopologicalSpace D<VAR>inst✝¹⁰ : TopologicalSpace E<VAR>inst✝⁹ : TopologicalGroup E<VAR>X : Type u_7<VAR>Y : Type u_8<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Group X<VAR>inst✝⁶ : TopologicalGroup X<VAR>inst✝⁵ : UniformSpace Y<VAR>inst✝⁴ : CommGroup Y<VAR>inst✝³ : UniformGroup Y<VAR>inst✝² : T0Space Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : LocallyCompactSpace X<VAR>V : ℕ → Set Y<VAR>hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)<VAR>hVo : (nhds 1).HasBasis (fun x => True) V<VAR>U0 : Set X<VAR>hU0c : IsCompact U0<VAR>hU0o : U0 ∈ nhds 1<VAR>U_aux : ℕ → ↑{S | S ∈ nhds 1} := fun t => Nat.rec ⟨U0, hU0o⟩ (fun x S => let h := ⋯; ⟨Classical.choose h, ⋯⟩) t<VAR>U : ℕ → Set X := fun n => ↑(U_aux n)<GOAL>LocallyCompactSpace (ContinuousMonoidHom X Y)
<VAR>F : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>D : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁹ : Monoid A<VAR>inst✝¹⁸ : Monoid B<VAR>inst✝¹⁷ : Monoid C<VAR>inst✝¹⁶ : Monoid D<VAR>inst✝¹⁵ : CommGroup E<VAR>inst✝¹⁴ : TopologicalSpace A<VAR>inst✝¹³ : TopologicalSpace B<VAR>inst✝¹² : TopologicalSpace C<VAR>inst✝¹¹ : TopologicalSpace D<VAR>inst✝¹⁰ : TopologicalSpace E<VAR>inst✝⁹ : TopologicalGroup E<VAR>X : Type u_7<VAR>Y : Type u_8<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Group X<VAR>inst✝⁶ : TopologicalGroup X<VAR>inst✝⁵ : UniformSpace Y<VAR>inst✝⁴ : CommGroup Y<VAR>inst✝³ : UniformGroup Y<VAR>inst✝² : T0Space Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : LocallyCompactSpace X<VAR>V : ℕ → Set Y<VAR>hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)<VAR>hVo : (nhds 1).HasBasis (fun x => True) V<VAR>U0 : Set X<VAR>hU0c : IsCompact U0<VAR>hU0o : U0 ∈ nhds 1<VAR>U_aux : ℕ → ↑{S | S ∈ nhds 1} := fun t => Nat.rec ⟨U0, hU0o⟩ (fun x S => let h := ⋯; ⟨Classical.choose h, ⋯⟩) t<VAR>U : ℕ → Set X := fun n => ↑(U_aux n)<VAR>hU1 : ∀ (n : ℕ), U n ∈ nhds 1<GOAL>LocallyCompactSpace (ContinuousMonoidHom X Y)
<VAR>F : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>D : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁹ : Monoid A<VAR>inst✝¹⁸ : Monoid B<VAR>inst✝¹⁷ : Monoid C<VAR>inst✝¹⁶ : Monoid D<VAR>inst✝¹⁵ : CommGroup E<VAR>inst✝¹⁴ : TopologicalSpace A<VAR>inst✝¹³ : TopologicalSpace B<VAR>inst✝¹² : TopologicalSpace C<VAR>inst✝¹¹ : TopologicalSpace D<VAR>inst✝¹⁰ : TopologicalSpace E<VAR>inst✝⁹ : TopologicalGroup E<VAR>X : Type u_7<VAR>Y : Type u_8<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Group X<VAR>inst✝⁶ : TopologicalGroup X<VAR>inst✝⁵ : UniformSpace Y<VAR>inst✝⁴ : CommGroup Y<VAR>inst✝³ : UniformGroup Y<VAR>inst✝² : T0Space Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : LocallyCompactSpace X<VAR>V : ℕ → Set Y<VAR>hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)<VAR>hVo : (nhds 1).HasBasis (fun x => True) V<VAR>U0 : Set X<VAR>hU0c : IsCompact U0<VAR>hU0o : U0 ∈ nhds 1<VAR>U_aux : ℕ → ↑{S | S ∈ nhds 1} := fun t => Nat.rec ⟨U0, hU0o⟩ (fun x S => let h := ⋯; ⟨Classical.choose h, ⋯⟩) t<VAR>U : ℕ → Set X := fun n => ↑(U_aux n)<VAR>hU1 : ∀ (n : ℕ), U n ∈ nhds 1<VAR>hU2 : ∀ (n : ℕ), U (n + 1) * U (n + 1) ⊆ U n<GOAL>LocallyCompactSpace (ContinuousMonoidHom X Y)
<VAR>F : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>D : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁹ : Monoid A<VAR>inst✝¹⁸ : Monoid B<VAR>inst✝¹⁷ : Monoid C<VAR>inst✝¹⁶ : Monoid D<VAR>inst✝¹⁵ : CommGroup E<VAR>inst✝¹⁴ : TopologicalSpace A<VAR>inst✝¹³ : TopologicalSpace B<VAR>inst✝¹² : TopologicalSpace C<VAR>inst✝¹¹ : TopologicalSpace D<VAR>inst✝¹⁰ : TopologicalSpace E<VAR>inst✝⁹ : TopologicalGroup E<VAR>X : Type u_7<VAR>Y : Type u_8<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Group X<VAR>inst✝⁶ : TopologicalGroup X<VAR>inst✝⁵ : UniformSpace Y<VAR>inst✝⁴ : CommGroup Y<VAR>inst✝³ : UniformGroup Y<VAR>inst✝² : T0Space Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : LocallyCompactSpace X<VAR>V : ℕ → Set Y<VAR>hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)<VAR>hVo : (nhds 1).HasBasis (fun x => True) V<VAR>U0 : Set X<VAR>hU0c : IsCompact U0<VAR>hU0o : U0 ∈ nhds 1<VAR>U_aux : ℕ → ↑{S | S ∈ nhds 1} := fun t => Nat.rec ⟨U0, hU0o⟩ (fun x S => let h := ⋯; ⟨Classical.choose h, ⋯⟩) t<VAR>U : ℕ → Set X := fun n => ↑(U_aux n)<VAR>hU1 : ∀ (n : ℕ), U n ∈ nhds 1<VAR>hU2 : ∀ (n : ℕ), U (n + 1) * U (n + 1) ⊆ U n<VAR>hU3 : ∀ (n : ℕ), U (n + 1) ⊆ U n<GOAL>LocallyCompactSpace (ContinuousMonoidHom X Y)