Theorem: skipInverse_eq (Saturn/Skip.lean)

State before:
n m : Nat
eqn : m ≠ n
⊢ skip n (skipInverse n m eqn) = m
Tactic:
by_cases c : m < n
State after:
case inl
n m : Nat
eqn : m ≠ n
c : m < n
⊢ skip n (skipInverse n m eqn) = m

case inr
n m : Nat
eqn : m ≠ n
c : ¬m < n
⊢ skip n (skipInverse n m eqn) = m

State before:
case inl
n m : Nat
eqn : m ≠ n
c : m < n
⊢ skip n (skipInverse n m eqn) = m
Tactic:
rw [skipInverse]
State after:
case inl
n m : Nat
eqn : m ≠ n
c : m < n
⊢ skip n
      (if x : n < m then
        match m, eqn, x with
        | zero, x, x_1 =>
          let_fun x := (_ : 0 ≤ n);
          False.elim (_ : False)
        | succ p, x, x_1 => p
      else m) =
    m

State before:
case inl
n m : Nat
eqn : m ≠ n
c : m < n
⊢ skip n
      (if x : n < m then
        match m, eqn, x with
        | zero, x, x_1 =>
          let_fun x := (_ : 0 ≤ n);
          False.elim (_ : False)
        | succ p, x, x_1 => p
      else m) =
    m
Tactic:
simp [eqn, c]
State after:
case inl
n m : Nat
eqn : m ≠ n
c : m < n
⊢ skip n
      (if h : n < m then
        match m, eqn, (_ : n < m) with
        | zero, x, x_1 => False.elim (_ : False)
        | succ p, x, x_1 => p
      else m) =
    m

State before:
case inl
n m : Nat
eqn : m ≠ n
c : m < n
⊢ skip n
      (if h : n < m then
        match m, eqn, (_ : n < m) with
        | zero, x, x_1 => False.elim (_ : False)
        | succ p, x, x_1 => p
      else m) =
    m
Tactic:
have h' : ¬ (n < m) := by
  apply Nat.not_le_of_gt
  apply Nat.le_trans c
  apply Nat.le_succ
State after:
case inl
n m : Nat
eqn : m ≠ n
c : m < n
h' : ¬n < m
⊢ skip n
      (if h : n < m then
        match m, eqn, (_ : n < m) with
        | zero, x, x_1 => False.elim (_ : False)
        | succ p, x, x_1 => p
      else m) =
    m

State before:
case inl
n m : Nat
eqn : m ≠ n
c : m < n
h' : ¬n < m
⊢ skip n
      (if h : n < m then
        match m, eqn, (_ : n < m) with
        | zero, x, x_1 => False.elim (_ : False)
        | succ p, x, x_1 => p
      else m) =
    m
Tactic:
simp [h']
State after:
case inl
n m : Nat
eqn : m ≠ n
c : m < n
h' : ¬n < m
⊢ skip n m = m

State before:
case inl
n m : Nat
eqn : m ≠ n
c : m < n
h' : ¬n < m
⊢ skip n m = m
Tactic:
exact skip_below_eq c
State after:
no goals

State before:
n m : Nat
eqn : m ≠ n
c : m < n
⊢ ¬n < m
Tactic:
apply Nat.not_le_of_gt
State after:
case h
n m : Nat
eqn : m ≠ n
c : m < n
⊢ succ n > m

State before:
case h
n m : Nat
eqn : m ≠ n
c : m < n
⊢ succ n > m
Tactic:
apply Nat.le_trans c
State after:
case h
n m : Nat
eqn : m ≠ n
c : m < n
⊢ n ≤ succ n

State before:
case h
n m : Nat
eqn : m ≠ n
c : m < n
⊢ n ≤ succ n
Tactic:
apply Nat.le_succ
State after:
no goals

State before:
case inr
n m : Nat
eqn : m ≠ n
c : ¬m < n
⊢ skip n (skipInverse n m eqn) = m
Tactic:
rw [skipInverse]
State after:
case inr
n m : Nat
eqn : m ≠ n
c : ¬m < n
⊢ skip n
      (if x : n < m then
        match m, eqn, x with
        | zero, x, x_1 =>
          let_fun x := (_ : 0 ≤ n);
          False.elim (_ : False)
        | succ p, x, x_1 => p
      else m) =
    m

State before:
case inr
n m : Nat
eqn : m ≠ n
c : ¬m < n
h' : n < m
⊢ skip n
      (if x : n < m then
        match m, eqn, x with
        | zero, x, x_1 =>
          let_fun x := (_ : 0 ≤ n);
          False.elim (_ : False)
        | succ p, x, x_1 => p
      else m) =
    m
Tactic:
simp [h']
State after:
case inr
n m : Nat
eqn : m ≠ n
c : ¬m < n
h' : n < m
⊢ skip n
      (match m, eqn, (_ : n < m) with
      | zero, x, x_1 => False.elim (_ : False)
      | succ p, x, x_1 => p) =
    m

State before:
case inr
n m : Nat
eqn : m ≠ n
c : ¬m < n
h' : n < m
⊢ skip n
      (match m, eqn, (_ : n < m) with
      | zero, x, x_1 => False.elim (_ : False)
      | succ p, x, x_1 => p) =
    m
Tactic:
match m with
| zero =>
  have _ := Nat.zero_le n
  contradiction
| succ p =>
  apply skip_above_eq n p
  apply Nat.le_of_succ_le_succ
  apply Nat.le_trans h'
  simp
State after:
no goals

State before:
n m : Nat
eqn : m ≠ n
c : ¬m < n
⊢ n < m
Tactic:
apply Nat.lt_of_le_of_ne
State after:
case h₁
n m : Nat
eqn : m ≠ n
c : ¬m < n
⊢ n ≤ m

case h₂
n m : Nat
eqn : m ≠ n
c : ¬m < n
⊢ ¬n = m

State before:
case h₁
n m : Nat
eqn : m ≠ n
c : ¬m < n
⊢ n ≤ m
Tactic:
by_cases h'' : n ≤ m
State after:
case h₁.inl
n m : Nat
eqn : m ≠ n
c : ¬m < n
h'' : n ≤ m
⊢ n ≤ m

case h₁.inr
n m : Nat
eqn : m ≠ n
c : ¬m < n
h'' : ¬n ≤ m
⊢ n ≤ m

State before:
case h₁.inl
n m : Nat
eqn : m ≠ n
c : ¬m < n
h'' : n ≤ m
⊢ n ≤ m
Tactic:
assumption
State after:
no goals

State before:
case h₁.inr
n m : Nat
eqn : m ≠ n
c : ¬m < n
h'' : ¬n ≤ m
⊢ n ≤ m
Tactic:
let h''' := Nat.gt_of_not_le h''
State after:
case h₁.inr
n m : Nat
eqn : m ≠ n
c : ¬m < n
h'' : ¬n ≤ m
h''' : n > m := gt_of_not_le h''
⊢ n ≤ m

State before:
case h₁.inr
n m : Nat
eqn : m ≠ n
c : ¬m < n
h'' : ¬n ≤ m
h''' : n > m := gt_of_not_le h''
⊢ n ≤ m
Tactic:
contradiction
State after:
no goals

State before:
case h₂
n m : Nat
eqn : m ≠ n
c : ¬m < n
⊢ ¬n = m
Tactic:
intro contra
State after:
case h₂
n m : Nat
eqn : m ≠ n
c : ¬m < n
contra : n = m
⊢ False

State before:
case h₂
n m : Nat
eqn : m ≠ n
c : ¬m < n
contra : n = m
⊢ False
Tactic:
simp [contra] at eqn
State after:
no goals

State before:
n m : Nat
eqn : zero ≠ n
c : ¬zero < n
h' : n < zero
⊢ skip n
      (match zero, eqn, (_ : n < zero) with
      | zero, x, x_1 => False.elim (_ : False)
      | succ p, x, x_1 => p) =
    zero
Tactic:
have _ := Nat.zero_le n
State after:
n m : Nat
eqn : zero ≠ n
c : ¬zero < n
h' : n < zero
x✝ : 0 ≤ n
⊢ skip n
      (match zero, eqn, (_ : n < zero) with
      | zero, x, x_1 => False.elim (_ : False)
      | succ p, x, x_1 => p) =
    zero

State before:
n m : Nat
eqn : zero ≠ n
c : ¬zero < n
h' : n < zero
x✝ : 0 ≤ n
⊢ skip n
      (match zero, eqn, (_ : n < zero) with
      | zero, x, x_1 => False.elim (_ : False)
      | succ p, x, x_1 => p) =
    zero
Tactic:
contradiction
State after:
no goals

State before:
n m p : Nat
eqn : succ p ≠ n
c : ¬succ p < n
h' : n < succ p
⊢ skip n
      (match succ p, eqn, (_ : n < succ p) with
      | zero, x, x_1 => False.elim (_ : False)
      | succ p, x, x_1 => p) =
    succ p
Tactic:
apply skip_above_eq n p
State after:
n m p : Nat
eqn : succ p ≠ n
c : ¬succ p < n
h' : n < succ p
⊢ n ≤ p

State before:
n m p : Nat
eqn : succ p ≠ n
c : ¬succ p < n
h' : n < succ p
⊢ n ≤ p
Tactic:
apply Nat.le_of_succ_le_succ
State after:
case a
n m p : Nat
eqn : succ p ≠ n
c : ¬succ p < n
h' : n < succ p
⊢ succ n ≤ succ p

State before:
case a
n m p : Nat
eqn : succ p ≠ n
c : ¬succ p < n
h' : n < succ p
⊢ succ n ≤ succ p
Tactic:
apply Nat.le_trans h'
State after:
case a
n m p : Nat
eqn : succ p ≠ n
c : ¬succ p < n
h' : n < succ p
⊢ succ p ≤ succ p

State before:
case a
n m p : Nat
eqn : succ p ≠ n
c : ¬succ p < n
h' : n < succ p
⊢ succ p ≤ succ p
Tactic:
simp
State after:
no goals