ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p : R[X]<VAR>hp : p.Monic<VAR>hp2 : 2 ≤ p.natDegree<VAR>hp3 : p.natDegree ≤ 3<VAR>hp0 : p ≠ 0<VAR>hp1 : p ≠ 1<VAR>h : ∀ (a : R), ¬X - C a ∣ p<VAR>q : R[X]<VAR>hq : q.Monic<VAR>hq1 : q.natDegree = 1<GOAL>¬X - C (-q.coeff 0) ∣ p
<VAR>J : Type v<VAR>inst✝ : Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>c : Cone F<VAR>t : IsLimit c<VAR>x : ↑F.sections<VAR>j : J<GOAL>c.π.app j ((isLimitEquivSections t).symm x) = ↑x j
<VAR>J : Type v<VAR>inst✝ : Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>c : Cone F<VAR>t : IsLimit c<VAR>x : ↑F.sections<VAR>j : J<GOAL>c.π.app j ((isLimitEquivSections t).symm x) = ↑((isLimitEquivSections t).toFun ((isLimitEquivSections t).invFun x)) j
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝¹ : CommRing R<VAR>inst✝ : NoZeroDivisors R<VAR>a✝ b✝ : R<VAR>a b : Rˣ<GOAL>a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b
<VAR>p : ZFSet → ZFSet → Prop<VAR>x y z : ZFSet<GOAL>z ∈ pairSep p x y ↔ ∃ a ∈ x, ∃ b ∈ y, z = a.pair b ∧ p a b
<VAR>p : ZFSet → ZFSet → Prop<VAR>x y z : ZFSet<VAR>e : ∃ a ∈ x, ∃ b ∈ y, z = a.pair b ∧ p a b<GOAL>z ∈ (x ∪ y).powerset.powerset
<VAR>p : ZFSet → ZFSet → Prop<VAR>x y a : ZFSet<VAR>ax : a ∈ x<VAR>b : ZFSet<VAR>bY : b ∈ y<VAR>pab : p a b<GOAL>a.pair b ∈ (x ∪ y).powerset.powerset
<VAR>p : ZFSet → ZFSet → Prop<VAR>x y a : ZFSet<VAR>ax : a ∈ x<VAR>b : ZFSet<VAR>bY : b ∈ y<VAR>pab : p a b<GOAL>∀ ⦃z : ZFSet⦄, z = {a} ∨ z = {a, b} → ∀ ⦃z_1 : ZFSet⦄, z_1 ∈ z → z_1 ∈ x ∨ z_1 ∈ y
<VAR>p : ZFSet → ZFSet → Prop<VAR>x y a : ZFSet<VAR>ax : a ∈ x<VAR>b : ZFSet<VAR>bY : b ∈ y<VAR>pab : p a b<VAR>v : ZFSet<GOAL>v = a → v ∈ x ∨ v ∈ y
<VAR>p : ZFSet → ZFSet → Prop<VAR>x y a : ZFSet<VAR>ax : a ∈ x<VAR>b : ZFSet<VAR>bY : b ∈ y<VAR>pab : p a b<VAR>v : ZFSet<GOAL>v = a ∨ v = b → v ∈ x ∨ v ∈ y
<VAR>z τ : ℂ<GOAL>jacobiTheta₂'' (z + 1) τ = jacobiTheta₂'' z τ
<VAR>z τ : ℂ<GOAL>cexp (↑π * I * (z + 1) ^ 2 * τ) * (cexp (-↑π * I * (τ + 2 * (z * τ))) * (jacobiTheta₂' (z * τ) τ - 2 * ↑π * I * jacobiTheta₂ (z * τ) τ) / (2 * ↑π * I) + (z * (cexp (-↑π * I * (τ + 2 * (z * τ))) * jacobiTheta₂ (z * τ) τ) + cexp (-↑π * I * (τ + 2 * (z * τ))) * jacobiTheta₂ (z * τ) τ)) = cexp (↑π * I * z ^ 2 * τ) * (jacobiTheta₂' (z * τ) τ / (2 * ↑π * I) + z * jacobiTheta₂ (z * τ) τ)
<VAR>z τ J J' : ℂ<GOAL>cexp (↑π * I * (z + 1) ^ 2 * τ) * (cexp (-↑π * I * (τ + 2 * (z * τ))) * (J' - 2 * ↑π * I * J) / (2 * ↑π * I) + (z * (cexp (-↑π * I * (τ + 2 * (z * τ))) * J) + cexp (-↑π * I * (τ + 2 * (z * τ))) * J)) = cexp (↑π * I * z ^ 2 * τ) * (J' / (2 * ↑π * I) + z * J)
<VAR>z τ J J' : ℂ<GOAL>cexp (↑π * I * (z + 1) ^ 2 * τ) * (cexp (-↑π * I * (τ + 2 * (z * τ))) * (J' - 2 * ↑π * I * J) + (z * (cexp (-↑π * I * (τ + 2 * (z * τ))) * J) + cexp (-↑π * I * (τ + 2 * (z * τ))) * J) * (2 * ↑π * I)) / (2 * ↑π * I) = cexp (↑π * I * z ^ 2 * τ) * (J' + z * J * (2 * ↑π * I)) / (2 * ↑π * I)
<VAR>z τ J J' : ℂ<GOAL>cexp (↑π * I * (z + 1) ^ 2 * τ) * (cexp (-↑π * I * (τ + 2 * (z * τ))) * (J' - 2 * ↑π * I * J) + (z * (cexp (-↑π * I * (τ + 2 * (z * τ))) * J) + cexp (-↑π * I * (τ + 2 * (z * τ))) * J) * (2 * ↑π * I)) = cexp (↑π * I * z ^ 2 * τ) * (J' + z * J * (2 * ↑π * I))
<VAR>z τ J J' : ℂ<GOAL>cexp (↑π * I * (z + 1) ^ 2 * τ + -↑π * I * (τ + 2 * (z * τ))) * (J' - 2 * ↑π * I * J + (z * J + J) * (2 * ↑π * I)) = cexp (↑π * I * z ^ 2 * τ) * (J' + z * J * (2 * ↑π * I))
<VAR>n : ℕ<VAR>α : Type u_1<VAR>v : Vector α (n + 1)<GOAL>v.reverse.head = v.last
<VAR>n : ℕ<VAR>α : Type u_1<VAR>v : Vector α (n + 1)<GOAL>v.reverse.toList.get (Fin.cast ⋯ 0) = v.toList.get (Fin.cast ⋯ (Fin.last n))
<VAR>n : ℕ<VAR>α : Type u_1<VAR>v : Vector α (n + 1)<GOAL>v.toList.reverse.get (Fin.cast ⋯ 0) = v.toList.get (Fin.cast ⋯ (Fin.last n))
<VAR>n : ℕ<VAR>α : Type u_1<VAR>v : Vector α (n + 1)<GOAL>v.toList[v.toList.length - 1 - ↑⟨↑0, ⋯⟩]? = v.toList[↑⟨↑(Fin.last n), ⋯⟩]?
<VAR>n : ℕ<VAR>α : Type u_1<VAR>v : Vector α (n + 1)<GOAL>↑⟨↑0, ⋯⟩ < v.toList.length
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → PartialOrder (α i)<VAR>f : (i : ι) → α i<VAR>i : ι<VAR>b : α i<GOAL>update f i '' Icc (f i) b = Icc f (update f i b)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : OrderedAddCommGroup α<VAR>s t : Interval α<VAR>a : α<GOAL>(s - t).length ≤ s.length + t.length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E I✝ s : Set α<VAR>M✝ : Matroid α<VAR>N✝ : Matroid β<VAR>X I : Set α<VAR>M N : Matroid α<VAR>hN : N.E = M.E<VAR>h : M.restrictSubtype M.E = N.restrictSubtype M.E<GOAL>M = N
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E I✝¹ s : Set α<VAR>M✝ : Matroid α<VAR>N✝ : Matroid β<VAR>X I✝ : Set α<VAR>M N : Matroid α<VAR>hN : N.E = M.E<VAR>h : M.restrictSubtype M.E = N.restrictSubtype M.E<VAR>I : Set α<VAR>hI : I ⊆ M.E<GOAL>M.Indep I ↔ N.Indep I
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α : E<VAR>S : Set E<VAR>K L : IntermediateField F E<GOAL>finrank F ↥K = 1 ↔ K = ⊥
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t✝ : Set α<VAR>hs : MeasurableSet s<VAR>t : Set α<GOAL>t ∈ ae (μ.restrict s) ↔ t ∈ ae μ ⊓ 𝓟 s
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t✝ : Set α<VAR>hs : MeasurableSet s<VAR>t : Set α<GOAL>μ (tᶜ ∩ s) = 0 ↔ μ {a | a ∉ t ∧ a ∈ s} = 0
<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>HasProd (fun p => (1 - ↑↑p ^ (-s))⁻¹) (riemannZeta s)
<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>HasProd (fun p => (1 - ↑↑p ^ (-s))⁻¹) (∑' (n : ℕ), (riemannZetaSummandHom ⋯) n)
<VAR>C : Type u_1<VAR>inst✝³ : Category.{?u.11479, u_1} C<VAR>Φ : C ⥤ C<VAR>ε : 𝟭 C ⟶ Φ<VAR>J : Type u<VAR>inst✝² : LinearOrder J<VAR>inst✝¹ : IsWellOrder J fun x x_1 => x < x_1<VAR>inst✝ : OrderBot J<VAR>j : J<VAR>F : { i // i ≤ j } ⥤ C<VAR>i : J<VAR>hi : i ≤ j<VAR>x✝² x✝¹ : { k // k < i }<VAR>k₁ : J<VAR>hk₁ : k₁ < i<VAR>k₂ : J<VAR>hk₂ : k₂ < i<VAR>x✝ : ⟨k₁, hk₁⟩ ⟶ ⟨k₂, hk₂⟩<GOAL>(restrictionLT F hi).map x✝ ≫ (fun x => match x with | ⟨k, hk⟩ => F.map (homOfLE ⋯)) ⟨k₂, hk₂⟩ = (fun x => match x with | ⟨k, hk⟩ => F.map (homOfLE ⋯)) ⟨k₁, hk₁⟩ ≫ ((const { k // k < i }).obj (F.obj ⟨i, hi⟩)).map x✝
<VAR>X Y : SemiNormedGrp<VAR>f : X ⟶ Y<VAR>x : ↑X<GOAL>(f ≫ explicitCokernelπ f) x = 0
<VAR>X Y : SemiNormedGrp<VAR>f : X ⟶ Y<VAR>x : ↑X<GOAL>0 x = 0
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : DecidableEq (K →+* ℂ)<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>a : Matrix α β (𝓞 K)<VAR>ha : a ≠ 0<VAR>p q : ℕ<VAR>cardα : Fintype.card α = p<VAR>cardβ : Fintype.card β = q<VAR>h0p : 0 < p<VAR>hpq : p < q<VAR>x : β × (K →+* ℂ) → ℤ<VAR>hxl : x ≠ 0<VAR>hmulvec0 : NumberField.house.asiegel K a *ᵥ x = 0<VAR>hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))<VAR>l : β<VAR>k : α<VAR>r : K →+* ℂ<GOAL>a k l * (NumberField.house.newBasis K) r = ∑ u : K →+* ℂ, ↑(NumberField.house.a' K a k l r u) * (NumberField.house.newBasis K) u
<VAR>a b k m n p : ℕ<VAR>hp : Prime p<GOAL>p.primeFactors = {p}
<VAR>M : Type u<VAR>G : Type v<VAR>X : Type w<VAR>inst✝⁵ : PseudoEMetricSpace X<VAR>inst✝⁴ : Group G<VAR>inst✝³ : MulAction G X<VAR>inst✝² : IsometricSMul G X<VAR>inst✝¹ : PseudoEMetricSpace G<VAR>inst✝ : IsometricSMul Gᵐᵒᵖ G<VAR>a b : G<VAR>r : ℝ≥0∞<GOAL>(fun x => x * a) ⁻¹' closedBall b r = closedBall (b / a) r
<VAR>M : Type u<VAR>G : Type v<VAR>X : Type w<VAR>inst✝⁵ : PseudoEMetricSpace X<VAR>inst✝⁴ : Group G<VAR>inst✝³ : MulAction G X<VAR>inst✝² : IsometricSMul G X<VAR>inst✝¹ : PseudoEMetricSpace G<VAR>inst✝ : IsometricSMul Gᵐᵒᵖ G<VAR>a b : G<VAR>r : ℝ≥0∞<GOAL>(fun x => x * a) ⁻¹' closedBall b r = closedBall (b * a⁻¹) r
<VAR>α : Type u<VAR>β✝ : α → Type v<VAR>β : α → Type u<GOAL>(sum fun a => #(WType β) ^ lift.{u, u} #(β a)) = sum fun a => #(WType β) ^ #(β a)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<GOAL>Continuous fun f => setToFun μ T hT ↑↑f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<GOAL>Continuous fun f => (L1.setToL1 hT) f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>mab : α → β<VAR>mba : β → α<VAR>f : Filter α<VAR>g : Filter β<VAR>h₁ : mab ∘ mba =ᶠ[g] id<VAR>h₂ : Tendsto mba g f<GOAL>g ≤ map mab f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>mab : α → β<VAR>mba : β → α<VAR>f : Filter α<VAR>g : Filter β<VAR>h₁ : mab ∘ mba =ᶠ[g] id<VAR>h₂ : Tendsto mba g f<GOAL>map mab (map mba g) ≤ map mab f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 F<VAR>inst✝ : Nonempty ι<VAR>B✝ B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>p : SeminormFamily 𝕜 E F := B.toSeminormFamily<GOAL>(𝓝 0).HasBasis B.toSeminormFamily.basisSets _root_.id
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 F<VAR>inst✝ : Nonempty ι<VAR>B✝ B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>p : SeminormFamily 𝕜 E F := B.toSeminormFamily<GOAL>(Filter.comap (fun x y => (B x) y) (Filter.pi fun i => 𝓝 ((B 0) i))).HasBasis B.toSeminormFamily.basisSets _root_.id
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 F<VAR>inst✝ : Nonempty ι<VAR>B✝ B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>p : SeminormFamily 𝕜 E F := B.toSeminormFamily<GOAL>(Filter.comap (fun x y => (B x) y) (Filter.pi fun i => 𝓝 0)).HasBasis B.toSeminormFamily.basisSets _root_.id
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 F<VAR>inst✝ : Nonempty ι<VAR>B✝ B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>p : SeminormFamily 𝕜 E F := B.toSeminormFamily<VAR>h : (𝓝 0).HasBasis (fun x => 0 < x) (Metric.ball 0)<GOAL>(Filter.comap (fun x y => (B x) y) (Filter.pi fun i => 𝓝 0)).HasBasis B.toSeminormFamily.basisSets _root_.id
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 F<VAR>inst✝ : Nonempty ι<VAR>B✝ B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>p : SeminormFamily 𝕜 E F := B.toSeminormFamily<VAR>h : (𝓝 0).HasBasis (fun x => 0 < x) (Metric.ball 0)<VAR>h' : (Filter.pi fun x => 𝓝 0).HasBasis (fun If => If.1.Finite ∧ ∀ i ∈ If.1, 0 < If.2 i) fun If => If.1.pi fun i => Metric.ball 0 (If.2 i)<GOAL>(Filter.comap (fun x y => (B x) y) (Filter.pi fun i => 𝓝 0)).HasBasis B.toSeminormFamily.basisSets _root_.id
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 F<VAR>inst✝ : Nonempty ι<VAR>B✝ B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>p : SeminormFamily 𝕜 E F := B.toSeminormFamily<VAR>h : (𝓝 0).HasBasis (fun x => 0 < x) (Metric.ball 0)<VAR>h' : (Filter.pi fun x => 𝓝 0).HasBasis (fun If => If.1.Finite ∧ ∀ i ∈ If.1, 0 < If.2 i) fun If => If.1.pi fun i => Metric.ball 0 (If.2 i)<VAR>h'' : (Filter.comap (fun x y => (B x) y) (Filter.pi fun x => 𝓝 0)).HasBasis (fun If => If.1.Finite ∧ ∀ i ∈ If.1, 0 < If.2 i) fun i => (fun x y => (B x) y) ⁻¹' i.1.pi fun i_1 => Metric.ball 0 (i.2 i_1)<GOAL>(Filter.comap (fun x y => (B x) y) (Filter.pi fun i => 𝓝 0)).HasBasis B.toSeminormFamily.basisSets _root_.id
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 F<VAR>inst✝ : Nonempty ι<VAR>B✝ B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>p : SeminormFamily 𝕜 E F := B.toSeminormFamily<VAR>h : (𝓝 0).HasBasis (fun x => 0 < x) (Metric.ball 0)<VAR>h' : (Filter.pi fun x => 𝓝 0).HasBasis (fun If => If.1.Finite ∧ ∀ i ∈ If.1, 0 < If.2 i) fun If => If.1.pi fun i => Metric.ball 0 (If.2 i)<VAR>h'' : (Filter.comap (fun x y => (B x) y) (Filter.pi fun x => 𝓝 0)).HasBasis (fun If => If.1.Finite ∧ ∀ i ∈ If.1, 0 < If.2 i) fun i => (fun x y => (B x) y) ⁻¹' i.1.pi fun i_1 => Metric.ball 0 (i.2 i_1)<GOAL>∀ (i : Set F × (F → ℝ)), (i.1.Finite ∧ ∀ i_1 ∈ i.1, 0 < i.2 i_1) → ∃ i', B.toSeminormFamily.basisSets i' ∧ _root_.id i' ⊆ (fun x y => (B x) y) ⁻¹' i.1.pi fun i_1 => Metric.ball 0 (i.2 i_1)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 F<VAR>inst✝ : Nonempty ι<VAR>B✝ B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>p : SeminormFamily 𝕜 E F := B.toSeminormFamily<VAR>h : (𝓝 0).HasBasis (fun x => 0 < x) (Metric.ball 0)<VAR>h' : (Filter.pi fun x => 𝓝 0).HasBasis (fun If => If.1.Finite ∧ ∀ i ∈ If.1, 0 < If.2 i) fun If => If.1.pi fun i => Metric.ball 0 (If.2 i)<VAR>h'' : (Filter.comap (fun x y => (B x) y) (Filter.pi fun x => 𝓝 0)).HasBasis (fun If => If.1.Finite ∧ ∀ i ∈ If.1, 0 < If.2 i) fun i => (fun x y => (B x) y) ⁻¹' i.1.pi fun i_1 => Metric.ball 0 (i.2 i_1)<GOAL>∀ (i' : Set E), B.toSeminormFamily.basisSets i' → ∃ i, (i.1.Finite ∧ ∀ i_1 ∈ i.1, 0 < i.2 i_1) ∧ ((fun x y => (B x) y) ⁻¹' i.1.pi fun i_1 => Metric.ball 0 (i.2 i_1)) ⊆ _root_.id i'
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 F<VAR>inst✝ : Nonempty ι<VAR>B✝ B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>p : SeminormFamily 𝕜 E F := B.toSeminormFamily<VAR>h : (𝓝 0).HasBasis (fun x => 0 < x) (Metric.ball 0)<VAR>h' : (Filter.pi fun x => 𝓝 0).HasBasis (fun If => If.1.Finite ∧ ∀ i ∈ If.1, 0 < If.2 i) fun If => If.1.pi fun i => Metric.ball 0 (If.2 i)<VAR>h'' : (Filter.comap (fun x y => (B x) y) (Filter.pi fun x => 𝓝 0)).HasBasis (fun If => If.1.Finite ∧ ∀ i ∈ If.1, 0 < If.2 i) fun i => (fun x y => (B x) y) ⁻¹' i.1.pi fun i_1 => Metric.ball 0 (i.2 i_1)<VAR>U : Set E<VAR>hU : U ∈ p.basisSets<GOAL>∃ i, (i.1.Finite ∧ ∀ i_1 ∈ i.1, 0 < i.2 i_1) ∧ ((fun x y => (B x) y) ⁻¹' i.1.pi fun i_1 => Metric.ball 0 (i.2 i_1)) ⊆ _root_.id U
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 F<VAR>inst✝ : Nonempty ι<VAR>B✝ B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>p : SeminormFamily 𝕜 E F := B.toSeminormFamily<VAR>h : (𝓝 0).HasBasis (fun x => 0 < x) (Metric.ball 0)<VAR>h' : (Filter.pi fun x => 𝓝 0).HasBasis (fun If => If.1.Finite ∧ ∀ i ∈ If.1, 0 < If.2 i) fun If => If.1.pi fun i => Metric.ball 0 (If.2 i)<VAR>h'' : (Filter.comap (fun x y => (B x) y) (Filter.pi fun x => 𝓝 0)).HasBasis (fun If => If.1.Finite ∧ ∀ i ∈ If.1, 0 < If.2 i) fun i => (fun x y => (B x) y) ⁻¹' i.1.pi fun i_1 => Metric.ball 0 (i.2 i_1)<VAR>U : Set E<VAR>hU : ∃ i r, 0 < r ∧ U = (i.sup p).ball 0 r<GOAL>∃ i, (i.1.Finite ∧ ∀ i_1 ∈ i.1, 0 < i.2 i_1) ∧ ((fun x y => (B x) y) ⁻¹' i.1.pi fun i_1 => Metric.ball 0 (i.2 i_1)) ⊆ _root_.id U
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 F<VAR>inst✝ : Nonempty ι<VAR>B✝ B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>p : SeminormFamily 𝕜 E F := B.toSeminormFamily<VAR>h : (𝓝 0).HasBasis (fun x => 0 < x) (Metric.ball 0)<VAR>h' : (Filter.pi fun x => 𝓝 0).HasBasis (fun If => If.1.Finite ∧ ∀ i ∈ If.1, 0 < If.2 i) fun If => If.1.pi fun i => Metric.ball 0 (If.2 i)<VAR>h'' : (Filter.comap (fun x y => (B x) y) (Filter.pi fun x => 𝓝 0)).HasBasis (fun If => If.1.Finite ∧ ∀ i ∈ If.1, 0 < If.2 i) fun i => (fun x y => (B x) y) ⁻¹' i.1.pi fun i_1 => Metric.ball 0 (i.2 i_1)<VAR>U : Set E<VAR>s : Finset F<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hU : U = (s.sup p).ball 0 r<GOAL>∃ i, (i.1.Finite ∧ ∀ i_1 ∈ i.1, 0 < i.2 i_1) ∧ ((fun x y => (B x) y) ⁻¹' i.1.pi fun i_1 => Metric.ball 0 (i.2 i_1)) ⊆ _root_.id ((s.sup p).ball 0 r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 F<VAR>inst✝ : Nonempty ι<VAR>B✝ B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>p : SeminormFamily 𝕜 E F := B.toSeminormFamily<VAR>h : (𝓝 0).HasBasis (fun x => 0 < x) (Metric.ball 0)<VAR>h' : (Filter.pi fun x => 𝓝 0).HasBasis (fun If => If.1.Finite ∧ ∀ i ∈ If.1, 0 < If.2 i) fun If => If.1.pi fun i => Metric.ball 0 (If.2 i)<VAR>h'' : (Filter.comap (fun x y => (B x) y) (Filter.pi fun x => 𝓝 0)).HasBasis (fun If => If.1.Finite ∧ ∀ i ∈ If.1, 0 < If.2 i) fun i => (fun x y => (B x) y) ⁻¹' i.1.pi fun i_1 => Metric.ball 0 (i.2 i_1)<VAR>U : Set E<VAR>s : Finset F<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hU : U = (s.sup p).ball 0 r<VAR>x : E<VAR>hx : x ∈ (fun x y => (B x) y) ⁻¹' (↑s, fun x => r).1.pi fun i => Metric.ball 0 ((↑s, fun x => r).2 i)<GOAL>x ∈ _root_.id ((s.sup p).ball 0 r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 F<VAR>inst✝ : Nonempty ι<VAR>B✝ B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>p : SeminormFamily 𝕜 E F := B.toSeminormFamily<VAR>h : (𝓝 0).HasBasis (fun x => 0 < x) (Metric.ball 0)<VAR>h' : (Filter.pi fun x => 𝓝 0).HasBasis (fun If => If.1.Finite ∧ ∀ i ∈ If.1, 0 < If.2 i) fun If => If.1.pi fun i => Metric.ball 0 (If.2 i)<VAR>h'' : (Filter.comap (fun x y => (B x) y) (Filter.pi fun x => 𝓝 0)).HasBasis (fun If => If.1.Finite ∧ ∀ i ∈ If.1, 0 < If.2 i) fun i => (fun x y => (B x) y) ⁻¹' i.1.pi fun i_1 => Metric.ball 0 (i.2 i_1)<VAR>U : Set E<VAR>s : Finset F<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hU : U = (s.sup p).ball 0 r<VAR>x : E<VAR>hx : ∀ i ∈ s, ‖(B x) i‖ < r<GOAL>x ∈ _root_.id ((s.sup p).ball 0 r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 F<VAR>inst✝ : Nonempty ι<VAR>B✝ B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>p : SeminormFamily 𝕜 E F := B.toSeminormFamily<VAR>h : (𝓝 0).HasBasis (fun x => 0 < x) (Metric.ball 0)<VAR>h' : (Filter.pi fun x => 𝓝 0).HasBasis (fun If => If.1.Finite ∧ ∀ i ∈ If.1, 0 < If.2 i) fun If => If.1.pi fun i => Metric.ball 0 (If.2 i)<VAR>h'' : (Filter.comap (fun x y => (B x) y) (Filter.pi fun x => 𝓝 0)).HasBasis (fun If => If.1.Finite ∧ ∀ i ∈ If.1, 0 < If.2 i) fun i => (fun x y => (B x) y) ⁻¹' i.1.pi fun i_1 => Metric.ball 0 (i.2 i_1)<VAR>U : Set E<VAR>s : Finset F<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hU : U = (s.sup p).ball 0 r<VAR>x : E<VAR>hx : ∀ i ∈ s, ‖(B x) i‖ < r<GOAL>(s.sup p) x < r
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 F<VAR>inst✝ : Nonempty ι<VAR>B✝ B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>p : SeminormFamily 𝕜 E F := B.toSeminormFamily<VAR>h : (𝓝 0).HasBasis (fun x => 0 < x) (Metric.ball 0)<VAR>h' : (Filter.pi fun x => 𝓝 0).HasBasis (fun If => If.1.Finite ∧ ∀ i ∈ If.1, 0 < If.2 i) fun If => If.1.pi fun i => Metric.ball 0 (If.2 i)<VAR>h'' : (Filter.comap (fun x y => (B x) y) (Filter.pi fun x => 𝓝 0)).HasBasis (fun If => If.1.Finite ∧ ∀ i ∈ If.1, 0 < If.2 i) fun i => (fun x y => (B x) y) ⁻¹' i.1.pi fun i_1 => Metric.ball 0 (i.2 i_1)<VAR>U : Set E<VAR>s : Finset F<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hU : U = (s.sup p).ball 0 r<VAR>x : E<VAR>hx : ∀ i ∈ s, ‖(B x) i‖ < r<VAR>y : F<VAR>hy : y ∈ s<GOAL>(p y) x < r
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 F<VAR>inst✝ : Nonempty ι<VAR>B✝ B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>p : SeminormFamily 𝕜 E F := B.toSeminormFamily<VAR>h : (𝓝 0).HasBasis (fun x => 0 < x) (Metric.ball 0)<VAR>h' : (Filter.pi fun x => 𝓝 0).HasBasis (fun If => If.1.Finite ∧ ∀ i ∈ If.1, 0 < If.2 i) fun If => If.1.pi fun i => Metric.ball 0 (If.2 i)<VAR>h'' : (Filter.comap (fun x y => (B x) y) (Filter.pi fun x => 𝓝 0)).HasBasis (fun If => If.1.Finite ∧ ∀ i ∈ If.1, 0 < If.2 i) fun i => (fun x y => (B x) y) ⁻¹' i.1.pi fun i_1 => Metric.ball 0 (i.2 i_1)<VAR>U : Set E<VAR>s : Finset F<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hU : U = (s.sup p).ball 0 r<VAR>x : E<VAR>hx : ∀ i ∈ s, ‖(B x) i‖ < r<VAR>y : F<VAR>hy : y ∈ s<GOAL>‖(B x) y‖ < r
<VAR>α : Type u_1<VAR>M : α → Type u_2<VAR>u : Ultrafilter α<VAR>L : Language<VAR>inst✝ : (a : α) → L.Structure (M a)<VAR>n : ℕ<VAR>f : L.Functions n<VAR>x : Fin n → (a : α) → M a<GOAL>(funMap f fun i => Quotient.mk' (x i)) = Quotient.mk' fun a => funMap f fun i => x i a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>R : Type u_6<VAR>S : Type u_7<VAR>F : Filter R<VAR>inst✝¹ : LinearOrder R<VAR>inst✝ : LinearOrder S<VAR>f : R → S<VAR>f_incr : Monotone f<VAR>l : R<VAR>freq_ge : ∃ᶠ (x : R) in F, l ≤ x<VAR>ev : ∀ᶠ (x : S) in map f F, ¬(fun x' => f l ≤ x') x<GOAL>∀ᶠ (x : R) in F, ¬(fun x => l ≤ x) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>R : Type u_6<VAR>S : Type u_7<VAR>F : Filter R<VAR>inst✝¹ : LinearOrder R<VAR>inst✝ : LinearOrder S<VAR>f : R → S<VAR>f_incr : Monotone f<VAR>l : R<VAR>freq_ge : ∃ᶠ (x : R) in F, l ≤ x<VAR>ev : ∀ᶠ (x : S) in map f F, x < f l<GOAL>∀ᶠ (x : R) in F, x < l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>R : Type u_6<VAR>S : Type u_7<VAR>F : Filter R<VAR>inst✝¹ : LinearOrder R<VAR>inst✝ : LinearOrder S<VAR>f : R → S<VAR>f_incr : Monotone f<VAR>l : R<VAR>freq_ge : ∃ᶠ (x : R) in F, l ≤ x<VAR>ev : ∀ᶠ (x : S) in map f F, x < f l<VAR>z : R<VAR>hz : z ∈ f ⁻¹' {x | x < f l}<GOAL>z < l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>R : Type u_6<VAR>S : Type u_7<VAR>F : Filter R<VAR>inst✝¹ : LinearOrder R<VAR>inst✝ : LinearOrder S<VAR>f : R → S<VAR>f_incr : Monotone f<VAR>l : R<VAR>freq_ge : ∃ᶠ (x : R) in F, l ≤ x<VAR>ev : ∀ᶠ (x : S) in map f F, x < f l<VAR>z : R<VAR>hz : z ∈ f ⁻¹' {x | x < f l}<VAR>con : ¬z < l<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>a : α<VAR>as✝ : List α<VAR>b : β<VAR>bs✝ : List β<VAR>as : List α<VAR>bs : List β<GOAL>zipWithLeft Prod.mk as bs = (zipWithLeft' Prod.mk as bs).1
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>c : F<GOAL>DifferentiableWithinAt 𝕜 (fun y => f y - c) s x ↔ DifferentiableWithinAt 𝕜 f s x