Theorem: skip_preimage_lt (Saturn/Skip.lean)

State before:
i j k n : Nat
kw : k < n + 1
jw : j < n + 1
eqn : skip k i = j
ineq : i + 1 ≤ skip k i
⊢ i < n
Tactic:
have lem1 : i <  j :=
by
  rw [← eqn]
  exact ineq
State after:
i j k n : Nat
kw : k < n + 1
jw : j < n + 1
eqn : skip k i = j
ineq : i + 1 ≤ skip k i
lem1 : i < j
⊢ i < n

State before:
i j k n : Nat
kw : k < n + 1
jw : j < n + 1
eqn : skip k i = j
ineq : i + 1 ≤ skip k i
lem1 : i < j
⊢ i < n
Tactic:
apply Nat.lt_of_lt_of_le lem1
State after:
i j k n : Nat
kw : k < n + 1
jw : j < n + 1
eqn : skip k i = j
ineq : i + 1 ≤ skip k i
lem1 : i < j
⊢ j ≤ n

State before:
i j k n : Nat
kw : k < n + 1
jw : j < n + 1
eqn : skip k i = j
ineq : i + 1 ≤ skip k i
lem1 : i < j
⊢ j ≤ n
Tactic:
apply Nat.le_of_succ_le_succ
State after:
case a
i j k n : Nat
kw : k < n + 1
jw : j < n + 1
eqn : skip k i = j
ineq : i + 1 ≤ skip k i
lem1 : i < j
⊢ succ j ≤ succ n

State before:
case a
i j k n : Nat
kw : k < n + 1
jw : j < n + 1
eqn : skip k i = j
ineq : i + 1 ≤ skip k i
lem1 : i < j
⊢ succ j ≤ succ n
Tactic:
apply jw
State after:
no goals

State before:
i j k n : Nat
kw : k < n + 1
jw : j < n + 1
eqn : skip k i = j
ineq : i + 1 ≤ skip k i
⊢ i < j
Tactic:
rw [← eqn]
State after:
i j k n : Nat
kw : k < n + 1
jw : j < n + 1
eqn : skip k i = j
ineq : i + 1 ≤ skip k i
⊢ i < skip k i

State before:
i j k n : Nat
kw : k < n + 1
jw : j < n + 1
eqn : skip k i = j
ineq : i + 1 ≤ skip k i
⊢ i < skip k i
Tactic:
exact ineq
State after:
no goals

State before:
i j k n : Nat
kw : k < n + 1
jw : j < n + 1
eqn : skip k i = j
ineqn : i < k
⊢ i < n
Tactic:
apply Nat.lt_of_lt_of_le ineqn
State after:
i j k n : Nat
kw : k < n + 1
jw : j < n + 1
eqn : skip k i = j
ineqn : i < k
⊢ k ≤ n

State before:
i j k n : Nat
kw : k < n + 1
jw : j < n + 1
eqn : skip k i = j
ineqn : i < k
⊢ k ≤ n
Tactic:
apply Nat.le_of_succ_le_succ
State after:
case a
i j k n : Nat
kw : k < n + 1
jw : j < n + 1
eqn : skip k i = j
ineqn : i < k
⊢ succ k ≤ succ n

State before:
case a
i j k n : Nat
kw : k < n + 1
jw : j < n + 1
eqn : skip k i = j
ineqn : i < k
⊢ succ k ≤ succ n
Tactic:
apply kw
State after:
no goals