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

State before:
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → ν₂
φ φ₁ φ₂ : PropFun ν₁
⊢ map f (φ₁ ⊔ φ₂) = map f φ₁ ⊔ map f φ₂
Tactic:
ext
State after:
case a
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → ν₂
φ φ₁ φ₂ : PropFun ν₁
τ✝ : PropAssignment ν₂
⊢ τ✝ ⊨ map f (φ₁ ⊔ φ₂) ↔ τ✝ ⊨ map f φ₁ ⊔ map f φ₂

State before:
case a
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → ν₂
φ φ₁ φ₂ : PropFun ν₁
τ✝ : PropAssignment ν₂
⊢ τ✝ ⊨ map f (φ₁ ⊔ φ₂) ↔ τ✝ ⊨ map f φ₁ ⊔ map f φ₂
Tactic:
simp
State after:
no goals