ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>hLK : ↑(finrank K L) ≤ #K<VAR>U : LieSubalgebra K L<VAR>x : L<VAR>hxU : x ∈ U<VAR>y : L<VAR>hyU : y ∈ U<VAR>Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩<VAR>Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩<VAR>hUle : U ≤ ↑Ex<VAR>hmin : ∀ E ≤ Ex, Ex ≤ E<VAR>E : LieSubmodule K (↥U) L := let __src := engel K x; { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }<VAR>hx₀ : x ≠ 0<VAR>Q : Type u_2 := L ⧸ E<VAR>r : ℕ := finrank K ↥↑E<VAR>hr : r < finrank K L<VAR>x' : ↥U := ⟨x, hxU⟩<VAR>y' : ↥U := ⟨y, hyU⟩<VAR>u : ↥U := y' - x'<VAR>χ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K (↥↑E) x' u<VAR>ψ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K Q x' u<VAR>i : ℕ<VAR>hi : i < r<VAR>hi0 : i ≠ 0<VAR>hψ : constantCoeff ψ ≠ 0<VAR>s : Finset K<VAR>hs : r ≤ s.card<VAR>hsψ : ∀ α ∈ s, eval α (constantCoeff ψ) ≠ 0<VAR>α : K<VAR>hα : α ∈ s<VAR>v : ↥U := α • u + x'<GOAL>engel K ↑v ≤ engel K x
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>hLK : ↑(finrank K L) ≤ #K<VAR>U : LieSubalgebra K L<VAR>x : L<VAR>hxU : x ∈ U<VAR>y : L<VAR>hyU : y ∈ U<VAR>Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩<VAR>Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩<VAR>hUle : U ≤ ↑Ex<VAR>hmin : ∀ E ≤ Ex, Ex ≤ E<VAR>E : LieSubmodule K (↥U) L := let __src := engel K x; { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }<VAR>hx₀ : x ≠ 0<VAR>Q : Type u_2 := L ⧸ E<VAR>r : ℕ := finrank K ↥↑E<VAR>hr : r < finrank K L<VAR>x' : ↥U := ⟨x, hxU⟩<VAR>y' : ↥U := ⟨y, hyU⟩<VAR>u : ↥U := y' - x'<VAR>χ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K (↥↑E) x' u<VAR>ψ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K Q x' u<VAR>i : ℕ<VAR>hi : i < r<VAR>hi0 : i ≠ 0<VAR>hψ : constantCoeff ψ ≠ 0<VAR>s : Finset K<VAR>hs : r ≤ s.card<VAR>hsψ : ∀ α ∈ s, eval α (constantCoeff ψ) ≠ 0<VAR>α : K<VAR>hα : α ∈ s<VAR>v : ↥U := α • u + x'<VAR>z : L<VAR>hz : z ∈ engel K ↑v<GOAL>z ∈ E
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>hLK : ↑(finrank K L) ≤ #K<VAR>U : LieSubalgebra K L<VAR>x : L<VAR>hxU : x ∈ U<VAR>y : L<VAR>hyU : y ∈ U<VAR>Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩<VAR>Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩<VAR>hUle : U ≤ ↑Ex<VAR>hmin : ∀ E ≤ Ex, Ex ≤ E<VAR>E : LieSubmodule K (↥U) L := let __src := engel K x; { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }<VAR>hx₀ : x ≠ 0<VAR>Q : Type u_2 := L ⧸ E<VAR>r : ℕ := finrank K ↥↑E<VAR>hr : r < finrank K L<VAR>x' : ↥U := ⟨x, hxU⟩<VAR>y' : ↥U := ⟨y, hyU⟩<VAR>u : ↥U := y' - x'<VAR>χ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K (↥↑E) x' u<VAR>ψ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K Q x' u<VAR>i : ℕ<VAR>hi : i < r<VAR>hi0 : i ≠ 0<VAR>hψ : constantCoeff ψ ≠ 0<VAR>s : Finset K<VAR>hs : r ≤ s.card<VAR>hsψ : ∀ α ∈ s, eval α (constantCoeff ψ) ≠ 0<VAR>α : K<VAR>hα : α ∈ s<VAR>v : ↥U := α • u + x'<VAR>z : L<VAR>hz : z ∈ engel K ↑v<GOAL>(LieSubmodule.Quotient.mk' E) z = 0
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>hLK : ↑(finrank K L) ≤ #K<VAR>U : LieSubalgebra K L<VAR>x : L<VAR>hxU : x ∈ U<VAR>y : L<VAR>hyU : y ∈ U<VAR>Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩<VAR>Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩<VAR>hUle : U ≤ ↑Ex<VAR>hmin : ∀ E ≤ Ex, Ex ≤ E<VAR>E : LieSubmodule K (↥U) L := let __src := engel K x; { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }<VAR>hx₀ : x ≠ 0<VAR>Q : Type u_2 := L ⧸ E<VAR>r : ℕ := finrank K ↥↑E<VAR>hr : r < finrank K L<VAR>x' : ↥U := ⟨x, hxU⟩<VAR>y' : ↥U := ⟨y, hyU⟩<VAR>u : ↥U := y' - x'<VAR>χ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K (↥↑E) x' u<VAR>ψ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K Q x' u<VAR>i : ℕ<VAR>hi : i < r<VAR>hi0 : i ≠ 0<VAR>hψ : constantCoeff ψ ≠ 0<VAR>s : Finset K<VAR>hs : r ≤ s.card<VAR>hsψ : ∀ α ∈ s, eval α (constantCoeff ψ) ≠ 0<VAR>α : K<VAR>hα : α ∈ s<VAR>v : ↥U := α • u + x'<VAR>z : L<VAR>hz : z ∈ engel K ↑v<VAR>z' : Q := (LieSubmodule.Quotient.mk' E) z<GOAL>z' = 0
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>hLK : ↑(finrank K L) ≤ #K<VAR>U : LieSubalgebra K L<VAR>x : L<VAR>hxU : x ∈ U<VAR>y : L<VAR>hyU : y ∈ U<VAR>Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩<VAR>Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩<VAR>hUle : U ≤ ↑Ex<VAR>hmin : ∀ E ≤ Ex, Ex ≤ E<VAR>E : LieSubmodule K (↥U) L := let __src := engel K x; { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }<VAR>hx₀ : x ≠ 0<VAR>Q : Type u_2 := L ⧸ E<VAR>r : ℕ := finrank K ↥↑E<VAR>hr : r < finrank K L<VAR>x' : ↥U := ⟨x, hxU⟩<VAR>y' : ↥U := ⟨y, hyU⟩<VAR>u : ↥U := y' - x'<VAR>χ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K (↥↑E) x' u<VAR>ψ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K Q x' u<VAR>i : ℕ<VAR>hi : i < r<VAR>hi0 : i ≠ 0<VAR>hψ : constantCoeff ψ ≠ 0<VAR>s : Finset K<VAR>hs : r ≤ s.card<VAR>hsψ : ∀ α ∈ s, eval α (constantCoeff ψ) ≠ 0<VAR>α : K<VAR>hα : α ∈ s<VAR>v : ↥U := α • u + x'<VAR>z : L<VAR>hz : z ∈ engel K ↑v<VAR>z' : Q := (LieSubmodule.Quotient.mk' E) z<VAR>hz' : ∃ n, ((toEnd K (↥U) Q) v ^ n) z' = 0<GOAL>z' = 0
<VAR>P : Type u_1<VAR>inst✝ : BooleanAlgebra P<VAR>x : P<VAR>I : Ideal P<VAR>hI : I.IsProper<GOAL>x ∉ I ∨ xᶜ ∉ I
<VAR>P : Type u_1<VAR>inst✝ : BooleanAlgebra P<VAR>x : P<VAR>I : Ideal P<VAR>hI : I.IsProper<VAR>h : xᶜ ∈ I → x ∉ I<GOAL>x ∉ I ∨ xᶜ ∉ I
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : _root_.RCLike 𝕜<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>c : Core 𝕜 F<VAR>x : F<GOAL>⟪x, 0⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : _root_.RCLike 𝕜<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>c : Core 𝕜 F<VAR>x : F<GOAL>(starRingEnd 𝕜) 0 = 0
<VAR>a b m n p : ℕ<GOAL>a.factorizationLCMRight b ∣ b
<VAR>b m n p : ℕ<GOAL>factorizationLCMRight 0 b ∣ b
<VAR>a b m n p : ℕ<VAR>ha : a ≠ 0<GOAL>a.factorizationLCMRight b ∣ b
<VAR>a m n p : ℕ<VAR>ha : a ≠ 0<GOAL>a.factorizationLCMRight 0 ∣ 0
<VAR>a b m n p : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>a.factorizationLCMRight b ∣ b
<VAR>a b m n p : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>a.factorizationLCMRight b ∣ b.factorization.prod fun x x_1 => x ^ x_1
<VAR>a b m n p : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>a.factorizationLCMRight b ∣ ∏ x ∈ (a.lcm b).factorization.support, x ^ b.factorization x
<VAR>a b m n p : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>b.factorization.support ⊆ (a.lcm b).factorization.support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<GOAL>{ ofColex := s } < { ofColex := t } ↔ s ≠ t ∧ ∀ ⦃a : α⦄, a ∈ s → a ∉ t → ∃ b ∈ t, b ∉ s ∧ a ≤ b
<VAR>L : Language<VAR>M : Type u_1<VAR>s : Setoid M<VAR>ps : L.Prestructure s<VAR>n : ℕ<VAR>f : L.Functions n<VAR>x : Fin n → M<GOAL>(funMap f fun i => ⟦x i⟧) = ⟦funMap f x⟧
<VAR>L : Language<VAR>M : Type u_1<VAR>s : Setoid M<VAR>ps : L.Prestructure s<VAR>n : ℕ<VAR>f : L.Functions n<VAR>x : Fin n → M<GOAL>Quotient.map (funMap f) ⋯ (Quotient.finChoice fun i => ⟦x i⟧) = ⟦funMap f x⟧
<VAR>α : Sort u_1<VAR>hα : Nonempty α<VAR>o : Ordinal.{u_2}<VAR>f : α → Ordinal.{u_2}<VAR>H : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ i, a < f i<VAR>b a : Ordinal.{u_2}<VAR>h : a < b + o<GOAL>∃ i, a < b + f i
<VAR>α : Sort u_1<VAR>hα : Nonempty α<VAR>o : Ordinal.{u_2}<VAR>f : α → Ordinal.{u_2}<VAR>H : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ i, a < f i<VAR>b a : Ordinal.{u_2}<VAR>h✝ : a < b + o<VAR>h : a < b<GOAL>∃ i, a < b + f i
<VAR>α : Sort u_1<VAR>hα : Nonempty α<VAR>o : Ordinal.{u_2}<VAR>f : α → Ordinal.{u_2}<VAR>H : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ i, a < f i<VAR>b a : Ordinal.{u_2}<VAR>h : a < b + o<VAR>h' : b ≤ a<GOAL>∃ i, a < b + f i
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : CommRing α<VAR>A✝ B✝ A B C : Matrix n n α<VAR>inst✝ : Invertible A<VAR>h : A⁻¹ * B = C<GOAL>B = A * C
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : CommRing α<VAR>A✝ B✝ A B C : Matrix n n α<VAR>inst✝ : Invertible A<VAR>h : B = A * C<GOAL>A⁻¹ * B = C
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Field R<VAR>p q : R[X]<VAR>inst✝ : Field k<VAR>f : R →+* k<GOAL>map f (p / q) = map f p / map f q
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>hz : z ≤ y<VAR>hx : x ≤ y<VAR>H : x ≤ z<GOAL>y = z ⊔ y \ x
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>hz : z ≤ y<VAR>hx : x ≤ y<VAR>H : x ≤ z<GOAL>y ≤ z ⊔ y \ x
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>hz : z ≤ y<VAR>hx : x ≤ y<VAR>H : x ≤ z<GOAL>z ⊔ y \ x ≤ y
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>hz : z ≤ y<VAR>hx : x ≤ y<VAR>H : y = z ⊔ y \ x<GOAL>x ≤ z
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>hz : z ≤ y<VAR>hx : x ≤ y<VAR>H : x ⊔ y \ x = z ⊔ y \ x<GOAL>x ≤ z
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>hz : z ≤ y<VAR>hx : x ≤ y<VAR>H : x ⊔ y \ x = z ⊔ y \ x<GOAL>x ⊓ y \ x ≤ z ⊓ y \ x
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>hz : z ≤ y<VAR>hx : x ≤ y<VAR>H : x ⊔ y \ x = z ⊔ y \ x<GOAL>⊥ ≤ z ⊓ y \ x
<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>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₃ : Type u_9<VAR>V : Type u_10<VAR>V₂ : Type u_11<VAR>inst✝¹¹ : Ring R<VAR>inst✝¹⁰ : Ring R₂<VAR>inst✝⁹ : Ring R₃<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : AddCommGroup M₃<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R₂ M₂<VAR>inst✝³ : Module R₃ M₃<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝² : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>F : Type u_12<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>f✝ : F<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>S : Submodule R M<GOAL>Injective ⇑(f.domRestrict S) ↔ S ⊓ ker f = ⊥
<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>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₃ : Type u_9<VAR>V : Type u_10<VAR>V₂ : Type u_11<VAR>inst✝¹¹ : Ring R<VAR>inst✝¹⁰ : Ring R₂<VAR>inst✝⁹ : Ring R₃<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : AddCommGroup M₃<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R₂ M₂<VAR>inst✝³ : Module R₃ M₃<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝² : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>F : Type u_12<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>f✝ : F<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>S : Submodule R M<GOAL>ker (f.domRestrict S) = ⊥ ↔ S ⊓ ker f = ⊥
<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>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₃ : Type u_9<VAR>V : Type u_10<VAR>V₂ : Type u_11<VAR>inst✝¹¹ : Ring R<VAR>inst✝¹⁰ : Ring R₂<VAR>inst✝⁹ : Ring R₃<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : AddCommGroup M₃<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R₂ M₂<VAR>inst✝³ : Module R₃ M₃<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝² : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>F : Type u_12<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>f✝ : F<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>S : Submodule R M<VAR>h : ker (f.domRestrict S) = ⊥<GOAL>S ⊓ ker f ≤ ⊥
<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>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₃ : Type u_9<VAR>V : Type u_10<VAR>V₂ : Type u_11<VAR>inst✝¹¹ : Ring R<VAR>inst✝¹⁰ : Ring R₂<VAR>inst✝⁹ : Ring R₃<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : AddCommGroup M₃<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R₂ M₂<VAR>inst✝³ : Module R₃ M₃<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝² : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>F : Type u_12<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>f✝ : F<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>S : Submodule R M<VAR>h : S ⊓ ker f = ⊥<GOAL>ker (f.domRestrict S) ≤ ⊥
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>a b : α<VAR>μ : Measure α<VAR>l : Filter α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : SecondCountableTopology α<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : CompactIccSpace α<VAR>inst✝² : atTop.IsMeasurablyGenerated<VAR>inst✝¹ : MeasurableNeg α<VAR>inst✝ : μ.IsNegInvariant<VAR>hf : LocallyIntegrable f μ<VAR>hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg<VAR>ho : f =O[atTop] g<VAR>hg : IntegrableAtFilter g atTop μ<GOAL>Integrable f μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>a b : α<VAR>μ : Measure α<VAR>l : Filter α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : SecondCountableTopology α<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : CompactIccSpace α<VAR>inst✝² : atTop.IsMeasurablyGenerated<VAR>inst✝¹ : MeasurableNeg α<VAR>inst✝ : μ.IsNegInvariant<VAR>hf : LocallyIntegrable f μ<VAR>hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg<VAR>ho : f =O[atTop] g<VAR>hg : IntegrableAtFilter g atTop μ<VAR>h_int : IntegrableOn f (Ici 0) μ<GOAL>Integrable f μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>a b : α<VAR>μ : Measure α<VAR>l : Filter α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : SecondCountableTopology α<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : CompactIccSpace α<VAR>inst✝² : atTop.IsMeasurablyGenerated<VAR>inst✝¹ : MeasurableNeg α<VAR>inst✝ : μ.IsNegInvariant<VAR>hf : LocallyIntegrable f μ<VAR>hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg<VAR>ho : f =O[atTop] g<VAR>hg : IntegrableAtFilter g atTop μ<VAR>h_int : IntegrableOn f (Ici 0) μ<GOAL>IntegrableOn f (Iic ?m.33104) μ ∧ IntegrableOn f (Ici ?m.33104) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>a b : α<VAR>μ : Measure α<VAR>l : Filter α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : SecondCountableTopology α<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : CompactIccSpace α<VAR>inst✝² : atTop.IsMeasurablyGenerated<VAR>inst✝¹ : MeasurableNeg α<VAR>inst✝ : μ.IsNegInvariant<VAR>hf : LocallyIntegrable f μ<VAR>hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg<VAR>ho : f =O[atTop] g<VAR>hg : IntegrableAtFilter g atTop μ<VAR>h_int : IntegrableOn f (Ici 0) μ<GOAL>α
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>a b : α<VAR>μ : Measure α<VAR>l : Filter α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : SecondCountableTopology α<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : CompactIccSpace α<VAR>inst✝² : atTop.IsMeasurablyGenerated<VAR>inst✝¹ : MeasurableNeg α<VAR>inst✝ : μ.IsNegInvariant<VAR>hf : LocallyIntegrable f μ<VAR>hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg<VAR>ho : f =O[atTop] g<VAR>hg : IntegrableAtFilter g atTop μ<VAR>h_int : IntegrableOn f (Ici 0) μ<GOAL>IntegrableOn f (Iic 0) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>a b : α<VAR>μ : Measure α<VAR>l : Filter α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : SecondCountableTopology α<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : CompactIccSpace α<VAR>inst✝² : atTop.IsMeasurablyGenerated<VAR>inst✝¹ : MeasurableNeg α<VAR>inst✝ : μ.IsNegInvariant<VAR>hf : LocallyIntegrable f μ<VAR>hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg<VAR>ho : f =O[atTop] g<VAR>hg : IntegrableAtFilter g atTop μ<VAR>h_int : IntegrableOn f (Ici 0) μ<VAR>h_map_neg : Measure.map Neg.neg (μ.restrict (Ici 0)) = μ.restrict (Iic 0)<GOAL>IntegrableOn f (Iic 0) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>a b : α<VAR>μ : Measure α<VAR>l : Filter α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : SecondCountableTopology α<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : CompactIccSpace α<VAR>inst✝² : atTop.IsMeasurablyGenerated<VAR>inst✝¹ : MeasurableNeg α<VAR>inst✝ : μ.IsNegInvariant<VAR>hf : LocallyIntegrable f μ<VAR>hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg<VAR>ho : f =O[atTop] g<VAR>hg : IntegrableAtFilter g atTop μ<VAR>h_int : IntegrableOn f (Ici 0) μ<VAR>h_map_neg : Measure.map Neg.neg (μ.restrict (Ici 0)) = μ.restrict (Iic 0)<GOAL>Integrable (f ∘ Neg.neg) (μ.restrict (Ici 0))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>a b : α<VAR>μ : Measure α<VAR>l : Filter α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : SecondCountableTopology α<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : CompactIccSpace α<VAR>inst✝² : atTop.IsMeasurablyGenerated<VAR>inst✝¹ : MeasurableNeg α<VAR>inst✝ : μ.IsNegInvariant<VAR>hf : LocallyIntegrable f μ<VAR>hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg<VAR>ho : f =O[atTop] g<VAR>hg : IntegrableAtFilter g atTop μ<VAR>h_int : IntegrableOn f (Ici 0) μ<VAR>h_map_neg : Measure.map Neg.neg (μ.restrict (Ici 0)) = μ.restrict (Iic 0)<GOAL>AEStronglyMeasurable (f ∘ Neg.neg) (μ.restrict (Ici 0))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>a b : α<VAR>μ : Measure α<VAR>l : Filter α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : SecondCountableTopology α<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : CompactIccSpace α<VAR>inst✝² : atTop.IsMeasurablyGenerated<VAR>inst✝¹ : MeasurableNeg α<VAR>inst✝ : μ.IsNegInvariant<VAR>hf : LocallyIntegrable f μ<VAR>hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg<VAR>ho : f =O[atTop] g<VAR>hg : IntegrableAtFilter g atTop μ<VAR>h_int : IntegrableOn f (Ici 0) μ<VAR>h_map_neg : Measure.map Neg.neg (μ.restrict (Ici 0)) = μ.restrict (Iic 0)<GOAL>AEStronglyMeasurable f (Measure.map Neg.neg (μ.restrict (Ici 0)))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r r' : α → α → Prop<VAR>f : β → α<VAR>s t : Set α<VAR>x y : α<GOAL>univ.WellFoundedOn r ↔ WellFounded r
<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>h : x ∉ closure s<GOAL>fderivWithin 𝕜 f s x = 0
<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>h : x ∉ closure s<GOAL>𝓝[s \ {x}] x = ⊥
<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>h : 𝓝[s] x = ⊥<GOAL>𝓝[s \ {x}] x = ⊥
<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>h : 𝓝[s] x = ⊥<GOAL>𝓝[s \ {x}] x ≤ 𝓝[s] x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f : E → F<VAR>g : F →ₗᵢ[𝕜] G<VAR>hf : ContDiffOn 𝕜 n f s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>i : ℕ<VAR>hi : ↑i ≤ n<GOAL>‖iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s x‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f : E → F<VAR>g : F →ₗᵢ[𝕜] G<VAR>hf : ContDiffOn 𝕜 n f s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>i : ℕ<VAR>hi : ↑i ≤ n<VAR>this : iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s x = g.toContinuousLinearMap.compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x)<GOAL>‖iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s x‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f : E → F<VAR>g : F →ₗᵢ[𝕜] G<VAR>hf : ContDiffOn 𝕜 n f s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>i : ℕ<VAR>hi : ↑i ≤ n<VAR>this : iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s x = g.toContinuousLinearMap.compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x)<GOAL>‖g.toContinuousLinearMap.compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x)‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖