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)
inst_3 : (i : ι) → Group (α i)
inst_4 : ∀ (i : ι), MeasurableMul.{u_3} (α i)
inst_5 : ∀ (i : ι), (μ i).IsMulRightInvariant
refine :
  ∀ (v : (i : ι) → α i) (s : (i : ι) → Set (α i)) (hs : ∀ (i : ι), MeasurableSet (s i)),
    Eq (α := ℝ≥0∞)
      ((map (fun (x : (i : ι) → α i) ↦ x * v) (Measure.pi (α := α) μ) : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
          (Set.pi (α := α) univ s) :
        ℝ≥0∞)
      (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ (Measure.pi (α := α) μ).IsMulRightInvariant

Tactic:
refine ⟨fun v => (pi_eq fun s hs => ?_).symm⟩
-- 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)
inst_3 : (i : ι) → Group (α i)
inst_4 : ∀ (i : ι), MeasurableMul.{u_3} (α i)
inst_5 : ∀ (i : ι), (μ i).IsMulRightInvariant
v : (i : ι) → α i
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ Eq (α := Set ((i : ι) → α i)) ((fun (x : (i : ι) → α i) ↦ x * v) ⁻¹' Set.pi (α := α) univ s)
    (Set.pi (α := α) univ fun (i : ι) ↦ (fun (x : α i) ↦ x * v i) ⁻¹' s i)

Tactic:
rfl
-- 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)
inst_3 : (i : ι) → Group (α i)
inst_4 : ∀ (i : ι), MeasurableMul.{u_3} (α i)
inst_5 : ∀ (i : ι), (μ i).IsMulRightInvariant
v : (i : ι) → α i
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
rw :
  Eq (α := ℝ≥0∞) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) ((fun (x : α i) ↦ x * v i) ⁻¹' s i))
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i))
⊢ Eq (α := ℝ≥0∞)
    ((map (fun (x : (i : ι) → α i) ↦ x * v) (Measure.pi (α := α) μ) : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ s) :
      ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
rw [map_apply (measurable_mul_const _) (MeasurableSet.univ_pi hs),
    show (· * v) ⁻¹' univ.pi s = univ.pi fun i => (· * v i) ⁻¹' s i by rfl, pi_pi]

Premises used: MeasureTheory.Measure.map_apply, MeasurableMul.measurable_mul_const, MeasureTheory.Measure.pi_pi, MeasurableSet.univ_pi
-- 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)
inst_3 : (i : ι) → Group (α i)
inst_4 : ∀ (i : ι), MeasurableMul.{u_3} (α i)
inst_5 : ∀ (i : ι), (μ i).IsMulRightInvariant
v : (i : ι) → α i
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ Eq (α := ℝ≥0∞) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) ((fun (x : α i) ↦ x * v i) ⁻¹' s i))
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i))

Tactic:
simp_rw [measure_preimage_mul_right]

Premises used: MeasureTheory.measure_preimage_mul_right
-- 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 : ι), SigmaFinite.{u_4} (α := G i) (m0 := MeasureSpace.toMeasurableSpace) volume
inst_7 : ∀ (i : ι), IsMulRightInvariant.{u_4} (G := G i) volume
⊢ IsMulRightInvariant (G := (i : ι) → G i) volume

Tactic:
pi.isMulRightInvariant _

Premises used: MeasureTheory.Measure.pi.isMulRightInvariant
-- 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)
inst_3 : (i : ι) → Group (α i)
inst_4 : ∀ (i : ι), MeasurableInv.{u_3} (α i)
inst_5 : ∀ (i : ι), (μ i).IsInvInvariant
⊢ (Measure.pi (α := α) μ).IsInvInvariant

Tactic:
⟨(Measure.pi_eq fun s hs => ?_).symm⟩

Premises used: MeasureTheory.Measure.pi_eq, Eq.symm, MeasureTheory.Measure.IsInvInvariant.mk
-- 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)
inst_3 : (i : ι) → Group (α i)
inst_4 : ∀ (i : ι), MeasurableInv.{u_3} (α i)
inst_5 : ∀ (i : ι), (μ i).IsInvInvariant
refine :
  ∀ (s : (i : ι) → Set (α i)) (hs : ∀ (i : ι), MeasurableSet (s i)),
    Eq (α := ℝ≥0∞) (((Measure.pi (α := α) μ).inv : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
      (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ (Measure.pi (α := α) μ).IsInvInvariant

Tactic:
refine ⟨(Measure.pi_eq fun s hs => ?_).symm⟩
-- 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)
inst_3 : (i : ι) → Group (α i)
inst_4 : ∀ (i : ι), MeasurableInv.{u_3} (α i)
inst_5 : ∀ (i : ι), (μ i).IsInvInvariant
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
h :
  ∀ (x : (i : ι) → α i),
    x ∈ Inv.inv ⁻¹' Set.pi (α := α) univ s ↔
      Membership.mem (γ := Set ((i : ι) → α i)) (Set.pi (α := α) univ fun (i : ι) ↦ Inv.inv ⁻¹' s i) x
⊢ Inv.inv ⁻¹' Set.pi (α := α) univ s = Set.pi (α := α) univ fun (i : ι) ↦ Inv.inv ⁻¹' s i

Tactic:
ext
-- 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)
inst_3 : (i : ι) → Group (α i)
inst_4 : ∀ (i : ι), MeasurableInv.{u_3} (α i)
inst_5 : ∀ (i : ι), (μ i).IsInvInvariant
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
x : (i : ι) → α i
⊢ x ∈ Inv.inv ⁻¹' Set.pi (α := α) univ s ↔
    Membership.mem (γ := Set ((i : ι) → α i)) (Set.pi (α := α) univ fun (i : ι) ↦ Inv.inv ⁻¹' s i) x

Tactic:
simp
-- 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)
inst_3 : (i : ι) → Group (α i)
inst_4 : ∀ (i : ι), MeasurableInv.{u_3} (α i)
inst_5 : ∀ (i : ι), (μ i).IsInvInvariant
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ Inv.inv ⁻¹' Set.pi (α := α) univ s = Set.pi (α := α) univ fun (i : ι) ↦ Inv.inv ⁻¹' s i

Tactic:
have A : Inv.inv ⁻¹' pi univ s = Set.pi univ fun i => Inv.inv ⁻¹' s i := by ext; simp
-- 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)
inst_3 : (i : ι) → Group (α i)
inst_4 : ∀ (i : ι), MeasurableInv.{u_3} (α i)
inst_5 : ∀ (i : ι), (μ i).IsInvInvariant
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
A : Inv.inv ⁻¹' Set.pi (α := α) univ s = Set.pi (α := α) univ fun (i : ι) ↦ Inv.inv ⁻¹' s i
simp_rw :
  Eq (α := ℝ≥0∞)
    ((map Inv.inv (Measure.pi (α := α) μ) : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
simp_rw₁ :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Inv.inv ⁻¹' Set.pi (α := α) univ s) : ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
simp_rw₂ :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ fun (i : ι) ↦ Inv.inv ⁻¹' s i) :
      ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
simp_rw₃ :
  Eq (α := ℝ≥0∞) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (Inv.inv ⁻¹' s i))
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i))
⊢ Eq (α := ℝ≥0∞) (((Measure.pi (α := α) μ).inv : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
simp_rw [Measure.inv, Measure.map_apply measurable_inv (MeasurableSet.univ_pi hs), A, pi_pi,
    measure_preimage_inv]

Premises used: MeasureTheory.Measure.map_apply, MeasurableInv.measurable_inv, MeasureTheory.Measure.inv, MeasureTheory.Measure.measure_preimage_inv, MeasureTheory.Measure.pi_pi, MeasurableSet.univ_pi
-- 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 : ι), MeasurableInv.{u_4} (G i)
inst_6 : ∀ (i : ι), SigmaFinite.{u_4} (α := G i) (m0 := MeasureSpace.toMeasurableSpace) volume
inst_7 : ∀ (i : ι), IsInvInvariant.{u_4} (G := G i) volume
⊢ IsInvInvariant (G := (i : ι) → G i) volume

Tactic:
pi.isInvInvariant _

Premises used: MeasureTheory.Measure.pi.isInvInvariant
-- 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)
inst_3 : (i : ι) → TopologicalSpace (α i)
inst_4 : ∀ (i : ι), (μ i).IsOpenPosMeasure
open_pos :
  ∀ (U : Set ((i : ι) → α i)),
    IsOpen[Pi.topologicalSpace] U →
      U.Nonempty → Ne (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (Measure.pi (α := α) μ).IsOpenPosMeasure

Tactic:
constructor
-- 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)
inst_3 : (i : ι) → TopologicalSpace (α i)
inst_4 : ∀ (i : ι), (μ i).IsOpenPosMeasure
U : Set ((i : ι) → α i)
U_open : IsOpen[Pi.topologicalSpace] U
a : (i : ι) → α i
ha : a ∈ U
open_pos :
  ∀ (s : (a : ι) → Set (α a)) (hs : ∀ (a_1 : ι), IsOpen[inst_3 a_1] (s a_1) ∧ a a_1 ∈ s a_1)
    (hsU : Set.pi (α := α) univ s ⊆ U),
    Ne (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
obtain ⟨s, ⟨hs, hsU⟩⟩ := isOpen_pi_iff'.1 U_open a ha

Premises used: isOpen_pi_iff', Iff.mp
-- 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)
inst_3 : (i : ι) → TopologicalSpace (α i)
inst_4 : ∀ (i : ι), (μ i).IsOpenPosMeasure
U : Set ((i : ι) → α i)
U_open : IsOpen[Pi.topologicalSpace] U
a : (i : ι) → α i
ha : a ∈ U
s : (a : ι) → Set (α a)
hs : ∀ (a_1 : ι), IsOpen[inst_3 a_1] (s a_1) ∧ a a_1 ∈ s a_1
hsU : Set.pi (α := α) univ s ⊆ U
⊢ Ne (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
ne_of_gt (lt_of_lt_of_le ?_ (measure_mono hsU))

Premises used: ne_of_gt, MeasureTheory.measure_mono, lt_of_lt_of_le
-- 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)
inst_3 : (i : ι) → TopologicalSpace (α i)
inst_4 : ∀ (i : ι), (μ i).IsOpenPosMeasure
U : Set ((i : ι) → α i)
U_open : IsOpen[Pi.topologicalSpace] U
a : (i : ι) → α i
ha : a ∈ U
s : (a : ι) → Set (α a)
hs : ∀ (a_1 : ι), IsOpen[inst_3 a_1] (s a_1) ∧ a a_1 ∈ s a_1
hsU : Set.pi (α := α) univ s ⊆ U
open_pos :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
refine ne_of_gt (lt_of_lt_of_le ?_ (measure_mono hsU))

Premises used: ne_of_gt, MeasureTheory.measure_mono, lt_of_lt_of_le
-- 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)
inst_3 : (i : ι) → TopologicalSpace (α i)
inst_4 : ∀ (i : ι), (μ i).IsOpenPosMeasure
U : Set ((i : ι) → α i)
U_open : IsOpen[Pi.topologicalSpace] U
a : (i : ι) → α i
ha : a ∈ U
s : (a : ι) → Set (α a)
hs : ∀ (a_1 : ι), IsOpen[inst_3 a_1] (s a_1) ∧ a a_1 ∈ s a_1
hsU : Set.pi (α := α) univ s ⊆ U
open_pos : LT.lt (α := ℝ≥0∞) 0 (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i))
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)

Tactic:
simp only [pi_pi]

Premises used: MeasureTheory.Measure.pi_pi
-- 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)
inst_3 : (i : ι) → TopologicalSpace (α i)
inst_4 : ∀ (i : ι), (μ i).IsOpenPosMeasure
U : Set ((i : ι) → α i)
U_open : IsOpen[Pi.topologicalSpace] U
a : (i : ι) → α i
ha : a ∈ U
s : (a : ι) → Set (α a)
hs : ∀ (a_1 : ι), IsOpen[inst_3 a_1] (s a_1) ∧ a a_1 ∈ s a_1
hsU : Set.pi (α := α) univ s ⊆ U
open_pos :
  ∀ (i : ι),
    Membership.mem (γ := Finset ι) Finset.univ i →
      LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) 0 (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i))

Tactic:
rw [CanonicallyOrderedAdd.prod_pos]

Premises used: CanonicallyOrderedAdd.prod_pos
-- 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)
inst_3 : (i : ι) → TopologicalSpace (α i)
inst_4 : ∀ (i : ι), (μ i).IsOpenPosMeasure
U : Set ((i : ι) → α i)
U_open : IsOpen[Pi.topologicalSpace] U
a : (i : ι) → α i
ha : a ∈ U
s : (a : ι) → Set (α a)
hs : ∀ (a_1 : ι), IsOpen[inst_3 a_1] (s a_1) ∧ a a_1 ∈ s a_1
hsU : Set.pi (α := α) univ s ⊆ U
i : ι
open_pos :
  Membership.mem (γ := Finset ι) Finset.univ i →
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ Membership.mem (γ := Finset ι) Finset.univ i →
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
_
-- 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)
inst_3 : (i : ι) → TopologicalSpace (α i)
inst_4 : ∀ (i : ι), (μ i).IsOpenPosMeasure
U : Set ((i : ι) → α i)
U_open : IsOpen[Pi.topologicalSpace] U
a : (i : ι) → α i
ha : a ∈ U
s : (a : ι) → Set (α a)
hs : ∀ (a_1 : ι), IsOpen[inst_3 a_1] (s a_1) ∧ a a_1 ∈ s a_1
hsU : Set.pi (α := α) univ s ⊆ U
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
apply (hs i).1.measure_pos (μ i) ⟨a i, (hs i).2⟩

Premises used: IsOpen.measure_pos, And.right, And.left, Exists.intro
-- 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)
X : ι → Type u_4
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : (i : ι) → MeasureSpace (X i)
inst_5 : ∀ (i : ι), IsOpenPosMeasure.{u_4} (X := X i) (m := MeasureSpace.toMeasurableSpace) volume
inst_6 : ∀ (i : ι), SigmaFinite.{u_4} (α := X i) (m0 := MeasureSpace.toMeasurableSpace) volume
⊢ IsOpenPosMeasure (X := (i : ι) → X i) (m := MeasureSpace.toMeasurableSpace) volume

Tactic:
pi.isOpenPosMeasure _

Premises used: MeasureTheory.Measure.pi.isOpenPosMeasure
-- 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)
inst_3 : (i : ι) → TopologicalSpace (α i)
inst_4 : ∀ (i : ι), IsFiniteMeasureOnCompacts (μ i)
lt_top_of_isCompact :
  ∀ ⦃K : Set ((i : ι) → α i)⦄,
    IsCompact K → LT.lt (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IsFiniteMeasureOnCompacts (Measure.pi (α := α) μ)

Tactic:
constructor
-- 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)
inst_3 : (i : ι) → TopologicalSpace (α i)
inst_4 : ∀ (i : ι), IsFiniteMeasureOnCompacts (μ i)
K : Set ((i : ι) → α i)
hK : IsCompact K
this :
  LT.lt (α := ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ fun (j : ι) ↦ eval (β := α) j '' K) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
lt_of_le_of_lt (measure_mono (univ.subset_pi_eval_image K)) this

Premises used: lt_of_le_of_lt, Set.univ, MeasureTheory.measure_mono, Set.subset_pi_eval_image
-- 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)
inst_3 : (i : ι) → TopologicalSpace (α i)
inst_4 : ∀ (i : ι), IsFiniteMeasureOnCompacts (μ i)
K : Set ((i : ι) → α i)
hK : IsCompact K
this :
  LT.lt (α := ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ fun (j : ι) ↦ eval (β := α) j '' K) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact lt_of_le_of_lt (measure_mono (univ.subset_pi_eval_image K)) this

Premises used: lt_of_le_of_lt, Set.univ, MeasureTheory.measure_mono, Set.subset_pi_eval_image
-- 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)
inst_3 : (i : ι) → TopologicalSpace (α i)
inst_4 : ∀ (i : ι), IsFiniteMeasureOnCompacts (μ i)
K : Set ((i : ι) → α i)
hK : IsCompact K
lt_top_of_isCompact :
  LT.lt (α := ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ fun (j : ι) ↦ eval (β := α) j '' K) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
suffices Measure.pi μ (Set.univ.pi fun j => Function.eval j '' K) < ⊤ by
    exact lt_of_le_of_lt (measure_mono (univ.subset_pi_eval_image K)) this
-- 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)
inst_3 : (i : ι) → TopologicalSpace (α i)
inst_4 : ∀ (i : ι), IsFiniteMeasureOnCompacts (μ i)
K : Set ((i : ι) → α i)
hK : IsCompact K
lt_top_of_isCompact : LT.lt (α := ℝ≥0∞) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (eval (β := α) i '' K)) ∞
⊢ LT.lt (α := ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ fun (j : ι) ↦ eval (β := α) j '' K) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
rw [Measure.pi_pi]

Premises used: MeasureTheory.Measure.pi_pi
-- 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)
inst_3 : (i : ι) → TopologicalSpace (α i)
inst_4 : ∀ (i : ι), IsFiniteMeasureOnCompacts (μ i)
K : Set ((i : ι) → α i)
hK : IsCompact K
⊢ LT.lt (α := ℝ≥0∞) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (eval (β := α) i '' K)) ∞

Tactic:
WithTop.prod_lt_top ?_

Premises used: WithTop.prod_lt_top, ENNReal.ofNNReal, ENNReal
-- 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)
inst_3 : (i : ι) → TopologicalSpace (α i)
inst_4 : ∀ (i : ι), IsFiniteMeasureOnCompacts (μ i)
K : Set ((i : ι) → α i)
hK : IsCompact K
lt_top_of_isCompact :
  ∀ (i : ι),
    Membership.mem (γ := Finset ι) Finset.univ i →
      LT.lt (α := WithTop NNReal) ((μ i : (a : Set (α i)) → ℝ≥0∞) (eval (β := α) i '' K) : ℝ≥0∞) (⊤ : WithTop NNReal)
⊢ LT.lt (α := ℝ≥0∞) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (eval (β := α) i '' K)) ∞

Tactic:
refine WithTop.prod_lt_top ?_

Premises used: WithTop.prod_lt_top
-- 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)
inst_3 : (i : ι) → TopologicalSpace (α i)
inst_4 : ∀ (i : ι), IsFiniteMeasureOnCompacts (μ i)
K : Set ((i : ι) → α i)
hK : IsCompact K
⊢ ∀ (i : ι),
    Membership.mem (γ := Finset ι) Finset.univ i →
      LT.lt (α := WithTop NNReal) ((μ i : (a : Set (α i)) → ℝ≥0∞) (eval (β := α) i '' K) : ℝ≥0∞) (⊤ : WithTop NNReal)

Tactic:
fun i _ => IsCompact.measure_lt_top (IsCompact.image hK (continuous_apply i))

Premises used: IsCompact.measure_lt_top, continuous_apply, IsCompact.image
-- 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)
inst_3 : (i : ι) → TopologicalSpace (α i)
inst_4 : ∀ (i : ι), IsFiniteMeasureOnCompacts (μ i)
K : Set ((i : ι) → α i)
hK : IsCompact K
⊢ ∀ (i : ι),
    Membership.mem (γ := Finset ι) Finset.univ i →
      LT.lt (α := WithTop NNReal) ((μ i : (a : Set (α i)) → ℝ≥0∞) (eval (β := α) i '' K) : ℝ≥0∞) (⊤ : WithTop NNReal)

Tactic:
exact fun i _ => IsCompact.measure_lt_top (IsCompact.image hK (continuous_apply i))

Premises used: IsCompact.measure_lt_top, continuous_apply, IsCompact.image
-- 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)
X : ι → Type u_4
inst_3 : (i : ι) → MeasureSpace (X i)
inst_4 : (i : ι) → TopologicalSpace (X i)
inst_5 : ∀ (i : ι), SigmaFinite.{u_4} (α := X i) (m0 := MeasureSpace.toMeasurableSpace) volume
inst_6 : ∀ (i : ι), IsFiniteMeasureOnCompacts.{u_4} (α := X i) (m0 := MeasureSpace.toMeasurableSpace) volume
⊢ IsFiniteMeasureOnCompacts (α := (i : ι) → X i) (m0 := MeasureSpace.toMeasurableSpace) volume

Tactic:
pi.isFiniteMeasureOnCompacts _

Premises used: MeasureTheory.Measure.pi.isFiniteMeasureOnCompacts