Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multibox_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 : M.Frame.World), w ≺^[n] v → Satisfies M v p
Tactic:
induction n generalizing w with
| zero => simp;
| succ n ih =>
  constructor;
  . intro h w' hww';
    simp at h;
    obtain ⟨v, hwv, hvw'⟩ := hww';
    exact (ih.mp $ h _ hwv) w' hvw';
  . simp;
    intro h w' hww';
    apply ih.mpr;
    intro v hwv;
    exact h v w' hww' hwv;
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 : M.Frame.World), 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 : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
⊢ Satisfies M w (□^[(n + 1)]p) ↔ ∀ (v : M.Frame.World), 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 : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
⊢ Satisfies M w (□^[(n + 1)]p) → ∀ (v : M.Frame.World), 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 : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
⊢ (∀ (v : M.Frame.World), 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 : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
⊢ Satisfies M w (□^[(n + 1)]p) → ∀ (v : M.Frame.World), 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 : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
⊢ (∀ (v : M.Frame.World), w ≺^[n + 1] v → Satisfies M v p) → Satisfies M w (□^[(n + 1)]p)
Tactic:
. intro h w' hww';
  simp at h;
  obtain ⟨v, hwv, hvw'⟩ := hww';
  exact (ih.mp $ h _ hwv) w' hvw';
State after:
case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (□^[n]p) ↔ ∀ (v : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
⊢ (∀ (v : M.Frame.World), 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 : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
⊢ (∀ (v : M.Frame.World), w ≺^[n + 1] v → Satisfies M v p) → Satisfies M w (□^[(n + 1)]p)
Tactic:
. simp;
  intro h w' hww';
  apply ih.mpr;
  intro v hwv;
  exact h v w' hww' hwv;
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 : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
⊢ Satisfies M w (□^[(n + 1)]p) → ∀ (v : M.Frame.World), w ≺^[n + 1] v → Satisfies M v p
Tactic:
intro h w' hww'
State after:
case succ.mp
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (□^[n]p) ↔ ∀ (v : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
h : Satisfies M w (□^[(n + 1)]p)
w' : M.Frame.World
hww' : w ≺^[n + 1] w'
⊢ Satisfies M w' 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 : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
h : Satisfies M w (□^[(n + 1)]p)
w' : M.Frame.World
hww' : w ≺^[n + 1] w'
⊢ Satisfies M w' p
Tactic:
simp at 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 : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
w' : M.Frame.World
hww' : w ≺^[n + 1] w'
h : ∀ (w' : M.Frame.World), w ≺ w' → Satisfies M w' ((UnaryModalOperator.mop true)^[n] p)
⊢ Satisfies M w' 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 : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
w' : M.Frame.World
hww' : w ≺^[n + 1] w'
h : ∀ (w' : M.Frame.World), w ≺ w' → Satisfies M w' ((UnaryModalOperator.mop true)^[n] p)
⊢ Satisfies M w' p
Tactic:
obtain ⟨v, hwv, hvw'⟩ := hww'
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 : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
w' : M.Frame.World
h : ∀ (w' : M.Frame.World), w ≺ w' → Satisfies M w' ((UnaryModalOperator.mop true)^[n] p)
v : M.Frame.World
hwv : w ≺ v
hvw' : RelItr (fun x x_1 => x ≺ x_1) n v w'
⊢ Satisfies M w' 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 : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
w' : M.Frame.World
h : ∀ (w' : M.Frame.World), w ≺ w' → Satisfies M w' ((UnaryModalOperator.mop true)^[n] p)
v : M.Frame.World
hwv : w ≺ v
hvw' : RelItr (fun x x_1 => x ≺ x_1) n v w'
⊢ Satisfies M w' p
Tactic:
exact (ih.mp $ h _ hwv) w' hvw'
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 : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
⊢ (∀ (v : M.Frame.World), 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 : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
⊢ (∀ (v x : M.Frame.World), w ≺ x → RelItr (fun x x_1 => x ≺ x_1) n x v → Satisfies M v p) →
    ∀ (w' : M.Frame.World), w ≺ w' → Satisfies M w' ((UnaryModalOperator.mop true)^[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 : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
⊢ (∀ (v x : M.Frame.World), w ≺ x → RelItr (fun x x_1 => x ≺ x_1) n x v → Satisfies M v p) →
    ∀ (w' : M.Frame.World), w ≺ w' → Satisfies M w' ((UnaryModalOperator.mop true)^[n] p)
Tactic:
intro h w' hww'
State after:
case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (□^[n]p) ↔ ∀ (v : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
h : ∀ (v x : M.Frame.World), w ≺ x → RelItr (fun x x_1 => x ≺ x_1) n x v → Satisfies M v p
w' : M.Frame.World
hww' : w ≺ w'
⊢ Satisfies M w' ((UnaryModalOperator.mop true)^[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 : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
h : ∀ (v x : M.Frame.World), w ≺ x → RelItr (fun x x_1 => x ≺ x_1) n x v → Satisfies M v p
w' : M.Frame.World
hww' : w ≺ w'
⊢ Satisfies M w' ((UnaryModalOperator.mop true)^[n] p)
Tactic:
apply ih.mpr
State after:
case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (□^[n]p) ↔ ∀ (v : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
h : ∀ (v x : M.Frame.World), w ≺ x → RelItr (fun x x_1 => x ≺ x_1) n x v → Satisfies M v p
w' : M.Frame.World
hww' : w ≺ w'
⊢ ∀ (v : M.Frame.World), w' ≺^[n] v → Satisfies M v 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 : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
h : ∀ (v x : M.Frame.World), w ≺ x → RelItr (fun x x_1 => x ≺ x_1) n x v → Satisfies M v p
w' : M.Frame.World
hww' : w ≺ w'
⊢ ∀ (v : M.Frame.World), w' ≺^[n] v → Satisfies M v p
Tactic:
intro v hwv
State after:
case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (□^[n]p) ↔ ∀ (v : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
h : ∀ (v x : M.Frame.World), w ≺ x → RelItr (fun x x_1 => x ≺ x_1) n x v → Satisfies M v p
w' : M.Frame.World
hww' : w ≺ w'
v : M.Frame.World
hwv : w' ≺^[n] v
⊢ Satisfies M v 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 : M.Frame.World), w ≺^[n] v → Satisfies M v p
w : M.World
h : ∀ (v x : M.Frame.World), w ≺ x → RelItr (fun x x_1 => x ≺ x_1) n x v → Satisfies M v p
w' : M.Frame.World
hww' : w ≺ w'
v : M.Frame.World
hwv : w' ≺^[n] v
⊢ Satisfies M v p
Tactic:
exact h v w' hww' hwv
State after:
no goals