ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>x y : α<VAR>hx : x ∈ l<VAR>hy : y ∈ l<VAR>h : indexOf x l = indexOf y l<VAR>x_eq_y : x = y<GOAL>x = y
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>F : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>inst✝ : Category.{v₄, u₄} F<VAR>G : C ⥤ E<VAR>H : D ⥤ F<VAR>L₁ : C ⥤ D<VAR>R₁ : D ⥤ C<VAR>L₂ : E ⥤ F<VAR>R₂ : F ⥤ E<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>α : G ⋙ L₂ ⟶ L₁ ⋙ H<VAR>c : C<GOAL>adj₂.unit.app (G.obj c) ≫ R₂.map (L₂.map (G.map (adj₁.unit.app c))) ≫ R₂.map (α.app (R₁.obj (L₁.obj c))) ≫ R₂.map (H.map (adj₁.counit.app (L₁.obj c))) = adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>F : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>inst✝ : Category.{v₄, u₄} F<VAR>G : C ⥤ E<VAR>H : D ⥤ F<VAR>L₁ : C ⥤ D<VAR>R₁ : D ⥤ C<VAR>L₂ : E ⥤ F<VAR>R₂ : F ⥤ E<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>α : G ⋙ L₂ ⟶ L₁ ⋙ H<VAR>c : C<GOAL>adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c ≫ (L₁ ⋙ H).map (adj₁.unit.app c)) ≫ R₂.map (H.map (adj₁.counit.app (L₁.obj c))) = adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>F : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>inst✝ : Category.{v₄, u₄} F<VAR>G : C ⥤ E<VAR>H : D ⥤ F<VAR>L₁ : C ⥤ D<VAR>R₁ : D ⥤ C<VAR>L₂ : E ⥤ F<VAR>R₂ : F ⥤ E<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>α : G ⋙ L₂ ⟶ L₁ ⋙ H<VAR>c : C<GOAL>adj₂.unit.app (G.obj c) ≫ (R₂.map (α.app c) ≫ R₂.map ((L₁ ⋙ H).map (adj₁.unit.app c))) ≫ R₂.map (H.map (adj₁.counit.app (L₁.obj c))) = adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>F : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>inst✝ : Category.{v₄, u₄} F<VAR>G : C ⥤ E<VAR>H : D ⥤ F<VAR>L₁ : C ⥤ D<VAR>R₁ : D ⥤ C<VAR>L₂ : E ⥤ F<VAR>R₂ : F ⥤ E<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>α : G ⋙ L₂ ⟶ L₁ ⋙ H<VAR>c : C<GOAL>adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c) ≫ R₂.map (H.map (𝟙 (L₁.obj c))) = adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c)
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : DivisionCommMonoid α<VAR>m : Multiset ι<VAR>f g : ι → α<GOAL>(map (fun i => (f i)⁻¹) m).prod = (map f m).prod⁻¹
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>a₂✝ : W.Point<VAR>hP : toClass zero = toClass a₂✝<GOAL>zero = a₂✝
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x✝ y✝ : F<VAR>h : W.Nonsingular x✝ y✝<VAR>a₂✝ : W.Point<VAR>hP : toClass (some h) = toClass a₂✝<GOAL>some h = a₂✝
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>a₂✝ : W.Point<VAR>hP : toClass zero = toClass a₂✝<GOAL>toClass (-zero) + toClass zero = 0
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x✝ y✝ : F<VAR>h : W.Nonsingular x✝ y✝<VAR>a₂✝ : W.Point<VAR>hP : toClass (some h) = toClass a₂✝<GOAL>toClass (-some h) + toClass (some h) = 0
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f g : R<GOAL>basicOpen (f * g) ≤ basicOpen f
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f g : R<GOAL>basicOpen f ⊓ basicOpen g ≤ basicOpen f
<VAR>R : Type u<VAR>inst✝⁵ : Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : ι → Type w<VAR>inst✝⁴ : (i : ι) → AddCommMonoid (M i)<VAR>inst✝³ : (i : ι) → Module R (M i)<VAR>N : Type u₁<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>φ : (i : ι) → M i →ₗ[R] N<VAR>ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N<VAR>inst✝ : Fintype ι<VAR>f g : ⨁ (i : ι), M i<VAR>x✝ : ι<GOAL>(f + g) x✝ = (⇑f + ⇑g) x✝
<VAR>R : Type u<VAR>inst✝⁵ : Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : ι → Type w<VAR>inst✝⁴ : (i : ι) → AddCommMonoid (M i)<VAR>inst✝³ : (i : ι) → Module R (M i)<VAR>N : Type u₁<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>φ : (i : ι) → M i →ₗ[R] N<VAR>ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N<VAR>inst✝ : Fintype ι<VAR>c : R<VAR>f : ⨁ (i : ι), M i<GOAL>{ toFun := DFunLike.coe, map_add' := ⋯ }.toFun (c • f) = (RingHom.id R) c • { toFun := DFunLike.coe, map_add' := ⋯ }.toFun f
<VAR>R : Type u<VAR>inst✝⁵ : Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : ι → Type w<VAR>inst✝⁴ : (i : ι) → AddCommMonoid (M i)<VAR>inst✝³ : (i : ι) → Module R (M i)<VAR>N : Type u₁<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>φ : (i : ι) → M i →ₗ[R] N<VAR>ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N<VAR>inst✝ : Fintype ι<VAR>c : R<VAR>f : ⨁ (i : ι), M i<GOAL>⇑(c • f) = c • ⇑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t S U : Set X<VAR>hS : IsPreirreducible S<VAR>hU : IsOpen U<VAR>h : (S ∩ U).Nonempty<GOAL>S ⊆ closure (S ∩ U)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t S U : Set X<VAR>hS : IsPreirreducible S<VAR>hU : IsOpen U<VAR>h : (S ∩ U).Nonempty<VAR>h' : ¬S ⊆ closure (S ∩ U)<GOAL>False
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t S U : Set X<VAR>hS : IsPreirreducible S<VAR>hU : IsOpen U<VAR>h : (S ∩ U).Nonempty<VAR>h' : ¬S ⊆ closure (S ∩ U)<VAR>x : X<VAR>h₁ : x ∈ S<VAR>h₂ : x ∈ U<VAR>h₃ : x ∈ (closure (S ∩ U))ᶜ<GOAL>False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>f : ι' → ι<VAR>hf : Function.Injective f<GOAL>Orthonormal 𝕜 (v ∘ f)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : α → β<VAR>g : β → γ<VAR>hg : UniformInducing g<GOAL>map (fun x => (f x.1, f x.2)) (𝓤 α) ≤ 𝓤 β ↔ map (fun x => ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 α) ≤ 𝓤 γ
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>x : R<GOAL>eval x (C a * p) = a * eval x p
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemifield α<VAR>inst✝ : FloorSemiring α<VAR>m n : ℕ<GOAL>⌊↑m / ↑n⌋₊ = m / n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemifield α<VAR>inst✝ : FloorSemiring α<VAR>m n : ℕ<GOAL>m = ⌊↑m⌋₊
<VAR>E : Type u_1<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : T1Space E<VAR>s t u : Set E<VAR>hta : Absorbent ℝ t<VAR>htb : IsVonNBounded ℝ t<VAR>x : E<GOAL>gaugeRescale t u (gaugeRescale s t x) = gaugeRescale s u x
<VAR>E : Type u_1<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : T1Space E<VAR>s t u : Set E<VAR>hta : Absorbent ℝ t<VAR>htb : IsVonNBounded ℝ t<GOAL>gaugeRescale t u (gaugeRescale s t 0) = gaugeRescale s u 0
<VAR>E : Type u_1<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : T1Space E<VAR>s t u : Set E<VAR>hta : Absorbent ℝ t<VAR>htb : IsVonNBounded ℝ t<VAR>x : E<VAR>hx : x ≠ 0<GOAL>gaugeRescale t u (gaugeRescale s t x) = gaugeRescale s u x
<VAR>E : Type u_1<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : T1Space E<VAR>s t u : Set E<VAR>hta : Absorbent ℝ t<VAR>htb : IsVonNBounded ℝ t<VAR>x : E<VAR>hx : x ≠ 0<GOAL>gauge t x ≠ 0
<VAR>E : Type u_1<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : T1Space E<VAR>s t u : Set E<VAR>hta : Absorbent ℝ t<VAR>htb : IsVonNBounded ℝ t<VAR>x : E<VAR>hx : x ≠ 0<GOAL>0 ≤ gauge s x / gauge t 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>A : E →L[ℝ] E<VAR>m : ℝ≥0<VAR>hm : ENNReal.ofReal |A.det| < ↑m<GOAL>∀ᶠ (δ : ℝ≥0) in 𝓝[>] 0, ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → μ (f '' s) ≤ ↑m * μ 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>A : E →L[ℝ] E<VAR>m : ℝ≥0<VAR>hm : ENNReal.ofReal |A.det| < ↑m<GOAL>{x | (fun δ => ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → μ (f '' s) ≤ ↑m * μ s) x} ∈ 𝓝 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>A : E →L[ℝ] E<VAR>m : ℝ≥0<VAR>hm : ENNReal.ofReal |A.det| < ↑m<VAR>d : ℝ≥0∞ := ENNReal.ofReal |A.det|<GOAL>{x | (fun δ => ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → μ (f '' s) ≤ ↑m * μ s) x} ∈ 𝓝 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>A : E →L[ℝ] E<VAR>m : ℝ≥0<VAR>hm : ENNReal.ofReal |A.det| < ↑m<VAR>d : ℝ≥0∞ := ENNReal.ofReal |A.det|<VAR>ε : ℝ<VAR>hε : μ (closedBall 0 ε + ⇑A '' closedBall 0 1) < ↑m * μ (closedBall 0 1)<VAR>εpos : 0 < ε<GOAL>{x | (fun δ => ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → μ (f '' s) ≤ ↑m * μ s) x} ∈ 𝓝 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>A : E →L[ℝ] E<VAR>m : ℝ≥0<VAR>hm : ENNReal.ofReal |A.det| < ↑m<VAR>d : ℝ≥0∞ := ENNReal.ofReal |A.det|<VAR>ε : ℝ<VAR>hε : μ (closedBall 0 ε + ⇑A '' closedBall 0 1) < ↑m * μ (closedBall 0 1)<VAR>εpos : 0 < ε<VAR>this : Iio ⟨ε, ⋯⟩ ∈ 𝓝 0<GOAL>{x | (fun δ => ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → μ (f '' s) ≤ ↑m * μ s) x} ∈ 𝓝 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>A : E →L[ℝ] E<VAR>m : ℝ≥0<VAR>hm : ENNReal.ofReal |A.det| < ↑m<VAR>d : ℝ≥0∞ := ENNReal.ofReal |A.det|<VAR>ε : ℝ<VAR>hε : μ (closedBall 0 ε + ⇑A '' closedBall 0 1) < ↑m * μ (closedBall 0 1)<VAR>εpos : 0 < ε<VAR>this : Iio ⟨ε, ⋯⟩ ∈ 𝓝 0<GOAL>∀ a ∈ Iio ⟨ε, ⋯⟩, ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s a → μ (f '' s) ≤ ↑m * μ 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>A : E →L[ℝ] E<VAR>m : ℝ≥0<VAR>hm : ENNReal.ofReal |A.det| < ↑m<VAR>d : ℝ≥0∞ := ENNReal.ofReal |A.det|<VAR>ε : ℝ<VAR>hε : μ (closedBall 0 ε + ⇑A '' closedBall 0 1) < ↑m * μ (closedBall 0 1)<VAR>εpos : 0 < ε<VAR>this : Iio ⟨ε, ⋯⟩ ∈ 𝓝 0<VAR>δ : ℝ≥0<VAR>hδ : δ ∈ Iio ⟨ε, ⋯⟩<VAR>s : Set E<VAR>f : E → E<VAR>hf : ApproximatesLinearOn f A s δ<GOAL>μ (f '' s) ≤ ↑m * μ 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>A : E →L[ℝ] E<VAR>m : ℝ≥0<VAR>hm : ENNReal.ofReal |A.det| < ↑m<VAR>d : ℝ≥0∞ := ENNReal.ofReal |A.det|<VAR>ε : ℝ<VAR>hε : μ (closedBall 0 ε + ⇑A '' closedBall 0 1) < ↑m * μ (closedBall 0 1)<VAR>εpos : 0 < ε<VAR>this : Iio ⟨ε, ⋯⟩ ∈ 𝓝 0<VAR>δ : ℝ≥0<VAR>s : Set E<VAR>f : E → E<VAR>hf : ApproximatesLinearOn f A s δ<VAR>hδ : ↑δ < ε<GOAL>μ (f '' s) ≤ ↑m * μ 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>A : E →L[ℝ] E<VAR>m : ℝ≥0<VAR>hm : ENNReal.ofReal |A.det| < ↑m<VAR>d : ℝ≥0∞ := ENNReal.ofReal |A.det|<VAR>ε : ℝ<VAR>hε : μ (closedBall 0 ε + ⇑A '' closedBall 0 1) < ↑m * μ (closedBall 0 1)<VAR>εpos : 0 < ε<VAR>this : Iio ⟨ε, ⋯⟩ ∈ 𝓝 0<VAR>δ : ℝ≥0<VAR>s : Set E<VAR>f : E → E<VAR>hf : ApproximatesLinearOn f A s δ<VAR>hδ : ↑δ < ε<VAR>I : ∀ (x : E) (r : ℝ), x ∈ s → 0 ≤ r → μ (f '' (s ∩ closedBall x r)) ≤ ↑m * μ (closedBall x r)<GOAL>μ (f '' s) ≤ ↑m * μ 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>A : E →L[ℝ] E<VAR>m : ℝ≥0<VAR>hm : ENNReal.ofReal |A.det| < ↑m<VAR>d : ℝ≥0∞ := ENNReal.ofReal |A.det|<VAR>ε : ℝ<VAR>hε : μ (closedBall 0 ε + ⇑A '' closedBall 0 1) < ↑m * μ (closedBall 0 1)<VAR>εpos : 0 < ε<VAR>this : Iio ⟨ε, ⋯⟩ ∈ 𝓝 0<VAR>δ : ℝ≥0<VAR>s : Set E<VAR>f : E → E<VAR>hf : ApproximatesLinearOn f A s δ<VAR>hδ : ↑δ < ε<VAR>I : ∀ (x : E) (r : ℝ), x ∈ s → 0 ≤ r → μ (f '' (s ∩ closedBall x r)) ≤ ↑m * μ (closedBall x r)<VAR>J : ∀ᶠ (a : ℝ≥0∞) in 𝓝[>] 0, μ (f '' s) ≤ ↑m * (μ s + a)<GOAL>μ (f '' s) ≤ ↑m * μ 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>A : E →L[ℝ] E<VAR>m : ℝ≥0<VAR>hm : ENNReal.ofReal |A.det| < ↑m<VAR>d : ℝ≥0∞ := ENNReal.ofReal |A.det|<VAR>ε : ℝ<VAR>hε : μ (closedBall 0 ε + ⇑A '' closedBall 0 1) < ↑m * μ (closedBall 0 1)<VAR>εpos : 0 < ε<VAR>this : Iio ⟨ε, ⋯⟩ ∈ 𝓝 0<VAR>δ : ℝ≥0<VAR>s : Set E<VAR>f : E → E<VAR>hf : ApproximatesLinearOn f A s δ<VAR>hδ : ↑δ < ε<VAR>I : ∀ (x : E) (r : ℝ), x ∈ s → 0 ≤ r → μ (f '' (s ∩ closedBall x r)) ≤ ↑m * μ (closedBall x r)<VAR>J : ∀ᶠ (a : ℝ≥0∞) in 𝓝[>] 0, μ (f '' s) ≤ ↑m * (μ s + a)<VAR>L : Tendsto (fun a => ↑m * (μ s + a)) (𝓝[>] 0) (𝓝 (↑m * (μ s + 0)))<GOAL>μ (f '' s) ≤ ↑m * μ 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>A : E →L[ℝ] E<VAR>m : ℝ≥0<VAR>hm : ENNReal.ofReal |A.det| < ↑m<VAR>d : ℝ≥0∞ := ENNReal.ofReal |A.det|<VAR>ε : ℝ<VAR>hε : μ (closedBall 0 ε + ⇑A '' closedBall 0 1) < ↑m * μ (closedBall 0 1)<VAR>εpos : 0 < ε<VAR>this : Iio ⟨ε, ⋯⟩ ∈ 𝓝 0<VAR>δ : ℝ≥0<VAR>s : Set E<VAR>f : E → E<VAR>hf : ApproximatesLinearOn f A s δ<VAR>hδ : ↑δ < ε<VAR>I : ∀ (x : E) (r : ℝ), x ∈ s → 0 ≤ r → μ (f '' (s ∩ closedBall x r)) ≤ ↑m * μ (closedBall x r)<VAR>J : ∀ᶠ (a : ℝ≥0∞) in 𝓝[>] 0, μ (f '' s) ≤ ↑m * (μ s + a)<VAR>L : Tendsto (fun a => ↑m * (μ s + a)) (𝓝[>] 0) (𝓝 (↑m * μ s))<GOAL>μ (f '' s) ≤ ↑m * μ s
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : _root_.Prime p<VAR>hBint : IsIntegral R B.gen<VAR>z : L<VAR>Q : R[X]<VAR>hQ : (aeval B.gen) Q = p • z<VAR>hzint : IsIntegral R z<VAR>hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})<GOAL>p ∣ Q.coeff 0
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : _root_.Prime p<VAR>hBint : IsIntegral R B.gen<VAR>z : L<VAR>Q : R[X]<VAR>hQ : (aeval B.gen) Q = p • z<VAR>hzint : IsIntegral R z<VAR>hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})<VAR>this : Module.Finite K L := finite B<GOAL>p ∣ Q.coeff 0
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : _root_.Prime p<VAR>hBint : IsIntegral R B.gen<VAR>z : L<VAR>Q : R[X]<VAR>hQ : (aeval B.gen) Q = p • z<VAR>hzint : IsIntegral R z<VAR>hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})<VAR>this : Module.Finite K L := finite B<VAR>P : R[X] := minpoly R B.gen<GOAL>p ∣ Q.coeff 0
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : _root_.Prime p<VAR>hBint : IsIntegral R B.gen<VAR>z : L<VAR>Q : R[X]<VAR>hQ : (aeval B.gen) Q = p • z<VAR>hzint : IsIntegral R z<VAR>hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})<VAR>this : Module.Finite K L := finite B<VAR>P : R[X] := minpoly R B.gen<VAR>n : ℕ<VAR>hn : B.dim = n.succ<GOAL>p ∣ Q.coeff 0
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : _root_.Prime p<VAR>hBint : IsIntegral R B.gen<VAR>z : L<VAR>Q : R[X]<VAR>hQ : (aeval B.gen) Q = p • z<VAR>hzint : IsIntegral R z<VAR>hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})<VAR>this : Module.Finite K L := finite B<VAR>P : R[X] := minpoly R B.gen<VAR>n : ℕ<VAR>hn : B.dim = n.succ<VAR>finrank_K_L : FiniteDimensional.finrank K L = B.dim<GOAL>p ∣ Q.coeff 0
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : _root_.Prime p<VAR>hBint : IsIntegral R B.gen<VAR>z : L<VAR>Q : R[X]<VAR>hQ : (aeval B.gen) Q = p • z<VAR>hzint : IsIntegral R z<VAR>hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})<VAR>this : Module.Finite K L := finite B<VAR>P : R[X] := minpoly R B.gen<VAR>n : ℕ<VAR>hn : B.dim = n.succ<VAR>finrank_K_L : FiniteDimensional.finrank K L = B.dim<VAR>deg_K_P : (minpoly K B.gen).natDegree = B.dim<GOAL>p ∣ Q.coeff 0
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : _root_.Prime p<VAR>hBint : IsIntegral R B.gen<VAR>z : L<VAR>Q : R[X]<VAR>hQ : (aeval B.gen) Q = p • z<VAR>hzint : IsIntegral R z<VAR>hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})<VAR>this : Module.Finite K L := finite B<VAR>P : R[X] := minpoly R B.gen<VAR>n : ℕ<VAR>hn : B.dim = n.succ<VAR>finrank_K_L : FiniteDimensional.finrank K L = B.dim<VAR>deg_K_P : (minpoly K B.gen).natDegree = B.dim<VAR>deg_R_P : P.natDegree = B.dim<GOAL>p ∣ Q.coeff 0
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : _root_.Prime p<VAR>hBint : IsIntegral R B.gen<VAR>z : L<VAR>Q : R[X]<VAR>hQ : (aeval B.gen) Q = p • z<VAR>hzint : IsIntegral R z<VAR>hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})<VAR>this : Module.Finite K L := finite B<VAR>P : R[X] := minpoly R B.gen<VAR>n : ℕ<VAR>hn : B.dim = n.succ<VAR>finrank_K_L : FiniteDimensional.finrank K L = B.dim<VAR>deg_K_P : (minpoly K B.gen).natDegree = B.dim<VAR>deg_R_P : P.natDegree = B.dim<VAR>f : ℕ → L<VAR>hf : ∀ (i : ℕ), (Polynomial.map (algebraMap R L) (minpoly R B.gen)).natDegree ≤ i → f i ∈ adjoin R {B.gen} ∧ (algebraMap R L) p * f i = B.gen ^ i<GOAL>p ∣ Q.coeff 0
<VAR>R : Type u<VAR>K : Type v<VAR>L : Type z<VAR>p : R<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : Field L<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsIntegrallyClosed R<VAR>B : PowerBasis K L<VAR>hp : _root_.Prime p<VAR>hBint : IsIntegral R B.gen<VAR>z : L<VAR>Q : R[X]<VAR>hQ : (aeval B.gen) Q = p • z<VAR>hzint : IsIntegral R z<VAR>hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})<VAR>this : Module.Finite K L := finite B<VAR>P : R[X] := minpoly R B.gen<VAR>n : ℕ<VAR>hn : B.dim = n.succ<VAR>finrank_K_L : FiniteDimensional.finrank K L = B.dim<VAR>deg_K_P : (minpoly K B.gen).natDegree = B.dim<VAR>deg_R_P : P.natDegree = B.dim<VAR>f : ℕ → L<VAR>hf : ∀ (i : ℕ), B.dim ≤ i → f i ∈ adjoin R {B.gen} ∧ (algebraMap R L) p * f i = B.gen ^ i<GOAL>p ∣ Q.coeff 0