ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>q r : ℚ<VAR>s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)<VAR>hs : ↑q.den * ↑r.den ≠ 0<VAR>c : ℤ<VAR>c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num<VAR>c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den<GOAL>↑q.den * ↑r.den * (q * r).num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑(q * r).den
<VAR>q r : ℚ<VAR>s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)<VAR>hs : ↑q.den * ↑r.den ≠ 0<VAR>c : ℤ<VAR>c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num<VAR>c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den<GOAL>c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den * (q * r).num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑(q * r).den
<VAR>q r : ℚ<VAR>s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)<VAR>hs : ↑q.den * ↑r.den ≠ 0<VAR>c : ℤ<VAR>c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num<VAR>c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den<GOAL>¬c = 0 → ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den * (q * r).num = (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑(q * r).den
<VAR>q r : ℚ<VAR>s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)<VAR>hs : ↑q.den * ↑r.den ≠ 0<VAR>c : ℤ<VAR>c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num<VAR>c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den<VAR>a✝ : ¬c = 0<GOAL>↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den * (q * r).num = (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑(q * r).den
<VAR>q r : ℚ<VAR>s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)<VAR>hs : ↑q.den * ↑r.den ≠ 0<VAR>c : ℤ<VAR>c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num<VAR>c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den<VAR>a✝ : ¬c = 0<VAR>h : q.num /. ↑q.den * (r.num /. ↑r.den) = s<GOAL>↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den * (q * r).num = (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑(q * r).den
<VAR>q r : ℚ<VAR>s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)<VAR>hs : ↑q.den * ↑r.den ≠ 0<VAR>c : ℤ<VAR>c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num<VAR>c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den<VAR>a✝ : ¬c = 0<VAR>h : q * r = s<GOAL>↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den * (q * r).num = (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑(q * r).den
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>S : Type u_4<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Fintype σ<VAR>inst✝¹ : Fintype τ<VAR>inst✝ : Algebra R S<VAR>f : σ → S<VAR>n : ℕ<GOAL>(aeval f) (esymm σ R n) = (Multiset.map f univ.val).esymm n
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁸ : Category.{u_4, u_1} C<VAR>inst✝¹⁷ : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>inst✝¹⁶ : HasShift C ℤ<VAR>inst✝¹⁵ : Preadditive C<VAR>inst✝¹⁴ : HasZeroObject C<VAR>inst✝¹³ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝¹² : Pretriangulated C<VAR>inst✝¹¹ : HasShift D ℤ<VAR>inst✝¹⁰ : L.CommShift ℤ<VAR>W : MorphismProperty C<VAR>inst✝⁹ : L.IsLocalization W<VAR>inst✝⁸ : W.IsCompatibleWithTriangulation<VAR>inst✝⁷ : W.HasLeftCalculusOfFractions<VAR>inst✝⁶ : Preadditive D<VAR>inst✝⁵ : HasZeroObject D<VAR>inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝³ : L.Additive<VAR>inst✝² : Pretriangulated D<VAR>inst✝¹ : L.IsTriangulated<VAR>inst✝ : IsTriangulated C<GOAL>IsTriangulated D
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁸ : Category.{u_4, u_1} C<VAR>inst✝¹⁷ : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>inst✝¹⁶ : HasShift C ℤ<VAR>inst✝¹⁵ : Preadditive C<VAR>inst✝¹⁴ : HasZeroObject C<VAR>inst✝¹³ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝¹² : Pretriangulated C<VAR>inst✝¹¹ : HasShift D ℤ<VAR>inst✝¹⁰ : L.CommShift ℤ<VAR>W : MorphismProperty C<VAR>inst✝⁹ : L.IsLocalization W<VAR>inst✝⁸ : W.IsCompatibleWithTriangulation<VAR>inst✝⁷ : W.HasLeftCalculusOfFractions<VAR>inst✝⁶ : Preadditive D<VAR>inst✝⁵ : HasZeroObject D<VAR>inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝³ : L.Additive<VAR>inst✝² : Pretriangulated D<VAR>inst✝¹ : L.IsTriangulated<VAR>inst✝ : IsTriangulated C<VAR>this : (L.mapComposableArrows 2).EssSurj<GOAL>IsTriangulated D
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : LieAlgebra.IsNilpotent R L<VAR>χ₁ χ₂ : L → R<VAR>p q : ℤ<VAR>this : ∀ (k : ℤ), k ∈ Ioo p q ↔ k ∈ Finset.Ioo p q<GOAL>weightSpaceChain M χ₁ χ₂ p q = ⨆ k ∈ Finset.Ioo p q, weightSpace M (k • χ₁ + χ₂)
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : BooleanAlgebra α<GOAL>x ⇨ y = x ↔ x = ⊤ ∧ y = ⊤
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : BooleanAlgebra α<GOAL>x ⇨ y = ⊤ ∧ x = ⊤ ↔ x = ⊤ ∧ y = ⊤
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>M₃ : Type u_5<VAR>M₄ : Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M₂<VAR>inst✝⁵ : AddCommGroup M₃<VAR>inst✝⁴ : AddCommGroup M₄<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Module R M₃<VAR>inst✝ : Module R M₄<VAR>r : R<VAR>rs : List R<GOAL>IsRegular M (r :: rs) ↔ IsSMulRegular M r ∧ IsRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>M₃ : Type u_5<VAR>M₄ : Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M₂<VAR>inst✝⁵ : AddCommGroup M₃<VAR>inst✝⁴ : AddCommGroup M₄<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Module R M₃<VAR>inst✝ : Module R M₄<VAR>r : R<VAR>rs : List R<GOAL>IsWeaklyRegular M (r :: rs) ∧ ¬⊤ = Ideal.ofList (r :: rs) • ⊤ ↔ IsSMulRegular M r ∧ IsWeaklyRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) ∧ ¬⊤ = Ideal.ofList (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) • ⊤
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u v w x y : V<VAR>p : G.Walk u v<VAR>hnp : ¬p.Nil<VAR>u✝ v✝ w✝ : V<VAR>x✝¹ : G.Adj u✝ v✝<VAR>x✝ : G.Walk v✝ w✝<GOAL>(cons x✝¹ x✝).getVert 1 = (cons x✝¹ x✝).sndOfNotNil ⋯
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroupWithZero α<VAR>a b c✝ d : α<VAR>m n : ℕ<VAR>c : α<VAR>h : a < b<VAR>hc : c ≠ 0<GOAL>a * c < b * c
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroupWithZero α<VAR>a b c✝ d : α<VAR>m n : ℕ<VAR>c : α<VAR>hc : c ≠ 0<VAR>h : b * c ≤ a * c<GOAL>b ≤ a
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>Y : D<GOAL>e.inverse.map (e.counitInv.app Y) ≫ e.unitInv.app (e.inverse.obj Y) = 𝟙 (e.inverse.obj Y)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>Y : D<GOAL>(e.unitIso.app (e.inverse.obj Y) ≪≫ e.inverse.mapIso (e.counitIso.app Y)).hom = (Iso.refl ((𝟭 C).obj (e.inverse.obj Y))).hom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H✝ : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : AddZeroClass M<VAR>inst✝ : AddZeroClass N<VAR>f g : (α →₀ M) →+ N<VAR>H : ∀ (x : α) (y : M), f (single x y) = g (single x y)<GOAL>f = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H✝ : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : AddZeroClass M<VAR>inst✝ : AddZeroClass N<VAR>f g : (α →₀ M) →+ N<VAR>H : ∀ (x : α) (y : M), f (single x y) = g (single x y)<GOAL>Set.EqOn ⇑f ⇑g {f | ∃ a b, f = single a b}
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h : a ≠ 0<GOAL>a / 0 = ⊤
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<GOAL>AEMeasurable f' (μ.restrict s)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>ε : ℝ<VAR>εpos : ε > 0<GOAL>∃ f, AEMeasurable f (μ.restrict s) ∧ ∀ᵐ (x : E) ∂μ.restrict s, dist (f x) (f' x) ≤ ε
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>δ : ℝ≥0 := ⟨ε, ⋯⟩<GOAL>∃ f, AEMeasurable f (μ.restrict s) ∧ ∀ᵐ (x : E) ∂μ.restrict s, dist (f x) (f' x) ≤ ε
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>δ : ℝ≥0 := ⟨ε, ⋯⟩<VAR>δpos : 0 < δ<GOAL>∃ f, AEMeasurable f (μ.restrict s) ∧ ∀ᵐ (x : E) ∂μ.restrict s, dist (f x) (f' x) ≤ ε
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>δ : ℝ≥0 := ⟨ε, ⋯⟩<VAR>δpos : 0 < δ<VAR>t : ℕ → Set E<VAR>A : ℕ → E →L[ℝ] E<VAR>t_disj : Pairwise (Disjoint on t)<VAR>t_meas : ∀ (n : ℕ), MeasurableSet (t n)<VAR>t_cover : s ⊆ ⋃ n, t n<VAR>ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ<VAR>right✝ : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y<GOAL>∃ f, AEMeasurable f (μ.restrict s) ∧ ∀ᵐ (x : E) ∂μ.restrict s, dist (f x) (f' x) ≤ ε
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>δ : ℝ≥0 := ⟨ε, ⋯⟩<VAR>δpos : 0 < δ<VAR>t : ℕ → Set E<VAR>A : ℕ → E →L[ℝ] E<VAR>t_disj : Pairwise (Disjoint on t)<VAR>t_meas : ∀ (n : ℕ), MeasurableSet (t n)<VAR>t_cover : s ⊆ ⋃ n, t n<VAR>ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ<VAR>right✝ : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y<VAR>g : E → E →L[ℝ] E<VAR>g_meas : Measurable g<VAR>hg : ∀ (n : ℕ), ∀ x ∈ t n, g x = A n<GOAL>∃ f, AEMeasurable f (μ.restrict s) ∧ ∀ᵐ (x : E) ∂μ.restrict s, dist (f x) (f' x) ≤ ε
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>δ : ℝ≥0 := ⟨ε, ⋯⟩<VAR>δpos : 0 < δ<VAR>t : ℕ → Set E<VAR>A : ℕ → E →L[ℝ] E<VAR>t_disj : Pairwise (Disjoint on t)<VAR>t_meas : ∀ (n : ℕ), MeasurableSet (t n)<VAR>t_cover : s ⊆ ⋃ n, t n<VAR>ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ<VAR>right✝ : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y<VAR>g : E → E →L[ℝ] E<VAR>g_meas : Measurable g<VAR>hg : ∀ (n : ℕ), ∀ x ∈ t n, g x = A n<GOAL>∀ᵐ (x : E) ∂μ.restrict s, dist (g x) (f' x) ≤ ε
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>δ : ℝ≥0 := ⟨ε, ⋯⟩<VAR>δpos : 0 < δ<VAR>t : ℕ → Set E<VAR>A : ℕ → E →L[ℝ] E<VAR>t_disj : Pairwise (Disjoint on t)<VAR>t_meas : ∀ (n : ℕ), MeasurableSet (t n)<VAR>t_cover : s ⊆ ⋃ n, t n<VAR>ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ<VAR>right✝ : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y<VAR>g : E → E →L[ℝ] E<VAR>g_meas : Measurable g<VAR>hg : ∀ (n : ℕ), ∀ x ∈ t n, g x = A n<GOAL>∀ᵐ (x : E) ∂sum fun n => μ.restrict (s ∩ t n), dist (g x) (f' x) ≤ ε
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>δ : ℝ≥0 := ⟨ε, ⋯⟩<VAR>δpos : 0 < δ<VAR>t : ℕ → Set E<VAR>A : ℕ → E →L[ℝ] E<VAR>t_disj : Pairwise (Disjoint on t)<VAR>t_meas : ∀ (n : ℕ), MeasurableSet (t n)<VAR>t_cover : s ⊆ ⋃ n, t n<VAR>ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ<VAR>right✝ : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y<VAR>g : E → E →L[ℝ] E<VAR>g_meas : Measurable g<VAR>hg : ∀ (n : ℕ), ∀ x ∈ t n, g x = A n<VAR>n : ℕ<GOAL>∀ᵐ (x : E) ∂μ.restrict (s ∩ t n), dist (g x) (f' x) ≤ ε
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>δ : ℝ≥0 := ⟨ε, ⋯⟩<VAR>δpos : 0 < δ<VAR>t : ℕ → Set E<VAR>A : ℕ → E →L[ℝ] E<VAR>t_disj : Pairwise (Disjoint on t)<VAR>t_meas : ∀ (n : ℕ), MeasurableSet (t n)<VAR>t_cover : s ⊆ ⋃ n, t n<VAR>ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ<VAR>right✝ : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y<VAR>g : E → E →L[ℝ] E<VAR>g_meas : Measurable g<VAR>hg : ∀ (n : ℕ), ∀ x ∈ t n, g x = A n<VAR>n : ℕ<VAR>E₁ : ∀ᵐ (x : E) ∂μ.restrict (s ∩ t n), ‖f' x - A n‖₊ ≤ δ<GOAL>∀ᵐ (x : E) ∂μ.restrict (s ∩ t n), dist (g x) (f' x) ≤ ε
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>δ : ℝ≥0 := ⟨ε, ⋯⟩<VAR>δpos : 0 < δ<VAR>t : ℕ → Set E<VAR>A : ℕ → E →L[ℝ] E<VAR>t_disj : Pairwise (Disjoint on t)<VAR>t_meas : ∀ (n : ℕ), MeasurableSet (t n)<VAR>t_cover : s ⊆ ⋃ n, t n<VAR>ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ<VAR>right✝ : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y<VAR>g : E → E →L[ℝ] E<VAR>g_meas : Measurable g<VAR>hg : ∀ (n : ℕ), ∀ x ∈ t n, g x = A n<VAR>n : ℕ<VAR>E₁ : ∀ᵐ (x : E) ∂μ.restrict (s ∩ t n), ‖f' x - A n‖₊ ≤ δ<VAR>E₂ : ∀ᵐ (x : E) ∂μ.restrict (s ∩ t n), g x = A n<GOAL>∀ᵐ (x : E) ∂μ.restrict (s ∩ t n), dist (g x) (f' x) ≤ ε
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>δ : ℝ≥0 := ⟨ε, ⋯⟩<VAR>δpos : 0 < δ<VAR>t : ℕ → Set E<VAR>A : ℕ → E →L[ℝ] E<VAR>t_disj : Pairwise (Disjoint on t)<VAR>t_meas : ∀ (n : ℕ), MeasurableSet (t n)<VAR>t_cover : s ⊆ ⋃ n, t n<VAR>ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ<VAR>right✝ : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y<VAR>g : E → E →L[ℝ] E<VAR>g_meas : Measurable g<VAR>hg : ∀ (n : ℕ), ∀ x ∈ t n, g x = A n<VAR>n : ℕ<VAR>E₁ : ∀ᵐ (x : E) ∂μ.restrict (s ∩ t n), ‖f' x - A n‖₊ ≤ δ<VAR>E₂ : ∀ᵐ (x : E) ∂μ.restrict (s ∩ t n), g x = A n<VAR>x : E<VAR>hx1 : ‖f' x - A n‖₊ ≤ δ<VAR>hx2 : g x = A n<GOAL>dist (g x) (f' x) ≤ ε
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>δ : ℝ≥0 := ⟨ε, ⋯⟩<VAR>δpos : 0 < δ<VAR>t : ℕ → Set E<VAR>A : ℕ → E →L[ℝ] E<VAR>t_disj : Pairwise (Disjoint on t)<VAR>t_meas : ∀ (n : ℕ), MeasurableSet (t n)<VAR>t_cover : s ⊆ ⋃ n, t n<VAR>ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ<VAR>right✝ : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y<VAR>g : E → E →L[ℝ] E<VAR>g_meas : Measurable g<VAR>hg : ∀ (n : ℕ), ∀ x ∈ t n, g x = A n<VAR>n : ℕ<VAR>E₁ : ∀ᵐ (x : E) ∂μ.restrict (s ∩ t n), ‖f' x - A n‖₊ ≤ δ<VAR>E₂ : ∀ᵐ (x : E) ∂μ.restrict (s ∩ t n), g x = A n<VAR>x : E<VAR>hx1 : nndist (f' x) (A n) ≤ δ<VAR>hx2 : g x = A n<GOAL>dist (g x) (f' x) ≤ ε
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>δ : ℝ≥0 := ⟨ε, ⋯⟩<VAR>δpos : 0 < δ<VAR>t : ℕ → Set E<VAR>A : ℕ → E →L[ℝ] E<VAR>t_disj : Pairwise (Disjoint on t)<VAR>t_meas : ∀ (n : ℕ), MeasurableSet (t n)<VAR>t_cover : s ⊆ ⋃ n, t n<VAR>ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ<VAR>right✝ : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y<VAR>g : E → E →L[ℝ] E<VAR>g_meas : Measurable g<VAR>hg : ∀ (n : ℕ), ∀ x ∈ t n, g x = A n<VAR>n : ℕ<VAR>E₁ : ∀ᵐ (x : E) ∂μ.restrict (s ∩ t n), ‖f' x - A n‖₊ ≤ δ<VAR>E₂ : ∀ᵐ (x : E) ∂μ.restrict (s ∩ t n), g x = A n<VAR>x : E<VAR>hx1 : nndist (f' x) (A n) ≤ δ<VAR>hx2 : g x = A n<GOAL>dist (f' x) (A n) ≤ ε
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionRing α<VAR>p q✝ q : ℚ<GOAL>↑(-q) = -↑q
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>p : R[X]<VAR>s : R<GOAL>(p.scaleRoots s).coeff p.natDegree = p.leadingCoeff
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Seq α<VAR>f g : Seq α → Seq β<VAR>H : ∀ (s : Seq α), BisimO (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct<GOAL>f s = g s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Seq α<VAR>f g : Seq α → Seq β<VAR>H : ∀ (s : Seq α), BisimO (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct<GOAL>IsBisimulation fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<GOAL>Measure.map (s.restrict f) (Measure.comap Subtype.val (μ.withDensity fun x => ENNReal.ofReal |(f' x).det|)) = μ.restrict (f '' s)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>u : E → E<VAR>u_meas : Measurable u<VAR>uf : EqOn u f s<GOAL>Measure.map (s.restrict f) (Measure.comap Subtype.val (μ.withDensity fun x => ENNReal.ofReal |(f' x).det|)) = μ.restrict (f '' s)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>u : E → E<VAR>u_meas : Measurable u<VAR>uf : EqOn u f s<VAR>u' : ∀ x ∈ s, HasFDerivWithinAt u (f' x) s x<GOAL>Measure.map (s.restrict f) (Measure.comap Subtype.val (μ.withDensity fun x => ENNReal.ofReal |(f' x).det|)) = μ.restrict (f '' s)
<VAR>E : Type u_1<VAR>F✝ : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F✝<VAR>inst✝³ : NormedSpace ℝ F✝<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>u : E → E<VAR>u_meas : Measurable u<VAR>uf : EqOn u f s<VAR>u' : ∀ x ∈ s, HasFDerivWithinAt u (f' x) s x<VAR>F : ↑s → E := u ∘ Subtype.val<VAR>hF : F = u ∘ Subtype.val<GOAL>Measure.map (s.restrict f) (Measure.comap Subtype.val (μ.withDensity fun x => ENNReal.ofReal |(f' x).det|)) = μ.restrict (f '' s)
<VAR>E : Type u_1<VAR>F✝ : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F✝<VAR>inst✝³ : NormedSpace ℝ F✝<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>u : E → E<VAR>u_meas : Measurable u<VAR>uf : EqOn u f s<VAR>u' : ∀ x ∈ s, HasFDerivWithinAt u (f' x) s x<VAR>F : ↑s → E := u ∘ Subtype.val<VAR>hF : F = u ∘ Subtype.val<VAR>A : Measure.map F (Measure.comap Subtype.val (μ.withDensity fun x => ENNReal.ofReal |(f' x).det|)) = μ.restrict (u '' s)<GOAL>Measure.map (s.restrict f) (Measure.comap Subtype.val (μ.withDensity fun x => ENNReal.ofReal |(f' x).det|)) = μ.restrict (f '' s)