awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
p : α → Prop
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (cons hd tl) → p hd ∧ motive tl
n : ℕ
this : motive (s.drop n)
h : ∀ (x : α), (s.drop n).head = some x → p x
⊢ ∀ (x : α), s.get? n = some x → p x

Tactic:
rw [← head_dropn]

Premises used: Stream'.Seq.head_dropn
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
p : α → Prop
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (cons hd tl) → p hd ∧ motive tl
n : ℕ
this : motive (s.drop n)
h : ∀ (s' : Seq α) (this : motive s') (x : α), s'.head = some x → p x
⊢ ∀ (x : α), (s.drop n).head = some x → p x

Tactic:
generalize s.drop n = s' at this

Premises used: Stream'.Seq.drop
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
p : α → Prop
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (cons hd tl) → p hd ∧ motive tl
n : ℕ
this : motive nil
⊢ ∀ (x : α), head nil = some x → p x

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
p : α → Prop
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (cons hd tl) → p hd ∧ motive tl
n : ℕ
hd : α
tl : Seq α
this : motive (cons hd tl)
⊢ ∀ (x : α), (cons hd tl).head = some x → p x

Tactic:
simp [(step hd tl this).left]

Premises used: And.left
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
p : α → Prop
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (cons hd tl) → p hd ∧ motive tl
n : ℕ
s' : Seq α
this : motive s'
h : ∀ (this : motive nil) (x : α), head nil = some x → p x
h₁ : ∀ (hd : α) (tl : Seq α) (this : motive (cons hd tl)) (x : α), (cons hd tl).head = some x → p x
⊢ ∀ (x : α), s'.head = some x → p x

Tactic:
cases s' with
  | nil => simp
  | cons hd tl => simp [(step hd tl this).left]

Premises used: Stream'.Seq.nil, Stream'.Seq.cons
-- Module: Mathlib.Data.Seq.Basic
Goal:
α β : Type u
f : α → β
p : β → Prop
s : Seq α
⊢ (∀ x ∈ map f s, p x) ↔ ∀ x ∈ s, (p ∘ f) x

Tactic:
⟨fun _ _ hx ↦ ?_, fun _ _ hx ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Data.Seq.Basic
Goal:
α β : Type u
f : α → β
p : β → Prop
s : Seq α
refine_1 : (∀ x ∈ map f s, p x) → ∀ (x : α) (hx : x ∈ s), (p ∘ f) x
refine_2 : (∀ x ∈ s, (p ∘ f) x) → ∀ (x : β) (hx : x ∈ map f s), p x
⊢ (∀ x ∈ map f s, p x) ↔ ∀ x ∈ s, (p ∘ f) x

Tactic:
refine ⟨fun _ _ hx ↦ ?_, fun _ _ hx ↦ ?_⟩
-- Module: Mathlib.Data.Seq.Basic
Goal:
α β : Type u
f : α → β
p : β → Prop
s : Seq α
h : ∀ x ∈ map f s, p x
x : α
hx : x ∈ s
⊢ (p ∘ f) x

Tactic:
solve_by_elim [mem_map f hx]

Premises used: Stream'.Seq.mem_map
-- Module: Mathlib.Data.Seq.Basic
Goal:
α β : Type u
f : α → β
p : β → Prop
s : Seq α
h : ∀ x ∈ s, (p ∘ f) x
x : β
hx : x ∈ map f s
refine_2 : ∀ w ∈ s, ∀ (hx' : f w = x), p x
⊢ p x

Tactic:
obtain ⟨_, _, hx'⟩ := exists_of_mem_map hx

Premises used: Stream'.Seq.exists_of_mem_map
-- Module: Mathlib.Data.Seq.Basic
Goal:
α β : Type u
f : α → β
p : β → Prop
s : Seq α
h : ∀ x ∈ s, (p ∘ f) x
x : β
hx : x ∈ map f s
w : α
left : w ∈ s
hx' : f w = x
refine_2 : p (f w)
⊢ p x

Tactic:
rw [← hx']
-- Module: Mathlib.Data.Seq.Basic
Goal:
α β : Type u
f : α → β
p : β → Prop
s : Seq α
h : ∀ x ∈ s, (p ∘ f) x
x : β
hx : x ∈ map f s
w : α
left : w ∈ s
hx' : f w = x
⊢ p (f w)

Tactic:
solve_by_elim
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
p : α → Prop
x : α
s : Seq α
h_all : ∀ x ∈ s, p x
hx : x ∈ take 0 s
⊢ p x

Tactic:
simp [take] at hx

Premises used: Stream'.Seq.take
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
p : α → Prop
x : α
m : ℕ
ih : ∀ {s : Seq α} (h_all : ∀ x ∈ s, p x) (hx : x ∈ take m s), p x
h_all : ∀ (x : α), Membership.mem (γ := Seq α) nil x → p x
hx : Membership.mem (γ := List α) (take (m + 1) nil) x
⊢ p x

Tactic:
simp at hx
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
p : α → Prop
x : α
m : ℕ
ih : ∀ {s : Seq α} (h_all : ∀ x ∈ s, p x) (hx : x ∈ take m s), p x
hd : α
tl : Seq α
h_all : ∀ x ∈ cons hd tl, p x
hx : x ∈ take (m + 1) (cons hd tl)
⊢ x = hd ∨ x ∈ take m tl

Tactic:
simp only [take_succ_cons, List.mem_cons, mem_cons_iff, forall_eq_or_imp] at hx h_all

Premises used: Stream'.Seq.take_succ_cons, forall_eq_or_imp, List.mem_cons, Stream'.Seq.mem_cons_iff
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
p : α → Prop
x : α
m : ℕ
ih : ∀ {s : Seq α} (h_all : ∀ x ∈ s, p x) (hx : x ∈ take m s), p x
hd : α
tl : Seq α
h_all : ∀ x ∈ cons hd tl, p x
hx : x ∈ take (m + 1) (cons hd tl)
hx₁ : x = hd ∨ x ∈ take m tl
⊢ p hd ∧ ∀ a ∈ tl, p a

Tactic:
simp only [take_succ_cons, List.mem_cons, mem_cons_iff, forall_eq_or_imp] at hx h_all

Premises used: Stream'.Seq.take_succ_cons, forall_eq_or_imp, List.mem_cons, Stream'.Seq.mem_cons_iff
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
p : α → Prop
x : α
m : ℕ
ih : ∀ {s : Seq α} (h_all : ∀ x ∈ s, p x) (hx : x ∈ take m s), p x
hd : α
tl : Seq α
hx : x = hd ∨ x ∈ take m tl
h_all : p hd ∧ ∀ a ∈ tl, p a
succ : ∀ (h_all : p x ∧ ∀ a ∈ tl, p a), p x
succ₁ : ∀ (hx : x ∈ take m tl), p x
⊢ p x

Tactic:
rcases hx with (rfl | hx)

Premises used: rfl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
p : α → Prop
x : α
m : ℕ
ih : ∀ {s : Seq α} (h_all : ∀ x ∈ s, p x) (hx : x ∈ take m s), p x
tl : Seq α
h_all : p x ∧ ∀ a ∈ tl, p a
⊢ p x

Tactic:
h_all.left

Premises used: And.left
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
p : α → Prop
x : α
m : ℕ
ih : ∀ {s : Seq α} (h_all : ∀ x ∈ s, p x) (hx : x ∈ take m s), p x
hd : α
tl : Seq α
h_all : p hd ∧ ∀ a ∈ tl, p a
hx : x ∈ take m tl
⊢ p x

Tactic:
ih h_all.right hx

Premises used: And.right
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
p : α → Prop
x : α
m : ℕ
ih : ∀ {s : Seq α} (h_all : ∀ x ∈ s, p x) (hx : x ∈ take m s), p x
tl : Seq α
h_all : p x ∧ ∀ a ∈ tl, p a
⊢ p x

Tactic:
exacts [h_all.left, ih h_all.right hx]

Premises used: And.left
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
p : α → Prop
x : α
m : ℕ
ih : ∀ {s : Seq α} (h_all : ∀ x ∈ s, p x) (hx : x ∈ take m s), p x
s : Seq α
h_all : ∀ x ∈ s, p x
hx : x ∈ take (m + 1) s
succ :
  ∀ (h_all : ∀ (x : α), Membership.mem (γ := Seq α) nil x → p x)
    (hx : Membership.mem (γ := List α) (take (m + 1) nil) x), p x
succ₁ : ∀ (hd : α) (tl : Seq α) (h_all : ∀ x ∈ cons hd tl, p x) (hx : x ∈ take (m + 1) (cons hd tl)), p x
⊢ p x

Tactic:
cases s with
    | nil => simp at hx
    | cons hd tl =>
      simp only [take_succ_cons, List.mem_cons, mem_cons_iff, forall_eq_or_imp] at hx h_all
      rcases hx with (rfl | hx)
      exacts [h_all.left, ih h_all.right hx]

Premises used: Stream'.Seq.take_succ_cons, forall_eq_or_imp, Stream'.Seq.nil, Stream'.Seq.cons, List.mem_cons, Stream'.Seq.mem_cons_iff, rfl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
p : α → Prop
h_all : ∀ x ∈ s, p x
n : ℕ
x : α
hx : x ∈ take n s
zero : ∀ {s : Seq α} (h_all : ∀ x ∈ s, p x) (hx : x ∈ take 0 s), p x
succ :
  ∀ (m : ℕ) (ih : ∀ {s : Seq α} (h_all : ∀ x ∈ s, p x) (hx : x ∈ take m s), p x) {s : Seq α} (h_all : ∀ x ∈ s, p x)
    (hx : x ∈ take (m + 1) s), p x
⊢ p x

Tactic:
induction n generalizing s with
  | zero => simp [take] at hx
  | succ m ih =>
    cases s with
    | nil => simp at hx
    | cons hd tl =>
      simp only [take_succ_cons, List.mem_cons, mem_cons_iff, forall_eq_or_imp] at hx h_all
      rcases hx with (rfl | hx)
      exacts [h_all.left, ih h_all.right hx]

Premises used: Stream'.Seq.take_succ_cons, Stream'.Seq.take, forall_eq_or_imp, Stream'.Seq.nil, Stream'.Seq.cons, List.mem_cons, Stream'.Seq.mem_cons_iff, rfl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
p : α → Prop
s : Seq α
h_all : ∀ x ∈ s, p x
n : ℕ
x : α
hx : p x
y : α
hy : y ∈ s.set n x
⊢ ∃ (i : ℕ), some y = (s.set n x).get? i

Tactic:
simp only [mem_iff_exists_get?] at hy

Premises used: Stream'.Seq.mem_iff_exists_get?
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
p : α → Prop
s : Seq α
h_all : ∀ x ∈ s, p x
n : ℕ
x : α
hx : p x
y : α
hy : ∃ (i : ℕ), some y = (s.set n x).get? i
obtain : ∀ (m : ℕ) (hy : some y = (s.set n x).get? m), p y
⊢ p y

Tactic:
obtain ⟨m, hy⟩ := hy
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
p : α → Prop
s : Seq α
h_all : ∀ x ∈ s, p x
n : ℕ
x : α
hx : p x
y : α
m : ℕ
hy : some y = (s.set n x).get? m
inl : ∀ (hy : some y = (s.set n x).get? n), p y
inr : ∀ (h_nm : n ≠ m), p y
⊢ p y

Tactic:
rcases eq_or_ne n m with (rfl | h_nm)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
p : α → Prop
s : Seq α
h_all : ∀ x ∈ s, p x
n : ℕ
x : α
hx : p x
y : α
hy : some y = (s.set n x).get? n
pos : ∀ (h_term : s.TerminatedAt n), p y
neg : ∀ (h_term : ¬s.TerminatedAt n), p y
⊢ p y

Tactic:
by_cases h_term : s.TerminatedAt n

Premises used: Stream'.Seq.TerminatedAt
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
p : α → Prop
s : Seq α
h_all : ∀ x ∈ s, p x
n : ℕ
x : α
hx : p x
y : α
hy : some y = (s.set n x).get? n
h_term : s.TerminatedAt n
⊢ p y

Tactic:
simp [get?_set_of_terminatedAt _ h_term] at hy

Premises used: Stream'.Seq.get?_set_of_terminatedAt
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
p : α → Prop
s : Seq α
h_all : ∀ x ∈ s, p x
n : ℕ
x : α
hx : p x
y : α
hy : some y = (s.set n x).get? n
h_term : ¬s.TerminatedAt n
⊢ p y

Tactic:
simp_all [get?_set_of_not_terminatedAt _ h_term]

Premises used: Stream'.Seq.get?_set_of_not_terminatedAt
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
p : α → Prop
s : Seq α
h_all : ∀ x ∈ s, p x
n : ℕ
x : α
hx : p x
y : α
m : ℕ
hy : some y = (s.set n x).get? m
h_nm : n ≠ m
⊢ some y = s.get? m

Tactic:
rw [get?_set_of_ne _ _ h_nm.symm] at hy

Premises used: Ne.symm, Stream'.Seq.get?_set_of_ne
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
p : α → Prop
s : Seq α
h_all : ∀ x ∈ s, p x
n : ℕ
x : α
hx : p x
y : α
m : ℕ
hy : some y = (s.set n x).get? m
h_nm : n ≠ m
hy₁ : some y = s.get? m
⊢ n ≠ m

Tactic:
rw [get?_set_of_ne _ _ h_nm.symm] at hy

Premises used: Ne.symm, Stream'.Seq.get?_set_of_ne
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
p : α → Prop
s : Seq α
h_all : ∀ x ∈ s, p x
n : ℕ
x : α
hx : p x
y : α
m : ℕ
hy : some y = s.get? m
h_nm : n ≠ m
⊢ p y

Tactic:
apply h_all _ (get?_mem hy.symm)

Premises used: Stream'.Seq.get?_mem, Eq.symm
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
⊢ Pairwise R Seq.nil

Tactic:
simp [Pairwise]

Premises used: Stream'.Seq.Pairwise
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h_hd : ∀ x ∈ tl, R hd x
h_tl : ∀ (i j : ℕ), i < j → ∀ x ∈ tl.get? i, ∀ y ∈ tl.get? j, R x y
i : ℕ
x : α
hx : x ∈ (Seq.cons hd tl).get? i
y : α
h_ij : i < 0
hy : y ∈ (Seq.cons hd tl).get? 0
⊢ R x y

Tactic:
simp at h_ij
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h_hd : ∀ x ∈ tl, R hd x
h_tl : ∀ (i j : ℕ), i < j → ∀ x ∈ tl.get? i, ∀ y ∈ tl.get? j, R x y
x y : α
k : ℕ
hy : y ∈ tl.get? k
hx : x ∈ (Seq.cons hd tl).get? 0
h_ij : 0 < k + 1
⊢ hd = x

Tactic:
simp only [get?_cons_zero, Option.mem_def, Option.some.injEq] at hx

Premises used: Stream'.Seq.get?_cons_zero, Option.some.injEq, Option.mem_def
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h_hd : ∀ x ∈ tl, R hd x
h_tl : ∀ (i j : ℕ), i < j → ∀ x ∈ tl.get? i, ∀ y ∈ tl.get? j, R x y
x y : α
k : ℕ
hy : y ∈ tl.get? k
h_ij : 0 < k + 1
hx : hd = x
⊢ R x y

Tactic:
hx ▸ all_get h_hd hy

Premises used: Eq.rec, Stream'.Seq.all_get
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h_hd : ∀ x ∈ tl, R hd x
h_tl : ∀ (i j : ℕ), i < j → ∀ x ∈ tl.get? i, ∀ y ∈ tl.get? j, R x y
x y : α
k : ℕ
hy : y ∈ tl.get? k
h_ij : 0 < k + 1
hx : hd = x
⊢ R x y

Tactic:
exact hx ▸ all_get h_hd hy
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h_hd : ∀ x ∈ tl, R hd x
h_tl : ∀ (i j : ℕ), i < j → ∀ x ∈ tl.get? i, ∀ y ∈ tl.get? j, R x y
x y : α
k : ℕ
hy : y ∈ tl.get? k
n : ℕ
hx : x ∈ (Seq.cons hd tl).get? (n + 1)
h_ij : n + 1 < k + 1
⊢ n < k

Tactic:
lia
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h_hd : ∀ x ∈ tl, R hd x
h_tl : ∀ (i j : ℕ), i < j → ∀ x ∈ tl.get? i, ∀ y ∈ tl.get? j, R x y
x y : α
k : ℕ
hy : y ∈ tl.get? k
n : ℕ
hx : x ∈ (Seq.cons hd tl).get? (n + 1)
h_ij : n + 1 < k + 1
⊢ R x y

Tactic:
exact h_tl n k (by lia) x hx y hy
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h_hd : ∀ x ∈ tl, R hd x
h_tl : ∀ (i j : ℕ), i < j → ∀ x ∈ tl.get? i, ∀ y ∈ tl.get? j, R x y
i : ℕ
x : α
hx : x ∈ (Seq.cons hd tl).get? i
y : α
k : ℕ
h_ij : i < k + 1
hy : y ∈ tl.get? k
succ : ∀ (hx : x ∈ (Seq.cons hd tl).get? 0) (h_ij : 0 < k + 1), R x y
succ₁ : ∀ (n : ℕ) (hx : x ∈ (Seq.cons hd tl).get? (n + 1)) (h_ij : n + 1 < k + 1), R x y
⊢ R x y

Tactic:
cases i with
    | zero =>
      simp only [get?_cons_zero, Option.mem_def, Option.some.injEq] at hx
      exact hx ▸ all_get h_hd hy
    | succ n => exact h_tl n k (by lia) x hx y hy

Premises used: Stream'.Seq.get?_cons_zero, Option.some.injEq, Option.mem_def
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h_hd : ∀ x ∈ tl, R hd x
h_tl : ∀ (i j : ℕ), i < j → ∀ x ∈ tl.get? i, ∀ y ∈ tl.get? j, R x y
i j : ℕ
h_ij : i < j
x : α
hx : x ∈ (Seq.cons hd tl).get? i
y : α
hy : y ∈ (Seq.cons hd tl).get? j
zero : ∀ (h_ij : i < 0) (hy : y ∈ (Seq.cons hd tl).get? 0), R x y
succ : ∀ (k : ℕ) (h_ij : i < k + 1) (hy : y ∈ (Seq.cons hd tl).get? (k + 1)), R x y
⊢ R x y

Tactic:
cases j with
  | zero => simp at h_ij
  | succ k =>
    simp only [get?_cons_succ] at hy
    cases i with
    | zero =>
      simp only [get?_cons_zero, Option.mem_def, Option.some.injEq] at hx
      exact hx ▸ all_get h_hd hy
    | succ n => exact h_tl n k (by lia) x hx y hy

Premises used: Stream'.Seq.get?_cons_zero, Option.some.injEq, Stream'.Seq.get?_cons_succ, Option.mem_def
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h : ∀ (i j : ℕ), i < j → ∀ x ∈ (Seq.cons hd tl).get? i, ∀ y ∈ (Seq.cons hd tl).get? j, R x y
i j : ℕ
h_ij : i < j
⊢ i + 1 < j + 1

Tactic:
lia
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h : ∀ (i j : ℕ), i < j → ∀ x ∈ (Seq.cons hd tl).get? i, ∀ y ∈ (Seq.cons hd tl).get? j, R x y
refine : ∀ x ∈ tl, R hd x
⊢ (∀ x ∈ tl, R hd x) ∧ ∀ (i j : ℕ), i < j → ∀ x ∈ tl.get? i, ∀ y ∈ tl.get? j, R x y

Tactic:
refine ⟨?_, fun i j h_ij ↦ h (i + 1) (j + 1) (by lia)⟩
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h : ∀ (i j : ℕ), i < j → ∀ x ∈ (Seq.cons hd tl).get? i, ∀ y ∈ (Seq.cons hd tl).get? j, R x y
x : α
hx : x ∈ tl
⊢ ∃ (i : ℕ), some x = tl.get? i

Tactic:
rw [mem_iff_exists_get?] at hx

Premises used: Stream'.Seq.mem_iff_exists_get?
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h : ∀ (i j : ℕ), i < j → ∀ x ∈ (Seq.cons hd tl).get? i, ∀ y ∈ (Seq.cons hd tl).get? j, R x y
x : α
hx : ∃ (i : ℕ), some x = tl.get? i
obtain : ∀ (n : ℕ) (hx : some x = tl.get? n), R hd x
⊢ R hd x

Tactic:
obtain ⟨n, hx⟩ := hx
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h : ∀ (i j : ℕ), i < j → ∀ x ∈ (Seq.cons hd tl).get? i, ∀ y ∈ (Seq.cons hd tl).get? j, R x y
x : α
n : ℕ
hx : some x = tl.get? n
⊢ 0 < n + 1

Tactic:
lia
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h : ∀ (i j : ℕ), i < j → ∀ x ∈ (Seq.cons hd tl).get? i, ∀ y ∈ (Seq.cons hd tl).get? j, R x y
x : α
n : ℕ
hx : some x = tl.get? n
⊢ R hd x

Tactic:
simpa [← hx] using h 0 (n + 1) (by lia)

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
hd : α
h_hd : ∀ (x : α), Membership.mem (γ := Seq α) nil x → R hd x
h_tl : Pairwise R nil
⊢ Pairwise R (cons hd nil)

Tactic:
apply Pairwise.cons

Premises used: Stream'.Seq.Pairwise.cons
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
hd : α
⊢ ∀ (x : α), Membership.mem (γ := Seq α) nil x → R hd x

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
hd : α
⊢ Pairwise R nil

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
hd tl_hd : α
tl_tl : Seq α
h : ∀ (i j : ℕ), i < j → ∀ x ∈ (cons hd (cons tl_hd tl_tl)).get? i, ∀ y ∈ (cons hd (cons tl_hd tl_tl)).get? j, R x y
⊢ R hd tl_hd

Tactic:
simpa using h 0 1 Nat.one_pos

Premises used: Nat.one_pos, OfNat.ofNat
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
inst : IsTrans α R
hd tl_hd : α
tl_tl : Seq α
h_hd : R hd tl_hd
h_tl : Pairwise R (Seq.cons tl_hd tl_tl)
apply : ∀ x ∈ Seq.cons tl_hd tl_tl, R hd x
⊢ Pairwise R (Seq.cons hd (Seq.cons tl_hd tl_tl))

Tactic:
apply Pairwise.cons _ h_tl

Premises used: Stream'.Seq.Pairwise.cons
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
inst : IsTrans α R
hd tl_hd : α
tl_tl : Seq α
h_hd : R hd tl_hd
h_tl : Pairwise R (Seq.cons tl_hd tl_tl)
simp : R hd tl_hd ∧ ∀ a ∈ tl_tl, R hd a
⊢ ∀ x ∈ Seq.cons tl_hd tl_tl, R hd x

Tactic:
simp only [mem_cons_iff, forall_eq_or_imp]

Premises used: forall_eq_or_imp, Stream'.Seq.mem_cons_iff
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
inst : IsTrans α R
hd tl_hd : α
tl_tl : Seq α
h_hd : R hd tl_hd
h_tl : Pairwise R (Seq.cons tl_hd tl_tl)
⊢ R hd tl_hd ∧ ∀ a ∈ tl_tl, R hd a

Tactic:
⟨h_hd, fun x hx ↦ Trans.simple h_hd ((cons_elim h_tl).left x hx)⟩

Premises used: And.left, And.intro, Trans.simple, Stream'.Seq.Pairwise.cons_elim
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
inst : IsTrans α R
hd tl_hd : α
tl_tl : Seq α
h_hd : R hd tl_hd
h_tl : Pairwise R (Seq.cons tl_hd tl_tl)
⊢ R hd tl_hd ∧ ∀ a ∈ tl_tl, R hd a

Tactic:
exact ⟨h_hd, fun x hx ↦ Trans.simple h_hd ((cons_elim h_tl).left x hx)⟩
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl, R hd x) ∧ motive tl
i j : ℕ
h_ij : i < j
x : α
hx : x ∈ s.get? i
y : α
hy : y ∈ s.get? j
obtain : ∀ (k : ℕ) (hj : j = i + k + 1), R x y
⊢ R x y

Tactic:
obtain ⟨k, hj⟩ := Nat.exists_eq_add_of_lt h_ij

Premises used: Nat.exists_eq_add_of_lt
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl, R hd x) ∧ motive tl
i j : ℕ
h_ij : i < j
x : α
hx : x ∈ s.get? i
y : α
hy : y ∈ s.get? j
k : ℕ
hj : j = i + k + 1
rw : ∀ (hx : x ∈ (s.drop i).head) (y : α) (hy : y ∈ s.get? j) (k : ℕ) (hj : j = i + k + 1), R x y
⊢ R x y

Tactic:
rw [← head_dropn] at hx

Premises used: Stream'.Seq.head_dropn
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl, R hd x) ∧ motive tl
i j : ℕ
h_ij : i < j
x : α
hx : x ∈ (s.drop i).head
y : α
hy : y ∈ s.get? j
k : ℕ
hj : j = i + k + 1
⊢ y ∈ (s.drop i).get? (k + 1)

Tactic:
rw [hj, ← head_dropn, Nat.add_assoc, dropn_add, head_dropn] at hy

Premises used: Stream'.Seq.dropn_add, Nat.add_assoc, Stream'.Seq.head_dropn
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl, R hd x) ∧ motive tl
i j : ℕ
h_ij : i < j
x : α
hx : x ∈ (s.drop i).head
y : α
hy : y ∈ s.get? j
k : ℕ
hj : j = i + k + 1
hy₁ : y ∈ (s.drop i).get? (k + 1)
⊢ j = i + k + 1

Tactic:
rw [hj, ← head_dropn, Nat.add_assoc, dropn_add, head_dropn] at hy

Premises used: Stream'.Seq.dropn_add, Nat.add_assoc, Stream'.Seq.head_dropn
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl, R hd x) ∧ motive tl
i j : ℕ
h_ij : i < j
x : α
hx : x ∈ (s.drop i).head
y : α
k : ℕ
hy : y ∈ (s.drop i).get? (k + 1)
hj : j = i + k + 1
have : ∀ (this : motive (s.drop i)), R x y
⊢ R x y

Tactic:
have := all_coind_drop_motive motive base (fun hd tl ih ↦ (step hd tl ih).right) i
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl, R hd x) ∧ motive tl
i j : ℕ
h_ij : i < j
x : α
hx : x ∈ (s.drop i).head
y : α
k : ℕ
hy : y ∈ (s.drop i).get? (k + 1)
hj : j = i + k + 1
this : motive (s.drop i)
generalize : ∀ (s' : Seq α) (hx : x ∈ s'.head) (hy : y ∈ s'.get? (k + 1)) (this : motive s'), R x y
⊢ R x y

Tactic:
generalize s.drop i = s' at *

Premises used: Stream'.Seq.drop
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl, R hd x) ∧ motive tl
i j : ℕ
h_ij : i < j
x y : α
k : ℕ
hj : j = i + k + 1
hx : Membership.mem (γ := Option α) (head Seq.nil) x
hy : Membership.mem (γ := Option α) (get? Seq.nil (k + 1)) y
this : motive Seq.nil
⊢ R x y

Tactic:
simp at hx
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl, R hd x) ∧ motive tl
i j : ℕ
h_ij : i < j
x y : α
k : ℕ
hj : j = i + k + 1
hd : α
tl : Seq α
hx : x ∈ (Seq.cons hd tl).head
hy : y ∈ (Seq.cons hd tl).get? (k + 1)
this : motive (Seq.cons hd tl)
⊢ hd = x

Tactic:
simp only [head_cons, Option.mem_def, Option.some.injEq, get?_cons_succ] at hx hy

Premises used: Option.some.injEq, Stream'.Seq.head_cons, Stream'.Seq.get?_cons_succ, Option.mem_def
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl, R hd x) ∧ motive tl
i j : ℕ
h_ij : i < j
x y : α
k : ℕ
hj : j = i + k + 1
hd : α
tl : Seq α
hx : x ∈ (Seq.cons hd tl).head
hy : y ∈ (Seq.cons hd tl).get? (k + 1)
this : motive (Seq.cons hd tl)
hx₁ : hd = x
⊢ tl.get? k = some y

Tactic:
simp only [head_cons, Option.mem_def, Option.some.injEq, get?_cons_succ] at hx hy

Premises used: Option.some.injEq, Stream'.Seq.head_cons, Stream'.Seq.get?_cons_succ, Option.mem_def
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl, R hd x) ∧ motive tl
i j : ℕ
h_ij : i < j
x y : α
k : ℕ
hj : j = i + k + 1
hd : α
tl : Seq α
this : motive (Seq.cons hd tl)
hx : hd = x
hy : tl.get? k = some y
⊢ R x y

Tactic:
hx ▸ all_get (step hd tl this).left hy

Premises used: Eq.rec, And.left, Stream'.Seq.all_get
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl, R hd x) ∧ motive tl
i j : ℕ
h_ij : i < j
x y : α
k : ℕ
hj : j = i + k + 1
hd : α
tl : Seq α
this : motive (Seq.cons hd tl)
hx : hd = x
hy : tl.get? k = some y
⊢ R x y

Tactic:
exact hx ▸ all_get (step hd tl this).left hy
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
R : α → α → Prop
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl, R hd x) ∧ motive tl
i j : ℕ
h_ij : i < j
x y : α
k : ℕ
hj : j = i + k + 1
s' : Seq α
hx : x ∈ s'.head
hy : y ∈ s'.get? (k + 1)
this : motive s'
nil :
  ∀ (hx : Membership.mem (γ := Option α) (head Seq.nil) x)
    (hy : Membership.mem (γ := Option α) (get? Seq.nil (k + 1)) y) (this : motive Seq.nil), R x y
cons :
  ∀ (hd : α) (tl : Seq α) (hx : x ∈ (Seq.cons hd tl).head) (hy : y ∈ (Seq.cons hd tl).get? (k + 1))
    (this : motive (Seq.cons hd tl)), R x y
⊢ R x y

Tactic:
cases s' with
  | nil => simp at hx
  | cons hd tl =>
    simp only [head_cons, Option.mem_def, Option.some.injEq, get?_cons_succ] at hx hy
    exact hx ▸ all_get (step hd tl this).left hy

Premises used: Option.some.injEq, Stream'.Seq.Pairwise.nil, Stream'.Seq.head_cons, Stream'.Seq.get?_cons_succ, Stream'.Seq.Pairwise.cons, Option.mem_def