Theorem: LO.Modal.Standard.Kripke.Frame.terminal.relItr (Logic/Modal/Standard/Kripke/Semantics.lean)

State before:
n : ℕ
x y : terminal.World
⊢ x ≺^[n] y ↔ x = y
Tactic:
induction n with
| zero => simp;
| succ n ih => simp; use x; simp [ih];
State after:
no goals

State before:
case zero
x y : terminal.World
⊢ x ≺^[0] y ↔ x = y
Tactic:
simp
State after:
no goals

State before:
case succ
x y : terminal.World
n : ℕ
ih : x ≺^[n] y ↔ x = y
⊢ x ≺^[n + 1] y ↔ x = y
Tactic:
simp
State after:
case succ
x y : terminal.World
n : ℕ
ih : x ≺^[n] y ↔ x = y
⊢ ∃ x, RelItr (fun x x_1 => x ≺ x_1) n x y

State before:
case succ
x y : terminal.World
n : ℕ
ih : x ≺^[n] y ↔ x = y
⊢ ∃ x, RelItr (fun x x_1 => x ≺ x_1) n x y
Tactic:
use x
State after:
case h
x y : terminal.World
n : ℕ
ih : x ≺^[n] y ↔ x = y
⊢ RelItr (fun x x_1 => x ≺ x_1) n x y

State before:
case h
x y : terminal.World
n : ℕ
ih : x ≺^[n] y ↔ x = y
⊢ RelItr (fun x x_1 => x ≺ x_1) n x y
Tactic:
simp [ih]
State after:
no goals