Theorem: FOL.NV.finset_var_name_max_len_mem (FOL/NV/Fresh.lean)

State before:
x : VarName
xs : Finset VarName
h1 : x ∈ xs
⊢ x.length ≤ finset_var_name_max_len xs
Tactic:
induction xs using Finset.induction_on
State after:
case empty
x : VarName
h1 : x ∈ ∅
⊢ x.length ≤ finset_var_name_max_len ∅

case insert
x a✝² : VarName
s✝ : Finset VarName
a✝¹ : a✝² ∉ s✝
a✝ : x ∈ s✝ → x.length ≤ finset_var_name_max_len s✝
h1 : x ∈ insert a✝² s✝
⊢ x.length ≤ finset_var_name_max_len (insert a✝² s✝)

State before:
x : VarName
h1 : x ∈ ∅
⊢ x.length ≤ finset_var_name_max_len ∅
Tactic:
case empty =>
  simp at h1
State after:
no goals

State before:
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ finset_var_name_max_len tl
h1 : x ∈ insert hd tl
⊢ x.length ≤ finset_var_name_max_len (insert hd tl)
Tactic:
case insert hd tl a1 ih =>
  simp at h1
  cases h1
  case inl c1 =>
    subst c1
    simp only [finset_var_name_max_len]
    simp
  case inr c1 =>
    simp only [finset_var_name_max_len] at ih
    simp only [finset_var_name_max_len]
    simp
    right
    exact ih c1
State after:
no goals

State before:
x : VarName
h1 : x ∈ ∅
⊢ x.length ≤ finset_var_name_max_len ∅
Tactic:
simp at h1
State after:
no goals

State before:
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ finset_var_name_max_len tl
h1 : x ∈ insert hd tl
⊢ x.length ≤ finset_var_name_max_len (insert hd tl)
Tactic:
simp at h1
State after:
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ finset_var_name_max_len tl
h1 : x = hd ∨ x ∈ tl
⊢ x.length ≤ finset_var_name_max_len (insert hd tl)

State before:
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ finset_var_name_max_len tl
h1 : x = hd ∨ x ∈ tl
⊢ x.length ≤ finset_var_name_max_len (insert hd tl)
Tactic:
cases h1
State after:
case inl
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ finset_var_name_max_len tl
h✝ : x = hd
⊢ x.length ≤ finset_var_name_max_len (insert hd tl)

case inr
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ finset_var_name_max_len tl
h✝ : x ∈ tl
⊢ x.length ≤ finset_var_name_max_len (insert hd tl)

State before:
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ finset_var_name_max_len tl
c1 : x = hd
⊢ x.length ≤ finset_var_name_max_len (insert hd tl)
Tactic:
case inl c1 =>
  subst c1
  simp only [finset_var_name_max_len]
  simp
State after:
no goals

State before:
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ finset_var_name_max_len tl
c1 : x ∈ tl
⊢ x.length ≤ finset_var_name_max_len (insert hd tl)
Tactic:
case inr c1 =>
  simp only [finset_var_name_max_len] at ih
  simp only [finset_var_name_max_len]
  simp
  right
  exact ih c1
State after:
no goals

State before:
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ finset_var_name_max_len tl
c1 : x = hd
⊢ x.length ≤ finset_var_name_max_len (insert hd tl)
Tactic:
subst c1
State after:
x : VarName
tl : Finset VarName
ih : x ∈ tl → x.length ≤ finset_var_name_max_len tl
a1 : x ∉ tl
⊢ x.length ≤ finset_var_name_max_len (insert x tl)

State before:
x : VarName
tl : Finset VarName
ih : x ∈ tl → x.length ≤ finset_var_name_max_len tl
a1 : x ∉ tl
⊢ x.length ≤ finset_var_name_max_len (insert x tl)
Tactic:
simp only [finset_var_name_max_len]
State after:
x : VarName
tl : Finset VarName
ih : x ∈ tl → x.length ≤ finset_var_name_max_len tl
a1 : x ∉ tl
⊢ x.length ≤ Finset.fold (fun m n => max m n) 0 (String.length ∘ VarName.toString) (insert x tl)

State before:
x : VarName
tl : Finset VarName
ih : x ∈ tl → x.length ≤ finset_var_name_max_len tl
a1 : x ∉ tl
⊢ x.length ≤ Finset.fold (fun m n => max m n) 0 (String.length ∘ VarName.toString) (insert x tl)
Tactic:
simp
State after:
no goals

State before:
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ finset_var_name_max_len tl
c1 : x ∈ tl
⊢ x.length ≤ finset_var_name_max_len (insert hd tl)
Tactic:
simp only [finset_var_name_max_len] at ih
State after:
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ Finset.fold (fun m n => max m n) 0 (String.length ∘ VarName.toString) tl
c1 : x ∈ tl
⊢ x.length ≤ finset_var_name_max_len (insert hd tl)

State before:
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ Finset.fold (fun m n => max m n) 0 (String.length ∘ VarName.toString) tl
c1 : x ∈ tl
⊢ x.length ≤ finset_var_name_max_len (insert hd tl)
Tactic:
simp only [finset_var_name_max_len]
State after:
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ Finset.fold (fun m n => max m n) 0 (String.length ∘ VarName.toString) tl
c1 : x ∈ tl
⊢ x.length ≤ Finset.fold (fun m n => max m n) 0 (String.length ∘ VarName.toString) (insert hd tl)

State before:
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ Finset.fold (fun m n => max m n) 0 (String.length ∘ VarName.toString) tl
c1 : x ∈ tl
⊢ x.length ≤ Finset.fold (fun m n => max m n) 0 (String.length ∘ VarName.toString) (insert hd tl)
Tactic:
simp
State after:
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ Finset.fold (fun m n => max m n) 0 (String.length ∘ VarName.toString) tl
c1 : x ∈ tl
⊢ x.length ≤ hd.length ∨ x.length ≤ Finset.fold (fun m n => max m n) 0 (fun x => x.length) tl

State before:
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ Finset.fold (fun m n => max m n) 0 (String.length ∘ VarName.toString) tl
c1 : x ∈ tl
⊢ x.length ≤ hd.length ∨ x.length ≤ Finset.fold (fun m n => max m n) 0 (fun x => x.length) tl
Tactic:
right
State after:
case h
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ Finset.fold (fun m n => max m n) 0 (String.length ∘ VarName.toString) tl
c1 : x ∈ tl
⊢ x.length ≤ Finset.fold (fun m n => max m n) 0 (fun x => x.length) tl

State before:
case h
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ Finset.fold (fun m n => max m n) 0 (String.length ∘ VarName.toString) tl
c1 : x ∈ tl
⊢ x.length ≤ Finset.fold (fun m n => max m n) 0 (fun x => x.length) tl
Tactic:
exact ih c1
State after:
no goals