awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : SigmaFinite μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
h0 : NeZero μ
hf' : AEMeasurable f μ
x : α
hx : (μ.tilted f).rnDeriv μ x = ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
⊢ log ((μ.tilted f).rnDeriv μ x).toReal = f x - log (∫ (x : α), rexp (f x) ∂μ)
have h : Ne (α := ℝ) (∫ (x : α), rexp (f x) ∂μ) 0
Tactic: rw [hx, ENNReal.toReal_ofReal (by positivity), log_div (exp_pos _).ne', log_exp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : SigmaFinite μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ log ((μ.tilted f).rnDeriv μ x).toReal) fun (x : α) ↦
    f x - log (∫ (x : α), rexp (f x) ∂μ)
have x : μ = 0 ∨ NeZero μ
Tactic: cases eq_zero_or_neZero μ with
  | inl h => simp_rw [h, ae_zero, Filter.EventuallyEq]; exact Filter.eventually_bot
  | inr h0 =>
    have hf' : AEMeasurable f μ := aemeasurable_of_aemeasurable_exp hf.1.aemeasurable
    filter_upwards [rnDeriv_tilted_left_self hf'] with x hx
    rw [hx, ENNReal.toReal_ofReal (by positivity), log_div (exp_pos _).ne', log_exp]
    exact (integral_exp_pos hf).ne'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
⊢ (μ.trim hm).toOuterMeasure = μ.trim
have rw : (μ.toMeasure sorry).toOuterMeasure = μ.trim
Tactic: rw [Measure.trim, toMeasure_toOuterMeasure (ms := m)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
rw : (μ.toMeasure ⋯).toOuterMeasure = μ.trim
⊢ (μ.trim hm).toOuterMeasure = μ.trim
have rw₁ : μ.trim = μ.trim
Tactic: rw [Measure.trim, toMeasure_toOuterMeasure (ms := m)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ.toMeasure sorry : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [Measure.trim, toMeasure_apply (ms := m) _ _ hs, Measure.coe_toOuterMeasure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
rw : Eq (α := ℝ≥0∞) ((μ.toMeasure ⋯ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [Measure.trim, toMeasure_apply (ms := m) _ _ hs, Measure.coe_toOuterMeasure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
rw : Eq (α := ℝ≥0∞) ((μ.toMeasure ⋯ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ : Eq (α := ℝ≥0∞) ((μ.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [Measure.trim, toMeasure_apply (ms := m) _ _ hs, Measure.coe_toOuterMeasure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
⊢ μ.trim hm = Measure.map id μ
have refine : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.map id μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: refine @Measure.ext α m _ _ (fun s hs ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.map id μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (id ⁻¹' s) : ℝ≥0∞)
Tactic: rw [Measure.map_apply (measurable_id'' hm) hs, trim_measurableSet_eq hm hs, Set.preimage_id]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
s : Set α
hs : MeasurableSet s
rw : Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (id ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.map id μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (id ⁻¹' s) : ℝ≥0∞)
Tactic: rw [Measure.map_apply (measurable_id'' hm) hs, trim_measurableSet_eq hm hs, Set.preimage_id]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
s : Set α
hs : MeasurableSet s
rw : Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (id ⁻¹' s) : ℝ≥0∞)
rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (id ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.map id μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [Measure.map_apply (measurable_id'' hm) hs, trim_measurableSet_eq hm hs, Set.preimage_id]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : Measurable f
⊢ Eq (α := Measure β) (Measure.map f (μ.trim ⋯)) (Measure.map f μ)
have h : ∀ (s : Set β) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((Measure.map f (μ.trim sorry) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((Measure.map f (μ.trim ⋯) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h : MeasurableSet (f ⁻¹' s)
Tactic: rw [Measure.map_apply hf hs, Measure.map_apply _ hs, trim_measurableSet_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
h : MeasurableSet (f ⁻¹' s)
⊢ Eq (α := ℝ≥0∞) (((Measure.map f (μ.trim ⋯) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have rw : Measurable f
Tactic: rw [Measure.map_apply hf hs, Measure.map_apply _ hs, trim_measurableSet_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ.trim ⋯ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ.trim sorry : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
  (((Measure.map f (μ.trim sorry) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← map_trim_comap hf, Measure.map_apply (Measurable.of_comap_le le_rfl) hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
rw :
  Eq (α := ℝ≥0∞) ((μ.trim ⋯ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((Measure.map f (μ.trim ⋯) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.trim ⋯ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ.trim sorry : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) ((μ.trim sorry : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
Tactic: rw [← map_trim_comap hf, Measure.map_apply (Measurable.of_comap_le le_rfl) hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : Measurable f
p : β → Prop
hp : MeasurableSet.{u_2} (α := β) {x : β | p x}
⊢ (∀ᵐ (y : β) ∂Measure.map f μ, p y) ↔ ∀ᵐ (x : α) ∂μ.trim ⋯, p (f x)
have rw : (∀ᵐ (y : β) ∂Measure.map f (μ.trim sorry), p y) ↔ ∀ᵐ (x : α) ∂μ.trim sorry, p (f x)
Tactic: rw [← map_trim_comap hf, ae_map_iff (Measurable.of_comap_le le_rfl).aemeasurable hp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : Measurable f
p : β → Prop
hp : MeasurableSet.{u_2} (α := β) {x : β | p x}
rw : (∀ᵐ (y : β) ∂Measure.map f (μ.trim ⋯), p y) ↔ ∀ᵐ (x : α) ∂μ.trim ⋯, p (f x)
⊢ (∀ᵐ (y : β) ∂Measure.map f μ, p y) ↔ ∀ᵐ (x : α) ∂μ.trim ⋯, p (f x)
have rw₁ : (∀ᵐ (x : α) ∂μ.trim sorry, p (f x)) ↔ ∀ᵐ (x : α) ∂μ.trim sorry, p (f x)
Tactic: rw [← map_trim_comap hf, ae_map_iff (Measurable.of_comap_le le_rfl).aemeasurable hp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
h : Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have grw : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: grw [← nonpos_iff_eq_zero, ← h, le_trim hm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
h : Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
grw : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have grw₁ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: grw [← nonpos_iff_eq_zero, ← h, le_trim hm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
h : Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
grw : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
grw₁ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have grw₂ : LE.le (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: grw [← nonpos_iff_eq_zero, ← h, le_trim hm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
m₁ m₂ : MeasurableSpace α
hm₁₂ : m₁ ≤ m₂
hm₂ : m₂ ≤ m0
⊢ (μ.trim hm₂).trim hm₁₂ = μ.trim ⋯
have refine : ∀ (t : Set α) (ht : MeasurableSet t),
  Eq (α := ℝ≥0∞) (((μ.trim hm₂).trim hm₁₂ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ.trim sorry : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: refine @Measure.ext _ m₁ _ _ (fun t ht => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
m₁ m₂ : MeasurableSpace α
hm₁₂ : m₁ ≤ m₂
hm₂ : m₂ ≤ m0
t : Set α
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) (((μ.trim hm₂).trim hm₁₂ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ.trim ⋯ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ.trim hm₂ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ.trim sorry : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [trim_measurableSet_eq hm₁₂ ht, trim_measurableSet_eq (hm₁₂.trans hm₂) ht,
    trim_measurableSet_eq hm₂ (hm₁₂ t ht)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
m₁ m₂ : MeasurableSpace α
hm₁₂ : m₁ ≤ m₂
hm₂ : m₂ ≤ m0
t : Set α
ht : MeasurableSet t
rw : Eq (α := ℝ≥0∞) ((μ.trim hm₂ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ.trim ⋯ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((μ.trim hm₂).trim hm₁₂ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ.trim ⋯ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ.trim hm₂ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [trim_measurableSet_eq hm₁₂ ht, trim_measurableSet_eq (hm₁₂.trans hm₂) ht,
    trim_measurableSet_eq hm₂ (hm₁₂ t ht)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
m₁ m₂ : MeasurableSpace α
hm₁₂ : m₁ ≤ m₂
hm₂ : m₂ ≤ m0
t : Set α
ht : MeasurableSet t
rw : Eq (α := ℝ≥0∞) ((μ.trim hm₂ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ.trim ⋯ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
rw₁ : Eq (α := ℝ≥0∞) ((μ.trim hm₂ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((μ.trim hm₂).trim hm₁₂ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ.trim ⋯ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [trim_measurableSet_eq hm₁₂ ht, trim_measurableSet_eq (hm₁₂.trans hm₂) ht,
    trim_measurableSet_eq hm₂ (hm₁₂ t ht)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
s : Set α
hm : m ≤ m0
μ : Measure α
hs : MeasurableSet s
⊢ (μ.trim hm).restrict s = (μ.restrict s).trim hm
have refine : ∀ (t : Set α) (ht : MeasurableSet t),
  Eq (α := ℝ≥0∞) (((μ.trim hm).restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((μ.restrict s).trim hm : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: refine @Measure.ext _ m _ _ (fun t ht => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
s : Set α
hm : m ≤ m0
μ : Measure α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) (((μ.trim hm).restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((μ.restrict s).trim hm : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
  (((μ.restrict s).trim hm : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [@Measure.restrict_apply α m _ _ _ ht, trim_measurableSet_eq hm ht,
    Measure.restrict_apply (hm t ht),
    trim_measurableSet_eq hm (@MeasurableSet.inter α m t s ht hs)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
s : Set α
hm : m ≤ m0
μ : Measure α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
rw :
  Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    (((μ.restrict s).trim hm : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((μ.trim hm).restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((μ.restrict s).trim hm : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [@Measure.restrict_apply α m _ _ _ ht, trim_measurableSet_eq hm ht,
    Measure.restrict_apply (hm t ht),
    trim_measurableSet_eq hm (@MeasurableSet.inter α m t s ht hs)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
s : Set α
hm : m ≤ m0
μ : Measure α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
rw :
  Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    (((μ.restrict s).trim hm : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
rw₁ : Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((μ.trim hm).restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((μ.restrict s).trim hm : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
Tactic: rw [@Measure.restrict_apply α m _ _ _ ht, trim_measurableSet_eq hm ht,
    Measure.restrict_apply (hm t ht),
    trim_measurableSet_eq hm (@MeasurableSet.inter α m t s ht hs)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
s : Set α
hm : m ≤ m0
μ : Measure α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
rw :
  Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    (((μ.restrict s).trim hm : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
rw₁ : Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
rw₂ : Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((μ.trim hm).restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((μ.restrict s).trim hm : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have rw₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
Tactic: rw [@Measure.restrict_apply α m _ _ _ ht, trim_measurableSet_eq hm ht,
    Measure.restrict_apply (hm t ht),
    trim_measurableSet_eq hm (@MeasurableSet.inter α m t s ht hs)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
β : Type u_2
m m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
s : Set α
hm : m ≤ m0
inst : IsFiniteMeasure μ
⊢ LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [trim_measurableSet_eq hm (@MeasurableSet.univ _ m)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m
inst : SigmaFinite (μ.trim ⋯)
⊢ SigmaFinite (μ.trim hm)
have refine : (μ.trim hm).FiniteSpanningSetsIn Set.univ
Tactic: refine ⟨⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m
inst : SigmaFinite (μ.trim ⋯)
⊢ (μ.trim hm).FiniteSpanningSetsIn Set.univ
have set : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) (spanningSets (μ.trim sorry) i) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine
    { set := spanningSets (μ.trim (hm₂.trans hm))
      set_mem := fun _ => Set.mem_univ _
      finite := fun i => ?_
      spanning := iUnion_spanningSets _ }
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m
inst : SigmaFinite (μ.trim ⋯)
i : ℕ
⊢ Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) (spanningSets (μ.trim ⋯) i) : ℝ≥0∞)
    (((μ.trim hm).trim hm₂ : (a : Set α) → ℝ≥0∞) (spanningSets (μ.trim ⋯) i) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) (spanningSets (μ.trim sorry) i) : ℝ≥0∞)
  ((μ.trim hm : (a : Set α) → ℝ≥0∞) (spanningSets (μ.trim sorry) i) : ℝ≥0∞)
Tactic: rw [@trim_measurableSet_eq α m₂ m (μ.trim hm) _ hm₂ (measurableSet_spanningSets _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m
inst : SigmaFinite (μ.trim ⋯)
i : ℕ
⊢ Eq (α := ℝ≥0∞) (((μ.trim hm).trim hm₂ : (a : Set α) → ℝ≥0∞) (spanningSets (μ.trim ⋯) i) : ℝ≥0∞)
    ((μ.trim ⋯ : (a : Set α) → ℝ≥0∞) (spanningSets (μ.trim ⋯) i) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ.trim sorry : (a : Set α) → ℝ≥0∞) (spanningSets (μ.trim sorry) i) : ℝ≥0∞)
  ((μ.trim sorry : (a : Set α) → ℝ≥0∞) (spanningSets (μ.trim sorry) i) : ℝ≥0∞)
Tactic: rw [@trim_trim _ _ μ _ _ hm₂ hm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m
inst : SigmaFinite (μ.trim ⋯)
i : ℕ
⊢ LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) (spanningSets (μ.trim ⋯) i) : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) (spanningSets (μ.trim sorry) i) : ℝ≥0∞)
  (((μ.trim hm).trim hm₂ : (a : Set α) → ℝ≥0∞) (spanningSets (μ.trim sorry) i) : ℝ≥0∞)
Tactic: calc
    (μ.trim hm) (spanningSets (μ.trim (hm₂.trans hm)) i) =
        ((μ.trim hm).trim hm₂) (spanningSets (μ.trim (hm₂.trans hm)) i) := by
      rw [@trim_measurableSet_eq α m₂ m (μ.trim hm) _ hm₂ (measurableSet_spanningSets _ _)]
    _ = (μ.trim (hm₂.trans hm)) (spanningSets (μ.trim (hm₂.trans hm)) i) := by
      rw [@trim_trim _ _ μ _ _ hm₂ hm]
    _ < ∞ := measure_spanningSets_lt_top _ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m
inst : SigmaFinite (μ.trim ⋯)
i : ℕ
rw :
  Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) (spanningSets (μ.trim ⋯) i) : ℝ≥0∞)
    (((μ.trim hm).trim hm₂ : (a : Set α) → ℝ≥0∞) (spanningSets (μ.trim ⋯) i) : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) (spanningSets (μ.trim ⋯) i) : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) (((μ.trim hm).trim hm₂ : (a : Set α) → ℝ≥0∞) (spanningSets (μ.trim sorry) i) : ℝ≥0∞)
  ((μ.trim sorry : (a : Set α) → ℝ≥0∞) (spanningSets (μ.trim sorry) i) : ℝ≥0∞)
Tactic: calc
    (μ.trim hm) (spanningSets (μ.trim (hm₂.trans hm)) i) =
        ((μ.trim hm).trim hm₂) (spanningSets (μ.trim (hm₂.trans hm)) i) := by
      rw [@trim_measurableSet_eq α m₂ m (μ.trim hm) _ hm₂ (measurableSet_spanningSets _ _)]
    _ = (μ.trim (hm₂.trans hm)) (spanningSets (μ.trim (hm₂.trans hm)) i) := by
      rw [@trim_trim _ _ μ _ _ hm₂ hm]
    _ < ∞ := measure_spanningSets_lt_top _ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst : SigmaFinite (μ.trim hm)
⊢ SigmaFinite μ
have rw : SigmaFinite (μ.trim sorry)
Tactic: rw [← trim_eq_self (μ := μ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ SigmaFinite (m0 := ⊥) (μ.trim ⋯) ↔ IsFiniteMeasure μ
have rw : IsFiniteMeasure (m0 := ⊥) (μ.trim sorry) ↔ IsFiniteMeasure μ
Tactic: rw [sigmaFinite_bot_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ IsFiniteMeasure (m0 := ⊥) (μ.trim ⋯) ↔ IsFiniteMeasure μ
have refine_1 : ∀ (h : IsFiniteMeasure (m0 := ⊥) (μ.trim sorry)), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine ⟨fun h => ⟨?_⟩, fun h => ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
refine_1 :
  ∀ (h : IsFiniteMeasure (m0 := ⊥) (μ.trim ⋯)), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IsFiniteMeasure (m0 := ⊥) (μ.trim ⋯) ↔ IsFiniteMeasure μ
have refine_2 : ∀ (h : IsFiniteMeasure μ), LT.lt (α := ℝ≥0∞) (((μ.trim sorry : Measure α) : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine ⟨fun h => ⟨?_⟩, fun h => ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : IsFiniteMeasure (m0 := ⊥) (μ.trim ⋯)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have h_univ : LT.lt (α := ℝ≥0∞) (((μ.trim sorry : Measure α) : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have h_univ := h.measure_univ_lt_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : IsFiniteMeasure μ
⊢ LT.lt (α := ℝ≥0∞) (((μ.trim ⋯ : Measure α) : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have h_univ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have h_univ := h.measure_univ_lt_top