-- Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
theorem cbiSup_eq_of_not_forall {p : ι → Prop} {f : Subtype p → α} (hp : ¬ (∀ i, p i)) :
    ⨆ (i) (h : p i), f ⟨i, h⟩ = iSup f ⊔ sSup ∅

Proof state:
case h.e'_5
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
i₀ : ι
hi₀ : ¬p i₀
this✝ : Nonempty ι
this : iSup f = sSup ∅
H : BddAbove (range fun i => if h : p i then f ⟨i, h⟩ else sSup ∅)
i : Subtype p
⊢ f i = if h : p ↑i then f ⟨↑i, h⟩ else sSup ∅

Tactic:
simp [i.2]

Result:
no goals

Proof state:
case pos
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
i₀ : ι
hi₀ : ¬p i₀
this : Nonempty ι
H : BddAbove (range f)
B : BddAbove (range fun i => if h : p i then f ⟨i, h⟩ else sSup ∅)
⊢ (⨆ i, if h : p i then f ⟨i, h⟩ else sSup ∅) = iSup f ⊔ sSup ∅

Tactic:
apply le_antisymm

Result:
case pos.a
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
i₀ : ι
hi₀ : ¬p i₀
this : Nonempty ι
H : BddAbove (range f)
B : BddAbove (range fun i => if h : p i then f ⟨i, h⟩ else sSup ∅)
⊢ (⨆ i, if h : p i then f ⟨i, h⟩ else sSup ∅) ≤ iSup f ⊔ sSup ∅

case pos.a
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
i₀ : ι
hi₀ : ¬p i₀
this : Nonempty ι
H : BddAbove (range f)
B : BddAbove (range fun i => if h : p i then f ⟨i, h⟩ else sSup ∅)
⊢ iSup f ⊔ sSup ∅ ≤ ⨆ i, if h : p i then f ⟨i, h⟩ else sSup ∅

Proof state:
case intro
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
i₀ : ι
hi₀ : ¬p i₀
this : Nonempty ι
c : α
hc : c ∈ upperBounds (range f)
⊢ c ⊔ sSup ∅ ∈ upperBounds (range fun i => if h : p i then f ⟨i, h⟩ else sSup ∅)

Tactic:
rintro - ⟨i, rfl⟩

Result:
case intro.intro
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
i₀ : ι
hi₀ : ¬p i₀
this : Nonempty ι
c : α
hc : c ∈ upperBounds (range f)
i : ι
⊢ (fun i => if h : p i then f ⟨i, h⟩ else sSup ∅) i ≤ c ⊔ sSup ∅

Proof state:
case neg.hs.intro
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
i₀ : ι
hi₀ : ¬p i₀
this✝ : Nonempty ι
this : iSup f = sSup ∅
H : BddAbove (range fun i => if h : p i then f ⟨i, h⟩ else sSup ∅)
i : Subtype p
⊢ f i ∈ range fun i => if h : p i then f ⟨i, h⟩ else sSup ∅

Tactic:
convert mem_range_self i.1

Result:
case h.e'_5
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
i₀ : ι
hi₀ : ¬p i₀
this✝ : Nonempty ι
this : iSup f = sSup ∅
H : BddAbove (range fun i => if h : p i then f ⟨i, h⟩ else sSup ∅)
i : Subtype p
⊢ f i = if h : p ↑i then f ⟨↑i, h⟩ else sSup ∅

Proof state:
case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
i₀ : ι
hi₀ : ¬p i₀
this : Nonempty ι
H : BddAbove (range f)
B : BddAbove (range fun i => if h : p i then f ⟨i, h⟩ else sSup ∅)
i : ι
hi : ¬p i
⊢ (if h : p i then f ⟨i, h⟩ else sSup ∅) ≤ iSup f ⊔ sSup ∅

Tactic:
simp [hi]

Result:
no goals

Proof state:
case pos.a.a
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
i₀ : ι
hi₀ : ¬p i₀
this : Nonempty ι
H : BddAbove (range f)
B : BddAbove (range fun i => if h : p i then f ⟨i, h⟩ else sSup ∅)
⊢ iSup f ≤ ⨆ i, if h : p i then f ⟨i, h⟩ else sSup ∅

Tactic:
rcases isEmpty_or_nonempty (Subtype p) with hp|hp

Result:
case pos.a.a.inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp✝ : ¬∀ (i : ι), p i
i₀ : ι
hi₀ : ¬p i₀
this : Nonempty ι
H : BddAbove (range f)
B : BddAbove (range fun i => if h : p i then f ⟨i, h⟩ else sSup ∅)
hp : IsEmpty (Subtype p)
⊢ iSup f ≤ ⨆ i, if h : p i then f ⟨i, h⟩ else sSup ∅

case pos.a.a.inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp✝ : ¬∀ (i : ι), p i
i₀ : ι
hi₀ : ¬p i₀
this : Nonempty ι
H : BddAbove (range f)
B : BddAbove (range fun i => if h : p i then f ⟨i, h⟩ else sSup ∅)
hp : Nonempty (Subtype p)
⊢ iSup f ≤ ⨆ i, if h : p i then f ⟨i, h⟩ else sSup ∅

Proof state:
case h.e'_3
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
i₀ : ι
hi₀ : ¬p i₀
this : Nonempty ι
H : BddAbove (range f)
B : BddAbove (range fun i => if h : p i then f ⟨i, h⟩ else sSup ∅)
⊢ sSup ∅ = if h : p i₀ then f ⟨i₀, h⟩ else sSup ∅

Tactic:
simp [hi₀]

Result:
no goals

Proof state:
case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
i₀ : ι
hi₀ : ¬p i₀
this✝ : Nonempty ι
H : ¬BddAbove (range f)
this : iSup f = sSup ∅
⊢ (⨆ i, if h : p i then f ⟨i, h⟩ else sSup ∅) = iSup f ⊔ sSup ∅

Tactic:
simp only [this, le_refl, sup_of_le_left]

Result:
case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
i₀ : ι
hi₀ : ¬p i₀
this✝ : Nonempty ι
H : ¬BddAbove (range f)
this : iSup f = sSup ∅
⊢ (⨆ i, if h : p i then f ⟨i, h⟩ else sSup ∅) = sSup ∅

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
i₀ : ι
hi₀ : ¬p i₀
this : Nonempty ι
H : BddAbove (range f)
B : BddAbove (range fun i => if h : p i then f ⟨i, h⟩ else sSup ∅)
i : ι
⊢ (if h : p i then f ⟨i, h⟩ else sSup ∅) ≤ iSup f ⊔ sSup ∅

Tactic:
by_cases hi : p i

Result:
case pos
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
i₀ : ι
hi₀ : ¬p i₀
this : Nonempty ι
H : BddAbove (range f)
B : BddAbove (range fun i => if h : p i then f ⟨i, h⟩ else sSup ∅)
i : ι
hi : p i
⊢ (if h : p i then f ⟨i, h⟩ else sSup ∅) ≤ iSup f ⊔ sSup ∅

case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
i₀ : ι
hi₀ : ¬p i₀
this : Nonempty ι
H : BddAbove (range f)
B : BddAbove (range fun i => if h : p i then f ⟨i, h⟩ else sSup ∅)
i : ι
hi : ¬p i
⊢ (if h : p i then f ⟨i, h⟩ else sSup ∅) ≤ iSup f ⊔ sSup ∅

Proof state:
case intro
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
i₀ : ι
hi₀ : ¬p i₀
this : Nonempty ι
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = iSup f ⊔ sSup ∅

Tactic:
simp only [ciSup_eq_ite]

Result:
case intro
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
i₀ : ι
hi₀ : ¬p i₀
this : Nonempty ι
⊢ (⨆ i, if h : p i then f ⟨i, h⟩ else sSup ∅) = iSup f ⊔ sSup ∅

Proof state:
case intro
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
i₀ : ι
hi₀ : ¬p i₀
this : Nonempty ι
c : α
hc : c ∈ upperBounds (range f)
⊢ BddAbove (range fun i => if h : p i then f ⟨i, h⟩ else sSup ∅)

Tactic:
refine ⟨c ⊔ sSup ∅, ?_⟩

Result:
case intro
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
i₀ : ι
hi₀ : ¬p i₀
this : Nonempty ι
c : α
hc : c ∈ upperBounds (range f)
⊢ c ⊔ sSup ∅ ∈ upperBounds (range fun i => if h : p i then f ⟨i, h⟩ else sSup ∅)