internlm/Lean-Github huggingface dataset:
Theorem: Nat.Arith₁.unpair₂
Proof state before:
n : ℕ
i : Fin n
hf : Arith₁ fun v => (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt
hg : Arith₁ fun v => (v.get i).sqrt
hh : Arith₁ fun v => v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt
⊢ Arith₁ fun v => (v.get i).unpair.2
Tactic:
have := if_pos hf hg hh
Proof state after:
n : ℕ
i : Fin n
hf : Arith₁ fun v => (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt
hg : Arith₁ fun v => (v.get i).sqrt
hh : Arith₁ fun v => v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt
this :
  Arith₁ fun v =>
    if 0 < (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt then (v.get i).sqrt
    else v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt
⊢ Arith₁ fun v => (v.get i).unpair.2
Theorem: Nat.Arith₁.unpair₂
Proof state before:
n : ℕ
i : Fin n
hf : Arith₁ fun v => (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt
hg : Arith₁ fun v => (v.get i).sqrt
hh : Arith₁ fun v => v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt
this :
  Arith₁ fun v =>
    if 0 < (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt then (v.get i).sqrt
    else v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt
⊢ Arith₁ fun v => (v.get i).unpair.2
Tactic:
exact this.of_eq <| by
  intro v; simp[unpair]
  by_cases v.get i - (v.get i).sqrt * (v.get i).sqrt < sqrt (v.get i) <;> simp[*]
Proof state after:
no goals
Theorem: Nat.Arith₁.unpair₂
Proof state before:
n : ℕ
i : Fin n
hf : Arith₁ fun v => (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt
hg : Arith₁ fun v => (v.get i).sqrt
hh : Arith₁ fun v => v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt
this :
  Arith₁ fun v =>
    if 0 < (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt then (v.get i).sqrt
    else v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt
⊢ ∀ (i_1 : Vector ℕ n),
    (if 0 < (i_1.get i - (i_1.get i).sqrt * (i_1.get i).sqrt).isLtNat (i_1.get i).sqrt then (i_1.get i).sqrt
      else i_1.get i - (i_1.get i).sqrt * (i_1.get i).sqrt - (i_1.get i).sqrt) =
      (i_1.get i).unpair.2
Tactic:
intro v
Proof state after:
n : ℕ
i : Fin n
hf : Arith₁ fun v => (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt
hg : Arith₁ fun v => (v.get i).sqrt
hh : Arith₁ fun v => v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt
this :
  Arith₁ fun v =>
    if 0 < (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt then (v.get i).sqrt
    else v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt
v : Vector ℕ n
⊢ (if 0 < (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt then (v.get i).sqrt
    else v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt) =
    (v.get i).unpair.2
Theorem: Nat.Arith₁.unpair₂
Proof state before:
n : ℕ
i : Fin n
hf : Arith₁ fun v => (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt
hg : Arith₁ fun v => (v.get i).sqrt
hh : Arith₁ fun v => v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt
this :
  Arith₁ fun v =>
    if 0 < (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt then (v.get i).sqrt
    else v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt
v : Vector ℕ n
⊢ (if 0 < (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt then (v.get i).sqrt
    else v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt) =
    (v.get i).unpair.2
Tactic:
simp[unpair]
Proof state after:
n : ℕ
i : Fin n
hf : Arith₁ fun v => (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt
hg : Arith₁ fun v => (v.get i).sqrt
hh : Arith₁ fun v => v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt
this :
  Arith₁ fun v =>
    if 0 < (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt then (v.get i).sqrt
    else v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt
v : Vector ℕ n
⊢ (if v.get i - (v.get i).sqrt * (v.get i).sqrt < (v.get i).sqrt then (v.get i).sqrt
    else v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt) =
    (if v.get i - (v.get i).sqrt * (v.get i).sqrt < (v.get i).sqrt then
        (v.get i - (v.get i).sqrt * (v.get i).sqrt, (v.get i).sqrt)
      else ((v.get i).sqrt, v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt)).2
Theorem: Nat.Arith₁.unpair₂
Proof state before:
n : ℕ
i : Fin n
hf : Arith₁ fun v => (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt
hg : Arith₁ fun v => (v.get i).sqrt
hh : Arith₁ fun v => v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt
this :
  Arith₁ fun v =>
    if 0 < (v.get i - (v.get i).sqrt * (v.get i).sqrt).isLtNat (v.get i).sqrt then (v.get i).sqrt
    else v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt
v : Vector ℕ n
⊢ (if v.get i - (v.get i).sqrt * (v.get i).sqrt < (v.get i).sqrt then (v.get i).sqrt
    else v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt) =
    (if v.get i - (v.get i).sqrt * (v.get i).sqrt < (v.get i).sqrt then
        (v.get i - (v.get i).sqrt * (v.get i).sqrt, (v.get i).sqrt)
      else ((v.get i).sqrt, v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt)).2
Tactic:
by_cases v.get i - (v.get i).sqrt * (v.get i).sqrt < sqrt (v.get i) <;> simp[*]
Proof state after:
no goals
Theorem: Nat.Arith₁.dvd
Proof 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)
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)
⊢ Arith₁ fun v => (v.get i).isDvdNat (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)
⊢ 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)
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)
⊢ Arith₁ fun v => (v.get i).isDvdNat (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)
⊢ 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)
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))))
⊢ Arith₁ fun v => (v.get i).isDvdNat (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)
⊢ ∀ (i : Vector ℕ n.succ), i.get j.succ = i.tail.get j
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))))
⊢ ∀ (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
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
⊢ 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
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
⊢ 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]
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
⊢ ∃ 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
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
⊢ ∃ 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
Proof 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
Theorem: Nat.Arith₁.dvd
Proof 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]
Proof 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
Theorem: Nat.Arith₁.dvd
Proof 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⟩
Proof 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
Theorem: Nat.Arith₁.dvd
Proof 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]⟩
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
⊢ k ≤ v.get j
Tactic:
by_cases hkz : k = 0
Proof 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
Theorem: Nat.Arith₁.dvd
Proof 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]
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
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]
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
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
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
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)
Proof state after:
no goals