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

State before:
n : ℕ
f : Vector ℕ n → ℕ → ℕ
hf : Arith₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
⊢ ∀ (i : Vector ℕ (n + 1)), (↑fun v => f v.tail v.head) i = (fun x x_1 => Part.some (f x x_1)) i.tail i.head
Tactic:
simp
State after:
no goals

State before:
n : ℕ
f : Vector ℕ n → ℕ → ℕ
hf : Arith₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
⊢ ∀ (i : Vector ℕ n), ((g i).bind fun x => Part.some (f i x)) = Part.map (f i) (g i)
Tactic:
intro v
State after:
n : ℕ
f : Vector ℕ n → ℕ → ℕ
hf : Arith₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
⊢ ((g v).bind fun x => Part.some (f v x)) = Part.map (f v) (g v)

State before:
n : ℕ
f : Vector ℕ n → ℕ → ℕ
hf : Arith₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
⊢ ((g v).bind fun x => Part.some (f v x)) = Part.map (f v) (g v)
Tactic:
rcases Part.eq_none_or_eq_some (g v) with (_ | ⟨x, _⟩) <;> simp[*]
State after:
no goals