awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (goal)
Goal:
α : Type u_1
ι : Sort u_2
s : Set α
m : ι → OuterMeasure α
⊢ Eq (α := OuterMeasure α)
    ((restrict s : (a : OuterMeasure α) → OuterMeasure α)
        (⨅ (i : ι), (restrict s : (a : OuterMeasure α) → OuterMeasure α) (m i)) :
      OuterMeasure α)
    ((restrict (range (ι := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))) :
          (a : OuterMeasure α) → OuterMeasure α)
        (⨅ (i : ι), (restrict s : (a : OuterMeasure α) → OuterMeasure α) (m i)) :
      OuterMeasure α)
have rw : Eq (α := OuterMeasure α)
  ((restrict s : (a : OuterMeasure α) → OuterMeasure α)
      (⨅ (i : ι), (restrict s : (a : OuterMeasure α) → OuterMeasure α) (m i)) :
    OuterMeasure α)
  ((restrict s : (a : OuterMeasure α) → OuterMeasure α)
      (⨅ (i : ι), (restrict s : (a : OuterMeasure α) → OuterMeasure α) (m i)) :
    OuterMeasure α)
Tactic: rw [Subtype.range_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.OfFunction (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
I : Set ι
hI : I.Nonempty
s : Set α
m : ι → OuterMeasure α
⊢ Eq (α := OuterMeasure α) ((restrict s : (a : OuterMeasure α) → OuterMeasure α) (⨅ i ∈ I, m i) : OuterMeasure α)
    (⨅ i ∈ I, (restrict s : (a : OuterMeasure α) → OuterMeasure α) (m i) : OuterMeasure α)
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
I : Set ι
hI : I.Nonempty
s : Set α
m : ι → OuterMeasure α
this : Nonempty.{u_2 + 1} (↑I : Type u_2)
⊢ Eq (α := OuterMeasure α) ((restrict s : (a : OuterMeasure α) → OuterMeasure α) (⨅ i ∈ I, m i) : OuterMeasure α)
    (⨅ i ∈ I, (restrict s : (a : OuterMeasure α) → OuterMeasure α) (m i) : OuterMeasure α)
have rw : Eq (α := OuterMeasure α)
  ((restrict s : (a : OuterMeasure α) → OuterMeasure α) (⨅ (i : (↑I : Type u_2)), m (↑i : ι)) : OuterMeasure α)
  (⨅ (i : (↑I : Type u_2)), (restrict s : (a : OuterMeasure α) → OuterMeasure α) (m (↑i : ι)) : OuterMeasure α)
Tactic: rw [← iInf_subtype'', ← iInf_subtype'']
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Operations (goal)
Goal:
α : Type u_1
β : Type u_2
m_1 : OuterMeasure α
R : Type u_3
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
R' : Type u_4
inst_2 : SMul R' ℝ≥0∞
inst_3 : IsScalarTower R' ℝ≥0∞ ℝ≥0∞
c : R
m : OuterMeasure α
⊢ HSMul.hSMul (β := ℝ≥0∞) c ((m : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) = 0
have simp : HSMul.hSMul (β := ℝ≥0∞) c 0 = 0
Tactic: simp only [measure_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Operations (goal)
Goal:
α : Type u_1
β : Type u_2
m_1 : OuterMeasure α
R : Type u_3
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
R' : Type u_4
inst_2 : SMul R' ℝ≥0∞
inst_3 : IsScalarTower R' ℝ≥0∞ ℝ≥0∞
c : R
m : OuterMeasure α
⊢ HSMul.hSMul (β := ℝ≥0∞) c 0 = 0
have rw : HSMul.hSMul (β := ℝ≥0∞) c 1 * 0 = 0
Tactic: rw [← smul_one_mul c]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Operations (goal)
Goal:
α : Type u_1
β : Type u_2
m_1 : OuterMeasure α
R : Type u_3
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
R' : Type u_4
inst_2 : SMul R' ℝ≥0∞
inst_3 : IsScalarTower R' ℝ≥0∞ ℝ≥0∞
c : R
m : OuterMeasure α
s t : Set α
h : s ⊆ t
⊢ HSMul.hSMul (β := ℝ≥0∞) c ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≤
    HSMul.hSMul (β := ℝ≥0∞) c ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have rw : HMul.hMul (β := ℝ≥0∞) (HSMul.hSMul (β := ℝ≥0∞) c 1) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≤
  HMul.hMul (β := ℝ≥0∞) (HSMul.hSMul (β := ℝ≥0∞) c 1) ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [← smul_one_mul c, ← smul_one_mul c (m t)]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Operations (goal)
Goal:
α : Type u_1
β : Type u_2
m_1 : OuterMeasure α
R : Type u_3
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
R' : Type u_4
inst_2 : SMul R' ℝ≥0∞
inst_3 : IsScalarTower R' ℝ≥0∞ ℝ≥0∞
c : R
m : OuterMeasure α
s : ℕ → Set α
h : Pairwise (Disjoint on s)
⊢ HSMul.hSMul (β := ℝ≥0∞) c ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞) ≤
    ∑' (i : ℕ), HSMul.hSMul (β := ℝ≥0∞) c ((m : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
have simp_rw : HMul.hMul (β := ℝ≥0∞) (HSMul.hSMul (β := ℝ≥0∞) c 1) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞) ≤
  HSMul.hSMul (β := ℝ≥0∞) c 1 * ∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (s i)
Tactic: simp_rw [← smul_one_mul c (m _), ENNReal.tsum_mul_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Operations (goal)
Goal:
α : Type u_1
ι : Sort u_3
f : ι → OuterMeasure α
s : Set α
⊢ Eq (α := ℝ≥0∞) (((⨆ (i : ι), f i : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨆ (i : ι), (f i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (((sSup (range fun (i : ι) ↦ f i) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
  (⨆ (i : ι), (f i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [iSup, sSup_apply, iSup_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Operations (goal)
Goal:
α : Type u_1
ι : Sort u_3
f : ι → OuterMeasure α
s : Set α
rw :
  Eq (α := ℝ≥0∞) (((sSup (range fun (i : ι) ↦ f i) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨆ (i : ι), (f i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((⨆ (i : ι), f i : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨆ (i : ι), (f i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞)
  (⨆ (m : OuterMeasure α),
    ⨆ (_ : Membership.mem (γ := Set (OuterMeasure α)) (range fun (i : ι) ↦ f i) m), (m : (a : Set α) → ℝ≥0∞) s)
  (⨆ (i : ι), (f i : (a : Set α) → ℝ≥0∞) s)
Tactic: rw [iSup, sSup_apply, iSup_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Operations (goal)
Goal:
α : Type u_1
ι : Sort u_3
f : ι → OuterMeasure α
s : Set α
rw :
  Eq (α := ℝ≥0∞) (((sSup (range fun (i : ι) ↦ f i) : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨆ (i : ι), (f i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞)
    (⨆ (m : OuterMeasure α),
      ⨆ (_ : Membership.mem (γ := Set (OuterMeasure α)) (range fun (i : ι) ↦ f i) m), (m : (a : Set α) → ℝ≥0∞) s)
    (⨆ (i : ι), (f i : (a : Set α) → ℝ≥0∞) s)
⊢ Eq (α := ℝ≥0∞) (((⨆ (i : ι), f i : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨆ (i : ι), (f i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) (⨆ (i : ι), (f i : (a : Set α) → ℝ≥0∞) s) (⨆ (i : ι), (f i : (a : Set α) → ℝ≥0∞) s)
Tactic: rw [iSup, sSup_apply, iSup_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Operations (hypothesis)
Goal:
α : Type u_1
m₁ m₂ : OuterMeasure α
s : Set α
⊢ Eq (α := ℝ≥0∞) ((m₁ ⊔ m₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (max ((m₁ : (a : Set α) → ℝ≥0∞) s) ((m₂ : (a : Set α) → ℝ≥0∞) s) : ℝ≥0∞)
have this : Eq (α := ℝ≥0∞) (((⨆ (i : Bool), bif i then m₁ else m₂ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
  (⨆ (i : Bool), (bif i then m₁ else m₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: have := iSup_apply (fun b => cond b m₁ m₂) s
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Operations (goal)
Goal:
α : Type u_1
m₁ m₂ : OuterMeasure α
s : Set α
this :
  Eq (α := ℝ≥0∞) (((⨆ (i : Bool), bif i then m₁ else m₂ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨆ (i : Bool), (bif i then m₁ else m₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((m₁ ⊔ m₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (max ((m₁ : (a : Set α) → ℝ≥0∞) s) ((m₂ : (a : Set α) → ℝ≥0∞) s) : ℝ≥0∞)
have rwa : ∀
  (this :
    Eq (α := ℝ≥0∞) (((bif true then m₁ else m₂) ⊔ bif false then m₁ else m₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (⨆ (i : Bool), (bif i then m₁ else m₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((m₁ ⊔ m₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (max ((m₁ : (a : Set α) → ℝ≥0∞) s) ((m₂ : (a : Set α) → ℝ≥0∞) s) : ℝ≥0∞)
Tactic: rwa [iSup_bool_eq, iSup_bool_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Operations (goal)
Goal:
α : Type u_1
m₁ m₂ : OuterMeasure α
s : Set α
this :
  Eq (α := ℝ≥0∞) (((⨆ (i : Bool), bif i then m₁ else m₂ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨆ (i : Bool), (bif i then m₁ else m₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rwa :
  ∀
    (this :
      Eq (α := ℝ≥0∞) (((bif true then m₁ else m₂) ⊔ bif false then m₁ else m₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
        (⨆ (i : Bool), (bif i then m₁ else m₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((m₁ ⊔ m₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (max ((m₁ : (a : Set α) → ℝ≥0∞) s) ((m₂ : (a : Set α) → ℝ≥0∞) s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((m₁ ⊔ m₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (max ((m₁ : (a : Set α) → ℝ≥0∞) s) ((m₂ : (a : Set α) → ℝ≥0∞) s) : ℝ≥0∞)
have rwa₁ : ∀
  (this :
    Eq (α := ℝ≥0∞) (((bif true then m₁ else m₂) ⊔ bif false then m₁ else m₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (max ((bif true then m₁ else m₂ : (a : Set α) → ℝ≥0∞) s) ((bif false then m₁ else m₂ : (a : Set α) → ℝ≥0∞) s) :
        ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((m₁ ⊔ m₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (max ((m₁ : (a : Set α) → ℝ≥0∞) s) ((m₂ : (a : Set α) → ℝ≥0∞) s) : ℝ≥0∞)
Tactic: rwa [iSup_bool_eq, iSup_bool_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Operations (goal)
Goal:
α : Type u_1
β : Type u_2
m : OuterMeasure α
⊢ LawfulFunctor OuterMeasure
have map_const : ∀ {α β : Type u_3}, Eq (α := α → OuterMeasure β → OuterMeasure α) Functor.mapConst (Functor.map ∘ const β)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Operations (goal)
Goal:
α : Type u_1
β : Type u_2
m : OuterMeasure α
map_const : ∀ {α β : Type u_3}, Eq (α := α → OuterMeasure β → OuterMeasure α) Functor.mapConst (Functor.map ∘ const β)
⊢ LawfulFunctor OuterMeasure
have id_map : ∀ {α : Type u_3} (x : OuterMeasure α), id <$> x = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Operations (goal)
Goal:
α : Type u_1
β : Type u_2
m : OuterMeasure α
map_const : ∀ {α β : Type u_3}, Eq (α := α → OuterMeasure β → OuterMeasure α) Functor.mapConst (Functor.map ∘ const β)
id_map : ∀ {α : Type u_3} (x : OuterMeasure α), id <$> x = x
⊢ LawfulFunctor OuterMeasure
have comp_map : ∀ {α β γ : Type u_3} (g : α → β) (h : β → γ) (x : OuterMeasure α), (h ∘ g) <$> x = h <$> g <$> x
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Operations (goal)
Goal:
α : Type u_1
β : Type u_2
m : OuterMeasure α
a : α
x x_1 : Set α
h : x ⊆ x_1
⊢ LE.le (α := ℝ≥0∞) (x.indicator (fun (x : α) ↦ 1) a) (x_1.indicator (fun (x : α) ↦ 1) a)
have h₁ : LE.le (α := ℝ≥0∞) 0 1
Tactic: grw [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Operations (goal)
Goal:
α : Type u_1
β : Type u_2
m : OuterMeasure α
a : α
x x_1 : Set α
h : x ⊆ x_1
h₁ : LE.le (α := ℝ≥0∞) 0 1
⊢ LE.le (α := ℝ≥0∞) (x.indicator (fun (x : α) ↦ 1) a) (x_1.indicator (fun (x : α) ↦ 1) a)
have grw : LE.le (α := ℝ≥0∞) (x_1.indicator (fun (x : α) ↦ 1) a) (x_1.indicator (fun (x : α) ↦ 1) a)
Tactic: grw [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Operations (goal)
Goal:
α : Type u_1
β : Type u_2
m : OuterMeasure α
ι : Type u_3
f : ι → OuterMeasure α
s : ℕ → Set α
h : Pairwise (Disjoint on s)
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i))
    (∑' (i : ℕ) (i_1 : ι), (f i_1 : (a : Set α) → ℝ≥0∞) (s i))
have rw : LE.le (α := ℝ≥0∞) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i))
  (∑' (b : ι) (a : ℕ), (f b : (a : Set α) → ℝ≥0∞) (s a))
Tactic: rw [ENNReal.tsum_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Operations (goal)
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
m m' : OuterMeasure α
hm : m ≤ m'
u : Set α
⊢ LE.le (α := ℝ≥0∞)
    ((((restrict s : (a : OuterMeasure α) → OuterMeasure α) m : OuterMeasure α) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
    ((((restrict t : (a : OuterMeasure α) → OuterMeasure α) m' : OuterMeasure α) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
have simp : LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞) ((m' : (a : Set α) → ℝ≥0∞) (u ∩ t) : ℝ≥0∞)
Tactic: simp only [restrict_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Operations (goal)
Goal:
α : Type u_1
β : Type u_3
f : α → β
hf : Surjective f
m : OuterMeasure β
s : Set β
⊢ Eq (α := ℝ≥0∞)
    ((((map f : (a : OuterMeasure α) → OuterMeasure β) ((comap f : (a : OuterMeasure β) → OuterMeasure α) m) :
            OuterMeasure β) :
          (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((m : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞)
  ((((comap f : (a : OuterMeasure β) → OuterMeasure α) m : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
  ((m : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [map_apply, comap_apply, hf.image_preimage]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Operations (goal)
Goal:
α : Type u_1
β : Type u_3
f : α → β
hf : Surjective f
m : OuterMeasure β
s : Set β
rw :
  Eq (α := ℝ≥0∞)
    ((((comap f : (a : OuterMeasure β) → OuterMeasure α) m : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    ((m : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((map f : (a : OuterMeasure α) → OuterMeasure β) ((comap f : (a : OuterMeasure β) → OuterMeasure α) m) :
            OuterMeasure β) :
          (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((m : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) (f '' f ⁻¹' s) : ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [map_apply, comap_apply, hf.image_preimage]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Operations (goal)
Goal:
α : Type u_1
β : Type u_3
f : α → β
hf : Surjective f
m : OuterMeasure β
s : Set β
rw :
  Eq (α := ℝ≥0∞)
    ((((comap f : (a : OuterMeasure β) → OuterMeasure α) m : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    ((m : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ : Eq (α := ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) (f '' f ⁻¹' s) : ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((map f : (a : OuterMeasure α) → OuterMeasure β) ((comap f : (a : OuterMeasure β) → OuterMeasure α) m) :
            OuterMeasure β) :
          (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((m : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [map_apply, comap_apply, hf.image_preimage]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Operations (goal)
Goal:
α : Type u_1
β : Type u_3
f : α → β
hf : Injective f
m : OuterMeasure α
s : Set α
⊢ Eq (α := ℝ≥0∞)
    ((((comap f : (a : OuterMeasure β) → OuterMeasure α) ((map f : (a : OuterMeasure α) → OuterMeasure β) m) :
            OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞)
  ((((map f : (a : OuterMeasure α) → OuterMeasure β) m : OuterMeasure β) : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
  ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [comap_apply, map_apply, hf.preimage_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Operations (goal)
Goal:
α : Type u_1
β : Type u_3
f : α → β
hf : Injective f
m : OuterMeasure α
s : Set α
rw :
  Eq (α := ℝ≥0∞)
    ((((map f : (a : OuterMeasure α) → OuterMeasure β) m : OuterMeasure β) : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((comap f : (a : OuterMeasure β) → OuterMeasure α) ((map f : (a : OuterMeasure α) → OuterMeasure β) m) :
            OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (f ⁻¹' f '' s) : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [comap_apply, map_apply, hf.preimage_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Operations (goal)
Goal:
α : Type u_1
β : Type u_3
f : α → β
hf : Injective f
m : OuterMeasure α
s : Set α
rw :
  Eq (α := ℝ≥0∞)
    ((((map f : (a : OuterMeasure α) → OuterMeasure β) m : OuterMeasure β) : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ : Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (f ⁻¹' f '' s) : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((comap f : (a : OuterMeasure β) → OuterMeasure α) ((map f : (a : OuterMeasure α) → OuterMeasure β) m) :
            OuterMeasure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [comap_apply, map_apply, hf.preimage_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Operations (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
hs : s.Nonempty
⊢ Eq (α := ℝ≥0∞)
    ((((comap f : (a : OuterMeasure β) → OuterMeasure α) ⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (((⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
  (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [comap_apply, top_apply hs, top_apply (hs.image _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Operations (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
hs : s.Nonempty
rw :
  Eq (α := ℝ≥0∞) (((⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((comap f : (a : OuterMeasure β) → OuterMeasure α) ⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) (((⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [comap_apply, top_apply hs, top_apply (hs.image _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Operations (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
hs : s.Nonempty
rw :
  Eq (α := ℝ≥0∞) (((⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ : Eq (α := ℝ≥0∞) (((⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((comap f : (a : OuterMeasure β) → OuterMeasure α) ⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) ∞ ∞
Tactic: rw [comap_apply, top_apply hs, top_apply (hs.image _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Operations (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ Eq (α := ℝ≥0∞) ((((map f : (a : OuterMeasure α) → OuterMeasure β) ⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((restrict (range f) : (a : OuterMeasure β) → OuterMeasure β) ⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
  ((((restrict (range f) : (a : OuterMeasure β) → OuterMeasure β) ⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [map_apply, restrict_apply, ← image_preimage_eq_inter_range, top_apply', top_apply',
      Set.image_eq_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Operations (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
rw :
  Eq (α := ℝ≥0∞) (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    ((((restrict (range f) : (a : OuterMeasure β) → OuterMeasure β) ⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((map f : (a : OuterMeasure α) → OuterMeasure β) ⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((restrict (range f) : (a : OuterMeasure β) → OuterMeasure β) ⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
  (((⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
Tactic: rw [map_apply, restrict_apply, ← image_preimage_eq_inter_range, top_apply', top_apply',
      Set.image_eq_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Operations (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
rw :
  Eq (α := ℝ≥0∞) (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    ((((restrict (range f) : (a : OuterMeasure β) → OuterMeasure β) ⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((map f : (a : OuterMeasure α) → OuterMeasure β) ⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((restrict (range f) : (a : OuterMeasure β) → OuterMeasure β) ⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
  (((⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) (f '' f ⁻¹' s) : ℝ≥0∞)
Tactic: rw [map_apply, restrict_apply, ← image_preimage_eq_inter_range, top_apply', top_apply',
      Set.image_eq_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Operations (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
rw :
  Eq (α := ℝ≥0∞) (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    ((((restrict (range f) : (a : OuterMeasure β) → OuterMeasure β) ⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
rw₂ :
  Eq (α := ℝ≥0∞) (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) (f '' f ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((map f : (a : OuterMeasure α) → OuterMeasure β) ⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((restrict (range f) : (a : OuterMeasure β) → OuterMeasure β) ⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have rw₃ : Eq (α := ℝ≥0∞) (⨅ (_ : f ⁻¹' s = ∅), 0 : ℝ≥0∞) (((⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) (f '' f ⁻¹' s) : ℝ≥0∞)
Tactic: rw [map_apply, restrict_apply, ← image_preimage_eq_inter_range, top_apply', top_apply',
      Set.image_eq_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Operations (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
rw :
  Eq (α := ℝ≥0∞) (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    ((((restrict (range f) : (a : OuterMeasure β) → OuterMeasure β) ⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
rw₂ :
  Eq (α := ℝ≥0∞) (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) (f '' f ⁻¹' s) : ℝ≥0∞)
rw₃ : Eq (α := ℝ≥0∞) (⨅ (_ : f ⁻¹' s = ∅), 0 : ℝ≥0∞) (((⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) (f '' f ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((map f : (a : OuterMeasure α) → OuterMeasure β) ⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((restrict (range f) : (a : OuterMeasure β) → OuterMeasure β) ⊤ : OuterMeasure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have rw₄ : Eq (α := ℝ≥0∞) (⨅ (_ : f ⁻¹' s = ∅), 0) (⨅ (_ : f '' f ⁻¹' s = ∅), 0)
Tactic: rw [map_apply, restrict_apply, ← image_preimage_eq_inter_range, top_apply', top_apply',
      Set.image_eq_empty]