Theorem: existsOfSlowMono (FromTheBook/Ch02/Bertrand/LandauTrick.lean)

State before:
a b : ℕ
l : List ℕ
hl_mono : List.Chain (fun u v => u < v) a l
hl_slow : List.Chain (fun u v => v ≤ 2 * u) a l
hl_cons : l ≠ []
hb : b < List.getLast l hl_cons
⊢ ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ l ∧ lᵢ ∈ Set.Ioc n (2 * n)
Tactic:
cases l with
| nil => contradiction
| cons x l =>
  induction l generalizing a x with
  | nil =>
    intro n hn
    simp at *
    apply And.intro <;> linarith
  | cons y l h =>
    rw [List.chain_cons] at hl_mono
    rw [List.chain_cons] at hl_slow
    simp at hb
    specialize @h x y hl_mono.right hl_slow.right (List.cons_ne_nil y l) hb
    intro n hn
    specialize h n
    have : ∀ lᵢ, lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l := by simp
    simp_rw [this]
    simp only [or_and_right]
    rw [exists_or]
    cases le_or_lt x n with
    | inl hx =>
      apply Or.inr
      simp only [Set.mem_Ico] at *
      specialize h (And.intro hx hn.right)
      exact h
    | inr hx =>
      apply Or.inl
      simp at *
      apply And.intro <;> linarith
State after:
no goals

State before:
case nil
a b : ℕ
hl_mono : List.Chain (fun u v => u < v) a []
hl_slow : List.Chain (fun u v => v ≤ 2 * u) a []
hl_cons : [] ≠ []
hb : b < List.getLast [] hl_cons
⊢ ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ [] ∧ lᵢ ∈ Set.Ioc n (2 * n)
Tactic:
contradiction
State after:
no goals

State before:
case cons
a b x : ℕ
l : List ℕ
hl_mono : List.Chain (fun u v => u < v) a (x :: l)
hl_slow : List.Chain (fun u v => v ≤ 2 * u) a (x :: l)
hl_cons : x :: l ≠ []
hb : b < List.getLast (x :: l) hl_cons
⊢ ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
Tactic:
induction l generalizing a x with
| nil =>
  intro n hn
  simp at *
  apply And.intro <;> linarith
| cons y l h =>
  rw [List.chain_cons] at hl_mono
  rw [List.chain_cons] at hl_slow
  simp at hb
  specialize @h x y hl_mono.right hl_slow.right (List.cons_ne_nil y l) hb
  intro n hn
  specialize h n
  have : ∀ lᵢ, lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l := by simp
  simp_rw [this]
  simp only [or_and_right]
  rw [exists_or]
  cases le_or_lt x n with
  | inl hx =>
    apply Or.inr
    simp only [Set.mem_Ico] at *
    specialize h (And.intro hx hn.right)
    exact h
  | inr hx =>
    apply Or.inl
    simp at *
    apply And.intro <;> linarith
State after:
no goals

State before:
case cons.nil
b a x : ℕ
hl_mono : List.Chain (fun u v => u < v) a [x]
hl_slow : List.Chain (fun u v => v ≤ 2 * u) a [x]
hl_cons : [x] ≠ []
hb : b < List.getLast [x] hl_cons
⊢ ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ [x] ∧ lᵢ ∈ Set.Ioc n (2 * n)
Tactic:
intro n hn
State after:
case cons.nil
b a x : ℕ
hl_mono : List.Chain (fun u v => u < v) a [x]
hl_slow : List.Chain (fun u v => v ≤ 2 * u) a [x]
hl_cons : [x] ≠ []
hb : b < List.getLast [x] hl_cons
n : ℕ
hn : n ∈ Set.Icc a b
⊢ ∃ lᵢ, lᵢ ∈ [x] ∧ lᵢ ∈ Set.Ioc n (2 * n)

State before:
case cons.nil
b a x : ℕ
hl_mono : List.Chain (fun u v => u < v) a [x]
hl_slow : List.Chain (fun u v => v ≤ 2 * u) a [x]
hl_cons : [x] ≠ []
hb : b < List.getLast [x] hl_cons
n : ℕ
hn : n ∈ Set.Icc a b
⊢ ∃ lᵢ, lᵢ ∈ [x] ∧ lᵢ ∈ Set.Ioc n (2 * n)
Tactic:
simp at *
State after:
case cons.nil
b a x : ℕ
hl_cons : [x] ≠ []
hb : b < x
n : ℕ
hl_mono : a < x
hl_slow : x ≤ 2 * a
hn : a ≤ n ∧ n ≤ b
⊢ n < x ∧ x ≤ 2 * n

State before:
case cons.nil
b a x : ℕ
hl_cons : [x] ≠ []
hb : b < x
n : ℕ
hl_mono : a < x
hl_slow : x ≤ 2 * a
hn : a ≤ n ∧ n ≤ b
⊢ n < x ∧ x ≤ 2 * n
Tactic:
apply And.intro <;> linarith
State after:
no goals

State before:
case cons.cons
b y : ℕ
l : List ℕ
h :
  ∀ {a : ℕ} (x : ℕ),
    List.Chain (fun u v => u < v) a (x :: l) →
      List.Chain (fun u v => v ≤ 2 * u) a (x :: l) →
        ∀ (hl_cons : x :: l ≠ []),
          b < List.getLast (x :: l) hl_cons → ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
a x : ℕ
hl_mono : List.Chain (fun u v => u < v) a (x :: y :: l)
hl_slow : List.Chain (fun u v => v ≤ 2 * u) a (x :: y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (x :: y :: l) hl_cons
⊢ ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
Tactic:
rw [List.chain_cons] at hl_mono
State after:
case cons.cons
b y : ℕ
l : List ℕ
h :
  ∀ {a : ℕ} (x : ℕ),
    List.Chain (fun u v => u < v) a (x :: l) →
      List.Chain (fun u v => v ≤ 2 * u) a (x :: l) →
        ∀ (hl_cons : x :: l ≠ []),
          b < List.getLast (x :: l) hl_cons → ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : List.Chain (fun u v => v ≤ 2 * u) a (x :: y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (x :: y :: l) hl_cons
⊢ ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)

State before:
case cons.cons
b y : ℕ
l : List ℕ
h :
  ∀ {a : ℕ} (x : ℕ),
    List.Chain (fun u v => u < v) a (x :: l) →
      List.Chain (fun u v => v ≤ 2 * u) a (x :: l) →
        ∀ (hl_cons : x :: l ≠ []),
          b < List.getLast (x :: l) hl_cons → ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : List.Chain (fun u v => v ≤ 2 * u) a (x :: y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (x :: y :: l) hl_cons
⊢ ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
Tactic:
rw [List.chain_cons] at hl_slow
State after:
case cons.cons
b y : ℕ
l : List ℕ
h :
  ∀ {a : ℕ} (x : ℕ),
    List.Chain (fun u v => u < v) a (x :: l) →
      List.Chain (fun u v => v ≤ 2 * u) a (x :: l) →
        ∀ (hl_cons : x :: l ≠ []),
          b < List.getLast (x :: l) hl_cons → ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (x :: y :: l) hl_cons
⊢ ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)

State before:
case cons.cons
b y : ℕ
l : List ℕ
h :
  ∀ {a : ℕ} (x : ℕ),
    List.Chain (fun u v => u < v) a (x :: l) →
      List.Chain (fun u v => v ≤ 2 * u) a (x :: l) →
        ∀ (hl_cons : x :: l ≠ []),
          b < List.getLast (x :: l) hl_cons → ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (x :: y :: l) hl_cons
⊢ ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
Tactic:
simp at hb
State after:
case cons.cons
b y : ℕ
l : List ℕ
h :
  ∀ {a : ℕ} (x : ℕ),
    List.Chain (fun u v => u < v) a (x :: l) →
      List.Chain (fun u v => v ≤ 2 * u) a (x :: l) →
        ∀ (hl_cons : x :: l ≠ []),
          b < List.getLast (x :: l) hl_cons → ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
⊢ ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)

State before:
case cons.cons
b y : ℕ
l : List ℕ
h :
  ∀ {a : ℕ} (x : ℕ),
    List.Chain (fun u v => u < v) a (x :: l) →
      List.Chain (fun u v => v ≤ 2 * u) a (x :: l) →
        ∀ (hl_cons : x :: l ≠ []),
          b < List.getLast (x :: l) hl_cons → ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
⊢ ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
Tactic:
specialize @h x y hl_mono.right hl_slow.right (List.cons_ne_nil y l) hb
State after:
case cons.cons
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
h : ∀ (n : ℕ), n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
⊢ ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)

State before:
case cons.cons
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
h : ∀ (n : ℕ), n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
⊢ ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
Tactic:
intro n hn
State after:
case cons.cons
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
h : ∀ (n : ℕ), n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
n : ℕ
hn : n ∈ Set.Icc a b
⊢ ∃ lᵢ, lᵢ ∈ x :: y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)

State before:
case cons.cons
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
h : ∀ (n : ℕ), n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
n : ℕ
hn : n ∈ Set.Icc a b
⊢ ∃ lᵢ, lᵢ ∈ x :: y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
Tactic:
specialize h n
State after:
case cons.cons
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
h : n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
⊢ ∃ lᵢ, lᵢ ∈ x :: y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)

State before:
case cons.cons
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
h : n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
⊢ ∃ lᵢ, lᵢ ∈ x :: y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
Tactic:
have : ∀ lᵢ, lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l := by simp
State after:
case cons.cons
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
h : n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
this : ∀ (lᵢ : ℕ), lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l
⊢ ∃ lᵢ, lᵢ ∈ x :: y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)

State before:
case cons.cons
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
h : n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
this : ∀ (lᵢ : ℕ), lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l
⊢ ∃ lᵢ, lᵢ ∈ x :: y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
Tactic:
simp_rw [this]
State after:
case cons.cons
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
h : n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
this : ∀ (lᵢ : ℕ), lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l
⊢ ∃ lᵢ, (lᵢ = x ∨ lᵢ ∈ y :: l) ∧ lᵢ ∈ Set.Ioc n (2 * n)

State before:
case cons.cons
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
h : n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
this : ∀ (lᵢ : ℕ), lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l
⊢ ∃ lᵢ, (lᵢ = x ∨ lᵢ ∈ y :: l) ∧ lᵢ ∈ Set.Ioc n (2 * n)
Tactic:
simp only [or_and_right]
State after:
case cons.cons
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
h : n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
this : ∀ (lᵢ : ℕ), lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l
⊢ ∃ lᵢ, lᵢ = x ∧ lᵢ ∈ Set.Ioc n (2 * n) ∨ lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)

State before:
case cons.cons
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
h : n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
this : ∀ (lᵢ : ℕ), lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l
⊢ ∃ lᵢ, lᵢ = x ∧ lᵢ ∈ Set.Ioc n (2 * n) ∨ lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
Tactic:
rw [exists_or]
State after:
case cons.cons
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
h : n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
this : ∀ (lᵢ : ℕ), lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l
⊢ (∃ x_1, x_1 = x ∧ x_1 ∈ Set.Ioc n (2 * n)) ∨ ∃ x, x ∈ y :: l ∧ x ∈ Set.Ioc n (2 * n)

State before:
case cons.cons
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
h : n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
this : ∀ (lᵢ : ℕ), lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l
⊢ (∃ x_1, x_1 = x ∧ x_1 ∈ Set.Ioc n (2 * n)) ∨ ∃ x, x ∈ y :: l ∧ x ∈ Set.Ioc n (2 * n)
Tactic:
cases le_or_lt x n with
| inl hx =>
  apply Or.inr
  simp only [Set.mem_Ico] at *
  specialize h (And.intro hx hn.right)
  exact h
| inr hx =>
  apply Or.inl
  simp at *
  apply And.intro <;> linarith
State after:
no goals

State before:
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
h : n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
⊢ ∀ (lᵢ : ℕ), lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l
Tactic:
simp
State after:
no goals

State before:
case cons.cons.inl
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
h : n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
this : ∀ (lᵢ : ℕ), lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l
hx : x ≤ n
⊢ (∃ x_1, x_1 = x ∧ x_1 ∈ Set.Ioc n (2 * n)) ∨ ∃ x, x ∈ y :: l ∧ x ∈ Set.Ioc n (2 * n)
Tactic:
apply Or.inr
State after:
case cons.cons.inl.h
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
h : n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
this : ∀ (lᵢ : ℕ), lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l
hx : x ≤ n
⊢ ∃ x, x ∈ y :: l ∧ x ∈ Set.Ioc n (2 * n)

State before:
case cons.cons.inl.h
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
h : n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
this : ∀ (lᵢ : ℕ), lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l
hx : x ≤ n
⊢ ∃ x, x ∈ y :: l ∧ x ∈ Set.Ioc n (2 * n)
Tactic:
specialize h (And.intro hx hn.right)
State after:
case cons.cons.inl.h
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
this : ∀ (lᵢ : ℕ), lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l
hx : x ≤ n
h : ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
⊢ ∃ x, x ∈ y :: l ∧ x ∈ Set.Ioc n (2 * n)

State before:
case cons.cons.inl.h
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
this : ∀ (lᵢ : ℕ), lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l
hx : x ≤ n
h : ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
⊢ ∃ x, x ∈ y :: l ∧ x ∈ Set.Ioc n (2 * n)
Tactic:
exact h
State after:
no goals

State before:
case cons.cons.inr
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
h : n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
this : ∀ (lᵢ : ℕ), lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l
hx : n < x
⊢ (∃ x_1, x_1 = x ∧ x_1 ∈ Set.Ioc n (2 * n)) ∨ ∃ x, x ∈ y :: l ∧ x ∈ Set.Ioc n (2 * n)
Tactic:
apply Or.inl
State after:
case cons.cons.inr.h
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
h : n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
this : ∀ (lᵢ : ℕ), lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l
hx : n < x
⊢ ∃ x_1, x_1 = x ∧ x_1 ∈ Set.Ioc n (2 * n)

State before:
case cons.cons.inr.h
b y : ℕ
l : List ℕ
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
h : n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
this : ∀ (lᵢ : ℕ), lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l
hx : n < x
⊢ ∃ x_1, x_1 = x ∧ x_1 ∈ Set.Ioc n (2 * n)
Tactic:
simp at *
State after:
case cons.cons.inr.h
b y : ℕ
l : List ℕ
a x : ℕ
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hx : n < x
hl_mono : a < x ∧ x < y ∧ List.Chain (fun u v => u < v) y l
hl_slow : x ≤ 2 * a ∧ y ≤ 2 * x ∧ List.Chain (fun u v => v ≤ 2 * u) y l
hl_cons : True
hn : a ≤ n ∧ n ≤ b
h : x ≤ n → n ≤ b → n < y ∧ y ≤ 2 * n ∨ ∃ a, a ∈ l ∧ n < a ∧ a ≤ 2 * n
this : True
⊢ n < x ∧ x ≤ 2 * n

State before:
case cons.cons.inr.h
b y : ℕ
l : List ℕ
a x : ℕ
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hx : n < x
hl_mono : a < x ∧ x < y ∧ List.Chain (fun u v => u < v) y l
hl_slow : x ≤ 2 * a ∧ y ≤ 2 * x ∧ List.Chain (fun u v => v ≤ 2 * u) y l
hl_cons : True
hn : a ≤ n ∧ n ≤ b
h : x ≤ n → n ≤ b → n < y ∧ y ≤ 2 * n ∨ ∃ a, a ∈ l ∧ n < a ∧ a ≤ 2 * n
this : True
⊢ n < x ∧ x ≤ 2 * n
Tactic:
apply And.intro <;> linarith
State after:
no goals