Theorem: LO.Modal.Standard.Formula.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₁ ⊧ p → F₂ ⊧ p
Tactic:
contrapose
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₂ ⊧ p → ¬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
⊢ ¬F₂ ⊧ p → ¬F₁ ⊧ p
Tactic:
intro h
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₂ ⊧ p
⊢ ¬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₂ ⊧ p
⊢ ¬F₁ ⊧ p
Tactic:
obtain ⟨V₂, w₂, h⟩ := by simpa [ValidOnFrame, ValidOnModel] using h;
State after:
case intro.intro
α : 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₂ ⊧ p
V₂ : Valuation F₂.World α
w₂ : { Frame := F₂, Valuation := V₂ }.World
h : ¬Satisfies { Frame := F₂, Valuation := V₂ } w₂ p
⊢ ¬F₁ ⊧ p

State before:
case intro.intro
α : 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₂ ⊧ p
V₂ : Valuation F₂.World α
w₂ : { Frame := F₂, Valuation := V₂ }.World
h : ¬Satisfies { Frame := F₂, Valuation := V₂ } w₂ p
⊢ ¬F₁ ⊧ p
Tactic:
simp [ValidOnFrame, ValidOnModel]
State after:
case intro.intro
α : 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₂ ⊧ p
V₂ : Valuation F₂.World α
w₂ : { Frame := F₂, Valuation := V₂ }.World
h : ¬Satisfies { Frame := F₂, Valuation := V₂ } w₂ p
⊢ ∃ x x_1, ¬Satisfies { Frame := F₁, Valuation := x } x_1 p

State before:
case intro.intro
α : 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₂ ⊧ p
V₂ : Valuation F₂.World α
w₂ : { Frame := F₂, Valuation := V₂ }.World
h : ¬Satisfies { Frame := F₂, Valuation := V₂ } w₂ p
⊢ ∃ x x_1, ¬Satisfies { Frame := F₁, Valuation := x } x_1 p
Tactic:
obtain ⟨w₁, e⟩ : ∃ w₁, f w₁ = w₂ := by apply hSur;
State after:
case intro.intro.intro
α : 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₂ ⊧ p
V₂ : Valuation F₂.World α
w₂ : { Frame := F₂, Valuation := V₂ }.World
h : ¬Satisfies { Frame := F₂, Valuation := V₂ } w₂ p
w₁ : F₁.World
e : f w₁ = w₂
⊢ ∃ x x_1, ¬Satisfies { Frame := F₁, Valuation := x } x_1 p

State before:
case intro.intro.intro
α : 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₂ ⊧ p
V₂ : Valuation F₂.World α
w₂ : { Frame := F₂, Valuation := V₂ }.World
h : ¬Satisfies { Frame := F₂, Valuation := V₂ } w₂ p
w₁ : F₁.World
e : f w₁ = w₂
⊢ ∃ x x_1, ¬Satisfies { Frame := F₁, Valuation := x } x_1 p
Tactic:
existsi λ w a => V₂ (f w) a, w₁
State after:
case intro.intro.intro
α : 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₂ ⊧ p
V₂ : Valuation F₂.World α
w₂ : { Frame := F₂, Valuation := V₂ }.World
h : ¬Satisfies { Frame := F₂, Valuation := V₂ } w₂ p
w₁ : F₁.World
e : f w₁ = w₂
⊢ ¬Satisfies { Frame := F₁, Valuation := fun w a => V₂ (f w) a } w₁ p

State before:
case intro.intro.intro
α : 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₂ ⊧ p
V₂ : Valuation F₂.World α
w₂ : { Frame := F₂, Valuation := V₂ }.World
h : ¬Satisfies { Frame := F₂, Valuation := V₂ } w₂ p
w₁ : F₁.World
e : f w₁ = w₂
⊢ ¬Satisfies { Frame := F₁, Valuation := fun w a => V₂ (f w) a } w₁ p
Tactic:
subst e
State after:
case intro.intro.intro
α : 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₂ ⊧ p
V₂ : Valuation F₂.World α
w₁ : F₁.World
h : ¬Satisfies { Frame := F₂, Valuation := V₂ } (f w₁) p
⊢ ¬Satisfies { Frame := F₁, Valuation := fun w a => V₂ (f w) a } w₁ p

State before:
case intro.intro.intro
α : 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₂ ⊧ p
V₂ : Valuation F₂.World α
w₁ : F₁.World
h : ¬Satisfies { Frame := F₂, Valuation := V₂ } (f w₁) p
⊢ ¬Satisfies { Frame := F₁, Valuation := fun w a => V₂ (f w) a } w₁ p
Tactic:
exact Satisfies.morphism ({
  forth := by intro w v hwv; apply hMorF.forth hwv,
  back := by intro w v h; apply hMorF.back h,
  atomic := by simp_all;
}) |>.not.mpr h
State after:
no goals

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₂ ⊧ p
⊢ ?m.13927
Tactic:
simpa [ValidOnFrame, ValidOnModel] using h
State after:
no goals

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₂ ⊧ p
V₂ : Valuation F₂.World α
w₂ : { Frame := F₂, Valuation := V₂ }.World
h : ¬Satisfies { Frame := F₂, Valuation := V₂ } w₂ p
⊢ ∃ w₁, f w₁ = w₂
Tactic:
apply hSur
State after:
no goals

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₂ ⊧ p
V₂ : Valuation F₂.World α
w₁ : F₁.World
h : ¬Satisfies { Frame := F₂, Valuation := V₂ } (f w₁) p
⊢ ∀ {w v : { Frame := F₁, Valuation := fun w a => V₂ (f w) a }.Frame.World}, w ≺ v → f w ≺ f v
Tactic:
intro w v hwv
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₂ ⊧ p
V₂ : Valuation F₂.World α
w₁ : F₁.World
h : ¬Satisfies { Frame := F₂, Valuation := V₂ } (f w₁) p
w v : { Frame := F₁, Valuation := fun w a => V₂ (f w) a }.Frame.World
hwv : w ≺ v
⊢ f w ≺ f v

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₂ ⊧ p
V₂ : Valuation F₂.World α
w₁ : F₁.World
h : ¬Satisfies { Frame := F₂, Valuation := V₂ } (f w₁) p
w v : { Frame := F₁, Valuation := fun w a => V₂ (f w) a }.Frame.World
hwv : w ≺ v
⊢ f w ≺ f v
Tactic:
apply hMorF.forth hwv
State after:
no goals

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₂ ⊧ p
V₂ : Valuation F₂.World α
w₁ : F₁.World
h : ¬Satisfies { Frame := F₂, Valuation := V₂ } (f w₁) p
⊢ ∀ {w : { Frame := F₁, Valuation := fun w a => V₂ (f w) a }.Frame.World}
    {v : { Frame := F₂, Valuation := V₂ }.Frame.World}, f w ≺ v → ∃ u, w ≺ u ∧ f u = v
Tactic:
intro w v h
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₂ ⊧ p
V₂ : Valuation F₂.World α
w₁ : F₁.World
h✝ : ¬Satisfies { Frame := F₂, Valuation := V₂ } (f w₁) p
w : { Frame := F₁, Valuation := fun w a => V₂ (f w) a }.Frame.World
v : { Frame := F₂, Valuation := V₂ }.Frame.World
h : f w ≺ v
⊢ ∃ u, w ≺ u ∧ f u = v

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₂ ⊧ p
V₂ : Valuation F₂.World α
w₁ : F₁.World
h✝ : ¬Satisfies { Frame := F₂, Valuation := V₂ } (f w₁) p
w : { Frame := F₁, Valuation := fun w a => V₂ (f w) a }.Frame.World
v : { Frame := F₂, Valuation := V₂ }.Frame.World
h : f w ≺ v
⊢ ∃ u, w ≺ u ∧ f u = v
Tactic:
apply hMorF.back h
State after:
no goals

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₂ ⊧ p
V₂ : Valuation F₂.World α
w₁ : F₁.World
h : ¬Satisfies { Frame := F₂, Valuation := V₂ } (f w₁) p
⊢ ∀ {w : { Frame := F₁, Valuation := fun w a => V₂ (f w) a }.World} {a : α},
    { Frame := F₁, Valuation := fun w a => V₂ (f w) a }.Valuation w a ↔
      { Frame := F₂, Valuation := V₂ }.Valuation (f w) a
Tactic:
simp_all
State after:
no goals