Theorem: repl_in_dis (Pdl/Substitution.lean)

State before:
x : ℕ
ψ : Formula
l : List Formula
⊢ repl_in_F x ψ (dis l) = dis (List.map (repl_in_F x ψ) l)
Tactic:
cases l
State after:
case nil
x : ℕ
ψ : Formula
⊢ repl_in_F x ψ (dis []) = dis (List.map (repl_in_F x ψ) [])

case cons
x : ℕ
ψ head✝ : Formula
tail✝ : List Formula
⊢ repl_in_F x ψ (dis (head✝ :: tail✝)) = dis (List.map (repl_in_F x ψ) (head✝ :: tail✝))

State before:
case nil
x : ℕ
ψ : Formula
⊢ repl_in_F x ψ (dis []) = dis (List.map (repl_in_F x ψ) [])
Tactic:
simp
State after:
no goals

State before:
x : ℕ
ψ φ1 : Formula
l : List Formula
⊢ repl_in_F x ψ (dis (φ1 :: l)) = dis (List.map (repl_in_F x ψ) (φ1 :: l))
Tactic:
cases l
State after:
case nil
x : ℕ
ψ φ1 : Formula
⊢ repl_in_F x ψ (dis [φ1]) = dis (List.map (repl_in_F x ψ) [φ1])

case cons
x : ℕ
ψ φ1 head✝ : Formula
tail✝ : List Formula
⊢ repl_in_F x ψ (dis (φ1 :: head✝ :: tail✝)) = dis (List.map (repl_in_F x ψ) (φ1 :: head✝ :: tail✝))

State before:
x : ℕ
ψ φ1 φ2 : Formula
l : List Formula
⊢ repl_in_F x ψ (dis (φ1 :: φ2 :: l)) = dis (List.map (repl_in_F x ψ) (φ1 :: φ2 :: l))
Tactic:
case cons φ2 l =>
  simp [dis]
  apply repl_in_dis
State after:
no goals

State before:
case nil
x : ℕ
ψ φ1 : Formula
⊢ repl_in_F x ψ (dis [φ1]) = dis (List.map (repl_in_F x ψ) [φ1])
Tactic:
simp
State after:
no goals

State before:
x : ℕ
ψ φ1 φ2 : Formula
l : List Formula
⊢ repl_in_F x ψ (dis (φ1 :: φ2 :: l)) = dis (List.map (repl_in_F x ψ) (φ1 :: φ2 :: l))
Tactic:
simp [dis]
State after:
x : ℕ
ψ φ1 φ2 : Formula
l : List Formula
⊢ repl_in_F x ψ (dis (φ2 :: l)) = dis (repl_in_F x ψ φ2 :: List.map (repl_in_F x ψ) l)

State before:
x : ℕ
ψ φ1 φ2 : Formula
l : List Formula
⊢ repl_in_F x ψ (dis (φ2 :: l)) = dis (repl_in_F x ψ φ2 :: List.map (repl_in_F x ψ) l)
Tactic:
apply repl_in_dis
State after:
no goals