[GOAL]
α : Type u_3
n : ℕ
β : Type u_2
σ₁ : Type
γ : Type u_1
σ₂ : Type
xs : Vector α n
f₁ : β → σ₁ → σ₁ × γ
f₂ : α → σ₂ → σ₂ × β
s₂ : σ₂
s₁ : σ₁
⊢ mapAccumr f₁ (mapAccumr f₂ xs s₂).snd s₁ =
    let m :=
      mapAccumr
        (fun x s =>
          let r₂ := f₂ x s.snd;
          let r₁ := f₁ r₂.snd s.fst;
          ((r₁.fst, r₂.fst), r₁.snd))
        xs (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
induction xs using Vector.revInductionOn generalizing s₁ s₂
[GOAL]
case nil
α : Type u_3
n : ℕ
β : Type u_2
σ₁ : Type
γ : Type u_1
σ₂ : Type
xs : Vector α n
f₁ : β → σ₁ → σ₁ × γ
f₂ : α → σ₂ → σ₂ × β
s₂ : σ₂
s₁ : σ₁
⊢ mapAccumr f₁ (mapAccumr f₂ nil s₂).snd s₁ =
    let m :=
      mapAccumr
        (fun x s =>
          let r₂ := f₂ x s.snd;
          let r₁ := f₁ r₂.snd s.fst;
          ((r₁.fst, r₂.fst), r₁.snd))
        nil (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
simp_all
[GOAL]
case snoc
α : Type u_3
n : ℕ
β : Type u_2
σ₁ : Type
γ : Type u_1
σ₂ : Type
xs : Vector α n
f₁ : β → σ₁ → σ₁ × γ
f₂ : α → σ₂ → σ₂ × β
n✝ : ℕ
xs✝ : Vector α n✝
x✝ : α
a✝ :
  ∀ {s₂ : σ₂} {s₁ : σ₁},
    mapAccumr f₁ (mapAccumr f₂ xs✝ s₂).snd s₁ =
      let m :=
        mapAccumr
          (fun x s =>
            let r₂ := f₂ x s.snd;
            let r₁ := f₁ r₂.snd s.fst;
            ((r₁.fst, r₂.fst), r₁.snd))
          xs✝ (s₁, s₂);
      (m.fst.fst, m.snd)
s₂ : σ₂
s₁ : σ₁
⊢ mapAccumr f₁ (mapAccumr f₂ (snoc xs✝ x✝) s₂).snd s₁ =
    let m :=
      mapAccumr
        (fun x s =>
          let r₂ := f₂ x s.snd;
          let r₁ := f₁ r₂.snd s.fst;
          ((r₁.fst, r₂.fst), r₁.snd))
        (snoc xs✝ x✝) (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
simp_all
[GOAL]
α : Type u_3
n : ℕ
β : Type u_2
σ₁ : Type
γ : Type u_1
σ₂ : Type ?u.3222
xs : Vector α n
f₁ : β → σ₁ → σ₁ × γ
f₂✝ : α → σ₂ → σ₂ × β
s : σ₁
f₂ : α → β
⊢ mapAccumr f₁ (map f₂ xs) s = mapAccumr (fun x s => f₁ (f₂ x) s) xs s
[PROOFSTEP]
induction xs using Vector.revInductionOn generalizing s
[GOAL]
case nil
α : Type u_3
n : ℕ
β : Type u_2
σ₁ : Type
γ : Type u_1
σ₂ : Type ?u.3222
xs : Vector α n
f₁ : β → σ₁ → σ₁ × γ
f₂✝ : α → σ₂ → σ₂ × β
f₂ : α → β
s : σ₁
⊢ mapAccumr f₁ (map f₂ nil) s = mapAccumr (fun x s => f₁ (f₂ x) s) nil s
[PROOFSTEP]
simp_all
[GOAL]
case snoc
α : Type u_3
n : ℕ
β : Type u_2
σ₁ : Type
γ : Type u_1
σ₂ : Type ?u.3222
xs : Vector α n
f₁ : β → σ₁ → σ₁ × γ
f₂✝ : α → σ₂ → σ₂ × β
f₂ : α → β
n✝ : ℕ
xs✝ : Vector α n✝
x✝ : α
a✝ : ∀ {s : σ₁}, mapAccumr f₁ (map f₂ xs✝) s = mapAccumr (fun x s => f₁ (f₂ x) s) xs✝ s
s : σ₁
⊢ mapAccumr f₁ (map f₂ (snoc xs✝ x✝)) s = mapAccumr (fun x s => f₁ (f₂ x) s) (snoc xs✝ x✝) s
[PROOFSTEP]
simp_all
[GOAL]
α : Type u_3
n : ℕ
β : Type u_2
σ₁ : Type ?u.4482
γ : Type u_1
σ₂ : Type
xs : Vector α n
f₁✝ : β → σ₁ → σ₁ × γ
f₂ : α → σ₂ → σ₂ × β
s : σ₂
f₁ : β → γ
⊢ map f₁ (mapAccumr f₂ xs s).snd =
    (mapAccumr
        (fun x s =>
          let r := f₂ x s;
          (r.fst, f₁ r.snd))
        xs s).snd
[PROOFSTEP]
induction xs using Vector.revInductionOn generalizing s
[GOAL]
case nil
α : Type u_3
n : ℕ
β : Type u_2
σ₁ : Type ?u.4482
γ : Type u_1
σ₂ : Type
xs : Vector α n
f₁✝ : β → σ₁ → σ₁ × γ
f₂ : α → σ₂ → σ₂ × β
f₁ : β → γ
s : σ₂
⊢ map f₁ (mapAccumr f₂ nil s).snd =
    (mapAccumr
        (fun x s =>
          let r := f₂ x s;
          (r.fst, f₁ r.snd))
        nil s).snd
[PROOFSTEP]
simp_all
[GOAL]
case snoc
α : Type u_3
n : ℕ
β : Type u_2
σ₁ : Type ?u.4482
γ : Type u_1
σ₂ : Type
xs : Vector α n
f₁✝ : β → σ₁ → σ₁ × γ
f₂ : α → σ₂ → σ₂ × β
f₁ : β → γ
n✝ : ℕ
xs✝ : Vector α n✝
x✝ : α
a✝ :
  ∀ {s : σ₂},
    map f₁ (mapAccumr f₂ xs✝ s).snd =
      (mapAccumr
          (fun x s =>
            let r := f₂ x s;
            (r.fst, f₁ r.snd))
          xs✝ s).snd
s : σ₂
⊢ map f₁ (mapAccumr f₂ (snoc xs✝ x✝) s).snd =
    (mapAccumr
        (fun x s =>
          let r := f₂ x s;
          (r.fst, f₁ r.snd))
        (snoc xs✝ x✝) s).snd
[PROOFSTEP]
simp_all
[GOAL]
α : Type u_3
n : ℕ
β : Type u_2
σ₁ : Type ?u.6822
γ : Type u_1
σ₂ : Type ?u.6830
xs : Vector α n
f₁✝ : β → σ₁ → σ₁ × γ
f₂✝ : α → σ₂ → σ₂ × β
f₁ : β → γ
f₂ : α → β
⊢ map f₁ (map f₂ xs) = map (fun x => f₁ (f₂ x)) xs
[PROOFSTEP]
induction xs using Vector.inductionOn
[GOAL]
case h_nil
α : Type u_3
n : ℕ
β : Type u_2
σ₁ : Type ?u.6822
γ : Type u_1
σ₂ : Type ?u.6830
xs : Vector α n
f₁✝ : β → σ₁ → σ₁ × γ
f₂✝ : α → σ₂ → σ₂ × β
f₁ : β → γ
f₂ : α → β
⊢ map f₁ (map f₂ nil) = map (fun x => f₁ (f₂ x)) nil
[PROOFSTEP]
simp_all
[GOAL]
case h_cons
α : Type u_3
n : ℕ
β : Type u_2
σ₁ : Type ?u.6822
γ : Type u_1
σ₂ : Type ?u.6830
xs : Vector α n
f₁✝ : β → σ₁ → σ₁ × γ
f₂✝ : α → σ₂ → σ₂ × β
f₁ : β → γ
f₂ : α → β
n✝ : ℕ
x✝ : α
w✝ : Vector α n✝
a✝ : map f₁ (map f₂ w✝) = map (fun x => f₁ (f₂ x)) w✝
⊢ map f₁ (map f₂ (x✝ ::ᵥ w✝)) = map (fun x => f₁ (f₂ x)) (x✝ ::ᵥ w✝)
[PROOFSTEP]
simp_all
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ ζ σ₂ : Type
s₂ : σ₂
s₁ : σ₁
f₁ : γ → β → σ₁ → σ₁ × ζ
f₂ : α → σ₂ → σ₂ × γ
⊢ mapAccumr₂ f₁ (mapAccumr f₂ xs s₂).snd ys s₁ =
    let m :=
      mapAccumr₂
        (fun x y s =>
          let r₂ := f₂ x s.snd;
          let r₁ := f₁ r₂.snd y s.fst;
          ((r₁.fst, r₂.fst), r₁.snd))
        xs ys (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂
[GOAL]
case nil
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ ζ σ₂ : Type
f₁ : γ → β → σ₁ → σ₁ × ζ
f₂ : α → σ₂ → σ₂ × γ
s₂ : σ₂
s₁ : σ₁
⊢ mapAccumr₂ f₁ (mapAccumr f₂ nil s₂).snd nil s₁ =
    let m :=
      mapAccumr₂
        (fun x y s =>
          let r₂ := f₂ x s.snd;
          let r₁ := f₁ r₂.snd y s.fst;
          ((r₁.fst, r₂.fst), r₁.snd))
        nil nil (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
simp_all
[GOAL]
case snoc
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ ζ σ₂ : Type
f₁ : γ → β → σ₁ → σ₁ × ζ
f₂ : α → σ₂ → σ₂ × γ
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ :
  ∀ {s₂ : σ₂} {s₁ : σ₁},
    mapAccumr₂ f₁ (mapAccumr f₂ xs✝ s₂).snd ys✝ s₁ =
      let m :=
        mapAccumr₂
          (fun x y s =>
            let r₂ := f₂ x s.snd;
            let r₁ := f₁ r₂.snd y s.fst;
            ((r₁.fst, r₂.fst), r₁.snd))
          xs✝ ys✝ (s₁, s₂);
      (m.fst.fst, m.snd)
s₂ : σ₂
s₁ : σ₁
⊢ mapAccumr₂ f₁ (mapAccumr f₂ (snoc xs✝ x✝) s₂).snd (snoc ys✝ y✝) s₁ =
    let m :=
      mapAccumr₂
        (fun x y s =>
          let r₂ := f₂ x s.snd;
          let r₁ := f₁ r₂.snd y s.fst;
          ((r₁.fst, r₂.fst), r₁.snd))
        (snoc xs✝ x✝) (snoc ys✝ y✝) (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
simp_all
[GOAL]
α : Type u_4
n : ℕ
β : Type u_3
xs : Vector α n
ys : Vector β n
γ : Type u_1
ζ : Type u_2
f₁ : γ → β → ζ
f₂ : α → γ
⊢ map₂ f₁ (map f₂ xs) ys = map₂ (fun x y => f₁ (f₂ x) y) xs ys
[PROOFSTEP]
induction xs, ys using Vector.revInductionOn₂
[GOAL]
case nil
α : Type u_4
n : ℕ
β : Type u_3
xs : Vector α n
ys : Vector β n
γ : Type u_1
ζ : Type u_2
f₁ : γ → β → ζ
f₂ : α → γ
⊢ map₂ f₁ (map f₂ nil) nil = map₂ (fun x y => f₁ (f₂ x) y) nil nil
[PROOFSTEP]
simp_all
[GOAL]
case snoc
α : Type u_4
n : ℕ
β : Type u_3
xs : Vector α n
ys : Vector β n
γ : Type u_1
ζ : Type u_2
f₁ : γ → β → ζ
f₂ : α → γ
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ : map₂ f₁ (map f₂ xs✝) ys✝ = map₂ (fun x y => f₁ (f₂ x) y) xs✝ ys✝
⊢ map₂ f₁ (map f₂ (snoc xs✝ x✝)) (snoc ys✝ y✝) = map₂ (fun x y => f₁ (f₂ x) y) (snoc xs✝ x✝) (snoc ys✝ y✝)
[PROOFSTEP]
simp_all
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ ζ σ₂ : Type
s₂ : σ₂
s₁ : σ₁
f₁ : α → γ → σ₁ → σ₁ × ζ
f₂ : β → σ₂ → σ₂ × γ
⊢ mapAccumr₂ f₁ xs (mapAccumr f₂ ys s₂).snd s₁ =
    let m :=
      mapAccumr₂
        (fun x y s =>
          let r₂ := f₂ y s.snd;
          let r₁ := f₁ x r₂.snd s.fst;
          ((r₁.fst, r₂.fst), r₁.snd))
        xs ys (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂
[GOAL]
case nil
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ ζ σ₂ : Type
f₁ : α → γ → σ₁ → σ₁ × ζ
f₂ : β → σ₂ → σ₂ × γ
s₂ : σ₂
s₁ : σ₁
⊢ mapAccumr₂ f₁ nil (mapAccumr f₂ nil s₂).snd s₁ =
    let m :=
      mapAccumr₂
        (fun x y s =>
          let r₂ := f₂ y s.snd;
          let r₁ := f₁ x r₂.snd s.fst;
          ((r₁.fst, r₂.fst), r₁.snd))
        nil nil (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
simp_all
[GOAL]
case snoc
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ ζ σ₂ : Type
f₁ : α → γ → σ₁ → σ₁ × ζ
f₂ : β → σ₂ → σ₂ × γ
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ :
  ∀ {s₂ : σ₂} {s₁ : σ₁},
    mapAccumr₂ f₁ xs✝ (mapAccumr f₂ ys✝ s₂).snd s₁ =
      let m :=
        mapAccumr₂
          (fun x y s =>
            let r₂ := f₂ y s.snd;
            let r₁ := f₁ x r₂.snd s.fst;
            ((r₁.fst, r₂.fst), r₁.snd))
          xs✝ ys✝ (s₁, s₂);
      (m.fst.fst, m.snd)
s₂ : σ₂
s₁ : σ₁
⊢ mapAccumr₂ f₁ (snoc xs✝ x✝) (mapAccumr f₂ (snoc ys✝ y✝) s₂).snd s₁ =
    let m :=
      mapAccumr₂
        (fun x y s =>
          let r₂ := f₂ y s.snd;
          let r₁ := f₁ x r₂.snd s.fst;
          ((r₁.fst, r₂.fst), r₁.snd))
        (snoc xs✝ x✝) (snoc ys✝ y✝) (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
simp_all
[GOAL]
α : Type u_3
n : ℕ
β : Type u_4
xs : Vector α n
ys : Vector β n
γ : Type u_1
ζ : Type u_2
f₁ : α → γ → ζ
f₂ : β → γ
⊢ map₂ f₁ xs (map f₂ ys) = map₂ (fun x y => f₁ x (f₂ y)) xs ys
[PROOFSTEP]
induction xs, ys using Vector.revInductionOn₂
[GOAL]
case nil
α : Type u_3
n : ℕ
β : Type u_4
xs : Vector α n
ys : Vector β n
γ : Type u_1
ζ : Type u_2
f₁ : α → γ → ζ
f₂ : β → γ
⊢ map₂ f₁ nil (map f₂ nil) = map₂ (fun x y => f₁ x (f₂ y)) nil nil
[PROOFSTEP]
simp_all
[GOAL]
case snoc
α : Type u_3
n : ℕ
β : Type u_4
xs : Vector α n
ys : Vector β n
γ : Type u_1
ζ : Type u_2
f₁ : α → γ → ζ
f₂ : β → γ
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ : map₂ f₁ xs✝ (map f₂ ys✝) = map₂ (fun x y => f₁ x (f₂ y)) xs✝ ys✝
⊢ map₂ f₁ (snoc xs✝ x✝) (map f₂ (snoc ys✝ y✝)) = map₂ (fun x y => f₁ x (f₂ y)) (snoc xs✝ x✝) (snoc ys✝ y✝)
[PROOFSTEP]
simp_all
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ ζ σ₂ : Type
s₂ : σ₂
s₁ : σ₁
f₁ : γ → σ₁ → σ₁ × ζ
f₂ : α → β → σ₂ → σ₂ × γ
⊢ mapAccumr f₁ (mapAccumr₂ f₂ xs ys s₂).snd s₁ =
    let m :=
      mapAccumr₂
        (fun x y s =>
          let r₂ := f₂ x y s.snd;
          let r₁ := f₁ r₂.snd s.fst;
          ((r₁.fst, r₂.fst), r₁.snd))
        xs ys (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂
[GOAL]
case nil
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ ζ σ₂ : Type
f₁ : γ → σ₁ → σ₁ × ζ
f₂ : α → β → σ₂ → σ₂ × γ
s₂ : σ₂
s₁ : σ₁
⊢ mapAccumr f₁ (mapAccumr₂ f₂ nil nil s₂).snd s₁ =
    let m :=
      mapAccumr₂
        (fun x y s =>
          let r₂ := f₂ x y s.snd;
          let r₁ := f₁ r₂.snd s.fst;
          ((r₁.fst, r₂.fst), r₁.snd))
        nil nil (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
simp_all
[GOAL]
case snoc
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ ζ σ₂ : Type
f₁ : γ → σ₁ → σ₁ × ζ
f₂ : α → β → σ₂ → σ₂ × γ
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ :
  ∀ {s₂ : σ₂} {s₁ : σ₁},
    mapAccumr f₁ (mapAccumr₂ f₂ xs✝ ys✝ s₂).snd s₁ =
      let m :=
        mapAccumr₂
          (fun x y s =>
            let r₂ := f₂ x y s.snd;
            let r₁ := f₁ r₂.snd s.fst;
            ((r₁.fst, r₂.fst), r₁.snd))
          xs✝ ys✝ (s₁, s₂);
      (m.fst.fst, m.snd)
s₂ : σ₂
s₁ : σ₁
⊢ mapAccumr f₁ (mapAccumr₂ f₂ (snoc xs✝ x✝) (snoc ys✝ y✝) s₂).snd s₁ =
    let m :=
      mapAccumr₂
        (fun x y s =>
          let r₂ := f₂ x y s.snd;
          let r₁ := f₁ r₂.snd s.fst;
          ((r₁.fst, r₂.fst), r₁.snd))
        (snoc xs✝ x✝) (snoc ys✝ y✝) (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
simp_all
[GOAL]
α : Type u_3
n : ℕ
β : Type u_4
xs : Vector α n
ys : Vector β n
γ : Type u_1
ζ : Type u_2
f₁ : γ → ζ
f₂ : α → β → γ
⊢ map f₁ (map₂ f₂ xs ys) = map₂ (fun x y => f₁ (f₂ x y)) xs ys
[PROOFSTEP]
induction xs, ys using Vector.revInductionOn₂
[GOAL]
case nil
α : Type u_3
n : ℕ
β : Type u_4
xs : Vector α n
ys : Vector β n
γ : Type u_1
ζ : Type u_2
f₁ : γ → ζ
f₂ : α → β → γ
⊢ map f₁ (map₂ f₂ nil nil) = map₂ (fun x y => f₁ (f₂ x y)) nil nil
[PROOFSTEP]
simp_all
[GOAL]
case snoc
α : Type u_3
n : ℕ
β : Type u_4
xs : Vector α n
ys : Vector β n
γ : Type u_1
ζ : Type u_2
f₁ : γ → ζ
f₂ : α → β → γ
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ : map f₁ (map₂ f₂ xs✝ ys✝) = map₂ (fun x y => f₁ (f₂ x y)) xs✝ ys✝
⊢ map f₁ (map₂ f₂ (snoc xs✝ x✝) (snoc ys✝ y✝)) = map₂ (fun x y => f₁ (f₂ x y)) (snoc xs✝ x✝) (snoc ys✝ y✝)
[PROOFSTEP]
simp_all
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ φ σ₂ : Type
s₂ : σ₂
s₁ : σ₁
f₁ : γ → α → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
⊢ mapAccumr₂ f₁ (mapAccumr₂ f₂ xs ys s₂).snd xs s₁ =
    let m :=
      mapAccumr₂
        (fun x y x_1 =>
          match x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ r₂.snd x s₁;
            ((r₁.fst, r₂.fst), r₁.snd))
        xs ys (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂
[GOAL]
case nil
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ φ σ₂ : Type
f₁ : γ → α → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
s₂ : σ₂
s₁ : σ₁
⊢ mapAccumr₂ f₁ (mapAccumr₂ f₂ nil nil s₂).snd nil s₁ =
    let m :=
      mapAccumr₂
        (fun x y x_1 =>
          match x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ r₂.snd x s₁;
            ((r₁.fst, r₂.fst), r₁.snd))
        nil nil (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
simp_all
[GOAL]
case snoc
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ φ σ₂ : Type
f₁ : γ → α → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ :
  ∀ {s₂ : σ₂} {s₁ : σ₁},
    mapAccumr₂ f₁ (mapAccumr₂ f₂ xs✝ ys✝ s₂).snd xs✝ s₁ =
      let m :=
        mapAccumr₂
          (fun x y x_1 =>
            match x_1 with
            | (s₁, s₂) =>
              let r₂ := f₂ x y s₂;
              let r₁ := f₁ r₂.snd x s₁;
              ((r₁.fst, r₂.fst), r₁.snd))
          xs✝ ys✝ (s₁, s₂);
      (m.fst.fst, m.snd)
s₂ : σ₂
s₁ : σ₁
⊢ mapAccumr₂ f₁ (mapAccumr₂ f₂ (snoc xs✝ x✝) (snoc ys✝ y✝) s₂).snd (snoc xs✝ x✝) s₁ =
    let m :=
      mapAccumr₂
        (fun x y x_1 =>
          match x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ r₂.snd x s₁;
            ((r₁.fst, r₂.fst), r₁.snd))
        (snoc xs✝ x✝) (snoc ys✝ y✝) (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
simp_all
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ φ σ₂ : Type
s₂ : σ₂
s₁ : σ₁
f₁ : γ → β → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
⊢ mapAccumr₂ f₁ (mapAccumr₂ f₂ xs ys s₂).snd ys s₁ =
    let m :=
      mapAccumr₂
        (fun x y x_1 =>
          match x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ r₂.snd y s₁;
            ((r₁.fst, r₂.fst), r₁.snd))
        xs ys (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂
[GOAL]
case nil
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ φ σ₂ : Type
f₁ : γ → β → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
s₂ : σ₂
s₁ : σ₁
⊢ mapAccumr₂ f₁ (mapAccumr₂ f₂ nil nil s₂).snd nil s₁ =
    let m :=
      mapAccumr₂
        (fun x y x_1 =>
          match x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ r₂.snd y s₁;
            ((r₁.fst, r₂.fst), r₁.snd))
        nil nil (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
simp_all
[GOAL]
case snoc
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ φ σ₂ : Type
f₁ : γ → β → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ :
  ∀ {s₂ : σ₂} {s₁ : σ₁},
    mapAccumr₂ f₁ (mapAccumr₂ f₂ xs✝ ys✝ s₂).snd ys✝ s₁ =
      let m :=
        mapAccumr₂
          (fun x y x_1 =>
            match x_1 with
            | (s₁, s₂) =>
              let r₂ := f₂ x y s₂;
              let r₁ := f₁ r₂.snd y s₁;
              ((r₁.fst, r₂.fst), r₁.snd))
          xs✝ ys✝ (s₁, s₂);
      (m.fst.fst, m.snd)
s₂ : σ₂
s₁ : σ₁
⊢ mapAccumr₂ f₁ (mapAccumr₂ f₂ (snoc xs✝ x✝) (snoc ys✝ y✝) s₂).snd (snoc ys✝ y✝) s₁ =
    let m :=
      mapAccumr₂
        (fun x y x_1 =>
          match x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ r₂.snd y s₁;
            ((r₁.fst, r₂.fst), r₁.snd))
        (snoc xs✝ x✝) (snoc ys✝ y✝) (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
simp_all
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ φ σ₂ : Type
s₂ : σ₂
s₁ : σ₁
f₁ : α → γ → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
⊢ mapAccumr₂ f₁ xs (mapAccumr₂ f₂ xs ys s₂).snd s₁ =
    let m :=
      mapAccumr₂
        (fun x y x_1 =>
          match x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ x r₂.snd s₁;
            ((r₁.fst, r₂.fst), r₁.snd))
        xs ys (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂
[GOAL]
case nil
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ φ σ₂ : Type
f₁ : α → γ → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
s₂ : σ₂
s₁ : σ₁
⊢ mapAccumr₂ f₁ nil (mapAccumr₂ f₂ nil nil s₂).snd s₁ =
    let m :=
      mapAccumr₂
        (fun x y x_1 =>
          match x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ x r₂.snd s₁;
            ((r₁.fst, r₂.fst), r₁.snd))
        nil nil (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
simp_all
[GOAL]
case snoc
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ φ σ₂ : Type
f₁ : α → γ → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ :
  ∀ {s₂ : σ₂} {s₁ : σ₁},
    mapAccumr₂ f₁ xs✝ (mapAccumr₂ f₂ xs✝ ys✝ s₂).snd s₁ =
      let m :=
        mapAccumr₂
          (fun x y x_1 =>
            match x_1 with
            | (s₁, s₂) =>
              let r₂ := f₂ x y s₂;
              let r₁ := f₁ x r₂.snd s₁;
              ((r₁.fst, r₂.fst), r₁.snd))
          xs✝ ys✝ (s₁, s₂);
      (m.fst.fst, m.snd)
s₂ : σ₂
s₁ : σ₁
⊢ mapAccumr₂ f₁ (snoc xs✝ x✝) (mapAccumr₂ f₂ (snoc xs✝ x✝) (snoc ys✝ y✝) s₂).snd s₁ =
    let m :=
      mapAccumr₂
        (fun x y x_1 =>
          match x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ x r₂.snd s₁;
            ((r₁.fst, r₂.fst), r₁.snd))
        (snoc xs✝ x✝) (snoc ys✝ y✝) (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
simp_all
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ φ σ₂ : Type
s₂ : σ₂
s₁ : σ₁
f₁ : β → γ → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
⊢ mapAccumr₂ f₁ ys (mapAccumr₂ f₂ xs ys s₂).snd s₁ =
    let m :=
      mapAccumr₂
        (fun x y x_1 =>
          match x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ y r₂.snd s₁;
            ((r₁.fst, r₂.fst), r₁.snd))
        xs ys (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂
[GOAL]
case nil
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ φ σ₂ : Type
f₁ : β → γ → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
s₂ : σ₂
s₁ : σ₁
⊢ mapAccumr₂ f₁ nil (mapAccumr₂ f₂ nil nil s₂).snd s₁ =
    let m :=
      mapAccumr₂
        (fun x y x_1 =>
          match x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ y r₂.snd s₁;
            ((r₁.fst, r₂.fst), r₁.snd))
        nil nil (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
simp_all
[GOAL]
case snoc
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ φ σ₂ : Type
f₁ : β → γ → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ :
  ∀ {s₂ : σ₂} {s₁ : σ₁},
    mapAccumr₂ f₁ ys✝ (mapAccumr₂ f₂ xs✝ ys✝ s₂).snd s₁ =
      let m :=
        mapAccumr₂
          (fun x y x_1 =>
            match x_1 with
            | (s₁, s₂) =>
              let r₂ := f₂ x y s₂;
              let r₁ := f₁ y r₂.snd s₁;
              ((r₁.fst, r₂.fst), r₁.snd))
          xs✝ ys✝ (s₁, s₂);
      (m.fst.fst, m.snd)
s₂ : σ₂
s₁ : σ₁
⊢ mapAccumr₂ f₁ (snoc ys✝ y✝) (mapAccumr₂ f₂ (snoc xs✝ x✝) (snoc ys✝ y✝) s₂).snd s₁ =
    let m :=
      mapAccumr₂
        (fun x y x_1 =>
          match x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ y r₂.snd s₁;
            ((r₁.fst, r₂.fst), r₁.snd))
        (snoc xs✝ x✝) (snoc ys✝ y✝) (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
simp_all
[GOAL]
α : Type u_2
n : ℕ
xs : Vector α n
σ₁ : Type
β : Type u_1
σ₂ : Type
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
s₁ : σ₁
s₂ : σ₂
R : σ₁ → σ₂ → Prop
h₀ : R s₁ s₂
hR : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).fst (f₂ a q).fst ∧ (f₁ a s).snd = (f₂ a q).snd
⊢ R (mapAccumr f₁ xs s₁).fst (mapAccumr f₂ xs s₂).fst ∧ (mapAccumr f₁ xs s₁).snd = (mapAccumr f₂ xs s₂).snd
[PROOFSTEP]
induction xs using Vector.revInductionOn generalizing s₁ s₂
[GOAL]
case nil
α : Type u_2
n : ℕ
xs : Vector α n
σ₁ : Type
β : Type u_1
σ₂ : Type
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).fst (f₂ a q).fst ∧ (f₁ a s).snd = (f₂ a q).snd
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr f₁ nil s₁).fst (mapAccumr f₂ nil s₂).fst ∧ (mapAccumr f₁ nil s₁).snd = (mapAccumr f₂ nil s₂).snd
case snoc
α : Type u_2
n : ℕ
xs : Vector α n
σ₁ : Type
β : Type u_1
σ₂ : Type
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).fst (f₂ a q).fst ∧ (f₁ a s).snd = (f₂ a q).snd
n✝ : ℕ
xs✝ : Vector α n✝
x✝ : α
a✝ :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ →
      R (mapAccumr f₁ xs✝ s₁).fst (mapAccumr f₂ xs✝ s₂).fst ∧ (mapAccumr f₁ xs✝ s₁).snd = (mapAccumr f₂ xs✝ s₂).snd
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr f₁ (snoc xs✝ x✝) s₁).fst (mapAccumr f₂ (snoc xs✝ x✝) s₂).fst ∧
    (mapAccumr f₁ (snoc xs✝ x✝) s₁).snd = (mapAccumr f₂ (snoc xs✝ x✝) s₂).snd
[PROOFSTEP]
next => exact ⟨h₀, rfl⟩
[GOAL]
α : Type u_2
n : ℕ
xs : Vector α n
σ₁ : Type
β : Type u_1
σ₂ : Type
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).fst (f₂ a q).fst ∧ (f₁ a s).snd = (f₂ a q).snd
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr f₁ nil s₁).fst (mapAccumr f₂ nil s₂).fst ∧ (mapAccumr f₁ nil s₁).snd = (mapAccumr f₂ nil s₂).snd
[PROOFSTEP]
exact ⟨h₀, rfl⟩
[GOAL]
case snoc
α : Type u_2
n : ℕ
xs : Vector α n
σ₁ : Type
β : Type u_1
σ₂ : Type
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).fst (f₂ a q).fst ∧ (f₁ a s).snd = (f₂ a q).snd
n✝ : ℕ
xs✝ : Vector α n✝
x✝ : α
a✝ :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ →
      R (mapAccumr f₁ xs✝ s₁).fst (mapAccumr f₂ xs✝ s₂).fst ∧ (mapAccumr f₁ xs✝ s₁).snd = (mapAccumr f₂ xs✝ s₂).snd
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr f₁ (snoc xs✝ x✝) s₁).fst (mapAccumr f₂ (snoc xs✝ x✝) s₂).fst ∧
    (mapAccumr f₁ (snoc xs✝ x✝) s₁).snd = (mapAccumr f₂ (snoc xs✝ x✝) s₂).snd
[PROOFSTEP]
next xs x ih =>
  rcases(hR x h₀) with ⟨hR, _⟩
  simp only [mapAccumr_snoc, ih hR, true_and]
  congr 1
[GOAL]
α : Type u_2
n : ℕ
xs✝ : Vector α n
σ₁ : Type
β : Type u_1
σ₂ : Type
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).fst (f₂ a q).fst ∧ (f₁ a s).snd = (f₂ a q).snd
n✝ : ℕ
xs : Vector α n✝
x : α
ih :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ → R (mapAccumr f₁ xs s₁).fst (mapAccumr f₂ xs s₂).fst ∧ (mapAccumr f₁ xs s₁).snd = (mapAccumr f₂ xs s₂).snd
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr f₁ (snoc xs x) s₁).fst (mapAccumr f₂ (snoc xs x) s₂).fst ∧
    (mapAccumr f₁ (snoc xs x) s₁).snd = (mapAccumr f₂ (snoc xs x) s₂).snd
[PROOFSTEP]
rcases(hR x h₀) with ⟨hR, _⟩
[GOAL]
case intro
α : Type u_2
n : ℕ
xs✝ : Vector α n
σ₁ : Type
β : Type u_1
σ₂ : Type
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
R : σ₁ → σ₂ → Prop
hR✝ : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).fst (f₂ a q).fst ∧ (f₁ a s).snd = (f₂ a q).snd
n✝ : ℕ
xs : Vector α n✝
x : α
ih :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ → R (mapAccumr f₁ xs s₁).fst (mapAccumr f₂ xs s₂).fst ∧ (mapAccumr f₁ xs s₁).snd = (mapAccumr f₂ xs s₂).snd
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
hR : R (f₁ x s₁).fst (f₂ x s₂).fst
right✝ : (f₁ x s₁).snd = (f₂ x s₂).snd
⊢ R (mapAccumr f₁ (snoc xs x) s₁).fst (mapAccumr f₂ (snoc xs x) s₂).fst ∧
    (mapAccumr f₁ (snoc xs x) s₁).snd = (mapAccumr f₂ (snoc xs x) s₂).snd
[PROOFSTEP]
simp only [mapAccumr_snoc, ih hR, true_and]
[GOAL]
case intro
α : Type u_2
n : ℕ
xs✝ : Vector α n
σ₁ : Type
β : Type u_1
σ₂ : Type
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
R : σ₁ → σ₂ → Prop
hR✝ : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).fst (f₂ a q).fst ∧ (f₁ a s).snd = (f₂ a q).snd
n✝ : ℕ
xs : Vector α n✝
x : α
ih :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ → R (mapAccumr f₁ xs s₁).fst (mapAccumr f₂ xs s₂).fst ∧ (mapAccumr f₁ xs s₁).snd = (mapAccumr f₂ xs s₂).snd
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
hR : R (f₁ x s₁).fst (f₂ x s₂).fst
right✝ : (f₁ x s₁).snd = (f₂ x s₂).snd
⊢ snoc (mapAccumr f₂ xs (f₂ x s₂).fst).snd (f₁ x s₁).snd = snoc (mapAccumr f₂ xs (f₂ x s₂).fst).snd (f₂ x s₂).snd
[PROOFSTEP]
congr 1
[GOAL]
α : Type u_2
n : ℕ
xs : Vector α n
σ₁ : Type
β : Type u_1
σ₂ : Type
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
s₁ : σ₁
s₂ : σ₂
h : ∃ R, R s₁ s₂ ∧ ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).fst (f₂ a q).fst ∧ (f₁ a s).snd = (f₂ a q).snd
⊢ (mapAccumr f₁ xs s₁).snd = (mapAccumr f₂ xs s₂).snd
[PROOFSTEP]
rcases h with ⟨R, h₀, hR⟩
[GOAL]
case intro.intro
α : Type u_2
n : ℕ
xs : Vector α n
σ₁ : Type
β : Type u_1
σ₂ : Type
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
s₁ : σ₁
s₂ : σ₂
R : σ₁ → σ₂ → Prop
h₀ : R s₁ s₂
hR : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).fst (f₂ a q).fst ∧ (f₁ a s).snd = (f₂ a q).snd
⊢ (mapAccumr f₁ xs s₁).snd = (mapAccumr f₂ xs s₂).snd
[PROOFSTEP]
exact (mapAccumr_bisim R h₀ hR).2
[GOAL]
α : Type
n : ℕ
xs : Vector α n
β σ₁ γ σ₂ : Type
ys : Vector β n
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
s₁ : σ₁
s₂ : σ₂
R : σ₁ → σ₂ → Prop
h₀ : R s₁ s₂
hR : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).fst (f₂ a b q).fst ∧ (f₁ a b s).snd = (f₂ a b q).snd
⊢ R (mapAccumr₂ f₁ xs ys s₁).fst (mapAccumr₂ f₂ xs ys s₂).fst ∧
    (mapAccumr₂ f₁ xs ys s₁).snd = (mapAccumr₂ f₂ xs ys s₂).snd
[PROOFSTEP]
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂
[GOAL]
case nil
α : Type
n : ℕ
xs : Vector α n
β σ₁ γ σ₂ : Type
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).fst (f₂ a b q).fst ∧ (f₁ a b s).snd = (f₂ a b q).snd
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr₂ f₁ nil nil s₁).fst (mapAccumr₂ f₂ nil nil s₂).fst ∧
    (mapAccumr₂ f₁ nil nil s₁).snd = (mapAccumr₂ f₂ nil nil s₂).snd
case snoc
α : Type
n : ℕ
xs : Vector α n
β σ₁ γ σ₂ : Type
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).fst (f₂ a b q).fst ∧ (f₁ a b s).snd = (f₂ a b q).snd
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ →
      R (mapAccumr₂ f₁ xs✝ ys✝ s₁).fst (mapAccumr₂ f₂ xs✝ ys✝ s₂).fst ∧
        (mapAccumr₂ f₁ xs✝ ys✝ s₁).snd = (mapAccumr₂ f₂ xs✝ ys✝ s₂).snd
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr₂ f₁ (snoc xs✝ x✝) (snoc ys✝ y✝) s₁).fst (mapAccumr₂ f₂ (snoc xs✝ x✝) (snoc ys✝ y✝) s₂).fst ∧
    (mapAccumr₂ f₁ (snoc xs✝ x✝) (snoc ys✝ y✝) s₁).snd = (mapAccumr₂ f₂ (snoc xs✝ x✝) (snoc ys✝ y✝) s₂).snd
[PROOFSTEP]
next => exact ⟨h₀, rfl⟩
[GOAL]
α : Type
n : ℕ
xs : Vector α n
β σ₁ γ σ₂ : Type
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).fst (f₂ a b q).fst ∧ (f₁ a b s).snd = (f₂ a b q).snd
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr₂ f₁ nil nil s₁).fst (mapAccumr₂ f₂ nil nil s₂).fst ∧
    (mapAccumr₂ f₁ nil nil s₁).snd = (mapAccumr₂ f₂ nil nil s₂).snd
[PROOFSTEP]
exact ⟨h₀, rfl⟩
[GOAL]
case snoc
α : Type
n : ℕ
xs : Vector α n
β σ₁ γ σ₂ : Type
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).fst (f₂ a b q).fst ∧ (f₁ a b s).snd = (f₂ a b q).snd
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ →
      R (mapAccumr₂ f₁ xs✝ ys✝ s₁).fst (mapAccumr₂ f₂ xs✝ ys✝ s₂).fst ∧
        (mapAccumr₂ f₁ xs✝ ys✝ s₁).snd = (mapAccumr₂ f₂ xs✝ ys✝ s₂).snd
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr₂ f₁ (snoc xs✝ x✝) (snoc ys✝ y✝) s₁).fst (mapAccumr₂ f₂ (snoc xs✝ x✝) (snoc ys✝ y✝) s₂).fst ∧
    (mapAccumr₂ f₁ (snoc xs✝ x✝) (snoc ys✝ y✝) s₁).snd = (mapAccumr₂ f₂ (snoc xs✝ x✝) (snoc ys✝ y✝) s₂).snd
[PROOFSTEP]
next xs ys x y ih =>
  rcases(hR x y h₀) with ⟨hR, _⟩
  simp only [mapAccumr₂_snoc, ih hR, true_and]
  congr 1
[GOAL]
α : Type
n : ℕ
xs✝ : Vector α n
β σ₁ γ σ₂ : Type
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).fst (f₂ a b q).fst ∧ (f₁ a b s).snd = (f₂ a b q).snd
n✝ : ℕ
xs : Vector α n✝
ys : Vector β n✝
x : α
y : β
ih :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ →
      R (mapAccumr₂ f₁ xs ys s₁).fst (mapAccumr₂ f₂ xs ys s₂).fst ∧
        (mapAccumr₂ f₁ xs ys s₁).snd = (mapAccumr₂ f₂ xs ys s₂).snd
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr₂ f₁ (snoc xs x) (snoc ys y) s₁).fst (mapAccumr₂ f₂ (snoc xs x) (snoc ys y) s₂).fst ∧
    (mapAccumr₂ f₁ (snoc xs x) (snoc ys y) s₁).snd = (mapAccumr₂ f₂ (snoc xs x) (snoc ys y) s₂).snd
[PROOFSTEP]
rcases(hR x y h₀) with ⟨hR, _⟩
[GOAL]
case intro
α : Type
n : ℕ
xs✝ : Vector α n
β σ₁ γ σ₂ : Type
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
R : σ₁ → σ₂ → Prop
hR✝ : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).fst (f₂ a b q).fst ∧ (f₁ a b s).snd = (f₂ a b q).snd
n✝ : ℕ
xs : Vector α n✝
ys : Vector β n✝
x : α
y : β
ih :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ →
      R (mapAccumr₂ f₁ xs ys s₁).fst (mapAccumr₂ f₂ xs ys s₂).fst ∧
        (mapAccumr₂ f₁ xs ys s₁).snd = (mapAccumr₂ f₂ xs ys s₂).snd
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
hR : R (f₁ x y s₁).fst (f₂ x y s₂).fst
right✝ : (f₁ x y s₁).snd = (f₂ x y s₂).snd
⊢ R (mapAccumr₂ f₁ (snoc xs x) (snoc ys y) s₁).fst (mapAccumr₂ f₂ (snoc xs x) (snoc ys y) s₂).fst ∧
    (mapAccumr₂ f₁ (snoc xs x) (snoc ys y) s₁).snd = (mapAccumr₂ f₂ (snoc xs x) (snoc ys y) s₂).snd
[PROOFSTEP]
simp only [mapAccumr₂_snoc, ih hR, true_and]
[GOAL]
case intro
α : Type
n : ℕ
xs✝ : Vector α n
β σ₁ γ σ₂ : Type
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
R : σ₁ → σ₂ → Prop
hR✝ : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).fst (f₂ a b q).fst ∧ (f₁ a b s).snd = (f₂ a b q).snd
n✝ : ℕ
xs : Vector α n✝
ys : Vector β n✝
x : α
y : β
ih :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ →
      R (mapAccumr₂ f₁ xs ys s₁).fst (mapAccumr₂ f₂ xs ys s₂).fst ∧
        (mapAccumr₂ f₁ xs ys s₁).snd = (mapAccumr₂ f₂ xs ys s₂).snd
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
hR : R (f₁ x y s₁).fst (f₂ x y s₂).fst
right✝ : (f₁ x y s₁).snd = (f₂ x y s₂).snd
⊢ snoc (mapAccumr₂ f₂ xs ys (f₂ x y s₂).fst).snd (f₁ x y s₁).snd =
    snoc (mapAccumr₂ f₂ xs ys (f₂ x y s₂).fst).snd (f₂ x y s₂).snd
[PROOFSTEP]
congr 1
[GOAL]
α : Type
n : ℕ
xs : Vector α n
β σ₁ γ σ₂ : Type
ys : Vector β n
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
s₁ : σ₁
s₂ : σ₂
h :
  ∃ R,
    R s₁ s₂ ∧
      ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).fst (f₂ a b q).fst ∧ (f₁ a b s).snd = (f₂ a b q).snd
⊢ (mapAccumr₂ f₁ xs ys s₁).snd = (mapAccumr₂ f₂ xs ys s₂).snd
[PROOFSTEP]
rcases h with ⟨R, h₀, hR⟩
[GOAL]
case intro.intro
α : Type
n : ℕ
xs : Vector α n
β σ₁ γ σ₂ : Type
ys : Vector β n
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
s₁ : σ₁
s₂ : σ₂
R : σ₁ → σ₂ → Prop
h₀ : R s₁ s₂
hR : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).fst (f₂ a b q).fst ∧ (f₁ a b s).snd = (f₂ a b q).snd
⊢ (mapAccumr₂ f₁ xs ys s₁).snd = (mapAccumr₂ f₂ xs ys s₂).snd
[PROOFSTEP]
exact (mapAccumr₂_bisim R h₀ hR).2
[GOAL]
α : Type u_2
n : ℕ
β : Type ?u.34261
xs : Vector α n
ys : Vector β n
α✝ : Type u_1
f : α → α✝
⊢ map f xs = (mapAccumr (fun x x_1 => ((), f x)) xs ()).snd
[PROOFSTEP]
clear ys
[GOAL]
α : Type u_2
n : ℕ
β : Type ?u.34261
xs : Vector α n
α✝ : Type u_1
f : α → α✝
⊢ map f xs = (mapAccumr (fun x x_1 => ((), f x)) xs ()).snd
[PROOFSTEP]
induction xs using Vector.revInductionOn
[GOAL]
case nil
α : Type u_2
n : ℕ
β : Type ?u.34261
xs : Vector α n
α✝ : Type u_1
f : α → α✝
⊢ map f nil = (mapAccumr (fun x x_1 => ((), f x)) nil ()).snd
[PROOFSTEP]
simp_all
[GOAL]
case snoc
α : Type u_2
n : ℕ
β : Type ?u.34261
xs : Vector α n
α✝ : Type u_1
f : α → α✝
n✝ : ℕ
xs✝ : Vector α n✝
x✝ : α
a✝ : map f xs✝ = (mapAccumr (fun x x_1 => ((), f x)) xs✝ ()).snd
⊢ map f (snoc xs✝ x✝) = (mapAccumr (fun x x_1 => ((), f x)) (snoc xs✝ x✝) ()).snd
[PROOFSTEP]
simp_all
[GOAL]
α : Type u_2
n : ℕ
β : Type u_1
xs : Vector α n
ys : Vector β n
σ : Type
f : α → σ → σ × β
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (s : σ), s ∈ S → (f a s).fst ∈ S
out : ∀ (a : α) (s s' : σ), s ∈ S → s' ∈ S → (f a s).snd = (f a s').snd
⊢ (mapAccumr f xs s₀).snd = map (fun x => (f x s₀).snd) xs
[PROOFSTEP]
rw [Vector.map_eq_mapAccumr]
[GOAL]
α : Type u_2
n : ℕ
β : Type u_1
xs : Vector α n
ys : Vector β n
σ : Type
f : α → σ → σ × β
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (s : σ), s ∈ S → (f a s).fst ∈ S
out : ∀ (a : α) (s s' : σ), s ∈ S → s' ∈ S → (f a s).snd = (f a s').snd
⊢ (mapAccumr f xs s₀).snd = (mapAccumr (fun x x_1 => ((), (f x s₀).snd)) xs ()).snd
[PROOFSTEP]
apply mapAccumr_bisim_tail
[GOAL]
case h
α : Type u_2
n : ℕ
β : Type u_1
xs : Vector α n
ys : Vector β n
σ : Type
f : α → σ → σ × β
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (s : σ), s ∈ S → (f a s).fst ∈ S
out : ∀ (a : α) (s s' : σ), s ∈ S → s' ∈ S → (f a s).snd = (f a s').snd
⊢ ∃ R,
    R s₀ () ∧
      ∀ {s : σ} {q : Unit} (a : α), R s q → R (f a s).fst ((), (f a s₀).snd).fst ∧ (f a s).snd = ((), (f a s₀).snd).snd
[PROOFSTEP]
use fun s _ => s ∈ S, h₀
[GOAL]
case right
α : Type u_2
n : ℕ
β : Type u_1
xs : Vector α n
ys : Vector β n
σ : Type
f : α → σ → σ × β
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (s : σ), s ∈ S → (f a s).fst ∈ S
out : ∀ (a : α) (s s' : σ), s ∈ S → s' ∈ S → (f a s).snd = (f a s').snd
⊢ ∀ {s : σ} {q : Unit} (a : α), s ∈ S → (f a s).fst ∈ S ∧ (f a s).snd = ((), (f a s₀).snd).snd
[PROOFSTEP]
exact @fun s _q a h => ⟨closure a s h, out a s s₀ h h₀⟩
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
α✝ : Type
f : α → β → α✝
⊢ map₂ f xs ys = (mapAccumr₂ (fun x y x_1 => ((), f x y)) xs ys ()).snd
[PROOFSTEP]
induction xs, ys using Vector.revInductionOn₂
[GOAL]
case nil
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
α✝ : Type
f : α → β → α✝
⊢ map₂ f nil nil = (mapAccumr₂ (fun x y x_1 => ((), f x y)) nil nil ()).snd
[PROOFSTEP]
simp_all
[GOAL]
case snoc
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
α✝ : Type
f : α → β → α✝
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ : map₂ f xs✝ ys✝ = (mapAccumr₂ (fun x y x_1 => ((), f x y)) xs✝ ys✝ ()).snd
⊢ map₂ f (snoc xs✝ x✝) (snoc ys✝ y✝) = (mapAccumr₂ (fun x y x_1 => ((), f x y)) (snoc xs✝ x✝) (snoc ys✝ y✝) ()).snd
[PROOFSTEP]
simp_all
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
f : α → β → σ → σ × γ
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (b : β) (s : σ), s ∈ S → (f a b s).fst ∈ S
out : ∀ (a : α) (b : β) (s s' : σ), s ∈ S → s' ∈ S → (f a b s).snd = (f a b s').snd
⊢ (mapAccumr₂ f xs ys s₀).snd = map₂ (fun x x_1 => (f x x_1 s₀).snd) xs ys
[PROOFSTEP]
rw [Vector.map₂_eq_mapAccumr₂]
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
f : α → β → σ → σ × γ
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (b : β) (s : σ), s ∈ S → (f a b s).fst ∈ S
out : ∀ (a : α) (b : β) (s s' : σ), s ∈ S → s' ∈ S → (f a b s).snd = (f a b s').snd
⊢ (mapAccumr₂ f xs ys s₀).snd = (mapAccumr₂ (fun x y x_1 => ((), (f x y s₀).snd)) xs ys ()).snd
[PROOFSTEP]
apply mapAccumr₂_bisim_tail
[GOAL]
case h
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
f : α → β → σ → σ × γ
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (b : β) (s : σ), s ∈ S → (f a b s).fst ∈ S
out : ∀ (a : α) (b : β) (s s' : σ), s ∈ S → s' ∈ S → (f a b s).snd = (f a b s').snd
⊢ ∃ R,
    R s₀ () ∧
      ∀ {s : σ} {q : Unit} (a : α) (b : β),
        R s q → R (f a b s).fst ((), (f a b s₀).snd).fst ∧ (f a b s).snd = ((), (f a b s₀).snd).snd
[PROOFSTEP]
use fun s _ => s ∈ S, h₀
[GOAL]
case right
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
f : α → β → σ → σ × γ
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (b : β) (s : σ), s ∈ S → (f a b s).fst ∈ S
out : ∀ (a : α) (b : β) (s s' : σ), s ∈ S → s' ∈ S → (f a b s).snd = (f a b s').snd
⊢ ∀ {s : σ} {q : Unit} (a : α) (b : β), s ∈ S → (f a b s).fst ∈ S ∧ (f a b s).snd = ((), (f a b s₀).snd).snd
[PROOFSTEP]
exact @fun s _q a b h => ⟨closure a b s h, out a b s s₀ h h₀⟩
[GOAL]
α : Type u_2
n : ℕ
β : Type u_1
xs : Vector α n
ys : Vector β n
σ : Type
f : α → σ → σ × β
s : σ
h : ∀ (a : α), (f a s).fst = s
⊢ mapAccumr f xs s = (s, map (fun x => (f x s).snd) xs)
[PROOFSTEP]
clear ys
[GOAL]
α : Type u_2
n : ℕ
β : Type u_1
xs : Vector α n
σ : Type
f : α → σ → σ × β
s : σ
h : ∀ (a : α), (f a s).fst = s
⊢ mapAccumr f xs s = (s, map (fun x => (f x s).snd) xs)
[PROOFSTEP]
induction xs using revInductionOn
[GOAL]
case nil
α : Type u_2
n : ℕ
β : Type u_1
xs : Vector α n
σ : Type
f : α → σ → σ × β
s : σ
h : ∀ (a : α), (f a s).fst = s
⊢ mapAccumr f nil s = (s, map (fun x => (f x s).snd) nil)
[PROOFSTEP]
simp_all
[GOAL]
case snoc
α : Type u_2
n : ℕ
β : Type u_1
xs : Vector α n
σ : Type
f : α → σ → σ × β
s : σ
h : ∀ (a : α), (f a s).fst = s
n✝ : ℕ
xs✝ : Vector α n✝
x✝ : α
a✝ : mapAccumr f xs✝ s = (s, map (fun x => (f x s).snd) xs✝)
⊢ mapAccumr f (snoc xs✝ x✝) s = (s, map (fun x => (f x s).snd) (snoc xs✝ x✝))
[PROOFSTEP]
simp_all
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
f : α → β → σ → σ × γ
s : σ
h : ∀ (a : α) (b : β), (f a b s).fst = s
⊢ mapAccumr₂ f xs ys s = (s, map₂ (fun x y => (f x y s).snd) xs ys)
[PROOFSTEP]
induction xs, ys using revInductionOn₂
[GOAL]
case nil
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
f : α → β → σ → σ × γ
s : σ
h : ∀ (a : α) (b : β), (f a b s).fst = s
⊢ mapAccumr₂ f nil nil s = (s, map₂ (fun x y => (f x y s).snd) nil nil)
[PROOFSTEP]
simp_all
[GOAL]
case snoc
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
f : α → β → σ → σ × γ
s : σ
h : ∀ (a : α) (b : β), (f a b s).fst = s
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ : mapAccumr₂ f xs✝ ys✝ s = (s, map₂ (fun x y => (f x y s).snd) xs✝ ys✝)
⊢ mapAccumr₂ f (snoc xs✝ x✝) (snoc ys✝ y✝) s = (s, map₂ (fun x y => (f x y s).snd) (snoc xs✝ x✝) (snoc ys✝ y✝))
[PROOFSTEP]
simp_all
[GOAL]
α : Type u_2
n : ℕ
β : Type u_1
xs : Vector α n
ys : Vector β n
σ : Type
s : σ
f : α → σ × σ → (σ × σ) × β
h : ∀ (x : α) (s : σ), (f x (s, s)).fst.fst = (f x (s, s)).fst.snd
⊢ ∃ R,
    R (s, s) s ∧
      ∀ {s : σ × σ} {q : σ} (a : α),
        R s q →
          R (f a s).fst ((f a (q, q)).fst.fst, (f a (q, q)).snd).fst ∧
            (f a s).snd = ((f a (q, q)).fst.fst, (f a (q, q)).snd).snd
[PROOFSTEP]
use fun (s₁, s₂) s => s₂ = s ∧ s₁ = s
[GOAL]
case h
α : Type u_2
n : ℕ
β : Type u_1
xs : Vector α n
ys : Vector β n
σ : Type
s : σ
f : α → σ × σ → (σ × σ) × β
h : ∀ (x : α) (s : σ), (f x (s, s)).fst.fst = (f x (s, s)).fst.snd
⊢ (match (s, s) with
    | (s₁, s₂) => s₂ = s ∧ s₁ = s) ∧
    ∀ {s : σ × σ} {q : σ} (a : α),
      (match s with
        | (s₁, s₂) => s₂ = q ∧ s₁ = q) →
        (match (f a s).fst with
          | (s₁, s₂) =>
            s₂ = ((f a (q, q)).fst.fst, (f a (q, q)).snd).fst ∧ s₁ = ((f a (q, q)).fst.fst, (f a (q, q)).snd).fst) ∧
          (f a s).snd = ((f a (q, q)).fst.fst, (f a (q, q)).snd).snd
[PROOFSTEP]
simp_all
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
s : σ
f : α → β → σ × σ → (σ × σ) × γ
h :
  ∀ (x : α) (y : β) (s : σ),
    let s' := (f x y (s, s)).fst;
    s'.fst = s'.snd
⊢ ∃ R,
    R (s, s) s ∧
      ∀ {s : σ × σ} {q : σ} (a : α) (b : β),
        R s q →
          R (f a b s).fst ((f a b (q, q)).fst.fst, (f a b (q, q)).snd).fst ∧
            (f a b s).snd = ((f a b (q, q)).fst.fst, (f a b (q, q)).snd).snd
[PROOFSTEP]
use fun (s₁, s₂) s => s₂ = s ∧ s₁ = s
[GOAL]
case h
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
s : σ
f : α → β → σ × σ → (σ × σ) × γ
h :
  ∀ (x : α) (y : β) (s : σ),
    let s' := (f x y (s, s)).fst;
    s'.fst = s'.snd
⊢ (match (s, s) with
    | (s₁, s₂) => s₂ = s ∧ s₁ = s) ∧
    ∀ {s : σ × σ} {q : σ} (a : α) (b : β),
      (match s with
        | (s₁, s₂) => s₂ = q ∧ s₁ = q) →
        (match (f a b s).fst with
          | (s₁, s₂) =>
            s₂ = ((f a b (q, q)).fst.fst, (f a b (q, q)).snd).fst ∧
              s₁ = ((f a b (q, q)).fst.fst, (f a b (q, q)).snd).fst) ∧
          (f a b s).snd = ((f a b (q, q)).fst.fst, (f a b (q, q)).snd).snd
[PROOFSTEP]
simp_all
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
s : σ
inst✝ : Inhabited α
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f default b s = f a b s
⊢ mapAccumr₂ f xs ys s = mapAccumr (fun b s => f default b s) ys s
[PROOFSTEP]
induction xs, ys using Vector.revInductionOn₂ generalizing s
[GOAL]
case nil
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
inst✝ : Inhabited α
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f default b s = f a b s
s : σ
⊢ mapAccumr₂ f nil nil s = mapAccumr (fun b s => f default b s) nil s
case snoc
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
inst✝ : Inhabited α
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f default b s = f a b s
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ : ∀ {s : σ}, mapAccumr₂ f xs✝ ys✝ s = mapAccumr (fun b s => f default b s) ys✝ s
s : σ
⊢ mapAccumr₂ f (snoc xs✝ x✝) (snoc ys✝ y✝) s = mapAccumr (fun b s => f default b s) (snoc ys✝ y✝) s
[PROOFSTEP]
case nil => rfl
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
inst✝ : Inhabited α
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f default b s = f a b s
s : σ
⊢ mapAccumr₂ f nil nil s = mapAccumr (fun b s => f default b s) nil s
[PROOFSTEP]
case nil => rfl
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
inst✝ : Inhabited α
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f default b s = f a b s
s : σ
⊢ mapAccumr₂ f nil nil s = mapAccumr (fun b s => f default b s) nil s
[PROOFSTEP]
rfl
[GOAL]
case snoc
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
inst✝ : Inhabited α
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f default b s = f a b s
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ : ∀ {s : σ}, mapAccumr₂ f xs✝ ys✝ s = mapAccumr (fun b s => f default b s) ys✝ s
s : σ
⊢ mapAccumr₂ f (snoc xs✝ x✝) (snoc ys✝ y✝) s = mapAccumr (fun b s => f default b s) (snoc ys✝ y✝) s
[PROOFSTEP]
case snoc xs ys x y ih => simp [h x y s, ih]
[GOAL]
α : Type
n : ℕ
β : Type
xs✝ : Vector α n
ys✝ : Vector β n
σ γ : Type
inst✝ : Inhabited α
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f default b s = f a b s
n✝ : ℕ
xs : Vector α n✝
ys : Vector β n✝
x : α
y : β
ih : ∀ {s : σ}, mapAccumr₂ f xs ys s = mapAccumr (fun b s => f default b s) ys s
s : σ
⊢ mapAccumr₂ f (snoc xs x) (snoc ys y) s = mapAccumr (fun b s => f default b s) (snoc ys y) s
[PROOFSTEP]
case snoc xs ys x y ih => simp [h x y s, ih]
[GOAL]
α : Type
n : ℕ
β : Type
xs✝ : Vector α n
ys✝ : Vector β n
σ γ : Type
inst✝ : Inhabited α
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f default b s = f a b s
n✝ : ℕ
xs : Vector α n✝
ys : Vector β n✝
x : α
y : β
ih : ∀ {s : σ}, mapAccumr₂ f xs ys s = mapAccumr (fun b s => f default b s) ys s
s : σ
⊢ mapAccumr₂ f (snoc xs x) (snoc ys y) s = mapAccumr (fun b s => f default b s) (snoc ys y) s
[PROOFSTEP]
simp [h x y s, ih]
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
s : σ
inst✝ : Inhabited β
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f a default s = f a b s
⊢ mapAccumr₂ f xs ys s = mapAccumr (fun a s => f a default s) xs s
[PROOFSTEP]
induction xs, ys using Vector.revInductionOn₂ generalizing s
[GOAL]
case nil
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
inst✝ : Inhabited β
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f a default s = f a b s
s : σ
⊢ mapAccumr₂ f nil nil s = mapAccumr (fun a s => f a default s) nil s
case snoc
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
inst✝ : Inhabited β
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f a default s = f a b s
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ : ∀ {s : σ}, mapAccumr₂ f xs✝ ys✝ s = mapAccumr (fun a s => f a default s) xs✝ s
s : σ
⊢ mapAccumr₂ f (snoc xs✝ x✝) (snoc ys✝ y✝) s = mapAccumr (fun a s => f a default s) (snoc xs✝ x✝) s
[PROOFSTEP]
case nil => rfl
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
inst✝ : Inhabited β
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f a default s = f a b s
s : σ
⊢ mapAccumr₂ f nil nil s = mapAccumr (fun a s => f a default s) nil s
[PROOFSTEP]
case nil => rfl
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
inst✝ : Inhabited β
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f a default s = f a b s
s : σ
⊢ mapAccumr₂ f nil nil s = mapAccumr (fun a s => f a default s) nil s
[PROOFSTEP]
rfl
[GOAL]
case snoc
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
inst✝ : Inhabited β
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f a default s = f a b s
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ : ∀ {s : σ}, mapAccumr₂ f xs✝ ys✝ s = mapAccumr (fun a s => f a default s) xs✝ s
s : σ
⊢ mapAccumr₂ f (snoc xs✝ x✝) (snoc ys✝ y✝) s = mapAccumr (fun a s => f a default s) (snoc xs✝ x✝) s
[PROOFSTEP]
case snoc xs ys x y ih => simp [h x y s, ih]
[GOAL]
α : Type
n : ℕ
β : Type
xs✝ : Vector α n
ys✝ : Vector β n
σ γ : Type
inst✝ : Inhabited β
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f a default s = f a b s
n✝ : ℕ
xs : Vector α n✝
ys : Vector β n✝
x : α
y : β
ih : ∀ {s : σ}, mapAccumr₂ f xs ys s = mapAccumr (fun a s => f a default s) xs s
s : σ
⊢ mapAccumr₂ f (snoc xs x) (snoc ys y) s = mapAccumr (fun a s => f a default s) (snoc xs x) s
[PROOFSTEP]
case snoc xs ys x y ih => simp [h x y s, ih]
[GOAL]
α : Type
n : ℕ
β : Type
xs✝ : Vector α n
ys✝ : Vector β n
σ γ : Type
inst✝ : Inhabited β
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f a default s = f a b s
n✝ : ℕ
xs : Vector α n✝
ys : Vector β n✝
x : α
y : β
ih : ∀ {s : σ}, mapAccumr₂ f xs ys s = mapAccumr (fun a s => f a default s) xs s
s : σ
⊢ mapAccumr₂ f (snoc xs x) (snoc ys y) s = mapAccumr (fun a s => f a default s) (snoc xs x) s
[PROOFSTEP]
simp [h x y s, ih]
[GOAL]
α : Type u_2
n : ℕ
xs ys : Vector α n
β : Type u_1
f : α → α → β
comm : ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁
⊢ map₂ f xs ys = map₂ f ys xs
[PROOFSTEP]
induction xs, ys using Vector.inductionOn₂
[GOAL]
case nil
α : Type u_2
n : ℕ
xs ys : Vector α n
β : Type u_1
f : α → α → β
comm : ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁
⊢ map₂ f nil nil = map₂ f nil nil
[PROOFSTEP]
simp_all
[GOAL]
case cons
α : Type u_2
n : ℕ
xs ys : Vector α n
β : Type u_1
f : α → α → β
comm : ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁
n✝ : ℕ
a✝¹ b✝ : α
x✝ y✝ : Vector α n✝
a✝ : map₂ f x✝ y✝ = map₂ f y✝ x✝
⊢ map₂ f (a✝¹ ::ᵥ x✝) (b✝ ::ᵥ y✝) = map₂ f (b✝ ::ᵥ y✝) (a✝¹ ::ᵥ x✝)
[PROOFSTEP]
simp_all
[GOAL]
α : Type
n : ℕ
xs ys : Vector α n
σ γ : Type
s : σ
f : α → α → σ → σ × γ
comm : ∀ (a₁ a₂ : α) (s : σ), f a₁ a₂ s = f a₂ a₁ s
⊢ mapAccumr₂ f xs ys s = mapAccumr₂ f ys xs s
[PROOFSTEP]
induction xs, ys using Vector.inductionOn₂ generalizing s
[GOAL]
case nil
α : Type
n : ℕ
xs ys : Vector α n
σ γ : Type
f : α → α → σ → σ × γ
comm : ∀ (a₁ a₂ : α) (s : σ), f a₁ a₂ s = f a₂ a₁ s
s : σ
⊢ mapAccumr₂ f nil nil s = mapAccumr₂ f nil nil s
[PROOFSTEP]
simp_all
[GOAL]
case cons
α : Type
n : ℕ
xs ys : Vector α n
σ γ : Type
f : α → α → σ → σ × γ
comm : ∀ (a₁ a₂ : α) (s : σ), f a₁ a₂ s = f a₂ a₁ s
n✝ : ℕ
a✝¹ b✝ : α
x✝ y✝ : Vector α n✝
a✝ : ∀ {s : σ}, mapAccumr₂ f x✝ y✝ s = mapAccumr₂ f y✝ x✝ s
s : σ
⊢ mapAccumr₂ f (a✝¹ ::ᵥ x✝) (b✝ ::ᵥ y✝) s = mapAccumr₂ f (b✝ ::ᵥ y✝) (a✝¹ ::ᵥ x✝) s
[PROOFSTEP]
simp_all
[GOAL]
α : Type u_2
n : ℕ
β : Type u_3
xs : Vector α n
ys : Vector β n
γ : Type u_1
f : α → β → γ
⊢ map₂ f xs ys = map₂ (flip f) ys xs
[PROOFSTEP]
induction xs, ys using Vector.inductionOn₂
[GOAL]
case nil
α : Type u_2
n : ℕ
β : Type u_3
xs : Vector α n
ys : Vector β n
γ : Type u_1
f : α → β → γ
⊢ map₂ f nil nil = map₂ (flip f) nil nil
[PROOFSTEP]
simp_all [flip]
[GOAL]
case cons
α : Type u_2
n : ℕ
β : Type u_3
xs : Vector α n
ys : Vector β n
γ : Type u_1
f : α → β → γ
n✝ : ℕ
a✝¹ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
a✝ : map₂ f x✝ y✝ = map₂ (flip f) y✝ x✝
⊢ map₂ f (a✝¹ ::ᵥ x✝) (b✝ ::ᵥ y✝) = map₂ (flip f) (b✝ ::ᵥ y✝) (a✝¹ ::ᵥ x✝)
[PROOFSTEP]
simp_all [flip]
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
s : σ
f : α → β → σ → σ × γ
⊢ mapAccumr₂ f xs ys s = mapAccumr₂ (flip f) ys xs s
[PROOFSTEP]
induction xs, ys using Vector.inductionOn₂
[GOAL]
case nil
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
s : σ
f : α → β → σ → σ × γ
⊢ mapAccumr₂ f nil nil s = mapAccumr₂ (flip f) nil nil s
[PROOFSTEP]
simp_all [flip]
[GOAL]
case cons
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
s : σ
f : α → β → σ → σ × γ
n✝ : ℕ
a✝¹ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
a✝ : mapAccumr₂ f x✝ y✝ s = mapAccumr₂ (flip f) y✝ x✝ s
⊢ mapAccumr₂ f (a✝¹ ::ᵥ x✝) (b✝ ::ᵥ y✝) s = mapAccumr₂ (flip f) (b✝ ::ᵥ y✝) (a✝¹ ::ᵥ x✝) s
[PROOFSTEP]
simp_all [flip]
