ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m m' : MeasurableSpace α<VAR>h : m ≤ m'<VAR>hsep : HasCountableSeparatingOn α MeasurableSet univ<GOAL>HasCountableSeparatingOn α MeasurableSet univ
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s✝ t : Set E<VAR>L L₁ L₂ : Filter E<VAR>s : Set E<VAR>x₀ : E<VAR>n : ℕ<VAR>h : f =O[𝓝[s] x₀] fun x => ‖x - x₀‖ ^ n<VAR>hx₀ : x₀ ∈ s<VAR>hn : 1 < n<GOAL>HasFDerivWithinAt f 0 s x₀
<VAR>R : Type u<VAR>inst✝³ : Field R<VAR>inst✝² : Fintype R<VAR>R' : Type v<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : IsDomain R'<VAR>χ : MulChar R R'<VAR>hχ : χ ≠ 1<VAR>ψ : AddChar R R'<VAR>hψ : ψ.IsPrimitive<GOAL>gaussSum χ ψ * gaussSum χ⁻¹ ψ⁻¹ = ↑(Fintype.card R)
<VAR>R : Type u<VAR>inst✝³ : Field R<VAR>inst✝² : Fintype R<VAR>R' : Type v<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : IsDomain R'<VAR>χ : MulChar R R'<VAR>hχ : χ ≠ 1<VAR>ψ : AddChar R R'<VAR>hψ : ψ.IsPrimitive<GOAL>∑ x : R, ∑ i : R, χ i * ψ i * (χ x⁻¹ * ψ (-x)) = ↑(Fintype.card R)
<VAR>R : Type u<VAR>inst✝³ : Field R<VAR>inst✝² : Fintype R<VAR>R' : Type v<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : IsDomain R'<VAR>χ : MulChar R R'<VAR>hχ : χ ≠ 1<VAR>ψ : AddChar R R'<VAR>hψ : ψ.IsPrimitive<GOAL>∑ x : R, ∑ y : R, χ (y * x⁻¹) * ψ (y - x) = ↑(Fintype.card R)
<VAR>R : Type u<VAR>inst✝³ : Field R<VAR>inst✝² : Fintype R<VAR>R' : Type v<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : IsDomain R'<VAR>χ : MulChar R R'<VAR>hχ : χ ≠ 1<VAR>ψ : AddChar R R'<VAR>hψ : ψ.IsPrimitive<GOAL>∑ x : R, ∑ c : R, χ c * ψ (x * (c - 1)) = ↑(Fintype.card R)
<VAR>R : Type u<VAR>inst✝³ : Field R<VAR>inst✝² : Fintype R<VAR>R' : Type v<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : IsDomain R'<VAR>χ : MulChar R R'<VAR>hχ : χ ≠ 1<VAR>ψ : AddChar R R'<VAR>hψ : ψ.IsPrimitive<GOAL>∑ y : R, ∑ x : R, χ y * ψ (x * (y - 1)) = ↑(Fintype.card R)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S✝ : Type u_5<VAR>F✝ : Type u_6<VAR>inst✝⁸ : CommMonoid M<VAR>inst✝⁷ : CommMonoid N<VAR>inst✝⁶ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>inst✝⁵ : CommRing R<VAR>ζ : Rˣ<VAR>h : IsPrimitiveRoot ζ k<VAR>inst✝⁴ : IsDomain R<VAR>S : Type u_7<VAR>F : Type u_8<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : MonoidHomClass F R S<VAR>n : ℕ+<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>hζ : (primitiveRoots (↑n) R).Nonempty<VAR>η : ↥(rootsOfUnity n S)<GOAL>f ↑↑((rootsOfUnityEquivOfPrimitiveRoots hf hζ).symm η) = ↑↑η
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S✝ : Type u_5<VAR>F✝ : Type u_6<VAR>inst✝⁸ : CommMonoid M<VAR>inst✝⁷ : CommMonoid N<VAR>inst✝⁶ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>inst✝⁵ : CommRing R<VAR>ζ : Rˣ<VAR>h : IsPrimitiveRoot ζ k<VAR>inst✝⁴ : IsDomain R<VAR>S : Type u_7<VAR>F : Type u_8<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : MonoidHomClass F R S<VAR>n : ℕ+<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>hζ : (primitiveRoots (↑n) R).Nonempty<VAR>ε : ↥(rootsOfUnity n R)<GOAL>f ↑↑((rootsOfUnityEquivOfPrimitiveRoots hf hζ).symm ((rootsOfUnityEquivOfPrimitiveRoots hf hζ) ε)) = ↑↑((rootsOfUnityEquivOfPrimitiveRoots hf hζ) ε)
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>p : ℝ≥0∞<VAR>inst✝ : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<GOAL>(span ℂ (range (fourierLp p))).topologicalClosure = ⊤
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>p : ℝ≥0∞<VAR>inst✝ : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>e_3✝ : Complex.instSemiring = DivisionSemiring.toSemiring<VAR>he✝ : Lp.instModule = Lp.instModule<GOAL>span ℂ (range (fourierLp p)) = Submodule.map (↑(toLp p haarAddCircle ℂ)) (span ℂ (range fourier))
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>p : ℝ≥0∞<VAR>inst✝ : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>e_3✝ : Complex.instSemiring = DivisionSemiring.toSemiring<VAR>he✝ : Lp.instModule = Lp.instModule<GOAL>span ℂ (⇑(toLp p haarAddCircle ℂ) '' range fourier) = span ℂ (⇑↑(toLp p haarAddCircle ℂ) '' range fourier)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁴ : CountablyGenerated γ<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>κ : Kernel α (γ × ℝ)<VAR>inst✝ : IsFiniteKernel κ<VAR>a : α<VAR>s : ℕ → ℚ<VAR>hs_anti : Antitone s<VAR>hs_tendsto : Tendsto s atTop atBot<VAR>s' : ℕ → Set ℝ := fun n => Iic ↑(s n)<GOAL>Tendsto (fun m => ∫ (c : γ), κ.density κ.fst (a, c).1 (a, c).2 (Iic ↑(s m)) ∂κ.fst a) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁴ : CountablyGenerated γ<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>κ : Kernel α (γ × ℝ)<VAR>inst✝ : IsFiniteKernel κ<VAR>a : α<VAR>s : ℕ → ℚ<VAR>hs_anti : Antitone s<VAR>hs_tendsto : Tendsto s atTop atBot<VAR>s' : ℕ → Set ℝ := fun n => Iic ↑(s n)<GOAL>Antitone s'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁴ : CountablyGenerated γ<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>κ : Kernel α (γ × ℝ)<VAR>inst✝ : IsFiniteKernel κ<VAR>a : α<VAR>s : ℕ → ℚ<VAR>hs_anti : Antitone s<VAR>hs_tendsto : Tendsto s atTop atBot<VAR>s' : ℕ → Set ℝ := fun n => Iic ↑(s n)<GOAL>⋂ i, s' i = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁴ : CountablyGenerated γ<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>κ : Kernel α (γ × ℝ)<VAR>inst✝ : IsFiniteKernel κ<VAR>a : α<VAR>s : ℕ → ℚ<VAR>hs_mono : Monotone s<VAR>hs_tendsto : Tendsto s atTop atTop<GOAL>Tendsto (fun m => ∫ (c : γ), κ.density κ.fst (a, c).1 (a, c).2 (Iic ↑(s m)) ∂κ.fst a) atTop (𝓝 ((κ.fst a) univ).toReal)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁴ : CountablyGenerated γ<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>κ : Kernel α (γ × ℝ)<VAR>inst✝ : IsFiniteKernel κ<VAR>a : α<VAR>s : ℕ → ℚ<VAR>hs_mono : Monotone s<VAR>hs_tendsto : Tendsto s atTop atTop<GOAL>Tendsto (fun m => ∫ (c : γ), κ.density κ.fst (a, c).1 (a, c).2 (Iic ↑(s m)) ∂κ.fst a) atTop (𝓝 ((κ a) {p | p.1 ∈ univ}).toReal)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁴ : CountablyGenerated γ<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>κ : Kernel α (γ × ℝ)<VAR>inst✝ : IsFiniteKernel κ<VAR>a : α<VAR>s : ℕ → ℚ<VAR>hs_mono : Monotone s<VAR>hs_tendsto : Tendsto s atTop atTop<VAR>s' : ℕ → Set ℝ := fun n => Iic ↑(s n)<GOAL>Tendsto (fun m => ∫ (c : γ), κ.density κ.fst (a, c).1 (a, c).2 (Iic ↑(s m)) ∂κ.fst a) atTop (𝓝 ((κ a) {p | p.1 ∈ univ}).toReal)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁴ : CountablyGenerated γ<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>κ : Kernel α (γ × ℝ)<VAR>inst✝ : IsFiniteKernel κ<VAR>a : α<VAR>s : ℕ → ℚ<VAR>hs_mono : Monotone s<VAR>hs_tendsto : Tendsto s atTop atTop<VAR>s' : ℕ → Set ℝ := fun n => Iic ↑(s n)<GOAL>Monotone s'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁴ : CountablyGenerated γ<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>κ : Kernel α (γ × ℝ)<VAR>inst✝ : IsFiniteKernel κ<VAR>a : α<VAR>s : ℕ → ℚ<VAR>hs_mono : Monotone s<VAR>hs_tendsto : Tendsto s atTop atTop<VAR>s' : ℕ → Set ℝ := fun n => Iic ↑(s n)<GOAL>⋃ i, s' i = univ
<VAR>a b d m n : ℤ<VAR>hb : b ≠ 0<VAR>k : ℤ<VAR>h : b * a = b * k * d<GOAL>a = b * k / b * d
<VAR>a b d m n : ℤ<VAR>hb : b ≠ 0<VAR>k : ℤ<VAR>h : b * a = b * k * d<GOAL>a = k * d
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α✝<VAR>inst✝⁸ : TopologicalSpace α✝<VAR>inst✝⁷ : MeasurableSpace α✝<VAR>inst✝⁶ : BorelSpace α✝<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : BorelSpace β<VAR>inst✝² : MeasurableSpace δ<VAR>α : Type u_5<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : ConditionallyCompleteLattice α<VAR>p : Prop<VAR>f : δ → α<VAR>hf : Measurable f<GOAL>Measurable fun b => ⨅ (_ : p), f b
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α✝<VAR>inst✝⁸ : TopologicalSpace α✝<VAR>inst✝⁷ : MeasurableSpace α✝<VAR>inst✝⁶ : BorelSpace α✝<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : BorelSpace β<VAR>inst✝² : MeasurableSpace δ<VAR>α : Type u_5<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : ConditionallyCompleteLattice α<VAR>p : Prop<VAR>f : δ → α<VAR>hf : Measurable f<GOAL>Measurable fun b => if h : p then f b else sInf ∅
<VAR>a✝ b✝ c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>a : ℕ<VAR>ha : 2 ≤ a<VAR>b : ℕ<VAR>x✝ : 2 ≤ b + 3<GOAL>a + (b + 3) ≤ a * (b + 3)
<VAR>a✝ b✝ c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>a : ℕ<VAR>ha : 2 ≤ a<VAR>b : ℕ<VAR>x✝ : 2 ≤ b + 3<VAR>this : a + (b + 2) ≤ a * (b + 2)<GOAL>a + (b + 3) ≤ a * (b + 3)
<VAR>a✝ b✝ c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>a : ℕ<VAR>ha : 2 ≤ a<VAR>b : ℕ<VAR>x✝ : 2 ≤ b + 3<VAR>this : a + (b + 2) ≤ a * (b + 2)<GOAL>a + (b + 3) ≤ a * (b + 2) + a
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>F : ι → β → α<VAR>S : Set β<GOAL>UniformEquicontinuousOn F S ↔ UniformContinuousOn (⇑UniformFun.ofFun ∘ swap F) S
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>F : ι → β → α<VAR>S : Set β<GOAL>UniformEquicontinuousOn F S ↔ ∀ i ∈ 𝓤 α, ∀ᶠ (x : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S), ((⇑UniformFun.ofFun ∘ swap F) x.1, (⇑UniformFun.ofFun ∘ swap F) x.2) ∈ UniformFun.gen ι α i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝¹ : Lattice α<VAR>inst✝ : OrderBot α<VAR>s t : Finset ι<VAR>f : ι → α<VAR>i : ι<VAR>hs : s.SupIndep f<VAR>hts : t ⊆ s<VAR>hi : i ∈ s<VAR>hf : ∀ (i : ι), f i ≠ ⊥<GOAL>f i ≤ t.sup f ↔ i ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝¹ : Lattice α<VAR>inst✝ : OrderBot α<VAR>s t : Finset ι<VAR>f : ι → α<VAR>i : ι<VAR>hs : s.SupIndep f<VAR>hts : t ⊆ s<VAR>hi : i ∈ s<VAR>hf : ∀ (i : ι), f i ≠ ⊥<VAR>h : f i ≤ t.sup f<GOAL>i ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝¹ : Lattice α<VAR>inst✝ : OrderBot α<VAR>s t : Finset ι<VAR>f : ι → α<VAR>i : ι<VAR>hs : s.SupIndep f<VAR>hts : t ⊆ s<VAR>hi : i ∈ s<VAR>hf : ∀ (i : ι), f i ≠ ⊥<VAR>h : f i ≤ t.sup f<VAR>hit : i ∉ t<GOAL>False
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>i j k : 𝒰.J<GOAL>t' 𝒰 f g i j k ≫ pullback.fst (fV 𝒰 f g j k) (fV 𝒰 f g j i) ≫ pullback.snd (pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map k) = pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a✝ : α<VAR>f✝ g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>f : α → β<VAR>a : α<VAR>h : a ∈ filter p s<GOAL>f a = if p a then f a else 1
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a✝ : α<VAR>f✝ g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>f : α → β<VAR>a : α<VAR>h : a ∈ filter p s<GOAL>p a
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>f : α → β<GOAL>(∏ a ∈ filter p s, if p a then f a else 1) = ∏ a ∈ s, if p a then f a else 1
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>f : α → β<VAR>x : α<VAR>hs : x ∈ s<VAR>h : x ∉ filter p s<GOAL>(if p x then f x else 1) = 1
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>f : α → β<VAR>x : α<VAR>hs : x ∈ s<VAR>h : x ∈ s → ¬p x<GOAL>(if p x then f x else 1) = 1
<VAR>K : Type u_1<VAR>S : Type u_2<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : Algebra K S<VAR>R : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Algebra R K<VAR>inst✝⁵ : IsScalarTower R K S<VAR>A : Type u_4<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : IsScalarTower R S A<VAR>B : PowerBasis S A<VAR>hB : IsIntegral R B.gen<VAR>inst✝ : IsDomain S<VAR>x : A<VAR>hx : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)<VAR>hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)<VAR>n : ℕ<GOAL>∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr (x ^ n)) i)
<VAR>K : Type u_1<VAR>S : Type u_2<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : Algebra K S<VAR>R : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Algebra R K<VAR>inst✝⁵ : IsScalarTower R K S<VAR>A : Type u_4<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : IsScalarTower R S A<VAR>B : PowerBasis S A<VAR>hB : IsIntegral R B.gen<VAR>inst✝ : IsDomain S<VAR>x : A<VAR>hx : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)<VAR>hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)<VAR>n : ℕ<VAR>a✝ : Nontrivial A<GOAL>∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr (x ^ n)) i)
<VAR>K : Type u_1<VAR>S : Type u_2<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : Algebra K S<VAR>R : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Algebra R K<VAR>inst✝⁵ : IsScalarTower R K S<VAR>A : Type u_4<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : IsScalarTower R S A<VAR>B : PowerBasis S A<VAR>hB : IsIntegral R B.gen<VAR>inst✝ : IsDomain S<VAR>x : A<VAR>hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)<VAR>n : ℕ<VAR>a✝ : Nontrivial A<GOAL>(∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)) → ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr (x ^ n)) i)
<VAR>K : Type u_1<VAR>S : Type u_2<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : Algebra K S<VAR>R : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Algebra R K<VAR>inst✝⁵ : IsScalarTower R K S<VAR>A : Type u_4<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : IsScalarTower R S A<VAR>B : PowerBasis S A<VAR>hB : IsIntegral R B.gen<VAR>inst✝ : IsDomain S<VAR>x : A<VAR>hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)<VAR>n : ℕ<VAR>a✝ : Nontrivial A<GOAL>(fun n => (∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)) → ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr (x ^ n)) i)) 0
<VAR>K : Type u_1<VAR>S : Type u_2<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : Algebra K S<VAR>R : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Algebra R K<VAR>inst✝⁵ : IsScalarTower R K S<VAR>A : Type u_4<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : IsScalarTower R S A<VAR>B : PowerBasis S A<VAR>hB : IsIntegral R B.gen<VAR>inst✝ : IsDomain S<VAR>x : A<VAR>hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)<VAR>n✝ : ℕ<VAR>a✝ : Nontrivial A<VAR>n : ℕ<VAR>hn : ∀ m ≤ n, (fun n => (∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)) → ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr (x ^ n)) i)) m<GOAL>(fun n => (∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)) → ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr (x ^ n)) i)) n.succ
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s : Set α<VAR>inst✝ : Fintype ↑s<VAR>h : s.Finite<GOAL>h.toFinset = s.toFinset
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s : Set α<VAR>inst✝ : Fintype ↑s<VAR>h : s.Finite<VAR>this : h.fintype = inst✝<GOAL>h.toFinset = s.toFinset
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : ConcreteCategory C<VAR>inst✝² : HasLimits C<VAR>inst✝¹ : ConcreteCategory.forget.ReflectsIsomorphisms<VAR>inst✝ : PreservesLimits ConcreteCategory.forget<VAR>X : TopCat<VAR>F : Sheaf C X<VAR>ι : Type v<VAR>U : ι → Opens ↑X<VAR>V : Opens ↑X<VAR>iUV : (i : ι) → U i ⟶ V<VAR>hcover : V ≤ iSup U<VAR>sf : (i : ι) → (CategoryTheory.forget C).obj (F.val.obj (op (U i)))<VAR>h : IsCompatible F.val U sf<GOAL>∃! s, ∀ (i : ι), (F.val.map (iUV i).op) s = sf i
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : ConcreteCategory C<VAR>inst✝² : HasLimits C<VAR>inst✝¹ : ConcreteCategory.forget.ReflectsIsomorphisms<VAR>inst✝ : PreservesLimits ConcreteCategory.forget<VAR>X : TopCat<VAR>F : Sheaf C X<VAR>ι : Type v<VAR>U : ι → Opens ↑X<VAR>V : Opens ↑X<VAR>iUV : (i : ι) → U i ⟶ V<VAR>hcover : V ≤ iSup U<VAR>sf : (i : ι) → (CategoryTheory.forget C).obj (F.val.obj (op (U i)))<VAR>h : IsCompatible F.val U sf<VAR>V_eq_supr_U : V = iSup U<GOAL>∃! s, ∀ (i : ι), (F.val.map (iUV i).op) s = sf i
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : ConcreteCategory C<VAR>inst✝² : HasLimits C<VAR>inst✝¹ : ConcreteCategory.forget.ReflectsIsomorphisms<VAR>inst✝ : PreservesLimits ConcreteCategory.forget<VAR>X : TopCat<VAR>F : Sheaf C X<VAR>ι : Type v<VAR>U : ι → Opens ↑X<VAR>V : Opens ↑X<VAR>iUV : (i : ι) → U i ⟶ V<VAR>hcover : V ≤ iSup U<VAR>sf : (i : ι) → (CategoryTheory.forget C).obj (F.val.obj (op (U i)))<VAR>h : IsCompatible F.val U sf<VAR>V_eq_supr_U : V = iSup U<VAR>gl : (CategoryTheory.forget C).obj (F.val.obj (op (iSup U)))<VAR>gl_spec : IsGluing F.val U sf gl<VAR>gl_uniq : ∀ (y : (CategoryTheory.forget C).obj (F.val.obj (op (iSup U)))), (fun s => IsGluing F.val U sf s) y → y = gl<GOAL>∃! s, ∀ (i : ι), (F.val.map (iUV i).op) s = sf i
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type v'<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup N<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R N<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Module S N<VAR>inst✝² : IsScalarTower R S N<VAR>p : Submonoid R<VAR>inst✝¹ : IsLocalization p S<VAR>f : M →ₗ[R] N<VAR>inst✝ : IsLocalizedModule p f<VAR>hp : p ≤ R⁰<VAR>ι : Type u_1<VAR>v : ι → N<VAR>hf : LinearIndependent S v<GOAL>∃ w, LinearIndependent R w
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type v'<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup N<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R N<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Module S N<VAR>inst✝² : IsScalarTower R S N<VAR>p : Submonoid R<VAR>inst✝¹ : IsLocalization p S<VAR>f : M →ₗ[R] N<VAR>inst✝ : IsLocalizedModule p f<VAR>hp : p ≤ R⁰<VAR>ι : Type u_1<VAR>v : ι → N<VAR>hf : LinearIndependent S v<VAR>sec : N → M × ↥p<VAR>hsec : ∀ (y : N), (sec y).2 • y = f (sec y).1<GOAL>∃ w, LinearIndependent R w
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type v'<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup N<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R N<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Module S N<VAR>inst✝² : IsScalarTower R S N<VAR>p : Submonoid R<VAR>inst✝¹ : IsLocalization p S<VAR>f : M →ₗ[R] N<VAR>inst✝ : IsLocalizedModule p f<VAR>hp : p ≤ R⁰<VAR>ι : Type u_1<VAR>v : ι → N<VAR>hf : LinearIndependent S v<VAR>sec : N → M × ↥p<VAR>hsec : ∀ (y : N), (sec y).2 • y = f (sec y).1<GOAL>LinearIndependent R fun i => (sec (v i)).1
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type v'<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup N<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R N<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Module S N<VAR>inst✝² : IsScalarTower R S N<VAR>p : Submonoid R<VAR>inst✝¹ : IsLocalization p S<VAR>f : M →ₗ[R] N<VAR>inst✝ : IsLocalizedModule p f<VAR>hp : p ≤ R⁰<VAR>ι : Type u_1<VAR>v : ι → N<VAR>hf : ∀ (s : Finset ι) (g : ι → S), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0<VAR>sec : N → M × ↥p<VAR>hsec : ∀ (y : N), (sec y).2 • y = f (sec y).1<GOAL>∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • (sec (v i)).1 = 0 → ∀ i ∈ s, g i = 0
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type v'<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup N<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R N<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Module S N<VAR>inst✝² : IsScalarTower R S N<VAR>p : Submonoid R<VAR>inst✝¹ : IsLocalization p S<VAR>f : M →ₗ[R] N<VAR>inst✝ : IsLocalizedModule p f<VAR>hp : p ≤ R⁰<VAR>ι : Type u_1<VAR>v : ι → N<VAR>hf : ∀ (s : Finset ι) (g : ι → S), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0<VAR>sec : N → M × ↥p<VAR>hsec : ∀ (y : N), (sec y).2 • y = f (sec y).1<VAR>t : Finset ι<VAR>g : ι → R<VAR>hg : ∑ i ∈ t, g i • (sec (v i)).1 = 0<VAR>i : ι<VAR>hit : i ∈ t<GOAL>g i = 0
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type v'<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup N<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R N<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Module S N<VAR>inst✝² : IsScalarTower R S N<VAR>p : Submonoid R<VAR>inst✝¹ : IsLocalization p S<VAR>f : M →ₗ[R] N<VAR>inst✝ : IsLocalizedModule p f<VAR>hp : p ≤ R⁰<VAR>ι : Type u_1<VAR>v : ι → N<VAR>hf : ∀ (s : Finset ι) (g : ι → S), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0<VAR>sec : N → M × ↥p<VAR>hsec : ∀ (y : N), (sec y).2 • y = f (sec y).1<VAR>t : Finset ι<VAR>g : ι → R<VAR>hg : ∑ i ∈ t, g i • (sec (v i)).1 = 0<VAR>i : ι<VAR>hit : i ∈ t<GOAL>g i * ↑(sec (v i)).2 = 0
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type v'<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup N<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R N<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Module S N<VAR>inst✝² : IsScalarTower R S N<VAR>p : Submonoid R<VAR>inst✝¹ : IsLocalization p S<VAR>f : M →ₗ[R] N<VAR>inst✝ : IsLocalizedModule p f<VAR>hp : p ≤ R⁰<VAR>ι : Type u_1<VAR>v : ι → N<VAR>hf : ∀ (s : Finset ι) (g : ι → S), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0<VAR>sec : N → M × ↥p<VAR>hsec : ∀ (y : N), (sec y).2 • y = f (sec y).1<VAR>t : Finset ι<VAR>g : ι → R<VAR>hg : ∑ i ∈ t, g i • (sec (v i)).1 = 0<VAR>i : ι<VAR>hit : i ∈ t<GOAL>(algebraMap R S) (g i * ↑(sec (v i)).2) = (algebraMap R S) 0