awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst_4 : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
e : E := Classical.choice hE
conv : Set X := {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
mconv : MeasurableSet conv
hconv : StronglyMeasurable.{u_2, u_3} (β := E) fun (x : (↑conv : Type u_2)) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)
x : X
hx : x ∈ conv
pos pos₁ :
  Eq.{u_3 + 1} (α := E) (l.limUnder fun (x_1 : ι) ↦ f x_1 x)
    (l.limUnder fun (x_1 : ι) ↦ f x_1 (↑(Subtype.mk (p := fun (x : X) ↦ x ∈ conv) x hx) : X))
⊢ Eq.{u_3 + 1} (α := E) (l.limUnder fun (x_1 : ι) ↦ f x_1 x)
    (Function.extend (Subtype.val (p := fun (x : X) ↦ x ∈ conv))
      (fun (x : { x : X // x ∈ conv }) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)) (fun (x : X) ↦ e) x)

Tactic:
rw [Function.extend_val_apply hx]

Premises used: Function.extend_val_apply
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst_4 : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
e : E := Classical.choice hE
conv : Set X := {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
mconv : MeasurableSet conv
hconv : StronglyMeasurable.{u_2, u_3} (β := E) fun (x : (↑conv : Type u_2)) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)
x : X
hx : x ∉ conv
neg : (l.limUnder fun (x_1 : ι) ↦ f x_1 x) = e
neg₁ neg₂ : Classical.choice hE = e
⊢ Eq.{u_3 + 1} (α := E) (l.limUnder fun (x_1 : ι) ↦ f x_1 x)
    (Function.extend (Subtype.val (p := fun (x : X) ↦ x ∈ conv))
      (fun (x : { x : X // x ∈ conv }) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)) (fun (x : X) ↦ e) x)

Tactic:
rw [Function.extend_val_apply' hx, limUnder_of_not_tendsto hx]

Premises used: Function.extend_val_apply', limUnder_of_not_tendsto
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst_4 : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
e : E := Classical.choice hE
conv : Set X := {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
mconv : MeasurableSet conv
hconv : StronglyMeasurable.{u_2, u_3} (β := E) fun (x : (↑conv : Type u_2)) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)
⊢ Eq (α := (x : X) → E) (fun (x : X) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 x)
    (Function.extend (Subtype.val (p := fun (x : X) ↦ x ∈ conv))
      (fun (x : { x : X // x ∈ conv }) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)) fun (x : X) ↦ e)

Tactic:
have : (fun x ↦ limUnder l (f · x)) = ((↑) : conv → X).extend
      (fun x ↦ limUnder l (f · x)) (fun _ ↦ e) := by
    ext x
    by_cases hx : x ∈ conv
    · rw [Function.extend_val_apply hx]
    · rw [Function.extend_val_apply' hx, limUnder_of_not_tendsto hx]
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst_4 : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
e : E := Classical.choice hE
conv : Set X := {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
mconv : MeasurableSet conv
hconv : StronglyMeasurable.{u_2, u_3} (β := E) fun (x : (↑conv : Type u_2)) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)
this :
  Eq (α := (x : X) → E) (fun (x : X) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 x)
    (Function.extend (Subtype.val (p := fun (x : X) ↦ x ∈ conv))
      (fun (x : { x : X // x ∈ conv }) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)) fun (x : X) ↦ e)
inr :
  StronglyMeasurable.{u_2, u_3} (α := X) (β := E)
    (Function.extend (Subtype.val (p := fun (x : X) ↦ x ∈ conv))
      (fun (x : { x : X // x ∈ conv }) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)) fun (x : X) ↦ e)
⊢ StronglyMeasurable.{u_2, u_3} (β := E) fun (x : X) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 x

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst_4 : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
e : E := Classical.choice hE
conv : Set X := {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
mconv : MeasurableSet conv
hconv : StronglyMeasurable.{u_2, u_3} (β := E) fun (x : (↑conv : Type u_2)) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)
this :
  Eq (α := (x : X) → E) (fun (x : X) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 x)
    (Function.extend (Subtype.val (p := fun (x : X) ↦ x ∈ conv))
      (fun (x : { x : X // x ∈ conv }) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)) fun (x : X) ↦ e)
⊢ StronglyMeasurable.{u_2, u_3} (α := X) (β := E)
    (Function.extend (Subtype.val (p := fun (x : X) ↦ x ∈ conv))
      (fun (x : { x : X // x ∈ conv }) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)) fun (x : X) ↦ e)

Tactic:
(MeasurableEmbedding.subtype_coe mconv).stronglyMeasurable_extend hconv
    stronglyMeasurable_const

Premises used: MeasureTheory.stronglyMeasurable_const, MeasurableEmbedding.stronglyMeasurable_extend, MeasurableEmbedding.subtype_coe
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst_4 : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
e : E := Classical.choice hE
conv : Set X := {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
mconv : MeasurableSet conv
hconv : StronglyMeasurable.{u_2, u_3} (β := E) fun (x : (↑conv : Type u_2)) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)
this :
  Eq (α := (x : X) → E) (fun (x : X) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 x)
    (Function.extend (Subtype.val (p := fun (x : X) ↦ x ∈ conv))
      (fun (x : { x : X // x ∈ conv }) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)) fun (x : X) ↦ e)
⊢ StronglyMeasurable.{u_2, u_3} (α := X) (β := E)
    (Function.extend (Subtype.val (p := fun (x : X) ↦ x ∈ conv))
      (fun (x : { x : X // x ∈ conv }) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)) fun (x : X) ↦ e)

Tactic:
exact (MeasurableEmbedding.subtype_coe mconv).stronglyMeasurable_extend hconv
    stronglyMeasurable_const

Premises used: MeasureTheory.stronglyMeasurable_const, MeasurableEmbedding.stronglyMeasurable_extend, MeasurableEmbedding.subtype_coe
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E_1 : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E_1
inst_2 : TopologicalSpace E_1
inst_3 : IsCompletelyPseudoMetrizableSpace E_1
inst_4 : ContinuousMul E_1
inst_5 : Countable ι
L : SummationFilter ι
inst_6 : L.NeBot
inst_7 : L.filter.IsCountablyGenerated
f : ι → X → E_1
h : ∀ (i : ι), StronglyMeasurable (f i)
E : Set X := {x : X | Multipliable.{u_5, u_6} (α := E_1) (fun (x_1 : ι) ↦ f x_1 x) L}
⊢ ∀ (i : Finset ι), StronglyMeasurable.{u_4, u_5} (β := E_1) fun (x : X) ↦ ∏ b ∈ i, (fun (x_1 : ι) ↦ f x_1 x) b

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E_1 : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E_1
inst_2 : TopologicalSpace E_1
inst_3 : IsCompletelyPseudoMetrizableSpace E_1
inst_4 : ContinuousMul E_1
inst_5 : Countable ι
L : SummationFilter ι
inst_6 : L.NeBot
inst_7 : L.filter.IsCountablyGenerated
f : ι → X → E_1
h : ∀ (i : ι), StronglyMeasurable (f i)
E : Set X := {x : X | Multipliable.{u_5, u_6} (α := E_1) (fun (x_1 : ι) ↦ f x_1 x) L}
⊢ MeasurableSet E

Tactic:
have hE : MeasurableSet E := StronglyMeasurable.measurableSet_exists_tendsto (by fun_prop)
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E_1 : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E_1
inst_2 : TopologicalSpace E_1
inst_3 : IsCompletelyPseudoMetrizableSpace E_1
inst_4 : ContinuousMul E_1
inst_5 : Countable ι
L : SummationFilter ι
inst_6 : L.NeBot
inst_7 : L.filter.IsCountablyGenerated
f : ι → X → E_1
h : ∀ (i : ι), StronglyMeasurable (f i)
E : Set X := {x : X | Multipliable.{u_5, u_6} (α := E_1) (fun (x_1 : ι) ↦ f x_1 x) L}
hE : MeasurableSet E
⊢ Eq (α := (a : (↑Eᶜ : Type u_4)) → E_1)
    (Eᶜ.restrict (π := fun (x : X) ↦ E_1) fun (x : X) ↦ ∏'[L] (i : ι), f i x : (a : (↑Eᶜ : Type u_4)) → E_1)
    fun (x : (↑Eᶜ : Type u_4)) ↦ (1 : E_1)

Tactic:
have h0 : (Eᶜ.restrict fun x => ∏'[L] i, f i x) = fun _ => 1 :=
    funext fun ⟨x, hx⟩ => tprod_eq_one_of_not_multipliable hx
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E_1 : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E_1
inst_2 : TopologicalSpace E_1
inst_3 : IsCompletelyPseudoMetrizableSpace E_1
inst_4 : ContinuousMul E_1
inst_5 : Countable ι
L : SummationFilter ι
inst_6 : L.NeBot
inst_7 : L.filter.IsCountablyGenerated
f : ι → X → E_1
h : ∀ (i : ι), StronglyMeasurable (f i)
E : Set X := {x : X | Multipliable.{u_5, u_6} (α := E_1) (fun (x_1 : ι) ↦ f x_1 x) L}
hE : MeasurableSet E
h0 :
  Eq (α := (a : (↑Eᶜ : Type u_4)) → E_1)
    (Eᶜ.restrict (π := fun (x : X) ↦ E_1) fun (x : X) ↦ ∏'[L] (i : ι), f i x : (a : (↑Eᶜ : Type u_4)) → E_1)
    fun (x : (↑Eᶜ : Type u_4)) ↦ (1 : E_1)
⊢ StronglyMeasurable.{u_4, u_5} (β := E_1) fun (x : X) ↦ ∏'[L] (i : ι), f i x

Tactic:
stronglyMeasurable_of_restrict_of_restrict_compl hE ?_ (h0 ▸ stronglyMeasurable_const)

Premises used: MeasureTheory.stronglyMeasurable_const, stronglyMeasurable_of_restrict_of_restrict_compl, Eq.rec, Eq.symm
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E_1 : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E_1
inst_2 : TopologicalSpace E_1
inst_3 : IsCompletelyPseudoMetrizableSpace E_1
inst_4 : ContinuousMul E_1
inst_5 : Countable ι
L : SummationFilter ι
inst_6 : L.NeBot
inst_7 : L.filter.IsCountablyGenerated
f : ι → X → E_1
h : ∀ (i : ι), StronglyMeasurable (f i)
E : Set X := {x : X | Multipliable.{u_5, u_6} (α := E_1) (fun (x_1 : ι) ↦ f x_1 x) L}
hE : MeasurableSet E
h0 :
  Eq (α := (a : (↑Eᶜ : Type u_4)) → E_1)
    (Eᶜ.restrict (π := fun (x : X) ↦ E_1) fun (x : X) ↦ ∏'[L] (i : ι), f i x : (a : (↑Eᶜ : Type u_4)) → E_1)
    fun (x : (↑Eᶜ : Type u_4)) ↦ (1 : E_1)
refine :
  StronglyMeasurable.{u_4, u_5} (α := (↑E : Type u_4)) (β := E_1)
    (E.restrict (π := fun (a : X) ↦ E_1) fun (x : X) ↦ ∏'[L] (i : ι), f i x)
⊢ StronglyMeasurable.{u_4, u_5} (β := E_1) fun (x : X) ↦ ∏'[L] (i : ι), f i x

Tactic:
refine stronglyMeasurable_of_restrict_of_restrict_compl hE ?_ (h0 ▸ stronglyMeasurable_const)

Premises used: stronglyMeasurable_of_restrict_of_restrict_compl
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E_1 : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E_1
inst_2 : TopologicalSpace E_1
inst_3 : IsCompletelyPseudoMetrizableSpace E_1
inst_4 : ContinuousMul E_1
inst_5 : Countable ι
L : SummationFilter ι
inst_6 : L.NeBot
inst_7 : L.filter.IsCountablyGenerated
f : ι → X → E_1
h : ∀ (i : ι), StronglyMeasurable (f i)
E : Set X := {x : X | Multipliable.{u_5, u_6} (α := E_1) (fun (x_1 : ι) ↦ f x_1 x) L}
hE : MeasurableSet E
h0 :
  Eq (α := (a : (↑Eᶜ : Type u_4)) → E_1)
    (Eᶜ.restrict (π := fun (x : X) ↦ E_1) fun (x : X) ↦ ∏'[L] (i : ι), f i x : (a : (↑Eᶜ : Type u_4)) → E_1)
    fun (x : (↑Eᶜ : Type u_4)) ↦ (1 : E_1)
⊢ StronglyMeasurable.{u_4, u_5} (α := (↑E : Type u_4)) (β := E_1)
    (E.restrict (π := fun (a : X) ↦ E_1) fun (x : X) ↦ ∏'[L] (i : ι), f i x)

Tactic:
stronglyMeasurable_of_tendsto L.filter ?_ (tendsto_pi_nhds.mpr fun e => e.2.hasProd)

Premises used: Iff.mpr, stronglyMeasurable_of_tendsto, tendsto_pi_nhds, Multipliable.hasProd, SummationFilter.filter, Subtype.property
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E_1 : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E_1
inst_2 : TopologicalSpace E_1
inst_3 : IsCompletelyPseudoMetrizableSpace E_1
inst_4 : ContinuousMul E_1
inst_5 : Countable ι
L : SummationFilter ι
inst_6 : L.NeBot
inst_7 : L.filter.IsCountablyGenerated
f : ι → X → E_1
h : ∀ (i : ι), StronglyMeasurable (f i)
E : Set X := {x : X | Multipliable.{u_5, u_6} (α := E_1) (fun (x_1 : ι) ↦ f x_1 x) L}
hE : MeasurableSet E
h0 :
  Eq (α := (a : (↑Eᶜ : Type u_4)) → E_1)
    (Eᶜ.restrict (π := fun (x : X) ↦ E_1) fun (x : X) ↦ ∏'[L] (i : ι), f i x : (a : (↑Eᶜ : Type u_4)) → E_1)
    fun (x : (↑Eᶜ : Type u_4)) ↦ (1 : E_1)
refine :
  ∀ (i : Finset ι),
    StronglyMeasurable.{u_4, u_5} (β := E_1) fun (e : (↑E : Type u_4)) ↦ ∏ b ∈ i, (fun (x : ι) ↦ f x (↑e : X)) b
⊢ StronglyMeasurable.{u_4, u_5} (α := (↑E : Type u_4)) (β := E_1)
    (E.restrict (π := fun (a : X) ↦ E_1) fun (x : X) ↦ ∏'[L] (i : ι), f i x)

Tactic:
refine stronglyMeasurable_of_tendsto L.filter ?_ (tendsto_pi_nhds.mpr fun e => e.2.hasProd)

Premises used: Iff.mpr, stronglyMeasurable_of_tendsto, tendsto_pi_nhds, SummationFilter.filter
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
X : Type u_4
E_1 : Type u_5
ι : Type u_6
inst : MeasurableSpace X
inst_1 : CommMonoid E_1
inst_2 : TopologicalSpace E_1
inst_3 : IsCompletelyPseudoMetrizableSpace E_1
inst_4 : ContinuousMul E_1
inst_5 : Countable ι
L : SummationFilter ι
inst_6 : L.NeBot
inst_7 : L.filter.IsCountablyGenerated
f : ι → X → E_1
h : ∀ (i : ι), StronglyMeasurable (f i)
E : Set X := {x : X | Multipliable.{u_5, u_6} (α := E_1) (fun (x_1 : ι) ↦ f x_1 x) L}
hE : MeasurableSet E
h0 :
  Eq (α := (a : (↑Eᶜ : Type u_4)) → E_1)
    (Eᶜ.restrict (π := fun (x : X) ↦ E_1) fun (x : X) ↦ ∏'[L] (i : ι), f i x : (a : (↑Eᶜ : Type u_4)) → E_1)
    fun (x : (↑Eᶜ : Type u_4)) ↦ (1 : E_1)
⊢ ∀ (i : Finset ι),
    StronglyMeasurable.{u_4, u_5} (β := E_1) fun (e : (↑E : Type u_4)) ↦ ∏ b ∈ i, (fun (x : ι) ↦ f x (↑e : X)) b

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 : IsCompletelyPseudoMetrizableSpace E
inst_4 : ContinuousMul E
inst_5 : Countable ι
L : SummationFilter ι
inst_6 : L.NeBot
inst_7 : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
choose :
  ∀ (g : (i : ι) → X → E) (hg_meas : ∀ (i : ι), StronglyMeasurable (g i)) (hg_eq_f : ∀ (i : ι), f i =ᶠ[ae μ] g i),
    AEStronglyMeasurable.{u_4, u_5} (β := E) (fun (x : X) ↦ ∏'[L] (i : ι), f i x) μ
⊢ AEStronglyMeasurable.{u_4, u_5} (β := E) (fun (x : X) ↦ ∏'[L] (i : ι), f i x) μ

Tactic:
choose g hg_meas hg_eq_f using h
-- 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 : IsCompletelyPseudoMetrizableSpace E
inst_4 : ContinuousMul E
inst_5 : Countable ι
L : SummationFilter ι
inst_6 : L.NeBot
inst_7 : L.filter.IsCountablyGenerated
μ : Measure X
f g : (i : ι) → X → E
hg_meas : ∀ (i : ι), StronglyMeasurable (g i)
hg_eq_f : ∀ (i : ι), f i =ᶠ[ae μ] g i
right : EventuallyEq.{u_4, u_5} (β := E) (ae μ) (fun (x : X) ↦ ∏'[L] (i : ι), f i x) fun (x : X) ↦ ∏'[L] (i : ι), g i x
⊢ AEStronglyMeasurable.{u_4, u_5} (β := E) (fun (x : X) ↦ ∏'[L] (i : ι), f i x) μ

Tactic:
use (fun x => ∏'[L] i, g i x), StronglyMeasurable.tprod hg_meas

Premises used: tprod, MeasureTheory.StronglyMeasurable.tprod
-- 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 : IsCompletelyPseudoMetrizableSpace E
inst_4 : ContinuousMul E
inst_5 : Countable ι
L : SummationFilter ι
inst_6 : L.NeBot
inst_7 : L.filter.IsCountablyGenerated
μ : Measure X
f g : (i : ι) → X → E
hg_meas : ∀ (i : ι), StronglyMeasurable (g i)
hg_eq_f : ∀ (i : ι), f i =ᶠ[ae μ] g i
x : X
h_eq : ∀ (i : ι), f i x = g i x
⊢ Eq.{u_5 + 1} (α := E) (∏'[L] (i : ι), f i x) (∏'[L] (i : ι), g i x)

Tactic:
tprod_congr h_eq

Premises used: tprod_congr
-- 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 : IsCompletelyPseudoMetrizableSpace E
inst_4 : ContinuousMul E
inst_5 : Countable ι
L : SummationFilter ι
inst_6 : L.NeBot
inst_7 : L.filter.IsCountablyGenerated
μ : Measure X
f g : (i : ι) → X → E
hg_meas : ∀ (i : ι), StronglyMeasurable (g i)
hg_eq_f : ∀ (i : ι), f i =ᶠ[ae μ] g i
h :
  ∀ (a : X),
    Membership.mem (γ := Set X)
      {x : X |
        Membership.mem (γ := Set X) {x : X | (fun (a : X) ↦ ∀ (i : ι), f i a = g i a) x} x →
          Membership.mem (γ := Set X)
            {x : X |
              (fun (x : X) ↦
                  Eq.{u_5 + 1} (α := E) ((fun (x : X) ↦ (∏'[L] (i : ι), f i x : E)) x)
                    ((fun (x : X) ↦ (∏'[L] (i : ι), g i x : E)) x))
                x}
            x}
      a
h₁ h₂ : ∀ (x : X) (h_eq : ∀ (i : ι), f i x = g i x), Eq.{u_5 + 1} (α := E) (∏'[L] (i : ι), f i x) (∏'[L] (i : ι), g i x)
⊢ EventuallyEq.{u_4, u_5} (β := E) (ae μ) (fun (x : X) ↦ ∏'[L] (i : ι), f i x) fun (x : X) ↦ ∏'[L] (i : ι), g i x

Tactic:
filter_upwards [ae_all_iff.mpr hg_eq_f] with x h_eq using tprod_congr h_eq

Premises used: Iff.mpr, MeasureTheory.ae_all_iff
-- 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
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (f i)
rw :
  StronglyMeasurable.{u_4, u_5} (α := X) (β := 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)
⊢ StronglyMeasurable.{u_4, u_5} (α := X) (β := E) (∏'[L] (i : ι), f i)

Tactic:
rw [tprod_def, finprod_def']

Premises used: finprod_def', tprod_def
-- 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
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (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)),
        StronglyMeasurable.{u_4, u_5} (α := X) (β := 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) →
        StronglyMeasurable.{u_4, u_5} (α := X) (β := 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 → StronglyMeasurable.{u_4, u_5} (α := X) (β := 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 →
        StronglyMeasurable (Exists.choose (p := fun (a : X → E) ↦ HasProd (fun (i : ι) ↦ f i) a L) hm)
neg₂ : ∀ (hm : ¬Multipliable (α := X → E) (fun (i : ι) ↦ f i) L), StronglyMeasurable.{u_4, u_5} (α := X) (β := E) 1
⊢ StronglyMeasurable.{u_4, u_5} (α := X) (β := 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)

Tactic:
split_ifs with hm
-- 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
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (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)
⊢ StronglyMeasurable.{u_4, u_5} (α := X) (β := 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:
stronglyMeasurable_one

Premises used: MeasureTheory.stronglyMeasurable_one
-- 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
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (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)
⊢ StronglyMeasurable.{u_4, u_5} (α := X) (β := E) 1

Tactic:
stronglyMeasurable_one

Premises used: MeasureTheory.stronglyMeasurable_one