ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n : ℕ<VAR>ifp_n : IntFractPair K<VAR>seq_nth_eq : IntFractPair.stream v n = some ifp_n<VAR>left✝ : ifp_n.fr ≠ 0<VAR>stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)<VAR>succ_nth_fr_eq_zero : (IntFractPair.of ifp_n.fr⁻¹).fr = 0<GOAL>∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n : ℕ<VAR>ifp_n : IntFractPair K<VAR>seq_nth_eq : IntFractPair.stream v n = some ifp_n<VAR>left✝ : ifp_n.fr ≠ 0<VAR>stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)<VAR>succ_nth_fr_eq_zero : (IntFractPair.of ifp_n.fr⁻¹).fr = 0<GOAL>ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : TopologicalSpace B<VAR>inst✝⁴ : TopologicalSpace F<VAR>E : B → Type u_5<VAR>inst✝³ : TopologicalSpace (TotalSpace F E)<VAR>inst✝² : (b : B) → TopologicalSpace (E b)<VAR>inst✝¹ : FiberBundle F E<VAR>inst✝ : T1Space B<VAR>x : B<GOAL>IsClosed (range (TotalSpace.mk x))
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : TopologicalSpace B<VAR>inst✝⁴ : TopologicalSpace F<VAR>E : B → Type u_5<VAR>inst✝³ : TopologicalSpace (TotalSpace F E)<VAR>inst✝² : (b : B) → TopologicalSpace (E b)<VAR>inst✝¹ : FiberBundle F E<VAR>inst✝ : T1Space B<VAR>x : B<GOAL>IsClosed (TotalSpace.proj ⁻¹' {x})
<GOAL>2 * π - 0 = 2 * π * ↑1
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type w<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : Small.{v, u} R<GOAL>Flat R M ↔ ∀ ⦃N N' N'' : Type v⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N''] [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄, Function.Exact ⇑f ⇑g → Function.Exact ⇑(lTensor M f) ⇑(lTensor M g)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type w<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : Small.{v, u} R<VAR>H : ∀ ⦃N N' N'' : Type v⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N''] [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄, Function.Exact ⇑f ⇑g → Function.Exact ⇑(lTensor M f) ⇑(lTensor M g)<VAR>N' N'' : Type v<VAR>x✝³ : AddCommGroup N'<VAR>x✝² : AddCommGroup N''<VAR>x✝¹ : Module R N'<VAR>x✝ : Module R N''<VAR>L : N' →ₗ[R] N''<VAR>hL : Function.Injective ⇑L<VAR>x : M ⊗[R] N'<VAR>hx : (lTensor M L) x = 0<GOAL>x ∈ ⊥
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>S : Type u_3<VAR>M₀ : Type u_4<VAR>M₁ : Type u_5<VAR>R : Type u_6<VAR>G : Type u_7<VAR>G₀ : Type u_8<VAR>inst✝⁷ : Mul M<VAR>inst✝⁶ : Monoid N<VAR>inst✝⁵ : Semigroup S<VAR>inst✝⁴ : MulZeroClass M₀<VAR>inst✝³ : MulOneClass M₁<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Group G<VAR>inst✝ : CancelMonoidWithZero G₀<VAR>p : G₀<GOAL>IsIdempotentElem p ↔ p = 0 ∨ p = 1
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>S : Type u_3<VAR>M₀ : Type u_4<VAR>M₁ : Type u_5<VAR>R : Type u_6<VAR>G : Type u_7<VAR>G₀ : Type u_8<VAR>inst✝⁷ : Mul M<VAR>inst✝⁶ : Monoid N<VAR>inst✝⁵ : Semigroup S<VAR>inst✝⁴ : MulZeroClass M₀<VAR>inst✝³ : MulOneClass M₁<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Group G<VAR>inst✝ : CancelMonoidWithZero G₀<VAR>p : G₀<VAR>h : IsIdempotentElem p<VAR>hp : ¬p = 0<GOAL>p = 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝³ : Monoid M<VAR>inst✝² : Monoid N<VAR>inst✝¹ : Monoid P<VAR>l✝ l₁ l₂ : List M<VAR>a : M<VAR>inst✝ : DecidableEq M<VAR>b : M<VAR>l : List M<VAR>ih : a ∈ l → (∀ x ∈ l, ∀ y ∈ l, x * y = y * x) → a * (l.erase a).prod = l.prod<VAR>ha : a ∈ b :: l<VAR>comm : ∀ x ∈ b :: l, ∀ y ∈ b :: l, x * y = y * x<GOAL>a * ((b :: l).erase a).prod = (b :: l).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝³ : Monoid M<VAR>inst✝² : Monoid N<VAR>inst✝¹ : Monoid P<VAR>l✝ l₁ l₂ : List M<VAR>a : M<VAR>inst✝ : DecidableEq M<VAR>l : List M<VAR>ih : a ∈ l → (∀ x ∈ l, ∀ y ∈ l, x * y = y * x) → a * (l.erase a).prod = l.prod<VAR>ha : a ∈ a :: l<VAR>comm : ∀ x ∈ a :: l, ∀ y ∈ a :: l, x * y = y * x<GOAL>a * ((a :: l).erase a).prod = (a :: l).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝³ : Monoid M<VAR>inst✝² : Monoid N<VAR>inst✝¹ : Monoid P<VAR>l✝ l₁ l₂ : List M<VAR>a : M<VAR>inst✝ : DecidableEq M<VAR>b : M<VAR>l : List M<VAR>ih : a ∈ l → (∀ x ∈ l, ∀ y ∈ l, x * y = y * x) → a * (l.erase a).prod = l.prod<VAR>ha : a ∈ b :: l<VAR>comm : ∀ x ∈ b :: l, ∀ y ∈ b :: l, x * y = y * x<VAR>ne : a ≠ b<VAR>h : a ∈ l<GOAL>a * ((b :: l).erase a).prod = (b :: l).prod
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁵ : AddCommMonoid A<VAR>inst✝⁴ : AddCommMonoid B<VAR>inst✝³ : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s✝ : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i : ι<VAR>g✝ : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝² : Zero M<VAR>inst✝¹ : Zero M'<VAR>inst✝ : CommMonoid N<VAR>f : α →₀ M<VAR>s : Finset α<VAR>hs : f.support ⊆ s<VAR>g : α → M → N<VAR>h : ∀ i ∈ s, g i 0 = 1<GOAL>f.prod g = ∏ x ∈ s, g x (f x)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁵ : AddCommMonoid A<VAR>inst✝⁴ : AddCommMonoid B<VAR>inst✝³ : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s✝ : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i : ι<VAR>g✝ : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x✝ : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝² : Zero M<VAR>inst✝¹ : Zero M'<VAR>inst✝ : CommMonoid N<VAR>f : α →₀ M<VAR>s : Finset α<VAR>hs : f.support ⊆ s<VAR>g : α → M → N<VAR>h : ∀ i ∈ s, g i 0 = 1<VAR>x : α<VAR>hxs : x ∈ s<VAR>hx : x ∉ f.support<GOAL>f x = 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : ConcreteCategory C<VAR>X : TopCat<VAR>F : Presheaf (Type u) X<VAR>ι : Type x<VAR>U : ι → Opens ↑X<GOAL>F.IsSheaf ↔ F.IsSheafUniqueGluing
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : ConcreteCategory C<VAR>X : TopCat<VAR>F : Presheaf (Type u) X<VAR>ι : Type x<VAR>U : ι → Opens ↑X<GOAL>(∀ ⦃ι : Type x⦄ (U : ι → Opens ↑X), ∀ s ∈ ((Pairwise.diagram U).op ⋙ F).sections, ∃! x, ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ), (Functor.mapCone F (Pairwise.cocone U).op).π.app j x = s j) ↔ ∀ ⦃ι : Type x⦄ (U : ι → Opens ↑X) (sf : (i : ι) → (forget (Type u)).obj (F.obj (op (U i)))), F.IsCompatible U sf → ∃! s, ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ), (Functor.mapCone F (Pairwise.cocone U).op).π.app i s = objPairwiseOfFamily sf i
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : ConcreteCategory C<VAR>X : TopCat<VAR>F : Presheaf (Type u) X<VAR>ι✝ : Type x<VAR>U✝ : ι✝ → Opens ↑X<VAR>ι : Type x<VAR>U : ι → Opens ↑X<VAR>h : ∀ s ∈ ((Pairwise.diagram U).op ⋙ F).sections, ∃! x, ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ), (Functor.mapCone F (Pairwise.cocone U).op).π.app j x = s j<VAR>sf : (i : ι) → (forget (Type u)).obj (F.obj (op (U i)))<VAR>cpt : F.IsCompatible U sf<GOAL>∃! s, ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ), (Functor.mapCone F (Pairwise.cocone U).op).π.app i s = objPairwiseOfFamily sf i
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : ConcreteCategory C<VAR>X : TopCat<VAR>F : Presheaf (Type u) X<VAR>ι✝ : Type x<VAR>U✝ : ι✝ → Opens ↑X<VAR>ι : Type x<VAR>U : ι → Opens ↑X<VAR>h : ∀ (sf : (i : ι) → (forget (Type u)).obj (F.obj (op (U i)))), F.IsCompatible U sf → ∃! s, ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ), (Functor.mapCone F (Pairwise.cocone U).op).π.app i s = objPairwiseOfFamily sf i<VAR>s : (j : (CategoryTheory.Pairwise ι)ᵒᵖ) → ((Pairwise.diagram U).op ⋙ F).obj j<VAR>hs : s ∈ ((Pairwise.diagram U).op ⋙ F).sections<GOAL>∃! x, ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ), (Functor.mapCone F (Pairwise.cocone U).op).π.app j x = s j
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Computation α<VAR>a : α<VAR>n : ℕ<VAR>h : s.think.Results a n<GOAL>∃ m, s.Results a m ∧ n = m + 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Computation α<VAR>a : α<VAR>n : ℕ<VAR>h : s.think.Results a n<VAR>this : s.Terminates<GOAL>∃ m, s.Results a m ∧ n = m + 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Computation α<VAR>a : α<VAR>n : ℕ<VAR>h : s.think.Results a n<VAR>this✝ : s.Terminates<VAR>this : s.Results a s.length<GOAL>∃ m, s.Results a m ∧ n = m + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>inst✝ : IsFiniteMeasure μ<GOAL>measureUnivNNReal μ = 0 ↔ μ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>inst✝ : IsFiniteMeasure μ<GOAL>measureUnivNNReal μ = 0 ↔ ↑(measureUnivNNReal μ) = 0
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝³ : Monoid M<VAR>a : M<VAR>N : Type u_4<VAR>F : Type u_5<VAR>inst✝² : Monoid N<VAR>inst✝¹ : FunLike F M N<VAR>inst✝ : MonoidHomClass F M N<VAR>f : F<VAR>m : M<GOAL>map f (powers m) = powers (f m)
<VAR>a b n : ℕ<GOAL>n.floorRoot a ≠ 0 ↔ n ≠ 0 ∧ a ≠ 0
<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>m : M<VAR>X Y : C<VAR>f : X ⟶ (F.obj m).obj Y<GOAL>(F.obj (𝟙_ M)).map f ≫ (F.μ m (𝟙_ M)).app Y = F.εIso.inv.app X ≫ f ≫ (F.map (ρ_ m).inv).app Y
<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>m : M<VAR>X Y : C<VAR>f : X ⟶ (F.obj m).obj Y<GOAL>(inv (F.εIso.inv.app X) ≫ (F.obj (𝟙_ M)).map f ≫ (F.μ m (𝟙_ M)).app Y) ≫ inv ((F.map (ρ_ m).inv).app Y) = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝³ : μ.InnerRegularCompactLTTop<VAR>inst✝² : IsLocallyFiniteMeasure μ<VAR>inst✝¹ : R1Space α<VAR>inst✝ : BorelSpace α<VAR>K : Set α<VAR>hK : IsCompact K<VAR>r : ℝ≥0∞<VAR>hr : μ K < r<GOAL>∃ U, K ⊆ U ∧ IsOpen U ∧ μ U < r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝³ : μ.InnerRegularCompactLTTop<VAR>inst✝² : IsLocallyFiniteMeasure μ<VAR>inst✝¹ : R1Space α<VAR>inst✝ : BorelSpace α<VAR>K : Set α<VAR>hK : IsCompact K<VAR>r : ℝ≥0∞<VAR>hr : μ K < r<VAR>V : Set α<VAR>hKV : V ⊇ K<VAR>hVo : IsOpen V<VAR>hμV : μ V < ⊤<GOAL>∃ U, K ⊆ U ∧ IsOpen U ∧ μ U < r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝³ : μ.InnerRegularCompactLTTop<VAR>inst✝² : IsLocallyFiniteMeasure μ<VAR>inst✝¹ : R1Space α<VAR>inst✝ : BorelSpace α<VAR>K : Set α<VAR>hK : IsCompact K<VAR>r : ℝ≥0∞<VAR>hr : μ K < r<VAR>V : Set α<VAR>hKV : V ⊇ K<VAR>hVo : IsOpen V<VAR>hμV : μ V < ⊤<VAR>this : Fact (μ V < ⊤)<GOAL>∃ U, K ⊆ U ∧ IsOpen U ∧ μ U < r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝³ : μ.InnerRegularCompactLTTop<VAR>inst✝² : IsLocallyFiniteMeasure μ<VAR>inst✝¹ : R1Space α<VAR>inst✝ : BorelSpace α<VAR>K : Set α<VAR>hK : IsCompact K<VAR>r : ℝ≥0∞<VAR>hr : μ K < r<VAR>V : Set α<VAR>hKV : V ⊇ K<VAR>hVo : IsOpen V<VAR>hμV : μ V < ⊤<VAR>this : Fact (μ V < ⊤)<VAR>U : Set α<VAR>hKU : K ⊆ U<VAR>hUo : IsOpen U<VAR>hμU : (μ.restrict V) U < r<GOAL>∃ U, K ⊆ U ∧ IsOpen U ∧ μ U < r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝³ : μ.InnerRegularCompactLTTop<VAR>inst✝² : IsLocallyFiniteMeasure μ<VAR>inst✝¹ : R1Space α<VAR>inst✝ : BorelSpace α<VAR>K : Set α<VAR>hK : IsCompact K<VAR>r : ℝ≥0∞<VAR>hr : μ K < r<VAR>V : Set α<VAR>hKV : V ⊇ K<VAR>hVo : IsOpen V<VAR>hμV : μ V < ⊤<VAR>this : Fact (μ V < ⊤)<VAR>U : Set α<VAR>hKU : K ⊆ U<VAR>hUo : IsOpen U<VAR>hμU : (μ.restrict V) U < r<GOAL>μ (U ∩ V) < r
<VAR>x y✝ z : ℝ<VAR>n : ℕ<VAR>hx : 0 ≤ x<VAR>y : ℝ<GOAL>x⁻¹ ^ y = (x ^ y)⁻¹
<VAR>n : ℕ<VAR>α : Type u_1<VAR>a : α<VAR>v : Vector α n.succ<VAR>v' : Vector α n<GOAL>v ≠ a ::ᵥ v' ↔ v.head ≠ a ∨ v.tail ≠ v'
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LT α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c✝ d c : α<GOAL>a / c < b / c ↔ a < b
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>HasStrictDerivAt (fun x => √x) (1 / (2 * √x)) x ∧ ∀ (n : ℕ∞), ContDiffAt ℝ n (fun x => √x) x
<VAR>x : ℝ<VAR>hx✝ : x ≠ 0<VAR>hx : x < 0<GOAL>HasStrictDerivAt (fun x => √x) (1 / (2 * √x)) x ∧ ∀ (n : ℕ∞), ContDiffAt ℝ n (fun x => √x) x
<VAR>x : ℝ<VAR>hx✝ : x ≠ 0<VAR>hx : 0 < x<GOAL>HasStrictDerivAt (fun x => √x) (1 / (2 * √x)) x ∧ ∀ (n : ℕ∞), ContDiffAt ℝ n (fun x => √x) x
<VAR>α : Type u<VAR>β : Type u_1<VAR>l : List α<VAR>f : α → β<GOAL>(ofFn fun i => f l[↑i]) = map f l
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f f₁ f₂ : (i : ι) → Filter (α i)<VAR>s : (i : ι) → Set (α i)<VAR>p : (i : ι) → α i → Prop<VAR>inst✝ : ∀ (i : ι), Nonempty (α i)<GOAL>(Filter.coprodᵢ f).NeBot ↔ ∃ d, (f d).NeBot
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>hτ : IsStoppingTime f τ<VAR>h_countable : (Set.range τ).Countable<VAR>i : ι<GOAL>MeasurableSet {ω | i ≤ τ ω}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>hτ : IsStoppingTime f τ<VAR>h_countable : (Set.range τ).Countable<VAR>i : ι<VAR>this : {ω | i ≤ τ ω} = {ω | τ ω = i} ∪ {ω | i < τ ω}<GOAL>MeasurableSet {ω | i ≤ τ ω}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>hτ : IsStoppingTime f τ<VAR>h_countable : (Set.range τ).Countable<VAR>i : ι<VAR>this : {ω | i ≤ τ ω} = {ω | τ ω = i} ∪ {ω | i < τ ω}<GOAL>MeasurableSet ({ω | τ ω = i} ∪ {ω | i < τ ω})
<VAR>F : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>inst✝² : CompleteSpace F<VAR>inst✝¹ : MeasurableSpace F<VAR>inst✝ : BorelSpace F<GOAL>Measurable fun x => derivWithin f (Ioi x) x
<VAR>M : Type u<VAR>inst✝ : Monoid M<VAR>X x✝¹ x✝ : Discrete M<VAR>f : x✝¹ ⟶ x✝<GOAL>{ as := X.as * x✝¹.as } = { as := X.as * x✝.as }
<VAR>M : Type u<VAR>inst✝ : Monoid M<VAR>X₁✝ X₂✝ : Discrete M<VAR>f : X₁✝ ⟶ X₂✝<VAR>X : Discrete M<GOAL>{ as := X₁✝.as * X.as } = { as := X₂✝.as * X.as }
<VAR>M : Type u<VAR>inst✝ : Monoid M<VAR>X₁✝ Y₁✝ X₂✝ Y₂✝ : Discrete M<VAR>f : X₁✝ ⟶ Y₁✝<VAR>g : X₂✝ ⟶ Y₂✝<GOAL>{ as := X₁✝.as * X₂✝.as } = { as := Y₁✝.as * Y₂✝.as }
<VAR>Γ : Type u_1<VAR>inst✝ : Inhabited Γ<VAR>head✝ : Γ<VAR>left✝ right✝ : ListBlank Γ<GOAL>mk' { head := head✝, left := left✝, right := right✝ }.left { head := head✝, left := left✝, right := right✝ }.right₀ = { head := head✝, left := left✝, right := right✝ }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>a b : α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>f : α → β<GOAL>((StrictMono fun a => map f ↑a) ∧ ∀ (x : α), map f ⊥ < map f ↑x) ↔ StrictMono f
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : M →ₗ[R] M<VAR>p q : R[X]<VAR>hpq : IsCoprime p q<GOAL>LinearMap.range ((aeval f) p) ⊔ LinearMap.range ((aeval f) q) = ⊤
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : M →ₗ[R] M<VAR>p q : R[X]<VAR>hpq : IsCoprime p q<GOAL>⊤ ≤ LinearMap.range ((aeval f) p) ⊔ LinearMap.range ((aeval f) q)
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : M →ₗ[R] M<VAR>p q : R[X]<VAR>hpq : IsCoprime p q<VAR>v : M<VAR>a✝ : v ∈ ⊤<GOAL>v ∈ LinearMap.range ((aeval f) p) ⊔ LinearMap.range ((aeval f) q)
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : M →ₗ[R] M<VAR>p q : R[X]<VAR>hpq : IsCoprime p q<VAR>v : M<VAR>a✝ : v ∈ ⊤<GOAL>∃ y ∈ LinearMap.range ((aeval f) p), ∃ z ∈ LinearMap.range ((aeval f) q), y + z = v
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : M →ₗ[R] M<VAR>p q : R[X]<VAR>v : M<VAR>a✝ : v ∈ ⊤<VAR>p' q' : R[X]<VAR>hpq' : p' * p + q' * q = 1<GOAL>∃ y ∈ LinearMap.range ((aeval f) p), ∃ z ∈ LinearMap.range ((aeval f) q), y + z = v
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : M →ₗ[R] M<VAR>p q : R[X]<VAR>v : M<VAR>a✝ : v ∈ ⊤<VAR>p' q' : R[X]<VAR>hpq' : p' * p + q' * q = 1<GOAL>((aeval f) (p * p')) v ∈ LinearMap.range ((aeval f) p) ∧ ∃ z ∈ LinearMap.range ((aeval f) q), ((aeval f) (p * p')) v + z = v
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : M →ₗ[R] M<VAR>p q : R[X]<VAR>v : M<VAR>a✝ : v ∈ ⊤<VAR>p' q' : R[X]<VAR>hpq' : p' * p + q' * q = 1<GOAL>∃ z ∈ LinearMap.range ((aeval f) q), ((aeval f) (p * p')) v + z = v
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : M →ₗ[R] M<VAR>p q : R[X]<VAR>v : M<VAR>a✝ : v ∈ ⊤<VAR>p' q' : R[X]<VAR>hpq' : p' * p + q' * q = 1<GOAL>((aeval f) (q * q')) v ∈ LinearMap.range ((aeval f) q) ∧ ((aeval f) (p * p')) v + ((aeval f) (q * q')) v = v
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : M →ₗ[R] M<VAR>p q : R[X]<VAR>v : M<VAR>a✝ : v ∈ ⊤<VAR>p' q' : R[X]<VAR>hpq' : p' * p + q' * q = 1<GOAL>((aeval f) (p * p')) v + ((aeval f) (q * q')) v = v
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : MonoidalPreadditive C<VAR>P Q R S : C<VAR>J : Type u_2<VAR>s : Finset J<VAR>f : P ⟶ Q<VAR>g : J → (R ⟶ S)<GOAL>f ⊗ ∑ j ∈ s, g j = ∑ j ∈ s, f ⊗ g j
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : Set P<VAR>p : P<VAR>h : p ∈ affineSpan k s<GOAL>Collinear k (insert p s) ↔ Collinear k s
<VAR>C : Type u_1<VAR>inst✝⁸ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_6, u_2} D<VAR>E : Type u_3<VAR>inst✝⁶ : Category.{u_7, u_3} E<VAR>M : Type u_4<VAR>inst✝⁵ : AddMonoid M<VAR>inst✝⁴ : HasShift C M<VAR>inst✝³ : HasShift D M<VAR>inst✝² : HasShift E M<VAR>X Y Z T : C<VAR>a : M<VAR>f : ShiftedHom X Y a<VAR>F : C ⥤ D<VAR>inst✝¹ : F.CommShift M<VAR>G : D ⥤ E<VAR>inst✝ : G.CommShift M<GOAL>f.map (F ⋙ G) = (f.map F).map G
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>r : ℝ<VAR>hr : 0 < r<VAR>x : E<GOAL>x +ᵥ r • ball 0 1 = ball x r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : ι → α<VAR>s t : Set α<VAR>f : ι → α<GOAL>range f = ∅ ↔ IsEmpty ι
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝¹ : Semiring R<VAR>q r : R[X]<VAR>inst✝ : Semiring S<VAR>n : ℕ<VAR>f : ℕ → R → S[X]<VAR>toFinsupp✝ : R[ℕ]<GOAL>({ toFinsupp := toFinsupp✝ }.sum f).coeff n = { toFinsupp := toFinsupp✝ }.sum fun a b => (f a b).coeff n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a✝ b✝ c d : α<VAR>a b : WithTop α<GOAL>a - b = ⊤ ↔ a = ⊤ ∨ b = ⊤
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<GOAL>sInf {C | 0 ≤ C ∧ ∀ (x : α), dist (f x) (g x) ≤ C} = ↑(sInf {C | ∀ (x : α), nndist (f x) (g x) ≤ C})
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<GOAL>sInf {C | 0 ≤ C ∧ ∀ (x : α), dist (f x) (g x) ≤ C} = sInf {x | ∃ (h : 0 ≤ x), ⟨x, h⟩ ∈ {C | ∀ (x : α), nndist (f x) (g x) ≤ C}}
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : Ring S<VAR>M : Type u_4<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>m : Submodule R M<VAR>N : Type u_5<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsSimpleModule R N<VAR>f : M →ₗ[R] N<GOAL>Function.Surjective ⇑f ∨ f = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : Ring S<VAR>M : Type u_4<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>m : Submodule R M<VAR>N : Type u_5<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsSimpleModule R N<VAR>f : M →ₗ[R] N<GOAL>range f = ⊥ ∨ range f = ⊤
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝¹ : TopologicalSpace X'<VAR>inst✝ : TopologicalSpace Y'<VAR>h : X ≃ₜ Y<VAR>s : Set X<GOAL>⇑h '' interior s = interior (⇑h '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s : ι → Set β<GOAL>⋃ i, s i = range fun a => ↑a.snd
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a✝ a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>a : E<GOAL>0 ≤ ‖a‖
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a✝ a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>a : E<GOAL>0 ≤ dist a 1
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.426465, u_1} C<VAR>n m : ℕ<VAR>F G : ComposableArrows C n<VAR>f g : ComposableArrows C 5<VAR>app₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯<VAR>app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯<VAR>app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯<VAR>app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯<VAR>app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯<VAR>app₅ : f.obj' 5 ⋯ ⟶ g.obj' 5 ⋯<VAR>w₀ : f.map' 0 1 ⋯ ⋯ ≫ app₁ = app₀ ≫ g.map' 0 1 ⋯ ⋯<VAR>w₁ : f.map' 1 2 ⋯ ⋯ ≫ app₂ = app₁ ≫ g.map' 1 2 ⋯ ⋯<VAR>w₂ : f.map' 2 3 ⋯ ⋯ ≫ app₃ = app₂ ≫ g.map' 2 3 ⋯ ⋯<VAR>w₃ : f.map' 3 4 ⋯ ⋯ ≫ app₄ = app₃ ≫ g.map' 3 4 ⋯ ⋯<VAR>w₄ : f.map' 4 5 ⋯ ⋯ ≫ app₅ = app₄ ≫ g.map' 4 5 ⋯ ⋯<GOAL>4 < 5 + 1