ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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 ∈ span R (range fun x => v ↑x)<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>r : R<VAR>hm : r • v i ∈ span R (range fun x => v ↑x)<GOAL>r = 0
<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>r : R<VAR>hm : r • v i ∈ span R (range fun x => v ↑x)<GOAL>r • v i ∈ span R (v '' (univ \ {i}))
<VAR>R : Type u<VAR>ι✝ : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>I✝ J K L : Ideal R<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>I : ι → R<VAR>hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)<GOAL>⨅ i, span {I i} = span {∏ i : ι, I i}
<VAR>R : Type u<VAR>ι✝ : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>I✝ J K L : Ideal R<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>I : ι → R<VAR>hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)<GOAL>(↑Finset.univ).Pairwise (IsCoprime on I)
<VAR>α✝ : Type u<VAR>m n o : ℕ<VAR>m' : Type u_1<VAR>n' : Type u_2<VAR>o' : Type u_3<VAR>α : Type u_4<VAR>h : 0 = 0 + 0<GOAL>vecAlt0 h ![] = ![]
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>K✝ : Type u_1<VAR>inst✝² : Category.{?u.119287, u_1} K✝<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.119294, u_2} D<VAR>K : Type u_3<VAR>inst✝ : Category.{u_4, u_3} K<VAR>e : J ≌ K<VAR>F : K ⥤ C<VAR>c : Cocone F<VAR>hc : IsUniversalColimit c<VAR>F' : J ⥤ C<VAR>c' : Cocone F'<VAR>α : F' ⟶ e.functor ⋙ F<VAR>f : c'.pt ⟶ (Cocone.whisker e.functor c).pt<VAR>e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j)<GOAL>Nonempty (IsColimit c')
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>K✝ : Type u_1<VAR>inst✝² : Category.{?u.119287, u_1} K✝<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.119294, u_2} D<VAR>K : Type u_3<VAR>inst✝ : Category.{u_4, u_3} K<VAR>e : J ≌ K<VAR>F : K ⥤ C<VAR>c : Cocone F<VAR>hc : IsUniversalColimit c<VAR>F' : J ⥤ C<VAR>c' : Cocone F'<VAR>α : F' ⟶ e.functor ⋙ F<VAR>f : c'.pt ⟶ (Cocone.whisker e.functor c).pt<VAR>e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j)<GOAL>Nonempty (IsColimit c') ↔ Nonempty (IsColimit (Cocone.whisker e.inverse c'))
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>K✝ : Type u_1<VAR>inst✝² : Category.{?u.119287, u_1} K✝<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.119294, u_2} D<VAR>K : Type u_3<VAR>inst✝ : Category.{u_4, u_3} K<VAR>e : J ≌ K<VAR>F : K ⥤ C<VAR>c : Cocone F<VAR>hc : IsUniversalColimit c<VAR>F' : J ⥤ C<VAR>c' : Cocone F'<VAR>α : F' ⟶ e.functor ⋙ F<VAR>f : c'.pt ⟶ (Cocone.whisker e.functor c).pt<VAR>e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j)<GOAL>(whiskerLeft e.inverse α ≫ (e.invFunIdAssoc F).hom) ≫ c.ι = (Cocone.whisker e.inverse c').ι ≫ (Functor.const K).map f
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>K✝ : Type u_1<VAR>inst✝² : Category.{?u.119287, u_1} K✝<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.119294, u_2} D<VAR>K : Type u_3<VAR>inst✝ : Category.{u_4, u_3} K<VAR>e : J ≌ K<VAR>F : K ⥤ C<VAR>c : Cocone F<VAR>hc : IsUniversalColimit c<VAR>F' : J ⥤ C<VAR>c' : Cocone F'<VAR>α : F' ⟶ e.functor ⋙ F<VAR>f : c'.pt ⟶ (Cocone.whisker e.functor c).pt<VAR>e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j)<GOAL>∀ (j : K), IsPullback ((Cocone.whisker e.inverse c').ι.app j) ((whiskerLeft e.inverse α ≫ (e.invFunIdAssoc F).hom).app j) f (c.ι.app j)
<VAR>a x z : ℂ<VAR>θ : Real.Angle<GOAL>↑(↑θ.cos + ↑θ.sin * I).arg = θ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>s t : Set α<VAR>a b x y : α<VAR>hf : f.IsCycleOn s<VAR>hx : f x ∈ s<GOAL>x ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>s t : Set α<VAR>a b x y : α<VAR>hf : f.IsCycleOn s<VAR>hx : f x ∈ s<GOAL>x = f⁻¹ (f x)
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LE α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>1 ≤ a * b⁻¹ ↔ b ≤ a
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootSystem ι R M N<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>P₁ P₂ : RootSystem ι R M N<VAR>he : P₁.toLin = P₂.toLin<VAR>hr : P₁.root = P₂.root<GOAL>P₁ = P₂
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootSystem ι R M N<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>P₁ P₂ : RootSystem ι R M N<VAR>he : P₁.toLin = P₂.toLin<VAR>hr : P₁.root = P₂.root<GOAL>∀ (P₁ P₂ : RootSystem ι R M N), P₁.toLin = P₂.toLin → P₁.root = P₂.root → range ⇑P₁.coroot ⊆ range ⇑P₂.coroot
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootSystem ι R M N<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>P₁ P₂ : RootSystem ι R M N<VAR>he : P₁.toLin = P₂.toLin<VAR>hr : P₁.root = P₂.root<VAR>i : ι<GOAL>P₁.coroot i ∈ range ⇑P₂.coroot
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootSystem ι R M N<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>P₁ P₂ : RootSystem ι R M N<VAR>he : P₁.toLin = P₂.toLin<VAR>hr : P₁.root = P₂.root<VAR>i : ι<GOAL>P₂.coroot i = P₁.coroot i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootSystem ι R M N<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>P₁ P₂ : RootSystem ι R M N<VAR>he : P₁.toLin = P₂.toLin<VAR>hr : P₁.root = P₂.root<VAR>i : ι<GOAL>P₁.toLin.flip (P₂.coroot i) = P₁.toLin.flip (P₁.coroot i)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootSystem ι R M N<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>P₁ P₂ : RootSystem ι R M N<VAR>he : P₁.toLin = P₂.toLin<VAR>hr : P₁.root = P₂.root<VAR>i : ι<GOAL>(P₁.toLin.flip (P₂.coroot i)) (P₁.root i) = 2
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootSystem ι R M N<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>P₁ P₂ : RootSystem ι R M N<VAR>he : P₁.toLin = P₂.toLin<VAR>hr : P₁.root = P₂.root<VAR>i : ι<GOAL>MapsTo (⇑(preReflection (P₁.root i) (P₁.toLin.flip (P₂.coroot i)))) (range ⇑P₁.root) (range ⇑P₁.root)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootSystem ι R M N<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>P₁ P₂ : RootSystem ι R M N<VAR>he : P₁.toLin = P₂.toLin<VAR>hr : P₁.root = P₂.root<VAR>i : ι<GOAL>(P₁.toLin.flip (P₁.coroot i)) (P₁.root i) = 2
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootSystem ι R M N<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>P₁ P₂ : RootSystem ι R M N<VAR>he : P₁.toLin = P₂.toLin<VAR>hr : P₁.root = P₂.root<VAR>i : ι<GOAL>MapsTo (⇑(preReflection (P₁.root i) (P₁.toLin.flip (P₁.coroot i)))) (range ⇑P₁.root) (range ⇑P₁.root)
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>x y : G → CoeSort.coe A<VAR>g : G × G<GOAL>(A.ρ g.1) (x g.2 + y g.2) - (x (g.1 * g.2) + y (g.1 * g.2)) + (x g.1 + y g.1) = (A.ρ g.1) (x g.2) - x (g.1 * g.2) + x g.1 + ((A.ρ g.1) (y g.2) - y (g.1 * g.2) + y g.1)
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>r : k<VAR>x : G → CoeSort.coe A<VAR>g : G × G<GOAL>(A.ρ g.1) (r • x g.2) - r • x (g.1 * g.2) + r • x g.1 = r • ((A.ρ g.1) (x g.2) - x (g.1 * g.2) + x g.1)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : MulAction G α<VAR>inst✝⁴ : MeasurableSpace α<VAR>ν : Measure α<VAR>inst✝³ : Countable G<VAR>inst✝² : MeasurableSpace G<VAR>inst✝¹ : SMulInvariantMeasure G α ν<VAR>inst✝ : MeasurableSMul G α<VAR>s : Set α<VAR>fund_dom_s : IsFundamentalDomain G s ν<VAR>t : Set α<VAR>fund_dom_t : IsFundamentalDomain G t ν<GOAL>Measure.map (Quotient.mk α_mod_G) (ν.restrict s) = Measure.map (Quotient.mk α_mod_G) (ν.restrict t)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>hr : r ≠ ⊤<GOAL>μ.withDensity (r • f) = r • μ.withDensity f
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>hr : r ≠ ⊤<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(μ.withDensity (r • f)) s = (r • μ.withDensity f) s
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>hr : r ≠ ⊤<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∫⁻ (a : α) in s, (r • f) a ∂μ = ∫⁻ (a : α) in s, r * f a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l✝ l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>l : Filter α<VAR>P : Set α → Prop<GOAL>l.HasBasis (fun s => s ∈ l ∧ P s) id ↔ ∀ t ∈ l, ∃ r ∈ l, P r ∧ r ⊆ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l✝ l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>l : Filter α<VAR>P : Set α → Prop<GOAL>(∀ (t : Set α), t ∈ l ↔ ∃ i ∈ l, P i ∧ i ⊆ t) ↔ ∀ t ∈ l, ∃ r ∈ l, P r ∧ r ⊆ t
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>s : PullbackCone f g<VAR>i : 𝒰.J<GOAL>(pullbackP1Iso 𝒰 f g i).inv ≫ pullback.fst (p1 𝒰 f g) (𝒰.map i) = (gluing 𝒰 f g).ι i
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>p : R[X]<GOAL>p ∈ Subring.closure (insert X {f | f.degree ≤ 0})
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>p : R[X]<GOAL>∀ (a : R), C a ∈ Subring.closure (insert X {f | f.degree ≤ 0})
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>p : R[X]<GOAL>∀ (p q : R[X]), p ∈ Subring.closure (insert X {f | f.degree ≤ 0}) → q ∈ Subring.closure (insert X {f | f.degree ≤ 0}) → p + q ∈ Subring.closure (insert X {f | f.degree ≤ 0})
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>p : R[X]<GOAL>∀ (n : ℕ) (a : R), C a * X ^ n ∈ Subring.closure (insert X {f | f.degree ≤ 0}) → C a * X ^ (n + 1) ∈ Subring.closure (insert X {f | f.degree ≤ 0})
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>x y : X<VAR>s : Set X<VAR>hxy : x ≠ y<GOAL>𝓝[insert y s] x = 𝓝[s] x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>x y : X<VAR>s : Set X<VAR>hxy : x ≠ y<VAR>t : Set X<VAR>ht : t ∈ 𝓝[s] x<GOAL>t ∈ 𝓝[insert y s] x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>x y : X<VAR>s : Set X<VAR>hxy : x ≠ y<VAR>t : Set X<VAR>ht : t ∈ 𝓝[s] x<VAR>o : Set X<VAR>ho : IsOpen o<VAR>hxo : x ∈ o<VAR>host : o ∩ s ⊆ t<GOAL>t ∈ 𝓝[insert y s] x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>x y : X<VAR>s : Set X<VAR>hxy : x ≠ y<VAR>t : Set X<VAR>ht : t ∈ 𝓝[s] x<VAR>o : Set X<VAR>ho : IsOpen o<VAR>hxo : x ∈ o<VAR>host : o ∩ s ⊆ t<GOAL>o \ {y} ∩ insert y s ⊆ t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>x y : X<VAR>s : Set X<VAR>hxy : x ≠ y<VAR>t : Set X<VAR>ht : t ∈ 𝓝[s] x<VAR>o : Set X<VAR>ho : IsOpen o<VAR>hxo : x ∈ o<VAR>host : o ∩ s ⊆ t<GOAL>o \ {y} ∩ s ⊆ t
<VAR>G : Type u_1<VAR>inst✝ : DivisionMonoid G<VAR>a b : G<VAR>h : a * b = 1<GOAL>b⁻¹ = a
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>x y z : Finmap β<GOAL>x.Disjoint (y ∪ z) ↔ x.Disjoint y ∧ x.Disjoint z
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>inst✝³ : Field k<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module k E<VAR>inst✝ : AddTorsor E PE<VAR>f : k → PE<VAR>a b : k<GOAL>(b - a) • slope f a b +ᵥ f a = f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>inst✝ : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<GOAL>Dense ↑(simpleFunc E p μ)
<VAR>x : ℝ<VAR>p : ℤ[X]<VAR>hx : Irrational x<VAR>p_nonzero : p ≠ 0<VAR>x_is_root : (aeval x) p = 0<GOAL>1 < p.natDegree
<VAR>x : ℝ<VAR>p : ℤ[X]<VAR>hx : Irrational x<VAR>p_nonzero : p ≠ 0<VAR>x_is_root : (aeval x) p = 0<VAR>rid : ¬1 < p.natDegree<GOAL>False
<VAR>x : ℝ<VAR>hx : Irrational x<VAR>a b : ℤ<VAR>p_nonzero : C a * X + C b ≠ 0<VAR>x_is_root : (aeval x) (C a * X + C b) = 0<VAR>rid : ¬1 < (C a * X + C b).natDegree<GOAL>False
<VAR>x : ℝ<VAR>hx : Irrational x<VAR>a b : ℤ<VAR>p_nonzero : C a * X + C b ≠ 0<VAR>x_is_root : (aeval x) (C a * X + C b) = 0<GOAL>False
<VAR>x : ℝ<VAR>hx : Irrational x<VAR>a b : ℤ<VAR>p_nonzero : C a * X + C b ≠ 0<VAR>x_is_root : (aeval x) (C a * X + C b) = 0<VAR>this : ↑a * x = -↑b<GOAL>False
<VAR>x : ℝ*<VAR>r : ℝ<VAR>hxr : x.IsSt r<VAR>f : ℝ → ℝ<VAR>hf : ContinuousAt f r<GOAL>IsSt (Germ.map f x) (f r)
<VAR>r : ℝ<VAR>f : ℝ → ℝ<VAR>hf : ContinuousAt f r<VAR>g : ℕ → ℝ<VAR>hxr : (ofSeq g).IsSt r<GOAL>IsSt (Germ.map f (ofSeq g)) (f r)
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>a b : ℕ<GOAL>eval (↑a + ↑b) (descPochhammer ℤ b) = ↑((a + 1).ascFactorial b)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x : 𝕎 R<VAR>m : ℕ<GOAL>truncateFun n (x ^ m) = truncateFun n x ^ m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : OpensMeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : BorelSpace β<VAR>f : α → β<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : ContinuousOn f s<VAR>hs : MeasurableSet s<VAR>a✝ : Nontrivial α<VAR>inhabited_h : Inhabited α<GOAL>AEMeasurable f (μ.restrict s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : OpensMeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : BorelSpace β<VAR>f : α → β<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : ContinuousOn f s<VAR>hs : MeasurableSet s<VAR>a✝ : Nontrivial α<VAR>inhabited_h : Inhabited α<VAR>this : (s.piecewise f fun x => f default) =ᶠ[ae (μ.restrict s)] f<GOAL>AEMeasurable f (μ.restrict s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : OpensMeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : BorelSpace β<VAR>f : α → β<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : ContinuousOn f s<VAR>hs : MeasurableSet s<VAR>a✝ : Nontrivial α<VAR>inhabited_h : Inhabited α<VAR>this : (s.piecewise f fun x => f default) =ᶠ[ae (μ.restrict s)] f<GOAL>Measurable (s.piecewise f fun x => f default)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : OpensMeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : BorelSpace β<VAR>f : α → β<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : ContinuousOn f s<VAR>hs : MeasurableSet s<VAR>a✝ : Nontrivial α<VAR>inhabited_h : Inhabited α<VAR>this : (s.piecewise f fun x => f default) =ᶠ[ae (μ.restrict s)] f<GOAL>∀ (s_1 : Set β), IsOpen s_1 → MeasurableSet ((s.piecewise f fun x => f default) ⁻¹' s_1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : OpensMeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : BorelSpace β<VAR>f : α → β<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : ContinuousOn f s<VAR>hs : MeasurableSet s<VAR>a✝ : Nontrivial α<VAR>inhabited_h : Inhabited α<VAR>this : (s.piecewise f fun x => f default) =ᶠ[ae (μ.restrict s)] f<VAR>t : Set β<VAR>ht : IsOpen t<GOAL>MeasurableSet ((s.piecewise f fun x => f default) ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : OpensMeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : BorelSpace β<VAR>f : α → β<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : ContinuousOn f s<VAR>hs : MeasurableSet s<VAR>a✝ : Nontrivial α<VAR>inhabited_h : Inhabited α<VAR>this : (s.piecewise f fun x => f default) =ᶠ[ae (μ.restrict s)] f<VAR>t : Set β<VAR>ht : IsOpen t<VAR>u : Set α<VAR>u_open : IsOpen u<VAR>hu : f ⁻¹' t ∩ s = u ∩ s<GOAL>MeasurableSet ((s.piecewise f fun x => f default) ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : OpensMeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : BorelSpace β<VAR>f : α → β<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : ContinuousOn f s<VAR>hs : MeasurableSet s<VAR>a✝ : Nontrivial α<VAR>inhabited_h : Inhabited α<VAR>this : (s.piecewise f fun x => f default) =ᶠ[ae (μ.restrict s)] f<VAR>t : Set β<VAR>ht : IsOpen t<VAR>u : Set α<VAR>u_open : IsOpen u<VAR>hu : f ⁻¹' t ∩ s = u ∩ s<GOAL>MeasurableSet (u ∩ s ∪ (fun x => f default) ⁻¹' t \ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : CompleteSpace F<VAR>u : α → ℝ<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : α → E → F<VAR>f' : α → E → E →L[𝕜] F<VAR>g g' : α → 𝕜 → F<VAR>v : ℕ → α → ℝ<VAR>s : Set E<VAR>t : Set 𝕜<VAR>x₀ x : E<VAR>y₀ y : 𝕜<VAR>N : ℕ∞<VAR>hu : Summable u<VAR>hs : IsOpen s<VAR>h's : IsPreconnected s<VAR>hf : ∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x<VAR>hf' : ∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n<VAR>hx₀ : x₀ ∈ s<VAR>hf0 : Summable fun x => f x x₀<VAR>hx : x ∈ s<VAR>this : DecidableEq α<GOAL>Summable fun n => f n x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : CompleteSpace F<VAR>u : α → ℝ<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : α → E → F<VAR>f' : α → E → E →L[𝕜] F<VAR>g g' : α → 𝕜 → F<VAR>v : ℕ → α → ℝ<VAR>s : Set E<VAR>t : Set 𝕜<VAR>x₀ x : E<VAR>y₀ y : 𝕜<VAR>N : ℕ∞<VAR>hu : Summable u<VAR>hs : IsOpen s<VAR>h's : IsPreconnected s<VAR>hf : ∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x<VAR>hf' : ∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n<VAR>hx₀ : x₀ ∈ s<VAR>hf0 : CauchySeq fun s => ∑ b ∈ s, f b x₀<VAR>hx : x ∈ s<VAR>this : DecidableEq α<GOAL>CauchySeq fun s => ∑ b ∈ s, f b x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : CompleteSpace F<VAR>u : α → ℝ<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : α → E → F<VAR>f' : α → E → E →L[𝕜] F<VAR>g g' : α → 𝕜 → F<VAR>v : ℕ → α → ℝ<VAR>s : Set E<VAR>t : Set 𝕜<VAR>x₀ x : E<VAR>y₀ y : 𝕜<VAR>N : ℕ∞<VAR>hu : Summable u<VAR>hs : IsOpen s<VAR>h's : IsPreconnected s<VAR>hf : ∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x<VAR>hf' : ∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n<VAR>hx₀ : x₀ ∈ s<VAR>hf0 : CauchySeq fun s => ∑ b ∈ s, f b x₀<VAR>hx : x ∈ s<VAR>this : DecidableEq α<VAR>A : UniformCauchySeqOn (fun t x => ∑ i ∈ t, f' i x) atTop s<GOAL>CauchySeq fun s => ∑ b ∈ s, f b x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : CompleteSpace F<VAR>u : α → ℝ<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : α → E → F<VAR>f' : α → E → E →L[𝕜] F<VAR>g g' : α → 𝕜 → F<VAR>v : ℕ → α → ℝ<VAR>s : Set E<VAR>t✝ : Set 𝕜<VAR>x₀ x : E<VAR>y₀ y✝ : 𝕜<VAR>N : ℕ∞<VAR>hu : Summable u<VAR>hs : IsOpen s<VAR>h's : IsPreconnected s<VAR>hf : ∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x<VAR>hf' : ∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n<VAR>hx₀ : x₀ ∈ s<VAR>hf0 : CauchySeq fun s => ∑ b ∈ s, f b x₀<VAR>hx : x ∈ s<VAR>this : DecidableEq α<VAR>A : UniformCauchySeqOn (fun t x => ∑ i ∈ t, f' i x) atTop s<VAR>t : Finset α<VAR>y : E<VAR>hy : y ∈ s<GOAL>HasFDerivAt ((fun t x => ∑ i ∈ t, f i x) t) (∑ i ∈ t, f' i y) y
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>P Q R : Karoubi C<VAR>g : Q.Hom R<VAR>f : P.Hom Q<GOAL>f.f ≫ g.f = P.p ≫ (f.f ≫ g.f) ≫ R.p
<VAR>R : Type u<VAR>inst✝⁶ : CommSemiring R<VAR>M : Type v<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>ι : Type w<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>κ : Type u_1<VAR>inst✝¹ : DecidableEq κ<VAR>inst✝ : Fintype κ<VAR>b : Basis ι R M<VAR>c : Basis κ R M<VAR>f g h : M →ₗ[R] M<GOAL>(trace R M) (f * (g * h)) = (trace R M) (h * (f * g))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>J : Type u_4<VAR>inst✝² : Category.{u_5, u_1} C<VAR>inst✝¹ : Category.{u_6, u_2} D<VAR>inst✝ : Category.{?u.8873, u_3} E<VAR>X Y : GradedObject J C<VAR>e : X ≅ Y<VAR>F : C ⥤ D<VAR>j : J<GOAL>F.map (e.hom j) ≫ F.map (e.inv j) = 𝟙 (F.obj (X j))