-- Mathlib/MeasureTheory/Constructions/Pi.lean
lemma pi_map_piCongrLeft [hι' : Fintype ι'] (e : ι ≃ ι') {β : ι' → Type*}
    [∀ i, MeasurableSpace (β i)] (μ : (i : ι') → Measure (β i)) [∀ i, SigmaFinite (μ i)] :
    (Measure.pi fun i ↦ μ (e i)).map (MeasurableEquiv.piCongrLeft (fun i ↦ β i) e)
      = Measure.pi μ

Proof state:
case h
ι : Type u_1
ι' : Type u_2
inst✝² : Fintype ι
hι' : Fintype ι'
e : ι ≃ ι'
β : ι' → Type u_4
inst✝¹ : (i : ι') → MeasurableSpace (β i)
μ : (i : ι') → Measure (β i)
inst✝ : ∀ (i : ι'), SigmaFinite (μ i)
e_meas : ((b : ι) → β (e b)) ≃ᵐ ((a : ι') → β a) := MeasurableEquiv.piCongrLeft (fun i => β i) e
s : (i : ι') → Set (β i)
x✝ : ∀ (i : ι'), MeasurableSet (s i)
s' : (i : ι) → Set (β (e i)) := fun i => s (e i)
x : (b : ι) → β (e b)
⊢ (∀ (i : ι'), e_meas x i ∈ s i) ↔ ∀ (i : ι), x i ∈ s (e i)

Tactic:
refine (e.forall_congr ?_).symm

Result:
case h
ι : Type u_1
ι' : Type u_2
inst✝² : Fintype ι
hι' : Fintype ι'
e : ι ≃ ι'
β : ι' → Type u_4
inst✝¹ : (i : ι') → MeasurableSpace (β i)
μ : (i : ι') → Measure (β i)
inst✝ : ∀ (i : ι'), SigmaFinite (μ i)
e_meas : ((b : ι) → β (e b)) ≃ᵐ ((a : ι') → β a) := MeasurableEquiv.piCongrLeft (fun i => β i) e
s : (i : ι') → Set (β i)
x✝ : ∀ (i : ι'), MeasurableSet (s i)
s' : (i : ι) → Set (β (e i)) := fun i => s (e i)
x : (b : ι) → β (e b)
⊢ ∀ (a : ι), x a ∈ s (e a) ↔ e_meas x (e a) ∈ s (e a)

Proof state:
case hst
ι : Type u_1
ι' : Type u_2
inst✝² : Fintype ι
hι' : Fintype ι'
e : ι ≃ ι'
β : ι' → Type u_4
inst✝¹ : (i : ι') → MeasurableSpace (β i)
μ : (i : ι') → Measure (β i)
inst✝ : ∀ (i : ι'), SigmaFinite (μ i)
e_meas : ((b : ι) → β (e b)) ≃ᵐ ((a : ι') → β a) := MeasurableEquiv.piCongrLeft (fun i => β i) e
s : (i : ι') → Set (β i)
x✝ : ∀ (i : ι'), MeasurableSet (s i)
s' : (i : ι) → Set (β (e i)) := fun i => s (e i)
this : ⇑e_meas ⁻¹' univ.pi s = univ.pi s'
⊢ ∀ (i : ι'), i ∈ Finset.univ ↔ e.symm i ∈ Finset.univ

Tactic:
simp only [Finset.mem_univ, implies_true]

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
inst✝² : Fintype ι
hι' : Fintype ι'
e : ι ≃ ι'
β : ι' → Type u_4
inst✝¹ : (i : ι') → MeasurableSpace (β i)
μ : (i : ι') → Measure (β i)
inst✝ : ∀ (i : ι'), SigmaFinite (μ i)
e_meas : ((b : ι) → β (e b)) ≃ᵐ ((a : ι') → β a) := MeasurableEquiv.piCongrLeft (fun i => β i) e
⊢ map (⇑(MeasurableEquiv.piCongrLeft (fun i => β i) e)) (Measure.pi fun i => μ (e i)) = Measure.pi μ

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

Result:
ι : Type u_1
ι' : Type u_2
inst✝² : Fintype ι
hι' : Fintype ι'
e : ι ≃ ι'
β : ι' → Type u_4
inst✝¹ : (i : ι') → MeasurableSpace (β i)
μ : (i : ι') → Measure (β i)
inst✝ : ∀ (i : ι'), SigmaFinite (μ i)
e_meas : ((b : ι) → β (e b)) ≃ᵐ ((a : ι') → β a) := MeasurableEquiv.piCongrLeft (fun i => β i) e
s : (i : ι') → Set (β i)
x✝ : ∀ (i : ι'), MeasurableSet (s i)
⊢ (map (⇑(MeasurableEquiv.piCongrLeft (fun i => β i) e)) (Measure.pi fun i => μ (e i))) (univ.pi s) =
    ∏ i : ι', (μ i) (s i)

Proof state:
case hfg.h.e_6
ι : Type u_1
ι' : Type u_2
inst✝² : Fintype ι
hι' : Fintype ι'
e : ι ≃ ι'
β : ι' → Type u_4
inst✝¹ : (i : ι') → MeasurableSpace (β i)
μ : (i : ι') → Measure (β i)
inst✝ : ∀ (i : ι'), SigmaFinite (μ i)
e_meas : ((b : ι) → β (e b)) ≃ᵐ ((a : ι') → β a) := MeasurableEquiv.piCongrLeft (fun i => β i) e
s : (i : ι') → Set (β i)
x✝ : ∀ (i : ι'), MeasurableSet (s i)
s' : (i : ι) → Set (β (e i)) := fun i => s (e i)
this : ⇑e_meas ⁻¹' univ.pi s = univ.pi s'
i : ι'
a✝ : i ∈ Finset.univ
⊢ HEq (s i) (s (e (e.symm i)))

Tactic:
rw [e.apply_symm_apply]

Result:
no goals

Proof state:
case hfg
ι : Type u_1
ι' : Type u_2
inst✝² : Fintype ι
hι' : Fintype ι'
e : ι ≃ ι'
β : ι' → Type u_4
inst✝¹ : (i : ι') → MeasurableSpace (β i)
μ : (i : ι') → Measure (β i)
inst✝ : ∀ (i : ι'), SigmaFinite (μ i)
e_meas : ((b : ι) → β (e b)) ≃ᵐ ((a : ι') → β a) := MeasurableEquiv.piCongrLeft (fun i => β i) e
s : (i : ι') → Set (β i)
x✝ : ∀ (i : ι'), MeasurableSet (s i)
s' : (i : ι) → Set (β (e i)) := fun i => s (e i)
this : ⇑e_meas ⁻¹' univ.pi s = univ.pi s'
⊢ ∀ i ∈ Finset.univ, (μ i) (s i) = (μ (e (e.symm i))) (s' (e.symm i))

Tactic:
intro i _

Result:
case hfg
ι : Type u_1
ι' : Type u_2
inst✝² : Fintype ι
hι' : Fintype ι'
e : ι ≃ ι'
β : ι' → Type u_4
inst✝¹ : (i : ι') → MeasurableSpace (β i)
μ : (i : ι') → Measure (β i)
inst✝ : ∀ (i : ι'), SigmaFinite (μ i)
e_meas : ((b : ι) → β (e b)) ≃ᵐ ((a : ι') → β a) := MeasurableEquiv.piCongrLeft (fun i => β i) e
s : (i : ι') → Set (β i)
x✝ : ∀ (i : ι'), MeasurableSet (s i)
s' : (i : ι) → Set (β (e i)) := fun i => s (e i)
this : ⇑e_meas ⁻¹' univ.pi s = univ.pi s'
i : ι'
a✝ : i ∈ Finset.univ
⊢ (μ i) (s i) = (μ (e (e.symm i))) (s' (e.symm i))

Proof state:
case h
ι : Type u_1
ι' : Type u_2
inst✝² : Fintype ι
hι' : Fintype ι'
e : ι ≃ ι'
β : ι' → Type u_4
inst✝¹ : (i : ι') → MeasurableSpace (β i)
μ : (i : ι') → Measure (β i)
inst✝ : ∀ (i : ι'), SigmaFinite (μ i)
e_meas : ((b : ι) → β (e b)) ≃ᵐ ((a : ι') → β a) := MeasurableEquiv.piCongrLeft (fun i => β i) e
s : (i : ι') → Set (β i)
x✝ : ∀ (i : ι'), MeasurableSet (s i)
s' : (i : ι) → Set (β (e i)) := fun i => s (e i)
x : (b : ι) → β (e b)
i : ι
⊢ x i ∈ s (e i) ↔ e_meas x (e i) ∈ s (e i)

Tactic:
rw [MeasurableEquiv.piCongrLeft_apply_apply e x i]

Result:
no goals

Proof state:
case h
ι : Type u_1
ι' : Type u_2
inst✝² : Fintype ι
hι' : Fintype ι'
e : ι ≃ ι'
β : ι' → Type u_4
inst✝¹ : (i : ι') → MeasurableSpace (β i)
μ : (i : ι') → Measure (β i)
inst✝ : ∀ (i : ι'), SigmaFinite (μ i)
e_meas : ((b : ι) → β (e b)) ≃ᵐ ((a : ι') → β a) := MeasurableEquiv.piCongrLeft (fun i => β i) e
s : (i : ι') → Set (β i)
x✝ : ∀ (i : ι'), MeasurableSet (s i)
s' : (i : ι) → Set (β (e i)) := fun i => s (e i)
x : (b : ι) → β (e b)
⊢ x ∈ ⇑e_meas ⁻¹' univ.pi s ↔ x ∈ univ.pi s'

Tactic:
simp only [mem_preimage, Set.mem_pi, mem_univ, forall_true_left, s']

Result:
case h
ι : Type u_1
ι' : Type u_2
inst✝² : Fintype ι
hι' : Fintype ι'
e : ι ≃ ι'
β : ι' → Type u_4
inst✝¹ : (i : ι') → MeasurableSpace (β i)
μ : (i : ι') → Measure (β i)
inst✝ : ∀ (i : ι'), SigmaFinite (μ i)
e_meas : ((b : ι) → β (e b)) ≃ᵐ ((a : ι') → β a) := MeasurableEquiv.piCongrLeft (fun i => β i) e
s : (i : ι') → Set (β i)
x✝ : ∀ (i : ι'), MeasurableSet (s i)
s' : (i : ι) → Set (β (e i)) := fun i => s (e i)
x : (b : ι) → β (e b)
⊢ (∀ (i : ι'), e_meas x i ∈ s i) ↔ ∀ (i : ι), x i ∈ s (e i)

Proof state:
ι : Type u_1
ι' : Type u_2
inst✝² : Fintype ι
hι' : Fintype ι'
e : ι ≃ ι'
β : ι' → Type u_4
inst✝¹ : (i : ι') → MeasurableSpace (β i)
μ : (i : ι') → Measure (β i)
inst✝ : ∀ (i : ι'), SigmaFinite (μ i)
e_meas : ((b : ι) → β (e b)) ≃ᵐ ((a : ι') → β a) := MeasurableEquiv.piCongrLeft (fun i => β i) e
s : (i : ι') → Set (β i)
x✝ : ∀ (i : ι'), MeasurableSet (s i)
s' : (i : ι) → Set (β (e i)) := fun i => s (e i)
this : ⇑e_meas ⁻¹' univ.pi s = univ.pi s'
⊢ (Measure.pi fun i => μ (e i)) (⇑e_meas ⁻¹' univ.pi s) = ∏ i : ι', (μ i) (s i)

Tactic:
rw [this, pi_pi, Finset.prod_equiv e.symm]

Result:
case hst
ι : Type u_1
ι' : Type u_2
inst✝² : Fintype ι
hι' : Fintype ι'
e : ι ≃ ι'
β : ι' → Type u_4
inst✝¹ : (i : ι') → MeasurableSpace (β i)
μ : (i : ι') → Measure (β i)
inst✝ : ∀ (i : ι'), SigmaFinite (μ i)
e_meas : ((b : ι) → β (e b)) ≃ᵐ ((a : ι') → β a) := MeasurableEquiv.piCongrLeft (fun i => β i) e
s : (i : ι') → Set (β i)
x✝ : ∀ (i : ι'), MeasurableSet (s i)
s' : (i : ι) → Set (β (e i)) := fun i => s (e i)
this : ⇑e_meas ⁻¹' univ.pi s = univ.pi s'
⊢ ∀ (i : ι'), i ∈ Finset.univ ↔ e.symm i ∈ Finset.univ

case hfg
ι : Type u_1
ι' : Type u_2
inst✝² : Fintype ι
hι' : Fintype ι'
e : ι ≃ ι'
β : ι' → Type u_4
inst✝¹ : (i : ι') → MeasurableSpace (β i)
μ : (i : ι') → Measure (β i)
inst✝ : ∀ (i : ι'), SigmaFinite (μ i)
e_meas : ((b : ι) → β (e b)) ≃ᵐ ((a : ι') → β a) := MeasurableEquiv.piCongrLeft (fun i => β i) e
s : (i : ι') → Set (β i)
x✝ : ∀ (i : ι'), MeasurableSet (s i)
s' : (i : ι) → Set (β (e i)) := fun i => s (e i)
this : ⇑e_meas ⁻¹' univ.pi s = univ.pi s'
⊢ ∀ i ∈ Finset.univ, (μ i) (s i) = (μ (e (e.symm i))) (s' (e.symm i))