[GOAL]
s : Set ℕ
⊢ sInf s = 0 ↔ 0 ∈ s ∨ s = ∅
[PROOFSTEP]
cases eq_empty_or_nonempty s with
| inl h =>
  subst h
  simp only [or_true_iff, eq_self_iff_true, iff_true_iff, iInf, InfSet.sInf, mem_empty_iff_false, exists_false, dif_neg,
    not_false_iff]
| inr h => simp only [h.ne_empty, or_false_iff, Nat.sInf_def, h, Nat.find_eq_zero]
[GOAL]
s : Set ℕ
x✝ : s = ∅ ∨ Set.Nonempty s
⊢ sInf s = 0 ↔ 0 ∈ s ∨ s = ∅
[PROOFSTEP]
cases eq_empty_or_nonempty s with
| inl h =>
  subst h
  simp only [or_true_iff, eq_self_iff_true, iff_true_iff, iInf, InfSet.sInf, mem_empty_iff_false, exists_false, dif_neg,
    not_false_iff]
| inr h => simp only [h.ne_empty, or_false_iff, Nat.sInf_def, h, Nat.find_eq_zero]
[GOAL]
case inl
s : Set ℕ
h : s = ∅
⊢ sInf s = 0 ↔ 0 ∈ s ∨ s = ∅
[PROOFSTEP]

| inl h =>
  subst h
  simp only [or_true_iff, eq_self_iff_true, iff_true_iff, iInf, InfSet.sInf, mem_empty_iff_false, exists_false, dif_neg,
    not_false_iff]
[GOAL]
case inl
s : Set ℕ
h : s = ∅
⊢ sInf s = 0 ↔ 0 ∈ s ∨ s = ∅
[PROOFSTEP]
subst h
[GOAL]
case inl
⊢ sInf ∅ = 0 ↔ 0 ∈ ∅ ∨ ∅ = ∅
[PROOFSTEP]
simp only [or_true_iff, eq_self_iff_true, iff_true_iff, iInf, InfSet.sInf, mem_empty_iff_false, exists_false, dif_neg,
  not_false_iff]
[GOAL]
case inr
s : Set ℕ
h : Set.Nonempty s
⊢ sInf s = 0 ↔ 0 ∈ s ∨ s = ∅
[PROOFSTEP]

| inr h => simp only [h.ne_empty, or_false_iff, Nat.sInf_def, h, Nat.find_eq_zero]
[GOAL]
case inr
s : Set ℕ
h : Set.Nonempty s
⊢ sInf s = 0 ↔ 0 ∈ s ∨ s = ∅
[PROOFSTEP]
simp only [h.ne_empty, or_false_iff, Nat.sInf_def, h, Nat.find_eq_zero]
[GOAL]
⊢ sInf ∅ = 0
[PROOFSTEP]
rw [sInf_eq_zero]
[GOAL]
⊢ 0 ∈ ∅ ∨ ∅ = ∅
[PROOFSTEP]
right
[GOAL]
case h
⊢ ∅ = ∅
[PROOFSTEP]
rfl
[GOAL]
ι : Sort u_1
inst✝ : IsEmpty ι
f : ι → ℕ
⊢ iInf f = 0
[PROOFSTEP]
rw [iInf_of_empty', sInf_empty]
[GOAL]
s : Set ℕ
h : Set.Nonempty s
⊢ sInf s ∈ s
[PROOFSTEP]
rw [Nat.sInf_def h]
[GOAL]
s : Set ℕ
h : Set.Nonempty s
⊢ Nat.find h ∈ s
[PROOFSTEP]
exact Nat.find_spec h
[GOAL]
s : Set ℕ
m : ℕ
hm : m < sInf s
⊢ ¬m ∈ s
[PROOFSTEP]
cases eq_empty_or_nonempty s with
| inl h => subst h; apply not_mem_empty
| inr h => rw [Nat.sInf_def h] at hm ; exact Nat.find_min h hm
[GOAL]
s : Set ℕ
m : ℕ
hm : m < sInf s
x✝ : s = ∅ ∨ Set.Nonempty s
⊢ ¬m ∈ s
[PROOFSTEP]
cases eq_empty_or_nonempty s with
| inl h => subst h; apply not_mem_empty
| inr h => rw [Nat.sInf_def h] at hm ; exact Nat.find_min h hm
[GOAL]
case inl
s : Set ℕ
m : ℕ
hm : m < sInf s
h : s = ∅
⊢ ¬m ∈ s
[PROOFSTEP]

| inl h => subst h; apply not_mem_empty
[GOAL]
case inl
s : Set ℕ
m : ℕ
hm : m < sInf s
h : s = ∅
⊢ ¬m ∈ s
[PROOFSTEP]
subst h
[GOAL]
case inl
m : ℕ
hm : m < sInf ∅
⊢ ¬m ∈ ∅
[PROOFSTEP]
apply not_mem_empty
[GOAL]
case inr
s : Set ℕ
m : ℕ
hm : m < sInf s
h : Set.Nonempty s
⊢ ¬m ∈ s
[PROOFSTEP]

| inr h => rw [Nat.sInf_def h] at hm ; exact Nat.find_min h hm
[GOAL]
case inr
s : Set ℕ
m : ℕ
hm : m < sInf s
h : Set.Nonempty s
⊢ ¬m ∈ s
[PROOFSTEP]
rw [Nat.sInf_def h] at hm 
[GOAL]
case inr
s : Set ℕ
m : ℕ
h : Set.Nonempty s
hm : m < Nat.find h
⊢ ¬m ∈ s
[PROOFSTEP]
exact Nat.find_min h hm
[GOAL]
s : Set ℕ
m : ℕ
hm : m ∈ s
⊢ sInf s ≤ m
[PROOFSTEP]
rw [Nat.sInf_def ⟨m, hm⟩]
[GOAL]
s : Set ℕ
m : ℕ
hm : m ∈ s
⊢ Nat.find (_ : ∃ x, x ∈ s) ≤ m
[PROOFSTEP]
exact Nat.find_min' ⟨m, hm⟩ hm
[GOAL]
s : Set ℕ
h : 0 < sInf s
⊢ Set.Nonempty s
[PROOFSTEP]
by_contra contra
[GOAL]
s : Set ℕ
h : 0 < sInf s
contra : ¬Set.Nonempty s
⊢ False
[PROOFSTEP]
rw [Set.not_nonempty_iff_eq_empty] at contra 
[GOAL]
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
⊢ False
[PROOFSTEP]
have h' : sInf s ≠ 0 := ne_of_gt h
[GOAL]
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
h' : sInf s ≠ 0
⊢ False
[PROOFSTEP]
apply h'
[GOAL]
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
h' : sInf s ≠ 0
⊢ sInf s = 0
[PROOFSTEP]
rw [Nat.sInf_eq_zero]
[GOAL]
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
h' : sInf s ≠ 0
⊢ 0 ∈ s ∨ s = ∅
[PROOFSTEP]
right
[GOAL]
case h
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
h' : sInf s ≠ 0
⊢ s = ∅
[PROOFSTEP]
assumption
[GOAL]
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
⊢ sInf s = k + 1 ↔ k + 1 ∈ s ∧ ¬k ∈ s
[PROOFSTEP]
constructor
[GOAL]
case mp
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
⊢ sInf s = k + 1 → k + 1 ∈ s ∧ ¬k ∈ s
[PROOFSTEP]
intro H
[GOAL]
case mp
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ k + 1 ∈ s ∧ ¬k ∈ s
[PROOFSTEP]
rw [eq_Ici_of_nonempty_of_upward_closed (nonempty_of_sInf_eq_succ _) hs, H, mem_Ici, mem_Ici]
[GOAL]
case mp
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ k + 1 ≤ k + 1 ∧ ¬k + 1 ≤ k
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ ℕ
s : Set ℕ hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s k : ℕ H : sInf s = k + 1 ⊢ sInf s = ?m.6254 + 1
[PROOFSTEP]
exact ⟨le_rfl, k.not_succ_le_self⟩
[GOAL]
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ ℕ
s : Set ℕ hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s k : ℕ H : sInf s = k + 1 ⊢ sInf s = ?m.6254 + 1
[PROOFSTEP]
exact k
[GOAL]
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ sInf s = k + 1
[PROOFSTEP]
assumption
[GOAL]
case mpr
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
⊢ k + 1 ∈ s ∧ ¬k ∈ s → sInf s = k + 1
[PROOFSTEP]
rintro ⟨H, H'⟩
[GOAL]
case mpr.intro
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : k + 1 ∈ s
H' : ¬k ∈ s
⊢ sInf s = k + 1
[PROOFSTEP]
rw [sInf_def (⟨_, H⟩ : s.Nonempty), find_eq_iff]
[GOAL]
case mpr.intro
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : k + 1 ∈ s
H' : ¬k ∈ s
⊢ k + 1 ∈ s ∧ ∀ (n : ℕ), n < k + 1 → ¬n ∈ s
[PROOFSTEP]
exact ⟨H, fun n hnk hns ↦ H' <| hs n k (lt_succ_iff.mp hnk) hns⟩
[GOAL]
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
s : Set ℕ
a : ℕ
hb : BddAbove s
ha : a ∈ s
⊢ a ≤ sSup s
[PROOFSTEP]
rw [sSup_def hb]
[GOAL]
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
s : Set ℕ
a : ℕ
hb : BddAbove s
ha : a ∈ s
⊢ a ≤ Nat.find hb
[PROOFSTEP]
revert a ha
[GOAL]
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
s : Set ℕ
hb : BddAbove s
⊢ ∀ (a : ℕ), a ∈ s → a ≤ Nat.find hb
[PROOFSTEP]
exact @Nat.find_spec _ _ hb
[GOAL]
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
s : Set ℕ
a : ℕ
x✝ : Set.Nonempty s
ha : a ∈ upperBounds s
⊢ sSup s ≤ a
[PROOFSTEP]
rw [sSup_def ⟨a, ha⟩]
[GOAL]
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
s : Set ℕ
a : ℕ
x✝ : Set.Nonempty s
ha : a ∈ upperBounds s
⊢ Nat.find (_ : ∃ n, ∀ (a : ℕ), a ∈ s → a ≤ n) ≤ a
[PROOFSTEP]
exact Nat.find_min' _ ha
[GOAL]
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
s : Set ℕ
a : ℕ
x✝ : BddBelow s
ha : a ∈ s
⊢ sInf s ≤ a
[PROOFSTEP]
rw [sInf_def ⟨a, ha⟩]
[GOAL]
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
s : Set ℕ
a : ℕ
x✝ : BddBelow s
ha : a ∈ s
⊢ Nat.find (_ : ∃ x, x ∈ s) ≤ a
[PROOFSTEP]
exact Nat.find_min' _ ha
[GOAL]
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
s : Set ℕ
a : ℕ
hs : Set.Nonempty s
hb : a ∈ lowerBounds s
⊢ a ≤ sInf s
[PROOFSTEP]
rw [sInf_def hs]
[GOAL]
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
s : Set ℕ
a : ℕ
hs : Set.Nonempty s
hb : a ∈ lowerBounds s
⊢ a ≤ Nat.find hs
[PROOFSTEP]
exact hb (@Nat.find_spec (fun n ↦ n ∈ s) _ _)
[GOAL]
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
⊢ ∀ (s : Set ℕ), ¬BddAbove s → sSup s = sSup univ
[PROOFSTEP]
intro s hs
[GOAL]
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
s : Set ℕ
hs : ¬BddAbove s
⊢ sSup s = sSup univ
[PROOFSTEP]
simp only [mem_univ, forall_true_left, sSup]
[GOAL]
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
s : Set ℕ
hs : ¬BddAbove s
⊢ (if h : ∃ n, ∀ (a : ℕ), a ∈ s → a ≤ n then Nat.find h else 0) =
    if h : ∃ n, ∀ (a : ℕ), a ≤ n then Nat.find (_ : ∃ n, (fun n => ∀ (a : ℕ), a ≤ n) n) else 0
[PROOFSTEP]
rw [dif_neg, dif_neg]
[GOAL]
case hnc
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
s : Set ℕ
hs : ¬BddAbove s
⊢ ¬∃ n, ∀ (a : ℕ), a ≤ n
[PROOFSTEP]
simp only [not_exists, not_forall, not_le]
[GOAL]
case hnc
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
s : Set ℕ
hs : ¬BddAbove s
⊢ ∀ (x : ℕ), ∃ x_1, x < x_1
[PROOFSTEP]
exact fun n ↦ ⟨n + 1, lt.base n⟩
[GOAL]
case hnc
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
s : Set ℕ
hs : ¬BddAbove s
⊢ ¬∃ n, ∀ (a : ℕ), a ∈ s → a ≤ n
[PROOFSTEP]
exact hs
[GOAL]
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
s : Set ℕ
hs : ¬BddBelow s
⊢ sInf s = sInf univ
[PROOFSTEP]
simp at hs 
[GOAL]
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
⊢ sSup ∅ = ⊥
[PROOFSTEP]
simp only [sSup_def, Set.mem_empty_iff_false, forall_const, forall_prop_of_false, not_false_iff, exists_const]
[GOAL]
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
⊢ Nat.find (_ : ∃ n, (fun n => True) n) = ⊥
[PROOFSTEP]
apply bot_unique (Nat.find_min' _ _)
[GOAL]
src✝² : OrderBot ℕ := inferInstance
src✝¹ : Lattice ℕ := LinearOrder.toLattice
src✝ : LinearOrder ℕ := inferInstance
⊢ True
[PROOFSTEP]
trivial
[GOAL]
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
⊢ sInf {m | p (m + n)} + n = sInf {m | p m}
[PROOFSTEP]
obtain h | ⟨m, hm⟩ := {m | p (m + n)}.eq_empty_or_nonempty
[GOAL]
case inl
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
⊢ sInf {m | p (m + n)} + n = sInf {m | p m}
[PROOFSTEP]
rw [h, Nat.sInf_empty, zero_add]
[GOAL]
case inl
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
⊢ n = sInf {m | p m}
[PROOFSTEP]
obtain hnp | hnp := hn.eq_or_lt
[GOAL]
case inl.inl
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
hnp : n = sInf {m | p m}
⊢ n = sInf {m | p m}
[PROOFSTEP]
exact hnp
[GOAL]
case inl.inr
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
hnp : n < sInf {m | p m}
⊢ n = sInf {m | p m}
[PROOFSTEP]
suffices hp : p (sInf {m | p m} - n + n)
[GOAL]
case inl.inr
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
hnp : n < sInf {m | p m}
hp : p (sInf {m | p m} - n + n)
⊢ n = sInf {m | p m}
[PROOFSTEP]
exact (h.subset hp).elim
[GOAL]
case hp
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
hnp : n < sInf {m | p m}
⊢ p (sInf {m | p m} - n + n)
[PROOFSTEP]
rw [tsub_add_cancel_of_le hn]
[GOAL]
case hp
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
hnp : n < sInf {m | p m}
⊢ p (sInf {m | p m})
[PROOFSTEP]
exact csInf_mem (nonempty_of_pos_sInf <| n.zero_le.trans_lt hnp)
[GOAL]
case inr.intro
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
m : ℕ
hm : m ∈ {m | p (m + n)}
⊢ sInf {m | p (m + n)} + n = sInf {m | p m}
[PROOFSTEP]
have hp : ∃ n, n ∈ {m | p m} := ⟨_, hm⟩
[GOAL]
case inr.intro
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
m : ℕ
hm : m ∈ {m | p (m + n)}
hp : ∃ n, n ∈ {m | p m}
⊢ sInf {m | p (m + n)} + n = sInf {m | p m}
[PROOFSTEP]
rw [Nat.sInf_def ⟨m, hm⟩, Nat.sInf_def hp]
[GOAL]
case inr.intro
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
m : ℕ
hm : m ∈ {m | p (m + n)}
hp : ∃ n, n ∈ {m | p m}
⊢ Nat.find (_ : ∃ x, x ∈ {m | p (m + n)}) + n = Nat.find hp
[PROOFSTEP]
rw [Nat.sInf_def hp] at hn 
[GOAL]
case inr.intro
n : ℕ
p : ℕ → Prop
m : ℕ
hm : m ∈ {m | p (m + n)}
hp : ∃ n, n ∈ {m | p m}
hn : n ≤ Nat.find hp
⊢ Nat.find (_ : ∃ x, x ∈ {m | p (m + n)}) + n = Nat.find hp
[PROOFSTEP]
exact find_add hn
[GOAL]
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
⊢ sInf {m | p m} + n = sInf {m | p (m - n)}
[PROOFSTEP]
suffices h₁ : n ≤ sInf {m | p (m - n)}
[GOAL]
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
h₁ : n ≤ sInf {m | p (m - n)}
⊢ sInf {m | p m} + n = sInf {m | p (m - n)}
case h₁ n : ℕ p : ℕ → Prop h : 0 < sInf {m | p m} ⊢ n ≤ sInf {m | p (m - n)}
[PROOFSTEP]
convert sInf_add h₁
[GOAL]
case h.e'_2.h.e'_5.h.e'_3.h.e'_2.h.h.e'_1
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
h₁ : n ≤ sInf {m | p (m - n)}
x✝ : ℕ
⊢ x✝ = x✝ + n - n
[PROOFSTEP]
simp_rw [add_tsub_cancel_right]
[GOAL]
case h₁
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
⊢ n ≤ sInf {m | p (m - n)}
[PROOFSTEP]
obtain ⟨m, hm⟩ := nonempty_of_pos_sInf h
[GOAL]
case h₁.intro
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
m : ℕ
hm : m ∈ {m | p m}
⊢ n ≤ sInf {m | p (m - n)}
[PROOFSTEP]
refine'
  le_csInf ⟨m + n, _⟩ fun b hb ↦
    le_of_not_lt fun hbn ↦ ne_of_mem_of_not_mem _ (not_mem_of_lt_sInf h) (tsub_eq_zero_of_le hbn.le)
[GOAL]
case h₁.intro.refine'_1
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
m : ℕ
hm : m ∈ {m | p m}
⊢ m + n ∈ {m | p (m - n)}
[PROOFSTEP]
dsimp
[GOAL]
case h₁.intro.refine'_1
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
m : ℕ
hm : m ∈ {m | p m}
⊢ p (m + n - n)
[PROOFSTEP]
rwa [add_tsub_cancel_right]
[GOAL]
case h₁.intro.refine'_2
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
m : ℕ
hm : m ∈ {m | p m}
b : ℕ
hb : b ∈ {m | p (m - n)}
hbn : b < n
⊢ b - n ∈ {m | p m}
[PROOFSTEP]
exact hb
[GOAL]
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ (k : ℕ) (_ : k < n + 1), u k = (⨆ (k : ℕ) (_ : k < n), u k) ⊔ u n
[PROOFSTEP]
simp [Nat.lt_succ_iff_lt_or_eq, iSup_or, iSup_sup_eq]
[GOAL]
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ (k : ℕ) (_ : k < n + 1), u k = u 0 ⊔ ⨆ (k : ℕ) (_ : k < n), u (k + 1)
[PROOFSTEP]
rw [← sup_iSup_nat_succ]
[GOAL]
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ (⨆ (_ : 0 < n + 1), u 0) ⊔ ⨆ (i : ℕ) (_ : i + 1 < n + 1), u (i + 1) = u 0 ⊔ ⨆ (k : ℕ) (_ : k < n), u (k + 1)
[PROOFSTEP]
simp
