awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_2 : ∀ (n : ℕ), m (f ⁻¹' (fun (n : ℕ) ↦ (range f)ᶜ ∪ f '' t n) n) = m (t n)
⊢ LE.le (α := ℝ≥0∞) (∑' (n : ℕ), m (f ⁻¹' (fun (n : ℕ) ↦ (range f)ᶜ ∪ f '' t n) n)) (∑' (n : ℕ), m (t n))

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

Premises used: ENNReal.tsum_le_tsum, le_of_eq
-- 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
n : ℕ
⊢ m (f ⁻¹' (fun (n : ℕ) ↦ (range f)ᶜ ∪ f '' t n) n) = m (t n)

Tactic:
simp [hf.preimage_image]

Premises used: Function.Injective.preimage_image
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
simp : m ∅ = 0
⊢ Eq (α := ℝ≥0∞) ((fun (t : Set α) ↦ m (t ∩ s)) ∅) 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ m ∅ = 0

Tactic:
simp [m_empty]
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
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)) ⋯ : OuterMeasure α)
⊢ 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 α)

Tactic:
simp only [inter_comm _ s, LinearMap.comp_apply]

Premises used: LinearMap.comp_apply, Set.inter_comm
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
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)) ⋯) :
      OuterMeasure α)
    (OuterMeasure.ofFunction (fun (t : Set α) ↦ m (s ∩ t)) ⋯ : OuterMeasure α)
⊢ 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 α)

Tactic:
rw [comap_ofFunction _ (Or.inl hm)]

Premises used: Or.inl, MeasureTheory.OuterMeasure.comap_ofFunction
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ 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)) ⋯) :
      OuterMeasure α)
    (OuterMeasure.ofFunction (fun (t : Set α) ↦ m (s ∩ t)) ⋯ : OuterMeasure α)

Tactic:
simp only [map_ofFunction Subtype.coe_injective, Subtype.image_preimage_coe]

Premises used: Subtype.image_preimage_coe, MeasureTheory.OuterMeasure.map_ofFunction, Subtype.coe_injective
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
c : ℝ≥0∞
hc : c ≠ ∞
⊢ (c • m) ∅ = 0

Tactic:
simp [m_empty]
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
c : ℝ≥0∞
hc : c ≠ ∞
h :
  ∀ (s : Set α),
    Eq (α := ℝ≥0∞) ((c • OuterMeasure.ofFunction m m_empty : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((OuterMeasure.ofFunction (c • m) ⋯ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ c • OuterMeasure.ofFunction m m_empty = OuterMeasure.ofFunction (c • m) ⋯

Tactic:
ext1 s
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
c : ℝ≥0∞
hc : c ≠ ∞
s : Set α
⊢ 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⟩⟩
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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 }
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)
⊢ Eq (α := ℝ≥0∞) ((c • OuterMeasure.ofFunction m m_empty : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((OuterMeasure.ofFunction (c • m) ⋯ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [smul_apply, ofFunction_apply, ENNReal.tsum_mul_left, Pi.smul_apply, smul_eq_mul,
  iInf_subtype']

Premises used: ENNReal.tsum_mul_left, iInf_subtype', smul_eq_mul, MeasureTheory.OuterMeasure.ofFunction_apply, MeasureTheory.OuterMeasure.smul_apply, Pi.smul_apply
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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 }
h 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))
⊢ 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:
rw [ENNReal.mul_iInf fun h => (hc h).elim]

Premises used: ENNReal.mul_iInf, False.elim
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
⊢ Eq (α := ℝ≥0∞) ((fun (s : Set α) ↦ (⨆ (_ : s.Nonempty), m s : ℝ≥0∞)) ∅) 0

Tactic:
simp [Set.not_nonempty_empty]

Premises used: Set.not_nonempty_empty
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
⊢ (boundedBy m : (a : Set α) → ℝ≥0∞) s ≤ m s

Tactic:
(ofFunction_le _).trans iSup_const_le

Premises used: MeasureTheory.OuterMeasure.ofFunction_le, LE.le.trans, iSup_const_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
h : ∀ (t : Set α), ⨆ (_ : t.Nonempty), m t = m t
⊢ (fun (s : Set α) ↦ ⨆ (_ : s.Nonempty), m s) = m

Tactic:
ext1 t
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
h : ∀ (h : t = ∅), ⨆ (_ : t.Nonempty), m t = m t
h₁ : ∀ (h : t.Nonempty), ⨆ (_ : t.Nonempty), m t = m t
⊢ ⨆ (_ : t.Nonempty), m t = m t

Tactic:
rcases t.eq_empty_or_nonempty with h | h

Premises used: Set.eq_empty_or_nonempty
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
h : t = ∅
⊢ ⨆ (_ : t.Nonempty), m t = m t

Tactic:
simp [h, Set.not_nonempty_empty, m_empty]

Premises used: Set.not_nonempty_empty
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
h : t.Nonempty
⊢ ⨆ (_ : t.Nonempty), m t = m t

Tactic:
simp [h, Set.not_nonempty_empty, m_empty]

Premises used: Set.not_nonempty_empty
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
⊢ (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]
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
this : (fun (s : Set α) ↦ ⨆ (_ : s.Nonempty), m s) = m
⊢ Eq (α := ℝ≥0∞) ((boundedBy m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((OuterMeasure.ofFunction m m_empty : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [boundedBy, this]

Premises used: MeasureTheory.OuterMeasure.boundedBy
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
⊢ Eq (α := ℝ≥0∞) ((boundedBy m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (t n) : ℝ≥0∞)

Tactic:
simp [boundedBy, ofFunction_apply]

Premises used: MeasureTheory.OuterMeasure.boundedBy, MeasureTheory.OuterMeasure.ofFunction_apply
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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
rw₁ rw₂ : m s = m s
⊢ (boundedBy m : (a : Set α) → ℝ≥0∞) s = m s

Tactic:
rw [boundedBy_eq_ofFunction m_empty, ofFunction_eq s m_mono m_subadd]

Premises used: MeasureTheory.OuterMeasure.boundedBy_eq_ofFunction, MeasureTheory.OuterMeasure.ofFunction_eq
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : OuterMeasure α
⊢ boundedBy (⇑m : (a : Set α) → ℝ≥0∞) = m

Tactic:
ext fun _ => boundedBy_eq _ measure_empty (fun _ ht => measure_mono ht) measure_iUnion_le

Premises used: MeasureTheory.OuterMeasure.boundedBy_eq, MeasureTheory.measure_empty, MeasureTheory.measure_iUnion_le, MeasureTheory.measure_mono, MeasureTheory.OuterMeasure.ext
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
rw :
  ∀ (a : Set α),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) (⨆ (_ : a.Nonempty), m a : ℝ≥0∞) ↔
      (μ : (a : Set α) → ℝ≥0∞) a ≤ m a
⊢ μ ≤ boundedBy m ↔ ∀ (s : Set α), (μ : (a : Set α) → ℝ≥0∞) s ≤ m s

Tactic:
rw [boundedBy, le_ofFunction, forall_congr']

Premises used: MeasureTheory.OuterMeasure.boundedBy, forall_congr', MeasureTheory.OuterMeasure.le_ofFunction
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
s : Set α
inl :
  ∀ (h : s = ∅),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (⨆ (_ : s.Nonempty), m s : ℝ≥0∞) ↔
      (μ : (a : Set α) → ℝ≥0∞) s ≤ m s
inr :
  ∀ (h : s.Nonempty),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (⨆ (_ : s.Nonempty), m s : ℝ≥0∞) ↔
      (μ : (a : Set α) → ℝ≥0∞) s ≤ m 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

Premises used: Set.eq_empty_or_nonempty
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
s : Set α
h : s = ∅
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (⨆ (_ : s.Nonempty), m s : ℝ≥0∞) ↔
    (μ : (a : Set α) → ℝ≥0∞) s ≤ m s

Tactic:
simp [h, Set.not_nonempty_empty]

Premises used: Set.not_nonempty_empty
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
s : Set α
h : s.Nonempty
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (⨆ (_ : s.Nonempty), m s : ℝ≥0∞) ↔
    (μ : (a : Set α) → ℝ≥0∞) s ≤ m s

Tactic:
simp [h, Set.not_nonempty_empty]

Premises used: Set.not_nonempty_empty
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
rw : ∀ (a : Set α), (μ : (a : Set α) → ℝ≥0∞) a ≤ m a ↔ a.Nonempty → (μ : (a : Set α) → ℝ≥0∞) a ≤ m a
⊢ μ ≤ boundedBy m ↔ ∀ (s : Set α), s.Nonempty → (μ : (a : Set α) → ℝ≥0∞) s ≤ m s

Tactic:
rw [le_boundedBy, forall_congr']

Premises used: forall_congr', MeasureTheory.OuterMeasure.le_boundedBy
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
s : Set α
inl : ∀ (h : s = ∅), (μ : (a : Set α) → ℝ≥0∞) s ≤ m s ↔ s.Nonempty → (μ : (a : Set α) → ℝ≥0∞) s ≤ m s
inr : ∀ (h : s.Nonempty), (μ : (a : Set α) → ℝ≥0∞) s ≤ m s ↔ s.Nonempty → (μ : (a : Set α) → ℝ≥0∞) s ≤ m s
⊢ (μ : (a : Set α) → ℝ≥0∞) s ≤ m s ↔ s.Nonempty → (μ : (a : Set α) → ℝ≥0∞) s ≤ m s

Tactic:
rcases s.eq_empty_or_nonempty with h | h

Premises used: Set.eq_empty_or_nonempty
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
s : Set α
h : s = ∅
⊢ (μ : (a : Set α) → ℝ≥0∞) s ≤ m s ↔ s.Nonempty → (μ : (a : Set α) → ℝ≥0∞) s ≤ m s

Tactic:
simp [h]
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
s : Set α
h : s.Nonempty
⊢ (μ : (a : Set α) → ℝ≥0∞) s ≤ m s ↔ s.Nonempty → (μ : (a : Set α) → ℝ≥0∞) s ≤ m s

Tactic:
simp [h]
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
rw : ∀ (s : Set α), s.Nonempty → LE.le (α := ℝ≥0∞) (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (⊤ s : ℝ≥0∞)
⊢ Eq.{u_1 + 1} (α := OuterMeasure α) (boundedBy ⊤) ⊤

Tactic:
rw [eq_top_iff, le_boundedBy']

Premises used: MeasureTheory.OuterMeasure.le_boundedBy', eq_top_iff
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
s : Set α
hs : s.Nonempty
rw : LE.le (α := ℝ≥0∞) ∞ (⊤ s)
⊢ LE.le (α := ℝ≥0∞) (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (⊤ s : ℝ≥0∞)

Tactic:
rw [top_apply hs]

Premises used: MeasureTheory.OuterMeasure.top_apply
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
s : Set α
hs : s.Nonempty
⊢ LE.le (α := ℝ≥0∞) ∞ (⊤ s)

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
s : Set α
hs : s.Nonempty
⊢ LE.le (α := ℝ≥0∞) ∞ (⊤ s)

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
simp :
  OuterMeasure.ofFunction (HSMul.hSMul (β := Set α → ℝ≥0∞) c fun (s : Set α) ↦ ⨆ (_ : s.Nonempty), m s) ⋯ =
    OuterMeasure.ofFunction (fun (s : Set α) ↦ ⨆ (_ : s.Nonempty), (c • m) s) ⋯
⊢ c • boundedBy m = boundedBy (c • m)

Tactic:
simp only [boundedBy, smul_ofFunction hc]

Premises used: MeasureTheory.OuterMeasure.boundedBy, MeasureTheory.OuterMeasure.smul_ofFunction
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
e_m :
  ∀ (s : Set α),
    HSMul.hSMul (β := Set α → ℝ≥0∞) c (fun (s : Set α) ↦ ⨆ (_ : s.Nonempty), m s) s = ⨆ (_ : s.Nonempty), (c • m) s
⊢ OuterMeasure.ofFunction (HSMul.hSMul (β := Set α → ℝ≥0∞) c fun (s : Set α) ↦ ⨆ (_ : s.Nonempty), m s) ⋯ =
    OuterMeasure.ofFunction (fun (s : Set α) ↦ ⨆ (_ : s.Nonempty), (c • m) s) ⋯

Tactic:
congr 1 with s : 1
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
s : Set α
e_m :
  HSMul.hSMul (β := Set α → ℝ≥0∞) c (fun (s : Set α) ↦ ⨆ (_ : s.Nonempty), m s) ∅ =
    ⨆ (_ : Set.Nonempty.{u_1} (α := α) ∅), (c • m) ∅
e_m₁ :
  ∀ (hs : s.Nonempty),
    HSMul.hSMul (β := Set α → ℝ≥0∞) c (fun (s : Set α) ↦ ⨆ (_ : s.Nonempty), m s) s = ⨆ (_ : s.Nonempty), (c • m) s
⊢ HSMul.hSMul (β := Set α → ℝ≥0∞) c (fun (s : Set α) ↦ ⨆ (_ : s.Nonempty), m s) s = ⨆ (_ : s.Nonempty), (c • m) s

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hs)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
⊢ HSMul.hSMul (β := Set α → ℝ≥0∞) c (fun (s : Set α) ↦ ⨆ (_ : s.Nonempty), m s) ∅ =
    ⨆ (_ : Set.Nonempty.{u_1} (α := α) ∅), (c • m) ∅

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
s : Set α
hs : s.Nonempty
⊢ HSMul.hSMul (β := Set α → ℝ≥0∞) c (fun (s : Set α) ↦ ⨆ (_ : s.Nonempty), m s) s = ⨆ (_ : s.Nonempty), (c • m) s

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
β : Type u_2
f : β → α
h : (Monotone (β := ℝ≥0∞) fun (s : { s : Set α // s.Nonempty }) ↦ m (↑s : Set α)) ∨ Surjective f
⊢ Eq.{u_2 + 1} (α := OuterMeasure β) ((comap f : (a : OuterMeasure α) → OuterMeasure β) (boundedBy m) : OuterMeasure β)
    (boundedBy fun (s : Set β) ↦ m (f '' s) : OuterMeasure β)

Tactic:
(comap_ofFunction _ ?_).trans ?_

Premises used: MeasureTheory.OuterMeasure.comap_ofFunction, Eq.trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
β : Type u_2
f : β → α
h : (Monotone (β := ℝ≥0∞) fun (s : { s : Set α // s.Nonempty }) ↦ m (↑s : Set α)) ∨ Surjective f
refine_1 : (Monotone (β := ℝ≥0∞) fun (s : Set α) ↦ ⨆ (_ : s.Nonempty), m s) ∨ Surjective f
refine_2 :
  Eq.{u_2 + 1} (α := OuterMeasure β)
    (OuterMeasure.ofFunction (fun (s : Set β) ↦ ⨆ (_ : (f '' s).Nonempty), m (f '' s)) ⋯)
    (boundedBy fun (s : Set β) ↦ m (f '' s))
⊢ Eq.{u_2 + 1} (α := OuterMeasure β) ((comap f : (a : OuterMeasure α) → OuterMeasure β) (boundedBy m) : OuterMeasure β)
    (boundedBy fun (s : Set β) ↦ m (f '' s) : OuterMeasure β)

Tactic:
refine (comap_ofFunction _ ?_).trans ?_

Premises used: MeasureTheory.OuterMeasure.comap_ofFunction, Eq.trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
β : Type u_2
f : β → α
h : (Monotone (β := ℝ≥0∞) fun (s : { s : Set α // s.Nonempty }) ↦ m (↑s : Set α)) ∨ Surjective f
⊢ (Monotone (β := ℝ≥0∞) fun (s : Set α) ↦ ⨆ (_ : s.Nonempty), m s) ∨ Surjective f

Tactic:
h.imp (fun H s t hst => iSup_le fun hs => ?_) id

Premises used: id, iSup_le, Or.imp
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
β : Type u_2
f : β → α
h : (Monotone (β := ℝ≥0∞) fun (s : { s : Set α // s.Nonempty }) ↦ m (↑s : Set α)) ∨ Surjective f
refine_1 :
  ∀ (H : Monotone (β := ℝ≥0∞) fun (s : { s : Set α // s.Nonempty }) ↦ m (↑s : Set α)) (s t : Set α) (hst : s ≤ t)
    (hs : s.Nonempty), m s ≤ (fun (s : Set α) ↦ (⨆ (_ : s.Nonempty), m s : ℝ≥0∞)) t
⊢ (Monotone (β := ℝ≥0∞) fun (s : Set α) ↦ ⨆ (_ : s.Nonempty), m s) ∨ Surjective f

Tactic:
refine h.imp (fun H s t hst => iSup_le fun hs => ?_) id

Premises used: id, Or.imp
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
β : Type u_2
f : β → α
h : (Monotone (β := ℝ≥0∞) fun (s : { s : Set α // s.Nonempty }) ↦ m (↑s : Set α)) ∨ Surjective f
H : Monotone (β := ℝ≥0∞) fun (s : { s : Set α // s.Nonempty }) ↦ m (↑s : Set α)
s t : Set α
hst : s ≤ t
hs : s.Nonempty
⊢ t.Nonempty

Tactic:
have ht : t.Nonempty := hs.mono hst
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
β : Type u_2
f : β → α
h : (Monotone (β := ℝ≥0∞) fun (s : { s : Set α // s.Nonempty }) ↦ m (↑s : Set α)) ∨ Surjective f
H : Monotone (β := ℝ≥0∞) fun (s : { s : Set α // s.Nonempty }) ↦ m (↑s : Set α)
s t : Set α
hst : s ≤ t
hs : s.Nonempty
ht : t.Nonempty
⊢ m s ≤ (fun (s : Set α) ↦ (⨆ (_ : s.Nonempty), m s : ℝ≥0∞)) t

Tactic:
(@H ⟨s, hs⟩ ⟨t, ht⟩ hst).trans (le_iSup (fun _ : t.Nonempty => m t) ht)

Premises used: le_iSup, LE.le.trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
β : Type u_2
f : β → α
h : (Monotone (β := ℝ≥0∞) fun (s : { s : Set α // s.Nonempty }) ↦ m (↑s : Set α)) ∨ Surjective f
H : Monotone (β := ℝ≥0∞) fun (s : { s : Set α // s.Nonempty }) ↦ m (↑s : Set α)
s t : Set α
hst : s ≤ t
hs : s.Nonempty
ht : t.Nonempty
⊢ m s ≤ (fun (s : Set α) ↦ (⨆ (_ : s.Nonempty), m s : ℝ≥0∞)) t

Tactic:
exact (@H ⟨s, hs⟩ ⟨t, ht⟩ hst).trans (le_iSup (fun _ : t.Nonempty => m t) ht)

Premises used: le_iSup, LE.le.trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
β : Type u_2
f : β → α
h : (Monotone (β := ℝ≥0∞) fun (s : { s : Set α // s.Nonempty }) ↦ m (↑s : Set α)) ∨ Surjective f
refine_2 :
  Eq.{u_2 + 1} (α := OuterMeasure β)
    (OuterMeasure.ofFunction (fun (s : Set β) ↦ ⨆ (_ : (f '' s).Nonempty), m (f '' s)) ⋯)
    (OuterMeasure.ofFunction (fun (s : Set β) ↦ ⨆ (_ : s.Nonempty), m (f '' s)) ⋯)
⊢ Eq.{u_2 + 1} (α := OuterMeasure β)
    (OuterMeasure.ofFunction (fun (s : Set β) ↦ ⨆ (_ : (f '' s).Nonempty), m (f '' s)) ⋯)
    (boundedBy fun (s : Set β) ↦ m (f '' s))

Tactic:
dsimp only [boundedBy]

Premises used: MeasureTheory.OuterMeasure.boundedBy
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
β : Type u_2
f : β → α
h : (Monotone (β := ℝ≥0∞) fun (s : { s : Set α // s.Nonempty }) ↦ m (↑s : Set α)) ∨ Surjective f
refine_2 : ∀ (s : Set β), Eq (α := ℝ≥0∞) (⨆ (_ : (f '' s).Nonempty), m (f '' s)) (⨆ (_ : s.Nonempty), m (f '' s))
⊢ Eq.{u_2 + 1} (α := OuterMeasure β)
    (OuterMeasure.ofFunction (fun (s : Set β) ↦ ⨆ (_ : (f '' s).Nonempty), m (f '' s)) ⋯)
    (OuterMeasure.ofFunction (fun (s : Set β) ↦ ⨆ (_ : s.Nonempty), m (f '' s)) ⋯)

Tactic:
congr with s : 1
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
β : Type u_2
f : β → α
h : (Monotone (β := ℝ≥0∞) fun (s : { s : Set α // s.Nonempty }) ↦ m (↑s : Set α)) ∨ Surjective f
s : Set β
refine_2 refine_2₁ : Eq (α := ℝ≥0∞) (⨆ (_ : s.Nonempty), m (f '' s)) (⨆ (_ : s.Nonempty), m (f '' s))
⊢ Eq (α := ℝ≥0∞) (⨆ (_ : (f '' s).Nonempty), m (f '' s)) (⨆ (_ : s.Nonempty), m (f '' s))

Tactic:
rw [image_nonempty]

Premises used: Set.image_nonempty
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
s t : Set α
h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ∞
⊢ (boundedBy m : (a : Set α) → ℝ≥0∞) (s ∪ t) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((boundedBy m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((boundedBy m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
ofFunction_union_of_top_of_nonempty_inter fun u hs ht =>
    top_unique <| (h u hs ht).ge.trans <| le_iSup (fun _ => m u) (hs.mono inter_subset_right)

Premises used: Eq.ge, le_iSup, Set.Nonempty.mono, top_unique, MeasureTheory.OuterMeasure.ofFunction_union_of_top_of_nonempty_inter, LE.le.trans, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set (OuterMeasure α)
t : Set α
⊢ sInfGen m t = ⨅ μ ∈ m, (μ : (a : Set α) → ℝ≥0∞) t

Tactic:
rfl

Premises used: MeasureTheory.OuterMeasure.sInfGen, rfl
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set (OuterMeasure α)
⊢ sInf m = boundedBy (sInfGen m)

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set (OuterMeasure α)
refine_1 : sInf m ≤ boundedBy (sInfGen m)
refine_2 : boundedBy (sInfGen m) ≤ sInf m
⊢ sInf m = boundedBy (sInfGen m)

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set (OuterMeasure α)
⊢ sInf m ≤ boundedBy (sInfGen m)

Tactic:
le_boundedBy.2 fun s => le_iInf₂ fun μ hμ => ?_

Premises used: Iff.mpr, le_iInf₂, MeasureTheory.OuterMeasure.le_boundedBy
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set (OuterMeasure α)
refine_1 :
  ∀ (s : Set α) (μ : OuterMeasure α) (hμ : μ ∈ m),
    LE.le (α := ℝ≥0∞) ((sInf m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ sInf m ≤ boundedBy (sInfGen m)

Tactic:
refine le_boundedBy.2 fun s => le_iInf₂ fun μ hμ => ?_

Premises used: Iff.mpr, le_iInf₂, MeasureTheory.OuterMeasure.le_boundedBy
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set (OuterMeasure α)
s : Set α
μ : OuterMeasure α
hμ : μ ∈ m
⊢ LE.le (α := ℝ≥0∞) ((sInf m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
apply sInf_le hμ

Premises used: sInf_le