α✝ : Type ?u.27201
β : Type ?u.27204
ι : Type ?u.27207
ι' : Type ?u.27210
inst✝¹ : CompleteLattice α✝
s✝ : Set α✝
hs : SetIndependent s✝
α : Type u_1
inst✝ : CompleteLattice α
s : Set α
⊢ (∀ ⦃a : α⦄, a ∈ s → Disjoint a (⨆ (a_2 : α) (_ : a_2 ∈ s \ {a}), a_2)) ↔
    ∀ (x : α) (h : x ∈ s), Disjoint x (⨆ (j : { x // x ∈ s }) (_ : j ≠ { val := x, property := h }), ↑j)
α✝ : Type ?u.27201
β : Type ?u.27204
ι : Type ?u.27207
ι' : Type ?u.27210
inst✝¹ : CompleteLattice α✝
s✝ : Set α✝
hs : SetIndependent s✝
α : Type u_1
inst✝ : CompleteLattice α
s : Set α
⊢ SetIndependent s ↔ Independent Subtype.val
simp_rw [Independent, SetIndependent, SetCoe.forall, sSup_eq_iSup]
α✝ : Type ?u.27201
β : Type ?u.27204
ι : Type ?u.27207
ι' : Type ?u.27210
inst✝¹ : CompleteLattice α✝
s✝ : Set α✝
hs : SetIndependent s✝
α : Type u_1
inst✝ : CompleteLattice α
s : Set α
a : α
ha : a ∈ s
⊢ Disjoint a (⨆ (a_1 : α) (_ : a_1 ∈ s \ {a}), a_1) ↔
    Disjoint a (⨆ (j : { x // x ∈ s }) (_ : j ≠ { val := a, property := ha }), ↑j)
α✝ : Type ?u.27201
β : Type ?u.27204
ι : Type ?u.27207
ι' : Type ?u.27210
inst✝¹ : CompleteLattice α✝
s✝ : Set α✝
hs : SetIndependent s✝
α : Type u_1
inst✝ : CompleteLattice α
s : Set α
⊢ (∀ ⦃a : α⦄, a ∈ s → Disjoint a (⨆ (a_2 : α) (_ : a_2 ∈ s \ {a}), a_2)) ↔
    ∀ (x : α) (h : x ∈ s), Disjoint x (⨆ (j : { x // x ∈ s }) (_ : j ≠ { val := x, property := h }), ↑j)
refine' forall₂_congr fun a ha => _
no goals
α✝ : Type ?u.27201
β : Type ?u.27204
ι : Type ?u.27207
ι' : Type ?u.27210
inst✝¹ : CompleteLattice α✝
s✝ : Set α✝
hs : SetIndependent s✝
α : Type u_1
inst✝ : CompleteLattice α
s : Set α
a : α
ha : a ∈ s
⊢ Disjoint a (⨆ (a_1 : α) (_ : a_1 ∈ s \ {a}), a_1) ↔
    Disjoint a (⨆ (j : { x // x ∈ s }) (_ : j ≠ { val := a, property := ha }), ↑j)
simp [iSup_subtype, iSup_and]