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

State before:
x : VarName
c : Char
xs : Finset VarName
h : x ∈ xs
⊢ finset_var_name_max_len xs - x.length < finset_var_name_max_len xs + 1 - x.length
Tactic:
obtain s1 := finset_var_name_max_len_mem x xs h
State after:
x : VarName
c : Char
xs : Finset VarName
h : x ∈ xs
s1 : x.length ≤ finset_var_name_max_len xs
⊢ finset_var_name_max_len xs - x.length < finset_var_name_max_len xs + 1 - x.length

State before:
x : VarName
c : Char
xs : Finset VarName
h : x ∈ xs
s1 : x.length ≤ finset_var_name_max_len xs
⊢ finset_var_name_max_len xs - x.length < finset_var_name_max_len xs + 1 - x.length
Tactic:
simp only [tsub_lt_tsub_iff_right s1]
State after:
x : VarName
c : Char
xs : Finset VarName
h : x ∈ xs
s1 : x.length ≤ finset_var_name_max_len xs
⊢ finset_var_name_max_len xs < finset_var_name_max_len xs + 1

State before:
x : VarName
c : Char
xs : Finset VarName
h : x ∈ xs
s1 : x.length ≤ finset_var_name_max_len xs
⊢ finset_var_name_max_len xs < finset_var_name_max_len xs + 1
Tactic:
simp
State after:
no goals

State before:
x : VarName
c : Char
xs : Finset VarName
h : x ∈ xs
this : finset_var_name_max_len xs - x.length < finset_var_name_max_len xs + 1 - x.length
⊢ fresh x c xs ∉ xs
Tactic:
unfold fresh
State after:
x : VarName
c : Char
xs : Finset VarName
h : x ∈ xs
this : finset_var_name_max_len xs - x.length < finset_var_name_max_len xs + 1 - x.length
⊢ (if h : x ∈ xs then
      let_fun this := ⋯;
      fresh { toString := x.toString ++ c.toString } c xs
    else x) ∉
    xs

State before:
x : VarName
c : Char
xs : Finset VarName
h : x ∈ xs
this : finset_var_name_max_len xs - x.length < finset_var_name_max_len xs + 1 - x.length
⊢ (if h : x ∈ xs then
      let_fun this := ⋯;
      fresh { toString := x.toString ++ c.toString } c xs
    else x) ∉
    xs
Tactic:
simp
State after:
x : VarName
c : Char
xs : Finset VarName
h : x ∈ xs
this : finset_var_name_max_len xs - x.length < finset_var_name_max_len xs + 1 - x.length
⊢ (if x ∈ xs then fresh { toString := x.toString ++ c.toString } c xs else x) ∉ xs

State before:
x : VarName
c : Char
xs : Finset VarName
h : x ∈ xs
this : finset_var_name_max_len xs - x.length < finset_var_name_max_len xs + 1 - x.length
⊢ (if x ∈ xs then fresh { toString := x.toString ++ c.toString } c xs else x) ∉ xs
Tactic:
simp only [if_pos h]
State after:
x : VarName
c : Char
xs : Finset VarName
h : x ∈ xs
this : finset_var_name_max_len xs - x.length < finset_var_name_max_len xs + 1 - x.length
⊢ fresh { toString := x.toString ++ c.toString } c xs ∉ xs

State before:
x : VarName
c : Char
xs : Finset VarName
h : x ∈ xs
this : finset_var_name_max_len xs - x.length < finset_var_name_max_len xs + 1 - x.length
⊢ fresh { toString := x.toString ++ c.toString } c xs ∉ xs
Tactic:
apply fresh_not_mem
State after:
no goals

State before:
x : VarName
c : Char
xs : Finset VarName
h : x ∉ xs
⊢ fresh x c xs ∉ xs
Tactic:
unfold fresh
State after:
x : VarName
c : Char
xs : Finset VarName
h : x ∉ xs
⊢ (if h : x ∈ xs then
      let_fun this := ⋯;
      fresh { toString := x.toString ++ c.toString } c xs
    else x) ∉
    xs

State before:
x : VarName
c : Char
xs : Finset VarName
h : x ∉ xs
⊢ (if h : x ∈ xs then
      let_fun this := ⋯;
      fresh { toString := x.toString ++ c.toString } c xs
    else x) ∉
    xs
Tactic:
simp
State after:
x : VarName
c : Char
xs : Finset VarName
h : x ∉ xs
⊢ (if x ∈ xs then fresh { toString := x.toString ++ c.toString } c xs else x) ∉ xs

State before:
x : VarName
c : Char
xs : Finset VarName
h : x ∉ xs
⊢ (if x ∈ xs then fresh { toString := x.toString ++ c.toString } c xs else x) ∉ xs
Tactic:
simp [if_neg h]
State after:
x : VarName
c : Char
xs : Finset VarName
h : x ∉ xs
⊢ x ∉ xs

State before:
x : VarName
c : Char
xs : Finset VarName
h : x ∉ xs
⊢ x ∉ xs
Tactic:
exact h
State after:
no goals