awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
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
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (⨆ (_ : s.Nonempty), m s : ℝ≥0∞) ↔
    (μ : (a : Set α) → ℝ≥0∞) s ≤ m s
have inr : ∀ (h : s.Nonempty),
  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
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
⊢ μ ≤ boundedBy m ↔ ∀ (s : Set α), s.Nonempty → (μ : (a : Set α) → ℝ≥0∞) s ≤ m s
have rw : ∀ (a : Set α), (μ : (a : Set α) → ℝ≥0∞) a ≤ m a ↔ a.Nonempty → (μ : (a : Set α) → ℝ≥0∞) a ≤ m a
Tactic: rw [le_boundedBy, forall_congr']
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
s : Set α
⊢ (μ : (a : Set α) → ℝ≥0∞) s ≤ m s ↔ s.Nonempty → (μ : (a : Set α) → ℝ≥0∞) s ≤ m s
have inl : ∀ (h : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
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
⊢ (μ : (a : Set α) → ℝ≥0∞) s ≤ m s ↔ s.Nonempty → (μ : (a : Set α) → ℝ≥0∞) s ≤ m s
have inr : ∀ (h : s.Nonempty), (μ : (a : Set α) → ℝ≥0∞) s ≤ m s ↔ s.Nonempty → (μ : (a : Set α) → ℝ≥0∞) s ≤ m s
Tactic: rcases s.eq_empty_or_nonempty with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := OuterMeasure α) (boundedBy ⊤) ⊤
have rw : ∀ (s : Set α), s.Nonempty → LE.le (α := ℝ≥0∞) (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (⊤ s : ℝ≥0∞)
Tactic: rw [eq_top_iff, le_boundedBy']
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Nonempty
⊢ LE.le (α := ℝ≥0∞) (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (⊤ s : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ∞ (⊤ s)
Tactic: rw [top_apply hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
⊢ c • boundedBy m = boundedBy (c • m)
have simp : OuterMeasure.ofFunction (HSMul.hSMul (β := Set α → ℝ≥0∞) c fun (s : Set α) ↦ ⨆ (_ : s.Nonempty), m s) sorry =
  OuterMeasure.ofFunction (fun (s : Set α) ↦ ⨆ (_ : s.Nonempty), (c • m) s) sorry
Tactic: simp only [boundedBy, smul_ofFunction hc]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
⊢ OuterMeasure.ofFunction (HSMul.hSMul (β := Set α → ℝ≥0∞) c fun (s : Set α) ↦ ⨆ (_ : s.Nonempty), m s) ⋯ =
    OuterMeasure.ofFunction (fun (s : Set α) ↦ ⨆ (_ : s.Nonempty), (c • m) s) ⋯
have e_m : ∀ (s : Set α),
  HSMul.hSMul (β := Set α → ℝ≥0∞) c (fun (s : Set α) ↦ ⨆ (_ : s.Nonempty), m s) s = ⨆ (_ : s.Nonempty), (c • m) s
Tactic: congr 1 with s : 1
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set α → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
s : Set α
⊢ HSMul.hSMul (β := Set α → ℝ≥0∞) c (fun (s : Set α) ↦ ⨆ (_ : s.Nonempty), m s) s = ⨆ (_ : s.Nonempty), (c • m) s
have e_m : HSMul.hSMul (β := Set α → ℝ≥0∞) c (fun (s : Set α) ↦ ⨆ (_ : s.Nonempty), m s) ∅ =
  ⨆ (_ : Set.Nonempty.{u_1} (α := α) ∅), (c • m) ∅
Tactic: rcases s.eq_empty_or_nonempty with (rfl | hs)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
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) ∅
⊢ HSMul.hSMul (β := Set α → ℝ≥0∞) c (fun (s : Set α) ↦ ⨆ (_ : s.Nonempty), m s) s = ⨆ (_ : s.Nonempty), (c • m) s
have e_m₁ : ∀ (hs : s.Nonempty),
  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)
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
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 β)
have refine_1 : (Monotone (β := ℝ≥0∞) fun (s : Set α) ↦ ⨆ (_ : s.Nonempty), m s) ∨ Surjective f
Tactic: refine (comap_ofFunction _ ?_).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
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
⊢ Eq.{u_2 + 1} (α := OuterMeasure β) ((comap f : (a : OuterMeasure α) → OuterMeasure β) (boundedBy m) : OuterMeasure β)
    (boundedBy fun (s : Set β) ↦ m (f '' s) : OuterMeasure β)
have refine_2 : Eq.{u_2 + 1} (α := OuterMeasure β) (OuterMeasure.ofFunction (fun (s : Set β) ↦ ⨆ (_ : (f '' s).Nonempty), m (f '' s)) sorry)
  (boundedBy fun (s : Set β) ↦ m (f '' s))
Tactic: refine (comap_ofFunction _ ?_).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
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
have 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
Tactic: refine h.imp (fun H s t hst => iSup_le fun hs => ?_) id
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (hypothesis)
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
⊢ m s ≤ (fun (s : Set α) ↦ (⨆ (_ : s.Nonempty), m s : ℝ≥0∞)) t
have ht : t.Nonempty
Tactic: have ht : t.Nonempty := hs.mono hst
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
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 β)
    (OuterMeasure.ofFunction (fun (s : Set β) ↦ ⨆ (_ : (f '' s).Nonempty), m (f '' s)) ⋯)
    (boundedBy fun (s : Set β) ↦ m (f '' s))
have refine_2 : Eq.{u_2 + 1} (α := OuterMeasure β) (OuterMeasure.ofFunction (fun (s : Set β) ↦ ⨆ (_ : (f '' s).Nonempty), m (f '' s)) sorry)
  (OuterMeasure.ofFunction (fun (s : Set β) ↦ ⨆ (_ : s.Nonempty), m (f '' s)) sorry)
Tactic: dsimp only [boundedBy]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
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 β)
    (OuterMeasure.ofFunction (fun (s : Set β) ↦ ⨆ (_ : (f '' s).Nonempty), m (f '' s)) ⋯)
    (OuterMeasure.ofFunction (fun (s : Set β) ↦ ⨆ (_ : s.Nonempty), m (f '' s)) ⋯)
have refine_2 : ∀ (s : Set β), Eq (α := ℝ≥0∞) (⨆ (_ : (f '' s).Nonempty), m (f '' s)) (⨆ (_ : s.Nonempty), m (f '' s))
Tactic: congr with s : 1
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
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 β
⊢ Eq (α := ℝ≥0∞) (⨆ (_ : (f '' s).Nonempty), m (f '' s)) (⨆ (_ : s.Nonempty), m (f '' s))
have refine_2 : Eq (α := ℝ≥0∞) (⨆ (_ : s.Nonempty), m (f '' s)) (⨆ (_ : s.Nonempty), m (f '' s))
Tactic: rw [image_nonempty]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set (OuterMeasure α)
⊢ sInf m = boundedBy (sInfGen m)
have refine_1 : sInf m ≤ boundedBy (sInfGen m)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set (OuterMeasure α)
refine_1 : sInf m ≤ boundedBy (sInfGen m)
⊢ sInf m = boundedBy (sInfGen m)
have refine_2 : boundedBy (sInfGen m) ≤ sInf m
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set (OuterMeasure α)
⊢ sInf m ≤ boundedBy (sInfGen m)
have refine_1 : ∀ (s : Set α) (μ : OuterMeasure α) (hμ : μ ∈ m),
  LE.le (α := ℝ≥0∞) ((sInf m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: refine le_boundedBy.2 fun s => le_iInf₂ fun μ hμ => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set (OuterMeasure α)
⊢ boundedBy (sInfGen m) ≤ sInf m
have refine_2 : ∀ b ∈ m, boundedBy (sInfGen m) ≤ b
Tactic: refine le_sInf ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set (OuterMeasure α)
h : m.Nonempty
t : Set α
⊢ Eq (α := ℝ≥0∞) (⨆ (_ : t.Nonempty), sInfGen m t) (⨅ μ ∈ m, (μ : (a : Set α) → ℝ≥0∞) t)
have inl : Eq (α := ℝ≥0∞) (⨆ (_ : Set.Nonempty.{u_1} (α := α) ∅), sInfGen m ∅) (⨅ μ ∈ m, (μ : (a : Set α) → ℝ≥0∞) ∅)
Tactic: rcases t.eq_empty_or_nonempty with (rfl | ht)
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
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∞) ∅)
⊢ Eq (α := ℝ≥0∞) (⨆ (_ : t.Nonempty), sInfGen m t) (⨅ μ ∈ m, (μ : (a : Set α) → ℝ≥0∞) t)
have inr : ∀ (ht : t.Nonempty), Eq (α := ℝ≥0∞) (⨆ (_ : t.Nonempty), sInfGen m t) (⨅ μ ∈ m, (μ : (a : Set α) → ℝ≥0∞) t)
Tactic: rcases t.eq_empty_or_nonempty with (rfl | ht)
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
m : Set (OuterMeasure α)
s : Set α
h : m.Nonempty
⊢ Eq (α := ℝ≥0∞) ((sInf m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ μ ∈ m, (μ : (a : Set α) → ℝ≥0∞) (t n) : ℝ≥0∞)
have 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∞)
Tactic: simp_rw [sInf_eq_boundedBy_sInfGen, boundedBy_apply, iSup_sInfGen_nonempty h]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((sInf m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ μ ∈ m, (μ : (a : Set α) → ℝ≥0∞) (t n) : ℝ≥0∞)
have 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))
Tactic: simp_rw [sInf_eq_boundedBy_sInfGen, boundedBy_apply, iSup_sInfGen_nonempty h]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
ι : Sort u_2
inst : Nonempty ι
m : ι → OuterMeasure α
s : Set α
⊢ 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∞)
have 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))
Tactic: rw [iInf, sInf_apply (range_nonempty m)]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
ι : Sort u_2
m : ι → OuterMeasure α
s : Set α
hs : s.Nonempty
⊢ 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∞)
have 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))
Tactic: rw [iInf, sInf_apply' hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
I : Set ι
hI : I.Nonempty
m : ι → OuterMeasure α
s : Set α
⊢ 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∞)
have this : Nonempty.{u_2 + 1} (↑I : Type u_2)
Tactic: haveI := hI.to_subtype
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
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))
have 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∞)
Tactic: refine ext_nonempty fun s hs => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
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∞)
have 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∞)
Tactic: refine ((comap_mono f).map_iInf_le s).antisymm ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
ι : Sort u_2
β : Type u_3
f : α → β
m : ι → OuterMeasure β
s : Set α
hs : s.Nonempty
⊢ 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∞)
have 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))
Tactic: simp only [comap_apply, iInf_apply' _ hs, iInf_apply' _ (hs.image _), le_iInf_iff,
    Set.image_subset_iff, preimage_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
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))
have 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))
Tactic: refine fun t ht => iInf_le_of_le _ (iInf_le_of_le ht <| ENNReal.tsum_le_tsum fun k => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
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 β)
have 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 β)
Tactic: refine Eq.trans ?_ (map_comap _ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
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)))
have 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∞)
Tactic: refine (map_iInf_le _ _).antisymm fun s => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
ι : Sort u_2
β : Type u_3
inst : Nonempty ι
f : α → β
m : ι → OuterMeasure β
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∞)
have 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))
Tactic: simp only [map_apply, comap_apply, iInf_apply, le_iInf_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
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))
have refine_1 : ∀ (t : ℕ → Set α) (ht : f ⁻¹' s ⊆ iUnion t), s ⊆ ⋃ (n : ℕ), f '' t n ∪ (range f)ᶜ
Tactic: refine fun t ht => iInf_le_of_le (fun n => f '' t n ∪ (range f)ᶜ) (iInf_le_of_le ?_ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
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)ᶜ
⊢ ∀ (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))
have 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))
Tactic: refine fun t ht => iInf_le_of_le (fun n => f '' t n ∪ (range f)ᶜ) (iInf_le_of_le ?_ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
ι : Sort u_2
β : Type u_3
inst : Nonempty ι
f : α → β
m : ι → OuterMeasure β
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ s ⊆ ⋃ (n : ℕ), f '' t n ∪ (range f)ᶜ
have refine_1 : f '' f ⁻¹' s ⊆ f '' ⋃ (i : ℕ), t i
Tactic: rw [← iUnion_union, Set.union_comm, ← inter_subset, ← image_iUnion, ←
      image_preimage_eq_inter_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
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))
have refine_2 : ∀ (n : ℕ) (i : ι), f '' f ⁻¹' (fun (n : ℕ) ↦ f '' t n ∪ (range f)ᶜ) n ⊆ f '' t n
Tactic: refine ENNReal.tsum_le_tsum fun n => iInf_mono fun i => (m i).mono ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
β : Type u_3
I : Set ι
hI : I.Nonempty
f : α → β
m : ι → OuterMeasure β
⊢ 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)))
have this : Nonempty.{u_2 + 1} (↑I : Type u_2)
Tactic: haveI := hI.to_subtype
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
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)
⊢ 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)))
have 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 : ι))))
Tactic: rw [← iInf_subtype'', ← iInf_subtype'']