internlm/Lean-Github huggingface dataset:
Theorem: Nat.Arith₁.dvd
Proof 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
Proof 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
Theorem: Nat.Arith₁.dvd
Proof 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)
Proof 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
Theorem: Nat.Arith₁.dvd
Proof 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
Proof state after:
no goals
Theorem: Nat.Arith₁.dvd
Proof 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
Proof 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
Theorem: Nat.Arith₁.dvd
Proof 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
Proof 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
Theorem: Nat.Arith₁.dvd
Proof 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
Proof 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
Theorem: Nat.Arith₁.dvd
Proof 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]
Proof state after:
no goals
Theorem: Nat.Arith₁.dvd
Proof 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
Proof 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))
Theorem: Nat.Arith₁.dvd
Proof 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
Proof 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
Theorem: Nat.Arith₁.dvd
Proof 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)]
Proof state after:
no goals
Theorem: Nat.Arith₁.dvd
Proof 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]
Proof state after:
no goals
Theorem: Nat.Arith₁.dvd
Proof 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]
Proof 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
Theorem: Nat.Arith₁.dvd
Proof 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]⟩
Proof state after:
no goals
Theorem: Nat.Arith₁.dvd
Proof 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
Proof 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
Theorem: Nat.Arith₁.dvd
Proof 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
Proof state after:
no goals
Theorem: Nat.Arith₁.dvd
Proof 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
Proof 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))
Theorem: Nat.Arith₁.dvd
Proof 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
Proof 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
Theorem: Nat.Arith₁.dvd
Proof 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]
Proof 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
Theorem: Nat.Arith₁.dvd
Proof 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
Proof 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