ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s✝ t : Set α<VAR>a✝ b a : α<VAR>s : Set α<GOAL>upperBounds (insert a s) = Ici a ∩ upperBounds s
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>hsp : ⊤ ≤ (span 𝕜 (Set.range v)).topologicalClosure<GOAL>(fun i => (HilbertBasis.mk hv hsp).repr.symm (lp.single 2 i 1)) = v
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l l' : List α<VAR>h✝ : l <+~ l'<VAR>xs : List α<VAR>hp : xs ~ l<VAR>h : xs <+ l'<GOAL>List.filter p l <+~ List.filter p l'
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>f : α → α<VAR>a : α<GOAL>iterate f a = a :: iterate f (f a)
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>f : α → α<VAR>a : α<GOAL>(iterate f a).head :: (iterate f a).tail = a :: iterate f (f a)
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>f : α → α<VAR>a : α<GOAL>(iterate f a).head :: iterate f (f a) = a :: iterate f (f a)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g : G<VAR>s t : Set α<VAR>a b : α<GOAL>b ∈ doset a s t ↔ ∃ x ∈ s, ∃ y ∈ t, b = x * a * y
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>a✝ : α<VAR>b : β<VAR>s✝¹ : Multiset α<VAR>t✝ : Multiset β<VAR>s✝ : Multiset α<VAR>a : α<VAR>s : Multiset α<VAR>IH : ∀ (t u : Multiset β), s ×ˢ (t + u) = s ×ˢ t + s ×ˢ u<VAR>t u : Multiset β<GOAL>(a ::ₘ s) ×ˢ (t + u) = (a ::ₘ s) ×ˢ t + (a ::ₘ s) ×ˢ u
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>a✝ : α<VAR>b : β<VAR>s✝¹ : Multiset α<VAR>t✝ : Multiset β<VAR>s✝ : Multiset α<VAR>a : α<VAR>s : Multiset α<VAR>IH : ∀ (t u : Multiset β), s ×ˢ (t + u) = s ×ˢ t + s ×ˢ u<VAR>t u : Multiset β<GOAL>map (Prod.mk a) (t + u) + (s ×ˢ t + s ×ˢ u) = (a ::ₘ s) ×ˢ t + (a ::ₘ s) ×ˢ u
<VAR>d✝ d : ℤ<VAR>hd : d ≤ 0<VAR>z : ℤ√d<GOAL>z.norm = 1 ↔ IsUnit z
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝³ : MonoidalCategory C✝<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : MonoidalCategory C<VAR>U V✝ W✝ X✝ Y✝ Z✝ V W X Y Z : C<VAR>f : V ⟶ W<VAR>inst✝ : IsIso f<VAR>g : X ⟶ Y<VAR>h : Y ⟶ Z<GOAL>(g ⊗ f) ≫ (h ⊗ inv f) = (g ⊗ 𝟙 V) ≫ (h ⊗ 𝟙 V)
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝³ : MonoidalCategory C✝<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : MonoidalCategory C<VAR>U V✝ W✝ X✝ Y✝ Z✝ V W X Y Z : C<VAR>f : V ⟶ W<VAR>inst✝ : IsIso f<VAR>g : X ⟶ Y<VAR>h : Y ⟶ Z<GOAL>g ≫ h ⊗ 𝟙 V = (g ⊗ 𝟙 V) ≫ (h ⊗ 𝟙 V)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : SimplicialCategory C<VAR>K K' K'' : C<VAR>f : K ⟶ K'<VAR>f' : K' ⟶ K''<VAR>L : C<GOAL>(λ_ (sHom K'' L)).inv ≫ (homEquiv K K'') (f ≫ f') ▷ sHom K'' L ≫ sHomComp K K'' L = ((λ_ (sHom K'' L)).inv ≫ (homEquiv K' K'') f' ▷ sHom K'' L ≫ sHomComp K' K'' L) ≫ (λ_ (sHom K' L)).inv ≫ (homEquiv K K') f ▷ sHom K' L ≫ sHomComp K K' L
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : SimplicialCategory C<VAR>K K' K'' : C<VAR>f : K ⟶ K'<VAR>f' : K' ⟶ K''<VAR>L : C<GOAL>(λ_ (sHom K'' L)).inv ≫ (λ_ (𝟙_ SSet ⊗ sHom K'' L)).inv ≫ (α_ (𝟙_ SSet) (𝟙_ SSet) (sHom K'' L)).inv ≫ ((homEquiv K K') f ⊗ (homEquiv K' K'') f') ▷ sHom K'' L ≫ (α_ (EnrichedCategory.Hom K K') (EnrichedCategory.Hom K' K'') (EnrichedCategory.Hom K'' L)).hom ≫ EnrichedCategory.Hom K K' ◁ eComp SSet K' K'' L ≫ eComp SSet K K' L = (λ_ (sHom K'' L)).inv ≫ (homEquiv K' K'') f' ▷ sHom K'' L ≫ sHomComp K' K'' L ≫ (λ_ (sHom K' L)).inv ≫ (homEquiv K K') f ▷ sHom K' L ≫ sHomComp K K' L
<VAR>x y : ZFSet<VAR>H : {x} = {y}<VAR>this : ⋃₀ {x} = ⋃₀ {y} := congr_arg sUnion H<GOAL>x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>h_mono : Monotone f<VAR>h_surj : Surjective f<VAR>a b : α<VAR>hab : a ≤ b<VAR>p : β<VAR>hp : p ∈ Icc (f a) (f b)<GOAL>p ∈ f '' Icc a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>h_mono : Monotone f<VAR>h_surj : Surjective f<VAR>a b : α<VAR>hab : a ≤ b<VAR>hp : f a ∈ Icc (f a) (f b)<GOAL>f a ∈ f '' Icc a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>h_mono : Monotone f<VAR>h_surj : Surjective f<VAR>a b : α<VAR>hab : a ≤ b<VAR>hp : f b ∈ Icc (f a) (f b)<GOAL>f b ∈ f '' Icc a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>h_mono : Monotone f<VAR>h_surj : Surjective f<VAR>a b : α<VAR>hab : a ≤ b<VAR>p : β<VAR>hp : p ∈ Icc (f a) (f b)<VAR>hp' : p ∈ Ioo (f a) (f b)<GOAL>p ∈ f '' Icc a b
<VAR>l r : List Char<VAR>it : Iterator<VAR>h : ValidFor l r it<GOAL>it.i = it.s.endPos ↔ r = []
<VAR>l r : List Char<VAR>it : Iterator<VAR>h : ValidFor l r it<GOAL>utf8Len l = utf8Len l + utf8Len r ↔ r = []
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : Module R S<VAR>inst✝² : Module S A<VAR>inst✝¹ : Module R A<VAR>inst✝ : IsScalarTower R S A<VAR>ι : Type v₁<VAR>b : ι → S<VAR>ι' : Type w₁<VAR>c : ι' → A<VAR>hb : LinearIndependent R b<VAR>hc : LinearIndependent S c<GOAL>LinearIndependent R fun p => b p.1 • c p.2
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : Module R S<VAR>inst✝² : Module S A<VAR>inst✝¹ : Module R A<VAR>inst✝ : IsScalarTower R S A<VAR>ι : Type v₁<VAR>b : ι → S<VAR>ι' : Type w₁<VAR>c : ι' → A<VAR>hb : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • b i = 0 → ∀ i ∈ s, g i = 0<VAR>hc : ∀ (s : Finset ι') (g : ι' → S), ∑ i ∈ s, g i • c i = 0 → ∀ i ∈ s, g i = 0<GOAL>LinearIndependent R fun p => b p.1 • c p.2
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : Module R S<VAR>inst✝² : Module S A<VAR>inst✝¹ : Module R A<VAR>inst✝ : IsScalarTower R S A<VAR>ι : Type v₁<VAR>b : ι → S<VAR>ι' : Type w₁<VAR>c : ι' → A<VAR>hb : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • b i = 0 → ∀ i ∈ s, g i = 0<VAR>hc : ∀ (s : Finset ι') (g : ι' → S), ∑ i ∈ s, g i • c i = 0 → ∀ i ∈ s, g i = 0<GOAL>∀ (s : Finset (ι × ι')) (g : ι × ι' → R), (∀ i ∉ s, g i = 0) → ∑ i ∈ s, g i • b i.1 • c i.2 = 0 → ∀ (i : ι × ι'), g i = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ l₃ : List α<VAR>a b : α<VAR>m n : ℕ<VAR>s : List α<VAR>this : s = [] ↔ s <+: []<GOAL>s ∈ [].inits ↔ s <+: []
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ l₃ : List α<VAR>a✝ b : α<VAR>m n : ℕ<VAR>s✝ : List α<VAR>a : α<VAR>t : List α<VAR>o : s✝ = [] ∨ ∃ l, l ∈ t.inits ∧ a :: l = s✝<VAR>s r : List α<VAR>hr : r ∈ t.inits<VAR>hs : a :: r = s<GOAL>s <+: a :: t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ l₃ : List α<VAR>a✝ b : α<VAR>m n : ℕ<VAR>s✝¹ : List α<VAR>a : α<VAR>t : List α<VAR>o : s✝¹ = [] ∨ ∃ l, l ∈ t.inits ∧ a :: l = s✝¹<VAR>s✝ r : List α<VAR>hr : r ∈ t.inits<VAR>hs : a :: r = s✝<VAR>s : List α<VAR>ht : r ++ s = t<GOAL>s✝ <+: a :: t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ l₃ : List α<VAR>a✝ b✝ : α<VAR>m n : ℕ<VAR>s✝ : List α<VAR>a : α<VAR>t : List α<VAR>mi : s✝ <+: a :: t<VAR>b : α<VAR>s r : List α<VAR>hr : b :: s ++ r = a :: t<VAR>ba : b = a<VAR>st : s ++ r = t<GOAL>∃ l, l ∈ t.inits ∧ a :: l = a :: s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>p q : Set α → Prop<VAR>U s : Set α<VAR>ε r✝ : ℝ≥0∞<VAR>X : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : SigmaCompactSpace X<VAR>inst✝ : MeasurableSpace X<VAR>μ : Measure X<VAR>F : Set X<VAR>hF : IsClosed F<VAR>r : ℝ≥0∞<VAR>hr : r < μ F<VAR>B : ℕ → Set X := compactCovering X<GOAL>∃ K ⊆ F, IsCompact K ∧ r < μ K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>p q : Set α → Prop<VAR>U s : Set α<VAR>ε r✝ : ℝ≥0∞<VAR>X : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : SigmaCompactSpace X<VAR>inst✝ : MeasurableSpace X<VAR>μ : Measure X<VAR>F : Set X<VAR>hF : IsClosed F<VAR>r : ℝ≥0∞<VAR>hr : r < μ F<VAR>B : ℕ → Set X := compactCovering X<VAR>hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)<GOAL>∃ K ⊆ F, IsCompact K ∧ r < μ K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>p q : Set α → Prop<VAR>U s : Set α<VAR>ε r✝ : ℝ≥0∞<VAR>X : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : SigmaCompactSpace X<VAR>inst✝ : MeasurableSpace X<VAR>μ : Measure X<VAR>F : Set X<VAR>hF : IsClosed F<VAR>r : ℝ≥0∞<VAR>hr : r < μ F<VAR>B : ℕ → Set X := compactCovering X<VAR>hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)<VAR>hBU : ⋃ n, F ∩ B n = F<GOAL>∃ K ⊆ F, IsCompact K ∧ r < μ K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>p q : Set α → Prop<VAR>U s : Set α<VAR>ε r✝ : ℝ≥0∞<VAR>X : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : SigmaCompactSpace X<VAR>inst✝ : MeasurableSpace X<VAR>μ : Measure X<VAR>F : Set X<VAR>hF : IsClosed F<VAR>r : ℝ≥0∞<VAR>hr : r < μ F<VAR>B : ℕ → Set X := compactCovering X<VAR>hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)<VAR>hBU : ⋃ n, F ∩ B n = F<VAR>this : μ F = ⨆ n, μ (F ∩ B n)<GOAL>∃ K ⊆ F, IsCompact K ∧ r < μ K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>p q : Set α → Prop<VAR>U s : Set α<VAR>ε r✝ : ℝ≥0∞<VAR>X : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : SigmaCompactSpace X<VAR>inst✝ : MeasurableSpace X<VAR>μ : Measure X<VAR>F : Set X<VAR>hF : IsClosed F<VAR>r : ℝ≥0∞<VAR>B : ℕ → Set X := compactCovering X<VAR>hr : r < ⨆ n, μ (F ∩ B n)<VAR>hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)<VAR>hBU : ⋃ n, F ∩ B n = F<VAR>this : μ F = ⨆ n, μ (F ∩ B n)<GOAL>∃ K ⊆ F, IsCompact K ∧ r < μ K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>p q : Set α → Prop<VAR>U s : Set α<VAR>ε r✝ : ℝ≥0∞<VAR>X : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : SigmaCompactSpace X<VAR>inst✝ : MeasurableSpace X<VAR>μ : Measure X<VAR>F : Set X<VAR>hF : IsClosed F<VAR>r : ℝ≥0∞<VAR>B : ℕ → Set X := compactCovering X<VAR>hr : r < ⨆ n, μ (F ∩ B n)<VAR>hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)<VAR>hBU : ⋃ n, F ∩ B n = F<VAR>this : μ F = ⨆ n, μ (F ∩ B n)<VAR>n : ℕ<VAR>hn : r < μ (F ∩ B n)<GOAL>∃ K ⊆ F, IsCompact K ∧ r < μ K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : LinearOrder α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : LinearOrder β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderTopology β<VAR>inst✝ : DenselyOrdered β<VAR>f : α → β<VAR>h_mono : Monotone f<VAR>h_dense : DenseRange f<VAR>a : α<GOAL>closure (f '' univ) ∈ 𝓝 (f a)
<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>x y✝ : E<VAR>s t✝ : Set E<VAR>t : Set F<VAR>y : F<VAR>hs : UniqueDiffWithinAt 𝕜 s x<VAR>ht : UniqueDiffWithinAt 𝕜 t y<GOAL>UniqueDiffWithinAt 𝕜 (s ×ˢ t) (x, y)
<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>x y✝ : E<VAR>s t✝ : Set E<VAR>t : Set F<VAR>y : F<VAR>hs : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) ∧ x ∈ closure s<VAR>ht : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t y)) ∧ y ∈ closure t<GOAL>Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y))) ∧ (x, y) ∈ closure (s ×ˢ t)
<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>x y✝ : E<VAR>s t✝ : Set E<VAR>t : Set F<VAR>y : F<VAR>hs : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) ∧ x ∈ closure s<VAR>ht : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t y)) ∧ y ∈ closure t<GOAL>Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y))) ∧ (x, y) ∈ closure s ×ˢ closure t
<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>x y✝ : E<VAR>s t✝ : Set E<VAR>t : Set F<VAR>y : F<VAR>hs : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) ∧ x ∈ closure s<VAR>ht : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t y)) ∧ y ∈ closure t<GOAL>Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y)))
<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>x y✝ : E<VAR>s t✝ : Set E<VAR>t : Set F<VAR>y : F<VAR>hs : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) ∧ x ∈ closure s<VAR>ht : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t y)) ∧ y ∈ closure t<VAR>this : Submodule.span 𝕜 (⇑(LinearMap.inl 𝕜 E F) '' tangentConeAt 𝕜 s x ∪ ⇑(LinearMap.inr 𝕜 E F) '' tangentConeAt 𝕜 t y) ≤ Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y))<GOAL>Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y)))
<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>x y✝ : E<VAR>s t✝ : Set E<VAR>t : Set F<VAR>y : F<VAR>hs : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) ∧ x ∈ closure s<VAR>ht : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t y)) ∧ y ∈ closure t<VAR>this : ∀ ⦃x_1 : E × F⦄, x_1 ∈ (Submodule.span 𝕜 (tangentConeAt 𝕜 s x)).prod (Submodule.span 𝕜 (tangentConeAt 𝕜 t y)) → x_1 ∈ Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y))<GOAL>Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s ×ˢ t) (x, y)))
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hI : M.Indep I<VAR>heI : e ∉ I<VAR>he : autoParam (e ∈ M.E) _auto✝<GOAL>e ∉ M.closure I ↔ M.Indep (insert e I)
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : PointClass F<VAR>a✝ : Fin 3 → F<VAR>hP : W.NonsingularLift (Quot.mk Setoid.r a✝)<GOAL>W.NonsingularLift (W.negMap (Quot.mk Setoid.r a✝))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y z : E<VAR>δ ε : ℝ<VAR>hε : 0 ≤ ε<VAR>hδ : 0 < δ<VAR>a b : E<GOAL>Metric.closedBall a ε + Metric.ball b δ = Metric.ball (a + b) (ε + δ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n n' m : ℕ<VAR>s✝ : Sym α n<VAR>a✝ b : α<VAR>inst✝ : DecidableEq α<VAR>a x : α<VAR>i : Fin (n + 1)<VAR>s : Sym α (n - ↑i)<VAR>hx : x ≠ a<GOAL>count x ↑(fill a i s) = count x ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n n' m : ℕ<VAR>s✝ : Sym α n<VAR>a✝ b : α<VAR>inst✝ : DecidableEq α<VAR>a x : α<VAR>i : Fin (n + 1)<VAR>s : Sym α (n - ↑i)<VAR>hx : x ≠ a<GOAL>x ∉ Multiset.replicate (↑i) a
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<VAR>h : l.length = 0<GOAL>l.rotate n = l.rotate' n
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<VAR>h : ¬l.length = 0<GOAL>l.rotate n = l.rotate' n
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<VAR>h : ¬l.length = 0<GOAL>l.rotate n = drop (n % l.length) l ++ take (n % l.length) l
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>M : Type w'<VAR>inst✝¹ : L.Structure M<VAR>inst✝ : Infinite M<VAR>κ : Cardinal.{w}<VAR>h1 : ℵ₀ ≤ κ<VAR>h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ<GOAL>∃ N, (M ≅[L] ↑N) ∧ #↑N = κ
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>M : Type w'<VAR>inst✝¹ : L.Structure M<VAR>inst✝ : Infinite M<VAR>κ : Cardinal.{w}<VAR>h1 : ℵ₀ ≤ κ<VAR>h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ<VAR>N : Bundled L.Structure<VAR>hNκ : #↑N = κ<VAR>NM : Nonempty (↑N ↪ₑ[L] M)<GOAL>∃ N, (M ≅[L] ↑N) ∧ #↑N = κ
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>M : Type w'<VAR>inst✝¹ : L.Structure M<VAR>inst✝ : Infinite M<VAR>κ : Cardinal.{w}<VAR>h1 : ℵ₀ ≤ κ<VAR>h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ<VAR>N : Bundled L.Structure<VAR>hNκ : #↑N = κ<VAR>MN : Nonempty (M ↪ₑ[L] ↑N)<GOAL>∃ N, (M ≅[L] ↑N) ∧ #↑N = κ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝ : OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>ι : Sort u_4<VAR>p : α → ι → Prop<VAR>hp : ∀ᵐ (a : α) ∂μ, ∀ (i : ι), p a i<VAR>i : ι<GOAL>∀ᵐ (a : α) ∂μ, p a i
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>C : ℝ<VAR>le_hf' : ∀ x ∈ interior D, deriv f x ≤ C<VAR>x✝ : ℝ<VAR>hx✝ : x✝ ∈ D<VAR>y : ℝ<VAR>hy : y ∈ D<VAR>hxy : x✝ ≤ y<VAR>x : ℝ<VAR>hx : x ∈ interior D<GOAL>-C ≤ deriv (fun y => -f y) x
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>C : ℝ<VAR>le_hf' : ∀ x ∈ interior D, deriv f x ≤ C<VAR>x✝ : ℝ<VAR>hx✝ : x✝ ∈ D<VAR>y : ℝ<VAR>hy : y ∈ D<VAR>hxy : x✝ ≤ y<VAR>x : ℝ<VAR>hx : x ∈ interior D<GOAL>deriv f x ≤ C
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>C : ℝ<VAR>le_hf' : ∀ x ∈ interior D, deriv f x ≤ C<VAR>x : ℝ<VAR>hx : x ∈ D<VAR>y : ℝ<VAR>hy : y ∈ D<VAR>hxy : x ≤ y<VAR>hf'_ge : ∀ x ∈ interior D, -C ≤ deriv (fun y => -f y) x<GOAL>f y - f x ≤ C * (y - x)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝² : Finite ι<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (α i)<VAR>r : (i : ι) → α i → Finset (α i) → Prop<VAR>H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)<VAR>p : ((i : ι) → Finset (α i)) → Prop<VAR>f : (i : ι) → Finset (α i)<VAR>h0 : p fun x => ∅<VAR>step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))<GOAL>p f
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝² : Finite ι<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (α i)<VAR>r : (i : ι) → α i → Finset (α i) → Prop<VAR>H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)<VAR>p : ((i : ι) → Finset (α i)) → Prop<VAR>f : (i : ι) → Finset (α i)<VAR>h0 : p fun x => ∅<VAR>step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))<VAR>val✝ : Fintype ι<GOAL>p f
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝² : Finite ι<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (α i)<VAR>r : (i : ι) → α i → Finset (α i) → Prop<VAR>H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)<VAR>p : ((i : ι) → Finset (α i)) → Prop<VAR>h0 : p fun x => ∅<VAR>step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))<VAR>val✝ : Fintype ι<VAR>f : (i : ι) → Finset (α i)<VAR>ihs : ∀ t ⊂ univ.sigma f, ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f<GOAL>p f
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝² : Finite ι<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (α i)<VAR>r : (i : ι) → α i → Finset (α i) → Prop<VAR>H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)<VAR>p : ((i : ι) → Finset (α i)) → Prop<VAR>h0 : p fun x => ∅<VAR>step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))<VAR>val✝ : Fintype ι<VAR>f : (i : ι) → Finset (α i)<VAR>ihs : ∀ t ⊂ univ.sigma f, ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f<VAR>he : univ.sigma f = ∅<GOAL>p f
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝² : Finite ι<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (α i)<VAR>r : (i : ι) → α i → Finset (α i) → Prop<VAR>H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)<VAR>p : ((i : ι) → Finset (α i)) → Prop<VAR>h0 : p fun x => ∅<VAR>step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))<VAR>val✝ : Fintype ι<VAR>f : (i : ι) → Finset (α i)<VAR>ihs : ∀ t ⊂ univ.sigma f, ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f<VAR>hne : (univ.sigma f).Nonempty<GOAL>p f
<VAR>t : ℝ<GOAL>Tendsto (fun x => (1 + t / x) ^ x) atTop (𝓝 (rexp t))
<VAR>t : ℝ<GOAL>(rexp ∘ fun x => x * log (1 + t / x)) =ᶠ[atTop] fun x => (1 + t / x) ^ x
<VAR>t : ℝ<VAR>h₁ : 1 / 2 < 1<GOAL>(rexp ∘ fun x => x * log (1 + t / x)) =ᶠ[atTop] fun x => (1 + t / x) ^ x
<VAR>t : ℝ<VAR>h₁ : 1 / 2 < 1<VAR>h₂ : Tendsto (fun x => 1 + t / x) atTop (𝓝 1)<GOAL>(rexp ∘ fun x => x * log (1 + t / x)) =ᶠ[atTop] fun x => (1 + t / x) ^ x
<VAR>t : ℝ<VAR>h₁ : 1 / 2 < 1<VAR>h₂ : Tendsto (fun x => 1 + t / x) atTop (𝓝 1)<VAR>x : ℝ<VAR>hx : 1 / 2 ≤ 1 + t / x<GOAL>(rexp ∘ fun x => x * log (1 + t / x)) x = (fun x => (1 + t / x) ^ x) x
<VAR>t : ℝ<VAR>h₁ : 1 / 2 < 1<VAR>h₂ : Tendsto (fun x => 1 + t / x) atTop (𝓝 1)<VAR>x : ℝ<VAR>hx : 1 / 2 ≤ 1 + t / x<VAR>hx' : 0 < 1 + t / x<GOAL>(rexp ∘ fun x => x * log (1 + t / x)) x = (fun x => (1 + t / x) ^ x) x
<VAR>R : Type u_1<VAR>inst✝¹ : AddMonoidWithOne R<VAR>inst✝ : CharZero R<VAR>n : ℕ<GOAL>↑n = 0 ↔ n = 0
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ : ℤ_[p]<VAR>n : ℕ<VAR>x : ℤ_[p]<GOAL>x ∈ RingHom.ker (toZModPow n) ↔ x ∈ Ideal.span {↑p ^ n}
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ : ℤ_[p]<VAR>n : ℕ<VAR>x : ℤ_[p]<GOAL>(toZModPow n) x = 0 ↔ x ∈ Ideal.span {↑p ^ n}
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f g x y : Perm α<VAR>h : f.Disjoint g<VAR>hf : x.support ≤ f.support<VAR>hg : y.support ≤ g.support<GOAL>x.Disjoint y
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f g x y : Perm α<VAR>h : _root_.Disjoint f.support g.support<VAR>hf : x.support ≤ f.support<VAR>hg : y.support ≤ g.support<GOAL>_root_.Disjoint x.support y.support
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>f : R →+* S<VAR>n : ℤ<GOAL>(W.map f).preΨ n = Polynomial.map f (W.preΨ n)
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>f : R →+* S<VAR>n : ℤ<GOAL>preNormEDS ((mapRingHom f) W.Ψ₂Sq ^ 2) ((mapRingHom f) W.Ψ₃) ((mapRingHom f) W.preΨ₄) n = preNormEDS ((mapRingHom f) (W.Ψ₂Sq ^ 2)) ((mapRingHom f) W.Ψ₃) ((mapRingHom f) W.preΨ₄) n
<VAR>q : ℚ<GOAL>(q * q).den = q.den * q.den
<VAR>q : ℚ<GOAL>(q.num.natAbs * q.num.natAbs).Coprime (q.den * q.den)
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpTo n f p<VAR>x : E<GOAL>p x 0 = (continuousMultilinearCurryFin0 𝕜 E F).symm (f x)