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

State before:
n : ℕ
i j : Fin n
⊢ Arith₁ fun v => v.get i % v.get j
Tactic:
let F : Vector ℕ (n + 1) → ℕ := fun v => isDvdNat (v.get j.succ) (v.get i.succ - v.head)
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

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)
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

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
State after:
no goals

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
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

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]
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

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
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

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)
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

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))
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

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)
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

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
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

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
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

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
State after:
no goals

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)]
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

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]
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)

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))
State after:
no goals

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)]
State after:
no goals

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
State after:
no goals

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)
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

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
State after:
no goals

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
State after:
no goals