ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : PredOrder α<VAR>inst✝ : SuccOrder α<VAR>a : α<GOAL>IsOpen {a}
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : PredOrder α<VAR>inst✝ : SuccOrder α<VAR>a : α<VAR>h_singleton_eq_inter : {a} = Iic a ∩ Ici a<GOAL>IsOpen {a}
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>m : M<GOAL>((RingQuot.mkAlgHom R (Rel Q)).toLinearMap ∘ₗ TensorAlgebra.ι R) m * ((RingQuot.mkAlgHom R (Rel Q)).toLinearMap ∘ₗ TensorAlgebra.ι R) m = (algebraMap R (CliffordAlgebra Q)) (Q m)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>m : M<GOAL>(RingQuot.mkAlgHom R (Rel Q)).toLinearMap ((TensorAlgebra.ι R) m) * (RingQuot.mkAlgHom R (Rel Q)).toLinearMap ((TensorAlgebra.ι R) m) = (algebraMap R (CliffordAlgebra Q)) (Q m)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>m : M<GOAL>(algebraMap R (RingQuot (Rel Q))) (Q m) = (algebraMap R (CliffordAlgebra Q)) (Q m)
<VAR>K : Type u_1<VAR>inst✝⁸ : NormedLinearOrderedField K<VAR>inst✝⁷ : HasSolidNorm K<VAR>inst✝⁶ : FloorRing K<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace K E<VAR>inst✝³ : FiniteDimensional K E<VAR>inst✝² : ProperSpace E<VAR>L : AddSubgroup E<VAR>inst✝¹ : DiscreteTopology ↥L<VAR>inst✝ : IsZlattice K L<GOAL>Module.Free ℤ ↥L
<VAR>K : Type u_1<VAR>inst✝⁸ : NormedLinearOrderedField K<VAR>inst✝⁷ : HasSolidNorm K<VAR>inst✝⁶ : FloorRing K<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace K E<VAR>inst✝³ : FiniteDimensional K E<VAR>inst✝² : ProperSpace E<VAR>L : AddSubgroup E<VAR>inst✝¹ : DiscreteTopology ↥L<VAR>inst✝ : IsZlattice K L<VAR>this : Module.Finite ℤ ↥L<GOAL>Module.Free ℤ ↥L
<VAR>C : Type u₁<VAR>inst✝¹⁰ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁹ : Category.{v₂, u₂} D<VAR>W : MorphismProperty C<VAR>M : Type w'<VAR>inst✝⁸ : AddMonoid M<VAR>inst✝⁷ : HasShift C M<VAR>inst✝⁶ : HasShift D M<VAR>inst✝⁵ : W.IsCompatibleWithShift M<VAR>L : C ⥤ D<VAR>inst✝⁴ : L.IsLocalization W<VAR>inst✝³ : HasShift D M<VAR>inst✝² : L.CommShift M<VAR>X Y Z T : C<VAR>a : M<VAR>inst✝¹ : HasSmallLocalizedShiftedHom W M X Y<VAR>inst✝ : HasSmallLocalizedShiftedHom W M Y Y<VAR>f : SmallShiftedHom W X Y a<VAR>n a' : M<VAR>h : a + n = a'<GOAL>((L.commShiftIso a').app Y).homToEquiv ((SmallHom.equiv W L) (f.shift n a' h)) = (L.commShiftIso n).hom.app X ≫ (shiftFunctor D n).map (((L.commShiftIso a).app Y).homToEquiv ((SmallHom.equiv W L) f)) ≫ (shiftFunctorAdd' D a n a' h).inv.app (L.obj Y)
<VAR>C : Type u₁<VAR>inst✝¹⁰ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁹ : Category.{v₂, u₂} D<VAR>W : MorphismProperty C<VAR>M : Type w'<VAR>inst✝⁸ : AddMonoid M<VAR>inst✝⁷ : HasShift C M<VAR>inst✝⁶ : HasShift D M<VAR>inst✝⁵ : W.IsCompatibleWithShift M<VAR>L : C ⥤ D<VAR>inst✝⁴ : L.IsLocalization W<VAR>inst✝³ : HasShift D M<VAR>inst✝² : L.CommShift M<VAR>X Y Z T : C<VAR>a : M<VAR>inst✝¹ : HasSmallLocalizedShiftedHom W M X Y<VAR>inst✝ : HasSmallLocalizedShiftedHom W M Y Y<VAR>f : SmallShiftedHom W X Y a<VAR>n a' : M<VAR>h : a + n = a'<GOAL>((L.commShiftIso n).hom.app X ≫ (shiftFunctor D n).map ((SmallHom.equiv W L) f) ≫ (shiftFunctor D n).map ((L.commShiftIso a).hom.app Y) ≫ (shiftFunctorAdd' D a n a' h).inv.app (L.obj Y) ≫ (L.commShiftIso a').inv.app Y) ≫ ((L.commShiftIso a').app Y).hom = (L.commShiftIso n).hom.app X ≫ (shiftFunctor D n).map ((SmallHom.equiv W L) f ≫ ((L.commShiftIso a).app Y).hom) ≫ (shiftFunctorAdd' D a n a' h).inv.app (L.obj Y)
<VAR>C : Type u₁<VAR>inst✝¹⁰ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁹ : Category.{v₂, u₂} D<VAR>W : MorphismProperty C<VAR>M : Type w'<VAR>inst✝⁸ : AddMonoid M<VAR>inst✝⁷ : HasShift C M<VAR>inst✝⁶ : HasShift D M<VAR>inst✝⁵ : W.IsCompatibleWithShift M<VAR>L : C ⥤ D<VAR>inst✝⁴ : L.IsLocalization W<VAR>inst✝³ : HasShift D M<VAR>inst✝² : L.CommShift M<VAR>X Y Z T : C<VAR>a : M<VAR>inst✝¹ : HasSmallLocalizedShiftedHom W M X Y<VAR>inst✝ : HasSmallLocalizedShiftedHom W M Y Y<VAR>f : SmallShiftedHom W X Y a<VAR>n a' : M<VAR>h : a + n = a'<GOAL>(L.commShiftIso n).hom.app X ≫ (shiftFunctor D n).map ((SmallHom.equiv W L) f) ≫ (shiftFunctor D n).map ((L.commShiftIso a).hom.app Y) ≫ (shiftFunctorAdd' D a n a' h).inv.app (L.obj Y) = (L.commShiftIso n).hom.app X ≫ (shiftFunctor D n).map ((SmallHom.equiv W L) f) ≫ (shiftFunctor D n).map ((L.commShiftIso a).hom.app Y) ≫ (shiftFunctorAdd' D a n a' h).inv.app (L.obj Y)
<VAR>α : Type u_1<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>d : Set α → ℝ := fun s => ↑(μ s).toNNReal - ↑(ν s).toNNReal<VAR>c : Set ℝ := d '' {s | MeasurableSet s}<VAR>γ : ℝ := sSup c<GOAL>∃ s, MeasurableSet s ∧ (∀ (t : Set α), MeasurableSet t → t ⊆ s → ν t ≤ μ t) ∧ ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → μ t ≤ ν t
<VAR>α : Type u_1<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>d : Set α → ℝ := fun s => ↑(μ s).toNNReal - ↑(ν s).toNNReal<VAR>c : Set ℝ := d '' {s | MeasurableSet s}<VAR>γ : ℝ := sSup c<VAR>hμ : ∀ (s : Set α), μ s ≠ ⊤<GOAL>∃ s, MeasurableSet s ∧ (∀ (t : Set α), MeasurableSet t → t ⊆ s → ν t ≤ μ t) ∧ ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → μ t ≤ ν t
<VAR>α : Type u_1<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>d : Set α → ℝ := fun s => ↑(μ s).toNNReal - ↑(ν s).toNNReal<VAR>c : Set ℝ := d '' {s | MeasurableSet s}<VAR>γ : ℝ := sSup c<VAR>hμ : ∀ (s : Set α), μ s ≠ ⊤<VAR>hν : ∀ (s : Set α), ν s ≠ ⊤<GOAL>∃ s, MeasurableSet s ∧ (∀ (t : Set α), MeasurableSet t → t ⊆ s → ν t ≤ μ t) ∧ ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → μ t ≤ ν t
<VAR>α : Type u_1<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>d : Set α → ℝ := fun s => ↑(μ s).toNNReal - ↑(ν s).toNNReal<VAR>c : Set ℝ := d '' {s | MeasurableSet s}<VAR>γ : ℝ := sSup c<VAR>hμ : ∀ (s : Set α), μ s ≠ ⊤<VAR>hν : ∀ (s : Set α), ν s ≠ ⊤<VAR>to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s<GOAL>∃ s, MeasurableSet s ∧ (∀ (t : Set α), MeasurableSet t → t ⊆ s → ν t ≤ μ t) ∧ ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → μ t ≤ ν t
<VAR>α : Type u_1<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>d : Set α → ℝ := fun s => ↑(μ s).toNNReal - ↑(ν s).toNNReal<VAR>c : Set ℝ := d '' {s | MeasurableSet s}<VAR>γ : ℝ := sSup c<VAR>hμ : ∀ (s : Set α), μ s ≠ ⊤<VAR>hν : ∀ (s : Set α), ν s ≠ ⊤<VAR>to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s<VAR>to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s<GOAL>∃ s, MeasurableSet s ∧ (∀ (t : Set α), MeasurableSet t → t ⊆ s → ν t ≤ μ t) ∧ ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → μ t ≤ ν t
<VAR>α : Type u_1<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>d : Set α → ℝ := fun s => ↑(μ s).toNNReal - ↑(ν s).toNNReal<VAR>c : Set ℝ := d '' {s | MeasurableSet s}<VAR>γ : ℝ := sSup c<VAR>hμ : ∀ (s : Set α), μ s ≠ ⊤<VAR>hν : ∀ (s : Set α), ν s ≠ ⊤<VAR>to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s<VAR>to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s<VAR>d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)<GOAL>∃ s, MeasurableSet s ∧ (∀ (t : Set α), MeasurableSet t → t ⊆ s → ν t ≤ μ t) ∧ ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → μ t ≤ ν t
<VAR>α : Type u_1<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>d : Set α → ℝ := fun s => ↑(μ s).toNNReal - ↑(ν s).toNNReal<VAR>c : Set ℝ := d '' {s | MeasurableSet s}<VAR>γ : ℝ := sSup c<VAR>hμ : ∀ (s : Set α), μ s ≠ ⊤<VAR>hν : ∀ (s : Set α), ν s ≠ ⊤<VAR>to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s<VAR>to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s<VAR>d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)<VAR>d_Union : ∀ (s : ℕ → Set α), Monotone s → Tendsto (fun n => d (s n)) atTop (𝓝 (d (⋃ n, s n)))<GOAL>∃ s, MeasurableSet s ∧ (∀ (t : Set α), MeasurableSet t → t ⊆ s → ν t ≤ μ t) ∧ ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → μ t ≤ ν t
<VAR>α : Type u_1<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>d : Set α → ℝ := fun s => ↑(μ s).toNNReal - ↑(ν s).toNNReal<VAR>c : Set ℝ := d '' {s | MeasurableSet s}<VAR>γ : ℝ := sSup c<VAR>hμ : ∀ (s : Set α), μ s ≠ ⊤<VAR>hν : ∀ (s : Set α), ν s ≠ ⊤<VAR>to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s<VAR>to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s<VAR>d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)<VAR>d_Union : ∀ (s : ℕ → Set α), Monotone s → Tendsto (fun n => d (s n)) atTop (𝓝 (d (⋃ n, s n)))<VAR>d_Inter : ∀ (s : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (s n)) → (∀ (n m : ℕ), n ≤ m → s m ⊆ s n) → Tendsto (fun n => d (s n)) atTop (𝓝 (d (⋂ n, s n)))<GOAL>∃ s, MeasurableSet s ∧ (∀ (t : Set α), MeasurableSet t → t ⊆ s → ν t ≤ μ t) ∧ ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → μ t ≤ ν t
<VAR>α : Type u_1<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>d : Set α → ℝ := fun s => ↑(μ s).toNNReal - ↑(ν s).toNNReal<VAR>c : Set ℝ := d '' {s | MeasurableSet s}<VAR>γ : ℝ := sSup c<VAR>hμ : ∀ (s : Set α), μ s ≠ ⊤<VAR>hν : ∀ (s : Set α), ν s ≠ ⊤<VAR>to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s<VAR>to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s<VAR>d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)<VAR>d_Union : ∀ (s : ℕ → Set α), Monotone s → Tendsto (fun n => d (s n)) atTop (𝓝 (d (⋃ n, s n)))<VAR>d_Inter : ∀ (s : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (s n)) → (∀ (n m : ℕ), n ≤ m → s m ⊆ s n) → Tendsto (fun n => d (s n)) atTop (𝓝 (d (⋂ n, s n)))<VAR>bdd_c : BddAbove c<GOAL>∃ s, MeasurableSet s ∧ (∀ (t : Set α), MeasurableSet t → t ⊆ s → ν t ≤ μ t) ∧ ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → μ t ≤ ν t
<VAR>α : Type u_1<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>d : Set α → ℝ := fun s => ↑(μ s).toNNReal - ↑(ν s).toNNReal<VAR>c : Set ℝ := d '' {s | MeasurableSet s}<VAR>γ : ℝ := sSup c<VAR>hμ : ∀ (s : Set α), μ s ≠ ⊤<VAR>hν : ∀ (s : Set α), ν s ≠ ⊤<VAR>to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s<VAR>to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s<VAR>d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)<VAR>d_Union : ∀ (s : ℕ → Set α), Monotone s → Tendsto (fun n => d (s n)) atTop (𝓝 (d (⋃ n, s n)))<VAR>d_Inter : ∀ (s : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (s n)) → (∀ (n m : ℕ), n ≤ m → s m ⊆ s n) → Tendsto (fun n => d (s n)) atTop (𝓝 (d (⋂ n, s n)))<VAR>bdd_c : BddAbove c<VAR>c_nonempty : c.Nonempty<GOAL>∃ s, MeasurableSet s ∧ (∀ (t : Set α), MeasurableSet t → t ⊆ s → ν t ≤ μ t) ∧ ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → μ t ≤ ν t
<VAR>α : Type u_1<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>d : Set α → ℝ := fun s => ↑(μ s).toNNReal - ↑(ν s).toNNReal<VAR>c : Set ℝ := d '' {s | MeasurableSet s}<VAR>γ : ℝ := sSup c<VAR>hμ : ∀ (s : Set α), μ s ≠ ⊤<VAR>hν : ∀ (s : Set α), ν s ≠ ⊤<VAR>to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s<VAR>to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s<VAR>d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)<VAR>d_Union : ∀ (s : ℕ → Set α), Monotone s → Tendsto (fun n => d (s n)) atTop (𝓝 (d (⋃ n, s n)))<VAR>d_Inter : ∀ (s : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (s n)) → (∀ (n m : ℕ), n ≤ m → s m ⊆ s n) → Tendsto (fun n => d (s n)) atTop (𝓝 (d (⋂ n, s n)))<VAR>bdd_c : BddAbove c<VAR>c_nonempty : c.Nonempty<VAR>d_le_γ : ∀ (s : Set α), MeasurableSet s → d s ≤ γ<GOAL>∃ s, MeasurableSet s ∧ (∀ (t : Set α), MeasurableSet t → t ⊆ s → ν t ≤ μ t) ∧ ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → μ t ≤ ν t
<VAR>α : Type u_1<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>d : Set α → ℝ := fun s => ↑(μ s).toNNReal - ↑(ν s).toNNReal<VAR>c : Set ℝ := d '' {s | MeasurableSet s}<VAR>γ : ℝ := sSup c<VAR>hμ : ∀ (s : Set α), μ s ≠ ⊤<VAR>hν : ∀ (s : Set α), ν s ≠ ⊤<VAR>to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s<VAR>to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s<VAR>d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)<VAR>d_Union : ∀ (s : ℕ → Set α), Monotone s → Tendsto (fun n => d (s n)) atTop (𝓝 (d (⋃ n, s n)))<VAR>d_Inter : ∀ (s : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (s n)) → (∀ (n m : ℕ), n ≤ m → s m ⊆ s n) → Tendsto (fun n => d (s n)) atTop (𝓝 (d (⋂ n, s n)))<VAR>bdd_c : BddAbove c<VAR>c_nonempty : c.Nonempty<VAR>d_le_γ : ∀ (s : Set α), MeasurableSet s → d s ≤ γ<VAR>this : ∀ (n : ℕ), ∃ s, MeasurableSet s ∧ γ - (1 / 2) ^ n < d s<GOAL>∃ s, MeasurableSet s ∧ (∀ (t : Set α), MeasurableSet t → t ⊆ s → ν t ≤ μ t) ∧ ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → μ t ≤ ν t
<VAR>α : Type u_1<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>d : Set α → ℝ := fun s => ↑(μ s).toNNReal - ↑(ν s).toNNReal<VAR>c : Set ℝ := d '' {s | MeasurableSet s}<VAR>γ : ℝ := sSup c<VAR>hμ : ∀ (s : Set α), μ s ≠ ⊤<VAR>hν : ∀ (s : Set α), ν s ≠ ⊤<VAR>to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s<VAR>to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s<VAR>d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)<VAR>d_Union : ∀ (s : ℕ → Set α), Monotone s → Tendsto (fun n => d (s n)) atTop (𝓝 (d (⋃ n, s n)))<VAR>d_Inter : ∀ (s : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (s n)) → (∀ (n m : ℕ), n ≤ m → s m ⊆ s n) → Tendsto (fun n => d (s n)) atTop (𝓝 (d (⋂ n, s n)))<VAR>bdd_c : BddAbove c<VAR>c_nonempty : c.Nonempty<VAR>d_le_γ : ∀ (s : Set α), MeasurableSet s → d s ≤ γ<VAR>this : ∀ (n : ℕ), ∃ s, MeasurableSet s ∧ γ - (1 / 2) ^ n < d s<VAR>e : ℕ → Set α<VAR>he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d (e x)<GOAL>∃ s, MeasurableSet s ∧ (∀ (t : Set α), MeasurableSet t → t ⊆ s → ν t ≤ μ t) ∧ ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → μ t ≤ ν t
<VAR>α : Type u_1<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>d : Set α → ℝ := fun s => ↑(μ s).toNNReal - ↑(ν s).toNNReal<VAR>c : Set ℝ := d '' {s | MeasurableSet s}<VAR>γ : ℝ := sSup c<VAR>hμ : ∀ (s : Set α), μ s ≠ ⊤<VAR>hν : ∀ (s : Set α), ν s ≠ ⊤<VAR>to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s<VAR>to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s<VAR>d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)<VAR>d_Union : ∀ (s : ℕ → Set α), Monotone s → Tendsto (fun n => d (s n)) atTop (𝓝 (d (⋃ n, s n)))<VAR>d_Inter : ∀ (s : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (s n)) → (∀ (n m : ℕ), n ≤ m → s m ⊆ s n) → Tendsto (fun n => d (s n)) atTop (𝓝 (d (⋂ n, s n)))<VAR>bdd_c : BddAbove c<VAR>c_nonempty : c.Nonempty<VAR>d_le_γ : ∀ (s : Set α), MeasurableSet s → d s ≤ γ<VAR>this : ∀ (n : ℕ), ∃ s, MeasurableSet s ∧ γ - (1 / 2) ^ n < d s<VAR>e : ℕ → Set α<VAR>he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d (e x)<VAR>he₁ : ∀ (n : ℕ), MeasurableSet (e n)<GOAL>∃ s, MeasurableSet s ∧ (∀ (t : Set α), MeasurableSet t → t ⊆ s → ν t ≤ μ t) ∧ ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → μ t ≤ ν t
<VAR>α : Type u_1<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>d : Set α → ℝ := fun s => ↑(μ s).toNNReal - ↑(ν s).toNNReal<VAR>c : Set ℝ := d '' {s | MeasurableSet s}<VAR>γ : ℝ := sSup c<VAR>hμ : ∀ (s : Set α), μ s ≠ ⊤<VAR>hν : ∀ (s : Set α), ν s ≠ ⊤<VAR>to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s<VAR>to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s<VAR>d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)<VAR>d_Union : ∀ (s : ℕ → Set α), Monotone s → Tendsto (fun n => d (s n)) atTop (𝓝 (d (⋃ n, s n)))<VAR>d_Inter : ∀ (s : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (s n)) → (∀ (n m : ℕ), n ≤ m → s m ⊆ s n) → Tendsto (fun n => d (s n)) atTop (𝓝 (d (⋂ n, s n)))<VAR>bdd_c : BddAbove c<VAR>c_nonempty : c.Nonempty<VAR>d_le_γ : ∀ (s : Set α), MeasurableSet s → d s ≤ γ<VAR>this : ∀ (n : ℕ), ∃ s, MeasurableSet s ∧ γ - (1 / 2) ^ n < d s<VAR>e : ℕ → Set α<VAR>he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d (e x)<VAR>he₁ : ∀ (n : ℕ), MeasurableSet (e n)<VAR>he₂ : ∀ (n : ℕ), γ - (1 / 2) ^ n < d (e n)<GOAL>∃ s, MeasurableSet s ∧ (∀ (t : Set α), MeasurableSet t → t ⊆ s → ν t ≤ μ t) ∧ ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → μ t ≤ ν t
<VAR>α : Type u_1<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>d : Set α → ℝ := fun s => ↑(μ s).toNNReal - ↑(ν s).toNNReal<VAR>c : Set ℝ := d '' {s | MeasurableSet s}<VAR>γ : ℝ := sSup c<VAR>hμ : ∀ (s : Set α), μ s ≠ ⊤<VAR>hν : ∀ (s : Set α), ν s ≠ ⊤<VAR>to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s<VAR>to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s<VAR>d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)<VAR>d_Union : ∀ (s : ℕ → Set α), Monotone s → Tendsto (fun n => d (s n)) atTop (𝓝 (d (⋃ n, s n)))<VAR>d_Inter : ∀ (s : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (s n)) → (∀ (n m : ℕ), n ≤ m → s m ⊆ s n) → Tendsto (fun n => d (s n)) atTop (𝓝 (d (⋂ n, s n)))<VAR>bdd_c : BddAbove c<VAR>c_nonempty : c.Nonempty<VAR>d_le_γ : ∀ (s : Set α), MeasurableSet s → d s ≤ γ<VAR>this : ∀ (n : ℕ), ∃ s, MeasurableSet s ∧ γ - (1 / 2) ^ n < d s<VAR>e : ℕ → Set α<VAR>he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d (e x)<VAR>he₁ : ∀ (n : ℕ), MeasurableSet (e n)<VAR>he₂ : ∀ (n : ℕ), γ - (1 / 2) ^ n < d (e n)<VAR>f : ℕ → ℕ → Set α := fun n m => (Finset.Ico n (m + 1)).inf e<GOAL>∃ s, MeasurableSet s ∧ (∀ (t : Set α), MeasurableSet t → t ⊆ s → ν t ≤ μ t) ∧ ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → μ t ≤ ν t
<VAR>α : Type u_1<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>d : Set α → ℝ := fun s => ↑(μ s).toNNReal - ↑(ν s).toNNReal<VAR>c : Set ℝ := d '' {s | MeasurableSet s}<VAR>γ : ℝ := sSup c<VAR>hμ : ∀ (s : Set α), μ s ≠ ⊤<VAR>hν : ∀ (s : Set α), ν s ≠ ⊤<VAR>to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s<VAR>to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s<VAR>d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)<VAR>d_Union : ∀ (s : ℕ → Set α), Monotone s → Tendsto (fun n => d (s n)) atTop (𝓝 (d (⋃ n, s n)))<VAR>d_Inter : ∀ (s : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (s n)) → (∀ (n m : ℕ), n ≤ m → s m ⊆ s n) → Tendsto (fun n => d (s n)) atTop (𝓝 (d (⋂ n, s n)))<VAR>bdd_c : BddAbove c<VAR>c_nonempty : c.Nonempty<VAR>d_le_γ : ∀ (s : Set α), MeasurableSet s → d s ≤ γ<VAR>this : ∀ (n : ℕ), ∃ s, MeasurableSet s ∧ γ - (1 / 2) ^ n < d s<VAR>e : ℕ → Set α<VAR>he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d (e x)<VAR>he₁ : ∀ (n : ℕ), MeasurableSet (e n)<VAR>he₂ : ∀ (n : ℕ), γ - (1 / 2) ^ n < d (e n)<VAR>f : ℕ → ℕ → Set α := fun n m => (Finset.Ico n (m + 1)).inf e<VAR>hf : ∀ (n m : ℕ), MeasurableSet (f n m)<GOAL>∃ s, MeasurableSet s ∧ (∀ (t : Set α), MeasurableSet t → t ⊆ s → ν t ≤ μ t) ∧ ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → μ t ≤ ν t
<VAR>α : Type u_1<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>d : Set α → ℝ := fun s => ↑(μ s).toNNReal - ↑(ν s).toNNReal<VAR>c : Set ℝ := d '' {s | MeasurableSet s}<VAR>γ : ℝ := sSup c<VAR>hμ : ∀ (s : Set α), μ s ≠ ⊤<VAR>hν : ∀ (s : Set α), ν s ≠ ⊤<VAR>to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s<VAR>to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s<VAR>d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)<VAR>d_Union : ∀ (s : ℕ → Set α), Monotone s → Tendsto (fun n => d (s n)) atTop (𝓝 (d (⋃ n, s n)))<VAR>d_Inter : ∀ (s : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (s n)) → (∀ (n m : ℕ), n ≤ m → s m ⊆ s n) → Tendsto (fun n => d (s n)) atTop (𝓝 (d (⋂ n, s n)))<VAR>bdd_c : BddAbove c<VAR>c_nonempty : c.Nonempty<VAR>d_le_γ : ∀ (s : Set α), MeasurableSet s → d s ≤ γ<VAR>this : ∀ (n : ℕ), ∃ s, MeasurableSet s ∧ γ - (1 / 2) ^ n < d s<VAR>e : ℕ → Set α<VAR>he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d (e x)<VAR>he₁ : ∀ (n : ℕ), MeasurableSet (e n)<VAR>he₂ : ∀ (n : ℕ), γ - (1 / 2) ^ n < d (e n)<VAR>f : ℕ → ℕ → Set α := fun n m => (Finset.Ico n (m + 1)).inf e<VAR>hf : ∀ (n m : ℕ), MeasurableSet (f n m)<VAR>f_subset_f : ∀ {a b c d : ℕ}, a ≤ b → c ≤ d → f a d ⊆ f b c<GOAL>∃ s, MeasurableSet s ∧ (∀ (t : Set α), MeasurableSet t → t ⊆ s → ν t ≤ μ t) ∧ ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → μ t ≤ ν t
<VAR>α : Type u_1<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>d : Set α → ℝ := fun s => ↑(μ s).toNNReal - ↑(ν s).toNNReal<VAR>c : Set ℝ := d '' {s | MeasurableSet s}<VAR>γ : ℝ := sSup c<VAR>hμ : ∀ (s : Set α), μ s ≠ ⊤<VAR>hν : ∀ (s : Set α), ν s ≠ ⊤<VAR>to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s<VAR>to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s<VAR>d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)<VAR>d_Union : ∀ (s : ℕ → Set α), Monotone s → Tendsto (fun n => d (s n)) atTop (𝓝 (d (⋃ n, s n)))<VAR>d_Inter : ∀ (s : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (s n)) → (∀ (n m : ℕ), n ≤ m → s m ⊆ s n) → Tendsto (fun n => d (s n)) atTop (𝓝 (d (⋂ n, s n)))<VAR>bdd_c : BddAbove c<VAR>c_nonempty : c.Nonempty<VAR>d_le_γ : ∀ (s : Set α), MeasurableSet s → d s ≤ γ<VAR>this : ∀ (n : ℕ), ∃ s, MeasurableSet s ∧ γ - (1 / 2) ^ n < d s<VAR>e : ℕ → Set α<VAR>he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d (e x)<VAR>he₁ : ∀ (n : ℕ), MeasurableSet (e n)<VAR>he₂ : ∀ (n : ℕ), γ - (1 / 2) ^ n < d (e n)<VAR>f : ℕ → ℕ → Set α := fun n m => (Finset.Ico n (m + 1)).inf e<VAR>hf : ∀ (n m : ℕ), MeasurableSet (f n m)<VAR>f_subset_f : ∀ {a b c d : ℕ}, a ≤ b → c ≤ d → f a d ⊆ f b c<VAR>f_succ : ∀ (n m : ℕ), n ≤ m → f n (m + 1) = f n m ∩ e (m + 1)<GOAL>∃ s, MeasurableSet s ∧ (∀ (t : Set α), MeasurableSet t → t ⊆ s → ν t ≤ μ t) ∧ ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → μ t ≤ ν t
<VAR>α : Type u_1<VAR>inst✝² : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>d : Set α → ℝ := fun s => ↑(μ s).toNNReal - ↑(ν s).toNNReal<VAR>c : Set ℝ := d '' {s | MeasurableSet s}<VAR>γ : ℝ := sSup c<VAR>hμ : ∀ (s : Set α), μ s ≠ ⊤<VAR>hν : ∀ (s : Set α), ν s ≠ ⊤<VAR>to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s<VAR>to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s<VAR>d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)<VAR>d_Union : ∀ (s : ℕ → Set α), Monotone s → Tendsto (fun n => d (s n)) atTop (𝓝 (d (⋃ n, s n)))<VAR>d_Inter : ∀ (s : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (s n)) → (∀ (n m : ℕ), n ≤ m → s m ⊆ s n) → Tendsto (fun n => d (s n)) atTop (𝓝 (d (⋂ n, s n)))<VAR>bdd_c : BddAbove c<VAR>c_nonempty : c.Nonempty<VAR>d_le_γ : ∀ (s : Set α), MeasurableSet s → d s ≤ γ<VAR>this : ∀ (n : ℕ), ∃ s, MeasurableSet s ∧ γ - (1 / 2) ^ n < d s<VAR>e : ℕ → Set α<VAR>he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d (e x)<VAR>he₁ : ∀ (n : ℕ), MeasurableSet (e n)<VAR>he₂ : ∀ (n : ℕ), γ - (1 / 2) ^ n < d (e n)<VAR>f : ℕ → ℕ → Set α := fun n m => (Finset.Ico n (m + 1)).inf e<VAR>hf : ∀ (n m : ℕ), MeasurableSet (f n m)<VAR>f_subset_f : ∀ {a b c d : ℕ}, a ≤ b → c ≤ d → f a d ⊆ f b c<VAR>f_succ : ∀ (n m : ℕ), n ≤ m → f n (m + 1) = f n m ∩ e (m + 1)<VAR>le_d_f : ∀ (n m : ℕ), m ≤ n → γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n ≤ d (f m n)<VAR>s : Set α := ⋃ m, ⋂ n, f m n<VAR>γ_le_d_s : γ ≤ d s<GOAL>∃ s, MeasurableSet s ∧ (∀ (t : Set α), MeasurableSet t → t ⊆ s → ν t ≤ μ t) ∧ ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → μ t ≤ ν t