ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module R E<VAR>inst✝⁷ : Module R F<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : ContinuousAdd E<VAR>inst✝³ : ContinuousAdd F<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : ContinuousSMul R E<VAR>inst✝ : ContinuousSMul R F<VAR>f : E →ₗ.[R] F<VAR>hf : LinearMap.ker f.toFun = ⊥<VAR>hf' : f.IsClosable<VAR>hcf : LinearMap.ker f.closure.toFun = ⊥<VAR>h1 : (fun a => a.swap) '' ↑f.graph = ⇑↑(LinearEquiv.prodComm R E F).symm ⁻¹' ↑f.graph<VAR>h2 : (fun a => a.swap) '' _root_.closure ↑f.graph = ⇑↑(LinearEquiv.prodComm R E F).symm ⁻¹' _root_.closure ↑f.graph<GOAL>_root_.closure (⇑↑(LinearEquiv.prodComm R E F).symm ⁻¹' ↑f.graph) ⊆ ⇑↑(LinearEquiv.prodComm R E F).symm ⁻¹' _root_.closure ↑f.graph
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>s t : Set α<VAR>a : α<GOAL>s * ↑(lowerClosure t) = ↑(lowerClosure (s * t))
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>s t : Set α<VAR>a : α<GOAL>⋃ a ∈ s, a • ↑(lowerClosure t) = ⋃ i ∈ s, ↑(i • lowerClosure t)
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>a : A<VAR>X : C<GOAL>(shiftFunctor C (0 + a)).obj X = (shiftFunctor C a).obj X
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>a : A<VAR>X : C<GOAL>(shiftFunctorAdd C 0 a).hom.app X = eqToHom ⋯ ≫ (shiftFunctor C a).map ((shiftFunctorZero C A).inv.app X)
<VAR>m n✝ n : ℕ<GOAL>(-1).val = n
<VAR>m n✝ n : ℕ<GOAL>↑(-1) = n
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>mα : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>ρ : Measure (α × Ω)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>f : α × Ω → E<VAR>hf_int : Integrable f ρ<GOAL>Integrable (fun x => ‖∫ (y : Ω), f (x, y) ∂ρ.condKernel x‖) ρ.fst
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>mα : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>ρ : Measure (α × Ω)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>f : α × Ω → E<VAR>hf_int : Integrable f ρ<GOAL>∀ᵐ (a : α) ∂ρ.fst, ‖‖∫ (y : Ω), f (a, y) ∂ρ.condKernel a‖‖ ≤ ‖∫ (y : Ω), ‖f (a, y)‖ ∂ρ.condKernel a‖
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>mα : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>ρ : Measure (α × Ω)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>f : α × Ω → E<VAR>hf_int : Integrable f ρ<VAR>x : α<GOAL>‖‖∫ (y : Ω), f (x, y) ∂ρ.condKernel x‖‖ ≤ ‖∫ (y : Ω), ‖f (x, y)‖ ∂ρ.condKernel x‖
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>mα : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>ρ : Measure (α × Ω)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>f : α × Ω → E<VAR>hf_int : Integrable f ρ<VAR>x : α<GOAL>‖∫ (y : Ω), f (x, y) ∂ρ.condKernel x‖ ≤ ‖∫ (y : Ω), ‖f (x, y)‖ ∂ρ.condKernel x‖
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>mα : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>ρ : Measure (α × Ω)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>f : α × Ω → E<VAR>hf_int : Integrable f ρ<VAR>x : α<GOAL>0 ≤ ∫ (a : Ω), ‖f (x, a)‖ ∂ρ.condKernel x
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a b : R<VAR>n : ℕ<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Semiring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>p q r : R[X]<VAR>C : Type z<VAR>inst✝¹ : Semiring C<VAR>inst✝ : Algebra R C<VAR>f : B →ₐ[R] C<VAR>g : A →ₐ[R] B<GOAL>(mapAlgHom f).comp (mapAlgHom g) = mapAlgHom (f.comp g)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a b : R<VAR>n : ℕ<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Semiring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>p q r : R[X]<VAR>C : Type z<VAR>inst✝¹ : Semiring C<VAR>inst✝ : Algebra R C<VAR>f : B →ₐ[R] C<VAR>g : A →ₐ[R] B<GOAL>∀ (x : A[X]), ((mapAlgHom f).comp (mapAlgHom g)) x = (mapAlgHom (f.comp g)) x
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a b : R<VAR>n : ℕ<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Semiring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>p q r : R[X]<VAR>C : Type z<VAR>inst✝¹ : Semiring C<VAR>inst✝ : Algebra R C<VAR>f : B →ₐ[R] C<VAR>g : A →ₐ[R] B<VAR>x : A[X]<GOAL>((mapAlgHom f).comp (mapAlgHom g)) x = (mapAlgHom (f.comp g)) x
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a b : R<VAR>n : ℕ<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Semiring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>p q r : R[X]<VAR>C : Type z<VAR>inst✝¹ : Semiring C<VAR>inst✝ : Algebra R C<VAR>f : B →ₐ[R] C<VAR>g : A →ₐ[R] B<VAR>x : A[X]<GOAL>map ((↑f).comp ↑g) x = map (↑(f.comp g)) x
<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>F : Type u_3<VAR>inst✝ : Field F<VAR>w : InfinitePlace K<VAR>hw : w.IsReal<VAR>x : K<GOAL>‖(embedding_of_isReal hw) x‖ = w x
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝ : CommMonoid G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>g : ↥(primaryComponent G p)<GOAL>∃ n, orderOf g = p ^ n
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Type u_1<VAR>π : ι✝ → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v : Set α<VAR>ι : Type u_3<VAR>b : α → ι → Set α<VAR>p : α → ι → Prop<VAR>hbasis : ∀ (x : α), (𝓝 x).HasBasis (p x) (b x)<VAR>hconnected : ∀ (x : α) (i : ι), p x i → IsPreconnected (b x i)<GOAL>LocallyConnectedSpace α
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Type u_1<VAR>π : ι✝ → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v : Set α<VAR>ι : Type u_3<VAR>b : α → ι → Set α<VAR>p : α → ι → Prop<VAR>hbasis : ∀ (x : α), (𝓝 x).HasBasis (p x) (b x)<VAR>hconnected : ∀ (x : α) (i : ι), p x i → IsPreconnected (b x i)<GOAL>∀ (x : α), (𝓝 x).HasBasis (fun s => s ∈ 𝓝 x ∧ IsPreconnected s) id
<VAR>C : Type u_2<VAR>inst✝⁵ : Category.{u_1, u_2} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>S₁ S₂ S₃ S₄ : ShortComplex C<VAR>inst✝³ : S₁.HasHomology<VAR>inst✝² : S₂.HasHomology<VAR>inst✝¹ : S₃.HasHomology<VAR>inst✝ : S₄.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>γ : LeftHomologyMapData φ h₁ h₂<GOAL>QuasiIso φ ↔ IsIso γ.φH
<VAR>C : Type u_2<VAR>inst✝⁵ : Category.{u_1, u_2} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>S₁ S₂ S₃ S₄ : ShortComplex C<VAR>inst✝³ : S₁.HasHomology<VAR>inst✝² : S₂.HasHomology<VAR>inst✝¹ : S₃.HasHomology<VAR>inst✝ : S₄.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>γ : LeftHomologyMapData φ h₁ h₂<GOAL>IsIso (h₁.homologyIso.hom ≫ γ.φH ≫ h₂.homologyIso.inv) ↔ IsIso γ.φH
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s t : Set α<VAR>x : α<VAR>f : α ≃o β<GOAL>upperClosure (⇑f '' s) = (UpperSet.map f) (upperClosure s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s t : Set α<VAR>x : α<VAR>f : α ≃o β<GOAL>upperClosure (⇑f '' s) = (UpperSet.map f.symm).symm (upperClosure s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s t : Set α<VAR>x : α<VAR>f : α ≃o β<VAR>x✝ : β<GOAL>x✝ ∈ ↑(upperClosure (⇑f '' s)) ↔ x✝ ∈ ↑((UpperSet.map f.symm).symm (upperClosure s))
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : (i : ι) → AddZeroClass (β i)<VAR>f : Π₀ (i : ι), β i<VAR>p : ι → Prop<VAR>inst✝ : DecidablePred p<VAR>i : ι<GOAL>(filter p f + filter (fun i => ¬p i) f) i = f i
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : (i : ι) → AddZeroClass (β i)<VAR>f : Π₀ (i : ι), β i<VAR>p : ι → Prop<VAR>inst✝ : DecidablePred p<VAR>i : ι<GOAL>((if p i then f i else 0) + if ¬p i then f i else 0) = f i
<VAR>r s : ℝ<VAR>hrs : r.IsConjExponent s<GOAL>{x | ∃ k > 0, beattySeq r k = x} ∆ {x | ∃ k > 0, beattySeq' s k = x} = {n | 0 < n}
<VAR>r s : ℝ<VAR>hrs : r.IsConjExponent s<GOAL>{x | ∃ k > 0, beattySeq r k = x} ∆ {x | ∃ k > 0, beattySeq' s k = x} ⊆ {n | 0 < n}
<VAR>r s : ℝ<VAR>hrs : r.IsConjExponent s<GOAL>{n | 0 < n} ⊆ {x | ∃ k > 0, beattySeq r k = x} ∆ {x | ∃ k > 0, beattySeq' s k = x}
<VAR>r s : ℝ<VAR>hrs : r.IsConjExponent s<VAR>j : ℤ<VAR>hj : 0 < j<GOAL>j ∈ {x | ∃ k > 0, beattySeq r k = x} ∆ {x | ∃ k > 0, beattySeq' s k = x}
<VAR>r s : ℝ<VAR>hrs : r.IsConjExponent s<VAR>j : ℤ<VAR>hj : 0 < j<VAR>hb₁ : ∀ s ≥ 0, j ∈ {x | ∃ k > 0, beattySeq s k = x} ↔ j ∈ {x | ∃ k, beattySeq s k = x}<GOAL>j ∈ {x | ∃ k > 0, beattySeq r k = x} ∆ {x | ∃ k > 0, beattySeq' s k = x}
<VAR>r s : ℝ<VAR>hrs : r.IsConjExponent s<VAR>j : ℤ<VAR>hj : 0 < j<VAR>hb₁ : ∀ s ≥ 0, j ∈ {x | ∃ k > 0, beattySeq s k = x} ↔ j ∈ {x | ∃ k, beattySeq s k = x}<VAR>hb₂ : ∀ s ≥ 0, j ∈ {x | ∃ k > 0, beattySeq' s k = x} ↔ j ∈ {x | ∃ k, beattySeq' s k = x}<GOAL>j ∈ {x | ∃ k > 0, beattySeq r k = x} ∆ {x | ∃ k > 0, beattySeq' s k = x}
<VAR>r s : ℝ<VAR>hrs : r.IsConjExponent s<VAR>j : ℤ<VAR>hj : 0 < j<VAR>hb₁ : ∀ s ≥ 0, j ∈ {x | ∃ k > 0, beattySeq s k = x} ↔ j ∈ {x | ∃ k, beattySeq s k = x}<VAR>hb₂ : ∀ s ≥ 0, j ∈ {x | ∃ k > 0, beattySeq' s k = x} ↔ j ∈ {x | ∃ k, beattySeq' s k = x}<GOAL>j ∈ {x | ∃ k, beattySeq r k = x} ∨ j ∉ {x | ∃ k, beattySeq r k = x}
<VAR>R : Type u<VAR>inst✝ : EuclideanDomain R<VAR>a b c d : R<VAR>hac : c ∣ a<VAR>hbd : d ∣ b<GOAL>a * b / (c * d) = a / c * (b / d)
<VAR>R : Type u<VAR>inst✝ : EuclideanDomain R<VAR>a b d : R<VAR>hbd : d ∣ b<VAR>hac : 0 ∣ a<GOAL>a * b / (0 * d) = a / 0 * (b / d)
<VAR>R : Type u<VAR>inst✝ : EuclideanDomain R<VAR>a b c d : R<VAR>hac : c ∣ a<VAR>hbd : d ∣ b<VAR>hc0 : c ≠ 0<GOAL>a * b / (c * d) = a / c * (b / d)
<VAR>R : Type u<VAR>inst✝ : EuclideanDomain R<VAR>a b c : R<VAR>hac : c ∣ a<VAR>hc0 : c ≠ 0<VAR>hbd : 0 ∣ b<GOAL>a * b / (c * 0) = a / c * (b / 0)
<VAR>R : Type u<VAR>inst✝ : EuclideanDomain R<VAR>a b c d : R<VAR>hac : c ∣ a<VAR>hbd : d ∣ b<VAR>hc0 : c ≠ 0<VAR>hd0 : d ≠ 0<GOAL>a * b / (c * d) = a / c * (b / d)
<VAR>R : Type u<VAR>inst✝ : EuclideanDomain R<VAR>c d : R<VAR>hc0 : c ≠ 0<VAR>hd0 : d ≠ 0<VAR>k1 k2 : R<GOAL>c * k1 * (d * k2) / (c * d) = c * k1 / c * (d * k2 / d)
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>hf : IsBoundedLinearMap 𝕜 f<VAR>hg : IsBoundedLinearMap 𝕜 g<GOAL>IsBoundedLinearMap 𝕜 fun e => f e - g e
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>G : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁸ : NormedField R<VAR>inst✝⁷ : SeminormedAddCommGroup M<VAR>inst✝⁶ : SeminormedAddCommGroup N<VAR>inst✝⁵ : SeminormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace R M<VAR>inst✝³ : NormedSpace R N<VAR>inst✝² : NormedSpace R G<VAR>inst✝¹ : NormedAddCommGroup M'<VAR>inst✝ : NormedSpace R M'<VAR>c cf : R<VAR>hcf : cf ≠ 0<VAR>lif : M →ₗᵢ[R] N<VAR>cg : R<VAR>hcg : cg ≠ 0<VAR>lig : N →ₗᵢ[R] G<GOAL>IsConformalMap ((cg • lig.toContinuousLinearMap).comp (cf • lif.toContinuousLinearMap))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>G : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁸ : NormedField R<VAR>inst✝⁷ : SeminormedAddCommGroup M<VAR>inst✝⁶ : SeminormedAddCommGroup N<VAR>inst✝⁵ : SeminormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace R M<VAR>inst✝³ : NormedSpace R N<VAR>inst✝² : NormedSpace R G<VAR>inst✝¹ : NormedAddCommGroup M'<VAR>inst✝ : NormedSpace R M'<VAR>c cf : R<VAR>hcf : cf ≠ 0<VAR>lif : M →ₗᵢ[R] N<VAR>cg : R<VAR>hcg : cg ≠ 0<VAR>lig : N →ₗᵢ[R] G<GOAL>(cg • lig.toContinuousLinearMap).comp (cf • lif.toContinuousLinearMap) = (cg * cf) • (lig.comp lif).toContinuousLinearMap
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>G : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁸ : NormedField R<VAR>inst✝⁷ : SeminormedAddCommGroup M<VAR>inst✝⁶ : SeminormedAddCommGroup N<VAR>inst✝⁵ : SeminormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace R M<VAR>inst✝³ : NormedSpace R N<VAR>inst✝² : NormedSpace R G<VAR>inst✝¹ : NormedAddCommGroup M'<VAR>inst✝ : NormedSpace R M'<VAR>c cf : R<VAR>hcf : cf ≠ 0<VAR>lif : M →ₗᵢ[R] N<VAR>cg : R<VAR>hcg : cg ≠ 0<VAR>lig : N →ₗᵢ[R] G<GOAL>cg • cf • lig.toContinuousLinearMap.comp lif.toContinuousLinearMap = cg • cf • (lig.comp lif).toContinuousLinearMap
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type w<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Semiring S<VAR>ι : Type u_1<VAR>I J : Ideal R<VAR>coprime : IsCoprime I J<GOAL>(snd (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientMulEquivQuotientProd J coprime) = factor (I * J) J ⋯
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type w<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Semiring S<VAR>ι : Type u_1<VAR>I J : Ideal R<VAR>coprime : IsCoprime I J<GOAL>((snd (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientMulEquivQuotientProd J coprime)).comp (Quotient.mk (I * J)) = (factor (I * J) J ⋯).comp (Quotient.mk (I * J))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g g' : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : LinearOrderedField β<VAR>inst✝ : OrderTopology β<VAR>hk : Tendsto k l atTop<GOAL>SuperpolynomialDecay l k f ↔ ∀ (z : ℕ), IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun a => |k a ^ z * f a|
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g g' : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : LinearOrderedField β<VAR>inst✝ : OrderTopology β<VAR>hk : Tendsto k l atTop<VAR>h : ∀ (z : ℕ), IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun a => |k a ^ z * f a|<VAR>z : ℕ<GOAL>Tendsto (fun a => |k a ^ z * f a|) l (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g g' : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : LinearOrderedField β<VAR>inst✝ : OrderTopology β<VAR>hk : Tendsto k l atTop<VAR>h : ∀ (z : ℕ), IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun a => |k a ^ z * f a|<VAR>z : ℕ<VAR>m : β<VAR>hm : ∀ᶠ (x : β) in Filter.map (fun a => |k a ^ (z + 1) * f a|) l, (fun x x_1 => x ≤ x_1) x m<GOAL>Tendsto (fun a => |k a ^ z * f a|) l (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g g' : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : LinearOrderedField β<VAR>inst✝ : OrderTopology β<VAR>hk : Tendsto k l atTop<VAR>h : ∀ (z : ℕ), IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun a => |k a ^ z * f a|<VAR>z : ℕ<VAR>m : β<VAR>hm : ∀ᶠ (x : β) in Filter.map (fun a => |k a ^ (z + 1) * f a|) l, (fun x x_1 => x ≤ x_1) x m<VAR>h1 : Tendsto (fun x => 0) l (𝓝 0)<GOAL>Tendsto (fun a => |k a ^ z * f a|) l (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g g' : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : LinearOrderedField β<VAR>inst✝ : OrderTopology β<VAR>hk : Tendsto k l atTop<VAR>h : ∀ (z : ℕ), IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun a => |k a ^ z * f a|<VAR>z : ℕ<VAR>m : β<VAR>hm : ∀ᶠ (x : β) in Filter.map (fun a => |k a ^ (z + 1) * f a|) l, (fun x x_1 => x ≤ x_1) x m<VAR>h1 : Tendsto (fun x => 0) l (𝓝 0)<VAR>h2 : Tendsto (fun a => |(k a)⁻¹| * m) l (𝓝 0)<GOAL>Tendsto (fun a => |k a ^ z * f a|) l (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g g' : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : LinearOrderedField β<VAR>inst✝ : OrderTopology β<VAR>hk : Tendsto k l atTop<VAR>h : ∀ (z : ℕ), IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun a => |k a ^ z * f a|<VAR>z : ℕ<VAR>m : β<VAR>hm : ∀ᶠ (x : β) in Filter.map (fun a => |k a ^ (z + 1) * f a|) l, (fun x x_1 => x ≤ x_1) x m<VAR>h1 : Tendsto (fun x => 0) l (𝓝 0)<VAR>h2 : Tendsto (fun a => |(k a)⁻¹| * m) l (𝓝 0)<GOAL>∀ᶠ (x : α) in l, (fun x x_1 => x ≤ x_1) |k x ^ (z + 1) * f x| m → |k x ^ z * f x| ≤ |(k x)⁻¹| * m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g g' : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : LinearOrderedField β<VAR>inst✝ : OrderTopology β<VAR>hk : Tendsto k l atTop<VAR>h : ∀ (z : ℕ), IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun a => |k a ^ z * f a|<VAR>z : ℕ<VAR>m : β<VAR>hm : ∀ᶠ (x : β) in Filter.map (fun a => |k a ^ (z + 1) * f a|) l, (fun x x_1 => x ≤ x_1) x m<VAR>h1 : Tendsto (fun x => 0) l (𝓝 0)<VAR>h2 : Tendsto (fun a => |(k a)⁻¹| * m) l (𝓝 0)<VAR>x : α<VAR>hk0 : k x ≠ 0<VAR>hx : (fun x x_1 => x ≤ x_1) |k x ^ (z + 1) * f x| m<GOAL>|k x ^ z * f x| ≤ |(k x)⁻¹| * m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g g' : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : LinearOrderedField β<VAR>inst✝ : OrderTopology β<VAR>hk : Tendsto k l atTop<VAR>h : ∀ (z : ℕ), IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun a => |k a ^ z * f a|<VAR>z : ℕ<VAR>m : β<VAR>hm : ∀ᶠ (x : β) in Filter.map (fun a => |k a ^ (z + 1) * f a|) l, (fun x x_1 => x ≤ x_1) x m<VAR>h1 : Tendsto (fun x => 0) l (𝓝 0)<VAR>h2 : Tendsto (fun a => |(k a)⁻¹| * m) l (𝓝 0)<VAR>x : α<VAR>hk0 : k x ≠ 0<VAR>hx : (fun x x_1 => x ≤ x_1) |k x ^ (z + 1) * f x| m<GOAL>|k x ^ z * f x| = |(k x)⁻¹| * |k x ^ (z + 1) * f x|
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>I : Ideal R<GOAL>I.jacobson = I ↔ ∃ M, (∀ J ∈ M, J.IsMaximal ∨ J = ⊤) ∧ I = sInf M
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>I : Ideal R<GOAL>(∃ M, (∀ J ∈ M, J.IsMaximal ∨ J = ⊤) ∧ I = sInf M) → I.jacobson = I
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>I : Ideal R<VAR>M : Set (Ideal R)<VAR>hM : ∀ J ∈ M, J.IsMaximal ∨ J = ⊤<VAR>hInf : I = sInf M<GOAL>I.jacobson = I
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>I : Ideal R<VAR>M : Set (Ideal R)<VAR>hM : ∀ J ∈ M, J.IsMaximal ∨ J = ⊤<VAR>hInf : I = sInf M<VAR>x : R<VAR>hx : x ∈ I.jacobson<GOAL>x ∈ I
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>I : Ideal R<VAR>M : Set (Ideal R)<VAR>hM : ∀ J ∈ M, J.IsMaximal ∨ J = ⊤<VAR>hInf : I = sInf M<VAR>x : R<VAR>hx : x ∈ I.jacobson<GOAL>∀ ⦃I : Ideal R⦄, I ∈ M → x ∈ I
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<VAR>a b c : α<VAR>h : a ⩿ b<GOAL>Ioc a b ⊆ {b}
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>H : Subgroup G<VAR>g : ι → G<GOAL>⋃ i ∈ s, g i • ↑H = Set.univ ↔ Set.SurjOn (fun x => ↑(g x)) (↑s) Set.univ
<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>K K' : IntermediateField F L<VAR>inst✝ : Normal F L<VAR>h : K ≤ K'<GOAL>normalClosure F (↥K) L ≤ normalClosure F (↥K') L
<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>K K' : IntermediateField F L<VAR>inst✝ : Normal F L<VAR>h : K ≤ K'<GOAL>⨆ f, map f K ≤ ⨆ f, map f K'
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>a b : α<GOAL>Pairwise (Disjoint on fun n => Ioc (b ^ n) (b ^ (n + 1)))
<VAR>α : Type u<VAR>inst✝ : CanonicallyOrderedCommMonoid α<VAR>a b c d : α<GOAL>a ≤ b * a
<VAR>α : Type u<VAR>inst✝ : CanonicallyOrderedCommMonoid α<VAR>a b c d : α<GOAL>a ≤ a * b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Monoid N<VAR>inst✝ : Monoid P<VAR>l l₁ l₂ : List M<VAR>a : M<VAR>f : ℕ → M<VAR>n : ℕ<GOAL>(map f (range n.succ)).prod = (map f (range n)).prod * f n
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : Monoid γ<VAR>inst✝ : FunLike F β γ<VAR>s : Finset α<VAR>f : α → β<VAR>comm : (↑s).Pairwise fun a b => Commute (f a) (f b)<VAR>m : β<VAR>h : ∀ x ∈ s, f x = m<GOAL>s.noncommProd f comm = m ^ s.card
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : Monoid γ<VAR>inst✝ : FunLike F β γ<VAR>s : Finset α<VAR>f : α → β<VAR>comm : (↑s).Pairwise fun a b => Commute (f a) (f b)<VAR>m : β<VAR>h : ∀ x ∈ s, f x = m<GOAL>m ^ Multiset.card (Multiset.map f s.val) = m ^ s.card
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : Monoid γ<VAR>inst✝ : FunLike F β γ<VAR>s : Finset α<VAR>f : α → β<VAR>comm : (↑s).Pairwise fun a b => Commute (f a) (f b)<VAR>m : β<VAR>h : ∀ x ∈ s, f x = m<GOAL>∀ x ∈ Multiset.map f s.val, x = m
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>A : Type u_2<VAR>inst✝¹ : Field A<VAR>inst✝ : CharZero A<VAR>N : ℕ<VAR>hK : |discr K| ≤ ↑N<GOAL>minkowskiBound K 1 < ↑(boundOfDiscBdd N)
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>A : Type u_2<VAR>inst✝¹ : Field A<VAR>inst✝ : CharZero A<VAR>N : ℕ<VAR>hK : |discr K| ≤ ↑N<VAR>this : boundOfDiscBdd N - 1 < boundOfDiscBdd N<GOAL>minkowskiBound K 1 < ↑(boundOfDiscBdd N)
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>A : Type u_2<VAR>inst✝¹ : Field A<VAR>inst✝ : CharZero A<VAR>N : ℕ<VAR>hK : |discr K| ≤ ↑N<VAR>this : boundOfDiscBdd N - 1 < boundOfDiscBdd N<GOAL>minkowskiBound K 1 ≤ ↑(boundOfDiscBdd N - 1)
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>A : Type u_2<VAR>inst✝¹ : Field A<VAR>inst✝ : CharZero A<VAR>N : ℕ<VAR>hK : |discr K| ≤ ↑N<VAR>this : boundOfDiscBdd N - 1 < boundOfDiscBdd N<GOAL>2⁻¹ ^ NrComplexPlaces K * ↑(sqrt ‖discr K‖₊) * 2 ^ finrank ℚ K ≤ 1 * ↑(sqrt ↑N) * 2 ^ rankOfDiscrBdd N
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<GOAL>discr K ≠ 0
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<GOAL>Algebra.discr ℚ ⇑(integralBasis K) ≠ ↑0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>h : s.ncard < t.ncard<VAR>hs : autoParam s.Finite _auto✝<GOAL>(t \ s).Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>h : s.ncard < t.ncard<VAR>hs : autoParam s.Finite _auto✝<GOAL>¬t ⊆ s
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a✝ a₁ a₂ b✝ b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>a b : E<GOAL>|‖a‖ - ‖b‖| ≤ ‖a / b‖
<VAR>a : ℝ<GOAL>frontier {z | a ≤ z.im} = {z | z.im = a}
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : K<GOAL>(canonicalEmbedding K) x ∈ Submodule.span ℚ (Set.range ⇑(latticeBasis K))
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : K<GOAL>∑ x_1 : Free.ChooseBasisIndex ℤ (𝓞 K), (canonicalEmbedding K) (((integralBasis K).repr x) x_1 • (integralBasis K) x_1) ∈ Submodule.span ℚ (Set.range ⇑(latticeBasis K))
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : K<GOAL>∑ x_1 : Free.ChooseBasisIndex ℤ (𝓞 K), ((integralBasis K).repr x) x_1 • (canonicalEmbedding K) ((integralBasis K) x_1) ∈ Submodule.span ℚ (Set.range ⇑(latticeBasis K))
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : K<VAR>i : Free.ChooseBasisIndex ℤ (𝓞 K)<VAR>x✝ : i ∈ Finset.univ<GOAL>(canonicalEmbedding K) ((integralBasis K) i) ∈ Set.range ⇑(latticeBasis K)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : K<VAR>i : Free.ChooseBasisIndex ℤ (𝓞 K)<VAR>x✝ : i ∈ Finset.univ<GOAL>(latticeBasis K) i ∈ Set.range ⇑(latticeBasis K)