awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
this : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p
⊢ (∀ᵐ (x : ℝ) ∂μ.restrict (s \ u), p x) ∧ ∀ i ∈ A, ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ T i), p x
have left : ∀ᵐ (x : ℝ) ∂μ.restrict (s \ u), p x
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
this : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p
left : ∀ᵐ (x : ℝ) ∂μ.restrict (s \ u), p x
⊢ (∀ᵐ (x : ℝ) ∂μ.restrict (s \ u), p x) ∧ ∀ i ∈ A, ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ T i), p x
have right : ∀ i ∈ A, ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ T i), p x
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (hypothesis)
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
this : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict (s \ u), p x
have this₁ : μ.restrict (s \ u) = 0
Tactic: have : μ.restrict (s \ u) = 0 := by simp only [restrict_eq_zero, hfinite.measure_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
this : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p
a : ℝ
as : a ∈ s
b : ℝ
bs : b ∈ s
⊢ ∀ᵐ (x :
    ℝ) ∂μ.restrict (s ∩ T (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ s) a as, Subtype.mk (p := fun (x : ℝ) ↦ x ∈ s) b bs)), p x
have right : ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
Tactic: dsimp [T]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
this : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p
a : ℝ
as : a ∈ s
b : ℝ
bs : b ∈ s
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
have right : ∀ (hba : b ≤ a), ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
Tactic: rcases le_or_gt b a with (hba | hab)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
this : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p
a : ℝ
as : a ∈ s
b : ℝ
bs : b ∈ s
right : ∀ (hba : b ≤ a), ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
have right₁ : ∀ (hab : a < b), ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
Tactic: rcases le_or_gt b a with (hba | hab)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (hypothesis)
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∈ s → p x
have hfinite : (s \ u).Finite
Tactic: have hfinite : (s \ u).Finite := s.finite_diff_iUnion_Ioo'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∈ s → p x
have obtain : ∀ (A : Set ((↑s : Type) × (↑s : Type))) (A_count : A.Countable)
  (hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)), ∀ᵐ (x : ℝ) ∂μ, x ∈ s → p x
Tactic: obtain ⟨A, A_count, hA⟩ :
    ∃ A : Set (↥s × ↥s), A.Countable ∧ ⋃ i ∈ A, T i = ⋃ i : ↥s × ↥s, T i :=
    isOpen_iUnion_countable _ fun p => isOpen_Ioo
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (hypothesis)
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∈ s → p x
have M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u
Tactic: have M : ∀ᵐ x ∂μ, x ∉ s \ u := hfinite.countable.ae_notMem _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u
⊢ ∀ᵐ (x : ℝ) ∂μ, ∀ i ∈ A, x ∈ s ∩ T i → p x
have rw : ∀ (i : (↑s : Type) × (↑s : Type)) (hi : i ∈ A), ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ T i → p x
Tactic: rw [ae_ball_iff A_count]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u
a : ℝ
as : a ∈ s
b : ℝ
bs : b ∈ s
⊢ ∀ᵐ (x : ℝ) ∂μ,
    x ∈ s ∩ T (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ s) a as, Subtype.mk (p := fun (x : ℝ) ↦ x ∈ s) b bs) → p x
have change : ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
Tactic: change ∀ᵐ x : ℝ ∂μ, x ∈ s ∩ Ioo a b → p x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u
a : ℝ
as : a ∈ s
b : ℝ
bs : b ∈ s
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
have inl : ∀ (hba : b ≤ a), ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
Tactic: rcases le_or_gt b a with (hba | hab)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u
a : ℝ
as : a ∈ s
b : ℝ
bs : b ∈ s
inl : ∀ (hba : b ≤ a), ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
have inr : ∀ (hab : a < b), ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
Tactic: rcases le_or_gt b a with (hba | hab)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (hypothesis)
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∈ s → p x
have M' : ∀ᵐ (x : ℝ) ∂μ, ∀ i ∈ A, x ∈ s ∩ T i → p x
Tactic: have M' : ∀ᵐ x ∂μ, ∀ (i : ↥s × ↥s), i ∈ A → x ∈ s ∩ T i → p x := by
    rw [ae_ball_iff A_count]
    rintro ⟨⟨a, as⟩, ⟨b, bs⟩⟩ -
    change ∀ᵐ x : ℝ ∂μ, x ∈ s ∩ Ioo a b → p x
    rcases le_or_gt b a with (hba | hab)
    · simp only [Ioo_eq_empty_of_le hba, inter_empty, IsEmpty.forall_iff, eventually_true,
        mem_empty_iff_false]
    · exact h a b as bs hab
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u
M' : ∀ᵐ (x : ℝ) ∂μ, ∀ i ∈ A, x ∈ s ∩ T i → p x
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∈ s → p x
have h₁ : ∀ (x : ℝ) (hx : x ∉ s \ u) (h'x : ∀ i ∈ A, x ∈ s ∩ T i → p x), x ∈ s → p x
Tactic: filter_upwards [M, M'] with x hx h'x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u
M' : ∀ᵐ (x : ℝ) ∂μ, ∀ i ∈ A, x ∈ s ∩ T i → p x
x : ℝ
hx : x ∉ s \ u
h'x : ∀ i ∈ A, x ∈ s ∩ T i → p x
xs : x ∈ s
⊢ p x
have pos : ∀ (Hx : Membership.mem (γ := Set ℝ) (⋃ (i : (↑s : Type) × (↑s : Type)), T i) x), p x
Tactic: by_cases Hx : x ∈ ⋃ i : ↥s × ↥s, T i
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u
M' : ∀ᵐ (x : ℝ) ∂μ, ∀ i ∈ A, x ∈ s ∩ T i → p x
x : ℝ
hx : x ∉ s \ u
h'x : ∀ i ∈ A, x ∈ s ∩ T i → p x
xs : x ∈ s
pos : ∀ (Hx : Membership.mem (γ := Set ℝ) (⋃ (i : (↑s : Type) × (↑s : Type)), T i) x), p x
⊢ p x
have neg : ∀ (Hx : x ∉ ⋃ (i : (↑s : Type) × (↑s : Type)), T i), p x
Tactic: by_cases Hx : x ∈ ⋃ i : ↥s × ↥s, T i
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (hypothesis)
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u
M' : ∀ᵐ (x : ℝ) ∂μ, ∀ i ∈ A, x ∈ s ∩ T i → p x
x : ℝ
hx : x ∉ s \ u
h'x : ∀ i ∈ A, x ∈ s ∩ T i → p x
xs : x ∈ s
Hx : Membership.mem (γ := Set ℝ) (⋃ (i : (↑s : Type) × (↑s : Type)), T i) x
⊢ p x
have Hx₁ : Membership.mem (γ := Set ℝ) (⋃ i ∈ A, T i) x
Tactic: rw [← hA] at Hx
Cleared hypotheses: Hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u
M' : ∀ᵐ (x : ℝ) ∂μ, ∀ i ∈ A, x ∈ s ∩ T i → p x
x : ℝ
hx : x ∉ s \ u
h'x : ∀ i ∈ A, x ∈ s ∩ T i → p x
xs : x ∈ s
Hx : Membership.mem (γ := Set ℝ) (⋃ i ∈ A, T i) x
⊢ p x
have pos : ∀ (p_1 : (↑s : Type) × (↑s : Type)) (pA : p_1 ∈ A) (xp : x ∈ T p_1), p x
Tactic: obtain ⟨p, pA, xp⟩ : ∃ p : ↥s × ↥s, p ∈ A ∧ x ∈ T p := by
      simpa only [mem_iUnion, exists_prop, SetCoe.exists, exists_and_right] using Hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Complex (goal)
Goal:
⊢ MeasurePreserving (α := ℂ) (β := Fin 2 → ℝ) (⇑measurableEquivPi : (a : ℂ) → Fin 2 → ℝ) volume volume
have h : Eq (α := autoParam (Measure ℂ) MeasurePreserving._auto_1) volume
  (Measure.map (α := Fin 2 → ℝ) (⇑measurableEquivPi.symm : (a : Fin 2 → ℝ) → ℂ) volume)
Tactic: convert! (measurableEquivPi.symm.measurable.measurePreserving volume).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Complex (goal)
Goal:
⊢ Eq (α := autoParam (Measure ℂ) MeasurePreserving._auto_1) volume
    (Measure.map (α := Fin 2 → ℝ) (⇑measurableEquivPi.symm : (a : Fin 2 → ℝ) → ℂ) volume)
have h : Eq (α := autoParam (Measure ℂ) MeasurePreserving._auto_1)
  (Basis.map (Pi.basisFun ℝ (Fin 2))
      (↑(ContinuousLinearEquiv.symm basisOneI.equivFun.toContinuousLinearEquiv) : (Fin 2 → ℝ) ≃ₗ[ℝ] ℂ)).addHaar
  volume
Tactic: rw [← addHaarMeasure_eq_volume_pi, ← Basis.parallelepiped_basisFun, ← Basis.addHaar,
    measurableEquivPi, Homeomorph.toMeasurableEquiv_symm_coe,
    ContinuousLinearEquiv.coe_symm_toHomeomorph, Basis.map_addHaar, eq_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
⊢ Set.Nonempty (α := ℝ) (interior (Icc 0 1))
have simp_rw : Set.Nonempty (α := ℝ) (Ioo 0 1)
Tactic: simp_rw [interior_Icc, nonempty_Ioo, zero_lt_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
simp_rw : Set.Nonempty (α := ℝ) (Ioo 0 1)
⊢ Set.Nonempty (α := ℝ) (interior (Icc 0 1))
have simp_rw₁ : LT.lt (α := ℝ) 0 1
Tactic: simp_rw [interior_Icc, nonempty_Ioo, zero_lt_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
ι : Type u_1
inst : Fintype ι
⊢ (↑(parallelepiped (Pi.basisFun ℝ ι)) : Set (ι → ℝ)) = (↑(PositiveCompacts.piIcc01 ι) : Set (ι → ℝ))
have refine_1 : (↑(parallelepiped (Pi.basisFun ℝ ι)) : Set (ι → ℝ)) = uIcc (fun (i : ι) ↦ 0) fun (i : ι) ↦ 1
Tactic: refine Eq.trans ?_ ((uIcc_of_le ?_).trans (Set.pi_univ_Icc _ _).symm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
ι : Type u_1
inst : Fintype ι
refine_1 : (↑(parallelepiped (Pi.basisFun ℝ ι)) : Set (ι → ℝ)) = uIcc (fun (i : ι) ↦ 0) fun (i : ι) ↦ 1
⊢ (↑(parallelepiped (Pi.basisFun ℝ ι)) : Set (ι → ℝ)) = (↑(PositiveCompacts.piIcc01 ι) : Set (ι → ℝ))
have refine_2 : LE.le.{u_1} (α := ι → ℝ) (fun (i : ι) ↦ 0) fun (i : ι) ↦ 1
Tactic: refine Eq.trans ?_ ((uIcc_of_le ?_).trans (Set.pi_univ_Icc _ _).symm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
ι : Type u_1
E : Type u_2
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : Basis ι ℝ E
⊢ b.parallelepiped = PositiveCompacts.map (⇑b.equivFun.symm : (a : ι → ℝ) → E) ⋯ ⋯ (PositiveCompacts.piIcc01 ι)
have rw : b.parallelepiped = (Basis.map (Pi.basisFun ℝ ι) b.equivFun.symm).parallelepiped
Tactic: rw [← Basis.parallelepiped_basisFun, ← Basis.parallelepiped_map]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
ι : Type u_1
E : Type u_2
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : Basis ι ℝ E
⊢ b.parallelepiped = (Basis.map (Pi.basisFun ℝ ι) b.equivFun.symm).parallelepiped
have e_b : ∀ (x : ι),
  Eq.{u_2 + 1} (α := E) ((b : (a : ι) → E) x : E) ((Basis.map (Pi.basisFun ℝ ι) b.equivFun.symm : (a : ι) → E) x : E)
Tactic: congr with x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
ι : Type u_1
E : Type u_2
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : Basis ι ℝ E
⊢ b.parallelepiped = PositiveCompacts.map (⇑b.equivFun.symm : (a : ι → ℝ) → E) ⋯ ⋯ (PositiveCompacts.piIcc01 ι)
have rw : b.parallelepiped = PositiveCompacts.map (⇑b.equivFun.symm : (a : ι → ℝ) → E) sorry sorry (parallelepiped (Pi.basisFun ℝ ι))
Tactic: classical
  rw [← Basis.parallelepiped_basisFun, ← Basis.parallelepiped_map]
  congr with x
  simp [Pi.single_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
ι : Type u_1
E : Type u_2
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : Basis ι ℝ E
rw : b.parallelepiped = PositiveCompacts.map (⇑b.equivFun.symm : (a : ι → ℝ) → E) ⋯ ⋯ (parallelepiped (Pi.basisFun ℝ ι))
⊢ b.parallelepiped = PositiveCompacts.map (⇑b.equivFun.symm : (a : ι → ℝ) → E) ⋯ ⋯ (PositiveCompacts.piIcc01 ι)
have rw₁ : b.parallelepiped = (Basis.map (Pi.basisFun ℝ ι) b.equivFun.symm).parallelepiped
Tactic: classical
  rw [← Basis.parallelepiped_basisFun, ← Basis.parallelepiped_map]
  congr with x
  simp [Pi.single_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
ι : Type u_1
E : Type u_2
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : Basis ι ℝ E
rw : b.parallelepiped = PositiveCompacts.map (⇑b.equivFun.symm : (a : ι → ℝ) → E) ⋯ ⋯ (parallelepiped (Pi.basisFun ℝ ι))
rw₁ rw₂ rw₃ : b.parallelepiped = (Basis.map (Pi.basisFun ℝ ι) b.equivFun.symm).parallelepiped
⊢ b.parallelepiped = PositiveCompacts.map (⇑b.equivFun.symm : (a : ι → ℝ) → E) ⋯ ⋯ (PositiveCompacts.piIcc01 ι)
have e_b : ∀ (x : ι),
  Eq.{u_2 + 1} (α := E) ((b : (a : ι) → E) x : E) ((Basis.map (Pi.basisFun ℝ ι) b.equivFun.symm : (a : ι) → E) x : E)
Tactic: classical
  rw [← Basis.parallelepiped_basisFun, ← Basis.parallelepiped_map]
  congr with x
  simp [Pi.single_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
ι : Type u_1
E : Type u_2
F : Type u_3
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ F
inst_5 : MeasurableSpace E
inst_6 : MeasurableSpace F
inst_7 : BorelSpace E
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : SigmaCompactSpace F
b : Basis ι ℝ E
f : E ≃L[ℝ] F
⊢ Eq (α := Measure F) (Measure.map (⇑f : (a : E) → F) b.addHaar) (b.map (↑f : E ≃ₗ[ℝ] F)).addHaar
have rw : Eq (α := ℝ≥0∞)
  (((b.addHaar : Measure E) : (a : Set E) → ℝ≥0∞)
      (preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F)
        (_root_.parallelepiped.{u_1, u_3} (ι := ι)
          (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := E) (⇑(↑f : E ≃ₗ[ℝ] F) : (a : E) → F) (⇑b : (a : ι) → E)))) :
    ℝ≥0∞)
  (1 : ℝ≥0∞)
Tactic: rw [eq_comm, Basis.addHaar_eq_iff, Measure.map_apply f.continuous.measurable
    (PositiveCompacts.isCompact _).measurableSet, Basis.coe_parallelepiped, Basis.coe_map]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
ι : Type u_1
E : Type u_2
F : Type u_3
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ F
inst_5 : MeasurableSpace E
inst_6 : MeasurableSpace F
inst_7 : BorelSpace E
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : SigmaCompactSpace F
b : Basis ι ℝ E
f : E ≃L[ℝ] F
⊢ Eq (α := ℝ≥0∞)
    (((b.addHaar : Measure E) : (a : Set E) → ℝ≥0∞)
        (preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F)
          (_root_.parallelepiped.{u_1, u_3} (ι := ι)
            (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := E) (⇑(↑f : E ≃ₗ[ℝ] F) : (a : E) → F)
              (⇑b : (a : ι) → E)))) :
      ℝ≥0∞)
    (1 : ℝ≥0∞)
have erw : Eq (α := ℝ≥0∞)
  (((b.addHaar : Measure E) : (a : Set E) → ℝ≥0∞)
      (preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F)
        (image.{u_2, u_3} (α := E) (⇑(↑(↑f : E ≃ₗ[ℝ] F) : E →ₗ[ℝ] F) : (a : E) → F)
          (_root_.parallelepiped.{u_1, u_2} (ι := ι) (⇑b : (a : ι) → E)))) :
    ℝ≥0∞)
  (1 : ℝ≥0∞)
Tactic: erw [← image_parallelepiped, f.toEquiv.preimage_image, addHaar_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
ι : Type u_1
E : Type u_2
F : Type u_3
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ F
inst_5 : MeasurableSpace E
inst_6 : MeasurableSpace F
inst_7 : BorelSpace E
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : SigmaCompactSpace F
b : Basis ι ℝ E
f : E ≃L[ℝ] F
erw :
  Eq (α := ℝ≥0∞)
    (((b.addHaar : Measure E) : (a : Set E) → ℝ≥0∞)
        (preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F)
          (image.{u_2, u_3} (α := E) (⇑(↑(↑f : E ≃ₗ[ℝ] F) : E →ₗ[ℝ] F) : (a : E) → F)
            (_root_.parallelepiped.{u_1, u_2} (ι := ι) (⇑b : (a : ι) → E)))) :
      ℝ≥0∞)
    (1 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((b.addHaar : Measure E) : (a : Set E) → ℝ≥0∞)
        (preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F)
          (_root_.parallelepiped.{u_1, u_3} (ι := ι)
            (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := E) (⇑(↑f : E ≃ₗ[ℝ] F) : (a : E) → F)
              (⇑b : (a : ι) → E)))) :
      ℝ≥0∞)
    (1 : ℝ≥0∞)
have erw₁ : Eq (α := ℝ≥0∞)
  (((b.addHaar : Measure E) : (a : Set E) → ℝ≥0∞) (_root_.parallelepiped.{u_1, u_2} (ι := ι) (⇑b : (a : ι) → E)) : ℝ≥0∞)
  (1 : ℝ≥0∞)
Tactic: erw [← image_parallelepiped, f.toEquiv.preimage_image, addHaar_self]