Theorem: LO.Modal.Standard.Theory.Kripke.ValidOnFrame.morphism (Logic/Modal/Standard/Kripke/Morphism.lean)

State before:
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
⊢ F₁ ⊧* T → F₂ ⊧* T
Tactic:
simp only [Semantics.realizeSet_iff]
State after:
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
⊢ (∀ ⦃f : Formula α⦄, f ∈ T → F₁ ⊧ f) → ∀ ⦃f : Formula α⦄, f ∈ T → F₂ ⊧ f

State before:
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
⊢ (∀ ⦃f : Formula α⦄, f ∈ T → F₁ ⊧ f) → ∀ ⦃f : Formula α⦄, f ∈ T → F₂ ⊧ f
Tactic:
intro h p hp
State after:
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p✝ : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
h : ∀ ⦃f : Formula α⦄, f ∈ T → F₁ ⊧ f
p : Formula α
hp : p ∈ T
⊢ F₂ ⊧ p

State before:
α : Type u_1
M₁ M₂ : Model α
F₁ F₂ : Frame' α
f : F₁.World → F₂.World
p✝ : Formula α
T : Theory α
hSur : Function.Surjective f
hMorF : Frame.pMorphism F₁ F₂ f
h : ∀ ⦃f : Formula α⦄, f ∈ T → F₁ ⊧ f
p : Formula α
hp : p ∈ T
⊢ F₂ ⊧ p
Tactic:
exact Formula.Kripke.ValidOnFrame.morphism hSur hMorF (h hp)
State after:
no goals