ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>l r : Ordnode α<VAR>H : (∃ l', Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r' r.size ∧ BalancedSz l.size r'<GOAL>(∃ l', Raised l' r.size ∧ BalancedSz l' l.size) ∨ ∃ r', Raised l.size r' ∧ BalancedSz r.size r'
<VAR>J K : Type v<VAR>inst✝⁵ : SmallCategory J<VAR>inst✝⁴ : SmallCategory K<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>G : J × K ⥤ C<VAR>inst✝² : HasLimitsOfShape K C<VAR>inst✝¹ : HasLimit G<VAR>inst✝ : HasLimit (curry.obj G ⋙ lim)<VAR>j : J<VAR>k : K<GOAL>(limitIsoLimitCurryCompLim G).inv ≫ limit.π G (j, k) = limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k
<VAR>J K : Type v<VAR>inst✝⁵ : SmallCategory J<VAR>inst✝⁴ : SmallCategory K<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>G : J × K ⥤ C<VAR>inst✝² : HasLimitsOfShape K C<VAR>inst✝¹ : HasLimit G<VAR>inst✝ : HasLimit (curry.obj G ⋙ lim)<VAR>j : J<VAR>k : K<GOAL>(limitIsoLimitCurryCompLim G).hom ≫ (limitIsoLimitCurryCompLim G).inv ≫ limit.π G (j, k) = (limitIsoLimitCurryCompLim G).hom ≫ limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>o.oangle (x - y) x = ↑(Real.arcsin (‖y‖ / ‖x - y‖))
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (-o).oangle y x = ↑(π / 2)<GOAL>(-o).oangle x (x - y) = ↑(Real.arcsin (‖y‖ / ‖x - y‖))
<VAR>R : Type uR<VAR>M : Type uM<VAR>K : Type uK<VAR>V : Type uV<VAR>ι : Type uι<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι R M<VAR>i : ι<VAR>m : M<GOAL>(b.toDual (b i)) m = (b.repr m) i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>h : s ⊆ t<GOAL>s.encard ≤ t.encard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>h : s ⊆ t<GOAL>s.encard ≤ s.encard + (t \ s).encard
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E B I X R J : Set α<GOAL>(freeOn E)✶ = loopyOn E
<VAR>f g : CircleDeg1Lift<VAR>x : ℝ<VAR>n : ℕ<GOAL>(⇑↑(translate (Multiplicative.ofAdd x)))^[n] = ⇑↑(translate (Multiplicative.ofAdd (↑n * x)))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>x y : S<VAR>hy : y ∈ ↑(conductor R x)<GOAL>y ∈ ↑(adjoin R {x})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t u v : Finset α<VAR>a b : α<VAR>ha : a ∉ s<GOAL>insert a s \ s = {a}
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m mΩ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>μ : Measure Ω<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : NormedAddCommGroup F<VAR>f : Ω → F<VAR>hf_int : Integrable f μ<GOAL>Integrable (fun ω => ∫ (y : Ω), ‖f y‖ ∂(condexpKernel μ m) ω) μ
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m mΩ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>μ : Measure Ω<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : NormedAddCommGroup F<VAR>f : Ω → F<VAR>hf_int : Integrable f μ<GOAL>Integrable (fun ω => ∫ (y : Ω), ‖f y‖ ∂((condDistrib id id μ).comap id ⋯) ω) μ
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c c₁ c₂ : ℝ≥0<VAR>ε ε₁ ε₂ : ℝ<VAR>π₁ π₂ : TaggedPrepartition I<VAR>h : Integrable I l f vol<GOAL>Tendsto (fun π => (integralSum f vol π.1, integralSum f vol π.2)) (l.toFilter I ×ˢ l.toFilter I ⊓ 𝓟 {π | π.1.iUnion = π.2.iUnion}) (𝓤 F)
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c c₁ c₂ : ℝ≥0<VAR>ε✝ ε₁ ε₂ : ℝ<VAR>π₁ π₂ : TaggedPrepartition I<VAR>h : Integrable I l f vol<VAR>ε : ℝ<VAR>ε0 : 0 < ε<GOAL>∃ ia, (∀ (c : ℝ≥0), l.RCond (ia c)) ∧ ∀ x ∈ {π | ∃ c, l.MemBaseSet I c (ia c) π} ×ˢ {π | ∃ c, l.MemBaseSet I c (ia c) π} ∩ {π | π.1.iUnion = π.2.iUnion}, (integralSum f vol x.1, integralSum f vol x.2) ∈ {p | dist p.1 p.2 ≤ ε}
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c c₁ c₂ : ℝ≥0<VAR>ε✝ ε₁ ε₂ : ℝ<VAR>π₁ π₂ : TaggedPrepartition I<VAR>h : Integrable I l f vol<VAR>ε : ℝ<VAR>ε0 : 0 < ε / 2<GOAL>∃ ia, (∀ (c : ℝ≥0), l.RCond (ia c)) ∧ ∀ x ∈ {π | ∃ c, l.MemBaseSet I c (ia c) π} ×ˢ {π | ∃ c, l.MemBaseSet I c (ia c) π} ∩ {π | π.1.iUnion = π.2.iUnion}, (integralSum f vol x.1, integralSum f vol x.2) ∈ {p | dist p.1 p.2 ≤ ε}
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c c₁ c₂ : ℝ≥0<VAR>ε✝ ε₁ ε₂ : ℝ<VAR>π₁ π₂ : TaggedPrepartition I<VAR>h : Integrable I l f vol<VAR>ε : ℝ<VAR>ε0 : 0 < ε / 2<GOAL>∀ x ∈ {π | ∃ c, l.MemBaseSet I c (h.convergenceR (ε / 2) c) π} ×ˢ {π | ∃ c, l.MemBaseSet I c (h.convergenceR (ε / 2) c) π} ∩ {π | π.1.iUnion = π.2.iUnion}, (integralSum f vol x.1, integralSum f vol x.2) ∈ {p | dist p.1 p.2 ≤ ε}
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c c₁ c₂ : ℝ≥0<VAR>ε✝ ε₁ ε₂ : ℝ<VAR>π₁✝ π₂✝ : TaggedPrepartition I<VAR>h : Integrable I l f vol<VAR>ε : ℝ<VAR>ε0 : 0 < ε / 2<VAR>π₁ π₂ : TaggedPrepartition I<VAR>hU : (π₁, π₂) ∈ {π | π.1.iUnion = π.2.iUnion}<VAR>h₁ : (π₁, π₂).1 ∈ {π | ∃ c, l.MemBaseSet I c (h.convergenceR (ε / 2) c) π}<VAR>h₂ : (π₁, π₂).2 ∈ {π | ∃ c, l.MemBaseSet I c (h.convergenceR (ε / 2) c) π}<GOAL>(integralSum f vol (π₁, π₂).1, integralSum f vol (π₁, π₂).2) ∈ {p | dist p.1 p.2 ≤ ε}
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c c₁ c₂ : ℝ≥0<VAR>ε✝ ε₁ ε₂ : ℝ<VAR>π₁✝ π₂✝ : TaggedPrepartition I<VAR>h : Integrable I l f vol<VAR>ε : ℝ<VAR>ε0 : 0 < ε / 2<VAR>π₁ π₂ : TaggedPrepartition I<VAR>hU : (π₁, π₂) ∈ {π | π.1.iUnion = π.2.iUnion}<VAR>h₁ : (π₁, π₂).1 ∈ {π | ∃ c, l.MemBaseSet I c (h.convergenceR (ε / 2) c) π}<VAR>h₂ : (π₁, π₂).2 ∈ {π | ∃ c, l.MemBaseSet I c (h.convergenceR (ε / 2) c) π}<GOAL>(integralSum f vol (π₁, π₂).1, integralSum f vol (π₁, π₂).2) ∈ {p | dist p.1 p.2 ≤ ε / 2 + ε / 2}
<VAR>α✝ : Type u_1<VAR>l₁ l₂ l r : List α✝<GOAL>l ++ l₁ ++ r = l ++ l₂ ↔ l₁ ++ r = l₂
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S M<VAR>inst✝¹ : SMul S R<VAR>inst✝ : IsScalarTower S R M<VAR>p✝ q : Submodule R M<VAR>ι : Sort u_4<VAR>p : ι → Submodule R M<VAR>x : M<GOAL>x ∈ ⨅ i, p i ↔ ∀ (i : ι), x ∈ p i
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S M<VAR>inst✝¹ : SMul S R<VAR>inst✝ : IsScalarTower S R M<VAR>p✝ q : Submodule R M<VAR>ι : Sort u_4<VAR>p : ι → Submodule R M<VAR>x : M<GOAL>(∀ (i : ι), x ∈ ↑(p i)) ↔ ∀ (i : ι), x ∈ p i
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>h : ∀ (u : ℕ → E), (Summable fun x => ‖u x‖) → ∃ a, Tendsto (fun n => ∑ i ∈ range n, u i) atTop (𝓝 a)<GOAL>CompleteSpace E
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>h : ∀ (u : ℕ → E), (Summable fun x => ‖u x‖) → ∃ a, Tendsto (fun n => ∑ i ∈ range n, u i) atTop (𝓝 a)<GOAL>∀ (u : ℕ → E), CauchySeq u → ∃ a, Tendsto u atTop (𝓝 a)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>h : ∀ (u : ℕ → E), (Summable fun x => ‖u x‖) → ∃ a, Tendsto (fun n => ∑ i ∈ range n, u i) atTop (𝓝 a)<VAR>u : ℕ → E<VAR>hu : CauchySeq u<GOAL>∃ a, Tendsto u atTop (𝓝 a)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>h : ∀ (u : ℕ → E), (Summable fun x => ‖u x‖) → ∃ a, Tendsto (fun n => ∑ i ∈ range n, u i) atTop (𝓝 a)<VAR>u : ℕ → E<VAR>hu : CauchySeq u<VAR>f : ℕ → ℕ<VAR>hf₁ : StrictMono f<VAR>hf₂ : Summable fun i => dist (u (f (i + 1))) (u (f i))<GOAL>∃ a, Tendsto u atTop (𝓝 a)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>h : ∀ (u : ℕ → E), (Summable fun x => ‖u x‖) → ∃ a, Tendsto (fun n => ∑ i ∈ range n, u i) atTop (𝓝 a)<VAR>u : ℕ → E<VAR>hu : CauchySeq u<VAR>f : ℕ → ℕ<VAR>hf₁ : StrictMono f<VAR>hf₂ : Summable fun i => ‖u (f (i + 1)) - u (f i)‖<VAR>v : ℕ → E := fun n => u (f (n + 1)) - u (f n)<GOAL>∃ a, Tendsto u atTop (𝓝 a)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>h : ∀ (u : ℕ → E), (Summable fun x => ‖u x‖) → ∃ a, Tendsto (fun n => ∑ i ∈ range n, u i) atTop (𝓝 a)<VAR>u : ℕ → E<VAR>hu : CauchySeq u<VAR>f : ℕ → ℕ<VAR>hf₁ : StrictMono f<VAR>hf₂ : Summable fun i => ‖u (f (i + 1)) - u (f i)‖<VAR>v : ℕ → E := fun n => u (f (n + 1)) - u (f n)<VAR>hv_sum : (fun n => ∑ i ∈ range n, v i) = fun n => u (f n) - u (f 0)<GOAL>∃ a, Tendsto u atTop (𝓝 a)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>h : ∀ (u : ℕ → E), (Summable fun x => ‖u x‖) → ∃ a, Tendsto (fun n => ∑ i ∈ range n, u i) atTop (𝓝 a)<VAR>u : ℕ → E<VAR>hu : CauchySeq u<VAR>f : ℕ → ℕ<VAR>hf₁ : StrictMono f<VAR>hf₂ : Summable fun i => ‖u (f (i + 1)) - u (f i)‖<VAR>v : ℕ → E := fun n => u (f (n + 1)) - u (f n)<VAR>hv_sum : (fun n => ∑ i ∈ range n, v i) = fun n => u (f n) - u (f 0)<VAR>a : E<VAR>ha : Tendsto (fun n => ∑ i ∈ range n, v i) atTop (𝓝 a)<GOAL>Tendsto u atTop (𝓝 (a + u (f 0)))
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>h : ∀ (u : ℕ → E), (Summable fun x => ‖u x‖) → ∃ a, Tendsto (fun n => ∑ i ∈ range n, u i) atTop (𝓝 a)<VAR>u : ℕ → E<VAR>hu : CauchySeq u<VAR>f : ℕ → ℕ<VAR>hf₁ : StrictMono f<VAR>hf₂ : Summable fun i => ‖u (f (i + 1)) - u (f i)‖<VAR>v : ℕ → E := fun n => u (f (n + 1)) - u (f n)<VAR>hv_sum : (fun n => ∑ i ∈ range n, v i) = fun n => u (f n) - u (f 0)<VAR>a : E<VAR>ha : Tendsto (fun n => ∑ i ∈ range n, v i) atTop (𝓝 a)<GOAL>Tendsto (u ∘ f) atTop (𝓝 (a + u (f 0)))
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>h : ∀ (u : ℕ → E), (Summable fun x => ‖u x‖) → ∃ a, Tendsto (fun n => ∑ i ∈ range n, u i) atTop (𝓝 a)<VAR>u : ℕ → E<VAR>hu : CauchySeq u<VAR>f : ℕ → ℕ<VAR>hf₁ : StrictMono f<VAR>hf₂ : Summable fun i => ‖u (f (i + 1)) - u (f i)‖<VAR>v : ℕ → E := fun n => u (f (n + 1)) - u (f n)<VAR>hv_sum : (fun n => ∑ i ∈ range n, v i) = fun n => u (f n) - u (f 0)<VAR>a : E<VAR>ha : Tendsto (fun n => u (f n) - u (f 0)) atTop (𝓝 a)<GOAL>Tendsto (u ∘ f) atTop (𝓝 (a + u (f 0)))
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>h : ∀ (u : ℕ → E), (Summable fun x => ‖u x‖) → ∃ a, Tendsto (fun n => ∑ i ∈ range n, u i) atTop (𝓝 a)<VAR>u : ℕ → E<VAR>hu : CauchySeq u<VAR>f : ℕ → ℕ<VAR>hf₁ : StrictMono f<VAR>hf₂ : Summable fun i => ‖u (f (i + 1)) - u (f i)‖<VAR>v : ℕ → E := fun n => u (f (n + 1)) - u (f n)<VAR>hv_sum : (fun n => ∑ i ∈ range n, v i) = fun n => u (f n) - u (f 0)<VAR>a : E<VAR>ha : Tendsto (fun n => u (f n) - u (f 0)) atTop (𝓝 a)<VAR>h₁ : Tendsto (fun n => u (f n) - u (f 0) + u (f 0)) atTop (𝓝 (a + u (f 0)))<GOAL>Tendsto (u ∘ f) atTop (𝓝 (a + u (f 0)))
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : Group α<VAR>inst✝¹ : MulAction α β<VAR>inst✝ : ContinuousConstSMul α β<VAR>s : Set α<VAR>t : Set β<VAR>ht : IsOpen t<GOAL>IsOpen (s • t)
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : Group α<VAR>inst✝¹ : MulAction α β<VAR>inst✝ : ContinuousConstSMul α β<VAR>s : Set α<VAR>t : Set β<VAR>ht : IsOpen t<GOAL>IsOpen (⋃ a ∈ s, a • t)
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>s : Set (α × α)<VAR>x y : α<GOAL>(x, y) ∈ closure s ↔ (x, y) ∈ ⋂ V ∈ {V | V ∈ 𝓤 α ∧ SymmetricRel V}, V ○ s ○ V
<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>insert n n.properDivisors = n.divisors
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : MulOneClass M<VAR>inst✝² : MulOneClass N<VAR>inst✝¹ : MulOneClass P<VAR>S : Submonoid M<VAR>A : Type u_4<VAR>inst✝ : SetLike A M<VAR>hA : SubmonoidClass A M<VAR>S' : A<VAR>s : Submonoid M<VAR>t : Submonoid N<GOAL>s.prod t = ⊥ ↔ s = ⊥ ∧ t = ⊥
<VAR>R : Type u_1<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>ι₁ : Type u_4<VAR>ι₂ : Type u_5<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : Module R M₂<VAR>inst✝⁴ : Fintype ι₁<VAR>inst✝³ : Finite ι₂<VAR>inst✝² : DecidableEq ι₁<VAR>b₁ : Basis ι₁ R M₁<VAR>b₂ : Basis ι₂ R M₂<VAR>f : M₁ →ₗ[R] M₂<VAR>i : ι₂<VAR>A : Type u_6<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra R A<GOAL>toMvPolynomial (basis A b₁) (basis A b₂) (baseChange A f) i = (MvPolynomial.map (algebraMap R A)) (toMvPolynomial b₁ b₂ f i)
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>r : HomRel C<VAR>h : Congruence r<VAR>x✝³ x✝² : C<VAR>x✝¹ x✝ : x✝³ ⟶ x✝²<GOAL>CompClosure r x✝¹ x✝ ↔ r x✝¹ x✝
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>inst✝ : SeparableSpace α<VAR>ι : Type u_2<VAR>s : ι → Set α<VAR>hd : Pairwise (Disjoint on s)<VAR>ho : ∀ (i : ι), IsOpen (s i)<VAR>hne : ∀ (i : ι), (s i).Nonempty<GOAL>Countable ι
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>inst✝ : SeparableSpace α<VAR>ι : Type u_2<VAR>s : ι → Set α<VAR>hd : Pairwise (Disjoint on s)<VAR>ho : ∀ (i : ι), IsOpen (s i)<VAR>hne : ∀ (i : ι), (s i).Nonempty<VAR>u : Set α<VAR>u_countable : u.Countable<VAR>u_dense : Dense u<GOAL>Countable ι
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>inst✝ : SeparableSpace α<VAR>ι : Type u_2<VAR>s : ι → Set α<VAR>hd : Pairwise (Disjoint on s)<VAR>ho : ∀ (i : ι), IsOpen (s i)<VAR>hne : ∀ (i : ι), (s i).Nonempty<VAR>u : Set α<VAR>u_countable : u.Countable<VAR>u_dense : Dense u<VAR>f : ι → α<VAR>hfu : ∀ (i : ι), f i ∈ u<VAR>hfs : ∀ (i : ι), f i ∈ s i<GOAL>Countable ι
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>inst✝ : SeparableSpace α<VAR>ι : Type u_2<VAR>s : ι → Set α<VAR>hd : Pairwise (Disjoint on s)<VAR>ho : ∀ (i : ι), IsOpen (s i)<VAR>hne : ∀ (i : ι), (s i).Nonempty<VAR>u : Set α<VAR>u_countable : u.Countable<VAR>u_dense : Dense u<VAR>f : ι → α<VAR>hfu : ∀ (i : ι), f i ∈ u<VAR>hfs : ∀ (i : ι), f i ∈ s i<VAR>f_inj : Injective f<GOAL>Countable ι
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>inst✝ : SeparableSpace α<VAR>ι : Type u_2<VAR>s : ι → Set α<VAR>hd : Pairwise (Disjoint on s)<VAR>ho : ∀ (i : ι), IsOpen (s i)<VAR>hne : ∀ (i : ι), (s i).Nonempty<VAR>u : Set α<VAR>u_countable : u.Countable<VAR>u_dense : Dense u<VAR>f : ι → α<VAR>hfu : ∀ (i : ι), f i ∈ u<VAR>hfs : ∀ (i : ι), f i ∈ s i<VAR>f_inj : Injective f<VAR>this : Countable ↑u<GOAL>Countable ι
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>f : ℝ → E<VAR>c ca cb : E<VAR>l l' la la' lb lb' : Filter ℝ<VAR>lt : Filter ι<VAR>a b z : ℝ<VAR>u v ua ub va vb : ι → ℝ<VAR>inst✝¹ : FTCFilter a la la'<VAR>inst✝ : FTCFilter b lb lb'<VAR>hab : IntervalIntegrable f volume a b<VAR>hmeas : StronglyMeasurableAtFilter f la' volume<VAR>hf : Tendsto f (la' ⊓ ae volume) (𝓝 c)<VAR>hu : Tendsto u lt la<VAR>hv : Tendsto v lt la<GOAL>(fun t => ((∫ (x : ℝ) in v t..b, f x) - ∫ (x : ℝ) in u t..b, f x) + (v t - u t) • c) =o[lt] (v - u)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>HasSum (fun n => cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s) (expZeta (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>(fun n => cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s) = fun b => ↑(Real.cos (2 * π * a * ↑b)) / ↑b ^ s + I * (↑(Real.sin (2 * π * a * ↑b)) / ↑b ^ s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>n : ℕ<GOAL>cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s = ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s + I * (↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>n : ℕ<GOAL>(Complex.cos (2 * ↑π * ↑a * ↑n) + Complex.sin (2 * ↑π * ↑a * ↑n) * I) / ↑n ^ s = Complex.cos (2 * ↑π * ↑a * ↑n) / ↑n ^ s + I * (Complex.sin (2 * ↑π * ↑a * ↑n) / ↑n ^ s)
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>V₁ : Type u_3<VAR>V₂ : Type u_4<VAR>V₃ : Type u_5<VAR>inst✝⁷ : SeminormedAddCommGroup V<VAR>inst✝⁶ : SeminormedAddCommGroup W<VAR>inst✝⁵ : SeminormedAddCommGroup V₁<VAR>inst✝⁴ : SeminormedAddCommGroup V₂<VAR>inst✝³ : SeminormedAddCommGroup V₃<VAR>f : NormedAddGroupHom V W<VAR>W₁ : Type u_6<VAR>W₂ : Type u_7<VAR>W₃ : Type u_8<VAR>inst✝² : SeminormedAddCommGroup W₁<VAR>inst✝¹ : SeminormedAddCommGroup W₂<VAR>inst✝ : SeminormedAddCommGroup W₃<VAR>g : NormedAddGroupHom V W<VAR>f₁ g₁ : NormedAddGroupHom V₁ W₁<VAR>f₂ g₂ : NormedAddGroupHom V₂ W₂<VAR>f₃ g₃ : NormedAddGroupHom V₃ W₃<VAR>φ : NormedAddGroupHom V₁ V<VAR>h : f.comp φ = g.comp φ<VAR>v : V₁<GOAL>(f - g) (φ v) = 0
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>V₁ : Type u_3<VAR>V₂ : Type u_4<VAR>V₃ : Type u_5<VAR>inst✝⁷ : SeminormedAddCommGroup V<VAR>inst✝⁶ : SeminormedAddCommGroup W<VAR>inst✝⁵ : SeminormedAddCommGroup V₁<VAR>inst✝⁴ : SeminormedAddCommGroup V₂<VAR>inst✝³ : SeminormedAddCommGroup V₃<VAR>f : NormedAddGroupHom V W<VAR>W₁ : Type u_6<VAR>W₂ : Type u_7<VAR>W₃ : Type u_8<VAR>inst✝² : SeminormedAddCommGroup W₁<VAR>inst✝¹ : SeminormedAddCommGroup W₂<VAR>inst✝ : SeminormedAddCommGroup W₃<VAR>g : NormedAddGroupHom V W<VAR>f₁ g₁ : NormedAddGroupHom V₁ W₁<VAR>f₂ g₂ : NormedAddGroupHom V₂ W₂<VAR>f₃ g₃ : NormedAddGroupHom V₃ W₃<VAR>φ : NormedAddGroupHom V₁ V<VAR>h : f.comp φ = g.comp φ<VAR>v₁ v₂ : V₁<GOAL>↑((fun v => ⟨φ v, ⋯⟩) (v₁ + v₂)) = ↑((fun v => ⟨φ v, ⋯⟩) v₁ + (fun v => ⟨φ v, ⋯⟩) v₂)
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>V₁ : Type u_3<VAR>V₂ : Type u_4<VAR>V₃ : Type u_5<VAR>inst✝⁷ : SeminormedAddCommGroup V<VAR>inst✝⁶ : SeminormedAddCommGroup W<VAR>inst✝⁵ : SeminormedAddCommGroup V₁<VAR>inst✝⁴ : SeminormedAddCommGroup V₂<VAR>inst✝³ : SeminormedAddCommGroup V₃<VAR>f : NormedAddGroupHom V W<VAR>W₁ : Type u_6<VAR>W₂ : Type u_7<VAR>W₃ : Type u_8<VAR>inst✝² : SeminormedAddCommGroup W₁<VAR>inst✝¹ : SeminormedAddCommGroup W₂<VAR>inst✝ : SeminormedAddCommGroup W₃<VAR>g : NormedAddGroupHom V W<VAR>f₁ g₁ : NormedAddGroupHom V₁ W₁<VAR>f₂ g₂ : NormedAddGroupHom V₂ W₂<VAR>f₃ g₃ : NormedAddGroupHom V₃ W₃<VAR>φ : NormedAddGroupHom V₁ V<VAR>h : f.comp φ = g.comp φ<GOAL>∃ C, ∀ (v : V₁), ‖(fun v => ⟨φ v, ⋯⟩) v‖ ≤ C * ‖v‖
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>V₁ : Type u_3<VAR>V₂ : Type u_4<VAR>V₃ : Type u_5<VAR>inst✝⁷ : SeminormedAddCommGroup V<VAR>inst✝⁶ : SeminormedAddCommGroup W<VAR>inst✝⁵ : SeminormedAddCommGroup V₁<VAR>inst✝⁴ : SeminormedAddCommGroup V₂<VAR>inst✝³ : SeminormedAddCommGroup V₃<VAR>f : NormedAddGroupHom V W<VAR>W₁ : Type u_6<VAR>W₂ : Type u_7<VAR>W₃ : Type u_8<VAR>inst✝² : SeminormedAddCommGroup W₁<VAR>inst✝¹ : SeminormedAddCommGroup W₂<VAR>inst✝ : SeminormedAddCommGroup W₃<VAR>g : NormedAddGroupHom V W<VAR>f₁ g₁ : NormedAddGroupHom V₁ W₁<VAR>f₂ g₂ : NormedAddGroupHom V₂ W₂<VAR>f₃ g₃ : NormedAddGroupHom V₃ W₃<VAR>φ : NormedAddGroupHom V₁ V<VAR>h : f.comp φ = g.comp φ<VAR>C : ℝ<VAR>_C_pos : 0 < C<VAR>hC : ∀ (x : V₁), ‖φ x‖ ≤ C * ‖x‖<GOAL>∃ C, ∀ (v : V₁), ‖(fun v => ⟨φ v, ⋯⟩) v‖ ≤ C * ‖v‖
<VAR>C : ℕ<VAR>u : ℕ → ℕ<VAR>h_pos : ∀ (n : ℕ), 0 < u n<VAR>hu_strict : StrictMono u<VAR>hC_nonzero : C ≠ 0<VAR>h_succ_diff : SuccDiffBounded C u<VAR>f : ℕ → ℝ≥0<VAR>hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → (fun i => ↑(f i)) n ≤ (fun i => ↑(f i)) m<GOAL>(Summable fun k => (↑(u (k + 1)) - ↑(u k)) * (fun i => ↑(f i)) (u k)) ↔ Summable fun i => ↑(f i)
<VAR>C : ℕ<VAR>u : ℕ → ℕ<VAR>h_pos : ∀ (n : ℕ), 0 < u n<VAR>hu_strict : StrictMono u<VAR>hC_nonzero : C ≠ 0<VAR>h_succ_diff : SuccDiffBounded C u<VAR>f : ℕ → ℝ≥0<VAR>hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m<GOAL>(Summable fun k => (↑(u (k + 1)) - ↑(u k)) * ↑(f (u k))) ↔ Summable fun i => ↑(f i)
<VAR>C : ℕ<VAR>u : ℕ → ℕ<VAR>h_pos : ∀ (n : ℕ), 0 < u n<VAR>hu_strict : StrictMono u<VAR>hC_nonzero : C ≠ 0<VAR>h_succ_diff : SuccDiffBounded C u<VAR>f : ℕ → ℝ≥0<VAR>hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m<VAR>this : ∀ (k : ℕ), ↑(u (k + 1)) - ↑(u k) = ↑(↑(u (k + 1)) - ↑(u k))<GOAL>(Summable fun k => (↑(u (k + 1)) - ↑(u k)) * ↑(f (u k))) ↔ Summable fun i => ↑(f i)
<VAR>C : ℕ<VAR>u : ℕ → ℕ<VAR>h_pos : ∀ (n : ℕ), 0 < u n<VAR>hu_strict : StrictMono u<VAR>hC_nonzero : C ≠ 0<VAR>h_succ_diff : SuccDiffBounded C u<VAR>f : ℕ → ℝ≥0<VAR>hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m<VAR>this : ∀ (k : ℕ), ↑(u (k + 1)) - ↑(u k) = ↑(↑(u (k + 1)) - ↑(u k))<GOAL>(Summable fun k => ↑(↑(u (k + 1)) - ↑(u k)) * ↑(f (u k))) ↔ Summable fun i => ↑(f i)
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>hv✝ hv : LinearIndependent R v<GOAL>CompleteLattice.Independent fun i => span R {v i}
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>hv✝ hv : LinearIndependent R v<VAR>i : ι<GOAL>Disjoint (span R {v i}) (⨆ j, ⨆ (_ : j ≠ i), span R {v j})
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>hv✝ hv : LinearIndependent R v<VAR>i : ι<GOAL>span R {v i} ⊓ ⨆ j, ⨆ (_ : j ≠ i), span R {v j} ≤ ⊥
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>hv✝ hv : LinearIndependent R v<VAR>i : ι<VAR>m : M<VAR>hm : m ∈ span R {v i} ⊓ ⨆ j, ⨆ (_ : j ≠ i), span R {v j}<GOAL>m ∈ ⊥
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>hv✝ hv : LinearIndependent R v<VAR>i : ι<VAR>m : M<VAR>hm : (∃ a, a • v i = m) ∧ m ∈ ⨆ x, span R {v ↑x}<GOAL>m ∈ ⊥