awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
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) μ
pos :
  ∀ (hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L),
    L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite →
      ∀ (h : Function.HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.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,
            L.support.mulIndicator (fun (i : ι) ↦ f i) i.down)
          μ
neg :
  ∀ (hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L),
    L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite →
      ¬Function.HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down) →
        AEStronglyMeasurable.{u_4, u_5} (β := E) 1 μ
⊢ AEStronglyMeasurable.{u_4, u_5} (β := E)
    (if h : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L then
      if L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite then
        if h : Function.HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down) then
          ∏
            i ∈
              Finite.toFinset (s :=
                Function.mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)) h,
            L.support.mulIndicator (fun (i : ι) ↦ f i) i.down
        else 1
      else
        if HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L then 1
        else Exists.choose (p := fun (a : X → E) ↦ HasProd (fun (i : ι) ↦ f i) a L) h
    else 1)
    μ
have pos₁ : ∀ (hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L),
  ¬(L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite) →
    HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L → AEStronglyMeasurable.{u_4, u_5} (β := E) 1 μ
Tactic: split_ifs with hm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
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) μ
pos :
  ∀ (hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L),
    L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite →
      ∀ (h : Function.HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.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,
            L.support.mulIndicator (fun (i : ι) ↦ f i) i.down)
          μ
neg :
  ∀ (hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L),
    L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite →
      ¬Function.HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down) →
        AEStronglyMeasurable.{u_4, u_5} (β := E) 1 μ
pos₁ :
  ∀ (hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L),
    ¬(L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite) →
      HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L → AEStronglyMeasurable.{u_4, u_5} (β := E) 1 μ
⊢ AEStronglyMeasurable.{u_4, u_5} (β := E)
    (if h : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L then
      if L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite then
        if h : Function.HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down) then
          ∏
            i ∈
              Finite.toFinset (s :=
                Function.mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)) h,
            L.support.mulIndicator (fun (i : ι) ↦ f i) i.down
        else 1
      else
        if HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L then 1
        else Exists.choose (p := fun (a : X → E) ↦ HasProd (fun (i : ι) ↦ f i) a L) h
    else 1)
    μ
have neg₁ : ∀ (hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L),
  ¬(L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite) →
    ¬HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L →
      AEStronglyMeasurable (Exists.choose (p := fun (a : X → E) ↦ HasProd (fun (i : ι) ↦ f i) a L) hm) μ
Tactic: split_ifs with hm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
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) μ
pos :
  ∀ (hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L),
    L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite →
      ∀ (h : Function.HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.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,
            L.support.mulIndicator (fun (i : ι) ↦ f i) i.down)
          μ
neg :
  ∀ (hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L),
    L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite →
      ¬Function.HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down) →
        AEStronglyMeasurable.{u_4, u_5} (β := E) 1 μ
pos₁ :
  ∀ (hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L),
    ¬(L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite) →
      HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L → AEStronglyMeasurable.{u_4, u_5} (β := E) 1 μ
neg₁ :
  ∀ (hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L),
    ¬(L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite) →
      ¬HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L →
        AEStronglyMeasurable (Exists.choose (p := fun (a : X → E) ↦ HasProd (fun (i : ι) ↦ f i) a L) hm) μ
⊢ AEStronglyMeasurable.{u_4, u_5} (β := E)
    (if h : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L then
      if L.HasSupport ∧ ((Function.mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite then
        if h : Function.HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down) then
          ∏
            i ∈
              Finite.toFinset (s :=
                Function.mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)) h,
            L.support.mulIndicator (fun (i : ι) ↦ f i) i.down
        else 1
      else
        if HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L then 1
        else Exists.choose (p := fun (a : X → E) ↦ HasProd (fun (i : ι) ↦ f i) a L) h
    else 1)
    μ
have neg₂ : ∀ (hm : ¬Multipliable (α := X → E) (fun (i : ι) ↦ f i) L), AEStronglyMeasurable.{u_4, u_5} (β := E) 1 μ
Tactic: split_ifs with hm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
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)
⊢ 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)
    μ
have 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) μ
Tactic: refine Finset.aestronglyMeasurable_prod _ (fun _ _ ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
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
⊢ AEStronglyMeasurable.{u_4, u_5} (β := E) (L.support.mulIndicator (fun (i : ι) ↦ f i) x.down) μ
have pos : AEStronglyMeasurable (if x.down ∈ L.support then f x.down else 1) μ
Tactic: rw [Set.mulIndicator]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
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
⊢ AEStronglyMeasurable (if x.down ∈ L.support then f x.down else 1) μ
have pos : x.down ∈ L.support → AEStronglyMeasurable (f x.down) μ
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
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) μ
⊢ AEStronglyMeasurable (if x.down ∈ L.support then f x.down else 1) μ
have neg : x.down ∉ L.support → AEStronglyMeasurable.{u_4, u_5} (β := E) 1 μ
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (goal)
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
⊢ AEStronglyMeasurable (Exists.choose (p := fun (a : X → E) ↦ HasProd (fun (i : ι) ↦ f i) a L) hm) μ
have 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))
Tactic: apply aestronglyMeasurable_of_tendsto_ae L.filter (f := fun s => ∏ i ∈ s, f i) (by fun_prop)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Projective (goal)
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 ι
⊢ P I = 0
have obtain : ∀ (i : ι) (hi : IsEmpty.{u_2 + 1} (α i)), P I = 0
Tactic: obtain ⟨i, hi⟩ := isEmpty_pi.mp h
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Projective (goal)
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)
⊢ P I = 0
have rw : Eq (α := Measure ((j : ↥I) → α (↑j : ι)))
  (Measure.map (α := (i_1 : ↥(insert i I)) → α (↑i_1 : ι)) (Finset.restrict₂ (π := α) sorry) (P (insert i I))) 0
Tactic: rw [hP (insert i I) I (I.subset_insert i)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Projective (hypothesis)
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)
⊢ Eq (α := Measure ((j : ↥I) → α (↑j : ι)))
    (Measure.map (α := (i_1 : ↥(insert i I)) → α (↑i_1 : ι)) (Finset.restrict₂ (π := α) ⋯) (P (insert i I))) 0
have this : IsEmpty ((j : ↥(insert i I)) → α (↑j : ι))
Tactic: have : IsEmpty (Π j : ↑(insert i I), α j) := by simp [hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Projective (goal)
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₂ (π := α) ⋯) (P (insert i I))) 0
have rw : Eq (α := Measure ((j : ↥I) → α (↑j : ι)))
  (Measure.map (α := (i_1 : ↥(insert i I)) → α (↑i_1 : ι)) (Finset.restrict₂ (π := α) sorry) 0) 0
Tactic: rw [(P (insert i I)).eq_zero_of_isEmpty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Projective (goal)
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 ι
⊢ P I = 0
have obtain : ∀ (i : ι) (hi : IsEmpty.{u_2 + 1} (α i)), 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Projective (goal)
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
have obtain₁ : ∀ (i : ι) (hi : IsEmpty.{u_2 + 1} (α i)),
  Eq (α := Measure ((j : ↥I) → α (↑j : ι)))
    (Measure.map (α := (i_1 : ↥(insert i I)) → α (↑i_1 : ι)) (Finset.restrict₂ (π := α) sorry) (P (insert i 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Projective (goal)
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
⊢ P I = 0
have 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₂ (π := α) sorry) (P (insert i 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Projective (goal)
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
⊢ P I = 0
have 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₂ (π := α) sorry) 0) 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Projective (goal)
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)
have rw : Eq (α := Set ((i : ↥I) → α (↑i : ι))) univ univ
Tactic: rw [preimage_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Projective (hypothesis)
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 (α := 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)
Tactic: have : (univ : Set (∀ i : I, α i)) =
      Finset.restrict₂ hJI ⁻¹' (univ : Set (∀ i : J, α i)) := by
    rw [preimage_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Projective (goal)
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)
⊢ Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) univ : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)
have 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)
Tactic: rw [this, ← Measure.map_apply _ MeasurableSet.univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Projective (goal)
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)
⊢ Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) univ : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)
have rw₁ : MeasurableSpace ((i : ↥J) → α (↑i : ι))
Tactic: rw [this, ← Measure.map_apply _ MeasurableSet.univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Projective (goal)
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 : ι))
⊢ Eq (α := ENNReal) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ENNReal) univ : ENNReal)
    ((P J : (a : Set ((j : ↥J) → α (↑j : ι))) → ENNReal) univ : ENNReal)
have rw₂ : Measurable (α := (j : ↥I) → α (↑j : ι)) (Finset.restrict₂ (π := α) hJI)
Tactic: rw [this, ← Measure.map_apply _ MeasurableSet.univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Projective (goal)
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)
⊢ 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 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)
Tactic: rw [hP I J hJI]