ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x✝ y✝ x y : M<VAR>h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0<VAR>g : Fin (Nat.succ 0).succ → R<VAR>hg : g 0 • x + g 1 • y = 0<GOAL>g ⟨0, ⋯⟩ = 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x✝ y✝ x y : M<VAR>h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0<VAR>g : Fin (Nat.succ 0).succ → R<VAR>hg : g 0 • x + g 1 • y = 0<GOAL>g ⟨1, ⋯⟩ = 0
<VAR>u v m n : ℤ<GOAL>¬Even n ↔ n % 2 = 1
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>a : P.A<VAR>f' : P.drop.B a ⟹ α<VAR>f : P.last.B a → P.W α<GOAL>P.wDest' (P.wMk a f' f) = ⟨a, splitFun f' f⟩
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁷ : RCLike 𝕜<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : T2Space A<VAR>inst✝⁴ : NonUnitalRing A<VAR>inst✝³ : StarRing A<VAR>inst✝² : Module 𝕜 A<VAR>inst✝¹ : IsScalarTower 𝕜 A A<VAR>inst✝ : SMulCommClass 𝕜 A A<VAR>h✝ : ∀ (a : A), CompactSpace ↑(quasispectrum 𝕜 a)<VAR>s : Set 𝕜<VAR>hs : CompactSpace ↑s<VAR>_inst : Zero ↑s<VAR>h0 : ↑0 = 0<VAR>φ ψ : ContinuousMapZero (↑s) 𝕜 →⋆ₙₐ[𝕜] A<VAR>hφ : Continuous ⇑φ<VAR>hψ : Continuous ⇑ψ<VAR>h : φ { toContinuousMap := ContinuousMap.restrict s (ContinuousMap.id 𝕜), map_zero' := h0 } = ψ { toContinuousMap := ContinuousMap.restrict s (ContinuousMap.id 𝕜), map_zero' := h0 }<GOAL>φ = ψ
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁷ : RCLike 𝕜<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : T2Space A<VAR>inst✝⁴ : NonUnitalRing A<VAR>inst✝³ : StarRing A<VAR>inst✝² : Module 𝕜 A<VAR>inst✝¹ : IsScalarTower 𝕜 A A<VAR>inst✝ : SMulCommClass 𝕜 A A<VAR>h✝ : ∀ (a : A), CompactSpace ↑(quasispectrum 𝕜 a)<VAR>s : Set 𝕜<VAR>hs : CompactSpace ↑s<VAR>_inst : Zero ↑s<VAR>h0 : ↑0 = 0<VAR>φ ψ : ContinuousMapZero (↑s) 𝕜 →⋆ₙₐ[𝕜] A<VAR>hφ : Continuous ⇑φ<VAR>hψ : Continuous ⇑ψ<VAR>h : φ { toContinuousMap := ContinuousMap.restrict s (ContinuousMap.id 𝕜), map_zero' := h0 } = ψ { toContinuousMap := ContinuousMap.restrict s (ContinuousMap.id 𝕜), map_zero' := h0 }<GOAL>Set.EqOn (⇑φ) (⇑ψ) (closure ↑(adjoin 𝕜 {ContinuousMapZero.id h0}))
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁷ : RCLike 𝕜<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : T2Space A<VAR>inst✝⁴ : NonUnitalRing A<VAR>inst✝³ : StarRing A<VAR>inst✝² : Module 𝕜 A<VAR>inst✝¹ : IsScalarTower 𝕜 A A<VAR>inst✝ : SMulCommClass 𝕜 A A<VAR>h✝ : ∀ (a : A), CompactSpace ↑(quasispectrum 𝕜 a)<VAR>s : Set 𝕜<VAR>hs : CompactSpace ↑s<VAR>_inst : Zero ↑s<VAR>h0 : ↑0 = 0<VAR>φ ψ : ContinuousMapZero (↑s) 𝕜 →⋆ₙₐ[𝕜] A<VAR>hφ : Continuous ⇑φ<VAR>hψ : Continuous ⇑ψ<VAR>h : φ { toContinuousMap := ContinuousMap.restrict s (ContinuousMap.id 𝕜), map_zero' := h0 } = ψ { toContinuousMap := ContinuousMap.restrict s (ContinuousMap.id 𝕜), map_zero' := h0 }<VAR>f : ContinuousMapZero (↑s) 𝕜<VAR>hf : f ∈ ↑(adjoin 𝕜 {ContinuousMapZero.id h0})<GOAL>φ f = ψ f
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁷ : RCLike 𝕜<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : T2Space A<VAR>inst✝⁴ : NonUnitalRing A<VAR>inst✝³ : StarRing A<VAR>inst✝² : Module 𝕜 A<VAR>inst✝¹ : IsScalarTower 𝕜 A A<VAR>inst✝ : SMulCommClass 𝕜 A A<VAR>h✝ : ∀ (a : A), CompactSpace ↑(quasispectrum 𝕜 a)<VAR>s : Set 𝕜<VAR>hs : CompactSpace ↑s<VAR>_inst : Zero ↑s<VAR>h0 : ↑0 = 0<VAR>φ ψ : ContinuousMapZero (↑s) 𝕜 →⋆ₙₐ[𝕜] A<VAR>hφ : Continuous ⇑φ<VAR>hψ : Continuous ⇑ψ<VAR>h : φ { toContinuousMap := ContinuousMap.restrict s (ContinuousMap.id 𝕜), map_zero' := h0 } = ψ { toContinuousMap := ContinuousMap.restrict s (ContinuousMap.id 𝕜), map_zero' := h0 }<VAR>f : ContinuousMapZero (↑s) 𝕜<VAR>hf : f ∈ ↑(adjoin 𝕜 {ContinuousMapZero.id h0})<GOAL>f ∈ NonUnitalStarAlgHom.equalizer φ ψ
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁷ : RCLike 𝕜<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : T2Space A<VAR>inst✝⁴ : NonUnitalRing A<VAR>inst✝³ : StarRing A<VAR>inst✝² : Module 𝕜 A<VAR>inst✝¹ : IsScalarTower 𝕜 A A<VAR>inst✝ : SMulCommClass 𝕜 A A<VAR>h✝ : ∀ (a : A), CompactSpace ↑(quasispectrum 𝕜 a)<VAR>s : Set 𝕜<VAR>hs : CompactSpace ↑s<VAR>_inst : Zero ↑s<VAR>h0 : ↑0 = 0<VAR>φ ψ : ContinuousMapZero (↑s) 𝕜 →⋆ₙₐ[𝕜] A<VAR>hφ : Continuous ⇑φ<VAR>hψ : Continuous ⇑ψ<VAR>h : φ { toContinuousMap := ContinuousMap.restrict s (ContinuousMap.id 𝕜), map_zero' := h0 } = ψ { toContinuousMap := ContinuousMap.restrict s (ContinuousMap.id 𝕜), map_zero' := h0 }<VAR>f : ContinuousMapZero (↑s) 𝕜<VAR>hf : f ∈ ↑(adjoin 𝕜 {ContinuousMapZero.id h0})<GOAL>{ContinuousMapZero.id h0} ⊆ ↑(NonUnitalStarAlgHom.equalizer φ ψ)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁷ : RCLike 𝕜<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : T2Space A<VAR>inst✝⁴ : NonUnitalRing A<VAR>inst✝³ : StarRing A<VAR>inst✝² : Module 𝕜 A<VAR>inst✝¹ : IsScalarTower 𝕜 A A<VAR>inst✝ : SMulCommClass 𝕜 A A<VAR>h✝ : ∀ (a : A), CompactSpace ↑(quasispectrum 𝕜 a)<VAR>s : Set 𝕜<VAR>hs : CompactSpace ↑s<VAR>_inst : Zero ↑s<VAR>h0 : ↑0 = 0<VAR>φ ψ : ContinuousMapZero (↑s) 𝕜 →⋆ₙₐ[𝕜] A<VAR>hφ : Continuous ⇑φ<VAR>hψ : Continuous ⇑ψ<VAR>h : φ { toContinuousMap := ContinuousMap.restrict s (ContinuousMap.id 𝕜), map_zero' := h0 } = ψ { toContinuousMap := ContinuousMap.restrict s (ContinuousMap.id 𝕜), map_zero' := h0 }<VAR>f : ContinuousMapZero (↑s) 𝕜<VAR>hf : f ∈ ↑(adjoin 𝕜 {ContinuousMapZero.id h0})<GOAL>ContinuousMapZero.id h0 ∈ ↑(NonUnitalStarAlgHom.equalizer φ ψ)
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : StarModule ℂ A<VAR>a : A<VAR>ha : IsSelfAdjoint a<GOAL>SpectrumRestricts (a ^ 2) ⇑ContinuousMap.realToNNReal
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : StarModule ℂ A<VAR>a : A<VAR>ha : IsSelfAdjoint a<GOAL>∀ x ∈ (fun x => id x ^ 2) '' σ ℝ a, 0 ≤ x
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : StarModule ℂ A<VAR>a : A<VAR>ha : IsSelfAdjoint a<VAR>x : ℝ<GOAL>0 ≤ (fun x => id x ^ 2) x
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NNNorm 𝕜<VAR>E : Type u_2<VAR>inst✝ : SMul 𝕜 E<VAR>c : 𝕜<VAR>s t : Set E<VAR>x : E<VAR>r : ℝ≥0∞<GOAL>egauge 𝕜 s x < r ↔ ∃ c, x ∈ c • s ∧ ↑‖c‖₊ < r
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>a : R<VAR>n : ℕ<GOAL>(C a * X ^ n).leadingCoeff = a
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : AddCommMonoid ι<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>f : NumDenSameDeg 𝒜 x<VAR>h : f.num = 0<GOAL>mk f = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : AddCommMonoid ι<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>f : NumDenSameDeg 𝒜 x<VAR>h : f.num = 0<GOAL>(mk f).val = val 0
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ : Set α<VAR>s : ι → Set α<VAR>t : Set ι<VAR>ht : t.Countable<VAR>this : Countable ↑t<GOAL>ae (μ.restrict (⋃ i ∈ t, s i)) = ⨆ i ∈ t, ae (μ.restrict (s i))
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝¹⁴ : CommSemiring R✝<VAR>inst✝¹³ : NonUnitalRing A✝<VAR>inst✝¹² : Module R✝ A✝<VAR>inst✝¹¹ : IsScalarTower R✝ A✝ A✝<VAR>inst✝¹⁰ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Nontrivial S<VAR>inst✝⁶ : NonUnitalRing A<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Module S A<VAR>inst✝³ : IsScalarTower S A A<VAR>inst✝² : SMulCommClass S A A<VAR>inst✝¹ : Module R A<VAR>inst✝ : IsScalarTower R S A<VAR>a : A<GOAL>0 ∈ spectrum R ↑a
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝¹⁴ : CommSemiring R✝<VAR>inst✝¹³ : NonUnitalRing A✝<VAR>inst✝¹² : Module R✝ A✝<VAR>inst✝¹¹ : IsScalarTower R✝ A✝ A✝<VAR>inst✝¹⁰ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Nontrivial S<VAR>inst✝⁶ : NonUnitalRing A<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Module S A<VAR>inst✝³ : IsScalarTower S A A<VAR>inst✝² : SMulCommClass S A A<VAR>inst✝¹ : Module R A<VAR>inst✝ : IsScalarTower R S A<VAR>a : A<GOAL>¬IsUnit ↑a
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝¹⁴ : CommSemiring R✝<VAR>inst✝¹³ : NonUnitalRing A✝<VAR>inst✝¹² : Module R✝ A✝<VAR>inst✝¹¹ : IsScalarTower R✝ A✝ A✝<VAR>inst✝¹⁰ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Nontrivial S<VAR>inst✝⁶ : NonUnitalRing A<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Module S A<VAR>inst✝³ : IsScalarTower S A A<VAR>inst✝² : SMulCommClass S A A<VAR>inst✝¹ : Module R A<VAR>inst✝ : IsScalarTower R S A<VAR>a : A<VAR>u : (Unitization S A)ˣ<VAR>hu : ↑u = ↑a<GOAL>False
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<VAR>inst✝⁹ : LieRing L'<VAR>inst✝⁸ : LieAlgebra R L'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I I₂ : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>x : L<VAR>hx : x ∈ I<GOAL>f x ∈ map f I
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<VAR>inst✝⁹ : LieRing L'<VAR>inst✝⁸ : LieAlgebra R L'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I I₂ : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>x : L<VAR>hx : x ∈ I<GOAL>f x ∈ ↑(Submodule.map (↑f) (lieIdealSubalgebra R L I).toSubmodule)
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<VAR>inst✝⁹ : LieRing L'<VAR>inst✝⁸ : LieAlgebra R L'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I I₂ : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>x : L<VAR>hx : x ∈ I<GOAL>x ∈ ↑(lieIdealSubalgebra R L I).toSubmodule ∧ ↑f x = f x
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : UniformSpace β<VAR>K : Set α<VAR>V : Set (β × β)<VAR>f✝ : C(α, β)<VAR>ι : Type u₃<VAR>p : Filter ι<VAR>F : ι → C(α, β)<VAR>f : C(α, β)<GOAL>Tendsto F p (𝓝 f) ↔ ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => (F i) a) (⇑f) p K
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : UniformSpace β<VAR>K : Set α<VAR>V : Set (β × β)<VAR>f✝ : C(α, β)<VAR>ι : Type u₃<VAR>p : Filter ι<VAR>F : ι → C(α, β)<VAR>f : C(α, β)<GOAL>(∀ (K : Set α), IsCompact K → ∀ (U : Set β), IsOpen U → MapsTo (⇑f) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U) ↔ ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => (F i) a) (⇑f) p K
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>p q : R<VAR>hp : Irreducible p<VAR>hq : Irreducible q<VAR>ϖ : R<VAR>hϖ : Irreducible ϖ<VAR>hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x<GOAL>Associated p q
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>p q : R<VAR>hp : Irreducible p<VAR>hq : Irreducible q<VAR>ϖ : R<VAR>hϖ : Irreducible ϖ<VAR>hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x<GOAL>∀ {p : R}, Irreducible p → Associated p ϖ
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>ϖ : R<VAR>hϖ : Irreducible ϖ<VAR>hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x<VAR>p : R<VAR>hp : Irreducible p<GOAL>Associated p ϖ
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>ϖ : R<VAR>hϖ : Irreducible ϖ<VAR>hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x<VAR>p : R<VAR>hp : Irreducible p<VAR>n : ℕ<VAR>hn : Associated (ϖ ^ n) p<GOAL>Associated p ϖ
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>ϖ : R<VAR>hϖ : Irreducible ϖ<VAR>hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x<VAR>p : R<VAR>hp : Irreducible p<VAR>n : ℕ<VAR>hn : Associated (ϖ ^ n) p<VAR>this : Irreducible (ϖ ^ n)<GOAL>Associated p ϖ
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>ϖ : R<VAR>hϖ : Irreducible ϖ<VAR>hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x<VAR>p : R<VAR>hp : Irreducible p<VAR>n : ℕ<VAR>hn : Associated (ϖ ^ n) p<VAR>this : Irreducible (ϖ ^ n)<VAR>H : n < 1<GOAL>Associated p ϖ
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>ϖ : R<VAR>hϖ : Irreducible ϖ<VAR>hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x<VAR>p : R<VAR>hp : Irreducible p<VAR>hn : Associated (ϖ ^ 1) p<VAR>this : Irreducible (ϖ ^ 1)<GOAL>Associated p ϖ
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>ϖ : R<VAR>hϖ : Irreducible ϖ<VAR>hR : ∀ {x : R}, x ≠ 0 → ∃ n, Associated (ϖ ^ n) x<VAR>p : R<VAR>hp : Irreducible p<VAR>n : ℕ<VAR>hn : Associated (ϖ ^ n) p<VAR>this : Irreducible (ϖ ^ n)<VAR>H : 1 < n<GOAL>Associated p ϖ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>S : Set (Set β)<VAR>h_pi : IsPiSystem S<VAR>f : α → β<VAR>s : Set β<VAR>hs_mem : s ∈ S<VAR>t : Set β<VAR>ht_mem : t ∈ S<VAR>hst : (f ⁻¹' s ∩ f ⁻¹' t).Nonempty<GOAL>f ⁻¹' s ∩ f ⁻¹' t ∈ {s | ∃ t ∈ S, f ⁻¹' t = s}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>S : Set (Set β)<VAR>h_pi : IsPiSystem S<VAR>f : α → β<VAR>s : Set β<VAR>hs_mem : s ∈ S<VAR>t : Set β<VAR>ht_mem : t ∈ S<VAR>hst : (f ⁻¹' (s ∩ t)).Nonempty<GOAL>f ⁻¹' (s ∩ t) ∈ {s | ∃ t ∈ S, f ⁻¹' t = s}
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup X<VAR>inst✝¹ : NormedSpace ℝ X<VAR>inst✝ : HasContDiffBump E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x✝ : E<VAR>n : ℕ∞<VAR>x : E<GOAL>↑f (c - x) = ↑f (c + x)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m✝ n✝ : ℤ<VAR>a1 : 1 < a<VAR>m n : ℕ<VAR>mn : m < n<GOAL>1 / a ^ n < 1 / a ^ m
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>x : R<GOAL>BddBelow (Set.range (seminormFromConst_seq c f x))
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>x : R<GOAL>0 ∈ lowerBounds (Set.range (seminormFromConst_seq c f x))
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>x : R<VAR>n : ℕ<GOAL>0 ≤ seminormFromConst_seq c f x n
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>s t : Set α<VAR>a b x y : α<VAR>hs : f.IsCycleOn s<GOAL>s.Countable
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>t : Set α<VAR>a b x y : α<VAR>hs : f.IsCycleOn ∅<GOAL>∅.Countable
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>s t : Set α<VAR>a✝ b x y : α<VAR>hs : f.IsCycleOn s<VAR>a : α<VAR>ha : a ∈ s<GOAL>s.Countable
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝¹² : CommRing K<VAR>inst✝¹¹ : CommRing L<VAR>inst✝¹⁰ : CommRing M<VAR>inst✝⁹ : CommRing N<VAR>i : K →+* L<VAR>j : K →+* M<VAR>k : K →+* N<VAR>f : L →+* M<VAR>g : L →+* N<VAR>p : ℕ<VAR>inst✝⁸ : ExpChar K p<VAR>inst✝⁷ : ExpChar L p<VAR>inst✝⁶ : ExpChar M p<VAR>inst✝⁵ : ExpChar N p<VAR>inst✝⁴ : PerfectRing M p<VAR>inst✝³ : IsPRadical i p<VAR>inst✝² : PerfectRing N p<VAR>inst✝¹ : IsPRadical j p<VAR>inst✝ : PerfectRing L p<VAR>x : L<GOAL>(lift j i p) ((lift i j p) x) = x
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝⁴ : MulOneClass α<VAR>inst✝³ : Zero α<VAR>inst✝² : Preorder α<VAR>inst✝¹ : PosMulMono α<VAR>inst✝ : PosMulReflectLE α<VAR>a0 : 0 < a<GOAL>a * b ≤ a ↔ a * b ≤ a * 1
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>I J : Ideal R<VAR>K L : Ideal S<GOAL>{ toFun := map f, map_zero' := ⋯ }.toFun 1 = 1
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>I J : Ideal R<VAR>K L : Ideal S<GOAL>map f ⊤ = ⊤
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<VAR>n : ℤ<GOAL>toIocMod hp a b = b ↔ b ∈ Set.Ioc a (a + p)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<VAR>n : ℤ<GOAL>∃ z, b = b + z • p
<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 β<GOAL>image2 f s t = (f '' s).seq t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t✝ t₁ t₂ u : Set α<VAR>p : Prop<VAR>inst✝ : Decidable p<VAR>t : p → Set α<VAR>x : α<GOAL>(x ∈ if h : p then t h else ∅) ↔ ∃ (h : p), x ∈ t h
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t✝ t₁ t₂ u : Set α<VAR>p : Prop<VAR>inst✝ : Decidable p<VAR>t : p → Set α<VAR>x : α<GOAL>(∀ (h : p), x ∈ t h) ∧ p ↔ ∃ (h : p), x ∈ t h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>c : β<GOAL>Integrable (fun x => c) μ ↔ c = 0 ∨ μ univ < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>c : β<VAR>this : AEStronglyMeasurable (fun x => c) μ<GOAL>Integrable (fun x => c) μ ↔ c = 0 ∨ μ univ < ⊤
<VAR>ι : Type u<VAR>f✝ : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>f : ι → Ordinal.{max u u_1} → Ordinal.{max u u_1}<VAR>a : Ordinal.{max u u_1}<VAR>h : ∀ (i : ι), f i a = a<VAR>l : List ι<GOAL>List.foldr f a l ≤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : DivisionMonoid α<VAR>a b c d : α<VAR>h : a * b = 1<GOAL>b = 1 / a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a b c : α<VAR>h : a ⋖ b<GOAL>Iio b = Iic a
<VAR>K : Type u_1<VAR>L : Type ?u.592984<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>p q : K[X]<VAR>hpq : q ∣ p<GOAL>(algHomOfDvd hpq) (root p) = root q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>c : Cardinal.{u_3}<GOAL>toPartENat c < ↑n ↔ c < ↑n
<VAR>p q✝ q : ℚ<GOAL>q⁻¹.toNNRat = q.toNNRat⁻¹
<VAR>p q✝ q : ℚ<VAR>hq : q ≤ 0<GOAL>q⁻¹.toNNRat = q.toNNRat⁻¹
<VAR>p q✝ q : ℚ<VAR>hq : 0 ≤ q<GOAL>q⁻¹.toNNRat = q.toNNRat⁻¹
<VAR>u : Level<VAR>α : Q(Type u)<VAR>zα : Q(Zero «$α»)<VAR>pα : Q(PartialOrder «$α»)<VAR>A : Type u_1<VAR>e : A<VAR>n : ℤ<VAR>d : ℕ<VAR>inst✝ : LinearOrderedRing A<VAR>inv : Invertible ↑d<VAR>eq : e = ↑n * ⅟↑d<VAR>h : decide (0 < n) = true<GOAL>0 < e
<VAR>u : Level<VAR>α : Q(Type u)<VAR>zα : Q(Zero «$α»)<VAR>pα : Q(PartialOrder «$α»)<VAR>A : Type u_1<VAR>e : A<VAR>n : ℤ<VAR>d : ℕ<VAR>inst✝ : LinearOrderedRing A<VAR>inv : Invertible ↑d<VAR>eq : e = ↑n * ⅟↑d<VAR>h : decide (0 < n) = true<VAR>pos_invOf_d : 0 < ⅟↑d<GOAL>0 < e
<VAR>u : Level<VAR>α : Q(Type u)<VAR>zα : Q(Zero «$α»)<VAR>pα : Q(PartialOrder «$α»)<VAR>A : Type u_1<VAR>e : A<VAR>n : ℤ<VAR>d : ℕ<VAR>inst✝ : LinearOrderedRing A<VAR>inv : Invertible ↑d<VAR>eq : e = ↑n * ⅟↑d<VAR>h : decide (0 < n) = true<VAR>pos_invOf_d : 0 < ⅟↑d<VAR>pos_n : 0 < ↑n<GOAL>0 < e
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<GOAL>W.φ 2 = C X * W.ψ₂ ^ 2 - C W.Ψ₃
<VAR>X : LocallyRingedSpace<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)<VAR>U : (Opens ↑↑(Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R))).toPresheafedSpace)ᵒᵖ<GOAL>toOpen R (unop U) ≫ ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).val.c.app U = f.unop ≫ X.presheaf.map (homOfLE ⋯).op
<VAR>X : LocallyRingedSpace<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)<VAR>U : (Opens ↑↑(Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R))).toPresheafedSpace)ᵒᵖ<GOAL>(locallyRingedSpaceAdjunction.counit.app (op (CommRingCat.of R))).unop ≫ ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).val.c.app (op ⊤) ≫ ((pushforward CommRingCat ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).val.base).obj X.presheaf).map (homOfLE ⋯).op = f.unop ≫ X.presheaf.map (homOfLE ⋯).op
<VAR>X : LocallyRingedSpace<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)<VAR>U : (Opens ↑↑(Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R))).toPresheafedSpace)ᵒᵖ<GOAL>(locallyRingedSpaceAdjunction.counit.app (op (CommRingCat.of R))).unop ≫ Γ.map ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).op ≫ ((pushforward CommRingCat ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).val.base).obj X.presheaf).map (homOfLE ⋯).op = f.unop ≫ X.presheaf.map (homOfLE ⋯).op
<VAR>X : LocallyRingedSpace<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)<VAR>U : (Opens ↑↑(Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R))).toPresheafedSpace)ᵒᵖ<GOAL>f.unop ≫ ((pushforward CommRingCat ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).val.base).obj X.presheaf).map (homOfLE ⋯).op = f.unop ≫ X.presheaf.map (homOfLE ⋯).op
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝ : Category.{v', u'} A<VAR>F G : Cᵒᵖ ⥤ A<VAR>hG : IsSheaf J G<GOAL>IsSheaf J (presheafHom F G)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝ : Category.{v', u'} A<VAR>F G : Cᵒᵖ ⥤ A<VAR>hG : IsSheaf J G<GOAL>Presieve.IsSheaf J (presheafHom F G)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝ : Category.{v', u'} A<VAR>F G : Cᵒᵖ ⥤ A<VAR>hG : IsSheaf J G<VAR>X : C<VAR>S : Sieve X<VAR>hS : S ∈ J.sieves X<GOAL>Presieve.IsSheafFor (presheafHom F G) S.arrows
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : TopologicalSpace β<VAR>f g : α → β<VAR>hfg : f =ᶠ[ae μ] g<VAR>f' : α → β<VAR>hf'_meas : StronglyMeasurable f'<VAR>hff' : f =ᶠ[ae μ] f'<GOAL>AEStronglyMeasurable' m g μ
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => a + x) '' Iio b = Iio (a + b)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : SemilatticeInf α<VAR>s t : Set α<VAR>a : α<GOAL>a ∈ ↑(lowerClosure (s ⊼ t)) ↔ a ∈ ↑(lowerClosure s ⊓ lowerClosure t)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : SemilatticeInf α<VAR>s t : Set α<VAR>a : α<GOAL>(∃ a_1, (∃ a ∈ s, ∃ b ∈ t, a ⊓ b = a_1) ∧ a ≤ a_1) ↔ a ∈ lowerClosure s ⊓ lowerClosure t
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>a : ℤ<GOAL>multiplicity.Finite (↑p) a ↔ a ≠ 0