mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
a₁✝ : P.mp.A
f₁✝ : P.mp.B a₁✝ ⟹ α
a₂✝ : P.mp.A
f₂✝ : P.mp.B a₂✝ ⟹ α
r✝ : R ⟨a₁✝, f₁✝⟩ ⟨a₂✝, f₂✝⟩
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a₂ : P.mp.A
f₂ : P.mp.B a₂ ⟹ α
r : R ⟨a₁, f₁⟩ ⟨a₂, f₂⟩
a' : P.A
g₁' : P.last.B a' → P.last.M
e₁' : PFunctor.M.dest a₁ = ⟨a', g₁'⟩
e₁ : dest P ⟨a₁, f₁⟩ = ⟨a', splitFun (pathDestLeft P e₁' f₁) fun x ↦ ⟨g₁' x, pathDestRight P e₁' f₁ x⟩⟩
g₂' : P.last.B a' → P.last.M
e₂' : PFunctor.M.dest a₂ = ⟨a', g₂'⟩
left✝ : pathDestLeft P e₁' f₁ = pathDestLeft P e₂' f₂
e₂ : dest P ⟨a₂, f₂⟩ = ⟨a', splitFun (pathDestLeft P e₁' f₁) fun x ↦ ⟨g₂' x, pathDestRight P e₂' f₂ x⟩⟩
h' :
  ∀ (i : (P.B a').last),
    R ((fun x ↦ ⟨g₁' x, pathDestRight P e₁' f₁ x⟩) i) ((fun x ↦ ⟨g₂' x, pathDestRight P e₂' f₂ x⟩) i)
⊢ ∃ a f f', ⟨a', g₁'⟩ = ⟨a, f⟩ ∧ ⟨a', g₂'⟩ = ⟨a, f'⟩ ∧ ∀ (i : P.last.B a), ∃ x y, R x y ∧ x.fst = f i ∧ y.fst = f' i

Tactic:
exact ⟨_, _, _, rfl, rfl, fun b => ⟨_, _, h' b, rfl, rfl⟩⟩

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
inst✝¹ : LE α
inst✝ : DecidableLE α
x : α
t : Ordnode α
h : t.Sized
h_mem : x ∈ t
⊢ 0 < t.size

Tactic:
cases t; · { contradiction }; · { simp [h.1] }

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (nil.node' rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs nil rx (node rrs rrl rrx rrr)).Sized
this : rrs ≤ 1
⊢ rrl.size = 0 ∧ rrr.size = 0

Tactic:
sr.2.2.1,

Goal state after:
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (nil.node' rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs nil rx (node rrs rrl rrx rrr)).Sized
this : rrl.size + rrr.size + 1 ≤ 1
⊢ rrl.size = 0 ∧ rrr.size = 0
Module: Mathlib.Data.PNat.Find

Goal state before:
pp: case refine_2
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
this : ∃ n' n x, p n
n : { n // (∃ n_1 x, p n_1) ∧ ∀ (m : ℕ), m < n → ¬∃ n x, p n }
n' : ℕ+
hn' : ↑n = ↑n'
pn' : p n'
⊢ p ⟨↑n, ⋯⟩

Tactic:
simpa [hn', Subtype.coe_eta] using! pn'

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case H2.inr.inl.intro
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
l1 : 1 ≤ l.size
a✝ : 1 ≤ r.size
r' : ℕ
e : Raised r.size r'
H : l.size + r' ≤ 1
left✝ : r.size ≤ r'
right✝ : r' ≤ r.size + 1
⊢ r.size ≤ delta * l.size

Tactic:
unfold delta

Goal state after:
case H2.inr.inl.intro
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
l1 : 1 ≤ l.size
a✝ : 1 ≤ r.size
r' : ℕ
e : Raised r.size r'
H : l.size + r' ≤ 1
left✝ : r.size ≤ r'
right✝ : r' ≤ r.size + 1
⊢ r.size ≤ 3 * l.size
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
⊢ (∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u) ↔
    ∃ a f,
      abs ⟨a, f⟩ = x ∧
        ∀ (i : Fin2 n) (a' : (P F).A) (f' : (P F).B a' ⟹ α), abs ⟨a', f'⟩ = x → f i '' univ ⊆ f' i '' univ

Tactic:
by
  constructor
  · intro h
    have : LiftP (fun i u => u ∈ supp x i) x := by rw [h]; introv; exact id
    rw [liftP_iff] at this
    rcases this with ⟨a, f, xeq, h'⟩
    refine ⟨a, f, xeq.symm, ?_⟩
    intro a' f' h''
    rintro hu u ⟨j, _h₂, hfi⟩
    have hh : u ∈ supp x a' := by rw [← hfi]; apply h'
    exact (mem_supp x _ u).mp hh _ _ hu
  rintro ⟨a, f, xeq, h⟩ p; rw [liftP_iff]; constructor
  · rintro ⟨a', f', xeq', h'⟩ i u usuppx
    rcases (mem_supp x _ u).mp (@usuppx) a' f' xeq'.symm with ⟨i, _, f'ieq⟩
    rw [← f'ieq]
    apply h'
  intro h'
  refine ⟨a, f, xeq.symm, ?_⟩; intro j y
  apply h'; rw [mem_supp]
  intro a' f' xeq'
  apply h _ a' f' xeq'
  apply mem_image_of_mem _ (mem_univ _)

Goal state after:
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ insert' x (node size✝ l y r) = insertWith id x (node size✝ l y r)

Tactic:
by
    unfold insert' insertWith; cases cmpLE x y <;> simp [insert'_eq_insertWith]

Goal state after:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Sigma

Goal state before:
pp: n : ℕ
A : Type u
F : A → TypeVec.{u} n → Type u
inst✝ : (α : A) → MvQPF (F α)
α : TypeVec.{u} n
f : Pi F α
⊢ Pi.abs F (Pi.repr F f) = f

Tactic:
simp +instances only [Pi.abs, Pi.repr, Sigma.eta, abs_repr]

Goal state after:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x y : (P F).W α
h : WEquiv x y
⊢ WEquiv (g <$$> x) (g <$$> y)

Tactic:
induction h with
  | ind a f' f₀ f₁ h ih => rw [q.P.w_map_wMk, q.P.w_map_wMk]; apply WEquiv.ind; exact ih
  | abs a₀ f'₀ f₀ a₁ f'₁ f₁ h =>
    rw [q.P.w_map_wMk, q.P.w_map_wMk]; apply WEquiv.abs
    change
      abs (q.P.objAppend1 a₀ (g ⊚ f'₀) fun x => q.P.wMap g (f₀ x)) =
        abs (q.P.objAppend1 a₁ (g ⊚ f'₁) fun x => q.P.wMap g (f₁ x))
    rw [← q.P.map_objAppend1, ← q.P.map_objAppend1, abs_map, abs_map, h]
  | trans x y z _ _ ih₁ ih₂ =>
    apply MvQPF.WEquiv.trans
    · apply ih₁
    · apply ih₂

Goal state after:
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
h : SuppPreservation
α : Type u
p : α → Prop
a : (P F).A
f : (P F).B a → α
h' : SuppPreservation
⊢ Liftp p (abs ⟨a, f⟩) ↔ Liftp p ⟨a, f⟩

Tactic:
rw [suppPreservation_iff_uniform] at h'

Goal state after:
case mp
F : Type u → Type u
q : QPF F
h : SuppPreservation
α : Type u
p : α → Prop
a : (P F).A
f : (P F).B a → α
h' : IsUniform
⊢ Liftp p (abs ⟨a, f⟩) ↔ Liftp p ⟨a, f⟩
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case none.some.none
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
ha : none ∈ s.destruct
c : α × WSeq α
hc : some c ∈ u.destruct
hb : none ∈ t.destruct
t1 : LiftRelO R (LiftRel R) none none
t2 : LiftRelO R (LiftRel R) none (some c)
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) none (some c)

pp: case none.some.some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
ha : none ∈ s.destruct
c : α × WSeq α
hc : some c ∈ u.destruct
val✝ : α × WSeq α
hb : some val✝ ∈ t.destruct
t1 : LiftRelO R (LiftRel R) none (some val✝)
t2 : LiftRelO R (LiftRel R) (some val✝) (some c)
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) none (some c)

Tactic:
· cases t2

Goal state after:
case none.some.some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
ha : none ∈ s.destruct
c : α × WSeq α
hc : some c ∈ u.destruct
val✝ : α × WSeq α
hb : some val✝ ∈ t.destruct
t1 : LiftRelO R (LiftRel R) none (some val✝)
t2 : LiftRelO R (LiftRel R) (some val✝) (some c)
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) none (some c)
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
m : s.think ∈ l
⊢ (corec parallel.aux1 (l, S)).Terminates

Tactic:
have H1 (l') (e' : parallel.aux2 l = Sum.inr l') : s ∈ l' := by
      induction l generalizing l' with | nil => simp at m | cons c l IH' => ?_
      simp only [List.mem_cons] at m
      rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
      · rw [← e] at e'
        -- Porting note: `revert e'` is required.
        revert e'
        split
        · simp
        · simp only [destruct_think, Sum.inr.injEq]
          rintro rfl
          simp
      · rcases e : List.foldr (fun c o =>
            match o with
            | Sum.inl a => Sum.inl a
            | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
          (Sum.inr List.nil) l with a' | ls <;> simp only [rmap] at e <;> rw [e] at e'
        · contradiction
        have := IH' m _ e
        grind

Goal state after:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
m : s.think ∈ l
H1 : ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
⊢ (corec parallel.aux1 (l, S)).Terminates
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case some.some
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
b : α × WSeq α
dtm : some b ∈ t.destruct
a : α
s' : WSeq α
dsm : some (a, s') ∈ s.destruct
dse : Prod.fst <$> some (a, s') = o
dst : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some (a, s')) (some b)
⊢ Prod.fst <$> some (a, s') ∈ t.head

Tactic:
obtain ⟨b, t'⟩ := b

Goal state after:
case some.some
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
a : α
s' : WSeq α
dsm : some (a, s') ∈ s.destruct
dse : Prod.fst <$> some (a, s') = o
b : α
t' : WSeq α
dtm : some (b, t') ∈ t.destruct
dst : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some (a, s')) (some (b, t'))
⊢ Prod.fst <$> some (a, s') ∈ t.head
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case some.some
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
b : α × WSeq α
a : α
s' : WSeq α
h : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some (a, s')) (some b)
⊢ Option.rec nil Prod.snd (some (a, s')) ~ʷ Option.rec nil Prod.snd (some b)

Tactic:
obtain ⟨b, t'⟩ := b

Goal state after:
case some.some
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
a : α
s' : WSeq α
b : α
t' : WSeq α
h : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some (a, s')) (some (b, t'))
⊢ Option.rec nil Prod.snd (some (a, s')) ~ʷ Option.rec nil Prod.snd (some (b, t'))
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case refine_2.some.some
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
b : α × WSeq α
mb : some b ∈ t.destruct
a : α
s' : WSeq α
ma : some (a, s') ∈ s.destruct
⊢ LiftRelO Eq (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) (some (a, s')) (some b)

Tactic:
obtain ⟨b, t'⟩ := b

Goal state after:
case refine_2.some.some
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
a : α
s' : WSeq α
ma : some (a, s') ∈ s.destruct
b : α
t' : WSeq α
mb : some (b, t') ∈ t.destruct
⊢ LiftRelO Eq (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) (some (a, s')) (some (b, t'))
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: case refine_2.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i✝ j✝ : ι
a : α i✝
b : α j✝
hij : i✝ < j✝
hba : ¬⟨j✝, b⟩ ≤ ⟨i✝, a⟩
⊢ ⟨i✝, a⟩ < ⟨j✝, b⟩

Tactic:
exact Sigma.Lex.left _ _ hij

Goal state after:
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₁ : γ₁
⊢ inl c₁ ∈ sumLift₂ f g a b ↔ ∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ c₁ ∈ f a₁ b₁

Tactic:
by
  rw [mem_sumLift₂, or_iff_left]
  · simp only [inl.injEq, exists_and_left, exists_eq_left']
  rintro ⟨_, _, c₂, _, _, h, _⟩
  exact inl_ne_inr h

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

Goal state before:
pp: α : 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₂ : α → σ₂ → σ₂ × γ
⊢ 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)

Tactic:
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂

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: α : 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₂ : β → σ₂ → σ₂ × γ
⊢ 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)

Tactic:
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂

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: α : 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₂ : α → β → σ₂ → σ₂ × γ
⊢ 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)

Tactic:
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂

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: α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
s₁ : σ₁
s₂ : σ₂
xs : Vector α n
ys : Vector β n
f₁ : γ → α → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
⊢ 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)

Tactic:
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂

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: α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
s₁ : σ₁
s₂ : σ₂
xs : Vector α n
ys : Vector β n
f₁ : γ → β → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
⊢ 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)

Tactic:
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂

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: α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
s₁ : σ₁
s₂ : σ₂
xs : Vector α n
ys : Vector β n
f₁ : α → γ → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
⊢ 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)

Tactic:
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂

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)