-- Mathlib/MeasureTheory/Constructions/Pi.lean
theorem pi_caratheodory :
    MeasurableSpace.pi ≤ (OuterMeasure.pi fun i => (μ i).toOuterMeasure).caratheodory

Proof state:
case intro.intro.hs
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ ∏ x : ι, (μ x).toOuterMeasure (eval x '' (t ∩ (fun b => b i) ⁻¹' s)) +
      ∏ x : ι, (μ x).toOuterMeasure (eval x '' (t \ (fun b => b i) ⁻¹' s)) ≤
    ∏ x : ι, (μ x).toOuterMeasure (eval x '' t)

Tactic:
refine Finset.prod_add_prod_le' (Finset.mem_univ i) ?_ ?_ ?_

Result:
case intro.intro.hs.refine_1
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ (μ i).toOuterMeasure (eval i '' (t ∩ (fun b => b i) ⁻¹' s)) +
      (μ i).toOuterMeasure (eval i '' (t \ (fun b => b i) ⁻¹' s)) ≤
    (μ i).toOuterMeasure (eval i '' t)

case intro.intro.hs.refine_2
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ ∀ j ∈ Finset.univ,
    j ≠ i → (μ j).toOuterMeasure (eval j '' (t ∩ (fun b => b i) ⁻¹' s)) ≤ (μ j).toOuterMeasure (eval j '' t)

case intro.intro.hs.refine_3
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ ∀ j ∈ Finset.univ,
    j ≠ i → (μ j).toOuterMeasure (eval j '' (t \ (fun b => b i) ⁻¹' s)) ≤ (μ j).toOuterMeasure (eval j '' t)

Proof state:
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((a : ι) → α a)
hs : MeasurableSet s
⊢ MeasurableSet s

Tactic:
rcases hs with ⟨s, hs, rfl⟩

Result:
case intro.intro
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
⊢ MeasurableSet ((fun b => b i) ⁻¹' s)

Proof state:
case intro.intro.hs.refine_2.h.h
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
j : ι
a✝ : j ≠ i
⊢ t ∩ (fun b => b i) ⁻¹' s ⊆ t

Tactic:
apply inter_subset_left

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
⊢ MeasurableSpace.pi ≤ (OuterMeasure.pi fun i => (μ i).toOuterMeasure).caratheodory

Tactic:
refine iSup_le ?_

Result:
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
⊢ ∀ (i : ι),
    MeasurableSpace.comap (fun b => b i) (inst✝ i) ≤ (OuterMeasure.pi fun i => (μ i).toOuterMeasure).caratheodory

Proof state:
case intro.intro.hs.refine_3.h.h
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
j : ι
a✝ : j ≠ i
⊢ t \ (fun b => b i) ⁻¹' s ⊆ t

Tactic:
apply diff_subset

Result:
no goals

Proof state:
case intro.intro.hs.refine_2
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
j : ι
a✝ : j ≠ i
⊢ (μ j).toOuterMeasure (eval j '' (t ∩ (fun b => b i) ⁻¹' s)) ≤ (μ j).toOuterMeasure (eval j '' t)

Tactic:
gcongr

Result:
case intro.intro.hs.refine_2.h.h
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
j : ι
a✝ : j ≠ i
⊢ t ∩ (fun b => b i) ⁻¹' s ⊆ t

Proof state:
case intro.intro.hs.refine_3
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ ∀ j ∈ Finset.univ,
    j ≠ i → (μ j).toOuterMeasure (eval j '' (t \ (fun b => b i) ⁻¹' s)) ≤ (μ j).toOuterMeasure (eval j '' t)

Tactic:
rintro j - _

Result:
case intro.intro.hs.refine_3
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
j : ι
a✝ : j ≠ i
⊢ (μ j).toOuterMeasure (eval j '' (t \ (fun b => b i) ⁻¹' s)) ≤ (μ j).toOuterMeasure (eval j '' t)

Proof state:
case intro.intro.hs
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ piPremeasure (fun i => (μ i).toOuterMeasure) (t ∩ (fun b => b i) ⁻¹' s) +
      piPremeasure (fun i => (μ i).toOuterMeasure) (t \ (fun b => b i) ⁻¹' s) ≤
    piPremeasure (fun i => (μ i).toOuterMeasure) t

Tactic:
simp_rw [piPremeasure]

Result:
case intro.intro.hs
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ ∏ x : ι, (μ x).toOuterMeasure (eval x '' (t ∩ (fun b => b i) ⁻¹' s)) +
      ∏ x : ι, (μ x).toOuterMeasure (eval x '' (t \ (fun b => b i) ⁻¹' s)) ≤
    ∏ x : ι, (μ x).toOuterMeasure (eval x '' t)

Proof state:
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
⊢ ∀ (i : ι),
    MeasurableSpace.comap (fun b => b i) (inst✝ i) ≤ (OuterMeasure.pi fun i => (μ i).toOuterMeasure).caratheodory

Tactic:
intro i s hs

Result:
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((a : ι) → α a)
hs : MeasurableSet s
⊢ MeasurableSet s

Proof state:
case intro.intro
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
⊢ MeasurableSet ((fun b => b i) ⁻¹' s)

Tactic:
apply boundedBy_caratheodory

Result:
case intro.intro.hs
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
⊢ ∀ (t : Set ((a : ι) → α a)),
    piPremeasure (fun i => (μ i).toOuterMeasure) (t ∩ (fun b => b i) ⁻¹' s) +
        piPremeasure (fun i => (μ i).toOuterMeasure) (t \ (fun b => b i) ⁻¹' s) ≤
      piPremeasure (fun i => (μ i).toOuterMeasure) t

Proof state:
case intro.intro.hs.refine_1
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ (μ i).toOuterMeasure (eval i '' (t ∩ (fun b => b i) ⁻¹' s)) +
      (μ i).toOuterMeasure (eval i '' (t \ (fun b => b i) ⁻¹' s)) ≤
    (μ i).toOuterMeasure (eval i '' t)

Tactic:
simp [image_inter_preimage, image_diff_preimage, measure_inter_add_diff _ hs, le_refl]

Result:
no goals