ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : (i : ι) → Module R (M₁ i)<VAR>inst✝¹ : Module R M₂<VAR>f : MultilinearMap R M₁ M₂<VAR>inst✝ : LinearOrder ι<VAR>a b v : (i : ι) → M₁ i<VAR>s : Finset ι<GOAL>f (s.piecewise a v) - f (s.piecewise b v) = ∑ i ∈ s, f fun j => if j ∈ s then if j < i then a j else if j = i then a j - b j else b j else v j
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : (i : ι) → Module R (M₁ i)<VAR>inst✝¹ : Module R M₂<VAR>f : MultilinearMap R M₁ M₂<VAR>inst✝ : LinearOrder ι<VAR>a b v : (i : ι) → M₁ i<VAR>s : Finset ι<GOAL>(∑ i ∈ s, f fun j => if j ∈ s → j < i then s.piecewise a v j else if i = j then s.piecewise a v j - b j else b j) = ∑ i ∈ s, f fun j => if j ∈ s then if j < i then a j else if j = i then a j - b j else b j else v j
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : (i : ι) → Module R (M₁ i)<VAR>inst✝¹ : Module R M₂<VAR>f : MultilinearMap R M₁ M₂<VAR>inst✝ : LinearOrder ι<VAR>a b v : (i : ι) → M₁ i<VAR>s : Finset ι<VAR>i : ι<VAR>hi : i ∈ s<VAR>j : ι<GOAL>(if j ∈ s → j < i then s.piecewise a v j else if i = j then s.piecewise a v j - b j else b j) = if j ∈ s then if j < i then a j else if j = i then a j - b j else b j else v j
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝³ : Semiring S<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Field K<VAR>p : S[X]<VAR>f : S →+* A<VAR>a : A<VAR>s : S<VAR>hsa : Commute (f s) a<VAR>hf : ∀ (s₁ s₂ : S), Commute (f s₁) (f s₂)<GOAL>eval₂ f (f s * a) (p.scaleRoots s) = f s ^ p.natDegree * eval₂ f a p
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝¹ : ConditionallyCompleteLinearOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>f : Filtration ℕ m<VAR>i n : ι<VAR>ω : Ω<VAR>hx : ∃ j ≤ n, u j ω ∈ s<GOAL>hitting u s ⊥ n ω ≤ i ↔ ∃ j ≤ i, u j ω ∈ s
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝¹ : ConditionallyCompleteLinearOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>f : Filtration ℕ m<VAR>i n : ι<VAR>ω : Ω<VAR>hx : ∃ j ≤ n, u j ω ∈ s<VAR>hi : i < n<GOAL>hitting u s ⊥ n ω ≤ i ↔ ∃ j ≤ i, u j ω ∈ s
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝¹ : ConditionallyCompleteLinearOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>f : Filtration ℕ m<VAR>i n : ι<VAR>ω : Ω<VAR>hx : ∃ j ≤ n, u j ω ∈ s<VAR>hi : n ≤ i<GOAL>hitting u s ⊥ n ω ≤ i ↔ ∃ j ≤ i, u j ω ∈ s
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>a : R<GOAL>a ∈ ker f → f a = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>S : Submonoid R<GOAL>Subsingleton (LocalizedModule S M) ↔ ∀ (m : M), ∃ r ∈ S, r • m = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>h : IsLocalRingHom f<VAR>a : Sˣ<VAR>b : R<VAR>hb : f b = ↑a<GOAL>∃ a_1, (Units.map ↑f) a_1 = a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>h : IsLocalRingHom f<VAR>a : Sˣ<VAR>b : R<VAR>hb : f b = ↑a<GOAL>(Units.map ↑f) ⋯.unit = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>a b : α<VAR>ha : a ∉ s<VAR>hb : b ∈ s<GOAL>(insert a s \ {b}).encard = s.encard
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ✝ : Measure Ω<VAR>ℱ✝ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>s✝ : ℕ → Set Ω<VAR>ℱ : Filtration ℕ m0<VAR>μ : Measure Ω<VAR>s : ℕ → Set Ω<VAR>n : ℕ<GOAL>martingalePart (process s) ℱ μ n = ∑ k ∈ Finset.range n, ((s (k + 1)).indicator 1 - μ[(s (k + 1)).indicator 1|↑ℱ k])
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ✝ : Measure Ω<VAR>ℱ✝ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>s✝ : ℕ → Set Ω<VAR>ℱ : Filtration ℕ m0<VAR>μ : Measure Ω<VAR>s : ℕ → Set Ω<VAR>n : ℕ<GOAL>∑ i ∈ Finset.range n, (process s (i + 1) - process s i - μ[process s (i + 1) - process s i|↑ℱ i]) = ∑ k ∈ Finset.range n, ((s (k + 1)).indicator 1 - μ[(s (k + 1)).indicator 1|↑ℱ k])
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ✝ : Measure Ω<VAR>ℱ✝ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>s✝ : ℕ → Set Ω<VAR>ℱ : Filtration ℕ m0<VAR>μ : Measure Ω<VAR>s : ℕ → Set Ω<VAR>n k : ℕ<VAR>x✝ : k ∈ Finset.range n<GOAL>process s (k + 1) - process s k - μ[process s (k + 1) - process s k|↑ℱ k] = (s (k + 1)).indicator 1 - μ[(s (k + 1)).indicator 1|↑ℱ k]
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCancelCommMonoid G<VAR>x : k[G]<VAR>g : G<GOAL>x %ᵒᶠ g + of' k G g * (x /ᵒᶠ g) = x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedHeytingAlgebra α<VAR>a✝ b✝ c✝ d✝ a b c d : α<GOAL>d ≤ a ⇨ b ⊓ c ↔ d ≤ (a ⇨ b) ⊓ (a ⇨ c)
<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>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>x : H<GOAL>ContDiffWithinAtProp I I n id univ 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>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>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>x : H<GOAL>ContDiffWithinAt 𝕜 n (↑I ∘ ↑I.symm) (range ↑I) (↑I 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>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>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>x : H<VAR>this : ContDiffWithinAt 𝕜 n id (range ↑I) (↑I x)<GOAL>ContDiffWithinAt 𝕜 n (↑I ∘ ↑I.symm) (range ↑I) (↑I 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>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>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>x : H<VAR>this : ContDiffWithinAt 𝕜 n id (range ↑I) (↑I x)<VAR>y : E<VAR>hy : y ∈ range ↑I<GOAL>(↑I ∘ ↑I.symm) y = id y
<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>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>x : H<VAR>this : ContDiffWithinAt 𝕜 n id (range ↑I) (↑I x)<GOAL>(↑I ∘ ↑I.symm) (↑I x) = id (↑I x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : AddCommSemigroup α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<GOAL>a - b - c = a - c - b
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hI : M.Basis I X<VAR>hXY : X ⊆ Y<VAR>hY : autoParam (Y ⊆ M.E) _auto✝<GOAL>∃ J, M.Basis J Y ∧ J ∩ X = I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J✝ X Y : Set α<VAR>e : α<VAR>hI : M.Basis I X<VAR>hXY : X ⊆ Y<VAR>hY : autoParam (Y ⊆ M.E) _auto✝<VAR>J : Set α<VAR>hJ : M.Basis J Y<VAR>hIJ : I ⊆ J<GOAL>∃ J, M.Basis J Y ∧ J ∩ X = I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J✝ X Y : Set α<VAR>e : α<VAR>hI : M.Basis I X<VAR>hXY : X ⊆ Y<VAR>hY : autoParam (Y ⊆ M.E) _auto✝<VAR>J : Set α<VAR>hJ : M.Basis J Y<VAR>hIJ : I ⊆ J<GOAL>J ∩ X ⊆ I
<VAR>α✝ β✝ : Type u<VAR>a✝ : Cardinal.{u_1}<VAR>α : Type u_1<VAR>b✝ : Cardinal.{u_1}<VAR>β : Type u_1<VAR>c✝ : Cardinal.{u_1}<VAR>γ : Type u_1<VAR>hα : Quot.mk Setoid.r α ≠ 0<VAR>e : β ↪ γ<GOAL>Quot.mk Setoid.r α ^ Quot.mk Setoid.r β ≤ Quot.mk Setoid.r α ^ Quot.mk Setoid.r γ
<VAR>α✝ β✝ : Type u<VAR>a✝ : Cardinal.{u_1}<VAR>α : Type u_1<VAR>b✝ : Cardinal.{u_1}<VAR>β : Type u_1<VAR>c✝ : Cardinal.{u_1}<VAR>γ : Type u_1<VAR>hα : Quot.mk Setoid.r α ≠ 0<VAR>e : β ↪ γ<VAR>a : α<GOAL>Quot.mk Setoid.r α ^ Quot.mk Setoid.r β ≤ Quot.mk Setoid.r α ^ Quot.mk Setoid.r γ
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<GOAL>SigmaFinite (μ.trim ⋯) ↔ IsFiniteMeasure μ
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<GOAL>IsFiniteMeasure (μ.trim ⋯) ↔ IsFiniteMeasure μ
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<VAR>h : IsFiniteMeasure (μ.trim ⋯)<VAR>h_univ : (μ.trim ⋯) Set.univ < ⊤<GOAL>μ Set.univ < ⊤
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<VAR>h : IsFiniteMeasure μ<VAR>h_univ : μ Set.univ < ⊤<GOAL>(μ.trim ⋯) Set.univ < ⊤
<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 : G → E<VAR>s : Set G<VAR>x : G<VAR>f' : G →L[𝕜] E<GOAL>HasFDerivWithinAt (⇑iso ∘ f) ((↑iso).comp f') s x ↔ HasFDerivWithinAt f f' s x
<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 : G → E<VAR>s : Set G<VAR>x : G<VAR>f' : G →L[𝕜] E<VAR>H : HasFDerivWithinAt (⇑iso ∘ f) ((↑iso).comp f') s x<GOAL>HasFDerivWithinAt f f' s x
<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 : G → E<VAR>s : Set G<VAR>x : G<VAR>f' : G →L[𝕜] E<VAR>H : HasFDerivWithinAt (⇑iso ∘ f) ((↑iso).comp f') s x<VAR>A : f = ⇑iso.symm ∘ ⇑iso ∘ f<GOAL>HasFDerivWithinAt f f' s x
<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 : G → E<VAR>s : Set G<VAR>x : G<VAR>f' : G →L[𝕜] E<VAR>H : HasFDerivWithinAt (⇑iso ∘ f) ((↑iso).comp f') s x<VAR>A : f = ⇑iso.symm ∘ ⇑iso ∘ f<VAR>B : f' = (↑iso.symm).comp ((↑iso).comp f')<GOAL>HasFDerivWithinAt f f' s x
<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 : G → E<VAR>s : Set G<VAR>x : G<VAR>f' : G →L[𝕜] E<VAR>H : HasFDerivWithinAt (⇑iso ∘ f) ((↑iso).comp f') s x<VAR>A : f = ⇑iso.symm ∘ ⇑iso ∘ f<VAR>B : f' = (↑iso.symm).comp ((↑iso).comp f')<GOAL>HasFDerivWithinAt (⇑iso.symm ∘ ⇑iso ∘ f) ((↑iso.symm).comp ((↑iso).comp f')) s x
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p✝ q p : R[X]<VAR>a : R<VAR>hp0 : 0 < p.degree<VAR>h : p = 0<GOAL>False
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>(fun n => 1 / log n) =o[atTop] fun x => 1
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>Tendsto (fun x => 1 / log x / 1) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>Tendsto (fun x => (log x)⁻¹) atTop (𝓝 0)
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>V3 : Type u_6<VAR>P3 : Type u_7<VAR>V4 : Type u_8<VAR>P4 : Type u_9<VAR>inst✝¹² : Ring k<VAR>inst✝¹¹ : AddCommGroup V1<VAR>inst✝¹⁰ : Module k V1<VAR>inst✝⁹ : AffineSpace V1 P1<VAR>inst✝⁸ : AddCommGroup V2<VAR>inst✝⁷ : Module k V2<VAR>inst✝⁶ : AffineSpace V2 P2<VAR>inst✝⁵ : AddCommGroup V3<VAR>inst✝⁴ : Module k V3<VAR>inst✝³ : AffineSpace V3 P3<VAR>inst✝² : AddCommGroup V4<VAR>inst✝¹ : Module k V4<VAR>inst✝ : AffineSpace V4 P4<VAR>p₀ p₁ : P1<GOAL>(lineMap p₀ p₁) 0 = p₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>f✝ g : α → E<VAR>s✝ t : Set α<VAR>μ✝ ν : Measure α<VAR>inst✝ : MeasurableSpace β<VAR>e : α ≃ᵐ β<VAR>f : β → E<VAR>μ : Measure α<VAR>s : Set β<GOAL>IntegrableOn f s (Measure.map (⇑e) μ) ↔ IntegrableOn (f ∘ ⇑e) (⇑e ⁻¹' s) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : NoMinOrder α<VAR>inst✝ : DenselyOrdered α<VAR>a : α<VAR>s : Set α<GOAL>s ∈ 𝓝[<] a ↔ ∃ l ∈ Iio a, Ico l a ⊆ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : NoMinOrder α<VAR>inst✝ : DenselyOrdered α<VAR>a : α<VAR>s : Set α<VAR>this : ⇑ofDual ⁻¹' s ∈ 𝓝[>] toDual a ↔ ∃ u ∈ Ioi (toDual a), Ioc (toDual a) u ⊆ ⇑ofDual ⁻¹' s<GOAL>s ∈ 𝓝[<] a ↔ ∃ l ∈ Iio a, Ico l a ⊆ s
<VAR>z w : ℍ<VAR>r R a y₁ y₂ : ℝ<GOAL>dist (mk { re := a, im := rexp y₁ } ⋯) (mk { re := a, im := rexp y₂ } ⋯) = dist y₁ y₂
<VAR>z w : ℍ<VAR>r R a y₁ y₂ : ℝ<GOAL>dist (log (mk { re := a, im := rexp y₁ } ⋯).im) (log (mk { re := a, im := rexp y₂ } ⋯).im) = dist y₁ y₂
<VAR>z w : ℍ<VAR>r R a y₁ y₂ : ℝ<GOAL>(mk { re := a, im := rexp y₁ } ⋯).re = (mk { re := a, im := rexp y₂ } ⋯).re