ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝² : MetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>inst✝¹ : Nonempty α<VAR>inst✝ : CompleteSpace α<VAR>x : α<VAR>n : ℕ<GOAL>dist (f^[n] x) (fixedPoint f hf) ≤ dist (f^[n] x) (f^[n + 1] x) / (1 - ↑K)
<VAR>α : Type u_1<VAR>inst✝² : MetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>inst✝¹ : Nonempty α<VAR>inst✝ : CompleteSpace α<VAR>x : α<VAR>n : ℕ<GOAL>dist (f^[n] x) (fixedPoint f hf) ≤ dist (f^[n] x) ((f ∘ f^[n]) x) / (1 - ↑K)
<VAR>α : Type u<VAR>β : Type v<VAR>R : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Nontrivial R<VAR>hf : ¬IsField R<GOAL>∃ x, ∃ (_ : x ≠ 0), ¬IsUnit x
<VAR>α : Type u<VAR>β : Type v<VAR>R : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Nontrivial R<VAR>hf : ¬IsField R<VAR>this : ¬∀ {a : R}, a ≠ 0 → ∃ b, a * b = 1<GOAL>∃ x, ∃ (_ : x ≠ 0), ¬IsUnit x
<VAR>α : Type u<VAR>β : Type v<VAR>R : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Nontrivial R<VAR>hf : ¬IsField R<VAR>this : ¬∀ {a : R}, a ≠ 0 → ∃ b, a * b = 1<GOAL>∃ x, ∃ (_ : x ≠ 0), ¬∃ b, x * b = 1
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x ≠ 0 ∨ y = 0<GOAL>Real.tan (angle x (x + y)) * ‖x‖ = ‖y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x ≠ 0 ∨ y = 0<GOAL>‖y‖ / ‖x‖ * ‖x‖ = ‖y‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<GOAL>2 * (image Sym2.mk s.offDiag).card = s.offDiag.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<GOAL>∀ (x y : α), s(x, y) ∈ image Sym2.mk s.offDiag → (filter (fun x_1 => Sym2.mk x_1 = s(x, y)) s.offDiag).card = 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>x y : α<VAR>hxy : s(x, y) ∈ image Sym2.mk s.offDiag<GOAL>(filter (fun x_1 => Sym2.mk x_1 = s(x, y)) s.offDiag).card = 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>x y : α<VAR>hxy : ∃ a, (a.1 ∈ s ∧ a.2 ∈ s ∧ a.1 ≠ a.2) ∧ Sym2.mk a = s(x, y)<GOAL>(filter (fun x_1 => Sym2.mk x_1 = s(x, y)) s.offDiag).card = 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>x y : α<VAR>a : α × α<VAR>h : Sym2.mk a = s(x, y)<VAR>ha₁ : a.1 ∈ s<VAR>ha₂ : a.2 ∈ s<VAR>ha : a.1 ≠ a.2<GOAL>(filter (fun x_1 => Sym2.mk x_1 = s(x, y)) s.offDiag).card = 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>x y : α<VAR>a : α × α<VAR>ha₁ : a.1 ∈ s<VAR>ha₂ : a.2 ∈ s<VAR>ha : a.1 ≠ a.2<VAR>h : Rel α a (x, y)<GOAL>(filter (fun x_1 => Sym2.mk x_1 = s(x, y)) s.offDiag).card = 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>x y : α<VAR>a : α × α<VAR>ha₁ : a.1 ∈ s<VAR>ha₂ : a.2 ∈ s<VAR>ha : a.1 ≠ a.2<VAR>h : Rel α a (x, y)<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hxy : x ≠ y<GOAL>(filter (fun x_1 => Sym2.mk x_1 = s(x, y)) s.offDiag).card = 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>x y : α<VAR>a : α × α<VAR>ha₁ : a.1 ∈ s<VAR>ha₂ : a.2 ∈ s<VAR>ha : a.1 ≠ a.2<VAR>h : Rel α a (x, y)<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hxy : x ≠ y<VAR>hxy' : y ≠ x<GOAL>(filter (fun x_1 => Sym2.mk x_1 = s(x, y)) s.offDiag).card = 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>x y : α<VAR>a : α × α<VAR>ha₁ : a.1 ∈ s<VAR>ha₂ : a.2 ∈ s<VAR>ha : a.1 ≠ a.2<VAR>h : Rel α a (x, y)<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hxy : x ≠ y<VAR>hxy' : y ≠ x<VAR>this : filter (fun z => Sym2.mk z = s(x, y)) s.offDiag = {(x, y), (y, x)}<GOAL>(filter (fun x_1 => Sym2.mk x_1 = s(x, y)) s.offDiag).card = 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>x y : α<VAR>a : α × α<VAR>ha₁ : a.1 ∈ s<VAR>ha₂ : a.2 ∈ s<VAR>ha : a.1 ≠ a.2<VAR>h : Rel α a (x, y)<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hxy : x ≠ y<VAR>hxy' : y ≠ x<VAR>this : filter (fun z => Sym2.mk z = s(x, y)) s.offDiag = {(x, y), (y, x)}<GOAL>(x, y) ∉ {(y, x)}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>x y : α<VAR>a : α × α<VAR>ha₁ : a.1 ∈ s<VAR>ha₂ : a.2 ∈ s<VAR>ha : a.1 ≠ a.2<VAR>h : Rel α a (x, y)<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hxy : x ≠ y<VAR>hxy' : y ≠ x<VAR>this : filter (fun z => Sym2.mk z = s(x, y)) s.offDiag = {(x, y), (y, x)}<GOAL>x = y → ¬y = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Mul α<VAR>inst✝² : LinearOrder α<VAR>a b c d : α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>h : a * b < c * d<GOAL>min a b < max c d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Mul α<VAR>inst✝² : LinearOrder α<VAR>a b c d : α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>h : a * b < c * d<GOAL>(a < c ∨ a < d) ∨ b < c ∨ b < d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Mul α<VAR>inst✝² : LinearOrder α<VAR>a b c d : α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>h : (c ≤ a ∧ d ≤ a) ∧ c ≤ b ∧ d ≤ b<GOAL>c * d ≤ a * b
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>t : ℝ<VAR>f : AddCircle T → E<GOAL>∫ (a : ℝ) in Ioc t (t + T), f ↑a = ∫ (b : AddCircle T), f b
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>t : ℝ<VAR>f : AddCircle T → E<VAR>m : MeasurableSet (Ioc t (t + T))<GOAL>∫ (a : ℝ) in Ioc t (t + T), f ↑a = ∫ (b : AddCircle T), f b
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>t : ℝ<VAR>f : AddCircle T → E<VAR>m : MeasurableSet (Ioc t (t + T))<VAR>this : ∫ (y : AddCircle T), f y ∂Measure.map (⇑(measurableEquivIoc T t).symm) volume = ∫ (x : ↑(Ioc t (t + T))), f ((measurableEquivIoc T t).symm x)<GOAL>∫ (a : ℝ) in Ioc t (t + T), f ↑a = ∫ (b : AddCircle T), f b
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>t : ℝ<VAR>f : AddCircle T → E<VAR>m : MeasurableSet (Ioc t (t + T))<VAR>this : ∫ (y : AddCircle T), f y ∂Measure.map (fun x => ↑↑x) volume = ∫ (x : ↑(Ioc t (t + T))), f ↑↑x<GOAL>∫ (a : ℝ) in Ioc t (t + T), f ↑a = ∫ (b : AddCircle T), f b
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>t : ℝ<VAR>f : AddCircle T → E<VAR>m : MeasurableSet (Ioc t (t + T))<VAR>this : ∫ (y : AddCircle T), f y ∂Measure.map (fun x => ↑↑x) volume = ∫ (x : ↑(Ioc t (t + T))), f ↑↑x<GOAL>∫ (y : AddCircle T), f y ∂Measure.map (fun x => ↑↑x) volume = ∫ (b : AddCircle T), f b ∂Measure.map QuotientAddGroup.mk (volume.restrict (Ioc t (t + T)))
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>t : ℝ<VAR>f : AddCircle T → E<VAR>m : MeasurableSet (Ioc t (t + T))<VAR>this✝ : ∫ (y : AddCircle T), f y ∂Measure.map (fun x => ↑↑x) volume = ∫ (x : ↑(Ioc t (t + T))), f ↑↑x<VAR>this : (fun x => ↑↑x) = QuotientAddGroup.mk ∘ Subtype.val<GOAL>∫ (y : AddCircle T), f y ∂Measure.map (QuotientAddGroup.mk ∘ Subtype.val) volume = ∫ (y : AddCircle T), f y ∂Measure.map QuotientAddGroup.mk (volume.restrict (Ioc t (t + T)))
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>t : ℝ<VAR>f : AddCircle T → E<VAR>m : MeasurableSet (Ioc t (t + T))<VAR>this✝ : ∫ (y : AddCircle T), f y ∂Measure.map (fun x => ↑↑x) volume = ∫ (x : ↑(Ioc t (t + T))), f ↑↑x<VAR>this : (fun x => ↑↑x) = QuotientAddGroup.mk ∘ Subtype.val<GOAL>∫ (y : AddCircle T), f y ∂Measure.map QuotientAddGroup.mk (Measure.map Subtype.val volume) = ∫ (y : AddCircle T), f y ∂Measure.map QuotientAddGroup.mk (Measure.map Subtype.val (Measure.comap Subtype.val volume))
<VAR>α✝ : Type u_1<VAR>R : α✝ → α✝ → Prop<VAR>a : α✝<VAR>l : List α✝<VAR>p : Pairwise R (a :: l)<GOAL>Chain R a l
<VAR>α✝ : Type u_1<VAR>R : α✝ → α✝ → Prop<VAR>a : α✝<VAR>l : List α✝<VAR>p : Pairwise R (a :: l)<VAR>r : ∀ (a' : α✝), a' ∈ l → R a a'<VAR>p' : Pairwise R l<GOAL>Chain R a l
<VAR>α✝ : Type u_1<VAR>R : α✝ → α✝ → Prop<VAR>a : α✝<VAR>l : List α✝<VAR>r : ∀ (a' : α✝), a' ∈ l → R a a'<VAR>p' : Pairwise R l<GOAL>Chain R a l
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>M'' : Type u_5<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M''<VAR>I : Ideal R<VAR>N : Submodule R M<VAR>r✝ : R<VAR>M''' : Type u_6<VAR>inst✝¹ : AddCommGroup M'''<VAR>inst✝ : Module R M'''<VAR>r : R<VAR>f₁ : M →ₗ[R] M'<VAR>f₂ : M' →ₗ[R] M''<VAR>f₃ : M'' →ₗ[R] M'''<VAR>h₁₂ : Exact ⇑f₁ ⇑f₂<VAR>h₂₃ : Exact ⇑f₂ ⇑f₃<VAR>h : IsSMulRegular M''' r<VAR>this : IsSMulRegular (M'' ⧸ LinearMap.range f₂) r<GOAL>Exact ⇑((r • ⊤).mapQ (r • ⊤) f₁ ⋯) ⇑((r • ⊤).mapQ (r • ⊤) f₂ ⋯)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>M'' : Type u_5<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M''<VAR>I : Ideal R<VAR>N : Submodule R M<VAR>r✝ : R<VAR>M''' : Type u_6<VAR>inst✝¹ : AddCommGroup M'''<VAR>inst✝ : Module R M'''<VAR>r : R<VAR>f₁ : M →ₗ[R] M'<VAR>f₂ : M' →ₗ[R] M''<VAR>f₃ : M'' →ₗ[R] M'''<VAR>h₁₂ : Exact ⇑f₁ ⇑f₂<VAR>h₂₃ : Exact ⇑f₂ ⇑f₃<VAR>h : IsSMulRegular M''' r<VAR>this : IsSMulRegular (M'' ⧸ LinearMap.range f₂) r<GOAL>r • ⊤ ⊓ LinearMap.range f₂ ≤ r • LinearMap.range f₂
<VAR>T : Type u₁<VAR>inst✝ : Category.{v₁, u₁} T<VAR>X✝ X Y Z : T<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>map (f ≫ g) = map g ⋙ map f
<VAR>T : Type u₁<VAR>inst✝ : Category.{v₁, u₁} T<VAR>X✝ X Y Z : T<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>∀ (X_1 : Under Z), (map (f ≫ g)).obj X_1 = (map g ⋙ map f).obj X_1
<VAR>T : Type u₁<VAR>inst✝ : Category.{v₁, u₁} T<VAR>X✝ X Y Z : T<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>autoParam (∀ (X_1 Y_1 : Under Z) (f_1 : X_1 ⟶ Y_1), (map (f ≫ g)).map f_1 = eqToHom ⋯ ≫ (map g ⋙ map f).map f_1 ≫ eqToHom ⋯) _auto✝
<VAR>a : ℂ<VAR>ha : a.re < -1<VAR>c : ℝ<VAR>hc : 0 < c<GOAL>IntegrableOn (fun t => ↑t ^ a) (Ioi c) volume
<VAR>a : ℂ<VAR>ha : a.re < -1<VAR>c : ℝ<VAR>hc : 0 < c<GOAL>IntegrableOn (fun a_1 => ‖↑a_1 ^ a‖) (Ioi c) volume
<VAR>a : ℂ<VAR>ha : a.re < -1<VAR>c : ℝ<VAR>hc : 0 < c<GOAL>AEStronglyMeasurable (fun t => ↑t ^ a) (volume.restrict (Ioi c))
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → Option β<VAR>g : α → β<VAR>a : α<VAR>l : List α<VAR>ih : filterMap f l = map g l → ∀ (x : α), x ∈ l → f x = some (g x)<GOAL>filterMap f (a :: l) = map g (a :: l) → ∀ (x : α), x ∈ a :: l → f x = some (g x)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → Option β<VAR>g : α → β<VAR>a : α<VAR>l : List α<VAR>ih : filterMap f l = map g l → ∀ (x : α), x ∈ l → f x = some (g x)<VAR>ha : f a = none<GOAL>¬filterMap f l = g a :: map g l
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → Option β<VAR>g : α → β<VAR>a : α<VAR>l : List α<VAR>ih : filterMap f l = map g l → ∀ (x : α), x ∈ l → f x = some (g x)<VAR>b : β<VAR>ha : f a = some b<GOAL>b = g a → filterMap f l = map g l → b = g a ∧ ∀ (a : α), a ∈ l → f a = some (g a)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedLinearOrderedField 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : StrictConvexSpace 𝕜 E<VAR>x : E<VAR>r : ℝ<GOAL>StrictConvex 𝕜 (closedBall x r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedLinearOrderedField 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : StrictConvexSpace 𝕜 E<VAR>x : E<VAR>r : ℝ<VAR>hr : r ≤ 0<GOAL>StrictConvex 𝕜 (closedBall x r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedLinearOrderedField 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : StrictConvexSpace 𝕜 E<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>StrictConvex 𝕜 (closedBall x r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedLinearOrderedField 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : StrictConvexSpace 𝕜 E<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>StrictConvex 𝕜 (x +ᵥ closedBall 0 r)
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Ioi a) volume<VAR>fint : IntegrableOn f (Ioi a) volume<VAR>F : E →L[ℝ] Completion E := Completion.toComplL<GOAL>Tendsto f atTop (𝓝 0)
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Ioi a) volume<VAR>fint : IntegrableOn f (Ioi a) volume<VAR>F : E →L[ℝ] Completion E := Completion.toComplL<VAR>Fderiv : ∀ x ∈ Ioi a, HasDerivAt (⇑F ∘ f) (F (f' x)) x<GOAL>Tendsto f atTop (𝓝 0)
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Ioi a) volume<VAR>fint : IntegrableOn f (Ioi a) volume<VAR>F : E →L[ℝ] Completion E := Completion.toComplL<VAR>Fderiv : ∀ x ∈ Ioi a, HasDerivAt (⇑F ∘ f) (F (f' x)) x<VAR>Fint : IntegrableOn (⇑F ∘ f) (Ioi a) volume<GOAL>Tendsto f atTop (𝓝 0)
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Ioi a) volume<VAR>fint : IntegrableOn f (Ioi a) volume<VAR>F : E →L[ℝ] Completion E := Completion.toComplL<VAR>Fderiv : ∀ x ∈ Ioi a, HasDerivAt (⇑F ∘ f) (F (f' x)) x<VAR>Fint : IntegrableOn (⇑F ∘ f) (Ioi a) volume<VAR>F'int : IntegrableOn (⇑F ∘ f') (Ioi a) volume<GOAL>Tendsto f atTop (𝓝 0)
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Ioi a) volume<VAR>fint : IntegrableOn f (Ioi a) volume<VAR>F : E →L[ℝ] Completion E := Completion.toComplL<VAR>Fderiv : ∀ x ∈ Ioi a, HasDerivAt (⇑F ∘ f) (F (f' x)) x<VAR>Fint : IntegrableOn (⇑F ∘ f) (Ioi a) volume<VAR>F'int : IntegrableOn (⇑F ∘ f') (Ioi a) volume<VAR>A : Tendsto (⇑F ∘ f) atTop (𝓝 (limUnder atTop (⇑F ∘ f)))<GOAL>Tendsto f atTop (𝓝 0)
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Ioi a) volume<VAR>fint : IntegrableOn f (Ioi a) volume<VAR>F : E →L[ℝ] Completion E := Completion.toComplL<VAR>Fderiv : ∀ x ∈ Ioi a, HasDerivAt (⇑F ∘ f) (F (f' x)) x<VAR>Fint : IntegrableOn (⇑F ∘ f) (Ioi a) volume<VAR>F'int : IntegrableOn (⇑F ∘ f') (Ioi a) volume<VAR>A : Tendsto (⇑F ∘ f) atTop (𝓝 (limUnder atTop (⇑F ∘ f)))<VAR>B : limUnder atTop (⇑F ∘ f) = F 0<GOAL>Tendsto f atTop (𝓝 0)
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Ioi a) volume<VAR>fint : IntegrableOn f (Ioi a) volume<VAR>F : E →L[ℝ] Completion E := Completion.toComplL<VAR>Fderiv : ∀ x ∈ Ioi a, HasDerivAt (⇑F ∘ f) (F (f' x)) x<VAR>Fint : IntegrableOn (⇑F ∘ f) (Ioi a) volume<VAR>F'int : IntegrableOn (⇑F ∘ f') (Ioi a) volume<VAR>A : Tendsto (⇑F ∘ f) atTop (𝓝 (F 0))<VAR>B : limUnder atTop (⇑F ∘ f) = F 0<GOAL>Embedding ⇑F
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : C<VAR>α β : X ≅ Y<VAR>w : α.hom = β.hom<GOAL>α.inv = α.inv ≫ β.hom ≫ β.inv
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : C<VAR>α β : X ≅ Y<VAR>w : α.hom = β.hom<GOAL>α.inv ≫ β.hom ≫ β.inv = (α.inv ≫ α.hom) ≫ β.inv
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : C<VAR>α β : X ≅ Y<VAR>w : α.hom = β.hom<GOAL>(α.inv ≫ α.hom) ≫ β.inv = β.inv
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type w<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Semiring S<VAR>ι : Type u_1<VAR>I J : Ideal R<VAR>coprime : IsCoprime I J<GOAL>(fst (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientInfEquivQuotientProd J coprime) = factor (I ⊓ J) I ⋯
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type w<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Semiring S<VAR>ι : Type u_1<VAR>I J : Ideal R<VAR>coprime : IsCoprime I J<GOAL>((fst (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientInfEquivQuotientProd J coprime)).comp (Quotient.mk (I ⊓ J)) = (factor (I ⊓ J) I ⋯).comp (Quotient.mk (I ⊓ J))
<VAR>R : Type u_1<VAR>Rₛ : Type u_2<VAR>inst✝¹⁰ : CommSemiring R<VAR>S : Submonoid R<VAR>inst✝⁹ : CommRing Rₛ<VAR>inst✝⁸ : Algebra R Rₛ<VAR>hT : IsLocalization S Rₛ<VAR>M : Type u_3<VAR>Mₛ : Type u_4<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup Mₛ<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ inst✝³ : Module R Mₛ<VAR>inst✝² : Module Rₛ Mₛ<VAR>f : M →ₗ[R] Mₛ<VAR>inst✝¹ : IsLocalizedModule S f<VAR>inst✝ : IsScalarTower R Rₛ Mₛ<VAR>ι : Type u_5<VAR>b : Basis ι R M<VAR>m : M<VAR>i : ι<GOAL>((ofIsLocalizedModule Rₛ S f b).repr (f m)) i = (algebraMap R Rₛ) ((b.repr m) i)
<VAR>R : Type u_1<VAR>Rₛ : Type u_2<VAR>inst✝¹⁰ : CommSemiring R<VAR>S : Submonoid R<VAR>inst✝⁹ : CommRing Rₛ<VAR>inst✝⁸ : Algebra R Rₛ<VAR>hT : IsLocalization S Rₛ<VAR>M : Type u_3<VAR>Mₛ : Type u_4<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup Mₛ<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ inst✝³ : Module R Mₛ<VAR>inst✝² : Module Rₛ Mₛ<VAR>f : M →ₗ[R] Mₛ<VAR>inst✝¹ : IsLocalizedModule S f<VAR>inst✝ : IsScalarTower R Rₛ Mₛ<VAR>ι : Type u_5<VAR>b : Basis ι R M<VAR>m : M<VAR>i : ι<GOAL>↑R ↑(ofIsLocalizedModule Rₛ S f b).repr ∘ₗ f = Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ) ∘ₗ ↑b.repr
<VAR>R : Type u_1<VAR>Rₛ : Type u_2<VAR>inst✝¹⁰ : CommSemiring R<VAR>S : Submonoid R<VAR>inst✝⁹ : CommRing Rₛ<VAR>inst✝⁸ : Algebra R Rₛ<VAR>hT : IsLocalization S Rₛ<VAR>M : Type u_3<VAR>Mₛ : Type u_4<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup Mₛ<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ inst✝³ : Module R Mₛ<VAR>inst✝² : Module Rₛ Mₛ<VAR>f : M →ₗ[R] Mₛ<VAR>inst✝¹ : IsLocalizedModule S f<VAR>inst✝ : IsScalarTower R Rₛ Mₛ<VAR>ι : Type u_5<VAR>b : Basis ι R M<VAR>m : M<VAR>i✝ i : ι<GOAL>(↑R ↑(ofIsLocalizedModule Rₛ S f b).repr ∘ₗ f) (b i) = (Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ) ∘ₗ ↑b.repr) (b i)
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>ht : t ∈ 𝓝 x<GOAL>(fderivWithin 𝕜 f (s ∩ t) x) 1 = (fderivWithin 𝕜 f s x) 1
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝¹⁰ : Semiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁷ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝⁴ : FunLike F M M₂<VAR>inst✝³ : SemilinearMapClass F σ₁₂ M M₂<VAR>s✝ t : Set M<VAR>inst✝² : SetLike S M<VAR>inst✝¹ : AddSubmonoidClass S M<VAR>inst✝ : SMulMemClass S R M<VAR>s : S<GOAL>↑(span R ↑s) = ↑s
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝¹⁰ : Semiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁷ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝⁴ : FunLike F M M₂<VAR>inst✝³ : SemilinearMapClass F σ₁₂ M M₂<VAR>s✝ t : Set M<VAR>inst✝² : SetLike S M<VAR>inst✝¹ : AddSubmonoidClass S M<VAR>inst✝ : SMulMemClass S R M<VAR>s : S<GOAL>↑(span R ↑s) ≤ ↑s
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝¹⁰ : Semiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁷ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝⁴ : FunLike F M M₂<VAR>inst✝³ : SemilinearMapClass F σ₁₂ M M₂<VAR>s✝ t : Set M<VAR>inst✝² : SetLike S M<VAR>inst✝¹ : AddSubmonoidClass S M<VAR>inst✝ : SMulMemClass S R M<VAR>s : S<VAR>s' : Submodule R M := { carrier := ↑s, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }<GOAL>↑(span R ↑s) ≤ ↑s
<VAR>x n m : ℕ<VAR>x✝ : x ∣ n * m<VAR>y : ℕ<VAR>hy : n * m = x * y<GOAL>x ∣ x.gcd n * m
<VAR>x n m : ℕ<VAR>x✝ : x ∣ n * m<VAR>y : ℕ<VAR>hy : n * m = x * y<GOAL>x ∣ x * m.gcd y
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>m✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s : Set α<VAR>hμs : μ s ≠ ⊤<VAR>hνs : ν s ≠ ⊤<VAR>x : F<GOAL>(weightedSMul (μ + ν) s) x = (⇑(weightedSMul μ s) + ⇑(weightedSMul ν s)) x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>m✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s : Set α<VAR>hμs : μ s ≠ ⊤<VAR>hνs : ν s ≠ ⊤<VAR>x : F<GOAL>((μ + ν) s).toReal • x = (μ s).toReal • x + (ν s).toReal • x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>m✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s : Set α<VAR>hμs : μ s ≠ ⊤<VAR>hνs : ν s ≠ ⊤<VAR>x : F<GOAL>((⇑μ + ⇑ν) s).toReal • x = (μ s).toReal • x + (ν s).toReal • x
<VAR>Γ : Type u_1<VAR>inst✝² : Inhabited Γ<VAR>Λ : Type u_2<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_3<VAR>inst✝ : Inhabited σ<VAR>n : ℕ<VAR>enc : Γ → Vector Bool n<VAR>dec : Vector Bool n → Γ<VAR>S : Finset Λ'<VAR>f✝ : Γ → Stmt Bool Λ' σ<VAR>this : ∀ (i : ℕ) (f : Vector Bool i → Stmt Bool Λ' σ), (∀ (v : Vector Bool i), SupportsStmt S (f v)) → SupportsStmt S (readAux i f)<VAR>hf : ∀ (a : Γ), SupportsStmt S (f✝ a)<VAR>v✝ : Vector Bool n<GOAL>SupportsStmt S (move Dir.left (f✝ (dec v✝)))
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : GroupWithZero G₀<VAR>a b c : G₀<VAR>hac : Commute a c<VAR>hbc : Commute b c<GOAL>Commute (a / b) c
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : GroupWithZero G₀<VAR>a b c : G₀<VAR>hac : Commute a c<VAR>hbc : Commute b c<GOAL>Commute (a * b⁻¹) c
<VAR>s n : Nat<GOAL>range' s (n + 1) = range' s n ++ [s + n]
<VAR>α : Type u_1<VAR>inst✝⁵ : CancelCommMonoidWithZero α<VAR>inst✝⁴ : UniqueFactorizationMonoid α<VAR>inst✝³ : DecidableEq (Associates α)<VAR>inst✝² : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝¹ : Nontrivial α<VAR>inst✝ : DecidableEq (Associates α)<VAR>p : Associates α<VAR>hp : Irreducible p<GOAL>p.count p.factors = 1
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>S₁ S₂ : Split C<VAR>Φ : S₁ ⟶ S₂<VAR>Δ : SimplexCategoryᵒᵖ<VAR>A : Splitting.IndexSet Δ<GOAL>(S₁.s.cofan Δ).inj A ≫ Φ.F.app Δ = Φ.f (unop A.fst).len ≫ (S₂.s.cofan Δ).inj A
<VAR>s : Finset ℕ<VAR>m n p : ℕ<GOAL>Squarefree 2
<VAR>R : Type u<VAR>ι : Type w<VAR>s✝ : Finset ι<VAR>inst✝ : CommRing R<VAR>s : Finset ι<VAR>f : ι → R<GOAL>(∏ i ∈ s, (X - C (f i))).nextCoeff = -∑ i ∈ s, f i