Theorem: LN.lc_at_zero_iff_is_free (FOL/LN/Paper.lean)

State before:
v : Var
⊢ Var.lc_at 0 v ↔ v.isFree
Tactic:
cases v
State after:
case free_
a✝ : String
⊢ Var.lc_at 0 (free_ a✝) ↔ (free_ a✝).isFree

case bound_
a✝ : ℕ
⊢ Var.lc_at 0 (bound_ a✝) ↔ (bound_ a✝).isFree

State before:
x : String
⊢ Var.lc_at 0 (free_ x) ↔ (free_ x).isFree
Tactic:
case free_ x =>
  simp only [Var.lc_at]
  simp only [isFree]
State after:
no goals

State before:
i : ℕ
⊢ Var.lc_at 0 (bound_ i) ↔ (bound_ i).isFree
Tactic:
case bound_ i =>
  simp only [Var.lc_at]
  simp only [isFree]
  simp
State after:
no goals

State before:
x : String
⊢ Var.lc_at 0 (free_ x) ↔ (free_ x).isFree
Tactic:
simp only [Var.lc_at]
State after:
x : String
⊢ True ↔ (free_ x).isFree

State before:
x : String
⊢ True ↔ (free_ x).isFree
Tactic:
simp only [isFree]
State after:
no goals

State before:
i : ℕ
⊢ Var.lc_at 0 (bound_ i) ↔ (bound_ i).isFree
Tactic:
simp only [Var.lc_at]
State after:
i : ℕ
⊢ i < 0 ↔ (bound_ i).isFree

State before:
i : ℕ
⊢ i < 0 ↔ (bound_ i).isFree
Tactic:
simp only [isFree]
State after:
i : ℕ
⊢ i < 0 ↔ False

State before:
i : ℕ
⊢ i < 0 ↔ False
Tactic:
simp
State after:
no goals