ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>G'' : Type u_7<VAR>G' : Type u_8<VAR>inst✝³ : NormedLatticeAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : NormedLatticeAddCommGroup G''<VAR>inst✝ : NormedSpace ℝ G''<VAR>T : Set α → G'' →L[ℝ] G'<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : FinMeasAdditive μ T<VAR>hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G''), 0 ≤ x → 0 ≤ (T s) x<VAR>f : ↥(simpleFunc G'' 1 μ)<VAR>hf : 0 ≤ f<GOAL>0 ≤ SimpleFunc.setToSimpleFunc T (toSimpleFunc f)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>G'' : Type u_7<VAR>G' : Type u_8<VAR>inst✝³ : NormedLatticeAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : NormedLatticeAddCommGroup G''<VAR>inst✝ : NormedSpace ℝ G''<VAR>T : Set α → G'' →L[ℝ] G'<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : FinMeasAdditive μ T<VAR>hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G''), 0 ≤ x → 0 ≤ (T s) x<VAR>f : ↥(simpleFunc G'' 1 μ)<VAR>hf : 0 ≤ f<VAR>f' : α →ₛ G''<VAR>hf' : 0 ≤ f'<VAR>hff' : ↑(toSimpleFunc f) =ᶠ[ae μ] ↑f'<GOAL>0 ≤ SimpleFunc.setToSimpleFunc T (toSimpleFunc f)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>G'' : Type u_7<VAR>G' : Type u_8<VAR>inst✝³ : NormedLatticeAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : NormedLatticeAddCommGroup G''<VAR>inst✝ : NormedSpace ℝ G''<VAR>T : Set α → G'' →L[ℝ] G'<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : FinMeasAdditive μ T<VAR>hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G''), 0 ≤ x → 0 ≤ (T s) x<VAR>f : ↥(simpleFunc G'' 1 μ)<VAR>hf : 0 ≤ f<VAR>f' : α →ₛ G''<VAR>hf' : 0 ≤ f'<VAR>hff' : ↑(toSimpleFunc f) =ᶠ[ae μ] ↑f'<GOAL>0 ≤ SimpleFunc.setToSimpleFunc T f'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : α → M<VAR>s : Set α<GOAL>∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f), f i = ∏ᶠ (i : α) (_ : i ∈ s), f i
<VAR>ι : Type u_1<VAR>C : Type u<VAR>inst✝¹² : Category.{v, u} C<VAR>inst✝¹¹ : HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K✝ L✝ M K' L' : HomologicalComplex C c<VAR>C₁ : Type u_2<VAR>C₂ : Type u_3<VAR>inst✝¹⁰ : Category.{u_4, u_2} C₁<VAR>inst✝⁹ : Category.{u_5, u_3} C₂<VAR>inst✝⁸ : Preadditive C₁<VAR>inst✝⁷ : Preadditive C₂<VAR>K L : HomologicalComplex C₁ c<VAR>φ : K ⟶ L<VAR>F : C₁ ⥤ C₂<VAR>inst✝⁶ : F.Additive<VAR>inst✝⁵ : F.PreservesHomology<VAR>i : ι<VAR>inst✝⁴ : K.HasHomology i<VAR>inst✝³ : L.HasHomology i<VAR>inst✝² : ((F.mapHomologicalComplex c).obj K).HasHomology i<VAR>inst✝¹ : ((F.mapHomologicalComplex c).obj L).HasHomology i<VAR>inst✝ : F.ReflectsIsomorphisms<GOAL>QuasiIsoAt ((F.mapHomologicalComplex c).map φ) i ↔ QuasiIsoAt φ i
<VAR>ι : Type u_1<VAR>C : Type u<VAR>inst✝¹² : Category.{v, u} C<VAR>inst✝¹¹ : HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K✝ L✝ M K' L' : HomologicalComplex C c<VAR>C₁ : Type u_2<VAR>C₂ : Type u_3<VAR>inst✝¹⁰ : Category.{u_4, u_2} C₁<VAR>inst✝⁹ : Category.{u_5, u_3} C₂<VAR>inst✝⁸ : Preadditive C₁<VAR>inst✝⁷ : Preadditive C₂<VAR>K L : HomologicalComplex C₁ c<VAR>φ : K ⟶ L<VAR>F : C₁ ⥤ C₂<VAR>inst✝⁶ : F.Additive<VAR>inst✝⁵ : F.PreservesHomology<VAR>i : ι<VAR>inst✝⁴ : K.HasHomology i<VAR>inst✝³ : L.HasHomology i<VAR>inst✝² : ((F.mapHomologicalComplex c).obj K).HasHomology i<VAR>inst✝¹ : ((F.mapHomologicalComplex c).obj L).HasHomology i<VAR>inst✝ : F.ReflectsIsomorphisms<GOAL>ShortComplex.QuasiIso ((shortComplexFunctor C₂ c i).map ((F.mapHomologicalComplex c).map φ)) ↔ ShortComplex.QuasiIso ((shortComplexFunctor C₁ c i).map φ)
<VAR>J : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>F✝ F : J ⥤ C<VAR>inst✝¹ : HasLimit F<VAR>G : K ⥤ C<VAR>inst✝ : HasLimit G<VAR>e : J ≌ K<VAR>w : e.functor ⋙ G ≅ F<VAR>j : J<GOAL>(isoOfEquivalence e w).inv ≫ limit.π F j = limit.π G (e.functor.obj j) ≫ w.hom.app j
<VAR>J : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>F✝ F : J ⥤ C<VAR>inst✝¹ : HasLimit F<VAR>G : K ⥤ C<VAR>inst✝ : HasLimit G<VAR>e : J ≌ K<VAR>w : e.functor ⋙ G ≅ F<VAR>j : J<GOAL>((limit.isLimit F).conePointsIsoOfEquivalence (limit.isLimit G) e w).inv ≫ limit.π F j = limit.π G (e.functor.obj j) ≫ w.hom.app j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ζ : Type u_6<VAR>r : α → β → Prop<VAR>p : β → γ → Prop<VAR>q : γ → δ → Prop<GOAL>(r ∘r p) ∘r q = r ∘r p ∘r q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ζ : Type u_6<VAR>r : α → β → Prop<VAR>p : β → γ → Prop<VAR>q : γ → δ → Prop<VAR>a : α<VAR>d : δ<GOAL>((r ∘r p) ∘r q) a d = (r ∘r p ∘r q) a d
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_6, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_5, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.45377, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.45429, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ Type v<VAR>ℱ' : SheafOfTypes K<VAR>α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X : D<VAR>x : ℱ.obj (op X)<VAR>Y : C<VAR>f : G.obj Y ⟶ X<GOAL>pushforwardFamily α x f ⋯ = α.app (op Y) (ℱ.map f.op x)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_6, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_5, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.45377, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.45429, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ Type v<VAR>ℱ' : SheafOfTypes K<VAR>α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X : D<VAR>x : ℱ.obj (op X)<VAR>Y : C<VAR>f : G.obj Y ⟶ X<GOAL>ℱ'.val.map (Nonempty.some ⋯).lift.op (α.app (op (Nonempty.some ⋯).1) (ℱ.map (Nonempty.some ⋯).map.op x)) = α.app (op Y) (ℱ.map f.op x)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_6, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_5, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.45377, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.45429, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ Type v<VAR>ℱ' : SheafOfTypes K<VAR>α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X : D<VAR>x : ℱ.obj (op X)<VAR>Y : C<VAR>f : G.obj Y ⟶ X<VAR>l : CoverByImageStructure G f<GOAL>ℱ'.val.map l.lift.op (α.app (op l.1) (ℱ.map l.map.op x)) = α.app (op Y) (ℱ.map f.op x)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_6, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_5, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.45377, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.45429, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ Type v<VAR>ℱ' : SheafOfTypes K<VAR>α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X : D<VAR>x : ℱ.obj (op X)<VAR>Y W : C<VAR>iYW : G.obj Y ⟶ G.obj W<VAR>iWX : G.obj W ⟶ X<GOAL>ℱ'.val.map { obj := W, lift := iYW, map := iWX, fac := ⋯ }.lift.op (α.app (op { obj := W, lift := iYW, map := iWX, fac := ⋯ }.1) (ℱ.map { obj := W, lift := iYW, map := iWX, fac := ⋯ }.map.op x)) = α.app (op Y) (ℱ.map (iYW ≫ iWX).op x)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M✝ : Matroid α<VAR>F X✝ Y : Set α<VAR>e : α<VAR>M : Matroid α<VAR>X : Set α<GOAL>X ∩ M.E ⊆ M.closure X
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M✝ : Matroid α<VAR>F X✝ Y : Set α<VAR>e : α<VAR>M : Matroid α<VAR>X : Set α<GOAL>∀ t' ∈ {F | M.Flat F ∧ X ∩ M.E ⊆ F}, X ∩ M.E ⊆ t'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>t : TopologicalSpace γ<VAR>inst✝ : CompactSpace γ<VAR>u u' : UniformSpace γ<VAR>h : toTopologicalSpace = t<VAR>h' : toTopologicalSpace = t<GOAL>u = u'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>t : TopologicalSpace γ<VAR>inst✝ : CompactSpace γ<VAR>u u' : UniformSpace γ<VAR>h : toTopologicalSpace = t<VAR>h' : toTopologicalSpace = t<GOAL>𝓤 γ = 𝓤 γ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>t : TopologicalSpace γ<VAR>inst✝ : CompactSpace γ<VAR>u u' : UniformSpace γ<VAR>h : toTopologicalSpace = t<VAR>h' : toTopologicalSpace = t<VAR>this✝ : CompactSpace γ<VAR>this : CompactSpace γ<GOAL>𝓤 γ = 𝓤 γ
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝¹⁰ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁹ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁸ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>E : Type u_9<VAR>inst✝⁵ : AddCommMonoid E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_10<VAR>inst✝³ : AddCommMonoid F<VAR>t : ι → Type u_11<VAR>inst✝² : (i : ι) → AddCommMonoid (t i)<VAR>inst✝¹ : (i : ι) → Module R (t i)<VAR>inst✝ : Subsingleton ι<VAR>i₀ : ι<VAR>x : ⨂[R] (x : ι), M<GOAL>((tprod R) fun x_1 => (lift ((ofSubsingleton R M M i₀) LinearMap.id)) x) = x
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝¹⁰ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁹ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁸ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>E : Type u_9<VAR>inst✝⁵ : AddCommMonoid E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_10<VAR>inst✝³ : AddCommMonoid F<VAR>t : ι → Type u_11<VAR>inst✝² : (i : ι) → AddCommMonoid (t i)<VAR>inst✝¹ : (i : ι) → Module R (t i)<VAR>inst✝ : Subsingleton ι<VAR>i₀ : ι<VAR>x : ⨂[R] (x : ι), M<VAR>this : ∀ (f : ι → M) (z : M), (fun x => z) = update f i₀ z<GOAL>((tprod R) fun x_1 => (lift ((ofSubsingleton R M M i₀) LinearMap.id)) x) = x
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝¹⁰ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁹ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁸ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>E : Type u_9<VAR>inst✝⁵ : AddCommMonoid E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_10<VAR>inst✝³ : AddCommMonoid F<VAR>t : ι → Type u_11<VAR>inst✝² : (i : ι) → AddCommMonoid (t i)<VAR>inst✝¹ : (i : ι) → Module R (t i)<VAR>inst✝ : Subsingleton ι<VAR>i₀ : ι<VAR>x : ⨂[R] (x : ι), M<VAR>this : ∀ (f : ι → M) (z : M), (fun x => z) = update f i₀ z<GOAL>∀ (r : R) (f : ι → M), ((tprod R) fun x => (lift ((ofSubsingleton R M M i₀) LinearMap.id)) (r • (tprod R) f)) = r • (tprod R) f
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝¹⁰ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁹ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁸ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>E : Type u_9<VAR>inst✝⁵ : AddCommMonoid E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_10<VAR>inst✝³ : AddCommMonoid F<VAR>t : ι → Type u_11<VAR>inst✝² : (i : ι) → AddCommMonoid (t i)<VAR>inst✝¹ : (i : ι) → Module R (t i)<VAR>inst✝ : Subsingleton ι<VAR>i₀ : ι<VAR>x : ⨂[R] (x : ι), M<VAR>this : ∀ (f : ι → M) (z : M), (fun x => z) = update f i₀ z<GOAL>∀ (x y : ⨂[R] (i : ι), M), ((tprod R) fun x_1 => (lift ((ofSubsingleton R M M i₀) LinearMap.id)) x) = x → ((tprod R) fun x => (lift ((ofSubsingleton R M M i₀) LinearMap.id)) y) = y → ((tprod R) fun x_1 => (lift ((ofSubsingleton R M M i₀) LinearMap.id)) (x + y)) = x + y
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝¹⁰ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁹ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁸ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>E : Type u_9<VAR>inst✝⁵ : AddCommMonoid E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_10<VAR>inst✝³ : AddCommMonoid F<VAR>t✝ : ι → Type u_11<VAR>inst✝² : (i : ι) → AddCommMonoid (t✝ i)<VAR>inst✝¹ : (i : ι) → Module R (t✝ i)<VAR>inst✝ : Subsingleton ι<VAR>i₀ : ι<VAR>t : M<GOAL>{ toFun := ⇑(lift ((ofSubsingleton R M M i₀) LinearMap.id)), map_add' := ⋯, map_smul' := ⋯ }.toFun ((fun m => (tprod R) fun x => m) t) = t
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝¹⁰ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁹ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁸ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>E : Type u_9<VAR>inst✝⁵ : AddCommMonoid E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_10<VAR>inst✝³ : AddCommMonoid F<VAR>t : ι → Type u_11<VAR>inst✝² : (i : ι) → AddCommMonoid (t i)<VAR>inst✝¹ : (i : ι) → Module R (t i)<VAR>inst✝ : Subsingleton ι<VAR>i₀ : ι<VAR>r : R<VAR>x : ⨂[R] (x : ι), M<GOAL>(lift ((ofSubsingleton R M M i₀) LinearMap.id)) (r • x) = (RingHom.id R) r • (lift ((ofSubsingleton R M M i₀) LinearMap.id)) x
<VAR>α : Type u_1<VAR>p q : α → Bool<VAR>l : List α<VAR>h : ∀ (x : α), x ∈ l → p x = true → q x = true<GOAL>countP p l ≤ countP q l
<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 : Filter 𝕜<GOAL>fderiv 𝕜 (fun x => x⁻¹) x = smulRight 1 (-(x ^ 2)⁻¹)
<VAR>a b m n✝ p n k : ℕ<VAR>ih : (n ^ k).factorization = k • n.factorization<GOAL>(n ^ (k + 1)).factorization = (k + 1) • n.factorization
<VAR>a b m n p k : ℕ<VAR>ih : (0 ^ k).factorization = k • factorization 0<GOAL>(0 ^ (k + 1)).factorization = (k + 1) • factorization 0
<VAR>a b m n✝ p n k : ℕ<VAR>ih : (n ^ k).factorization = k • n.factorization<VAR>hn : n ≠ 0<GOAL>(n ^ (k + 1)).factorization = (k + 1) • n.factorization
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ l₃ : List α<VAR>a b : α<VAR>m✝ n✝ : ℕ<VAR>l : List α<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>drop n l <+ drop m l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ l₃ : List α<VAR>a b : α<VAR>m✝ n✝ : ℕ<VAR>l : List α<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>drop (n - m) (drop m l) <+ drop m l
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>W : MorphismProperty C<VAR>J : Type u_1<VAR>inst✝¹ : W.RespectsIso<VAR>inst✝ : HasProductsOfShape J C<VAR>hW : ∀ (X₁ X₂ : J → C) (f : (j : J) → X₁ j ⟶ X₂ j), (∀ (j : J), W (f j)) → W (Pi.map f)<VAR>X₁ X₂ : Discrete J ⥤ C<VAR>c₁ : Cone X₁<VAR>c₂ : Cone X₂<VAR>hc₁ : IsLimit c₁<VAR>hc₂ : IsLimit c₂<VAR>f : X₁ ⟶ X₂<VAR>hf : W.functorCategory (Discrete J) f<VAR>φ : (j : J) → X₁.obj { as := j } ⟶ X₂.obj { as := j } := fun j => f.app { as := j }<VAR>hf' : W (Pi.map φ)<GOAL>W (hc₂.lift { pt := c₁.pt, π := c₁.π ≫ f })
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>W : MorphismProperty C<VAR>J : Type u_1<VAR>inst✝¹ : W.RespectsIso<VAR>inst✝ : HasProductsOfShape J C<VAR>hW : ∀ (X₁ X₂ : J → C) (f : (j : J) → X₁ j ⟶ X₂ j), (∀ (j : J), W (f j)) → W (Pi.map f)<VAR>X₁ X₂ : Discrete J ⥤ C<VAR>c₁ : Cone X₁<VAR>c₂ : Cone X₂<VAR>hc₁ : IsLimit c₁<VAR>hc₂ : IsLimit c₂<VAR>f : X₁ ⟶ X₂<VAR>hf : W.functorCategory (Discrete J) f<VAR>φ : (j : J) → X₁.obj { as := j } ⟶ X₂.obj { as := j } := fun j => f.app { as := j }<VAR>hf' : W (Pi.map φ)<GOAL>Arrow.mk (hc₂.lift { pt := c₁.pt, π := c₁.π ≫ f }) ≅ Arrow.mk (Pi.map φ)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>W : MorphismProperty C<VAR>J : Type u_1<VAR>inst✝¹ : W.RespectsIso<VAR>inst✝ : HasProductsOfShape J C<VAR>hW : ∀ (X₁ X₂ : J → C) (f : (j : J) → X₁ j ⟶ X₂ j), (∀ (j : J), W (f j)) → W (Pi.map f)<VAR>X₁ X₂ : Discrete J ⥤ C<VAR>c₁ : Cone X₁<VAR>c₂ : Cone X₂<VAR>hc₁ : IsLimit c₁<VAR>hc₂ : IsLimit c₂<VAR>f : X₁ ⟶ X₂<VAR>hf : W.functorCategory (Discrete J) f<VAR>φ : (j : J) → X₁.obj { as := j } ⟶ X₂.obj { as := j } := fun j => f.app { as := j }<VAR>hf' : W (Pi.map φ)<GOAL>(hc₁.conePointUniqueUpToIso (limit.isLimit X₁) ≪≫ (Pi.isoLimit X₁).symm).hom ≫ (Arrow.mk (Pi.map φ)).hom = (Arrow.mk (hc₂.lift { pt := c₁.pt, π := c₁.π ≫ f })).hom ≫ (hc₂.conePointUniqueUpToIso (limit.isLimit X₂) ≪≫ (Pi.isoLimit X₂).symm).hom
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>W : MorphismProperty C<VAR>J : Type u_1<VAR>inst✝¹ : W.RespectsIso<VAR>inst✝ : HasProductsOfShape J C<VAR>hW : ∀ (X₁ X₂ : J → C) (f : (j : J) → X₁ j ⟶ X₂ j), (∀ (j : J), W (f j)) → W (Pi.map f)<VAR>X₁ X₂ : Discrete J ⥤ C<VAR>c₁ : Cone X₁<VAR>c₂ : Cone X₂<VAR>hc₁ : IsLimit c₁<VAR>hc₂ : IsLimit c₂<VAR>f : X₁ ⟶ X₂<VAR>hf : W.functorCategory (Discrete J) f<VAR>φ : (j : J) → X₁.obj { as := j } ⟶ X₂.obj { as := j } := fun j => f.app { as := j }<VAR>hf' : W (Pi.map φ)<GOAL>∀ (j : Discrete J), ((hc₁.conePointUniqueUpToIso (limit.isLimit X₁) ≪≫ (Pi.isoLimit X₁).symm).hom ≫ (Arrow.mk (Pi.map φ)).hom) ≫ limit.π (Discrete.functor fun j => X₂.obj { as := j }) j = ((Arrow.mk (hc₂.lift { pt := c₁.pt, π := c₁.π ≫ f })).hom ≫ (hc₂.conePointUniqueUpToIso (limit.isLimit X₂) ≪≫ (Pi.isoLimit X₂).symm).hom) ≫ limit.π (Discrete.functor fun j => X₂.obj { as := j }) j
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s k : Set α<VAR>hs : μ.IsEverywherePos s<VAR>c : ℝ≥0∞<VAR>hc : c ≠ 0<VAR>x : α<VAR>hx : x ∈ s<VAR>n : Set α<VAR>hn : n ∈ 𝓝[s] x<GOAL>0 < (c • μ) n
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i k₀ : ι<VAR>hk₀ : ∀ (l : ι), ¬c.Rel k₀ l<VAR>hk₀' : ∀ (l : ι), ¬c.Rel l k₀<VAR>hom : (i j : ι) → C.X i ⟶ D.X j<GOAL>C.d k₀ (c.next k₀) ≫ hom (c.next k₀) k₀ + hom k₀ (c.prev k₀) ≫ D.d (c.prev k₀) k₀ = 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>hρ : ρ ≪ μ<VAR>p q : ℝ≥0<VAR>hpq : p < q<VAR>s : Set α := {x | ∃ c, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 c)}<VAR>o : ℕ → Set α := spanningSets (ρ + μ)<VAR>u : ℕ → Set α := fun n => s ∩ {x | v.limRatio ρ x < ↑p} ∩ o n<VAR>w : ℕ → Set α := fun n => s ∩ {x | ↑q < v.limRatio ρ x} ∩ o n<VAR>m n : ℕ<GOAL>μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 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>hρ : ρ ≪ μ<VAR>p q : ℝ≥0<VAR>hpq : p < q<VAR>s : Set α := {x | ∃ c, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 c)}<VAR>o : ℕ → Set α := spanningSets (ρ + μ)<VAR>u : ℕ → Set α := fun n => s ∩ {x | v.limRatio ρ x < ↑p} ∩ o n<VAR>w : ℕ → Set α := fun n => s ∩ {x | ↑q < v.limRatio ρ x} ∩ o n<VAR>m n : ℕ<VAR>I : (ρ + μ) (u m) ≠ ⊤<GOAL>μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 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>hρ : ρ ≪ μ<VAR>p q : ℝ≥0<VAR>hpq : p < q<VAR>s : Set α := {x | ∃ c, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 c)}<VAR>o : ℕ → Set α := spanningSets (ρ + μ)<VAR>u : ℕ → Set α := fun n => s ∩ {x | v.limRatio ρ x < ↑p} ∩ o n<VAR>w : ℕ → Set α := fun n => s ∩ {x | ↑q < v.limRatio ρ x} ∩ o n<VAR>m n : ℕ<VAR>I : (ρ + μ) (u m) ≠ ⊤<VAR>J : (ρ + μ) (w n) ≠ ⊤<GOAL>μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 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>hρ : ρ ≪ μ<VAR>p q : ℝ≥0<VAR>hpq : p < q<VAR>s : Set α := {x | ∃ c, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 c)}<VAR>o : ℕ → Set α := spanningSets (ρ + μ)<VAR>u : ℕ → Set α := fun n => s ∩ {x | v.limRatio ρ x < ↑p} ∩ o n<VAR>w : ℕ → Set α := fun n => s ∩ {x | ↑q < v.limRatio ρ x} ∩ o n<VAR>m n : ℕ<VAR>I : (ρ + μ) (u m) ≠ ⊤<VAR>J : (ρ + μ) (w n) ≠ ⊤<VAR>A : ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤ ↑p * μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))<GOAL>μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 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>hρ : ρ ≪ μ<VAR>p q : ℝ≥0<VAR>hpq : p < q<VAR>s : Set α := {x | ∃ c, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 c)}<VAR>o : ℕ → Set α := spanningSets (ρ + μ)<VAR>u : ℕ → Set α := fun n => s ∩ {x | v.limRatio ρ x < ↑p} ∩ o n<VAR>w : ℕ → Set α := fun n => s ∩ {x | ↑q < v.limRatio ρ x} ∩ o n<VAR>m n : ℕ<VAR>I : (ρ + μ) (u m) ≠ ⊤<VAR>J : (ρ + μ) (w n) ≠ ⊤<VAR>A : ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤ ↑p * μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))<VAR>B : ↑q * μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤ ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))<GOAL>μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 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>hρ : ρ ≪ μ<VAR>p q : ℝ≥0<VAR>hpq : p < q<VAR>s : Set α := {x | ∃ c, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 c)}<VAR>o : ℕ → Set α := spanningSets (ρ + μ)<VAR>u : ℕ → Set α := fun n => s ∩ {x | v.limRatio ρ x < ↑p} ∩ o n<VAR>w : ℕ → Set α := fun n => s ∩ {x | ↑q < v.limRatio ρ x} ∩ o n<VAR>m n : ℕ<VAR>I : (ρ + μ) (u m) ≠ ⊤<VAR>J : (ρ + μ) (w n) ≠ ⊤<VAR>A : ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤ ↑p * μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))<VAR>B : ↑q * μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤ ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))<VAR>h : ¬μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0<GOAL>False