-- Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
theorem ciSup_subtype [Nonempty ι] {p : ι → Prop} [Nonempty (Subtype p)] {f : Subtype p → α}
    (hf : BddAbove (Set.range f)) (hf' : sSup ∅ ≤ iSup f) :
    iSup f = ⨆ (i) (h : p i), f ⟨i, h⟩

Proof state:
case neg
α : Type u_1
ι : Sort u_4
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
p : ι → Prop
inst✝ : Nonempty (Subtype p)
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
i : ι
h : p i
this : f ⟨i, h⟩ = (fun i => ⨆ (h : p i), f ⟨i, h⟩) i
a✝ : α
b : ι
h✝ : ¬p b
hb : sSup ∅ = a✝
⊢ a✝ = sSup ∅ ∨ ∃ a, ∃ (b : p a), f ⟨a, b⟩ = a✝

Tactic:
simp_all

Result:
no goals

Proof state:
case refine_2
α : Type u_1
ι : Sort u_4
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
p : ι → Prop
inst✝ : Nonempty (Subtype p)
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
i : ι
⊢ (if h : p i then f ⟨i, h⟩ else sSup ∅) ≤ iSup f

Tactic:
split_ifs

Result:
case pos
α : Type u_1
ι : Sort u_4
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
p : ι → Prop
inst✝ : Nonempty (Subtype p)
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
i : ι
h✝ : p i
⊢ f ⟨i, h✝⟩ ≤ iSup f

case neg
α : Type u_1
ι : Sort u_4
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
p : ι → Prop
inst✝ : Nonempty (Subtype p)
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
i : ι
h✝ : ¬p i
⊢ sSup ∅ ≤ iSup f

Proof state:
case refine_1
α : Type u_1
ι : Sort u_4
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
p : ι → Prop
inst✝ : Nonempty (Subtype p)
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
i : ι
h : p i
this : f ⟨i, h⟩ = (fun i => ⨆ (h : p i), f ⟨i, h⟩) i
⊢ BddAbove (range fun i => if h : p i then f ⟨i, h⟩ else sSup ∅)

Tactic:
refine (hf.union (bddAbove_singleton (a := sSup ∅))).mono ?_

Result:
case refine_1
α : Type u_1
ι : Sort u_4
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
p : ι → Prop
inst✝ : Nonempty (Subtype p)
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
i : ι
h : p i
this : f ⟨i, h⟩ = (fun i => ⨆ (h : p i), f ⟨i, h⟩) i
⊢ (range fun i => if h : p i then f ⟨i, h⟩ else sSup ∅) ⊆ range f ∪ {sSup ∅}

Proof state:
α : Type u_1
ι : Sort u_4
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
p : ι → Prop
inst✝ : Nonempty (Subtype p)
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
i : ι
h : p i
⊢ f ⟨i, h⟩ = (fun i => ⨆ (h : p i), f ⟨i, h⟩) i

Tactic:
simp [h]

Result:
no goals

Proof state:
case refine_1
α : Type u_1
ι : Sort u_4
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
p : ι → Prop
inst✝ : Nonempty (Subtype p)
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
i : ι
h : p i
this : f ⟨i, h⟩ = (fun i => ⨆ (h : p i), f ⟨i, h⟩) i
⊢ (range fun i => if h : p i then f ⟨i, h⟩ else sSup ∅) ⊆ range f ∪ {sSup ∅}

Tactic:
intro

Result:
case refine_1
α : Type u_1
ι : Sort u_4
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
p : ι → Prop
inst✝ : Nonempty (Subtype p)
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
i : ι
h : p i
this : f ⟨i, h⟩ = (fun i => ⨆ (h : p i), f ⟨i, h⟩) i
a✝ : α
⊢ (a✝ ∈ range fun i => if h : p i then f ⟨i, h⟩ else sSup ∅) → a✝ ∈ range f ∪ {sSup ∅}

Proof state:
case refine_1
α : Type u_1
ι : Sort u_4
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
p : ι → Prop
inst✝ : Nonempty (Subtype p)
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
⊢ ∀ (x : Subtype p), f x ≤ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩

Tactic:
intro ⟨i, h⟩

Result:
case refine_1
α : Type u_1
ι : Sort u_4
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
p : ι → Prop
inst✝ : Nonempty (Subtype p)
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
i : ι
h : p i
⊢ f ⟨i, h⟩ ≤ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩

Proof state:
case refine_2
α : Type u_1
ι : Sort u_4
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
p : ι → Prop
inst✝ : Nonempty (Subtype p)
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ ≤ iSup f

Tactic:
refine ciSup_le fun i ↦ ?_

Result:
case refine_2
α : Type u_1
ι : Sort u_4
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
p : ι → Prop
inst✝ : Nonempty (Subtype p)
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
i : ι
⊢ ⨆ (h : p i), f ⟨i, h⟩ ≤ iSup f

Proof state:
case refine_1
α : Type u_1
ι : Sort u_4
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
p : ι → Prop
inst✝ : Nonempty (Subtype p)
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
i : ι
h : p i
⊢ f ⟨i, h⟩ ≤ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩

Tactic:
have : f ⟨i, h⟩ = (fun i : ι ↦ ⨆ (h : p i), f ⟨i, h⟩) i := by simp [h]

Result:
case refine_1
α : Type u_1
ι : Sort u_4
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
p : ι → Prop
inst✝ : Nonempty (Subtype p)
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
i : ι
h : p i
this : f ⟨i, h⟩ = (fun i => ⨆ (h : p i), f ⟨i, h⟩) i
⊢ f ⟨i, h⟩ ≤ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩