awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ 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:
map_iInf_comap _

Premises used: MeasureTheory.OuterMeasure.map_iInf_comap
-- 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)
⊢ 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:
exact map_iInf_comap _

Premises used: MeasureTheory.OuterMeasure.map_iInf_comap
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
ι : Sort u_2
s : Set α
m : ι → OuterMeasure α
rw 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 α)
⊢ 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 α)

Tactic:
rw [Subtype.range_coe]

Premises used: Subtype.range_coe
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
ι : Sort u_2
inst : Nonempty ι
s : Set α
m : ι → OuterMeasure α
⊢ Eq (α := OuterMeasure α) ((restrict s : (a : OuterMeasure α) → OuterMeasure α) (⨅ (i : ι), m i) : OuterMeasure α)
    (⨅ (i : ι), (restrict s : (a : OuterMeasure α) → OuterMeasure α) (m i) : OuterMeasure α)

Tactic:
(congr_arg (map ((↑) : s → α)) (comap_iInf _ _)).trans (map_iInf_comap _)

Premises used: MeasureTheory.OuterMeasure.comap_iInf, MeasureTheory.OuterMeasure.map_iInf_comap, congr_arg, MeasureTheory.OuterMeasure.map, Subtype.val, DFunLike.coe, Eq.trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
ι : Type u_2
I : Set ι
hI : I.Nonempty
s : Set α
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
I : Set ι
hI : I.Nonempty
s : Set α
m : ι → OuterMeasure α
this : Nonempty.{u_2 + 1} (↑I : Type u_2)
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 α)
⊢ Eq (α := OuterMeasure α) ((restrict s : (a : OuterMeasure α) → OuterMeasure α) (⨅ i ∈ I, m i) : OuterMeasure α)
    (⨅ i ∈ I, (restrict s : (a : OuterMeasure α) → OuterMeasure α) (m i) : OuterMeasure α)

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

Premises used: iInf_subtype''
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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 : Type u_2)), m (↑i : ι)) : OuterMeasure α)
    (⨅ (i : (↑I : Type u_2)), (restrict s : (a : OuterMeasure α) → OuterMeasure α) (m (↑i : ι)) : OuterMeasure α)

Tactic:
restrict_iInf _ _

Premises used: MeasureTheory.OuterMeasure.restrict_iInf
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
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 : Type u_2)), m (↑i : ι)) : OuterMeasure α)
    (⨅ (i : (↑I : Type u_2)), (restrict s : (a : OuterMeasure α) → OuterMeasure α) (m (↑i : ι)) : OuterMeasure α)

Tactic:
exact restrict_iInf _ _

Premises used: MeasureTheory.OuterMeasure.restrict_iInf
-- Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction
Goal:
α : Type u_1
m : Set (OuterMeasure α)
s : Set α
hm : m.Nonempty
⊢ Eq (α := OuterMeasure α) ((restrict s : (a : OuterMeasure α) → OuterMeasure α) (sInf m) : OuterMeasure α)
    (sInf ((⇑(restrict s) : (a : OuterMeasure α) → OuterMeasure α) '' m) : OuterMeasure α)

Tactic:
simp only [sInf_eq_iInf, restrict_biInf, hm, iInf_image]

Premises used: sInf_eq_iInf, iInf_image, MeasureTheory.OuterMeasure.restrict_biInf
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := (a : Set α) → ℝ≥0∞) (⇑0 : (a : Set α) → ℝ≥0∞) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
β : Type u_2
m m₁ m₂ : OuterMeasure α
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m₁ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) ((m₂ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) = 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
m₁ m₂ : OuterMeasure α
⊢ (⇑(m₁ + m₂) : (a : Set α) → ℝ≥0∞) =
    HAdd.hAdd (α := (a : Set α) → ℝ≥0∞) (⇑m₁ : (a : Set α) → ℝ≥0∞) (⇑m₂ : (a : Set α) → ℝ≥0∞)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
m₁ m₂ : OuterMeasure α
s : Set α
⊢ (m₁ + m₂ : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((m₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
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 α
simp : HSMul.hSMul (β := ℝ≥0∞) c 0 = 0
⊢ HSMul.hSMul (β := ℝ≥0∞) c ((m : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) = 0

Tactic:
simp only [measure_empty]

Premises used: MeasureTheory.measure_empty
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
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 α
rw : HSMul.hSMul (β := ℝ≥0∞) c 1 * 0 = 0
⊢ HSMul.hSMul (β := ℝ≥0∞) c 0 = 0

Tactic:
rw [← smul_one_mul c]

Premises used: smul_one_mul
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
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 1 * 0 = 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
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
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∞)
⊢ HSMul.hSMul (β := ℝ≥0∞) c ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≤
    HSMul.hSMul (β := ℝ≥0∞) c ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [← smul_one_mul c, ← smul_one_mul c (m t)]

Premises used: smul_one_mul, DFunLike.coe
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
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
⊢ 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:
mul_right_mono (m.mono h)

Premises used: MeasureTheory.OuterMeasure.mono, mul_right_mono
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
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
⊢ 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:
exact mul_right_mono (m.mono h)

Premises used: MeasureTheory.OuterMeasure.mono, mul_right_mono
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
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)
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)
⊢ HSMul.hSMul (β := ℝ≥0∞) c ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞) ≤
    ∑' (i : ℕ), HSMul.hSMul (β := ℝ≥0∞) c ((m : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
simp_rw [← smul_one_mul c (m _), ENNReal.tsum_mul_left]

Premises used: ENNReal.tsum_mul_left, smul_one_mul, DFunLike.coe
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
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)
⊢ 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:
mul_right_mono (measure_iUnion_le _)

Premises used: mul_right_mono, MeasureTheory.measure_iUnion_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
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)
⊢ 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:
exact mul_right_mono (measure_iUnion_le _)

Premises used: mul_right_mono, MeasureTheory.measure_iUnion_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
R : Type u_3
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
m : OuterMeasure α
⊢ (⇑(c • m) : (a : Set α) → ℝ≥0∞) = HSMul.hSMul (β := (a : Set α) → ℝ≥0∞) c (⇑m : (a : Set α) → ℝ≥0∞)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
R : Type u_3
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
m : OuterMeasure α
s : Set α
⊢ (c • m : (a : Set α) → ℝ≥0∞) s = HSMul.hSMul (β := ℝ≥0∞) c ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
β : Type u_2
m : 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∞
inst_4 : SMulCommClass R R' ℝ≥0∞
⊢ SMulCommClass.{u_3, u_4, u_1} R R' (OuterMeasure α)

Tactic:
⟨fun _ _ _ => ext fun _ => smul_comm _ _ _⟩

Premises used: SMulCommClass.smul_comm, SMulCommClass.mk, DFunLike.coe, MeasureTheory.OuterMeasure.ext
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
β : Type u_2
m : 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∞
inst_4 : SMul R R'
inst_5 : IsScalarTower R R' ℝ≥0∞
⊢ IsScalarTower.{u_3, u_4, u_1} R R' (OuterMeasure α)

Tactic:
⟨fun _ _ _ => ext fun _ => smul_assoc _ _ _⟩

Premises used: smul_assoc, IsScalarTower.mk, DFunLike.coe, MeasureTheory.OuterMeasure.ext
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
β : Type u_2
m : 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∞
inst_4 : SMul Rᵐᵒᵖ ℝ≥0∞
inst_5 : IsCentralScalar R ℝ≥0∞
⊢ IsCentralScalar.{u_3, u_1} R (OuterMeasure α)

Tactic:
⟨fun _ _ => ext fun _ => op_smul_eq_smul _ _⟩

Premises used: IsCentralScalar.mk, DFunLike.coe, MeasureTheory.OuterMeasure.ext, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := OuterMeasure α) ⊥ 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
β : Type u_2
m a : OuterMeasure α
s : Set α
⊢ LE.le (α := ℝ≥0∞) (((0 : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((a : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [coe_zero, Pi.zero_apply, zero_le]

Premises used: zero_le, Pi.zero_apply, MeasureTheory.OuterMeasure.coe_zero
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
m : OuterMeasure α
⊢ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞) ↔ m = 0

Tactic:
⟨fun h => bot_unique fun s => (measure_mono <| subset_univ s).trans_eq h, fun h => h.symm ▸ rfl⟩

Premises used: LE.le.trans_eq, Set.subset_univ, Eq.rec, Iff.intro, MeasureTheory.measure_mono, bot_unique, Eq.symm, rfl
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
β : Type u_2
m_1 : OuterMeasure α
ms : Set (OuterMeasure α)
f : ℕ → Set α
h : Pairwise (Disjoint on f)
m : OuterMeasure α
hm : m ∈ ms
i : ℕ
⊢ LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) (⨆ m ∈ ms, (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
apply le_iSup₂ m hm

Premises used: le_iSup₂
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
β : Type u_2
m_1 : OuterMeasure α
ms : Set (OuterMeasure α)
m : OuterMeasure α
hm : m ∈ ms
s : Set α
⊢ LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((sSup ms : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
apply le_iSup₂ m hm

Premises used: le_iSup₂
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
ms : Set (OuterMeasure α)
s : Set α
⊢ Eq (α := ℝ≥0∞) ((sSup ms : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (⨆ m ∈ ms, (m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rfl

Premises used: iSup, rfl, ite
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
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)
rw₂ rw₃ : Eq (α := ℝ≥0∞) (⨆ (i : ι), (f i : (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∞)

Tactic:
rw [iSup, sSup_apply, iSup_range]

Premises used: iSup, iSup_range, MeasureTheory.OuterMeasure.sSup_apply
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
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∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
m₁ m₂ : OuterMeasure α
s : Set α
⊢ 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
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
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∞)
rwa₁ rwa₂ rwa₃ 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∞)
⊢ 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

Premises used: iSup_bool_eq
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
R : Type u_3
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
ι : Sort u_4
f : ι → OuterMeasure α
c : R
s : Set α
⊢ Eq (α := ℝ≥0∞) ((HSMul.hSMul (β := OuterMeasure α) c (⨆ (i : ι), f i) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((⨆ (i : ι), c • f i : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [smul_apply, iSup_apply, ENNReal.smul_iSup]

Premises used: ENNReal.smul_iSup, MeasureTheory.OuterMeasure.iSup_apply, MeasureTheory.OuterMeasure.smul_apply
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
m₁ m₂ : OuterMeasure α
s₁ s₂ : Set α
hm : m₁ ≤ m₂
hs : s₁ ⊆ s₂
⊢ LE.le (α := ℝ≥0∞) ((m₁ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) ((m₂ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞)

Tactic:
(hm s₁).trans (m₂.mono hs)

Premises used: MeasureTheory.OuterMeasure.mono, LE.le.trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
β_1 : Type u_2
m_1 : OuterMeasure α
β : Type u_3
f : α → β
m : OuterMeasure α
s : ℕ → Set β
h : Pairwise (Disjoint on s)
⊢ LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (f ⁻¹' ⋃ (i : ℕ), s i) : ℝ≥0∞)
    (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f ⁻¹' s i) : ℝ≥0∞)

Tactic:
simpa using measure_iUnion_le fun i => f ⁻¹' s i

Premises used: MeasureTheory.measure_iUnion_le, Set.preimage
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
β : Type u_3
f : α → β
m : OuterMeasure α
s : Set β
⊢ Eq (α := ℝ≥0∞) ((((map f : (a : OuterMeasure α) → OuterMeasure β) m : OuterMeasure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
m : OuterMeasure α
⊢ (map id : (a : OuterMeasure α) → OuterMeasure α) m = m

Tactic:
ext fun _ => rfl

Premises used: MeasureTheory.OuterMeasure.ext, rfl
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
β : Type u_3
γ : Type u_4
f : α → β
g : β → γ
m : OuterMeasure α
⊢ Eq.{u_4 + 1} (α := OuterMeasure γ)
    ((map g : (a : OuterMeasure β) → OuterMeasure γ) ((map f : (a : OuterMeasure α) → OuterMeasure β) m) :
      OuterMeasure γ)
    ((map (g ∘ f) : (a : OuterMeasure α) → OuterMeasure γ) m : OuterMeasure γ)

Tactic:
ext fun _ => rfl

Premises used: MeasureTheory.OuterMeasure.ext, rfl
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
β : Type u_3
f : α → β
⊢ Monotone.{u_1, u_3} (α := OuterMeasure α) (β := OuterMeasure β) (⇑(map f) : (a : OuterMeasure α) → OuterMeasure β)

Tactic:
fun _ _ h _ => h _

Premises used: Monotone, Set.preimage
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
β : Type u_3
f : α → β
m m' : OuterMeasure α
s : Set β
⊢ Eq (α := ℝ≥0∞)
    ((((map f : (a : OuterMeasure α) → OuterMeasure β) (m ⊔ m') : OuterMeasure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((map f : (a : OuterMeasure α) → OuterMeasure β) m ⊔ (map f : (a : OuterMeasure α) → OuterMeasure β) m' :
            OuterMeasure β) :
          (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
simp only [map_apply, sup_apply]

Premises used: MeasureTheory.OuterMeasure.map_apply, MeasureTheory.OuterMeasure.sup_apply
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
β : Type u_3
ι : Sort u_4
f : α → β
m : ι → OuterMeasure α
s : Set β
⊢ Eq (α := ℝ≥0∞)
    ((((map f : (a : OuterMeasure α) → OuterMeasure β) (⨆ (i : ι), m i) : OuterMeasure β) : (a : Set β) → ℝ≥0∞) s :
      ℝ≥0∞)
    (((⨆ (i : ι), (map f : (a : OuterMeasure α) → OuterMeasure β) (m i) : OuterMeasure β) : (a : Set β) → ℝ≥0∞) s :
      ℝ≥0∞)

Tactic:
simp only [map_apply, iSup_apply]

Premises used: MeasureTheory.OuterMeasure.map_apply, MeasureTheory.OuterMeasure.iSup_apply
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
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
comp_map : ∀ {α β γ : Type u_3} (g : α → β) (h : β → γ) (x : OuterMeasure α), (h ∘ g) <$> x = h <$> g <$> x
⊢ LawfulFunctor OuterMeasure

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
β : Type u_2
m : OuterMeasure α
α_1 β_1 : Type u_3
⊢ Eq (α := α_1 → OuterMeasure β_1 → OuterMeasure α_1) Functor.mapConst (Functor.map ∘ const β_1)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
β : Type u_2
m : OuterMeasure α
α_1 : Type u_3
x : OuterMeasure α_1
⊢ id <$> x = x

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
β : Type u_2
m : OuterMeasure α
α_1 β_1 γ : Type u_3
g : α_1 → β_1
h : β_1 → γ
x : OuterMeasure α_1
⊢ (h ∘ g) <$> x = h <$> g <$> x

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
β : Type u_2
m : OuterMeasure α
a : α
⊢ Eq (α := ℝ≥0∞) (indicator ∅ (fun (x : α) ↦ 1) a) 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
β : Type u_2
m : OuterMeasure α
a : α
x x_1 : Set α
h : x ⊆ x_1
h₁ : LE.le (α := ℝ≥0∞) 0 1
grw grw₁ : LE.le (α := ℝ≥0∞) (x_1.indicator (fun (x : α) ↦ 1) a) (x_1.indicator (fun (x : α) ↦ 1) a)
⊢ LE.le (α := ℝ≥0∞) (x.indicator (fun (x : α) ↦ 1) a) (x_1.indicator (fun (x : α) ↦ 1) a)

Tactic:
grw [h]
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
a : α
s : Set α
⊢ Eq (α := ℝ≥0∞) ((dirac a : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (s.indicator (fun (x : α) ↦ 1) a : ℝ≥0∞)

Tactic:
rfl

Premises used: Set.indicator, rfl, ite
-- Module: Mathlib.MeasureTheory.OuterMeasure.Operations
Goal:
α : Type u_1
β : Type u_2
m : OuterMeasure α
ι : Type u_3
f : ι → OuterMeasure α
⊢ Eq (α := ℝ≥0∞) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) ∅) 0

Tactic:
simp