Theorem: max_var_name_mem (ReckonLean/Fol.lean)

State before:
⊢ ∀ (v : String) (vars : List String), v ∈ vars → String.length v ≤ max_var_name vars
Tactic:
intro v vars
State after:
v : String
vars : List String
⊢ v ∈ vars → String.length v ≤ max_var_name vars

State before:
v : String
vars : List String
⊢ v ∈ vars → String.length v ≤ max_var_name vars
Tactic:
induction vars with
| nil =>
  intro hm
  exact absurd hm (List.not_mem_nil v)
| cons x xs ih =>
  intro h
  rw [List.mem_cons] at h
  cases h with
  | inl hvx =>
    unfold max_var_name
    conv => rhs; rw [← hvx]
    apply Nat.le_max_left
  | inr hvxs =>
    unfold max_var_name
    calc
      v.length ≤ max_var_name xs := ih hvxs
      _        ≤ Nat.max x.length (max_var_name xs) := by apply Nat.le_max_right
State after:
no goals

State before:
case nil
v : String
⊢ v ∈ [] → String.length v ≤ max_var_name []
Tactic:
intro hm
State after:
case nil
v : String
hm : v ∈ []
⊢ String.length v ≤ max_var_name []

State before:
case nil
v : String
hm : v ∈ []
⊢ String.length v ≤ max_var_name []
Tactic:
exact absurd hm (List.not_mem_nil v)
State after:
no goals

State before:
case cons
v x : String
xs : List String
ih : v ∈ xs → String.length v ≤ max_var_name xs
⊢ v ∈ x :: xs → String.length v ≤ max_var_name (x :: xs)
Tactic:
intro h
State after:
case cons
v x : String
xs : List String
ih : v ∈ xs → String.length v ≤ max_var_name xs
h : v ∈ x :: xs
⊢ String.length v ≤ max_var_name (x :: xs)

State before:
case cons
v x : String
xs : List String
ih : v ∈ xs → String.length v ≤ max_var_name xs
h : v ∈ x :: xs
⊢ String.length v ≤ max_var_name (x :: xs)
Tactic:
rw [List.mem_cons] at h
State after:
case cons
v x : String
xs : List String
ih : v ∈ xs → String.length v ≤ max_var_name xs
h : v = x ∨ v ∈ xs
⊢ String.length v ≤ max_var_name (x :: xs)

State before:
case cons
v x : String
xs : List String
ih : v ∈ xs → String.length v ≤ max_var_name xs
h : v = x ∨ v ∈ xs
⊢ String.length v ≤ max_var_name (x :: xs)
Tactic:
cases h with
| inl hvx =>
  unfold max_var_name
  conv => rhs; rw [← hvx]
  apply Nat.le_max_left
| inr hvxs =>
  unfold max_var_name
  calc
    v.length ≤ max_var_name xs := ih hvxs
    _        ≤ Nat.max x.length (max_var_name xs) := by apply Nat.le_max_right
State after:
no goals

State before:
case cons.inl
v x : String
xs : List String
ih : v ∈ xs → String.length v ≤ max_var_name xs
hvx : v = x
⊢ String.length v ≤ max_var_name (x :: xs)
Tactic:
unfold max_var_name
State after:
case cons.inl
v x : String
xs : List String
ih : v ∈ xs → String.length v ≤ max_var_name xs
hvx : v = x
⊢ String.length v ≤ Nat.max (String.length x) (max_var_name xs)

State before:
case cons.inl
v x : String
xs : List String
ih : v ∈ xs → String.length v ≤ max_var_name xs
hvx : v = x
⊢ String.length v ≤ Nat.max (String.length x) (max_var_name xs)
Tactic:
conv => rhs; rw [← hvx]
State after:
case cons.inl
v x : String
xs : List String
ih : v ∈ xs → String.length v ≤ max_var_name xs
hvx : v = x
⊢ String.length v ≤ Nat.max (String.length v) (max_var_name xs)

State before:
case cons.inl
v x : String
xs : List String
ih : v ∈ xs → String.length v ≤ max_var_name xs
hvx : v = x
⊢ String.length v ≤ Nat.max (String.length v) (max_var_name xs)
Tactic:
apply Nat.le_max_left
State after:
no goals

State before:
case cons.inr
v x : String
xs : List String
ih : v ∈ xs → String.length v ≤ max_var_name xs
hvxs : v ∈ xs
⊢ String.length v ≤ max_var_name (x :: xs)
Tactic:
unfold max_var_name
State after:
case cons.inr
v x : String
xs : List String
ih : v ∈ xs → String.length v ≤ max_var_name xs
hvxs : v ∈ xs
⊢ String.length v ≤ Nat.max (String.length x) (max_var_name xs)

State before:
case cons.inr
v x : String
xs : List String
ih : v ∈ xs → String.length v ≤ max_var_name xs
hvxs : v ∈ xs
⊢ String.length v ≤ Nat.max (String.length x) (max_var_name xs)
Tactic:
calc
  v.length ≤ max_var_name xs := ih hvxs
  _        ≤ Nat.max x.length (max_var_name xs) := by apply Nat.le_max_right
State after:
no goals

State before:
v x : String
xs : List String
ih : v ∈ xs → String.length v ≤ max_var_name xs
hvxs : v ∈ xs
⊢ max_var_name xs ≤ Nat.max (String.length x) (max_var_name xs)
Tactic:
apply Nat.le_max_right
State after:
no goals