ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>HasContDiffBump E<VAR>MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>μ : MeasureTheory.Measure E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>μ.IsOpenPosMeasure<GOAL>HasCompactSupport (f.normed μ)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>HasContDiffBump E<VAR>MeasurableSpace E<VAR>c : E<VAR>μ : MeasureTheory.Measure E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>μ.IsOpenPosMeasure<VAR>ι : Type u_2<VAR>φ : ι → ContDiffBump c<VAR>l : Filter ι<VAR>hφ : Filter.Tendsto (fun i => (φ i).rOut) l (𝓝 0)<GOAL>Filter.Tendsto (fun i => Function.support fun x => (φ i).normed μ x) l (𝓝 c).smallSets
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>HasContDiffBump E<VAR>MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>μ : MeasureTheory.Measure E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>μ.IsOpenPosMeasure<VAR>X : Type u_2<VAR>NormedAddCommGroup X<VAR>NormedSpace ℝ X<VAR>CompleteSpace X<VAR>z : X<GOAL>∫ (x : E), f.normed μ x • z ∂μ = z
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>HasContDiffBump E<VAR>MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>μ : MeasureTheory.Measure E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<GOAL>(μ (Metric.closedBall c f.rIn)).toReal ≤ ∫ (x : E), ↑f x ∂μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>HasContDiffBump E<VAR>MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>μ : MeasureTheory.Measure E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>μ.IsOpenPosMeasure<VAR>x : E<GOAL>f.normed μ x ≤ 1 / (μ (Metric.closedBall c f.rIn)).toReal
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>HasContDiffBump E<VAR>MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>μ : MeasureTheory.Measure E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<GOAL>∫ (x : E), ↑f x ∂μ ≤ (μ (Metric.closedBall c f.rOut)).toReal
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>HasContDiffBump E<VAR>MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>μ : MeasureTheory.Measure E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>μ.IsAddHaarMeasure<VAR>K : ℝ<VAR>h : f.rOut ≤ K * f.rIn<GOAL>(μ (Metric.closedBall c f.rOut)).toReal / K ^ FiniteDimensional.finrank ℝ E ≤ ∫ (x : E), ↑f x ∂μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>HasContDiffBump E<VAR>MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>μ : MeasureTheory.Measure E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>μ.IsOpenPosMeasure<VAR>μ.IsAddHaarMeasure<VAR>K : ℝ<VAR>h : f.rOut ≤ K * f.rIn<VAR>x : E<GOAL>f.normed μ x ≤ K ^ FiniteDimensional.finrank ℝ E / (μ (Metric.closedBall c f.rOut)).toReal
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>LocallyCompactSpace 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>MeasurableSpace E<VAR>OpensMeasurableSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : E → F<VAR>v : E<VAR>hf : Continuous f<GOAL>MeasurableSet {x | LineDifferentiableAt 𝕜 f x v}
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>LocallyCompactSpace 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>MeasurableSpace E<VAR>OpensMeasurableSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : E → F<VAR>v : E<VAR>MeasurableSpace F<VAR>BorelSpace F<VAR>hf : Continuous f<GOAL>Measurable fun x => lineDeriv 𝕜 f x v
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>LocallyCompactSpace 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>MeasurableSpace E<VAR>OpensMeasurableSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : E → F<VAR>v : E<VAR>SecondCountableTopologyEither E F<VAR>hf : Continuous f<GOAL>MeasureTheory.StronglyMeasurable fun x => lineDeriv 𝕜 f x v
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>LocallyCompactSpace 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>MeasurableSpace E<VAR>OpensMeasurableSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : E → F<VAR>v : E<VAR>MeasurableSpace F<VAR>BorelSpace F<VAR>hf : Continuous f<VAR>μ : MeasureTheory.Measure E<GOAL>AEMeasurable (fun x => lineDeriv 𝕜 f x v) μ
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>LocallyCompactSpace 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>MeasurableSpace E<VAR>OpensMeasurableSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : E → F<VAR>v : E<VAR>SecondCountableTopologyEither E F<VAR>hf : Continuous f<VAR>μ : MeasureTheory.Measure E<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => lineDeriv 𝕜 f x v) μ
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>LocallyCompactSpace 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>MeasurableSpace E<VAR>OpensMeasurableSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : E → F<VAR>SecondCountableTopology E<VAR>hf : Continuous f<GOAL>MeasurableSet {p | LineDifferentiableAt 𝕜 f p.1 p.2}
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>LocallyCompactSpace 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>MeasurableSpace E<VAR>OpensMeasurableSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : E → F<VAR>SecondCountableTopology E<VAR>MeasurableSpace F<VAR>BorelSpace F<VAR>hf : Continuous f<GOAL>Measurable fun p => lineDeriv 𝕜 f p.1 p.2
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>LocallyCompactSpace 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>MeasurableSpace E<VAR>OpensMeasurableSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : E → F<VAR>SecondCountableTopology E<VAR>hf : Continuous f<GOAL>MeasureTheory.StronglyMeasurable fun p => lineDeriv 𝕜 f p.1 p.2
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>LocallyCompactSpace 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>MeasurableSpace E<VAR>OpensMeasurableSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : E → F<VAR>SecondCountableTopology E<VAR>MeasurableSpace F<VAR>BorelSpace F<VAR>hf : Continuous f<VAR>μ : MeasureTheory.Measure (E × E)<GOAL>AEMeasurable (fun p => lineDeriv 𝕜 f p.1 p.2) μ
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>LocallyCompactSpace 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>MeasurableSpace E<VAR>OpensMeasurableSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : E → F<VAR>SecondCountableTopology E<VAR>hf : Continuous f<VAR>μ : MeasureTheory.Measure (E × E)<GOAL>MeasureTheory.AEStronglyMeasurable (fun p => lineDeriv 𝕜 f p.1 p.2) μ
<VAR>f f' : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a < b<VAR>hfc : ContinuousOn f (Set.Icc a b)<VAR>hfI : f a = f b<VAR>hff' : ∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x<GOAL>∃ c ∈ Set.Ioo a b, f' c = 0
<VAR>f : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a < b<VAR>hfc : ContinuousOn f (Set.Icc a b)<VAR>hfI : f a = f b<GOAL>∃ c ∈ Set.Ioo a b, deriv f c = 0
<VAR>f f' : ℝ → ℝ<VAR>a b l : ℝ<VAR>hab : a < b<VAR>hfa : Filter.Tendsto f (𝓝[>] a) (𝓝 l)<VAR>hfb : Filter.Tendsto f (𝓝[<] b) (𝓝 l)<VAR>hff' : ∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x<GOAL>∃ c ∈ Set.Ioo a b, f' c = 0
<VAR>f : ℝ → ℝ<VAR>a b l : ℝ<VAR>hab : a < b<VAR>hfa : Filter.Tendsto f (𝓝[>] a) (𝓝 l)<VAR>hfb : Filter.Tendsto f (𝓝[<] b) (𝓝 l)<GOAL>∃ c ∈ Set.Ioo a b, deriv f c = 0
<VAR>p : Polynomial ℝ<GOAL>p.roots.toFinset.card ≤ ((Polynomial.derivative p).roots.toFinset \ p.roots.toFinset).card + 1
<VAR>p : Polynomial ℝ<GOAL>p.roots.toFinset.card ≤ (Polynomial.derivative p).roots.toFinset.card + 1
<VAR>p : Polynomial ℝ<GOAL>Multiset.card p.roots ≤ Multiset.card (Polynomial.derivative p).roots + 1
<VAR>F : Type u_1<VAR>CommRing F<VAR>Algebra F ℝ<VAR>p : Polynomial F<GOAL>Fintype.card ↑(p.rootSet ℝ) ≤ Fintype.card ↑((Polynomial.derivative p).rootSet ℝ) + 1
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ E<VAR>InnerProductSpace ℝ F<VAR>f : E → F<VAR>x : E<GOAL>ConformalAt f x ↔ ∃ c, 0 < c ∧ ∀ (u v : E), ⟪(fderiv ℝ f x) u, (fderiv ℝ f x) v⟫_ℝ = c * ⟪u, v⟫_ℝ
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ E<VAR>InnerProductSpace ℝ F<VAR>f : E → F<VAR>x : E<VAR>f' : E →L[ℝ] F<VAR>h : HasFDerivAt f f' x<GOAL>ConformalAt f x ↔ ∃ c, 0 < c ∧ ∀ (u v : E), ⟪f' u, f' v⟫_ℝ = c * ⟪u, v⟫_ℝ
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ E<VAR>InnerProductSpace ℝ F<VAR>f : E → F<VAR>x : E<VAR>h : ConformalAt f x<GOAL>0 < conformalFactorAt h
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ E<VAR>InnerProductSpace ℝ F<VAR>f : E → F<VAR>x : E<VAR>h : ConformalAt f x<VAR>u v : E<GOAL>⟪(fderiv ℝ f x) u, (fderiv ℝ f x) v⟫_ℝ = conformalFactorAt h * ⟪u, v⟫_ℝ
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ E<VAR>InnerProductSpace ℝ F<VAR>f : E → F<VAR>x : E<VAR>f' : E →L[ℝ] F<VAR>h : HasFDerivAt f f' x<VAR>H : ConformalAt f x<VAR>u v : E<GOAL>⟪f' u, f' v⟫_ℝ = conformalFactorAt H * ⟪u, v⟫_ℝ
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>CompleteSpace G<VAR>self : ImplicitFunctionData 𝕜 E F G<GOAL>HasStrictFDerivAt self.leftFun self.leftDeriv self.pt
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>CompleteSpace G<VAR>self : ImplicitFunctionData 𝕜 E F G<GOAL>IsCompl (LinearMap.ker self.leftDeriv) (LinearMap.ker self.rightDeriv)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>CompleteSpace G<VAR>self : ImplicitFunctionData 𝕜 E F G<GOAL>LinearMap.range self.rightDeriv = ⊤
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>CompleteSpace G<VAR>self : ImplicitFunctionData 𝕜 E F G<GOAL>HasStrictFDerivAt self.rightFun self.rightDeriv self.pt
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>CompleteSpace G<VAR>self : ImplicitFunctionData 𝕜 E F G<GOAL>LinearMap.range self.leftDeriv = ⊤
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>CompleteSpace G<VAR>φ : ImplicitFunctionData 𝕜 E F G<VAR>x : E<GOAL>φ.prodFun x = (φ.leftFun x, φ.rightFun x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>CompleteSpace G<VAR>φ : ImplicitFunctionData 𝕜 E F G<GOAL>HasStrictFDerivAt φ.prodFun (↑(φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯)) φ.pt
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>CompleteSpace G<VAR>φ : ImplicitFunctionData 𝕜 E F G<GOAL>↑φ.toPartialHomeomorph = φ.prodFun
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>CompleteSpace G<VAR>φ : ImplicitFunctionData 𝕜 E F G<VAR>x : E<GOAL>↑φ.toPartialHomeomorph x = (φ.leftFun x, φ.rightFun x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>CompleteSpace G<VAR>φ : ImplicitFunctionData 𝕜 E F G<GOAL>φ.pt ∈ φ.toPartialHomeomorph.source
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>CompleteSpace G<VAR>φ : ImplicitFunctionData 𝕜 E F G<GOAL>(φ.leftFun φ.pt, φ.rightFun φ.pt) ∈ φ.toPartialHomeomorph.target
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>CompleteSpace G<VAR>φ : ImplicitFunctionData 𝕜 E F G<GOAL>∀ᶠ (p : F × G) in 𝓝 (φ.prodFun φ.pt), φ.prodFun (φ.implicitFunction p.1 p.2) = p
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>CompleteSpace G<VAR>φ : ImplicitFunctionData 𝕜 E F G<GOAL>∀ᶠ (p : F × G) in 𝓝 (φ.prodFun φ.pt), φ.leftFun (φ.implicitFunction p.1 p.2) = p.1
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>CompleteSpace G<VAR>φ : ImplicitFunctionData 𝕜 E F G<GOAL>∀ᶠ (p : F × G) in 𝓝 (φ.prodFun φ.pt), φ.rightFun (φ.implicitFunction p.1 p.2) = p.2
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>CompleteSpace G<VAR>φ : ImplicitFunctionData 𝕜 E F G<GOAL>∀ᶠ (x : E) in 𝓝 φ.pt, φ.implicitFunction (φ.leftFun x) (φ.rightFun x) = x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>CompleteSpace G<VAR>φ : ImplicitFunctionData 𝕜 E F G<GOAL>Filter.map φ.leftFun (𝓝 φ.pt) = 𝓝 (φ.leftFun φ.pt)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>CompleteSpace G<VAR>φ : ImplicitFunctionData 𝕜 E F G<VAR>g'inv : G →L[𝕜] E<VAR>hg'inv : φ.rightDeriv.comp g'inv = ContinuousLinearMap.id 𝕜 G<VAR>hg'invf : φ.leftDeriv.comp g'inv = 0<GOAL>HasStrictFDerivAt (φ.implicitFunction (φ.leftFun φ.pt)) g'inv (φ.rightFun φ.pt)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>hf' : LinearMap.range f' = ⊤<VAR>hker : (LinearMap.ker f').ClosedComplemented<VAR>x : E<GOAL>(↑(HasStrictFDerivAt.implicitToPartialHomeomorphOfComplemented f f' hf hf' hker) x).1 = f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>hf' : LinearMap.range f' = ⊤<VAR>hker : (LinearMap.ker f').ClosedComplemented<VAR>y : E<GOAL>↑(HasStrictFDerivAt.implicitToPartialHomeomorphOfComplemented f f' hf hf' hker) y = (f y, (Classical.choose hker) (y - a))
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>hf' : LinearMap.range f' = ⊤<VAR>hker : (LinearMap.ker f').ClosedComplemented<VAR>y : ↥(LinearMap.ker f')<GOAL>↑(HasStrictFDerivAt.implicitToPartialHomeomorphOfComplemented f f' hf hf' hker) (↑y + a) = (f (↑y + a), y)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>hf' : LinearMap.range f' = ⊤<VAR>hker : (LinearMap.ker f').ClosedComplemented<GOAL>↑(HasStrictFDerivAt.implicitToPartialHomeomorphOfComplemented f f' hf hf' hker) a = (f a, 0)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>hf' : LinearMap.range f' = ⊤<VAR>hker : (LinearMap.ker f').ClosedComplemented<GOAL>a ∈ (HasStrictFDerivAt.implicitToPartialHomeomorphOfComplemented f f' hf hf' hker).source
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>hf' : LinearMap.range f' = ⊤<VAR>hker : (LinearMap.ker f').ClosedComplemented<GOAL>(f a, 0) ∈ (HasStrictFDerivAt.implicitToPartialHomeomorphOfComplemented f f' hf hf' hker).target
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>hf' : LinearMap.range f' = ⊤<VAR>hker : (LinearMap.ker f').ClosedComplemented<GOAL>∀ᶠ (p : F × ↥(LinearMap.ker f')) in 𝓝 (f a, 0), f (HasStrictFDerivAt.implicitFunctionOfComplemented f f' hf hf' hker p.1 p.2) = p.1
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>hf' : LinearMap.range f' = ⊤<VAR>hker : (LinearMap.ker f').ClosedComplemented<GOAL>∀ᶠ (x : E) in 𝓝 a, HasStrictFDerivAt.implicitFunctionOfComplemented f f' hf hf' hker (f x) (↑(HasStrictFDerivAt.implicitToPartialHomeomorphOfComplemented f f' hf hf' hker) x).2 = x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>hf' : LinearMap.range f' = ⊤<VAR>hker : (LinearMap.ker f').ClosedComplemented<GOAL>HasStrictFDerivAt.implicitFunctionOfComplemented f f' hf hf' hker (f a) 0 = a
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>hf' : LinearMap.range f' = ⊤<VAR>hker : (LinearMap.ker f').ClosedComplemented<GOAL>HasStrictFDerivAt (HasStrictFDerivAt.implicitFunctionOfComplemented f f' hf hf' hker (f a)) (LinearMap.ker f').subtypeL 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>FiniteDimensional 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>hf' : LinearMap.range f' = ⊤<VAR>x : E<GOAL>(↑(HasStrictFDerivAt.implicitToPartialHomeomorph f f' hf hf') x).1 = f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>FiniteDimensional 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>hf' : LinearMap.range f' = ⊤<VAR>y : ↥(LinearMap.ker f')<GOAL>↑(HasStrictFDerivAt.implicitToPartialHomeomorph f f' hf hf') (↑y + a) = (f (↑y + a), y)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>FiniteDimensional 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>hf' : LinearMap.range f' = ⊤<GOAL>↑(HasStrictFDerivAt.implicitToPartialHomeomorph f f' hf hf') a = (f a, 0)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>FiniteDimensional 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>hf' : LinearMap.range f' = ⊤<GOAL>a ∈ (HasStrictFDerivAt.implicitToPartialHomeomorph f f' hf hf').source
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>FiniteDimensional 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>hf' : LinearMap.range f' = ⊤<GOAL>(f a, 0) ∈ (HasStrictFDerivAt.implicitToPartialHomeomorph f f' hf hf').target
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>FiniteDimensional 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>hf' : LinearMap.range f' = ⊤<VAR>α : Type u_4<VAR>l : Filter α<VAR>g₁ : α → F<VAR>g₂ : α → ↥(LinearMap.ker f')<VAR>h₁ : Filter.Tendsto g₁ l (𝓝 (f a))<VAR>h₂ : Filter.Tendsto g₂ l (𝓝 0)<GOAL>Filter.Tendsto (fun t => HasStrictFDerivAt.implicitFunction f f' hf hf' (g₁ t) (g₂ t)) l (𝓝 a)