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

State before:
f : ℕ → ℕ →. ℕ
hf : ArithPart₁ fun v => f (v.get 0) (v.get 1)
n : ℕ
g h : Vector ℕ n → ℕ
hg : Arith₁ g
hh : Arith₁ h
i✝ : Fin (succ 0).succ
i : Fin 1
⊢ ArithPart₁ (![↑g, ↑h] i.succ)
Tactic:
simpa using hh
State after:
no goals

State before:
f : ℕ → ℕ →. ℕ
hf : ArithPart₁ fun v => f (v.get 0) (v.get 1)
n : ℕ
g h : Vector ℕ n → ℕ
hg : Arith₁ g
hh : Arith₁ h
⊢ ∀ (i : Vector ℕ n),
    (do
        let v ← mOfFn fun i_1 => ![↑g, ↑h] i_1 i
        f (v.get 0) (v.get 1)) =
      f (g i) (h i)
Tactic:
intro i
State after:
f : ℕ → ℕ →. ℕ
hf : ArithPart₁ fun v => f (v.get 0) (v.get 1)
n : ℕ
g h : Vector ℕ n → ℕ
hg : Arith₁ g
hh : Arith₁ h
i : Vector ℕ n
⊢ (do
      let v ← mOfFn fun i_1 => ![↑g, ↑h] i_1 i
      f (v.get 0) (v.get 1)) =
    f (g i) (h i)

State before:
f : ℕ → ℕ →. ℕ
hf : ArithPart₁ fun v => f (v.get 0) (v.get 1)
n : ℕ
g h : Vector ℕ n → ℕ
hg : Arith₁ g
hh : Arith₁ h
i : Vector ℕ n
⊢ (do
      let v ← mOfFn fun i_1 => ![↑g, ↑h] i_1 i
      f (v.get 0) (v.get 1)) =
    f (g i) (h i)
Tactic:
have : (fun j => (![↑g, h] : Fin 2 → Vector ℕ n →. ℕ) j i) = (fun j => pure (![g i, h i] j)) := by
  funext j; cases j using Fin.cases <;> simp[Fin.eq_zero]
State after:
f : ℕ → ℕ →. ℕ
hf : ArithPart₁ fun v => f (v.get 0) (v.get 1)
n : ℕ
g h : Vector ℕ n → ℕ
hg : Arith₁ g
hh : Arith₁ h
i : Vector ℕ n
this : (fun j => ![↑g, ↑h] j i) = fun j => pure (![g i, h i] j)
⊢ (do
      let v ← mOfFn fun i_1 => ![↑g, ↑h] i_1 i
      f (v.get 0) (v.get 1)) =
    f (g i) (h i)

State before:
f : ℕ → ℕ →. ℕ
hf : ArithPart₁ fun v => f (v.get 0) (v.get 1)
n : ℕ
g h : Vector ℕ n → ℕ
hg : Arith₁ g
hh : Arith₁ h
i : Vector ℕ n
this : (fun j => ![↑g, ↑h] j i) = fun j => pure (![g i, h i] j)
⊢ (do
      let v ← mOfFn fun i_1 => ![↑g, ↑h] i_1 i
      f (v.get 0) (v.get 1)) =
    f (g i) (h i)
Tactic:
simp[Matrix.comp_vecCons']
State after:
f : ℕ → ℕ →. ℕ
hf : ArithPart₁ fun v => f (v.get 0) (v.get 1)
n : ℕ
g h : Vector ℕ n → ℕ
hg : Arith₁ g
hh : Arith₁ h
i : Vector ℕ n
this : (fun j => ![↑g, ↑h] j i) = fun j => pure (![g i, h i] j)
⊢ ((mOfFn fun i_1 => ![↑g, ↑h] i_1 i).bind fun v => f v.head (v.get 1)) = f (g i) (h i)

State before:
f : ℕ → ℕ →. ℕ
hf : ArithPart₁ fun v => f (v.get 0) (v.get 1)
n : ℕ
g h : Vector ℕ n → ℕ
hg : Arith₁ g
hh : Arith₁ h
i : Vector ℕ n
this : (fun j => ![↑g, ↑h] j i) = fun j => pure (![g i, h i] j)
⊢ ((mOfFn fun i_1 => ![↑g, ↑h] i_1 i).bind fun v => f v.head (v.get 1)) = f (g i) (h i)
Tactic:
simp[this]
State after:
no goals

State before:
f : ℕ → ℕ →. ℕ
hf : ArithPart₁ fun v => f (v.get 0) (v.get 1)
n : ℕ
g h : Vector ℕ n → ℕ
hg : Arith₁ g
hh : Arith₁ h
i : Vector ℕ n
⊢ (fun j => ![↑g, ↑h] j i) = fun j => pure (![g i, h i] j)
Tactic:
funext j
State after:
case h
f : ℕ → ℕ →. ℕ
hf : ArithPart₁ fun v => f (v.get 0) (v.get 1)
n : ℕ
g h : Vector ℕ n → ℕ
hg : Arith₁ g
hh : Arith₁ h
i : Vector ℕ n
j : Fin (succ 1)
⊢ ![↑g, ↑h] j i = pure (![g i, h i] j)

State before:
case h
f : ℕ → ℕ →. ℕ
hf : ArithPart₁ fun v => f (v.get 0) (v.get 1)
n : ℕ
g h : Vector ℕ n → ℕ
hg : Arith₁ g
hh : Arith₁ h
i : Vector ℕ n
j : Fin (succ 1)
⊢ ![↑g, ↑h] j i = pure (![g i, h i] j)
Tactic:
cases j using Fin.cases <;> simp[Fin.eq_zero]
State after:
no goals