awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (hypothesis)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
A : t' ∩ s =ᶠ[ae μ] t ∩ s
s' : Set α
hs' : MeasurableSet s'
s's : s' =ᶠ[ae μ] s
⊢ NullMeasurableSet (t ∩ s) μ
have B : t' ∩ s' =ᶠ[ae μ] t' ∩ s
Tactic: have B : (t' ∩ s' : Set α) =ᵐ[μ] (t' ∩ s : Set α) :=
      ae_eq_set_inter (EventuallyEq.refl _ _) s's
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet (t ∩ s) μ
⊢ NullMeasurableSet (t \ s) (μ.restrict s)
have h₁ : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: apply NullMeasurableSet.of_null
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet (t ∩ s) μ
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (0 : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [Measure.restrict_apply₀' hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (hypothesis)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet (t ∩ s) μ
⊢ NullMeasurableSet t (μ.restrict s)
have A : NullMeasurableSet (t \ s) (μ.restrict s)
Tactic: have A : NullMeasurableSet (t \ s) (μ.restrict s) := by
      apply NullMeasurableSet.of_null
      rw [Measure.restrict_apply₀' hs]
      simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (hypothesis)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet (t ∩ s) μ
A : NullMeasurableSet (t \ s) (μ.restrict s)
⊢ NullMeasurableSet t (μ.restrict s)
have B : NullMeasurableSet (t ∩ s) (μ.restrict s)
Tactic: have B : NullMeasurableSet (t ∩ s) (μ.restrict s) :=
      h.mono_ac absolutelyContinuous_restrict
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
⊢ NullMeasurableSet t (μ.restrict s) ↔ NullMeasurableSet t μ
have refine : ∀ (h : NullMeasurableSet t (μ.restrict s)), NullMeasurableSet t μ
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ h.mono_ac absolutelyContinuous_restrict⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
⊢ NullMeasurableSet t μ
have obtain : ∀ (t' : Set α) (t'_subs : t' ⊆ t) (ht' : MeasurableSet t') (t't : t' =ᶠ[ae (μ.restrict s)] t), NullMeasurableSet t μ
Tactic: obtain ⟨t', t'_subs, ht', t't⟩ : ∃ t' ⊆ t, MeasurableSet t' ∧ t' =ᵐ[μ.restrict s] t :=
    h.exists_measurable_subset_ae_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
t'_subs : t' ⊆ t
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t' ↔ x ∈ t)
have h₁ : ∀ᵐ (x : α) ∂μ.restrict s, x ∈ t' ↔ x ∈ t
Tactic: apply ae_imp_of_ae_restrict
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
t'_subs : t' ⊆ t
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
⊢ ∀ᵐ (x : α) ∂μ.restrict s, x ∈ t' ↔ x ∈ t
have h₁ : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ t' x = t x) x} x →
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ x ∈ t' ↔ x ∈ t) x} x}
    a
Tactic: filter_upwards [t't] with x hx using by simpa using hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
t'_subs : t' ⊆ t
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ t' x = t x) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ x ∈ t' ↔ x ∈ t) x} x}
      a
⊢ ∀ᵐ (x : α) ∂μ.restrict s, x ∈ t' ↔ x ∈ t
have h₂ : ∀ (a : α), t' a = t a → (a ∈ t' ↔ a ∈ t)
Tactic: filter_upwards [t't] with x hx using by simpa using hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (hypothesis)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
t'_subs : t' ⊆ t
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
⊢ NullMeasurableSet t μ
have this : ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t' ↔ x ∈ t)
Tactic: have : ∀ᵐ x ∂μ, x ∈ s → (x ∈ t' ↔ x ∈ t) := by
    apply ae_imp_of_ae_restrict
    filter_upwards [t't] with x hx using by simpa using hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
t'_subs : t' ⊆ t
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
this : ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t' ↔ x ∈ t)
⊢ t' =ᶠ[ae μ] t
have h₁ : ∀ (x : α) (hx : x ∈ s → (x ∈ t' ↔ x ∈ t)), t' x = t x
Tactic: filter_upwards [this] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
t'_subs : t' ⊆ t
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
this : ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t' ↔ x ∈ t)
x : α
hx : x ∈ s → (x ∈ t' ↔ x ∈ t)
⊢ t' x = t x
have h₁ : (x ∈ t') = (x ∈ t)
Tactic: change (x ∈ t') = (x ∈ t)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
t'_subs : t' ⊆ t
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
this : ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t' ↔ x ∈ t)
x : α
hx : x ∈ s → (x ∈ t' ↔ x ∈ t)
⊢ (x ∈ t') = (x ∈ t)
have h₁ : x ∈ t' ↔ x ∈ t
Tactic: simp only [eq_iff_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
t'_subs : t' ⊆ t
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
this : ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t' ↔ x ∈ t)
x : α
hx : x ∈ s → (x ∈ t' ↔ x ∈ t)
⊢ x ∈ t' ↔ x ∈ t
have h₁ : ∀ (hx : x ∉ s), x ∈ t' ↔ x ∈ t
Tactic: tauto
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
t'_subs : t' ⊆ t
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
this : ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t' ↔ x ∈ t)
x : α
hx : x ∈ s → (x ∈ t' ↔ x ∈ t)
h₁ : ∀ (hx : x ∉ s), x ∈ t' ↔ x ∈ t
⊢ x ∈ t' ↔ x ∈ t
have h₂ : ∀ (hx : x ∈ t' ↔ x ∈ t), x ∈ t' ↔ x ∈ t
Tactic: tauto
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
t'_subs : t' ⊆ t
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
this : ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t' ↔ x ∈ t)
x : α
hx : x ∈ s → (x ∈ t' ↔ x ∈ t)
h₁ : ∀ (hx : x ∉ s), x ∈ t' ↔ x ∈ t
h₂ : ∀ (hx : x ∈ t' ↔ x ∈ t), x ∈ t' ↔ x ∈ t
h₃ : ∀ (hx : x ∉ s), x ∈ t' ↔ x ∈ t
h₄ : ∀ (hx : x ∈ t' ↔ x ∈ t), x ∈ t' ↔ x ∈ t
⊢ x ∈ t' ↔ x ∈ t
have h₅ : ∀ (hx : x ∉ s), x ∈ t' → x ∈ t
Tactic: tauto
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
t'_subs : t' ⊆ t
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
this : ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t' ↔ x ∈ t)
x : α
hx : x ∈ s → (x ∈ t' ↔ x ∈ t)
h₁ : ∀ (hx : x ∉ s), x ∈ t' ↔ x ∈ t
h₂ : ∀ (hx : x ∈ t' ↔ x ∈ t), x ∈ t' ↔ x ∈ t
h₃ : ∀ (hx : x ∉ s), x ∈ t' ↔ x ∈ t
h₄ : ∀ (hx : x ∈ t' ↔ x ∈ t), x ∈ t' ↔ x ∈ t
h₅ : ∀ (hx : x ∉ s), x ∈ t' → x ∈ t
⊢ x ∈ t' ↔ x ∈ t
have h₆ : ∀ (hx : x ∉ s), x ∈ t → x ∈ t'
Tactic: tauto
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
t'_subs : t' ⊆ t
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
this : ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t' ↔ x ∈ t)
x : α
hx : x ∈ s → (x ∈ t' ↔ x ∈ t)
h₁ : ∀ (hx : x ∉ s), x ∈ t' ↔ x ∈ t
h₂ : ∀ (hx : x ∈ t' ↔ x ∈ t), x ∈ t' ↔ x ∈ t
h₃ : ∀ (hx : x ∉ s), x ∈ t' ↔ x ∈ t
h₄ : ∀ (hx : x ∈ t' ↔ x ∈ t), x ∈ t' ↔ x ∈ t
h₅ : ∀ (hx : x ∉ s), x ∈ t' → x ∈ t
h₆ : ∀ (hx : x ∉ s), x ∈ t → x ∈ t'
⊢ x ∈ t' ↔ x ∈ t
have h₇ : ∀ (hx : x ∈ t' ↔ x ∈ t), x ∈ t' → x ∈ t
Tactic: tauto
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
t'_subs : t' ⊆ t
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
this : ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t' ↔ x ∈ t)
x : α
hx : x ∈ s → (x ∈ t' ↔ x ∈ t)
h₁ : ∀ (hx : x ∉ s), x ∈ t' ↔ x ∈ t
h₂ : ∀ (hx : x ∈ t' ↔ x ∈ t), x ∈ t' ↔ x ∈ t
h₃ : ∀ (hx : x ∉ s), x ∈ t' ↔ x ∈ t
h₄ : ∀ (hx : x ∈ t' ↔ x ∈ t), x ∈ t' ↔ x ∈ t
h₅ : ∀ (hx : x ∉ s), x ∈ t' → x ∈ t
h₆ : ∀ (hx : x ∉ s), x ∈ t → x ∈ t'
h₇ : ∀ (hx : x ∈ t' ↔ x ∈ t), x ∈ t' → x ∈ t
⊢ x ∈ t' ↔ x ∈ t
have h₈ : ∀ (hx : x ∈ t' ↔ x ∈ t), x ∈ t → x ∈ t'
Tactic: tauto
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
t'_subs : t' ⊆ t
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
this : ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t' ↔ x ∈ t)
x : α
hx : x ∈ s → (x ∈ t' ↔ x ∈ t)
h₁ : ∀ (hx : x ∉ s), x ∈ t' ↔ x ∈ t
h₂ : ∀ (hx : x ∈ t' ↔ x ∈ t), x ∈ t' ↔ x ∈ t
h₃ : ∀ (hx : x ∉ s), x ∈ t' ↔ x ∈ t
h₄ : ∀ (hx : x ∈ t' ↔ x ∈ t), x ∈ t' ↔ x ∈ t
h₅ : ∀ (hx : x ∉ s), x ∈ t' → x ∈ t
h₆ : ∀ (hx : x ∉ s), x ∈ t → x ∈ t'
h₇ : ∀ (hx : x ∈ t' ↔ x ∈ t), x ∈ t' → x ∈ t
h₈ : ∀ (hx : x ∈ t' ↔ x ∈ t), x ∈ t → x ∈ t'
h₉ h₁₀ h₁₁ : ∀ (hx : x ∉ s), x ∈ t' → x ∈ t
h₁₂ h₁₃ h₁₄ : ∀ (hx : x ∉ s), x ∈ t → x ∈ t'
⊢ x ∈ t' ↔ x ∈ t
have h₁₅ : x ∈ t' → x ∈ t' → x ∈ t → x ∈ t
Tactic: tauto
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
t'_subs : t' ⊆ t
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
this : ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t' ↔ x ∈ t)
x : α
hx : x ∈ s → (x ∈ t' ↔ x ∈ t)
h₁ : ∀ (hx : x ∉ s), x ∈ t' ↔ x ∈ t
h₂ : ∀ (hx : x ∈ t' ↔ x ∈ t), x ∈ t' ↔ x ∈ t
h₃ : ∀ (hx : x ∉ s), x ∈ t' ↔ x ∈ t
h₄ : ∀ (hx : x ∈ t' ↔ x ∈ t), x ∈ t' ↔ x ∈ t
h₅ : ∀ (hx : x ∉ s), x ∈ t' → x ∈ t
h₆ : ∀ (hx : x ∉ s), x ∈ t → x ∈ t'
h₇ : ∀ (hx : x ∈ t' ↔ x ∈ t), x ∈ t' → x ∈ t
h₈ : ∀ (hx : x ∈ t' ↔ x ∈ t), x ∈ t → x ∈ t'
h₉ h₁₀ h₁₁ : ∀ (hx : x ∉ s), x ∈ t' → x ∈ t
h₁₂ h₁₃ h₁₄ : ∀ (hx : x ∉ s), x ∈ t → x ∈ t'
h₁₅ : x ∈ t' → x ∈ t' → x ∈ t → x ∈ t
⊢ x ∈ t' ↔ x ∈ t
have h₁₆ : x ∈ t' → x ∉ t' → x ∉ t → x ∈ t
Tactic: tauto
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
t'_subs : t' ⊆ t
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
this : ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t' ↔ x ∈ t)
x : α
hx : x ∈ s → (x ∈ t' ↔ x ∈ t)
h₁ : ∀ (hx : x ∉ s), x ∈ t' ↔ x ∈ t
h₂ : ∀ (hx : x ∈ t' ↔ x ∈ t), x ∈ t' ↔ x ∈ t
h₃ : ∀ (hx : x ∉ s), x ∈ t' ↔ x ∈ t
h₄ : ∀ (hx : x ∈ t' ↔ x ∈ t), x ∈ t' ↔ x ∈ t
h₅ : ∀ (hx : x ∉ s), x ∈ t' → x ∈ t
h₆ : ∀ (hx : x ∉ s), x ∈ t → x ∈ t'
h₇ : ∀ (hx : x ∈ t' ↔ x ∈ t), x ∈ t' → x ∈ t
h₈ : ∀ (hx : x ∈ t' ↔ x ∈ t), x ∈ t → x ∈ t'
h₉ h₁₀ h₁₁ : ∀ (hx : x ∉ s), x ∈ t' → x ∈ t
h₁₂ h₁₃ h₁₄ : ∀ (hx : x ∉ s), x ∈ t → x ∈ t'
h₁₅ : x ∈ t' → x ∈ t' → x ∈ t → x ∈ t
h₁₆ : x ∈ t' → x ∉ t' → x ∉ t → x ∈ t
h₁₇ h₁₈ : x ∈ t' → x ∈ t' → x ∈ t → x ∈ t
⊢ x ∈ t' ↔ x ∈ t
have h₁₉ : x ∈ t → x ∈ t' → x ∈ t → x ∈ t'
Tactic: tauto
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
t'_subs : t' ⊆ t
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
this : ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t' ↔ x ∈ t)
x : α
hx : x ∈ s → (x ∈ t' ↔ x ∈ t)
h₁ : ∀ (hx : x ∉ s), x ∈ t' ↔ x ∈ t
h₂ : ∀ (hx : x ∈ t' ↔ x ∈ t), x ∈ t' ↔ x ∈ t
h₃ : ∀ (hx : x ∉ s), x ∈ t' ↔ x ∈ t
h₄ : ∀ (hx : x ∈ t' ↔ x ∈ t), x ∈ t' ↔ x ∈ t
h₅ : ∀ (hx : x ∉ s), x ∈ t' → x ∈ t
h₆ : ∀ (hx : x ∉ s), x ∈ t → x ∈ t'
h₇ : ∀ (hx : x ∈ t' ↔ x ∈ t), x ∈ t' → x ∈ t
h₈ : ∀ (hx : x ∈ t' ↔ x ∈ t), x ∈ t → x ∈ t'
h₉ h₁₀ h₁₁ : ∀ (hx : x ∉ s), x ∈ t' → x ∈ t
h₁₂ h₁₃ h₁₄ : ∀ (hx : x ∉ s), x ∈ t → x ∈ t'
h₁₅ : x ∈ t' → x ∈ t' → x ∈ t → x ∈ t
h₁₆ : x ∈ t' → x ∉ t' → x ∉ t → x ∈ t
h₁₇ h₁₈ : x ∈ t' → x ∈ t' → x ∈ t → x ∈ t
h₁₉ : x ∈ t → x ∈ t' → x ∈ t → x ∈ t'
⊢ x ∈ t' ↔ x ∈ t
have h₂₀ : x ∈ t → x ∉ t' → x ∉ t → x ∈ t'
Tactic: tauto
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (hypothesis)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
t'_subs : t' ⊆ t
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
this : ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t' ↔ x ∈ t)
⊢ NullMeasurableSet t μ
have this₁ : t' =ᶠ[ae μ] t
Tactic: have : t' =ᵐ[μ] t := by
    filter_upwards [this] with x hx
    change (x ∈ t') = (x ∈ t)
    simp only [eq_iff_iff]
    tauto
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (hypothesis)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set (↑s : Type u_2)
hs : NullMeasurableSet s μ
ht : MeasurableSet t
⊢ NullMeasurableSet (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) μ
have ht₁ : MeasurableSet t
Tactic: rw [Subtype.instMeasurableSpace, comap_eq_generateFrom] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set (↑s : Type u_2)
hs : NullMeasurableSet s μ
t' : Set (↑s : Type u_2)
ht' :
  Membership.mem (γ := Set (Set (↑s : Type u_2)))
    {t : Set { x : α // x ∈ s } |
      ∃ (s_1 : Set α), MeasurableSet s_1 ∧ Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' s_1 = t}
    t'
ht : MeasurableSet t'
⊢ NullMeasurableSet (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t') μ
have hC : ∀ (s' : Set α) (hs' : MeasurableSet s'),
  MeasurableSet (α := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' s') →
    NullMeasurableSet
      (image (α := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
        (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' s'))
      μ
Tactic: obtain ⟨s', hs', rfl⟩ := ht'
Cleared hypotheses: t', ht', ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set (↑s : Type u_2)
hs : NullMeasurableSet s μ
s' : Set α
hs' : MeasurableSet s'
ht : MeasurableSet (α := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' s')
⊢ NullMeasurableSet
    (image (α := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' s'))
    μ
have hC : NullMeasurableSet (s ∩ s') μ
Tactic: rw [Subtype.image_preimage_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set (↑s : Type u_2)
hs : NullMeasurableSet s μ
t' : Set (↑s : Type u_2)
ht : MeasurableSet t'
ht' : NullMeasurableSet (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t') μ
⊢ NullMeasurableSet (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t'ᶜ) μ
have compl : NullMeasurableSet (s \ (fun (a : { x : α // x ∈ s }) ↦ (↑a : α)) '' t') μ
Tactic: simp only [← range_diff_image Subtype.coe_injective, Subtype.range_coe_subtype, setOf_mem_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set (↑s : Type u_2)
hs : NullMeasurableSet s μ
f : ℕ → Set (↑s : Type u_2)
hs_1 : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), NullMeasurableSet (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' f n) μ
⊢ NullMeasurableSet (image (α := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (⋃ (i : ℕ), f i)) μ
have iUnion : NullMeasurableSet (⋃ (i : ℕ), Subtype.val (p := fun (x : α) ↦ x ∈ s) '' f i) μ
Tactic: rw [image_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set (↑s : Type u_2)
hs : NullMeasurableSet s μ
ht : MeasurableSet t
⊢ NullMeasurableSet (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) μ
have hC : ∀ (t' : Set (↑s : Type u_2))
  (ht' :
    Membership.mem (γ := Set (Set (↑s : Type u_2)))
      {t : Set { x : α // x ∈ s } |
        ∃ (s_1 : Set α), MeasurableSet s_1 ∧ Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' s_1 = t}
      t'),
  MeasurableSet t' → NullMeasurableSet (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t') μ
Tactic: induction t, ht using generateFrom_induction with
  | hC t' ht' =>
    obtain ⟨s', hs', rfl⟩ := ht'
    rw [Subtype.image_preimage_coe]
    exact hs.inter (hs'.nullMeasurableSet)
  | empty => simp only [image_empty, nullMeasurableSet_empty]
  | compl t' _ ht' =>
    simp only [← range_diff_image Subtype.coe_injective, Subtype.range_coe_subtype, setOf_mem_eq]
    exact hs.diff ht'
  | iUnion f _ hf =>
    dsimp only []
    rw [image_iUnion]
    exact .iUnion hf
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set (↑s : Type u_2)
hs : NullMeasurableSet s μ
ht : MeasurableSet t
hC :
  ∀ (t' : Set (↑s : Type u_2))
    (ht' :
      Membership.mem (γ := Set (Set (↑s : Type u_2)))
        {t : Set { x : α // x ∈ s } |
          ∃ (s_1 : Set α), MeasurableSet s_1 ∧ Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' s_1 = t}
        t'),
    MeasurableSet t' → NullMeasurableSet (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t') μ
⊢ NullMeasurableSet (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) μ
have empty : NullMeasurableSet (image (α := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) ∅) μ
Tactic: induction t, ht using generateFrom_induction with
  | hC t' ht' =>
    obtain ⟨s', hs', rfl⟩ := ht'
    rw [Subtype.image_preimage_coe]
    exact hs.inter (hs'.nullMeasurableSet)
  | empty => simp only [image_empty, nullMeasurableSet_empty]
  | compl t' _ ht' =>
    simp only [← range_diff_image Subtype.coe_injective, Subtype.range_coe_subtype, setOf_mem_eq]
    exact hs.diff ht'
  | iUnion f _ hf =>
    dsimp only []
    rw [image_iUnion]
    exact .iUnion hf
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set (↑s : Type u_2)
hs : NullMeasurableSet s μ
ht : MeasurableSet t
hC :
  ∀ (t' : Set (↑s : Type u_2))
    (ht' :
      Membership.mem (γ := Set (Set (↑s : Type u_2)))
        {t : Set { x : α // x ∈ s } |
          ∃ (s_1 : Set α), MeasurableSet s_1 ∧ Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' s_1 = t}
        t'),
    MeasurableSet t' → NullMeasurableSet (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t') μ
empty : NullMeasurableSet (image (α := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) ∅) μ
⊢ NullMeasurableSet (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) μ
have compl : ∀ (t' : Set (↑s : Type u_2)),
  MeasurableSet t' →
    ∀ (ht' : NullMeasurableSet (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t') μ),
      NullMeasurableSet (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t'ᶜ) μ
Tactic: induction t, ht using generateFrom_induction with
  | hC t' ht' =>
    obtain ⟨s', hs', rfl⟩ := ht'
    rw [Subtype.image_preimage_coe]
    exact hs.inter (hs'.nullMeasurableSet)
  | empty => simp only [image_empty, nullMeasurableSet_empty]
  | compl t' _ ht' =>
    simp only [← range_diff_image Subtype.coe_injective, Subtype.range_coe_subtype, setOf_mem_eq]
    exact hs.diff ht'
  | iUnion f _ hf =>
    dsimp only []
    rw [image_iUnion]
    exact .iUnion hf
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set (↑s : Type u_2)
hs : NullMeasurableSet s μ
ht : MeasurableSet t
hC :
  ∀ (t' : Set (↑s : Type u_2))
    (ht' :
      Membership.mem (γ := Set (Set (↑s : Type u_2)))
        {t : Set { x : α // x ∈ s } |
          ∃ (s_1 : Set α), MeasurableSet s_1 ∧ Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' s_1 = t}
        t'),
    MeasurableSet t' → NullMeasurableSet (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t') μ
empty : NullMeasurableSet (image (α := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) ∅) μ
compl :
  ∀ (t' : Set (↑s : Type u_2)),
    MeasurableSet t' →
      ∀ (ht' : NullMeasurableSet (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t') μ),
        NullMeasurableSet (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t'ᶜ) μ
⊢ NullMeasurableSet (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) μ
have iUnion : ∀ (f : ℕ → Set (↑s : Type u_2)),
  (∀ (n : ℕ), MeasurableSet (f n)) →
    ∀ (hf : ∀ (n : ℕ), NullMeasurableSet (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' f n) μ),
      NullMeasurableSet (image (α := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (⋃ (i : ℕ), f i)) μ
Tactic: induction t, ht using generateFrom_induction with
  | hC t' ht' =>
    obtain ⟨s', hs', rfl⟩ := ht'
    rw [Subtype.image_preimage_coe]
    exact hs.inter (hs'.nullMeasurableSet)
  | empty => simp only [image_empty, nullMeasurableSet_empty]
  | compl t' _ ht' =>
    simp only [← range_diff_image Subtype.coe_injective, Subtype.range_coe_subtype, setOf_mem_eq]
    exact hs.diff ht'
  | iUnion f _ hf =>
    dsimp only []
    rw [image_iUnion]
    exact .iUnion hf
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
δ : Type u_4
u : Set δ
inst : MeasureSpace δ
hu : NullMeasurableSet u volume
⊢ Eq (α := ℝ≥0∞) (((volume : Measure (↑u : Type u_4)) : (a : Set (↑u : Type u_4)) → ℝ≥0∞) univ : ℝ≥0∞)
    (((volume : Measure δ) : (a : Set δ) → ℝ≥0∞) u : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞)
  (((volume : Measure δ) : (a : Set δ) → ℝ≥0∞)
      (image (α := { x : δ // x ∈ u }) (Subtype.val (p := fun (x : δ) ↦ x ∈ u)) univ) :
    ℝ≥0∞)
  (((volume : Measure δ) : (a : Set δ) → ℝ≥0∞) u : ℝ≥0∞)
Tactic: rw [Subtype.volume_def, comap_apply₀ _ _ _ _ MeasurableSet.univ.nullMeasurableSet]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
δ : Type u_4
u : Set δ
inst : MeasureSpace δ
hu : NullMeasurableSet u volume
rw :
  Eq (α := ℝ≥0∞)
    (((volume : Measure δ) : (a : Set δ) → ℝ≥0∞)
        (image (α := { x : δ // x ∈ u }) (Subtype.val (p := fun (x : δ) ↦ x ∈ u)) univ) :
      ℝ≥0∞)
    (((volume : Measure δ) : (a : Set δ) → ℝ≥0∞) u : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((volume : Measure (↑u : Type u_4)) : (a : Set (↑u : Type u_4)) → ℝ≥0∞) univ : ℝ≥0∞)
    (((volume : Measure δ) : (a : Set δ) → ℝ≥0∞) u : ℝ≥0∞)
have rw₁ : Injective.{u_4 + 1, u_4 + 1} (α := { x : δ // x ∈ u }) (Subtype.val (p := fun (x : δ) ↦ x ∈ u))
Tactic: rw [Subtype.volume_def, comap_apply₀ _ _ _ _ MeasurableSet.univ.nullMeasurableSet]