-- 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 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 ∅

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 ι
c : α
hc : c ∈ upperBounds (range f)
i : ι
hi : p i
⊢ (fun i => if h : p i then f ⟨i, h⟩ else sSup ∅) i ≤ c ⊔ 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 ι
c : α
hc : c ∈ upperBounds (range f)
i : ι
hi : ¬p i
⊢ (fun i => if h : p i then f ⟨i, h⟩ else sSup ∅) i ≤ c ⊔ sSup ∅

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

Tactic:
convert le_ciSup B i₀

Result:
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 ∅)
hp : IsEmpty (Subtype p)
⊢ sSup ∅ = if h : p i₀ then f ⟨i₀, h⟩ else sSup ∅

Proof state:
case pos.a.a.inr.H
α : 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)
⊢ ∀ (x : Subtype p), f x ≤ ⨆ i, if h : p i then f ⟨i, h⟩ else sSup ∅

Tactic:
rintro ⟨i, hi⟩

Result:
case pos.a.a.inr.H.mk
α : 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)
i : ι
hi : p i
⊢ f ⟨i, hi⟩ ≤ ⨆ 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₀
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = iSup f ⊔ sSup ∅

Tactic:
have : Nonempty ι := ⟨i₀⟩

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, ⨆ (h : p i), f ⟨i, h⟩ = iSup f ⊔ 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 ∅)
hp : Nonempty (Subtype p)
i : ι
hi : p i
⊢ f ⟨i, hi⟩ = if h : p i then f ⟨i, h⟩ else sSup ∅

Tactic:
simp [hi]

Result:
no goals

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 ∅)
hp : IsEmpty (Subtype p)
⊢ sSup ∅ = if h : p i₀ then f ⟨i₀, h⟩ else sSup ∅

Tactic:
simp [hi₀]

Result:
no goals

Proof state:
case neg.hs
α : 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 ∅)
⊢ range f ⊆ range fun i => if h : p i then f ⟨i, h⟩ else sSup ∅

Tactic:
rintro - ⟨i, rfl⟩

Result:
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 ∅

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)
⊢ BddAbove (range fun i => if h : p i then f ⟨i, h⟩ else sSup ∅)

Tactic:
rcases H with ⟨c, hc⟩

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)
⊢ BddAbove (range fun i => if h : p i then f ⟨i, h⟩ else sSup ∅)

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

Tactic:
rw [iSup_of_empty']

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

Tactic:
by_cases H : BddAbove (range f)

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

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 : ι
hi : p i
⊢ f ⟨i, ⋯⟩ ≤ iSup f ∨ f ⟨i, ⋯⟩ ≤ sSup ∅

Tactic:
left

Result:
case pos.h
α : 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
⊢ f ⟨i, ⋯⟩ ≤ iSup f

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 ι
c : α
hc : c ∈ upperBounds (range f)
i : ι
hi : p i
⊢ (fun i => if h : p i then f ⟨i, h⟩ else sSup ∅) i ≤ c ⊔ sSup ∅

Tactic:
simp only [hi, dite_true, le_sup_iff, hc (mem_range_self _), true_or]

Result:
no goals