ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α✝ β✝ : Weight K (↥H) L<VAR>hα : α✝.IsNonZero<VAR>α β : { α // α.IsNonZero }<VAR>u : K<VAR>hu : u • Weight.toLinear K (↥H) L ↑α = Weight.toLinear K (↥H) L ↑β<VAR>h : ↑β = ↑α<GOAL>(rootSystem H).root α = (rootSystem H).root β ∨ (rootSystem H).root α = -(rootSystem H).root β
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>E : B → Type u_5<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : (x : B) → TopologicalSpace (E x)<VAR>a : FiberPrebundle F E<VAR>e✝ e e' : Pretrivialization F TotalSpace.proj<VAR>he' : e' ∈ a.pretrivializationAtlas<VAR>this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology<GOAL>IsOpen (e'.target ∩ ↑e'.symm ⁻¹' e.source)
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>E : B → Type u_5<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : (x : B) → TopologicalSpace (E x)<VAR>a : FiberPrebundle F E<VAR>e✝ e e' : Pretrivialization F TotalSpace.proj<VAR>he' : e' ∈ a.pretrivializationAtlas<VAR>this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology<VAR>u : Set (B × F)<VAR>hu1 : IsOpen u<VAR>hu2 : ↑e'.symm ⁻¹' e.source ∩ e'.target = u ∩ e'.target<GOAL>IsOpen (e'.target ∩ ↑e'.symm ⁻¹' e.source)
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>E : B → Type u_5<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : (x : B) → TopologicalSpace (E x)<VAR>a : FiberPrebundle F E<VAR>e✝ e e' : Pretrivialization F TotalSpace.proj<VAR>he' : e' ∈ a.pretrivializationAtlas<VAR>this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology<VAR>u : Set (B × F)<VAR>hu1 : IsOpen u<VAR>hu2 : ↑e'.symm ⁻¹' e.source ∩ e'.target = u ∩ e'.target<GOAL>IsOpen (u ∩ e'.target)
<VAR>p✝ : ℕ<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>p : ℕ<VAR>inst✝² : Fact (Nat.Prime p)<VAR>N : Subgroup G<VAR>inst✝¹ : N.Normal<VAR>inst✝ : Finite (Sylow p ↥N)<VAR>P : Sylow p ↥N<GOAL>(map N.subtype ↑P).normalizer ⊔ N = ⊤
<VAR>p✝ : ℕ<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>p : ℕ<VAR>inst✝² : Fact (Nat.Prime p)<VAR>N : Subgroup G<VAR>inst✝¹ : N.Normal<VAR>inst✝ : Finite (Sylow p ↥N)<VAR>P : Sylow p ↥N<VAR>g : G<VAR>x✝ : g ∈ ⊤<GOAL>g ∈ (map N.subtype ↑P).normalizer ⊔ N
<VAR>p✝ : ℕ<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>p : ℕ<VAR>inst✝² : Fact (Nat.Prime p)<VAR>N : Subgroup G<VAR>inst✝¹ : N.Normal<VAR>inst✝ : Finite (Sylow p ↥N)<VAR>P : Sylow p ↥N<VAR>g : G<VAR>x✝ : g ∈ ⊤<VAR>n : ↥N<VAR>hn : n • MulAut.conjNormal g • P = P<GOAL>g ∈ (map N.subtype ↑P).normalizer ⊔ N
<VAR>p✝ : ℕ<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>p : ℕ<VAR>inst✝² : Fact (Nat.Prime p)<VAR>N : Subgroup G<VAR>inst✝¹ : N.Normal<VAR>inst✝ : Finite (Sylow p ↥N)<VAR>P : Sylow p ↥N<VAR>g : G<VAR>x✝ : g ∈ ⊤<VAR>n : ↥N<VAR>hn : n • MulAut.conjNormal g • P = P<GOAL>(↑n)⁻¹ * (↑n * g) ∈ N ⊔ (map N.subtype ↑P).normalizer
<VAR>p✝ : ℕ<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>p : ℕ<VAR>inst✝² : Fact (Nat.Prime p)<VAR>N : Subgroup G<VAR>inst✝¹ : N.Normal<VAR>inst✝ : Finite (Sylow p ↥N)<VAR>P : Sylow p ↥N<VAR>g : G<VAR>x✝ : g ∈ ⊤<VAR>n : ↥N<VAR>hn : n • MulAut.conjNormal g • P = P<GOAL>↑n * g ∈ (map N.subtype ↑P).normalizer
<VAR>p✝ : ℕ<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>p : ℕ<VAR>inst✝² : Fact (Nat.Prime p)<VAR>N : Subgroup G<VAR>inst✝¹ : N.Normal<VAR>inst✝ : Finite (Sylow p ↥N)<VAR>P : Sylow p ↥N<VAR>g : G<VAR>x✝ : g ∈ ⊤<VAR>n : ↥N<VAR>hn : map ((MulDistribMulAction.toMonoidEnd (MulAut ↥N) ↥N) (MulAut.conjNormal (↑n * g))) ↑P = ↑P<GOAL>↑n * g ∈ (map N.subtype ↑P).normalizer
<VAR>p✝ : ℕ<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>p : ℕ<VAR>inst✝² : Fact (Nat.Prime p)<VAR>N : Subgroup G<VAR>inst✝¹ : N.Normal<VAR>inst✝ : Finite (Sylow p ↥N)<VAR>P : Sylow p ↥N<VAR>g : G<VAR>x✝ : g ∈ ⊤<VAR>n : ↥N<VAR>hn : map ((MulDistribMulAction.toMonoidEnd (MulAut ↥N) ↥N) (MulAut.conjNormal (↑n * g))) ↑P = ↑P<VAR>this : Function.Injective ⇑(MulEquiv.toMonoidHom (MulAut.conj (↑n * g)))<GOAL>↑n * g ∈ (map N.subtype ↑P).normalizer
<VAR>p✝ : ℕ<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>p : ℕ<VAR>inst✝² : Fact (Nat.Prime p)<VAR>N : Subgroup G<VAR>inst✝¹ : N.Normal<VAR>inst✝ : Finite (Sylow p ↥N)<VAR>P : Sylow p ↥N<VAR>g : G<VAR>x✝ : g ∈ ⊤<VAR>n : ↥N<VAR>hn : map ((MulDistribMulAction.toMonoidEnd (MulAut ↥N) ↥N) (MulAut.conjNormal (↑n * g))) ↑P = ↑P<VAR>this : Function.Injective ⇑(MulEquiv.toMonoidHom (MulAut.conj (↑n * g)))<VAR>x : G<GOAL>(MulEquiv.toMonoidHom (MulAut.conj (↑n * g))) x ∈ map (MulEquiv.toMonoidHom (MulAut.conj (↑n * g))) (map N.subtype ↑P) ↔ ↑n * g * x * (↑n * g)⁻¹ ∈ map N.subtype ↑P
<VAR>p✝ : ℕ<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>p : ℕ<VAR>inst✝² : Fact (Nat.Prime p)<VAR>N : Subgroup G<VAR>inst✝¹ : N.Normal<VAR>inst✝ : Finite (Sylow p ↥N)<VAR>P : Sylow p ↥N<VAR>g : G<VAR>x✝ : g ∈ ⊤<VAR>n : ↥N<VAR>hn : map ((MulDistribMulAction.toMonoidEnd (MulAut ↥N) ↥N) (MulAut.conjNormal (↑n * g))) ↑P = ↑P<VAR>this : Function.Injective ⇑(MulEquiv.toMonoidHom (MulAut.conj (↑n * g)))<VAR>x : G<GOAL>(MulEquiv.toMonoidHom (MulAut.conj (↑n * g))) x ∈ map ((MulEquiv.toMonoidHom (MulAut.conj (↑n * g))).comp N.subtype) ↑P ↔ ↑n * g * x * (↑n * g)⁻¹ ∈ map (N.subtype.comp ((MulDistribMulAction.toMonoidEnd (MulAut ↥N) ↥N) (MulAut.conjNormal (↑n * g)))) ↑P
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>s : Set E<VAR>x : E<VAR>hs : s ∈ 𝓝 x<GOAL>∃ f, tsupport f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ⊤ f ∧ range f ⊆ Icc 0 1 ∧ f x = 1
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>s : Set E<VAR>x : E<VAR>hs : s ∈ 𝓝 x<VAR>d : ℝ<VAR>d_pos : 0 < d<VAR>hd : Euclidean.closedBall x d ⊆ s<GOAL>∃ f, tsupport f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ⊤ f ∧ range f ⊆ Icc 0 1 ∧ f x = 1
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>s : Set E<VAR>x : E<VAR>hs : s ∈ 𝓝 x<VAR>d : ℝ<VAR>d_pos : 0 < d<VAR>hd : Euclidean.closedBall x d ⊆ s<VAR>c : ContDiffBump (toEuclidean x) := { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }<GOAL>∃ f, tsupport f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ⊤ f ∧ range f ⊆ Icc 0 1 ∧ f x = 1
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>s : Set E<VAR>x : E<VAR>hs : s ∈ 𝓝 x<VAR>d : ℝ<VAR>d_pos : 0 < d<VAR>hd : Euclidean.closedBall x d ⊆ s<VAR>c : ContDiffBump (toEuclidean x) := { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }<VAR>f : E → ℝ := ↑c ∘ ⇑toEuclidean<GOAL>∃ f, tsupport f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ⊤ f ∧ range f ⊆ Icc 0 1 ∧ f x = 1
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>s : Set E<VAR>x : E<VAR>hs : s ∈ 𝓝 x<VAR>d : ℝ<VAR>d_pos : 0 < d<VAR>hd : Euclidean.closedBall x d ⊆ s<VAR>c : ContDiffBump (toEuclidean x) := { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }<VAR>f : E → ℝ := ↑c ∘ ⇑toEuclidean<VAR>f_supp : support f ⊆ Euclidean.ball x d<GOAL>∃ f, tsupport f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ⊤ f ∧ range f ⊆ Icc 0 1 ∧ f x = 1
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>s : Set E<VAR>x : E<VAR>hs : s ∈ 𝓝 x<VAR>d : ℝ<VAR>d_pos : 0 < d<VAR>hd : Euclidean.closedBall x d ⊆ s<VAR>c : ContDiffBump (toEuclidean x) := { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }<VAR>f : E → ℝ := ↑c ∘ ⇑toEuclidean<VAR>f_supp : support f ⊆ Euclidean.ball x d<VAR>f_tsupp : tsupport f ⊆ Euclidean.closedBall x d<GOAL>∃ f, tsupport f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ⊤ f ∧ range f ⊆ Icc 0 1 ∧ f x = 1
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q✝ : ℕ<VAR>q p : R[X]<VAR>hp : (q * q * p).Separable<GOAL>IsUnit q
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q✝ : ℕ<VAR>q p : R[X]<VAR>hp : (q * q * p).Separable<GOAL>IsCoprime q q
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q✝ : ℕ<VAR>q p : R[X]<VAR>hp : (q * q * p).Separable<VAR>this : IsCoprime (q * (q * p)) (q * (derivative q * p + derivative q * p + q * derivative p))<GOAL>IsCoprime q q
<VAR>R : Type u_1<VAR>inst✝⁵ : CommSemiring R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>ι : Type u_4<VAR>inst✝ : DecidableEq ι<VAR>m : M<VAR>p : ι →₀ N<GOAL>(finsuppRight R M N ι) (m ⊗ₜ[R] p) = p.sum fun i n => Finsupp.single i (m ⊗ₜ[R] n)
<VAR>R : Type u_1<VAR>inst✝⁵ : CommSemiring R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>ι : Type u_4<VAR>inst✝ : DecidableEq ι<VAR>m : M<VAR>p : ι →₀ N<GOAL>(finsuppRight R M N ι) (m ⊗ₜ[R] 0) = Finsupp.sum 0 fun i n => Finsupp.single i (m ⊗ₜ[R] n)
<VAR>R : Type u_1<VAR>inst✝⁵ : CommSemiring R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>ι : Type u_4<VAR>inst✝ : DecidableEq ι<VAR>m : M<VAR>p : ι →₀ N<GOAL>∀ (f g : ι →₀ N), ((finsuppRight R M N ι) (m ⊗ₜ[R] f) = f.sum fun i n => Finsupp.single i (m ⊗ₜ[R] n)) → ((finsuppRight R M N ι) (m ⊗ₜ[R] g) = g.sum fun i n => Finsupp.single i (m ⊗ₜ[R] n)) → (finsuppRight R M N ι) (m ⊗ₜ[R] (f + g)) = (f + g).sum fun i n => Finsupp.single i (m ⊗ₜ[R] n)
<VAR>R : Type u_1<VAR>inst✝⁵ : CommSemiring R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>ι : Type u_4<VAR>inst✝ : DecidableEq ι<VAR>m : M<VAR>p : ι →₀ N<GOAL>∀ (a : ι) (b : N), (finsuppRight R M N ι) (m ⊗ₜ[R] Finsupp.single a b) = (Finsupp.single a b).sum fun i n => Finsupp.single i (m ⊗ₜ[R] n)
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n → α<VAR>a : α<GOAL>a ∈ ofFn f ↔ a ∈ Set.range f
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n → α<VAR>a : α<GOAL>(∃ n_1, f (Fin.cast ⋯ n_1) = a) ↔ ∃ y, f y = a
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>x : RelSeries r<GOAL>List.Chain' r x.toList
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>x : RelSeries r<GOAL>∀ (i : ℕ) (h : i < x.toList.length - 1), r (x.toList.get ⟨i, ⋯⟩) (x.toList.get ⟨i + 1, ⋯⟩)
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>x : RelSeries r<VAR>i : ℕ<VAR>h : i < x.toList.length - 1<GOAL>r (x.toList.get ⟨i, ⋯⟩) (x.toList.get ⟨i + 1, ⋯⟩)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K : ℝ≥0<VAR>f : α → β<VAR>x y : α<VAR>r : ℝ≥0∞<VAR>a : α<GOAL>LipschitzWith 1 (Prod.mk a)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsReflexive R M<VAR>e : N ≃ₗ[R] Dual R M<GOAL>Bijective ⇑(Dual.eval R N)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsReflexive R M<VAR>e : N ≃ₗ[R] Dual R M<GOAL>Bijective ⇑↑(e ≪≫ₗ e.flip.symm.dualMap)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>hr : 0 < r<GOAL>Tendsto (fun x => f x * r) l atBot ↔ Tendsto f l atBot
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>ha : ¬IsUnit a<VAR>hb : IsUnit b<GOAL>a ^ 0 ∣ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>ha : ¬IsUnit a<VAR>hb : IsUnit b<GOAL>¬a ^ (0 + 1) ∣ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>ha : ¬IsUnit a<VAR>hb : IsUnit b<GOAL>¬a ∣ b
<VAR>Γ✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ✝<VAR>inst✝¹ : AddMonoid R<VAR>Γ : Type u_3<VAR>inst✝ : LinearOrder Γ<VAR>x y : HahnSeries Γ R<VAR>hxy : y.orderTop < x.orderTop<GOAL>(x + y).orderTop = y.orderTop
<VAR>R : Type u_1<VAR>inst✝⁶ : Semiring R<VAR>p✝ : R[X]<VAR>r : R<VAR>p q : R[X]<VAR>S : Type u_2<VAR>inst✝⁵ : NonAssocSemiring S<VAR>inst✝⁴ : Module R S<VAR>inst✝³ : IsScalarTower R S S<VAR>inst✝² : SMulCommClass R S S<VAR>inst✝¹ : Pow S ℕ<VAR>inst✝ : NatPowAssoc S<VAR>x : S<GOAL>(p.comp q).smeval x = p.smeval (q.smeval x)
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace 𝕜 E'<VAR>f : E → E'<VAR>s : Set E<VAR>x : E<GOAL>mfderiv 𝓘(𝕜, E) 𝓘(𝕜, E') f x = fderiv 𝕜 f x
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace 𝕜 E'<VAR>f : E → E'<VAR>s : Set E<VAR>x : E<GOAL>mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f Set.univ x = fderivWithin 𝕜 f Set.univ x
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ inst✝ : NumberField K<VAR>x : (𝓞 K)ˣ<VAR>ζ : (𝓞 K)ˣ := x * (∏ i : Fin (rank K), fundSystem K i ^ ((basisModTorsion K).repr (Additive.ofMul ↑x)) i)⁻¹<GOAL>∃! ζe, x = ↑ζe.1 * ∏ i : Fin (rank K), fundSystem K i ^ ζe.2 i
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ inst✝ : NumberField K<VAR>x : (𝓞 K)ˣ<VAR>ζ : (𝓞 K)ˣ := x * (∏ i : Fin (rank K), fundSystem K i ^ ((basisModTorsion K).repr (Additive.ofMul ↑x)) i)⁻¹<VAR>h_tors : ζ ∈ torsion K<GOAL>∃! ζe, x = ↑ζe.1 * ∏ i : Fin (rank K), fundSystem K i ^ ζe.2 i
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : Fintype α<VAR>s✝ t✝ : Finset α<VAR>a b : α<VAR>s t : Finset α<VAR>h : _root_.Disjoint s t<GOAL>(s.disjUnion t h).dens = s.dens + t.dens
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁶ : SeminormedAddCommGroup E<VAR>inst✝¹⁵ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁴ : SeminormedAddCommGroup F<VAR>inst✝¹³ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹² : SeminormedAddCommGroup G<VAR>inst✝¹¹ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁵ : NormedSpace 𝕜₂ F<VAR>inst✝⁴ : NormedSpace 𝕜 Fₗ<VAR>inst✝³ : NormedSpace 𝕜₃ G<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝¹ : FunLike 𝓕 E F<VAR>inst✝ : SemilinearMapClass 𝓕 σ₁₂ E F<VAR>f : 𝓕<VAR>hf : Continuous ⇑f<VAR>x : E<VAR>hx : ‖x‖ = 0<GOAL>‖f x‖ = 0
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁶ : SeminormedAddCommGroup E<VAR>inst✝¹⁵ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁴ : SeminormedAddCommGroup F<VAR>inst✝¹³ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹² : SeminormedAddCommGroup G<VAR>inst✝¹¹ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁵ : NormedSpace 𝕜₂ F<VAR>inst✝⁴ : NormedSpace 𝕜 Fₗ<VAR>inst✝³ : NormedSpace 𝕜₃ G<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝¹ : FunLike 𝓕 E F<VAR>inst✝ : SemilinearMapClass 𝓕 σ₁₂ E F<VAR>f : 𝓕<VAR>hf : Continuous ⇑f<VAR>x : E<VAR>hx : 0 ⤳ x<GOAL>f 0 ⤳ f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h₁ : c < b<VAR>x : α<GOAL>x ∈ Ioo a b ∪ Ioi c ↔ x ∈ Ioi (min a c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h₁ : c < b<VAR>x : α<GOAL>a < x ∧ x < b ∨ c < x ↔ a < x ∨ c < x
<VAR>α : Type u<VAR>inst✝² : UniformSpace α<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>s : Set (α × α)<VAR>x✝ : α × α<VAR>a₁ a₂ : α<GOAL>(a₁, a₂) ∈ ((preimage fun x => (pureCauchy x.1, pureCauchy x.2)) ∘ gen) s ↔ (a₁, a₂) ∈ id s
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<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✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>H : LieSubalgebra R L<VAR>x : L<GOAL>x ∈ H.normalizer ↔ ∀ y ∈ H, ⁅x, y⁆ ∈ H
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<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✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>H : LieSubalgebra R L<VAR>x : L<GOAL>(∀ y ∈ H, ⁅y, x⁆ ∈ H) ↔ ∀ y ∈ H, ⁅x, y⁆ ∈ H
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<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✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>H : LieSubalgebra R L<VAR>x y : L<VAR>hy : y ∈ H<GOAL>⁅y, x⁆ ∈ H ↔ ⁅x, y⁆ ∈ H
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : Zero α<VAR>inst✝² : Zero β<VAR>inst✝¹ : SMulWithZero α β<VAR>inst✝ : DecidableEq β<VAR>s✝ : Finset α<VAR>t s : Finset β<VAR>h : s.Nonempty<GOAL>↑(0 • s) = ↑0
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>x : M<GOAL>x ∈ N ⊓ N' ↔ x ∈ N ∧ x ∈ N'
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x✝ : E<VAR>inst✝ : l.NeBot<VAR>hf' : TendstoUniformly f' g' l<VAR>hf✝ : ∀ (n : ι) (x : E), HasFDerivAt (f n) (f' n x) x<VAR>hfg✝ : ∀ (x : E), Tendsto (fun n => f n x) l (𝓝 (g x))<VAR>x : E<VAR>hf : ∀ (n : ι), ∀ x ∈ Set.univ, HasFDerivAt (f n) (f' n x) x<VAR>hfg : ∀ x ∈ Set.univ, Tendsto (fun n => f n x) l (𝓝 (g x))<GOAL>HasFDerivAt g (g' x) x
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x✝ : E<VAR>inst✝ : l.NeBot<VAR>hf'✝ : TendstoUniformly f' g' l<VAR>hf✝ : ∀ (n : ι) (x : E), HasFDerivAt (f n) (f' n x) x<VAR>hfg✝ : ∀ (x : E), Tendsto (fun n => f n x) l (𝓝 (g x))<VAR>x : E<VAR>hf : ∀ (n : ι), ∀ x ∈ Set.univ, HasFDerivAt (f n) (f' n x) x<VAR>hfg : ∀ x ∈ Set.univ, Tendsto (fun n => f n x) l (𝓝 (g x))<VAR>hf' : TendstoUniformlyOn f' g' l Set.univ<GOAL>HasFDerivAt g (g' x) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>h : l.HasBasis p s<VAR>x✝ : Set α<GOAL>x✝ ∈ l ↔ ∃ i, p i ∧ x✝ ∈ 𝓟 (s i)
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : AddCommMonoid M'<VAR>inst✝⁸ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁷ : CommSemiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Module A M'<VAR>inst✝⁴ : IsLocalization S A<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>inst✝ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g✝ g : M →ₗ[R] M''<VAR>h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)<VAR>l : LocalizedModule S M →ₗ[R] M''<VAR>hl : l ∘ₗ mkLinearMap S M = g<VAR>m : M<VAR>s : ↥S<GOAL>(lift S g h) (mk m s) = l (mk m s)
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : AddCommMonoid M'<VAR>inst✝⁸ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁷ : CommSemiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Module A M'<VAR>inst✝⁴ : IsLocalization S A<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>inst✝ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g✝ g : M →ₗ[R] M''<VAR>h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)<VAR>l : LocalizedModule S M →ₗ[R] M''<VAR>hl : l ∘ₗ mkLinearMap S M = g<VAR>m : M<VAR>s : ↥S<GOAL>↑⋯.unit⁻¹ (g m) = l (mk m s)
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : AddCommMonoid M'<VAR>inst✝⁸ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁷ : CommSemiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Module A M'<VAR>inst✝⁴ : IsLocalization S A<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>inst✝ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g✝ g : M →ₗ[R] M''<VAR>h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)<VAR>l : LocalizedModule S M →ₗ[R] M''<VAR>hl : l ∘ₗ mkLinearMap S M = g<VAR>m : M<VAR>s : ↥S<GOAL>l (mk m 1) = l (mk (↑s • m) s)
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : AddCommMonoid M'<VAR>inst✝⁸ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁷ : CommSemiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Module A M'<VAR>inst✝⁴ : IsLocalization S A<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>inst✝ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g✝ g : M →ₗ[R] M''<VAR>h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)<VAR>l : LocalizedModule S M →ₗ[R] M''<VAR>hl : l ∘ₗ mkLinearMap S M = g<VAR>m : M<VAR>s : ↥S<GOAL>mk m 1 = mk (↑s • m) s
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : AddCommMonoid M'<VAR>inst✝⁸ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁷ : CommSemiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Module A M'<VAR>inst✝⁴ : IsLocalization S A<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>inst✝ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g✝ g : M →ₗ[R] M''<VAR>h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)<VAR>l : LocalizedModule S M →ₗ[R] M''<VAR>hl : l ∘ₗ mkLinearMap S M = g<VAR>m : M<VAR>s : ↥S<GOAL>∃ u, u • s • m = u • 1 • ↑s • m