-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem volume_preserving_transvectionStruct [DecidableEq ι] (t : TransvectionStruct ι ℝ) :
    MeasurePreserving (toLin' t.toMatrix)

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
⊢ MeasurePreserving (⇑(toLin' t.toMatrix)) volume volume

Tactic:
have ht : Measurable (toLin' t.toMatrix) :=
  (toLin' t.toMatrix).continuous_of_finiteDimensional.measurable

Result:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
ht : Measurable ⇑(toLin' t.toMatrix)
⊢ MeasurePreserving (⇑(toLin' t.toMatrix)) volume volume

Proof state:
case h.mk
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
h2s : MeasurableSet (univ.pi s)
x : ι → ℝ
t_i t_j : ι
t_hij : t_i ≠ t_j
t_c : ℝ
ht : Measurable ⇑(toLin' { i := t_i, j := t_j, hij := t_hij, c := t_c }.toMatrix)
⊢ ∫⁻ (xᵢ : ℝ),
      (univ.pi s).indicator 1
        ((toLin' { i := t_i, j := t_j, hij := t_hij, c := t_c }.toMatrix)
          (Function.update x { i := t_i, j := t_j, hij := t_hij, c := t_c }.i xᵢ)) =
    ∫⁻ (xᵢ : ℝ), (univ.pi s).indicator 1 (Function.update x { i := t_i, j := t_j, hij := t_hij, c := t_c }.i xᵢ)

Tactic:
simp [transvection, mulVec_stdBasisMatrix, t_hij.symm, ← Function.update_add,
  lintegral_add_right_eq_self fun xᵢ ↦ indicator (univ.pi s) 1 (Function.update x t_i xᵢ)]

Result:
no goals

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
ht : Measurable ⇑(toLin' t.toMatrix)
⊢ Measure.map (⇑(toLin' t.toMatrix)) volume = volume

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

Result:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
ht : Measurable ⇑(toLin' t.toMatrix)
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ (Measure.map (⇑(toLin' t.toMatrix)) volume) (univ.pi s) = ∏ i : ι, volume (s i)

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
ht : Measurable ⇑(toLin' t.toMatrix)
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
h2s : MeasurableSet (univ.pi s)
⊢ (fun x => ∫⁻ (xᵢ : ℝ), (univ.pi s).indicator 1 ((toLin' t.toMatrix) (Function.update x t.i xᵢ))) = fun x =>
    ∫⁻ (xᵢ : ℝ), (univ.pi s).indicator 1 (Function.update x t.i xᵢ)

Tactic:
ext x

Result:
case h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
ht : Measurable ⇑(toLin' t.toMatrix)
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
h2s : MeasurableSet (univ.pi s)
x : ι → ℝ
⊢ ∫⁻ (xᵢ : ℝ), (univ.pi s).indicator 1 ((toLin' t.toMatrix) (Function.update x t.i xᵢ)) =
    ∫⁻ (xᵢ : ℝ), (univ.pi s).indicator 1 (Function.update x t.i xᵢ)

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
ht : Measurable ⇑(toLin' t.toMatrix)
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
h2s : MeasurableSet (univ.pi s)
⊢ (∫⁻ (a : ι → ℝ), (univ.pi s).indicator 1 ((toLin' t.toMatrix) a) ∂Measure.pi fun x => volume) =
    ∫⁻ (a : ι → ℝ), (univ.pi s).indicator 1 a ∂Measure.pi fun i => volume

Tactic:
refine lintegral_eq_of_lmarginal_eq {t.i} ((measurable_one.indicator h2s).comp ht)
  (measurable_one.indicator h2s) ?_

Result:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
ht : Measurable ⇑(toLin' t.toMatrix)
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
h2s : MeasurableSet (univ.pi s)
⊢ (∫⋯∫⁻_{t.i}, fun a => (univ.pi s).indicator 1 ((toLin' t.toMatrix) a) ∂fun x => volume) =
    ∫⋯∫⁻_{t.i}, (univ.pi s).indicator 1 ∂fun x => volume

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
ht : Measurable ⇑(toLin' t.toMatrix)
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
h2s : MeasurableSet (univ.pi s)
⊢ ∫⁻ (a : ι → ℝ), (univ.pi s).indicator 1 a ∂Measure.map (⇑(toLin' t.toMatrix)) volume =
    ∫⁻ (a : ι → ℝ), (univ.pi s).indicator 1 a ∂Measure.pi fun i => volume

Tactic:
rw [lintegral_map (measurable_one.indicator h2s) ht, volume_pi]

Result:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
ht : Measurable ⇑(toLin' t.toMatrix)
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
h2s : MeasurableSet (univ.pi s)
⊢ (∫⁻ (a : ι → ℝ), (univ.pi s).indicator 1 ((toLin' t.toMatrix) a) ∂Measure.pi fun x => volume) =
    ∫⁻ (a : ι → ℝ), (univ.pi s).indicator 1 a ∂Measure.pi fun i => volume

Proof state:
case h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
ht : Measurable ⇑(toLin' t.toMatrix)
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
h2s : MeasurableSet (univ.pi s)
x : ι → ℝ
⊢ ∫⁻ (xᵢ : ℝ), (univ.pi s).indicator 1 ((toLin' t.toMatrix) (Function.update x t.i xᵢ)) =
    ∫⁻ (xᵢ : ℝ), (univ.pi s).indicator 1 (Function.update x t.i xᵢ)

Tactic:
cases t with | mk t_i t_j t_hij t_c =>
simp [transvection, mulVec_stdBasisMatrix, t_hij.symm, ← Function.update_add,
  lintegral_add_right_eq_self fun xᵢ ↦ indicator (univ.pi s) 1 (Function.update x t_i xᵢ)]

Result:
no goals

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
ht : Measurable ⇑(toLin' t.toMatrix)
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ (Measure.map (⇑(toLin' t.toMatrix)) volume) (univ.pi s) = ∏ i : ι, volume (s i)

Tactic:
have h2s : MeasurableSet (univ.pi s) := .pi countable_univ fun i _ ↦ hs i

Result:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
ht : Measurable ⇑(toLin' t.toMatrix)
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
h2s : MeasurableSet (univ.pi s)
⊢ (Measure.map (⇑(toLin' t.toMatrix)) volume) (univ.pi s) = ∏ i : ι, volume (s i)

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
ht : Measurable ⇑(toLin' t.toMatrix)
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
h2s : MeasurableSet (univ.pi s)
⊢ (Measure.map (⇑(toLin' t.toMatrix)) volume) (univ.pi s) = ∏ i : ι, volume (s i)

Tactic:
simp_rw [← pi_pi, ← lintegral_indicator_one h2s]

Result:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
ht : Measurable ⇑(toLin' t.toMatrix)
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
h2s : MeasurableSet (univ.pi s)
⊢ ∫⁻ (a : ι → ℝ), (univ.pi s).indicator 1 a ∂Measure.map (⇑(toLin' t.toMatrix)) volume =
    ∫⁻ (a : ι → ℝ), (univ.pi s).indicator 1 a ∂Measure.pi fun i => volume

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
ht : Measurable ⇑(toLin' t.toMatrix)
⊢ MeasurePreserving (⇑(toLin' t.toMatrix)) volume volume

Tactic:
refine ⟨ht, ?_⟩

Result:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
ht : Measurable ⇑(toLin' t.toMatrix)
⊢ Measure.map (⇑(toLin' t.toMatrix)) volume = volume

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
ht : Measurable ⇑(toLin' t.toMatrix)
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
h2s : MeasurableSet (univ.pi s)
⊢ (∫⋯∫⁻_{t.i}, fun a => (univ.pi s).indicator 1 ((toLin' t.toMatrix) a) ∂fun x => volume) =
    ∫⋯∫⁻_{t.i}, (univ.pi s).indicator 1 ∂fun x => volume

Tactic:
simp_rw [lmarginal_singleton]

Result:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
t : TransvectionStruct ι ℝ
ht : Measurable ⇑(toLin' t.toMatrix)
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
h2s : MeasurableSet (univ.pi s)
⊢ (fun x => ∫⁻ (xᵢ : ℝ), (univ.pi s).indicator 1 ((toLin' t.toMatrix) (Function.update x t.i xᵢ))) = fun x =>
    ∫⁻ (xᵢ : ℝ), (univ.pi s).indicator 1 (Function.update x t.i xᵢ)