ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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.23191, u_1} K<VAR>D : Type u_2<VAR>inst✝ : Category.{?u.23198, u_2} D<VAR>F : J ⥤ C<VAR>c c' : Cocone F<VAR>hc : IsUniversalColimit c<VAR>e : c ≅ c'<VAR>F' : J ⥤ C<VAR>c'' : Cocone F'<VAR>α : F' ⟶ F<VAR>f : c''.pt ⟶ c'.pt<VAR>h : α ≫ c'.ι = c''.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>H : ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)<VAR>this : c'.ι ≫ (Functor.const J).map e.inv.hom = c.ι<GOAL>∀ (j : J), IsPullback (c''.ι.app j) (α.app j) (f ≫ e.inv.hom) (c.ι.app j)
<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.23191, u_1} K<VAR>D : Type u_2<VAR>inst✝ : Category.{?u.23198, u_2} D<VAR>F : J ⥤ C<VAR>c c' : Cocone F<VAR>hc : IsUniversalColimit c<VAR>e : c ≅ c'<VAR>F' : J ⥤ C<VAR>c'' : Cocone F'<VAR>α : F' ⟶ F<VAR>f : c''.pt ⟶ c'.pt<VAR>h : α ≫ c'.ι = c''.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>H : ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)<VAR>this : c'.ι ≫ (Functor.const J).map e.inv.hom = c.ι<VAR>j : J<GOAL>IsPullback (c''.ι.app j) (α.app j) (f ≫ e.inv.hom) (c.ι.app j)
<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.23191, u_1} K<VAR>D : Type u_2<VAR>inst✝ : Category.{?u.23198, u_2} D<VAR>F : J ⥤ C<VAR>c c' : Cocone F<VAR>hc : IsUniversalColimit c<VAR>e : c ≅ c'<VAR>F' : J ⥤ C<VAR>c'' : Cocone F'<VAR>α : F' ⟶ F<VAR>f : c''.pt ⟶ c'.pt<VAR>h : α ≫ c'.ι = c''.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>H : ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)<VAR>this : c'.ι ≫ (Functor.const J).map e.inv.hom = c.ι<VAR>j : J<GOAL>IsPullback (c''.ι.app j) (α.app j ≫ 𝟙 (F.obj j)) (f ≫ e.inv.hom) (c.ι.app j)
<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.23191, u_1} K<VAR>D : Type u_2<VAR>inst✝ : Category.{?u.23198, u_2} D<VAR>F : J ⥤ C<VAR>c c' : Cocone F<VAR>hc : IsUniversalColimit c<VAR>e : c ≅ c'<VAR>F' : J ⥤ C<VAR>c'' : Cocone F'<VAR>α : F' ⟶ F<VAR>f : c''.pt ⟶ c'.pt<VAR>h : α ≫ c'.ι = c''.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>H : ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)<VAR>this✝ : c'.ι ≫ (Functor.const J).map e.inv.hom = c.ι<VAR>j : J<VAR>this : IsIso e.inv.hom<GOAL>IsPullback (c''.ι.app j) (α.app j ≫ 𝟙 (F.obj j)) (f ≫ e.inv.hom) (c.ι.app j)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s✝ s₁ s₂ t t₁ t₂ u s : Set α<VAR>h : a ∈ t<VAR>x✝ : α<GOAL>x✝ ∈ insert a s \ t ↔ x✝ ∈ s \ t
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μα : Measure α<VAR>μ : Measure Ω<VAR>inst✝⁴ : IsMarkovKernel κ<VAR>inst✝³ : IsProbabilityMeasure μ<VAR>inst✝² : SemilatticeSup ι<VAR>inst✝¹ : NoMaxOrder ι<VAR>inst✝ : Nonempty ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : iIndep s κ μα<VAR>ns : ι → Set ι := Set.Iic<GOAL>Indep (limsup s atTop) (limsup s atTop) κ μα
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μα : Measure α<VAR>μ : Measure Ω<VAR>inst✝⁴ : IsMarkovKernel κ<VAR>inst✝³ : IsProbabilityMeasure μ<VAR>inst✝² : SemilatticeSup ι<VAR>inst✝¹ : NoMaxOrder ι<VAR>inst✝ : Nonempty ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : iIndep s κ μα<VAR>ns : ι → Set ι := Set.Iic<VAR>hnsp : ∀ (i : ι), BddAbove (ns i)<GOAL>Indep (limsup s atTop) (limsup s atTop) κ μα
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μα : Measure α<VAR>μ : Measure Ω<VAR>inst✝⁴ : IsMarkovKernel κ<VAR>inst✝³ : IsProbabilityMeasure μ<VAR>inst✝² : SemilatticeSup ι<VAR>inst✝¹ : NoMaxOrder ι<VAR>inst✝ : Nonempty ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : iIndep s κ μα<VAR>ns : ι → Set ι := Set.Iic<VAR>hnsp : ∀ (i : ι), BddAbove (ns i)<GOAL>∀ (t : Set ι), BddAbove t → tᶜ ∈ atTop
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μα : Measure α<VAR>μ : Measure Ω<VAR>inst✝⁴ : IsMarkovKernel κ<VAR>inst✝³ : IsProbabilityMeasure μ<VAR>inst✝² : SemilatticeSup ι<VAR>inst✝¹ : NoMaxOrder ι<VAR>inst✝ : Nonempty ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : iIndep s κ μα<VAR>ns : ι → Set ι := Set.Iic<VAR>hnsp : ∀ (i : ι), BddAbove (ns i)<GOAL>Directed (fun x x_1 => x ≤ x_1) ns
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μα : Measure α<VAR>μ : Measure Ω<VAR>inst✝⁴ : IsMarkovKernel κ<VAR>inst✝³ : IsProbabilityMeasure μ<VAR>inst✝² : SemilatticeSup ι<VAR>inst✝¹ : NoMaxOrder ι<VAR>inst✝ : Nonempty ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : iIndep s κ μα<VAR>ns : ι → Set ι := Set.Iic<VAR>hnsp : ∀ (i : ι), BddAbove (ns i)<GOAL>∀ (n : ι), ∃ a, n ∈ ns a
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable σ<VAR>C : Set (ℕ →. ℕ)<VAR>f g : ℕ →. ℕ<VAR>hf : Nat.Partrec f<VAR>hg : Nat.Partrec g<VAR>fC : f ∈ C<VAR>w✝ : DecidablePred fun c => c.eval ∈ C<VAR>h : Computable fun a => decide ((fun c => c.eval ∈ C) a)<GOAL>g ∈ C
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable σ<VAR>C : Set (ℕ →. ℕ)<VAR>f g : ℕ →. ℕ<VAR>hf : Nat.Partrec f<VAR>hg : Nat.Partrec g<VAR>fC : f ∈ C<VAR>w✝ : DecidablePred fun c => c.eval ∈ C<VAR>h : Computable fun a => decide ((fun c => c.eval ∈ C) a)<VAR>c : Code<VAR>e : c.eval = fun b => bif decide ((fun c => c.eval ∈ C) (c, b).1) then (fun a b => g (a, b).2) (c, b).1 (c, b).2 else (fun a b => f (a, b).2) (c, b).1 (c, b).2<GOAL>g ∈ C
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable σ<VAR>C : Set (ℕ →. ℕ)<VAR>f g : ℕ →. ℕ<VAR>hf : Nat.Partrec f<VAR>hg : Nat.Partrec g<VAR>fC : f ∈ C<VAR>w✝ : DecidablePred fun c => c.eval ∈ C<VAR>h : Computable fun a => decide ((fun c => c.eval ∈ C) a)<VAR>c : Code<VAR>e : c.eval = fun b => if c.eval ∈ C then g b else f b<GOAL>g ∈ C
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s : Set E<VAR>x : E<VAR>t : Set E<VAR>hs : Convex 𝕜 s<VAR>ht : Convex 𝕜 t<GOAL>Convex 𝕜 (s + t)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s : Set E<VAR>x : E<VAR>t : Set E<VAR>hs : Convex 𝕜 s<VAR>ht : Convex 𝕜 t<GOAL>Convex 𝕜 ((fun x => x.1 + x.2) '' s ×ˢ t)
<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<GOAL>IsSimpleModule R ↥m ↔ IsAtom m
<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<GOAL>IsSimpleModule R ↥m ↔ IsSimpleOrder ↑(Set.Iic m)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x : FreeCommRing α<VAR>s : Set α<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>hxs : x.IsSupported s<GOAL>(map Subtype.val) ((restriction s) x) = x
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x : FreeCommRing α<VAR>s : Set α<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>hxs : x.IsSupported s<GOAL>(map Subtype.val) ((restriction s) 1) = 1
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x : FreeCommRing α<VAR>s : Set α<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>hxs : x.IsSupported s<GOAL>(map Subtype.val) ((restriction s) (-1)) = -1
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x : FreeCommRing α<VAR>s : Set α<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>hxs : x.IsSupported s<GOAL>∀ z ∈ of '' s, ∀ (n : FreeCommRing α), (map Subtype.val) ((restriction s) n) = n → (map Subtype.val) ((restriction s) (z * n)) = z * n
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x : FreeCommRing α<VAR>s : Set α<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>hxs : x.IsSupported s<GOAL>∀ {x y : FreeCommRing α}, (map Subtype.val) ((restriction s) x) = x → (map Subtype.val) ((restriction s) y) = y → (map Subtype.val) ((restriction s) (x + y)) = x + y
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n₁ n₂ d₁ d₂ : ℤ<VAR>hn₁ : n₁ ≠ 0<VAR>hn₂ : n₂ ≠ 0<VAR>hd₁ : d₁ ≠ 0<VAR>hd₂ : d₂ ≠ 0<GOAL>padicValRat p (n₁ /. d₁) ≤ padicValRat p (n₂ /. d₂) ↔ ∀ (n : ℕ), ↑p ^ n ∣ n₁ * d₂ → ↑p ^ n ∣ n₂ * d₁
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n₁ n₂ d₁ d₂ : ℤ<VAR>hn₁ : n₁ ≠ 0<VAR>hn₂ : n₂ ≠ 0<VAR>hd₁ : d₁ ≠ 0<VAR>hd₂ : d₂ ≠ 0<VAR>hf1 : multiplicity.Finite (↑p) (n₁ * d₂)<GOAL>padicValRat p (n₁ /. d₁) ≤ padicValRat p (n₂ /. d₂) ↔ ∀ (n : ℕ), ↑p ^ n ∣ n₁ * d₂ → ↑p ^ n ∣ n₂ * d₁
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n₁ n₂ d₁ d₂ : ℤ<VAR>hn₁ : n₁ ≠ 0<VAR>hn₂ : n₂ ≠ 0<VAR>hd₁ : d₁ ≠ 0<VAR>hd₂ : d₂ ≠ 0<VAR>hf1 : multiplicity.Finite (↑p) (n₁ * d₂)<VAR>hf2 : multiplicity.Finite (↑p) (n₂ * d₁)<GOAL>padicValRat p (n₁ /. d₁) ≤ padicValRat p (n₂ /. d₂) ↔ ∀ (n : ℕ), ↑p ^ n ∣ n₁ * d₂ → ↑p ^ n ∣ n₂ * d₁
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>D : ℝ<VAR>x : E<VAR>Dpos : 0 < D<VAR>hx : x ∈ closedBall 0 (1 - D)<GOAL>(w D ⋆[lsmul ℝ ℝ, μ] φ) x = 1
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>D : ℝ<VAR>x : E<VAR>Dpos : 0 < D<VAR>hx : x ∈ closedBall 0 (1 - D)<VAR>B : ∀ y ∈ ball x D, φ y = 1<GOAL>(w D ⋆[lsmul ℝ ℝ, μ] φ) x = 1
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>D : ℝ<VAR>x : E<VAR>Dpos : 0 < D<VAR>hx : x ∈ closedBall 0 (1 - D)<VAR>B : ∀ y ∈ ball x D, φ y = 1<VAR>Bx : φ x = 1<GOAL>(w D ⋆[lsmul ℝ ℝ, μ] φ) x = 1
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>D : ℝ<VAR>x : E<VAR>Dpos : 0 < D<VAR>hx : x ∈ closedBall 0 (1 - D)<VAR>B : ∀ y ∈ ball x D, φ y = 1<VAR>Bx : φ x = 1<VAR>B' : ∀ y ∈ ball x D, φ y = φ x<GOAL>(w D ⋆[lsmul ℝ ℝ, μ] φ) x = 1
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>D : ℝ<VAR>x : E<VAR>Dpos : 0 < D<VAR>hx : x ∈ closedBall 0 (1 - D)<VAR>B : ∀ y ∈ ball x D, φ y = 1<VAR>Bx : φ x = 1<VAR>B' : ∀ y ∈ ball x D, φ y = φ x<GOAL>∫ (t : E), ((lsmul ℝ ℝ) (w D t)) (φ x) ∂μ = 1
<VAR>a b : ℝ<VAR>nb ne : ℕ<VAR>pb : IsInt b (Int.negOfNat nb)<VAR>pe' : IsInt (a ^ Int.negOfNat nb) (Int.negOfNat ne)<GOAL>IsInt (a ^ b) (Int.negOfNat ne)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.35536, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>h : S.LeftHomologyData<GOAL>IsZero (CokernelCofork.ofπ h.π ⋯).pt
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.35536, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>h : S.LeftHomologyData<VAR>this : S.HasHomology<GOAL>IsZero (CokernelCofork.ofπ h.π ⋯).pt
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.35536, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>h : S.LeftHomologyData<VAR>this : S.HasHomology<GOAL>IsZero h.H
<VAR>K : Type u_1<VAR>inst✝¹ : DivisionRing K<VAR>inst✝ : CharZero K<VAR>a b : ℕ<GOAL>↑(a.choose b) = Polynomial.eval (↑(a - (b - 1))) (ascPochhammer K b) / ↑b !
<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>T : Type u_4<VAR>inst✝¹ : CommRing T<VAR>inst✝ : IsDedekindDomain T<VAR>I J : Ideal T<VAR>hJ : Irreducible J<VAR>n : ℕ<VAR>hn : ↑n ≤ multiplicity J I<VAR>hI : ¬I = ⊥<GOAL>J ^ n ⊔ I = J ^ n
<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>T : Type u_4<VAR>inst✝¹ : CommRing T<VAR>inst✝ : IsDedekindDomain T<VAR>I J : Ideal T<VAR>hJ : Irreducible J<VAR>n : ℕ<VAR>hn : ↑n ≤ multiplicity J I<VAR>hI : ¬I = ⊥<GOAL>n ≤ count J (normalizedFactors I)
<VAR>α : Type u_1<VAR>l₂ : List (Lists α)<VAR>head✝ : Lists α<VAR>tail✝ : List (Lists α)<VAR>l₁_ih : tail✝ ⊆ l₂ → ofList tail✝ ⊆ ofList l₂<VAR>h : head✝ :: tail✝ ⊆ l₂<GOAL>ofList (head✝ :: tail✝) ⊆ ofList l₂
<VAR>α : Type u_1<VAR>l₂ : List (Lists α)<VAR>head✝ : Lists α<VAR>tail✝ : List (Lists α)<VAR>l₁_ih : tail✝ ⊆ l₂ → ofList tail✝ ⊆ ofList l₂<VAR>h : head✝ :: tail✝ ⊆ l₂<GOAL>head✝ ∈ (ofList l₂).toList
<VAR>α : Type u_1<VAR>l₂ : List (Lists α)<VAR>head✝ : Lists α<VAR>tail✝ : List (Lists α)<VAR>l₁_ih : tail✝ ⊆ l₂ → ofList tail✝ ⊆ ofList l₂<VAR>h : head✝ ∈ l₂ ∧ tail✝ ⊆ l₂<GOAL>head✝ ∈ (ofList l₂).toList
<VAR>R : Type u_1<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>a b c : R<VAR>hab : a ≤ b<VAR>hc : 0 ≤ c<GOAL>c * a ≤ c * b
<VAR>R : Type u_1<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>a b c : R<VAR>hab : a ≤ b<VAR>hc : c ∈ AddSubmonoid.closure (Set.range fun s => star s * s)<GOAL>c * a ≤ c * b
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n m : ℕ<VAR>inst✝ : DivisionRing K<VAR>n_lt_m : n < m<VAR>terminatedAt_n : g.TerminatedAt n<GOAL>g.contsAux m = g.contsAux (n + 1)
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n m : ℕ<VAR>inst✝ : DivisionRing K<VAR>n_lt_m : n < m<VAR>terminatedAt_n : g.TerminatedAt n<VAR>k : ℕ<VAR>hnk : n.succ ≤ k<VAR>hk : g.contsAux k = g.contsAux (n + 1)<GOAL>g.contsAux (k + 1) = g.contsAux (n + 1)
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n m : ℕ<VAR>inst✝ : DivisionRing K<VAR>n_lt_m : n < m<VAR>terminatedAt_n : g.TerminatedAt n<VAR>k : ℕ<VAR>hnk : n.succ ≤ n + k + 1<VAR>hk : g.contsAux (n + k + 1) = g.contsAux (n + 1)<GOAL>g.contsAux (n + k + 1 + 1) = g.contsAux (n + 1)
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n m : ℕ<VAR>inst✝ : DivisionRing K<VAR>n_lt_m : n < m<VAR>terminatedAt_n : g.TerminatedAt n<VAR>k : ℕ<VAR>hnk : n.succ ≤ n + k + 1<VAR>hk : g.contsAux (n + k + 1) = g.contsAux (n + 1)<GOAL>g.TerminatedAt (n + k)
<VAR>z τ : ℂ<VAR>hτ : τ.im ≤ 0<GOAL>jacobiTheta₂' z τ = 0
<VAR>z τ : ℂ<VAR>hτ : τ.im ≤ 0<GOAL>¬Summable fun b => jacobiTheta₂'_term b z τ
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z✝ W X Y Z S T : TopCat<VAR>f₁ : W ⟶ S<VAR>f₂ : X ⟶ S<VAR>g₁ : Y ⟶ T<VAR>g₂ : Z ⟶ T<VAR>i₁ : W ⟶ Y<VAR>i₂ : X ⟶ Z<VAR>H₁ : Embedding ⇑i₁<VAR>H₂ : Embedding ⇑i₂<VAR>i₃ : S ⟶ T<VAR>eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁<VAR>eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂<GOAL>Embedding ⇑(pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z✝ W X Y Z S T : TopCat<VAR>f₁ : W ⟶ S<VAR>f₂ : X ⟶ S<VAR>g₁ : Y ⟶ T<VAR>g₂ : Z ⟶ T<VAR>i₁ : W ⟶ Y<VAR>i₂ : X ⟶ Z<VAR>H₁ : Embedding ⇑i₁<VAR>H₂ : Embedding ⇑i₂<VAR>i₃ : S ⟶ T<VAR>eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁<VAR>eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂<GOAL>Embedding (⇑(prod.lift (pullback.fst g₁ g₂) (pullback.snd g₁ g₂)) ∘ ⇑(pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂))
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z✝ W X Y Z S T : TopCat<VAR>f₁ : W ⟶ S<VAR>f₂ : X ⟶ S<VAR>g₁ : Y ⟶ T<VAR>g₂ : Z ⟶ T<VAR>i₁ : W ⟶ Y<VAR>i₂ : X ⟶ Z<VAR>H₁ : Embedding ⇑i₁<VAR>H₂ : Embedding ⇑i₂<VAR>i₃ : S ⟶ T<VAR>eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁<VAR>eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂<GOAL>Embedding ⇑(prod.lift (pullback.fst f₁ f₂) (pullback.snd f₁ f₂) ≫ prod.map i₁ i₂)
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z✝ W X Y Z S T : TopCat<VAR>f₁ : W ⟶ S<VAR>f₂ : X ⟶ S<VAR>g₁ : Y ⟶ T<VAR>g₂ : Z ⟶ T<VAR>i₁ : W ⟶ Y<VAR>i₂ : X ⟶ Z<VAR>H₁ : Embedding ⇑i₁<VAR>H₂ : Embedding ⇑i₂<VAR>i₃ : S ⟶ T<VAR>eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁<VAR>eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂<GOAL>Embedding (⇑(prod.map i₁ i₂) ∘ ⇑(prod.lift (pullback.fst f₁ f₂) (pullback.snd f₁ f₂)))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.4719, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>S✝ S₁ S₂ : ShortComplex C<VAR>S : ShortComplex Cᵒᵖ<VAR>h : S.ShortExact<GOAL>Mono S.unop.f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.4719, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>S✝ S₁ S₂ : ShortComplex C<VAR>S : ShortComplex Cᵒᵖ<VAR>h : S.ShortExact<VAR>this : Epi S.g<GOAL>Mono S.unop.f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.4719, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>S✝ S₁ S₂ : ShortComplex C<VAR>S : ShortComplex Cᵒᵖ<VAR>h : S.ShortExact<GOAL>Epi S.unop.g
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.4719, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>S✝ S₁ S₂ : ShortComplex C<VAR>S : ShortComplex Cᵒᵖ<VAR>h : S.ShortExact<VAR>this : Mono S.f<GOAL>Epi S.unop.g
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : α → β<GOAL>UniformInducing f ↔ UniformContinuous f ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : α → β<GOAL>𝓤 α ≤ comap (fun x => (f x.1, f x.2)) (𝓤 β) ∧ comap (fun x => (f x.1, f x.2)) (𝓤 β) ≤ 𝓤 α ↔ 𝓤 α ≤ comap (fun x => (f x.1, f x.2)) (𝓤 β) ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : Semigroup M<VAR>a b : M<VAR>ha : a ∈ S.centralizer<VAR>hb : b ∈ S.centralizer<VAR>g : M<VAR>hg : g ∈ S<GOAL>g * (a * b) = a * b * g
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a✝ : α<VAR>n : ℕ<VAR>a : α<VAR>ha : 0 ≤ a<VAR>x✝ : ℕ<GOAL>x✝ ∈ Nat.cast ⁻¹' Iic a ↔ x✝ ∈ Iic ⌊a⌋₊
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : TopologicalSpace V<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : Module R V<VAR>inst✝¹ : SeparatingDual R V<VAR>inst✝ : T1Space R<GOAL>T1Space V
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : TopologicalSpace V<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : Module R V<VAR>inst✝¹ : SeparatingDual R V<VAR>inst✝ : T1Space R<VAR>x y : V<VAR>hxy : x ≠ y<GOAL>∃ U, IsOpen U ∧ x ∈ U ∧ y ∉ U
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : TopologicalSpace V<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : Module R V<VAR>inst✝¹ : SeparatingDual R V<VAR>inst✝ : T1Space R<VAR>x y : V<VAR>hxy : x ≠ y<VAR>f : V →L[R] R<VAR>hf : f x ≠ f y<GOAL>∃ U, IsOpen U ∧ x ∈ U ∧ y ∉ U
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>f : α → E<VAR>hf : Integrable f μ<GOAL>∀ᵐ (x : α) ∂μ, Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>f : α → E<VAR>hf : Integrable f μ<VAR>I : Integrable (AEStronglyMeasurable.mk f ⋯) μ<GOAL>∀ᵐ (x : α) ∂μ, Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>f : α → E<VAR>hf : Integrable f μ<VAR>I : Integrable (AEStronglyMeasurable.mk f ⋯) μ<VAR>x : α<VAR>hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖AEStronglyMeasurable.mk f ⋯ y - AEStronglyMeasurable.mk f ⋯ x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)<VAR>h'x : f x = AEStronglyMeasurable.mk f ⋯ x<GOAL>Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>f : α → E<VAR>hf : Integrable f μ<VAR>I : Integrable (AEStronglyMeasurable.mk f ⋯) μ<VAR>x : α<VAR>hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖AEStronglyMeasurable.mk f ⋯ y - AEStronglyMeasurable.mk f ⋯ x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)<VAR>h'x : f x = AEStronglyMeasurable.mk f ⋯ x<GOAL>∀ (x_1 : Set α), (∫⁻ (y : α) in x_1, ↑‖AEStronglyMeasurable.mk f ⋯ y - AEStronglyMeasurable.mk f ⋯ x‖₊ ∂μ) / μ x_1 = (∫⁻ (y : α) in x_1, ↑‖f y - f x‖₊ ∂μ) / μ x_1
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>f : α → E<VAR>hf : Integrable f μ<VAR>I : Integrable (AEStronglyMeasurable.mk f ⋯) μ<VAR>x : α<VAR>hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖AEStronglyMeasurable.mk f ⋯ y - AEStronglyMeasurable.mk f ⋯ x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)<VAR>h'x : f x = AEStronglyMeasurable.mk f ⋯ x<VAR>a : Set α<GOAL>∫⁻ (y : α) in a, ↑‖AEStronglyMeasurable.mk f ⋯ y - AEStronglyMeasurable.mk f ⋯ x‖₊ ∂μ = ∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>f : α → E<VAR>hf : Integrable f μ<VAR>I : Integrable (AEStronglyMeasurable.mk f ⋯) μ<VAR>x : α<VAR>hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖AEStronglyMeasurable.mk f ⋯ y - AEStronglyMeasurable.mk f ⋯ x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)<VAR>h'x : f x = AEStronglyMeasurable.mk f ⋯ x<VAR>a : Set α<GOAL>(fun a => ↑‖AEStronglyMeasurable.mk f ⋯ a - AEStronglyMeasurable.mk f ⋯ x‖₊) =ᶠ[ae (μ.restrict a)] fun a => ↑‖f a - f x‖₊
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>f : α → E<VAR>hf : Integrable f μ<VAR>I : Integrable (AEStronglyMeasurable.mk f ⋯) μ<VAR>x : α<VAR>hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖AEStronglyMeasurable.mk f ⋯ y - AEStronglyMeasurable.mk f ⋯ x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)<VAR>h'x : f x = AEStronglyMeasurable.mk f ⋯ x<VAR>a : Set α<GOAL>∀ᵐ (x_1 : α) ∂μ, (fun a => ↑‖AEStronglyMeasurable.mk f ⋯ a - AEStronglyMeasurable.mk f ⋯ x‖₊) x_1 = (fun a => ↑‖f a - f x‖₊) x_1