Theorem: Encodable.encode_list_lt (Logic/Vorspiel/Computability.lean)

State before:
β : Type u_1
inst✝ : Encodable β
b : β
bs : List β
h : b ∈ bs
⊢ encode b < encode bs
Tactic:
induction' bs with b' bs ih
State after:
case nil
β : Type u_1
inst✝ : Encodable β
b : β
h : b ∈ []
⊢ encode b < encode []

case cons
β : Type u_1
inst✝ : Encodable β
b b' : β
bs : List β
ih : b ∈ bs → encode b < encode bs
h : b ∈ b' :: bs
⊢ encode b < encode (b' :: bs)

State before:
case nil
β : Type u_1
inst✝ : Encodable β
b : β
h : b ∈ []
⊢ encode b < encode []
Tactic:
simp at h
State after:
no goals

State before:
case cons
β : Type u_1
inst✝ : Encodable β
b b' : β
bs : List β
ih : b ∈ bs → encode b < encode bs
h : b ∈ b' :: bs
⊢ encode b < encode (b' :: bs)
Tactic:
have : b = b' ∨ b ∈ bs := by simpa using h
State after:
case cons
β : Type u_1
inst✝ : Encodable β
b b' : β
bs : List β
ih : b ∈ bs → encode b < encode bs
h : b ∈ b' :: bs
this : b = b' ∨ b ∈ bs
⊢ encode b < encode (b' :: bs)

State before:
case cons
β : Type u_1
inst✝ : Encodable β
b b' : β
bs : List β
ih : b ∈ bs → encode b < encode bs
h : b ∈ b' :: bs
this : b = b' ∨ b ∈ bs
⊢ encode b < encode (b' :: bs)
Tactic:
rcases this with (rfl | lt) <;> simp
State after:
case cons.inl
β : Type u_1
inst✝ : Encodable β
b : β
bs : List β
ih : b ∈ bs → encode b < encode bs
h : b ∈ b :: bs
⊢ encode b < (encode b).pair (encode bs) + 1

case cons.inr
β : Type u_1
inst✝ : Encodable β
b b' : β
bs : List β
ih : b ∈ bs → encode b < encode bs
h : b ∈ b' :: bs
lt : b ∈ bs
⊢ encode b < (encode b').pair (encode bs) + 1

State before:
β : Type u_1
inst✝ : Encodable β
b b' : β
bs : List β
ih : b ∈ bs → encode b < encode bs
h : b ∈ b' :: bs
⊢ b = b' ∨ b ∈ bs
Tactic:
simpa using h
State after:
no goals

State before:
case cons.inl
β : Type u_1
inst✝ : Encodable β
b : β
bs : List β
ih : b ∈ bs → encode b < encode bs
h : b ∈ b :: bs
⊢ encode b < (encode b).pair (encode bs) + 1
Tactic:
exact Nat.lt_succ.mpr (Nat.left_le_pair (encode b) (encode bs))
State after:
no goals

State before:
case cons.inr
β : Type u_1
inst✝ : Encodable β
b b' : β
bs : List β
ih : b ∈ bs → encode b < encode bs
h : b ∈ b' :: bs
lt : b ∈ bs
⊢ encode b < (encode b').pair (encode bs) + 1
Tactic:
exact Nat.lt.step <| lt_of_lt_of_le (ih lt) (Nat.right_le_pair (encode b') (encode bs))
State after:
no goals