ι : Type u_1
ι' : Type ?u.2502507
α : ι → Type u_2
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
⊢ ∀ (i : ι),
    MeasurableSpace.comap (fun b => b i) ((fun a => inst✝ a) i) ≤
      OuterMeasure.caratheodory (OuterMeasure.pi fun i => ↑(μ i))
ι : Type u_1
ι' : Type ?u.2502507
α : ι → Type u_2
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
⊢ MeasurableSpace.pi ≤ OuterMeasure.caratheodory (OuterMeasure.pi fun i => ↑(μ i))
refine' iSup_le _
ι : Type u_1
ι' : Type ?u.2502507
α : ι → Type u_2
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((a : ι) → α a)
hs : MeasurableSet s
⊢ MeasurableSet s
ι : Type u_1
ι' : Type ?u.2502507
α : ι → Type u_2
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
⊢ ∀ (i : ι),
    MeasurableSpace.comap (fun b => b i) ((fun a => inst✝ a) i) ≤
      OuterMeasure.caratheodory (OuterMeasure.pi fun i => ↑(μ i))
intro i s hs
ι : Type u_1
ι' : Type ?u.2502507
α : ι → Type u_2
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((a : ι) → α a)
hs : MeasurableSet s
⊢ MeasurableSet s
ι : Type u_1
ι' : Type ?u.2502507
α : ι → Type u_2
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((a : ι) → α a)
hs : MeasurableSet s
⊢ MeasurableSet s
rw [MeasurableSpace.comap] at hs
case intro.intro
ι : Type u_1
ι' : Type ?u.2502507
α : ι → Type u_2
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
⊢ MeasurableSet ((fun b => b i) ⁻¹' s)
ι : Type u_1
ι' : Type ?u.2502507
α : ι → Type u_2
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((a : ι) → α a)
hs : MeasurableSet s
⊢ MeasurableSet s
rcases hs with ⟨s, hs, rfl⟩
case intro.intro.hs
ι : Type u_1
ι' : Type ?u.2502507
α : ι → Type u_2
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
⊢ ∀ (t : Set ((a : ι) → α a)),
    piPremeasure (fun i => ↑(μ i)) (t ∩ (fun b => b i) ⁻¹' s) +
        piPremeasure (fun i => ↑(μ i)) (t \ (fun b => b i) ⁻¹' s) ≤
      piPremeasure (fun i => ↑(μ i)) t
case intro.intro
ι : Type u_1
ι' : Type ?u.2502507
α : ι → Type u_2
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
⊢ MeasurableSet ((fun b => b i) ⁻¹' s)
apply boundedBy_caratheodory
case intro.intro.hs
ι : Type u_1
ι' : Type ?u.2502507
α : ι → Type u_2
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ piPremeasure (fun i => ↑(μ i)) (t ∩ (fun b => b i) ⁻¹' s) +
      piPremeasure (fun i => ↑(μ i)) (t \ (fun b => b i) ⁻¹' s) ≤
    piPremeasure (fun i => ↑(μ i)) t
case intro.intro.hs
ι : Type u_1
ι' : Type ?u.2502507
α : ι → Type u_2
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
⊢ ∀ (t : Set ((a : ι) → α a)),
    piPremeasure (fun i => ↑(μ i)) (t ∩ (fun b => b i) ⁻¹' s) +
        piPremeasure (fun i => ↑(μ i)) (t \ (fun b => b i) ⁻¹' s) ≤
      piPremeasure (fun i => ↑(μ i)) t
intro t
case intro.intro.hs
ι : Type u_1
ι' : Type ?u.2502507
α : ι → Type u_2
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ ∏ x : ι, ↑↑(μ x) (eval x '' (t ∩ (fun b => b i) ⁻¹' s)) + ∏ x : ι, ↑↑(μ x) (eval x '' (t \ (fun b => b i) ⁻¹' s)) ≤
    ∏ x : ι, ↑↑(μ x) (eval x '' t)
case intro.intro.hs
ι : Type u_1
ι' : Type ?u.2502507
α : ι → Type u_2
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ piPremeasure (fun i => ↑(μ i)) (t ∩ (fun b => b i) ⁻¹' s) +
      piPremeasure (fun i => ↑(μ i)) (t \ (fun b => b i) ⁻¹' s) ≤
    piPremeasure (fun i => ↑(μ i)) t
simp_rw [piPremeasure]
case intro.intro.hs.refine'_1
ι : Type u_1
ι' : Type ?u.2502507
α : ι → Type u_2
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ ↑↑(μ i) (eval i '' (t ∩ (fun b => b i) ⁻¹' s)) + ↑↑(μ i) (eval i '' (t \ (fun b => b i) ⁻¹' s)) ≤
    ↑↑(μ i) (eval i '' t)

case intro.intro.hs.refine'_2
ι : Type u_1
ι' : Type ?u.2502507
α : ι → Type u_2
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ ∀ (j : ι), j ∈ Finset.univ → j ≠ i → ↑↑(μ j) (eval j '' (t ∩ (fun b => b i) ⁻¹' s)) ≤ ↑↑(μ j) (eval j '' t)

case intro.intro.hs.refine'_3
ι : Type u_1
ι' : Type ?u.2502507
α : ι → Type u_2
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ ∀ (j : ι), j ∈ Finset.univ → j ≠ i → ↑↑(μ j) (eval j '' (t \ (fun b => b i) ⁻¹' s)) ≤ ↑↑(μ j) (eval j '' t)
case intro.intro.hs
ι : Type u_1
ι' : Type ?u.2502507
α : ι → Type u_2
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ ∏ x : ι, ↑↑(μ x) (eval x '' (t ∩ (fun b => b i) ⁻¹' s)) + ∏ x : ι, ↑↑(μ x) (eval x '' (t \ (fun b => b i) ⁻¹' s)) ≤
    ∏ x : ι, ↑↑(μ x) (eval x '' t)
refine' Finset.prod_add_prod_le' (Finset.mem_univ i) _ _ _
no goals
case intro.intro.hs.refine'_1
ι : Type u_1
ι' : Type ?u.2502507
α : ι → Type u_2
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ ↑↑(μ i) (eval i '' (t ∩ (fun b => b i) ⁻¹' s)) + ↑↑(μ i) (eval i '' (t \ (fun b => b i) ⁻¹' s)) ≤
    ↑↑(μ i) (eval i '' t)
simp [image_inter_preimage, image_diff_preimage, measure_inter_add_diff _ hs, le_refl]
case intro.intro.hs.refine'_2
ι : Type u_1
ι' : Type ?u.2502507
α : ι → Type u_2
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
j : ι
a✝ : j ≠ i
⊢ ↑↑(μ j) (eval j '' (t ∩ (fun b => b i) ⁻¹' s)) ≤ ↑↑(μ j) (eval j '' t)
case intro.intro.hs.refine'_2
ι : Type u_1
ι' : Type ?u.2502507
α : ι → Type u_2
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ ∀ (j : ι), j ∈ Finset.univ → j ≠ i → ↑↑(μ j) (eval j '' (t ∩ (fun b => b i) ⁻¹' s)) ≤ ↑↑(μ j) (eval j '' t)
rintro j - _
case intro.intro.hs.refine'_2.h
ι : Type u_1
ι' : Type ?u.2502507
α : ι → Type u_2
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
j : ι
a✝ : j ≠ i
⊢ eval j '' (t ∩ (fun b => b i) ⁻¹' s) ⊆ eval j '' t
case intro.intro.hs.refine'_2
ι : Type u_1
ι' : Type ?u.2502507
α : ι → Type u_2
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
j : ι
a✝ : j ≠ i
⊢ ↑↑(μ j) (eval j '' (t ∩ (fun b => b i) ⁻¹' s)) ≤ ↑↑(μ j) (eval j '' t)
apply mono'
case intro.intro.hs.refine'_2.h.h
ι : Type u_1
ι' : Type ?u.2502507
α : ι → Type u_2
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
j : ι
a✝ : j ≠ i
⊢ t ∩ (fun b => b i) ⁻¹' s ⊆ t
case intro.intro.hs.refine'_2.h
ι : Type u_1
ι' : Type ?u.2502507
α : ι → Type u_2
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
j : ι
a✝ : j ≠ i
⊢ eval j '' (t ∩ (fun b => b i) ⁻¹' s) ⊆ eval j '' t
apply image_subset
no goals
case intro.intro.hs.refine'_2.h.h
ι : Type u_1
ι' : Type ?u.2502507
α : ι → Type u_2
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
j : ι
a✝ : j ≠ i
⊢ t ∩ (fun b => b i) ⁻¹' s ⊆ t
apply inter_subset_left
case intro.intro.hs.refine'_3
ι : Type u_1
ι' : Type ?u.2502507
α : ι → Type u_2
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
j : ι
a✝ : j ≠ i
⊢ ↑↑(μ j) (eval j '' (t \ (fun b => b i) ⁻¹' s)) ≤ ↑↑(μ j) (eval j '' t)
case intro.intro.hs.refine'_3
ι : Type u_1
ι' : Type ?u.2502507
α : ι → Type u_2
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ ∀ (j : ι), j ∈ Finset.univ → j ≠ i → ↑↑(μ j) (eval j '' (t \ (fun b => b i) ⁻¹' s)) ≤ ↑↑(μ j) (eval j '' t)
rintro j - _
case intro.intro.hs.refine'_3.h
ι : Type u_1
ι' : Type ?u.2502507
α : ι → Type u_2
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
j : ι
a✝ : j ≠ i
⊢ eval j '' (t \ (fun b => b i) ⁻¹' s) ⊆ eval j '' t
case intro.intro.hs.refine'_3
ι : Type u_1
ι' : Type ?u.2502507
α : ι → Type u_2
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
j : ι
a✝ : j ≠ i
⊢ ↑↑(μ j) (eval j '' (t \ (fun b => b i) ⁻¹' s)) ≤ ↑↑(μ j) (eval j '' t)
apply mono'
case intro.intro.hs.refine'_3.h.h
ι : Type u_1
ι' : Type ?u.2502507
α : ι → Type u_2
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
j : ι
a✝ : j ≠ i
⊢ t \ (fun b => b i) ⁻¹' s ⊆ t
case intro.intro.hs.refine'_3.h
ι : Type u_1
ι' : Type ?u.2502507
α : ι → Type u_2
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
j : ι
a✝ : j ≠ i
⊢ eval j '' (t \ (fun b => b i) ⁻¹' s) ⊆ eval j '' t
apply image_subset
no goals
case intro.intro.hs.refine'_3.h.h
ι : Type u_1
ι' : Type ?u.2502507
α : ι → Type u_2
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((fun i => α i) i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
j : ι
a✝ : j ≠ i
⊢ t \ (fun b => b i) ⁻¹' s ⊆ t
apply diff_subset