ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>f g : L ≃ₐ[K] L<VAR>hf' : ∃ m, f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m<VAR>hg' : ∃ m, g ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m<VAR>hfg : hf'.choose ≡ hg'.choose [MOD ↑n]<VAR>hf : f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ hf'.choose<VAR>hg : g ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ hg'.choose<GOAL>orderOf hμ.toRootsOfUnity = orderOf ↑↑hμ.toRootsOfUnity
<VAR>s : ℝ<GOAL>Gamma s = 0 → ∃ m, s = -↑m
<VAR>s : ℝ<GOAL>(∀ (m : ℕ), s ≠ -↑m) → Gamma s ≠ 0
<VAR>m : ℕ<GOAL>Gamma (-↑m) = 0
<VAR>C : Type u_2<VAR>inst✝⁵ : Category.{u_1, u_2} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>S₁ S₂ S₃ S₄ : ShortComplex C<VAR>inst✝³ : S₁.HasHomology<VAR>inst✝² : S₂.HasHomology<VAR>inst✝¹ : S₃.HasHomology<VAR>inst✝ : S₄.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>γ : RightHomologyMapData φ h₁ h₂<GOAL>QuasiIso φ ↔ IsIso γ.φH
<VAR>C : Type u_2<VAR>inst✝⁵ : Category.{u_1, u_2} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>S₁ S₂ S₃ S₄ : ShortComplex C<VAR>inst✝³ : S₁.HasHomology<VAR>inst✝² : S₂.HasHomology<VAR>inst✝¹ : S₃.HasHomology<VAR>inst✝ : S₄.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>γ : RightHomologyMapData φ h₁ h₂<GOAL>IsIso (h₁.homologyIso.hom ≫ γ.φH ≫ h₂.homologyIso.inv) ↔ IsIso γ.φH
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<VAR>r k : ℕ<VAR>ih : ∀ {t : Finset α}, t ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ u, u.card = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜<VAR>t : Finset α<GOAL>t ∈ ∂⁺ ^[k + 1] 𝒜 ↔ ∃ u, u.card = k + 1 ∧ u ⊆ t ∧ t \ u ∈ 𝒜
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<VAR>r k : ℕ<VAR>ih : ∀ {t : Finset α}, t ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ u, u.card = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜<VAR>t : Finset α<GOAL>(∃ a ∈ t, ∃ u, u.card = k ∧ (u ⊆ t ∧ a ∉ u) ∧ t \ insert a u ∈ 𝒜) ↔ ∃ u, (∃ a t, a ∉ t ∧ insert a t = u ∧ t.card = k) ∧ u ⊆ t ∧ t \ u ∈ 𝒜
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p✝ q a p : R[X]<VAR>hp : p.Monic<VAR>hap : a ∣ p<GOAL>a.leadingCoeff ∣ 1
<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>X : C<VAR>f : J → C<VAR>j : J<GOAL>(leftDistributor X f).hom ≫ biproduct.π (fun j => X ⊗ f j) j = X ◁ biproduct.π f 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 t : Set α<VAR>x : α<GOAL>s ⊆ insert x t ↔ s ⊆ t ∨ x ∈ s ∧ s \ {x} ⊆ t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u s t : Set α<VAR>x : α<GOAL>s \ {x} ⊆ t ↔ s ⊆ t ∨ x ∈ s ∧ s \ {x} ⊆ t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u s t : Set α<VAR>x : α<VAR>hx : x ∉ s<GOAL>s \ {x} ⊆ t ↔ s ⊆ t ∨ x ∈ s ∧ s \ {x} ⊆ t
<VAR>F : Type u_1<VAR>inst✝⁶ : Field F<VAR>E : Type u_2<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>L : Type u_3<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>x : L<VAR>hx : IsIntegral K x<GOAL>FiniteDimensional.finrank K ↥K⟮x⟯ = (minpoly K x).natDegree
<VAR>F : Type u_1<VAR>inst✝⁶ : Field F<VAR>E : Type u_2<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>L : Type u_3<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>x : L<VAR>hx : IsIntegral K x<GOAL>(powerBasis hx).dim = (minpoly K x).natDegree
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>m n : ℕ<VAR>h : n ≤ m<GOAL>yz a1 (m - n) = xz a1 n * yz a1 m - xz a1 m * yz a1 n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>m n : ℕ<VAR>h : n ≤ m<GOAL>yz a1 (m - n) = xz a1 m * -yz a1 n + yz a1 m * xz a1 n
<VAR>a b : ℤ<VAR>ha : a ≠ 0<GOAL>IsLeast {n | 0 < n ∧ ∃ x y, ↑n = a * x + b * y} (a.gcd b)
<VAR>a b : ℤ<VAR>ha : a ≠ 0<GOAL>IsLeast {n | 0 < n ∧ a.gcd b ∣ n} (a.gcd b)
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁴ : Ring K<VAR>inst✝³ : StrongRankCondition K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module.Free K V<GOAL>Module.rank K V ≤ 1 ↔ ∃ v₀, ∀ (v : V), ∃ r, r • v₀ = v
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁴ : Ring K<VAR>inst✝³ : StrongRankCondition K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module.Free K V<VAR>κ : Type v<VAR>b : Basis κ K V<GOAL>Module.rank K V ≤ 1 ↔ ∃ v₀, ∀ (v : V), ∃ r, r • v₀ = v
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y : ℝ<GOAL>Ioo x y = ball ((x + y) / 2) ((y - x) / 2)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>a✝ : α<VAR>b✝ : β<VAR>h₀ : ∀ (b : β), Antitone (swap f b)<VAR>h₁ : ∀ (a : α), Antitone (f a)<VAR>a : α<VAR>ha : a ∈ upperBounds s<VAR>b : β<VAR>hb : b ∈ upperBounds t<GOAL>BddBelow (image2 f s t)
<VAR>x : ℝ<VAR>h₁ : -1 < x<VAR>h₂ : x < 1<GOAL>2 * arctan x = arctan (2 * x / (1 - x ^ 2))
<VAR>x : ℝ<VAR>h₁ : -1 < x<VAR>h₂ : x < 1<GOAL>arctan ((x + x) / (1 - x * x)) = arctan (2 * x / (1 - x ^ 2))
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : CommMonoid α<VAR>inst✝³ : CommMonoid β<VAR>inst✝² : CommMonoid γ<VAR>A A₁ A₂ : Set α<VAR>B B₁ B₂ : Set β<VAR>C : Set γ<VAR>f✝ f₁ f₂ : α → β<VAR>g : β → γ<VAR>m n : ℕ<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : MonoidHomClass F α β<VAR>f : F<VAR>hfAB : MapsTo (⇑f) A B<VAR>s t : Multiset α<VAR>x✝³ : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>x✝² : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>x✝¹ : card s = n<VAR>x✝ : card t = n<VAR>h : s.prod = t.prod<GOAL>(map (⇑f) s).prod = (map (⇑f) t).prod
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>inst✝ : PartialOrder α<VAR>a b : α<VAR>ha : μ {a} = 0<GOAL>Iio a =ᶠ[ae μ] Iic a
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hm : m ≤ m0<VAR>hfint : Integrable f μ<GOAL>∫ (x : α), |(μ[f|m]) x| ∂μ ≤ ∫ (x : α), |f x| ∂μ
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hm : m ≤ m0<VAR>hfint : Integrable f μ<GOAL>(∫⁻ (a : α), ENNReal.ofReal |(μ[f|m]) a| ∂μ).toReal ≤ (∫⁻ (a : α), ENNReal.ofReal |f a| ∂μ).toReal
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hm : m ≤ m0<VAR>hfint : Integrable f μ<GOAL>0 ≤ᶠ[ae μ] fun x => |f x|
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hm : m ≤ m0<VAR>hfint : Integrable f μ<GOAL>AEStronglyMeasurable (fun x => |f x|) μ
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hm : m ≤ m0<VAR>hfint : Integrable f μ<GOAL>0 ≤ᶠ[ae μ] fun x => |(μ[f|m]) x|
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hm : m ≤ m0<VAR>hfint : Integrable f μ<GOAL>AEStronglyMeasurable (fun x => |(μ[f|m]) x|) μ
<VAR>I : Type u<VAR>inst✝¹⁰ : AddMonoid I<VAR>C : Type u_1<VAR>inst✝⁹ : Category.{u_2, u_1} C<VAR>inst✝⁸ : MonoidalCategory C<VAR>Z : C<VAR>X₁ X₂ X₃ : GradedObject I C<VAR>inst✝⁷ : X₁.HasTensor X₂<VAR>inst✝⁶ : X₂.HasTensor X₃<VAR>inst✝⁵ : (tensorObj X₁ X₂).HasTensor X₃<VAR>inst✝⁴ : X₁.HasTensor (tensorObj X₂ X₃)<VAR>Y₁ Y₂ Y₃ : GradedObject I C<VAR>inst✝³ : Y₁.HasTensor Y₂<VAR>inst✝² : Y₂.HasTensor Y₃<VAR>inst✝¹ : (tensorObj Y₁ Y₂).HasTensor Y₃<VAR>inst✝ : Y₁.HasTensor (tensorObj Y₂ Y₃)<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₂<VAR>f₃ : X₃ ⟶ Y₃<VAR>i₁ i₂ i₃ j : I<VAR>h : i₁ + i₂ + i₃ = j<GOAL>ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ tensorHom f₁ (tensorHom f₂ f₃) j = (f₁ i₁ ⊗ f₂ i₂ ⊗ f₃ i₃) ≫ ιTensorObj₃ Y₁ Y₂ Y₃ i₁ i₂ i₃ j h
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasShift C ℤ<VAR>X : Cᵒᵖ<VAR>a₁ a₂ a₃ : ℤ<VAR>h : a₁ + a₂ = a₃<VAR>b₁ b₂ b₃ : ℤ<VAR>h₁ : a₁ + b₁ = 0<VAR>h₂ : a₂ + b₂ = 0<VAR>h₃ : a₃ + b₃ = 0<GOAL>(shiftFunctorAdd' Cᵒᵖ a₁ a₂ a₃ h).inv.app X = (shiftFunctor Cᵒᵖ a₂).map ((shiftFunctorOpIso C a₁ b₁ h₁).hom.app X) ≫ (shiftFunctorOpIso C a₂ b₂ h₂).hom.app ((shiftFunctor C b₁).op.obj X) ≫ ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).hom.app (Opposite.unop X)).op ≫ (shiftFunctorOpIso C a₃ b₃ h₃).inv.app X
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasShift C ℤ<VAR>X : Cᵒᵖ<VAR>a₁ a₂ a₃ : ℤ<VAR>h : a₁ + a₂ = a₃<VAR>b₁ b₂ b₃ : ℤ<VAR>h₁ : a₁ + b₁ = 0<VAR>h₂ : a₂ + b₂ = 0<VAR>h₃ : a₃ + b₃ = 0<GOAL>𝟙 ((shiftFunctor Cᵒᵖ a₃).obj X) = (shiftFunctorOpIso C a₃ b₃ h₃).hom.app X ≫ ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).inv.app (Opposite.unop X)).op ≫ (shiftFunctorOpIso C a₂ b₂ h₂).inv.app (Opposite.op ((shiftFunctor C b₁).toPrefunctor.1 (Opposite.unop X))) ≫ (shiftFunctor Cᵒᵖ a₂).map (𝟙 ((shiftFunctor C b₁).op.obj X)) ≫ (shiftFunctorOpIso C a₂ b₂ h₂).hom.app ((shiftFunctor C b₁).op.obj X) ≫ ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).hom.app (Opposite.unop X)).op ≫ (shiftFunctorOpIso C a₃ b₃ h₃).inv.app X
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasShift C ℤ<VAR>X : Cᵒᵖ<VAR>a₁ a₂ a₃ : ℤ<VAR>h : a₁ + a₂ = a₃<VAR>b₁ b₂ b₃ : ℤ<VAR>h₁ : a₁ + b₁ = 0<VAR>h₂ : a₂ + b₂ = 0<VAR>h₃ : a₃ + b₃ = 0<GOAL>𝟙 ((shiftFunctor Cᵒᵖ a₃).obj X) = (shiftFunctorOpIso C a₃ b₃ h₃).hom.app X ≫ ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).inv.app (Opposite.unop X)).op ≫ ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).hom.app (Opposite.unop X)).op ≫ (shiftFunctorOpIso C a₃ b₃ h₃).inv.app X
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>inst✝⁴ : IsPrincipalIdealRing R<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>b : ι → M<VAR>n : ℕ<VAR>N : Submodule R M<VAR>snf : SmithNormalForm N ι n<VAR>m : ↥N<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>f : M →ₗ[R] M<VAR>hf : ∀ (x : M), f x ∈ N<VAR>hf' : optParam (∀ x ∈ N, f x ∈ N) ⋯<VAR>i : Fin n<GOAL>(LinearMap.toMatrix snf.bN snf.bN) (f.restrict hf') i i = (LinearMap.toMatrix snf.bM snf.bM) f (snf.f i) (snf.f i)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>inst✝⁴ : IsPrincipalIdealRing R<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>b : ι → M<VAR>n : ℕ<VAR>N : Submodule R M<VAR>snf : SmithNormalForm N ι n<VAR>m : ↥N<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>f : M →ₗ[R] M<VAR>hf : ∀ (x : M), f x ∈ N<VAR>hf' : optParam (∀ x ∈ N, f x ∈ N) ⋯<VAR>i : Fin n<GOAL>(snf.bN.repr ((f.restrict hf') (snf.bN i))) i = (snf.bN.repr (snf.a i • ⟨f (snf.bM (snf.f i)), ⋯⟩)) i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>inst✝⁴ : IsPrincipalIdealRing R<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>b : ι → M<VAR>n : ℕ<VAR>N : Submodule R M<VAR>snf : SmithNormalForm N ι n<VAR>m : ↥N<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>f : M →ₗ[R] M<VAR>hf : ∀ (x : M), f x ∈ N<VAR>hf' : optParam (∀ x ∈ N, f x ∈ N) ⋯<VAR>i : Fin n<GOAL>↑((f.restrict hf') (snf.bN i)) = ↑(snf.a i • ⟨f (snf.bM (snf.f i)), ⋯⟩)
<VAR>θ : Angle<GOAL>(2 • θ).toReal = 2 * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / 2) (π / 2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoid α<VAR>p : Multiset α<VAR>a : α<VAR>s : Multiset α<VAR>ih : (Multiset.map Associates.mk s).prod = Associates.mk s.prod<GOAL>(Multiset.map Associates.mk (a ::ₘ s)).prod = Associates.mk (a ::ₘ s).prod
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.1332, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>P : Karoubi (SimplicialObject C)<VAR>α : N.obj ((𝟭 (Karoubi (SimplicialObject C))).obj P) ≅ N.obj ((N₂ ⋙ Γ₂).obj P) := N.mapIso (Γ₂N₂.app P)<VAR>β : (Γ₂ ⋙ N₂).obj (N.obj P) ≅ (𝟭 (Karoubi (ChainComplex C ℕ))).obj (N.obj P) := N₂Γ₂.app (N.obj P)<GOAL>𝟙 (N.obj ((𝟭 (Karoubi (SimplicialObject C))).obj P)) = α.hom ≫ β.hom
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.1332, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>P : Karoubi (SimplicialObject C)<VAR>α : N.obj ((𝟭 (Karoubi (SimplicialObject C))).obj P) ≅ N.obj ((N₂ ⋙ Γ₂).obj P) := N.mapIso (Γ₂N₂.app P)<VAR>β : (Γ₂ ⋙ N₂).obj (N.obj P) ≅ (𝟭 (Karoubi (ChainComplex C ℕ))).obj (N.obj P) := N₂Γ₂.app (N.obj P)<GOAL>β.inv ≫ α.inv = 𝟙 ((𝟭 (Karoubi (ChainComplex C ℕ))).obj (N.obj P))
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>H : Type u_2<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<GOAL>MetrizableSpace M
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>H : Type u_2<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>this : LocallyCompactSpace H<GOAL>MetrizableSpace M
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>H : Type u_2<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>this✝ : LocallyCompactSpace H<VAR>this : LocallyCompactSpace M<GOAL>MetrizableSpace M
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>H : Type u_2<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>this✝¹ : LocallyCompactSpace H<VAR>this✝ : LocallyCompactSpace M<VAR>this : SecondCountableTopology H<GOAL>MetrizableSpace M
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>H : Type u_2<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>this✝² : LocallyCompactSpace H<VAR>this✝¹ : LocallyCompactSpace M<VAR>this✝ : SecondCountableTopology H<VAR>this : SecondCountableTopology M<GOAL>MetrizableSpace M
<VAR>p : ℕ<GOAL>(Summable fun n => 1 / ↑n ^ p) ↔ 1 < p
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ : E → F<VAR>f' : F<VAR>s t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F<VAR>h : f₀ =ᶠ[𝓝 x] f₁<GOAL>HasLineDerivAt 𝕜 f₀ f' x v ↔ HasLineDerivAt 𝕜 f₁ f' x v
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ : E → F<VAR>f' : F<VAR>s t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F<VAR>h : f₀ =ᶠ[𝓝 x] f₁<GOAL>(fun t => f₀ (x + t • v)) =ᶠ[𝓝 0] fun t => f₁ (x + t • v)
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F✝ : Type u_2<VAR>inst✝³ : NormedAddCommGroup F✝<VAR>inst✝² : NormedSpace 𝕜 F✝<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ : E → F✝<VAR>f' : F✝<VAR>s t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F✝<VAR>h : f₀ =ᶠ[𝓝 x] f₁<VAR>F : 𝕜 → E := fun t => x + t • v<GOAL>(fun t => f₀ (x + t • v)) =ᶠ[𝓝 0] fun t => f₁ (x + t • v)
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F✝ : Type u_2<VAR>inst✝³ : NormedAddCommGroup F✝<VAR>inst✝² : NormedSpace 𝕜 F✝<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ : E → F✝<VAR>f' : F✝<VAR>s t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F✝<VAR>h : f₀ =ᶠ[𝓝 x] f₁<VAR>F : 𝕜 → E := fun t => x + t • v<VAR>B : ContinuousAt F 0<GOAL>(fun t => f₀ (x + t • v)) =ᶠ[𝓝 0] fun t => f₁ (x + t • v)
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F✝ : Type u_2<VAR>inst✝³ : NormedAddCommGroup F✝<VAR>inst✝² : NormedSpace 𝕜 F✝<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ : E → F✝<VAR>f' : F✝<VAR>s t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F✝<VAR>h : f₀ =ᶠ[𝓝 x] f₁<VAR>F : 𝕜 → E := fun t => x + t • v<VAR>B : ContinuousAt F 0<VAR>this : f₀ =ᶠ[𝓝 (F 0)] f₁<GOAL>(fun t => f₀ (x + t • v)) =ᶠ[𝓝 0] fun t => f₁ (x + t • v)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u : Multiset α<VAR>a b : α<VAR>s t : Multiset α<GOAL>s ∪ t + s ∩ t = s + t
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u : Multiset α<VAR>a b : α<VAR>s t : Multiset α<GOAL>s ∪ t + s ∩ t ≤ s + t
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u : Multiset α<VAR>a b : α<VAR>s t : Multiset α<GOAL>s + t ≤ s ∪ t + s ∩ t
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>f✝ g✝ : α → ℝ<VAR>s✝ : Set α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>f_mble : AEMeasurable f μ<VAR>g_mble : AEMeasurable g μ<VAR>s : Set α<VAR>s_mble : NullMeasurableSet s μ<GOAL>NullMeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Ico (f p.1) (g p.1)} (μ.prod volume)
<VAR>X✝ : Scheme<VAR>P : {X : Scheme} → X.Opens → Prop<VAR>X : Scheme<VAR>U : X.Opens<VAR>h₁ : ∀ (X : Scheme) (U : X.Opens), (∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ x, P V) → P U<VAR>h₂ : ∀ (X Y : Scheme) (f : X ⟶ Y) [hf : IsOpenImmersion f], ∃ U V, ∃ (hU : U = ⊤) (hV : V = Set.range ⇑f.val.base), P { carrier := U, is_open' := ⋯ } → P { carrier := V, is_open' := ⋯ }<VAR>h₃ : ∀ (R : CommRingCat), P ⊤<VAR>x : ↥U<GOAL>∃ V, ∃ (_ : ↑x ∈ V), ∃ x, P V
<VAR>X✝ : Scheme<VAR>P : {X : Scheme} → X.Opens → Prop<VAR>X : Scheme<VAR>U : X.Opens<VAR>h₁ : ∀ (X : Scheme) (U : X.Opens), (∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ x, P V) → P U<VAR>h₂ : ∀ (X Y : Scheme) (f : X ⟶ Y) [hf : IsOpenImmersion f], ∃ U V, ∃ (hU : U = ⊤) (hV : V = Set.range ⇑f.val.base), P { carrier := U, is_open' := ⋯ } → P { carrier := V, is_open' := ⋯ }<VAR>h₃ : ∀ (R : CommRingCat), P ⊤<VAR>x : ↥U<VAR>j : X.affineBasisCover.J<VAR>hx : ↑x ∈ Set.range ⇑(X.affineBasisCover.map j).val.base<VAR>i : Set.range ⇑(X.affineBasisCover.map j).val.base ⊆ ↑U<GOAL>∃ V, ∃ (_ : ↑x ∈ V), ∃ x, P V
<VAR>X✝ : Scheme<VAR>P : {X : Scheme} → X.Opens → Prop<VAR>X : Scheme<VAR>U : X.Opens<VAR>h₁ : ∀ (X : Scheme) (U : X.Opens), (∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ x, P V) → P U<VAR>h₂ : ∀ (X Y : Scheme) (f : X ⟶ Y) [hf : IsOpenImmersion f], ∃ U V, ∃ (hU : U = ⊤) (hV : V = Set.range ⇑f.val.base), P { carrier := U, is_open' := ⋯ } → P { carrier := V, is_open' := ⋯ }<VAR>h₃ : ∀ (R : CommRingCat), P ⊤<VAR>x : ↥U<VAR>j : X.affineBasisCover.J<VAR>hx : ↑x ∈ Set.range ⇑(X.affineBasisCover.map j).val.base<VAR>i : Set.range ⇑(X.affineBasisCover.map j).val.base ⊆ ↑U<VAR>U' : Opens ↑↑X.toPresheafedSpace := { carrier := Set.range ⇑(X.affineBasisCover.map j).val.base, is_open' := ⋯ }<GOAL>∃ V, ∃ (_ : ↑x ∈ V), ∃ x, P V
<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 G : C ⥤ D<VAR>α : F ≅ G<VAR>X : D<VAR>Y : C<VAR>f f' : X ⟶ F.obj Y<GOAL>f ≫ α.hom.app Y = f' ≫ α.hom.app Y ↔ f = f'
<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 : α → β<VAR>s : Set β<GOAL>f ⁻¹' (f '' (f ⁻¹' s)) = f ⁻¹' s
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>inst✝¹ : SeminormedAddCommGroup α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>x₁ x₂ : α<GOAL>nndist ((WithLp.equiv p (α × β)).symm (x₁, 0)) ((WithLp.equiv p (α × β)).symm (x₂, 0)) = nndist x₁ x₂
<VAR>L : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>x : 𝓞 K<GOAL>(norm K) ((algebraMap (𝓞 K) (𝓞 L)) x) = x ^ finrank K L
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>f✝¹ : ℝ → E<VAR>g' g✝ φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝² : CompleteSpace E<VAR>f✝ f'✝ : ℝ → E<VAR>G : Type u_6<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f f' : ℝ → ℝ<VAR>g : ℝ → G<VAR>hf : ContinuousOn f [[a, b]]<VAR>hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x<VAR>hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))<VAR>hg1 : IntegrableOn g (f '' [[a, b]]) volume<VAR>hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]] volume<VAR>hG : CompleteSpace G<GOAL>∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>f✝¹ : ℝ → E<VAR>g' g✝ φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝² : CompleteSpace E<VAR>f✝ f'✝ : ℝ → E<VAR>G : Type u_6<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f f' : ℝ → ℝ<VAR>g : ℝ → G<VAR>hf : ContinuousOn f [[a, b]]<VAR>hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x<VAR>hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))<VAR>hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))<VAR>hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]] volume<VAR>hG : CompleteSpace G<GOAL>∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>f✝¹ : ℝ → E<VAR>g' g✝ φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝² : CompleteSpace E<VAR>f✝ f'✝ : ℝ → E<VAR>G : Type u_6<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f f' : ℝ → ℝ<VAR>g : ℝ → G<VAR>hf : ContinuousOn f [[a, b]]<VAR>hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x<VAR>hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))<VAR>hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))<VAR>hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]] volume<VAR>hG : CompleteSpace G<VAR>h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]<GOAL>∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>f✝¹ : ℝ → E<VAR>g' g✝ φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝² : CompleteSpace E<VAR>f✝ f'✝ : ℝ → E<VAR>G : Type u_6<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f f' : ℝ → ℝ<VAR>g : ℝ → G<VAR>hf : ContinuousOn f [[a, b]]<VAR>hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x<VAR>hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))<VAR>hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))<VAR>hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]] volume<VAR>hG : CompleteSpace G<VAR>h_cont : ContinuousOn (fun u => ∫ (t : ℝ) in f a..f u, g t) [[a, b]]<VAR>h_der : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt (fun u => ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x<GOAL>∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u