ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : TopologicalSpace X<VAR>a✝ b✝ b₀✝ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f : ℝ → E<VAR>inst✝ : FirstCountableTopology X<VAR>F : X → ℝ → E<VAR>bound : ℝ → ℝ<VAR>a b a₀ b₀ : ℝ<VAR>x₀ : X<VAR>hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t<VAR>bound_integrable : IntervalIntegrable bound μ a b<VAR>h_cont : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ContinuousAt (fun x => F x t) x₀<VAR>ha₀ : a₀ ∈ Ioo a b<VAR>hb₀ : b₀ ∈ Ioo a b<VAR>hμb₀ : μ {b₀} = 0<VAR>hsub : ∀ {a₀ b₀ : ℝ}, a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → Ι a₀ b₀ ⊆ Ι a b<VAR>Ioo_nhds : Ioo a b ∈ 𝓝 b₀<VAR>Icc_nhds : Icc a b ∈ 𝓝 b₀<VAR>hx₀ : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x₀ t‖ ≤ bound t<VAR>this : ∀ᶠ (p : X × ℝ) in 𝓝 (x₀, b₀), ∫ (s : ℝ) in a₀..p.2, F p.1 s ∂μ = ∫ (s : ℝ) in a₀..b₀, F p.1 s ∂μ + ∫ (s : ℝ) in b₀..p.2, F x₀ s ∂μ + ∫ (s : ℝ) in b₀..p.2, F p.1 s - F x₀ s ∂μ<GOAL>ContinuousAt (fun p => ∫ (t : ℝ) in a₀..p.2, F p.1 t ∂μ) (x₀, b₀)
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : TopologicalSpace X<VAR>a✝ b✝ b₀✝ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f : ℝ → E<VAR>inst✝ : FirstCountableTopology X<VAR>F : X → ℝ → E<VAR>bound : ℝ → ℝ<VAR>a b a₀ b₀ : ℝ<VAR>x₀ : X<VAR>hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t<VAR>bound_integrable : IntervalIntegrable bound μ a b<VAR>h_cont : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ContinuousAt (fun x => F x t) x₀<VAR>ha₀ : a₀ ∈ Ioo a b<VAR>hb₀ : b₀ ∈ Ioo a b<VAR>hμb₀ : μ {b₀} = 0<VAR>hsub : ∀ {a₀ b₀ : ℝ}, a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → Ι a₀ b₀ ⊆ Ι a b<VAR>Ioo_nhds : Ioo a b ∈ 𝓝 b₀<VAR>Icc_nhds : Icc a b ∈ 𝓝 b₀<VAR>hx₀ : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x₀ t‖ ≤ bound t<VAR>this : ∀ᶠ (p : X × ℝ) in 𝓝 (x₀, b₀), ∫ (s : ℝ) in a₀..p.2, F p.1 s ∂μ = ∫ (s : ℝ) in a₀..b₀, F p.1 s ∂μ + ∫ (s : ℝ) in b₀..p.2, F x₀ s ∂μ + ∫ (s : ℝ) in b₀..p.2, F p.1 s - F x₀ s ∂μ<GOAL>ContinuousAt (fun x => ∫ (s : ℝ) in a₀..b₀, F x.1 s ∂μ + ∫ (s : ℝ) in b₀..x.2, F x₀ s ∂μ + ∫ (s : ℝ) in b₀..x.2, F x.1 s - F x₀ s ∂μ) (x₀, b₀)
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : TopologicalSpace X<VAR>a✝ b✝ b₀✝ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f : ℝ → E<VAR>inst✝ : FirstCountableTopology X<VAR>F : X → ℝ → E<VAR>bound : ℝ → ℝ<VAR>a b a₀ b₀ : ℝ<VAR>x₀ : X<VAR>hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t<VAR>bound_integrable : IntervalIntegrable bound μ a b<VAR>h_cont : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ContinuousAt (fun x => F x t) x₀<VAR>ha₀ : a₀ ∈ Ioo a b<VAR>hb₀ : b₀ ∈ Ioo a b<VAR>hμb₀ : μ {b₀} = 0<VAR>hsub : ∀ {a₀ b₀ : ℝ}, a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → Ι a₀ b₀ ⊆ Ι a b<VAR>Ioo_nhds : Ioo a b ∈ 𝓝 b₀<VAR>Icc_nhds : Icc a b ∈ 𝓝 b₀<VAR>hx₀ : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x₀ t‖ ≤ bound t<GOAL>ContinuousAt (fun x => ∫ (s : ℝ) in a₀..b₀, F x.1 s ∂μ + ∫ (s : ℝ) in b₀..x.2, F x₀ s ∂μ + ∫ (s : ℝ) in b₀..x.2, F x.1 s - F x₀ s ∂μ) (x₀, b₀)
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : TopologicalSpace X<VAR>a✝ b✝ b₀✝ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f : ℝ → E<VAR>inst✝ : FirstCountableTopology X<VAR>F : X → ℝ → E<VAR>bound : ℝ → ℝ<VAR>a b a₀ b₀ : ℝ<VAR>x₀ : X<VAR>hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t<VAR>bound_integrable : IntervalIntegrable bound μ a b<VAR>h_cont : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ContinuousAt (fun x => F x t) x₀<VAR>ha₀ : a₀ ∈ Ioo a b<VAR>hb₀ : b₀ ∈ Ioo a b<VAR>hμb₀ : μ {b₀} = 0<VAR>hsub : ∀ {a₀ b₀ : ℝ}, a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → Ι a₀ b₀ ⊆ Ι a b<VAR>Ioo_nhds : Ioo a b ∈ 𝓝 b₀<VAR>Icc_nhds : Icc a b ∈ 𝓝 b₀<VAR>hx₀ : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x₀ t‖ ≤ bound t<GOAL>ContinuousAt (fun x => ∫ (s : ℝ) in a₀..b₀, F x.1 s ∂μ) (x₀, b₀)
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : TopologicalSpace X<VAR>a✝ b✝ b₀✝ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f : ℝ → E<VAR>inst✝ : FirstCountableTopology X<VAR>F : X → ℝ → E<VAR>bound : ℝ → ℝ<VAR>a b a₀ b₀ : ℝ<VAR>x₀ : X<VAR>hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t<VAR>bound_integrable : IntervalIntegrable bound μ a b<VAR>h_cont : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ContinuousAt (fun x => F x t) x₀<VAR>ha₀ : a₀ ∈ Ioo a b<VAR>hb₀ : b₀ ∈ Ioo a b<VAR>hμb₀ : μ {b₀} = 0<VAR>hsub : ∀ {a₀ b₀ : ℝ}, a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → Ι a₀ b₀ ⊆ Ι a b<VAR>Ioo_nhds : Ioo a b ∈ 𝓝 b₀<VAR>Icc_nhds : Icc a b ∈ 𝓝 b₀<VAR>hx₀ : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x₀ t‖ ≤ bound t<GOAL>ContinuousAt (fun x => ∫ (s : ℝ) in b₀..x.2, F x₀ s ∂μ) (x₀, b₀)
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : TopologicalSpace X<VAR>a✝ b✝ b₀✝ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f : ℝ → E<VAR>inst✝ : FirstCountableTopology X<VAR>F : X → ℝ → E<VAR>bound : ℝ → ℝ<VAR>a b a₀ b₀ : ℝ<VAR>x₀ : X<VAR>hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t<VAR>bound_integrable : IntervalIntegrable bound μ a b<VAR>h_cont : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ContinuousAt (fun x => F x t) x₀<VAR>ha₀ : a₀ ∈ Ioo a b<VAR>hb₀ : b₀ ∈ Ioo a b<VAR>hμb₀ : μ {b₀} = 0<VAR>hsub : ∀ {a₀ b₀ : ℝ}, a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → Ι a₀ b₀ ⊆ Ι a b<VAR>Ioo_nhds : Ioo a b ∈ 𝓝 b₀<VAR>Icc_nhds : Icc a b ∈ 𝓝 b₀<VAR>hx₀ : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x₀ t‖ ≤ bound t<GOAL>ContinuousAt (fun x => ∫ (s : ℝ) in b₀..x.2, F x.1 s - F x₀ s ∂μ) (x₀, b₀)
<VAR>m : Type u_1 → Type u_2<VAR>α β : Type u_1<VAR>p : α → Prop<VAR>x✝ : m α<VAR>q : β → Prop<VAR>inst✝¹ : Monad m<VAR>inst✝ : LawfulMonad m<VAR>f : α → m β<VAR>hx : SatisfiesM p x✝<VAR>hf : ∀ (a : α), p a → SatisfiesM q (f a)<VAR>x : m { a // p a }<VAR>g : (a : α) → p a → { x // Subtype.val <$> x = f a }<GOAL>(Subtype.val <$> do let x ← x match x with | ⟨a, h⟩ => (g a h).val) = Subtype.val <$> x >>= f
<VAR>m : Type u_1 → Type u_2<VAR>α β : Type u_1<VAR>p : α → Prop<VAR>x✝ : m α<VAR>q : β → Prop<VAR>inst✝¹ : Monad m<VAR>inst✝ : LawfulMonad m<VAR>f : α → m β<VAR>hx : SatisfiesM p x✝<VAR>hf : ∀ (a : α), p a → SatisfiesM q (f a)<VAR>x : m { a // p a }<VAR>g : (a : α) → p a → { x // Subtype.val <$> x = f a }<GOAL>(do let x ← x let a ← (g x.val ⋯).val pure a.val) = do let x ← x f x.val
<VAR>m : Type u_1 → Type u_2<VAR>α β : Type u_1<VAR>p : α → Prop<VAR>x✝ : m α<VAR>q : β → Prop<VAR>inst✝¹ : Monad m<VAR>inst✝ : LawfulMonad m<VAR>f : α → m β<VAR>hx : SatisfiesM p x✝<VAR>hf : ∀ (a : α), p a → SatisfiesM q (f a)<VAR>x : m { a // p a }<VAR>g : (a : α) → p a → { x // Subtype.val <$> x = f a }<GOAL>(fun x => do let a ← (g x.val ⋯).val pure a.val) = fun x => f x.val
<VAR>m : Type u_1 → Type u_2<VAR>α β : Type u_1<VAR>p : α → Prop<VAR>x✝ : m α<VAR>q : β → Prop<VAR>inst✝¹ : Monad m<VAR>inst✝ : LawfulMonad m<VAR>f : α → m β<VAR>hx : SatisfiesM p x✝<VAR>hf : ∀ (a : α), p a → SatisfiesM q (f a)<VAR>x : m { a // p a }<VAR>g : (a : α) → p a → { x // Subtype.val <$> x = f a }<VAR>a : α<VAR>h : p a<GOAL>(do let a ← (g ⟨a, h⟩.val ⋯).val pure a.val) = f ⟨a, h⟩.val
<VAR>α : Type u_1<VAR>Γ₀ : Type u_2<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>γ γ₁ γ₂ : Γ₀<VAR>l : Filter α<VAR>f : α → Γ₀<GOAL>(𝓝 0).HasBasis (fun γ => γ ≠ 0) Iio
<VAR>α : Type u_1<VAR>Γ₀ : Type u_2<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>γ γ₁ γ₂ : Γ₀<VAR>l : Filter α<VAR>f : α → Γ₀<GOAL>(⨅ γ, ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ)).HasBasis (fun γ => γ ≠ 0) Iio
<VAR>α : Type u_1<VAR>Γ₀ : Type u_2<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>γ γ₁ γ₂ : Γ₀<VAR>l : Filter α<VAR>f : α → Γ₀<GOAL>DirectedOn (Iio ⁻¹'o fun x x_1 => x ≥ x_1) fun γ => γ = 0 → False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝³ : OrderedSemiring 𝕜<VAR>inst✝² : OrderedAddCommMonoid E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : OrderedSMul 𝕜 E<VAR>s : Set E<VAR>hs : s.OrdConnected<VAR>h : IsChain (fun x x_1 => x ≤ x_1) s<GOAL>Convex 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝³ : OrderedSemiring 𝕜<VAR>inst✝² : OrderedAddCommMonoid E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : OrderedSMul 𝕜 E<VAR>s : Set E<VAR>hs : s.OrdConnected<VAR>h : IsChain (fun x x_1 => x ≤ x_1) s<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<GOAL>[x-[𝕜]y] ⊆ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝³ : OrderedSemiring 𝕜<VAR>inst✝² : OrderedAddCommMonoid E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : OrderedSMul 𝕜 E<VAR>s : Set E<VAR>hs : s.OrdConnected<VAR>h : IsChain (fun x x_1 => x ≤ x_1) s<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>hxy : x ≤ y<GOAL>[x-[𝕜]y] ⊆ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝³ : OrderedSemiring 𝕜<VAR>inst✝² : OrderedAddCommMonoid E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : OrderedSMul 𝕜 E<VAR>s : Set E<VAR>hs : s.OrdConnected<VAR>h : IsChain (fun x x_1 => x ≤ x_1) s<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>hyx : y ≤ x<GOAL>[x-[𝕜]y] ⊆ s
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A B✝ : Matrix n n α<VAR>B : Matrix n m α<VAR>h : IsUnit A.det<GOAL>A⁻¹ * (A * B) = B
<VAR>η : Type u_1<VAR>α : Type u_2<VAR>ι : Type u_3<VAR>κ : Type u_4<VAR>l : Line α ι<VAR>i : ι<VAR>a x : α<VAR>h : l.idxFun i = some a<GOAL>(fun x i => (l.idxFun i).getD x) x i = a
<VAR>R : Type u<VAR>inst✝¹⁰ : CommRing R<VAR>S : Submonoid R<VAR>M : Type w<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>t : Finset R<VAR>ht : Ideal.span ↑t = ⊤<VAR>Mₚ : { x // x ∈ t } → Type u_1<VAR>inst✝⁷ : (g : { x // x ∈ t }) → AddCommMonoid (Mₚ g)<VAR>inst✝⁶ : (g : { x // x ∈ t }) → Module R (Mₚ g)<VAR>Rₚ : { x // x ∈ t } → Type u<VAR>inst✝⁵ : (g : { x // x ∈ t }) → CommRing (Rₚ g)<VAR>inst✝⁴ : (g : { x // x ∈ t }) → Algebra R (Rₚ g)<VAR>inst✝³ : ∀ (g : { x // x ∈ t }), IsLocalization.Away (↑g) (Rₚ g)<VAR>inst✝² : (g : { x // x ∈ t }) → Module (Rₚ g) (Mₚ g)<VAR>inst✝¹ : ∀ (g : { x // x ∈ t }), IsScalarTower R (Rₚ g) (Mₚ g)<VAR>f : (g : { x // x ∈ t }) → M →ₗ[R] Mₚ g<VAR>inst✝ : ∀ (g : { x // x ∈ t }), IsLocalizedModule (Submonoid.powers ↑g) (f g)<VAR>H : ∀ (g : { x // x ∈ t }), Finite (Rₚ g) (Mₚ g)<GOAL>⊤.FG
<VAR>R : Type u<VAR>inst✝¹⁰ : CommRing R<VAR>S : Submonoid R<VAR>M : Type w<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>t : Finset R<VAR>ht : Ideal.span ↑t = ⊤<VAR>Mₚ : { x // x ∈ t } → Type u_1<VAR>inst✝⁷ : (g : { x // x ∈ t }) → AddCommMonoid (Mₚ g)<VAR>inst✝⁶ : (g : { x // x ∈ t }) → Module R (Mₚ g)<VAR>Rₚ : { x // x ∈ t } → Type u<VAR>inst✝⁵ : (g : { x // x ∈ t }) → CommRing (Rₚ g)<VAR>inst✝⁴ : (g : { x // x ∈ t }) → Algebra R (Rₚ g)<VAR>inst✝³ : ∀ (g : { x // x ∈ t }), IsLocalization.Away (↑g) (Rₚ g)<VAR>inst✝² : (g : { x // x ∈ t }) → Module (Rₚ g) (Mₚ g)<VAR>inst✝¹ : ∀ (g : { x // x ∈ t }), IsScalarTower R (Rₚ g) (Mₚ g)<VAR>f : (g : { x // x ∈ t }) → M →ₗ[R] Mₚ g<VAR>inst✝ : ∀ (g : { x // x ∈ t }), IsLocalizedModule (Submonoid.powers ↑g) (f g)<VAR>H : ∀ (g : { x // x ∈ t }), Finite (Rₚ g) (Mₚ g)<VAR>s₁ : (g : { x // x ∈ t }) → Finset (Mₚ g)<VAR>s₂ : ∀ (g : { x // x ∈ t }), Submodule.span (Rₚ g) ↑(s₁ g) = ⊤<GOAL>⊤.FG
<VAR>R : Type u<VAR>inst✝¹⁰ : CommRing R<VAR>S : Submonoid R<VAR>M : Type w<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>t : Finset R<VAR>ht : Ideal.span ↑t = ⊤<VAR>Mₚ : { x // x ∈ t } → Type u_1<VAR>inst✝⁷ : (g : { x // x ∈ t }) → AddCommMonoid (Mₚ g)<VAR>inst✝⁶ : (g : { x // x ∈ t }) → Module R (Mₚ g)<VAR>Rₚ : { x // x ∈ t } → Type u<VAR>inst✝⁵ : (g : { x // x ∈ t }) → CommRing (Rₚ g)<VAR>inst✝⁴ : (g : { x // x ∈ t }) → Algebra R (Rₚ g)<VAR>inst✝³ : ∀ (g : { x // x ∈ t }), IsLocalization.Away (↑g) (Rₚ g)<VAR>inst✝² : (g : { x // x ∈ t }) → Module (Rₚ g) (Mₚ g)<VAR>inst✝¹ : ∀ (g : { x // x ∈ t }), IsScalarTower R (Rₚ g) (Mₚ g)<VAR>f : (g : { x // x ∈ t }) → M →ₗ[R] Mₚ g<VAR>inst✝ : ∀ (g : { x // x ∈ t }), IsLocalizedModule (Submonoid.powers ↑g) (f g)<VAR>H : ∀ (g : { x // x ∈ t }), Finite (Rₚ g) (Mₚ g)<VAR>s₁ : (g : { x // x ∈ t }) → Finset (Mₚ g)<VAR>s₂ : ∀ (g : { x // x ∈ t }), Submodule.span (Rₚ g) ↑(s₁ g) = ⊤<VAR>sf : { x // x ∈ t } → Finset M := fun x => IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers ↑x) (f x) (s₁ x)<GOAL>⊤.FG
<VAR>R : Type u<VAR>inst✝¹⁰ : CommRing R<VAR>S : Submonoid R<VAR>M : Type w<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>t : Finset R<VAR>ht : Ideal.span ↑t = ⊤<VAR>Mₚ : { x // x ∈ t } → Type u_1<VAR>inst✝⁷ : (g : { x // x ∈ t }) → AddCommMonoid (Mₚ g)<VAR>inst✝⁶ : (g : { x // x ∈ t }) → Module R (Mₚ g)<VAR>Rₚ : { x // x ∈ t } → Type u<VAR>inst✝⁵ : (g : { x // x ∈ t }) → CommRing (Rₚ g)<VAR>inst✝⁴ : (g : { x // x ∈ t }) → Algebra R (Rₚ g)<VAR>inst✝³ : ∀ (g : { x // x ∈ t }), IsLocalization.Away (↑g) (Rₚ g)<VAR>inst✝² : (g : { x // x ∈ t }) → Module (Rₚ g) (Mₚ g)<VAR>inst✝¹ : ∀ (g : { x // x ∈ t }), IsScalarTower R (Rₚ g) (Mₚ g)<VAR>f : (g : { x // x ∈ t }) → M →ₗ[R] Mₚ g<VAR>inst✝ : ∀ (g : { x // x ∈ t }), IsLocalizedModule (Submonoid.powers ↑g) (f g)<VAR>H : ∀ (g : { x // x ∈ t }), Finite (Rₚ g) (Mₚ g)<VAR>s₁ : (g : { x // x ∈ t }) → Finset (Mₚ g)<VAR>s₂ : ∀ (g : { x // x ∈ t }), Submodule.span (Rₚ g) ↑(s₁ g) = ⊤<VAR>sf : { x // x ∈ t } → Finset M := fun x => IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers ↑x) (f x) (s₁ x)<GOAL>Submodule.span R ↑(t.attach.biUnion sf) = ⊤
<VAR>R : Type u<VAR>inst✝¹⁰ : CommRing R<VAR>S : Submonoid R<VAR>M : Type w<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>t : Finset R<VAR>ht : Ideal.span ↑t = ⊤<VAR>Mₚ : { x // x ∈ t } → Type u_1<VAR>inst✝⁷ : (g : { x // x ∈ t }) → AddCommMonoid (Mₚ g)<VAR>inst✝⁶ : (g : { x // x ∈ t }) → Module R (Mₚ g)<VAR>Rₚ : { x // x ∈ t } → Type u<VAR>inst✝⁵ : (g : { x // x ∈ t }) → CommRing (Rₚ g)<VAR>inst✝⁴ : (g : { x // x ∈ t }) → Algebra R (Rₚ g)<VAR>inst✝³ : ∀ (g : { x // x ∈ t }), IsLocalization.Away (↑g) (Rₚ g)<VAR>inst✝² : (g : { x // x ∈ t }) → Module (Rₚ g) (Mₚ g)<VAR>inst✝¹ : ∀ (g : { x // x ∈ t }), IsScalarTower R (Rₚ g) (Mₚ g)<VAR>f : (g : { x // x ∈ t }) → M →ₗ[R] Mₚ g<VAR>inst✝ : ∀ (g : { x // x ∈ t }), IsLocalizedModule (Submonoid.powers ↑g) (f g)<VAR>H : ∀ (g : { x // x ∈ t }), Finite (Rₚ g) (Mₚ g)<VAR>s₁ : (g : { x // x ∈ t }) → Finset (Mₚ g)<VAR>s₂ : ∀ (g : { x // x ∈ t }), Submodule.span (Rₚ g) ↑(s₁ g) = ⊤<VAR>sf : { x // x ∈ t } → Finset M := fun x => IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers ↑x) (f x) (s₁ x)<GOAL>⊤ ≤ ⨆ x, Submodule.span R ↑(sf x)
<VAR>R : Type u<VAR>inst✝¹⁰ : CommRing R<VAR>S : Submonoid R<VAR>M : Type w<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>t : Finset R<VAR>ht : Ideal.span ↑t = ⊤<VAR>Mₚ : { x // x ∈ t } → Type u_1<VAR>inst✝⁷ : (g : { x // x ∈ t }) → AddCommMonoid (Mₚ g)<VAR>inst✝⁶ : (g : { x // x ∈ t }) → Module R (Mₚ g)<VAR>Rₚ : { x // x ∈ t } → Type u<VAR>inst✝⁵ : (g : { x // x ∈ t }) → CommRing (Rₚ g)<VAR>inst✝⁴ : (g : { x // x ∈ t }) → Algebra R (Rₚ g)<VAR>inst✝³ : ∀ (g : { x // x ∈ t }), IsLocalization.Away (↑g) (Rₚ g)<VAR>inst✝² : (g : { x // x ∈ t }) → Module (Rₚ g) (Mₚ g)<VAR>inst✝¹ : ∀ (g : { x // x ∈ t }), IsScalarTower R (Rₚ g) (Mₚ g)<VAR>f : (g : { x // x ∈ t }) → M →ₗ[R] Mₚ g<VAR>inst✝ : ∀ (g : { x // x ∈ t }), IsLocalizedModule (Submonoid.powers ↑g) (f g)<VAR>H : ∀ (g : { x // x ∈ t }), Finite (Rₚ g) (Mₚ g)<VAR>s₁ : (g : { x // x ∈ t }) → Finset (Mₚ g)<VAR>s₂ : ∀ (g : { x // x ∈ t }), Submodule.span (Rₚ g) ↑(s₁ g) = ⊤<VAR>sf : { x // x ∈ t } → Finset M := fun x => IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers ↑x) (f x) (s₁ x)<VAR>x : M<GOAL>x ∈ ⨆ x, Submodule.span R ↑(sf x)
<VAR>R : Type u<VAR>inst✝¹⁰ : CommRing R<VAR>S : Submonoid R<VAR>M : Type w<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>t : Finset R<VAR>ht : Ideal.span ↑t = ⊤<VAR>Mₚ : { x // x ∈ t } → Type u_1<VAR>inst✝⁷ : (g : { x // x ∈ t }) → AddCommMonoid (Mₚ g)<VAR>inst✝⁶ : (g : { x // x ∈ t }) → Module R (Mₚ g)<VAR>Rₚ : { x // x ∈ t } → Type u<VAR>inst✝⁵ : (g : { x // x ∈ t }) → CommRing (Rₚ g)<VAR>inst✝⁴ : (g : { x // x ∈ t }) → Algebra R (Rₚ g)<VAR>inst✝³ : ∀ (g : { x // x ∈ t }), IsLocalization.Away (↑g) (Rₚ g)<VAR>inst✝² : (g : { x // x ∈ t }) → Module (Rₚ g) (Mₚ g)<VAR>inst✝¹ : ∀ (g : { x // x ∈ t }), IsScalarTower R (Rₚ g) (Mₚ g)<VAR>f : (g : { x // x ∈ t }) → M →ₗ[R] Mₚ g<VAR>inst✝ : ∀ (g : { x // x ∈ t }), IsLocalizedModule (Submonoid.powers ↑g) (f g)<VAR>H : ∀ (g : { x // x ∈ t }), Finite (Rₚ g) (Mₚ g)<VAR>s₁ : (g : { x // x ∈ t }) → Finset (Mₚ g)<VAR>s₂ : ∀ (g : { x // x ∈ t }), Submodule.span (Rₚ g) ↑(s₁ g) = ⊤<VAR>sf : { x // x ∈ t } → Finset M := fun x => IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers ↑x) (f x) (s₁ x)<VAR>x : M<VAR>r : ↑↑t<GOAL>∃ n, ↑r ^ n • x ∈ ⨆ x, Submodule.span R ↑(sf x)
<VAR>R : Type u<VAR>inst✝¹⁰ : CommRing R<VAR>S✝ : Submonoid R<VAR>M : Type w<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>t : Finset R<VAR>ht : Ideal.span ↑t = ⊤<VAR>Mₚ : { x // x ∈ t } → Type u_1<VAR>inst✝⁷ : (g : { x // x ∈ t }) → AddCommMonoid (Mₚ g)<VAR>inst✝⁶ : (g : { x // x ∈ t }) → Module R (Mₚ g)<VAR>Rₚ : { x // x ∈ t } → Type u<VAR>inst✝⁵ : (g : { x // x ∈ t }) → CommRing (Rₚ g)<VAR>inst✝⁴ : (g : { x // x ∈ t }) → Algebra R (Rₚ g)<VAR>inst✝³ : ∀ (g : { x // x ∈ t }), IsLocalization.Away (↑g) (Rₚ g)<VAR>inst✝² : (g : { x // x ∈ t }) → Module (Rₚ g) (Mₚ g)<VAR>inst✝¹ : ∀ (g : { x // x ∈ t }), IsScalarTower R (Rₚ g) (Mₚ g)<VAR>f : (g : { x // x ∈ t }) → M →ₗ[R] Mₚ g<VAR>inst✝ : ∀ (g : { x // x ∈ t }), IsLocalizedModule (Submonoid.powers ↑g) (f g)<VAR>H : ∀ (g : { x // x ∈ t }), Finite (Rₚ g) (Mₚ g)<VAR>s₁ : (g : { x // x ∈ t }) → Finset (Mₚ g)<VAR>s₂ : ∀ (g : { x // x ∈ t }), Submodule.span (Rₚ g) ↑(s₁ g) = ⊤<VAR>sf : { x // x ∈ t } → Finset M := fun x => IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers ↑x) (f x) (s₁ x)<VAR>x : M<VAR>r : ↑↑t<VAR>S : Submonoid R := Submonoid.powers ↑r<GOAL>∃ n, ↑r ^ n • x ∈ ⨆ x, Submodule.span R ↑(sf x)
<VAR>R : Type u<VAR>inst✝¹⁰ : CommRing R<VAR>S✝ : Submonoid R<VAR>M : Type w<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>t : Finset R<VAR>ht : Ideal.span ↑t = ⊤<VAR>Mₚ : { x // x ∈ t } → Type u_1<VAR>inst✝⁷ : (g : { x // x ∈ t }) → AddCommMonoid (Mₚ g)<VAR>inst✝⁶ : (g : { x // x ∈ t }) → Module R (Mₚ g)<VAR>Rₚ : { x // x ∈ t } → Type u<VAR>inst✝⁵ : (g : { x // x ∈ t }) → CommRing (Rₚ g)<VAR>inst✝⁴ : (g : { x // x ∈ t }) → Algebra R (Rₚ g)<VAR>inst✝³ : ∀ (g : { x // x ∈ t }), IsLocalization.Away (↑g) (Rₚ g)<VAR>inst✝² : (g : { x // x ∈ t }) → Module (Rₚ g) (Mₚ g)<VAR>inst✝¹ : ∀ (g : { x // x ∈ t }), IsScalarTower R (Rₚ g) (Mₚ g)<VAR>f : (g : { x // x ∈ t }) → M →ₗ[R] Mₚ g<VAR>inst✝ : ∀ (g : { x // x ∈ t }), IsLocalizedModule (Submonoid.powers ↑g) (f g)<VAR>H : ∀ (g : { x // x ∈ t }), Finite (Rₚ g) (Mₚ g)<VAR>s₁ : (g : { x // x ∈ t }) → Finset (Mₚ g)<VAR>s₂ : ∀ (g : { x // x ∈ t }), Submodule.span (Rₚ g) ↑(s₁ g) = ⊤<VAR>sf : { x // x ∈ t } → Finset M := fun x => IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers ↑x) (f x) (s₁ x)<VAR>x : M<VAR>r : ↑↑t<VAR>S : Submonoid R := Submonoid.powers ↑r<VAR>n₁ : ℕ<VAR>hn₁ : ⟨(fun x => ↑r ^ x) n₁, ⋯⟩ • IsLocalizedModule.mk' (f r) x 1 ∈ Submodule.span R ↑(s₁ r)<GOAL>∃ n, ↑r ^ n • x ∈ ⨆ x, Submodule.span R ↑(sf x)
<VAR>R : Type u<VAR>inst✝¹⁰ : CommRing R<VAR>S✝ : Submonoid R<VAR>M : Type w<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>t : Finset R<VAR>ht : Ideal.span ↑t = ⊤<VAR>Mₚ : { x // x ∈ t } → Type u_1<VAR>inst✝⁷ : (g : { x // x ∈ t }) → AddCommMonoid (Mₚ g)<VAR>inst✝⁶ : (g : { x // x ∈ t }) → Module R (Mₚ g)<VAR>Rₚ : { x // x ∈ t } → Type u<VAR>inst✝⁵ : (g : { x // x ∈ t }) → CommRing (Rₚ g)<VAR>inst✝⁴ : (g : { x // x ∈ t }) → Algebra R (Rₚ g)<VAR>inst✝³ : ∀ (g : { x // x ∈ t }), IsLocalization.Away (↑g) (Rₚ g)<VAR>inst✝² : (g : { x // x ∈ t }) → Module (Rₚ g) (Mₚ g)<VAR>inst✝¹ : ∀ (g : { x // x ∈ t }), IsScalarTower R (Rₚ g) (Mₚ g)<VAR>f : (g : { x // x ∈ t }) → M →ₗ[R] Mₚ g<VAR>inst✝ : ∀ (g : { x // x ∈ t }), IsLocalizedModule (Submonoid.powers ↑g) (f g)<VAR>H : ∀ (g : { x // x ∈ t }), Finite (Rₚ g) (Mₚ g)<VAR>s₁ : (g : { x // x ∈ t }) → Finset (Mₚ g)<VAR>s₂ : ∀ (g : { x // x ∈ t }), Submodule.span (Rₚ g) ↑(s₁ g) = ⊤<VAR>sf : { x // x ∈ t } → Finset M := fun x => IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers ↑x) (f x) (s₁ x)<VAR>x : M<VAR>r : ↑↑t<VAR>S : Submonoid R := Submonoid.powers ↑r<VAR>n₁ : ℕ<VAR>hn₁ : (f r) (↑⟨(fun x => ↑r ^ x) n₁, ⋯⟩ • x) ∈ Submodule.span R ↑(s₁ r)<GOAL>∃ n, ↑r ^ n • x ∈ ⨆ x, Submodule.span R ↑(sf x)
<VAR>R : Type u<VAR>inst✝¹⁰ : CommRing R<VAR>S✝ : Submonoid R<VAR>M : Type w<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>t : Finset R<VAR>ht : Ideal.span ↑t = ⊤<VAR>Mₚ : { x // x ∈ t } → Type u_1<VAR>inst✝⁷ : (g : { x // x ∈ t }) → AddCommMonoid (Mₚ g)<VAR>inst✝⁶ : (g : { x // x ∈ t }) → Module R (Mₚ g)<VAR>Rₚ : { x // x ∈ t } → Type u<VAR>inst✝⁵ : (g : { x // x ∈ t }) → CommRing (Rₚ g)<VAR>inst✝⁴ : (g : { x // x ∈ t }) → Algebra R (Rₚ g)<VAR>inst✝³ : ∀ (g : { x // x ∈ t }), IsLocalization.Away (↑g) (Rₚ g)<VAR>inst✝² : (g : { x // x ∈ t }) → Module (Rₚ g) (Mₚ g)<VAR>inst✝¹ : ∀ (g : { x // x ∈ t }), IsScalarTower R (Rₚ g) (Mₚ g)<VAR>f : (g : { x // x ∈ t }) → M →ₗ[R] Mₚ g<VAR>inst✝ : ∀ (g : { x // x ∈ t }), IsLocalizedModule (Submonoid.powers ↑g) (f g)<VAR>H : ∀ (g : { x // x ∈ t }), Finite (Rₚ g) (Mₚ g)<VAR>s₁ : (g : { x // x ∈ t }) → Finset (Mₚ g)<VAR>s₂ : ∀ (g : { x // x ∈ t }), Submodule.span (Rₚ g) ↑(s₁ g) = ⊤<VAR>sf : { x // x ∈ t } → Finset M := fun x => IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers ↑x) (f x) (s₁ x)<VAR>x : M<VAR>r : ↑↑t<VAR>S : Submonoid R := Submonoid.powers ↑r<VAR>n₁ : ℕ<VAR>hn₁ : (f r) (↑⟨(fun x => ↑r ^ x) n₁, ⋯⟩ • x) ∈ Submodule.span R ↑(s₁ r)<VAR>n₂ : ℕ<VAR>hn₂ : ⟨(fun x => ↑r ^ x) n₂, ⋯⟩ • ↑⟨(fun x => ↑r ^ x) n₁, ⋯⟩ • x ∈ Submodule.span R ↑(IsLocalizedModule.finsetIntegerMultiple S (f r) (s₁ r))<GOAL>∃ n, ↑r ^ n • x ∈ ⨆ x, Submodule.span R ↑(sf x)
<VAR>R : Type u<VAR>inst✝¹⁰ : CommRing R<VAR>S✝ : Submonoid R<VAR>M : Type w<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>t : Finset R<VAR>ht : Ideal.span ↑t = ⊤<VAR>Mₚ : { x // x ∈ t } → Type u_1<VAR>inst✝⁷ : (g : { x // x ∈ t }) → AddCommMonoid (Mₚ g)<VAR>inst✝⁶ : (g : { x // x ∈ t }) → Module R (Mₚ g)<VAR>Rₚ : { x // x ∈ t } → Type u<VAR>inst✝⁵ : (g : { x // x ∈ t }) → CommRing (Rₚ g)<VAR>inst✝⁴ : (g : { x // x ∈ t }) → Algebra R (Rₚ g)<VAR>inst✝³ : ∀ (g : { x // x ∈ t }), IsLocalization.Away (↑g) (Rₚ g)<VAR>inst✝² : (g : { x // x ∈ t }) → Module (Rₚ g) (Mₚ g)<VAR>inst✝¹ : ∀ (g : { x // x ∈ t }), IsScalarTower R (Rₚ g) (Mₚ g)<VAR>f : (g : { x // x ∈ t }) → M →ₗ[R] Mₚ g<VAR>inst✝ : ∀ (g : { x // x ∈ t }), IsLocalizedModule (Submonoid.powers ↑g) (f g)<VAR>H : ∀ (g : { x // x ∈ t }), Finite (Rₚ g) (Mₚ g)<VAR>s₁ : (g : { x // x ∈ t }) → Finset (Mₚ g)<VAR>s₂ : ∀ (g : { x // x ∈ t }), Submodule.span (Rₚ g) ↑(s₁ g) = ⊤<VAR>sf : { x // x ∈ t } → Finset M := fun x => IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers ↑x) (f x) (s₁ x)<VAR>x : M<VAR>r : ↑↑t<VAR>S : Submonoid R := Submonoid.powers ↑r<VAR>n₁ : ℕ<VAR>hn₁ : (f r) (↑⟨(fun x => ↑r ^ x) n₁, ⋯⟩ • x) ∈ Submodule.span R ↑(s₁ r)<VAR>n₂ : ℕ<VAR>hn₂ : ↑⟨(fun x => ↑r ^ x) n₂, ⋯⟩ • ↑⟨(fun x => ↑r ^ x) n₁, ⋯⟩ • x ∈ Submodule.span R ↑(IsLocalizedModule.finsetIntegerMultiple S (f r) (s₁ r))<GOAL>∃ n, ↑r ^ n • x ∈ ⨆ x, Submodule.span R ↑(sf x)