ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra F K<VAR>inst✝¹ : Algebra F L<VAR>inst✝ : Algebra.IsAlgebraic F K<VAR>splits : ∀ (x : K), Splits (algebraMap F L) (minpoly F x)<VAR>x : ↥(⨆ f, f.fieldRange)<VAR>x✝ : x ∈ ⊤<VAR>f : K →ₐ[F] L<GOAL>f.fieldRange ≤ ⨆ i, IntermediateField.map (⨆ f, f.fieldRange).val i.fieldRange
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra F K<VAR>inst✝¹ : Algebra F L<VAR>inst✝ : Algebra.IsAlgebraic F K<VAR>splits : ∀ (x : K), Splits (algebraMap F L) (minpoly F x)<VAR>x : ↥(⨆ f, f.fieldRange)<VAR>x✝ : x ∈ ⊤<VAR>f : K →ₐ[F] L<GOAL>f.fieldRange ≤ IntermediateField.map (⨆ f, f.fieldRange).val (f.codRestrict (⨆ f, f.fieldRange).toSubalgebra ⋯).fieldRange
<VAR>U : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁴ : Quiver U<VAR>inst✝³ : Quiver V<VAR>inst✝² : Quiver W<VAR>V' : Type u_4<VAR>inst✝¹ : Quiver V'<VAR>inst✝ : HasReverse V'<VAR>Φ : Symmetrify V ⥤q V'<VAR>hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)<GOAL>Φ = lift (of ⋙q Φ)
<VAR>U : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁴ : Quiver U<VAR>inst✝³ : Quiver V<VAR>inst✝² : Quiver W<VAR>V' : Type u_4<VAR>inst✝¹ : Quiver V'<VAR>inst✝ : HasReverse V'<VAR>Φ : Symmetrify V ⥤q V'<VAR>hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)<GOAL>∀ (X : Symmetrify V), Φ.obj X = (lift (of ⋙q Φ)).obj X
<VAR>U : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁴ : Quiver U<VAR>inst✝³ : Quiver V<VAR>inst✝² : Quiver W<VAR>V' : Type u_4<VAR>inst✝¹ : Quiver V'<VAR>inst✝ : HasReverse V'<VAR>Φ : Symmetrify V ⥤q V'<VAR>hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)<GOAL>∀ (X Y : Symmetrify V) (f : X ⟶ Y), Φ.map f = Eq.recOn ⋯ (Eq.recOn ⋯ ((lift (of ⋙q Φ)).map f))
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V'<VAR>f : V ≃ₗᵢ[ℝ] V'<GOAL>((map (Fin 2) f.toLinearEquiv) o).oangle x y = o.oangle (f.symm x) (f.symm y)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e✝ : I → R<VAR>he✝ : OrthogonalIdempotents e✝<VAR>inst✝ : Finite I<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>e : I → S<VAR>he : OrthogonalIdempotents e<VAR>he' : ∀ (i : I), e i ∈ f.range<GOAL>∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e✝ : I → R<VAR>he✝ : OrthogonalIdempotents e✝<VAR>inst✝ : Finite I<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>e : I → S<VAR>he : OrthogonalIdempotents e<VAR>he' : ∀ (i : I), e i ∈ f.range<VAR>val✝ : Fintype I<GOAL>∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e✝ : I → R<VAR>he✝ : OrthogonalIdempotents e✝<VAR>inst✝ : Finite I<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>e : I → S<VAR>he : OrthogonalIdempotents e<VAR>he' : ∀ (i : I), e i ∈ f.range<VAR>val✝ : Fintype I<VAR>e' : Fin (Fintype.card I) → R<VAR>h₁ : OrthogonalIdempotents e'<VAR>h₂ : ⇑f ∘ e' = e ∘ ⇑(Fintype.equivFin I).symm.toEmbedding<GOAL>∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
<VAR>a x✝ y : ℂ<VAR>x : ℝ<GOAL>angle (cexp (↑x * I)) 1 = |toIocMod Real.two_pi_pos (-π) x|
<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>ι : Type u_5<VAR>s : Finset ι<VAR>f : ι → NormedAddGroupHom V₁ V₂<VAR>v : V₁<GOAL>(∑ i ∈ s, f i) v = ∑ i ∈ s, (f i) v
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>p : α → Prop<GOAL>IsEmpty (Subtype p) ↔ ∀ (x : α), ¬p x
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hb : b ≠ 0<GOAL>0 < a / b ↔ b ≤ a
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>a : α<VAR>l : List α<GOAL>(a :: l).reverse = l.reverse.concat a
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f p : R[X]<VAR>a✝ : Nontrivial R<GOAL>(p * X).reverse = p.reverse
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>a✝ : Nontrivial R<GOAL>(0 * X).reverse = reverse 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f p : R[X]<VAR>a✝ : Nontrivial R<VAR>hp : p ≠ 0<GOAL>(p * X).reverse = p.reverse
<VAR>L : Language<VAR>ι : Type v<VAR>inst✝² : Preorder ι<VAR>G : ι → Type w<VAR>inst✝¹ : (i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>G' : ℕ → Type w<VAR>inst✝ : (i : ℕ) → L.Structure (G' i)<VAR>f' : (n : ℕ) → G' n ↪[L] G' (n + 1)<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>⇑(natLERec f' m n h) = fun a => Nat.leRecOn h (fun k => ⇑(f' k)) a
<VAR>L : Language<VAR>ι : Type v<VAR>inst✝² : Preorder ι<VAR>G : ι → Type w<VAR>inst✝¹ : (i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>G' : ℕ → Type w<VAR>inst✝ : (i : ℕ) → L.Structure (G' i)<VAR>f' : (n : ℕ) → G' n ↪[L] G' (n + 1)<VAR>m k : ℕ<VAR>h : m ≤ m + k<GOAL>⇑(natLERec f' m (m + k) h) = fun a => Nat.leRecOn h (fun k => ⇑(f' k)) a
<VAR>F : Type u_1<VAR>inst✝ : Field F<VAR>S : Set F<VAR>p : F<VAR>hp : p ∈ Ring.closure S<VAR>q : F<VAR>hq : q ∈ Ring.closure S<VAR>ha : p / q ∈ closure S<VAR>r : F<VAR>hr : r ∈ Ring.closure S<VAR>s : F<VAR>hs : s ∈ Ring.closure S<VAR>hb : r / s ∈ closure S<VAR>hq0 : ¬q = 0<VAR>hs0 : ¬s = 0<GOAL>p / q + r / s ∈ closure S
<VAR>F : Type u_1<VAR>inst✝ : Field F<VAR>S : Set F<VAR>p : F<VAR>hp : p ∈ Ring.closure S<VAR>q : F<VAR>hq : q ∈ Ring.closure S<GOAL>-(p / q) ∈ closure S
<VAR>F : Type u_1<VAR>inst✝ : Field F<VAR>S : Set F<VAR>p : F<VAR>hp : p ∈ Ring.closure S<VAR>q : F<VAR>hq : q ∈ Ring.closure S<GOAL>(p / q)⁻¹ ∈ closure S
<VAR>a b k m n p : ℕ<VAR>hk : k ≠ 0<VAR>hp : Prime p<GOAL>(p ^ k).primeFactors = {p}
<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✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p✝ : Seminorm 𝕜 E<VAR>A B : Set E<VAR>a✝ : 𝕜<VAR>r✝ : ℝ<VAR>x : E<VAR>p : Seminorm 𝕜 E<VAR>y : E<VAR>r : ℝ<VAR>a : 𝕜<VAR>ha : a ≠ 0<VAR>x✝ : E<GOAL>x✝ ∈ (fun x => a • x) ⁻¹' p.ball y r ↔ x✝ ∈ p.ball (a⁻¹ • y) (r / ‖a‖)
<VAR>μ : YoungDiagram<VAR>i : ℕ<VAR>h : i < μ.rowLens.length<GOAL>μ.rowLens[i] = μ.rowLen i
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : DecidableEq (Associates α)<VAR>inst✝ : (p : Associates α) → Decidable (Irreducible p)<VAR>p : Associates α<VAR>hp : Irreducible p<GOAL>p.count 0 = 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f✝ g : Ultrafilter α<VAR>s t : Set α<VAR>p q : α → Prop<VAR>f : Ultrafilter γ<VAR>m : α → β<VAR>n : β → γ<VAR>inj₀ : Injective n<VAR>large₀ : range n ∈ f<VAR>inj₁ : Injective m<VAR>large₁ : range m ∈ f.comap inj₀ large₀<VAR>inj₂ : optParam (Injective (n ∘ m)) ⋯<GOAL>range (n ∘ m) ∈ f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f✝ g : Ultrafilter α<VAR>s t : Set α<VAR>p q : α → Prop<VAR>f : Ultrafilter γ<VAR>m : α → β<VAR>n : β → γ<VAR>inj₀ : Injective n<VAR>large₀ : range n ∈ f<VAR>inj₁ : Injective m<VAR>large₁ : range m ∈ f.comap inj₀ large₀<VAR>inj₂ : optParam (Injective (n ∘ m)) ⋯<GOAL>n '' range m ∈ f
<VAR>α : Type u_1<VAR>inst✝¹ : Finite α<VAR>inst✝ : DecidableEq α<VAR>f : Perm α<VAR>hf : f.IsCycle<GOAL>∃! s, (↑s).formPerm ⋯ = f
<VAR>α : Type u_1<VAR>inst✝¹ : Finite α<VAR>inst✝ : DecidableEq α<VAR>f : Perm α<VAR>hf : f.IsCycle<VAR>s : Cycle α<VAR>hn : s.Nodup<VAR>hs : (↑⟨s, hn⟩).formPerm ⋯ = f<VAR>hs' : ∀ (y : { s // s.Nodup }), (fun s => (↑s).formPerm ⋯ = f) y → y = ⟨s, hn⟩<GOAL>∃! s, (↑s).formPerm ⋯ = f
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : DecidableEq L<VAR>inst✝⁷ : Algebra R K<VAR>inst✝⁶ : IsFractionRing R K<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra R L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsDedekindDomain R<VAR>b✝ : ClassGroup R<VAR>I : (FractionalIdeal R⁰ (FractionRing R))ˣ<GOAL>∃ a, mk0 a = Quot.mk Setoid.r I
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : DecidableEq L<VAR>inst✝⁷ : Algebra R K<VAR>inst✝⁶ : IsFractionRing R K<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra R L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsDedekindDomain R<VAR>b✝ : ClassGroup R<VAR>I : (FractionalIdeal R⁰ (FractionRing R))ˣ<GOAL>mk0 ⟨integralRep ↑I, ⋯⟩ = Quot.mk Setoid.r I
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>m : α → β → γ<VAR>f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>h h₁ h₂ : Filter γ<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>u : Set γ<VAR>v : Set δ<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>inst✝ : g.NeBot<GOAL>map₂ (fun x x_1 => x) f g = f
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>H : IsCoprime (x * y) z<VAR>a b : R<VAR>h : a * (x * y) + b * z = 1<GOAL>a * y * x + b * z = 1
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasBinaryBiproducts C<VAR>X₁ X₂ X₃ : CochainComplex C ℤ<VAR>f : X₁ ⟶ X₂<VAR>g : X₂ ⟶ X₃<VAR>n : ℤ<GOAL>(hom f g ≫ inv f g).f n = (𝟙 (mappingCone g)).f n
<VAR>a✝ b n : ℕ<VAR>hn : n ≠ 0<VAR>a : ℕ<GOAL>n.ceilRoot (a ^ n) = a
<VAR>a✝ b n : ℕ<VAR>hn : n ≠ 0<VAR>a : ℕ<GOAL>(if a = 0 then 0 else a.factorization.prod fun x x_1 => x ^ x_1) = a
<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>f₁ f₂ : α → E'<VAR>g₁ g₂ : α → F'<VAR>h₁ : IsBigOWith c₁ l f₁ g<VAR>h₂ : IsBigOWith c₂ l f₂ g<GOAL>IsBigOWith (c₁ + c₂) l (fun x => f₁ x + f₂ x) g
<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>f₁ f₂ : α → E'<VAR>g₁ g₂ : α → F'<VAR>h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g x‖<VAR>h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g x‖<GOAL>∀ᶠ (x : α) in l, ‖f₁ x + f₂ x‖ ≤ (c₁ + c₂) * ‖g x‖
<VAR>G : Type u<VAR>M : Type v<VAR>α : Type w<VAR>s : Set α<VAR>m : MeasurableSpace α<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : MulAction G α<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : MeasurableSMul G α<VAR>c : G<VAR>μ : Measure α<VAR>inst✝³ : SMulInvariantMeasure G α μ<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : ContinuousConstSMul G α<VAR>inst✝ : MulAction.IsMinimal G α<VAR>K U : Set α<VAR>hU : IsOpen U<VAR>hne : U.Nonempty<VAR>hμU : μ U ≠ ⊤<VAR>x : α<VAR>g : G<VAR>hg : g • x ∈ U<GOAL>μ ((fun x => g • x) ⁻¹' U) ≠ ⊤
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>ι : Sort u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : M →* N<VAR>g : α → M<VAR>h : (mulSupport (g ∘ PLift.down)).Finite<GOAL>f (∏ᶠ (x : α), g x) = ∏ᶠ (x : α), f (g x)
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>ι : Sort u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : M →* N<VAR>g : α → M<VAR>h : (mulSupport (g ∘ PLift.down)).Finite<GOAL>mulSupport ((fun x => f (g x)) ∘ PLift.down) ⊆ ↑h.toFinset
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>ι : Sort u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : M →* N<VAR>g : α → M<VAR>h : (mulSupport (g ∘ PLift.down)).Finite<GOAL>mulSupport ((fun x => f (g x)) ∘ PLift.down) ⊆ mulSupport (g ∘ PLift.down)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f g : R<GOAL>zeroLocus {f} ⊆ zeroLocus {g} ↔ g ∈ (Ideal.span {f}).radical
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : OrderedCommMonoid β<VAR>f : α → β<VAR>p : α → Prop<VAR>h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b<VAR>hp_mul : ∀ (a b : α), p a → p b → p (a * b)<GOAL>∀ (s : Multiset α), s ≠ ∅ → (∀ a ∈ s, p a) → f s.prod ≤ (map f s).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : OrderedCommMonoid β<VAR>f : α → β<VAR>p : α → Prop<VAR>h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b<VAR>hp_mul : ∀ (a b : α), p a → p b → p (a * b)<GOAL>0 ≠ ∅ → (∀ a ∈ 0, p a) → f (prod 0) ≤ (map f 0).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : OrderedCommMonoid β<VAR>f : α → β<VAR>p : α → Prop<VAR>h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b<VAR>hp_mul : ∀ (a b : α), p a → p b → p (a * b)<GOAL>∀ (a : α) (s : Multiset α), (s ≠ ∅ → (∀ a ∈ s, p a) → f s.prod ≤ (map f s).prod) → a ::ₘ s ≠ ∅ → (∀ a_2 ∈ a ::ₘ s, p a_2) → f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : OrderedCommMonoid β<VAR>f : α → β<VAR>p : α → Prop<VAR>h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b<VAR>hp_mul : ∀ (a b : α), p a → p b → p (a * b)<VAR>a : α<VAR>s : Multiset α<VAR>hs : s ≠ ∅ → (∀ a ∈ s, p a) → f s.prod ≤ (map f s).prod<VAR>hsa_prop : ∀ a_1 ∈ a ::ₘ s, p a_1<GOAL>f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : OrderedCommMonoid β<VAR>f : α → β<VAR>p : α → Prop<VAR>h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b<VAR>hp_mul : ∀ (a b : α), p a → p b → p (a * b)<VAR>a : α<VAR>s : Multiset α<VAR>hs : s ≠ ∅ → (∀ a ∈ s, p a) → f s.prod ≤ (map f s).prod<VAR>hsa_prop : ∀ a_1 ∈ a ::ₘ s, p a_1<GOAL>f (a * s.prod) ≤ f a * (map f s).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : OrderedCommMonoid β<VAR>f : α → β<VAR>p : α → Prop<VAR>h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b<VAR>hp_mul : ∀ (a b : α), p a → p b → p (a * b)<VAR>a : α<VAR>s : Multiset α<VAR>hs : s ≠ ∅ → (∀ a ∈ s, p a) → f s.prod ≤ (map f s).prod<VAR>hsa_prop : ∀ a_1 ∈ a ::ₘ s, p a_1<VAR>hs_empty : ¬s = ∅<GOAL>f (a * s.prod) ≤ f a * (map f s).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : OrderedCommMonoid β<VAR>f : α → β<VAR>p : α → Prop<VAR>h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b<VAR>hp_mul : ∀ (a b : α), p a → p b → p (a * b)<VAR>a : α<VAR>s : Multiset α<VAR>hs : s ≠ ∅ → (∀ a ∈ s, p a) → f s.prod ≤ (map f s).prod<VAR>hsa_prop : ∀ a_1 ∈ a ::ₘ s, p a_1<VAR>hs_empty : ¬s = ∅<VAR>hsa_restrict : ∀ x ∈ s, p x<GOAL>f (a * s.prod) ≤ f a * (map f s).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : OrderedCommMonoid β<VAR>f : α → β<VAR>p : α → Prop<VAR>h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b<VAR>hp_mul : ∀ (a b : α), p a → p b → p (a * b)<VAR>a : α<VAR>s : Multiset α<VAR>hs : s ≠ ∅ → (∀ a ∈ s, p a) → f s.prod ≤ (map f s).prod<VAR>hsa_prop : ∀ a_1 ∈ a ::ₘ s, p a_1<VAR>hs_empty : ¬s = ∅<VAR>hsa_restrict : ∀ x ∈ s, p x<VAR>hp_sup : p s.prod<GOAL>f (a * s.prod) ≤ f a * (map f s).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : OrderedCommMonoid β<VAR>f : α → β<VAR>p : α → Prop<VAR>h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b<VAR>hp_mul : ∀ (a b : α), p a → p b → p (a * b)<VAR>a : α<VAR>s : Multiset α<VAR>hs : s ≠ ∅ → (∀ a ∈ s, p a) → f s.prod ≤ (map f s).prod<VAR>hsa_prop : ∀ a_1 ∈ a ::ₘ s, p a_1<VAR>hs_empty : ¬s = ∅<VAR>hsa_restrict : ∀ x ∈ s, p x<VAR>hp_sup : p s.prod<VAR>hp_a : p a<GOAL>f (a * s.prod) ≤ f a * (map f s).prod
<VAR>α : Type v<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>m : M<VAR>a : α<GOAL>period m a ∣ Monoid.exponent M
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s✝ t : Set α<VAR>a : α<VAR>hs : s✝.Finite<VAR>ht : t.Finite<VAR>s : Finset α<GOAL>s ⊂ ht.toFinset ↔ ↑s ⊂ t
<VAR>d✝ : ℤ<VAR>c d a b : ℕ<GOAL>Nonnegg c d (↑a) (-↑b) ↔ SqLe b c a d
<VAR>d✝ : ℤ<VAR>c d a b : ℕ<GOAL>Nonnegg d c (-↑b) ↑a ↔ SqLe b c a d
<VAR>a b : ℤ<VAR>H1 : 0 ≤ a<VAR>H2✝ : a < |b|<VAR>n : ℕ<VAR>H2 : a < ↑-[n+1].natAbs<GOAL>-(a / -[n+1]) = -0
<VAR>a b : ℤ<VAR>H1 : 0 ≤ a<VAR>H2✝ : a < |b|<VAR>n : ℕ<VAR>H2 : a < ↑-[n+1].natAbs<GOAL>a / - -[n+1] = -0
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>completedHurwitzZetaEven₀ a (1 - s) = completedCosZeta₀ a s
<VAR>g : SL(2, ℝ)<VAR>hc : ↑↑g 1 0 = 0<GOAL>∃ u v, (fun x => g • x) = (fun x => v +ᵥ x) ∘ fun x => u • x
<VAR>a b : ℝ<VAR>ha : a ≠ 0<VAR>hc : ↑↑⟨!![a, b; 0, a⁻¹], ⋯⟩ 1 0 = 0<GOAL>∃ u v, (fun x => ⟨!![a, b; 0, a⁻¹], ⋯⟩ • x) = (fun x => v +ᵥ x) ∘ fun x => u • x
<VAR>a b : ℝ<VAR>ha : a ≠ 0<VAR>hc : ↑↑⟨!![a, b; 0, a⁻¹], ⋯⟩ 1 0 = 0<GOAL>(fun x => ⟨!![a, b; 0, a⁻¹], ⋯⟩ • x) = (fun x => b * a +ᵥ x) ∘ fun x => ⟨a * a, ⋯⟩ • x
<VAR>a b : ℝ<VAR>ha : a ≠ 0<VAR>hc : ↑↑⟨!![a, b; 0, a⁻¹], ⋯⟩ 1 0 = 0<VAR>z : ℂ<VAR>hz : 0 < z.im<GOAL>↑(⟨!![a, b; 0, a⁻¹], ⋯⟩ • ⟨z, hz⟩) = ↑(((fun x => b * a +ᵥ x) ∘ fun x => ⟨a * a, ⋯⟩ • x) ⟨z, hz⟩)
<VAR>a b : ℝ<VAR>ha : a ≠ 0<VAR>hc : ↑↑⟨!![a, b; 0, a⁻¹], ⋯⟩ 1 0 = 0<VAR>z : ℂ<VAR>hz : 0 < z.im<GOAL>↑a * z * ↑a + ↑b * ↑a = ↑b * ↑a + ↑a * ↑a * z
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<VAR>b a : α<GOAL>some (b, s) ∈ (cons b s).destruct
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b c d : R<VAR>n m : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>a : R<GOAL>(p - C a).natDegree = p.natDegree
<VAR>q✝ q : ℚ<VAR>n : ℕ<GOAL>q.den ^ n ≠ 0
<VAR>q✝ q : ℚ<VAR>n : ℕ<GOAL>(q.num ^ n).natAbs.Coprime (q.den ^ n)
<VAR>q✝ q : ℚ<VAR>n : ℕ<GOAL>(q.num.natAbs ^ n).Coprime (q.den ^ n)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>b : α<VAR>l : List α<VAR>a : α<VAR>h : a ∈ (b :: l).head?<GOAL>a :: (b :: l).tail = b :: l
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>b : α<VAR>l : List α<VAR>a : α<VAR>h : b = a<GOAL>a :: (b :: l).tail = b :: l
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x y : G<VAR>n m : ℕ<VAR>hn : 0 < n<VAR>h : x ^ n = 1<GOAL>IsPeriodicPt (fun x_1 => x * x_1) n 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>μ : Measure α<VAR>ν : Measure β<VAR>f : α → γ<VAR>g : β → γ<VAR>h : IdentDistrib f g μ ν<VAR>p : γ → Prop<VAR>pmeas : MeasurableSet {x | p x}<VAR>hp : ∀ᵐ (x : α) ∂μ, p (f x)<GOAL>∀ᵐ (x : β) ∂ν, p (g x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>μ : Measure α<VAR>ν : Measure β<VAR>f : α → γ<VAR>g : β → γ<VAR>h : IdentDistrib f g μ ν<VAR>p : γ → Prop<VAR>pmeas : MeasurableSet {x | p x}<VAR>hp : ∀ᵐ (x : α) ∂μ, p (f x)<GOAL>∀ᵐ (y : γ) ∂Measure.map g ν, p y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>μ : Measure α<VAR>ν : Measure β<VAR>f : α → γ<VAR>g : β → γ<VAR>h : IdentDistrib f g μ ν<VAR>p : γ → Prop<VAR>pmeas : MeasurableSet {x | p x}<VAR>hp : ∀ᵐ (x : α) ∂μ, p (f x)<GOAL>∀ᵐ (y : γ) ∂Measure.map f μ, p y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t s : Set α<GOAL>Nat.card ↑s = s.ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t s : Set α<VAR>h : s.Finite<GOAL>Nat.card ↑s = s.ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t s : Set α<VAR>h : s.Infinite<GOAL>Nat.card ↑s = s.ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t s : Set α<VAR>h : s.Infinite<VAR>this : Infinite ↑s<GOAL>Nat.card ↑s = s.ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>R : Type u_5<VAR>inst✝¹ : CancelCommMonoidWithZero R<VAR>inst✝ : Unique Rˣ<VAR>p₁ p₂ : R<VAR>k₁ k₂ : ℕ<VAR>hp₁ : Prime p₁<VAR>hp₂ : Prime p₂<VAR>hk₁ : 0 < k₂<VAR>h : p₁ ^ k₁ = p₂ ^ k₂<GOAL>p₁ = p₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>R : Type u_5<VAR>inst✝¹ : CancelCommMonoidWithZero R<VAR>inst✝ : Unique Rˣ<VAR>p₁ p₂ : R<VAR>k₁ k₂ : ℕ<VAR>hp₁ : Prime p₁<VAR>hp₂ : Prime p₂<VAR>hk₁ : 0 < k₂<VAR>h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂<GOAL>p₁ ~ᵤ p₂
<VAR>z x✝ y x p : ℝ<VAR>h : x ≠ 0 ∨ 1 ≤ p<GOAL>HasDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x
<VAR>z x✝ y x p : ℝ<VAR>h : x ≠ 0 ∨ 1 ≤ p<VAR>hx : x ≠ 0<GOAL>HasDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x
<VAR>z x y p : ℝ<VAR>h : 0 ≠ 0 ∨ 1 ≤ p<GOAL>HasDerivAt (fun x => x ^ p) (p * 0 ^ (p - 1)) 0
<VAR>z x y p : ℝ<VAR>h : 1 ≤ p<GOAL>HasDerivAt (fun x => x ^ p) (p * 0 ^ (p - 1)) 0
<VAR>z x y p : ℝ<VAR>h : 1 ≤ p<GOAL>ContinuousAt (fun x => x ^ p) 0
<VAR>z x y p : ℝ<VAR>h : 1 ≤ p<GOAL>ContinuousAt (fun x => p * x ^ (p - 1)) 0
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι → Type u_4<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : (i : ι) → PseudoEMetricSpace (β i)<VAR>f g : PiLp p β<GOAL>edist f g = edist g f
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι → Type u_4<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : (i : ι) → PseudoEMetricSpace (β i)<VAR>f g : PiLp 0 β<GOAL>edist f g = edist g f
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι → Type u_4<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : (i : ι) → PseudoEMetricSpace (β i)<VAR>f g : PiLp ⊤ β<GOAL>edist f g = edist g f
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι → Type u_4<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : (i : ι) → PseudoEMetricSpace (β i)<VAR>f g : PiLp p β<VAR>h : 0 < p.toReal<GOAL>edist f g = edist g f
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>n : ℕ<GOAL>rdropWhile p l <+: l
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>n : ℕ<GOAL>dropWhile p l.reverse <:+ l.reverse
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E✝ : Type u_3<VAR>E : Type u_4<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>p q : Submodule ℝ E<VAR>hpq : IsCompl p q<VAR>hpc : IsPathConnected {0}ᶜ<GOAL>IsPathConnected (↑q)ᶜ