case refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.533340
inst✝ : DecidableEq β
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
t : Finset β
⊢ _root_.Disjoint (Finset.biUnion ∅ f) t ↔ ∀ (i : α), i ∈ ∅ → _root_.Disjoint (f i) t

case refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.533340
inst✝ : DecidableEq β
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
t : Finset β
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    ¬a ∈ s →
      (_root_.Disjoint (Finset.biUnion s f) t ↔ ∀ (i : α), i ∈ s → _root_.Disjoint (f i) t) →
        (_root_.Disjoint (Finset.biUnion (insert a s) f) t ↔ ∀ (i : α), i ∈ insert a s → _root_.Disjoint (f i) t)
α : Type u_1
β : Type u_2
γ : Type ?u.533340
inst✝ : DecidableEq β
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
t : Finset β
⊢ _root_.Disjoint (Finset.biUnion s f) t ↔ ∀ (i : α), i ∈ s → _root_.Disjoint (f i) t
refine' s.induction _ _
no goals
case refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.533340
inst✝ : DecidableEq β
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
t : Finset β
⊢ _root_.Disjoint (Finset.biUnion ∅ f) t ↔ ∀ (i : α), i ∈ ∅ → _root_.Disjoint (f i) t
simp only [forall_mem_empty_iff, biUnion_empty, disjoint_empty_left]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.533340
inst✝ : DecidableEq β
s✝¹ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
s✝ : Finset α
f : α → Finset β
t : Finset β
i : α
s : Finset α
his : ¬i ∈ s
ih : _root_.Disjoint (Finset.biUnion s f) t ↔ ∀ (i : α), i ∈ s → _root_.Disjoint (f i) t
⊢ _root_.Disjoint (Finset.biUnion (insert i s) f) t ↔ ∀ (i_1 : α), i_1 ∈ insert i s → _root_.Disjoint (f i_1) t
case refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.533340
inst✝ : DecidableEq β
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
t : Finset β
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    ¬a ∈ s →
      (_root_.Disjoint (Finset.biUnion s f) t ↔ ∀ (i : α), i ∈ s → _root_.Disjoint (f i) t) →
        (_root_.Disjoint (Finset.biUnion (insert a s) f) t ↔ ∀ (i : α), i ∈ insert a s → _root_.Disjoint (f i) t)
intro i s his ih
no goals
case refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.533340
inst✝ : DecidableEq β
s✝¹ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
s✝ : Finset α
f : α → Finset β
t : Finset β
i : α
s : Finset α
his : ¬i ∈ s
ih : _root_.Disjoint (Finset.biUnion s f) t ↔ ∀ (i : α), i ∈ s → _root_.Disjoint (f i) t
⊢ _root_.Disjoint (Finset.biUnion (insert i s) f) t ↔ ∀ (i_1 : α), i_1 ∈ insert i s → _root_.Disjoint (f i_1) t
simp only [disjoint_union_left, biUnion_insert, his, forall_mem_insert, ih]