Theorem: bciSup_of_emptyset (Carleson/Theorem1_1/Carleson_on_the_real_line.lean)

State before:
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
⊢ ⨆ i ∈ ∅, f i = sSup ∅
Tactic:
rw [iSup]
State after:
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
⊢ sSup (Set.range fun i => ⨆ (_ : i ∈ ∅), f i) = sSup ∅

State before:
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
⊢ sSup (Set.range fun i => ⨆ (_ : i ∈ ∅), f i) = sSup ∅
Tactic:
convert csSup_singleton _
State after:
case h.e'_2.h.e'_3
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
⊢ (Set.range fun i => ⨆ (_ : i ∈ ∅), f i) = {sSup ∅}

State before:
case h.e'_2.h.e'_3
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
⊢ (Set.range fun i => ⨆ (_ : i ∈ ∅), f i) = {sSup ∅}
Tactic:
have : ∀ i : ι, IsEmpty (i ∈ (∅ : Set ι)) := by
  intro i
  simp
State after:
case h.e'_2.h.e'_3
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
this : ∀ (i : ι), IsEmpty (i ∈ ∅)
⊢ (Set.range fun i => ⨆ (_ : i ∈ ∅), f i) = {sSup ∅}

State before:
case h.e'_2.h.e'_3
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
this : ∀ (i : ι), IsEmpty (i ∈ ∅)
⊢ (Set.range fun i => ⨆ (_ : i ∈ ∅), f i) = {sSup ∅}
Tactic:
have : (fun (i : ι) ↦ ⨆ (_ : i ∈ (∅ : Set ι)), f i) = fun i ↦ sSup ∅ := by
  ext i
  rw [iSup]
  congr
  rw [Set.range_eq_empty_iff]
  simp
State after:
case h.e'_2.h.e'_3
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
this✝ : ∀ (i : ι), IsEmpty (i ∈ ∅)
this : (fun i => ⨆ (_ : i ∈ ∅), f i) = fun i => sSup ∅
⊢ (Set.range fun i => ⨆ (_ : i ∈ ∅), f i) = {sSup ∅}

State before:
case h.e'_2.h.e'_3
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
this✝ : ∀ (i : ι), IsEmpty (i ∈ ∅)
this : (fun i => ⨆ (_ : i ∈ ∅), f i) = fun i => sSup ∅
⊢ (Set.range fun i => ⨆ (_ : i ∈ ∅), f i) = {sSup ∅}
Tactic:
rw [this]
State after:
case h.e'_2.h.e'_3
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
this✝ : ∀ (i : ι), IsEmpty (i ∈ ∅)
this : (fun i => ⨆ (_ : i ∈ ∅), f i) = fun i => sSup ∅
⊢ (Set.range fun i => sSup ∅) = {sSup ∅}

State before:
case h.e'_2.h.e'_3
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
this✝ : ∀ (i : ι), IsEmpty (i ∈ ∅)
this : (fun i => ⨆ (_ : i ∈ ∅), f i) = fun i => sSup ∅
⊢ (Set.range fun i => sSup ∅) = {sSup ∅}
Tactic:
apply Set.range_const
State after:
no goals

State before:
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
⊢ ∀ (i : ι), IsEmpty (i ∈ ∅)
Tactic:
intro i
State after:
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
i : ι
⊢ IsEmpty (i ∈ ∅)

State before:
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
i : ι
⊢ IsEmpty (i ∈ ∅)
Tactic:
simp
State after:
no goals

State before:
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
this : ∀ (i : ι), IsEmpty (i ∈ ∅)
⊢ (fun i => ⨆ (_ : i ∈ ∅), f i) = fun i => sSup ∅
Tactic:
ext i
State after:
case h
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
this : ∀ (i : ι), IsEmpty (i ∈ ∅)
i : ι
⊢ ⨆ (_ : i ∈ ∅), f i = sSup ∅

State before:
case h
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
this : ∀ (i : ι), IsEmpty (i ∈ ∅)
i : ι
⊢ ⨆ (_ : i ∈ ∅), f i = sSup ∅
Tactic:
rw [iSup]
State after:
case h
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
this : ∀ (i : ι), IsEmpty (i ∈ ∅)
i : ι
⊢ sSup (Set.range fun x => f i) = sSup ∅

State before:
case h
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
this : ∀ (i : ι), IsEmpty (i ∈ ∅)
i : ι
⊢ sSup (Set.range fun x => f i) = sSup ∅
Tactic:
congr
State after:
case h.e_a
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
this : ∀ (i : ι), IsEmpty (i ∈ ∅)
i : ι
⊢ (Set.range fun x => f i) = ∅

State before:
case h.e_a
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
this : ∀ (i : ι), IsEmpty (i ∈ ∅)
i : ι
⊢ (Set.range fun x => f i) = ∅
Tactic:
rw [Set.range_eq_empty_iff]
State after:
case h.e_a
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
this : ∀ (i : ι), IsEmpty (i ∈ ∅)
i : ι
⊢ IsEmpty (i ∈ ∅)

State before:
case h.e_a
α : Type
inst✝¹ : ConditionallyCompleteLattice α
ι : Type
inst✝ : Nonempty ι
f : ι → α
this : ∀ (i : ι), IsEmpty (i ∈ ∅)
i : ι
⊢ IsEmpty (i ∈ ∅)
Tactic:
simp
State after:
no goals