ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>inst✝⁷ : 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>inst✝¹ : SmoothManifoldWithCorners I' M'<VAR>e✝ : PartialHomeomorph M H<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>inst✝ : ChartedSpace H M'<VAR>IsM' : SmoothManifoldWithCorners I M'<VAR>f : PartialHomeomorph M M'<VAR>hf : LiftPropOn (contDiffGroupoid ⊤ I).IsLocalStructomorphWithinAt (↑f) f.source<VAR>x : M<VAR>hx : x ∈ f.source<VAR>c : PartialHomeomorph M H := chartAt H x<VAR>c' : PartialHomeomorph M' H := chartAt H (↑f x)<VAR>hxf : (contDiffGroupoid ⊤ I).IsLocalStructomorphWithinAt (↑(chartAt H (↑f x)) ∘ ↑f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' f.source) (↑(chartAt H x) x)<VAR>e : PartialHomeomorph H H<VAR>he : e ∈ contDiffGroupoid ⊤ I<VAR>he' : EqOn (↑c' ∘ ↑f ∘ ↑c.symm) (↑e) (↑c.symm ⁻¹' f.source ∩ e.source)<VAR>hex : ↑c x ∈ e.source<VAR>s : Set M := (f ≫ₕ c').source ∩ ((c ≫ₕ e) ≫ₕ c'.symm).source<VAR>H₁ : ContMDiffOn I I ⊤ (↑c'.symm ∘ ↑e ∘ ↑c) s<GOAL>ContMDiffOn I I ⊤ (↑f) (f.source ∩ 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>inst✝⁷ : 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>inst✝¹ : SmoothManifoldWithCorners I' M'<VAR>e✝ : PartialHomeomorph M H<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>inst✝ : ChartedSpace H M'<VAR>IsM' : SmoothManifoldWithCorners I M'<VAR>f : PartialHomeomorph M M'<VAR>hf : LiftPropOn (contDiffGroupoid ⊤ I).IsLocalStructomorphWithinAt (↑f) f.source<VAR>x : M<VAR>hx : x ∈ f.source<VAR>c : PartialHomeomorph M H := chartAt H x<VAR>c' : PartialHomeomorph M' H := chartAt H (↑f x)<VAR>hxf : (contDiffGroupoid ⊤ I).IsLocalStructomorphWithinAt (↑(chartAt H (↑f x)) ∘ ↑f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' f.source) (↑(chartAt H x) x)<VAR>e : PartialHomeomorph H H<VAR>he : e ∈ contDiffGroupoid ⊤ I<VAR>he' : EqOn (↑c' ∘ ↑f ∘ ↑c.symm) (↑e) (↑c.symm ⁻¹' f.source ∩ e.source)<VAR>hex : ↑c x ∈ e.source<VAR>s : Set M := (f ≫ₕ c').source ∩ ((c ≫ₕ e) ≫ₕ c'.symm).source<VAR>H₁ : ContMDiffOn I I ⊤ (↑c'.symm ∘ ↑e ∘ ↑c) s<VAR>H₂ : EqOn (↑f) (↑c'.symm ∘ ↑e ∘ ↑c) s<GOAL>ContMDiffOn I I ⊤ (↑f) (f.source ∩ 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>inst✝⁷ : 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>inst✝¹ : SmoothManifoldWithCorners I' M'<VAR>e✝ : PartialHomeomorph M H<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>inst✝ : ChartedSpace H M'<VAR>IsM' : SmoothManifoldWithCorners I M'<VAR>f : PartialHomeomorph M M'<VAR>hf : LiftPropOn (contDiffGroupoid ⊤ I).IsLocalStructomorphWithinAt (↑f) f.source<VAR>x : M<VAR>hx : x ∈ f.source<VAR>c : PartialHomeomorph M H := chartAt H x<VAR>c' : PartialHomeomorph M' H := chartAt H (↑f x)<VAR>hxf : (contDiffGroupoid ⊤ I).IsLocalStructomorphWithinAt (↑(chartAt H (↑f x)) ∘ ↑f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' f.source) (↑(chartAt H x) x)<VAR>e : PartialHomeomorph H H<VAR>he : e ∈ contDiffGroupoid ⊤ I<VAR>he' : EqOn (↑c' ∘ ↑f ∘ ↑c.symm) (↑e) (↑c.symm ⁻¹' f.source ∩ e.source)<VAR>hex : ↑c x ∈ e.source<VAR>s : Set M := (f ≫ₕ c').source ∩ ((c ≫ₕ e) ≫ₕ c'.symm).source<VAR>H₁ : ContMDiffOn I I ⊤ (↑c'.symm ∘ ↑e ∘ ↑c) s<VAR>H₂ : EqOn (↑f) (↑c'.symm ∘ ↑e ∘ ↑c) s<GOAL>f.source ∩ s ⊆ s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : CompleteLattice β<VAR>s : Finset α<VAR>f : α → β<GOAL>s.sup f = sSup (f '' ↑s)
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>inst✝³ : Semiring R<VAR>inst✝² : Semiring S<VAR>inst✝¹ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f✝ : F<VAR>I J : Ideal R<VAR>K L : Ideal S<VAR>G : Type u_2<VAR>inst✝ : FunLike G S R<VAR>rcg : RingHomClass G S R<VAR>f : F<VAR>s : Set R<GOAL>map f (span s) = span (⇑f '' s)
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>inst✝³ : Semiring R<VAR>inst✝² : Semiring S<VAR>inst✝¹ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f✝ : F<VAR>I J : Ideal R<VAR>K L : Ideal S<VAR>G : Type u_2<VAR>inst✝ : FunLike G S R<VAR>rcg : RingHomClass G S R<VAR>f : F<VAR>s : Set R<GOAL>⇑f '' s ⊆ ↑(map f (span s))
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>inst✝³ : Semiring R<VAR>inst✝² : Semiring S<VAR>inst✝¹ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f✝ : F<VAR>I J : Ideal R<VAR>K L : Ideal S<VAR>G : Type u_2<VAR>inst✝ : FunLike G S R<VAR>rcg : RingHomClass G S R<VAR>f : F<VAR>s : Set R<GOAL>map f (span s) ≤ Submodule.span S (⇑f '' s)
<VAR>V : Type u<VAR>G✝ : SimpleGraph V<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G✝.Coloring α<VAR>G : SimpleGraph V<VAR>n : ℕ<VAR>h : G.Colorable n<GOAL>G.chromaticNumber = ↑(sInf {n' | G.Colorable n'})
<VAR>V : Type u<VAR>G✝ : SimpleGraph V<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G✝.Coloring α<VAR>G : SimpleGraph V<VAR>n : ℕ<VAR>h : G.Colorable n<GOAL>{n' | G.Colorable n'}.Nonempty
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K : Set ℂ<VAR>z : ℂ<VAR>M r δ : ℝ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>u : ι → ℝ<VAR>hu : Summable u<VAR>hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U<VAR>hU : IsOpen U<VAR>hF_le : ∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i<GOAL>DifferentiableOn ℂ (fun w => ∑' (i : ι), F i w) U
<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>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>f✝ f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s✝ s' : Set α<VAR>t t' : Set β<VAR>u u' : Set γ<VAR>v : Set δ<VAR>a a' : α<VAR>b✝ b' : β<VAR>c c' : γ<VAR>d d' : δ<VAR>f : α → β → α<VAR>b : β<VAR>h : ∀ (a : α), f a b = a<VAR>s : Set α<GOAL>image2 f s {b} = s
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>r : ℝ<GOAL>(o.oangle (x + r • y) y).sign = (o.oangle x y).sign
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<GOAL>(starRingEnd K) (-I) = I
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝ : L.Structure M<VAR>s : Set M<VAR>hs : s.Finite<GOAL>(closure L).toFun ↑hs.toFinset = (closure L).toFun s
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁✝ : S₁.HomologyData<VAR>h₂✝ : S₂.HomologyData<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>γ : LeftHomologyMapData φ h₁ h₂<VAR>inst✝¹ : S₁.HasHomology<VAR>inst✝ : S₂.HasHomology<GOAL>leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left = (leftHomologyMap' (𝟙 S₁) S₁.homologyData.left S₁.leftHomologyData ≫ leftHomologyMap' (𝟙 S₁) S₁.leftHomologyData h₁) ≫ γ.φH ≫ leftHomologyMap' (𝟙 S₂) h₂ S₂.leftHomologyData ≫ leftHomologyMap' (𝟙 S₂) S₂.leftHomologyData S₂.homologyData.left
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>k : Type u_3<VAR>inst✝ : Field k<VAR>φ : MvPowerSeries σ k<VAR>h : (constantCoeff σ k) φ ≠ 0<GOAL>φ * φ⁻¹ = 1
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : NonAssocSemiring R<VAR>M : Submonoid R<VAR>inst✝¹ : NonAssocSemiring S<VAR>inst✝ : NonAssocSemiring T<VAR>s : Subsemiring R<VAR>x : R × S<GOAL>x ∈ s.prod ⊤ ↔ x ∈ comap (RingHom.fst R S) s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>p : P<GOAL>vectorSpan k {p} = ⊥
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>a b c d : α<GOAL>b ≤ a ∆ b ↔ Disjoint a b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>m : α → β<VAR>hm : Injective m<VAR>f₁ f₂ : Filter α<GOAL>Disjoint (map m f₁) (map m f₂) ↔ Disjoint f₁ f₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>inst✝ : CompleteLattice β<VAR>S : Set (Set α)<VAR>p : α → Prop<GOAL>(∀ x ∈ ⋃₀ S, p x) ↔ ∀ s ∈ S, ∀ x ∈ s, p x
<VAR>m n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>x : α✝ 0<VAR>q : (i : Fin (n + 1)) → α✝ i<VAR>p : (i : Fin n) → α✝ i.succ<VAR>i : Fin n<VAR>y : α✝ i.succ<VAR>z : α✝ 0<VAR>α : Type u_1<VAR>a : Fin n → α<VAR>m₁ m₂ : ℕ<VAR>h : (m₁ + m₂) * n = m₁ * n + m₂ * n<GOAL>repeat (m₁ + m₂) a = append (repeat m₁ a) (repeat m₂ a) ∘ cast h
<VAR>m n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>x : α✝ 0<VAR>q : (i : Fin (n + 1)) → α✝ i<VAR>p : (i : Fin n) → α✝ i.succ<VAR>i : Fin n<VAR>y : α✝ i.succ<VAR>z : α✝ 0<VAR>α : Type u_1<VAR>a : Fin n → α<VAR>m₁ m₂ : ℕ<VAR>h : (m₁ + m₂) * n = m₁ * n + m₂ * n<GOAL>∀ (x : Fin ((m₁ + m₂) * n)), repeat (m₁ + m₂) a x = (append (repeat m₁ a) (repeat m₂ a) ∘ cast h) x
<VAR>m n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>x : α✝ 0<VAR>q : (i : Fin (n + 1)) → α✝ i<VAR>p : (i : Fin n) → α✝ i.succ<VAR>i : Fin n<VAR>y : α✝ i.succ<VAR>z : α✝ 0<VAR>α : Type u_1<VAR>a : Fin n → α<VAR>m₁ m₂ : ℕ<VAR>h : (m₁ + m₂) * n = m₁ * n + m₂ * n<GOAL>∀ (x : Fin (m₁ * n + m₂ * n)), repeat (m₁ + m₂) a (cast ⋯ x) = (append (repeat m₁ a) (repeat m₂ a) ∘ cast h) (cast ⋯ x)
<VAR>J : Type v'<VAR>inst✝³ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝¹ : Category.{?u.5921, u_1} K<VAR>D : Type u_2<VAR>inst✝ : Category.{?u.5928, u_2} D<VAR>F F' : Discrete WalkingPair ⥤ C<VAR>α : F ⟶ F'<GOAL>IsPullback (F.map { down := { down := ⋯ } }) (α.app { as := WalkingPair.left }) (α.app { as := { as := WalkingPair.left }.as }) (F'.map { down := { down := ⋯ } })
<VAR>J : Type v'<VAR>inst✝³ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝¹ : Category.{?u.5921, u_1} K<VAR>D : Type u_2<VAR>inst✝ : Category.{?u.5928, u_2} D<VAR>F F' : Discrete WalkingPair ⥤ C<VAR>α : F ⟶ F'<GOAL>IsPullback (F.map { down := { down := ⋯ } }) (α.app { as := WalkingPair.right }) (α.app { as := { as := WalkingPair.right }.as }) (F'.map { down := { down := ⋯ } })
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommRing P<VAR>A : Type u_4<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : UniqueFactorizationMonoid A<VAR>K : Type u_5<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>x y : K<VAR>h : y * (algebraMap A K) ↑(den A x) = (algebraMap A K) (num A x)<GOAL>x = y
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommRing P<VAR>A : Type u_4<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : UniqueFactorizationMonoid A<VAR>K : Type u_5<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>x y : K<VAR>h : x = y<GOAL>y = mk' K (num A x) (den A 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✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f : α → ℝ<VAR>hfi : Integrable f μ<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>this : f =ᶠ[ae μ] fun x => ‖f x‖<GOAL>ENNReal.ofReal (∫ (x : α), f x ∂μ) = ∫⁻ (x : α), ENNReal.ofReal (f 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✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f : α → ℝ<VAR>hfi : Integrable f μ<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>this : f =ᶠ[ae μ] fun x => ‖f x‖<GOAL>∫⁻ (x : α), ENNReal.ofReal ‖f x‖ ∂μ = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>H : Subgroup G<VAR>inst✝² : H.IsCommutative<VAR>inst✝¹ : H.FiniteIndex<VAR>α✝¹ β : ↑(leftTransversals ↑H)<VAR>inst✝ : H.Normal<VAR>hH : (Nat.card ↥H).Coprime H.index<VAR>α✝ : H.QuotientDiff<VAR>h : ↥H<VAR>α : ↑(leftTransversals ↑H)<VAR>hα : h • Quotient.mk'' α = Quotient.mk'' α<GOAL>h ^ H.index = diff (MonoidHom.id ↥H) (op ↑h⁻¹ • α) α
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderClosedTopology α<VAR>a b c d : α<GOAL>𝓝ˢ (Ici a) = 𝓝 a ⊔ 𝓟 (Ioi a)
<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>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g✝ : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x✝ : E<VAR>s✝ t✝ : Set E<VAR>L L₁ L₂ : Filter E<VAR>g : F → G<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>t : Set F<VAR>hf : DifferentiableWithinAt 𝕜 f s x<VAR>h : MapsTo f s t<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>v : E<VAR>hg : DifferentiableWithinAt 𝕜 g t (f x)<GOAL>(fderivWithin 𝕜 g t (f x)) ((fderivWithin 𝕜 f s x) v) = (fderivWithin 𝕜 (g ∘ f) s x) v
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f g : Filter α<VAR>s t : Set α<GOAL>¬Disjoint f f ↔ f.NeBot
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : Field 𝕜<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : DecidableEq p<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Fintype n<VAR>P : Matrix n n 𝕜 → Prop<VAR>M : Matrix n n 𝕜<VAR>hdiag : ∀ (D : n → 𝕜), (diagonal D).det = M.det → P (diagonal D)<VAR>htransvec : ∀ (t : TransvectionStruct n 𝕜), P t.toMatrix<VAR>hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A * B)<GOAL>P M
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : Field 𝕜<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : DecidableEq p<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Fintype n<VAR>P : Matrix n n 𝕜 → Prop<VAR>M : Matrix n n 𝕜<VAR>hdiag : ∀ (D : n → 𝕜), (diagonal D).det = M.det → P (diagonal D)<VAR>htransvec : ∀ (t : TransvectionStruct n 𝕜), P t.toMatrix<VAR>hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A * B)<VAR>L L' : List (TransvectionStruct n 𝕜)<VAR>D : n → 𝕜<VAR>h : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod<GOAL>P M
<VAR>x✝ y z a : ℝ<VAR>ha : 0 < a<VAR>x : ℝ<GOAL>HasStrictDerivAt (fun x => a ^ x) (a ^ x * log a) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>hfg : IsBigOWith c l f g<VAR>hgk : g =o[l] k<VAR>hc : 0 < c<GOAL>f =o[l] k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>hfg : IsBigOWith c l f g<VAR>hc : 0 < c<VAR>hgk : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l g k<GOAL>∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c'✝ c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>hfg : IsBigOWith c l f g<VAR>hc : 0 < c<VAR>hgk : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l g k<VAR>c' : ℝ<VAR>c'pos : 0 < c'<GOAL>IsBigOWith c' l f k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c'✝ c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>hfg : IsBigOWith c l f g<VAR>hc : 0 < c<VAR>hgk : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l g k<VAR>c' : ℝ<VAR>c'pos : 0 < c'<VAR>this : 0 < c' / c<GOAL>IsBigOWith c' l f k
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : Zero M<VAR>inst✝ : DecidableEq α<VAR>l : AList fun _x => M<VAR>a : α<GOAL>l.lookupFinsupp a = 0 ↔ a ∉ l ∨ 0 ∈ lookup a l
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : Zero M<VAR>inst✝ : DecidableEq α<VAR>l : AList fun _x => M<VAR>a : α<GOAL>(lookup a l).getD 0 = 0 ↔ lookup a l = none ∨ 0 ∈ lookup a l
<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>hb : AddLECancellable b<VAR>hba : b ≤ a<GOAL>a - b < c ↔ a < b + c
<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>hb : AddLECancellable b<VAR>hba : b ≤ a<GOAL>a < b + c → a - b < c
<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>hb : AddLECancellable b<VAR>hba : b ≤ a<VAR>h : a < b + c<GOAL>a - b < c
<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>hb : AddLECancellable b<VAR>hba : b ≤ a<VAR>h : a < b + c<GOAL>a - b ≠ c
<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 d : α<VAR>hb : AddLECancellable b<VAR>hba : b ≤ a<VAR>h : a < b + (a - b)<GOAL>False
<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 : ℕ<GOAL>f' ^ (n + 1) = (f' ^ n) ∘ₗ f'
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : Fintype σ<VAR>inst✝² : Fintype τ<VAR>n : ℕ<VAR>inst✝¹ : DecidableEq σ<VAR>inst✝ : Nontrivial R<GOAL>(esymm σ R n).support = (powersetCard n univ).biUnion fun t => (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1).support
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : Fintype σ<VAR>inst✝² : Fintype τ<VAR>n : ℕ<VAR>inst✝¹ : DecidableEq σ<VAR>inst✝ : Nontrivial R<GOAL>(∑ t ∈ powersetCard n univ, (monomial (∑ i ∈ t, Finsupp.single i 1)) 1).support = (powersetCard n univ).biUnion fun t => (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1).support
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : Fintype σ<VAR>inst✝² : Fintype τ<VAR>n : ℕ<VAR>inst✝¹ : DecidableEq σ<VAR>inst✝ : Nontrivial R<GOAL>(∑ x ∈ powersetCard n univ, Finsupp.single (∑ i ∈ x, Finsupp.single i 1) 1).support = (powersetCard n univ).biUnion fun t => (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1).support