ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>x y : ℝ<VAR>s s' : Set ℝ<VAR>hs'_unique : UniqueDiffWithinAt ℝ s' y<VAR>hs_unique : UniqueDiffOn ℝ s<VAR>hs' : s' ∈ 𝓝[s] y<VAR>hy : y ∈ s'<VAR>h : s' ⊆ s<VAR>k : ℕ<VAR>hk : ContDiffOn ℝ (↑k) f s → DifferentiableWithinAt ℝ (iteratedDerivWithin k f s) s y → HasDerivWithinAt (fun t => taylorWithinEval f k s t x) (((↑k !)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y) s' y<VAR>hf : ContDiffOn ℝ (↑(k + 1)) f s<VAR>hf' : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y<VAR>coe_lt_succ : ↑k < ↑k.succ<GOAL>HasDerivWithinAt (fun t => taylorWithinEval f k s t x + (((↑k + 1) * ↑k !)⁻¹ * (x - t) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s t) ((((↑k + 1) * ↑k !)⁻¹ * (x - y) ^ k.succ) • iteratedDerivWithin k.succ.succ f s y) s' y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>x y : ℝ<VAR>s s' : Set ℝ<VAR>hs'_unique : UniqueDiffWithinAt ℝ s' y<VAR>hs_unique : UniqueDiffOn ℝ s<VAR>hs' : s' ∈ 𝓝[s] y<VAR>hy : y ∈ s'<VAR>h : s' ⊆ s<VAR>k : ℕ<VAR>hk : ContDiffOn ℝ (↑k) f s → DifferentiableWithinAt ℝ (iteratedDerivWithin k f s) s y → HasDerivWithinAt (fun t => taylorWithinEval f k s t x) (((↑k !)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y) s' y<VAR>hf : ContDiffOn ℝ (↑(k + 1)) f s<VAR>hf' : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y<VAR>coe_lt_succ : ↑k < ↑k.succ<VAR>hdiff : DifferentiableOn ℝ (iteratedDerivWithin k f s) s'<GOAL>HasDerivWithinAt (fun t => taylorWithinEval f k s t x + (((↑k + 1) * ↑k !)⁻¹ * (x - t) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s t) ((((↑k + 1) * ↑k !)⁻¹ * (x - y) ^ k.succ) • iteratedDerivWithin k.succ.succ f s y) s' y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>x y : ℝ<VAR>s s' : Set ℝ<VAR>hs'_unique : UniqueDiffWithinAt ℝ s' y<VAR>hs_unique : UniqueDiffOn ℝ s<VAR>hs' : s' ∈ 𝓝[s] y<VAR>hy : y ∈ s'<VAR>h : s' ⊆ s<VAR>k : ℕ<VAR>hf : ContDiffOn ℝ (↑(k + 1)) f s<VAR>hf' : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y<VAR>coe_lt_succ : ↑k < ↑k.succ<VAR>hdiff : DifferentiableOn ℝ (iteratedDerivWithin k f s) s'<VAR>hk : HasDerivWithinAt (fun t => taylorWithinEval f k s t x) (((↑k !)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y) s' y<GOAL>HasDerivWithinAt (fun t => taylorWithinEval f k s t x + (((↑k + 1) * ↑k !)⁻¹ * (x - t) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s t) ((((↑k + 1) * ↑k !)⁻¹ * (x - y) ^ k.succ) • iteratedDerivWithin k.succ.succ f s y) s' y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>x y : ℝ<VAR>s s' : Set ℝ<VAR>hs'_unique : UniqueDiffWithinAt ℝ s' y<VAR>hs_unique : UniqueDiffOn ℝ s<VAR>hs' : s' ∈ 𝓝[s] y<VAR>hy : y ∈ s'<VAR>h : s' ⊆ s<VAR>k : ℕ<VAR>hf : ContDiffOn ℝ (↑(k + 1)) f s<VAR>hf' : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y<VAR>coe_lt_succ : ↑k < ↑k.succ<VAR>hdiff : DifferentiableOn ℝ (iteratedDerivWithin k f s) s'<VAR>hk : HasDerivWithinAt (fun t => taylorWithinEval f k s t x) (((↑k !)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y) s' y<GOAL>(((↑k + 1) * ↑k !)⁻¹ * (x - y) ^ k.succ) • iteratedDerivWithin k.succ.succ f s y = ((↑k !)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y + ((((↑k + 1) * ↑k !)⁻¹ * (x - y) ^ (k + 1)) • iteratedDerivWithin (k + 2) f s y - ((↑k !)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>minAx : MinimalAxioms α<VAR>s : Set α<VAR>a✝ b : α<VAR>f : ι → α<VAR>a : α<GOAL>(⨅ i, f i) ⊔ a = ⨅ i, f i ⊔ a
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k✝ : ℕ<VAR>f✝ : R[X]<VAR>k : ℕ<VAR>ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]<VAR>f : R[X]<VAR>n : ℕ<GOAL>(((k + 1)! • hasseDeriv (k + 1)) f).coeff n = ((⇑derivative)^[k + 1] f).coeff n
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k✝ : ℕ<VAR>f✝ : R[X]<VAR>k : ℕ<VAR>ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]<VAR>f : R[X]<VAR>n : ℕ<GOAL>(((k + 1)! • hasseDeriv (k + 1)) f).coeff n = (derivative ((k ! • hasseDeriv k) f)).coeff n
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k✝ : ℕ<VAR>f✝ : R[X]<VAR>k : ℕ<VAR>ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]<VAR>f : R[X]<VAR>n : ℕ<GOAL>(k + 1)! • (↑((n + (k + 1)).choose (k + 1)) * f.coeff (n + (k + 1))) = k ! • (↑((n + 1 + k).choose (n + 1)) * f.coeff (n + 1 + k) * (↑n + 1))
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k✝ : ℕ<VAR>f✝ : R[X]<VAR>k : ℕ<VAR>ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]<VAR>f : R[X]<VAR>n : ℕ<GOAL>↑((k + 1) * k !) * (↑((n + k + 1).choose (k + 1)) * f.coeff (n + k + 1)) = ↑k ! * (↑((n + k + 1).choose (n + 1)) * (f.coeff (n + k + 1) * ↑(n + 1)))
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k✝ : ℕ<VAR>f✝ : R[X]<VAR>k : ℕ<VAR>ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]<VAR>f : R[X]<VAR>n : ℕ<GOAL>↑((k + 1) * k !) * (↑((n + k + 1).choose (k + 1)) * f.coeff (n + k + 1)) = ↑k ! * (↑((n + k + 1).choose (n + 1)) * (↑(n + 1) * f.coeff (n + k + 1)))
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k✝ : ℕ<VAR>f✝ : R[X]<VAR>k : ℕ<VAR>ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]<VAR>f : R[X]<VAR>n : ℕ<GOAL>↑((k + 1) * k !) * ↑((n + k + 1).choose (k + 1)) * f.coeff (n + k + 1) = ↑k ! * ↑((n + k + 1).choose (n + 1)) * ↑(n + 1) * f.coeff (n + k + 1)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k✝ : ℕ<VAR>f✝ : R[X]<VAR>k : ℕ<VAR>ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]<VAR>f : R[X]<VAR>n : ℕ<GOAL>(k + 1) * k ! * (n + k + 1).choose (k + 1) = k ! * (n + k + 1).choose (n + 1) * (n + 1)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k✝ : ℕ<VAR>f✝ : R[X]<VAR>k : ℕ<VAR>ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]<VAR>f : R[X]<VAR>n : ℕ<GOAL>k ! * ((k + 1) * (n + k + 1).choose (k + 1)) = k ! * ((n + k + 1).choose (n + 1) * (n + 1))
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k✝ : ℕ<VAR>f✝ : R[X]<VAR>k : ℕ<VAR>ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]<VAR>f : R[X]<VAR>n : ℕ<GOAL>(k + 1) * (n + k + 1).choose (k + 1) = (n + k + 1).choose (n + 1) * (n + 1)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k✝ : ℕ<VAR>f✝ : R[X]<VAR>k : ℕ<VAR>ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]<VAR>f : R[X]<VAR>n : ℕ<VAR>this : n + k + 1 = n + (k + 1)<GOAL>(k + 1) * (n + k + 1).choose (k + 1) = (n + k + 1).choose (n + 1) * (n + 1)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k✝ : ℕ<VAR>f✝ : R[X]<VAR>k : ℕ<VAR>ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]<VAR>f : R[X]<VAR>n : ℕ<VAR>this : n + k + 1 = n + (k + 1)<GOAL>(n + k + 1).choose n * (k + 1) = (n + k + 1).choose n * (n + k + 1 - n)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k✝ : ℕ<VAR>f✝ : R[X]<VAR>k : ℕ<VAR>ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]<VAR>f : R[X]<VAR>n : ℕ<VAR>this : n + k + 1 = n + (k + 1)<GOAL>k + 1 = n + k + 1 - n
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>i j : ι<VAR>inst✝³ : K.HasHomology i<VAR>inst✝² : K.HasHomology j<VAR>inst✝¹ : L.HasHomology i<VAR>inst✝ : L.HasHomology j<GOAL>K.homologyι i ≫ K.opcyclesToCycles i j = 0
<VAR>R✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>ι : Type u_3<VAR>inst✝ : DecidableEq ι<VAR>n : ℕ<VAR>φ : R⟦X⟧<GOAL>(coeff R 1) (φ ^ n) = ↑n * (coeff R 1) φ * (constantCoeff R) φ ^ (n - 1)
<VAR>R✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>ι : Type u_3<VAR>inst✝ : DecidableEq ι<VAR>φ : R⟦X⟧<GOAL>(coeff R 1) (φ ^ 0) = ↑0 * (coeff R 1) φ * (constantCoeff R) φ ^ (0 - 1)
<VAR>R✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>ι : Type u_3<VAR>inst✝ : DecidableEq ι<VAR>n : ℕ<VAR>φ : R⟦X⟧<VAR>hn : n > 0<GOAL>(coeff R 1) (φ ^ n) = ↑n * (coeff R 1) φ * (constantCoeff R) φ ^ (n - 1)
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<GOAL>l.rotate' (l.length * (n + 1)) = (l.rotate' (l.length * n)).rotate' (l.rotate' (l.length * n)).length
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<GOAL>(l.rotate' (l.length * n)).rotate' (l.rotate' (l.length * n)).length = l
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K V : Set G<VAR>hK : IsCompact K<VAR>hV : (interior V).Nonempty<GOAL>∃ n, n ∈ Finset.card '' {t | K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K V : Set G<VAR>hK : IsCompact K<VAR>hV : (interior V).Nonempty<VAR>t : Finset G<VAR>ht : K ⊆ ⋃ g ∈ t, (fun x => g * x) ⁻¹' V<GOAL>∃ n, n ∈ Finset.card '' {t | K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f✝ g : α → β<VAR>μ ν : Measure α<VAR>f : α → δ<VAR>hf : AEMeasurable f μ<VAR>s : Set δ<VAR>hs : MeasurableSet s<GOAL>map f μ = map (AEMeasurable.mk f hf) μ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f✝ g : α → β<VAR>μ ν : Measure α<VAR>f : α → δ<VAR>hf : AEMeasurable f μ<VAR>s : Set δ<VAR>hs : MeasurableSet s<VAR>t : Set α<VAR>ht : MeasurableSet t<GOAL>(μ.restrict (AEMeasurable.mk f hf ⁻¹' s)) t = (μ.restrict (f ⁻¹' s)) t
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f✝ g : α → β<VAR>μ ν : Measure α<VAR>f : α → δ<VAR>hf : AEMeasurable f μ<VAR>s : Set δ<VAR>hs : MeasurableSet s<VAR>t : Set α<VAR>ht : MeasurableSet t<GOAL>μ (t ∩ AEMeasurable.mk f hf ⁻¹' s) = μ (t ∩ f ⁻¹' s)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f✝ g : α → β<VAR>μ ν : Measure α<VAR>f : α → δ<VAR>hf : AEMeasurable f μ<VAR>s : Set δ<VAR>hs : MeasurableSet s<VAR>t : Set α<VAR>ht : MeasurableSet t<GOAL>t ∩ AEMeasurable.mk f hf ⁻¹' s =ᶠ[ae μ] t ∩ f ⁻¹' s
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p✝ p₀✝ p₁ p₂ p₀ p : P<GOAL>InnerProductGeometry.angle (p₀ -ᵥ p₀) (p -ᵥ p₀) = π / 2
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p✝ p₀✝ p₁ p₂ p₀ p : P<GOAL>InnerProductGeometry.angle 0 (p -ᵥ p₀) = π / 2
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>D : ℝ<VAR>Dpos : 0 < D<GOAL>support (w D) = ball 0 D
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>D : ℝ<VAR>Dpos : 0 < D<VAR>B : D • ball 0 1 = ball 0 D<GOAL>support (w D) = ball 0 D
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>D : ℝ<VAR>Dpos : 0 < D<VAR>B : D • ball 0 1 = ball 0 D<VAR>C : D ^ finrank ℝ E ≠ 0<GOAL>support (w D) = ball 0 D
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : DecidableEq β<VAR>b : β<VAR>a : α<GOAL>HasProd (Pi.mulSingle b a) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : DecidableEq β<VAR>b : β<VAR>a : α<VAR>x✝ : β<GOAL>Pi.mulSingle b a x✝ = if x✝ = b then a else 1
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m✝ : σ<VAR>s : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p✝ q✝ : MvPolynomial σ R<VAR>inst✝ : DecidableEq σ<VAR>p q : MvPolynomial σ R<VAR>m : σ →₀ ℕ<VAR>hm : m ∈ p.support \ q.support<GOAL>m ∈ (p + q).support
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m✝ : σ<VAR>s : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p✝ q✝ : MvPolynomial σ R<VAR>inst✝ : DecidableEq σ<VAR>p q : MvPolynomial σ R<VAR>m : σ →₀ ℕ<VAR>hm : ¬coeff m p = 0 ∧ coeff m q = 0<GOAL>m ∈ (p + q).support
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Category.{?u.133484, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝ : L.IsLocalization W<VAR>X Y : C<VAR>z₁ z₂ : W.LeftFraction X Y<VAR>Z : C<VAR>t₁ : z₁.Y' ⟶ Z<VAR>t₂ : z₂.Y' ⟶ Z<VAR>hs : z₁.s ≫ t₁ = z₂.s ≫ t₂<VAR>hf : z₁.f ≫ t₁ = z₂.f ≫ t₂<VAR>ht : W (z₁.s ≫ t₁)<GOAL>RightFractionRel z₁.op z₂.op
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>a : α<VAR>g : G<GOAL>g⁻¹ • a ∈ fixedBy α g ↔ a ∈ fixedBy α g
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>κ : Type u_7<VAR>inst✝¹ : TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>f : X → (i : ι) → π i<VAR>inst✝ : DecidableEq ι<VAR>s : Set ((a : ι) → π a)<VAR>x : (a : ι) → π a<VAR>hs : s ∈ 𝓝 x<VAR>y : (a : ι) → π a<GOAL>∃ I, I.piecewise x y ∈ s
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>κ : Type u_7<VAR>inst✝¹ : TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>f : X → (i : ι) → π i<VAR>inst✝ : DecidableEq ι<VAR>s : Set ((a : ι) → π a)<VAR>x y : (a : ι) → π a<VAR>hs : ∃ I t, (∀ (i : ι), t i ∈ 𝓝 (x i)) ∧ (↑I).pi t ⊆ s<GOAL>∃ I, I.piecewise x y ∈ s
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>κ : Type u_7<VAR>inst✝¹ : TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>f : X → (i : ι) → π i<VAR>inst✝ : DecidableEq ι<VAR>s : Set ((a : ι) → π a)<VAR>x y : (a : ι) → π a<VAR>I : Finset ι<VAR>t : (i : ι) → Set (π i)<VAR>htx : ∀ (i : ι), t i ∈ 𝓝 (x i)<VAR>hts : (↑I).pi t ⊆ s<VAR>i : ι<VAR>hi : i ∈ ↑I<GOAL>I.piecewise x y i ∈ t i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>U : Set E<VAR>hU : U ∈ 𝓝 0<GOAL>balancedCore 𝕜 U ∈ 𝓝 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>U : Set E<VAR>hU : U ∈ 𝓝 0<VAR>r : ℝ<VAR>V : Set E<VAR>hr : 0 < r<VAR>hV : V ∈ 𝓝 0<VAR>hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U<GOAL>balancedCore 𝕜 U ∈ 𝓝 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>U : Set E<VAR>hU : U ∈ 𝓝 0<VAR>r : ℝ<VAR>V : Set E<VAR>hr : 0 < r<VAR>hV : V ∈ 𝓝 0<VAR>hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U<VAR>y : 𝕜<VAR>hy₀ : 0 < ‖y‖<VAR>hyr : ‖y‖ < r<GOAL>balancedCore 𝕜 U ∈ 𝓝 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>U : Set E<VAR>hU : U ∈ 𝓝 0<VAR>r : ℝ<VAR>V : Set E<VAR>hr : 0 < r<VAR>hV : V ∈ 𝓝 0<VAR>hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U<VAR>y : 𝕜<VAR>hy₀ : y ≠ 0<VAR>hyr : ‖y‖ < r<GOAL>balancedCore 𝕜 U ∈ 𝓝 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>U : Set E<VAR>hU : U ∈ 𝓝 0<VAR>r : ℝ<VAR>V : Set E<VAR>hr : 0 < r<VAR>hV : V ∈ 𝓝 0<VAR>hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U<VAR>y : 𝕜<VAR>hy₀ : y ≠ 0<VAR>hyr : ‖y‖ < r<VAR>this : y • V ∈ 𝓝 0<GOAL>balancedCore 𝕜 U ∈ 𝓝 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>U : Set E<VAR>hU : U ∈ 𝓝 0<VAR>r : ℝ<VAR>V : Set E<VAR>hr : 0 < r<VAR>hV : V ∈ 𝓝 0<VAR>hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U<VAR>y : 𝕜<VAR>hy₀ : y ≠ 0<VAR>hyr : ‖y‖ < r<VAR>this : y • V ∈ 𝓝 0<VAR>a : 𝕜<VAR>ha : ‖a‖ ≤ 1<GOAL>a • y • V ⊆ U
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>U : Set E<VAR>hU : U ∈ 𝓝 0<VAR>r : ℝ<VAR>V : Set E<VAR>hr : 0 < r<VAR>hV : V ∈ 𝓝 0<VAR>hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U<VAR>y : 𝕜<VAR>hy₀ : y ≠ 0<VAR>hyr : ‖y‖ < r<VAR>this : y • V ∈ 𝓝 0<VAR>a : 𝕜<VAR>ha : ‖a‖ ≤ 1<GOAL>(a * y) • V ⊆ U
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>U : Set E<VAR>hU : U ∈ 𝓝 0<VAR>r : ℝ<VAR>V : Set E<VAR>hr : 0 < r<VAR>hV : V ∈ 𝓝 0<VAR>hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U<VAR>y : 𝕜<VAR>hy₀ : y ≠ 0<VAR>hyr : ‖y‖ < r<VAR>this : y • V ∈ 𝓝 0<VAR>a : 𝕜<VAR>ha : ‖a‖ ≤ 1<VAR>z : E<VAR>hz : z ∈ V<GOAL>‖a * y‖ < r
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>U : Set E<VAR>hU : U ∈ 𝓝 0<VAR>r : ℝ<VAR>V : Set E<VAR>hr : 0 < r<VAR>hV : V ∈ 𝓝 0<VAR>hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U<VAR>y : 𝕜<VAR>hy₀ : y ≠ 0<VAR>hyr : ‖y‖ < r<VAR>this : y • V ∈ 𝓝 0<VAR>a : 𝕜<VAR>ha : ‖a‖ ≤ 1<VAR>z : E<VAR>hz : z ∈ V<GOAL>‖a‖ * ‖y‖ < 1 * r
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : TopCat<VAR>F : Presheaf C X<VAR>ι : Type w<VAR>U : ι → Opens ↑X<VAR>Y : Opens ↑X<VAR>hY : Y = iSup U<VAR>j : (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)ᵒᵖ<GOAL>F.map (eqToHom ⋯) ≫ (Functor.mapCone F (Sieve.generate (presieveOfCoveringAux U Y)).arrows.cocone.op).π.app j = (Cone.whisker (generateEquivalenceOpensLe U hY).op.functor (Functor.mapCone F (opensLeCoverCocone U).op)).π.app j
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : TopCat<VAR>F : Presheaf C X<VAR>ι : Type w<VAR>U : ι → Opens ↑X<VAR>Y : Opens ↑X<VAR>hY : Y = iSup U<VAR>j : (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)ᵒᵖ<GOAL>F.map (eqToHom ⋯ ≫ (Sieve.generate (presieveOfCoveringAux U Y)).arrows.cocone.op.π.app j) = (Cone.whisker (generateEquivalenceOpensLe U hY).op.functor (Functor.mapCone F (opensLeCoverCocone U).op)).π.app j
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : TopCat<VAR>F : Presheaf C X<VAR>ι : Type w<VAR>U : ι → Opens ↑X<VAR>Y : Opens ↑X<VAR>hY : Y = iSup U<VAR>j : (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)ᵒᵖ<GOAL>F.map (eqToHom ⋯) ≫ (Cone.whisker (generateEquivalenceOpensLe U hY).op.functor (Functor.mapCone F (opensLeCoverCocone U).op)).π.app j = (Functor.mapCone F (Sieve.generate (presieveOfCoveringAux U Y)).arrows.cocone.op).π.app j
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : TopCat<VAR>F : Presheaf C X<VAR>ι : Type w<VAR>U : ι → Opens ↑X<VAR>Y : Opens ↑X<VAR>hY : Y = iSup U<VAR>j : (FullSubcategory fun f => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)ᵒᵖ<GOAL>F.map (eqToHom ⋯ ≫ (opensLeCoverCocone U).op.π.app ((generateEquivalenceOpensLe U hY).op.functor.obj j)) = (Functor.mapCone F (Sieve.generate (presieveOfCoveringAux U Y)).arrows.cocone.op).π.app j
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : TopCat<VAR>F : Presheaf C X<VAR>ι : Type w<VAR>U : ι → Opens ↑X<VAR>Y : Opens ↑X<VAR>hY : Y = iSup U<GOAL>({ hom := F.map (eqToHom ⋯), w := ⋯ } ≫ { hom := F.map (eqToHom ⋯), w := ⋯ }).hom = (𝟙 (Cone.whisker (generateEquivalenceOpensLe U hY).op.functor (Functor.mapCone F (opensLeCoverCocone U).op))).hom
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : TopCat<VAR>F : Presheaf C X<VAR>ι : Type w<VAR>U : ι → Opens ↑X<VAR>Y : Opens ↑X<VAR>hY : Y = iSup U<GOAL>({ hom := F.map (eqToHom ⋯), w := ⋯ } ≫ { hom := F.map (eqToHom ⋯), w := ⋯ }).hom = (𝟙 (Functor.mapCone F (Sieve.generate (presieveOfCoveringAux U Y)).arrows.cocone.op)).hom
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hf : QuotientMap f<GOAL>Continuous g ↔ Continuous (g ∘ f)
<VAR>c d a b : Nat<VAR>cop : c.Coprime d<VAR>h : a * b = c * d<GOAL>a.gcd c * b.gcd c = c
<VAR>c d a b : Nat<VAR>cop : c.Coprime d<VAR>h : a * b = c * d<GOAL>a.gcd c * b.gcd c ∣ c
<VAR>c d a b : Nat<VAR>cop : c.Coprime d<VAR>h : a * b = c * d<GOAL>c ∣ a.gcd c * b.gcd c
<VAR>n p : ℕ<VAR>L : List ℕ<VAR>h_nonempty : L ≠ []<VAR>h_ne_zero : L.getLast h_nonempty ≠ 0<VAR>h_lt : ∀ l ∈ L, l < p<GOAL>(p - 1) * ∑ i ∈ range L.length, ofDigits p L / p ^ i.succ = ofDigits p L - L.sum
<VAR>n p : ℕ<VAR>L : List ℕ<VAR>h_nonempty : L ≠ []<VAR>h_ne_zero : L.getLast h_nonempty ≠ 0<VAR>h_lt : ∀ l ∈ L, l < p<VAR>h : 1 < p<GOAL>(p - 1) * ∑ i ∈ range L.length, ofDigits p L / p ^ i.succ = ofDigits p L - L.sum
<VAR>n : ℕ<VAR>L : List ℕ<VAR>h_nonempty : L ≠ []<VAR>h_ne_zero : L.getLast h_nonempty ≠ 0<VAR>h_lt : ∀ l ∈ L, l < 1<GOAL>(1 - 1) * ∑ i ∈ range L.length, ofDigits 1 L / 1 ^ i.succ = ofDigits 1 L - L.sum
<VAR>n p : ℕ<VAR>L : List ℕ<VAR>h_nonempty : L ≠ []<VAR>h_ne_zero : L.getLast h_nonempty ≠ 0<VAR>h_lt : ∀ l ∈ L, l < p<VAR>h : p < 1<GOAL>(p - 1) * ∑ i ∈ range L.length, ofDigits p L / p ^ i.succ = ofDigits p L - L.sum
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : Group α<VAR>s t : Finset α<VAR>a b : α<GOAL>preimage 1 (fun x => a⁻¹ * x) ⋯ = {a}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝⁴ : NormedAddCommGroup E'<VAR>inst✝³ : NormedSpace 𝕜 E'<VAR>inst✝² : TopologicalSpace H'<VAR>inst✝¹ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s✝ t : Set M<VAR>X : Type u_8<VAR>inst✝ : TopologicalSpace X<VAR>g : M → X<VAR>s : Set M<VAR>x : M<GOAL>ContinuousWithinAt (g ∘ ↑(f.extend I).symm) (↑(f.extend I).symm ⁻¹' s ∩ range ↑I) (↑(f.extend I) x) ↔ ContinuousWithinAt (g ∘ ↑f.symm) (↑f.symm ⁻¹' s) (↑f x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝⁴ : NormedAddCommGroup E'<VAR>inst✝³ : NormedSpace 𝕜 E'<VAR>inst✝² : TopologicalSpace H'<VAR>inst✝¹ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s✝ t : Set M<VAR>X : Type u_8<VAR>inst✝ : TopologicalSpace X<VAR>g : M → X<VAR>s : Set M<VAR>x : M<GOAL>ContinuousWithinAt (g ∘ ↑(f.extend I).symm) (↑(f.extend I).symm ⁻¹' s ∩ range ↑I) (↑(f.extend I) x) ↔ ContinuousWithinAt ((g ∘ ↑f.symm) ∘ ↑I.symm) (↑I.symm ⁻¹' (↑f.symm ⁻¹' s) ∩ range ↑I) (↑I (↑f x))