ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s✝ : Set β<VAR>ι : Type u_3<VAR>U : ι → Opens β<VAR>hU : iSup U = ⊤<VAR>H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)<VAR>s : Set α<VAR>hs : IsOpen s<VAR>i : ι<VAR>e_1✝ : ↥(U i) = ↑(U i).carrier<VAR>x : β<VAR>hx : x ∈ U i<GOAL>⟨x, hx⟩ ∈ Subtype.val ⁻¹' (f '' s) ↔ ⟨x, hx⟩ ∈ (U i).carrier.restrictPreimage f '' (Subtype.val ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s✝ : Set β<VAR>ι : Type u_3<VAR>U : ι → Opens β<VAR>hU : iSup U = ⊤<VAR>H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)<VAR>s : Set α<VAR>hs : IsOpen s<VAR>i : ι<VAR>e_1✝ : ↥(U i) = ↑(U i).carrier<VAR>x : β<VAR>hx : x ∈ U i<GOAL>(∃ y ∈ s, f y = x) ↔ ∃ y ∈ s, f y ∈ U i ∧ f y = x
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>X Y : C<VAR>D : Type u₂<VAR>inst✝⁴ : Category.{w, u₂} D<VAR>F : C ⥤ D<VAR>A A' B B' : C<VAR>inst✝³ : HasBinaryCoproduct A B<VAR>inst✝² : HasBinaryCoproduct A' B'<VAR>inst✝¹ : HasBinaryCoproduct (F.obj A) (F.obj B)<VAR>inst✝ : HasBinaryCoproduct (F.obj A') (F.obj B')<VAR>f : A ⟶ A'<VAR>g : B ⟶ B'<GOAL>coprodComparison F A B ≫ F.map (coprod.map f g) = coprod.map (F.map f) (F.map g) ≫ coprodComparison F A' B'
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ✝ μ : Measure Ω<GOAL>variance 0 μ = 0
<VAR>R : Type u_1<VAR>inst✝ : AddCommGroup R<VAR>f g : ℕ → R<VAR>s : Set ℕ<VAR>hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s<VAR>hs₀ : 0 ∉ s<GOAL>(∀ n ∈ s, ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n ∈ s, ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n
<VAR>R : Type u_1<VAR>inst✝ : AddCommGroup R<VAR>f g : ℕ → R<VAR>s : Set ℕ<VAR>hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s<VAR>hs₀ : 0 ∉ s<VAR>this : ∀ (P : ℕ → Prop), (∀ n ∈ s, P n) ↔ ∀ n > 0, n ∈ s → P n<GOAL>(∀ n ∈ s, ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n ∈ s, ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<GOAL>s ∈ memberSubfamily a 𝒜 ↔ insert a s ∈ 𝒜 ∧ a ∉ s
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<GOAL>(∃ a_1, (a_1 ∈ 𝒜 ∧ a ∈ a_1) ∧ a_1.erase a = s) ↔ insert a s ∈ 𝒜 ∧ a ∉ s
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<GOAL>(∃ a_1, (a_1 ∈ 𝒜 ∧ a ∈ a_1) ∧ a_1.erase a = s) → insert a s ∈ 𝒜 ∧ a ∉ s
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>a : α<VAR>s : Finset α<VAR>hs1 : s ∈ 𝒜<VAR>hs2 : a ∈ s<GOAL>insert a (s.erase a) ∈ 𝒜 ∧ a ∉ s.erase a
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>a : α<VAR>s : Finset α<VAR>hs1 : s ∈ 𝒜<VAR>hs2 : a ∈ s<GOAL>s ∈ 𝒜 ∧ a ∉ s.erase a
<VAR>n : ℕ<GOAL>fib (2 * n + 1) = fib (n + 1) ^ 2 + fib n ^ 2
<VAR>n : ℕ<GOAL>fib n * fib n + fib (n + 1) * fib (n + 1) = fib (n + 1) ^ 2 + fib n ^ 2
<VAR>a✝ b✝ c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>a b : ℝ≥0∞<VAR>hr : a ≠ ⊤<VAR>hp : b ≠ ⊤<VAR>h : a ≤ b<GOAL>(min a b).toReal = min a.toReal b.toReal
<VAR>a✝ b✝ c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>a b : ℝ≥0∞<VAR>hr : a ≠ ⊤<VAR>hp : b ≠ ⊤<VAR>h : b ≤ a<GOAL>(min a b).toReal = min a.toReal b.toReal
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂✝ : Finset ι₂<VAR>w : ι → k<VAR>p : ι → P<VAR>b : P<VAR>s₁ s₂ : Finset ι<VAR>h : s₁ ⊆ s₂<GOAL>(s₁.weightedVSubOfPoint p b) w = (s₂.weightedVSubOfPoint p b) ((↑s₁).indicator w)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂✝ : Finset ι₂<VAR>w : ι → k<VAR>p : ι → P<VAR>b : P<VAR>s₁ s₂ : Finset ι<VAR>h : s₁ ⊆ s₂<GOAL>∑ i ∈ s₁, w i • (p i -ᵥ b) = ∑ i ∈ s₂, (↑s₁).indicator w i • (p i -ᵥ b)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>f✝ : α → β<VAR>s t : Set α<VAR>a : α<VAR>hs : s.PartiallyWellOrderedOn r<VAR>ht : t.PartiallyWellOrderedOn r<VAR>f : ℕ → α<VAR>hf : ∀ (n : ℕ), f n ∈ s ∪ t<GOAL>∃ m n, m < n ∧ r (f m) (f n)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>f✝ : α → β<VAR>s t : Set α<VAR>a : α<VAR>hs : s.PartiallyWellOrderedOn r<VAR>ht : t.PartiallyWellOrderedOn r<VAR>f : ℕ → α<VAR>hf : ∀ (n : ℕ), f n ∈ s ∪ t<VAR>g : ℕ ↪o ℕ<VAR>hgs : ∀ (n : ℕ), f (g n) ∈ s<GOAL>∃ m n, m < n ∧ r (f m) (f n)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>f✝ : α → β<VAR>s t : Set α<VAR>a : α<VAR>hs : s.PartiallyWellOrderedOn r<VAR>ht : t.PartiallyWellOrderedOn r<VAR>f : ℕ → α<VAR>hf : ∀ (n : ℕ), f n ∈ s ∪ t<VAR>g : ℕ ↪o ℕ<VAR>hgt : ∀ (n : ℕ), f (g n) ∈ t<GOAL>∃ m n, m < n ∧ r (f m) (f n)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>h : edist x y = 0<GOAL>edist x z ≤ edist y z
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>h : edist x y = 0<GOAL>edist y z ≤ edist x z
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝² : CommRing P<VAR>inst✝¹ : Algebra R P<VAR>loc : IsLocalization S P<VAR>inst✝ : NoZeroSMulDivisors R P<VAR>hS : 0 ∉ S<VAR>I : FractionalIdeal S P<VAR>hI : I.num = ⊥<GOAL>I = 0
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝² : CommRing P<VAR>inst✝¹ : Algebra R P<VAR>loc : IsLocalization S P<VAR>inst✝ : NoZeroSMulDivisors R P<VAR>hS : 0 ∉ S<VAR>I : FractionalIdeal S P<VAR>hI : I.num = ⊥<GOAL>↑I ≤ ⊥
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝² : CommRing P<VAR>inst✝¹ : Algebra R P<VAR>loc : IsLocalization S P<VAR>inst✝ : NoZeroSMulDivisors R P<VAR>hS : 0 ∉ S<VAR>I : FractionalIdeal S P<VAR>hI : I.num = ⊥<VAR>x : P<VAR>hx : x ∈ ↑I<GOAL>x ∈ ⊥
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝² : CommRing P<VAR>inst✝¹ : Algebra R P<VAR>loc : IsLocalization S P<VAR>inst✝ : NoZeroSMulDivisors R P<VAR>hS : 0 ∉ S<VAR>I : FractionalIdeal S P<VAR>hI : I.num = ⊥<VAR>x : P<VAR>hx : x ∈ ↑I<GOAL>↑I.den • x = 0
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝² : CommRing P<VAR>inst✝¹ : Algebra R P<VAR>loc : IsLocalization S P<VAR>inst✝ : NoZeroSMulDivisors R P<VAR>hS : 0 ∉ S<VAR>I : FractionalIdeal S P<VAR>hI : I.num = ⊥<VAR>x : P<VAR>hx : x ∈ ↑I<VAR>h_eq : I.den • ↑I = ⊥<GOAL>↑I.den • x = 0
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → R<VAR>u : R<GOAL>W'.negY (u • P) = u ^ 3 * W'.negY P
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → R<VAR>u : R<GOAL>-(u ^ 3 * P y) - W'.a₁ * (u ^ 2 * P x) * (u * P z) - W'.a₃ * (u * P z) ^ 3 = u ^ 3 * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁶ : MeasurableSpace X<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝ : SecondCountableTopology X<VAR>hf : LocallyIntegrableOn f s μ<GOAL>AEStronglyMeasurable f (μ.restrict s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁶ : MeasurableSpace X<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝ : SecondCountableTopology X<VAR>hf : LocallyIntegrableOn f s μ<VAR>u : ℕ → Set X<VAR>su : s ⊆ ⋃ n, u n<VAR>hu : ∀ (n : ℕ), IntegrableOn f (u n ∩ s) μ<GOAL>AEStronglyMeasurable f (μ.restrict s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁶ : MeasurableSpace X<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝ : SecondCountableTopology X<VAR>hf : LocallyIntegrableOn f s μ<VAR>u : ℕ → Set X<VAR>su : s ⊆ ⋃ n, u n<VAR>hu : ∀ (n : ℕ), IntegrableOn f (u n ∩ s) μ<VAR>this : s = ⋃ n, u n ∩ s<GOAL>AEStronglyMeasurable f (μ.restrict s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁶ : MeasurableSpace X<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝ : SecondCountableTopology X<VAR>hf : LocallyIntegrableOn f s μ<VAR>u : ℕ → Set X<VAR>su : s ⊆ ⋃ n, u n<VAR>hu : ∀ (n : ℕ), IntegrableOn f (u n ∩ s) μ<VAR>this : s = ⋃ n, u n ∩ s<GOAL>∀ (i : ℕ), AEStronglyMeasurable f (μ.restrict (u i ∩ s))
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>m m0 : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>μ : Measure α<VAR>f : α → E<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hf : f =ᶠ[ae (μ.restrict sᶜ)] 0<VAR>hm : m ≤ m0<GOAL>μ[s.indicator f|m] =ᶠ[ae μ] s.indicator (μ[f|m])
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>m m0 : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>μ : Measure α<VAR>f : α → E<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hf : f =ᶠ[ae (μ.restrict sᶜ)] 0<VAR>hm : m ≤ m0<VAR>hsf_zero : ∀ (g : α → E), g =ᶠ[ae (μ.restrict sᶜ)] 0 → s.indicator g =ᶠ[ae μ] g<GOAL>μ[s.indicator f|m] =ᶠ[ae μ] s.indicator (μ[f|m])
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>m m0 : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>μ : Measure α<VAR>f : α → E<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hf : f =ᶠ[ae (μ.restrict sᶜ)] 0<VAR>hm : m ≤ m0<VAR>hsf_zero : ∀ (g : α → E), g =ᶠ[ae (μ.restrict sᶜ)] 0 → s.indicator g =ᶠ[ae μ] g<GOAL>μ[f|m] =ᶠ[ae μ] μ[s.indicator f|m]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>I : Set ι<VAR>s : (i : ι) → Set (π i)<VAR>x : (i : ι) → π i<GOAL>(𝓝[I.pi s] x).NeBot ↔ ∀ i ∈ I, (𝓝[s i] x i).NeBot
<VAR>V : Type u_1<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>V₃ : Type u_4<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : SeminormedAddCommGroup V₁<VAR>inst✝¹ : SeminormedAddCommGroup V₂<VAR>inst✝ : SeminormedAddCommGroup V₃<VAR>f g : NormedAddGroupHom V₁ V₂<VAR>x y : V₁<GOAL>dist (f x) (f y) ≤ ↑⟨‖f‖, ⋯⟩ * dist x y
<VAR>V : Type u_1<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>V₃ : Type u_4<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : SeminormedAddCommGroup V₁<VAR>inst✝¹ : SeminormedAddCommGroup V₂<VAR>inst✝ : SeminormedAddCommGroup V₃<VAR>f g : NormedAddGroupHom V₁ V₂<VAR>x y : V₁<GOAL>‖f (x - y)‖ ≤ ↑⟨‖f‖, ⋯⟩ * ‖x - y‖
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>F : Jᵒᵖ ⥤ C<VAR>c : Cocone F.rightOp<VAR>hc : IsColimit c<VAR>s : Cone F<VAR>m : s.pt ⟶ (coneOfCoconeRightOp c).pt<VAR>w : ∀ (j : Jᵒᵖ), m ≫ (coneOfCoconeRightOp c).π.app j = s.π.app j<GOAL>m = (fun s => (hc.desc (coconeRightOpOfCone s)).unop) s
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>F : Jᵒᵖ ⥤ C<VAR>c : Cocone F.rightOp<VAR>hc : IsColimit c<VAR>s : Cone F<VAR>m : s.pt ⟶ (coneOfCoconeRightOp c).pt<VAR>w : ∀ (j : Jᵒᵖ), m ≫ (coneOfCoconeRightOp c).π.app j = s.π.app j<VAR>j : J<GOAL>(c.ι.app j ≫ m.op).unop = (c.ι.app j ≫ ((fun s => (hc.desc (coconeRightOpOfCone s)).unop) s).op).unop
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>f g : R[X]<VAR>ι : Type u_2<VAR>v : ι → R<VAR>s : Finset ι<VAR>hvs : Set.InjOn v ↑s<VAR>degree_f_lt : f.degree < ↑s.card<VAR>eval_f : ∀ i ∈ s, eval (v i) f = 0<GOAL>f = 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>n : ℕ<VAR>IH : ∀ (s : Seq α), (s.drop n).head = s.get? n<VAR>s : Seq α<GOAL>(s.drop (n + 1)).head = s.get? (n + 1)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>n : ℕ<VAR>IH : ∀ (s : Seq α), (s.drop n).head = s.get? n<VAR>s : Seq α<GOAL>(s.tail.drop n).head = s.tail.get? n
<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>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>f : MvPolynomial (Fin (n + 1)) R<VAR>i : ℕ<VAR>hi : ((finSuccEquiv R n) f).coeff i ≠ 0<GOAL>(((finSuccEquiv R n) f).coeff i).totalDegree + i ≤ f.totalDegree
<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>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>f : MvPolynomial (Fin (n + 1)) R<VAR>i : ℕ<VAR>hi : ((finSuccEquiv R n) f).coeff i ≠ 0<VAR>hf'_sup : (((finSuccEquiv R n) f).coeff i).support.Nonempty<GOAL>(((finSuccEquiv R n) f).coeff i).totalDegree + i ≤ f.totalDegree
<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>s : σ✝ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>f : MvPolynomial (Fin (n + 1)) R<VAR>i : ℕ<VAR>hi : ((finSuccEquiv R n) f).coeff i ≠ 0<VAR>hf'_sup : (((finSuccEquiv R n) f).coeff i).support.Nonempty<VAR>σ : Fin n →₀ ℕ<VAR>hσ1 : σ ∈ (((finSuccEquiv R n) f).coeff i).support<VAR>hσ2 : ((((finSuccEquiv R n) f).coeff i).support.sup fun s => s.sum fun x e => e) = σ.sum fun x e => e<GOAL>(((finSuccEquiv R n) f).coeff i).totalDegree + i ≤ f.totalDegree
<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>s : σ✝ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>f : MvPolynomial (Fin (n + 1)) R<VAR>i : ℕ<VAR>hi : ((finSuccEquiv R n) f).coeff i ≠ 0<VAR>hf'_sup : (((finSuccEquiv R n) f).coeff i).support.Nonempty<VAR>σ : Fin n →₀ ℕ<VAR>hσ1 : σ ∈ (((finSuccEquiv R n) f).coeff i).support<VAR>hσ2 : ((((finSuccEquiv R n) f).coeff i).support.sup fun s => s.sum fun x e => e) = σ.sum fun x e => e<VAR>σ' : Fin (n + 1) →₀ ℕ := cons i σ<GOAL>(((finSuccEquiv R n) f).coeff i).totalDegree + i ≤ f.totalDegree
<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>s : σ✝ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>f : MvPolynomial (Fin (n + 1)) R<VAR>i : ℕ<VAR>hi : ((finSuccEquiv R n) f).coeff i ≠ 0<VAR>hf'_sup : (((finSuccEquiv R n) f).coeff i).support.Nonempty<VAR>σ : Fin n →₀ ℕ<VAR>hσ1 : σ ∈ (((finSuccEquiv R n) f).coeff i).support<VAR>hσ2 : ((((finSuccEquiv R n) f).coeff i).support.sup fun s => s.sum fun x e => e) = σ.sum fun x e => e<VAR>σ' : Fin (n + 1) →₀ ℕ := cons i σ<GOAL>(((finSuccEquiv R n) f).coeff i).totalDegree + i = σ'.sum fun x e => e
<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>s : σ✝ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>f : MvPolynomial (Fin (n + 1)) R<VAR>i : ℕ<VAR>hi : ((finSuccEquiv R n) f).coeff i ≠ 0<VAR>hf'_sup : (((finSuccEquiv R n) f).coeff i).support.Nonempty<VAR>σ : Fin n →₀ ℕ<VAR>hσ1 : σ ∈ (((finSuccEquiv R n) f).coeff i).support<VAR>hσ2 : ((((finSuccEquiv R n) f).coeff i).support.sup fun s => s.sum fun x e => e) = σ.sum fun x e => e<VAR>σ' : Fin (n + 1) →₀ ℕ := cons i σ<GOAL>σ' ∈ f.support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β → γ<VAR>s✝ : Set α<VAR>t✝ : Set β<VAR>s : ι → Set α<VAR>t : Set β<GOAL>image2 f (⋂ i, s i) t ⊆ ⋂ i, image2 f (s i) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β → γ<VAR>s✝ : Set α<VAR>t✝ : Set β<VAR>s : ι → Set α<VAR>t : Set β<GOAL>∀ (x : α), (∀ (i : ι), x ∈ s i) → ∀ y ∈ t, ∀ (i : ι), f x y ∈ image2 f (s i) t
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝ : CommMonoid β<VAR>s : Finset α<VAR>f : Finset α → β<GOAL>∏ t ∈ s.powerset, f t = ∏ j ∈ range (s.card + 1), ∏ t ∈ powersetCard j s, f t
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>x✝ : L ≃ₐ[K] L<GOAL>x✝ ∈ ⊤.fixingSubgroup ↔ x✝ ∈ ⊥
<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✝² : SeminormedRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : SMul 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>x✝ y : E<VAR>r : ℝ<VAR>x : E<VAR>hr : 0 < r<GOAL>ball 0 x r = univ
<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✝² : SeminormedRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : SMul 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>x✝ y : E<VAR>r : ℝ<VAR>x : E<VAR>hr : 0 < r<GOAL>∀ (x_1 : E), x_1 ∈ {y | 0 (y - x) < r}
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<GOAL>eLpNorm' f 0 μ = 1
<VAR>a b : Cardinal.{u}<VAR>n m : ℕ<VAR>k : Cardinal.{u_1}<VAR>hk : ↑m = ↑n * k<GOAL>n ∣ m
<VAR>a b : Cardinal.{u}<VAR>n m : ℕ<VAR>k : Cardinal.{u_1}<VAR>hk : ↑m = ↑n * k<VAR>this : ↑m < ℵ₀<GOAL>n ∣ m
<VAR>a b : Cardinal.{u}<VAR>n m : ℕ<VAR>k : Cardinal.{u_1}<VAR>hk : ↑m = ↑n * k<VAR>this : ↑n = 0 ∨ k = 0 ∨ ↑n < ℵ₀ ∧ k < ℵ₀<GOAL>n ∣ m
<VAR>a b : Cardinal.{u}<VAR>n m : ℕ<VAR>k : Cardinal.{u_1}<VAR>hk : ↑m = ↑n * k<VAR>h : ↑n = 0<GOAL>n ∣ m
<VAR>a b : Cardinal.{u}<VAR>n m : ℕ<VAR>k : Cardinal.{u_1}<VAR>hk : ↑m = ↑n * k<VAR>h : k = 0<GOAL>n ∣ m
<VAR>a b : Cardinal.{u}<VAR>n m : ℕ<VAR>k : Cardinal.{u_1}<VAR>hk : ↑m = ↑n * k<VAR>hk' : k < ℵ₀<GOAL>n ∣ m
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁷ : SeminormedAddCommGroup E<VAR>inst✝¹⁶ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁵ : SeminormedAddCommGroup F<VAR>inst✝¹⁴ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹³ : SeminormedAddCommGroup G<VAR>inst✝¹² : SeminormedAddCommGroup Gₗ<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁹ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁶ : NormedSpace 𝕜₂ F<VAR>inst✝⁵ : NormedSpace 𝕜 Fₗ<VAR>inst✝⁴ : NormedSpace 𝕜₃ G<VAR>inst✝³ : NormedSpace 𝕜 Gₗ<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝¹ : FunLike 𝓕 E F<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<VAR>r : ℝ≥0<VAR>hr : r < ‖f‖₊<GOAL>∃ x, r * ‖x‖₊ < ‖f x‖₊
<VAR>n k : ℕ<VAR>h1 : MinFacHelper n k<VAR>h2 : (k * k).ble n = false<GOAL>IsNat n.minFac n
<VAR>n k : ℕ<VAR>h1 : MinFacHelper n k<VAR>h2 : (k * k).ble n = false<GOAL>Nat.Prime n
<VAR>n k : ℕ<VAR>h1 : MinFacHelper n k<VAR>h2 : (k * k).ble n = false<GOAL>2 ≤ n ∧ ∀ (m : ℕ), 2 ≤ m → m ≤ n.sqrt → ¬m ∣ n
<VAR>n k : ℕ<VAR>h1 : MinFacHelper n k<VAR>h2 : (k * k).ble n = false<VAR>m : ℕ<VAR>hm : 2 ≤ m<VAR>hmn : m ≤ n.sqrt<VAR>h2mn : m ∣ n<GOAL>False
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S : Subgroupoid C<VAR>D : Set C<VAR>x✝² x✝¹ : C<VAR>x✝ : x✝² ⟶ x✝¹<GOAL>x✝ ∈ (full univ).arrows x✝² x✝¹ ↔ x✝ ∈ ⊤.arrows x✝² x✝¹
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : AddCommMonoid A<VAR>inst✝¹ : Module R A<VAR>inst✝ : Module R[X] A<VAR>D₁ D₂ : Derivation R R[X] A<VAR>h : D₁ X = D₂ X<VAR>f : R[X]<GOAL>f ∈ ↑(Algebra.adjoin R {X})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>h : ∃ᶠ (x : α) in l, ‖f' x‖ ≠ 0<VAR>ho : f' =o[l] f'<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>h : ∃ᶠ (x : α) in l, ‖f' x‖ ≠ 0<VAR>ho : f' =o[l] f'<VAR>x : α<VAR>hle : ‖f' x‖ ≤ 1 / 2 * ‖f' x‖<VAR>hne : ‖f' x‖ ≠ 0<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>h : ∃ᶠ (x : α) in l, ‖f' x‖ ≠ 0<VAR>ho : f' =o[l] f'<VAR>x : α<VAR>hle : ‖f' x‖ ≤ ‖f' x‖ / 2<VAR>hne : ‖f' x‖ ≠ 0<GOAL>False
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G✝ : Type u_3<VAR>H : Type u_4<VAR>A✝ : Type u_5<VAR>B✝ : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>γ : Type u_9<VAR>δ : Type u_10<VAR>inst✝⁶ : Monoid M<VAR>inst✝⁵ : MulAction M α<VAR>A : Type u_11<VAR>B : Type u_12<VAR>G : Type u_13<VAR>inst✝⁴ : CommMonoid G<VAR>inst✝³ : SMul A G<VAR>inst✝² : SMul B G<VAR>inst✝¹ : IsScalarTower A G G<VAR>inst✝ : IsScalarTower B G G<VAR>r : A<VAR>s : B<VAR>x : G<GOAL>r • s • x = s • r • x
<VAR>α : Type u_1<VAR>inst✝ : Monoid α<VAR>s : Submonoid α<VAR>a : α<VAR>ha : op a • ↑s = ↑s<GOAL>a ∈ s
<VAR>α : Type u_1<VAR>inst✝ : Monoid α<VAR>s : Submonoid α<VAR>a : α<VAR>ha : op a • ↑s = ↑s<GOAL>a ∈ op a • ↑s