ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>S : Type u_3<VAR>inst✝¹³ : Semiring R<VAR>inst✝¹² : Semiring S<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M₂<VAR>inst✝⁹ : AddCommMonoid M₃<VAR>inst✝⁸ : AddCommMonoid M₄<VAR>inst✝⁷ : AddCommMonoid M₅<VAR>inst✝⁶ : AddCommMonoid M₆<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module R M₃<VAR>inst✝² : Module R M₄<VAR>inst✝¹ : Module R M₅<VAR>inst✝ : Module R M₆<VAR>f✝ : M →ₗ[R] M₂<VAR>f : M →ₗ[R] M₃<VAR>g : M₂ →ₗ[R] M₃<VAR>x✝ : M<GOAL>(f.coprod g ∘ₗ inl R M M₂) x✝ = f x✝
<VAR>f : Code<VAR>k : Cont<VAR>v : List ℕ<VAR>fok : f.Ok<GOAL>eval step (stepNormal f (Cont.fix f k) v) = do let v ← f.fix.eval v eval step (Cfg.ret k v)
<VAR>f : Code<VAR>k : Cont<VAR>v : List ℕ<VAR>fok : f.Ok<VAR>x : Cfg<GOAL>x ∈ eval step (stepNormal f (Cont.fix f k) v) ↔ x ∈ do let v ← f.fix.eval v eval step (Cfg.ret k v)
<VAR>f : Code<VAR>k : Cont<VAR>v : List ℕ<VAR>fok : f.Ok<VAR>x : Cfg<GOAL>x ∈ eval step (stepNormal f (Cont.fix f k) v) ↔ ∃ a ∈ f.fix.eval v, x ∈ eval step (Cfg.ret k a)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c : α<VAR>h : a ≤ b<GOAL>Icc a b = cons a (Ioc a b) ⋯
<VAR>x y : EReal<GOAL>⊥ < x + y ↔ ⊥ < x ∧ ⊥ < y
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>s : Set G<VAR>N : Subgroup G<VAR>inst✝ : N.Normal<VAR>h : s ⊆ ↑N<VAR>a : G<VAR>w : a ∈ normalClosure s<GOAL>a ∈ N
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>s : Set G<VAR>N : Subgroup G<VAR>inst✝ : N.Normal<VAR>h : s ⊆ ↑N<VAR>a : G<VAR>w : a ∈ normalClosure s<VAR>x : G<VAR>hx : x ∈ conjugatesOfSet s<GOAL>x ∈ N
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>s : Set G<VAR>N : Subgroup G<VAR>inst✝ : N.Normal<VAR>h : s ⊆ ↑N<VAR>a : G<VAR>w : a ∈ normalClosure s<GOAL>1 ∈ N
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>s : Set G<VAR>N : Subgroup G<VAR>inst✝ : N.Normal<VAR>h : s ⊆ ↑N<VAR>a : G<VAR>w : a ∈ normalClosure s<VAR>x y : G<VAR>ihx : x ∈ N<VAR>ihy : y ∈ N<GOAL>x * y ∈ N
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>s : Set G<VAR>N : Subgroup G<VAR>inst✝ : N.Normal<VAR>h : s ⊆ ↑N<VAR>a : G<VAR>w : a ∈ normalClosure s<VAR>x : G<VAR>ihx : x ∈ N<GOAL>x⁻¹ ∈ N
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I : Box ι<VAR>i : ι<VAR>x : ℝ<VAR>y : ι → ℝ<GOAL>I.splitLower i x = ↑I ↔ I.upper i ≤ x
<VAR>α : Type u<VAR>inst✝¹ : DecidableEq α<VAR>β : Type v<VAR>inst✝ : Fintype α<VAR>f : Perm α<GOAL>sign f⁻¹ = sign f
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>-Ico a b = Ioc (-b) (-a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β → β<VAR>inst✝¹ : BEq α<VAR>inst✝ : Hashable α<VAR>m : Imp α β<VAR>k : α<VAR>h : m.size = m.buckets.size<GOAL>m.size = ((m.buckets.update (mkIdx ⋯ (hash k).toUSize).val AssocList.nil ⋯).update (mkIdx ⋯ (hash k).toUSize).val (AssocList.modify k f m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat]) ⋯).size
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β → β<VAR>inst✝¹ : BEq α<VAR>inst✝ : Hashable α<VAR>m : Imp α β<VAR>k : α<VAR>h : m.size = m.buckets.size<GOAL>m.size = (m.buckets.update (mkIdx ⋯ (hash k).toUSize).val (AssocList.modify k f m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat]) ⋯).size
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β → β<VAR>inst✝¹ : BEq α<VAR>inst✝ : Hashable α<VAR>m : Imp α β<VAR>k : α<VAR>h : m.size = m.buckets.size<GOAL>Nat.sum (List.map (fun x => x.toList.length) m.buckets.val.data) = Nat.sum (List.map (fun x => x.toList.length) (m.buckets.update (mkIdx ⋯ (hash k).toUSize).val (AssocList.modify k f m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat]) ⋯).val.data)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β → β<VAR>inst✝¹ : BEq α<VAR>inst✝ : Hashable α<VAR>m : Imp α β<VAR>k : α<VAR>h : m.size = m.buckets.size<VAR>w✝¹ w✝ : List (AssocList α β)<VAR>h₁ : m.buckets.val.data = w✝¹ ++ m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val] :: w✝<VAR>left✝ : w✝¹.length = (mkIdx ⋯ (hash k).toUSize).val.toNat<VAR>eq : (m.buckets.update (mkIdx ⋯ (hash k).toUSize).val (AssocList.modify k f m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat]) ⋯).val.data = w✝¹ ++ AssocList.modify k f m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat] :: w✝<GOAL>Nat.sum (List.map (fun x => x.toList.length) m.buckets.val.data) = Nat.sum (List.map (fun x => x.toList.length) (w✝¹ ++ AssocList.modify k f m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat] :: w✝))
<VAR>n : ℕ<VAR>x✝ : Fin (n + 1)<VAR>i : ℕ<VAR>h : i < n + 1<GOAL>(i, n - i) ∈ antidiagonal n
<VAR>n : ℕ<VAR>x✝ : Fin (n + 1)<VAR>i : ℕ<VAR>h : i < n + 1<GOAL>i ≤ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>n : ι<GOAL>f n = gramSchmidt 𝕜 f n + ∑ i ∈ Iio n, (⟪gramSchmidt 𝕜 f i, f n⟫_𝕜 / ↑‖gramSchmidt 𝕜 f i‖ ^ 2) • gramSchmidt 𝕜 f i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>n x✝ : ι<VAR>a✝ : x✝ ∈ Iio n<GOAL>(⟪gramSchmidt 𝕜 f x✝, f n⟫_𝕜 / ↑‖gramSchmidt 𝕜 f x✝‖ ^ 2) • gramSchmidt 𝕜 f x✝ = ↑((orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f x✝})) (f n))
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : TopologicalSpace α<VAR>R : Type u_2<VAR>inst✝ : SeminormedRing R<VAR>f : α →ᵇ R<GOAL>⇑(npowRec 0 f) = ⇑f ^ 0
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : TopologicalSpace α<VAR>R : Type u_2<VAR>inst✝ : SeminormedRing R<VAR>f : α →ᵇ R<VAR>n : ℕ<GOAL>⇑(npowRec (n + 1) f) = ⇑f ^ (n + 1)
<VAR>x : ℝ<GOAL>(∀ (p : ℝ), LiouvilleWith p x) ↔ Liouville x
<VAR>x : ℝ<VAR>H : ∀ (p : ℝ), LiouvilleWith p x<VAR>n : ℕ<GOAL>∃ a b, 1 < b ∧ x ≠ ↑a / ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ n
<VAR>x : ℝ<VAR>H : ∀ (p : ℝ), LiouvilleWith p x<VAR>n b : ℕ<VAR>hb : 1 < b<VAR>a : ℤ<VAR>hne : x ≠ ↑a / ↑b<VAR>hlt : |x - ↑a / ↑b| < ↑b ^ (-↑n)<GOAL>∃ a b, 1 < b ∧ x ≠ ↑a / ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN : 4096 ≤ N<GOAL>↑N ^ (↑(nValue N))⁻¹ / rexp 1 < ↑(dValue N)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN : 4096 ≤ N<GOAL>2 / (1 - 2 / rexp 1) ≤ ↑N ^ (↑(nValue N))⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN : 4096 ≤ N<GOAL>log (2 / (1 - 2 / rexp 1)) ≤ log ↑N / ↑(nValue N)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN : 4096 ≤ N<GOAL>0 < ↑N
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN : 4096 ≤ N<GOAL>0 < 2 / (1 - 2 / rexp 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN : 4096 ≤ N<GOAL>0 < ↑N ^ (↑(nValue N))⁻¹
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : NormedRing R<VAR>inst✝² : IsAbsoluteValue norm<VAR>F : Type u_3<VAR>K : Type u_4<VAR>inst✝¹ : CommRing F<VAR>inst✝ : NormedField K<VAR>p : F[X]<VAR>f : F →+* K<VAR>B : ℝ<VAR>hB : B < 0<VAR>h1 : p.Monic<VAR>h2 : Splits f p<VAR>h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B<GOAL>p.natDegree = 0
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : NormedRing R<VAR>inst✝² : IsAbsoluteValue norm<VAR>F : Type u_3<VAR>K : Type u_4<VAR>inst✝¹ : CommRing F<VAR>inst✝ : NormedField K<VAR>p : F[X]<VAR>f : F →+* K<VAR>B : ℝ<VAR>h1 : p.Monic<VAR>h2 : Splits f p<VAR>h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B<VAR>hB : p.natDegree ≠ 0<GOAL>0 ≤ B
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : NormedRing R<VAR>inst✝² : IsAbsoluteValue norm<VAR>F : Type u_3<VAR>K : Type u_4<VAR>inst✝¹ : CommRing F<VAR>inst✝ : NormedField K<VAR>p : F[X]<VAR>f : F →+* K<VAR>B : ℝ<VAR>h1 : p.Monic<VAR>h2 : Splits f p<VAR>h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B<VAR>hB : card (map f p).roots ≠ 0<GOAL>0 ≤ B
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : NormedRing R<VAR>inst✝² : IsAbsoluteValue norm<VAR>F : Type u_3<VAR>K : Type u_4<VAR>inst✝¹ : CommRing F<VAR>inst✝ : NormedField K<VAR>p : F[X]<VAR>f : F →+* K<VAR>B : ℝ<VAR>h1 : p.Monic<VAR>h2 : Splits f p<VAR>h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B<VAR>hB : card (map f p).roots ≠ 0<VAR>z : K<VAR>hz : z ∈ (map f p).roots<GOAL>0 ≤ B
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : Monoid M<VAR>a : M<GOAL>closure {1} = ⊥
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : ConcreteCategory D<VAR>J : GrothendieckTopology C<VAR>F₁ F₂ F₃ : Cᵒᵖ ⥤ D<VAR>φ : F₁ ⟶ F₂<VAR>ψ : F₂ ⟶ F₃<VAR>hφ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(φ.app X)<VAR>X : Cᵒᵖ<VAR>x y : (forget D).obj (F₁.obj X)<VAR>h : (φ.app X) x = (φ.app X) y<GOAL>equalizerSieve x y ∈ J.sieves (unop X)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : ConcreteCategory D<VAR>J : GrothendieckTopology C<VAR>F₁ F₂ F₃ : Cᵒᵖ ⥤ D<VAR>φ : F₁ ⟶ F₂<VAR>ψ : F₂ ⟶ F₃<VAR>hφ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(φ.app X)<VAR>X : Cᵒᵖ<VAR>x y : (forget D).obj (F₁.obj X)<VAR>h : (φ.app X) x = (φ.app X) y<GOAL>equalizerSieve x y = ⊤
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : ConcreteCategory D<VAR>J : GrothendieckTopology C<VAR>F₁ F₂ F₃ : Cᵒᵖ ⥤ D<VAR>φ : F₁ ⟶ F₂<VAR>ψ : F₂ ⟶ F₃<VAR>hφ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(φ.app X)<VAR>X : Cᵒᵖ<VAR>x y : (forget D).obj (F₁.obj X)<VAR>h : (φ.app X) x = (φ.app X) y<VAR>Y : C<VAR>f : Y ⟶ unop X<GOAL>(equalizerSieve x y).arrows f ↔ ⊤.arrows f
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : ConcreteCategory D<VAR>J : GrothendieckTopology C<VAR>F₁ F₂ F₃ : Cᵒᵖ ⥤ D<VAR>φ : F₁ ⟶ F₂<VAR>ψ : F₂ ⟶ F₃<VAR>hφ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(φ.app X)<VAR>X : Cᵒᵖ<VAR>x y : (forget D).obj (F₁.obj X)<VAR>h : (φ.app X) x = (φ.app X) y<VAR>Y : C<VAR>f : Y ⟶ unop X<GOAL>(F₁.map f.op) x = (F₁.map f.op) y
<VAR>p q✝ : ℚ≥0<VAR>n₁ n₂ d₁ d₂ d : ℕ<VAR>q r : ℚ≥0<GOAL>↑(q * r) = ↑(divNat (q.num * r.num) (q.den * r.den))
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<GOAL>QuasiMeasurePreserving Prod.fst (μ.prod ν) μ
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>h2s : μ s = 0<GOAL>(map Prod.fst (μ.prod ν)) s = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝ : CommSemiring R<VAR>x x✝ : R<GOAL>eval₂ (evalRingHom x) x✝ = evalEval x x✝
<VAR>k : Type u_1<VAR>inst✝³ : Field k<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>inst✝ : NumberField K<VAR>x : K<GOAL>∏ w : InfinitePlace K, w x ^ w.mult = ↑|(Algebra.norm ℚ) x|
<VAR>k : Type u_1<VAR>inst✝³ : Field k<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>inst✝ : NumberField K<VAR>x : K<GOAL>∏ w : InfinitePlace K, w x ^ w.mult = Complex.abs (∏ σ : K →ₐ[ℚ] ℂ, σ x)
<VAR>k : Type u_1<VAR>inst✝³ : Field k<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>inst✝ : NumberField K<VAR>x : K<GOAL>↑|(Algebra.norm ℚ) x| = Complex.abs ((algebraMap ℚ ℂ) ((Algebra.norm ℚ) x))
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ<VAR>s✝ s : Set α<VAR>a : α<GOAL>(∀ (i : ℝ), 0 < i → ∃ y ∈ s, y ∈ ball a i) ↔ ∀ ε > 0, ∃ b ∈ s, dist a b < ε
<VAR>n : ℕ<VAR>h : 2 ≤ n<GOAL>(finRotate n).IsCycle
<VAR>m : ℕ<VAR>h : 2 ≤ 2 + m<GOAL>(finRotate (2 + m)).IsCycle
<VAR>m : ℕ<VAR>h : 2 ≤ 2 + m<GOAL>(finRotate (m + 2)).IsCycle
<VAR>L : Type u_1<VAR>inst✝³ : SemilatticeSup L<VAR>inst✝² : TopologicalSpace L<VAR>inst✝¹ : ContinuousSup L<VAR>X : Type u_2<VAR>inst✝ : TopologicalSpace X<VAR>f : ℕ → X → L<VAR>n : ℕ<VAR>s : Set X<VAR>x : X<VAR>hf : ∀ k ≤ n, ContinuousAt (f k) x<GOAL>ContinuousAt ((partialSups f) n) x
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : Nonempty ι<VAR>x : 𝕜<VAR>U : Set E<VAR>hU : U ∈ p.basisSets<GOAL>∃ V ∈ AddGroupFilterBasis.toFilterBasis.sets, V ⊆ (fun y => x • y) ⁻¹' U
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : Nonempty ι<VAR>x : 𝕜<VAR>U : Set E<VAR>hU✝ : U ∈ p.basisSets<VAR>s : Finset ι<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hU : U = (s.sup p).ball 0 r<GOAL>∃ V ∈ AddGroupFilterBasis.toFilterBasis.sets, V ⊆ (fun y => x • y) ⁻¹' U
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : Nonempty ι<VAR>x : 𝕜<VAR>U : Set E<VAR>hU✝ : U ∈ p.basisSets<VAR>s : Finset ι<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hU : U = (s.sup p).ball 0 r<VAR>h : ¬x ≠ 0<GOAL>∃ V ∈ AddGroupFilterBasis.toFilterBasis.sets, V ⊆ (fun y => x • y) ⁻¹' (s.sup p).ball 0 r
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : Nonempty ι<VAR>x : 𝕜<VAR>U : Set E<VAR>hU✝ : U ∈ p.basisSets<VAR>s : Finset ι<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hU : U = (s.sup p).ball 0 r<VAR>h : ¬x ≠ 0<GOAL>(s.sup p).ball 0 r ⊆ (fun y => x • y) ⁻¹' (s.sup p).ball 0 r
<VAR>x : ℝ<GOAL>WithBot.some ∘ WithTop.some ⁻¹' Ioi ↑↑x = Ioi x
<VAR>x : ℝ<GOAL>WithTop.some ⁻¹' (WithBot.some ⁻¹' Ioi ↑↑x) = Ioi x
<VAR>α : Type u<VAR>β : Type v<VAR>l✝ : List α<VAR>x : α<VAR>xs : List α<VAR>n✝ : ℕ<VAR>d✝ : α<VAR>l l' : List α<VAR>d : α<VAR>n : ℕ<VAR>h : n < l.length<GOAL>(l ++ l').getD n d = l.getD n d
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : IsIntegralClosure A R B<VAR>h : optParam (IsIntegral R 1) ⋯<GOAL>(algebraMap A B) (mk' A 1 h) = (algebraMap A B) 1
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace ℝ E<VAR>inst✝² : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>hF : Fact (finrank ℝ F = 2)<VAR>φ : E ≃ₗᵢ[ℝ] F<VAR>x y : F<GOAL>(((map (Fin 2) φ.toLinearEquiv) o).kahler x) y = (o.kahler (φ.symm x)) (φ.symm y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<GOAL>(N.comap f).Dep I ↔ N.Dep (f '' I) ∨ N.Indep (f '' I) ∧ ¬InjOn f I
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<GOAL>(N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E ↔ ¬N.Indep (f '' I) ∧ I ⊆ f ⁻¹' N.E ∨ N.Indep (f '' I) ∧ ¬InjOn f I
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>hI : N.Indep (f '' I) ∧ ¬InjOn f I<GOAL>(N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>hI : N.Indep (f '' I) ∧ ¬InjOn f I<GOAL>I ⊆ f ⁻¹' N.E
<VAR>Fq F : Type<VAR>inst✝⁹ : Field Fq<VAR>inst✝⁸ : Field F<VAR>Fqt : Type u_1<VAR>inst✝⁷ : Field Fqt<VAR>inst✝⁶ : Algebra Fq[X] Fqt<VAR>inst✝⁵ : IsFractionRing Fq[X] Fqt<VAR>inst✝⁴ : Algebra (RatFunc Fq) F<VAR>inst✝³ : Algebra Fqt F<VAR>inst✝² : Algebra Fq[X] F<VAR>inst✝¹ : IsScalarTower Fq[X] Fqt F<VAR>inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F<VAR>e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt<GOAL>FunctionField Fq F ↔ FiniteDimensional Fqt F
<VAR>Fq F : Type<VAR>inst✝⁹ : Field Fq<VAR>inst✝⁸ : Field F<VAR>Fqt : Type u_1<VAR>inst✝⁷ : Field Fqt<VAR>inst✝⁶ : Algebra Fq[X] Fqt<VAR>inst✝⁵ : IsFractionRing Fq[X] Fqt<VAR>inst✝⁴ : Algebra (RatFunc Fq) F<VAR>inst✝³ : Algebra Fqt F<VAR>inst✝² : Algebra Fq[X] F<VAR>inst✝¹ : IsScalarTower Fq[X] Fqt F<VAR>inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F<VAR>e : RatFunc Fq ≃ₐ[Fq[X]] Fqt := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt<VAR>this : ∀ (c : RatFunc Fq) (x : F), e c • x = c • x<GOAL>FunctionField Fq F ↔ FiniteDimensional Fqt F
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ<VAR>a b : (x : ↥(unop U)) → at ↑x<VAR>ha : (isLocallyFraction 𝒜).pred a<VAR>hb : (isLocallyFraction 𝒜).pred b<VAR>x : ↥(unop U)<VAR>Va : Opens ↑(ProjectiveSpectrum.top 𝒜)<VAR>ma : ↑x ∈ Va<VAR>ia : Va ⟶ unop U<VAR>ja : ℕ<VAR>ra : A<VAR>ra_mem : ra ∈ 𝒜 ja<VAR>sa : A<VAR>sa_mem : sa ∈ 𝒜 ja<VAR>hwa : ∀ (x : ↥Va), ↑⟨sa, sa_mem⟩ ∉ (↑x).asHomogeneousIdeal<VAR>wa : ∀ (x : ↥Va), (fun x => a ((fun x => ⟨↑x, ⋯⟩) x)) x = HomogeneousLocalization.mk { deg := ja, num := ⟨ra, ra_mem⟩, den := ⟨sa, sa_mem⟩, den_mem := ⋯ }<VAR>Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)<VAR>mb : ↑x ∈ Vb<VAR>ib : Vb ⟶ unop U<VAR>jb : ℕ<VAR>rb : A<VAR>rb_mem : rb ∈ 𝒜 jb<VAR>sb : A<VAR>sb_mem : sb ∈ 𝒜 jb<VAR>hwb : ∀ (x : ↥Vb), ↑⟨sb, sb_mem⟩ ∉ (↑x).asHomogeneousIdeal<VAR>wb : ∀ (x : ↥Vb), (fun x => b ((fun x => ⟨↑x, ⋯⟩) x)) x = HomogeneousLocalization.mk { deg := jb, num := ⟨rb, rb_mem⟩, den := ⟨sb, sb_mem⟩, den_mem := ⋯ }<GOAL>∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (isFractionPrelocal 𝒜).pred fun x => (a + b) ((fun x => ⟨↑x, ⋯⟩) x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ<VAR>a b : (x : ↥(unop U)) → at ↑x<VAR>ha : (isLocallyFraction 𝒜).pred a<VAR>hb : (isLocallyFraction 𝒜).pred b<VAR>x : ↥(unop U)<VAR>Va : Opens ↑(ProjectiveSpectrum.top 𝒜)<VAR>ma : ↑x ∈ Va<VAR>ia : Va ⟶ unop U<VAR>ja : ℕ<VAR>ra : A<VAR>ra_mem : ra ∈ 𝒜 ja<VAR>sa : A<VAR>sa_mem : sa ∈ 𝒜 ja<VAR>hwa : ∀ (x : ↥Va), ↑⟨sa, sa_mem⟩ ∉ (↑x).asHomogeneousIdeal<VAR>wa : ∀ (x : ↥Va), (fun x => a ((fun x => ⟨↑x, ⋯⟩) x)) x = HomogeneousLocalization.mk { deg := ja, num := ⟨ra, ra_mem⟩, den := ⟨sa, sa_mem⟩, den_mem := ⋯ }<VAR>Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)<VAR>mb : ↑x ∈ Vb<VAR>ib : Vb ⟶ unop U<VAR>jb : ℕ<VAR>rb : A<VAR>rb_mem : rb ∈ 𝒜 jb<VAR>sb : A<VAR>sb_mem : sb ∈ 𝒜 jb<VAR>hwb : ∀ (x : ↥Vb), ↑⟨sb, sb_mem⟩ ∉ (↑x).asHomogeneousIdeal<VAR>wb : ∀ (x : ↥Vb), (fun x => b ((fun x => ⟨↑x, ⋯⟩) x)) x = HomogeneousLocalization.mk { deg := jb, num := ⟨rb, rb_mem⟩, den := ⟨sb, sb_mem⟩, den_mem := ⋯ }<VAR>y : ↥(Va ⊓ Vb)<GOAL>(fun x => (a + b) ((fun x => ⟨↑x, ⋯⟩) x)) y = HomogeneousLocalization.mk { deg := ja + jb, num := ⟨sb * ra + sa * rb, ⋯⟩, den := ⟨sa * sb, ⋯⟩, den_mem := ⋯ }
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ<VAR>a b : (x : ↥(unop U)) → at ↑x<VAR>ha : (isLocallyFraction 𝒜).pred a<VAR>hb : (isLocallyFraction 𝒜).pred b<VAR>x : ↥(unop U)<VAR>Va : Opens ↑(ProjectiveSpectrum.top 𝒜)<VAR>ma : ↑x ∈ Va<VAR>ia : Va ⟶ unop U<VAR>ja : ℕ<VAR>ra : A<VAR>ra_mem : ra ∈ 𝒜 ja<VAR>sa : A<VAR>sa_mem : sa ∈ 𝒜 ja<VAR>hwa : ∀ (x : ↥Va), ↑⟨sa, sa_mem⟩ ∉ (↑x).asHomogeneousIdeal<VAR>wa : ∀ (x : ↥Va), a ⟨↑x, ⋯⟩ = HomogeneousLocalization.mk { deg := ja, num := ⟨ra, ra_mem⟩, den := ⟨sa, sa_mem⟩, den_mem := ⋯ }<VAR>Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)<VAR>mb : ↑x ∈ Vb<VAR>ib : Vb ⟶ unop U<VAR>jb : ℕ<VAR>rb : A<VAR>rb_mem : rb ∈ 𝒜 jb<VAR>sb : A<VAR>sb_mem : sb ∈ 𝒜 jb<VAR>hwb : ∀ (x : ↥Vb), ↑⟨sb, sb_mem⟩ ∉ (↑x).asHomogeneousIdeal<VAR>wb : ∀ (x : ↥Vb), b ⟨↑x, ⋯⟩ = HomogeneousLocalization.mk { deg := jb, num := ⟨rb, rb_mem⟩, den := ⟨sb, sb_mem⟩, den_mem := ⋯ }<VAR>y : ↥(Va ⊓ Vb)<GOAL>(fun x => (a + b) ((fun x => ⟨↑x, ⋯⟩) x)) y = HomogeneousLocalization.mk { deg := ja + jb, num := ⟨sb * ra + sa * rb, ⋯⟩, den := ⟨sa * sb, ⋯⟩, den_mem := ⋯ }
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ<VAR>a b : (x : ↥(unop U)) → at ↑x<VAR>ha : (isLocallyFraction 𝒜).pred a<VAR>hb : (isLocallyFraction 𝒜).pred b<VAR>x : ↥(unop U)<VAR>Va : Opens ↑(ProjectiveSpectrum.top 𝒜)<VAR>ma : ↑x ∈ Va<VAR>ia : Va ⟶ unop U<VAR>ja : ℕ<VAR>ra : A<VAR>ra_mem : ra ∈ 𝒜 ja<VAR>sa : A<VAR>sa_mem : sa ∈ 𝒜 ja<VAR>hwa : ∀ (x : ↥Va), ↑⟨sa, sa_mem⟩ ∉ (↑x).asHomogeneousIdeal<VAR>wa : ∀ (x : ↥Va), a ⟨↑x, ⋯⟩ = HomogeneousLocalization.mk { deg := ja, num := ⟨ra, ra_mem⟩, den := ⟨sa, sa_mem⟩, den_mem := ⋯ }<VAR>Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)<VAR>mb : ↑x ∈ Vb<VAR>ib : Vb ⟶ unop U<VAR>jb : ℕ<VAR>rb : A<VAR>rb_mem : rb ∈ 𝒜 jb<VAR>sb : A<VAR>sb_mem : sb ∈ 𝒜 jb<VAR>hwb : ∀ (x : ↥Vb), ↑⟨sb, sb_mem⟩ ∉ (↑x).asHomogeneousIdeal<VAR>wb : ∀ (x : ↥Vb), b ⟨↑x, ⋯⟩ = HomogeneousLocalization.mk { deg := jb, num := ⟨rb, rb_mem⟩, den := ⟨sb, sb_mem⟩, den_mem := ⋯ }<VAR>y : ↥(Va ⊓ Vb)<GOAL>Localization.mk (sb * ra + sa * rb) (⟨sa, ⋯⟩ * ⟨sb, ⋯⟩) = Localization.mk (sb * ra + sa * rb) ⟨sa * sb, ⋯⟩
<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>K L M : CochainComplex C ℤ<VAR>n✝ : ℤ<VAR>γ γ₁✝ γ₂✝ : Cochain K L n✝<VAR>n' a : ℤ<VAR>γ₁ γ₂ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'<VAR>n : ℤ<VAR>hn : n' + a = n<GOAL>(rightShiftAddEquiv K L n a n' hn).symm (γ₁ + γ₂) = γ₁.rightUnshift n hn + γ₂.rightUnshift n hn
<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<GOAL>s ∈ coclosedLindelof X ↔ ∃ t, IsClosed t ∧ IsLindelof t ∧ tᶜ ⊆ s
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B✝ C : Finset α<VAR>hA : A.Nonempty<VAR>B : Finset α<VAR>m n : ℕ<GOAL>↑(B ^ m / B ^ n).card ≤ (↑(A * B).card / ↑A.card) ^ (m + n) * ↑A.card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B✝ C : Finset α<VAR>hA : A.Nonempty<VAR>B : Finset α<VAR>m n : ℕ<VAR>hA' : A ∈ A.powerset.erase ∅<GOAL>↑(B ^ m / B ^ n).card ≤ (↑(A * B).card / ↑A.card) ^ (m + n) * ↑A.card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B✝ C✝ : Finset α<VAR>hA : A.Nonempty<VAR>B : Finset α<VAR>m n : ℕ<VAR>hA' : A ∈ A.powerset.erase ∅<VAR>C : Finset α<VAR>hC : C ∈ A.powerset.erase ∅<VAR>hCA : ∀ x' ∈ A.powerset.erase ∅, ↑(C * B).card / ↑C.card ≤ ↑(x' * B).card / ↑x'.card<GOAL>↑(B ^ m / B ^ n).card ≤ (↑(A * B).card / ↑A.card) ^ (m + n) * ↑A.card