α : Type ?u.58427
β : Type ?u.58430
inst✝¹ : Denumerable α
inst✝ : Denumerable β
m : ℕ
l : List ℕ
n : ℕ
h₁ : ∀ (m_1 : ℕ), m_1 ∈ m :: l → n ≤ m_1
h₂ : Sorted (fun x x_1 => x < x_1) (m :: l)
this : n ≤ m
⊢ raise' (lower' (m :: l) n) n = m :: l
α : Type ?u.58427
β : Type ?u.58430
inst✝¹ : Denumerable α
inst✝ : Denumerable β
m : ℕ
l : List ℕ
n : ℕ
h₁ : ∀ (m_1 : ℕ), m_1 ∈ m :: l → n ≤ m_1
h₂ : Sorted (fun x x_1 => x < x_1) (m :: l)
⊢ raise' (lower' (m :: l) n) n = m :: l
have : n ≤ m := h₁ _ (l.mem_cons_self _)
no goals
α : Type ?u.58427
β : Type ?u.58430
inst✝¹ : Denumerable α
inst✝ : Denumerable β
m : ℕ
l : List ℕ
n : ℕ
h₁ : ∀ (m_1 : ℕ), m_1 ∈ m :: l → n ≤ m_1
h₂ : Sorted (fun x x_1 => x < x_1) (m :: l)
this : n ≤ m
⊢ raise' (lower' (m :: l) n) n = m :: l
simp [raise', lower', tsub_add_cancel_of_le this,
  raise_lower' (List.rel_of_sorted_cons h₂ : ∀ a ∈ l, m < a) h₂.of_cons]