Theorem: LO.FirstOrder.Semiformula.lMap_exItr (Logic/FirstOrder/Basic/Syntax/Formula.lean)

State before:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
k : ℕ
p : Semiformula L₁ ξ (n + k)
⊢ (lMap Φ) (∃^[k] p) = ∃^[k] (lMap Φ) p
Tactic:
induction k <;> simp [*, exItr_succ]
State after:
case succ
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
n✝ : ℕ
a✝ : ∀ (p : Semiformula L₁ ξ (n + n✝)), (lMap Φ) (∃^[n✝] p) = ∃^[n✝] (lMap Φ) p
p : Semiformula L₁ ξ (n + (n✝ + 1))
⊢ (lMap Φ) p = (lMap Φ) p

State before:
case succ
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
n✝ : ℕ
a✝ : ∀ (p : Semiformula L₁ ξ (n + n✝)), (lMap Φ) (∃^[n✝] p) = ∃^[n✝] (lMap Φ) p
p : Semiformula L₁ ξ (n + (n✝ + 1))
⊢ (lMap Φ) p = (lMap Φ) p
Tactic:
rfl
State after:
no goals