ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>Q : Type v<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>inst✝ : Fact (Function.Injective ⇑i)<VAR>h : Baer R Q<VAR>y : N<VAR>r : R<VAR>eq1 : r • y = 0<GOAL>(extendIdealTo i f h y) r = 0
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>Q : Type v<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>inst✝ : Fact (Function.Injective ⇑i)<VAR>h : Baer R Q<VAR>y : N<VAR>r : R<VAR>eq1 : r • y = 0<VAR>this : r ∈ ideal i f y<GOAL>(extendIdealTo i f h y) r = 0
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>Q : Type v<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>inst✝ : Fact (Function.Injective ⇑i)<VAR>h : Baer R Q<VAR>y : N<VAR>r : R<VAR>eq1 : r • y = 0<VAR>this : r ∈ ideal i f y<GOAL>(idealTo i f y) ⟨r, this⟩ = 0
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>Q : Type v<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>inst✝ : Fact (Function.Injective ⇑i)<VAR>h : Baer R Q<VAR>y : N<VAR>r : R<VAR>eq1 : r • y = 0<VAR>this : r ∈ ideal i f y<GOAL>↑(extensionOfMax i f).toLinearPMap ⟨r • y, ⋯⟩ = 0
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s✝ : Set α<VAR>F : ι → β → α<VAR>f : β → α<VAR>p : Filter ι<VAR>s : Set β<GOAL>TendstoUniformlyOn F f p s ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, dist (f x) (F n x) < ε
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s✝ : Set α<VAR>F : ι → β → α<VAR>f : β → α<VAR>p : Filter ι<VAR>s : Set β<VAR>H : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, dist (f x) (F n x) < ε<VAR>u : Set (α × α)<VAR>hu : u ∈ 𝓤 α<GOAL>∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ u
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε✝ ε₁ ε₂ : ℝ<VAR>s✝ : Set α<VAR>F : ι → β → α<VAR>f : β → α<VAR>p : Filter ι<VAR>s : Set β<VAR>H : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, dist (f x) (F n x) < ε<VAR>u : Set (α × α)<VAR>hu : u ∈ 𝓤 α<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ u<GOAL>∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ u
<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 : β<VAR>f : α → β<VAR>s : Finset α<VAR>t : Finset β<VAR>h : ∀ x ∈ s, f x ∈ t<VAR>a✝ : β<GOAL>a✝ ∈ filter (fun y => y ∈ image f s) t ↔ a✝ ∈ image f s
<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 : β<VAR>f : α → β<VAR>s : Finset α<VAR>t : Finset β<VAR>h : ∀ x ∈ s, f x ∈ t<VAR>a✝ : β<GOAL>∀ x ∈ s, f x = a✝ → a✝ ∈ t
<VAR>α β γ : Type u<VAR>t : Type u → Type u<VAR>inst✝³ : Traversable t<VAR>inst✝² : LawfulTraversable t<VAR>m : Type u → Type u<VAR>inst✝¹ : Monad m<VAR>inst✝ : LawfulMonad m<VAR>f : α → β → m β<VAR>x : β<VAR>xs : t α<GOAL>foldrm f x xs = (foldrM.ofFreeMonoid f) (FreeMonoid.ofList (toList xs)) x
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f g : Perm α<VAR>x y : α<GOAL>(swap x y).support = {x, y} ↔ x ≠ y
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f g : Perm α<VAR>x y : α<VAR>h : (swap x y).support = {x, y}<GOAL>x ≠ y
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f g : Perm α<VAR>x : α<VAR>h : (swap x x).support = {x, x}<GOAL>False
<VAR>α : Sort u_1<GOAL>⨅ x, 0 = 0
<VAR>α : Sort u_1<VAR>h✝ : IsEmpty α<GOAL>⨅ x, 0 = 0
<VAR>α : Sort u_1<VAR>h✝ : Nonempty α<GOAL>⨅ x, 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : μ.HaveLebesgueDecomposition ν<VAR>inst✝ : SFinite ν<VAR>hμν : μ ≪ ν<VAR>s : Set α<GOAL>∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν = μ s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁵ : SemilatticeInf α<VAR>inst✝⁴ : OrderTop α<VAR>s✝¹ s₁ s₂ : Finset β<VAR>f✝ g✝ : β → α<VAR>a : α<VAR>inst✝³ : SemilatticeInf β<VAR>inst✝² : OrderTop β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : InfTopHomClass F α β<VAR>f : F<VAR>s✝ : Finset ι<VAR>g : ι → α<VAR>i : ι<VAR>s : Finset ι<VAR>x✝ : i ∉ s<VAR>h : f (s.inf g) = s.inf (⇑f ∘ g)<GOAL>f ((cons i s x✝).inf g) = (cons i s x✝).inf (⇑f ∘ g)
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Monoid G<VAR>X✝ Y✝ : Action (Type u) (MonCat.of G)<VAR>f : X✝ ⟶ Y✝<VAR>X Y : Action (Type u) (MonCat.of G)<GOAL>(inv ((linearization k G).μ X Y)).hom = ↑(finsuppTensorFinsupp' k X.V Y.V).symm
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Monoid G<VAR>X✝ Y✝ : Action (Type u) (MonCat.of G)<VAR>f : X✝ ⟶ Y✝<VAR>X Y : Action (Type u) (MonCat.of G)<GOAL>inv ((Action.forget (ModuleCat k) (MonCat.of G)).map ((linearization k G).μ X Y)) = ↑(finsuppTensorFinsupp' k X.V Y.V).symm
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Monoid G<VAR>X✝ Y✝ : Action (Type u) (MonCat.of G)<VAR>f : X✝ ⟶ Y✝<VAR>X Y : Action (Type u) (MonCat.of G)<GOAL>(Action.forget (ModuleCat k) (MonCat.of G)).map ((linearization k G).μ X Y) ≫ ↑(finsuppTensorFinsupp' k X.V Y.V).symm = 𝟙 ((Action.forget (ModuleCat k) (MonCat.of G)).obj (MonoidalCategory.tensorObj ((linearization k G).obj X) ((linearization k G).obj Y)))
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>V1 : Type u_3<VAR>P1 : Type u_4<VAR>V2 : Type u_5<VAR>P2 : Type u_6<VAR>V3 : Type u_7<VAR>P3 : Type u_8<VAR>inst✝⁵ : CommRing k<VAR>inst✝⁴ : AddCommGroup V1<VAR>inst✝³ : AffineSpace V1 P1<VAR>inst✝² : AddCommGroup V2<VAR>inst✝¹ : Module k V1<VAR>inst✝ : Module k V2<VAR>c p : P1<GOAL>(homothety c 1) p = (id k P1) p
<VAR>a b : ℝ<VAR>nb : ℕ<VAR>num : ℤ<VAR>den : ℕ<VAR>pb : IsInt b (Int.negOfNat nb)<VAR>pe' : IsRat (a ^ Int.negOfNat nb) num den<GOAL>IsRat (a ^ b) num den
<VAR>J : Type w<VAR>K : Type u_1<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>f : J → C<VAR>inst✝ : HasBiproduct f<VAR>j : J<GOAL>ι f j ≫ π f j = 𝟙 (f j)
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝ : TopologicalSpace M<VAR>s : Set H<VAR>hs : IsOpen s<GOAL>PartialHomeomorph.ofSet s hs ∈ contDiffGroupoid ⊤ I ⊓ { property := fun f s => AnalyticOn 𝕜 (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ interior (range ↑I)) ∧ ↑I ∘ f ∘ ↑I.symm '' (↑I.symm ⁻¹' s ∩ interior (range ↑I)) ⊆ interior (range ↑I), comp := ⋯, id_mem := ⋯, locality := ⋯, congr := ⋯ }.groupoid
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝ : TopologicalSpace M<VAR>s : Set H<VAR>hs : IsOpen s<GOAL>PartialHomeomorph.ofSet s hs ∈ { property := fun f s => AnalyticOn 𝕜 (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ interior (range ↑I)) ∧ ↑I ∘ f ∘ ↑I.symm '' (↑I.symm ⁻¹' s ∩ interior (range ↑I)) ⊆ interior (range ↑I), comp := ⋯, id_mem := ⋯, locality := ⋯, congr := ⋯ }.groupoid.members
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝ : TopologicalSpace M<VAR>s : Set H<VAR>hs : IsOpen s<GOAL>{ property := fun f s => AnalyticOn 𝕜 (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ interior (range ↑I)) ∧ ↑I ∘ f ∘ ↑I.symm '' (↑I.symm ⁻¹' s ∩ interior (range ↑I)) ⊆ interior (range ↑I), comp := ⋯, id_mem := ⋯, locality := ⋯, congr := ⋯ }.property (↑(PartialHomeomorph.ofSet s hs)) (PartialHomeomorph.ofSet s hs).source ∧ { property := fun f s => AnalyticOn 𝕜 (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ interior (range ↑I)) ∧ ↑I ∘ f ∘ ↑I.symm '' (↑I.symm ⁻¹' s ∩ interior (range ↑I)) ⊆ interior (range ↑I), comp := ⋯, id_mem := ⋯, locality := ⋯, congr := ⋯ }.property (↑(PartialHomeomorph.ofSet s hs).symm) (PartialHomeomorph.ofSet s hs).target
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝ : TopologicalSpace M<VAR>s : Set H<VAR>hs : IsOpen s<GOAL>AnalyticOn 𝕜 (↑I ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ interior (range ↑I)) ∧ ↑I ∘ ↑I.symm '' (↑I.symm ⁻¹' s ∩ interior (range ↑I)) ⊆ interior (range ↑I)
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>s✝ t✝ : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<GOAL>(s \ t).dens + (s ∩ t).dens = s.dens
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Ring B<VAR>inst✝⁴ : Algebra R B<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>f g : M →ₗ[R] N<VAR>x✝ : M<GOAL>((AlgebraTensorModule.curry (baseChange A (f - g))) 1) x✝ = ((AlgebraTensorModule.curry (baseChange A f - baseChange A g)) 1) x✝
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : Unique ι<GOAL>stdSimplex 𝕜 ι = {fun x => 1}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : Unique ι<GOAL>∀ x ∈ stdSimplex 𝕜 ι, x = fun x => 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : Unique ι<VAR>f : ι → 𝕜<VAR>hf : ∑ x : ι, f x = 1<GOAL>f = fun x => 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : Unique ι<VAR>f : ι → 𝕜<VAR>hf : f default = 1<GOAL>f = fun x => 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>f : E ≃ₗᵢ[𝕜] F<VAR>U V : Submodule 𝕜 E<VAR>h : Submodule.map f U ⟂ Submodule.map f V<GOAL>U ⟂ V
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>f : E ≃ₗᵢ[𝕜] F<VAR>U V : Submodule 𝕜 E<VAR>h : Submodule.map f U ⟂ Submodule.map f V<VAR>hf : ∀ (p : Submodule 𝕜 E), Submodule.comap f.toLinearIsometry (Submodule.map f p) = p<GOAL>U ⟂ V
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>m : M<GOAL>(fromLocalizedModule S f) (LocalizedModule.mk m 1) = f m
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x✝ y✝ : R<VAR>inst✝ : CommSemiring R<VAR>x y : R<GOAL>IsNilpotent x ↔ ∀ (J : Ideal R), J.IsPrime → x ∈ J
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x✝ y✝ : R<VAR>inst✝ : CommSemiring R<VAR>x y : R<GOAL>(∀ p ∈ {J | J.IsPrime}, x ∈ p) ↔ ∀ (J : Ideal R), J.IsPrime → x ∈ J
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>n : ℕ<VAR>f : Fin n → α → σ<VAR>hf : ∀ (i : Fin n), Primrec (f i)<GOAL>Primrec fun a => (Vector.ofFn fun i => f i a).toList
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝³ : CommMonoid M<VAR>inst✝² : CommMonoid N<VAR>inst✝¹ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>M₀ : Type u_7<VAR>inst✝ : CancelCommMonoidWithZero M₀<VAR>n : ℕ<VAR>ζ : M₀<VAR>hζ : IsPrimitiveRoot ζ n<VAR>α : M₀<VAR>hα : α ≠ 0<VAR>i : ℕ<VAR>hi : i ∈ ↑(range n)<VAR>j : ℕ<VAR>hj : j ∈ ↑(range n)<VAR>e : (fun x => ζ ^ x * α) i = (fun x => ζ ^ x * α) j<GOAL>(fun x => ζ ^ x) i = (fun x => ζ ^ x) j
<VAR>x✝ y✝ z : ℝ<VAR>n : ℕ<VAR>x : ℝ<VAR>hx : 0 < x<VAR>y : ℝ<GOAL>log (x ^ y) = y * log x
<VAR>x✝ y✝ z : ℝ<VAR>n : ℕ<VAR>x : ℝ<VAR>hx : 0 < x<VAR>y : ℝ<GOAL>rexp (log (x ^ y)) = rexp (y * log x)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s1 s2 : AffineSubspace k P<VAR>h : s1 < s2<VAR>p : P<VAR>hp : p ∈ ↑s1<GOAL>s1.direction < s2.direction
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s1 s2 : AffineSubspace k P<VAR>h : s1 ≤ s2 ∧ ∃ p ∈ s2, p ∉ s1<VAR>p : P<VAR>hp : p ∈ ↑s1<GOAL>s1.direction < s2.direction
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s1 s2 : AffineSubspace k P<VAR>p : P<VAR>hp : p ∈ ↑s1<VAR>hle : s1 ≤ s2<VAR>p2 : P<VAR>hp2 : p2 ∈ s2<VAR>hp2s1 : p2 ∉ s1<GOAL>s1.direction < s2.direction
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s1 s2 : AffineSubspace k P<VAR>p : P<VAR>hp : p ∈ ↑s1<VAR>hle : s1 ≤ s2<VAR>p2 : P<VAR>hp2 : p2 ∈ s2<VAR>hp2s1 : p2 ∉ s1<GOAL>s1.direction ≤ s2.direction ∧ ∃ x ∈ s2.direction, x ∉ s1.direction
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s1 s2 : AffineSubspace k P<VAR>p : P<VAR>hp : p ∈ ↑s1<VAR>hle : s1 ≤ s2<VAR>p2 : P<VAR>hp2 : p2 ∈ s2<VAR>hp2s1 : p2 ∉ s1<GOAL>p2 -ᵥ p ∉ s1.direction
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s1 s2 : AffineSubspace k P<VAR>p : P<VAR>hp : p ∈ ↑s1<VAR>hle : s1 ≤ s2<VAR>p2 : P<VAR>hp2 : p2 ∈ s2<VAR>hp2s1 : p2 ∉ s1<VAR>hm : p2 -ᵥ p ∈ s1.direction<GOAL>False
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s1 s2 : AffineSubspace k P<VAR>p : P<VAR>hp : p ∈ ↑s1<VAR>hle : s1 ≤ s2<VAR>p2 : P<VAR>hp2 : p2 ∈ s2<VAR>hp2s1 : p2 ∉ s1<VAR>hm : p2 ∈ s1<GOAL>False
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹¹ : Category.{u_3, u_1} C<VAR>inst✝¹⁰ : Category.{u_4, u_2} D<VAR>inst✝⁹ : HasZeroMorphisms C<VAR>inst✝⁸ : HasZeroMorphisms D<VAR>S : ShortComplex C<VAR>h₁ : S.LeftHomologyData<VAR>h₂ : S.RightHomologyData<VAR>F : C ⥤ D<VAR>inst✝⁷ : F.PreservesZeroMorphisms<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hl₁ : S₁.LeftHomologyData<VAR>hr₁ : S₁.RightHomologyData<VAR>hl₂ : S₂.LeftHomologyData<VAR>hr₂ : S₂.RightHomologyData<VAR>ψl : LeftHomologyMapData φ hl₁ hl₂<VAR>ψr : RightHomologyMapData φ hr₁ hr₂<VAR>inst✝⁶ : S₁.HasHomology<VAR>inst✝⁵ : S₂.HasHomology<VAR>inst✝⁴ : (F.mapShortComplex.obj S₁).HasHomology<VAR>inst✝³ : (F.mapShortComplex.obj S₂).HasHomology<VAR>inst✝² : F.PreservesRightHomologyOf S₁<VAR>inst✝¹ : F.PreservesRightHomologyOf S₂<VAR>inst✝ : F.ReflectsIsomorphisms<VAR>γ : RightHomologyMapData φ S₁.rightHomologyData S₂.rightHomologyData<GOAL>QuasiIso (F.mapShortComplex.map φ) ↔ QuasiIso φ
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹¹ : Category.{u_3, u_1} C<VAR>inst✝¹⁰ : Category.{u_4, u_2} D<VAR>inst✝⁹ : HasZeroMorphisms C<VAR>inst✝⁸ : HasZeroMorphisms D<VAR>S : ShortComplex C<VAR>h₁ : S.LeftHomologyData<VAR>h₂ : S.RightHomologyData<VAR>F : C ⥤ D<VAR>inst✝⁷ : F.PreservesZeroMorphisms<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hl₁ : S₁.LeftHomologyData<VAR>hr₁ : S₁.RightHomologyData<VAR>hl₂ : S₂.LeftHomologyData<VAR>hr₂ : S₂.RightHomologyData<VAR>ψl : LeftHomologyMapData φ hl₁ hl₂<VAR>ψr : RightHomologyMapData φ hr₁ hr₂<VAR>inst✝⁶ : S₁.HasHomology<VAR>inst✝⁵ : S₂.HasHomology<VAR>inst✝⁴ : (F.mapShortComplex.obj S₁).HasHomology<VAR>inst✝³ : (F.mapShortComplex.obj S₂).HasHomology<VAR>inst✝² : F.PreservesRightHomologyOf S₁<VAR>inst✝¹ : F.PreservesRightHomologyOf S₂<VAR>inst✝ : F.ReflectsIsomorphisms<VAR>γ : RightHomologyMapData φ S₁.rightHomologyData S₂.rightHomologyData<GOAL>IsIso (F.map γ.φH) ↔ IsIso γ.φH
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K✝ : Set (E →L[𝕜] F)<VAR>r s t : ℝ<VAR>hf : Continuous (Function.uncurry f)<VAR>K : Set (E →L[𝕜] F)<GOAL>IsOpen (⋃ L ∈ K, {p | p.2 ∈ A (f p.1) L r t ∧ p.2 ∈ A (f p.1) L s t})
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K✝ : Set (E →L[𝕜] F)<VAR>r s t : ℝ<VAR>hf : Continuous (Function.uncurry f)<VAR>K : Set (E →L[𝕜] F)<VAR>L : E →L[𝕜] F<VAR>x✝ : L ∈ K<GOAL>IsOpen {p | p.2 ∈ A (f p.1) L r t ∧ p.2 ∈ A (f p.1) L s t}
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y x : V<GOAL>arccos (⟪x, 0⟫_ℝ / (‖x‖ * ‖0‖)) = π / 2
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<VAR>a : (_ : Fin n) × Fin n<GOAL>a ∈ finPairsLT n ↔ a.snd < a.fst
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>y : ℝ≥0∞<VAR>hy : 1 < y<VAR>h'y : y ≠ ⊤<VAR>x : ℝ≥0∞<GOAL>x ∈ Ioo 0 ⊤ ↔ x ∈ ⋃ n, Ico (y ^ n) (y ^ (n + 1))
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>y : ℝ≥0∞<VAR>hy : 1 < y<VAR>h'y : y ≠ ⊤<VAR>x : ℝ≥0∞<GOAL>0 < x ∧ x < ⊤ ↔ ∃ i, y ^ i ≤ x ∧ x < y ^ (i + 1)
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<GOAL>#((n : ℕ) × L.BoundedFormula α n) ≤ max ℵ₀ (lift.{max u v, u'} #α + lift.{u', max u v} L.card)
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<GOAL>lift.{max (max u' v) u, max (max u' v) u} #(List BoundedFormula.encoding.Γ) ≤ lift.{max (max u u') v, max (max u u') v} (max ℵ₀ (lift.{max u v, u'} #α + lift.{u', max u v} L.card))
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<GOAL>lift.{max (max u u') v, max (max u u') v} #((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ) ≤ max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card)) ∧ ℵ₀ ≤ max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card))
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<GOAL>lift.{max (max u u') v, max (max u u') v} #((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ) ≤ max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card))
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<GOAL>lift.{max (max u u') v, max (max u u') v} (lift.{v, max u u'} (ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))) + lift.{max u u', v} (lift.{0, v} #((n : ℕ) × L.Relations n) + lift.{v, 0} ℵ₀)) ≤ max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card))
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<GOAL>ℵ₀ + (lift.{max (max u v) (max u u') v, u'} #α + lift.{max (max u' v) (max u u') v, u} #((i : ℕ) × L.Functions i)) + (lift.{max (max u u') v, v} #((n : ℕ) × L.Relations n) + ℵ₀) ≤ max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>f : α → β → ℝ≥0∞<VAR>κ : Kernel α β<VAR>inst✝ : IsSFiniteKernel κ<VAR>hf : ¬Measurable (Function.uncurry f)<GOAL>κ.withDensity f = 0
<VAR>C : Type u₁<VAR>inst✝⁸ : Category.{v₁, u₁} C<VAR>W : MorphismProperty C<VAR>D : Type u₂<VAR>inst✝⁷ : Category.{v₂, u₂} D<VAR>D' : Type u₃<VAR>inst✝⁶ : Category.{v₃, u₃} D'<VAR>X Y Z T : C<VAR>inst✝⁵ : HasSmallLocalizedHom W X Y<VAR>inst✝⁴ : HasSmallLocalizedHom W X Z<VAR>inst✝³ : HasSmallLocalizedHom W X T<VAR>inst✝² : HasSmallLocalizedHom W Y Z<VAR>inst✝¹ : HasSmallLocalizedHom W Y T<VAR>inst✝ : HasSmallLocalizedHom W Z T<VAR>α : SmallHom W X Y<VAR>β : SmallHom W Y Z<VAR>γ : SmallHom W Z T<GOAL>(α.comp β).comp γ = α.comp (β.comp γ)
<VAR>C : Type u₁<VAR>inst✝⁸ : Category.{v₁, u₁} C<VAR>W : MorphismProperty C<VAR>D : Type u₂<VAR>inst✝⁷ : Category.{v₂, u₂} D<VAR>D' : Type u₃<VAR>inst✝⁶ : Category.{v₃, u₃} D'<VAR>X Y Z T : C<VAR>inst✝⁵ : HasSmallLocalizedHom W X Y<VAR>inst✝⁴ : HasSmallLocalizedHom W X Z<VAR>inst✝³ : HasSmallLocalizedHom W X T<VAR>inst✝² : HasSmallLocalizedHom W Y Z<VAR>inst✝¹ : HasSmallLocalizedHom W Y T<VAR>inst✝ : HasSmallLocalizedHom W Z T<VAR>α : SmallHom W X Y<VAR>β : SmallHom W Y Z<VAR>γ : SmallHom W Z T<GOAL>(equiv W W.Q) ((α.comp β).comp γ) = (equiv W W.Q) (α.comp (β.comp γ))
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝² : MetricSpace X<VAR>inst✝¹ : MetricSpace Y<VAR>Φ✝ : Z → X<VAR>Ψ✝ : Z → Y<VAR>ε✝ : ℝ<VAR>inst✝ : Nonempty Z<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε<VAR>x : X<VAR>y : Y<VAR>z : X<GOAL>glueDist Φ Ψ ε (Sum.inl x) (Sum.inl z) ≤ glueDist Φ Ψ ε (Sum.inl x) (Sum.inr y) + glueDist Φ Ψ ε (Sum.inr y) (Sum.inl z)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝² : MetricSpace X<VAR>inst✝¹ : MetricSpace Y<VAR>Φ✝ : Z → X<VAR>Ψ✝ : Z → Y<VAR>ε✝ : ℝ<VAR>inst✝ : Nonempty Z<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε<VAR>x : X<VAR>y : Y<VAR>z : X<GOAL>dist x z ≤ (⨅ p, dist x (Φ p) + dist y (Ψ p)) + ((⨅ p, dist z (Φ p) + dist y (Ψ p)) + (ε + ε))
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝² : MetricSpace X<VAR>inst✝¹ : MetricSpace Y<VAR>Φ✝ : Z → X<VAR>Ψ✝ : Z → Y<VAR>ε✝ : ℝ<VAR>inst✝ : Nonempty Z<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε<VAR>x : X<VAR>y : Y<VAR>z : X<VAR>p : Z<GOAL>dist x z ≤ dist x (Φ p) + dist y (Ψ p) + ((⨅ p, dist z (Φ p) + dist y (Ψ p)) + (ε + ε))