ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : Fintype α<VAR>P : Finpartition univ<VAR>u : Finset α<VAR>ε : ℝ<VAR>l : ℕ<VAR>ι : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : ι → ι → Prop<VAR>inst✝ : DecidableRel r<VAR>s t : Finset ι<VAR>x : 𝕜<VAR>hst : s ⊆ t<VAR>f : ι → 𝕜<VAR>d : 𝕜<VAR>hx : 0 ≤ x<VAR>hs : x ≤ |(∑ i ∈ s, f i) / ↑s.card - (∑ i ∈ t, f i) / ↑t.card|<VAR>ht : d ≤ ((∑ i ∈ t, f i) / ↑t.card) ^ 2<VAR>hscard : 0 < ↑s.card<VAR>htcard : 0 < ↑t.card<VAR>h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑s.card - (∑ i ∈ t, f i) / ↑t.card) ^ 2<VAR>h₂ : x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / ↑t.card)) / ↑s.card) ^ 2<VAR>h₃ : ↑s.card * x ^ 2 ≤ ∑ i ∈ t, (fun i => f i - (∑ j ∈ t, f j) / ↑t.card) i ^ 2<GOAL>(∑ i ∈ t, f i) ^ 2 * ↑t.card + ((∑ i ∈ t, f i ^ 2) * ↑t.card ^ 2 - 2 * ((∑ i ∈ t, f i) * ↑t.card) * ∑ i ∈ t, f i + ↑t.card * (∑ i ∈ t, f i) ^ 2) ≤ (∑ i ∈ t, f i ^ 2) * ↑t.card ^ 2
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>P0 : P ∅<VAR>m0 : m ∅ P0 = 0<VAR>PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯<VAR>m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂<VAR>s : Set α<GOAL>MeasurableSet s ↔ ∀ (t : Set α), P t → (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s) ≤ (inducedOuterMeasure m P0 m0) t
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>P0 : P ∅<VAR>m0 : m ∅ P0 = 0<VAR>PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯<VAR>m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂<VAR>s : Set α<GOAL>(∀ (t : Set α), (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s) ≤ (inducedOuterMeasure m P0 m0) t) ↔ ∀ (t : Set α), P t → (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s) ≤ (inducedOuterMeasure m P0 m0) t
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>inst✝ : Fact (finrank ℝ E = n + 1)<VAR>this : SmoothManifoldWithCorners 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) ↑(sphere 0 1)<GOAL>ContMDiff 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) 𝓘(ℝ, E) ⊤ Subtype.val
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>inst✝ : Fact (finrank ℝ E = n + 1)<VAR>this : SmoothManifoldWithCorners 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) ↑(sphere 0 1)<GOAL>Continuous Subtype.val ∧ ∀ (x : { x // x ∈ sphere 0 1 }) (y : E), ContDiffOn ℝ ⊤ (↑(extChartAt 𝓘(ℝ, E) y) ∘ Subtype.val ∘ ↑(extChartAt 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) x).symm) ((extChartAt 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) x).target ∩ ↑(extChartAt 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) x).symm ⁻¹' (Subtype.val ⁻¹' (extChartAt 𝓘(ℝ, E) y).source))
<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✝³ : Group α<VAR>inst✝² : DivisionMonoid β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : MonoidHomClass F α β<VAR>m : F<VAR>f g f₁ g₁ : Filter α<VAR>f₂ g₂ : Filter β<GOAL>IsUnit f ↔ ∃ a, f = pure a
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : T2Space M<VAR>inst✝ : SigmaCompactSpace M<VAR>s : Set M<VAR>hs : IsClosed s<VAR>U : ι → Set M<VAR>ho : ∀ (i : ι), IsOpen (U i)<VAR>hU : s ⊆ ⋃ i, U i<GOAL>∃ f, f.IsSubordinate U
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : T2Space M<VAR>inst✝ : SigmaCompactSpace M<VAR>s : Set M<VAR>hs : IsClosed s<VAR>U : ι → Set M<VAR>ho : ∀ (i : ι), IsOpen (U i)<VAR>hU : s ⊆ ⋃ i, U i<VAR>this : LocallyCompactSpace H<GOAL>∃ f, f.IsSubordinate U
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : T2Space M<VAR>inst✝ : SigmaCompactSpace M<VAR>s : Set M<VAR>hs : IsClosed s<VAR>U : ι → Set M<VAR>ho : ∀ (i : ι), IsOpen (U i)<VAR>hU : s ⊆ ⋃ i, U i<VAR>this✝ : LocallyCompactSpace H<VAR>this : LocallyCompactSpace M<GOAL>∃ f, f.IsSubordinate U
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : T2Space M<VAR>inst✝ : SigmaCompactSpace M<VAR>s : Set M<VAR>hs : IsClosed s<VAR>U : ι → Set M<VAR>ho : ∀ (i : ι), IsOpen (U i)<VAR>hU : s ⊆ ⋃ i, U i<VAR>this✝¹ : LocallyCompactSpace H<VAR>this✝ : LocallyCompactSpace M<VAR>this : ∃ f, (∀ (i : ι), Smooth I 𝓘(ℝ, ℝ) ⇑(f i)) ∧ f.IsSubordinate U<GOAL>∃ f, f.IsSubordinate U
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : T2Space M<VAR>inst✝ : SigmaCompactSpace M<VAR>s : Set M<VAR>hs : IsClosed s<VAR>U : ι → Set M<VAR>ho : ∀ (i : ι), IsOpen (U i)<VAR>hU : s ⊆ ⋃ i, U i<VAR>this✝ : LocallyCompactSpace H<VAR>this : LocallyCompactSpace M<GOAL>∀ (s t : Set M), IsClosed s → IsClosed t → Disjoint s t → ∃ f, Smooth I 𝓘(ℝ, ℝ) ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : M), f x ∈ Icc 0 1
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n✝ l : ℕ<VAR>φ✝ ψ : L.BoundedFormula α l<VAR>θ : L.BoundedFormula α l.succ<VAR>v✝ : α → M<VAR>xs✝ : Fin l → M<VAR>n m : ℕ<VAR>φ : L.BoundedFormula α n<VAR>v : α → M<VAR>xs : Fin (n + 1) → M<VAR>hmn : m ≤ n<GOAL>(liftAt 1 m φ).Realize v xs ↔ φ.Realize v (xs ∘ fun i => if ↑i < m then i.castSucc else i.succ)
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ η : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>inst✝ : IsFiniteKernel η<VAR>hκη : κ ≤ η<VAR>a : α<GOAL>κ.rnDerivAux η a ≤ᶠ[ae (η a)] 1
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ η : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>inst✝ : IsFiniteKernel η<VAR>hκη : κ ≤ η<VAR>a : α<VAR>x : γ<VAR>hx_le_one : (∂κ a/∂η a) x ≤ 1 x<GOAL>κ.rnDerivAux η a x ≤ 1 x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsRatCondKernelCDF f κ ν<VAR>a : α<VAR>x : ℝ<GOAL>Integrable (fun b => ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) (ν a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsRatCondKernelCDF f κ ν<VAR>a : α<VAR>x : ℝ<VAR>this : (fun b => ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) = fun b => (ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x)).toReal<GOAL>Integrable (fun b => ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) (ν a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsRatCondKernelCDF f κ ν<VAR>a : α<VAR>x : ℝ<VAR>this : (fun b => ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) = fun b => (ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x)).toReal<GOAL>Integrable (fun b => (ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x)).toReal) (ν a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsRatCondKernelCDF f κ ν<VAR>a : α<VAR>x : ℝ<VAR>this : (fun b => ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) = fun b => (ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x)).toReal<GOAL>AEMeasurable (fun b => ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x)) (ν a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsRatCondKernelCDF f κ ν<VAR>a : α<VAR>x : ℝ<VAR>this : (fun b => ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) = fun b => (ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x)).toReal<GOAL>∫⁻ (x_1 : β), ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, x_1)) x) ∂ν a ≠ ⊤
<VAR>m n i h : ℕ<VAR>a✝ : Nat.le 1 h<GOAL>i + h.succ ! ≤ (i + h.succ)!
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>r r' s✝ : α → α → Prop<VAR>s : Set α<GOAL>DirectedOn r s ↔ Directed r Subtype.val
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>r r' s✝ : α → α → Prop<VAR>s : Set α<GOAL>(∀ x ∈ s, ∀ y ∈ s, ∃ z ∈ s, r x z ∧ r y z) ↔ ∀ a ∈ s, ∀ a_1 ∈ s, ∃ a_2, r a a_2 ∧ a_2 ∈ s ∧ r a_1 a_2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>mδ : MeasurableSpace δ<VAR>f✝ : β → γ<VAR>g : γ → α<VAR>μ : Measure α<VAR>f : α → β<VAR>hf : Measurable f<VAR>x : γ<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>(((const γ μ).map f hf) x) s = ((const γ (Measure.map f μ)) x) s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M✝ : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : TopologicalSpace M✝<VAR>inst✝⁴ : Mul M✝<VAR>inst✝³ : ContinuousMul M✝<VAR>M : Type u_6<VAR>inst✝² : Monoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ContinuousMul M<VAR>a b : M<VAR>h : a ⤳ b<VAR>n : ℕ<GOAL>(a ^ Nat.zero) ⤳ (b ^ Nat.zero)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M✝ : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : TopologicalSpace M✝<VAR>inst✝⁴ : Mul M✝<VAR>inst✝³ : ContinuousMul M✝<VAR>M : Type u_6<VAR>inst✝² : Monoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ContinuousMul M<VAR>a b : M<VAR>h : a ⤳ b<VAR>n x✝ : ℕ<VAR>ihn : (a ^ x✝) ⤳ (b ^ x✝)<GOAL>(a ^ x✝.succ) ⤳ (b ^ x✝.succ)
<VAR>J : Type u<VAR>inst✝¹ : Category.{v, u} J<VAR>inst✝ : FinallySmall J<VAR>i : J<GOAL>∃ j ∈ Set.range (fromFinalModel J).obj, Nonempty (i ⟶ j)
<VAR>J : Type u<VAR>inst✝¹ : Category.{v, u} J<VAR>inst✝ : FinallySmall J<VAR>i : J<VAR>f : StructuredArrow i (fromFinalModel J)<GOAL>∃ j ∈ Set.range (fromFinalModel J).obj, Nonempty (i ⟶ j)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x y : ι → ℝ<VAR>δ : ℝ<GOAL>MonotoneOn (fun x => dist x y) (Ici y)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x y : ι → ℝ<VAR>δ : ℝ<VAR>y₁ : ι → ℝ<VAR>hy₁ : y₁ ∈ Ici y<VAR>y₂ : ι → ℝ<VAR>hy₂ : y₂ ∈ Ici y<VAR>hy : y₁ ≤ y₂<VAR>i : ι<VAR>x✝ : i ∈ Finset.univ<GOAL>nndist (y₁ i) (y i) ≤ nndist (y₂ i) (y i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x y : ι → ℝ<VAR>δ : ℝ<VAR>y₁ : ι → ℝ<VAR>hy₁ : y₁ ∈ Ici y<VAR>y₂ : ι → ℝ<VAR>hy₂ : y₂ ∈ Ici y<VAR>hy : y₁ ≤ y₂<VAR>i : ι<VAR>x✝ : i ∈ Finset.univ<GOAL>(y₁ i - y i).toNNReal ≤ (y₂ i - y i).toNNReal
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.61456, u_1} C<VAR>inst✝ : HasShift C ℤ<VAR>n : ℤ<VAR>X : Cᵒᵖ<GOAL>((shiftFunctorCompIsoId C n (-n) ⋯).inv.app (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)) ≫ 𝟙 (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj (Opposite.op ((shiftFunctor C n).obj (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X))))))) ≫ ((shiftFunctor Cᵒᵖ n).map (((shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)).op ≫ ((shiftFunctor C n).map (𝟙 ((shiftFunctor Cᵒᵖ n).obj X)).unop).op)).unop = 𝟙 (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X))
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.61456, u_1} C<VAR>inst✝ : HasShift C ℤ<VAR>n : ℤ<VAR>X : Cᵒᵖ<GOAL>(shiftFunctorCompIsoId C n (-n) ⋯).inv.app (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)) ≫ ((shiftFunctor Cᵒᵖ n).map ((shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)).op).unop = 𝟙 (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X))
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.61456, u_1} C<VAR>inst✝ : HasShift C ℤ<VAR>n : ℤ<VAR>X : Cᵒᵖ<GOAL>(shiftFunctorCompIsoId C n (-n) ⋯).inv.app ((shiftFunctor C (-n)).obj (Opposite.unop X)) ≫ (shiftFunctor C (-n)).map ((shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)) = 𝟙 ((𝟭 C).obj ((shiftFunctor C (-n)).obj (Opposite.unop X)))
<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 : F[X]<VAR>h : f.natDegree = 0<GOAL>f.natSepDegree = 0
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>I✝ I' : Ideal R<VAR>J J' I : Ideal S<VAR>h : (⊤.prod I).IsPrime<GOAL>I.IsPrime
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>I✝ I' : Ideal R<VAR>J J' I : Ideal S<VAR>h : (⊤.prod I).IsPrime<GOAL>(I.prod ⊤).IsPrime
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>I✝ I' : Ideal R<VAR>J J' I : Ideal S<VAR>h : (⊤.prod I).IsPrime<GOAL>(map (↑RingEquiv.prodComm) (⊤.prod I)).IsPrime
<VAR>x✝ y✝ z x y : ℝ<GOAL>rexp (x * y) = rexp x ^ y
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>s : Set ι<VAR>f : ι → Set X<VAR>hs : s.Finite<VAR>hf : ∀ i ∈ s, IsCompact (f i)<VAR>l : Ultrafilter X<VAR>hl : ⋃ i ∈ s, f i ∈ l<GOAL>∃ x ∈ ⋃ i ∈ s, f i, ↑l ≤ 𝓝 x
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>s : Set ι<VAR>f : ι → Set X<VAR>hs : s.Finite<VAR>hf : ∀ i ∈ s, IsCompact (f i)<VAR>l : Ultrafilter X<VAR>hl : ∃ i ∈ s, f i ∈ l<GOAL>∃ x ∈ ⋃ i ∈ s, f i, ↑l ≤ 𝓝 x
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>s : Set ι<VAR>f : ι → Set X<VAR>hs : s.Finite<VAR>hf : ∀ i ∈ s, IsCompact (f i)<VAR>l : Ultrafilter X<VAR>i : ι<VAR>his : i ∈ s<VAR>hi : f i ∈ l<GOAL>∃ x ∈ ⋃ i ∈ s, f i, ↑l ≤ 𝓝 x
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>s : Set ι<VAR>f : ι → Set X<VAR>hs : s.Finite<VAR>hf : ∀ i ∈ s, IsCompact (f i)<VAR>l : Ultrafilter X<VAR>i : ι<VAR>his : i ∈ s<VAR>hi : f i ∈ l<VAR>x : X<VAR>hxi : x ∈ f i<VAR>hlx : ↑l ≤ 𝓝 x<GOAL>∃ x ∈ ⋃ i ∈ s, f i, ↑l ≤ 𝓝 x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : C(X, ℝ)<VAR>t : Set ℝ<VAR>e : X → Y<VAR>hs : t.OrdConnected<VAR>hf : ∀ (x : X), f x ∈ t<VAR>hne : t.Nonempty<VAR>he : ClosedEmbedding e<VAR>h : ℝ ≃o ↑(Ioo (-1) 1)<GOAL>∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : C(X, ℝ)<VAR>t : Set ℝ<VAR>e : X → Y<VAR>hs : t.OrdConnected<VAR>hf : ∀ (x : X), f x ∈ t<VAR>hne : t.Nonempty<VAR>he : ClosedEmbedding e<VAR>h : ℝ ≃o ↑(Ioo (-1) 1)<VAR>F : X →ᵇ ℝ := { toFun := Subtype.val ∘ ⇑h ∘ ⇑f, continuous_toFun := ⋯, map_bounded' := ⋯ }<GOAL>∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : C(X, ℝ)<VAR>t : Set ℝ<VAR>e : X → Y<VAR>hs : t.OrdConnected<VAR>hf : ∀ (x : X), f x ∈ t<VAR>hne : t.Nonempty<VAR>he : ClosedEmbedding e<VAR>h : ℝ ≃o ↑(Ioo (-1) 1)<VAR>F : X →ᵇ ℝ := { toFun := Subtype.val ∘ ⇑h ∘ ⇑f, continuous_toFun := ⋯, map_bounded' := ⋯ }<VAR>t' : Set ℝ := Subtype.val ∘ ⇑h '' t<GOAL>∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : C(X, ℝ)<VAR>t : Set ℝ<VAR>e : X → Y<VAR>hs : t.OrdConnected<VAR>hf : ∀ (x : X), f x ∈ t<VAR>hne : t.Nonempty<VAR>he : ClosedEmbedding e<VAR>h : ℝ ≃o ↑(Ioo (-1) 1)<VAR>F : X →ᵇ ℝ := { toFun := Subtype.val ∘ ⇑h ∘ ⇑f, continuous_toFun := ⋯, map_bounded' := ⋯ }<VAR>t' : Set ℝ := Subtype.val ∘ ⇑h '' t<VAR>ht_sub : t' ⊆ Ioo (-1) 1<GOAL>∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : C(X, ℝ)<VAR>t : Set ℝ<VAR>e : X → Y<VAR>hs : t.OrdConnected<VAR>hf : ∀ (x : X), f x ∈ t<VAR>hne : t.Nonempty<VAR>he : ClosedEmbedding e<VAR>h : ℝ ≃o ↑(Ioo (-1) 1)<VAR>F : X →ᵇ ℝ := { toFun := Subtype.val ∘ ⇑h ∘ ⇑f, continuous_toFun := ⋯, map_bounded' := ⋯ }<VAR>t' : Set ℝ := Subtype.val ∘ ⇑h '' t<VAR>ht_sub : t' ⊆ Ioo (-1) 1<VAR>this : t'.OrdConnected<GOAL>∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : C(X, ℝ)<VAR>t : Set ℝ<VAR>e : X → Y<VAR>hs : t.OrdConnected<VAR>hf : ∀ (x : X), f x ∈ t<VAR>hne : t.Nonempty<VAR>he : ClosedEmbedding e<VAR>h : ℝ ≃o ↑(Ioo (-1) 1)<VAR>F : X →ᵇ ℝ := { toFun := Subtype.val ∘ ⇑h ∘ ⇑f, continuous_toFun := ⋯, map_bounded' := ⋯ }<VAR>t' : Set ℝ := Subtype.val ∘ ⇑h '' t<VAR>ht_sub : t' ⊆ Ioo (-1) 1<VAR>this : t'.OrdConnected<VAR>hFt : ∀ (x : X), F x ∈ t'<GOAL>∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : C(X, ℝ)<VAR>t : Set ℝ<VAR>e : X → Y<VAR>hs : t.OrdConnected<VAR>hf : ∀ (x : X), f x ∈ t<VAR>hne : t.Nonempty<VAR>he : ClosedEmbedding e<VAR>h : ℝ ≃o ↑(Ioo (-1) 1)<VAR>F : X →ᵇ ℝ := { toFun := Subtype.val ∘ ⇑h ∘ ⇑f, continuous_toFun := ⋯, map_bounded' := ⋯ }<VAR>t' : Set ℝ := Subtype.val ∘ ⇑h '' t<VAR>ht_sub : t' ⊆ Ioo (-1) 1<VAR>this : t'.OrdConnected<VAR>hFt : ∀ (x : X), F x ∈ t'<VAR>G : Y →ᵇ ℝ<VAR>hG : ∀ (y : Y), G y ∈ t'<VAR>hGF : ⇑G ∘ e = ⇑F<GOAL>∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : C(X, ℝ)<VAR>t : Set ℝ<VAR>e : X → Y<VAR>hs : t.OrdConnected<VAR>hf : ∀ (x : X), f x ∈ t<VAR>hne : t.Nonempty<VAR>he : ClosedEmbedding e<VAR>h : ℝ ≃o ↑(Ioo (-1) 1)<VAR>F : X →ᵇ ℝ := { toFun := Subtype.val ∘ ⇑h ∘ ⇑f, continuous_toFun := ⋯, map_bounded' := ⋯ }<VAR>t' : Set ℝ := Subtype.val ∘ ⇑h '' t<VAR>ht_sub : t' ⊆ Ioo (-1) 1<VAR>this : t'.OrdConnected<VAR>hFt : ∀ (x : X), F x ∈ t'<VAR>G : Y →ᵇ ℝ<VAR>hG : ∀ (y : Y), G y ∈ t'<VAR>hGF : ⇑G ∘ e = ⇑F<VAR>g : C(Y, ℝ) := { toFun := ⇑h.symm ∘ Set.codRestrict (⇑G) (Ioo (-1) 1) ⋯, continuous_toFun := ⋯ }<GOAL>∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : C(X, ℝ)<VAR>t : Set ℝ<VAR>e : X → Y<VAR>hs : t.OrdConnected<VAR>hf : ∀ (x : X), f x ∈ t<VAR>hne : t.Nonempty<VAR>he : ClosedEmbedding e<VAR>h : ℝ ≃o ↑(Ioo (-1) 1)<VAR>F : X →ᵇ ℝ := { toFun := Subtype.val ∘ ⇑h ∘ ⇑f, continuous_toFun := ⋯, map_bounded' := ⋯ }<VAR>t' : Set ℝ := Subtype.val ∘ ⇑h '' t<VAR>ht_sub : t' ⊆ Ioo (-1) 1<VAR>this : t'.OrdConnected<VAR>hFt : ∀ (x : X), F x ∈ t'<VAR>G : Y →ᵇ ℝ<VAR>hG : ∀ (y : Y), G y ∈ t'<VAR>hGF : ⇑G ∘ e = ⇑F<VAR>g : C(Y, ℝ) := { toFun := ⇑h.symm ∘ Set.codRestrict (⇑G) (Ioo (-1) 1) ⋯, continuous_toFun := ⋯ }<VAR>hgG : ∀ {y : Y} {a : ℝ}, g y = a ↔ G y = ↑(h a)<GOAL>∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>X : C<GOAL>e.counitInv.app (e.functor.obj X) ≫ e.functor.map (e.unitInv.app X) = 𝟙 (e.functor.obj X)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>X : C<GOAL>(e.functor.mapIso (e.unitIso.app X) ≪≫ e.counitIso.app (e.functor.obj X)).hom = (Iso.refl (e.functor.obj ((𝟭 C).obj X))).hom
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝³ : Zero R<VAR>inst✝² : Zero M<VAR>inst✝¹ : SMulWithZero R M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>c : R<VAR>g : α → M<VAR>hc : c ≠ 0<VAR>x : α<GOAL>x ∈ support (c • g) ↔ x ∈ support g
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>L' : Type w₁<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>I✝ J : LieIdeal R L<VAR>f : L' →ₗ⁅R⁆ L<VAR>I : LieIdeal R L<VAR>s₁ : Set ℕ := {k | derivedSeries R (↥↑I) k = ⊥}<VAR>s₂ : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}<VAR>k : ℕ<GOAL>k ∈ s₁ ↔ k ∈ s₂
<VAR>x y : ℂ<GOAL>cos x - cos y = 0 ↔ -2 * sin ((x + y) / 2) * sin ((x - y) / 2) = 0
<VAR>x y : ℂ<GOAL>sin ((x - y) / 2) = 0 ∨ sin ((x + y) / 2) = 0 ↔ (∃ k, y = 2 * ↑k * ↑π + x) ∨ ∃ k, y = 2 * ↑k * ↑π - x
<VAR>x y : ℂ<GOAL>(∃ k, x = ↑k * ↑π * 2 + y) ↔ ∃ k, y = ↑k * ↑π * 2 + x
<VAR>x y z : ℂ<VAR>hx : x ≠ 0<GOAL>x ^ (y - z) = x ^ y / x ^ z
<GOAL>¬{x | ∀ ⦃a : ℝ⦄, (a ∈ range fun x => ↑x) → a ≤ x}.Nonempty
<GOAL>{x | ∀ ⦃a : ℝ⦄, (a ∈ range fun x => ↑x) → a ≤ x} = ∅
<VAR>x✝ : ℝ<GOAL>x✝ ∈ {x | ∀ ⦃a : ℝ⦄, (a ∈ range fun x => ↑x) → a ≤ x} ↔ x✝ ∈ ∅
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X : C<VAR>inst✝ : HasBinaryCoproducts C<VAR>X✝ Y✝ : (coprodMonad X).Algebra<VAR>f : X✝ ⟶ Y✝<GOAL>((fun A => Under.mk (coprod.inl ≫ A.a)) X✝).hom ≫ f.f = ((fun A => Under.mk (coprod.inl ≫ A.a)) Y✝).hom
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X : C<VAR>inst✝ : HasBinaryCoproducts C<VAR>X✝ Y✝ : (coprodMonad X).Algebra<VAR>f : X✝ ⟶ Y✝<GOAL>coprod.inl ≫ (coprodMonad X).map f.f ≫ Y✝.a = ((fun A => Under.mk (coprod.inl ≫ A.a)) Y✝).hom
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>s : Set M<GOAL>(LinearIndependent R fun (x : ↑s) => ↑x) ↔ LinearMap.ker (Finsupp.totalOn M M R id s) = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>h : l.HasBasis p s<VAR>i✝ j✝ : ι<VAR>hi : p i✝<VAR>hj : p j✝<GOAL>∃ k, p k ∧ s k ⊆ s i✝ ∩ s j✝
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y : α<GOAL>nndist x y = (edist x y).toNNReal