awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
inst_3 : (i : ι) → PartialOrder (α i)
inst_4 : ∀ (i : ι), NoAtoms (μ i)
f g : (i : ι) → α i
⊢ (Set.pi (α := α) univ fun (i : ι) ↦ Ico (f i) (g i)) =ᶠ[ae (Measure.pi (α := α) μ)] Icc f g
have rw : (Set.pi (α := α) univ fun (i : ι) ↦ Ico (f i) (g i)) =ᶠ[ae (Measure.pi (α := α) μ)]
  Set.pi (α := α) univ fun (i : ι) ↦ Icc (f i) (g i)
Tactic: rw [← pi_univ_Icc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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 : ι), IsLocallyFiniteMeasure (μ i)
⊢ IsLocallyFiniteMeasure (Measure.pi (α := α) μ)
have refine : ∀ (x : (i : ι) → α i), (Measure.pi (α := α) μ).FiniteAtFilter (𝓝 x)
Tactic: refine ⟨fun x => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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 : ι), IsLocallyFiniteMeasure (μ i)
x : (i : ι) → α i
⊢ (Measure.pi (α := α) μ).FiniteAtFilter (𝓝 x)
have choose : ∀ (s : (i : ι) → Set (α i)) (hxs : ∀ (i : ι), x i ∈ s i) (ho : ∀ (i : ι), IsOpen[inst_3 i] (s i))
  (hμ : ∀ (i : ι), LT.lt (α := ℝ≥0∞) ((μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)),
  (Measure.pi (α := α) μ).FiniteAtFilter (𝓝 x)
Tactic: choose s hxs ho hμ using fun i => (μ i).exists_isOpen_measure_lt_top (x i)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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 : ι), IsLocallyFiniteMeasure (μ i)
x : (i : ι) → α i
s : (i : ι) → Set (α i)
hxs : ∀ (i : ι), x i ∈ s i
ho : ∀ (i : ι), IsOpen[inst_3 i] (s i)
hμ : ∀ (i : ι), LT.lt (α := ℝ≥0∞) ((μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (Measure.pi (α := α) μ).FiniteAtFilter (𝓝 x)
have refine : LT.lt (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
  (∞ : ℝ≥0∞)
Tactic: refine ⟨pi univ s, set_pi_mem_nhds finite_univ fun i _ => IsOpen.mem_nhds (ho i) (hxs i), ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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 : ι), IsLocallyFiniteMeasure (μ i)
x : (i : ι) → α i
s : (i : ι) → Set (α i)
hxs : ∀ (i : ι), x i ∈ s i
ho : ∀ (i : ι), IsOpen[inst_3 i] (s i)
hμ : ∀ (i : ι), LT.lt (α := ℝ≥0∞) ((μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
have rw : LT.lt (α := ℝ≥0∞) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i)) ∞
Tactic: rw [pi_pi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι_1 : Type u_1
ι' : Type u_2
α : ι_1 → Type u_3
inst : Fintype ι_1
m : (i : ι_1) → OuterMeasure (α i)
inst_1 : (i : ι_1) → MeasurableSpace (α i)
μ_1 : (i : ι_1) → Measure (α i)
inst_2 : ∀ (i : ι_1), SigmaFinite (μ_1 i)
ι : Type u_4
inst_3 : Fintype ι
X : ι → Type u_5
inst_4 : (i : ι) → PseudoMetricSpace (X i)
inst_5 : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst_6 : ∀ (i : ι), SigmaFinite (μ i)
inst_7 : ∀ (i : ι), IsUnifLocDoublingMeasure (μ i)
⊢ IsUnifLocDoublingMeasure (Measure.pi (α := X) μ)
have h : ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
  ∀ (x : (i : ι) → X i),
    (Measure.pi (α := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (Metric.closedBall x (2 * ε)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑(∏ i : ι, IsUnifLocDoublingMeasure.doublingConstant (μ i)) : ℝ≥0∞)
        ((Measure.pi (α := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (Metric.closedBall x ε) : ℝ≥0∞)
Tactic: use ∏ i, IsUnifLocDoublingMeasure.doublingConstant (μ i)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι_1 : Type u_1
ι' : Type u_2
α : ι_1 → Type u_3
inst : Fintype ι_1
m : (i : ι_1) → OuterMeasure (α i)
inst_1 : (i : ι_1) → MeasurableSpace (α i)
μ_1 : (i : ι_1) → Measure (α i)
inst_2 : ∀ (i : ι_1), SigmaFinite (μ_1 i)
ι : Type u_4
inst_3 : Fintype ι
X : ι → Type u_5
inst_4 : (i : ι) → PseudoMetricSpace (X i)
inst_5 : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst_6 : ∀ (i : ι), SigmaFinite (μ i)
inst_7 : ∀ (i : ι), IsUnifLocDoublingMeasure (μ i)
r : ℝ
hr :
  ∀ (i : ι) (x : X i),
    (μ i : (a : Set (X i)) → ℝ≥0∞) (Metric.closedBall x (2 * r)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑(IsUnifLocDoublingMeasure.doublingConstant (μ i)) : ℝ≥0∞)
        ((μ i : (a : Set (X i)) → ℝ≥0∞) (Metric.closedBall x r) : ℝ≥0∞)
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) r →
    ∀ (x : (i : ι) → X i),
      (Measure.pi (α := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (Metric.closedBall x (2 * r)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑(∏ i : ι, IsUnifLocDoublingMeasure.doublingConstant (μ i)) : ℝ≥0∞)
          ((Measure.pi (α := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (Metric.closedBall x r) : ℝ≥0∞)
have h : ∀ (hr₀ : 0 < r) (x : (i : ι) → X i),
  (Measure.pi (α := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (Metric.closedBall x (2 * r)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(∏ i : ι, IsUnifLocDoublingMeasure.doublingConstant (μ i)) : ℝ≥0∞)
      ((Measure.pi (α := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (Metric.closedBall x r) : ℝ≥0∞)
Tactic: (hr₀ : 0 < r)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι_1 : Type u_1
ι' : Type u_2
α : ι_1 → Type u_3
inst : Fintype ι_1
m : (i : ι_1) → OuterMeasure (α i)
inst_1 : (i : ι_1) → MeasurableSpace (α i)
μ_1 : (i : ι_1) → Measure (α i)
inst_2 : ∀ (i : ι_1), SigmaFinite (μ_1 i)
ι : Type u_4
inst_3 : Fintype ι
X : ι → Type u_5
inst_4 : (i : ι) → PseudoMetricSpace (X i)
inst_5 : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst_6 : ∀ (i : ι), SigmaFinite (μ i)
inst_7 : ∀ (i : ι), IsUnifLocDoublingMeasure (μ i)
⊢ ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∀ (x : (i : ι) → X i),
      (Measure.pi (α := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (Metric.closedBall x (2 * ε)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑(∏ i : ι, IsUnifLocDoublingMeasure.doublingConstant (μ i)) : ℝ≥0∞)
          ((Measure.pi (α := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (Metric.closedBall x ε) : ℝ≥0∞)
have h : ∀ (r : ℝ)
  (hr :
    ∀ (i : ι) (x : X i),
      (μ i : (a : Set (X i)) → ℝ≥0∞) (Metric.closedBall x (2 * r)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑(IsUnifLocDoublingMeasure.doublingConstant (μ i)) : ℝ≥0∞)
          ((μ i : (a : Set (X i)) → ℝ≥0∞) (Metric.closedBall x r) : ℝ≥0∞))
  (hr₀ : 0 < r) (x : (i : ι) → X i),
  (Measure.pi (α := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (Metric.closedBall x (2 * r)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(∏ i : ι, IsUnifLocDoublingMeasure.doublingConstant (μ i)) : ℝ≥0∞)
      ((Measure.pi (α := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (Metric.closedBall x r) : ℝ≥0∞)
Tactic: filter_upwards [Filter.eventually_all.mpr fun i ↦
      IsUnifLocDoublingMeasure.eventually_measure_le_doublingConstant_mul (μ i),
    eventually_mem_nhdsWithin] with r hr (hr₀ : 0 < r) x
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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).IsMulLeftInvariant
⊢ (Measure.pi (α := α) μ).IsMulLeftInvariant
have refine : ∀ (v : (i : ι) → α i) (s : (i : ι) → Set (α i)) (hs : ∀ (i : ι), MeasurableSet (s i)),
  Eq (α := ℝ≥0∞)
    ((map (fun (x : (i : ι) → α i) ↦ v * x) (Measure.pi (α := α) μ) : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ s) :
      ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: refine ⟨fun v => (pi_eq fun s hs => ?_).symm⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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).IsMulLeftInvariant
v : (i : ι) → α i
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ Eq (α := ℝ≥0∞)
    ((map (fun (x : (i : ι) → α i) ↦ v * x) (Measure.pi (α := α) μ) : (a : Set ((i : ι) → α i)) → ℝ≥0∞)
        (Set.pi (α := α) univ s) :
      ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) ((fun (x : α i) ↦ v i * x) ⁻¹' s i))
  (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i))
Tactic: rw [map_apply (measurable_const_mul _) (MeasurableSet.univ_pi hs),
    show (v * ·) ⁻¹' univ.pi s = univ.pi fun i => (v i * ·) ⁻¹' s i by rfl, pi_pi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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
⊢ (Measure.pi (α := α) μ).IsMulRightInvariant
have 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∞)
Tactic: refine ⟨fun v => (pi_eq fun s hs => ?_).symm⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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∞)
    ((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∞)
have 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))
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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
have 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∞)
Tactic: refine ⟨(Measure.pi_eq fun s hs => ?_).symm⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (hypothesis)
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)
⊢ Eq (α := ℝ≥0∞) (((Measure.pi (α := α) μ).inv : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
have A : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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
⊢ Eq (α := ℝ≥0∞) (((Measure.pi (α := α) μ).inv : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
have 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∞)
Tactic: simp_rw [Measure.inv, Measure.map_apply measurable_inv (MeasurableSet.univ_pi hs), A, pi_pi,
    measure_preimage_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.pi (α := α) μ).inv : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
have 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∞)
Tactic: simp_rw [Measure.inv, Measure.map_apply measurable_inv (MeasurableSet.univ_pi hs), A, pi_pi,
    measure_preimage_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.pi (α := α) μ).inv : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
have 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∞)
Tactic: simp_rw [Measure.inv, Measure.map_apply measurable_inv (MeasurableSet.univ_pi hs), A, pi_pi,
    measure_preimage_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.pi (α := α) μ).inv : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
have simp_rw₃ : Eq (α := ℝ≥0∞) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (Inv.inv ⁻¹' s i))
  (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i))
Tactic: simp_rw [Measure.inv, Measure.map_apply measurable_inv (MeasurableSet.univ_pi hs), A, pi_pi,
    measure_preimage_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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
⊢ (Measure.pi (α := α) μ).IsOpenPosMeasure
have 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∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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
⊢ Ne (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
have 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∞)
Tactic: obtain ⟨s, ⟨hs, hsU⟩⟩ := isOpen_pi_iff'.1 U_open a ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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∞)
have open_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
  ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
Tactic: refine ne_of_gt (lt_of_lt_of_le ?_ (measure_mono hsU))
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
have open_pos : LT.lt (α := ℝ≥0∞) 0 (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i))
Tactic: simp only [pi_pi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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
⊢ LT.lt (α := ℝ≥0∞) 0 (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i))
have open_pos : ∀ (i : ι),
  Membership.mem (γ := Finset ι) Finset.univ i →
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: rw [CanonicallyOrderedAdd.prod_pos]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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)
⊢ IsFiniteMeasureOnCompacts (Measure.pi (α := α) μ)
have lt_top_of_isCompact : ∀ ⦃K : Set ((i : ι) → α i)⦄,
  IsCompact K → LT.lt (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: constructor