-- Mathlib/MeasureTheory/Constructions/Pi.lean
theorem le_pi {m : ∀ i, OuterMeasure (α i)} {n : OuterMeasure (∀ i, α i)} :
    n ≤ OuterMeasure.pi m ↔
      ∀ s : ∀ i, Set (α i), (pi univ s).Nonempty → n (pi univ s) ≤ ∏ i, m i (s i)

Proof state:
case mpr
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
h : ∀ (s : (i : ι) → Set (α i)), (univ.pi s).Nonempty → n (univ.pi s) ≤ ∏ i : ι, (m i) (s i)
s : Set ((i : ι) → α i)
hs : s.Nonempty
⊢ (univ.pi fun i => eval i '' s).Nonempty

Tactic:
simp [univ_pi_nonempty_iff, hs]

Result:
no goals

Proof state:
case mp
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
h : ∀ (s : Set ((i : ι) → α i)), s.Nonempty → n s ≤ piPremeasure m s
s : (i : ι) → Set (α i)
hs : (univ.pi s).Nonempty
⊢ n (univ.pi s) ≤ ∏ i : ι, (m i) (s i)

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

Result:
no goals

Proof state:
case mp
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
⊢ (∀ (s : Set ((i : ι) → α i)), s.Nonempty → n s ≤ piPremeasure m s) →
    ∀ (s : (i : ι) → Set (α i)), (univ.pi s).Nonempty → n (univ.pi s) ≤ ∏ i : ι, (m i) (s i)

Tactic:
intro h s hs

Result:
case mp
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
h : ∀ (s : Set ((i : ι) → α i)), s.Nonempty → n s ≤ piPremeasure m s
s : (i : ι) → Set (α i)
hs : (univ.pi s).Nonempty
⊢ n (univ.pi s) ≤ ∏ i : ι, (m i) (s i)

Proof state:
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
⊢ n ≤ OuterMeasure.pi m ↔ ∀ (s : (i : ι) → Set (α i)), (univ.pi s).Nonempty → n (univ.pi s) ≤ ∏ i : ι, (m i) (s i)

Tactic:
rw [OuterMeasure.pi, le_boundedBy']

Result:
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
⊢ (∀ (s : Set ((i : ι) → α i)), s.Nonempty → n s ≤ piPremeasure m s) ↔
    ∀ (s : (i : ι) → Set (α i)), (univ.pi s).Nonempty → n (univ.pi s) ≤ ∏ i : ι, (m i) (s i)

Proof state:
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
⊢ (∀ (s : Set ((i : ι) → α i)), s.Nonempty → n s ≤ piPremeasure m s) ↔
    ∀ (s : (i : ι) → Set (α i)), (univ.pi s).Nonempty → n (univ.pi s) ≤ ∏ i : ι, (m i) (s i)

Tactic:
constructor

Result:
case mp
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
⊢ (∀ (s : Set ((i : ι) → α i)), s.Nonempty → n s ≤ piPremeasure m s) →
    ∀ (s : (i : ι) → Set (α i)), (univ.pi s).Nonempty → n (univ.pi s) ≤ ∏ i : ι, (m i) (s i)

case mpr
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
⊢ (∀ (s : (i : ι) → Set (α i)), (univ.pi s).Nonempty → n (univ.pi s) ≤ ∏ i : ι, (m i) (s i)) →
    ∀ (s : Set ((i : ι) → α i)), s.Nonempty → n s ≤ piPremeasure m s

Proof state:
case mpr
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
h : ∀ (s : (i : ι) → Set (α i)), (univ.pi s).Nonempty → n (univ.pi s) ≤ ∏ i : ι, (m i) (s i)
s : Set ((i : ι) → α i)
hs : s.Nonempty
⊢ n s ≤ piPremeasure m s

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

Result:
case mpr
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
h : ∀ (s : (i : ι) → Set (α i)), (univ.pi s).Nonempty → n (univ.pi s) ≤ ∏ i : ι, (m i) (s i)
s : Set ((i : ι) → α i)
hs : s.Nonempty
⊢ (univ.pi fun i => eval i '' s).Nonempty

Proof state:
case mpr
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
⊢ (∀ (s : (i : ι) → Set (α i)), (univ.pi s).Nonempty → n (univ.pi s) ≤ ∏ i : ι, (m i) (s i)) →
    ∀ (s : Set ((i : ι) → α i)), s.Nonempty → n s ≤ piPremeasure m s

Tactic:
intro h s hs

Result:
case mpr
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
h : ∀ (s : (i : ι) → Set (α i)), (univ.pi s).Nonempty → n (univ.pi s) ≤ ∏ i : ι, (m i) (s i)
s : Set ((i : ι) → α i)
hs : s.Nonempty
⊢ n s ≤ piPremeasure m s