awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
⊢ ∀ (i : ℕ → Set α) (i_1 : s ⊆ iUnion i),
    LE.le (α := ℝ≥0∞) (⨅ (t : ℕ → Set α), ⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i))
      (∑' (n : ℕ), m (i n))
have a : ∀ (t : ℕ → Set α) (ht_subset : s ⊆ iUnion t),
  LE.le (α := ℝ≥0∞) (⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i)) (∑' (n : ℕ), m (t n))
Tactic: refine fun t ht_subset ↦ iInf_le_of_le t ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
t : ℕ → Set α
ht_subset : s ⊆ iUnion t
⊢ LE.le (α := ℝ≥0∞) (⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i)) (∑' (n : ℕ), m (t n))
have pos : ∀ (ht : ∀ (i : ℕ), P (t i)),
  LE.le (α := ℝ≥0∞) (⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i)) (∑' (n : ℕ), m (t n))
Tactic: by_cases ht : ∀ i, P (t i)
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
t : ℕ → Set α
ht_subset : s ⊆ iUnion t
pos :
  ∀ (ht : ∀ (i : ℕ), P (t i)),
    LE.le (α := ℝ≥0∞) (⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i))
      (∑' (n : ℕ), m (t n))
⊢ LE.le (α := ℝ≥0∞) (⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i)) (∑' (n : ℕ), m (t n))
have neg : ∀ (ht : ¬∀ (i : ℕ), P (t i)),
  LE.le (α := ℝ≥0∞) (⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i)) (∑' (n : ℕ), m (t n))
Tactic: by_cases ht : ∀ i, P (t i)
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
t : ℕ → Set α
ht_subset : s ⊆ iUnion t
ht : ¬∀ (i : ℕ), P (t i)
⊢ LE.le (α := ℝ≥0∞) (⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ (i : ℕ), t i), ∑' (i : ℕ), m (t i)) (∑' (n : ℕ), m (t n))
have neg : Eq (α := ℝ≥0∞) (∑' (i : ℕ), m (t i)) ∞
Tactic: simp only [ht, not_false_eq_true, iInf_neg, top_le_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (hypothesis)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
t : ℕ → Set α
ht_subset : s ⊆ iUnion t
ht : ¬∀ (i : ℕ), P (t i)
⊢ Eq (α := ℝ≥0∞) (∑' (i : ℕ), m (t i)) ∞
have ht₁ : ∃ (i : ℕ), ¬P (t i)
Tactic: push Not at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
t : ℕ → Set α
ht_subset : s ⊆ iUnion t
ht : ∃ (i : ℕ), ¬P (t i)
⊢ Eq (α := ℝ≥0∞) (∑' (i : ℕ), m (t i)) ∞
have neg : ∀ (i : ℕ) (hti_notMem : ¬P (t i)), Eq (α := ℝ≥0∞) (∑' (i : ℕ), m (t i)) ∞
Tactic: obtain ⟨i, hti_notMem⟩ := ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (hypothesis)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
t : ℕ → Set α
ht_subset : s ⊆ iUnion t
i : ℕ
hti_notMem : ¬P (t i)
⊢ Eq (α := ℝ≥0∞) (∑' (i : ℕ), m (t i)) ∞
have hfi_top : m (t i) = ∞
Tactic: have hfi_top : m (t i) = ∞ := m_top _ hti_notMem
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ∞
⊢ (OuterMeasure.ofFunction m m_empty : (a : Set α) → ℝ≥0∞) (s ∪ t) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((OuterMeasure.ofFunction m m_empty : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((OuterMeasure.ofFunction m m_empty : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have refine : ∀ (f : ℕ → Set α) (hf : s ∪ t ⊆ ⋃ (i : ℕ), f i),
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((OuterMeasure.ofFunction m m_empty : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((OuterMeasure.ofFunction m m_empty : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≤
    ∑' (i : ℕ), m (f i)
Tactic: refine le_antisymm (measure_union_le _ _) (le_iInf₂ fun f hf ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ∞
f : ℕ → Set α
hf : s ∪ t ⊆ ⋃ (i : ℕ), f i
μ : OuterMeasure α := OuterMeasure.ofFunction m m_empty
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≤
    ∑' (i : ℕ), m (f i)
have inl : ∀ (i : ℕ) (hs : (s ∩ f i).Nonempty) (ht : (t ∩ f i).Nonempty),
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≤
    ∑' (i : ℕ), m (f i)
Tactic: rcases Classical.em (∃ i, (s ∩ f i).Nonempty ∧ (t ∩ f i).Nonempty) with (⟨i, hs, ht⟩ | he)
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ∞
f : ℕ → Set α
hf : s ∪ t ⊆ ⋃ (i : ℕ), f i
μ : OuterMeasure α := OuterMeasure.ofFunction m m_empty
inl :
  ∀ (i : ℕ) (hs : (s ∩ f i).Nonempty) (ht : (t ∩ f i).Nonempty),
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≤
      ∑' (i : ℕ), m (f i)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≤
    ∑' (i : ℕ), m (f i)
have inr : ∀ (he : ¬∃ (i : ℕ), (s ∩ f i).Nonempty ∧ (t ∩ f i).Nonempty),
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≤
    ∑' (i : ℕ), m (f i)
Tactic: rcases Classical.em (∃ i, (s ∩ f i).Nonempty ∧ (t ∩ f i).Nonempty) with (⟨i, hs, ht⟩ | he)
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (hypothesis)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ∞
f : ℕ → Set α
hf : s ∪ t ⊆ ⋃ (i : ℕ), f i
μ : OuterMeasure α := OuterMeasure.ofFunction m m_empty
he : ¬∃ (i : ℕ), (s ∩ f i).Nonempty ∧ (t ∩ f i).Nonempty
I : (s : Set α) → Set ℕ := fun (s : Set α) ↦ {i : ℕ | (s ∩ f i).Nonempty}
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≤
    ∑' (i : ℕ), m (f i)
have hd : Disjoint (I s) (I t)
Tactic: have hd : Disjoint (I s) (I t) := disjoint_iff_inf_le.mpr fun i hi => he ⟨i, hi⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (hypothesis)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ∞
f : ℕ → Set α
hf : s ∪ t ⊆ ⋃ (i : ℕ), f i
μ : OuterMeasure α := OuterMeasure.ofFunction m m_empty
he : ¬∃ (i : ℕ), (s ∩ f i).Nonempty ∧ (t ∩ f i).Nonempty
I : (s : Set α) → Set ℕ := fun (s : Set α) ↦ {i : ℕ | (s ∩ f i).Nonempty}
hd : Disjoint (I s) (I t)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≤
    ∑' (i : ℕ), m (f i)
have hI : ∀ u ⊆ s ∪ t,
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
    (∑' (i : (↑(I u) : Type)), (μ : (a : Set α) → ℝ≥0∞) (f (↑i : ℕ)) : ℝ≥0∞)
Tactic: have hI : ∀ u ⊆ s ∪ t, μ u ≤ ∑' i : I u, μ (f i) := fun u hu =>
    calc
      μ u ≤ μ (⋃ i : I u, f i) :=
        μ.mono fun x hx =>
          let ⟨i, hi⟩ := mem_iUnion.1 (hf (hu hx))
          mem_iUnion.2 ⟨⟨i, ⟨x, hx, hi⟩⟩, hi⟩
      _ ≤ ∑' i : I u, μ (f i) := measure_iUnion_le _
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
⊢ Eq.{u_2 + 1} (α := OuterMeasure β)
    ((comap f : (a : OuterMeasure α) → OuterMeasure β) (OuterMeasure.ofFunction m m_empty) : OuterMeasure β)
    (OuterMeasure.ofFunction (fun (s : Set β) ↦ m (f '' s)) ⋯ : OuterMeasure β)
have refine_1 : ∀ (s : Set β),
  (((comap f : (a : OuterMeasure α) → OuterMeasure β) (OuterMeasure.ofFunction m m_empty) : OuterMeasure β) :
        (a : Set β) → ℝ≥0∞)
      s ≤
    m (f '' s)
Tactic: refine le_antisymm (le_ofFunction.2 fun s => ?_) fun s => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
refine_1 :
  ∀ (s : Set β),
    (((comap f : (a : OuterMeasure α) → OuterMeasure β) (OuterMeasure.ofFunction m m_empty) : OuterMeasure β) :
          (a : Set β) → ℝ≥0∞)
        s ≤
      m (f '' s)
⊢ Eq.{u_2 + 1} (α := OuterMeasure β)
    ((comap f : (a : OuterMeasure α) → OuterMeasure β) (OuterMeasure.ofFunction m m_empty) : OuterMeasure β)
    (OuterMeasure.ofFunction (fun (s : Set β) ↦ m (f '' s)) ⋯ : OuterMeasure β)
have refine_2 : ∀ (s : Set β),
  LE.le (α := ℝ≥0∞)
    (((OuterMeasure.ofFunction (fun (s : Set β) ↦ m (f '' s)) sorry : OuterMeasure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((comap f : (a : OuterMeasure α) → OuterMeasure β) (OuterMeasure.ofFunction m m_empty) : OuterMeasure β) :
          (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)
Tactic: refine le_antisymm (le_ofFunction.2 fun s => ?_) fun s => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
⊢ LE.le (α := ℝ≥0∞)
    (((OuterMeasure.ofFunction (fun (s : Set β) ↦ m (f '' s)) ⋯ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((comap f : (a : OuterMeasure α) → OuterMeasure β) (OuterMeasure.ofFunction m m_empty) : OuterMeasure β) :
          (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have refine_2 : LE.le (α := ℝ≥0∞) (⨅ (t : ℕ → Set β), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (f '' t n))
  (⨅ (t : ℕ → Set α), ⨅ (_ : f '' s ⊆ iUnion t), ∑' (n : ℕ), m (t n))
Tactic: rw [comap_apply, ofFunction_apply, ofFunction_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
⊢ LE.le (α := ℝ≥0∞) (⨅ (t : ℕ → Set β), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (f '' t n))
    (⨅ (t : ℕ → Set α), ⨅ (_ : f '' s ⊆ iUnion t), ∑' (n : ℕ), m (t n))
have refine_2 : ∀ (t : ℕ → Set α),
  LE.le (α := ℝ≥0∞) (⨅ (_ : s ⊆ ⋃ (k : ℕ), f ⁻¹' t k), ∑' (n : ℕ), m (f '' (fun (k : ℕ) ↦ f ⁻¹' t k) n))
    (⨅ (_ : f '' s ⊆ iUnion t), ∑' (n : ℕ), m (t n))
Tactic: refine iInf_mono' fun t => ⟨fun k => f ⁻¹' t k, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
t : ℕ → Set α
⊢ LE.le (α := ℝ≥0∞) (⨅ (_ : s ⊆ ⋃ (k : ℕ), f ⁻¹' t k), ∑' (n : ℕ), m (f '' (fun (k : ℕ) ↦ f ⁻¹' t k) n))
    (⨅ (_ : f '' s ⊆ iUnion t), ∑' (n : ℕ), m (t n))
have refine_2 : ∀ (ht : f '' s ⊆ iUnion t),
  ∃ (_ : s ⊆ ⋃ (k : ℕ), f ⁻¹' t k),
    LE.le (α := ℝ≥0∞) (∑' (n : ℕ), m (f '' (fun (k : ℕ) ↦ f ⁻¹' t k) n)) (∑' (n : ℕ), m (t n))
Tactic: refine iInf_mono' fun ht => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (hypothesis)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
t : ℕ → Set α
ht : f '' s ⊆ iUnion t
⊢ ∃ (_ : s ⊆ ⋃ (k : ℕ), f ⁻¹' t k),
    LE.le (α := ℝ≥0∞) (∑' (n : ℕ), m (f '' (fun (k : ℕ) ↦ f ⁻¹' t k) n)) (∑' (n : ℕ), m (t n))
have ht₁ : s ⊆ ⋃ (i : ℕ), f ⁻¹' t i
Tactic: rw [Set.image_subset_iff, preimage_iUnion] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
t : ℕ → Set α
ht : s ⊆ ⋃ (i : ℕ), f ⁻¹' t i
⊢ ∃ (_ : s ⊆ ⋃ (k : ℕ), f ⁻¹' t k),
    LE.le (α := ℝ≥0∞) (∑' (n : ℕ), m (f '' (fun (k : ℕ) ↦ f ⁻¹' t k) n)) (∑' (n : ℕ), m (t n))
have refine_2 : ∀ (n : ℕ), m (f '' (fun (k : ℕ) ↦ f ⁻¹' t k) n) ≤ m (t n)
Tactic: refine ⟨ht, ENNReal.tsum_le_tsum fun n => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
t : ℕ → Set α
ht : s ⊆ ⋃ (i : ℕ), f ⁻¹' t i
n : ℕ
⊢ m (f '' (fun (k : ℕ) ↦ f ⁻¹' t k) n) ≤ m (t n)
have refine_2 : ∀ (hl : Monotone m), m (f '' (fun (k : ℕ) ↦ f ⁻¹' t k) n) ≤ m (t n)
Tactic: rcases h with hl | hr
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
t : ℕ → Set α
ht : s ⊆ ⋃ (i : ℕ), f ⁻¹' t i
n : ℕ
refine_2 : ∀ (hl : Monotone m), m (f '' (fun (k : ℕ) ↦ f ⁻¹' t k) n) ≤ m (t n)
⊢ m (f '' (fun (k : ℕ) ↦ f ⁻¹' t k) n) ≤ m (t n)
have refine_2₁ : ∀ (hr : Surjective f), m (f '' (fun (k : ℕ) ↦ f ⁻¹' t k) n) ≤ m (t n)
Tactic: rcases h with hl | hr
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
hf : Injective f
⊢ (map f : (a : OuterMeasure α) → OuterMeasure β) (OuterMeasure.ofFunction m m_empty) =
    OuterMeasure.ofFunction (fun (s : Set β) ↦ m (f ⁻¹' s)) m_empty
have refine : ∀ (s : Set β),
  LE.le (α := ℝ≥0∞) ((OuterMeasure.ofFunction (fun (s : Set β) ↦ m (f ⁻¹' s)) m_empty : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((map f : (a : OuterMeasure α) → OuterMeasure β) (OuterMeasure.ofFunction m m_empty) : OuterMeasure β) :
          (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)
Tactic: refine (map_ofFunction_le _).antisymm fun s => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
hf : Injective f
s : Set β
⊢ LE.le (α := ℝ≥0∞) ((OuterMeasure.ofFunction (fun (s : Set β) ↦ m (f ⁻¹' s)) m_empty : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((map f : (a : OuterMeasure α) → OuterMeasure β) (OuterMeasure.ofFunction m m_empty) : OuterMeasure β) :
          (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have simp : ∀ (i : ℕ → Set α) (i_1 : f ⁻¹' s ⊆ iUnion i),
  LE.le (α := ℝ≥0∞) (⨅ (t : ℕ → Set β), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (f ⁻¹' t n)) (∑' (n : ℕ), m (i n))
Tactic: simp only [ofFunction_apply, map_apply, le_iInf_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
hf : Injective f
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ LE.le (α := ℝ≥0∞) (⨅ (t : ℕ → Set β), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (f ⁻¹' t n)) (∑' (n : ℕ), m (t n))
have refine_1 : s ⊆ ⋃ (n : ℕ), (range f)ᶜ ∪ f '' t n
Tactic: refine iInf_le_of_le (fun n => (range f)ᶜ ∪ f '' t n) (iInf_le_of_le ?_ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
hf : Injective f
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
refine_1 : s ⊆ ⋃ (n : ℕ), (range f)ᶜ ∪ f '' t n
⊢ LE.le (α := ℝ≥0∞) (⨅ (t : ℕ → Set β), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (f ⁻¹' t n)) (∑' (n : ℕ), m (t n))
have refine_2 : LE.le (α := ℝ≥0∞) (∑' (n : ℕ), m (f ⁻¹' (fun (n : ℕ) ↦ (range f)ᶜ ∪ f '' t n) n)) (∑' (n : ℕ), m (t n))
Tactic: refine iInf_le_of_le (fun n => (range f)ᶜ ∪ f '' t n) (iInf_le_of_le ?_ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
hf : Injective f
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ s ⊆ ⋃ (n : ℕ), (range f)ᶜ ∪ f '' t n
have refine_1 : f '' f ⁻¹' s ⊆ f '' ⋃ (i : ℕ), t i
Tactic: rw [← union_iUnion, ← inter_subset, ← image_preimage_eq_inter_range, ← image_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
hf : Injective f
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ LE.le (α := ℝ≥0∞) (∑' (n : ℕ), m (f ⁻¹' (fun (n : ℕ) ↦ (range f)ᶜ ∪ f '' t n) n)) (∑' (n : ℕ), m (t n))
have refine_2 : ∀ (n : ℕ), m (f ⁻¹' (fun (n : ℕ) ↦ (range f)ᶜ ∪ f '' t n) n) = m (t n)
Tactic: refine ENNReal.tsum_le_tsum fun n => le_of_eq ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ Eq (α := OuterMeasure α)
    ((map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) ∘ₗ comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) :
          (a : OuterMeasure α) → OuterMeasure α)
        (OuterMeasure.ofFunction m m_empty) :
      OuterMeasure α)
    (OuterMeasure.ofFunction (fun (t : Set α) ↦ m (t ∩ s)) ⋯ : OuterMeasure α)
have simp : Eq (α := OuterMeasure α)
  ((map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : OuterMeasure { x : α // x ∈ s }) → OuterMeasure α)
      ((comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : OuterMeasure α) → OuterMeasure { x : α // x ∈ s })
          (OuterMeasure.ofFunction m m_empty) :
        OuterMeasure { x : α // x ∈ s }) :
    OuterMeasure α)
  (OuterMeasure.ofFunction (fun (t : Set α) ↦ m (s ∩ t)) sorry : OuterMeasure α)
Tactic: simp only [inter_comm _ s, LinearMap.comp_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ Eq (α := OuterMeasure α)
    ((map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : OuterMeasure { x : α // x ∈ s }) → OuterMeasure α)
        ((comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : OuterMeasure α) → OuterMeasure { x : α // x ∈ s })
            (OuterMeasure.ofFunction m m_empty) :
          OuterMeasure { x : α // x ∈ s }) :
      OuterMeasure α)
    (OuterMeasure.ofFunction (fun (t : Set α) ↦ m (s ∩ t)) ⋯ : OuterMeasure α)
have rw : Eq.{u_1 + 1} (α := OuterMeasure α)
  ((map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : OuterMeasure { x : α // x ∈ s }) → OuterMeasure α)
      (OuterMeasure.ofFunction (fun (s_1 : Set { x : α // x ∈ s }) ↦ m (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' s_1))
        sorry) :
    OuterMeasure α)
  (OuterMeasure.ofFunction (fun (t : Set α) ↦ m (s ∩ t)) sorry : OuterMeasure α)
Tactic: rw [comap_ofFunction _ (Or.inl hm)]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
c : ℝ≥0∞
hc : c ≠ ∞
⊢ c • OuterMeasure.ofFunction m m_empty = OuterMeasure.ofFunction (c • m) ⋯
have h : ∀ (s : Set α),
  Eq (α := ℝ≥0∞) ((c • OuterMeasure.ofFunction m m_empty : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((OuterMeasure.ofFunction (c • m) sorry : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext1 s
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (hypothesis)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
c : ℝ≥0∞
hc : c ≠ ∞
s : Set α
⊢ Eq (α := ℝ≥0∞) ((c • OuterMeasure.ofFunction m m_empty : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((OuterMeasure.ofFunction (c • m) ⋯ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have this : Nonempty.{max 1 (u_1 + 1)} { t : ℕ → Set α // s ⊆ ⋃ (i : ℕ), t i }
Tactic: haveI : Nonempty { t : ℕ → Set α // s ⊆ ⋃ i, t i } := ⟨⟨fun _ => s, subset_iUnion (fun _ => s) 0⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
c : ℝ≥0∞
hc : c ≠ ∞
s : Set α
this : Nonempty.{max 1 (u_1 + 1)} { t : ℕ → Set α // s ⊆ ⋃ (i : ℕ), t i }
⊢ Eq (α := ℝ≥0∞) ((c • OuterMeasure.ofFunction m m_empty : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((OuterMeasure.ofFunction (c • m) ⋯ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h : c * ⨅ (x : { i : ℕ → Set α // s ⊆ iUnion i }), ∑' (n : ℕ), m ((↑x : ℕ → Set α) n) =
  ⨅ (x : { i : ℕ → Set α // s ⊆ iUnion i }), c * ∑' (i : ℕ), m ((↑x : ℕ → Set α) i)
Tactic: simp only [smul_apply, ofFunction_apply, ENNReal.tsum_mul_left, Pi.smul_apply, smul_eq_mul,
  iInf_subtype']
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
c : ℝ≥0∞
hc : c ≠ ∞
s : Set α
this : Nonempty.{max 1 (u_1 + 1)} { t : ℕ → Set α // s ⊆ ⋃ (i : ℕ), t i }
⊢ c * ⨅ (x : { i : ℕ → Set α // s ⊆ iUnion i }), ∑' (n : ℕ), m ((↑x : ℕ → Set α) n) =
    ⨅ (x : { i : ℕ → Set α // s ⊆ iUnion i }), c * ∑' (i : ℕ), m ((↑x : ℕ → Set α) i)
have h : Eq (α := ℝ≥0∞) (⨅ (i : { i : ℕ → Set α // s ⊆ iUnion i }), c * ∑' (n : ℕ), m ((↑i : ℕ → Set α) n))
  (⨅ (x : { i : ℕ → Set α // s ⊆ iUnion i }), c * ∑' (i : ℕ), m ((↑x : ℕ → Set α) i))
Tactic: rw [ENNReal.mul_iInf fun h => (hc h).elim]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
⊢ (fun (s : Set α) ↦ ⨆ (_ : s.Nonempty), m s) = m
have h : ∀ (t : Set α), ⨆ (_ : t.Nonempty), m t = m t
Tactic: ext1 t
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
⊢ ⨆ (_ : t.Nonempty), m t = m t
have h : ∀ (h : t = ∅), ⨆ (_ : t.Nonempty), m t = m t
Tactic: rcases t.eq_empty_or_nonempty with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
h : ∀ (h : t = ∅), ⨆ (_ : t.Nonempty), m t = m t
⊢ ⨆ (_ : t.Nonempty), m t = m t
have h₁ : ∀ (h : t.Nonempty), ⨆ (_ : t.Nonempty), m t = m t
Tactic: rcases t.eq_empty_or_nonempty with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (hypothesis)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
⊢ Eq (α := ℝ≥0∞) ((boundedBy m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((OuterMeasure.ofFunction m m_empty : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have this : (fun (s : Set α) ↦ ⨆ (_ : s.Nonempty), m s) = m
Tactic: have : (fun s : Set α => ⨆ _ : s.Nonempty, m s) = m := by
    ext1 t
    rcases t.eq_empty_or_nonempty with h | h <;> simp [h, Set.not_nonempty_empty, m_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
m_empty : m ∅ = 0
m_mono : ∀ ⦃t : Set α⦄, s ⊆ t → m s ≤ m t
m_subadd : ∀ (s : ℕ → Set α), m (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), m (s i)
⊢ (boundedBy m : (a : Set α) → ℝ≥0∞) s = m s
have rw : (OuterMeasure.ofFunction m m_empty : (a : Set α) → ℝ≥0∞) s = m s
Tactic: rw [boundedBy_eq_ofFunction m_empty, ofFunction_eq s m_mono m_subadd]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
m_empty : m ∅ = 0
m_mono : ∀ ⦃t : Set α⦄, s ⊆ t → m s ≤ m t
m_subadd : ∀ (s : ℕ → Set α), m (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), m (s i)
rw : (OuterMeasure.ofFunction m m_empty : (a : Set α) → ℝ≥0∞) s = m s
⊢ (boundedBy m : (a : Set α) → ℝ≥0∞) s = m s
have rw₁ : m s = m s
Tactic: rw [boundedBy_eq_ofFunction m_empty, ofFunction_eq s m_mono m_subadd]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
⊢ μ ≤ boundedBy m ↔ ∀ (s : Set α), (μ : (a : Set α) → ℝ≥0∞) s ≤ m s
have rw : ∀ (a : Set α),
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) (⨆ (_ : a.Nonempty), m a : ℝ≥0∞) ↔
    (μ : (a : Set α) → ℝ≥0∞) a ≤ m a
Tactic: rw [boundedBy, le_ofFunction, forall_congr']
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
s : Set α
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (⨆ (_ : s.Nonempty), m s : ℝ≥0∞) ↔
    (μ : (a : Set α) → ℝ≥0∞) s ≤ m s
have inl : ∀ (h : s = ∅),
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (⨆ (_ : s.Nonempty), m s : ℝ≥0∞) ↔
    (μ : (a : Set α) → ℝ≥0∞) s ≤ m s
Tactic: rcases s.eq_empty_or_nonempty with h | h