mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: case mp.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 : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
a : α₁
⊢ c ∈ sumLexLift f₁ f₂ g₁ g₂ (inl a) b →
    (∃ a₁ b₁ c₁, inl a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
      (∃ a₁ b₂ c₁, inl a = inl a₁ ∧ b = inr b₂ ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
        (∃ a₁ b₂ c₂, inl a = inl a₁ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
          ∃ a₂ b₂ c₂, inl a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂

pp: case mp.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 : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
a : α₂
⊢ c ∈ sumLexLift f₁ f₂ g₁ g₂ (inr a) b →
    (∃ a₁ b₁ c₁, inr a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
      (∃ a₁ b₂ c₁, inr a = inl a₁ ∧ b = inr b₂ ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
        (∃ a₁ b₂ c₂, inr a = inl a₁ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
          ∃ a₂ b₂ c₂, inr a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂

Tactic:
<;>

Goal state after:
case mp.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 : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
a : α₁
⊢ c ∈ sumLexLift f₁ f₂ g₁ g₂ (inl a) b →
    (∃ a₁ b₁ c₁, inl a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
      (∃ a₁ b₂ c₁, inl a = inl a₁ ∧ b = inr b₂ ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
        (∃ a₁ b₂ c₂, inl a = inl a₁ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
          ∃ a₂ b₂ c₂, inl a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂

case mp.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 : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
a : α₂
⊢ c ∈ sumLexLift f₁ f₂ g₁ g₂ (inr a) b →
    (∃ a₁ b₁ c₁, inr a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
      (∃ a₁ b₂ c₁, inr a = inl a₁ ∧ b = inr b₂ ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
        (∃ a₁ b₂ c₂, inr a = inl a₁ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
          ∃ a₂ b₂ c₂, inr a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂
Module: Mathlib.Data.Vector.Snoc

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
n : ℕ
x : α
xs : Vector α n
f : α → β
⊢ map f (nil.snoc x) = (map f nil).snoc (f x)

pp: case cons
α : Type u_1
β : Type u_2
n : ℕ
x : α
xs : Vector α n
f : α → β
n✝ : ℕ
x✝ : α
w✝ : Vector α n✝
a✝ : map f (w✝.snoc x) = (map f w✝).snoc (f x)
⊢ map f ((x✝ ::ᵥ w✝).snoc x) = (map f (x✝ ::ᵥ w✝)).snoc (f x)

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
β : Type u_2
n : ℕ
x : α
xs : Vector α n
f : α → β
⊢ map f (nil.snoc x) = (map f nil).snoc (f x)

case cons
α : Type u_1
β : Type u_2
n : ℕ
x : α
xs : Vector α n
f : α → β
n✝ : ℕ
x✝ : α
w✝ : Vector α n✝
a✝ : map f (w✝.snoc x) = (map f w✝).snoc (f x)
⊢ map f ((x✝ ::ᵥ w✝).snoc x) = (map f (x✝ ::ᵥ w✝)).snoc (f x)
Module: Mathlib.Data.Vector.Snoc

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
σ : Type u_3
n : ℕ
x : α
xs : Vector α n
ys : Vector β n
f : α → β → σ
y : β
⊢ map₂ f (nil.snoc x) (nil.snoc y) = (map₂ f nil nil).snoc (f x y)

pp: case cons
α : Type u_1
β : Type u_2
σ : Type u_3
n : ℕ
x : α
xs : Vector α n
ys : Vector β n
f : α → β → σ
y : β
n✝ : ℕ
a✝¹ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
a✝ : map₂ f (x✝.snoc x) (y✝.snoc y) = (map₂ f x✝ y✝).snoc (f x y)
⊢ map₂ f ((a✝¹ ::ᵥ x✝).snoc x) ((b✝ ::ᵥ y✝).snoc y) = (map₂ f (a✝¹ ::ᵥ x✝) (b✝ ::ᵥ y✝)).snoc (f x y)

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
β : Type u_2
σ : Type u_3
n : ℕ
x : α
xs : Vector α n
ys : Vector β n
f : α → β → σ
y : β
⊢ map₂ f (nil.snoc x) (nil.snoc y) = (map₂ f nil nil).snoc (f x y)

case cons
α : Type u_1
β : Type u_2
σ : Type u_3
n : ℕ
x : α
xs : Vector α n
ys : Vector β n
f : α → β → σ
y : β
n✝ : ℕ
a✝¹ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
a✝ : map₂ f (x✝.snoc x) (y✝.snoc y) = (map₂ f x✝ y✝).snoc (f x y)
⊢ map₂ f ((a✝¹ ::ᵥ x✝).snoc x) ((b✝ ::ᵥ y✝).snoc y) = (map₂ f (a✝¹ ::ᵥ x✝) (b✝ ::ᵥ y✝)).snoc (f x y)
Module: Mathlib.Data.Vector.Snoc

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × φ
x : α
y : β
⊢ mapAccumr₂ f (nil.snoc x) (nil.snoc y) s =
    let q := f x y s;
    let r := mapAccumr₂ f nil nil q.1;
    (r.1, r.2.snoc q.2)

pp: case cons
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × φ
x : α
y : β
n✝ : ℕ
a✝¹ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
a✝ :
  mapAccumr₂ f (x✝.snoc x) (y✝.snoc y) s =
    let q := f x y s;
    let r := mapAccumr₂ f x✝ y✝ q.1;
    (r.1, r.2.snoc q.2)
⊢ mapAccumr₂ f ((a✝¹ ::ᵥ x✝).snoc x) ((b✝ ::ᵥ y✝).snoc y) s =
    let q := f x y s;
    let r := mapAccumr₂ f (a✝¹ ::ᵥ x✝) (b✝ ::ᵥ y✝) q.1;
    (r.1, r.2.snoc q.2)

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × φ
x : α
y : β
⊢ mapAccumr₂ f (nil.snoc x) (nil.snoc y) s =
    let q := f x y s;
    let r := mapAccumr₂ f nil nil q.1;
    (r.1, r.2.snoc q.2)

case cons
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × φ
x : α
y : β
n✝ : ℕ
a✝¹ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
a✝ :
  mapAccumr₂ f (x✝.snoc x) (y✝.snoc y) s =
    let q := f x y s;
    let r := mapAccumr₂ f x✝ y✝ q.1;
    (r.1, r.2.snoc q.2)
⊢ mapAccumr₂ f ((a✝¹ ::ᵥ x✝).snoc x) ((b✝ ::ᵥ y✝).snoc y) s =
    let q := f x y s;
    let r := mapAccumr₂ f (a✝¹ ::ᵥ x✝) (b✝ ::ᵥ y✝) q.1;
    (r.1, r.2.snoc q.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
n : ℕ
f₁ : β → σ₁ → σ₁ × γ
f₂ : α → σ₂ → σ₂ × β
s₁ : σ₁
s₂ : σ₂
⊢ mapAccumr f₁ (mapAccumr f₂ nil s₂).2 s₁ =
    let m :=
      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)

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

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

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

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

pp: case snoc
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
n : ℕ
xs : Vector α n
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₂ (xs✝.snoc x✝)) s = mapAccumr (fun x s ↦ f₁ (f₂ x) s) (xs✝.snoc x✝) s

Tactic:
<;>

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

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

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

pp: case snoc
α : Type u_1
β : Type u_2
γ : Type u_3
σ₂ : Type u_7
n : ℕ
xs : Vector α n
f₂ : α → σ₂ → σ₂ × β
f₁ : β → γ
n✝ : ℕ
xs✝ : Vector α n✝
x✝ : α
a✝ :
  ∀ {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

Tactic:
<;>

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

case snoc
α : Type u_1
β : Type u_2
γ : Type u_3
σ₂ : Type u_7
n : ℕ
xs : Vector α n
f₂ : α → σ₂ → σ₂ × β
f₁ : β → γ
n✝ : ℕ
xs✝ : Vector α n✝
x✝ : α
a✝ :
  ∀ {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
Module: Mathlib.Data.Vector.MapLemmas

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

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

Tactic:
<;>

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

case cons
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
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✝)
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
p : α → Prop
f₁ : β → γ
f₂ : (a : α) → p a → β
H : ∀ (x : α), x ∈ nil.toList → p x
⊢ map f₁ (pmap f₂ nil H) = pmap (fun x hx ↦ f₁ (f₂ x hx)) nil H

pp: case cons
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
p : α → Prop
f₁ : β → γ
f₂ : (a : α) → p a → β
n✝ : ℕ
x✝ : α
w✝ : Vector α n✝
a✝ : ∀ (H : ∀ (x : α), x ∈ w✝.toList → p x), map f₁ (pmap f₂ w✝ H) = pmap (fun x hx ↦ f₁ (f₂ x hx)) w✝ H
H : ∀ (x : α), x ∈ (x✝ ::ᵥ w✝).toList → p x
⊢ map f₁ (pmap f₂ (x✝ ::ᵥ w✝) H) = pmap (fun x hx ↦ f₁ (f₂ x hx)) (x✝ ::ᵥ w✝) H

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
p : α → Prop
f₁ : β → γ
f₂ : (a : α) → p a → β
H : ∀ (x : α), x ∈ nil.toList → p x
⊢ map f₁ (pmap f₂ nil H) = pmap (fun x hx ↦ f₁ (f₂ x hx)) nil H

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

Goal state before:
pp: case nil
α : 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 f₁ (map f₂ nil) H = pmap (fun x hx ↦ f₁ (f₂ x) hx) nil ⋯

pp: case cons
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
p : β → Prop
f₁ : (b : β) → p b → γ
f₂ : α → β
n✝ : ℕ
x✝ : α
w✝ : Vector α n✝
a✝ : ∀ (H : ∀ (x : β), x ∈ (map f₂ w✝).toList → p x), pmap f₁ (map f₂ w✝) H = pmap (fun x hx ↦ f₁ (f₂ x) hx) w✝ ⋯
H : ∀ (x : β), x ∈ (map f₂ (x✝ ::ᵥ w✝)).toList → p x
⊢ pmap f₁ (map f₂ (x✝ ::ᵥ w✝)) H = pmap (fun x hx ↦ f₁ (f₂ x) hx) (x✝ ::ᵥ w✝) ⋯

Tactic:
<;>

Goal state after:
case nil
α : 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 f₁ (map f₂ nil) H = pmap (fun x hx ↦ f₁ (f₂ x) hx) nil ⋯

case cons
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
p : β → Prop
f₁ : (b : β) → p b → γ
f₂ : α → β
n✝ : ℕ
x✝ : α
w✝ : Vector α n✝
a✝ : ∀ (H : ∀ (x : β), x ∈ (map f₂ w✝).toList → p x), pmap f₁ (map f₂ w✝) H = pmap (fun x hx ↦ f₁ (f₂ x) hx) w✝ ⋯
H : ∀ (x : β), x ∈ (map f₂ (x✝ ::ᵥ w✝)).toList → p x
⊢ pmap f₁ (map f₂ (x✝ ::ᵥ w✝)) H = pmap (fun x hx ↦ f₁ (f₂ x) hx) (x✝ ::ᵥ w✝) ⋯
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: case inl
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ f₁' : α₁ → β₁ → Finset γ₁
f₂ f₂' : α₂ → β₂ → Finset γ₂
g₁ g₁' : α₁ → β₂ → Finset γ₁
g₂ g₂' : α₁ → β₂ → Finset γ₂
hf₁ : ∀ (a : α₁) (b : β₁), f₁ a b ⊆ f₁' a b
hf₂ : ∀ (a : α₂) (b : β₂), f₂ a b ⊆ f₂' a b
hg₁ : ∀ (a : α₁) (b : β₂), g₁ a b ⊆ g₁' a b
hg₂ : ∀ (a : α₁) (b : β₂), g₂ a b ⊆ g₂' a b
b : β₁ ⊕ β₂
val✝ : α₁
⊢ sumLexLift f₁ f₂ g₁ g₂ (inl val✝) b ⊆ sumLexLift f₁' f₂' g₁' g₂' (inl val✝) b

pp: case inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ f₁' : α₁ → β₁ → Finset γ₁
f₂ f₂' : α₂ → β₂ → Finset γ₂
g₁ g₁' : α₁ → β₂ → Finset γ₁
g₂ g₂' : α₁ → β₂ → Finset γ₂
hf₁ : ∀ (a : α₁) (b : β₁), f₁ a b ⊆ f₁' a b
hf₂ : ∀ (a : α₂) (b : β₂), f₂ a b ⊆ f₂' a b
hg₁ : ∀ (a : α₁) (b : β₂), g₁ a b ⊆ g₁' a b
hg₂ : ∀ (a : α₁) (b : β₂), g₂ a b ⊆ g₂' a b
b : β₁ ⊕ β₂
val✝ : α₂
⊢ sumLexLift f₁ f₂ g₁ g₂ (inr val✝) b ⊆ sumLexLift f₁' f₂' g₁' g₂' (inr val✝) b

Tactic:
<;>

Goal state after:
case inl
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ f₁' : α₁ → β₁ → Finset γ₁
f₂ f₂' : α₂ → β₂ → Finset γ₂
g₁ g₁' : α₁ → β₂ → Finset γ₁
g₂ g₂' : α₁ → β₂ → Finset γ₂
hf₁ : ∀ (a : α₁) (b : β₁), f₁ a b ⊆ f₁' a b
hf₂ : ∀ (a : α₂) (b : β₂), f₂ a b ⊆ f₂' a b
hg₁ : ∀ (a : α₁) (b : β₂), g₁ a b ⊆ g₁' a b
hg₂ : ∀ (a : α₁) (b : β₂), g₂ a b ⊆ g₂' a b
b : β₁ ⊕ β₂
val✝ : α₁
⊢ sumLexLift f₁ f₂ g₁ g₂ (inl val✝) b ⊆ sumLexLift f₁' f₂' g₁' g₂' (inl val✝) b

case inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ f₁' : α₁ → β₁ → Finset γ₁
f₂ f₂' : α₂ → β₂ → Finset γ₂
g₁ g₁' : α₁ → β₂ → Finset γ₁
g₂ g₂' : α₁ → β₂ → Finset γ₂
hf₁ : ∀ (a : α₁) (b : β₁), f₁ a b ⊆ f₁' a b
hf₂ : ∀ (a : α₂) (b : β₂), f₂ a b ⊆ f₂' a b
hg₁ : ∀ (a : α₁) (b : β₂), g₁ a b ⊆ g₁' a b
hg₂ : ∀ (a : α₁) (b : β₂), g₂ a b ⊆ g₂' a b
b : β₁ ⊕ β₂
val✝ : α₂
⊢ sumLexLift f₁ f₂ g₁ g₂ (inr val✝) b ⊆ sumLexLift f₁' f₂' g₁' g₂' (inr val✝) b
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 s₂).2 nil s₁ =
    let m :=
      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)

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✝ s₂).2 ys✝ s₁ =
      let m :=
        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 :=
      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:
<;>

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 s₂).2 nil s₁ =
    let m :=
      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)

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✝ s₂).2 ys✝ s₁ =
      let m :=
        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 :=
      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)
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_4
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
f₁ : α → γ → σ₁ → σ₁ × ζ
f₂ : β → σ₂ → σ₂ × γ
s₁ : σ₁
s₂ : σ₂
⊢ mapAccumr₂ f₁ nil (mapAccumr f₂ nil s₂).2 s₁ =
    let m :=
      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)

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₁ xs✝ (mapAccumr f₂ ys✝ s₂).2 s₁ =
      let m :=
        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 :=
      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:
<;>

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₁ nil (mapAccumr f₂ nil s₂).2 s₁ =
    let m :=
      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)

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₁ xs✝ (mapAccumr f₂ ys✝ s₂).2 s₁ =
      let m :=
        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 :=
      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)
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₁ nil (map f₂ nil) = map₂ (fun x y ↦ f₁ x (f₂ 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₁ 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✝)

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₁ nil (map f₂ nil) = map₂ (fun x y ↦ f₁ x (f₂ 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₁ 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✝)