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

State before:
ν : Type u_1
φ₁ φ₂ : PropFun ν
⊢ φ₁ = φ₂ᶜ → φ₁ ≠ φ₂
Tactic:
rintro rfl h
State after:
ν : Type u_1
φ₂ : PropFun ν
h : φ₂ᶜ = φ₂
⊢ False

State before:
ν : Type u_1
φ₂ : PropFun ν
h : φ₂ᶜ = φ₂
⊢ False
Tactic:
rw [ext_iff] at h
State after:
ν : Type u_1
φ₂ : PropFun ν
h : ∀ (τ : PropAssignment ν), τ ⊨ φ₂ᶜ ↔ τ ⊨ φ₂
⊢ False

State before:
ν : Type u_1
φ₂ : PropFun ν
h : ∀ (τ : PropAssignment ν), τ ⊨ φ₂ᶜ ↔ τ ⊨ φ₂
⊢ False
Tactic:
simp at h
State after:
no goals