ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝¹ : AddCommGroup α<VAR>inst✝ : AddGroup β<VAR>h : Antiperiodic f c<VAR>n : ℕ<GOAL>f (n • c - x) = (-1) ^ n • f (-x)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>ha : P.a = 0<VAR>hb : P.b = 1<VAR>a✝ : Nontrivial R<GOAL>P.toPoly.Monic
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>K : Type u_4<VAR>K₂ : Type u_5<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>V : Type u_9<VAR>V₂ : Type u_10<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring R₂<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R₂ M₂<VAR>p p' : Submodule R M<VAR>q : Submodule R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_11<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<GOAL>range p.subtype = p
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>inst✝ : FiniteDimensional 𝕜 E<GOAL>(⨆ μ, eigenspace T μ)ᗮ = ⊥
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>hT' : (T.restrict ⋯).IsSymmetric<GOAL>(⨆ μ, eigenspace T μ)ᗮ = ⊥
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>hT' : (T.restrict ⋯).IsSymmetric<VAR>this : Subsingleton ↥(⨆ μ, eigenspace T μ)ᗮ<GOAL>(⨆ μ, eigenspace T μ)ᗮ = ⊥
<VAR>m n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>x✝ : α✝ 0<VAR>q : (i : Fin (n + 1)) → α✝ i<VAR>p : (i : Fin n) → α✝ i.succ<VAR>i : Fin n<VAR>y : α✝ i.succ<VAR>z : α✝ 0<VAR>α : Type u_1<VAR>x : α<VAR>xs : Fin n → α<GOAL>cons x xs = append (cons x elim0) xs ∘ cast ⋯
<VAR>m n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>x✝ : α✝ 0<VAR>q : (i : Fin (n + 1)) → α✝ i<VAR>p : (i : Fin n) → α✝ i.succ<VAR>i✝ : Fin n<VAR>y : α✝ i✝.succ<VAR>z : α✝ 0<VAR>α : Type u_1<VAR>x : α<VAR>xs : Fin n → α<VAR>i : Fin (n + 1)<GOAL>cons x xs i = (append (cons x elim0) xs ∘ cast ⋯) i
<VAR>P : TopCat → Prop<VAR>inst✝ : HasExplicitPullbacks P<VAR>hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Function.Surjective ⇑f<VAR>X Y Z : CompHausLike P<VAR>f : X ⟶ Y<VAR>π : Z ⟶ Y<VAR>hπ : EffectiveEpi π<GOAL>∃ W h, ∃ (_ : EffectiveEpi h), ∃ i, i ≫ π = h ≫ f
<VAR>P : TopCat → Prop<VAR>inst✝ : HasExplicitPullbacks P<VAR>hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Function.Surjective ⇑f<VAR>X Y Z : CompHausLike P<VAR>f : X ⟶ Y<VAR>π : Z ⟶ Y<VAR>hπ : EffectiveEpi π<GOAL>Function.Surjective ⇑(pullback.fst f π)
<VAR>P : TopCat → Prop<VAR>inst✝ : HasExplicitPullbacks P<VAR>hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Function.Surjective ⇑f<VAR>X Y Z : CompHausLike P<VAR>f : X ⟶ Y<VAR>π : Z ⟶ Y<VAR>hπ : EffectiveEpi π<VAR>y : (forget (CompHausLike P)).obj X<VAR>z : (forget (CompHausLike P)).obj Z<VAR>hz : π z = f y<GOAL>∃ a, (pullback.fst f π) a = y
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>x✝ : G<GOAL>x✝ • ⊤ = ⊤
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁵ : EMetricSpace X<VAR>inst✝⁴ : EMetricSpace Y<VAR>C K r✝ : ℝ≥0<VAR>f : X → Y<VAR>s t : Set X<VAR>E : Type u_4<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>x : ι → ℝ<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>dimH (Metric.ball x r) = ↑(Fintype.card ι)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁵ : EMetricSpace X<VAR>inst✝⁴ : EMetricSpace Y<VAR>C K r✝ : ℝ≥0<VAR>f : X → Y<VAR>s t : Set X<VAR>E : Type u_4<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>x : ι → ℝ<VAR>r : ℝ<VAR>hr : 0 < r<VAR>h✝ : IsEmpty ι<GOAL>dimH (Metric.ball x r) = ↑(Fintype.card ι)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁵ : EMetricSpace X<VAR>inst✝⁴ : EMetricSpace Y<VAR>C K r✝ : ℝ≥0<VAR>f : X → Y<VAR>s t : Set X<VAR>E : Type u_4<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>x : ι → ℝ<VAR>r : ℝ<VAR>hr : 0 < r<VAR>h✝ : Nonempty ι<GOAL>dimH (Metric.ball x r) = ↑(Fintype.card ι)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : AddCommMonoid M'<VAR>inst✝⁵ : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i : ι<VAR>c : R<VAR>x✝ : M<VAR>R₁ : Type u_10<VAR>inst✝⁴ : Semiring R₁<VAR>σ : R →+* R₁<VAR>σ' : R₁ →+* R<VAR>inst✝³ : RingHomInvPair σ σ'<VAR>inst✝² : RingHomInvPair σ' σ<VAR>M₁ : Type u_11<VAR>inst✝¹ : AddCommMonoid M₁<VAR>inst✝ : Module R₁ M₁<VAR>f₁ f₂ : M →ₛₗ[σ] M₁<VAR>h : ∀ (i : ι), f₁ (b i) = f₂ (b i)<VAR>x : M<GOAL>f₁ x = f₂ x
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : AddCommMonoid M'<VAR>inst✝⁵ : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i : ι<VAR>c : R<VAR>x✝ : M<VAR>R₁ : Type u_10<VAR>inst✝⁴ : Semiring R₁<VAR>σ : R →+* R₁<VAR>σ' : R₁ →+* R<VAR>inst✝³ : RingHomInvPair σ σ'<VAR>inst✝² : RingHomInvPair σ' σ<VAR>M₁ : Type u_11<VAR>inst✝¹ : AddCommMonoid M₁<VAR>inst✝ : Module R₁ M₁<VAR>f₁ f₂ : M →ₛₗ[σ] M₁<VAR>h : ∀ (i : ι), f₁ (b i) = f₂ (b i)<VAR>x : M<GOAL>f₁ (∑ a ∈ (b.repr x).support, (b.repr x) a • b a) = f₂ (∑ a ∈ (b.repr x).support, (b.repr x) a • b a)
<VAR>a : UnitAddCircle<GOAL>ContinuousOn (cosKernel a) (Ioi 0)
<VAR>a' : ℝ<GOAL>ContinuousOn (cosKernel ↑a') (Ioi 0)
<VAR>a' : ℝ<GOAL>ContinuousOn (fun x => ↑(cosKernel (↑a') x)) (Ioi 0)
<VAR>a' : ℝ<GOAL>ContinuousOn (fun x => jacobiTheta₂ (↑a') (I * ↑x)) (Ioi 0)
<VAR>a' x : ℝ<VAR>hx : x ∈ Ioi 0<GOAL>ContinuousAt (fun x => jacobiTheta₂ (↑a') (I * ↑x)) x
<VAR>a' x : ℝ<VAR>hx : x ∈ Ioi 0<VAR>this : 0 < (I * ↑x).im<GOAL>ContinuousAt (fun x => jacobiTheta₂ (↑a') (I * ↑x)) x
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝³³ : AddCommMonoid M<VAR>inst✝³² : AddCommMonoid N<VAR>inst✝³¹ : CommSemiring R<VAR>inst✝³⁰ : CommSemiring S<VAR>inst✝²⁹ : Algebra R S<VAR>inst✝²⁸ : Module R M<VAR>inst✝²⁷ : Module R N<VAR>inst✝²⁶ : Module S N<VAR>inst✝²⁵ : IsScalarTower R S N<VAR>f✝ : M →ₗ[R] N<VAR>h : IsBaseChange S f✝<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝²⁴ : AddCommMonoid P<VAR>inst✝²³ : Module R P<VAR>inst✝²² : AddCommMonoid Q<VAR>inst✝²¹ : Module S Q<VAR>T : Type u_4<VAR>O : Type u_5<VAR>inst✝²⁰ : CommSemiring T<VAR>inst✝¹⁹ : Algebra R T<VAR>inst✝¹⁸ : Algebra S T<VAR>inst✝¹⁷ : IsScalarTower R S T<VAR>inst✝¹⁶ : AddCommMonoid O<VAR>inst✝¹⁵ : Module R O<VAR>inst✝¹⁴ : Module S O<VAR>inst✝¹³ : Module T O<VAR>inst✝¹² : IsScalarTower S T O<VAR>inst✝¹¹ : IsScalarTower R S O<VAR>inst✝¹⁰ : IsScalarTower R T O<VAR>R' : Type u_6<VAR>S' : Type u_7<VAR>inst✝⁹ : CommSemiring R'<VAR>inst✝⁸ : CommSemiring S'<VAR>inst✝⁷ : Algebra R R'<VAR>inst✝⁶ : Algebra S S'<VAR>inst✝⁵ : Algebra R' S'<VAR>inst✝⁴ : Algebra R S'<VAR>inst✝³ : IsScalarTower R R' S'<VAR>inst✝² : IsScalarTower R S S'<VAR>H : IsPushout R S R' S'<VAR>A : Type u_8<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f g : S' →ₐ[R] A<VAR>h₁ : f.comp (toAlgHom R R' S') = g.comp (toAlgHom R R' S')<VAR>h₂ : f.comp (toAlgHom R S S') = g.comp (toAlgHom R S S')<VAR>x : S'<GOAL>f x = g x
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝³³ : AddCommMonoid M<VAR>inst✝³² : AddCommMonoid N<VAR>inst✝³¹ : CommSemiring R<VAR>inst✝³⁰ : CommSemiring S<VAR>inst✝²⁹ : Algebra R S<VAR>inst✝²⁸ : Module R M<VAR>inst✝²⁷ : Module R N<VAR>inst✝²⁶ : Module S N<VAR>inst✝²⁵ : IsScalarTower R S N<VAR>f✝ : M →ₗ[R] N<VAR>h : IsBaseChange S f✝<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝²⁴ : AddCommMonoid P<VAR>inst✝²³ : Module R P<VAR>inst✝²² : AddCommMonoid Q<VAR>inst✝²¹ : Module S Q<VAR>T : Type u_4<VAR>O : Type u_5<VAR>inst✝²⁰ : CommSemiring T<VAR>inst✝¹⁹ : Algebra R T<VAR>inst✝¹⁸ : Algebra S T<VAR>inst✝¹⁷ : IsScalarTower R S T<VAR>inst✝¹⁶ : AddCommMonoid O<VAR>inst✝¹⁵ : Module R O<VAR>inst✝¹⁴ : Module S O<VAR>inst✝¹³ : Module T O<VAR>inst✝¹² : IsScalarTower S T O<VAR>inst✝¹¹ : IsScalarTower R S O<VAR>inst✝¹⁰ : IsScalarTower R T O<VAR>R' : Type u_6<VAR>S' : Type u_7<VAR>inst✝⁹ : CommSemiring R'<VAR>inst✝⁸ : CommSemiring S'<VAR>inst✝⁷ : Algebra R R'<VAR>inst✝⁶ : Algebra S S'<VAR>inst✝⁵ : Algebra R' S'<VAR>inst✝⁴ : Algebra R S'<VAR>inst✝³ : IsScalarTower R R' S'<VAR>inst✝² : IsScalarTower R S S'<VAR>H : IsPushout R S R' S'<VAR>A : Type u_8<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f g : S' →ₐ[R] A<VAR>h₁ : f.comp (toAlgHom R R' S') = g.comp (toAlgHom R R' S')<VAR>h₂ : f.comp (toAlgHom R S S') = g.comp (toAlgHom R S S')<VAR>x : S'<GOAL>f 0 = g 0
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝³³ : AddCommMonoid M<VAR>inst✝³² : AddCommMonoid N<VAR>inst✝³¹ : CommSemiring R<VAR>inst✝³⁰ : CommSemiring S<VAR>inst✝²⁹ : Algebra R S<VAR>inst✝²⁸ : Module R M<VAR>inst✝²⁷ : Module R N<VAR>inst✝²⁶ : Module S N<VAR>inst✝²⁵ : IsScalarTower R S N<VAR>f✝ : M →ₗ[R] N<VAR>h : IsBaseChange S f✝<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝²⁴ : AddCommMonoid P<VAR>inst✝²³ : Module R P<VAR>inst✝²² : AddCommMonoid Q<VAR>inst✝²¹ : Module S Q<VAR>T : Type u_4<VAR>O : Type u_5<VAR>inst✝²⁰ : CommSemiring T<VAR>inst✝¹⁹ : Algebra R T<VAR>inst✝¹⁸ : Algebra S T<VAR>inst✝¹⁷ : IsScalarTower R S T<VAR>inst✝¹⁶ : AddCommMonoid O<VAR>inst✝¹⁵ : Module R O<VAR>inst✝¹⁴ : Module S O<VAR>inst✝¹³ : Module T O<VAR>inst✝¹² : IsScalarTower S T O<VAR>inst✝¹¹ : IsScalarTower R S O<VAR>inst✝¹⁰ : IsScalarTower R T O<VAR>R' : Type u_6<VAR>S' : Type u_7<VAR>inst✝⁹ : CommSemiring R'<VAR>inst✝⁸ : CommSemiring S'<VAR>inst✝⁷ : Algebra R R'<VAR>inst✝⁶ : Algebra S S'<VAR>inst✝⁵ : Algebra R' S'<VAR>inst✝⁴ : Algebra R S'<VAR>inst✝³ : IsScalarTower R R' S'<VAR>inst✝² : IsScalarTower R S S'<VAR>H : IsPushout R S R' S'<VAR>A : Type u_8<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f g : S' →ₐ[R] A<VAR>h₁ : f.comp (toAlgHom R R' S') = g.comp (toAlgHom R R' S')<VAR>h₂ : f.comp (toAlgHom R S S') = g.comp (toAlgHom R S S')<VAR>x : S'<GOAL>∀ (m : R'), f ((toAlgHom R R' S').toLinearMap m) = g ((toAlgHom R R' S').toLinearMap m)
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝³³ : AddCommMonoid M<VAR>inst✝³² : AddCommMonoid N<VAR>inst✝³¹ : CommSemiring R<VAR>inst✝³⁰ : CommSemiring S<VAR>inst✝²⁹ : Algebra R S<VAR>inst✝²⁸ : Module R M<VAR>inst✝²⁷ : Module R N<VAR>inst✝²⁶ : Module S N<VAR>inst✝²⁵ : IsScalarTower R S N<VAR>f✝ : M →ₗ[R] N<VAR>h : IsBaseChange S f✝<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝²⁴ : AddCommMonoid P<VAR>inst✝²³ : Module R P<VAR>inst✝²² : AddCommMonoid Q<VAR>inst✝²¹ : Module S Q<VAR>T : Type u_4<VAR>O : Type u_5<VAR>inst✝²⁰ : CommSemiring T<VAR>inst✝¹⁹ : Algebra R T<VAR>inst✝¹⁸ : Algebra S T<VAR>inst✝¹⁷ : IsScalarTower R S T<VAR>inst✝¹⁶ : AddCommMonoid O<VAR>inst✝¹⁵ : Module R O<VAR>inst✝¹⁴ : Module S O<VAR>inst✝¹³ : Module T O<VAR>inst✝¹² : IsScalarTower S T O<VAR>inst✝¹¹ : IsScalarTower R S O<VAR>inst✝¹⁰ : IsScalarTower R T O<VAR>R' : Type u_6<VAR>S' : Type u_7<VAR>inst✝⁹ : CommSemiring R'<VAR>inst✝⁸ : CommSemiring S'<VAR>inst✝⁷ : Algebra R R'<VAR>inst✝⁶ : Algebra S S'<VAR>inst✝⁵ : Algebra R' S'<VAR>inst✝⁴ : Algebra R S'<VAR>inst✝³ : IsScalarTower R R' S'<VAR>inst✝² : IsScalarTower R S S'<VAR>H : IsPushout R S R' S'<VAR>A : Type u_8<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f g : S' →ₐ[R] A<VAR>h₁ : f.comp (toAlgHom R R' S') = g.comp (toAlgHom R R' S')<VAR>h₂ : f.comp (toAlgHom R S S') = g.comp (toAlgHom R S S')<VAR>x : S'<GOAL>∀ (s : S) (n : S'), f n = g n → f (s • n) = g (s • n)
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝³³ : AddCommMonoid M<VAR>inst✝³² : AddCommMonoid N<VAR>inst✝³¹ : CommSemiring R<VAR>inst✝³⁰ : CommSemiring S<VAR>inst✝²⁹ : Algebra R S<VAR>inst✝²⁸ : Module R M<VAR>inst✝²⁷ : Module R N<VAR>inst✝²⁶ : Module S N<VAR>inst✝²⁵ : IsScalarTower R S N<VAR>f✝ : M →ₗ[R] N<VAR>h : IsBaseChange S f✝<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝²⁴ : AddCommMonoid P<VAR>inst✝²³ : Module R P<VAR>inst✝²² : AddCommMonoid Q<VAR>inst✝²¹ : Module S Q<VAR>T : Type u_4<VAR>O : Type u_5<VAR>inst✝²⁰ : CommSemiring T<VAR>inst✝¹⁹ : Algebra R T<VAR>inst✝¹⁸ : Algebra S T<VAR>inst✝¹⁷ : IsScalarTower R S T<VAR>inst✝¹⁶ : AddCommMonoid O<VAR>inst✝¹⁵ : Module R O<VAR>inst✝¹⁴ : Module S O<VAR>inst✝¹³ : Module T O<VAR>inst✝¹² : IsScalarTower S T O<VAR>inst✝¹¹ : IsScalarTower R S O<VAR>inst✝¹⁰ : IsScalarTower R T O<VAR>R' : Type u_6<VAR>S' : Type u_7<VAR>inst✝⁹ : CommSemiring R'<VAR>inst✝⁸ : CommSemiring S'<VAR>inst✝⁷ : Algebra R R'<VAR>inst✝⁶ : Algebra S S'<VAR>inst✝⁵ : Algebra R' S'<VAR>inst✝⁴ : Algebra R S'<VAR>inst✝³ : IsScalarTower R R' S'<VAR>inst✝² : IsScalarTower R S S'<VAR>H : IsPushout R S R' S'<VAR>A : Type u_8<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f g : S' →ₐ[R] A<VAR>h₁ : f.comp (toAlgHom R R' S') = g.comp (toAlgHom R R' S')<VAR>h₂ : f.comp (toAlgHom R S S') = g.comp (toAlgHom R S S')<VAR>x : S'<GOAL>∀ (n₁ n₂ : S'), f n₁ = g n₁ → f n₂ = g n₂ → f (n₁ + n₂) = g (n₁ + n₂)
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝ : TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>x : X<GOAL>∑ᶠ (i : ι), f.toPOUFun i x = 1 - ∏ᶠ (i : ι), (1 - (f i) x)
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝ : TopologicalSpace X<VAR>s✝ : Set X<VAR>f : BumpCovering ι X s✝<VAR>x : X<VAR>s : Finset ι := ⋯.toFinset<GOAL>∑ᶠ (i : ι), f.toPOUFun i x = 1 - ∏ᶠ (i : ι), (1 - (f i) x)
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝ : TopologicalSpace X<VAR>s✝ : Set X<VAR>f : BumpCovering ι X s✝<VAR>x : X<VAR>s : Finset ι := ⋯.toFinset<VAR>hs : ↑s = {i | (f i) x ≠ 0}<GOAL>∑ᶠ (i : ι), f.toPOUFun i x = 1 - ∏ᶠ (i : ι), (1 - (f i) x)
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝ : TopologicalSpace X<VAR>s✝ : Set X<VAR>f : BumpCovering ι X s✝<VAR>x : X<VAR>s : Finset ι := ⋯.toFinset<VAR>hs : ↑s = {i | (f i) x ≠ 0}<VAR>A : (support fun i => f.toPOUFun i x) ⊆ ↑s<GOAL>∑ᶠ (i : ι), f.toPOUFun i x = 1 - ∏ᶠ (i : ι), (1 - (f i) x)
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝ : TopologicalSpace X<VAR>s✝ : Set X<VAR>f : BumpCovering ι X s✝<VAR>x : X<VAR>s : Finset ι := ⋯.toFinset<VAR>hs : ↑s = {i | (f i) x ≠ 0}<VAR>A : (support fun i => f.toPOUFun i x) ⊆ ↑s<VAR>B : (mulSupport fun i => 1 - (f i) x) ⊆ ↑s<GOAL>∑ᶠ (i : ι), f.toPOUFun i x = 1 - ∏ᶠ (i : ι), (1 - (f i) x)
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝ : TopologicalSpace X<VAR>s✝ : Set X<VAR>f : BumpCovering ι X s✝<VAR>x : X<VAR>s : Finset ι := ⋯.toFinset<VAR>hs : ↑s = {i | (f i) x ≠ 0}<VAR>A : (support fun i => f.toPOUFun i x) ⊆ ↑s<VAR>B : (mulSupport fun i => 1 - (f i) x) ⊆ ↑s<VAR>this : LinearOrder ι := linearOrderOfSTO WellOrderingRel<GOAL>∑ᶠ (i : ι), f.toPOUFun i x = 1 - ∏ᶠ (i : ι), (1 - (f i) x)
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝ : TopologicalSpace X<VAR>s✝ : Set X<VAR>f : BumpCovering ι X s✝<VAR>x : X<VAR>s : Finset ι := ⋯.toFinset<VAR>hs : ↑s = {i | (f i) x ≠ 0}<VAR>A : (support fun i => f.toPOUFun i x) ⊆ ↑s<VAR>B : (mulSupport fun i => 1 - (f i) x) ⊆ ↑s<VAR>this : LinearOrder ι := linearOrderOfSTO WellOrderingRel<GOAL>∑ i ∈ s, f.toPOUFun i x = ∑ i ∈ s, (f i) x * ∏ j ∈ Finset.filter (fun x => x < i) s, (1 - (f j) x)
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝ : TopologicalSpace X<VAR>s✝ : Set X<VAR>f : BumpCovering ι X s✝<VAR>x : X<VAR>s : Finset ι := ⋯.toFinset<VAR>hs : ↑s = {i | (f i) x ≠ 0}<VAR>A : (support fun i => f.toPOUFun i x) ⊆ ↑s<VAR>B : (mulSupport fun i => 1 - (f i) x) ⊆ ↑s<VAR>this : LinearOrder ι := linearOrderOfSTO WellOrderingRel<VAR>i : ι<VAR>x✝ : i ∈ s<GOAL>f.toPOUFun i x = (f i) x * ∏ j ∈ Finset.filter (fun x => x < i) s, (1 - (f j) x)
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝ : TopologicalSpace X<VAR>s✝ : Set X<VAR>f : BumpCovering ι X s✝<VAR>x : X<VAR>s : Finset ι := ⋯.toFinset<VAR>hs : ↑s = {i | (f i) x ≠ 0}<VAR>A : (support fun i => f.toPOUFun i x) ⊆ ↑s<VAR>B : (mulSupport fun i => 1 - (f i) x) ⊆ ↑s<VAR>this : LinearOrder ι := linearOrderOfSTO WellOrderingRel<VAR>i : ι<VAR>x✝¹ : i ∈ s<VAR>j : ι<VAR>x✝ : WellOrderingRel j i<VAR>hj : (f j) x ≠ 0<GOAL>j ∈ s
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Category.{u_4, u_2} D<VAR>F F' : C ⥤ D<VAR>G : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G<VAR>x : D<GOAL>(adj1.leftAdjointUniq adj2).hom.app (G.obj x) ≫ adj2.counit.app x = adj1.counit.app x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Category.{u_4, u_2} D<VAR>F F' : C ⥤ D<VAR>G : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G<VAR>x : D<GOAL>(adj1.leftAdjointUniq adj2).hom.app (G.obj x) ≫ adj2.counit.app x = (whiskerLeft G (adj1.leftAdjointUniq adj2).hom ≫ adj2.counit).app x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι✝ : Type u_3<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>ι : Type u_4<VAR>inst✝ : Countable ι<GOAL>∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), ↑(ε' i) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι✝ : Type u_3<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>ι : Type u_4<VAR>inst✝ : Countable ι<VAR>r : ℝ≥0∞<VAR>h0r : 0 < r<VAR>hrε : r < ε<GOAL>∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), ↑(ε' i) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι✝ : Type u_3<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>ι : Type u_4<VAR>inst✝ : Countable ι<VAR>x : ℝ≥0<VAR>right✝ : ↑x < ε<VAR>h0r : 0 < ↑x<VAR>hrε : ↑x < ε<GOAL>∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), ↑(ε' i) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι✝ : Type u_3<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>ι : Type u_4<VAR>inst✝ : Countable ι<VAR>x : ℝ≥0<VAR>right✝ : ↑x < ε<VAR>h0r : 0 < ↑x<VAR>hrε : ↑x < ε<VAR>ε' : ι → ℝ≥0<VAR>hp : ∀ (i : ι), 0 < ε' i<VAR>c : ℝ≥0<VAR>hc : HasSum ε' c<VAR>hcr : c < x<GOAL>∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), ↑(ε' i) < ε
<VAR>ι : Type u<VAR>s✝ : Finset ι<VAR>f✝ g : ι → ℝ<VAR>p✝ q : ℝ<VAR>s : Finset ι<VAR>p : ℝ<VAR>w f : ι → ℝ≥0<VAR>hp : 1 ≤ p<GOAL>∑ a ∈ s, w a * f a ≤ (∑ a ∈ s, w a) ^ (1 - p⁻¹) * (∑ a ∈ s, w a * f a ^ p) ^ p⁻¹
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>M : Type u_7<VAR>E : Type u_8<VAR>R : Type u_9<VAR>ι : Type u_10<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : Zero M<VAR>inst✝ : SMulZeroClass R M<VAR>f : ι → X → M<VAR>h✝ : LocallyFinite fun i => support (f i)<VAR>s : ι → X → R<VAR>i : ι<VAR>x : X<VAR>h : f i x = 0<GOAL>(s i • f i) x = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra ℝ A<VAR>f g : ℂ →ₐ[ℝ] A<VAR>h : f I = g I<VAR>x y : ℝ<GOAL>f { re := x, im := y } = g { re := x, im := y }
<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✝¹ : NonUnitalSemiring α<VAR>inst✝ : StarRing α<VAR>M : Matrix m n α<VAR>N : Matrix n l α<GOAL>∀ (i : l) (j : m), (M * N)ᴴ i j = (Nᴴ * Mᴴ) i j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : CompleteLattice β<VAR>γ : Type u_3<VAR>mγ : MeasurableSpace γ<VAR>f : α → γ<VAR>g : γ → β<VAR>hf : MeasurableEmbedding f<GOAL>essSup g (Measure.map f μ) = essSup (g ∘ f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : CompleteLattice β<VAR>γ : Type u_3<VAR>mγ : MeasurableSpace γ<VAR>f : α → γ<VAR>g : γ → β<VAR>hf : MeasurableEmbedding f<GOAL>essSup g (Measure.map f μ) ≤ essSup (g ∘ f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : CompleteLattice β<VAR>γ : Type u_3<VAR>mγ : MeasurableSpace γ<VAR>f : α → γ<VAR>g : γ → β<VAR>hf : MeasurableEmbedding f<VAR>c : β<VAR>h_le : ∀ᶠ (n : β) in map (g ∘ f) (ae μ), n ≤ c<GOAL>∀ᶠ (n : β) in map g (ae (Measure.map f μ)), n ≤ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : CompleteLattice β<VAR>γ : Type u_3<VAR>mγ : MeasurableSpace γ<VAR>f : α → γ<VAR>g : γ → β<VAR>hf : MeasurableEmbedding f<VAR>c : β<VAR>h_le : ∀ᵐ (a : α) ∂μ, (g ∘ f) a ≤ c<GOAL>∀ᵐ (a : γ) ∂Measure.map f μ, g a ≤ c
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : CommRing T<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : Algebra R T<VAR>ι✝ κ✝ : Type w<VAR>inst✝⁴ : Fintype ι✝<VAR>b✝ : Basis ι✝ R S<VAR>inst✝³ : Algebra S T<VAR>inst✝² : IsScalarTower R S T<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>inst✝¹ : Finite ι<VAR>inst✝ : Finite κ<VAR>b : Basis ι R S<VAR>c : Basis κ S T<VAR>x : T<VAR>this✝ : DecidableEq ι<VAR>this : DecidableEq κ<GOAL>(trace R S) ((trace S T) x) = (trace R T) x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : CommRing T<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : Algebra R T<VAR>ι✝ κ✝ : Type w<VAR>inst✝⁴ : Fintype ι✝<VAR>b✝ : Basis ι✝ R S<VAR>inst✝³ : Algebra S T<VAR>inst✝² : IsScalarTower R S T<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>inst✝¹ : Finite ι<VAR>inst✝ : Finite κ<VAR>b : Basis ι R S<VAR>c : Basis κ S T<VAR>x : T<VAR>this✝ : DecidableEq ι<VAR>this : DecidableEq κ<VAR>val✝ : Fintype ι<GOAL>(trace R S) ((trace S T) x) = (trace R T) x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : CommRing T<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : Algebra R T<VAR>ι✝ κ✝ : Type w<VAR>inst✝⁴ : Fintype ι✝<VAR>b✝ : Basis ι✝ R S<VAR>inst✝³ : Algebra S T<VAR>inst✝² : IsScalarTower R S T<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>inst✝¹ : Finite ι<VAR>inst✝ : Finite κ<VAR>b : Basis ι R S<VAR>c : Basis κ S T<VAR>x : T<VAR>this✝ : DecidableEq ι<VAR>this : DecidableEq κ<VAR>val✝¹ : Fintype ι<VAR>val✝ : Fintype κ<GOAL>(trace R S) ((trace S T) x) = (trace R T) x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : CommRing T<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : Algebra R T<VAR>ι✝ κ✝ : Type w<VAR>inst✝⁴ : Fintype ι✝<VAR>b✝ : Basis ι✝ R S<VAR>inst✝³ : Algebra S T<VAR>inst✝² : IsScalarTower R S T<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>inst✝¹ : Finite ι<VAR>inst✝ : Finite κ<VAR>b : Basis ι R S<VAR>c : Basis κ S T<VAR>x : T<VAR>this✝ : DecidableEq ι<VAR>this : DecidableEq κ<VAR>val✝¹ : Fintype ι<VAR>val✝ : Fintype κ<GOAL>∑ i : ι, ((leftMulMatrix b) (∑ i : κ, ((leftMulMatrix c) x).diag i)).diag i = ∑ x_1 : ι, ∑ y : κ, ((leftMulMatrix (b.smulTower c)) x).diag (x_1, y)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : CommRing T<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : Algebra R T<VAR>ι✝ κ✝ : Type w<VAR>inst✝⁴ : Fintype ι✝<VAR>b✝ : Basis ι✝ R S<VAR>inst✝³ : Algebra S T<VAR>inst✝² : IsScalarTower R S T<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>inst✝¹ : Finite ι<VAR>inst✝ : Finite κ<VAR>b : Basis ι R S<VAR>c : Basis κ S T<VAR>x : T<VAR>this✝ : DecidableEq ι<VAR>this : DecidableEq κ<VAR>val✝¹ : Fintype ι<VAR>val✝ : Fintype κ<VAR>i : ι<VAR>x✝ : i ∈ Finset.univ<GOAL>((leftMulMatrix b) (∑ i : κ, ((leftMulMatrix c) x).diag i)).diag i = ∑ y : κ, ((leftMulMatrix (b.smulTower c)) x).diag (i, y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>inst✝ : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t : Set α<GOAL>¬μ (s ∪ t) = ⊤ ↔ ¬(μ s = ⊤ ∨ μ t = ⊤)
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>r : ℝ<GOAL>Submartingale (fun i => stoppedValue f (leastGE f r i)) ℱ μ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>r : ℝ<GOAL>∀ (τ π : Ω → ℕ), IsStoppingTime ℱ τ → IsStoppingTime ℱ π → τ ≤ π → (∃ N, ∀ (x : Ω), π x ≤ N) → ∫ (x : Ω), stoppedValue (fun i => stoppedValue f (leastGE f r i)) τ x ∂μ ≤ ∫ (x : Ω), stoppedValue (fun i => stoppedValue f (leastGE f r i)) π x ∂μ