ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β✝<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>β : Type u_5<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : T1Space β<VAR>inst✝¹ : SecondCountableTopology β<VAR>inst✝ : Nonempty β<VAR>f : α → β<VAR>m : OuterMeasure β := (OuterMeasure.map f) μ.toOuterMeasure<VAR>h : ∀ (b : β), m {b}ᶜ ≠ 0<GOAL>∃ a b, a ≠ b ∧ (∀ s ∈ 𝓝 a, 0 < μ (f ⁻¹' s)) ∧ ∀ t ∈ 𝓝 b, 0 < μ (f ⁻¹' t)
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β✝<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>β : Type u_5<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : T1Space β<VAR>inst✝¹ : SecondCountableTopology β<VAR>inst✝ : Nonempty β<VAR>f : α → β<VAR>m : OuterMeasure β := (OuterMeasure.map f) μ.toOuterMeasure<VAR>h : ∀ (b : β), m {b}ᶜ ≠ 0<VAR>inhabited_h : Inhabited β<GOAL>∃ a b, a ≠ b ∧ (∀ s ∈ 𝓝 a, 0 < μ (f ⁻¹' s)) ∧ ∀ t ∈ 𝓝 b, 0 < μ (f ⁻¹' t)
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β✝<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>β : Type u_5<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : T1Space β<VAR>inst✝¹ : SecondCountableTopology β<VAR>inst✝ : Nonempty β<VAR>f : α → β<VAR>m : OuterMeasure β := (OuterMeasure.map f) μ.toOuterMeasure<VAR>h : ∀ (b : β), m {b}ᶜ ≠ 0<VAR>inhabited_h : Inhabited β<VAR>this : m univ ≠ 0<GOAL>∃ a b, a ≠ b ∧ (∀ s ∈ 𝓝 a, 0 < μ (f ⁻¹' s)) ∧ ∀ t ∈ 𝓝 b, 0 < μ (f ⁻¹' t)
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β✝<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>β : Type u_5<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : T1Space β<VAR>inst✝¹ : SecondCountableTopology β<VAR>inst✝ : Nonempty β<VAR>f : α → β<VAR>m : OuterMeasure β := (OuterMeasure.map f) μ.toOuterMeasure<VAR>h : ∀ (b : β), m {b}ᶜ ≠ 0<VAR>inhabited_h : Inhabited β<VAR>this : m univ ≠ 0<VAR>b : β<VAR>hb : ∀ t ∈ 𝓝[univ] b, 0 < m t<GOAL>∃ a b, a ≠ b ∧ (∀ s ∈ 𝓝 a, 0 < μ (f ⁻¹' s)) ∧ ∀ t ∈ 𝓝 b, 0 < μ (f ⁻¹' t)
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β✝<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>β : Type u_5<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : T1Space β<VAR>inst✝¹ : SecondCountableTopology β<VAR>inst✝ : Nonempty β<VAR>f : α → β<VAR>m : OuterMeasure β := (OuterMeasure.map f) μ.toOuterMeasure<VAR>h : ∀ (b : β), m {b}ᶜ ≠ 0<VAR>inhabited_h : Inhabited β<VAR>this : m univ ≠ 0<VAR>b : β<VAR>hb : ∀ t ∈ 𝓝 b, 0 < m t<GOAL>∃ a b, a ≠ b ∧ (∀ s ∈ 𝓝 a, 0 < μ (f ⁻¹' s)) ∧ ∀ t ∈ 𝓝 b, 0 < μ (f ⁻¹' t)
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β✝<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>β : Type u_5<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : T1Space β<VAR>inst✝¹ : SecondCountableTopology β<VAR>inst✝ : Nonempty β<VAR>f : α → β<VAR>m : OuterMeasure β := (OuterMeasure.map f) μ.toOuterMeasure<VAR>h : ∀ (b : β), m {b}ᶜ ≠ 0<VAR>inhabited_h : Inhabited β<VAR>this : m univ ≠ 0<VAR>b : β<VAR>hb : ∀ t ∈ 𝓝 b, 0 < m t<VAR>a : β<VAR>hab : a ≠ b<VAR>ha : ∀ t ∈ 𝓝[{b}ᶜ] a, 0 < m t<GOAL>∃ a b, a ≠ b ∧ (∀ s ∈ 𝓝 a, 0 < μ (f ⁻¹' s)) ∧ ∀ t ∈ 𝓝 b, 0 < μ (f ⁻¹' t)
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β✝<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>β : Type u_5<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : T1Space β<VAR>inst✝¹ : SecondCountableTopology β<VAR>inst✝ : Nonempty β<VAR>f : α → β<VAR>m : OuterMeasure β := (OuterMeasure.map f) μ.toOuterMeasure<VAR>h : ∀ (b : β), m {b}ᶜ ≠ 0<VAR>inhabited_h : Inhabited β<VAR>this : m univ ≠ 0<VAR>b : β<VAR>hb : ∀ t ∈ 𝓝 b, 0 < m t<VAR>a : β<VAR>hab : a ≠ b<VAR>ha : ∀ t ∈ 𝓝 a, 0 < m t<GOAL>∃ a b, a ≠ b ∧ (∀ s ∈ 𝓝 a, 0 < μ (f ⁻¹' s)) ∧ ∀ t ∈ 𝓝 b, 0 < μ (f ⁻¹' t)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w₁ w₂ z₁ z₂ : ℝ≥0∞<VAR>hw' : w₁ + w₂ = 1<VAR>p : ℝ<VAR>hp : 1 ≤ p<GOAL>(w₁ * z₁ + w₂ * z₂) ^ p ≤ w₁ * z₁ ^ p + w₂ * z₂ ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w₁ w₂ z₁ z₂ : ℝ≥0∞<VAR>hw' : w₁ + w₂ = 1<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>h : (∑ i : Fin (Nat.succ 0).succ, ![w₁, w₂] i * ![z₁, z₂] i) ^ p ≤ ∑ i : Fin (Nat.succ 0).succ, ![w₁, w₂] i * ![z₁, z₂] i ^ p<GOAL>(w₁ * z₁ + w₂ * z₂) ^ p ≤ w₁ * z₁ ^ p + w₂ * z₂ ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w₁ w₂ z₁ z₂ : ℝ≥0∞<VAR>hw' : w₁ + w₂ = 1<VAR>p : ℝ<VAR>hp : 1 ≤ p<GOAL>∑ i : Fin (Nat.succ 0).succ, ![w₁, w₂] i = 1
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Monoid (G i)<VAR>inst✝ : Monoid H<VAR>φ : (i : ι) → H →* G i<VAR>i : ι<VAR>x : H<GOAL>((of i).comp (φ i)) x = (base φ) x
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Monoid (G i)<VAR>inst✝ : Monoid H<VAR>φ : (i : ι) → H →* G i<VAR>i : ι<VAR>x : H<GOAL>(con φ) ((inl.comp CoprodI.of) ((φ i) x)) (inr x)
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Monoid (G i)<VAR>inst✝ : Monoid H<VAR>φ : (i : ι) → H →* G i<VAR>i : ι<VAR>x : H<GOAL>∃ i_1 x', (inl.comp CoprodI.of) ((φ i) x) = inl (CoprodI.of ((φ i_1) x')) ∧ inr x = inr x'
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Monoid (G i)<VAR>inst✝ : Monoid H<VAR>φ : (i : ι) → H →* G i<VAR>i : ι<VAR>x : H<GOAL>∃ i_1 x', inl (CoprodI.of ((φ i) x)) = inl (CoprodI.of ((φ i_1) x')) ∧ inr x = inr x'
<VAR>x : ℂ<GOAL>cos (x + ↑π / 2) = -sin x
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>inst✝⁴ : Abelian C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : Abelian D<VAR>F : C ⥤ D<VAR>inst✝¹ : F.PreservesZeroMorphisms<VAR>inst✝ : F.Faithful<VAR>S : ShortComplex C<VAR>hS : (S.map F).Exact<GOAL>S.Exact
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>inst✝⁴ : Abelian C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : Abelian D<VAR>F : C ⥤ D<VAR>inst✝¹ : F.PreservesZeroMorphisms<VAR>inst✝ : F.Faithful<VAR>S : ShortComplex C<VAR>hS : kernel.ι (S.map F).g ≫ cokernel.π (S.map F).f = 0<GOAL>kernel.ι S.g ≫ cokernel.π S.f = 0
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>inst✝⁴ : Abelian C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : Abelian D<VAR>F : C ⥤ D<VAR>inst✝¹ : F.PreservesZeroMorphisms<VAR>inst✝ : F.Faithful<VAR>S : ShortComplex C<VAR>hS : kernel.ι (F.map S.g) ≫ cokernel.π (F.map S.f) = 0<GOAL>kernel.ι S.g ≫ cokernel.π S.f = 0
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>inst✝⁴ : Abelian C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : Abelian D<VAR>F : C ⥤ D<VAR>inst✝¹ : F.PreservesZeroMorphisms<VAR>inst✝ : F.Faithful<VAR>S : ShortComplex C<VAR>hS : kernel.ι (F.map S.g) ≫ cokernel.π (F.map S.f) = 0<GOAL>F.map (kernel.ι S.g ≫ cokernel.π S.f) = 0
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>inst✝⁴ : Abelian C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : Abelian D<VAR>F : C ⥤ D<VAR>inst✝¹ : F.PreservesZeroMorphisms<VAR>inst✝ : F.Faithful<VAR>S : ShortComplex C<VAR>hS : kernel.ι (F.map S.g) ≫ cokernel.π (F.map S.f) = 0<VAR>k : F.obj (kernel S.g) ⟶ kernel (F.map S.g)<VAR>hk : k ≫ kernel.ι (F.map S.g) = F.map (kernel.ι S.g)<GOAL>F.map (kernel.ι S.g ≫ cokernel.π S.f) = 0
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>inst✝⁴ : Abelian C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : Abelian D<VAR>F : C ⥤ D<VAR>inst✝¹ : F.PreservesZeroMorphisms<VAR>inst✝ : F.Faithful<VAR>S : ShortComplex C<VAR>hS : kernel.ι (F.map S.g) ≫ cokernel.π (F.map S.f) = 0<VAR>k : F.obj (kernel S.g) ⟶ kernel (F.map S.g)<VAR>hk : k ≫ kernel.ι (F.map S.g) = F.map (kernel.ι S.g)<VAR>l : cokernel (F.map S.f) ⟶ F.obj (cokernel S.f)<VAR>hl : cokernel.π (F.map S.f) ≫ l = F.map (cokernel.π S.f)<GOAL>F.map (kernel.ι S.g ≫ cokernel.π S.f) = 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a : α<VAR>n : ℕ<GOAL>⌈a + ↑n⌉ = ⌈a⌉ + ↑n
<VAR>α : Type u_1<VAR>inst✝² : Preorder α<VAR>inst✝¹ : IsTotal α fun x x_1 => x ≤ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>x : α<VAR>t : Ordnode α<VAR>h : t.Valid<GOAL>(Ordnode.insert x t).Valid
<VAR>α : Type u_1<VAR>inst✝² : Preorder α<VAR>inst✝¹ : IsTotal α fun x x_1 => x ≤ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>x : α<VAR>t : Ordnode α<VAR>h : t.Valid<GOAL>(insertWith (fun x_1 => x) x t).Valid
<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>inst✝¹ : Nonempty ↥s<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>p : P<VAR>hp : p ∈ s<VAR>v : V<VAR>hv : v ∈ s.directionᗮ<GOAL>(orthogonalProjection s) (v +ᵥ p) = ⟨p, hp⟩
<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>inst✝¹ : Nonempty ↥s<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>p : P<VAR>hp : p ∈ s<VAR>v : V<VAR>hv : v ∈ s.directionᗮ<VAR>h : v +ᵥ p -ᵥ ↑((orthogonalProjection s) (v +ᵥ p)) ∈ s.directionᗮ<GOAL>(orthogonalProjection s) (v +ᵥ p) = ⟨p, hp⟩
<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>inst✝¹ : Nonempty ↥s<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>p : P<VAR>hp : p ∈ s<VAR>v : V<VAR>hv : v ∈ s.directionᗮ<VAR>h : p -ᵥ ↑((orthogonalProjection s) (v +ᵥ p)) ∈ s.directionᗮ<GOAL>(orthogonalProjection s) (v +ᵥ p) = ⟨p, hp⟩
<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>inst✝¹ : Nonempty ↥s<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>p : P<VAR>hp : p ∈ s<VAR>v : V<VAR>hv : v ∈ s.directionᗮ<VAR>h : p -ᵥ ↑((orthogonalProjection s) (v +ᵥ p)) ∈ s.directionᗮ<GOAL>⟨p, hp⟩ -ᵥ (orthogonalProjection s) (v +ᵥ p) = 0
<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>inst✝¹ : Nonempty ↥s<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>p : P<VAR>hp : p ∈ s<VAR>v : V<VAR>hv : v ∈ s.directionᗮ<VAR>h : p -ᵥ ↑((orthogonalProjection s) (v +ᵥ p)) ∈ s.directionᗮ<GOAL>↑(⟨p, hp⟩ -ᵥ (orthogonalProjection s) (v +ᵥ p)) = ↑0
<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>inst✝¹ : Nonempty ↥s<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>p : P<VAR>hp : p ∈ s<VAR>v : V<VAR>hv : v ∈ s.directionᗮ<VAR>h : p -ᵥ ↑((orthogonalProjection s) (v +ᵥ p)) ∈ s.directionᗮ<GOAL>↑(⟨p, hp⟩ -ᵥ (orthogonalProjection s) (v +ᵥ p)) ∈ s.direction
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>A : Type u_3<VAR>B : 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>inst✝² : One M<VAR>inst✝¹ : One N<VAR>inst✝ : One P<VAR>f : α → M<VAR>s : Set α<GOAL>Disjoint s (mulSupport f) ↔ EqOn f 1 s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : α<VAR>ts : List α<VAR>r L : List (List α)<VAR>l' : List α<VAR>this : (∃ a, a ∈ L ∧ ∃ l₁ l₂, ¬l₂ = [] ∧ a = l₁ ++ l₂ ∧ l' = l₁ ++ t :: (l₂ ++ ts)) ↔ ∃ l₁ l₂, ¬l₂ = [] ∧ l₁ ++ l₂ ∈ L ∧ l' = l₁ ++ t :: (l₂ ++ ts)<GOAL>l' ∈ foldr (fun y r => (permutationsAux2 t ts r y id).2) r L ↔ l' ∈ r ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ L ∧ l₂ ≠ [] ∧ l' = l₁ ++ t :: l₂ ++ ts
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : α<VAR>ts : List α<VAR>r L : List (List α)<VAR>l' : List α<VAR>this : (∃ a, a ∈ L ∧ ∃ l₁ l₂, ¬l₂ = [] ∧ a = l₁ ++ l₂ ∧ l' = l₁ ++ t :: (l₂ ++ ts)) ↔ ∃ l₁ l₂, ¬l₂ = [] ∧ l₁ ++ l₂ ∈ L ∧ l' = l₁ ++ t :: (l₂ ++ ts)<GOAL>l' ∈ (L.bind fun y => (permutationsAux2 t ts [] y id).2) ++ r ↔ l' ∈ r ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ L ∧ l₂ ≠ [] ∧ l' = l₁ ++ t :: l₂ ++ ts
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝ : TopologicalSpace X<VAR>s t : Set X<GOAL>SeparatedNhds s t ↔ Disjoint (𝓝ˢ s) (𝓝ˢ t)
<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>f g : F[X]<VAR>q : ℕ<VAR>inst✝ : ExpChar F q<VAR>h1 : g.Separable<VAR>m : ℕ<VAR>h2 : (expand F (q ^ m)) g = f<GOAL>f.natSepDegree = g.natDegree
<VAR>F : Type u_1<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>inst✝ : CompleteSpace F<VAR>this✝¹ : MeasurableSpace F := borel F<VAR>this✝ : BorelSpace F<GOAL>StronglyMeasurable fun x => derivWithin f (Ici x) x
<VAR>F : Type u_1<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>inst✝ : CompleteSpace F<VAR>this✝¹ : MeasurableSpace F := borel F<VAR>this✝ : BorelSpace F<GOAL>IsSeparable (range fun x => derivWithin f (Ici x) x)
<VAR>F : Type u_1<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>inst✝ : CompleteSpace F<VAR>this✝¹ : MeasurableSpace F := borel F<VAR>this✝ : BorelSpace F<VAR>t : Set ℝ<VAR>t_count : t.Countable<VAR>ht : Dense t<GOAL>IsSeparable (range fun x => derivWithin f (Ici x) x)
<VAR>F : Type u_1<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>inst✝ : CompleteSpace F<VAR>this✝¹ : MeasurableSpace F := borel F<VAR>this✝ : BorelSpace F<VAR>t : Set ℝ<VAR>t_count : t.Countable<VAR>ht : Dense t<GOAL>(range fun x => derivWithin f (Ici x) x) ⊆ closure ↑(Submodule.span ℝ (f '' t))
<VAR>F : Type u_1<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>inst✝ : CompleteSpace F<VAR>this✝¹ : MeasurableSpace F := borel F<VAR>this✝ : BorelSpace F<VAR>t : Set ℝ<VAR>t_count : t.Countable<VAR>ht : Dense t<VAR>x : ℝ<GOAL>(fun x => derivWithin f (Ici x) x) x ∈ closure ↑(Submodule.span ℝ (f '' t))
<VAR>F : Type u_1<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>inst✝ : CompleteSpace F<VAR>this✝¹ : MeasurableSpace F := borel F<VAR>this✝ : BorelSpace F<VAR>t : Set ℝ<VAR>t_count : t.Countable<VAR>ht : Dense t<VAR>x : ℝ<GOAL>(range fun y => derivWithin f (Ici x) y) ⊆ closure ↑(Submodule.span ℝ (f '' t))
<VAR>F : Type u_1<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>inst✝ : CompleteSpace F<VAR>this✝¹ : MeasurableSpace F := borel F<VAR>this✝ : BorelSpace F<VAR>t : Set ℝ<VAR>t_count : t.Countable<VAR>ht : Dense t<VAR>x : ℝ<GOAL>Ici x ⊆ closure (Ici x ∩ t)
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>g : Submodule R (E × F)<VAR>hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0<VAR>x : E × F<VAR>hx : x ∈ g<GOAL>x ∈ g.toLinearPMap.graph
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>g : Submodule R (E × F)<VAR>hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0<VAR>x : E × F<VAR>hx : x ∈ g<GOAL>∃ y, ↑y = x.1 ∧ ↑g.toLinearPMap y = x.2
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>g : Submodule R (E × F)<VAR>hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0<VAR>x_fst : E<VAR>x_snd : F<VAR>hx : (x_fst, x_snd) ∈ g<GOAL>∃ y, ↑y = (x_fst, x_snd).1 ∧ ↑g.toLinearPMap y = (x_fst, x_snd).2
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>g : Submodule R (E × F)<VAR>hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0<VAR>x_fst : E<VAR>x_snd : F<VAR>hx : (x_fst, x_snd) ∈ g<VAR>hx_fst : x_fst ∈ map (LinearMap.fst R E F) g<GOAL>∃ y, ↑y = (x_fst, x_snd).1 ∧ ↑g.toLinearPMap y = (x_fst, x_snd).2
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>g : Submodule R (E × F)<VAR>hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0<VAR>x_fst : E<VAR>x_snd : F<VAR>hx : (x_fst, x_snd) ∈ g<VAR>hx_fst : x_fst ∈ map (LinearMap.fst R E F) g<GOAL>↑g.toLinearPMap ⟨x_fst, hx_fst⟩ = (x_fst, x_snd).2
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>g : Submodule R (E × F)<VAR>hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0<VAR>x_fst : E<VAR>x_snd : F<VAR>hx : (x_fst, x_snd) ∈ g<VAR>hx_fst : x_fst ∈ map (LinearMap.fst R E F) g<GOAL>valFromGraph hg ⋯ = (x_fst, x_snd).2
<VAR>M₀✝ : Type u_1<VAR>inst✝¹ : MonoidWithZero M₀✝<VAR>M₀ : Type u_2<VAR>inst✝ : CommMonoidWithZero M₀<VAR>x : M₀<GOAL>x ∈ nonZeroDivisorsLeft M₀ ↔ x ∈ nonZeroDivisorsRight M₀
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<VAR>m : ℤ<GOAL>toIocMod hp a (m • p + b) = toIocMod hp a b
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>M : Type u_1<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : LieRingModule L M<VAR>inst✝³ : LieModule R L M<VAR>M' : Type u_2<VAR>inst✝² : AddCommGroup M'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : LieRingModule L M'<VAR>e : M ≃ₗ⁅R,L⁆ M'<GOAL>e.range = ⊤
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>M : Type u_1<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : LieRingModule L M<VAR>inst✝³ : LieModule R L M<VAR>M' : Type u_2<VAR>inst✝² : AddCommGroup M'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : LieRingModule L M'<VAR>e : M ≃ₗ⁅R,L⁆ M'<GOAL>Function.Surjective ⇑e.toLieModuleHom
<VAR>G : Type u_1<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : SecondCountableTopology G<VAR>μ : Measure G<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>K : Set G<VAR>hK : IsCompact K<VAR>h2K : (interior K).Nonempty<VAR>hμK : μ K ≠ ⊤<GOAL>μ.Regular
<VAR>G : Type u_1<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : SecondCountableTopology G<VAR>μ : Measure G<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>K : Set G<VAR>hK : IsCompact K<VAR>h2K : (interior K).Nonempty<VAR>hμK : μ K ≠ ⊤<GOAL>(μ ↑{ carrier := K, isCompact' := hK, interior_nonempty' := h2K } • haarMeasure { carrier := K, isCompact' := hK, interior_nonempty' := h2K }).Regular
<VAR>α : Type u_1<VAR>inst✝⁵ : Mul α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝¹ : CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c d : α<GOAL>↑(Ioc a b * Ico c d) ⊆ ↑(Ioo (a * c) (b * d))
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>h : p ≠ 0<GOAL>p.natTrailingDegree = p.support.min' ⋯
<VAR>a b c d m n x : ℤ<GOAL>↑x.natAbs ^ 2 = x ^ 2
<VAR>ι : Type u_1<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L M K' L' : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>φ' : K' ⟶ L'<VAR>e : Arrow.mk φ ≅ Arrow.mk φ'<VAR>inst✝³ : ∀ (i : ι), K.HasHomology i<VAR>inst✝² : ∀ (i : ι), L.HasHomology i<VAR>inst✝¹ : ∀ (i : ι), K'.HasHomology i<VAR>inst✝ : ∀ (i : ι), L'.HasHomology i<VAR>hφ : QuasiIso φ<GOAL>QuasiIso φ'
<VAR>p : ℕ<VAR>hp : 0 < p<GOAL>φ p = p - 1 ↔ Prime p
<VAR>p : ℕ<VAR>hp : 0 < p<VAR>h : φ p = p - 1<GOAL>Prime p
<VAR>p : ℕ<VAR>h : φ p = p - 1<VAR>hp : 1 < p<GOAL>Prime p
<VAR>p : ℕ<VAR>h : (filter p.Coprime (Ico (succ 0) p)).card = (Ico 1 p).card<VAR>hp : 1 < p<GOAL>Prime p
<VAR>p : ℕ<VAR>h : (filter p.Coprime (Ico (succ 0) p)).card = (Ico 1 p).card<VAR>hp : 1 < p<VAR>n : ℕ<VAR>hn : n < p<VAR>hnz : n ≠ 0<GOAL>succ 0 ≤ n
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝⁴ : MulOneClass α<VAR>inst✝³ : Zero α<VAR>inst✝² : Preorder α<VAR>inst✝¹ : MulPosMono α<VAR>inst✝ : MulPosReflectLE α<VAR>b0 : 0 < b<GOAL>a * b ≤ b ↔ a * b ≤ 1 * b
<VAR>w x✝ y z✝ : ℝ<VAR>x : ℝ≥0<VAR>z : ℝ<VAR>hx : x ≤ 1<VAR>h_one_le : 1 ≤ z<GOAL>x ^ z ≤ x
<VAR>w x y z✝ z : ℝ<VAR>h_one_le : 1 ≤ z<VAR>hx : ⊥ ≤ 1<GOAL>⊥ ^ z ≤ ⊥
<VAR>w x✝ y z✝ : ℝ<VAR>x : ℝ≥0<VAR>z : ℝ<VAR>hx : x ≤ 1<VAR>h_one_le : 1 ≤ z<VAR>h : 0 < x<GOAL>x ^ z ≤ x
<VAR>w x✝ y z✝ : ℝ<VAR>x : ℝ≥0<VAR>z : ℝ<VAR>hx : x ≤ 1<VAR>h_one_le : 1 ≤ z<VAR>h : 0 < x<GOAL>x ^ z ≤ x ^ 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l : List α<GOAL>l.sublists'.Nodup ↔ l.Nodup
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : E<VAR>p q : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f g : 𝕜 → E<VAR>n : ℕ<VAR>z z₀ : 𝕜<VAR>a : ℕ → E<VAR>hs : HasSum (fun m => z ^ m • a m) s<VAR>ha : ∀ k < n, a k = 0<GOAL>∃ t, z ^ n • t = s ∧ HasSum (fun m => z ^ m • a (m + n)) t
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : E<VAR>p q : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f g : 𝕜 → E<VAR>z z₀ : 𝕜<VAR>a : ℕ → E<VAR>hs : HasSum (fun m => z ^ m • a m) s<VAR>ha : ∀ k < 0, a k = 0<GOAL>∃ t, z ^ 0 • t = s ∧ HasSum (fun m => z ^ m • a (m + 0)) t
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : E<VAR>p q : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f g : 𝕜 → E<VAR>n : ℕ<VAR>z z₀ : 𝕜<VAR>a : ℕ → E<VAR>hs : HasSum (fun m => z ^ m • a m) s<VAR>ha : ∀ k < n, a k = 0<VAR>hn : n > 0<GOAL>∃ t, z ^ n • t = s ∧ HasSum (fun m => z ^ m • a (m + n)) t
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : AddCommGroup L<VAR>inst✝¹² : Module R L<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : Fintype ι'<VAR>inst✝⁷ : Fintype ιM<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : DecidableEq ι'<VAR>inst✝⁴ : Module.Free R M<VAR>inst✝³ : Module.Finite R M<VAR>b✝ : Basis ι R L<VAR>inst✝² : Module.Finite R L<VAR>inst✝¹ : Module.Free R L<VAR>inst✝ : Nontrivial R<VAR>b : Basis ι R L<GOAL>φ.nilRank = (φ.polyCharpoly b).natTrailingDegree
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>wittOne p n = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>(map (Int.castRingHom ℚ)) (wittOne p n) = (map (Int.castRingHom ℚ)) 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>(bind₁ fun k => 1) (xInTermsOfW p ℚ n) = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>IH : ∀ m < n, 0 < m → (bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0<VAR>hn : 0 < n<GOAL>(bind₁ fun k => 1) (xInTermsOfW p ℚ n) = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>IH : ∀ m < n, 0 < m → (bind₁ fun k => 1) (xInTermsOfW p ℚ m) = 0<VAR>hn : 0 < n<GOAL>(bind₁ fun k => 1) ((X n - ∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) * C (⅟↑p ^ n)) = 0