awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set (OuterMeasure α)
⊢ boundedBy (sInfGen m) ≤ sInf m

Tactic:
le_sInf ?_

Premises used: le_sInf
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set (OuterMeasure α)
refine_2 : ∀ b ∈ m, boundedBy (sInfGen m) ≤ b
⊢ boundedBy (sInfGen m) ≤ sInf m

Tactic:
refine le_sInf ?_

Premises used: le_sInf
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set (OuterMeasure α)
μ : OuterMeasure α
hμ : μ ∈ m
t : Set α
⊢ LE.le (α := ℝ≥0∞) ((boundedBy (sInfGen m) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
le_trans (boundedBy_le t) (iInf₂_le μ hμ)

Premises used: iInf₂_le, MeasureTheory.OuterMeasure.boundedBy_le, le_trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set (OuterMeasure α)
μ : OuterMeasure α
hμ : μ ∈ m
t : Set α
⊢ LE.le (α := ℝ≥0∞) ((boundedBy (sInfGen m) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
exact le_trans (boundedBy_le t) (iInf₂_le μ hμ)

Premises used: MeasureTheory.OuterMeasure.boundedBy_le, le_trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set (OuterMeasure α)
h : m.Nonempty
t : Set α
inl : Eq (α := ℝ≥0∞) (⨆ (_ : Set.Nonempty.{u_1} (α := α) ∅), sInfGen m ∅) (⨅ μ ∈ m, (μ : (a : Set α) → ℝ≥0∞) ∅)
inr : ∀ (ht : t.Nonempty), Eq (α := ℝ≥0∞) (⨆ (_ : t.Nonempty), sInfGen m t) (⨅ μ ∈ m, (μ : (a : Set α) → ℝ≥0∞) t)
⊢ Eq (α := ℝ≥0∞) (⨆ (_ : t.Nonempty), sInfGen m t) (⨅ μ ∈ m, (μ : (a : Set α) → ℝ≥0∞) t)

Tactic:
rcases t.eq_empty_or_nonempty with (rfl | ht)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set (OuterMeasure α)
h : m.Nonempty
⊢ Eq (α := ℝ≥0∞) (⨆ (_ : Set.Nonempty.{u_1} (α := α) ∅), sInfGen m ∅) (⨅ μ ∈ m, (μ : (a : Set α) → ℝ≥0∞) ∅)

Tactic:
simp [biInf_const h]

Premises used: biInf_const
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set (OuterMeasure α)
h : m.Nonempty
t : Set α
ht : t.Nonempty
⊢ Eq (α := ℝ≥0∞) (⨆ (_ : t.Nonempty), sInfGen m t) (⨅ μ ∈ m, (μ : (a : Set α) → ℝ≥0∞) t)

Tactic:
simp [ht, sInfGen_def]

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

Tactic:
simp_rw [sInf_eq_boundedBy_sInfGen, boundedBy_apply, iSup_sInfGen_nonempty h]

Premises used: MeasureTheory.OuterMeasure.boundedBy_apply, MeasureTheory.OuterMeasure.sInf_eq_boundedBy_sInfGen, MeasureTheory.OuterMeasure.iSup_sInfGen_nonempty
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set (OuterMeasure α)
s : Set α
h : s.Nonempty
hm : m = ∅
⊢ Eq (α := ℝ≥0∞) ((sInf m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ μ ∈ m, (μ : (a : Set α) → ℝ≥0∞) (t n) : ℝ≥0∞)

Tactic:
simp [hm, h]
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
ι : Sort u_2
inst : Nonempty ι
m : ι → OuterMeasure α
s : Set α
rw :
  Eq (α := ℝ≥0∞) (⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ μ ∈ range m, (μ : (a : Set α) → ℝ≥0∞) (t n))
    (⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ (i : ι), (m i : (a : Set α) → ℝ≥0∞) (t n))
⊢ Eq (α := ℝ≥0∞) (((⨅ (i : ι), m i : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ (i : ι), (m i : (a : Set α) → ℝ≥0∞) (t n) : ℝ≥0∞)

Tactic:
rw [iInf, sInf_apply (range_nonempty m)]

Premises used: iInf, MeasureTheory.OuterMeasure.sInf_apply, Set.range_nonempty
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
ι : Sort u_2
inst : Nonempty ι
m : ι → OuterMeasure α
s : Set α
⊢ Eq (α := ℝ≥0∞) (⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ μ ∈ range m, (μ : (a : Set α) → ℝ≥0∞) (t n))
    (⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ (i : ι), (m i : (a : Set α) → ℝ≥0∞) (t n))

Tactic:
simp only [iInf_range]

Premises used: iInf_range
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
ι : Sort u_2
m : ι → OuterMeasure α
s : Set α
hs : s.Nonempty
rw :
  Eq (α := ℝ≥0∞)
    (⨅ (t : ℕ → Set α),
      ⨅ (_ : s ⊆ iUnion t),
        ∑' (n : ℕ),
          ⨅ (μ : OuterMeasure α),
            ⨅ (_ : Membership.mem (γ := Set (OuterMeasure α)) (range fun (i : ι) ↦ m i) μ),
              (μ : (a : Set α) → ℝ≥0∞) (t n))
    (⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ (i : ι), (m i : (a : Set α) → ℝ≥0∞) (t n))
⊢ Eq (α := ℝ≥0∞) (((⨅ (i : ι), m i : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ (i : ι), (m i : (a : Set α) → ℝ≥0∞) (t n) : ℝ≥0∞)

Tactic:
rw [iInf, sInf_apply' hs]

Premises used: iInf, MeasureTheory.OuterMeasure.sInf_apply'
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
ι : Sort u_2
m : ι → OuterMeasure α
s : Set α
hs : s.Nonempty
⊢ Eq (α := ℝ≥0∞)
    (⨅ (t : ℕ → Set α),
      ⨅ (_ : s ⊆ iUnion t),
        ∑' (n : ℕ),
          ⨅ (μ : OuterMeasure α),
            ⨅ (_ : Membership.mem (γ := Set (OuterMeasure α)) (range fun (i : ι) ↦ m i) μ),
              (μ : (a : Set α) → ℝ≥0∞) (t n))
    (⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ (i : ι), (m i : (a : Set α) → ℝ≥0∞) (t n))

Tactic:
simp only [iInf_range]

Premises used: iInf_range
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
ι : Type u_2
I : Set ι
hI : I.Nonempty
m : ι → OuterMeasure α
s : Set α
⊢ Nonempty.{u_2 + 1} (↑I : Type u_2)

Tactic:
haveI := hI.to_subtype
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
ι : Type u_2
I : Set ι
hI : I.Nonempty
m : ι → OuterMeasure α
s : Set α
this : Nonempty.{u_2 + 1} (↑I : Type u_2)
⊢ Eq (α := ℝ≥0∞) (((⨅ i ∈ I, m i : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ i ∈ I, (m i : (a : Set α) → ℝ≥0∞) (t n) : ℝ≥0∞)

Tactic:
simp only [← iInf_subtype'', iInf_apply]

Premises used: MeasureTheory.OuterMeasure.iInf_apply, iInf_subtype''
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
ι : Type u_2
I : Set ι
m : ι → OuterMeasure α
s : Set α
hs : s.Nonempty
⊢ Eq (α := ℝ≥0∞) (((⨅ i ∈ I, m i : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ i ∈ I, (m i : (a : Set α) → ℝ≥0∞) (t n) : ℝ≥0∞)

Tactic:
simp only [← iInf_subtype'', iInf_apply' _ hs]

Premises used: MeasureTheory.OuterMeasure.iInf_apply', iInf_subtype''
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
ι : Sort u_2
β : Type u_3
f : α → β
m : ι → OuterMeasure α
⊢ LE.le.{u_3} (α := OuterMeasure β) ((map f : (a : OuterMeasure α) → OuterMeasure β) (⨅ (i : ι), m i))
    (⨅ (i : ι), (map f : (a : OuterMeasure α) → OuterMeasure β) (m i))

Tactic:
(map_mono f).map_iInf_le

Premises used: Monotone.map_iInf_le, MeasureTheory.OuterMeasure.map_mono
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
ι : Sort u_2
β : Type u_3
f : α → β
m : ι → OuterMeasure β
⊢ Eq.{u_1 + 1} (α := OuterMeasure α) ((comap f : (a : OuterMeasure β) → OuterMeasure α) (⨅ (i : ι), m i))
    (⨅ (i : ι), (comap f : (a : OuterMeasure β) → OuterMeasure α) (m i))

Tactic:
ext_nonempty fun s hs => ?_

Premises used: MeasureTheory.OuterMeasure.ext_nonempty
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
ι : Sort u_2
β : Type u_3
f : α → β
m : ι → OuterMeasure β
refine :
  ∀ (s : Set α) (hs : s.Nonempty),
    Eq (α := ℝ≥0∞)
      ((((comap f : (a : OuterMeasure β) → OuterMeasure α) (⨅ (i : ι), m i) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s :
        ℝ≥0∞)
      (((⨅ (i : ι), (comap f : (a : OuterMeasure β) → OuterMeasure α) (m i) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s :
        ℝ≥0∞)
⊢ Eq.{u_1 + 1} (α := OuterMeasure α) ((comap f : (a : OuterMeasure β) → OuterMeasure α) (⨅ (i : ι), m i))
    (⨅ (i : ι), (comap f : (a : OuterMeasure β) → OuterMeasure α) (m i))

Tactic:
refine ext_nonempty fun s hs => ?_

Premises used: MeasureTheory.OuterMeasure.ext_nonempty
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
ι : Sort u_2
β : Type u_3
f : α → β
m : ι → OuterMeasure β
s : Set α
hs : s.Nonempty
⊢ Eq (α := ℝ≥0∞)
    ((((comap f : (a : OuterMeasure β) → OuterMeasure α) (⨅ (i : ι), m i) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s :
      ℝ≥0∞)
    (((⨅ (i : ι), (comap f : (a : OuterMeasure β) → OuterMeasure α) (m i) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s :
      ℝ≥0∞)

Tactic:
((comap_mono f).map_iInf_le s).antisymm ?_

Premises used: LE.le.antisymm, Monotone.map_iInf_le, MeasureTheory.OuterMeasure.comap_mono
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
ι : Sort u_2
β : Type u_3
f : α → β
m : ι → OuterMeasure β
s : Set α
hs : s.Nonempty
refine :
  LE.le (α := ℝ≥0∞)
    (((⨅ (i : ι), (comap f : (a : OuterMeasure β) → OuterMeasure α) (m i) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s :
      ℝ≥0∞)
    ((((comap f : (a : OuterMeasure β) → OuterMeasure α) (⨅ (i : ι), m i) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((comap f : (a : OuterMeasure β) → OuterMeasure α) (⨅ (i : ι), m i) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s :
      ℝ≥0∞)
    (((⨅ (i : ι), (comap f : (a : OuterMeasure β) → OuterMeasure α) (m i) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s :
      ℝ≥0∞)

Tactic:
refine ((comap_mono f).map_iInf_le s).antisymm ?_

Premises used: LE.le.antisymm, Monotone.map_iInf_le, MeasureTheory.OuterMeasure.comap_mono
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
ι : Sort u_2
β : Type u_3
f : α → β
m : ι → OuterMeasure β
s : Set α
hs : s.Nonempty
simp :
  ∀ (i : ℕ → Set β) (i_1 : s ⊆ ⋃ (i_1 : ℕ), f ⁻¹' i i_1),
    LE.le (α := ℝ≥0∞)
      (⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ (i : ι), (m i : (a : Set β) → ℝ≥0∞) (f '' t n))
      (∑' (n : ℕ), ⨅ (i_2 : ι), (m i_2 : (a : Set β) → ℝ≥0∞) (i n))
⊢ LE.le (α := ℝ≥0∞)
    (((⨅ (i : ι), (comap f : (a : OuterMeasure β) → OuterMeasure α) (m i) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s :
      ℝ≥0∞)
    ((((comap f : (a : OuterMeasure β) → OuterMeasure α) (⨅ (i : ι), m i) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s :
      ℝ≥0∞)

Tactic:
simp only [comap_apply, iInf_apply' _ hs, iInf_apply' _ (hs.image _), le_iInf_iff,
    Set.image_subset_iff, preimage_iUnion]

Premises used: MeasureTheory.OuterMeasure.iInf_apply', MeasureTheory.OuterMeasure.comap_apply, le_iInf_iff, Set.Nonempty.image, Set.image_subset_iff, Set.preimage_iUnion
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
ι : Sort u_2
β : Type u_3
f : α → β
m : ι → OuterMeasure β
s : Set α
hs : s.Nonempty
⊢ ∀ (i : ℕ → Set β) (i_1 : s ⊆ ⋃ (i_1 : ℕ), f ⁻¹' i i_1),
    LE.le (α := ℝ≥0∞)
      (⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ (i : ι), (m i : (a : Set β) → ℝ≥0∞) (f '' t n))
      (∑' (n : ℕ), ⨅ (i_2 : ι), (m i_2 : (a : Set β) → ℝ≥0∞) (i n))

Tactic:
fun t ht => iInf_le_of_le _ (iInf_le_of_le ht <| ENNReal.tsum_le_tsum fun k => ?_)

Premises used: ENNReal.tsum_le_tsum, Set.preimage, iInf_le_of_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
ι : Sort u_2
β : Type u_3
f : α → β
m : ι → OuterMeasure β
s : Set α
hs : s.Nonempty
refine :
  ∀ (t : ℕ → Set β) (ht : s ⊆ ⋃ (i : ℕ), f ⁻¹' t i) (k : ℕ),
    LE.le (α := ℝ≥0∞) (⨅ (i : ι), (m i : (a : Set β) → ℝ≥0∞) (f '' f ⁻¹' t k))
      (⨅ (i : ι), (m i : (a : Set β) → ℝ≥0∞) (t k))
⊢ ∀ (i : ℕ → Set β) (i_1 : s ⊆ ⋃ (i_1 : ℕ), f ⁻¹' i i_1),
    LE.le (α := ℝ≥0∞)
      (⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ (i : ι), (m i : (a : Set β) → ℝ≥0∞) (f '' t n))
      (∑' (n : ℕ), ⨅ (i_2 : ι), (m i_2 : (a : Set β) → ℝ≥0∞) (i n))

Tactic:
refine fun t ht => iInf_le_of_le _ (iInf_le_of_le ht <| ENNReal.tsum_le_tsum fun k => ?_)

Premises used: iInf_le_of_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
ι : Sort u_2
β : Type u_3
f : α → β
m : ι → OuterMeasure β
s : Set α
hs : s.Nonempty
t : ℕ → Set β
ht : s ⊆ ⋃ (i : ℕ), f ⁻¹' t i
k : ℕ
⊢ LE.le (α := ℝ≥0∞) (⨅ (i : ι), (m i : (a : Set β) → ℝ≥0∞) (f '' f ⁻¹' t k))
    (⨅ (i : ι), (m i : (a : Set β) → ℝ≥0∞) (t k))

Tactic:
iInf_mono fun i => (m i).mono (image_preimage_subset _ _)

Premises used: MeasureTheory.OuterMeasure.mono, iInf_mono, Set.image_preimage_subset
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
ι : Sort u_2
β : Type u_3
f : α → β
m : ι → OuterMeasure β
s : Set α
hs : s.Nonempty
t : ℕ → Set β
ht : s ⊆ ⋃ (i : ℕ), f ⁻¹' t i
k : ℕ
⊢ LE.le (α := ℝ≥0∞) (⨅ (i : ι), (m i : (a : Set β) → ℝ≥0∞) (f '' f ⁻¹' t k))
    (⨅ (i : ι), (m i : (a : Set β) → ℝ≥0∞) (t k))

Tactic:
exact iInf_mono fun i => (m i).mono (image_preimage_subset _ _)

Premises used: MeasureTheory.OuterMeasure.mono, iInf_mono, Set.image_preimage_subset
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
ι : Sort u_2
β : Type u_3
f : α → β
hf : Injective f
m : ι → OuterMeasure α
⊢ Eq (α := OuterMeasure β) ((map f : (a : OuterMeasure α) → OuterMeasure β) (⨅ (i : ι), m i) : OuterMeasure β)
    ((restrict (range f) : (a : OuterMeasure β) → OuterMeasure β)
        (⨅ (i : ι), (map f : (a : OuterMeasure α) → OuterMeasure β) (m i)) :
      OuterMeasure β)

Tactic:
Eq.trans ?_ (map_comap _ _)

Premises used: MeasureTheory.OuterMeasure.map_comap, Eq.trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
ι : Sort u_2
β : Type u_3
f : α → β
hf : Injective f
m : ι → OuterMeasure α
refine :
  Eq.{u_3 + 1} (α := OuterMeasure β) ((map f : (a : OuterMeasure α) → OuterMeasure β) (⨅ (i : ι), m i) : OuterMeasure β)
    ((map f : (a : OuterMeasure α) → OuterMeasure β)
        ((comap f : (a : OuterMeasure β) → OuterMeasure α)
          (⨅ (i : ι), (map f : (a : OuterMeasure α) → OuterMeasure β) (m i))) :
      OuterMeasure β)
⊢ Eq (α := OuterMeasure β) ((map f : (a : OuterMeasure α) → OuterMeasure β) (⨅ (i : ι), m i) : OuterMeasure β)
    ((restrict (range f) : (a : OuterMeasure β) → OuterMeasure β)
        (⨅ (i : ι), (map f : (a : OuterMeasure α) → OuterMeasure β) (m i)) :
      OuterMeasure β)

Tactic:
refine Eq.trans ?_ (map_comap _ _)

Premises used: MeasureTheory.OuterMeasure.map_comap, Eq.trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
ι : Sort u_2
β : Type u_3
f : α → β
hf : Injective f
m : ι → OuterMeasure α
⊢ Eq.{u_3 + 1} (α := OuterMeasure β) ((map f : (a : OuterMeasure α) → OuterMeasure β) (⨅ (i : ι), m i) : OuterMeasure β)
    ((map f : (a : OuterMeasure α) → OuterMeasure β)
        ((comap f : (a : OuterMeasure β) → OuterMeasure α)
          (⨅ (i : ι), (map f : (a : OuterMeasure α) → OuterMeasure β) (m i))) :
      OuterMeasure β)

Tactic:
simp only [comap_iInf, comap_map hf]

Premises used: MeasureTheory.OuterMeasure.comap_map, MeasureTheory.OuterMeasure.comap_iInf
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
ι : Sort u_2
β : Type u_3
inst : Nonempty ι
f : α → β
m : ι → OuterMeasure β
⊢ Eq.{u_3 + 1} (α := OuterMeasure β)
    ((map f : (a : OuterMeasure α) → OuterMeasure β)
      (⨅ (i : ι), (comap f : (a : OuterMeasure β) → OuterMeasure α) (m i)))
    (⨅ (i : ι),
      (map f : (a : OuterMeasure α) → OuterMeasure β) ((comap f : (a : OuterMeasure β) → OuterMeasure α) (m i)))

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

Premises used: LE.le.antisymm, MeasureTheory.OuterMeasure.map_iInf_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
ι : Sort u_2
β : Type u_3
inst : Nonempty ι
f : α → β
m : ι → OuterMeasure β
refine :
  ∀ (s : Set β),
    LE.le (α := ℝ≥0∞)
      (((⨅ (i : ι),
                (map f : (a : OuterMeasure α) → OuterMeasure β)
                  ((comap f : (a : OuterMeasure β) → OuterMeasure α) (m i)) :
              OuterMeasure β) :
            (a : Set β) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      ((((map f : (a : OuterMeasure α) → OuterMeasure β)
                (⨅ (i : ι), (comap f : (a : OuterMeasure β) → OuterMeasure α) (m i)) :
              OuterMeasure β) :
            (a : Set β) → ℝ≥0∞)
          s :
        ℝ≥0∞)
⊢ Eq.{u_3 + 1} (α := OuterMeasure β)
    ((map f : (a : OuterMeasure α) → OuterMeasure β)
      (⨅ (i : ι), (comap f : (a : OuterMeasure β) → OuterMeasure α) (m i)))
    (⨅ (i : ι),
      (map f : (a : OuterMeasure α) → OuterMeasure β) ((comap f : (a : OuterMeasure β) → OuterMeasure α) (m i)))

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

Premises used: LE.le.antisymm, MeasureTheory.OuterMeasure.map_iInf_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
ι : Sort u_2
β : Type u_3
inst : Nonempty ι
f : α → β
m : ι → OuterMeasure β
s : Set β
simp :
  ∀ (i : ℕ → Set α) (i_1 : f ⁻¹' s ⊆ iUnion i),
    LE.le (α := ℝ≥0∞)
      (⨅ (t : ℕ → Set β), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ (i : ι), (m i : (a : Set β) → ℝ≥0∞) (f '' f ⁻¹' t n))
      (∑' (n : ℕ), ⨅ (i_2 : ι), (m i_2 : (a : Set β) → ℝ≥0∞) (f '' i n))
⊢ LE.le (α := ℝ≥0∞)
    (((⨅ (i : ι),
              (map f : (a : OuterMeasure α) → OuterMeasure β)
                ((comap f : (a : OuterMeasure β) → OuterMeasure α) (m i)) :
            OuterMeasure β) :
          (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((map f : (a : OuterMeasure α) → OuterMeasure β)
              (⨅ (i : ι), (comap f : (a : OuterMeasure β) → OuterMeasure α) (m i)) :
            OuterMeasure β) :
          (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
simp only [map_apply, comap_apply, iInf_apply, le_iInf_iff]

Premises used: MeasureTheory.OuterMeasure.map_apply, MeasureTheory.OuterMeasure.comap_apply, le_iInf_iff, MeasureTheory.OuterMeasure.iInf_apply
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
ι : Sort u_2
β : Type u_3
inst : Nonempty ι
f : α → β
m : ι → OuterMeasure β
s : Set β
⊢ ∀ (i : ℕ → Set α) (i_1 : f ⁻¹' s ⊆ iUnion i),
    LE.le (α := ℝ≥0∞)
      (⨅ (t : ℕ → Set β), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ (i : ι), (m i : (a : Set β) → ℝ≥0∞) (f '' f ⁻¹' t n))
      (∑' (n : ℕ), ⨅ (i_2 : ι), (m i_2 : (a : Set β) → ℝ≥0∞) (f '' i n))

Tactic:
fun t ht => iInf_le_of_le (fun n => f '' t n ∪ (range f)ᶜ) (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
ι : Sort u_2
β : Type u_3
inst : Nonempty ι
f : α → β
m : ι → OuterMeasure β
s : Set β
refine_1 : ∀ (t : ℕ → Set α) (ht : f ⁻¹' s ⊆ iUnion t), s ⊆ ⋃ (n : ℕ), f '' t n ∪ (range f)ᶜ
refine_2 :
  ∀ (t : ℕ → Set α) (ht : f ⁻¹' s ⊆ iUnion t),
    LE.le (α := ℝ≥0∞)
      (∑' (n : ℕ), ⨅ (i : ι), (m i : (a : Set β) → ℝ≥0∞) (f '' f ⁻¹' (fun (n : ℕ) ↦ f '' t n ∪ (range f)ᶜ) n))
      (∑' (n : ℕ), ⨅ (i : ι), (m i : (a : Set β) → ℝ≥0∞) (f '' t n))
⊢ ∀ (i : ℕ → Set α) (i_1 : f ⁻¹' s ⊆ iUnion i),
    LE.le (α := ℝ≥0∞)
      (⨅ (t : ℕ → Set β), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ (i : ι), (m i : (a : Set β) → ℝ≥0∞) (f '' f ⁻¹' t n))
      (∑' (n : ℕ), ⨅ (i_2 : ι), (m i_2 : (a : Set β) → ℝ≥0∞) (f '' i n))

Tactic:
refine fun t ht => iInf_le_of_le (fun n => f '' t n ∪ (range f)ᶜ) (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
ι : Sort u_2
β : Type u_3
inst : Nonempty ι
f : α → β
m : ι → OuterMeasure β
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
refine_1 : f '' f ⁻¹' s ⊆ f '' ⋃ (i : ℕ), t i
⊢ s ⊆ ⋃ (n : ℕ), f '' t n ∪ (range f)ᶜ

Tactic:
rw [← iUnion_union, Set.union_comm, ← inter_subset, ← image_iUnion, ←
      image_preimage_eq_inter_range]

Premises used: Set.iUnion_union, Set.union_comm, Set.image_preimage_eq_inter_range, Set.image_iUnion, Set.inter_subset
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
ι : Sort u_2
β : Type u_3
inst : Nonempty ι
f : α → β
m : ι → OuterMeasure β
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
ι : Sort u_2
β : Type u_3
inst : Nonempty ι
f : α → β
m : ι → OuterMeasure β
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
ι : Sort u_2
β : Type u_3
inst : Nonempty ι
f : α → β
m : ι → OuterMeasure β
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ LE.le (α := ℝ≥0∞)
    (∑' (n : ℕ), ⨅ (i : ι), (m i : (a : Set β) → ℝ≥0∞) (f '' f ⁻¹' (fun (n : ℕ) ↦ f '' t n ∪ (range f)ᶜ) n))
    (∑' (n : ℕ), ⨅ (i : ι), (m i : (a : Set β) → ℝ≥0∞) (f '' t n))

Tactic:
ENNReal.tsum_le_tsum fun n => iInf_mono fun i => (m i).mono ?_

Premises used: ENNReal.tsum_le_tsum, MeasureTheory.OuterMeasure.mono, iInf_mono
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
ι : Sort u_2
β : Type u_3
inst : Nonempty ι
f : α → β
m : ι → OuterMeasure β
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
refine_2 : ∀ (n : ℕ) (i : ι), f '' f ⁻¹' (fun (n : ℕ) ↦ f '' t n ∪ (range f)ᶜ) n ⊆ f '' t n
⊢ LE.le (α := ℝ≥0∞)
    (∑' (n : ℕ), ⨅ (i : ι), (m i : (a : Set β) → ℝ≥0∞) (f '' f ⁻¹' (fun (n : ℕ) ↦ f '' t n ∪ (range f)ᶜ) n))
    (∑' (n : ℕ), ⨅ (i : ι), (m i : (a : Set β) → ℝ≥0∞) (f '' t n))

Tactic:
refine ENNReal.tsum_le_tsum fun n => iInf_mono fun i => (m i).mono ?_

Premises used: ENNReal.tsum_le_tsum, MeasureTheory.OuterMeasure.mono, iInf_mono
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
ι : Sort u_2
β : Type u_3
inst : Nonempty ι
f : α → β
m : ι → OuterMeasure β
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
n : ℕ
i : ι
⊢ f '' f ⁻¹' (fun (n : ℕ) ↦ f '' t n ∪ (range f)ᶜ) n ⊆ f '' t n

Tactic:
simpa only [preimage_union, preimage_compl, preimage_range, compl_univ, union_empty,
      image_subset_iff] using subset_rfl

Premises used: Set.union_empty, Set.preimage_range, Set.compl_univ, Set.preimage_union, Set.image_subset_iff, Set.preimage_compl, subset_rfl
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
ι : Type u_2
β : Type u_3
I : Set ι
hI : I.Nonempty
f : α → β
m : ι → OuterMeasure β
⊢ Nonempty.{u_2 + 1} (↑I : Type u_2)

Tactic:
haveI := hI.to_subtype
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
ι : Type u_2
β : Type u_3
I : Set ι
hI : I.Nonempty
f : α → β
m : ι → OuterMeasure β
this : Nonempty.{u_2 + 1} (↑I : Type u_2)
rw :
  Eq.{u_3 + 1} (α := OuterMeasure β)
    ((map f : (a : OuterMeasure α) → OuterMeasure β)
      (⨅ (i : (↑I : Type u_2)), (comap f : (a : OuterMeasure β) → OuterMeasure α) (m (↑i : ι))))
    (⨅ (i : (↑I : Type u_2)),
      (map f : (a : OuterMeasure α) → OuterMeasure β) ((comap f : (a : OuterMeasure β) → OuterMeasure α) (m (↑i : ι))))
⊢ Eq.{u_3 + 1} (α := OuterMeasure β)
    ((map f : (a : OuterMeasure α) → OuterMeasure β) (⨅ i ∈ I, (comap f : (a : OuterMeasure β) → OuterMeasure α) (m i)))
    (⨅ i ∈ I, (map f : (a : OuterMeasure α) → OuterMeasure β) ((comap f : (a : OuterMeasure β) → OuterMeasure α) (m i)))

Tactic:
rw [← iInf_subtype'', ← iInf_subtype'']

Premises used: iInf_subtype''