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

State before:
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
i : Fin n.succ
⊢ ArithPart₁ ((g :> fun i v => ↑(Option.some (v.get i))) i)
Tactic:
cases i using Fin.cases <;> simp[*]
State after:
case succ
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
i✝ : Fin n
⊢ ArithPart₁ fun v => Part.some (v.get i✝)

State before:
case succ
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
i✝ : Fin n
⊢ ArithPart₁ fun v => Part.some (v.get i✝)
Tactic:
exact proj _
State after:
no goals

State before:
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
⊢ ∀ (i : Vector ℕ n),
    (do
        let v ← mOfFn fun i_1 => (g :> fun i v => ↑(Option.some (v.get i))) i_1 i
        f v.tail v.head) =
      (g i).bind (f i)
Tactic:
intro v
State after:
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
⊢ (do
      let v ← mOfFn fun i => (g :> fun i v => ↑(Option.some (v.get i))) i v
      f v.tail v.head) =
    (g v).bind (f v)

State before:
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
⊢ (do
      let v ← mOfFn fun i => (g :> fun i v => ↑(Option.some (v.get i))) i v
      f v.tail v.head) =
    (g v).bind (f v)
Tactic:
simp
State after:
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
⊢ ((mOfFn fun i => (g :> fun i v => Part.some (v.get i)) i v).bind fun v => f v.tail v.head) = (g v).bind (f v)

State before:
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
⊢ ((mOfFn fun i => (g :> fun i v => Part.some (v.get i)) i v).bind fun v => f v.tail v.head) = (g v).bind (f v)
Tactic:
rcases Part.eq_none_or_eq_some (g v) with (hgv | ⟨x, hgv⟩)
State after:
case inl
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
hgv : g v = Part.none
⊢ ((mOfFn fun i => (g :> fun i v => Part.some (v.get i)) i v).bind fun v => f v.tail v.head) = (g v).bind (f v)

case inr.intro
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
x : ℕ
hgv : g v = Part.some x
⊢ ((mOfFn fun i => (g :> fun i v => Part.some (v.get i)) i v).bind fun v => f v.tail v.head) = (g v).bind (f v)

State before:
case inl
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
hgv : g v = Part.none
⊢ ((mOfFn fun i => (g :> fun i v => Part.some (v.get i)) i v).bind fun v => f v.tail v.head) = (g v).bind (f v)
Tactic:
simp[hgv, mOfFn]
State after:
no goals

State before:
case inr.intro
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
x : ℕ
hgv : g v = Part.some x
⊢ ((mOfFn fun i => (g :> fun i v => Part.some (v.get i)) i v).bind fun v => f v.tail v.head) = (g v).bind (f v)
Tactic:
simp[hgv, Matrix.comp_vecCons']
State after:
case inr.intro
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
x : ℕ
hgv : g v = Part.some x
⊢ ((mOfFn fun i => (g :> fun i v => Part.some (v.get i)) i v).bind fun v => f v.tail v.head) = f v x

State before:
case inr.intro
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
x : ℕ
hgv : g v = Part.some x
⊢ ((mOfFn fun i => (g :> fun i v => Part.some (v.get i)) i v).bind fun v => f v.tail v.head) = f v x
Tactic:
have : mOfFn (fun i => (g :> fun j v => Part.some $ v.get j) i v) = pure (Vector.ofFn (x :> fun j => v.get j)) := by
  rw[←Vector.mOfFn_pure]; apply congr_arg
  funext i; cases i using Fin.cases <;> simp[hgv]
State after:
case inr.intro
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
x : ℕ
hgv : g v = Part.some x
this : (mOfFn fun i => (g :> fun j v => Part.some (v.get j)) i v) = pure (ofFn (x :> fun j => v.get j))
⊢ ((mOfFn fun i => (g :> fun i v => Part.some (v.get i)) i v).bind fun v => f v.tail v.head) = f v x

State before:
case inr.intro
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
x : ℕ
hgv : g v = Part.some x
this : (mOfFn fun i => (g :> fun j v => Part.some (v.get j)) i v) = pure (ofFn (x :> fun j => v.get j))
⊢ ((mOfFn fun i => (g :> fun i v => Part.some (v.get i)) i v).bind fun v => f v.tail v.head) = f v x
Tactic:
simp[this]
State after:
no goals

State before:
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
x : ℕ
hgv : g v = Part.some x
⊢ (mOfFn fun i => (g :> fun j v => Part.some (v.get j)) i v) = pure (ofFn (x :> fun j => v.get j))
Tactic:
rw[←Vector.mOfFn_pure]
State after:
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
x : ℕ
hgv : g v = Part.some x
⊢ (mOfFn fun i => (g :> fun j v => Part.some (v.get j)) i v) = mOfFn fun i => pure ((x :> fun j => v.get j) i)

State before:
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
x : ℕ
hgv : g v = Part.some x
⊢ (mOfFn fun i => (g :> fun j v => Part.some (v.get j)) i v) = mOfFn fun i => pure ((x :> fun j => v.get j) i)
Tactic:
apply congr_arg
State after:
case h
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
x : ℕ
hgv : g v = Part.some x
⊢ (fun i => (g :> fun j v => Part.some (v.get j)) i v) = fun i => pure ((x :> fun j => v.get j) i)

State before:
case h
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
x : ℕ
hgv : g v = Part.some x
⊢ (fun i => (g :> fun j v => Part.some (v.get j)) i v) = fun i => pure ((x :> fun j => v.get j) i)
Tactic:
funext i
State after:
case h.h
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
x : ℕ
hgv : g v = Part.some x
i : Fin n.succ
⊢ (g :> fun j v => Part.some (v.get j)) i v = pure ((x :> fun j => v.get j) i)

State before:
case h.h
n : ℕ
f : Vector ℕ n → ℕ →. ℕ
hf : ArithPart₁ fun v => f v.tail v.head
g : Vector ℕ n →. ℕ
hg : ArithPart₁ g
v : Vector ℕ n
x : ℕ
hgv : g v = Part.some x
i : Fin n.succ
⊢ (g :> fun j v => Part.some (v.get j)) i v = pure ((x :> fun j => v.get j) i)
Tactic:
cases i using Fin.cases <;> simp[hgv]
State after:
no goals