mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: case nil
α : 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 :=
      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)

pp: case snoc
α : Type u_1
β : Type u_2
γ : Type u_3
ζ : Type u_4
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
f₁ : γ → σ₁ → σ₁ × ζ
f₂ : α → β → σ₂ → σ₂ × γ
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    mapAccumr f₁ (mapAccumr₂ f₂ xs✝ ys✝ s₂).2 s₁ =
      let m :=
        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 :=
      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:
<;>

Goal state after:
case nil
α : 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 :=
      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)

case snoc
α : Type u_1
β : Type u_2
γ : Type u_3
ζ : Type u_4
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
f₁ : γ → σ₁ → σ₁ × ζ
f₂ : α → β → σ₂ → σ₂ × γ
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    mapAccumr f₁ (mapAccumr₂ f₂ xs✝ ys✝ s₂).2 s₁ =
      let m :=
        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 :=
      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)
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: case nil
α : 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

pp: case snoc
α : Type u_1
β : Type u_2
γ : Type u_3
ζ : Type u_4
n : ℕ
xs : Vector α n
ys : Vector β n
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₂ (xs✝.snoc x✝) (ys✝.snoc y✝)) = map₂ (fun x y ↦ f₁ (f₂ x y)) (xs✝.snoc x✝) (ys✝.snoc y✝)

Tactic:
<;>

Goal state after:
case nil
α : 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

case snoc
α : Type u_1
β : Type u_2
γ : Type u_3
ζ : Type u_4
n : ℕ
xs : Vector α n
ys : Vector β n
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₂ (xs✝.snoc x✝) (ys✝.snoc y✝)) = map₂ (fun x y ↦ f₁ (f₂ x y)) (xs✝.snoc x✝) (ys✝.snoc y✝)
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
f₁ : γ → α → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
s₁ : σ₁
s₂ : σ₂
⊢ mapAccumr₂ f₁ (mapAccumr₂ f₂ nil nil s₂).2 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₂.2 x s₁;
            ((r₁.1, r₂.1), r₁.2))
        nil nil (s₁, s₂);
    (m.1.1, m.2)

pp: case snoc
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
f₁ : γ → α → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    mapAccumr₂ f₁ (mapAccumr₂ f₂ xs✝ ys✝ s₂).2 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₂.2 x s₁;
              ((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 (xs✝.snoc 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₂.2 x s₁;
            ((r₁.1, r₂.1), r₁.2))
        (xs✝.snoc x✝) (ys✝.snoc y✝) (s₁, s₂);
    (m.1.1, m.2)

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
f₁ : γ → α → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
s₁ : σ₁
s₂ : σ₂
⊢ mapAccumr₂ f₁ (mapAccumr₂ f₂ nil nil s₂).2 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₂.2 x s₁;
            ((r₁.1, r₂.1), r₁.2))
        nil nil (s₁, s₂);
    (m.1.1, m.2)

case snoc
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
f₁ : γ → α → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    mapAccumr₂ f₁ (mapAccumr₂ f₂ xs✝ ys✝ s₂).2 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₂.2 x s₁;
              ((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 (xs✝.snoc 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₂.2 x s₁;
            ((r₁.1, r₂.1), r₁.2))
        (xs✝.snoc x✝) (ys✝.snoc y✝) (s₁, s₂);
    (m.1.1, m.2)
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
f₁ : γ → β → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
s₁ : σ₁
s₂ : σ₂
⊢ mapAccumr₂ f₁ (mapAccumr₂ f₂ nil nil s₂).2 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₂.2 y s₁;
            ((r₁.1, r₂.1), r₁.2))
        nil nil (s₁, s₂);
    (m.1.1, m.2)

pp: case snoc
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
f₁ : γ → β → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    mapAccumr₂ f₁ (mapAccumr₂ f₂ xs✝ ys✝ s₂).2 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₂.2 y s₁;
              ((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 (ys✝.snoc 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₂.2 y s₁;
            ((r₁.1, r₂.1), r₁.2))
        (xs✝.snoc x✝) (ys✝.snoc y✝) (s₁, s₂);
    (m.1.1, m.2)

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
f₁ : γ → β → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
s₁ : σ₁
s₂ : σ₂
⊢ mapAccumr₂ f₁ (mapAccumr₂ f₂ nil nil s₂).2 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₂.2 y s₁;
            ((r₁.1, r₂.1), r₁.2))
        nil nil (s₁, s₂);
    (m.1.1, m.2)

case snoc
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
f₁ : γ → β → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    mapAccumr₂ f₁ (mapAccumr₂ f₂ xs✝ ys✝ s₂).2 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₂.2 y s₁;
              ((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 (ys✝.snoc 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₂.2 y s₁;
            ((r₁.1, r₂.1), r₁.2))
        (xs✝.snoc x✝) (ys✝.snoc y✝) (s₁, s₂);
    (m.1.1, m.2)
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
f₁ : α → γ → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
s₁ : σ₁
s₂ : σ₂
⊢ mapAccumr₂ f₁ nil (mapAccumr₂ f₂ nil nil s₂).2 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₂.2 s₁;
            ((r₁.1, r₂.1), r₁.2))
        nil nil (s₁, s₂);
    (m.1.1, m.2)

pp: case snoc
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
f₁ : α → γ → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    mapAccumr₂ f₁ xs✝ (mapAccumr₂ f₂ xs✝ ys✝ s₂).2 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₂.2 s₁;
              ((r₁.1, r₂.1), r₁.2))
          xs✝ ys✝ (s₁, s₂);
      (m.1.1, m.2)
s₁ : σ₁
s₂ : σ₂
⊢ mapAccumr₂ f₁ (xs✝.snoc x✝) (mapAccumr₂ f₂ (xs✝.snoc x✝) (ys✝.snoc y✝) s₂).2 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₂.2 s₁;
            ((r₁.1, r₂.1), r₁.2))
        (xs✝.snoc x✝) (ys✝.snoc y✝) (s₁, s₂);
    (m.1.1, m.2)

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
f₁ : α → γ → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
s₁ : σ₁
s₂ : σ₂
⊢ mapAccumr₂ f₁ nil (mapAccumr₂ f₂ nil nil s₂).2 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₂.2 s₁;
            ((r₁.1, r₂.1), r₁.2))
        nil nil (s₁, s₂);
    (m.1.1, m.2)

case snoc
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
f₁ : α → γ → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    mapAccumr₂ f₁ xs✝ (mapAccumr₂ f₂ xs✝ ys✝ s₂).2 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₂.2 s₁;
              ((r₁.1, r₂.1), r₁.2))
          xs✝ ys✝ (s₁, s₂);
      (m.1.1, m.2)
s₁ : σ₁
s₂ : σ₂
⊢ mapAccumr₂ f₁ (xs✝.snoc x✝) (mapAccumr₂ f₂ (xs✝.snoc x✝) (ys✝.snoc y✝) s₂).2 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₂.2 s₁;
            ((r₁.1, r₂.1), r₁.2))
        (xs✝.snoc x✝) (ys✝.snoc y✝) (s₁, s₂);
    (m.1.1, m.2)
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
f₁ : β → γ → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
s₁ : σ₁
s₂ : σ₂
⊢ mapAccumr₂ f₁ nil (mapAccumr₂ f₂ nil nil s₂).2 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₂.2 s₁;
            ((r₁.1, r₂.1), r₁.2))
        nil nil (s₁, s₂);
    (m.1.1, m.2)

pp: case snoc
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
f₁ : β → γ → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    mapAccumr₂ f₁ ys✝ (mapAccumr₂ f₂ xs✝ ys✝ s₂).2 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₂.2 s₁;
              ((r₁.1, r₂.1), r₁.2))
          xs✝ ys✝ (s₁, s₂);
      (m.1.1, m.2)
s₁ : σ₁
s₂ : σ₂
⊢ mapAccumr₂ f₁ (ys✝.snoc y✝) (mapAccumr₂ f₂ (xs✝.snoc x✝) (ys✝.snoc y✝) s₂).2 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₂.2 s₁;
            ((r₁.1, r₂.1), r₁.2))
        (xs✝.snoc x✝) (ys✝.snoc y✝) (s₁, s₂);
    (m.1.1, m.2)

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
f₁ : β → γ → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
s₁ : σ₁
s₂ : σ₂
⊢ mapAccumr₂ f₁ nil (mapAccumr₂ f₂ nil nil s₂).2 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₂.2 s₁;
            ((r₁.1, r₂.1), r₁.2))
        nil nil (s₁, s₂);
    (m.1.1, m.2)

case snoc
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
f₁ : β → γ → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    mapAccumr₂ f₁ ys✝ (mapAccumr₂ f₂ xs✝ ys✝ s₂).2 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₂.2 s₁;
              ((r₁.1, r₂.1), r₁.2))
          xs✝ ys✝ (s₁, s₂);
      (m.1.1, m.2)
s₁ : σ₁
s₂ : σ₂
⊢ mapAccumr₂ f₁ (ys✝.snoc y✝) (mapAccumr₂ f₂ (xs✝.snoc x✝) (ys✝.snoc y✝) s₂).2 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₂.2 s₁;
            ((r₁.1, r₂.1), r₁.2))
        (xs✝.snoc x✝) (ys✝.snoc y✝) (s₁, s₂);
    (m.1.1, m.2)
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
n : ℕ
xs : Vector α n
f : α → β
⊢ map f nil = (mapAccumr (fun x x_1 ↦ ((), f x)) nil ()).2

pp: case snoc
α : Type u_1
β : Type u_2
n : ℕ
xs : Vector α n
f : α → β
n✝ : ℕ
xs✝ : Vector α n✝
x✝ : α
a✝ : map f xs✝ = (mapAccumr (fun x x_1 ↦ ((), f x)) xs✝ ()).2
⊢ map f (xs✝.snoc x✝) = (mapAccumr (fun x x_1 ↦ ((), f x)) (xs✝.snoc x✝) ()).2

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
β : Type u_2
n : ℕ
xs : Vector α n
f : α → β
⊢ map f nil = (mapAccumr (fun x x_1 ↦ ((), f x)) nil ()).2

case snoc
α : Type u_1
β : Type u_2
n : ℕ
xs : Vector α n
f : α → β
n✝ : ℕ
xs✝ : Vector α n✝
x✝ : α
a✝ : map f xs✝ = (mapAccumr (fun x x_1 ↦ ((), f x)) xs✝ ()).2
⊢ map f (xs✝.snoc x✝) = (mapAccumr (fun x x_1 ↦ ((), f x)) (xs✝.snoc x✝) ()).2
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → γ
⊢ map₂ f nil nil = (mapAccumr₂ (fun x y x_1 ↦ ((), f x y)) nil nil ()).2

pp: case snoc
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
ys : Vector β n
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✝ ()).2
⊢ map₂ f (xs✝.snoc x✝) (ys✝.snoc y✝) = (mapAccumr₂ (fun x y x_1 ↦ ((), f x y)) (xs✝.snoc x✝) (ys✝.snoc y✝) ()).2

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → γ
⊢ map₂ f nil nil = (mapAccumr₂ (fun x y x_1 ↦ ((), f x y)) nil nil ()).2

case snoc
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
ys : Vector β n
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✝ ()).2
⊢ map₂ f (xs✝.snoc x✝) (ys✝.snoc y✝) = (mapAccumr₂ (fun x y x_1 ↦ ((), f x y)) (xs✝.snoc x✝) (ys✝.snoc y✝) ()).2
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
s : σ
h : ∀ (a : α), (f a s).1 = s
⊢ mapAccumr f nil s = (s, map (fun x ↦ (f x s).2) nil)

pp: case snoc
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
s : σ
h : ∀ (a : α), (f a s).1 = s
n✝ : ℕ
xs✝ : Vector α n✝
x✝ : α
a✝ : mapAccumr f xs✝ s = (s, map (fun x ↦ (f x s).2) xs✝)
⊢ mapAccumr f (xs✝.snoc x✝) s = (s, map (fun x ↦ (f x s).2) (xs✝.snoc x✝))

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
s : σ
h : ∀ (a : α), (f a s).1 = s
⊢ mapAccumr f nil s = (s, map (fun x ↦ (f x s).2) nil)

case snoc
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
s : σ
h : ∀ (a : α), (f a s).1 = s
n✝ : ℕ
xs✝ : Vector α n✝
x✝ : α
a✝ : mapAccumr f xs✝ s = (s, map (fun x ↦ (f x s).2) xs✝)
⊢ mapAccumr f (xs✝.snoc x✝) s = (s, map (fun x ↦ (f x s).2) (xs✝.snoc x✝))
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
s : σ
h : ∀ (a : α) (b : β), (f a b s).1 = s
⊢ mapAccumr₂ f nil nil s = (s, map₂ (fun x y ↦ (f x y s).2) nil nil)

pp: case snoc
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
s : σ
h : ∀ (a : α) (b : β), (f a b s).1 = 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).2) xs✝ ys✝)
⊢ mapAccumr₂ f (xs✝.snoc x✝) (ys✝.snoc y✝) s = (s, map₂ (fun x y ↦ (f x y s).2) (xs✝.snoc x✝) (ys✝.snoc y✝))

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
s : σ
h : ∀ (a : α) (b : β), (f a b s).1 = s
⊢ mapAccumr₂ f nil nil s = (s, map₂ (fun x y ↦ (f x y s).2) nil nil)

case snoc
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
s : σ
h : ∀ (a : α) (b : β), (f a b s).1 = 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).2) xs✝ ys✝)
⊢ mapAccumr₂ f (xs✝.snoc x✝) (ys✝.snoc y✝) s = (s, map₂ (fun x y ↦ (f x y s).2) (xs✝.snoc x✝) (ys✝.snoc y✝))
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: case refine_4.inl
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
b : β₁ ⊕ β₂
val✝ : α₁
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inl val✝ = inl a₁ → b = inl b₁ → f₁ a₁ b₁ = ∅) ∧
    (∀ (a₁ : α₁) (b₂ : β₂), inl val✝ = inl a₁ → b = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
      ∀ (a₂ : α₂) (b₂ : β₂), inl val✝ = inr a₂ → b = inr b₂ → f₂ a₂ b₂ = ∅
⊢ sumLexLift f₁ f₂ g₁ g₂ (inl val✝) b = ∅

pp: case refine_4.inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
b : β₁ ⊕ β₂
val✝ : α₂
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inr val✝ = inl a₁ → b = inl b₁ → f₁ a₁ b₁ = ∅) ∧
    (∀ (a₁ : α₁) (b₂ : β₂), inr val✝ = inl a₁ → b = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
      ∀ (a₂ : α₂) (b₂ : β₂), inr val✝ = inr a₂ → b = inr b₂ → f₂ a₂ b₂ = ∅
⊢ sumLexLift f₁ f₂ g₁ g₂ (inr val✝) b = ∅

Tactic:
<;>

Goal state after:
case refine_4.inl
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
b : β₁ ⊕ β₂
val✝ : α₁
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inl val✝ = inl a₁ → b = inl b₁ → f₁ a₁ b₁ = ∅) ∧
    (∀ (a₁ : α₁) (b₂ : β₂), inl val✝ = inl a₁ → b = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
      ∀ (a₂ : α₂) (b₂ : β₂), inl val✝ = inr a₂ → b = inr b₂ → f₂ a₂ b₂ = ∅
⊢ sumLexLift f₁ f₂ g₁ g₂ (inl val✝) b = ∅

case refine_4.inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
b : β₁ ⊕ β₂
val✝ : α₂
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inr val✝ = inl a₁ → b = inl b₁ → f₁ a₁ b₁ = ∅) ∧
    (∀ (a₁ : α₁) (b₂ : β₂), inr val✝ = inl a₁ → b = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
      ∀ (a₂ : α₂) (b₂ : β₂), inr val✝ = inr a₂ → b = inr b₂ → f₂ a₂ b₂ = ∅
⊢ sumLexLift f₁ f₂ g₁ g₂ (inr val✝) b = ∅
Module: Mathlib.Data.Vector3

Goal state before:
pp: case refine_1
α : Type u_1
n : ℕ
a : α
v : Vector3 α n
j : Fin2 (n + 1)
⊢ insert a v fz fz = (a :: v) fz

pp: case refine_2
α : Type u_1
n : ℕ
a : α
v : Vector3 α n
j : Fin2 (n + 1)
⊢ ∀ (n_1 : Fin2 n), insert a v fz n_1.fs = (a :: v) n_1.fs

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
n : ℕ
a : α
v : Vector3 α n
j : Fin2 (n + 1)
⊢ insert a v fz fz = (a :: v) fz

case refine_2
α : Type u_1
n : ℕ
a : α
v : Vector3 α n
j : Fin2 (n + 1)
⊢ ∀ (n_1 : Fin2 n), insert a v fz n_1.fs = (a :: v) n_1.fs
Module: Mathlib.Data.Vector3

Goal state before:
pp: case refine_1
α : Type u_1
n : ℕ
a : α
v : Vector3 α n
j : Fin2 (n + 1)
⊢ insert a v fz fz = (a :: v) fz

pp: case refine_2
α : Type u_1
n : ℕ
a : α
v : Vector3 α n
j : Fin2 (n + 1)
n✝ : Fin2 n
⊢ insert a v fz n✝.fs = (a :: v) n✝.fs

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
n : ℕ
a : α
v : Vector3 α n
j : Fin2 (n + 1)
⊢ insert a v fz fz = (a :: v) fz

case refine_2
α : Type u_1
n : ℕ
a : α
v : Vector3 α n
j : Fin2 (n + 1)
n✝ : Fin2 n
⊢ insert a v fz n✝.fs = (a :: v) n✝.fs
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
n : ℕ
xs ys : Vector α n
f : α → α → β
comm : ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁
⊢ map₂ f nil nil = map₂ f nil nil

pp: case cons
α : Type u_1
β : Type u_2
n : ℕ
xs ys : Vector α n
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✝)

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
β : Type u_2
n : ℕ
xs ys : Vector α n
f : α → α → β
comm : ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁
⊢ map₂ f nil nil = map₂ f nil nil

case cons
α : Type u_1
β : Type u_2
n : ℕ
xs ys : Vector α n
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✝)