awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Vector.Defs
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p : α → Prop
v : Vector α n
i : ℕ
hi : i < v.toList.length
⊢ i < n

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.Defs
Goal:
α : Type u_1
n : ℕ
v : Vector α n
i : ℕ
hi : i < v.toList.length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) v.toList i hi =
    getElem (valid := fun (x : Vector α n) (i : ℕ) ↦ i < n) v i ⋯

Tactic:
rfl

Premises used: List.Vector.get, List.Vector.toList, rfl
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
s₁ : σ₁
s₂ : σ₂
xs : Vector α n
f₁ : β → σ₁ → σ₁ × γ
f₂ : α → σ₂ → σ₂ × β
nil :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    mapAccumr f₁ (mapAccumr f₂ Vector.nil s₂).2 s₁ =
      let m : (σ₁ × σ₂) × Vector γ 0 :=
        mapAccumr
          (fun (x : α) (s : σ₁ × σ₂) ↦
            let r₂ := f₂ x s.2;
            let r₁ := f₁ r₂.2 s.1;
            ((r₁.1, r₂.1), r₁.2))
          Vector.nil (s₁, s₂);
      (m.1.1, m.2)
snoc :
  ∀ {n : ℕ} (xs : Vector α n) (x : α),
    (∀ {s₁ : σ₁} {s₂ : σ₂},
        mapAccumr f₁ (mapAccumr f₂ xs s₂).2 s₁ =
          let m : (σ₁ × σ₂) × Vector γ n :=
            mapAccumr
              (fun (x : α) (s : σ₁ × σ₂) ↦
                let r₂ := f₂ x s.2;
                let r₁ := f₁ r₂.2 s.1;
                ((r₁.1, r₂.1), r₁.2))
              xs (s₁, s₂);
          (m.1.1, m.2)) →
      ∀ {s₁ : σ₁} {s₂ : σ₂},
        mapAccumr f₁ (mapAccumr f₂ (xs.snoc x) s₂).2 s₁ =
          let m : (σ₁ × σ₂) × Vector γ (n + 1) :=
            mapAccumr
              (fun (x : α) (s : σ₁ × σ₂) ↦
                let r₂ := f₂ x s.2;
                let r₁ := f₁ r₂.2 s.1;
                ((r₁.1, r₂.1), r₁.2))
              (xs.snoc x) (s₁, s₂);
          (m.1.1, m.2)
⊢ mapAccumr f₁ (mapAccumr f₂ xs s₂).2 s₁ =
    let m : (σ₁ × σ₂) × Vector γ n :=
      mapAccumr
        (fun (x : α) (s : σ₁ × σ₂) ↦
          let r₂ := f₂ x s.2;
          let r₁ := f₁ r₂.2 s.1;
          ((r₁.1, r₂.1), r₁.2))
        xs (s₁, s₂);
    (m.1.1, m.2)

Tactic:
induction xs using Vector.revInductionOn generalizing s₁ s₂
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
f₁ : β → σ₁ → σ₁ × γ
f₂ : α → σ₂ → σ₂ × β
s₁ : σ₁
s₂ : σ₂
⊢ mapAccumr f₁ (mapAccumr f₂ nil s₂).2 s₁ =
    let m : (σ₁ × σ₂) × Vector γ 0 :=
      mapAccumr
        (fun (x : α) (s : σ₁ × σ₂) ↦
          let r₂ := f₂ x s.2;
          let r₁ := f₁ r₂.2 s.1;
          ((r₁.1, r₂.1), r₁.2))
        nil (s₁, s₂);
    (m.1.1, m.2)

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
f₁ : β → σ₁ → σ₁ × γ
f₂ : α → σ₂ → σ₂ × β
n_1 : ℕ
xs : Vector α n_1
x : α
h :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    mapAccumr f₁ (mapAccumr f₂ xs s₂).2 s₁ =
      let m : (σ₁ × σ₂) × Vector γ n_1 :=
        mapAccumr
          (fun (x : α) (s : σ₁ × σ₂) ↦
            let r₂ := f₂ x s.2;
            let r₁ := f₁ r₂.2 s.1;
            ((r₁.1, r₂.1), r₁.2))
          xs (s₁, s₂);
      (m.1.1, m.2)
s₁ : σ₁
s₂ : σ₂
⊢ mapAccumr f₁ (mapAccumr f₂ (xs.snoc x) s₂).2 s₁ =
    let m : (σ₁ × σ₂) × Vector γ (n_1 + 1) :=
      mapAccumr
        (fun (x : α) (s : σ₁ × σ₂) ↦
          let r₂ := f₂ x s.2;
          let r₁ := f₁ r₂.2 s.1;
          ((r₁.1, r₂.1), r₁.2))
        (xs.snoc x) (s₁, s₂);
    (m.1.1, m.2)

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
n : ℕ
xs : Vector α n
f₁ : β → σ₁ → σ₁ × γ
s : σ₁
f₂ : α → β
nil : ∀ {s : σ₁}, mapAccumr f₁ (map f₂ Vector.nil) s = mapAccumr (fun (x : α) (s : σ₁) ↦ f₁ (f₂ x) s) Vector.nil s
snoc :
  ∀ {n : ℕ} (xs : Vector α n) (x : α),
    (∀ {s : σ₁}, mapAccumr f₁ (map f₂ xs) s = mapAccumr (fun (x : α) (s : σ₁) ↦ f₁ (f₂ x) s) xs s) →
      ∀ {s : σ₁}, mapAccumr f₁ (map f₂ (xs.snoc x)) s = mapAccumr (fun (x : α) (s : σ₁) ↦ f₁ (f₂ x) s) (xs.snoc x) s
⊢ mapAccumr f₁ (map f₂ xs) s = mapAccumr (fun (x : α) (s : σ₁) ↦ f₁ (f₂ x) s) xs s

Tactic:
induction xs using Vector.revInductionOn generalizing s
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
n : ℕ
xs : Vector α n
f₁ : β → σ₁ → σ₁ × γ
f₂ : α → β
s : σ₁
⊢ mapAccumr f₁ (map f₂ nil) s = mapAccumr (fun (x : α) (s : σ₁) ↦ f₁ (f₂ x) s) nil s

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
n : ℕ
xs : Vector α n
f₁ : β → σ₁ → σ₁ × γ
f₂ : α → β
n_1 : ℕ
xs_1 : Vector α n_1
x : α
h : ∀ {s : σ₁}, mapAccumr f₁ (map f₂ xs_1) s = mapAccumr (fun (x : α) (s : σ₁) ↦ f₁ (f₂ x) s) xs_1 s
s : σ₁
⊢ mapAccumr f₁ (map f₂ (xs_1.snoc x)) s = mapAccumr (fun (x : α) (s : σ₁) ↦ f₁ (f₂ x) s) (xs_1.snoc x) s

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₂ : Type u_7
n : ℕ
xs : Vector α n
f₂ : α → σ₂ → σ₂ × β
s : σ₂
f₁ : β → γ
nil :
  ∀ {s : σ₂},
    map f₁ (mapAccumr f₂ Vector.nil s).2 =
      (mapAccumr
          (fun (x : α) (s : σ₂) ↦
            let r := f₂ x s;
            (r.1, f₁ r.2))
          Vector.nil s).2
snoc :
  ∀ {n : ℕ} (xs : Vector α n) (x : α),
    (∀ {s : σ₂},
        map f₁ (mapAccumr f₂ xs s).2 =
          (mapAccumr
              (fun (x : α) (s : σ₂) ↦
                let r := f₂ x s;
                (r.1, f₁ r.2))
              xs s).2) →
      ∀ {s : σ₂},
        map f₁ (mapAccumr f₂ (xs.snoc x) s).2 =
          (mapAccumr
              (fun (x : α) (s : σ₂) ↦
                let r := f₂ x s;
                (r.1, f₁ r.2))
              (xs.snoc x) s).2
⊢ map f₁ (mapAccumr f₂ xs s).2 =
    (mapAccumr
        (fun (x : α) (s : σ₂) ↦
          let r := f₂ x s;
          (r.1, f₁ r.2))
        xs s).2

Tactic:
induction xs using Vector.revInductionOn generalizing s
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₂ : Type u_7
n : ℕ
xs : Vector α n
f₂ : α → σ₂ → σ₂ × β
f₁ : β → γ
s : σ₂
⊢ map f₁ (mapAccumr f₂ nil s).2 =
    (mapAccumr
        (fun (x : α) (s : σ₂) ↦
          let r := f₂ x s;
          (r.1, f₁ r.2))
        nil s).2

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₂ : Type u_7
n : ℕ
xs : Vector α n
f₂ : α → σ₂ → σ₂ × β
f₁ : β → γ
n_1 : ℕ
xs_1 : Vector α n_1
x : α
h :
  ∀ {s : σ₂},
    map f₁ (mapAccumr f₂ xs_1 s).2 =
      (mapAccumr
          (fun (x : α) (s : σ₂) ↦
            let r := f₂ x s;
            (r.1, f₁ r.2))
          xs_1 s).2
s : σ₂
⊢ map f₁ (mapAccumr f₂ (xs_1.snoc x) s).2 =
    (mapAccumr
        (fun (x : α) (s : σ₂) ↦
          let r := f₂ x s;
          (r.1, f₁ r.2))
        (xs_1.snoc x) s).2

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
f₁ : β → γ
f₂ : α → β
nil : map f₁ (map f₂ Vector.nil) = map (fun (x : α) ↦ f₁ (f₂ x)) Vector.nil
cons :
  ∀ {n : ℕ} {x : α} {w : Vector α n},
    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)
⊢ map f₁ (map f₂ xs) = map (fun (x : α) ↦ f₁ (f₂ x)) xs

Tactic:
induction xs
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
f₁ : β → γ
f₂ : α → β
⊢ map f₁ (map f₂ nil) = map (fun (x : α) ↦ f₁ (f₂ x)) nil

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
f₁ : β → γ
f₂ : α → β
n_1 : ℕ
x : α
w : Vector α n_1
h : 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)

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
p : α → Prop
f₁ : β → γ
f₂ : (a : α) → p a → β
H : ∀ (x : α), x ∈ xs.toList → p x
nil :
  ∀ (H : ∀ (x : α), Membership.mem (γ := List α) (toList Vector.nil) x → p x),
    map f₁ (pmap (p := p) f₂ Vector.nil H) = pmap (p := p) (fun (x : α) (hx : p x) ↦ f₁ (f₂ x hx)) Vector.nil H
cons :
  ∀ {n : ℕ} {x : α} {w : Vector α n},
    (∀ (H : ∀ (x : α), x ∈ w.toList → p x),
        map f₁ (pmap (p := p) f₂ w H) = pmap (p := p) (fun (x : α) (hx : p x) ↦ f₁ (f₂ x hx)) w H) →
      ∀ (H : ∀ (x_1 : α), x_1 ∈ (x ::ᵥ w).toList → p x_1),
        map f₁ (pmap (p := p) f₂ (x ::ᵥ w) H) = pmap (p := p) (fun (x : α) (hx : p x) ↦ f₁ (f₂ x hx)) (x ::ᵥ w) H
⊢ map f₁ (pmap (p := p) f₂ xs H) = pmap (p := p) (fun (x : α) (hx : p x) ↦ f₁ (f₂ x hx)) xs H

Tactic:
induction xs
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
p : α → Prop
f₁ : β → γ
f₂ : (a : α) → p a → β
H : ∀ (x : α), Membership.mem (γ := List α) (toList nil) x → p x
⊢ map f₁ (pmap (p := p) f₂ nil H) = pmap (p := p) (fun (x : α) (hx : p x) ↦ f₁ (f₂ x hx)) nil H

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
p : α → Prop
f₁ : β → γ
f₂ : (a : α) → p a → β
n_1 : ℕ
x : α
w : Vector α n_1
h :
  ∀ (H : ∀ (x : α), x ∈ w.toList → p x),
    map f₁ (pmap (p := p) f₂ w H) = pmap (p := p) (fun (x : α) (hx : p x) ↦ f₁ (f₂ x hx)) w H
H : ∀ (x_1 : α), x_1 ∈ (x ::ᵥ w).toList → p x_1
⊢ map f₁ (pmap (p := p) f₂ (x ::ᵥ w) H) = pmap (p := p) (fun (x : α) (hx : p x) ↦ f₁ (f₂ x hx)) (x ::ᵥ w) H

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ζ : Type u_4
σ : Type u_5
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
s : σ
s₁ : σ₁
s₂ : σ₂
xs : Vector α n
f₁_1 : β → σ₁ → σ₁ × γ
f₂_1 : α → σ₂ → σ₂ × β
p : β → Prop
f₁ : (b : β) → p b → γ
f₂ : α → β
H : ∀ (x : β), x ∈ (map f₂ xs).toList → p x
⊢ ∀ (x : α), x ∈ xs.toList → p (f₂ x)

Tactic:
simpa using H
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
p : β → Prop
f₁ : (b : β) → p b → γ
f₂ : α → β
H : ∀ (x : β), x ∈ (map f₂ xs).toList → p x
nil :
  ∀ (H : ∀ (x : β), x ∈ (map f₂ Vector.nil).toList → p x),
    pmap (p := p) f₁ (map f₂ Vector.nil) H =
      pmap (p := fun (x : α) ↦ p (f₂ x)) (fun (x : α) (hx : p (f₂ x)) ↦ f₁ (f₂ x) hx) Vector.nil ⋯
cons :
  ∀ {n : ℕ} {x : α} {w : Vector α n},
    (∀ (H : ∀ (x : β), x ∈ (map f₂ w).toList → p x),
        pmap (p := p) f₁ (map f₂ w) H =
          pmap (p := fun (x : α) ↦ p (f₂ x)) (fun (x : α) (hx : p (f₂ x)) ↦ f₁ (f₂ x) hx) w ⋯) →
      ∀ (H : ∀ (x_1 : β), x_1 ∈ (map f₂ (x ::ᵥ w)).toList → p x_1),
        pmap (p := p) f₁ (map f₂ (x ::ᵥ w)) H =
          pmap (p := fun (x : α) ↦ p (f₂ x)) (fun (x : α) (hx : p (f₂ x)) ↦ f₁ (f₂ x) hx) (x ::ᵥ w) ⋯
⊢ pmap (p := p) f₁ (map f₂ xs) H = pmap (p := fun (x : α) ↦ p (f₂ x)) (fun (x : α) (hx : p (f₂ x)) ↦ f₁ (f₂ x) hx) xs ⋯

Tactic:
induction xs
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
p : β → Prop
f₁ : (b : β) → p b → γ
f₂ : α → β
H : ∀ (x : β), x ∈ (map f₂ nil).toList → p x
⊢ pmap (p := p) f₁ (map f₂ nil) H =
    pmap (p := fun (x : α) ↦ p (f₂ x)) (fun (x : α) (hx : p (f₂ x)) ↦ f₁ (f₂ x) hx) nil ⋯

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
p : β → Prop
f₁ : (b : β) → p b → γ
f₂ : α → β
n_1 : ℕ
x : α
w : Vector α n_1
h :
  ∀ (H : ∀ (x : β), x ∈ (map f₂ w).toList → p x),
    pmap (p := p) f₁ (map f₂ w) H = pmap (p := fun (x : α) ↦ p (f₂ x)) (fun (x : α) (hx : p (f₂ x)) ↦ f₁ (f₂ x) hx) w ⋯
H : ∀ (x_1 : β), x_1 ∈ (map f₂ (x ::ᵥ w)).toList → p x_1
⊢ pmap (p := p) f₁ (map f₂ (x ::ᵥ w)) H =
    pmap (p := fun (x : α) ↦ p (f₂ x)) (fun (x : α) (hx : p (f₂ x)) ↦ f₁ (f₂ x) hx) (x ::ᵥ w) ⋯

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ζ : Type u_4
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
s₁ : σ₁
s₂ : σ₂
xs : Vector α n
ys : Vector β n
f₁ : γ → β → σ₁ → σ₁ × ζ
f₂ : α → σ₂ → σ₂ × γ
nil :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    mapAccumr₂ f₁ (mapAccumr f₂ Vector.nil s₂).2 Vector.nil s₁ =
      let m : (σ₁ × σ₂) × Vector ζ 0 :=
        mapAccumr₂
          (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
            let r₂ := f₂ x s.2;
            let r₁ := f₁ r₂.2 y s.1;
            ((r₁.1, r₂.1), r₁.2))
          Vector.nil Vector.nil (s₁, s₂);
      (m.1.1, m.2)
snoc :
  ∀ {n : ℕ} (xs : Vector α n) (ys : Vector β n) (x : α) (y : β),
    (∀ {s₁ : σ₁} {s₂ : σ₂},
        mapAccumr₂ f₁ (mapAccumr f₂ xs s₂).2 ys s₁ =
          let m : (σ₁ × σ₂) × Vector ζ n :=
            mapAccumr₂
              (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
                let r₂ := f₂ x s.2;
                let r₁ := f₁ r₂.2 y s.1;
                ((r₁.1, r₂.1), r₁.2))
              xs ys (s₁, s₂);
          (m.1.1, m.2)) →
      ∀ {s₁ : σ₁} {s₂ : σ₂},
        mapAccumr₂ f₁ (mapAccumr f₂ (xs.snoc x) s₂).2 (ys.snoc y) s₁ =
          let m : (σ₁ × σ₂) × Vector ζ (n + 1) :=
            mapAccumr₂
              (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
                let r₂ := f₂ x s.2;
                let r₁ := f₁ r₂.2 y s.1;
                ((r₁.1, r₂.1), r₁.2))
              (xs.snoc x) (ys.snoc y) (s₁, s₂);
          (m.1.1, m.2)
⊢ mapAccumr₂ f₁ (mapAccumr f₂ xs s₂).2 ys s₁ =
    let m : (σ₁ × σ₂) × Vector ζ n :=
      mapAccumr₂
        (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
          let r₂ := f₂ x s.2;
          let r₁ := f₁ r₂.2 y s.1;
          ((r₁.1, r₂.1), r₁.2))
        xs ys (s₁, s₂);
    (m.1.1, m.2)

Tactic:
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ζ : Type u_4
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
f₁ : γ → β → σ₁ → σ₁ × ζ
f₂ : α → σ₂ → σ₂ × γ
s₁ : σ₁
s₂ : σ₂
⊢ mapAccumr₂ f₁ (mapAccumr f₂ nil s₂).2 nil s₁ =
    let m : (σ₁ × σ₂) × Vector ζ 0 :=
      mapAccumr₂
        (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
          let r₂ := f₂ x s.2;
          let r₁ := f₁ r₂.2 y s.1;
          ((r₁.1, r₂.1), r₁.2))
        nil nil (s₁, s₂);
    (m.1.1, m.2)

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ζ : Type u_4
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
f₁ : γ → β → σ₁ → σ₁ × ζ
f₂ : α → σ₂ → σ₂ × γ
n_1 : ℕ
xs : Vector α n_1
ys : Vector β n_1
x : α
y : β
h :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    mapAccumr₂ f₁ (mapAccumr f₂ xs s₂).2 ys s₁ =
      let m : (σ₁ × σ₂) × Vector ζ n_1 :=
        mapAccumr₂
          (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
            let r₂ := f₂ x s.2;
            let r₁ := f₁ r₂.2 y s.1;
            ((r₁.1, r₂.1), r₁.2))
          xs ys (s₁, s₂);
      (m.1.1, m.2)
s₁ : σ₁
s₂ : σ₂
⊢ mapAccumr₂ f₁ (mapAccumr f₂ (xs.snoc x) s₂).2 (ys.snoc y) s₁ =
    let m : (σ₁ × σ₂) × Vector ζ (n_1 + 1) :=
      mapAccumr₂
        (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
          let r₂ := f₂ x s.2;
          let r₁ := f₁ r₂.2 y s.1;
          ((r₁.1, r₂.1), r₁.2))
        (xs.snoc x) (ys.snoc y) (s₁, s₂);
    (m.1.1, m.2)

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ζ : Type u_4
n : ℕ
xs : Vector α n
ys : Vector β n
f₁ : γ → β → ζ
f₂ : α → γ
nil : map₂ f₁ (map f₂ Vector.nil) Vector.nil = map₂ (fun (x : α) (y : β) ↦ f₁ (f₂ x) y) Vector.nil Vector.nil
snoc :
  ∀ {n : ℕ} (xs : Vector α n) (ys : Vector β n) (x : α) (y : β),
    map₂ f₁ (map f₂ xs) ys = map₂ (fun (x : α) (y : β) ↦ f₁ (f₂ x) y) xs ys →
      map₂ f₁ (map f₂ (xs.snoc x)) (ys.snoc y) = map₂ (fun (x : α) (y : β) ↦ f₁ (f₂ x) y) (xs.snoc x) (ys.snoc y)
⊢ map₂ f₁ (map f₂ xs) ys = map₂ (fun (x : α) (y : β) ↦ f₁ (f₂ x) y) xs ys

Tactic:
induction xs, ys using Vector.revInductionOn₂
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ζ : Type u_4
n : ℕ
xs : Vector α n
ys : Vector β n
f₁ : γ → β → ζ
f₂ : α → γ
⊢ map₂ f₁ (map f₂ nil) nil = map₂ (fun (x : α) (y : β) ↦ f₁ (f₂ x) y) nil nil

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ζ : Type u_4
n : ℕ
xs : Vector α n
ys : Vector β n
f₁ : γ → β → ζ
f₂ : α → γ
n_1 : ℕ
xs_1 : Vector α n_1
ys_1 : Vector β n_1
x : α
y : β
h : map₂ f₁ (map f₂ xs_1) ys_1 = map₂ (fun (x : α) (y : β) ↦ f₁ (f₂ x) y) xs_1 ys_1
⊢ map₂ f₁ (map f₂ (xs_1.snoc x)) (ys_1.snoc y) = map₂ (fun (x : α) (y : β) ↦ f₁ (f₂ x) y) (xs_1.snoc x) (ys_1.snoc y)

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ζ : Type u_4
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
s₁ : σ₁
s₂ : σ₂
xs : Vector α n
ys : Vector β n
f₁ : α → γ → σ₁ → σ₁ × ζ
f₂ : β → σ₂ → σ₂ × γ
nil :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    mapAccumr₂ f₁ Vector.nil (mapAccumr f₂ Vector.nil s₂).2 s₁ =
      let m : (σ₁ × σ₂) × Vector ζ 0 :=
        mapAccumr₂
          (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
            let r₂ := f₂ y s.2;
            let r₁ := f₁ x r₂.2 s.1;
            ((r₁.1, r₂.1), r₁.2))
          Vector.nil Vector.nil (s₁, s₂);
      (m.1.1, m.2)
snoc :
  ∀ {n : ℕ} (xs : Vector α n) (ys : Vector β n) (x : α) (y : β),
    (∀ {s₁ : σ₁} {s₂ : σ₂},
        mapAccumr₂ f₁ xs (mapAccumr f₂ ys s₂).2 s₁ =
          let m : (σ₁ × σ₂) × Vector ζ n :=
            mapAccumr₂
              (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
                let r₂ := f₂ y s.2;
                let r₁ := f₁ x r₂.2 s.1;
                ((r₁.1, r₂.1), r₁.2))
              xs ys (s₁, s₂);
          (m.1.1, m.2)) →
      ∀ {s₁ : σ₁} {s₂ : σ₂},
        mapAccumr₂ f₁ (xs.snoc x) (mapAccumr f₂ (ys.snoc y) s₂).2 s₁ =
          let m : (σ₁ × σ₂) × Vector ζ (n + 1) :=
            mapAccumr₂
              (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
                let r₂ := f₂ y s.2;
                let r₁ := f₁ x r₂.2 s.1;
                ((r₁.1, r₂.1), r₁.2))
              (xs.snoc x) (ys.snoc y) (s₁, s₂);
          (m.1.1, m.2)
⊢ mapAccumr₂ f₁ xs (mapAccumr f₂ ys s₂).2 s₁ =
    let m : (σ₁ × σ₂) × Vector ζ n :=
      mapAccumr₂
        (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
          let r₂ := f₂ y s.2;
          let r₁ := f₁ x r₂.2 s.1;
          ((r₁.1, r₂.1), r₁.2))
        xs ys (s₁, s₂);
    (m.1.1, m.2)

Tactic:
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ζ : Type u_4
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
f₁ : α → γ → σ₁ → σ₁ × ζ
f₂ : β → σ₂ → σ₂ × γ
s₁ : σ₁
s₂ : σ₂
⊢ mapAccumr₂ f₁ nil (mapAccumr f₂ nil s₂).2 s₁ =
    let m : (σ₁ × σ₂) × Vector ζ 0 :=
      mapAccumr₂
        (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
          let r₂ := f₂ y s.2;
          let r₁ := f₁ x r₂.2 s.1;
          ((r₁.1, r₂.1), r₁.2))
        nil nil (s₁, s₂);
    (m.1.1, m.2)

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ζ : Type u_4
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
f₁ : α → γ → σ₁ → σ₁ × ζ
f₂ : β → σ₂ → σ₂ × γ
n_1 : ℕ
xs : Vector α n_1
ys : Vector β n_1
x : α
y : β
h :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    mapAccumr₂ f₁ xs (mapAccumr f₂ ys s₂).2 s₁ =
      let m : (σ₁ × σ₂) × Vector ζ n_1 :=
        mapAccumr₂
          (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
            let r₂ := f₂ y s.2;
            let r₁ := f₁ x r₂.2 s.1;
            ((r₁.1, r₂.1), r₁.2))
          xs ys (s₁, s₂);
      (m.1.1, m.2)
s₁ : σ₁
s₂ : σ₂
⊢ mapAccumr₂ f₁ (xs.snoc x) (mapAccumr f₂ (ys.snoc y) s₂).2 s₁ =
    let m : (σ₁ × σ₂) × Vector ζ (n_1 + 1) :=
      mapAccumr₂
        (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
          let r₂ := f₂ y s.2;
          let r₁ := f₁ x r₂.2 s.1;
          ((r₁.1, r₂.1), r₁.2))
        (xs.snoc x) (ys.snoc y) (s₁, s₂);
    (m.1.1, m.2)

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ζ : Type u_4
n : ℕ
xs : Vector α n
ys : Vector β n
f₁ : α → γ → ζ
f₂ : β → γ
nil : map₂ f₁ Vector.nil (map f₂ Vector.nil) = map₂ (fun (x : α) (y : β) ↦ f₁ x (f₂ y)) Vector.nil Vector.nil
snoc :
  ∀ {n : ℕ} (xs : Vector α n) (ys : Vector β n) (x : α) (y : β),
    map₂ f₁ xs (map f₂ ys) = map₂ (fun (x : α) (y : β) ↦ f₁ x (f₂ y)) xs ys →
      map₂ f₁ (xs.snoc x) (map f₂ (ys.snoc y)) = map₂ (fun (x : α) (y : β) ↦ f₁ x (f₂ y)) (xs.snoc x) (ys.snoc y)
⊢ map₂ f₁ xs (map f₂ ys) = map₂ (fun (x : α) (y : β) ↦ f₁ x (f₂ y)) xs ys

Tactic:
induction xs, ys using Vector.revInductionOn₂
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ζ : Type u_4
n : ℕ
xs : Vector α n
ys : Vector β n
f₁ : α → γ → ζ
f₂ : β → γ
⊢ map₂ f₁ nil (map f₂ nil) = map₂ (fun (x : α) (y : β) ↦ f₁ x (f₂ y)) nil nil

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ζ : Type u_4
n : ℕ
xs : Vector α n
ys : Vector β n
f₁ : α → γ → ζ
f₂ : β → γ
n_1 : ℕ
xs_1 : Vector α n_1
ys_1 : Vector β n_1
x : α
y : β
h : map₂ f₁ xs_1 (map f₂ ys_1) = map₂ (fun (x : α) (y : β) ↦ f₁ x (f₂ y)) xs_1 ys_1
⊢ map₂ f₁ (xs_1.snoc x) (map f₂ (ys_1.snoc y)) = map₂ (fun (x : α) (y : β) ↦ f₁ x (f₂ y)) (xs_1.snoc x) (ys_1.snoc y)

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ζ : Type u_4
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
s₁ : σ₁
s₂ : σ₂
xs : Vector α n
ys : Vector β n
f₁ : γ → σ₁ → σ₁ × ζ
f₂ : α → β → σ₂ → σ₂ × γ
nil :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    mapAccumr f₁ (mapAccumr₂ f₂ Vector.nil Vector.nil s₂).2 s₁ =
      let m : (σ₁ × σ₂) × Vector ζ 0 :=
        mapAccumr₂
          (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
            let r₂ := f₂ x y s.2;
            let r₁ := f₁ r₂.2 s.1;
            ((r₁.1, r₂.1), r₁.2))
          Vector.nil Vector.nil (s₁, s₂);
      (m.1.1, m.2)
snoc :
  ∀ {n : ℕ} (xs : Vector α n) (ys : Vector β n) (x : α) (y : β),
    (∀ {s₁ : σ₁} {s₂ : σ₂},
        mapAccumr f₁ (mapAccumr₂ f₂ xs ys s₂).2 s₁ =
          let m : (σ₁ × σ₂) × Vector ζ n :=
            mapAccumr₂
              (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
                let r₂ := f₂ x y s.2;
                let r₁ := f₁ r₂.2 s.1;
                ((r₁.1, r₂.1), r₁.2))
              xs ys (s₁, s₂);
          (m.1.1, m.2)) →
      ∀ {s₁ : σ₁} {s₂ : σ₂},
        mapAccumr f₁ (mapAccumr₂ f₂ (xs.snoc x) (ys.snoc y) s₂).2 s₁ =
          let m : (σ₁ × σ₂) × Vector ζ (n + 1) :=
            mapAccumr₂
              (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
                let r₂ := f₂ x y s.2;
                let r₁ := f₁ r₂.2 s.1;
                ((r₁.1, r₂.1), r₁.2))
              (xs.snoc x) (ys.snoc y) (s₁, s₂);
          (m.1.1, m.2)
⊢ mapAccumr f₁ (mapAccumr₂ f₂ xs ys s₂).2 s₁ =
    let m : (σ₁ × σ₂) × Vector ζ n :=
      mapAccumr₂
        (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
          let r₂ := f₂ x y s.2;
          let r₁ := f₁ r₂.2 s.1;
          ((r₁.1, r₂.1), r₁.2))
        xs ys (s₁, s₂);
    (m.1.1, m.2)

Tactic:
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ζ : Type u_4
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
f₁ : γ → σ₁ → σ₁ × ζ
f₂ : α → β → σ₂ → σ₂ × γ
s₁ : σ₁
s₂ : σ₂
⊢ mapAccumr f₁ (mapAccumr₂ f₂ nil nil s₂).2 s₁ =
    let m : (σ₁ × σ₂) × Vector ζ 0 :=
      mapAccumr₂
        (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
          let r₂ := f₂ x y s.2;
          let r₁ := f₁ r₂.2 s.1;
          ((r₁.1, r₂.1), r₁.2))
        nil nil (s₁, s₂);
    (m.1.1, m.2)

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ζ : Type u_4
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
f₁ : γ → σ₁ → σ₁ × ζ
f₂ : α → β → σ₂ → σ₂ × γ
n_1 : ℕ
xs : Vector α n_1
ys : Vector β n_1
x : α
y : β
h :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    mapAccumr f₁ (mapAccumr₂ f₂ xs ys s₂).2 s₁ =
      let m : (σ₁ × σ₂) × Vector ζ n_1 :=
        mapAccumr₂
          (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
            let r₂ := f₂ x y s.2;
            let r₁ := f₁ r₂.2 s.1;
            ((r₁.1, r₂.1), r₁.2))
          xs ys (s₁, s₂);
      (m.1.1, m.2)
s₁ : σ₁
s₂ : σ₂
⊢ mapAccumr f₁ (mapAccumr₂ f₂ (xs.snoc x) (ys.snoc y) s₂).2 s₁ =
    let m : (σ₁ × σ₂) × Vector ζ (n_1 + 1) :=
      mapAccumr₂
        (fun (x : α) (y : β) (s : σ₁ × σ₂) ↦
          let r₂ := f₂ x y s.2;
          let r₁ := f₁ r₂.2 s.1;
          ((r₁.1, r₂.1), r₁.2))
        (xs.snoc x) (ys.snoc y) (s₁, s₂);
    (m.1.1, m.2)

Tactic:
simp_all