awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst_1 : (i : ι) → MeasurableSpace (α i)
μ_1 : (i : ι) → Measure (α i)
δ : Type u_4
X : δ → Type u_5
inst_2 : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_3 : ∀ (i : δ), SigmaFinite (μ i)
i : δ
l : List δ
ih : SigmaFinite (Measure.tprod (X := X) l μ)
⊢ SigmaFinite ((μ i).prod (Measure.tprod (X := X) l μ))

Tactic:
@prod.instSigmaFinite _ _ _ _ _ _ _ ih

Premises used: MeasureTheory.Measure.prod.instSigmaFinite, List.foldr
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst_1 : (i : ι) → MeasurableSpace (α i)
μ_1 : (i : ι) → Measure (α i)
δ : Type u_4
X : δ → Type u_5
inst_2 : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_3 : ∀ (i : δ), SigmaFinite (μ i)
i : δ
l : List δ
ih : SigmaFinite (Measure.tprod (X := X) l μ)
⊢ SigmaFinite ((μ i).prod (Measure.tprod (X := X) l μ))

Tactic:
exact @prod.instSigmaFinite _ _ _ _ _ _ _ ih

Premises used: MeasureTheory.Measure.prod.instSigmaFinite
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst_1 : (i : ι) → MeasurableSpace (α i)
μ_1 : (i : ι) → Measure (α i)
δ : Type u_4
X : δ → Type u_5
inst_2 : (i : δ) → MeasurableSpace (X i)
l : List δ
μ : (i : δ) → Measure (X i)
inst_3 : ∀ (i : δ), SigmaFinite (μ i)
nil : SigmaFinite (α := TProd X []) (Measure.tprod (X := X) [] μ)
cons :
  ∀ (i : δ) (l : List δ) (ih : SigmaFinite (Measure.tprod (X := X) l μ)),
    SigmaFinite (Measure.tprod (X := X) (i :: l) μ)
⊢ SigmaFinite (Measure.tprod (X := X) l μ)

Tactic:
induction l with
  | nil => rw [tprod_nil]; infer_instance
  | cons i l ih => rw [tprod_cons]; exact @prod.instSigmaFinite _ _ _ _ _ _ _ ih

Premises used: List.cons, MeasureTheory.Measure.tprod_cons, MeasureTheory.Measure.tprod_nil, List.nil
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
δ : Type u_4
X : δ → Type u_5
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : ∀ (i : δ), SigmaFinite (μ i)
s : (i : δ) → Set (X i)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.tprod (X := X) [] μ : Measure (TProd X [])) : (a : Set (TProd X [])) → ℝ≥0∞) (Set.tprod (α := X) [] s) :
      ℝ≥0∞)
    (List.prod (List.map (fun (i : δ) ↦ (μ i : (a : Set (X i)) → ℝ≥0∞) (s i)) []) : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
δ : Type u_4
X : δ → Type u_5
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : ∀ (i : δ), SigmaFinite (μ i)
s : (i : δ) → Set (X i)
a : δ
l : List δ
ih :
  Eq (α := ℝ≥0∞) ((Measure.tprod (X := X) l μ : (a : Set (TProd X l)) → ℝ≥0∞) (Set.tprod (α := X) l s) : ℝ≥0∞)
    (List.prod (List.map (fun (i : δ) ↦ (μ i : (a : Set (X i)) → ℝ≥0∞) (s i)) l) : ℝ≥0∞)
cons :
  Eq (α := ℝ≥0∞)
    (((μ a).prod (Measure.tprod (X := X) l μ) : (a : Set (TProd X (a :: l))) → ℝ≥0∞) (s a ×ˢ Set.tprod (α := X) l s) :
      ℝ≥0∞)
    (List.prod (List.map (fun (i : δ) ↦ (μ i : (a : Set (X i)) → ℝ≥0∞) (s i)) (a :: l)) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((Measure.tprod (X := X) (a :: l) μ : (a : Set (TProd X (a :: l))) → ℝ≥0∞) (Set.tprod (α := X) (a :: l) s) : ℝ≥0∞)
    (List.prod (List.map (fun (i : δ) ↦ (μ i : (a : Set (X i)) → ℝ≥0∞) (s i)) (a :: l)) : ℝ≥0∞)

Tactic:
rw [tprod_cons, Set.tprod]

Premises used: Set.tprod, MeasureTheory.Measure.tprod_cons
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
δ : Type u_4
X : δ → Type u_5
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : ∀ (i : δ), SigmaFinite (μ i)
s : (i : δ) → Set (X i)
a : δ
l : List δ
ih :
  Eq (α := ℝ≥0∞) ((Measure.tprod (X := X) l μ : (a : Set (TProd X l)) → ℝ≥0∞) (Set.tprod (α := X) l s) : ℝ≥0∞)
    (List.prod (List.map (fun (i : δ) ↦ (μ i : (a : Set (X i)) → ℝ≥0∞) (s i)) l) : ℝ≥0∞)
cons :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ a : (a : Set (X a)) → ℝ≥0∞) (s a) : ℝ≥0∞)
      ((Measure.tprod (X := X) l μ : (a : Set (TProd X l)) → ℝ≥0∞) (Set.tprod (α := X) l s) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ a : (a : Set (X a)) → ℝ≥0∞) (s a) : ℝ≥0∞)
      (List.prod (List.map (fun (i : δ) ↦ (μ i : (a : Set (X i)) → ℝ≥0∞) (s i)) l) : ℝ≥0∞)
cons₁ cons₂ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ a : (a : Set (X a)) → ℝ≥0∞) (s a) : ℝ≥0∞)
      (List.prod (List.map (fun (i : δ) ↦ (μ i : (a : Set (X i)) → ℝ≥0∞) (s i)) l) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ a : (a : Set (X a)) → ℝ≥0∞) (s a) : ℝ≥0∞)
      (List.prod (List.map (fun (i : δ) ↦ (μ i : (a : Set (X i)) → ℝ≥0∞) (s i)) l) : ℝ≥0∞)
⊢ ((μ a).prod (Measure.tprod (X := X) l μ) :
        (a : Set (X a × foldr (fun (i : δ) (β : Type u_5) ↦ X i × β) PUnit.{u_5 + 1} l)) → ℝ≥0∞)
      (s a ×ˢ Set.tprod (α := X) l s) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ a : (a : Set (X a)) → ℝ≥0∞) (s a) : ℝ≥0∞)
      (List.prod (List.map (fun (i : δ) ↦ (μ i : (a : Set (X i)) → ℝ≥0∞) (s i)) l) : ℝ≥0∞)

Tactic:
rw [prod_prod, ih]

Premises used: MeasureTheory.Measure.prod_prod
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
δ : Type u_4
X : δ → Type u_5
inst : (i : δ) → MeasurableSpace (X i)
l : List δ
μ : (i : δ) → Measure (X i)
inst_1 : ∀ (i : δ), SigmaFinite (μ i)
s : (i : δ) → Set (X i)
nil :
  Eq (α := ℝ≥0∞)
    (((Measure.tprod (X := X) [] μ : Measure (TProd X [])) : (a : Set (TProd X [])) → ℝ≥0∞) (Set.tprod (α := X) [] s) :
      ℝ≥0∞)
    (List.prod (List.map (fun (i : δ) ↦ (μ i : (a : Set (X i)) → ℝ≥0∞) (s i)) []) : ℝ≥0∞)
cons :
  ∀ (a : δ) (l : List δ)
    (ih :
      Eq (α := ℝ≥0∞) ((Measure.tprod (X := X) l μ : (a : Set (TProd X l)) → ℝ≥0∞) (Set.tprod (α := X) l s) : ℝ≥0∞)
        (List.prod (List.map (fun (i : δ) ↦ (μ i : (a : Set (X i)) → ℝ≥0∞) (s i)) l) : ℝ≥0∞)),
    Eq (α := ℝ≥0∞)
      ((Measure.tprod (X := X) (a :: l) μ : (a : Set (TProd X (a :: l))) → ℝ≥0∞) (Set.tprod (α := X) (a :: l) s) : ℝ≥0∞)
      (List.prod (List.map (fun (i : δ) ↦ (μ i : (a : Set (X i)) → ℝ≥0∞) (s i)) (a :: l)) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((Measure.tprod (X := X) l μ : (a : Set (TProd X l)) → ℝ≥0∞) (Set.tprod (α := X) l s) : ℝ≥0∞)
    (List.prod (List.map (fun (i : δ) ↦ (μ i : (a : Set (X i)) → ℝ≥0∞) (s i)) l) : ℝ≥0∞)

Tactic:
induction l with
  | nil => simp
  | cons a l ih =>
    rw [tprod_cons, Set.tprod]
    dsimp only [foldr_cons, map_cons, prod_cons]
    rw [prod_prod, ih]

Premises used: Set.tprod, List.foldr_cons, List.map_cons, MeasureTheory.Measure.prod_prod, List.cons, MeasureTheory.Measure.tprod_cons, List.prod_cons, List.nil
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : Encodable ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
_hl hnd hnd₁ : (sortedUniv ι).Nodup
⊢ Eq (α := ℝ≥0∞)
    ((map (TProd.elim' (α := α) ⋯) (Measure.tprod (X := α) (sortedUniv ι) μ) : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ s) :
      ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
rw [← MeasurableEquiv.piMeasurableEquivTProd_symm_apply, MeasurableEquiv.map_apply,
    MeasurableEquiv.piMeasurableEquivTProd_symm_apply, elim_preimage_pi, tprod_tprod _ μ, ←
    List.prod_toFinset, sortedUniv_toFinset]

Premises used: MeasurableEquiv.map_apply, MeasureTheory.Measure.tprod_tprod, Encodable.sortedUniv_toFinset, Set.elim_preimage_pi, List.prod_toFinset, MeasurableEquiv.piMeasurableEquivTProd_symm_apply
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : Encodable ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ (sortedUniv ι).Nodup

Tactic:
sortedUniv_nodup ι

Premises used: Encodable.sortedUniv_nodup
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : Encodable ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ (sortedUniv ι).Nodup

Tactic:
exact sortedUniv_nodup ι

Premises used: Encodable.sortedUniv_nodup
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : Encodable ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
rw rw₁ rw₂ :
  Eq (α := ℝ≥0∞)
    ((map (TProd.elim' (α := α) ⋯) (Measure.tprod (X := α) (sortedUniv ι) μ) : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ s) :
      ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((pi' (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
classical
  rw [pi']
  rw [← MeasurableEquiv.piMeasurableEquivTProd_symm_apply, MeasurableEquiv.map_apply,
    MeasurableEquiv.piMeasurableEquivTProd_symm_apply, elim_preimage_pi, tprod_tprod _ μ, ←
    List.prod_toFinset, sortedUniv_toFinset] <;>
  exact sortedUniv_nodup ι

Premises used: MeasurableEquiv.map_apply, MeasureTheory.Measure.pi', MeasureTheory.Measure.tprod_tprod, Encodable.sortedUniv_toFinset, Set.elim_preimage_pi, List.prod_toFinset, Encodable.sortedUniv_nodup, MeasurableEquiv.piMeasurableEquivTProd_symm_apply
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
⊢ LE.le (α := MeasurableSpace ((a : ι) → α a)) (MeasurableSpace.pi (X := α))
    (OuterMeasure.caratheodory (OuterMeasure.pi (α := α) fun (i : ι) ↦ (μ i).toOuterMeasure))

Tactic:
iSup_le ?_

Premises used: iSup_le
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
refine :
  ∀ (i : ι),
    LE.le (α := MeasurableSpace ((a : ι) → α a)) (MeasurableSpace.comap (fun (b : (a : ι) → α a) ↦ b i) (inst_1 i))
      (OuterMeasure.caratheodory (OuterMeasure.pi (α := α) fun (i : ι) ↦ (μ i).toOuterMeasure))
⊢ LE.le (α := MeasurableSpace ((a : ι) → α a)) (MeasurableSpace.pi (X := α))
    (OuterMeasure.caratheodory (OuterMeasure.pi (α := α) fun (i : ι) ↦ (μ i).toOuterMeasure))

Tactic:
refine iSup_le ?_

Premises used: iSup_le
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set ((a : ι) → α a)
hs : MeasurableSet s
⊢ MeasurableSet s

Tactic:
rw [MeasurableSpace.comap] at hs

Premises used: MeasurableSpace.comap
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
hs₁ :
  ∀ (t : Set ((a : ι) → α a)),
    piPremeasure (α := α) (fun (i : ι) ↦ (μ i).toOuterMeasure) (t ∩ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s) +
        piPremeasure (α := α) (fun (i : ι) ↦ (μ i).toOuterMeasure) (t \ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s) ≤
      piPremeasure (α := α) (fun (i : ι) ↦ (μ i).toOuterMeasure) t
⊢ MeasurableSet (α := (a : ι) → α a) ((fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s)

Tactic:
apply boundedBy_caratheodory

Premises used: MeasureTheory.OuterMeasure.boundedBy_caratheodory
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
hs₁ :
  HAdd.hAdd (α := ℝ≥0∞)
      (∏ x : ι,
        ((μ x).toOuterMeasure : (a : Set (α x)) → ℝ≥0∞)
          (eval (β := α) x '' (t ∩ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s)))
      (∏ x : ι,
        ((μ x).toOuterMeasure : (a : Set (α x)) → ℝ≥0∞)
          (eval (β := α) x '' (t \ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s))) ≤
    ∏ x : ι, ((μ x).toOuterMeasure : (a : Set (α x)) → ℝ≥0∞) (eval (β := α) x '' t)
⊢ piPremeasure (α := α) (fun (i : ι) ↦ (μ i).toOuterMeasure) (t ∩ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s) +
      piPremeasure (α := α) (fun (i : ι) ↦ (μ i).toOuterMeasure) (t \ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s) ≤
    piPremeasure (α := α) (fun (i : ι) ↦ (μ i).toOuterMeasure) t

Tactic:
simp_rw [piPremeasure]

Premises used: MeasureTheory.piPremeasure
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ HAdd.hAdd (α := ℝ≥0∞)
      (∏ x : ι,
        ((μ x).toOuterMeasure : (a : Set (α x)) → ℝ≥0∞)
          (eval (β := α) x '' (t ∩ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s)))
      (∏ x : ι,
        ((μ x).toOuterMeasure : (a : Set (α x)) → ℝ≥0∞)
          (eval (β := α) x '' (t \ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s))) ≤
    ∏ x : ι, ((μ x).toOuterMeasure : (a : Set (α x)) → ℝ≥0∞) (eval (β := α) x '' t)

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

Premises used: Finset.mem_univ, Finset.prod_add_prod_le'
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
hs₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      (((μ i).toOuterMeasure : (a : Set (α i)) → ℝ≥0∞)
          (eval (β := α) i '' (t ∩ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s)) :
        ℝ≥0∞)
      (((μ i).toOuterMeasure : (a : Set (α i)) → ℝ≥0∞)
          (eval (β := α) i '' (t \ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s)) :
        ℝ≥0∞) ≤
    ((μ i).toOuterMeasure : (a : Set (α i)) → ℝ≥0∞) (eval (β := α) i '' t)
hs₂ :
  ∀ (j : ι),
    Membership.mem (γ := Finset ι) Finset.univ j →
      j ≠ i →
        LE.le (α := ℝ≥0∞)
          (((μ j).toOuterMeasure : (a : Set (α j)) → ℝ≥0∞)
              (eval (β := α) j '' (t ∩ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s)) :
            ℝ≥0∞)
          (((μ j).toOuterMeasure : (a : Set (α j)) → ℝ≥0∞) (eval (β := α) j '' t) : ℝ≥0∞)
hs₃ :
  ∀ (j : ι),
    Membership.mem (γ := Finset ι) Finset.univ j →
      j ≠ i →
        LE.le (α := ℝ≥0∞)
          (((μ j).toOuterMeasure : (a : Set (α j)) → ℝ≥0∞)
              (eval (β := α) j '' (t \ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s)) :
            ℝ≥0∞)
          (((μ j).toOuterMeasure : (a : Set (α j)) → ℝ≥0∞) (eval (β := α) j '' t) : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞)
      (∏ x : ι,
        ((μ x).toOuterMeasure : (a : Set (α x)) → ℝ≥0∞)
          (eval (β := α) x '' (t ∩ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s)))
      (∏ x : ι,
        ((μ x).toOuterMeasure : (a : Set (α x)) → ℝ≥0∞)
          (eval (β := α) x '' (t \ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s))) ≤
    ∏ x : ι, ((μ x).toOuterMeasure : (a : Set (α x)) → ℝ≥0∞) (eval (β := α) x '' t)

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

Premises used: Finset.mem_univ, Finset.prod_add_prod_le'
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      (((μ i).toOuterMeasure : (a : Set (α i)) → ℝ≥0∞)
          (eval (β := α) i '' (t ∩ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s)) :
        ℝ≥0∞)
      (((μ i).toOuterMeasure : (a : Set (α i)) → ℝ≥0∞)
          (eval (β := α) i '' (t \ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s)) :
        ℝ≥0∞) ≤
    ((μ i).toOuterMeasure : (a : Set (α i)) → ℝ≥0∞) (eval (β := α) i '' t)

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

Premises used: Set.image_inter_preimage, Set.image_diff_preimage, MeasureTheory.measure_inter_add_diff
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
j : ι
h : j ≠ i
hs₁ : t ∩ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s ⊆ t
⊢ LE.le (α := ℝ≥0∞)
    (((μ j).toOuterMeasure : (a : Set (α j)) → ℝ≥0∞) (eval (β := α) j '' (t ∩ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s)) :
      ℝ≥0∞)
    (((μ j).toOuterMeasure : (a : Set (α j)) → ℝ≥0∞) (eval (β := α) j '' t) : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
j : ι
h : j ≠ i
⊢ t ∩ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s ⊆ t

Tactic:
apply inter_subset_left

Premises used: Set.inter_subset_left
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
j : ι
h : j ≠ i
hs₁ : t \ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s ⊆ t
⊢ LE.le (α := ℝ≥0∞)
    (((μ j).toOuterMeasure : (a : Set (α j)) → ℝ≥0∞) (eval (β := α) j '' (t \ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s)) :
      ℝ≥0∞)
    (((μ j).toOuterMeasure : (a : Set (α j)) → ℝ≥0∞) (eval (β := α) j '' t) : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
j : ι
h : j ≠ i
⊢ t \ (fun (b : (a : ι) → α a) ↦ b i) ⁻¹' s ⊆ t

Tactic:
apply diff_subset

Premises used: Set.diff_subset
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
refine_1 :
  LE.le (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
refine_2 :
  LE.le (α := ℝ≥0∞) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
refine_1 :
  LE.le (α := ℝ≥0∞)
    ((OuterMeasure.pi (α := α) fun (i : ι) ↦ (μ i).toOuterMeasure : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ s) :
      ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
rw [Measure.pi, toMeasure_apply _ _ (MeasurableSet.pi countable_univ fun i _ => hs i)]

Premises used: Set.countable_univ, MeasureTheory.toMeasure_apply, MeasureTheory.Measure.pi, MeasurableSet.pi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ LE.le (α := ℝ≥0∞)
    ((OuterMeasure.pi (α := α) fun (i : ι) ↦ (μ i).toOuterMeasure : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ s) :
      ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
apply OuterMeasure.pi_pi_le

Premises used: MeasureTheory.OuterMeasure.pi_pi_le
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
refine_2 :
  ∀ (this : Encodable ι),
    LE.le (α := ℝ≥0∞) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
      ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)

Tactic:
haveI : Encodable ι := Fintype.toEncodable ι
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
this : Encodable ι
refine_2 :
  LE.le (α := ℝ≥0∞) ((pi' (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    ((OuterMeasure.pi (α := α) fun (i : ι) ↦ (μ i).toOuterMeasure : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ s) :
      ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)

Tactic:
simp_rw [← pi'_pi μ s, Measure.pi,
      toMeasure_apply _ _ (MeasurableSet.pi countable_univ fun i _ => hs i)]

Premises used: MeasureTheory.Measure.pi'_pi, Set.countable_univ, MeasureTheory.toMeasure_apply, MeasureTheory.Measure.pi, MeasurableSet.pi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
this_1 : Encodable ι
this : (pi' (α := α) μ).toOuterMeasure ≤ OuterMeasure.pi (α := α) fun (i : ι) ↦ (μ i).toOuterMeasure
⊢ LE.le (α := ℝ≥0∞) ((pi' (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    ((OuterMeasure.pi (α := α) fun (i : ι) ↦ (μ i).toOuterMeasure : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ s) :
      ℝ≥0∞)

Tactic:
this _
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
this_1 : Encodable ι
this : (pi' (α := α) μ).toOuterMeasure ≤ OuterMeasure.pi (α := α) fun (i : ι) ↦ (μ i).toOuterMeasure
⊢ LE.le (α := ℝ≥0∞) ((pi' (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    ((OuterMeasure.pi (α := α) fun (i : ι) ↦ (μ i).toOuterMeasure : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ s) :
      ℝ≥0∞)

Tactic:
exact this _