ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝⁵ : AddCommSemigroup α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>h : c ≤ b<GOAL>a - c - (b - c) = a - b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>ht : t.Finite<VAR>hst : s ⊆ t<VAR>hts : t.encard ≤ s.encard<GOAL>s = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>ht : t.Finite<VAR>hst : s ⊆ t<VAR>hts : (t \ s).encard + s.encard ≤ 0 + s.encard<GOAL>s = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>ht : t.Finite<VAR>hst : s ⊆ t<VAR>hts : (t \ s).encard + s.encard ≤ 0 + s.encard<VAR>hdiff : (t \ s).encard ≤ 0<GOAL>s = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>ht : t.Finite<VAR>hst : s ⊆ t<VAR>hts : (t \ s).encard + s.encard ≤ 0 + s.encard<VAR>hdiff : t ⊆ s<GOAL>s = t
<VAR>α : Type u<VAR>inst✝³ : DecidableEq α<VAR>β : Type v<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Fintype β<VAR>σ : α → Perm β<GOAL>sign (prodCongrLeft σ) = ∏ k : α, sign (σ k)
<VAR>α : Type u<VAR>inst✝³ : DecidableEq α<VAR>β : Type v<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Fintype β<VAR>σ : α → Perm β<GOAL>∀ (x : β × α), (prodComm β α) ((prodCongrLeft σ) x) = (prodCongrRight σ) ((prodComm β α) x)
<VAR>K : Type u<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>x : K[X]<VAR>hx : x = 0<GOAL>(algebraMap K[X] (RatFunc K)) x = 0
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>inst✝² : Category.{v₂, v₁} I<VAR>F : I ⥤ C<VAR>inst✝¹ : HasColimit F<VAR>inst✝ : HasLimitsOfShape Iᵒᵖ (Type u₂)<VAR>A : C<VAR>i : I<GOAL>(colimitHomIsoLimitYoneda F A).hom ≫ limit.π (F.op ⋙ yoneda.obj A) (op i) = (coyoneda.map (colimit.ι F i).op).app A
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>inst✝² : Category.{v₂, v₁} I<VAR>F : I ⥤ C<VAR>inst✝¹ : HasColimit F<VAR>inst✝ : HasLimitsOfShape Iᵒᵖ (Type u₂)<VAR>A : C<VAR>i : I<GOAL>(coyonedaOpColimitIsoLimitCoyoneda F).hom.app A ≫ (limitObjIsoLimitCompEvaluation (F.op ⋙ coyoneda) A).hom ≫ limit.π (F.op ⋙ yoneda.obj A) (op i) = (coyoneda.map (colimit.ι F i).op).app A
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>inst✝² : Category.{v₂, v₁} I<VAR>F : I ⥤ C<VAR>inst✝¹ : HasColimit F<VAR>inst✝ : HasLimitsOfShape Iᵒᵖ (Type u₂)<VAR>A : C<VAR>i : I<GOAL>(coyonedaOpColimitIsoLimitCoyoneda F).hom.app A ≫ (limit.π (F.op ⋙ coyoneda) (op i)).app A = (coyoneda.map (colimit.ι F i).op).app A
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>inst✝² : Category.{v₂, v₁} I<VAR>F : I ⥤ C<VAR>inst✝¹ : HasColimit F<VAR>inst✝ : HasLimitsOfShape Iᵒᵖ (Type u₂)<VAR>A : C<VAR>i : I<GOAL>((coyonedaOpColimitIsoLimitCoyoneda F).hom ≫ limit.π (F.op ⋙ coyoneda) (op i)).app A = (coyoneda.map (colimit.ι F i).op).app A
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>f✝ : E → F<VAR>φ : E → ℝ<VAR>x₀ : E<VAR>f'✝ : E →L[ℝ] F<VAR>φ' : E →L[ℝ] ℝ<VAR>ι : Type u_3<VAR>inst✝ : Finite ι<VAR>f : ι → E → ℝ<VAR>f' : ι → E →L[ℝ] ℝ<VAR>hextr : IsLocalExtrOn φ {x | ∀ (i : ι), f i x = f i x₀} x₀<VAR>hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀<VAR>hφ' : HasStrictFDerivAt φ φ' x₀<GOAL>¬LinearIndependent ℝ (Option.elim' φ' f')
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>f✝ : E → F<VAR>φ : E → ℝ<VAR>x₀ : E<VAR>f'✝ : E →L[ℝ] F<VAR>φ' : E →L[ℝ] ℝ<VAR>ι : Type u_3<VAR>inst✝ : Finite ι<VAR>f : ι → E → ℝ<VAR>f' : ι → E →L[ℝ] ℝ<VAR>hextr : IsLocalExtrOn φ {x | ∀ (i : ι), f i x = f i x₀} x₀<VAR>hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀<VAR>hφ' : HasStrictFDerivAt φ φ' x₀<VAR>val✝ : Fintype ι<GOAL>¬LinearIndependent ℝ (Option.elim' φ' f')
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>f✝ : E → F<VAR>φ : E → ℝ<VAR>x₀ : E<VAR>f'✝ : E →L[ℝ] F<VAR>φ' : E →L[ℝ] ℝ<VAR>ι : Type u_3<VAR>inst✝ : Finite ι<VAR>f : ι → E → ℝ<VAR>f' : ι → E →L[ℝ] ℝ<VAR>hextr : IsLocalExtrOn φ {x | ∀ (i : ι), f i x = f i x₀} x₀<VAR>hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀<VAR>hφ' : HasStrictFDerivAt φ φ' x₀<VAR>val✝ : Fintype ι<GOAL>¬∀ (g : Option ι → ℝ), ∑ i : Option ι, g i • Option.elim' φ' f' i = 0 → ∀ (i : Option ι), g i = 0
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>f✝ : E → F<VAR>φ : E → ℝ<VAR>x₀ : E<VAR>f'✝ : E →L[ℝ] F<VAR>φ' : E →L[ℝ] ℝ<VAR>ι : Type u_3<VAR>inst✝ : Finite ι<VAR>f : ι → E → ℝ<VAR>f' : ι → E →L[ℝ] ℝ<VAR>hextr : IsLocalExtrOn φ {x | ∀ (i : ι), f i x = f i x₀} x₀<VAR>hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀<VAR>hφ' : HasStrictFDerivAt φ φ' x₀<VAR>val✝ : Fintype ι<GOAL>∃ g, ∑ i : Option ι, g i • Option.elim' φ' f' i = 0 ∧ ∃ i, g i ≠ 0
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>f✝ : E → F<VAR>φ : E → ℝ<VAR>x₀ : E<VAR>f'✝ : E →L[ℝ] F<VAR>φ' : E →L[ℝ] ℝ<VAR>ι : Type u_3<VAR>inst✝ : Finite ι<VAR>f : ι → E → ℝ<VAR>f' : ι → E →L[ℝ] ℝ<VAR>hextr : IsLocalExtrOn φ {x | ∀ (i : ι), f i x = f i x₀} x₀<VAR>hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀<VAR>hφ' : HasStrictFDerivAt φ φ' x₀<VAR>val✝ : Fintype ι<VAR>Λ : ι → ℝ<VAR>Λ₀ : ℝ<VAR>hΛ : (Λ, Λ₀) ≠ 0<VAR>hΛf : ∑ i : ι, Λ i • f' i + Λ₀ • φ' = 0<GOAL>∃ g, ∑ i : Option ι, g i • Option.elim' φ' f' i = 0 ∧ ∃ i, g i ≠ 0
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>I : Finset (Set α)<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>hI : ↑I ⊆ C<VAR>hI_ss : ∀ t ∈ I, t ⊆ s<GOAL>⋃₀ ↑I ∪ ⋃₀ ↑(hC.diffFinset₀ hs hI) = s
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>S : Set (Set X)<VAR>t : Set X<VAR>x : X<VAR>hS : RestrictGenTopology S<GOAL>IsClosed t ↔ ∀ s ∈ S, IsClosed (Subtype.val ⁻¹' t)
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>o : Ordinal.{u}<VAR>α : Type u<VAR>r : α → α → Prop<VAR>x✝ : IsWellOrder α r<VAR>z : (type r).cof = 1<GOAL>∃ a, type r = succ a
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>o : Ordinal.{u}<VAR>α : Type u<VAR>r : α → α → Prop<VAR>x✝ : IsWellOrder α r<VAR>z : (type r).cof = 1<VAR>S : Set α<VAR>hl : Unbounded r S<VAR>e : #↑S = (type r).cof<GOAL>∃ a, type r = succ a
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>o : Ordinal.{u}<VAR>α : Type u<VAR>r : α → α → Prop<VAR>x✝ : IsWellOrder α r<VAR>z : (type r).cof = 1<VAR>S : Set α<VAR>hl : Unbounded r S<VAR>e : #↑S = 1<GOAL>∃ a, type r = succ a
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>o : Ordinal.{u}<VAR>α : Type u<VAR>r : α → α → Prop<VAR>x✝ : IsWellOrder α r<VAR>z : (type r).cof = 1<VAR>S : Set α<VAR>hl : Unbounded r S<VAR>e : #↑S = 1<VAR>a : ↑S<GOAL>∃ a, type r = succ a
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>o : Ordinal.{u}<VAR>α : Type u<VAR>r : α → α → Prop<VAR>x✝ : IsWellOrder α r<VAR>z : (type r).cof = 1<VAR>S : Set α<VAR>hl : Unbounded r S<VAR>e : #↑S = 1<VAR>a : ↑S<GOAL>↑{b | r b ↑a} ⊕ PUnit.{u + 1} → α
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>o : Ordinal.{u}<VAR>α : Type u<VAR>r : α → α → Prop<VAR>x✝ : IsWellOrder α r<VAR>z : (type r).cof = 1<VAR>S : Set α<VAR>hl : Unbounded r S<VAR>e : #↑S = 1<VAR>a : ↑S<VAR>x y : ↑{b | r b ↑a} ⊕ PUnit.{u + 1}<GOAL>Sum.Lex (Subrel r {b | r b ↑a}) EmptyRelation x y → r (?intro.intro.intro.refine_1 x) (?intro.intro.intro.refine_1 y)
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>o : Ordinal.{u}<VAR>α : Type u<VAR>r : α → α → Prop<VAR>x✝ : IsWellOrder α r<VAR>z : (type r).cof = 1<VAR>S : Set α<VAR>hl : Unbounded r S<VAR>e : #↑S = 1<VAR>a : ↑S<VAR>x : α<GOAL>∃ a_1, (RelEmbedding.ofMonotone ?intro.intro.intro.refine_1 ⋯) a_1 = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Encodable α<VAR>a a✝ : α<GOAL>a✝ ∈ decode₂ α (encode a) ↔ a✝ ∈ some a
<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>μ : Measure ℝ<VAR>inst✝³ : IsLocallyFiniteMeasure μ<VAR>inst✝² : ConditionallyCompleteLinearOrder E<VAR>inst✝¹ : OrderTopology E<VAR>inst✝ : SecondCountableTopology E<VAR>u : ℝ → E<VAR>a b : ℝ<VAR>hu : MonotoneOn u [[a, b]]<GOAL>IntervalIntegrable u μ a b
<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>μ : Measure ℝ<VAR>inst✝³ : IsLocallyFiniteMeasure μ<VAR>inst✝² : ConditionallyCompleteLinearOrder E<VAR>inst✝¹ : OrderTopology E<VAR>inst✝ : SecondCountableTopology E<VAR>u : ℝ → E<VAR>a b : ℝ<VAR>hu : MonotoneOn u [[a, b]]<GOAL>IntegrableOn u (Ι a b) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : SMulCommClass ℝ 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace E<VAR>f : ↥(Lp ℝ 1 μ)<GOAL>integral f = ‖Lp.posPart f‖ - ‖Lp.negPart f‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : SMulCommClass ℝ 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace E<VAR>f : ↥(Lp ℝ 1 μ)<GOAL>Continuous integral
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : SMulCommClass ℝ 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace E<VAR>f : ↥(Lp ℝ 1 μ)<GOAL>Continuous fun x => ‖Lp.posPart x‖ - ‖Lp.negPart x‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : SMulCommClass ℝ 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace E<VAR>f : ↥(Lp ℝ 1 μ)<GOAL>∀ (a : { x // x ∈ ↑(simpleFunc ℝ 1 μ) }), (fun f => integral f = ‖Lp.posPart f‖ - ‖Lp.negPart f‖) ↑a
<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✝ : NormedRing A<VAR>f✝ g✝ : ℝ → E<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>f g : ℝ → A<VAR>hf : IntervalIntegrable f μ a b<VAR>hg : ContinuousOn g [[a, b]]<GOAL>IntervalIntegrable (fun x => f x * g x) μ a b
<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✝ : NormedRing A<VAR>f✝ g✝ : ℝ → E<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>f g : ℝ → A<VAR>hf : IntegrableOn f (Ι a b) μ<VAR>hg : ContinuousOn g [[a, b]]<GOAL>IntegrableOn (fun x => f x * g x) (Ι a b) μ
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>k : Type u_5<VAR>S : Type u_6<VAR>S₃ : Type u_7<VAR>T : Type u_8<VAR>M : Type u_9<VAR>M₁ : Type u_10<VAR>M₂ : Type u_11<VAR>M₃ : Type u_12<VAR>N₁ : Type u_13<VAR>N₂ : Type u_14<VAR>N₃ : Type u_15<VAR>ι : Type u_16<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : AddCommMonoid M₃<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : Module R M<VAR>inst✝² : Semiring S<VAR>inst✝¹ : Module S M₂<VAR>inst✝ : Module R M₃<VAR>σ : R →+* S<VAR>f g : M →ₑ+[↑σ] M₂<VAR>h : ↑f = ↑g<VAR>m : M<GOAL>f m = g m
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 →ᵃ[𝕜] E<VAR>a b : E<VAR>L : Filter 𝕜<VAR>s : Set 𝕜<VAR>x : 𝕜<GOAL>HasStrictDerivAt (⇑f) (f.linear 1) x
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 →ᵃ[𝕜] E<VAR>a b : E<VAR>L : Filter 𝕜<VAR>s : Set 𝕜<VAR>x : 𝕜<GOAL>HasStrictDerivAt (⇑f.linear + fun x => f 0) (f.linear 1) x
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : SMul M X<VAR>inst✝ : ContinuousSMul M X<VAR>f : Y → M<VAR>g : Y → X<VAR>b : Y<VAR>s : Set Y<VAR>k : Set M<VAR>u : Set X<VAR>hk : IsCompact k<VAR>hu : IsCompact u<GOAL>IsCompact (k • u)
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : SMul M X<VAR>inst✝ : ContinuousSMul M X<VAR>f : Y → M<VAR>g : Y → X<VAR>b : Y<VAR>s : Set Y<VAR>k : Set M<VAR>u : Set X<VAR>hk : IsCompact k<VAR>hu : IsCompact u<GOAL>IsCompact ((fun x => x.1 • x.2) '' k ×ˢ u)
<VAR>α : Type u<VAR>inst✝ : Semiring α<VAR>x : α<GOAL>∑ i ∈ range 2, x ^ i = x + 1
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup G<VAR>inst✝¹⁰ : NormedSpace 𝕜 G<VAR>R : Type u_5<VAR>𝕜₂ : Type u_6<VAR>𝕜' : Type u_7<VAR>inst✝⁹ : NontriviallyNormedField 𝕜'<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₂<VAR>M : Type u_8<VAR>inst✝⁷ : TopologicalSpace M<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>G' : Type u_9<VAR>inst✝⁶ : NormedAddCommGroup G'<VAR>inst✝⁵ : NormedSpace 𝕜₂ G'<VAR>inst✝⁴ : NormedSpace 𝕜' G'<VAR>inst✝³ : SMulCommClass 𝕜₂ 𝕜' G'<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>ρ₁₂ : R →+* 𝕜'<VAR>f : M →SL[ρ₁₂] F →SL[σ₁₂] G'<VAR>c : R<VAR>x : M<VAR>y : F<GOAL>(f (c • x)) y = ρ₁₂ c • (f x) y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>hi₂ : ¬restrict s i ≤ restrict 0 i<VAR>n : ℕ<VAR>hn : ¬restrict s (i \ ⋃ k, ⋃ (_ : k < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤ restrict 0 (i \ ⋃ k, ⋃ (_ : k < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)<GOAL>0 < ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i 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✝ : ι<VAR>h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)<VAR>i j : ι<VAR>hij : ¬c.Rel j i<GOAL>(dite (c.Rel j i) (h i j) fun x => 0) = 0
<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✝ : ι<VAR>h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)<VAR>i j : ι<VAR>hij : ¬c.Rel j i<GOAL>∀ (h_1 : c.Rel j i), h i j h_1 = 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>f : α → β<VAR>x : Filter α<VAR>y : ι → Filter β<GOAL>Tendsto f x (⨅ i, y i) ↔ ∀ (i : ι), Tendsto f x (y i)
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>f g : ℕ → R<GOAL>(∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, ↑(μ x.1) * g x.2 = f n
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>f g : ℕ → R<GOAL>(∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n) ↔ ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, ↑(μ x.1) * g x.2 = f n
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>f g : ℕ → R<GOAL>∀ (a : ℕ), a > 0 → ∑ x ∈ a.divisorsAntidiagonal, μ x.1 • g x.2 = f a ↔ a > 0 → ∑ x ∈ a.divisorsAntidiagonal, ↑(μ x.1) * g x.2 = f a
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>f g : ℕ → R<VAR>a : ℕ<VAR>x✝ : a > 0<VAR>x : ℕ × ℕ<VAR>_hx : x ∈ a.divisorsAntidiagonal<GOAL>μ x.1 • g x.2 = ↑(μ x.1) * g x.2
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>N : Type u_9<VAR>N₁ : Type u_10<VAR>N₂ : Type u_11<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : AddCommGroup N₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N₁<VAR>inst✝² : Monoid S<VAR>inst✝¹ : DistribMulAction S M<VAR>inst✝ : SMulCommClass R S M<VAR>f' : M →ₗ[R] M<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>h : Injective ⇑(f' ^ n)<GOAL>Injective ⇑f'
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>N : Type u_9<VAR>N₁ : Type u_10<VAR>N₂ : Type u_11<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : AddCommGroup N₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N₁<VAR>inst✝² : Monoid S<VAR>inst✝¹ : DistribMulAction S M<VAR>inst✝ : SMulCommClass R S M<VAR>f' : M →ₗ[R] M<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>h : Injective (⇑(f' ^ n.pred) ∘ ⇑f')<GOAL>Injective ⇑f'
<VAR>n m : ℕ<GOAL>n ^^^ m = 0 ↔ n = m
<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<GOAL>∃ t, t.Countable ∧ (∀ p ∈ t, p.1 ∈ s) ∧ (∀ p ∈ t, p.2 ∈ f p.1) ∧ μ (s \ ⋃ p ∈ t, closedBall p.1 p.2) = 0 ∧ t.PairwiseDisjoint fun p => closedBall p.1 p.2
<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>ν : Measure α<VAR>hν : IsFiniteMeasure ν<VAR>hμν : μ ≪ ν<GOAL>∃ t, t.Countable ∧ (∀ p ∈ t, p.1 ∈ s) ∧ (∀ p ∈ t, p.2 ∈ f p.1) ∧ μ (s \ ⋃ p ∈ t, closedBall p.1 p.2) = 0 ∧ t.PairwiseDisjoint fun p => closedBall p.1 p.2
<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>ν : Measure α<VAR>hν : IsFiniteMeasure ν<VAR>hμν : μ ≪ ν<VAR>t : Set (α × ℝ)<VAR>t_count : t.Countable<VAR>ts : ∀ p ∈ t, p.1 ∈ s<VAR>tr : ∀ p ∈ t, p.2 ∈ f p.1<VAR>tν : ν (s \ ⋃ p ∈ t, closedBall p.1 p.2) = 0<VAR>tdisj : t.PairwiseDisjoint fun p => closedBall p.1 p.2<GOAL>∃ t, t.Countable ∧ (∀ p ∈ t, p.1 ∈ s) ∧ (∀ p ∈ t, p.2 ∈ f p.1) ∧ μ (s \ ⋃ p ∈ t, closedBall p.1 p.2) = 0 ∧ t.PairwiseDisjoint fun p => closedBall p.1 p.2
<VAR>a : UnitAddCircle<GOAL>ContinuousOn (sinKernel a) (Ioi 0)
<VAR>a : ℝ<GOAL>ContinuousOn (sinKernel ↑a) (Ioi 0)
<VAR>a : ℝ<GOAL>ContinuousOn (fun x => ↑(sinKernel (↑a) x)) (Ioi 0)
<VAR>a : ℝ<GOAL>ContinuousOn (fun x => jacobiTheta₂' (↑a) (I * ↑x) / (-2 * ↑π)) (Ioi 0)
<VAR>a x : ℝ<VAR>hx : x ∈ Ioi 0<GOAL>ContinuousAt (fun x => jacobiTheta₂' (↑a) (I * ↑x)) x
<VAR>a x : ℝ<VAR>hx : x ∈ Ioi 0<VAR>h : ContinuousAt (fun p => jacobiTheta₂' p.1 p.2) (↑a, I * ↑x)<GOAL>ContinuousAt (fun x => jacobiTheta₂' (↑a) (I * ↑x)) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>K : Submodule 𝕜 E<GOAL>⊥ᗮ = ⊤
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>K : Submodule 𝕜 E<GOAL>⊤ ≤ ⊤ᗮᗮ
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R⟦X⟧ˣ<GOAL>(d⁄dX R) ↑f⁻¹ = -↑f⁻¹ ^ 2 * (d⁄dX R) ↑f
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R⟦X⟧ˣ<GOAL>↑f⁻¹ * ↑f = 1
<VAR>ι : Sort uι<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>s : Submodule R M<VAR>n : N<GOAL>map₂ f s (span R {n}) = map (f.flip n) s
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>n : ℕ<VAR>a : ⨂[R]^n M<GOAL>(cast R M ⋯) (GradedMonoid.GMul.mul GradedMonoid.GOne.one a) = a
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>n : ℕ<VAR>a : ⨂[R]^n M<GOAL>(cast R M ⋯) (mulEquiv ((tprod R) Fin.elim0 ⊗ₜ[R] a)) = a
<VAR>R : Type u<VAR>inst✝¹⁴ : CommSemiring R<VAR>S : Type ?u.139799<VAR>inst✝¹³ : Semiring S<VAR>inst✝¹² : Algebra R S<VAR>ι₁ : Type v₁<VAR>ι₂ : Type v₂<VAR>inst✝¹¹ : DecidableEq ι₁<VAR>inst✝¹⁰ : DecidableEq ι₂<VAR>M₁ : ι₁ → Type w₁<VAR>M₁' : Type w₁'<VAR>M₂ : ι₂ → Type w₂<VAR>M₂' : Type w₂'<VAR>inst✝⁹ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)<VAR>inst✝⁸ : AddCommMonoid M₁'<VAR>inst✝⁷ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)<VAR>inst✝⁶ : AddCommMonoid M₂'<VAR>inst✝⁵ : (i₁ : ι₁) → Module R (M₁ i₁)<VAR>inst✝⁴ : Module R M₁'<VAR>inst✝³ : (i₂ : ι₂) → Module R (M₂ i₂)<VAR>inst✝² : Module R M₂'<VAR>inst✝¹ : (i₁ : ι₁) → Module S (M₁ i₁)<VAR>inst✝ : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)<VAR>x : M₁'<VAR>i : ι₂<VAR>y : M₂ i<GOAL>(directSumRight R M₁' M₂) (x ⊗ₜ[R] (lof R ι₂ M₂ i) y) = (lof R ι₂ (fun i => M₁' ⊗[R] M₂ i) i) (x ⊗ₜ[R] y)
<VAR>R : Type u<VAR>inst✝¹⁴ : CommSemiring R<VAR>S : Type ?u.139799<VAR>inst✝¹³ : Semiring S<VAR>inst✝¹² : Algebra R S<VAR>ι₁ : Type v₁<VAR>ι₂ : Type v₂<VAR>inst✝¹¹ : DecidableEq ι₁<VAR>inst✝¹⁰ : DecidableEq ι₂<VAR>M₁ : ι₁ → Type w₁<VAR>M₁' : Type w₁'<VAR>M₂ : ι₂ → Type w₂<VAR>M₂' : Type w₂'<VAR>inst✝⁹ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)<VAR>inst✝⁸ : AddCommMonoid M₁'<VAR>inst✝⁷ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)<VAR>inst✝⁶ : AddCommMonoid M₂'<VAR>inst✝⁵ : (i₁ : ι₁) → Module R (M₁ i₁)<VAR>inst✝⁴ : Module R M₁'<VAR>inst✝³ : (i₂ : ι₂) → Module R (M₂ i₂)<VAR>inst✝² : Module R M₂'<VAR>inst✝¹ : (i₁ : ι₁) → Module S (M₁ i₁)<VAR>inst✝ : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)<VAR>x : M₁'<VAR>i : ι₂<VAR>y : M₂ i<GOAL>(DFinsupp.mapRange.linearEquiv fun x => TensorProduct.comm R (M₂ x) M₁') ((directSumLeft R M₂ M₁') ((lof R ι₂ M₂ i) y ⊗ₜ[R] x)) = (lof R ι₂ (fun i => M₁' ⊗[R] M₂ i) i) (x ⊗ₜ[R] y)
<VAR>R : Type u<VAR>inst✝¹⁴ : CommSemiring R<VAR>S : Type ?u.139799<VAR>inst✝¹³ : Semiring S<VAR>inst✝¹² : Algebra R S<VAR>ι₁ : Type v₁<VAR>ι₂ : Type v₂<VAR>inst✝¹¹ : DecidableEq ι₁<VAR>inst✝¹⁰ : DecidableEq ι₂<VAR>M₁ : ι₁ → Type w₁<VAR>M₁' : Type w₁'<VAR>M₂ : ι₂ → Type w₂<VAR>M₂' : Type w₂'<VAR>inst✝⁹ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)<VAR>inst✝⁸ : AddCommMonoid M₁'<VAR>inst✝⁷ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)<VAR>inst✝⁶ : AddCommMonoid M₂'<VAR>inst✝⁵ : (i₁ : ι₁) → Module R (M₁ i₁)<VAR>inst✝⁴ : Module R M₁'<VAR>inst✝³ : (i₂ : ι₂) → Module R (M₂ i₂)<VAR>inst✝² : Module R M₂'<VAR>inst✝¹ : (i₁ : ι₁) → Module S (M₁ i₁)<VAR>inst✝ : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)<VAR>x : M₁'<VAR>i : ι₂<VAR>y : M₂ i<GOAL>(DFinsupp.mapRange.linearEquiv fun x => TensorProduct.comm R (M₂ x) M₁') ((lof R ι₂ (fun i => M₂ i ⊗[R] M₁') i) (y ⊗ₜ[R] x)) = (lof R ι₂ (fun i => M₁' ⊗[R] M₂ i) i) (x ⊗ₜ[R] y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>a b : α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>f : α → β<VAR>mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b<VAR>x✝ : WithBot α<GOAL>map f ⊥ ≤ map f x✝ ↔ ⊥ ≤ x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>a✝ b : α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>f : α → β<VAR>mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b<VAR>a : α<GOAL>map f ↑a ≤ map f ⊥ ↔ ↑a ≤ ⊥