Theorem: repl_in_disMap (Pdl/Substitution.lean)

State before:
α : Type u_1
x : ℕ
ρ : Formula
L : List α
p : α → Prop
f : α → Formula
inst✝ : DecidablePred p
⊢ repl_in_F x ρ (dis (List.map (fun Fδ => if p Fδ then Formula.bottom else f Fδ) L)) =
    dis (List.map (fun Fδ => if p Fδ then Formula.bottom else repl_in_F x ρ (f Fδ)) L)
Tactic:
rw [repl_in_dis, listEq_to_disEq]
State after:
α : Type u_1
x : ℕ
ρ : Formula
L : List α
p : α → Prop
f : α → Formula
inst✝ : DecidablePred p
⊢ List.map (repl_in_F x ρ) (List.map (fun Fδ => if p Fδ then Formula.bottom else f Fδ) L) =
    List.map (fun Fδ => if p Fδ then Formula.bottom else repl_in_F x ρ (f Fδ)) L

State before:
α : Type u_1
x : ℕ
ρ : Formula
L : List α
p : α → Prop
f : α → Formula
inst✝ : DecidablePred p
⊢ List.map (repl_in_F x ρ) (List.map (fun Fδ => if p Fδ then Formula.bottom else f Fδ) L) =
    List.map (fun Fδ => if p Fδ then Formula.bottom else repl_in_F x ρ (f Fδ)) L
Tactic:
simp only [List.map_map]
State after:
α : Type u_1
x : ℕ
ρ : Formula
L : List α
p : α → Prop
f : α → Formula
inst✝ : DecidablePred p
⊢ List.map (repl_in_F x ρ ∘ fun Fδ => if p Fδ then Formula.bottom else f Fδ) L =
    List.map (fun Fδ => if p Fδ then Formula.bottom else repl_in_F x ρ (f Fδ)) L

State before:
α : Type u_1
x : ℕ
ρ : Formula
L : List α
p : α → Prop
f : α → Formula
inst✝ : DecidablePred p
⊢ List.map (repl_in_F x ρ ∘ fun Fδ => if p Fδ then Formula.bottom else f Fδ) L =
    List.map (fun Fδ => if p Fδ then Formula.bottom else repl_in_F x ρ (f Fδ)) L
Tactic:
aesop
State after:
no goals