awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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 = ∞
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)
⊢ (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∞)

Tactic:
refine le_antisymm (measure_union_le _ _) (le_iInf₂ fun f hf ↦ ?_)

Premises used: le_antisymm, MeasureTheory.measure_union_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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
set :
  let μ := OuterMeasure.ofFunction m m_empty;
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≤
    ∑' (i : ℕ), m (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:
set μ := OuterMeasure.ofFunction m m_empty

Premises used: MeasureTheory.OuterMeasure.ofFunction
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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)
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)
⊢ 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)

Premises used: Exists, Inter.inter, And, Set.Nonempty, Classical.em
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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
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∞) ≤ ∞

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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
i : ℕ
hs : (s ∩ f i).Nonempty
ht : (t ∩ f i).Nonempty
⊢ ∞ = m (f i)

Tactic:
(h (f i) hs ht).symm

Premises used: Eq.symm
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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
i : ℕ
hs : (s ∩ f i).Nonempty
ht : (t ∩ f i).Nonempty
⊢ m (f i) ≤ ∑' (i : ℕ), m (f i)

Tactic:
ENNReal.le_tsum i

Premises used: ENNReal.le_tsum
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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
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:
calc
      μ s + μ t ≤ ∞ := le_top
      _ = m (f i) := (h (f i) hs ht).symm
      _ ≤ ∑' i, m (f i) := ENNReal.le_tsum i

Premises used: ENNReal.le_tsum, le_top, Eq.symm, DFunLike.coe
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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}
⊢ Disjoint (I s) (I t)

Tactic:
have hd : Disjoint (I s) (I t) := disjoint_iff_inf_le.mpr fun i hi => he ⟨i, hi⟩
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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)
⊢ ∀ 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 _
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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)
hI :
  ∀ u ⊆ s ∪ t,
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
      (∑' (i : (↑(I u) : Type)), (μ : (a : Set α) → ℝ≥0∞) (f (↑i : ℕ)) : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (∑' (i : (↑(I s) : Type)), (μ : (a : Set α) → ℝ≥0∞) (f (↑i : ℕ)))
      (∑' (i : (↑(I t) : Type)), (μ : (a : Set α) → ℝ≥0∞) (f (↑i : ℕ)))

Tactic:
add_le_add (hI _ subset_union_left) (hI _ subset_union_right)

Premises used: add_le_add, Set.subset_union_right, Set.subset_union_left
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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)
hI :
  ∀ u ⊆ s ∪ t,
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
      (∑' (i : (↑(I u) : Type)), (μ : (a : Set α) → ℝ≥0∞) (f (↑i : ℕ)) : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (∑' (i : (↑(I s) : Type)), (μ : (a : Set α) → ℝ≥0∞) (f (↑i : ℕ)))
      (∑' (i : (↑(I t) : Type)), (μ : (a : Set α) → ℝ≥0∞) (f (↑i : ℕ))) =
    ∑' (i : (↑(I s ∪ I t) : Type)), (μ : (a : Set α) → ℝ≥0∞) (f (↑i : ℕ))

Tactic:
(ENNReal.summable.tsum_union_disjoint (f := fun i => μ (f i)) hd ENNReal.summable).symm

Premises used: ENNReal.summable, Summable.tsum_union_disjoint, Eq.symm
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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)
hI :
  ∀ u ⊆ s ∪ t,
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
      (∑' (i : (↑(I u) : Type)), (μ : (a : Set α) → ℝ≥0∞) (f (↑i : ℕ)) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (∑' (i : (↑(I s ∪ I t) : Type)), (μ : (a : Set α) → ℝ≥0∞) (f (↑i : ℕ)))
    (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (f i))

Tactic:
(ENNReal.summable.tsum_le_tsum_of_inj (↑) Subtype.coe_injective (fun _ _ => zero_le)
        (fun _ => le_rfl) ENNReal.summable)

Premises used: zero_le, le_rfl, ENNReal.summable, Subtype.coe_injective, Summable.tsum_le_tsum_of_inj, Subtype.val
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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)
hI :
  ∀ u ⊆ s ∪ t,
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
      (∑' (i : (↑(I u) : Type)), (μ : (a : Set α) → ℝ≥0∞) (f (↑i : ℕ)) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (f i)) (∑' (i : ℕ), m (f i))

Tactic:
ENNReal.tsum_le_tsum fun i => ofFunction_le _

Premises used: ENNReal.tsum_le_tsum, MeasureTheory.OuterMeasure.ofFunction_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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)
hI :
  ∀ u ⊆ s ∪ t,
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
      (∑' (i : (↑(I u) : Type)), (μ : (a : Set α) → ℝ≥0∞) (f (↑i : ℕ)) : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≤
    ∑' (i : ℕ), m (f i)

Tactic:
calc
    μ s + μ t ≤ (∑' i : I s, μ (f i)) + ∑' i : I t, μ (f i) :=
      add_le_add (hI _ subset_union_left) (hI _ subset_union_right)
    _ = ∑' i : ↑(I s ∪ I t), μ (f i) :=
      (ENNReal.summable.tsum_union_disjoint (f := fun i => μ (f i)) hd ENNReal.summable).symm
    _ ≤ ∑' i, μ (f i) :=
      (ENNReal.summable.tsum_le_tsum_of_inj (↑) Subtype.coe_injective (fun _ _ => zero_le)
        (fun _ => le_rfl) ENNReal.summable)
    _ ≤ ∑' i, m (f i) := ENNReal.tsum_le_tsum fun i => ofFunction_le _

Premises used: zero_le, ENNReal.tsum_le_tsum, le_rfl, add_le_add, Set.subset_union_right, ENNReal.summable, Set.subset_union_left, tsum, Summable.tsum_union_disjoint, MeasureTheory.OuterMeasure.ofFunction_le, Summable.tsum_le_tsum_of_inj, Union.union, Eq.symm, Subtype.val, DFunLike.coe, SummationFilter.unconditional
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
simp : m ∅ = 0
⊢ Eq (α := ℝ≥0∞) ((fun (s : Set β) ↦ m (f '' s)) ∅) 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
⊢ m ∅ = 0

Tactic:
simp [m_empty]
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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 β)

Tactic:
le_antisymm (le_ofFunction.2 fun s => ?_) fun s => ?_

Premises used: Iff.mpr, le_antisymm, MeasureTheory.OuterMeasure.le_ofFunction
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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)
refine_2 :
  ∀ (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∞)
⊢ 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 β)

Tactic:
refine le_antisymm (le_ofFunction.2 fun s => ?_) fun s => ?_

Premises used: Iff.mpr, le_antisymm, MeasureTheory.OuterMeasure.le_ofFunction
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
⊢ (OuterMeasure.ofFunction m m_empty : (a : Set α) → ℝ≥0∞) (f '' s) ≤ m (f '' s)

Tactic:
apply ofFunction_le

Premises used: MeasureTheory.OuterMeasure.ofFunction_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
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))
⊢ 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∞)

Tactic:
rw [comap_apply, ofFunction_apply, ofFunction_apply]

Premises used: MeasureTheory.OuterMeasure.comap_apply, MeasureTheory.OuterMeasure.ofFunction_apply
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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))

Tactic:
iInf_mono' fun t => ⟨fun k => f ⁻¹' t k, ?_⟩

Premises used: Set.preimage, Exists.intro, iInf_mono'
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
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))
⊢ LE.le (α := ℝ≥0∞) (⨅ (t : ℕ → Set β), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (f '' t n))
    (⨅ (t : ℕ → Set α), ⨅ (_ : f '' s ⊆ iUnion t), ∑' (n : ℕ), m (t n))

Tactic:
refine iInf_mono' fun t => ⟨fun k => f ⁻¹' t k, ?_⟩

Premises used: Set.preimage, Exists.intro, iInf_mono'
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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))

Tactic:
iInf_mono' fun ht => ?_

Premises used: iInf_mono'
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
t : ℕ → Set α
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))
⊢ 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 ht => ?_

Premises used: iInf_mono'
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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 ⊆ ⋃ (i : ℕ), f ⁻¹' t i

Tactic:
rw [Set.image_subset_iff, preimage_iUnion] at ht

Premises used: Set.image_subset_iff, Set.preimage_iUnion
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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))

Tactic:
⟨ht, ENNReal.tsum_le_tsum fun n => ?_⟩

Premises used: ENNReal.tsum_le_tsum, Exists.intro
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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
refine_2 : ∀ (n : ℕ), m (f '' (fun (k : ℕ) ↦ f ⁻¹' t k) n) ≤ m (t n)
⊢ ∃ (_ : s ⊆ ⋃ (k : ℕ), f ⁻¹' t k),
    LE.le (α := ℝ≥0∞) (∑' (n : ℕ), m (f '' (fun (k : ℕ) ↦ f ⁻¹' t k) n)) (∑' (n : ℕ), m (t n))

Tactic:
refine ⟨ht, ENNReal.tsum_le_tsum fun n => ?_⟩
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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)
refine_2₁ : ∀ (hr : Surjective f), m (f '' (fun (k : ℕ) ↦ f ⁻¹' t k) n) ≤ m (t n)
⊢ m (f '' (fun (k : ℕ) ↦ f ⁻¹' t k) n) ≤ m (t n)

Tactic:
rcases h with hl | hr
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
s : Set β
t : ℕ → Set α
ht : s ⊆ ⋃ (i : ℕ), f ⁻¹' t i
n : ℕ
hl : Monotone m
⊢ m (f '' (fun (k : ℕ) ↦ f ⁻¹' t k) n) ≤ m (t n)

Tactic:
hl (image_preimage_subset _ _)

Premises used: Set.image_preimage_subset
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
s : Set β
t : ℕ → Set α
ht : s ⊆ ⋃ (i : ℕ), f ⁻¹' t i
n : ℕ
hr : Surjective f
⊢ m (f '' (fun (k : ℕ) ↦ f ⁻¹' t k) n) ≤ m (t n)

Tactic:
(congr_arg m (hr.image_preimage (t n))).le

Premises used: Eq.le, congr_arg, Function.Surjective.image_preimage
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
s : Set β
t : ℕ → Set α
ht : s ⊆ ⋃ (i : ℕ), f ⁻¹' t i
n : ℕ
hl : Monotone m
⊢ m (f '' (fun (k : ℕ) ↦ f ⁻¹' t k) n) ≤ m (t n)

Tactic:
exacts [hl (image_preimage_subset _ _), (congr_arg m (hr.image_preimage (t n))).le]

Premises used: Set.image_preimage_subset
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
s : Set β
⊢ (OuterMeasure.ofFunction m m_empty : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) ≤ m (f ⁻¹' s)

Tactic:
apply ofFunction_le

Premises used: MeasureTheory.OuterMeasure.ofFunction_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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

Tactic:
(map_ofFunction_le _).antisymm fun s => ?_

Premises used: LE.le.antisymm, MeasureTheory.OuterMeasure.map_ofFunction_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
hf : Injective f
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∞)
⊢ (map f : (a : OuterMeasure α) → OuterMeasure β) (OuterMeasure.ofFunction m m_empty) =
    OuterMeasure.ofFunction (fun (s : Set β) ↦ m (f ⁻¹' s)) m_empty

Tactic:
refine (map_ofFunction_le _).antisymm fun s => ?_

Premises used: LE.le.antisymm, MeasureTheory.OuterMeasure.map_ofFunction_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
hf : Injective f
s : Set β
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))
⊢ 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:
simp only [ofFunction_apply, map_apply, le_iInf_iff]

Premises used: MeasureTheory.OuterMeasure.map_apply, le_iInf_iff, MeasureTheory.OuterMeasure.ofFunction_apply
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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))

Tactic:
iInf_le_of_le (fun n => (range f)ᶜ ∪ f '' t n) (iInf_le_of_le ?_ ?_)

Premises used: Compl.compl, Set.image, Set.range, Union.union, iInf_le_of_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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
refine_2 : LE.le (α := ℝ≥0∞) (∑' (n : ℕ), m (f ⁻¹' (fun (n : ℕ) ↦ (range f)ᶜ ∪ f '' t n) n)) (∑' (n : ℕ), m (t n))
⊢ LE.le (α := ℝ≥0∞) (⨅ (t : ℕ → Set β), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (f ⁻¹' t n)) (∑' (n : ℕ), m (t n))

Tactic:
refine iInf_le_of_le (fun n => (range f)ᶜ ∪ f '' t n) (iInf_le_of_le ?_ ?_)

Premises used: Compl.compl, Set.image, Set.range, Union.union, iInf_le_of_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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 : f '' f ⁻¹' s ⊆ f '' ⋃ (i : ℕ), t i
⊢ s ⊆ ⋃ (n : ℕ), (range f)ᶜ ∪ f '' t n

Tactic:
rw [← union_iUnion, ← inter_subset, ← image_preimage_eq_inter_range, ← image_iUnion]

Premises used: Set.union_iUnion, Set.image_preimage_eq_inter_range, Set.image_iUnion, Set.inter_subset
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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
⊢ f '' f ⁻¹' s ⊆ f '' ⋃ (i : ℕ), t i

Tactic:
image_mono ht

Premises used: Set.image_mono
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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
⊢ f '' f ⁻¹' s ⊆ f '' ⋃ (i : ℕ), t i

Tactic:
exact image_mono ht

Premises used: Set.image_mono
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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))

Tactic:
ENNReal.tsum_le_tsum fun n => le_of_eq ?_

Premises used: ENNReal.tsum_le_tsum, le_of_eq