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

State before:
n : ℕ
p : Vector ℕ n → ℕ → ℕ
hp : Arith₁ fun v => p v.tail v.head
i : Fin n
⊢ Arith₁ fun v => (v.get i).ball (p v)
Tactic:
let F : Vector ℕ (n + 1) → ℕ := fun v => (p v.tail v.head).inv.or (isLeNat (v.get i.succ) v.head)
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)
⊢ Arith₁ fun v => (v.get i).ball (p v)

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)
⊢ Arith₁ fun v => (v.get i).ball (p v)
Tactic:
have hF : Arith₁ F := (or 0 1).comp₂ _ ((inv 0).comp₁ _ hp) ((le 0 1).comp₂ _ (proj i.succ) head)
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
⊢ Arith₁ fun v => (v.get i).ball (p v)

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
⊢ Arith₁ fun v => (v.get i).ball (p v)
Tactic:
have : @Arith₁ (n + 1) (fun v => isEqNat v.head (v.get i.succ)) :=
  (equal 0 1).comp₂ _ head (proj i.succ)
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)
⊢ Arith₁ fun v => (v.get i).ball (p v)

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)
⊢ Arith₁ fun v => (v.get i).ball (p v)
Tactic:
have := ArithPart₁.map (fun v x => isEqNat x (v.get i)) (this.of_eq $ by simp) (ArithPart₁.rfindPos hF)
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))))
⊢ Arith₁ fun v => (v.get i).ball (p v)

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)
⊢ ∀ (i_1 : Vector ℕ (n + 1)), i_1.head.isEqNat (i_1.get i.succ) = (fun v x => x.isEqNat (v.get i)) i_1.tail i_1.head
Tactic:
simp
State after:
no goals

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))))
⊢ ∀ (i_1 : Vector ℕ n),
    Part.map ((fun v x => x.isEqNat (v.get i)) i_1) (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ i_1)))) =
      (↑fun v => (v.get i).ball (p v)) i_1
Tactic:
intro v
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
⊢ Part.map ((fun v x => x.isEqNat (v.get i)) v) (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v)))) =
    (↑fun v => (v.get i).ball (p v)) v

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
⊢ Part.map ((fun v x => x.isEqNat (v.get i)) v) (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v)))) =
    (↑fun v => (v.get i).ball (p v)) v
Tactic:
simp only [tail_cons, head_cons, get_cons_succ, or_pos_iff, inv_pos_iff, not_lt,
  nonpos_iff_eq_zero, isLeNat_pos_iff, Bool.decide_or, PFun.coe_val, eq_some_iff, mem_map_iff,
  mem_rfind, mem_some_iff, F]
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
⊢ ∃ 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)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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
⊢ ∀ {m : ℕ}, m < x → false = (decide (p v m = 0) || decide (v.get i ≤ m))
Tactic:
intro m hm
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
m : ℕ
hm : m < x
⊢ false = (decide (p v m = 0) || decide (v.get i ≤ m))

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
m : ℕ
hm : m < x
⊢ false = (decide (p v m = 0) || decide (v.get i ≤ m))
Tactic:
symm
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
m : ℕ
hm : m < x
⊢ (decide (p v m = 0) || decide (v.get i ≤ m)) = false

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
m : ℕ
hm : m < x
⊢ (decide (p v m = 0) || decide (v.get i ≤ m)) = false
Tactic:
simp[hlx m hm, lt_trans hm hx]
State after:
no goals

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
⊢ x.isEqNat (v.get i) = (v.get i).ball (p v)
Tactic:
have : isEqNat x (v.get i) = 0 := by simp[isEqNat, imp_false]; exact ne_of_lt hx
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
this : x.isEqNat (v.get i) = 0
⊢ x.isEqNat (v.get i) = (v.get i).ball (p v)

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
this : x.isEqNat (v.get i) = 0
⊢ x.isEqNat (v.get i) = (v.get i).ball (p v)
Tactic:
simp[this]
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
this : x.isEqNat (v.get i) = 0
⊢ 0 = (v.get i).ball (p v)

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
this : x.isEqNat (v.get i) = 0
⊢ 0 = (v.get i).ball (p v)
Tactic:
symm
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
this : x.isEqNat (v.get i) = 0
⊢ (v.get i).ball (p v) = 0

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
this : x.isEqNat (v.get i) = 0
⊢ (v.get i).ball (p v) = 0
Tactic:
simp
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
this : x.isEqNat (v.get i) = 0
⊢ ∃ m < v.get i, p v m = 0

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
this : x.isEqNat (v.get i) = 0
⊢ ∃ m < v.get i, p v m = 0
Tactic:
exact ⟨x, hx, hpx⟩
State after:
no goals

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
⊢ x.isEqNat (v.get i) = 0
Tactic:
simp[isEqNat, imp_false]
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
⊢ ¬x = v.get i

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
⊢ ¬x = v.get i
Tactic:
exact ne_of_lt hx
State after:
no goals