no goals
α : Type u_1
β : Type ?u.57697
ι : Type u_2
ι' : Type ?u.57703
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
⊢ Independent (f ∘ Subtype.val) ↔ Finset.SupIndep s f
classical
  rw [Finset.supIndep_iff_disjoint_erase]
  refine' Subtype.forall.trans (forall₂_congr fun a b => _)
  rw [Finset.sup_eq_iSup]
  congr! 1
  refine' iSup_subtype.trans _
  congr! 1
  simp [iSup_and, @iSup_comm _ (_ ∈ s)]
α : Type u_1
β : Type ?u.57697
ι : Type u_2
ι' : Type ?u.57703
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
⊢ Independent (f ∘ Subtype.val) ↔ ∀ (i : ι), i ∈ s → Disjoint (f i) (Finset.sup (Finset.erase s i) f)
α : Type u_1
β : Type ?u.57697
ι : Type u_2
ι' : Type ?u.57703
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
⊢ Independent (f ∘ Subtype.val) ↔ Finset.SupIndep s f
rw [Finset.supIndep_iff_disjoint_erase]
α : Type u_1
β : Type ?u.57697
ι : Type u_2
ι' : Type ?u.57703
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
⊢ Disjoint ((f ∘ Subtype.val) { val := a, property := b })
      (⨆ (j : { x // x ∈ s }) (_ : j ≠ { val := a, property := b }), (f ∘ Subtype.val) j) ↔
    Disjoint (f a) (Finset.sup (Finset.erase s a) f)
α : Type u_1
β : Type ?u.57697
ι : Type u_2
ι' : Type ?u.57703
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
⊢ Independent (f ∘ Subtype.val) ↔ ∀ (i : ι), i ∈ s → Disjoint (f i) (Finset.sup (Finset.erase s i) f)
refine' Subtype.forall.trans (forall₂_congr fun a b => _)
α : Type u_1
β : Type ?u.57697
ι : Type u_2
ι' : Type ?u.57703
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
⊢ Disjoint ((f ∘ Subtype.val) { val := a, property := b })
      (⨆ (j : { x // x ∈ s }) (_ : j ≠ { val := a, property := b }), (f ∘ Subtype.val) j) ↔
    Disjoint (f a) (⨆ (a_1 : ι) (_ : a_1 ∈ Finset.erase s a), f a_1)
α : Type u_1
β : Type ?u.57697
ι : Type u_2
ι' : Type ?u.57703
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
⊢ Disjoint ((f ∘ Subtype.val) { val := a, property := b })
      (⨆ (j : { x // x ∈ s }) (_ : j ≠ { val := a, property := b }), (f ∘ Subtype.val) j) ↔
    Disjoint (f a) (Finset.sup (Finset.erase s a) f)
rw [Finset.sup_eq_iSup]
case a.h.e'_5
α : Type u_1
β : Type ?u.57697
ι : Type u_2
ι' : Type ?u.57703
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
⊢ (⨆ (j : { x // x ∈ s }) (_ : j ≠ { val := a, property := b }), (f ∘ Subtype.val) j) =
    ⨆ (a_1 : ι) (_ : a_1 ∈ Finset.erase s a), f a_1
α : Type u_1
β : Type ?u.57697
ι : Type u_2
ι' : Type ?u.57703
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
⊢ Disjoint ((f ∘ Subtype.val) { val := a, property := b })
      (⨆ (j : { x // x ∈ s }) (_ : j ≠ { val := a, property := b }), (f ∘ Subtype.val) j) ↔
    Disjoint (f a) (⨆ (a_1 : ι) (_ : a_1 ∈ Finset.erase s a), f a_1)
congr! 1
case a.h.e'_5
α : Type u_1
β : Type ?u.57697
ι : Type u_2
ι' : Type ?u.57703
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
⊢ (⨆ (i : ι) (h : i ∈ s) (_ : { val := i, property := h } ≠ { val := a, property := b }),
      (f ∘ Subtype.val) { val := i, property := h }) =
    ⨆ (a_1 : ι) (_ : a_1 ∈ Finset.erase s a), f a_1
case a.h.e'_5
α : Type u_1
β : Type ?u.57697
ι : Type u_2
ι' : Type ?u.57703
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
⊢ (⨆ (j : { x // x ∈ s }) (_ : j ≠ { val := a, property := b }), (f ∘ Subtype.val) j) =
    ⨆ (a_1 : ι) (_ : a_1 ∈ Finset.erase s a), f a_1
refine' iSup_subtype.trans _
case a.h.e'_5.h.e'_4
α : Type u_1
β : Type ?u.57697
ι : Type u_2
ι' : Type ?u.57703
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
⊢ (fun i =>
      ⨆ (h : i ∈ s) (_ : { val := i, property := h } ≠ { val := a, property := b }),
        (f ∘ Subtype.val) { val := i, property := h }) =
    fun a_1 => ⨆ (_ : a_1 ∈ Finset.erase s a), f a_1
case a.h.e'_5
α : Type u_1
β : Type ?u.57697
ι : Type u_2
ι' : Type ?u.57703
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
⊢ (⨆ (i : ι) (h : i ∈ s) (_ : { val := i, property := h } ≠ { val := a, property := b }),
      (f ∘ Subtype.val) { val := i, property := h }) =
    ⨆ (a_1 : ι) (_ : a_1 ∈ Finset.erase s a), f a_1
congr! 1
no goals
case a.h.e'_5.h.e'_4
α : Type u_1
β : Type ?u.57697
ι : Type u_2
ι' : Type ?u.57703
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
⊢ (fun i =>
      ⨆ (h : i ∈ s) (_ : { val := i, property := h } ≠ { val := a, property := b }),
        (f ∘ Subtype.val) { val := i, property := h }) =
    fun a_1 => ⨆ (_ : a_1 ∈ Finset.erase s a), f a_1
simp [iSup_and, @iSup_comm _ (_ ∈ s)]