ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring α<VAR>inst✝² : Semiring β<VAR>inst✝¹ : Algebra R α<VAR>inst✝ : Algebra R β<VAR>r : R<VAR>f : α → β<VAR>hf : f 0 = 0<VAR>hf₂ : f ((algebraMap R α) r) = (algebraMap R β) r<GOAL>(diagonal fun m => f ((algebraMap R (n → α)) r m)) = diagonal ((algebraMap R (n → β)) r)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring α<VAR>inst✝² : Semiring β<VAR>inst✝¹ : Algebra R α<VAR>inst✝ : Algebra R β<VAR>r : R<VAR>f : α → β<VAR>hf : f 0 = 0<VAR>hf₂ : f ((algebraMap R α) r) = (algebraMap R β) r<GOAL>n → f ((algebraMap R α) r) = (algebraMap R β) r
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemifield α<VAR>n m : ℕ<VAR>h : n ≤ m<GOAL>1 / (↑m + 1) ≤ 1 / (↑n + 1)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemifield α<VAR>n m : ℕ<VAR>h : n ≤ m<GOAL>0 < ↑n + 1
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemifield α<VAR>n m : ℕ<VAR>h : n ≤ m<GOAL>↑n + 1 ≤ ↑m + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<GOAL>IsPeriodicPt f m x → IsPeriodicPt f n x → IsPeriodicPt f (m.gcd n) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n✝ n : ℕ<VAR>x✝ : IsPeriodicPt f 0 x<VAR>hn : IsPeriodicPt f n x<GOAL>IsPeriodicPt f (Nat.gcd 0 n) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m✝ n✝ m n : ℕ<VAR>x✝ : 0 < m<VAR>ih : IsPeriodicPt f (n % m) x → IsPeriodicPt f m x → IsPeriodicPt f ((n % m).gcd m) x<VAR>hm : IsPeriodicPt f m x<VAR>hn : IsPeriodicPt f n x<GOAL>IsPeriodicPt f (m.gcd n) x
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>X : Cᵒᵖ<GOAL>e.functor.op.map ((NatIso.op e.unitIso).symm.hom.app X) ≫ (NatIso.op e.counitIso).symm.hom.app (e.functor.op.obj X) = 𝟙 (e.functor.op.obj X)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>X : Cᵒᵖ<GOAL>(e.functor.op.map ((NatIso.op e.unitIso).symm.hom.app X) ≫ (NatIso.op e.counitIso).symm.hom.app (e.functor.op.obj X)).unop = (𝟙 (e.functor.op.obj X)).unop
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ φ' : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>γ : LeftHomologyMapData φ h₁ h₂<VAR>γ' : LeftHomologyMapData φ' h₁ h₂<GOAL>leftHomologyMap' (φ + φ') h₁ h₂ = leftHomologyMap' φ h₁ h₂ + leftHomologyMap' φ' h₁ h₂
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : Semiring k<VAR>inst✝³ : Mul G<VAR>inst✝² : Semiring R<VAR>g_hom : Type u_3<VAR>inst✝¹ : FunLike g_hom G R<VAR>inst✝ : MulHomClass g_hom G R<VAR>f : k →+* R<VAR>g : g_hom<VAR>a b : MonoidAlgebra k G<VAR>h_comm : ∀ {x y : G}, y ∈ a.support → Commute (f (b x)) (g y)<GOAL>(liftNC ↑f ⇑g) (a * b) = (liftNC ↑f ⇑g) a * (liftNC ↑f ⇑g) b
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : Semiring k<VAR>inst✝³ : Mul G<VAR>inst✝² : Semiring R<VAR>g_hom : Type u_3<VAR>inst✝¹ : FunLike g_hom G R<VAR>inst✝ : MulHomClass g_hom G R<VAR>f : k →+* R<VAR>g : g_hom<VAR>a b : MonoidAlgebra k G<VAR>h_comm : ∀ {x y : G}, y ∈ a.support → Commute (f (b x)) (g y)<GOAL>(liftNC ↑f ⇑g) (a * b) = (liftNC ↑f ⇑g) (sum a single) * (liftNC ↑f ⇑g) (sum b single)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : Semiring k<VAR>inst✝³ : Mul G<VAR>inst✝² : Semiring R<VAR>g_hom : Type u_3<VAR>inst✝¹ : FunLike g_hom G R<VAR>inst✝ : MulHomClass g_hom G R<VAR>f : k →+* R<VAR>g : g_hom<VAR>a b : MonoidAlgebra k G<VAR>h_comm : ∀ {x y : G}, y ∈ a.support → Commute (f (b x)) (g y)<GOAL>(sum a fun a b_1 => sum b fun a_1 b => ↑f (b_1 * b) * g (a * a_1)) = sum a fun a c => sum b fun a_1 c_1 => ↑f c * g a * (↑f c_1 * g a_1)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : Semiring k<VAR>inst✝³ : Mul G<VAR>inst✝² : Semiring R<VAR>g_hom : Type u_3<VAR>inst✝¹ : FunLike g_hom G R<VAR>inst✝ : MulHomClass g_hom G R<VAR>f : k →+* R<VAR>g : g_hom<VAR>a b : MonoidAlgebra k G<VAR>h_comm : ∀ {x y : G}, y ∈ a.support → Commute (f (b x)) (g y)<VAR>y : G<VAR>hy : y ∈ a.support<VAR>x : G<VAR>_hx : x ∈ b.support<GOAL>(fun a_1 b => ↑f (a y * b) * g (y * a_1)) x (b x) = (fun a_1 c => ↑f (a y) * g y * (↑f c * g a_1)) x (b x)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>K : Type u_3<VAR>inst✝¹ : Field K<VAR>inst✝ : Module K M<VAR>f g : End K M<VAR>p : K[X]<VAR>hp : Squarefree p<VAR>hpf : (aeval f) p = 0<GOAL>f.IsSemisimple
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>K : Type u_3<VAR>inst✝¹ : Field K<VAR>inst✝ : Module K M<VAR>f g : End K M<VAR>p : K[X]<VAR>hp : Squarefree p<VAR>hpf : IsTorsionBySet K[X] (AEval K M f) ↑(Ideal.span {p})<GOAL>f.IsSemisimple
<VAR>R✝ : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : CommRing R✝<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R✝ M<VAR>K : Type u_3<VAR>inst✝¹ : Field K<VAR>inst✝ : Module K M<VAR>f g : End K M<VAR>p : K[X]<VAR>hp : Squarefree p<VAR>hpf : IsTorsionBySet K[X] (AEval K M f) ↑(Ideal.span {p})<VAR>R : Type u_3 := K[X] ⧸ Ideal.span {p}<GOAL>f.IsSemisimple
<VAR>R✝ : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : CommRing R✝<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R✝ M<VAR>K : Type u_3<VAR>inst✝¹ : Field K<VAR>inst✝ : Module K M<VAR>f g : End K M<VAR>p : K[X]<VAR>hp : Squarefree p<VAR>hpf : IsTorsionBySet K[X] (AEval K M f) ↑(Ideal.span {p})<VAR>R : Type u_3 := K[X] ⧸ Ideal.span {p}<VAR>this : IsReduced R<GOAL>f.IsSemisimple
<VAR>R✝ : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : CommRing R✝<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R✝ M<VAR>K : Type u_3<VAR>inst✝¹ : Field K<VAR>inst✝ : Module K M<VAR>f g : End K M<VAR>p : K[X]<VAR>hp : Squarefree p<VAR>hpf : IsTorsionBySet K[X] (AEval K M f) ↑(Ideal.span {p})<VAR>R : Type u_3 := K[X] ⧸ Ideal.span {p}<VAR>this✝ : IsReduced R<VAR>this : FiniteDimensional K R<GOAL>f.IsSemisimple
<VAR>R✝ : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : CommRing R✝<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R✝ M<VAR>K : Type u_3<VAR>inst✝¹ : Field K<VAR>inst✝ : Module K M<VAR>f g : End K M<VAR>p : K[X]<VAR>hp : Squarefree p<VAR>hpf : IsTorsionBySet K[X] (AEval K M f) ↑(Ideal.span {p})<VAR>R : Type u_3 := K[X] ⧸ Ideal.span {p}<VAR>this✝¹ : IsReduced R<VAR>this✝ : FiniteDimensional K R<VAR>this : IsArtinianRing R<GOAL>f.IsSemisimple
<VAR>R✝ : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : CommRing R✝<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R✝ M<VAR>K : Type u_3<VAR>inst✝¹ : Field K<VAR>inst✝ : Module K M<VAR>f g : End K M<VAR>p : K[X]<VAR>hp : Squarefree p<VAR>hpf : IsTorsionBySet K[X] (AEval K M f) ↑(Ideal.span {p})<VAR>R : Type u_3 := K[X] ⧸ Ideal.span {p}<VAR>this✝² : IsReduced R<VAR>this✝¹ : FiniteDimensional K R<VAR>this✝ : IsArtinianRing R<VAR>this : IsSemisimpleRing R<GOAL>f.IsSemisimple
<VAR>R✝ : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : CommRing R✝<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R✝ M<VAR>K : Type u_3<VAR>inst✝¹ : Field K<VAR>inst✝ : Module K M<VAR>f g : End K M<VAR>p : K[X]<VAR>hp : Squarefree p<VAR>hpf : IsTorsionBySet K[X] (AEval K M f) ↑(Ideal.span {p})<VAR>R : Type u_3 := K[X] ⧸ Ideal.span {p}<VAR>this✝³ : IsReduced R<VAR>this✝² : FiniteDimensional K R<VAR>this✝¹ : IsArtinianRing R<VAR>this✝ : IsSemisimpleRing R<VAR>this : Module R (AEval' f) := hpf.module<VAR>e : AEval' f →ₛₗ[Ideal.Quotient.mk (Ideal.span {p})] AEval' f := let __src := AddMonoidHom.id (AEval' f); { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }<GOAL>f.IsSemisimple
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → R<VAR>hPz : P z = 0<GOAL>W'.negY P = -P y
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w₁ w₂ w₃ p₁ p₂ p₃ : ℝ≥0<GOAL>w₁ + w₂ + w₃ = 1 → p₁ ^ ↑w₁ * p₂ ^ ↑w₂ * p₃ ^ ↑w₃ ≤ w₁ * p₁ + w₂ * p₂ + w₃ * p₃
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ γ₁ γ₂ : Cochain K L n<VAR>a : ℤ<VAR>x : R<VAR>p q : ℤ<VAR>hpq : p + n = q<GOAL>((x • γ).shift a).v p q hpq = (x • γ.shift a).v p q hpq
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>f : ((a : α) → Part (β a)) → (a : α) → Part (β a)<VAR>x : α<VAR>h' : ∃ i, (Fix.approx f i x).Dom<VAR>p : ℕ → Prop := fun i => (Fix.approx f i x).Dom<GOAL>Part.fix f x = Fix.approx f (Nat.find h').succ x
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>f : ((a : α) → Part (β a)) → (a : α) → Part (β a)<VAR>x : α<VAR>h' : ∃ i, (Fix.approx f i x).Dom<VAR>p : ℕ → Prop := fun i => (Fix.approx f i x).Dom<VAR>this : p (Nat.find h')<GOAL>Part.fix f x = Fix.approx f (Nat.find h').succ x
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>f : ((a : α) → Part (β a)) → (a : α) → Part (β a)<VAR>x : α<VAR>h' : ∃ i, (Fix.approx f i x).Dom<VAR>p : ℕ → Prop := fun i => (Fix.approx f i x).Dom<VAR>k : ℕ<VAR>this : p (k + ↑Upto.zero)<GOAL>Nat.find h' = k + ↑Upto.zero → (assert (∃ i, (Fix.approx f i x).Dom) fun h => ⋯.fix (fixAux f) Upto.zero x) = Fix.approx f (k + 1) x
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>f : ((a : α) → Part (β a)) → (a : α) → Part (β a)<VAR>x : α<VAR>h' : ∃ i, (Fix.approx f i x).Dom<VAR>p : ℕ → Prop := fun i => (Fix.approx f i x).Dom<VAR>k : ℕ<VAR>this : p (k + ↑Upto.zero)<GOAL>Nat.find h' = k + ↑Upto.zero → ⋯.fix (fixAux f) Upto.zero x = Fix.approx f (k + 1) x
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>β : Type u_2<VAR>inst✝ : TopologicalSpace β<VAR>F : Filter X<VAR>x : X<VAR>h : AccPt x F<VAR>f : X → β<VAR>hf1 : ContinuousAt f x<VAR>hf2 : Function.Injective f<GOAL>AccPt (f x) (Filter.map f F)
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>β : Type u_2<VAR>inst✝ : TopologicalSpace β<VAR>F : Filter X<VAR>x : X<VAR>h : AccPt x F<VAR>f : X → β<VAR>hf1 : ContinuousAt f x<VAR>hf2 : Function.Injective f<GOAL>Filter.map f (𝓝[≠] x ⊓ F) ≤ 𝓝[≠] f x ⊓ Filter.map f F
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>β : Type u_2<VAR>inst✝ : TopologicalSpace β<VAR>F : Filter X<VAR>x : X<VAR>h : AccPt x F<VAR>f : X → β<VAR>hf1 : ContinuousAt f x<VAR>hf2 : Function.Injective f<GOAL>Filter.map f (𝓝[≠] x) ⊓ Filter.map f F ≤ 𝓝[≠] f x ⊓ Filter.map f F
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>β : Type u_2<VAR>inst✝ : TopologicalSpace β<VAR>F : Filter X<VAR>x : X<VAR>h : AccPt x F<VAR>f : X → β<VAR>hf1 : ContinuousAt f x<VAR>hf2 : Function.Injective f<GOAL>Filter.map f (𝓝[≠] x) ≤ 𝓝[≠] f x
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>β : Type u_2<VAR>inst✝ : TopologicalSpace β<VAR>F : Filter X<VAR>x : X<VAR>h : AccPt x F<VAR>f : X → β<VAR>hf1 : ContinuousAt f x<VAR>hf2 : Function.Injective f<GOAL>∀ᶠ (x_1 : X) in 𝓝[≠] x, f x_1 ∈ {f x}ᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : SeminormedRing α<VAR>a : α<VAR>n : ℕ<VAR>h : 0 < n<GOAL>‖a ^ n‖ ≤ ‖a‖ ^ n
<VAR>n : ℕ<VAR>n0 : n ≠ 0<VAR>a : ℕ<GOAL>addOrderOf ↑(a + 1) = n / n.gcd (a + 1)
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : MulAction G α<VAR>inst✝² : MulAction G β<VAR>inst✝¹ : SMul α β<VAR>inst✝ : SMulCommClass G α β<VAR>a : α<VAR>b : β<GOAL>stabilizer G b ≤ stabilizer G (a • b)
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : MulAction G α<VAR>inst✝² : MulAction G β<VAR>inst✝¹ : SMul α β<VAR>inst✝ : SMulCommClass G α β<VAR>a : α<VAR>b : β<GOAL>∀ ⦃x : G⦄, x • b = b → a • x • b = a • b
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>f g : (i : α) → E i<VAR>hf : Memℓp f p<VAR>hg : Memℓp g p<GOAL>Memℓp (f - g) p
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>f g : (i : α) → E i<VAR>hf : Memℓp f p<VAR>hg : Memℓp g p<GOAL>Memℓp (f + -g) p
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>D₁ : Type u₃<VAR>D₂ : Type u₄<VAR>inst✝⁶ : Category.{v₁, u₁} C₁<VAR>inst✝⁵ : Category.{v₂, u₂} C₂<VAR>inst✝⁴ : Category.{v₃, u₃} D₁<VAR>inst✝³ : Category.{v₄, u₄} D₂<VAR>L₁ : C₁ ⥤ D₁<VAR>W₁ : MorphismProperty C₁<VAR>L₂ : C₂ ⥤ D₂<VAR>W₂ : MorphismProperty C₂<VAR>E : Type u₅<VAR>inst✝² : Category.{v₅, u₅} E<VAR>F : C₁ × C₂ ⥤ E<VAR>hF : (W₁.prod W₂).IsInvertedBy F<VAR>inst✝¹ : W₁.ContainsIdentities<VAR>inst✝ : W₂.ContainsIdentities<GOAL>W₂.Q ⋙ (curry.obj (prodLift F hF)).flip = (prodLift₁ F hF).flip
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>D₁ : Type u₃<VAR>D₂ : Type u₄<VAR>inst✝⁶ : Category.{v₁, u₁} C₁<VAR>inst✝⁵ : Category.{v₂, u₂} C₂<VAR>inst✝⁴ : Category.{v₃, u₃} D₁<VAR>inst✝³ : Category.{v₄, u₄} D₂<VAR>L₁ : C₁ ⥤ D₁<VAR>W₁ : MorphismProperty C₁<VAR>L₂ : C₂ ⥤ D₂<VAR>W₂ : MorphismProperty C₂<VAR>E : Type u₅<VAR>inst✝² : Category.{v₅, u₅} E<VAR>F : C₁ × C₂ ⥤ E<VAR>hF : (W₁.prod W₂).IsInvertedBy F<VAR>inst✝¹ : W₁.ContainsIdentities<VAR>inst✝ : W₂.ContainsIdentities<GOAL>W₂.Q ⋙ Construction.lift (prodLift₁ F hF).flip ⋯ = (prodLift₁ F hF).flip
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<VAR>S T : Set R<GOAL>Submodule.span R S * Submodule.span R T = Submodule.span R (S * T)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : IsFilteredOrEmpty C<VAR>D : Type u₁<VAR>inst✝ : Category.{v₁, u₁} D<VAR>L : D ⥤ C<VAR>R : C ⥤ D<VAR>h : L ⊣ R<VAR>X Y : D<VAR>f g : X ⟶ Y<GOAL>f ≫ (h.homEquiv Y (coeq (L.map f) (L.map g))) (coeqHom (L.map f) (L.map g)) = g ≫ (h.homEquiv Y (coeq (L.map f) (L.map g))) (coeqHom (L.map f) (L.map g))
<VAR>A : Type u_1<VAR>inst✝¹² : TopologicalSpace A<VAR>inst✝¹¹ : Ring A<VAR>inst✝¹⁰ : PartialOrder A<VAR>inst✝⁹ : StarRing A<VAR>inst✝⁸ : StarOrderedRing A<VAR>inst✝⁷ : Algebra ℝ A<VAR>inst✝⁶ : TopologicalRing A<VAR>inst✝⁵ : ContinuousStar A<VAR>inst✝⁴ : StarModule ℝ A<VAR>inst✝³ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun x => 0 ≤ x<VAR>inst✝¹ : UniqueContinuousFunctionalCalculus ℝ A<VAR>inst✝ : NonnegSpectrumClass ℝ A<VAR>a : A<VAR>f : ℝ≥0 → ℝ≥0<VAR>ha : autoParam (0 ≤ a) _auto✝<GOAL>cfc f a = cfc (fun x => ↑(f x.toNNReal)) a
<VAR>A : Type u_1<VAR>inst✝¹² : TopologicalSpace A<VAR>inst✝¹¹ : Ring A<VAR>inst✝¹⁰ : PartialOrder A<VAR>inst✝⁹ : StarRing A<VAR>inst✝⁸ : StarOrderedRing A<VAR>inst✝⁷ : Algebra ℝ A<VAR>inst✝⁶ : TopologicalRing A<VAR>inst✝⁵ : ContinuousStar A<VAR>inst✝⁴ : StarModule ℝ A<VAR>inst✝³ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun x => 0 ≤ x<VAR>inst✝¹ : UniqueContinuousFunctionalCalculus ℝ A<VAR>inst✝ : NonnegSpectrumClass ℝ A<VAR>a : A<VAR>f : ℝ≥0 → ℝ≥0<VAR>ha : autoParam (0 ≤ a) _auto✝<VAR>this : CompactSpace ↑(σ ℝ a)<GOAL>cfc f a = cfc (fun x => ↑(f x.toNNReal)) a
<VAR>A : Type u_1<VAR>inst✝¹² : TopologicalSpace A<VAR>inst✝¹¹ : Ring A<VAR>inst✝¹⁰ : PartialOrder A<VAR>inst✝⁹ : StarRing A<VAR>inst✝⁸ : StarOrderedRing A<VAR>inst✝⁷ : Algebra ℝ A<VAR>inst✝⁶ : TopologicalRing A<VAR>inst✝⁵ : ContinuousStar A<VAR>inst✝⁴ : StarModule ℝ A<VAR>inst✝³ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun x => 0 ≤ x<VAR>inst✝¹ : UniqueContinuousFunctionalCalculus ℝ A<VAR>inst✝ : NonnegSpectrumClass ℝ A<VAR>a : A<VAR>f : ℝ≥0 → ℝ≥0<VAR>this : CompactSpace ↑(σ ℝ a)<VAR>ha : 0 ≤ a<GOAL>cfc f a = cfc (fun x => ↑(f x.toNNReal)) a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Ring S<VAR>inst✝⁵ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B<VAR>inst✝² : IsDomain B<VAR>inst✝¹ : Algebra A B<VAR>K : Type u_6<VAR>inst✝ : Field K<VAR>x y : S<VAR>d : ℕ<GOAL>y ∈ Submodule.span R (Set.range fun i => x ^ ↑i) ↔ ∃ f, f.degree < ↑d ∧ y = (aeval x) f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Ring S<VAR>inst✝⁵ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B<VAR>inst✝² : IsDomain B<VAR>inst✝¹ : Algebra A B<VAR>K : Type u_6<VAR>inst✝ : Field K<VAR>x y : S<VAR>d : ℕ<VAR>this : (Set.range fun i => x ^ ↑i) = (fun i => x ^ i) '' ↑(Finset.range d)<GOAL>y ∈ Submodule.span R (Set.range fun i => x ^ ↑i) ↔ ∃ f, f.degree < ↑d ∧ y = (aeval x) f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Ring S<VAR>inst✝⁵ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B<VAR>inst✝² : IsDomain B<VAR>inst✝¹ : Algebra A B<VAR>K : Type u_6<VAR>inst✝ : Field K<VAR>x y : S<VAR>d : ℕ<VAR>this : (Set.range fun i => x ^ ↑i) = (fun i => x ^ i) '' ↑(Finset.range d)<GOAL>(∃ l, (∀ (x : ℕ), d ≤ x → l x = 0) ∧ ∑ x_1 ∈ l.support, (algebraMap R S) (l x_1) * x ^ x_1 = y) ↔ ∃ q, (∀ (m : ℕ), d ≤ m → q m = 0) ∧ y = ∑ x_1 ∈ q.support, (algebraMap R S) (q x_1) * x ^ x_1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Ring S<VAR>inst✝⁵ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B<VAR>inst✝² : IsDomain B<VAR>inst✝¹ : Algebra A B<VAR>K : Type u_6<VAR>inst✝ : Field K<VAR>x y : S<VAR>d : ℕ<VAR>this : (Set.range fun i => x ^ ↑i) = (fun i => x ^ i) '' ↑(Finset.range d)<GOAL>(∃ l, (∀ (x : ℕ), d ≤ x → l x = 0) ∧ ∑ x_1 ∈ l.support, (algebraMap R S) (l x_1) * x ^ x_1 = y) ↔ ∃ q, (∀ (m : ℕ), d ≤ m → q m = 0) ∧ ∑ x_1 ∈ q.support, (algebraMap R S) (q x_1) * x ^ x_1 = y
<VAR>w x✝ y✝ z✝ z : ℝ<VAR>h : 0 < z<VAR>x y : ℝ≥0<VAR>hxy : x < y<GOAL>(fun x => x ^ z) x < (fun x => x ^ z) y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f✝ g : α → β<VAR>μ ν : Measure α<VAR>f : α → β<VAR>hc : MeasurableSpace.CountablyGenerated β<VAR>h : NullMeasurable f μ<VAR>a✝ : Nontrivial β<VAR>inhabited_h : Inhabited β<GOAL>AEMeasurable f μ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f✝ g : α → β<VAR>μ ν : Measure α<VAR>f : α → β<VAR>a✝ : Nontrivial β<VAR>inhabited_h : Inhabited β<VAR>S : Set (Set β)<VAR>hSc : S.Countable<VAR>hc : MeasurableSpace.CountablyGenerated β<VAR>h : NullMeasurable f μ<GOAL>AEMeasurable f μ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f✝ g : α → β<VAR>μ ν : Measure α<VAR>f : α → β<VAR>a✝ : Nontrivial β<VAR>inhabited_h : Inhabited β<VAR>S : Set (Set β)<VAR>hSc : S.Countable<VAR>hc : MeasurableSpace.CountablyGenerated β<VAR>h : NullMeasurable f μ<VAR>T : Set β → Set α<VAR>hTf : ∀ s ∈ S, T s ⊆ f ⁻¹' s<VAR>hTm : ∀ s ∈ S, MeasurableSet (T s)<VAR>hTeq : ∀ s ∈ S, T s =ᶠ[ae μ] f ⁻¹' s<GOAL>AEMeasurable f μ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f✝ g : α → β<VAR>μ ν : Measure α<VAR>f : α → β<VAR>a✝ : Nontrivial β<VAR>inhabited_h : Inhabited β<VAR>S : Set (Set β)<VAR>hSc : S.Countable<VAR>hc : MeasurableSpace.CountablyGenerated β<VAR>h : NullMeasurable f μ<VAR>T : Set β → Set α<VAR>hTf : ∀ s ∈ S, T s ⊆ f ⁻¹' s<VAR>hTm : ∀ s ∈ S, MeasurableSet (T s)<VAR>hTeq : ∀ s ∈ S, T s =ᶠ[ae μ] f ⁻¹' s<VAR>U : Set β → Set α<VAR>hUf : ∀ s ∈ S, U s ⊇ f ⁻¹' s<VAR>hUm : ∀ s ∈ S, MeasurableSet (U s)<VAR>hUeq : ∀ s ∈ S, U s =ᶠ[ae μ] f ⁻¹' s<GOAL>AEMeasurable f μ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f✝ g : α → β<VAR>μ ν : Measure α<VAR>f : α → β<VAR>a✝ : Nontrivial β<VAR>inhabited_h : Inhabited β<VAR>S : Set (Set β)<VAR>hSc : S.Countable<VAR>hc : MeasurableSpace.CountablyGenerated β<VAR>h : NullMeasurable f μ<VAR>T : Set β → Set α<VAR>hTf : ∀ s ∈ S, T s ⊆ f ⁻¹' s<VAR>hTm : ∀ s ∈ S, MeasurableSet (T s)<VAR>hTeq : ∀ s ∈ S, T s =ᶠ[ae μ] f ⁻¹' s<VAR>U : Set β → Set α<VAR>hUf : ∀ s ∈ S, U s ⊇ f ⁻¹' s<VAR>hUm : ∀ s ∈ S, MeasurableSet (U s)<VAR>hUeq : ∀ s ∈ S, U s =ᶠ[ae μ] f ⁻¹' s<VAR>v : Set α := ⋃ s ∈ S, U s \ T s<GOAL>AEMeasurable f μ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f✝ g : α → β<VAR>μ ν : Measure α<VAR>f : α → β<VAR>a✝ : Nontrivial β<VAR>inhabited_h : Inhabited β<VAR>S : Set (Set β)<VAR>hSc : S.Countable<VAR>hc : MeasurableSpace.CountablyGenerated β<VAR>h : NullMeasurable f μ<VAR>T : Set β → Set α<VAR>hTf : ∀ s ∈ S, T s ⊆ f ⁻¹' s<VAR>hTm : ∀ s ∈ S, MeasurableSet (T s)<VAR>hTeq : ∀ s ∈ S, T s =ᶠ[ae μ] f ⁻¹' s<VAR>U : Set β → Set α<VAR>hUf : ∀ s ∈ S, U s ⊇ f ⁻¹' s<VAR>hUm : ∀ s ∈ S, MeasurableSet (U s)<VAR>hUeq : ∀ s ∈ S, U s =ᶠ[ae μ] f ⁻¹' s<VAR>v : Set α := ⋃ s ∈ S, U s \ T s<VAR>hvm : MeasurableSet v<GOAL>AEMeasurable f μ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f✝ g : α → β<VAR>μ ν : Measure α<VAR>f : α → β<VAR>a✝ : Nontrivial β<VAR>inhabited_h : Inhabited β<VAR>S : Set (Set β)<VAR>hSc : S.Countable<VAR>hc : MeasurableSpace.CountablyGenerated β<VAR>h : NullMeasurable f μ<VAR>T : Set β → Set α<VAR>hTf : ∀ s ∈ S, T s ⊆ f ⁻¹' s<VAR>hTm : ∀ s ∈ S, MeasurableSet (T s)<VAR>hTeq : ∀ s ∈ S, T s =ᶠ[ae μ] f ⁻¹' s<VAR>U : Set β → Set α<VAR>hUf : ∀ s ∈ S, U s ⊇ f ⁻¹' s<VAR>hUm : ∀ s ∈ S, MeasurableSet (U s)<VAR>hUeq : ∀ s ∈ S, U s =ᶠ[ae μ] f ⁻¹' s<VAR>v : Set α := ⋃ s ∈ S, U s \ T s<VAR>hvm : MeasurableSet v<VAR>hvμ : μ v = 0<GOAL>AEMeasurable f μ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f✝ g : α → β<VAR>μ ν : Measure α<VAR>f : α → β<VAR>a✝ : Nontrivial β<VAR>inhabited_h : Inhabited β<VAR>S : Set (Set β)<VAR>hSc : S.Countable<VAR>hc : MeasurableSpace.CountablyGenerated β<VAR>h : NullMeasurable f μ<VAR>T : Set β → Set α<VAR>hTf : ∀ s ∈ S, T s ⊆ f ⁻¹' s<VAR>hTm : ∀ s ∈ S, MeasurableSet (T s)<VAR>hTeq : ∀ s ∈ S, T s =ᶠ[ae μ] f ⁻¹' s<VAR>U : Set β → Set α<VAR>hUf : ∀ s ∈ S, U s ⊇ f ⁻¹' s<VAR>hUm : ∀ s ∈ S, MeasurableSet (U s)<VAR>hUeq : ∀ s ∈ S, U s =ᶠ[ae μ] f ⁻¹' s<VAR>v : Set α := ⋃ s ∈ S, U s \ T s<VAR>hvm : MeasurableSet v<VAR>hvμ : μ v = 0<GOAL>Measurable (v.piecewise (fun x => default) f)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f✝ g : α → β<VAR>μ ν : Measure α<VAR>f : α → β<VAR>a✝ : Nontrivial β<VAR>inhabited_h : Inhabited β<VAR>S : Set (Set β)<VAR>hSc : S.Countable<VAR>hc : MeasurableSpace.CountablyGenerated β<VAR>h : NullMeasurable f μ<VAR>T : Set β → Set α<VAR>hTf : ∀ s ∈ S, T s ⊆ f ⁻¹' s<VAR>hTm : ∀ s ∈ S, MeasurableSet (T s)<VAR>hTeq : ∀ s ∈ S, T s =ᶠ[ae μ] f ⁻¹' s<VAR>U : Set β → Set α<VAR>hUf : ∀ s ∈ S, U s ⊇ f ⁻¹' s<VAR>hUm : ∀ s ∈ S, MeasurableSet (U s)<VAR>hUeq : ∀ s ∈ S, U s =ᶠ[ae μ] f ⁻¹' s<VAR>v : Set α := ⋃ s ∈ S, U s \ T s<VAR>hvm : MeasurableSet v<VAR>hvμ : μ v = 0<GOAL>Measurable (v.restrict (v.piecewise (fun x => default) f))