ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>u v : V<VAR>h : G.Adj u v<VAR>x✝ : V<GOAL>(∃ w, u = x✝ ∧ v = w ∨ u = w ∧ v = x✝) → x✝ ∈ {u, v}
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>u v : V<VAR>h : G.Adj u v<VAR>x✝ w✝ : V<VAR>hw : u = x✝ ∧ v = w✝ ∨ u = w✝ ∧ v = x✝<GOAL>x✝ ∈ {u, v}
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasStrongEpiMonoFactorisations C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>I' : C<VAR>e : X ⟶ I'<VAR>m : I' ⟶ Y<VAR>comm : e ≫ m = f<VAR>inst✝¹ : StrongEpi e<VAR>inst✝ : Mono m<GOAL>(StrongEpiMonoFactorisation.mk (MonoFactorisation.mk I' m e ⋯)).toMonoIsImage.lift (Image.monoFactorisation f) ≫ ι f = m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>x : M ⊗[R] N<GOAL>∃ S, x = S.sum fun n m => m ⊗ₜ[R] n
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>x : M ⊗[R] N<VAR>S : N →₀ M<VAR>h : (TensorProduct.comm R M N) x = S.sum fun m n => m ⊗ₜ[R] n<GOAL>∃ S, x = S.sum fun n m => m ⊗ₜ[R] n
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>x : M ⊗[R] N<VAR>S : N →₀ M<VAR>h : (TensorProduct.comm R M N) x = S.sum fun m n => m ⊗ₜ[R] n<GOAL>(TensorProduct.comm R M N) x = (TensorProduct.comm R M N) (S.sum fun n m => m ⊗ₜ[R] n)
<VAR>x : ℝ<VAR>hx : 0 ≤ x<VAR>hx' : x ≤ 1<GOAL>x ≤ sin (π / 2 * x)
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝³ : Category.{v', u'} A<VAR>inst✝² : ConcreteCategory A<VAR>F₁ F₂ F₃ : Cᵒᵖ ⥤ A<VAR>f₁ : F₁ ⟶ F₂<VAR>f₂ : F₂ ⟶ F₃<VAR>inst✝¹ : IsLocallyInjective J f₂<VAR>inst✝ : IsLocallySurjective J (f₁ ≫ f₂)<GOAL>IsLocallySurjective J f₁
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<GOAL>eLpNorm 0 p μ < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<GOAL>0 < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq β<VAR>f g : α → β<VAR>s : Finset α<VAR>t : Finset β<VAR>a : α<VAR>b c : β<GOAL>c ∈ image (const α b) s ↔ s.Nonempty ∧ b = c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq β<VAR>f g : α → β<VAR>s : Finset α<VAR>t : Finset β<VAR>a : α<VAR>b c : β<GOAL>(∃ a ∈ s, const α b a = c) ↔ s.Nonempty ∧ b = c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq β<VAR>f g : α → β<VAR>s : Finset α<VAR>t : Finset β<VAR>a : α<VAR>b c : β<GOAL>(∃ x, x ∈ s) ∧ b = c ↔ s.Nonempty ∧ b = c
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>hg : HasStrictDerivAt g₁ g₁' (h x)<VAR>hh : HasStrictDerivAt h h' x<VAR>hy : y = h x<GOAL>HasStrictDerivAt (g₁ ∘ h) (h' • g₁') x
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>f : α → γ<VAR>g : β → γ<VAR>s : Multiset α<VAR>t : Multiset β<GOAL>(map f s).Disjoint (map g t) ↔ ∀ a ∈ s, ∀ b ∈ t, f a ≠ g b
<VAR>x y : ℂ<GOAL>sinh (x * I) = sin x * I
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>m✝ m : Multiset α<VAR>x : m.ToType<GOAL>m.coeEmbedding x ∈ m.toEnumFinset
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>m✝ m : Multiset α<VAR>x : m.ToType<GOAL>(m.coeEmbedding x).2 < count (m.coeEmbedding x).1 m
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>m✝ m : Multiset α<VAR>x : { x // x ∈ m.toEnumFinset }<GOAL>(↑x).2 < count (↑x).1 m
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>m✝ m : Multiset α<VAR>x : { x // x ∈ m.toEnumFinset }<GOAL>↑x ∈ m.toEnumFinset
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDedekindDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>a : A<GOAL>Prime (span {a}) ↔ Prime a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDedekindDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<GOAL>Prime (span {0}) ↔ Prime 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDedekindDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>a : A<VAR>ha : a ≠ 0<GOAL>Prime (span {a}) ↔ Prime a
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<VAR>h : IsUnit A.det<GOAL>A⁻¹ = ↑h.unit⁻¹ • A.adjugate
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝³ : DecidableEq l<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Semiring α<VAR>i : m<VAR>j : n<VAR>c : α<VAR>i' : m<VAR>j' : n<VAR>h : ¬(i = i' ∧ j = j')<GOAL>stdBasisMatrix i j c i' j' = 0
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝³ : DecidableEq l<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Semiring α<VAR>i : m<VAR>j : n<VAR>c : α<VAR>i' : m<VAR>j' : n<VAR>h : ¬(i = i' ∧ j = j')<GOAL>i = i' → j = j' → c = 0
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : PartialOrder R<VAR>inst✝² : StarRing R<VAR>inst✝¹ : StarOrderedRing R<VAR>inst✝ : RCLike 𝕜<VAR>M : Matrix n n R<VAR>hM : M.PosDef<GOAL>Mᵀ.PosDef
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : PartialOrder R<VAR>inst✝² : StarRing R<VAR>inst✝¹ : StarOrderedRing R<VAR>inst✝ : RCLike 𝕜<VAR>M : Matrix n n R<VAR>hM : M.PosDef<VAR>x : n → R<VAR>hx : x ≠ 0<GOAL>0 < star x ⬝ᵥ Mᵀ *ᵥ x
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : PartialOrder R<VAR>inst✝² : StarRing R<VAR>inst✝¹ : StarOrderedRing R<VAR>inst✝ : RCLike 𝕜<VAR>M : Matrix n n R<VAR>hM : M.PosDef<VAR>x : n → R<VAR>hx : x ≠ 0<GOAL>star x ⬝ᵥ Mᵀ *ᵥ x = star (star x) ⬝ᵥ M *ᵥ star x
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>inst✝⁷ : Category.{v₁, u₁} A<VAR>inst✝⁶ : Category.{v₂, u₂} B<VAR>inst✝⁵ : HasEqualizers A<VAR>inst✝⁴ : HasImages A<VAR>inst✝³ : StrongEpiCategory B<VAR>inst✝² : HasImages B<VAR>L : A ⥤ B<VAR>inst✝¹ : {X Y Z : A} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PreservesLimit (cospan f g) L<VAR>inst✝ : {X Y Z : A} → (f : X ⟶ Y) → (g : X ⟶ Z) → PreservesColimit (span f g) L<VAR>X Y : A<VAR>f : X ⟶ Y<GOAL>L.map (factorThruImage f) ≫ L.map (image.ι f) = L.map f
<VAR>X : Type u<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>h : Projective X<VAR>U : Set X<VAR>hU : IsOpen U<VAR>Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}<VAR>Z₂ : Set (X × Bool) := closure U ×ˢ {false}<VAR>Z : Set (X × Bool) := Z₁ ∪ Z₂<GOAL>IsOpen (closure U)
<VAR>X : Type u<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>h : Projective X<VAR>U : Set X<VAR>hU : IsOpen U<VAR>Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}<VAR>Z₂ : Set (X × Bool) := closure U ×ˢ {false}<VAR>Z : Set (X × Bool) := Z₁ ∪ Z₂<VAR>hZ₁₂ : Disjoint Z₁ Z₂<GOAL>IsOpen (closure U)
<VAR>X : Type u<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>h : Projective X<VAR>U : Set X<VAR>hU : IsOpen U<VAR>Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}<VAR>Z₂ : Set (X × Bool) := closure U ×ˢ {false}<VAR>Z : Set (X × Bool) := Z₁ ∪ Z₂<VAR>hZ₁₂ : Disjoint Z₁ Z₂<VAR>hZ₁ : IsClosed Z₁<GOAL>IsOpen (closure U)
<VAR>X : Type u<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>h : Projective X<VAR>U : Set X<VAR>hU : IsOpen U<VAR>Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}<VAR>Z₂ : Set (X × Bool) := closure U ×ˢ {false}<VAR>Z : Set (X × Bool) := Z₁ ∪ Z₂<VAR>hZ₁₂ : Disjoint Z₁ Z₂<VAR>hZ₁ : IsClosed Z₁<VAR>hZ₂ : IsClosed Z₂<GOAL>IsOpen (closure U)
<VAR>X : Type u<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>h : Projective X<VAR>U : Set X<VAR>hU : IsOpen U<VAR>Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}<VAR>Z₂ : Set (X × Bool) := closure U ×ˢ {false}<VAR>Z : Set (X × Bool) := Z₁ ∪ Z₂<VAR>hZ₁₂ : Disjoint Z₁ Z₂<VAR>hZ₁ : IsClosed Z₁<VAR>hZ₂ : IsClosed Z₂<VAR>hZ : IsClosed Z<GOAL>IsOpen (closure U)
<VAR>X : Type u<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>h : Projective X<VAR>U : Set X<VAR>hU : IsOpen U<VAR>Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}<VAR>Z₂ : Set (X × Bool) := closure U ×ˢ {false}<VAR>Z : Set (X × Bool) := Z₁ ∪ Z₂<VAR>hZ₁₂ : Disjoint Z₁ Z₂<VAR>hZ₁ : IsClosed Z₁<VAR>hZ₂ : IsClosed Z₂<VAR>hZ : IsClosed Z<VAR>f : ↑Z → X := Prod.fst ∘ Subtype.val<GOAL>IsOpen (closure U)
<VAR>X : Type u<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>h : Projective X<VAR>U : Set X<VAR>hU : IsOpen U<VAR>Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}<VAR>Z₂ : Set (X × Bool) := closure U ×ˢ {false}<VAR>Z : Set (X × Bool) := Z₁ ∪ Z₂<VAR>hZ₁₂ : Disjoint Z₁ Z₂<VAR>hZ₁ : IsClosed Z₁<VAR>hZ₂ : IsClosed Z₂<VAR>hZ : IsClosed Z<VAR>f : ↑Z → X := Prod.fst ∘ Subtype.val<VAR>f_cont : Continuous f<GOAL>IsOpen (closure U)
<VAR>X : Type u<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>h : Projective X<VAR>U : Set X<VAR>hU : IsOpen U<VAR>Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}<VAR>Z₂ : Set (X × Bool) := closure U ×ˢ {false}<VAR>Z : Set (X × Bool) := Z₁ ∪ Z₂<VAR>hZ₁₂ : Disjoint Z₁ Z₂<VAR>hZ₁ : IsClosed Z₁<VAR>hZ₂ : IsClosed Z₂<VAR>hZ : IsClosed Z<VAR>f : ↑Z → X := Prod.fst ∘ Subtype.val<VAR>f_cont : Continuous f<VAR>f_sur : Surjective f<GOAL>IsOpen (closure U)
<VAR>X : Type u<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>h : Projective X<VAR>U : Set X<VAR>hU : IsOpen U<VAR>Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}<VAR>Z₂ : Set (X × Bool) := closure U ×ˢ {false}<VAR>Z : Set (X × Bool) := Z₁ ∪ Z₂<VAR>hZ₁₂ : Disjoint Z₁ Z₂<VAR>hZ₁ : IsClosed Z₁<VAR>hZ₂ : IsClosed Z₂<VAR>hZ : IsClosed Z<VAR>f : ↑Z → X := Prod.fst ∘ Subtype.val<VAR>f_cont : Continuous f<VAR>f_sur : Surjective f<VAR>this : CompactSpace ↑Z<GOAL>IsOpen (closure U)
<VAR>X : Type u<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>h : Projective X<VAR>U : Set X<VAR>hU : IsOpen U<VAR>Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}<VAR>Z₂ : Set (X × Bool) := closure U ×ˢ {false}<VAR>Z : Set (X × Bool) := Z₁ ∪ Z₂<VAR>hZ₁₂ : Disjoint Z₁ Z₂<VAR>hZ₁ : IsClosed Z₁<VAR>hZ₂ : IsClosed Z₂<VAR>hZ : IsClosed Z<VAR>f : ↑Z → X := Prod.fst ∘ Subtype.val<VAR>f_cont : Continuous f<VAR>f_sur : Surjective f<VAR>this : CompactSpace ↑Z<VAR>g : X → ↑Z<VAR>hg : Continuous g<VAR>g_sec : f ∘ g = id<GOAL>IsOpen (closure U)
<VAR>X : Type u<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>h : Projective X<VAR>U : Set X<VAR>hU : IsOpen U<VAR>Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}<VAR>Z₂ : Set (X × Bool) := closure U ×ˢ {false}<VAR>Z : Set (X × Bool) := Z₁ ∪ Z₂<VAR>hZ₁₂ : Disjoint Z₁ Z₂<VAR>hZ₁ : IsClosed Z₁<VAR>hZ₂ : IsClosed Z₂<VAR>hZ : IsClosed Z<VAR>f : ↑Z → X := Prod.fst ∘ Subtype.val<VAR>f_cont : Continuous f<VAR>f_sur : Surjective f<VAR>this : CompactSpace ↑Z<VAR>g : X → ↑Z<VAR>hg : Continuous g<VAR>g_sec : f ∘ g = id<VAR>φ : X → X × Bool := Subtype.val ∘ g<GOAL>IsOpen (closure U)
<VAR>X : Type u<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>h : Projective X<VAR>U : Set X<VAR>hU : IsOpen U<VAR>Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}<VAR>Z₂ : Set (X × Bool) := closure U ×ˢ {false}<VAR>Z : Set (X × Bool) := Z₁ ∪ Z₂<VAR>hZ₁₂ : Disjoint Z₁ Z₂<VAR>hZ₁ : IsClosed Z₁<VAR>hZ₂ : IsClosed Z₂<VAR>hZ : IsClosed Z<VAR>f : ↑Z → X := Prod.fst ∘ Subtype.val<VAR>f_cont : Continuous f<VAR>f_sur : Surjective f<VAR>this : CompactSpace ↑Z<VAR>g : X → ↑Z<VAR>hg : Continuous g<VAR>g_sec : f ∘ g = id<VAR>φ : X → X × Bool := Subtype.val ∘ g<VAR>hφ : Continuous φ<GOAL>IsOpen (closure U)
<VAR>X : Type u<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>h : Projective X<VAR>U : Set X<VAR>hU : IsOpen U<VAR>Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}<VAR>Z₂ : Set (X × Bool) := closure U ×ˢ {false}<VAR>Z : Set (X × Bool) := Z₁ ∪ Z₂<VAR>hZ₁₂ : Disjoint Z₁ Z₂<VAR>hZ₁ : IsClosed Z₁<VAR>hZ₂ : IsClosed Z₂<VAR>hZ : IsClosed Z<VAR>f : ↑Z → X := Prod.fst ∘ Subtype.val<VAR>f_cont : Continuous f<VAR>f_sur : Surjective f<VAR>this : CompactSpace ↑Z<VAR>g : X → ↑Z<VAR>hg : Continuous g<VAR>g_sec : f ∘ g = id<VAR>φ : X → X × Bool := Subtype.val ∘ g<VAR>hφ : Continuous φ<VAR>hφ₁ : ∀ (x : X), (φ x).1 = x<GOAL>closure U = φ ⁻¹' Z₂
<VAR>X : Type u<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>h : Projective X<VAR>U : Set X<VAR>hU : IsOpen U<VAR>Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}<VAR>Z₂ : Set (X × Bool) := closure U ×ˢ {false}<VAR>Z : Set (X × Bool) := Z₁ ∪ Z₂<VAR>hZ₁₂ : Disjoint Z₁ Z₂<VAR>hZ₁ : IsClosed Z₁<VAR>hZ₂ : IsClosed Z₂<VAR>hZ : IsClosed Z<VAR>f : ↑Z → X := Prod.fst ∘ Subtype.val<VAR>f_cont : Continuous f<VAR>f_sur : Surjective f<VAR>this : CompactSpace ↑Z<VAR>g : X → ↑Z<VAR>hg : Continuous g<VAR>g_sec : f ∘ g = id<VAR>φ : X → X × Bool := Subtype.val ∘ g<VAR>hφ : Continuous φ<VAR>hφ₁ : ∀ (x : X), (φ x).1 = x<GOAL>U ⊆ φ ⁻¹' Z₂
<VAR>X : Type u<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>h : Projective X<VAR>U : Set X<VAR>hU : IsOpen U<VAR>Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}<VAR>Z₂ : Set (X × Bool) := closure U ×ˢ {false}<VAR>Z : Set (X × Bool) := Z₁ ∪ Z₂<VAR>hZ₁₂ : Disjoint Z₁ Z₂<VAR>hZ₁ : IsClosed Z₁<VAR>hZ₂ : IsClosed Z₂<VAR>hZ : IsClosed Z<VAR>f : ↑Z → X := Prod.fst ∘ Subtype.val<VAR>f_cont : Continuous f<VAR>f_sur : Surjective f<VAR>this : CompactSpace ↑Z<VAR>g : X → ↑Z<VAR>hg : Continuous g<VAR>g_sec : f ∘ g = id<VAR>φ : X → X × Bool := Subtype.val ∘ g<VAR>hφ : Continuous φ<VAR>hφ₁ : ∀ (x : X), (φ x).1 = x<VAR>x : X<VAR>hx : x ∈ φ ⁻¹' Z₂<GOAL>x ∈ closure U
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f✝ : α → β<VAR>b : β<VAR>s : Finset α<VAR>a : α<VAR>f g : α → β<VAR>b₁ b₂ : β<GOAL>fold op (op b₁ b₂) (fun x => op (f x) (g x)) s = op (fold op b₁ f s) (fold op b₂ g s)
<VAR>α : Type u<VAR>β : Type v<VAR>γ✝ : Type w<VAR>ι : Sort x<VAR>γ : Type u_1<VAR>inst✝¹ : Preorder β<VAR>inst✝ : Preorder γ<VAR>f : α → β<VAR>g : β → γ<VAR>hf : BddAbove (range f)<VAR>hg : Monotone g<GOAL>BddAbove (range (g ∘ f))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedLinearOrderedField 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → ‖x + y‖ = 2 → SameRay ℝ x y<GOAL>StrictConvexSpace ℝ E
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedLinearOrderedField 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → ‖x + y‖ = 2 → SameRay ℝ x y<VAR>x : E<VAR>hx : x ∈ sphere 0 1<VAR>y : E<VAR>hy : y ∈ sphere 0 1<VAR>h₂ : ‖x + y‖ = 2<GOAL>x = y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedLinearOrderedField 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → ‖x + y‖ = 2 → SameRay ℝ x y<VAR>x : E<VAR>hx : ‖x‖ = 1<VAR>y : E<VAR>hy : ‖y‖ = 1<VAR>h₂ : ‖x + y‖ = 2<GOAL>x = y
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<GOAL>(fun p => dist p.1 p.2) ∈ candidates X Y
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<GOAL>(∀ (x y : X), dist (inl x) (inl y) = dist x y) ∧ ∀ (x y : Y), dist (inr x) (inr y) = dist x y
<VAR>X✝ Y✝ Z✝ : Stonean<VAR>f✝ : X✝ ⟶ Z✝<VAR>i✝ : Y✝ ⟶ Z✝<VAR>hi✝ : OpenEmbedding ⇑i✝<VAR>X Y Z : Stonean<VAR>f : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>hi : OpenEmbedding ⇑i<VAR>x : (forget Stonean).obj X<VAR>h : x ∈ ⇑f ⁻¹' Set.range ⇑i<GOAL>(fst f hi ≫ f) ⟨x, h⟩ = (snd f hi ≫ i) ⟨x, h⟩
<VAR>X✝ Y✝ Z✝ : Stonean<VAR>f✝ : X✝ ⟶ Z✝<VAR>i✝ : Y✝ ⟶ Z✝<VAR>hi✝ : OpenEmbedding ⇑i✝<VAR>X Y Z : Stonean<VAR>f : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>hi : OpenEmbedding ⇑i<VAR>x : (forget Stonean).obj X<VAR>h✝ : x ∈ ⇑f ⁻¹' Set.range ⇑i<VAR>h : f x ∈ Set.range ⇑i<GOAL>(fst f hi ≫ f) ⟨x, h✝⟩ = (snd f hi ≫ i) ⟨x, h✝⟩
<VAR>X✝ Y✝ Z✝ : Stonean<VAR>f✝ : X✝ ⟶ Z✝<VAR>i✝ : Y✝ ⟶ Z✝<VAR>hi✝ : OpenEmbedding ⇑i✝<VAR>X Y Z : Stonean<VAR>f : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>hi : OpenEmbedding ⇑i<VAR>x : (forget Stonean).obj X<VAR>h : x ∈ ⇑f ⁻¹' Set.range ⇑i<VAR>y : (forget Stonean).obj Y<VAR>hy : i y = f x<GOAL>(fst f hi ≫ f) ⟨x, h⟩ = (snd f hi ≫ i) ⟨x, h⟩
<VAR>X✝ Y✝ Z✝ : Stonean<VAR>f✝ : X✝ ⟶ Z✝<VAR>i✝ : Y✝ ⟶ Z✝<VAR>hi✝ : OpenEmbedding ⇑i✝<VAR>X Y Z : Stonean<VAR>f : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>hi : OpenEmbedding ⇑i<VAR>x : (forget Stonean).obj X<VAR>h : x ∈ ⇑f ⁻¹' Set.range ⇑i<VAR>y : (forget Stonean).obj Y<VAR>hy : i y = f x<GOAL>f ({ toFun := Subtype.val, continuous_toFun := ⋯ } ⟨x, h⟩) = i ({ toFun := ⇑(Homeomorph.ofEmbedding ⇑i ⋯).symm ∘ Set.MapsTo.restrict (⇑f) (⇑f ⁻¹' Set.range ⇑i) (Set.range ⇑i) ⋯, continuous_toFun := ⋯ } ⟨x, h⟩)
<VAR>X✝ Y✝ Z✝ : Stonean<VAR>f✝ : X✝ ⟶ Z✝<VAR>i✝ : Y✝ ⟶ Z✝<VAR>hi✝ : OpenEmbedding ⇑i✝<VAR>X Y Z : Stonean<VAR>f : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>hi : OpenEmbedding ⇑i<VAR>x : (forget Stonean).obj X<VAR>h : x ∈ ⇑f ⁻¹' Set.range ⇑i<VAR>y : (forget Stonean).obj Y<VAR>hy : i y = f x<VAR>t : TopologicalSpace ↑(pullback f hi).toTop := inferInstance<GOAL>f x = i ({ toFun := ⇑(Homeomorph.ofEmbedding ⇑i ⋯).symm ∘ Set.MapsTo.restrict (⇑f) (⇑f ⁻¹' Set.range ⇑i) (Set.range ⇑i) ⋯, continuous_toFun := ⋯ } ⟨x, h⟩)
<VAR>X✝ Y✝ Z✝ : Stonean<VAR>f✝ : X✝ ⟶ Z✝<VAR>i✝ : Y✝ ⟶ Z✝<VAR>hi✝ : OpenEmbedding ⇑i✝<VAR>X Y Z : Stonean<VAR>f : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>hi : OpenEmbedding ⇑i<VAR>x : (forget Stonean).obj X<VAR>h : x ∈ ⇑f ⁻¹' Set.range ⇑i<VAR>y : (forget Stonean).obj Y<VAR>hy : i y = f x<VAR>t : TopologicalSpace ↑(pullback f hi).toTop := inferInstance<GOAL>i y = i ((⇑(Homeomorph.ofEmbedding ⇑i ⋯).symm ∘ Set.MapsTo.restrict (⇑f) (⇑f ⁻¹' Set.range ⇑i) (Set.range ⇑i) ⋯) ⟨x, h⟩)
<VAR>X✝ Y✝ Z✝ : Stonean<VAR>f✝ : X✝ ⟶ Z✝<VAR>i✝ : Y✝ ⟶ Z✝<VAR>hi✝ : OpenEmbedding ⇑i✝<VAR>X Y Z : Stonean<VAR>f : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>hi : OpenEmbedding ⇑i<VAR>x : (forget Stonean).obj X<VAR>h : x ∈ ⇑f ⁻¹' Set.range ⇑i<VAR>y : (forget Stonean).obj Y<VAR>hy : i y = f x<VAR>t : TopologicalSpace ↑(pullback f hi).toTop := inferInstance<GOAL>Continuous (⇑(Homeomorph.ofEmbedding ⇑i ⋯).symm ∘ Set.MapsTo.restrict (⇑f) (⇑f ⁻¹' Set.range ⇑i) (Set.range ⇑i) ⋯)
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝¹² : AddCommMonoid M<VAR>inst✝¹¹ : AddCommMonoid N<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module S N<VAR>inst✝⁴ : IsScalarTower R S N<VAR>f : M →ₗ[R] N<VAR>h✝ : IsBaseChange S f<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R P<VAR>inst✝¹ : AddCommMonoid Q<VAR>inst✝ : Module S Q<VAR>h : ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q] [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g<VAR>g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)<VAR>hg : ↑R g ∘ₗ f = ↑ULift.moduleEquiv.symm ∘ₗ (mk R S M) 1<VAR>f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))<VAR>f'' : S ⊗[R] M →ₗ[S] N := { toAddHom := f'.toAddHom, map_smul' := ⋯ }<GOAL>Function.Bijective ⇑f'
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝¹² : AddCommMonoid M<VAR>inst✝¹¹ : AddCommMonoid N<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module S N<VAR>inst✝⁴ : IsScalarTower R S N<VAR>f : M →ₗ[R] N<VAR>h✝ : IsBaseChange S f<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R P<VAR>inst✝¹ : AddCommMonoid Q<VAR>inst✝ : Module S Q<VAR>h : ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q] [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g<VAR>g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)<VAR>f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))<VAR>f'' : S ⊗[R] M →ₗ[S] N := { toAddHom := f'.toAddHom, map_smul' := ⋯ }<VAR>hg : ∀ (x : M), g (f x) = ↑ULift.moduleEquiv.symm (((mk R S M) 1) x)<GOAL>Function.Bijective ⇑f'
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>P : Subgroup G<VAR>hP : IsPGroup p ↥P<VAR>Q : Sylow p G<GOAL>Q ∈ fixedPoints (↥P) (Sylow p G) ↔ P ≤ ↑Q
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ✝ φ : R⟦X⟧<VAR>n : PartENat<VAR>h : ∀ (i : ℕ), ↑i < n → (coeff R i) φ = 0<GOAL>n ≤ φ.order
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ✝ φ : R⟦X⟧<VAR>h : ∀ (i : ℕ), ↑i < ⊤ → (coeff R i) φ = 0<GOAL>⊤ ≤ φ.order
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ✝ φ : R⟦X⟧<VAR>n✝ : ℕ<VAR>h : ∀ (i : ℕ), ↑i < ↑n✝ → (coeff R i) φ = 0<GOAL>↑n✝ ≤ φ.order
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>G : Type u_3<VAR>G₀ : Type u_4<VAR>R : Type u_5<VAR>K : Type u_6<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<VAR>g : G<VAR>h : ↥H<GOAL>ofConjAct (toConjAct.toMonoidHom g)⁻¹ * ↑h * (toConjAct.toMonoidHom g)⁻¹⁻¹ = g⁻¹ * ↑h * g
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>G : Type u_3<VAR>G₀ : Type u_4<VAR>R : Type u_5<VAR>K : Type u_6<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<VAR>g : G<VAR>h : ↥H<GOAL>ofConjAct (toConjAct.toMonoidHom g)⁻¹ * ↑h * toConjAct.toMonoidHom g = g⁻¹ * ↑h * g
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : CompleteSpace E<VAR>u : ℕ → E<VAR>hu : Summable fun x => ‖u x‖<GOAL>∃ a, Tendsto (fun n => ∑ i ∈ range n, u i) atTop (𝓝 a)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : CompleteSpace E<VAR>u : ℕ → E<VAR>hu : Summable fun x => ‖u x‖<GOAL>Summable fun n => dist (∑ i ∈ range n, u i) (∑ i ∈ range n.succ, u i)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommRing P<VAR>inst✝ : IsLocalization M S<VAR>a : R<VAR>ha : a ∈ ↑M<GOAL>(algebraMap R S) a ∈ IsUnit.submonoid S
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>hs : s₂ ⊆ s₁<VAR>ht : t₂ ⊆ t₁<VAR>hs₂ : s₂.Nonempty<VAR>ht₂ : t₂.Nonempty<GOAL>edgeDensity r s₂ t₂ - edgeDensity r s₁ t₁ ≤ 1 - ↑s₂.card / ↑s₁.card * (↑t₂.card / ↑t₁.card)