awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
G : ι → Type u_4
inst_3 : (i : ι) → Group (G i)
inst_4 : (i : ι) → MeasureSpace (G i)
inst_5 : ∀ (i : ι), MeasurableMul.{u_4} (G i)
inst_6 : (i : ι) → TopologicalSpace (G i)
inst_7 : ∀ (i : ι), SigmaFinite.{u_4} (α := G i) (m0 := MeasureSpace.toMeasurableSpace) volume
inst_8 : ∀ (i : ι), IsHaarMeasure.{u_4} (G := G i) volume
⊢ IsHaarMeasure (G := (i : ι) → G i) volume

Tactic:
pi.isHaarMeasure _

Premises used: MeasureTheory.Measure.pi.isHaarMeasure
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasureSpace (α i)
⊢ Eq (α := Measure ((i : ι) → α i)) volume (Measure.pi (α := α) fun (x : ι) ↦ volume)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasureSpace (α i)
inst_2 : ∀ (i : ι), SigmaFinite.{u_3} (α := α i) (m0 := MeasureSpace.toMeasurableSpace) volume
s : (i : ι) → Set (α i)
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    (∏ i : ι, ((volume : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
Measure.pi_pi (fun _ => volume) s

Premises used: MeasureTheory.MeasureSpace.volume, MeasureTheory.Measure.pi_pi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasureSpace (α i)
inst_2 : ∀ (i : ι), SigmaFinite.{u_3} (α := α i) (m0 := MeasureSpace.toMeasurableSpace) volume
inst_3 : (i : ι) → MetricSpace (α i)
x : (i : ι) → α i
r : ℝ
hr : 0 < r
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Metric.ball x r) : ℝ≥0∞)
    (∏ i : ι, ((volume : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) (Metric.ball (x i) r) : ℝ≥0∞)

Tactic:
Measure.pi_ball _ _ hr

Premises used: MeasureTheory.Measure.pi_ball
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasureSpace (α i)
inst_2 : ∀ (i : ι), SigmaFinite.{u_3} (α := α i) (m0 := MeasureSpace.toMeasurableSpace) volume
inst_3 : (i : ι) → MetricSpace (α i)
x : (i : ι) → α i
r : ℝ
hr : 0 ≤ r
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Metric.closedBall x r) : ℝ≥0∞)
    (∏ i : ι, ((volume : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) (Metric.closedBall (x i) r) : ℝ≥0∞)

Tactic:
Measure.pi_closedBall _ _ hr

Premises used: MeasureTheory.Measure.pi_closedBall
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
ι' : Type u_2
α_1 : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α_1 i)
α : Type u_4
inst_1 : Group α
inst_2 : MeasureSpace α
inst_3 : SigmaFinite.{u_4} (α := α) (m0 := MeasureSpace.toMeasurableSpace) volume
inst_4 : MeasurableMul α
inst_5 : IsMulLeftInvariant.{u_4} (G := α) volume
⊢ IsMulLeftInvariant (G := ι → α) volume

Tactic:
pi.isMulLeftInvariant _

Premises used: MeasureTheory.Measure.pi.isMulLeftInvariant
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
ι' : Type u_2
α_1 : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α_1 i)
α : Type u_4
inst_1 : Group α
inst_2 : MeasureSpace α
inst_3 : SigmaFinite.{u_4} (α := α) (m0 := MeasureSpace.toMeasurableSpace) volume
inst_4 : MeasurableInv α
inst_5 : IsInvInvariant.{u_4} (G := α) volume
⊢ IsInvInvariant (G := ι → α) volume

Tactic:
pi.isInvInvariant _

Premises used: MeasureTheory.Measure.pi.isInvInvariant
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_1 : ∀ (i : ι), SigmaFinite (μ i)
p : ι → Prop
inst_2 : DecidablePred p
e : ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι)) ≃ᵐ ((i : ι) → α i) :=
  MeasurableEquiv.symm (MeasurableEquiv.piEquivPiSubtypeProd α p)
⊢ MeasurePreserving (β := ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι)))
    (⇑(MeasurableEquiv.piEquivPiSubtypeProd α p) :
      (a : (i : ι) → α i) → ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι)))
    (Measure.pi (α := α) μ)
    (Measure.prod (Measure.pi (α := fun (i : Subtype p) ↦ α (↑i : ι)) fun (i : Subtype p) ↦ μ (↑i : ι))
      (Measure.pi (α := fun (i : { i : ι // ¬p i }) ↦ α (↑i : ι)) fun (i : { i : ι // ¬p i }) ↦ μ (↑i : ι)))

Tactic:
MeasurePreserving.symm e ?_

Premises used: MeasureTheory.MeasurePreserving.symm
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_1 : ∀ (i : ι), SigmaFinite (μ i)
p : ι → Prop
inst_2 : DecidablePred p
e : ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι)) ≃ᵐ ((i : ι) → α i) :=
  MeasurableEquiv.symm (MeasurableEquiv.piEquivPiSubtypeProd α p)
refine :
  MeasurePreserving (α := ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι)))
    (⇑e : (a : ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι))) → (i : ι) → α i)
    (Measure.prod (Measure.pi (α := fun (i : Subtype p) ↦ α (↑i : ι)) fun (i : Subtype p) ↦ μ (↑i : ι))
      (Measure.pi (α := fun (i : { i : ι // ¬p i }) ↦ α (↑i : ι)) fun (i : { i : ι // ¬p i }) ↦ μ (↑i : ι)))
    (Measure.pi (α := α) μ)
⊢ MeasurePreserving (β := ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι)))
    (⇑(MeasurableEquiv.piEquivPiSubtypeProd α p) :
      (a : (i : ι) → α i) → ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι)))
    (Measure.pi (α := α) μ)
    (Measure.prod (Measure.pi (α := fun (i : Subtype p) ↦ α (↑i : ι)) fun (i : Subtype p) ↦ μ (↑i : ι))
      (Measure.pi (α := fun (i : { i : ι // ¬p i }) ↦ α (↑i : ι)) fun (i : { i : ι // ¬p i }) ↦ μ (↑i : ι)))

Tactic:
refine MeasurePreserving.symm e ?_

Premises used: MeasureTheory.MeasurePreserving.symm
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_1 : ∀ (i : ι), SigmaFinite (μ i)
p : ι → Prop
inst_2 : DecidablePred p
e : ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι)) ≃ᵐ ((i : ι) → α i) :=
  MeasurableEquiv.symm (MeasurableEquiv.piEquivPiSubtypeProd α p)
⊢ MeasurePreserving (α := ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι)))
    (⇑e : (a : ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι))) → (i : ι) → α i)
    (Measure.prod (Measure.pi (α := fun (i : Subtype p) ↦ α (↑i : ι)) fun (i : Subtype p) ↦ μ (↑i : ι))
      (Measure.pi (α := fun (i : { i : ι // ¬p i }) ↦ α (↑i : ι)) fun (i : { i : ι // ¬p i }) ↦ μ (↑i : ι)))
    (Measure.pi (α := α) μ)

Tactic:
⟨e.measurable, (pi_eq fun s _ => ?_).symm⟩

Premises used: MeasureTheory.MeasurePreserving.mk, MeasureTheory.Measure.pi_eq, MeasurableEquiv.measurable, Eq.symm
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_1 : ∀ (i : ι), SigmaFinite (μ i)
p : ι → Prop
inst_2 : DecidablePred p
e : ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι)) ≃ᵐ ((i : ι) → α i) :=
  MeasurableEquiv.symm (MeasurableEquiv.piEquivPiSubtypeProd α p)
refine :
  ∀ (s : (i : ι) → Set (α i)),
    (∀ (i : ι), MeasurableSet (s i)) →
      Eq (α := ℝ≥0∞)
        ((Measure.map (α := ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι)))
                (⇑e : (a : ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι))) → (i : ι) → α i)
                (Measure.prod (Measure.pi (α := fun (i : Subtype p) ↦ α (↑i : ι)) fun (i : Subtype p) ↦ μ (↑i : ι))
                  (Measure.pi (α := fun (i : { i : ι // ¬p i }) ↦ α (↑i : ι)) fun (i : { i : ι // ¬p i }) ↦
                    μ (↑i : ι))) :
              (a : Set ((i : ι) → α i)) → ℝ≥0∞)
            (Set.pi (α := α) univ s) :
          ℝ≥0∞)
        (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ MeasurePreserving (α := ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι)))
    (⇑e : (a : ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι))) → (i : ι) → α i)
    (Measure.prod (Measure.pi (α := fun (i : Subtype p) ↦ α (↑i : ι)) fun (i : Subtype p) ↦ μ (↑i : ι))
      (Measure.pi (α := fun (i : { i : ι // ¬p i }) ↦ α (↑i : ι)) fun (i : { i : ι // ¬p i }) ↦ μ (↑i : ι)))
    (Measure.pi (α := α) μ)

Tactic:
refine ⟨e.measurable, (pi_eq fun s _ => ?_).symm⟩
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_1 : ∀ (i : ι), SigmaFinite (μ i)
p : ι → Prop
inst_2 : DecidablePred p
e : ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι)) ≃ᵐ ((i : ι) → α i) :=
  MeasurableEquiv.symm (MeasurableEquiv.piEquivPiSubtypeProd α p)
s : (i : ι) → Set (α i)
h : ∀ (i : ι), MeasurableSet (s i)
⊢ (⇑e : (a : ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι))) → (i : ι) → α i) ⁻¹'
      Set.pi (α := α) univ s =
    SProd.sprod (α := Set ((i : { i : ι // p i }) → α (↑i : ι))) (β := Set ((i : { i : ι // ¬p i }) → α (↑i : ι)))
      (Set.pi (α := fun (i : { i : ι // p i }) ↦ α (↑i : ι)) univ fun (i : { i : ι // p i }) ↦ s (↑i : ι))
      (Set.pi (α := fun (i : { i : ι // ¬p i }) ↦ α (↑i : ι)) univ fun (i : { i : ι // ¬p i }) ↦ s (↑i : ι))

Tactic:
have : e ⁻¹' pi univ s =
      (pi univ fun i : { i // p i } => s i) ×ˢ pi univ fun i : { i // ¬p i } => s i :=
    Equiv.preimage_piEquivPiSubtypeProd_symm_pi p s
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_1 : ∀ (i : ι), SigmaFinite (μ i)
p : ι → Prop
inst_2 : DecidablePred p
e : ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι)) ≃ᵐ ((i : ι) → α i) :=
  MeasurableEquiv.symm (MeasurableEquiv.piEquivPiSubtypeProd α p)
s : (i : ι) → Set (α i)
h : ∀ (i : ι), MeasurableSet (s i)
this :
  (⇑e : (a : ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι))) → (i : ι) → α i) ⁻¹'
      Set.pi (α := α) univ s =
    SProd.sprod (α := Set ((i : { i : ι // p i }) → α (↑i : ι))) (β := Set ((i : { i : ι // ¬p i }) → α (↑i : ι)))
      (Set.pi (α := fun (i : { i : ι // p i }) ↦ α (↑i : ι)) univ fun (i : { i : ι // p i }) ↦ s (↑i : ι))
      (Set.pi (α := fun (i : { i : ι // ¬p i }) ↦ α (↑i : ι)) univ fun (i : { i : ι // ¬p i }) ↦ s (↑i : ι))
rw :
  HMul.hMul (α := ℝ≥0∞)
      (∏ i : Subtype p, ((μ (↑i : ι) : Measure (α (↑i : ι))) : (a : Set (α (↑i : ι))) → ℝ≥0∞) (s (↑i : ι)))
      (∏ i : { i : ι // ¬p i }, ((μ (↑i : ι) : Measure (α (↑i : ι))) : (a : Set (α (↑i : ι))) → ℝ≥0∞) (s (↑i : ι))) =
    ∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i)
⊢ Eq (α := ℝ≥0∞)
    ((Measure.map (α := ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι)))
            (⇑e : (a : ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι))) → (i : ι) → α i)
            (Measure.prod (Measure.pi (α := fun (i : Subtype p) ↦ α (↑i : ι)) fun (i : Subtype p) ↦ μ (↑i : ι))
              (Measure.pi (α := fun (i : { i : ι // ¬p i }) ↦ α (↑i : ι)) fun (i : { i : ι // ¬p i }) ↦ μ (↑i : ι))) :
          (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ s) :
      ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
rw [e.map_apply, this, prod_prod, pi_pi, pi_pi]

Premises used: MeasurableEquiv.map_apply, MeasureTheory.Measure.prod_prod, MeasureTheory.Measure.pi_pi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_1 : ∀ (i : ι), SigmaFinite (μ i)
p : ι → Prop
inst_2 : DecidablePred p
e : ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι)) ≃ᵐ ((i : ι) → α i) :=
  MeasurableEquiv.symm (MeasurableEquiv.piEquivPiSubtypeProd α p)
s : (i : ι) → Set (α i)
h : ∀ (i : ι), MeasurableSet (s i)
this :
  (⇑e : (a : ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι))) → (i : ι) → α i) ⁻¹'
      Set.pi (α := α) univ s =
    SProd.sprod (α := Set ((i : { i : ι // p i }) → α (↑i : ι))) (β := Set ((i : { i : ι // ¬p i }) → α (↑i : ι)))
      (Set.pi (α := fun (i : { i : ι // p i }) ↦ α (↑i : ι)) univ fun (i : { i : ι // p i }) ↦ s (↑i : ι))
      (Set.pi (α := fun (i : { i : ι // ¬p i }) ↦ α (↑i : ι)) univ fun (i : { i : ι // ¬p i }) ↦ s (↑i : ι))
⊢ HMul.hMul (α := ℝ≥0∞)
      (∏ i : Subtype p, ((μ (↑i : ι) : Measure (α (↑i : ι))) : (a : Set (α (↑i : ι))) → ℝ≥0∞) (s (↑i : ι)))
      (∏ i : { i : ι // ¬p i }, ((μ (↑i : ι) : Measure (α (↑i : ι))) : (a : Set (α (↑i : ι))) → ℝ≥0∞) (s (↑i : ι))) =
    ∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i)

Tactic:
Fintype.prod_subtype_mul_prod_subtype p fun i => μ i (s i)

Premises used: Fintype.prod_subtype_mul_prod_subtype, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_1 : ∀ (i : ι), SigmaFinite (μ i)
p : ι → Prop
inst_2 : DecidablePred p
e : ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι)) ≃ᵐ ((i : ι) → α i) :=
  MeasurableEquiv.symm (MeasurableEquiv.piEquivPiSubtypeProd α p)
s : (i : ι) → Set (α i)
h : ∀ (i : ι), MeasurableSet (s i)
this :
  (⇑e : (a : ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι))) → (i : ι) → α i) ⁻¹'
      Set.pi (α := α) univ s =
    SProd.sprod (α := Set ((i : { i : ι // p i }) → α (↑i : ι))) (β := Set ((i : { i : ι // ¬p i }) → α (↑i : ι)))
      (Set.pi (α := fun (i : { i : ι // p i }) ↦ α (↑i : ι)) univ fun (i : { i : ι // p i }) ↦ s (↑i : ι))
      (Set.pi (α := fun (i : { i : ι // ¬p i }) ↦ α (↑i : ι)) univ fun (i : { i : ι // ¬p i }) ↦ s (↑i : ι))
⊢ HMul.hMul (α := ℝ≥0∞)
      (∏ i : Subtype p, ((μ (↑i : ι) : Measure (α (↑i : ι))) : (a : Set (α (↑i : ι))) → ℝ≥0∞) (s (↑i : ι)))
      (∏ i : { i : ι // ¬p i }, ((μ (↑i : ι) : Measure (α (↑i : ι))) : (a : Set (α (↑i : ι))) → ℝ≥0∞) (s (↑i : ι))) =
    ∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i)

Tactic:
exact Fintype.prod_subtype_mul_prod_subtype p fun i => μ i (s i)

Premises used: Fintype.prod_subtype_mul_prod_subtype, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
inst : Fintype ι
α : ι → Type u_4
inst_1 : (i : ι) → MeasureSpace (α i)
inst_2 : ∀ (i : ι), SigmaFinite.{u_4} (α := α i) (m0 := MeasureSpace.toMeasurableSpace) volume
p : ι → Prop
inst_3 : DecidablePred p
⊢ MeasurePreserving (α := (i : ι) → α i) (β := ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι)))
    (⇑(MeasurableEquiv.piEquivPiSubtypeProd α p) :
      (a : (i : ι) → α i) → ((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι)))
    (volume : Measure ((i : ι) → α i))
    (volume : Measure (((i : Subtype p) → α (↑i : ι)) × ((i : { i : ι // ¬p i }) → α (↑i : ι))))

Tactic:
measurePreserving_piEquivPiSubtypeProd (fun _ => volume) p

Premises used: MeasureTheory.MeasureSpace.volume, MeasureTheory.measurePreserving_piEquivPiSubtypeProd
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_1 : ∀ (i : ι), SigmaFinite (μ i)
inst_2 : Fintype ι'
f : ι' ≃ ι
⊢ Measure.map (α := (b : ι') → α ((f : (a : ι') → ι) b))
      (⇑(MeasurableEquiv.piCongrLeft α f) : (a : (b : ι') → α ((f : (a : ι') → ι) b)) → (a : ι) → α a)
      (Measure.pi (α := fun (b : ι') ↦ α ((f : (a : ι') → ι) b)) fun (i' : ι') ↦ μ ((f : (a : ι') → ι) i')) =
    Measure.pi (α := α) μ

Tactic:
(pi_eq fun s _ => ?_).symm

Premises used: MeasureTheory.Measure.pi_eq, Eq.symm
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_1 : ∀ (i : ι), SigmaFinite (μ i)
inst_2 : Fintype ι'
f : ι' ≃ ι
refine :
  ∀ (s : (i : ι) → Set (α i)),
    (∀ (i : ι), MeasurableSet (s i)) →
      Eq (α := ℝ≥0∞)
        ((Measure.map (α := (b : ι') → α ((f : (a : ι') → ι) b))
                (⇑(MeasurableEquiv.piCongrLeft α f) : (a : (b : ι') → α ((f : (a : ι') → ι) b)) → (a : ι) → α a)
                (Measure.pi (α := fun (b : ι') ↦ α ((f : (a : ι') → ι) b)) fun (i' : ι') ↦ μ ((f : (a : ι') → ι) i')) :
              (a : Set ((i : ι) → α i)) → ℝ≥0∞)
            (Set.pi (α := α) univ s) :
          ℝ≥0∞)
        (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ Measure.map (α := (b : ι') → α ((f : (a : ι') → ι) b))
      (⇑(MeasurableEquiv.piCongrLeft α f) : (a : (b : ι') → α ((f : (a : ι') → ι) b)) → (a : ι) → α a)
      (Measure.pi (α := fun (b : ι') ↦ α ((f : (a : ι') → ι) b)) fun (i' : ι') ↦ μ ((f : (a : ι') → ι) i')) =
    Measure.pi (α := α) μ

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

Premises used: MeasureTheory.Measure.pi_eq, Eq.symm
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_1 : ∀ (i : ι), SigmaFinite (μ i)
inst_2 : Fintype ι'
f : ι' ≃ ι
s : (i : ι) → Set (α i)
h : ∀ (i : ι), MeasurableSet (s i)
rw :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := fun (b : ι') ↦ α ((f : (a : ι') → ι) b)) fun (i' : ι') ↦ μ ((f : (a : ι') → ι) i') :
          (a : Set ((b : ι') → α ((f : (a : ι') → ι) b))) → ℝ≥0∞)
        ((⇑(MeasurableEquiv.piCongrLeft α f) : (a : (b : ι') → α ((f : (a : ι') → ι) b)) → (a : ι) → α a) ⁻¹'
          Set.pi (α := α) univ s) :
      ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := fun (b : ι') ↦ α ((f : (a : ι') → ι) b)) fun (i' : ι') ↦ μ ((f : (a : ι') → ι) i') :
          (a : Set ((b : ι') → α ((f : (a : ι') → ι) b))) → ℝ≥0∞)
        ((⇑(Equiv.piCongrLeft α f) : (a : (a : ι') → α ((f : (a : ι') → ι) a)) → (b : ι) → α b) ⁻¹'
          Set.pi (α := α) univ s) :
      ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
rw₂ :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := fun (b : ι') ↦ α ((f : (a : ι') → ι) b)) fun (i' : ι') ↦ μ ((f : (a : ι') → ι) i') :
          (a : Set ((b : ι') → α ((f : (a : ι') → ι) b))) → ℝ≥0∞)
        (Set.pi (α := fun (i : ι') ↦ α ((f : (a : ι') → ι) i)) univ fun (i : ι') ↦ s ((f : (a : ι') → ι) i)) :
      ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
rw₃ :
  Eq (α := ℝ≥0∞)
    (∏ i : ι',
      ((μ ((f : (a : ι') → ι) i) : Measure (α ((f : (a : ι') → ι) i))) : (a : Set (α ((f : (a : ι') → ι) i))) → ℝ≥0∞)
        (s ((f : (a : ι') → ι) i)))
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i))
rw₄ rw₅ : Eq (α := ℝ≥0∞) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i)) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i))
⊢ Eq (α := ℝ≥0∞)
    ((Measure.map (α := (b : ι') → α ((f : (a : ι') → ι) b))
            (⇑(MeasurableEquiv.piCongrLeft α f) : (a : (b : ι') → α ((f : (a : ι') → ι) b)) → (a : ι) → α a)
            (Measure.pi (α := fun (b : ι') ↦ α ((f : (a : ι') → ι) b)) fun (i' : ι') ↦ μ ((f : (a : ι') → ι) i')) :
          (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ s) :
      ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
rw [MeasurableEquiv.map_apply, MeasurableEquiv.coe_piCongrLeft f,
      Equiv.piCongrLeft_preimage_univ_pi, pi_pi _ _, f.prod_comp (fun i => μ i (s i))]

Premises used: MeasurableEquiv.map_apply, Equiv.piCongrLeft_preimage_univ_pi, MeasurableEquiv.coe_piCongrLeft, Equiv.prod_comp, MeasureTheory.Measure.pi_pi, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
ι' : Type u_2
inst : Fintype ι
inst_1 : Fintype ι'
α : ι → Type u_4
f : ι' ≃ ι
inst_2 : (i : ι) → MeasureSpace (α i)
inst_3 : ∀ (i : ι), SigmaFinite.{u_4} (α := α i) (m0 := MeasureSpace.toMeasurableSpace) volume
⊢ MeasurePreserving (α := (b : ι') → α ((f : (a : ι') → ι) b)) (β := (a : ι) → α a)
    (⇑(MeasurableEquiv.piCongrLeft α f : ((b : ι') → α ((f : (a : ι') → ι) b)) ≃ᵐ ((a : ι) → α a)) :
      (a : (b : ι') → α ((f : (a : ι') → ι) b)) → (a : ι) → α a)
    volume volume

Tactic:
measurePreserving_piCongrLeft (fun _ ↦ volume) f

Premises used: MeasureTheory.measurePreserving_piCongrLeft, MeasureTheory.MeasureSpace.volume
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
ι' : Type u_2
inst : Fintype ι
inst_1 : Fintype ι'
e : ι ≃ ι'
β : ι' → Type u_4
inst_2 : (i : ι') → MeasurableSpace (β i)
μ : (i : ι') → Measure (β i)
inst_3 : ∀ (i : ι'), SigmaFinite (μ i)
⊢ map (α := (b : ι) → β ((e : (a : ι) → ι') b))
      (⇑(MeasurableEquiv.piCongrLeft (fun (i : ι') ↦ β i) e) :
        (a : (b : ι) → β ((e : (a : ι) → ι') b)) → (a : ι') → β a)
      (Measure.pi (α := fun (i : ι) ↦ β ((e : (a : ι) → ι') i)) fun (i : ι) ↦ μ ((e : (a : ι) → ι') i)) =
    Measure.pi (α := β) μ

Tactic:
(measurePreserving_piCongrLeft (α := fun i ↦ β i) μ e).map_eq

Premises used: MeasureTheory.measurePreserving_piCongrLeft, MeasureTheory.MeasurePreserving.map_eq
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst_3 : ∀ (i : γ), SigmaFinite (μ i)
inst_4 : ∀ (i : γ), SigmaFinite (ν i)
⊢ Eq (α := Measure ((γ → α) × (γ → β)))
    (Measure.map (α := γ → α × β)
      (⇑(MeasurableEquiv.arrowProdEquivProdArrow α β γ) : (a : γ → α × β) → (γ → α) × (γ → β))
      (Measure.pi (α := fun (a : γ) ↦ α × β) fun (i : γ) ↦ (μ i).prod (ν i)))
    (Measure.prod (Measure.pi (α := fun (i : γ) ↦ α) fun (i : γ) ↦ μ i)
      (Measure.pi (α := fun (a : γ) ↦ β) fun (i : γ) ↦ ν i))

Tactic:
(FiniteSpanningSetsIn.ext ?_ (isPiSystem_pi.prod isPiSystem_pi)
      ((FiniteSpanningSetsIn.pi fun i ↦ (μ i).toFiniteSpanningSetsIn).prod
      (FiniteSpanningSetsIn.pi (fun i ↦ (ν i).toFiniteSpanningSetsIn))) ?_).symm

Premises used: MeasureTheory.Measure.FiniteSpanningSetsIn.pi, IsPiSystem.prod, MeasureTheory.Measure.toFiniteSpanningSetsIn, isPiSystem_pi, Eq.symm, MeasureTheory.Measure.FiniteSpanningSetsIn.prod, MeasureTheory.Measure.FiniteSpanningSetsIn.ext