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

Tactic:
apply sup_le

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

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

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 ∅)
⊢ 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 ∅)
⊢ sSup ∅ = 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 ι
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_false, le_sup_right]

Result:
no goals

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

Tactic:
apply ciSup_le

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

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

Tactic:
simp only [hi, dite_true, le_sup_iff]

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

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

Tactic:
apply ciSup_le (fun i ↦ ?_)

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

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

Tactic:
contrapose! H

Result:
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 ∅)
⊢ BddAbove (range f)

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

Tactic:
have : iSup f = sSup (∅ : Set α) := csSup_of_not_bddAbove H

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 ∅) = iSup f ⊔ sSup ∅

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

Tactic:
exact le_ciSup H _

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 ∅)
⊢ BddAbove (range f)

Tactic:
apply H.mono

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

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

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

Tactic:
rcases not_forall.1 hp with ⟨i₀, hi₀⟩

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