ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>S : Type u_3<VAR>M : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Field S<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>B : BilinForm S M<VAR>N₁ N₂ : Submodule R M<GOAL>(∀ x ∈ N₁, ∀ y ∈ N₂, ∃ y_1, (algebraMap R S) y_1 = (B y) x) ↔ ∀ x ∈ N₂, ∀ y ∈ N₁, ∃ y_1, (algebraMap R S) y_1 = (B x) y
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>G : C<VAR>hG : IsDetector G<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hf : ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h<VAR>H : C<VAR>hH : H ∈ {G}<VAR>h : H ⟶ Y<GOAL>∃! h', h' ≫ f = h
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>H : C<VAR>h : H ⟶ Y<VAR>hG : IsDetector H<VAR>hf : ∀ (h : H ⟶ Y), ∃! h', h' ≫ f = h<VAR>hH : H ∈ {H}<GOAL>∃! h', h' ≫ f = h
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommSemiring R<VAR>p : R[X]<GOAL>derivative (p ^ 2) = C 2 * p * derivative p
<VAR>S : Profinite<GOAL>ClosedEmbedding (ι S)
<VAR>S : Profinite<GOAL>Continuous (ι S)
<VAR>S : Profinite<GOAL>Function.Injective (ι S)
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>G✝ H✝ : ModuleCat R<VAR>f✝ : G✝ ⟶ H✝<VAR>G H : ModuleCat R<VAR>f : G ⟶ H<GOAL>(imageIsoRange f).hom ≫ ofHom (LinearMap.range f).subtype = Limits.image.ι f
<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 : Y ⟶ Z<GOAL>0 ⊗ f = 0
<VAR>xl xr : Type u<VAR>x : PGame<GOAL>0 ⧏ -x ↔ x ⧏ 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasPullbacks C<VAR>P : MorphismProperty C<VAR>hP : P.StableUnderBaseChange<VAR>S S' : C<VAR>f : S' ⟶ S<VAR>X Y : Over S<VAR>g : X ⟶ Y<VAR>H : P g.left<GOAL>P ((Over.pullback f).map g).left
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasPullbacks C<VAR>P : MorphismProperty C<VAR>hP : P.StableUnderBaseChange<VAR>S S' : C<VAR>f : S' ⟶ S<VAR>X Y : Over S<VAR>g : X ⟶ Y<VAR>H : P g.left<VAR>this : P.RespectsIso<GOAL>P ((Over.pullback f).map g).left
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasPullbacks C<VAR>P : MorphismProperty C<VAR>hP : P.StableUnderBaseChange<VAR>S S' : C<VAR>f : S' ⟶ S<VAR>X Y : Over S<VAR>g : X ⟶ Y<VAR>H : P g.left<VAR>this : P.RespectsIso<VAR>e : pullback g.left (pullback.fst Y.hom f) ≅ pullback X.hom f := pullbackRightPullbackFstIso Y.hom f g.left ≪≫ pullback.congrHom ⋯ ⋯<GOAL>P ((Over.pullback f).map g).left
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasPullbacks C<VAR>P : MorphismProperty C<VAR>hP : P.StableUnderBaseChange<VAR>S S' : C<VAR>f : S' ⟶ S<VAR>X Y : Over S<VAR>g : X ⟶ Y<VAR>H : P g.left<VAR>this✝ : P.RespectsIso<VAR>e : pullback g.left (pullback.fst Y.hom f) ≅ pullback X.hom f := pullbackRightPullbackFstIso Y.hom f g.left ≪≫ pullback.congrHom ⋯ ⋯<VAR>this : e.inv ≫ pullback.snd g.left (pullback.fst Y.hom f) = ((Over.pullback f).map g).left<GOAL>P ((Over.pullback f).map g).left
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasPullbacks C<VAR>P : MorphismProperty C<VAR>hP : P.StableUnderBaseChange<VAR>S S' : C<VAR>f : S' ⟶ S<VAR>X Y : Over S<VAR>g : X ⟶ Y<VAR>H : P g.left<VAR>this✝ : P.RespectsIso<VAR>e : pullback g.left (pullback.fst Y.hom f) ≅ pullback X.hom f := pullbackRightPullbackFstIso Y.hom f g.left ≪≫ pullback.congrHom ⋯ ⋯<VAR>this : e.inv ≫ pullback.snd g.left (pullback.fst Y.hom f) = ((Over.pullback f).map g).left<GOAL>P (pullback.snd g.left (pullback.fst Y.hom f))
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝ : Group G<VAR>hN : Nontrivial G<VAR>tfG : IsTorsionFree G<GOAL>∃ g, ¬IsOfFinOrder g
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝ : Group G<VAR>hN : Nontrivial G<VAR>tfG : IsTorsionFree G<VAR>x : G<VAR>hx : x ≠ 1<GOAL>∃ g, ¬IsOfFinOrder g
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : LaxMonoidalFunctor C D<VAR>X : C<GOAL>(ρ_ (F.obj X)).inv ≫ F.obj X ◁ F.ε ≫ F.μ X (𝟙_ C) = F.map (ρ_ X).inv
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>f : α → β<VAR>g✝ : β → α<VAR>g : ↑(range f) → α<VAR>hf₁ : Measurable f<VAR>hf₂ : MeasurableSet (range f)<VAR>hg : Measurable g<VAR>H : LeftInverse g (rangeFactorization f)<GOAL>MeasurableEmbedding f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>f : α → β<VAR>g✝ : β → α<VAR>g : ↑(range f) → α<VAR>hf₁ : Measurable f<VAR>hf₂ : MeasurableSet (range f)<VAR>hg : Measurable g<VAR>H : LeftInverse g (rangeFactorization f)<VAR>e : α ≃ᵐ ↑(range f) := { toFun := rangeFactorization f, invFun := g, left_inv := H, right_inv := ⋯, measurable_toFun := ⋯, measurable_invFun := hg }<GOAL>MeasurableEmbedding f
<VAR>α : Type u_1<VAR>inst✝ : AddMonoidWithOne α<VAR>m n : PosNum<GOAL>↑(m + n) = ↑m + ↑n
<VAR>R : Type u_1<VAR>inst✝⁷ : CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : Finite m<VAR>inst✝⁴ : DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝³ : AddCommMonoid M₁<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>f : M₁ →ₗ[R] M₂<GOAL>(toLin v₁ v₂) ((toMatrix v₁ v₂) f) = f
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>G₁ G₂ : SimpleGraph V<VAR>inst✝⁴ : Fintype ↑G.edgeSet<VAR>inst✝³ : Fintype ↑G₁.edgeSet<VAR>inst✝² : Fintype ↑G₂.edgeSet<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableEq V<GOAL>⊤.edgeFinset = filter (fun e => ¬e.IsDiag) univ
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>G₁ G₂ : SimpleGraph V<VAR>inst✝⁴ : Fintype ↑G.edgeSet<VAR>inst✝³ : Fintype ↑G₁.edgeSet<VAR>inst✝² : Fintype ↑G₂.edgeSet<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableEq V<GOAL>↑⊤.edgeFinset = ↑(filter (fun e => ¬e.IsDiag) univ)
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I : Box ι<VAR>i : ι<VAR>x : ℝ<VAR>y : ι → ℝ<GOAL>↑(I.splitLower i x) = ↑I ∩ {y | y i ≤ x}
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I : Box ι<VAR>i : ι<VAR>x : ℝ<VAR>y : ι → ℝ<GOAL>(univ.pi fun i_1 => Ioc (I.lower i_1) (update I.upper i (min x (I.upper i)) i_1)) = ↑I ∩ {y | y i ≤ x}
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I : Box ι<VAR>i : ι<VAR>x : ℝ<VAR>y✝ y : ι → ℝ<GOAL>(y ∈ univ.pi fun i_1 => Ioc (I.lower i_1) (update I.upper i (min x (I.upper i)) i_1)) ↔ y ∈ ↑I ∩ {y | y i ≤ x}
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I : Box ι<VAR>i : ι<VAR>x : ℝ<VAR>y✝ y : ι → ℝ<GOAL>(∀ (x : ι), I.lower x < y x) ∧ y i ≤ x ∧ y ≤ I.upper ↔ (∀ (x : ι), I.lower x < y x) ∧ y ≤ I.upper ∧ y i ≤ x
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : NonAssocSemiring R<VAR>M : Submonoid R<VAR>inst✝¹ : NonAssocSemiring S<VAR>inst✝ : NonAssocSemiring T<VAR>s : Set R<VAR>p : (x : R) → x ∈ closure s → Prop<VAR>mem : ∀ (x : R) (h : x ∈ s), p x ⋯<VAR>zero : p 0 ⋯<VAR>one : p 1 ⋯<VAR>add : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x + y) ⋯<VAR>mul : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) ⋯<VAR>a : R<VAR>ha : a ∈ closure s<GOAL>p a ha
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : NonAssocSemiring R<VAR>M : Submonoid R<VAR>inst✝¹ : NonAssocSemiring S<VAR>inst✝ : NonAssocSemiring T<VAR>s : Set R<VAR>p : (x : R) → x ∈ closure s → Prop<VAR>mem : ∀ (x : R) (h : x ∈ s), p x ⋯<VAR>zero : p 0 ⋯<VAR>one : p 1 ⋯<VAR>add : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x + y) ⋯<VAR>mul : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) ⋯<VAR>a : R<VAR>ha : a ∈ closure s<GOAL>∃ (x : a ∈ closure s), p a x
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : NonAssocSemiring R<VAR>M : Submonoid R<VAR>inst✝¹ : NonAssocSemiring S<VAR>inst✝ : NonAssocSemiring T<VAR>s : Set R<VAR>p : (x : R) → x ∈ closure s → Prop<VAR>mem : ∀ (x : R) (h : x ∈ s), p x ⋯<VAR>zero : p 0 ⋯<VAR>one : p 1 ⋯<VAR>add : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x + y) ⋯<VAR>mul : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) ⋯<VAR>a : R<VAR>ha : a ∈ closure s<GOAL>∀ (x y : R), (∃ (x_1 : x ∈ closure s), p x x_1) → (∃ (x : y ∈ closure s), p y x) → ∃ (x_1 : x + y ∈ closure s), p (x + y) x_1
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : NonAssocSemiring R<VAR>M : Submonoid R<VAR>inst✝¹ : NonAssocSemiring S<VAR>inst✝ : NonAssocSemiring T<VAR>s : Set R<VAR>p : (x : R) → x ∈ closure s → Prop<VAR>mem : ∀ (x : R) (h : x ∈ s), p x ⋯<VAR>zero : p 0 ⋯<VAR>one : p 1 ⋯<VAR>add : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x + y) ⋯<VAR>mul : ∀ (x : R) (hx : x ∈ closure s) (y : R) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) ⋯<VAR>a : R<VAR>ha : a ∈ closure s<GOAL>∀ (x y : R), (∃ (x_1 : x ∈ closure s), p x x_1) → (∃ (x : y ∈ closure s), p y x) → ∃ (x_1 : x * y ∈ closure s), p (x * y) x_1
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Semiring R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>σ₁₂ : R →+* R₂<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s : Set M<VAR>f g : F<GOAL>Set.EqOn ⇑f ⇑g ↑(span R s) ↔ Set.EqOn (⇑f) (⇑g) s
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Semiring R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>σ₁₂ : R →+* R₂<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s : Set M<VAR>f g : F<GOAL>s ⊆ ↑(eqLocus f g) ↔ Set.EqOn (⇑f) (⇑g) s
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>inst✝⁵ : Semiring R₁<VAR>inst✝⁴ : Semiring R₂<VAR>inst✝³ : Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>σ : R₁ →+* R₂<VAR>σ' : R₂ →+* R₁<VAR>inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝¹ : RingHomSurjective σ₁₂<VAR>inst✝ : RingHomSurjective σ₂₃<GOAL>Function.Surjective ⇑σ₁₃
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>inst✝⁵ : Semiring R₁<VAR>inst✝⁴ : Semiring R₂<VAR>inst✝³ : Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>σ : R₁ →+* R₂<VAR>σ' : R₂ →+* R₁<VAR>inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝¹ : RingHomSurjective σ₁₂<VAR>inst✝ : RingHomSurjective σ₂₃<VAR>this : Function.Surjective (⇑σ₂₃ ∘ ⇑σ₁₂)<GOAL>Function.Surjective ⇑σ₁₃
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>μ : Measure E<VAR>F : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : CompleteSpace F<VAR>inst✝¹ : IsFiniteMeasure ℙ<VAR>X : Ω → E<VAR>inst✝ : HasPDF X ℙ μ<VAR>f : E → F<VAR>hf : AEStronglyMeasurable f μ<GOAL>∫ (x : E), (pdf X ℙ μ x).toReal • f x ∂μ = ∫ (x : Ω), f (X x) ∂ℙ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>e : α ↪o β<VAR>he : (range ⇑e).OrdConnected<VAR>x y : α<GOAL>⇑e '' Ioc x y = Ioc (e x) (e y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f : Filter α<VAR>u : α → ℝ≥0∞<VAR>a : ℝ≥0∞<VAR>ha : a ≠ ⊤<GOAL>Tendsto u f (𝓝 a) ↔ ∀ ε > 0, ∀ᶠ (x : α) in f, u x ∈ Icc (a - ε) (a + ε)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>o : α → Option β<VAR>f : α → σ<VAR>g : α → β →. σ<VAR>ho : Computable o<VAR>hf : Computable f<VAR>hg : Partrec₂ g<VAR>this : Partrec fun a => Nat.casesOn (encode (o a)) (Part.some (f a)) fun n => (↑(decode n)).bind (g a)<VAR>a : α<GOAL>(Nat.casesOn (encode (o a)) (Part.some (f a)) fun n => (↑(decode n)).bind (g a)) = Option.casesOn (o a) (Part.some (f a)) (g a)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Sort w<VAR>inst✝ : DecidableEq α<VAR>xs : List ((_ : α) × α)<VAR>hperm : map Sigma.fst xs ~ map Sigma.snd xs<VAR>hnodup : (map Sigma.snd xs).Nodup<VAR>xs₀ : List α<VAR>h₀ : map Sigma.fst xs = xs₀<VAR>xs₁ : List α<VAR>h₁ : map Sigma.snd xs = xs₁<GOAL>Injective (mapToSelf xs hperm hnodup).apply
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Sort w<VAR>inst✝ : DecidableEq α<VAR>xs : List ((_ : α) × α)<VAR>hperm : map Sigma.fst xs ~ map Sigma.snd xs<VAR>hnodup : (map Sigma.snd xs).Nodup<VAR>xs₀ : List α<VAR>h₀ : map Sigma.fst xs = xs₀<VAR>xs₁ : List α<VAR>h₁ : map Sigma.snd xs = xs₁<VAR>hxs : xs = List.toFinmap' (xs₀.zip xs₁)<GOAL>Injective (mapToSelf xs hperm hnodup).apply
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Sort w<VAR>inst✝ : DecidableEq α<VAR>xs : List ((_ : α) × α)<VAR>xs₀ : List α<VAR>h₀ : map Sigma.fst xs = xs₀<VAR>xs₁ : List α<VAR>h₁ : map Sigma.snd xs = xs₁<VAR>hxs : xs = List.toFinmap' (xs₀.zip xs₁)<VAR>hperm : map Sigma.fst (List.toFinmap' (xs₀.zip xs₁)) ~ map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))<VAR>hnodup : (map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))).Nodup<GOAL>Injective (mapToSelf (List.toFinmap' (xs₀.zip xs₁)) hperm hnodup).apply
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Sort w<VAR>inst✝ : DecidableEq α<VAR>xs : List ((_ : α) × α)<VAR>xs₀ : List α<VAR>h₀ : map Sigma.fst xs = xs₀<VAR>xs₁ : List α<VAR>h₁ : map Sigma.snd xs = xs₁<VAR>hxs : xs = List.toFinmap' (xs₀.zip xs₁)<VAR>hperm : map Sigma.fst (List.toFinmap' (xs₀.zip xs₁)) ~ map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))<VAR>hnodup : (map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))).Nodup<GOAL>xs₀.Nodup
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Sort w<VAR>inst✝ : DecidableEq α<VAR>xs : List ((_ : α) × α)<VAR>xs₀ : List α<VAR>h₀ : map Sigma.fst xs = xs₀<VAR>xs₁ : List α<VAR>h₁ : map Sigma.snd xs = xs₁<VAR>hxs : xs = List.toFinmap' (xs₀.zip xs₁)<VAR>hperm : map Sigma.fst (List.toFinmap' (xs₀.zip xs₁)) ~ map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))<VAR>hnodup : (map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))).Nodup<GOAL>xs₀ ~ xs₁
<VAR>α : Type u<VAR>β : Type v<VAR>a : α<VAR>f : Filter α<VAR>t : TopologicalSpace α<GOAL>t ≤ nhdsAdjoint a f ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
<VAR>n : ℕ<VAR>α : Type u_1<VAR>a : α<VAR>i : Fin n<GOAL>(replicate n a).get i = a
<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>inst✝¹² : SmoothManifoldWithCorners I 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>inst✝⁶ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝³ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝² : TopologicalSpace M''<VAR>inst✝¹ : ChartedSpace H'' M''<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>s : Set M<VAR>x : M<VAR>f : M × M' → M''<VAR>p : M × M'<VAR>hf : MDifferentiableAt (I.prod I') I'' f p<GOAL>mfderiv (I.prod I') I'' f p = mfderiv (I.prod I') I'' (fun z => f (z.1, p.2)) p + mfderiv (I.prod I') I'' (fun z => f (p.1, z.2)) p
<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>inst✝¹² : SmoothManifoldWithCorners I 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>inst✝⁶ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝³ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝² : TopologicalSpace M''<VAR>inst✝¹ : ChartedSpace H'' M''<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>s : Set M<VAR>x : M<VAR>f : M × M' → M''<VAR>p : M × M'<VAR>hf : MDifferentiableAt (I.prod I') I'' f p<GOAL>mfderiv (I.prod I') I'' f p = (mfderiv (I.prod I') I'' f (p.1, p.2)).comp ((ContinuousLinearMap.fst 𝕜 (TangentSpace I p.1) (TangentSpace I' p.2)).prod 0 + ContinuousLinearMap.prod 0 (ContinuousLinearMap.snd 𝕜 (TangentSpace I p.1) (TangentSpace I' p.2)))
<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>inst✝¹² : SmoothManifoldWithCorners I 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>inst✝⁶ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝³ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝² : TopologicalSpace M''<VAR>inst✝¹ : ChartedSpace H'' M''<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>s : Set M<VAR>x : M<VAR>f : M × M' → M''<VAR>p : M × M'<VAR>hf : MDifferentiableAt (I.prod I') I'' f p<GOAL>(mfderiv (I.prod I') I'' f (p.1, p.2)).comp ((ContinuousLinearMap.fst 𝕜 (TangentSpace I p.1) (TangentSpace I' p.2)).prod 0 + ContinuousLinearMap.prod 0 (ContinuousLinearMap.snd 𝕜 (TangentSpace I p.1) (TangentSpace I' p.2))) = mfderiv (I.prod I') I'' f p
<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>inst✝¹² : SmoothManifoldWithCorners I 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>inst✝⁶ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝³ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝² : TopologicalSpace M''<VAR>inst✝¹ : ChartedSpace H'' M''<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>s : Set M<VAR>x : M<VAR>f : M × M' → M''<VAR>p : M × M'<VAR>hf : MDifferentiableAt (I.prod I') I'' f p<GOAL>(ContinuousLinearMap.fst 𝕜 (TangentSpace I p.1) (TangentSpace I' p.2)).prod 0 + ContinuousLinearMap.prod 0 (ContinuousLinearMap.snd 𝕜 (TangentSpace I p.1) (TangentSpace I' p.2)) = ContinuousLinearMap.id 𝕜 (TangentSpace (I.prod I') (p.1, p.2))
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℕ<VAR>a b : α<VAR>n : ℕ<VAR>inst✝ : DecidableEq α<VAR>h : a ≠ b<GOAL>multinomial {a, b} f = (f a + f b)! / ((f a)! * (f b)!)
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>t✝ : M → Set F<VAR>n : ℕ∞<VAR>s t : Set M<VAR>hs : IsOpen s<VAR>ht : IsClosed t<VAR>h : t ⊆ s<GOAL>∃ f, Smooth I 𝓘(ℝ, ℝ) f ∧ range f ⊆ Icc 0 1 ∧ support f = s ∧ ∀ (x : M), x ∈ t ↔ f x = 1
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>t✝ : M → Set F<VAR>n : ℕ∞<VAR>s t : Set M<VAR>hs : IsOpen s<VAR>ht : IsClosed t<VAR>h : t ⊆ s<VAR>f : M → ℝ<VAR>f_supp : support f = s<VAR>f_diff : Smooth I 𝓘(ℝ, ℝ) f<VAR>f_pos : ∀ (x : M), 0 ≤ f x<GOAL>∃ f, Smooth I 𝓘(ℝ, ℝ) f ∧ range f ⊆ Icc 0 1 ∧ support f = s ∧ ∀ (x : M), x ∈ t ↔ f x = 1
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>t✝ : M → Set F<VAR>n : ℕ∞<VAR>s t : Set M<VAR>hs : IsOpen s<VAR>ht : IsClosed t<VAR>h : t ⊆ s<VAR>f : M → ℝ<VAR>f_supp : support f = s<VAR>f_diff : Smooth I 𝓘(ℝ, ℝ) f<VAR>f_pos : ∀ (x : M), 0 ≤ f x<VAR>g : M → ℝ<VAR>g_supp : support g = tᶜ<VAR>g_diff : Smooth I 𝓘(ℝ, ℝ) g<VAR>g_pos : ∀ (x : M), 0 ≤ g x<GOAL>∃ f, Smooth I 𝓘(ℝ, ℝ) f ∧ range f ⊆ Icc 0 1 ∧ support f = s ∧ ∀ (x : M), x ∈ t ↔ f x = 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → ℝ<VAR>x x₀ : ℝ<VAR>n : ℕ<VAR>hx : x₀ < x<VAR>hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)<VAR>hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x)<VAR>gcont : ContinuousOn id (Icc x₀ x)<GOAL>∃ x' ∈ Ioo x₀ x, f x - taylorWithinEval f n (Icc x₀ x) x₀ x = iteratedDerivWithin (n + 1) f (Icc x₀ x) x' * (x - x') ^ n / ↑n ! * (x - x₀)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → ℝ<VAR>x x₀ : ℝ<VAR>n : ℕ<VAR>hx : x₀ < x<VAR>hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)<VAR>hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x)<VAR>gcont : ContinuousOn id (Icc x₀ x)<VAR>gdiff : ∀ x_1 ∈ Ioo x₀ x, HasDerivAt id ((fun x => 1) x_1) x_1<GOAL>∃ x' ∈ Ioo x₀ x, f x - taylorWithinEval f n (Icc x₀ x) x₀ x = iteratedDerivWithin (n + 1) f (Icc x₀ x) x' * (x - x') ^ n / ↑n ! * (x - x₀)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → ℝ<VAR>x x₀ : ℝ<VAR>n : ℕ<VAR>hx : x₀ < x<VAR>hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)<VAR>hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x)<VAR>gcont : ContinuousOn id (Icc x₀ x)<VAR>gdiff : ∀ x_1 ∈ Ioo x₀ x, HasDerivAt id ((fun x => 1) x_1) x_1<VAR>y : ℝ<VAR>hy : y ∈ Ioo x₀ x<VAR>h : f x - taylorWithinEval f n (Icc x₀ x) x₀ x = ((x - y) ^ n / ↑n ! * (id x - id x₀) / 1) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y<GOAL>∃ x' ∈ Ioo x₀ x, f x - taylorWithinEval f n (Icc x₀ x) x₀ x = iteratedDerivWithin (n + 1) f (Icc x₀ x) x' * (x - x') ^ n / ↑n ! * (x - x₀)