awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs : Vector α n
ys : Vector β n
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
s₁ : σ₁
s₂ : σ₂
R : σ₁ → σ₂ → Prop
h₀ : R s₁ s₂
hR : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).1 (f₂ a b q).1 ∧ (f₁ a b s).2 = (f₂ a b q).2
induction :
  ∀ {s₁ : σ₁} {s₂ : σ₂} (h₀ : R s₁ s₂),
    R (mapAccumr₂ f₁ nil nil s₁).1 (mapAccumr₂ f₂ nil nil s₂).1 ∧
      (mapAccumr₂ f₁ nil nil s₁).2 = (mapAccumr₂ f₂ nil nil s₂).2
snoc :
  ∀ {n : ℕ} (xs : Vector α n) (ys : Vector β n) (x : α) (y : β),
    (∀ {s₁ : σ₁} {s₂ : σ₂} (h₀ : R s₁ s₂),
        R (mapAccumr₂ f₁ xs ys s₁).1 (mapAccumr₂ f₂ xs ys s₂).1 ∧
          (mapAccumr₂ f₁ xs ys s₁).2 = (mapAccumr₂ f₂ xs ys s₂).2) →
      ∀ {s₁ : σ₁} {s₂ : σ₂} (h₀ : R s₁ s₂),
        R (mapAccumr₂ f₁ (xs.snoc x) (ys.snoc y) s₁).1 (mapAccumr₂ f₂ (xs.snoc x) (ys.snoc y) s₂).1 ∧
          (mapAccumr₂ f₁ (xs.snoc x) (ys.snoc y) s₁).2 = (mapAccumr₂ f₂ (xs.snoc x) (ys.snoc y) s₂).2
⊢ R (mapAccumr₂ f₁ xs ys s₁).1 (mapAccumr₂ f₂ xs ys s₂).1 ∧ (mapAccumr₂ f₁ xs ys s₁).2 = (mapAccumr₂ f₂ xs ys s₂).2

Tactic:
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs : Vector α n
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).1 (f₂ a b q).1 ∧ (f₁ a b s).2 = (f₂ a b q).2
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr₂ f₁ nil nil s₁).1 (mapAccumr₂ f₂ nil nil s₂).1 ∧
    (mapAccumr₂ f₁ nil nil s₁).2 = (mapAccumr₂ f₂ nil nil s₂).2

Tactic:
⟨h₀, rfl⟩

Premises used: And.intro, rfl
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs : Vector α n
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).1 (f₂ a b q).1 ∧ (f₁ a b s).2 = (f₂ a b q).2
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr₂ f₁ nil nil s₁).1 (mapAccumr₂ f₂ nil nil s₂).1 ∧
    (mapAccumr₂ f₁ nil nil s₁).2 = (mapAccumr₂ f₂ nil nil s₂).2

Tactic:
exact ⟨h₀, rfl⟩
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs : Vector α n
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).1 (f₂ a b q).1 ∧ (f₁ a b s).2 = (f₂ a b q).2
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr₂ f₁ nil nil s₁).1 (mapAccumr₂ f₂ nil nil s₂).1 ∧
    (mapAccumr₂ f₁ nil nil s₁).2 = (mapAccumr₂ f₂ nil nil s₂).2

Tactic:
next => exact ⟨h₀, rfl⟩
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs_1 : Vector α n
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).1 (f₂ a b q).1 ∧ (f₁ a b s).2 = (f₂ a b q).2
n_1 : ℕ
xs : Vector α n_1
ys : Vector β n_1
x : α
y : β
ih :
  ∀ {s₁ : σ₁} {s₂ : σ₂} (h₀ : R s₁ s₂),
    R (mapAccumr₂ f₁ xs ys s₁).1 (mapAccumr₂ f₂ xs ys s₂).1 ∧ (mapAccumr₂ f₁ xs ys s₁).2 = (mapAccumr₂ f₂ xs ys s₂).2
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (f₁ x y s₁).1 (f₂ x y s₂).1

Tactic:
rcases (hR x y h₀) with ⟨hR, _⟩
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs_1 : Vector α n
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).1 (f₂ a b q).1 ∧ (f₁ a b s).2 = (f₂ a b q).2
n_1 : ℕ
xs : Vector α n_1
ys : Vector β n_1
x : α
y : β
ih :
  ∀ {s₁ : σ₁} {s₂ : σ₂} (h₀ : R s₁ s₂),
    R (mapAccumr₂ f₁ xs ys s₁).1 (mapAccumr₂ f₂ xs ys s₂).1 ∧ (mapAccumr₂ f₁ xs ys s₁).2 = (mapAccumr₂ f₂ xs ys s₂).2
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
hR₁ : R (f₁ x y s₁).1 (f₂ x y s₂).1
⊢ (f₁ x y s₁).2 = (f₂ x y s₂).2

Tactic:
rcases (hR x y h₀) with ⟨hR, _⟩
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs_1 : Vector α n
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
R : σ₁ → σ₂ → Prop
hR_1 : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).1 (f₂ a b q).1 ∧ (f₁ a b s).2 = (f₂ a b q).2
n_1 : ℕ
xs : Vector α n_1
ys : Vector β n_1
x : α
y : β
ih :
  ∀ {s₁ : σ₁} {s₂ : σ₂} (h₀ : R s₁ s₂),
    R (mapAccumr₂ f₁ xs ys s₁).1 (mapAccumr₂ f₂ xs ys s₂).1 ∧ (mapAccumr₂ f₁ xs ys s₁).2 = (mapAccumr₂ f₂ xs ys s₂).2
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
hR : R (f₁ x y s₁).1 (f₂ x y s₂).1
right : (f₁ x y s₁).2 = (f₂ x y s₂).2
simp :
  (mapAccumr₂ f₂ xs ys (f₂ x y s₂).1).2.snoc (f₁ x y s₁).2 = (mapAccumr₂ f₂ xs ys (f₂ x y s₂).1).2.snoc (f₂ x y s₂).2
⊢ R (mapAccumr₂ f₁ (xs.snoc x) (ys.snoc y) s₁).1 (mapAccumr₂ f₂ (xs.snoc x) (ys.snoc y) s₂).1 ∧
    (mapAccumr₂ f₁ (xs.snoc x) (ys.snoc y) s₁).2 = (mapAccumr₂ f₂ (xs.snoc x) (ys.snoc y) s₂).2

Tactic:
simp only [mapAccumr₂_snoc, ih hR, true_and]

Premises used: List.Vector.mapAccumr₂_snoc, true_and
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs_1 : Vector α n
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
R : σ₁ → σ₂ → Prop
hR_1 : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).1 (f₂ a b q).1 ∧ (f₁ a b s).2 = (f₂ a b q).2
n_1 : ℕ
xs : Vector α n_1
ys : Vector β n_1
x : α
y : β
ih :
  ∀ {s₁ : σ₁} {s₂ : σ₂} (h₀ : R s₁ s₂),
    R (mapAccumr₂ f₁ xs ys s₁).1 (mapAccumr₂ f₂ xs ys s₂).1 ∧ (mapAccumr₂ f₁ xs ys s₁).2 = (mapAccumr₂ f₂ xs ys s₂).2
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
hR : R (f₁ x y s₁).1 (f₂ x y s₂).1
right : (f₁ x y s₁).2 = (f₂ x y s₂).2
⊢ (mapAccumr₂ f₂ xs ys (f₂ x y s₂).1).2.snoc (f₁ x y s₁).2 = (mapAccumr₂ f₂ xs ys (f₂ x y s₂).1).2.snoc (f₂ x y s₂).2

Tactic:
congr 1
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs : Vector α n
ys : Vector β n
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
s₁ : σ₁
s₂ : σ₂
h :
  ∃ (R : σ₁ → σ₂ → Prop),
    R s₁ s₂ ∧ ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).1 (f₂ a b q).1 ∧ (f₁ a b s).2 = (f₂ a b q).2
rcases :
  ∀ (R : σ₁ → σ₂ → Prop) (h₀ : R s₁ s₂)
    (hR : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).1 (f₂ a b q).1 ∧ (f₁ a b s).2 = (f₂ a b q).2),
    (mapAccumr₂ f₁ xs ys s₁).2 = (mapAccumr₂ f₂ xs ys s₂).2
⊢ (mapAccumr₂ f₁ xs ys s₁).2 = (mapAccumr₂ f₂ xs ys s₂).2

Tactic:
rcases h with ⟨R, h₀, hR⟩
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs : Vector α n
ys : Vector β n
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
s₁ : σ₁
s₂ : σ₂
R : σ₁ → σ₂ → Prop
h₀ : R s₁ s₂
hR : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).1 (f₂ a b q).1 ∧ (f₁ a b s).2 = (f₂ a b q).2
⊢ (mapAccumr₂ f₁ xs ys s₁).2 = (mapAccumr₂ f₂ xs ys s₂).2

Tactic:
(mapAccumr₂_bisim R h₀ hR).2

Premises used: List.Vector.mapAccumr₂_bisim, And.right
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs : Vector α n
ys : Vector β n
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
s₁ : σ₁
s₂ : σ₂
R : σ₁ → σ₂ → Prop
h₀ : R s₁ s₂
hR : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).1 (f₂ a b q).1 ∧ (f₁ a b s).2 = (f₂ a b q).2
⊢ (mapAccumr₂ f₁ xs ys s₁).2 = (mapAccumr₂ f₂ xs ys s₂).2

Tactic:
exact (mapAccumr₂_bisim R h₀ hR).2

Premises used: List.Vector.mapAccumr₂_bisim, And.right
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
n : ℕ
xs : Vector α n
f : α → β
nil : map f Vector.nil = (mapAccumr (fun (x : α) (x_1 : Unit) ↦ ((), f x)) Vector.nil ()).2
snoc :
  ∀ {n : ℕ} (xs : Vector α n) (x : α),
    map f xs = (mapAccumr (fun (x : α) (x_1 : Unit) ↦ ((), f x)) xs ()).2 →
      map f (xs.snoc x) = (mapAccumr (fun (x : α) (x_1 : Unit) ↦ ((), f x)) (xs.snoc x) ()).2
⊢ map f xs = (mapAccumr (fun (x : α) (x_1 : Unit) ↦ ((), f x)) xs ()).2

Tactic:
induction xs using Vector.revInductionOn
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
n : ℕ
xs : Vector α n
f : α → β
⊢ map f nil = (mapAccumr (fun (x : α) (x_1 : Unit) ↦ ((), f x)) nil ()).2

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
n : ℕ
xs : Vector α n
f : α → β
n_1 : ℕ
xs_1 : Vector α n_1
x : α
h : map f xs_1 = (mapAccumr (fun (x : α) (x_1 : Unit) ↦ ((), f x)) xs_1 ()).2
⊢ map f (xs_1.snoc x) = (mapAccumr (fun (x : α) (x_1 : Unit) ↦ ((), f x)) (xs_1.snoc x) ()).2

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (s : σ), s ∈ S → (f a s).1 ∈ S
out : ∀ (a : α) (s s' : σ), s ∈ S → s' ∈ S → (f a s).2 = (f a s').2
rw : (mapAccumr f xs s₀).2 = (mapAccumr (fun (x : α) (x_1 : Unit) ↦ ((), (f x s₀).2)) xs ()).2
⊢ (mapAccumr f xs s₀).2 = map (fun (x : α) ↦ (f x s₀).2) xs

Tactic:
rw [Vector.map_eq_mapAccumr]

Premises used: List.Vector.map_eq_mapAccumr
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (s : σ), s ∈ S → (f a s).1 ∈ S
out : ∀ (a : α) (s s' : σ), s ∈ S → s' ∈ S → (f a s).2 = (f a s').2
h :
  ∃ (R : σ → Unit → Prop),
    R s₀ () ∧ ∀ {s : σ} {q : Unit} (a : α), R s q → R (f a s).1 ((), (f a s₀).2).1 ∧ (f a s).2 = ((), (f a s₀).2).2
⊢ (mapAccumr f xs s₀).2 = (mapAccumr (fun (x : α) (x_1 : Unit) ↦ ((), (f x s₀).2)) xs ()).2

Tactic:
apply mapAccumr_bisim_tail

Premises used: List.Vector.mapAccumr_bisim_tail
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (s : σ), s ∈ S → (f a s).1 ∈ S
out : ∀ (a : α) (s s' : σ), s ∈ S → s' ∈ S → (f a s).2 = (f a s').2
right : ∀ {s : σ} {q : Unit} (a : α), s ∈ S → (f a s).1 ∈ S ∧ (f a s).2 = ((), (f a s₀).2).2
⊢ ∃ (R : σ → Unit → Prop),
    R s₀ () ∧ ∀ {s : σ} {q : Unit} (a : α), R s q → R (f a s).1 ((), (f a s₀).2).1 ∧ (f a s).2 = ((), (f a s₀).2).2

Tactic:
use fun s _ => s ∈ S, h₀

Premises used: Membership.mem
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (s : σ), s ∈ S → (f a s).1 ∈ S
out : ∀ (a : α) (s s' : σ), s ∈ S → s' ∈ S → (f a s).2 = (f a s').2
⊢ ∀ {s : σ} {q : Unit} (a : α), s ∈ S → (f a s).1 ∈ S ∧ (f a s).2 = ((), (f a s₀).2).2

Tactic:
@fun s _q a h => ⟨closure a s h, out a s s₀ h h₀⟩

Premises used: And.intro
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (s : σ), s ∈ S → (f a s).1 ∈ S
out : ∀ (a : α) (s s' : σ), s ∈ S → s' ∈ S → (f a s).2 = (f a s').2
⊢ ∀ {s : σ} {q : Unit} (a : α), s ∈ S → (f a s).1 ∈ S ∧ (f a s).2 = ((), (f a s₀).2).2

Tactic:
exact @fun s _q a h => ⟨closure a s h, out a s s₀ h h₀⟩
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → γ
nil :
  map₂ f Vector.nil Vector.nil =
    (mapAccumr₂ (fun (x : α) (y : β) (x_1 : Unit) ↦ ((), f x y)) Vector.nil Vector.nil ()).2
snoc :
  ∀ {n : ℕ} (xs : Vector α n) (ys : Vector β n) (x : α) (y : β),
    map₂ f xs ys = (mapAccumr₂ (fun (x : α) (y : β) (x_1 : Unit) ↦ ((), f x y)) xs ys ()).2 →
      map₂ f (xs.snoc x) (ys.snoc y) =
        (mapAccumr₂ (fun (x : α) (y : β) (x_1 : Unit) ↦ ((), f x y)) (xs.snoc x) (ys.snoc y) ()).2
⊢ map₂ f xs ys = (mapAccumr₂ (fun (x : α) (y : β) (x_1 : Unit) ↦ ((), f x y)) xs ys ()).2

Tactic:
induction xs, ys using Vector.revInductionOn₂
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : 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 : Unit) ↦ ((), f x y)) nil nil ()).2

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

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (b : β) (s : σ), s ∈ S → (f a b s).1 ∈ S
out : ∀ (a : α) (b : β) (s s' : σ), s ∈ S → s' ∈ S → (f a b s).2 = (f a b s').2
rw : (mapAccumr₂ f xs ys s₀).2 = (mapAccumr₂ (fun (x : α) (y : β) (x_1 : Unit) ↦ ((), (f x y s₀).2)) xs ys ()).2
⊢ (mapAccumr₂ f xs ys s₀).2 = map₂ (fun (x1 : α) (x2 : β) ↦ (f x1 x2 s₀).2) xs ys

Tactic:
rw [Vector.map₂_eq_mapAccumr₂]

Premises used: List.Vector.map₂_eq_mapAccumr₂
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (b : β) (s : σ), s ∈ S → (f a b s).1 ∈ S
out : ∀ (a : α) (b : β) (s s' : σ), s ∈ S → s' ∈ S → (f a b s).2 = (f a b s').2
h :
  ∃ (R : σ → Unit → Prop),
    R s₀ () ∧
      ∀ {s : σ} {q : Unit} (a : α) (b : β),
        R s q → R (f a b s).1 ((), (f a b s₀).2).1 ∧ (f a b s).2 = ((), (f a b s₀).2).2
⊢ (mapAccumr₂ f xs ys s₀).2 = (mapAccumr₂ (fun (x : α) (y : β) (x_1 : Unit) ↦ ((), (f x y s₀).2)) xs ys ()).2

Tactic:
apply mapAccumr₂_bisim_tail

Premises used: List.Vector.mapAccumr₂_bisim_tail
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (b : β) (s : σ), s ∈ S → (f a b s).1 ∈ S
out : ∀ (a : α) (b : β) (s s' : σ), s ∈ S → s' ∈ S → (f a b s).2 = (f a b s').2
right : ∀ {s : σ} {q : Unit} (a : α) (b : β), s ∈ S → (f a b s).1 ∈ S ∧ (f a b s).2 = ((), (f a b s₀).2).2
⊢ ∃ (R : σ → Unit → Prop),
    R s₀ () ∧
      ∀ {s : σ} {q : Unit} (a : α) (b : β),
        R s q → R (f a b s).1 ((), (f a b s₀).2).1 ∧ (f a b s).2 = ((), (f a b s₀).2).2

Tactic:
use fun s _ => s ∈ S, h₀

Premises used: Membership.mem
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (b : β) (s : σ), s ∈ S → (f a b s).1 ∈ S
out : ∀ (a : α) (b : β) (s s' : σ), s ∈ S → s' ∈ S → (f a b s).2 = (f a b s').2
⊢ ∀ {s : σ} {q : Unit} (a : α) (b : β), s ∈ S → (f a b s).1 ∈ S ∧ (f a b s).2 = ((), (f a b s₀).2).2

Tactic:
@fun s _q a b h => ⟨closure a b s h, out a b s s₀ h h₀⟩

Premises used: And.intro
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (b : β) (s : σ), s ∈ S → (f a b s).1 ∈ S
out : ∀ (a : α) (b : β) (s s' : σ), s ∈ S → s' ∈ S → (f a b s).2 = (f a b s').2
⊢ ∀ {s : σ} {q : Unit} (a : α) (b : β), s ∈ S → (f a b s).1 ∈ S ∧ (f a b s).2 = ((), (f a b s₀).2).2

Tactic:
exact @fun s _q a b h => ⟨closure a b s h, out a b s s₀ h h₀⟩
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
s : σ
h : ∀ (a : α), (f a s).1 = s
nil : mapAccumr f Vector.nil s = (s, map (fun (x : α) ↦ (f x s).2) Vector.nil)
snoc :
  ∀ {n : ℕ} (xs : Vector α n) (x : α),
    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))
⊢ mapAccumr f xs s = (s, map (fun (x : α) ↦ (f x s).2) xs)

Tactic:
induction xs using revInductionOn
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : 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)

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

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : 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
nil : mapAccumr₂ f Vector.nil Vector.nil s = (s, map₂ (fun (x : α) (y : β) ↦ (f x y s).2) Vector.nil Vector.nil)
snoc :
  ∀ {n : ℕ} (xs : Vector α n) (ys : Vector β n) (x : α) (y : β),
    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))
⊢ mapAccumr₂ f xs ys s = (s, map₂ (fun (x : α) (y : β) ↦ (f x y s).2) xs ys)

Tactic:
induction xs, ys using revInductionOn₂
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : 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)

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : 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_1 : ℕ
xs_1 : Vector α n_1
ys_1 : Vector β n_1
x : α
y : β
h_1 : mapAccumr₂ f xs_1 ys_1 s = (s, map₂ (fun (x : α) (y : β) ↦ (f x y s).2) xs_1 ys_1)
⊢ mapAccumr₂ f (xs_1.snoc x) (ys_1.snoc y) s = (s, map₂ (fun (x : α) (y : β) ↦ (f x y s).2) (xs_1.snoc x) (ys_1.snoc y))

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
f' : α → β
s_1 : σ
h : ∀ (a : α) (s : σ), (f a s).2 = f' a
a : α
s s' : σ
h_1 : Membership.mem (γ := Set σ) Set.univ s
h_2 : Membership.mem (γ := Set σ) Set.univ s'
rw : f' a = (f a s').2
rw₁ rw₂ : f' a = f' a
⊢ (f a s).2 = (f a s').2

Tactic:
rw [h, h]
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
f' : α → β
s : σ
h : ∀ (a : α) (s : σ), (f a s).2 = f' a
rw : map (fun (x : α) ↦ (f x s).2) xs = map f' xs
⊢ (mapAccumr f xs s).2 = map f' xs

Tactic:
rw [mapAccumr_eq_map Set.univ (Set.mem_univ _) (fun _ _ _ => Set.mem_univ _)
    (fun a s s' _ _ => by rw [h, h])]

Premises used: Set.univ, Prod.fst, List.Vector.mapAccumr_eq_map, Set.mem_univ
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
f' : α → β
s : σ
h : ∀ (a : α) (s : σ), (f a s).2 = f' a
⊢ map (fun (x : α) ↦ (f x s).2) xs = map f' xs

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
f' : α → β → γ
s_1 : σ
h : ∀ (a : α) (b : β) (s : σ), (f a b s).2 = f' a b
a : α
b : β
s s' : σ
h_1 : Membership.mem (γ := Set σ) Set.univ s
h_2 : Membership.mem (γ := Set σ) Set.univ s'
rw : f' a b = (f a b s').2
rw₁ rw₂ : f' a b = f' a b
⊢ (f a b s).2 = (f a b s').2

Tactic:
rw [h, h]
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
s : σ
xs : Vector α n
f : α → σ × σ → Prod.{u_5, u_2} (σ × σ) β
h : ∀ (x : α) (s : σ), (f x (s, s)).1.1 = (f x (s, s)).1.2
h₁ :
  (fun (x : σ × σ) (s : σ) ↦
        (match (motive := σ × σ → Prop) x with
          | (s₁, s₂) => s₂ = s ∧ s₁ = s :
          Prop))
      (s, s) s ∧
    ∀ {s : σ × σ} {q : σ} (a : α),
      (fun (x : σ × σ) (s : σ) ↦
            (match (motive := σ × σ → Prop) x with
              | (s₁, s₂) => s₂ = s ∧ s₁ = s :
              Prop))
          s q →
        (fun (x : σ × σ) (s : σ) ↦
              (match (motive := σ × σ → Prop) x with
                | (s₁, s₂) => s₂ = s ∧ s₁ = s :
                Prop))
            (f a s).1 ((f a (q, q)).1.1, (f a (q, q)).2).1 ∧
          (f a s).2 = ((f a (q, q)).1.1, (f a (q, q)).2).2
⊢ ∃ (R : σ × σ → σ → Prop),
    R (s, s) s ∧
      ∀ {s : σ × σ} {q : σ} (a : α),
        R s q → R (f a s).1 ((f a (q, q)).1.1, (f a (q, q)).2).1 ∧ (f a s).2 = ((f a (q, q)).1.1, (f a (q, q)).2).2

Tactic:
use fun (s₁, s₂) s => s₂ = s ∧ s₁ = s
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
s : σ
xs : Vector α n
f : α → σ × σ → Prod.{u_5, u_2} (σ × σ) β
h : ∀ (x : α) (s : σ), (f x (s, s)).1.1 = (f x (s, s)).1.2
⊢ (fun (x : σ × σ) (s : σ) ↦
        (match (motive := σ × σ → Prop) x with
          | (s₁, s₂) => s₂ = s ∧ s₁ = s :
          Prop))
      (s, s) s ∧
    ∀ {s : σ × σ} {q : σ} (a : α),
      (fun (x : σ × σ) (s : σ) ↦
            (match (motive := σ × σ → Prop) x with
              | (s₁, s₂) => s₂ = s ∧ s₁ = s :
              Prop))
          s q →
        (fun (x : σ × σ) (s : σ) ↦
              (match (motive := σ × σ → Prop) x with
                | (s₁, s₂) => s₂ = s ∧ s₁ = s :
                Prop))
            (f a s).1 ((f a (q, q)).1.1, (f a (q, q)).2).1 ∧
          (f a s).2 = ((f a (q, q)).1.1, (f a (q, q)).2).2

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ × σ → Prod.{u_5, u_3} (σ × σ) γ
h :
  ∀ (x : α) (y : β) (s : σ),
    let s' := (f x y (s, s)).1;
    s'.1 = s'.2
h₁ :
  (fun (x : σ × σ) (s : σ) ↦
        (match (motive := σ × σ → Prop) x with
          | (s₁, s₂) => s₂ = s ∧ s₁ = s :
          Prop))
      (s, s) s ∧
    ∀ {s : σ × σ} {q : σ} (a : α) (b : β),
      (fun (x : σ × σ) (s : σ) ↦
            (match (motive := σ × σ → Prop) x with
              | (s₁, s₂) => s₂ = s ∧ s₁ = s :
              Prop))
          s q →
        (fun (x : σ × σ) (s : σ) ↦
              (match (motive := σ × σ → Prop) x with
                | (s₁, s₂) => s₂ = s ∧ s₁ = s :
                Prop))
            (f a b s).1 ((f a b (q, q)).1.1, (f a b (q, q)).2).1 ∧
          (f a b s).2 = ((f a b (q, q)).1.1, (f a b (q, q)).2).2
⊢ ∃ (R : σ × σ → σ → Prop),
    R (s, s) s ∧
      ∀ {s : σ × σ} {q : σ} (a : α) (b : β),
        R s q →
          R (f a b s).1 ((f a b (q, q)).1.1, (f a b (q, q)).2).1 ∧
            (f a b s).2 = ((f a b (q, q)).1.1, (f a b (q, q)).2).2

Tactic:
use fun (s₁, s₂) s => s₂ = s ∧ s₁ = s
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ × σ → Prod.{u_5, u_3} (σ × σ) γ
h :
  ∀ (x : α) (y : β) (s : σ),
    let s' := (f x y (s, s)).1;
    s'.1 = s'.2
⊢ (fun (x : σ × σ) (s : σ) ↦
        (match (motive := σ × σ → Prop) x with
          | (s₁, s₂) => s₂ = s ∧ s₁ = s :
          Prop))
      (s, s) s ∧
    ∀ {s : σ × σ} {q : σ} (a : α) (b : β),
      (fun (x : σ × σ) (s : σ) ↦
            (match (motive := σ × σ → Prop) x with
              | (s₁, s₂) => s₂ = s ∧ s₁ = s :
              Prop))
          s q →
        (fun (x : σ × σ) (s : σ) ↦
              (match (motive := σ × σ → Prop) x with
                | (s₁, s₂) => s₂ = s ∧ s₁ = s :
                Prop))
            (f a b s).1 ((f a b (q, q)).1.1, (f a b (q, q)).2).1 ∧
          (f a b s).2 = ((f a b (q, q)).1.1, (f a b (q, q)).2).2

Tactic:
simp_all
-- Module: Mathlib.Data.Vector.MapLemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
f : α → β → σ → σ × γ
f' : β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f a b s = f' b s
s : σ
⊢ mapAccumr₂ f nil nil s = mapAccumr f' nil s

Tactic:
rfl