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

State before:
n : ℕ
i j : Fin n
⊢ Arith₁ fun v => (v.get i).isDvdNat (v.get j)
Tactic:
have hr : @Arith₁ (n + 1) (fun v =>
  (isEqNat (v.head * (v.get i.succ)) (v.get j.succ)).or (isLtNat (v.get j.succ) v.head)) :=
  (or 0 1).comp₂ _
    ((equal 0 1).comp₂ _ ((mul 0 1).comp₂ _ head (proj i.succ)) (proj j.succ))
    ((lt 0 1).comp₂ _ (proj j.succ) head)
State after:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
⊢ Arith₁ fun v => (v.get i).isDvdNat (v.get j)

State before:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
⊢ Arith₁ fun v => (v.get i).isDvdNat (v.get j)
Tactic:
have : @Arith₁ (n + 1) (fun v => isLeNat v.head (v.tail.get j)) :=
  (le 0 1).comp₂ _ head ((proj j.succ).of_eq <| by simp)
State after:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
⊢ Arith₁ fun v => (v.get i).isDvdNat (v.get j)

State before:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
⊢ Arith₁ fun v => (v.get i).isDvdNat (v.get j)
Tactic:
have := ArithPart₁.map (fun v x => isLeNat x (v.get j)) this (ArithPart₁.rfindPos hr)
State after:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
⊢ Arith₁ fun v => (v.get i).isDvdNat (v.get j)

State before:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
⊢ ∀ (i : Vector ℕ n.succ), i.get j.succ = i.tail.get j
Tactic:
simp
State after:
no goals

State before:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
⊢ ∀ (i_1 : Vector ℕ n),
    Part.map ((fun v x => x.isLeNat (v.get j)) i_1)
        (rfind fun n_1 =>
          Part.some
            (decide
              (0 <
                (((n_1 ::ᵥ i_1).head * (n_1 ::ᵥ i_1).get i.succ).isEqNat ((n_1 ::ᵥ i_1).get j.succ)).or
                  (((n_1 ::ᵥ i_1).get j.succ).isLtNat (n_1 ::ᵥ i_1).head)))) =
      (↑fun v => (v.get i).isDvdNat (v.get j)) i_1
Tactic:
intro v
State after:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
⊢ Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head)))) =
    (↑fun v => (v.get i).isDvdNat (v.get j)) v

State before:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
⊢ Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head)))) =
    (↑fun v => (v.get i).isDvdNat (v.get j)) v
Tactic:
simp only [head_cons, get_cons_succ, or_pos_iff, isEqNat_pos_iff, isLtNat_pos_iff,
  Bool.decide_or, isDvdNat, PFun.coe_val, eq_some_iff, mem_map_iff, mem_rfind, mem_some_iff]
State after:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
⊢ ∃ a,
    (true = (decide (a * v.get i = v.get j) || decide (v.get j < a)) ∧
        ∀ {m : ℕ}, m < a → false = (decide (m * v.get i = v.get j) || decide (v.get j < m))) ∧
      a.isLeNat (v.get j) = if v.get i ∣ v.get j then 1 else 0

State before:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
⊢ ∃ a,
    (true = (decide (a * v.get i = v.get j) || decide (v.get j < a)) ∧
        ∀ {m : ℕ}, m < a → false = (decide (m * v.get i = v.get j) || decide (v.get j < m))) ∧
      a.isLeNat (v.get j) = if v.get i ∣ v.get j then 1 else 0
Tactic:
by_cases hv : v.get i ∣ v.get j
State after:
case pos
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : v.get i ∣ v.get j
⊢ ∃ a,
    (true = (decide (a * v.get i = v.get j) || decide (v.get j < a)) ∧
        ∀ {m : ℕ}, m < a → false = (decide (m * v.get i = v.get j) || decide (v.get j < m))) ∧
      a.isLeNat (v.get j) = if v.get i ∣ v.get j then 1 else 0

case neg
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : ¬v.get i ∣ v.get j
⊢ ∃ a,
    (true = (decide (a * v.get i = v.get j) || decide (v.get j < a)) ∧
        ∀ {m : ℕ}, m < a → false = (decide (m * v.get i = v.get j) || decide (v.get j < m))) ∧
      a.isLeNat (v.get j) = if v.get i ∣ v.get j then 1 else 0

State before:
case pos
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : v.get i ∣ v.get j
⊢ ∃ a,
    (true = (decide (a * v.get i = v.get j) || decide (v.get j < a)) ∧
        ∀ {m : ℕ}, m < a → false = (decide (m * v.get i = v.get j) || decide (v.get j < m))) ∧
      a.isLeNat (v.get j) = if v.get i ∣ v.get j then 1 else 0
Tactic:
simp only [hv, ↓reduceIte]
State after:
case pos
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : v.get i ∣ v.get j
⊢ ∃ a,
    (true = (decide (a * v.get i = v.get j) || decide (v.get j < a)) ∧
        ∀ {m : ℕ}, m < a → false = (decide (m * v.get i = v.get j) || decide (v.get j < m))) ∧
      a.isLeNat (v.get j) = 1

State before:
case pos
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : v.get i ∣ v.get j
⊢ ∃ a,
    (true = (decide (a * v.get i = v.get j) || decide (v.get j < a)) ∧
        ∀ {m : ℕ}, m < a → false = (decide (m * v.get i = v.get j) || decide (v.get j < m))) ∧
      a.isLeNat (v.get j) = 1
Tactic:
rcases least_number _ hv with ⟨k, hk, hkm⟩
State after:
case pos.intro.intro
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : v.get i ∣ v.get j
k : ℕ
hk : v.get j = v.get i * k
hkm : ∀ z < k, ¬v.get j = v.get i * z
⊢ ∃ a,
    (true = (decide (a * v.get i = v.get j) || decide (v.get j < a)) ∧
        ∀ {m : ℕ}, m < a → false = (decide (m * v.get i = v.get j) || decide (v.get j < m))) ∧
      a.isLeNat (v.get j) = 1

State before:
case pos.intro.intro
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : v.get i ∣ v.get j
k : ℕ
hk : v.get j = v.get i * k
hkm : ∀ z < k, ¬v.get j = v.get i * z
hkvj : k ≤ v.get j
⊢ ∃ a,
    (true = (decide (a * v.get i = v.get j) || decide (v.get j < a)) ∧
        ∀ {m : ℕ}, m < a → false = (decide (m * v.get i = v.get j) || decide (v.get j < m))) ∧
      a.isLeNat (v.get j) = 1
Tactic:
refine ⟨k,
  ⟨by symm; simp; left; simp[hk, mul_comm],
   by intro m hm; symm; simp[mul_comm m, Ne.symm (hkm m hm), le_of_lt (lt_of_lt_of_le hm hkvj)]⟩,
  by simp[isLeNat, hkvj]⟩
State after:
no goals

State before:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : v.get i ∣ v.get j
k : ℕ
hk : v.get j = v.get i * k
hkm : ∀ z < k, ¬v.get j = v.get i * z
⊢ k ≤ v.get j
Tactic:
by_cases hkz : k = 0
State after:
case pos
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : v.get i ∣ v.get j
k : ℕ
hk : v.get j = v.get i * k
hkm : ∀ z < k, ¬v.get j = v.get i * z
hkz : k = 0
⊢ k ≤ v.get j

case neg
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : v.get i ∣ v.get j
k : ℕ
hk : v.get j = v.get i * k
hkm : ∀ z < k, ¬v.get j = v.get i * z
hkz : ¬k = 0
⊢ k ≤ v.get j

State before:
case pos
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : v.get i ∣ v.get j
k : ℕ
hk : v.get j = v.get i * k
hkm : ∀ z < k, ¬v.get j = v.get i * z
hkz : k = 0
⊢ k ≤ v.get j
Tactic:
simp[hkz]
State after:
no goals

State before:
case neg
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : v.get i ∣ v.get j
k : ℕ
hk : v.get j = v.get i * k
hkm : ∀ z < k, ¬v.get j = v.get i * z
hkz : ¬k = 0
⊢ k ≤ v.get j
Tactic:
rw[hk]
State after:
case neg
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : v.get i ∣ v.get j
k : ℕ
hk : v.get j = v.get i * k
hkm : ∀ z < k, ¬v.get j = v.get i * z
hkz : ¬k = 0
⊢ k ≤ v.get i * k

State before:
case neg
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : v.get i ∣ v.get j
k : ℕ
hk : v.get j = v.get i * k
hkm : ∀ z < k, ¬v.get j = v.get i * z
hkz : ¬k = 0
⊢ k ≤ v.get i * k
Tactic:
exact Nat.le_mul_of_pos_left _ (Nat.zero_lt_of_ne_zero $ fun hvi => by
simp[hvi] at hk
have : v.get j ≠ 0 := hkm 0 (Nat.pos_of_ne_zero hkz)
contradiction)
State after:
no goals

State before:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : v.get i ∣ v.get j
k : ℕ
hk : v.get j = v.get i * k
hkm : ∀ z < k, ¬v.get j = v.get i * z
hkz : ¬k = 0
hvi : v.get i = 0
⊢ False
Tactic:
simp[hvi] at hk
State after:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : v.get i ∣ v.get j
k : ℕ
hkm : ∀ z < k, ¬v.get j = v.get i * z
hkz : ¬k = 0
hvi : v.get i = 0
hk : v.get j = 0
⊢ False

State before:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : v.get i ∣ v.get j
k : ℕ
hkm : ∀ z < k, ¬v.get j = v.get i * z
hkz : ¬k = 0
hvi : v.get i = 0
hk : v.get j = 0
⊢ False
Tactic:
have : v.get j ≠ 0 := hkm 0 (Nat.pos_of_ne_zero hkz)
State after:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝¹ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this✝ :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : v.get i ∣ v.get j
k : ℕ
hkm : ∀ z < k, ¬v.get j = v.get i * z
hkz : ¬k = 0
hvi : v.get i = 0
hk : v.get j = 0
this : v.get j ≠ 0
⊢ False

State before:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝¹ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this✝ :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : v.get i ∣ v.get j
k : ℕ
hkm : ∀ z < k, ¬v.get j = v.get i * z
hkz : ¬k = 0
hvi : v.get i = 0
hk : v.get j = 0
this : v.get j ≠ 0
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : v.get i ∣ v.get j
k : ℕ
hk : v.get j = v.get i * k
hkm : ∀ z < k, ¬v.get j = v.get i * z
hkvj : k ≤ v.get j
⊢ true = (decide (k * v.get i = v.get j) || decide (v.get j < k))
Tactic:
symm
State after:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : v.get i ∣ v.get j
k : ℕ
hk : v.get j = v.get i * k
hkm : ∀ z < k, ¬v.get j = v.get i * z
hkvj : k ≤ v.get j
⊢ (decide (k * v.get i = v.get j) || decide (v.get j < k)) = true

State before:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : v.get i ∣ v.get j
k : ℕ
hk : v.get j = v.get i * k
hkm : ∀ z < k, ¬v.get j = v.get i * z
hkvj : k ≤ v.get j
⊢ (decide (k * v.get i = v.get j) || decide (v.get j < k)) = true
Tactic:
simp
State after:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : v.get i ∣ v.get j
k : ℕ
hk : v.get j = v.get i * k
hkm : ∀ z < k, ¬v.get j = v.get i * z
hkvj : k ≤ v.get j
⊢ k * v.get i = v.get j ∨ v.get j < k

State before:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : v.get i ∣ v.get j
k : ℕ
hk : v.get j = v.get i * k
hkm : ∀ z < k, ¬v.get j = v.get i * z
hkvj : k ≤ v.get j
⊢ k * v.get i = v.get j ∨ v.get j < k
Tactic:
left
State after:
case h
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : v.get i ∣ v.get j
k : ℕ
hk : v.get j = v.get i * k
hkm : ∀ z < k, ¬v.get j = v.get i * z
hkvj : k ≤ v.get j
⊢ k * v.get i = v.get j

State before:
case h
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : v.get i ∣ v.get j
k : ℕ
hk : v.get j = v.get i * k
hkm : ∀ z < k, ¬v.get j = v.get i * z
hkvj : k ≤ v.get j
⊢ k * v.get i = v.get j
Tactic:
simp[hk, mul_comm]
State after:
no goals

State before:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : v.get i ∣ v.get j
k : ℕ
hk : v.get j = v.get i * k
hkm : ∀ z < k, ¬v.get j = v.get i * z
hkvj : k ≤ v.get j
⊢ ∀ {m : ℕ}, m < k → false = (decide (m * v.get i = v.get j) || decide (v.get j < m))
Tactic:
intro m hm
State after:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : v.get i ∣ v.get j
k : ℕ
hk : v.get j = v.get i * k
hkm : ∀ z < k, ¬v.get j = v.get i * z
hkvj : k ≤ v.get j
m : ℕ
hm : m < k
⊢ false = (decide (m * v.get i = v.get j) || decide (v.get j < m))

State before:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : v.get i ∣ v.get j
k : ℕ
hk : v.get j = v.get i * k
hkm : ∀ z < k, ¬v.get j = v.get i * z
hkvj : k ≤ v.get j
m : ℕ
hm : m < k
⊢ false = (decide (m * v.get i = v.get j) || decide (v.get j < m))
Tactic:
symm
State after:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : v.get i ∣ v.get j
k : ℕ
hk : v.get j = v.get i * k
hkm : ∀ z < k, ¬v.get j = v.get i * z
hkvj : k ≤ v.get j
m : ℕ
hm : m < k
⊢ (decide (m * v.get i = v.get j) || decide (v.get j < m)) = false

State before:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : v.get i ∣ v.get j
k : ℕ
hk : v.get j = v.get i * k
hkm : ∀ z < k, ¬v.get j = v.get i * z
hkvj : k ≤ v.get j
m : ℕ
hm : m < k
⊢ (decide (m * v.get i = v.get j) || decide (v.get j < m)) = false
Tactic:
simp[mul_comm m, Ne.symm (hkm m hm), le_of_lt (lt_of_lt_of_le hm hkvj)]
State after:
no goals

State before:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : v.get i ∣ v.get j
k : ℕ
hk : v.get j = v.get i * k
hkm : ∀ z < k, ¬v.get j = v.get i * z
hkvj : k ≤ v.get j
⊢ k.isLeNat (v.get j) = 1
Tactic:
simp[isLeNat, hkvj]
State after:
no goals

State before:
case neg
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : ¬v.get i ∣ v.get j
⊢ ∃ a,
    (true = (decide (a * v.get i = v.get j) || decide (v.get j < a)) ∧
        ∀ {m : ℕ}, m < a → false = (decide (m * v.get i = v.get j) || decide (v.get j < m))) ∧
      a.isLeNat (v.get j) = if v.get i ∣ v.get j then 1 else 0
Tactic:
simp only [hv, ↓reduceIte]
State after:
case neg
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : ¬v.get i ∣ v.get j
⊢ ∃ a,
    (true = (decide (a * v.get i = v.get j) || decide (v.get j < a)) ∧
        ∀ {m : ℕ}, m < a → false = (decide (m * v.get i = v.get j) || decide (v.get j < m))) ∧
      a.isLeNat (v.get j) = 0

State before:
case neg
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : ¬v.get i ∣ v.get j
⊢ ∃ a,
    (true = (decide (a * v.get i = v.get j) || decide (v.get j < a)) ∧
        ∀ {m : ℕ}, m < a → false = (decide (m * v.get i = v.get j) || decide (v.get j < m))) ∧
      a.isLeNat (v.get j) = 0
Tactic:
exact ⟨v.get j + 1, ⟨by symm; simp, by
  intro m hm; symm; simp[lt_succ.mp hm]; intro A
  have : v.get i ∣ v.get j := by rw[←A]; exact Nat.dvd_mul_left (Vector.get v i) m
  contradiction⟩, by simp [isLeNat]⟩
State after:
no goals

State before:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : ¬v.get i ∣ v.get j
⊢ true = (decide ((v.get j + 1) * v.get i = v.get j) || decide (v.get j < v.get j + 1))
Tactic:
symm
State after:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : ¬v.get i ∣ v.get j
⊢ (decide ((v.get j + 1) * v.get i = v.get j) || decide (v.get j < v.get j + 1)) = true

State before:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : ¬v.get i ∣ v.get j
⊢ (decide ((v.get j + 1) * v.get i = v.get j) || decide (v.get j < v.get j + 1)) = true
Tactic:
simp
State after:
no goals

State before:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : ¬v.get i ∣ v.get j
⊢ ∀ {m : ℕ}, m < v.get j + 1 → false = (decide (m * v.get i = v.get j) || decide (v.get j < m))
Tactic:
intro m hm
State after:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : ¬v.get i ∣ v.get j
m : ℕ
hm : m < v.get j + 1
⊢ false = (decide (m * v.get i = v.get j) || decide (v.get j < m))

State before:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : ¬v.get i ∣ v.get j
m : ℕ
hm : m < v.get j + 1
⊢ false = (decide (m * v.get i = v.get j) || decide (v.get j < m))
Tactic:
symm
State after:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : ¬v.get i ∣ v.get j
m : ℕ
hm : m < v.get j + 1
⊢ (decide (m * v.get i = v.get j) || decide (v.get j < m)) = false

State before:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : ¬v.get i ∣ v.get j
m : ℕ
hm : m < v.get j + 1
⊢ (decide (m * v.get i = v.get j) || decide (v.get j < m)) = false
Tactic:
simp[lt_succ.mp hm]
State after:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : ¬v.get i ∣ v.get j
m : ℕ
hm : m < v.get j + 1
⊢ ¬m * v.get i = v.get j

State before:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : ¬v.get i ∣ v.get j
m : ℕ
hm : m < v.get j + 1
⊢ ¬m * v.get i = v.get j
Tactic:
intro A
State after:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : ¬v.get i ∣ v.get j
m : ℕ
hm : m < v.get j + 1
A : m * v.get i = v.get j
⊢ False

State before:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : ¬v.get i ∣ v.get j
m : ℕ
hm : m < v.get j + 1
A : m * v.get i = v.get j
⊢ False
Tactic:
have : v.get i ∣ v.get j := by rw[←A]; exact Nat.dvd_mul_left (Vector.get v i) m
State after:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝¹ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this✝ :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : ¬v.get i ∣ v.get j
m : ℕ
hm : m < v.get j + 1
A : m * v.get i = v.get j
this : v.get i ∣ v.get j
⊢ False

State before:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝¹ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this✝ :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : ¬v.get i ∣ v.get j
m : ℕ
hm : m < v.get j + 1
A : m * v.get i = v.get j
this : v.get i ∣ v.get j
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : ¬v.get i ∣ v.get j
m : ℕ
hm : m < v.get j + 1
A : m * v.get i = v.get j
⊢ v.get i ∣ v.get j
Tactic:
rw[←A]
State after:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : ¬v.get i ∣ v.get j
m : ℕ
hm : m < v.get j + 1
A : m * v.get i = v.get j
⊢ v.get i ∣ m * v.get i

State before:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : ¬v.get i ∣ v.get j
m : ℕ
hm : m < v.get j + 1
A : m * v.get i = v.get j
⊢ v.get i ∣ m * v.get i
Tactic:
exact Nat.dvd_mul_left (Vector.get v i) m
State after:
no goals

State before:
n : ℕ
i j : Fin n
hr : Arith₁ fun v => ((v.head * v.get i.succ).isEqNat (v.get j.succ)).or ((v.get j.succ).isLtNat v.head)
this✝ : Arith₁ fun v => v.head.isLeNat (v.tail.get j)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isLeNat (v.get j)) v)
      (rfind fun n_1 =>
        Part.some
          (decide
            (0 <
              (((n_1 ::ᵥ v).head * (n_1 ::ᵥ v).get i.succ).isEqNat ((n_1 ::ᵥ v).get j.succ)).or
                (((n_1 ::ᵥ v).get j.succ).isLtNat (n_1 ::ᵥ v).head))))
v : Vector ℕ n
hv : ¬v.get i ∣ v.get j
⊢ (v.get j + 1).isLeNat (v.get j) = 0
Tactic:
simp [isLeNat]
State after:
no goals