ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : CompleteSpace F<VAR>u : α → ℝ<VAR>f : α → β → F<VAR>hu : Summable u<VAR>s : Set β<VAR>hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n<VAR>ε : ℝ<VAR>εpos : ε > 0<GOAL>∀ᶠ (n : Finset α) in atTop, ∀ x ∈ s, dist (∑' (n : α), f n x) (∑ n ∈ n, f n x) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : CompleteSpace F<VAR>u : α → ℝ<VAR>f : α → β → F<VAR>hu : Summable u<VAR>s : Set β<VAR>hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>t : Finset α<VAR>ht : ∑' (a : { x // x ∉ t }), u ↑a < ε<VAR>x : β<VAR>hx : x ∈ s<GOAL>dist (∑' (n : α), f n x) (∑ n ∈ t, f n x) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : CompleteSpace F<VAR>u : α → ℝ<VAR>f : α → β → F<VAR>hu : Summable u<VAR>s : Set β<VAR>hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>t : Finset α<VAR>ht : ∑' (a : { x // x ∉ t }), u ↑a < ε<VAR>x : β<VAR>hx : x ∈ s<VAR>A : Summable fun n => ‖f n x‖<GOAL>dist (∑' (n : α), f n x) (∑ n ∈ t, f n x) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : CompleteSpace F<VAR>u : α → ℝ<VAR>f : α → β → F<VAR>hu : Summable u<VAR>s : Set β<VAR>hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>t : Finset α<VAR>ht : ∑' (a : { x // x ∉ t }), u ↑a < ε<VAR>x : β<VAR>hx : x ∈ s<VAR>A : Summable fun n => ‖f n x‖<GOAL>‖∑' (x_1 : { x // x ∉ t }), f (↑x_1) x‖ < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : CompleteSpace F<VAR>u : α → ℝ<VAR>f : α → β → F<VAR>hu : Summable u<VAR>s : Set β<VAR>hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>t : Finset α<VAR>ht : ∑' (a : { x // x ∉ t }), u ↑a < ε<VAR>x : β<VAR>hx : x ∈ s<VAR>A : Summable fun n => ‖f n x‖<GOAL>‖∑' (x_1 : { x // x ∉ t }), f (↑x_1) x‖ ≤ ∑' (a : { x // x ∉ t }), u ↑a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : CompleteSpace F<VAR>u : α → ℝ<VAR>f : α → β → F<VAR>hu : Summable u<VAR>s : Set β<VAR>hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>t : Finset α<VAR>ht : ∑' (a : { x // x ∉ t }), u ↑a < ε<VAR>x : β<VAR>hx : x ∈ s<VAR>A : Summable fun n => ‖f n x‖<GOAL>∑' (i : ↑fun x => x ∈ t → False), ‖f (↑i) x‖ ≤ ∑' (a : { x // x ∉ t }), u ↑a
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m : ℤ<VAR>n : ℕ<GOAL>LiouvilleWith p (↑r - x) ↔ LiouvilleWith p x
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : TopologicalSpace α✝<VAR>α : Type u_5<VAR>inst✝¹ : TopologicalSpace α<VAR>β : Type u_6<VAR>inst✝ : TopologicalSpace β<VAR>s u : Set α<VAR>t v : Set β<VAR>a : α<VAR>b : β<VAR>hu : u ∈ 𝓝[s] a<VAR>hv : v ∈ 𝓝[t] b<GOAL>u ×ˢ v ∈ 𝓝[s ×ˢ t] (a, b)
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : TopologicalSpace α✝<VAR>α : Type u_5<VAR>inst✝¹ : TopologicalSpace α<VAR>β : Type u_6<VAR>inst✝ : TopologicalSpace β<VAR>s u : Set α<VAR>t v : Set β<VAR>a : α<VAR>b : β<VAR>hu : u ∈ 𝓝[s] a<VAR>hv : v ∈ 𝓝[t] b<GOAL>u ×ˢ v ∈ 𝓝[s] a ×ˢ 𝓝[t] b
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝⁵ : Field 𝕜<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : DecidableEq p<VAR>inst✝² : CommRing R<VAR>r : ℕ<VAR>M✝ : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : Fintype p<VAR>M : Matrix n n 𝕜<GOAL>∃ L L' D, M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝⁵ : Field 𝕜<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : DecidableEq p<VAR>inst✝² : CommRing R<VAR>r : ℕ<VAR>M✝ : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : Fintype p<VAR>M : Matrix n n 𝕜<VAR>L L' : List (TransvectionStruct n 𝕜)<VAR>D : n → 𝕜<VAR>h : (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D<GOAL>∃ L L' D, M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝⁵ : Field 𝕜<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : DecidableEq p<VAR>inst✝² : CommRing R<VAR>r : ℕ<VAR>M✝ : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : Fintype p<VAR>M : Matrix n n 𝕜<VAR>L L' : List (TransvectionStruct n 𝕜)<VAR>D : n → 𝕜<VAR>h : (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D<GOAL>M = (List.map toMatrix (List.map TransvectionStruct.inv L.reverse)).prod * diagonal D * (List.map toMatrix (List.map TransvectionStruct.inv L'.reverse)).prod
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝⁵ : Field 𝕜<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : DecidableEq p<VAR>inst✝² : CommRing R<VAR>r : ℕ<VAR>M✝ : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : Fintype p<VAR>M : Matrix n n 𝕜<VAR>L L' : List (TransvectionStruct n 𝕜)<VAR>D : n → 𝕜<VAR>h : (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D<GOAL>M = (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod * (List.map toMatrix L).prod * M * ((List.map toMatrix L').prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod)
<VAR>α : Type u_1<VAR>g : GenContFract α<VAR>n : ℕ<GOAL>g.TerminatedAt n ↔ g.partNums.get? n = none
<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>f f' : ℝ → ℝ<VAR>hf : ∀ (x : ℝ), HasDerivAt f (f' x) x<VAR>hf' : ∀ (x : ℝ), 0 < f' x<VAR>x : ℝ<GOAL>0 < deriv f 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>f f' : ℝ → ℝ<VAR>hf : ∀ (x : ℝ), HasDerivAt f (f' x) x<VAR>hf' : ∀ (x : ℝ), 0 < f' x<VAR>x : ℝ<GOAL>0 < f' x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → ℝ<VAR>hf_nonneg : ∀ (n : α), 0 ≤ f n<VAR>hf : Summable f<GOAL>ENNReal.ofReal (∑' (n : α), f n) = ∑' (n : α), ENNReal.ofReal (f n)
<VAR>P : Type u_1<VAR>inst✝ : LE P<VAR>I✝ J s t : Ideal P<VAR>x y : P<VAR>I : Ideal P<VAR>p : P<VAR>nmem : p ∉ I<VAR>hp : ↑I = univ<GOAL>False
<VAR>P : Type u_1<VAR>inst✝ : LE P<VAR>I✝ J s t : Ideal P<VAR>x y : P<VAR>I : Ideal P<VAR>p : P<VAR>nmem : p ∉ I<VAR>hp : ↑I = univ<VAR>this : p ∈ univ<GOAL>False
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>ha : a ≠ 0<GOAL>a * b = a ↔ b = 1
<VAR>n : ℕ<GOAL>n.succ.descFactorial n.succ = n.succ !
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ✝ : Measure α<VAR>κ η : Kernel α β<VAR>μ : Measure β<VAR>inst✝ : IsFiniteMeasure μ<GOAL>dirac () ⊗ₘ Kernel.const Unit μ = map (Prod.mk ()) μ
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n : ℤ<VAR>z : Cochain F G n<GOAL>z ∈ cocycle F G n ↔ δ n (n + 1) z = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f₁ : α → β<VAR>f₂ : α → γ<VAR>g₁ : β → δ<VAR>g₂ : γ → δ<VAR>h : g₁ ∘ f₁ = g₂ ∘ f₂<VAR>a : α<GOAL>Option.map g₁ (Option.map f₁ (some a)) = Option.map g₂ (Option.map f₂ (some a))
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>hpq : p.degree ≤ q.degree<VAR>hp : p ≠ 0<GOAL>p.degree ≠ ⊥
<VAR>a : EReal<VAR>h : 0 < a<VAR>h' : a ≠ ⊤<GOAL>0 < a⁻¹
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M✝ : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹⁸ : CommSemiring R<VAR>inst✝¹⁷ : AddCommMonoid M₁<VAR>inst✝¹⁶ : Module R M₁<VAR>inst✝¹⁵ : AddCommMonoid M₂<VAR>inst✝¹⁴ : Module R M₂<VAR>inst✝¹³ : AddCommMonoid N₂<VAR>inst✝¹² : Module R N₂<VAR>inst✝¹¹ : DecidableEq n<VAR>inst✝¹⁰ : Fintype n<VAR>inst✝⁹ : DecidableEq m<VAR>inst✝⁸ : Fintype m<VAR>b₁✝ : Basis n R M₁<VAR>b₂✝ : Basis m R M₂<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis m R M₂<VAR>inst✝⁷ : AddCommMonoid M₁'<VAR>inst✝⁶ : Module R M₁'<VAR>inst✝⁵ : AddCommMonoid M₂'<VAR>inst✝⁴ : Module R M₂'<VAR>b₁' : Basis n' R M₁'<VAR>b₂' : Basis m' R M₂'<VAR>inst✝³ : Fintype n'<VAR>inst✝² : Fintype m'<VAR>inst✝¹ : DecidableEq n'<VAR>inst✝ : DecidableEq m'<VAR>B : M₁ →ₗ[R] M₂ →ₗ[R] R<VAR>M : Matrix m m' R<GOAL>(toMatrix₂ b₁ b₂) B * M = (toMatrix₂ b₁ b₂') (B.compl₂ ((toLin b₂' b₂) M))
<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>ι : Type u_4<VAR>μ : F<VAR>s : ι → Set α<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>h0 : Tendsto (fun k => μ ((⋃ n, s n) \ s k)) l (𝓝 0)<GOAL>μ (⋃ n, s n) = ⨆ n, μ (s 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>ι : Type u_4<VAR>μ : F<VAR>s : ι → Set α<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>h0 : Tendsto (fun k => μ ((⋃ n, s n) \ s k)) l (𝓝 0)<GOAL>μ (⋃ n, s n) ≤ ⨆ n, μ (s 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>ι : Type u_4<VAR>μ : F<VAR>s : ι → Set α<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>S : Set α := ⋃ n, s n<VAR>h0 : Tendsto (fun k => μ (S \ s k)) l (𝓝 0)<VAR>M : ℝ≥0∞ := ⨆ n, μ (s n)<GOAL>μ S ≤ M
<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>ι : Type u_4<VAR>μ : F<VAR>s : ι → Set α<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>S : Set α := ⋃ n, s n<VAR>h0 : Tendsto (fun k => μ (S \ s k)) l (𝓝 0)<VAR>M : ℝ≥0∞ := ⨆ n, μ (s n)<VAR>A : ∀ (k : ι), μ S ≤ M + μ (S \ s k)<GOAL>μ S ≤ M
<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>ι : Type u_4<VAR>μ : F<VAR>s : ι → Set α<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>S : Set α := ⋃ n, s n<VAR>h0 : Tendsto (fun k => μ (S \ s k)) l (𝓝 0)<VAR>M : ℝ≥0∞ := ⨆ n, μ (s n)<VAR>A : ∀ (k : ι), μ S ≤ M + μ (S \ s k)<VAR>B : Tendsto (fun k => M + μ (S \ s k)) l (𝓝 M)<GOAL>μ S ≤ M
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>M : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} M<VAR>inst✝ : MonoidalCategory M<VAR>F : MonoidalFunctor M (C ⥤ C)<VAR>n : M<VAR>X : C<GOAL>F.ε.app ((F.obj n).obj X) ≫ (F.μ n (𝟙_ M)).app X ≫ (F.map (ρ_ n).hom).app X = 𝟙 ((𝟙_ (C ⥤ C)).obj ((F.obj n).obj X))
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>M : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} M<VAR>inst✝ : MonoidalCategory M<VAR>F : MonoidalFunctor M (C ⥤ C)<VAR>n : M<VAR>X : C<VAR>this : (ρ_ (F.obj n)).hom.app X = (F.obj n ◁ F.ε ≫ F.μ n (𝟙_ M) ≫ F.map (ρ_ n).hom).app X<GOAL>F.ε.app ((F.obj n).obj X) ≫ (F.μ n (𝟙_ M)).app X ≫ (F.map (ρ_ n).hom).app X = 𝟙 ((𝟙_ (C ⥤ C)).obj ((F.obj n).obj X))
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>M : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} M<VAR>inst✝ : MonoidalCategory M<VAR>F : MonoidalFunctor M (C ⥤ C)<VAR>n : M<VAR>X : C<VAR>this : 𝟙 ((F.obj n).obj X) = F.ε.app ((F.obj n).obj X) ≫ (F.μ n (𝟙_ M)).app X ≫ (F.map (ρ_ n).hom).app X<GOAL>F.ε.app ((F.obj n).obj X) ≫ (F.μ n (𝟙_ M)).app X ≫ (F.map (ρ_ n).hom).app X = 𝟙 ((𝟙_ (C ⥤ C)).obj ((F.obj n).obj X))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDedekindDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>I J : FractionalIdeal A⁰ K<VAR>hI : I ≠ 0<VAR>hJ : J ≠ 0<GOAL>I⁻¹ ≤ J ↔ J⁻¹ ≤ I
<VAR>ι : Type u<VAR>f : ι → Scheme<VAR>i : ι<VAR>x : ↑↑(f i).toPresheafedSpace<GOAL>(TopCat.sigmaCofan fun x => (f x).toTopCat).inj i ≫ (colimit.isoColimitCocone { cocone := TopCat.sigmaCofan fun x => (f x).toTopCat, isColimit := TopCat.sigmaCofanIsColimit fun x => (f x).toTopCat }).inv ≫ (PreservesCoproduct.iso Scheme.forgetToTop f).symm.hom = Scheme.forgetToTop.map (Sigma.ι f i)
<VAR>ι : Type u<VAR>f : ι → Scheme<VAR>i : ι<VAR>x : ↑↑(f i).toPresheafedSpace<GOAL>colimit.ι (Discrete.functor fun x => (f x).toTopCat) { as := i } ≫ (PreservesCoproduct.iso Scheme.forgetToTop f).symm.hom = Scheme.forgetToTop.map (Sigma.ι f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Denumerable α<VAR>inst✝ : Denumerable β<VAR>v v₁ v₂ : ℕ<VAR>e : unpair v = (v₁, v₂)<GOAL>(Seq.seq (some fun x => ofNat α v₁ :: x) fun x => decodeList v₂) = some (ofNat α v₁ :: ofNat (List α) v₂)
<VAR>m n : ℕ<VAR>i : Fin n<GOAL>(finSuccEquiv' (Fin.last n)) i.castSucc = some 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>S : Set E<VAR>x : E<VAR>f : F<VAR>hf : (algebraMap F E) f = x<GOAL>(algebraMap F E) f ∈ ↑(adjoin F S)
<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 j : ι<GOAL>(b.toDual (b i)) (b j) = if i = j then 1 else 0
<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 j : ι<GOAL>(if j = i then 1 else 0) = if i = j then 1 else 0
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : HasContDiffBump E<VAR>inst✝⁴ : MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<VAR>n : ℕ∞<VAR>μ : Measure E<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : μ.IsOpenPosMeasure<GOAL>HasCompactSupport (f.normed μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>a b c : α<GOAL>(∀ ⦃c : α⦄, a < c → ¬c < b) ↔ Ioo a b = ∅
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>α : Type u_3<VAR>m : MeasurableSpace Ω<VAR>m' : MeasurableSpace Ω'<VAR>μ : Measure Ω<VAR>s t : Set Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>hms : MeasurableSet s<GOAL>μ[|s] t * μ s + μ[|sᶜ] t * μ sᶜ = μ t
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>α : Type u_3<VAR>m : MeasurableSpace Ω<VAR>m' : MeasurableSpace Ω'<VAR>μ : Measure Ω<VAR>s t : Set Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>hms : MeasurableSet s<GOAL>μ (t ∩ s) + μ (t ∩ sᶜ) = μ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t✝ t₁ t₂ : Set β<VAR>p : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>heq : EqOn f₁ f₂ s<VAR>t : Set β<VAR>x : α<VAR>hx : x ∈ s<GOAL>x ∈ f₁ ⁻¹' t ↔ x ∈ f₂ ⁻¹' t
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<GOAL>pseudoApply f 0 = 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<GOAL>⟦Over.mk ((Over.mk 0).hom ≫ f)⟧ = 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : OrderTopology α<VAR>f : β → α<VAR>a : α<VAR>x : Filter β<GOAL>Tendsto f x (𝓝 a) ↔ (∀ a' < a, ∀ᶠ (b : β) in x, a' < f b) ∧ ∀ a' > a, ∀ᶠ (b : β) in x, f b < a'
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : OrderTopology α<VAR>f : β → α<VAR>a : α<VAR>x : Filter β<GOAL>((∀ i ∈ Iio a, ∀ᶠ (a : β) in x, f a ∈ Ioi i) ∧ ∀ i ∈ Ioi a, ∀ᶠ (a : β) in x, f a ∈ Iio i) ↔ (∀ a' < a, ∀ᶠ (b : β) in x, a' < f b) ∧ ∀ a' > a, ∀ᶠ (b : β) in x, f b < a'
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommMonoid M'<VAR>inst✝¹ : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i : ι<VAR>c : R<VAR>x : M<VAR>inst✝ : Fintype ι<VAR>m : M<GOAL>b.sumCoords m = (∑ i : ι, b.coord i) m
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝² : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝¹ : Monoid N<VAR>inst✝ : (i : ι) → DecidableEq (M i)<VAR>i j : ι<VAR>p : Pair M i<VAR>m : M j<GOAL>⟨j, m⟩ ∈ (rcons p).toList ↔ ⟨j, m⟩ ∈ p.tail.toList ∨ m ≠ 1 ∧ ∃ (h : i = j), m = h ▸ p.head
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝² : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝¹ : Monoid N<VAR>inst✝ : (i : ι) → DecidableEq (M i)<VAR>i j : ι<VAR>p : Pair M i<VAR>m : M j<GOAL>⟨j, m⟩ ∈ (if h : p.head = 1 then p.tail else { toList := ⟨i, p.head⟩ :: p.tail.toList, ne_one := ⋯, chain_ne := ⋯ }).toList ↔ ⟨j, m⟩ ∈ p.tail.toList ∨ ¬m = 1 ∧ ∃ (h : i = j), m = h ▸ p.head
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : Nontrivial α<VAR>s : Set α<VAR>hs : IsOpen s<VAR>x : α<VAR>hx : x ∈ s<GOAL>∃ a b, a < b ∧ Ioo a b ⊆ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : Nontrivial α<VAR>s : Set α<VAR>hs : IsOpen s<VAR>x : α<VAR>hx : x ∈ s<VAR>y : α<VAR>hy : y ≠ x<GOAL>∃ a b, a < b ∧ Ioo a b ⊆ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : Nontrivial α<VAR>s : Set α<VAR>hs : IsOpen s<VAR>x : α<VAR>hx : x ∈ s<VAR>y : α<VAR>hy : y ≠ x<VAR>H : x < y<GOAL>∃ a b, a < b ∧ Ioo a b ⊆ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : Nontrivial α<VAR>s : Set α<VAR>hs : IsOpen s<VAR>x : α<VAR>hx : x ∈ s<VAR>hy : x ≠ x<GOAL>∃ a b, a < b ∧ Ioo a b ⊆ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : Nontrivial α<VAR>s : Set α<VAR>hs : IsOpen s<VAR>x : α<VAR>hx : x ∈ s<VAR>y : α<VAR>hy : y ≠ x<VAR>H : y < x<GOAL>∃ a b, a < b ∧ Ioo a b ⊆ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>hc : 0 ≤ c<VAR>hac : a ≤ c<VAR>hd : 0 < d<VAR>hbd : d ≤ b<GOAL>a / b ≤ c / d
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>hc : 0 ≤ c<VAR>hac : a ≤ c<VAR>hd : 0 < d<VAR>hbd : d ≤ b<GOAL>a * d ≤ c * b
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>h : a + c = b + d - 1<GOAL>b ≤ a ∨ d ≤ c
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>h : a + c = b + d - 1<VAR>h' : b ≤ a<GOAL>b ≤ a
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>h : a + c = b + d - 1<VAR>h' : a < b<GOAL>d ≤ c
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>x : ℕ<VAR>s : ι → ℕ<GOAL>x.Coprime (∏ i : ι, s i) ↔ ∀ (i : ι), x.Coprime (s i)
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝³ : Category.{v', u'} D<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasZeroObject C<VAR>X Y : C<VAR>inst✝ : HasImage 0<GOAL>ι 0 = 0
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝³ : Category.{v', u'} D<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasZeroObject C<VAR>X Y : C<VAR>inst✝ : HasImage 0<GOAL>lift (monoFactorisationZero X Y) ≫ (monoFactorisationZero X Y).m = 0
<VAR>a b m n✝ p✝ p d n : ℕ<VAR>hdn : d ∣ n<VAR>hpd : ¬p ∣ d<GOAL>d ∣ n / p ^ n.factorization p
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p q : 𝕜<VAR>hp : Fact (0 < p)<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>Nat.card ↑{u | addOrderOf u = n} ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : NormedAddCommGroup F<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>s : Set Ω<VAR>t : Set β<VAR>f : β × Ω → F<VAR>hX : Measurable X<VAR>hY : AEMeasurable Y μ<VAR>hs : MeasurableSet s<VAR>t' : Set β<VAR>ht' : MeasurableSet t'<GOAL>∫⁻ (a : α) in X ⁻¹' t', ((condDistrib Y X μ) (X a)) s ∂μ = μ (X ⁻¹' t' ∩ Y ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → ℝ≥0<VAR>h : Summable f<GOAL>(support f).Countable
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → ℝ≥0<VAR>h : Summable fun a => ↑(f a)<GOAL>(support f).Countable
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>F G H I : C ⥤ D<VAR>α : F ⟶ G<VAR>inst✝ : ∀ (X : C), Mono (α.app X)<VAR>Z✝ : C ⥤ D<VAR>g h : Z✝ ⟶ F<VAR>eq : g ≫ α = h ≫ α<VAR>X : C<GOAL>g.app X = h.app X
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>hts : s ⊆ t<VAR>h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0<VAR>haux : StronglyMeasurable f<VAR>h'aux : IntegrableOn f t μ<VAR>k : Set X := f ⁻¹' {0}<GOAL>∫ (x : X) in t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>hts : s ⊆ t<VAR>h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0<VAR>haux : StronglyMeasurable f<VAR>h'aux : IntegrableOn f t μ<VAR>k : Set X := f ⁻¹' {0}<VAR>hk : MeasurableSet k<GOAL>∫ (x : X) in t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>n : ℕ<VAR>a : R<VAR>this : DecidableEq R := Classical.decEq R<VAR>h : a = 0<GOAL>((monomial n) a).degree ≤ ↑n
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>n : ℕ<VAR>a : R<VAR>this : DecidableEq R := Classical.decEq R<VAR>h : a = 0<GOAL>⊥ ≤ ↑n
<VAR>k : Type u_1<VAR>inst✝⁷ : Field k<VAR>K : Type u_2<VAR>inst✝⁶ : Field K<VAR>F : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : NumberField K<VAR>inst✝³ : Algebra k K<VAR>inst✝² : Algebra k F<VAR>inst✝¹ : Algebra K F<VAR>inst✝ : IsScalarTower k K F<VAR>σ✝ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<VAR>φ : K →+* ℂ<VAR>σ : K ≃ₐ[k] K<GOAL>σ ∈ Stab (mk φ) ↔ σ = 1 ∨ ComplexEmbedding.IsConj φ σ
<VAR>k : Type u_1<VAR>inst✝⁷ : Field k<VAR>K : Type u_2<VAR>inst✝⁶ : Field K<VAR>F : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : NumberField K<VAR>inst✝³ : Algebra k K<VAR>inst✝² : Algebra k F<VAR>inst✝¹ : Algebra K F<VAR>inst✝ : IsScalarTower k K F<VAR>σ✝ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<VAR>φ : K →+* ℂ<VAR>σ : K ≃ₐ[k] K<GOAL>φ.comp ↑σ.symm = φ ∨ ComplexEmbedding.conjugate (φ.comp ↑σ.symm) = φ ↔ σ = 1 ∨ ComplexEmbedding.IsConj φ σ
<VAR>k : Type u_1<VAR>inst✝⁷ : Field k<VAR>K : Type u_2<VAR>inst✝⁶ : Field K<VAR>F : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : NumberField K<VAR>inst✝³ : Algebra k K<VAR>inst✝² : Algebra k F<VAR>inst✝¹ : Algebra K F<VAR>inst✝ : IsScalarTower k K F<VAR>σ✝ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<VAR>φ : K →+* ℂ<VAR>σ : K ≃ₐ[k] K<GOAL>φ.comp ↑σ.symm = φ ∨ star φ = φ.comp ↑σ.symm ↔ σ = 1 ∨ ComplexEmbedding.IsConj φ σ.symm
<VAR>k : Type u_1<VAR>inst✝⁷ : Field k<VAR>K : Type u_2<VAR>inst✝⁶ : Field K<VAR>F : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : NumberField K<VAR>inst✝³ : Algebra k K<VAR>inst✝² : Algebra k F<VAR>inst✝¹ : Algebra K F<VAR>inst✝ : IsScalarTower k K F<VAR>σ✝ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<VAR>φ : K →+* ℂ<VAR>σ : K ≃ₐ[k] K<VAR>H : φ.comp ↑σ.symm = φ<GOAL>σ = 1
<VAR>R : Type u_1<VAR>inst✝⁶ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra R S<VAR>P : Type u_3<VAR>inst✝³ : CommSemiring P<VAR>A : Type u_4<VAR>inst✝² : CommRing A<VAR>inst✝¹ : IsDomain A<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>inst✝ : IsLocalization.AtPrime S I<VAR>h : optParam (LocalRing S) ⋯<VAR>x : R<GOAL>x ∈ Ideal.comap (algebraMap R S) (LocalRing.maximalIdeal S) ↔ x ∈ I