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

State before:
ν : Type u_1
φ₁ φ₂ : PropFun ν
⊢ φ₁ ⊔ φ₂ ≠ ⊤ → φ₁ ≠ ⊤
Tactic:
intro h
State after:
ν : Type u_1
φ₁ φ₂ : PropFun ν
h : φ₁ ⊔ φ₂ ≠ ⊤
⊢ φ₁ ≠ ⊤

State before:
ν : Type u_1
φ₁ φ₂ : PropFun ν
h : φ₁ ⊔ φ₂ ≠ ⊤
⊢ φ₁ ≠ ⊤
Tactic:
aesop
State after:
no goals