ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : 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>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : LieRingModule L N<VAR>inst✝ : LieModule R L N<VAR>x : L<GOAL>x ∈ LieModule.ker R L M ↔ ∀ (m : M), ⁅x, m⁆ = 0
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u<VAR>S : Type v<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>inst✝¹ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>s t : Set σ<VAR>inst✝ : Nontrivial R<VAR>i : σ<GOAL>X i ∈ supported R s ↔ i ∈ s
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>Q : Type uQ<VAR>P' : Type uP'<VAR>Q' : Type uQ'<VAR>inst✝³¹ : CommSemiring R<VAR>inst✝³⁰ : Semiring A<VAR>inst✝²⁹ : Semiring B<VAR>inst✝²⁸ : Algebra R A<VAR>inst✝²⁷ : Algebra R B<VAR>inst✝²⁶ : AddCommMonoid M<VAR>inst✝²⁵ : Module R M<VAR>inst✝²⁴ : Module A M<VAR>inst✝²³ : Module B M<VAR>inst✝²² : IsScalarTower R A M<VAR>inst✝²¹ : IsScalarTower R B M<VAR>inst✝²⁰ : SMulCommClass A B M<VAR>inst✝¹⁹ : AddCommMonoid N<VAR>inst✝¹⁸ : Module R N<VAR>inst✝¹⁷ : AddCommMonoid P<VAR>inst✝¹⁶ : Module R P<VAR>inst✝¹⁵ : Module A P<VAR>inst✝¹⁴ : Module B P<VAR>inst✝¹³ : IsScalarTower R A P<VAR>inst✝¹² : IsScalarTower R B P<VAR>inst✝¹¹ : SMulCommClass A B P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : Module R Q<VAR>inst✝⁸ : AddCommMonoid P'<VAR>inst✝⁷ : Module R P'<VAR>inst✝⁶ : Module A P'<VAR>inst✝⁵ : Module B P'<VAR>inst✝⁴ : IsScalarTower R A P'<VAR>inst✝³ : IsScalarTower R B P'<VAR>inst✝² : SMulCommClass A B P'<VAR>inst✝¹ : AddCommMonoid Q'<VAR>inst✝ : Module R Q'<VAR>f₁ f₂ : M →ₗ[A] P<VAR>g : N →ₗ[R] Q<VAR>x✝¹ : M<VAR>x✝ : N<GOAL>((curry (map (f₁ + f₂) g)) x✝¹) x✝ = ((curry (map f₁ g + map f₂ g)) x✝¹) x✝
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f : R<VAR>s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))<VAR>ι : Type u := ↥(PrimeSpectrum.basicOpen f)<GOAL>∃ a, (toBasicOpen R f) a = s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f : R<VAR>s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))<VAR>ι : Type u := ↥(PrimeSpectrum.basicOpen f)<VAR>a' h' : ↥(PrimeSpectrum.basicOpen f) → R<VAR>iDh' : (x : ↥(PrimeSpectrum.basicOpen f)) → PrimeSpectrum.basicOpen (h' x) ⟶ PrimeSpectrum.basicOpen f<VAR>hxDh' : ∀ (x : ↥(PrimeSpectrum.basicOpen f)), ↑x ∈ PrimeSpectrum.basicOpen (h' x)<VAR>s_eq' : ∀ (x : ↥(PrimeSpectrum.basicOpen f)), const R (a' x) (h' x) (PrimeSpectrum.basicOpen (h' x)) ⋯ = ((structureSheaf R).val.map (iDh' x).op) s<GOAL>∃ a, (toBasicOpen R f) a = s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f : R<VAR>s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))<VAR>ι : Type u := ↥(PrimeSpectrum.basicOpen f)<VAR>a' h' : ↥(PrimeSpectrum.basicOpen f) → R<VAR>iDh' : (x : ↥(PrimeSpectrum.basicOpen f)) → PrimeSpectrum.basicOpen (h' x) ⟶ PrimeSpectrum.basicOpen f<VAR>hxDh' : ∀ (x : ↥(PrimeSpectrum.basicOpen f)), ↑x ∈ PrimeSpectrum.basicOpen (h' x)<VAR>s_eq' : ∀ (x : ↥(PrimeSpectrum.basicOpen f)), const R (a' x) (h' x) (PrimeSpectrum.basicOpen (h' x)) ⋯ = ((structureSheaf R).val.map (iDh' x).op) s<VAR>t : Finset ι<VAR>ht_cover' : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ i ∈ t, ↑(PrimeSpectrum.basicOpen (h' i))<GOAL>∃ a, (toBasicOpen R f) a = s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f : R<VAR>s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))<VAR>ι : Type u := ↥(PrimeSpectrum.basicOpen f)<VAR>a' h' : ↥(PrimeSpectrum.basicOpen f) → R<VAR>iDh' : (x : ↥(PrimeSpectrum.basicOpen f)) → PrimeSpectrum.basicOpen (h' x) ⟶ PrimeSpectrum.basicOpen f<VAR>hxDh' : ∀ (x : ↥(PrimeSpectrum.basicOpen f)), ↑x ∈ PrimeSpectrum.basicOpen (h' x)<VAR>s_eq' : ∀ (x : ↥(PrimeSpectrum.basicOpen f)), const R (a' x) (h' x) (PrimeSpectrum.basicOpen (h' x)) ⋯ = ((structureSheaf R).val.map (iDh' x).op) s<VAR>t : Finset ι<VAR>ht_cover' : PrimeSpectrum.basicOpen f ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h' i)<GOAL>∃ a, (toBasicOpen R f) a = s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f : R<VAR>s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))<VAR>ι : Type u := ↥(PrimeSpectrum.basicOpen f)<VAR>a' h' : ↥(PrimeSpectrum.basicOpen f) → R<VAR>iDh' : (x : ↥(PrimeSpectrum.basicOpen f)) → PrimeSpectrum.basicOpen (h' x) ⟶ PrimeSpectrum.basicOpen f<VAR>hxDh' : ∀ (x : ↥(PrimeSpectrum.basicOpen f)), ↑x ∈ PrimeSpectrum.basicOpen (h' x)<VAR>s_eq' : ∀ (x : ↥(PrimeSpectrum.basicOpen f)), const R (a' x) (h' x) (PrimeSpectrum.basicOpen (h' x)) ⋯ = ((structureSheaf R).val.map (iDh' x).op) s<VAR>t : Finset ι<VAR>ht_cover' : PrimeSpectrum.basicOpen f ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h' i)<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f<VAR>ht_cover : PrimeSpectrum.basicOpen f ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h i)<VAR>ah_ha : ∀ i ∈ t, ∀ j ∈ t, a i * h j = h i * a j<VAR>s_eq : ∀ i ∈ t, ((structureSheaf R).val.map (iDh i).op) s = const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯<GOAL>∃ a, (toBasicOpen R f) a = s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f : R<VAR>s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))<VAR>ι : Type u := ↥(PrimeSpectrum.basicOpen f)<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f<VAR>ht_cover : PrimeSpectrum.basicOpen f ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h i)<VAR>ah_ha : ∀ i ∈ t, ∀ j ∈ t, a i * h j = h i * a j<VAR>s_eq : ∀ i ∈ t, ((structureSheaf R).val.map (iDh i).op) s = const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯<GOAL>∃ a, (toBasicOpen R f) a = s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f : R<VAR>s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))<VAR>ι : Type u := ↥(PrimeSpectrum.basicOpen f)<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f<VAR>ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ i, ↑(⨆ (_ : i ∈ t), PrimeSpectrum.basicOpen (h i))<VAR>ah_ha : ∀ i ∈ t, ∀ j ∈ t, a i * h j = h i * a j<VAR>s_eq : ∀ i ∈ t, ((structureSheaf R).val.map (iDh i).op) s = const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯<GOAL>∃ a, (toBasicOpen R f) a = s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f : R<VAR>s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))<VAR>ι : Type u := ↥(PrimeSpectrum.basicOpen f)<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f<VAR>ah_ha : ∀ i ∈ t, ∀ j ∈ t, a i * h j = h i * a j<VAR>s_eq : ∀ i ∈ t, ((structureSheaf R).val.map (iDh i).op) s = const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯<VAR>ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ i ∈ t, ↑(PrimeSpectrum.basicOpen (h i))<GOAL>∃ a, (toBasicOpen R f) a = s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f : R<VAR>s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))<VAR>ι : Type u := ↥(PrimeSpectrum.basicOpen f)<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f<VAR>ah_ha : ∀ i ∈ t, ∀ j ∈ t, a i * h j = h i * a j<VAR>s_eq : ∀ i ∈ t, ((structureSheaf R).val.map (iDh i).op) s = const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯<VAR>ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ i ∈ t, ↑(PrimeSpectrum.basicOpen (h i))<VAR>n : ℕ<VAR>hn : f ^ n ∈ Ideal.span (h '' ↑t)<GOAL>∃ a, (toBasicOpen R f) a = s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f : R<VAR>s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))<VAR>ι : Type u := ↥(PrimeSpectrum.basicOpen f)<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f<VAR>ah_ha : ∀ i ∈ t, ∀ j ∈ t, a i * h j = h i * a j<VAR>s_eq : ∀ i ∈ t, ((structureSheaf R).val.map (iDh i).op) s = const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯<VAR>ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ i ∈ t, ↑(PrimeSpectrum.basicOpen (h i))<VAR>n : ℕ<VAR>hn : f ^ n * f ∈ Ideal.span (h '' ↑t)<GOAL>∃ a, (toBasicOpen R f) a = s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f : R<VAR>s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))<VAR>ι : Type u := ↥(PrimeSpectrum.basicOpen f)<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f<VAR>ah_ha : ∀ i ∈ t, ∀ j ∈ t, a i * h j = h i * a j<VAR>s_eq : ∀ i ∈ t, ((structureSheaf R).val.map (iDh i).op) s = const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯<VAR>ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ i ∈ t, ↑(PrimeSpectrum.basicOpen (h i))<VAR>n : ℕ<VAR>hn : ∃ l ∈ Finsupp.supported R R ↑t, (Finsupp.total ι R R h) l = f ^ (n + 1)<GOAL>∃ a, (toBasicOpen R f) a = s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f : R<VAR>s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))<VAR>ι : Type u := ↥(PrimeSpectrum.basicOpen f)<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f<VAR>ah_ha : ∀ i ∈ t, ∀ j ∈ t, a i * h j = h i * a j<VAR>s_eq : ∀ i ∈ t, ((structureSheaf R).val.map (iDh i).op) s = const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯<VAR>ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ i ∈ t, ↑(PrimeSpectrum.basicOpen (h i))<VAR>n : ℕ<VAR>b : ι →₀ R<VAR>b_supp : b ∈ Finsupp.supported R R ↑t<VAR>hb : (Finsupp.total ι R R h) b = f ^ (n + 1)<GOAL>∃ a, (toBasicOpen R f) a = s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f : R<VAR>s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))<VAR>ι : Type u := ↥(PrimeSpectrum.basicOpen f)<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f<VAR>ah_ha : ∀ i ∈ t, ∀ j ∈ t, a i * h j = h i * a j<VAR>s_eq : ∀ i ∈ t, ((structureSheaf R).val.map (iDh i).op) s = const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯<VAR>ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ i ∈ t, ↑(PrimeSpectrum.basicOpen (h i))<VAR>n : ℕ<VAR>b : ι →₀ R<VAR>b_supp : b ∈ Finsupp.supported R R ↑t<VAR>hb : ∑ i ∈ t, b i • h i = f ^ (n + 1)<GOAL>∃ a, (toBasicOpen R f) a = s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f : R<VAR>s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))<VAR>ι : Type u := ↥(PrimeSpectrum.basicOpen f)<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f<VAR>ah_ha : ∀ i ∈ t, ∀ j ∈ t, a i * h j = h i * a j<VAR>s_eq : ∀ i ∈ t, ((structureSheaf R).val.map (iDh i).op) s = const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯<VAR>ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ i ∈ t, ↑(PrimeSpectrum.basicOpen (h i))<VAR>n : ℕ<VAR>b : ι →₀ R<VAR>b_supp : b ∈ Finsupp.supported R R ↑t<VAR>hb : ∑ i ∈ t, b i * h i = f ^ (n + 1)<GOAL>∃ a, (toBasicOpen R f) a = s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f : R<VAR>s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))<VAR>ι : Type u := ↥(PrimeSpectrum.basicOpen f)<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f<VAR>ah_ha : ∀ i ∈ t, ∀ j ∈ t, a i * h j = h i * a j<VAR>s_eq : ∀ i ∈ t, ((structureSheaf R).val.map (iDh i).op) s = const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯<VAR>ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ i ∈ t, ↑(PrimeSpectrum.basicOpen (h i))<VAR>n : ℕ<VAR>b : ι →₀ R<VAR>b_supp : b ∈ Finsupp.supported R R ↑t<VAR>hb : ∑ i ∈ t, b i * h i = f ^ (n + 1)<GOAL>(toBasicOpen R f) (IsLocalization.mk' (Localization.Away f) (∑ i ∈ t, b i * a i) ⟨f ^ (n + 1), ⋯⟩) = s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f : R<VAR>s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))<VAR>ι : Type u := ↥(PrimeSpectrum.basicOpen f)<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f<VAR>ah_ha : ∀ i ∈ t, ∀ j ∈ t, a i * h j = h i * a j<VAR>s_eq : ∀ i ∈ t, ((structureSheaf R).val.map (iDh i).op) s = const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯<VAR>ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ i ∈ t, ↑(PrimeSpectrum.basicOpen (h i))<VAR>n : ℕ<VAR>b : ι →₀ R<VAR>b_supp : b ∈ Finsupp.supported R R ↑t<VAR>hb : ∑ i ∈ t, b i * h i = f ^ (n + 1)<GOAL>const R (∑ i ∈ t, b i * a i) (↑⟨f ^ (n + 1), ⋯⟩) (PrimeSpectrum.basicOpen f) ⋯ = s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f : R<VAR>s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))<VAR>ι : Type u := ↥(PrimeSpectrum.basicOpen f)<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f<VAR>ah_ha : ∀ i ∈ t, ∀ j ∈ t, a i * h j = h i * a j<VAR>s_eq : ∀ i ∈ t, ((structureSheaf R).val.map (iDh i).op) s = const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯<VAR>ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ i ∈ t, ↑(PrimeSpectrum.basicOpen (h i))<VAR>n : ℕ<VAR>b : ι →₀ R<VAR>b_supp : b ∈ Finsupp.supported R R ↑t<VAR>hb : ∑ i ∈ t, b i * h i = f ^ (n + 1)<VAR>tt : Type u := ↑↑t<GOAL>const R (∑ i ∈ t, b i * a i) (↑⟨f ^ (n + 1), ⋯⟩) (PrimeSpectrum.basicOpen f) ⋯ = s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f : R<VAR>s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))<VAR>ι : Type u := ↥(PrimeSpectrum.basicOpen f)<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f<VAR>ah_ha : ∀ i ∈ t, ∀ j ∈ t, a i * h j = h i * a j<VAR>s_eq : ∀ i ∈ t, ((structureSheaf R).val.map (iDh i).op) s = const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯<VAR>ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ i ∈ t, ↑(PrimeSpectrum.basicOpen (h i))<VAR>n : ℕ<VAR>b : ι →₀ R<VAR>b_supp : b ∈ Finsupp.supported R R ↑t<VAR>hb : ∑ i ∈ t, b i * h i = f ^ (n + 1)<VAR>tt : Type u := ↑↑t<GOAL>PrimeSpectrum.basicOpen f ≤ ⨆ i, PrimeSpectrum.basicOpen (h ↑i)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f : R<VAR>s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))<VAR>ι : Type u := ↥(PrimeSpectrum.basicOpen f)<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f<VAR>ah_ha : ∀ i ∈ t, ∀ j ∈ t, a i * h j = h i * a j<VAR>s_eq : ∀ i ∈ t, ((structureSheaf R).val.map (iDh i).op) s = const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯<VAR>ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ i ∈ t, ↑(PrimeSpectrum.basicOpen (h i))<VAR>n : ℕ<VAR>b : ι →₀ R<VAR>b_supp : b ∈ Finsupp.supported R R ↑t<VAR>hb : ∑ i ∈ t, b i * h i = f ^ (n + 1)<VAR>tt : Type u := ↑↑t<GOAL>∀ (i : tt), ((structureSheaf R).val.map (iDh ↑i).op) (const R (∑ i ∈ t, b i * a i) (↑⟨f ^ (n + 1), ⋯⟩) (PrimeSpectrum.basicOpen f) ⋯) = ((structureSheaf R).val.map (iDh ↑i).op) s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f : R<VAR>s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))<VAR>ι : Type u := ↥(PrimeSpectrum.basicOpen f)<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f<VAR>ah_ha : ∀ i ∈ t, ∀ j ∈ t, a i * h j = h i * a j<VAR>s_eq : ∀ i ∈ t, ((structureSheaf R).val.map (iDh i).op) s = const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯<VAR>ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ i ∈ t, ↑(PrimeSpectrum.basicOpen (h i))<VAR>n : ℕ<VAR>b : ι →₀ R<VAR>b_supp : b ∈ Finsupp.supported R R ↑t<VAR>hb : ∑ i ∈ t, b i * h i = f ^ (n + 1)<VAR>tt : Type u := ↑↑t<VAR>i : ι<VAR>hi : i ∈ ↑t<GOAL>((structureSheaf R).val.map (iDh i).op) (const R (∑ i ∈ t, b i * a i) (f ^ (n + 1)) (PrimeSpectrum.basicOpen f) ⋯) = ((structureSheaf R).val.map (iDh i).op) s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f : R<VAR>s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))<VAR>ι : Type u := ↥(PrimeSpectrum.basicOpen f)<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f<VAR>ah_ha : ∀ i ∈ t, ∀ j ∈ t, a i * h j = h i * a j<VAR>s_eq : ∀ i ∈ t, ((structureSheaf R).val.map (iDh i).op) s = const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯<VAR>ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ i ∈ t, ↑(PrimeSpectrum.basicOpen (h i))<VAR>n : ℕ<VAR>b : ι →₀ R<VAR>b_supp : b ∈ Finsupp.supported R R ↑t<VAR>hb : ∑ i ∈ t, b i * h i = f ^ (n + 1)<VAR>tt : Type u := ↑↑t<VAR>i : ι<VAR>hi : i ∈ ↑t<GOAL>const R (∑ i ∈ t, b i * a i) (f ^ (n + 1)) (PrimeSpectrum.basicOpen (h i)) ?h.h.mk.hv = const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f : R<VAR>s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))<VAR>ι : Type u := ↥(PrimeSpectrum.basicOpen f)<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f<VAR>ah_ha : ∀ i ∈ t, ∀ j ∈ t, a i * h j = h i * a j<VAR>s_eq : ∀ i ∈ t, ((structureSheaf R).val.map (iDh i).op) s = const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯<VAR>ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ i ∈ t, ↑(PrimeSpectrum.basicOpen (h i))<VAR>n : ℕ<VAR>b : ι →₀ R<VAR>b_supp : b ∈ Finsupp.supported R R ↑t<VAR>hb : ∑ i ∈ t, b i * h i = f ^ (n + 1)<VAR>tt : Type u := ↑↑t<VAR>i : ι<VAR>hi : i ∈ ↑t<GOAL>∀ x ∈ PrimeSpectrum.basicOpen (h i), f ^ (n + 1) ∈ x.asIdeal.primeCompl
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f : R<VAR>s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))<VAR>ι : Type u := ↥(PrimeSpectrum.basicOpen f)<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f<VAR>ah_ha : ∀ i ∈ t, ∀ j ∈ t, a i * h j = h i * a j<VAR>s_eq : ∀ i ∈ t, ((structureSheaf R).val.map (iDh i).op) s = const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯<VAR>ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ i ∈ t, ↑(PrimeSpectrum.basicOpen (h i))<VAR>n : ℕ<VAR>b : ι →₀ R<VAR>b_supp : b ∈ Finsupp.supported R R ↑t<VAR>hb : ∑ i ∈ t, b i * h i = f ^ (n + 1)<VAR>tt : Type u := ↑↑t<VAR>i : ι<VAR>hi : i ∈ ↑t<GOAL>const R (∑ i ∈ t, b i * a i) (f ^ (n + 1)) (PrimeSpectrum.basicOpen (h i)) ⋯ = const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f : R<VAR>s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))<VAR>ι : Type u := ↥(PrimeSpectrum.basicOpen f)<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f<VAR>ah_ha : ∀ i ∈ t, ∀ j ∈ t, a i * h j = h i * a j<VAR>s_eq : ∀ i ∈ t, ((structureSheaf R).val.map (iDh i).op) s = const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯<VAR>ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ i ∈ t, ↑(PrimeSpectrum.basicOpen (h i))<VAR>n : ℕ<VAR>b : ι →₀ R<VAR>b_supp : b ∈ Finsupp.supported R R ↑t<VAR>hb : ∑ i ∈ t, b i * h i = f ^ (n + 1)<VAR>tt : Type u := ↑↑t<VAR>i : ι<VAR>hi : i ∈ ↑t<GOAL>(∑ i ∈ t, b i * a i) * h i = a i * f ^ (n + 1)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f : R<VAR>s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))<VAR>ι : Type u := ↥(PrimeSpectrum.basicOpen f)<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f<VAR>ah_ha : ∀ i ∈ t, ∀ j ∈ t, a i * h j = h i * a j<VAR>s_eq : ∀ i ∈ t, ((structureSheaf R).val.map (iDh i).op) s = const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯<VAR>ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ i ∈ t, ↑(PrimeSpectrum.basicOpen (h i))<VAR>n : ℕ<VAR>b : ι →₀ R<VAR>b_supp : b ∈ Finsupp.supported R R ↑t<VAR>hb : ∑ i ∈ t, b i * h i = f ^ (n + 1)<VAR>tt : Type u := ↑↑t<VAR>i : ι<VAR>hi : i ∈ ↑t<GOAL>∑ i_1 ∈ t, b i_1 * a i_1 * h i = ∑ i_1 ∈ t, a i * (b i_1 * h i_1)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f : R<VAR>s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))<VAR>ι : Type u := ↥(PrimeSpectrum.basicOpen f)<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f<VAR>ah_ha : ∀ i ∈ t, ∀ j ∈ t, a i * h j = h i * a j<VAR>s_eq : ∀ i ∈ t, ((structureSheaf R).val.map (iDh i).op) s = const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯<VAR>ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ i ∈ t, ↑(PrimeSpectrum.basicOpen (h i))<VAR>n : ℕ<VAR>b : ι →₀ R<VAR>b_supp : b ∈ Finsupp.supported R R ↑t<VAR>hb : ∑ i ∈ t, b i * h i = f ^ (n + 1)<VAR>tt : Type u := ↑↑t<VAR>i : ι<VAR>hi : i ∈ ↑t<GOAL>∀ x ∈ t, b x * a x * h i = a i * (b x * h x)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f : R<VAR>s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))<VAR>ι : Type u := ↥(PrimeSpectrum.basicOpen f)<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f<VAR>ah_ha : ∀ i ∈ t, ∀ j ∈ t, a i * h j = h i * a j<VAR>s_eq : ∀ i ∈ t, ((structureSheaf R).val.map (iDh i).op) s = const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯<VAR>ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ i ∈ t, ↑(PrimeSpectrum.basicOpen (h i))<VAR>n : ℕ<VAR>b : ι →₀ R<VAR>b_supp : b ∈ Finsupp.supported R R ↑t<VAR>hb : ∑ i ∈ t, b i * h i = f ^ (n + 1)<VAR>tt : Type u := ↑↑t<VAR>i : ι<VAR>hi : i ∈ ↑t<VAR>j : ι<VAR>hj : j ∈ t<GOAL>b j * a j * h i = a i * (b j * h j)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f : R<VAR>s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))<VAR>ι : Type u := ↥(PrimeSpectrum.basicOpen f)<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f<VAR>ah_ha : ∀ i ∈ t, ∀ j ∈ t, a i * h j = h i * a j<VAR>s_eq : ∀ i ∈ t, ((structureSheaf R).val.map (iDh i).op) s = const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯<VAR>ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ i ∈ t, ↑(PrimeSpectrum.basicOpen (h i))<VAR>n : ℕ<VAR>b : ι →₀ R<VAR>b_supp : b ∈ Finsupp.supported R R ↑t<VAR>hb : ∑ i ∈ t, b i * h i = f ^ (n + 1)<VAR>tt : Type u := ↑↑t<VAR>i : ι<VAR>hi : i ∈ ↑t<VAR>j : ι<VAR>hj : j ∈ t<GOAL>b j * (h j * a i) = a i * (b j * h j)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>S : Type u_4<VAR>S₃ : Type u_5<VAR>inst✝³³ : Semiring R<VAR>inst✝³² : Semiring R₂<VAR>inst✝³¹ : Semiring R₃<VAR>inst✝³⁰ : Monoid S<VAR>inst✝²⁹ : Monoid S₃<VAR>M : Type u_6<VAR>inst✝²⁸ : TopologicalSpace M<VAR>inst✝²⁷ : AddCommMonoid M<VAR>inst✝²⁶ : Module R M<VAR>M₂ : Type u_7<VAR>inst✝²⁵ : TopologicalSpace M₂<VAR>inst✝²⁴ : AddCommMonoid M₂<VAR>inst✝²³ : Module R₂ M₂<VAR>M₃ : Type u_8<VAR>inst✝²² : TopologicalSpace M₃<VAR>inst✝²¹ : AddCommMonoid M₃<VAR>inst✝²⁰ : Module R₃ M₃<VAR>N₂ : Type u_9<VAR>inst✝¹⁹ : TopologicalSpace N₂<VAR>inst✝¹⁸ : AddCommMonoid N₂<VAR>inst✝¹⁷ : Module R N₂<VAR>N₃ : Type u_10<VAR>inst✝¹⁶ : TopologicalSpace N₃<VAR>inst✝¹⁵ : AddCommMonoid N₃<VAR>inst✝¹⁴ : Module R N₃<VAR>inst✝¹³ : DistribMulAction S₃ M₃<VAR>inst✝¹² : SMulCommClass R₃ S₃ M₃<VAR>inst✝¹¹ : ContinuousConstSMul S₃ M₃<VAR>inst✝¹⁰ : DistribMulAction S N₃<VAR>inst✝⁹ : SMulCommClass R S N₃<VAR>inst✝⁸ : ContinuousConstSMul S N₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝⁶ : DistribMulAction S₃ M₂<VAR>inst✝⁵ : ContinuousConstSMul S₃ M₂<VAR>inst✝⁴ : SMulCommClass R₂ S₃ M₂<VAR>inst✝³ : DistribMulAction S N₂<VAR>inst✝² : ContinuousConstSMul S N₂<VAR>inst✝¹ : SMulCommClass R S N₂<VAR>inst✝ : LinearMap.CompatibleSMul N₂ N₃ S R<VAR>hₗ : N₂ →L[R] N₃<VAR>c : S<VAR>fₗ : M →L[R] N₂<VAR>x : M<GOAL>(hₗ.comp (c • fₗ)) x = (c • hₗ.comp fₗ) x
<VAR>𝕜 : Type u_1<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p q : ℕ<VAR>hpq : p < q<GOAL>Tendsto (fun x => x ^ p / x ^ q) atTop (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p q : ℕ<VAR>hpq : p < q<GOAL>Tendsto (fun x => x ^ (↑p - ↑q)) atTop (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p q : ℕ<VAR>hpq : p < q<GOAL>↑p - ↑q < 0
<VAR>n : Nat<GOAL>list (n + 1) = 0 :: List.map succ (list n)
<VAR>n : Nat<GOAL>(list (n + 1)).length = (0 :: List.map succ (list n)).length
<VAR>n : Nat<GOAL>∀ (n_1 : Nat) (h₁ : n_1 < (list (n + 1)).length) (h₂ : n_1 < (0 :: List.map succ (list n)).length), (list (n + 1)).get ⟨n_1, h₁⟩ = (0 :: List.map succ (list n)).get ⟨n_1, h₂⟩
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommRing R<VAR>p✝ q p : MvPolynomial σ R<VAR>r : R<GOAL>max p.totalDegree (C r).totalDegree = p.totalDegree