awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
inst : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s_1 s₁ s₂ t : Set α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
s : Set α
hs : MeasurableSet s
rw : (inducedOuterMeasure (P := MeasurableSet) m ⋯ m0 : (a : Set α) → ℝ≥0∞) s ≤ m s hs
⊢ ((inducedOuterMeasure (P := MeasurableSet) m ⋯ m0).trim : (a : Set α) → ℝ≥0∞) s ≤ m s hs
have rw₁ : m s hs ≤ m s hs
Tactic: rw [OuterMeasure.trim_eq _ hs, inducedOuterMeasure_eq m0 mU hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ₁ μ₂ : Measure α
h :
  ∀ (s : Set α),
    MeasurableSet s → Eq (α := ℝ≥0∞) ((μ₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ₁.toOuterMeasure = μ₂.toOuterMeasure
have rw : μ₁.trim = μ₂.toOuterMeasure
Tactic: rw [← trimmed, OuterMeasure.trim_congr (h _), trimmed]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ₁ μ₂ : Measure α
h :
  ∀ (s : Set α),
    MeasurableSet s → Eq (α := ℝ≥0∞) ((μ₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rw : μ₁.trim = μ₂.toOuterMeasure
⊢ μ₁.toOuterMeasure = μ₂.toOuterMeasure
have rw₁ : μ₂.trim = μ₂.toOuterMeasure
Tactic: rw [← trimmed, OuterMeasure.trim_congr (h _), trimmed]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ₁ μ₂ : Measure α
h :
  ∀ (s : Set α),
    MeasurableSet s → Eq (α := ℝ≥0∞) ((μ₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rw : μ₁.trim = μ₂.toOuterMeasure
rw₁ : μ₂.trim = μ₂.toOuterMeasure
⊢ μ₁.toOuterMeasure = μ₂.toOuterMeasure
have rw₂ : μ₂.toOuterMeasure = μ₂.toOuterMeasure
Tactic: rw [← trimmed, OuterMeasure.trim_congr (h _), trimmed]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [μ.trimmed, μ.coe_toOuterMeasure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [μ.trimmed, μ.coe_toOuterMeasure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
  (⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [measure_eq_trim, OuterMeasure.trim_eq_iInf, μ.coe_toOuterMeasure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
rw :
  Eq (α := ℝ≥0∞) ((μ.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) (⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (μ.toOuterMeasure : (a : Set α) → ℝ≥0∞) t)
  (⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (μ : (a : Set α) → ℝ≥0∞) t)
Tactic: rw [measure_eq_trim, OuterMeasure.trim_eq_iInf, μ.coe_toOuterMeasure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
rw :
  Eq (α := ℝ≥0∞) ((μ.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) (⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (μ.toOuterMeasure : (a : Set α) → ℝ≥0∞) t)
    (⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (μ : (a : Set α) → ℝ≥0∞) t)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) (⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (μ : (a : Set α) → ℝ≥0∞) t)
  (⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (μ : (a : Set α) → ℝ≥0∞) t)
Tactic: rw [measure_eq_trim, OuterMeasure.trim_eq_iInf, μ.coe_toOuterMeasure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (t : { t : Set α // s ⊆ t ∧ MeasurableSet t }), (μ : (a : Set α) → ℝ≥0∞) (↑t : Set α) : ℝ≥0∞)
have simp_rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
  (⨅ (i : Set α), ⨅ (_ : s ⊆ i ∧ MeasurableSet i), (μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)
Tactic: simp_rw [iInf_subtype, iInf_and, ← measure_eq_iInf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
simp_rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (i : Set α), ⨅ (_ : s ⊆ i ∧ MeasurableSet i), (μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (t : { t : Set α // s ⊆ t ∧ MeasurableSet t }), (μ : (a : Set α) → ℝ≥0∞) (↑t : Set α) : ℝ≥0∞)
have simp_rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
  (⨅ (i : Set α), ⨅ (_ : s ⊆ i), ⨅ (_ : MeasurableSet i), (μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)
Tactic: simp_rw [iInf_subtype, iInf_and, ← measure_eq_iInf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Finite
hfin : ∀ i ∈ s, LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ s, f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
have h : Eq (α := β → Set α) (fun (i : β) ↦ ⋃ (_ : i ∈ s), f i) fun (i : β) ↦ ⋃ (_ : i ∈ hs.toFinset (s := s)), f i
Tactic: convert! (measure_biUnion_finset_le (μ := μ) hs.toFinset f).trans_lt _ using 3
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Finite
hfin : ∀ i ∈ s, LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
h : Eq (α := β → Set α) (fun (i : β) ↦ ⋃ (_ : i ∈ s), f i) fun (i : β) ↦ ⋃ (_ : i ∈ hs.toFinset (s := s)), f i
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ s, f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
have convert_2 : LT.lt (α := ℝ≥0∞) (∑ i ∈ hs.toFinset (s := s), (μ : (a : Set α) → ℝ≥0∞) (f i)) ∞
Tactic: convert! (measure_biUnion_finset_le (μ := μ) hs.toFinset f).trans_lt _ using 3
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Finite
hfin : ∀ i ∈ s, LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := β → Set α) (fun (i : β) ↦ ⋃ (_ : i ∈ s), f i) fun (i : β) ↦ ⋃ (_ : i ∈ hs.toFinset (s := s)), f i
have h : ∀ (x : β) (x_1 : α),
  Membership.mem (γ := Set α) (⋃ (_ : x ∈ s), f x) x_1 ↔
    Membership.mem (γ := Set α) (⋃ (_ : x ∈ hs.toFinset (s := s)), f x) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Finite
hfin : ∀ i ∈ s, LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
x : β
x_1 : α
⊢ Membership.mem (γ := Set α) (⋃ (_ : x ∈ s), f x) x_1 ↔
    Membership.mem (γ := Set α) (⋃ (_ : x ∈ hs.toFinset (s := s)), f x) x_1
have h : Membership.mem (γ := Set α) (⋃ (_ : x ∈ s), f x) x_1 ↔ Membership.mem (γ := Set α) (⋃ (_ : x ∈ s), f x) x_1
Tactic: rw [Finite.mem_toFinset]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s t : Set α
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) (∞ : ℝ≥0∞) ↔
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
have refine_1 : ∀ (h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) (∞ : ℝ≥0∞)),
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine ⟨fun h => ⟨?_, ?_⟩, fun h => measure_union_lt_top h.1 h.2⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s t : Set α
refine_1 :
  ∀ (h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) (∞ : ℝ≥0∞)),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) (∞ : ℝ≥0∞) ↔
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
have refine_2 : ∀ (h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) (∞ : ℝ≥0∞)),
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine ⟨fun h => ⟨?_, ?_⟩, fun h => measure_union_lt_top h.1 h.2⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
ι : Sort u_5
inst : MeasurableSpace α
μ : Measure α
inst_1 : Countable ι
s : ι → Set α
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ι), s n) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ (n : ι), LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞)
have contrapose! : ∀ (hs : ∀ (n : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (0 : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ι), s n) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: contrapose! hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_6
β : Type u_7
inst : MeasurableSpace β
μ : Measure β
C : β → Set α → Prop
s : Set (Set α)
m : MeasurableSpace α
h_eq : m = generateFrom s
h_inter : IsPiSystem s
h_empty : ∀ᵐ (x : β) ∂μ, C x ∅
h_basic : ∀ᵐ (x : β) ∂μ, ∀ t ∈ s, C x t
h_compl : ∀ᵐ (x : β) ∂μ, ∀ (t : Set α), MeasurableSet t → C x t → C x tᶜ
h_union :
  ∀ᵐ (x : β) ∂μ,
    ∀ (f : ℕ → Set α),
      Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C x (f i)) → C x (⋃ (i : ℕ), f i)
⊢ ∀ᵐ (x : β) ∂μ, ∀ ⦃t : Set α⦄, MeasurableSet t → C x t
have h : ∀ (a : β),
  Membership.mem (γ := Set β)
    {x : β |
      Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ C x ∅) x} x →
        Membership.mem (γ := Set β)
          {x : β |
            Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ ∀ t ∈ s, C x t) x} x →
              Membership.mem (γ := Set β)
                {x : β |
                  Membership.mem (γ := Set β)
                      {x : β | (fun (x : β) ↦ ∀ (t : Set α), MeasurableSet t → C x t → C x tᶜ) x} x →
                    Membership.mem (γ := Set β)
                      {x : β |
                        Membership.mem (γ := Set β)
                            {x : β |
                              (fun (x : β) ↦
                                  ∀ (f : ℕ → Set α),
                                    Pairwise (Disjoint on f) →
                                      (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C x (f i)) → C x (⋃ (i : ℕ), f i))
                                x}
                            x →
                          Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ ∀ ⦃t : Set α⦄, MeasurableSet t → C x t) x}
                            x}
                      x}
                x}
          x}
    a
Tactic: filter_upwards [h_empty, h_basic, h_compl, h_union] with x hx_empty hx_basic hx_compl hx_union
    using MeasurableSpace.induction_on_inter (C := fun t _ ↦ C x t)
      h_eq h_inter hx_empty hx_basic hx_compl hx_union
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_6
β : Type u_7
inst : MeasurableSpace β
μ : Measure β
C : β → Set α → Prop
s : Set (Set α)
m : MeasurableSpace α
h_eq : m = generateFrom s
h_inter : IsPiSystem s
h_empty : ∀ᵐ (x : β) ∂μ, C x ∅
h_basic : ∀ᵐ (x : β) ∂μ, ∀ t ∈ s, C x t
h_compl : ∀ᵐ (x : β) ∂μ, ∀ (t : Set α), MeasurableSet t → C x t → C x tᶜ
h_union :
  ∀ᵐ (x : β) ∂μ,
    ∀ (f : ℕ → Set α),
      Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C x (f i)) → C x (⋃ (i : ℕ), f i)
h :
  ∀ (a : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ C x ∅) x} x →
          Membership.mem (γ := Set β)
            {x : β |
              Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ ∀ t ∈ s, C x t) x} x →
                Membership.mem (γ := Set β)
                  {x : β |
                    Membership.mem (γ := Set β)
                        {x : β | (fun (x : β) ↦ ∀ (t : Set α), MeasurableSet t → C x t → C x tᶜ) x} x →
                      Membership.mem (γ := Set β)
                        {x : β |
                          Membership.mem (γ := Set β)
                              {x : β |
                                (fun (x : β) ↦
                                    ∀ (f : ℕ → Set α),
                                      Pairwise (Disjoint on f) →
                                        (∀ (i : ℕ), MeasurableSet (f i)) →
                                          (∀ (i : ℕ), C x (f i)) → C x (⋃ (i : ℕ), f i))
                                  x}
                              x →
                            Membership.mem (γ := Set β)
                              {x : β | (fun (x : β) ↦ ∀ ⦃t : Set α⦄, MeasurableSet t → C x t) x} x}
                        x}
                  x}
            x}
      a
⊢ ∀ᵐ (x : β) ∂μ, ∀ ⦃t : Set α⦄, MeasurableSet t → C x t
have h₁ : ∀ (a : β),
  C a ∅ →
    (∀ t ∈ s, C a t) →
      (∀ (t : Set α), MeasurableSet t → C a t → C a tᶜ) →
        (∀ (f : ℕ → Set α),
            Pairwise (Disjoint on f) →
              (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C a (f i)) → C a (⋃ (i : ℕ), f i)) →
          ∀ ⦃t : Set α⦄, MeasurableSet t → C a t
Tactic: filter_upwards [h_empty, h_basic, h_compl, h_union] with x hx_empty hx_basic hx_compl hx_union
    using MeasurableSpace.induction_on_inter (C := fun t _ ↦ C x t)
      h_eq h_inter hx_empty hx_basic hx_compl hx_union
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
⊢ s ⊆ toMeasurable μ s
have rw : s ⊆
  if h : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s then
    h.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s)
  else
    if h' :
        ∃ t ⊇ s,
          MeasurableSet t ∧
            ∀ (u : Set α),
              MeasurableSet u →
                Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞) then
      h'.choose (p := fun (t : Set α) ↦
        t ⊇ s ∧
          MeasurableSet t ∧
            ∀ (u : Set α),
              MeasurableSet u →
                Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞))
    else
      sorry.choose (p := fun (t : Set α) ↦
        s ⊆ t ∧
          MeasurableSet t ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
Tactic: rw [toMeasurable_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
⊢ s ⊆
    if h : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s then
      h.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s)
    else
      if h' :
          ∃ t ⊇ s,
            MeasurableSet t ∧
              ∀ (u : Set α),
                MeasurableSet u →
                  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
                    ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞) then
        h'.choose (p := fun (t : Set α) ↦
          t ⊇ s ∧
            MeasurableSet t ∧
              ∀ (u : Set α),
                MeasurableSet u →
                  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞))
      else
        ⋯.choose (p := fun (t : Set α) ↦
          s ⊆ t ∧
            MeasurableSet t ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
have pos : ∀ (hs : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s),
  s ⊆ hs.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s)
Tactic: split_ifs with hs h's
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
pos :
  ∀ (hs : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s),
    s ⊆ hs.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s)
⊢ s ⊆
    if h : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s then
      h.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s)
    else
      if h' :
          ∃ t ⊇ s,
            MeasurableSet t ∧
              ∀ (u : Set α),
                MeasurableSet u →
                  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
                    ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞) then
        h'.choose (p := fun (t : Set α) ↦
          t ⊇ s ∧
            MeasurableSet t ∧
              ∀ (u : Set α),
                MeasurableSet u →
                  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞))
      else
        ⋯.choose (p := fun (t : Set α) ↦
          s ⊆ t ∧
            MeasurableSet t ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
have pos₁ : ∀ (hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s)
  (h's :
    ∃ t ⊇ s,
      MeasurableSet t ∧
        ∀ (u : Set α),
          MeasurableSet u →
            Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞)),
  s ⊆
    h's.choose (p := fun (t : Set α) ↦
      t ⊇ s ∧
        MeasurableSet t ∧
          ∀ (u : Set α),
            MeasurableSet u →
              Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞))
Tactic: split_ifs with hs h's
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
pos :
  ∀ (hs : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s),
    s ⊆ hs.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s)
pos₁ :
  ∀ (hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s)
    (h's :
      ∃ t ⊇ s,
        MeasurableSet t ∧
          ∀ (u : Set α),
            MeasurableSet u →
              Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞)),
    s ⊆
      h's.choose (p := fun (t : Set α) ↦
        t ⊇ s ∧
          MeasurableSet t ∧
            ∀ (u : Set α),
              MeasurableSet u →
                Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞))
⊢ s ⊆
    if h : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s then
      h.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s)
    else
      if h' :
          ∃ t ⊇ s,
            MeasurableSet t ∧
              ∀ (u : Set α),
                MeasurableSet u →
                  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
                    ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞) then
        h'.choose (p := fun (t : Set α) ↦
          t ⊇ s ∧
            MeasurableSet t ∧
              ∀ (u : Set α),
                MeasurableSet u →
                  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞))
      else
        ⋯.choose (p := fun (t : Set α) ↦
          s ⊆ t ∧
            MeasurableSet t ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
have neg : ∀ (hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s)
  (h's :
    ¬∃ t ⊇ s,
        MeasurableSet t ∧
          ∀ (u : Set α),
            MeasurableSet u →
              Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞)),
  s ⊆
    sorry.choose (p := fun (t : Set α) ↦
      s ⊆ t ∧ MeasurableSet t ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
Tactic: split_ifs with hs h's
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
⊢ MeasurableSet (toMeasurable μ s)
have rw : MeasurableSet.{u_1} (α := α)
  (if h : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s then
    h.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s)
  else
    if h' :
        ∃ t ⊇ s,
          MeasurableSet t ∧
            ∀ (u : Set α),
              MeasurableSet u →
                Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞) then
      h'.choose (p := fun (t : Set α) ↦
        t ⊇ s ∧
          MeasurableSet t ∧
            ∀ (u : Set α),
              MeasurableSet u →
                Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞))
    else
      sorry.choose (p := fun (t : Set α) ↦
        s ⊆ t ∧
          MeasurableSet t ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)))
Tactic: rw [toMeasurable_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
⊢ MeasurableSet.{u_1} (α := α)
    (if h : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s then
      h.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s)
    else
      if h' :
          ∃ t ⊇ s,
            MeasurableSet t ∧
              ∀ (u : Set α),
                MeasurableSet u →
                  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
                    ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞) then
        h'.choose (p := fun (t : Set α) ↦
          t ⊇ s ∧
            MeasurableSet t ∧
              ∀ (u : Set α),
                MeasurableSet u →
                  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞))
      else
        ⋯.choose (p := fun (t : Set α) ↦
          s ⊆ t ∧
            MeasurableSet t ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)))
have pos : ∀ (hs : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s),
  MeasurableSet (hs.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s))
Tactic: split_ifs with hs h's