internlm/Lean-Github huggingface dataset:
Theorem: Nat.Arith₁.sub
Proof state before:
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
Tactic:
have : Arith₁ F :=
  (or 0 1).comp₂ _
    ((equal 0 1).comp₂ _ ((add 0 1).comp₂ _ head (proj j.succ)) (proj i.succ))
    ((and 0 1).comp₂ _ ((lt 0 1).comp₂ _ (proj i.succ) (proj j.succ)) ((equal 0 1).comp₂ _ head zero))
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))
this : Arith₁ F
⊢ Arith₁ fun v => v.get i - v.get j
Theorem: Nat.Arith₁.sub
Proof state before:
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))
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.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))
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₁.sub
Proof state before:
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))
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 only [head_cons, get_cons_succ, or_pos_iff, isEqNat_pos_iff, and_pos_iff,
  isLtNat_pos_iff, Bool.decide_or, Bool.decide_and, PFun.coe_val, eq_some_iff, mem_rfind,
  mem_some_iff, F]
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))
this : Arith₁ F
v : Vector ℕ n
⊢ true =
      (decide (v.get i - v.get j + v.get j = v.get i) || decide (v.get i < v.get j) && decide (v.get i - v.get j = 0)) ∧
    ∀ {m : ℕ},
      m < v.get i - v.get j → false = (decide (m + v.get j = v.get i) || decide (v.get i < v.get j) && decide (m = 0))
Theorem: Nat.Arith₁.sub
Proof state before:
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))
this : Arith₁ F
v : Vector ℕ n
⊢ true =
      (decide (v.get i - v.get j + v.get j = v.get i) || decide (v.get i < v.get j) && decide (v.get i - v.get j = 0)) ∧
    ∀ {m : ℕ},
      m < v.get i - v.get j → false = (decide (m + v.get j = v.get i) || decide (v.get i < v.get j) && decide (m = 0))
Tactic:
constructor
Proof state after:
case left
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))
this : Arith₁ F
v : Vector ℕ n
⊢ true =
    (decide (v.get i - v.get j + v.get j = v.get i) || decide (v.get i < v.get j) && decide (v.get i - v.get j = 0))

case right
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))
this : Arith₁ F
v : Vector ℕ n
⊢ ∀ {m : ℕ},
    m < v.get i - v.get j → false = (decide (m + v.get j = v.get i) || decide (v.get i < v.get j) && decide (m = 0))
Theorem: Nat.Arith₁.sub
Proof state before:
case left
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))
this : Arith₁ F
v : Vector ℕ n
⊢ true =
    (decide (v.get i - v.get j + v.get j = v.get i) || decide (v.get i < v.get j) && decide (v.get i - v.get j = 0))
Tactic:
symm
Proof state after:
case left
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))
this : Arith₁ F
v : Vector ℕ n
⊢ (decide (v.get i - v.get j + v.get j = v.get i) || decide (v.get i < v.get j) && decide (v.get i - v.get j = 0)) =
    true
Theorem: Nat.Arith₁.sub
Proof state before:
case left
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))
this : Arith₁ F
v : Vector ℕ n
⊢ (decide (v.get i - v.get j + v.get j = v.get i) || decide (v.get i < v.get j) && decide (v.get i - v.get j = 0)) =
    true
Tactic:
simp
Proof state after:
case left
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))
this : Arith₁ F
v : Vector ℕ n
⊢ v.get i - v.get j + v.get j = v.get i ∨ v.get i < v.get j ∧ v.get i - v.get j = 0
Theorem: Nat.Arith₁.sub
Proof state before:
case left
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))
this : Arith₁ F
v : Vector ℕ n
⊢ v.get i - v.get j + v.get j = v.get i ∨ v.get i < v.get j ∧ v.get i - v.get j = 0
Tactic:
have : v.get i < v.get j ∨ v.get j ≤ v.get i := Nat.lt_or_ge _ _
Proof state after:
case left
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))
this✝ : Arith₁ F
v : Vector ℕ n
this : v.get i < v.get j ∨ v.get j ≤ v.get i
⊢ v.get i - v.get j + v.get j = v.get i ∨ v.get i < v.get j ∧ v.get i - v.get j = 0
Theorem: Nat.Arith₁.sub
Proof state before:
case left
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))
this✝ : Arith₁ F
v : Vector ℕ n
this : v.get i < v.get j ∨ v.get j ≤ v.get i
⊢ v.get i - v.get j + v.get j = v.get i ∨ v.get i < v.get j ∧ v.get i - v.get j = 0
Tactic:
rcases this with (hv | hv)
Proof state after:
case left.inl
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))
this : Arith₁ F
v : Vector ℕ n
hv : v.get i < v.get j
⊢ v.get i - v.get j + v.get j = v.get i ∨ v.get i < v.get j ∧ v.get i - v.get j = 0

case left.inr
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))
this : Arith₁ F
v : Vector ℕ n
hv : v.get j ≤ v.get i
⊢ v.get i - v.get j + v.get j = v.get i ∨ v.get i < v.get j ∧ v.get i - v.get j = 0
Theorem: Nat.Arith₁.sub
Proof state before:
case left.inl
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))
this : Arith₁ F
v : Vector ℕ n
hv : v.get i < v.get j
⊢ v.get i - v.get j + v.get j = v.get i ∨ v.get i < v.get j ∧ v.get i - v.get j = 0
Tactic:
right
Proof state after:
case left.inl.h
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))
this : Arith₁ F
v : Vector ℕ n
hv : v.get i < v.get j
⊢ v.get i < v.get j ∧ v.get i - v.get j = 0
Theorem: Nat.Arith₁.sub
Proof state before:
case left.inl.h
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))
this : Arith₁ F
v : Vector ℕ n
hv : v.get i < v.get j
⊢ v.get i < v.get j ∧ v.get i - v.get j = 0
Tactic:
exact ⟨hv, Nat.sub_eq_zero_of_le (Nat.le_of_lt hv)⟩
Proof state after:
no goals
Theorem: Nat.Arith₁.sub
Proof state before:
case left.inr
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))
this : Arith₁ F
v : Vector ℕ n
hv : v.get j ≤ v.get i
⊢ v.get i - v.get j + v.get j = v.get i ∨ v.get i < v.get j ∧ v.get i - v.get j = 0
Tactic:
left
Proof state after:
case left.inr.h
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))
this : Arith₁ F
v : Vector ℕ n
hv : v.get j ≤ v.get i
⊢ v.get i - v.get j + v.get j = v.get i
Theorem: Nat.Arith₁.sub
Proof state before:
case left.inr.h
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))
this : Arith₁ F
v : Vector ℕ n
hv : v.get j ≤ v.get i
⊢ v.get i - v.get j + v.get j = v.get i
Tactic:
exact Nat.sub_add_cancel hv
Proof state after:
no goals
Theorem: Nat.Arith₁.sub
Proof state before:
case right
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))
this : Arith₁ F
v : Vector ℕ n
⊢ ∀ {m : ℕ},
    m < v.get i - v.get j → false = (decide (m + v.get j = v.get i) || decide (v.get i < v.get j) && decide (m = 0))
Tactic:
intro m hm
Proof state after:
case right
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))
this : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i - v.get j
⊢ false = (decide (m + v.get j = v.get i) || decide (v.get i < v.get j) && decide (m = 0))
Theorem: Nat.Arith₁.sub
Proof state before:
case right
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))
this : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i - v.get j
⊢ false = (decide (m + v.get j = v.get i) || decide (v.get i < v.get j) && decide (m = 0))
Tactic:
symm
Proof state after:
case right
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))
this : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i - v.get j
⊢ (decide (m + v.get j = v.get i) || decide (v.get i < v.get j) && decide (m = 0)) = false
Theorem: Nat.Arith₁.sub
Proof state before:
case right
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))
this : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i - v.get j
⊢ (decide (m + v.get j = v.get i) || decide (v.get i < v.get j) && decide (m = 0)) = false
Tactic:
simp only [Bool.or_eq_false_eq_eq_false_and_eq_false,
  decide_eq_false_iff_not, Bool.and_eq_false_eq_eq_false_or_eq_false, not_lt]
Proof state after:
case right
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))
this : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i - v.get j
⊢ ¬m + v.get j = v.get i ∧ (v.get j ≤ v.get i ∨ ¬m = 0)
Theorem: Nat.Arith₁.sub
Proof state before:
case right
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))
this : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i - v.get j
⊢ ¬m + v.get j = v.get i ∧ (v.get j ≤ v.get i ∨ ¬m = 0)
Tactic:
have : m + v.get j < v.get i := add_lt_of_lt_sub hm
Proof state after:
case right
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))
this✝ : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i - v.get j
this : m + v.get j < v.get i
⊢ ¬m + v.get j = v.get i ∧ (v.get j ≤ v.get i ∨ ¬m = 0)
Theorem: Nat.Arith₁.sub
Proof state before:
case right
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))
this✝ : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i - v.get j
this : m + v.get j < v.get i
⊢ ¬m + v.get j = v.get i ∧ (v.get j ≤ v.get i ∨ ¬m = 0)
Tactic:
exact ⟨ne_of_lt this, by left; exact le_trans le_add_self (le_of_lt this)⟩
Proof state after:
no goals
Theorem: Nat.Arith₁.sub
Proof state before:
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))
this✝ : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i - v.get j
this : m + v.get j < v.get i
⊢ v.get j ≤ v.get i ∨ ¬m = 0
Tactic:
left
Proof state after:
case h
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))
this✝ : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i - v.get j
this : m + v.get j < v.get i
⊢ v.get j ≤ v.get i
Theorem: Nat.Arith₁.sub
Proof state before:
case h
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))
this✝ : Arith₁ F
v : Vector ℕ n
m : ℕ
hm : m < v.get i - v.get j
this : m + v.get j < v.get i
⊢ v.get j ≤ v.get i
Tactic:
exact le_trans le_add_self (le_of_lt this)
Proof state after:
no goals
Theorem: Nat.Arith₁.pair
Proof state before:
n : ℕ
i j : Fin n
⊢ Arith₁ fun v => (v.get i).pair (v.get j)
Tactic:
have := if_pos (lt i j)
  ((add 0 1).comp₂ _ (mul j j) (proj i))
  ((add 0 1).comp₂ _ ((add 0 1).comp₂ _ (mul i i) (proj i)) (proj j))
Proof state after:
n : ℕ
i j : Fin n
this :
  Arith₁ fun v =>
    if 0 < (v.get i).isLtNat (v.get j) then v.get j * v.get j + v.get i else v.get i * v.get i + v.get i + v.get j
⊢ Arith₁ fun v => (v.get i).pair (v.get j)
Theorem: Nat.Arith₁.pair
Proof state before:
n : ℕ
i j : Fin n
this :
  Arith₁ fun v =>
    if 0 < (v.get i).isLtNat (v.get j) then v.get j * v.get j + v.get i else v.get i * v.get i + v.get i + v.get j
⊢ Arith₁ fun v => (v.get i).pair (v.get j)
Tactic:
exact this.of_eq <| by
  intro v; simp[pair]
Proof state after:
no goals
Theorem: Nat.Arith₁.pair
Proof state before:
n : ℕ
i j : Fin n
this :
  Arith₁ fun v =>
    if 0 < (v.get i).isLtNat (v.get j) then v.get j * v.get j + v.get i else v.get i * v.get i + v.get i + v.get j
⊢ ∀ (i_1 : Vector ℕ n),
    (if 0 < (i_1.get i).isLtNat (i_1.get j) then i_1.get j * i_1.get j + i_1.get i
      else i_1.get i * i_1.get i + i_1.get i + i_1.get j) =
      (i_1.get i).pair (i_1.get j)
Tactic:
intro v
Proof state after:
n : ℕ
i j : Fin n
this :
  Arith₁ fun v =>
    if 0 < (v.get i).isLtNat (v.get j) then v.get j * v.get j + v.get i else v.get i * v.get i + v.get i + v.get j
v : Vector ℕ n
⊢ (if 0 < (v.get i).isLtNat (v.get j) then v.get j * v.get j + v.get i else v.get i * v.get i + v.get i + v.get j) =
    (v.get i).pair (v.get j)
Theorem: Nat.Arith₁.pair
Proof state before:
n : ℕ
i j : Fin n
this :
  Arith₁ fun v =>
    if 0 < (v.get i).isLtNat (v.get j) then v.get j * v.get j + v.get i else v.get i * v.get i + v.get i + v.get j
v : Vector ℕ n
⊢ (if 0 < (v.get i).isLtNat (v.get j) then v.get j * v.get j + v.get i else v.get i * v.get i + v.get i + v.get j) =
    (v.get i).pair (v.get j)
Tactic:
simp[pair]
Proof state after:
no goals
Theorem: Nat.Arith₁.unpair₁
Proof state before:
n : ℕ
i : Fin n
⊢ Arith₁ fun v => (v.get i).unpair.1
Tactic:
have hf : Arith₁ (fun v => isLtNat (v.get i - (v.get i).sqrt * (v.get i).sqrt) (v.get i).sqrt) :=
  (lt 0 1).comp₂ _
    ((Arith₁.sub 0 1).comp₂ _ (proj i) ((mul 0 1).comp₂ _ (Arith₁.sqrt i) (Arith₁.sqrt i)))
    (Arith₁.sqrt i)
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
⊢ Arith₁ fun v => (v.get i).unpair.1
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
⊢ Arith₁ fun v => (v.get i).unpair.1
Tactic:
have hg : Arith₁ (fun v => v.get i - (v.get i).sqrt * (v.get i).sqrt) :=
  (sub 0 1).comp₂ _ (proj i) ((mul 0 1).comp₂ _ (Arith₁.sqrt i) (Arith₁.sqrt i))
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 - (v.get i).sqrt * (v.get i).sqrt
⊢ Arith₁ fun v => (v.get i).unpair.1
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 - (v.get i).sqrt * (v.get i).sqrt
⊢ Arith₁ fun v => (v.get i).unpair.1
Tactic:
have hh : Arith₁ (fun v => sqrt (v.get i)) := Arith₁.sqrt i
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 - (v.get i).sqrt * (v.get i).sqrt
hh : Arith₁ fun v => (v.get i).sqrt
⊢ Arith₁ fun v => (v.get i).unpair.1
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 - (v.get i).sqrt * (v.get i).sqrt
hh : Arith₁ fun v => (v.get i).sqrt
⊢ Arith₁ fun v => (v.get i).unpair.1
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 - (v.get i).sqrt * (v.get i).sqrt
hh : Arith₁ fun v => (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 - (v.get i).sqrt * (v.get i).sqrt
    else (v.get i).sqrt
⊢ Arith₁ fun v => (v.get i).unpair.1
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 - (v.get i).sqrt * (v.get i).sqrt
hh : Arith₁ fun v => (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 - (v.get i).sqrt * (v.get i).sqrt
    else (v.get i).sqrt
⊢ Arith₁ fun v => (v.get i).unpair.1
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 - (v.get i).sqrt * (v.get i).sqrt
hh : Arith₁ fun v => (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 - (v.get i).sqrt * (v.get i).sqrt
    else (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 - (i_1.get i).sqrt * (i_1.get i).sqrt
      else (i_1.get i).sqrt) =
      (i_1.get i).unpair.1
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 - (v.get i).sqrt * (v.get i).sqrt
hh : Arith₁ fun v => (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 - (v.get i).sqrt * (v.get i).sqrt
    else (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 - (v.get i).sqrt * (v.get i).sqrt
    else (v.get i).sqrt) =
    (v.get i).unpair.1
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 - (v.get i).sqrt * (v.get i).sqrt
hh : Arith₁ fun v => (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 - (v.get i).sqrt * (v.get i).sqrt
    else (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 - (v.get i).sqrt * (v.get i).sqrt
    else (v.get i).sqrt) =
    (v.get i).unpair.1
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 - (v.get i).sqrt * (v.get i).sqrt
hh : Arith₁ fun v => (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 - (v.get i).sqrt * (v.get i).sqrt
    else (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 - (v.get i).sqrt * (v.get i).sqrt
    else (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)).1
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 - (v.get i).sqrt * (v.get i).sqrt
hh : Arith₁ fun v => (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 - (v.get i).sqrt * (v.get i).sqrt
    else (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 - (v.get i).sqrt * (v.get i).sqrt
    else (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)).1
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₁.unpair₂
Proof state before:
n : ℕ
i : Fin n
⊢ Arith₁ fun v => (v.get i).unpair.2
Tactic:
have hf : Arith₁ (fun v => isLtNat (v.get i - (v.get i).sqrt * (v.get i).sqrt) (v.get i).sqrt) :=
  (lt 0 1).comp₂ _
    ((Arith₁.sub 0 1).comp₂ _ (proj i) ((mul 0 1).comp₂ _ (Arith₁.sqrt i) (Arith₁.sqrt i)))
    (Arith₁.sqrt i)
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
⊢ 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
⊢ Arith₁ fun v => (v.get i).unpair.2
Tactic:
have hg : Arith₁ (fun v => sqrt (v.get i)) := Arith₁.sqrt i
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
⊢ 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
⊢ Arith₁ fun v => (v.get i).unpair.2
Tactic:
have hh : Arith₁ (fun v => v.get i - (v.get i).sqrt * (v.get i).sqrt - (v.get i).sqrt) :=
  (sub 0 1).comp₂ _ ((sub 0 1).comp₂ _ (proj i) ((mul 0 1).comp₂ _ (Arith₁.sqrt i) (Arith₁.sqrt i))) (Arith₁.sqrt i)
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
⊢ Arith₁ fun v => (v.get i).unpair.2