ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝³ : Monoid N<VAR>hnontriv : Nontrivial ι<VAR>G : Type u_4<VAR>inst✝² : Group G<VAR>H : ι → Type u_5<VAR>inst✝¹ : (i : ι) → Group (H i)<VAR>f : (i : ι) → H i →* G<VAR>hcard : 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)<VAR>α : Type u_6<VAR>inst✝ : MulAction G α<VAR>X : ι → Set α<VAR>hXnonempty : ∀ (i : ι), (X i).Nonempty<VAR>hXdisj : Pairwise fun i j => Disjoint (X i) (X j)<VAR>hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i<VAR>i j k : ι<VAR>w : NeWord H i j<VAR>hhead : k ≠ i<VAR>hlast : k ≠ j<VAR>heq1 : (lift f) w.prod = 1<VAR>this : X k ⊆ X i<VAR>x : α<VAR>hx : x ∈ X k<GOAL>False
<VAR>R : Type u_1<VAR>inst✝⁶ : StrictOrderedCommSemiring 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>x✝ y z x : M<VAR>inst✝ : Nontrivial R<GOAL>SameRay R x x
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>z₁ z₂ : Cochain F G n<VAR>h : ∀ (p q : ℤ) (hpq : p + n = q), z₁.v p q hpq = z₂.v p q hpq<GOAL>z₁ = z₂
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>z₁ z₂ : Cochain F G n<VAR>h : ∀ (p q : ℤ) (hpq : p + n = q), z₁.v p q hpq = z₂.v p q hpq<VAR>p q : ℤ<VAR>hpq : p + n = q<GOAL>z₁ { p := p, q := q, hpq := hpq } = z₂ { p := p, q := q, hpq := hpq }
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : MeasurableSpace H<VAR>inst✝² : Group G<VAR>inst✝¹ : MeasurableMul G<VAR>μ : Measure G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>t : G<VAR>p : G → Prop<GOAL>(∀ᵐ (x : G) ∂μ, p (t * x)) ↔ ∀ᵐ (x : G) ∂μ, p x
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : MeasurableSpace H<VAR>inst✝² : Group G<VAR>inst✝¹ : MeasurableMul G<VAR>μ : Measure G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>t : G<VAR>p : G → Prop<GOAL>(∀ᵐ (x : G) ∂μ, p (t * x)) ↔ {x | p x} ∈ Filter.map (fun h => t * h) (ae μ)
<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 : α → ℝ≥0∞<VAR>s : Set α<GOAL>⨍⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α), f x ∂(μ s)⁻¹ • μ.restrict s
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : StarModule R A<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : StarRing B<VAR>inst✝ : StarModule R B<VAR>s : Set A<VAR>S : StarSubalgebra R A<GOAL>adjoin R s ≤ S ↔ s ≤ ↑S
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : StarModule R A<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : StarRing B<VAR>inst✝ : StarModule R B<VAR>s : Set A<VAR>S : StarSubalgebra R A<GOAL>s ∪ star s ⊆ ↑S ↔ s ≤ ↑S
<VAR>𝓕 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁✝ a₂✝ b b₁✝ b₂✝ : E<VAR>r r₁ r₂ : ℝ<VAR>a₁ a₂ b₁ b₂ : E<GOAL>edist (a₁ * a₂) (b₁ * b₂) ≤ edist a₁ b₁ + edist a₂ b₂
<VAR>𝓕 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁✝ a₂✝ b b₁✝ b₂✝ : E<VAR>r r₁ r₂ : ℝ<VAR>a₁ a₂ b₁ b₂ : E<GOAL>↑(nndist (a₁ * a₂) (b₁ * b₂)) ≤ ↑(nndist a₁ b₁) + ↑(nndist a₂ b₂)
<VAR>𝓕 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁✝ a₂✝ b b₁✝ b₂✝ : E<VAR>r r₁ r₂ : ℝ<VAR>a₁ a₂ b₁ b₂ : E<GOAL>nndist (a₁ * a₂) (b₁ * b₂) ≤ nndist a₁ b₁ + nndist a₂ b₂
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : MulOneClass M<VAR>inst✝³ : MulOneClass N<VAR>inst✝² : MulOneClass P<VAR>S : Submonoid M<VAR>A : Type u_4<VAR>inst✝¹ : SetLike A M<VAR>hA : SubmonoidClass A M<VAR>S' : A<VAR>F : Type u_5<VAR>inst✝ : FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>f : F<GOAL>closure (Set.range ⇑f) = mrange f
<VAR>𝕜 : Type u<VAR>𝕜' : Type u'<VAR>E : Type v<VAR>F : Type w<VAR>G : Type x<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : E<VAR>p : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f : 𝕜 → E<VAR>n : ℕ<VAR>z z₀ : 𝕜<VAR>y : Fin n → 𝕜<GOAL>(p n) y = (∏ i : Fin n, y i) • p.coeff n
<VAR>𝕜 : Type u<VAR>𝕜' : Type u'<VAR>E : Type v<VAR>F : Type w<VAR>G : Type x<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : E<VAR>p : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f : 𝕜 → E<VAR>n : ℕ<VAR>z z₀ : 𝕜<VAR>y : Fin n → 𝕜<VAR>x✝ : Fin n<GOAL>y x✝ = y x✝ • 1 x✝
<VAR>f : CauSeq ℂ ⇑abs'<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>i : ℕ<VAR>H : ∀ j ≥ i, abs' (↑f j - ↑f i) < ε<VAR>j : ℕ<VAR>ij : j ≥ i<GOAL>|(fun n => (↑f n).im) j - (fun n => (↑f n).im) i| < ε
<VAR>n : ℕ<VAR>hn1 : n ≠ 1<VAR>hn0 : ¬n = 0<VAR>hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1<GOAL>Irreducible (X ^ n - X - 1)
<VAR>n : ℕ<VAR>hn1 : n ≠ 1<VAR>hn0 : ¬n = 0<VAR>hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1<VAR>hn : 1 < n<GOAL>Irreducible (X ^ n - X - 1)
<VAR>n : ℕ<VAR>hn1 : n ≠ 1<VAR>hn0 : ¬n = 0<VAR>hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1<VAR>hn : 1 < n<VAR>h : Irreducible (map (Int.castRingHom ℚ) (X ^ n - X - 1))<GOAL>Irreducible (X ^ n - X - 1)
<VAR>n : ℕ<VAR>hn1 : n ≠ 1<VAR>hn0 : ¬n = 0<VAR>hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1<VAR>hn : 1 < n<GOAL>(X ^ n - X - 1).IsPrimitive
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝² : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>F : Cᵒᵖ ⥤ A<VAR>hF : Presheaf.IsSheaf J F<VAR>R : Dᵒᵖ ⥤ A<VAR>α : G.op ⋙ R ⟶ F<VAR>hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension<VAR>X : D<VAR>S : K.Cover X<VAR>s : Multifork (S.index R)<VAR>i : S.Arrow<GOAL>lift hF hR s ≫ R.map i.f.op = s.ι i
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝² : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>F : Cᵒᵖ ⥤ A<VAR>hF : Presheaf.IsSheaf J F<VAR>R : Dᵒᵖ ⥤ A<VAR>α : G.op ⋙ R ⟶ F<VAR>hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension<VAR>X : D<VAR>S : K.Cover X<VAR>s : Multifork (S.index R)<VAR>i : S.Arrow<GOAL>∀ (j : StructuredArrow (op i.Y) G.op), (lift hF hR s ≫ R.map i.f.op) ≫ ((Functor.RightExtension.mk R α).coneAt (op i.Y)).π.app j = s.ι i ≫ ((Functor.RightExtension.mk R α).coneAt (op i.Y)).π.app j
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝² : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>F : Cᵒᵖ ⥤ A<VAR>hF : Presheaf.IsSheaf J F<VAR>R : Dᵒᵖ ⥤ A<VAR>α : G.op ⋙ R ⟶ F<VAR>hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension<VAR>X : D<VAR>S : K.Cover X<VAR>s : Multifork (S.index R)<VAR>i : S.Arrow<VAR>j : StructuredArrow (op i.Y) G.op<GOAL>(lift hF hR s ≫ R.map i.f.op) ≫ ((Functor.RightExtension.mk R α).coneAt (op i.Y)).π.app j = s.ι i ≫ ((Functor.RightExtension.mk R α).coneAt (op i.Y)).π.app j
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝² : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>F : Cᵒᵖ ⥤ A<VAR>hF : Presheaf.IsSheaf J F<VAR>R : Dᵒᵖ ⥤ A<VAR>α : G.op ⋙ R ⟶ F<VAR>hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension<VAR>X : D<VAR>S : K.Cover X<VAR>s : Multifork (S.index R)<VAR>i : S.Arrow<VAR>j : StructuredArrow (op i.Y) G.op<VAR>eq : lift hF hR s ≫ R.map (StructuredArrow.mk (i.f.op ≫ j.hom)).hom ≫ α.app (StructuredArrow.mk (i.f.op ≫ j.hom)).right = liftAux hF α s (StructuredArrow.mk (i.f.op ≫ j.hom)).hom.unop<GOAL>(lift hF hR s ≫ R.map i.f.op) ≫ ((Functor.RightExtension.mk R α).coneAt (op i.Y)).π.app j = s.ι i ≫ ((Functor.RightExtension.mk R α).coneAt (op i.Y)).π.app j
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝² : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>F : Cᵒᵖ ⥤ A<VAR>hF : Presheaf.IsSheaf J F<VAR>R : Dᵒᵖ ⥤ A<VAR>α : G.op ⋙ R ⟶ F<VAR>hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension<VAR>X : D<VAR>S : K.Cover X<VAR>s : Multifork (S.index R)<VAR>i : S.Arrow<VAR>j : StructuredArrow (op i.Y) G.op<VAR>eq : lift hF hR s ≫ R.map (i.f.op ≫ j.hom) ≫ α.app j.right = liftAux hF α s (j.hom.unop ≫ i.f)<GOAL>(lift hF hR s ≫ R.map i.f.op) ≫ R.map j.hom ≫ α.app j.right = s.ι i ≫ R.map j.hom ≫ α.app j.right
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝² : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>F : Cᵒᵖ ⥤ A<VAR>hF : Presheaf.IsSheaf J F<VAR>R : Dᵒᵖ ⥤ A<VAR>α : G.op ⋙ R ⟶ F<VAR>hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension<VAR>X : D<VAR>S : K.Cover X<VAR>s : Multifork (S.index R)<VAR>i : S.Arrow<VAR>j : StructuredArrow (op i.Y) G.op<VAR>eq : lift hF hR s ≫ R.map i.f.op ≫ R.map j.hom ≫ α.app j.right = liftAux hF α s (j.hom.unop ≫ i.f)<GOAL>(lift hF hR s ≫ R.map i.f.op) ≫ R.map j.hom ≫ α.app j.right = s.ι i ≫ R.map j.hom ≫ α.app j.right
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝² : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>F : Cᵒᵖ ⥤ A<VAR>hF : Presheaf.IsSheaf J F<VAR>R : Dᵒᵖ ⥤ A<VAR>α : G.op ⋙ R ⟶ F<VAR>hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension<VAR>X : D<VAR>S : K.Cover X<VAR>s : Multifork (S.index R)<VAR>i : S.Arrow<VAR>j : StructuredArrow (op i.Y) G.op<VAR>eq : lift hF hR s ≫ R.map i.f.op ≫ R.map j.hom ≫ α.app j.right = liftAux hF α s (j.hom.unop ≫ i.f)<GOAL>liftAux hF α s (j.hom.unop ≫ i.f) = s.ι i ≫ R.map j.hom ≫ α.app j.right
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => x - a) '' Ici b = Ici (b - a)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>α : Type u_1<VAR>F : α → ℚ<VAR>t : ℚ<VAR>s : Finset α<VAR>hF : ∀ i ∈ s, padicNorm p (F i) ≤ t<VAR>ht : 0 ≤ t<GOAL>padicNorm p (∑ i ∈ s, F i) ≤ t
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>α : Type u_1<VAR>F : α → ℚ<VAR>t : ℚ<VAR>ht : 0 ≤ t<VAR>hF : ∀ i ∈ ∅, padicNorm p (F i) ≤ t<GOAL>padicNorm p (∑ i ∈ ∅, F i) ≤ t
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>α : Type u_1<VAR>F : α → ℚ<VAR>t : ℚ<VAR>s : Finset α<VAR>hF : ∀ i ∈ s, padicNorm p (F i) ≤ t<VAR>ht : 0 ≤ t<VAR>hs : s.Nonempty<GOAL>padicNorm p (∑ i ∈ s, F i) ≤ t
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y p₂ : P<VAR>h : p₂ ∈ s<GOAL>s.WOppSide x y ↔ y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y p₂ : P<VAR>h : p₂ ∈ s<GOAL>(y ∈ s ∨ ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (p₂_1 -ᵥ x)) ↔ y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder β<VAR>s t : Finset α<VAR>f : Finset α → β<VAR>inst✝ : DecidableEq α<GOAL>Monotone f ↔ ∀ (s : Finset α) ⦃a : α⦄, a ∉ s → f s ≤ f (insert a s)
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>G : Type u_3<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → 𝕜 → G<VAR>g : 𝕜 → G<VAR>f' : ι → 𝕜 → G<VAR>g' : 𝕜 → G<VAR>x : 𝕜<VAR>l' : Filter 𝕜<VAR>hf' : UniformCauchySeqOnFilter f' l l'<GOAL>UniformCauchySeqOnFilter (fun n z => ContinuousLinearMap.smulRight 1 (f' n z)) l l'
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>G : Type u_3<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → 𝕜 → G<VAR>g : 𝕜 → G<VAR>f' : ι → 𝕜 → G<VAR>g' : 𝕜 → G<VAR>x : 𝕜<VAR>l' : Filter 𝕜<VAR>hf' : ∀ ε > 0, ∀ᶠ (n : (ι × ι) × 𝕜) in (l ×ˢ l) ×ˢ l', dist (0 n.2) (f' n.1.1 n.2 - f' n.1.2 n.2) < ε<GOAL>∀ ε > 0, ∀ᶠ (n : (ι × ι) × 𝕜) in (l ×ˢ l) ×ˢ l', dist (0 n.2) (ContinuousLinearMap.smulRight 1 (f' n.1.1 n.2) - ContinuousLinearMap.smulRight 1 (f' n.1.2 n.2)) < ε
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>G : Type u_3<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → 𝕜 → G<VAR>g : 𝕜 → G<VAR>f' : ι → 𝕜 → G<VAR>g' : 𝕜 → G<VAR>x : 𝕜<VAR>l' : Filter 𝕜<VAR>hf' : ∀ ε > 0, ∀ᶠ (n : (ι × ι) × 𝕜) in (l ×ˢ l) ×ˢ l', dist (0 n.2) (f' n.1.1 n.2 - f' n.1.2 n.2) < ε<VAR>ε : ℝ<VAR>hε : ε > 0<GOAL>∀ᶠ (n : (ι × ι) × 𝕜) in (l ×ˢ l) ×ˢ l', dist (0 n.2) (ContinuousLinearMap.smulRight 1 (f' n.1.1 n.2) - ContinuousLinearMap.smulRight 1 (f' n.1.2 n.2)) < ε
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>G : Type u_3<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → 𝕜 → G<VAR>g : 𝕜 → G<VAR>f' : ι → 𝕜 → G<VAR>g' : 𝕜 → G<VAR>x : 𝕜<VAR>l' : Filter 𝕜<VAR>hf' : ∀ ε > 0, ∀ᶠ (n : (ι × ι) × 𝕜) in (l ×ˢ l) ×ˢ l', dist (0 n.2) (f' n.1.1 n.2 - f' n.1.2 n.2) < ε<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>q : ℝ<VAR>hq : 0 < q<VAR>hq' : q < ε<GOAL>∀ᶠ (n : (ι × ι) × 𝕜) in (l ×ˢ l) ×ˢ l', dist (0 n.2) (ContinuousLinearMap.smulRight 1 (f' n.1.1 n.2) - ContinuousLinearMap.smulRight 1 (f' n.1.2 n.2)) < ε
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>G : Type u_3<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → 𝕜 → G<VAR>g : 𝕜 → G<VAR>f' : ι → 𝕜 → G<VAR>g' : 𝕜 → G<VAR>x : 𝕜<VAR>l' : Filter 𝕜<VAR>hf' : ∀ ε > 0, ∀ᶠ (n : (ι × ι) × 𝕜) in (l ×ˢ l) ×ˢ l', dist (0 n.2) (f' n.1.1 n.2 - f' n.1.2 n.2) < ε<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>q : ℝ<VAR>hq : 0 < q<VAR>hq' : q < ε<GOAL>∀ (x : (ι × ι) × 𝕜), dist (0 x.2) (f' x.1.1 x.2 - f' x.1.2 x.2) < q → dist (0 x.2) (ContinuousLinearMap.smulRight 1 (f' x.1.1 x.2) - ContinuousLinearMap.smulRight 1 (f' x.1.2 x.2)) < ε
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>G : Type u_3<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → 𝕜 → G<VAR>g : 𝕜 → G<VAR>f' : ι → 𝕜 → G<VAR>g' : 𝕜 → G<VAR>x : 𝕜<VAR>l' : Filter 𝕜<VAR>hf' : ∀ ε > 0, ∀ᶠ (n : (ι × ι) × 𝕜) in (l ×ˢ l) ×ˢ l', dist (0 n.2) (f' n.1.1 n.2 - f' n.1.2 n.2) < ε<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>q : ℝ<VAR>hq : 0 < q<VAR>hq' : q < ε<VAR>n : (ι × ι) × 𝕜<VAR>hn : dist (0 n.2) (f' n.1.1 n.2 - f' n.1.2 n.2) < q<GOAL>dist (0 n.2) (ContinuousLinearMap.smulRight 1 (f' n.1.1 n.2) - ContinuousLinearMap.smulRight 1 (f' n.1.2 n.2)) < ε
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>G : Type u_3<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → 𝕜 → G<VAR>g : 𝕜 → G<VAR>f' : ι → 𝕜 → G<VAR>g' : 𝕜 → G<VAR>x : 𝕜<VAR>l' : Filter 𝕜<VAR>hf' : ∀ ε > 0, ∀ᶠ (n : (ι × ι) × 𝕜) in (l ×ˢ l) ×ˢ l', dist (0 n.2) (f' n.1.1 n.2 - f' n.1.2 n.2) < ε<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>q : ℝ<VAR>hq : 0 < q<VAR>hq' : q < ε<VAR>n : (ι × ι) × 𝕜<VAR>hn : dist (0 n.2) (f' n.1.1 n.2 - f' n.1.2 n.2) < q<GOAL>dist (0 n.2) (ContinuousLinearMap.smulRight 1 (f' n.1.1 n.2) - ContinuousLinearMap.smulRight 1 (f' n.1.2 n.2)) ≤ q
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>G : Type u_3<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → 𝕜 → G<VAR>g : 𝕜 → G<VAR>f' : ι → 𝕜 → G<VAR>g' : 𝕜 → G<VAR>x : 𝕜<VAR>l' : Filter 𝕜<VAR>hf' : ∀ ε > 0, ∀ᶠ (n : (ι × ι) × 𝕜) in (l ×ˢ l) ×ˢ l', dist (0 n.2) (f' n.1.1 n.2 - f' n.1.2 n.2) < ε<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>q : ℝ<VAR>hq : 0 < q<VAR>hq' : q < ε<VAR>n : (ι × ι) × 𝕜<VAR>hn : ‖f' n.1.1 n.2 - f' n.1.2 n.2‖ < q<GOAL>‖ContinuousLinearMap.smulRight 1 (f' n.1.1 n.2) - ContinuousLinearMap.smulRight 1 (f' n.1.2 n.2)‖ ≤ q
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>G : Type u_3<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → 𝕜 → G<VAR>g : 𝕜 → G<VAR>f' : ι → 𝕜 → G<VAR>g' : 𝕜 → G<VAR>x : 𝕜<VAR>l' : Filter 𝕜<VAR>hf' : ∀ ε > 0, ∀ᶠ (n : (ι × ι) × 𝕜) in (l ×ˢ l) ×ˢ l', dist (0 n.2) (f' n.1.1 n.2 - f' n.1.2 n.2) < ε<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>q : ℝ<VAR>hq : 0 < q<VAR>hq' : q < ε<VAR>n : (ι × ι) × 𝕜<VAR>hn : ‖f' n.1.1 n.2 - f' n.1.2 n.2‖ < q<GOAL>∀ (x : 𝕜), ‖(ContinuousLinearMap.smulRight 1 (f' n.1.1 n.2) - ContinuousLinearMap.smulRight 1 (f' n.1.2 n.2)) x‖ ≤ q * ‖x‖
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>G : Type u_3<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → 𝕜 → G<VAR>g : 𝕜 → G<VAR>f' : ι → 𝕜 → G<VAR>g' : 𝕜 → G<VAR>x : 𝕜<VAR>l' : Filter 𝕜<VAR>hf' : ∀ ε > 0, ∀ᶠ (n : (ι × ι) × 𝕜) in (l ×ˢ l) ×ˢ l', dist (0 n.2) (f' n.1.1 n.2 - f' n.1.2 n.2) < ε<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>q : ℝ<VAR>hq : 0 < q<VAR>hq' : q < ε<VAR>n : (ι × ι) × 𝕜<VAR>hn : ‖f' n.1.1 n.2 - f' n.1.2 n.2‖ < q<VAR>z : 𝕜<GOAL>‖(ContinuousLinearMap.smulRight 1 (f' n.1.1 n.2) - ContinuousLinearMap.smulRight 1 (f' n.1.2 n.2)) z‖ ≤ q * ‖z‖
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>G : Type u_3<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → 𝕜 → G<VAR>g : 𝕜 → G<VAR>f' : ι → 𝕜 → G<VAR>g' : 𝕜 → G<VAR>x : 𝕜<VAR>l' : Filter 𝕜<VAR>hf' : ∀ ε > 0, ∀ᶠ (n : (ι × ι) × 𝕜) in (l ×ˢ l) ×ˢ l', dist (0 n.2) (f' n.1.1 n.2 - f' n.1.2 n.2) < ε<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>q : ℝ<VAR>hq : 0 < q<VAR>hq' : q < ε<VAR>n : (ι × ι) × 𝕜<VAR>hn : ‖f' n.1.1 n.2 - f' n.1.2 n.2‖ < q<VAR>z : 𝕜<GOAL>‖z • f' n.1.1 n.2 - z • f' n.1.2 n.2‖ ≤ q * ‖z‖
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>G : Type u_3<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → 𝕜 → G<VAR>g : 𝕜 → G<VAR>f' : ι → 𝕜 → G<VAR>g' : 𝕜 → G<VAR>x : 𝕜<VAR>l' : Filter 𝕜<VAR>hf' : ∀ ε > 0, ∀ᶠ (n : (ι × ι) × 𝕜) in (l ×ˢ l) ×ˢ l', dist (0 n.2) (f' n.1.1 n.2 - f' n.1.2 n.2) < ε<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>q : ℝ<VAR>hq : 0 < q<VAR>hq' : q < ε<VAR>n : (ι × ι) × 𝕜<VAR>hn : ‖f' n.1.1 n.2 - f' n.1.2 n.2‖ < q<VAR>z : 𝕜<GOAL>‖f' n.1.1 n.2 - f' n.1.2 n.2‖ * ‖z‖ ≤ q * ‖z‖
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : Preorder β<VAR>l : Filter α<VAR>f₁ f₂ : α → β<VAR>h : f₁ ≤ᶠ[l] f₂<VAR>h₁ : Tendsto f₁ l atTop<VAR>b : β<GOAL>∀ᶠ (a : α) in l, b ≤ f₂ a
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>M : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} M<VAR>inst✝ : MonoidalCategory M<VAR>F : MonoidalFunctor M (C ⥤ C)<VAR>n : M<VAR>X : C<GOAL>(F.obj n).map (F.ε.app X) ≫ (F.μ (𝟙_ M) n).app X ≫ (F.map (λ_ n).hom).app X = 𝟙 ((F.obj n).obj ((𝟙_ (C ⥤ C)).obj X))
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>M : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} M<VAR>inst✝ : MonoidalCategory M<VAR>F : MonoidalFunctor M (C ⥤ C)<VAR>n : M<VAR>X : C<VAR>this : (λ_ (F.obj n)).hom.app X = (F.ε ▷ F.obj n ≫ F.μ (𝟙_ M) n ≫ F.map (λ_ n).hom).app X<GOAL>(F.obj n).map (F.ε.app X) ≫ (F.μ (𝟙_ M) n).app X ≫ (F.map (λ_ n).hom).app X = 𝟙 ((F.obj n).obj ((𝟙_ (C ⥤ C)).obj X))
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>M : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} M<VAR>inst✝ : MonoidalCategory M<VAR>F : MonoidalFunctor M (C ⥤ C)<VAR>n : M<VAR>X : C<VAR>this : 𝟙 ((F.obj n).obj X) = (F.obj n).map (F.ε.app X) ≫ (F.μ (𝟙_ M) n).app X ≫ (F.map (λ_ n).hom).app X<GOAL>(F.obj n).map (F.ε.app X) ≫ (F.μ (𝟙_ M) n).app X ≫ (F.map (λ_ n).hom).app X = 𝟙 ((F.obj n).obj ((𝟙_ (C ⥤ C)).obj X))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>n : ℕ<GOAL>image castSucc univ = {last n}ᶜ
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P✝ Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>P : Cᵒᵖ ⥤ Type w<VAR>x : FamilyOfElements P (singleton (𝟙 X))<VAR>a✝ : x.Compatible<GOAL>∃! t, x.IsAmalgamation t
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P✝ Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>P : Cᵒᵖ ⥤ Type w<VAR>x : FamilyOfElements P (singleton (𝟙 X))<VAR>a✝ : x.Compatible<GOAL>(fun t => x.IsAmalgamation t) (x (𝟙 X) ⋯)
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P✝ Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>P : Cᵒᵖ ⥤ Type w<VAR>x : FamilyOfElements P (singleton (𝟙 X))<VAR>a✝ : x.Compatible<GOAL>∀ (y : P.obj (op X)), (fun t => x.IsAmalgamation t) y → y = x (𝟙 X) ⋯
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : CauSeq ℚ_[p] ⇑padicNormE<VAR>q : ℚ_[p]<VAR>ε : ℚ<VAR>hε : 0 < ε<VAR>q' : CauSeq ℚ (padicNorm p)<VAR>this : ∃ N, ∀ m ≥ N, ∀ n ≥ N, padicNorm p (↑q' m - ↑q' n) < ε<VAR>N : ℕ<VAR>hN : ∀ m ≥ N, ∀ n ≥ N, padicNorm p (↑q' m - ↑q' n) < ε<GOAL>(q' - const (padicNorm p) (↑q' N)).norm < ε
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : CauSeq ℚ_[p] ⇑padicNormE<VAR>q : ℚ_[p]<VAR>ε : ℚ<VAR>hε : 0 < ε<VAR>q' : CauSeq ℚ (padicNorm p)<VAR>this : ∃ N, ∀ m ≥ N, ∀ n ≥ N, padicNorm p (↑q' m - ↑q' n) < ε<VAR>N : ℕ<VAR>hN : ∀ m ≥ N, ∀ n ≥ N, padicNorm p (↑q' m - ↑q' n) < ε<VAR>heq : q' - const (padicNorm p) (↑q' N) ≈ 0<GOAL>(q' - const (padicNorm p) (↑q' N)).norm < ε
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : CauSeq ℚ_[p] ⇑padicNormE<VAR>q : ℚ_[p]<VAR>ε : ℚ<VAR>hε : 0 < ε<VAR>q' : CauSeq ℚ (padicNorm p)<VAR>this : ∃ N, ∀ m ≥ N, ∀ n ≥ N, padicNorm p (↑q' m - ↑q' n) < ε<VAR>N : ℕ<VAR>hN : ∀ m ≥ N, ∀ n ≥ N, padicNorm p (↑q' m - ↑q' n) < ε<VAR>hne' : ¬q' - const (padicNorm p) (↑q' N) ≈ 0<GOAL>(q' - const (padicNorm p) (↑q' N)).norm < ε
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u_1<VAR>x✝ : α 0<VAR>q : (i : Fin (n + 1)) → α i<VAR>p✝ : (i : Fin n) → α i.succ<VAR>i✝ : Fin n<VAR>y : α i✝.succ<VAR>z : α 0<VAR>inst✝ : (i : Fin (n + 1)) → Preorder (α i)<VAR>i : Fin (n + 1)<VAR>x : α i<VAR>q₁ q₂ : (j : Fin (n + 1)) → α j<VAR>hx : x ∉ Icc (q₁ i) (q₂ i)<VAR>p : (j : Fin n) → α (i.succAbove j)<GOAL>p ∈ i.insertNth x ⁻¹' Icc q₁ q₂ ↔ p ∈ ∅
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>α : ι → Type u_6<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : DecidableEq κ<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : (i : ι) → DecidableEq (α i)<VAR>s : (i : ι) → Finset (α i)<GOAL>(piFinset s).card = ∏ i : ι, (s i).card
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ τ : Perm α<VAR>h : σ.Disjoint τ<GOAL>(σ * τ).cycleType = σ.cycleType + τ.cycleType
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ τ : Perm α<VAR>h : σ.Disjoint τ<GOAL>σ.cycleFactorsFinset.val.Disjoint τ.cycleFactorsFinset.val