Theorem: List.lt_upper (Logic/Vorspiel/Vorspiel.lean)

State before:
l : List ℕ
n : ℕ
h : n ∈ l
⊢ n < l.upper
Tactic:
induction' l with n ns ih <;> simp at h ⊢
State after:
case cons
n✝ n : ℕ
ns : List ℕ
ih : n✝ ∈ ns → n✝ < ns.upper
h : n✝ = n ∨ n✝ ∈ ns
⊢ n✝ < n + 1 ∨ n✝ < ns.upper

State before:
n✝ n : ℕ
ns : List ℕ
ih : n✝ ∈ ns → n✝ < ns.upper
h : n✝ = n ∨ n✝ ∈ ns
⊢ n✝ < n + 1 ∨ n✝ < ns.upper
Tactic:
case cons =>
  rcases h with (rfl | h); { exact Or.inl (Nat.lt_succ_self _) }
  exact Or.inr (ih h)
State after:
no goals

State before:
n✝ n : ℕ
ns : List ℕ
ih : n✝ ∈ ns → n✝ < ns.upper
h : n✝ = n ∨ n✝ ∈ ns
⊢ n✝ < n + 1 ∨ n✝ < ns.upper
Tactic:
rcases h with (rfl | h)
State after:
case inl
n : ℕ
ns : List ℕ
ih : n ∈ ns → n < ns.upper
⊢ n < n + 1 ∨ n < ns.upper

case inr
n✝ n : ℕ
ns : List ℕ
ih : n✝ ∈ ns → n✝ < ns.upper
h : n✝ ∈ ns
⊢ n✝ < n + 1 ∨ n✝ < ns.upper

State before:
case inl
n : ℕ
ns : List ℕ
ih : n ∈ ns → n < ns.upper
⊢ n < n + 1 ∨ n < ns.upper

case inr
n✝ n : ℕ
ns : List ℕ
ih : n✝ ∈ ns → n✝ < ns.upper
h : n✝ ∈ ns
⊢ n✝ < n + 1 ∨ n✝ < ns.upper
Tactic:
{ exact Or.inl (Nat.lt_succ_self _) }
State after:
case inr
n✝ n : ℕ
ns : List ℕ
ih : n✝ ∈ ns → n✝ < ns.upper
h : n✝ ∈ ns
⊢ n✝ < n + 1 ∨ n✝ < ns.upper

State before:
case inr
n✝ n : ℕ
ns : List ℕ
ih : n✝ ∈ ns → n✝ < ns.upper
h : n✝ ∈ ns
⊢ n✝ < n + 1 ∨ n✝ < ns.upper
Tactic:
exact Or.inr (ih h)
State after:
no goals

State before:
case inl
n : ℕ
ns : List ℕ
ih : n ∈ ns → n < ns.upper
⊢ n < n + 1 ∨ n < ns.upper
Tactic:
exact Or.inl (Nat.lt_succ_self _)
State after:
no goals