ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E'<VAR>inst✝³ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝² : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝¹ : TopologicalSpace M'<VAR>inst✝ : ChartedSpace H' M'<VAR>f : M → M'<VAR>x : M<GOAL>ContinuousAt f x ∧ DifferentiableWithinAtProp I I' (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) univ (↑(chartAt H x) x) ↔ ContinuousAt f x ∧ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) (range ↑I) (↑(extChartAt I x) x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E'<VAR>inst✝³ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝² : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝¹ : TopologicalSpace M'<VAR>inst✝ : ChartedSpace H' M'<VAR>f : M → M'<VAR>x : M<GOAL>DifferentiableWithinAtProp I I' (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) univ (↑(chartAt H x) x) ↔ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) (range ↑I) (↑(extChartAt I x) x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E'<VAR>inst✝³ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝² : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝¹ : TopologicalSpace M'<VAR>inst✝ : ChartedSpace H' M'<VAR>f : M → M'<VAR>x : M<GOAL>DifferentiableWithinAt 𝕜 (↑I' ∘ (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) ∘ ↑I.symm) (range ↑I) (↑I (↑(chartAt H x) x)) ↔ DifferentiableWithinAt 𝕜 ((↑I' ∘ ↑(chartAt H' (f x))) ∘ f ∘ ↑(chartAt H x).symm ∘ ↑I.symm) (range ↑I) (↑I (↑(chartAt H x) x))
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>c : ℂ<VAR>R θ : ℝ<GOAL>circleMap c R θ ∉ ball c R
<VAR>F : Type v'<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : StarRing R<VAR>inst✝¹⁴ : NonUnitalSemiring A<VAR>inst✝¹³ : StarRing A<VAR>inst✝¹² : Module R A<VAR>inst✝¹¹ : IsScalarTower R A A<VAR>inst✝¹⁰ : SMulCommClass R A A<VAR>inst✝⁹ : StarModule R A<VAR>inst✝⁸ : NonUnitalSemiring B<VAR>inst✝⁷ : StarRing B<VAR>inst✝⁶ : Module R B<VAR>inst✝⁵ : IsScalarTower R B B<VAR>inst✝⁴ : SMulCommClass R B B<VAR>inst✝³ : StarModule R B<VAR>inst✝² : FunLike F A B<VAR>inst✝¹ : NonUnitalAlgHomClass F R A B<VAR>inst✝ : NonUnitalStarAlgHomClass F R A B<VAR>S T : NonUnitalStarSubalgebra R A<GOAL>∀ {x : A}, x ∈ S → x ∈ S ⊔ T
<VAR>F : Type v'<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : StarRing R<VAR>inst✝¹⁴ : NonUnitalSemiring A<VAR>inst✝¹³ : StarRing A<VAR>inst✝¹² : Module R A<VAR>inst✝¹¹ : IsScalarTower R A A<VAR>inst✝¹⁰ : SMulCommClass R A A<VAR>inst✝⁹ : StarModule R A<VAR>inst✝⁸ : NonUnitalSemiring B<VAR>inst✝⁷ : StarRing B<VAR>inst✝⁶ : Module R B<VAR>inst✝⁵ : IsScalarTower R B B<VAR>inst✝⁴ : SMulCommClass R B B<VAR>inst✝³ : StarModule R B<VAR>inst✝² : FunLike F A B<VAR>inst✝¹ : NonUnitalAlgHomClass F R A B<VAR>inst✝ : NonUnitalStarAlgHomClass F R A B<VAR>S T : NonUnitalStarSubalgebra R A<GOAL>S ≤ S ⊔ T
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>l : Filter X<VAR>hs : IsCompact s<GOAL>Disjoint (𝓝ˢ s) l ↔ ∀ x ∈ s, Disjoint (𝓝 x) l
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>l : Filter X<VAR>hs : IsCompact s<VAR>H : ∀ x ∈ s, Disjoint (𝓝 x) l<GOAL>Disjoint (𝓝ˢ s) l
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>l : Filter X<VAR>hs : IsCompact s<VAR>H : ∀ x ∈ s, Disjoint (𝓝 x) l<VAR>U : X → Set X<VAR>hxU : ∀ x ∈ s, x ∈ U x ∧ IsOpen (U x)<VAR>hUl : ∀ x ∈ s, (U x)ᶜ ∈ l<GOAL>Disjoint (𝓝ˢ s) l
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>l : Filter X<VAR>hs : IsCompact s<VAR>H : ∀ x ∈ s, Disjoint (𝓝 x) l<VAR>U : X → Set X<VAR>hUl : ∀ x ∈ s, (U x)ᶜ ∈ l<VAR>hxU : ∀ x ∈ s, x ∈ U x<VAR>hUo : ∀ x ∈ s, IsOpen (U x)<GOAL>Disjoint (𝓝ˢ s) l
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>l : Filter X<VAR>hs : IsCompact s<VAR>H : ∀ x ∈ s, Disjoint (𝓝 x) l<VAR>U : X → Set X<VAR>hUl : ∀ x ∈ s, (U x)ᶜ ∈ l<VAR>hxU : ∀ x ∈ s, x ∈ U x<VAR>hUo : ∀ x ∈ s, IsOpen (U x)<VAR>t : Finset X<VAR>hts : ∀ x ∈ t, x ∈ s<VAR>hst : s ⊆ ⋃ x ∈ t, U x<GOAL>Disjoint (𝓝ˢ s) l
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>l : Filter X<VAR>hs : IsCompact s<VAR>H : ∀ x ∈ s, Disjoint (𝓝 x) l<VAR>U : X → Set X<VAR>hUl : ∀ x ∈ s, (U x)ᶜ ∈ l<VAR>hxU : ∀ x ∈ s, x ∈ U x<VAR>hUo : ∀ x ∈ s, IsOpen (U x)<VAR>t : Finset X<VAR>hts : ∀ x ∈ t, x ∈ s<VAR>hst : s ⊆ ⋃ x ∈ t, U x<GOAL>(⋃ x ∈ t, U x)ᶜ ∈ l
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>l : Filter X<VAR>hs : IsCompact s<VAR>H : ∀ x ∈ s, Disjoint (𝓝 x) l<VAR>U : X → Set X<VAR>hUl : ∀ x ∈ s, (U x)ᶜ ∈ l<VAR>hxU : ∀ x ∈ s, x ∈ U x<VAR>hUo : ∀ x ∈ s, IsOpen (U x)<VAR>t : Finset X<VAR>hts : ∀ x ∈ t, x ∈ s<VAR>hst : s ⊆ ⋃ x ∈ t, U x<GOAL>∀ i ∈ t, (U i)ᶜ ∈ l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>l m : Language α<VAR>a b x : List α<GOAL>a.reverse ∈ l.reverse ↔ a ∈ l
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>Q : Fin 3 → R<VAR>u : Rˣ<GOAL>(fun m => m • Q) u y * Q z ^ 3 = Q y * (fun m => m • Q) u z ^ 3
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>Q : Fin 3 → R<VAR>u : Rˣ<GOAL>↑u ^ 3 * Q y * Q z ^ 3 = Q y * (↑u * Q z) ^ 3
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>motive : List α → Sort u_2<VAR>nil : motive []<VAR>singleton : (a : α) → motive [a]<VAR>cons_append : (a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b]))<VAR>a : α<VAR>l : List α<VAR>b : α<GOAL>(match a :: (l ++ [b]) with | [] => nil | [a] => singleton a | a :: b :: l => let l' := (b :: l).dropLast; let b' := (b :: l).getLast ⋯; cast ⋯ (cons_append a l' b' (bidirectionalRec nil singleton cons_append l'))) = cons_append a l b (bidirectionalRec nil singleton cons_append l)
<VAR>n : ℕ<GOAL>Gamma (↑n + 1) = ↑n !
<VAR>R : Type u_1<VAR>inst✝⁵ : CommSemiring 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>m : M<VAR>p : ι →₀ N<VAR>i : ι<GOAL>((finsuppRight R M N ι) (m ⊗ₜ[R] p)) i = m ⊗ₜ[R] p i
<VAR>E : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>hs : s ∈ 𝓝 x<VAR>g : E ≃ₜ E := Homeomorph.addLeft x<VAR>t : Set E := ⇑g ⁻¹' s<GOAL>#↑s = #E
<VAR>E : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>hs : s ∈ 𝓝 x<VAR>g : E ≃ₜ E := Homeomorph.addLeft x<VAR>t : Set E := ⇑g ⁻¹' s<VAR>this : t ∈ 𝓝 0<GOAL>#↑s = #E
<VAR>E : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>hs : s ∈ 𝓝 x<VAR>g : E ≃ₜ E := Homeomorph.addLeft x<VAR>t : Set E := ⇑g ⁻¹' s<VAR>this : t ∈ 𝓝 0<VAR>A : #↑t = #E<GOAL>#↑s = #E
<VAR>E : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>hs : s ∈ 𝓝 x<VAR>g : E ≃ₜ E := Homeomorph.addLeft x<VAR>t : Set E := ⇑g ⁻¹' s<VAR>this : t ∈ 𝓝 0<VAR>A : #↑t = #E<VAR>B : #↑t = #↑s<GOAL>#↑s = #E
<VAR>G : Type u<VAR>inst✝¹ : Group G<VAR>X : Action FintypeCat (MonCat.of G)<VAR>inst✝ : IsConnected X<VAR>x y : ↑X.V<VAR>T : Set ↑X.V := MulAction.orbit G x<VAR>this✝ : Fintype ↑T<VAR>this : MulAction G ↑(FintypeCat.of ↑T) := inferInstanceAs (MulAction G ↑(MulAction.orbit G x))<VAR>T' : Action FintypeCat (MonCat.of G) := Action.FintypeCat.ofMulAction G (FintypeCat.of ↑T)<VAR>i : T' ⟶ X := { hom := Subtype.val, comm := ⋯ }<GOAL>∃ g, g • x = y
<VAR>G : Type u<VAR>inst✝¹ : Group G<VAR>X : Action FintypeCat (MonCat.of G)<VAR>inst✝ : IsConnected X<VAR>x y : ↑X.V<VAR>T : Set ↑X.V := MulAction.orbit G x<VAR>this✝¹ : Fintype ↑T<VAR>this✝ : MulAction G ↑(FintypeCat.of ↑T) := inferInstanceAs (MulAction G ↑(MulAction.orbit G x))<VAR>T' : Action FintypeCat (MonCat.of G) := Action.FintypeCat.ofMulAction G (FintypeCat.of ↑T)<VAR>i : T' ⟶ X := { hom := Subtype.val, comm := ⋯ }<VAR>this : Mono i<GOAL>∃ g, g • x = y
<VAR>G : Type u<VAR>inst✝¹ : Group G<VAR>X : Action FintypeCat (MonCat.of G)<VAR>inst✝ : IsConnected X<VAR>x y : ↑X.V<VAR>T : Set ↑X.V := MulAction.orbit G x<VAR>this✝² : Fintype ↑T<VAR>this✝¹ : MulAction G ↑(FintypeCat.of ↑T) := inferInstanceAs (MulAction G ↑(MulAction.orbit G x))<VAR>T' : Action FintypeCat (MonCat.of G) := Action.FintypeCat.ofMulAction G (FintypeCat.of ↑T)<VAR>i : T' ⟶ X := { hom := Subtype.val, comm := ⋯ }<VAR>this✝ : Mono i<VAR>this : IsIso i<GOAL>∃ g, g • x = y
<VAR>G : Type u<VAR>inst✝¹ : Group G<VAR>X : Action FintypeCat (MonCat.of G)<VAR>inst✝ : IsConnected X<VAR>x y : ↑X.V<VAR>T : Set ↑X.V := MulAction.orbit G x<VAR>this✝² : Fintype ↑T<VAR>this✝¹ : MulAction G ↑(FintypeCat.of ↑T) := inferInstanceAs (MulAction G ↑(MulAction.orbit G x))<VAR>T' : Action FintypeCat (MonCat.of G) := Action.FintypeCat.ofMulAction G (FintypeCat.of ↑T)<VAR>i : T' ⟶ X := { hom := Subtype.val, comm := ⋯ }<VAR>this✝ : Mono i<VAR>this : IsIso i<VAR>hb : Function.Bijective i.hom<GOAL>∃ g, g • x = y
<VAR>G : Type u<VAR>inst✝¹ : Group G<VAR>X : Action FintypeCat (MonCat.of G)<VAR>inst✝ : IsConnected X<VAR>x y : ↑X.V<VAR>T : Set ↑X.V := MulAction.orbit G x<VAR>this✝² : Fintype ↑T<VAR>this✝¹ : MulAction G ↑(FintypeCat.of ↑T) := inferInstanceAs (MulAction G ↑(MulAction.orbit G x))<VAR>T' : Action FintypeCat (MonCat.of G) := Action.FintypeCat.ofMulAction G (FintypeCat.of ↑T)<VAR>i : T' ⟶ X := { hom := Subtype.val, comm := ⋯ }<VAR>this✝ : Mono i<VAR>this : IsIso i<VAR>hb : Function.Bijective i.hom<VAR>y' : ↑X.V<VAR>g : G<VAR>hg : g • x = y'<VAR>hy' : y' = y<GOAL>∃ g, g • x = y
<VAR>G : Type u<VAR>inst✝¹ : Group G<VAR>X : Action FintypeCat (MonCat.of G)<VAR>inst✝ : IsConnected X<VAR>x y : ↑X.V<VAR>T : Set ↑X.V := MulAction.orbit G x<VAR>this✝² : Fintype ↑T<VAR>this✝¹ : MulAction G ↑(FintypeCat.of ↑T) := inferInstanceAs (MulAction G ↑(MulAction.orbit G x))<VAR>T' : Action FintypeCat (MonCat.of G) := Action.FintypeCat.ofMulAction G (FintypeCat.of ↑T)<VAR>i : T' ⟶ X := { hom := Subtype.val, comm := ⋯ }<VAR>this✝ : Mono i<VAR>this : IsIso i<VAR>hb : Function.Bijective i.hom<VAR>y' : ↑X.V<VAR>g : G<VAR>hg : g • x = y'<VAR>hy' : y' = y<GOAL>g • x = y
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>g h : G<VAR>comm : Commute g h<GOAL>(fixedBy α g)ᶜ ∈ fixedBy (Set α) h
<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>iso : E ≃L[𝕜] F<VAR>f : F → G<VAR>x : E<GOAL>fderiv 𝕜 (f ∘ ⇑iso) x = (fderiv 𝕜 f (iso x)).comp ↑iso
<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>iso : E ≃L[𝕜] F<VAR>f : F → G<VAR>x : E<GOAL>UniqueDiffWithinAt 𝕜 (⇑iso ⁻¹' univ) x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<GOAL>M.E ⊆ M.closure X ↔ M.closure X = M.E
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : AddMonoid A<VAR>h : ShiftMkCore C A<VAR>n : A<VAR>X : C<GOAL>(MonoidalCategory.leftUnitor (__src✝.obj { as := n })).hom.app X = (MonoidalCategory.whiskerRight h.zero.inv (__src✝.obj { as := n }) ≫ (fun m n => (h.add m.as n.as).inv) (𝟙_ (Discrete A)) { as := n } ≫ __src✝.map (MonoidalCategory.leftUnitor { as := n }).hom).app X
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : AddMonoid A<VAR>h : ShiftMkCore C A<VAR>n : A<VAR>X : C<GOAL>(MonoidalCategory.rightUnitor (__src✝.obj { as := n })).hom.app X = (MonoidalCategory.whiskerLeft (__src✝.obj { as := n }) h.zero.inv ≫ (fun m n => (h.add m.as n.as).inv) { as := n } (𝟙_ (Discrete A)) ≫ __src✝.map (MonoidalCategory.rightUnitor { as := n }).hom).app X
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>b : HilbertBasis ι 𝕜 E<GOAL>Orthonormal 𝕜 fun i => b.repr.symm (lp.single 2 i 1)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>b : HilbertBasis ι 𝕜 E<GOAL>∀ (i j : ι), ⟪b.repr.symm (lp.single 2 i 1), b.repr.symm (lp.single 2 j 1)⟫_𝕜 = if i = j then 1 else 0
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>b : HilbertBasis ι 𝕜 E<VAR>i j : ι<GOAL>⟪b.repr.symm (lp.single 2 i 1), b.repr.symm (lp.single 2 j 1)⟫_𝕜 = if i = j then 1 else 0
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>b : HilbertBasis ι 𝕜 E<VAR>i j : ι<GOAL>⟪1, if h : i = j then ⋯ ▸ 1 else 0⟫_𝕜 = if i = j then 1 else 0
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<GOAL>(fun t => inverse (1 - t)) =O[𝓝 0] fun _t => 1
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<GOAL>∃ c, ∃ ε > 0, ∀ ⦃y : R⦄, dist y 0 < ε → ‖inverse (1 - y)‖ ≤ c * ‖1‖
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>t : R<VAR>ht : dist t 0 < 2⁻¹<GOAL>‖inverse (1 - t)‖ ≤ (‖1‖ + 1) * ‖1‖
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>t : R<VAR>ht : ‖t‖ < 2⁻¹<GOAL>‖inverse (1 - t)‖ ≤ (‖1‖ + 1) * ‖1‖
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>t : R<VAR>ht : ‖t‖ < 2⁻¹<VAR>ht' : ‖t‖ < 1<GOAL>‖inverse (1 - t)‖ ≤ (‖1‖ + 1) * ‖1‖
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>t : R<VAR>ht : ‖t‖ < 2⁻¹<VAR>ht' : ‖t‖ < 1<GOAL>‖↑(Units.oneSub t ht')⁻¹‖ ≤ ‖1‖ + 1
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>t : R<VAR>ht : ‖t‖ < 2⁻¹<VAR>ht' : ‖t‖ < 1<GOAL>‖∑' (n : ℕ), t ^ n‖ ≤ ‖1‖ + 1
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>t : R<VAR>ht : ‖t‖ < 2⁻¹<VAR>ht' : ‖t‖ < 1<VAR>this : ‖∑' (n : ℕ), t ^ n‖ ≤ ‖1‖ - 1 + (1 - ‖t‖)⁻¹<GOAL>‖∑' (n : ℕ), t ^ n‖ ≤ ‖1‖ + 1
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>t : R<VAR>ht : ‖t‖ < 2⁻¹<VAR>ht' : ‖t‖ < 1<VAR>this✝ : ‖∑' (n : ℕ), t ^ n‖ ≤ ‖1‖ - 1 + (1 - ‖t‖)⁻¹<VAR>this : (1 - ‖t‖)⁻¹ ≤ 2<GOAL>‖∑' (n : ℕ), t ^ n‖ ≤ ‖1‖ + 1
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n m : ℕ<VAR>inst✝ : DivisionRing K<VAR>n_le_m : n ≤ m<VAR>terminatedAt_n : g.TerminatedAt n<GOAL>g.conts m = g.conts n
<VAR>S : Type u_1<VAR>inst✝⁶ : AddMonoidWithOne S<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasShift C S<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>inst✝ : HasShift D S<VAR>F : C ⥤ D<VAR>η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1<VAR>hF : ∀ (c c' : C), F.map 0 = 0<VAR>X : DifferentialObject S C<GOAL>(F.map X.d ≫ η.app X.obj) ≫ (shiftFunctor D 1).map (F.map X.d ≫ η.app X.obj) = 0
<VAR>S : Type u_1<VAR>inst✝⁶ : AddMonoidWithOne S<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasShift C S<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>inst✝ : HasShift D S<VAR>F : C ⥤ D<VAR>η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1<VAR>hF : ∀ (c c' : C), F.map 0 = 0<VAR>X : DifferentialObject S C<GOAL>(F.map X.d ≫ η.app X.obj) ≫ (F ⋙ shiftFunctor D 1).map X.d ≫ (shiftFunctor D 1).map (η.app X.obj) = 0
<VAR>S : Type u_1<VAR>inst✝⁶ : AddMonoidWithOne S<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasShift C S<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>inst✝ : HasShift D S<VAR>F : C ⥤ D<VAR>η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1<VAR>hF : ∀ (c c' : C), F.map 0 = 0<VAR>X : DifferentialObject S C<GOAL>F.map X.d ≫ ((shiftFunctor C 1 ⋙ F).map X.d ≫ η.app ((shiftFunctor C 1).obj X.obj)) ≫ (shiftFunctor D 1).map (η.app X.obj) = 0
<VAR>S : Type u_1<VAR>inst✝⁶ : AddMonoidWithOne S<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasShift C S<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>inst✝ : HasShift D S<VAR>F : C ⥤ D<VAR>η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1<VAR>hF : ∀ (c c' : C), F.map 0 = 0<VAR>X : DifferentialObject S C<GOAL>F.map X.d ≫ (F.map ((shiftFunctor C 1).map X.d) ≫ η.app ((shiftFunctor C 1).obj X.obj)) ≫ (shiftFunctor D 1).map (η.app X.obj) = 0
<VAR>S : Type u_1<VAR>inst✝⁶ : AddMonoidWithOne S<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasShift C S<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>inst✝ : HasShift D S<VAR>F : C ⥤ D<VAR>η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1<VAR>hF : ∀ (c c' : C), F.map 0 = 0<VAR>X : DifferentialObject S C<GOAL>(0 ≫ η.app ((shiftFunctor C 1).obj X.obj)) ≫ (shiftFunctor D 1).map (η.app X.obj) = 0
<VAR>S : Type u_1<VAR>inst✝⁶ : AddMonoidWithOne S<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasShift C S<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>inst✝ : HasShift D S<VAR>F : C ⥤ D<VAR>η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1<VAR>hF : ∀ (c c' : C), F.map 0 = 0<VAR>X✝ Y✝ : DifferentialObject S C<VAR>f : X✝ ⟶ Y✝<GOAL>(F.map X✝.d ≫ η.app X✝.obj) ≫ (shiftFunctor D 1).map (F.map f.f) = F.map f.f ≫ F.map Y✝.d ≫ η.app Y✝.obj
<VAR>S : Type u_1<VAR>inst✝⁶ : AddMonoidWithOne S<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasShift C S<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>inst✝ : HasShift D S<VAR>F : C ⥤ D<VAR>η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1<VAR>hF : ∀ (c c' : C), F.map 0 = 0<VAR>X✝ Y✝ : DifferentialObject S C<VAR>f : X✝ ⟶ Y✝<GOAL>F.map X✝.d ≫ (shiftFunctor C 1 ⋙ F).map f.f ≫ η.app Y✝.obj = F.map f.f ≫ F.map Y✝.d ≫ η.app Y✝.obj
<VAR>S : Type u_1<VAR>inst✝⁶ : AddMonoidWithOne S<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasShift C S<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>inst✝ : HasShift D S<VAR>F : C ⥤ D<VAR>η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1<VAR>hF : ∀ (c c' : C), F.map 0 = 0<VAR>X✝ Y✝ : DifferentialObject S C<VAR>f : X✝ ⟶ Y✝<GOAL>(F.map f.f ≫ F.map Y✝.d) ≫ η.app Y✝.obj = F.map f.f ≫ F.map Y✝.d ≫ η.app Y✝.obj
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>f : NormedAddGroupHom M N<VAR>hquot : f.IsQuotient<VAR>m : M<GOAL>‖f m‖ ≤ ‖m‖
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>f : NormedAddGroupHom M N<VAR>hquot : f.IsQuotient<VAR>m : M<GOAL>sInf ((fun m_1 => ‖m + m_1‖) '' ↑f.ker) ≤ ‖m‖
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>f : NormedAddGroupHom M N<VAR>hquot : f.IsQuotient<VAR>m : M<GOAL>BddBelow ((fun m_1 => ‖m + m_1‖) '' ↑f.ker)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>f : NormedAddGroupHom M N<VAR>hquot : f.IsQuotient<VAR>m : M<GOAL>‖m‖ ∈ (fun m_1 => ‖m + m_1‖) '' ↑f.ker
<VAR>α : Type u_1<VAR>n : Nat<VAR>a : α<VAR>l : List α<GOAL>(leftpad n a l).length = max n l.length
<VAR>α : Type u<VAR>β : α → Type v<VAR>l✝ l₁ l₂ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l : List (Sigma β)<VAR>h : l.NodupKeys<GOAL>lookupAll a l = (dlookup a l).toList
<VAR>α : Type u<VAR>β : α → Type v<VAR>l✝ l₁ l₂ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l : List (Sigma β)<VAR>h : l.NodupKeys<GOAL>lookupAll a l = (lookupAll a l).head?.toList
<VAR>α : Type u<VAR>β : α → Type v<VAR>l✝ l₁ l₂ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l : List (Sigma β)<VAR>h : l.NodupKeys<VAR>h1 : (lookupAll a l).length ≤ 1<GOAL>lookupAll a l = (lookupAll a l).head?.toList
<VAR>ι : Type u_1<VAR>π✝ : ι → Sort u_2<VAR>s : Finset ι<VAR>f✝ g✝ : (i : ι) → π✝ i<VAR>inst✝ : (j : ι) → Decidable (j ∈ s)<VAR>π : ι → Type u_3<VAR>t : Set ι<VAR>t' : (i : ι) → Set (π i)<VAR>f g f' g' h : (i : ι) → π i<VAR>hf : f ∈ t.pi t'<VAR>hg : g ∈ t.pi t'<GOAL>s.piecewise f g ∈ t.pi t'
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>P : (α : Type u_4) → [inst : Fintype α] → Prop<VAR>α : Type u_4<VAR>inst✝ : Fintype α<VAR>hbase : ∀ (α : Type u_4) [inst : Fintype α] [inst_1 : Subsingleton α], P α<VAR>hstep : ∀ (α : Type u_4) [inst : Fintype α] [inst_1 : Nontrivial α], (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α<VAR>n : ℕ<VAR>hn : card α = n<GOAL>P α