ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>D : Type u_1<VAR>C : Type u_2<VAR>inst✝³ : Groupoid D<VAR>inst✝² : Category.{?u.4103, u_2} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : MonoidalClosed C<VAR>F G : D ⥤ C<VAR>X Y : D<VAR>f : X ⟶ Y<GOAL>(ihom.coev (F.obj Y)).app (G.obj X) ≫ (ihom (F.obj Y)).map (F.obj Y ◁ G.map f) = (ihom.coev (F.obj X)).app (G.obj X) ≫ (pre (CategoryTheory.inv (F.map f))).app ((F ⊗ G).obj X) ≫ (ihom (F.obj Y)).map (F.map f ⊗ G.map f)
<VAR>D : Type u_1<VAR>C : Type u_2<VAR>inst✝³ : Groupoid D<VAR>inst✝² : Category.{?u.4103, u_2} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : MonoidalClosed C<VAR>F G : D ⥤ C<VAR>X Y : D<VAR>f : X ⟶ Y<GOAL>(ihom.coev (F.obj Y)).app (G.obj X) ≫ (ihom (F.obj Y)).map (F.obj Y ◁ G.map f) = (ihom.coev (F.obj X)).app (G.obj X) ≫ (pre (CategoryTheory.inv (F.map f))).app (F.obj X ⊗ G.obj X) ≫ (ihom (F.obj Y)).map (F.map f ⊗ G.map f)
<VAR>D : Type u_1<VAR>C : Type u_2<VAR>inst✝³ : Groupoid D<VAR>inst✝² : Category.{?u.4103, u_2} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : MonoidalClosed C<VAR>F G : D ⥤ C<VAR>X Y : D<VAR>f : X ⟶ Y<GOAL>(ihom.coev (F.obj Y)).app (G.obj X) ≫ (ihom (F.obj Y)).map (F.obj Y ◁ G.map f) = (ihom.coev (F.obj Y)).app (G.obj X) ≫ (ihom (F.obj Y)).map (CategoryTheory.inv (F.map f) ▷ G.obj X ≫ F.map f ▷ G.obj X ≫ F.obj Y ◁ G.map f)
<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>y : E<GOAL>HasFDerivWithinAt f f' (insert y s) x ↔ HasFDerivWithinAt f f' s x
<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<GOAL>HasFDerivWithinAt f f' (insert x s) x ↔ HasFDerivWithinAt f f' s x
<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>y : E<VAR>h : x ≠ y<GOAL>HasFDerivWithinAt f f' (insert y s) x ↔ HasFDerivWithinAt f f' s x
<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>y : E<VAR>h : x ≠ y<VAR>hf : HasFDerivWithinAt f f' s x<GOAL>s ∈ 𝓝[insert y s] x
<VAR>ι : Type u<VAR>α : Type v<VAR>inst✝¹ : DecidableEq α<VAR>t : ι → Finset α<VAR>inst✝ : Finite ι<VAR>ht : ∀ (s : Finset ι), s.card ≤ (s.biUnion t).card<GOAL>∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
<VAR>ι : Type u<VAR>α : Type v<VAR>inst✝¹ : DecidableEq α<VAR>t : ι → Finset α<VAR>inst✝ : Finite ι<VAR>ht : ∀ (s : Finset ι), s.card ≤ (s.biUnion t).card<VAR>val✝ : Fintype ι<GOAL>∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
<VAR>α : Type v<VAR>inst✝¹ : DecidableEq α<VAR>n : ℕ<VAR>ih : ∀ m < n, ∀ {ι : Type u} {t : ι → Finset α} [inst : Finite ι], (∀ (s : Finset ι), s.card ≤ (s.biUnion t).card) → ∀ (val : Fintype ι), Fintype.card ι = m → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x<VAR>ι : Type u<VAR>t : ι → Finset α<VAR>inst✝ : Finite ι<VAR>ht : ∀ (s : Finset ι), s.card ≤ (s.biUnion t).card<VAR>val✝ : Fintype ι<VAR>hn : Fintype.card ι = n<GOAL>∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R[X]<VAR>inst✝ : Algebra R S<VAR>h : IsAdjoinRoot S f<VAR>x : R<GOAL>(algebraMap R S) x = h.map (C x)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>g : β → γ<VAR>hg : UniformInducing g<VAR>f : α → β<VAR>hf : UniformInducing f<GOAL>comap (fun x => ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 γ) = 𝓤 α
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>g : β → γ<VAR>hg : UniformInducing g<VAR>f : α → β<VAR>hf : UniformInducing f<GOAL>comap (fun x => ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 γ) = comap ((fun x => (g x.1, g x.2)) ∘ fun x => (f x.1, f x.2)) (𝓤 γ)
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : TopologicalSpace Y<VAR>inst✝⁴ : Monoid M<VAR>inst✝³ : MulAction M X<VAR>inst✝² : ContinuousSMul M X<VAR>N : Type u_5<VAR>inst✝¹ : TopologicalSpace N<VAR>inst✝ : Monoid N<VAR>f : N →* M<VAR>hf : Continuous ⇑f<VAR>x✝ : MulAction N X := compHom X f<GOAL>ContinuousSMul N X
<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<GOAL>mrange (inl M N) = ⊤.prod ⊥
<VAR>α : Sort u_1<VAR>f : Bool → α<VAR>H : f false ≠ f true<VAR>hxy : f false = f false<GOAL>false = false
<VAR>α : Sort u_1<VAR>f : Bool → α<VAR>H : f false ≠ f true<VAR>hxy : f false = f true<GOAL>false = true
<VAR>α : Sort u_1<VAR>f : Bool → α<VAR>H : f false ≠ f true<VAR>hxy : f true = f false<GOAL>true = false
<VAR>α : Sort u_1<VAR>f : Bool → α<VAR>H : f false ≠ f true<VAR>hxy : f true = f true<GOAL>true = true
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝³ : OrderedCancelAddCommMonoid α<VAR>inst✝² : ExistsAddOfLE α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>inst✝ : DecidableEq α<VAR>a b c : α<GOAL>image (fun x => x + c) (Icc a b) = Icc (a + c) (b + c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁵ : GroupWithZero α<VAR>inst✝⁴ : Preorder α<VAR>inst✝³ : Preorder β<VAR>inst✝² : MulAction α β<VAR>inst✝¹ : PosSMulStrictMono α β<VAR>inst✝ : PosSMulReflectLT α β<VAR>ha : 0 < a<GOAL>b₁ < a⁻¹ • b₂ ↔ a • b₁ < b₂
<VAR>r p q a b x✝¹ : ℝ≥0<VAR>ac : ↑a < ↑x✝¹<VAR>x✝ : ℝ≥0<VAR>bd : ↑b < ↑x✝<GOAL>↑a + ↑b < ↑x✝¹ + ↑x✝
<VAR>r p q a b x✝¹ x✝ : ℝ≥0<VAR>ac : a < x✝¹<VAR>bd : b < x✝<GOAL>a + b < x✝¹ + x✝
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f✝ g : α✝ → ℝ≥0∞<VAR>α : Type u_4<VAR>f : α → ℝ≥0∞<VAR>hf : ∑' (x : α), f x ≠ ⊤<GOAL>Tendsto f cofinite (𝓝 0)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f✝ g : α✝ → ℝ≥0∞<VAR>α : Type u_4<VAR>f : α → ℝ≥0∞<VAR>hf : ∑' (x : α), f x ≠ ⊤<VAR>f_ne_top : ∀ (n : α), f n ≠ ⊤<GOAL>Tendsto f cofinite (𝓝 0)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f✝ g : α✝ → ℝ≥0∞<VAR>α : Type u_4<VAR>f : α → ℝ≥0∞<VAR>hf : ∑' (x : α), f x ≠ ⊤<VAR>f_ne_top : ∀ (n : α), f n ≠ ⊤<VAR>h_f_coe : f = fun n => ↑(f n).toNNReal<GOAL>Tendsto f cofinite (𝓝 0)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f✝ g : α✝ → ℝ≥0∞<VAR>α : Type u_4<VAR>f : α → ℝ≥0∞<VAR>hf : ∑' (x : α), f x ≠ ⊤<VAR>f_ne_top : ∀ (n : α), f n ≠ ⊤<VAR>h_f_coe : f = fun n => ↑(f n).toNNReal<GOAL>Tendsto (fun n => (f n).toNNReal) cofinite (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>G : Type u_5<VAR>inst✝¹⁶ : TopologicalSpace α<VAR>inst✝¹⁵ : AddCommGroup α<VAR>inst✝¹⁴ : TopologicalAddGroup α<VAR>inst✝¹³ : TopologicalSpace β<VAR>inst✝¹² : AddCommGroup β<VAR>inst✝¹¹ : TopologicalAddGroup β<VAR>inst✝¹⁰ : TopologicalSpace γ<VAR>inst✝⁹ : AddCommGroup γ<VAR>inst✝⁸ : TopologicalAddGroup γ<VAR>inst✝⁷ : TopologicalSpace δ<VAR>inst✝⁶ : AddCommGroup δ<VAR>inst✝⁵ : TopologicalAddGroup δ<VAR>inst✝⁴ : UniformSpace G<VAR>inst✝³ : AddCommGroup G<VAR>inst✝² : UniformAddGroup G<VAR>inst✝¹ : T0Space G<VAR>inst✝ : CompleteSpace G<VAR>e : β →+ α<VAR>de : DenseInducing ⇑e<VAR>f : δ →+ γ<VAR>df : DenseInducing ⇑f<VAR>φ : β →+ δ →+ G<VAR>hφ : Continuous fun p => (φ p.1) p.2<VAR>W' : Set G<VAR>W'_nhd : W' ∈ 𝓝 0<VAR>x₀ : α<VAR>y₁ : δ<VAR>Nx : Filter α := 𝓝 x₀<VAR>ee : β × β → α × α := fun u => (e u.1, e u.2)<GOAL>∃ U₂ ∈ comap (⇑e) (𝓝 x₀), ∀ x ∈ U₂, ∀ x' ∈ U₂, (fun p => (φ p.1) p.2) (x' - x, y₁) ∈ W'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>G : Type u_5<VAR>inst✝¹⁶ : TopologicalSpace α<VAR>inst✝¹⁵ : AddCommGroup α<VAR>inst✝¹⁴ : TopologicalAddGroup α<VAR>inst✝¹³ : TopologicalSpace β<VAR>inst✝¹² : AddCommGroup β<VAR>inst✝¹¹ : TopologicalAddGroup β<VAR>inst✝¹⁰ : TopologicalSpace γ<VAR>inst✝⁹ : AddCommGroup γ<VAR>inst✝⁸ : TopologicalAddGroup γ<VAR>inst✝⁷ : TopologicalSpace δ<VAR>inst✝⁶ : AddCommGroup δ<VAR>inst✝⁵ : TopologicalAddGroup δ<VAR>inst✝⁴ : UniformSpace G<VAR>inst✝³ : AddCommGroup G<VAR>inst✝² : UniformAddGroup G<VAR>inst✝¹ : T0Space G<VAR>inst✝ : CompleteSpace G<VAR>e : β →+ α<VAR>de : DenseInducing ⇑e<VAR>f : δ →+ γ<VAR>df : DenseInducing ⇑f<VAR>φ : β →+ δ →+ G<VAR>hφ : Continuous fun p => (φ p.1) p.2<VAR>W' : Set G<VAR>W'_nhd : W' ∈ 𝓝 0<VAR>x₀ : α<VAR>y₁ : δ<VAR>Nx : Filter α := 𝓝 x₀<VAR>ee : β × β → α × α := fun u => (e u.1, e u.2)<VAR>lim1 : Tendsto (fun a => (a.2 - a.1, y₁)) (comap (⇑e) Nx ×ˢ comap (⇑e) Nx) (𝓝 (0, y₁))<GOAL>∃ U₂ ∈ comap (⇑e) (𝓝 x₀), ∀ x ∈ U₂, ∀ x' ∈ U₂, (fun p => (φ p.1) p.2) (x' - x, y₁) ∈ W'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>G : Type u_5<VAR>inst✝¹⁶ : TopologicalSpace α<VAR>inst✝¹⁵ : AddCommGroup α<VAR>inst✝¹⁴ : TopologicalAddGroup α<VAR>inst✝¹³ : TopologicalSpace β<VAR>inst✝¹² : AddCommGroup β<VAR>inst✝¹¹ : TopologicalAddGroup β<VAR>inst✝¹⁰ : TopologicalSpace γ<VAR>inst✝⁹ : AddCommGroup γ<VAR>inst✝⁸ : TopologicalAddGroup γ<VAR>inst✝⁷ : TopologicalSpace δ<VAR>inst✝⁶ : AddCommGroup δ<VAR>inst✝⁵ : TopologicalAddGroup δ<VAR>inst✝⁴ : UniformSpace G<VAR>inst✝³ : AddCommGroup G<VAR>inst✝² : UniformAddGroup G<VAR>inst✝¹ : T0Space G<VAR>inst✝ : CompleteSpace G<VAR>e : β →+ α<VAR>de : DenseInducing ⇑e<VAR>f : δ →+ γ<VAR>df : DenseInducing ⇑f<VAR>φ : β →+ δ →+ G<VAR>hφ : Continuous fun p => (φ p.1) p.2<VAR>W' : Set G<VAR>W'_nhd : W' ∈ 𝓝 0<VAR>x₀ : α<VAR>y₁ : δ<VAR>Nx : Filter α := 𝓝 x₀<VAR>ee : β × β → α × α := fun u => (e u.1, e u.2)<VAR>lim1 : Tendsto (fun a => (a.2 - a.1, y₁)) (comap (⇑e) Nx ×ˢ comap (⇑e) Nx) (𝓝 (0, y₁))<VAR>lim2 : Tendsto (fun p => (φ p.1) p.2) (𝓝 (0, y₁)) (𝓝 0)<GOAL>∃ U₂ ∈ comap (⇑e) (𝓝 x₀), ∀ x ∈ U₂, ∀ x' ∈ U₂, (fun p => (φ p.1) p.2) (x' - x, y₁) ∈ W'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>G : Type u_5<VAR>inst✝¹⁶ : TopologicalSpace α<VAR>inst✝¹⁵ : AddCommGroup α<VAR>inst✝¹⁴ : TopologicalAddGroup α<VAR>inst✝¹³ : TopologicalSpace β<VAR>inst✝¹² : AddCommGroup β<VAR>inst✝¹¹ : TopologicalAddGroup β<VAR>inst✝¹⁰ : TopologicalSpace γ<VAR>inst✝⁹ : AddCommGroup γ<VAR>inst✝⁸ : TopologicalAddGroup γ<VAR>inst✝⁷ : TopologicalSpace δ<VAR>inst✝⁶ : AddCommGroup δ<VAR>inst✝⁵ : TopologicalAddGroup δ<VAR>inst✝⁴ : UniformSpace G<VAR>inst✝³ : AddCommGroup G<VAR>inst✝² : UniformAddGroup G<VAR>inst✝¹ : T0Space G<VAR>inst✝ : CompleteSpace G<VAR>e : β →+ α<VAR>de : DenseInducing ⇑e<VAR>f : δ →+ γ<VAR>df : DenseInducing ⇑f<VAR>φ : β →+ δ →+ G<VAR>hφ : Continuous fun p => (φ p.1) p.2<VAR>W' : Set G<VAR>W'_nhd : W' ∈ 𝓝 0<VAR>x₀ : α<VAR>y₁ : δ<VAR>Nx : Filter α := 𝓝 x₀<VAR>ee : β × β → α × α := fun u => (e u.1, e u.2)<VAR>lim1 : Tendsto (fun a => (a.2 - a.1, y₁)) (comap (⇑e) Nx ×ˢ comap (⇑e) Nx) (𝓝 (0, y₁))<VAR>lim2 : Tendsto (fun p => (φ p.1) p.2) (𝓝 (0, y₁)) (𝓝 0)<VAR>lim : Tendsto ((fun p => (φ p.1) p.2) ∘ fun a => (a.2 - a.1, y₁)) (comap (⇑e) Nx ×ˢ comap (⇑e) Nx) (𝓝 0)<GOAL>∃ U₂ ∈ comap (⇑e) (𝓝 x₀), ∀ x ∈ U₂, ∀ x' ∈ U₂, (fun p => (φ p.1) p.2) (x' - x, y₁) ∈ W'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>G : Type u_5<VAR>inst✝¹⁶ : TopologicalSpace α<VAR>inst✝¹⁵ : AddCommGroup α<VAR>inst✝¹⁴ : TopologicalAddGroup α<VAR>inst✝¹³ : TopologicalSpace β<VAR>inst✝¹² : AddCommGroup β<VAR>inst✝¹¹ : TopologicalAddGroup β<VAR>inst✝¹⁰ : TopologicalSpace γ<VAR>inst✝⁹ : AddCommGroup γ<VAR>inst✝⁸ : TopologicalAddGroup γ<VAR>inst✝⁷ : TopologicalSpace δ<VAR>inst✝⁶ : AddCommGroup δ<VAR>inst✝⁵ : TopologicalAddGroup δ<VAR>inst✝⁴ : UniformSpace G<VAR>inst✝³ : AddCommGroup G<VAR>inst✝² : UniformAddGroup G<VAR>inst✝¹ : T0Space G<VAR>inst✝ : CompleteSpace G<VAR>e : β →+ α<VAR>de : DenseInducing ⇑e<VAR>f : δ →+ γ<VAR>df : DenseInducing ⇑f<VAR>φ : β →+ δ →+ G<VAR>hφ : Continuous fun p => (φ p.1) p.2<VAR>W' : Set G<VAR>W'_nhd : W' ∈ 𝓝 0<VAR>x₀ : α<VAR>y₁ : δ<VAR>Nx : Filter α := 𝓝 x₀<VAR>ee : β × β → α × α := fun u => (e u.1, e u.2)<VAR>lim1 : Tendsto (fun a => (a.2 - a.1, y₁)) (comap (⇑e) Nx ×ˢ comap (⇑e) Nx) (𝓝 (0, y₁))<VAR>lim2 : Tendsto (fun p => (φ p.1) p.2) (𝓝 (0, y₁)) (𝓝 0)<VAR>lim : ∀ W ∈ 𝓝 0, ∃ U ∈ comap (⇑e) Nx, ∀ (x x' : β), x ∈ U → x' ∈ U → ((fun p => (φ p.1) p.2) ∘ fun a => (a.2 - a.1, y₁)) (x, x') ∈ W<GOAL>∃ U₂ ∈ comap (⇑e) (𝓝 x₀), ∀ x ∈ U₂, ∀ x' ∈ U₂, (fun p => (φ p.1) p.2) (x' - x, y₁) ∈ W'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>G : Type u_5<VAR>inst✝¹⁶ : TopologicalSpace α<VAR>inst✝¹⁵ : AddCommGroup α<VAR>inst✝¹⁴ : TopologicalAddGroup α<VAR>inst✝¹³ : TopologicalSpace β<VAR>inst✝¹² : AddCommGroup β<VAR>inst✝¹¹ : TopologicalAddGroup β<VAR>inst✝¹⁰ : TopologicalSpace γ<VAR>inst✝⁹ : AddCommGroup γ<VAR>inst✝⁸ : TopologicalAddGroup γ<VAR>inst✝⁷ : TopologicalSpace δ<VAR>inst✝⁶ : AddCommGroup δ<VAR>inst✝⁵ : TopologicalAddGroup δ<VAR>inst✝⁴ : UniformSpace G<VAR>inst✝³ : AddCommGroup G<VAR>inst✝² : UniformAddGroup G<VAR>inst✝¹ : T0Space G<VAR>inst✝ : CompleteSpace G<VAR>e : β →+ α<VAR>de : DenseInducing ⇑e<VAR>f : δ →+ γ<VAR>df : DenseInducing ⇑f<VAR>φ : β →+ δ →+ G<VAR>hφ : Continuous fun p => (φ p.1) p.2<VAR>W' : Set G<VAR>W'_nhd : W' ∈ 𝓝 0<VAR>x₀ : α<VAR>y₁ : δ<VAR>Nx : Filter α := 𝓝 x₀<VAR>ee : β × β → α × α := fun u => (e u.1, e u.2)<VAR>lim1 : Tendsto (fun a => (a.2 - a.1, y₁)) (comap (⇑e) Nx ×ˢ comap (⇑e) Nx) (𝓝 (0, y₁))<VAR>lim2 : Tendsto (fun p => (φ p.1) p.2) (𝓝 (0, y₁)) (𝓝 0)<VAR>lim : ∀ W ∈ 𝓝 0, ∃ U ∈ comap (⇑e) Nx, ∀ (x x' : β), x ∈ U → x' ∈ U → ((fun p => (φ p.1) p.2) ∘ fun a => (a.2 - a.1, y₁)) (x, x') ∈ W<GOAL>∃ U₂ ∈ comap (⇑e) (𝓝 x₀), ∀ (a b : β), a ∈ U₂ → b ∈ U₂ → (φ (b - a)) y₁ ∈ W'
<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>L : C ⥤ D<VAR>inst✝¹ : L.IsLocalization W<VAR>X Y : C<VAR>f : Y ⟶ X<VAR>hf : W f<VAR>inst✝ : HasSmallLocalizedHom W X Y<GOAL>(equiv W L) (mkInv f hf) = (isoOfHom L W f hf).inv
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Add α<VAR>inst✝¹ : Semigroup α<VAR>inst✝ : LeftDistribClass α<VAR>a b c : α<VAR>h₁ : a ∣ b<VAR>h₂ : a ∣ c<VAR>d : α<VAR>hd : b = a * d<VAR>e : α<VAR>he : c = a * e<GOAL>a * (d + e) = b + c
<VAR>a b c d k m : ℕ<VAR>h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = k * m<VAR>ha : 2 * a < m<VAR>hb : 2 * b < m<VAR>hc : 2 * c < m<VAR>hd : 2 * d < m<GOAL>k < m
<VAR>a b c d k m : ℕ<VAR>h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = k * m<VAR>ha : 2 * a < m<VAR>hb : 2 * b < m<VAR>hc : 2 * c < m<VAR>hd : 2 * d < m<GOAL>2 ^ 2 * (k * m) < 2 ^ 2 * (m * m)
<VAR>L : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : IsGalois K L<VAR>x : 𝓞 L<GOAL>x ∣ (algebraMap (𝓞 K) (𝓞 L)) ((norm K) x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : MeasurableSingletonClass α<VAR>a : α<VAR>s : Set α<VAR>h : a ∉ s<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (x : α) in insert a s, f x ∂μ = f a * μ {a} + ∫⁻ (x : α) in s, f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : MeasurableSingletonClass α<VAR>a : α<VAR>s : Set α<VAR>h : a ∉ s<VAR>f : α → ℝ≥0∞<GOAL>Disjoint s {a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>x : ℝ<GOAL>(hf.stieltjesFunction a).measure (Iic x) = ENNReal.ofReal (↑(hf.stieltjesFunction a) x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>x : ℝ<GOAL>(hf.stieltjesFunction a).measure (Iic x) = ENNReal.ofReal (↑(hf.stieltjesFunction a) x - 0)
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>φ ψ : R[X]<GOAL>↑1 = 1
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>φ ψ : R[X]<VAR>this : ↑((monomial 0) 1) = (PowerSeries.monomial R 0) 1<GOAL>↑1 = 1
<VAR>R : Type u_1<VAR>inst✝¹³ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝¹² : CommRing S<VAR>inst✝¹¹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹⁰ : CommRing P<VAR>Rₘ : Type u_4<VAR>Sₘ : Type u_5<VAR>inst✝⁹ : CommRing Rₘ<VAR>inst✝⁸ : CommRing Sₘ<VAR>inst✝⁷ : Algebra R Rₘ<VAR>inst✝⁶ : IsLocalization M Rₘ<VAR>inst✝⁵ : Algebra S Sₘ<VAR>i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<VAR>inst✝⁴ : Algebra Rₘ Sₘ<VAR>inst✝³ : Algebra R Sₘ<VAR>inst✝² : IsScalarTower R Rₘ Sₘ<VAR>inst✝¹ : IsScalarTower R S Sₘ<VAR>inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<VAR>y : ↥M<GOAL>IsUnit ((algebraMap R Sₘ) ↑y)
<VAR>R : Type u_1<VAR>inst✝¹³ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝¹² : CommRing S<VAR>inst✝¹¹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹⁰ : CommRing P<VAR>Rₘ : Type u_4<VAR>Sₘ : Type u_5<VAR>inst✝⁹ : CommRing Rₘ<VAR>inst✝⁸ : CommRing Sₘ<VAR>inst✝⁷ : Algebra R Rₘ<VAR>inst✝⁶ : IsLocalization M Rₘ<VAR>inst✝⁵ : Algebra S Sₘ<VAR>i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<VAR>inst✝⁴ : Algebra Rₘ Sₘ<VAR>inst✝³ : Algebra R Sₘ<VAR>inst✝² : IsScalarTower R Rₘ Sₘ<VAR>inst✝¹ : IsScalarTower R S Sₘ<VAR>inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<VAR>y : ↥M<GOAL>IsUnit ((algebraMap S Sₘ) ((algebraMap R S) ↑y))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>h : ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → (a / (a + b)) • x + (b / (a + b)) • y ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<VAR>h' : 0 < a + b → (a / (a + b)) • x + (b / (a + b)) • y ∈ s<GOAL>a • x + b • y ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>h : ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → (a / (a + b)) • x + (b / (a + b)) • y ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<VAR>h' : 0 < 1 → a • x + b • y ∈ s<GOAL>a • x + b • y ∈ s
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<GOAL>(𝓝 0).HasBasis (fun s => s ∈ p.basisSets) id
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : C<VAR>f g : X ⟶ Y<VAR>inst✝ : HasEqualizer f g<VAR>W : C<VAR>h : W ⟶ X<VAR>w : (equalizerSubobject f g).Factors h<GOAL>h ≫ f = h ≫ g
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : ConditionallyCompleteLinearOrderBot ι<VAR>a b : ℝ<VAR>f : ι → Ω → ℝ<VAR>N : ι<VAR>n m : ℕ<VAR>ω : Ω<GOAL>lowerCrossingTime a b f N n ω ≤ upperCrossingTime a b f N (n + 1) ω
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : ConditionallyCompleteLinearOrderBot ι<VAR>a b : ℝ<VAR>f : ι → Ω → ℝ<VAR>N : ι<VAR>n m : ℕ<VAR>ω : Ω<GOAL>lowerCrossingTime a b f N n ω ≤ hitting f (Set.Ici b) (lowerCrossingTimeAux a f (upperCrossingTime a b f N n ω) N ω) N ω
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<VAR>r s : R<GOAL>Submodule.span R {r} * Submodule.span R {s} = Submodule.span R {r * s}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>R S : α → β → Prop<VAR>P : γ → δ → Prop<VAR>Rₐ : α → α → Prop<VAR>hr : BiUnique R<VAR>a : α<VAR>b : β<VAR>x✝ : R a b<GOAL>(fun x x_1 => x ∈ x_1) a [] ↔ (fun x x_1 => x ∈ x_1) b []
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>R S : α → β → Prop<VAR>P : γ → δ → Prop<VAR>Rₐ : α → α → Prop<VAR>hr : BiUnique R<VAR>a : α<VAR>b : β<VAR>h : R a b<VAR>a' : α<VAR>as : List α<VAR>b' : β<VAR>bs : List β<VAR>h₁ : R a' b'<VAR>h₂ : Forall₂ R as bs<GOAL>(fun x x_1 => x ∈ x_1) a (a' :: as) ↔ (fun x x_1 => x ∈ x_1) b (b' :: bs)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>R S : α → β → Prop<VAR>P : γ → δ → Prop<VAR>Rₐ : α → α → Prop<VAR>hr : BiUnique R<VAR>a : α<VAR>b : β<VAR>h : R a b<VAR>a' : α<VAR>as : List α<VAR>b' : β<VAR>bs : List β<VAR>h₁ : R a' b'<VAR>h₂ : Forall₂ R as bs<GOAL>a = a' ∨ a ∈ as ↔ b = b' ∨ b ∈ bs
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<GOAL>⁅I ⊔ J, N⁆ = ⁅I, N⁆ ⊔ ⁅J, N⁆
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<VAR>h : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆<GOAL>⁅I ⊔ J, N⁆ = ⁅I, N⁆ ⊔ ⁅J, N⁆
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<VAR>h : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆<GOAL>⁅I ⊔ J, N⁆ ≤ ⁅I, N⁆ ⊔ ⁅J, N⁆
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<VAR>h : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆<GOAL>{m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑(⁅I, N⁆ ⊔ ⁅J, N⁆)