[GOAL]
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
m n : ℕ
h : m ≤ n
⊢ f m ≤ ↑(partialSups f) n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
m n : ℕ
h✝ : m ≤ n
h : m ≤ Nat.zero
⊢ f m ≤ ↑(partialSups f) Nat.zero
[PROOFSTEP]
rw [nonpos_iff_eq_zero.mp h, partialSups_zero]
[GOAL]
case succ
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
m n✝ : ℕ
h✝ : m ≤ n✝
n : ℕ
ih : m ≤ n → f m ≤ ↑(partialSups f) n
h : m ≤ Nat.succ n
⊢ f m ≤ ↑(partialSups f) (Nat.succ n)
[PROOFSTEP]
cases' h with h h
[GOAL]
case succ.refl
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
n✝ n : ℕ
h : Nat.succ n ≤ n✝
ih : Nat.succ n ≤ n → f (Nat.succ n) ≤ ↑(partialSups f) n
⊢ f (Nat.succ n) ≤ ↑(partialSups f) (Nat.succ n)
[PROOFSTEP]
exact le_sup_right
[GOAL]
case succ.step
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
m n✝ : ℕ
h✝ : m ≤ n✝
n : ℕ
ih : m ≤ n → f m ≤ ↑(partialSups f) n
h : Nat.le m n
⊢ f m ≤ ↑(partialSups f) (Nat.succ n)
[PROOFSTEP]
exact (ih h).trans le_sup_left
[GOAL]
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
n : ℕ
a : α
w : ∀ (m : ℕ), m ≤ n → f m ≤ a
⊢ ↑(partialSups f) n ≤ a
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
n : ℕ
a : α
w✝ : ∀ (m : ℕ), m ≤ n → f m ≤ a
w : ∀ (m : ℕ), m ≤ Nat.zero → f m ≤ a
⊢ ↑(partialSups f) Nat.zero ≤ a
[PROOFSTEP]
apply w 0 le_rfl
[GOAL]
case succ
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
n✝ : ℕ
a : α
w✝ : ∀ (m : ℕ), m ≤ n✝ → f m ≤ a
n : ℕ
ih : (∀ (m : ℕ), m ≤ n → f m ≤ a) → ↑(partialSups f) n ≤ a
w : ∀ (m : ℕ), m ≤ Nat.succ n → f m ≤ a
⊢ ↑(partialSups f) (Nat.succ n) ≤ a
[PROOFSTEP]
exact sup_le (ih fun m p => w m (Nat.le_succ_of_le p)) (w (n + 1) le_rfl)
[GOAL]
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
⊢ BddAbove (Set.range ↑(partialSups f)) ↔ BddAbove (Set.range f)
[PROOFSTEP]
apply exists_congr fun a => _
[GOAL]
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
⊢ ∀ (a : α), a ∈ upperBounds (Set.range ↑(partialSups f)) ↔ a ∈ upperBounds (Set.range f)
[PROOFSTEP]
intro a
[GOAL]
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
a : α
⊢ a ∈ upperBounds (Set.range ↑(partialSups f)) ↔ a ∈ upperBounds (Set.range f)
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
a : α
⊢ a ∈ upperBounds (Set.range ↑(partialSups f)) → a ∈ upperBounds (Set.range f)
[PROOFSTEP]
rintro h b ⟨i, rfl⟩
[GOAL]
case mp.intro
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
a : α
h : a ∈ upperBounds (Set.range ↑(partialSups f))
i : ℕ
⊢ f i ≤ a
[PROOFSTEP]
exact (le_partialSups _ _).trans (h (Set.mem_range_self i))
[GOAL]
case mpr
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
a : α
⊢ a ∈ upperBounds (Set.range f) → a ∈ upperBounds (Set.range ↑(partialSups f))
[PROOFSTEP]
rintro h b ⟨i, rfl⟩
[GOAL]
case mpr.intro
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
a : α
h : a ∈ upperBounds (Set.range f)
i : ℕ
⊢ ↑(partialSups f) i ≤ a
[PROOFSTEP]
exact partialSups_le _ _ _ fun _ _ => h (Set.mem_range_self _)
[GOAL]
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
hf : Monotone f
⊢ ↑(partialSups f) = f
[PROOFSTEP]
ext n
[GOAL]
case h
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
hf : Monotone f
n : ℕ
⊢ ↑(partialSups f) n = f n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case h.zero
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
hf : Monotone f
⊢ ↑(partialSups f) Nat.zero = f Nat.zero
[PROOFSTEP]
rfl
[GOAL]
case h.succ
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
hf : Monotone f
n : ℕ
ih : ↑(partialSups f) n = f n
⊢ ↑(partialSups f) (Nat.succ n) = f (Nat.succ n)
[PROOFSTEP]
rw [partialSups_succ, ih, sup_eq_right.2 (hf (Nat.le_succ _))]
[GOAL]
α : Type u_1
inst✝ : SemilatticeSup α
⊢ Monotone partialSups
[PROOFSTEP]
rintro f g h n
[GOAL]
α : Type u_1
inst✝ : SemilatticeSup α
f g : ℕ → α
h : f ≤ g
n : ℕ
⊢ OrderHom.toFun (partialSups f) n ≤ OrderHom.toFun (partialSups g) n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u_1
inst✝ : SemilatticeSup α
f g : ℕ → α
h : f ≤ g
⊢ OrderHom.toFun (partialSups f) Nat.zero ≤ OrderHom.toFun (partialSups g) Nat.zero
[PROOFSTEP]
exact h 0
[GOAL]
case succ
α : Type u_1
inst✝ : SemilatticeSup α
f g : ℕ → α
h : f ≤ g
n : ℕ
ih : OrderHom.toFun (partialSups f) n ≤ OrderHom.toFun (partialSups g) n
⊢ OrderHom.toFun (partialSups f) (Nat.succ n) ≤ OrderHom.toFun (partialSups g) (Nat.succ n)
[PROOFSTEP]
exact sup_le_sup ih (h _)
[GOAL]
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
h : ↑(partialSups f) ≤ f
⊢ Monotone f
[PROOFSTEP]
convert (partialSups f).monotone using 1
[GOAL]
case h.e'_5
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
h : ↑(partialSups f) ≤ f
⊢ f = ↑(partialSups f)
[PROOFSTEP]
exact (le_partialSups f).antisymm h
[GOAL]
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
g : ℕ →o α
⊢ partialSups f ≤ g ↔ f ≤ ↑g
[PROOFSTEP]
refine' ⟨(le_partialSups f).trans, fun h => _⟩
[GOAL]
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
g : ℕ →o α
h : f ≤ ↑g
⊢ partialSups f ≤ g
[PROOFSTEP]
convert partialSups_mono h
[GOAL]
case h.e'_4
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
g : ℕ →o α
h : f ≤ ↑g
⊢ g = partialSups ↑g
[PROOFSTEP]
exact OrderHom.ext _ _ g.monotone.partialSups_eq.symm
[GOAL]
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
n : ℕ
⊢ ↑(partialSups f) n = Finset.sup' (Finset.range (n + 1)) (_ : ∃ x, x ∈ Finset.range (n + 1)) f
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
⊢ ↑(partialSups f) Nat.zero = Finset.sup' (Finset.range (Nat.zero + 1)) (_ : ∃ x, x ∈ Finset.range (Nat.zero + 1)) f
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
n : ℕ
ih : ↑(partialSups f) n = Finset.sup' (Finset.range (n + 1)) (_ : ∃ x, x ∈ Finset.range (n + 1)) f
⊢ ↑(partialSups f) (Nat.succ n) =
    Finset.sup' (Finset.range (Nat.succ n + 1)) (_ : ∃ x, x ∈ Finset.range (Nat.succ n + 1)) f
[PROOFSTEP]
dsimp [partialSups] at ih ⊢
[GOAL]
case succ
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
n : ℕ
ih :
  Nat.rec (f 0) (fun n a => a ⊔ f (n + 1)) n = Finset.sup' (Finset.range (n + 1)) (_ : ∃ x, x ∈ Finset.range (n + 1)) f
⊢ Nat.rec (f 0) (fun n a => a ⊔ f (n + 1)) n ⊔ f (n + 1) =
    Finset.sup' (Finset.range (Nat.succ n + 1)) (_ : ∃ x, x ∈ Finset.range (Nat.succ n + 1)) f
[PROOFSTEP]
simp_rw [@Finset.range_succ n.succ]
[GOAL]
case succ
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
n : ℕ
ih :
  Nat.rec (f 0) (fun n a => a ⊔ f (n + 1)) n = Finset.sup' (Finset.range (n + 1)) (_ : ∃ x, x ∈ Finset.range (n + 1)) f
⊢ Nat.rec (f 0) (fun n a => a ⊔ f (n + 1)) n ⊔ f (n + 1) =
    Finset.sup' (insert (Nat.succ n) (Finset.range (Nat.succ n)))
      (_ : Finset.Nonempty (insert (Nat.succ n) (Finset.range (Nat.succ n)))) fun x => f x
[PROOFSTEP]
rw [ih, Finset.sup'_insert, sup_comm]
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : ℕ → α
n : ℕ
⊢ ↑(partialSups f) n = Finset.sup (Finset.range (n + 1)) f
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : ℕ → α
⊢ ↑(partialSups f) Nat.zero = Finset.sup (Finset.range (Nat.zero + 1)) f
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : ℕ → α
n : ℕ
ih : ↑(partialSups f) n = Finset.sup (Finset.range (n + 1)) f
⊢ ↑(partialSups f) (Nat.succ n) = Finset.sup (Finset.range (Nat.succ n + 1)) f
[PROOFSTEP]
dsimp [partialSups] at ih ⊢
[GOAL]
case succ
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : ℕ → α
n : ℕ
ih : Nat.rec (f 0) (fun n a => a ⊔ f (n + 1)) n = Finset.sup (Finset.range (n + 1)) f
⊢ Nat.rec (f 0) (fun n a => a ⊔ f (n + 1)) n ⊔ f (n + 1) = Finset.sup (Finset.range (Nat.succ n + 1)) f
[PROOFSTEP]
rw [Finset.range_succ, Finset.sup_insert, sup_comm, ih]
[GOAL]
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
f : ℕ → α
h : Pairwise (Disjoint on f)
m n : ℕ
hmn : m < n
⊢ Disjoint (↑(partialSups f) m) (f n)
[PROOFSTEP]
induction' m with m ih
[GOAL]
case zero
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
f : ℕ → α
h : Pairwise (Disjoint on f)
m n : ℕ
hmn✝ : m < n
hmn : Nat.zero < n
⊢ Disjoint (↑(partialSups f) Nat.zero) (f n)
[PROOFSTEP]
exact h hmn.ne
[GOAL]
case succ
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
f : ℕ → α
h : Pairwise (Disjoint on f)
m✝ n : ℕ
hmn✝ : m✝ < n
m : ℕ
ih : m < n → Disjoint (↑(partialSups f) m) (f n)
hmn : Nat.succ m < n
⊢ Disjoint (↑(partialSups f) (Nat.succ m)) (f n)
[PROOFSTEP]
rw [partialSups_succ, disjoint_sup_left]
[GOAL]
case succ
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
f : ℕ → α
h : Pairwise (Disjoint on f)
m✝ n : ℕ
hmn✝ : m✝ < n
m : ℕ
ih : m < n → Disjoint (↑(partialSups f) m) (f n)
hmn : Nat.succ m < n
⊢ Disjoint (↑(partialSups f) m) (f n) ∧ Disjoint (f (m + 1)) (f n)
[PROOFSTEP]
exact ⟨ih (Nat.lt_of_succ_lt hmn), h hmn.ne⟩
[GOAL]
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
f : ℕ → α
n : ℕ
⊢ ↑(partialSups f) n = ⨆ (i : ↑(Set.Iic n)), f ↑i
[PROOFSTEP]
have : Set.Iio (n + 1) = Set.Iic n := Set.ext fun _ => Nat.lt_succ_iff
[GOAL]
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
f : ℕ → α
n : ℕ
this : Set.Iio (n + 1) = Set.Iic n
⊢ ↑(partialSups f) n = ⨆ (i : ↑(Set.Iic n)), f ↑i
[PROOFSTEP]
rw [partialSups_eq_sup'_range, Finset.sup'_eq_csSup_image, Finset.coe_range, iSup, this]
[GOAL]
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
f : ℕ → α
n : ℕ
this : Set.Iio (n + 1) = Set.Iic n
⊢ sSup (f '' Set.Iic n) = sSup (Set.range fun i => f ↑i)
[PROOFSTEP]
simp only [Set.range, Subtype.exists, Set.mem_Iic, exists_prop, (· '' ·)]
[GOAL]
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
f : ℕ → α
h : BddAbove (Set.range f)
⊢ ⨆ (n : ℕ), ↑(partialSups f) n = ⨆ (n : ℕ), f n
[PROOFSTEP]
refine' (ciSup_le fun n => _).antisymm (ciSup_mono _ <| le_partialSups f)
[GOAL]
case refine'_1
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
f : ℕ → α
h : BddAbove (Set.range f)
n : ℕ
⊢ ↑(partialSups f) n ≤ ⨆ (n : ℕ), f n
[PROOFSTEP]
rw [partialSups_eq_ciSup_Iic]
[GOAL]
case refine'_1
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
f : ℕ → α
h : BddAbove (Set.range f)
n : ℕ
⊢ ⨆ (i : ↑(Set.Iic n)), f ↑i ≤ ⨆ (n : ℕ), f n
[PROOFSTEP]
exact ciSup_le fun i => le_ciSup h _
[GOAL]
case refine'_2
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
f : ℕ → α
h : BddAbove (Set.range f)
⊢ BddAbove (Set.range fun n => ↑(partialSups f) n)
[PROOFSTEP]
rwa [bddAbove_range_partialSups]
[GOAL]
α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → α
n : ℕ
⊢ ↑(partialSups f) n = ⨆ (i : ℕ) (_ : i ≤ n), f i
[PROOFSTEP]
simpa only [iSup_subtype] using partialSups_eq_ciSup_Iic f n
[GOAL]
α : Type u_1
inst✝ : CompleteLattice α
f g : ℕ → α
h : partialSups f ≤ partialSups g
⊢ ⨆ (n : ℕ), f n ≤ ⨆ (n : ℕ), g n
[PROOFSTEP]
rw [← iSup_partialSups_eq f, ← iSup_partialSups_eq g]
[GOAL]
α : Type u_1
inst✝ : CompleteLattice α
f g : ℕ → α
h : partialSups f ≤ partialSups g
⊢ ⨆ (n : ℕ), ↑(partialSups f) n ≤ ⨆ (n : ℕ), ↑(partialSups g) n
[PROOFSTEP]
exact iSup_mono h
[GOAL]
α : Type u_1
inst✝ : CompleteLattice α
f g : ℕ → α
h : partialSups f = partialSups g
⊢ ⨆ (n : ℕ), f n = ⨆ (n : ℕ), g n
[PROOFSTEP]
simp_rw [← iSup_partialSups_eq f, ← iSup_partialSups_eq g, h]
