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

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

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

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

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

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

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