ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r✝ R r : ℝ≥0<VAR>_h0 : 0 < r<VAR>hr : ↑‖x‖₊ + ↑r < p.radius<VAR>hr' : ↑‖x‖₊ < p.radius<VAR>this : ∀ (k : ℕ), ‖p.changeOrigin x k‖₊ * r ^ k ≤ (∑' (s : (l : ℕ) × { s // s.card = l }), ‖p (k + s.fst)‖₊ * ‖x‖₊ ^ s.fst) * r ^ k<GOAL>Summable fun b => (∑' (s : (l : ℕ) × { s // s.card = l }), ‖p (b + s.fst)‖₊ * ‖x‖₊ ^ s.fst) * r ^ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>δ₁ : Type u_5<VAR>δ₂ : Type u_6<VAR>φ₁ : δ₁ → α<VAR>φ₂ : δ₂ → α<VAR>𝔗₁ : Set (Set δ₁)<VAR>𝔗₂ : Set (Set δ₂)<VAR>h_image₁ : MapsTo (fun x => φ₁ '' x) 𝔗₁ 𝔖<VAR>h_image₂ : MapsTo (fun x => φ₂ '' x) 𝔗₂ 𝔖<VAR>h_preimage₁ : MapsTo (fun x => φ₁ ⁻¹' x) 𝔖 𝔗₁<VAR>h_preimage₂ : MapsTo (fun x => φ₂ ⁻¹' x) 𝔖 𝔗₂<VAR>h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂<VAR>ψ₁ : (S : Set α) → ↑(φ₁ ⁻¹' S) → ↑S := fun S => S.restrictPreimage φ₁<VAR>ψ₂ : (S : Set α) → ↑(φ₂ ⁻¹' S) → ↑S := fun S => S.restrictPreimage φ₂<VAR>this : ∀ S ∈ 𝔖, UniformFun.uniformSpace (↑S) β = UniformSpace.comap (fun x => x ∘ ψ₁ S) (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S)) β) ⊓ UniformSpace.comap (fun x => x ∘ ψ₂ S) (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S)) β)<GOAL>uniformSpace α β 𝔖 = UniformSpace.comap (⇑(ofFun 𝔗₁) ∘ (fun x => x ∘ φ₁) ∘ ⇑(toFun 𝔖)) (uniformSpace δ₁ β 𝔗₁) ⊓ UniformSpace.comap (⇑(ofFun 𝔗₂) ∘ (fun x => x ∘ φ₂) ∘ ⇑(toFun 𝔖)) (uniformSpace δ₂ β 𝔗₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>δ₁ : Type u_5<VAR>δ₂ : Type u_6<VAR>φ₁ : δ₁ → α<VAR>φ₂ : δ₂ → α<VAR>𝔗₁ : Set (Set δ₁)<VAR>𝔗₂ : Set (Set δ₂)<VAR>h_image₁ : MapsTo (fun x => φ₁ '' x) 𝔗₁ 𝔖<VAR>h_image₂ : MapsTo (fun x => φ₂ '' x) 𝔗₂ 𝔖<VAR>h_preimage₁ : MapsTo (fun x => φ₁ ⁻¹' x) 𝔖 𝔗₁<VAR>h_preimage₂ : MapsTo (fun x => φ₂ ⁻¹' x) 𝔖 𝔗₂<VAR>h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂<VAR>ψ₁ : (S : Set α) → ↑(φ₁ ⁻¹' S) → ↑S := fun S => S.restrictPreimage φ₁<VAR>ψ₂ : (S : Set α) → ↑(φ₂ ⁻¹' S) → ↑S := fun S => S.restrictPreimage φ₂<VAR>this : ∀ S ∈ 𝔖, UniformFun.uniformSpace (↑S) β = UniformSpace.comap (fun x => x ∘ ψ₁ S) (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S)) β) ⊓ UniformSpace.comap (fun x => x ∘ ψ₂ S) (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S)) β)<GOAL>uniformSpace α β 𝔖 ≤ UniformSpace.comap (⇑(ofFun 𝔗₁) ∘ (fun x => x ∘ φ₁) ∘ ⇑(toFun 𝔖)) (uniformSpace δ₁ β 𝔗₁)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>δ₁ : Type u_5<VAR>δ₂ : Type u_6<VAR>φ₁ : δ₁ → α<VAR>φ₂ : δ₂ → α<VAR>𝔗₁ : Set (Set δ₁)<VAR>𝔗₂ : Set (Set δ₂)<VAR>h_image₁ : MapsTo (fun x => φ₁ '' x) 𝔗₁ 𝔖<VAR>h_image₂ : MapsTo (fun x => φ₂ '' x) 𝔗₂ 𝔖<VAR>h_preimage₁ : MapsTo (fun x => φ₁ ⁻¹' x) 𝔖 𝔗₁<VAR>h_preimage₂ : MapsTo (fun x => φ₂ ⁻¹' x) 𝔖 𝔗₂<VAR>h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂<VAR>ψ₁ : (S : Set α) → ↑(φ₁ ⁻¹' S) → ↑S := fun S => S.restrictPreimage φ₁<VAR>ψ₂ : (S : Set α) → ↑(φ₂ ⁻¹' S) → ↑S := fun S => S.restrictPreimage φ₂<VAR>this : ∀ S ∈ 𝔖, UniformFun.uniformSpace (↑S) β = UniformSpace.comap (fun x => x ∘ ψ₁ S) (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S)) β) ⊓ UniformSpace.comap (fun x => x ∘ ψ₂ S) (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S)) β)<GOAL>uniformSpace α β 𝔖 ≤ UniformSpace.comap (⇑(ofFun 𝔗₂) ∘ (fun x => x ∘ φ₂) ∘ ⇑(toFun 𝔖)) (uniformSpace δ₂ β 𝔗₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>δ₁ : Type u_5<VAR>δ₂ : Type u_6<VAR>φ₁ : δ₁ → α<VAR>φ₂ : δ₂ → α<VAR>𝔗₁ : Set (Set δ₁)<VAR>𝔗₂ : Set (Set δ₂)<VAR>h_image₁ : MapsTo (fun x => φ₁ '' x) 𝔗₁ 𝔖<VAR>h_image₂ : MapsTo (fun x => φ₂ '' x) 𝔗₂ 𝔖<VAR>h_preimage₁ : MapsTo (fun x => φ₁ ⁻¹' x) 𝔖 𝔗₁<VAR>h_preimage₂ : MapsTo (fun x => φ₂ ⁻¹' x) 𝔖 𝔗₂<VAR>h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂<VAR>ψ₁ : (S : Set α) → ↑(φ₁ ⁻¹' S) → ↑S := fun S => S.restrictPreimage φ₁<VAR>ψ₂ : (S : Set α) → ↑(φ₂ ⁻¹' S) → ↑S := fun S => S.restrictPreimage φ₂<VAR>this : ∀ S ∈ 𝔖, UniformFun.uniformSpace (↑S) β = UniformSpace.comap (fun x => x ∘ ψ₁ S) (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S)) β) ⊓ UniformSpace.comap (fun x => x ∘ ψ₂ S) (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S)) β)<VAR>S : Set α<VAR>hS : S ∈ 𝔖<GOAL>UniformSpace.comap (⇑(ofFun 𝔗₁) ∘ (fun x => x ∘ φ₁) ∘ ⇑(toFun 𝔖)) (uniformSpace δ₁ β 𝔗₁) ⊓ UniformSpace.comap (⇑(ofFun 𝔗₂) ∘ (fun x => x ∘ φ₂) ∘ ⇑(toFun 𝔖)) (uniformSpace δ₂ β 𝔗₂) ≤ UniformSpace.comap (⇑UniformFun.ofFun ∘ S.restrict ∘ ⇑(toFun 𝔖)) (UniformFun.uniformSpace (↑S) β)
<VAR>σ✝ : Type u_1<VAR>τ : Type u_2<VAR>R✝ : Type u_3<VAR>S : Type u_4<VAR>inst✝⁴ inst✝³ : CommSemiring R✝<VAR>inst✝² : CommSemiring S<VAR>φ ψ : MvPolynomial σ✝ R✝<VAR>m n✝ : ℕ<VAR>R : Type u_5<VAR>σ : Type u_6<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>F G : MvPolynomial σ R<VAR>n : ℕ<VAR>hF : F.IsHomogeneous n<VAR>h : ∀ (r : σ → R), (eval r) F = 0<VAR>hnR : ↑n ≤ #R<GOAL>F = 0
<VAR>σ✝ : Type u_1<VAR>τ : Type u_2<VAR>R✝ : Type u_3<VAR>S : Type u_4<VAR>inst✝⁴ inst✝³ : CommSemiring R✝<VAR>inst✝² : CommSemiring S<VAR>φ ψ : MvPolynomial σ✝ R✝<VAR>m n✝ : ℕ<VAR>R : Type u_5<VAR>σ : Type u_6<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>F G : MvPolynomial σ R<VAR>n : ℕ<VAR>hF : F.IsHomogeneous n<VAR>hnR : ↑n ≤ #R<VAR>h : F ≠ 0<GOAL>∃ r, (eval r) F ≠ 0
<VAR>σ✝ : Type u_1<VAR>τ : Type u_2<VAR>R✝ : Type u_3<VAR>S : Type u_4<VAR>inst✝⁴ inst✝³ : CommSemiring R✝<VAR>inst✝² : CommSemiring S<VAR>φ ψ : MvPolynomial σ✝ R✝<VAR>m n✝ : ℕ<VAR>R : Type u_5<VAR>σ : Type u_6<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>G : MvPolynomial σ R<VAR>n : ℕ<VAR>hnR : ↑n ≤ #R<VAR>k : ℕ<VAR>f : Fin k → σ<VAR>hf : Function.Injective f<VAR>F : MvPolynomial (Fin k) R<VAR>hF : ((rename f) F).IsHomogeneous n<VAR>h : (rename f) F ≠ 0<GOAL>∃ r, (eval r) ((rename f) F) ≠ 0
<VAR>σ✝ : Type u_1<VAR>τ : Type u_2<VAR>R✝ : Type u_3<VAR>S : Type u_4<VAR>inst✝⁴ inst✝³ : CommSemiring R✝<VAR>inst✝² : CommSemiring S<VAR>φ ψ : MvPolynomial σ✝ R✝<VAR>m n✝ : ℕ<VAR>R : Type u_5<VAR>σ : Type u_6<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>G : MvPolynomial σ R<VAR>n : ℕ<VAR>hnR : ↑n ≤ #R<VAR>k : ℕ<VAR>f : Fin k → σ<VAR>hf : Function.Injective f<VAR>F : MvPolynomial (Fin k) R<VAR>hF : ((rename f) F).IsHomogeneous n<VAR>h : (rename f) F ≠ 0<VAR>hF₀ : F ≠ 0<GOAL>∃ r, (eval r) ((rename f) F) ≠ 0
<VAR>σ✝ : Type u_1<VAR>τ : Type u_2<VAR>R✝ : Type u_3<VAR>S : Type u_4<VAR>inst✝⁴ inst✝³ : CommSemiring R✝<VAR>inst✝² : CommSemiring S<VAR>φ ψ : MvPolynomial σ✝ R✝<VAR>m n✝ : ℕ<VAR>R : Type u_5<VAR>σ : Type u_6<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>G : MvPolynomial σ R<VAR>n : ℕ<VAR>hnR : ↑n ≤ #R<VAR>k : ℕ<VAR>f : Fin k → σ<VAR>hf : Function.Injective f<VAR>F : MvPolynomial (Fin k) R<VAR>hF✝ : ((rename f) F).IsHomogeneous n<VAR>h : (rename f) F ≠ 0<VAR>hF₀ : F ≠ 0<VAR>hF : F.IsHomogeneous n<GOAL>∃ r, (eval r) ((rename f) F) ≠ 0
<VAR>σ✝ : Type u_1<VAR>τ : Type u_2<VAR>R✝ : Type u_3<VAR>S : Type u_4<VAR>inst✝⁴ inst✝³ : CommSemiring R✝<VAR>inst✝² : CommSemiring S<VAR>φ ψ : MvPolynomial σ✝ R✝<VAR>m n✝ : ℕ<VAR>R : Type u_5<VAR>σ : Type u_6<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>G : MvPolynomial σ R<VAR>n : ℕ<VAR>hnR : ↑n ≤ #R<VAR>k : ℕ<VAR>f : Fin k → σ<VAR>hf : Function.Injective f<VAR>F : MvPolynomial (Fin k) R<VAR>hF✝ : ((rename f) F).IsHomogeneous n<VAR>h : (rename f) F ≠ 0<VAR>hF₀ : F ≠ 0<VAR>hF : F.IsHomogeneous n<VAR>r : Fin k → R<VAR>hr : (eval r) F ≠ 0<GOAL>∃ r, (eval r) ((rename f) F) ≠ 0
<VAR>σ✝ : Type u_1<VAR>τ : Type u_2<VAR>R✝ : Type u_3<VAR>S : Type u_4<VAR>inst✝⁴ inst✝³ : CommSemiring R✝<VAR>inst✝² : CommSemiring S<VAR>φ ψ : MvPolynomial σ✝ R✝<VAR>m n✝ : ℕ<VAR>R : Type u_5<VAR>σ : Type u_6<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>G : MvPolynomial σ R<VAR>n : ℕ<VAR>hnR : ↑n ≤ #R<VAR>k : ℕ<VAR>f : Fin k → σ<VAR>hf : Function.Injective f<VAR>F : MvPolynomial (Fin k) R<VAR>hF✝ : ((rename f) F).IsHomogeneous n<VAR>h : (rename f) F ≠ 0<VAR>hF₀ : F ≠ 0<VAR>hF : F.IsHomogeneous n<VAR>r : σ → R<VAR>hr : (eval (r ∘ f)) F ≠ 0<GOAL>∃ r, (eval r) ((rename f) F) ≠ 0
<VAR>σ✝ : Type u_1<VAR>τ : Type u_2<VAR>R✝ : Type u_3<VAR>S : Type u_4<VAR>inst✝⁴ inst✝³ : CommSemiring R✝<VAR>inst✝² : CommSemiring S<VAR>φ ψ : MvPolynomial σ✝ R✝<VAR>m n✝ : ℕ<VAR>R : Type u_5<VAR>σ : Type u_6<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>G : MvPolynomial σ R<VAR>n : ℕ<VAR>hnR : ↑n ≤ #R<VAR>k : ℕ<VAR>f : Fin k → σ<VAR>hf : Function.Injective f<VAR>F : MvPolynomial (Fin k) R<VAR>hF✝ : ((rename f) F).IsHomogeneous n<VAR>h : (rename f) F ≠ 0<VAR>hF₀ : F ≠ 0<VAR>hF : F.IsHomogeneous n<VAR>r : σ → R<VAR>hr : (eval (r ∘ f)) F ≠ 0<GOAL>(eval r) ((rename f) F) ≠ 0
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>β : Type u_3<VAR>f : α → β<VAR>hf : Injective f<VAR>m : ι → OuterMeasure α<GOAL>(map f) (⨅ i, m i) = (restrict (range f)) (⨅ i, (map f) (m i))
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>β : Type u_3<VAR>f : α → β<VAR>hf : Injective f<VAR>m : ι → OuterMeasure α<GOAL>(map f) (⨅ i, m i) = (map f) ((comap f) (⨅ i, (map f) (m i)))
<VAR>a✝ b✝ m n p✝ p a b : ℕ<VAR>hab : a.Coprime b<VAR>hpb : p ∈ b.primeFactorsList<GOAL>(a * b).factorization p = b.factorization p
<VAR>a✝ b✝ m n p✝ p a b : ℕ<VAR>hab : a.Coprime b<VAR>hpb : p ∈ b.primeFactorsList<GOAL>(b * a).factorization p = b.factorization p
<VAR>R : Type u_1<VAR>c₁ c₂ : R<GOAL>#↑Set.univ = #R ^ 4
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<VAR>φ : MultilinearMap R s E<VAR>r : R<VAR>x : ⨂[R] (i : ι), s i<GOAL>(liftAux φ) (r • x) = r • (liftAux φ) x
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<VAR>φ : MultilinearMap R s E<VAR>r : R<VAR>x : ⨂[R] (i : ι), s i<GOAL>∀ (r_1 : R) (f : (i : ι) → s i), (liftAux φ) (r • tprodCoeff R r_1 f) = r • (liftAux φ) (tprodCoeff R r_1 f)
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<VAR>φ : MultilinearMap R s E<VAR>r : R<VAR>x : ⨂[R] (i : ι), s i<GOAL>∀ (x y : ⨂[R] (i : ι), s i), (liftAux φ) (r • x) = r • (liftAux φ) x → (liftAux φ) (r • y) = r • (liftAux φ) y → (liftAux φ) (r • (x + y)) = r • (liftAux φ) (x + y)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ Z✝ X Y Z : C<VAR>f f' : X ⟶ Y<VAR>g : Y ≅ Z<GOAL>f ≫ g.hom = f' ≫ g.hom ↔ f = f'
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h : a < b / c<GOAL>a * c < b
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h : b ≤ a * c<GOAL>b / c ≤ a
<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>f : R[X] →+* MvPolynomial PUnit.{?u.2149 + 1} R := eval₂RingHom C (X PUnit.unit)<VAR>g : MvPolynomial PUnit.{?u.2149 + 1} R →+* R[X] := eval₂Hom Polynomial.C fun x => Polynomial.X<GOAL>∀ (p : MvPolynomial PUnit.{?u.2149 + 1} R), (f.comp g) p = p
<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>f : R[X] →+* MvPolynomial PUnit.{?u.2149 + 1} R := eval₂RingHom C (X PUnit.unit)<VAR>g : MvPolynomial PUnit.{?u.2149 + 1} R →+* R[X] := eval₂Hom Polynomial.C fun x => Polynomial.X<GOAL>(f.comp g).comp C = C
<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>f : R[X] →+* MvPolynomial PUnit.{?u.2149 + 1} R := eval₂RingHom C (X PUnit.unit)<VAR>g : MvPolynomial PUnit.{?u.2149 + 1} R →+* R[X] := eval₂Hom Polynomial.C fun x => Polynomial.X<GOAL>∀ (n : PUnit.{?u.2149 + 1}), (f.comp g) (X n) = X 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>p : R[X]<VAR>a : R<GOAL>eval₂ Polynomial.C (fun x => Polynomial.X) (Polynomial.eval₂ C (X PUnit.unit) (Polynomial.C a)) = Polynomial.C a
<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>p✝ p q : R[X]<VAR>hp : eval₂ Polynomial.C (fun x => Polynomial.X) (Polynomial.eval₂ C (X PUnit.unit) p) = p<VAR>hq : eval₂ Polynomial.C (fun x => Polynomial.X) (Polynomial.eval₂ C (X PUnit.unit) q) = q<GOAL>eval₂ Polynomial.C (fun x => Polynomial.X) (Polynomial.eval₂ C (X PUnit.unit) (p + q)) = p + q
<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>p✝ : R[X]<VAR>p : ℕ<VAR>n : R<VAR>x✝ : eval₂ Polynomial.C (fun x => Polynomial.X) (Polynomial.eval₂ C (X PUnit.unit) (Polynomial.C n * Polynomial.X ^ p)) = Polynomial.C n * Polynomial.X ^ p<GOAL>eval₂ Polynomial.C (fun x => Polynomial.X) (Polynomial.eval₂ C (X PUnit.unit) (Polynomial.C n * Polynomial.X ^ (p + 1))) = Polynomial.C n * Polynomial.X ^ (p + 1)
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>a b : R<VAR>ha : Irreducible a<VAR>hb : Irreducible b<GOAL>Associated a b
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>a b : R<VAR>ha : maximalIdeal R = span {a}<VAR>hb : maximalIdeal R = span {b}<GOAL>Associated a b
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<GOAL>ContDiffWithinAt 𝕜 n f (insert x s) x ↔ ContDiffWithinAt 𝕜 n f s x
<VAR>n : ℕ<VAR>G : Type u<VAR>inst✝¹ : Group G<VAR>N : Subgroup G<VAR>inst✝ : N.Normal<VAR>hN : (Nat.card ↥N).Coprime N.index<VAR>hN1 : ¬Nat.card ↥N = 0<VAR>hN2 : ¬N.index = 0<GOAL>∃ H, N.IsComplement' H
<VAR>n : ℕ<VAR>G : Type u<VAR>inst✝¹ : Group G<VAR>N : Subgroup G<VAR>inst✝ : N.Normal<VAR>hN : (Nat.card ↥N).Coprime N.index<VAR>hN1 : ¬Nat.card ↥N = 0<VAR>hN2 : ¬N.index = 0<VAR>hN3 : Nat.card G ≠ 0<GOAL>∃ H, N.IsComplement' H
<VAR>n : ℕ<VAR>G : Type u<VAR>inst✝¹ : Group G<VAR>N : Subgroup G<VAR>inst✝ : N.Normal<VAR>hN : (Nat.card ↥N).Coprime N.index<VAR>hN1 : ¬Nat.card ↥N = 0<VAR>hN2 : ¬N.index = 0<VAR>hN3 : Nat.card G ≠ 0<VAR>this : Fintype G<GOAL>∃ H, N.IsComplement' H
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Group M<VAR>inst✝¹ : CommRing R<VAR>inst✝ : MulSemiringAction M R<VAR>a : M<VAR>S : Ideal R<VAR>ha : Function.Surjective fun r => a • r<VAR>x✝ : R<GOAL>x✝ ∈ Submodule.toAddSubgroup (a • S) ↔ x✝ ∈ a • Submodule.toAddSubgroup S
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>hG : IsPGroup p G<VAR>n : ℕ<VAR>hn : p.Coprime n<VAR>g : G<GOAL>(hG.powEquiv hn).symm g = g ^ (orderOf g).gcdB n
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>hG : IsPGroup p G<VAR>n : ℕ<VAR>hn : p.Coprime n<VAR>g : G<GOAL>(hG.powEquiv hn).symm g = g ^ (Nat.card ↥(Subgroup.zpowers g)).gcdB n
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : DivisionCommMonoid α<VAR>a b✝ c d : α<VAR>h : IsUnit a<VAR>b : α<GOAL>a * (b / a) = b
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoidWithZero R<VAR>inst✝ : WfDvdMonoid R<VAR>r : R<VAR>hr : r ≠ 0<GOAL>Squarefree r ↔ ∀ (x : R), Irreducible x → ¬x * x ∣ r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a b : α<VAR>s : Set α<VAR>ha : s ⊆ Ioi a<VAR>hs : ∀ b' > a, ∃ b > a, Ioo a b ⊆ s<GOAL>map Subtype.val atBot = 𝓝[>] a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a b : α<VAR>s : Set α<VAR>ha : s ⊆ Ioi a<VAR>hs : ∀ b' > a, ∃ b > a, Ioo a b ⊆ s<VAR>b' : αᵒᵈ<VAR>hb' : b' < toDual a<GOAL>∃ a_1 < toDual a, Ioo a_1 (toDual a) ⊆ ⇑ofDual ⁻¹' s
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : LinearOrderedRing R<VAR>inst✝⁴ : FloorRing R<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : OrderTopology R<VAR>inst✝¹ : MeasurableSpace R<VAR>inst✝ : OpensMeasurableSpace R<VAR>x : R<GOAL>MeasurableSet (floor ⁻¹' {⌊x⌋})
<VAR>R✝ : Type u<VAR>inst✝¹¹ : CommRing R✝<VAR>W✝ : Affine R✝<VAR>R : Type r<VAR>inst✝¹⁰ : CommRing R<VAR>W : Affine R<VAR>S : Type s<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra S A<VAR>inst✝⁴ : IsScalarTower R S A<VAR>B : Type v<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra S B<VAR>inst✝ : IsScalarTower R S B<VAR>f : A →ₐ[S] B<VAR>hf : Function.Injective ⇑f<VAR>x y : A<GOAL>(baseChange W B).toAffine.Nonsingular (f x) (f y) ↔ (baseChange W A).toAffine.Nonsingular x y
<VAR>R✝ : Type u<VAR>inst✝¹¹ : CommRing R✝<VAR>W✝ : Affine R✝<VAR>R : Type r<VAR>inst✝¹⁰ : CommRing R<VAR>W : Affine R<VAR>S : Type s<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra S A<VAR>inst✝⁴ : IsScalarTower R S A<VAR>B : Type v<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra S B<VAR>inst✝ : IsScalarTower R S B<VAR>f : A →ₐ[S] B<VAR>hf : Function.Injective ⇑f<VAR>x y : A<GOAL>(baseChange W B).toAffine.Nonsingular (f x) (f y) ↔ (baseChange W B).toAffine.Nonsingular (f.toRingHom x) (f.toRingHom y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : MeasurableSpace α<VAR>p✝ : PMF α<VAR>s t : Set α<VAR>inst✝ : MeasurableSingletonClass α<VAR>p q : PMF α<VAR>h : p.toMeasure = q.toMeasure<VAR>x : α<GOAL>p x = q x
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>htwo : p ^ (k + 1) ≠ 2<GOAL>Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>htwo : p ^ (k + 1) ≠ 2<VAR>this : (Algebra.norm ℤ) (hζ.toInteger ^ ↑p ^ 0 - 1) = ↑↑p ^ ↑p ^ 0<GOAL>Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>htwo : p ^ (k + 1) ≠ 2<VAR>this : (Algebra.norm ℤ) (hζ.toInteger - 1) = ↑↑p<GOAL>Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>htwo : p ^ (k + 1) ≠ 2<VAR>this : (Algebra.norm ℤ) (hζ.toInteger - 1) = ↑↑p<GOAL>Prime ↑↑p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : CommGroup G<VAR>a✝ b✝ c✝ d a b c : G<GOAL>a / b = c / b * (a / c)
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : Zero R<VAR>a✝ b : Γ<VAR>r✝ : R<VAR>a : Γ<VAR>r s : R<VAR>rs : (single a) r = (single a) s<GOAL>r = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>hs : s.Finite<VAR>h : (f '' s).encard = s.encard<GOAL>InjOn f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>hs : s.Finite<VAR>h : (f '' s).encard = s.encard<VAR>h' : IsEmpty α<GOAL>InjOn f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>hs : s.Finite<VAR>h : (f '' s).encard = s.encard<VAR>hne : Nonempty α<GOAL>InjOn f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>hs : s.Finite<VAR>hne : Nonempty α<VAR>h : (Function.invFunOn f s '' (f '' s)).encard = s.encard<GOAL>InjOn f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>hs : s.Finite<VAR>hne : Nonempty α<VAR>h : (Function.invFunOn f s '' (f '' s)).encard = s.encard<GOAL>Function.invFunOn f s '' (f '' s) = s
<VAR>b : ℝ<GOAL>∫ (x : ℝ), rexp (-b * x ^ 2) = √(π / b)
<VAR>b : ℝ<VAR>hb : b ≤ 0<GOAL>∫ (x : ℝ), rexp (-b * x ^ 2) = √(π / b)
<VAR>b : ℝ<VAR>hb : 0 < b<GOAL>∫ (x : ℝ), rexp (-b * x ^ 2) = √(π / b)
<VAR>b : ℝ<VAR>hb : 0 < b<GOAL>(∫ (x : ℝ), rexp (-b * x ^ 2)) ^ 2 = √(π / b) ^ 2
<VAR>b : ℝ<VAR>hb : 0 < b<GOAL>(∫ (x : ℝ), ↑(rexp (-b * x ^ 2))) ^ 2 = ↑π / ↑b
<VAR>b : ℝ<VAR>hb : 0 < b<VAR>x : ℝ<GOAL>↑(rexp (-b * x ^ 2)) = cexp (-↑b * ↑x ^ 2)
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝² : Group H<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>d : TransversalPair G A B<VAR>inst✝ : DecidableEq G<VAR>g : HNNExtension G A B φ<VAR>w : NormalWord d<GOAL>ReducedWord.prod φ (g • w).toReducedWord = g * ReducedWord.prod φ w.toReducedWord
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>s : Set E<VAR>x : E<VAR>r : ℝ≥0∞<VAR>h : HasFPowerSeriesWithinOnBall f p s x r<GOAL>ContinuousWithinAt f s x
<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>I : ↥(Ideal R)⁰<GOAL>mk ((FractionalIdeal.mk0 K) I) = mk0 I
<VAR>G : Type u<VAR>inst✝² : Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>H : Type v<VAR>inst✝¹ : Group H<VAR>M : Type x<VAR>inst✝ : Monoid M<VAR>φ : G →* H<VAR>a✝ b✝ : G ⧸ φ.ker<VAR>a b : G<VAR>h : φ.rangeRestrict a = φ.rangeRestrict b<GOAL>Setoid.r a b