awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
h : ∀ᵐ (x : α) ∂μ.restrict s, p x
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → p x
have simp : ∀ (h : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {a : α | ¬p a} : ℝ≥0∞) (0 : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(a ∈ s → p a)} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp only [ae_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hs : NullMeasurableSet s μ
⊢ (∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : α) ∂μ, x ∈ s → p x
have simp : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | p x}ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s → p x}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp only [ae_iff, ← compl_setOf, restrict_apply₀' hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hs : NullMeasurableSet s μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | p x}ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s → p x}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | p x}ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞) =
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s → p x}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [iff_iff_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hs : NullMeasurableSet s μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | p x}ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞) =
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s → p x}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
have e_a : ∀ (x : α), x ∈ {x : α | p x}ᶜ ∩ s ↔ Membership.mem (γ := Set α) {x : α | x ∈ s → p x}ᶜ x
Tactic: congr with x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
δ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
f g : α → δ
s : Set α
hfg : f =ᶠ[ae μ] g
⊢ f =ᶠ[ae (μ.restrict s)] g
have refine : ae (μ.restrict s) ≤ ae μ
Tactic: refine hfg.filter_mono ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
δ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
f g : α → δ
s : Set α
hfg : f =ᶠ[ae μ] g
⊢ ae (μ.restrict s) ≤ ae μ
have rw : μ.restrict s ≪ μ
Tactic: rw [Measure.ae_le_iff_absolutelyContinuous]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t : Set α
p : α → Prop
ht : ∀ᵐ (x : α) ∂μ.restrict t, p x
htc : ∀ᵐ (x : α) ∂μ.restrict tᶜ, p x
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) {x : α | ¬p x} : ℝ≥0∞)
      ((μ.restrict tᶜ : (a : Set α) → ℝ≥0∞) {x : α | ¬p x} : ℝ≥0∞) =
    0
have rw : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict tᶜ : (a : Set α) → ℝ≥0∞) {x : α | ¬p x} : ℝ≥0∞) = 0
Tactic: rw [ae_iff.1 ht, ae_iff.1 htc, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t : Set α
p : α → Prop
ht : ∀ᵐ (x : α) ∂μ.restrict t, p x
htc : ∀ᵐ (x : α) ∂μ.restrict tᶜ, p x
rw : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict tᶜ : (a : Set α) → ℝ≥0∞) {x : α | ¬p x} : ℝ≥0∞) = 0
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) {x : α | ¬p x} : ℝ≥0∞)
      ((μ.restrict tᶜ : (a : Set α) → ℝ≥0∞) {x : α | ¬p x} : ℝ≥0∞) =
    0
have rw₁ : HAdd.hAdd (α := ℝ≥0∞) 0 0 = 0
Tactic: rw [ae_iff.1 ht, ae_iff.1 htc, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t : Set α
p : α → Prop
ht : ∀ᵐ (x : α) ∂μ.restrict t, p x
htc : ∀ᵐ (x : α) ∂μ.restrict tᶜ, p x
rw : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict tᶜ : (a : Set α) → ℝ≥0∞) {x : α | ¬p x} : ℝ≥0∞) = 0
rw₁ : HAdd.hAdd (α := ℝ≥0∞) 0 0 = 0
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) {x : α | ¬p x} : ℝ≥0∞)
      ((μ.restrict tᶜ : (a : Set α) → ℝ≥0∞) {x : α | ¬p x} : ℝ≥0∞) =
    0
have rw₂ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [ae_iff.1 ht, ae_iff.1 htc, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
s : Set α
t : Set β
f : α → β
hs : MeasurableSet s
⊢ t ∈ Filter.map f (ae (μ.restrict s)) ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : f ⁻¹' t ∈ ae (μ.restrict s) ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [mem_map, mem_ae_iff, Measure.restrict_apply' hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
s : Set α
t : Set β
f : α → β
hs : MeasurableSet s
rw : f ⁻¹' t ∈ ae (μ.restrict s) ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ t ∈ Filter.map f (ae (μ.restrict s)) ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) (f ⁻¹' t)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [mem_map, mem_ae_iff, Measure.restrict_apply' hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
s : Set α
t : Set β
f : α → β
hs : MeasurableSet s
rw : f ⁻¹' t ∈ ae (μ.restrict s) ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) (f ⁻¹' t)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ t ∈ Filter.map f (ae (μ.restrict s)) ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((f ⁻¹' t)ᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [mem_map, mem_ae_iff, Measure.restrict_apply' hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
p : α → Prop
s : Finset ι
μ : ι → Measure α
⊢ (∀ᵐ (x : α) ∂∑ i ∈ s, μ i, p x) ↔ ∀ i ∈ s, ∀ᵐ (x : α) ∂μ i, p x
have empty : (∀ᵐ (x : α) ∂∑ i ∈ ∅, μ i, p x) ↔ ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ∀ᵐ (x : α) ∂μ i, p x
Tactic: induction s using Finset.cons_induction
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
p : α → Prop
s : Finset ι
μ : ι → Measure α
empty : (∀ᵐ (x : α) ∂∑ i ∈ ∅, μ i, p x) ↔ ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ∀ᵐ (x : α) ∂μ i, p x
⊢ (∀ᵐ (x : α) ∂∑ i ∈ s, μ i, p x) ↔ ∀ i ∈ s, ∀ᵐ (x : α) ∂μ i, p x
have cons : ∀ (a : ι) (s : Finset ι) (h : a ∉ s),
  ((∀ᵐ (x : α) ∂∑ i ∈ s, μ i, p x) ↔ ∀ i ∈ s, ∀ᵐ (x : α) ∂μ i, p x) →
    ((∀ᵐ (x : α) ∂∑ i ∈ Finset.cons a s h, μ i, p x) ↔ ∀ i ∈ Finset.cons a s h, ∀ᵐ (x : α) ∂μ i, p x)
Tactic: induction s using Finset.cons_induction
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : Group β
f g : α → β
⊢ f / g =ᶠ[ae μ] 1 ↔ f =ᶠ[ae μ] g
have refine_1 : ∀ (h : f / g =ᶠ[ae μ] 1) (x : α) (hx : (f / g) x = 1 x), f x = g x
Tactic: refine ⟨fun h ↦ h.mono fun x hx ↦ ?_, fun h ↦ h.mono fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : Group β
f g : α → β
refine_1 : ∀ (h : f / g =ᶠ[ae μ] 1) (x : α) (hx : (f / g) x = 1 x), f x = g x
⊢ f / g =ᶠ[ae μ] 1 ↔ f =ᶠ[ae μ] g
have refine_2 : ∀ (h : f =ᶠ[ae μ] g) (x : α) (hx : f x = g x), (f / g) x = 1 x
Tactic: refine ⟨fun h ↦ h.mono fun x hx ↦ ?_, fun h ↦ h.mono fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : Group β
f g : α → β
h : f / g =ᶠ[ae μ] 1
x : α
hx : (f / g) x = 1 x
⊢ f x = g x
have refine_1 : ∀ (hx : f x / g x = 1 x), f x = g x
Tactic: rwa [Pi.div_apply, Pi.one_apply, div_eq_one] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : Group β
f g : α → β
h : f / g =ᶠ[ae μ] 1
x : α
hx : (f / g) x = 1 x
refine_1 : ∀ (hx : f x / g x = 1 x), f x = g x
⊢ f x = g x
have refine_1₁ : ∀ (hx : f x / g x = 1), f x = g x
Tactic: rwa [Pi.div_apply, Pi.one_apply, div_eq_one] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : Group β
f g : α → β
h : f / g =ᶠ[ae μ] 1
x : α
hx : (f / g) x = 1 x
refine_1 : ∀ (hx : f x / g x = 1 x), f x = g x
refine_1₁ : ∀ (hx : f x / g x = 1), f x = g x
⊢ f x = g x
have refine_1₂ : ∀ (hx : f x = g x), f x = g x
Tactic: rwa [Pi.div_apply, Pi.one_apply, div_eq_one] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : Group β
f g : α → β
h : f =ᶠ[ae μ] g
x : α
hx : f x = g x
⊢ (f / g) x = 1 x
have refine_2 : f x / g x = 1 x
Tactic: rwa [Pi.div_apply, Pi.one_apply, div_eq_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : Group β
f g : α → β
h : f =ᶠ[ae μ] g
x : α
hx : f x = g x
refine_2 : f x / g x = 1 x
⊢ (f / g) x = 1 x
have refine_2₁ : f x / g x = 1
Tactic: rwa [Pi.div_apply, Pi.one_apply, div_eq_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : Group β
inst_1 : LE β
inst_2 : MulRightMono β
f g : α → β
⊢ 1 ≤ᶠ[ae μ] g / f ↔ f ≤ᶠ[ae μ] g
have refine_1 : ∀ (h : 1 ≤ᶠ[ae μ] g / f) (a : α) (ha : 1 a ≤ (g / f) a), f a ≤ g a
Tactic: refine ⟨fun h ↦ h.mono fun a ha ↦ ?_, fun h ↦ h.mono fun a ha ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : Group β
inst_1 : LE β
inst_2 : MulRightMono β
f g : α → β
refine_1 : ∀ (h : 1 ≤ᶠ[ae μ] g / f) (a : α) (ha : 1 a ≤ (g / f) a), f a ≤ g a
⊢ 1 ≤ᶠ[ae μ] g / f ↔ f ≤ᶠ[ae μ] g
have refine_2 : ∀ (h : f ≤ᶠ[ae μ] g) (a : α) (ha : f a ≤ g a), 1 a ≤ (g / f) a
Tactic: refine ⟨fun h ↦ h.mono fun a ha ↦ ?_, fun h ↦ h.mono fun a ha ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : Group β
inst_1 : LE β
inst_2 : MulRightMono β
f g : α → β
h : 1 ≤ᶠ[ae μ] g / f
a : α
ha : 1 a ≤ (g / f) a
⊢ f a ≤ g a
have refine_1 : ∀ (ha : 1 ≤ (g / f) a), f a ≤ g a
Tactic: rwa [Pi.one_apply, Pi.div_apply, one_le_div'] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : Group β
inst_1 : LE β
inst_2 : MulRightMono β
f g : α → β
h : 1 ≤ᶠ[ae μ] g / f
a : α
ha : 1 a ≤ (g / f) a
refine_1 : ∀ (ha : 1 ≤ (g / f) a), f a ≤ g a
⊢ f a ≤ g a
have refine_1₁ : ∀ (ha : 1 ≤ g a / f a), f a ≤ g a
Tactic: rwa [Pi.one_apply, Pi.div_apply, one_le_div'] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : Group β
inst_1 : LE β
inst_2 : MulRightMono β
f g : α → β
h : 1 ≤ᶠ[ae μ] g / f
a : α
ha : 1 a ≤ (g / f) a
refine_1 : ∀ (ha : 1 ≤ (g / f) a), f a ≤ g a
refine_1₁ : ∀ (ha : 1 ≤ g a / f a), f a ≤ g a
⊢ f a ≤ g a
have refine_1₂ : ∀ (ha : f a ≤ g a), f a ≤ g a
Tactic: rwa [Pi.one_apply, Pi.div_apply, one_le_div'] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : Group β
inst_1 : LE β
inst_2 : MulRightMono β
f g : α → β
h : f ≤ᶠ[ae μ] g
a : α
ha : f a ≤ g a
⊢ 1 a ≤ (g / f) a
have refine_2 : 1 ≤ (g / f) a
Tactic: rwa [Pi.one_apply, Pi.div_apply, one_le_div']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : Group β
inst_1 : LE β
inst_2 : MulRightMono β
f g : α → β
h : f ≤ᶠ[ae μ] g
a : α
ha : f a ≤ g a
refine_2 : 1 ≤ (g / f) a
⊢ 1 a ≤ (g / f) a
have refine_2₁ : 1 ≤ g a / f a
Tactic: rwa [Pi.one_apply, Pi.div_apply, one_le_div']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ ae (μ.restrict s) = ae μ ⊓ 𝓟 s
have h : ∀ (t : Set α), t ∈ ae (μ.restrict s) ↔ t ∈ ae μ ⊓ 𝓟 s
Tactic: ext t
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
⊢ t ∈ ae (μ.restrict s) ↔ t ∈ ae μ ⊓ 𝓟 s
have h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | a ∉ t ∧ a ∈ s} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp only [mem_inf_principal, mem_ae_iff, restrict_apply_eq_zero' hs, compl_setOf,
    Classical.not_imp, fun a => and_comm (a := a ∈ s) (b := a ∉ t)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ s ∈ ae (μ.restrict s)
have simp : ∃ t₁ ∈ ae μ, ∃ (t₂ : Set α), s ⊆ t₂ ∧ s = t₁ ∩ t₂
Tactic: simp only [ae_restrict_eq hs, mem_principal, mem_inf_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : f =ᶠ[ae (μ.restrict sᶜ)] fun (x : α) ↦ b
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ s) : ℝ≥0∞)
Tactic: rw [Measure.restrict_apply₀ (f_mble t_mble)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : f =ᶠ[ae (μ.restrict sᶜ)] fun (x : α) ↦ b
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ s) : ℝ≥0∞)
have rw : ∀ (hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({a : α | ¬f a = b} ∩ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)) {t : Set β}
  (t_mble : MeasurableSet t) (ht : b ∉ t),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ s) : ℝ≥0∞)
Tactic: rw [EventuallyEq, ae_iff, Measure.restrict_apply₀] at hs
Cleared hypotheses: hs, t, t_mble, ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : f =ᶠ[ae (μ.restrict sᶜ)] fun (x : α) ↦ b
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
rw :
  ∀ (hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({a : α | ¬f a = b} ∩ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)) {t : Set β}
    (t_mble : MeasurableSet t) (ht : b ∉ t),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ s) : ℝ≥0∞)
have rw₁ : ∀ (hs : Eq (α := ℝ≥0∞) ((μ.restrict sᶜ : (a : Set α) → ℝ≥0∞) {a : α | ¬f a = b} : ℝ≥0∞) (0 : ℝ≥0∞)) {t : Set β}
  (t_mble : MeasurableSet t) (ht : b ∉ t), NullMeasurableSet {a : α | ¬f a = b} (μ.restrict sᶜ)
Tactic: rw [EventuallyEq, ae_iff, Measure.restrict_apply₀] at hs
Cleared hypotheses: hs, t, t_mble, ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({a : α | ¬f a = b} ∩ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ s) : ℝ≥0∞)
have apply : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ s) : ℝ≥0∞)
Tactic: apply le_antisymm _ (measure_mono inter_subset_left)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({a : α | ¬f a = b} ∩ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ s) : ℝ≥0∞)
have apply : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ s ∪ f ⁻¹' t ∩ sᶜ) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ s) : ℝ≥0∞)
Tactic: apply (measure_mono (Eq.symm (inter_union_compl (f ⁻¹' t) s)).le).trans
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({a : α | ¬f a = b} ∩ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ s ∪ f ⁻¹' t ∩ sᶜ) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ s) : ℝ≥0∞)
have apply : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ sᶜ) : ℝ≥0∞) ≤
  (μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ s)
Tactic: apply (measure_union_le _ _).trans
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({a : α | ¬f a = b} ∩ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ s) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ sᶜ) : ℝ≥0∞) ≤
    (μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ s)
have suffices : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: suffices μ ((f ⁻¹' t) ∩ sᶜ) = 0 by simp [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({a : α | ¬f a = b} ∩ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ sᶜ) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) ({a : α | ¬f a = b} ∩ sᶜ) : ℝ≥0∞)
Tactic: rw [← nonpos_iff_eq_zero, ← hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({a : α | ¬f a = b} ∩ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t ∩ sᶜ) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ({a : α | ¬f a = b} ∩ sᶜ) : ℝ≥0∞)
have h : f ⁻¹' t ⊆ {a : α | ¬f a = b}
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
⊢ NullMeasurableSet t (μ.restrict s) ↔ NullMeasurableSet (t ∩ s) μ
have refine_1 : ∀ (h : NullMeasurableSet t (μ.restrict s)), NullMeasurableSet (t ∩ s) μ
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
refine_1 : ∀ (h : NullMeasurableSet t (μ.restrict s)), NullMeasurableSet (t ∩ s) μ
⊢ NullMeasurableSet t (μ.restrict s) ↔ NullMeasurableSet (t ∩ s) μ
have refine_2 : ∀ (h : NullMeasurableSet (t ∩ s) μ), NullMeasurableSet t (μ.restrict s)
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- 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 (μ.restrict s)
⊢ NullMeasurableSet (t ∩ s) μ
have refine_1 : ∀ (t' : Set α) (ht' : MeasurableSet t') (t't : t' =ᶠ[ae (μ.restrict s)] t), NullMeasurableSet (t ∩ s) μ
Tactic: obtain ⟨t', -, ht', t't⟩ : ∃ t' ⊇ t, MeasurableSet t' ∧ t' =ᵐ[μ.restrict s] t :=
      h.exists_measurable_superset_ae_eq
-- 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
⊢ t' ∩ s =ᶠ[ae μ] t ∩ s
have this : ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t') = (x ∈ t)
Tactic: have : ∀ᵐ x ∂μ, x ∈ s → (x ∈ t') = (x ∈ t) :=
        (ae_restrict_iff'₀ hs).1 t't
-- 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 (μ.restrict s)
t' : Set α
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
this : ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t') = (x ∈ t)
⊢ t' ∩ s =ᶠ[ae μ] t ∩ s
have h₁ : ∀ (y : α) (hy : y ∈ s → (y ∈ t') = (y ∈ t)), (t' ∩ s) y = (t ∩ s) y
Tactic: filter_upwards [this] with y hy
-- 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
⊢ NullMeasurableSet (t ∩ s) μ
have A : t' ∩ s =ᶠ[ae μ] t ∩ s
Tactic: have A : (t' ∩ s : Set α) =ᵐ[μ] (t ∩ s : Set α) := by
      have : ∀ᵐ x ∂μ, x ∈ s → (x ∈ t') = (x ∈ t) :=
        (ae_restrict_iff'₀ hs).1 t't
      filter_upwards [this] with y hy
      change (y ∈ t' ∩ s) = (y ∈ t ∩ s)
      simpa only [eq_iff_iff, mem_inter_iff, and_congr_left_iff] using hy
-- 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 (μ.restrict s)
t' : Set α
ht' : MeasurableSet t'
t't : t' =ᶠ[ae (μ.restrict s)] t
A : t' ∩ s =ᶠ[ae μ] t ∩ s
⊢ NullMeasurableSet (t ∩ s) μ
have refine_1 : ∀ (s' : Set α) (hs' : MeasurableSet s') (s's : s' =ᶠ[ae μ] s), NullMeasurableSet (t ∩ s) μ
Tactic: obtain ⟨s', -, hs', s's⟩ : ∃ s' ⊇ s, MeasurableSet s' ∧ s' =ᵐ[μ] s :=
      hs.exists_measurable_superset_ae_eq