ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : atTop.IsCountablyGenerated<VAR>μ : Measure α<VAR>h✝ : Nonempty α<VAR>h_mono : Monotone fun x => μ (Iic x)<GOAL>Tendsto (fun x => μ (Iic x)) atTop (𝓝 (μ univ))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : atTop.IsCountablyGenerated<VAR>μ : Measure α<VAR>h✝ : Nonempty α<VAR>h_mono : Monotone fun x => μ (Iic x)<GOAL>μ univ = ⨆ i, μ (Iic i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : atTop.IsCountablyGenerated<VAR>μ : Measure α<VAR>h✝ : Nonempty α<VAR>h_mono : Monotone fun x => μ (Iic x)<VAR>xs : ℕ → α<VAR>hxs_mono : Monotone xs<VAR>hxs_tendsto : Tendsto xs atTop atTop<GOAL>μ univ = ⨆ i, μ (Iic i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : atTop.IsCountablyGenerated<VAR>μ : Measure α<VAR>h✝ : Nonempty α<VAR>h_mono : Monotone fun x => μ (Iic x)<VAR>xs : ℕ → α<VAR>hxs_mono : Monotone xs<VAR>hxs_tendsto : Tendsto xs atTop atTop<VAR>h_univ : univ = ⋃ n, Iic (xs n)<GOAL>μ univ = ⨆ i, μ (Iic i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : atTop.IsCountablyGenerated<VAR>μ : Measure α<VAR>h✝ : Nonempty α<VAR>h_mono : Monotone fun x => μ (Iic x)<VAR>xs : ℕ → α<VAR>hxs_mono : Monotone xs<VAR>hxs_tendsto : Tendsto xs atTop atTop<VAR>h_univ : univ = ⋃ n, Iic (xs n)<GOAL>Directed (fun x x_1 => x ⊆ x_1) fun n => Iic (xs n)
<VAR>n : Type u_1<VAR>inst✝⁶ : Fintype n<VAR>R : Type u_2<VAR>M✝ : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M✝<VAR>inst✝³ : Module R M✝<VAR>A : Type u_4<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : CommRing A<VAR>inst✝ : IsDomain A<VAR>M : Matrix n n A<GOAL>(∃ v, v ≠ 0 ∧ v ᵥ* M = 0) ↔ M.det = 0
<VAR>x : ℂ<VAR>y : ℝ<GOAL>abs (x ^ ↑y) = abs x ^ y
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>h5 : 5 ≤ card α<VAR>f : Perm α<VAR>hf : f.IsThreeCycle<GOAL>⊤ ≤ normalClosure {⟨f, ⋯⟩}
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>h5 : 5 ≤ card α<VAR>f : Perm α<VAR>hf : f.IsThreeCycle<VAR>hi : Function.Injective ⇑(alternatingGroup α).subtype<GOAL>⊤ ≤ normalClosure {⟨f, ⋯⟩}
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>h5 : 5 ≤ card α<VAR>f : Perm α<VAR>hf : f.IsThreeCycle<VAR>hi : Function.Injective ⇑(alternatingGroup α).subtype<GOAL>map (alternatingGroup α).subtype ⊤ ≤ map (alternatingGroup α).subtype (normalClosure {⟨f, ⋯⟩})
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>h5 : 5 ≤ card α<VAR>f : Perm α<VAR>hf : f.IsThreeCycle<VAR>hi : Function.Injective ⇑(alternatingGroup α).subtype<GOAL>alternatingGroup α ≤ closure (⇑(alternatingGroup α).subtype '' Group.conjugatesOfSet {⟨f, ⋯⟩})
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>h5 : 5 ≤ card α<VAR>f : Perm α<VAR>hf : f.IsThreeCycle<VAR>hi : Function.Injective ⇑(alternatingGroup α).subtype<GOAL>{σ | σ.IsThreeCycle} ⊆ ⇑(alternatingGroup α).subtype '' Group.conjugatesOfSet {⟨f, ⋯⟩}
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>h5 : 5 ≤ card α<VAR>f : Perm α<VAR>hf : f.IsThreeCycle<VAR>hi : Function.Injective ⇑(alternatingGroup α).subtype<VAR>g : Perm α<VAR>h : g ∈ {σ | σ.IsThreeCycle}<GOAL>g ∈ ⇑(alternatingGroup α).subtype '' Group.conjugatesOfSet {⟨f, ⋯⟩}
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>h5 : 5 ≤ card α<VAR>f : Perm α<VAR>hf : f.IsThreeCycle<VAR>hi : Function.Injective ⇑(alternatingGroup α).subtype<VAR>c : Perm α<VAR>h : c * f * c⁻¹ ∈ {σ | σ.IsThreeCycle}<GOAL>c * f * c⁻¹ ∈ ⇑(alternatingGroup α).subtype '' Group.conjugatesOfSet {⟨f, ⋯⟩}
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>h5 : 5 ≤ card α<VAR>f : Perm α<VAR>hf : f.IsThreeCycle<VAR>hi : Function.Injective ⇑(alternatingGroup α).subtype<VAR>c : Perm α<VAR>h : c * f * c⁻¹ ∈ {σ | σ.IsThreeCycle}<GOAL>⟨c * f * c⁻¹, ⋯⟩ ∈ Group.conjugatesOfSet {⟨f, ⋯⟩}
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>h5 : 5 ≤ card α<VAR>f : Perm α<VAR>hf : f.IsThreeCycle<VAR>hi : Function.Injective ⇑(alternatingGroup α).subtype<VAR>c : Perm α<VAR>h : c * f * c⁻¹ ∈ {σ | σ.IsThreeCycle}<GOAL>∃ a ∈ {⟨f, ⋯⟩}, IsConj a ⟨c * f * c⁻¹, ⋯⟩
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>β : Type w<VAR>f : β → C<VAR>inst✝ : HasCoproduct f<GOAL>IsSeparator (∐ f) ↔ IsSeparating (Set.range f)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>β : Type w<VAR>f : β → C<VAR>inst✝ : HasCoproduct f<VAR>h : IsSeparator (∐ f)<VAR>X Y : C<VAR>u v : X ⟶ Y<VAR>huv : ∀ G ∈ Set.range f, ∀ (h : G ⟶ X), h ≫ u = h ≫ v<GOAL>u = v
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>β : Type w<VAR>f : β → C<VAR>inst✝ : HasCoproduct f<VAR>h : IsSeparating (Set.range f)<VAR>X Y : C<VAR>u v : X ⟶ Y<VAR>huv : ∀ (h : ∐ f ⟶ X), h ≫ u = h ≫ v<VAR>Z : C<VAR>hZ : Z ∈ Set.range f<VAR>g : Z ⟶ X<GOAL>g ≫ u = g ≫ v
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>H : Subgroup (E ≃ₐ[F] E)<VAR>K : IntermediateField F E<VAR>inst✝ : FiniteDimensional F E<GOAL>(fixedField H).fixingSubgroup = H
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>H : Subgroup (E ≃ₐ[F] E)<VAR>K : IntermediateField F E<VAR>inst✝ : FiniteDimensional F E<VAR>H_le : H ≤ (fixedField H).fixingSubgroup<GOAL>(fixedField H).fixingSubgroup = H
<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>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>p q : FormalMultilinearSeries 𝕜 E F<GOAL>min p.radius q.radius ≤ (p + q).radius
<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>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>r✝ : ℝ≥0<VAR>p q : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>hr : ↑r < min p.radius q.radius<GOAL>↑r ≤ (p + q).radius
<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>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>r✝ : ℝ≥0<VAR>p q : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>hr : ↑r < p.radius ∧ ↑r < q.radius<GOAL>↑r ≤ (p + q).radius
<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>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>r✝ : ℝ≥0<VAR>p q : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>hr : ↑r < p.radius ∧ ↑r < q.radius<VAR>this : (fun x => ‖p x‖ * ↑r ^ x + ‖q x‖ * ↑r ^ x) =O[atTop] fun x => 1<GOAL>↑r ≤ (p + q).radius
<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>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>r✝ : ℝ≥0<VAR>p q : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>hr : ↑r < p.radius ∧ ↑r < q.radius<VAR>this : (fun x => ‖p x‖ * ↑r ^ x + ‖q x‖ * ↑r ^ x) =O[atTop] fun x => 1<VAR>n : ℕ<GOAL>‖‖(p + q) n‖ * ↑r ^ n‖ ≤ ‖‖p n‖ * ↑r ^ n + ‖q n‖ * ↑r ^ n‖
<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>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>r✝ : ℝ≥0<VAR>p q : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>hr : ↑r < p.radius ∧ ↑r < q.radius<VAR>this : (fun x => ‖p x‖ * ↑r ^ x + ‖q x‖ * ↑r ^ x) =O[atTop] fun x => 1<VAR>n : ℕ<GOAL>‖(p + q) n‖ * ‖↑r ^ n‖ ≤ ‖‖p n‖ + ‖q n‖‖ * ‖↑r ^ n‖
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>D✝ : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} D✝<VAR>J : Type u<VAR>inst✝³ : Category.{v, u} J<VAR>T : Comonad C<VAR>D : J ⥤ T.Coalgebra<VAR>c : Cone (D ⋙ T.forget)<VAR>t : IsLimit c<VAR>inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor<VAR>inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<VAR>inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<VAR>s : Cone D<VAR>j : J<GOAL>(s.pt.a ≫ T.map (t.lift (T.forget.mapCone s))) ≫ T.map (c.π.app j) = (t.lift (T.forget.mapCone s) ≫ lambda c t) ≫ T.map (c.π.app j)
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>D✝ : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} D✝<VAR>J : Type u<VAR>inst✝³ : Category.{v, u} J<VAR>T : Comonad C<VAR>D : J ⥤ T.Coalgebra<VAR>c : Cone (D ⋙ T.forget)<VAR>t : IsLimit c<VAR>inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor<VAR>inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<VAR>inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<VAR>s : Cone D<VAR>j : J<GOAL>s.pt.a ≫ T.map ((T.forget.mapCone s).π.app j) = (T.forget.mapCone s).π.app j ≫ (D.obj j).a
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>D✝ : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} D✝<VAR>J✝ : Type u<VAR>inst✝³ : Category.{v, u} J✝<VAR>T : Comonad C<VAR>D : J✝ ⥤ T.Coalgebra<VAR>c : Cone (D ⋙ T.forget)<VAR>t : IsLimit c<VAR>inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor<VAR>inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<VAR>inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<VAR>s : Cone D<VAR>m : s.pt ⟶ (liftedCone c t).pt<VAR>J : ∀ (j : J✝), m ≫ (liftedCone c t).π.app j = s.π.app j<GOAL>m.f = ((fun s => { f := t.lift (T.forget.mapCone s), h := ⋯ }) s).f
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>D✝ : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} D✝<VAR>J✝ : Type u<VAR>inst✝³ : Category.{v, u} J✝<VAR>T : Comonad C<VAR>D : J✝ ⥤ T.Coalgebra<VAR>c : Cone (D ⋙ T.forget)<VAR>t : IsLimit c<VAR>inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor<VAR>inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<VAR>inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<VAR>s : Cone D<VAR>m : s.pt ⟶ (liftedCone c t).pt<VAR>J : ∀ (j : J✝), m ≫ (liftedCone c t).π.app j = s.π.app j<GOAL>∀ (j : J✝), m.f ≫ c.π.app j = ((fun s => { f := t.lift (T.forget.mapCone s), h := ⋯ }) s).f ≫ c.π.app j
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f : M →ₗ[R] A<VAR>cond : ∀ (m : M), f m * f m = (algebraMap R A) (Q m)<VAR>g : CliffordAlgebra Q →ₐ[R] A<GOAL>g.toLinearMap ∘ₗ ι Q = f ↔ g = (lift Q) ⟨f, cond⟩
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f : M →ₗ[R] A<VAR>cond : ∀ (m : M), f m * f m = (algebraMap R A) (Q m)<VAR>g : CliffordAlgebra Q →ₐ[R] A<GOAL>g.toLinearMap ∘ₗ ι Q = f ↔ (lift Q).symm g = ⟨f, cond⟩
<VAR>n✝ b b' : ℕ<VAR>h : b' % b = 1<VAR>n : ℕ<GOAL>n ≡ (b'.digits n).sum [MOD b]
<VAR>n✝ b b' : ℕ<VAR>h : b' % b = 1<VAR>n : ℕ<GOAL>n ≡ ofDigits 1 (b'.digits n) [MOD b]
<VAR>n✝ b b' : ℕ<VAR>h : b' % b = 1<VAR>n : ℕ<GOAL>ofDigits b' (b'.digits n) ≡ ofDigits 1 (b'.digits n) [MOD b]
<VAR>n✝ b b' : ℕ<VAR>h : b' % b = 1<VAR>n : ℕ<GOAL>1 = b' % b
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCancelCommMonoid G<VAR>x : k[G]<VAR>g : G<GOAL>of' k G g * (x /ᵒᶠ g) + x %ᵒᶠ g = x
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCancelCommMonoid G<VAR>x : k[G]<VAR>g g' : G<GOAL>(of' k G g * (x /ᵒᶠ g) + x %ᵒᶠ g) g' = x g'
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCancelCommMonoid G<VAR>x : k[G]<VAR>g g' : G<GOAL>(of' k G g * (x /ᵒᶠ g)) g' + (x %ᵒᶠ g) g' = x g'
<VAR>α : Type u_1<VAR>inst✝¹ : Lattice α<VAR>inst✝ : IsWeakLowerModularLattice α<VAR>a b : α<GOAL>a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ b
<VAR>α : Type u_1<VAR>inst✝¹ : Lattice α<VAR>inst✝ : IsWeakLowerModularLattice α<VAR>a b : α<GOAL>a ⋖ b ⊔ a → b ⋖ b ⊔ a → b ⊓ a ⋖ b
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>a b x y z : α<VAR>h : IsCompl y z<GOAL>x ⊓ y = ⊥ ↔ x ≤ z
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>v : E → E<VAR>t₀ : ℝ<VAR>x₀ : E<VAR>hv : ContDiffAt ℝ 1 v x₀<GOAL>∃ ε > 0, ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>v : E → E<VAR>t₀ : ℝ<VAR>x₀ : E<VAR>hv : ContDiffAt ℝ 1 v x₀<VAR>L : ℝ≥0<VAR>s : Set E<VAR>hs : s ∈ 𝓝 x₀<VAR>hlip : LipschitzOnWith L v s<GOAL>∃ ε > 0, ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>v : E → E<VAR>t₀ : ℝ<VAR>x₀ : E<VAR>hv : ContDiffAt ℝ 1 v x₀<VAR>L : ℝ≥0<VAR>s : Set E<VAR>hs : s ∈ 𝓝 x₀<VAR>hlip : LipschitzOnWith L v s<VAR>R₁ : ℝ<VAR>hR₁ : 0 < R₁<VAR>hball : ball x₀ R₁ ⊆ s<GOAL>∃ ε > 0, ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>v : E → E<VAR>t₀ : ℝ<VAR>x₀ : E<VAR>hv : ContDiffAt ℝ 1 v x₀<VAR>L : ℝ≥0<VAR>s : Set E<VAR>hs : s ∈ 𝓝 x₀<VAR>hlip : LipschitzOnWith L v s<VAR>R₁ : ℝ<VAR>hR₁ : 0 < R₁<VAR>hball : ball x₀ R₁ ⊆ s<VAR>R₂ : ℝ<VAR>hR₂ : 0 < R₂<VAR>hbdd : ∀ {x : E}, dist x x₀ < R₂ → dist ‖v x‖ ‖v x₀‖ < 1<GOAL>∃ ε > 0, ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>v : E → E<VAR>t₀ : ℝ<VAR>x₀ : E<VAR>hv : ContDiffAt ℝ 1 v x₀<VAR>L : ℝ≥0<VAR>s : Set E<VAR>hs : s ∈ 𝓝 x₀<VAR>hlip : LipschitzOnWith L v s<VAR>R₁ : ℝ<VAR>hR₁ : 0 < R₁<VAR>hball : ball x₀ R₁ ⊆ s<VAR>R₂ : ℝ<VAR>hR₂ : 0 < R₂<VAR>hbdd : ∀ {x : E}, dist x x₀ < R₂ → dist ‖v x‖ ‖v x₀‖ < 1<VAR>hbdd' : ∀ x ∈ ball x₀ R₂, ‖v x‖ ≤ 1 + ‖v x₀‖<GOAL>∃ ε > 0, ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>v : E → E<VAR>t₀ : ℝ<VAR>x₀ : E<VAR>hv : ContDiffAt ℝ 1 v x₀<VAR>L : ℝ≥0<VAR>s : Set E<VAR>hs : s ∈ 𝓝 x₀<VAR>hlip : LipschitzOnWith L v s<VAR>R₁ : ℝ<VAR>hR₁ : 0 < R₁<VAR>hball : ball x₀ R₁ ⊆ s<VAR>R₂ : ℝ<VAR>hR₂ : 0 < R₂<VAR>hbdd : ∀ {x : E}, dist x x₀ < R₂ → dist ‖v x‖ ‖v x₀‖ < 1<VAR>hbdd' : ∀ x ∈ ball x₀ R₂, ‖v x‖ ≤ 1 + ‖v x₀‖<VAR>ε : ℝ := min R₁ R₂ / 2 / (1 + ‖v x₀‖)<VAR>hε : ε = min R₁ R₂ / 2 / (1 + ‖v x₀‖)<GOAL>∃ ε > 0, ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>v : E → E<VAR>t₀ : ℝ<VAR>x₀ : E<VAR>hv : ContDiffAt ℝ 1 v x₀<VAR>L : ℝ≥0<VAR>s : Set E<VAR>hs : s ∈ 𝓝 x₀<VAR>hlip : LipschitzOnWith L v s<VAR>R₁ : ℝ<VAR>hR₁ : 0 < R₁<VAR>hball : ball x₀ R₁ ⊆ s<VAR>R₂ : ℝ<VAR>hR₂ : 0 < R₂<VAR>hbdd : ∀ {x : E}, dist x x₀ < R₂ → dist ‖v x‖ ‖v x₀‖ < 1<VAR>hbdd' : ∀ x ∈ ball x₀ R₂, ‖v x‖ ≤ 1 + ‖v x₀‖<VAR>ε : ℝ := min R₁ R₂ / 2 / (1 + ‖v x₀‖)<VAR>hε : ε = min R₁ R₂ / 2 / (1 + ‖v x₀‖)<VAR>hε0 : 0 < ε<GOAL>∃ ε > 0, ∃ L R C, IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>v : E → E<VAR>t₀ : ℝ<VAR>x₀ : E<VAR>hv : ContDiffAt ℝ 1 v x₀<VAR>L : ℝ≥0<VAR>s : Set E<VAR>hs : s ∈ 𝓝 x₀<VAR>hlip : LipschitzOnWith L v s<VAR>R₁ : ℝ<VAR>hR₁ : 0 < R₁<VAR>hball : ball x₀ R₁ ⊆ s<VAR>R₂ : ℝ<VAR>hR₂ : 0 < R₂<VAR>hbdd : ∀ {x : E}, dist x x₀ < R₂ → dist ‖v x‖ ‖v x₀‖ < 1<VAR>hbdd' : ∀ x ∈ ball x₀ R₂, ‖v x‖ ≤ 1 + ‖v x₀‖<VAR>ε : ℝ := min R₁ R₂ / 2 / (1 + ‖v x₀‖)<VAR>hε : ε = min R₁ R₂ / 2 / (1 + ‖v x₀‖)<VAR>hε0 : 0 < ε<GOAL>IsPicardLindelof (fun x => v) (t₀ - ε) t₀ (t₀ + ε) x₀ L (min R₁ R₂ / 2) (1 + ‖v x₀‖)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : LinearOrderedField R<VAR>inst✝ : Archimedean R<VAR>f : α → ℚ<VAR>l : Filter α<GOAL>Tendsto (fun n => ↑(f n)) l atTop ↔ Tendsto f l atTop
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : LinearOrderedField R<VAR>inst✝ : Archimedean R<VAR>f : α → ℚ<VAR>l : Filter α<GOAL>Tendsto (fun n => ↑(f n)) l atTop ↔ Tendsto (Rat.cast ∘ f) l atTop
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v w : V<VAR>e : Sym2 V<VAR>h : a ≠ b<VAR>ha : e ∈ G.incidenceSet a<VAR>hb : e ∈ G.incidenceSet b<GOAL>G.Adj a b
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.9744, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>S : ShortComplex C<VAR>hS : S.ShortExact<VAR>inst✝ : Balanced C<GOAL>IsIso S.f ↔ IsZero S.X₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.9744, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>S : ShortComplex C<VAR>hS : S.ShortExact<VAR>inst✝ : Balanced C<VAR>this : HasZeroObject C<GOAL>IsIso S.f ↔ IsZero S.X₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.9744, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>S : ShortComplex C<VAR>hS : S.ShortExact<VAR>inst✝ : Balanced C<VAR>this✝ : HasZeroObject C<VAR>this : Mono S.f<GOAL>IsIso S.f ↔ IsZero S.X₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.9744, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>S : ShortComplex C<VAR>hS : S.ShortExact<VAR>inst✝ : Balanced C<VAR>this✝¹ : HasZeroObject C<VAR>this✝ : Mono S.f<VAR>this : Epi S.g<GOAL>IsIso S.f ↔ IsZero S.X₃
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f✝ : α ↪ β<VAR>s : Finset α<VAR>f : α ↪ β<VAR>a : α<GOAL>↑(map f {a}) = ↑{f a}
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : InvolutiveInv α<VAR>s t : Set α<VAR>a : α<GOAL>a⁻¹ ∈ s⁻¹ ↔ a ∈ s
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>inst✝² : FiniteDimensional ℝ F<VAR>inst✝¹ : MeasurableSpace F<VAR>inst✝ : BorelSpace F<VAR>b : OrthonormalBasis ι ℝ F<GOAL>MeasurePreserving (⇑b.measurableEquiv) volume volume
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>inst✝² : FiniteDimensional ℝ F<VAR>inst✝¹ : MeasurableSpace F<VAR>inst✝ : BorelSpace F<VAR>b : OrthonormalBasis ι ℝ F<VAR>e_3✝ : MeasureSpace.toMeasurableSpace = inst✝¹<GOAL>volume = map (⇑b.measurableEquiv.symm) volume
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>inst✝² : FiniteDimensional ℝ F<VAR>inst✝¹ : MeasurableSpace F<VAR>inst✝ : BorelSpace F<VAR>b : OrthonormalBasis ι ℝ F<VAR>e_3✝ : MeasureSpace.toMeasurableSpace = inst✝¹<GOAL>volume = map (⇑b.measurableEquiv.symm) (EuclideanSpace.basisFun ι ℝ).toBasis.addHaar
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>inst✝² : FiniteDimensional ℝ F<VAR>inst✝¹ : MeasurableSpace F<VAR>inst✝ : BorelSpace F<VAR>b : OrthonormalBasis ι ℝ F<VAR>e_3✝ : MeasureSpace.toMeasurableSpace = inst✝¹<GOAL>volume = ((EuclideanSpace.basisFun ι ℝ).toBasis.map b.repr.symm.toContinuousLinearEquiv.toLinearEquiv).addHaar
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹⁰ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>i : ι<VAR>a : 𝕜<VAR>v : EuclideanSpace 𝕜 ι<GOAL>⟪single i a, v⟫_𝕜 = (starRingEnd 𝕜) a * v i
<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>hf : HasFTaylorSeriesUpToOn n f p s<VAR>g : G →L[𝕜] E<VAR>A : (m : ℕ) → ContinuousMultilinearMap 𝕜 (fun i => E) F → ContinuousMultilinearMap 𝕜 (fun i => G) F := fun m h => h.compContinuousLinearMap fun x => g<GOAL>HasFTaylorSeriesUpToOn n (f ∘ ⇑g) (fun x k => (p (g x) k).compContinuousLinearMap fun x => g) (⇑g ⁻¹' s)
<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>hf : HasFTaylorSeriesUpToOn n f p s<VAR>g : G →L[𝕜] E<VAR>A : (m : ℕ) → ContinuousMultilinearMap 𝕜 (fun i => E) F → ContinuousMultilinearMap 𝕜 (fun i => G) F := fun m h => h.compContinuousLinearMap fun x => g<VAR>hA : ∀ (m : ℕ), IsBoundedLinearMap 𝕜 (A m)<GOAL>HasFTaylorSeriesUpToOn n (f ∘ ⇑g) (fun x k => (p (g x) k).compContinuousLinearMap fun x => g) (⇑g ⁻¹' s)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>x y : α<VAR>hx : x ∈ l<VAR>hy : y ∈ l<VAR>h : indexOf x l = indexOf y l<GOAL>x = y
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>x y : α<VAR>hx : x ∈ l<VAR>hy : y ∈ l<VAR>h : indexOf x l = indexOf y l<VAR>x_eq_y : l.get ⟨indexOf x l, ⋯⟩ = l.get ⟨indexOf y l, ⋯⟩<GOAL>x = y