-- Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean
theorem _root_.List.aestronglyMeasurable_prod' (l : List (α → M))
    (hl : ∀ f ∈ l, AEStronglyMeasurable f μ) : AEStronglyMeasurable l.prod μ

Proof state:
case cons
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
f : α → M
l : List (α → M)
ihl : (∀ f ∈ l, AEStronglyMeasurable f μ) → AEStronglyMeasurable l.prod μ
hl : ∀ f_1 ∈ f :: l, AEStronglyMeasurable f_1 μ
⊢ AEStronglyMeasurable (f :: l).prod μ

Tactic:
rw [List.forall_mem_cons] at hl

Result:
case cons
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
f : α → M
l : List (α → M)
ihl : (∀ f ∈ l, AEStronglyMeasurable f μ) → AEStronglyMeasurable l.prod μ
hl : AEStronglyMeasurable f μ ∧ ∀ x ∈ l, AEStronglyMeasurable x μ
⊢ AEStronglyMeasurable (f :: l).prod μ

Proof state:
case cons
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
f : α → M
l : List (α → M)
ihl : (∀ f ∈ l, AEStronglyMeasurable f μ) → AEStronglyMeasurable l.prod μ
hl : AEStronglyMeasurable f μ ∧ ∀ x ∈ l, AEStronglyMeasurable x μ
⊢ AEStronglyMeasurable (f * l.prod) μ

Tactic:
exact hl.1.mul (ihl hl.2)

Result:
no goals

Proof state:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
l : List (α → M)
hl : ∀ f ∈ l, AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable l.prod μ

Tactic:
induction' l with f l ihl

Result:
case nil
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
hl : ∀ f ∈ [], AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable [].prod μ

case cons
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
f : α → M
l : List (α → M)
ihl : (∀ f ∈ l, AEStronglyMeasurable f μ) → AEStronglyMeasurable l.prod μ
hl : ∀ f_1 ∈ f :: l, AEStronglyMeasurable f_1 μ
⊢ AEStronglyMeasurable (f :: l).prod μ

Proof state:
case cons
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
f : α → M
l : List (α → M)
ihl : (∀ f ∈ l, AEStronglyMeasurable f μ) → AEStronglyMeasurable l.prod μ
hl : AEStronglyMeasurable f μ ∧ ∀ x ∈ l, AEStronglyMeasurable x μ
⊢ AEStronglyMeasurable (f :: l).prod μ

Tactic:
rw [List.prod_cons]

Result:
case cons
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
f : α → M
l : List (α → M)
ihl : (∀ f ∈ l, AEStronglyMeasurable f μ) → AEStronglyMeasurable l.prod μ
hl : AEStronglyMeasurable f μ ∧ ∀ x ∈ l, AEStronglyMeasurable x μ
⊢ AEStronglyMeasurable (f * l.prod) μ

Proof state:
case nil
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
hl : ∀ f ∈ [], AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable [].prod μ

Tactic:
exact aestronglyMeasurable_one

Result:
no goals