-- Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
lemma ciSup_image {α ι ι' : Type*} [ConditionallyCompleteLattice α] [Nonempty ι] [Nonempty ι']
    {s : Set ι} (hs : s.Nonempty) {f : ι → ι'} {g : ι' → α}
    (hf : BddAbove (Set.range fun i : s ↦ g (f i))) (hg' : sSup ∅ ≤ ⨆ i : s, g (f i)) :
    ⨆ i ∈ (f '' s), g i = ⨆ x ∈ s, g (f x)

Proof state:
α : Type u_5
ι : Type u_6
ι' : Type u_7
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
s : Set ι
hs : s.Nonempty
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i => g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hg : BddAbove (range fun i => g ↑i)
⊢ ⨆ i, g (f ↑i) ≤ ⨆ i, g ↑i

Tactic:
have : Nonempty s := Set.Nonempty.to_subtype hs

Result:
α : Type u_5
ι : Type u_6
ι' : Type u_7
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
s : Set ι
hs : s.Nonempty
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i => g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hg : BddAbove (range fun i => g ↑i)
this : Nonempty ↑s
⊢ ⨆ i, g (f ↑i) ≤ ⨆ i, g ↑i

Proof state:
α : Type u_5
ι : Type u_6
ι' : Type u_7
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
s : Set ι
hs : s.Nonempty
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i => g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hg : BddAbove (range fun i => g ↑i)
hf' : sSup ∅ ≤ ⨆ i, g ↑i
⊢ ⨆ i ∈ f '' s, g i = ⨆ x ∈ s, g (f x)

Tactic:
rw [← csSup_image (by simpa using hs) hg hf', ← csSup_image hs hf hg', ← Set.image_comp, comp_def]

Result:
no goals

Proof state:
α : Type u_5
ι : Type u_6
ι' : Type u_7
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
s : Set ι
hs : s.Nonempty
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i => g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hg : BddAbove (range fun i => g ↑i)
hf' : sSup ∅ ≤ ⨆ i, g ↑i
⊢ (f '' s).Nonempty

Tactic:
simpa using hs

Result:
no goals

Proof state:
α : Type u_5
ι : Type u_6
ι' : Type u_7
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
s : Set ι
hs : s.Nonempty
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i => g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
⊢ ⨆ i ∈ f '' s, g i = ⨆ x ∈ s, g (f x)

Tactic:
have hg : BddAbove (Set.range fun i : f '' s ↦ g i) := by
  simpa [bddAbove_def] using hf

Result:
α : Type u_5
ι : Type u_6
ι' : Type u_7
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
s : Set ι
hs : s.Nonempty
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i => g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hg : BddAbove (range fun i => g ↑i)
⊢ ⨆ i ∈ f '' s, g i = ⨆ x ∈ s, g (f x)

Proof state:
α : Type u_5
ι : Type u_6
ι' : Type u_7
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
s : Set ι
hs : s.Nonempty
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i => g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hg : BddAbove (range fun i => g ↑i)
⊢ sSup ∅ ≤ ⨆ i, g ↑i

Tactic:
refine hg'.trans ?_

Result:
α : Type u_5
ι : Type u_6
ι' : Type u_7
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
s : Set ι
hs : s.Nonempty
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i => g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hg : BddAbove (range fun i => g ↑i)
⊢ ⨆ i, g (f ↑i) ≤ ⨆ i, g ↑i

Proof state:
α : Type u_5
ι : Type u_6
ι' : Type u_7
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
s : Set ι
hs : s.Nonempty
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i => g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
⊢ BddAbove (range fun i => g ↑i)

Tactic:
simpa [bddAbove_def] using hf

Result:
no goals

Proof state:
α : Type u_5
ι : Type u_6
ι' : Type u_7
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
s : Set ι
hs : s.Nonempty
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i => g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hg : BddAbove (range fun i => g ↑i)
this✝ : Nonempty ↑s
i : ι
h : i ∈ s
this : f i ∈ f '' s
⊢ g ↑⟨f i, this⟩ = g (f ↑⟨i, h⟩)

Tactic:
simp [this]

Result:
no goals

Proof state:
α : Type u_5
ι : Type u_6
ι' : Type u_7
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
s : Set ι
hs : s.Nonempty
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i => g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hg : BddAbove (range fun i => g ↑i)
this : Nonempty ↑s
i : ι
h : i ∈ s
⊢ g (f ↑⟨i, h⟩) ≤ ⨆ i, g ↑i

Tactic:
obtain ⟨t, ht⟩ : ∃ t : f '' s, g t = g (f (Subtype.mk i h)) := by
  have : f i ∈ f '' s := Set.mem_image_of_mem _ h
  exact ⟨⟨f i, this⟩, by simp [this]⟩

Result:
case intro
α : Type u_5
ι : Type u_6
ι' : Type u_7
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
s : Set ι
hs : s.Nonempty
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i => g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hg : BddAbove (range fun i => g ↑i)
this : Nonempty ↑s
i : ι
h : i ∈ s
t : ↑(f '' s)
ht : g ↑t = g (f ↑⟨i, h⟩)
⊢ g (f ↑⟨i, h⟩) ≤ ⨆ i, g ↑i

Proof state:
α : Type u_5
ι : Type u_6
ι' : Type u_7
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
s : Set ι
hs : s.Nonempty
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i => g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hg : BddAbove (range fun i => g ↑i)
this : Nonempty ↑s
⊢ ∀ (x : ↑s), g (f ↑x) ≤ ⨆ i, g ↑i

Tactic:
intro ⟨i, h⟩

Result:
α : Type u_5
ι : Type u_6
ι' : Type u_7
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
s : Set ι
hs : s.Nonempty
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i => g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hg : BddAbove (range fun i => g ↑i)
this : Nonempty ↑s
i : ι
h : i ∈ s
⊢ g (f ↑⟨i, h⟩) ≤ ⨆ i, g ↑i

Proof state:
case intro
α : Type u_5
ι : Type u_6
ι' : Type u_7
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
s : Set ι
hs : s.Nonempty
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i => g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hg : BddAbove (range fun i => g ↑i)
this : Nonempty ↑s
i : ι
h : i ∈ s
t : ↑(f '' s)
ht : g ↑t = g (f ↑⟨i, h⟩)
⊢ BddAbove (g '' (f '' s))

Tactic:
simpa [bddAbove_def] using hf

Result:
no goals

Proof state:
α : Type u_5
ι : Type u_6
ι' : Type u_7
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
s : Set ι
hs : s.Nonempty
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i => g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hg : BddAbove (range fun i => g ↑i)
⊢ ⨆ i ∈ f '' s, g i = ⨆ x ∈ s, g (f x)

Tactic:
have hf' : sSup ∅ ≤ ⨆ i : f '' s, g i := by
  refine hg'.trans ?_
  have : Nonempty s := Set.Nonempty.to_subtype hs
  refine ciSup_le ?_
  intro ⟨i, h⟩
  obtain ⟨t, ht⟩ : ∃ t : f '' s, g t = g (f (Subtype.mk i h)) := by
    have : f i ∈ f '' s := Set.mem_image_of_mem _ h
    exact ⟨⟨f i, this⟩, by simp [this]⟩
  rw [← ht]
  refine le_ciSup_set ?_ t.prop
  simpa [bddAbove_def] using hf

Result:
α : Type u_5
ι : Type u_6
ι' : Type u_7
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
s : Set ι
hs : s.Nonempty
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i => g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hg : BddAbove (range fun i => g ↑i)
hf' : sSup ∅ ≤ ⨆ i, g ↑i
⊢ ⨆ i ∈ f '' s, g i = ⨆ x ∈ s, g (f x)

Proof state:
case intro
α : Type u_5
ι : Type u_6
ι' : Type u_7
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
s : Set ι
hs : s.Nonempty
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i => g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hg : BddAbove (range fun i => g ↑i)
this : Nonempty ↑s
i : ι
h : i ∈ s
t : ↑(f '' s)
ht : g ↑t = g (f ↑⟨i, h⟩)
⊢ g (f ↑⟨i, h⟩) ≤ ⨆ i, g ↑i

Tactic:
rw [← ht]

Result:
case intro
α : Type u_5
ι : Type u_6
ι' : Type u_7
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
s : Set ι
hs : s.Nonempty
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i => g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hg : BddAbove (range fun i => g ↑i)
this : Nonempty ↑s
i : ι
h : i ∈ s
t : ↑(f '' s)
ht : g ↑t = g (f ↑⟨i, h⟩)
⊢ g ↑t ≤ ⨆ i, g ↑i