ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → StieltjesFunction<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsCondKernelCDF f κ ν<VAR>a : α<VAR>s : Set (β × ℝ)<VAR>hs : MeasurableSet s<GOAL>∀ (f_1 : ℕ → Set (β × ℝ)), Pairwise (Disjoint on f_1) → (∀ (i : ℕ), MeasurableSet (f_1 i)) → (∀ (i : ℕ), ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) {y | (b, y) ∈ f_1 i} ∂ν a = (κ a) (f_1 i)) → ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) {y | (b, y) ∈ ⋃ i, f_1 i} ∂ν a = (κ a) (⋃ i, f_1 i)
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : GroupWithZero G₀<VAR>a b c g h✝ x : G₀<VAR>h : a * b = 1<GOAL>a⁻¹ = b
<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>f : E → F<VAR>K✝ : Set (E →L[𝕜] F)<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : OpensMeasurableSpace E<VAR>K : Set (E →L[𝕜] F)<VAR>hK : IsComplete K<GOAL>MeasurableSet {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}
<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>f : E → F<VAR>K✝ : Set (E →L[𝕜] F)<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : OpensMeasurableSpace E<VAR>K : Set (E →L[𝕜] F)<VAR>hK : IsComplete K<GOAL>MeasurableSet (⋂ e, ⋃ n, ⋂ p, ⋂ (_ : p ≥ n), ⋂ q, ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e))
<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>f : E → F<VAR>K✝ : Set (E →L[𝕜] F)<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : OpensMeasurableSpace E<VAR>K : Set (E →L[𝕜] F)<VAR>hK : IsComplete K<VAR>b✝⁵ b✝⁴ b✝³ : ℕ<VAR>b✝² : b✝³ ≥ b✝⁴<VAR>b✝¹ : ℕ<VAR>b✝ : b✝¹ ≥ b✝⁴<GOAL>MeasurableSet (B f K ((1 / 2) ^ b✝³) ((1 / 2) ^ b✝¹) ((1 / 2) ^ b✝⁵))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<VAR>a b c : α<GOAL>a ⩿ b ↔ a ⋖ b ∨ a = b
<VAR>R✝ : Type u_1<VAR>inst✝⁶ : NonAssocRing R✝<VAR>inst✝⁵ : Pow R✝ ℕ<VAR>inst✝⁴ : BinomialRing R✝<VAR>R : Type u_2<VAR>inst✝³ : NonAssocRing R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : NatPowAssoc R<VAR>inst✝ : BinomialRing R<VAR>n : ℕ<GOAL>choose 0 (n + 1) = 0
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>n : ℤ<GOAL>(T ^ n • z).im = z.im
<VAR>r r₁ r₂ : ℝ≥0<VAR>x y : ℝ<VAR>s : Set ℝ≥0<GOAL>↑(sSup s) = sSup (toReal '' s)
<VAR>r r₁ r₂ : ℝ≥0<VAR>x y : ℝ<GOAL>↑(sSup ∅) = sSup (toReal '' ∅)
<VAR>r r₁ r₂ : ℝ≥0<VAR>x y : ℝ<VAR>s : Set ℝ≥0<VAR>hs : s.Nonempty<GOAL>↑(sSup s) = sSup (toReal '' s)
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M₁<VAR>s : Submodule R M<VAR>lt : finrank R ↥s < finrank R M<GOAL>s < ⊤
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M₁<VAR>s : Submodule R M<VAR>lt : finrank R ↥s < finrank R ↥⊤<GOAL>s < ⊤
<VAR>R : Type u_1<VAR>inst✝² : LinearOrderedField R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>x y : M<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>(∃ r, 0 < r ∧ x = r • y) ↔ SameRay R x y
<VAR>R : Type u_1<VAR>inst✝² : LinearOrderedField R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>x y : M<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>(∃ r, 0 < r ∧ x = r • y) ↔ SameRay R y x
<VAR>R : Type u_1<VAR>inst✝² : LinearOrderedField R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>x y : M<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>(∃ r, 0 < r ∧ r • y = x) ↔ SameRay R y x
<VAR>ιA : Type u_1<VAR>ιB : Type u_2<VAR>A : ιA → Type u_3<VAR>M : ιB → Type u_4<VAR>inst✝⁷ : AddMonoid ιA<VAR>inst✝⁶ : VAdd ιA ιB<VAR>inst✝⁵ : (i : ιA) → AddCommMonoid (A i)<VAR>inst✝⁴ : (i : ιB) → AddCommMonoid (M i)<VAR>inst✝³ : DecidableEq ιA<VAR>inst✝² : DecidableEq ιB<VAR>inst✝¹ : GSemiring A<VAR>inst✝ : Gmodule A M<VAR>a b : ⨁ (i : ιA), A i<VAR>c : ⨁ (i : ιB), M i<GOAL>(a * b) • c = a • b • c
<VAR>ιA : Type u_1<VAR>ιB : Type u_2<VAR>A : ιA → Type u_3<VAR>M : ιB → Type u_4<VAR>inst✝⁷ : AddMonoid ιA<VAR>inst✝⁶ : VAdd ιA ιB<VAR>inst✝⁵ : (i : ιA) → AddCommMonoid (A i)<VAR>inst✝⁴ : (i : ιB) → AddCommMonoid (M i)<VAR>inst✝³ : DecidableEq ιA<VAR>inst✝² : DecidableEq ιB<VAR>inst✝¹ : GSemiring A<VAR>inst✝ : Gmodule A M<VAR>a b : ⨁ (i : ιA), A i<VAR>c : ⨁ (i : ιB), M i<GOAL>(compHom (smulAddMonoidHom A M)).comp (mulHom A) = ((compHom flipHom) ((compHom (smulAddMonoidHom A M).flip).comp (smulAddMonoidHom A M))).flip
<VAR>ιA : Type u_1<VAR>ιB : Type u_2<VAR>A : ιA → Type u_3<VAR>M : ιB → Type u_4<VAR>inst✝⁷ : AddMonoid ιA<VAR>inst✝⁶ : VAdd ιA ιB<VAR>inst✝⁵ : (i : ιA) → AddCommMonoid (A i)<VAR>inst✝⁴ : (i : ιB) → AddCommMonoid (M i)<VAR>inst✝³ : DecidableEq ιA<VAR>inst✝² : DecidableEq ιB<VAR>inst✝¹ : GSemiring A<VAR>inst✝ : Gmodule A M<VAR>a b : ⨁ (i : ιA), A i<VAR>c : ⨁ (i : ιB), M i<VAR>ai : ιA<VAR>ax : A ai<VAR>bi : ιA<VAR>bx : A bi<VAR>ci : ιB<VAR>cx : M ci<GOAL>(((((((compHom (smulAddMonoidHom A M)).comp (mulHom A)).comp (of A ai)) ax).comp (of A bi)) bx).comp (of M ci)) cx = (((((((compHom flipHom) ((compHom (smulAddMonoidHom A M).flip).comp (smulAddMonoidHom A M))).flip.comp (of A ai)) ax).comp (of A bi)) bx).comp (of M ci)) cx
<VAR>ιA : Type u_1<VAR>ιB : Type u_2<VAR>A : ιA → Type u_3<VAR>M : ιB → Type u_4<VAR>inst✝⁷ : AddMonoid ιA<VAR>inst✝⁶ : VAdd ιA ιB<VAR>inst✝⁵ : (i : ιA) → AddCommMonoid (A i)<VAR>inst✝⁴ : (i : ιB) → AddCommMonoid (M i)<VAR>inst✝³ : DecidableEq ιA<VAR>inst✝² : DecidableEq ιB<VAR>inst✝¹ : GSemiring A<VAR>inst✝ : Gmodule A M<VAR>a b : ⨁ (i : ιA), A i<VAR>c : ⨁ (i : ιB), M i<VAR>ai : ιA<VAR>ax : A ai<VAR>bi : ιA<VAR>bx : A bi<VAR>ci : ιB<VAR>cx : M ci<GOAL>((smulAddMonoidHom A M) (((mulHom A) ((of A ai) ax)) ((of A bi) bx))) ((of M ci) cx) = ((smulAddMonoidHom A M) ((of A ai) ax)) (((smulAddMonoidHom A M) ((of A bi) bx)) ((of M ci) cx))
<VAR>ιA : Type u_1<VAR>ιB : Type u_2<VAR>A : ιA → Type u_3<VAR>M : ιB → Type u_4<VAR>inst✝⁷ : AddMonoid ιA<VAR>inst✝⁶ : VAdd ιA ιB<VAR>inst✝⁵ : (i : ιA) → AddCommMonoid (A i)<VAR>inst✝⁴ : (i : ιB) → AddCommMonoid (M i)<VAR>inst✝³ : DecidableEq ιA<VAR>inst✝² : DecidableEq ιB<VAR>inst✝¹ : GSemiring A<VAR>inst✝ : Gmodule A M<VAR>a b : ⨁ (i : ιA), A i<VAR>c : ⨁ (i : ιB), M i<VAR>ai : ιA<VAR>ax : A ai<VAR>bi : ιA<VAR>bx : A bi<VAR>ci : ιB<VAR>cx : M ci<GOAL>(of M (ai + bi +ᵥ ci)) (GSMul.smul (GMul.mul ax bx) cx) = (of M (ai +ᵥ (bi +ᵥ ci))) (GSMul.smul ax (GSMul.smul bx cx))
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n → α<VAR>i : ℕ<VAR>h : i < (ofFn f).length<GOAL>(ofFn f)[i] = f ⟨i, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>f✝ : α → β → ℝ≥0∞<VAR>E : Type u_4<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f : β → E<VAR>inst✝ : IsSFiniteKernel κ<VAR>a : α<VAR>g : α → β → ℝ≥0<VAR>hg : Measurable (Function.uncurry g)<GOAL>∫ (b : β), f b ∂(κ.withDensity fun a b => ↑(g a b)) a = ∫ (b : β), g a b • f b ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>f✝ : α → β → ℝ≥0∞<VAR>E : Type u_4<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f : β → E<VAR>inst✝ : IsSFiniteKernel κ<VAR>a : α<VAR>g : α → β → ℝ≥0<VAR>hg : Measurable (Function.uncurry g)<GOAL>Measurable (g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>f✝ : α → β → ℝ≥0∞<VAR>E : Type u_4<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f : β → E<VAR>inst✝ : IsSFiniteKernel κ<VAR>a : α<VAR>g : α → β → ℝ≥0<VAR>hg : Measurable (Function.uncurry g)<GOAL>Measurable (Function.uncurry fun a b => ↑(g a b))
<VAR>α : Type u_1<VAR>inst✝³ : DistribLattice α<VAR>inst✝² : OrderBot α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidablePred SupIrred<VAR>a b : α<GOAL>(if h : IsEmpty α then ofIsEmpty else let_fun this := Fintype.toOrderBot α; RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ }) (a ⊓ b) = (if h : IsEmpty α then ofIsEmpty else let_fun this := Fintype.toOrderBot α; RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ }) a ∩ (if h : IsEmpty α then ofIsEmpty else let_fun this := Fintype.toOrderBot α; RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ }) b
<VAR>V : Type u_1<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>V₃ : Type u_4<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : SeminormedAddCommGroup V₁<VAR>inst✝¹ : SeminormedAddCommGroup V₂<VAR>inst✝ : SeminormedAddCommGroup V₃<VAR>f✝ g : NormedAddGroupHom V₁ V₂<VAR>f : NormedAddGroupHom V₂ V₃<VAR>x✝ : V₁<GOAL>(f.comp 0) x✝ = 0 x✝
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{u} → Ordinal.{u}<VAR>c : Cardinal.{u}<VAR>hc : c.IsRegular<VAR>hι : o.card < c<VAR>hc' : c ≠ ℵ₀<VAR>hf : ∀ (i : Ordinal.{u}) (hi : i < o), ∀ b < c.ord, f i hi b < c.ord<VAR>a : Ordinal.{u}<GOAL>lift.{u, u} o.card < c
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s : Set α<VAR>x a : α<VAR>x✝ : x ∈ op a • s<VAR>b : α<VAR>hb : b ∈ s<VAR>Eq : (fun x => op a • x) b = x<GOAL>x * a⁻¹ ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>ι : Type u_2<VAR>inst✝ : TopologicalSpace β<VAR>F : ι → β → α<VAR>f : β → α<VAR>p : Filter ι<VAR>s : Set β<GOAL>TendstoLocallyUniformlyOn F f p s ↔ ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>ι : Type u_2<VAR>inst✝ : TopologicalSpace β<VAR>F : ι → β → α<VAR>f : β → α<VAR>p : Filter ι<VAR>s : Set β<VAR>H : ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε<VAR>u : Set (α × α)<VAR>hu : u ∈ 𝓤 α<VAR>x : β<VAR>hx : x ∈ s<GOAL>∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>ι : Type u_2<VAR>inst✝ : TopologicalSpace β<VAR>F : ι → β → α<VAR>f : β → α<VAR>p : Filter ι<VAR>s : Set β<VAR>H : ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε<VAR>u : Set (α × α)<VAR>hu : u ∈ 𝓤 α<VAR>x : β<VAR>hx : x ∈ s<VAR>ε : ℝ≥0∞<VAR>εpos : ε > 0<VAR>hε : ∀ {a b : α}, edist a b < ε → (a, b) ∈ u<GOAL>∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>ι : Type u_2<VAR>inst✝ : TopologicalSpace β<VAR>F : ι → β → α<VAR>f : β → α<VAR>p : Filter ι<VAR>s : Set β<VAR>H : ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε<VAR>u : Set (α × α)<VAR>hu : u ∈ 𝓤 α<VAR>x : β<VAR>hx : x ∈ s<VAR>ε : ℝ≥0∞<VAR>εpos : ε > 0<VAR>hε : ∀ {a b : α}, edist a b < ε → (a, b) ∈ u<VAR>t : Set β<VAR>ht : t ∈ 𝓝[s] x<VAR>Ht : ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε<GOAL>∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : Preorder α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : IsScott α<VAR>s : Set α<VAR>a : α<VAR>inst✝² : Preorder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : IsScott β<VAR>f : α → β<GOAL>ScottContinuous f ↔ Continuous f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : Preorder α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : IsScott α<VAR>s : Set α<VAR>a : α<VAR>inst✝² : Preorder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : IsScott β<VAR>f : α → β<VAR>h : ScottContinuous f<VAR>u : Set β<VAR>hu : IsOpen u<GOAL>IsOpen (f ⁻¹' u)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : Preorder α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : IsScott α<VAR>s : Set α<VAR>a : α<VAR>inst✝² : Preorder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : IsScott β<VAR>f : α → β<GOAL>Continuous f → ScottContinuous f
<VAR>xl xr : Type u<VAR>L R : List PGame<GOAL>-ofLists L R = ofLists (List.map (fun x => -x) R) (List.map (fun x => -x) L)
<VAR>xl xr : Type u<VAR>L R : List PGame<GOAL>(HEq (fun j => -R[↑j.down]) fun i => -R[↑i.down]) ∧ HEq (fun i => -L[↑i.down]) fun j => -L[↑j.down]
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.52660, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.52667, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.52674, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.52726, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ✝ : Dᵒᵖ ⥤ Type v<VAR>ℱ'✝ : SheafOfTypes K<VAR>α : G.op ⋙ ℱ✝ ⟶ G.op ⋙ ℱ'✝.val<VAR>ℱ ℱ' : SheafOfTypes K<VAR>i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val<VAR>X : D<VAR>x : ℱ.val.obj (op X)<GOAL>(appHom i.hom X ≫ appHom i.inv X) x = 𝟙 (ℱ.val.obj (op X)) x
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.52660, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.52667, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.52674, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.52726, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ✝ : Dᵒᵖ ⥤ Type v<VAR>ℱ'✝ : SheafOfTypes K<VAR>α : G.op ⋙ ℱ✝ ⟶ G.op ⋙ ℱ'✝.val<VAR>ℱ ℱ' : SheafOfTypes K<VAR>i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val<VAR>X : D<VAR>x : ℱ.val.obj (op X)<GOAL>∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X), ℱ.val.map f.op ((appHom i.hom X ≫ appHom i.inv X) x) = ℱ.val.map f.op (𝟙 (ℱ.val.obj (op X)) x)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.52660, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.52667, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.52674, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.52726, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ✝ : Dᵒᵖ ⥤ Type v<VAR>ℱ'✝ : SheafOfTypes K<VAR>α : G.op ⋙ ℱ✝ ⟶ G.op ⋙ ℱ'✝.val<VAR>ℱ ℱ' : SheafOfTypes K<VAR>i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val<VAR>X : D<VAR>x : ℱ'.val.obj (op X)<GOAL>(appHom i.inv X ≫ appHom i.hom X) x = 𝟙 (ℱ'.val.obj (op X)) x
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.52660, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.52667, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.52674, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.52726, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ✝ : Dᵒᵖ ⥤ Type v<VAR>ℱ'✝ : SheafOfTypes K<VAR>α : G.op ⋙ ℱ✝ ⟶ G.op ⋙ ℱ'✝.val<VAR>ℱ ℱ' : SheafOfTypes K<VAR>i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val<VAR>X : D<VAR>x : ℱ'.val.obj (op X)<GOAL>∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X), ℱ'.val.map f.op ((appHom i.inv X ≫ appHom i.hom X) x) = ℱ'.val.map f.op (𝟙 (ℱ'.val.obj (op X)) x)
<VAR>a b c x : ℕ<GOAL>x ∈ Ico a.succ b ↔ x ∈ Ioo a b
<VAR>z : ℂ<VAR>hz : 1 + z ∈ slitPlane<GOAL>log (1 + z) = z * ∫ (t : ℝ) in 0 ..1, (1 + t • z)⁻¹
<VAR>z : ℂ<VAR>hz : 1 + z ∈ slitPlane<GOAL>log (1 + z) = log (1 + z) - log 1
<VAR>m n✝ n : ℕ<VAR>nz : NeZero n<VAR>a : ZMod n<VAR>na : NeZero a<GOAL>(-a).val = n - a.val
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : CompleteSpace F<VAR>f : ℂ → F<VAR>z w : ℂ<VAR>r : ℝ := dist w z<VAR>hd : DiffContOnCl ℂ f (ball z r)<VAR>hz : IsMaxOn (norm ∘ f) (closedBall z r) z<GOAL>‖f w‖ = ‖f z‖
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : CompleteSpace F<VAR>f : ℂ → F<VAR>z w : ℂ<VAR>r : ℝ := dist w z<VAR>hd : DiffContOnCl ℂ f (ball z r)<VAR>hz : IsMaxOn (norm ∘ f) (closedBall z r) z<VAR>hw : w ∈ closedBall z r<GOAL>‖f w‖ = ‖f z‖
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : CompleteSpace F<VAR>f : ℂ → F<VAR>z w : ℂ<VAR>r : ℝ := dist w z<VAR>hd : DiffContOnCl ℂ f (ball z r)<VAR>hz : IsMaxOn (norm ∘ f) (closedBall z r) z<VAR>hw : w ∈ closedBall z r<GOAL>¬(norm ∘ f) w < (norm ∘ f) z
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : CompleteSpace F<VAR>f : ℂ → F<VAR>z w : ℂ<VAR>r : ℝ := dist w z<VAR>hd : DiffContOnCl ℂ f (ball z r)<VAR>hz : IsMaxOn (norm ∘ f) (closedBall z r) z<VAR>hw : w ∈ closedBall z r<VAR>hw_lt : ‖f w‖ < ‖f z‖<GOAL>False
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : CompleteSpace F<VAR>f : ℂ → F<VAR>z w : ℂ<VAR>r : ℝ := dist w z<VAR>hd : DiffContOnCl ℂ f (ball z r)<VAR>hz : IsMaxOn (norm ∘ f) (closedBall z r) z<VAR>hw : w ∈ closedBall z r<VAR>hw_lt : ‖f w‖ < ‖f z‖<VAR>hr : 0 < r<GOAL>False
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : CompleteSpace F<VAR>f : ℂ → F<VAR>z w : ℂ<VAR>r : ℝ := dist w z<VAR>hd : DiffContOnCl ℂ f (ball z r)<VAR>hz : IsMaxOn (norm ∘ f) (closedBall z r) z<VAR>hw : w ∈ closedBall z r<VAR>hw_lt : ‖f w‖ < ‖f z‖<VAR>hr : 0 < r<GOAL>‖∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ‖ < 2 * π * ‖f z‖
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : CompleteSpace F<VAR>f : ℂ → F<VAR>z w : ℂ<VAR>r : ℝ := dist w z<VAR>hd : DiffContOnCl ℂ f (ball z r)<VAR>hz : IsMaxOn (norm ∘ f) (closedBall z r) z<VAR>hw : w ∈ closedBall z r<VAR>hw_lt : ‖f w‖ < ‖f z‖<VAR>hr : 0 < r<GOAL>‖∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ‖ < 2 * π * r * (‖f z‖ / r)
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : CompleteSpace F<VAR>f : ℂ → F<VAR>z w : ℂ<VAR>r : ℝ := dist w z<VAR>hd : DiffContOnCl ℂ f (ball z r)<VAR>hz : IsMaxOn (norm ∘ f) (closedBall z r) z<VAR>hw : w ∈ closedBall z r<VAR>hw_lt : ‖f w‖ < ‖f z‖<VAR>hr : 0 < r<VAR>hsub : sphere z r ⊆ closedBall z r<GOAL>‖∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ‖ < 2 * π * r * (‖f z‖ / r)
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : CompleteSpace F<VAR>f : ℂ → F<VAR>z w : ℂ<VAR>r : ℝ := dist w z<VAR>hd : DiffContOnCl ℂ f (ball z r)<VAR>hz : IsMaxOn (norm ∘ f) (closedBall z r) z<VAR>hw : w ∈ closedBall z r<VAR>hw_lt : ‖f w‖ < ‖f z‖<VAR>hr : 0 < r<VAR>hsub : sphere z r ⊆ closedBall z r<GOAL>ContinuousOn (fun ζ => (ζ - z)⁻¹ • f ζ) (sphere z r)
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : CompleteSpace F<VAR>f : ℂ → F<VAR>z w : ℂ<VAR>r : ℝ := dist w z<VAR>hd : DiffContOnCl ℂ f (ball z r)<VAR>hz : IsMaxOn (norm ∘ f) (closedBall z r) z<VAR>hw : w ∈ closedBall z r<VAR>hw_lt : ‖f w‖ < ‖f z‖<VAR>hr : 0 < r<VAR>hsub : sphere z r ⊆ closedBall z r<GOAL>∀ z_1 ∈ sphere z r, ‖(z_1 - z)⁻¹ • f z_1‖ ≤ ‖f z‖ / r
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : CompleteSpace F<VAR>f : ℂ → F<VAR>z w : ℂ<VAR>r : ℝ := dist w z<VAR>hd : DiffContOnCl ℂ f (ball z r)<VAR>hz : IsMaxOn (norm ∘ f) (closedBall z r) z<VAR>hw : w ∈ closedBall z r<VAR>hw_lt : ‖f w‖ < ‖f z‖<VAR>hr : 0 < r<VAR>hsub : sphere z r ⊆ closedBall z r<GOAL>‖(w - z)⁻¹ • f w‖ < ‖f z‖ / r
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : CompleteSpace F<VAR>f : ℂ → F<VAR>z w : ℂ<VAR>r : ℝ := dist w z<VAR>hd : DiffContOnCl ℂ f (ball z r)<VAR>hz : IsMaxOn (norm ∘ f) (closedBall z r) z<VAR>hw : w ∈ closedBall z r<VAR>hw_lt : ‖f w‖ < ‖f z‖<VAR>hr : 0 < r<VAR>hsub : sphere z r ⊆ closedBall z r<GOAL>‖f w‖ / abs (w - z) < ‖f z‖ / r
<VAR>R S T : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : CommRing T<VAR>f : R →+* S<VAR>g : S →+* T<VAR>hf : f.Finite<VAR>hg : g.Finite<GOAL>(g.comp f).Finite
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>ht : t ∈ 𝓝[s] x<GOAL>LiftPropWithinAt P g (s ∩ t) x ↔ LiftPropWithinAt P g s x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>ht : t ∈ 𝓝[s] x<GOAL>↑(chartAt H x).symm ⁻¹' (s ∩ t) =ᶠ[𝓝 (↑(chartAt H x) x)] ↑(chartAt H x).symm ⁻¹' s
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>ht : t ∈ 𝓝[s] x<GOAL>∀ᶠ (x : M) in 𝓝 x, x ∈ s ∩ t ↔ x ∈ s
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIcoDiv hp a b = ⌊(b - a) / p⌋
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>b - ⌊(b - a) / p⌋ • p ∈ Set.Ico a (a + p)
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>0 ≤ b - a - ↑⌊(b - a) / p⌋ * p ∧ b - a - ↑⌊(b - a) / p⌋ * p < p
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : InnerProductSpace ℝ H<VAR>s✝ t : Set H<VAR>x : H<VAR>s : Set H<GOAL>(insert x s).innerDualCone = {x}.innerDualCone ⊓ s.innerDualCone
<VAR>R : Type u_1<VAR>inst✝³ : Monoid R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddMonoid X<VAR>inst✝ : DistribMulAction R X<VAR>r : R<VAR>s : ↥S<GOAL>(r /ₒ s) • 0 = 0
<VAR>o₁ o₂ : ONote<VAR>inst✝¹ : o₁.NF<VAR>inst✝ : o₂.NF<VAR>a : ONote<VAR>m : ℕ<VAR>e₁ : o₁.split = (a, m)<GOAL>(o₁ ^ o₂).repr = o₁.repr ^ o₂.repr