[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Encodable β
inst✝ : CompleteLattice α
f : β → α
⊢ ⨆ (i : ℕ) (b : β) (_ : b ∈ decode₂ β i), f b = ⨆ (b : β), f b
[PROOFSTEP]
rw [iSup_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Encodable β
inst✝ : CompleteLattice α
f : β → α
⊢ ⨆ (j : β) (i : ℕ) (_ : j ∈ decode₂ β i), f j = ⨆ (b : β), f b
[PROOFSTEP]
simp only [mem_decode₂, iSup_iSup_eq_right]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
C : Set α → Prop
H0 : C ∅
H1 : ∀ (b : β), C (f b)
n : ℕ
⊢ C (⋃ (b : β) (_ : b ∈ none), f b)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
C : Set α → Prop
H0 : C ∅
H1 : ∀ (b : β), C (f b)
n : ℕ
⊢ C ∅
[PROOFSTEP]
apply H0
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
C : Set α → Prop
H0 : C ∅
H1 : ∀ (b : β), C (f b)
n : ℕ
b : β
⊢ C (⋃ (b_1 : β) (_ : b_1 ∈ some b), f b_1)
[PROOFSTEP]
convert H1 b
[GOAL]
case h.e'_1
α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
C : Set α → Prop
H0 : C ∅
H1 : ∀ (b : β), C (f b)
n : ℕ
b : β
⊢ ⋃ (b_1 : β) (_ : b_1 ∈ some b), f b_1 = f b
[PROOFSTEP]
simp [ext_iff]
[GOAL]
α : 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)
[PROOFSTEP]
rintro i j ij
[GOAL]
α : 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
[PROOFSTEP]
refine' disjoint_left.mpr fun x => _
[GOAL]
α : 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
[PROOFSTEP]
suffices ∀ a, encode a = i → x ∈ f a → ∀ b, encode b = j → x ∉ f b by simpa [decode₂_eq_some]
[GOAL]
α : 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
[PROOFSTEP]
simpa [decode₂_eq_some]
[GOAL]
α : 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
[PROOFSTEP]
rintro a rfl ha b rfl hb
[GOAL]
α : 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
[PROOFSTEP]
exact (hd (mt (congr_arg encode) ij)).le_bot ⟨ha, hb⟩
