ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f g : X → Y<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>hs : IsOpen s<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hspec : ∀ (x : X), f x ⤳ g x<VAR>this : ∀ (U : Set Y), IsOpen U → g ⁻¹' U ⊆ f ⁻¹' U<VAR>U : Set Y<VAR>hU : IsOpen U<GOAL>IsOpen (f ⁻¹' U ∩ s ∪ g ⁻¹' U)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>ht : MeasurableSet t<VAR>hs_finite : μ s ≠ ⊤<VAR>ht_finite : μ t ≠ ⊤<VAR>h_inter : s ∩ t = ∅<VAR>x : F<GOAL>(weightedSMul μ (s ∪ t)) x = (weightedSMul μ s + weightedSMul μ t) x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>p : R[X]<VAR>n : ℕ<GOAL>(p.scaleRoots 0).coeff n = (p.leadingCoeff • X ^ p.natDegree).coeff n
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>p : R[X]<VAR>n : ℕ<GOAL>(if p.natDegree ≤ n then p.coeff n else 0) = if n = p.natDegree then p.leadingCoeff else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>n : ℕ<VAR>h : 1 < n<GOAL>(fun x => ‖x‖ ^ n) =o[𝓝 0] fun x => x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>n : ℕ<VAR>h : 1 < n<VAR>this : (fun x => ‖x‖ ^ n) =o[𝓝 0] fun x => ‖x‖ ^ 1<GOAL>(fun x => ‖x‖ ^ n) =o[𝓝 0] fun x => x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>n : ℕ<VAR>h : 1 < n<VAR>this : (fun x => ‖x‖ ^ n) =o[𝓝 0] fun x => ‖x‖<GOAL>(fun x => ‖x‖ ^ n) =o[𝓝 0] fun x => x
<VAR>F : 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✝⁸ : FunLike F α β<VAR>inst✝⁷ : Lattice α<VAR>inst✝⁶ : Lattice β<VAR>inst✝⁵ : Lattice γ<VAR>inst✝⁴ : Lattice δ<VAR>inst✝³ : BoundedOrder α<VAR>inst✝² : BoundedOrder β<VAR>inst✝¹ : BoundedOrder γ<VAR>inst✝ : BoundedOrder δ<VAR>g : BoundedLatticeHom β γ<VAR>f₁ f₂ : BoundedLatticeHom α β<VAR>hg : Injective ⇑g<VAR>h : g.comp f₁ = g.comp f₂<VAR>a : α<GOAL>g (f₁ a) = g (f₂ a)
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<GOAL>Algebra.IsAlgebraic R A ↔ ∀ x ∈ ⊤, IsAlgebraic R x
<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>r.toNNReal = ⟨r, hr⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>xs : List α<VAR>z : Sym2 α<GOAL>z ∈ xs.sym2 ↔ ∀ y ∈ z, y ∈ xs
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>xs : List α<VAR>z : Sym2 α<VAR>a b : α<GOAL>s(a, b) ∈ xs.sym2 ↔ ∀ y ∈ s(a, b), y ∈ xs
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>H K : Subgroup G<VAR>S T✝ : Set G<VAR>F : Type u_2<VAR>inst✝² : Group F<VAR>inst✝¹ : MulAction F G<VAR>inst✝ : QuotientAction F H<VAR>f : F<VAR>T : ↑(leftTransversals ↑H)<VAR>q : G ⧸ H<GOAL>↑((toEquiv ⋯) q) = f • ↑((toEquiv ⋯) (f⁻¹ • q))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f g : X → Y<VAR>t : Set (SeparationQuotient X)<GOAL>comap mk (𝓝ˢ t) = 𝓝ˢ (mk ⁻¹' t)
<VAR>α✝ : Type u_1<VAR>β : α✝ → Type u_2<VAR>α : Type u_3<VAR>f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)<VAR>hc : Continuous f<GOAL>Part.fix ⇑f = f (Part.fix ⇑f)
<VAR>α✝ : Type u_1<VAR>β : α✝ → Type u_2<VAR>α : Type u_3<VAR>f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)<VAR>hc : Continuous f<GOAL>ωSup (approxChain f) = ωSup ((approxChain f).map f)
<VAR>α✝ : Type u_1<VAR>β : α✝ → Type u_2<VAR>α : Type u_3<VAR>f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)<VAR>hc : Continuous f<GOAL>ωSup (approxChain f) ≤ ωSup ((approxChain f).map f)
<VAR>α✝ : Type u_1<VAR>β : α✝ → Type u_2<VAR>α : Type u_3<VAR>f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)<VAR>hc : Continuous f<GOAL>ωSup ((approxChain f).map f) ≤ ωSup (approxChain f)
<VAR>D : GlueData<VAR>U : Set ↑↑D.glued.toPresheafedSpace<GOAL>IsOpen U ↔ ∀ (i : D.J), IsOpen (⇑(D.ι i).val.base ⁻¹' U)
<VAR>D : GlueData<VAR>U : Set ↑↑D.glued.toPresheafedSpace<GOAL>IsOpen (⇑(TopCat.homeoOfIso D.isoCarrier.symm) ⁻¹' U) ↔ ∀ (i : D.J), IsOpen (⇑(D.ι i).val.base ⁻¹' U)
<VAR>D : GlueData<VAR>U : Set ↑↑D.glued.toPresheafedSpace<GOAL>(∀ (i : D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.J), IsOpen (⇑(D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i) ⁻¹' (⇑(TopCat.homeoOfIso D.isoCarrier.symm) ⁻¹' U))) ↔ ∀ (i : D.J), IsOpen (⇑(D.ι i).val.base ⁻¹' U)
<VAR>D : GlueData<VAR>U : Set ↑↑D.glued.toPresheafedSpace<GOAL>∀ (a : D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.J), IsOpen (⇑(D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι a) ⁻¹' (⇑(TopCat.homeoOfIso D.isoCarrier.symm) ⁻¹' U)) ↔ IsOpen (⇑(D.ι a).val.base ⁻¹' U)
<VAR>D : GlueData<VAR>U : Set ↑↑D.glued.toPresheafedSpace<VAR>i : D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.J<GOAL>IsOpen (⇑(D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i) ⁻¹' (⇑(TopCat.homeoOfIso D.isoCarrier.symm) ⁻¹' U)) ↔ IsOpen (⇑(D.ι i).val.base ⁻¹' U)
<VAR>D : GlueData<VAR>U : Set ↑↑D.glued.toPresheafedSpace<VAR>i : D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.J<GOAL>IsOpen (⇑(TopCat.homeoOfIso D.isoCarrier.symm) ∘ ⇑(D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i) ⁻¹' U) ↔ IsOpen (⇑(D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i ≫ D.isoCarrier.inv) ⁻¹' U)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : DecidableEq (ι → α)<VAR>s : Finset α<VAR>f : ι → α<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<GOAL>s.piDiag ι ⊆ Fintype.piFinset fun x => s
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>α : Type v<VAR>β : Type w<VAR>ι : Type u_6<VAR>M : Matrix m n α<VAR>i : m<VAR>j : n<VAR>b : n → α<VAR>c : m → α<VAR>inst✝ : DecidableEq m<VAR>i✝ : n<VAR>j✝ : m<GOAL>Mᵀ.updateColumn i b i✝ j✝ = (M.updateRow i b)ᵀ i✝ j✝
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>α : Type v<VAR>β : Type w<VAR>ι : Type u_6<VAR>M : Matrix m n α<VAR>i : m<VAR>j : n<VAR>b : n → α<VAR>c : m → α<VAR>inst✝ : DecidableEq m<VAR>i✝ : n<VAR>j✝ : m<GOAL>(if j✝ = i then b i✝ else Mᵀ i✝ j✝) = if j✝ = i then b i✝ else M j✝ i✝
<VAR>a b c d✝ n k : ℕ<VAR>p q : ℕ → Prop<VAR>d : ℕ<VAR>h1 : n * k < n * d<VAR>h2 : n * d < n * (k + 1)<GOAL>False
<VAR>a b c d✝ n k : ℕ<VAR>p q : ℕ → Prop<VAR>d : ℕ<VAR>h1 : n * k < n * d<VAR>h2 : n * d < n * (k + 1)<VAR>this : k < d<GOAL>False
<VAR>a b c d✝ n k : ℕ<VAR>p q : ℕ → Prop<VAR>d : ℕ<VAR>h1 : n * k < n * d<VAR>h2 : n * d < n * (k + 1)<VAR>this✝ : k < d<VAR>this : d < k + 1<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ : Set α<VAR>f : α → β<VAR>s t : Set α<VAR>hs : autoParam s.Finite _auto✝<GOAL>(s ∩ t).ncard + (s \ t).ncard = s.ncard
<VAR>P : Type u_1<VAR>inst✝¹ : LE P<VAR>inst✝ : OrderTop P<VAR>I : Ideal P<VAR>h : ⊤ ∈ I<VAR>x✝ : P<GOAL>x✝ ∈ ↑I ↔ x✝ ∈ ↑⊤
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f : F[X]<VAR>hm : f.Monic<VAR>hs : Splits (RingHom.id F) f<VAR>h : f.natSepDegree = 1<GOAL>∃ m y, m ≠ 0 ∧ f = (X - C y) ^ m
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f : F[X]<VAR>hm : f.Monic<VAR>hs : Splits (RingHom.id F) f<VAR>h : f.natSepDegree = 1<VAR>h1 : f = (Multiset.map (fun a => X - C a) f.roots).prod<GOAL>∃ m y, m ≠ 0 ∧ f = (X - C y) ^ m
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f : F[X]<VAR>hm : f.Monic<VAR>hs : Splits (RingHom.id F) f<VAR>h : f.natSepDegree = 1<VAR>h1 : f = (Multiset.map (fun a => X - C a) f.roots).prod<VAR>h2 : (f.aroots F).toFinset.card = f.natSepDegree<GOAL>∃ m y, m ≠ 0 ∧ f = (X - C y) ^ m
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f : F[X]<VAR>hm : f.Monic<VAR>hs : Splits (RingHom.id F) f<VAR>h : f.natSepDegree = 1<VAR>h1 : f = (Multiset.map (fun a => X - C a) f.roots).prod<VAR>h2 : Multiset.card f.roots ≠ 0 ∧ ∃ a, f.roots = Multiset.card f.roots • {a}<GOAL>∃ m y, m ≠ 0 ∧ f = (X - C y) ^ m
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f : F[X]<VAR>hm : f.Monic<VAR>hs : Splits (RingHom.id F) f<VAR>h : f.natSepDegree = 1<VAR>h1 : f = (Multiset.map (fun a => X - C a) f.roots).prod<VAR>h2 : Multiset.card f.roots ≠ 0<VAR>y : F<VAR>h3 : f.roots = Multiset.card f.roots • {y}<GOAL>∃ m y, m ≠ 0 ∧ f = (X - C y) ^ m
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hg : DifferentiableAt 𝕜 g x<GOAL>DifferentiableAt 𝕜 (fun y => f y + g y) x ↔ DifferentiableAt 𝕜 f x
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hg : DifferentiableAt 𝕜 g x<VAR>h : DifferentiableAt 𝕜 (fun y => f y + g y) x<GOAL>DifferentiableAt 𝕜 f x
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hf : AEStronglyMeasurable f μ<VAR>A : ℝ<VAR>h'f : 0 ≤ f<GOAL>∫ (x : α), truncation f A x ∂μ = ∫ (y : ℝ) in 0 ..A, y ∂Measure.map f μ
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : Monoid R<VAR>inst✝³ : AddMonoid M<VAR>inst✝² : DistribMulAction R M<VAR>inst✝¹ : DistribMulAction Rᵐᵒᵖ M<VAR>inst✝ : SMulCommClass R Rᵐᵒᵖ M<VAR>x : tsze R M<VAR>n : ℕ<VAR>h : x.snd <• x.fst = x.fst •> x.snd<GOAL>(x ^ n).snd = n •> x.fst ^ n.pred •> x.snd
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : Monoid R<VAR>inst✝³ : AddMonoid M<VAR>inst✝² : DistribMulAction R M<VAR>inst✝¹ : DistribMulAction Rᵐᵒᵖ M<VAR>inst✝ : SMulCommClass R Rᵐᵒᵖ M<VAR>x : tsze R M<VAR>n : ℕ<VAR>h : x.snd <• x.fst = x.fst •> x.snd<GOAL>(List.map (fun i => x.fst ^ (n.pred - i + i) •> x.snd) (List.range n)).sum = n •> x.fst ^ n.pred •> x.snd
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>m : M<VAR>s : ↥S<GOAL>1 • mk m s = mk m s
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>m : M<VAR>s : ↥S<GOAL>IsLocalization.mk' T 1 1 • mk m s = mk m s
<VAR>x : ℝ<VAR>h : |x| < 1<VAR>n : ℕ<VAR>F : ℝ → ℝ := fun x => ∑ i ∈ Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)<VAR>F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)<GOAL>|∑ i ∈ Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)| ≤ |x| ^ (n + 1) / (1 - |x|)
<VAR>x : ℝ<VAR>h : |x| < 1<VAR>n : ℕ<VAR>F : ℝ → ℝ := fun x => ∑ i ∈ Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)<VAR>F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)<VAR>A : ∀ y ∈ Set.Ioo (-1) 1, HasDerivAt F (F' y) y<GOAL>|∑ i ∈ Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)| ≤ |x| ^ (n + 1) / (1 - |x|)
<VAR>x : ℝ<VAR>h : |x| < 1<VAR>n : ℕ<VAR>F : ℝ → ℝ := fun x => ∑ i ∈ Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)<VAR>F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)<VAR>A : ∀ y ∈ Set.Ioo (-1) 1, HasDerivAt F (F' y) y<VAR>B : ∀ y ∈ Set.Icc (-|x|) |x|, |F' y| ≤ |x| ^ n / (1 - |x|)<GOAL>|∑ i ∈ Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)| ≤ |x| ^ (n + 1) / (1 - |x|)
<VAR>x : ℝ<VAR>h : |x| < 1<VAR>n : ℕ<VAR>F : ℝ → ℝ := fun x => ∑ i ∈ Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)<VAR>F' : ℝ → ℝ := fun x => -x ^ n / (1 - x)<VAR>A : ∀ y ∈ Set.Ioo (-1) 1, HasDerivAt F (F' y) y<VAR>B : ∀ y ∈ Set.Icc (-|x|) |x|, |F' y| ≤ |x| ^ n / (1 - |x|)<VAR>C : ‖F x - F 0‖ ≤ |x| ^ n / (1 - |x|) * ‖x - 0‖<GOAL>|∑ i ∈ Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)| ≤ |x| ^ (n + 1) / (1 - |x|)
<VAR>n : ℕ<VAR>α : Type u_1<VAR>v : Vector α 1<GOAL>v.toList = [v.head]
<VAR>n : ℕ<VAR>α : Type u_1<VAR>v : Vector α 1<GOAL>(v.head ::ᵥ v.tail).toList = [(v.head ::ᵥ v.tail).head]
<VAR>α β ι : Type u<VAR>c : ι → Cardinal.{v}<GOAL>lift.{w, max v u} (prod c) = prod fun i => lift.{w, v} (c i)
<VAR>α β ι : Type u<VAR>c : ι → Type v<GOAL>lift.{w, max v u} (prod fun i => #(c i)) = prod fun i => lift.{w, v} ((fun i => #(c i)) i)
<VAR>α β ι : Type u<VAR>c : ι → Type v<GOAL>#(ULift.{w, max u v} ((i : ι) → c i)) = #((i : ι) → ULift.{w, v} (c i))
<VAR>α✝ : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝² : Preorder α✝<VAR>inst✝¹ : Preorder β<VAR>s✝ t : Set α✝<VAR>a b : α✝<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>s : Set α<GOAL>¬BddAbove s ↔ ∀ (x : α), ∃ y ∈ s, x < y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s s₁✝ s₂✝ t t₁ t₂ u✝ v : Finset α<VAR>a b : α<VAR>s₁ s₂ u : Finset α<GOAL>s₁ ⊆ s₂ → s₁ ⊆ u → s₁ ⊆ s₂ ∩ u
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>J : Type w<VAR>f : J → ModuleCat R<VAR>s : Fan f<VAR>x y : ↑s.pt<GOAL>(fun x j => (s.π.app { as := j }) x) (x + y) = (fun x j => (s.π.app { as := j }) x) x + (fun x j => (s.π.app { as := j }) x) y
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>J : Type w<VAR>f : J → ModuleCat R<VAR>s : Fan f<VAR>x y : ↑s.pt<GOAL>(fun j => (s.π.app { as := j }) x + (s.π.app { as := j }) y) = (fun j => (s.π.app { as := j }) x) + fun j => (s.π.app { as := j }) y
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>J : Type w<VAR>f : J → ModuleCat R<VAR>s : Fan f<VAR>r : R<VAR>x : ↑s.pt<GOAL>{ toFun := fun x j => (s.π.app { as := j }) x, map_add' := ⋯ }.toFun (r • x) = (RingHom.id R) r • { toFun := fun x j => (s.π.app { as := j }) x, map_add' := ⋯ }.toFun x
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>J : Type w<VAR>f : J → ModuleCat R<VAR>s : Fan f<VAR>r : R<VAR>x : ↑s.pt<GOAL>(fun j => r • (s.π.app { as := j }) x) = (RingHom.id R) r • fun j => (s.π.app { as := j }) x
<VAR>α : Type u_1<VAR>a : α<VAR>inst✝¹ : Lattice α<VAR>inst✝ : BoundedOrder α<VAR>x y : ↑(Iic a)<GOAL>IsCompl x y ↔ Disjoint ↑x ↑y ∧ ↑x ⊔ ↑y = a
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>α : Type u_9<VAR>s : Set (α → Prop)<VAR>a : α<GOAL>sSup s a ↔ ∃ r ∈ s, r a
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>α : Type u_9<VAR>s : Set (α → Prop)<VAR>a : α<GOAL>⨆ f, ↑f a ↔ ∃ r ∈ s, r a
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : Archimedean α<VAR>a : α<VAR>ha : 0 < a<VAR>g : α<GOAL>∃! k, 0 ≤ g - k • a ∧ g - k • a < a
<VAR>J : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝² : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>inst✝ : Category.{v₄, u₄} D<VAR>F : J ⥤ C<VAR>G : C ⥤ D<VAR>A : Cone F<VAR>X✝ Y✝ : J<VAR>f✝ : X✝ ⟶ Y✝<GOAL>((const J).obj (G.obj A.pt)).map f✝ ≫ (fun j => G.map (A.π.app j)) Y✝ = (fun j => G.map (A.π.app j)) X✝ ≫ (F ⋙ G).map f✝
<VAR>J : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝² : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>inst✝ : Category.{v₄, u₄} D<VAR>F : J ⥤ C<VAR>G : C ⥤ D<VAR>A : Cone F<VAR>X✝ Y✝ : J<VAR>f✝ : X✝ ⟶ Y✝<GOAL>((const J).obj (G.obj A.pt)).map f✝ ≫ (fun j => G.map (A.π.app j)) Y✝ = G.map (A.π.app X✝ ≫ F.map f✝)
<VAR>J : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝² : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>inst✝ : Category.{v₄, u₄} D<VAR>F : J ⥤ C<VAR>G : C ⥤ D<VAR>X✝ Y✝ : Cone F<VAR>f : X✝ ⟶ Y✝<VAR>j : J<GOAL>G.map f.hom ≫ ((fun A => { pt := G.obj A.pt, π := { app := fun j => G.map (A.π.app j), naturality := ⋯ } }) Y✝).π.app j = ((fun A => { pt := G.obj A.pt, π := { app := fun j => G.map (A.π.app j), naturality := ⋯ } }) X✝).π.app j
<VAR>B : Type u₁<VAR>inst✝¹ : Bicategory B<VAR>C : Type u₂<VAR>inst✝ : Bicategory C<VAR>F : LaxFunctor B C<VAR>a b : B<VAR>f : a ⟶ b<GOAL>(λ_ (F.map f)).hom = F.mapId a ▷ F.map f ≫ F.mapComp (𝟙 a) f ≫ F.map₂ (λ_ f).hom
<VAR>B : Type u₁<VAR>inst✝¹ : Bicategory B<VAR>C : Type u₂<VAR>inst✝ : Bicategory C<VAR>F : LaxFunctor B C<VAR>a b : B<VAR>f : a ⟶ b<GOAL>(F.map₂Iso (λ_ f)).inv = (λ_ (F.map f)).inv ≫ F.mapId a ▷ F.map f ≫ F.mapComp (𝟙 a) f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>p : PrimeSpectrum R<VAR>f : R<GOAL>Subsingleton (LocalizedModule (Submonoid.powers f) M) ↔ Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>p : PrimeSpectrum R<VAR>f : R<GOAL>(∀ (m : M), ∃ r ∈ Submonoid.powers f, r • m = 0) ↔ Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}
<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>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>i : ℕ<GOAL>iteratedFDerivWithin 𝕜 i (fun x => 0) s x = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>ps : Set P<VAR>n : ℕ<VAR>inst✝ : FiniteDimensional ℝ V<VAR>hd : finrank ℝ V = n<VAR>hc : Cospherical ps<VAR>sx₁ sx₂ : Simplex ℝ P n<VAR>hsx₁ : Set.range sx₁.points ⊆ ps<VAR>hsx₂ : Set.range sx₂.points ⊆ ps<GOAL>sx₁.circumcenter = sx₂.circumcenter
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>ps : Set P<VAR>n : ℕ<VAR>inst✝ : FiniteDimensional ℝ V<VAR>hd : finrank ℝ V = n<VAR>hc : Cospherical ps<VAR>sx₁ sx₂ : Simplex ℝ P n<VAR>hsx₁ : Set.range sx₁.points ⊆ ps<VAR>hsx₂ : Set.range sx₂.points ⊆ ps<VAR>r : P<VAR>hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = r<GOAL>sx₁.circumcenter = sx₂.circumcenter
<VAR>u✝ x✝ : XgcdType<VAR>u : XgcdType := x✝<VAR>h : u.r = 0<GOAL>x✝.reduce.IsReduced
<VAR>u✝ x✝ : XgcdType<VAR>u : XgcdType := x✝<VAR>h : u.r = 0<GOAL>u.finish.IsReduced
<VAR>u✝ x✝ : XgcdType<VAR>u : XgcdType := x✝<VAR>h : ¬u.r = 0<GOAL>x✝.reduce.IsReduced
<VAR>u✝ x✝ : XgcdType<VAR>u : XgcdType := x✝<VAR>h : ¬u.r = 0<VAR>this : sizeOf u.step < sizeOf u<GOAL>x✝.reduce.IsReduced
<VAR>u✝ x✝ : XgcdType<VAR>u : XgcdType := x✝<VAR>h : ¬u.r = 0<VAR>this : sizeOf u.step < sizeOf u<GOAL>u.step.reduce.IsReduced
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>f : R →+* S<VAR>n : ℤ<GOAL>(W.map f).φ n = Polynomial.map (mapRingHom f) (W.φ n)
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>f : R →+* S<VAR>n : ℤ<GOAL>C X * Polynomial.map (mapRingHom f) (W.ψ n) ^ 2 - Polynomial.map (mapRingHom f) (W.ψ (n + 1)) * Polynomial.map (mapRingHom f) (W.ψ (n - 1)) = Polynomial.map (mapRingHom f) (C X * W.ψ n ^ 2 - W.ψ (n + 1) * W.ψ (n - 1))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝¹ : ConditionallyCompleteLattice α<VAR>s t : Set α<VAR>a b : α<VAR>inst✝ : Nonempty ι<VAR>f : ι → α<VAR>hf : BddBelow (range f)<GOAL>Iic (⨅ i, f i) = ⋂ i, Iic (f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝¹ : ConditionallyCompleteLattice α<VAR>s t : Set α<VAR>a b : α<VAR>inst✝ : Nonempty ι<VAR>f : ι → α<VAR>hf : BddBelow (range f)<GOAL>Iic (⨅ i, f i) ⊆ ⋂ i, Iic (f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝¹ : ConditionallyCompleteLattice α<VAR>s t : Set α<VAR>a b : α<VAR>inst✝ : Nonempty ι<VAR>f : ι → α<VAR>hf : BddBelow (range f)<GOAL>⋂ i, Iic (f i) ⊆ Iic (⨅ i, f i)