Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ClassicalSatisfies.imp_def (Logic/Propositional/Superintuitionistic/Kripke/Classical.lean)

State before:
α : Type u_1
inst✝ : Inhabited α
V : ClassicalValuation α
p q : Formula α
⊢ V ⊧ p ⟶ q ↔ V ⊧ p → V ⊧ q
Tactic:
simp
State after:
α : Type u_1
inst✝ : Inhabited α
V : ClassicalValuation α
p q : Formula α
⊢ (∀ {w' : PUnit.{u_1 + 1}}, Satisfies (ClassicalModel V) w' p → Satisfies (ClassicalModel V) w' q) ↔
    Satisfies (ClassicalModel V) PUnit.unit p → Satisfies (ClassicalModel V) PUnit.unit q

State before:
α : Type u_1
inst✝ : Inhabited α
V : ClassicalValuation α
p q : Formula α
⊢ (∀ {w' : PUnit.{u_1 + 1}}, Satisfies (ClassicalModel V) w' p → Satisfies (ClassicalModel V) w' q) ↔
    Satisfies (ClassicalModel V) PUnit.unit p → Satisfies (ClassicalModel V) PUnit.unit q
Tactic:
tauto
State after:
no goals