Theorem: LeanSAT.Model.PropFun.eval_conj (LeanSAT/Model/PropFun.lean)

State before:
ν : Type u_1
τ : PropAssignment ν
φ₁ φ₂ : PropFun ν
⊢ eval τ (conj φ₁ φ₂) = (eval τ φ₁ && eval τ φ₂)
Tactic:
have ⟨φ₁, h₁⟩ := Quotient.exists_rep φ₁
State after:
ν : Type u_1
τ : PropAssignment ν
φ₁✝ φ₂ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
⊢ eval τ (conj φ₁✝ φ₂) = (eval τ φ₁✝ && eval τ φ₂)

State before:
ν : Type u_1
τ : PropAssignment ν
φ₁✝ φ₂ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
⊢ eval τ (conj φ₁✝ φ₂) = (eval τ φ₁✝ && eval τ φ₂)
Tactic:
have ⟨φ₂, h₂⟩ := Quotient.exists_rep φ₂
State after:
ν : Type u_1
τ : PropAssignment ν
φ₁✝ φ₂✝ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
φ₂ : PropForm ν
h₂ : ⟦φ₂⟧ = φ₂✝
⊢ eval τ (conj φ₁✝ φ₂✝) = (eval τ φ₁✝ && eval τ φ₂✝)

State before:
ν : Type u_1
τ : PropAssignment ν
φ₁✝ φ₂✝ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
φ₂ : PropForm ν
h₂ : ⟦φ₂⟧ = φ₂✝
⊢ eval τ (conj φ₁✝ φ₂✝) = (eval τ φ₁✝ && eval τ φ₂✝)
Tactic:
simp [← h₁, ← h₂, conj, eval]
State after:
no goals