Theorem: contradiction_insert_none (Saturn/Clause.lean)

State before:
n focus : ℕ
focusLt : focus < n + 1
⊢ FinSeq.insert none n focus focusLt (get' (contradiction n)) = get' (contradiction (n + 1))
Tactic:
apply funext
State after:
case h
n focus : ℕ
focusLt : focus < n + 1
⊢ ∀ (x : ℕ), FinSeq.insert none n focus focusLt (get' (contradiction n)) x = get' (contradiction (n + 1)) x

State before:
case h
n focus : ℕ
focusLt : focus < n + 1
⊢ ∀ (x : ℕ), FinSeq.insert none n focus focusLt (get' (contradiction n)) x = get' (contradiction (n + 1)) x
Tactic:
intro j
State after:
case h
n focus : ℕ
focusLt : focus < n + 1
j : ℕ
⊢ FinSeq.insert none n focus focusLt (get' (contradiction n)) j = get' (contradiction (n + 1)) j

State before:
case h
n focus : ℕ
focusLt : focus < n + 1
j : ℕ
⊢ FinSeq.insert none n focus focusLt (get' (contradiction n)) j = get' (contradiction (n + 1)) j
Tactic:
apply funext
State after:
case h.h
n focus : ℕ
focusLt : focus < n + 1
j : ℕ
⊢ ∀ (x : j < succ n), FinSeq.insert none n focus focusLt (get' (contradiction n)) j x = get' (contradiction (n + 1)) j x

State before:
case h.h
n focus : ℕ
focusLt : focus < n + 1
j : ℕ
⊢ ∀ (x : j < succ n), FinSeq.insert none n focus focusLt (get' (contradiction n)) j x = get' (contradiction (n + 1)) j x
Tactic:
intro jw
State after:
case h.h
n focus : ℕ
focusLt : focus < n + 1
j : ℕ
jw : j < succ n
⊢ FinSeq.insert none n focus focusLt (get' (contradiction n)) j jw = get' (contradiction (n + 1)) j jw

State before:
case h.h
n focus : ℕ
focusLt : focus < n + 1
j : ℕ
jw : j < succ n
⊢ FinSeq.insert none n focus focusLt (get' (contradiction n)) j jw = get' (contradiction (n + 1)) j jw
Tactic:
rw [get'_contradiction]
State after:
case h.h
n focus : ℕ
focusLt : focus < n + 1
j : ℕ
jw : j < succ n
⊢ FinSeq.insert none n focus focusLt (get' (contradiction n)) j jw = none

State before:
case h.h
n focus : ℕ
focusLt : focus < n + 1
j : ℕ
jw : j < succ n
⊢ FinSeq.insert none n focus focusLt (get' (contradiction n)) j jw = none
Tactic:
exact if c : j = focus then
  match focus, c, focusLt with
  | .(j), rfl, .(jw) =>
    by
      rw [insert_at_focus]
else by
  let i := skipInverse focus j c
  let eqn : skip focus i = j := skipInverse_eq focus j c
  let iw := skip_preimage_lt focusLt jw eqn
  match j, eqn, jw with
  | .(skip focus i), rfl, .(skip_le_succ iw) =>
    rw [insert_at_image
        none n focus focusLt ((contradiction n).get')
        i iw, get'_contradiction]
State after:
no goals

State before:
n focus : ℕ
focusLt : focus < n + 1
j : ℕ
jw : j < succ n
c : j = focus
⊢ FinSeq.insert none n j jw (get' (contradiction n)) j jw = none
Tactic:
rw [insert_at_focus]
State after:
no goals

State before:
n focus : ℕ
focusLt : focus < n + 1
j : ℕ
jw : j < succ n
c : ¬j = focus
⊢ FinSeq.insert none n focus focusLt (get' (contradiction n)) j jw = none
Tactic:
let i := skipInverse focus j c
State after:
n focus : ℕ
focusLt : focus < n + 1
j : ℕ
jw : j < succ n
c : ¬j = focus
i : ℕ := skipInverse focus j c
⊢ FinSeq.insert none n focus focusLt (get' (contradiction n)) j jw = none

State before:
n focus : ℕ
focusLt : focus < n + 1
j : ℕ
jw : j < succ n
c : ¬j = focus
i : ℕ := skipInverse focus j c
⊢ FinSeq.insert none n focus focusLt (get' (contradiction n)) j jw = none
Tactic:
let eqn : skip focus i = j := skipInverse_eq focus j c
State after:
n focus : ℕ
focusLt : focus < n + 1
j : ℕ
jw : j < succ n
c : ¬j = focus
i : ℕ := skipInverse focus j c
eqn : skip focus i = j := skipInverse_eq focus j c
⊢ FinSeq.insert none n focus focusLt (get' (contradiction n)) j jw = none

State before:
n focus : ℕ
focusLt : focus < n + 1
j : ℕ
jw : j < succ n
c : ¬j = focus
i : ℕ := skipInverse focus j c
eqn : skip focus i = j := skipInverse_eq focus j c
⊢ FinSeq.insert none n focus focusLt (get' (contradiction n)) j jw = none
Tactic:
let iw := skip_preimage_lt focusLt jw eqn
State after:
n focus : ℕ
focusLt : focus < n + 1
j : ℕ
jw : j < succ n
c : ¬j = focus
i : ℕ := skipInverse focus j c
eqn : skip focus i = j := skipInverse_eq focus j c
iw : i < n := skip_preimage_lt focusLt jw eqn
⊢ FinSeq.insert none n focus focusLt (get' (contradiction n)) j jw = none

State before:
n focus : ℕ
focusLt : focus < n + 1
j : ℕ
jw : j < succ n
c : ¬j = focus
i : ℕ := skipInverse focus j c
eqn : skip focus i = j := skipInverse_eq focus j c
iw : i < n := skip_preimage_lt focusLt jw eqn
⊢ FinSeq.insert none n focus focusLt (get' (contradiction n)) j jw = none
Tactic:
match j, eqn, jw with
| .(skip focus i), rfl, .(skip_le_succ iw) =>
  rw [insert_at_image
      none n focus focusLt ((contradiction n).get')
      i iw, get'_contradiction]
State after:
no goals

State before:
n focus : ℕ
focusLt : focus < n + 1
j : ℕ
jw : j < succ n
c : ¬j = focus
i : ℕ := skipInverse focus j c
eqn : skip focus i = j := skipInverse_eq focus j c
iw : i < n := skip_preimage_lt focusLt jw eqn
⊢ FinSeq.insert none n focus focusLt (get' (contradiction n)) (skip focus i) (_ : skip focus i < n + 1) = none
Tactic:
rw [insert_at_image
    none n focus focusLt ((contradiction n).get')
    i iw, get'_contradiction]
State after:
no goals