-- Mathlib/Order/SupIndep.lean
theorem iSupIndep_ne_bot :
    iSupIndep (fun i : {i // t i ≠ ⊥} ↦ t i) ↔ iSupIndep t

Proof state:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
h : ∀ (i : { i // t i ≠ ⊥ }), Disjoint (t ↑i) (⨆ j, ⨆ (_ : j ≠ i), t ↑j)
⊢ ∀ (i : ι), Disjoint (t i) (⨆ j, ⨆ (_ : j ≠ i), t j)

Tactic:
intro i

Result:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
h : ∀ (i : { i // t i ≠ ⊥ }), Disjoint (t ↑i) (⨆ j, ⨆ (_ : j ≠ i), t ↑j)
i : ι
⊢ Disjoint (t i) (⨆ j, ⨆ (_ : j ≠ i), t j)

Proof state:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
h : ∀ (i : { i // t i ≠ ⊥ }), Disjoint (t ↑i) (⨆ j, ⨆ (_ : j ≠ i), t ↑j)
i : ι
⊢ Disjoint (t i) (⨆ j, ⨆ (_ : j ≠ i), t j)

Tactic:
cases eq_or_ne (t i) ⊥ with
| inl hi => simp [hi]
| inr hi => ?_

Result:
case inr
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
h : ∀ (i : { i // t i ≠ ⊥ }), Disjoint (t ↑i) (⨆ j, ⨆ (_ : j ≠ i), t ↑j)
i : ι
hi : t i ≠ ⊥
⊢ Disjoint (t i) (⨆ j, ⨆ (_ : j ≠ i), t j)

Proof state:
case h.e'_5
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
h : ∀ (i : { i // t i ≠ ⊥ }), Disjoint (t ↑i) (⨆ j, ⨆ (_ : j ≠ i), t ↑j)
i : ι
hi : t i ≠ ⊥
⊢ ⨆ j, ⨆ (_ : j ≠ i), t j = ⨆ j, ⨆ (_ : j ≠ ⟨i, hi⟩), t ↑j

Tactic:
have : ∀ j, ⨆ (_ : t j = ⊥), t j = ⊥ := fun j ↦ by simp only [iSup_eq_bot, imp_self]

Result:
case h.e'_5
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
h : ∀ (i : { i // t i ≠ ⊥ }), Disjoint (t ↑i) (⨆ j, ⨆ (_ : j ≠ i), t ↑j)
i : ι
hi : t i ≠ ⊥
this : ∀ (j : ι), ⨆ (_ : t j = ⊥), t j = ⊥
⊢ ⨆ j, ⨆ (_ : j ≠ i), t j = ⨆ j, ⨆ (_ : j ≠ ⟨i, hi⟩), t ↑j

Proof state:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
h : iSupIndep fun i => t ↑i
⊢ iSupIndep t

Tactic:
simp only [iSupIndep_def] at h ⊢

Result:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
h : ∀ (i : { i // t i ≠ ⊥ }), Disjoint (t ↑i) (⨆ j, ⨆ (_ : j ≠ i), t ↑j)
⊢ ∀ (i : ι), Disjoint (t i) (⨆ j, ⨆ (_ : j ≠ i), t j)

Proof state:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
h : ∀ (i : { i // t i ≠ ⊥ }), Disjoint (t ↑i) (⨆ j, ⨆ (_ : j ≠ i), t ↑j)
i : ι
hi : t i ≠ ⊥
j : ι
⊢ ⨆ (_ : t j = ⊥), t j = ⊥

Tactic:
simp only [iSup_eq_bot, imp_self]

Result:
no goals

Proof state:
case h.e'_5
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
h : ∀ (i : { i // t i ≠ ⊥ }), Disjoint (t ↑i) (⨆ j, ⨆ (_ : j ≠ i), t ↑j)
i : ι
hi : t i ≠ ⊥
this : ∀ (j : ι), ⨆ (_ : t j = ⊥), t j = ⊥
⊢ ⨆ j, ⨆ (_ : j ≠ i), t j = ⨆ j, ⨆ (_ : j ≠ ⟨i, hi⟩), t ↑j

Tactic:
rw [iSup_split _ (fun j ↦ t j = ⊥), iSup_subtype]

Result:
case h.e'_5
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
h : ∀ (i : { i // t i ≠ ⊥ }), Disjoint (t ↑i) (⨆ j, ⨆ (_ : j ≠ i), t ↑j)
i : ι
hi : t i ≠ ⊥
this : ∀ (j : ι), ⨆ (_ : t j = ⊥), t j = ⊥
⊢ (⨆ i_1, ⨆ (_ : t i_1 = ⊥), ⨆ (_ : i_1 ≠ i), t i_1) ⊔ ⨆ i_1, ⨆ (_ : ¬t i_1 = ⊥), ⨆ (_ : i_1 ≠ i), t i_1 =
    ⨆ i_1, ⨆ (h : t i_1 ≠ ⊥), ⨆ (_ : ⟨i_1, h⟩ ≠ ⟨i, hi⟩), t ↑⟨i_1, h⟩

Proof state:
case h.e'_5
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
h : ∀ (i : { i // t i ≠ ⊥ }), Disjoint (t ↑i) (⨆ j, ⨆ (_ : j ≠ i), t ↑j)
i : ι
hi : t i ≠ ⊥
this : ∀ (j : ι), ⨆ (_ : t j = ⊥), t j = ⊥
⊢ (⨆ i_1, ⨆ (_ : t i_1 = ⊥), ⨆ (_ : i_1 ≠ i), t i_1) ⊔ ⨆ i_1, ⨆ (_ : ¬t i_1 = ⊥), ⨆ (_ : i_1 ≠ i), t i_1 =
    ⨆ i_1, ⨆ (h : t i_1 ≠ ⊥), ⨆ (_ : ⟨i_1, h⟩ ≠ ⟨i, hi⟩), t ↑⟨i_1, h⟩

Tactic:
simp only [iSup_comm (ι' := _ ≠ i), this, ne_eq, sup_of_le_right, Subtype.mk.injEq, iSup_bot,
  bot_le]

Result:
no goals

Proof state:
case inl
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
h : ∀ (i : { i // t i ≠ ⊥ }), Disjoint (t ↑i) (⨆ j, ⨆ (_ : j ≠ i), t ↑j)
i : ι
hi : t i = ⊥
⊢ Disjoint (t i) (⨆ j, ⨆ (_ : j ≠ i), t j)

Tactic:
simp [hi]

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
⊢ (iSupIndep fun i => t ↑i) ↔ iSupIndep t

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.comp Subtype.val_injective⟩

Result:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
h : iSupIndep fun i => t ↑i
⊢ iSupIndep t

Proof state:
case inr
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
h : ∀ (i : { i // t i ≠ ⊥ }), Disjoint (t ↑i) (⨆ j, ⨆ (_ : j ≠ i), t ↑j)
i : ι
hi : t i ≠ ⊥
⊢ Disjoint (t i) (⨆ j, ⨆ (_ : j ≠ i), t j)

Tactic:
convert h ⟨i, hi⟩

Result:
case h.e'_5
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
h : ∀ (i : { i // t i ≠ ⊥ }), Disjoint (t ↑i) (⨆ j, ⨆ (_ : j ≠ i), t ↑j)
i : ι
hi : t i ≠ ⊥
⊢ ⨆ j, ⨆ (_ : j ≠ i), t j = ⨆ j, ⨆ (_ : j ≠ ⟨i, hi⟩), t ↑j