ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>h's : μ s ≠ ⊤<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>this : Tendsto (fun ε => ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ + 2 * ↑ε * μ s) (𝓝[>] 0) (𝓝 (∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ))<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<GOAL>μ (f '' s) ≤ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ + 2 * ↑ε * μ s
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<GOAL>Set.range (eval C) = Set.range (Sum.elim (fun l => Products.eval C ↑l) fun l => Products.eval C ↑l)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>H : Type u_3<VAR>inst✝¹¹ : TopologicalSpace H<VAR>E : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>inst✝⁸ : CommMonoid G<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : ChartedSpace H G<VAR>inst✝⁵ : SmoothMul I G<VAR>E' : Type u_6<VAR>inst✝⁴ : NormedAddCommGroup E'<VAR>inst✝³ : NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>inst✝² : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H' M<VAR>s : Set M<VAR>x x₀ : M<VAR>t : Finset ι<VAR>f : ι → M → G<VAR>n : ℕ∞<VAR>p : ι → Prop<VAR>h : ∀ i ∈ t, ContMDiffAt I' I n (f i) x₀<GOAL>ContMDiffAt I' I n (fun x => ∏ i ∈ t, f i x) x₀
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>H : Type u_3<VAR>inst✝¹¹ : TopologicalSpace H<VAR>E : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>inst✝⁸ : CommMonoid G<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : ChartedSpace H G<VAR>inst✝⁵ : SmoothMul I G<VAR>E' : Type u_6<VAR>inst✝⁴ : NormedAddCommGroup E'<VAR>inst✝³ : NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>inst✝² : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H' M<VAR>s : Set M<VAR>x x₀ : M<VAR>t : Finset ι<VAR>f : ι → M → G<VAR>n : ℕ∞<VAR>p : ι → Prop<VAR>h : ∀ i ∈ t, ContMDiffWithinAt I' I n (f i) Set.univ x₀<GOAL>ContMDiffWithinAt I' I n (fun x => ∏ i ∈ t, f i x) Set.univ x₀
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ s : Set E<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>t : Set E<VAR>ht : MeasurableSet t<VAR>h''t : μ t ≠ ⊤<GOAL>Tendsto (fun r => μ (s ∩ ({x} + r • t)) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 0)
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ s : Set E<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>t : Set E<VAR>ht : MeasurableSet t<VAR>h''t : μ t ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>εpos : 0 < ε<GOAL>∀ᶠ (b : ℝ) in 𝓝[>] 0, μ (s ∩ ({x} + b • t)) / μ ({x} + b • t) < ε
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ s : Set E<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>t : Set E<VAR>ht : MeasurableSet t<VAR>h''t : μ t ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>εpos : 0 < ε<VAR>h't : μ t = 0<GOAL>∀ᶠ (b : ℝ) in 𝓝[>] 0, μ (s ∩ ({x} + b • t)) / μ ({x} + b • t) < ε
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ s : Set E<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>t : Set E<VAR>ht : MeasurableSet t<VAR>h''t : μ t ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>εpos : 0 < ε<VAR>h't : μ t ≠ 0<GOAL>∀ᶠ (b : ℝ) in 𝓝[>] 0, μ (s ∩ ({x} + b • t)) / μ ({x} + b • t) < ε
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ s : Set E<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>t : Set E<VAR>ht : MeasurableSet t<VAR>h''t : μ t ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>εpos : 0 < ε<VAR>h't : μ t ≠ 0<VAR>n : ℕ<VAR>npos : 0 < n<VAR>hn : μ (t \ closedBall 0 ↑n) < ε / 2 * μ t<GOAL>∀ᶠ (b : ℝ) in 𝓝[>] 0, μ (s ∩ ({x} + b • t)) / μ ({x} + b • t) < ε
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ s : Set E<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>t : Set E<VAR>ht : MeasurableSet t<VAR>h''t : μ t ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>εpos : 0 < ε<VAR>h't : μ t ≠ 0<VAR>n : ℕ<VAR>npos : 0 < n<VAR>hn : μ (t \ closedBall 0 ↑n) < ε / 2 * μ t<VAR>L : Tendsto (fun r => μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 0)<GOAL>∀ᶠ (b : ℝ) in 𝓝[>] 0, μ (s ∩ ({x} + b • t)) / μ ({x} + b • t) < ε
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ s : Set E<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>t : Set E<VAR>ht : MeasurableSet t<VAR>h''t : μ t ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>εpos : 0 < ε<VAR>h't : μ t ≠ 0<VAR>n : ℕ<VAR>npos : 0 < n<VAR>hn : μ (t \ closedBall 0 ↑n) < ε / 2 * μ t<VAR>L : Tendsto (fun r => μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 0)<GOAL>∀ (a : ℝ), μ (s ∩ ({x} + a • (t ∩ closedBall 0 ↑n))) / μ ({x} + a • t) < ε / 2 → a ∈ Ioi 0 → μ (s ∩ ({x} + a • t)) / μ ({x} + a • t) < ε
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ s : Set E<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>t : Set E<VAR>ht : MeasurableSet t<VAR>h''t : μ t ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>εpos : 0 < ε<VAR>h't : μ t ≠ 0<VAR>n : ℕ<VAR>npos : 0 < n<VAR>hn : μ (t \ closedBall 0 ↑n) < ε / 2 * μ t<VAR>L : Tendsto (fun r => μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 0)<VAR>r : ℝ<VAR>hr : μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) / μ ({x} + r • t) < ε / 2<VAR>rpos : 0 < r<GOAL>μ (s ∩ ({x} + r • t)) / μ ({x} + r • t) < ε
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ s : Set E<VAR>x : E<VAR>h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>t : Set E<VAR>ht : MeasurableSet t<VAR>h''t : μ t ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>εpos : 0 < ε<VAR>h't : μ t ≠ 0<VAR>n : ℕ<VAR>npos : 0 < n<VAR>hn : μ (t \ closedBall 0 ↑n) < ε / 2 * μ t<VAR>L : Tendsto (fun r => μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 0)<VAR>r : ℝ<VAR>hr : μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) / μ ({x} + r • t) < ε / 2<VAR>rpos : 0 < r<VAR>I : μ (s ∩ ({x} + r • t)) ≤ μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) + μ ({x} + r • (t \ closedBall 0 ↑n))<GOAL>μ (s ∩ ({x} + r • t)) / μ ({x} + r • t) < ε
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<GOAL>(Ioc a b).Nonempty ↔ a < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : LE α<VAR>s t : LowerSet α<VAR>a : α<VAR>f : ι → LowerSet α<GOAL>↑(⨅ i, f i).compl = ↑(⨅ i, (f i).compl)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>r✝ : ℝ<VAR>x : E<VAR>r : ℝ<VAR>y : E<GOAL>y ∈ (normSeminorm 𝕜 E).ball x r ↔ y ∈ Metric.ball x r
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>M : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} M<VAR>inst✝ : MonoidalCategory M<VAR>F : MonoidalFunctor M (C ⥤ C)<VAR>n : M<VAR>X : C<GOAL>F.ε.app ((F.obj n).obj X) = (F.map (ρ_ n).inv).app X ≫ (F.μIso n (𝟙_ M)).inv.app X
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>M : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} M<VAR>inst✝ : MonoidalCategory M<VAR>F : MonoidalFunctor M (C ⥤ C)<VAR>n : M<VAR>X : C<GOAL>F.ε.app ((F.obj n).obj X) = 𝟙 ((𝟙_ (C ⥤ C)).obj ((F.obj n).obj X)) ≫ (F.map (ρ_ n).inv).app X ≫ (F.μIso n (𝟙_ M)).inv.app X
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>M : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} M<VAR>inst✝ : MonoidalCategory M<VAR>F : MonoidalFunctor M (C ⥤ C)<VAR>n : M<VAR>X : C<GOAL>F.ε.app ((F.obj n).obj X) ≫ inv ((F.μIso n (𝟙_ M)).inv.app X) ≫ inv ((F.map (ρ_ n).inv).app X) = 𝟙 ((𝟙_ (C ⥤ C)).obj ((F.obj n).obj X))
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>M : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} M<VAR>inst✝ : MonoidalCategory M<VAR>F : MonoidalFunctor M (C ⥤ C)<VAR>n : M<VAR>X : C<VAR>e_1✝ : ((𝟙_ (C ⥤ C)).obj ((F.obj n).obj X) ⟶ (𝟙_ (C ⥤ C)).obj ((F.obj n).obj X)) = ((𝟙_ (C ⥤ C)).obj ((F.obj n).obj X) ⟶ (F.obj n).obj X)<GOAL>F.ε.app ((F.obj n).obj X) ≫ inv ((F.μIso n (𝟙_ M)).inv.app X) ≫ inv ((F.map (ρ_ n).inv).app X) = F.ε.app ((F.obj n).obj X) ≫ (F.μ n (𝟙_ M)).app X ≫ (F.map (ρ_ n).hom).app X
<VAR>R : Type u_1<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Pow R ℕ<VAR>inst✝ : BinomialRing R<GOAL>(ascPochhammer ℕ 0).smeval (-↑0) = (-1) ^ 0 * ↑(Nat.factorial 0)
<VAR>R : Type u_1<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Pow R ℕ<VAR>inst✝ : BinomialRing R<VAR>n : ℕ<GOAL>(ascPochhammer ℕ (n + 1)).smeval (-↑(n + 1)) = (-1) ^ (n + 1) * ↑(n + 1).factorial
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k l✝ : ℕ<VAR>M₀ : Type u_7<VAR>inst✝¹ : CommMonoidWithZero M₀<VAR>inst✝ : Nontrivial M₀<VAR>l : ℕ<VAR>hl : 0 ^ l = 1<GOAL>0 ∣ l
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>r r' s : α → α → Prop<VAR>inst✝¹ : Preorder α<VAR>inst✝ : OrderBot α<VAR>e : ι → β<VAR>f : ι → α<VAR>hf : Directed (fun x x_1 => x ≤ x_1) f<VAR>he : Injective e<VAR>a b : β<GOAL>∃ z, (fun x x_1 => x ≤ x_1) (extend e f ⊥ a) (extend e f ⊥ z) ∧ (fun x x_1 => x ≤ x_1) (extend e f ⊥ b) (extend e f ⊥ z)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>r r' s : α → α → Prop<VAR>inst✝¹ : Preorder α<VAR>inst✝ : OrderBot α<VAR>e : ι → β<VAR>f : ι → α<VAR>hf : Directed (fun x x_1 => x ≤ x_1) f<VAR>he : Injective e<VAR>a b : β<VAR>ha : ¬∃ i, e i = a<GOAL>∃ z, (fun x x_1 => x ≤ x_1) (extend e f ⊥ a) (extend e f ⊥ z) ∧ (fun x x_1 => x ≤ x_1) (extend e f ⊥ b) (extend e f ⊥ z)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>r r' s : α → α → Prop<VAR>inst✝¹ : Preorder α<VAR>inst✝ : OrderBot α<VAR>e : ι → β<VAR>f : ι → α<VAR>hf : Directed (fun x x_1 => x ≤ x_1) f<VAR>he : Injective e<VAR>b : β<VAR>i : ι<GOAL>∃ z, (fun x x_1 => x ≤ x_1) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧ (fun x x_1 => x ≤ x_1) (extend e f ⊥ b) (extend e f ⊥ z)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>r r' s : α → α → Prop<VAR>inst✝¹ : Preorder α<VAR>inst✝ : OrderBot α<VAR>e : ι → β<VAR>f : ι → α<VAR>hf : Directed (fun x x_1 => x ≤ x_1) f<VAR>he : Injective e<VAR>b : β<VAR>i : ι<VAR>hb : ¬∃ i, e i = b<GOAL>∃ z, (fun x x_1 => x ≤ x_1) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧ (fun x x_1 => x ≤ x_1) (extend e f ⊥ b) (extend e f ⊥ z)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>r r' s : α → α → Prop<VAR>inst✝¹ : Preorder α<VAR>inst✝ : OrderBot α<VAR>e : ι → β<VAR>f : ι → α<VAR>hf : Directed (fun x x_1 => x ≤ x_1) f<VAR>he : Injective e<VAR>i j : ι<GOAL>∃ z, (fun x x_1 => x ≤ x_1) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧ (fun x x_1 => x ≤ x_1) (extend e f ⊥ (e j)) (extend e f ⊥ z)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>r r' s : α → α → Prop<VAR>inst✝¹ : Preorder α<VAR>inst✝ : OrderBot α<VAR>e : ι → β<VAR>f : ι → α<VAR>hf : Directed (fun x x_1 => x ≤ x_1) f<VAR>he : Injective e<VAR>i j k : ι<VAR>hi : f i ≤ f k<VAR>hj : f j ≤ f k<GOAL>∃ z, (fun x x_1 => x ≤ x_1) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧ (fun x x_1 => x ≤ x_1) (extend e f ⊥ (e j)) (extend e f ⊥ z)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>r r' s : α → α → Prop<VAR>inst✝¹ : Preorder α<VAR>inst✝ : OrderBot α<VAR>e : ι → β<VAR>f : ι → α<VAR>hf : Directed (fun x x_1 => x ≤ x_1) f<VAR>he : Injective e<VAR>i j k : ι<VAR>hi : f i ≤ f k<VAR>hj : f j ≤ f k<GOAL>(fun x x_1 => x ≤ x_1) (extend e f ⊥ (e i)) (extend e f ⊥ (e k)) ∧ (fun x x_1 => x ≤ x_1) (extend e f ⊥ (e j)) (extend e f ⊥ (e k))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : Preorder β<VAR>inst✝¹ : OrderTop β<VAR>inst✝ : OrderTopology β<VAR>l : Filter α<VAR>f g : α → β<VAR>hf : Tendsto f l (𝓝 ⊤)<VAR>hg : f ≤ᶠ[l] g<GOAL>Tendsto g l (𝓝 ⊤)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : Preorder β<VAR>inst✝¹ : OrderTop β<VAR>inst✝ : OrderTopology β<VAR>l : Filter α<VAR>f g : α → β<VAR>hg : f ≤ᶠ[l] g<VAR>hf : ∀ i < ⊤, ∀ᶠ (a : α) in l, f a ∈ Ioi i<GOAL>∀ i < ⊤, ∀ᶠ (a : α) in l, g a ∈ Ioi i
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : Preorder β<VAR>inst✝¹ : OrderTop β<VAR>inst✝ : OrderTopology β<VAR>l : Filter α<VAR>f g : α → β<VAR>hg : f ≤ᶠ[l] g<VAR>hf : ∀ i < ⊤, ∀ᶠ (a : α) in l, f a ∈ Ioi i<VAR>x : β<VAR>hx : x < ⊤<GOAL>∀ᶠ (a : α) in l, g a ∈ Ioi x
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>x y : (P F).W<VAR>h : Wequiv x y<GOAL>Wequiv y x
<VAR>R : Type u<VAR>a✝ b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q p : R[X]<VAR>n : ℕ<VAR>a : R<GOAL>(p.update n a).coeff n = a
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝⁹ : Category.{u_7, u_1} C<VAR>inst✝⁸ : Category.{u_6, u_2} D<VAR>inst✝⁷ : Category.{u_5, u_3} A<VAR>L : C ⥤ D<VAR>F : D ⥤ A<VAR>G : C ⥤ A<VAR>e : L ⋙ F ≅ G<VAR>M : Type u_4<VAR>inst✝⁶ : AddMonoid M<VAR>inst✝⁵ : HasShift C M<VAR>inst✝⁴ : HasShift D M<VAR>inst✝³ : L.CommShift M<VAR>inst✝² : G.ShiftSequence M<VAR>F' : M → D ⥤ A<VAR>e' : (m : M) → L ⋙ F' m ≅ G.shift m<VAR>inst✝¹ : ((whiskeringLeft C D A).obj L).Full<VAR>inst✝ : ((whiskeringLeft C D A).obj L).Faithful<VAR>n a a' : M<VAR>ha' : n + a = a'<VAR>X : C<GOAL>(F.shiftIso n a a' ha').hom.app (L.obj X) = (F.shift a).map ((L.commShiftIso n).inv.app X) ≫ (e' a).hom.app ((shiftFunctor C n).obj X) ≫ (G.shiftIso n a a' ha').hom.app X ≫ (e' a').inv.app X
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝ : NormedRing R<VAR>r : ℝ<VAR>hr : 1 < r<GOAL>Nat.cast =o[atTop] fun n => r ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteLattice α<VAR>f : Filter β<VAR>p : β → Prop<VAR>u : β → α<GOAL>blimsup u f p = ⨅ s ∈ f, ⨆ b, ⨆ (_ : p b ∧ b ∈ s), u b
<VAR>m n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>x✝ : α✝ 0<VAR>q : (i : Fin (n + 1)) → α✝ i<VAR>p✝ : (i : Fin n) → α✝ i.succ<VAR>i : Fin n<VAR>y : α✝ i.succ<VAR>z : α✝ 0<VAR>α : Fin (n + 2) → Type u_1<VAR>x : α 0<VAR>p : (i : Fin n.succ) → α i.succ<GOAL>cons x p 1 = p 0
<VAR>m n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>x✝ : α✝ 0<VAR>q : (i : Fin (n + 1)) → α✝ i<VAR>p✝ : (i : Fin n) → α✝ i.succ<VAR>i : Fin n<VAR>y : α✝ i.succ<VAR>z : α✝ 0<VAR>α : Fin (n + 2) → Type u_1<VAR>x : α 0<VAR>p : (i : Fin n.succ) → α i.succ<GOAL>cons x p 1 = cons x p (succ 0)
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>H : SimpleGraph V<GOAL>turanGraph n r = ⊤ ↔ r = 0 ∨ n ≤ r
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>H : SimpleGraph V<GOAL>(∀ (a a_1 : Fin n), ↑a % r = ↑a_1 % r ↔ a = a_1) ↔ r = 0 ∨ n ≤ r
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y z : E<VAR>δ ε : ℝ<VAR>hε : 0 < ε<VAR>hδ : 0 ≤ δ<VAR>a b : E<GOAL>Metric.ball a ε - Metric.closedBall b δ = Metric.ball (a - b) (ε + δ)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>M' : Type u_5<VAR>N' : Type u_6<VAR>ι : Type u_7<VAR>κ : Type u_8<VAR>τ : Type u_9<VAR>ι' : Type u_10<VAR>κ' : Type u_11<VAR>inst✝¹⁸ : DecidableEq ι<VAR>inst✝¹⁷ : DecidableEq κ<VAR>inst✝¹⁶ : DecidableEq τ<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : Fintype κ<VAR>inst✝¹³ : Fintype τ<VAR>inst✝¹² : Finite ι'<VAR>inst✝¹¹ : Finite κ'<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup N'<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R N'<VAR>bM : Basis ι R M<VAR>bN : Basis κ R N<VAR>bP : Basis τ R P<VAR>bM' : Basis ι' R M'<VAR>bN' : Basis κ' R N'<VAR>i : ι<VAR>j : κ<VAR>k k' : τ<VAR>i' : ι<VAR>j' : κ<GOAL>(toMatrix ((bM.tensorProduct bN).tensorProduct bP) (bM.tensorProduct (bN.tensorProduct bP))) ↑(TensorProduct.assoc R M N P) (i, j, k) ((i', j'), k') = submatrix 1 _root_.id ⇑(Equiv.prodAssoc ι κ τ) (i, j, k) ((i', j'), k')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h₁ : min a b < max c d<VAR>h₂ : min c d < max a b<GOAL>Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>hab : a ≤ b<VAR>hcd : c ≤ d<VAR>h₁ : a < d<VAR>h₂ : c < b<GOAL>Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>hab : a ≤ b<VAR>hcd : d ≤ c<VAR>h₁ : a < c<VAR>h₂ : d < b<GOAL>Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>hab : b ≤ a<VAR>hcd : c ≤ d<VAR>h₁ : b < d<VAR>h₂ : c < a<GOAL>Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>hab : b ≤ a<VAR>hcd : d ≤ c<VAR>h₁ : b < c<VAR>h₂ : d < a<GOAL>Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M✝ : Type u_3<VAR>N : Type u_4<VAR>X✝ : Type u_5<VAR>inst✝⁴ : TopologicalSpace X✝<VAR>inst✝³ : TopologicalSpace M✝<VAR>inst✝² : CommMonoid M✝<VAR>inst✝¹ : ContinuousMul M✝<VAR>X : Type u_6<VAR>M : Type u_7<VAR>inst✝ : CommMonoid M<VAR>s : Finset ι<VAR>l : Filter X<VAR>f g : ι → X → M<VAR>hs : ∀ i ∈ s, f i =ᶠ[l] g i<GOAL>∏ i ∈ s, f i =ᶠ[l] ∏ i ∈ s, g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M✝ : Type u_3<VAR>N : Type u_4<VAR>X✝ : Type u_5<VAR>inst✝⁴ : TopologicalSpace X✝<VAR>inst✝³ : TopologicalSpace M✝<VAR>inst✝² : CommMonoid M✝<VAR>inst✝¹ : ContinuousMul M✝<VAR>X : Type u_6<VAR>M : Type u_7<VAR>inst✝ : CommMonoid M<VAR>s : Finset ι<VAR>l : Filter X<VAR>f g : ι → X → M<VAR>hs : ∀ᶠ (x : X) in l, ∀ i ∈ s, f i x = g i x<GOAL>∏ i ∈ s, f i =ᶠ[l] ∏ i ∈ s, g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M✝ : Type u_3<VAR>N : Type u_4<VAR>X✝ : Type u_5<VAR>inst✝⁴ : TopologicalSpace X✝<VAR>inst✝³ : TopologicalSpace M✝<VAR>inst✝² : CommMonoid M✝<VAR>inst✝¹ : ContinuousMul M✝<VAR>X : Type u_6<VAR>M : Type u_7<VAR>inst✝ : CommMonoid M<VAR>s : Finset ι<VAR>l : Filter X<VAR>f g : ι → X → M<VAR>hs : ∀ᶠ (x : X) in l, ∀ i ∈ s, f i x = g i x<VAR>x : X<VAR>hx : ∀ i ∈ s, f i x = g i x<GOAL>(∏ i ∈ s, f i) x = (∏ i ∈ s, g i) x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : Semifield R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : TopologicalSemiring R<VAR>inst✝⁶ : ContinuousStar R<VAR>inst✝⁵ : HasContinuousInv₀ R<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<VAR>hf' : ∀ x ∈ spectrum R a, f x ≠ 0<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>cfc f a * cfc (fun x => (f x)⁻¹) a = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : Semifield R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : TopologicalSemiring R<VAR>inst✝⁶ : ContinuousStar R<VAR>inst✝⁵ : HasContinuousInv₀ R<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<VAR>hf' : ∀ x ∈ spectrum R a, f x ≠ 0<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>cfc (fun x => f x * (f x)⁻¹) a = cfc 1 a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : Semifield R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : TopologicalSemiring R<VAR>inst✝⁶ : ContinuousStar R<VAR>inst✝⁵ : HasContinuousInv₀ R<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<VAR>hf' : ∀ x ∈ spectrum R a, f x ≠ 0<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>cfc (fun x => (f x)⁻¹) a * cfc f a = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : Semifield R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : TopologicalSemiring R<VAR>inst✝⁶ : ContinuousStar R<VAR>inst✝⁵ : HasContinuousInv₀ R<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a : A<VAR>hf' : ∀ x ∈ spectrum R a, f x ≠ 0<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>cfc (fun x => (f x)⁻¹ * f x) a = cfc 1 a
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝¹ : Preorder α<VAR>inst✝ : NoMaxOrder α<VAR>a : α<GOAL>∃ f, StrictMono f ∧ f 0 = a
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝¹ : Preorder α<VAR>inst✝ : NoMaxOrder α<VAR>a : α<VAR>g : α → α<VAR>hg : ∀ (x : α), x < g x<GOAL>∃ f, StrictMono f ∧ f 0 = a