mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case inl
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x✝ : β
i : Cofix F α
R : Cofix F α → Cofix F α → Prop :=
  fun a b ↦
    ∃ x,
      a =
          corec
            (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
              Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
            (Sum.inl x) ∧
        b = x
a b x : Cofix F α
Ha :
  a =
    corec
      (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
        Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
      (Sum.inl x)
Hb : b = x
⊢ LiftR' (α.RelLast' R)
    ((TypeVec.id :::
        ((corec fun x ↦
              (TypeVec.id ::: fun x ↦ x) <$$>
                Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) (fun val ↦ g val) x) ∘
            fun x ↦ x) ∘
          Sum.inl) <$$>
      x.dest)
    x.dest

Tactic:
rw [MvFunctor.map_map, ← appendFun_comp_id]

Goal state after:
case inl
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x✝ : β
i : Cofix F α
R : Cofix F α → Cofix F α → Prop :=
  fun a b ↦
    ∃ x,
      a =
          corec
            (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
              Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
            (Sum.inl x) ∧
        b = x
a b x : Cofix F α
Ha :
  a =
    corec
      (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
        Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
      (Sum.inl x)
Hb : b = x
⊢ LiftR' (α.RelLast' R)
    ((TypeVec.id :::
        ((corec fun x ↦
              (TypeVec.id ::: fun x ↦ x) <$$>
                Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) (fun val ↦ g val) x) ∘
            fun x ↦ x) ∘
          Sum.inl) <$$>
      x.dest)
    x.dest
Module: Mathlib.Data.Set.Enumerate

Goal state before:
pp: case zero.succ
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
h₁ : enumerate sel s 0 = some a
m : ℕ
h₂ : enumerate sel s (0 + (m + 1)) = some a
h' : enumerate sel (s \ {a}) m = some a
this : a ∈ s \ {a}
⊢ 0 = 0 + (m + 1)

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) s.think.destruct t.destruct ↔ LiftRel R s t

Tactic:
liftRel_destruct_iff

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) s.think.destruct t.destruct ↔
    Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.think.destruct ↔ LiftRel R s t

Tactic:
liftRel_destruct_iff

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.think.destruct ↔
    Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h1.nil
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
m : nil.destruct = Computation.pure (some (a', s'))
⊢ a ∈ nil ↔ a = a' ∨ a ∈ s'

Tactic:
have := congr_arg Computation.destruct m

Goal state after:
case h1.nil
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
m : nil.destruct = Computation.pure (some (a', s'))
this : nil.destruct.destruct = (Computation.pure (some (a', s'))).destruct
⊢ a ∈ nil ↔ a = a' ∨ a ∈ s'
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h1.cons
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x✝ : α
s✝ : WSeq α
m : (cons x✝ s✝).destruct = Computation.pure (some (a', s'))
⊢ a ∈ cons x✝ s✝ ↔ a = a' ∨ a ∈ s'

Tactic:
have := congr_arg Computation.destruct m

Goal state after:
case h1.cons
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x✝ : α
s✝ : WSeq α
m : (cons x✝ s✝).destruct = Computation.pure (some (a', s'))
this : (cons x✝ s✝).destruct.destruct = (Computation.pure (some (a', s'))).destruct
⊢ a ∈ cons x✝ s✝ ↔ a = a' ∨ a ∈ s'
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h1.think
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
s✝ : WSeq α
m : s✝.think.destruct = Computation.pure (some (a', s'))
⊢ a ∈ s✝.think ↔ a = a' ∨ a ∈ s'

Tactic:
have := congr_arg Computation.destruct m

Goal state after:
case h1.think
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
s✝ : WSeq α
m : s✝.think.destruct = Computation.pure (some (a', s'))
this : s✝.think.destruct.destruct = (Computation.pure (some (a', s'))).destruct
⊢ a ∈ s✝.think ↔ a = a' ∨ a ∈ s'
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h2.nil
α : Type u
a a' : α
s' : WSeq α
c✝ : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c✝
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α}, s.destruct = c → (a ∈ s ↔ a = a' ∨ a ∈ s')
m : nil.destruct = c.think
⊢ a ∈ nil ↔ a = a' ∨ a ∈ s'

Tactic:
have := congr_arg Computation.destruct m

Goal state after:
case h2.nil
α : Type u
a a' : α
s' : WSeq α
c✝ : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c✝
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α}, s.destruct = c → (a ∈ s ↔ a = a' ∨ a ∈ s')
m : nil.destruct = c.think
this : nil.destruct.destruct = c.think.destruct
⊢ a ∈ nil ↔ a = a' ∨ a ∈ s'
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h2.cons
α : Type u
a a' : α
s' : WSeq α
c✝ : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c✝
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α}, s.destruct = c → (a ∈ s ↔ a = a' ∨ a ∈ s')
x✝ : α
s✝ : WSeq α
m : (cons x✝ s✝).destruct = c.think
⊢ a ∈ cons x✝ s✝ ↔ a = a' ∨ a ∈ s'

Tactic:
have := congr_arg Computation.destruct m

Goal state after:
case h2.cons
α : Type u
a a' : α
s' : WSeq α
c✝ : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c✝
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α}, s.destruct = c → (a ∈ s ↔ a = a' ∨ a ∈ s')
x✝ : α
s✝ : WSeq α
m : (cons x✝ s✝).destruct = c.think
this : (cons x✝ s✝).destruct.destruct = c.think.destruct
⊢ a ∈ cons x✝ s✝ ↔ a = a' ∨ a ∈ s'
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h2.think
α : Type u
a a' : α
s' : WSeq α
c✝ : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c✝
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α}, s.destruct = c → (a ∈ s ↔ a = a' ∨ a ∈ s')
s✝ : WSeq α
m : s✝.think.destruct = c.think
⊢ a ∈ s✝.think ↔ a = a' ∨ a ∈ s'

Tactic:
have := congr_arg Computation.destruct m

Goal state after:
case h2.think
α : Type u
a a' : α
s' : WSeq α
c✝ : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c✝
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α}, s.destruct = c → (a ∈ s ↔ a = a' ∨ a ∈ s')
s✝ : WSeq α
m : s✝.think.destruct = c.think
this : s✝.think.destruct.destruct = c.think.destruct
⊢ a ∈ s✝.think ↔ a = a' ∨ a ∈ s'
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case some
α : Type u
β : Type v
f : α → β
b : β
g : Stream' (Option (Option α))
al : g.IsSeq
h : b ∈ map f ⟨g, al⟩
a : α
om : some a ∈ ⟨g, al⟩
h' : f a = b
⊢ ∃ a ∈ ⟨g, al⟩, f a = b

Tactic:
exact ⟨a, om, h'⟩

Goal state after:
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case h1.inl
α : Type u
S✝ : WSeq (Computation α)
a : α
h : a ∈ parallel S✝
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = pure a
a' : α
this : F l (Sum.inl a')
e' :
  rmap (corec parallel.aux1)
      (rmap
        (fun l' ↦
          match Seq.destruct S with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))
        (Sum.inl a')) =
    Sum.inl a
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
injection e' with h'

Goal state after:
case h1.inl
α : Type u
S✝ : WSeq (Computation α)
a : α
h : a ∈ parallel S✝
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = pure a
a' : α
this : F l (Sum.inl a')
h' : a' = a
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case h2.inr
α : Type u
S✝ : WSeq (Computation α)
a : α
h : a ∈ parallel S✝
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
C' : Computation α
IH :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C' → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = C'.think
l' : List (Computation α)
this : F l (Sum.inr l')
e' :
  rmap (corec parallel.aux1)
      (rmap
        (fun l' ↦
          match Seq.destruct S with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))
        (Sum.inr l')) =
    Sum.inr C'
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
injection e' with h'

Goal state after:
case h2.inr
α : Type u
S✝ : WSeq (Computation α)
a : α
h : a ∈ parallel S✝
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
C' : Computation α
IH :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C' → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = C'.think
l' : List (Computation α)
this : F l (Sum.inr l')
h' :
  corec parallel.aux1
      ((fun l' ↦
          match Seq.destruct S with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))
        l') =
    C'
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
ss : WSeq α
IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
x✝ : WSeq α
s✝ : WSeq (WSeq α)
ej : nil.append (cons x✝ s✝).join = ss.think
m : a ∈ nil.append (cons x✝ s✝).join
this : x✝.append s✝.join = ss
⊢ a ∈ nil ∨ ∃ s ∈ cons x✝ s✝, a ∈ s

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
ss : WSeq α
IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
s✝ : WSeq (WSeq α)
ej : nil.append s✝.think.join = ss.think
m : a ∈ nil.append s✝.think.join
this : s✝.join = ss
⊢ a ∈ nil ∨ ∃ s ∈ s✝.think, a ∈ s

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
ss : WSeq α
IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
S : WSeq (WSeq α)
s✝ : WSeq α
ej : s✝.think.append S.join = ss.think
m : a ∈ s✝.think.append S.join
this : s✝.append S.join = ss
⊢ a ∈ s✝.think ∨ ∃ s ∈ S, a ∈ s

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.Tree.Traversable

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
f : α → β
⊢ traverse (pure ∘ f) nil = pure (map f nil)

Tactic:
rw [traverse, map]

Goal state after:
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)

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.Vector.Snoc

Goal state before:
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:
simp_all

Goal state after:
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)

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.Vector.Snoc

Goal state before:
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:
simp_all

Goal state after:
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)

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.Vector.Snoc

Goal state before:
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:
simp_all

Goal state after:
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)

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
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:
simp_all

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

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
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:
simp_all

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

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
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:
simp_all

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

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
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:
simp_all

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

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
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:
simp_all

Goal state after:
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 ⋯

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
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:
simp_all

Goal state after:
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)

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
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:
simp_all

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

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
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:
simp_all

Goal state after:
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)

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
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:
simp_all

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

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
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:
simp_all

Goal state after:
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)

Tactic:
simp_all

Goal state after: