ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>M : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} M<VAR>inst✝ : MonoidalCategory M<VAR>F : MonoidalFunctor M (C ⥤ C)<VAR>m₁ m₂ m₃ : M<VAR>X : C<VAR>this : (F.μ m₁ m₂ ▷ F.obj m₃ ≫ F.μ (m₁ ⊗ m₂) m₃ ≫ F.map (α_ m₁ m₂ m₃).hom).app X = ((α_ (F.obj m₁) (F.obj m₂) (F.obj m₃)).hom ≫ F.obj m₁ ◁ F.μ m₂ m₃ ≫ F.μ m₁ (m₂ ⊗ m₃)).app X<GOAL>(F.obj m₃).map ((F.μ m₁ m₂).app X) ≫ (F.μ (m₁ ⊗ m₂) m₃).app X ≫ (F.map (α_ m₁ m₂ m₃).hom).app X = (F.μ m₂ m₃).app ((F.obj m₁).obj X) ≫ (F.μ m₁ (m₂ ⊗ m₃)).app X
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁵ : EMetricSpace X<VAR>inst✝⁴ : EMetricSpace Y<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : BorelSpace X<VAR>inst✝¹ : MeasurableSpace Y<VAR>inst✝ : BorelSpace Y<VAR>C r : ℝ≥0<VAR>f : X → Y<VAR>s t : Set X<VAR>h : HolderOnWith C r f s<VAR>hr : 0 < r<VAR>d : ℝ<VAR>hd : 0 ≤ d<GOAL>μH[d] (f '' s) ≤ ↑C ^ d * μH[↑r * d] s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁵ : EMetricSpace X<VAR>inst✝⁴ : EMetricSpace Y<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : BorelSpace X<VAR>inst✝¹ : MeasurableSpace Y<VAR>inst✝ : BorelSpace Y<VAR>r : ℝ≥0<VAR>f : X → Y<VAR>s t : Set X<VAR>hr : 0 < r<VAR>d : ℝ<VAR>hd : 0 ≤ d<VAR>h : HolderOnWith 0 r f s<GOAL>μH[d] (f '' s) ≤ ↑0 ^ d * μH[↑r * d] s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁵ : EMetricSpace X<VAR>inst✝⁴ : EMetricSpace Y<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : BorelSpace X<VAR>inst✝¹ : MeasurableSpace Y<VAR>inst✝ : BorelSpace Y<VAR>C r : ℝ≥0<VAR>f : X → Y<VAR>s t : Set X<VAR>h : HolderOnWith C r f s<VAR>hr : 0 < r<VAR>d : ℝ<VAR>hd : 0 ≤ d<VAR>hC0 : 0 < C<GOAL>μH[d] (f '' s) ≤ ↑C ^ d * μH[↑r * d] s
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>r : ℕ<VAR>h𝒜 : Set.Sized r ↑𝒜<VAR>i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)<VAR>s : Finset α<VAR>hs : s ∈ ∂ 𝒜<GOAL>(bipartiteAbove (fun x x_1 => x ⊆ x_1) 𝒜 s).card ≤ Fintype.card α - r + 1
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>r : ℕ<VAR>h𝒜 : Set.Sized r ↑𝒜<VAR>i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)<VAR>s : Finset α<VAR>hs : s ∈ ∂ 𝒜<GOAL>(bipartiteAbove (fun x x_1 => x ⊆ x_1) 𝒜 s).card ≤ Fintype.card α - (r - 1)
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>r : ℕ<VAR>h𝒜 : Set.Sized r ↑𝒜<VAR>i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)<VAR>s : Finset α<VAR>hs : s ∈ ∂ 𝒜<GOAL>(bipartiteAbove (fun x x_1 => x ⊆ x_1) 𝒜 s).card ≤ (image (fun a => insert a s) sᶜ).card
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>r : ℕ<VAR>h𝒜 : Set.Sized r ↑𝒜<VAR>i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)<VAR>s : Finset α<VAR>hs : s ∈ ∂ 𝒜<VAR>t : Finset α<VAR>ht : t ∈ bipartiteAbove (fun x x_1 => x ⊆ x_1) 𝒜 s<GOAL>t ∈ image (fun a => insert a s) sᶜ
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>r : ℕ<VAR>h𝒜 : Set.Sized r ↑𝒜<VAR>i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)<VAR>s : Finset α<VAR>hs : s ∈ ∂ 𝒜<VAR>t : Finset α<VAR>ht : t ∈ 𝒜 ∧ s ⊆ t<GOAL>t ∈ image (fun a => insert a s) sᶜ
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>r : ℕ<VAR>h𝒜 : Set.Sized r ↑𝒜<VAR>i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)<VAR>s : Finset α<VAR>hs : s ∈ ∂ 𝒜<VAR>t : Finset α<VAR>ht : t ∈ 𝒜 ∧ s ⊆ t<VAR>this : ∅ ∉ 𝒜<GOAL>t ∈ image (fun a => insert a s) sᶜ
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>r : ℕ<VAR>h𝒜 : Set.Sized r ↑𝒜<VAR>i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)<VAR>s : Finset α<VAR>hs : s ∈ ∂ 𝒜<VAR>t : Finset α<VAR>ht : t ∈ 𝒜 ∧ s ⊆ t<VAR>this : ∅ ∉ 𝒜<VAR>h : ∃ a ∉ s, insert a s = t<GOAL>t ∈ image (fun a => insert a s) sᶜ
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>r : ℕ<VAR>h𝒜 : Set.Sized r ↑𝒜<VAR>i : DecidableRel fun x x_1 => x ⊆ x_1 := fun x x_1 => Classical.dec ((fun x x_2 => x ⊆ x_2) x x_1)<VAR>s : Finset α<VAR>hs : s ∈ ∂ 𝒜<VAR>this : ∅ ∉ 𝒜<VAR>a : α<VAR>ha : a ∉ s<VAR>ht : insert a s ∈ 𝒜 ∧ s ⊆ insert a s<GOAL>insert a s ∈ image (fun a => insert a s) sᶜ
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>t u : Multiset α<VAR>a b : α<GOAL>∀ {s : Multiset α}, s - t ≤ u ↔ s ≤ u + t
<VAR>α : Type u<VAR>β : Type v<VAR>l : List α<VAR>k : Nat<VAR>hk : k < l.length<VAR>l' : List α<GOAL>(l ++ l').eraseIdx k = l.eraseIdx k ++ l'
<VAR>α : Type u<VAR>β : Type v<VAR>l : List α<VAR>k : Nat<VAR>hk : k < l.length<VAR>l' : List α<GOAL>k + 1 ≤ l.length
<VAR>α : Type u<VAR>β : Type v<VAR>l : List α<VAR>k : Nat<VAR>hk : k < l.length<VAR>l' : List α<GOAL>k ≤ l.length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝ : AddGroup α<VAR>h : Periodic f c<GOAL>Periodic f (-c)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v, u₁} C<VAR>C' : Type u₂<VAR>inst✝ : Category.{v, u₂} C'<VAR>D : GlueData C<VAR>i j : D.J<GOAL>D.t' i j i = pullback.fst (D.f i j) (D.f i i) ≫ D.t i j ≫ inv (pullback.snd (D.f j i) (D.f j i))
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v, u₁} C<VAR>C' : Type u₂<VAR>inst✝ : Category.{v, u₂} C'<VAR>D : GlueData C<VAR>i j : D.J<GOAL>D.t' i j i = (D.t' i j i ≫ pullback.snd (D.f j i) (D.f j i)) ≫ inv (pullback.snd (D.f j i) (D.f j i))
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z w : K<VAR>x : ℝ<GOAL>0 ≤ ↑x ↔ 0 ≤ x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹⁰ : LinearOrderedCommRing 𝕜<VAR>inst✝⁹ : LinearOrderedCommRing E<VAR>inst✝⁸ : LinearOrderedAddCommGroup F<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜 F<VAR>inst✝⁵ : Module E F<VAR>inst✝⁴ : IsScalarTower 𝕜 E F<VAR>inst✝³ : SMulCommClass 𝕜 E F<VAR>inst✝² : OrderedSMul 𝕜 E<VAR>inst✝¹ : OrderedSMul 𝕜 F<VAR>inst✝ : OrderedSMul E F<VAR>s : Set 𝕜<VAR>f : 𝕜 → E<VAR>g : 𝕜 → F<VAR>hf : ConvexOn 𝕜 s f<VAR>hg : ConvexOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → f x ≤ 0<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → g x ≤ 0<VAR>hfg : AntivaryOn f g s<GOAL>ConcaveOn 𝕜 s (f • g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹⁰ : LinearOrderedCommRing 𝕜<VAR>inst✝⁹ : LinearOrderedCommRing E<VAR>inst✝⁸ : LinearOrderedAddCommGroup F<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜 F<VAR>inst✝⁵ : Module E F<VAR>inst✝⁴ : IsScalarTower 𝕜 E F<VAR>inst✝³ : SMulCommClass 𝕜 E F<VAR>inst✝² : OrderedSMul 𝕜 E<VAR>inst✝¹ : OrderedSMul 𝕜 F<VAR>inst✝ : OrderedSMul E F<VAR>s : Set 𝕜<VAR>f : 𝕜 → E<VAR>g : 𝕜 → F<VAR>hf : ConvexOn 𝕜 s f<VAR>hg : ConvexOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → f x ≤ 0<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → g x ≤ 0<VAR>hfg : AntivaryOn f g s<GOAL>ConcaveOn 𝕜 s (-f • -g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>f g : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : Zero β<VAR>m0 : MeasurableSpace α<VAR>hf : StronglyMeasurable f<VAR>μ : Measure α<VAR>inst✝ : SigmaFinite μ<GOAL>SigmaFinite (μ.restrict univ)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : OrderedAddCommMonoid α<VAR>inst✝² : OrderedAddCommMonoid β<VAR>inst✝¹ : SMulZeroClass α β<VAR>inst✝ : FloorDiv α β<VAR>f : ι →₀ β<VAR>a : α<GOAL>(f ⌊/⌋ a).support ⊆ f.support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ s₁ s₂ t t₁ t₂ u v : Finset α<VAR>a✝ b a : α<VAR>s : Finset α<VAR>h : a ∉ s<GOAL>s ∩ {a} = ∅
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f✝ : R →+* S<VAR>x : B<VAR>f : R[X]<VAR>hfm : f.Monic<VAR>hfx : eval₂ (algebraMap R B) x f = 0<GOAL>span R ↑(Finset.image (fun x_1 => x ^ x_1) (Finset.range f.natDegree)) = Subalgebra.toSubmodule (Algebra.adjoin R {x})
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : SeminormedRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : SMul 𝕜 E<VAR>p✝ : Seminorm 𝕜 E<VAR>x✝¹ y : E<VAR>r✝ : ℝ<VAR>p : Seminorm 𝕜 E<VAR>c : ℝ≥0<VAR>hc : 0 < c<VAR>r : ℝ<VAR>x x✝ : E<GOAL>x✝ ∈ (c • p).ball x r ↔ x✝ ∈ p.ball x (r / ↑c)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X✝ Y✝ Z✝¹ X Y Z✝ : C<VAR>f : X ⟶ Y<VAR>inst✝¹ : Epi f<VAR>g : Y ⟶ Z✝<VAR>inst✝ : Epi g<VAR>Z : C<VAR>a b : Z✝ ⟶ Z<VAR>w : (f ≫ g) ≫ a = (f ≫ g) ≫ b<GOAL>a = b
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X✝ Y✝ Z✝¹ X Y Z✝ : C<VAR>f : X ⟶ Y<VAR>inst✝¹ : Epi f<VAR>g : Y ⟶ Z✝<VAR>inst✝ : Epi g<VAR>Z : C<VAR>a b : Z✝ ⟶ Z<VAR>w : (f ≫ g) ≫ a = (f ≫ g) ≫ b<GOAL>g ≫ a = g ≫ b
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X✝ Y✝ Z✝¹ X Y Z✝ : C<VAR>f : X ⟶ Y<VAR>inst✝¹ : Epi f<VAR>g : Y ⟶ Z✝<VAR>inst✝ : Epi g<VAR>Z : C<VAR>a b : Z✝ ⟶ Z<VAR>w : (f ≫ g) ≫ a = (f ≫ g) ≫ b<GOAL>f ≫ g ≫ a = f ≫ g ≫ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r p q : α → α → Prop<VAR>f g : ι → α<VAR>s t u : Set α<VAR>a b : α<VAR>hr : Symmetric r<GOAL>(insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, a ≠ b → r a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Sort u_5<VAR>f : Filter α<VAR>h : f.IsCountablyGenerated<VAR>p : ι' → Prop<VAR>s : ι' → Set α<VAR>hs : f.HasBasis p s<GOAL>∃ x, (∀ (i : ℕ), p (x i)) ∧ f.HasAntitoneBasis fun i => s (x i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Sort u_5<VAR>f : Filter α<VAR>h : f.IsCountablyGenerated<VAR>p : ι' → Prop<VAR>s : ι' → Set α<VAR>hs : f.HasBasis p s<VAR>x' : ℕ → Set α<VAR>hx' : f = ⨅ i, 𝓟 (x' i)<GOAL>∃ x, (∀ (i : ℕ), p (x i)) ∧ f.HasAntitoneBasis fun i => s (x i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Sort u_5<VAR>f : Filter α<VAR>h : f.IsCountablyGenerated<VAR>p : ι' → Prop<VAR>s : ι' → Set α<VAR>hs : f.HasBasis p s<VAR>x' : ℕ → Set α<VAR>hx' : f = ⨅ i, 𝓟 (x' i)<VAR>this : ∀ (i : ℕ), x' i ∈ f<GOAL>∃ x, (∀ (i : ℕ), p (x i)) ∧ f.HasAntitoneBasis fun i => s (x i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Sort u_5<VAR>f : Filter α<VAR>h : f.IsCountablyGenerated<VAR>p : ι' → Prop<VAR>s : ι' → Set α<VAR>hs : f.HasBasis p s<VAR>x' : ℕ → Set α<VAR>hx' : f = ⨅ i, 𝓟 (x' i)<VAR>this : ∀ (i : ℕ), x' i ∈ f<VAR>x : ℕ → { i // p i } := fun n => Nat.recOn n (hs.index (x' 0) ⋯) fun n xn => hs.index (x' (n + 1) ∩ s ↑xn) ⋯<GOAL>∃ x, (∀ (i : ℕ), p (x i)) ∧ f.HasAntitoneBasis fun i => s (x i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Sort u_5<VAR>f : Filter α<VAR>h : f.IsCountablyGenerated<VAR>p : ι' → Prop<VAR>s : ι' → Set α<VAR>hs : f.HasBasis p s<VAR>x' : ℕ → Set α<VAR>hx' : f = ⨅ i, 𝓟 (x' i)<VAR>this : ∀ (i : ℕ), x' i ∈ f<VAR>x : ℕ → { i // p i } := fun n => Nat.recOn n (hs.index (x' 0) ⋯) fun n xn => hs.index (x' (n + 1) ∩ s ↑xn) ⋯<VAR>x_anti : Antitone fun i => s ↑(x i)<GOAL>∃ x, (∀ (i : ℕ), p (x i)) ∧ f.HasAntitoneBasis fun i => s (x i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Sort u_5<VAR>f : Filter α<VAR>h : f.IsCountablyGenerated<VAR>p : ι' → Prop<VAR>s : ι' → Set α<VAR>hs : f.HasBasis p s<VAR>x' : ℕ → Set α<VAR>hx' : f = ⨅ i, 𝓟 (x' i)<VAR>this : ∀ (i : ℕ), x' i ∈ f<VAR>x : ℕ → { i // p i } := fun n => Nat.recOn n (hs.index (x' 0) ⋯) fun n xn => hs.index (x' (n + 1) ∩ s ↑xn) ⋯<VAR>x_anti : Antitone fun i => s ↑(x i)<VAR>x_subset : ∀ (i : ℕ), s ↑(x i) ⊆ x' i<GOAL>∃ x, (∀ (i : ℕ), p (x i)) ∧ f.HasAntitoneBasis fun i => s (x i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Sort u_5<VAR>f : Filter α<VAR>h : f.IsCountablyGenerated<VAR>p : ι' → Prop<VAR>s : ι' → Set α<VAR>hs : f.HasBasis p s<VAR>x' : ℕ → Set α<VAR>hx' : f = ⨅ i, 𝓟 (x' i)<VAR>this : ∀ (i : ℕ), x' i ∈ f<VAR>x : ℕ → { i // p i } := fun n => Nat.recOn n (hs.index (x' 0) ⋯) fun n xn => hs.index (x' (n + 1) ∩ s ↑xn) ⋯<VAR>x_anti : Antitone fun i => s ↑(x i)<VAR>x_subset : ∀ (i : ℕ), s ↑(x i) ⊆ x' i<GOAL>f.HasAntitoneBasis fun i => s ((fun i => ↑(x i)) i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Sort u_5<VAR>f : Filter α<VAR>h : f.IsCountablyGenerated<VAR>p : ι' → Prop<VAR>s : ι' → Set α<VAR>hs : f.HasBasis p s<VAR>x' : ℕ → Set α<VAR>hx' : f = ⨅ i, 𝓟 (x' i)<VAR>this✝ : ∀ (i : ℕ), x' i ∈ f<VAR>x : ℕ → { i // p i } := fun n => Nat.recOn n (hs.index (x' 0) ⋯) fun n xn => hs.index (x' (n + 1) ∩ s ↑xn) ⋯<VAR>x_anti : Antitone fun i => s ↑(x i)<VAR>x_subset : ∀ (i : ℕ), s ↑(x i) ⊆ x' i<VAR>this : (⨅ i, 𝓟 (s ↑(x i))).HasAntitoneBasis fun i => s ↑(x i)<GOAL>f.HasAntitoneBasis fun i => s ((fun i => ↑(x i)) i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Sort u_5<VAR>f : Filter α<VAR>h : f.IsCountablyGenerated<VAR>p : ι' → Prop<VAR>s : ι' → Set α<VAR>hs : f.HasBasis p s<VAR>x' : ℕ → Set α<VAR>hx' : f = ⨅ i, 𝓟 (x' i)<VAR>this✝ : ∀ (i : ℕ), x' i ∈ f<VAR>x : ℕ → { i // p i } := fun n => Nat.recOn n (hs.index (x' 0) ⋯) fun n xn => hs.index (x' (n + 1) ∩ s ↑xn) ⋯<VAR>x_anti : Antitone fun i => s ↑(x i)<VAR>x_subset : ∀ (i : ℕ), s ↑(x i) ⊆ x' i<VAR>this : (⨅ i, 𝓟 (s ↑(x i))).HasAntitoneBasis fun i => s ↑(x i)<GOAL>f = ⨅ i, 𝓟 (s ↑(x i))
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>x y : α<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>Multiset.Rel Associated (factors (x * y)) (factors x + factors y)
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>x y : α<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>x * y ~ᵤ (factors x + factors y).prod
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>x y : α<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>x * y ~ᵤ (factors x).prod * (factors y).prod
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>l : Filter α✝<VAR>α : ι → Type u_4<VAR>inst✝ : Finite ι<VAR>s : Set ((i : ι) → α i)<GOAL>(sᶜ ∈ Filter.coprodᵢ fun i => cofinite) ↔ sᶜ ∈ cofinite
<VAR>m n i : ℕ<VAR>hi : 2 ≤ i<VAR>m✝ : ℕ<VAR>a✝ : Nat.le 1 m✝<GOAL>i + m✝.succ ! < (i + m✝.succ)!
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>φ : M → N<VAR>ψ : N → M<VAR>h : Function.RightInverse φ ψ<VAR>χ : M → M<VAR>inst✝ : IsId χ<GOAL>ψ ∘ φ = χ
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>β : Type v<VAR>inst✝ : (i : Fin (n + 1)) → Preorder (α i)<VAR>i : Fin (n + 1)<VAR>x : α i<VAR>p : (j : Fin n) → α (i.succAbove j)<VAR>q : (j : Fin (n + 1)) → α j<GOAL>q ≤ i.insertNth x p ↔ q i ≤ x ∧ (fun j => q (i.succAbove j)) ≤ p
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hg : _root_.Embedding g<GOAL>_root_.Embedding (g ∘ f) ↔ _root_.Embedding f
<VAR>S : Type u_1<VAR>R R' : Type u<VAR>M : Type v<VAR>inst✝²⁶ : CommSemiring S<VAR>inst✝²⁵ : Semiring R<VAR>inst✝²⁴ : CommSemiring R'<VAR>inst✝²³ : AddCommMonoid M<VAR>inst✝²² : Algebra S R<VAR>inst✝²¹ : Algebra S R'<VAR>inst✝²⁰ : Module S M<VAR>inst✝¹⁹ : Module R M<VAR>inst✝¹⁸ : Module Rᵐᵒᵖ M<VAR>inst✝¹⁷ : SMulCommClass R Rᵐᵒᵖ M<VAR>inst✝¹⁶ : IsScalarTower S R M<VAR>inst✝¹⁵ : IsScalarTower S Rᵐᵒᵖ M<VAR>inst✝¹⁴ : Module R' M<VAR>inst✝¹³ : Module R'ᵐᵒᵖ M<VAR>inst✝¹² : IsCentralScalar R' M<VAR>inst✝¹¹ : IsScalarTower S R' M<VAR>A : Type u_2<VAR>inst✝¹⁰ : Semiring A<VAR>inst✝⁹ : Algebra S A<VAR>inst✝⁸ : Algebra R' A<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁷ : AddCommMonoid N<VAR>inst✝⁶ : Module R' N<VAR>inst✝⁵ : Module R'ᵐᵒᵖ N<VAR>inst✝⁴ : IsCentralScalar R' N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R' P<VAR>inst✝¹ : Module R'ᵐᵒᵖ P<VAR>inst✝ : IsCentralScalar R' P<VAR>f : M →ₗ[R'] N<VAR>r : R'<GOAL>(map f) (inl r) = inl r
<VAR>X : Type u_1<VAR>inst✝¹ : PseudoMetricSpace X<VAR>inst✝ : IsUltrametricDist X<VAR>x y z : X<VAR>r✝ s r : ℝ<VAR>hr : r ≠ 0<GOAL>IsOpen (sphere x r)
<VAR>X : Type u_1<VAR>inst✝¹ : PseudoMetricSpace X<VAR>inst✝ : IsUltrametricDist X<VAR>x y z : X<VAR>r✝ s r : ℝ<VAR>hr : r ≠ 0<GOAL>IsOpen (closedBall x r ⊓ (ball x r)ᶜ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>s : Sym2 α<VAR>h : ∀ x ∈ s, f x = g x<VAR>y : β<GOAL>y ∈ map f s ↔ y ∈ map g s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>s : Sym2 α<VAR>h : ∀ x ∈ s, f x = g x<VAR>y : β<GOAL>(∃ a ∈ s, f a = y) ↔ ∃ a ∈ s, g a = y
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<GOAL>IsClosed s ↔ ∀ (x : X), (∀ U ∈ 𝓝 x, (U ∩ s).Nonempty) → x ∈ s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s✝ t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ι : Type u_5<VAR>inst✝ : Countable ι<VAR>s : ι → Set X<VAR>hm : ∀ (i : ι), NullMeasurableSet (s i) μ<VAR>hd : Pairwise (AEDisjoint μ on s)<VAR>hfi : IntegrableOn f (⋃ i, s i) μ<GOAL>HasSum (fun n => ∫ (x : X) in s n, f x ∂μ) (∫ (x : X) in ⋃ n, s n, f x ∂μ)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s✝ t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ι : Type u_5<VAR>inst✝ : Countable ι<VAR>s : ι → Set X<VAR>hm : ∀ (i : ι), NullMeasurableSet (s i) μ<VAR>hd : Pairwise (AEDisjoint μ on s)<VAR>hfi : Integrable f (Measure.sum fun i => μ.restrict (s i))<GOAL>HasSum (fun n => ∫ (x : X) in s n, f x ∂μ) (∫ (x : X), f x ∂Measure.sum fun i => μ.restrict (s i))
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁷ : CommRing A<VAR>inst✝¹⁶ : Field K<VAR>inst✝¹⁵ : CommRing B<VAR>inst✝¹⁴ : Field L<VAR>inst✝¹³ : Algebra A K<VAR>inst✝¹² : Algebra B L<VAR>inst✝¹¹ : Algebra A B<VAR>inst✝¹⁰ : Algebra K L<VAR>inst✝⁹ : Algebra A L<VAR>inst✝⁸ : IsScalarTower A K L<VAR>inst✝⁷ : IsScalarTower A B L<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : IsFractionRing A K<VAR>inst✝⁴ : IsIntegralClosure B A L<VAR>inst✝³ : IsFractionRing B L<VAR>inst✝² : FiniteDimensional K L<VAR>inst✝¹ : Algebra.IsSeparable K L<VAR>inst✝ : IsDomain B<VAR>x✝ : L<GOAL>x✝ ∈ ⊥ᵛ ↔ x✝ ∈ ⊤
<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>ι : Type u_5<VAR>κ : Type u_6<VAR>σ : ι → Type u_7<VAR>τ : κ → Type u_8<VAR>inst✝² : (i : ι) → TopologicalSpace (σ i)<VAR>inst✝¹ : (k : κ) → TopologicalSpace (τ k)<VAR>inst✝ : TopologicalSpace X<VAR>f : Sigma σ → X<GOAL>Continuous f ↔ ∀ (i : ι), Continuous fun a => f ⟨i, a⟩
<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>ι : Type u_5<VAR>κ : Type u_6<VAR>σ : ι → Type u_7<VAR>τ : κ → Type u_8<VAR>inst✝² : (i : ι) → TopologicalSpace (σ i)<VAR>inst✝¹ : (k : κ) → TopologicalSpace (τ k)<VAR>inst✝ : TopologicalSpace X<VAR>f : Sigma σ → X<GOAL>(∀ (i : ι), Continuous f) ↔ ∀ (i : ι), Continuous fun a => f ⟨i, a⟩
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<VAR>r : ℝ<VAR>hr : r < 0<GOAL>angle x (r • y) = angle x (-y)
<VAR>A : Type u_1<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : Algebra ℝ A<VAR>inst✝² : TopologicalSpace A<VAR>inst✝¹ : T2Space A<VAR>s : Set ℝ<VAR>inst✝ : CompactSpace ↑s<VAR>φ ψ : C(↑s, ℝ) →ₐ[ℝ] A<VAR>hφ : Continuous ⇑φ<VAR>hψ : Continuous ⇑ψ<VAR>h : φ ((toContinuousMapOnAlgHom s) X) = ψ ((toContinuousMapOnAlgHom s) X)<GOAL>φ = ψ
<VAR>A : Type u_1<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : Algebra ℝ A<VAR>inst✝² : TopologicalSpace A<VAR>inst✝¹ : T2Space A<VAR>s : Set ℝ<VAR>inst✝ : CompactSpace ↑s<VAR>φ ψ : C(↑s, ℝ) →ₐ[ℝ] A<VAR>hφ : Continuous ⇑φ<VAR>hψ : Continuous ⇑ψ<VAR>h : φ ((toContinuousMapOnAlgHom s) X) = ψ ((toContinuousMapOnAlgHom s) X)<GOAL>⊤ ≤ AlgHom.equalizer φ ψ
<VAR>A : Type u_1<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : Algebra ℝ A<VAR>inst✝² : TopologicalSpace A<VAR>inst✝¹ : T2Space A<VAR>s : Set ℝ<VAR>inst✝ : CompactSpace ↑s<VAR>φ ψ : C(↑s, ℝ) →ₐ[ℝ] A<VAR>hφ : Continuous ⇑φ<VAR>hψ : Continuous ⇑ψ<VAR>h : φ ((toContinuousMapOnAlgHom s) X) = ψ ((toContinuousMapOnAlgHom s) X)<GOAL>(polynomialFunctions s).topologicalClosure ≤ AlgHom.equalizer φ ψ
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : GroupWithZero G₀<VAR>a✝ b c a : G₀<GOAL>a * a / a = a
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f : E → F<VAR>hf : ContDiffAt 𝕜 n f x<GOAL>ContDiffAt 𝕜 n (fun x => -f x) x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f : E → F<VAR>hf : ContDiffWithinAt 𝕜 n f univ x<GOAL>ContDiffWithinAt 𝕜 n (fun x => -f x) univ x
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>h : b ≤ a<GOAL>max a b = a
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>h : b ≤ a<GOAL>a = max a b
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>h : b ≤ a<GOAL>∀ {d : α}, a ≤ d → b ≤ d → a ≤ d
<VAR>R : Type u_1<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Nontrivial R<VAR>n : ℕ<GOAL>(X ^ n).order = ↑n
<VAR>R : Type u_1<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Nontrivial R<VAR>n : ℕ<GOAL>1 ≠ 0
<VAR>α : Type u_1<VAR>inst✝ : OrderedRing α<VAR>a : α<GOAL>Pairwise (Disjoint on fun n => Ioc (a + ↑n) (a + ↑n + 1))
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : HasKernel f<VAR>F : MonoFactorisation f<GOAL>kernel.ι f ≫ F.e = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>r' : β → β → Prop<VAR>s t : Set α<VAR>a✝ b✝ : α<VAR>inst✝ : IsTrichotomous α r<VAR>h : IsAntichain r s<VAR>a : α<VAR>ha : a ∈ s<VAR>b : α<VAR>hb : b ∈ s<GOAL>a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>r' : β → β → Prop<VAR>s t : Set α<VAR>a✝ b✝ : α<VAR>inst✝ : IsTrichotomous α r<VAR>h : IsAntichain r s<VAR>a : α<VAR>ha : a ∈ s<VAR>b : α<VAR>hb : b ∈ s<VAR>hab : r a b<GOAL>a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>r' : β → β → Prop<VAR>s t : Set α<VAR>a✝ b✝ : α<VAR>inst✝ : IsTrichotomous α r<VAR>h : IsAntichain r s<VAR>a : α<VAR>ha : a ∈ s<VAR>b : α<VAR>hb : b ∈ s<VAR>hab : a = b<GOAL>a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>r' : β → β → Prop<VAR>s t : Set α<VAR>a✝ b✝ : α<VAR>inst✝ : IsTrichotomous α r<VAR>h : IsAntichain r s<VAR>a : α<VAR>ha : a ∈ s<VAR>b : α<VAR>hb : b ∈ s<VAR>hab : r b a<GOAL>a = b