case mp
α : Type u_1
β : Type ?u.24528
ι : Type ?u.24531
ι' : Type ?u.24534
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
a b : α
hab : a ≠ b
⊢ SetIndependent {a, b} → Disjoint a b

case mpr
α : Type u_1
β : Type ?u.24528
ι : Type ?u.24531
ι' : Type ?u.24534
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
a b : α
hab : a ≠ b
⊢ Disjoint a b → SetIndependent {a, b}
α : Type u_1
β : Type ?u.24528
ι : Type ?u.24531
ι' : Type ?u.24534
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
a b : α
hab : a ≠ b
⊢ SetIndependent {a, b} ↔ Disjoint a b
constructor
case mp
α : Type u_1
β : Type ?u.24528
ι : Type ?u.24531
ι' : Type ?u.24534
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
a b : α
hab : a ≠ b
h : SetIndependent {a, b}
⊢ Disjoint a b
case mp
α : Type u_1
β : Type ?u.24528
ι : Type ?u.24531
ι' : Type ?u.24534
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
a b : α
hab : a ≠ b
⊢ SetIndependent {a, b} → Disjoint a b
intro h
no goals
case mp
α : Type u_1
β : Type ?u.24528
ι : Type ?u.24531
ι' : Type ?u.24534
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
a b : α
hab : a ≠ b
h : SetIndependent {a, b}
⊢ Disjoint a b
exact h.pairwiseDisjoint (mem_insert _ _) (mem_insert_of_mem _ (mem_singleton _)) hab
case mpr.inl
α : Type u_1
β : Type ?u.24528
ι : Type ?u.24531
ι' : Type ?u.24534
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
b c : α
hab : c ≠ b
h : Disjoint c b
⊢ Disjoint c (sSup ({c, b} \ {c}))

case mpr.inr
α : Type u_1
β : Type ?u.24528
ι : Type ?u.24531
ι' : Type ?u.24534
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
a c : α
hab : a ≠ c
h : Disjoint a c
⊢ Disjoint c (sSup ({a, c} \ {c}))
case mpr
α : Type u_1
β : Type ?u.24528
ι : Type ?u.24531
ι' : Type ?u.24534
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
a b : α
hab : a ≠ b
⊢ Disjoint a b → SetIndependent {a, b}
rintro h c ((rfl : c = a) | (rfl : c = b))
case h.e'_5
α : Type u_1
β : Type ?u.24528
ι : Type ?u.24531
ι' : Type ?u.24534
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
b c : α
hab : c ≠ b
h : Disjoint c b
⊢ sSup ({c, b} \ {c}) = b
case mpr.inl
α : Type u_1
β : Type ?u.24528
ι : Type ?u.24531
ι' : Type ?u.24534
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
b c : α
hab : c ≠ b
h : Disjoint c b
⊢ Disjoint c (sSup ({c, b} \ {c}))
convert h using 1
no goals
case h.e'_5
α : Type u_1
β : Type ?u.24528
ι : Type ?u.24531
ι' : Type ?u.24534
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
b c : α
hab : c ≠ b
h : Disjoint c b
⊢ sSup ({c, b} \ {c}) = b
simp [hab, sSup_singleton]
case h.e'_5
α : Type u_1
β : Type ?u.24528
ι : Type ?u.24531
ι' : Type ?u.24534
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
a c : α
hab : a ≠ c
h : Disjoint a c
⊢ sSup ({a, c} \ {c}) = a
case mpr.inr
α : Type u_1
β : Type ?u.24528
ι : Type ?u.24531
ι' : Type ?u.24534
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
a c : α
hab : a ≠ c
h : Disjoint a c
⊢ Disjoint c (sSup ({a, c} \ {c}))
convert h.symm using 1
no goals
case h.e'_5
α : Type u_1
β : Type ?u.24528
ι : Type ?u.24531
ι' : Type ?u.24534
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
a c : α
hab : a ≠ c
h : Disjoint a c
⊢ sSup ({a, c} \ {c}) = a
simp [hab, sSup_singleton]