awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
X : Type u_6
E : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableMul₂ E
L : SummationFilter ι
inst_7 : L.NeBot
inst_8 : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), Measurable (f i)
pos :
  ∀ (hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L),
    L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite →
      ∀ (h : HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)),
        Measurable.{u_6, u_7} (α := X) (β := E)
          (∏
            i ∈
              Finite.toFinset (s := 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 ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite →
      ¬HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down) →
        Measurable.{u_6, u_7} (α := X) (β := E) 1
pos₁ :
  ∀ (hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L),
    ¬(L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite) →
      HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L → Measurable.{u_6, u_7} (α := X) (β := E) 1
neg₁ :
  ∀ (hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L),
    ¬(L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite) →
      ¬HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L →
        Measurable (Exists.choose (p := fun (a : X → E) ↦ HasProd (fun (i : ι) ↦ f i) a L) hm)
⊢ Measurable.{u_6, u_7} (α := X) (β := E)
    (if h : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L then
      if L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite then
        if h : HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down) then
          ∏
            i ∈
              Finite.toFinset (s := 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), Measurable.{u_6, u_7} (α := X) (β := E) 1
Tactic: split_ifs with hm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
X : Type u_6
E : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableMul₂ E
L : SummationFilter ι
inst_7 : L.NeBot
inst_8 : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), Measurable (f i)
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite
h_2 : HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)
⊢ Measurable.{u_6, u_7} (α := X) (β := E)
    (∏ i ∈ Finite.toFinset (s := 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 := mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)) h_2,
  Measurable (HasUncurry.uncurry (α := X → X → E) fun (a : X) ↦ L.support.mulIndicator (fun (i : ι) ↦ f i) x.down)
Tactic: refine Finset.measurable_prod_apply (fun _ _ ↦ ?_) measurable_id
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
X : Type u_6
E : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableMul₂ E
L : SummationFilter ι
inst_7 : L.NeBot
inst_8 : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), Measurable (f i)
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite
h_2 : HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)
x : PLift ι
h_3 : x ∈ Finite.toFinset (s := mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)) h_2
⊢ Measurable (HasUncurry.uncurry (α := X → X → E) fun (a : X) ↦ L.support.mulIndicator (fun (i : ι) ↦ f i) x.down)
have pos : Measurable (HasUncurry.uncurry (α := X → X → E) fun (a : X) ↦ if x.down ∈ L.support then f x.down else 1)
Tactic: rw [Set.mulIndicator]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
X : Type u_6
E : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableMul₂ E
L : SummationFilter ι
inst_7 : L.NeBot
inst_8 : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), Measurable (f i)
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite
h_2 : HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)
x : PLift ι
h_3 : x ∈ Finite.toFinset (s := mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)) h_2
⊢ Measurable (HasUncurry.uncurry (α := X → X → E) fun (a : X) ↦ if x.down ∈ L.support then f x.down else 1)
have pos : x.down ∈ L.support → Measurable (HasUncurry.uncurry (α := X → X → E) fun (a : X) ↦ f x.down)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
X : Type u_6
E : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableMul₂ E
L : SummationFilter ι
inst_7 : L.NeBot
inst_8 : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), Measurable (f i)
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite
h_2 : HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)
x : PLift ι
h_3 : x ∈ Finite.toFinset (s := mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)) h_2
pos : x.down ∈ L.support → Measurable (HasUncurry.uncurry (α := X → X → E) fun (a : X) ↦ f x.down)
⊢ Measurable (HasUncurry.uncurry (α := X → X → E) fun (a : X) ↦ if x.down ∈ L.support then f x.down else 1)
have neg : x.down ∉ L.support → Measurable (HasUncurry.uncurry (α := X → X → E) fun (a : X) ↦ 1)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
X : Type u_6
E : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableMul₂ E
L : SummationFilter ι
inst_7 : L.NeBot
inst_8 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
⊢ AEMeasurable.{u_6, u_7} (β := E) (∏'[L] (i : ι), f i) μ
have rw : AEMeasurable.{u_6, u_7} (β := E)
  (if h : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L then
    if L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite then
      if h : HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down) then
        ∏
          i ∈
            Finite.toFinset (s := 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)
  μ
Tactic: rw [tprod_def, finprod_def']
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
X : Type u_6
E : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableMul₂ E
L : SummationFilter ι
inst_7 : L.NeBot
inst_8 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
⊢ AEMeasurable.{u_6, u_7} (β := E)
    (if h : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L then
      if L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite then
        if h : HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down) then
          ∏
            i ∈
              Finite.toFinset (s := 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 ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite →
    ∀ (h : HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)),
      AEMeasurable.{u_6, u_7} (β := E)
        (∏
          i ∈
            Finite.toFinset (s := mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)) h,
          L.support.mulIndicator (fun (i : ι) ↦ f i) i.down)
        μ
Tactic: split_ifs with hm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
X : Type u_6
E : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableMul₂ E
L : SummationFilter ι
inst_7 : L.NeBot
inst_8 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
pos :
  ∀ (hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L),
    L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite →
      ∀ (h : HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)),
        AEMeasurable.{u_6, u_7} (β := E)
          (∏
            i ∈
              Finite.toFinset (s := mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down))
                h,
            L.support.mulIndicator (fun (i : ι) ↦ f i) i.down)
          μ
⊢ AEMeasurable.{u_6, u_7} (β := E)
    (if h : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L then
      if L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite then
        if h : HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down) then
          ∏
            i ∈
              Finite.toFinset (s := 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 ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite →
    ¬HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down) →
      AEMeasurable.{u_6, u_7} (β := E) 1 μ
Tactic: split_ifs with hm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
X : Type u_6
E : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableMul₂ E
L : SummationFilter ι
inst_7 : L.NeBot
inst_8 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
pos :
  ∀ (hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L),
    L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite →
      ∀ (h : HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)),
        AEMeasurable.{u_6, u_7} (β := E)
          (∏
            i ∈
              Finite.toFinset (s := 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 ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite →
      ¬HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down) →
        AEMeasurable.{u_6, u_7} (β := E) 1 μ
⊢ AEMeasurable.{u_6, u_7} (β := E)
    (if h : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L then
      if L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite then
        if h : HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down) then
          ∏
            i ∈
              Finite.toFinset (s := 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 ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite) →
    HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L → AEMeasurable.{u_6, u_7} (β := E) 1 μ
Tactic: split_ifs with hm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
X : Type u_6
E : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableMul₂ E
L : SummationFilter ι
inst_7 : L.NeBot
inst_8 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
pos :
  ∀ (hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L),
    L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite →
      ∀ (h : HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)),
        AEMeasurable.{u_6, u_7} (β := E)
          (∏
            i ∈
              Finite.toFinset (s := 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 ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite →
      ¬HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down) →
        AEMeasurable.{u_6, u_7} (β := E) 1 μ
pos₁ :
  ∀ (hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L),
    ¬(L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite) →
      HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L → AEMeasurable.{u_6, u_7} (β := E) 1 μ
⊢ AEMeasurable.{u_6, u_7} (β := E)
    (if h : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L then
      if L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite then
        if h : HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down) then
          ∏
            i ∈
              Finite.toFinset (s := 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 ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite) →
    ¬HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L →
      AEMeasurable (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.Basic (goal)
Goal:
X : Type u_6
E : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableMul₂ E
L : SummationFilter ι
inst_7 : L.NeBot
inst_8 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
pos :
  ∀ (hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L),
    L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite →
      ∀ (h : HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)),
        AEMeasurable.{u_6, u_7} (β := E)
          (∏
            i ∈
              Finite.toFinset (s := 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 ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite →
      ¬HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down) →
        AEMeasurable.{u_6, u_7} (β := E) 1 μ
pos₁ :
  ∀ (hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L),
    ¬(L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite) →
      HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L → AEMeasurable.{u_6, u_7} (β := E) 1 μ
neg₁ :
  ∀ (hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L),
    ¬(L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite) →
      ¬HasProd (α := X → E) (fun (i : ι) ↦ f i) 1 L →
        AEMeasurable (Exists.choose (p := fun (a : X → E) ↦ HasProd (fun (i : ι) ↦ f i) a L) hm) μ
⊢ AEMeasurable.{u_6, u_7} (β := E)
    (if h : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L then
      if L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite then
        if h : HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down) then
          ∏
            i ∈
              Finite.toFinset (s := 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), AEMeasurable.{u_6, u_7} (β := E) 1 μ
Tactic: split_ifs with hm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
X : Type u_6
E : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableMul₂ E
L : SummationFilter ι
inst_7 : L.NeBot
inst_8 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite
h_2 : HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)
⊢ AEMeasurable.{u_6, u_7} (β := E)
    (∏ i ∈ Finite.toFinset (s := 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 := mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)) h_2,
  AEMeasurable.{u_6, u_7} (β := E) (L.support.mulIndicator (fun (i : ι) ↦ f i) x.down) μ
Tactic: refine Finset.aemeasurable_prod _ (fun _ _ ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
X : Type u_6
E : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableMul₂ E
L : SummationFilter ι
inst_7 : L.NeBot
inst_8 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite
h_2 : HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)
x : PLift ι
h_3 : x ∈ Finite.toFinset (s := mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)) h_2
⊢ AEMeasurable.{u_6, u_7} (β := E) (L.support.mulIndicator (fun (i : ι) ↦ f i) x.down) μ
have pos : AEMeasurable (if x.down ∈ L.support then f x.down else 1) μ
Tactic: rw [Set.mulIndicator]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
X : Type u_6
E : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableMul₂ E
L : SummationFilter ι
inst_7 : L.NeBot
inst_8 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite
h_2 : HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)
x : PLift ι
h_3 : x ∈ Finite.toFinset (s := mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)) h_2
⊢ AEMeasurable (if x.down ∈ L.support then f x.down else 1) μ
have pos : x.down ∈ L.support → AEMeasurable (f x.down) μ
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
X : Type u_6
E : Type u_7
ι : Type u_8
inst : MeasurableSpace X
inst_1 : CommMonoid E
inst_2 : TopologicalSpace E
inst_3 : PseudoMetrizableSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableMul₂ E
L : SummationFilter ι
inst_7 : L.NeBot
inst_8 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : Multipliable (α := X → E) (fun (i : ι) ↦ f i) L
h_1 : L.HasSupport ∧ ((mulSupport (M := X → E) fun (i : ι) ↦ f i) ∩ L.support).Finite
h_2 : HasFiniteMulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)
x : PLift ι
h_3 : x ∈ Finite.toFinset (s := mulSupport (M := X → E) ((L.support.mulIndicator fun (i : ι) ↦ f i) ∘ PLift.down)) h_2
pos : x.down ∈ L.support → AEMeasurable (f x.down) μ
⊢ AEMeasurable (if x.down ∈ L.support then f x.down else 1) μ
have neg : x.down ∉ L.support → AEMeasurable.{u_6, u_7} (β := E) 1 μ
Tactic: split_ifs