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

State before:
L : Language
Δ✝ Δ₁✝ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
L₁ : Language
L₂ : Language
Δ₁ Γ₁ : Finset (SyntacticFormula L₁)
C : Set (SyntacticFormula L₂)
Δ : Sequent L₁
Φ : L₁ →ᵥ L₂
d :  ⊢¹ Δ
⊢ CutRestricted C (Derivation.lMap Φ d) ↔ CutRestricted (⇑(Semiformula.lMap Φ) ⁻¹' C) d
Tactic:
induction d <;> simp[Derivation.lMap, *]
State after:
no goals