α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
i j : ℕ
ij : i ≠ j
⊢ (Disjoint on fun i => ⋃ (b : β) (_ : b ∈ decode₂ β i), f b) i j
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
⊢ Pairwise (Disjoint on fun i => ⋃ (b : β) (_ : b ∈ decode₂ β i), f b)
rintro i j ij
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
i j : ℕ
ij : i ≠ j
x : α
⊢ x ∈ (fun i => ⋃ (b : β) (_ : b ∈ decode₂ β i), f b) i → ¬x ∈ (fun i => ⋃ (b : β) (_ : b ∈ decode₂ β i), f b) j
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
i j : ℕ
ij : i ≠ j
⊢ (Disjoint on fun i => ⋃ (b : β) (_ : b ∈ decode₂ β i), f b) i j
refine' disjoint_left.mpr fun x => _
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
i j : ℕ
ij : i ≠ j
x : α
⊢ ∀ (a : β), encode a = i → x ∈ f a → ∀ (b : β), encode b = j → ¬x ∈ f b
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
i j : ℕ
ij : i ≠ j
x : α
⊢ x ∈ (fun i => ⋃ (b : β) (_ : b ∈ decode₂ β i), f b) i → ¬x ∈ (fun i => ⋃ (b : β) (_ : b ∈ decode₂ β i), f b) j
suffices ∀ a, encode a = i → x ∈ f a → ∀ b, encode b = j → x ∉ f b by simpa [decode₂_eq_some]
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
x : α
a : β
ha : x ∈ f a
b : β
ij : encode a ≠ encode b
hb : x ∈ f b
⊢ False
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
i j : ℕ
ij : i ≠ j
x : α
⊢ ∀ (a : β), encode a = i → x ∈ f a → ∀ (b : β), encode b = j → ¬x ∈ f b
rintro a rfl ha b rfl hb
no goals
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
x : α
a : β
ha : x ∈ f a
b : β
ij : encode a ≠ encode b
hb : x ∈ f b
⊢ False
exact (hd (mt (congr_arg encode) ij)).le_bot ⟨ha, hb⟩
no goals
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
i j : ℕ
ij : i ≠ j
x : α
this : ∀ (a : β), encode a = i → x ∈ f a → ∀ (b : β), encode b = j → ¬x ∈ f b
⊢ x ∈ (fun i => ⋃ (b : β) (_ : b ∈ decode₂ β i), f b) i → ¬x ∈ (fun i => ⋃ (b : β) (_ : b ∈ decode₂ β i), f b) j
simpa [decode₂_eq_some]