ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>hν : IsFiniteKernel ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>u : Set γ<VAR>hu : u ∈ countablePartition γ n<VAR>this : IsFiniteKernel κ<VAR>hu_meas : MeasurableSet u<GOAL>∫ (x : γ) in u, κ.densityProcess ν n a x s ∂ν a = ((κ a) (u ×ˢ s)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>hν : IsFiniteKernel ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>u : Set γ<VAR>hu : u ∈ countablePartition γ n<VAR>this : IsFiniteKernel κ<VAR>hu_meas : MeasurableSet u<GOAL>∫ (x : γ) in u, ((κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x)).toReal ∂ν a = ((κ a) (u ×ˢ s)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>hν : IsFiniteKernel ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>u : Set γ<VAR>hu : u ∈ countablePartition γ n<VAR>this : IsFiniteKernel κ<VAR>hu_meas : MeasurableSet u<GOAL>(∫⁻ (a_1 : γ) in u, (κ a) (countablePartitionSet n a_1 ×ˢ s) / (ν a) (countablePartitionSet n a_1) ∂ν a).toReal = ((κ a) (u ×ˢ s)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>hν : IsFiniteKernel ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>u : Set γ<VAR>hu : u ∈ countablePartition γ n<VAR>this : IsFiniteKernel κ<VAR>hu_meas : MeasurableSet u<GOAL>AEMeasurable (fun x => (κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x)) ((ν a).restrict u)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>hν : IsFiniteKernel ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>u : Set γ<VAR>hu : u ∈ countablePartition γ n<VAR>this : IsFiniteKernel κ<VAR>hu_meas : MeasurableSet u<GOAL>∀ᵐ (x : γ) ∂(ν a).restrict u, (κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x) < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>hν : IsFiniteKernel ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>u : Set γ<VAR>hu : u ∈ countablePartition γ n<VAR>this : IsFiniteKernel κ<VAR>hu_meas : MeasurableSet u<GOAL>∫⁻ (a_1 : γ) in u, (κ a) (countablePartitionSet n a_1 ×ˢ s) / (ν a) (countablePartitionSet n a_1) ∂ν a = (κ a) (u ×ˢ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>hν : IsFiniteKernel ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>u : Set γ<VAR>hu : u ∈ countablePartition γ n<VAR>this✝ : IsFiniteKernel κ<VAR>hu_meas : MeasurableSet u<VAR>this : ∫⁻ (x : γ) in u, (κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x) ∂ν a = ∫⁻ (x : γ) in u, (κ a) (u ×ˢ s) / (ν a) u ∂ν a<GOAL>∫⁻ (a_1 : γ) in u, (κ a) (countablePartitionSet n a_1 ×ˢ s) / (ν a) (countablePartitionSet n a_1) ∂ν a = (κ a) (u ×ˢ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>hν : IsFiniteKernel ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>u : Set γ<VAR>hu : u ∈ countablePartition γ n<VAR>this✝ : IsFiniteKernel κ<VAR>hu_meas : MeasurableSet u<VAR>this : ∫⁻ (x : γ) in u, (κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x) ∂ν a = ∫⁻ (x : γ) in u, (κ a) (u ×ˢ s) / (ν a) u ∂ν a<GOAL>∫⁻ (x : γ) in u, (κ a) (u ×ˢ s) / (ν a) u ∂ν a = (κ a) (u ×ˢ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>hν : IsFiniteKernel ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>u : Set γ<VAR>hu : u ∈ countablePartition γ n<VAR>this✝ : IsFiniteKernel κ<VAR>hu_meas : MeasurableSet u<VAR>this : ∫⁻ (x : γ) in u, (κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x) ∂ν a = ∫⁻ (x : γ) in u, (κ a) (u ×ˢ s) / (ν a) u ∂ν a<GOAL>(κ a) (u ×ˢ s) / (ν a) u * (ν a) u = (κ a) (u ×ˢ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>hν : IsFiniteKernel ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>u : Set γ<VAR>hu : u ∈ countablePartition γ n<VAR>this✝ : IsFiniteKernel κ<VAR>hu_meas : MeasurableSet u<VAR>this : ∫⁻ (x : γ) in u, (κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x) ∂ν a = ∫⁻ (x : γ) in u, (κ a) (u ×ˢ s) / (ν a) u ∂ν a<VAR>h0 : ¬(ν a) u = 0<GOAL>(κ a) (u ×ˢ s) / (ν a) u * (ν a) u = (κ a) (u ×ˢ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>hν : IsFiniteKernel ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>u : Set γ<VAR>hu : u ∈ countablePartition γ n<VAR>this✝ : IsFiniteKernel κ<VAR>hu_meas : MeasurableSet u<VAR>this : ∫⁻ (x : γ) in u, (κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x) ∂ν a = ∫⁻ (x : γ) in u, (κ a) (u ×ˢ s) / (ν a) u ∂ν a<VAR>h0 : ¬(ν a) u = 0<GOAL>(ν a) u ≠ ⊤
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : CommRing F<VAR>inst✝⁴ : StrongRankCondition F<VAR>inst✝³ : Ring E<VAR>inst✝² : Algebra F E<VAR>S : Subalgebra F E<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : Module.Free F ↥S<GOAL>Module.rank F ↥S = 1 ↔ S = ⊥
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : CommRing F<VAR>inst✝⁴ : StrongRankCondition F<VAR>inst✝³ : Ring E<VAR>inst✝² : Algebra F E<VAR>S : Subalgebra F E<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : Module.Free F ↥S<GOAL>S = ⊥ → Module.rank F ↥S = 1
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : CommRing F<VAR>inst✝⁴ : StrongRankCondition F<VAR>inst✝³ : Ring E<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : Module.Free F ↥⊥<GOAL>Module.rank F ↥⊥ = 1
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : CommRing F<VAR>inst✝⁴ : StrongRankCondition F<VAR>inst✝³ : Ring E<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : Module.Free F ↥⊥<VAR>κ : Type u_2<VAR>b : Basis κ F ↥⊥<GOAL>Module.rank F ↥⊥ = 1
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : CommRing F<VAR>inst✝⁴ : StrongRankCondition F<VAR>inst✝³ : Ring E<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : Module.Free F ↥⊥<VAR>κ : Type u_2<VAR>b : Basis κ F ↥⊥<GOAL>Module.rank F ↥⊥ ≤ 1
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : CommRing F<VAR>inst✝⁴ : StrongRankCondition F<VAR>inst✝³ : Ring E<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : Module.Free F ↥⊥<VAR>κ : Type u_2<VAR>b : Basis κ F ↥⊥<GOAL>1 ≤ Module.rank F ↥⊥
<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>G : D ⥤ C<VAR>adj : CoreHomEquiv F G<VAR>X' X : C<VAR>Y Y' : D<VAR>f : X ⟶ G.obj Y<VAR>g : Y ⟶ Y'<GOAL>(adj.homEquiv X Y').symm (f ≫ G.map g) = (adj.homEquiv X Y).symm f ≫ g
<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>f : E → F<VAR>K✝ K : Set (E →L[𝕜] F)<VAR>r s ε : ℝ<GOAL>IsOpen (B f K r s ε)
<VAR>a : ℕ<GOAL>jacobiSymNat a 0 = 1
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>R₀ R : Cᵒᵖ ⥤ RingCat<VAR>α : R₀ ⟶ R<VAR>inst✝¹ : Presheaf.IsLocallyInjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : Cᵒᵖ ⥤ AddCommGrp<VAR>φ : M₀.presheaf ⟶ A<VAR>inst✝ : Presheaf.IsLocallyInjective J φ<VAR>hA : Presheaf.IsSeparated J A<VAR>X : C<VAR>r : ↑(R.obj (Opposite.op X))<VAR>m : ↑(A.obj (Opposite.op X))<VAR>P : Presieve X<VAR>r₀✝ : FamilyOfElements (R₀ ⋙ forget RingCat) P<VAR>m₀✝ : FamilyOfElements (M₀.presheaf ⋙ forget AddCommGrp) P<VAR>hr₀✝ : (r₀✝.map (whiskerRight α (forget RingCat))).IsAmalgamation r<VAR>hm₀✝ : (m₀✝.map (whiskerRight φ (forget AddCommGrp))).IsAmalgamation m<VAR>Y Z : C<VAR>f : Y ⟶ X<VAR>g : Z ⟶ Y<VAR>r₀ : ↑(R₀.obj (Opposite.op Y))<VAR>r₀' : ↑(R₀.obj (Opposite.op Z))<VAR>m₀ : ↑(M₀.presheaf.obj (Opposite.op Y))<VAR>m₀' : ↑(M₀.presheaf.obj (Opposite.op Z))<VAR>hr₀ : (α.app (Opposite.op Y)) r₀ = (R.map f.op) r<VAR>hr₀' : (α.app (Opposite.op Z)) r₀' = (R.map (f.op ≫ g.op)) r<VAR>hm₀ : (φ.app (Opposite.op Y)) m₀ = (A.map f.op) m<VAR>hm₀' : (φ.app (Opposite.op Z)) m₀' = (A.map (f.op ≫ g.op)) m<GOAL>(φ.app (Opposite.op Z)) ((M₀.presheaf.map g.op) (r₀ • m₀)) = (φ.app (Opposite.op Z)) (r₀' • m₀')
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>R₀ R : Cᵒᵖ ⥤ RingCat<VAR>α : R₀ ⟶ R<VAR>inst✝¹ : Presheaf.IsLocallyInjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : Cᵒᵖ ⥤ AddCommGrp<VAR>φ : M₀.presheaf ⟶ A<VAR>inst✝ : Presheaf.IsLocallyInjective J φ<VAR>hA : Presheaf.IsSeparated J A<VAR>X : C<VAR>r : ↑(R.obj (Opposite.op X))<VAR>m : ↑(A.obj (Opposite.op X))<VAR>P : Presieve X<VAR>r₀✝ : FamilyOfElements (R₀ ⋙ forget RingCat) P<VAR>m₀✝ : FamilyOfElements (M₀.presheaf ⋙ forget AddCommGrp) P<VAR>hr₀✝ : (r₀✝.map (whiskerRight α (forget RingCat))).IsAmalgamation r<VAR>hm₀✝ : (m₀✝.map (whiskerRight φ (forget AddCommGrp))).IsAmalgamation m<VAR>Y Z : C<VAR>f : Y ⟶ X<VAR>g : Z ⟶ Y<VAR>r₀ : ↑(R₀.obj (Opposite.op Y))<VAR>r₀' : ↑(R₀.obj (Opposite.op Z))<VAR>m₀ : ↑(M₀.presheaf.obj (Opposite.op Y))<VAR>m₀' : ↑(M₀.presheaf.obj (Opposite.op Z))<VAR>hr₀ : (α.app (Opposite.op Y)) r₀ = (R.map f.op) r<VAR>hr₀' : (α.app (Opposite.op Z)) r₀' = (R.map (f.op ≫ g.op)) r<VAR>hm₀ : (φ.app (Opposite.op Y)) m₀ = (A.map f.op) m<VAR>hm₀' : (φ.app (Opposite.op Z)) m₀' = (A.map (f.op ≫ g.op)) m<GOAL>(α.app (Opposite.op Z)) ((R₀.map g.op) r₀) = (α.app (Opposite.op Z)) r₀'
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>R₀ R : Cᵒᵖ ⥤ RingCat<VAR>α : R₀ ⟶ R<VAR>inst✝¹ : Presheaf.IsLocallyInjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : Cᵒᵖ ⥤ AddCommGrp<VAR>φ : M₀.presheaf ⟶ A<VAR>inst✝ : Presheaf.IsLocallyInjective J φ<VAR>hA : Presheaf.IsSeparated J A<VAR>X : C<VAR>r : ↑(R.obj (Opposite.op X))<VAR>m : ↑(A.obj (Opposite.op X))<VAR>P : Presieve X<VAR>r₀✝ : FamilyOfElements (R₀ ⋙ forget RingCat) P<VAR>m₀✝ : FamilyOfElements (M₀.presheaf ⋙ forget AddCommGrp) P<VAR>hr₀✝ : (r₀✝.map (whiskerRight α (forget RingCat))).IsAmalgamation r<VAR>hm₀✝ : (m₀✝.map (whiskerRight φ (forget AddCommGrp))).IsAmalgamation m<VAR>Y Z : C<VAR>f : Y ⟶ X<VAR>g : Z ⟶ Y<VAR>r₀ : ↑(R₀.obj (Opposite.op Y))<VAR>r₀' : ↑(R₀.obj (Opposite.op Z))<VAR>m₀ : ↑(M₀.presheaf.obj (Opposite.op Y))<VAR>m₀' : ↑(M₀.presheaf.obj (Opposite.op Z))<VAR>hr₀ : (α.app (Opposite.op Y)) r₀ = (R.map f.op) r<VAR>hr₀' : (α.app (Opposite.op Z)) r₀' = (R.map (f.op ≫ g.op)) r<VAR>hm₀ : (φ.app (Opposite.op Y)) m₀ = (A.map f.op) m<VAR>hm₀' : (φ.app (Opposite.op Z)) m₀' = (A.map (f.op ≫ g.op)) m<GOAL>(φ.app (Opposite.op Z)) ((M₀.presheaf.map g.op) m₀) = (φ.app (Opposite.op Z)) m₀'
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x : 𝕎 R<GOAL>truncateFun n (-x) = -truncateFun n x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r✝ r : α → α → Prop<VAR>inst✝¹ : IsRefl α r<VAR>inst✝ : IsTrans α r<VAR>s : Set α<VAR>h : s.PartiallyWellOrderedOn r<GOAL>{l | ∀ x ∈ l, x ∈ s}.PartiallyWellOrderedOn (List.SublistForall₂ r)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r✝ r : α → α → Prop<VAR>inst✝¹ : IsRefl α r<VAR>inst✝ : IsTrans α r<VAR>s : Set α<VAR>h : s.PartiallyWellOrderedOn r<VAR>h✝ : IsEmpty α<GOAL>{l | ∀ x ∈ l, x ∈ s}.PartiallyWellOrderedOn (List.SublistForall₂ r)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r✝ r : α → α → Prop<VAR>inst✝¹ : IsRefl α r<VAR>inst✝ : IsTrans α r<VAR>s : Set α<VAR>h : s.PartiallyWellOrderedOn r<VAR>h✝ : Nonempty α<GOAL>{l | ∀ x ∈ l, x ∈ s}.PartiallyWellOrderedOn (List.SublistForall₂ r)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r✝ r : α → α → Prop<VAR>inst✝¹ : IsRefl α r<VAR>inst✝ : IsTrans α r<VAR>s : Set α<VAR>h : s.PartiallyWellOrderedOn r<VAR>h✝ : Nonempty α<VAR>inhabited_h : Inhabited α<GOAL>{l | ∀ x ∈ l, x ∈ s}.PartiallyWellOrderedOn (List.SublistForall₂ r)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r✝ r : α → α → Prop<VAR>inst✝¹ : IsRefl α r<VAR>inst✝ : IsTrans α r<VAR>s : Set α<VAR>h : s.PartiallyWellOrderedOn r<VAR>h✝ : Nonempty α<VAR>inhabited_h : Inhabited α<GOAL>¬∃ f, IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f ∧ ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r✝ r : α → α → Prop<VAR>inst✝¹ : IsRefl α r<VAR>inst✝ : IsTrans α r<VAR>s : Set α<VAR>h : s.PartiallyWellOrderedOn r<VAR>h✝ : Nonempty α<VAR>inhabited_h : Inhabited α<VAR>f : ℕ → List α<VAR>hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f<VAR>hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r✝ r : α → α → Prop<VAR>inst✝¹ : IsRefl α r<VAR>inst✝ : IsTrans α r<VAR>s : Set α<VAR>h : s.PartiallyWellOrderedOn r<VAR>h✝ : Nonempty α<VAR>inhabited_h : Inhabited α<VAR>f : ℕ → List α<VAR>hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f<VAR>hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f<VAR>hnil : ∀ (n : ℕ), f n ≠ []<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r✝ r : α → α → Prop<VAR>inst✝¹ : IsRefl α r<VAR>inst✝ : IsTrans α r<VAR>s : Set α<VAR>h : s.PartiallyWellOrderedOn r<VAR>h✝ : Nonempty α<VAR>inhabited_h : Inhabited α<VAR>f : ℕ → List α<VAR>hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f<VAR>hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f<VAR>hnil : ∀ (n : ℕ), f n ≠ []<VAR>this : ∀ (n : ℕ), (f n).headI ∈ s<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r✝ r : α → α → Prop<VAR>inst✝¹ : IsRefl α r<VAR>inst✝ : IsTrans α r<VAR>s : Set α<VAR>h : s.PartiallyWellOrderedOn r<VAR>h✝ : Nonempty α<VAR>inhabited_h : Inhabited α<VAR>f : ℕ → List α<VAR>hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f<VAR>hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f<VAR>hnil : ∀ (n : ℕ), f n ≠ []<VAR>this : ∀ (n : ℕ), (f n).headI ∈ s<VAR>g : ℕ ↪o ℕ<VAR>hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).headI (f (g n)).headI<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r✝ r : α → α → Prop<VAR>inst✝¹ : IsRefl α r<VAR>inst✝ : IsTrans α r<VAR>s : Set α<VAR>h : s.PartiallyWellOrderedOn r<VAR>h✝ : Nonempty α<VAR>inhabited_h : Inhabited α<VAR>f : ℕ → List α<VAR>hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f<VAR>hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f<VAR>hnil : ∀ (n : ℕ), f n ≠ []<VAR>this : ∀ (n : ℕ), (f n).headI ∈ s<VAR>g : ℕ ↪o ℕ<VAR>hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).headI (f (g n)).headI<VAR>hf' : ¬IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} fun n => if n < g 0 then f n else (f (g (n - g 0))).tail<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r✝ r : α → α → Prop<VAR>inst✝¹ : IsRefl α r<VAR>inst✝ : IsTrans α r<VAR>s : Set α<VAR>h : s.PartiallyWellOrderedOn r<VAR>h✝ : Nonempty α<VAR>inhabited_h : Inhabited α<VAR>f : ℕ → List α<VAR>hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f<VAR>hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f<VAR>hnil : ∀ (n : ℕ), f n ≠ []<VAR>this : ∀ (n : ℕ), (f n).headI ∈ s<VAR>g : ℕ ↪o ℕ<VAR>hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).headI (f (g n)).headI<GOAL>((fun n => if n < g 0 then f n else (f (g (n - g 0))).tail) (g 0)).length < (f (g 0)).length
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r✝ r : α → α → Prop<VAR>inst✝¹ : IsRefl α r<VAR>inst✝ : IsTrans α r<VAR>s : Set α<VAR>h : s.PartiallyWellOrderedOn r<VAR>h✝ : Nonempty α<VAR>inhabited_h : Inhabited α<VAR>f : ℕ → List α<VAR>hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f<VAR>hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f<VAR>hnil : ∀ (n : ℕ), f n ≠ []<VAR>this : ∀ (n : ℕ), (f n).headI ∈ s<VAR>g : ℕ ↪o ℕ<VAR>hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).headI (f (g n)).headI<VAR>hf' : (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) → ∃ m n, m < n ∧ List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail) (if n < g 0 then f n else (f (g (n - g 0))).tail)<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r✝ r : α → α → Prop<VAR>inst✝¹ : IsRefl α r<VAR>inst✝ : IsTrans α r<VAR>s : Set α<VAR>h : s.PartiallyWellOrderedOn r<VAR>h✝ : Nonempty α<VAR>inhabited_h : Inhabited α<VAR>f : ℕ → List α<VAR>hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f<VAR>hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f<VAR>hnil : ∀ (n : ℕ), f n ≠ []<VAR>this : ∀ (n : ℕ), (f n).headI ∈ s<VAR>g : ℕ ↪o ℕ<VAR>hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).headI (f (g n)).headI<VAR>hf' : (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) → ∃ m n, m < n ∧ List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail) (if n < g 0 then f n else (f (g (n - g 0))).tail)<VAR>m n : ℕ<VAR>mn : m < n<VAR>hmn : List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail) (if n < g 0 then f n else (f (g (n - g 0))).tail)<GOAL>False
<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>I : Ideal R<VAR>hI : I.IsPrime<GOAL>Ideal.map (algebraMap R (Localization.AtPrime I)) I = LocalRing.maximalIdeal (Localization I.primeCompl)
<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>I : Ideal R<VAR>hI : I.IsPrime<GOAL>LocalRing.maximalIdeal (Localization I.primeCompl) = Ideal.map (algebraMap R (Localization.AtPrime I)) (Ideal.comap (algebraMap R (Localization.AtPrime I)) (LocalRing.maximalIdeal (Localization I.primeCompl)))
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : Ring A'<VAR>inst✝⁵ : Algebra ℚ A<VAR>inst✝⁴ : Algebra ℚ A'<VAR>inst✝³ : Ring A<VAR>inst✝² : Ring A'<VAR>inst✝¹ : Algebra ℚ A<VAR>inst✝ : Algebra ℚ A'<VAR>n : ℕ<VAR>f : A →+* A'<GOAL>(constantCoeff A) (exp A) = 1
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : Ring A'<VAR>inst✝⁵ : Algebra ℚ A<VAR>inst✝⁴ : Algebra ℚ A'<VAR>inst✝³ : Ring A<VAR>inst✝² : Ring A'<VAR>inst✝¹ : Algebra ℚ A<VAR>inst✝ : Algebra ℚ A'<VAR>n : ℕ<VAR>f : A →+* A'<GOAL>(algebraMap ℚ A) (1 / ↑0!) = 1
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>hs : Convex ℝ s<VAR>hsc : IsClosed s<VAR>hf : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : Integrable f μ<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<GOAL>∫ (x : α), f x ∂μ ∈ s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g✝ : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>hs : Convex ℝ s<VAR>hsc : IsClosed s<VAR>hf : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : Integrable f μ<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>g : α → E<VAR>hgm : StronglyMeasurable g<VAR>hfg : f =ᶠ[ae μ] g<GOAL>∫ (x : α), f x ∂μ ∈ s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g✝ : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>hs : Convex ℝ s<VAR>hsc : IsClosed s<VAR>hf : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : Integrable f μ<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>g : α → E<VAR>hgm : StronglyMeasurable g<VAR>hfg : f =ᶠ[ae μ] g<VAR>this : SeparableSpace ↑(range g ∩ s)<GOAL>∫ (x : α), f x ∂μ ∈ s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g✝ : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>hs : Convex ℝ s<VAR>hsc : IsClosed s<VAR>hf : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : Integrable f μ<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>g : α → E<VAR>hgm : StronglyMeasurable g<VAR>hfg : f =ᶠ[ae μ] g<VAR>this : SeparableSpace ↑(range g ∩ s)<VAR>y₀ : E<VAR>h₀ : y₀ ∈ range g ∩ s<GOAL>∫ (x : α), f x ∂μ ∈ s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g✝ : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>hs : Convex ℝ s<VAR>hsc : IsClosed s<VAR>hf : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : Integrable f μ<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>g : α → E<VAR>hgm : StronglyMeasurable g<VAR>hfg : f =ᶠ[ae μ] g<VAR>this : SeparableSpace ↑(range g ∩ s)<VAR>y₀ : E<VAR>h₀ : y₀ ∈ range g ∩ s<GOAL>∫ (a : α), g a ∂μ ∈ s