ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>f g h✝ : Perm α<VAR>h : f.Disjoint g<VAR>x : α<VAR>hg : g x = x<VAR>hf : f (f x) = f x<GOAL>(f * g) x = (g * f) x
<VAR>α : Type u_1<VAR>f g h✝ : Perm α<VAR>h : f.Disjoint g<VAR>x : α<VAR>hg : g x = x<VAR>hf : g (f x) = f x<GOAL>(f * g) x = (g * f) x
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.199007, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.LeftHomologyData<VAR>A : C<VAR>k : A ⟶ S.X₂<VAR>hk : k ≫ S.g = 0<VAR>inst✝ : S.HasLeftHomology<VAR>A' : C<VAR>α : A' ⟶ A<GOAL>(α ≫ k) ≫ S.g = 0
<VAR>n : ℕ<VAR>f : Vector ℕ (n + 1) → ℕ<VAR>hf : Partrec' ↑f<VAR>v : Vector ℕ n<VAR>b : ℕ<GOAL>(b ∈ (Nat.rfind fun n_1 => Part.some (decide (1 - f (n_1 ::ᵥ v) = 0))).bind fun a => ↑pred (f (a ::ᵥ v))) ↔ b ∈ Nat.rfindOpt fun a => ofNat (Option ℕ) (f (a ::ᵥ v))
<VAR>n : ℕ<VAR>f : Vector ℕ (n + 1) → ℕ<VAR>hf : Partrec' ↑f<VAR>v : Vector ℕ n<VAR>b : ℕ<GOAL>(∃ a ∈ Nat.rfind fun n_1 => Part.some (decide (1 ≤ f (n_1 ::ᵥ v))), b = (f (a ::ᵥ v)).pred) ↔ ∃ a ∈ Nat.rfind fun n_1 => ↑(some (ofNat (Option ℕ) (f (n_1 ::ᵥ v))).isSome), ofNat (Option ℕ) (f (a ::ᵥ v)) = some b
<VAR>n : ℕ<VAR>f : Vector ℕ (n + 1) → ℕ<VAR>hf : Partrec' ↑f<VAR>v : Vector ℕ n<VAR>b a : ℕ<GOAL>(a ∈ Nat.rfind fun n_1 => Part.some (decide (1 ≤ f (n_1 ::ᵥ v)))) = (a ∈ Nat.rfind fun n_1 => ↑(some (ofNat (Option ℕ) (f (n_1 ::ᵥ v))).isSome))
<VAR>n : ℕ<VAR>f : Vector ℕ (n + 1) → ℕ<VAR>hf : Partrec' ↑f<VAR>v : Vector ℕ n<VAR>b a : ℕ<VAR>h : a ∈ Nat.rfind fun n_1 => ↑(some (ofNat (Option ℕ) (f (n_1 ::ᵥ v))).isSome)<GOAL>b = (f (a ::ᵥ v)).pred ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b
<VAR>α : Type u<VAR>inst✝¹ : DecidableEq α<VAR>β : Type v<VAR>inst✝ : Finite α<VAR>f g : Perm α<VAR>s : Multiset α<VAR>hs : ∀ (x : α), x ∈ s<GOAL>(f * g).signAux3 hs = f.signAux3 hs * g.signAux3 hs ∧ Pairwise fun x y => (swap x y).signAux3 hs = -1
<VAR>α : Type u<VAR>inst✝¹ : DecidableEq α<VAR>β : Type v<VAR>inst✝ : Finite α<VAR>f g : Perm α<VAR>s : Multiset α<VAR>hs : ∀ (x : α), x ∈ s<VAR>n : ℕ<VAR>e : α ≃ Fin n<GOAL>(f * g).signAux3 hs = f.signAux3 hs * g.signAux3 hs ∧ Pairwise fun x y => (swap x y).signAux3 hs = -1
<VAR>α : Type u<VAR>inst✝¹ : DecidableEq α<VAR>β : Type v<VAR>inst✝ : Finite α<VAR>f g : Perm α<VAR>n : ℕ<VAR>e : α ≃ Fin n<VAR>l : List α<VAR>hs : ∀ (x : α), x ∈ ⟦l⟧<GOAL>(f * g).signAux3 hs = f.signAux3 hs * g.signAux3 hs ∧ Pairwise fun x y => (swap x y).signAux3 hs = -1
<VAR>α : Type u<VAR>inst✝¹ : DecidableEq α<VAR>β : Type v<VAR>inst✝ : Finite α<VAR>f g : Perm α<VAR>n : ℕ<VAR>e : α ≃ Fin n<VAR>l : List α<VAR>hs : ∀ (x : α), x ∈ ⟦l⟧<GOAL>signAux2 l (f * g) = signAux2 l f * signAux2 l g ∧ Pairwise fun x y => signAux2 l (swap x y) = -1
<VAR>α : Type u<VAR>inst✝¹ : DecidableEq α<VAR>β : Type v<VAR>inst✝ : Finite α<VAR>f g : Perm α<VAR>n : ℕ<VAR>e : α ≃ Fin n<VAR>l : List α<VAR>hs : ∀ (x : α), x ∈ ⟦l⟧<VAR>hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e<GOAL>signAux2 l (f * g) = signAux2 l f * signAux2 l g ∧ Pairwise fun x y => signAux2 l (swap x y) = -1
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X A B : C<VAR>f : A ⟶ X<VAR>g : B ⟶ X<VAR>a : ↑(F.obj A)<VAR>b : ↑(F.obj B)<VAR>h : F.map f a = F.map g b<GOAL>((Types.pullbackIsoPullback (F.map f) (F.map g)).inv ≫ (PreservesPullback.iso (F ⋙ FintypeCat.incl) f g).inv ≫ (F ⋙ FintypeCat.incl).map (pullback.snd f g)) ⟨(a, b), h⟩ = b
<VAR>C : Type u<VAR>𝒞 : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : Y ⟶ Z<GOAL>W ◁ g ≫ f ▷ Z = f ▷ Y ≫ X ◁ g
<VAR>x : ℝ<GOAL>ContinuousAt tan x ↔ cos x ≠ 0
<VAR>x : ℝ<VAR>hc : ContinuousAt tan x<VAR>h₀ : cos x = 0<GOAL>False
<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>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>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>h : HasMFDerivWithinAt I I' f s x f'<VAR>h₁ : f₁ =ᶠ[𝓝[s] x] f<VAR>hx : f₁ x = f x<GOAL>HasMFDerivWithinAt I I' f₁ s x f'
<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>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>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>h : HasMFDerivWithinAt I I' f s x f'<VAR>h₁ : f₁ =ᶠ[𝓝[s] x] f<VAR>hx : f₁ x = f x<GOAL>HasFDerivWithinAt (writtenInExtChartAt I I' x f₁) f' (↑(extChartAt I x).symm ⁻¹' s ∩ 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>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>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>h : HasMFDerivWithinAt I I' f s x f'<VAR>h₁ : f₁ =ᶠ[𝓝[s] x] f<VAR>hx : f₁ x = f x<GOAL>writtenInExtChartAt I I' x f₁ =ᶠ[𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x] writtenInExtChartAt I I' x f
<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>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>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>h : HasMFDerivWithinAt I I' f s x f'<VAR>h₁ : f₁ =ᶠ[𝓝[s] x] f<VAR>hx : f₁ x = f x<GOAL>writtenInExtChartAt I I' x f₁ (↑(extChartAt I x) x) = writtenInExtChartAt I I' x f (↑(extChartAt I x) x)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Monoid G<VAR>a b x y : G<VAR>n m : ℕ<VAR>inst✝ : Monoid H<VAR>f : G →* H<VAR>hf : Injective ⇑f<GOAL>IsOfFinOrder (f x) ↔ IsOfFinOrder x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : SemilatticeSup α<VAR>s : Finset β<VAR>H : s.Nonempty<VAR>f : β → α<VAR>b : β<VAR>hb : b ∉ s<GOAL>(cons b s hb).sup' ⋯ f = f b ⊔ s.sup' H f
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : SemilatticeSup α<VAR>s : Finset β<VAR>H : s.Nonempty<VAR>f : β → α<VAR>b : β<VAR>hb : b ∉ s<GOAL>↑((cons b s hb).sup' ⋯ f) = ↑(f b ⊔ s.sup' H f)
<VAR>a b r : ℕ<VAR>hr : 0 < r<VAR>v : ℕ<GOAL>↑(filter (fun x => x ≡ v [MOD r]) (Ioc a b)).card = max (⌊(↑b - ↑v) / ↑r⌋ - ⌊(↑a - ↑v) / ↑r⌋) 0
<VAR>R : Type uR<VAR>inst✝⁶ : Semiring R<VAR>S : Type uS<VAR>inst✝⁵ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝⁴ : Semiring A<VAR>inst✝³ : Algebra S A<VAR>r : R → R → Prop<VAR>inst✝² : Semiring T<VAR>B : Type u₄<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra S B<VAR>s : A → A → Prop<VAR>f g : RingQuot s →ₐ[S] B<VAR>w : f.comp (mkAlgHom S s) = g.comp (mkAlgHom S s)<VAR>x : RingQuot s<GOAL>f x = g x
<VAR>R : Type uR<VAR>inst✝⁶ : Semiring R<VAR>S : Type uS<VAR>inst✝⁵ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝⁴ : Semiring A<VAR>inst✝³ : Algebra S A<VAR>r : R → R → Prop<VAR>inst✝² : Semiring T<VAR>B : Type u₄<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra S B<VAR>s : A → A → Prop<VAR>f g : RingQuot s →ₐ[S] B<VAR>w : f.comp (mkAlgHom S s) = g.comp (mkAlgHom S s)<VAR>x : A<GOAL>f ((mkAlgHom S s) x) = g ((mkAlgHom S s) x)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>o : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Fintype o<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S<VAR>inst✝ : DecidableEq n<VAR>i : n<GOAL>toMvPolynomial 1 i = X i
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>o : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Fintype o<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S<VAR>inst✝ : DecidableEq n<VAR>i : n<GOAL>(monomial (Finsupp.single i 1)) (1 i i) = X i
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>o : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Fintype o<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S<VAR>inst✝ : DecidableEq n<VAR>i : n<GOAL>∀ b ∈ Finset.univ, b ≠ i → (monomial (Finsupp.single b 1)) (1 i b) = 0
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>o : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Fintype o<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S<VAR>inst✝ : DecidableEq n<VAR>i : n<GOAL>i ∉ Finset.univ → (monomial (Finsupp.single i 1)) (1 i i) = 0
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>s t u v : Set α<VAR>inst✝¹ : ConnectedSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>hf : Surjective f<VAR>hf' : Continuous f<GOAL>ConnectedSpace β
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>s t u v : Set α<VAR>inst✝¹ : ConnectedSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>hf : Surjective f<VAR>hf' : Continuous f<GOAL>IsConnected (range f)
<VAR>p q : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Fact (Nat.Prime q)<VAR>hp : p % 4 = 1<VAR>hq : q ≠ 2<GOAL>legendreSym q ↑p = legendreSym p ↑q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>hf : ContinuousOn f s<VAR>hs : IsOpen s<GOAL>interior (s ∩ f ⁻¹' t) = s ∩ interior (f ⁻¹' t)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>inst✝ : LinearOrder α<VAR>s✝ s : Set α<GOAL>(s \ ⋃ x, Ioo ↑x.1 ↑x.2).Finite
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f : PartialHomeomorph E F<VAR>n : ℕ<VAR>x : E<VAR>hx : x ∈ f.source<GOAL>↑f x ∈ {y | ContDiffAt 𝕜 (↑n) (↑f.symm) y ∧ ContDiffAt 𝕜 (↑n) (↑f) (↑f.symm y)} ↔ x ∈ {x | ContDiffAt 𝕜 (↑n) (↑f) x ∧ ContDiffAt 𝕜 (↑n) (↑f.symm) (↑f x)}
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : NormedLinearOrderedField K<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace K E<VAR>b : Basis ι K E<VAR>inst✝¹ : FloorRing K<VAR>inst✝ : Fintype ι<VAR>x : E<GOAL>fract b x = x ↔ x ∈ fundamentalDomain b
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hab : a ∣ b<VAR>h : b / a = 1<GOAL>a = b
<VAR>R : Type uR<VAR>M : Type uM<VAR>K : Type uK<VAR>V : Type uV<VAR>ι : Type uι<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι R M<VAR>i : ι<VAR>x✝ : M<GOAL>(b.toDual (b i)) x✝ = (b.coord i) x✝
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : RCLike 𝕜<VAR>μ : Measure ℝ<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : CompleteSpace E<VAR>H : Type u_3<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>a b ε : ℝ<VAR>bound : ℝ → ℝ<VAR>F F' : 𝕜 → ℝ → E<VAR>x₀ : 𝕜<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>hF_int : IntervalIntegrable (F x₀) μ a b<VAR>hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b))<VAR>h_bound : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ∀ x ∈ ball x₀ ε, ‖F' x t‖ ≤ bound t<VAR>bound_integrable : IntervalIntegrable bound μ a b<VAR>h_diff : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ∀ x ∈ ball x₀ ε, HasDerivAt (fun x => F x t) (F' x t) x<GOAL>IntervalIntegrable (F' x₀) μ a b ∧ HasDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : RCLike 𝕜<VAR>μ : Measure ℝ<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : CompleteSpace E<VAR>H : Type u_3<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>a b ε : ℝ<VAR>bound : ℝ → ℝ<VAR>F F' : 𝕜 → ℝ → E<VAR>x₀ : 𝕜<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>hF_int : IntervalIntegrable (F x₀) μ a b<VAR>hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b))<VAR>h_bound : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ ball x₀ ε, ‖F' x_1 x‖ ≤ bound x<VAR>bound_integrable : IntervalIntegrable bound μ a b<VAR>h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ ball x₀ ε, HasDerivAt (fun x_2 => F x_2 x) (F' x_1 x) x_1<GOAL>IntervalIntegrable (F' x₀) μ a b ∧ HasDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : RCLike 𝕜<VAR>μ : Measure ℝ<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : CompleteSpace E<VAR>H : Type u_3<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>a b ε : ℝ<VAR>bound : ℝ → ℝ<VAR>F F' : 𝕜 → ℝ → E<VAR>x₀ : 𝕜<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b))<VAR>h_bound : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ ball x₀ ε, ‖F' x_1 x‖ ≤ bound x<VAR>h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ ball x₀ ε, HasDerivAt (fun x_2 => F x_2 x) (F' x_1 x) x_1<VAR>hF_int : IntegrableOn (F x₀) (Ι a b) μ<VAR>bound_integrable : IntegrableOn bound (Ι a b) μ<GOAL>IntegrableOn (F' x₀) (Ι a b) μ ∧ HasDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : RCLike 𝕜<VAR>μ : Measure ℝ<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : CompleteSpace E<VAR>H : Type u_3<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>a b ε : ℝ<VAR>bound : ℝ → ℝ<VAR>F F' : 𝕜 → ℝ → E<VAR>x₀ : 𝕜<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b))<VAR>h_bound : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ ball x₀ ε, ‖F' x_1 x‖ ≤ bound x<VAR>h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ ball x₀ ε, HasDerivAt (fun x_2 => F x_2 x) (F' x_1 x) x_1<VAR>hF_int : IntegrableOn (F x₀) (Ι a b) μ<VAR>bound_integrable : IntegrableOn bound (Ι a b) μ<GOAL>IntegrableOn (F' x₀) (Ι a b) μ ∧ HasDerivAt (fun x => (if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F x t ∂μ) ((if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F' x₀ t ∂μ) x₀
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : RCLike 𝕜<VAR>μ : Measure ℝ<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : CompleteSpace E<VAR>H : Type u_3<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>a b ε : ℝ<VAR>bound : ℝ → ℝ<VAR>F F' : 𝕜 → ℝ → E<VAR>x₀ : 𝕜<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b))<VAR>h_bound : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ ball x₀ ε, ‖F' x_1 x‖ ≤ bound x<VAR>h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ ball x₀ ε, HasDerivAt (fun x_2 => F x_2 x) (F' x_1 x) x_1<VAR>hF_int : IntegrableOn (F x₀) (Ι a b) μ<VAR>bound_integrable : IntegrableOn bound (Ι a b) μ<VAR>this : Integrable (F' x₀) (μ.restrict (Ι a b)) ∧ HasDerivAt (fun n => ∫ (a : ℝ) in Ι a b, F n a ∂μ) (∫ (a : ℝ) in Ι a b, F' x₀ a ∂μ) x₀<GOAL>IntegrableOn (F' x₀) (Ι a b) μ ∧ HasDerivAt (fun x => (if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F x t ∂μ) ((if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F' x₀ t ∂μ) x₀
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>s : Set M<VAR>m : M<GOAL>m ∈ ↑(span R s) ↔ m ∈ ⋃ n, (fun f => ∑ i : Fin n, (f i).1 • (f i).2) '' {f | ∀ (i : Fin n), (f i).2 ∈ s}
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>s : Set M<VAR>m : M<GOAL>(∃ n f g, ∑ i : Fin n, f i • ↑(g i) = m) ↔ ∃ i x, (∀ (i : Fin i), (x i).2 ∈ s) ∧ ∑ i : Fin i, (x i).1 • (x i).2 = m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>s : Set M<VAR>m : M<VAR>n : ℕ<GOAL>(∃ f g, ∑ i : Fin n, f i • ↑(g i) = m) → ∃ x, (∀ (i : Fin n), (x i).2 ∈ s) ∧ ∑ i : Fin n, (x i).1 • (x i).2 = m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>s : Set M<VAR>m : M<VAR>n : ℕ<GOAL>(∃ x, (∀ (i : Fin n), (x i).2 ∈ s) ∧ ∑ i : Fin n, (x i).1 • (x i).2 = m) → ∃ f g, ∑ i : Fin n, f i • ↑(g i) = m
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁵ : SMul R ℝ≥0<VAR>inst✝⁴ : SMul R ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_3<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 0)<VAR>f : Ω →ᵇ ℝ≥0<GOAL>Tendsto (fun i => (μs i).testAgainstNN f) F (𝓝 0)
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁵ : SMul R ℝ≥0<VAR>inst✝⁴ : SMul R ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_3<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 0)<VAR>f : Ω →ᵇ ℝ≥0<GOAL>Tendsto (fun b => dist ((μs b).testAgainstNN f) 0) F (𝓝 0)
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁵ : SMul R ℝ≥0<VAR>inst✝⁴ : SMul R ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_3<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 0)<VAR>f : Ω →ᵇ ℝ≥0<VAR>obs : ∀ (i : γ), (μs i).testAgainstNN f ≤ (μs i).testAgainstNN 0 + nndist f 0 * (μs i).mass<GOAL>Tendsto (fun b => dist ((μs b).testAgainstNN f) 0) F (𝓝 0)
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁵ : SMul R ℝ≥0<VAR>inst✝⁴ : SMul R ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_3<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 0)<VAR>f : Ω →ᵇ ℝ≥0<VAR>obs : ∀ (i : γ), (μs i).testAgainstNN f ≤ nndist f 0 * (μs i).mass<GOAL>Tendsto (fun b => dist ((μs b).testAgainstNN f) 0) F (𝓝 0)
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁵ : SMul R ℝ≥0<VAR>inst✝⁴ : SMul R ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_3<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 0)<VAR>f : Ω →ᵇ ℝ≥0<VAR>obs : ∀ (i : γ), (μs i).testAgainstNN f ≤ nndist f 0 * (μs i).mass<GOAL>Tendsto (fun b => ↑((μs b).testAgainstNN f)) F (𝓝 0)
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁵ : SMul R ℝ≥0<VAR>inst✝⁴ : SMul R ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_3<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 0)<VAR>f : Ω →ᵇ ℝ≥0<VAR>obs : ∀ (i : γ), (μs i).testAgainstNN f ≤ nndist f 0 * (μs i).mass<GOAL>Tendsto (fun t => (fun a => ↑a) (nndist f 0 * (μs t).mass)) F (𝓝 0)