-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
have : InjOn f {i : ι | f i ≠ ⊥}
have₁ : ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}), Disjoint (f i) (sSup (f '' {j : ι | j ≠ i}))
have₂ : InjOn f {i : ι | f i ≠ ⊥}
have₃ have₄ : ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}), Disjoint (f i) (sSup (f '' {j : ι | j ≠ i}))
have₅ :
  ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}) (i_1 : Finset α) (i_2 : (↑i_1 : Set α) ⊆ f '' {j : ι | j ≠ i}),
    Disjoint (f i) (i_1.sup id)
have₆ :
  ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}) (s : Finset α) (hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}),
    Disjoint (f i) (s.sup id)
have₇ :
  ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}) (s : Finset α) (hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}),
    Disjoint (f i) ((s.erase ⊥).sup id)
have₈ :
  ∀ (hf : InjOn f {i : ι | f i ≠ ⊥}) (s : Finset α) (hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}),
    let t := s.erase ⊥;
    Disjoint (f i) (t.sup id)
have₉ :
  ∀ (s : Finset α) (hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}),
    let t := s.erase ⊥;
    ∀ (hf : InjOn f (f ⁻¹' (↑t : Set α))), Disjoint (f i) (t.sup id)
have₁₀ :
  ∀ (s : Finset α) (hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}),
    let t := s.erase ⊥;
    ∀ (hf : InjOn f (f ⁻¹' (↑t : Set α))) (this : Finset.image f ((insert i (t.preimage f hf)).erase i) = t),
      Disjoint (f i) (t.sup id)
have₁₁ :
  ∀ (s : Finset α) (hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}),
    let t := s.erase ⊥;
    ∀ (hf : InjOn f (f ⁻¹' (↑t : Set α))) (this : Finset.image f ((insert i (t.preimage f hf)).erase i) = t),
      Disjoint (f i) (((insert i (t.preimage f hf)).erase i).sup (id ∘ f))
have₁₂ :
  ∀ (s : Finset α) (hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}),
    let t := s.erase ⊥;
    ∀ (hf : InjOn f (f ⁻¹' (↑t : Set α))) (this : Finset.image f ((insert i (t.preimage f hf)).erase i) = t)
      (h : (insert i (t.preimage f hf)).SupIndep f),
      Disjoint (f i) (((insert i (t.preimage f hf)).erase i).sup (id ∘ f))
have₁₃ :
  ∀ (s : Finset α) (hs : (↑s : Set α) ⊆ f '' {j : ι | j ≠ i}),
    let t := s.erase ⊥;
    ∀ (hf : InjOn f (f ⁻¹' (↑t : Set α))) (this : Finset.image f ((insert i (t.preimage f hf)).erase i) = t)
      (h : ∀ i_1 ∈ insert i (t.preimage f hf), Disjoint (f i_1) (((insert i (t.preimage f hf)).erase i_1).sup f)),
      Disjoint (f i) (((insert i (t.preimage f hf)).erase i).sup (id ∘ f))
⊢ Disjoint (f i) (sSup (f '' {j : ι | j ≠ i}))

Tactic:
classical
  have hf : Set.InjOn f {i : ι | f i ≠ ⊥} := by
    by_contra! hf
    simp_all only [Set.InjOn, ne_eq, Set.mem_setOf_eq, not_forall]
    obtain ⟨x₁, hx₁, x₂, hx₂, hfeq, hneq⟩ := hf
    specialize h ({x₁, x₂} : Finset ι)
    rw [Finset.supIndep_pair hneq, disjoint_iff, hfeq, inf_idem (f x₂)] at h
    contradiction
  simp_rw [disjoint_iff, inf_sSup_eq_iSup_inf_sup_finset, iSup_eq_bot, ← disjoint_iff]
  intro s hs
  rw [← Finset.sup_erase_bot]
  set t := s.erase ⊥
  replace hf : InjOn f (f ⁻¹' t) := fun i hi j _ hij ↦ by
    refine hf ?_ ?_ hij <;> aesop (add norm simp [t])
  have : (Finset.erase (insert i (t.preimage _ hf)) i).image f = t := by
    ext a
    simp only [Finset.mem_preimage, Finset.mem_erase, ne_eq,
      Finset.erase_insert_eq_erase, Finset.mem_image, t]
    refine ⟨by aesop, fun ⟨ha, has⟩ ↦ ?_⟩
    obtain ⟨j, hj, rfl⟩ := hs has
    exact ⟨j, ⟨hj, ha, has⟩, rfl⟩
  rw [← this, Finset.sup_image]
  specialize h (insert i (t.preimage _ hf))
  rw [Finset.supIndep_iff_disjoint_erase] at h
  exact h i (Finset.mem_insert_self i _)

Premises used: Finset.sup_erase_bot, disjoint_iff, inf_sSup_eq_iSup_inf_sup_finset, Finset.supIndep_iff_disjoint_erase, Finset.sup_image, iSup_eq_bot