Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multidia_def (Logic/Modal/Standard/Kripke/Semantics.lean)

State before:
α : Type u_1
M : Model α
w : M.World
p q : Formula α
n : ℕ
⊢ Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
Tactic:
induction n generalizing w with
| zero => simp;
| succ n ih =>
  constructor;
  . intro h;
    obtain ⟨v, hwv, hv⟩ := by simpa using h;
    obtain ⟨x, hvx, hx⟩ := ih.mp hv;
    existsi x;
    constructor;
    . existsi v; simp_all;
    . simpa;
  . simp;
    intro x y hwy hyx hx;
    existsi y;
    constructor;
    . simpa;
    . apply ih.mpr;
      existsi x;
      simp_all;
State after:
no goals

State before:
case zero
α : Type u_1
M : Model α
p q : Formula α
w : M.World
⊢ Satisfies M w (◇^[0]p) ↔ ∃ v, w ≺^[0] v ∧ Satisfies M v p
Tactic:
simp
State after:
no goals

State before:
case succ
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
⊢ Satisfies M w (◇^[(n + 1)]p) ↔ ∃ v, w ≺^[n + 1] v ∧ Satisfies M v p
Tactic:
constructor
State after:
case succ.mp
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
⊢ Satisfies M w (◇^[(n + 1)]p) → ∃ v, w ≺^[n + 1] v ∧ Satisfies M v p

case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
⊢ (∃ v, w ≺^[n + 1] v ∧ Satisfies M v p) → Satisfies M w (◇^[(n + 1)]p)

State before:
case succ.mp
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
⊢ Satisfies M w (◇^[(n + 1)]p) → ∃ v, w ≺^[n + 1] v ∧ Satisfies M v p

case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
⊢ (∃ v, w ≺^[n + 1] v ∧ Satisfies M v p) → Satisfies M w (◇^[(n + 1)]p)
Tactic:
. intro h;
  obtain ⟨v, hwv, hv⟩ := by simpa using h;
  obtain ⟨x, hvx, hx⟩ := ih.mp hv;
  existsi x;
  constructor;
  . existsi v; simp_all;
  . simpa;
State after:
case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
⊢ (∃ v, w ≺^[n + 1] v ∧ Satisfies M v p) → Satisfies M w (◇^[(n + 1)]p)

State before:
case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
⊢ (∃ v, w ≺^[n + 1] v ∧ Satisfies M v p) → Satisfies M w (◇^[(n + 1)]p)
Tactic:
. simp;
  intro x y hwy hyx hx;
  existsi y;
  constructor;
  . simpa;
  . apply ih.mpr;
    existsi x;
    simp_all;
State after:
no goals

State before:
case succ.mp
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
⊢ Satisfies M w (◇^[(n + 1)]p) → ∃ v, w ≺^[n + 1] v ∧ Satisfies M v p
Tactic:
intro h
State after:
case succ.mp
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
⊢ ∃ v, w ≺^[n + 1] v ∧ Satisfies M v p

State before:
case succ.mp
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
⊢ ∃ v, w ≺^[n + 1] v ∧ Satisfies M v p
Tactic:
obtain ⟨v, hwv, hv⟩ := by simpa using h;
State after:
case succ.mp.intro.intro
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
v : M.Frame.World
hwv : w ≺ v
hv : Satisfies M v ((UnaryModalOperator.mop false)^[n] p)
⊢ ∃ v, w ≺^[n + 1] v ∧ Satisfies M v p

State before:
case succ.mp.intro.intro
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
v : M.Frame.World
hwv : w ≺ v
hv : Satisfies M v ((UnaryModalOperator.mop false)^[n] p)
⊢ ∃ v, w ≺^[n + 1] v ∧ Satisfies M v p
Tactic:
obtain ⟨x, hvx, hx⟩ := ih.mp hv
State after:
case succ.mp.intro.intro.intro.intro
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
v : M.Frame.World
hwv : w ≺ v
hv : Satisfies M v ((UnaryModalOperator.mop false)^[n] p)
x : M.Frame.World
hvx : v ≺^[n] x
hx : Satisfies M x p
⊢ ∃ v, w ≺^[n + 1] v ∧ Satisfies M v p

State before:
case succ.mp.intro.intro.intro.intro
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
v : M.Frame.World
hwv : w ≺ v
hv : Satisfies M v ((UnaryModalOperator.mop false)^[n] p)
x : M.Frame.World
hvx : v ≺^[n] x
hx : Satisfies M x p
⊢ ∃ v, w ≺^[n + 1] v ∧ Satisfies M v p
Tactic:
existsi x
State after:
case succ.mp.intro.intro.intro.intro
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
v : M.Frame.World
hwv : w ≺ v
hv : Satisfies M v ((UnaryModalOperator.mop false)^[n] p)
x : M.Frame.World
hvx : v ≺^[n] x
hx : Satisfies M x p
⊢ w ≺^[n + 1] x ∧ Satisfies M x p

State before:
case succ.mp.intro.intro.intro.intro
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
v : M.Frame.World
hwv : w ≺ v
hv : Satisfies M v ((UnaryModalOperator.mop false)^[n] p)
x : M.Frame.World
hvx : v ≺^[n] x
hx : Satisfies M x p
⊢ w ≺^[n + 1] x ∧ Satisfies M x p
Tactic:
constructor
State after:
case succ.mp.intro.intro.intro.intro.left
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
v : M.Frame.World
hwv : w ≺ v
hv : Satisfies M v ((UnaryModalOperator.mop false)^[n] p)
x : M.Frame.World
hvx : v ≺^[n] x
hx : Satisfies M x p
⊢ w ≺^[n + 1] x

case succ.mp.intro.intro.intro.intro.right
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
v : M.Frame.World
hwv : w ≺ v
hv : Satisfies M v ((UnaryModalOperator.mop false)^[n] p)
x : M.Frame.World
hvx : v ≺^[n] x
hx : Satisfies M x p
⊢ Satisfies M x p

State before:
case succ.mp.intro.intro.intro.intro.left
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
v : M.Frame.World
hwv : w ≺ v
hv : Satisfies M v ((UnaryModalOperator.mop false)^[n] p)
x : M.Frame.World
hvx : v ≺^[n] x
hx : Satisfies M x p
⊢ w ≺^[n + 1] x

case succ.mp.intro.intro.intro.intro.right
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
v : M.Frame.World
hwv : w ≺ v
hv : Satisfies M v ((UnaryModalOperator.mop false)^[n] p)
x : M.Frame.World
hvx : v ≺^[n] x
hx : Satisfies M x p
⊢ Satisfies M x p
Tactic:
. existsi v; simp_all;
State after:
case succ.mp.intro.intro.intro.intro.right
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
v : M.Frame.World
hwv : w ≺ v
hv : Satisfies M v ((UnaryModalOperator.mop false)^[n] p)
x : M.Frame.World
hvx : v ≺^[n] x
hx : Satisfies M x p
⊢ Satisfies M x p

State before:
case succ.mp.intro.intro.intro.intro.right
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
v : M.Frame.World
hwv : w ≺ v
hv : Satisfies M v ((UnaryModalOperator.mop false)^[n] p)
x : M.Frame.World
hvx : v ≺^[n] x
hx : Satisfies M x p
⊢ Satisfies M x p
Tactic:
. simpa;
State after:
no goals

State before:
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
⊢ ?m.54398
Tactic:
simpa using h
State after:
no goals

State before:
case succ.mp.intro.intro.intro.intro.left
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
v : M.Frame.World
hwv : w ≺ v
hv : Satisfies M v ((UnaryModalOperator.mop false)^[n] p)
x : M.Frame.World
hvx : v ≺^[n] x
hx : Satisfies M x p
⊢ w ≺^[n + 1] x
Tactic:
existsi v
State after:
case succ.mp.intro.intro.intro.intro.left
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
v : M.Frame.World
hwv : w ≺ v
hv : Satisfies M v ((UnaryModalOperator.mop false)^[n] p)
x : M.Frame.World
hvx : v ≺^[n] x
hx : Satisfies M x p
⊢ (fun x x_1 => x ≺ x_1) w v ∧ RelItr (fun x x_1 => x ≺ x_1) n v x

State before:
case succ.mp.intro.intro.intro.intro.left
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
v : M.Frame.World
hwv : w ≺ v
hv : Satisfies M v ((UnaryModalOperator.mop false)^[n] p)
x : M.Frame.World
hvx : v ≺^[n] x
hx : Satisfies M x p
⊢ (fun x x_1 => x ≺ x_1) w v ∧ RelItr (fun x x_1 => x ≺ x_1) n v x
Tactic:
simp_all
State after:
no goals

State before:
case succ.mp.intro.intro.intro.intro.right
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
v : M.Frame.World
hwv : w ≺ v
hv : Satisfies M v ((UnaryModalOperator.mop false)^[n] p)
x : M.Frame.World
hvx : v ≺^[n] x
hx : Satisfies M x p
⊢ Satisfies M x p
Tactic:
simpa
State after:
no goals

State before:
case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
⊢ (∃ v, w ≺^[n + 1] v ∧ Satisfies M v p) → Satisfies M w (◇^[(n + 1)]p)
Tactic:
simp
State after:
case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
⊢ ∀ (x x_1 : M.Frame.World),
    w ≺ x_1 →
      RelItr (fun x x_2 => x ≺ x_2) n x_1 x →
        Satisfies M x p → ∃ w', w ≺ w' ∧ Satisfies M w' ((UnaryModalOperator.mop false)^[n] p)

State before:
case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
⊢ ∀ (x x_1 : M.Frame.World),
    w ≺ x_1 →
      RelItr (fun x x_2 => x ≺ x_2) n x_1 x →
        Satisfies M x p → ∃ w', w ≺ w' ∧ Satisfies M w' ((UnaryModalOperator.mop false)^[n] p)
Tactic:
intro x y hwy hyx hx
State after:
case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
x y : M.Frame.World
hwy : w ≺ y
hyx : RelItr (fun x x_1 => x ≺ x_1) n y x
hx : Satisfies M x p
⊢ ∃ w', w ≺ w' ∧ Satisfies M w' ((UnaryModalOperator.mop false)^[n] p)

State before:
case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
x y : M.Frame.World
hwy : w ≺ y
hyx : RelItr (fun x x_1 => x ≺ x_1) n y x
hx : Satisfies M x p
⊢ ∃ w', w ≺ w' ∧ Satisfies M w' ((UnaryModalOperator.mop false)^[n] p)
Tactic:
existsi y
State after:
case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
x y : M.Frame.World
hwy : w ≺ y
hyx : RelItr (fun x x_1 => x ≺ x_1) n y x
hx : Satisfies M x p
⊢ w ≺ y ∧ Satisfies M y ((UnaryModalOperator.mop false)^[n] p)

State before:
case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
x y : M.Frame.World
hwy : w ≺ y
hyx : RelItr (fun x x_1 => x ≺ x_1) n y x
hx : Satisfies M x p
⊢ w ≺ y ∧ Satisfies M y ((UnaryModalOperator.mop false)^[n] p)
Tactic:
constructor
State after:
case succ.mpr.left
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
x y : M.Frame.World
hwy : w ≺ y
hyx : RelItr (fun x x_1 => x ≺ x_1) n y x
hx : Satisfies M x p
⊢ w ≺ y

case succ.mpr.right
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
x y : M.Frame.World
hwy : w ≺ y
hyx : RelItr (fun x x_1 => x ≺ x_1) n y x
hx : Satisfies M x p
⊢ Satisfies M y ((UnaryModalOperator.mop false)^[n] p)

State before:
case succ.mpr.left
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
x y : M.Frame.World
hwy : w ≺ y
hyx : RelItr (fun x x_1 => x ≺ x_1) n y x
hx : Satisfies M x p
⊢ w ≺ y

case succ.mpr.right
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
x y : M.Frame.World
hwy : w ≺ y
hyx : RelItr (fun x x_1 => x ≺ x_1) n y x
hx : Satisfies M x p
⊢ Satisfies M y ((UnaryModalOperator.mop false)^[n] p)
Tactic:
. simpa;
State after:
case succ.mpr.right
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
x y : M.Frame.World
hwy : w ≺ y
hyx : RelItr (fun x x_1 => x ≺ x_1) n y x
hx : Satisfies M x p
⊢ Satisfies M y ((UnaryModalOperator.mop false)^[n] p)

State before:
case succ.mpr.right
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
x y : M.Frame.World
hwy : w ≺ y
hyx : RelItr (fun x x_1 => x ≺ x_1) n y x
hx : Satisfies M x p
⊢ Satisfies M y ((UnaryModalOperator.mop false)^[n] p)
Tactic:
. apply ih.mpr;
  existsi x;
  simp_all;
State after:
no goals

State before:
case succ.mpr.left
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
x y : M.Frame.World
hwy : w ≺ y
hyx : RelItr (fun x x_1 => x ≺ x_1) n y x
hx : Satisfies M x p
⊢ w ≺ y
Tactic:
simpa
State after:
no goals

State before:
case succ.mpr.right
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
x y : M.Frame.World
hwy : w ≺ y
hyx : RelItr (fun x x_1 => x ≺ x_1) n y x
hx : Satisfies M x p
⊢ Satisfies M y ((UnaryModalOperator.mop false)^[n] p)
Tactic:
apply ih.mpr
State after:
case succ.mpr.right
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
x y : M.Frame.World
hwy : w ≺ y
hyx : RelItr (fun x x_1 => x ≺ x_1) n y x
hx : Satisfies M x p
⊢ ∃ v, y ≺^[n] v ∧ Satisfies M v p

State before:
case succ.mpr.right
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
x y : M.Frame.World
hwy : w ≺ y
hyx : RelItr (fun x x_1 => x ≺ x_1) n y x
hx : Satisfies M x p
⊢ ∃ v, y ≺^[n] v ∧ Satisfies M v p
Tactic:
existsi x
State after:
case succ.mpr.right
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
x y : M.Frame.World
hwy : w ≺ y
hyx : RelItr (fun x x_1 => x ≺ x_1) n y x
hx : Satisfies M x p
⊢ y ≺^[n] x ∧ Satisfies M x p

State before:
case succ.mpr.right
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
x y : M.Frame.World
hwy : w ≺ y
hyx : RelItr (fun x x_1 => x ≺ x_1) n y x
hx : Satisfies M x p
⊢ y ≺^[n] x ∧ Satisfies M x p
Tactic:
simp_all
State after:
no goals