internlm/Lean-Github huggingface dataset:
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
⊢ ∃ 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)
Tactic:
by_cases H : ∀ m < v.get i, 0 < p v m
Proof state after:
case pos
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
H : ∀ m < v.get i, 0 < p v m
⊢ ∃ 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)

case neg
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
H : ¬∀ m < v.get i, 0 < p v m
⊢ ∃ 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)
Theorem: Nat.Arith₁.ball
Proof state before:
case pos
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
H : ∀ m < v.get i, 0 < p v m
⊢ ∃ 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)
Tactic:
exact ⟨v.get i,
  ⟨by symm; simp, by intro m hm; symm; simp[hm]; exact Nat.not_eq_zero_of_lt (H m hm)⟩,
  by { simp[isEqNat]; symm; exact ball_pos_iff_eq_one.mpr (by simpa) }⟩
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))))
v : Vector ℕ n
H : ∀ m < v.get i, 0 < p v m
⊢ true = (decide (p v (v.get i) = 0) || decide (v.get i ≤ v.get i))
Tactic:
symm
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
H : ∀ m < v.get i, 0 < p v m
⊢ (decide (p v (v.get i) = 0) || decide (v.get i ≤ v.get i)) = true
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
H : ∀ m < v.get i, 0 < p v m
⊢ (decide (p v (v.get i) = 0) || decide (v.get i ≤ v.get i)) = true
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))))
v : Vector ℕ n
H : ∀ m < v.get i, 0 < p v m
⊢ ∀ {m : ℕ}, m < v.get i → false = (decide (p v m = 0) || decide (v.get i ≤ m))
Tactic:
intro m hm
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
H : ∀ m < v.get i, 0 < p v m
m : ℕ
hm : m < v.get i
⊢ false = (decide (p v m = 0) || decide (v.get i ≤ m))
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
H : ∀ m < v.get i, 0 < p v m
m : ℕ
hm : m < v.get i
⊢ false = (decide (p v m = 0) || decide (v.get i ≤ m))
Tactic:
symm
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
H : ∀ m < v.get i, 0 < p v m
m : ℕ
hm : m < v.get i
⊢ (decide (p v m = 0) || decide (v.get i ≤ m)) = false
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
H : ∀ m < v.get i, 0 < p v m
m : ℕ
hm : m < v.get i
⊢ (decide (p v m = 0) || decide (v.get i ≤ m)) = false
Tactic:
simp[hm]
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
H : ∀ m < v.get i, 0 < p v m
m : ℕ
hm : m < v.get i
⊢ ¬p v m = 0
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
H : ∀ m < v.get i, 0 < p v m
m : ℕ
hm : m < v.get i
⊢ ¬p v m = 0
Tactic:
exact Nat.not_eq_zero_of_lt (H m hm)
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))))
v : Vector ℕ n
H : ∀ m < v.get i, 0 < p v m
⊢ (v.get i).isEqNat (v.get i) = (v.get i).ball (p v)
Tactic:
simp[isEqNat]
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
H : ∀ m < v.get i, 0 < p v m
⊢ 1 = (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)
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
H : ∀ m < v.get i, 0 < p v m
⊢ 1 = (v.get i).ball (p v)
Tactic:
symm
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
H : ∀ m < v.get i, 0 < p v m
⊢ (v.get i).ball (p v) = 1
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
H : ∀ m < v.get i, 0 < p v m
⊢ (v.get i).ball (p v) = 1
Tactic:
exact ball_pos_iff_eq_one.mpr (by simpa)
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))))
v : Vector ℕ n
H : ∀ m < v.get i, 0 < p v m
⊢ 0 < (v.get i).ball (p v)
Tactic:
simpa
Proof state after:
no goals
Theorem: Nat.Arith₁.ball
Proof state before:
case neg
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
H : ¬∀ m < v.get i, 0 < p v m
⊢ ∃ 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)
Tactic:
have : ∃ x < Vector.get v i, p v x = 0 ∧ ∀ y < x, p v y ≠ 0 := by
  simp at H; rcases least_number _ H with ⟨x, hx, hxl⟩
  exact ⟨x, hx.1, hx.2, by
    intro y hy; have : y < v.get i → p v y ≠ 0 := by simpa using hxl y hy
    exact this (lt_trans hy hx.1)⟩
Proof state after:
case neg
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
H : ¬∀ m < v.get i, 0 < p v m
this : ∃ x < v.get i, p v x = 0 ∧ ∀ y < x, p v y ≠ 0
⊢ ∃ 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)
Theorem: Nat.Arith₁.ball
Proof state before:
case neg
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
H : ¬∀ m < v.get i, 0 < p v m
this : ∃ x < v.get i, p v x = 0 ∧ ∀ y < x, p v y ≠ 0
⊢ ∃ 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)
Tactic:
rcases this with ⟨x, hx, hpx, hlx⟩
Proof state after:
case neg.intro.intro.intro
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
H : ¬∀ m < v.get i, 0 < p v m
x : ℕ
hx : x < v.get i
hpx : p v x = 0
hlx : ∀ y < x, p v y ≠ 0
⊢ ∃ 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)
Theorem: Nat.Arith₁.ball
Proof state before:
case neg.intro.intro.intro
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
H : ¬∀ m < v.get i, 0 < p v m
x : ℕ
hx : x < v.get i
hpx : p v x = 0
hlx : ∀ y < x, p v y ≠ 0
⊢ ∃ 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)
Tactic:
exact ⟨x, ⟨by symm; simp[hpx], by intro m hm; symm; simp[hlx m hm, lt_trans hm hx]⟩, by
  have : isEqNat x (v.get i) = 0 := by simp[isEqNat, imp_false]; exact ne_of_lt hx
  simp[this]; symm; simp; exact ⟨x, hx, hpx⟩⟩
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))))
v : Vector ℕ n
H : ¬∀ m < v.get i, 0 < p v m
⊢ ∃ x < v.get i, p v x = 0 ∧ ∀ y < x, p v y ≠ 0
Tactic:
simp at H
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
H : ∃ x < v.get i, p v x = 0
⊢ ∃ x < v.get i, p v x = 0 ∧ ∀ y < x, p v y ≠ 0
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
H : ∃ x < v.get i, p v x = 0
⊢ ∃ x < v.get i, p v x = 0 ∧ ∀ y < x, p v y ≠ 0
Tactic:
rcases least_number _ H with ⟨x, hx, hxl⟩
Proof state after:
case intro.intro
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
H : ∃ x < v.get i, p v x = 0
x : ℕ
hx : x < v.get i ∧ p v x = 0
hxl : ∀ z < x, ¬(z < v.get i ∧ p v z = 0)
⊢ ∃ x < v.get i, p v x = 0 ∧ ∀ y < x, p v y ≠ 0
Theorem: Nat.Arith₁.ball
Proof state before:
case intro.intro
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
H : ∃ x < v.get i, p v x = 0
x : ℕ
hx : x < v.get i ∧ p v x = 0
hxl : ∀ z < x, ¬(z < v.get i ∧ p v z = 0)
⊢ ∃ x < v.get i, p v x = 0 ∧ ∀ y < x, p v y ≠ 0
Tactic:
exact ⟨x, hx.1, hx.2, by
  intro y hy; have : y < v.get i → p v y ≠ 0 := by simpa using hxl y hy
  exact this (lt_trans hy hx.1)⟩
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))))
v : Vector ℕ n
H : ∃ x < v.get i, p v x = 0
x : ℕ
hx : x < v.get i ∧ p v x = 0
hxl : ∀ z < x, ¬(z < v.get i ∧ p v z = 0)
⊢ ∀ y < x, p v y ≠ 0
Tactic:
intro y hy
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
H : ∃ x < v.get i, p v x = 0
x : ℕ
hx : x < v.get i ∧ p v x = 0
hxl : ∀ z < x, ¬(z < v.get i ∧ p v z = 0)
y : ℕ
hy : y < x
⊢ p v y ≠ 0
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
H : ∃ x < v.get i, p v x = 0
x : ℕ
hx : x < v.get i ∧ p v x = 0
hxl : ∀ z < x, ¬(z < v.get i ∧ p v z = 0)
y : ℕ
hy : y < x
⊢ p v y ≠ 0
Tactic:
have : y < v.get i → p v y ≠ 0 := by simpa using hxl y hy
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
H : ∃ x < v.get i, p v x = 0
x : ℕ
hx : x < v.get i ∧ p v x = 0
hxl : ∀ z < x, ¬(z < v.get i ∧ p v z = 0)
y : ℕ
hy : y < x
this : y < v.get i → p v y ≠ 0
⊢ p v y ≠ 0
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
H : ∃ x < v.get i, p v x = 0
x : ℕ
hx : x < v.get i ∧ p v x = 0
hxl : ∀ z < x, ¬(z < v.get i ∧ p v z = 0)
y : ℕ
hy : y < x
this : y < v.get i → p v y ≠ 0
⊢ p v y ≠ 0
Tactic:
exact this (lt_trans hy hx.1)
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))))
v : Vector ℕ n
H : ∃ x < v.get i, p v x = 0
x : ℕ
hx : x < v.get i ∧ p v x = 0
hxl : ∀ z < x, ¬(z < v.get i ∧ p v z = 0)
y : ℕ
hy : y < x
⊢ y < v.get i → p v y ≠ 0
Tactic:
simpa using hxl y hy
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))))
v : Vector ℕ n
H : ¬∀ m < v.get i, 0 < p v m
x : ℕ
hx : x < v.get i
hpx : p v x = 0
hlx : ∀ y < x, p v y ≠ 0
⊢ true = (decide (p v x = 0) || decide (v.get i ≤ x))
Tactic:
symm
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
H : ¬∀ m < v.get i, 0 < p v m
x : ℕ
hx : x < v.get i
hpx : p v x = 0
hlx : ∀ y < x, p v y ≠ 0
⊢ (decide (p v x = 0) || decide (v.get i ≤ x)) = true
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
H : ¬∀ m < v.get i, 0 < p v m
x : ℕ
hx : x < v.get i
hpx : p v x = 0
hlx : ∀ y < x, p v y ≠ 0
⊢ (decide (p v x = 0) || decide (v.get i ≤ x)) = true
Tactic:
simp[hpx]
Proof state after:
no goals