awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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)
s : Set ι
f g : (i : ι) → α i
⊢ (s.pi (α := α) fun (i : ι) ↦ Ioc (f i) (g i)) =ᶠ[ae (Measure.pi (α := α) μ)]
    s.pi (α := α) fun (i : ι) ↦ Icc (f i) (g i)

Tactic:
ae_eq_set_pi fun _ _ => Ioc_ae_eq_Icc

Premises used: MeasureTheory.Ioc_ae_eq_Icc, MeasureTheory.Measure.ae_eq_set_pi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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
rw :
  (Set.pi (α := α) univ fun (i : ι) ↦ Ioc (f i) (g i)) =ᶠ[ae (Measure.pi (α := α) μ)]
    Set.pi (α := α) univ fun (i : ι) ↦ Icc (f i) (g i)
⊢ (Set.pi (α := α) univ fun (i : ι) ↦ Ioc (f i) (g i)) =ᶠ[ae (Measure.pi (α := α) μ)] Icc f g

Tactic:
rw [← pi_univ_Icc]

Premises used: Set.pi_univ_Icc
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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 : ι) ↦ Ioc (f i) (g i)) =ᶠ[ae (Measure.pi (α := α) μ)]
    Set.pi (α := α) univ fun (i : ι) ↦ Icc (f i) (g i)

Tactic:
pi_Ioc_ae_eq_pi_Icc

Premises used: MeasureTheory.Measure.pi_Ioc_ae_eq_pi_Icc
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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 : ι) ↦ Ioc (f i) (g i)) =ᶠ[ae (Measure.pi (α := α) μ)]
    Set.pi (α := α) univ fun (i : ι) ↦ Icc (f i) (g i)

Tactic:
exact pi_Ioc_ae_eq_pi_Icc

Premises used: MeasureTheory.Measure.pi_Ioc_ae_eq_pi_Icc
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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)
s : Set ι
f g : (i : ι) → α i
⊢ (s.pi (α := α) fun (i : ι) ↦ Ico (f i) (g i)) =ᶠ[ae (Measure.pi (α := α) μ)]
    s.pi (α := α) fun (i : ι) ↦ Icc (f i) (g i)

Tactic:
ae_eq_set_pi fun _ _ => Ico_ae_eq_Icc

Premises used: MeasureTheory.Measure.ae_eq_set_pi, MeasureTheory.Ico_ae_eq_Icc
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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
rw :
  (Set.pi (α := α) univ fun (i : ι) ↦ Ico (f i) (g i)) =ᶠ[ae (Measure.pi (α := α) μ)]
    Set.pi (α := α) univ fun (i : ι) ↦ Icc (f i) (g i)
⊢ (Set.pi (α := α) univ fun (i : ι) ↦ Ico (f i) (g i)) =ᶠ[ae (Measure.pi (α := α) μ)] Icc f g

Tactic:
rw [← pi_univ_Icc]

Premises used: Set.pi_univ_Icc
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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 (α := α) μ)]
    Set.pi (α := α) univ fun (i : ι) ↦ Icc (f i) (g i)

Tactic:
pi_Ico_ae_eq_pi_Icc

Premises used: MeasureTheory.Measure.pi_Ico_ae_eq_pi_Icc
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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 (α := α) μ)]
    Set.pi (α := α) univ fun (i : ι) ↦ Icc (f i) (g i)

Tactic:
exact pi_Ico_ae_eq_pi_Icc

Premises used: MeasureTheory.Measure.pi_Ico_ae_eq_pi_Icc
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
i : ι
inst_3 : NoAtoms (μ i)
⊢ NoAtoms (Measure.pi (α := α) μ)

Tactic:
⟨fun x => flip measure_mono_null (pi_hyperplane μ i (x i)) (singleton_subset_iff.2 rfl)⟩

Premises used: Iff.mpr, Set.singleton_subset_iff, MeasureTheory.Measure.pi_hyperplane, MeasureTheory.NoAtoms.mk, flip, MeasureTheory.measure_mono_null, 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)
h : Nonempty ι
inst_3 : ∀ (i : ι), NoAtoms (μ i)
⊢ NoAtoms (Measure.pi (α := α) μ)

Tactic:
h.elim fun i => pi_noAtoms i

Premises used: MeasureTheory.Measure.pi_noAtoms, Nonempty.elim
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
ι' : Type u_2
α_1 : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α_1 i)
inst_1 : (i : ι) → MeasurableSpace (α_1 i)
μ : (i : ι) → Measure (α_1 i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
α : ι → Type u_4
inst_3 : Nonempty ι
inst_4 : (i : ι) → MeasureSpace (α i)
inst_5 : ∀ (i : ι), SigmaFinite.{u_4} (α := α i) (m0 := MeasureSpace.toMeasurableSpace) volume
inst_6 : ∀ (i : ι), NoAtoms.{u_4} (α := α i) (m0 := MeasureSpace.toMeasurableSpace) volume
⊢ NoAtoms (α := (i : ι) → α i) (m0 := MeasureSpace.toMeasurableSpace) volume

Tactic:
pi_noAtoms'

Premises used: MeasureTheory.Measure.pi_noAtoms'
-- 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 : ι), IsLocallyFiniteMeasure (μ i)
⊢ IsLocallyFiniteMeasure (Measure.pi (α := α) μ)

Tactic:
⟨fun x => ?_⟩

Premises used: MeasureTheory.IsLocallyFiniteMeasure.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 : ι) → TopologicalSpace (α i)
inst_4 : ∀ (i : ι), IsLocallyFiniteMeasure (μ i)
refine : ∀ (x : (i : ι) → α i), (Measure.pi (α := α) μ).FiniteAtFilter (𝓝 x)
⊢ IsLocallyFiniteMeasure (Measure.pi (α := α) μ)

Tactic:
refine ⟨fun x => ?_⟩
-- 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 : ι), IsLocallyFiniteMeasure (μ i)
x : (i : ι) → α i
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)
⊢ (Measure.pi (α := α) μ).FiniteAtFilter (𝓝 x)

Tactic:
choose s hxs ho hμ using fun i => (μ i).exists_isOpen_measure_lt_top (x i)

Premises used: MeasureTheory.Measure.exists_isOpen_measure_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 : ι), 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)

Tactic:
⟨pi univ s, set_pi_mem_nhds finite_univ fun i _ => IsOpen.mem_nhds (ho i) (hxs i), ?_⟩

Premises used: set_pi_mem_nhds, Set.univ, MeasureTheory.Measure.FiniteAtFilter, Set.finite_univ, And.intro, IsOpen.mem_nhds, Exists.intro, Set.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 : ι), 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∞)
refine :
  LT.lt (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ (Measure.pi (α := α) μ).FiniteAtFilter (𝓝 x)

Tactic:
refine ⟨pi univ s, set_pi_mem_nhds finite_univ fun i _ => IsOpen.mem_nhds (ho i) (hxs i), ?_⟩
-- 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 : ι), 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∞)
rw : LT.lt (α := ℝ≥0∞) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i)) ∞
⊢ LT.lt (α := ℝ≥0∞) ((Measure.pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
rw [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 : ι), 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∞) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i)) ∞

Tactic:
ENNReal.prod_lt_top fun i _ => hμ i

Premises used: ENNReal.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 : ι), 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∞) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0∞) (s i)) ∞

Tactic:
exact ENNReal.prod_lt_top fun i _ => hμ i

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

Tactic:
pi.isLocallyFiniteMeasure

Premises used: MeasureTheory.Measure.pi.isLocallyFiniteMeasure
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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)
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∞)
⊢ IsUnifLocDoublingMeasure (Measure.pi (α := X) μ)

Tactic:
use ∏ i, IsUnifLocDoublingMeasure.doublingConstant (μ i)
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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∞)
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∞)
⊢ 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∞)

Tactic:
(hr₀ : 0 < r)
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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)
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∞)
⊢ ∀ᶠ (ε : ℝ) 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:
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

Premises used: Iff.mpr, eventually_mem_nhdsWithin, Filter.eventually_all, IsUnifLocDoublingMeasure.eventually_measure_le_doublingConstant_mul
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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∞)
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:
simpa (disch := positivity) [Finset.prod_mul_distrib, closedBall_pi, pi_pi]
    using Fintype.prod_mono' fun i ↦ hr i (x i)

Premises used: Finset.prod_mul_distrib, Fintype.prod_mono', closedBall_pi, MeasureTheory.Measure.pi_pi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
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)
μ : (i : ι_1) → Measure (α i)
inst_2 : ∀ (i : ι_1), SigmaFinite (μ i)
ι : Type u_4
inst_3 : Fintype ι
X : ι → Type u_5
inst_4 : (i : ι) → PseudoMetricSpace (X i)
inst_5 : (i : ι) → MeasureSpace (X i)
inst_6 : ∀ (i : ι), SigmaFinite.{u_5} (α := X i) (m0 := MeasureSpace.toMeasurableSpace) volume
inst_7 : ∀ (i : ι), IsUnifLocDoublingMeasure.{u_5} (α := X i) volume
⊢ IsUnifLocDoublingMeasure (α := (i : ι) → X i) volume

Tactic:
.pi _

Premises used: IsUnifLocDoublingMeasure.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).IsMulLeftInvariant
⊢ (Measure.pi (α := α) μ).IsMulLeftInvariant

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

Premises used: MeasureTheory.Measure.IsMulLeftInvariant.mk, 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 : ι) → 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
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∞)
⊢ (Measure.pi (α := α) μ).IsMulLeftInvariant

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).IsMulLeftInvariant
v : (i : ι) → α i
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ Eq (α := Set ((i : ι) → α i)) ((fun (x : (i : ι) → α i) ↦ v * x) ⁻¹' Set.pi (α := α) univ s)
    (Set.pi (α := α) univ fun (i : ι) ↦ (fun (x : α i) ↦ v i * x) ⁻¹' 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).IsMulLeftInvariant
v : (i : ι) → α i
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
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))
⊢ 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:
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]

Premises used: MeasureTheory.Measure.map_apply, MeasurableMul.measurable_const_mul, 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).IsMulLeftInvariant
v : (i : ι) → α i
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ 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:
simp_rw [measure_preimage_mul]

Premises used: MeasureTheory.measure_preimage_mul
-- 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 : ι), IsMulLeftInvariant.{u_4} (G := G i) volume
⊢ IsMulLeftInvariant (G := (i : ι) → G i) volume

Tactic:
pi.isMulLeftInvariant _

Premises used: MeasureTheory.Measure.pi.isMulLeftInvariant
-- 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
⊢ (Measure.pi (α := α) μ).IsMulRightInvariant

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

Premises used: MeasureTheory.Measure.IsMulRightInvariant.mk, MeasureTheory.Measure.pi_eq, Eq.symm