ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>J : Type w<VAR>inst✝¹ : SmallCategory J<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : J ⥤ C<VAR>c₁ : Cofan fun f => F.obj f.fst.1<VAR>c₂ : Cofan F.obj<VAR>s t : c₁.pt ⟶ c₂.pt<VAR>hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), c₁.ι.app { as := f } ≫ s = F.map f.snd ≫ c₂.ι.app { as := f.fst.2 }<VAR>ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), c₁.ι.app { as := f } ≫ t = c₂.ι.app { as := f.fst.1 }<VAR>i : Cofork s t<VAR>j₁ j₂ : J<VAR>f : j₁ ⟶ j₂<VAR>reassoced : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)) {W : C} {h : c₂.pt ⟶ W}, c₁.ι.app { as := f } ≫ s ≫ h = F.map f.snd ≫ c₂.ι.app { as := f.fst.2 } ≫ h<GOAL>F.map f ≫ c₂.ι.app { as := j₂ } ≫ i.π = (c₂.ι.app { as := j₁ } ≫ i.π) ≫ 𝟙 i.pt
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>inst✝ : PathConnectedSpace X<VAR>n : ℕ<VAR>p : Fin (n + 1) → X<GOAL>∃ γ, ∀ (i : Fin (n + 1)), p i ∈ range ⇑γ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>inst✝ : PathConnectedSpace X<VAR>n : ℕ<VAR>p : Fin (n + 1) → X<VAR>this : IsPathConnected univ<GOAL>∃ γ, ∀ (i : Fin (n + 1)), p i ∈ range ⇑γ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>inst✝ : PathConnectedSpace X<VAR>n : ℕ<VAR>p : Fin (n + 1) → X<VAR>this : IsPathConnected univ<VAR>γ : Path (p 0) (p ↑n)<VAR>h : ∀ (i : Fin (n + 1)), p i ∈ range ⇑γ<GOAL>∃ γ, ∀ (i : Fin (n + 1)), p i ∈ range ⇑γ
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup N<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>Q : QuadraticMap R M N<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra S R<VAR>inst✝³ : Module S M<VAR>inst✝² : IsScalarTower S R M<VAR>inst✝¹ : Module S N<VAR>inst✝ : IsScalarTower S R N<VAR>toFun : M → N<VAR>toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x<VAR>polar_add_left : ∀ (x x' y : M), polar toFun (x + x') y = polar toFun x y + polar toFun x' y<VAR>polar_smul_left : ∀ (a : R) (x y : M), polar toFun (a • x) y = a • polar toFun x y<VAR>x x✝¹ x✝ : M<GOAL>polar toFun x (x✝¹ + x✝) = polar toFun x x✝¹ + polar toFun x x✝
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup N<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>Q : QuadraticMap R M N<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra S R<VAR>inst✝³ : Module S M<VAR>inst✝² : IsScalarTower S R M<VAR>inst✝¹ : Module S N<VAR>inst✝ : IsScalarTower S R N<VAR>toFun : M → N<VAR>toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x<VAR>polar_add_left : ∀ (x x' y : M), polar toFun (x + x') y = polar toFun x y + polar toFun x' y<VAR>polar_smul_left : ∀ (a : R) (x y : M), polar toFun (a • x) y = a • polar toFun x y<VAR>x✝² : R<VAR>x✝¹ x✝ : M<GOAL>polar toFun x✝¹ (x✝² • x✝) = x✝² • polar toFun x✝¹ x✝
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup N<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>Q : QuadraticMap R M N<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra S R<VAR>inst✝³ : Module S M<VAR>inst✝² : IsScalarTower S R M<VAR>inst✝¹ : Module S N<VAR>inst✝ : IsScalarTower S R N<VAR>toFun : M → N<VAR>toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x<VAR>polar_add_left : ∀ (x x' y : M), polar toFun (x + x') y = polar toFun x y + polar toFun x' y<VAR>polar_smul_left : ∀ (a : R) (x y : M), polar toFun (a • x) y = a • polar toFun x y<VAR>x✝¹ x✝ : M<GOAL>toFun (x✝¹ + x✝) = toFun x✝¹ + toFun x✝ + ((LinearMap.mk₂ R (polar toFun) polar_add_left polar_smul_left ⋯ ⋯) x✝¹) x✝
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup N<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>Q : QuadraticMap R M N<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra S R<VAR>inst✝³ : Module S M<VAR>inst✝² : IsScalarTower S R M<VAR>inst✝¹ : Module S N<VAR>inst✝ : IsScalarTower S R N<VAR>toFun : M → N<VAR>toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x<VAR>polar_add_left : ∀ (x x' y : M), polar toFun (x + x') y = polar toFun x y + polar toFun x' y<VAR>polar_smul_left : ∀ (a : R) (x y : M), polar toFun (a • x) y = a • polar toFun x y<VAR>x✝¹ x✝ : M<GOAL>toFun (x✝¹ + x✝) = toFun x✝¹ + toFun x✝ + polar toFun x✝¹ x✝
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hp : Fact (1 ≤ p)<VAR>hm : m ≤ m0<VAR>f g : ↥(lpMeasSubgroup F m p μ)<GOAL>dist (lpMeasSubgroupToLpTrim F p μ hm f) (lpMeasSubgroupToLpTrim F p μ hm g) = dist f g
<VAR>a b : Ordinal.{u_1}<VAR>a0 : 0 < a<VAR>h : a < ω ^ ω ^ b<VAR>b0 : ¬b = 0<GOAL>a * ω ^ ω ^ b = ω ^ ω ^ b
<VAR>a b : Ordinal.{u_1}<VAR>a0 : 0 < a<VAR>h : a < ω ^ ω ^ b<VAR>b0 : ¬b = 0<GOAL>a * ω ^ ω ^ b ≤ ω ^ ω ^ b
<VAR>a b : Ordinal.{u_1}<VAR>a0 : 0 < a<VAR>h : a < ω ^ ω ^ b<VAR>b0 : ¬b = 0<VAR>x : Ordinal.{u_1}<VAR>xb : x < ω ^ b<VAR>ax : a < ω ^ x<GOAL>a * ω ^ ω ^ b ≤ ω ^ ω ^ b
<VAR>a b : Ordinal.{u_1}<VAR>a0 : 0 < a<VAR>h : a < ω ^ ω ^ b<VAR>b0 : ¬b = 0<VAR>x : Ordinal.{u_1}<VAR>xb : x < ω ^ b<VAR>ax : a < ω ^ x<GOAL>ω ^ x * ω ^ ω ^ b ≤ ω ^ ω ^ b
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x y : G<VAR>n m : ℕ<VAR>h : Commute x y<GOAL>orderOf (x * y) ∣ (orderOf x).lcm (orderOf y)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x y : G<VAR>n m : ℕ<VAR>h : Commute x y<GOAL>minimalPeriod ((fun x_1 => x * x_1) ∘ fun x => y * x) 1 ∣ (orderOf x).lcm (orderOf y)
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>W : WeierstrassCurve R<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra S A<VAR>inst✝⁴ : IsScalarTower R S A<VAR>B : Type v<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra S B<VAR>inst✝ : IsScalarTower R S B<VAR>f : A →ₐ[S] B<VAR>n : ℤ<GOAL>(W.baseChange B).ΨSq n = Polynomial.map (↑f) ((W.baseChange A).ΨSq n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>hf : ContinuousOn f s<VAR>hs : IsClosed s<VAR>ht : IsClosed t<GOAL>IsClosed (s ∩ f ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>hf : ContinuousOn f s<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>u : Set α<VAR>hu : IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s<GOAL>IsClosed (s ∩ f ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>hf : ContinuousOn f s<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>u : Set α<VAR>hu : IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s<GOAL>IsClosed (u ∩ s)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝ : CommRing α<VAR>a b : α<VAR>u₁ u₂ : αˣ<GOAL>a /ₚ u₁ + b /ₚ u₂ = (a * ↑u₂ + ↑u₁ * b) /ₚ (u₁ * u₂)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝ : CommRing α<VAR>a b : α<VAR>u₁ u₂ : αˣ<GOAL>a * ↑u₁⁻¹ + b * ↑u₂⁻¹ = a * ↑u₂ * (↑u₂⁻¹ * ↑u₁⁻¹) + ↑u₁ * b * (↑u₂⁻¹ * ↑u₁⁻¹)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝ : CommRing α<VAR>a b : α<VAR>u₁ u₂ : αˣ<GOAL>a * ↑u₁⁻¹ + ↑u₂⁻¹ * b = a * ↑u₂ * (↑u₂⁻¹ * ↑u₁⁻¹) + ↑u₂⁻¹ * ↑u₁⁻¹ * (↑u₁ * b)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>m : ℕ<VAR>hm : n ≤ m<VAR>x : TruncatedWittVector p n R<GOAL>∃ a, (truncate hm) a = x
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>m : ℕ<VAR>hm : n ≤ m<VAR>x : 𝕎 R<GOAL>∃ a, (truncate hm) a = (WittVector.truncate n) x
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<GOAL>‖log (1 + z) - z‖ ≤ ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<GOAL>log (1 + z) - z = log (1 + z) - logTaylor (1 + 1) z
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<GOAL>2 = ↑1 + 1
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>v : V<VAR>inst✝² : Fintype ↑(G.neighborSet v)<VAR>inst✝¹ : DecidableEq V<VAR>inst✝ : Fintype ↑G.edgeSet<VAR>x✝ y✝ : V<GOAL>s(x✝, y✝) ∈ G.incidenceFinset v ↔ s(x✝, y✝) ∈ filter (Membership.mem v) G.edgeFinset
<VAR>a b : ℝ<VAR>n : ℕ<VAR>f : ℝ → ℝ<VAR>μ ν : Measure ℝ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>c d r : ℝ<VAR>h : -1 < r<GOAL>IntervalIntegrable (fun x => x ^ r) volume a b
<VAR>a b : ℝ<VAR>n : ℕ<VAR>f : ℝ → ℝ<VAR>μ ν : Measure ℝ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>c d r : ℝ<VAR>h : -1 < r<GOAL>∀ (c : ℝ), IntervalIntegrable (fun x => x ^ r) volume 0 c
<VAR>a b : ℝ<VAR>n : ℕ<VAR>f : ℝ → ℝ<VAR>μ ν : Measure ℝ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>c✝ d r : ℝ<VAR>h : -1 < r<VAR>this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c<VAR>c : ℝ<GOAL>IntervalIntegrable (fun x => x ^ r) volume 0 c
<VAR>a b : ℝ<VAR>n : ℕ<VAR>f : ℝ → ℝ<VAR>μ ν : Measure ℝ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>c✝ d r : ℝ<VAR>h : -1 < r<VAR>this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c<VAR>c : ℝ<VAR>hc : 0 ≤ c<GOAL>IntervalIntegrable (fun x => x ^ r) volume 0 c
<VAR>a b : ℝ<VAR>n : ℕ<VAR>f : ℝ → ℝ<VAR>μ ν : Measure ℝ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>c✝ d r : ℝ<VAR>h : -1 < r<VAR>this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c<VAR>c : ℝ<VAR>hc : c ≤ 0<GOAL>IntervalIntegrable (fun x => x ^ r) volume 0 c
<VAR>α : Type u_1<VAR>l l₁ l₂ : List α<VAR>p : α → Prop<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>xs ys : List α<GOAL>xs.inter ys.reverse = xs.inter ys
<VAR>α✝ β : Type u<VAR>α : Type u_1<VAR>n : ℕ<VAR>h : ↑n ≤ #α<GOAL>∃ s, n ≤ s.card
<VAR>α✝ β : Type u<VAR>α : Type u_1<VAR>n : ℕ<VAR>h : ↑n ≤ #α<VAR>hα : Finite α<GOAL>∃ s, n ≤ s.card
<VAR>α✝ β : Type u<VAR>α : Type u_1<VAR>n : ℕ<VAR>h : ↑n ≤ #α<VAR>hα : Infinite α<GOAL>∃ s, n ≤ s.card
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : Module ℝ E<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : T2Space E<VAR>inst✝⁶ : TopologicalAddGroup E<VAR>inst✝⁵ : ContinuousSMul ℝ E<VAR>inst✝⁴ : LocallyConvexSpace ℝ E<VAR>s : Set E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module ℝ F<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : T1Space F<VAR>hscomp : IsCompact s<VAR>hsnemp : s.Nonempty<VAR>S : Set (Set E) := {t | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}<GOAL>∃ t ∈ S, ∀ u ∈ S, u ⊆ t → u = t
<VAR>E : Type u_1<VAR>F✝ : Type u_2<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : Module ℝ E<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : T2Space E<VAR>inst✝⁶ : TopologicalAddGroup E<VAR>inst✝⁵ : ContinuousSMul ℝ E<VAR>inst✝⁴ : LocallyConvexSpace ℝ E<VAR>s : Set E<VAR>inst✝³ : AddCommGroup F✝<VAR>inst✝² : Module ℝ F✝<VAR>inst✝¹ : TopologicalSpace F✝<VAR>inst✝ : T1Space F✝<VAR>hscomp : IsCompact s<VAR>hsnemp : s.Nonempty<VAR>S : Set (Set E) := {t | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}<VAR>F : Set (Set E)<VAR>hFS : F ⊆ S<VAR>hF : IsChain (fun x x_1 => x ⊆ x_1) F<GOAL>∃ lb ∈ S, ∀ s ∈ F, lb ⊆ s
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : Module ℝ E<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : T2Space E<VAR>inst✝⁶ : TopologicalAddGroup E<VAR>inst✝⁵ : ContinuousSMul ℝ E<VAR>inst✝⁴ : LocallyConvexSpace ℝ E<VAR>s : Set E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module ℝ F<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : T1Space F<VAR>hscomp : IsCompact s<VAR>hsnemp : s.Nonempty<VAR>S : Set (Set E) := {t | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}<VAR>hFS : ∅ ⊆ S<VAR>hF : IsChain (fun x x_1 => x ⊆ x_1) ∅<GOAL>∃ lb ∈ S, ∀ s ∈ ∅, lb ⊆ s
<VAR>E : Type u_1<VAR>F✝ : Type u_2<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : Module ℝ E<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : T2Space E<VAR>inst✝⁶ : TopologicalAddGroup E<VAR>inst✝⁵ : ContinuousSMul ℝ E<VAR>inst✝⁴ : LocallyConvexSpace ℝ E<VAR>s : Set E<VAR>inst✝³ : AddCommGroup F✝<VAR>inst✝² : Module ℝ F✝<VAR>inst✝¹ : TopologicalSpace F✝<VAR>inst✝ : T1Space F✝<VAR>hscomp : IsCompact s<VAR>hsnemp : s.Nonempty<VAR>S : Set (Set E) := {t | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}<VAR>F : Set (Set E)<VAR>hFS : F ⊆ S<VAR>hF : IsChain (fun x x_1 => x ⊆ x_1) F<VAR>hFnemp : F.Nonempty<GOAL>∃ lb ∈ S, ∀ s ∈ F, lb ⊆ s
<VAR>E : Type u_1<VAR>F✝ : Type u_2<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : Module ℝ E<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : T2Space E<VAR>inst✝⁶ : TopologicalAddGroup E<VAR>inst✝⁵ : ContinuousSMul ℝ E<VAR>inst✝⁴ : LocallyConvexSpace ℝ E<VAR>s : Set E<VAR>inst✝³ : AddCommGroup F✝<VAR>inst✝² : Module ℝ F✝<VAR>inst✝¹ : TopologicalSpace F✝<VAR>inst✝ : T1Space F✝<VAR>hscomp : IsCompact s<VAR>hsnemp : s.Nonempty<VAR>S : Set (Set E) := {t | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}<VAR>F : Set (Set E)<VAR>hFS : F ⊆ S<VAR>hF : IsChain (fun x x_1 => x ⊆ x_1) F<VAR>hFnemp : F.Nonempty<GOAL>(⋂₀ F).Nonempty
<VAR>E : Type u_1<VAR>F✝ : Type u_2<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : Module ℝ E<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : T2Space E<VAR>inst✝⁶ : TopologicalAddGroup E<VAR>inst✝⁵ : ContinuousSMul ℝ E<VAR>inst✝⁴ : LocallyConvexSpace ℝ E<VAR>s : Set E<VAR>inst✝³ : AddCommGroup F✝<VAR>inst✝² : Module ℝ F✝<VAR>inst✝¹ : TopologicalSpace F✝<VAR>inst✝ : T1Space F✝<VAR>hscomp : IsCompact s<VAR>hsnemp : s.Nonempty<VAR>S : Set (Set E) := {t | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}<VAR>F : Set (Set E)<VAR>hFS : F ⊆ S<VAR>hF : IsChain (fun x x_1 => x ⊆ x_1) F<VAR>hFnemp : F.Nonempty<VAR>this : Nonempty ↑F<GOAL>(⋂₀ F).Nonempty
<VAR>E : Type u_1<VAR>F✝ : Type u_2<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : Module ℝ E<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : T2Space E<VAR>inst✝⁶ : TopologicalAddGroup E<VAR>inst✝⁵ : ContinuousSMul ℝ E<VAR>inst✝⁴ : LocallyConvexSpace ℝ E<VAR>s : Set E<VAR>inst✝³ : AddCommGroup F✝<VAR>inst✝² : Module ℝ F✝<VAR>inst✝¹ : TopologicalSpace F✝<VAR>inst✝ : T1Space F✝<VAR>hscomp : IsCompact s<VAR>hsnemp : s.Nonempty<VAR>S : Set (Set E) := {t | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}<VAR>F : Set (Set E)<VAR>hFS : F ⊆ S<VAR>hF : IsChain (fun x x_1 => x ⊆ x_1) F<VAR>hFnemp : F.Nonempty<VAR>this : Nonempty ↑F<GOAL>(⋂ i, ↑i).Nonempty
<VAR>E : Type u_1<VAR>F✝ : Type u_2<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : Module ℝ E<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : T2Space E<VAR>inst✝⁶ : TopologicalAddGroup E<VAR>inst✝⁵ : ContinuousSMul ℝ E<VAR>inst✝⁴ : LocallyConvexSpace ℝ E<VAR>s : Set E<VAR>inst✝³ : AddCommGroup F✝<VAR>inst✝² : Module ℝ F✝<VAR>inst✝¹ : TopologicalSpace F✝<VAR>inst✝ : T1Space F✝<VAR>hscomp : IsCompact s<VAR>hsnemp : s.Nonempty<VAR>S : Set (Set E) := {t | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}<VAR>F : Set (Set E)<VAR>hFS : F ⊆ S<VAR>hF : IsChain (fun x x_1 => x ⊆ x_1) F<VAR>hFnemp : F.Nonempty<VAR>this : Nonempty ↑F<VAR>t u : ↑F<GOAL>∃ z, (fun x x_1 => x ⊇ x_1) ↑t ↑z ∧ (fun x x_1 => x ⊇ x_1) ↑u ↑z
<VAR>E : Type u_1<VAR>F✝ : Type u_2<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : Module ℝ E<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : T2Space E<VAR>inst✝⁶ : TopologicalAddGroup E<VAR>inst✝⁵ : ContinuousSMul ℝ E<VAR>inst✝⁴ : LocallyConvexSpace ℝ E<VAR>s : Set E<VAR>inst✝³ : AddCommGroup F✝<VAR>inst✝² : Module ℝ F✝<VAR>inst✝¹ : TopologicalSpace F✝<VAR>inst✝ : T1Space F✝<VAR>hscomp : IsCompact s<VAR>hsnemp : s.Nonempty<VAR>S : Set (Set E) := {t | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}<VAR>F : Set (Set E)<VAR>hFS : F ⊆ S<VAR>hF : IsChain (fun x x_1 => x ⊆ x_1) F<VAR>hFnemp : F.Nonempty<VAR>this : Nonempty ↑F<VAR>t u : ↑F<VAR>htu : ↑t ⊆ ↑u<GOAL>∃ z, (fun x x_1 => x ⊇ x_1) ↑t ↑z ∧ (fun x x_1 => x ⊇ x_1) ↑u ↑z
<VAR>E : Type u_1<VAR>F✝ : Type u_2<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : Module ℝ E<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : T2Space E<VAR>inst✝⁶ : TopologicalAddGroup E<VAR>inst✝⁵ : ContinuousSMul ℝ E<VAR>inst✝⁴ : LocallyConvexSpace ℝ E<VAR>s : Set E<VAR>inst✝³ : AddCommGroup F✝<VAR>inst✝² : Module ℝ F✝<VAR>inst✝¹ : TopologicalSpace F✝<VAR>inst✝ : T1Space F✝<VAR>hscomp : IsCompact s<VAR>hsnemp : s.Nonempty<VAR>S : Set (Set E) := {t | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}<VAR>F : Set (Set E)<VAR>hFS : F ⊆ S<VAR>hF : IsChain (fun x x_1 => x ⊆ x_1) F<VAR>hFnemp : F.Nonempty<VAR>this : Nonempty ↑F<VAR>t u : ↑F<VAR>hut : ↑u ⊆ ↑t<GOAL>∃ z, (fun x x_1 => x ⊇ x_1) ↑t ↑z ∧ (fun x x_1 => x ⊇ x_1) ↑u ↑z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t : Finset α<VAR>a b : α<GOAL>Monotone card
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>I✝ : Ideal R<VAR>a b : R<VAR>S : Type v<VAR>x✝ y : R<VAR>inst✝ : Semiring S<VAR>I : Ideal R<VAR>f : R →+* S<VAR>H : ∀ a ∈ I, f a = 0<VAR>hf : Function.Surjective ⇑f<VAR>x : R<GOAL>∃ a, (lift I f H) a = f x
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>I✝ : Ideal R<VAR>a b : R<VAR>S : Type v<VAR>x✝ y : R<VAR>inst✝ : Semiring S<VAR>I : Ideal R<VAR>f : R →+* S<VAR>H : ∀ a ∈ I, f a = 0<VAR>hf : Function.Surjective ⇑f<VAR>x : R<GOAL>(lift I f H) ((mk I) x) = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : OuterMeasure α<VAR>f : α → β<VAR>s : Set α<VAR>hs : s.Nonempty<GOAL>((comap f) ⊤) s = ⊤ s
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x✝ : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>iso : E ≃L[𝕜] F<VAR>f : G → E<VAR>x : G<GOAL>DifferentiableAt 𝕜 (⇑iso ∘ f) x ↔ DifferentiableAt 𝕜 f x
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>ha : a ≠ ⊤<VAR>hb : b ≠ 0<GOAL>∃ n > 0, ↑n * a < b
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>ha : a ≠ ⊤<VAR>hb : b ≠ 0<VAR>n : ℕ<VAR>npos : 0 < n<VAR>hn : (↑n)⁻¹ * a < b<GOAL>∃ n > 0, ↑n * a < b
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>ha : a ≠ ⊤<VAR>hb : b ≠ 0<VAR>n : ℕ<VAR>npos : 0 < n<VAR>hn : (↑n)⁻¹ * a < b<GOAL>(↑n)⁻¹ > 0 ∧ ↑(↑n)⁻¹ * a < b
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CharP R 2<VAR>l : List R<GOAL>l.sum * l.sum = (List.map (fun x => x * x) l).sum
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f g : ↥(lpMeasSubgroup F m p μ)<GOAL>lpMeasSubgroupToLpTrim F p μ hm (f - g) = lpMeasSubgroupToLpTrim F p μ hm f - lpMeasSubgroupToLpTrim F p μ hm g
<VAR>X : TopCat<GOAL>EqualizerCondition (yonedaPresheaf LightProfinite.toTopCat ↑X)
<VAR>X : TopCat<GOAL>∀ (Z B : LightProfinite) (π : Z ⟶ B) [inst : EffectiveEpi π], QuotientMap ⇑(LightProfinite.toTopCat.map π)
<VAR>X : TopCat<VAR>Z B : LightProfinite<VAR>π : Z ⟶ B<VAR>he : EffectiveEpi π<GOAL>QuotientMap ⇑(LightProfinite.toTopCat.map π)
<VAR>X : TopCat<VAR>Z B : LightProfinite<VAR>π : Z ⟶ B<VAR>he : Function.Surjective ⇑π<GOAL>QuotientMap ⇑(LightProfinite.toTopCat.map π)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁵ : DivisionRing k<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module k V<VAR>inst✝² : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>inst✝¹ : CharZero k<VAR>inst✝ : Fintype ι<VAR>h : s.card ≠ 0<GOAL>∑ i : ι, centroidWeightsIndicator k s i = 1
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁵ : DivisionRing k<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module k V<VAR>inst✝² : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>inst✝¹ : CharZero k<VAR>inst✝ : Fintype ι<VAR>h : s.card ≠ 0<GOAL>∑ i ∈ s, centroidWeights k s i = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : PseudoMetrizableSpace β<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : BorelSpace β<VAR>ι : Type u_3<VAR>f : ι → α → β<VAR>g : α → β<VAR>u : Filter ι<VAR>inst✝¹ : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>lim : Tendsto f u (𝓝 g)<VAR>this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β<GOAL>Measurable g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : PseudoMetrizableSpace β<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : BorelSpace β<VAR>ι : Type u_3<VAR>f : ι → α → β<VAR>g : α → β<VAR>u : Filter ι<VAR>inst✝¹ : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>lim : Tendsto f u (𝓝 g)<VAR>this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β<GOAL>∀ (s : Set β), IsClosed s → s.Nonempty → s ≠ Set.univ → MeasurableSet (g ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : PseudoMetrizableSpace β<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : BorelSpace β<VAR>ι : Type u_3<VAR>f : ι → α → β<VAR>g : α → β<VAR>u : Filter ι<VAR>inst✝¹ : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>lim : Tendsto f u (𝓝 g)<VAR>this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β<VAR>s : Set β<VAR>h1s : IsClosed s<VAR>h2s : s.Nonempty<VAR>h3s : s ≠ Set.univ<GOAL>MeasurableSet (g ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : PseudoMetrizableSpace β<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : BorelSpace β<VAR>ι : Type u_3<VAR>f : ι → α → β<VAR>g : α → β<VAR>u : Filter ι<VAR>inst✝¹ : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>lim : Tendsto f u (𝓝 g)<VAR>this✝ : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β<VAR>s : Set β<VAR>h1s : IsClosed s<VAR>h2s : s.Nonempty<VAR>h3s : s ≠ Set.univ<VAR>this : Measurable fun x => infNndist (g x) s<GOAL>MeasurableSet (g ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : PseudoMetrizableSpace β<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : BorelSpace β<VAR>ι : Type u_3<VAR>f : ι → α → β<VAR>g : α → β<VAR>u : Filter ι<VAR>inst✝¹ : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>lim : Tendsto f u (𝓝 g)<VAR>this✝ : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β<VAR>s : Set β<VAR>h1s : IsClosed s<VAR>h2s : s.Nonempty<VAR>h3s : s ≠ Set.univ<VAR>this : Measurable fun x => infNndist (g x) s<VAR>h4s : g ⁻¹' s = (fun x => infNndist (g x) s) ⁻¹' {0}<GOAL>MeasurableSet (g ⁻¹' s)