ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>h : G.chromaticNumber ≠ ⊤<GOAL>G.Colorable G.chromaticNumber.toNat
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>h : ∃ n, G.Colorable n<GOAL>G.Colorable G.chromaticNumber.toNat
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>n : ℕ<VAR>hn : G.Colorable n<GOAL>G.Colorable G.chromaticNumber.toNat
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>l✝ : List α<VAR>a✝ m a : α<VAR>l : List α<GOAL>(l ++ [a]).maximum = max l.maximum ↑a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>l✝ : List α<VAR>a✝ m a : α<VAR>l : List α<GOAL>Option.rec (some a) (fun val => if val < a then some a else some val) (argmax id l) = max (argmax id l) ↑a
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : CanonicallyOrderedAddCommMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>a : A<VAR>n i : ι<VAR>h : ¬i ≤ n<VAR>b : ↥(𝒜 i)<GOAL>↑(((decompose 𝒜) (a * ↑b)) n) = 0
<VAR>x y : ℝ<VAR>hx₁ : -(π / 2) ≤ x<VAR>hy₂ : y ≤ π / 2<VAR>hxy : x < y<GOAL>sin x < sin y
<VAR>x y : ℝ<VAR>hx₁ : -(π / 2) ≤ x<VAR>hy₂ : y ≤ π / 2<VAR>hxy : x < y<GOAL>0 < 2 * sin ((y - x) / 2) * cos ((y + x) / 2)
<VAR>x y : ℝ<VAR>hx₁ : -(π / 2) ≤ x<VAR>hy₂ : y ≤ π / 2<VAR>hxy : x < y<VAR>this : 0 < sin ((y - x) / 2)<GOAL>0 < 2 * sin ((y - x) / 2) * cos ((y + x) / 2)
<VAR>x y : ℝ<VAR>hx₁ : -(π / 2) ≤ x<VAR>hy₂ : y ≤ π / 2<VAR>hxy : x < y<VAR>this✝ : 0 < sin ((y - x) / 2)<VAR>this : 0 < cos ((y + x) / 2)<GOAL>0 < 2 * sin ((y - x) / 2) * cos ((y + x) / 2)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>i : ι<VAR>hs : i ∈ s<VAR>ht : t i = ∅<VAR>f : (i : ι) → α i<GOAL>f ∈ s.pi t ↔ f ∈ ∅
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>i : ι<VAR>hs : i ∈ s<VAR>ht : t i = ∅<VAR>f : (i : ι) → α i<GOAL>∃ x, ∃ (_ : x ∈ s), f x ∉ t x
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : DivisionMonoid α<VAR>b c : α<VAR>u : αˣ<GOAL>(↑u)⁻¹ * ↑u = 1
<VAR>R : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>k : Type u_2<VAR>l : Type u_3<VAR>m : Type u_4<VAR>n : Type u_5<VAR>inst✝ : Fintype n<VAR>M : Matrix m n R<GOAL>ker M.mulVecLin = ⊥ ↔ ∀ (v : n → R), M *ᵥ v = 0 → v = 0
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>s : Fork f g<GOAL>s.π.app one = s.ι ≫ g
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a✝ a b c : α<VAR>h : 0 < c<GOAL>(fun x => x * c) ⁻¹' Ico a b = Ico (a / c) (b / c)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Mul M<VAR>inst✝¹ : Mul N<VAR>inst✝ : Mul P<VAR>c : Con M<VAR>ι : Sort u_4<VAR>f : ι → Con M<GOAL>⇑(iInf f) = ⨅ i, ⇑(f i)
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>θ : Real.Angle<VAR>f : V ≃ₗᵢ[ℝ] V'<VAR>x : V'<GOAL>(((map (Fin 2) f.toLinearEquiv) o).rotation θ) x = f ((o.rotation θ) (f.symm x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>f : α → β<VAR>h_range : N.E ⊆ range f<VAR>hf : InjOn f (f ⁻¹' N.E)<GOAL>(N.comap f).map f hf = N
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>f : α → β<VAR>h_range : N.E ⊆ range f<VAR>hf : InjOn f (f ⁻¹' N.E)<GOAL>∀ I ⊆ ((N.comap f).map f hf).E, ((N.comap f).map f hf).Indep I ↔ N.Indep I
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>f : α → β<VAR>h_range : N.E ⊆ range f<VAR>hf : InjOn f (f ⁻¹' N.E)<GOAL>∀ t ⊆ f ⁻¹' N.E, (∃ I₀, (N.Indep (f '' I₀) ∧ InjOn f I₀) ∧ f '' t = f '' I₀) ↔ N.Indep (f '' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>f : α → β<VAR>h_range : N.E ⊆ range f<VAR>hf : InjOn f (f ⁻¹' N.E)<VAR>I : Set α<VAR>hI : I ⊆ f ⁻¹' N.E<VAR>x✝ : ∃ I₀, (N.Indep (f '' I₀) ∧ InjOn f I₀) ∧ f '' I = f '' I₀<VAR>I₀ : Set α<VAR>hI₀ : N.Indep (f '' I₀)<VAR>right✝ : InjOn f I₀<VAR>hII₀ : f '' I = f '' I₀<GOAL>N.Indep (f '' I)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>f : α → β<VAR>h_range : N.E ⊆ range f<VAR>hf : InjOn f (f ⁻¹' N.E)<VAR>I : Set α<VAR>hI : I ⊆ f ⁻¹' N.E<VAR>x✝ : ∃ I₀, (N.Indep (f '' I₀) ∧ InjOn f I₀) ∧ f '' I = f '' I₀<VAR>I₀ : Set α<VAR>hI₀ : N.Indep (f '' I₀)<VAR>right✝ : InjOn f I₀<VAR>hII₀ : f '' I = f '' I₀<GOAL>I₀ ⊆ f ⁻¹' N.E
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s t : Finset V<VAR>hs : AffineIndependent k Subtype.val<VAR>hst : ↑s ⊆ ↑(affineSpan k ↑t)<GOAL>s.card ≤ t.card
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>t : Finset V<VAR>hs : AffineIndependent k Subtype.val<VAR>hst : ↑∅ ⊆ ↑(affineSpan k ↑t)<GOAL>∅.card ≤ t.card
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s t : Finset V<VAR>hs : AffineIndependent k Subtype.val<VAR>hst : ↑s ⊆ ↑(affineSpan k ↑t)<VAR>hs' : s.Nonempty<GOAL>s.card ≤ t.card
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : Finset V<VAR>hs : AffineIndependent k Subtype.val<VAR>hs' : s.Nonempty<VAR>hst : ↑s ⊆ ↑(affineSpan k ↑∅)<GOAL>s.card ≤ ∅.card
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s t : Finset V<VAR>hs : AffineIndependent k Subtype.val<VAR>hst : ↑s ⊆ ↑(affineSpan k ↑t)<VAR>hs' : s.Nonempty<VAR>ht' : t.Nonempty<GOAL>s.card ≤ t.card
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s t : Finset V<VAR>hs : AffineIndependent k Subtype.val<VAR>hst : ↑s ⊆ ↑(affineSpan k ↑t)<VAR>hs' : s.Nonempty<VAR>ht' : t.Nonempty<VAR>this : Nonempty { x // x ∈ s }<GOAL>s.card ≤ t.card
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s t : Finset V<VAR>hs : AffineIndependent k Subtype.val<VAR>hst : ↑s ⊆ ↑(affineSpan k ↑t)<VAR>hs' : s.Nonempty<VAR>ht' : t.Nonempty<VAR>this✝ : Nonempty { x // x ∈ s }<VAR>this : Nonempty ↑↑t<GOAL>s.card ≤ t.card
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s t : Finset V<VAR>hs : AffineIndependent k Subtype.val<VAR>hst : ↑s ⊆ ↑(affineSpan k ↑t)<VAR>hs' : s.Nonempty<VAR>ht' : t.Nonempty<VAR>this✝ : Nonempty { x // x ∈ s }<VAR>this : Nonempty ↑↑t<VAR>direction_le : (affineSpan k ↑s).direction ≤ (affineSpan k ↑(affineSpan k ↑t)).direction<GOAL>s.card ≤ t.card
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s t : Finset V<VAR>hs : AffineIndependent k Subtype.val<VAR>hst : ↑s ⊆ ↑(affineSpan k ↑t)<VAR>hs' : s.Nonempty<VAR>ht' : t.Nonempty<VAR>this✝ : Nonempty { x // x ∈ s }<VAR>this : Nonempty ↑↑t<VAR>direction_le : vectorSpan k (Set.range Subtype.val) ≤ vectorSpan k (Set.range Subtype.val)<GOAL>s.card ≤ t.card
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s t : Finset V<VAR>hs : AffineIndependent k Subtype.val<VAR>hst : ↑s ⊆ ↑(affineSpan k ↑t)<VAR>hs' : s.Nonempty<VAR>ht' : t.Nonempty<VAR>this✝ : Nonempty { x // x ∈ s }<VAR>this : Nonempty ↑↑t<VAR>direction_le : vectorSpan k (Set.range Subtype.val) ≤ vectorSpan k (Set.range Subtype.val)<VAR>finrank_le : finrank k ↥(vectorSpan k (Set.range Subtype.val)) + 1 ≤ finrank k ↥(vectorSpan k (Set.range Subtype.val)) + 1<GOAL>s.card ≤ t.card
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s t : Finset V<VAR>hs : AffineIndependent k Subtype.val<VAR>hst : ↑s ⊆ ↑(affineSpan k ↑t)<VAR>hs' : s.Nonempty<VAR>ht' : t.Nonempty<VAR>this✝ : Nonempty { x // x ∈ s }<VAR>this : Nonempty ↑↑t<VAR>direction_le : vectorSpan k (Set.range Subtype.val) ≤ vectorSpan k (Set.range Subtype.val)<VAR>finrank_le : Fintype.card { x // x ∈ s } ≤ finrank k ↥(vectorSpan k (Set.range Subtype.val)) + 1<GOAL>s.card ≤ t.card
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : Rˣ<GOAL>ContinuousAt inverse ↑x
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : Rˣ<VAR>h_is_o : (fun t => inverse (↑x + t) - ↑x⁻¹) =o[𝓝 0] fun x => 1<GOAL>ContinuousAt inverse ↑x
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : Rˣ<VAR>h_is_o : (fun t => inverse (↑x + t) - ↑x⁻¹) =o[𝓝 0] fun x => 1<VAR>h_lim : Tendsto (fun y => y - ↑x) (𝓝 ↑x) (𝓝 0)<GOAL>ContinuousAt inverse ↑x
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : Rˣ<VAR>h_is_o : (fun t => inverse (↑x + t) - ↑x⁻¹) =o[𝓝 0] fun x => 1<VAR>h_lim : Tendsto (fun y => y - ↑x) (𝓝 ↑x) (𝓝 0)<GOAL>Tendsto (fun e => ‖inverse e - ↑x⁻¹‖) (𝓝 ↑x) (𝓝 0)
<VAR>n m a b : ℕ<VAR>han : a ≤ n<VAR>hbn : b ≤ n<GOAL>↑a < ↑b ↔ a < b
<VAR>n m a b : ℕ<VAR>han : a < n.succ<VAR>hbn : b < n.succ<GOAL>↑a < ↑b ↔ a < b
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>Z : Set (ProjectiveSpectrum 𝒜)<GOAL>IsClosed Z ↔ ∃ s, Z = zeroLocus 𝒜 s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a : α<VAR>inst✝ : IsSFiniteKernel κ<VAR>t : Set (α × β)<VAR>ht : MeasurableSet t<GOAL>Measurable fun a => (κ a) (Prod.mk a ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a : α<VAR>inst✝ : IsSFiniteKernel κ<VAR>t : Set (α × β)<VAR>ht : MeasurableSet t<GOAL>Measurable fun a => ((Kernel.sum κ.seq) a) (Prod.mk a ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a : α<VAR>inst✝ : IsSFiniteKernel κ<VAR>t : Set (α × β)<VAR>ht : MeasurableSet t<VAR>this : ∀ (a : α), ((Kernel.sum κ.seq) a) (Prod.mk a ⁻¹' t) = ∑' (n : ℕ), ((κ.seq n) a) (Prod.mk a ⁻¹' t)<GOAL>Measurable fun a => ((Kernel.sum κ.seq) a) (Prod.mk a ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a : α<VAR>inst✝ : IsSFiniteKernel κ<VAR>t : Set (α × β)<VAR>ht : MeasurableSet t<VAR>this : ∀ (a : α), ((Kernel.sum κ.seq) a) (Prod.mk a ⁻¹' t) = ∑' (n : ℕ), ((κ.seq n) a) (Prod.mk a ⁻¹' t)<GOAL>Measurable fun a => ∑' (n : ℕ), ((κ.seq n) a) (Prod.mk a ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a : α<VAR>inst✝ : IsSFiniteKernel κ<VAR>t : Set (α × β)<VAR>ht : MeasurableSet t<VAR>this : ∀ (a : α), ((Kernel.sum κ.seq) a) (Prod.mk a ⁻¹' t) = ∑' (n : ℕ), ((κ.seq n) a) (Prod.mk a ⁻¹' t)<VAR>n : ℕ<GOAL>Measurable fun a => ((κ.seq n) a) (Prod.mk a ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b b₁✝ b₂✝ : β<VAR>inst✝³ : LinearOrderedField α<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>a : α<VAR>b₁ b₂ : β<VAR>inst✝ : PosSMulMono α β<VAR>h : a < 0<GOAL>b₁ ≤ a⁻¹ • b₂ ↔ b₂ ≤ a • b₁
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑p<GOAL>hζ.integralPowerBasis'.dim = φ ↑p
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>W : MorphismProperty C<VAR>D : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} D<VAR>D' : Type u₃<VAR>inst✝³ : Category.{v₃, u₃} D'<VAR>L : C ⥤ D<VAR>inst✝² : L.IsLocalization W<VAR>L' : C ⥤ D'<VAR>inst✝¹ : L'.IsLocalization W<VAR>G : D ⥤ D'<VAR>e : L ⋙ G ≅ L'<VAR>X Y : C<VAR>inst✝ : HasSmallLocalizedHom W X Y<VAR>f : L.obj X ⟶ L.obj Y<GOAL>(homEquiv W W.Q L') ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)).symm ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)) ((homEquiv W L W.Q) f))) = e.inv.app X ≫ G.map f ≫ e.hom.app Y
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>W : MorphismProperty C<VAR>D : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} D<VAR>D' : Type u₃<VAR>inst✝³ : Category.{v₃, u₃} D'<VAR>L : C ⥤ D<VAR>inst✝² : L.IsLocalization W<VAR>L' : C ⥤ D'<VAR>inst✝¹ : L'.IsLocalization W<VAR>G : D ⥤ D'<VAR>e : L ⋙ G ≅ L'<VAR>X Y : C<VAR>inst✝ : HasSmallLocalizedHom W X Y<VAR>f : L.obj X ⟶ L.obj Y<GOAL>(homEquiv W L L') f = e.inv.app X ≫ G.map f ≫ e.hom.app Y
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>z : ℤ_[p]<GOAL>z ∈ nonunits ℤ_[p] ↔ ‖z‖ < 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>z : ℤ_[p]<GOAL>z ∈ nonunits ℤ_[p] ↔ ‖z‖ ≤ 1 ∧ ‖z‖ ≠ 1
<VAR>X✝ Y : Scheme<VAR>f : X✝ ⟶ Y<VAR>X : Scheme<GOAL>QuasiSeparatedSpace ↑↑X.toPresheafedSpace ↔ ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
<VAR>X✝ Y : Scheme<VAR>f : X✝ ⟶ Y<VAR>X : Scheme<GOAL>(∀ (U V : Set ↑↑X.toPresheafedSpace), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)) ↔ ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
<VAR>a b c : Ordinal.{u}<GOAL>a ♯ 1 = succ a
<VAR>a✝ b c a : Ordinal.{u}<VAR>IH : ∀ k < a, k ♯ 1 = succ k<GOAL>a ♯ 1 = succ a
<VAR>a✝ b c a : Ordinal.{u}<VAR>IH : ∀ k < a, k ♯ 1 = succ k<GOAL>∀ i < a, i ♯ 1 < succ a
<VAR>a✝ b c a : Ordinal.{u}<VAR>IH : ∀ k < a, k ♯ 1 = succ k<VAR>i : Ordinal.{u}<VAR>hi : i < a<GOAL>i ♯ 1 < succ a
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m n₁ n₂ n₁₂ : ℤ<VAR>z₁ z₁' : Cochain F G n₁<VAR>z₂ : Cochain G K n₂<VAR>h : n₁ + n₂ = n₁₂<VAR>p q : ℤ<VAR>hpq : p + n₁₂ = q<GOAL>((z₁ - z₁').comp z₂ h).v p q hpq = (z₁.comp z₂ h - z₁'.comp z₂ h).v p q hpq
<VAR>ι : Type u<VAR>f : ι → Scheme<VAR>x : ↑↑(∐ f).toPresheafedSpace<GOAL>∃ i y, (Sigma.ι f i).val.base y = x
<VAR>ι : Type u<VAR>f : ι → Scheme<VAR>x : ↑↑(∐ f).toPresheafedSpace<VAR>i : (disjointGlueData f).J<VAR>y : ↑↑((disjointGlueData f).U i).toPresheafedSpace<VAR>e : ((disjointGlueData f).ι i).val.base y = (sigmaIsoGlued f).hom.val.base x<GOAL>∃ i y, (Sigma.ι f i).val.base y = x
<VAR>ι : Type u<VAR>f : ι → Scheme<VAR>x : ↑↑(∐ f).toPresheafedSpace<VAR>i : (disjointGlueData f).J<VAR>y : ↑↑((disjointGlueData f).U i).toPresheafedSpace<VAR>e : ((disjointGlueData f).ι i).val.base y = (sigmaIsoGlued f).hom.val.base x<GOAL>(sigmaIsoGlued f).hom.val.base ((Sigma.ι f i).val.base y) = (sigmaIsoGlued f).hom.val.base x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : SemilatticeSup α<VAR>a b✝ c✝ : α<VAR>h : ∀ ⦃b c : α⦄, a ≤ b ⊔ c → a ≤ b ∨ a ≤ c<VAR>b c : α<VAR>ha : b ⊔ c = a<GOAL>b = a ∨ c = a
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>x : { x // x ∈ e.source }<GOAL>𝓝 ↑x = comap (↑e) (𝓝 (↑e ↑x)) ⊓ 𝓟 e.source
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>x : { x // x ∈ e.source }<GOAL>map Subtype.val (comap (⇑e.toHomeomorphSourceTarget) (comap Subtype.val (𝓝 ↑(e.toHomeomorphSourceTarget x)))) = map Subtype.val (comap Subtype.val (comap (↑e) (𝓝 (↑e ↑x))))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<VAR>a b c x : α<GOAL>x ∈ Icc a b \ {a} ↔ x ∈ Ioc a b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : OrderedSemiring α<VAR>inst✝³ : OrderedAddCommMonoid β<VAR>inst✝² : MulActionWithZero α β<VAR>inst✝¹ : FloorDiv α β<VAR>a : α<VAR>inst✝ : Nontrivial α<VAR>b c : β<GOAL>c ≤ b ⌊/⌋ 1 ↔ c ≤ b
<VAR>E : Type u_1<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup V<VAR>inst✝⁸ : InnerProductSpace ℝ V<VAR>inst✝⁷ : MeasurableSpace V<VAR>inst✝⁶ : BorelSpace V<VAR>inst✝⁵ : FiniteDimensional ℝ V<VAR>W : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : InnerProductSpace ℝ W<VAR>inst✝² : MeasurableSpace W<VAR>inst✝¹ : BorelSpace W<VAR>inst✝ : FiniteDimensional ℝ W<VAR>A : W ≃ₗᵢ[ℝ] V<VAR>f : V → E<VAR>w : W<GOAL>𝓕⁻ (f ∘ ⇑A) w = 𝓕⁻ f (A w)
<VAR>M : Type u_1<VAR>inst✝³ : MeasurableSpace M<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g : α → M<VAR>δ : Type u_3<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : MeasurableSup₂ α<VAR>f : ℕ → δ → α<VAR>n : ℕ<VAR>hf : ∀ k ≤ n, Measurable (f k)<GOAL>Measurable fun x => (range (n + 1)).sup' ⋯ fun k => f k x
<VAR>M : Type u_1<VAR>inst✝³ : MeasurableSpace M<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g : α → M<VAR>δ : Type u_3<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : MeasurableSup₂ α<VAR>f : ℕ → δ → α<VAR>n : ℕ<VAR>hf : ∀ k ≤ n, Measurable (f k)<GOAL>(fun x => (range (n + 1)).sup' ⋯ fun k => f k x) = (range (n + 1)).sup' ⋯ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>inst✝ : Preorder α<GOAL>s.chainHeight = ⨆ i ∈ s, (s ∩ Iic i).chainHeight
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>inst✝ : Preorder α<GOAL>s.chainHeight = ⨆ i ∈ s, (⇑ofDual ⁻¹' (s ∩ Iic i)).chainHeight
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>inst✝ : Preorder α<GOAL>⨆ i ∈ ⇑ofDual ⁻¹' s, (⇑ofDual ⁻¹' s ∩ Ici i).chainHeight = ⨆ i ∈ s, (⇑ofDual ⁻¹' (s ∩ Iic i)).chainHeight
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R[X]<VAR>inst✝ : Algebra R S<VAR>h h' : IsAdjoinRoot S f<VAR>eq : h.root = h'.root<VAR>x : R[X]<GOAL>h.map x = h'.map x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>a : α<VAR>b₁ b₂ : β<GOAL>(G □ H).Adj (a, b₁) (a, b₂) ↔ H.Adj b₁ b₂
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p q : R[X]<GOAL>(p * q).IsRoot a ↔ p.IsRoot a ∨ q.IsRoot a
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>x y : Associates R<GOAL>↑((associatesEquivIsPrincipal R) (x * y)) = ↑((associatesEquivIsPrincipal R) x) * ↑((associatesEquivIsPrincipal R) y)
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>x y : Associates R<GOAL>↑((associatesEquivIsPrincipal R) (Associates.mk (Quot.out x) * Associates.mk (Quot.out y))) = ↑((associatesEquivIsPrincipal R) (Associates.mk (Quot.out x))) * ↑((associatesEquivIsPrincipal R) (Associates.mk (Quot.out y)))
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<VAR>i j k : ℕ<GOAL>I ^ (i + k) • F.N j ≤ I ^ k • F.N (i + j)
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<VAR>i j k : ℕ<GOAL>I ^ k • I ^ i • F.N j ≤ I ^ k • F.N (i + j)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : BooleanAlgebra α<VAR>a b c d : α<GOAL>bᶜ \ aᶜ ⊔ aᶜ \ bᶜ = a ∆ b
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>X : PresheafedSpace C<GOAL>⋯.functor.op ⋙ X.presheaf = (Presheaf.pushforward C (Opens.inclusionTopIso ↑X).inv).obj X.presheaf
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>X : PresheafedSpace C<GOAL>(Opens.map (Opens.inclusionTopIso ↑X).inv).op ⋙ X.presheaf = (Presheaf.pushforward C (Opens.inclusionTopIso ↑X).inv).obj X.presheaf
<VAR>J : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>F : J ⥤ C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : HasColimit F<VAR>G : C ⥤ D<VAR>inst✝ : HasColimit (F ⋙ G)<VAR>j : J<GOAL>ι (F ⋙ G) j ≫ post F G = G.map (ι F j)
<VAR>J : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>F : J ⥤ C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : HasColimit F<VAR>G : C ⥤ D<VAR>inst✝ : HasColimit (F ⋙ G)<VAR>j : J<GOAL>(G.mapCocone (cocone F)).ι.app j = G.map (ι F j)
<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 : Ultrafilter X), ↑u ≤ 𝓝 x → s ∈ u → x ∈ s
<VAR>x : ℝ<VAR>hx : x ∈ Ici 0<GOAL>normSq ↑√x = x
<VAR>x : ℝ*<VAR>h0 : x ≠ 0<VAR>hi : x⁻¹.Infinitesimal<GOAL>x.Infinite
<VAR>x : ℝ*<VAR>h0 : x ≠ 0<VAR>hi : x⁻¹.Infinitesimal<VAR>hn : x < 0<GOAL>x.Infinite
<VAR>x : ℝ*<VAR>h0 : x ≠ 0<VAR>hi : x⁻¹.Infinitesimal<VAR>hp : x > 0<GOAL>x.Infinite
<VAR>ι : Type u_1<VAR>inst✝¹⁰ : Fintype ι<VAR>A : ι → Type u_2<VAR>inst✝⁹ : (i : ι) → MeasurableSpace (A i)<VAR>μ✝ : (i : ι) → Measure (A i)<VAR>inst✝⁸ : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>E : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>u : E → F<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : HasCompactSupport u<VAR>p : ℝ≥0<VAR>hp : (↑(finrank ℝ E)).IsConjExponent p<GOAL>eLpNorm u (↑p) μ ≤ ↑(eLpNormLESNormFDerivOneConst μ ↑p) * eLpNorm (fderiv ℝ u) 1 μ
<VAR>ι : Type u_1<VAR>inst✝¹⁰ : Fintype ι<VAR>A : ι → Type u_2<VAR>inst✝⁹ : (i : ι) → MeasurableSpace (A i)<VAR>μ✝ : (i : ι) → Measure (A i)<VAR>inst✝⁸ : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>E : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>u : E → F<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : HasCompactSupport u<VAR>p : ℝ≥0<VAR>hp : (↑(finrank ℝ E)).IsConjExponent p<VAR>h0p : 0 < ↑p<GOAL>eLpNorm u (↑p) μ ≤ ↑(eLpNormLESNormFDerivOneConst μ ↑p) * eLpNorm (fderiv ℝ u) 1 μ