ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>J : Type v₁<VAR>inst✝² : SmallCategory J<VAR>inst✝¹ : FinCategory J<VAR>K✝ : J ⥤ C<VAR>F : C ⥤ D<VAR>inst✝ : RepresentablyFlat F<VAR>c✝ : Cone K✝<VAR>hc✝ : IsLimit c✝<VAR>s✝ : Cone (K✝ ⋙ F)<VAR>K : J ⥤ C<VAR>c : Cone K<VAR>hc : IsLimit c<VAR>s : Cone (K ⋙ F)<VAR>f₁ f₂ : s.pt ⟶ F.obj c.pt<VAR>h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j<VAR>h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j<VAR>α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow := { app := fun X => eqToHom ⋯, naturality := ⋯ }<VAR>α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow := { app := fun X => eqToHom ⋯, naturality := ⋯ }<VAR>c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) := (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₁)<VAR>c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) := (Cones.postcompose (whiskerRight α₂ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₂)<VAR>c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)<VAR>g₁ : c₀.pt ⟶ c₁.pt := c₀.π.app Bicone.left<VAR>g₂ : c₀.pt ⟶ c₂.pt := c₀.π.app Bicone.right<VAR>this : ∀ (j : J), g₁.right ≫ c.π.app j = g₂.right ≫ c.π.app j<GOAL>f₁ = f₂
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>J : Type v₁<VAR>inst✝² : SmallCategory J<VAR>inst✝¹ : FinCategory J<VAR>K✝ : J ⥤ C<VAR>F : C ⥤ D<VAR>inst✝ : RepresentablyFlat F<VAR>c✝ : Cone K✝<VAR>hc✝ : IsLimit c✝<VAR>s✝ : Cone (K✝ ⋙ F)<VAR>K : J ⥤ C<VAR>c : Cone K<VAR>hc : IsLimit c<VAR>s : Cone (K ⋙ F)<VAR>f₁ f₂ : s.pt ⟶ F.obj c.pt<VAR>h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j<VAR>h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j<VAR>α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow := { app := fun X => eqToHom ⋯, naturality := ⋯ }<VAR>α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow := { app := fun X => eqToHom ⋯, naturality := ⋯ }<VAR>c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) := (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₁)<VAR>c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) := (Cones.postcompose (whiskerRight α₂ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₂)<VAR>c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)<VAR>g₁ : c₀.pt ⟶ c₁.pt := c₀.π.app Bicone.left<VAR>g₂ : c₀.pt ⟶ c₂.pt := c₀.π.app Bicone.right<VAR>this✝ : ∀ (j : J), g₁.right ≫ c.π.app j = g₂.right ≫ c.π.app j<VAR>this : c.extend g₁.right = c.extend g₂.right<GOAL>f₁ = f₂
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>J : Type v₁<VAR>inst✝² : SmallCategory J<VAR>inst✝¹ : FinCategory J<VAR>K✝ : J ⥤ C<VAR>F : C ⥤ D<VAR>inst✝ : RepresentablyFlat F<VAR>c✝ : Cone K✝<VAR>hc✝ : IsLimit c✝<VAR>s✝ : Cone (K✝ ⋙ F)<VAR>K : J ⥤ C<VAR>c : Cone K<VAR>hc : IsLimit c<VAR>s : Cone (K ⋙ F)<VAR>f₁ f₂ : s.pt ⟶ F.obj c.pt<VAR>h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j<VAR>h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j<VAR>α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow := { app := fun X => eqToHom ⋯, naturality := ⋯ }<VAR>α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow := { app := fun X => eqToHom ⋯, naturality := ⋯ }<VAR>c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) := (Cones.postcompose (whiskerRight α₁ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₁)<VAR>c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) := (Cones.postcompose (whiskerRight α₂ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₂)<VAR>c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)<VAR>g₁ : c₀.pt ⟶ c₁.pt := c₀.π.app Bicone.left<VAR>g₂ : c₀.pt ⟶ c₂.pt := c₀.π.app Bicone.right<VAR>this✝¹ : ∀ (j : J), g₁.right ≫ c.π.app j = g₂.right ≫ c.π.app j<VAR>this✝ : c.extend g₁.right = c.extend g₂.right<VAR>this : g₁.right = g₂.right<GOAL>f₁ = f₂
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>ι : Type u_2<VAR>f : ι → Cardinal.{u_2}<VAR>c : Cardinal.{u_2}<VAR>hc : c.IsRegular<VAR>hι : #ι < c<GOAL>#ι < c.ord.cof
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>t : Set Y<VAR>hs : t ⊆ e.target<GOAL>IsOpen (↑e.symm '' t) ↔ IsOpen t
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>t : Set Y<VAR>hs : t ⊆ e.target<VAR>h : IsOpen (↑e.symm '' t)<GOAL>IsOpen t
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>t : Set Y<VAR>hs : t ⊆ e.target<VAR>h : IsOpen (↑e.symm '' t)<VAR>hs' : ↑e.symm '' t ⊆ e.source<GOAL>IsOpen t
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>t : Set Y<VAR>hs : t ⊆ e.target<VAR>h : IsOpen (↑e.symm '' t)<VAR>hs' : ↑e.symm '' t ⊆ e.source<GOAL>IsOpen (↑e.toPartialEquiv '' (↑e.symm '' t))
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : MonoidalPreadditive C<VAR>W X Y Z : C<VAR>f : W ⟶ X<GOAL>f ⊗ 0 = 0
<VAR>X : Type u_1<VAR>inst✝¹ : PseudoMetricSpace X<VAR>inst✝ : IsUltrametricDist X<VAR>x✝ y z : X<VAR>r✝ s : ℝ<VAR>x : X<VAR>r : ℝ<GOAL>IsClosed (ball x r)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ l : List α<VAR>a : α<GOAL>(l ++ [a]).reverse = a :: l.reverse
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ l : List α<VAR>a : α<GOAL>[a].reverse ++ l.reverse = a :: l.reverse
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Semiring β<VAR>x : α<VAR>n : ℕ<VAR>f : α →+* β<GOAL>f (∑ i ∈ range n, x ^ i) = ∑ i ∈ range n, f x ^ i
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝ : RCLike 𝕜<VAR>f : α → ℝ<VAR>x : ℝ<VAR>h : HasSum (fun x => ↑(f x)) ↑x<GOAL>HasSum f x
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝¹ : AddGroup G<VAR>inst✝ : AddTorsor G P<VAR>x y : P<GOAL>(pointReflection x) y -ᵥ y = 2 • (x -ᵥ y)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝² : Fintype n<VAR>inst✝¹ : NonAssocSemiring α<VAR>inst✝ : NonAssocSemiring β<VAR>M : Matrix m n α<VAR>N : Matrix n o α<VAR>i : m<VAR>j : o<VAR>f : α →+* β<GOAL>f ((M * N) i j) = (M.map ⇑f * N.map ⇑f) i j
<VAR>b : ℝ<VAR>hb : 1 < b<GOAL>Summable fun n => |↑n| ^ (-b)
<VAR>b : ℝ<VAR>hb : 1 < b<GOAL>Summable fun n => |↑↑n| ^ (-b)
<VAR>b : ℝ<VAR>hb : 1 < b<GOAL>Summable fun n => |↑(-↑n)| ^ (-b)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p✝ q✝ p q : R[X]<VAR>h₁ : p ∣ q<VAR>h₂ : q.natDegree < p.natDegree<GOAL>q = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p✝ q✝ p q : R[X]<VAR>h₁ : p ∣ q<VAR>h₂ : q.natDegree < p.natDegree<VAR>hc : ¬q = 0<GOAL>False
<VAR>α : Type u_1<VAR>r✝ : α → α → Prop<VAR>inst✝ : IsStrictOrder α r✝<VAR>a : α<VAR>r : α → α → Prop<VAR>h : ¬Acc r a<GOAL>∃ b, ¬Acc r b ∧ r b a
<VAR>α : Type u_1<VAR>r✝ : α → α → Prop<VAR>inst✝ : IsStrictOrder α r✝<VAR>a : α<VAR>r : α → α → Prop<VAR>h : ∀ (b : α), ¬Acc r b → ¬r b a<GOAL>Acc r a
<VAR>α : Type u_1<VAR>r✝ : α → α → Prop<VAR>inst✝ : IsStrictOrder α r✝<VAR>a : α<VAR>r : α → α → Prop<VAR>h : ∀ (b : α), ¬Acc r b → ¬r b a<VAR>b : α<VAR>hr : r b a<GOAL>Acc r b
<VAR>α : Type u_1<VAR>r✝ : α → α → Prop<VAR>inst✝ : IsStrictOrder α r✝<VAR>a : α<VAR>r : α → α → Prop<VAR>h : ∀ (b : α), ¬Acc r b → ¬r b a<VAR>b : α<VAR>hr : r b a<VAR>hb : ¬Acc r b<GOAL>False
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<GOAL>re 1 = 1
<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>γ✝ : Type w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : AddCommGroup γ<VAR>f : α → β<VAR>g : β → γ<VAR>x : FreeAbelianGroup α<GOAL>(lift (g ∘ f)) x = (lift g) ((map f) x)
<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>γ✝ : Type w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : AddCommGroup γ<VAR>f : α → β<VAR>g : β → γ<VAR>x : FreeAbelianGroup α<GOAL>(lift (g ∘ f)) 0 = (lift g) ((map f) 0)
<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>γ✝ : Type w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : AddCommGroup γ<VAR>f : α → β<VAR>g : β → γ<VAR>x : FreeAbelianGroup α<GOAL>∀ (x : α), (lift (g ∘ f)) (of x) = (lift g) ((map f) (of x))
<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>γ✝ : Type w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : AddCommGroup γ<VAR>f : α → β<VAR>g : β → γ<VAR>x : FreeAbelianGroup α<GOAL>∀ (x : α), (lift (g ∘ f)) (of x) = (lift g) ((map f) (of x)) → (lift (g ∘ f)) (-of x) = (lift g) ((map f) (-of x))
<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>γ✝ : Type w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : AddCommGroup γ<VAR>f : α → β<VAR>g : β → γ<VAR>x : FreeAbelianGroup α<GOAL>∀ (x y : FreeAbelianGroup α), (lift (g ∘ f)) x = (lift g) ((map f) x) → (lift (g ∘ f)) y = (lift g) ((map f) y) → (lift (g ∘ f)) (x + y) = (lift g) ((map f) (x + y))
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g✝ : α → β<VAR>inst✝¹ : CommMonoid β<VAR>s : Finset α<VAR>p : α → Prop<VAR>hp : DecidablePred p<VAR>inst✝ : DecidablePred fun x => ¬p x<VAR>f : (x : α) → p x → γ<VAR>g : (x : α) → ¬p x → γ<VAR>h : γ → β<VAR>x : { x // x ∈ filter p s }<GOAL>p ↑x
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g✝ : α → β<VAR>inst✝¹ : CommMonoid β<VAR>s : Finset α<VAR>p : α → Prop<VAR>hp : DecidablePred p<VAR>inst✝ : DecidablePred fun x => ¬p x<VAR>f : (x : α) → p x → γ<VAR>g : (x : α) → ¬p x → γ<VAR>h : γ → β<VAR>x : { x // x ∈ filter (fun x => ¬p x) s }<GOAL>¬p ↑x
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g✝ : α → β<VAR>inst✝¹ : CommMonoid β<VAR>s : Finset α<VAR>p : α → Prop<VAR>hp : DecidablePred p<VAR>inst✝ : DecidablePred fun x => ¬p x<VAR>f : (x : α) → p x → γ<VAR>g : (x : α) → ¬p x → γ<VAR>h : γ → β<VAR>x : { x // x ∈ filter p s }<VAR>_hx : x ∈ (filter p s).attach<GOAL>p ↑x
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g✝ : α → β<VAR>inst✝¹ : CommMonoid β<VAR>s : Finset α<VAR>p : α → Prop<VAR>hp : DecidablePred p<VAR>inst✝ : DecidablePred fun x => ¬p x<VAR>f : (x : α) → p x → γ<VAR>g : (x : α) → ¬p x → γ<VAR>h : γ → β<VAR>x : { x // x ∈ filter (fun x => ¬p x) s }<VAR>_hx : x ∈ (filter (fun x => ¬p x) s).attach<GOAL>¬p ↑x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>s : Set α<VAR>t : (a : α) → a ∈ s → Set β<VAR>hs : s.Countable<VAR>this : Countable ↑s<GOAL>(⋃ a, ⋃ (h : a ∈ s), t a h).Countable ↔ ∀ (a : α) (ha : a ∈ s), (t a ha).Countable
<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>ε : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>f' : E →L[𝕜] F<VAR>hf : ApproximatesLinearOn f f' s c<VAR>f'symm : f'.NonlinearRightInverse<VAR>hs : IsOpen s<VAR>hc : c < f'symm.nnnorm⁻¹<GOAL>IsOpen (f '' s)
<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>ε : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>f' : E →L[𝕜] F<VAR>hf : ApproximatesLinearOn f f' s c<VAR>f'symm : f'.NonlinearRightInverse<VAR>hc : c < f'symm.nnnorm⁻¹<VAR>hs : ∀ x ∈ s, ∃ i, 0 < i ∧ closedBall x i ⊆ s<GOAL>∀ ⦃x : E⦄, x ∈ s → ∃ i, 0 < i ∧ closedBall (f x) i ⊆ f '' s
<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>ε✝ : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>f' : E →L[𝕜] F<VAR>hf : ApproximatesLinearOn f f' s c<VAR>f'symm : f'.NonlinearRightInverse<VAR>hc : c < f'symm.nnnorm⁻¹<VAR>hs : ∀ x ∈ s, ∃ i, 0 < i ∧ closedBall x i ⊆ s<VAR>x : E<VAR>hx : x ∈ s<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>hε : closedBall x ε ⊆ s<GOAL>∃ i, 0 < i ∧ closedBall (f x) i ⊆ f '' s
<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>ε✝ : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>f' : E →L[𝕜] F<VAR>hf : ApproximatesLinearOn f f' s c<VAR>f'symm : f'.NonlinearRightInverse<VAR>hc : c < f'symm.nnnorm⁻¹<VAR>hs : ∀ x ∈ s, ∃ i, 0 < i ∧ closedBall x i ⊆ s<VAR>x : E<VAR>hx : x ∈ s<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>hε : closedBall x ε ⊆ s<GOAL>closedBall (f x) ((↑f'symm.nnnorm⁻¹ - ↑c) * ε) ⊆ f '' s
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝³ : Monoid M<VAR>inst✝² : AddMonoid N<VAR>G : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group G<VAR>inst✝ : AddGroup H<VAR>P : AddSubgroup H<GOAL>P.FG ↔ (toSubgroup P).FG
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>hp : p.Monic<VAR>r : R<GOAL>(p.comp (X - C r)).Monic
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>n : ℕ<VAR>a : F<VAR>h : Splits (RingHom.id F) (X ^ n - 1)<VAR>ha : ¬a = 0<GOAL>IsSolvable (X ^ n - C a).Gal
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>n : ℕ<VAR>a : F<VAR>h : Splits (RingHom.id F) (X ^ n - 1)<VAR>ha : ¬a = 0<VAR>ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0<GOAL>IsSolvable (X ^ n - C a).Gal
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>n : ℕ<VAR>a : F<VAR>h : Splits (RingHom.id F) (X ^ n - 1)<VAR>ha : ¬a = 0<VAR>ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0<VAR>hn : ¬n = 0<GOAL>IsSolvable (X ^ n - C a).Gal
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>n : ℕ<VAR>a : F<VAR>h : Splits (RingHom.id F) (X ^ n - 1)<VAR>ha : ¬a = 0<VAR>ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0<VAR>hn : ¬n = 0<VAR>hn' : 0 < n<GOAL>IsSolvable (X ^ n - C a).Gal
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>n : ℕ<VAR>a : F<VAR>h : Splits (RingHom.id F) (X ^ n - 1)<VAR>ha : ¬a = 0<VAR>ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0<VAR>hn : ¬n = 0<VAR>hn' : 0 < n<VAR>hn'' : X ^ n - C a ≠ 0<GOAL>IsSolvable (X ^ n - C a).Gal
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>n : ℕ<VAR>a : F<VAR>h : Splits (RingHom.id F) (X ^ n - 1)<VAR>ha : ¬a = 0<VAR>ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0<VAR>hn : ¬n = 0<VAR>hn' : 0 < n<VAR>hn'' : X ^ n - C a ≠ 0<VAR>hn''' : X ^ n - 1 ≠ 0<GOAL>IsSolvable (X ^ n - C a).Gal
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>n : ℕ<VAR>a : F<VAR>h : Splits (RingHom.id F) (X ^ n - 1)<VAR>ha : ¬a = 0<VAR>ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0<VAR>hn : ¬n = 0<VAR>hn' : 0 < n<VAR>hn'' : X ^ n - C a ≠ 0<VAR>hn''' : X ^ n - 1 ≠ 0<VAR>mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c<GOAL>IsSolvable (X ^ n - C a).Gal
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>n : ℕ<VAR>a : F<VAR>h : Splits (RingHom.id F) (X ^ n - 1)<VAR>ha : ¬a = 0<VAR>ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0<VAR>hn : ¬n = 0<VAR>hn' : 0 < n<VAR>hn'' : X ^ n - C a ≠ 0<VAR>hn''' : X ^ n - 1 ≠ 0<VAR>mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c<GOAL>∀ (a_1 b : (X ^ n - C a).Gal), a_1 * b = b * a_1
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>n : ℕ<VAR>a : F<VAR>h : Splits (RingHom.id F) (X ^ n - 1)<VAR>ha : ¬a = 0<VAR>ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0<VAR>hn : ¬n = 0<VAR>hn' : 0 < n<VAR>hn'' : X ^ n - C a ≠ 0<VAR>hn''' : X ^ n - 1 ≠ 0<VAR>mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c<VAR>σ τ : (X ^ n - C a).Gal<VAR>b : (X ^ n - C a).SplittingField<VAR>hb : b ∈ (X ^ n - C a).rootSet (X ^ n - C a).SplittingField<GOAL>(σ * τ) b = (τ * σ) b
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>n : ℕ<VAR>a : F<VAR>h : Splits (RingHom.id F) (X ^ n - 1)<VAR>ha : ¬a = 0<VAR>ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0<VAR>hn : ¬n = 0<VAR>hn' : 0 < n<VAR>hn'' : X ^ n - C a ≠ 0<VAR>hn''' : X ^ n - 1 ≠ 0<VAR>mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c<VAR>σ τ : (X ^ n - C a).Gal<VAR>b : (X ^ n - C a).SplittingField<VAR>hb : b ^ n = (algebraMap F (X ^ n - C a).SplittingField) a<GOAL>(σ * τ) b = (τ * σ) b
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>n : ℕ<VAR>a : F<VAR>h : Splits (RingHom.id F) (X ^ n - 1)<VAR>ha : ¬a = 0<VAR>ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0<VAR>hn : ¬n = 0<VAR>hn' : 0 < n<VAR>hn'' : X ^ n - C a ≠ 0<VAR>hn''' : X ^ n - 1 ≠ 0<VAR>mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c<VAR>σ τ : (X ^ n - C a).Gal<VAR>b : (X ^ n - C a).SplittingField<VAR>hb : b ^ n = (algebraMap F (X ^ n - C a).SplittingField) a<VAR>hb' : b ≠ 0<GOAL>(σ * τ) b = (τ * σ) b
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>n : ℕ<VAR>a : F<VAR>h : Splits (RingHom.id F) (X ^ n - 1)<VAR>ha : ¬a = 0<VAR>ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0<VAR>hn : ¬n = 0<VAR>hn' : 0 < n<VAR>hn'' : X ^ n - C a ≠ 0<VAR>hn''' : X ^ n - 1 ≠ 0<VAR>mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c<VAR>σ τ : (X ^ n - C a).Gal<VAR>b : (X ^ n - C a).SplittingField<VAR>hb : b ^ n = (algebraMap F (X ^ n - C a).SplittingField) a<VAR>hb' : b ≠ 0<VAR>key : ∀ (σ : (X ^ n - C a).Gal), ∃ c, σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c<GOAL>(σ * τ) b = (τ * σ) b
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>n : ℕ<VAR>a : F<VAR>h : Splits (RingHom.id F) (X ^ n - 1)<VAR>ha : ¬a = 0<VAR>ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0<VAR>hn : ¬n = 0<VAR>hn' : 0 < n<VAR>hn'' : X ^ n - C a ≠ 0<VAR>hn''' : X ^ n - 1 ≠ 0<VAR>mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c<VAR>σ τ : (X ^ n - C a).Gal<VAR>b : (X ^ n - C a).SplittingField<VAR>hb : b ^ n = (algebraMap F (X ^ n - C a).SplittingField) a<VAR>hb' : b ≠ 0<VAR>key : ∀ (σ : (X ^ n - C a).Gal), ∃ c, σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c<VAR>c : F<VAR>hc : σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c<VAR>d : F<VAR>hd : τ b = b * (algebraMap F (X ^ n - C a).SplittingField) d<GOAL>(σ * τ) b = (τ * σ) b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>m n : ℕ<VAR>s✝ : Finset α<VAR>inst✝ : DecidableEq α<VAR>h : G.CliqueFree n<VAR>s t : α<GOAL>(G.replaceVertex s t).CliqueFree n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>m n : ℕ<VAR>s✝ : Finset α<VAR>inst✝ : DecidableEq α<VAR>s t : α<VAR>h : ¬(G.replaceVertex s t).CliqueFree n<GOAL>¬G.CliqueFree n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>m n : ℕ<VAR>s✝ : Finset α<VAR>inst✝ : DecidableEq α<VAR>s t : α<VAR>h : ¬(G.replaceVertex s t).CliqueFree n<VAR>φ : Fin n ↪ α<VAR>hφ : ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ ⊤.Adj a b<GOAL>¬G.CliqueFree n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>m n : ℕ<VAR>s✝ : Finset α<VAR>inst✝ : DecidableEq α<VAR>s t : α<VAR>h : ¬(G.replaceVertex s t).CliqueFree n<VAR>φ : Fin n ↪ α<VAR>hφ : ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ ⊤.Adj a b<GOAL>Nonempty (⊤ ↪g G)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>p : α<VAR>h0 : p ≠ 0<VAR>hu : ¬IsUnit p<VAR>n : ℕ<GOAL>multiplicity p (p ^ n) = ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>p : α<VAR>h0 : p ≠ 0<VAR>hu : ¬IsUnit p<VAR>n : ℕ<GOAL>p ^ n ∣ p ^ n ∧ ¬p ^ (n + 1) ∣ p ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>p : α<VAR>h0 : p ≠ 0<VAR>hu : ¬IsUnit p<VAR>n : ℕ<GOAL>¬p ^ (n + 1) ∣ p ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>p : α<VAR>h0 : p ≠ 0<VAR>hu : ¬IsUnit p<VAR>n : ℕ<GOAL>¬n + 1 ≤ n
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>hv : v ≠ 0<VAR>f : ℝ → ℝ<VAR>hf : MeasurableEmbedding f<VAR>f' : ℝ → ℝ<VAR>h_deriv : ∀ (x : ℝ), HasDerivAt f (f' x) x<VAR>s : Set ℝ<VAR>hs : MeasurableSet s<GOAL>(Measure.comap f (gaussianReal μ v)) s = ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * gaussianPDFReal μ v (f x))
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>hv : v ≠ 0<VAR>f : ℝ → ℝ<VAR>hf : MeasurableEmbedding f<VAR>f' : ℝ → ℝ<VAR>h_deriv : ∀ (x : ℝ), HasDerivAt f (f' x) x<VAR>s : Set ℝ<VAR>hs : MeasurableSet s<GOAL>(Measure.comap f (ℙ.withDensity fun x => ENNReal.ofReal (gaussianPDFReal μ v x))) s = ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * gaussianPDFReal μ v (f x))
<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>S : Type v<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>p : R[X]<GOAL>(mapAlg R S) p = map (algebraMap R S) p
<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>S : Type v<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>p : R[X]<GOAL>(p.sum fun e a => C ((algebraMap R S) a) * X ^ e) = p.sum fun e a => (⇑C ∘ ⇑(algebraMap R S)) a * X ^ e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : Zero M<VAR>f : α →₀ M<VAR>a : α<VAR>b : M<GOAL>erase a (f.update a b) = erase a f