ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z : C<VAR>f : Y ⟶ X<VAR>inst✝ : HasPullbacks C<VAR>g : Z ⟶ X<GOAL>pullbackArrows f (singleton g) = singleton (pullback.snd g f)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z : C<VAR>f : Y ⟶ X<VAR>inst✝ : HasPullbacks C<VAR>g : Z ⟶ X<VAR>W : C<GOAL>pullbackArrows f (singleton g) = singleton (pullback.snd g f)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>f : J → C<VAR>X : C<VAR>j : J<GOAL>(rightDistributor f X).inv ≫ biproduct.π f j ▷ X = biproduct.π (fun j => f j ⊗ X) j
<VAR>J : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝² : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>F✝ : J ⥤ C<VAR>inst✝ : HasLimitsOfShape J C<VAR>F : J ⥤ C<GOAL>{ obj := fun F => limit F, map := fun {X Y} α => limMap α }.map (𝟙 F) = 𝟙 ({ obj := fun F => limit F, map := fun {X Y} α => limMap α }.obj F)
<VAR>J : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝² : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>F✝ : J ⥤ C<VAR>inst✝ : HasLimitsOfShape J C<VAR>F : J ⥤ C<GOAL>∀ (j : J), { obj := fun F => limit F, map := fun {X Y} α => limMap α }.map (𝟙 F) ≫ limit.π F j = 𝟙 ({ obj := fun F => limit F, map := fun {X Y} α => limMap α }.obj F) ≫ limit.π F j
<VAR>J : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝² : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>F✝ : J ⥤ C<VAR>inst✝ : HasLimitsOfShape J C<VAR>F : J ⥤ C<VAR>j : J<GOAL>{ obj := fun F => limit F, map := fun {X Y} α => limMap α }.map (𝟙 F) ≫ limit.π F j = 𝟙 ({ obj := fun F => limit F, map := fun {X Y} α => limMap α }.obj F) ≫ limit.π F j
<VAR>J : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝² : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>F : J ⥤ C<VAR>inst✝ : HasLimitsOfShape J C<VAR>X✝ Y✝ Z✝ : J ⥤ C<VAR>α : X✝ ⟶ Y✝<VAR>β : Y✝ ⟶ Z✝<GOAL>{ obj := fun F => limit F, map := fun {X Y} α => limMap α }.map (α ≫ β) = { obj := fun F => limit F, map := fun {X Y} α => limMap α }.map α ≫ { obj := fun F => limit F, map := fun {X Y} α => limMap α }.map β
<VAR>J : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝² : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>F : J ⥤ C<VAR>inst✝ : HasLimitsOfShape J C<VAR>X✝ Y✝ Z✝ : J ⥤ C<VAR>α : X✝ ⟶ Y✝<VAR>β : Y✝ ⟶ Z✝<GOAL>∀ (j : J), { obj := fun F => limit F, map := fun {X Y} α => limMap α }.map (α ≫ β) ≫ limit.π Z✝ j = ({ obj := fun F => limit F, map := fun {X Y} α => limMap α }.map α ≫ { obj := fun F => limit F, map := fun {X Y} α => limMap α }.map β) ≫ limit.π Z✝ j
<VAR>J : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝² : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>F : J ⥤ C<VAR>inst✝ : HasLimitsOfShape J C<VAR>X✝ Y✝ Z✝ : J ⥤ C<VAR>α : X✝ ⟶ Y✝<VAR>β : Y✝ ⟶ Z✝<VAR>j : J<GOAL>{ obj := fun F => limit F, map := fun {X Y} α => limMap α }.map (α ≫ β) ≫ limit.π Z✝ j = ({ obj := fun F => limit F, map := fun {X Y} α => limMap α }.map α ≫ { obj := fun F => limit F, map := fun {X Y} α => limMap α }.map β) ≫ limit.π Z✝ j
<VAR>J : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝² : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>F : J ⥤ C<VAR>inst✝ : HasLimitsOfShape J C<VAR>X✝ Y✝ Z✝ : J ⥤ C<VAR>α : X✝ ⟶ Y✝<VAR>β : Y✝ ⟶ Z✝<VAR>j : J<GOAL>((Cones.postcompose (α ≫ β)).obj (limit.cone X✝)).π.app j = (limit.cone X✝).π.app j ≫ α.app j ≫ β.app j
<VAR>f : ℕ → ℂ<VAR>c s : ℂ<VAR>hc : c ≠ 0<VAR>hf : LSeriesSummable (c • f) s<GOAL>LSeriesSummable f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>p : β → Prop<VAR>inst✝ : DecidablePred p<VAR>f : α ≃ Subtype p<VAR>g g₁ g₂ : Perm α<VAR>s t : Set α<VAR>h : MapsTo (⇑g) s t<VAR>a : α<VAR>ha : a ∈ s<GOAL>(g.extendDomain f) ((Subtype.val ∘ ⇑f) a) ∈ Subtype.val ∘ ⇑f '' t
<VAR>m k : ℕ<GOAL>m.psub 0 = some k ↔ k + 0 = m
<VAR>m n k : ℕ<GOAL>m.psub (n + 1) = some k ↔ k + (n + 1) = m
<VAR>m n k : ℕ<GOAL>(∃ a, m.psub n = some a ∧ a.ppred = some k) ↔ k + (n + 1) = m
<VAR>m n k : ℕ<GOAL>(∃ a, a + n = m ∧ k.succ = a) ↔ k + (n + 1) = m
<VAR>cmp✝ : ?m.4485 → ?m.4485 → Ordering<VAR>inst✝¹ : TransCmp cmp✝<VAR>x✝ : Sort ?u.4483<VAR>cmp : x✝ → x✝ → Ordering<VAR>inst✝ : TransCmp cmp<VAR>x y z : x✝<VAR>h₁ : cmp x y = Ordering.gt<VAR>h₂ : cmp y z = Ordering.gt<GOAL>cmp x z = Ordering.gt
<VAR>cmp✝ : ?m.4485 → ?m.4485 → Ordering<VAR>inst✝¹ : TransCmp cmp✝<VAR>x✝ : Sort ?u.4483<VAR>cmp : x✝ → x✝ → Ordering<VAR>inst✝ : TransCmp cmp<VAR>x y z : x✝<VAR>h₁ : cmp y x = Ordering.lt<VAR>h₂ : cmp z y = Ordering.lt<GOAL>cmp z x = Ordering.lt
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : SuccOrder α<VAR>inst✝ : IsSuccArchimedean α<VAR>a✝ b✝ : α<VAR>p : α → Prop<VAR>hsucc : ∀ (a : α), p a ↔ p (succ a)<VAR>a b : α<VAR>h : a ≤ b<GOAL>p a ↔ p b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : SuccOrder α<VAR>inst✝ : IsSuccArchimedean α<VAR>a✝ b : α<VAR>p : α → Prop<VAR>hsucc : ∀ (a : α), p a ↔ p (succ a)<VAR>a : α<VAR>n : ℕ<VAR>h : a ≤ succ^[n] a<GOAL>p a ↔ p (succ^[n] a)
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>s : Set α<GOAL>TotallyBounded s ↔ ∀ (f : Ultrafilter α), ↑f ≤ 𝓟 s → Cauchy ↑f
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>s : Set α<VAR>H : ∀ (f : Ultrafilter α), ↑f ≤ 𝓟 s → Cauchy ↑f<GOAL>∀ (f : Filter α), f.NeBot → f ≤ 𝓟 s → ∃ c ≤ f, Cauchy c
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>s : Set α<VAR>H : ∀ (f : Ultrafilter α), ↑f ≤ 𝓟 s → Cauchy ↑f<VAR>f : Filter α<VAR>hf : f.NeBot<VAR>hfs : f ≤ 𝓟 s<GOAL>∃ c ≤ f, Cauchy c
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>p : ℝ<VAR>hp1 : 1 ≤ p<VAR>B : ℕ → ℝ≥0∞<VAR>h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N<VAR>n : ℕ<VAR>f_norm_diff : ℕ → α → ℝ := fun i x => ‖f (i + 1) x - f i x‖<GOAL>eLpNorm' (fun x => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>p : ℝ<VAR>hp1 : 1 ≤ p<VAR>B : ℕ → ℝ≥0∞<VAR>h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N<VAR>n : ℕ<VAR>f_norm_diff : ℕ → α → ℝ := fun i x => ‖f (i + 1) x - f i x‖<VAR>hgf_norm_diff : ∀ (n : ℕ), (fun x => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) = ∑ i ∈ Finset.range (n + 1), f_norm_diff i<GOAL>eLpNorm' (fun x => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>p : ℝ<VAR>hp1 : 1 ≤ p<VAR>B : ℕ → ℝ≥0∞<VAR>h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N<VAR>n : ℕ<VAR>f_norm_diff : ℕ → α → ℝ := fun i x => ‖f (i + 1) x - f i x‖<VAR>hgf_norm_diff : ∀ (n : ℕ), (fun x => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) = ∑ i ∈ Finset.range (n + 1), f_norm_diff i<GOAL>eLpNorm' (∑ i ∈ Finset.range (n + 1), f_norm_diff i) p μ ≤ ∑' (i : ℕ), B i
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>p : ℝ<VAR>hp1 : 1 ≤ p<VAR>B : ℕ → ℝ≥0∞<VAR>h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N<VAR>n : ℕ<VAR>f_norm_diff : ℕ → α → ℝ := fun i x => ‖f (i + 1) x - f i x‖<VAR>hgf_norm_diff : ∀ (n : ℕ), (fun x => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) = ∑ i ∈ Finset.range (n + 1), f_norm_diff i<GOAL>∑ i ∈ Finset.range (n + 1), eLpNorm' (fun x => ‖(f (i + 1) - f i) x‖) p μ ≤ ∑' (i : ℕ), B i
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>p : ℝ<VAR>hp1 : 1 ≤ p<VAR>B : ℕ → ℝ≥0∞<VAR>h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N<VAR>n : ℕ<VAR>f_norm_diff : ℕ → α → ℝ := fun i x => ‖f (i + 1) x - f i x‖<VAR>hgf_norm_diff : ∀ (n : ℕ), (fun x => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) = ∑ i ∈ Finset.range (n + 1), f_norm_diff i<GOAL>∑ x ∈ Finset.range (n + 1), eLpNorm' (f (x + 1) - f x) p μ ≤ ∑' (i : ℕ), B i
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>p : ℝ<VAR>hp1 : 1 ≤ p<VAR>B : ℕ → ℝ≥0∞<VAR>h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N<VAR>n : ℕ<VAR>f_norm_diff : ℕ → α → ℝ := fun i x => ‖f (i + 1) x - f i x‖<VAR>hgf_norm_diff : ∀ (n : ℕ), (fun x => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) = ∑ i ∈ Finset.range (n + 1), f_norm_diff i<GOAL>∀ i ∈ Finset.range (n + 1), eLpNorm' (f (i + 1) - f i) p μ ≤ B i
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : CompleteSpace F<VAR>c : ℂ<VAR>R C : ℝ<VAR>f : ℂ → F<VAR>hR : 0 < R<VAR>hf : DiffContOnCl ℂ f (ball c R)<VAR>hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C<GOAL>‖deriv f c‖ ≤ C / R
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : CompleteSpace F<VAR>c : ℂ<VAR>R C : ℝ<VAR>f : ℂ → F<VAR>hR : 0 < R<VAR>hf : DiffContOnCl ℂ f (ball c R)<VAR>hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C<VAR>this : ∀ z ∈ sphere c R, ‖(z - c) ^ (-2) • f z‖ ≤ C / (R * R)<GOAL>‖deriv f c‖ ≤ C / R
<VAR>J : Type u<VAR>inst✝¹ : SmallCategory J<VAR>F : J ⥤ TopCat<VAR>inst✝ : ∀ (j : J), T2Space ↑(F.obj j)<VAR>G : Finset J<VAR>H : Finset (TopCat.FiniteDiagramArrow G)<GOAL>IsClosed (partialSections F H)
<VAR>J : Type u<VAR>inst✝¹ : SmallCategory J<VAR>F : J ⥤ TopCat<VAR>inst✝ : ∀ (j : J), T2Space ↑(F.obj j)<VAR>G : Finset J<VAR>H : Finset (TopCat.FiniteDiagramArrow G)<VAR>this : partialSections F H = ⋂ f ∈ H, {u | (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}<GOAL>IsClosed (partialSections F H)
<VAR>J : Type u<VAR>inst✝¹ : SmallCategory J<VAR>F : J ⥤ TopCat<VAR>inst✝ : ∀ (j : J), T2Space ↑(F.obj j)<VAR>G : Finset J<VAR>H : Finset (TopCat.FiniteDiagramArrow G)<VAR>this : partialSections F H = ⋂ f ∈ H, {u | (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}<GOAL>IsClosed (⋂ f ∈ H, {u | (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst})
<VAR>J : Type u<VAR>inst✝¹ : SmallCategory J<VAR>F : J ⥤ TopCat<VAR>inst✝ : ∀ (j : J), T2Space ↑(F.obj j)<VAR>G : Finset J<VAR>H : Finset (TopCat.FiniteDiagramArrow G)<VAR>this : partialSections F H = ⋂ f ∈ H, {u | (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}<GOAL>∀ i ∈ fun i => i ∈ H.val, IsClosed {u | (F.map i.snd.snd.snd.snd) (u i.fst) = u i.snd.fst}
<VAR>J : Type u<VAR>inst✝¹ : SmallCategory J<VAR>F : J ⥤ TopCat<VAR>inst✝ : ∀ (j : J), T2Space ↑(F.obj j)<VAR>G : Finset J<VAR>H : Finset (TopCat.FiniteDiagramArrow G)<VAR>this✝ : partialSections F H = ⋂ f ∈ H, {u | (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}<VAR>f : TopCat.FiniteDiagramArrow G<VAR>a✝ : f ∈ fun i => i ∈ H.val<VAR>this : T2Space ((forget TopCat).obj (F.obj f.snd.fst))<GOAL>IsClosed {u | (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}
<VAR>J : Type u<VAR>inst✝¹ : SmallCategory J<VAR>F : J ⥤ TopCat<VAR>inst✝ : ∀ (j : J), T2Space ↑(F.obj j)<VAR>G : Finset J<VAR>H : Finset (TopCat.FiniteDiagramArrow G)<VAR>this✝ : partialSections F H = ⋂ f ∈ H, {u | (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}<VAR>f : TopCat.FiniteDiagramArrow G<VAR>a✝ : f ∈ fun i => i ∈ H.val<VAR>this : T2Space ((forget TopCat).obj (F.obj f.snd.fst))<GOAL>Continuous fun y => (F.map f.snd.snd.snd.snd) (y f.fst)
<VAR>J : Type u<VAR>inst✝¹ : SmallCategory J<VAR>F : J ⥤ TopCat<VAR>inst✝ : ∀ (j : J), T2Space ↑(F.obj j)<VAR>G : Finset J<VAR>H : Finset (TopCat.FiniteDiagramArrow G)<VAR>this✝ : partialSections F H = ⋂ f ∈ H, {u | (F.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}<VAR>f : TopCat.FiniteDiagramArrow G<VAR>a✝ : f ∈ fun i => i ∈ H.val<VAR>this : T2Space ((forget TopCat).obj (F.obj f.snd.fst))<GOAL>Continuous fun y => y f.snd.fst
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : TopologicalSpace β✝<VAR>inst✝⁵ : PseudoMetrizableSpace β✝<VAR>inst✝⁴ : MeasurableSpace β✝<VAR>inst✝³ : BorelSpace β✝<VAR>β : Type u_3<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : BorelSpace β<VAR>μ : Measure α<VAR>g : α → β<VAR>hf : ∀ ε > 0, ∃ f, AEMeasurable f μ ∧ ∀ᵐ (x : α) ∂μ, dist (f x) (g x) ≤ ε<GOAL>AEMeasurable g μ
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : TopologicalSpace β✝<VAR>inst✝⁵ : PseudoMetrizableSpace β✝<VAR>inst✝⁴ : MeasurableSpace β✝<VAR>inst✝³ : BorelSpace β✝<VAR>β : Type u_3<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : BorelSpace β<VAR>μ : Measure α<VAR>g : α → β<VAR>hf : ∀ ε > 0, ∃ f, AEMeasurable f μ ∧ ∀ᵐ (x : α) ∂μ, dist (f x) (g x) ≤ ε<VAR>u : ℕ → ℝ<VAR>u_pos : ∀ (n : ℕ), 0 < u n<VAR>u_lim : Tendsto u atTop (𝓝 0)<GOAL>AEMeasurable g μ
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : TopologicalSpace β✝<VAR>inst✝⁵ : PseudoMetrizableSpace β✝<VAR>inst✝⁴ : MeasurableSpace β✝<VAR>inst✝³ : BorelSpace β✝<VAR>β : Type u_3<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : BorelSpace β<VAR>μ : Measure α<VAR>g : α → β<VAR>hf : ∀ ε > 0, ∃ f, AEMeasurable f μ ∧ ∀ᵐ (x : α) ∂μ, dist (f x) (g x) ≤ ε<VAR>u : ℕ → ℝ<VAR>u_pos : ∀ (n : ℕ), 0 < u n<VAR>u_lim : Tendsto u atTop (𝓝 0)<VAR>f : ℕ → α → β<VAR>Hf : ∀ (n : ℕ), AEMeasurable (f n) μ ∧ ∀ᵐ (x : α) ∂μ, dist (f n x) (g x) ≤ u n<GOAL>AEMeasurable g μ
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : TopologicalSpace β✝<VAR>inst✝⁵ : PseudoMetrizableSpace β✝<VAR>inst✝⁴ : MeasurableSpace β✝<VAR>inst✝³ : BorelSpace β✝<VAR>β : Type u_3<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : BorelSpace β<VAR>μ : Measure α<VAR>g : α → β<VAR>hf : ∀ ε > 0, ∃ f, AEMeasurable f μ ∧ ∀ᵐ (x : α) ∂μ, dist (f x) (g x) ≤ ε<VAR>u : ℕ → ℝ<VAR>u_pos : ∀ (n : ℕ), 0 < u n<VAR>u_lim : Tendsto u atTop (𝓝 0)<VAR>f : ℕ → α → β<VAR>Hf : ∀ (n : ℕ), AEMeasurable (f n) μ ∧ ∀ᵐ (x : α) ∂μ, dist (f n x) (g x) ≤ u n<VAR>this : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<GOAL>AEMeasurable g μ
<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>inst✝ : Nontrivial R<VAR>s t u : Set M<VAR>hl : LinearIndependent (ι := { x // x ∈ u }) R Subtype.val<VAR>hsu : s ⊆ u<VAR>htu : t ⊆ u<VAR>hst : span R s ≤ span R t<GOAL>s ⊆ t
<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>inst✝ : Nontrivial R<VAR>s t u : Set M<VAR>hl : LinearIndependent (ι := { x // x ∈ u }) R Subtype.val<VAR>hsu : s ⊆ u<VAR>htu : t ⊆ u<VAR>hst : span R s ≤ span R t<VAR>this : s ∪ t = t<GOAL>s ⊆ t
<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>inst✝ : Nontrivial R<VAR>s t u : Set M<VAR>hl : LinearIndependent (ι := { x // x ∈ u }) R Subtype.val<VAR>hsu : s ⊆ u<VAR>htu : t ⊆ u<VAR>hst : span R s ≤ span R t<VAR>this : s ∪ t = t<GOAL>s ⊆ s ∪ t
<VAR>α✝ : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>α : Type u_1<VAR>s : Set α<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>x : α<VAR>hx : x ∈ s<GOAL>(Set.sumCompl s).symm ↑⟨x, hx⟩ = Sum.inl ⟨x, hx⟩
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝⁹ : Ring R<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>inst✝¹ : Module R' M'<VAR>inst✝ : Module R' M₁<VAR>i : R' → R<VAR>j : M →+ M'<VAR>hi : ∀ (r : R'), i r = 0 → r = 0<VAR>hj : Injective ⇑j<VAR>hc : ∀ (r : R') (m : M), j (i r • m) = r • j m<GOAL>lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R' M')
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝⁹ : Ring R<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>inst✝¹ : Module R' M'<VAR>inst✝ : Module R' M₁<VAR>i : R' → R<VAR>j : M →+ M'<VAR>hi : ∀ (r : R'), i r = 0 → r = 0<VAR>hj : Injective ⇑j<VAR>hc : ∀ (r : R') (m : M), j (i r • m) = r • j m<GOAL>⨆ i, lift.{v', v} #↑↑i ≤ ⨆ i, lift.{v, v'} #↑↑i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : SemilatticeSup β<VAR>inst✝ : ContinuousSup β<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>H : s.Nonempty<VAR>f : ι → C(α, β)<VAR>x✝ : α<GOAL>(s.sup' H f) x✝ = s.sup' H (fun i => ⇑(f i)) x✝
<VAR>q : ℚ<VAR>x y : ℝ<VAR>h : Irrational (x - ↑q)<GOAL>Irrational (x + ↑(-q))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<VAR>w✝¹ : Ordinal.{u}<VAR>w✝ : w✝¹ < o<VAR>hf : f w✝¹ w✝ = o.bsup f<GOAL>succ (o.bsup f) ≤ o.blsub f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<VAR>w✝¹ : Ordinal.{u}<VAR>w✝ : w✝¹ < o<VAR>hf : f w✝¹ w✝ = o.bsup f<GOAL>f w✝¹ w✝ < o.blsub f
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁵ : SeminormedAddCommGroup V<VAR>inst✝⁴ : PseudoMetricSpace P<VAR>inst✝³ : NormedAddTorsor V P<VAR>inst✝² : NormedAddCommGroup W<VAR>inst✝¹ : MetricSpace Q<VAR>inst✝ : NormedAddTorsor W Q<VAR>v : V<VAR>x : P<GOAL>dist x (v +ᵥ x) = ‖v‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Multiset α<GOAL>s.dedup = t.dedup ↔ ∀ (a : α), a ∈ s ↔ a ∈ t
<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 : C ⥤ D<VAR>A : Type u<VAR>inst✝² : Category.{t, u} A<VAR>J✝ : GrothendieckTopology C<VAR>K✝ : GrothendieckTopology D<VAR>F₁ : C ⥤ D<VAR>F₂ : D ⥤ E<VAR>F₁₂ : C ⥤ E<VAR>e : F₁ ⋙ F₂ ≅ F₁₂<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>inst✝¹ : F₁.IsContinuous J K<VAR>inst✝ : F₂.IsContinuous K L<GOAL>F₁₂.IsContinuous J L
<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 : C ⥤ D<VAR>A : Type u<VAR>inst✝² : Category.{t, u} A<VAR>J✝ : GrothendieckTopology C<VAR>K✝ : GrothendieckTopology D<VAR>F₁ : C ⥤ D<VAR>F₂ : D ⥤ E<VAR>F₁₂ : C ⥤ E<VAR>e : F₁ ⋙ F₂ ≅ F₁₂<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>inst✝¹ : F₁.IsContinuous J K<VAR>inst✝ : F₂.IsContinuous K L<VAR>this : (F₁ ⋙ F₂).IsContinuous J L<GOAL>F₁₂.IsContinuous J L
<VAR>α : Type u<VAR>β : Type v<VAR>R r : α → α → Prop<VAR>l l₁ l₂ : List α<VAR>a b x y : α<GOAL>Chain' R [x, y] ↔ R x y
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>f : v.FunSpace<VAR>inst✝ : CompleteSpace E<VAR>t : ↑(Icc v.tMin v.tMax)<GOAL>HasDerivWithinAt (f.next.toFun ∘ v.proj) (v.toFun (↑t) (f.toFun t)) (Icc v.tMin v.tMax) ↑t
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>f : v.FunSpace<VAR>inst✝ : CompleteSpace E<VAR>t : ↑(Icc v.tMin v.tMax)<VAR>this : Fact (↑t ∈ Icc v.tMin v.tMax)<GOAL>HasDerivWithinAt (f.next.toFun ∘ v.proj) (v.toFun (↑t) (f.toFun t)) (Icc v.tMin v.tMax) ↑t
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>f : v.FunSpace<VAR>inst✝ : CompleteSpace E<VAR>t : ↑(Icc v.tMin v.tMax)<VAR>this : Fact (↑t ∈ Icc v.tMin v.tMax)<GOAL>HasDerivWithinAt (fun x => v.x₀ + ∫ (τ : ℝ) in ↑v.t₀..↑(v.proj x), f.vComp τ) (v.toFun (↑t) (f.toFun t)) (Icc v.tMin v.tMax) ↑t
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>f : v.FunSpace<VAR>inst✝ : CompleteSpace E<VAR>t : ↑(Icc v.tMin v.tMax)<VAR>this : Fact (↑t ∈ Icc v.tMin v.tMax)<GOAL>HasDerivWithinAt (fun x => ∫ (τ : ℝ) in ↑v.t₀..↑(v.proj x), f.vComp τ) (v.toFun (↑t) (f.toFun t)) (Icc v.tMin v.tMax) ↑t
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>f : v.FunSpace<VAR>inst✝ : CompleteSpace E<VAR>t : ↑(Icc v.tMin v.tMax)<VAR>this✝ : Fact (↑t ∈ Icc v.tMin v.tMax)<VAR>this : HasDerivWithinAt (fun x => ∫ (τ : ℝ) in ↑v.t₀..x, f.vComp τ) (f.vComp ↑t) (Icc v.tMin v.tMax) ↑t<GOAL>HasDerivWithinAt (fun x => ∫ (τ : ℝ) in ↑v.t₀..↑(v.proj x), f.vComp τ) (v.toFun (↑t) (f.toFun t)) (Icc v.tMin v.tMax) ↑t
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>f : v.FunSpace<VAR>inst✝ : CompleteSpace E<VAR>t : ↑(Icc v.tMin v.tMax)<VAR>this✝ : Fact (↑t ∈ Icc v.tMin v.tMax)<VAR>this : HasDerivWithinAt (fun x => ∫ (τ : ℝ) in ↑v.t₀..x, f.vComp τ) (v.toFun (↑t) (f.toFun t)) (Icc v.tMin v.tMax) ↑t<GOAL>HasDerivWithinAt (fun x => ∫ (τ : ℝ) in ↑v.t₀..↑(v.proj x), f.vComp τ) (v.toFun (↑t) (f.toFun t)) (Icc v.tMin v.tMax) ↑t
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>f : v.FunSpace<VAR>inst✝ : CompleteSpace E<VAR>t : ↑(Icc v.tMin v.tMax)<VAR>this✝ : Fact (↑t ∈ Icc v.tMin v.tMax)<VAR>this : HasDerivWithinAt (fun x => ∫ (τ : ℝ) in ↑v.t₀..x, f.vComp τ) (v.toFun (↑t) (f.toFun t)) (Icc v.tMin v.tMax) ↑t<GOAL>(fun x => ∫ (τ : ℝ) in ↑v.t₀..↑(v.proj x), f.vComp τ) =ᶠ[𝓝[Icc v.tMin v.tMax] ↑t] fun x => ∫ (τ : ℝ) in ↑v.t₀..x, f.vComp τ