Theorem: skip_injective (Saturn/Skip.lean)

State before:
n j1 j2 : Nat
hyp : skip n j1 = skip n j2
p1 : j1 < n
eq1 : skip n j1 = j1 := skip_below_eq p1
p2 : j2 < n
eq2 : skip n j2 = j2 := skip_below_eq p2
⊢ j1 = j2
Tactic:
rw [← eq1]
State after:
n j1 j2 : Nat
hyp : skip n j1 = skip n j2
p1 : j1 < n
eq1 : skip n j1 = j1 := skip_below_eq p1
p2 : j2 < n
eq2 : skip n j2 = j2 := skip_below_eq p2
⊢ skip n j1 = j2

State before:
n j1 j2 : Nat
hyp : skip n j1 = skip n j2
p1 : j1 < n
eq1 : skip n j1 = j1 := skip_below_eq p1
p2 : j2 < n
eq2 : skip n j2 = j2 := skip_below_eq p2
⊢ skip n j1 = j2
Tactic:
rw [← eq2]
State after:
n j1 j2 : Nat
hyp : skip n j1 = skip n j2
p1 : j1 < n
eq1 : skip n j1 = j1 := skip_below_eq p1
p2 : j2 < n
eq2 : skip n j2 = j2 := skip_below_eq p2
⊢ skip n j1 = skip n j2

State before:
n j1 j2 : Nat
hyp : skip n j1 = skip n j2
p1 : j1 < n
eq1 : skip n j1 = j1 := skip_below_eq p1
p2 : j2 < n
eq2 : skip n j2 = j2 := skip_below_eq p2
⊢ skip n j1 = skip n j2
Tactic:
exact hyp
State after:
no goals

State before:
n j1 j2 : Nat
hyp : skip n j1 = skip n j2
p1 : j1 ≥ n
eq1 : skip n j1 = succ j1 := skip_above_eq n j1 p1
p2 : j2 ≥ n
eq2 : skip n j2 = succ j2 := skip_above_eq n j2 p2
⊢ succ j1 = succ j2
Tactic:
rw [← eq1]
State after:
n j1 j2 : Nat
hyp : skip n j1 = skip n j2
p1 : j1 ≥ n
eq1 : skip n j1 = succ j1 := skip_above_eq n j1 p1
p2 : j2 ≥ n
eq2 : skip n j2 = succ j2 := skip_above_eq n j2 p2
⊢ skip n j1 = succ j2

State before:
n j1 j2 : Nat
hyp : skip n j1 = skip n j2
p1 : j1 ≥ n
eq1 : skip n j1 = succ j1 := skip_above_eq n j1 p1
p2 : j2 ≥ n
eq2 : skip n j2 = succ j2 := skip_above_eq n j2 p2
⊢ skip n j1 = succ j2
Tactic:
rw [← eq2]
State after:
n j1 j2 : Nat
hyp : skip n j1 = skip n j2
p1 : j1 ≥ n
eq1 : skip n j1 = succ j1 := skip_above_eq n j1 p1
p2 : j2 ≥ n
eq2 : skip n j2 = succ j2 := skip_above_eq n j2 p2
⊢ skip n j1 = skip n j2

State before:
n j1 j2 : Nat
hyp : skip n j1 = skip n j2
p1 : j1 ≥ n
eq1 : skip n j1 = succ j1 := skip_above_eq n j1 p1
p2 : j2 ≥ n
eq2 : skip n j2 = succ j2 := skip_above_eq n j2 p2
⊢ skip n j1 = skip n j2
Tactic:
exact hyp
State after:
no goals

State before:
n j1 j2 : Nat
hyp : skip n j1 = skip n j2
p1 : j1 ≥ n
eq1 : skip n j1 = succ j1 := skip_above_eq n j1 p1
p2 : j2 ≥ n
eq2 : skip n j2 = succ j2 := skip_above_eq n j2 p2
eq3 : succ j1 = succ j2 :=
  Eq.mpr (id (congrArg (fun _a => _a = succ j2) (Eq.symm eq1)))
    (Eq.mpr (id (congrArg (fun _a => skip n j1 = _a) (Eq.symm eq2))) hyp)
⊢ j1 = j2
Tactic:
injection eq3
State after:
no goals