-- Mathlib/Order/CompactlyGenerated/Basic.lean
lemma iSupIndep_iff_supIndep_of_injOn {ι : Type*} {f : ι → α}
    (hf : InjOn f {i | f i ≠ ⊥}) :
    iSupIndep f ↔ ∀ (s : Finset ι), s.SupIndep f

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
i : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
t : Finset α := s.erase ⊥
hf : InjOn f (f ⁻¹' ↑t)
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))

Tactic:
rw [Finset.supIndep_iff_disjoint_erase] at h

Result:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
i : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
t : Finset α := s.erase ⊥
hf : InjOn f (f ⁻¹' ↑t)
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))

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
t : Finset α := s.erase ⊥
hf : InjOn f (f ⁻¹' ↑t)
this : Finset.image f ((insert i (t.preimage f hf)).erase i) = t
⊢ Disjoint (f i) (t.sup id)

Tactic:
rw [← this, Finset.sup_image]

Result:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
t : Finset α := s.erase ⊥
hf : InjOn f (f ⁻¹' ↑t)
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))

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
t : Finset α := s.erase ⊥
hf : InjOn f (f ⁻¹' ↑t)
⊢ Disjoint (f i) (t.sup id)

Tactic:
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.mem_insert, true_or, not_true,
    Finset.erase_insert_eq_erase, not_and, Finset.mem_image, t]
  refine ⟨by aesop, fun ⟨ha, has⟩ ↦ ?_⟩
  obtain ⟨j, hj, rfl⟩ := hs has
  exact ⟨j, ⟨hj, ha, has⟩, rfl⟩

Result:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
t : Finset α := s.erase ⊥
hf : InjOn f (f ⁻¹' ↑t)
this : Finset.image f ((insert i (t.preimage f hf)).erase i) = t
⊢ Disjoint (f i) (t.sup id)

Proof state:
case h
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
t : Finset α := s.erase ⊥
hf : InjOn f (f ⁻¹' ↑t)
a : α
x✝ : ¬a = ⊥ ∧ a ∈ s
ha : ¬a = ⊥
has : a ∈ s
⊢ ∃ a_1, (¬a_1 = i ∧ ¬f a_1 = ⊥ ∧ f a_1 ∈ s) ∧ f a_1 = a

Tactic:
obtain ⟨j, hj, rfl⟩ := hs has

Result:
case h.intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
t : Finset α := s.erase ⊥
hf : InjOn f (f ⁻¹' ↑t)
j : ι
hj : j ∈ {j | j ≠ i}
x✝ : ¬f j = ⊥ ∧ f j ∈ s
ha : ¬f j = ⊥
has : f j ∈ s
⊢ ∃ a, (¬a = i ∧ ¬f a = ⊥ ∧ f a ∈ s) ∧ f a = f j

Proof state:
case h.intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
t : Finset α := s.erase ⊥
hf : InjOn f (f ⁻¹' ↑t)
j : ι
hj : j ∈ {j | j ≠ i}
x✝ : ¬f j = ⊥ ∧ f j ∈ s
ha : ¬f j = ⊥
has : f j ∈ s
⊢ ∃ a, (¬a = i ∧ ¬f a = ⊥ ∧ f a ∈ s) ∧ f a = f j

Tactic:
exact ⟨j, ⟨hj, ha, has⟩, rfl⟩

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
hf : InjOn f {i | f i ≠ ⊥}
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
⊢ Disjoint (f i) (s.sup id)

Tactic:
classical
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.mem_insert, true_or, not_true,
    Finset.erase_insert_eq_erase, not_and, 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 _)

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
hf : InjOn f {i | f i ≠ ⊥}
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
⊢ Disjoint (f i) (sSup (f '' {j | j ≠ i}))

Tactic:
simp_rw [disjoint_iff, inf_sSup_eq_iSup_inf_sup_finset, iSup_eq_bot, ← disjoint_iff]

Result:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
hf : InjOn f {i | f i ≠ ⊥}
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
⊢ ∀ (i_1 : Finset α), ↑i_1 ⊆ f '' {j | j ≠ i} → Disjoint (f i) (i_1.sup id)