ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : LinearOrderedCommSemiring β<VAR>inst✝ : ExistsAddOfLE β<VAR>𝒜✝ ℬ✝ : Finset (Finset α)<VAR>a : α<VAR>f f₁ f₂ f₃ f₄ g μ : Finset α → β<VAR>s✝ t✝ u : Finset α<VAR>hu : a ∉ u<VAR>h₁ : 0 ≤ f₁<VAR>h₂ : 0 ≤ f₂<VAR>h₃ : 0 ≤ f₃<VAR>h₄ : 0 ≤ f₄<VAR>h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>hsu : s ⊆ u<VAR>t : Finset α<VAR>htu : t ⊆ u<VAR>this✝² : s ⊆ insert a u<VAR>this✝¹ : t ⊆ insert a u<VAR>this✝ : insert a s ⊆ insert a u<VAR>this : insert a t ⊆ insert a u<VAR>has : a ∉ s<GOAL>collapse 𝒜 a f₁ s * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : LinearOrderedCommSemiring β<VAR>inst✝ : ExistsAddOfLE β<VAR>𝒜✝ ℬ✝ : Finset (Finset α)<VAR>a : α<VAR>f f₁ f₂ f₃ f₄ g μ : Finset α → β<VAR>s✝ t✝ u : Finset α<VAR>hu : a ∉ u<VAR>h₁ : 0 ≤ f₁<VAR>h₂ : 0 ≤ f₂<VAR>h₃ : 0 ≤ f₃<VAR>h₄ : 0 ≤ f₄<VAR>h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>hsu : s ⊆ u<VAR>t : Finset α<VAR>htu : t ⊆ u<VAR>this✝² : s ⊆ insert a u<VAR>this✝¹ : t ⊆ insert a u<VAR>this✝ : insert a s ⊆ insert a u<VAR>this : insert a t ⊆ insert a u<VAR>has : a ∉ s<VAR>hat : a ∉ t<GOAL>collapse 𝒜 a f₁ s * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : LinearOrderedCommSemiring β<VAR>inst✝ : ExistsAddOfLE β<VAR>𝒜✝ ℬ✝ : Finset (Finset α)<VAR>a : α<VAR>f f₁ f₂ f₃ f₄ g μ : Finset α → β<VAR>s✝ t✝ u : Finset α<VAR>hu : a ∉ u<VAR>h₁ : 0 ≤ f₁<VAR>h₂ : 0 ≤ f₂<VAR>h₃ : 0 ≤ f₃<VAR>h₄ : 0 ≤ f₄<VAR>h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>hsu : s ⊆ u<VAR>t : Finset α<VAR>htu : t ⊆ u<VAR>this✝³ : s ⊆ insert a u<VAR>this✝² : t ⊆ insert a u<VAR>this✝¹ : insert a s ⊆ insert a u<VAR>this✝ : insert a t ⊆ insert a u<VAR>has : a ∉ s<VAR>hat : a ∉ t<VAR>this : a ∉ s ∩ t<GOAL>collapse 𝒜 a f₁ s * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : LinearOrderedCommSemiring β<VAR>inst✝ : ExistsAddOfLE β<VAR>𝒜✝ ℬ✝ : Finset (Finset α)<VAR>a : α<VAR>f f₁ f₂ f₃ f₄ g μ : Finset α → β<VAR>s✝ t✝ u : Finset α<VAR>hu : a ∉ u<VAR>h₁ : 0 ≤ f₁<VAR>h₂ : 0 ≤ f₂<VAR>h₃ : 0 ≤ f₃<VAR>h₄ : 0 ≤ f₄<VAR>h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>hsu : s ⊆ u<VAR>t : Finset α<VAR>htu : t ⊆ u<VAR>this✝⁴ : s ⊆ insert a u<VAR>this✝³ : t ⊆ insert a u<VAR>this✝² : insert a s ⊆ insert a u<VAR>this✝¹ : insert a t ⊆ insert a u<VAR>has : a ∉ s<VAR>hat : a ∉ t<VAR>this✝ : a ∉ s ∩ t<VAR>this : a ∉ s ∪ t<GOAL>collapse 𝒜 a f₁ s * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : LinearOrderedCommSemiring β<VAR>inst✝ : ExistsAddOfLE β<VAR>𝒜✝ ℬ✝ : Finset (Finset α)<VAR>a : α<VAR>f f₁ f₂ f₃ f₄ g μ : Finset α → β<VAR>s✝ t✝ u : Finset α<VAR>hu : a ∉ u<VAR>h₁ : 0 ≤ f₁<VAR>h₂ : 0 ≤ f₂<VAR>h₃ : 0 ≤ f₃<VAR>h₄ : 0 ≤ f₄<VAR>h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>hsu : s ⊆ u<VAR>t : Finset α<VAR>htu : t ⊆ u<VAR>this✝⁴ : s ⊆ insert a u<VAR>this✝³ : t ⊆ insert a u<VAR>this✝² : insert a s ⊆ insert a u<VAR>this✝¹ : insert a t ⊆ insert a u<VAR>has : a ∉ s<VAR>hat : a ∉ t<VAR>this✝ : a ∉ s ∩ t<VAR>this : a ∉ s ∪ t<GOAL>((if s ∈ 𝒜 then f₁ s else 0) + if insert a s ∈ 𝒜 then f₁ (insert a s) else 0) * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>ha : a < liminf u f<VAR>hb : b < liminf v f<VAR>ha' : a ≠ ⊤<VAR>hb' : b ≠ ⊤<GOAL>a + b < liminf (u + v) f
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>ha : a < liminf u f<VAR>hb : b < liminf v f<VAR>ha' : a ≠ ⊤<VAR>hb' : b ≠ ⊤<VAR>h : limsup (-(u + v)) f = limsup (-u + -v) f<GOAL>a + b < liminf (u + v) f
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>ha : limsup (-u) f < -a<VAR>hb : limsup (-v) f < -b<VAR>ha' : a ≠ ⊤<VAR>hb' : b ≠ ⊤<VAR>h : limsup (-(u + v)) f = limsup (-u + -v) f<GOAL>limsup (-(u + v)) f < -(a + b)
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>ha : limsup (-u) f < -a<VAR>hb : limsup (-v) f < -b<VAR>ha' : a ≠ ⊤<VAR>hb' : b ≠ ⊤<VAR>h : limsup (-(u + v)) f = limsup (-u + -v) f<GOAL>limsup (-u + -v) f < -a - b
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>hr : r ≠ 0<GOAL>↑(p / r) = ↑p / ↑r
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>completedHurwitzZetaEven₀ (-a) s = completedHurwitzZetaEven₀ a s
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : TopologicalSpace L<VAR>inst✝² : TopologicalSpace X<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>s : Finset ι<VAR>f : ι → α → L<VAR>l : Filter α<VAR>g : ι → L<VAR>inst✝¹ : SemilatticeSup L<VAR>inst✝ : ContinuousSup L<VAR>hne : s.Nonempty<VAR>hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))<GOAL>Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g))
<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>l : List α<VAR>f : α → List β<GOAL>(l.bind f).length = (map (length ∘ f) l).sum
<VAR>J : Type w<VAR>inst✝³ : SmallCategory J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimitsOfShape J C<VAR>inst✝ : MonoidalCategory C<VAR>F G : J ⥤ C<VAR>j j' : J<VAR>f : j ⟶ j'<GOAL>𝟙 (limit F ⊗ limit G) ≫ (limit.π F j' ⊗ limit.π G j') = (limit.π F j ⊗ limit.π G j) ≫ (F.map f ⊗ G.map f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>inst✝⁵ : Fintype α<VAR>inst✝⁴ : DecidableEq α<VAR>inst✝³ : DecidableRel G.Adj<VAR>n : ℕ<VAR>a b c : α<VAR>s : Finset α<VAR>inst✝² : DecidableRel H.Adj<VAR>inst✝¹ : Fintype β<VAR>inst✝ : DecidableEq β<VAR>f : α ↪ β<VAR>hn : n ≠ 1<GOAL>↑((SimpleGraph.map f G).cliqueFinset n) = ↑(map { toFun := map f, inj' := ⋯ } (G.cliqueFinset n))
<VAR>P : Type u_1<VAR>inst✝ : Preorder P<VAR>IF : PrimePair P<GOAL>IF.I.IsProper
<VAR>P : Type u_1<VAR>inst✝ : Preorder P<VAR>IF : PrimePair P<VAR>w : P<VAR>h : w ∈ ↑IF.F<GOAL>IF.I.IsProper
<VAR>P : Type u_1<VAR>inst✝ : Preorder P<VAR>IF : PrimePair P<VAR>w : P<VAR>h : w ∈ ↑IF.F<GOAL>w ∉ IF.I
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x✝ y : G<VAR>n m : ℕ<VAR>x : G<GOAL>x ^ orderOf x = (fun x_1 => x * x_1)^[minimalPeriod (fun x_1 => x * x_1) 1] 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x✝ y : G<VAR>n m : ℕ<VAR>x : G<GOAL>x ^ minimalPeriod (fun x_1 => x * x_1) 1 = (fun x_1 => x ^ minimalPeriod (fun x_2 => x * x_2) 1 * x_1) 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x✝ y : G<VAR>n m : ℕ<VAR>x : G<GOAL>x ^ minimalPeriod (fun x_1 => x * x_1) 1 = x ^ minimalPeriod (fun x_1 => x * x_1) 1 * 1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>p : PrimeSpectrum R<GOAL>support R M = ∅ ↔ Subsingleton M
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>p : PrimeSpectrum R<GOAL>(∀ (m : M), ∃ r ∈ Submonoid.powers 1, r • m = 0) ↔ ∀ (y : M), y = 0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a a₁ a₂ b c : G<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>h : Injective f<VAR>x : G<VAR>hx : x ∈ ker f<GOAL>f x = f 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a a₁ a₂ b c : G<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>h : Injective f<VAR>x : G<VAR>hx : x ∈ ker f<GOAL>f x = 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a a₁ a₂ b c : G<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>h : Injective f<VAR>x : G<GOAL>x ∈ IsSubgroup.trivial G → x ∈ ker f
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<GOAL>l.rotate (l.length * n) = l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : LinearOrderedField 𝕜<VAR>t : Finset (α × β × γ)<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>x : α × β × γ<VAR>ε : 𝕜<VAR>inst✝⁶ : DecidableEq α<VAR>inst✝⁵ : DecidableEq β<VAR>inst✝⁴ : DecidableEq γ<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>inst✝¹ : Fintype γ<VAR>inst✝ : NoAccidental t<GOAL>(graph t).cliqueFinset 3 = map toTriangle t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>𝔗 : Set (Set γ)<VAR>f : γ → α<VAR>hf : MapsTo (fun x => f '' x) 𝔗 𝔖<GOAL>UniformContinuous fun g => (ofFun 𝔗) ((toFun 𝔖) g ∘ f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>𝔗 : Set (Set γ)<VAR>f : γ → α<VAR>hf : MapsTo (fun x => f '' x) 𝔗 𝔖<GOAL>∀ i ∈ 𝔗, ∀ i_2 ∈ 𝓤 β, Tendsto (fun x => ((ofFun 𝔗) ((toFun 𝔖) x.1 ∘ f), (ofFun 𝔗) ((toFun 𝔖) x.2 ∘ f))) (⨅ s ∈ 𝔖, ⨅ V ∈ 𝓤 β, 𝓟 (UniformOnFun.gen 𝔖 s V)) (𝓟 (UniformOnFun.gen 𝔗 i i_2))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>𝔗 : Set (Set γ)<VAR>f : γ → α<VAR>hf : MapsTo (fun x => f '' x) 𝔗 𝔖<VAR>t : Set γ<VAR>ht : t ∈ 𝔗<VAR>V : Set (β × β)<VAR>hV : V ∈ 𝓤 β<GOAL>Tendsto (fun x => ((ofFun 𝔗) ((toFun 𝔖) x.1 ∘ f), (ofFun 𝔗) ((toFun 𝔖) x.2 ∘ f))) (𝓟 (UniformOnFun.gen 𝔖 (f '' t) V)) (𝓟 (UniformOnFun.gen 𝔗 t V))
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>β : Type u_3<VAR>α : ι → Type u<VAR>U : (i : ι) → UniformSpace (α i)<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : Nonempty ι<VAR>l : Filter ((i : ι) → α i)<GOAL>Cauchy l ↔ ∀ (i : ι), Cauchy (map (eval i) l)
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>κ : Type u_1<VAR>inst✝ : (i : ι) → Zero (β i)<VAR>h : κ → ι<VAR>h' : ι → κ<VAR>hh' : Function.LeftInverse h' h<VAR>i✝ : κ<GOAL>(comapDomain' h hh' 0) i✝ = 0 i✝
<VAR>R✝ : Type u_1<VAR>inst✝¹ : Semiring R✝<VAR>r✝ : R✝<VAR>f✝ : R✝[X]<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>r : R<VAR>f g : R[X]<VAR>h : (taylor (-r)) ((taylor r) f) = (taylor (-r)) ((taylor r) g)<GOAL>f = g
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝⁹ : Fintype n<VAR>inst✝⁸ : Finite m<VAR>inst✝⁷ : DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝⁶ : AddCommMonoid M₁<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>G : Type u_7<VAR>inst✝² : Group G<VAR>inst✝¹ : DistribMulAction G M₂<VAR>inst✝ : SMulCommClass G R M₂<VAR>g : G<VAR>f : M₁ →ₗ[R] M₂<VAR>i✝ : m<VAR>j✝ : n<GOAL>(toMatrix v₁ (g • v₂)) f i✝ j✝ = (toMatrix v₁ v₂) (DistribMulAction.toLinearMap R M₂ g⁻¹ ∘ₗ f) i✝ j✝
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝⁹ : Fintype n<VAR>inst✝⁸ : Finite m<VAR>inst✝⁷ : DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝⁶ : AddCommMonoid M₁<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>G : Type u_7<VAR>inst✝² : Group G<VAR>inst✝¹ : DistribMulAction G M₂<VAR>inst✝ : SMulCommClass G R M₂<VAR>g : G<VAR>f : M₁ →ₗ[R] M₂<VAR>i✝ : m<VAR>j✝ : n<GOAL>((g • v₂).repr (f (v₁ j✝))) i✝ = (v₂.repr ((DistribMulAction.toLinearMap R M₂ g⁻¹ ∘ₗ f) (v₁ j✝))) i✝
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R<GOAL>∀ᵐ (ω : Ω) ∂μ, ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω✝ : Ω<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R<VAR>ω : Ω<VAR>h₁ : ∀ (a b : ℚ), a < b → upcrossings (↑a) (↑b) f ω < ⊤<VAR>h₂ : liminf (fun n => ↑‖f n ω‖₊) atTop < ⊤<GOAL>∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)
<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>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K F<VAR>ι : Type w<VAR>inst✝² : Finite ι<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsDomain S<VAR>b : Basis ι R S<VAR>x : S<GOAL>(norm R) x = 0 ↔ x = 0
<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>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K F<VAR>ι : Type w<VAR>inst✝² : Finite ι<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsDomain S<VAR>b : Basis ι R S<VAR>x : S<VAR>this : Module.Free R S<GOAL>(norm R) x = 0 ↔ x = 0
<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>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K F<VAR>ι : Type w<VAR>inst✝² : Finite ι<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsDomain S<VAR>b : Basis ι R S<VAR>x : S<VAR>this✝ : Module.Free R S<VAR>this : Module.Finite R S<GOAL>(norm R) x = 0 ↔ x = 0
<VAR>d : ℤ<VAR>h₀ : 0 < d<VAR>a : Solution₁ d<GOAL>∃ b, 0 < b.x ∧ 0 ≤ b.y ∧ a ∈ {b, b⁻¹, -b, -b⁻¹}
<VAR>α : Type u<VAR>L✝ L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>β : Type v<VAR>f : α → β<VAR>x y : FreeGroup α<VAR>g : FreeGroup α →* FreeGroup β<VAR>hg : ∀ (x : α), g (FreeGroup.of x) = FreeGroup.of (f x)<VAR>x✝ : FreeGroup α<VAR>L : List (α × Bool)<GOAL>g (Quot.mk Red.Step L) = (map f) (Quot.mk Red.Step L)
<VAR>α : Type u<VAR>x y : FreeSemigroup α<GOAL>(x * y).length = x.length + y.length
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LE α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>a ≤ 1 * b ↔ a ≤ b
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : (i : ι) → AddCommMonoid (M i)<VAR>inst✝⁶ : (i : ι) → Module R (M i)<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Semiring S<VAR>inst✝¹ : Module S N<VAR>inst✝ : SMulCommClass R S N<VAR>F : (i : ι) → M i →ₗ[R] N<VAR>c : R<VAR>f : Π₀ (i : ι), M i<GOAL>(sumAddHom fun i => (F i).toAddMonoidHom) (c • f) = c • (sumAddHom fun i => (F i).toAddMonoidHom) f
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : (i : ι) → AddCommMonoid (M i)<VAR>inst✝⁶ : (i : ι) → Module R (M i)<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Semiring S<VAR>inst✝¹ : Module S N<VAR>inst✝ : SMulCommClass R S N<VAR>F : (i : ι) → M i →ₗ[R] N<VAR>c : R<VAR>f : Π₀ (i : ι), M i<GOAL>(sumAddHom fun i => (F i).toAddMonoidHom) (c • 0) = c • (sumAddHom fun i => (F i).toAddMonoidHom) 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : (i : ι) → AddCommMonoid (M i)<VAR>inst✝⁶ : (i : ι) → Module R (M i)<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Semiring S<VAR>inst✝¹ : Module S N<VAR>inst✝ : SMulCommClass R S N<VAR>F : (i : ι) → M i →ₗ[R] N<VAR>c : R<VAR>f : Π₀ (i : ι), M i<GOAL>∀ (i : ι) (b : M i) (f : Π₀ (i : ι), M i), f i = 0 → b ≠ 0 → (sumAddHom fun i => (F i).toAddMonoidHom) (c • f) = c • (sumAddHom fun i => (F i).toAddMonoidHom) f → (sumAddHom fun i => (F i).toAddMonoidHom) (c • (single i b + f)) = c • (sumAddHom fun i => (F i).toAddMonoidHom) (single i b + f)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : (i : ι) → AddCommMonoid (M i)<VAR>inst✝⁶ : (i : ι) → Module R (M i)<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Semiring S<VAR>inst✝¹ : Module S N<VAR>inst✝ : SMulCommClass R S N<VAR>F : (Π₀ (i : ι), M i) →ₗ[R] N<GOAL>{ toFun := fun F => { toFun := ⇑(sumAddHom fun i => (F i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }.toFun ((fun F i => F ∘ₗ lsingle i) F) = F
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : (i : ι) → AddCommMonoid (M i)<VAR>inst✝⁶ : (i : ι) → Module R (M i)<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Semiring S<VAR>inst✝¹ : Module S N<VAR>inst✝ : SMulCommClass R S N<VAR>F : (Π₀ (i : ι), M i) →ₗ[R] N<VAR>i : ι<GOAL>{ toFun := fun F => { toFun := ⇑(sumAddHom fun i => (F i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }.toFun ((fun F i => F ∘ₗ lsingle i) F) ∘ₗ lsingle i = F ∘ₗ lsingle i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : (i : ι) → AddCommMonoid (M i)<VAR>inst✝⁶ : (i : ι) → Module R (M i)<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Semiring S<VAR>inst✝¹ : Module S N<VAR>inst✝ : SMulCommClass R S N<VAR>F G : (i : ι) → M i →ₗ[R] N<GOAL>(fun F => { toFun := ⇑(sumAddHom fun i => (F i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ }) (F + G) = (fun F => { toFun := ⇑(sumAddHom fun i => (F i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ }) F + (fun F => { toFun := ⇑(sumAddHom fun i => (F i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ }) G
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : (i : ι) → AddCommMonoid (M i)<VAR>inst✝⁶ : (i : ι) → Module R (M i)<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Semiring S<VAR>inst✝¹ : Module S N<VAR>inst✝ : SMulCommClass R S N<VAR>F G : (i : ι) → M i →ₗ[R] N<VAR>i : ι<GOAL>(fun F => { toFun := ⇑(sumAddHom fun i => (F i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ }) (F + G) ∘ₗ lsingle i = ((fun F => { toFun := ⇑(sumAddHom fun i => (F i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ }) F + (fun F => { toFun := ⇑(sumAddHom fun i => (F i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ }) G) ∘ₗ lsingle i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : (i : ι) → AddCommMonoid (M i)<VAR>inst✝⁶ : (i : ι) → Module R (M i)<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Semiring S<VAR>inst✝¹ : Module S N<VAR>inst✝ : SMulCommClass R S N<VAR>c : S<VAR>F : (i : ι) → M i →ₗ[R] N<GOAL>{ toFun := fun F => { toFun := ⇑(sumAddHom fun i => (F i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯ }.toFun (c • F) = (RingHom.id S) c • { toFun := fun F => { toFun := ⇑(sumAddHom fun i => (F i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯ }.toFun F
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : (i : ι) → AddCommMonoid (M i)<VAR>inst✝⁶ : (i : ι) → Module R (M i)<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Semiring S<VAR>inst✝¹ : Module S N<VAR>inst✝ : SMulCommClass R S N<VAR>c : S<VAR>F : (i : ι) → M i →ₗ[R] N<VAR>i : ι<GOAL>{ toFun := fun F => { toFun := ⇑(sumAddHom fun i => (F i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯ }.toFun (c • F) ∘ₗ lsingle i = ((RingHom.id S) c • { toFun := fun F => { toFun := ⇑(sumAddHom fun i => (F i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯ }.toFun F) ∘ₗ lsingle i
<VAR>k : Type u_1<VAR>P₁ : Type u_2<VAR>P₂ : Type u_3<VAR>P₃ : Type u_4<VAR>P₄ : Type u_5<VAR>V₁ : Type u_6<VAR>V₂ : Type u_7<VAR>V₃ : Type u_8<VAR>V₄ : Type u_9<VAR>inst✝¹³ : Ring k<VAR>inst✝¹² : AddCommGroup V₁<VAR>inst✝¹¹ : Module k V₁<VAR>inst✝¹⁰ : AffineSpace V₁ P₁<VAR>inst✝⁹ : AddCommGroup V₂<VAR>inst✝⁸ : Module k V₂<VAR>inst✝⁷ : AffineSpace V₂ P₂<VAR>inst✝⁶ : AddCommGroup V₃<VAR>inst✝⁵ : Module k V₃<VAR>inst✝⁴ : AffineSpace V₃ P₃<VAR>inst✝³ : AddCommGroup V₄<VAR>inst✝² : Module k V₄<VAR>inst✝¹ : AffineSpace V₄ P₄<VAR>inst✝ : Invertible 2<VAR>x y : V₁<VAR>h : 2 • x = 2 • y<GOAL>x = y
<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>x : E<VAR>hf✝ : IsBoundedLinearMap 𝕜 f<VAR>hf : IsLinearMap 𝕜 f<VAR>M : ℝ<VAR>left✝ : 0 < M<VAR>hM : ∀ (x : E), ‖f x‖ ≤ M * ‖x‖<VAR>e : E<GOAL>‖f e - f x‖ = ‖(IsLinearMap.mk' f hf) (e - x)‖
<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>x : E<VAR>hf✝ : IsBoundedLinearMap 𝕜 f<VAR>hf : IsLinearMap 𝕜 f<VAR>M : ℝ<VAR>left✝ : 0 < M<VAR>hM : ∀ (x : E), ‖f x‖ ≤ M * ‖x‖<VAR>e : E<GOAL>‖f e - f x‖ = ‖(IsLinearMap.mk' f hf) e - (IsLinearMap.mk' f hf) x‖
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>l : List α<GOAL>l.revzip.reverse = l.reverse.revzip
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>l : List α<GOAL>l.revzip.reverse.unzip.1.zip l.revzip.reverse.unzip.2 = l.reverse.revzip
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁷ : DecidableEq α'<VAR>inst✝⁶ : DecidableEq β'<VAR>inst✝⁵ : DecidableEq γ<VAR>inst✝⁴ : DecidableEq γ'<VAR>inst✝³ : DecidableEq δ<VAR>inst✝² : DecidableEq δ'<VAR>inst✝¹ : DecidableEq ε<VAR>inst✝ : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<GOAL>image₂ f s t ⊆ u ↔ ∀ b ∈ t, image (fun a => f a b) s ⊆ u
<VAR>G : Type u<VAR>inst✝² : Group G<VAR>inst✝¹ : Finite G<VAR>N : Subgroup G<VAR>inst✝ : N.Normal<VAR>h1 : (Nat.card ↥N).Coprime N.index<VAR>h2 : ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'], Nat.card G' < Nat.card G → ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'<VAR>h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H<VAR>K : Subgroup G<VAR>hK : K ⊔ N = ⊤<GOAL>K = ⊤
<VAR>G : Type u<VAR>inst✝² : Group G<VAR>inst✝¹ : Finite G<VAR>N : Subgroup G<VAR>inst✝ : N.Normal<VAR>h1 : (Nat.card ↥N).Coprime N.index<VAR>h2 : ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'], Nat.card G' < Nat.card G → ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'<VAR>K : Subgroup G<VAR>hK : K ⊔ N = ⊤<VAR>h3 : K ≠ ⊤<GOAL>∃ H, N.IsComplement' H