case mp
α : Type u_2
β : Type ?u.54428
ι : Type u_1
ι' : Type ?u.54434
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht : Independent t
i j : ι
hij : i ≠ j
huniv : ∀ (k : ι), k = i ∨ k = j
⊢ Independent t → Disjoint (t i) (t j)

case mpr
α : Type u_2
β : Type ?u.54428
ι : Type u_1
ι' : Type ?u.54434
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht : Independent t
i j : ι
hij : i ≠ j
huniv : ∀ (k : ι), k = i ∨ k = j
⊢ Disjoint (t i) (t j) → Independent t
α : Type u_2
β : Type ?u.54428
ι : Type u_1
ι' : Type ?u.54434
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht : Independent t
i j : ι
hij : i ≠ j
huniv : ∀ (k : ι), k = i ∨ k = j
⊢ Independent t ↔ Disjoint (t i) (t j)
constructor
no goals
case mp
α : Type u_2
β : Type ?u.54428
ι : Type u_1
ι' : Type ?u.54434
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht : Independent t
i j : ι
hij : i ≠ j
huniv : ∀ (k : ι), k = i ∨ k = j
⊢ Independent t → Disjoint (t i) (t j)
exact fun h => h.pairwiseDisjoint hij
case mpr
α : Type u_2
β : Type ?u.54428
ι : Type u_1
ι' : Type ?u.54434
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht : Independent t
i j : ι
hij : i ≠ j
huniv : ∀ (k : ι), k = i ∨ k = j
h : Disjoint (t i) (t j)
k : ι
⊢ Disjoint (t k) (⨆ (j : ι) (_ : j ≠ k), t j)
case mpr
α : Type u_2
β : Type ?u.54428
ι : Type u_1
ι' : Type ?u.54434
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht : Independent t
i j : ι
hij : i ≠ j
huniv : ∀ (k : ι), k = i ∨ k = j
⊢ Disjoint (t i) (t j) → Independent t
rintro h k
case mpr.inl
α : Type u_2
β : Type ?u.54428
ι : Type u_1
ι' : Type ?u.54434
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht : Independent t
j k : ι
hij : k ≠ j
huniv : ∀ (k_1 : ι), k_1 = k ∨ k_1 = j
h : Disjoint (t k) (t j)
⊢ Disjoint (t k) (⨆ (j : ι) (_ : j ≠ k), t j)

case mpr.inr
α : Type u_2
β : Type ?u.54428
ι : Type u_1
ι' : Type ?u.54434
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht : Independent t
i k : ι
hij : i ≠ k
huniv : ∀ (k_1 : ι), k_1 = i ∨ k_1 = k
h : Disjoint (t i) (t k)
⊢ Disjoint (t k) (⨆ (j : ι) (_ : j ≠ k), t j)
case mpr
α : Type u_2
β : Type ?u.54428
ι : Type u_1
ι' : Type ?u.54434
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht : Independent t
i j : ι
hij : i ≠ j
huniv : ∀ (k : ι), k = i ∨ k = j
h : Disjoint (t i) (t j)
k : ι
⊢ Disjoint (t k) (⨆ (j : ι) (_ : j ≠ k), t j)
obtain rfl | rfl := huniv k
case mpr.inl
α : Type u_2
β : Type ?u.54428
ι : Type u_1
ι' : Type ?u.54434
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht : Independent t
j k : ι
hij : k ≠ j
huniv : ∀ (k_1 : ι), k_1 = k ∨ k_1 = j
h : Disjoint (t k) (t j)
i : ι
hi : i ≠ k
⊢ t i = t j
case mpr.inl
α : Type u_2
β : Type ?u.54428
ι : Type u_1
ι' : Type ?u.54434
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht : Independent t
j k : ι
hij : k ≠ j
huniv : ∀ (k_1 : ι), k_1 = k ∨ k_1 = j
h : Disjoint (t k) (t j)
⊢ Disjoint (t k) (⨆ (j : ι) (_ : j ≠ k), t j)
refine' h.mono_right (iSup_le fun i => iSup_le fun hi => Eq.le _)
no goals
case mpr.inl
α : Type u_2
β : Type ?u.54428
ι : Type u_1
ι' : Type ?u.54434
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht : Independent t
j k : ι
hij : k ≠ j
huniv : ∀ (k_1 : ι), k_1 = k ∨ k_1 = j
h : Disjoint (t k) (t j)
i : ι
hi : i ≠ k
⊢ t i = t j
rw [(huniv i).resolve_left hi]
case mpr.inr
α : Type u_2
β : Type ?u.54428
ι : Type u_1
ι' : Type ?u.54434
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht : Independent t
i k : ι
hij : i ≠ k
huniv : ∀ (k_1 : ι), k_1 = i ∨ k_1 = k
h : Disjoint (t i) (t k)
j : ι
hj : j ≠ k
⊢ t j = t i
case mpr.inr
α : Type u_2
β : Type ?u.54428
ι : Type u_1
ι' : Type ?u.54434
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht : Independent t
i k : ι
hij : i ≠ k
huniv : ∀ (k_1 : ι), k_1 = i ∨ k_1 = k
h : Disjoint (t i) (t k)
⊢ Disjoint (t k) (⨆ (j : ι) (_ : j ≠ k), t j)
refine' h.symm.mono_right (iSup_le fun j => iSup_le fun hj => Eq.le _)
no goals
case mpr.inr
α : Type u_2
β : Type ?u.54428
ι : Type u_1
ι' : Type ?u.54434
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t : ι → α
ht : Independent t
i k : ι
hij : i ≠ k
huniv : ∀ (k_1 : ι), k_1 = i ∨ k_1 = k
h : Disjoint (t i) (t k)
j : ι
hj : j ≠ k
⊢ t j = t i
rw [(huniv j).resolve_right hj]