ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>T T' T'' : D<VAR>Y Y' Y'' : C<VAR>S S' : C ⥤ D<VAR>A : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} A<VAR>B : Type u₄<VAR>inst✝ : Category.{v₄, u₄} B<VAR>f g : CostructuredArrow S T<VAR>h : f.IsUniversal<VAR>c : C<VAR>η η' : c ⟶ f.left<VAR>w : S.map η ≫ f.hom = S.map η' ≫ f.hom<GOAL>η = η'
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>d n : ℕ<VAR>h : d ∈ n.properDivisors<GOAL>(X ^ d - 1) * cyclotomic n R ∣ X ^ n - 1
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>d n : ℕ<VAR>h : d ∈ n.properDivisors<VAR>hdn : d < n<GOAL>(X ^ d - 1) * cyclotomic n R ∣ X ^ n - 1
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>d n : ℕ<VAR>h : d ∈ n.properDivisors<VAR>hdn : d < n<GOAL>X ^ n - 1 = (X ^ d - 1) * cyclotomic n R * ∏ x ∈ n.properDivisors \ d.divisors, cyclotomic x R
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>d n : ℕ<VAR>h : d ∈ n.properDivisors<VAR>hdn : d < n<GOAL>(X ^ d - 1) * cyclotomic n R * ∏ x ∈ n.properDivisors \ d.divisors, cyclotomic x R = X ^ n - 1
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>d n : ℕ<VAR>h : d ∈ n.properDivisors<VAR>hdn : d < n<GOAL>(X ^ d - 1) * cyclotomic n R * ∏ x ∈ n.properDivisors \ d.divisors, cyclotomic x R = (X ^ d - 1) * ∏ x ∈ n.divisors \ d.divisors, cyclotomic x R
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>d n : ℕ<VAR>h : d ∈ n.properDivisors<VAR>hdn : d < n<GOAL>(X ^ d - 1) * (cyclotomic n R * ∏ x ∈ n.properDivisors \ d.divisors, cyclotomic x R) = (X ^ d - 1) * ∏ x ∈ n.divisors \ d.divisors, cyclotomic x R
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>d n : ℕ<VAR>h : d ∈ n.properDivisors<VAR>hdn : d < n<GOAL>cyclotomic n R * ∏ x ∈ n.properDivisors \ d.divisors, cyclotomic x R = ∏ x ∈ n.divisors \ d.divisors, cyclotomic x R
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>d n : ℕ<VAR>h : d ∈ n.properDivisors<VAR>hdn : d < n<GOAL>n ∉ n.properDivisors \ d.divisors
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>d n : ℕ<VAR>h : d ∈ n.properDivisors<VAR>hdn : d < n<GOAL>n ∉ d.divisors
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{u}<VAR>hf : a.IsFundamentalSequence o f<VAR>i : Ordinal.{u}<VAR>hi : i < a.cof.ord<GOAL>a.cof.ord ≤ o
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{u}<VAR>hf : a.IsFundamentalSequence o f<GOAL>a.IsFundamentalSequence a.cof.ord fun i hi => f i ⋯
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{u}<VAR>hf : a.IsFundamentalSequence o f<VAR>H : a.cof.ord = o<GOAL>a.IsFundamentalSequence a.cof.ord fun i hi => f i ⋯
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>d : D<VAR>X✝ Y✝ : (StructuredArrow (op d) F.op)ᵒᵖ<VAR>f : X✝ ⟶ Y✝<GOAL>F.map f.unop.right.unop ≫ (unop Y✝).hom.unop = (unop X✝).hom.unop
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>d : D<VAR>X✝ Y✝ : (StructuredArrow (op d) F.op)ᵒᵖ<VAR>f : X✝ ⟶ Y✝<GOAL>(𝟙 (op d) ≫ (unop X✝).hom).unop = (unop X✝).hom.unop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>a b : ℝ<VAR>h : a ≤ b<GOAL>Metric.diam (Ioo a b) = b - 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 : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>v : E<VAR>p : E := orthogonalProjectionFn K v<GOAL>‖v‖ * ‖v‖ = ‖v - p‖ * ‖v - p‖ + ‖p‖ * ‖p‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>v : E<VAR>p : E := orthogonalProjectionFn K v<VAR>h' : ⟪v - p, p⟫_𝕜 = 0<GOAL>‖v‖ * ‖v‖ = ‖v - p‖ * ‖v - p‖ + ‖p‖ * ‖p‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y z : E<VAR>δ ε : ℝ<VAR>hε : 0 < ε<VAR>hδ : 0 < δ<VAR>a b : E<GOAL>Metric.ball a ε - Metric.ball b δ = Metric.ball (a - b) (ε + δ)
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>𝒢 : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>τ π : Ω → ℕ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hadp : Adapted 𝒢 f<VAR>hint : ∀ (i : ℕ), Integrable (f i) μ<VAR>hf : ∀ (τ π : Ω → ℕ), IsStoppingTime 𝒢 τ → IsStoppingTime 𝒢 π → τ ≤ π → (∃ N, ∀ (ω : Ω), π ω ≤ N) → ∫ (x : Ω), stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), stoppedValue f π x ∂μ<GOAL>Submartingale f 𝒢 μ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>𝒢 : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>τ π : Ω → ℕ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hadp : Adapted 𝒢 f<VAR>hint : ∀ (i : ℕ), Integrable (f i) μ<VAR>hf : ∀ (τ π : Ω → ℕ), IsStoppingTime 𝒢 τ → IsStoppingTime 𝒢 π → τ ≤ π → (∃ N, ∀ (ω : Ω), π ω ≤ N) → ∫ (x : Ω), stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), stoppedValue f π x ∂μ<VAR>i j : ℕ<VAR>hij : i ≤ j<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>r r' s : α → α → Prop<VAR>inst✝³ : Preorder α<VAR>a : α<VAR>inst✝² : PartialOrder β<VAR>inst✝¹ : IsDirected β fun x x_1 => x ≥ x_1<VAR>inst✝ : Nontrivial β<GOAL>∃ a b, a < b
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>r r' s : α → α → Prop<VAR>inst✝³ : Preorder α<VAR>a✝ : α<VAR>inst✝² : PartialOrder β<VAR>inst✝¹ : IsDirected β fun x x_1 => x ≥ x_1<VAR>inst✝ : Nontrivial β<VAR>a b : β<VAR>hne : a ≠ b<GOAL>∃ a b, a < b
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>r r' s : α → α → Prop<VAR>inst✝³ : Preorder α<VAR>a✝ : α<VAR>inst✝² : PartialOrder β<VAR>inst✝¹ : IsDirected β fun x x_1 => x ≥ x_1<VAR>inst✝ : Nontrivial β<VAR>a b : β<VAR>hne : a ≠ b<VAR>ha : IsBot a<GOAL>∃ a b, a < b
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>r r' s : α → α → Prop<VAR>inst✝³ : Preorder α<VAR>a✝ : α<VAR>inst✝² : PartialOrder β<VAR>inst✝¹ : IsDirected β fun x x_1 => x ≥ x_1<VAR>inst✝ : Nontrivial β<VAR>a b : β<VAR>hne : a ≠ b<VAR>c : β<VAR>hc : c < a<GOAL>∃ a b, a < b
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>x : S₁<GOAL>(optionEquivRight R S₁) (X (Option.some x)) = X x
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : MonoidWithZero M₀<VAR>a : M₀<VAR>m n✝ n : ℕ<VAR>x✝ : n + 1 ≠ 0<GOAL>0 ^ (n + 1) = 0
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type w<VAR>inst✝¹⁴ : Ring R<VAR>inst✝¹³ : Ring S<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module.Free R M<VAR>inst✝⁹ : Module.Finite R M<VAR>inst✝⁸ : AddCommGroup N<VAR>inst✝⁷ : Module R N<VAR>inst✝⁶ : Module S N<VAR>inst✝⁵ : SMulCommClass R S N<VAR>inst✝⁴ : StrongRankCondition R<VAR>inst✝³ : StrongRankCondition S<VAR>inst✝² : Module.Free S N<VAR>inst✝¹ : Module R S<VAR>inst✝ : SMulCommClass R S S<GOAL>finrank S (M →ₗ[R] S) = finrank R M
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>f : X → Y<VAR>s : Set X<VAR>t : Set Y<VAR>cont : ∀ x ∈ s, ContinuousAt f x<VAR>x : X<VAR>hx : x ∈ s<VAR>g : PartialHomeomorph Y Z<VAR>hxg : f x ∈ g.source<VAR>hgf✝ : IsLocalHomeomorphOn (↑g ∘ f) s<VAR>hg : IsLocalHomeomorphOn (↑g) (f '' s)<VAR>gf : PartialHomeomorph X Z<VAR>hgf : x ∈ gf.source<VAR>he : ↑g ∘ f = ↑gf<GOAL>∃ e, x ∈ e.source ∧ Set.EqOn f (↑e) e.source
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>f : X → Y<VAR>s : Set X<VAR>t : Set Y<VAR>cont : ∀ x ∈ s, ContinuousAt f x<VAR>x : X<VAR>hx : x ∈ s<VAR>g : PartialHomeomorph Y Z<VAR>hxg : f x ∈ g.source<VAR>hgf✝ : IsLocalHomeomorphOn (↑g ∘ f) s<VAR>hg : IsLocalHomeomorphOn (↑g) (f '' s)<VAR>gf : PartialHomeomorph X Z<VAR>hgf : x ∈ gf.source<VAR>he : ↑g ∘ f = ↑gf<VAR>y : X<VAR>hy : y ∈ ((gf.restr (f ⁻¹' g.source)).trans g.symm).source<GOAL>f y = ↑((gf.restr (f ⁻¹' g.source)).trans g.symm) y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>f : X → Y<VAR>s : Set X<VAR>t : Set Y<VAR>cont : ∀ x ∈ s, ContinuousAt f x<VAR>x : X<VAR>hx : x ∈ s<VAR>g : PartialHomeomorph Y Z<VAR>hxg : f x ∈ g.source<VAR>hgf✝ : IsLocalHomeomorphOn (↑g ∘ f) s<VAR>hg : IsLocalHomeomorphOn (↑g) (f '' s)<VAR>gf : PartialHomeomorph X Z<VAR>hgf : x ∈ gf.source<VAR>he : ↑g ∘ f = ↑gf<VAR>y : X<VAR>hy : y ∈ ((gf.restr (f ⁻¹' g.source)).trans g.symm).source<GOAL>f y = ↑g.symm (↑gf y)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>f : X → Y<VAR>s : Set X<VAR>t : Set Y<VAR>cont : ∀ x ∈ s, ContinuousAt f x<VAR>x : X<VAR>hx : x ∈ s<VAR>g : PartialHomeomorph Y Z<VAR>hxg : f x ∈ g.source<VAR>hgf✝ : IsLocalHomeomorphOn (↑g ∘ f) s<VAR>hg : IsLocalHomeomorphOn (↑g) (f '' s)<VAR>gf : PartialHomeomorph X Z<VAR>hgf : x ∈ gf.source<VAR>he : ↑g ∘ f = ↑gf<VAR>y : X<VAR>hy : y ∈ ((gf.restr (f ⁻¹' g.source)).trans g.symm).source<VAR>this : f y ∈ g.source<GOAL>f y = ↑g.symm (↑gf y)
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : PseudoEMetricSpace Ω<VAR>μ ν : Measure Ω<VAR>δ : ℝ≥0∞<VAR>h : ∀ (ε : ℝ≥0∞) (B : Set Ω), δ < ε → ε < ⊤ → MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε ∧ ν B ≤ μ (thickening ε.toReal B) + ε<VAR>δ_top : ¬δ = ⊤<GOAL>levyProkhorovEDist μ ν ≤ δ
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : PseudoEMetricSpace Ω<VAR>μ ν : Measure Ω<VAR>δ : ℝ≥0∞<VAR>h : ∀ (ε : ℝ≥0∞) (B : Set Ω), δ < ε → ε < ⊤ → MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε ∧ ν B ≤ μ (thickening ε.toReal B) + ε<VAR>δ_top : ¬δ = ⊤<GOAL>∀ (ε : ℝ≥0∞) (B : Set Ω), 0 < ε → ε < ⊤ → MeasurableSet B → μ B ≤ ν (thickening (δ + ε).toReal B) + δ + ε ∧ ν B ≤ μ (thickening (δ + ε).toReal B) + δ + ε
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : PseudoEMetricSpace Ω<VAR>μ ν : Measure Ω<VAR>δ : ℝ≥0∞<VAR>h : ∀ (ε : ℝ≥0∞) (B : Set Ω), δ < ε → ε < ⊤ → MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε ∧ ν B ≤ μ (thickening ε.toReal B) + ε<VAR>δ_top : ¬δ = ⊤<VAR>x : ℝ≥0∞<VAR>B : Set Ω<VAR>x_pos : 0 < x<VAR>x_lt_top : x < ⊤<VAR>B_mble : MeasurableSet B<GOAL>μ B ≤ ν (thickening (δ + x).toReal B) + δ + x ∧ ν B ≤ μ (thickening (δ + x).toReal B) + δ + x
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : LinearOrderedRing R<VAR>inst✝⁴ : FloorRing R<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : OrderTopology R<VAR>inst✝¹ : MeasurableSpace R<VAR>inst✝ : BorelSpace R<VAR>s : Set R<VAR>hs : MeasurableSet s<GOAL>MeasurableSet (Int.fract ⁻¹' s)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : LinearOrderedRing R<VAR>inst✝⁴ : FloorRing R<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : OrderTopology R<VAR>inst✝¹ : MeasurableSpace R<VAR>inst✝ : BorelSpace R<VAR>s : Set R<VAR>hs : MeasurableSet s<GOAL>MeasurableSet (⋃ m, (fun x => x - ↑m) ⁻¹' (s ∩ Ico 0 1))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ✝ : ι → Type u_5<VAR>s✝ s₁ s₂ : Finset ι<VAR>i : ι<VAR>a : α<VAR>f✝ g✝ : ι → α<VAR>inst✝ : NonUnitalNonAssocSemiring α<VAR>κ : Type u_6<VAR>s : Finset ι<VAR>t : Finset κ<VAR>f : ι → α<VAR>g : κ → α<GOAL>(∑ i ∈ s, f i) * ∑ j ∈ t, g j = ∑ i ∈ s, ∑ j ∈ t, f i * g j
<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 n' : ℤ<VAR>hn' : n + a = n'<GOAL>(leftShiftAddEquiv K L n a n' hn').symm 0 = 0
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>n : ℕ<VAR>k : ℤ<GOAL>↑(eval k (descPochhammer ℤ n)) = eval (↑k) (descPochhammer R n)
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>n : ℕ<VAR>k : ℤ<GOAL>(algebraMap ℤ R) (eval k (descPochhammer ℤ n)) = eval₂ (algebraMap ℤ R) (↑k) (descPochhammer ℤ n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : LE α<VAR>s t : LowerSet α<VAR>a : α<VAR>S : Set (LowerSet α)<GOAL>↑(sInf S).compl = ↑(⨅ s ∈ S, s.compl)
<VAR>α : Type u_1<VAR>inst✝ : Field α<VAR>a b ad bd a' b' gcd : α<VAR>ha : ad * a = a'<VAR>hb : bd * b = b'<VAR>had : ad ≠ 0<VAR>hbd : bd ≠ 0<VAR>hgcd : gcd ≠ 0<GOAL>(a = b) = (1 / gcd * (bd * a') = 1 / gcd * (ad * b'))
<VAR>α : Type u_1<VAR>inst✝ : Field α<VAR>a b ad bd a' b' gcd : α<VAR>ha : ad * a = a'<VAR>hb : bd * b = b'<VAR>had : ad ≠ 0<VAR>hbd : bd ≠ 0<VAR>hgcd : gcd ≠ 0<GOAL>(a = b) = (1 / gcd * (ad * bd * a) = 1 / gcd * (ad * bd * b))
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s✝ t : Set α<VAR>inst✝ : LinearOrder β<VAR>s : Set α<VAR>f : α → β<VAR>h1 : s.Finite<VAR>x : α<VAR>hx : x ∈ s<GOAL>∃ a ∈ s, ∀ b ∈ s, f b ≤ f a
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>x : LaurentSeries R<VAR>n : ℤ<GOAL>((single (order x)) 1 * (ofPowerSeries ℤ R) x.powerSeriesPart).coeff n = x.coeff n
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>x : LaurentSeries R<VAR>n : ℤ<GOAL>((ofPowerSeries ℤ R) x.powerSeriesPart).coeff (n - order x) = x.coeff n
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : Balanced C<VAR>𝒢 : Set C<GOAL>IsCoseparating 𝒢 → IsCodetecting 𝒢
<VAR>n : ℕ<GOAL>antidiagonal (n + 1) = cons (0, n + 1) (map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ)) (antidiagonal n)) ⋯
<VAR>n : ℕ<GOAL>(antidiagonal (n + 1)).val = (cons (0, n + 1) (map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ)) (antidiagonal n)) ⋯).val
<VAR>n : ℕ<GOAL>(antidiagonal (n + 1)).val = (0, n + 1) ::ₘ Multiset.map (⇑({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ))) (antidiagonal n).val
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>X : C<VAR>f : X ⟶ T.obj₂<VAR>hf : f ≫ T.mor₂ = 0<GOAL>∃ g, f = g ≫ T.mor₁
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>X : C<VAR>f : X ⟶ T.obj₂<VAR>hf : f ≫ T.mor₂ = 0<VAR>a : (contractibleTriangle X).obj₁ ⟶ T.obj₁<VAR>ha₁ : (contractibleTriangle X).mor₁ ≫ f = a ≫ T.mor₁<VAR>right✝ : (contractibleTriangle X).mor₃ ≫ (CategoryTheory.shiftFunctor C 1).map a = 0 ≫ T.mor₃<GOAL>∃ g, f = g ≫ T.mor₁
<VAR>m : ℕ∞<GOAL>↑m + ℵ₀ = ℵ₀
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>n : ℕ<VAR>hc : G.chromaticNumber < ↑n<VAR>hne : G.chromaticNumber ≠ ⊤<GOAL>G.CliqueFree n
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>n : ℕ<VAR>hc : G.chromaticNumber < ↑n<VAR>hne : G.chromaticNumber ≠ ⊤<VAR>m : ℕ<VAR>hc' : G.Colorable m<GOAL>G.CliqueFree n
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>n : ℕ<VAR>hc : G.chromaticNumber < ↑n<VAR>hne : G.chromaticNumber ≠ ⊤<VAR>m : ℕ<VAR>hc' : G.Colorable m<VAR>this : G.Colorable G.chromaticNumber.toNat<GOAL>G.CliqueFree n
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>n : ℕ<VAR>hc : G.chromaticNumber < ↑n<VAR>hne : G.chromaticNumber ≠ ⊤<VAR>m : ℕ<VAR>hc' : G.Colorable m<VAR>this : G.Colorable G.chromaticNumber.toNat<GOAL>G.chromaticNumber.toNat < n
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>n : ℕ<VAR>hc : G.chromaticNumber < ↑n<VAR>hne : ↑G.chromaticNumber.toNat = G.chromaticNumber<VAR>m : ℕ<VAR>hc' : G.Colorable m<VAR>this : G.Colorable G.chromaticNumber.toNat<GOAL>G.chromaticNumber.toNat < n
<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>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f'✝ f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>f : E → E<VAR>f' : E →L[𝕜] E<VAR>hf : HasFDerivAt f f' x<VAR>hx : f x = x<VAR>n : ℕ<GOAL>HasFDerivAt f^[n] (f' ^ n) 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>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f'✝ f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>f : E → E<VAR>f' : E →L[𝕜] E<VAR>hf : HasFDerivAt f f' x<VAR>hx : f x = x<VAR>n : ℕ<GOAL>Tendsto f (𝓝 x) (𝓝 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>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f'✝ f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>f : E → E<VAR>f' : E →L[𝕜] E<VAR>hf : HasFDerivAt f f' x<VAR>hx : f x = x<VAR>n : ℕ<GOAL>x = f x
<VAR>α : Sort u_1<VAR>o b : Ordinal.{u_2}<VAR>hb : 1 < b<VAR>ho : o.IsLimit<VAR>f : α → Ordinal.{u_2}<VAR>H : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ i, a < f i<VAR>a : Ordinal.{u_2}<VAR>h : a < b ^ o<GOAL>∃ i, a < b ^ f i
<VAR>α : Sort u_1<VAR>o b : Ordinal.{u_2}<VAR>hb : 1 < b<VAR>ho : o.IsLimit<VAR>f : α → Ordinal.{u_2}<VAR>H : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ i, a < f i<VAR>a : Ordinal.{u_2}<VAR>h : a < b ^ o<VAR>d : Ordinal.{u_2}<VAR>hd : d < o<VAR>h' : a < b ^ d<GOAL>∃ i, a < b ^ f i
<VAR>n✝ m : ℕ<VAR>p : Fin (n✝ + 1)<VAR>i✝ j : Fin n✝<VAR>n : ℕ<VAR>inst✝ : NeZero n<VAR>i : Fin n<GOAL>castSucc 0 < i.succ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : MetricSpace R<VAR>inst✝⁶ : TopologicalSemiring R<VAR>inst✝⁵ : ContinuousStar R<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>f✝ g : R → R<VAR>a✝ : A<VAR>ha✝ : autoParam (p a✝) _auto✝<VAR>hf✝ : autoParam (ContinuousOn f✝ (spectrum R a✝)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a✝)) _auto✝<VAR>r : R<VAR>f : R → R<VAR>a : A<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>ha : autoParam (p a) _auto✝<VAR>this : (fun z => r + f z) = fun z => (fun x => r) z + f z<GOAL>cfc (fun x => r + f x) a = (algebraMap R A) r + cfc f a
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁰ : MeasurableSpace α<VAR>inst✝⁹ : MeasurableSpace α'<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : MeasurableSpace β'<VAR>inst✝⁶ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SFinite μ<VAR>E' : Type u_7<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>f g : α × β → E<VAR>F : E → E'<VAR>hf : Integrable f (μ.prod ν)<VAR>hg : Integrable g (μ.prod ν)<GOAL>∫ (x : α), F (∫ (y : β), f (x, y) + g (x, y) ∂ν) ∂μ = ∫ (x : α), F (∫ (y : β), f (x, y) ∂ν + ∫ (y : β), g (x, y) ∂ν) ∂μ
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁰ : MeasurableSpace α<VAR>inst✝⁹ : MeasurableSpace α'<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : MeasurableSpace β'<VAR>inst✝⁶ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SFinite μ<VAR>E' : Type u_7<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>f g : α × β → E<VAR>F : E → E'<VAR>hf : Integrable f (μ.prod ν)<VAR>hg : Integrable g (μ.prod ν)<GOAL>(fun x => F (∫ (y : β), f (x, y) + g (x, y) ∂ν)) =ᶠ[ae μ] fun x => F (∫ (y : β), f (x, y) ∂ν + ∫ (y : β), g (x, y) ∂ν)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁰ : MeasurableSpace α<VAR>inst✝⁹ : MeasurableSpace α'<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : MeasurableSpace β'<VAR>inst✝⁶ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SFinite μ<VAR>E' : Type u_7<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>f g : α × β → E<VAR>F : E → E'<VAR>hf : Integrable f (μ.prod ν)<VAR>hg : Integrable g (μ.prod ν)<VAR>a✝ : α<VAR>h2f : Integrable (fun y => f (a✝, y)) ν<VAR>h2g : Integrable (fun y => g (a✝, y)) ν<GOAL>F (∫ (y : β), f (a✝, y) + g (a✝, y) ∂ν) = F (∫ (y : β), f (a✝, y) ∂ν + ∫ (y : β), g (a✝, y) ∂ν)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X Y : C<VAR>inst✝¹ : HasTerminal C<VAR>P : C<VAR>inst✝ : HasBinaryProduct (⊤_ C) P<GOAL>snd ≫ lift (terminal.from P) (𝟙 P) = 𝟙 ((⊤_ C) ⨯ P)
<VAR>F : Type v'<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : StarRing R<VAR>inst✝¹⁴ : NonUnitalSemiring A<VAR>inst✝¹³ : StarRing A<VAR>inst✝¹² : Module R A<VAR>inst✝¹¹ : IsScalarTower R A A<VAR>inst✝¹⁰ : SMulCommClass R A A<VAR>inst✝⁹ : StarModule R A<VAR>inst✝⁸ : NonUnitalSemiring B<VAR>inst✝⁷ : StarRing B<VAR>inst✝⁶ : Module R B<VAR>inst✝⁵ : IsScalarTower R B B<VAR>inst✝⁴ : SMulCommClass R B B<VAR>inst✝³ : StarModule R B<VAR>inst✝² : FunLike F A B<VAR>inst✝¹ : NonUnitalAlgHomClass F R A B<VAR>inst✝ : NonUnitalStarAlgHomClass F R A B<VAR>S : NonUnitalStarSubalgebra R A<GOAL>↑(centralizer R Set.univ) = ↑(center R A)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>K✝ : ℝ≥0<VAR>f : α → β<VAR>x✝ y✝ : α<VAR>r K : ℝ<VAR>h : ∀ (x y : α), dist (f x) (f y) ≤ K * dist x y<VAR>x y : α<GOAL>K ≤ ↑K.toNNReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>as : Array α<VAR>bs : Array β<VAR>i : Nat<VAR>cs : Array γ<VAR>hia : i ≤ as.size<VAR>hib : i ≤ bs.size<VAR>h : ¬(i = as.size ∨ i = bs.size)<GOAL>(if h : i < as.size then let a := as[i]; if h : i < bs.size then let b := bs[i]; zipWithAux f as bs (i + 1) (cs.push (f a b)) else cs else cs).data = cs.data ++ List.zipWith f (List.drop i as.data) (List.drop i bs.data)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<GOAL>IsCompact s ↔ ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x
<VAR>𝕜 : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>inst✝¹⁰ : _root_.RCLike 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E✝<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : InnerProductSpace 𝕜 E✝<VAR>inst✝⁶ : InnerProductSpace ℝ F<VAR>K✝ : Submodule 𝕜 E✝<VAR>inst✝⁵ : HasOrthogonalProjection K✝<VAR>E : Type u_4<VAR>E' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace 𝕜 E'<VAR>f : E ≃ₗᵢ[𝕜] E'<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>x : E'<GOAL>(reflection (Submodule.map (↑f.toLinearEquiv) K)) x = f ((reflection K) (f.symm x))