-- Mathlib/MeasureTheory/Integral/Marginal.lean
theorem lmarginal_singleton (f : (∀ i, π i) → ℝ≥0∞) (i : δ) :
    ∫⋯∫⁻_{i}, f ∂μ = fun x => ∫⁻ xᵢ, f (Function.update x i xᵢ) ∂μ i

Proof state:
δ : Type u_1
π : δ → Type u_3
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : DecidableEq δ
f : ((i : δ) → π i) → ℝ≥0∞
i : δ
α : Type u_1 := { x // x ∈ {i} }
⊢ ∫⋯∫⁻_{i}, f ∂μ = fun x => ∫⁻ (xᵢ : π i), f (update x i xᵢ) ∂μ i

Tactic:
let e := (MeasurableEquiv.piUnique fun j : α ↦ π j).symm

Result:
δ : Type u_1
π : δ → Type u_3
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : DecidableEq δ
f : ((i : δ) → π i) → ℝ≥0∞
i : δ
α : Type u_1 := { x // x ∈ {i} }
e : π ↑default ≃ᵐ ((i_1 : α) → π ↑i_1) := (MeasurableEquiv.piUnique fun j => π ↑j).symm
⊢ ∫⋯∫⁻_{i}, f ∂μ = fun x => ∫⁻ (xᵢ : π i), f (update x i xᵢ) ∂μ i

Proof state:
δ : Type u_1
π : δ → Type u_3
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : DecidableEq δ
f : ((i : δ) → π i) → ℝ≥0∞
i : δ
α : Type u_1 := { x // x ∈ {i} }
e : π ↑default ≃ᵐ ((i_1 : α) → π ↑i_1) := (MeasurableEquiv.piUnique fun j => π ↑j).symm
x : (i : δ) → π i
⊢ (∫⋯∫⁻_{i}, f ∂μ) x = ∫⁻ (y : π ↑default), f (updateFinset x {i} (e y)) ∂μ ↑default

Tactic:
simp_rw [lmarginal,
  measurePreserving_piUnique (fun j : ({i} : Finset δ) ↦ μ j) |>.symm _
    |>.lintegral_map_equiv, e, α]

Result:
no goals

Proof state:
δ : Type u_1
π : δ → Type u_3
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : DecidableEq δ
f : ((i : δ) → π i) → ℝ≥0∞
i : δ
α : Type u_1 := { x // x ∈ {i} }
e : π ↑default ≃ᵐ ((i_1 : α) → π ↑i_1) := (MeasurableEquiv.piUnique fun j => π ↑j).symm
x : (i : δ) → π i
⊢ ∫⁻ (y : π ↑default), f (updateFinset x {i} (e y)) ∂μ ↑default = ∫⁻ (xᵢ : π i), f (update x i xᵢ) ∂μ i

Tactic:
simp [update_eq_updateFinset]

Result:
δ : Type u_1
π : δ → Type u_3
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : DecidableEq δ
f : ((i : δ) → π i) → ℝ≥0∞
i : δ
α : Type u_1 := { x // x ∈ {i} }
e : π ↑default ≃ᵐ ((i_1 : α) → π ↑i_1) := (MeasurableEquiv.piUnique fun j => π ↑j).symm
x : (i : δ) → π i
⊢ ∫⁻ (y : π ↑default), f (updateFinset x {i} (e y)) ∂μ ↑default =
    ∫⁻ (xᵢ : π i), f (updateFinset x {i} (uniqueElim xᵢ)) ∂μ i

Proof state:
δ : Type u_1
π : δ → Type u_3
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : DecidableEq δ
f : ((i : δ) → π i) → ℝ≥0∞
i : δ
α : Type u_1 := { x // x ∈ {i} }
e : π ↑default ≃ᵐ ((i_1 : α) → π ↑i_1) := (MeasurableEquiv.piUnique fun j => π ↑j).symm
⊢ ∫⋯∫⁻_{i}, f ∂μ = fun x => ∫⁻ (xᵢ : π i), f (update x i xᵢ) ∂μ i

Tactic:
ext1 x

Result:
case h
δ : Type u_1
π : δ → Type u_3
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : DecidableEq δ
f : ((i : δ) → π i) → ℝ≥0∞
i : δ
α : Type u_1 := { x // x ∈ {i} }
e : π ↑default ≃ᵐ ((i_1 : α) → π ↑i_1) := (MeasurableEquiv.piUnique fun j => π ↑j).symm
x : (i : δ) → π i
⊢ (∫⋯∫⁻_{i}, f ∂μ) x = ∫⁻ (xᵢ : π i), f (update x i xᵢ) ∂μ i

Proof state:
δ : Type u_1
π : δ → Type u_3
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : DecidableEq δ
f : ((i : δ) → π i) → ℝ≥0∞
i : δ
α : Type u_1 := { x // x ∈ {i} }
e : π ↑default ≃ᵐ ((i_1 : α) → π ↑i_1) := (MeasurableEquiv.piUnique fun j => π ↑j).symm
x : (i : δ) → π i
⊢ ∫⁻ (y : π ↑default), f (updateFinset x {i} (e y)) ∂μ ↑default =
    ∫⁻ (xᵢ : π i), f (updateFinset x {i} (uniqueElim xᵢ)) ∂μ i

Tactic:
rfl

Result:
no goals

Proof state:
δ : Type u_1
π : δ → Type u_3
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : DecidableEq δ
f : ((i : δ) → π i) → ℝ≥0∞
i : δ
⊢ ∫⋯∫⁻_{i}, f ∂μ = fun x => ∫⁻ (xᵢ : π i), f (update x i xᵢ) ∂μ i

Tactic:
let α : Type _ := ({i} : Finset δ)

Result:
δ : Type u_1
π : δ → Type u_3
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : DecidableEq δ
f : ((i : δ) → π i) → ℝ≥0∞
i : δ
α : Type u_1 := { x // x ∈ {i} }
⊢ ∫⋯∫⁻_{i}, f ∂μ = fun x => ∫⁻ (xᵢ : π i), f (update x i xᵢ) ∂μ i

Proof state:
case h
δ : Type u_1
π : δ → Type u_3
inst✝¹ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝ : DecidableEq δ
f : ((i : δ) → π i) → ℝ≥0∞
i : δ
α : Type u_1 := { x // x ∈ {i} }
e : π ↑default ≃ᵐ ((i_1 : α) → π ↑i_1) := (MeasurableEquiv.piUnique fun j => π ↑j).symm
x : (i : δ) → π i
⊢ (∫⋯∫⁻_{i}, f ∂μ) x = ∫⁻ (xᵢ : π i), f (update x i xᵢ) ∂μ i

Tactic:
calc (∫⋯∫⁻_{i}, f ∂μ) x
    = ∫⁻ (y : π (default : α)), f (updateFinset x {i} (e y)) ∂μ (default : α) := by
      simp_rw [lmarginal,
        measurePreserving_piUnique (fun j : ({i} : Finset δ) ↦ μ j) |>.symm _
          |>.lintegral_map_equiv, e, α]
  _ = ∫⁻ xᵢ, f (Function.update x i xᵢ) ∂μ i := by simp [update_eq_updateFinset]; rfl

Result:
no goals