internlm/Lean-Github huggingface dataset:
Theorem: Nat.ArithPart₁.comp₂
Proof state before:
f : ℕ → ℕ →. ℕ
hf : ArithPart₁ fun v => f (v.get 0) (v.get 1)
n : ℕ
g h : Vector ℕ n → ℕ
hg : Arith₁ g
hh : Arith₁ h
i : Vector ℕ n
⊢ (fun j => ![↑g, ↑h] j i) = fun j => pure (![g i, h i] j)
Tactic:
funext j
Proof state after:
case h
f : ℕ → ℕ →. ℕ
hf : ArithPart₁ fun v => f (v.get 0) (v.get 1)
n : ℕ
g h : Vector ℕ n → ℕ
hg : Arith₁ g
hh : Arith₁ h
i : Vector ℕ n
j : Fin (succ 1)
⊢ ![↑g, ↑h] j i = pure (![g i, h i] j)
Theorem: Nat.ArithPart₁.comp₂
Proof state before:
case h
f : ℕ → ℕ →. ℕ
hf : ArithPart₁ fun v => f (v.get 0) (v.get 1)
n : ℕ
g h : Vector ℕ n → ℕ
hg : Arith₁ g
hh : Arith₁ h
i : Vector ℕ n
j : Fin (succ 1)
⊢ ![↑g, ↑h] j i = pure (![g i, h i] j)
Tactic:
cases j using Fin.cases <;> simp[Fin.eq_zero]
Proof state after:
no goals
Theorem: Nat.Arith₁.head
Proof state before:
n : ℕ
⊢ ∀ (i : Vector ℕ (n + 1)), (↑fun v => v.get 0) i = (↑fun v => v.head) i
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.Arith₁.comp
Proof state before:
m n : ℕ
f : Vector ℕ n → ℕ
g : Fin n → Vector ℕ m → ℕ
hf : Arith₁ f
hg : ∀ (i : Fin n), Arith₁ (g i)
⊢ ∀ (i : Vector ℕ m), (mOfFn fun i_1 => ↑(g i_1) i) >>= ↑f = (↑fun v => f (ofFn fun i => g i v)) i
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.Arith₁.cons
Proof state before:
n m : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ n → Vector ℕ m
hf : Arith₁ f
hg : Vec g
i : Fin m.succ
⊢ Arith₁ fun v => ((fun v => f v ::ᵥ g v) v).get 0
Tactic:
simp [*]
Proof state after:
no goals
Theorem: Nat.Arith₁.cons
Proof state before:
n m : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ n → Vector ℕ m
hf : Arith₁ f
hg : Vec g
i✝ : Fin m.succ
i : Fin m
⊢ Arith₁ fun v => ((fun v => f v ::ᵥ g v) v).get i.succ
Tactic:
simp [hg i]
Proof state after:
no goals
Theorem: Nat.Arith₁.tail
Proof state before:
n : ℕ
f : Vector ℕ n → ℕ
hf : Arith₁ f
v : Vector ℕ n.succ
⊢ f (ofFn fun i => v.get i.succ) = f v.tail
Tactic:
rw[←ofFn_get v.tail]
Proof state after:
n : ℕ
f : Vector ℕ n → ℕ
hf : Arith₁ f
v : Vector ℕ n.succ
⊢ f (ofFn fun i => v.get i.succ) = f (ofFn v.tail.get)
Theorem: Nat.Arith₁.tail
Proof state before:
n : ℕ
f : Vector ℕ n → ℕ
hf : Arith₁ f
v : Vector ℕ n.succ
⊢ f (ofFn fun i => v.get i.succ) = f (ofFn v.tail.get)
Tactic:
congr
Proof state after:
case e_a.e_a
n : ℕ
f : Vector ℕ n → ℕ
hf : Arith₁ f
v : Vector ℕ n.succ
⊢ (fun i => v.get i.succ) = v.tail.get
Theorem: Nat.Arith₁.tail
Proof state before:
case e_a.e_a
n : ℕ
f : Vector ℕ n → ℕ
hf : Arith₁ f
v : Vector ℕ n.succ
⊢ (fun i => v.get i.succ) = v.tail.get
Tactic:
funext i
Proof state after:
case e_a.e_a.h
n : ℕ
f : Vector ℕ n → ℕ
hf : Arith₁ f
v : Vector ℕ n.succ
i : Fin n
⊢ v.get i.succ = v.tail.get i
Theorem: Nat.Arith₁.tail
Proof state before:
case e_a.e_a.h
n : ℕ
f : Vector ℕ n → ℕ
hf : Arith₁ f
v : Vector ℕ n.succ
i : Fin n
⊢ v.get i.succ = v.tail.get i
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.Arith₁.comp'
Proof state before:
n m : ℕ
f : Vector ℕ m → ℕ
g : Vector ℕ n → Vector ℕ m
hf : Arith₁ f
hg : Vec g
v : Vector ℕ n
⊢ f (ofFn fun i => (g v).get i) = f (g v)
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.Arith₁.comp₁
Proof state before:
f : ℕ → ℕ
hf : Arith₁ fun v => f (v.get 0)
n : ℕ
g : Vector ℕ n → ℕ
hg : Arith₁ g
⊢ ∀ (i : Vector ℕ n), f ((ofFn fun i_1 => g i).get 0) = f (g i)
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.Arith₁.comp₂
Proof state before:
f : ℕ → ℕ → ℕ
hf : Arith₁ fun v => f (v.get 0) (v.get 1)
n : ℕ
g h : Vector ℕ n → ℕ
hg : Arith₁ g
hh : Arith₁ h
i✝ : Fin (succ 0).succ
i : Fin 1
⊢ Arith₁ (![g, h] i.succ)
Tactic:
simpa using hh
Proof state after:
no goals
Theorem: Nat.Arith₁.comp₂
Proof state before:
f : ℕ → ℕ → ℕ
hf : Arith₁ fun v => f (v.get 0) (v.get 1)
n : ℕ
g h : Vector ℕ n → ℕ
hg : Arith₁ g
hh : Arith₁ h
⊢ ∀ (i : Vector ℕ n), f ((ofFn fun i_1 => ![g, h] i_1 i).get 0) ((ofFn fun i_1 => ![g, h] i_1 i).get 1) = f (g i) (h i)
Tactic:
intro i
Proof state after:
f : ℕ → ℕ → ℕ
hf : Arith₁ fun v => f (v.get 0) (v.get 1)
n : ℕ
g h : Vector ℕ n → ℕ
hg : Arith₁ g
hh : Arith₁ h
i : Vector ℕ n
⊢ f ((ofFn fun i_1 => ![g, h] i_1 i).get 0) ((ofFn fun i_1 => ![g, h] i_1 i).get 1) = f (g i) (h i)
Theorem: Nat.Arith₁.comp₂
Proof state before:
f : ℕ → ℕ → ℕ
hf : Arith₁ fun v => f (v.get 0) (v.get 1)
n : ℕ
g h : Vector ℕ n → ℕ
hg : Arith₁ g
hh : Arith₁ h
i : Vector ℕ n
⊢ f ((ofFn fun i_1 => ![g, h] i_1 i).get 0) ((ofFn fun i_1 => ![g, h] i_1 i).get 1) = f (g i) (h i)
Tactic:
simp[Matrix.comp_vecCons']
Proof state after:
no goals
Theorem: Nat.Arith₁.le
Proof state before:
n : ℕ
i j : Fin n
⊢ ∀ (i_1 : Vector ℕ n),
    ((i_1.get i).isLtNat (i_1.get j)).or ((i_1.get i).isEqNat (i_1.get j)) = (i_1.get i).isLeNat (i_1.get j)
Tactic:
simp[Nat.or_eq, Nat.le_iff_lt_or_eq, isLeNat]
Proof state after:
no goals
Theorem: Nat.Arith₁.if_pos
Proof state before:
n : ℕ
f g h : Vector ℕ n → ℕ
hf : Arith₁ f
hg : Arith₁ g
hh : Arith₁ h
⊢ Arith₁ fun v => if 0 < f v then g v else h v
Tactic:
have : Arith₁ (fun v => (f v).pos * (g v) + (f v).inv * (h v)) :=
  (add 0 1).comp₂ _
    ((mul 0 1).comp₂ _ ((pos 0).comp₁ _ hf) hg)
    ((mul 0 1).comp₂ _ ((inv 0).comp₁ _ hf) hh)
Proof state after:
n : ℕ
f g h : Vector ℕ n → ℕ
hf : Arith₁ f
hg : Arith₁ g
hh : Arith₁ h
this : Arith₁ fun v => (f v).pos * g v + (f v).inv * h v
⊢ Arith₁ fun v => if 0 < f v then g v else h v
Theorem: Nat.Arith₁.if_pos
Proof state before:
n : ℕ
f g h : Vector ℕ n → ℕ
hf : Arith₁ f
hg : Arith₁ g
hh : Arith₁ h
this : Arith₁ fun v => (f v).pos * g v + (f v).inv * h v
⊢ Arith₁ fun v => if 0 < f v then g v else h v
Tactic:
exact this.of_eq <| by
  intro i; by_cases hf : f i = 0 <;> simp[hf, zero_lt_iff]
Proof state after:
no goals
Theorem: Nat.Arith₁.if_pos
Proof state before:
n : ℕ
f g h : Vector ℕ n → ℕ
hf : Arith₁ f
hg : Arith₁ g
hh : Arith₁ h
this : Arith₁ fun v => (f v).pos * g v + (f v).inv * h v
⊢ ∀ (i : Vector ℕ n), (f i).pos * g i + (f i).inv * h i = if 0 < f i then g i else h i
Tactic:
intro i
Proof state after:
n : ℕ
f g h : Vector ℕ n → ℕ
hf : Arith₁ f
hg : Arith₁ g
hh : Arith₁ h
this : Arith₁ fun v => (f v).pos * g v + (f v).inv * h v
i : Vector ℕ n
⊢ (f i).pos * g i + (f i).inv * h i = if 0 < f i then g i else h i
Theorem: Nat.Arith₁.if_pos
Proof state before:
n : ℕ
f g h : Vector ℕ n → ℕ
hf : Arith₁ f
hg : Arith₁ g
hh : Arith₁ h
this : Arith₁ fun v => (f v).pos * g v + (f v).inv * h v
i : Vector ℕ n
⊢ (f i).pos * g i + (f i).inv * h i = if 0 < f i then g i else h i
Tactic:
by_cases hf : f i = 0 <;> simp[hf, zero_lt_iff]
Proof state after:
no goals
Theorem: Nat.ArithPart₁.rfindPos
Proof state before:
n : ℕ
f : Vector ℕ (n + 1) → ℕ
h : Arith₁ f
⊢ ∀ (i : Vector ℕ n),
    (Nat.rfind fun n_1 => Part.some (decide ((isLtNat 0 (f (n_1 ::ᵥ i))).inv = 0))) =
      Nat.rfind fun n_1 => Part.some (decide (0 < f (n_1 ::ᵥ i)))
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.ArithPart₁.inv_fun
Proof state before:
n : ℕ
i : Fin n
f : ℕ → ℕ
hf : Arith₁ fun v => f (v.get 0)
⊢ ArithPart₁ fun v => Nat.rfind fun x => Part.some (decide (f x ≤ v.get i ∧ v.get i < f (x + 1)))
Tactic:
let F : ℕ → ℕ → ℕ := fun x y => (isLeNat (f x) y).and (isLtNat y (f (x + 1)))
Proof state after:
n : ℕ
i : Fin n
f : ℕ → ℕ
hf : Arith₁ fun v => f (v.get 0)
F : ℕ → ℕ → ℕ := fun x y => ((f x).isLeNat y).and (y.isLtNat (f (x + 1)))
⊢ ArithPart₁ fun v => Nat.rfind fun x => Part.some (decide (f x ≤ v.get i ∧ v.get i < f (x + 1)))
Theorem: Nat.ArithPart₁.inv_fun
Proof state before:
n : ℕ
i : Fin n
f : ℕ → ℕ
hf : Arith₁ fun v => f (v.get 0)
F : ℕ → ℕ → ℕ := fun x y => ((f x).isLeNat y).and (y.isLtNat (f (x + 1)))
⊢ ArithPart₁ fun v => Nat.rfind fun x => Part.some (decide (f x ≤ v.get i ∧ v.get i < f (x + 1)))
Tactic:
have := rfindPos₁ i (f := F) <| (Arith₁.and 0 1).comp₂ _
    ((Arith₁.le 0 1).comp₂ _ (hf.comp₁ _ (proj 0)) (proj 1))
    ((Arith₁.lt 0 1).comp₂ _ (proj 1) (hf.comp₁ _ $ (Arith₁.succ 0).comp₁ _ $ proj 0))
Proof state after:
n : ℕ
i : Fin n
f : ℕ → ℕ
hf : Arith₁ fun v => f (v.get 0)
F : ℕ → ℕ → ℕ := fun x y => ((f x).isLeNat y).and (y.isLtNat (f (x + 1)))
this : ArithPart₁ fun v => Nat.rfind fun n_1 => Part.some (decide (0 < F n_1 (v.get i)))
⊢ ArithPart₁ fun v => Nat.rfind fun x => Part.some (decide (f x ≤ v.get i ∧ v.get i < f (x + 1)))
Theorem: Nat.ArithPart₁.inv_fun
Proof state before:
n : ℕ
i : Fin n
f : ℕ → ℕ
hf : Arith₁ fun v => f (v.get 0)
F : ℕ → ℕ → ℕ := fun x y => ((f x).isLeNat y).and (y.isLtNat (f (x + 1)))
this : ArithPart₁ fun v => Nat.rfind fun n_1 => Part.some (decide (0 < F n_1 (v.get i)))
⊢ ArithPart₁ fun v => Nat.rfind fun x => Part.some (decide (f x ≤ v.get i ∧ v.get i < f (x + 1)))
Tactic:
exact this.of_eq <| by intro v; simp [F]
Proof state after:
no goals
Theorem: Nat.ArithPart₁.inv_fun
Proof state before:
n : ℕ
i : Fin n
f : ℕ → ℕ
hf : Arith₁ fun v => f (v.get 0)
F : ℕ → ℕ → ℕ := fun x y => ((f x).isLeNat y).and (y.isLtNat (f (x + 1)))
this : ArithPart₁ fun v => Nat.rfind fun n_1 => Part.some (decide (0 < F n_1 (v.get i)))
⊢ ∀ (i_1 : Vector ℕ n),
    (Nat.rfind fun n_1 => Part.some (decide (0 < F n_1 (i_1.get i)))) =
      Nat.rfind fun x => Part.some (decide (f x ≤ i_1.get i ∧ i_1.get i < f (x + 1)))
Tactic:
intro v
Proof state after:
n : ℕ
i : Fin n
f : ℕ → ℕ
hf : Arith₁ fun v => f (v.get 0)
F : ℕ → ℕ → ℕ := fun x y => ((f x).isLeNat y).and (y.isLtNat (f (x + 1)))
this : ArithPart₁ fun v => Nat.rfind fun n_1 => Part.some (decide (0 < F n_1 (v.get i)))
v : Vector ℕ n
⊢ (Nat.rfind fun n_1 => Part.some (decide (0 < F n_1 (v.get i)))) =
    Nat.rfind fun x => Part.some (decide (f x ≤ v.get i ∧ v.get i < f (x + 1)))
Theorem: Nat.ArithPart₁.inv_fun
Proof state before:
n : ℕ
i : Fin n
f : ℕ → ℕ
hf : Arith₁ fun v => f (v.get 0)
F : ℕ → ℕ → ℕ := fun x y => ((f x).isLeNat y).and (y.isLtNat (f (x + 1)))
this : ArithPart₁ fun v => Nat.rfind fun n_1 => Part.some (decide (0 < F n_1 (v.get i)))
v : Vector ℕ n
⊢ (Nat.rfind fun n_1 => Part.some (decide (0 < F n_1 (v.get i)))) =
    Nat.rfind fun x => Part.some (decide (f x ≤ v.get i ∧ v.get i < f (x + 1)))
Tactic:
simp [F]
Proof state after:
no goals
Theorem: Nat.ArithPart₁.implicit_fun
Proof state before:
n : ℕ
i : Fin n
f : Vector ℕ n → ℕ → ℕ
hf : Arith₁ fun v => f v.tail v.head
⊢ ArithPart₁ fun v => Nat.rfind fun x => Part.some (decide (f v x ≤ v.get i ∧ v.get i < f v (x + 1)))
Tactic:
let F : Vector ℕ (n + 1) → ℕ :=
  fun v => (isLeNat (f v.tail v.head) (v.get i.succ)).and (isLtNat (v.get i.succ) (f v.tail (v.head + 1)))
Proof state after:
n : ℕ
i : Fin n
f : Vector ℕ n → ℕ → ℕ
hf : Arith₁ fun v => f v.tail v.head
F : Vector ℕ (n + 1) → ℕ :=
  fun v => ((f v.tail v.head).isLeNat (v.get i.succ)).and ((v.get i.succ).isLtNat (f v.tail (v.head + 1)))
⊢ ArithPart₁ fun v => Nat.rfind fun x => Part.some (decide (f v x ≤ v.get i ∧ v.get i < f v (x + 1)))
Theorem: Nat.ArithPart₁.implicit_fun
Proof state before:
n : ℕ
i : Fin n
f : Vector ℕ n → ℕ → ℕ
hf : Arith₁ fun v => f v.tail v.head
F : Vector ℕ (n + 1) → ℕ :=
  fun v => ((f v.tail v.head).isLeNat (v.get i.succ)).and ((v.get i.succ).isLtNat (f v.tail (v.head + 1)))
⊢ ArithPart₁ fun v => Nat.rfind fun x => Part.some (decide (f v x ≤ v.get i ∧ v.get i < f v (x + 1)))
Tactic:
have : Arith₁ F :=
  (Arith₁.and 0 1).comp₂ _
    ((Arith₁.le 0 1).comp₂ _ hf (proj i.succ))
    ((Arith₁.lt 0 1).comp₂ _ (proj i.succ)
      (Arith₁.comp' hf (Arith₁.cons
        ((Arith₁.add 0 1).comp₂ _ Arith₁.head one) (fun i => Arith₁.tail (proj i)))))
Proof state after:
n : ℕ
i : Fin n
f : Vector ℕ n → ℕ → ℕ
hf : Arith₁ fun v => f v.tail v.head
F : Vector ℕ (n + 1) → ℕ :=
  fun v => ((f v.tail v.head).isLeNat (v.get i.succ)).and ((v.get i.succ).isLtNat (f v.tail (v.head + 1)))
this : Arith₁ F
⊢ ArithPart₁ fun v => Nat.rfind fun x => Part.some (decide (f v x ≤ v.get i ∧ v.get i < f v (x + 1)))
Theorem: Nat.ArithPart₁.implicit_fun
Proof state before:
n : ℕ
i : Fin n
f : Vector ℕ n → ℕ → ℕ
hf : Arith₁ fun v => f v.tail v.head
F : Vector ℕ (n + 1) → ℕ :=
  fun v => ((f v.tail v.head).isLeNat (v.get i.succ)).and ((v.get i.succ).isLtNat (f v.tail (v.head + 1)))
this : Arith₁ F
⊢ ArithPart₁ fun v => Nat.rfind fun x => Part.some (decide (f v x ≤ v.get i ∧ v.get i < f v (x + 1)))
Tactic:
have := rfindPos this
Proof state after:
n : ℕ
i : Fin n
f : Vector ℕ n → ℕ → ℕ
hf : Arith₁ fun v => f v.tail v.head
F : Vector ℕ (n + 1) → ℕ :=
  fun v => ((f v.tail v.head).isLeNat (v.get i.succ)).and ((v.get i.succ).isLtNat (f v.tail (v.head + 1)))
this✝ : Arith₁ F
this : ArithPart₁ fun v => Nat.rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v)))
⊢ ArithPart₁ fun v => Nat.rfind fun x => Part.some (decide (f v x ≤ v.get i ∧ v.get i < f v (x + 1)))
Theorem: Nat.ArithPart₁.implicit_fun
Proof state before:
n : ℕ
i : Fin n
f : Vector ℕ n → ℕ → ℕ
hf : Arith₁ fun v => f v.tail v.head
F : Vector ℕ (n + 1) → ℕ :=
  fun v => ((f v.tail v.head).isLeNat (v.get i.succ)).and ((v.get i.succ).isLtNat (f v.tail (v.head + 1)))
this✝ : Arith₁ F
this : ArithPart₁ fun v => Nat.rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v)))
⊢ ArithPart₁ fun v => Nat.rfind fun x => Part.some (decide (f v x ≤ v.get i ∧ v.get i < f v (x + 1)))
Tactic:
exact this.of_eq <| by intro v; simp [F]
Proof state after:
no goals
Theorem: Nat.ArithPart₁.implicit_fun
Proof state before:
n : ℕ
i : Fin n
f : Vector ℕ n → ℕ → ℕ
hf : Arith₁ fun v => f v.tail v.head
F : Vector ℕ (n + 1) → ℕ :=
  fun v => ((f v.tail v.head).isLeNat (v.get i.succ)).and ((v.get i.succ).isLtNat (f v.tail (v.head + 1)))
this✝ : Arith₁ F
this : ArithPart₁ fun v => Nat.rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v)))
⊢ ∀ (i_1 : Vector ℕ n),
    (Nat.rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ i_1)))) =
      Nat.rfind fun x => Part.some (decide (f i_1 x ≤ i_1.get i ∧ i_1.get i < f i_1 (x + 1)))
Tactic:
intro v
Proof state after:
n : ℕ
i : Fin n
f : Vector ℕ n → ℕ → ℕ
hf : Arith₁ fun v => f v.tail v.head
F : Vector ℕ (n + 1) → ℕ :=
  fun v => ((f v.tail v.head).isLeNat (v.get i.succ)).and ((v.get i.succ).isLtNat (f v.tail (v.head + 1)))
this✝ : Arith₁ F
this : ArithPart₁ fun v => Nat.rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v)))
v : Vector ℕ n
⊢ (Nat.rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v)))) =
    Nat.rfind fun x => Part.some (decide (f v x ≤ v.get i ∧ v.get i < f v (x + 1)))
Theorem: Nat.ArithPart₁.implicit_fun
Proof state before:
n : ℕ
i : Fin n
f : Vector ℕ n → ℕ → ℕ
hf : Arith₁ fun v => f v.tail v.head
F : Vector ℕ (n + 1) → ℕ :=
  fun v => ((f v.tail v.head).isLeNat (v.get i.succ)).and ((v.get i.succ).isLtNat (f v.tail (v.head + 1)))
this✝ : Arith₁ F
this : ArithPart₁ fun v => Nat.rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v)))
v : Vector ℕ n
⊢ (Nat.rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v)))) =
    Nat.rfind fun x => Part.some (decide (f v x ≤ v.get i ∧ v.get i < f v (x + 1)))
Tactic:
simp [F]
Proof state after:
no goals
Theorem: Nat.Arith₁.sqrt
Proof state before:
n : ℕ
i : Fin n
⊢ Arith₁ fun v => (v.get i).sqrt
Tactic:
have := ArithPart₁.implicit_fun i (fun _ x => x * x) ((mul 0 1).comp₂ _ head head)
Proof state after:
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
⊢ Arith₁ fun v => (v.get i).sqrt
Theorem: Nat.Arith₁.sqrt
Proof state before:
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
⊢ ∀ (i_1 : Vector ℕ n),
    (rfind fun x =>
        Part.some (decide ((fun x x => x * x) i_1 x ≤ i_1.get i ∧ i_1.get i < (fun x x => x * x) i_1 (x + 1)))) =
      (↑fun v => (v.get i).sqrt) i_1
Tactic:
intro v
Proof state after:
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
⊢ (rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))) =
    (↑fun v => (v.get i).sqrt) v
Theorem: Nat.Arith₁.sqrt
Proof state before:
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
⊢ (rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))) =
    (↑fun v => (v.get i).sqrt) v
Tactic:
simp only [Bool.decide_and, PFun.coe_val, eq_some_iff, mem_rfind, mem_some_iff]
Proof state after:
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
⊢ true =
      (decide ((v.get i).sqrt * (v.get i).sqrt ≤ v.get i) &&
        decide (v.get i < ((v.get i).sqrt + 1) * ((v.get i).sqrt + 1))) ∧
    ∀ {m : ℕ}, m < (v.get i).sqrt → false = (decide (m * m ≤ v.get i) && decide (v.get i < (m + 1) * (m + 1)))
Theorem: Nat.Arith₁.sqrt
Proof state before:
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
⊢ true =
      (decide ((v.get i).sqrt * (v.get i).sqrt ≤ v.get i) &&
        decide (v.get i < ((v.get i).sqrt + 1) * ((v.get i).sqrt + 1))) ∧
    ∀ {m : ℕ}, m < (v.get i).sqrt → false = (decide (m * m ≤ v.get i) && decide (v.get i < (m + 1) * (m + 1)))
Tactic:
constructor
Proof state after:
case left
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
⊢ true =
    (decide ((v.get i).sqrt * (v.get i).sqrt ≤ v.get i) &&
      decide (v.get i < ((v.get i).sqrt + 1) * ((v.get i).sqrt + 1)))

case right
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
⊢ ∀ {m : ℕ}, m < (v.get i).sqrt → false = (decide (m * m ≤ v.get i) && decide (v.get i < (m + 1) * (m + 1)))
Theorem: Nat.Arith₁.sqrt
Proof state before:
case left
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
⊢ true =
    (decide ((v.get i).sqrt * (v.get i).sqrt ≤ v.get i) &&
      decide (v.get i < ((v.get i).sqrt + 1) * ((v.get i).sqrt + 1)))
Tactic:
symm
Proof state after:
case left
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
⊢ (decide ((v.get i).sqrt * (v.get i).sqrt ≤ v.get i) &&
      decide (v.get i < ((v.get i).sqrt + 1) * ((v.get i).sqrt + 1))) =
    true
Theorem: Nat.Arith₁.sqrt
Proof state before:
case left
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
⊢ (decide ((v.get i).sqrt * (v.get i).sqrt ≤ v.get i) &&
      decide (v.get i < ((v.get i).sqrt + 1) * ((v.get i).sqrt + 1))) =
    true
Tactic:
simp
Proof state after:
case left
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
⊢ (v.get i).sqrt * (v.get i).sqrt ≤ v.get i ∧ v.get i < ((v.get i).sqrt + 1) * ((v.get i).sqrt + 1)
Theorem: Nat.Arith₁.sqrt
Proof state before:
case left
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
⊢ (v.get i).sqrt * (v.get i).sqrt ≤ v.get i ∧ v.get i < ((v.get i).sqrt + 1) * ((v.get i).sqrt + 1)
Tactic:
constructor
Proof state after:
case left.left
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
⊢ (v.get i).sqrt * (v.get i).sqrt ≤ v.get i

case left.right
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
⊢ v.get i < ((v.get i).sqrt + 1) * ((v.get i).sqrt + 1)
Theorem: Nat.Arith₁.sqrt
Proof state before:
case left.left
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
⊢ (v.get i).sqrt * (v.get i).sqrt ≤ v.get i
Tactic:
exact sqrt_le (Vector.get v i)
Proof state after:
no goals
Theorem: Nat.Arith₁.sqrt
Proof state before:
case left.right
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
⊢ v.get i < ((v.get i).sqrt + 1) * ((v.get i).sqrt + 1)
Tactic:
exact lt_succ_sqrt (Vector.get v i)
Proof state after:
no goals
Theorem: Nat.Arith₁.sqrt
Proof state before:
case right
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
⊢ ∀ {m : ℕ}, m < (v.get i).sqrt → false = (decide (m * m ≤ v.get i) && decide (v.get i < (m + 1) * (m + 1)))
Tactic:
intro m hm
Proof state after:
case right
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
m : ℕ
hm : m < (v.get i).sqrt
⊢ false = (decide (m * m ≤ v.get i) && decide (v.get i < (m + 1) * (m + 1)))
Theorem: Nat.Arith₁.sqrt
Proof state before:
case right
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
m : ℕ
hm : m < (v.get i).sqrt
⊢ false = (decide (m * m ≤ v.get i) && decide (v.get i < (m + 1) * (m + 1)))
Tactic:
symm
Proof state after:
case right
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
m : ℕ
hm : m < (v.get i).sqrt
⊢ (decide (m * m ≤ v.get i) && decide (v.get i < (m + 1) * (m + 1))) = false
Theorem: Nat.Arith₁.sqrt
Proof state before:
case right
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
m : ℕ
hm : m < (v.get i).sqrt
⊢ (decide (m * m ≤ v.get i) && decide (v.get i < (m + 1) * (m + 1))) = false
Tactic:
simp only [Bool.and_eq_false_eq_eq_false_or_eq_false, decide_eq_false_iff_not, not_le, not_lt]
Proof state after:
case right
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
m : ℕ
hm : m < (v.get i).sqrt
⊢ v.get i < m * m ∨ (m + 1) * (m + 1) ≤ v.get i
Theorem: Nat.Arith₁.sqrt
Proof state before:
case right
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
m : ℕ
hm : m < (v.get i).sqrt
⊢ v.get i < m * m ∨ (m + 1) * (m + 1) ≤ v.get i
Tactic:
right
Proof state after:
case right.h
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
m : ℕ
hm : m < (v.get i).sqrt
⊢ (m + 1) * (m + 1) ≤ v.get i
Theorem: Nat.Arith₁.sqrt
Proof state before:
case right.h
n : ℕ
i : Fin n
this :
  ArithPart₁ fun v =>
    rfind fun x => Part.some (decide ((fun x x => x * x) v x ≤ v.get i ∧ v.get i < (fun x x => x * x) v (x + 1)))
v : Vector ℕ n
m : ℕ
hm : m < (v.get i).sqrt
⊢ (m + 1) * (m + 1) ≤ v.get i
Tactic:
exact Iff.mp le_sqrt hm
Proof state after:
no goals
Theorem: Nat.Arith₁.sub
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 =>
  (isEqNat (v.head + v.get j.succ) (v.get i.succ)).or
  ((isLtNat (v.get i.succ) (v.get j.succ)).and (isEqNat v.head 0))
Proof state after:
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
⊢ Arith₁ fun v => v.get i - v.get j