internlm/Lean-Github huggingface dataset:
Theorem: PrependClause.revrelAux
Proof state before:
num_reducedClauses n num_clauses : ℕ
v : Vector ℕ num_reducedClauses
clauses : Vector (Clause (n + 1)) num_clauses
head : Clause (n + 1)
l : ℕ
w : l < num_reducedClauses
bd : Vector.get v { val := l, isLt := w } < num_clauses
lem :
  Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) =
    Vector.get v { val := l, isLt := w } + 1
lem' : Fin.succ { val := Vector.get v { val := l, isLt := w }, isLt := bd } =
  { val := Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }),
    isLt := (_ : Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) < succ num_clauses) } :=
  Fin.eq_of_veq (id lem.symm)
lem'' : Vector.get (head ::ᵥ clauses) (Fin.succ { val := Vector.get v { val := l, isLt := w }, isLt := bd }) =
  Vector.get clauses { val := Vector.get v { val := l, isLt := w }, isLt := bd } :=
  get_cons_succ head clauses { val := Vector.get v { val := l, isLt := w }, isLt := bd }
⊢ Vector.get (head ::ᵥ clauses)
      { val := Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }),
        isLt :=
          (_ : Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) < succ num_clauses) } =
    Vector.get clauses { val := Vector.get v { val := l, isLt := w }, isLt := bd }
Tactic:
rw [lem'] at lem''
Proof state after:
num_reducedClauses n num_clauses : ℕ
v : Vector ℕ num_reducedClauses
clauses : Vector (Clause (n + 1)) num_clauses
head : Clause (n + 1)
l : ℕ
w : l < num_reducedClauses
bd : Vector.get v { val := l, isLt := w } < num_clauses
lem :
  Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) =
    Vector.get v { val := l, isLt := w } + 1
lem' : Fin.succ { val := Vector.get v { val := l, isLt := w }, isLt := bd } =
  { val := Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }),
    isLt := (_ : Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) < succ num_clauses) } :=
  Fin.eq_of_veq (id lem.symm)
lem'' :
  Vector.get (head ::ᵥ clauses)
      { val := Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }),
        isLt :=
          (_ : Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) < succ num_clauses) } =
    Vector.get clauses { val := Vector.get v { val := l, isLt := w }, isLt := bd }
⊢ Vector.get (head ::ᵥ clauses)
      { val := Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }),
        isLt :=
          (_ : Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) < succ num_clauses) } =
    Vector.get clauses { val := Vector.get v { val := l, isLt := w }, isLt := bd }
Theorem: PrependClause.revrelAux
Proof state before:
num_reducedClauses n num_clauses : ℕ
v : Vector ℕ num_reducedClauses
clauses : Vector (Clause (n + 1)) num_clauses
head : Clause (n + 1)
l : ℕ
w : l < num_reducedClauses
bd : Vector.get v { val := l, isLt := w } < num_clauses
lem :
  Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) =
    Vector.get v { val := l, isLt := w } + 1
lem' : Fin.succ { val := Vector.get v { val := l, isLt := w }, isLt := bd } =
  { val := Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }),
    isLt := (_ : Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) < succ num_clauses) } :=
  Fin.eq_of_veq (id lem.symm)
lem'' :
  Vector.get (head ::ᵥ clauses)
      { val := Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }),
        isLt :=
          (_ : Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) < succ num_clauses) } =
    Vector.get clauses { val := Vector.get v { val := l, isLt := w }, isLt := bd }
⊢ Vector.get (head ::ᵥ clauses)
      { val := Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }),
        isLt :=
          (_ : Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) < succ num_clauses) } =
    Vector.get clauses { val := Vector.get v { val := l, isLt := w }, isLt := bd }
Tactic:
exact lem''
Proof state after:
no goals
Theorem: PrependClause.revrelAux
Proof state before:
num_reducedClauses n num_clauses : ℕ
v : Vector ℕ num_reducedClauses
clauses : Vector (Clause (n + 1)) num_clauses
head : Clause (n + 1)
l : ℕ
w : l < num_reducedClauses
bd : Vector.get v { val := l, isLt := w } < num_clauses
lem :
  Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) =
    Vector.get v { val := l, isLt := w } + 1
⊢ Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) < succ num_clauses
Tactic:
rw [lem]
Proof state after:
num_reducedClauses n num_clauses : ℕ
v : Vector ℕ num_reducedClauses
clauses : Vector (Clause (n + 1)) num_clauses
head : Clause (n + 1)
l : ℕ
w : l < num_reducedClauses
bd : Vector.get v { val := l, isLt := w } < num_clauses
lem :
  Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) =
    Vector.get v { val := l, isLt := w } + 1
⊢ Vector.get v { val := l, isLt := w } + 1 < succ num_clauses
Theorem: PrependClause.revrelAux
Proof state before:
num_reducedClauses n num_clauses : ℕ
v : Vector ℕ num_reducedClauses
clauses : Vector (Clause (n + 1)) num_clauses
head : Clause (n + 1)
l : ℕ
w : l < num_reducedClauses
bd : Vector.get v { val := l, isLt := w } < num_clauses
lem :
  Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) =
    Vector.get v { val := l, isLt := w } + 1
⊢ Vector.get v { val := l, isLt := w } + 1 < succ num_clauses
Tactic:
apply Nat.succ_lt_succ
Proof state after:
case a
num_reducedClauses n num_clauses : ℕ
v : Vector ℕ num_reducedClauses
clauses : Vector (Clause (n + 1)) num_clauses
head : Clause (n + 1)
l : ℕ
w : l < num_reducedClauses
bd : Vector.get v { val := l, isLt := w } < num_clauses
lem :
  Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) =
    Vector.get v { val := l, isLt := w } + 1
⊢ Vector.get v { val := l, isLt := w } < num_clauses
Theorem: PrependClause.revrelAux
Proof state before:
case a
num_reducedClauses n num_clauses : ℕ
v : Vector ℕ num_reducedClauses
clauses : Vector (Clause (n + 1)) num_clauses
head : Clause (n + 1)
l : ℕ
w : l < num_reducedClauses
bd : Vector.get v { val := l, isLt := w } < num_clauses
lem :
  Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) =
    Vector.get v { val := l, isLt := w } + 1
⊢ Vector.get v { val := l, isLt := w } < num_clauses
Tactic:
exact bd
Proof state after:
no goals
Theorem: PrependClause.revrelAux
Proof state before:
num_reducedClauses n num_clauses : ℕ
v : Vector ℕ num_reducedClauses
clauses : Vector (Clause (n + 1)) num_clauses
head : Clause (n + 1)
l : ℕ
w : l < num_reducedClauses
bd : Vector.get v { val := l, isLt := w } < num_clauses
lem :
  Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) =
    Vector.get v { val := l, isLt := w } + 1
⊢ Fin.succ { val := Vector.get v { val := l, isLt := w }, isLt := bd } =
    { val := Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }),
      isLt := (_ : Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) < succ num_clauses) }
Tactic:
apply Fin.eq_of_veq
Proof state after:
case a
num_reducedClauses n num_clauses : ℕ
v : Vector ℕ num_reducedClauses
clauses : Vector (Clause (n + 1)) num_clauses
head : Clause (n + 1)
l : ℕ
w : l < num_reducedClauses
bd : Vector.get v { val := l, isLt := w } < num_clauses
lem :
  Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) =
    Vector.get v { val := l, isLt := w } + 1
⊢ ↑(Fin.succ { val := Vector.get v { val := l, isLt := w }, isLt := bd }) =
    ↑{ val := Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }),
        isLt := (_ : Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) < succ num_clauses) }
Theorem: PrependClause.revrelAux
Proof state before:
case a
num_reducedClauses n num_clauses : ℕ
v : Vector ℕ num_reducedClauses
clauses : Vector (Clause (n + 1)) num_clauses
head : Clause (n + 1)
l : ℕ
w : l < num_reducedClauses
bd : Vector.get v { val := l, isLt := w } < num_clauses
lem :
  Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) =
    Vector.get v { val := l, isLt := w } + 1
⊢ ↑(Fin.succ { val := Vector.get v { val := l, isLt := w }, isLt := bd }) =
    ↑{ val := Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }),
        isLt := (_ : Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) < succ num_clauses) }
Tactic:
simp
Proof state after:
case a
num_reducedClauses n num_clauses : ℕ
v : Vector ℕ num_reducedClauses
clauses : Vector (Clause (n + 1)) num_clauses
head : Clause (n + 1)
l : ℕ
w : l < num_reducedClauses
bd : Vector.get v { val := l, isLt := w } < num_clauses
lem :
  Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) =
    Vector.get v { val := l, isLt := w } + 1
⊢ Vector.get v { val := l, isLt := w } + 1 =
    Vector.get (0 ::ᵥ map (fun x => x + 1) v) { val := l + 1, isLt := (_ : succ l < succ num_reducedClauses) }
Theorem: PrependClause.revrelAux
Proof state before:
case a
num_reducedClauses n num_clauses : ℕ
v : Vector ℕ num_reducedClauses
clauses : Vector (Clause (n + 1)) num_clauses
head : Clause (n + 1)
l : ℕ
w : l < num_reducedClauses
bd : Vector.get v { val := l, isLt := w } < num_clauses
lem :
  Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) =
    Vector.get v { val := l, isLt := w } + 1
⊢ Vector.get v { val := l, isLt := w } + 1 =
    Vector.get (0 ::ᵥ map (fun x => x + 1) v) { val := l + 1, isLt := (_ : succ l < succ num_reducedClauses) }
Tactic:
symm
Proof state after:
case a
num_reducedClauses n num_clauses : ℕ
v : Vector ℕ num_reducedClauses
clauses : Vector (Clause (n + 1)) num_clauses
head : Clause (n + 1)
l : ℕ
w : l < num_reducedClauses
bd : Vector.get v { val := l, isLt := w } < num_clauses
lem :
  Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) =
    Vector.get v { val := l, isLt := w } + 1
⊢ Vector.get (0 ::ᵥ map (fun x => x + 1) v) { val := l + 1, isLt := (_ : succ l < succ num_reducedClauses) } =
    Vector.get v { val := l, isLt := w } + 1
Theorem: PrependClause.revrelAux
Proof state before:
case a
num_reducedClauses n num_clauses : ℕ
v : Vector ℕ num_reducedClauses
clauses : Vector (Clause (n + 1)) num_clauses
head : Clause (n + 1)
l : ℕ
w : l < num_reducedClauses
bd : Vector.get v { val := l, isLt := w } < num_clauses
lem :
  Vector.get (0 ::ᵥ map (fun x => x + 1) v) (Fin.succ { val := l, isLt := w }) =
    Vector.get v { val := l, isLt := w } + 1
⊢ Vector.get (0 ::ᵥ map (fun x => x + 1) v) { val := l + 1, isLt := (_ : succ l < succ num_reducedClauses) } =
    Vector.get v { val := l, isLt := w } + 1
Tactic:
exact lem
Proof state after:
no goals
Theorem: skip_below_eq
Proof state before:
n m : Nat
⊢ m < n → skip n m = m
Tactic:
intro hyp
Proof state after:
n m : Nat
hyp : m < n
⊢ skip n m = m
Theorem: skip_below_eq
Proof state before:
n m : Nat
hyp : m < n
⊢ skip n m = m
Tactic:
rw [skip]
Proof state after:
n m : Nat
hyp : m < n
⊢ (match n, m with
    | n, m => if m < n then m else m + 1) =
    m
Theorem: skip_below_eq
Proof state before:
n m : Nat
hyp : m < n
⊢ (match n, m with
    | n, m => if m < n then m else m + 1) =
    m
Tactic:
by_cases c: m < n
Proof state after:
case inl
n m : Nat
hyp c : m < n
⊢ (match n, m with
    | n, m => if m < n then m else m + 1) =
    m

case inr
n m : Nat
hyp : m < n
c : ¬m < n
⊢ (match n, m with
    | n, m => if m < n then m else m + 1) =
    m
Theorem: skip_below_eq
Proof state before:
case inl
n m : Nat
hyp c : m < n
⊢ (match n, m with
    | n, m => if m < n then m else m + 1) =
    m
Tactic:
simp [c]
Proof state after:
no goals
Theorem: skip_below_eq
Proof state before:
case inr
n m : Nat
hyp : m < n
c : ¬m < n
⊢ (match n, m with
    | n, m => if m < n then m else m + 1) =
    m
Tactic:
contradiction
Proof state after:
no goals
Theorem: skip_above_eq
Proof state before:
n m : Nat
⊢ n ≤ m → skip n m = m + 1
Tactic:
intro hyp
Proof state after:
n m : Nat
hyp : n ≤ m
⊢ skip n m = m + 1
Theorem: skip_above_eq
Proof state before:
n m : Nat
hyp : n ≤ m
⊢ skip n m = m + 1
Tactic:
rw [skip]
Proof state after:
n m : Nat
hyp : n ≤ m
⊢ (match n, m with
    | n, m => if m < n then m else m + 1) =
    m + 1
Theorem: skip_above_eq
Proof state before:
n m : Nat
hyp : n ≤ m
⊢ (match n, m with
    | n, m => if m < n then m else m + 1) =
    m + 1
Tactic:
by_cases c: m < n
Proof state after:
case inl
n m : Nat
hyp : n ≤ m
c : m < n
⊢ (match n, m with
    | n, m => if m < n then m else m + 1) =
    m + 1

case inr
n m : Nat
hyp : n ≤ m
c : ¬m < n
⊢ (match n, m with
    | n, m => if m < n then m else m + 1) =
    m + 1
Theorem: skip_above_eq
Proof state before:
case inl
n m : Nat
hyp : n ≤ m
c : m < n
⊢ (match n, m with
    | n, m => if m < n then m else m + 1) =
    m + 1
Tactic:
have c' : ¬(n ≤ m)  := Nat.not_le_of_gt c
Proof state after:
case inl
n m : Nat
hyp : n ≤ m
c : m < n
c' : ¬n ≤ m
⊢ (match n, m with
    | n, m => if m < n then m else m + 1) =
    m + 1
Theorem: skip_above_eq
Proof state before:
case inl
n m : Nat
hyp : n ≤ m
c : m < n
c' : ¬n ≤ m
⊢ (match n, m with
    | n, m => if m < n then m else m + 1) =
    m + 1
Tactic:
contradiction
Proof state after:
no goals
Theorem: skip_above_eq
Proof state before:
case inr
n m : Nat
hyp : n ≤ m
c : ¬m < n
⊢ (match n, m with
    | n, m => if m < n then m else m + 1) =
    m + 1
Tactic:
simp [c]
Proof state after:
no goals
Theorem: skipInverse_eq
Proof state before:
n m : Nat
eqn : m ≠ n
⊢ skip n (skipInverse n m eqn) = m
Tactic:
by_cases c : m < n
Proof 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
Theorem: skipInverse_eq
Proof state before:
case inl
n m : Nat
eqn : m ≠ n
c : m < n
⊢ skip n (skipInverse n m eqn) = m
Tactic:
rw [skipInverse]
Proof 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
Theorem: skipInverse_eq
Proof 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]
Proof 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
Theorem: skipInverse_eq
Proof 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
Proof 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
Theorem: skipInverse_eq
Proof 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']
Proof state after:
case inl
n m : Nat
eqn : m ≠ n
c : m < n
h' : ¬n < m
⊢ skip n m = m
Theorem: skipInverse_eq
Proof 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
Proof state after:
no goals
Theorem: skipInverse_eq
Proof state before:
n m : Nat
eqn : m ≠ n
c : m < n
⊢ ¬n < m
Tactic:
apply Nat.not_le_of_gt
Proof state after:
case h
n m : Nat
eqn : m ≠ n
c : m < n
⊢ succ n > m
Theorem: skipInverse_eq
Proof state before:
case h
n m : Nat
eqn : m ≠ n
c : m < n
⊢ succ n > m
Tactic:
apply Nat.le_trans c
Proof state after:
case h
n m : Nat
eqn : m ≠ n
c : m < n
⊢ n ≤ succ n
Theorem: skipInverse_eq
Proof state before:
case h
n m : Nat
eqn : m ≠ n
c : m < n
⊢ n ≤ succ n
Tactic:
apply Nat.le_succ
Proof state after:
no goals
Theorem: skipInverse_eq
Proof state before:
case inr
n m : Nat
eqn : m ≠ n
c : ¬m < n
⊢ skip n (skipInverse n m eqn) = m
Tactic:
rw [skipInverse]
Proof 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
Theorem: skipInverse_eq
Proof 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']
Proof 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
Theorem: skipInverse_eq
Proof 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
Proof state after:
no goals
Theorem: skipInverse_eq
Proof state before:
n m : Nat
eqn : m ≠ n
c : ¬m < n
⊢ n < m
Tactic:
apply Nat.lt_of_le_of_ne
Proof 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
Theorem: skipInverse_eq
Proof state before:
case h₁
n m : Nat
eqn : m ≠ n
c : ¬m < n
⊢ n ≤ m
Tactic:
by_cases h'' : n ≤ m
Proof 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
Theorem: skipInverse_eq
Proof state before:
case h₁.inl
n m : Nat
eqn : m ≠ n
c : ¬m < n
h'' : n ≤ m
⊢ n ≤ m
Tactic:
assumption
Proof state after:
no goals
Theorem: skipInverse_eq
Proof 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''
Proof 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
Theorem: skipInverse_eq
Proof 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
Proof state after:
no goals
Theorem: skipInverse_eq
Proof state before:
case h₂
n m : Nat
eqn : m ≠ n
c : ¬m < n
⊢ ¬n = m
Tactic:
intro contra
Proof state after:
case h₂
n m : Nat
eqn : m ≠ n
c : ¬m < n
contra : n = m
⊢ False
Theorem: skipInverse_eq
Proof state before:
case h₂
n m : Nat
eqn : m ≠ n
c : ¬m < n
contra : n = m
⊢ False
Tactic:
simp [contra] at eqn
Proof state after:
no goals
Theorem: skipInverse_eq
Proof 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
Proof 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
Theorem: skipInverse_eq
Proof 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
Proof state after:
no goals
Theorem: skipInverse_eq
Proof 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
Proof state after:
n m p : Nat
eqn : succ p ≠ n
c : ¬succ p < n
h' : n < succ p
⊢ n ≤ p
Theorem: skipInverse_eq
Proof 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
Proof state after:
case a
n m p : Nat
eqn : succ p ≠ n
c : ¬succ p < n
h' : n < succ p
⊢ succ n ≤ succ p
Theorem: skipInverse_eq
Proof 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'
Proof state after:
case a
n m p : Nat
eqn : succ p ≠ n
c : ¬succ p < n
h' : n < succ p
⊢ succ p ≤ succ p
Theorem: skipInverse_eq
Proof 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
Proof state after:
no goals
Theorem: skip_lt
Proof state before:
k j : Nat
c : j < k
eqn : skip k j = j := skip_below_eq c
⊢ skip k j < j + 2
Tactic:
rw [eqn]
Proof state after:
k j : Nat
c : j < k
eqn : skip k j = j := skip_below_eq c
⊢ j < j + 2
Theorem: skip_lt
Proof state before:
k j : Nat
c : j < k
eqn : skip k j = j := skip_below_eq c
⊢ j < j + 2
Tactic:
apply Nat.le_step
Proof state after:
case h
k j : Nat
c : j < k
eqn : skip k j = j := skip_below_eq c
⊢ succ j ≤ j + 1
Theorem: skip_lt
Proof state before:
case h
k j : Nat
c : j < k
eqn : skip k j = j := skip_below_eq c
⊢ succ j ≤ j + 1
Tactic:
apply Nat.le_refl
Proof state after:
no goals
Theorem: skip_lt
Proof state before:
k j : Nat
c : ¬j < k
eqn : skip k j = j + 1 := skip_not_below_eq k j c
⊢ skip k j < j + 2
Tactic:
rw [eqn]
Proof state after:
k j : Nat
c : ¬j < k
eqn : skip k j = j + 1 := skip_not_below_eq k j c
⊢ j + 1 < j + 2
Theorem: skip_lt
Proof state before:
k j : Nat
c : ¬j < k
eqn : skip k j = j + 1 := skip_not_below_eq k j c
⊢ j + 1 < j + 2
Tactic:
apply Nat.le_refl
Proof state after:
no goals
Theorem: skip_ge
Proof state before:
k j : Nat
c : j < k
eqn : skip k j = j := skip_below_eq c
⊢ j ≤ skip k j
Tactic:
rw [eqn]
Proof state after:
k j : Nat
c : j < k
eqn : skip k j = j := skip_below_eq c
⊢ j ≤ j
Theorem: skip_ge
Proof state before:
k j : Nat
c : j < k
eqn : skip k j = j := skip_below_eq c
⊢ j ≤ j
Tactic:
apply Nat.le_refl
Proof state after:
no goals
Theorem: skip_ge
Proof state before:
k j : Nat
c : ¬j < k
eqn : skip k j = j + 1 := skip_not_below_eq k j c
⊢ j ≤ skip k j
Tactic:
rw [eqn]
Proof state after:
k j : Nat
c : ¬j < k
eqn : skip k j = j + 1 := skip_not_below_eq k j c
⊢ j ≤ j + 1
Theorem: skip_ge
Proof state before:
k j : Nat
c : ¬j < k
eqn : skip k j = j + 1 := skip_not_below_eq k j c
⊢ j ≤ j + 1
Tactic:
apply Nat.le_step
Proof state after:
case h
k j : Nat
c : ¬j < k
eqn : skip k j = j + 1 := skip_not_below_eq k j c
⊢ j ≤ j
Theorem: skip_ge
Proof state before:
case h
k j : Nat
c : ¬j < k
eqn : skip k j = j + 1 := skip_not_below_eq k j c
⊢ j ≤ j
Tactic:
apply Nat.le_refl
Proof state after:
no goals
Theorem: skip_gt_or_arg_below
Proof state before:
k j : Nat
c : ¬j < k
eqn : skip k j = j + 1 := skip_not_below_eq k j c
⊢ j + 1 ≤ skip k j
Tactic:
rw [eqn]
Proof state after:
k j : Nat
c : ¬j < k
eqn : skip k j = j + 1 := skip_not_below_eq k j c
⊢ j + 1 ≤ j + 1
Theorem: skip_gt_or_arg_below
Proof state before:
k j : Nat
c : ¬j < k
eqn : skip k j = j + 1 := skip_not_below_eq k j c
⊢ j + 1 ≤ j + 1
Tactic:
apply Nat.le_refl
Proof state after:
no goals
Theorem: skip_le_succ
Proof state before:
n k j : Nat
⊢ j < n → skip k j < n + 1
Tactic:
intro hyp
Proof state after:
n k j : Nat
hyp : j < n
⊢ skip k j < n + 1
Theorem: skip_le_succ
Proof state before:
n k j : Nat
hyp : j < n
⊢ skip k j < n + 1
Tactic:
apply Nat.le_trans (skip_lt k j)
Proof state after:
n k j : Nat
hyp : j < n
⊢ j + 2 ≤ n + 1
Theorem: skip_le_succ
Proof state before:
n k j : Nat
hyp : j < n
⊢ j + 2 ≤ n + 1
Tactic:
apply Nat.succ_lt_succ
Proof state after:
case a
n k j : Nat
hyp : j < n
⊢ j < n