ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>s : AffineSubspace ℝ P<VAR>ps : Set P<VAR>h : ps ⊆ ↑s<VAR>inst✝¹ : Nonempty ↥s<VAR>n : ℕ<VAR>inst✝ : FiniteDimensional ℝ ↥s.direction<VAR>hd : finrank ℝ ↥s.direction = n<VAR>hc : Cospherical ps<VAR>sx₁ sx₂ : Simplex ℝ P n<VAR>hsx₁ : Set.range sx₁.points ⊆ ps<VAR>hsx₂ : Set.range sx₂.points ⊆ ps<GOAL>sx₁.circumcenter = sx₂.circumcenter
<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>s : AffineSubspace ℝ P<VAR>ps : Set P<VAR>h : ps ⊆ ↑s<VAR>inst✝¹ : Nonempty ↥s<VAR>n : ℕ<VAR>inst✝ : FiniteDimensional ℝ ↥s.direction<VAR>hd : finrank ℝ ↥s.direction = n<VAR>hc : Cospherical ps<VAR>sx₁ sx₂ : Simplex ℝ P n<VAR>hsx₁ : Set.range sx₁.points ⊆ ps<VAR>hsx₂ : Set.range sx₂.points ⊆ ps<VAR>r : P<VAR>hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = r<GOAL>sx₁.circumcenter = sx₂.circumcenter
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type u_3<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>f : AdicCauchySequence I M<VAR>k : ℕ<VAR>h : ∀ n ≥ k, ∃ m ≥ n, ∃ l ≥ n, ↑f m ∈ I ^ l • ⊤<VAR>n m : ℕ<VAR>hnm : m ≥ n + k<VAR>l : ℕ<VAR>hnl : l ≥ n + k<VAR>hl : ↑f m ∈ I ^ l • ⊤<GOAL>↑((mk I M) f) n = ↑0 n
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type u_3<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>f : AdicCauchySequence I M<VAR>k : ℕ<VAR>h : ∀ n ≥ k, ∃ m ≥ n, ∃ l ≥ n, ↑f m ∈ I ^ l • ⊤<VAR>n m : ℕ<VAR>hnm : m ≥ n + k<VAR>l : ℕ<VAR>hnl : l ≥ n + k<VAR>hl : ↑f m ∈ I ^ l • ⊤<GOAL>Submodule.Quotient.mk (↑f m) = 0
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : TopologicalSpace F<VAR>inst✝⁵ : TopologicalSpace B<VAR>e✝ : Pretrivialization F TotalSpace.proj<VAR>x : TotalSpace F E<VAR>b✝ : B<VAR>y : E b✝<VAR>inst✝⁴ : AddCommMonoid F<VAR>inst✝³ : Module R F<VAR>inst✝² : (x : B) → AddCommMonoid (E x)<VAR>inst✝¹ : (x : B) → Module R (E x)<VAR>e : Pretrivialization F TotalSpace.proj<VAR>inst✝ : Pretrivialization.IsLinear R e<VAR>b : B<VAR>hb : b ∈ e.baseSet<VAR>v : F<GOAL>{ toFun := fun y => (↑e { proj := b, snd := y }).2, map_add' := ⋯, map_smul' := ⋯ }.toFun (e.symm b v) = v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : Measure α<VAR>κ η : Kernel α β<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : IsSFiniteKernel κ<VAR>p : α × β → Prop<VAR>h : ∀ᵐ (x : α × β) ∂μ ⊗ₘ κ, p x<GOAL>∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂κ a, p (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>s✝ t : Set α<VAR>a b : α<VAR>s : Set α<VAR>h_sup : sSup s = ⊥<VAR>hne : s.Nonempty<GOAL>s = {⊥}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>s✝ t : Set α<VAR>a b : α<VAR>s : Set α<VAR>h_sup : sSup s = ⊥<VAR>hne : s.Nonempty<GOAL>s.Nonempty ∧ ∀ x ∈ s, x = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>s✝ t : Set α<VAR>a b : α<VAR>s : Set α<VAR>h_sup : ∀ a ∈ s, a = ⊥<VAR>hne : s.Nonempty<GOAL>s.Nonempty ∧ ∀ x ∈ s, x = ⊥
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>inst✝⁸ : FunLike F α β<VAR>inst✝⁷ : Sup α<VAR>inst✝⁶ : Bot α<VAR>inst✝⁵ : Sup β<VAR>inst✝⁴ : Bot β<VAR>inst✝³ : Sup γ<VAR>inst✝² : Bot γ<VAR>inst✝¹ : Sup δ<VAR>inst✝ : Bot δ<VAR>g : SupBotHom β γ<VAR>f₁ f₂ : SupBotHom α β<VAR>hg : Injective ⇑g<VAR>h : g.comp f₁ = g.comp f₂<VAR>a : α<GOAL>g (f₁ a) = g (f₂ a)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<GOAL>⁅I, J⁆ = ⁅J, I⁆
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<GOAL>∀ (I J : LieIdeal R L), ⁅I, J⁆ ≤ ⁅J, I⁆
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>N₂ : LieSubmodule R L M₂<VAR>I J : LieIdeal R L<GOAL>⁅I, J⁆ ≤ ⁅J, I⁆
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>N₂ : LieSubmodule R L M₂<VAR>I J : LieIdeal R L<GOAL>{m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑⁅J, I⁆
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>N₂ : LieSubmodule R L M₂<VAR>I J : LieIdeal R L<VAR>x : L<VAR>y : ↥I<VAR>z : ↥J<VAR>h : ⁅↑y, ↑z⁆ = x<GOAL>⁅↑y, ↑z⁆ ∈ ↑⁅J, I⁆
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>N₂ : LieSubmodule R L M₂<VAR>I J : LieIdeal R L<VAR>x : L<VAR>y : ↥I<VAR>z : ↥J<VAR>h : ⁅↑y, ↑z⁆ = x<GOAL>⁅↑z, ↑(-y)⁆ ∈ ↑⁅J, I⁆
<VAR>z : ↥circle<GOAL>↑z⁻¹ = (starRingEnd ℂ) ↑z
<VAR>i j : ℕ<GOAL>i.succ.dist j.succ = i.dist j
<VAR>c d : ℝ≥0∞<VAR>r p q a b : ℝ≥0<GOAL>(↑a).toReal = (↑b).toReal ↔ ↑a = ↑b
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<GOAL>l.rotate n = drop (n % l.length) l ++ take (n % l.length) l
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<VAR>hl : 0 = l.length<GOAL>l.rotate n = drop (n % l.length) l ++ take (n % l.length) l
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<VAR>hl : 0 < l.length<GOAL>l.rotate n = drop (n % l.length) l ++ take (n % l.length) l
<VAR>R : Type u_1<VAR>S : Type ?u.48975<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : LocalRing R<VAR>M : Type u_2<VAR>N✝ : Type ?u.49440<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup N✝<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N✝<VAR>P : Type ?u.50580<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>f : M →ₗ[R] N✝<VAR>g : N✝ →ₗ[R] P<VAR>hg : Surjective ⇑g<VAR>h : Exact ⇑f ⇑g<VAR>N : Submodule R M<VAR>inst✝ : Module.Finite R M<GOAL>Submodule.map (𝔪 • ⊤).mkQ N = ⊤ ↔ N = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝¹ : Ring R<VAR>inst✝ : SetLike S R<VAR>hSR : SubringClass S R<VAR>s : S<VAR>n : ℤ<GOAL>↑n ∈ s
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : CharZero R<VAR>p : R[X]<VAR>t : R<VAR>hpt : p.IsRoot t<VAR>h : ¬p = 0<GOAL>rootMultiplicity t (derivative p) = rootMultiplicity t p - 1
<VAR>n✝ n : ℕ<GOAL>∏ x ∈ Icc 1 (n + 1), x ! = sf n + 1
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>inst✝⁵ : CommSemiring k<VAR>inst✝⁴ : Group G<VAR>inst✝³ : AddCommMonoid V<VAR>inst✝² : Module k V<VAR>ρ : Representation k G V<VAR>inst✝¹ : Fintype G<VAR>inst✝ : Invertible ↑(Fintype.card G)<VAR>v : V<VAR>g : G<GOAL>(ρ g) (ρ.averageMap v) = ρ.averageMap v
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : LinearOrder β<VAR>U : Filter (α × α)<VAR>z : β<VAR>D : α → α → β<VAR>H : ∀ (s : Set (α × α)), s ∈ U ↔ ∃ ε > z, ∀ {a b : α}, D a b < ε → (a, b) ∈ s<VAR>s : Set (α × α)<GOAL>s ∈ U ↔ ∃ i > z, {p | D p.1 p.2 < i} ⊆ s
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n✝ : ℕ<VAR>M : Fin n✝.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : (i : Fin n✝.succ) → AddCommMonoid (M i)<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : (i : Fin n✝.succ) → Module R (M i)<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M₂<VAR>ι' : Type u_1<VAR>k l n : ℕ<VAR>s : Finset (Fin n)<VAR>hk : s.card = k<VAR>hl : sᶜ.card = l<VAR>f : MultilinearMap R (fun x => M') M₂<VAR>x y : M'<GOAL>(f fun i => Sum.elim (fun x_1 => x) (fun x => y) ((finSumEquivOfFinset hk hl).symm i)) = f (s.piecewise (fun x_1 => x) fun x => y)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n✝ : ℕ<VAR>M : Fin n✝.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : (i : Fin n✝.succ) → AddCommMonoid (M i)<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : (i : Fin n✝.succ) → Module R (M i)<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M₂<VAR>ι' : Type u_1<VAR>k l n : ℕ<VAR>s : Finset (Fin n)<VAR>hk : s.card = k<VAR>hl : sᶜ.card = l<VAR>f : MultilinearMap R (fun x => M') M₂<VAR>x y : M'<GOAL>((((curryFinFinset R M₂ M' hk hl) f) fun x_1 => x) fun x => y) = f (s.piecewise (fun x_1 => x) fun x => y)
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring S<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R S A<VAR>s✝ t s : Set A<GOAL>adjoin R (Subtype.val ⁻¹' s) = ⊤
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring S<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R S A<VAR>s✝ t s : Set A<VAR>x : { x // x ∈ ↑(adjoin R s) }<VAR>a : A<VAR>ha : a ∈ s<GOAL>⟨a, ⋯⟩ ∈ adjoin R (Subtype.val ⁻¹' s)
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring S<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R S A<VAR>s✝ t s : Set A<VAR>x : { x // x ∈ ↑(adjoin R s) }<VAR>r : R<GOAL>(algebraMap R ↥(adjoin R s)) r ∈ adjoin R (Subtype.val ⁻¹' s)
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring S<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R S A<VAR>s✝ t s : Set A<VAR>x : { x // x ∈ ↑(adjoin R s) }<VAR>x✝¹ x✝ : ↥(adjoin R s)<GOAL>x✝¹ ∈ adjoin R (Subtype.val ⁻¹' s) → x✝ ∈ adjoin R (Subtype.val ⁻¹' s) → x✝¹ + x✝ ∈ adjoin R (Subtype.val ⁻¹' s)
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring S<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R S A<VAR>s✝ t s : Set A<VAR>x : { x // x ∈ ↑(adjoin R s) }<VAR>x✝¹ x✝ : ↥(adjoin R s)<GOAL>x✝¹ ∈ adjoin R (Subtype.val ⁻¹' s) → x✝ ∈ adjoin R (Subtype.val ⁻¹' s) → x✝¹ * x✝ ∈ adjoin R (Subtype.val ⁻¹' s)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>β : Type u_2<VAR>inst✝⁶ : CompleteLinearOrder β<VAR>inst✝⁵ : DenselyOrdered β<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : OrderTopology β<VAR>inst✝² : SecondCountableTopology β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : BorelSpace β<VAR>s : Set β<VAR>s_count : s.Countable<VAR>s_dense : Dense s<VAR>f : α → β<VAR>h : ∀ p ∈ s, ∀ q ∈ s, p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ μ (u ∩ v) = 0<VAR>this : Encodable ↑s<VAR>u v : β → β → Set α<VAR>huv : ∀ (p q : β), MeasurableSet (u p q) ∧ MeasurableSet (v p q) ∧ {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → μ (u p q ∩ v p q) = 0)<VAR>u' : β → Set α := fun p => ⋂ q ∈ s ∩ Ioi p, u p q<GOAL>AEMeasurable f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>β : Type u_2<VAR>inst✝⁶ : CompleteLinearOrder β<VAR>inst✝⁵ : DenselyOrdered β<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : OrderTopology β<VAR>inst✝² : SecondCountableTopology β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : BorelSpace β<VAR>s : Set β<VAR>s_count : s.Countable<VAR>s_dense : Dense s<VAR>f : α → β<VAR>h : ∀ p ∈ s, ∀ q ∈ s, p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ μ (u ∩ v) = 0<VAR>this : Encodable ↑s<VAR>u v : β → β → Set α<VAR>huv : ∀ (p q : β), MeasurableSet (u p q) ∧ MeasurableSet (v p q) ∧ {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → μ (u p q ∩ v p q) = 0)<VAR>u' : β → Set α := fun p => ⋂ q ∈ s ∩ Ioi p, u p q<VAR>u'_meas : ∀ (i : β), MeasurableSet (u' i)<GOAL>AEMeasurable f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>β : Type u_2<VAR>inst✝⁶ : CompleteLinearOrder β<VAR>inst✝⁵ : DenselyOrdered β<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : OrderTopology β<VAR>inst✝² : SecondCountableTopology β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : BorelSpace β<VAR>s : Set β<VAR>s_count : s.Countable<VAR>s_dense : Dense s<VAR>f : α → β<VAR>h : ∀ p ∈ s, ∀ q ∈ s, p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ μ (u ∩ v) = 0<VAR>this : Encodable ↑s<VAR>u v : β → β → Set α<VAR>huv : ∀ (p q : β), MeasurableSet (u p q) ∧ MeasurableSet (v p q) ∧ {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → μ (u p q ∩ v p q) = 0)<VAR>u' : β → Set α := fun p => ⋂ q ∈ s ∩ Ioi p, u p q<VAR>u'_meas : ∀ (i : β), MeasurableSet (u' i)<VAR>f' : α → β := fun x => ⨅ i, (u' ↑i).piecewise (fun x => ↑i) (fun x => ⊤) x<GOAL>AEMeasurable f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>β : Type u_2<VAR>inst✝⁶ : CompleteLinearOrder β<VAR>inst✝⁵ : DenselyOrdered β<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : OrderTopology β<VAR>inst✝² : SecondCountableTopology β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : BorelSpace β<VAR>s : Set β<VAR>s_count : s.Countable<VAR>s_dense : Dense s<VAR>f : α → β<VAR>h : ∀ p ∈ s, ∀ q ∈ s, p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ μ (u ∩ v) = 0<VAR>this : Encodable ↑s<VAR>u v : β → β → Set α<VAR>huv : ∀ (p q : β), MeasurableSet (u p q) ∧ MeasurableSet (v p q) ∧ {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → μ (u p q ∩ v p q) = 0)<VAR>u' : β → Set α := fun p => ⋂ q ∈ s ∩ Ioi p, u p q<VAR>u'_meas : ∀ (i : β), MeasurableSet (u' i)<VAR>f' : α → β := fun x => ⨅ i, (u' ↑i).piecewise (fun x => ↑i) (fun x => ⊤) x<VAR>f'_meas : Measurable f'<GOAL>AEMeasurable f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>β : Type u_2<VAR>inst✝⁶ : CompleteLinearOrder β<VAR>inst✝⁵ : DenselyOrdered β<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : OrderTopology β<VAR>inst✝² : SecondCountableTopology β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : BorelSpace β<VAR>s : Set β<VAR>s_count : s.Countable<VAR>s_dense : Dense s<VAR>f : α → β<VAR>h : ∀ p ∈ s, ∀ q ∈ s, p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ μ (u ∩ v) = 0<VAR>this : Encodable ↑s<VAR>u v : β → β → Set α<VAR>huv : ∀ (p q : β), MeasurableSet (u p q) ∧ MeasurableSet (v p q) ∧ {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → μ (u p q ∩ v p q) = 0)<VAR>u' : β → Set α := fun p => ⋂ q ∈ s ∩ Ioi p, u p q<VAR>u'_meas : ∀ (i : β), MeasurableSet (u' i)<VAR>f' : α → β := fun x => ⨅ i, (u' ↑i).piecewise (fun x => ↑i) (fun x => ⊤) x<VAR>f'_meas : Measurable f'<VAR>t : Set α := ⋃ p, ⋃ q, u' ↑p ∩ v ↑p ↑q<GOAL>AEMeasurable f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>β : Type u_2<VAR>inst✝⁶ : CompleteLinearOrder β<VAR>inst✝⁵ : DenselyOrdered β<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : OrderTopology β<VAR>inst✝² : SecondCountableTopology β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : BorelSpace β<VAR>s : Set β<VAR>s_count : s.Countable<VAR>s_dense : Dense s<VAR>f : α → β<VAR>h : ∀ p ∈ s, ∀ q ∈ s, p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ μ (u ∩ v) = 0<VAR>this : Encodable ↑s<VAR>u v : β → β → Set α<VAR>huv : ∀ (p q : β), MeasurableSet (u p q) ∧ MeasurableSet (v p q) ∧ {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → μ (u p q ∩ v p q) = 0)<VAR>u' : β → Set α := fun p => ⋂ q ∈ s ∩ Ioi p, u p q<VAR>u'_meas : ∀ (i : β), MeasurableSet (u' i)<VAR>f' : α → β := fun x => ⨅ i, (u' ↑i).piecewise (fun x => ↑i) (fun x => ⊤) x<VAR>f'_meas : Measurable f'<VAR>t : Set α := ⋃ p, ⋃ q, u' ↑p ∩ v ↑p ↑q<VAR>μt : μ t ≤ 0<GOAL>AEMeasurable f μ
<VAR>R : Type u_1<VAR>A✝ : Type u_2<VAR>B : Type u_3<VAR>A : Type u_4<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Semiring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f g : A[ε] →ₐ[R] B<VAR>hinl : f.comp (inlAlgHom R A A) = g.comp (inlAlgHom R A A)<VAR>hinr : f.toLinearMap ∘ₗ ↑R (LinearMap.toSpanSingleton A A[ε] ε) = g.toLinearMap ∘ₗ ↑R (LinearMap.toSpanSingleton A A[ε] ε)<VAR>a : A<GOAL>f (inr a) = g (inr a)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a✝ b : R<VAR>n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>a : R<VAR>n : ℕ<GOAL>derivative ((monomial n) a) = (monomial (n - 1)) (a * ↑n)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a✝ b : R<VAR>n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>a : R<VAR>n : ℕ<GOAL>C (0 * ↑n) * X ^ (n - 1) = 0
<VAR>c : Code<VAR>h : c.Ok<VAR>v : List ℕ<GOAL>Turing.eval step (stepNormal c Cont.halt v) = Cfg.halt <$> c.eval v
<VAR>c : Code<VAR>h : c.Ok<VAR>v : List ℕ<GOAL>(do let v ← c.eval v Turing.eval step (Cfg.ret Cont.halt v)) = do let a ← c.eval v pure (Cfg.halt a)
<VAR>c : Code<VAR>h : c.Ok<VAR>v : List ℕ<GOAL>(fun v => Turing.eval step (Cfg.ret Cont.halt v)) = fun a => pure (Cfg.halt a)
<VAR>c : Code<VAR>h : c.Ok<VAR>v✝ v : List ℕ<GOAL>Turing.eval step (Cfg.ret Cont.halt v) = pure (Cfg.halt v)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>φ : M → N<VAR>ψ : N → P<VAR>χ : M → P<VAR>h : CompTriple φ ψ χ<VAR>x : M<GOAL>ψ (φ x) = χ x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>x₁ x₂ : ↑↑(Proj.restrict ⋯).toPresheafedSpace<VAR>h : (toSpec 𝒜 f) x₁ = (toSpec 𝒜 f) x₂<VAR>this : FromSpec.toFun f_deg hm ((toSpec 𝒜 f) x₁) = FromSpec.toFun f_deg hm ((toSpec 𝒜 f) x₂)<GOAL>x₁ = x₂
<VAR>α : Type u_1<VAR>M✝ M : Matroid α<VAR>hE : M.E.Finite<GOAL>M ∈ {M_1 | M_1.E ⊆ M.E}
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>s : Set (α × α)<VAR>e : α → β<VAR>b : β<VAR>he₁ : UniformInducing e<VAR>he₂ : DenseInducing e<VAR>hs : s ∈ 𝓤 α<GOAL>∃ a, closure (e '' {a' | (a, a') ∈ s}) ∈ 𝓝 b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>s : Set (α × α)<VAR>e : α → β<VAR>b : β<VAR>he₁ : UniformInducing e<VAR>he₂ : DenseInducing e<VAR>hs✝ : s ∈ 𝓤 α<VAR>U : Set (β × β)<VAR>hs : Prod.map e e ⁻¹' U ⊆ s<VAR>hU : U ∈ 𝓤 β<VAR>hUo : IsOpen U<VAR>hsymm : SymmetricRel U<GOAL>∃ a, closure (e '' {a' | (a, a') ∈ s}) ∈ 𝓝 b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>s : Set (α × α)<VAR>e : α → β<VAR>b : β<VAR>he₁ : UniformInducing e<VAR>he₂ : DenseInducing e<VAR>hs✝ : s ∈ 𝓤 α<VAR>U : Set (β × β)<VAR>hs : Prod.map e e ⁻¹' U ⊆ s<VAR>hU : U ∈ 𝓤 β<VAR>hUo : IsOpen U<VAR>hsymm : SymmetricRel U<VAR>a : α<VAR>ha : e a ∈ UniformSpace.ball b U<GOAL>∃ a, closure (e '' {a' | (a, a') ∈ s}) ∈ 𝓝 b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>s : Set (α × α)<VAR>e : α → β<VAR>b : β<VAR>he₁ : UniformInducing e<VAR>he₂ : DenseInducing e<VAR>hs✝ : s ∈ 𝓤 α<VAR>U : Set (β × β)<VAR>hs : Prod.map e e ⁻¹' U ⊆ s<VAR>hU : U ∈ 𝓤 β<VAR>hUo : IsOpen U<VAR>hsymm : SymmetricRel U<VAR>a : α<VAR>ha : e a ∈ UniformSpace.ball b U<GOAL>closure (e '' UniformSpace.ball a (Prod.map e e ⁻¹' U)) ∈ 𝓝 b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>s : Set (α × α)<VAR>e : α → β<VAR>b : β<VAR>he₁ : UniformInducing e<VAR>he₂ : DenseInducing e<VAR>hs✝ : s ∈ 𝓤 α<VAR>U : Set (β × β)<VAR>hs : Prod.map e e ⁻¹' U ⊆ s<VAR>hU : U ∈ 𝓤 β<VAR>hUo : IsOpen U<VAR>hsymm : SymmetricRel U<VAR>a : α<VAR>ha : e a ∈ UniformSpace.ball b U<VAR>ho : IsOpen (UniformSpace.ball (e a) U)<GOAL>closure (e '' UniformSpace.ball a (Prod.map e e ⁻¹' U)) ∈ 𝓝 b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>s : Set (α × α)<VAR>e : α → β<VAR>b : β<VAR>he₁ : UniformInducing e<VAR>he₂ : DenseInducing e<VAR>hs✝ : s ∈ 𝓤 α<VAR>U : Set (β × β)<VAR>hs : Prod.map e e ⁻¹' U ⊆ s<VAR>hU : U ∈ 𝓤 β<VAR>hUo : IsOpen U<VAR>hsymm : SymmetricRel U<VAR>a : α<VAR>ha : e a ∈ UniformSpace.ball b U<VAR>ho : IsOpen (UniformSpace.ball (e a) U)<VAR>y : β<VAR>hy : y ∈ UniformSpace.ball (e a) U<GOAL>y ∈ closure (e '' UniformSpace.ball a (Prod.map e e ⁻¹' U))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>s : Set (α × α)<VAR>e : α → β<VAR>b : β<VAR>he₁ : UniformInducing e<VAR>he₂ : DenseInducing e<VAR>hs✝ : s ∈ 𝓤 α<VAR>U : Set (β × β)<VAR>hs : Prod.map e e ⁻¹' U ⊆ s<VAR>hU : U ∈ 𝓤 β<VAR>hUo : IsOpen U<VAR>hsymm : SymmetricRel U<VAR>a : α<VAR>ha : e a ∈ UniformSpace.ball b U<VAR>ho : IsOpen (UniformSpace.ball (e a) U)<VAR>y : β<VAR>hy : y ∈ UniformSpace.ball (e a) U<VAR>V : Set β<VAR>hV : V ∈ 𝓝 y<GOAL>(V ∩ e '' UniformSpace.ball a (Prod.map e e ⁻¹' U)).Nonempty
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>s : Set (α × α)<VAR>e : α → β<VAR>b : β<VAR>he₁ : UniformInducing e<VAR>he₂ : DenseInducing e<VAR>hs✝ : s ∈ 𝓤 α<VAR>U : Set (β × β)<VAR>hs : Prod.map e e ⁻¹' U ⊆ s<VAR>hU : U ∈ 𝓤 β<VAR>hUo : IsOpen U<VAR>hsymm : SymmetricRel U<VAR>a : α<VAR>ha : e a ∈ UniformSpace.ball b U<VAR>ho : IsOpen (UniformSpace.ball (e a) U)<VAR>y : β<VAR>hy : y ∈ UniformSpace.ball (e a) U<VAR>V : Set β<VAR>hV : V ∈ 𝓝 y<VAR>x : α<VAR>hxV : e x ∈ V<VAR>hxU : e x ∈ UniformSpace.ball (e a) U<GOAL>(V ∩ e '' UniformSpace.ball a (Prod.map e e ⁻¹' U)).Nonempty
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>v : V<VAR>inst✝¹ : Fintype ↑(G.neighborSet v)<VAR>inst✝ : DecidableEq V<GOAL>(G.incidenceFinset v).card = G.degree v