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
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
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
this : v.get i ∣ v.get j
⊢ 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
A : m * v.get i = v.get j
this : v.get i ∣ v.get j
⊢ 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
m : ℕ
hm : m < v.get j + 1
A : m * v.get i = v.get j
⊢ v.get i ∣ v.get j
Tactic:
rw[←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
⊢ v.get i ∣ m * v.get i
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
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
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
⊢ (v.get j + 1).isLeNat (v.get j) = 0
Tactic:
simp [isLeNat]
Proof state after:
no goals
Theorem: Nat.Arith₁.rem
Proof state before:
n : ℕ
i j : Fin n
⊢ Arith₁ fun v => v.get i % v.get j
Tactic:
let F : Vector ℕ (n + 1) → ℕ := fun v => isDvdNat (v.get j.succ) (v.get i.succ - v.head)
Proof state after:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (v.get j.succ).isDvdNat (v.get i.succ - v.head)
⊢ Arith₁ fun v => v.get i % v.get j
Theorem: Nat.Arith₁.rem
Proof state before:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (v.get j.succ).isDvdNat (v.get i.succ - v.head)
⊢ Arith₁ fun v => v.get i % v.get j
Tactic:
have : Arith₁ F :=
  (dvd 0 1).comp₂ _ (proj j.succ) ((sub 0 1).comp₂ _ (proj i.succ) head)
Proof state after:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (v.get j.succ).isDvdNat (v.get i.succ - v.head)
this : Arith₁ F
⊢ Arith₁ fun v => v.get i % v.get j
Theorem: Nat.Arith₁.rem
Proof state before:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (v.get j.succ).isDvdNat (v.get i.succ - v.head)
this : Arith₁ F
⊢ Arith₁ fun v => v.get i % v.get j
Tactic:
exact (ArithPart₁.rfindPos this).of_eq <| by
  intro v; simp [F, Part.eq_some_iff, Nat.dvd_sub_mod]
  intro m hm A
  have hmvi : m < v.get i := lt_of_lt_of_le hm <| Nat.mod_le (v.get i) (v.get j)
  have hsub : v.get j ∣ v.get i % v.get j - m := by
    have : v.get i - m - (v.get i - v.get i % v.get j) = v.get i % v.get j - m := by
      rw[Nat.sub_eq_iff_eq_add (Nat.sub_le_sub_left (le_of_lt hm) _), Nat.sub_eq_iff_eq_add (le_of_lt hmvi),
        ←Nat.sub_add_comm (le_of_lt hm), Nat.add_sub_of_le (Nat.mod_le (v.get i) (v.get j)),
        Nat.sub_add_cancel (le_of_lt hmvi)]
    rw[←this]
    exact Nat.dvd_sub (Nat.sub_le_sub_left (le_of_lt hm) _) A (@Nat.dvd_sub_mod (v.get j) (v.get i))
  have hpos : 0 < v.get i % v.get j - m := Nat.lt_sub_of_add_lt (by simpa using hm)
  have : v.get i % v.get j - m < v.get j := by
    have : v.get i % v.get j < v.get j :=
      Nat.mod_lt _ (Nat.pos_of_ne_zero $ fun h => (Nat.not_lt.mpr (by simpa [Nat.sub_eq_zero_iff_le, h] using hsub)) hmvi)
    exact lt_of_le_of_lt (sub_le _ _) this
  have : ¬v.get j ∣ v.get i % v.get j - m := Nat.not_dvd_of_pos_of_lt hpos this
  contradiction
Proof state after:
no goals
Theorem: Nat.Arith₁.rem
Proof state before:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (v.get j.succ).isDvdNat (v.get i.succ - v.head)
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
Proof state after:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (v.get j.succ).isDvdNat (v.get i.succ - v.head)
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
Theorem: Nat.Arith₁.rem
Proof state before:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (v.get j.succ).isDvdNat (v.get i.succ - v.head)
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 [F, Part.eq_some_iff, Nat.dvd_sub_mod]
Proof state after:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (v.get j.succ).isDvdNat (v.get i.succ - v.head)
this : Arith₁ F
v : Vector ℕ n
⊢ ∀ {m : ℕ}, m < v.get i % v.get j → ¬v.get j ∣ v.get i - m
Theorem: Nat.Arith₁.rem
Proof state before:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (v.get j.succ).isDvdNat (v.get i.succ - v.head)
this : Arith₁ F
v : Vector ℕ n
⊢ ∀ {m : ℕ}, m < v.get i % v.get j → ¬v.get j ∣ v.get i - m
Tactic:
intro m hm A
Proof state after:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (v.get j.succ).isDvdNat (v.get i.succ - v.head)
this : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i % v.get j
A : v.get j ∣ v.get i - m
⊢ False
Theorem: Nat.Arith₁.rem
Proof state before:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (v.get j.succ).isDvdNat (v.get i.succ - v.head)
this : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i % v.get j
A : v.get j ∣ v.get i - m
⊢ False
Tactic:
have hmvi : m < v.get i := lt_of_lt_of_le hm <| Nat.mod_le (v.get i) (v.get j)
Proof state after:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (v.get j.succ).isDvdNat (v.get i.succ - v.head)
this : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i % v.get j
A : v.get j ∣ v.get i - m
hmvi : m < v.get i
⊢ False
Theorem: Nat.Arith₁.rem
Proof state before:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (v.get j.succ).isDvdNat (v.get i.succ - v.head)
this : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i % v.get j
A : v.get j ∣ v.get i - m
hmvi : m < v.get i
⊢ False
Tactic:
have hsub : v.get j ∣ v.get i % v.get j - m := by
  have : v.get i - m - (v.get i - v.get i % v.get j) = v.get i % v.get j - m := by
    rw[Nat.sub_eq_iff_eq_add (Nat.sub_le_sub_left (le_of_lt hm) _), Nat.sub_eq_iff_eq_add (le_of_lt hmvi),
      ←Nat.sub_add_comm (le_of_lt hm), Nat.add_sub_of_le (Nat.mod_le (v.get i) (v.get j)),
      Nat.sub_add_cancel (le_of_lt hmvi)]
  rw[←this]
  exact Nat.dvd_sub (Nat.sub_le_sub_left (le_of_lt hm) _) A (@Nat.dvd_sub_mod (v.get j) (v.get i))
Proof state after:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (v.get j.succ).isDvdNat (v.get i.succ - v.head)
this : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i % v.get j
A : v.get j ∣ v.get i - m
hmvi : m < v.get i
hsub : v.get j ∣ v.get i % v.get j - m
⊢ False
Theorem: Nat.Arith₁.rem
Proof state before:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (v.get j.succ).isDvdNat (v.get i.succ - v.head)
this : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i % v.get j
A : v.get j ∣ v.get i - m
hmvi : m < v.get i
hsub : v.get j ∣ v.get i % v.get j - m
⊢ False
Tactic:
have hpos : 0 < v.get i % v.get j - m := Nat.lt_sub_of_add_lt (by simpa using hm)
Proof state after:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (v.get j.succ).isDvdNat (v.get i.succ - v.head)
this : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i % v.get j
A : v.get j ∣ v.get i - m
hmvi : m < v.get i
hsub : v.get j ∣ v.get i % v.get j - m
hpos : 0 < v.get i % v.get j - m
⊢ False
Theorem: Nat.Arith₁.rem
Proof state before:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (v.get j.succ).isDvdNat (v.get i.succ - v.head)
this : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i % v.get j
A : v.get j ∣ v.get i - m
hmvi : m < v.get i
hsub : v.get j ∣ v.get i % v.get j - m
hpos : 0 < v.get i % v.get j - m
⊢ False
Tactic:
have : v.get i % v.get j - m < v.get j := by
  have : v.get i % v.get j < v.get j :=
    Nat.mod_lt _ (Nat.pos_of_ne_zero $ fun h => (Nat.not_lt.mpr (by simpa [Nat.sub_eq_zero_iff_le, h] using hsub)) hmvi)
  exact lt_of_le_of_lt (sub_le _ _) this
Proof state after:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (v.get j.succ).isDvdNat (v.get i.succ - v.head)
this✝ : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i % v.get j
A : v.get j ∣ v.get i - m
hmvi : m < v.get i
hsub : v.get j ∣ v.get i % v.get j - m
hpos : 0 < v.get i % v.get j - m
this : v.get i % v.get j - m < v.get j
⊢ False
Theorem: Nat.Arith₁.rem
Proof state before:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (v.get j.succ).isDvdNat (v.get i.succ - v.head)
this✝ : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i % v.get j
A : v.get j ∣ v.get i - m
hmvi : m < v.get i
hsub : v.get j ∣ v.get i % v.get j - m
hpos : 0 < v.get i % v.get j - m
this : v.get i % v.get j - m < v.get j
⊢ False
Tactic:
have : ¬v.get j ∣ v.get i % v.get j - m := Nat.not_dvd_of_pos_of_lt hpos this
Proof state after:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (v.get j.succ).isDvdNat (v.get i.succ - v.head)
this✝¹ : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i % v.get j
A : v.get j ∣ v.get i - m
hmvi : m < v.get i
hsub : v.get j ∣ v.get i % v.get j - m
hpos : 0 < v.get i % v.get j - m
this✝ : v.get i % v.get j - m < v.get j
this : ¬v.get j ∣ v.get i % v.get j - m
⊢ False
Theorem: Nat.Arith₁.rem
Proof state before:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (v.get j.succ).isDvdNat (v.get i.succ - v.head)
this✝¹ : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i % v.get j
A : v.get j ∣ v.get i - m
hmvi : m < v.get i
hsub : v.get j ∣ v.get i % v.get j - m
hpos : 0 < v.get i % v.get j - m
this✝ : v.get i % v.get j - m < v.get j
this : ¬v.get j ∣ v.get i % v.get j - m
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: Nat.Arith₁.rem
Proof state before:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (v.get j.succ).isDvdNat (v.get i.succ - v.head)
this : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i % v.get j
A : v.get j ∣ v.get i - m
hmvi : m < v.get i
⊢ v.get j ∣ v.get i % v.get j - m
Tactic:
have : v.get i - m - (v.get i - v.get i % v.get j) = v.get i % v.get j - m := by
  rw[Nat.sub_eq_iff_eq_add (Nat.sub_le_sub_left (le_of_lt hm) _), Nat.sub_eq_iff_eq_add (le_of_lt hmvi),
    ←Nat.sub_add_comm (le_of_lt hm), Nat.add_sub_of_le (Nat.mod_le (v.get i) (v.get j)),
    Nat.sub_add_cancel (le_of_lt hmvi)]
Proof state after:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (v.get j.succ).isDvdNat (v.get i.succ - v.head)
this✝ : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i % v.get j
A : v.get j ∣ v.get i - m
hmvi : m < v.get i
this : v.get i - m - (v.get i - v.get i % v.get j) = v.get i % v.get j - m
⊢ v.get j ∣ v.get i % v.get j - m
Theorem: Nat.Arith₁.rem
Proof state before:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (v.get j.succ).isDvdNat (v.get i.succ - v.head)
this✝ : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i % v.get j
A : v.get j ∣ v.get i - m
hmvi : m < v.get i
this : v.get i - m - (v.get i - v.get i % v.get j) = v.get i % v.get j - m
⊢ v.get j ∣ v.get i % v.get j - m
Tactic:
rw[←this]
Proof state after:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (v.get j.succ).isDvdNat (v.get i.succ - v.head)
this✝ : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i % v.get j
A : v.get j ∣ v.get i - m
hmvi : m < v.get i
this : v.get i - m - (v.get i - v.get i % v.get j) = v.get i % v.get j - m
⊢ v.get j ∣ v.get i - m - (v.get i - v.get i % v.get j)
Theorem: Nat.Arith₁.rem
Proof state before:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (v.get j.succ).isDvdNat (v.get i.succ - v.head)
this✝ : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i % v.get j
A : v.get j ∣ v.get i - m
hmvi : m < v.get i
this : v.get i - m - (v.get i - v.get i % v.get j) = v.get i % v.get j - m
⊢ v.get j ∣ v.get i - m - (v.get i - v.get i % v.get j)
Tactic:
exact Nat.dvd_sub (Nat.sub_le_sub_left (le_of_lt hm) _) A (@Nat.dvd_sub_mod (v.get j) (v.get i))
Proof state after:
no goals
Theorem: Nat.Arith₁.rem
Proof state before:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (v.get j.succ).isDvdNat (v.get i.succ - v.head)
this : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i % v.get j
A : v.get j ∣ v.get i - m
hmvi : m < v.get i
⊢ v.get i - m - (v.get i - v.get i % v.get j) = v.get i % v.get j - m
Tactic:
rw[Nat.sub_eq_iff_eq_add (Nat.sub_le_sub_left (le_of_lt hm) _), Nat.sub_eq_iff_eq_add (le_of_lt hmvi),
  ←Nat.sub_add_comm (le_of_lt hm), Nat.add_sub_of_le (Nat.mod_le (v.get i) (v.get j)),
  Nat.sub_add_cancel (le_of_lt hmvi)]
Proof state after:
no goals
Theorem: Nat.Arith₁.rem
Proof state before:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (v.get j.succ).isDvdNat (v.get i.succ - v.head)
this : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i % v.get j
A : v.get j ∣ v.get i - m
hmvi : m < v.get i
hsub : v.get j ∣ v.get i % v.get j - m
⊢ 0 + m < v.get i % v.get j
Tactic:
simpa using hm
Proof state after:
no goals
Theorem: Nat.Arith₁.rem
Proof state before:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (v.get j.succ).isDvdNat (v.get i.succ - v.head)
this : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i % v.get j
A : v.get j ∣ v.get i - m
hmvi : m < v.get i
hsub : v.get j ∣ v.get i % v.get j - m
hpos : 0 < v.get i % v.get j - m
⊢ v.get i % v.get j - m < v.get j
Tactic:
have : v.get i % v.get j < v.get j :=
  Nat.mod_lt _ (Nat.pos_of_ne_zero $ fun h => (Nat.not_lt.mpr (by simpa [Nat.sub_eq_zero_iff_le, h] using hsub)) hmvi)
Proof state after:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (v.get j.succ).isDvdNat (v.get i.succ - v.head)
this✝ : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i % v.get j
A : v.get j ∣ v.get i - m
hmvi : m < v.get i
hsub : v.get j ∣ v.get i % v.get j - m
hpos : 0 < v.get i % v.get j - m
this : v.get i % v.get j < v.get j
⊢ v.get i % v.get j - m < v.get j
Theorem: Nat.Arith₁.rem
Proof state before:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (v.get j.succ).isDvdNat (v.get i.succ - v.head)
this✝ : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i % v.get j
A : v.get j ∣ v.get i - m
hmvi : m < v.get i
hsub : v.get j ∣ v.get i % v.get j - m
hpos : 0 < v.get i % v.get j - m
this : v.get i % v.get j < v.get j
⊢ v.get i % v.get j - m < v.get j
Tactic:
exact lt_of_le_of_lt (sub_le _ _) this
Proof state after:
no goals
Theorem: Nat.Arith₁.rem
Proof state before:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (v.get j.succ).isDvdNat (v.get i.succ - v.head)
this : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i % v.get j
A : v.get j ∣ v.get i - m
hmvi : m < v.get i
hsub : v.get j ∣ v.get i % v.get j - m
hpos : 0 < v.get i % v.get j - m
h : v.get j = 0
⊢ v.get i ≤ m
Tactic:
simpa [Nat.sub_eq_zero_iff_le, h] using hsub
Proof state after:
no goals
Theorem: Nat.Arith₁.ball
Proof state before:
n : ℕ
p : Vector ℕ n → ℕ → ℕ
hp : Arith₁ fun v => p v.tail v.head
i : Fin n
⊢ Arith₁ fun v => (v.get i).ball (p v)
Tactic:
let F : Vector ℕ (n + 1) → ℕ := fun v => (p v.tail v.head).inv.or (isLeNat (v.get i.succ) v.head)
Proof state after:
n : ℕ
p : Vector ℕ n → ℕ → ℕ
hp : Arith₁ fun v => p v.tail v.head
i : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (p v.tail v.head).inv.or ((v.get i.succ).isLeNat v.head)
⊢ Arith₁ fun v => (v.get i).ball (p v)
Theorem: Nat.Arith₁.ball
Proof state before:
n : ℕ
p : Vector ℕ n → ℕ → ℕ
hp : Arith₁ fun v => p v.tail v.head
i : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (p v.tail v.head).inv.or ((v.get i.succ).isLeNat v.head)
⊢ Arith₁ fun v => (v.get i).ball (p v)
Tactic:
have hF : Arith₁ F := (or 0 1).comp₂ _ ((inv 0).comp₁ _ hp) ((le 0 1).comp₂ _ (proj i.succ) head)
Proof state after:
n : ℕ
p : Vector ℕ n → ℕ → ℕ
hp : Arith₁ fun v => p v.tail v.head
i : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (p v.tail v.head).inv.or ((v.get i.succ).isLeNat v.head)
hF : Arith₁ F
⊢ Arith₁ fun v => (v.get i).ball (p v)
Theorem: Nat.Arith₁.ball
Proof state before:
n : ℕ
p : Vector ℕ n → ℕ → ℕ
hp : Arith₁ fun v => p v.tail v.head
i : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (p v.tail v.head).inv.or ((v.get i.succ).isLeNat v.head)
hF : Arith₁ F
⊢ Arith₁ fun v => (v.get i).ball (p v)
Tactic:
have : @Arith₁ (n + 1) (fun v => isEqNat v.head (v.get i.succ)) :=
  (equal 0 1).comp₂ _ head (proj i.succ)
Proof state after:
n : ℕ
p : Vector ℕ n → ℕ → ℕ
hp : Arith₁ fun v => p v.tail v.head
i : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (p v.tail v.head).inv.or ((v.get i.succ).isLeNat v.head)
hF : Arith₁ F
this : Arith₁ fun v => v.head.isEqNat (v.get i.succ)
⊢ Arith₁ fun v => (v.get i).ball (p v)
Theorem: Nat.Arith₁.ball
Proof state before:
n : ℕ
p : Vector ℕ n → ℕ → ℕ
hp : Arith₁ fun v => p v.tail v.head
i : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (p v.tail v.head).inv.or ((v.get i.succ).isLeNat v.head)
hF : Arith₁ F
this : Arith₁ fun v => v.head.isEqNat (v.get i.succ)
⊢ Arith₁ fun v => (v.get i).ball (p v)
Tactic:
have := ArithPart₁.map (fun v x => isEqNat x (v.get i)) (this.of_eq $ by simp) (ArithPart₁.rfindPos hF)
Proof state after:
n : ℕ
p : Vector ℕ n → ℕ → ℕ
hp : Arith₁ fun v => p v.tail v.head
i : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (p v.tail v.head).inv.or ((v.get i.succ).isLeNat v.head)
hF : Arith₁ F
this✝ : Arith₁ fun v => v.head.isEqNat (v.get i.succ)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isEqNat (v.get i)) v) (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v))))
⊢ Arith₁ fun v => (v.get i).ball (p v)
Theorem: Nat.Arith₁.ball
Proof state before:
n : ℕ
p : Vector ℕ n → ℕ → ℕ
hp : Arith₁ fun v => p v.tail v.head
i : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (p v.tail v.head).inv.or ((v.get i.succ).isLeNat v.head)
hF : Arith₁ F
this : Arith₁ fun v => v.head.isEqNat (v.get i.succ)
⊢ ∀ (i_1 : Vector ℕ (n + 1)), i_1.head.isEqNat (i_1.get i.succ) = (fun v x => x.isEqNat (v.get i)) i_1.tail i_1.head
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.Arith₁.ball
Proof state before:
n : ℕ
p : Vector ℕ n → ℕ → ℕ
hp : Arith₁ fun v => p v.tail v.head
i : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (p v.tail v.head).inv.or ((v.get i.succ).isLeNat v.head)
hF : Arith₁ F
this✝ : Arith₁ fun v => v.head.isEqNat (v.get i.succ)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isEqNat (v.get i)) v) (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v))))
⊢ ∀ (i_1 : Vector ℕ n),
    Part.map ((fun v x => x.isEqNat (v.get i)) i_1) (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ i_1)))) =
      (↑fun v => (v.get i).ball (p v)) i_1
Tactic:
intro v
Proof state after:
n : ℕ
p : Vector ℕ n → ℕ → ℕ
hp : Arith₁ fun v => p v.tail v.head
i : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (p v.tail v.head).inv.or ((v.get i.succ).isLeNat v.head)
hF : Arith₁ F
this✝ : Arith₁ fun v => v.head.isEqNat (v.get i.succ)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isEqNat (v.get i)) v) (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v))))
v : Vector ℕ n
⊢ Part.map ((fun v x => x.isEqNat (v.get i)) v) (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v)))) =
    (↑fun v => (v.get i).ball (p v)) v
Theorem: Nat.Arith₁.ball
Proof state before:
n : ℕ
p : Vector ℕ n → ℕ → ℕ
hp : Arith₁ fun v => p v.tail v.head
i : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (p v.tail v.head).inv.or ((v.get i.succ).isLeNat v.head)
hF : Arith₁ F
this✝ : Arith₁ fun v => v.head.isEqNat (v.get i.succ)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isEqNat (v.get i)) v) (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v))))
v : Vector ℕ n
⊢ Part.map ((fun v x => x.isEqNat (v.get i)) v) (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v)))) =
    (↑fun v => (v.get i).ball (p v)) v
Tactic:
simp only [tail_cons, head_cons, get_cons_succ, or_pos_iff, inv_pos_iff, not_lt,
  nonpos_iff_eq_zero, isLeNat_pos_iff, Bool.decide_or, PFun.coe_val, eq_some_iff, mem_map_iff,
  mem_rfind, mem_some_iff, F]
Proof state after:
n : ℕ
p : Vector ℕ n → ℕ → ℕ
hp : Arith₁ fun v => p v.tail v.head
i : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (p v.tail v.head).inv.or ((v.get i.succ).isLeNat v.head)
hF : Arith₁ F
this✝ : Arith₁ fun v => v.head.isEqNat (v.get i.succ)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isEqNat (v.get i)) v) (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v))))
v : Vector ℕ n
⊢ ∃ a,
    (true = (decide (p v a = 0) || decide (v.get i ≤ a)) ∧
        ∀ {m : ℕ}, m < a → false = (decide (p v m = 0) || decide (v.get i ≤ m))) ∧
      a.isEqNat (v.get i) = (v.get i).ball (p v)