ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝ : TopologicalSpace X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>s' : Set X<VAR>hs' : IsClosed s'<VAR>ht : IsClosed (Subtype.val ⁻¹' s')<GOAL>IsClosed (Subtype.val '' (Subtype.val ⁻¹' s'))
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝ : TopologicalSpace X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>s' : Set X<VAR>hs' : IsClosed s'<VAR>ht : IsClosed (Subtype.val ⁻¹' s')<GOAL>IsClosed (s ∩ s')
<VAR>R : Type u_1<VAR>inst✝³ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝ : CommSemiring P<VAR>m : ℕ<GOAL>mk (↑m) 1 = ↑m
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} A<VAR>A' : Type u₂<VAR>inst✝² : Category.{max v₁ u₁, u₂} A'<VAR>B : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} B<VAR>J : GrothendieckTopology C<VAR>U : C<VAR>R : Presieve U<VAR>P : Cᵒᵖ ⥤ A<VAR>P' : Cᵒᵖ ⥤ A'<VAR>s : A ⥤ B<VAR>inst✝ : PreservesLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s<VAR>h : IsSheaf J P<GOAL>IsSheaf J (P ⋙ s)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} A<VAR>A' : Type u₂<VAR>inst✝² : Category.{max v₁ u₁, u₂} A'<VAR>B : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} B<VAR>J : GrothendieckTopology C<VAR>U : C<VAR>R : Presieve U<VAR>P : Cᵒᵖ ⥤ A<VAR>P' : Cᵒᵖ ⥤ A'<VAR>s : A ⥤ B<VAR>inst✝ : PreservesLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s<VAR>h : ∀ ⦃X : C⦄, ∀ S ∈ J.sieves X, Nonempty (IsLimit (P.mapCone S.arrows.cocone.op))<GOAL>∀ ⦃X : C⦄, ∀ S ∈ J.sieves X, Nonempty (IsLimit ((P ⋙ s).mapCone S.arrows.cocone.op))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>A : Set γ<VAR>hA : MeasurableSet A<GOAL>∫ (x : γ) in A, κ.density ν a x s ∂ν a = ((κ a) (A ×ˢ s)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>A : Set γ<VAR>hA : MeasurableSet A<VAR>this : IsFiniteKernel κ<GOAL>∫ (x : γ) in A, κ.density ν a x s ∂ν a = ((κ a) (A ×ˢ s)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>A : Set γ<VAR>hA : MeasurableSet A<VAR>this : IsFiniteKernel κ<VAR>hA' : MeasurableSet A<GOAL>∫ (x : γ) in A, κ.density ν a x s ∂ν a = ((κ a) (A ×ˢ s)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>A : Set γ<VAR>hA : MeasurableSet A<VAR>this : IsFiniteKernel κ<VAR>hA' : MeasurableSet A<GOAL>IsPiSystem {s | ∃ n, MeasurableSet s}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>A : Set γ<VAR>hA : MeasurableSet A<VAR>this : IsFiniteKernel κ<VAR>hA' : MeasurableSet A<GOAL>(fun A => ∫ (x : γ) in A, κ.density ν a x s ∂ν a = ((κ a) (A ×ˢ s)).toReal) ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>A : Set γ<VAR>hA : MeasurableSet A<VAR>this : IsFiniteKernel κ<VAR>hA' : MeasurableSet A<GOAL>∀ t ∈ {s | ∃ n, MeasurableSet s}, (fun A => ∫ (x : γ) in A, κ.density ν a x s ∂ν a = ((κ a) (A ×ˢ s)).toReal) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>A : Set γ<VAR>hA : MeasurableSet A<VAR>this : IsFiniteKernel κ<VAR>hA' : MeasurableSet A<GOAL>∀ (t : Set γ), MeasurableSet t → (fun A => ∫ (x : γ) in A, κ.density ν a x s ∂ν a = ((κ a) (A ×ˢ s)).toReal) t → (fun A => ∫ (x : γ) in A, κ.density ν a x s ∂ν a = ((κ a) (A ×ˢ s)).toReal) tᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>A : Set γ<VAR>hA : MeasurableSet A<VAR>this : IsFiniteKernel κ<VAR>hA' : MeasurableSet A<GOAL>∀ (f : ℕ → Set γ), Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), (fun A => ∫ (x : γ) in A, κ.density ν a x s ∂ν a = ((κ a) (A ×ˢ s)).toReal) (f i)) → (fun A => ∫ (x : γ) in A, κ.density ν a x s ∂ν a = ((κ a) (A ×ˢ s)).toReal) (⋃ i, f i)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l✝ : Filter α<VAR>s t : Set α<VAR>l : Filter α<GOAL>s =ᶠ[l] t ↔ l ⊓ 𝓟 s = l ⊓ 𝓟 t
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w₁ w₂ : W<GOAL>cs.length w₁ - cs.length w₂ ≤ cs.length (w₁ * w₂)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>T : Type u_4<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>inst✝¹¹ : SemilatticeSup B<VAR>inst✝¹⁰ : OrderBot B<VAR>inst✝⁹ : SemilatticeInf T<VAR>inst✝⁸ : OrderTop T<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : AddCommMonoid A<VAR>inst✝⁵ : AddCommMonoid B<VAR>inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝² : AddCommMonoid T<VAR>inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>degb : A → B<VAR>degt : A → T<VAR>degt0 : 0 ≤ degt 0<VAR>degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)<VAR>m : Multiset R[A]<GOAL>(Multiset.map (fun f => f.support.inf degt) m).sum ≤ m.prod.support.inf degt
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>T : Type u_4<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>inst✝¹¹ : SemilatticeSup B<VAR>inst✝¹⁰ : OrderBot B<VAR>inst✝⁹ : SemilatticeInf T<VAR>inst✝⁸ : OrderTop T<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : AddCommMonoid A<VAR>inst✝⁵ : AddCommMonoid B<VAR>inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝² : AddCommMonoid T<VAR>inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>degb : A → B<VAR>degt : A → T<VAR>degt0 : 0 ≤ degt 0<VAR>degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)<VAR>m : Multiset R[A]<GOAL>OrderDual.ofDual (degt 0) ≤ OrderDual.ofDual 0
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>T : Type u_4<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>inst✝¹¹ : SemilatticeSup B<VAR>inst✝¹⁰ : OrderBot B<VAR>inst✝⁹ : SemilatticeInf T<VAR>inst✝⁸ : OrderTop T<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : AddCommMonoid A<VAR>inst✝⁵ : AddCommMonoid B<VAR>inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝² : AddCommMonoid T<VAR>inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>degb : A → B<VAR>degt : A → T<VAR>degt0 : 0 ≤ degt 0<VAR>degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)<VAR>m : Multiset R[A]<VAR>a b : A<GOAL>OrderDual.ofDual (degt (a + b)) ≤ OrderDual.ofDual (degt a + degt b)
<VAR>X₁ X₂ Y : TopCat<VAR>f : C(↑X₁, ↑Y)<VAR>g : C(↑X₂, ↑Y)<VAR>x₀ x₁ : ↑X₁<VAR>x₂ x₃ : ↑X₂<VAR>p : Path x₀ x₁<VAR>q : Path x₂ x₃<VAR>hfg : ∀ (t : ↑I), f (p t) = g (q t)<GOAL>f x₁ = g x₃
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<VAR>f : Perm (Fin n)<VAR>x✝ : (_ : Fin n) × Fin n<VAR>a₁ a₂ : Fin n<VAR>ha : ⟨a₁, a₂⟩ ∈ finPairsLT n<VAR>hxa : f⁻¹ a₂ < f⁻¹ a₁<GOAL>(if f (f⁻¹ a₂) < f (f⁻¹ a₁) then ⟨f (f⁻¹ a₁), f (f⁻¹ a₂)⟩ else ⟨f (f⁻¹ a₂), f (f⁻¹ a₁)⟩) = ⟨a₁, a₂⟩
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<VAR>f : Perm (Fin n)<VAR>x✝ : (_ : Fin n) × Fin n<VAR>a₁ a₂ : Fin n<VAR>ha : ⟨a₁, a₂⟩ ∈ finPairsLT n<VAR>hxa : ¬f⁻¹ a₂ < f⁻¹ a₁<VAR>h : f⁻¹ a₁ = f⁻¹ a₂<GOAL>False
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<VAR>f : Perm (Fin n)<VAR>x✝ : (_ : Fin n) × Fin n<VAR>a₁ a₂ : Fin n<VAR>ha : ⟨a₁, a₂⟩ ∈ finPairsLT n<VAR>hxa : ¬f⁻¹ a₂ < f⁻¹ a₁<GOAL>(if f (f⁻¹ a₁) < f (f⁻¹ a₂) then ⟨f (f⁻¹ a₂), f (f⁻¹ a₁)⟩ else ⟨f (f⁻¹ a₁), f (f⁻¹ a₂)⟩) = ⟨a₁, a₂⟩
<VAR>c : ℝ<GOAL>∫ (x : ℝ) in Iic c, rexp x = rexp c
<VAR>c : ℝ<GOAL>Tendsto (fun i => ∫ (x : ℝ) in id i..c, rexp x) atBot (𝓝 (rexp c))
<VAR>c : ℝ<GOAL>Tendsto (fun i => rexp c - rexp (id i)) atBot (𝓝 (rexp c - 0))
<VAR>u v : Level<VAR>n nn n' : ℕ<VAR>pn : NormNum.IsNat n nn<VAR>pn' : nn = n'.succ<GOAL>Multiset.range n = n' ::ₘ Multiset.range n'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p q : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred q<VAR>s t : Finset α<GOAL>filter p s = ∅ ↔ ∀ ⦃x : α⦄, x ∈ s → ¬p x
<VAR>a x z : ℂ<VAR>h : x ∈ slitPlane<GOAL>ContinuousAt arg x
<VAR>a x z : ℂ<VAR>h : x ∈ slitPlane<VAR>h₀ : abs x ≠ 0<GOAL>ContinuousAt arg x
<VAR>a x z : ℂ<VAR>h : 0 < x.re ∨ x.im < 0 ∨ 0 < x.im<VAR>h₀ : abs x ≠ 0<GOAL>ContinuousAt arg x
<VAR>a x z : ℂ<VAR>h₀ : abs x ≠ 0<VAR>hx_re : 0 < x.re<GOAL>ContinuousAt arg x
<VAR>a x z : ℂ<VAR>h₀ : abs x ≠ 0<VAR>hx_im : x.im < 0<GOAL>ContinuousAt arg x
<VAR>a x z : ℂ<VAR>h₀ : abs x ≠ 0<VAR>hx_im : 0 < x.im<GOAL>ContinuousAt arg x
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>inst✝ : L.Structure M<VAR>α : Type w'<GOAL>L[[α]].card = lift.{w', max u v} L.card + lift.{max u v, w'} #α
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>inst✝² : Category.{u_3, u_1} J<VAR>inst✝¹ : Category.{u_4, u_2} C<VAR>inst✝ : ChosenFiniteProducts C<VAR>F : J ⥤ C<VAR>j : J<GOAL>(λ_ F).inv.app j = (λ_ (F.obj j)).inv
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : Mul α<VAR>inst✝² : Mul β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : MulHomClass F α β<VAR>m : F<VAR>s✝ t✝ : Set α<VAR>s t : Set β<VAR>w✝¹ : α<VAR>left✝¹ : w✝¹ ∈ ⇑m ⁻¹' s<VAR>w✝ : α<VAR>left✝ : w✝ ∈ ⇑m ⁻¹' t<GOAL>(fun x x_1 => x * x_1) w✝¹ w✝ ∈ ⇑m ⁻¹' (s * t)
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>cof 0 = 0
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>cof 0 ≤ 0
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>cof 0 ≤ card 0
<VAR>𝕜 : Type u_1<VAR>E : Type u<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>hx : x ∈ (convexHull 𝕜) s<VAR>k : ℕ := (minCardFinsetOfMemConvexHull hx).card - 1<GOAL>AffineIndependent 𝕜 Subtype.val
<VAR>𝕜 : Type u_1<VAR>E : Type u<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>hx : x ∈ (convexHull 𝕜) s<VAR>k : ℕ := (minCardFinsetOfMemConvexHull hx).card - 1<VAR>hk : (minCardFinsetOfMemConvexHull hx).card = k + 1<GOAL>AffineIndependent 𝕜 Subtype.val
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f✝ g : Filter α<VAR>s t : Set α<VAR>f : ι → Filter α<VAR>h : Directed (fun x x_1 => x ≥ x_1) f<VAR>ne : Nonempty ι<VAR>i : ι<GOAL>∀ {x y : Set α}, x ∈ ⋃ i, (f i).sets → x ⊆ y → y ∈ ⋃ i, (f i).sets
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f✝ g : Filter α<VAR>s t : Set α<VAR>f : ι → Filter α<VAR>h : Directed (fun x x_1 => x ≥ x_1) f<VAR>ne : Nonempty ι<VAR>i : ι<GOAL>∀ {x y : Set α} (x_1 : ι), x ∈ (f x_1).sets → x ⊆ y → ∃ i, y ∈ (f i).sets
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f✝ g : Filter α<VAR>s t : Set α<VAR>f : ι → Filter α<VAR>h : Directed (fun x x_1 => x ≥ x_1) f<VAR>ne : Nonempty ι<VAR>i : ι<GOAL>∀ {x y : Set α}, x ∈ ⋃ i, (f i).sets → y ∈ ⋃ i, (f i).sets → x ∩ y ∈ ⋃ i, (f i).sets
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f✝ g : Filter α<VAR>s t : Set α<VAR>f : ι → Filter α<VAR>h : Directed (fun x x_1 => x ≥ x_1) f<VAR>ne : Nonempty ι<VAR>i : ι<GOAL>∀ {x y : Set α} (x_1 : ι), x ∈ (f x_1).sets → ∀ (x_2 : ι), y ∈ (f x_2).sets → ∃ i, x ∩ y ∈ (f i).sets
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f✝ g : Filter α<VAR>s t : Set α<VAR>f : ι → Filter α<VAR>h : Directed (fun x x_1 => x ≥ x_1) f<VAR>ne : Nonempty ι<VAR>i : ι<VAR>x y : Set α<VAR>a : ι<VAR>hx : x ∈ (f a).sets<VAR>b : ι<VAR>hy : y ∈ (f b).sets<VAR>c : ι<VAR>ha : f a ≥ f c<VAR>hb : f b ≥ f c<GOAL>∃ i, x ∩ y ∈ (f i).sets
<VAR>f : ℕ → ℂ<VAR>s s' : ℂ<VAR>h : s.re ≤ s'.re<VAR>n : ℕ<GOAL>‖term f s' n‖ ≤ ‖term f s n‖
<VAR>f : ℕ → ℂ<VAR>s s' : ℂ<VAR>h : s.re ≤ s'.re<VAR>n : ℕ<GOAL>(if n = 0 then 0 else ‖f n‖ / ↑n ^ s'.re) ≤ if n = 0 then 0 else ‖f n‖ / ↑n ^ s.re
<VAR>f : ℕ → ℂ<VAR>s s' : ℂ<VAR>h : s.re ≤ s'.re<VAR>n : ℕ<VAR>h✝ : ¬n = 0<GOAL>‖f n‖ / ↑n ^ s'.re ≤ ‖f n‖ / ↑n ^ s.re
<VAR>R : Type u_1<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Pow R ℕ<VAR>inst✝ : BinomialRing R<VAR>n : ℕ<GOAL>multichoose (-↑n) n = (-1) ^ n
<VAR>R : Type u_1<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Pow R ℕ<VAR>inst✝ : BinomialRing R<VAR>n : ℕ<GOAL>(fun x => ?m.77547.factorial • x) (multichoose (-↑n) n) = (fun x => ?m.77547.factorial • x) ((-1) ^ n)
<VAR>R : Type u_1<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Pow R ℕ<VAR>inst✝ : BinomialRing R<VAR>n : ℕ<GOAL>ℕ
<VAR>R : Type u_1<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Pow R ℕ<VAR>inst✝ : BinomialRing R<VAR>n : ℕ<GOAL>?m.77547.factorial • multichoose (-↑n) n = ?m.77547.factorial • (-1) ^ n
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a a₁ a₂ b c : G<VAR>inst✝ : Group G<VAR>a✝ b✝ : G<VAR>ha : a✝ ∈ center G<VAR>hb : b✝ ∈ center G<VAR>g : G<GOAL>g * (a✝ * b✝) = a✝ * b✝ * g
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a✝ a₁ a₂ b c : G<VAR>inst✝ : Group G<VAR>a : G<VAR>ha : a ∈ center G<VAR>g : G<GOAL>a⁻¹ * (g * a) * a⁻¹ = a⁻¹ * g
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a✝ a₁ a₂ b c : G<VAR>inst✝ : Group G<VAR>a : G<VAR>ha : a ∈ center G<VAR>g : G<GOAL>a⁻¹ * g * (a * a⁻¹) = a⁻¹ * g
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a a₁ a₂ b c : G<VAR>inst✝ : Group G<VAR>n : G<VAR>ha : n ∈ center G<VAR>g h : G<GOAL>h * (g * n * g⁻¹) = h * n
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a a₁ a₂ b c : G<VAR>inst✝ : Group G<VAR>n : G<VAR>ha : n ∈ center G<VAR>g h : G<GOAL>g * g⁻¹ * n * h = g * n * g⁻¹ * h
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>φ ψ : R[X]<GOAL>↑φ = 1 ↔ φ = 1
<VAR>R✝ : Type u_1<VAR>inst✝¹⁵ : Semiring R✝<VAR>M : Type u_2<VAR>inst✝¹⁴ : AddCommMonoid M<VAR>inst✝¹³ : Module R✝ M<VAR>N : Type u_3<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : Module R✝ N<VAR>P : Type u_4<VAR>inst✝¹⁰ : AddCommMonoid P<VAR>inst✝⁹ : Module R✝ P<VAR>M' : Type u_5<VAR>inst✝⁸ : AddCommGroup M'<VAR>inst✝⁷ : Module R✝ M'<VAR>N' : Type u_6<VAR>inst✝⁶ : AddCommGroup N'<VAR>inst✝⁵ : Module R✝ N'<VAR>ι✝ : Type u_7<VAR>ι' : Type u_8<VAR>ι'' : Type u_9<VAR>f✝ f' : M [⋀^ι✝]→ₗ[R✝] N<VAR>g g₂ : M [⋀^ι✝]→ₗ[R✝] N'<VAR>g' : M' [⋀^ι✝]→ₗ[R✝] N'<VAR>v✝ : ι✝ → M<VAR>v' : ι✝ → M'<VAR>R : Type u_10<VAR>M₁ : Type u_11<VAR>M₂ : Type u_12<VAR>ι : Type u_13<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M₁<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Module R M₂<VAR>f : M₁ [⋀^ι]→ₗ[R] R<VAR>z : M₂<VAR>v : ι → M₁<VAR>i j : ι<VAR>h : v i = v j<VAR>hne : i ≠ j<GOAL>__src✝.toFun v = 0
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Semiring α<VAR>i j : n<VAR>c : α<VAR>i' j' : n<VAR>inst✝ : Fintype n<VAR>a b : n<VAR>h : a ≠ i<VAR>M : Matrix n n α<GOAL>(stdBasisMatrix i j c * M) a b = 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>p p₀ p₁ p₂ p1 p2 p3 : P<VAR>hp1p2 : p1 ≠ p2<VAR>hp3p2 : p3 ≠ p2<GOAL>dist p1 p3 = dist p1 p2 + dist p3 p2 ↔ ∠ p1 p2 p3 = π
<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>p p₀ p₁ p₂ p1 p2 p3 : P<VAR>hp1p2 : p1 ≠ p2<VAR>hp3p2 : p3 ≠ p2<GOAL>‖p1 -ᵥ ?p₃ - (p3 -ᵥ ?p₃)‖ = ‖p1 -ᵥ p2‖ + ‖p3 -ᵥ p2‖ ↔ ∠ p1 p2 p3 = π
<VAR>X : Type u_1<VAR>inst✝¹ : PseudoMetricSpace X<VAR>inst✝ : IsUltrametricDist X<VAR>x✝¹ y✝ z : X<VAR>r✝ s : ℝ<VAR>x y : X<VAR>r : ℝ<VAR>h : y ∈ closedBall x r<VAR>x✝ : X<GOAL>x✝ ∈ closedBall x r ↔ x✝ ∈ closedBall y r
<VAR>X : Type u_1<VAR>inst✝¹ : PseudoMetricSpace X<VAR>inst✝ : IsUltrametricDist X<VAR>x✝¹ y✝ z : X<VAR>r✝ s : ℝ<VAR>x y : X<VAR>r : ℝ<VAR>x✝ : X<VAR>h : dist y x ≤ r<GOAL>dist x✝ x ≤ r ↔ dist x✝ y ≤ r
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x y : G<VAR>n m : ℕ<VAR>h : IsOfFinOrder x<GOAL>minimalPeriod (fun x_1 => x ^ n * x_1) 1 = minimalPeriod (fun x_1 => x * x_1) 1 / (minimalPeriod (fun x_1 => x * x_1) 1).gcd n
<VAR>X : Compactum<VAR>A : Set X.A<GOAL>IsClosed (Compactum.cl A)
<VAR>X : Compactum<VAR>A : Set X.A<GOAL>∀ (F : Ultrafilter X.A), Compactum.cl A ∈ F → X.str F ∈ Compactum.cl A
<VAR>X : Compactum<VAR>A : Set X.A<VAR>F : Ultrafilter X.A<VAR>hF : Compactum.cl A ∈ F<GOAL>X.str F ∈ Compactum.cl A
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s : Set α<VAR>t : Set β<VAR>hs : s.Finite<VAR>ht : t.Finite<GOAL>(s ×ˢ t).Finite
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s : Set α<VAR>t : Set β<VAR>hs : s.Finite<VAR>ht : t.Finite<VAR>this : Finite ↑s<GOAL>(s ×ˢ t).Finite
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s : Set α<VAR>t : Set β<VAR>hs : s.Finite<VAR>ht : t.Finite<VAR>this✝ : Finite ↑s<VAR>this : Finite ↑t<GOAL>(s ×ˢ t).Finite
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : AffineSubspace k P<VAR>h : (↑s).Nonempty<GOAL>directionOfNonempty h = s.direction
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : AffineSubspace k P<VAR>h : (↑s).Nonempty<GOAL>directionOfNonempty h ≤ s.direction
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : AffineSubspace k P<VAR>h : (↑s).Nonempty<GOAL>↑{ carrier := ↑s -ᵥ ↑s, add_mem' := ⋯ } ⊆ ↑(vectorSpan k ↑s)
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>s₁✝ : Finmap β<VAR>s₁ : AList β<GOAL>⟦s₁⟧ ∪ ∅ = ⟦s₁⟧
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>s₁✝ : Finmap β<VAR>s₁ : AList β<GOAL>⟦s₁⟧ ∪ ⟦∅⟧ = ⟦s₁⟧
<VAR>X : Type u_1<VAR>x : X<GOAL>toFinsupp (of x) = single x 1
<VAR>α✝ : Sort u<VAR>β✝ : Sort v<VAR>γ✝ : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Set α<VAR>t : Set β<VAR>u : Set γ<GOAL>⇑(prodAssoc α β γ) '' (s ×ˢ t) ×ˢ u = s ×ˢ t ×ˢ u
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a : Associates α<VAR>a✝ : Nontrivial α<GOAL>a.factors = ⊤ ↔ a = 0
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>f : G →g G'<VAR>f' : G' →g G''<VAR>u v u' v' : V<VAR>p : G.Walk u v<GOAL>(Walk.map f p).reverse = Walk.map f p.reverse
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>deriv negMulLog x = -log x - 1
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>-(log x + 1) = -log x - 1
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → F'<VAR>s : Set α<VAR>hm_not : ¬m ≤ m0<GOAL>μ[f|m] = 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>p1 p2 p3 : P<VAR>h : InnerProductGeometry.angle (p1 -ᵥ p2) (p3 -ᵥ p2) = InnerProductGeometry.angle (p1 -ᵥ p3) (p2 -ᵥ p3)<VAR>hpi : InnerProductGeometry.angle (p2 -ᵥ p1) (p3 -ᵥ p1) ≠ π<GOAL>dist p1 p2 = dist p1 p3
<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>p1 p2 p3 : P<VAR>h : InnerProductGeometry.angle (p1 -ᵥ p2) (p3 -ᵥ p2) = InnerProductGeometry.angle (p1 -ᵥ p3) (p2 -ᵥ p3)<VAR>hpi : InnerProductGeometry.angle (p2 -ᵥ p1) (p3 -ᵥ p1) ≠ π<GOAL>‖p1 -ᵥ p2‖ = ‖p1 -ᵥ p3‖
<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>p1 p2 p3 : P<VAR>h : InnerProductGeometry.angle (p1 -ᵥ p2) (p3 -ᵥ p2) = InnerProductGeometry.angle (p1 -ᵥ p3) (p2 -ᵥ p3)<VAR>hpi : InnerProductGeometry.angle (p1 -ᵥ p2) (p1 -ᵥ p3) ≠ π<GOAL>‖p1 -ᵥ p2‖ = ‖p1 -ᵥ p3‖
<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>p1 p2 p3 : P<VAR>h : InnerProductGeometry.angle (p1 -ᵥ p2) (p1 -ᵥ p2 - (p1 -ᵥ p3)) = InnerProductGeometry.angle (p1 -ᵥ p3) (p1 -ᵥ p3 - (p1 -ᵥ p2))<VAR>hpi : InnerProductGeometry.angle (p1 -ᵥ p2) (p1 -ᵥ p3) ≠ π<GOAL>‖p1 -ᵥ p2‖ = ‖p1 -ᵥ p3‖
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n ν : ℕ<VAR>h : ν ≤ n<GOAL>eval 1 ((⇑derivative)^[n - ν] (bernsteinPolynomial R n ν)) = (-1) ^ (n - ν) * eval (↑ν + 1) (ascPochhammer R (n - ν))
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n ν : ℕ<VAR>h : ν ≤ n<GOAL>eval 1 ((⇑derivative)^[n - ν] ((bernsteinPolynomial R n (n - ν)).comp (1 - X))) = (-1) ^ (n - ν) * eval (↑ν + 1) (ascPochhammer R (n - ν))
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n ν : ℕ<VAR>h : ν ≤ n<GOAL>(-1) ^ (n - ν) * eval (↑(n - (n - ν - 1))) (ascPochhammer R (n - ν)) = (-1) ^ (n - ν) * eval (↑ν + 1) (ascPochhammer R (n - ν))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizedGCDMonoid α<VAR>s s₁ s₂ : Finset β<VAR>f : β → α<VAR>inst✝ : DecidableEq β<VAR>b : β<VAR>h : b ∉ s<GOAL>(insert b s).lcm f = GCDMonoid.lcm (f b) (s.lcm f)
<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>hl : l.HasBasis p s<VAR>q : α → Prop<GOAL>(∃ᶠ (x : α) in l, q x) ↔ ∀ (i : ι), p i → ∃ x ∈ s i, q x
<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>hl : l.HasBasis p s<VAR>q : α → Prop<GOAL>(¬∃ i, p i ∧ ∀ ⦃x : α⦄, x ∈ s i → ¬q x) ↔ ∀ (i : ι), p i → ∃ x ∈ s i, q x