case refine_1
α : Type u_2
β : Type u_1
E : Type u_3
F : Type ?u.1506239
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s✝ t✝ : Set α
μ ν : Measure α
s : Set β
hs : Set.Finite s
t : β → Set α
⊢ IntegrableOn f (⋃ (i : β) (_ : i ∈ ∅), t i) ↔ ∀ (i : β), i ∈ ∅ → IntegrableOn f (t i)

case refine_2
α : Type u_2
β : Type u_1
E : Type u_3
F : Type ?u.1506239
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s✝ t✝ : Set α
μ ν : Measure α
s : Set β
hs : Set.Finite s
t : β → Set α
⊢ ∀ {a : β} {s : Set β},
    ¬a ∈ s →
      Set.Finite s →
        (IntegrableOn f (⋃ (i : β) (_ : i ∈ s), t i) ↔ ∀ (i : β), i ∈ s → IntegrableOn f (t i)) →
          (IntegrableOn f (⋃ (i : β) (_ : i ∈ insert a s), t i) ↔ ∀ (i : β), i ∈ insert a s → IntegrableOn f (t i))
α : Type u_2
β : Type u_1
E : Type u_3
F : Type ?u.1506239
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s✝ t✝ : Set α
μ ν : Measure α
s : Set β
hs : Set.Finite s
t : β → Set α
⊢ IntegrableOn f (⋃ (i : β) (_ : i ∈ s), t i) ↔ ∀ (i : β), i ∈ s → IntegrableOn f (t i)
refine hs.induction_on ?_ ?_
no goals
case refine_1
α : Type u_2
β : Type u_1
E : Type u_3
F : Type ?u.1506239
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s✝ t✝ : Set α
μ ν : Measure α
s : Set β
hs : Set.Finite s
t : β → Set α
⊢ IntegrableOn f (⋃ (i : β) (_ : i ∈ ∅), t i) ↔ ∀ (i : β), i ∈ ∅ → IntegrableOn f (t i)
simp
case refine_2
α : Type u_2
β : Type u_1
E : Type u_3
F : Type ?u.1506239
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s✝¹ t✝ : Set α
μ ν : Measure α
s✝ : Set β
hs : Set.Finite s✝
t : β → Set α
a : β
s : Set β
a✝¹ : ¬a ∈ s
a✝ : Set.Finite s
hf : IntegrableOn f (⋃ (i : β) (_ : i ∈ s), t i) ↔ ∀ (i : β), i ∈ s → IntegrableOn f (t i)
⊢ IntegrableOn f (⋃ (i : β) (_ : i ∈ insert a s), t i) ↔ ∀ (i : β), i ∈ insert a s → IntegrableOn f (t i)
case refine_2
α : Type u_2
β : Type u_1
E : Type u_3
F : Type ?u.1506239
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s✝ t✝ : Set α
μ ν : Measure α
s : Set β
hs : Set.Finite s
t : β → Set α
⊢ ∀ {a : β} {s : Set β},
    ¬a ∈ s →
      Set.Finite s →
        (IntegrableOn f (⋃ (i : β) (_ : i ∈ s), t i) ↔ ∀ (i : β), i ∈ s → IntegrableOn f (t i)) →
          (IntegrableOn f (⋃ (i : β) (_ : i ∈ insert a s), t i) ↔ ∀ (i : β), i ∈ insert a s → IntegrableOn f (t i))
intro a s _ _ hf
no goals
case refine_2
α : Type u_2
β : Type u_1
E : Type u_3
F : Type ?u.1506239
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s✝¹ t✝ : Set α
μ ν : Measure α
s✝ : Set β
hs : Set.Finite s✝
t : β → Set α
a : β
s : Set β
a✝¹ : ¬a ∈ s
a✝ : Set.Finite s
hf : IntegrableOn f (⋃ (i : β) (_ : i ∈ s), t i) ↔ ∀ (i : β), i ∈ s → IntegrableOn f (t i)
⊢ IntegrableOn f (⋃ (i : β) (_ : i ∈ insert a s), t i) ↔ ∀ (i : β), i ∈ insert a s → IntegrableOn f (t i)
simp [hf, or_imp, forall_and]