Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.morphism (Logic/Modal/Standard/Kripke/Morphism.lean)

State before:
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
w : M₁.World
⊢ w ⊧ p ↔ f w ⊧ p
Tactic:
induction p using Formula.rec' generalizing w with
| hatom p =>
  constructor;
  . apply hMor.atomic |>.mp;
  . apply hMor.atomic |>.mpr
| hbox p ih =>
  simp;
  constructor;
  . intro h w₂ hw₂;
    obtain ⟨w₁, ⟨hww₁, e⟩⟩ := hMor.back hw₂;
    have := ih.mp $ h w₁ hww₁;
    subst e;
    assumption;
  . intro h w' hww';
    exact ih.mpr $ h (f w') $ hMor.forth hww';
| _ => simp_all;
State after:
no goals

State before:
case hatom
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : α
w : M₁.World
⊢ w ⊧ atom p ↔ f w ⊧ atom p
Tactic:
constructor
State after:
case hatom.mp
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : α
w : M₁.World
⊢ w ⊧ atom p → f w ⊧ atom p

case hatom.mpr
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : α
w : M₁.World
⊢ f w ⊧ atom p → w ⊧ atom p

State before:
case hatom.mp
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : α
w : M₁.World
⊢ w ⊧ atom p → f w ⊧ atom p

case hatom.mpr
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : α
w : M₁.World
⊢ f w ⊧ atom p → w ⊧ atom p
Tactic:
. apply hMor.atomic |>.mp;
State after:
case hatom.mpr
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : α
w : M₁.World
⊢ f w ⊧ atom p → w ⊧ atom p

State before:
case hatom.mpr
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : α
w : M₁.World
⊢ f w ⊧ atom p → w ⊧ atom p
Tactic:
. apply hMor.atomic |>.mpr
State after:
no goals

State before:
case hatom.mp
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : α
w : M₁.World
⊢ w ⊧ atom p → f w ⊧ atom p
Tactic:
apply hMor.atomic |>.mp
State after:
no goals

State before:
case hatom.mpr
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : α
w : M₁.World
⊢ f w ⊧ atom p → w ⊧ atom p
Tactic:
apply hMor.atomic |>.mpr
State after:
no goals

State before:
case hbox
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
⊢ w ⊧ □p ↔ f w ⊧ □p
Tactic:
simp
State after:
case hbox
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
⊢ (∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p) ↔ ∀ (w' : M₂.Frame.World), f w ≺ w' → Satisfies M₂ w' p

State before:
case hbox
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
⊢ (∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p) ↔ ∀ (w' : M₂.Frame.World), f w ≺ w' → Satisfies M₂ w' p
Tactic:
constructor
State after:
case hbox.mp
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
⊢ (∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p) → ∀ (w' : M₂.Frame.World), f w ≺ w' → Satisfies M₂ w' p

case hbox.mpr
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
⊢ (∀ (w' : M₂.Frame.World), f w ≺ w' → Satisfies M₂ w' p) → ∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p

State before:
case hbox.mp
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
⊢ (∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p) → ∀ (w' : M₂.Frame.World), f w ≺ w' → Satisfies M₂ w' p

case hbox.mpr
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
⊢ (∀ (w' : M₂.Frame.World), f w ≺ w' → Satisfies M₂ w' p) → ∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p
Tactic:
. intro h w₂ hw₂;
  obtain ⟨w₁, ⟨hww₁, e⟩⟩ := hMor.back hw₂;
  have := ih.mp $ h w₁ hww₁;
  subst e;
  assumption;
State after:
case hbox.mpr
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
⊢ (∀ (w' : M₂.Frame.World), f w ≺ w' → Satisfies M₂ w' p) → ∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p

State before:
case hbox.mpr
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
⊢ (∀ (w' : M₂.Frame.World), f w ≺ w' → Satisfies M₂ w' p) → ∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p
Tactic:
. intro h w' hww';
  exact ih.mpr $ h (f w') $ hMor.forth hww';
State after:
no goals

State before:
case hbox.mp
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
⊢ (∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p) → ∀ (w' : M₂.Frame.World), f w ≺ w' → Satisfies M₂ w' p
Tactic:
intro h w₂ hw₂
State after:
case hbox.mp
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
h : ∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p
w₂ : M₂.Frame.World
hw₂ : f w ≺ w₂
⊢ Satisfies M₂ w₂ p

State before:
case hbox.mp
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
h : ∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p
w₂ : M₂.Frame.World
hw₂ : f w ≺ w₂
⊢ Satisfies M₂ w₂ p
Tactic:
obtain ⟨w₁, ⟨hww₁, e⟩⟩ := hMor.back hw₂
State after:
case hbox.mp.intro.intro
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
h : ∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p
w₂ : M₂.Frame.World
hw₂ : f w ≺ w₂
w₁ : M₁.Frame.World
hww₁ : w ≺ w₁
e : f w₁ = w₂
⊢ Satisfies M₂ w₂ p

State before:
case hbox.mp.intro.intro
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
h : ∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p
w₂ : M₂.Frame.World
hw₂ : f w ≺ w₂
w₁ : M₁.Frame.World
hww₁ : w ≺ w₁
e : f w₁ = w₂
⊢ Satisfies M₂ w₂ p
Tactic:
have := ih.mp $ h w₁ hww₁
State after:
case hbox.mp.intro.intro
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
h : ∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p
w₂ : M₂.Frame.World
hw₂ : f w ≺ w₂
w₁ : M₁.Frame.World
hww₁ : w ≺ w₁
e : f w₁ = w₂
this : f w₁ ⊧ p
⊢ Satisfies M₂ w₂ p

State before:
case hbox.mp.intro.intro
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
h : ∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p
w₂ : M₂.Frame.World
hw₂ : f w ≺ w₂
w₁ : M₁.Frame.World
hww₁ : w ≺ w₁
e : f w₁ = w₂
this : f w₁ ⊧ p
⊢ Satisfies M₂ w₂ p
Tactic:
subst e
State after:
case hbox.mp.intro.intro
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
h : ∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p
w₁ : M₁.Frame.World
hww₁ : w ≺ w₁
this : f w₁ ⊧ p
hw₂ : f w ≺ f w₁
⊢ Satisfies M₂ (f w₁) p

State before:
case hbox.mp.intro.intro
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
h : ∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p
w₁ : M₁.Frame.World
hww₁ : w ≺ w₁
this : f w₁ ⊧ p
hw₂ : f w ≺ f w₁
⊢ Satisfies M₂ (f w₁) p
Tactic:
assumption
State after:
no goals

State before:
case hbox.mpr
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
⊢ (∀ (w' : M₂.Frame.World), f w ≺ w' → Satisfies M₂ w' p) → ∀ (w' : M₁.Frame.World), w ≺ w' → Satisfies M₁ w' p
Tactic:
intro h w' hww'
State after:
case hbox.mpr
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
h : ∀ (w' : M₂.Frame.World), f w ≺ w' → Satisfies M₂ w' p
w' : M₁.Frame.World
hww' : w ≺ w'
⊢ Satisfies M₁ w' p

State before:
case hbox.mpr
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p✝ : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p : Formula α
ih : ∀ {w : M₁.World}, w ⊧ p ↔ f w ⊧ p
w : M₁.World
h : ∀ (w' : M₂.Frame.World), f w ≺ w' → Satisfies M₂ w' p
w' : M₁.Frame.World
hww' : w ≺ w'
⊢ Satisfies M₁ w' p
Tactic:
exact ih.mpr $ h (f w') $ hMor.forth hww'
State after:
no goals

State before:
case hor
α : Type u_1
M₁ M₂ : Model α
F₁ : Frame' α
F₂ : Frame' α
f : M₁.World → M₂.World
p : Formula α
T : Theory α
hMor : M₁.pMorphism M₂ f
p✝ q✝ : Formula α
a✝¹ : ∀ {w : M₁.World}, w ⊧ p✝ ↔ f w ⊧ p✝
a✝ : ∀ {w : M₁.World}, w ⊧ q✝ ↔ f w ⊧ q✝
w : M₁.World
⊢ w ⊧ p✝ ⋎ q✝ ↔ f w ⊧ p✝ ⋎ q✝
Tactic:
simp_all
State after:
no goals