awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
t : Set α
m0 : MeasurableSpace α
m : Set (Measure α)
hm : m.Nonempty
ht : MeasurableSet t
s : Set α
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (((sInf m).restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((sInf (image (α := Measure α) toOuterMeasure ((fun (μ : Measure α) ↦ μ.restrict t) '' m)) : OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((sInf m).restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((sInf ((fun (μ : Measure α) ↦ μ.restrict t) '' m) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) ((sInf m : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
  (((sInf (image (α := Measure α) toOuterMeasure ((fun (μ : Measure α) ↦ μ.restrict t) '' m)) : OuterMeasure α) :
        (a : Set α) → ℝ≥0∞)
      s :
    ℝ≥0∞)
Tactic: simp_rw [sInf_apply hs, restrict_apply hs, sInf_apply (MeasurableSet.inter hs ht),
    Set.image_image, restrict_toOuterMeasure_eq_toOuterMeasure_restrict ht, ←
    Set.image_image _ toOuterMeasure, ← OuterMeasure.restrict_sInf_eq_sInf_restrict _ (hm.image _),
    OuterMeasure.restrict_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
t : Set α
m0 : MeasurableSpace α
m : Set (Measure α)
hm : m.Nonempty
ht : MeasurableSet t
s : Set α
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (((sInf m).restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((sInf (image (α := Measure α) toOuterMeasure ((fun (μ : Measure α) ↦ μ.restrict t) '' m)) : OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) ((sInf m : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
    (((sInf (image (α := Measure α) toOuterMeasure ((fun (μ : Measure α) ↦ μ.restrict t) '' m)) : OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((sInf m).restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((sInf ((fun (μ : Measure α) ↦ μ.restrict t) '' m) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h₂ : Eq (α := ℝ≥0∞) ((sInf (toOuterMeasure '' m) : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
  (((sInf (image (α := Measure α) toOuterMeasure ((fun (μ : Measure α) ↦ μ.restrict t) '' m)) : OuterMeasure α) :
        (a : Set α) → ℝ≥0∞)
      s :
    ℝ≥0∞)
Tactic: simp_rw [sInf_apply hs, restrict_apply hs, sInf_apply (MeasurableSet.inter hs ht),
    Set.image_image, restrict_toOuterMeasure_eq_toOuterMeasure_restrict ht, ←
    Set.image_image _ toOuterMeasure, ← OuterMeasure.restrict_sInf_eq_sInf_restrict _ (hm.image _),
    OuterMeasure.restrict_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
t : Set α
m0 : MeasurableSpace α
m : Set (Measure α)
hm : m.Nonempty
ht : MeasurableSet t
s : Set α
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (((sInf m).restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((sInf (image (α := Measure α) toOuterMeasure ((fun (μ : Measure α) ↦ μ.restrict t) '' m)) : OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) ((sInf m : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
    (((sInf (image (α := Measure α) toOuterMeasure ((fun (μ : Measure α) ↦ μ.restrict t) '' m)) : OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
h₂ :
  Eq (α := ℝ≥0∞) ((sInf (toOuterMeasure '' m) : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
    (((sInf (image (α := Measure α) toOuterMeasure ((fun (μ : Measure α) ↦ μ.restrict t) '' m)) : OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((sInf m).restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((sInf ((fun (μ : Measure α) ↦ μ.restrict t) '' m) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h₃ : Eq (α := ℝ≥0∞) ((sInf (toOuterMeasure '' m) : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
  (((sInf ((fun (x : Measure α) ↦ (x.restrict t).toOuterMeasure) '' m) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: simp_rw [sInf_apply hs, restrict_apply hs, sInf_apply (MeasurableSet.inter hs ht),
    Set.image_image, restrict_toOuterMeasure_eq_toOuterMeasure_restrict ht, ←
    Set.image_image _ toOuterMeasure, ← OuterMeasure.restrict_sInf_eq_sInf_restrict _ (hm.image _),
    OuterMeasure.restrict_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
t : Set α
m0 : MeasurableSpace α
m : Set (Measure α)
hm : m.Nonempty
ht : MeasurableSet t
s : Set α
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (((sInf m).restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((sInf (image (α := Measure α) toOuterMeasure ((fun (μ : Measure α) ↦ μ.restrict t) '' m)) : OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) ((sInf m : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
    (((sInf (image (α := Measure α) toOuterMeasure ((fun (μ : Measure α) ↦ μ.restrict t) '' m)) : OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
h₂ :
  Eq (α := ℝ≥0∞) ((sInf (toOuterMeasure '' m) : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
    (((sInf (image (α := Measure α) toOuterMeasure ((fun (μ : Measure α) ↦ μ.restrict t) '' m)) : OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
h₃ :
  Eq (α := ℝ≥0∞) ((sInf (toOuterMeasure '' m) : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
    (((sInf ((fun (x : Measure α) ↦ (x.restrict t).toOuterMeasure) '' m) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((sInf m).restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((sInf ((fun (μ : Measure α) ↦ μ.restrict t) '' m) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h₄ : Eq (α := ℝ≥0∞) ((sInf (toOuterMeasure '' m) : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
  (((sInf
            ((fun (a : Measure α) ↦
                (OuterMeasure.restrict t : (a : OuterMeasure α) → OuterMeasure α) a.toOuterMeasure) ''
              m) :
          OuterMeasure α) :
        (a : Set α) → ℝ≥0∞)
      s :
    ℝ≥0∞)
Tactic: simp_rw [sInf_apply hs, restrict_apply hs, sInf_apply (MeasurableSet.inter hs ht),
    Set.image_image, restrict_toOuterMeasure_eq_toOuterMeasure_restrict ht, ←
    Set.image_image _ toOuterMeasure, ← OuterMeasure.restrict_sInf_eq_sInf_restrict _ (hm.image _),
    OuterMeasure.restrict_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
t : Set α
m0 : MeasurableSpace α
m : Set (Measure α)
hm : m.Nonempty
ht : MeasurableSet t
s : Set α
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (((sInf m).restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((sInf (image (α := Measure α) toOuterMeasure ((fun (μ : Measure α) ↦ μ.restrict t) '' m)) : OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) ((sInf m : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
    (((sInf (image (α := Measure α) toOuterMeasure ((fun (μ : Measure α) ↦ μ.restrict t) '' m)) : OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
h₂ :
  Eq (α := ℝ≥0∞) ((sInf (toOuterMeasure '' m) : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
    (((sInf (image (α := Measure α) toOuterMeasure ((fun (μ : Measure α) ↦ μ.restrict t) '' m)) : OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
h₃ :
  Eq (α := ℝ≥0∞) ((sInf (toOuterMeasure '' m) : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
    (((sInf ((fun (x : Measure α) ↦ (x.restrict t).toOuterMeasure) '' m) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s :
      ℝ≥0∞)
h₄ :
  Eq (α := ℝ≥0∞) ((sInf (toOuterMeasure '' m) : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
    (((sInf
              ((fun (a : Measure α) ↦
                  (OuterMeasure.restrict t : (a : OuterMeasure α) → OuterMeasure α) a.toOuterMeasure) ''
                m) :
            OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((sInf m).restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((sInf ((fun (μ : Measure α) ↦ μ.restrict t) '' m) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h₅ : Eq (α := ℝ≥0∞) ((sInf (toOuterMeasure '' m) : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
  (((sInf ((⇑(OuterMeasure.restrict t) : (a : OuterMeasure α) → OuterMeasure α) '' toOuterMeasure '' m) :
          OuterMeasure α) :
        (a : Set α) → ℝ≥0∞)
      s :
    ℝ≥0∞)
Tactic: simp_rw [sInf_apply hs, restrict_apply hs, sInf_apply (MeasurableSet.inter hs ht),
    Set.image_image, restrict_toOuterMeasure_eq_toOuterMeasure_restrict ht, ←
    Set.image_image _ toOuterMeasure, ← OuterMeasure.restrict_sInf_eq_sInf_restrict _ (hm.image _),
    OuterMeasure.restrict_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
t : Set α
m0 : MeasurableSpace α
m : Set (Measure α)
hm : m.Nonempty
ht : MeasurableSet t
s : Set α
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (((sInf m).restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((sInf (image (α := Measure α) toOuterMeasure ((fun (μ : Measure α) ↦ μ.restrict t) '' m)) : OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) ((sInf m : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
    (((sInf (image (α := Measure α) toOuterMeasure ((fun (μ : Measure α) ↦ μ.restrict t) '' m)) : OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
h₂ :
  Eq (α := ℝ≥0∞) ((sInf (toOuterMeasure '' m) : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
    (((sInf (image (α := Measure α) toOuterMeasure ((fun (μ : Measure α) ↦ μ.restrict t) '' m)) : OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
h₃ :
  Eq (α := ℝ≥0∞) ((sInf (toOuterMeasure '' m) : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
    (((sInf ((fun (x : Measure α) ↦ (x.restrict t).toOuterMeasure) '' m) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s :
      ℝ≥0∞)
h₄ :
  Eq (α := ℝ≥0∞) ((sInf (toOuterMeasure '' m) : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
    (((sInf
              ((fun (a : Measure α) ↦
                  (OuterMeasure.restrict t : (a : OuterMeasure α) → OuterMeasure α) a.toOuterMeasure) ''
                m) :
            OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
h₅ :
  Eq (α := ℝ≥0∞) ((sInf (toOuterMeasure '' m) : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
    (((sInf ((⇑(OuterMeasure.restrict t) : (a : OuterMeasure α) → OuterMeasure α) '' toOuterMeasure '' m) :
            OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((sInf m).restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((sInf ((fun (μ : Measure α) ↦ μ.restrict t) '' m) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h₆ : Eq (α := ℝ≥0∞) ((sInf (toOuterMeasure '' m) : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
  ((((OuterMeasure.restrict t : (a : OuterMeasure α) → OuterMeasure α) (sInf (toOuterMeasure '' m)) : OuterMeasure α) :
        (a : Set α) → ℝ≥0∞)
      s :
    ℝ≥0∞)
Tactic: simp_rw [sInf_apply hs, restrict_apply hs, sInf_apply (MeasurableSet.inter hs ht),
    Set.image_image, restrict_toOuterMeasure_eq_toOuterMeasure_restrict ht, ←
    Set.image_image _ toOuterMeasure, ← OuterMeasure.restrict_sInf_eq_sInf_restrict _ (hm.image _),
    OuterMeasure.restrict_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
p : α → Prop
hp : ∀ᵐ (x : α) ∂μ.restrict s, p x
⊢ ∃ x ∈ s, p x
have rw : ∀ (hs : ∃ᵐ (a : α) ∂μ.restrict s, a ∈ s) {p : α → Prop} (hp : ∀ᵐ (x : α) ∂μ.restrict s, p x), ∃ x ∈ s, p x
Tactic: rw [← μ.restrict_apply_self, ← frequently_ae_mem_iff] at hs
Cleared hypotheses: hs, p, hp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
ν : Measure β
f : α → β
hf : QuasiMeasurePreserving f μ ν
t : Set β
hmaps : MapsTo f s t
⊢ map f (μ.restrict s) ≪ ν.restrict t
have refine : ∀ (u : Set β) (hum : MeasurableSet u),
  Eq (α := ℝ≥0∞) ((ν.restrict t : (a : Set β) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) (((map f (μ.restrict s) : Measure β) : (a : Set β) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine AbsolutelyContinuous.mk fun u hum ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
ν : Measure β
f : α → β
hf : QuasiMeasurePreserving f μ ν
t : Set β
hmaps : MapsTo f s t
u : Set β
hum : MeasurableSet u
⊢ Eq (α := ℝ≥0∞) ((ν.restrict t : (a : Set β) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) (((map f (μ.restrict s) : Measure β) : (a : Set β) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
have suffices : Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞) →
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' u ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: suffices ν (u ∩ t) = 0 → μ (f ⁻¹' u ∩ s) = 0 by simpa [hum, hf.measurable, hf.measurable hum]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
ν : Measure β
f : α → β
hf : QuasiMeasurePreserving f μ ν
t : Set β
hmaps : MapsTo f s t
u : Set β
hum : MeasurableSet u
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' u ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
have refine : ∀ (hu : Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)), f ⁻¹' u ∩ s ⊆ f ⁻¹' (u ∩ t)
Tactic: refine fun hu ↦ measure_mono_null ?_ (hf.preimage_null hu)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
ν : Measure β
f : α → β
hf : QuasiMeasurePreserving f μ ν
t : Set β
hmaps : MapsTo f s t
u : Set β
hum : MeasurableSet u
hu : Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ f ⁻¹' u ∩ s ⊆ f ⁻¹' (u ∩ t)
have rw : f ⁻¹' u ∩ s ⊆ f ⁻¹' u ∩ f ⁻¹' t
Tactic: rw [preimage_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
ν : Measure β
f : α → β
hf : QuasiMeasurePreserving f μ ν
t : Set β
hmaps : MapsTo f s t
u : Set β
hum : MeasurableSet u
hu : Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ f ⁻¹' u ∩ s ⊆ f ⁻¹' u ∩ f ⁻¹' t
have h₂ : s ⊆ f ⁻¹' t
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
inst : Countable ι
s : ι → Set α
hs : Eq.{u_2 + 1} (α := Set α) (⋃ (i : ι), s i) univ
⊢ μ = ν ↔ ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)
have rw : μ = ν ↔ μ.restrict (⋃ (i : ι), s i) = ν.restrict (⋃ (i : ι), s i)
Tactic: rw [← restrict_iUnion_congr, hs, restrict_univ, restrict_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
inst : Countable ι
s : ι → Set α
hs : Eq.{u_2 + 1} (α := Set α) (⋃ (i : ι), s i) univ
rw : μ = ν ↔ μ.restrict (⋃ (i : ι), s i) = ν.restrict (⋃ (i : ι), s i)
⊢ μ = ν ↔ ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)
have rw₁ : μ = ν ↔ μ.restrict univ = ν.restrict univ
Tactic: rw [← restrict_iUnion_congr, hs, restrict_univ, restrict_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
inst : Countable ι
s : ι → Set α
hs : Eq.{u_2 + 1} (α := Set α) (⋃ (i : ι), s i) univ
rw : μ = ν ↔ μ.restrict (⋃ (i : ι), s i) = ν.restrict (⋃ (i : ι), s i)
rw₁ : μ = ν ↔ μ.restrict univ = ν.restrict univ
⊢ μ = ν ↔ ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)
have rw₂ : μ = ν ↔ μ = ν.restrict univ
Tactic: rw [← restrict_iUnion_congr, hs, restrict_univ, restrict_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
inst : Countable ι
s : ι → Set α
hs : Eq.{u_2 + 1} (α := Set α) (⋃ (i : ι), s i) univ
rw : μ = ν ↔ μ.restrict (⋃ (i : ι), s i) = ν.restrict (⋃ (i : ι), s i)
rw₁ : μ = ν ↔ μ.restrict univ = ν.restrict univ
rw₂ : μ = ν ↔ μ = ν.restrict univ
⊢ μ = ν ↔ ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)
have rw₃ : μ = ν ↔ μ = ν
Tactic: rw [← restrict_iUnion_congr, hs, restrict_univ, restrict_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
S : Set ι
s : ι → Set α
hc : S.Countable
hs : Eq.{u_2 + 1} (α := Set α) (⋃ i ∈ S, s i) univ
⊢ μ = ν ↔ ∀ i ∈ S, μ.restrict (s i) = ν.restrict (s i)
have rw : μ = ν ↔ μ.restrict (⋃ i ∈ S, s i) = ν.restrict (⋃ i ∈ S, s i)
Tactic: rw [← restrict_biUnion_congr hc, hs, restrict_univ, restrict_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
S : Set ι
s : ι → Set α
hc : S.Countable
hs : Eq.{u_2 + 1} (α := Set α) (⋃ i ∈ S, s i) univ
rw : μ = ν ↔ μ.restrict (⋃ i ∈ S, s i) = ν.restrict (⋃ i ∈ S, s i)
⊢ μ = ν ↔ ∀ i ∈ S, μ.restrict (s i) = ν.restrict (s i)
have rw₁ : μ = ν ↔ μ.restrict univ = ν.restrict univ
Tactic: rw [← restrict_biUnion_congr hc, hs, restrict_univ, restrict_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
S : Set ι
s : ι → Set α
hc : S.Countable
hs : Eq.{u_2 + 1} (α := Set α) (⋃ i ∈ S, s i) univ
rw : μ = ν ↔ μ.restrict (⋃ i ∈ S, s i) = ν.restrict (⋃ i ∈ S, s i)
rw₁ : μ = ν ↔ μ.restrict univ = ν.restrict univ
⊢ μ = ν ↔ ∀ i ∈ S, μ.restrict (s i) = ν.restrict (s i)
have rw₂ : μ = ν ↔ μ = ν.restrict univ
Tactic: rw [← restrict_biUnion_congr hc, hs, restrict_univ, restrict_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
S : Set ι
s : ι → Set α
hc : S.Countable
hs : Eq.{u_2 + 1} (α := Set α) (⋃ i ∈ S, s i) univ
rw : μ = ν ↔ μ.restrict (⋃ i ∈ S, s i) = ν.restrict (⋃ i ∈ S, s i)
rw₁ : μ = ν ↔ μ.restrict univ = ν.restrict univ
rw₂ : μ = ν ↔ μ = ν.restrict univ
⊢ μ = ν ↔ ∀ i ∈ S, μ.restrict (s i) = ν.restrict (s i)
have rw₃ : μ = ν ↔ μ = ν
Tactic: rw [← restrict_biUnion_congr hc, hs, restrict_univ, restrict_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
hc : T.Countable
h_inter : IsPiSystem S
hU : ⋃₀ T = univ
htop : ∀ t ∈ T, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ST_eq :
  ∀ t ∈ T, ∀ s ∈ S, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
T_eq : ∀ t ∈ T, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ μ = ν
have refine : ∀ (t : Set α) (ht : t ∈ T), μ.restrict t = ν.restrict t
Tactic: refine ext_of_sUnion_eq_univ hc hU fun t ht => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
hc : T.Countable
h_inter : IsPiSystem S
hU : ⋃₀ T = univ
htop : ∀ t ∈ T, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ST_eq :
  ∀ t ∈ T, ∀ s ∈ S, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
T_eq : ∀ t ∈ T, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
t : Set α
ht : t ∈ T
⊢ μ.restrict t = ν.restrict t
have h : ∀ (u : Set α) (hu : MeasurableSet u),
  Eq (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) ((ν.restrict t : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
Tactic: ext1 u hu
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
hc : T.Countable
h_inter : IsPiSystem S
hU : ⋃₀ T = univ
htop : ∀ t ∈ T, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ST_eq :
  ∀ t ∈ T, ∀ s ∈ S, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
T_eq : ∀ t ∈ T, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
t : Set α
ht : t ∈ T
u : Set α
hu : MeasurableSet u
⊢ Eq (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) ((ν.restrict t : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞)
Tactic: simp only [restrict_apply hu]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (hypothesis)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
hc : T.Countable
h_inter : IsPiSystem S
hU : ⋃₀ T = univ
htop : ∀ t ∈ T, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ST_eq :
  ∀ t ∈ T, ∀ s ∈ S, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
T_eq : ∀ t ∈ T, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
t : Set α
ht : t ∈ T
u_1 u : Set α
hu : MeasurableSet u
ihu : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (uᶜ ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (uᶜ ∩ t) : ℝ≥0∞)
have this : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: have := T_eq t ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
hc : T.Countable
h_inter : IsPiSystem S
hU : ⋃₀ T = univ
htop : ∀ t ∈ T, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ST_eq :
  ∀ t ∈ T, ∀ s ∈ S, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
T_eq : ∀ t ∈ T, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
t : Set α
ht : t ∈ T
u_1 u : Set α
hu : MeasurableSet u
ihu : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞)
this : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (uᶜ ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (uᶜ ∩ t) : ℝ≥0∞)
have h : ∀ (ihu : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞))
  (this : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ uᶜ) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t ∩ uᶜ) : ℝ≥0∞)
Tactic: rw [Set.inter_comm] at ihu ⊢
Cleared hypotheses: ihu, this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
hc : T.Countable
h_inter : IsPiSystem S
hU : ⋃₀ T = univ
htop : ∀ t ∈ T, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ST_eq :
  ∀ t ∈ T, ∀ s ∈ S, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
T_eq : ∀ t ∈ T, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
t : Set α
ht : t ∈ T
u_1 u : Set α
hu : MeasurableSet u
ihu : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
this : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ uᶜ) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t ∩ uᶜ) : ℝ≥0∞)
have h : ∀
  (this :
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (t \ u) : ℝ≥0∞) =
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
        ((ν : (a : Set α) → ℝ≥0∞) (t \ u) : ℝ≥0∞)),
  Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rwa [← measure_inter_add_diff t hu, ← measure_inter_add_diff t hu, ← ihu,
      ENNReal.add_right_inj] at this
Cleared hypotheses: this