ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>inst✝ : DiscreteTopology X<VAR>hs : IsLindelof s<VAR>this : ∀ (x : X), {x} ∈ 𝓝 x<GOAL>s.Countable
<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>inst✝ : DiscreteTopology X<VAR>hs : IsLindelof s<VAR>this : ∀ (x : X), {x} ∈ 𝓝 x<VAR>t : Set X<VAR>ht : t.Countable<VAR>left✝ : ∀ x ∈ t, x ∈ s<VAR>hssubt : s ⊆ ⋃ x ∈ t, {x}<GOAL>s.Countable
<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>inst✝ : DiscreteTopology X<VAR>hs : IsLindelof s<VAR>this : ∀ (x : X), {x} ∈ 𝓝 x<VAR>t : Set X<VAR>ht : t.Countable<VAR>left✝ : ∀ x ∈ t, x ∈ s<VAR>hssubt : s ⊆ t<GOAL>s.Countable
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Finite α<VAR>this : Fintype α<GOAL>1 < Nat.card α ↔ Nontrivial α
<VAR>R : Type u_1<VAR>inst✝³ : Semiring R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddCommMonoid X<VAR>inst✝ : Module R X<VAR>n : ℕ<VAR>x : OreLocalization S X<VAR>inst : Module ℕ (OreLocalization S X) := instModuleOfIsScalarTower<GOAL>n • x = n • x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>s✝ t✝ u : Set H<VAR>x✝ : H<VAR>hG : G.LocalInvariantProp G' P<VAR>s t : Set H<VAR>x : H<VAR>f : H → H'<VAR>hu : s =ᶠ[𝓝 x] t<GOAL>P f s x ↔ P f t x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>s✝ t✝ u : Set H<VAR>x✝ : H<VAR>hG : G.LocalInvariantProp G' P<VAR>s t : Set H<VAR>x : H<VAR>f : H → H'<VAR>hu : s =ᶠ[𝓝 x] t<VAR>o : Set H<VAR>host : o ⊆ {x | (fun x => x ∈ s ↔ x ∈ t) x}<VAR>ho : IsOpen o<VAR>hxo : x ∈ o<GOAL>P f s x ↔ P f t x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>s✝ t✝ u : Set H<VAR>x✝ : H<VAR>hG : G.LocalInvariantProp G' P<VAR>s t : Set H<VAR>x : H<VAR>f : H → H'<VAR>hu : s =ᶠ[𝓝 x] t<VAR>o : Set H<VAR>ho : IsOpen o<VAR>hxo : x ∈ o<VAR>host : s ∩ o = t ∩ o<GOAL>P f s x ↔ P f t x
<VAR>V : Type u_1<VAR>G G' : SimpleGraph V<VAR>M M' : G.Subgraph<VAR>v w : V<VAR>h : G.Adj v w<VAR>v✝ : V<VAR>hv : v✝ ∈ (G.subgraphOfAdj h).verts<GOAL>∃! w_1, (G.subgraphOfAdj h).Adj v✝ w_1
<VAR>V : Type u_1<VAR>G G' : SimpleGraph V<VAR>M M' : G.Subgraph<VAR>v w : V<VAR>h : G.Adj v w<VAR>v✝ : V<VAR>hv : v✝ = v ∨ v✝ = w<GOAL>∃! w_1, (G.subgraphOfAdj h).Adj v✝ w_1
<VAR>K : Type u<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>p : FractionRing K[X]<VAR>h : { toFractionRing := p } ≠ 0<GOAL>{ toFractionRing := p } * { toFractionRing := p }⁻¹ = 1
<VAR>K : Type u<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>p : FractionRing K[X]<VAR>h : { toFractionRing := p } ≠ 0<VAR>this : p ≠ 0<GOAL>{ toFractionRing := p } * { toFractionRing := p }⁻¹ = 1
<VAR>ι : Type u<VAR>f : ι → Scheme<VAR>i j : ι<VAR>h : i ≠ j<VAR>U : (∐ f).Opens<VAR>hU : U ≤ Scheme.Hom.opensRange (Sigma.ι f i)<VAR>hU' : U ≤ Scheme.Hom.opensRange (Sigma.ι f j)<VAR>x : ↑↑(f i).toPresheafedSpace<VAR>hx : (Sigma.ι f i).val.base x ∈ ↑U<VAR>y : ↑↑(f j).toPresheafedSpace<VAR>hy : (Sigma.ι f j).val.base y = (Sigma.ι f i).val.base x<GOAL>(Sigma.ι f i).val.base x ∈ ↑⊥
<VAR>ι : Type u<VAR>f : ι → Scheme<VAR>i : ι<VAR>U : (∐ f).Opens<VAR>hU : U ≤ Scheme.Hom.opensRange (Sigma.ι f i)<VAR>x : ↑↑(f i).toPresheafedSpace<VAR>hx : (Sigma.ι f i).val.base x ∈ ↑U<VAR>h : i ≠ i<VAR>hU' : U ≤ Scheme.Hom.opensRange (Sigma.ι f i)<VAR>hy : (Sigma.ι f i).val.base x = (Sigma.ι f i).val.base x<GOAL>(Sigma.ι f i).val.base x ∈ ↑⊥
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝ : Mul M<VAR>S : ι → Subsemigroup M<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : M<GOAL>x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝ : Mul M<VAR>S : ι → Subsemigroup M<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : M<GOAL>x ∈ ⨆ i, S i → ∃ i, x ∈ S i
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝ : Mul M<VAR>S : ι → Subsemigroup M<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : M<GOAL>x ∈ closure (⋃ i, ↑(S i)) → ∃ i, x ∈ S i
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝ : Mul M<VAR>S : ι → Subsemigroup M<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : M<VAR>hx : x ∈ closure (⋃ i, ↑(S i))<GOAL>∀ (x y : M), (∃ i, x ∈ S i) → (∃ i, y ∈ S i) → ∃ i, x * y ∈ S i
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝ : Mul M<VAR>S : ι → Subsemigroup M<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x✝ : M<VAR>hx : x✝ ∈ closure (⋃ i, ↑(S i))<VAR>x y : M<VAR>i : ι<VAR>hi : x ∈ S i<VAR>j : ι<VAR>hj : y ∈ S j<VAR>k : ι<VAR>hki : S i ≤ S k<VAR>hkj : S j ≤ S k<GOAL>∃ i, x * y ∈ S i
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → Option β<VAR>l : List α<GOAL>filterMap f l = l.bind fun a => (f a).toList
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → Option β<VAR>a : α<VAR>l : List α<VAR>ih : filterMap f l = l.bind fun a => (f a).toList<GOAL>(match f a with | none => filterMap f l | some b => b :: filterMap f l) = (f a).toList ++ l.bind fun a => (f a).toList
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.63038, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ✝ : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>φ : S₁ ⟶ S₂<VAR>hf₁ : S₁.f = 0<VAR>c₁ : KernelFork S₁.g<VAR>hc₁ : IsLimit c₁<VAR>hf₂ : S₂.f = 0<VAR>c₂ : KernelFork S₂.g<VAR>hc₂ : IsLimit c₂<VAR>f : c₁.pt ⟶ c₂.pt<VAR>comm : Fork.ι c₁ ≫ φ.τ₂ = f ≫ Fork.ι c₂<GOAL>φ.τ₂ ≫ (RightHomologyData.ofIsLimitKernelFork S₂ hf₂ c₂ hc₂).g' = (RightHomologyData.ofIsLimitKernelFork S₁ hf₁ c₁ hc₁).g' ≫ φ.τ₃
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>g : E → F<VAR>c : ℝ≥0<VAR>𝕜 : Type u_5<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : Fact (1 ≤ p)<VAR>L L' : E →L[𝕜] F<VAR>f : ↥(Lp E p μ)<GOAL>(compLpL p μ (L + L')) f = (compLpL p μ L + compLpL p μ L') f
<VAR>θ : Angle<GOAL>θ.sin = 0 ↔ θ = 0 ∨ θ = ↑π
<VAR>θ : Angle<GOAL>θ.sin = sin 0 ↔ θ = 0 ∨ θ = ↑π
<VAR>θ : Angle<GOAL>θ = 0 ∨ θ + 0 = ↑π ↔ θ = 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>n : ℕ<VAR>s : Simplex ℝ P (n + 2)<VAR>i₁ i₂ : Fin (n + 3)<GOAL>(s.mongePlane i₁ i₂).direction = (Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂})ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>f : X → Y<VAR>s : Set X<VAR>x : X<VAR>y : Y<GOAL>Continuous f ↔ ∀ (x : X) (g : Ultrafilter X), ↑g ≤ 𝓝 x → Tendsto f (↑g) (𝓝 (f x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteSemilatticeInf α<VAR>s t : Set α<VAR>b : α<GOAL>IsGLB s (sInf s)
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z : ℝ≥0∞<VAR>h1 : y ≠ 0<VAR>h2 : y ≠ ⊤<GOAL>x * y⁻¹ ≤ z ↔ x ≤ z * y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g✝ : ι → α<VAR>g : α → β<VAR>hf : TendstoUniformlyOn F f p s<VAR>hfg : EqOn f g s<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<GOAL>∀ᶠ (n : ι) in p, ∀ x ∈ s, (g x, F n x) ∈ u
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>X : Cᵒᵖ<VAR>hX : Limits.IsInitial X<VAR>M : PresheafOfModules R<VAR>c₁ c₂ : Cᵒᵖ<VAR>f : c₁ ⟶ c₂<VAR>r : ↑(R.obj X)<VAR>m : ↑((ModuleCat.restrictScalars (R.map (hX.to c₁))).obj (M.obj c₁))<GOAL>{ toFun := fun x => (M.presheaf.map f) x, map_add' := ⋯ }.toFun (r • m) = (RingHom.id ↑(R.obj X)) r • { toFun := fun x => (M.presheaf.map f) x, map_add' := ⋯ }.toFun m
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>X : Cᵒᵖ<VAR>hX : Limits.IsInitial X<VAR>M : PresheafOfModules R<VAR>c₁ c₂ : Cᵒᵖ<VAR>f : c₁ ⟶ c₂<VAR>r : ↑(R.obj X)<VAR>m : ↑((ModuleCat.restrictScalars (R.map (hX.to c₁))).obj (M.obj c₁))<GOAL>(R.map f) ((R.map (hX.to c₁)) r) • (M.presheaf.map f) m = r • (M.presheaf.map f) m
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>X : Cᵒᵖ<VAR>hX : Limits.IsInitial X<VAR>M : PresheafOfModules R<VAR>c₁ c₂ : Cᵒᵖ<VAR>f : c₁ ⟶ c₂<VAR>r : ↑(R.obj X)<VAR>m : ↑((ModuleCat.restrictScalars (R.map (hX.to c₁))).obj (M.obj c₁))<GOAL>(R.map (hX.to c₁ ≫ f)) r • (M.presheaf.map f) m = r • (M.presheaf.map f) m
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>X : Cᵒᵖ<VAR>hX : Limits.IsInitial X<VAR>M : PresheafOfModules R<VAR>c₁ c₂ : Cᵒᵖ<VAR>f : c₁ ⟶ c₂<VAR>r : ↑(R.obj X)<VAR>m : ↑((ModuleCat.restrictScalars (R.map (hX.to c₁))).obj (M.obj c₁))<GOAL>hX.to c₁ ≫ f = hX.to c₂
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>X : Cᵒᵖ<VAR>hX : Limits.IsInitial X<VAR>M : PresheafOfModules R<VAR>c : Cᵒᵖ<VAR>x✝ : ↑({ obj := fun c => (ModuleCat.restrictScalars (R.map (hX.to c))).obj (M.obj c), map := fun {c₁ c₂} f => { toFun := fun x => (M.presheaf.map f) x, map_add' := ⋯, map_smul' := ⋯ } }.obj c)<GOAL>({ obj := fun c => (ModuleCat.restrictScalars (R.map (hX.to c))).obj (M.obj c), map := fun {c₁ c₂} f => { toFun := fun x => (M.presheaf.map f) x, map_add' := ⋯, map_smul' := ⋯ } }.map (𝟙 c)) x✝ = (𝟙 ({ obj := fun c => (ModuleCat.restrictScalars (R.map (hX.to c))).obj (M.obj c), map := fun {c₁ c₂} f => { toFun := fun x => (M.presheaf.map f) x, map_add' := ⋯, map_smul' := ⋯ } }.obj c)) x✝
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>X : Cᵒᵖ<VAR>hX : Limits.IsInitial X<VAR>M : PresheafOfModules R<VAR>c : Cᵒᵖ<VAR>x✝ : ↑({ obj := fun c => (ModuleCat.restrictScalars (R.map (hX.to c))).obj (M.obj c), map := fun {c₁ c₂} f => { toFun := fun x => (M.presheaf.map f) x, map_add' := ⋯, map_smul' := ⋯ } }.obj c)<GOAL>{ toFun := fun x => (𝟙 (M.presheaf.obj c)) x, map_add' := ⋯, map_smul' := ⋯ } x✝ = (𝟙 ((ModuleCat.restrictScalars (R.map (hX.to c))).obj (M.obj c))) x✝
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>X : Cᵒᵖ<VAR>hX : Limits.IsInitial X<VAR>M : PresheafOfModules R<VAR>c₁ c₂ c₃ : Cᵒᵖ<VAR>f : c₁ ⟶ c₂<VAR>g : c₂ ⟶ c₃<VAR>x : ↑({ obj := fun c => (ModuleCat.restrictScalars (R.map (hX.to c))).obj (M.obj c), map := fun {c₁ c₂} f => { toFun := fun x => (M.presheaf.map f) x, map_add' := ⋯, map_smul' := ⋯ } }.obj c₁)<GOAL>({ obj := fun c => (ModuleCat.restrictScalars (R.map (hX.to c))).obj (M.obj c), map := fun {c₁ c₂} f => { toFun := fun x => (M.presheaf.map f) x, map_add' := ⋯, map_smul' := ⋯ } }.map (f ≫ g)) x = ({ obj := fun c => (ModuleCat.restrictScalars (R.map (hX.to c))).obj (M.obj c), map := fun {c₁ c₂} f => { toFun := fun x => (M.presheaf.map f) x, map_add' := ⋯, map_smul' := ⋯ } }.map f ≫ { obj := fun c => (ModuleCat.restrictScalars (R.map (hX.to c))).obj (M.obj c), map := fun {c₁ c₂} f => { toFun := fun x => (M.presheaf.map f) x, map_add' := ⋯, map_smul' := ⋯ } }.map g) x
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>X : Cᵒᵖ<VAR>hX : Limits.IsInitial X<VAR>M : PresheafOfModules R<VAR>c₁ c₂ c₃ : Cᵒᵖ<VAR>f : c₁ ⟶ c₂<VAR>g : c₂ ⟶ c₃<VAR>x : ↑({ obj := fun c => (ModuleCat.restrictScalars (R.map (hX.to c))).obj (M.obj c), map := fun {c₁ c₂} f => { toFun := fun x => (M.presheaf.map f) x, map_add' := ⋯, map_smul' := ⋯ } }.obj c₁)<GOAL>{ toFun := fun x => (M.presheaf.map f ≫ M.presheaf.map g) x, map_add' := ⋯, map_smul' := ⋯ } x = ({ toFun := fun x => (M.presheaf.map f) x, map_add' := ⋯, map_smul' := ⋯ } ≫ { toFun := fun x => (M.presheaf.map g) x, map_add' := ⋯, map_smul' := ⋯ }) x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>inst✝ : OrderedAddCommGroup β<VAR>f g : α → β<VAR>a : α<VAR>s : Set α<VAR>l : Filter α<VAR>hf : IsMaxFilter f l a<VAR>hg : IsMinFilter g l a<GOAL>IsMaxFilter (fun x => f x - g x) l a
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>f g : ArithmeticFunction R<VAR>x✝ : ℕ<GOAL>(f.pmul g) x✝ = (g.pmul f) x✝
<VAR>n✝ m n : ℕ<VAR>h : m ∈ n.properDivisors<GOAL>1 < n / m
<VAR>n✝ m n : ℕ<VAR>h : m ∈ n.properDivisors<VAR>h_dvd : m ∣ n<VAR>h_lt : m < n<GOAL>1 < n / m
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Mul α<VAR>s s₁ s₂ t t₁ t₂ : Finset α<GOAL>Eₘ[s, t] = 0 ↔ s = ∅ ∨ t = ∅
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>x : E<VAR>s : Set E<VAR>x✝ : ℝ<GOAL>logDeriv sin x✝ = x✝.cot
<VAR>p q : ℤ[X]<VAR>h : p * p.mirror = q * q.mirror<GOAL>p.IsUnitTrinomial ↔ q.IsUnitTrinomial
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NontriviallyNormedField 𝕜<VAR>inst✝ : NormedAlgebra 𝕜 ℂ<VAR>n : ℕ<GOAL>deriv^[n + 1] cexp = cexp
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : MeasurableSpace γ<VAR>inst✝¹ : MeasurableSpace δ<VAR>μa : Measure α<VAR>μb : Measure β<VAR>μc : Measure γ<VAR>μd : Measure δ<VAR>μ : Measure α<VAR>f : α → α<VAR>s : Set α<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : MeasurePreserving f μ μ<VAR>hs : NullMeasurableSet s μ<VAR>hs' : μ s ≠ 0<GOAL>∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[m] x ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : MeasurableSpace γ<VAR>inst✝¹ : MeasurableSpace δ<VAR>μa : Measure α<VAR>μb : Measure β<VAR>μc : Measure γ<VAR>μd : Measure δ<VAR>μ : Measure α<VAR>f : α → α<VAR>s : Set α<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : MeasurePreserving f μ μ<VAR>hs : NullMeasurableSet s μ<VAR>hs' : μ s ≠ 0<VAR>N : ℕ<VAR>hN : μ univ < ↑N * μ s<GOAL>∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[m] x ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : MeasurableSpace γ<VAR>inst✝¹ : MeasurableSpace δ<VAR>μa : Measure α<VAR>μb : Measure β<VAR>μc : Measure γ<VAR>μd : Measure δ<VAR>μ : Measure α<VAR>f : α → α<VAR>s : Set α<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : MeasurePreserving f μ μ<VAR>hs : NullMeasurableSet s μ<VAR>hs' : μ s ≠ 0<VAR>N : ℕ<VAR>hN : μ univ < ↑N * μ s<VAR>x : α<VAR>hx : x ∈ s<VAR>m : ℕ<VAR>hm : m ∈ Ioo 0 N<VAR>hmx : f^[m] x ∈ s<GOAL>∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[m] x ∈ s
<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝¹ : IsOpenImmersion f<VAR>inst✝ : IsLocallyNoetherian Y<VAR>U : ↑X.affineOpens<GOAL>IsNoetherianRing ↑Γ(X, ↑U)
<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝¹ : IsOpenImmersion f<VAR>inst✝ : IsLocallyNoetherian Y<VAR>U : ↑X.affineOpens<VAR>V : ↑Y.affineOpens := ⟨f ''ᵁ ↑U, ⋯⟩<GOAL>IsNoetherianRing ↑Γ(X, ↑U)
<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝¹ : IsOpenImmersion f<VAR>inst✝ : IsLocallyNoetherian Y<VAR>U : ↑X.affineOpens<VAR>V : ↑Y.affineOpens := ⟨f ''ᵁ ↑U, ⋯⟩<GOAL>Γ(X, ↑U) ≅ Γ(Y, ↑V)
<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝¹ : IsOpenImmersion f<VAR>inst✝ : IsLocallyNoetherian Y<VAR>U : ↑X.affineOpens<VAR>V : ↑Y.affineOpens := ⟨f ''ᵁ ↑U, ⋯⟩<GOAL>Γ(X, f ⁻¹ᵁ f ''ᵁ ↑U) ≅ Γ(Y, ↑V)
<VAR>R : Type u_1<VAR>inst✝³ : Finite R<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsReduced R<VAR>inst✝ : CharP R 2<VAR>a : R<GOAL>IsSquare a
<VAR>R : Type u_1<VAR>inst✝³ : Finite R<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsReduced R<VAR>inst✝ : CharP R 2<VAR>a : R<VAR>val✝ : Fintype R<GOAL>IsSquare a
<VAR>B : Type u₁<VAR>inst✝¹ : Bicategory B<VAR>C : Type u₂<VAR>inst✝ : Bicategory C<VAR>F G : OplaxFunctor B C<VAR>η θ ι : F ⟶ G<VAR>app : (a : B) → η.app a ≅ θ.app a<VAR>naturality : ∀ {a b : B} (f : a ⟶ b), F.map f ◁ (app b).hom ≫ θ.naturality f = η.naturality f ≫ (app a).hom ▷ G.map f<VAR>a b : B<VAR>f : a ⟶ b<GOAL>F.map f ◁ (fun a => (app a).inv) b ≫ η.naturality f = θ.naturality f ≫ (fun a => (app a).inv) a ▷ G.map f
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>M : Type w<VAR>inst✝ : L.Structure M<VAR>φ : L.Sentence<GOAL>φ ∈ L.completeTheory M ∨ Formula.not φ ∈ L.completeTheory M
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>I ^ n ≤ I ^ m
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<VAR>m n : ℕ<VAR>h : m ≤ n<VAR>k : ℕ<VAR>hk : n = m + k<GOAL>I ^ n ≤ I ^ m
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<VAR>m n : ℕ<VAR>h : m ≤ n<VAR>k : ℕ<VAR>hk : n = m + k<GOAL>I ^ m * I ^ k ≤ I ^ m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>𝓕 : Filter ι<VAR>a : α<GOAL>a ∈ liminf s 𝓕 ↔ ∀ᶠ (i : ι) in 𝓕, a ∈ s i
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p q : R[X]<VAR>hp : p.IsPrimitive<VAR>hq : q.IsPrimitive<GOAL>(p * q).IsPrimitive
<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✝¹ : IsIntegrallyClosed A<VAR>inst✝ : IsDedekindDomain B<VAR>I J : FractionalIdeal B⁰ L<VAR>hI : I ≠ 0<VAR>hJ : J ≠ 0<GOAL>↑(dual A K 1) = 1ᵛ
<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✝¹ : IsIntegrallyClosed A<VAR>inst✝ : IsDedekindDomain B<VAR>I J : FractionalIdeal B⁰ L<VAR>hI : I ≠ 0<VAR>hJ : J ≠ 0<GOAL>1 ≠ 0
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>r : ℝ<VAR>z : K<GOAL>re (r • z) = r * re z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f g : α →ₘ[μ] β<GOAL>f.Integrable → g.Integrable → (f + g).Integrable
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f✝ g✝ : α →ₘ[μ] β<VAR>f : α → β<VAR>hf : AEStronglyMeasurable f μ<VAR>g : α → β<VAR>hg : AEStronglyMeasurable g μ<VAR>hfi : (mk f hf).Integrable<VAR>hgi : (mk g hg).Integrable<GOAL>(mk f hf + mk g hg).Integrable
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f✝ g✝ : α →ₘ[μ] β<VAR>f : α → β<VAR>hf : AEStronglyMeasurable f μ<VAR>g : α → β<VAR>hg : AEStronglyMeasurable g μ<VAR>hfi : MeasureTheory.Integrable f μ<VAR>hgi : MeasureTheory.Integrable g μ<GOAL>MeasureTheory.Integrable (f + g) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s : Set α<VAR>h_le : μ.restrict s ≤ ν.restrict s<VAR>h_meas_s : MeasurableSet s<GOAL>(μ - ν) s = 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>J✝ : Type v<VAR>inst✝ : HasFiniteColimits C<VAR>J : Type<VAR>x✝ : Finite J<GOAL>HasColimitsOfShape (WidePushoutShape J) C
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>J✝ : Type v<VAR>inst✝ : HasFiniteColimits C<VAR>J : Type<VAR>x✝ : Finite J<VAR>val✝ : Fintype J<GOAL>HasColimitsOfShape (WidePushoutShape J) C
<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✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p✝ : Seminorm 𝕜 E<VAR>A B : Set E<VAR>a : 𝕜<VAR>r✝ : ℝ<VAR>x : E<VAR>p : Seminorm 𝕜 E<VAR>k : 𝕜<VAR>r : ℝ<GOAL>p.ball 0 (‖k‖ * r) ⊆ k • p.ball 0 r
<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✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p✝ : Seminorm 𝕜 E<VAR>A B : Set E<VAR>a : 𝕜<VAR>r✝ : ℝ<VAR>x : E<VAR>p : Seminorm 𝕜 E<VAR>r : ℝ<GOAL>p.ball 0 (‖0‖ * r) ⊆ 0 • p.ball 0 r
<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✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p✝ : Seminorm 𝕜 E<VAR>A B : Set E<VAR>a : 𝕜<VAR>r✝ : ℝ<VAR>x : E<VAR>p : Seminorm 𝕜 E<VAR>k : 𝕜<VAR>r : ℝ<VAR>hk : k ≠ 0<GOAL>p.ball 0 (‖k‖ * r) ⊆ k • p.ball 0 r
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ZMod p<VAR>ha : a ≠ 0<GOAL>a ^ (p - 1) = 1
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ZMod p<VAR>ha : a ≠ 0<VAR>h : a ^ (Fintype.card (ZMod p) - 1) = 1<GOAL>a ^ (p - 1) = 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedDivisionRing 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : BoundedSMul 𝕜 E<VAR>c : 𝕜<VAR>s : Set E<GOAL>EMetric.diam (c • s) = ‖c‖₊ • EMetric.diam s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedDivisionRing 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : BoundedSMul 𝕜 E<VAR>c : 𝕜<VAR>s : Set E<GOAL>‖c‖₊ • EMetric.diam s ≤ EMetric.diam (c • s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedDivisionRing 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : BoundedSMul 𝕜 E<VAR>s : Set E<GOAL>‖0‖₊ • EMetric.diam s ≤ EMetric.diam (0 • s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedDivisionRing 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : BoundedSMul 𝕜 E<VAR>c : 𝕜<VAR>s : Set E<VAR>hc : c ≠ 0<GOAL>‖c‖₊ • EMetric.diam s ≤ EMetric.diam (c • s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t u v : Finset α<VAR>a b : α<VAR>ha : a ∉ s<GOAL>insert a s ⊆ insert a t ↔ s ⊆ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t u v : Finset α<VAR>a b : α<VAR>ha : a ∉ s<GOAL>↑(insert a s) ⊆ ↑(insert a t) ↔ ↑s ⊆ ↑t