case empty
α : Type u_2
β : Type ?u.310858
γ : Type ?u.310861
δ : Type ?u.310864
ι : Type u_1
R : Type ?u.310870
R' : Type ?u.310873
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
t : ι → Set α
⊢ restrict μ (⋃ (i : ι) (_ : i ∈ ∅), t i) = restrict ν (⋃ (i : ι) (_ : i ∈ ∅), t i) ↔
    ∀ (i : ι), i ∈ ∅ → restrict μ (t i) = restrict ν (t i)

case insert
α : Type u_2
β : Type ?u.310858
γ : Type ?u.310861
δ : Type ?u.310864
ι : Type u_1
R : Type ?u.310870
R' : Type ?u.310873
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
t : ι → Set α
i : ι
s : Finset ι
a✝ : ¬i ∈ s
hs :
  restrict μ (⋃ (i : ι) (_ : i ∈ s), t i) = restrict ν (⋃ (i : ι) (_ : i ∈ s), t i) ↔
    ∀ (i : ι), i ∈ s → restrict μ (t i) = restrict ν (t i)
⊢ restrict μ (⋃ (i_1 : ι) (_ : i_1 ∈ insert i s), t i_1) = restrict ν (⋃ (i_1 : ι) (_ : i_1 ∈ insert i s), t i_1) ↔
    ∀ (i_1 : ι), i_1 ∈ insert i s → restrict μ (t i_1) = restrict ν (t i_1)
α : Type u_2
β : Type ?u.310858
γ : Type ?u.310861
δ : Type ?u.310864
ι : Type u_1
R : Type ?u.310870
R' : Type ?u.310873
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
s : Finset ι
t : ι → Set α
⊢ restrict μ (⋃ (i : ι) (_ : i ∈ s), t i) = restrict ν (⋃ (i : ι) (_ : i ∈ s), t i) ↔
    ∀ (i : ι), i ∈ s → restrict μ (t i) = restrict ν (t i)
induction' s using Finset.induction_on with i s _ hs
case insert
α : Type u_2
β : Type ?u.310858
γ : Type ?u.310861
δ : Type ?u.310864
ι : Type u_1
R : Type ?u.310870
R' : Type ?u.310873
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
t : ι → Set α
i : ι
s : Finset ι
a✝ : ¬i ∈ s
hs :
  restrict μ (⋃ (i : ι) (_ : i ∈ s), t i) = restrict ν (⋃ (i : ι) (_ : i ∈ s), t i) ↔
    ∀ (i : ι), i ∈ s → restrict μ (t i) = restrict ν (t i)
⊢ restrict μ (t i ∪ ⋃ (x : ι) (_ : x ∈ s), t x) = restrict ν (t i ∪ ⋃ (x : ι) (_ : x ∈ s), t x) ↔
    restrict μ (t i) = restrict ν (t i) ∧ ∀ (a : ι), a ∈ s → restrict μ (t a) = restrict ν (t a)
case insert
α : Type u_2
β : Type ?u.310858
γ : Type ?u.310861
δ : Type ?u.310864
ι : Type u_1
R : Type ?u.310870
R' : Type ?u.310873
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
t : ι → Set α
i : ι
s : Finset ι
a✝ : ¬i ∈ s
hs :
  restrict μ (⋃ (i : ι) (_ : i ∈ s), t i) = restrict ν (⋃ (i : ι) (_ : i ∈ s), t i) ↔
    ∀ (i : ι), i ∈ s → restrict μ (t i) = restrict ν (t i)
⊢ restrict μ (⋃ (i_1 : ι) (_ : i_1 ∈ insert i s), t i_1) = restrict ν (⋃ (i_1 : ι) (_ : i_1 ∈ insert i s), t i_1) ↔
    ∀ (i_1 : ι), i_1 ∈ insert i s → restrict μ (t i_1) = restrict ν (t i_1)
simp only [forall_eq_or_imp, iUnion_iUnion_eq_or_left, Finset.mem_insert]
no goals
case insert
α : Type u_2
β : Type ?u.310858
γ : Type ?u.310861
δ : Type ?u.310864
ι : Type u_1
R : Type ?u.310870
R' : Type ?u.310873
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
t : ι → Set α
i : ι
s : Finset ι
a✝ : ¬i ∈ s
hs :
  restrict μ (⋃ (i : ι) (_ : i ∈ s), t i) = restrict ν (⋃ (i : ι) (_ : i ∈ s), t i) ↔
    ∀ (i : ι), i ∈ s → restrict μ (t i) = restrict ν (t i)
⊢ restrict μ (t i ∪ ⋃ (x : ι) (_ : x ∈ s), t x) = restrict ν (t i ∪ ⋃ (x : ι) (_ : x ∈ s), t x) ↔
    restrict μ (t i) = restrict ν (t i) ∧ ∀ (a : ι), a ∈ s → restrict μ (t a) = restrict ν (t a)
rw [restrict_union_congr, ← hs]
no goals
case empty
α : Type u_2
β : Type ?u.310858
γ : Type ?u.310861
δ : Type ?u.310864
ι : Type u_1
R : Type ?u.310870
R' : Type ?u.310873
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
t : ι → Set α
⊢ restrict μ (⋃ (i : ι) (_ : i ∈ ∅), t i) = restrict ν (⋃ (i : ι) (_ : i ∈ ∅), t i) ↔
    ∀ (i : ι), i ∈ ∅ → restrict μ (t i) = restrict ν (t i)
simp