Theorem: LeanSAT.Model.PropForm.satisfies_map (LeanSAT/Model/Subst.lean)

State before:
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ φ : PropForm ν₁
f : ν₁ → ν₂
τ : PropAssignment ν₂
⊢ τ ⊨ map f φ ↔ PropAssignment.map f τ ⊨ φ
Tactic:
induction φ <;> (simp [map, PropAssignment.map] at *) <;> (simp [*])
State after:
no goals

State before:
case biImpl
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ φ₁ φ₂ : PropForm ν₁
f : ν₁ → ν₂
τ : PropAssignment ν₂
φ₁✝ φ₂✝ : PropForm ν₁
φ₁_ih✝ : τ ⊨ map f φ₁✝ ↔ PropAssignment.map f τ ⊨ φ₁✝
φ₂_ih✝ : τ ⊨ map f φ₂✝ ↔ PropAssignment.map f τ ⊨ φ₂✝
⊢ τ ⊨ map f (biImpl φ₁✝ φ₂✝) ↔ PropAssignment.map f τ ⊨ biImpl φ₁✝ φ₂✝
Tactic:
simp [map, PropAssignment.map] at *
State after:
case biImpl
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ φ₁ φ₂ : PropForm ν₁
f : ν₁ → ν₂
τ : PropAssignment ν₂
φ₁✝ φ₂✝ : PropForm ν₁
φ₁_ih✝ : τ ⊨ map f φ₁✝ ↔ τ ∘ f ⊨ φ₁✝
φ₂_ih✝ : τ ⊨ map f φ₂✝ ↔ τ ∘ f ⊨ φ₂✝
⊢ (τ ⊨ map f φ₁✝ ↔ τ ⊨ map f φ₂✝) ↔ (τ ∘ f ⊨ φ₁✝ ↔ τ ∘ f ⊨ φ₂✝)

State before:
case biImpl
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ φ₁ φ₂ : PropForm ν₁
f : ν₁ → ν₂
τ : PropAssignment ν₂
φ₁✝ φ₂✝ : PropForm ν₁
φ₁_ih✝ : τ ⊨ map f φ₁✝ ↔ τ ∘ f ⊨ φ₁✝
φ₂_ih✝ : τ ⊨ map f φ₂✝ ↔ τ ∘ f ⊨ φ₂✝
⊢ (τ ⊨ map f φ₁✝ ↔ τ ⊨ map f φ₂✝) ↔ (τ ∘ f ⊨ φ₁✝ ↔ τ ∘ f ⊨ φ₂✝)
Tactic:
simp [*]
State after:
no goals