ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>p : ℕ → Prop<VAR>s : ℕ → Set α<VAR>hs : ∀ (i : ℕ), IsClosed (s i)<VAR>r₁ r₂ : ℕ → ℝ<VAR>hrp : 0 ≤ r₁<VAR>M : ℝ<VAR>hM : 0 < M<VAR>hM' : M < 1<VAR>Y₁ : ℕ → Set α := fun i => cthickening (r₁ i) (s i)<VAR>Y₂ : ℕ → Set α := fun i => cthickening (r₂ i) (s i)<VAR>Z : ℕ → Set α := fun i => ⋃ j, ⋃ (_ : p j ∧ i ≤ j), Y₂ j<VAR>i : ℕ<VAR>W : Set α := blimsup Y₁ atTop p \ Z i<VAR>contra : ¬μ W = 0<VAR>d : α<VAR>hd' : ∀ {ι : Type} {l : Filter ι} (w : ι → α) (δ : ι → ℝ), Tendsto δ l (𝓝[>] 0) → (∀ᶠ (j : ι) in l, d ∈ closedBall (w j) (2 * δ j)) → Tendsto (fun j => μ (W ∩ closedBall (w j) (δ j)) / μ (closedBall (w j) (δ j))) l (𝓝 1)<VAR>hd : d ∈ blimsup Y₁ atTop p<VAR>f : ℕ → ℕ<VAR>hf₁ : ∀ (x : ℕ), p (f x)<VAR>hf₂ : ∀ (j : ℕ), j ≤ f j<VAR>hf₃ : Tendsto f atTop atTop<VAR>hr : Tendsto (r₁ ∘ f) atTop (𝓝[>] 0)<VAR>hMr : ∀ᶠ (j : ℕ) in atTop, M * r₁ (f j) ≤ r₂ (f j)<VAR>w : ℕ → α<VAR>hw : ∀ (j : ℕ), w j ∈ s (f j)<VAR>hw' : ∀ (j : ℕ), d ∈ closedBall (w j) (2 * r₁ (f j))<VAR>C : ℝ≥0 := IsUnifLocDoublingMeasure.scalingConstantOf μ M⁻¹<VAR>hC : C ≠ 0<VAR>b : ℕ → Set α := fun j => closedBall (w j) (M * r₁ (f j))<VAR>B : ℕ → Set α := fun j => closedBall (w j) (r₁ (f j))<VAR>h₁ : ∀ (j : ℕ), b j ⊆ B j<VAR>h₂ : ∀ (j : ℕ), W ∩ B j ⊆ B j<VAR>h₃ : ∀ᶠ (j : ℕ) in atTop, Disjoint (b j) (W ∩ B j)<VAR>h₄ : ∀ᶠ (j : ℕ) in atTop, μ (B j) ≤ ↑C * μ (b j)<VAR>j : ℕ<VAR>hB : ↑C⁻¹ * μ (B j) ≠ ⊤<VAR>hj₁ : Disjoint (b j) (W ∩ B j)<VAR>hj₂ : ↑C⁻¹ * μ (B j) ≤ μ (b j)<VAR>hj₃ : ↑C⁻¹ * μ (B j) + μ (W ∩ B j) ≤ μ (B j)<GOAL>μ (W ∩ B j) ≤ μ (B j) - ↑C⁻¹ * μ (B j)
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>p : ℕ → Prop<VAR>s : ℕ → Set α<VAR>hs : ∀ (i : ℕ), IsClosed (s i)<VAR>r₁ r₂ : ℕ → ℝ<VAR>hrp : 0 ≤ r₁<VAR>M : ℝ<VAR>hM : 0 < M<VAR>hM' : M < 1<VAR>Y₁ : ℕ → Set α := fun i => cthickening (r₁ i) (s i)<VAR>Y₂ : ℕ → Set α := fun i => cthickening (r₂ i) (s i)<VAR>Z : ℕ → Set α := fun i => ⋃ j, ⋃ (_ : p j ∧ i ≤ j), Y₂ j<VAR>i : ℕ<VAR>W : Set α := blimsup Y₁ atTop p \ Z i<VAR>contra : ¬μ W = 0<VAR>d : α<VAR>hd' : ∀ {ι : Type} {l : Filter ι} (w : ι → α) (δ : ι → ℝ), Tendsto δ l (𝓝[>] 0) → (∀ᶠ (j : ι) in l, d ∈ closedBall (w j) (2 * δ j)) → Tendsto (fun j => μ (W ∩ closedBall (w j) (δ j)) / μ (closedBall (w j) (δ j))) l (𝓝 1)<VAR>hd : d ∈ blimsup Y₁ atTop p<VAR>f : ℕ → ℕ<VAR>hf₁ : ∀ (x : ℕ), p (f x)<VAR>hf₂ : ∀ (j : ℕ), j ≤ f j<VAR>hf₃ : Tendsto f atTop atTop<VAR>hr : Tendsto (r₁ ∘ f) atTop (𝓝[>] 0)<VAR>hMr : ∀ᶠ (j : ℕ) in atTop, M * r₁ (f j) ≤ r₂ (f j)<VAR>w : ℕ → α<VAR>hw : ∀ (j : ℕ), w j ∈ s (f j)<VAR>hw' : ∀ (j : ℕ), d ∈ closedBall (w j) (2 * r₁ (f j))<VAR>C : ℝ≥0 := IsUnifLocDoublingMeasure.scalingConstantOf μ M⁻¹<VAR>hC : C ≠ 0<VAR>b : ℕ → Set α := fun j => closedBall (w j) (M * r₁ (f j))<VAR>B : ℕ → Set α := fun j => closedBall (w j) (r₁ (f j))<VAR>h₁ : ∀ (j : ℕ), b j ⊆ B j<VAR>h₂ : ∀ (j : ℕ), W ∩ B j ⊆ B j<VAR>h₃ : ∀ᶠ (j : ℕ) in atTop, Disjoint (b j) (W ∩ B j)<VAR>h₄ : ∀ᶠ (j : ℕ) in atTop, μ (B j) ≤ ↑C * μ (b j)<VAR>j : ℕ<VAR>hB : ↑C⁻¹ * μ (B j) ≠ ⊤<VAR>hj₁ : Disjoint (b j) (W ∩ B j)<VAR>hj₂ : ↑C⁻¹ * μ (B j) ≤ μ (b j)<VAR>hj₃ : ↑C⁻¹ * μ (B j) + μ (W ∩ B j) - ↑C⁻¹ * μ (B j) ≤ μ (B j) - ↑C⁻¹ * μ (B j)<GOAL>μ (W ∩ B j) ≤ μ (B j) - ↑C⁻¹ * μ (B j)
<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>l : Filter ι<VAR>p : ι → Prop<VAR>inst✝ : l.IsCountablyGenerated<VAR>h : ∃ᶠ (n : ι) in l, p n<GOAL>∃ ns, Tendsto ns atTop l ∧ ∀ (n : ℕ), p (ns 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>l : Filter ι<VAR>p : ι → Prop<VAR>inst✝ : l.IsCountablyGenerated<VAR>h : ∃ x, Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)<GOAL>∃ ns, Tendsto ns atTop l ∧ ∀ (n : ℕ), p (ns 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>l : Filter ι<VAR>p : ι → Prop<VAR>inst✝ : l.IsCountablyGenerated<VAR>x : ℕ → ι<VAR>hx_tendsto : Tendsto x atTop l<VAR>hx_freq : ∃ᶠ (n : ℕ) in atTop, p (x n)<GOAL>∃ ns, Tendsto ns atTop l ∧ ∀ (n : ℕ), p (ns 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>l : Filter ι<VAR>p : ι → Prop<VAR>inst✝ : l.IsCountablyGenerated<VAR>x : ℕ → ι<VAR>hx_tendsto : Tendsto x atTop l<VAR>hx_freq : ∃ᶠ (n : ℕ) in atTop, p (x n)<VAR>n_to_n : ℕ → ℕ<VAR>h_tendsto : Tendsto (fun n => x (n_to_n n)) atTop l<VAR>h_freq : ∀ (n : ℕ), p (x (n_to_n n))<GOAL>∃ ns, Tendsto ns atTop l ∧ ∀ (n : ℕ), p (ns n)
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>u v : V<VAR>p : G.Walk u v<GOAL>(induce {v_1 | v_1 ∈ p.support} G).Connected
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>u v : V<VAR>p : G.Walk u v<GOAL>(induce p.toSubgraph.verts G).Connected
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : NormedOrderedGroup α<VAR>s : Set α<VAR>hs : IsLowerSet s<VAR>ε : ℝ<GOAL>IsLowerSet (cthickening ε s)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : NormedOrderedGroup α<VAR>s : Set α<VAR>hs : IsLowerSet s<VAR>ε : ℝ<GOAL>IsLowerSet (⋂ ε_1, ⋂ (_ : max 0 ε < ε_1), thickening ε_1 s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁✝ a₂✝ : α<VAR>b✝ b₁ b₂ : β<VAR>γ : Type u_3<VAR>inst✝⁸ : Zero α<VAR>inst✝⁷ : Preorder α<VAR>inst✝⁶ : Zero β<VAR>inst✝⁵ : Preorder β<VAR>inst✝⁴ : Zero γ<VAR>inst✝³ : Preorder γ<VAR>inst✝² : SMul α β<VAR>inst✝¹ : SMul α γ<VAR>f : β → γ<VAR>inst✝ : SMulPosReflectLT α γ<VAR>hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂<VAR>smul : ∀ (a : α) (b : β), f (a • b) = a • f b<VAR>zero : f 0 = 0<VAR>b : β<VAR>hb : 0 ≤ b<VAR>a₁ a₂ : α<VAR>h : a₁ • b < a₂ • b<GOAL>a₁ < a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁✝ a₂✝ : α<VAR>b✝ b₁ b₂ : β<VAR>γ : Type u_3<VAR>inst✝⁸ : Zero α<VAR>inst✝⁷ : Preorder α<VAR>inst✝⁶ : Zero β<VAR>inst✝⁵ : Preorder β<VAR>inst✝⁴ : Zero γ<VAR>inst✝³ : Preorder γ<VAR>inst✝² : SMul α β<VAR>inst✝¹ : SMul α γ<VAR>f : β → γ<VAR>inst✝ : SMulPosReflectLT α γ<VAR>b : β<VAR>a₁ a₂ : α<VAR>hf : ∀ {b₁ b₂ : β}, True<VAR>smul : α → β → True<VAR>zero : True<VAR>hb : 0 ≤ f b<VAR>h : a₁ • f b < a₂ • f b<GOAL>a₁ < a₂
<VAR>α : Type u_1<VAR>inst✝ : CoheytingAlgebra α<VAR>a✝ b a : α<GOAL>∂ ∂ a = ∂ a
<VAR>α : Type u_1<VAR>f : α → ℝ<VAR>y : ℝ<VAR>hf₀ : ∀ (n : α), 0 ≤ f n<VAR>hy : HasSum f y<GOAL>HasSum (fun x => (f x).toNNReal) y.toNNReal
<VAR>α : Type u_1<VAR>f : α → ℝ<VAR>hf₀ : ∀ (n : α), 0 ≤ f n<VAR>y : ℝ≥0<VAR>hy : HasSum f ↑y<GOAL>HasSum (fun x => (f x).toNNReal) (↑y).toNNReal
<VAR>α : Type u_1<VAR>y : ℝ≥0<VAR>f : α → ℝ≥0<VAR>hy : HasSum (fun i => ↑(f i)) ↑y<GOAL>HasSum (fun x => ((fun i => ↑(f i)) x).toNNReal) (↑y).toNNReal
<VAR>R : Type u_1<VAR>inst✝⁷ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁶ : CommSemiring S<VAR>inst✝⁵ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁴ : CommSemiring P<VAR>inst✝³ : IsLocalization M S<VAR>g : R →+* P<VAR>hg : ∀ (y : ↥M), IsUnit (g ↑y)<VAR>T : Submonoid P<VAR>Q : Type u_4<VAR>inst✝² : CommSemiring Q<VAR>hy : M ≤ Submonoid.comap g T<VAR>inst✝¹ : Algebra P Q<VAR>inst✝ : IsLocalization T Q<VAR>h : R ≃+* P<VAR>H : Submonoid.map h.toMonoidHom M = T<GOAL>Submonoid.map h.symm.toMonoidHom T = M
<VAR>R : Type u_1<VAR>inst✝⁷ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁶ : CommSemiring S<VAR>inst✝⁵ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁴ : CommSemiring P<VAR>inst✝³ : IsLocalization M S<VAR>g : R →+* P<VAR>hg : ∀ (y : ↥M), IsUnit (g ↑y)<VAR>T : Submonoid P<VAR>Q : Type u_4<VAR>inst✝² : CommSemiring Q<VAR>hy : M ≤ Submonoid.comap g T<VAR>inst✝¹ : Algebra P Q<VAR>inst✝ : IsLocalization T Q<VAR>h : R ≃+* P<VAR>H : Submonoid.map h.toMonoidHom M = T<GOAL>Submonoid.map (h.symm.toMonoidHom.comp h.toMonoidHom) M = Submonoid.map (MonoidHom.id R) M
<VAR>R : Type u_1<VAR>inst✝⁷ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁶ : CommSemiring S<VAR>inst✝⁵ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁴ : CommSemiring P<VAR>inst✝³ : IsLocalization M S<VAR>g : R →+* P<VAR>hg : ∀ (y : ↥M), IsUnit (g ↑y)<VAR>T : Submonoid P<VAR>Q : Type u_4<VAR>inst✝² : CommSemiring Q<VAR>hy : M ≤ Submonoid.comap g T<VAR>inst✝¹ : Algebra P Q<VAR>inst✝ : IsLocalization T Q<VAR>h : R ≃+* P<VAR>H : Submonoid.map h.toMonoidHom M = T<VAR>x✝ : R<GOAL>(h.symm.toMonoidHom.comp h.toMonoidHom) x✝ = (MonoidHom.id R) x✝
<VAR>R : Type u_1<VAR>inst✝⁷ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁶ : CommSemiring S<VAR>inst✝⁵ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁴ : CommSemiring P<VAR>inst✝³ : IsLocalization M S<VAR>g : R →+* P<VAR>hg : ∀ (y : ↥M), IsUnit (g ↑y)<VAR>T : Submonoid P<VAR>Q : Type u_4<VAR>inst✝² : CommSemiring Q<VAR>hy : M ≤ Submonoid.comap g T<VAR>inst✝¹ : Algebra P Q<VAR>inst✝ : IsLocalization T Q<VAR>h : R ≃+* P<VAR>H : Submonoid.map h.toMonoidHom M = T<VAR>H' : Submonoid.map h.symm.toMonoidHom T = M<VAR>x : S<GOAL>(map S ↑h.symm ⋯) ((map Q ↑h ⋯) x) = x
<VAR>R : Type u_1<VAR>inst✝⁷ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁶ : CommSemiring S<VAR>inst✝⁵ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁴ : CommSemiring P<VAR>inst✝³ : IsLocalization M S<VAR>g : R →+* P<VAR>hg : ∀ (y : ↥M), IsUnit (g ↑y)<VAR>T : Submonoid P<VAR>Q : Type u_4<VAR>inst✝² : CommSemiring Q<VAR>hy : M ≤ Submonoid.comap g T<VAR>inst✝¹ : Algebra P Q<VAR>inst✝ : IsLocalization T Q<VAR>h : R ≃+* P<VAR>H : Submonoid.map h.toMonoidHom M = T<VAR>H' : Submonoid.map h.symm.toMonoidHom T = M<VAR>x : S<GOAL>∀ (x : R), (RingHom.id S) ((algebraMap R S) x) = (algebraMap R S) (((↑h.symm).comp ↑h) x)
<VAR>R : Type u_1<VAR>inst✝⁷ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁶ : CommSemiring S<VAR>inst✝⁵ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁴ : CommSemiring P<VAR>inst✝³ : IsLocalization M S<VAR>g : R →+* P<VAR>hg : ∀ (y : ↥M), IsUnit (g ↑y)<VAR>T : Submonoid P<VAR>Q : Type u_4<VAR>inst✝² : CommSemiring Q<VAR>hy : M ≤ Submonoid.comap g T<VAR>inst✝¹ : Algebra P Q<VAR>inst✝ : IsLocalization T Q<VAR>h : R ≃+* P<VAR>H : Submonoid.map h.toMonoidHom M = T<VAR>H' : Submonoid.map h.symm.toMonoidHom T = M<VAR>x : Q<GOAL>(map Q ↑h ⋯) ((map S ↑h.symm ⋯) x) = x
<VAR>R : Type u_1<VAR>inst✝⁷ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁶ : CommSemiring S<VAR>inst✝⁵ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁴ : CommSemiring P<VAR>inst✝³ : IsLocalization M S<VAR>g : R →+* P<VAR>hg : ∀ (y : ↥M), IsUnit (g ↑y)<VAR>T : Submonoid P<VAR>Q : Type u_4<VAR>inst✝² : CommSemiring Q<VAR>hy : M ≤ Submonoid.comap g T<VAR>inst✝¹ : Algebra P Q<VAR>inst✝ : IsLocalization T Q<VAR>h : R ≃+* P<VAR>H : Submonoid.map h.toMonoidHom M = T<VAR>H' : Submonoid.map h.symm.toMonoidHom T = M<VAR>x : Q<GOAL>∀ (x : P), (RingHom.id Q) ((algebraMap P Q) x) = (algebraMap P Q) (((↑h).comp ↑h.symm) x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>as : List α<GOAL>𝓝 as = traverse 𝓝 as
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>as : List α<GOAL>pure ≤ traverse 𝓝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>as : List α<GOAL>∀ (a : List α), ∀ s ∈ traverse 𝓝 a, ∀ᶠ (y : List α) in traverse 𝓝 a, s ∈ traverse 𝓝 y
<VAR>R✝ : Type u_1<VAR>inst✝¹⁷ : CommRing R✝<VAR>M✝ : Submonoid R✝<VAR>S✝ : Type u_2<VAR>inst✝¹⁶ : CommRing S✝<VAR>inst✝¹⁵ : Algebra R✝ S✝<VAR>P : Type u_3<VAR>inst✝¹⁴ : CommRing P<VAR>Rₘ✝ : Type u_4<VAR>Sₘ✝ : Type u_5<VAR>inst✝¹³ : CommRing Rₘ✝<VAR>inst✝¹² : CommRing Sₘ✝<VAR>inst✝¹¹ : Algebra R✝ Rₘ✝<VAR>inst✝¹⁰ : IsLocalization M✝ Rₘ✝<VAR>inst✝⁹ : Algebra S✝ Sₘ✝<VAR>inst✝⁸ : IsLocalization (Algebra.algebraMapSubmonoid S✝ M✝) Sₘ✝<VAR>R : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>x : S<VAR>p : R[X]<VAR>hf : eval₂ f x p = 0<VAR>M : Submonoid R<VAR>hM : p.leadingCoeff ∈ M<VAR>Rₘ : Type u_8<VAR>Sₘ : Type u_9<VAR>inst✝⁵ : CommRing Rₘ<VAR>inst✝⁴ : CommRing Sₘ<VAR>inst✝³ : Algebra R Rₘ<VAR>inst✝² : IsLocalization M Rₘ<VAR>inst✝¹ : Algebra S Sₘ<VAR>inst✝ : IsLocalization (Submonoid.map f M) Sₘ<VAR>triv : ¬1 = 0<GOAL>(IsLocalization.map Sₘ f ⋯).IsIntegralElem ((algebraMap S Sₘ) x)
<VAR>R✝ : Type u_1<VAR>inst✝¹⁷ : CommRing R✝<VAR>M✝ : Submonoid R✝<VAR>S✝ : Type u_2<VAR>inst✝¹⁶ : CommRing S✝<VAR>inst✝¹⁵ : Algebra R✝ S✝<VAR>P : Type u_3<VAR>inst✝¹⁴ : CommRing P<VAR>Rₘ✝ : Type u_4<VAR>Sₘ✝ : Type u_5<VAR>inst✝¹³ : CommRing Rₘ✝<VAR>inst✝¹² : CommRing Sₘ✝<VAR>inst✝¹¹ : Algebra R✝ Rₘ✝<VAR>inst✝¹⁰ : IsLocalization M✝ Rₘ✝<VAR>inst✝⁹ : Algebra S✝ Sₘ✝<VAR>inst✝⁸ : IsLocalization (Algebra.algebraMapSubmonoid S✝ M✝) Sₘ✝<VAR>R : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>x : S<VAR>p : R[X]<VAR>hf : eval₂ f x p = 0<VAR>M : Submonoid R<VAR>hM : p.leadingCoeff ∈ M<VAR>Rₘ : Type u_8<VAR>Sₘ : Type u_9<VAR>inst✝⁵ : CommRing Rₘ<VAR>inst✝⁴ : CommRing Sₘ<VAR>inst✝³ : Algebra R Rₘ<VAR>inst✝² : IsLocalization M Rₘ<VAR>inst✝¹ : Algebra S Sₘ<VAR>inst✝ : IsLocalization (Submonoid.map f M) Sₘ<VAR>triv : ¬1 = 0<VAR>this : Nontrivial Rₘ<GOAL>(IsLocalization.map Sₘ f ⋯).IsIntegralElem ((algebraMap S Sₘ) x)
<VAR>R✝ : Type u_1<VAR>inst✝¹⁷ : CommRing R✝<VAR>M✝ : Submonoid R✝<VAR>S✝ : Type u_2<VAR>inst✝¹⁶ : CommRing S✝<VAR>inst✝¹⁵ : Algebra R✝ S✝<VAR>P : Type u_3<VAR>inst✝¹⁴ : CommRing P<VAR>Rₘ✝ : Type u_4<VAR>Sₘ✝ : Type u_5<VAR>inst✝¹³ : CommRing Rₘ✝<VAR>inst✝¹² : CommRing Sₘ✝<VAR>inst✝¹¹ : Algebra R✝ Rₘ✝<VAR>inst✝¹⁰ : IsLocalization M✝ Rₘ✝<VAR>inst✝⁹ : Algebra S✝ Sₘ✝<VAR>inst✝⁸ : IsLocalization (Algebra.algebraMapSubmonoid S✝ M✝) Sₘ✝<VAR>R : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>x : S<VAR>p : R[X]<VAR>hf : eval₂ f x p = 0<VAR>M : Submonoid R<VAR>hM : p.leadingCoeff ∈ M<VAR>Rₘ : Type u_8<VAR>Sₘ : Type u_9<VAR>inst✝⁵ : CommRing Rₘ<VAR>inst✝⁴ : CommRing Sₘ<VAR>inst✝³ : Algebra R Rₘ<VAR>inst✝² : IsLocalization M Rₘ<VAR>inst✝¹ : Algebra S Sₘ<VAR>inst✝ : IsLocalization (Submonoid.map f M) Sₘ<VAR>triv : ¬1 = 0<VAR>this : Nontrivial Rₘ<VAR>b : Rₘ<VAR>hb : (algebraMap R Rₘ) ↑⟨p.leadingCoeff, hM⟩ * b = 1<GOAL>(IsLocalization.map Sₘ f ⋯).IsIntegralElem ((algebraMap S Sₘ) x)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝³ : (i : ι) → Zero (α i)<VAR>inst✝² : (i : ι) → Lattice (α i)<VAR>f g : Π₀ (i : ι), α i<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)<VAR>x✝ : ι<GOAL>x✝ ∈ (↑((f ⊓ g).support ∪ (f ⊔ g).support))ᶜ ↔ x✝ ∈ (↑(f.support ∪ g.support))ᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>inst✝¹ : AddZeroClass δ<VAR>inst✝ : Min δ<VAR>C : Cost α β δ<VAR>xs : List α<VAR>ys : List β<GOAL>(suffixLevenshtein C xs ys).val.length = xs.length + 1
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizationMonoid R<GOAL>normUnit X = 1
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizationMonoid R<VAR>this : ↑(normUnit X) = C ↑(normUnit X.leadingCoeff)<GOAL>normUnit X = 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>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>f : α × α → β<GOAL>∏ i ∈ s.diag, f i = ∏ i ∈ s, f (i, i)
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝¹⁰ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁹ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁸ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>E : Type u_9<VAR>inst✝⁵ : AddCommMonoid E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_10<VAR>inst✝³ : AddCommMonoid F<VAR>t : ι → Type u_11<VAR>inst✝² : (i : ι) → AddCommMonoid (t i)<VAR>inst✝¹ : (i : ι) → Module R (t i)<VAR>inst✝ : IsEmpty ι<VAR>x : ⨂[R] (i : ι), s i<GOAL>(fun r => r • (tprod R) isEmptyElim) ({ toFun := ⇑(lift (constOfIsEmpty R s 1)), map_add' := ⋯, map_smul' := ⋯ }.toFun x) = x
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝¹⁰ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁹ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁸ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>E : Type u_9<VAR>inst✝⁵ : AddCommMonoid E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_10<VAR>inst✝³ : AddCommMonoid F<VAR>t : ι → Type u_11<VAR>inst✝² : (i : ι) → AddCommMonoid (t i)<VAR>inst✝¹ : (i : ι) → Module R (t i)<VAR>inst✝ : IsEmpty ι<VAR>x : ⨂[R] (i : ι), s i<GOAL>∀ (r : R) (f : (i : ι) → s i), (fun r => r • (tprod R) isEmptyElim) ({ toFun := ⇑(lift (constOfIsEmpty R s 1)), map_add' := ⋯, map_smul' := ⋯ }.toFun (r • (tprod R) f)) = r • (tprod R) f
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝¹⁰ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁹ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁸ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>E : Type u_9<VAR>inst✝⁵ : AddCommMonoid E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_10<VAR>inst✝³ : AddCommMonoid F<VAR>t : ι → Type u_11<VAR>inst✝² : (i : ι) → AddCommMonoid (t i)<VAR>inst✝¹ : (i : ι) → Module R (t i)<VAR>inst✝ : IsEmpty ι<VAR>x : ⨂[R] (i : ι), s i<GOAL>∀ (x y : ⨂[R] (i : ι), s i), (fun r => r • (tprod R) isEmptyElim) ({ toFun := ⇑(lift (constOfIsEmpty R s 1)), map_add' := ⋯, map_smul' := ⋯ }.toFun x) = x → (fun r => r • (tprod R) isEmptyElim) ({ toFun := ⇑(lift (constOfIsEmpty R s 1)), map_add' := ⋯, map_smul' := ⋯ }.toFun y) = y → (fun r => r • (tprod R) isEmptyElim) ({ toFun := ⇑(lift (constOfIsEmpty R s 1)), map_add' := ⋯, map_smul' := ⋯ }.toFun (x + y)) = x + y
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝¹⁰ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁹ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁸ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>E : Type u_9<VAR>inst✝⁵ : AddCommMonoid E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_10<VAR>inst✝³ : AddCommMonoid F<VAR>t : ι → Type u_11<VAR>inst✝² : (i : ι) → AddCommMonoid (t i)<VAR>inst✝¹ : (i : ι) → Module R (t i)<VAR>inst✝ : IsEmpty ι<VAR>r : R<VAR>x : ⨂[R] (i : ι), s i<GOAL>(lift (constOfIsEmpty R s 1)) (r • x) = (RingHom.id R) r • (lift (constOfIsEmpty R s 1)) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s : Set α<VAR>t : Set β<GOAL>s ×ˢ t = (Prod.mk '' s).seq t
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>a : R<GOAL>(if a0 : 0 = 0 then a else let_fun x := ⋯; gcd (a % 0) 0) = a
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>τ σ : Ω → ι<VAR>E : Type u_4<VAR>p : ℝ≥0∞<VAR>u : ι → Ω → E<VAR>inst✝⁴ : LinearOrder ι<VAR>inst✝³ : TopologicalSpace ι<VAR>inst✝² : OrderTopology ι<VAR>inst✝¹ : FirstCountableTopology ι<VAR>ℱ : Filtration ι m<VAR>inst✝ : NormedAddCommGroup E<VAR>hτ : IsStoppingTime ℱ τ<VAR>hu : ∀ (n : ι), Memℒp (u n) p μ<VAR>n : ι<VAR>s : Finset ι<VAR>hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s<GOAL>Memℒp (stoppedProcess u τ n) p μ
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>τ σ : Ω → ι<VAR>E : Type u_4<VAR>p : ℝ≥0∞<VAR>u : ι → Ω → E<VAR>inst✝⁴ : LinearOrder ι<VAR>inst✝³ : TopologicalSpace ι<VAR>inst✝² : OrderTopology ι<VAR>inst✝¹ : FirstCountableTopology ι<VAR>ℱ : Filtration ι m<VAR>inst✝ : NormedAddCommGroup E<VAR>hτ : IsStoppingTime ℱ τ<VAR>hu : ∀ (n : ι), Memℒp (u n) p μ<VAR>n : ι<VAR>s : Finset ι<VAR>hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s<GOAL>Memℒp ({a | n ≤ τ a}.indicator (u n) + ∑ i ∈ Finset.filter (fun x => x < n) s, {ω | τ ω = i}.indicator (u i)) p μ
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>τ σ : Ω → ι<VAR>E : Type u_4<VAR>p : ℝ≥0∞<VAR>u : ι → Ω → E<VAR>inst✝⁴ : LinearOrder ι<VAR>inst✝³ : TopologicalSpace ι<VAR>inst✝² : OrderTopology ι<VAR>inst✝¹ : FirstCountableTopology ι<VAR>ℱ : Filtration ι m<VAR>inst✝ : NormedAddCommGroup E<VAR>hτ : IsStoppingTime ℱ τ<VAR>hu : ∀ (n : ι), Memℒp (u n) p μ<VAR>n : ι<VAR>s : Finset ι<VAR>hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s<GOAL>Memℒp ({a | n ≤ τ a}.indicator (u n)) p μ
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>τ σ : Ω → ι<VAR>E : Type u_4<VAR>p : ℝ≥0∞<VAR>u : ι → Ω → E<VAR>inst✝⁴ : LinearOrder ι<VAR>inst✝³ : TopologicalSpace ι<VAR>inst✝² : OrderTopology ι<VAR>inst✝¹ : FirstCountableTopology ι<VAR>ℱ : Filtration ι m<VAR>inst✝ : NormedAddCommGroup E<VAR>hτ : IsStoppingTime ℱ τ<VAR>hu : ∀ (n : ι), Memℒp (u n) p μ<VAR>n : ι<VAR>s : Finset ι<VAR>hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s<GOAL>Memℒp (∑ i ∈ Finset.filter (fun x => x < n) s, {ω | τ ω = i}.indicator (u i)) p μ
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : Preorder γ<VAR>c c' : Chain α<VAR>f : α →o β<VAR>g✝ : β →o γ<VAR>g : α →o β<VAR>h : f ≤ g<VAR>i : ℕ<GOAL>∃ j, (c.map f) i ≤ (c.map g) j
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : Preorder γ<VAR>c c' : Chain α<VAR>f : α →o β<VAR>g✝ : β →o γ<VAR>g : α →o β<VAR>h : f ≤ g<VAR>i : ℕ<GOAL>∃ j, f (c i) ≤ g (c j)
<VAR>M : Type u_1<VAR>inst✝²⁴ : Monoid M<VAR>N : Type u_2<VAR>inst✝²³ : Monoid N<VAR>P : Type u_3<VAR>inst✝²² : Monoid P<VAR>φ : M →* N<VAR>φ' : N →* M<VAR>ψ : N →* P<VAR>χ : M →* P<VAR>A : Type u_4<VAR>inst✝²¹ : AddMonoid A<VAR>inst✝²⁰ : DistribMulAction M A<VAR>B : Type u_5<VAR>inst✝¹⁹ : AddMonoid B<VAR>inst✝¹⁸ : DistribMulAction N B<VAR>B₁ : Type u_6<VAR>inst✝¹⁷ : AddMonoid B₁<VAR>inst✝¹⁶ : DistribMulAction M B₁<VAR>C : Type u_7<VAR>inst✝¹⁵ : AddMonoid C<VAR>inst✝¹⁴ : DistribMulAction P C<VAR>A' : Type u_8<VAR>inst✝¹³ : AddGroup A'<VAR>inst✝¹² : DistribMulAction M A'<VAR>B' : Type u_9<VAR>inst✝¹¹ : AddGroup B'<VAR>inst✝¹⁰ : DistribMulAction N B'<VAR>R : Type u_10<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : MulSemiringAction M R<VAR>R' : Type u_11<VAR>inst✝⁷ : Ring R'<VAR>inst✝⁶ : MulSemiringAction M R'<VAR>S : Type u_12<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : MulSemiringAction N S<VAR>S' : Type u_13<VAR>inst✝³ : Ring S'<VAR>inst✝² : MulSemiringAction N S'<VAR>T : Type u_14<VAR>inst✝¹ : Semiring T<VAR>inst✝ : MulSemiringAction P T<VAR>f : R →ₑ+*[φ] S<VAR>x : R<GOAL>(f.comp (MulSemiringActionHom.id M)) x = f x
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u_1<VAR>Q : β → Prop<VAR>u v : β → Cofix F α<VAR>h : ∀ (x : β), Q x → ∃ a f' f₀ f₁, (u x).dest = MvQPF.abs ⟨a, (P F).appendContents f' f₀⟩ ∧ (v x).dest = MvQPF.abs ⟨a, (P F).appendContents f' f₁⟩ ∧ ∀ (i : (P F).last.B a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'<VAR>x✝¹ : β<VAR>Qx : Q x✝¹<VAR>R : Cofix F α → Cofix F α → Prop := fun w z => ∃ x', Q x' ∧ w = u x' ∧ z = v x'<VAR>x y : Cofix F α<VAR>x✝ : R x y<VAR>x' : β<VAR>Qx' : Q x'<VAR>xeq : x = u x'<VAR>yeq : y = v x'<VAR>a : (P F).A<VAR>f' : (P F).drop.B a ⟹ α<VAR>f₀ f₁ : (P F).last.B a → Cofix F α<VAR>ux'eq : (u x').dest = MvQPF.abs ⟨a, (P F).appendContents f' f₀⟩<VAR>vx'eq : (v x').dest = MvQPF.abs ⟨a, (P F).appendContents f' f₁⟩<VAR>h' : ∀ (i : (P F).last.B a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'<GOAL>LiftR (fun {i} => α.RelLast R) x.dest y.dest