Theorem: ConditionallyCompleteLattice.le_biSup (Carleson/Theorem1_1/Carleson_on_the_real_line.lean)

State before:
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
ha : ∃ i ∈ s, f i = a
⊢ a ≤ ⨆ i ∈ s, f i
Tactic:
apply ConditionallyCompleteLattice.le_csSup
State after:
case a
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
ha : ∃ i ∈ s, f i = a
⊢ BddAbove (Set.range fun i => ⨆ (_ : i ∈ s), f i)

case a
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
ha : ∃ i ∈ s, f i = a
⊢ a ∈ Set.range fun i => ⨆ (_ : i ∈ s), f i

State before:
case a
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
ha : ∃ i ∈ s, f i = a
⊢ BddAbove (Set.range fun i => ⨆ (_ : i ∈ s), f i)

case a
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
ha : ∃ i ∈ s, f i = a
⊢ a ∈ Set.range fun i => ⨆ (_ : i ∈ s), f i
Tactic:
. rw [bddAbove_def] at *
  rcases hfs with ⟨x, hx⟩
  use (max x (sSup ∅))
  intro y hy
  simp at hy
  rcases hy with ⟨z, hz⟩
  rw [iSup] at hz
  by_cases h : z ∈ s
  . have : (@Set.range α (z ∈ s) fun _ ↦ f z) = {f z} := by
      rw [Set.eq_singleton_iff_unique_mem]
      constructor
      . simpa
      . intro x hx
        simp at hx
        exact hx.2.symm
    rw [this] at hz
    have : sSup {f z} = f z := by apply csSup_singleton
    rw [this] at hz
    simp at hx
    have : f z ≤ x := hx z h
    rw [hz] at this
    apply le_max_of_le_left this
  have : (@Set.range α (z ∈ s) fun _ ↦ f z) = ∅ := by
    simpa
  rw [this] at hz
  rw [hz]
  exact le_max_right x y
State after:
case a
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
ha : ∃ i ∈ s, f i = a
⊢ a ∈ Set.range fun i => ⨆ (_ : i ∈ s), f i

State before:
case a
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
ha : ∃ i ∈ s, f i = a
⊢ a ∈ Set.range fun i => ⨆ (_ : i ∈ s), f i
Tactic:
rw [Set.mem_range]
State after:
case a
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
ha : ∃ i ∈ s, f i = a
⊢ ∃ y, ⨆ (_ : y ∈ s), f y = a

State before:
case a
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
ha : ∃ i ∈ s, f i = a
⊢ ∃ y, ⨆ (_ : y ∈ s), f y = a
Tactic:
rcases ha with ⟨i, hi, fia⟩
State after:
case a.intro.intro
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ ∃ y, ⨆ (_ : y ∈ s), f y = a

State before:
case a.intro.intro
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ ∃ y, ⨆ (_ : y ∈ s), f y = a
Tactic:
use i
State after:
case h
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ ⨆ (_ : i ∈ s), f i = a

State before:
case h
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ ⨆ (_ : i ∈ s), f i = a
Tactic:
rw [iSup]
State after:
case h
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ sSup (Set.range fun h => f i) = a

State before:
case h
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ sSup (Set.range fun h => f i) = a
Tactic:
convert csSup_singleton _
State after:
case h.e'_2.h.e'_3
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ (Set.range fun h => f i) = {a}

State before:
case h.e'_2.h.e'_3
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ (Set.range fun h => f i) = {a}
Tactic:
rw [Set.eq_singleton_iff_unique_mem]
State after:
case h.e'_2.h.e'_3
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ (a ∈ Set.range fun h => f i) ∧ ∀ x ∈ Set.range fun h => f i, x = a

State before:
case h.e'_2.h.e'_3
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ (a ∈ Set.range fun h => f i) ∧ ∀ x ∈ Set.range fun h => f i, x = a
Tactic:
constructor
State after:
case h.e'_2.h.e'_3.left
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ a ∈ Set.range fun h => f i

case h.e'_2.h.e'_3.right
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ ∀ x ∈ Set.range fun h => f i, x = a

State before:
case h.e'_2.h.e'_3.left
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ a ∈ Set.range fun h => f i

case h.e'_2.h.e'_3.right
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ ∀ x ∈ Set.range fun h => f i, x = a
Tactic:
. simp
  use hi, fia
State after:
case h.e'_2.h.e'_3.right
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ ∀ x ∈ Set.range fun h => f i, x = a

State before:
case h.e'_2.h.e'_3.right
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ ∀ x ∈ Set.range fun h => f i, x = a
Tactic:
. intro x hx
  simp at hx
  rwa [hx.2] at fia
State after:
no goals

State before:
case a
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
ha : ∃ i ∈ s, f i = a
⊢ BddAbove (Set.range fun i => ⨆ (_ : i ∈ s), f i)
Tactic:
rw [bddAbove_def] at *
State after:
case a
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : ∃ x, ∀ y ∈ f '' s, y ≤ x
ha : ∃ i ∈ s, f i = a
⊢ ∃ x, ∀ y ∈ Set.range fun i => ⨆ (_ : i ∈ s), f i, y ≤ x

State before:
case a
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : ∃ x, ∀ y ∈ f '' s, y ≤ x
ha : ∃ i ∈ s, f i = a
⊢ ∃ x, ∀ y ∈ Set.range fun i => ⨆ (_ : i ∈ s), f i, y ≤ x
Tactic:
rcases hfs with ⟨x, hx⟩
State after:
case a.intro
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
⊢ ∃ x, ∀ y ∈ Set.range fun i => ⨆ (_ : i ∈ s), f i, y ≤ x

State before:
case a.intro
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
⊢ ∃ x, ∀ y ∈ Set.range fun i => ⨆ (_ : i ∈ s), f i, y ≤ x
Tactic:
use (max x (sSup ∅))
State after:
case h
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
⊢ ∀ y ∈ Set.range fun i => ⨆ (_ : i ∈ s), f i, y ≤ max x (sSup ∅)

State before:
case h
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
⊢ ∀ y ∈ Set.range fun i => ⨆ (_ : i ∈ s), f i, y ≤ max x (sSup ∅)
Tactic:
intro y hy
State after:
case h
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
hy : y ∈ Set.range fun i => ⨆ (_ : i ∈ s), f i
⊢ y ≤ max x (sSup ∅)

State before:
case h
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
hy : y ∈ Set.range fun i => ⨆ (_ : i ∈ s), f i
⊢ y ≤ max x (sSup ∅)
Tactic:
simp at hy
State after:
case h
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
hy : ∃ y_1, ⨆ (_ : y_1 ∈ s), f y_1 = y
⊢ y ≤ max x (sSup ∅)

State before:
case h
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
hy : ∃ y_1, ⨆ (_ : y_1 ∈ s), f y_1 = y
⊢ y ≤ max x (sSup ∅)
Tactic:
rcases hy with ⟨z, hz⟩
State after:
case h.intro
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : ⨆ (_ : z ∈ s), f z = y
⊢ y ≤ max x (sSup ∅)

State before:
case h.intro
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : ⨆ (_ : z ∈ s), f z = y
⊢ y ≤ max x (sSup ∅)
Tactic:
rw [iSup] at hz
State after:
case h.intro
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
⊢ y ≤ max x (sSup ∅)

State before:
case h.intro
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
⊢ y ≤ max x (sSup ∅)
Tactic:
by_cases h : z ∈ s
State after:
case pos
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
⊢ y ≤ max x (sSup ∅)

case neg
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∉ s
⊢ y ≤ max x (sSup ∅)

State before:
case pos
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
⊢ y ≤ max x (sSup ∅)

case neg
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∉ s
⊢ y ≤ max x (sSup ∅)
Tactic:
. have : (@Set.range α (z ∈ s) fun _ ↦ f z) = {f z} := by
    rw [Set.eq_singleton_iff_unique_mem]
    constructor
    . simpa
    . intro x hx
      simp at hx
      exact hx.2.symm
  rw [this] at hz
  have : sSup {f z} = f z := by apply csSup_singleton
  rw [this] at hz
  simp at hx
  have : f z ≤ x := hx z h
  rw [hz] at this
  apply le_max_of_le_left this
State after:
case neg
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∉ s
⊢ y ≤ max x (sSup ∅)

State before:
case neg
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∉ s
⊢ y ≤ max x (sSup ∅)
Tactic:
have : (@Set.range α (z ∈ s) fun _ ↦ f z) = ∅ := by
  simpa
State after:
case neg
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∉ s
this : (Set.range fun x => f z) = ∅
⊢ y ≤ max x (sSup ∅)

State before:
case neg
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∉ s
this : (Set.range fun x => f z) = ∅
⊢ y ≤ max x (sSup ∅)
Tactic:
rw [this] at hz
State after:
case neg
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup ∅ = y
h : z ∉ s
this : (Set.range fun x => f z) = ∅
⊢ y ≤ max x (sSup ∅)

State before:
case neg
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup ∅ = y
h : z ∉ s
this : (Set.range fun x => f z) = ∅
⊢ y ≤ max x (sSup ∅)
Tactic:
rw [hz]
State after:
case neg
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup ∅ = y
h : z ∉ s
this : (Set.range fun x => f z) = ∅
⊢ y ≤ max x y

State before:
case neg
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup ∅ = y
h : z ∉ s
this : (Set.range fun x => f z) = ∅
⊢ y ≤ max x y
Tactic:
exact le_max_right x y
State after:
no goals

State before:
case pos
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
⊢ y ≤ max x (sSup ∅)
Tactic:
have : (@Set.range α (z ∈ s) fun _ ↦ f z) = {f z} := by
  rw [Set.eq_singleton_iff_unique_mem]
  constructor
  . simpa
  . intro x hx
    simp at hx
    exact hx.2.symm
State after:
case pos
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
this : (Set.range fun x => f z) = {f z}
⊢ y ≤ max x (sSup ∅)

State before:
case pos
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
this : (Set.range fun x => f z) = {f z}
⊢ y ≤ max x (sSup ∅)
Tactic:
rw [this] at hz
State after:
case pos
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup {f z} = y
h : z ∈ s
this : (Set.range fun x => f z) = {f z}
⊢ y ≤ max x (sSup ∅)

State before:
case pos
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup {f z} = y
h : z ∈ s
this : (Set.range fun x => f z) = {f z}
⊢ y ≤ max x (sSup ∅)
Tactic:
have : sSup {f z} = f z := by apply csSup_singleton
State after:
case pos
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup {f z} = y
h : z ∈ s
this✝ : (Set.range fun x => f z) = {f z}
this : sSup {f z} = f z
⊢ y ≤ max x (sSup ∅)

State before:
case pos
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup {f z} = y
h : z ∈ s
this✝ : (Set.range fun x => f z) = {f z}
this : sSup {f z} = f z
⊢ y ≤ max x (sSup ∅)
Tactic:
rw [this] at hz
State after:
case pos
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : f z = y
h : z ∈ s
this✝ : (Set.range fun x => f z) = {f z}
this : sSup {f z} = f z
⊢ y ≤ max x (sSup ∅)

State before:
case pos
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : f z = y
h : z ∈ s
this✝ : (Set.range fun x => f z) = {f z}
this : sSup {f z} = f z
⊢ y ≤ max x (sSup ∅)
Tactic:
simp at hx
State after:
case pos
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x y : α
z : ι
hz : f z = y
h : z ∈ s
this✝ : (Set.range fun x => f z) = {f z}
this : sSup {f z} = f z
hx : ∀ a ∈ s, f a ≤ x
⊢ y ≤ max x (sSup ∅)

State before:
case pos
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x y : α
z : ι
hz : f z = y
h : z ∈ s
this✝ : (Set.range fun x => f z) = {f z}
this : sSup {f z} = f z
hx : ∀ a ∈ s, f a ≤ x
⊢ y ≤ max x (sSup ∅)
Tactic:
have : f z ≤ x := hx z h
State after:
case pos
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x y : α
z : ι
hz : f z = y
h : z ∈ s
this✝¹ : (Set.range fun x => f z) = {f z}
this✝ : sSup {f z} = f z
hx : ∀ a ∈ s, f a ≤ x
this : f z ≤ x
⊢ y ≤ max x (sSup ∅)

State before:
case pos
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x y : α
z : ι
hz : f z = y
h : z ∈ s
this✝¹ : (Set.range fun x => f z) = {f z}
this✝ : sSup {f z} = f z
hx : ∀ a ∈ s, f a ≤ x
this : f z ≤ x
⊢ y ≤ max x (sSup ∅)
Tactic:
rw [hz] at this
State after:
case pos
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x y : α
z : ι
hz : f z = y
h : z ∈ s
this✝¹ : (Set.range fun x => f z) = {f z}
this✝ : sSup {f z} = f z
hx : ∀ a ∈ s, f a ≤ x
this : y ≤ x
⊢ y ≤ max x (sSup ∅)

State before:
case pos
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x y : α
z : ι
hz : f z = y
h : z ∈ s
this✝¹ : (Set.range fun x => f z) = {f z}
this✝ : sSup {f z} = f z
hx : ∀ a ∈ s, f a ≤ x
this : y ≤ x
⊢ y ≤ max x (sSup ∅)
Tactic:
apply le_max_of_le_left this
State after:
no goals

State before:
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
⊢ (Set.range fun x => f z) = {f z}
Tactic:
rw [Set.eq_singleton_iff_unique_mem]
State after:
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
⊢ (f z ∈ Set.range fun x => f z) ∧ ∀ x ∈ Set.range fun x => f z, x = f z

State before:
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
⊢ (f z ∈ Set.range fun x => f z) ∧ ∀ x ∈ Set.range fun x => f z, x = f z
Tactic:
constructor
State after:
case left
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
⊢ f z ∈ Set.range fun x => f z

case right
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
⊢ ∀ x ∈ Set.range fun x => f z, x = f z

State before:
case left
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
⊢ f z ∈ Set.range fun x => f z

case right
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
⊢ ∀ x ∈ Set.range fun x => f z, x = f z
Tactic:
. simpa
State after:
case right
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
⊢ ∀ x ∈ Set.range fun x => f z, x = f z

State before:
case right
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
⊢ ∀ x ∈ Set.range fun x => f z, x = f z
Tactic:
. intro x hx
  simp at hx
  exact hx.2.symm
State after:
no goals

State before:
case left
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
⊢ f z ∈ Set.range fun x => f z
Tactic:
simpa
State after:
no goals

State before:
case right
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
⊢ ∀ x ∈ Set.range fun x => f z, x = f z
Tactic:
intro x hx
State after:
case right
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x✝ : α
hx✝ : ∀ y ∈ f '' s, y ≤ x✝
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
x : α
hx : x ∈ Set.range fun x => f z
⊢ x = f z

State before:
case right
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x✝ : α
hx✝ : ∀ y ∈ f '' s, y ≤ x✝
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
x : α
hx : x ∈ Set.range fun x => f z
⊢ x = f z
Tactic:
simp at hx
State after:
case right
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x✝ : α
hx✝ : ∀ y ∈ f '' s, y ≤ x✝
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
x : α
hx : z ∈ s ∧ f z = x
⊢ x = f z

State before:
case right
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x✝ : α
hx✝ : ∀ y ∈ f '' s, y ≤ x✝
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∈ s
x : α
hx : z ∈ s ∧ f z = x
⊢ x = f z
Tactic:
exact hx.2.symm
State after:
no goals

State before:
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup {f z} = y
h : z ∈ s
this : (Set.range fun x => f z) = {f z}
⊢ sSup {f z} = f z
Tactic:
apply csSup_singleton
State after:
no goals

State before:
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
ha : ∃ i ∈ s, f i = a
x : α
hx : ∀ y ∈ f '' s, y ≤ x
y : α
z : ι
hz : sSup (Set.range fun h => f z) = y
h : z ∉ s
⊢ (Set.range fun x => f z) = ∅
Tactic:
simpa
State after:
no goals

State before:
case h.e'_2.h.e'_3.left
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ a ∈ Set.range fun h => f i
Tactic:
simp
State after:
case h.e'_2.h.e'_3.left
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ i ∈ s ∧ f i = a

State before:
case h.e'_2.h.e'_3.left
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ i ∈ s ∧ f i = a
Tactic:
use hi, fia
State after:
no goals

State before:
case h.e'_2.h.e'_3.right
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
⊢ ∀ x ∈ Set.range fun h => f i, x = a
Tactic:
intro x hx
State after:
case h.e'_2.h.e'_3.right
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
x : α
hx : x ∈ Set.range fun h => f i
⊢ x = a

State before:
case h.e'_2.h.e'_3.right
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
x : α
hx : x ∈ Set.range fun h => f i
⊢ x = a
Tactic:
simp at hx
State after:
case h.e'_2.h.e'_3.right
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
x : α
hx : i ∈ s ∧ f i = x
⊢ x = a

State before:
case h.e'_2.h.e'_3.right
α : Type
inst✝¹ : ConditionallyCompleteLinearOrder α
ι : Type
inst✝ : Nonempty ι
f : ι → α
s : Set ι
a : α
hfs : BddAbove (f '' s)
i : ι
hi : i ∈ s
fia : f i = a
x : α
hx : i ∈ s ∧ f i = x
⊢ x = a
Tactic:
rwa [hx.2] at fia
State after:
no goals