ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>S : Finset R<VAR>hS : Ideal.span ↑S = ⊤<VAR>hN : ∀ (s : { x // x ∈ S }), IsNoetherianRing (Localization.Away ↑s)<VAR>I : ℕ →o Submodule R R<VAR>floc : (s : R) → R →+* Localization.Away s := fun s => algebraMap R (Localization.Away s)<VAR>suitableN : R → Set ℕ := fun s => {n | ∀ (m : ℕ), n ≤ m → Ideal.map (floc s) (I n) = Ideal.map (floc s) (I m)}<VAR>minN : R → ℕ := fun s => sInf (suitableN s)<VAR>hSuit : ∀ (s : { x // x ∈ S }), minN ↑s ∈ suitableN ↑s<VAR>N : ℕ := S.sup minN<GOAL>∃ n, ∀ (m : ℕ), n ≤ m → I n = I m
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>S : Finset R<VAR>hS : Ideal.span ↑S = ⊤<VAR>hN : ∀ (s : { x // x ∈ S }), IsNoetherianRing (Localization.Away ↑s)<VAR>I : ℕ →o Submodule R R<VAR>floc : (s : R) → R →+* Localization.Away s := fun s => algebraMap R (Localization.Away s)<VAR>suitableN : R → Set ℕ := fun s => {n | ∀ (m : ℕ), n ≤ m → Ideal.map (floc s) (I n) = Ideal.map (floc s) (I m)}<VAR>minN : R → ℕ := fun s => sInf (suitableN s)<VAR>hSuit : ∀ (s : { x // x ∈ S }), minN ↑s ∈ suitableN ↑s<VAR>N : ℕ := S.sup minN<GOAL>∀ (m : ℕ), N ≤ m → I N = I m
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>S : Finset R<VAR>hS : Ideal.span ↑S = ⊤<VAR>hN✝ : ∀ (s : { x // x ∈ S }), IsNoetherianRing (Localization.Away ↑s)<VAR>I : ℕ →o Submodule R R<VAR>floc : (s : R) → R →+* Localization.Away s := fun s => algebraMap R (Localization.Away s)<VAR>suitableN : R → Set ℕ := fun s => {n | ∀ (m : ℕ), n ≤ m → Ideal.map (floc s) (I n) = Ideal.map (floc s) (I m)}<VAR>minN : R → ℕ := fun s => sInf (suitableN s)<VAR>hSuit : ∀ (s : { x // x ∈ S }), minN ↑s ∈ suitableN ↑s<VAR>N : ℕ := S.sup minN<VAR>hN : ∀ (s : { x // x ∈ S }), minN ↑s ≤ N<GOAL>∀ (m : ℕ), N ≤ m → I N = I m
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>S : Finset R<VAR>hS : Ideal.span ↑S = ⊤<VAR>hN✝ : ∀ (s : { x // x ∈ S }), IsNoetherianRing (Localization.Away ↑s)<VAR>I : ℕ →o Submodule R R<VAR>floc : (s : R) → R →+* Localization.Away s := fun s => algebraMap R (Localization.Away s)<VAR>suitableN : R → Set ℕ := fun s => {n | ∀ (m : ℕ), n ≤ m → Ideal.map (floc s) (I n) = Ideal.map (floc s) (I m)}<VAR>minN : R → ℕ := fun s => sInf (suitableN s)<VAR>hSuit : ∀ (s : { x // x ∈ S }), minN ↑s ∈ suitableN ↑s<VAR>N : ℕ := S.sup minN<VAR>hN : ∀ (s : { x // x ∈ S }), minN ↑s ≤ N<VAR>n : ℕ<VAR>hn : N ≤ n<GOAL>I N = I n
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>S : Finset R<VAR>hS : Ideal.span ↑S = ⊤<VAR>hN✝ : ∀ (s : { x // x ∈ S }), IsNoetherianRing (Localization.Away ↑s)<VAR>I : ℕ →o Submodule R R<VAR>floc : (s : R) → R →+* Localization.Away s := fun s => algebraMap R (Localization.Away s)<VAR>suitableN : R → Set ℕ := fun s => {n | ∀ (m : ℕ), n ≤ m → Ideal.map (floc s) (I n) = Ideal.map (floc s) (I m)}<VAR>minN : R → ℕ := fun s => sInf (suitableN s)<VAR>hSuit : ∀ (s : { x // x ∈ S }), minN ↑s ∈ suitableN ↑s<VAR>N : ℕ := S.sup minN<VAR>hN : ∀ (s : { x // x ∈ S }), minN ↑s ≤ N<VAR>n : ℕ<VAR>hn : N ≤ n<GOAL>⨅ x, Ideal.comap (algebraMap R (Localization.Away ↑x)) (Ideal.map (algebraMap R (Localization.Away ↑x)) (I N)) = ⨅ x, Ideal.comap (algebraMap R (Localization.Away ↑x)) (Ideal.map (algebraMap R (Localization.Away ↑x)) (I n))
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>S : Finset R<VAR>hS : Ideal.span ↑S = ⊤<VAR>hN✝ : ∀ (s : { x // x ∈ S }), IsNoetherianRing (Localization.Away ↑s)<VAR>I : ℕ →o Submodule R R<VAR>floc : (s : R) → R →+* Localization.Away s := fun s => algebraMap R (Localization.Away s)<VAR>suitableN : R → Set ℕ := fun s => {n | ∀ (m : ℕ), n ≤ m → Ideal.map (floc s) (I n) = Ideal.map (floc s) (I m)}<VAR>minN : R → ℕ := fun s => sInf (suitableN s)<VAR>hSuit : ∀ (s : { x // x ∈ S }), minN ↑s ∈ suitableN ↑s<VAR>N : ℕ := S.sup minN<VAR>hN : ∀ (s : { x // x ∈ S }), minN ↑s ≤ N<VAR>n : ℕ<VAR>hn : N ≤ n<GOAL>∀ (i : { f // f ∈ S }), Ideal.comap (algebraMap R (Localization.Away ↑i)) (Ideal.map (algebraMap R (Localization.Away ↑i)) (I N)) = Ideal.comap (algebraMap R (Localization.Away ↑i)) (Ideal.map (algebraMap R (Localization.Away ↑i)) (I n))
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>S : Finset R<VAR>hS : Ideal.span ↑S = ⊤<VAR>hN✝ : ∀ (s : { x // x ∈ S }), IsNoetherianRing (Localization.Away ↑s)<VAR>I : ℕ →o Submodule R R<VAR>floc : (s : R) → R →+* Localization.Away s := fun s => algebraMap R (Localization.Away s)<VAR>suitableN : R → Set ℕ := fun s => {n | ∀ (m : ℕ), n ≤ m → Ideal.map (floc s) (I n) = Ideal.map (floc s) (I m)}<VAR>minN : R → ℕ := fun s => sInf (suitableN s)<VAR>hSuit : ∀ (s : { x // x ∈ S }), minN ↑s ∈ suitableN ↑s<VAR>N : ℕ := S.sup minN<VAR>hN : ∀ (s : { x // x ∈ S }), minN ↑s ≤ N<VAR>n : ℕ<VAR>hn : N ≤ n<VAR>s : { f // f ∈ S }<GOAL>Ideal.map (floc ↑s) (I (minN ↑s)) = Ideal.map (algebraMap R (Localization.Away ↑s)) (I n)
<VAR>α : Type u_1<VAR>α' : 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>ε : Type u_9<VAR>ε' : Type u_10<VAR>m : α → β → γ<VAR>f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>h h₁ h₂ : Filter γ<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>u : Set γ<VAR>v : Set δ<VAR>a : α<VAR>b : β<VAR>c : γ<GOAL>(map₂ m f g).NeBot ↔ f.NeBot ∧ g.NeBot
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>γ : Type x<VAR>ι : Type u_1<VAR>inst✝ : Finite ι<VAR>κ : ι → Type u_2<VAR>t : (i : ι) → Set (κ i)<VAR>ht : ∀ (i : ι), (t i).Finite<GOAL>{f | ∀ (i : ι), f i ∈ t i}.Finite
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>k : ℕ<VAR>N N₁ N₂ : LieSubmodule R L M<GOAL>LieModule.IsNilpotent R L M ↔ ∃ k, ucs k ⊥ = ⊤
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>k : ℕ<VAR>N N₁ N₂ : LieSubmodule R L M<GOAL>(∃ k, LieModule.lowerCentralSeries R L M k = ⊥) ↔ ∃ k, ucs k ⊥ = ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Semiring α<VAR>I : Ideal α<VAR>a b : α<VAR>s : Set (Ideal α)<VAR>hs : s.Nonempty<VAR>hs' : IsChain (fun x x_1 => x ≤ x_1) s<VAR>H : ∀ p ∈ s, p.IsPrime<VAR>x✝ y✝ : α<VAR>e : x✝ * y✝ ∈ sInf s<VAR>hx : x✝ ∉ sInf s<GOAL>y✝ ∈ sInf s
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Semiring α<VAR>I : Ideal α<VAR>a b : α<VAR>s : Set (Ideal α)<VAR>hs : s.Nonempty<VAR>hs' : IsChain (fun x x_1 => x ≤ x_1) s<VAR>H : ∀ p ∈ s, p.IsPrime<VAR>x✝ y✝ : α<VAR>e : ∀ ⦃I : Ideal α⦄, I ∈ s → x✝ * y✝ ∈ I<VAR>hx : ¬∀ ⦃I : Ideal α⦄, I ∈ s → x✝ ∈ I<GOAL>∀ ⦃I : Ideal α⦄, I ∈ s → y✝ ∈ I
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Semiring α<VAR>I✝ : Ideal α<VAR>a b : α<VAR>s : Set (Ideal α)<VAR>hs : s.Nonempty<VAR>hs' : IsChain (fun x x_1 => x ≤ x_1) s<VAR>H : ∀ p ∈ s, p.IsPrime<VAR>x✝ y✝ : α<VAR>e : ∀ ⦃I : Ideal α⦄, I ∈ s → x✝ * y✝ ∈ I<VAR>I : Ideal α<VAR>hI : I ∈ s<VAR>hI' : x✝ ∉ I<VAR>J : Ideal α<VAR>hJ : J ∈ s<GOAL>y✝ ∈ J
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Semiring α<VAR>I✝ : Ideal α<VAR>a b : α<VAR>s : Set (Ideal α)<VAR>hs : s.Nonempty<VAR>hs' : IsChain (fun x x_1 => x ≤ x_1) s<VAR>H : ∀ p ∈ s, p.IsPrime<VAR>x✝ y✝ : α<VAR>e : ∀ ⦃I : Ideal α⦄, I ∈ s → x✝ * y✝ ∈ I<VAR>I : Ideal α<VAR>hI : I ∈ s<VAR>hI' : x✝ ∉ I<VAR>J : Ideal α<VAR>hJ : J ∈ s<VAR>h : I ≤ J<GOAL>y✝ ∈ J
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Semiring α<VAR>I✝ : Ideal α<VAR>a b : α<VAR>s : Set (Ideal α)<VAR>hs : s.Nonempty<VAR>hs' : IsChain (fun x x_1 => x ≤ x_1) s<VAR>H : ∀ p ∈ s, p.IsPrime<VAR>x✝ y✝ : α<VAR>e : ∀ ⦃I : Ideal α⦄, I ∈ s → x✝ * y✝ ∈ I<VAR>I : Ideal α<VAR>hI : I ∈ s<VAR>hI' : x✝ ∉ I<VAR>J : Ideal α<VAR>hJ : J ∈ s<VAR>h : J ≤ I<GOAL>y✝ ∈ J
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : Finite Rˣ<VAR>χ : MulChar R ℂ<VAR>a : R<GOAL>star (χ a) = χ⁻¹ a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M✝ : Matroid α<VAR>F X✝ Y✝ : Set α<VAR>e : α<VAR>M : Matroid α<VAR>X Y : Set α<GOAL>M.closure (X ∪ M.closure Y) = M.closure (X ∪ Y)
<VAR>R : Type u<VAR>inst✝³ : NonUnitalSemiring R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>x y : R<GOAL>star x ≤ star y ↔ x ≤ y
<VAR>R : Type u<VAR>inst✝³ : NonUnitalSemiring R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>x y : R<GOAL>∀ (x y : R), x ≤ y → star x ≤ star y
<VAR>R : Type u<VAR>inst✝³ : NonUnitalSemiring R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>x✝ y✝ x y : R<VAR>h : x ≤ y<GOAL>star x ≤ star y
<VAR>R : Type u<VAR>inst✝³ : NonUnitalSemiring R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>x✝ y✝ x y : R<VAR>h : ∃ p ∈ AddSubmonoid.closure (range fun s => star s * s), y = x + p<GOAL>∃ p ∈ AddSubmonoid.closure (range fun s => star s * s), star y = star x + p
<VAR>R : Type u<VAR>inst✝³ : NonUnitalSemiring R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>x✝ y x d : R<VAR>hd : d ∈ AddSubmonoid.closure (range fun s => star s * s)<GOAL>∃ p ∈ AddSubmonoid.closure (range fun s => star s * s), star (x + d) = star x + p
<VAR>R : Type u<VAR>inst✝³ : NonUnitalSemiring R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>x✝ y x d : R<VAR>hd : d ∈ AddSubmonoid.closure (range fun s => star s * s)<GOAL>starAddEquiv d ∈ AddSubmonoid.closure (range fun s => star s * s)
<VAR>R : Type u<VAR>inst✝³ : NonUnitalSemiring R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>x✝ y x d : R<VAR>hd : d ∈ AddSubmonoid.closure (range fun s => star s * s)<GOAL>(range fun s => star s * s) ⊆ ⇑starAddEquiv ⁻¹' range fun s => star s * s
<VAR>α : Type u<VAR>β : Type v<VAR>f fa g : α → α<VAR>x y : α<VAR>fb : β → β<VAR>m n k : ℕ<VAR>e : Perm α<VAR>h : Function.Commute f g<GOAL>Set.BijOn f (fixedPoints (f ∘ g)) (fixedPoints (f ∘ g))
<VAR>n : ℕ<GOAL>(n + 1).descFactorial (0 + 1) = (n + 1) * n.descFactorial 0
<VAR>n k : ℕ<GOAL>(n + 1).descFactorial (k.succ + 1) = (n + 1) * n.descFactorial k.succ
<VAR>R : CommRingCat<VAR>U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace<VAR>x✝ : (forget CommRingCat).obj ((sheafedSpaceObj R).presheaf.obj (op U✝))<GOAL>((structureSheaf ↑R).val.map (𝟙 (op ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U✝)))) ((comap (𝟙 R) U✝ ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U✝) ⋯) x✝) = (𝟙 ((structureSheaf ↑R).val.obj (op U✝))) x✝
<VAR>R : CommRingCat<VAR>U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace<VAR>x✝ : (forget CommRingCat).obj ((sheafedSpaceObj R).presheaf.obj (op U✝))<GOAL>((structureSheaf ↑R).val.map (𝟙 (op ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U✝)))) ((eqToHom ⋯) x✝) = (𝟙 ((structureSheaf ↑R).val.obj (op U✝))) x✝
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : DecidableEq p<VAR>inst✝ : CommRing R<VAR>r : ℕ<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>hM : M (inr ()) (inr ()) ≠ 0<VAR>i : Fin r<GOAL>((listTransvecCol M).prod * M * (listTransvecRow M).prod) (inr ()) (inl i) = 0
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : DecidableEq p<VAR>inst✝ : CommRing R<VAR>r : ℕ<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>hM : M (inr ()) (inr ()) ≠ 0<VAR>i : Fin r<VAR>this : listTransvecRow M = listTransvecRow ((listTransvecCol M).prod * M)<GOAL>((listTransvecCol M).prod * M * (listTransvecRow M).prod) (inr ()) (inl i) = 0
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : DecidableEq p<VAR>inst✝ : CommRing R<VAR>r : ℕ<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>hM : M (inr ()) (inr ()) ≠ 0<VAR>i : Fin r<VAR>this : listTransvecRow M = listTransvecRow ((listTransvecCol M).prod * M)<GOAL>((listTransvecCol M).prod * M * (listTransvecRow ((listTransvecCol M).prod * M)).prod) (inr ()) (inl i) = 0
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : DecidableEq p<VAR>inst✝ : CommRing R<VAR>r : ℕ<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>hM : M (inr ()) (inr ()) ≠ 0<VAR>i : Fin r<VAR>this : listTransvecRow M = listTransvecRow ((listTransvecCol M).prod * M)<GOAL>((listTransvecCol M).prod * M) (inr ()) (inr ()) ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f : α → β<VAR>s✝ t s : Set α<VAR>σ : Equiv.Perm α<VAR>hs : {a | σ a ≠ a} ⊆ s<VAR>i : α<GOAL>i ∈ ⇑σ '' s ↔ i ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f : α → β<VAR>s✝ t s : Set α<VAR>σ : Equiv.Perm α<VAR>hs : {a | σ a ≠ a} ⊆ s<VAR>i : α<VAR>hi : σ i = i<GOAL>i ∈ ⇑σ '' s ↔ i ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f : α → β<VAR>s✝ t s : Set α<VAR>σ : Equiv.Perm α<VAR>hs : {a | σ a ≠ a} ⊆ s<VAR>i : α<VAR>hi : σ i ≠ i<GOAL>i ∈ ⇑σ '' s ↔ i ∈ s
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>ai : R<VAR>au : ai * a = 1<GOAL>p.natDegree = (1 * p).natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>ai : R<VAR>au : ai * a = 1<GOAL>(1 * p).natDegree = (C ai * (C a * p)).natDegree
<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>inst✝ : TopologicalSpace α<VAR>x✝³ : α<VAR>x✝² : x✝³ ∈ s<VAR>x✝¹ : Set (β × β)<VAR>x✝ : x✝¹ ∈ 𝓤 β<GOAL>(∃ t ∈ 𝓝[s] x✝³, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ x✝¹) ↔ x✝¹ ∈ map (fun y => (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x✝³)
<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>inst✝ : TopologicalSpace α<VAR>x✝³ : α<VAR>x✝² : x✝³ ∈ s<VAR>x✝¹ : Set (β × β)<VAR>x✝ : x✝¹ ∈ 𝓤 β<GOAL>(∃ t ∈ 𝓝[s] x✝³, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ x✝¹) ↔ ∃ t ∈ 𝓝[s] x✝³, ∀ᶠ (x : ι) in p, ∀ y ∈ t, (x, y) ∈ (fun y => (f y.2, F y.1 y.2)) ⁻¹' x✝¹
<VAR>R : Type u<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>Rₚ : Type v<VAR>inst✝¹⁰ : CommSemiring Rₚ<VAR>inst✝⁹ : Algebra R Rₚ<VAR>inst✝⁸ : IsLocalization S Rₚ<VAR>M : Type w<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>Mₚ : Type t<VAR>inst✝⁵ : AddCommMonoid Mₚ<VAR>inst✝⁴ : Module R Mₚ<VAR>inst✝³ : Module Rₚ Mₚ<VAR>inst✝² : IsScalarTower R Rₚ Mₚ<VAR>f : M →ₗ[R] Mₚ<VAR>inst✝¹ : IsLocalizedModule S f<VAR>inst✝ : Finite R M<VAR>T : Finset M<VAR>hT : Submodule.span R ↑T = ⊤<GOAL>Finite Rₚ Mₚ
<VAR>R : Type u<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>Rₚ : Type v<VAR>inst✝¹⁰ : CommSemiring Rₚ<VAR>inst✝⁹ : Algebra R Rₚ<VAR>inst✝⁸ : IsLocalization S Rₚ<VAR>M : Type w<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>Mₚ : Type t<VAR>inst✝⁵ : AddCommMonoid Mₚ<VAR>inst✝⁴ : Module R Mₚ<VAR>inst✝³ : Module Rₚ Mₚ<VAR>inst✝² : IsScalarTower R Rₚ Mₚ<VAR>f : M →ₗ[R] Mₚ<VAR>inst✝¹ : IsLocalizedModule S f<VAR>inst✝ : Finite R M<VAR>T : Finset M<VAR>hT : Submodule.span R ↑T = ⊤<GOAL>Submodule.span Rₚ ↑(Finset.image (⇑f) T) = ⊤
<VAR>R : Type u<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>Rₚ : Type v<VAR>inst✝¹⁰ : CommSemiring Rₚ<VAR>inst✝⁹ : Algebra R Rₚ<VAR>inst✝⁸ : IsLocalization S Rₚ<VAR>M : Type w<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>Mₚ : Type t<VAR>inst✝⁵ : AddCommMonoid Mₚ<VAR>inst✝⁴ : Module R Mₚ<VAR>inst✝³ : Module Rₚ Mₚ<VAR>inst✝² : IsScalarTower R Rₚ Mₚ<VAR>f : M →ₗ[R] Mₚ<VAR>inst✝¹ : IsLocalizedModule S f<VAR>inst✝ : Finite R M<VAR>T : Finset M<VAR>hT : Submodule.span R ↑T = ⊤<GOAL>⊤ ≤ Submodule.span Rₚ ↑(Finset.image (⇑f) T)
<VAR>R : Type u<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>Rₚ : Type v<VAR>inst✝¹⁰ : CommSemiring Rₚ<VAR>inst✝⁹ : Algebra R Rₚ<VAR>inst✝⁸ : IsLocalization S Rₚ<VAR>M : Type w<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>Mₚ : Type t<VAR>inst✝⁵ : AddCommMonoid Mₚ<VAR>inst✝⁴ : Module R Mₚ<VAR>inst✝³ : Module Rₚ Mₚ<VAR>inst✝² : IsScalarTower R Rₚ Mₚ<VAR>f : M →ₗ[R] Mₚ<VAR>inst✝¹ : IsLocalizedModule S f<VAR>inst✝ : Finite R M<VAR>T : Finset M<VAR>hT : Submodule.span R ↑T = ⊤<VAR>x : Mₚ<GOAL>x ∈ Submodule.span Rₚ ↑(Finset.image (⇑f) T)
<VAR>R : Type u<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>Rₚ : Type v<VAR>inst✝¹⁰ : CommSemiring Rₚ<VAR>inst✝⁹ : Algebra R Rₚ<VAR>inst✝⁸ : IsLocalization S Rₚ<VAR>M : Type w<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>Mₚ : Type t<VAR>inst✝⁵ : AddCommMonoid Mₚ<VAR>inst✝⁴ : Module R Mₚ<VAR>inst✝³ : Module Rₚ Mₚ<VAR>inst✝² : IsScalarTower R Rₚ Mₚ<VAR>f : M →ₗ[R] Mₚ<VAR>inst✝¹ : IsLocalizedModule S f<VAR>inst✝ : Finite R M<VAR>T : Finset M<VAR>hT : Submodule.span R ↑T = ⊤<VAR>x : Mₚ<VAR>y : M<VAR>m : ↥S<VAR>hyx : IsLocalizedModule.mk' f y m = x<GOAL>x ∈ Submodule.span Rₚ ↑(Finset.image (⇑f) T)
<VAR>R : Type u<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>Rₚ : Type v<VAR>inst✝¹⁰ : CommSemiring Rₚ<VAR>inst✝⁹ : Algebra R Rₚ<VAR>inst✝⁸ : IsLocalization S Rₚ<VAR>M : Type w<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>Mₚ : Type t<VAR>inst✝⁵ : AddCommMonoid Mₚ<VAR>inst✝⁴ : Module R Mₚ<VAR>inst✝³ : Module Rₚ Mₚ<VAR>inst✝² : IsScalarTower R Rₚ Mₚ<VAR>f : M →ₗ[R] Mₚ<VAR>inst✝¹ : IsLocalizedModule S f<VAR>inst✝ : Finite R M<VAR>T : Finset M<VAR>hT : Submodule.span R ↑T = ⊤<VAR>x : Mₚ<VAR>y : M<VAR>m : ↥S<VAR>hyx : IsLocalizedModule.mk' f y m = x<VAR>hy : y ∈ Submodule.span R ↑T<GOAL>x ∈ Submodule.span Rₚ ↑(Finset.image (⇑f) T)
<VAR>R : Type u<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>Rₚ : Type v<VAR>inst✝¹⁰ : CommSemiring Rₚ<VAR>inst✝⁹ : Algebra R Rₚ<VAR>inst✝⁸ : IsLocalization S Rₚ<VAR>M : Type w<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>Mₚ : Type t<VAR>inst✝⁵ : AddCommMonoid Mₚ<VAR>inst✝⁴ : Module R Mₚ<VAR>inst✝³ : Module Rₚ Mₚ<VAR>inst✝² : IsScalarTower R Rₚ Mₚ<VAR>f : M →ₗ[R] Mₚ<VAR>inst✝¹ : IsLocalizedModule S f<VAR>inst✝ : Finite R M<VAR>T : Finset M<VAR>hT : Submodule.span R ↑T = ⊤<VAR>x : Mₚ<VAR>y : M<VAR>m : ↥S<VAR>hyx : IsLocalizedModule.mk' f y m = x<VAR>hy : y ∈ Submodule.span R ↑T<VAR>this : f y ∈ Submodule.map f (Submodule.span R ↑T)<GOAL>x ∈ Submodule.span Rₚ ↑(Finset.image (⇑f) T)
<VAR>R : Type u<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>Rₚ : Type v<VAR>inst✝¹⁰ : CommSemiring Rₚ<VAR>inst✝⁹ : Algebra R Rₚ<VAR>inst✝⁸ : IsLocalization S Rₚ<VAR>M : Type w<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>Mₚ : Type t<VAR>inst✝⁵ : AddCommMonoid Mₚ<VAR>inst✝⁴ : Module R Mₚ<VAR>inst✝³ : Module Rₚ Mₚ<VAR>inst✝² : IsScalarTower R Rₚ Mₚ<VAR>f : M →ₗ[R] Mₚ<VAR>inst✝¹ : IsLocalizedModule S f<VAR>inst✝ : Finite R M<VAR>T : Finset M<VAR>hT : Submodule.span R ↑T = ⊤<VAR>x : Mₚ<VAR>y : M<VAR>m : ↥S<VAR>hyx : IsLocalizedModule.mk' f y m = x<VAR>hy : y ∈ Submodule.span R ↑T<VAR>this : f y ∈ Submodule.span R (⇑f '' ↑T)<GOAL>x ∈ Submodule.span Rₚ ↑(Finset.image (⇑f) T)
<VAR>R : Type u<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>Rₚ : Type v<VAR>inst✝¹⁰ : CommSemiring Rₚ<VAR>inst✝⁹ : Algebra R Rₚ<VAR>inst✝⁸ : IsLocalization S Rₚ<VAR>M : Type w<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>Mₚ : Type t<VAR>inst✝⁵ : AddCommMonoid Mₚ<VAR>inst✝⁴ : Module R Mₚ<VAR>inst✝³ : Module Rₚ Mₚ<VAR>inst✝² : IsScalarTower R Rₚ Mₚ<VAR>f : M →ₗ[R] Mₚ<VAR>inst✝¹ : IsLocalizedModule S f<VAR>inst✝ : Finite R M<VAR>T : Finset M<VAR>hT : Submodule.span R ↑T = ⊤<VAR>x : Mₚ<VAR>y : M<VAR>m : ↥S<VAR>hyx : IsLocalizedModule.mk' f y m = x<VAR>hy : y ∈ Submodule.span R ↑T<VAR>this : f y ∈ Submodule.span R (⇑f '' ↑T)<VAR>H : Submodule.span R (⇑f '' ↑T) ≤ Submodule.restrictScalars R (Submodule.span Rₚ (⇑f '' ↑T))<GOAL>x ∈ Submodule.span Rₚ ↑(Finset.image (⇑f) T)
<VAR>R : Type u<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>Rₚ : Type v<VAR>inst✝¹⁰ : CommSemiring Rₚ<VAR>inst✝⁹ : Algebra R Rₚ<VAR>inst✝⁸ : IsLocalization S Rₚ<VAR>M : Type w<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>Mₚ : Type t<VAR>inst✝⁵ : AddCommMonoid Mₚ<VAR>inst✝⁴ : Module R Mₚ<VAR>inst✝³ : Module Rₚ Mₚ<VAR>inst✝² : IsScalarTower R Rₚ Mₚ<VAR>f : M →ₗ[R] Mₚ<VAR>inst✝¹ : IsLocalizedModule S f<VAR>inst✝ : Finite R M<VAR>T : Finset M<VAR>hT : Submodule.span R ↑T = ⊤<VAR>x : Mₚ<VAR>y : M<VAR>m : ↥S<VAR>hyx : IsLocalizedModule.mk' f y m = x<VAR>hy : y ∈ Submodule.span R ↑T<VAR>this : f y ∈ Submodule.span R (⇑f '' ↑T)<VAR>H : Submodule.span R (⇑f '' ↑T) ≤ Submodule.restrictScalars R (Submodule.span Rₚ (⇑f '' ↑T))<GOAL>x = IsLocalization.mk' Rₚ 1 m • f y
<VAR>R : Type u<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>Rₚ : Type v<VAR>inst✝¹⁰ : CommSemiring Rₚ<VAR>inst✝⁹ : Algebra R Rₚ<VAR>inst✝⁸ : IsLocalization S Rₚ<VAR>M : Type w<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>Mₚ : Type t<VAR>inst✝⁵ : AddCommMonoid Mₚ<VAR>inst✝⁴ : Module R Mₚ<VAR>inst✝³ : Module Rₚ Mₚ<VAR>inst✝² : IsScalarTower R Rₚ Mₚ<VAR>f : M →ₗ[R] Mₚ<VAR>inst✝¹ : IsLocalizedModule S f<VAR>inst✝ : Finite R M<VAR>T : Finset M<VAR>hT : Submodule.span R ↑T = ⊤<VAR>x : Mₚ<VAR>y : M<VAR>m : ↥S<VAR>hyx : IsLocalizedModule.mk' f y m = x<VAR>hy : y ∈ Submodule.span R ↑T<VAR>this : f y ∈ Submodule.span R (⇑f '' ↑T)<VAR>H : Submodule.span R (⇑f '' ↑T) ≤ Submodule.restrictScalars R (Submodule.span Rₚ (⇑f '' ↑T))<GOAL>Submodule.span Rₚ ↑(Finset.image (⇑f) T) = Submodule.span Rₚ (⇑f '' ↑T)
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>inst✝⁴ : NonUnitalNonAssocSemiring R<VAR>M : Subsemigroup R<VAR>inst✝³ : NonUnitalNonAssocSemiring S✝<VAR>inst✝² : NonUnitalNonAssocSemiring T<VAR>F : Type u_1<VAR>inst✝¹ : FunLike F R S✝<VAR>inst✝ : NonUnitalRingHomClass F R S✝<VAR>S : Set (NonUnitalSubsemiring R)<VAR>Sne : S.Nonempty<VAR>hS : DirectedOn (fun x x_1 => x ≤ x_1) S<VAR>x : R<GOAL>x ∈ ↑(sSup S) ↔ x ∈ ⋃ s ∈ S, ↑s
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>cR : Type u<VAR>inst✝ : CommRing cR<VAR>s : Set R<VAR>C : R → Prop<VAR>x : R<VAR>hx : x ∈ closure s<VAR>h1 : C 1<VAR>hneg1 : C (-1)<VAR>hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)<VAR>ha : ∀ {x y : R}, C x → C y → C (x + y)<GOAL>C x
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>cR : Type u<VAR>inst✝ : CommRing cR<VAR>s : Set R<VAR>C : R → Prop<VAR>x : R<VAR>hx : x ∈ closure s<VAR>h1 : C 1<VAR>hneg1 : C (-1)<VAR>hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)<VAR>ha : ∀ {x y : R}, C x → C y → C (x + y)<VAR>h0 : C 0<GOAL>C x
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>cR : Type u<VAR>inst✝ : CommRing cR<VAR>s : Set R<VAR>C : R → Prop<VAR>h1 : C 1<VAR>hneg1 : C (-1)<VAR>hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)<VAR>ha : ∀ {x y : R}, C x → C y → C (x + y)<VAR>h0 : C 0<VAR>L : List (List R)<VAR>HL : ∀ l ∈ L, ∀ x ∈ l, x ∈ s ∨ x = -1<VAR>hx : (List.map List.prod L).sum ∈ closure s<GOAL>C (List.map List.prod L).sum
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>cR : Type u<VAR>inst✝ : CommRing cR<VAR>s : Set R<VAR>C : R → Prop<VAR>h1 : C 1<VAR>hneg1 : C (-1)<VAR>hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)<VAR>ha : ∀ {x y : R}, C x → C y → C (x + y)<VAR>h0 : C 0<VAR>hd : List R<VAR>tl : List (List R)<VAR>ih : (∀ l ∈ tl, ∀ x ∈ l, x ∈ s ∨ x = -1) → C (List.map List.prod tl).sum<VAR>HL : ∀ l ∈ hd :: tl, ∀ x ∈ l, x ∈ s ∨ x = -1<GOAL>C (List.map List.prod (hd :: tl)).sum
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>cR : Type u<VAR>inst✝ : CommRing cR<VAR>s : Set R<VAR>C : R → Prop<VAR>h1 : C 1<VAR>hneg1 : C (-1)<VAR>hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)<VAR>ha : ∀ {x y : R}, C x → C y → C (x + y)<VAR>h0 : C 0<VAR>hd : List R<VAR>tl : List (List R)<VAR>ih : (∀ l ∈ tl, ∀ x ∈ l, x ∈ s ∨ x = -1) → C (List.map List.prod tl).sum<VAR>HL : (∀ x ∈ hd, x ∈ s ∨ x = -1) ∧ ∀ x ∈ tl, ∀ x_1 ∈ x, x_1 ∈ s ∨ x_1 = -1<GOAL>C (List.map List.prod (hd :: tl)).sum
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>cR : Type u<VAR>inst✝ : CommRing cR<VAR>s : Set R<VAR>C : R → Prop<VAR>h1 : C 1<VAR>hneg1 : C (-1)<VAR>hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)<VAR>ha : ∀ {x y : R}, C x → C y → C (x + y)<VAR>h0 : C 0<VAR>hd : List R<VAR>tl : List (List R)<VAR>ih : (∀ l ∈ tl, ∀ x ∈ l, x ∈ s ∨ x = -1) → C (List.map List.prod tl).sum<VAR>HL : (∀ x ∈ hd, x ∈ s ∨ x = -1) ∧ ∀ x ∈ tl, ∀ x_1 ∈ x, x_1 ∈ s ∨ x_1 = -1<GOAL>C hd.prod