-- Mathlib/MeasureTheory/Constructions/Pi.lean
lemma pi_map_piOptionEquivProd {β : Option ι → Type*} [∀ i, MeasurableSpace (β i)]
    (μ : (i : Option ι) → Measure (β i)) [∀ (i : Option ι), SigmaFinite (μ i)] :
    ((Measure.pi fun i ↦ μ (some i)).prod (μ none)).map
      (MeasurableEquiv.piOptionEquivProd β).symm = Measure.pi μ

Proof state:
case h
ι : Type u_1
inst✝² : Fintype ι
β : Option ι → Type u_4
inst✝¹ : (i : Option ι) → MeasurableSpace (β i)
μ : (i : Option ι) → Measure (β i)
inst✝ : ∀ (i : Option ι), SigmaFinite (μ i)
s : (i : Option ι) → Set (β i)
x✝ : ∀ (i : Option ι), MeasurableSet (s i)
e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) := (MeasurableEquiv.piOptionEquivProd β).symm
me : MeasurableEmbedding ⇑e_meas
x : ((i : ι) → β (some i)) × β none
⊢ (∀ (i : Option ι), e_meas x i ∈ s i) ↔ (∀ (i : ι), x.1 i ∈ s (some i)) ∧ x.2 ∈ s none

Tactic:
refine ⟨by tauto, fun _ i ↦ ?_⟩

Result:
case h
ι : Type u_1
inst✝² : Fintype ι
β : Option ι → Type u_4
inst✝¹ : (i : Option ι) → MeasurableSpace (β i)
μ : (i : Option ι) → Measure (β i)
inst✝ : ∀ (i : Option ι), SigmaFinite (μ i)
s : (i : Option ι) → Set (β i)
x✝¹ : ∀ (i : Option ι), MeasurableSet (s i)
e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) := (MeasurableEquiv.piOptionEquivProd β).symm
me : MeasurableEmbedding ⇑e_meas
x : ((i : ι) → β (some i)) × β none
x✝ : (∀ (i : ι), x.1 i ∈ s (some i)) ∧ x.2 ∈ s none
i : Option ι
⊢ e_meas x i ∈ s i

Proof state:
ι : Type u_1
inst✝² : Fintype ι
β : Option ι → Type u_4
inst✝¹ : (i : Option ι) → MeasurableSpace (β i)
μ : (i : Option ι) → Measure (β i)
inst✝ : ∀ (i : Option ι), SigmaFinite (μ i)
s : (i : Option ι) → Set (β i)
x✝ : ∀ (i : Option ι), MeasurableSet (s i)
e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) := (MeasurableEquiv.piOptionEquivProd β).symm
me : MeasurableEmbedding ⇑e_meas
this : ⇑e_meas ⁻¹' univ.pi s = (univ.pi fun i => s (some i)) ×ˢ s none
⊢ (map (⇑(MeasurableEquiv.piOptionEquivProd β).symm) ((Measure.pi fun i => μ (some i)).prod (μ none))) (univ.pi s) =
    ∏ i : Option ι, (μ i) (s i)

Tactic:
simp only [e_meas, me.map_apply, univ_option, le_eq_subset, Finset.prod_insertNone, this,
  prod_prod, pi_pi, mul_comm]

Result:
no goals

Proof state:
ι : Type u_1
inst✝² : Fintype ι
β : Option ι → Type u_4
inst✝¹ : (i : Option ι) → MeasurableSpace (β i)
μ : (i : Option ι) → Measure (β i)
inst✝ : ∀ (i : Option ι), SigmaFinite (μ i)
s : (i : Option ι) → Set (β i)
x✝ : ∀ (i : Option ι), MeasurableSet (s i)
e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) := (MeasurableEquiv.piOptionEquivProd β).symm
me : MeasurableEmbedding ⇑e_meas
x : ((i : ι) → β (some i)) × β none
⊢ (∀ (i : Option ι), e_meas x i ∈ s i) → (∀ (i : ι), x.1 i ∈ s (some i)) ∧ x.2 ∈ s none

Tactic:
tauto

Result:
no goals

Proof state:
ι : Type u_1
inst✝² : Fintype ι
β : Option ι → Type u_4
inst✝¹ : (i : Option ι) → MeasurableSpace (β i)
μ : (i : Option ι) → Measure (β i)
inst✝ : ∀ (i : Option ι), SigmaFinite (μ i)
s : (i : Option ι) → Set (β i)
x✝ : ∀ (i : Option ι), MeasurableSet (s i)
e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) := (MeasurableEquiv.piOptionEquivProd β).symm
⊢ (map (⇑(MeasurableEquiv.piOptionEquivProd β).symm) ((Measure.pi fun i => μ (some i)).prod (μ none))) (univ.pi s) =
    ∏ i : Option ι, (μ i) (s i)

Tactic:
have me := MeasurableEquiv.measurableEmbedding e_meas

Result:
ι : Type u_1
inst✝² : Fintype ι
β : Option ι → Type u_4
inst✝¹ : (i : Option ι) → MeasurableSpace (β i)
μ : (i : Option ι) → Measure (β i)
inst✝ : ∀ (i : Option ι), SigmaFinite (μ i)
s : (i : Option ι) → Set (β i)
x✝ : ∀ (i : Option ι), MeasurableSet (s i)
e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) := (MeasurableEquiv.piOptionEquivProd β).symm
me : MeasurableEmbedding ⇑e_meas
⊢ (map (⇑(MeasurableEquiv.piOptionEquivProd β).symm) ((Measure.pi fun i => μ (some i)).prod (μ none))) (univ.pi s) =
    ∏ i : Option ι, (μ i) (s i)

Proof state:
ι : Type u_1
inst✝² : Fintype ι
β : Option ι → Type u_4
inst✝¹ : (i : Option ι) → MeasurableSpace (β i)
μ : (i : Option ι) → Measure (β i)
inst✝ : ∀ (i : Option ι), SigmaFinite (μ i)
s : (i : Option ι) → Set (β i)
x✝ : ∀ (i : Option ι), MeasurableSet (s i)
e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) := (MeasurableEquiv.piOptionEquivProd β).symm
me : MeasurableEmbedding ⇑e_meas
⊢ ⇑e_meas ⁻¹' univ.pi s = (univ.pi fun i => s (some i)) ×ˢ s none

Tactic:
ext x

Result:
case h
ι : Type u_1
inst✝² : Fintype ι
β : Option ι → Type u_4
inst✝¹ : (i : Option ι) → MeasurableSpace (β i)
μ : (i : Option ι) → Measure (β i)
inst✝ : ∀ (i : Option ι), SigmaFinite (μ i)
s : (i : Option ι) → Set (β i)
x✝ : ∀ (i : Option ι), MeasurableSet (s i)
e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) := (MeasurableEquiv.piOptionEquivProd β).symm
me : MeasurableEmbedding ⇑e_meas
x : ((i : ι) → β (some i)) × β none
⊢ x ∈ ⇑e_meas ⁻¹' univ.pi s ↔ x ∈ (univ.pi fun i => s (some i)) ×ˢ s none

Proof state:
ι : Type u_1
inst✝² : Fintype ι
β : Option ι → Type u_4
inst✝¹ : (i : Option ι) → MeasurableSpace (β i)
μ : (i : Option ι) → Measure (β i)
inst✝ : ∀ (i : Option ι), SigmaFinite (μ i)
⊢ map (⇑(MeasurableEquiv.piOptionEquivProd β).symm) ((Measure.pi fun i => μ (some i)).prod (μ none)) = Measure.pi μ

Tactic:
refine pi_eq (fun s _ ↦ ?_) |>.symm

Result:
ι : Type u_1
inst✝² : Fintype ι
β : Option ι → Type u_4
inst✝¹ : (i : Option ι) → MeasurableSpace (β i)
μ : (i : Option ι) → Measure (β i)
inst✝ : ∀ (i : Option ι), SigmaFinite (μ i)
s : (i : Option ι) → Set (β i)
x✝ : ∀ (i : Option ι), MeasurableSet (s i)
⊢ (map (⇑(MeasurableEquiv.piOptionEquivProd β).symm) ((Measure.pi fun i => μ (some i)).prod (μ none))) (univ.pi s) =
    ∏ i : Option ι, (μ i) (s i)

Proof state:
ι : Type u_1
inst✝² : Fintype ι
β : Option ι → Type u_4
inst✝¹ : (i : Option ι) → MeasurableSpace (β i)
μ : (i : Option ι) → Measure (β i)
inst✝ : ∀ (i : Option ι), SigmaFinite (μ i)
s : (i : Option ι) → Set (β i)
x✝ : ∀ (i : Option ι), MeasurableSet (s i)
e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) := (MeasurableEquiv.piOptionEquivProd β).symm
me : MeasurableEmbedding ⇑e_meas
⊢ (map (⇑(MeasurableEquiv.piOptionEquivProd β).symm) ((Measure.pi fun i => μ (some i)).prod (μ none))) (univ.pi s) =
    ∏ i : Option ι, (μ i) (s i)

Tactic:
have : e_meas ⁻¹' pi univ s = (pi univ (fun i ↦ s (some i))) ×ˢ (s none) := by
  ext x
  simp only [mem_preimage, Set.mem_pi, mem_univ, forall_true_left, mem_prod]
  refine ⟨by tauto, fun _ i ↦ ?_⟩
  rcases i <;> tauto

Result:
ι : Type u_1
inst✝² : Fintype ι
β : Option ι → Type u_4
inst✝¹ : (i : Option ι) → MeasurableSpace (β i)
μ : (i : Option ι) → Measure (β i)
inst✝ : ∀ (i : Option ι), SigmaFinite (μ i)
s : (i : Option ι) → Set (β i)
x✝ : ∀ (i : Option ι), MeasurableSet (s i)
e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) := (MeasurableEquiv.piOptionEquivProd β).symm
me : MeasurableEmbedding ⇑e_meas
this : ⇑e_meas ⁻¹' univ.pi s = (univ.pi fun i => s (some i)) ×ˢ s none
⊢ (map (⇑(MeasurableEquiv.piOptionEquivProd β).symm) ((Measure.pi fun i => μ (some i)).prod (μ none))) (univ.pi s) =
    ∏ i : Option ι, (μ i) (s i)