ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜 F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : CompleteSpace F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>x : G<GOAL>↑↑0 =ᶠ[ae μ] ↑↑(0 x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜 F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : CompleteSpace F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>x : G<GOAL>0 =ᶠ[ae μ] ↑↑(0 x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜 F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : CompleteSpace F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>x : G<GOAL>0 =ᶠ[ae μ] 0
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<GOAL>s \ t ⊆ closure t ↔ s ⊆ closure t
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>‖(o.kahler x) y‖ = ‖x‖ * ‖y‖
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIocMod hp a (-b) = p - toIcoMod hp (-a) b
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>-b - -(toIcoDiv hp (-a) b • p + 1 • p) = p - (b - toIcoDiv hp (-a) b • p)
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>inst✝² : DecidablePred p<VAR>H : ∃ n, p n<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred q<VAR>hₘ : ∃ m, p (m + n)<VAR>hₙ : ∃ n, p n<VAR>hn : n ≤ Nat.find hₙ<GOAL>Nat.find hₘ + n = Nat.find hₙ
<VAR>a b c d m✝ n k : ℕ<VAR>p q : ℕ → Prop<VAR>inst✝² : DecidablePred p<VAR>H : ∃ n, p n<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred q<VAR>hₘ : ∃ m, p (m + n)<VAR>hₙ : ∃ n, p n<VAR>hn : n ≤ Nat.find hₙ<VAR>m : ℕ<VAR>hm : m < Nat.find hₘ + n<VAR>hpm : p m<GOAL>Nat.find hₘ + n ≤ m
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>inst✝² : DecidablePred p<VAR>H : ∃ n, p n<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred q<VAR>hₘ : ∃ m, p (m + n)<VAR>hₙ : ∃ n, p n<VAR>hn : n ≤ Nat.find hₙ<GOAL>Nat.find hₙ ≤ Nat.find hₘ + n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : Zero M<VAR>inst✝ : AddCommMonoid N<VAR>f : α → β<VAR>l : β →₀ M<VAR>g : β → M → N<VAR>hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support<GOAL>∑ x ∈ l.support.preimage f ⋯, g (f x) ({ support := l.support.preimage f ⋯, toFun := fun a => l (f a), mem_support_toFun := ⋯ } x) = ∑ a ∈ l.support, g a (l a)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : IsNoetherian R L<VAR>H : LieSubalgebra R L<VAR>h : ∀ x ∈ H, H ≤ engel R x<GOAL>LieAlgebra.IsNilpotent R ↥H
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : IsNoetherian R L<VAR>H : LieSubalgebra R L<VAR>h : ∀ x ∈ H, H ≤ engel R x<GOAL>∀ (x : ↥H), _root_.IsNilpotent ((ad R ↥H) x)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : IsNoetherian R L<VAR>H : LieSubalgebra R L<VAR>h : ∀ x ∈ H, H ≤ engel R x<VAR>x : ↥H<VAR>K : ℕ →o Submodule R ↥H := { toFun := fun n => LinearMap.ker ((ad R ↥H) x ^ n), monotone' := ⋯ }<GOAL>_root_.IsNilpotent ((ad R ↥H) x)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : IsNoetherian R L<VAR>H : LieSubalgebra R L<VAR>h : ∀ x ∈ H, H ≤ engel R x<VAR>x : ↥H<VAR>m n : ℕ<VAR>hmn : m ≤ n<GOAL>(fun n => LinearMap.ker ((ad R ↥H) x ^ n)) m ≤ (fun n => LinearMap.ker ((ad R ↥H) x ^ n)) n
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : IsNoetherian R L<VAR>H : LieSubalgebra R L<VAR>h : ∀ x ∈ H, H ≤ engel R x<VAR>x : ↥H<VAR>K : ℕ →o Submodule R ↥H := { toFun := fun n => LinearMap.ker ((ad R ↥H) x ^ n), monotone' := ⋯ }<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → K n = K m<GOAL>_root_.IsNilpotent ((ad R ↥H) x)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : IsNoetherian R L<VAR>H : LieSubalgebra R L<VAR>h : ∀ x ∈ H, H ≤ engel R x<VAR>x : ↥H<VAR>K : ℕ →o Submodule R ↥H := { toFun := fun n => LinearMap.ker ((ad R ↥H) x ^ n), monotone' := ⋯ }<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → K n = K m<GOAL>(ad R ↥H) x ^ n = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : IsNoetherian R L<VAR>H : LieSubalgebra R L<VAR>h : ∀ x ∈ H, H ≤ engel R x<VAR>x : ↥H<VAR>K : ℕ →o Submodule R ↥H := { toFun := fun n => LinearMap.ker ((ad R ↥H) x ^ n), monotone' := ⋯ }<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → K n = K m<VAR>y : ↥H<GOAL>↑(((ad R ↥H) x ^ n) y) = ↑(0 y)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : IsNoetherian R L<VAR>H : LieSubalgebra R L<VAR>h : ∀ x ∈ H, H ≤ engel R x<VAR>x : ↥H<VAR>K : ℕ →o Submodule R ↥H := { toFun := fun n => LinearMap.ker ((ad R ↥H) x ^ n), monotone' := ⋯ }<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → K n = K m<VAR>y : ↥H<GOAL>((ad R L) ↑x ^ n) ↑y = ↑(0 y)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : IsNoetherian R L<VAR>H : LieSubalgebra R L<VAR>x : ↥H<VAR>K : ℕ →o Submodule R ↥H := { toFun := fun n => LinearMap.ker ((ad R ↥H) x ^ n), monotone' := ⋯ }<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → K n = K m<VAR>y : ↥H<VAR>h : ↑y ∈ engel R ↑x<GOAL>((ad R L) ↑x ^ n) ↑y = ↑(0 y)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : IsNoetherian R L<VAR>H : LieSubalgebra R L<VAR>x : ↥H<VAR>K : ℕ →o Submodule R ↥H := { toFun := fun n => LinearMap.ker ((ad R ↥H) x ^ n), monotone' := ⋯ }<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → K n = K m<VAR>y : ↥H<VAR>h : ∃ n, ((ad R L) ↑x ^ n) ↑y = 0<GOAL>((ad R L) ↑x ^ n) ↑y = ↑(0 y)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : IsNoetherian R L<VAR>H : LieSubalgebra R L<VAR>x : ↥H<VAR>K : ℕ →o Submodule R ↥H := { toFun := fun n => LinearMap.ker ((ad R ↥H) x ^ n), monotone' := ⋯ }<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → K n = K m<VAR>y : ↥H<VAR>m : ℕ<VAR>hm : ((ad R L) ↑x ^ m) ↑y = 0<GOAL>((ad R L) ↑x ^ n) ↑y = ↑(0 y)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : IsNoetherian R L<VAR>H : LieSubalgebra R L<VAR>x : ↥H<VAR>K : ℕ →o Submodule R ↥H := { toFun := fun n => LinearMap.ker ((ad R ↥H) x ^ n), monotone' := ⋯ }<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → K n = K m<VAR>y : ↥H<VAR>m : ℕ<VAR>hm : ((ad R L) ↑x ^ m) ↑y = 0<VAR>hmn : m ≤ n<GOAL>((ad R L) ↑x ^ n) ↑y = ↑(0 y)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : IsNoetherian R L<VAR>H : LieSubalgebra R L<VAR>x : ↥H<VAR>K : ℕ →o Submodule R ↥H := { toFun := fun n => LinearMap.ker ((ad R ↥H) x ^ n), monotone' := ⋯ }<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → K n = K m<VAR>y : ↥H<VAR>m : ℕ<VAR>hm : ((ad R L) ↑x ^ m) ↑y = 0<VAR>hmn : n ≤ m<GOAL>((ad R L) ↑x ^ n) ↑y = ↑(0 y)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁵ : OrderedCommSemiring R<VAR>inst✝¹⁴ : StarRing R<VAR>inst✝¹³ : StarOrderedRing R<VAR>inst✝¹² : MetricSpace R<VAR>inst✝¹¹ : TopologicalSemiring R<VAR>inst✝¹⁰ : ContinuousStar R<VAR>inst✝⁹ : ∀ (α : Type ?u.815889) [inst : TopologicalSpace α], StarOrderedRing C(α, R)<VAR>inst✝⁸ : TopologicalSpace A<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : PartialOrder A<VAR>inst✝⁴ : StarOrderedRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : StarModule R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>inst✝ : NonnegSpectrumClass R A<VAR>f : R → R<VAR>a : A<VAR>h : ∀ x ∈ spectrum R a, 1 ≤ f x<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>1 ≤ cfc f a
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n✝ : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x : 𝕎 R<VAR>n : ℕ<GOAL>init n (init n x) = init n x
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n✝ : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x : 𝕎 R<VAR>n : ℕ<GOAL>∀ (n_1 : ℕ), (init n (init n x)).coeff n_1 = (init n x).coeff n_1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n✝ : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x : 𝕎 R<VAR>n i : ℕ<GOAL>(init n (init n x)).coeff i = (init n x).coeff i
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n✝ : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x : 𝕎 R<VAR>n i : ℕ<GOAL>(if i < n then if i < n then x.coeff i else 0 else 0) = if i < n then x.coeff i else 0
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : UniformSpace K<VAR>inst✝ : CompletableTopField K<VAR>x : hat K<VAR>h : x ≠ 0<GOAL>ContinuousAt hatInv x
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : UniformSpace K<VAR>inst✝ : CompletableTopField K<VAR>x : hat K<VAR>h : x ≠ 0<GOAL>∀ᶠ (x : hat K) in 𝓝 x, ∃ c, Tendsto (fun x => ↑K x⁻¹) (Filter.comap (↑K) (𝓝 x)) (𝓝 c)
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : UniformSpace K<VAR>inst✝ : CompletableTopField K<VAR>x : hat K<VAR>h : x ≠ 0<GOAL>{0}ᶜ ⊆ {x | (fun x => ∃ c, Tendsto (fun x => ↑K x⁻¹) (Filter.comap (↑K) (𝓝 x)) (𝓝 c)) x}
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : UniformSpace K<VAR>inst✝ : CompletableTopField K<VAR>x : hat K<VAR>h : x ≠ 0<VAR>y : hat K<VAR>y_ne : y ∈ {0}ᶜ<GOAL>y ∈ {x | (fun x => ∃ c, Tendsto (fun x => ↑K x⁻¹) (Filter.comap (↑K) (𝓝 x)) (𝓝 c)) x}
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : UniformSpace K<VAR>inst✝ : CompletableTopField K<VAR>x : hat K<VAR>h : x ≠ 0<VAR>y : hat K<VAR>y_ne : y ≠ 0<GOAL>y ∈ {x | (fun x => ∃ c, Tendsto (fun x => ↑K x⁻¹) (Filter.comap (↑K) (𝓝 x)) (𝓝 c)) x}
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : UniformSpace K<VAR>inst✝ : CompletableTopField K<VAR>x : hat K<VAR>h : x ≠ 0<VAR>y : hat K<VAR>y_ne : y ≠ 0<GOAL>Cauchy (map (fun x => ↑K x⁻¹) (Filter.comap (↑K) (𝓝 y)))
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : UniformSpace K<VAR>inst✝ : CompletableTopField K<VAR>x : hat K<VAR>h : x ≠ 0<VAR>y : hat K<VAR>y_ne : y ≠ 0<VAR>this : (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹<GOAL>Cauchy (map (fun x => ↑K x⁻¹) (Filter.comap (↑K) (𝓝 y)))
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : UniformSpace K<VAR>inst✝ : CompletableTopField K<VAR>x : hat K<VAR>h : x ≠ 0<VAR>y : hat K<VAR>y_ne : y ≠ 0<VAR>this : (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹<GOAL>Cauchy (map (fun y => ↑K y) (map (fun x => x⁻¹) (Filter.comap (↑K) (𝓝 y))))
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : UniformSpace K<VAR>inst✝ : CompletableTopField K<VAR>x : hat K<VAR>h : x ≠ 0<VAR>y : hat K<VAR>y_ne : y ≠ 0<VAR>this : (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹<GOAL>Cauchy (map (fun x => x⁻¹) (Filter.comap (↑K) (𝓝 y)))
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : UniformSpace K<VAR>inst✝ : CompletableTopField K<VAR>x : hat K<VAR>h : x ≠ 0<VAR>y : hat K<VAR>y_ne : y ≠ 0<VAR>this : (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹<GOAL>Cauchy (Filter.comap (↑K) (𝓝 y))
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : UniformSpace K<VAR>inst✝ : CompletableTopField K<VAR>x : hat K<VAR>h : x ≠ 0<VAR>y : hat K<VAR>y_ne : y ≠ 0<VAR>this : (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹<GOAL>𝓝 0 ⊓ Filter.comap (↑K) (𝓝 y) = ⊥
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : Archimedean α<VAR>a : α<GOAL>⋃ n, Icc (↑n) (↑n + 1) = univ
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>inst✝³ : Monoid M<VAR>inst✝² : Preorder M<VAR>inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>x : M<VAR>inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a : M<VAR>n m : ℕ<VAR>ha : 1 < a<VAR>h : n < m<GOAL>a ^ n < a ^ m
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>inst✝³ : Monoid M<VAR>inst✝² : Preorder M<VAR>inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>x : M<VAR>inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a : M<VAR>n : ℕ<VAR>ha : 1 < a<VAR>k : ℕ<VAR>h : n < n.succ + k<GOAL>a ^ n < a ^ (n.succ + k)
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>inst✝³ : Monoid M<VAR>inst✝² : Preorder M<VAR>inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>x : M<VAR>inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a : M<VAR>n : ℕ<VAR>ha : 1 < a<VAR>k : ℕ<GOAL>a ^ n < a ^ (n.succ + k)
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>inst✝³ : Monoid M<VAR>inst✝² : Preorder M<VAR>inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>x : M<VAR>inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a : M<VAR>n : ℕ<VAR>ha : 1 < a<VAR>k : ℕ<GOAL>a ^ n < a ^ n * a ^ (k + 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>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>c : F<GOAL>DifferentiableWithinAt 𝕜 (fun y => c - f y) s x ↔ DifferentiableWithinAt 𝕜 f s x
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : Ring R<VAR>φ : MvPowerSeries σ R<VAR>u : Rˣ<VAR>h : (constantCoeff σ R) φ = ↑u<VAR>n : σ →₀ ℕ<VAR>this : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)<VAR>H : n = 0<GOAL>(coeff R 0) (φ * φ.invOfUnit u) = (coeff R 0) 1
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>p : Perm α<VAR>x y : α<VAR>H : p.toList x = [y]<GOAL>False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>n m✝ : ℕ<VAR>hf : HasFiniteFPowerSeriesOnBall f pf x n r<VAR>m : ℕ<VAR>hm : n ≤ m<GOAL>(-pf) m = 0
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f✝ g✝ : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>β : Type u_2<VAR>β' : Type u_3<VAR>mβ : MeasurableSpace β<VAR>mβ' : MeasurableSpace β'<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>hfm : Measurable f<VAR>hgm : Measurable g<GOAL>IndepFun f g μ ↔ ∀ {φ : β → ℝ} {ψ : β' → ℝ}, Measurable φ → Measurable ψ → Integrable (φ ∘ f) μ → Integrable (ψ ∘ g) μ → integral μ (φ ∘ f * ψ ∘ g) = integral μ (φ ∘ f) * integral μ (ψ ∘ g)
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f✝ g✝ : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>β : Type u_2<VAR>β' : Type u_3<VAR>mβ : MeasurableSpace β<VAR>mβ' : MeasurableSpace β'<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>hfm : Measurable f<VAR>hgm : Measurable g<GOAL>(∀ {φ : β → ℝ} {ψ : β' → ℝ}, Measurable φ → Measurable ψ → Integrable (φ ∘ f) μ → Integrable (ψ ∘ g) μ → integral μ (φ ∘ f * ψ ∘ g) = integral μ (φ ∘ f) * integral μ (ψ ∘ g)) → IndepFun f g μ
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f✝ g✝ : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>β : Type u_2<VAR>β' : Type u_3<VAR>mβ : MeasurableSpace β<VAR>mβ' : MeasurableSpace β'<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>hfm : Measurable f<VAR>hgm : Measurable g<GOAL>(∀ {φ : β → ℝ} {ψ : β' → ℝ}, Measurable φ → Measurable ψ → Integrable (φ ∘ f) μ → Integrable (ψ ∘ g) μ → integral μ (φ ∘ f * ψ ∘ g) = integral μ (φ ∘ f) * integral μ (ψ ∘ g)) → ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → μ (t1 ∩ t2) = μ t1 * μ t2
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f✝ g✝ : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>β : Type u_2<VAR>β' : Type u_3<VAR>mβ : MeasurableSpace β<VAR>mβ' : MeasurableSpace β'<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>hfm : Measurable f<VAR>hgm : Measurable g<VAR>h : ∀ {φ : β → ℝ} {ψ : β' → ℝ}, Measurable φ → Measurable ψ → Integrable (φ ∘ f) μ → Integrable (ψ ∘ g) μ → integral μ (φ ∘ f * ψ ∘ g) = integral μ (φ ∘ f) * integral μ (ψ ∘ g)<VAR>A : Set β<VAR>hA : MeasurableSet A<VAR>B : Set β'<VAR>hB : MeasurableSet B<GOAL>μ (f ⁻¹' A ∩ g ⁻¹' B) = μ (f ⁻¹' A) * μ (g ⁻¹' B)
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f✝ g✝ : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>β : Type u_2<VAR>β' : Type u_3<VAR>mβ : MeasurableSpace β<VAR>mβ' : MeasurableSpace β'<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>hfm : Measurable f<VAR>hgm : Measurable g<VAR>A : Set β<VAR>hA : MeasurableSet A<VAR>B : Set β'<VAR>hB : MeasurableSet B<VAR>h : integral μ (A.indicator 1 ∘ f * B.indicator 1 ∘ g) = integral μ (A.indicator 1 ∘ f) * integral μ (B.indicator 1 ∘ g)<GOAL>μ (f ⁻¹' A ∩ g ⁻¹' B) = μ (f ⁻¹' A) * μ (g ⁻¹' B)
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f✝ g✝ : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>β : Type u_2<VAR>β' : Type u_3<VAR>mβ : MeasurableSpace β<VAR>mβ' : MeasurableSpace β'<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>hfm : Measurable f<VAR>hgm : Measurable g<VAR>A : Set β<VAR>hA : MeasurableSet A<VAR>B : Set β'<VAR>hB : MeasurableSet B<VAR>h : integral μ (A.indicator 1 ∘ f * B.indicator 1 ∘ g) = integral μ (A.indicator 1 ∘ f) * integral μ (B.indicator 1 ∘ g)<GOAL>μ (f ⁻¹' A) * μ (g ⁻¹' B) ≠ ⊤
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁵ : Fintype l<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>inst✝² : Unique ι<VAR>inst✝¹ : SeminormedAddCommGroup α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>A : Matrix m n α<VAR>f : α → β<VAR>hf : ∀ (a : α), ‖f a‖₊ = ‖a‖₊<GOAL>‖A.map f‖₊ = ‖A‖₊
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>f : X → Y<VAR>s : Set X<VAR>hf : ContinuousOn f s<VAR>K : ℕ → Set X<VAR>hcompact : ∀ (n : ℕ), IsCompact (K n)<VAR>hcov : ⋃ n, K n = s<GOAL>IsSigmaCompact (f '' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>f : X → Y<VAR>s : Set X<VAR>hf : ContinuousOn f s<VAR>K : ℕ → Set X<VAR>hcompact : ∀ (n : ℕ), IsCompact (K n)<VAR>hcov : ⋃ n, K n = s<GOAL>∀ (n : ℕ), IsCompact ((fun n => f '' K n) n)
<VAR>α : Type u_1<VAR>s : Cycle α<VAR>h : s.Subsingleton<GOAL>∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y
<VAR>α : Type u_1<VAR>l : List α<VAR>h : Subsingleton (Quot.mk Setoid.r l)<GOAL>∀ ⦃x : α⦄, x ∈ Quot.mk Setoid.r l → ∀ ⦃y : α⦄, y ∈ Quot.mk Setoid.r l → x = y
<VAR>α : Type u_1<VAR>l : List α<VAR>h : l = [] ∨ ∃ a, l = [a]<GOAL>∀ ⦃x : α⦄, x ∈ Quot.mk Setoid.r l → ∀ ⦃y : α⦄, y ∈ Quot.mk Setoid.r l → x = y
<VAR>Γ : Type u_1<VAR>inst✝ : Inhabited Γ<VAR>l : ListBlank Γ<GOAL>l.nth 0 = l.head
<VAR>Γ : Type u_1<VAR>inst✝ : Inhabited Γ<VAR>l : ListBlank Γ<GOAL>(cons l.head l.tail).nth 0 = l.head
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f g : α → ℂ<VAR>hl : IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => |(g x).im|<GOAL>(let_fun this := fun x => abs (f x) ^ (g x).re / 1; this) =ᶠ[l] let_fun this := fun x => abs (f x) ^ (g x).re; this
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f g : α → ℂ<VAR>hl : IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => |(g x).im|<GOAL>(fun x => abs (f x) ^ (g x).re) =ᶠ[l] fun x => abs (f x) ^ (g x).re
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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 uX<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>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : ContDiffWithinAt 𝕜 n f s x<VAR>hx : s ∈ 𝓝 x<GOAL>ContDiffAt 𝕜 n f x
<VAR>α : Type u<VAR>f g : MonoOver α<VAR>t : f ⟶ g<VAR>x : (𝟭 (Type u)).obj f.obj.left<GOAL>f.obj.hom x ∈ (fun f => Set.range f.obj.hom) g
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : NormedLinearOrderedField 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : StrictConvexSpace ℝ E<VAR>x y z : E<VAR>a b r : ℝ<VAR>h : ¬SameRay ℝ x y<GOAL>‖x‖ - ‖y‖ < ‖x - y‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : NormedLinearOrderedField 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : StrictConvexSpace ℝ E<VAR>x y z : E<VAR>a b r : ℝ<VAR>h : ¬SameRay ℝ (x - y + y) y<GOAL>‖x - y + y‖ - ‖y‖ < ‖x - y‖