-- 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 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
⊢ (fun i => ⨆ (h : p i), f ⟨i, h⟩) i ≤ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩

Tactic:
refine le_ciSup (f := (fun i : ι ↦ ⨆ (h : p i), f ⟨i, h⟩)) ?_ i

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
⊢ BddAbove (range fun i => ⨆ (h : p i), f ⟨i, h⟩)

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 => ⨆ (h : p i), f ⟨i, h⟩)

Tactic:
simp_rw [ciSup_eq_ite]

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
⊢ BddAbove (range fun i => if h : p i then f ⟨i, h⟩ else 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
i : ι
h : p i
this : f ⟨i, h⟩ = (fun i => ⨆ (h : p i), f ⟨i, h⟩) i
a✝ : α
b : ι
hb : (if h : p b then f ⟨b, h⟩ else sSup ∅) = a✝
⊢ a✝ = sSup ∅ ∨ ∃ a, ∃ (b : p a), f ⟨a, b⟩ = a✝

Tactic:
split_ifs at hb

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
this : f ⟨i, h⟩ = (fun i => ⨆ (h : p i), f ⟨i, h⟩) i
a✝ : α
b : ι
h✝ : p b
hb : f ⟨b, h✝⟩ = a✝
⊢ a✝ = sSup ∅ ∨ ∃ a, ∃ (b : p a), f ⟨a, b⟩ = a✝

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✝

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
a✝ : α
⊢ ∀ (x : ι), (if h : p x then f ⟨x, h⟩ else sSup ∅) = a✝ → a✝ = sSup ∅ ∨ ∃ a, ∃ (b : p a), f ⟨a, b⟩ = a✝

Tactic:
intro b hb

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✝ : α
b : ι
hb : (if h : p b then f ⟨b, h⟩ else sSup ∅) = a✝
⊢ a✝ = sSup ∅ ∨ ∃ a, ∃ (b : p a), f ⟨a, b⟩ = a✝

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
⊢ iSup f = ⨆ i, ⨆ (h : p i), f ⟨i, h⟩

Tactic:
refine le_antisymm (ciSup_le ?_) ?_

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
⊢ ∀ (x : Subtype p), f x ≤ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩

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_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:
simp_rw [ciSup_eq_ite]

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 : ι
⊢ (if h : p i then f ⟨i, h⟩ else sSup ∅) ≤ iSup f

Proof state:
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

Tactic:
exact le_ciSup hf ?_

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
a✝ : α
⊢ (a✝ ∈ range fun i => if h : p i then f ⟨i, h⟩ else sSup ∅) → a✝ ∈ range f ∪ {sSup ∅}

Tactic:
simp only [Set.mem_range, Set.union_singleton, Set.mem_insert_iff, Subtype.exists,
  forall_exists_index]

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✝ : α
⊢ ∀ (x : ι), (if h : p x then f ⟨x, h⟩ else sSup ∅) = a✝ → a✝ = sSup ∅ ∨ ∃ a, ∃ (b : p a), f ⟨a, b⟩ = a✝

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
⊢ f ⟨i, h⟩ ≤ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩

Tactic:
rw [this]

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
⊢ (fun i => ⨆ (h : p i), f ⟨i, h⟩) i ≤ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩

Proof state:
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
this : f ⟨i, h⟩ = (fun i => ⨆ (h : p i), f ⟨i, h⟩) i
a✝ : α
b : ι
h✝ : p b
hb : f ⟨b, h✝⟩ = a✝
⊢ a✝ = sSup ∅ ∨ ∃ a, ∃ (b : p a), f ⟨a, b⟩ = a✝

Tactic:
exact Or.inr ⟨_, _, hb⟩

Result:
no goals

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
⊢ sSup ∅ ≤ iSup f

Tactic:
exact hf'

Result:
no goals