-- Mathlib/Order/SupIndep.lean
theorem iSupIndep_iff_supIndep {s : Finset ι} {f : ι → α} :
    iSupIndep (f ∘ ((↑) : s → ι)) ↔ s.SupIndep f

Proof state:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
⊢ Disjoint ((f ∘ Subtype.val) ⟨a, b⟩) (⨆ j, ⨆ (_ : j ≠ ⟨a, b⟩), (f ∘ Subtype.val) j) ↔
    Disjoint (f a) ((s.erase a).sup f)

Tactic:
rw [Finset.sup_eq_iSup]

Result:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
⊢ Disjoint ((f ∘ Subtype.val) ⟨a, b⟩) (⨆ j, ⨆ (_ : j ≠ ⟨a, b⟩), (f ∘ Subtype.val) j) ↔
    Disjoint (f a) (⨆ a_1 ∈ s.erase a, f a_1)

Proof state:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
⊢ iSupIndep (f ∘ Subtype.val) ↔ s.SupIndep f

Tactic:
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)]

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
⊢ iSupIndep (f ∘ Subtype.val) ↔ ∀ i ∈ s, Disjoint (f i) ((s.erase i).sup f)

Tactic:
refine Subtype.forall.trans (forall₂_congr fun a b => ?_)

Result:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
⊢ Disjoint ((f ∘ Subtype.val) ⟨a, b⟩) (⨆ j, ⨆ (_ : j ≠ ⟨a, b⟩), (f ∘ Subtype.val) j) ↔
    Disjoint (f a) ((s.erase a).sup f)

Proof state:
case a.h.e'_5
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
⊢ ⨆ i, ⨆ (h : i ∈ s), ⨆ (_ : ⟨i, h⟩ ≠ ⟨a, b⟩), (f ∘ Subtype.val) ⟨i, h⟩ = ⨆ a_1 ∈ s.erase a, f a_1

Tactic:
congr! 1

Result:
case a.h.e'_5.h.e'_4
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
⊢ (fun i => ⨆ (h : i ∈ s), ⨆ (_ : ⟨i, h⟩ ≠ ⟨a, b⟩), (f ∘ Subtype.val) ⟨i, h⟩) = fun a_1 =>
    ⨆ (_ : a_1 ∈ s.erase a), f a_1

Proof state:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
⊢ Disjoint ((f ∘ Subtype.val) ⟨a, b⟩) (⨆ j, ⨆ (_ : j ≠ ⟨a, b⟩), (f ∘ Subtype.val) j) ↔
    Disjoint (f a) (⨆ a_1 ∈ s.erase a, f a_1)

Tactic:
congr! 1

Result:
case a.h.e'_5
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
⊢ ⨆ j, ⨆ (_ : j ≠ ⟨a, b⟩), (f ∘ Subtype.val) j = ⨆ a_1 ∈ s.erase a, f a_1

Proof state:
case a.h.e'_5
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
⊢ ⨆ j, ⨆ (_ : j ≠ ⟨a, b⟩), (f ∘ Subtype.val) j = ⨆ a_1 ∈ s.erase a, f a_1

Tactic:
refine iSup_subtype.trans ?_

Result:
case a.h.e'_5
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
⊢ ⨆ i, ⨆ (h : i ∈ s), ⨆ (_ : ⟨i, h⟩ ≠ ⟨a, b⟩), (f ∘ Subtype.val) ⟨i, h⟩ = ⨆ a_1 ∈ s.erase a, f a_1

Proof state:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
⊢ iSupIndep (f ∘ Subtype.val) ↔ s.SupIndep f

Tactic:
rw [Finset.supIndep_iff_disjoint_erase]

Result:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
⊢ iSupIndep (f ∘ Subtype.val) ↔ ∀ i ∈ s, Disjoint (f i) ((s.erase i).sup f)

Proof state:
case a.h.e'_5.h.e'_4
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
a : ι
b : a ∈ s
⊢ (fun i => ⨆ (h : i ∈ s), ⨆ (_ : ⟨i, h⟩ ≠ ⟨a, b⟩), (f ∘ Subtype.val) ⟨i, h⟩) = fun a_1 =>
    ⨆ (_ : a_1 ∈ s.erase a), f a_1

Tactic:
simp [iSup_and, @iSup_comm _ (_ ∈ s)]

Result:
no goals