ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>J : Type u_4<VAR>inst✝⁷ : Category.{u_5, u_1} C<VAR>inst✝⁶ : Preadditive C<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c : ComplexShape J<VAR>inst✝⁵ : TotalComplexShape c₁ c₂ c<VAR>inst✝⁴ : TotalComplexShape c₂ c₁ c<VAR>inst✝³ : TotalComplexShapeSymmetry c₁ c₂ c<VAR>inst✝² : K.HasTotal c<VAR>inst✝¹ : K.flip.HasTotal c<VAR>inst✝ : DecidableEq J<VAR>j j' : J<GOAL>(K.totalFlipIso c).hom.f j ≫ K.D₂ c j j' = K.flip.D₁ c j j' ≫ (K.totalFlipIso c).hom.f j'
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝ : NonUnitalNonAssocRing R<VAR>a b x y x' y' : R<VAR>ha : SemiconjBy a x y<VAR>hb : SemiconjBy b x y<GOAL>SemiconjBy (a - b) x y
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>X✝ Y✝ : C<VAR>inst✝¹ : HasBinaryBiproduct X✝ Y✝<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : IsSplitMono f<VAR>c : CokernelCofork f<VAR>i : IsColimit c<GOAL>(splitEpiOfIdempotentOfIsColimitCofork C ⋯ (isColimitCoforkOfCokernelCofork (isCokernelEpiComp i (retraction f) ⋯))).section_ ≫ retraction f = 0
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>X✝ Y✝ : C<VAR>inst✝¹ : HasBinaryBiproduct X✝ Y✝<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : IsSplitMono f<VAR>c : CokernelCofork f<VAR>i : IsColimit c<GOAL>i.desc (Cofork.ofπ (Cofork.π (cokernelCoforkOfCofork (Cofork.ofπ (𝟙 Y - retraction f ≫ f) ⋯))) ⋯) ≫ retraction f = 0
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>X✝ Y✝ : C<VAR>inst✝¹ : HasBinaryBiproduct X✝ Y✝<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : IsSplitMono f<VAR>c : CokernelCofork f<VAR>i : IsColimit c<GOAL>i.desc (Cofork.ofπ (Cofork.π (CokernelCofork.ofπ (𝟙 Y - retraction f ≫ f) ⋯)) ⋯) ≫ retraction f = 0
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>X✝ Y✝ : C<VAR>inst✝¹ : HasBinaryBiproduct X✝ Y✝<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : IsSplitMono f<VAR>c : CokernelCofork f<VAR>i : IsColimit c<VAR>this : Epi (Cofork.π c) := epi_of_isColimit_cofork i<GOAL>i.desc (Cofork.ofπ (Cofork.π (CokernelCofork.ofπ (𝟙 Y - retraction f ≫ f) ⋯)) ⋯) ≫ retraction f = 0
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>X✝ Y✝ : C<VAR>inst✝¹ : HasBinaryBiproduct X✝ Y✝<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : IsSplitMono f<VAR>c : CokernelCofork f<VAR>i : IsColimit c<VAR>this : Epi (Cofork.π c) := epi_of_isColimit_cofork i<GOAL>Cofork.π c ≫ i.desc (Cofork.ofπ (Cofork.π (CokernelCofork.ofπ (𝟙 Y - retraction f ≫ f) ⋯)) ⋯) ≫ retraction f = 0
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>X✝ Y✝ : C<VAR>inst✝¹ : HasBinaryBiproduct X✝ Y✝<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : IsSplitMono f<VAR>c : CokernelCofork f<VAR>i : IsColimit c<VAR>this : Epi (Cofork.π c) := epi_of_isColimit_cofork i<GOAL>𝟙 Y ≫ retraction f - retraction f = 0
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>X✝ Y✝ : C<VAR>inst✝¹ : HasBinaryBiproduct X✝ Y✝<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : IsSplitMono f<VAR>c : CokernelCofork f<VAR>i : IsColimit c<VAR>this : Epi (Cofork.π c) := epi_of_isColimit_cofork i<GOAL>𝟙 Y ≫ retraction f = retraction f
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>X✝ Y✝ : C<VAR>inst✝¹ : HasBinaryBiproduct X✝ Y✝<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : IsSplitMono f<VAR>c : CokernelCofork f<VAR>i : IsColimit c<GOAL>(let c' := CokernelCofork.ofπ (Cofork.π c) ⋯; let i' := isCokernelEpiComp i (retraction f) ⋯; let i'' := isColimitCoforkOfCokernelCofork i'; (splitEpiOfIdempotentOfIsColimitCofork C ⋯ i'').section_) ≫ Cofork.π c = 𝟙 c.pt
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ η : Kernel α β<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>a : α<VAR>g : β → ℝ≥0∞<GOAL>∫⁻ (b : β), g b ∂(piecewise hs κ η) a = if a ∈ s then ∫⁻ (b : β), g b ∂κ a else ∫⁻ (b : β), g b ∂η a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ η : Kernel α β<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>a : α<VAR>g : β → ℝ≥0∞<GOAL>(∫⁻ (b : β), g b ∂if a ∈ s then κ a else η a) = if a ∈ s then ∫⁻ (b : β), g b ∂κ a else ∫⁻ (b : β), g b ∂η a
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>r : R<VAR>n : ℕ<GOAL>(coeff R n) ((C R) r).derivativeFun = (coeff R n) 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : DecidableEq β<VAR>f g : α → β<VAR>s : Finset α<VAR>t : Finset β<VAR>a : α<VAR>b c : β<VAR>inst✝ : DecidableEq α<VAR>x✝ : α<GOAL>x✝ ∈ image id s ↔ x✝ ∈ s
<VAR>α : Type u_1<VAR>inst✝ : CompleteLattice α<VAR>f : ℕ → ℕ → α<GOAL>⨆ n, f (unpair n).1 (unpair n).2 = ⨆ i, ⨆ j, f i j
<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>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>hg : HasDerivAt g₁ g₁' (h x)<VAR>hh : HasDerivAt h h' x<VAR>hy : y = h x<GOAL>HasDerivAt (g₁ ∘ h) (h' • g₁') x
<VAR>M : Type u_1<VAR>inst✝²⁹ : Monoid M<VAR>N : Type u_2<VAR>inst✝²⁸ : Monoid N<VAR>P : Type u_3<VAR>inst✝²⁷ : Monoid P<VAR>φ : M →* N<VAR>φ' : N →* M<VAR>ψ : N →* P<VAR>χ : M →* P<VAR>A : Type u_4<VAR>inst✝²⁶ : AddMonoid A<VAR>inst✝²⁵ : DistribMulAction M A<VAR>B : Type u_5<VAR>inst✝²⁴ : AddMonoid B<VAR>inst✝²³ : DistribMulAction N B<VAR>B₁ : Type u_6<VAR>inst✝²² : AddMonoid B₁<VAR>inst✝²¹ : DistribMulAction M B₁<VAR>C : Type u_7<VAR>inst✝²⁰ : AddMonoid C<VAR>inst✝¹⁹ : DistribMulAction P C<VAR>A' : Type u_8<VAR>inst✝¹⁸ : AddGroup A'<VAR>inst✝¹⁷ : DistribMulAction M A'<VAR>B' : Type u_9<VAR>inst✝¹⁶ : AddGroup B'<VAR>inst✝¹⁵ : DistribMulAction N B'<VAR>F : Type u_10<VAR>inst✝¹⁴ : FunLike F A B<VAR>R : Type u_11<VAR>inst✝¹³ : Semiring R<VAR>inst✝¹² : MulSemiringAction M R<VAR>R' : Type u_12<VAR>inst✝¹¹ : Ring R'<VAR>inst✝¹⁰ : MulSemiringAction M R'<VAR>S : Type u_13<VAR>inst✝⁹ : Semiring S<VAR>inst✝⁸ : MulSemiringAction N S<VAR>S' : Type u_14<VAR>inst✝⁷ : Ring S'<VAR>inst✝⁶ : MulSemiringAction N S'<VAR>T : Type u_15<VAR>inst✝⁵ : Semiring T<VAR>inst✝⁴ : MulSemiringAction P T<VAR>M' : Type ?u.130188<VAR>N' : Type u_16<VAR>inst✝³ : AddMonoid M'<VAR>inst✝² : DistribMulAction R M'<VAR>inst✝¹ : AddMonoid N'<VAR>inst✝ : DistribMulAction S N'<VAR>σ : R →* S<VAR>f g : R →ₑ+[σ] N'<VAR>h : f 1 = g 1<VAR>x : R<GOAL>f x = g x
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>y : ↥S<GOAL>f.toMap ↑y * ↑((IsUnit.liftRight (f.toMap.restrict S) ⋯) y)⁻¹ = 1
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹⁸ : CommSemiring R<VAR>inst✝¹⁷ : AddCommMonoid M₁<VAR>inst✝¹⁶ : Module R M₁<VAR>inst✝¹⁵ : AddCommMonoid M₂<VAR>inst✝¹⁴ : Module R M₂<VAR>inst✝¹³ : AddCommMonoid N₂<VAR>inst✝¹² : Module R N₂<VAR>inst✝¹¹ : DecidableEq n<VAR>inst✝¹⁰ : Fintype n<VAR>inst✝⁹ : DecidableEq m<VAR>inst✝⁸ : Fintype m<VAR>b₁✝ : Basis n R M₁<VAR>b₂✝ : Basis m R M₂<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis m R M₂<VAR>inst✝⁷ : AddCommMonoid M₁'<VAR>inst✝⁶ : Module R M₁'<VAR>inst✝⁵ : AddCommMonoid M₂'<VAR>inst✝⁴ : Module R M₂'<VAR>b₁' : Basis n' R M₁'<VAR>b₂' : Basis m' R M₂'<VAR>inst✝³ : Fintype n'<VAR>inst✝² : Fintype m'<VAR>inst✝¹ : DecidableEq n'<VAR>inst✝ : DecidableEq m'<VAR>c₁ : Basis n' R M₁<VAR>c₂ : Basis m' R M₂<VAR>B : M₁ →ₗ[R] M₂ →ₗ[R] R<GOAL>(b₁.toMatrix ⇑c₁)ᵀ * (toMatrix₂ b₁ b₂) B * b₂.toMatrix ⇑c₂ = (toMatrix₂ c₁ c₂) B
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹⁸ : CommSemiring R<VAR>inst✝¹⁷ : AddCommMonoid M₁<VAR>inst✝¹⁶ : Module R M₁<VAR>inst✝¹⁵ : AddCommMonoid M₂<VAR>inst✝¹⁴ : Module R M₂<VAR>inst✝¹³ : AddCommMonoid N₂<VAR>inst✝¹² : Module R N₂<VAR>inst✝¹¹ : DecidableEq n<VAR>inst✝¹⁰ : Fintype n<VAR>inst✝⁹ : DecidableEq m<VAR>inst✝⁸ : Fintype m<VAR>b₁✝ : Basis n R M₁<VAR>b₂✝ : Basis m R M₂<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis m R M₂<VAR>inst✝⁷ : AddCommMonoid M₁'<VAR>inst✝⁶ : Module R M₁'<VAR>inst✝⁵ : AddCommMonoid M₂'<VAR>inst✝⁴ : Module R M₂'<VAR>b₁' : Basis n' R M₁'<VAR>b₂' : Basis m' R M₂'<VAR>inst✝³ : Fintype n'<VAR>inst✝² : Fintype m'<VAR>inst✝¹ : DecidableEq n'<VAR>inst✝ : DecidableEq m'<VAR>c₁ : Basis n' R M₁<VAR>c₂ : Basis m' R M₂<VAR>B : M₁ →ₗ[R] M₂ →ₗ[R] R<GOAL>((toMatrix c₁ b₁) id)ᵀ * (toMatrix₂ b₁ b₂) B * (toMatrix c₂ b₂) id = (toMatrix₂ c₁ c₂) B
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : MulOneClass M<VAR>inst✝³ : MulOneClass N<VAR>inst✝² : MulOneClass P<VAR>S : Submonoid M<VAR>A : Type u_4<VAR>inst✝¹ : SetLike A M<VAR>hA : SubmonoidClass A M<VAR>S' : A<VAR>F : Type u_5<VAR>inst✝ : FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>x✝ : M<GOAL>x✝ ∈ mker 1 ↔ x✝ ∈ ⊤
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>h : IsClosed ↑A<VAR>f g : ↥A<GOAL>↑f ⊓ ↑g ∈ A
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>inst✝¹ : PreconnectedSpace α<VAR>s : ι → Set α<VAR>h_nonempty : ∀ (i : ι), (s i).Nonempty<VAR>h_disj : Pairwise (Disjoint on s)<VAR>inst✝ : Finite ι<VAR>h_closed : ∀ (i : ι), IsClosed (s i)<VAR>h_Union : ⋃ i, s i = univ<GOAL>Subsingleton ι
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>inst✝¹ : PreconnectedSpace α<VAR>s : ι → Set α<VAR>h_nonempty : ∀ (i : ι), (s i).Nonempty<VAR>h_disj : Pairwise (Disjoint on s)<VAR>inst✝ : Finite ι<VAR>h_closed : ∀ (i : ι), IsClosed (s i)<VAR>h_Union : ⋃ i, s i = univ<VAR>i : ι<GOAL>IsOpen (s i)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>inst✝¹ : PreconnectedSpace α<VAR>s : ι → Set α<VAR>h_nonempty : ∀ (i : ι), (s i).Nonempty<VAR>h_disj : Pairwise (Disjoint on s)<VAR>inst✝ : Finite ι<VAR>h_closed : ∀ (i : ι), IsClosed (s i)<VAR>h_Union : ⋃ i, s i = univ<VAR>i : ι<GOAL>IsClosed (⋃ i_1, s i_1 \ s i)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>inst✝¹ : PreconnectedSpace α<VAR>s : ι → Set α<VAR>h_nonempty : ∀ (i : ι), (s i).Nonempty<VAR>h_disj : Pairwise (Disjoint on s)<VAR>inst✝ : Finite ι<VAR>h_closed : ∀ (i : ι), IsClosed (s i)<VAR>h_Union : ⋃ i, s i = univ<VAR>i j : ι<GOAL>IsClosed (s j \ s i)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>inst✝¹ : PreconnectedSpace α<VAR>s : ι → Set α<VAR>h_nonempty : ∀ (i : ι), (s i).Nonempty<VAR>h_disj : Pairwise (Disjoint on s)<VAR>inst✝ : Finite ι<VAR>h_closed : ∀ (i : ι), IsClosed (s i)<VAR>h_Union : ⋃ i, s i = univ<VAR>i : ι<GOAL>IsClosed (s i \ s i)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>inst✝¹ : PreconnectedSpace α<VAR>s : ι → Set α<VAR>h_nonempty : ∀ (i : ι), (s i).Nonempty<VAR>h_disj : Pairwise (Disjoint on s)<VAR>inst✝ : Finite ι<VAR>h_closed : ∀ (i : ι), IsClosed (s i)<VAR>h_Union : ⋃ i, s i = univ<VAR>i j : ι<VAR>h_ne : i ≠ j<GOAL>IsClosed (s j \ s i)
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>β : Type u<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : HasBesicovitchCovering α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>f : α → Set ℝ<VAR>s : Set α<VAR>hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty<VAR>R : α → ℝ<VAR>hR : ∀ x ∈ s, 0 < R x<VAR>g : α → Set ℝ := fun x => f x ∩ Ioo 0 (R x)<GOAL>∃ t r, t.Countable ∧ t ⊆ s ∧ (∀ x ∈ t, r x ∈ f x ∩ Ioo 0 (R x)) ∧ μ (s \ ⋃ x ∈ t, closedBall x (r x)) = 0 ∧ t.PairwiseDisjoint fun x => closedBall x (r x)
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>β : Type u<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : HasBesicovitchCovering α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>f : α → Set ℝ<VAR>s : Set α<VAR>hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty<VAR>R : α → ℝ<VAR>hR : ∀ x ∈ s, 0 < R x<VAR>g : α → Set ℝ := fun x => f x ∩ Ioo 0 (R x)<VAR>hg : ∀ x ∈ s, ∀ δ > 0, (g x ∩ Ioo 0 δ).Nonempty<GOAL>∃ t r, t.Countable ∧ t ⊆ s ∧ (∀ x ∈ t, r x ∈ f x ∩ Ioo 0 (R x)) ∧ μ (s \ ⋃ x ∈ t, closedBall x (r x)) = 0 ∧ t.PairwiseDisjoint fun x => closedBall x (r x)
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>β : Type u<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : HasBesicovitchCovering α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>f : α → Set ℝ<VAR>s : Set α<VAR>hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty<VAR>R : α → ℝ<VAR>hR : ∀ x ∈ s, 0 < R x<VAR>g : α → Set ℝ := fun x => f x ∩ Ioo 0 (R x)<VAR>hg : ∀ x ∈ s, ∀ δ > 0, (g x ∩ Ioo 0 δ).Nonempty<VAR>v : Set (α × ℝ)<VAR>v_count : v.Countable<VAR>vs : ∀ p ∈ v, p.1 ∈ s<VAR>vg : ∀ p ∈ v, p.2 ∈ g p.1<VAR>μv : μ (s \ ⋃ p ∈ v, closedBall p.1 p.2) = 0<VAR>v_disj : v.PairwiseDisjoint fun p => closedBall p.1 p.2<GOAL>∃ t r, t.Countable ∧ t ⊆ s ∧ (∀ x ∈ t, r x ∈ f x ∩ Ioo 0 (R x)) ∧ μ (s \ ⋃ x ∈ t, closedBall x (r x)) = 0 ∧ t.PairwiseDisjoint fun x => closedBall x (r x)
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>β : Type u<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : HasBesicovitchCovering α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>f : α → Set ℝ<VAR>s : Set α<VAR>hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty<VAR>R : α → ℝ<VAR>hR : ∀ x ∈ s, 0 < R x<VAR>g : α → Set ℝ := fun x => f x ∩ Ioo 0 (R x)<VAR>hg : ∀ x ∈ s, ∀ δ > 0, (g x ∩ Ioo 0 δ).Nonempty<VAR>r : α → ℝ<VAR>t : Set α<VAR>v_count : (graphOn r t).Countable<VAR>vs : ∀ p ∈ graphOn r t, p.1 ∈ s<VAR>vg : ∀ p ∈ graphOn r t, p.2 ∈ g p.1<VAR>μv : μ (s \ ⋃ p ∈ graphOn r t, closedBall p.1 p.2) = 0<VAR>v_disj : (graphOn r t).PairwiseDisjoint fun p => closedBall p.1 p.2<GOAL>∃ t r, t.Countable ∧ t ⊆ s ∧ (∀ x ∈ t, r x ∈ f x ∩ Ioo 0 (R x)) ∧ μ (s \ ⋃ x ∈ t, closedBall x (r x)) = 0 ∧ t.PairwiseDisjoint fun x => closedBall x (r x)
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>β : Type u<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : HasBesicovitchCovering α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>f : α → Set ℝ<VAR>s : Set α<VAR>hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty<VAR>R : α → ℝ<VAR>hR : ∀ x ∈ s, 0 < R x<VAR>g : α → Set ℝ := fun x => f x ∩ Ioo 0 (R x)<VAR>hg : ∀ x ∈ s, ∀ δ > 0, (g x ∩ Ioo 0 δ).Nonempty<VAR>r : α → ℝ<VAR>t : Set α<VAR>v_count : (graphOn r t).Countable<VAR>vs : ∀ p ∈ graphOn r t, p.1 ∈ s<VAR>vg : ∀ p ∈ graphOn r t, p.2 ∈ g p.1<VAR>μv : μ (s \ ⋃ p ∈ graphOn r t, closedBall p.1 p.2) = 0<VAR>v_disj : (graphOn r t).PairwiseDisjoint fun p => closedBall p.1 p.2<VAR>hinj : InjOn (fun x => (x, r x)) t<GOAL>∃ t r, t.Countable ∧ t ⊆ s ∧ (∀ x ∈ t, r x ∈ f x ∩ Ioo 0 (R x)) ∧ μ (s \ ⋃ x ∈ t, closedBall x (r x)) = 0 ∧ t.PairwiseDisjoint fun x => closedBall x (r x)
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>β : Type u<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : HasBesicovitchCovering α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>f : α → Set ℝ<VAR>s : Set α<VAR>hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty<VAR>R : α → ℝ<VAR>hR : ∀ x ∈ s, 0 < R x<VAR>g : α → Set ℝ := fun x => f x ∩ Ioo 0 (R x)<VAR>hg : ∀ x ∈ s, ∀ δ > 0, (g x ∩ Ioo 0 δ).Nonempty<VAR>r : α → ℝ<VAR>t : Set α<VAR>v_count : ((fun x => (x, r x)) '' t).Countable<VAR>hinj : InjOn (fun x => (x, r x)) t<VAR>vs : ∀ ⦃x : α⦄, x ∈ t → x ∈ s<VAR>vg : ∀ ⦃x : α⦄, x ∈ t → r x ∈ g x<VAR>μv : μ (s \ ⋃ y ∈ t, closedBall y (r y)) = 0<VAR>v_disj : t.PairwiseDisjoint ((fun p => closedBall p.1 p.2) ∘ fun x => (x, r x))<GOAL>∃ t r, t.Countable ∧ t ⊆ s ∧ (∀ x ∈ t, r x ∈ f x ∩ Ioo 0 (R x)) ∧ μ (s \ ⋃ x ∈ t, closedBall x (r x)) = 0 ∧ t.PairwiseDisjoint fun x => closedBall x (r x)
<VAR>α : Type u<VAR>β : Type v<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : One M<VAR>inst✝ : One N<VAR>f : OneHom M N<GOAL>map (⇑f) 1 = 1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module.Finite R M<VAR>hM : Module.IsTorsion R M<GOAL>↑⊤.annihilator ∩ ↑R⁰ ≠ ∅
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module.Finite R M<VAR>hM : Module.IsTorsion R M<VAR>S : Finset M<VAR>hS : span R ↑S = ⊤<GOAL>↑⊤.annihilator ∩ ↑R⁰ ≠ ∅
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module.Finite R M<VAR>hM : Module.IsTorsion R M<VAR>S : Finset M<VAR>hS : span R ↑S = ⊤<GOAL>↑(∏ x ∈ S, ⋯.choose) ∈ ↑⊤.annihilator
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module.Finite R M<VAR>hM : Module.IsTorsion R M<VAR>S : Finset M<VAR>hS : span R ↑S = ⊤<GOAL>∀ (n : ↑↑S), (∏ i ∈ S, ↑⋯.choose) • ↑n = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module.Finite R M<VAR>hM : Module.IsTorsion R M<VAR>S : Finset M<VAR>hS : span R ↑S = ⊤<VAR>n : ↑↑S<VAR>this : DecidableEq M := Classical.decEq M<GOAL>(∏ i ∈ S, ↑⋯.choose) • ↑n = 0
<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 ⟶ G.obj Y<GOAL>f ≫ α.inv.app Y = f' ≫ α.inv.app Y ↔ f = f'
<VAR>𝕜 : Type u_1<VAR>inst✝²⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝²³ : NormedAddCommGroup E<VAR>inst✝²² : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝²¹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝²⁰ : TopologicalSpace M<VAR>inst✝¹⁹ : ChartedSpace H M<VAR>Is : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹⁸ : NormedAddCommGroup E'<VAR>inst✝¹⁷ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁶ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝¹⁵ : TopologicalSpace M'<VAR>inst✝¹⁴ : ChartedSpace H' M'<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N<VAR>inst✝⁹ : ChartedSpace G N<VAR>Js : SmoothManifoldWithCorners J N<VAR>F' : Type u_11<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝⁶ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝⁵ : TopologicalSpace N'<VAR>inst✝⁴ : ChartedSpace G' N'<VAR>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f✝ f₁ : M → M'<VAR>s✝ s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>f : H → H'<VAR>s : Set H<VAR>hf : ContMDiffOn I I' n f s<VAR>hn : 1 ≤ n<VAR>hs : UniqueMDiffOn I s<GOAL>ContinuousOn (fun p => (f p.1, (fderivWithin 𝕜 (writtenInExtChartAt I I' p.1 f) (↑I.symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I p.1) p.1)) p.2)) (Prod.fst ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>inst✝²⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝²³ : NormedAddCommGroup E<VAR>inst✝²² : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝²¹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝²⁰ : TopologicalSpace M<VAR>inst✝¹⁹ : ChartedSpace H M<VAR>Is : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹⁸ : NormedAddCommGroup E'<VAR>inst✝¹⁷ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁶ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝¹⁵ : TopologicalSpace M'<VAR>inst✝¹⁴ : ChartedSpace H' M'<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N<VAR>inst✝⁹ : ChartedSpace G N<VAR>Js : SmoothManifoldWithCorners J N<VAR>F' : Type u_11<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝⁶ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝⁵ : TopologicalSpace N'<VAR>inst✝⁴ : ChartedSpace G' N'<VAR>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f✝ f₁ : M → M'<VAR>s✝ s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>f : H → H'<VAR>s : Set H<VAR>hf : ContMDiffOn I I' n f s<VAR>hn : 1 ≤ n<VAR>hs : UniqueMDiffOn I s<GOAL>ContinuousOn (fun p => (fderivWithin 𝕜 (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I p.1)) p.2) (Prod.fst ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>inst✝²⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝²³ : NormedAddCommGroup E<VAR>inst✝²² : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝²¹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝²⁰ : TopologicalSpace M<VAR>inst✝¹⁹ : ChartedSpace H M<VAR>Is : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹⁸ : NormedAddCommGroup E'<VAR>inst✝¹⁷ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁶ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝¹⁵ : TopologicalSpace M'<VAR>inst✝¹⁴ : ChartedSpace H' M'<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N<VAR>inst✝⁹ : ChartedSpace G N<VAR>Js : SmoothManifoldWithCorners J N<VAR>F' : Type u_11<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝⁶ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝⁵ : TopologicalSpace N'<VAR>inst✝⁴ : ChartedSpace G' N'<VAR>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f✝ f₁ : M → M'<VAR>s✝ s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>f : H → H'<VAR>s : Set H<VAR>hf : ContMDiffOn I I' n f s<VAR>hn : 1 ≤ n<VAR>hs : UniqueMDiffOn I s<GOAL>ContinuousOn (fderivWithin 𝕜 (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I)) (↑I '' s)