ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>i j : ℤ<VAR>h : ¬i = j<VAR>hij : -i + j ≠ 0<GOAL>∫ (x : AddCircle T), (fourier (-i + j)) x ∂haarAddCircle = 0
<VAR>α : Type u<VAR>inst✝ : EMetricSpace α<VAR>s : Set α<VAR>hs : IsClosed s<GOAL>IsClosed {t | ↑t ⊆ s}
<VAR>α : Type u<VAR>inst✝ : EMetricSpace α<VAR>s : Set α<VAR>hs : IsClosed s<VAR>t : Closeds α<VAR>ht : t ∈ closure {t | ↑t ⊆ s}<VAR>x : α<VAR>hx : x ∈ t<GOAL>x ∈ s
<VAR>α : Type u<VAR>inst✝ : EMetricSpace α<VAR>s : Set α<VAR>hs : IsClosed s<VAR>t : Closeds α<VAR>ht : t ∈ closure {t | ↑t ⊆ s}<VAR>x : α<VAR>hx : x ∈ t<VAR>this : x ∈ closure s<GOAL>x ∈ s
<VAR>R : Type u_1<VAR>inst✝¹ : AddMonoidWithOne R<VAR>r : R<VAR>n p✝ p : ℕ<VAR>inst✝ : CharP R p<VAR>k : ℕ<VAR>h : NeZero ↑k<GOAL>¬p ∣ k
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℤ<GOAL>U R (n - 2) = 2 * X * U R (n - 1) - U R n
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x : α<VAR>s t : Set α<VAR>r : ℝ<VAR>c : α<VAR>f : β → α<VAR>l : Filter β<GOAL>Tendsto (fun x => dist c (f x)) l atTop ↔ Tendsto f l (cobounded α)
<VAR>α : Type u_1<VAR>inst✝³ : GeneralizedBooleanAlgebra α<VAR>inst✝² : DecidableRel Disjoint<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>u v a b : α<VAR>inst✝ : DecidableEq α<VAR>ha : a ∈ 𝓒 u v s<VAR>hva : v ≤ a<VAR>hvu : v = ⊥ → u = ⊥<GOAL>a ∈ s
<VAR>α : Type u_1<VAR>inst✝³ : GeneralizedBooleanAlgebra α<VAR>inst✝² : DecidableRel Disjoint<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>u v a b : α<VAR>inst✝ : DecidableEq α<VAR>ha : a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a<VAR>hva : v ≤ a<VAR>hvu : v = ⊥ → u = ⊥<GOAL>a ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f g : Ultrafilter α<VAR>s✝ t : Set α<VAR>p q : α → Prop<VAR>is : Set β<VAR>s : β → Set α<VAR>his : is.Finite<GOAL>⋃ i ∈ is, s i ∈ f ↔ ∃ i ∈ is, s i ∈ f
<VAR>α : Type u_1<VAR>M : α → Type u_2<VAR>u : Ultrafilter α<VAR>L : Language<VAR>inst✝¹ : (a : α) → L.Structure (M a)<VAR>inst✝ : ∀ (a : α), Nonempty (M a)<VAR>φ : L.Sentence<GOAL>Formula.Realize φ default ↔ ∀ᶠ (a : α) in ↑u, Formula.Realize φ default
<VAR>α : Type u_1<VAR>M : α → Type u_2<VAR>u : Ultrafilter α<VAR>L : Language<VAR>inst✝¹ : (a : α) → L.Structure (M a)<VAR>inst✝ : ∀ (a : α), Nonempty (M a)<VAR>φ : L.Sentence<GOAL>Formula.Realize φ default = Formula.Realize φ fun i => Quotient.mk' fun a => default i
<VAR>m n : ℕ<VAR>hn : 0 < n<GOAL>n ! < m ! ↔ n < m
<VAR>m n : ℕ<VAR>hn : 0 < n<VAR>h : n < m<GOAL>n ! < m !
<VAR>m n : ℕ<VAR>hn : 0 < n<VAR>h : n < m<VAR>this : ∀ {n : ℕ}, 0 < n → n ! < (n + 1)!<GOAL>n ! < m !
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>n : ℤ<GOAL>map f (T R n) = T S n
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x✝ y : α<VAR>inst✝³ : DecidableRel f.SameCycle<VAR>inst✝² : DecidableRel g.SameCycle<VAR>inst✝¹ : DecidableRel (f * g).SameCycle<VAR>inst✝ : DecidableRel (g * f).SameCycle<VAR>h : f.Disjoint g<VAR>x : α<GOAL>(f * g).cycleOf x = f.cycleOf x * g.cycleOf x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x✝ y : α<VAR>inst✝³ : DecidableRel f.SameCycle<VAR>inst✝² : DecidableRel g.SameCycle<VAR>inst✝¹ : DecidableRel (f * g).SameCycle<VAR>inst✝ : DecidableRel (g * f).SameCycle<VAR>h : f.Disjoint g<VAR>x : α<VAR>hfx : f x = x<GOAL>(f * g).cycleOf x = f.cycleOf x * g.cycleOf x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x✝ y : α<VAR>inst✝³ : DecidableRel f.SameCycle<VAR>inst✝² : DecidableRel g.SameCycle<VAR>inst✝¹ : DecidableRel (f * g).SameCycle<VAR>inst✝ : DecidableRel (g * f).SameCycle<VAR>h : f.Disjoint g<VAR>x : α<VAR>hgx : g x = x<GOAL>(f * g).cycleOf x = f.cycleOf x * g.cycleOf x
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : SFinite μ<VAR>x : α<VAR>y : β<GOAL>(dirac x).prod (dirac y) = dirac (x, y)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>r : R<VAR>x y : M<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>p p' : Submodule R M<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁶ : Ring R₂<VAR>inst✝⁵ : AddCommGroup M₂<VAR>inst✝⁴ : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>q : Submodule R₂ M₂<VAR>N : Type u_5<VAR>O : Type u_6<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommGroup O<VAR>inst✝ : Module R O<VAR>P : Submodule R M<VAR>Q : Submodule R N<VAR>S : Submodule R O<VAR>e : M ≃ₗ[R] N<VAR>f : N ≃ₗ[R] O<VAR>he : map e P = Q<VAR>hf : map f Q = S<VAR>hef : map (e ≪≫ₗ f) P = S<VAR>x✝ : M ⧸ P<GOAL>(equiv P S (e ≪≫ₗ f) hef) x✝ = (equiv P Q e he ≪≫ₗ equiv Q S f hf) x✝
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>r : R<VAR>x y : M<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>p p' : Submodule R M<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁶ : Ring R₂<VAR>inst✝⁵ : AddCommGroup M₂<VAR>inst✝⁴ : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>q : Submodule R₂ M₂<VAR>N : Type u_5<VAR>O : Type u_6<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommGroup O<VAR>inst✝ : Module R O<VAR>P : Submodule R M<VAR>Q : Submodule R N<VAR>S : Submodule R O<VAR>e : M ≃ₗ[R] N<VAR>f : N ≃ₗ[R] O<VAR>he : map e P = Q<VAR>hf : map f Q = S<VAR>hef : map (e ≪≫ₗ f) P = S<VAR>x✝ : M ⧸ P<GOAL>(P.mapQ S (↑f ∘ₗ ↑e) ⋯) x✝ = (Q.mapQ S ↑f ⋯) ((P.mapQ Q ↑e ⋯) x✝)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N : Bimod Y Z<GOAL>(whiskerRight (𝟙 M) N).hom = (𝟙 (M.tensorBimod N)).hom
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N : Bimod Y Z<GOAL>coequalizer.π (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft) ≫ (whiskerRight (𝟙 M) N).hom = coequalizer.π (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft) ≫ (𝟙 (M.tensorBimod N)).hom
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N : Bimod Y Z<GOAL>coequalizer.π (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft) ≫ colimMap (parallelPairHom (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft) (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft) (𝟙 M.X ▷ Y.X ▷ N.X) (𝟙 M.X ▷ N.X) ⋯ ⋯) = coequalizer.π (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft) ≫ 𝟙 (TensorBimod.X M N)
<VAR>R : Type u_1<VAR>inst✝² : CommMonoid R<VAR>R' : Type u_2<VAR>inst✝¹ : CommRing R'<VAR>R'' : Type u_3<VAR>inst✝ : CommRing R''<VAR>χ φ : MulChar R R'<VAR>f : R' →+* R''<VAR>a✝ : Rˣ<GOAL>((χ * φ).ringHomComp f) ↑a✝ = (χ.ringHomComp f * φ.ringHomComp f) ↑a✝
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : HasUpperLowerClosure α<VAR>s : Set α<VAR>h : IsUpperSet s<GOAL>IsUpperSet (interior s)
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : HasUpperLowerClosure α<VAR>s : Set α<VAR>h : IsUpperSet s<GOAL>IsLowerSet (closure sᶜ)
<VAR>J : Type v<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u<VAR>inst✝¹ : Category.{v, u} D<VAR>G : D ⥤ C<VAR>inst✝ : G.IsRightAdjoint<VAR>A : C<VAR>B : D<VAR>h : A ⟶ G.obj B<GOAL>(fun x => (Adjunction.ofIsRightAdjoint G).unit.app A) PUnit.unit ≫ G.map (((Adjunction.ofIsRightAdjoint G).homEquiv A B).symm h) = h
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<GOAL>T.mor₂ = 0 ↔ Epi T.mor₁
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>h : T.invRotate.mor₃ = 0 ↔ Epi T.invRotate.mor₂<GOAL>T.mor₂ = 0 ↔ Epi T.mor₁
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>h : T.mor₂ ≫ (shiftFunctorCompIsoId C (-1) 1 ⋯).inv.app T.3 = 0 ↔ Epi T.mor₁<GOAL>T.mor₂ = 0 ↔ Epi T.mor₁
<VAR>B : Type u<VAR>inst✝ : Bicategory B<VAR>a b c d e : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<VAR>i : d ⟶ e<GOAL>(α_ f g (h ≫ i)).hom ≫ f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv = (α_ (f ≫ g) h i).inv ≫ (α_ f g h).hom ▷ i
<VAR>B : Type u<VAR>inst✝ : Bicategory B<VAR>a b c d e : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<VAR>i : d ⟶ e<GOAL>((α_ f g (h ≫ i)).inv ≫ (α_ f g (h ≫ i)).hom ≫ f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv) ≫ (α_ f g h).inv ▷ i = ((α_ f g (h ≫ i)).inv ≫ (α_ (f ≫ g) h i).inv ≫ (α_ f g h).hom ▷ i) ≫ (α_ f g h).inv ▷ i
<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>h : ↑r < p.radius<GOAL>∃ a ∈ Ioo 0 1, (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x
<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>h : ↑r < p.radius<VAR>this : (∃ a ∈ Ioo 0 1, (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x) ↔ ∃ a < 1, ∃ C, (0 < C ∨ 0 < 1) ∧ ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n<GOAL>∃ a ∈ Ioo 0 1, (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x
<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>h : ↑r < p.radius<VAR>this : (∃ a ∈ Ioo 0 1, (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x) ↔ ∃ a < 1, ∃ C, (0 < C ∨ 0 < 1) ∧ ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n<GOAL>∃ a < 1, ∃ C, (0 < C ∨ 0 < 1) ∧ ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ 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>this : (∃ a ∈ Ioo 0 1, (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x) ↔ ∃ a < 1, ∃ C, (0 < C ∨ 0 < 1) ∧ ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n<VAR>h : ∃ i i_1, ∃ (_ : ∀ (n : ℕ), ‖p n‖ * ↑i ^ n ≤ i_1), ↑r < ↑i<GOAL>∃ a < 1, ∃ C, (0 < C ∨ 0 < 1) ∧ ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ 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>this : (∃ a ∈ Ioo 0 1, (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x) ↔ ∃ a < 1, ∃ C, (0 < C ∨ 0 < 1) ∧ ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n<VAR>t : ℝ≥0<VAR>C : ℝ<VAR>hC : ∀ (n : ℕ), ‖p n‖ * ↑t ^ n ≤ C<VAR>rt : ↑r < ↑t<GOAL>∃ a < 1, ∃ C, (0 < C ∨ 0 < 1) ∧ ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ 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>this : (∃ a ∈ Ioo 0 1, (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x) ↔ ∃ a < 1, ∃ C, (0 < C ∨ 0 < 1) ∧ ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n<VAR>t : ℝ≥0<VAR>C : ℝ<VAR>hC : ∀ (n : ℕ), ‖p n‖ * ↑t ^ n ≤ C<VAR>rt : r < t<GOAL>∃ a < 1, ∃ C, (0 < C ∨ 0 < 1) ∧ ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ 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>this✝ : (∃ a ∈ Ioo 0 1, (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x) ↔ ∃ a < 1, ∃ C, (0 < C ∨ 0 < 1) ∧ ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n<VAR>t : ℝ≥0<VAR>C : ℝ<VAR>hC : ∀ (n : ℕ), ‖p n‖ * ↑t ^ n ≤ C<VAR>rt : ↑r < ↑t<VAR>this : 0 < ↑t<GOAL>∃ a < 1, ∃ C, (0 < C ∨ 0 < 1) ∧ ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ 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>this✝ : (∃ a ∈ Ioo 0 1, (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x) ↔ ∃ a < 1, ∃ C, (0 < C ∨ 0 < 1) ∧ ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n<VAR>t : ℝ≥0<VAR>C : ℝ<VAR>hC : ∀ (n : ℕ), ‖p n‖ * ↑t ^ n ≤ C<VAR>rt : ↑r / ↑t < 1<VAR>this : 0 < ↑t<GOAL>∃ a < 1, ∃ C, (0 < C ∨ 0 < 1) ∧ ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ 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>this✝ : (∃ a ∈ Ioo 0 1, (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x) ↔ ∃ a < 1, ∃ C, (0 < C ∨ 0 < 1) ∧ ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n<VAR>t : ℝ≥0<VAR>C : ℝ<VAR>hC : ∀ (n : ℕ), ‖p n‖ * ↑t ^ n ≤ C<VAR>rt : ↑r / ↑t < 1<VAR>this : 0 < ↑t<VAR>n : ℕ<GOAL>|‖p n‖ * ↑r ^ n| ≤ C * (↑r / ↑t) ^ n
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f✝¹ : ℝ → E<VAR>g' g✝ φ : ℝ → ℝ<VAR>a✝ b✝ : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f✝ f'✝ : ℝ → E<VAR>a b : ℝ<VAR>f f' g : ℝ → ℝ<VAR>hf : ContinuousOn f [[a, b]]<VAR>hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x<VAR>hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))<VAR>hg1 : IntegrableOn g (f '' [[a, b]]) volume<VAR>hg2 : IntegrableOn (fun x => (g ∘ f) x * f' x) [[a, b]] volume<GOAL>∫ (x : ℝ) in a..b, (g ∘ f) x * f' x = ∫ (u : ℝ) in f a..f b, g u
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f✝¹ : ℝ → E<VAR>g' g✝ φ : ℝ → ℝ<VAR>a✝ b✝ : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f✝ f'✝ : ℝ → E<VAR>a b : ℝ<VAR>f f' g : ℝ → ℝ<VAR>hf : ContinuousOn f [[a, b]]<VAR>hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x<VAR>hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))<VAR>hg1 : IntegrableOn g (f '' [[a, b]]) volume<VAR>hg2 : IntegrableOn (fun x => (g ∘ f) x * f' x) [[a, b]] volume<VAR>hg2' : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]] volume<GOAL>∫ (x : ℝ) in a..b, (g ∘ f) x * f' x = ∫ (u : ℝ) in f a..f b, g u
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} D<VAR>inst✝⁴ : Abelian C<VAR>inst✝³ : HasProjectiveResolutions C<VAR>inst✝² : Abelian D<VAR>F : C ⥤ D<VAR>inst✝¹ : F.Additive<VAR>n : ℕ<VAR>X : C<VAR>inst✝ : Projective X<GOAL>IsZero ((F.leftDerived (n + 1)).obj X)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} D<VAR>inst✝⁴ : Abelian C<VAR>inst✝³ : HasProjectiveResolutions C<VAR>inst✝² : Abelian D<VAR>F : C ⥤ D<VAR>inst✝¹ : F.Additive<VAR>n : ℕ<VAR>X : C<VAR>inst✝ : Projective X<GOAL>IsZero ((HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) (n + 1)).obj ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj (ProjectiveResolution.self X).complex))
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} D<VAR>inst✝⁴ : Abelian C<VAR>inst✝³ : HasProjectiveResolutions C<VAR>inst✝² : Abelian D<VAR>F : C ⥤ D<VAR>inst✝¹ : F.Additive<VAR>n : ℕ<VAR>X : C<VAR>inst✝ : Projective X<GOAL>((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj (ProjectiveResolution.self X).complex).ExactAt (n + 1)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s t : Set α<GOAL>x ∈ closedBall y ε ↔ y ∈ closedBall x ε
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y : C<VAR>S✝ R : Sieve X<VAR>J : GrothendieckTopology C<VAR>i : X ⟶ Y<VAR>inst✝ : IsIso i<VAR>S : Sieve Y<GOAL>Sieve.pullback i S ∈ J.sieves X ↔ S ∈ J.sieves Y
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y : C<VAR>S✝ R : Sieve X<VAR>J : GrothendieckTopology C<VAR>i : X ⟶ Y<VAR>inst✝ : IsIso i<VAR>S : Sieve Y<VAR>H : Sieve.pullback i S ∈ J.sieves X<GOAL>S ∈ J.sieves Y
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y : C<VAR>S✝ R : Sieve X<VAR>J : GrothendieckTopology C<VAR>i : X ⟶ Y<VAR>inst✝ : IsIso i<VAR>S : Sieve Y<VAR>H : Sieve.pullback i S ∈ J.sieves X<GOAL>S = Sieve.pullback (inv i) (Sieve.pullback i S)
<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<VAR>hs : Dense s<VAR>ht : IsOpen t<GOAL>t = t ∩ closure s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h : b₂ < b₁<GOAL>Ioo a₁ b₁ ∩ Ioc a₂ b₂ = Ioc (max a₁ a₂) b₂
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>e : c.Embedding c'<VAR>inst✝ : e.IsRelIff<VAR>j k : ι<VAR>hk : c.Rel j k<GOAL>¬(c'.Rel (c'.prev (e.f k)) (e.f k) ∧ ∀ (i : ι), ¬c'.Rel (e.f i) (e.f k))
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>e : c.Embedding c'<VAR>inst✝ : e.IsRelIff<VAR>j k : ι<VAR>hk : c.Rel j k<GOAL>c'.Rel (c'.prev (e.f k)) (e.f k) → ∃ x, c'.Rel (e.f x) (e.f k)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>e : c.Embedding c'<VAR>inst✝ : e.IsRelIff<VAR>j k : ι<VAR>hk : c.Rel j k<VAR>a✝ : c'.Rel (c'.prev (e.f k)) (e.f k)<GOAL>∃ x, c'.Rel (e.f x) (e.f k)
<VAR>G : Type u_1<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : BorelSpace G<VAR>inst✝⁴ : LocallyCompactSpace G<VAR>inst✝³ : SecondCountableTopology G<VAR>μ ν : Measure G<VAR>inst✝² : SigmaFinite μ<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : ν.IsHaarMeasure<VAR>K : PositiveCompacts G<GOAL>μ ≪ ν
<VAR>G : Type u_1<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : BorelSpace G<VAR>inst✝⁴ : LocallyCompactSpace G<VAR>inst✝³ : SecondCountableTopology G<VAR>μ ν : Measure G<VAR>inst✝² : SigmaFinite μ<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : ν.IsHaarMeasure<VAR>K : PositiveCompacts G<VAR>h : haarMeasure K = ↑((haarMeasure K).haarScalarFactor ν) • ν<GOAL>μ ≪ ν
<VAR>G : Type u_1<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : BorelSpace G<VAR>inst✝⁴ : LocallyCompactSpace G<VAR>inst✝³ : SecondCountableTopology G<VAR>μ ν : Measure G<VAR>inst✝² : SigmaFinite μ<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : ν.IsHaarMeasure<VAR>K : PositiveCompacts G<VAR>h : haarMeasure K = ↑((haarMeasure K).haarScalarFactor ν) • ν<GOAL>(μ ↑K * ↑((haarMeasure K).haarScalarFactor ν)) • ν ≪ ν
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace 𝕜 E<VAR>ι✝ : Type u_3<VAR>inst✝⁶ : LinearOrder ι✝<VAR>inst✝⁵ : LocallyFiniteOrderBot ι✝<VAR>inst✝⁴ : IsWellOrder ι✝ fun x x_1 => x < x_1<VAR>ι : Type u_4<VAR>inst✝³ : LinearOrder ι<VAR>inst✝² : LocallyFiniteOrder ι<VAR>inst✝¹ : OrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<GOAL>gramSchmidt 𝕜 f ⊥ = f ⊥
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle y (y - x)).cos = ‖y‖ / ‖y - x‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<VAR>hs : (o.oangle y (y - x)).sign = 1<GOAL>(o.oangle y (y - x)).cos = ‖y‖ / ‖y - x‖
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>W : Subspace K V<VAR>v : V<GOAL>(∀ φ ∈ dualAnnihilator W, φ v = 0) ↔ v ∈ W
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t : Set α<VAR>f✝ g f : α → E<GOAL>⨍ (x : α), f x ∂μ = (μ univ).toReal⁻¹ • ∫ (x : α), f x ∂μ
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝² : Category.{v₂, u₂} J<VAR>X✝ : Type v₂<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝¹ : HasPullback f g<VAR>inst✝ : HasPushout f.op g.op<GOAL>pushout.inr f.op g.op ≫ (pullbackIsoUnopPushout f g).hom.op = (pullback.snd f g).op
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝² : Category.{v₂, u₂} J<VAR>X✝ : Type v₂<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝¹ : HasPullback f g<VAR>inst✝ : HasPushout f.op g.op<GOAL>(pushout.inr f.op g.op ≫ (pullbackIsoUnopPushout f g).hom.op).unop = (pullback.snd f g).op.unop
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝² : Category.{v₂, u₂} J<VAR>X✝ : Type v₂<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝¹ : HasPullback f g<VAR>inst✝ : HasPushout f.op g.op<GOAL>(pullbackIsoUnopPushout f g).hom ≫ (pushout.inr f.op g.op).unop = pullback.snd f g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : LocallyFiniteOrderBot α<VAR>inst✝ : DecidableEq α<VAR>b a✝ : α<GOAL>a✝ ∈ insert b (Iio b) ↔ a✝ ∈ Iic b
<VAR>k : Type u_1<VAR>inst✝⁹ : Field k<VAR>K : Type u_2<VAR>inst✝⁸ : Field K<VAR>F : Type u_3<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : NumberField K<VAR>inst✝⁵ : Algebra k K<VAR>inst✝⁴ : Algebra k F<VAR>inst✝³ : Algebra K F<VAR>inst✝² : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<VAR>inst✝¹ : NumberField k<VAR>inst✝ : IsGalois k K<GOAL>(filter (IsUnramified k) univ)ᶜ.card = (filter (IsUnramifiedIn K) univ)ᶜ.card * (finrank k K / 2)