ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝¹⁰ : AddCommGroup V<VAR>inst✝⁹ : TopologicalSpace V<VAR>inst✝⁸ : TopologicalAddGroup V<VAR>inst✝⁷ : T2Space V<VAR>inst✝⁶ : MeasurableSpace V<VAR>inst✝⁵ : BorelSpace V<VAR>inst✝⁴ : Module ℝ V<VAR>inst✝³ : ContinuousSMul ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure V<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))<VAR>A : V ≃L[ℝ] V'<VAR>this✝¹ : MeasurableSpace V' := borel V'<VAR>this✝ : BorelSpace V'<VAR>Aₘ : V ≃ᵐ V' := A.toHomeomorph.toMeasurableEquiv<VAR>Adualₗ : (V →L[ℝ] ℝ) ≃ₗ[ℝ] V' →L[ℝ] ℝ := { toFun := fun t => t.comp ↑A.symm, map_add' := ⋯, map_smul' := ⋯, invFun := fun t => t.comp ↑A, left_inv := ⋯, right_inv := ⋯ }<VAR>Adual : (V →L[ℝ] ℝ) ≃L[ℝ] V' →L[ℝ] ℝ := { toLinearEquiv := Adualₗ, continuous_toFun := ⋯, continuous_invFun := ⋯ }<VAR>this : (Measure.map (⇑Aₘ) μ).IsAddHaarMeasure<VAR>w : V →L[ℝ] ℝ<GOAL>∫ (v : V), 𝐞 (-w v) • f v ∂μ = ((fun w => ∫ (v : V'), 𝐞 (-w v) • (f ∘ ⇑A.symm) v ∂Measure.map (⇑Aₘ) μ) ∘ Adual.toHomeomorph.toCocompactMap.toFun) w
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝¹⁰ : AddCommGroup V<VAR>inst✝⁹ : TopologicalSpace V<VAR>inst✝⁸ : TopologicalAddGroup V<VAR>inst✝⁷ : T2Space V<VAR>inst✝⁶ : MeasurableSpace V<VAR>inst✝⁵ : BorelSpace V<VAR>inst✝⁴ : Module ℝ V<VAR>inst✝³ : ContinuousSMul ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure V<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))<VAR>A : V ≃L[ℝ] V'<VAR>this✝¹ : MeasurableSpace V' := borel V'<VAR>this✝ : BorelSpace V'<VAR>Aₘ : V ≃ᵐ V' := A.toHomeomorph.toMeasurableEquiv<VAR>Adualₗ : (V →L[ℝ] ℝ) ≃ₗ[ℝ] V' →L[ℝ] ℝ := { toFun := fun t => t.comp ↑A.symm, map_add' := ⋯, map_smul' := ⋯, invFun := fun t => t.comp ↑A, left_inv := ⋯, right_inv := ⋯ }<VAR>Adual : (V →L[ℝ] ℝ) ≃L[ℝ] V' →L[ℝ] ℝ := { toLinearEquiv := Adualₗ, continuous_toFun := ⋯, continuous_invFun := ⋯ }<VAR>this : (Measure.map (⇑Aₘ) μ).IsAddHaarMeasure<VAR>w : V →L[ℝ] ℝ<GOAL>∫ (v : V), 𝐞 (-w v) • f v ∂μ = ∫ (x : V), 𝐞 (-(Adual.toHomeomorph.toCocompactMap.toFun w) (Aₘ x)) • (f ∘ ⇑A.symm) (Aₘ x) ∂μ
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>a b : G<VAR>h : Commute a b<GOAL>a⁻¹ * (b * a) = b
<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>r : α → α → Prop<VAR>a b c d : α<VAR>hr : Reflexive r<VAR>x y : α<GOAL>ReflGen r x y ↔ r x y
<VAR>B : Type u<VAR>inst✝ : Bicategory B<VAR>a b c d e : B<GOAL>(λ_ (𝟙 a)).inv = (ρ_ (𝟙 a)).inv
<VAR>a b c d : Ordinal.{u}<GOAL>d < a ⨳ (b ⨳ c) ↔ ∃ a' < a, ∃ b' < b, ∃ c' < c, d ♯ a' ⨳ (b' ⨳ c) ♯ a' ⨳ (b ⨳ c') ♯ a ⨳ (b' ⨳ c') ≤ a' ⨳ (b ⨳ c) ♯ a ⨳ (b' ⨳ c) ♯ a ⨳ (b ⨳ c') ♯ a' ⨳ (b' ⨳ c')
<VAR>a b c d : Ordinal.{u}<GOAL>(∃ a' < b, ∃ b' < c, ∃ c' < a, toOrdinal (toNatOrdinal d + toNatOrdinal (a' ⨳ b' ⨳ a) + toNatOrdinal (a' ⨳ c ⨳ c') + toNatOrdinal (b ⨳ b' ⨳ c')) ≤ toOrdinal (toNatOrdinal (a' ⨳ c ⨳ a) + toNatOrdinal (b ⨳ b' ⨳ a) + toNatOrdinal (b ⨳ c ⨳ c') + toNatOrdinal (a' ⨳ b' ⨳ c'))) ↔ ∃ a' < a, ∃ b' < b, ∃ c' < c, toOrdinal (toNatOrdinal d + toNatOrdinal (b' ⨳ c ⨳ a') + toNatOrdinal (b ⨳ c' ⨳ a') + toNatOrdinal (b' ⨳ c' ⨳ a)) ≤ toOrdinal (toNatOrdinal (b ⨳ c ⨳ a') + toNatOrdinal (b' ⨳ c ⨳ a) + toNatOrdinal (b ⨳ c' ⨳ a) + toNatOrdinal (b' ⨳ c' ⨳ a'))
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : DivisionRing k<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module k V<VAR>inst✝² : AffineSpace V P<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : Nonempty ι<VAR>p : ι → P<VAR>hi : AffineIndependent k p<GOAL>finrank k ↥(vectorSpan k (Set.range p)) + 1 = Fintype.card ι
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 F<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : CompleteSpace F<VAR>A : E →L[𝕜] F<VAR>p : Submodule 𝕜 E<VAR>hp : Dense ↑p<VAR>x : ↥((↑A).toPMap p).adjoint.domain<VAR>y : ↥((↑(adjoint A)).toPMap ⊤).domain<VAR>hxy : ↑x = ↑y<GOAL>↑((↑A).toPMap p).adjoint x = ↑((↑(adjoint A)).toPMap ⊤) y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 F<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : CompleteSpace F<VAR>A : E →L[𝕜] F<VAR>p : Submodule 𝕜 E<VAR>hp : Dense ↑p<VAR>x : ↥((↑A).toPMap p).adjoint.domain<VAR>y : ↥((↑(adjoint A)).toPMap ⊤).domain<VAR>hxy : ↑x = ↑y<GOAL>Dense ↑((↑A).toPMap p).domain
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 F<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : CompleteSpace F<VAR>A : E →L[𝕜] F<VAR>p : Submodule 𝕜 E<VAR>hp : Dense ↑p<VAR>x : ↥((↑A).toPMap p).adjoint.domain<VAR>y : ↥((↑(adjoint A)).toPMap ⊤).domain<VAR>hxy : ↑x = ↑y<VAR>v : ↥((↑A).toPMap p).domain<GOAL>⟪↑((↑(adjoint A)).toPMap ⊤) y, ↑v⟫_𝕜 = ⟪↑x, ↑((↑A).toPMap p) v⟫_𝕜
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : Group α<VAR>inst✝ : UniformGroup α<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>l' : Filter β<VAR>f f' : ι → β → α<VAR>g g' : β → α<VAR>s : Set β<VAR>hf : UniformCauchySeqOn f l s<VAR>hf' : UniformCauchySeqOn f' l s<VAR>u : Set (α × α)<VAR>hu : u ∈ 𝓤 α<GOAL>∀ᶠ (m : ι × ι) in l ×ˢ l, ∀ x ∈ s, ((f * f') m.1 x, (f * f') m.2 x) ∈ u
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>r : R<GOAL>Finsupp.mapDomain Nat.cast ((monomial n) r).toFinsupp = C r * T ↑n
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Set E<VAR>α : E<GOAL>⨆ x ∈ S, F⟮x⟯ = adjoin F S
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Set E<VAR>α : E<GOAL>adjoin F (⨆ t ∈ S, {t}) = adjoin F S
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Set E<VAR>α : E<GOAL>⨆ t ∈ S, {t} = S
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>c c₁ c₂ p₁ p₂ : P<GOAL>c ∈ perpBisector p₁ p₂ ↔ dist c p₁ = dist c p₂
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>hf : LocallyBoundedVariationOn f s<VAR>b : α<VAR>bs : b ∈ s<VAR>a : α<VAR>as : a ∈ s<VAR>c : α<VAR>cs : c ∈ s<VAR>ac : a ≤ c<GOAL>variationOnFromTo f s c b ≤ variationOnFromTo f s a b
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>hf : LocallyBoundedVariationOn f s<VAR>b : α<VAR>bs : b ∈ s<VAR>a : α<VAR>as : a ∈ s<VAR>c : α<VAR>cs : c ∈ s<VAR>ac : a ≤ c<GOAL>variationOnFromTo f s c b ≤ variationOnFromTo f s a c + variationOnFromTo f s c b
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>inst✝ : Finite α<GOAL>Cardinal.toPartENat (Cardinal.mk α) = ↑(Nat.card α)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>inst✝ : Finite α<GOAL>↑(Nat.card α) = Cardinal.toPartENat (Cardinal.mk α)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>inst✝ : Finite α<GOAL>↑(Nat.card α) = Cardinal.mk α
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<GOAL>∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, |f i| ^ p) ^ (1 / p) * (∑ i ∈ s, |g i| ^ q) ^ (1 / q)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>this : ↑(∑ i ∈ s, (fun i => ⟨|f i|, ⋯⟩) i * (fun i => ⟨|g i|, ⋯⟩) i) ≤ ↑((∑ i ∈ s, (fun i => ⟨|f i|, ⋯⟩) i ^ p) ^ (1 / p) * (∑ i ∈ s, (fun i => ⟨|g i|, ⋯⟩) i ^ q) ^ (1 / q))<GOAL>∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, |f i| ^ p) ^ (1 / p) * (∑ i ∈ s, |g i| ^ q) ^ (1 / q)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>this : ∑ x ∈ s, |f x| * |g x| ≤ (∑ x ∈ s, |f x| ^ p) ^ (1 / p) * (∑ x ∈ s, |g x| ^ q) ^ (1 / q)<GOAL>∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, |f i| ^ p) ^ (1 / p) * (∑ i ∈ s, |g i| ^ q) ^ (1 / q)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>this : ∑ x ∈ s, |f x| * |g x| ≤ (∑ x ∈ s, |f x| ^ p) ^ (1 / p) * (∑ x ∈ s, |g x| ^ q) ^ (1 / q)<VAR>i : ι<VAR>x✝ : i ∈ s<GOAL>f i * g i ≤ |f i| * |g i|
<VAR>X : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : Semiring R<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalSemiring R<VAR>s : Set X<VAR>f : C(X, R)<GOAL>f ∉ idealOfSet R s ↔ ∃ x ∈ sᶜ, f x ≠ 0
<VAR>X : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : Semiring R<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalSemiring R<VAR>s : Set X<VAR>f : C(X, R)<GOAL>(¬∀ ⦃x : X⦄, x ∈ sᶜ → f x = 0) ↔ ∃ x ∈ sᶜ, f x ≠ 0
<VAR>X : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : Semiring R<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalSemiring R<VAR>s : Set X<VAR>f : C(X, R)<GOAL>(∃ x ∈ sᶜ, f x ≠ 0) ↔ ∃ x ∈ sᶜ, f x ≠ 0
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β✝<VAR>β : Type u_3<VAR>f : List α → β<VAR>r : List α → Filter β<VAR>h_nil : Tendsto f (pure []) (r [])<VAR>h_cons : ∀ (l : List α) (a : α), Tendsto f (𝓝 l) (r l) → Tendsto (fun p => f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))<GOAL>Tendsto f (𝓝 []) (r [])
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β✝<VAR>β : Type u_3<VAR>f : List α → β<VAR>r : List α → Filter β<VAR>h_nil : Tendsto f (pure []) (r [])<VAR>h_cons : ∀ (l : List α) (a : α), Tendsto f (𝓝 l) (r l) → Tendsto (fun p => f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))<VAR>a : α<VAR>l : List α<GOAL>Tendsto f (𝓝 (a :: l)) (r (a :: l))
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β✝<VAR>β : Type u_3<VAR>f : List α → β<VAR>r : List α → Filter β<VAR>h_nil : Tendsto f (pure []) (r [])<VAR>h_cons : ∀ (l : List α) (a : α), Tendsto f (𝓝 l) (r l) → Tendsto (fun p => f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))<VAR>a : α<VAR>l : List α<GOAL>Tendsto (fun p => f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M✝ : Type u_4<VAR>M : Type u<VAR>inst✝ : LeftCancelMonoid M<VAR>a b : M<GOAL>a * b = a ↔ a * b = a * 1
<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 g : α → β<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<GOAL>edist (toL1 f hf) (toL1 g hg) = ∫⁻ (a : α), edist (f a) (g 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 g : α → β<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<GOAL>(if 1 = ⊤ then eLpNormEssSup (f - g) μ else ∫⁻ (a : α), ↑‖f a - g a‖₊ ∂μ) = ∫⁻ (a : α), edist (f a) (g a) ∂μ
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝⁶ : DivisionRing K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>inst✝³ : AddCommGroup V'<VAR>inst✝² : Module K V'<VAR>inst✝¹ : AddCommGroup V₁<VAR>inst✝ : Module K V₁<VAR>p : Submodule K V<GOAL>Module.rank K (V ⧸ p) + Module.rank K ↥p = Module.rank K V
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>φ ψ : R[X]<VAR>n : ℕ<GOAL>(PowerSeries.coeff R n) ↑(φ * ψ) = (PowerSeries.coeff R n) (↑φ * ↑ψ)
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>R I J X Y : Set α<VAR>N M : Matroid α<VAR>hR : R ⊂ M.E<GOAL>M ↾ R <r M
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>R I J X Y : Set α<VAR>N M : Matroid α<VAR>hR : R ⊂ M.E<VAR>h : M ↾ R = M<GOAL>False
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>R I J X Y : Set α<VAR>N M : Matroid α<VAR>hR : R ⊂ R<VAR>h : M ↾ R = M<GOAL>False
<VAR>G : Type u_1<VAR>inst✝⁷ : MeasurableSpace G<VAR>μ : Measure G<VAR>g : G<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : TopologicalGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : μ.IsMulLeftInvariant<VAR>inst✝¹ : μ.Regular<VAR>inst✝ : NeZero μ<VAR>f : G → ℝ≥0∞<VAR>hf : Continuous f<GOAL>∫⁻ (x : G), f x ∂μ = 0 ↔ f = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>a b : α<VAR>s : Set α<GOAL>s = ∅ ∨ s.encard = ⊤ ∨ ∃ a ∈ s, (s \ {a}).encard < s.encard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>a✝ b : α<VAR>s : Set α<VAR>x✝ : s.Nonempty<VAR>a : α<VAR>ha : a ∈ s<VAR>hfin : s.Finite<GOAL>(s \ {a}).encard < s.encard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>a✝ b : α<VAR>s : Set α<VAR>x✝ : s.Nonempty<VAR>a : α<VAR>ha : a ∈ s<VAR>hfin : s.Finite<GOAL>(s \ {a}).encard < (s \ {a}).encard + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>a✝ b : α<VAR>s : Set α<VAR>x✝ : s.Nonempty<VAR>a : α<VAR>ha : a ∈ s<VAR>hfin : s.Finite<GOAL>(s \ {a}).encard + 0 < (s \ {a}).encard + 1
<VAR>α : Type u_1<VAR>K : Type u_2<VAR>inst✝ : LinearOrderedField K<VAR>a b r : K<VAR>hr : 0 < r<VAR>x : K<GOAL>x ∈ r • Iic a ↔ x ∈ Iic (r • a)
<VAR>α : Type u_1<VAR>K : Type u_2<VAR>inst✝ : LinearOrderedField K<VAR>a b r : K<VAR>hr : 0 < r<VAR>x : K<GOAL>(∃ y ∈ Iic a, r * y = x) ↔ x ∈ Iic (r * a)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : Group α<VAR>s t : Set α<GOAL>Nat.card ↑(s / t) ≤ Nat.card ↑s * Nat.card ↑t
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : Group α<VAR>s t : Set α<GOAL>Nat.card ↑(s * t⁻¹) ≤ Nat.card ↑s * Nat.card ↑t⁻¹
<VAR>ι : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>p : Type u_4<VAR>α : Type u_5<VAR>R : Type u_6<VAR>S : Type u_7<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype p<VAR>inst✝¹ : AddCommMonoid R<VAR>inst✝ : DecidableEq p<VAR>M : p → Matrix n n R<GOAL>(blockDiagonal M).trace = ∑ i : p, (M i).trace
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁸ : SeminormedAddCommGroup E<VAR>inst✝¹⁷ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁶ : SeminormedAddCommGroup F<VAR>inst✝¹⁵ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹⁴ : SeminormedAddCommGroup G<VAR>inst✝¹³ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₂<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁷ : NormedSpace 𝕜₂ F<VAR>inst✝⁶ : NormedSpace 𝕜 Fₗ<VAR>inst✝⁵ : NormedSpace 𝕜₃ G<VAR>inst✝⁴ : NormedSpace 𝕜 Gₗ<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝² : FunLike 𝓕 E F<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>inst✝ : RingHomIsometric σ₂₃<VAR>f✝ g : E →SL[σ₁₂] F<VAR>h : F →SL[σ₂₃] G<VAR>x : E<VAR>f : E →SL[σ₁₂] F<GOAL>↑‖f‖₊ = ↑(sInf {c | ∀ (x : E), ‖f x‖₊ ≤ c * ‖x‖₊})
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁸ : SeminormedAddCommGroup E<VAR>inst✝¹⁷ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁶ : SeminormedAddCommGroup F<VAR>inst✝¹⁵ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹⁴ : SeminormedAddCommGroup G<VAR>inst✝¹³ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₂<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁷ : NormedSpace 𝕜₂ F<VAR>inst✝⁶ : NormedSpace 𝕜 Fₗ<VAR>inst✝⁵ : NormedSpace 𝕜₃ G<VAR>inst✝⁴ : NormedSpace 𝕜 Gₗ<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝² : FunLike 𝓕 E F<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>inst✝ : RingHomIsometric σ₂₃<VAR>f✝ g : E →SL[σ₁₂] F<VAR>h : F →SL[σ₂₃] G<VAR>x : E<VAR>f : E →SL[σ₁₂] F<GOAL>sInf {c | 0 ≤ c ∧ ∀ (x : E), ‖f x‖ ≤ c * ‖x‖} = sInf {x | ∃ (h : 0 ≤ x), ⟨x, h⟩ ∈ {c | ∀ (x : E), ‖f x‖₊ ≤ c * ‖x‖₊}}
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝¹ : HasCokernel f<VAR>X' Y' : C<VAR>f' : X' ⟶ Y'<VAR>inst✝ : HasCokernel f'<VAR>p : X ≅ X'<VAR>q : Y ≅ Y'<VAR>w : f ≫ q.hom = p.hom ≫ f'<GOAL>f' ≫ q.inv = p.inv ≫ f
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝¹ : HasCokernel f<VAR>X' Y' : C<VAR>f' : X' ⟶ Y'<VAR>inst✝ : HasCokernel f'<VAR>p : X ≅ X'<VAR>q : Y ≅ Y'<VAR>w : f ≫ q.hom = p.hom ≫ f'<GOAL>(f' ≫ q.inv) ≫ q.hom = (p.inv ≫ f) ≫ q.hom
<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>n m✝ : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>m : σ →₀ ℕ<GOAL>(monomial m) 1 = m.prod fun n e => X n ^ e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>f : α → β<VAR>g : α → γ<VAR>g' : β → γ<GOAL>(range f).restrict (extend f g g') = fun x => g (Exists.choose ⋯)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Preadditive C<VAR>D : Type u_1<VAR>inst✝¹ : Category.{v₁, u_1} D<VAR>inst✝ : Preadditive D<VAR>ι✝¹ : Type<VAR>fintype✝¹ : Fintype ι✝¹<VAR>X✝¹ : ι✝¹ → C<VAR>i✝ : ((𝟭 C).mapMat_.obj (Mat_.mk ι✝¹ X✝¹)).ι<VAR>ι✝ : Type<VAR>fintype✝ : Fintype ι✝<VAR>X✝ : ι✝ → C<VAR>j✝ : ((𝟭 (Mat_ C)).obj (Mat_.mk ι✝ X✝)).ι<VAR>f : Mat_.mk ι✝¹ X✝¹ ⟶ Mat_.mk ι✝ X✝<GOAL>((𝟭 C).mapMat_.map f ≫ ((fun M => eqToIso ⋯) (Mat_.mk ι✝ X✝)).hom) i✝ j✝ = (((fun M => eqToIso ⋯) (Mat_.mk ι✝¹ X✝¹)).hom ≫ (𝟭 (Mat_ C)).map f) i✝ j✝
<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>F : Type u_7<VAR>G : Type u_8<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a✝ a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>a : E<GOAL>dist a 1 = ‖a‖
<VAR>S : Finset Λ'<VAR>q : Λ'<VAR>K : Finset Λ'<VAR>H₁ : Λ'.Supports S q<VAR>H₂ : trStmts₁ q ∪ K ⊆ S<VAR>H₃ : K ⊆ S → Supports K S<GOAL>Supports (trStmts₁ q ∪ K) S
<VAR>S : Finset Λ'<VAR>q : Λ'<VAR>K : Finset Λ'<VAR>H₁ : Λ'.Supports S q<VAR>H₃ : K ⊆ S → Supports K S<VAR>H₂ : trStmts₁ q ⊆ S ∧ K ⊆ S<GOAL>Supports (trStmts₁ q ∪ K) S
<VAR>e : ONote<VAR>n : ℕ+<VAR>a o : ONote<VAR>h₁ : (e.oadd n a).NF<VAR>h₂ : o.NF<GOAL>(e.oadd n a + o).repr = (e.oadd n a).repr + o.repr
<VAR>e : ONote<VAR>n : ℕ+<VAR>a o : ONote<VAR>h₁ : (e.oadd n a).NF<VAR>h₂ : o.NF<VAR>this : a.NF<GOAL>(e.oadd n a + o).repr = (e.oadd n a).repr + o.repr
<VAR>e : ONote<VAR>n : ℕ+<VAR>a o : ONote<VAR>h₁ : (e.oadd n a).NF<VAR>h₂ : o.NF<VAR>this : a.NF<VAR>h' : (a.add o).repr = a.repr + o.repr<VAR>nf : (a.add o).NF<GOAL>((e.oadd n a).add o).repr = (e.oadd n a).repr + o.repr
<VAR>e : ONote<VAR>n : ℕ+<VAR>a o : ONote<VAR>h₁ : (e.oadd n a).NF<VAR>h₂ : o.NF<VAR>this : a.NF<VAR>h' : (a.add o).repr = a.repr + o.repr<VAR>e' : ONote<VAR>n' : ℕ+<VAR>a' : ONote<VAR>h : a.add o = e'.oadd n' a'<VAR>nf : (e'.oadd n' a').NF<GOAL>(match e.cmp e' with | Ordering.lt => e'.oadd n' a' | Ordering.eq => e.oadd (n + n') a' | Ordering.gt => e.oadd n (e'.oadd n' a')).repr = ω ^ e.repr * ↑↑n + (ω ^ e'.repr * ↑↑n' + a'.repr)
<VAR>e : ONote<VAR>n : ℕ+<VAR>a o : ONote<VAR>h₁ : (e.oadd n a).NF<VAR>h₂ : o.NF<VAR>this✝ : a.NF<VAR>h' : (a.add o).repr = a.repr + o.repr<VAR>e' : ONote<VAR>n' : ℕ+<VAR>a' : ONote<VAR>h : a.add o = e'.oadd n' a'<VAR>nf : (e'.oadd n' a').NF<VAR>this : e.NF<GOAL>(match e.cmp e' with | Ordering.lt => e'.oadd n' a' | Ordering.eq => e.oadd (n + n') a' | Ordering.gt => e.oadd n (e'.oadd n' a')).repr = ω ^ e.repr * ↑↑n + (ω ^ e'.repr * ↑↑n' + a'.repr)
<VAR>e : ONote<VAR>n : ℕ+<VAR>a o : ONote<VAR>h₁ : (e.oadd n a).NF<VAR>h₂ : o.NF<VAR>this✝¹ : a.NF<VAR>h' : (a.add o).repr = a.repr + o.repr<VAR>e' : ONote<VAR>n' : ℕ+<VAR>a' : ONote<VAR>h : a.add o = e'.oadd n' a'<VAR>nf : (e'.oadd n' a').NF<VAR>this✝ : e.NF<VAR>this : e'.NF<GOAL>(match e.cmp e' with | Ordering.lt => e'.oadd n' a' | Ordering.eq => e.oadd (n + n') a' | Ordering.gt => e.oadd n (e'.oadd n' a')).repr = ω ^ e.repr * ↑↑n + (ω ^ e'.repr * ↑↑n' + a'.repr)
<VAR>e : ONote<VAR>n : ℕ+<VAR>a o : ONote<VAR>h₁ : (e.oadd n a).NF<VAR>h₂ : o.NF<VAR>this✝¹ : a.NF<VAR>h' : (a.add o).repr = a.repr + o.repr<VAR>e' : ONote<VAR>n' : ℕ+<VAR>a' : ONote<VAR>h : a.add o = e'.oadd n' a'<VAR>nf : (e'.oadd n' a').NF<VAR>this✝ : e.NF<VAR>this : e'.NF<VAR>ee : (e.cmp e').Compares e e'<GOAL>(match e.cmp e' with | Ordering.lt => e'.oadd n' a' | Ordering.eq => e.oadd (n + n') a' | Ordering.gt => e.oadd n (e'.oadd n' a')).repr = ω ^ e.repr * ↑↑n + (ω ^ e'.repr * ↑↑n' + a'.repr)
<VAR>e : ONote<VAR>n : ℕ+<VAR>a o : ONote<VAR>h₁ : (e.oadd n a).NF<VAR>h₂ : o.NF<VAR>this✝¹ : a.NF<VAR>h' : (a.add o).repr = a.repr + o.repr<VAR>e' : ONote<VAR>n' : ℕ+<VAR>a' : ONote<VAR>h : a.add o = e'.oadd n' a'<VAR>nf : (e'.oadd n' a').NF<VAR>this✝ : e.NF<VAR>this : e'.NF<VAR>he : e.cmp e' = Ordering.lt<VAR>ee : e < e'<GOAL>ω ^ e'.repr * ↑↑n' + a'.repr = ω ^ e.repr * ↑↑n + (ω ^ e'.repr * ↑↑n' + a'.repr)
<VAR>e : ONote<VAR>n : ℕ+<VAR>a o : ONote<VAR>h₁ : (e.oadd n a).NF<VAR>h₂ : o.NF<VAR>this✝¹ : a.NF<VAR>h' : (a.add o).repr = a.repr + o.repr<VAR>e' : ONote<VAR>n' : ℕ+<VAR>a' : ONote<VAR>h : a.add o = e'.oadd n' a'<VAR>nf : (e'.oadd n' a').NF<VAR>this✝ : e.NF<VAR>this : e'.NF<VAR>he : e.cmp e' = Ordering.eq<VAR>ee : e = e'<GOAL>ω ^ e.repr * (↑↑n + ↑↑n') + a'.repr = ω ^ e.repr * ↑↑n + (ω ^ e'.repr * ↑↑n' + a'.repr)
<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✝¹¹ : Semiring R₃<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : AddCommMonoid M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R₂ M₂<VAR>inst✝⁴ : Module R₃ M₃<VAR>σ₂₁ : R₂ →+* R<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝³ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>F : Type u_11<VAR>inst✝² : FunLike F M M₂<VAR>inst✝¹ : SemilinearMapClass F τ₁₂ M M₂<VAR>inst✝ : RingHomSurjective τ₁₂<VAR>f : M →ₛₗ[τ₁₂] M₂<GOAL>range f ≤ ⊥ ↔ f = 0
<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✝¹¹ : Semiring R₃<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : AddCommMonoid M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R₂ M₂<VAR>inst✝⁴ : Module R₃ M₃<VAR>σ₂₁ : R₂ →+* R<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝³ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>F : Type u_11<VAR>inst✝² : FunLike F M M₂<VAR>inst✝¹ : SemilinearMapClass F τ₁₂ M M₂<VAR>inst✝ : RingHomSurjective τ₁₂<VAR>f : M →ₛₗ[τ₁₂] M₂<GOAL>comap f ⊥ = ⊤ ↔ f = 0
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l₁ l₂ : List α<GOAL>(a :: l₁).diff l₂ <+~ a :: l₁.diff l₂
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁷ : OrderedRing R<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : Module R V<VAR>inst✝⁴ : AddTorsor V P<VAR>inst✝³ : AddCommGroup V'<VAR>inst✝² : Module R V'<VAR>inst✝¹ : AddTorsor V' P'<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>x y : P<VAR>r : R<VAR>hxy : ¬x = y<GOAL>Wbtw R x ((lineMap x y) r) y ↔ x = y ∨ r ∈ Set.Icc 0 1
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>L : IntermediateField F E<VAR>h : IsPurelyInseparable (↥L) E<VAR>x : E<VAR>hx : x ∈ separableClosure F E<GOAL>x ∈ L