awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : Nontrivial E
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : BorelSpace E
inst_8 : μ.IsAddHaarMeasure
f : ℝ → F
rw : Eq.{u_2 + 1} (α := F) (∫ (x : E), f ‖x‖ ∂μ) (∫ (x : E) in {0}ᶜ, f ‖x‖ ∂μ)
rw₁ rw₂ : Eq.{u_2 + 1} (α := F) (∫ (x : E), f ‖x‖ ∂μ) (∫ (x : E), f ‖x‖ ∂μ)
⊢ Eq.{u_2 + 1} (α := F) (∫ (x : E), f ‖x‖ ∂μ)
    (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
      (Measure.comap (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x)) μ)
      fun (x : (↑{0}ᶜ : Type u_1)) ↦ f ‖(↑x : E)‖)

Tactic:
rw [integral_subtype_comap (measurableSet_singleton _).compl fun x ↦ f (‖x‖),
        restrict_compl_singleton]

Premises used: Norm.norm, MeasureTheory.restrict_compl_singleton, MeasurableSingletonClass.measurableSet_singleton, MeasurableSet.compl, MeasureTheory.integral_subtype_comap
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : Nontrivial E
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : BorelSpace E
inst_8 : μ.IsAddHaarMeasure
f : ℝ → F
⊢ Eq.{u_2 + 1} (α := F)
    (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
      (Measure.comap (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x)) μ)
      fun (x : (↑{0}ᶜ : Type u_1)) ↦ f ‖(↑x : E)‖)
    (∫ (x : (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type)),
      f (↑x.2 : ℝ) ∂Measure.prod μ.toSphere (Measure.volumeIoiPow (dim E - 1)))

Tactic:
simpa using μ.measurePreserving_homeomorphUnitSphereProd.integral_comp
        (Homeomorph.measurableEmbedding _) (f ∘ Subtype.val ∘ Prod.snd)

Premises used: MeasureTheory.MeasurePreserving.integral_comp, Homeomorph.measurableEmbedding, Function.comp, MeasureTheory.Measure.measurePreserving_homeomorphUnitSphereProd, Subtype.val, Prod.snd
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : Nontrivial E
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : BorelSpace E
inst_8 : μ.IsAddHaarMeasure
f : ℝ → F
simp :
  HSMul.hSMul (β := F) (Measure.real (α := (↑(sphere 0 1) : Type u_1)) μ.toSphere univ)
      (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x))
        (Measure.withDensity
          (Measure.comap (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x)) volume)
          fun (r : (↑(Ioi 0) : Type)) ↦ (↑((↑r : ℝ) ^ (dim E - 1)).toNNReal : ℝ≥0∞))
        fun (x : (↑(Ioi 0) : Type)) ↦ f (↑x : ℝ)) =
    dim E •
      HSMul.hSMul (β := F) (μ.real (ball 0 1))
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (y : ℝ) ↦
          y ^ (dim E - 1) • f y)
⊢ HSMul.hSMul (β := F) (Measure.real (α := (↑(sphere 0 1) : Type u_1)) μ.toSphere univ)
      (∫ (x : (↑(Ioi 0) : Type)), f (↑x : ℝ) ∂Measure.volumeIoiPow (dim E - 1)) =
    dim E •
      HSMul.hSMul (β := F) (μ.real (ball 0 1))
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (y : ℝ) ↦
          y ^ (dim E - 1) • f y)

Tactic:
simp only [Measure.volumeIoiPow, ENNReal.ofReal]

Premises used: ENNReal.ofReal, MeasureTheory.Measure.volumeIoiPow
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : Nontrivial E
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : BorelSpace E
inst_8 : μ.IsAddHaarMeasure
f : ℝ → F
rw : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x), (x ^ (dim E - 1)).toNNReal • f x = x ^ (dim E - 1) • f x
f_meas : Measurable (β := ℝ≥0) fun (r : (↑(Ioi 0) : Type)) ↦ ((↑r : ℝ) ^ (dim E - 1)).toNNReal
⊢ HSMul.hSMul (β := F) (Measure.real (α := (↑(sphere 0 1) : Type u_1)) μ.toSphere univ)
      (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x))
        (Measure.withDensity
          (Measure.comap (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x)) volume)
          fun (r : (↑(Ioi 0) : Type)) ↦ (↑((↑r : ℝ) ^ (dim E - 1)).toNNReal : ℝ≥0∞))
        fun (x : (↑(Ioi 0) : Type)) ↦ f (↑x : ℝ)) =
    dim E •
      HSMul.hSMul (β := F) (μ.real (ball 0 1))
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (y : ℝ) ↦
          y ^ (dim E - 1) • f y)

Tactic:
rw [integral_withDensity_eq_integral_smul, μ.toSphere_real_apply_univ,
        ← nsmul_eq_mul, smul_assoc,
        integral_subtype_comap measurableSet_Ioi fun a ↦ Real.toNNReal (a ^ (dim E - 1)) • f a,
        setIntegral_congr_fun measurableSet_Ioi fun x hx ↦ ?_]

Premises used: Real, MeasureTheory.Measure.toSphere_real_apply_univ, smul_assoc, integral_withDensity_eq_integral_smul, HSub.hSub, measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun, HPow.hPow, MeasureTheory.integral_subtype_comap, nsmul_eq_mul, HSMul.hSMul, OfNat.ofNat, Module.finrank, Real.toNNReal
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : Nontrivial E
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : BorelSpace E
inst_8 : μ.IsAddHaarMeasure
f : ℝ → F
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
rw : (↑(x ^ (dim E - 1)).toNNReal : ℝ) • f x = x ^ (dim E - 1) • f x
rw₁ rw₂ : x ^ (dim E - 1) • f x = x ^ (dim E - 1) • f x
⊢ (x ^ (dim E - 1)).toNNReal • f x = x ^ (dim E - 1) • f x

Tactic:
rw [NNReal.smul_def, Real.coe_toNNReal _ (pow_nonneg hx.out.le _)]

Premises used: Membership.mem.out, pow_nonneg, LT.lt.le, Real.coe_toNNReal, NNReal.smul_def
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : Nontrivial E
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : BorelSpace E
inst_8 : μ.IsAddHaarMeasure
f : ℝ → F
⊢ Measurable (β := ℝ≥0) fun (r : (↑(Ioi 0) : Type)) ↦ ((↑r : ℝ) ^ (dim E - 1)).toNNReal

Tactic:
(measurable_subtype_coe.pow_const _).real_toNNReal

Premises used: measurable_subtype_coe, Measurable.real_toNNReal, Measurable.pow_const
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : Nontrivial E
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : BorelSpace E
inst_8 : μ.IsAddHaarMeasure
f : ℝ → F
⊢ Measurable (β := ℝ≥0) fun (r : (↑(Ioi 0) : Type)) ↦ ((↑r : ℝ) ^ (dim E - 1)).toNNReal

Tactic:
exact (measurable_subtype_coe.pow_const _).real_toNNReal

Premises used: measurable_subtype_coe, Measurable.real_toNNReal, Measurable.pow_const
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
hs : (Set.pi (α := α) univ s).Nonempty
⊢ piPremeasure (α := α) m (Set.pi (α := α) univ s) = ∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i)

Tactic:
simp [hs, piPremeasure]

Premises used: MeasureTheory.piPremeasure
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
inl : IsEmpty ι → piPremeasure (α := α) m (Set.pi (α := α) univ s) = ∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i)
inr : Nonempty ι → piPremeasure (α := α) m (Set.pi (α := α) univ s) = ∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i)
⊢ piPremeasure (α := α) m (Set.pi (α := α) univ s) = ∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i)

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h : IsEmpty ι
⊢ piPremeasure (α := α) m (Set.pi (α := α) univ s) = ∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i)

Tactic:
simp [piPremeasure]

Premises used: MeasureTheory.piPremeasure
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h : Nonempty ι
inr :
  ∀ (h : Set.pi (α := α) univ s = ∅),
    piPremeasure (α := α) m (Set.pi (α := α) univ s) = ∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i)
inr₁ :
  ∀ (h : (Set.pi (α := α) univ s).Nonempty),
    piPremeasure (α := α) m (Set.pi (α := α) univ s) = ∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i)
⊢ piPremeasure (α := α) m (Set.pi (α := α) univ s) = ∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i)

Tactic:
rcases (pi univ s).eq_empty_or_nonempty with h | h

Premises used: Set.univ, Set.eq_empty_or_nonempty, Set.pi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h_1 : Nonempty ι
h : Set.pi (α := α) univ s = ∅
inr :
  ∀ (i : ι) (hi : s i = ∅),
    piPremeasure (α := α) m (Set.pi (α := α) univ s) = ∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i)
⊢ piPremeasure (α := α) m (Set.pi (α := α) univ s) = ∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i)

Tactic:
rcases univ_pi_eq_empty_iff.mp h with ⟨i, hi⟩

Premises used: Set.univ_pi_eq_empty_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h_1 : Nonempty ι
h : Set.pi (α := α) univ s = ∅
i : ι
hi : s i = ∅
⊢ Eq (α := ℝ≥0∞) ((m i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [hi]
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h_1 : Nonempty ι
h : Set.pi (α := α) univ s = ∅
i : ι
hi : s i = ∅
⊢ ∃ (i : ι), Eq (α := ℝ≥0∞) ((m i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have : ∃ i, m i (s i) = 0 := ⟨i, by simp [hi]⟩
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h_1 : Nonempty ι
h : Set.pi (α := α) univ s = ∅
i : ι
hi : s i = ∅
this : ∃ (i : ι), Eq (α := ℝ≥0∞) ((m i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ piPremeasure (α := α) m (Set.pi (α := α) univ s) = ∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i)

Tactic:
simpa [h, Finset.card_univ, zero_pow Fintype.card_ne_zero, @eq_comm _ (0 : ℝ≥0∞),
      Finset.prod_eq_zero_iff, piPremeasure]

Premises used: Finset.card_univ, eq_comm, Fintype.card_ne_zero, MeasureTheory.piPremeasure, Finset.prod_eq_zero_iff, zero_pow
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h_1 : Nonempty ι
h : (Set.pi (α := α) univ s).Nonempty
⊢ piPremeasure (α := α) m (Set.pi (α := α) univ s) = ∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i)

Tactic:
simp [h, piPremeasure]

Premises used: MeasureTheory.piPremeasure
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s t : Set ((i : ι) → α i)
h : s ⊆ t
⊢ piPremeasure (α := α) m s ≤ piPremeasure (α := α) m t

Tactic:
Finset.prod_le_prod' fun _ _ => measure_mono (Set.image_mono h)

Premises used: Finset.prod_le_prod', Set.image_mono, MeasureTheory.piPremeasure, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : Set ((i : ι) → α i)
simp : ∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) ((fun (a : (x : ι) → α x) ↦ a i) '' s) = piPremeasure (α := α) m s
⊢ piPremeasure (α := α) m (Set.pi (α := α) univ fun (i : ι) ↦ eval (β := α) i '' s) = piPremeasure (α := α) m s

Tactic:
simp only [eval, piPremeasure_pi']

Premises used: Function.eval, MeasureTheory.piPremeasure_pi'
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : Set ((i : ι) → α i)
⊢ ∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) ((fun (a : (x : ι) → α x) ↦ a i) '' s) = piPremeasure (α := α) m s

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
inl :
  ∀ (h : Set.pi (α := α) univ s = ∅),
    LE.le (α := ℝ≥0∞) ((OuterMeasure.pi (α := α) m : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
      (∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
inr :
  ∀ (h : (Set.pi (α := α) univ s).Nonempty),
    LE.le (α := ℝ≥0∞) ((OuterMeasure.pi (α := α) m : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
      (∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((OuterMeasure.pi (α := α) m : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    (∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
rcases (pi univ s).eq_empty_or_nonempty with h | h

Premises used: Set.univ, Set.eq_empty_or_nonempty, Set.pi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h : Set.pi (α := α) univ s = ∅
⊢ LE.le (α := ℝ≥0∞) ((OuterMeasure.pi (α := α) m : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    (∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
simp [h]
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h : (Set.pi (α := α) univ s).Nonempty
⊢ LE.le (α := ℝ≥0∞) ((OuterMeasure.pi (α := α) m : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    (∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
(boundedBy_le _).trans_eq (piPremeasure_pi h)

Premises used: LE.le.trans_eq, MeasureTheory.OuterMeasure.boundedBy_le, MeasureTheory.piPremeasure_pi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h : (Set.pi (α := α) univ s).Nonempty
⊢ LE.le (α := ℝ≥0∞) ((OuterMeasure.pi (α := α) m : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    (∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
exact (boundedBy_le _).trans_eq (piPremeasure_pi h)

Premises used: LE.le.trans_eq, MeasureTheory.OuterMeasure.boundedBy_le, MeasureTheory.piPremeasure_pi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
rw :
  (∀ (s : Set ((i : ι) → α i)), s.Nonempty → (n : (a : Set ((i : ι) → α i)) → ℝ≥0∞) s ≤ piPremeasure (α := α) m s) ↔
    ∀ (s : (i : ι) → Set (α i)),
      (Set.pi (α := α) univ s).Nonempty →
        LE.le (α := ℝ≥0∞) ((n : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
          (∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ n ≤ OuterMeasure.pi (α := α) m ↔
    ∀ (s : (i : ι) → Set (α i)),
      (Set.pi (α := α) univ s).Nonempty →
        LE.le (α := ℝ≥0∞) ((n : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
          (∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
rw [OuterMeasure.pi, le_boundedBy']

Premises used: MeasureTheory.OuterMeasure.le_boundedBy', MeasureTheory.OuterMeasure.pi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
mp :
  (∀ (s : Set ((i : ι) → α i)), s.Nonempty → (n : (a : Set ((i : ι) → α i)) → ℝ≥0∞) s ≤ piPremeasure (α := α) m s) →
    ∀ (s : (i : ι) → Set (α i)),
      (Set.pi (α := α) univ s).Nonempty →
        LE.le (α := ℝ≥0∞) ((n : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
          (∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
mpr :
  (∀ (s : (i : ι) → Set (α i)),
      (Set.pi (α := α) univ s).Nonempty →
        LE.le (α := ℝ≥0∞) ((n : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
          (∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)) →
    ∀ (s : Set ((i : ι) → α i)), s.Nonempty → (n : (a : Set ((i : ι) → α i)) → ℝ≥0∞) s ≤ piPremeasure (α := α) m s
⊢ (∀ (s : Set ((i : ι) → α i)), s.Nonempty → (n : (a : Set ((i : ι) → α i)) → ℝ≥0∞) s ≤ piPremeasure (α := α) m s) ↔
    ∀ (s : (i : ι) → Set (α i)),
      (Set.pi (α := α) univ s).Nonempty →
        LE.le (α := ℝ≥0∞) ((n : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
          (∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
h : ∀ (s : Set ((i : ι) → α i)), s.Nonempty → (n : (a : Set ((i : ι) → α i)) → ℝ≥0∞) s ≤ piPremeasure (α := α) m s
s : (i : ι) → Set (α i)
hs : (Set.pi (α := α) univ s).Nonempty
⊢ LE.le (α := ℝ≥0∞) ((n : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    (∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
(h _ hs).trans_eq (piPremeasure_pi hs)

Premises used: LE.le.trans_eq, MeasureTheory.piPremeasure_pi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
h : ∀ (s : Set ((i : ι) → α i)), s.Nonempty → (n : (a : Set ((i : ι) → α i)) → ℝ≥0∞) s ≤ piPremeasure (α := α) m s
s : (i : ι) → Set (α i)
hs : (Set.pi (α := α) univ s).Nonempty
⊢ LE.le (α := ℝ≥0∞) ((n : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
    (∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
refine (h _ hs).trans_eq (piPremeasure_pi hs)

Premises used: LE.le.trans_eq, MeasureTheory.piPremeasure_pi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
h :
  ∀ (s : (i : ι) → Set (α i)),
    (Set.pi (α := α) univ s).Nonempty →
      LE.le (α := ℝ≥0∞) ((n : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
        (∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
s : Set ((i : ι) → α i)
hs : s.Nonempty
⊢ (n : (a : Set ((i : ι) → α i)) → ℝ≥0∞) s ≤ piPremeasure (α := α) m s

Tactic:
le_trans (n.mono <| subset_pi_eval_image univ s) (h _ ?_)

Premises used: Set.univ, MeasureTheory.OuterMeasure.mono, Set.subset_pi_eval_image, le_trans
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
h :
  ∀ (s : (i : ι) → Set (α i)),
    (Set.pi (α := α) univ s).Nonempty →
      LE.le (α := ℝ≥0∞) ((n : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
        (∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
s : Set ((i : ι) → α i)
hs : s.Nonempty
mpr : Set.Nonempty (α := (i : ι) → α i) (Set.pi (α := α) univ fun (i : ι) ↦ eval (β := α) i '' s)
⊢ (n : (a : Set ((i : ι) → α i)) → ℝ≥0∞) s ≤ piPremeasure (α := α) m s

Tactic:
refine le_trans (n.mono <| subset_pi_eval_image univ s) (h _ ?_)

Premises used: Set.univ, MeasureTheory.OuterMeasure.mono, Set.subset_pi_eval_image, le_trans
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
h :
  ∀ (s : (i : ι) → Set (α i)),
    (Set.pi (α := α) univ s).Nonempty →
      LE.le (α := ℝ≥0∞) ((n : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (Set.pi (α := α) univ s) : ℝ≥0∞)
        (∏ i : ι, (m i : (a : Set (α i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
s : Set ((i : ι) → α i)
hs : s.Nonempty
⊢ Set.Nonempty (α := (i : ι) → α i) (Set.pi (α := α) univ fun (i : ι) ↦ eval (β := α) i '' s)

Tactic:
simp [univ_pi_nonempty_iff, hs]

Premises used: Set.univ_pi_nonempty_iff
-- 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)
μ_1 : (i : ι) → Measure (α i)
δ : Type u_4
X : δ → Type u_5
inst_2 : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
⊢ Measure (TProd X [])

Tactic:
exact dirac PUnit.unit

Premises used: MeasureTheory.Measure.dirac, PUnit.unit
-- 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)
μ_1 : (i : ι) → Measure (α i)
δ : Type u_4
X : δ → Type u_5
inst_2 : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
i : δ
l : List δ
ih : Measure (TProd X l)
⊢ Measure (TProd X (i :: l))

Tactic:
exact (μ i).prod (α := X i) ih

Premises used: MeasureTheory.Measure.prod
-- 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)
μ_1 : (i : ι) → Measure (α i)
δ : Type u_4
X : δ → Type u_5
inst_2 : (i : δ) → MeasurableSpace (X i)
l : List δ
μ : (i : δ) → Measure (X i)
nil : Measure (TProd X [])
cons : (i : δ) → (l : List δ) → (ih : Measure (TProd X l)) → Measure (TProd X (i :: l))
⊢ Measure (TProd X l)

Tactic:
induction l with
  | nil => exact dirac PUnit.unit
  | cons i l ih => exact (μ i).prod (α := X i) ih

Premises used: MeasureTheory.Measure.dirac, List.cons, PUnit.unit, List.nil
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
δ : Type u_4
X : δ → Type u_5
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
⊢ Eq (α := Measure (TProd X [])) (Measure.tprod (X := X) [] μ) (dirac PUnit.unit)

Tactic:
rfl

Premises used: MeasureTheory.Measure.tprod, List.foldr, rfl
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
δ : Type u_4
X : δ → Type u_5
inst : (i : δ) → MeasurableSpace (X i)
i : δ
l : List δ
μ : (i : δ) → Measure (X i)
⊢ Measure.tprod (X := X) (i :: l) μ = (μ i).prod (Measure.tprod (X := X) l μ)

Tactic:
rfl

Premises used: MeasureTheory.Measure.tprod, 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)
μ_1 : (i : ι) → Measure (α i)
δ : Type u_4
X : δ → Type u_5
inst_2 : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_3 : ∀ (i : δ), SigmaFinite (μ i)
⊢ SigmaFinite (m0 := TProd.instMeasurableSpace X []) (dirac PUnit.unit)

Tactic:
infer_instance
-- 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)
μ_1 : (i : ι) → Measure (α i)
δ : Type u_4
X : δ → Type u_5
inst_2 : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_3 : ∀ (i : δ), SigmaFinite (μ i)
i : δ
l : List δ
ih : SigmaFinite (Measure.tprod (X := X) l μ)
cons : SigmaFinite ((μ i).prod (Measure.tprod (X := X) l μ))
⊢ SigmaFinite (Measure.tprod (X := X) (i :: l) μ)

Tactic:
rw [tprod_cons]

Premises used: MeasureTheory.Measure.tprod_cons