Theorem: LeanSAT.Model.PropFun.semVars_map (LeanSAT/Model/Subst.lean)

State before:
ν₁ : Type u_1
ν₂ : Type u_2
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
φ : PropFun ν₁
hf : Function.Injective f
⊢ semVars (map f φ) = Finset.map { toFun := f, inj' := hf } (semVars φ)
Tactic:
let ⟨ϕ,hϕ⟩ := φ.toTrunc.out
State after:
ν₁ : Type u_1
ν₂ : Type u_2
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
φ : PropFun ν₁
hf : Function.Injective f
ϕ : PropForm ν₁
hϕ : ⟦ϕ⟧ = φ
⊢ semVars (map f φ) = Finset.map { toFun := f, inj' := hf } (semVars φ)

State before:
ν₁ : Type u_1
ν₂ : Type u_2
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
φ : PropFun ν₁
hf : Function.Injective f
ϕ : PropForm ν₁
hϕ : ⟦ϕ⟧ = φ
⊢ semVars (map f φ) = Finset.map { toFun := f, inj' := hf } (semVars φ)
Tactic:
cases hϕ
State after:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
ϕ : PropForm ν₁
⊢ semVars (map f ⟦ϕ⟧) = Finset.map { toFun := f, inj' := hf } (semVars ⟦ϕ⟧)

State before:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
ϕ : PropForm ν₁
⊢ semVars (map f ⟦ϕ⟧) = Finset.map { toFun := f, inj' := hf } (semVars ⟦ϕ⟧)
Tactic:
simp [map, *, PropForm.semVars_map]
State after:
no goals