ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>hT_empty : T ∅ = 0<VAR>x : F<VAR>m : MeasurableSpace α<VAR>h✝ : Nonempty α<GOAL>setToSimpleFunc T (const α x) = (T Set.univ) x
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u v w : V<VAR>n : ℕ<VAR>p : G.Walk v w<VAR>h : G.Adj u v<VAR>hn : n ≠ 0<GOAL>(cons h p).getVert n = p.getVert (n - 1)
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u v w : V<VAR>n : ℕ<VAR>p : G.Walk v w<VAR>h : G.Adj u v<VAR>hn : n ≠ 0<VAR>i : ℕ<VAR>hi : i.succ = n<GOAL>(cons h p).getVert n = p.getVert (n - 1)
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u v w : V<VAR>n : ℕ<VAR>p : G.Walk v w<VAR>h : G.Adj u v<VAR>hn : n ≠ 0<VAR>i : ℕ<VAR>hi : i.succ = n<GOAL>(cons h p).getVert i.succ = p.getVert (i.succ - 1)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>inst✝² : IsFilteredOrEmpty D<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)<GOAL>F.Final
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>inst✝² : IsFilteredOrEmpty D<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)<VAR>this : IsFilteredOrEmpty C<GOAL>F.Final
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>inst✝² : IsFilteredOrEmpty D<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)<VAR>this : IsFilteredOrEmpty C<VAR>d : D<VAR>c : C<VAR>s s' : d ⟶ F.obj c<GOAL>∃ c' t, s ≫ F.map t = s' ≫ F.map t
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>inst✝² : IsFilteredOrEmpty D<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)<VAR>this : IsFilteredOrEmpty C<VAR>d : D<VAR>c : C<VAR>s s' : d ⟶ F.obj c<VAR>c₀ : C<VAR>f : IsFiltered.coeq s s' ⟶ F.obj c₀<GOAL>s ≫ F.map (F.preimage (IsFiltered.coeqHom s s' ≫ f)) = s' ≫ F.map (F.preimage (IsFiltered.coeqHom s s' ≫ f))
<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>C : Set (Set α)<VAR>t : Set β<GOAL>⋃₀ C ×ˢ t = ⋃₀ ((fun s => s ×ˢ t) '' C)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>u : δ → δ → Prop<VAR>f : r ↪r s<VAR>g : t ↪r u<GOAL>∀ {a b : α ⊕ γ}, Sum.LiftRel s u ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } a) ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } b) ↔ Sum.LiftRel r t a b
<VAR>B : Type u_1<VAR>F : Type u_2<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : TopologicalSpace F<GOAL>topologicalSpace B F = induced (⇑(TotalSpace.toProd B F)) instTopologicalSpaceProd
<VAR>B : Type u_1<VAR>F : Type u_2<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : TopologicalSpace F<GOAL>topologicalSpace B F = induced (Prod.fst ∘ ⇑(TotalSpace.toProd B F)) inst✝¹ ⊓ induced (Prod.snd ∘ ⇑(TotalSpace.toProd B F)) inst✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>s : ι → Set α<VAR>hs : ∀ (i : ι), NullMeasurableSet (s i) μ<VAR>H : Pairwise (AEDisjoint μ on s)<GOAL>∑' (i : ι), μ (s i) ≤ μ univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>s : ι → Set α<VAR>hs : ∀ (i : ι), NullMeasurableSet (s i) μ<VAR>H : Pairwise (AEDisjoint μ on s)<GOAL>⨆ s_1, ∑ a ∈ s_1, μ (s a) ≤ μ univ
<VAR>x n : ℂ<VAR>hx : x.arg ≠ π<GOAL>x ^ (starRingEnd ℂ) n = (starRingEnd ℂ) ((starRingEnd ℂ) x ^ n)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : _root_.RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>inst✝² : NormedSpace ℝ E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f✝ g✝ : G → E<VAR>f'✝ g'✝ : G →L[ℝ] E<VAR>s✝ : Set G<VAR>x✝ : G<VAR>n : ℕ∞<VAR>f g : ℝ → E<VAR>f' g' : E<VAR>s : Set ℝ<VAR>x : ℝ<VAR>hf : HasDerivWithinAt f f' s x<VAR>hg : HasDerivWithinAt g g' s x<GOAL>HasDerivWithinAt (fun t => ⟪f t, g t⟫_𝕜) (⟪f x, g'⟫_𝕜 + ⟪f', g x⟫_𝕜) s x
<VAR>G : Type u_1<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁷ : SFinite ν<VAR>inst✝⁶ : SFinite μ<VAR>s : Set G<VAR>inst✝⁵ : MeasurableInv G<VAR>inst✝⁴ : μ.IsMulLeftInvariant<VAR>μ' ν' : Measure G<VAR>inst✝³ : SigmaFinite μ'<VAR>inst✝² : SigmaFinite ν'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : ν'.IsMulLeftInvariant<VAR>sm : MeasurableSet s<VAR>h2s : ν' s ≠ 0<VAR>h3s : ν' s ≠ ⊤<VAR>f : G → ℝ≥0∞<VAR>hf : Measurable f<VAR>g : G → ℝ≥0∞ := fun y => f y⁻¹ / ν' ((fun x => x * y⁻¹) ⁻¹' s)<GOAL>μ' s * lintegral ν' g = ∫⁻ (x : G), f x ∂μ'
<VAR>G : Type u_1<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁷ : SFinite ν<VAR>inst✝⁶ : SFinite μ<VAR>s : Set G<VAR>inst✝⁵ : MeasurableInv G<VAR>inst✝⁴ : μ.IsMulLeftInvariant<VAR>μ' ν' : Measure G<VAR>inst✝³ : SigmaFinite μ'<VAR>inst✝² : SigmaFinite ν'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : ν'.IsMulLeftInvariant<VAR>sm : MeasurableSet s<VAR>h2s : ν' s ≠ 0<VAR>h3s : ν' s ≠ ⊤<VAR>f : G → ℝ≥0∞<VAR>hf : Measurable f<VAR>g : G → ℝ≥0∞ := fun y => f y⁻¹ / ν' ((fun x => x * y⁻¹) ⁻¹' s)<VAR>hg : Measurable g<GOAL>μ' s * lintegral ν' g = ∫⁻ (x : G), f x ∂μ'
<VAR>G : Type u_1<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁷ : SFinite ν<VAR>inst✝⁶ : SFinite μ<VAR>s : Set G<VAR>inst✝⁵ : MeasurableInv G<VAR>inst✝⁴ : μ.IsMulLeftInvariant<VAR>μ' ν' : Measure G<VAR>inst✝³ : SigmaFinite μ'<VAR>inst✝² : SigmaFinite ν'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : ν'.IsMulLeftInvariant<VAR>sm : MeasurableSet s<VAR>h2s : ν' s ≠ 0<VAR>h3s : ν' s ≠ ⊤<VAR>f : G → ℝ≥0∞<VAR>hf : Measurable f<VAR>g : G → ℝ≥0∞ := fun y => f y⁻¹ / ν' ((fun x => x * y⁻¹) ⁻¹' s)<VAR>hg : Measurable g<GOAL>∫⁻ (x : G), ν' ((fun x_1 => x_1 * x) ⁻¹' s) * (f x / ν' ((fun x_1 => x_1 * x) ⁻¹' s)) ∂μ' = ∫⁻ (x : G), f x ∂μ'
<VAR>G : Type u_1<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁷ : SFinite ν<VAR>inst✝⁶ : SFinite μ<VAR>s : Set G<VAR>inst✝⁵ : MeasurableInv G<VAR>inst✝⁴ : μ.IsMulLeftInvariant<VAR>μ' ν' : Measure G<VAR>inst✝³ : SigmaFinite μ'<VAR>inst✝² : SigmaFinite ν'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : ν'.IsMulLeftInvariant<VAR>sm : MeasurableSet s<VAR>h2s : ν' s ≠ 0<VAR>h3s : ν' s ≠ ⊤<VAR>f : G → ℝ≥0∞<VAR>hf : Measurable f<VAR>g : G → ℝ≥0∞ := fun y => f y⁻¹ / ν' ((fun x => x * y⁻¹) ⁻¹' s)<VAR>hg : Measurable g<GOAL>(fun x => ν' ((fun x_1 => x_1 * x) ⁻¹' s) * (f x / ν' ((fun x_1 => x_1 * x) ⁻¹' s))) =ᶠ[ae μ'] f
<VAR>G : Type u_1<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁷ : SFinite ν<VAR>inst✝⁶ : SFinite μ<VAR>s : Set G<VAR>inst✝⁵ : MeasurableInv G<VAR>inst✝⁴ : μ.IsMulLeftInvariant<VAR>μ' ν' : Measure G<VAR>inst✝³ : SigmaFinite μ'<VAR>inst✝² : SigmaFinite ν'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : ν'.IsMulLeftInvariant<VAR>sm : MeasurableSet s<VAR>h2s : ν' s ≠ 0<VAR>h3s : ν' s ≠ ⊤<VAR>f : G → ℝ≥0∞<VAR>hf : Measurable f<VAR>g : G → ℝ≥0∞ := fun y => f y⁻¹ / ν' ((fun x => x * y⁻¹) ⁻¹' s)<VAR>hg : Measurable g<VAR>x : G<VAR>hx : ν' ((fun y => y * x) ⁻¹' s) < ⊤<GOAL>(fun x => ν' ((fun x_1 => x_1 * x) ⁻¹' s) * (f x / ν' ((fun x_1 => x_1 * x) ⁻¹' s))) x = f x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>h : IsDedekindDomainInv A<VAR>P : Ideal A<VAR>P_ne : P ≠ ⊥<VAR>hP : P.IsPrime<GOAL>P.IsMaximal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>h : IsDedekindDomainInv A<VAR>P : Ideal A<VAR>P_ne : P ≠ ⊥<VAR>hP : P.IsPrime<VAR>M : Ideal A<VAR>hM : P < M<GOAL>M = ⊤
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>h : IsDedekindDomainInv A<VAR>P : Ideal A<VAR>P_ne : P ≠ ⊥<VAR>hP : P.IsPrime<VAR>M : Ideal A<VAR>hM : P < M<VAR>P'_ne : ↑P ≠ 0<GOAL>M = ⊤
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>h : IsDedekindDomainInv A<VAR>P : Ideal A<VAR>P_ne : P ≠ ⊥<VAR>hP : P.IsPrime<VAR>M : Ideal A<VAR>hM : P < M<VAR>P'_ne : ↑P ≠ 0<VAR>M'_ne : ↑M ≠ 0<GOAL>M = ⊤
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>h : IsDedekindDomainInv A<VAR>P : Ideal A<VAR>P_ne : P ≠ ⊥<VAR>hP : P.IsPrime<VAR>M : Ideal A<VAR>hM : P < M<VAR>P'_ne : ↑P ≠ 0<VAR>M'_ne : ↑M ≠ 0<VAR>x : FractionRing A<VAR>hx : x ∈ (fun a => ↑a) ((↑M)⁻¹ * ↑P)<GOAL>x ∈ (fun a => ↑a) ↑P
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>h : IsDedekindDomainInv A<VAR>P : Ideal A<VAR>P_ne : P ≠ ⊥<VAR>hP : P.IsPrime<VAR>M : Ideal A<VAR>hM : P < M<VAR>P'_ne : ↑P ≠ 0<VAR>M'_ne : ↑M ≠ 0<VAR>x : FractionRing A<VAR>hx : x ∈ (fun a => ↑a) ((↑M)⁻¹ * ↑P)<VAR>le_one : (↑M)⁻¹ * ↑P ≤ 1<GOAL>x ∈ (fun a => ↑a) ↑P
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>h : IsDedekindDomainInv A<VAR>P : Ideal A<VAR>P_ne : P ≠ ⊥<VAR>hP : P.IsPrime<VAR>M : Ideal A<VAR>hM : P < M<VAR>P'_ne : ↑P ≠ 0<VAR>M'_ne : ↑M ≠ 0<VAR>le_one : (↑M)⁻¹ * ↑P ≤ 1<VAR>y : A<VAR>_hy : y ∈ ⊤<VAR>hx : (algebraMap A (FractionRing A)) y ∈ (fun a => ↑a) ((↑M)⁻¹ * ↑P)<GOAL>(algebraMap A (FractionRing A)) y ∈ (fun a => ↑a) ↑P
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>h : IsDedekindDomainInv A<VAR>P : Ideal A<VAR>P_ne : P ≠ ⊥<VAR>hP : P.IsPrime<VAR>M : Ideal A<VAR>hM : P < M<VAR>P'_ne : ↑P ≠ 0<VAR>M'_ne : ↑M ≠ 0<VAR>le_one : (↑M)⁻¹ * ↑P ≤ 1<VAR>y : A<VAR>_hy : y ∈ ⊤<VAR>hx : (algebraMap A (FractionRing A)) y ∈ (fun a => ↑a) ((↑M)⁻¹ * ↑P)<VAR>z : A<VAR>hzM : z ∈ M<VAR>hzp : z ∉ P<GOAL>(algebraMap A (FractionRing A)) y ∈ (fun a => ↑a) ↑P
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>h : IsDedekindDomainInv A<VAR>P : Ideal A<VAR>P_ne : P ≠ ⊥<VAR>hP : P.IsPrime<VAR>M : Ideal A<VAR>hM : P < M<VAR>P'_ne : ↑P ≠ 0<VAR>M'_ne : ↑M ≠ 0<VAR>le_one : (↑M)⁻¹ * ↑P ≤ 1<VAR>y : A<VAR>_hy : y ∈ ⊤<VAR>hx : (algebraMap A (FractionRing A)) y ∈ (fun a => ↑a) ((↑M)⁻¹ * ↑P)<VAR>z : A<VAR>hzM : z ∈ M<VAR>hzp : z ∉ P<VAR>zy_mem : (algebraMap A (FractionRing A)) z * (algebraMap A (FractionRing A)) y ∈ ↑M * ((↑M)⁻¹ * ↑P)<GOAL>(algebraMap A (FractionRing A)) y ∈ (fun a => ↑a) ↑P
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>h : IsDedekindDomainInv A<VAR>P : Ideal A<VAR>P_ne : P ≠ ⊥<VAR>hP : P.IsPrime<VAR>M : Ideal A<VAR>hM : P < M<VAR>P'_ne : ↑P ≠ 0<VAR>M'_ne : ↑M ≠ 0<VAR>le_one : (↑M)⁻¹ * ↑P ≤ 1<VAR>y : A<VAR>_hy : y ∈ ⊤<VAR>hx : (algebraMap A (FractionRing A)) y ∈ (fun a => ↑a) ((↑M)⁻¹ * ↑P)<VAR>z : A<VAR>hzM : z ∈ M<VAR>hzp : z ∉ P<VAR>zy_mem : (algebraMap A (FractionRing A)) (z * y) ∈ ↑P<GOAL>(algebraMap A (FractionRing A)) y ∈ (fun a => ↑a) ↑P
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>h : IsDedekindDomainInv A<VAR>P : Ideal A<VAR>P_ne : P ≠ ⊥<VAR>hP : P.IsPrime<VAR>M : Ideal A<VAR>hM : P < M<VAR>P'_ne : ↑P ≠ 0<VAR>M'_ne : ↑M ≠ 0<VAR>le_one : (↑M)⁻¹ * ↑P ≤ 1<VAR>y : A<VAR>_hy : y ∈ ⊤<VAR>hx : (algebraMap A (FractionRing A)) y ∈ (fun a => ↑a) ((↑M)⁻¹ * ↑P)<VAR>z : A<VAR>hzM : z ∈ M<VAR>hzp : z ∉ P<VAR>zy_mem : (algebraMap A (FractionRing A)) (z * y) ∈ ↑P<VAR>zy : A<VAR>hzy : zy ∈ P<VAR>zy_eq : (algebraMap A (FractionRing A)) zy = (algebraMap A (FractionRing A)) (z * y)<GOAL>(algebraMap A (FractionRing A)) y ∈ (fun a => ↑a) ↑P
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>h : IsDedekindDomainInv A<VAR>P : Ideal A<VAR>P_ne : P ≠ ⊥<VAR>hP : P.IsPrime<VAR>M : Ideal A<VAR>hM : P < M<VAR>P'_ne : ↑P ≠ 0<VAR>M'_ne : ↑M ≠ 0<VAR>le_one : (↑M)⁻¹ * ↑P ≤ 1<VAR>y : A<VAR>_hy : y ∈ ⊤<VAR>hx : (algebraMap A (FractionRing A)) y ∈ (fun a => ↑a) ((↑M)⁻¹ * ↑P)<VAR>z : A<VAR>hzM : z ∈ M<VAR>hzp : z ∉ P<VAR>zy_mem : (algebraMap A (FractionRing A)) (z * y) ∈ ↑P<VAR>zy : A<VAR>hzy : z * y ∈ P<VAR>zy_eq : (algebraMap A (FractionRing A)) zy = (algebraMap A (FractionRing A)) (z * y)<GOAL>(algebraMap A (FractionRing A)) y ∈ (fun a => ↑a) ↑P
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : SeparableSpace R<VAR>inst✝¹ : ContinuousAdd M<VAR>inst✝ : ContinuousSMul R M<VAR>s : Set M<VAR>hs : IsSeparable s<GOAL>IsSeparable ↑(Submodule.span R s)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : SeparableSpace R<VAR>inst✝¹ : ContinuousAdd M<VAR>inst✝ : ContinuousSMul R M<VAR>s : Set M<VAR>hs : IsSeparable s<GOAL>IsSeparable (⋃ n, (fun f => ∑ i : Fin n, (f i).1 • (f i).2) '' {f | ∀ (i : Fin n), (f i).2 ∈ s})
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : SeparableSpace R<VAR>inst✝¹ : ContinuousAdd M<VAR>inst✝ : ContinuousSMul R M<VAR>s : Set M<VAR>hs : IsSeparable s<VAR>n : ℕ<GOAL>IsSeparable {f | ∀ (i : Fin n), (f i).2 ∈ s}
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : SeparableSpace R<VAR>inst✝¹ : ContinuousAdd M<VAR>inst✝ : ContinuousSMul R M<VAR>s : Set M<VAR>hs : IsSeparable s<VAR>n : ℕ<GOAL>Continuous fun f => ∑ i : Fin n, (f i).1 • (f i).2
<VAR>α : Type u_1<VAR>m n✝ a n : ℕ<VAR>hn : Odd n<VAR>hm : 2 ∣ n<GOAL>False
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>S : Set (Set α)<VAR>hc : S.Countable<VAR>hs : ⋃₀ S = univ<GOAL>⋃ i ∈ S, i = univ
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>γ : RightHomologyMapData φ h₁ h₂<VAR>inst✝¹ : S₁.HasRightHomology<VAR>inst✝ : S₂.HasRightHomology<GOAL>rightHomologyMap φ = rightHomologyMap' (𝟙 S₁) S₁.rightHomologyData h₁ ≫ γ.φH ≫ rightHomologyMap' (𝟙 S₂) h₂ S₂.rightHomologyData
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>γ : RightHomologyMapData φ h₁ h₂<VAR>inst✝¹ : S₁.HasRightHomology<VAR>inst✝ : S₂.HasRightHomology<GOAL>rightHomologyMap φ = rightHomologyMap' φ S₁.rightHomologyData S₂.rightHomologyData
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z✝ : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>h : dist x y ≤ ε₂ - ε₁<VAR>z : α<VAR>zx : z ∈ ball x ε₁<GOAL>z ∈ ball y ε₂
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z✝ : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>h : dist x y ≤ ε₂ - ε₁<VAR>z : α<VAR>zx : z ∈ ball x ε₁<GOAL>z ∈ ball y (ε₁ + (ε₂ - ε₁))
<VAR>α : Type w<VAR>inst✝ : Finite α<VAR>X : α → LightProfinite<VAR>a : α<VAR>x y : (forget LightProfinite).obj (X a)<VAR>hxy : (ι X a) x = (ι X a) y<GOAL>x = y
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>m n✝ : ℕ<VAR>i : σ<VAR>n : ℕ<GOAL>(X i ^ n).IsHomogeneous n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁✝ s₂✝ t s₁ s₂ s₃ : Set α<VAR>h12 : s₁ ⊆ s₂<VAR>h23 : s₂ ⊆ s₃<VAR>h_nulldiff : μ (s₃ \ s₁) = 0<GOAL>μ s₁ = μ s₂ ∧ μ s₂ = μ s₃
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁✝ s₂✝ t s₁ s₂ s₃ : Set α<VAR>h12 : s₁ ⊆ s₂<VAR>h23 : s₂ ⊆ s₃<VAR>h_nulldiff : μ (s₃ \ s₁) = 0<VAR>le12 : μ s₁ ≤ μ s₂<GOAL>μ s₁ = μ s₂ ∧ μ s₂ = μ s₃
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁✝ s₂✝ t s₁ s₂ s₃ : Set α<VAR>h12 : s₁ ⊆ s₂<VAR>h23 : s₂ ⊆ s₃<VAR>h_nulldiff : μ (s₃ \ s₁) = 0<VAR>le12 : μ s₁ ≤ μ s₂<VAR>le23 : μ s₂ ≤ μ s₃<GOAL>μ s₁ = μ s₂ ∧ μ s₂ = μ s₃
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁✝ s₂✝ t s₁ s₂ s₃ : Set α<VAR>h12 : s₁ ⊆ s₂<VAR>h23 : s₂ ⊆ s₃<VAR>h_nulldiff : μ (s₃ \ s₁) = 0<VAR>le12 : μ s₁ ≤ μ s₂<VAR>le23 : μ s₂ ≤ μ s₃<VAR>key : μ s₃ ≤ μ s₁<GOAL>μ s₁ = μ s₂ ∧ μ s₂ = μ s₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₀ p₁✝ p₂✝ p₁ p₂ p₃ : P<GOAL>∠ p₁ p₂ p₃ = 0 ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ p₂ p₃ p₁
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₀ p₁✝ p₂✝ p₁ p₂ p₃ : P<GOAL>p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ p₂ p₃ p₁
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₀ p₁✝ p₂✝ p₁ p₂ p₃ : P<VAR>hp₁p₂ : ¬p₁ = p₂<VAR>hp₁p₃ : ¬p₁ = p₃<VAR>hp₃p₂ : ¬p₃ = p₂<GOAL>p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ p₂ p₃ p₁
<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>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : Fintype κ<VAR>inst✝ : CommMonoid α<VAR>s : Finset ι<VAR>f : ι → α<VAR>h : ∀ (i : ι), f i ≠ 1 → i ∈ s<GOAL>∀ x ∈ univ, x ∉ s → f x = 1
<VAR>p : ℚ[X]<VAR>hp : ¬p = 0<GOAL>(p.rootSet ℂ).toFinset.card = (p.rootSet ℝ).toFinset.card + ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card
<VAR>p : ℚ[X]<VAR>hp : ¬p = 0<VAR>inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)<GOAL>(p.rootSet ℂ).toFinset.card = (p.rootSet ℝ).toFinset.card + ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card
<VAR>p : ℚ[X]<VAR>hp : ¬p = 0<VAR>inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)<GOAL>(p.rootSet ℂ).toFinset.card = (Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (p.rootSet ℝ).toFinset).card + (Finset.image (fun a => ↑a) ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support).card
<VAR>p : ℚ[X]<VAR>hp : ¬p = 0<VAR>inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)<VAR>a : Finset ℂ := (p.rootSet ℂ).toFinset<VAR>b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (p.rootSet ℝ).toFinset<VAR>c : Finset ℂ := Finset.image (fun a => ↑a) ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support<GOAL>a.card = b.card + c.card
<VAR>p : ℚ[X]<VAR>hp : ¬p = 0<VAR>inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)<VAR>a : Finset ℂ := (p.rootSet ℂ).toFinset<VAR>b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (p.rootSet ℝ).toFinset<VAR>c : Finset ℂ := Finset.image (fun a => ↑a) ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support<VAR>ha : ∀ (z : ℂ), z ∈ a ↔ (aeval z) p = 0<GOAL>a.card = b.card + c.card
<VAR>p : ℚ[X]<VAR>hp : ¬p = 0<VAR>inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)<VAR>a : Finset ℂ := (p.rootSet ℂ).toFinset<VAR>b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (p.rootSet ℝ).toFinset<VAR>c : Finset ℂ := Finset.image (fun a => ↑a) ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support<VAR>ha : ∀ (z : ℂ), z ∈ a ↔ (aeval z) p = 0<VAR>hb : ∀ (z : ℂ), z ∈ b ↔ (aeval z) p = 0 ∧ z.im = 0<GOAL>a.card = b.card + c.card
<VAR>p : ℚ[X]<VAR>hp : ¬p = 0<VAR>inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)<VAR>a : Finset ℂ := (p.rootSet ℂ).toFinset<VAR>b : Finset ℂ := Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (p.rootSet ℝ).toFinset<VAR>c : Finset ℂ := Finset.image (fun a => ↑a) ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support<VAR>ha : ∀ (z : ℂ), z ∈ a ↔ (aeval z) p = 0<VAR>hb : ∀ (z : ℂ), z ∈ b ↔ (aeval z) p = 0 ∧ z.im = 0<VAR>hc0 : ∀ (w : ↑(p.rootSet ℂ)), ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))) w = w ↔ (↑w).im = 0<GOAL>a.card = b.card + c.card
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIocDiv hp a (b + p) = toIocDiv hp a b + 1
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M✝ M N : Comon_ C<VAR>f : M.X ≅ N.X<VAR>f_counit : autoParam (f.hom ≫ N.counit = M.counit) _auto✝<VAR>f_comul : autoParam (f.hom ≫ N.comul = M.comul ≫ (f.hom ⊗ f.hom)) _auto✝<GOAL>f.inv ≫ M.comul = N.comul ≫ (f.inv ⊗ f.inv)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M✝ M N : Comon_ C<VAR>f : M.X ≅ N.X<VAR>f_counit : autoParam (f.hom ≫ N.counit = M.counit) _auto✝<VAR>f_comul : autoParam (f.hom ≫ N.comul = M.comul ≫ (f.hom ⊗ f.hom)) _auto✝<GOAL>f.hom ≫ f.inv ≫ M.comul = f.hom ≫ N.comul ≫ (f.inv ⊗ f.inv)