awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : ContinuousMul E
L : SummationFilter ι
inst_5 : L.NeBot
inst_6 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite
h_2 : Function.HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)
pos :
  ∀
    x ∈
      Finite.toFinset (s := Function.mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down))
        h_2,
    AEStronglyMeasurable.{u_4, u_5} (β := E) (L.support.mulIndicator (fun (i : ι) ↦ f i) x.down) μ
⊢ AEStronglyMeasurable.{u_4, u_5} (β := E)
    (∏
      i ∈
        Finite.toFinset (s :=
          Function.mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)) h_2,
      L.support.mulIndicator (fun (i : ι) ↦ f i) i.down)
    μ

Tactic:
refine Finset.aestronglyMeasurable_prod _ (fun _ _ ↦ ?_)

Premises used: Finset.aestronglyMeasurable_prod
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : ContinuousMul E
L : SummationFilter ι
inst_5 : L.NeBot
inst_6 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite
h_2 : Function.HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)
x : PLift ι
h_3 :
  x ∈
    Finite.toFinset (s := Function.mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down))
      h_2
pos : AEStronglyMeasurable (if x.down ∈ L.support then f x.down else 1) μ
⊢ AEStronglyMeasurable.{u_4, u_5} (β := E) (L.support.mulIndicator (fun (i : ι) ↦ f i) x.down) μ

Tactic:
rw [Set.mulIndicator]

Premises used: Set.mulIndicator
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : ContinuousMul E
L : SummationFilter ι
inst_5 : L.NeBot
inst_6 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite
h_2 : Function.HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)
x : PLift ι
h_3 :
  x ∈
    Finite.toFinset (s := Function.mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down))
      h_2
pos : x.down ∈ L.support → AEStronglyMeasurable (f x.down) μ
neg : x.down ∉ L.support → AEStronglyMeasurable.{u_4, u_5} (β := E) 1 μ
⊢ AEStronglyMeasurable (if x.down ∈ L.support then f x.down else 1) μ

Tactic:
split_ifs
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : ContinuousMul E
L : SummationFilter ι
inst_5 : L.NeBot
inst_6 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite
h_2 : Function.HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)
x : PLift ι
h_3 :
  x ∈
    Finite.toFinset (s := Function.mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down))
      h_2
h_4 : x.down ∈ L.support
⊢ AEStronglyMeasurable (f x.down) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : ContinuousMul E
L : SummationFilter ι
inst_5 : L.NeBot
inst_6 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite
h_2 : Function.HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)
x : PLift ι
h_3 :
  x ∈
    Finite.toFinset (s := Function.mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down))
      h_2
h_4 : x.down ∉ L.support
⊢ AEStronglyMeasurable.{u_4, u_5} (β := E) 1 μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : ContinuousMul E
L : SummationFilter ι
inst_5 : L.NeBot
inst_6 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : ¬(L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite)
h_2 : ¬HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L
⊢ ∀ (i : Finset ι), AEStronglyMeasurable.{u_4, u_5} (β := E) ((fun (s : Finset ι) ↦ (∏ i ∈ s, f i : X → E)) i) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : ContinuousMul E
L : SummationFilter ι
inst_5 : L.NeBot
inst_6 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : ¬(L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite)
h_2 : ¬HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L
neg :
  ∀ᵐ (x : X) ∂μ,
    Tendsto (fun (n : Finset ι) ↦ (∏ i ∈ n, f i) x) L.filter
      (𝓝 (Exists.choose (p := fun (a : X → E) ↦ HasProd (fun (i : ι) ↦ f i) a L) hm x))
⊢ AEStronglyMeasurable (Exists.choose (p := fun (a : X → E) ↦ HasProd (fun (i : ι) ↦ f i) a L) hm) μ

Tactic:
apply aestronglyMeasurable_of_tendsto_ae L.filter (f := fun s => ∏ i ∈ s, f i) (by fun_prop)

Premises used: aestronglyMeasurable_of_tendsto_ae, SummationFilter.filter
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : ContinuousMul E
L : SummationFilter ι
inst_5 : L.NeBot
inst_6 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : ¬(L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite)
h_2 : ¬HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L
⊢ ∀ᵐ (x : X) ∂μ,
    Tendsto (fun (n : Finset ι) ↦ (∏ i ∈ n, f i) x) L.filter
      (𝓝 (Exists.choose (p := fun (a : X → E) ↦ HasProd (fun (i : ι) ↦ f i) a L) hm x))

Tactic:
.of_forall fun x ↦ hm.choose_spec.apply_nhds x

Premises used: Exists.choose_spec, Filter.Eventually.of_forall, Filter.Tendsto.apply_nhds
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : ContinuousMul E
L : SummationFilter ι
inst_5 : L.NeBot
inst_6 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : ¬(L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite)
h_2 : ¬HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L
⊢ ∀ᵐ (x : X) ∂μ,
    Tendsto (fun (n : Finset ι) ↦ (∏ i ∈ n, f i) x) L.filter
      (𝓝 (Exists.choose (p := fun (a : X → E) ↦ HasProd (fun (i : ι) ↦ f i) a L) hm x))

Tactic:
exact .of_forall fun x ↦ hm.choose_spec.apply_nhds x
-- Module: Mathlib.MeasureTheory.Constructions.Projective
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
h : IsEmpty ((i : ι) → α i)
hP : IsProjectiveMeasureFamily (α := α) P
I : Finset ι
obtain : ∀ (i : ι) (hi : IsEmpty.{u_2 + 1} (α i)), P I = 0
⊢ P I = 0

Tactic:
obtain ⟨i, hi⟩ := isEmpty_pi.mp h

Premises used: isEmpty_pi, Iff.mp
-- Module: Mathlib.MeasureTheory.Constructions.Projective
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
h : IsEmpty ((i : ι) → α i)
hP : IsProjectiveMeasureFamily (α := α) P
I : Finset ι
i : ι
hi : IsEmpty.{u_2 + 1} (α i)
rw :
  Eq (α := Measure ((j : ↥I) → α (↑j : ι)))
    (Measure.map (α := (i_1 : ↥(insert i I)) → α (↑i_1 : ι)) (Finset.restrict₂ (π := α) ⋯) (P (insert i I))) 0
⊢ P I = 0

Tactic:
rw [hP (insert i I) I (I.subset_insert i)]

Premises used: Insert.insert, Finset.subset_insert
-- Module: Mathlib.MeasureTheory.Constructions.Projective
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
h : IsEmpty ((i : ι) → α i)
hP : IsProjectiveMeasureFamily (α := α) P
I : Finset ι
i : ι
hi : IsEmpty.{u_2 + 1} (α i)
⊢ IsEmpty ((j : ↥(insert i I)) → α (↑j : ι))

Tactic:
simp [hi]
-- Module: Mathlib.MeasureTheory.Constructions.Projective
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
h : IsEmpty ((i : ι) → α i)
hP : IsProjectiveMeasureFamily (α := α) P
I : Finset ι
i : ι
hi : IsEmpty.{u_2 + 1} (α i)
⊢ IsEmpty ((j : ↥(insert i I)) → α (↑j : ι))

Tactic:
have : IsEmpty (Π j : ↑(insert i I), α j) := by simp [hi]
-- Module: Mathlib.MeasureTheory.Constructions.Projective
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
h : IsEmpty ((i : ι) → α i)
hP : IsProjectiveMeasureFamily (α := α) P
I : Finset ι
i : ι
hi : IsEmpty.{u_2 + 1} (α i)
this : IsEmpty ((j : ↥(insert i I)) → α (↑j : ι))
rw :
  Eq (α := Measure ((j : ↥I) → α (↑j : ι)))
    (Measure.map (α := (i_1 : ↥(insert i I)) → α (↑i_1 : ι)) (Finset.restrict₂ (π := α) ⋯) 0) 0
⊢ Eq (α := Measure ((j : ↥I) → α (↑j : ι)))
    (Measure.map (α := (i_1 : ↥(insert i I)) → α (↑i_1 : ι)) (Finset.restrict₂ (π := α) ⋯) (P (insert i I))) 0

Tactic:
rw [(P (insert i I)).eq_zero_of_isEmpty]

Premises used: Insert.insert, MeasureTheory.Measure.eq_zero_of_isEmpty
-- Module: Mathlib.MeasureTheory.Constructions.Projective
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
h : IsEmpty ((i : ι) → α i)
hP : IsProjectiveMeasureFamily (α := α) P
I : Finset ι
i : ι
hi : IsEmpty.{u_2 + 1} (α i)
this : IsEmpty ((j : ↥(insert i I)) → α (↑j : ι))
⊢ Eq (α := Measure ((j : ↥I) → α (↑j : ι)))
    (Measure.map (α := (i_1 : ↥(insert i I)) → α (↑i_1 : ι)) (Finset.restrict₂ (π := α) ⋯) 0) 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Constructions.Projective
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
h : IsEmpty ((i : ι) → α i)
hP : IsProjectiveMeasureFamily (α := α) P
I : Finset ι
obtain : ∀ (i : ι) (hi : IsEmpty.{u_2 + 1} (α i)), P I = 0
obtain₁ :
  ∀ (i : ι) (hi : IsEmpty.{u_2 + 1} (α i)),
    Eq (α := Measure ((j : ↥I) → α (↑j : ι)))
      (Measure.map (α := (i_1 : ↥(insert i I)) → α (↑i_1 : ι)) (Finset.restrict₂ (π := α) ⋯) (P (insert i I))) 0
obtain₂ :
  ∀ (i : ι) (hi : IsEmpty.{u_2 + 1} (α i)) (this : IsEmpty ((j : ↥(insert i I)) → α (↑j : ι))),
    Eq (α := Measure ((j : ↥I) → α (↑j : ι)))
      (Measure.map (α := (i_1 : ↥(insert i I)) → α (↑i_1 : ι)) (Finset.restrict₂ (π := α) ⋯) (P (insert i I))) 0
obtain₃ :
  ∀ (i : ι) (hi : IsEmpty.{u_2 + 1} (α i)) (this : IsEmpty ((j : ↥(insert i I)) → α (↑j : ι))),
    Eq (α := Measure ((j : ↥I) → α (↑j : ι)))
      (Measure.map (α := (i_1 : ↥(insert i I)) → α (↑i_1 : ι)) (Finset.restrict₂ (π := α) ⋯) 0) 0
⊢ P I = 0

Tactic:
classical
  obtain ⟨i, hi⟩ := isEmpty_pi.mp h
  rw [hP (insert i I) I (I.subset_insert i)]
  have : IsEmpty (Π j : ↑(insert i I), α j) := by simp [hi]
  rw [(P (insert i I)).eq_zero_of_isEmpty]
  simp

Premises used: isEmpty_pi, Iff.mp
-- Module: Mathlib.MeasureTheory.Constructions.Projective
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
I J : Finset ι
hP : IsProjectiveMeasureFamily (α := α) P
hJI : J ⊆ I
rw rw₁ : Eq (α := Set ((i : ↥I) → α (↑i : ι))) univ univ
⊢ Eq (α := Set ((i : ↥I) → α (↑i : ι))) univ (Finset.restrict₂ (π := α) hJI ⁻¹' univ)

Tactic:
rw [preimage_univ]

Premises used: Set.preimage_univ
-- Module: Mathlib.MeasureTheory.Constructions.Projective
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
I J : Finset ι
hP : IsProjectiveMeasureFamily (α := α) P
hJI : J ⊆ I
⊢ Eq (α := Set ((i : ↥I) → α (↑i : ι))) univ (Finset.restrict₂ (π := α) hJI ⁻¹' univ)

Tactic:
have : (univ : Set (∀ i : I, α i)) =
      Finset.restrict₂ hJI ⁻¹' (univ : Set (∀ i : J, α i)) := by
    rw [preimage_univ]
-- Module: Mathlib.MeasureTheory.Constructions.Projective
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
I J : Finset ι
hP : IsProjectiveMeasureFamily (α := α) P
hJI : J ⊆ I
this : Eq (α := Set ((i : ↥I) → α (↑i : ι))) univ (Finset.restrict₂ (π := α) hJI ⁻¹' univ)
rw :
  Eq (α := ENNReal)
    ((Measure.map (Finset.restrict₂ (π := α) hJI) (P I) : (a : Set ((i : ↥J) → α (↑i : ι))) → ENNReal) univ : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)
rw₁ : MeasurableSpace ((i : ↥J) → α (↑i : ι))
rw₂ : Measurable (α := (j : ↥I) → α (↑j : ι)) (Finset.restrict₂ (π := α) hJI)
⊢ Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) univ : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)

Tactic:
rw [this, ← Measure.map_apply _ MeasurableSet.univ]

Premises used: MeasureTheory.Measure.map_apply, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Constructions.Projective
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
I J : Finset ι
hP : IsProjectiveMeasureFamily (α := α) P
hJI : J ⊆ I
this : Eq (α := Set ((i : ↥I) → α (↑i : ι))) univ (Finset.restrict₂ (π := α) hJI ⁻¹' univ)
rw rw₁ :
  Eq (α := ENNReal)
    ((Measure.map (Finset.restrict₂ (π := α) hJI) (P I) : (a : Set ((i : ↥J) → α (↑i : ι))) → ENNReal) univ : ENNReal)
    ((Measure.map (Finset.restrict₂ (π := α) hJI) (P I) : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)
⊢ Eq (α := ENNReal)
    ((Measure.map (Finset.restrict₂ (π := α) hJI) (P I) : (a : Set ((i : ↥J) → α (↑i : ι))) → ENNReal) univ : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)

Tactic:
rw [hP I J hJI]
-- Module: Mathlib.MeasureTheory.Constructions.Projective
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
I J : Finset ι
hP : IsProjectiveMeasureFamily (α := α) P
hJI : J ⊆ I
this : Eq (α := Set ((i : ↥I) → α (↑i : ι))) univ (Finset.restrict₂ (π := α) hJI ⁻¹' univ)
⊢ Measurable (α := (j : ↥I) → α (↑j : ι)) (Finset.restrict₂ (π := α) hJI)

Tactic:
measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _)

Premises used: measurable_pi_lambda, measurable_pi_apply, Subtype.mk, Finset.restrict₂._proof_1, Subtype.val
-- Module: Mathlib.MeasureTheory.Constructions.Projective
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
I J : Finset ι
hP : IsProjectiveMeasureFamily (α := α) P
hJI : J ⊆ I
this : Eq (α := Set ((i : ↥I) → α (↑i : ι))) univ (Finset.restrict₂ (π := α) hJI ⁻¹' univ)
⊢ Measurable (α := (j : ↥I) → α (↑j : ι)) (Finset.restrict₂ (π := α) hJI)

Tactic:
exact measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _)

Premises used: measurable_pi_lambda, measurable_pi_apply
-- Module: Mathlib.MeasureTheory.Constructions.Projective
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
I J : Finset ι
hP : IsProjectiveMeasureFamily (α := α) P
hJI : J ⊆ I
have : Eq (α := Set ((i : ↥I) → α (↑i : ι))) univ (Finset.restrict₂ (π := α) hJI ⁻¹' univ)
have₁ :
  ∀ (this : Eq (α := Set ((i : ↥I) → α (↑i : ι))) univ (Finset.restrict₂ (π := α) hJI ⁻¹' univ)),
    Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) univ : ENNReal)
      ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)
have₂ : Eq (α := Set ((i : ↥I) → α (↑i : ι))) univ (Finset.restrict₂ (π := α) hJI ⁻¹' univ)
have₃ have₄ :
  ∀ (this : Eq (α := Set ((i : ↥I) → α (↑i : ι))) univ (Finset.restrict₂ (π := α) hJI ⁻¹' univ)),
    Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) univ : ENNReal)
      ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)
have₅ :
  ∀ (this : Eq (α := Set ((i : ↥I) → α (↑i : ι))) univ (Finset.restrict₂ (π := α) hJI ⁻¹' univ)),
    Eq (α := ENNReal)
      ((Measure.map (Finset.restrict₂ (π := α) hJI) (P I) : (a : Set ((i : ↥J) → α (↑i : ι))) → ENNReal) univ : ENNReal)
      ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)
have₆ :
  (this : Eq (α := Set ((i : ↥I) → α (↑i : ι))) univ (Finset.restrict₂ (π := α) hJI ⁻¹' univ)) →
    MeasurableSpace ((i : ↥J) → α (↑i : ι))
have₇ have₈ :
  ∀ (this : Eq (α := Set ((i : ↥I) → α (↑i : ι))) univ (Finset.restrict₂ (π := α) hJI ⁻¹' univ)),
    Measurable (α := (j : ↥I) → α (↑j : ι)) (Finset.restrict₂ (π := α) hJI)
⊢ Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) univ : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)

Tactic:
classical
  have : (univ : Set (∀ i : I, α i)) =
      Finset.restrict₂ hJI ⁻¹' (univ : Set (∀ i : J, α i)) := by
    rw [preimage_univ]
  rw [this, ← Measure.map_apply _ MeasurableSet.univ]
  · rw [hP I J hJI]
  · exact measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _)

Premises used: measurable_pi_lambda, MeasureTheory.Measure.map_apply, measurable_pi_apply, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Constructions.Projective
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
hP : IsProjectiveMeasureFamily (α := α) P
I J : Finset ι
rw :
  Eq (α := ENNReal) ((P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ENNReal) univ : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)
rw₁ : Finset ι
rw₂ :
  Eq (α := ENNReal) ((P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ENNReal) univ : ENNReal)
    ((P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ENNReal) univ : ENNReal)
rw₃ : Finset ι
rw₄ :
  Eq (α := ENNReal) ((P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ENNReal) univ : ENNReal)
    ((P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ENNReal) univ : ENNReal)
rw₅ : Finset ι
⊢ Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) univ : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)

Tactic:
rw [← hP.measure_univ_eq_of_subset I.subset_union_left,
    ← hP.measure_univ_eq_of_subset (I.subset_union_right (s₂ := J))]

Premises used: MeasureTheory.IsProjectiveMeasureFamily.measure_univ_eq_of_subset, Finset.subset_union_left, Finset.subset_union_right
-- Module: Mathlib.MeasureTheory.Constructions.Projective
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
hP : IsProjectiveMeasureFamily (α := α) P
I J : Finset ι
rw :
  Eq (α := ENNReal) ((P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ENNReal) univ : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)
rw₁ : Finset ι
rw₂ :
  Eq (α := ENNReal) ((P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ENNReal) univ : ENNReal)
    ((P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ENNReal) univ : ENNReal)
rw₃ : Finset ι
rw₄ :
  Eq (α := ENNReal) ((P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ENNReal) univ : ENNReal)
    ((P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ENNReal) univ : ENNReal)
rw₅ : Finset ι
⊢ Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) univ : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)

Tactic:
classical
  rw [← hP.measure_univ_eq_of_subset I.subset_union_left,
    ← hP.measure_univ_eq_of_subset (I.subset_union_right (s₂ := J))]
-- Module: Mathlib.MeasureTheory.Constructions.Projective
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
I J : Finset ι
hP : IsProjectiveMeasureFamily (α := α) P
S : Set ((i : ↥I) → α (↑i : ι))
T : Set ((i : ↥J) → α (↑i : ι))
hT : MeasurableSet T
h_eq : cylinder (α := α) I S = cylinder (α := α) J T
hJI : J ⊆ I
h : IsEmpty ((i : ι) → α i)
this :
  ∀ (I : Finset ι), Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) univ : ENNReal) (0 : ENNReal)
⊢ ∀ (I : Finset ι), P I = 0

Tactic:
simp only [Measure.measure_univ_eq_zero] at this

Premises used: MeasureTheory.Measure.measure_univ_eq_zero
-- Module: Mathlib.MeasureTheory.Constructions.Projective
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
I J : Finset ι
hP : IsProjectiveMeasureFamily (α := α) P
S : Set ((i : ↥I) → α (↑i : ι))
T : Set ((i : ↥J) → α (↑i : ι))
hT : MeasurableSet T
h_eq : cylinder (α := α) I S = cylinder (α := α) J T
hJI : J ⊆ I
h : IsEmpty ((i : ι) → α i)
this : ∀ (I : Finset ι), P I = 0
⊢ Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) S : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) T : ENNReal)

Tactic:
simp [this]
-- Module: Mathlib.MeasureTheory.Constructions.Projective
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
I J : Finset ι
hP : IsProjectiveMeasureFamily (α := α) P
S : Set ((i : ↥I) → α (↑i : ι))
T : Set ((i : ↥J) → α (↑i : ι))
hT : MeasurableSet T
h_eq : cylinder (α := α) I S = cylinder (α := α) J T
hJI : J ⊆ I
h : IsEmpty ((i : ι) → α i)
inl :
  ∀ (I : Finset ι), Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) univ : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) S : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) T : ENNReal)

Tactic:
suffices ∀ I, P I univ = 0 by
      simp only [Measure.measure_univ_eq_zero] at this
      simp [this]
-- Module: Mathlib.MeasureTheory.Constructions.Projective
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
I J : Finset ι
hP : IsProjectiveMeasureFamily (α := α) P
S : Set ((i : ↥I) → α (↑i : ι))
T : Set ((i : ↥J) → α (↑i : ι))
hT : MeasurableSet T
h_eq : cylinder (α := α) I S = cylinder (α := α) J T
hJI : J ⊆ I
h : IsEmpty ((i : ι) → α i)
⊢ ∀ (I : Finset ι), Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) univ : ENNReal) (0 : ENNReal)

Tactic:
simpa using eq_zero_of_isEmpty hP

Premises used: MeasureTheory.IsProjectiveMeasureFamily.eq_zero_of_isEmpty