Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_same_on_free (FOL/NV/Sub/Var/All/Rec/ReplaceFree.lean)

State before:
F : Formula
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v F → σ v = σ' v
⊢ fastReplaceFree σ F = fastReplaceFree σ' F
Tactic:
induction F generalizing σ σ'
State after:
case pred_const_
a✝¹ : PredName
a✝ : List VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v (pred_const_ a✝¹ a✝) → σ v = σ' v
⊢ fastReplaceFree σ (pred_const_ a✝¹ a✝) = fastReplaceFree σ' (pred_const_ a✝¹ a✝)

case pred_var_
a✝¹ : PredName
a✝ : List VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v (pred_var_ a✝¹ a✝) → σ v = σ' v
⊢ fastReplaceFree σ (pred_var_ a✝¹ a✝) = fastReplaceFree σ' (pred_var_ a✝¹ a✝)

case eq_
a✝¹ a✝ : VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v (eq_ a✝¹ a✝) → σ v = σ' v
⊢ fastReplaceFree σ (eq_ a✝¹ a✝) = fastReplaceFree σ' (eq_ a✝¹ a✝)

case true_
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v true_ → σ v = σ' v
⊢ fastReplaceFree σ true_ = fastReplaceFree σ' true_

case false_
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v false_ → σ v = σ' v
⊢ fastReplaceFree σ false_ = fastReplaceFree σ' false_

case not_
a✝ : Formula
a_ih✝ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝ → σ v = σ' v) → fastReplaceFree σ a✝ = fastReplaceFree σ' a✝
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v a✝.not_ → σ v = σ' v
⊢ fastReplaceFree σ a✝.not_ = fastReplaceFree σ' a✝.not_

case imp_
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝¹ → σ v = σ' v) → fastReplaceFree σ a✝¹ = fastReplaceFree σ' a✝¹
a_ih✝ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝ → σ v = σ' v) → fastReplaceFree σ a✝ = fastReplaceFree σ' a✝
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v (a✝¹.imp_ a✝) → σ v = σ' v
⊢ fastReplaceFree σ (a✝¹.imp_ a✝) = fastReplaceFree σ' (a✝¹.imp_ a✝)

case and_
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝¹ → σ v = σ' v) → fastReplaceFree σ a✝¹ = fastReplaceFree σ' a✝¹
a_ih✝ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝ → σ v = σ' v) → fastReplaceFree σ a✝ = fastReplaceFree σ' a✝
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v (a✝¹.and_ a✝) → σ v = σ' v
⊢ fastReplaceFree σ (a✝¹.and_ a✝) = fastReplaceFree σ' (a✝¹.and_ a✝)

case or_
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝¹ → σ v = σ' v) → fastReplaceFree σ a✝¹ = fastReplaceFree σ' a✝¹
a_ih✝ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝ → σ v = σ' v) → fastReplaceFree σ a✝ = fastReplaceFree σ' a✝
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v (a✝¹.or_ a✝) → σ v = σ' v
⊢ fastReplaceFree σ (a✝¹.or_ a✝) = fastReplaceFree σ' (a✝¹.or_ a✝)

case iff_
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝¹ → σ v = σ' v) → fastReplaceFree σ a✝¹ = fastReplaceFree σ' a✝¹
a_ih✝ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝ → σ v = σ' v) → fastReplaceFree σ a✝ = fastReplaceFree σ' a✝
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v (a✝¹.iff_ a✝) → σ v = σ' v
⊢ fastReplaceFree σ (a✝¹.iff_ a✝) = fastReplaceFree σ' (a✝¹.iff_ a✝)

case forall_
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝ → σ v = σ' v) → fastReplaceFree σ a✝ = fastReplaceFree σ' a✝
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v (forall_ a✝¹ a✝) → σ v = σ' v
⊢ fastReplaceFree σ (forall_ a✝¹ a✝) = fastReplaceFree σ' (forall_ a✝¹ a✝)

case exists_
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝ → σ v = σ' v) → fastReplaceFree σ a✝ = fastReplaceFree σ' a✝
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v (exists_ a✝¹ a✝) → σ v = σ' v
⊢ fastReplaceFree σ (exists_ a✝¹ a✝) = fastReplaceFree σ' (exists_ a✝¹ a✝)

case def_
a✝¹ : DefName
a✝ : List VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v (def_ a✝¹ a✝) → σ v = σ' v
⊢ fastReplaceFree σ (def_ a✝¹ a✝) = fastReplaceFree σ' (def_ a✝¹ a✝)

State before:
case pred_const_
a✝¹ : PredName
a✝ : List VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v (pred_const_ a✝¹ a✝) → σ v = σ' v
⊢ fastReplaceFree σ (pred_const_ a✝¹ a✝) = fastReplaceFree σ' (pred_const_ a✝¹ a✝)

case pred_var_
a✝¹ : PredName
a✝ : List VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v (pred_var_ a✝¹ a✝) → σ v = σ' v
⊢ fastReplaceFree σ (pred_var_ a✝¹ a✝) = fastReplaceFree σ' (pred_var_ a✝¹ a✝)

case eq_
a✝¹ a✝ : VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v (eq_ a✝¹ a✝) → σ v = σ' v
⊢ fastReplaceFree σ (eq_ a✝¹ a✝) = fastReplaceFree σ' (eq_ a✝¹ a✝)

case true_
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v true_ → σ v = σ' v
⊢ fastReplaceFree σ true_ = fastReplaceFree σ' true_

case false_
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v false_ → σ v = σ' v
⊢ fastReplaceFree σ false_ = fastReplaceFree σ' false_

case not_
a✝ : Formula
a_ih✝ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝ → σ v = σ' v) → fastReplaceFree σ a✝ = fastReplaceFree σ' a✝
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v a✝.not_ → σ v = σ' v
⊢ fastReplaceFree σ a✝.not_ = fastReplaceFree σ' a✝.not_

case imp_
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝¹ → σ v = σ' v) → fastReplaceFree σ a✝¹ = fastReplaceFree σ' a✝¹
a_ih✝ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝ → σ v = σ' v) → fastReplaceFree σ a✝ = fastReplaceFree σ' a✝
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v (a✝¹.imp_ a✝) → σ v = σ' v
⊢ fastReplaceFree σ (a✝¹.imp_ a✝) = fastReplaceFree σ' (a✝¹.imp_ a✝)

case and_
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝¹ → σ v = σ' v) → fastReplaceFree σ a✝¹ = fastReplaceFree σ' a✝¹
a_ih✝ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝ → σ v = σ' v) → fastReplaceFree σ a✝ = fastReplaceFree σ' a✝
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v (a✝¹.and_ a✝) → σ v = σ' v
⊢ fastReplaceFree σ (a✝¹.and_ a✝) = fastReplaceFree σ' (a✝¹.and_ a✝)

case or_
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝¹ → σ v = σ' v) → fastReplaceFree σ a✝¹ = fastReplaceFree σ' a✝¹
a_ih✝ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝ → σ v = σ' v) → fastReplaceFree σ a✝ = fastReplaceFree σ' a✝
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v (a✝¹.or_ a✝) → σ v = σ' v
⊢ fastReplaceFree σ (a✝¹.or_ a✝) = fastReplaceFree σ' (a✝¹.or_ a✝)

case iff_
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝¹ → σ v = σ' v) → fastReplaceFree σ a✝¹ = fastReplaceFree σ' a✝¹
a_ih✝ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝ → σ v = σ' v) → fastReplaceFree σ a✝ = fastReplaceFree σ' a✝
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v (a✝¹.iff_ a✝) → σ v = σ' v
⊢ fastReplaceFree σ (a✝¹.iff_ a✝) = fastReplaceFree σ' (a✝¹.iff_ a✝)

case forall_
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝ → σ v = σ' v) → fastReplaceFree σ a✝ = fastReplaceFree σ' a✝
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v (forall_ a✝¹ a✝) → σ v = σ' v
⊢ fastReplaceFree σ (forall_ a✝¹ a✝) = fastReplaceFree σ' (forall_ a✝¹ a✝)

case exists_
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝ → σ v = σ' v) → fastReplaceFree σ a✝ = fastReplaceFree σ' a✝
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v (exists_ a✝¹ a✝) → σ v = σ' v
⊢ fastReplaceFree σ (exists_ a✝¹ a✝) = fastReplaceFree σ' (exists_ a✝¹ a✝)

case def_
a✝¹ : DefName
a✝ : List VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v (def_ a✝¹ a✝) → σ v = σ' v
⊢ fastReplaceFree σ (def_ a✝¹ a✝) = fastReplaceFree σ' (def_ a✝¹ a✝)
Tactic:
all_goals
  simp only [isFreeIn] at h1
  simp only [fastReplaceFree]
State after:
case pred_const_
a✝¹ : PredName
a✝ : List VarName
σ σ' : VarName → VarName
h1 : ∀ v ∈ a✝, σ v = σ' v
⊢ pred_const_ a✝¹ (List.map σ a✝) = pred_const_ a✝¹ (List.map σ' a✝)

case pred_var_
a✝¹ : PredName
a✝ : List VarName
σ σ' : VarName → VarName
h1 : ∀ v ∈ a✝, σ v = σ' v
⊢ pred_var_ a✝¹ (List.map σ a✝) = pred_var_ a✝¹ (List.map σ' a✝)

case eq_
a✝¹ a✝ : VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), v = a✝¹ ∨ v = a✝ → σ v = σ' v
⊢ eq_ (σ a✝¹) (σ a✝) = eq_ (σ' a✝¹) (σ' a✝)

case not_
a✝ : Formula
a_ih✝ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝ → σ v = σ' v) → fastReplaceFree σ a✝ = fastReplaceFree σ' a✝
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v a✝ → σ v = σ' v
⊢ (fastReplaceFree σ a✝).not_ = (fastReplaceFree σ' a✝).not_

case imp_
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝¹ → σ v = σ' v) → fastReplaceFree σ a✝¹ = fastReplaceFree σ' a✝¹
a_ih✝ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝ → σ v = σ' v) → fastReplaceFree σ a✝ = fastReplaceFree σ' a✝
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v a✝¹ ∨ isFreeIn v a✝ → σ v = σ' v
⊢ (fastReplaceFree σ a✝¹).imp_ (fastReplaceFree σ a✝) = (fastReplaceFree σ' a✝¹).imp_ (fastReplaceFree σ' a✝)

case and_
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝¹ → σ v = σ' v) → fastReplaceFree σ a✝¹ = fastReplaceFree σ' a✝¹
a_ih✝ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝ → σ v = σ' v) → fastReplaceFree σ a✝ = fastReplaceFree σ' a✝
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v a✝¹ ∨ isFreeIn v a✝ → σ v = σ' v
⊢ (fastReplaceFree σ a✝¹).and_ (fastReplaceFree σ a✝) = (fastReplaceFree σ' a✝¹).and_ (fastReplaceFree σ' a✝)

case or_
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝¹ → σ v = σ' v) → fastReplaceFree σ a✝¹ = fastReplaceFree σ' a✝¹
a_ih✝ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝ → σ v = σ' v) → fastReplaceFree σ a✝ = fastReplaceFree σ' a✝
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v a✝¹ ∨ isFreeIn v a✝ → σ v = σ' v
⊢ (fastReplaceFree σ a✝¹).or_ (fastReplaceFree σ a✝) = (fastReplaceFree σ' a✝¹).or_ (fastReplaceFree σ' a✝)

case iff_
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝¹ → σ v = σ' v) → fastReplaceFree σ a✝¹ = fastReplaceFree σ' a✝¹
a_ih✝ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝ → σ v = σ' v) → fastReplaceFree σ a✝ = fastReplaceFree σ' a✝
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v a✝¹ ∨ isFreeIn v a✝ → σ v = σ' v
⊢ (fastReplaceFree σ a✝¹).iff_ (fastReplaceFree σ a✝) = (fastReplaceFree σ' a✝¹).iff_ (fastReplaceFree σ' a✝)

case forall_
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝ → σ v = σ' v) → fastReplaceFree σ a✝ = fastReplaceFree σ' a✝
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), ¬v = a✝¹ ∧ isFreeIn v a✝ → σ v = σ' v
⊢ forall_ a✝¹ (fastReplaceFree (Function.updateITE σ a✝¹ a✝¹) a✝) =
    forall_ a✝¹ (fastReplaceFree (Function.updateITE σ' a✝¹ a✝¹) a✝)

case exists_
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝ → σ v = σ' v) → fastReplaceFree σ a✝ = fastReplaceFree σ' a✝
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), ¬v = a✝¹ ∧ isFreeIn v a✝ → σ v = σ' v
⊢ exists_ a✝¹ (fastReplaceFree (Function.updateITE σ a✝¹ a✝¹) a✝) =
    exists_ a✝¹ (fastReplaceFree (Function.updateITE σ' a✝¹ a✝¹) a✝)

case def_
a✝¹ : DefName
a✝ : List VarName
σ σ' : VarName → VarName
h1 : ∀ v ∈ a✝, σ v = σ' v
⊢ def_ a✝¹ (List.map σ a✝) = def_ a✝¹ (List.map σ' a✝)

State before:
X : DefName
xs : List VarName
σ σ' : VarName → VarName
h1 : ∀ v ∈ xs, σ v = σ' v
⊢ def_ X (List.map σ xs) = def_ X (List.map σ' xs)
Tactic:
case pred_const_ X xs | pred_var_ X xs | def_ X xs =>
  congr! 1
  simp only [List.map_eq_map_iff]
  exact h1
State after:
no goals

State before:
phi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi → σ v = σ' v
⊢ (fastReplaceFree σ phi).not_ = (fastReplaceFree σ' phi).not_
Tactic:
case not_ phi phi_ih =>
  congr! 1
  exact phi_ih σ σ' h1
State after:
no goals

State before:
x : VarName
phi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), ¬v = x ∧ isFreeIn v phi → σ v = σ' v
⊢ exists_ x (fastReplaceFree (Function.updateITE σ x x) phi) =
    exists_ x (fastReplaceFree (Function.updateITE σ' x x) phi)
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  congr! 1
  apply phi_ih
  intro v a1
  simp only [Function.updateITE]
  split_ifs
  case _ c1 =>
    rfl
  case _ c1 =>
    apply h1
    tauto
State after:
no goals

State before:
case def_
a✝¹ : DefName
a✝ : List VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v (def_ a✝¹ a✝) → σ v = σ' v
⊢ fastReplaceFree σ (def_ a✝¹ a✝) = fastReplaceFree σ' (def_ a✝¹ a✝)
Tactic:
simp only [isFreeIn] at h1
State after:
case def_
a✝¹ : DefName
a✝ : List VarName
σ σ' : VarName → VarName
h1 : ∀ v ∈ a✝, σ v = σ' v
⊢ fastReplaceFree σ (def_ a✝¹ a✝) = fastReplaceFree σ' (def_ a✝¹ a✝)

State before:
case def_
a✝¹ : DefName
a✝ : List VarName
σ σ' : VarName → VarName
h1 : ∀ v ∈ a✝, σ v = σ' v
⊢ fastReplaceFree σ (def_ a✝¹ a✝) = fastReplaceFree σ' (def_ a✝¹ a✝)
Tactic:
simp only [fastReplaceFree]
State after:
case def_
a✝¹ : DefName
a✝ : List VarName
σ σ' : VarName → VarName
h1 : ∀ v ∈ a✝, σ v = σ' v
⊢ def_ a✝¹ (List.map σ a✝) = def_ a✝¹ (List.map σ' a✝)

State before:
X : DefName
xs : List VarName
σ σ' : VarName → VarName
h1 : ∀ v ∈ xs, σ v = σ' v
⊢ def_ X (List.map σ xs) = def_ X (List.map σ' xs)
Tactic:
congr! 1
State after:
case h.e'_2
X : DefName
xs : List VarName
σ σ' : VarName → VarName
h1 : ∀ v ∈ xs, σ v = σ' v
⊢ List.map σ xs = List.map σ' xs

State before:
case h.e'_2
X : DefName
xs : List VarName
σ σ' : VarName → VarName
h1 : ∀ v ∈ xs, σ v = σ' v
⊢ List.map σ xs = List.map σ' xs
Tactic:
simp only [List.map_eq_map_iff]
State after:
case h.e'_2
X : DefName
xs : List VarName
σ σ' : VarName → VarName
h1 : ∀ v ∈ xs, σ v = σ' v
⊢ ∀ x ∈ xs, σ x = σ' x

State before:
case h.e'_2
X : DefName
xs : List VarName
σ σ' : VarName → VarName
h1 : ∀ v ∈ xs, σ v = σ' v
⊢ ∀ x ∈ xs, σ x = σ' x
Tactic:
exact h1
State after:
no goals

State before:
x y : VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), v = x ∨ v = y → σ v = σ' v
⊢ eq_ (σ x) (σ y) = eq_ (σ' x) (σ' y)
Tactic:
congr! 1
State after:
case h.e'_1
x y : VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), v = x ∨ v = y → σ v = σ' v
⊢ σ x = σ' x

case h.e'_2
x y : VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), v = x ∨ v = y → σ v = σ' v
⊢ σ y = σ' y

State before:
case h.e'_1
x y : VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), v = x ∨ v = y → σ v = σ' v
⊢ σ x = σ' x
Tactic:
apply h1
State after:
case h.e'_1.a
x y : VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), v = x ∨ v = y → σ v = σ' v
⊢ x = x ∨ x = y

State before:
case h.e'_1.a
x y : VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), v = x ∨ v = y → σ v = σ' v
⊢ x = x ∨ x = y
Tactic:
left
State after:
case h.e'_1.a.h
x y : VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), v = x ∨ v = y → σ v = σ' v
⊢ x = x

State before:
case h.e'_1.a.h
x y : VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), v = x ∨ v = y → σ v = σ' v
⊢ x = x
Tactic:
rfl
State after:
no goals

State before:
case h.e'_2
x y : VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), v = x ∨ v = y → σ v = σ' v
⊢ σ y = σ' y
Tactic:
apply h1
State after:
case h.e'_2.a
x y : VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), v = x ∨ v = y → σ v = σ' v
⊢ y = x ∨ y = y

State before:
case h.e'_2.a
x y : VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), v = x ∨ v = y → σ v = σ' v
⊢ y = x ∨ y = y
Tactic:
right
State after:
case h.e'_2.a.h
x y : VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), v = x ∨ v = y → σ v = σ' v
⊢ y = y

State before:
case h.e'_2.a.h
x y : VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), v = x ∨ v = y → σ v = σ' v
⊢ y = y
Tactic:
rfl
State after:
no goals

State before:
phi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi → σ v = σ' v
⊢ (fastReplaceFree σ phi).not_ = (fastReplaceFree σ' phi).not_
Tactic:
congr! 1
State after:
case h.e'_1
phi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi → σ v = σ' v
⊢ fastReplaceFree σ phi = fastReplaceFree σ' phi

State before:
case h.e'_1
phi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi → σ v = σ' v
⊢ fastReplaceFree σ phi = fastReplaceFree σ' phi
Tactic:
exact phi_ih σ σ' h1
State after:
no goals

State before:
phi psi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
psi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v psi → σ v = σ' v) → fastReplaceFree σ psi = fastReplaceFree σ' psi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → σ v = σ' v
⊢ (fastReplaceFree σ phi).iff_ (fastReplaceFree σ psi) = (fastReplaceFree σ' phi).iff_ (fastReplaceFree σ' psi)
Tactic:
congr! 1
State after:
case h.e'_1
phi psi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
psi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v psi → σ v = σ' v) → fastReplaceFree σ psi = fastReplaceFree σ' psi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → σ v = σ' v
⊢ fastReplaceFree σ phi = fastReplaceFree σ' phi

case h.e'_2
phi psi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
psi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v psi → σ v = σ' v) → fastReplaceFree σ psi = fastReplaceFree σ' psi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → σ v = σ' v
⊢ fastReplaceFree σ psi = fastReplaceFree σ' psi

State before:
case h.e'_1
phi psi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
psi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v psi → σ v = σ' v) → fastReplaceFree σ psi = fastReplaceFree σ' psi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → σ v = σ' v
⊢ fastReplaceFree σ phi = fastReplaceFree σ' phi
Tactic:
apply phi_ih
State after:
case h.e'_1.h1
phi psi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
psi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v psi → σ v = σ' v) → fastReplaceFree σ psi = fastReplaceFree σ' psi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → σ v = σ' v
⊢ ∀ (v : VarName), isFreeIn v phi → σ v = σ' v

State before:
case h.e'_1.h1
phi psi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
psi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v psi → σ v = σ' v) → fastReplaceFree σ psi = fastReplaceFree σ' psi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → σ v = σ' v
⊢ ∀ (v : VarName), isFreeIn v phi → σ v = σ' v
Tactic:
intro v a1
State after:
case h.e'_1.h1
phi psi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
psi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v psi → σ v = σ' v) → fastReplaceFree σ psi = fastReplaceFree σ' psi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → σ v = σ' v
v : VarName
a1 : isFreeIn v phi
⊢ σ v = σ' v

State before:
case h.e'_1.h1
phi psi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
psi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v psi → σ v = σ' v) → fastReplaceFree σ psi = fastReplaceFree σ' psi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → σ v = σ' v
v : VarName
a1 : isFreeIn v phi
⊢ σ v = σ' v
Tactic:
apply h1
State after:
case h.e'_1.h1.a
phi psi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
psi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v psi → σ v = σ' v) → fastReplaceFree σ psi = fastReplaceFree σ' psi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → σ v = σ' v
v : VarName
a1 : isFreeIn v phi
⊢ isFreeIn v phi ∨ isFreeIn v psi

State before:
case h.e'_1.h1.a
phi psi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
psi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v psi → σ v = σ' v) → fastReplaceFree σ psi = fastReplaceFree σ' psi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → σ v = σ' v
v : VarName
a1 : isFreeIn v phi
⊢ isFreeIn v phi ∨ isFreeIn v psi
Tactic:
left
State after:
case h.e'_1.h1.a.h
phi psi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
psi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v psi → σ v = σ' v) → fastReplaceFree σ psi = fastReplaceFree σ' psi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → σ v = σ' v
v : VarName
a1 : isFreeIn v phi
⊢ isFreeIn v phi

State before:
case h.e'_1.h1.a.h
phi psi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
psi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v psi → σ v = σ' v) → fastReplaceFree σ psi = fastReplaceFree σ' psi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → σ v = σ' v
v : VarName
a1 : isFreeIn v phi
⊢ isFreeIn v phi
Tactic:
exact a1
State after:
no goals

State before:
case h.e'_2
phi psi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
psi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v psi → σ v = σ' v) → fastReplaceFree σ psi = fastReplaceFree σ' psi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → σ v = σ' v
⊢ fastReplaceFree σ psi = fastReplaceFree σ' psi
Tactic:
apply psi_ih
State after:
case h.e'_2.h1
phi psi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
psi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v psi → σ v = σ' v) → fastReplaceFree σ psi = fastReplaceFree σ' psi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → σ v = σ' v
⊢ ∀ (v : VarName), isFreeIn v psi → σ v = σ' v

State before:
case h.e'_2.h1
phi psi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
psi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v psi → σ v = σ' v) → fastReplaceFree σ psi = fastReplaceFree σ' psi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → σ v = σ' v
⊢ ∀ (v : VarName), isFreeIn v psi → σ v = σ' v
Tactic:
intro v a1
State after:
case h.e'_2.h1
phi psi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
psi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v psi → σ v = σ' v) → fastReplaceFree σ psi = fastReplaceFree σ' psi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → σ v = σ' v
v : VarName
a1 : isFreeIn v psi
⊢ σ v = σ' v

State before:
case h.e'_2.h1
phi psi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
psi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v psi → σ v = σ' v) → fastReplaceFree σ psi = fastReplaceFree σ' psi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → σ v = σ' v
v : VarName
a1 : isFreeIn v psi
⊢ σ v = σ' v
Tactic:
apply h1
State after:
case h.e'_2.h1.a
phi psi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
psi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v psi → σ v = σ' v) → fastReplaceFree σ psi = fastReplaceFree σ' psi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → σ v = σ' v
v : VarName
a1 : isFreeIn v psi
⊢ isFreeIn v phi ∨ isFreeIn v psi

State before:
case h.e'_2.h1.a
phi psi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
psi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v psi → σ v = σ' v) → fastReplaceFree σ psi = fastReplaceFree σ' psi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → σ v = σ' v
v : VarName
a1 : isFreeIn v psi
⊢ isFreeIn v phi ∨ isFreeIn v psi
Tactic:
right
State after:
case h.e'_2.h1.a.h
phi psi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
psi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v psi → σ v = σ' v) → fastReplaceFree σ psi = fastReplaceFree σ' psi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → σ v = σ' v
v : VarName
a1 : isFreeIn v psi
⊢ isFreeIn v psi

State before:
case h.e'_2.h1.a.h
phi psi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
psi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v psi → σ v = σ' v) → fastReplaceFree σ psi = fastReplaceFree σ' psi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → σ v = σ' v
v : VarName
a1 : isFreeIn v psi
⊢ isFreeIn v psi
Tactic:
exact a1
State after:
no goals

State before:
x : VarName
phi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), ¬v = x ∧ isFreeIn v phi → σ v = σ' v
⊢ exists_ x (fastReplaceFree (Function.updateITE σ x x) phi) =
    exists_ x (fastReplaceFree (Function.updateITE σ' x x) phi)
Tactic:
congr! 1
State after:
case h.e'_2
x : VarName
phi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), ¬v = x ∧ isFreeIn v phi → σ v = σ' v
⊢ fastReplaceFree (Function.updateITE σ x x) phi = fastReplaceFree (Function.updateITE σ' x x) phi

State before:
case h.e'_2
x : VarName
phi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), ¬v = x ∧ isFreeIn v phi → σ v = σ' v
⊢ fastReplaceFree (Function.updateITE σ x x) phi = fastReplaceFree (Function.updateITE σ' x x) phi
Tactic:
apply phi_ih
State after:
case h.e'_2.h1
x : VarName
phi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), ¬v = x ∧ isFreeIn v phi → σ v = σ' v
⊢ ∀ (v : VarName), isFreeIn v phi → Function.updateITE σ x x v = Function.updateITE σ' x x v

State before:
case h.e'_2.h1
x : VarName
phi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), ¬v = x ∧ isFreeIn v phi → σ v = σ' v
⊢ ∀ (v : VarName), isFreeIn v phi → Function.updateITE σ x x v = Function.updateITE σ' x x v
Tactic:
intro v a1
State after:
case h.e'_2.h1
x : VarName
phi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), ¬v = x ∧ isFreeIn v phi → σ v = σ' v
v : VarName
a1 : isFreeIn v phi
⊢ Function.updateITE σ x x v = Function.updateITE σ' x x v

State before:
case h.e'_2.h1
x : VarName
phi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), ¬v = x ∧ isFreeIn v phi → σ v = σ' v
v : VarName
a1 : isFreeIn v phi
⊢ Function.updateITE σ x x v = Function.updateITE σ' x x v
Tactic:
simp only [Function.updateITE]
State after:
case h.e'_2.h1
x : VarName
phi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), ¬v = x ∧ isFreeIn v phi → σ v = σ' v
v : VarName
a1 : isFreeIn v phi
⊢ (if v = x then x else σ v) = if v = x then x else σ' v

State before:
case h.e'_2.h1
x : VarName
phi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), ¬v = x ∧ isFreeIn v phi → σ v = σ' v
v : VarName
a1 : isFreeIn v phi
⊢ (if v = x then x else σ v) = if v = x then x else σ' v
Tactic:
split_ifs
State after:
case pos
x : VarName
phi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), ¬v = x ∧ isFreeIn v phi → σ v = σ' v
v : VarName
a1 : isFreeIn v phi
h✝ : v = x
⊢ x = x

case neg
x : VarName
phi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), ¬v = x ∧ isFreeIn v phi → σ v = σ' v
v : VarName
a1 : isFreeIn v phi
h✝ : ¬v = x
⊢ σ v = σ' v

State before:
x : VarName
phi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), ¬v = x ∧ isFreeIn v phi → σ v = σ' v
v : VarName
a1 : isFreeIn v phi
c1 : v = x
⊢ x = x
Tactic:
case _ c1 =>
  rfl
State after:
no goals

State before:
x : VarName
phi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), ¬v = x ∧ isFreeIn v phi → σ v = σ' v
v : VarName
a1 : isFreeIn v phi
c1 : ¬v = x
⊢ σ v = σ' v
Tactic:
case _ c1 =>
  apply h1
  tauto
State after:
no goals

State before:
x : VarName
phi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), ¬v = x ∧ isFreeIn v phi → σ v = σ' v
v : VarName
a1 : isFreeIn v phi
c1 : v = x
⊢ x = x
Tactic:
rfl
State after:
no goals

State before:
x : VarName
phi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), ¬v = x ∧ isFreeIn v phi → σ v = σ' v
v : VarName
a1 : isFreeIn v phi
c1 : ¬v = x
⊢ σ v = σ' v
Tactic:
apply h1
State after:
case a
x : VarName
phi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), ¬v = x ∧ isFreeIn v phi → σ v = σ' v
v : VarName
a1 : isFreeIn v phi
c1 : ¬v = x
⊢ ¬v = x ∧ isFreeIn v phi

State before:
case a
x : VarName
phi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), ¬v = x ∧ isFreeIn v phi → σ v = σ' v
v : VarName
a1 : isFreeIn v phi
c1 : ¬v = x
⊢ ¬v = x ∧ isFreeIn v phi
Tactic:
tauto
State after:
no goals