Theorem: forms_to_sets (Bml/Semantics.lean)

State before:
φ ψ : Formula
⊢ φ⊨ψ → {φ}⊨{ψ}
Tactic:
intro impTaut
State after:
φ ψ : Formula
impTaut : φ⊨ψ
⊢ {φ}⊨{ψ}

State before:
φ ψ : Formula
impTaut : φ⊨ψ
⊢ {φ}⊨{ψ}
Tactic:
intro W M w lhs ψ1 psi1_in_setpsi
State after:
φ ψ : Formula
impTaut : φ⊨ψ
W : Type
M : KripkeModel W
w : W
lhs : ∀ φ_1 ∈ {φ}, Evaluate (M, w) φ_1
ψ1 : Formula
psi1_in_setpsi : ψ1 ∈ {ψ}
⊢ Evaluate (M, w) ψ1

State before:
φ ψ : Formula
impTaut : φ⊨ψ
W : Type
M : KripkeModel W
w : W
lhs : ∀ φ_1 ∈ {φ}, Evaluate (M, w) φ_1
ψ1 : Formula
psi1_in_setpsi : ψ1 ∈ {ψ}
⊢ Evaluate (M, w) ψ1
Tactic:
specialize impTaut W M w
State after:
φ ψ : Formula
W : Type
M : KripkeModel W
w : W
lhs : ∀ φ_1 ∈ {φ}, Evaluate (M, w) φ_1
ψ1 : Formula
psi1_in_setpsi : ψ1 ∈ {ψ}
impTaut : (∀ φ_1 ∈ {φ}, Evaluate (M, w) φ_1) → ∀ ψ_1 ∈ {ψ}, Evaluate (M, w) ψ_1
⊢ Evaluate (M, w) ψ1

State before:
φ ψ : Formula
W : Type
M : KripkeModel W
w : W
lhs : ∀ φ_1 ∈ {φ}, Evaluate (M, w) φ_1
ψ1 : Formula
psi1_in_setpsi : ψ1 ∈ {ψ}
impTaut : (∀ φ_1 ∈ {φ}, Evaluate (M, w) φ_1) → ∀ ψ_1 ∈ {ψ}, Evaluate (M, w) ψ_1
⊢ Evaluate (M, w) ψ1
Tactic:
simp at *
State after:
φ ψ : Formula
W : Type
M : KripkeModel W
w : W
ψ1 : Formula
lhs : Evaluate (M, w) φ
psi1_in_setpsi : ψ1 = ψ
impTaut : Evaluate (M, w) φ → Evaluate (M, w) ψ
⊢ Evaluate (M, w) ψ1

State before:
φ ψ : Formula
W : Type
M : KripkeModel W
w : W
ψ1 : Formula
lhs : Evaluate (M, w) φ
psi1_in_setpsi : ψ1 = ψ
impTaut : Evaluate (M, w) φ → Evaluate (M, w) ψ
⊢ Evaluate (M, w) ψ1
Tactic:
subst psi1_in_setpsi
State after:
φ : Formula
W : Type
M : KripkeModel W
w : W
ψ1 : Formula
lhs : Evaluate (M, w) φ
impTaut : Evaluate (M, w) φ → Evaluate (M, w) ψ1
⊢ Evaluate (M, w) ψ1

State before:
φ : Formula
W : Type
M : KripkeModel W
w : W
ψ1 : Formula
lhs : Evaluate (M, w) φ
impTaut : Evaluate (M, w) φ → Evaluate (M, w) ψ1
⊢ Evaluate (M, w) ψ1
Tactic:
apply impTaut
State after:
φ : Formula
W : Type
M : KripkeModel W
w : W
ψ1 : Formula
lhs : Evaluate (M, w) φ
impTaut : Evaluate (M, w) φ → Evaluate (M, w) ψ1
⊢ Evaluate (M, w) φ

State before:
φ : Formula
W : Type
M : KripkeModel W
w : W
ψ1 : Formula
lhs : Evaluate (M, w) φ
impTaut : Evaluate (M, w) φ → Evaluate (M, w) ψ1
⊢ Evaluate (M, w) φ
Tactic:
exact lhs
State after:
no goals