Theorem: LO.FirstOrder.Semiformula.fvarList_lMap (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₂
p : Semiformula L₁ ξ n
⊢ ((lMap Φ) p).fvarList = p.fvarList
Tactic:
induction p using Semiformula.rec' <;> try simp [lMap_rel, lMap_nrel, *]
State after:
case hrel
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✝ k✝ : ℕ
r✝ : L₁.Rel k✝
v✝ : Fin k✝ → Semiterm L₁ ξ n✝
⊢ (rel (Φ.rel r✝) fun i => Semiterm.lMap Φ (v✝ i)).fvarList = (rel r✝ v✝).fvarList

case hnrel
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✝ k✝ : ℕ
r✝ : L₁.Rel k✝
v✝ : Fin k✝ → Semiterm L₁ ξ n✝
⊢ (nrel (Φ.rel r✝) fun i => Semiterm.lMap Φ (v✝ i)).fvarList = (nrel r✝ v✝).fvarList

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₂
n k : ℕ
r : L₁.Rel k
v : Fin k → Semiterm L₁ ξ n
⊢ (rel (Φ.rel r) fun i => Semiterm.lMap Φ (v i)).fvarList = (rel r v).fvarList
Tactic:
case hrel n k r v => simp [fvarList]
State after:
no goals

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₂
n k : ℕ
r : L₁.Rel k
v : Fin k → Semiterm L₁ ξ n
⊢ (nrel (Φ.rel r) fun i => Semiterm.lMap Φ (v i)).fvarList = (nrel r v).fvarList
Tactic:
case hnrel n k r v => simp [fvarList]
State after:
no goals

State before:
case hex
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✝ : ℕ
p✝ : Semiformula L₁ ξ (n✝ + 1)
a✝ : ((lMap Φ) p✝).fvarList = p✝.fvarList
⊢ ((lMap Φ) (∃' p✝)).fvarList = (∃' p✝).fvarList
Tactic:
simp [lMap_rel, lMap_nrel, *]
State after:
no goals

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₂
n k : ℕ
r : L₁.Rel k
v : Fin k → Semiterm L₁ ξ n
⊢ (rel (Φ.rel r) fun i => Semiterm.lMap Φ (v i)).fvarList = (rel r v).fvarList
Tactic:
simp [fvarList]
State after:
no goals

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₂
n k : ℕ
r : L₁.Rel k
v : Fin k → Semiterm L₁ ξ n
⊢ (nrel (Φ.rel r) fun i => Semiterm.lMap Φ (v i)).fvarList = (nrel r v).fvarList
Tactic:
simp [fvarList]
State after:
no goals