Theorem: Nat.Arith₁.sub (Logic/Vorspiel/Arith.lean)

State before:
n : ℕ
i j : Fin n
⊢ Arith₁ fun v => v.get i - v.get j
Tactic:
let F : Vector ℕ (n + 1) → ℕ := fun v =>
  (isEqNat (v.head + v.get j.succ) (v.get i.succ)).or
  ((isLtNat (v.get i.succ) (v.get j.succ)).and (isEqNat v.head 0))
State after:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
⊢ Arith₁ fun v => v.get i - v.get j

State before:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
⊢ Arith₁ fun v => v.get i - v.get j
Tactic:
have : Arith₁ F :=
  (or 0 1).comp₂ _
    ((equal 0 1).comp₂ _ ((add 0 1).comp₂ _ head (proj j.succ)) (proj i.succ))
    ((and 0 1).comp₂ _ ((lt 0 1).comp₂ _ (proj i.succ) (proj j.succ)) ((equal 0 1).comp₂ _ head zero))
State after:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
this : Arith₁ F
⊢ Arith₁ fun v => v.get i - v.get j

State before:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
this : Arith₁ F
⊢ ∀ (i_1 : Vector ℕ n), (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ i_1)))) = (↑fun v => v.get i - v.get j) i_1
Tactic:
intro v
State after:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
this : Arith₁ F
v : Vector ℕ n
⊢ (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v)))) = (↑fun v => v.get i - v.get j) v

State before:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
this : Arith₁ F
v : Vector ℕ n
⊢ (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v)))) = (↑fun v => v.get i - v.get j) v
Tactic:
simp only [head_cons, get_cons_succ, or_pos_iff, isEqNat_pos_iff, and_pos_iff,
  isLtNat_pos_iff, Bool.decide_or, Bool.decide_and, PFun.coe_val, eq_some_iff, mem_rfind,
  mem_some_iff, F]
State after:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
this : Arith₁ F
v : Vector ℕ n
⊢ true =
      (decide (v.get i - v.get j + v.get j = v.get i) || decide (v.get i < v.get j) && decide (v.get i - v.get j = 0)) ∧
    ∀ {m : ℕ},
      m < v.get i - v.get j → false = (decide (m + v.get j = v.get i) || decide (v.get i < v.get j) && decide (m = 0))

State before:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
this : Arith₁ F
v : Vector ℕ n
⊢ true =
      (decide (v.get i - v.get j + v.get j = v.get i) || decide (v.get i < v.get j) && decide (v.get i - v.get j = 0)) ∧
    ∀ {m : ℕ},
      m < v.get i - v.get j → false = (decide (m + v.get j = v.get i) || decide (v.get i < v.get j) && decide (m = 0))
Tactic:
constructor
State after:
case left
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
this : Arith₁ F
v : Vector ℕ n
⊢ true =
    (decide (v.get i - v.get j + v.get j = v.get i) || decide (v.get i < v.get j) && decide (v.get i - v.get j = 0))

case right
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
this : Arith₁ F
v : Vector ℕ n
⊢ ∀ {m : ℕ},
    m < v.get i - v.get j → false = (decide (m + v.get j = v.get i) || decide (v.get i < v.get j) && decide (m = 0))

State before:
case left
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
this : Arith₁ F
v : Vector ℕ n
⊢ true =
    (decide (v.get i - v.get j + v.get j = v.get i) || decide (v.get i < v.get j) && decide (v.get i - v.get j = 0))
Tactic:
symm
State after:
case left
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
this : Arith₁ F
v : Vector ℕ n
⊢ (decide (v.get i - v.get j + v.get j = v.get i) || decide (v.get i < v.get j) && decide (v.get i - v.get j = 0)) =
    true

State before:
case left
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
this : Arith₁ F
v : Vector ℕ n
⊢ (decide (v.get i - v.get j + v.get j = v.get i) || decide (v.get i < v.get j) && decide (v.get i - v.get j = 0)) =
    true
Tactic:
simp
State after:
case left
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
this : Arith₁ F
v : Vector ℕ n
⊢ v.get i - v.get j + v.get j = v.get i ∨ v.get i < v.get j ∧ v.get i - v.get j = 0

State before:
case left
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
this : Arith₁ F
v : Vector ℕ n
⊢ v.get i - v.get j + v.get j = v.get i ∨ v.get i < v.get j ∧ v.get i - v.get j = 0
Tactic:
have : v.get i < v.get j ∨ v.get j ≤ v.get i := Nat.lt_or_ge _ _
State after:
case left
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
this✝ : Arith₁ F
v : Vector ℕ n
this : v.get i < v.get j ∨ v.get j ≤ v.get i
⊢ v.get i - v.get j + v.get j = v.get i ∨ v.get i < v.get j ∧ v.get i - v.get j = 0

State before:
case left
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
this✝ : Arith₁ F
v : Vector ℕ n
this : v.get i < v.get j ∨ v.get j ≤ v.get i
⊢ v.get i - v.get j + v.get j = v.get i ∨ v.get i < v.get j ∧ v.get i - v.get j = 0
Tactic:
rcases this with (hv | hv)
State after:
case left.inl
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
this : Arith₁ F
v : Vector ℕ n
hv : v.get i < v.get j
⊢ v.get i - v.get j + v.get j = v.get i ∨ v.get i < v.get j ∧ v.get i - v.get j = 0

case left.inr
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
this : Arith₁ F
v : Vector ℕ n
hv : v.get j ≤ v.get i
⊢ v.get i - v.get j + v.get j = v.get i ∨ v.get i < v.get j ∧ v.get i - v.get j = 0

State before:
case left.inl
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
this : Arith₁ F
v : Vector ℕ n
hv : v.get i < v.get j
⊢ v.get i - v.get j + v.get j = v.get i ∨ v.get i < v.get j ∧ v.get i - v.get j = 0
Tactic:
right
State after:
case left.inl.h
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
this : Arith₁ F
v : Vector ℕ n
hv : v.get i < v.get j
⊢ v.get i < v.get j ∧ v.get i - v.get j = 0

State before:
case left.inl.h
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
this : Arith₁ F
v : Vector ℕ n
hv : v.get i < v.get j
⊢ v.get i < v.get j ∧ v.get i - v.get j = 0
Tactic:
exact ⟨hv, Nat.sub_eq_zero_of_le (Nat.le_of_lt hv)⟩
State after:
no goals

State before:
case left.inr
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
this : Arith₁ F
v : Vector ℕ n
hv : v.get j ≤ v.get i
⊢ v.get i - v.get j + v.get j = v.get i ∨ v.get i < v.get j ∧ v.get i - v.get j = 0
Tactic:
left
State after:
case left.inr.h
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
this : Arith₁ F
v : Vector ℕ n
hv : v.get j ≤ v.get i
⊢ v.get i - v.get j + v.get j = v.get i

State before:
case left.inr.h
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
this : Arith₁ F
v : Vector ℕ n
hv : v.get j ≤ v.get i
⊢ v.get i - v.get j + v.get j = v.get i
Tactic:
exact Nat.sub_add_cancel hv
State after:
no goals

State before:
case right
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
this : Arith₁ F
v : Vector ℕ n
⊢ ∀ {m : ℕ},
    m < v.get i - v.get j → false = (decide (m + v.get j = v.get i) || decide (v.get i < v.get j) && decide (m = 0))
Tactic:
intro m hm
State after:
case right
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
this : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i - v.get j
⊢ false = (decide (m + v.get j = v.get i) || decide (v.get i < v.get j) && decide (m = 0))

State before:
case right
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
this : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i - v.get j
⊢ false = (decide (m + v.get j = v.get i) || decide (v.get i < v.get j) && decide (m = 0))
Tactic:
symm
State after:
case right
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
this : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i - v.get j
⊢ (decide (m + v.get j = v.get i) || decide (v.get i < v.get j) && decide (m = 0)) = false

State before:
case right
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
this : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i - v.get j
⊢ (decide (m + v.get j = v.get i) || decide (v.get i < v.get j) && decide (m = 0)) = false
Tactic:
simp only [Bool.or_eq_false_eq_eq_false_and_eq_false,
  decide_eq_false_iff_not, Bool.and_eq_false_eq_eq_false_or_eq_false, not_lt]
State after:
case right
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
this : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i - v.get j
⊢ ¬m + v.get j = v.get i ∧ (v.get j ≤ v.get i ∨ ¬m = 0)

State before:
case right
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
this : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i - v.get j
⊢ ¬m + v.get j = v.get i ∧ (v.get j ≤ v.get i ∨ ¬m = 0)
Tactic:
have : m + v.get j < v.get i := add_lt_of_lt_sub hm
State after:
case right
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
this✝ : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i - v.get j
this : m + v.get j < v.get i
⊢ ¬m + v.get j = v.get i ∧ (v.get j ≤ v.get i ∨ ¬m = 0)

State before:
case right
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
this✝ : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i - v.get j
this : m + v.get j < v.get i
⊢ ¬m + v.get j = v.get i ∧ (v.get j ≤ v.get i ∨ ¬m = 0)
Tactic:
exact ⟨ne_of_lt this, by left; exact le_trans le_add_self (le_of_lt this)⟩
State after:
no goals

State before:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
this✝ : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i - v.get j
this : m + v.get j < v.get i
⊢ v.get j ≤ v.get i ∨ ¬m = 0
Tactic:
left
State after:
case h
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
this✝ : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i - v.get j
this : m + v.get j < v.get i
⊢ v.get j ≤ v.get i

State before:
case h
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
this✝ : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i - v.get j
this : m + v.get j < v.get i
⊢ v.get j ≤ v.get i
Tactic:
exact le_trans le_add_self (le_of_lt this)
State after:
no goals