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

State before:
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
⊢ 𝔽(Ax(𝐂𝐥)) ⊧ p → ∀ (V : ClassicalValuation α), V ⊧ p
Tactic:
intro h V
State after:
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
h : 𝔽(Ax(𝐂𝐥)) ⊧ p
V : ClassicalValuation α
⊢ V ⊧ p

State before:
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
h : 𝔽(Ax(𝐂𝐥)) ⊧ p
V : ClassicalValuation α
⊢ V ⊧ p
Tactic:
apply Formula.Kripke.ValidOnModel.classical_iff.mp
State after:
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
h : 𝔽(Ax(𝐂𝐥)) ⊧ p
V : ClassicalValuation α
⊢ ClassicalModel V ⊧ p

State before:
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
h : 𝔽(Ax(𝐂𝐥)) ⊧ p
V : ClassicalValuation α
⊢ ClassicalModel V ⊧ p
Tactic:
exact h (by
  apply iff_definability_memAxiomSetFrameClass instClassicalDefinabilityExtensive |>.mpr;
  simp [Extensive];
) (ClassicalModel V).Valuation (ClassicalModel V).hereditary
State after:
no goals

State before:
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
h : 𝔽(Ax(𝐂𝐥)) ⊧ p
V : ClassicalValuation α
⊢ (ClassicalModel V).Frame ∈ 𝔽(Ax(𝐂𝐥))
Tactic:
apply iff_definability_memAxiomSetFrameClass instClassicalDefinabilityExtensive |>.mpr
State after:
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
h : 𝔽(Ax(𝐂𝐥)) ⊧ p
V : ClassicalValuation α
⊢ Extensive (ClassicalModel V).Frame.Rel

State before:
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
h : 𝔽(Ax(𝐂𝐥)) ⊧ p
V : ClassicalValuation α
⊢ Extensive (ClassicalModel V).Frame.Rel
Tactic:
simp [Extensive]
State after:
no goals