ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>C : ℝ<VAR>hf'_gt : ∀ x ∈ interior D, C < deriv f x<VAR>x : ℝ<GOAL>x ∈ D → ∀ y ∈ D, x < y → C * (y - x) < f y - f x
<VAR>f : ℝ → ℝ<VAR>hf : Differentiable ℝ f<VAR>C : ℝ<VAR>hf'_gt : ∀ (x : ℝ), C < deriv f x<VAR>x y : ℝ<VAR>hxy : x < y<GOAL>C * (y - x) < f y - f x
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>C : ℝ<VAR>hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x<VAR>x : ℝ<GOAL>x ∈ D → ∀ y ∈ D, x ≤ y → C * (y - x) ≤ f y - f x
<VAR>f : ℝ → ℝ<VAR>hf : Differentiable ℝ f<VAR>C : ℝ<VAR>hf'_ge : ∀ (x : ℝ), C ≤ deriv f x<VAR>x y : ℝ<VAR>hxy : x ≤ y<GOAL>C * (y - x) ≤ f y - f x
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>C : ℝ<VAR>lt_hf' : ∀ x ∈ interior D, deriv f x < C<VAR>x : ℝ<VAR>hx : x ∈ D<VAR>y : ℝ<VAR>hy : y ∈ D<VAR>hxy : x < y<GOAL>f y - f x < C * (y - x)
<VAR>f : ℝ → ℝ<VAR>hf : Differentiable ℝ f<VAR>C : ℝ<VAR>lt_hf' : ∀ (x : ℝ), deriv f x < C<VAR>x y : ℝ<VAR>hxy : x < y<GOAL>f y - f x < C * (y - x)
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>C : ℝ<VAR>le_hf' : ∀ x ∈ interior D, deriv f x ≤ C<VAR>x : ℝ<VAR>hx : x ∈ D<VAR>y : ℝ<VAR>hy : y ∈ D<VAR>hxy : x ≤ y<GOAL>f y - f x ≤ C * (y - x)
<VAR>f : ℝ → ℝ<VAR>hf : Differentiable ℝ f<VAR>C : ℝ<VAR>le_hf' : ∀ (x : ℝ), deriv f x ≤ C<VAR>x y : ℝ<VAR>hxy : x ≤ y<GOAL>f y - f x ≤ C * (y - x)
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : ∀ x ∈ interior D, 0 < deriv f x<GOAL>StrictMonoOn f D
<VAR>f : ℝ → ℝ<VAR>hf' : ∀ (x : ℝ), 0 < deriv f x<GOAL>StrictMono f
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f f' : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x<VAR>hf'₀ : ∀ x ∈ interior D, 0 < f' x<GOAL>StrictMonoOn f D
<VAR>f f' : ℝ → ℝ<VAR>hf : ∀ (x : ℝ), HasDerivAt f (f' x) x<VAR>hf' : ∀ (x : ℝ), 0 < f' x<GOAL>StrictMono f
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>hf'_nonneg : ∀ x ∈ interior D, 0 ≤ deriv f x<GOAL>MonotoneOn f D
<VAR>f : ℝ → ℝ<VAR>hf : Differentiable ℝ f<VAR>hf' : ∀ (x : ℝ), 0 ≤ deriv f x<GOAL>Monotone f
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f f' : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x<VAR>hf'₀ : ∀ x ∈ interior D, 0 ≤ f' x<GOAL>MonotoneOn f D
<VAR>f f' : ℝ → ℝ<VAR>hf : ∀ (x : ℝ), HasDerivAt f (f' x) x<VAR>hf' : 0 ≤ f'<GOAL>Monotone f
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : ∀ x ∈ interior D, deriv f x < 0<GOAL>StrictAntiOn f D
<VAR>f : ℝ → ℝ<VAR>hf' : ∀ (x : ℝ), deriv f x < 0<GOAL>StrictAnti f
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f f' : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x<VAR>hf'₀ : ∀ x ∈ interior D, f' x < 0<GOAL>StrictAntiOn f D
<VAR>f f' : ℝ → ℝ<VAR>hf : ∀ (x : ℝ), HasDerivAt f (f' x) x<VAR>hf' : ∀ (x : ℝ), f' x < 0<GOAL>StrictAnti f
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>hf'_nonpos : ∀ x ∈ interior D, deriv f x ≤ 0<GOAL>AntitoneOn f D
<VAR>f : ℝ → ℝ<VAR>hf : Differentiable ℝ f<VAR>hf' : ∀ (x : ℝ), deriv f x ≤ 0<GOAL>Antitone f
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f f' : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x<VAR>hf'₀ : ∀ x ∈ interior D, f' x ≤ 0<GOAL>AntitoneOn f D
<VAR>f f' : ℝ → ℝ<VAR>hf : ∀ (x : ℝ), HasDerivAt f (f' x) x<VAR>hf' : f' ≤ 0<GOAL>Antitone f
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>x y : E<VAR>f' : E → E →L[ℝ] ℝ<VAR>hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hs : Convex ℝ s<VAR>xs : x ∈ s<VAR>ys : y ∈ s<GOAL>∃ z ∈ segment ℝ x y, f y - f x = (f' z) (y - x)
<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>H : Type u_5<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>f : G → H<VAR>f' : G → G →L[𝕜] H<VAR>x : G<VAR>hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt f (f' y) y<VAR>hcont : ContinuousAt f' x<GOAL>HasStrictFDerivAt f (f' x) x
<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f f' : 𝕜 → G<VAR>x : 𝕜<VAR>hder : ∀ᶠ (y : 𝕜) in 𝓝 x, HasDerivAt f (f' y) y<VAR>hcont : ContinuousAt f' x<GOAL>HasStrictDerivAt f (f' x) x
<VAR>C : Type w<VAR>CategoryTheory.Category.{u, w} C<VAR>CategoryTheory.HasSheafify (CategoryTheory.coherentTopology LightProfinite) C<VAR>X : C<GOAL>(LightCondensed.discrete C).obj X = (CategoryTheory.presheafToSheaf (CategoryTheory.coherentTopology LightProfinite) C).obj ((CategoryTheory.Functor.const LightProfiniteᵒᵖ).obj X)
<VAR>C : Type w<VAR>CategoryTheory.Category.{u, w} C<VAR>CategoryTheory.HasSheafify (CategoryTheory.coherentTopology LightProfinite) C<GOAL>∀ {X Y : C} (f : X ⟶ Y), (LightCondensed.discrete C).map f = (CategoryTheory.presheafToSheaf (CategoryTheory.coherentTopology LightProfinite) C).map ((CategoryTheory.Functor.const LightProfiniteᵒᵖ).map f)
<VAR>C : Type w<VAR>CategoryTheory.Category.{u, w} C<VAR>j : CategoryTheory.Sheaf (CategoryTheory.coherentTopology LightProfinite) C<GOAL>(LightCondensed.underlying C).obj j = j.val.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))
<VAR>C : Type w<VAR>CategoryTheory.Category.{u, w} C<GOAL>∀ {X Y : CategoryTheory.Sheaf (CategoryTheory.coherentTopology LightProfinite) C} (f : X ⟶ Y), (LightCondensed.underlying C).map f = f.val.app (Opposite.op (LightProfinite.of PUnit.{u + 1}))
<VAR>a b : ℍ<VAR>h : ↑a = ↑b<GOAL>a = b
<VAR>a b : ℍ<GOAL>a = b ↔ ↑a = ↑b
<VAR>a b : ℍ<GOAL>↑a = ↑b ↔ a = b
<VAR>a b : ℍ<VAR>hre : a.re = b.re<VAR>him : a.im = b.im<GOAL>a = b
<VAR>z : ℍ<GOAL>(↑z).im = z.im
<VAR>z : ℍ<GOAL>(↑z).re = z.re
<VAR>z : ℂ<VAR>h : 0 < z.im<GOAL>(UpperHalfPlane.mk z h).re = z.re
<VAR>z : ℂ<VAR>h : 0 < z.im<GOAL>(UpperHalfPlane.mk z h).im = z.im
<VAR>z : ℂ<VAR>h : 0 < z.im<GOAL>↑(UpperHalfPlane.mk z h) = z
<VAR>z : ℍ<VAR>h : 0 < (↑z).im := ⋯<GOAL>UpperHalfPlane.mk (↑z) h = z
<VAR>z : ℍ<GOAL>↑z.re + ↑z.im * Complex.I = ↑z
<VAR>z : ℍ<GOAL>z.im ≠ 0
<VAR>z : ℍ<GOAL>Complex.normSq ↑z ≠ 0
<VAR>g : ↥GL(2, ℝ)⁺<VAR>z : ℍ<GOAL>UpperHalfPlane.denom g z ≠ 0
<VAR>g : ↥GL(2, ℝ)⁺<VAR>z : ℍ<GOAL>0 < Complex.normSq (UpperHalfPlane.denom g z)
<VAR>g : ↥GL(2, ℝ)⁺<VAR>z : ℍ<GOAL>Complex.normSq (UpperHalfPlane.denom g z) ≠ 0
<VAR>g : ↥GL(2, ℝ)⁺<VAR>z : ℍ<GOAL>(UpperHalfPlane.smulAux' g z).im = (↑↑g).det * z.im / Complex.normSq (UpperHalfPlane.denom g z)
<VAR>x y : ↥GL(2, ℝ)⁺<VAR>z : ℍ<GOAL>UpperHalfPlane.denom (x * y) z = UpperHalfPlane.denom x (UpperHalfPlane.smulAux y z) * UpperHalfPlane.denom y z
<VAR>x y : ↥GL(2, ℝ)⁺<VAR>z : ℍ<GOAL>UpperHalfPlane.smulAux (x * y) z = UpperHalfPlane.smulAux x (UpperHalfPlane.smulAux y z)
<VAR>g : SL(2, ℤ)<VAR>i j : Fin 2<GOAL>↑(↑↑↑g i j) = ↑(↑g i j)
<VAR>g : SL(2, ℤ)<GOAL>(↑↑↑g).det = 1
<VAR>s : SL(2, ℤ)<VAR>g : ↥GL(2, ℝ)⁺<VAR>z : ℍ<GOAL>(s • g) • z = (↑s * g) • z
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>s : ↥Γ<VAR>g : ↥GL(2, ℝ)⁺<VAR>z : ℍ<GOAL>(s • g) • z = (↑↑s * g) • z
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>s : ↥Γ<VAR>g : SL(2, ℤ)<VAR>z : ℍ<GOAL>(s • g) • z = (↑s * g) • z
<VAR>R : Type u_1<VAR>CommRing R<VAR>Algebra R ℝ<VAR>g : SL(2, R)<VAR>z : ℍ<GOAL>g • z = UpperHalfPlane.mk ((↑((algebraMap R ℝ) (↑↑g 0 0)) * ↑z + ↑((algebraMap R ℝ) (↑↑g 0 1))) / (↑((algebraMap R ℝ) (↑↑g 1 0)) * ↑z + ↑((algebraMap R ℝ) (↑↑g 1 1)))) ⋯
<VAR>g : ↥GL(2, ℝ)⁺<VAR>z : ℍ<GOAL>↑(g • z) = UpperHalfPlane.num g z / UpperHalfPlane.denom g z
<VAR>g : ↥GL(2, ℝ)⁺<VAR>z : ℍ<GOAL>(g • z).re = (UpperHalfPlane.num g z / UpperHalfPlane.denom g z).re
<VAR>g : ↥GL(2, ℝ)⁺<VAR>z : ℍ<GOAL>(g • z).im = (UpperHalfPlane.num g z / UpperHalfPlane.denom g z).im
<VAR>g : ↥GL(2, ℝ)⁺<VAR>z : ℍ<GOAL>(g • z).im = (↑↑g).det * z.im / Complex.normSq (UpperHalfPlane.denom g z)
<VAR>z : ℍ<VAR>g : SL(2, ℝ)<GOAL>(↑↑(Matrix.SpecialLinearGroup.toGLPos g) 1 0 * z.im) ^ 2 ≤ Complex.normSq (UpperHalfPlane.denom (Matrix.SpecialLinearGroup.toGLPos g) z)
<VAR>g : ↥GL(2, ℝ)⁺<VAR>z : ℍ<GOAL>-g • z = g • z
<VAR>A : SL(2, ℤ)<VAR>z : ℍ<GOAL>A • z = ↑A • z
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>A : ↥Γ<VAR>z : ℍ<GOAL>A • z = ↑↑A • z
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>A : ↥Γ<VAR>z : ℍ<GOAL>A • z = ↑A • z
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<GOAL>-g • z = g • z
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<GOAL>(g • z).im = z.im / Complex.normSq (UpperHalfPlane.denom (↑g) z)
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<GOAL>UpperHalfPlane.denom (↑g) z = ↑(↑g 1 0) * ↑z + ↑(↑g 1 1)
<VAR>x : { x // 0 < x }<VAR>z : ℍ<GOAL>↑(x • z) = ↑x • ↑z
<VAR>x : { x // 0 < x }<VAR>z : ℍ<GOAL>(x • z).im = ↑x * z.im
<VAR>x : { x // 0 < x }<VAR>z : ℍ<GOAL>(x • z).re = ↑x * z.re
<VAR>x : ℝ<VAR>z : ℍ<GOAL>↑(x +ᵥ z) = ↑x + ↑z
<VAR>x : ℝ<VAR>z : ℍ<GOAL>(x +ᵥ z).re = x + z.re
<VAR>x : ℝ<VAR>z : ℍ<GOAL>(x +ᵥ z).im = z.im
<VAR>z : ℍ<GOAL>ModularGroup.S • z = UpperHalfPlane.mk (-↑z)⁻¹ ⋯
<VAR>X : CondensedSet<VAR>S : CompHaus<VAR>x : X.val.obj (Opposite.op S)<GOAL>Continuous fun a => CondensedSet.coinducingCoprod X ⟨⟨S, x⟩, a⟩
<VAR>X Y : CondensedSet<VAR>f : X ⟶ Y<GOAL>∀ (a : X.val.obj (Opposite.op (CompHaus.of PUnit.{u + 1}))), (CondensedSet.toTopCatMap f) a = f.val.app (Opposite.op (CompHaus.of PUnit.{u + 1})) a
<GOAL>∀ {X Y : CondensedSet} (f : X ⟶ Y), condensedSetToTopCat.map f = CondensedSet.toTopCatMap f
<VAR>X : CondensedSet<GOAL>condensedSetToTopCat.obj X = X.toTopCat
<VAR>X : TopCat<VAR>x : ↑X.toCondensedSet.toTopCat<GOAL>(CondensedSet.topCatAdjunctionCounit X) x = x.toFun PUnit.unit
<VAR>X : TopCat<GOAL>Function.Bijective ⇑(CondensedSet.topCatAdjunctionCounit X)
<VAR>X : CondensedSet<VAR>S : CompHausᵒᵖ<VAR>x : X.val.obj S<GOAL>X.topCatAdjunctionUnit.val.app S x = { toFun := fun s => X.val.map (CompHaus.const (Opposite.unop S) s).op x, continuous_toFun := ⋯ }
<VAR>X : CondensedSet<VAR>S : CompHausᵒᵖ<VAR>x : X.val.obj S<VAR>s : ↑(compHausToTop.obj (Opposite.unop S))<GOAL>(X.topCatAdjunctionUnit.val.app S x) s = X.val.map (CompHaus.const (Opposite.unop S) s).op x
<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>CategoryTheory.ConcreteCategory A<VAR>CategoryTheory.ConcreteCategory.HasFunctorialSurjectiveInjectiveFactorization A<VAR>(CategoryTheory.coherentTopology CompHaus).WEqualsLocallyBijective A<VAR>CategoryTheory.HasSheafify (CategoryTheory.coherentTopology CompHaus) A<VAR>(CategoryTheory.coherentTopology CompHaus).HasSheafCompose (CategoryTheory.forget A)<VAR>CategoryTheory.Balanced (CategoryTheory.Sheaf (CategoryTheory.coherentTopology CompHaus) A)<VAR>CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.forget A)<VAR>X Y : Condensed A<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Epi f ↔ ∀ (S : CompHaus) (y : (CategoryTheory.forget A).obj (Y.val.obj (Opposite.op S))), ∃ S' φ, ∃ (_ : Function.Surjective ⇑φ), ∃ x, (f.val.app (Opposite.op S')) x = (Y.val.map (Opposite.op φ)) y
<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>CategoryTheory.ConcreteCategory A<VAR>CategoryTheory.ConcreteCategory.HasFunctorialSurjectiveInjectiveFactorization A<VAR>CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.forget A)<VAR>∀ (X : CompHausᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X Stonean.toCompHaus.op) A<VAR>X Y : Condensed A<VAR>f : X ⟶ Y<VAR>(CategoryTheory.extensiveTopology Stonean).WEqualsLocallyBijective A<VAR>CategoryTheory.HasSheafify (CategoryTheory.extensiveTopology Stonean) A<VAR>(CategoryTheory.extensiveTopology Stonean).HasSheafCompose (CategoryTheory.forget A)<VAR>CategoryTheory.Balanced (CategoryTheory.Sheaf (CategoryTheory.extensiveTopology Stonean) A)<GOAL>CategoryTheory.Epi f ↔ ∀ (S : Stonean), Function.Surjective ⇑(f.val.app (Opposite.op S.compHaus))
<VAR>X Y : CondensedSet<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Epi f ↔ ∀ (S : CompHaus) (y : Y.val.obj (Opposite.op S)), ∃ S' φ, ∃ (_ : Function.Surjective ⇑φ), ∃ x, f.val.app (Opposite.op S') x = Y.val.map (Opposite.op φ) y
<VAR>X Y : CondensedSet<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Epi f ↔ ∀ (S : Stonean), Function.Surjective (f.val.app (Opposite.op S.compHaus))
<VAR>R : Type (u + 1)<VAR>Ring R<VAR>X Y : CondensedMod R<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Epi f ↔ ∀ (S : CompHaus) (y : ↑(Y.val.obj (Opposite.op S))), ∃ S' φ, ∃ (_ : Function.Surjective ⇑φ), ∃ x, (f.val.app (Opposite.op S')) x = (Y.val.map (Opposite.op φ)) y
<VAR>R : Type (u + 1)<VAR>Ring R<VAR>X Y : CondensedMod R<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Epi f ↔ ∀ (S : Stonean), Function.Surjective ⇑(f.val.app (Opposite.op S.compHaus))
<VAR>A : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} A<VAR>F : LightProfiniteᵒᵖ ⥤ A<VAR>CategoryTheory.Limits.PreservesFiniteProducts F<VAR>hF : CategoryTheory.regularTopology.EqualizerCondition F<GOAL>(LightCondensed.ofSheafLightProfinite F hF).val = F
<VAR>A : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} A<VAR>CategoryTheory.ConcreteCategory A<VAR>CategoryTheory.Limits.ReflectsFiniteLimits (CategoryTheory.forget A)<VAR>F : LightProfiniteᵒᵖ ⥤ A<VAR>CategoryTheory.Limits.PreservesFiniteProducts (F ⋙ CategoryTheory.forget A)<VAR>hF : CategoryTheory.regularTopology.EqualizerCondition (F ⋙ CategoryTheory.forget A)<GOAL>(LightCondensed.ofSheafForgetLightProfinite F hF).val = F
<VAR>A : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} A<VAR>X : LightCondensed A<GOAL>CategoryTheory.regularTopology.EqualizerCondition X.val
<VAR>X : TopCat<GOAL>∀ (X_1 : LightProfiniteᵒᵖ), X.toLightCondSet.val.obj X_1 = C(↑(Opposite.unop X_1).toTop, ↑X)
<VAR>X : TopCat<GOAL>∀ {X_1 Y : LightProfiniteᵒᵖ} (f : X_1 ⟶ Y) (g : C(↑(LightProfinite.toTopCat.obj (Opposite.unop X_1)), ↑X)), X.toLightCondSet.val.map f g = g.comp f.unop
<VAR>X : TopCat<GOAL>topCatToLightCondSet.obj X = X.toLightCondSet
<GOAL>∀ {X Y : TopCat} (f : X ⟶ Y) (x : LightProfiniteᵒᵖ) (g : ((fun X => X.toLightCondSet) X).val.obj x), (topCatToLightCondSet.map f).val.app x g = ContinuousMap.comp f g
<VAR>R : Type u<VAR>Ring R<VAR>X Y : LightCondMod R<VAR>f : X ⟶ Y<VAR>S T : LightProfiniteᵒᵖ<VAR>g : S ⟶ T<VAR>x : ↑(X.val.obj S)<GOAL>(f.val.app T) ((X.val.map g) x) = (Y.val.map g) ((f.val.app S) x)
<VAR>C : Type w<VAR>CategoryTheory.Category.{u + 1, w} C<VAR>CategoryTheory.HasWeakSheafify (CategoryTheory.coherentTopology CompHaus) C<GOAL>∀ {X Y : C} (f : X ⟶ Y), (Condensed.discrete C).map f = (CategoryTheory.presheafToSheaf (CategoryTheory.coherentTopology CompHaus) C).map ((CategoryTheory.Functor.const CompHausᵒᵖ).map f)
<VAR>C : Type w<VAR>CategoryTheory.Category.{u + 1, w} C<VAR>CategoryTheory.HasWeakSheafify (CategoryTheory.coherentTopology CompHaus) C<VAR>X : C<GOAL>(Condensed.discrete C).obj X = (CategoryTheory.presheafToSheaf (CategoryTheory.coherentTopology CompHaus) C).obj ((CategoryTheory.Functor.const CompHausᵒᵖ).obj X)
<VAR>C : Type w<VAR>CategoryTheory.Category.{u + 1, w} C<VAR>j : CategoryTheory.Sheaf (CategoryTheory.coherentTopology CompHaus) C<GOAL>(Condensed.underlying C).obj j = j.val.obj (Opposite.op (CompHaus.of PUnit.{u + 1}))
<VAR>C : Type w<VAR>CategoryTheory.Category.{u + 1, w} C<GOAL>∀ {X Y : CategoryTheory.Sheaf (CategoryTheory.coherentTopology CompHaus) C} (f : X ⟶ Y), (Condensed.underlying C).map f = f.val.app (Opposite.op (CompHaus.of PUnit.{u + 1}))
<VAR>R : Type (u + 1)<VAR>Ring R<VAR>A : CondensedMod R<VAR>self : CondensedMod.IsSolid R A<VAR>X : Profinite<GOAL>CategoryTheory.IsIso ((CategoryTheory.yoneda.obj A).map ((Condensed.profiniteSolidification R).app X).op)
<VAR>K : SSet<VAR>Δ : SimplexCategoryᵒᵖ<VAR>x : (𝟙_ SSet ⊗ K).obj Δ<GOAL>(λ_ K).hom.app Δ x = x.2
<VAR>K : SSet<VAR>Δ : SimplexCategoryᵒᵖ<VAR>x : K.obj Δ<GOAL>(λ_ K).inv.app Δ x = (PUnit.unit, x)
<VAR>K : SSet<VAR>Δ : SimplexCategoryᵒᵖ<VAR>x : (K ⊗ 𝟙_ SSet).obj Δ<GOAL>(ρ_ K).hom.app Δ x = x.1
<VAR>K : SSet<VAR>Δ : SimplexCategoryᵒᵖ<VAR>x : K.obj Δ<GOAL>(ρ_ K).inv.app Δ x = (x, PUnit.unit)
<VAR>K K' L L' : SSet<VAR>f : K ⟶ K'<VAR>g : L ⟶ L'<VAR>Δ : SimplexCategoryᵒᵖ<VAR>x : (K ⊗ L).obj Δ<GOAL>(f ⊗ g).app Δ x = (f.app Δ x.1, g.app Δ x.2)
<VAR>K : SSet<VAR>L L' : SSet<VAR>g : L ⟶ L'<VAR>Δ : SimplexCategoryᵒᵖ<VAR>x : (K ⊗ L).obj Δ<GOAL>(K ◁ g).app Δ x = (x.1, g.app Δ x.2)
<VAR>K K' : SSet<VAR>f : K ⟶ K'<VAR>L : SSet<VAR>Δ : SimplexCategoryᵒᵖ<VAR>x : (K ⊗ L).obj Δ<GOAL>(f ▷ L).app Δ x = (f.app Δ x.1, x.2)
<VAR>K L M : SSet<VAR>Δ : SimplexCategoryᵒᵖ<VAR>x : ((K ⊗ L) ⊗ M).obj Δ<GOAL>(α_ K L M).hom.app Δ x = (x.1.1, x.1.2, x.2)
<VAR>K L M : SSet<VAR>Δ : SimplexCategoryᵒᵖ<VAR>x : (K ⊗ L ⊗ M).obj Δ<GOAL>(α_ K L M).inv.app Δ x = ((x.1, x.2.1), x.2.2)
<VAR>X : LightCondSet<VAR>S : LightProfinite<VAR>x : X.val.obj (Opposite.op S)<GOAL>Continuous fun a => LightCondSet.coinducingCoprod X ⟨⟨S, x⟩, a⟩
<VAR>X Y : LightCondSet<VAR>f : X ⟶ Y<GOAL>∀ (a : X.val.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))), (LightCondSet.toTopCatMap f) a = f.val.app (Opposite.op (LightProfinite.of PUnit.{u + 1})) a
<GOAL>∀ {X Y : LightCondSet} (f : X ⟶ Y), lightCondSetToTopCat.map f = LightCondSet.toTopCatMap f
<VAR>X : LightCondSet<GOAL>lightCondSetToTopCat.obj X = X.toTopCat
<VAR>X : TopCat<GOAL>Function.Bijective ⇑(LightCondSet.topCatAdjunctionCounit X)
<VAR>X : LightCondSet<VAR>S : LightProfiniteᵒᵖ<VAR>x : X.val.obj S<VAR>s : ↑(LightProfinite.toTopCat.obj (Opposite.unop S))<GOAL>(X.topCatAdjunctionUnit.val.app S x) s = X.val.map (LightProfinite.const (Opposite.unop S) s).op x
<VAR>X : LightCondSet<VAR>S : LightProfiniteᵒᵖ<VAR>x : X.val.obj S<GOAL>X.topCatAdjunctionUnit.val.app S x = { toFun := fun s => X.val.map (LightProfinite.const (Opposite.unop S) s).op x, continuous_toFun := ⋯ }
<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace ℂ F<VAR>CompleteSpace F<VAR>f : ℂ → F<VAR>z w : ℂ<VAR>hd : DiffContOnCl ℂ f (Metric.ball z (dist w z))<VAR>hz : IsMaxOn (norm ∘ f) (Metric.closedBall z (dist w z)) z<GOAL>‖f w‖ = ‖f z‖
<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace ℂ F<VAR>f : ℂ → F<VAR>z w : ℂ<VAR>hd : DiffContOnCl ℂ f (Metric.ball z (dist w z))<VAR>hz : IsMaxOn (norm ∘ f) (Metric.closedBall z (dist w z)) z<GOAL>‖f w‖ = ‖f z‖
<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace ℂ F<VAR>f : ℂ → F<VAR>z w : ℂ<VAR>r : ℝ<VAR>hr : dist w z = r<VAR>hd : DiffContOnCl ℂ f (Metric.ball z r)<VAR>hz : IsMaxOn (norm ∘ f) (Metric.ball z r) z<GOAL>‖f w‖ = ‖f z‖
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace ℂ F<VAR>f : E → F<VAR>z : E<VAR>r : ℝ<VAR>hd : DiffContOnCl ℂ f (Metric.ball z r)<VAR>hz : IsMaxOn (norm ∘ f) (Metric.ball z r) z<GOAL>Set.EqOn (norm ∘ f) (Function.const E ‖f z‖) (Metric.closedBall z r)
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace ℂ F<VAR>f : E → F<VAR>s : Set E<VAR>z w : E<VAR>hd : DiffContOnCl ℂ f s<VAR>hz : IsMaxOn (norm ∘ f) s z<VAR>hsub : Metric.ball z (dist w z) ⊆ s<GOAL>‖f w‖ = ‖f z‖
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace ℂ F<VAR>f : E → F<VAR>c : E<VAR>hd : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z<VAR>hc : IsLocalMax (norm ∘ f) c<GOAL>∀ᶠ (y : E) in 𝓝 c, ‖f y‖ = ‖f c‖
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace ℂ F<VAR>f : E → F<VAR>s : Set E<VAR>hd : DifferentiableOn ℂ f s<GOAL>IsOpen {z | s ∈ 𝓝 z ∧ IsMaxOn (norm ∘ f) s z}
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace ℂ F<VAR>f : E → F<VAR>U : Set E<VAR>c : E<VAR>hc : IsPreconnected U<VAR>ho : IsOpen U<VAR>hd : DifferentiableOn ℂ f U<VAR>hcU : c ∈ U<VAR>hm : IsMaxOn (norm ∘ f) U c<GOAL>Set.EqOn (norm ∘ f) (Function.const E ‖f c‖) U
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace ℂ F<VAR>f : E → F<VAR>U : Set E<VAR>c : E<VAR>hc : IsPreconnected U<VAR>ho : IsOpen U<VAR>hd : DiffContOnCl ℂ f U<VAR>hcU : c ∈ U<VAR>hm : IsMaxOn (norm ∘ f) U c<GOAL>Set.EqOn (norm ∘ f) (Function.const E ‖f c‖) (closure U)
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace ℂ F<VAR>StrictConvexSpace ℝ F<VAR>f : E → F<VAR>U : Set E<VAR>c : E<VAR>hc : IsPreconnected U<VAR>ho : IsOpen U<VAR>hd : DifferentiableOn ℂ f U<VAR>hcU : c ∈ U<VAR>hm : IsMaxOn (norm ∘ f) U c<GOAL>Set.EqOn f (Function.const E (f c)) U
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace ℂ F<VAR>StrictConvexSpace ℝ F<VAR>f : E → F<VAR>U : Set E<VAR>c : E<VAR>hc : IsPreconnected U<VAR>ho : IsOpen U<VAR>hd : DiffContOnCl ℂ f U<VAR>hcU : c ∈ U<VAR>hm : IsMaxOn (norm ∘ f) U c<GOAL>Set.EqOn f (Function.const E (f c)) (closure U)
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace ℂ F<VAR>StrictConvexSpace ℝ F<VAR>f : E → F<VAR>s : Set E<VAR>z w : E<VAR>hd : DiffContOnCl ℂ f s<VAR>hz : IsMaxOn (norm ∘ f) s z<VAR>hsub : Metric.ball z (dist w z) ⊆ s<GOAL>f w = f z
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace ℂ F<VAR>StrictConvexSpace ℝ F<VAR>f : E → F<VAR>z : E<VAR>r : ℝ<VAR>hd : DiffContOnCl ℂ f (Metric.ball z r)<VAR>hz : IsMaxOn (norm ∘ f) (Metric.ball z r) z<GOAL>Set.EqOn f (Function.const E (f z)) (Metric.closedBall z r)
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace ℂ F<VAR>StrictConvexSpace ℝ F<VAR>f : E → F<VAR>c : E<VAR>hd : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z<VAR>hc : IsLocalMax (norm ∘ f) c<GOAL>∀ᶠ (y : E) in 𝓝 c, f y = f c
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>c : E<VAR>hf : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z<VAR>hc : IsLocalMin (norm ∘ f) c<GOAL>(∀ᶠ (z : E) in 𝓝 c, f z = f c) ∨ f c = 0
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace ℂ F<VAR>Nontrivial E<VAR>FiniteDimensional ℂ E<VAR>f : E → F<VAR>U : Set E<VAR>hb : Bornology.IsBounded U<VAR>hne : U.Nonempty<VAR>hd : DiffContOnCl ℂ f U<GOAL>∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure U) z
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace ℂ F<VAR>Nontrivial E<VAR>f : E → F<VAR>U : Set E<VAR>hU : Bornology.IsBounded U<VAR>hd : DiffContOnCl ℂ f U<VAR>C : ℝ<VAR>hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C<VAR>z : E<VAR>hz : z ∈ closure U<GOAL>‖f z‖ ≤ C
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace ℂ F<VAR>Nontrivial E<VAR>f g : E → F<VAR>U : Set E<VAR>hU : Bornology.IsBounded U<VAR>hf : DiffContOnCl ℂ f U<VAR>hg : DiffContOnCl ℂ g U<VAR>hfg : Set.EqOn f g (frontier U)<GOAL>Set.EqOn f g (closure U)
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace ℂ F<VAR>Nontrivial E<VAR>f g : E → F<VAR>U : Set E<VAR>hU : Bornology.IsBounded U<VAR>hf : DiffContOnCl ℂ f U<VAR>hg : DiffContOnCl ℂ g U<VAR>hfg : Set.EqOn f g (frontier U)<GOAL>Set.EqOn f g U
<VAR>R : Type (u + 1)<VAR>Ring R<VAR>X Y : CondensedMod R<VAR>f : X ⟶ Y<VAR>S T : CompHausᵒᵖ<VAR>g : S ⟶ T<VAR>x : ↑(X.val.obj S)<GOAL>(f.val.app T) ((X.val.map g) x) = (Y.val.map g) ((f.val.app S) x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>f : E → F<VAR>x : E<VAR>h : HasFPowerSeriesAt f p x<GOAL>HasStrictFDerivAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p 1)) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>f : E → F<VAR>x : E<VAR>h : HasFPowerSeriesAt f p x<GOAL>HasFDerivAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p 1)) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>f : E → F<VAR>x : E<VAR>h : HasFPowerSeriesAt f p x<GOAL>DifferentiableAt 𝕜 f x