-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem measure_iUnion_congr_of_subset {ι : Sort*} [Countable ι] {s : ι → Set α} {t : ι → Set α}
    (hsub : ∀ i, s i ⊆ t i) (h_le : ∀ i, μ (t i) ≤ μ (s i)) : μ (⋃ i, s i) = μ (⋃ i, t i)

Proof state:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
htop : ∀ (i : ι), μ (t i) ≠ ⊤
M : Set α → Set α := toMeasurable μ
b : ι
⊢ NullMeasurableSet (M (t b) ∩ M (⋃ b, s b)) μ

Tactic:
measurability

Result:
no goals

Proof state:
case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
htop : ∀ (i : ι), μ (t i) ≠ ⊤
⊢ μ (⋃ i, t i) ≤ μ (⋃ i, s i)

Tactic:
set M := toMeasurable μ

Result:
case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
htop : ∀ (i : ι), μ (t i) ≠ ⊤
M : Set α → Set α := toMeasurable μ
⊢ μ (⋃ i, t i) ≤ μ (⋃ i, s i)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
htop : ∀ (i : ι), μ (t i) ≠ ⊤
M : Set α → Set α := toMeasurable μ
⊢ ∀ (b : ι), M (t b) ∩ M (⋃ b, s b) =ᶠ[ae μ] M (t b)

Tactic:
refine fun b => ae_eq_of_subset_of_measure_ge inter_subset_left ?_ ?_ ?_

Result:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
htop : ∀ (i : ι), μ (t i) ≠ ⊤
M : Set α → Set α := toMeasurable μ
b : ι
⊢ μ (M (t b)) ≤ μ (M (t b) ∩ M (⋃ b, s b))

case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
htop : ∀ (i : ι), μ (t i) ≠ ⊤
M : Set α → Set α := toMeasurable μ
b : ι
⊢ NullMeasurableSet (M (t b) ∩ M (⋃ b, s b)) μ

case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
htop : ∀ (i : ι), μ (t i) ≠ ⊤
M : Set α → Set α := toMeasurable μ
b : ι
⊢ μ (M (t b)) ≠ ⊤

Proof state:
case inl.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
i : ι
hi : μ (t i) = ⊤
⊢ μ (⋃ i, t i) ≤ μ (⋃ i, s i)

Tactic:
calc
  μ (⋃ i, t i) ≤ ∞ := le_top
  _ ≤ μ (s i) := hi ▸ h_le i
  _ ≤ μ (⋃ i, s i) := measure_mono <| subset_iUnion _ _

Result:
no goals

Proof state:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
htop : ∀ (i : ι), μ (t i) ≠ ⊤
M : Set α → Set α := toMeasurable μ
b : ι
⊢ μ (M (t b)) ≤ μ (M (t b) ∩ M (⋃ b, s b))

Tactic:
calc
  μ (M (t b)) = μ (t b) := measure_toMeasurable _
  _ ≤ μ (s b) := h_le b
  _ ≤ μ (M (t b) ∩ M (⋃ b, s b)) :=
    measure_mono <|
      subset_inter ((hsub b).trans <| subset_toMeasurable _ _)
        ((subset_iUnion _ _).trans <| subset_toMeasurable _ _)

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
⊢ μ (⋃ i, s i) = μ (⋃ i, t i)

Tactic:
refine le_antisymm (by gcongr; apply hsub) ?_

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
⊢ μ (⋃ i, t i) ≤ μ (⋃ i, s i)

Proof state:
case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
htop : ∀ (i : ι), μ (t i) ≠ ⊤
M : Set α → Set α := toMeasurable μ
H : ∀ (b : ι), M (t b) ∩ M (⋃ b, s b) =ᶠ[ae μ] M (t b)
⊢ μ (⋃ i, t i) ≤ μ (⋃ i, s i)

Tactic:
calc
  μ (⋃ b, t b) ≤ μ (⋃ b, M (t b)) := measure_mono (iUnion_mono fun b => subset_toMeasurable _ _)
  _ = μ (⋃ b, M (t b) ∩ M (⋃ b, s b)) := measure_congr (EventuallyEq.countable_iUnion H).symm
  _ ≤ μ (M (⋃ b, s b)) := measure_mono (iUnion_subset fun b => inter_subset_right)
  _ = μ (⋃ b, s b) := measure_toMeasurable _

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
⊢ μ (⋃ i, t i) ≤ μ (⋃ i, s i)

Tactic:
rcases Classical.em (∃ i, μ (t i) = ∞) with (⟨i, hi⟩ | htop)

Result:
case inl.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
i : ι
hi : μ (t i) = ⊤
⊢ μ (⋃ i, t i) ≤ μ (⋃ i, s i)

case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
htop : ¬∃ i, μ (t i) = ⊤
⊢ μ (⋃ i, t i) ≤ μ (⋃ i, s i)

Proof state:
case h.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
i✝ : ι
⊢ s i✝ ⊆ t i✝

Tactic:
apply hsub

Result:
no goals

Proof state:
case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
htop : ∀ (i : ι), μ (t i) ≠ ⊤
M : Set α → Set α := toMeasurable μ
b : ι
⊢ μ (M (t b)) ≠ ⊤

Tactic:
rw [measure_toMeasurable]

Result:
case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
htop : ∀ (i : ι), μ (t i) ≠ ⊤
M : Set α → Set α := toMeasurable μ
b : ι
⊢ μ (t b) ≠ ⊤

Proof state:
case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
htop : ∀ (i : ι), μ (t i) ≠ ⊤
M : Set α → Set α := toMeasurable μ
b : ι
⊢ μ (t b) ≠ ⊤

Tactic:
exact htop b

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
⊢ μ (⋃ i, s i) ≤ μ (⋃ i, t i)

Tactic:
gcongr

Result:
case h.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
i✝ : ι
⊢ s i✝ ⊆ t i✝

Proof state:
case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
htop : ¬∃ i, μ (t i) = ⊤
⊢ μ (⋃ i, t i) ≤ μ (⋃ i, s i)

Tactic:
push_neg at htop

Result:
case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
htop : ∀ (i : ι), μ (t i) ≠ ⊤
⊢ μ (⋃ i, t i) ≤ μ (⋃ i, s i)