ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝⁴ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : SecondCountableTopology α<VAR>inst✝¹ : BorelSpace α<VAR>ρ ν : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ν<VAR>hρ : ρ ≪ μ<VAR>s : Set α<VAR>hs : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ν a<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>x✝ : ν s < ⊤<VAR>U : Set α<VAR>sU : s ⊆ U<VAR>U_open : IsOpen U<VAR>νU : ν U ≤ ν s + ↑ε<VAR>f : α → Set (Set α) := fun x => {a | ρ a ≤ ν a ∧ a ⊆ U}<GOAL>ρ s ≤ ν s + ↑ε
<VAR>α : Type u_1<VAR>inst✝⁴ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : SecondCountableTopology α<VAR>inst✝¹ : BorelSpace α<VAR>ρ ν : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ν<VAR>hρ : ρ ≪ μ<VAR>s : Set α<VAR>hs : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ν a<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>x✝ : ν s < ⊤<VAR>U : Set α<VAR>sU : s ⊆ U<VAR>U_open : IsOpen U<VAR>νU : ν U ≤ ν s + ↑ε<VAR>f : α → Set (Set α) := fun x => {a | ρ a ≤ ν a ∧ a ⊆ U}<VAR>h : v.FineSubfamilyOn f s<GOAL>ρ s ≤ ν s + ↑ε
<VAR>α : Type u_1<VAR>inst✝⁴ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : SecondCountableTopology α<VAR>inst✝¹ : BorelSpace α<VAR>ρ ν : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ν<VAR>hρ : ρ ≪ μ<VAR>s : Set α<VAR>hs : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ν a<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>x✝ : ν s < ⊤<VAR>U : Set α<VAR>sU : s ⊆ U<VAR>U_open : IsOpen U<VAR>νU : ν U ≤ ν s + ↑ε<VAR>f : α → Set (Set α) := fun x => {a | ρ a ≤ ν a ∧ a ⊆ U}<VAR>h : v.FineSubfamilyOn f s<VAR>this : Encodable ↑h.index<GOAL>ρ s ≤ ν s + ↑ε
<VAR>α : Type u_1<VAR>inst✝⁸ : TopologicalSpace α<VAR>inst✝⁷ : NormalSpace α<VAR>inst✝⁶ : R1Space α<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : WeaklyLocallyCompactSpace α<VAR>inst✝ : μ.Regular<VAR>f : α → E<VAR>hf : Integrable f μ<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ g, HasCompactSupport g ∧ ∫ (x : α), ‖f x - g x‖ ∂μ ≤ ε ∧ Continuous g ∧ Integrable g μ
<VAR>α : Type u_1<VAR>inst✝⁸ : TopologicalSpace α<VAR>inst✝⁷ : NormalSpace α<VAR>inst✝⁶ : R1Space α<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : WeaklyLocallyCompactSpace α<VAR>inst✝ : μ.Regular<VAR>f : α → E<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hf : Memℒp f (ENNReal.ofReal 1) μ<GOAL>∃ g, HasCompactSupport g ∧ ∫ (x : α), ‖f x - g x‖ ∂μ ≤ ε ∧ Continuous g ∧ Memℒp g (ENNReal.ofReal 1) μ
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Finite α<VAR>f : α → β<VAR>hf : Surjective f<GOAL>Nat.card β ≤ Nat.card α
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Finite α<VAR>f : α → β<VAR>hf : Surjective f<VAR>this : lift.{u, v} #β ≤ lift.{v, u} #α<GOAL>Nat.card β ≤ Nat.card α
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>m M N k : ℕ<VAR>blocks_fun : Fin k → ℕ<VAR>hi : ⟨k, blocks_fun⟩ ∈ compPartialSumSource m M N<GOAL>{ blocks := ofFn fun a => blocks_fun a, blocks_pos := ⋯, blocks_sum := ⋯ }.length = k
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End R M<VAR>μ : R<VAR>k : ℕ<VAR>hk : 0 < k<VAR>hμ : f.HasEigenvalue μ<GOAL>f.HasGenEigenvalue μ k
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End R M<VAR>μ : R<VAR>k : ℕ<VAR>hk : 0 < k<VAR>hμ : f.HasEigenvalue μ<GOAL>f.HasGenEigenvalue μ (Nat.succ 0)
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End R M<VAR>μ : R<VAR>k : ℕ<VAR>hk : 0 < k<VAR>hμ : f.HasEigenvalue μ<GOAL>LinearMap.ker (f - (algebraMap R (End R M)) μ) ≠ ⊥
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>a✝ b✝ c a b : α<VAR>inst✝ : DecidablePred fun x => x ≤ a<VAR>hab : a < b<VAR>x : α<GOAL>x ∈ filter (fun x => x ≤ a) (Ico a b) ↔ x ∈ {a}
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>a✝ b✝ c a b : α<VAR>inst✝ : DecidablePred fun x => x ≤ a<VAR>hab : a < b<VAR>x : α<GOAL>x = a ∧ x < b ↔ x = a
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε✝ : ℝ<VAR>s✝ t : Set α<VAR>x : α<VAR>ε δ : ℝ<VAR>s : Set α<GOAL>thickening ε (thickening δ s) ⊆ thickening (ε + δ) s
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε✝ : ℝ<VAR>s✝ t : Set α<VAR>x : α<VAR>ε δ : ℝ<VAR>s : Set α<VAR>hε : ε ≤ 0<GOAL>thickening ε (thickening δ s) ⊆ thickening (ε + δ) s
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε✝ : ℝ<VAR>s✝ t : Set α<VAR>x : α<VAR>ε δ : ℝ<VAR>s : Set α<VAR>hε : 0 ≤ ε<GOAL>thickening ε (thickening δ s) ⊆ thickening (ε + δ) s
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε✝ : ℝ<VAR>s✝ t : Set α<VAR>x : α<VAR>ε δ : ℝ<VAR>s : Set α<VAR>hε : 0 ≤ ε<VAR>hδ : δ ≤ 0<GOAL>thickening ε (thickening δ s) ⊆ thickening (ε + δ) s
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε✝ : ℝ<VAR>s✝ t : Set α<VAR>x : α<VAR>ε δ : ℝ<VAR>s : Set α<VAR>hε : 0 ≤ ε<VAR>hδ : 0 ≤ δ<GOAL>thickening ε (thickening δ s) ⊆ thickening (ε + δ) s
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε✝ : ℝ<VAR>s✝ t : Set α<VAR>x✝ : α<VAR>ε δ : ℝ<VAR>s : Set α<VAR>hε : 0 ≤ ε<VAR>hδ : 0 ≤ δ<VAR>x : α<GOAL>x ∈ thickening ε (thickening δ s) → x ∈ thickening (ε + δ) s
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε✝ : ℝ<VAR>s✝ t : Set α<VAR>x✝ : α<VAR>ε δ : ℝ<VAR>s : Set α<VAR>hε : 0 ≤ ε<VAR>hδ : 0 ≤ δ<VAR>x : α<GOAL>(∃ z, (∃ z_1 ∈ s, edist z z_1 < ENNReal.ofReal δ) ∧ edist x z < ENNReal.ofReal ε) → ∃ z ∈ s, edist x z < ENNReal.ofReal ε + ENNReal.ofReal δ
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : CompleteLattice α✝<VAR>α : Type u_6<VAR>β : Type u_7<VAR>inst✝ : CompleteLattice β<VAR>f : Filter α<VAR>u : α → β<VAR>x : β<VAR>h : ∃ᶠ (a : α) in f, u a ≤ x<GOAL>liminf u f ≤ x
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : CompleteLattice α✝<VAR>α : Type u_6<VAR>β : Type u_7<VAR>inst✝ : CompleteLattice β<VAR>f : Filter α<VAR>u : α → β<VAR>x : β<VAR>h : ∃ᶠ (a : α) in f, u a ≤ x<GOAL>sSup {a | ∀ᶠ (n : α) in f, a ≤ u n} ≤ x
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : CompleteLattice α✝<VAR>α : Type u_6<VAR>β : Type u_7<VAR>inst✝ : CompleteLattice β<VAR>f : Filter α<VAR>u : α → β<VAR>x : β<VAR>h : ∃ᶠ (a : α) in f, u a ≤ x<VAR>b : β<VAR>hb : b ∈ {a | ∀ᶠ (n : α) in f, a ≤ u n}<GOAL>b ≤ x
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : CompleteLattice α✝<VAR>α : Type u_6<VAR>β : Type u_7<VAR>inst✝ : CompleteLattice β<VAR>f : Filter α<VAR>u : α → β<VAR>x : β<VAR>h : ∃ᶠ (a : α) in f, u a ≤ x<VAR>b : β<VAR>hb : b ∈ {a | ∀ᶠ (n : α) in f, a ≤ u n}<VAR>hbx : ∃ᶠ (x_1 : α) in f, b ≤ x<GOAL>b ≤ x
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ μ₁ μ₂ ν ν₁ ν₂ : Measure α<VAR>h : μ ⟂ₘ ν<VAR>s : Set α<GOAL>μ.restrict s ⟂ₘ ν
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ μ₁ μ₂ ν ν₁ ν₂ : Measure α<VAR>h : μ ⟂ₘ ν<VAR>s : Set α<GOAL>(μ.restrict s) h.nullSet = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ μ₁ μ₂ ν ν₁ ν₂ : Measure α<VAR>h : μ ⟂ₘ ν<VAR>s : Set α<GOAL>μ (h.nullSet ∩ s) = 0
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>C K L : HomologicalComplex V c<VAR>φ : K ⟶ L<VAR>hφ : ∀ (i : ι), Epi (φ.f i)<VAR>Z✝ : HomologicalComplex V c<VAR>g h : L ⟶ Z✝<VAR>eq : φ ≫ g = φ ≫ h<VAR>i : ι<GOAL>g.f i = h.f i
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>C K L : HomologicalComplex V c<VAR>φ : K ⟶ L<VAR>hφ : ∀ (i : ι), Epi (φ.f i)<VAR>Z✝ : HomologicalComplex V c<VAR>g h : L ⟶ Z✝<VAR>eq : φ ≫ g = φ ≫ h<VAR>i : ι<GOAL>φ.f i ≫ g.f i = φ.f i ≫ h.f i
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ l : List α<VAR>a : α<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>h : n < (a :: l).length<GOAL>n - 1 < l.length
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ l : List α<VAR>a : α<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>h : l.length ≤ n - 1<GOAL>(a :: l).length ≤ n
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ l : List α<VAR>a : α<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>h : l.length ≤ n - 1<GOAL>l.length + 1 ≤ n
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : DecidableEq L<VAR>inst✝⁷ : Algebra R K<VAR>inst✝⁶ : IsFractionRing R K<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra R L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsDedekindDomain R<VAR>I J : ↥(Ideal R)⁰<GOAL>mk0 I = mk0 J ↔ ∃ x, ∃ (_ : x ≠ 0), spanSingleton R⁰ x * ↑↑I = ↑↑J
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : DecidableEq L<VAR>inst✝⁷ : Algebra R K<VAR>inst✝⁶ : IsFractionRing R K<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra R L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsDedekindDomain R<VAR>I J : ↥(Ideal R)⁰<GOAL>(equiv K) (mk0 I) = (equiv K) (mk0 J) ↔ ∃ x, ∃ (_ : x ≠ 0), spanSingleton R⁰ x * ↑↑I = ↑↑J
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : DecidableEq L<VAR>inst✝⁷ : Algebra R K<VAR>inst✝⁶ : IsFractionRing R K<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra R L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsDedekindDomain R<VAR>I J : ↥(Ideal R)⁰<GOAL>(∃ z, (∃ x, spanSingleton R⁰ x = ↑z) ∧ ↑↑I * ↑z = ↑↑J) ↔ ∃ x, x ≠ 0 ∧ spanSingleton R⁰ x * ↑↑I = ↑↑J
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>p : ℝ≥0<VAR>hp : p ≠ 0<GOAL>eLpNorm f (↑p) μ ^ ↑p = ∫⁻ (x : α), ↑‖f x‖₊ ^ ↑p ∂μ
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c✝ c₁ c₂ : ℝ≥0<VAR>ε✝ ε₁ ε₂ : ℝ<VAR>π₁ π₂ : TaggedPrepartition I<VAR>h : Integrable I l f vol<VAR>ε : ℝ<VAR>c : ℝ≥0<VAR>h₀ : 0 < ε<GOAL>l.RCond (⋯.choose c)
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c✝ c₁ c₂ : ℝ≥0<VAR>ε✝ ε₁ ε₂ : ℝ<VAR>π₁ π₂ : TaggedPrepartition I<VAR>h : Integrable I l f vol<VAR>ε : ℝ<VAR>c : ℝ≥0<VAR>h₀ : ¬0 < ε<GOAL>l.RCond ((fun x x => ⟨1, convergenceR.proof_3⟩) c)
<VAR>V W : SemiNormedGrp₁<VAR>i : V ≅ W<GOAL>Isometry ⇑i.hom
<VAR>V W : SemiNormedGrp₁<VAR>i : V ≅ W<GOAL>Isometry ⇑{ toFun := ⇑i.hom, map_zero' := ⋯, map_add' := ⋯ }
<VAR>V W : SemiNormedGrp₁<VAR>i : V ≅ W<VAR>v : ↑V<GOAL>‖{ toFun := ⇑i.hom, map_zero' := ⋯, map_add' := ⋯ } v‖ = ‖v‖
<VAR>V W : SemiNormedGrp₁<VAR>i : V ≅ W<VAR>v : ↑V<GOAL>‖v‖ ≤ ‖↑i.hom v‖
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝² : Primcodable α<VAR>inst✝¹ : Primcodable σ<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>x✝ : RePred p ∧ RePred fun a => ¬p a<VAR>h₁ : RePred p<VAR>h₂ : RePred fun a => ¬p a<GOAL>Computable fun a => decide (p a)
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝² : Primcodable α<VAR>inst✝¹ : Primcodable σ<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>x✝ : RePred p ∧ RePred fun a => ¬p a<VAR>h₁ : RePred p<VAR>h₂ : RePred fun a => ¬p a<VAR>k : α →. Bool<VAR>pk : Partrec k<VAR>hk : ∀ (a : α) (x : Bool), x ∈ k a ↔ x ∈ Part.map (fun b => true) (Part.assert (p a) fun x => Part.some ()) ∨ x ∈ Part.map (fun b => false) (Part.assert ((fun a => ¬p a) a) fun x => Part.some ())<GOAL>Computable fun a => decide (p a)
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝² : Primcodable α<VAR>inst✝¹ : Primcodable σ<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>x✝ : RePred p ∧ RePred fun a => ¬p a<VAR>h₁ : RePred p<VAR>h₂ : RePred fun a => ¬p a<VAR>k : α →. Bool<VAR>pk : Partrec k<VAR>hk : ∀ (a : α) (x : Bool), x ∈ k a ↔ x ∈ Part.map (fun b => true) (Part.assert (p a) fun x => Part.some ()) ∨ x ∈ Part.map (fun b => false) (Part.assert ((fun a => ¬p a) a) fun x => Part.some ())<VAR>n : α<GOAL>(fun a => decide (p a)) n ∈ k n
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝² : Primcodable α<VAR>inst✝¹ : Primcodable σ<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>x✝ : RePred p ∧ RePred fun a => ¬p a<VAR>h₁ : RePred p<VAR>h₂ : RePred fun a => ¬p a<VAR>k : α →. Bool<VAR>pk : Partrec k<VAR>hk : ∀ (a : α) (x : Bool), x ∈ k a ↔ x ∈ Part.map (fun b => true) (Part.assert (p a) fun x => Part.some ()) ∨ x ∈ Part.map (fun b => false) (Part.assert ((fun a => ¬p a) a) fun x => Part.some ())<VAR>n : α<GOAL>(fun a => decide (p a)) n ∈ Part.map (fun b => true) (Part.assert (p n) fun x => Part.some ()) ∨ (fun a => decide (p a)) n ∈ Part.map (fun b => false) (Part.assert ((fun a => ¬p a) n) fun x => Part.some ())
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝² : Primcodable α<VAR>inst✝¹ : Primcodable σ<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>x✝ : RePred p ∧ RePred fun a => ¬p a<VAR>h₁ : RePred p<VAR>h₂ : RePred fun a => ¬p a<VAR>k : α →. Bool<VAR>pk : Partrec k<VAR>hk : ∀ (a : α) (x : Bool), x ∈ k a ↔ x ∈ Part.map (fun b => true) (Part.assert (p a) fun x => Part.some ()) ∨ x ∈ Part.map (fun b => false) (Part.assert ((fun a => ¬p a) a) fun x => Part.some ())<VAR>n : α<GOAL>p n ∨ ¬p n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set (Setoid α)<GOAL>sSup s = EqvGen.Setoid (sSup (Rel '' s))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set (Setoid α)<GOAL>(EqvGen.Setoid fun x y => ∃ r ∈ s, r.Rel x y) = EqvGen.Setoid (⨆ a ∈ s, a.Rel)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set (Setoid α)<VAR>x y : α<GOAL>(∃ r ∈ s, r.Rel x y) ↔ (⨆ a ∈ s, a.Rel) x y
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>n : ℕ<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>h : HasFiniteFPowerSeriesOnBall f p x n r<GOAL>HasFiniteFPowerSeriesOnBall (fderiv 𝕜 f) p.derivSeries x (n - 1) r
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>h : HasFiniteFPowerSeriesOnBall f p x 0 r<GOAL>HasFiniteFPowerSeriesOnBall (fderiv 𝕜 f) p.derivSeries x (0 - 1) r
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>n : ℕ<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>h : HasFiniteFPowerSeriesOnBall f p x n r<VAR>hn : n ≠ 0<GOAL>HasFiniteFPowerSeriesOnBall (fderiv 𝕜 f) p.derivSeries x (n - 1) r
<VAR>m n : ℕ<VAR>hn : 1 < n<VAR>h : n ! = m !<GOAL>n = m
<VAR>m n : ℕ<VAR>hn : 1 < n<VAR>h : n ! = m !<VAR>hnm : n < m<GOAL>n = m
<VAR>n : ℕ<VAR>hn : 1 < n<VAR>h : n ! = n !<GOAL>n = n
<VAR>m n : ℕ<VAR>hn : 1 < n<VAR>h : n ! = m !<VAR>hnm : m < n<GOAL>n = m
<VAR>m n : ℕ<VAR>hn : 1 < m<VAR>h : n ! = m !<VAR>hnm : m < n<GOAL>n = m
<VAR>m n : ℕ<VAR>hn : 1 < m<VAR>h : n ! = m !<VAR>hnm : m ! < m !<GOAL>n = m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝² : Zero M<VAR>inst✝¹ : Zero N<VAR>inst✝ : Zero P<VAR>D : DecidableEq α<VAR>f : M → N → P<VAR>hf : f 0 0 = 0<VAR>g₁ : α →₀ M<VAR>g₂ : α →₀ N<GOAL>(zipWith f hf g₁ g₂).support ⊆ g₁.support ∪ g₂.support
<VAR>R : Type u<VAR>inst✝²⁶ : CommRing R<VAR>S : Type v<VAR>inst✝²⁵ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝²⁴ : Algebra R S<VAR>K : Type u_1<VAR>inst✝²³ : Field K<VAR>inst✝²² : Algebra R K<VAR>hRK : IsFractionRing R K<VAR>L : Type u_2<VAR>inst✝²¹ : Field L<VAR>inst✝²⁰ : Algebra S L<VAR>inst✝¹⁹ : IsFractionRing S L<VAR>V : Type u_3<VAR>V' : Type u_4<VAR>V'' : Type u_5<VAR>inst✝¹⁸ : AddCommGroup V<VAR>inst✝¹⁷ : Module R V<VAR>inst✝¹⁶ : Module K V<VAR>inst✝¹⁵ : IsScalarTower R K V<VAR>inst✝¹⁴ : AddCommGroup V'<VAR>inst✝¹³ : Module R V'<VAR>inst✝¹² : Module S V'<VAR>inst✝¹¹ : IsScalarTower R S V'<VAR>inst✝¹⁰ : AddCommGroup V''<VAR>inst✝⁹ : Module R V''<VAR>inst✝⁸ : IsDomain R<VAR>inst✝⁷ : IsDomain S<VAR>inst✝⁶ : Algebra K L<VAR>inst✝⁵ : IsNoetherian R S<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : IsScalarTower R S L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsIntegralClosure S R L<VAR>inst✝ : NoZeroSMulDivisors R K<VAR>hp : p ≠ ⊤<VAR>b : Set S<VAR>hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map (algebraMap R S) p) = ⊤<GOAL>Submodule.span K (⇑(algebraMap S L) '' b) = ⊤
<VAR>R : Type u<VAR>inst✝²⁶ : CommRing R<VAR>S : Type v<VAR>inst✝²⁵ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝²⁴ : Algebra R S<VAR>K : Type u_1<VAR>inst✝²³ : Field K<VAR>inst✝²² : Algebra R K<VAR>hRK : IsFractionRing R K<VAR>L : Type u_2<VAR>inst✝²¹ : Field L<VAR>inst✝²⁰ : Algebra S L<VAR>inst✝¹⁹ : IsFractionRing S L<VAR>V : Type u_3<VAR>V' : Type u_4<VAR>V'' : Type u_5<VAR>inst✝¹⁸ : AddCommGroup V<VAR>inst✝¹⁷ : Module R V<VAR>inst✝¹⁶ : Module K V<VAR>inst✝¹⁵ : IsScalarTower R K V<VAR>inst✝¹⁴ : AddCommGroup V'<VAR>inst✝¹³ : Module R V'<VAR>inst✝¹² : Module S V'<VAR>inst✝¹¹ : IsScalarTower R S V'<VAR>inst✝¹⁰ : AddCommGroup V''<VAR>inst✝⁹ : Module R V''<VAR>inst✝⁸ : IsDomain R<VAR>inst✝⁷ : IsDomain S<VAR>inst✝⁶ : Algebra K L<VAR>inst✝⁵ : IsNoetherian R S<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : IsScalarTower R S L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsIntegralClosure S R L<VAR>inst✝ : NoZeroSMulDivisors R K<VAR>hp : p ≠ ⊤<VAR>b : Set S<VAR>hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map (algebraMap R S) p) = ⊤<VAR>hRL : Function.Injective ⇑(algebraMap R L)<GOAL>Submodule.span K (⇑(algebraMap S L) '' b) = ⊤
<VAR>R : Type u<VAR>inst✝²⁶ : CommRing R<VAR>S : Type v<VAR>inst✝²⁵ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝²⁴ : Algebra R S<VAR>K : Type u_1<VAR>inst✝²³ : Field K<VAR>inst✝²² : Algebra R K<VAR>hRK : IsFractionRing R K<VAR>L : Type u_2<VAR>inst✝²¹ : Field L<VAR>inst✝²⁰ : Algebra S L<VAR>inst✝¹⁹ : IsFractionRing S L<VAR>V : Type u_3<VAR>V' : Type u_4<VAR>V'' : Type u_5<VAR>inst✝¹⁸ : AddCommGroup V<VAR>inst✝¹⁷ : Module R V<VAR>inst✝¹⁶ : Module K V<VAR>inst✝¹⁵ : IsScalarTower R K V<VAR>inst✝¹⁴ : AddCommGroup V'<VAR>inst✝¹³ : Module R V'<VAR>inst✝¹² : Module S V'<VAR>inst✝¹¹ : IsScalarTower R S V'<VAR>inst✝¹⁰ : AddCommGroup V''<VAR>inst✝⁹ : Module R V''<VAR>inst✝⁸ : IsDomain R<VAR>inst✝⁷ : IsDomain S<VAR>inst✝⁶ : Algebra K L<VAR>inst✝⁵ : IsNoetherian R S<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : IsScalarTower R S L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsIntegralClosure S R L<VAR>inst✝ : NoZeroSMulDivisors R K<VAR>hp : p ≠ ⊤<VAR>b : Set S<VAR>hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map (algebraMap R S) p) = ⊤<VAR>hRL : Function.Injective ⇑(algebraMap R L)<VAR>M : Submodule R S := Submodule.span R b<GOAL>Submodule.span K (⇑(algebraMap S L) '' b) = ⊤
<VAR>R : Type u<VAR>inst✝²⁶ : CommRing R<VAR>S : Type v<VAR>inst✝²⁵ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝²⁴ : Algebra R S<VAR>K : Type u_1<VAR>inst✝²³ : Field K<VAR>inst✝²² : Algebra R K<VAR>hRK : IsFractionRing R K<VAR>L : Type u_2<VAR>inst✝²¹ : Field L<VAR>inst✝²⁰ : Algebra S L<VAR>inst✝¹⁹ : IsFractionRing S L<VAR>V : Type u_3<VAR>V' : Type u_4<VAR>V'' : Type u_5<VAR>inst✝¹⁸ : AddCommGroup V<VAR>inst✝¹⁷ : Module R V<VAR>inst✝¹⁶ : Module K V<VAR>inst✝¹⁵ : IsScalarTower R K V<VAR>inst✝¹⁴ : AddCommGroup V'<VAR>inst✝¹³ : Module R V'<VAR>inst✝¹² : Module S V'<VAR>inst✝¹¹ : IsScalarTower R S V'<VAR>inst✝¹⁰ : AddCommGroup V''<VAR>inst✝⁹ : Module R V''<VAR>inst✝⁸ : IsDomain R<VAR>inst✝⁷ : IsDomain S<VAR>inst✝⁶ : Algebra K L<VAR>inst✝⁵ : IsNoetherian R S<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : IsScalarTower R S L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsIntegralClosure S R L<VAR>inst✝ : NoZeroSMulDivisors R K<VAR>hp : p ≠ ⊤<VAR>b : Set S<VAR>hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map (algebraMap R S) p) = ⊤<VAR>hRL : Function.Injective ⇑(algebraMap R L)<VAR>M : Submodule R S := Submodule.span R b<VAR>h : Module.Finite R (S ⧸ M) := Module.Finite.of_surjective M.mkQ (Submodule.Quotient.mk_surjective M)<GOAL>Submodule.span K (⇑(algebraMap S L) '' b) = ⊤
<VAR>R : Type u<VAR>inst✝²⁶ : CommRing R<VAR>S : Type v<VAR>inst✝²⁵ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝²⁴ : Algebra R S<VAR>K : Type u_1<VAR>inst✝²³ : Field K<VAR>inst✝²² : Algebra R K<VAR>hRK : IsFractionRing R K<VAR>L : Type u_2<VAR>inst✝²¹ : Field L<VAR>inst✝²⁰ : Algebra S L<VAR>inst✝¹⁹ : IsFractionRing S L<VAR>V : Type u_3<VAR>V' : Type u_4<VAR>V'' : Type u_5<VAR>inst✝¹⁸ : AddCommGroup V<VAR>inst✝¹⁷ : Module R V<VAR>inst✝¹⁶ : Module K V<VAR>inst✝¹⁵ : IsScalarTower R K V<VAR>inst✝¹⁴ : AddCommGroup V'<VAR>inst✝¹³ : Module R V'<VAR>inst✝¹² : Module S V'<VAR>inst✝¹¹ : IsScalarTower R S V'<VAR>inst✝¹⁰ : AddCommGroup V''<VAR>inst✝⁹ : Module R V''<VAR>inst✝⁸ : IsDomain R<VAR>inst✝⁷ : IsDomain S<VAR>inst✝⁶ : Algebra K L<VAR>inst✝⁵ : IsNoetherian R S<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : IsScalarTower R S L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsIntegralClosure S R L<VAR>inst✝ : NoZeroSMulDivisors R K<VAR>hp : p ≠ ⊤<VAR>b : Set S<VAR>hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map (algebraMap R S) p) = ⊤<VAR>hRL : Function.Injective ⇑(algebraMap R L)<VAR>M : Submodule R S := Submodule.span R b<VAR>h : Module.Finite R (S ⧸ M) := Module.Finite.of_surjective M.mkQ (Submodule.Quotient.mk_surjective M)<VAR>n : ℕ<VAR>a : Fin n → S ⧸ M<VAR>ha : Submodule.span R (Set.range a) = ⊤<GOAL>Submodule.span K (⇑(algebraMap S L) '' b) = ⊤