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

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

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

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

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

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