ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>s : Set α<VAR>h : f'' =o[𝓟 s] g'<VAR>x : α<VAR>hx : x ∈ s<GOAL>‖f'' x‖ ≤ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>s : Set α<VAR>h : ∀ x ∈ s, f'' x = 0<GOAL>f'' =o[𝓟 s] g'
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X : C<VAR>inst✝ : HasBinaryProducts C<VAR>X✝ Y✝ : (prodComonad X).Coalgebra<VAR>f : X✝ ⟶ Y✝<GOAL>f.f ≫ ((fun A => Over.mk (A.a ≫ prod.fst)) Y✝).hom = ((fun A => Over.mk (A.a ≫ prod.fst)) X✝).hom
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X : C<VAR>inst✝ : HasBinaryProducts C<VAR>X✝ Y✝ : (prodComonad X).Coalgebra<VAR>f : X✝ ⟶ Y✝<GOAL>X✝.a ≫ (prodComonad X).map f.f ≫ prod.fst = ((fun A => Over.mk (A.a ≫ prod.fst)) X✝).hom
<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₂<GOAL>cyclesMap' (-φ) h₁ h₂ = -cyclesMap' φ h₁ h₂
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>n : ℤ<GOAL>rootSpace H (n • ⇑α + ⇑β) ≠ ⊥ ↔ n ∈ Finset.Icc (-↑(chainBotCoeff (⇑α) β)) ↑(chainTopCoeff (⇑α) β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MulOneClass α<VAR>inst✝² : LE α<VAR>inst✝¹ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a * b ≤ b ↔ a * b ≤ 1 * b
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>Q : QuadraticForm R M<VAR>inst✝ : Invertible 2<VAR>x : M × M<GOAL>(dualProd R M) ((((⟨⅟2, ⋯⟩ • { toFun := polarBilin, map_add' := ⋯, map_smul' := ⋯ }) Q ∘ₗ LinearMap.fst R M M + (⟨⅟2, ⋯⟩ • { toFun := polarBilin, map_add' := ⋯, map_smul' := ⋯ }) Q ∘ₗ LinearMap.snd R M M).prod (LinearMap.fst R M M - LinearMap.snd R M M)).toFun x) = (prod Q (-Q)) x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>Q : QuadraticForm R M<VAR>inst✝ : Invertible 2<VAR>x : M × M<GOAL>⟨⅟2, ⋯⟩ • polar (⇑Q) x.1 (x.1 - x.2) + ⟨⅟2, ⋯⟩ • polar (⇑Q) x.2 (x.1 - x.2) = Q x.1 + -Q x.2
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>n : ℕ<VAR>toFinsupp✝¹ toFinsupp✝ : R[ℕ]<GOAL>({ toFinsupp := toFinsupp✝¹ } + { toFinsupp := toFinsupp✝ }).coeff n = { toFinsupp := toFinsupp✝¹ }.coeff n + { toFinsupp := toFinsupp✝ }.coeff n
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>n : ℕ<VAR>toFinsupp✝¹ toFinsupp✝ : R[ℕ]<GOAL>(toFinsupp✝¹ + toFinsupp✝) n = toFinsupp✝¹ n + toFinsupp✝ n
<VAR>M✝ : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>H : Type u_4<VAR>A : Type u_5<VAR>B : Type u_6<VAR>α✝ : Type u_7<VAR>β : Type u_8<VAR>γ : Type u_9<VAR>δ : Type u_10<VAR>M : Type u_11<VAR>α : Type u_12<VAR>inst✝² : SMul M α<VAR>inst✝¹ : SMul Mᵐᵒᵖ α<VAR>inst✝ : IsCentralScalar M α<VAR>a : α<VAR>X✝ : M<GOAL>MulOpposite.unop (MulOpposite.op X✝) • a = MulOpposite.op X✝ • a
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝²⁵ : CommRing R<VAR>inst✝²⁴ : CommRing S<VAR>inst✝²³ : Algebra R S<VAR>P : Generators R S<VAR>R' : Type ?u.248221<VAR>S' : Type ?u.248224<VAR>inst✝²² : CommRing R'<VAR>inst✝²¹ : CommRing S'<VAR>inst✝²⁰ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝¹⁹ : Algebra R R'<VAR>inst✝¹⁸ : Algebra S S'<VAR>inst✝¹⁷ : Algebra R S'<VAR>inst✝¹⁶ : IsScalarTower R R' S'<VAR>inst✝¹⁵ : IsScalarTower R S S'<VAR>R'' : Type ?u.250655<VAR>S'' : Type ?u.250658<VAR>inst✝¹⁴ : CommRing R''<VAR>inst✝¹³ : CommRing S''<VAR>inst✝¹² : Algebra R'' S''<VAR>P'' : Generators R'' S''<VAR>inst✝¹¹ : Algebra R R''<VAR>inst✝¹⁰ : Algebra S S''<VAR>inst✝⁹ : Algebra R S''<VAR>inst✝⁸ : IsScalarTower R R'' S''<VAR>inst✝⁷ : IsScalarTower R S S''<VAR>inst✝⁶ : Algebra R' R''<VAR>inst✝⁵ : Algebra S' S''<VAR>inst✝⁴ : Algebra R' S''<VAR>inst✝³ : IsScalarTower R' R'' S''<VAR>inst✝² : IsScalarTower R' S' S''<VAR>inst✝¹ : IsScalarTower R R' R''<VAR>inst✝ : IsScalarTower S S' S''<VAR>f : { f // ∀ (x : P.Ring), (aeval P'.val) (f x) = (algebraMap S S') ((aeval P.val) x) }<VAR>i : P.vars<GOAL>(aeval P'.val) ((fun i => ↑f (X i)) i) = (algebraMap S S') (P.val i)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁶ inst✝⁵ : Group α<VAR>inst✝⁴ : MulAction α β<VAR>x : β<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>inst✝¹ : Fintype (Quotient (orbitRel α β))<VAR>inst✝ : (b : β) → Fintype ↥(stabilizer α b)<VAR>φ : Quotient (orbitRel α β) → β<VAR>hφ : LeftInverse Quotient.mk'' φ<GOAL>Fintype.card β = ∑ ω : Quotient (orbitRel α β), Fintype.card α / Fintype.card ↥(stabilizer α (φ ω))
<VAR>S : ShortComplex Ab<GOAL>S.Exact ↔ ∀ (x₂ : ↑S.X₂), S.g x₂ = 0 → ∃ x₁, S.f x₁ = x₂
<VAR>S : ShortComplex Ab<GOAL>Function.Surjective ⇑S.abToCycles ↔ ∀ (x₂ : ↑S.X₂), S.g x₂ = 0 → ∃ x₁, S.f x₁ = x₂
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hs : s ≠ univ<GOAL>supSum {s} = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hs : s ≠ univ<VAR>this : ∀ (t : Finset α), (↑(card α) - ↑({s}.truncatedSup t).card) / ((↑(card α) - ↑t.card) * ↑((card α).choose t.card)) = if t ⊆ s then (↑(card α) - ↑s.card) / ((↑(card α) - ↑t.card) * ↑((card α).choose t.card)) else 0<GOAL>supSum {s} = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hs : s ≠ univ<VAR>this : ∀ (t : Finset α), (↑(card α) - ↑({s}.truncatedSup t).card) / ((↑(card α) - ↑t.card) * ↑((card α).choose t.card)) = if t ⊆ s then (↑(card α) - ↑s.card) / ((↑(card α) - ↑t.card) * ↑((card α).choose t.card)) else 0<GOAL>1 = ∑ x : Finset α, (↑(card α) - ↑({s}.truncatedSup x).card) / ((↑(card α) - ↑x.card) * ↑((card α).choose x.card))
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hs : s ≠ univ<VAR>this : ∀ (t : Finset α), (↑(card α) - ↑({s}.truncatedSup t).card) / ((↑(card α) - ↑t.card) * ↑((card α).choose t.card)) = if t ⊆ s then (↑(card α) - ↑s.card) / ((↑(card α) - ↑t.card) * ↑((card α).choose t.card)) else 0<GOAL>∑ j ∈ range (s.card + 1), ∑ t ∈ powersetCard j s, (↑(card α) - ↑s.card) / ((↑(card α) - ↑t.card) * ↑((card α).choose t.card)) = ∑ i ∈ range (s.card + 1), ↑(s.card.choose i) * (↑(card α) - ↑s.card) / ((↑(card α) - ↑i) * ↑((card α).choose i))
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hs : s ≠ univ<VAR>this : ∀ (t : Finset α), (↑(card α) - ↑({s}.truncatedSup t).card) / ((↑(card α) - ↑t.card) * ↑((card α).choose t.card)) = if t ⊆ s then (↑(card α) - ↑s.card) / ((↑(card α) - ↑t.card) * ↑((card α).choose t.card)) else 0<VAR>n : ℕ<VAR>x✝ : n ∈ range (s.card + 1)<GOAL>∑ t ∈ powersetCard n s, (↑(card α) - ↑s.card) / ((↑(card α) - ↑t.card) * ↑((card α).choose t.card)) = ↑(s.card.choose n) * (↑(card α) - ↑s.card) / ((↑(card α) - ↑n) * ↑((card α).choose n))
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hs : s ≠ univ<VAR>this : ∀ (t : Finset α), (↑(card α) - ↑({s}.truncatedSup t).card) / ((↑(card α) - ↑t.card) * ↑((card α).choose t.card)) = if t ⊆ s then (↑(card α) - ↑s.card) / ((↑(card α) - ↑t.card) * ↑((card α).choose t.card)) else 0<VAR>n : ℕ<VAR>x✝ : n ∈ range (s.card + 1)<GOAL>∑ t ∈ powersetCard n s, (↑(card α) - ↑s.card) / ((↑(card α) - ↑t.card) * ↑((card α).choose t.card)) = s.card.choose n • ((↑(card α) - ↑s.card) / ((↑(card α) - ↑n) * ↑((card α).choose n)))
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : DecidableEq α<VAR>i j : α<VAR>σ : Perm α<GOAL>σ * swap i j = σ ↔ i = j
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : Mono f<VAR>i : IsZero Y<GOAL>IsZero X
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : Mono f<VAR>i : IsZero Y<VAR>hf : f = 0<GOAL>IsZero X
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>X Y : C<VAR>i : IsZero Y<VAR>inst✝ : Mono 0<GOAL>IsZero X
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>N' : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : AddCommGroup N'<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R N'<VAR>F : ExteriorAlgebra R M →ₗ[R] N<GOAL>F ∘ₗ liftAlternating (ιMulti R) = F
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<GOAL>principalSeg.top = type fun x x_1 => x < x_1
<VAR>R : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero R<VAR>x y p d : R<VAR>k : ℕ<VAR>hy : Squarefree y<VAR>hp : Prime p<VAR>h : p ^ (k + 1) ∣ x * y<GOAL>p ^ k ∣ x
<VAR>R : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero R<VAR>x y p d : R<VAR>k : ℕ<VAR>hy : Squarefree y<VAR>hp : Prime p<VAR>h : p ^ (k + 1) ∣ y * x<GOAL>p ^ k ∣ x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<GOAL>(∀ (x : Set Y), IsOpen xᶜ ↔ IsOpen (f ⁻¹' xᶜ)) ↔ ∀ (s : Set Y), IsClosed s ↔ IsClosed (f ⁻¹' s)
<VAR>a b c : Prop<GOAL>((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c))
<VAR>a x✝ z x : ℂ<VAR>hi : 0 < x.im<GOAL>(-x).arg = x.arg - π
<VAR>a x✝ z x : ℂ<VAR>hi : 0 < x.im<GOAL>-Real.arccos ((-x).re / abs (-x)) = Real.arccos (x.re / abs x) - π
<VAR>α : Type u_1<VAR>t : Ordnode α<GOAL>t.eraseMax.dual = t.dual.eraseMin
<VAR>L : Language<VAR>M : Type w<VAR>inst✝¹ : Nonempty M<VAR>inst✝ : L.Structure M<VAR>S : (L.sum L.skolem₁).Substructure M<GOAL>(LHom.sumInl.substructureReduct S).IsElementary
<VAR>L : Language<VAR>M : Type w<VAR>inst✝¹ : Nonempty M<VAR>inst✝ : L.Structure M<VAR>S : (L.sum L.skolem₁).Substructure M<GOAL>∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → ↥(LHom.sumInl.substructureReduct S)) (a : M), φ.Realize default (Fin.snoc (Subtype.val ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (Subtype.val ∘ x) ↑b)
<VAR>L : Language<VAR>M : Type w<VAR>inst✝¹ : Nonempty M<VAR>inst✝ : L.Structure M<VAR>S : (L.sum L.skolem₁).Substructure M<VAR>n : ℕ<VAR>φ : L.BoundedFormula Empty (n + 1)<VAR>x : Fin n → ↥(LHom.sumInl.substructureReduct S)<VAR>a : M<VAR>h : φ.Realize default (Fin.snoc (Subtype.val ∘ x) a)<VAR>φ' : (L.sum L.skolem₁).Functions n := LHom.sumInr.onFunction φ<GOAL>∃ b, φ.Realize default (Fin.snoc (Subtype.val ∘ x) ↑b)
<VAR>R : Type u_1<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>ι : Type u_4<VAR>ι₂ : Type u_5<VAR>A : Type u_6<VAR>inst✝¹⁰ : Fintype ι<VAR>inst✝⁹ : Finite ι₂<VAR>inst✝⁸ : DecidableEq ι<VAR>inst✝⁷ : DecidableEq ι₂<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : CommSemiring A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : AddCommMonoid M₁<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : AddCommMonoid M₂<VAR>inst✝ : Module R M₂<VAR>f : M₁ →ₗ[R] M₂<VAR>b₁ : Basis ι R M₁<VAR>b₂ : Basis ι₂ R M₂<VAR>i✝ : ι₂<VAR>j✝ : ι<GOAL>(toMatrix (basis A b₁) (basis A b₂)) (baseChange A f) i✝ j✝ = ((toMatrix b₁ b₂) f).map (⇑(algebraMap R A)) i✝ j✝
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : CompleteSpace E<VAR>ι : Type u_3<VAR>inst✝⁵ : LinearOrder ι<VAR>inst✝⁴ : TopologicalSpace ι<VAR>inst✝³ : OrderTopology ι<VAR>inst✝² : FirstCountableTopology ι<VAR>ℱ : Filtration ι m<VAR>inst✝¹ : SigmaFiniteFiltration μ ℱ<VAR>τ σ : Ω → ι<VAR>f : ι → Ω → E<VAR>i✝ n : ι<VAR>h : Martingale f ℱ μ<VAR>hτ : IsStoppingTime ℱ τ<VAR>hτ_le : ∀ (x : Ω), τ x ≤ n<VAR>inst✝ : SigmaFinite (μ.trim ⋯)<VAR>i : ι<GOAL>stoppedValue f τ =ᶠ[ae (μ.restrict {x | τ x = i})] μ[f n|hτ.measurableSpace]
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : CompleteSpace E<VAR>ι : Type u_3<VAR>inst✝⁵ : LinearOrder ι<VAR>inst✝⁴ : TopologicalSpace ι<VAR>inst✝³ : OrderTopology ι<VAR>inst✝² : FirstCountableTopology ι<VAR>ℱ : Filtration ι m<VAR>inst✝¹ : SigmaFiniteFiltration μ ℱ<VAR>τ σ : Ω → ι<VAR>f : ι → Ω → E<VAR>i✝ n : ι<VAR>h : Martingale f ℱ μ<VAR>hτ : IsStoppingTime ℱ τ<VAR>hτ_le : ∀ (x : Ω), τ x ≤ n<VAR>inst✝ : SigmaFinite (μ.trim ⋯)<VAR>i : ι<GOAL>stoppedValue f τ =ᶠ[ae (μ.restrict {x | τ x = i})] f i
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : CompleteSpace E<VAR>ι : Type u_3<VAR>inst✝⁵ : LinearOrder ι<VAR>inst✝⁴ : TopologicalSpace ι<VAR>inst✝³ : OrderTopology ι<VAR>inst✝² : FirstCountableTopology ι<VAR>ℱ : Filtration ι m<VAR>inst✝¹ : SigmaFiniteFiltration μ ℱ<VAR>τ σ : Ω → ι<VAR>f : ι → Ω → E<VAR>i✝ n : ι<VAR>h : Martingale f ℱ μ<VAR>hτ : IsStoppingTime ℱ τ<VAR>hτ_le : ∀ (x : Ω), τ x ≤ n<VAR>inst✝ : SigmaFinite (μ.trim ⋯)<VAR>i : ι<GOAL>∀ᵐ (x : Ω) ∂μ, x ∈ {ω | τ ω = i} → stoppedValue f τ x = f i x
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : CompleteSpace E<VAR>ι : Type u_3<VAR>inst✝⁵ : LinearOrder ι<VAR>inst✝⁴ : TopologicalSpace ι<VAR>inst✝³ : OrderTopology ι<VAR>inst✝² : FirstCountableTopology ι<VAR>ℱ : Filtration ι m<VAR>inst✝¹ : SigmaFiniteFiltration μ ℱ<VAR>τ σ : Ω → ι<VAR>f : ι → Ω → E<VAR>i✝ n : ι<VAR>h : Martingale f ℱ μ<VAR>hτ : IsStoppingTime ℱ τ<VAR>hτ_le : ∀ (x : Ω), τ x ≤ n<VAR>inst✝ : SigmaFinite (μ.trim ⋯)<VAR>i : ι<VAR>x : Ω<VAR>hx : x ∈ {ω | τ ω = i}<GOAL>stoppedValue f τ x = f i x
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : CompleteSpace E<VAR>ι : Type u_3<VAR>inst✝⁵ : LinearOrder ι<VAR>inst✝⁴ : TopologicalSpace ι<VAR>inst✝³ : OrderTopology ι<VAR>inst✝² : FirstCountableTopology ι<VAR>ℱ : Filtration ι m<VAR>inst✝¹ : SigmaFiniteFiltration μ ℱ<VAR>τ σ : Ω → ι<VAR>f : ι → Ω → E<VAR>i✝ n : ι<VAR>h : Martingale f ℱ μ<VAR>hτ : IsStoppingTime ℱ τ<VAR>hτ_le : ∀ (x : Ω), τ x ≤ n<VAR>inst✝ : SigmaFinite (μ.trim ⋯)<VAR>i : ι<VAR>x : Ω<VAR>hx : τ x = i<GOAL>stoppedValue f τ x = f i x
<VAR>μ : Measure ℝ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>x : ℝ<GOAL>↑(cdf μ) x = (μ (Iic x)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : OrderedCommSemiring α<VAR>inst✝² : OrderedSemiring β<VAR>inst✝¹ : Algebra α β<VAR>inst✝ : SMulPosMono α β<VAR>a : α<VAR>ha : 0 ≤ a<GOAL>0 ≤ (algebraMap α β) a
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoidWithZero M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝² : CommMonoidWithZero N<VAR>P : Type u_3<VAR>inst✝¹ : CommMonoidWithZero P<VAR>f : S.LocalizationWithZeroMap N<VAR>inst✝ : IsCancelMulZero M<VAR>h : ∀ ⦃x : M⦄, x ∈ S → IsRegular x<GOAL>IsCancelMulZero N
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoidWithZero M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝² : CommMonoidWithZero N<VAR>P : Type u_3<VAR>inst✝¹ : CommMonoidWithZero P<VAR>f : S.LocalizationWithZeroMap N<VAR>inst✝ : IsCancelMulZero M<VAR>h : ∀ ⦃x : M⦄, x ∈ S → IsRegular x<VAR>this : IsLeftCancelMulZero N<GOAL>IsCancelMulZero N
<VAR>p q : ℝ<VAR>hp : 1 ≤ p<VAR>hq : -2 < q<GOAL>∫ (x : ℂ), ‖x‖ ^ q * rexp (-‖x‖ ^ p) = 2 * π / p * Real.Gamma ((q + 2) / p)
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>n : ℕ<VAR>hp : ∀ n' < n, p n'<GOAL>count p n = n
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>n : ℕ<VAR>hp : ∀ n' < n, p n'<GOAL>∀ x ∈ range n, p x
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f✝ g✝ : C ⟶ D<VAR>h✝ k : D ⟶ E<VAR>i✝ : ι<VAR>e f : C ⟶ D<VAR>h : Homotopy e f<VAR>g : D ⟶ E<VAR>i j : ι<VAR>w : ¬c.Rel j i<GOAL>h.hom i j ≫ g.f j = 0
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f✝ g✝ : C ⟶ D<VAR>h✝ k : D ⟶ E<VAR>i✝ : ι<VAR>e f : C ⟶ D<VAR>h : Homotopy e f<VAR>g : D ⟶ E<VAR>i : ι<GOAL>(e ≫ g).f i = (((dNext i) fun i j => h.hom i j ≫ g.f j) + (prevD i) fun i j => h.hom i j ≫ g.f j) + (f ≫ g).f i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : F<GOAL>‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ ⟪x, y⟫_ℝ = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : F<GOAL>2 = 0 ∨ re ⟪x, y⟫_ℝ = 0 ↔ ⟪x, y⟫_ℝ = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a✝ b✝ c a b : α<GOAL>(Ioo a b).card = (Icc a b).card - 2
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a✝ b✝ c a b : α<GOAL>(Icc a b).card - 1 - 1 = (Icc a b).card - 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : MeasurableSpace δ<VAR>inst✝³ : NormedAddCommGroup β<VAR>inst✝² : NormedAddCommGroup γ<VAR>E : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤<VAR>g : α → E<GOAL>Integrable g (μ.withDensity f) ↔ Integrable (fun x => (f x).toReal • g x) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : MeasurableSpace δ<VAR>inst✝³ : NormedAddCommGroup β<VAR>inst✝² : NormedAddCommGroup γ<VAR>E : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤<VAR>g : α → E<GOAL>Integrable (fun x => (f x).toNNReal • g x) μ ↔ Integrable (fun x => (f x).toReal • g x) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : MeasurableSpace δ<VAR>inst✝³ : NormedAddCommGroup β<VAR>inst✝² : NormedAddCommGroup γ<VAR>E : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤<VAR>g : α → E<GOAL>Measurable fun x => (f x).toNNReal
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>p : α → Prop<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<GOAL>(∀ᵐ (x : α) ∂μ.withDensity f, p x) ↔ ∀ᵐ (x : α) ∂μ, f x ≠ 0 → p x
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>p : α → Prop<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<GOAL>(μ ({x | f x ≠ 0} ∩ {a | ¬p a}) = 0) = (μ {a | ¬(f a ≠ 0 → p a)} = 0)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>p : α → Prop<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>x : α<GOAL>x ∈ {x | f x ≠ 0} ∩ {a | ¬p a} ↔ x ∈ {a | ¬(f a ≠ 0 → p a)}
<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 K₁ K₂ : Submodule 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 ↥K₂<VAR>h : K₁ ≤ K₂<VAR>n : ℕ<VAR>h_dim : finrank 𝕜 ↥K₁ + n = finrank 𝕜 ↥K₂<GOAL>finrank 𝕜 ↥(K₁ᗮ ⊓ K₂) = 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 K₁ K₂ : Submodule 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 ↥K₂<VAR>h : K₁ ≤ K₂<VAR>n : ℕ<VAR>h_dim : finrank 𝕜 ↥K₁ + n = finrank 𝕜 ↥K₂<GOAL>finrank 𝕜 ↥K₁ + finrank 𝕜 ↥(K₁ᗮ ⊓ K₂) = finrank 𝕜 ↥K₁ + n
<VAR>n : ℕ<GOAL>(hermite (n + 1)).coeff 0 = -(hermite n).coeff 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t u v : Finset α<VAR>a✝ b : α<VAR>s : Finset α<VAR>a : α<GOAL>s.erase a = ∅ ↔ s = ∅ ∨ s = {a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : ↥(Lp β 1 μ)<GOAL>ENNReal.ofReal ‖f‖ = ∫⁻ (x : α), ↑‖↑↑f x‖₊ ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : ↥(Lp β 1 μ)<GOAL>∫⁻ (a : α), ↑‖↑↑f a‖₊ ∂μ ≠ ⊤
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : LinearOrderedAddCommGroup β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>x y z : E<VAR>hf : ConvexOn 𝕜 [x-[𝕜]y] f<VAR>hz : z ∈ [x-[𝕜]y]<GOAL>f z ≤ max (f x) (f y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : LinearOrderedAddCommGroup β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>x y z : E<VAR>hf : ConvexOn 𝕜 ((convexHull 𝕜) {x, y}) f<VAR>hz : z ∈ (convexHull 𝕜) {x, y}<GOAL>f z ≤ max (f x) (f y)
<VAR>α : Type u<VAR>β : Type u_1<VAR>a b n : ℕ<GOAL>(b - 1) * ∑ i ∈ range n.succ, a / b ^ i = ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
<VAR>α : Type u<VAR>β : Type u_1<VAR>a b n : ℕ<GOAL>∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n) ≤ ∑ i ∈ range n, a / b ^ i + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)