ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : Semiring S<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R P<VAR>α' : Type u_7<VAR>M' : Type u_8<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>v : α → M<VAR>v' : α' → M'<VAR>f : α → α'<VAR>l : α' →₀ R<VAR>hf : InjOn f (f ⁻¹' ↑l.support)<GOAL>(Finsupp.total α M R v) (comapDomain f l hf) = ∑ i ∈ l.support.preimage f hf, l (f i) • v i
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : Semiring S<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R P<VAR>α' : Type u_7<VAR>M' : Type u_8<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>v : α → M<VAR>v' : α' → M'<VAR>f : α → α'<VAR>l : α' →₀ R<VAR>hf : InjOn f (f ⁻¹' ↑l.support)<GOAL>((comapDomain f l hf).sum fun i a => a • v i) = ∑ i ∈ l.support.preimage f hf, l (f i) • v i
<VAR>F : Type u₀ → Type u₁ → Type u₂<VAR>inst✝¹ : Bifunctor F<VAR>inst✝ : LawfulBifunctor F<VAR>α₀ α₁ : Type u₀<VAR>β₀ β₁ : Type u₁<VAR>f : α₀ → α₁<VAR>f' : β₀ → β₁<VAR>x : F α₀ β₀<GOAL>snd f' (fst f x) = bimap f f' x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Encodable α<VAR>x y : α<VAR>e : encode x = encode y<GOAL>some x = some y
<VAR>α : Type u_1<VAR>s : α → α → Bool<VAR>a b : α<VAR>l r : List α<GOAL>(match s a b with | true => merge.loop s l (b :: r) [a] | false => merge.loop s (a :: l) r [b]) = if s a b = true then a :: merge.loop s l (b :: r) [] else b :: merge.loop s (a :: l) r []
<VAR>xl xr : Type u<VAR>xR : xr → PGame<VAR>i : xl<VAR>xL : xl → PGame<VAR>j : (xL i).RightMoves<GOAL>((xL i).moveRight j).Subsequent (mk xl xr xL xR)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>inst✝¹ : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝ : Module.Flat R ↥M<VAR>ι : Type u_1<VAR>n : ι → ↥N<VAR>hn : LinearIndependent R n<GOAL>LinearMap.ker (M.mulRightMap n) = ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>inst✝¹ : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝ : Module.Flat R ↥M<VAR>ι : Type u_1<VAR>n : ι → ↥N<VAR>hn : LinearIndependent R n<GOAL>Function.Injective ⇑(M.mulRightMap n)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>inst✝¹ : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝ : Module.Flat R ↥M<VAR>ι : Type u_1<VAR>n : ι → ↥N<VAR>hn : LinearIndependent R n<GOAL>Function.Injective (⇑(M.mulMap N) ∘ ⇑(LinearMap.lTensor (↥M) (Finsupp.total ι (↥N) R n)))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>inst✝¹ : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>inst✝ : Module.Flat R ↥M<VAR>ι : Type u_1<VAR>n : ι → ↥N<VAR>hn : Function.Injective ⇑(Finsupp.total ι (↥N) R n)<GOAL>Function.Injective (⇑(M.mulMap N) ∘ ⇑(LinearMap.lTensor (↥M) (Finsupp.total ι (↥N) R n)))
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<VAR>hG : Group.IsNilpotent G<GOAL>lowerCentralSeries G (Group.nilpotencyClass G) = ⊥
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<VAR>hG : Group.IsNilpotent G<GOAL>lowerCentralSeries G (Nat.find ⋯) = ⊥
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝¹⁸ : SeminormedRing 𝕜<VAR>inst✝¹⁷ : SeminormedRing 𝕜₂<VAR>inst✝¹⁶ : SeminormedRing 𝕜₃<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹⁵ : RingHomIsometric σ₁₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>inst✝¹⁴ : RingHomIsometric σ₂₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝¹³ : RingHomIsometric σ₁₃<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : AddCommGroup E₂<VAR>inst✝¹⁰ : AddCommGroup E₃<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : AddCommGroup G<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜₂ E₂<VAR>inst✝⁵ : Module 𝕜₃ E₃<VAR>inst✝⁴ : Module 𝕜 F<VAR>inst✝³ : Module 𝕜 G<VAR>inst✝² : SMul R ℝ<VAR>inst✝¹ : SMul R ℝ≥0<VAR>inst✝ : IsScalarTower R ℝ≥0 ℝ<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>x : E<VAR>a : ℝ≥0<VAR>ha : 0 < ↑a<VAR>h : ∀ i ∈ s, (p i) x < ↑a<GOAL>(s.sup p) x < ↑a
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝¹⁸ : SeminormedRing 𝕜<VAR>inst✝¹⁷ : SeminormedRing 𝕜₂<VAR>inst✝¹⁶ : SeminormedRing 𝕜₃<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹⁵ : RingHomIsometric σ₁₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>inst✝¹⁴ : RingHomIsometric σ₂₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝¹³ : RingHomIsometric σ₁₃<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : AddCommGroup E₂<VAR>inst✝¹⁰ : AddCommGroup E₃<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : AddCommGroup G<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜₂ E₂<VAR>inst✝⁵ : Module 𝕜₃ E₃<VAR>inst✝⁴ : Module 𝕜 F<VAR>inst✝³ : Module 𝕜 G<VAR>inst✝² : SMul R ℝ<VAR>inst✝¹ : SMul R ℝ≥0<VAR>inst✝ : IsScalarTower R ℝ≥0 ℝ<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>x : E<VAR>a : ℝ≥0<VAR>ha : 0 < ↑a<VAR>h : ∀ i ∈ s, (p i) x < ↑a<GOAL>∀ b ∈ s, ⟨(p b) x, ⋯⟩ < a
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝¹⁸ : SeminormedRing 𝕜<VAR>inst✝¹⁷ : SeminormedRing 𝕜₂<VAR>inst✝¹⁶ : SeminormedRing 𝕜₃<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹⁵ : RingHomIsometric σ₁₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>inst✝¹⁴ : RingHomIsometric σ₂₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝¹³ : RingHomIsometric σ₁₃<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : AddCommGroup E₂<VAR>inst✝¹⁰ : AddCommGroup E₃<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : AddCommGroup G<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜₂ E₂<VAR>inst✝⁵ : Module 𝕜₃ E₃<VAR>inst✝⁴ : Module 𝕜 F<VAR>inst✝³ : Module 𝕜 G<VAR>inst✝² : SMul R ℝ<VAR>inst✝¹ : SMul R ℝ≥0<VAR>inst✝ : IsScalarTower R ℝ≥0 ℝ<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>x : E<VAR>a : ℝ≥0<VAR>ha : 0 < ↑a<VAR>h : ∀ i ∈ s, (p i) x < ↑a<GOAL>⊥ < a
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>H : Subgroup G<VAR>inst✝² : H.IsCommutative<VAR>inst✝¹ : H.FiniteIndex<VAR>α β : ↑(leftTransversals ↑H)<VAR>inst✝ : H.Normal<VAR>h : ↥H<VAR>this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex<GOAL>diff (MonoidHom.id ↥H) α (op ↑h • β) = diff (MonoidHom.id ↥H) α β * h ^ H.index
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>H : Subgroup G<VAR>inst✝² : H.IsCommutative<VAR>inst✝¹ : H.FiniteIndex<VAR>α β : ↑(leftTransversals ↑H)<VAR>inst✝ : H.Normal<VAR>h : ↥H<VAR>this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex<GOAL>(let α_1 := toEquiv ⋯; let β_1 := toEquiv ⋯; ∏ q : G ⧸ H, (MonoidHom.id ↥H) ⟨(↑(α_1 q))⁻¹ * ↑(β_1 q), ⋯⟩) = ∏ x : G ⧸ H, (MonoidHom.id ↥H) ⟨(↑((toEquiv ⋯) x))⁻¹ * ↑((toEquiv ⋯) x), ⋯⟩ * h
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>H : Subgroup G<VAR>inst✝² : H.IsCommutative<VAR>inst✝¹ : H.FiniteIndex<VAR>α β : ↑(leftTransversals ↑H)<VAR>inst✝ : H.Normal<VAR>h : ↥H<VAR>this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex<VAR>q : G ⧸ H<VAR>x✝ : q ∈ Finset.univ<GOAL>(MonoidHom.id ↥H) ⟨(↑((toEquiv ⋯) q))⁻¹ * ↑((toEquiv ⋯) q), ⋯⟩ = (MonoidHom.id ↥H) ⟨(↑((toEquiv ⋯) q))⁻¹ * ↑((toEquiv ⋯) q), ⋯⟩ * h
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>H : Subgroup G<VAR>inst✝² : H.IsCommutative<VAR>inst✝¹ : H.FiniteIndex<VAR>α β : ↑(leftTransversals ↑H)<VAR>inst✝ : H.Normal<VAR>h : ↥H<VAR>this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex<VAR>q : G ⧸ H<VAR>x✝ : q ∈ Finset.univ<GOAL>↑((toEquiv ⋯) q) = ↑((toEquiv ⋯) q) * ↑h
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>H : Subgroup G<VAR>inst✝² : H.IsCommutative<VAR>inst✝¹ : H.FiniteIndex<VAR>α β : ↑(leftTransversals ↑H)<VAR>inst✝ : H.Normal<VAR>h : ↥H<VAR>this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex<VAR>q : G ⧸ H<VAR>x✝ : q ∈ Finset.univ<GOAL>q = op ↑h • q
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>m : ℕ<VAR>inst✝ : NeZero m<VAR>hm : n ∣ m<VAR>a₁✝ a₂✝ : DirichletCharacter R n<VAR>h : (changeLevel hm) a₁✝ = (changeLevel hm) a₂✝<VAR>y : (ZMod n)ˣ<GOAL>a₁✝ ↑y = a₂✝ ↑y
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>m : ℕ<VAR>inst✝ : NeZero m<VAR>hm : n ∣ m<VAR>a₁✝ a₂✝ : DirichletCharacter R n<VAR>h : (changeLevel hm) a₁✝ = (changeLevel hm) a₂✝<VAR>z : (ZMod m)ˣ<GOAL>a₁✝ ↑((ZMod.unitsMap hm) z) = a₂✝ ↑((ZMod.unitsMap hm) z)
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>m : ℕ<VAR>inst✝ : NeZero m<VAR>hm : n ∣ m<VAR>a₁✝ a₂✝ : DirichletCharacter R n<VAR>h : ∀ (a : (ZMod m)ˣ), ((changeLevel hm) a₁✝) ↑a = ((changeLevel hm) a₂✝) ↑a<VAR>z : (ZMod m)ˣ<GOAL>a₁✝ ↑((ZMod.unitsMap hm) z) = a₂✝ ↑((ZMod.unitsMap hm) z)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>p : MvPolynomial (Fin (n + 1)) R<GOAL>(finSuccEquiv R n) p = (eval₂Hom (Polynomial.C.comp C) fun i => Fin.cases Polynomial.X (fun k => Polynomial.C (X k)) i) p
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace β<VAR>μ : ProbabilityMeasure α<VAR>ν : ProbabilityMeasure β<VAR>s : Set (α × β)<VAR>s_mble : MeasurableSet s<GOAL>(μ.prod ν) s = (∫⁻ (y : β), ↑μ ((fun x => (x, y)) ⁻¹' s) ∂↑ν).toNNReal
<VAR>p' : ℕ<VAR>h : lucasLehmerResidue (p' + 2) = 0<GOAL>orderOf (ωUnit (p' + 2)) = 2 ^ (p' + 2)
<VAR>p' : ℕ<VAR>h : lucasLehmerResidue (p' + 2) = 0<GOAL>Nat.Prime 2
<VAR>p' : ℕ<VAR>h : lucasLehmerResidue (p' + 2) = 0<GOAL>¬orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
<VAR>p' : ℕ<VAR>h : lucasLehmerResidue (p' + 2) = 0<GOAL>orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1 + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>hs : autoParam s.Finite _auto✝<GOAL>2 < s.ncard ↔ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : TopologicalSpace α<VAR>s t : Set α<VAR>x : α<GOAL>t ∈ 𝓝[s] x ↔ s =ᶠ[𝓝 x] s ∩ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : Measure α<VAR>κ η : Kernel α β<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : IsSFiniteKernel κ<VAR>f : α × β → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∫⁻ (x : α × β), f x ∂μ ⊗ₘ κ = ∫⁻ (a : α), ∫⁻ (b : β), f (a, b) ∂κ a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : Measure α<VAR>κ η : Kernel α β<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : IsSFiniteKernel κ<VAR>f : α × β → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∫⁻ (b : α), ∫⁻ (c : β), f (b, c) ∂(Kernel.prodMkLeft Unit κ) ((), b) ∂(Kernel.const Unit μ) () = ∫⁻ (a : α), ∫⁻ (b : β), f (a, b) ∂κ a ∂μ
<VAR>x✝ : ZFSet<VAR>s : Set ZFSet<VAR>hs : Small.{u, u + 1} ↑s<VAR>x : ZFSet<GOAL>x ∈ (mk (PSet.mk (Shrink.{u, u + 1} ↑s) fun x => Quotient.out ↑((equivShrink ↑s).symm x))).toSet ↔ x ∈ s
<VAR>x✝ : ZFSet<VAR>s : Set ZFSet<VAR>hs : Small.{u, u + 1} ↑s<VAR>x : ZFSet<GOAL>(Quotient.out x ∈ PSet.mk (Shrink.{u, u + 1} ↑s) fun x => Quotient.out ↑((equivShrink ↑s).symm x)) ↔ x ∈ s
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>‖↑p ^ n‖ = ↑p ^ (-↑n)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s✝ s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>s : Set X<GOAL>closure s \ frontier s = interior s
<VAR>a b c d : Ordinal.{u}<VAR>h₁✝ : a ≤ b<VAR>h₂✝ : 0 ≤ c<VAR>h₁ : a < b<VAR>h₂ : 0 < c<GOAL>c ⨳ a ≤ c ⨳ b
<VAR>a b d : Ordinal.{u}<VAR>h₁✝ : a ≤ b<VAR>h₁ : a < b<VAR>h₂ : 0 ≤ 0<GOAL>0 ⨳ a ≤ 0 ⨳ b
<VAR>a c d : Ordinal.{u}<VAR>h₂✝ : 0 ≤ c<VAR>h₁ : a ≤ a<VAR>h₂ : 0 < c<GOAL>c ⨳ a ≤ c ⨳ a
<VAR>a d : Ordinal.{u}<VAR>h₁ : a ≤ a<VAR>h₂ : 0 ≤ 0<GOAL>0 ⨳ a ≤ 0 ⨳ a
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>w : InfinitePlace K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>0 ≤ (normAtPlace w) x
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>w : InfinitePlace K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>0 ≤ if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝² : MulZeroClass α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : MulPosStrictMono α<VAR>ha : a < 0<VAR>hb : 0 < b<GOAL>a * b < 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ≥0∞<VAR>hμ : μ ≠ 0<VAR>hint : ∫⁻ (a : α), f a ∂μ ≠ ⊤<GOAL>0 < μ {x | ⨍⁻ (a : α), f a ∂μ ≤ f x}
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : Ring B'<VAR>inst✝² : Algebra A B<VAR>inst✝¹ : Algebra A B'<VAR>x : B<VAR>inst✝ : Nontrivial B<GOAL>¬IsUnit (minpoly A x)
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : Ring B'<VAR>inst✝² : Algebra A B<VAR>inst✝¹ : Algebra A B'<VAR>x : B<VAR>inst✝ : Nontrivial B<VAR>this : Nontrivial A<GOAL>¬IsUnit (minpoly A x)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R⟦X⟧<VAR>n : ℕ<GOAL>trunc n.succ f = trunc n f + (Polynomial.monomial n) ((coeff R n) f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>inst✝¹ : TopologicalSpace X<VAR>C₀ C₁ C₂ : Set X<VAR>h₀ : C₀ ⊆ C₁ ∪ C₂<VAR>h₁ : IsClosed C₁<VAR>h₂ : IsClosed C₂<VAR>f₁ : LocallyConstant (↑C₁) Z<VAR>f₂ : LocallyConstant (↑C₂) Z<VAR>inst✝ : DecidablePred fun x => x ∈ C₁<VAR>hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩<VAR>x : ↑C₀<VAR>hx : ↑x ∈ C₂<GOAL>(piecewise' h₀ h₁ h₂ f₁ f₂ hf) x = f₂ ⟨↑x, hx⟩
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>inst✝¹ : TopologicalSpace X<VAR>C₀ C₁ C₂ : Set X<VAR>h₀ : C₀ ⊆ C₁ ∪ C₂<VAR>h₁ : IsClosed C₁<VAR>h₂ : IsClosed C₂<VAR>f₁ : LocallyConstant (↑C₁) Z<VAR>f₂ : LocallyConstant (↑C₂) Z<VAR>inst✝ : DecidablePred fun x => x ∈ C₁<VAR>hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩<VAR>x : ↑C₀<VAR>hx : ↑x ∈ C₂<VAR>this : (j : ↑C₀) → Decidable (j ∈ Subtype.val ⁻¹' C₁) := fun j => decidable_of_iff (↑j ∈ C₁) ⋯<GOAL>(piecewise' h₀ h₁ h₂ f₁ f₂ hf) x = f₂ ⟨↑x, hx⟩
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>inst✝¹ : TopologicalSpace X<VAR>C₀ C₁ C₂ : Set X<VAR>h₀ : C₀ ⊆ C₁ ∪ C₂<VAR>h₁ : IsClosed C₁<VAR>h₂ : IsClosed C₂<VAR>f₁ : LocallyConstant (↑C₁) Z<VAR>f₂ : LocallyConstant (↑C₂) Z<VAR>inst✝ : DecidablePred fun x => x ∈ C₁<VAR>hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩<VAR>x : ↑C₀<VAR>hx : ↑x ∈ C₂<VAR>this : (j : ↑C₀) → Decidable (j ∈ Subtype.val ⁻¹' C₁) := fun j => decidable_of_iff (↑j ∈ C₁) ⋯<GOAL>(comap { toFun := C₂.restrictPreimage Subtype.val, continuous_toFun := ⋯ } f₂) ⟨x, hx⟩ = f₂ ⟨↑x, hx⟩
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>A : Matrix n n R<VAR>c : R<GOAL>(c • A).det = ((diagonal fun x => c) * A).det
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>A : Matrix n n R<VAR>c : R<GOAL>(diagonal fun x => c).det * A.det = c ^ Fintype.card n * A.det
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : SeminormedAddCommGroup α<VAR>r C : ℝ<VAR>f : ℕ → α<VAR>hr : r < 1<VAR>hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n<VAR>a : α<VAR>ha : HasSum f a<VAR>n : ℕ<GOAL>dist (∑ x ∈ Finset.range n, f x) a ≤ C * r ^ n / (1 - r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : SeminormedAddCommGroup α<VAR>r C : ℝ<VAR>f : ℕ → α<VAR>hr : r < 1<VAR>hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n<VAR>a : α<VAR>ha : HasSum f a<VAR>n : ℕ<GOAL>Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 a)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>R : Type u_3<VAR>α : Type u_4<VAR>inst✝² : NonUnitalNonAssocSemiring α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSemiring α<VAR>f g : ι → α<VAR>a a₁ a₂✝ a₂ : α<VAR>h : HasSum f a₁<GOAL>HasSum (fun i => a₂ * f i) (a₂ * a₁)
<VAR>ι : Sort u_1<VAR>κ : ι → Sort u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : AlexandrovDiscrete α<VAR>S : Set (Set α)<VAR>f : ι → Set α<VAR>hS : ∀ s ∈ S, IsClosed s<GOAL>IsClosed (⋃₀ S)
<VAR>ι : Sort u_1<VAR>κ : ι → Sort u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : AlexandrovDiscrete α<VAR>S : Set (Set α)<VAR>f : ι → Set α<VAR>hS : ∀ s ∈ S, IsOpen sᶜ<GOAL>IsOpen (⋂₀ (compl '' S))
<GOAL>0.3678794412⁻¹ < rexp 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>n : ℕ<VAR>_i : Fact (finrank 𝕜 E = n + 1)<VAR>v : E<VAR>hv : v ≠ 0<GOAL>finrank 𝕜 ↥(Submodule.span 𝕜 {v})ᗮ = n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>n : ℕ<VAR>_i : Fact (finrank 𝕜 E = n + 1)<VAR>v : E<VAR>hv : v ≠ 0<VAR>this : FiniteDimensional 𝕜 E<GOAL>finrank 𝕜 ↥(Submodule.span 𝕜 {v})ᗮ = n
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>M N U : ModuleCat R<VAR>X : Type u<GOAL>{ obj := fun S => mk (FreeAlgebra R S), map := fun {X Y} f => (FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.map (𝟙 X) = 𝟙 ({ obj := fun S => mk (FreeAlgebra R S), map := fun {X Y} f => (FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.obj X)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>M N U : ModuleCat R<VAR>X : Type u<GOAL>⇑({ obj := fun S => mk (FreeAlgebra R S), map := fun {X Y} f => (FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.map (𝟙 X)) ∘ FreeAlgebra.ι R = ⇑(𝟙 ({ obj := fun S => mk (FreeAlgebra R S), map := fun {X Y} f => (FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.obj X)) ∘ FreeAlgebra.ι R
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>M N U : ModuleCat R<VAR>X : Type u<GOAL>FreeAlgebra.ι R ∘ 𝟙 X = ⇑(𝟙 (mk (FreeAlgebra R X))) ∘ FreeAlgebra.ι R
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>M N U : ModuleCat R<VAR>X✝ Y✝ Z✝ : Type u<VAR>f✝ : X✝ ⟶ Y✝<VAR>g✝ : Y✝ ⟶ Z✝<GOAL>{ obj := fun S => mk (FreeAlgebra R S), map := fun {X Y} f => (FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.map (f✝ ≫ g✝) = { obj := fun S => mk (FreeAlgebra R S), map := fun {X Y} f => (FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.map f✝ ≫ { obj := fun S => mk (FreeAlgebra R S), map := fun {X Y} f => (FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.map g✝
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>M N U : ModuleCat R<VAR>X✝ Y✝ Z✝ : Type u<VAR>f✝ : X✝ ⟶ Y✝<VAR>g✝ : Y✝ ⟶ Z✝<GOAL>⇑({ obj := fun S => mk (FreeAlgebra R S), map := fun {X Y} f => (FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.map (f✝ ≫ g✝)) ∘ FreeAlgebra.ι R = ⇑({ obj := fun S => mk (FreeAlgebra R S), map := fun {X Y} f => (FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.map f✝ ≫ { obj := fun S => mk (FreeAlgebra R S), map := fun {X Y} f => (FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f) }.map g✝) ∘ FreeAlgebra.ι R
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>M N U : ModuleCat R<VAR>X✝ Y✝ Z✝ : Type u<VAR>f✝ : X✝ ⟶ Y✝<VAR>g✝ : Y✝ ⟶ Z✝<GOAL>FreeAlgebra.ι R ∘ (f✝ ≫ g✝) = ⇑((FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f✝) ≫ (FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ g✝)) ∘ FreeAlgebra.ι R
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>M N U : ModuleCat R<VAR>X✝ Y✝ Z✝ : Type u<VAR>f✝ : X✝ ⟶ Y✝<VAR>g✝ : Y✝ ⟶ Z✝<VAR>x✝ : X✝<GOAL>(FreeAlgebra.ι R ∘ (f✝ ≫ g✝)) x✝ = (⇑((FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f✝) ≫ (FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ g✝)) ∘ FreeAlgebra.ι R) x✝
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>M N U : ModuleCat R<VAR>X✝ Y✝ Z✝ : Type u<VAR>f✝ : X✝ ⟶ Y✝<VAR>g✝ : Y✝ ⟶ Z✝<VAR>x✝ : X✝<GOAL>(FreeAlgebra.ι R ∘ (f✝ ≫ g✝)) x✝ = ((⇑((FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ g✝)) ∘ ⇑((FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f✝))) ∘ FreeAlgebra.ι R) x✝
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>M N U : ModuleCat R<VAR>X✝ Y✝ Z✝ : Type u<VAR>f✝ : X✝ ⟶ Y✝<VAR>g✝ : Y✝ ⟶ Z✝<VAR>x✝ : X✝<GOAL>FreeAlgebra.ι R (g✝ (f✝ x✝)) = ((FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ g✝)) (((FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f✝)) (FreeAlgebra.ι R x✝))
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>M N U : ModuleCat R<VAR>X✝ Y✝ Z✝ : Type u<VAR>f✝ : X✝ ⟶ Y✝<VAR>g✝ : Y✝ ⟶ Z✝<VAR>x✝ : X✝<GOAL>FreeAlgebra.ι R (g✝ (f✝ x✝)) = (FreeAlgebra.ι R ∘ g✝) (f✝ x✝)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>p q : A → Prop<VAR>inst✝²⁴ : Semifield R<VAR>inst✝²³ : StarRing R<VAR>inst✝²² : MetricSpace R<VAR>inst✝²¹ : TopologicalSemiring R<VAR>inst✝²⁰ : ContinuousStar R<VAR>inst✝¹⁹ : Field S<VAR>inst✝¹⁸ : StarRing S<VAR>inst✝¹⁷ : MetricSpace S<VAR>inst✝¹⁶ : TopologicalRing S<VAR>inst✝¹⁵ : ContinuousStar S<VAR>inst✝¹⁴ : TopologicalSpace A<VAR>inst✝¹³ : NonUnitalRing A<VAR>inst✝¹² : StarRing A<VAR>inst✝¹¹ : Module S A<VAR>inst✝¹⁰ : IsScalarTower S A A<VAR>inst✝⁹ : SMulCommClass S A A<VAR>inst✝⁸ : NonUnitalContinuousFunctionalCalculus S q<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Module R A<VAR>inst✝⁵ : IsScalarTower R S A<VAR>inst✝⁴ : StarModule R S<VAR>inst✝³ : ContinuousSMul R S<VAR>inst✝² : CompleteSpace R<VAR>inst✝¹ : IsScalarTower R A A<VAR>inst✝ : SMulCommClass R A A<VAR>f : C(S, R)<VAR>halg : UniformEmbedding ⇑(algebraMap R S)<VAR>h0 : p 0<VAR>h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f<VAR>h_cpct : ∀ (a : A), q a → CompactSpace ↑(σₙ S a)<VAR>a : A<VAR>ha : p a<GOAL>∃ φ, ClosedEmbedding ⇑φ ∧ φ { toContinuousMap := ContinuousMap.restrict (σₙ R a) (ContinuousMap.id R), map_zero' := ⋯ } = a ∧ (∀ (f : C(↑(σₙ R a), R)₀), σₙ R (φ f) = range ⇑f) ∧ ∀ (f : C(↑(σₙ R a), R)₀), p (φ f)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>p q : A → Prop<VAR>inst✝²⁴ : Semifield R<VAR>inst✝²³ : StarRing R<VAR>inst✝²² : MetricSpace R<VAR>inst✝²¹ : TopologicalSemiring R<VAR>inst✝²⁰ : ContinuousStar R<VAR>inst✝¹⁹ : Field S<VAR>inst✝¹⁸ : StarRing S<VAR>inst✝¹⁷ : MetricSpace S<VAR>inst✝¹⁶ : TopologicalRing S<VAR>inst✝¹⁵ : ContinuousStar S<VAR>inst✝¹⁴ : TopologicalSpace A<VAR>inst✝¹³ : NonUnitalRing A<VAR>inst✝¹² : StarRing A<VAR>inst✝¹¹ : Module S A<VAR>inst✝¹⁰ : IsScalarTower S A A<VAR>inst✝⁹ : SMulCommClass S A A<VAR>inst✝⁸ : NonUnitalContinuousFunctionalCalculus S q<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Module R A<VAR>inst✝⁵ : IsScalarTower R S A<VAR>inst✝⁴ : StarModule R S<VAR>inst✝³ : ContinuousSMul R S<VAR>inst✝² : CompleteSpace R<VAR>inst✝¹ : IsScalarTower R A A<VAR>inst✝ : SMulCommClass R A A<VAR>f : C(S, R)<VAR>halg : UniformEmbedding ⇑(algebraMap R S)<VAR>h0 : p 0<VAR>h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f<VAR>h_cpct : ∀ (a : A), q a → CompactSpace ↑(σₙ S a)<VAR>a : A<VAR>ha : p a<GOAL>ClosedEmbedding ⇑(nonUnitalStarAlgHom (cfcₙHom ⋯) ⋯)