Theorem: LO.FirstOrder.Derivation.shifts_image (Logic/FirstOrder/Basic/Calculus.lean)

State before:
L : Language
Δ✝ Δ₁✝ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
L₁ : Language
L₂ : Language
Δ₁ Γ₁ : Finset (SyntacticFormula L₁)
Φ : L₁ →ᵥ L₂
Δ : List (SyntacticFormula L₁)
⊢ (List.map (⇑(lMap Φ)) Δ)⁺ = List.map (⇑(lMap Φ)) Δ⁺
Tactic:
simp[shifts, shiftEmb, Finset.map_eq_image, Finset.image_image, Function.comp, Semiformula.lMap_shift]
State after:
no goals