awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
hd : α
tl : Seq α
f : α → α
n : ℕ
⊢ (cons hd tl).update (n + 1) f = cons hd (tl.update n f)
have h : ∀ (n_1 : ℕ), ((cons hd tl).update (n + 1) f).get? n_1 = (cons hd (tl.update n f)).get? n_1
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
hd : α
tl : Seq α
f : α → α
n_1 n : ℕ
⊢ ((cons hd tl).update (n_1 + 1) f).get? n = (cons hd (tl.update n_1 f)).get? n
have h : ((cons hd tl).update (n_1 + 1) f).get? 0 = (cons hd (tl.update n_1 f)).get? 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
hd : α
tl : Seq α
f : α → α
n_1 n : ℕ
h : ((cons hd tl).update (n_1 + 1) f).get? 0 = (cons hd (tl.update n_1 f)).get? 0
⊢ ((cons hd tl).update (n_1 + 1) f).get? n = (cons hd (tl.update n_1 f)).get? n
have h₁ : ∀ (n : ℕ), ((cons hd tl).update (n_1 + 1) f).get? (n + 1) = (cons hd (tl.update n_1 f)).get? (n + 1)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
x : α
s : Seq α
m n : ℕ
h : m < n
⊢ (s.set m x).drop n = s.drop n
have h₁ : ∀ (i : ℕ), ((s.set m x).drop n).get? i = (s.drop n).get? i
Tactic: ext1 i
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
p : α → Prop
hd : α
tl : Seq α
h_hd : p hd
h_tl : ∀ x ∈ tl, p x
⊢ ∀ x ∈ cons hd tl, p x
have simp : p hd ∧ ∀ a ∈ tl, p a
Tactic: simp only [mem_cons_iff, forall_eq_or_imp] at *
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (cons hd tl) → motive tl
m : ℕ
ih : motive (s.drop m)
⊢ motive (s.drop (m + 1))
have succ : motive (s.drop m).tail
Tactic: simp only [drop]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (cons hd tl) → motive tl
m : ℕ
ih : motive (s.drop m)
⊢ motive (s.drop m).tail
have succ : ∀ (t : Seq α) (ih : motive t), motive t.tail
Tactic: generalize s.drop m = t at *
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (cons hd tl) → motive tl
m : ℕ
t : Seq α
ih : motive t
⊢ motive t.tail
have succ : ∀ (ih : motive nil), motive (tail nil)
Tactic: cases t
Cleared hypotheses: t, ih
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (cons hd tl) → motive tl
m : ℕ
t : Seq α
ih : motive t
succ : ∀ (ih : motive nil), motive (tail nil)
⊢ motive t.tail
have succ₁ : ∀ (x : α) (s : Seq α) (ih : motive (cons x s)), motive (cons x s).tail
Tactic: cases t
Cleared hypotheses: t, ih
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (cons hd tl) → motive tl
n : ℕ
⊢ motive (s.drop n)
have zero : motive (s.drop 0)
Tactic: induction n with
  | zero => simpa
  | succ m ih =>
    simp only [drop]
    generalize s.drop m = t at *
    cases t
    · simpa
    · exact step _ _ ih
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (cons hd tl) → motive tl
n : ℕ
zero : motive (s.drop 0)
⊢ motive (s.drop n)
have succ : ∀ (m : ℕ) (ih : motive (s.drop m)), motive (s.drop (m + 1))
Tactic: induction n with
  | zero => simpa
  | succ m ih =>
    simp only [drop]
    generalize s.drop m = t at *
    cases t
    · simpa
    · exact step _ _ ih
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
⊢ ∀ x ∈ s, p x
have h : ∀ (n : ℕ) (x : α), s.get? n = some x → p x
Tactic: apply all_of_get
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (hypothesis)
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 : ℕ
⊢ ∀ (x : α), s.get? n = some x → p x
have this : motive (s.drop n)
Tactic: have := all_coind_drop_motive motive base (fun hd tl ih ↦ (step hd tl ih).right) n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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)
⊢ ∀ (x : α), s.get? n = some x → p x
have h : ∀ (x : α), (s.drop n).head = some x → p x
Tactic: rw [← head_dropn]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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)
⊢ ∀ (x : α), (s.drop n).head = some x → p x
have h : ∀ (s' : Seq α) (this : motive s') (x : α), s'.head = some x → p x
Tactic: generalize s.drop n = s' at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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'
⊢ ∀ (x : α), s'.head = some x → p x
have h : ∀ (this : motive nil) (x : α), head nil = some x → p x
Tactic: cases s' with
  | nil => simp
  | cons hd tl => simp [(step hd tl this).left]
Cleared hypotheses: s', this
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
⊢ ∀ (x : α), s'.head = some x → p x
have h₁ : ∀ (hd : α) (tl : Seq α) (this : motive (cons hd tl)) (x : α), (cons hd tl).head = some x → p x
Tactic: cases s' with
  | nil => simp
  | cons hd tl => simp [(step hd tl this).left]
Cleared hypotheses: s', this
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α β : Type u
f : α → β
p : β → Prop
s : Seq α
⊢ (∀ x ∈ map f s, p x) ↔ ∀ x ∈ s, (p ∘ f) x
have refine_1 : (∀ x ∈ map f s, p x) → ∀ (x : α) (hx : x ∈ s), (p ∘ f) x
Tactic: refine ⟨fun _ _ hx ↦ ?_, fun _ _ hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α β : Type u
f : α → β
p : β → Prop
s : Seq α
refine_1 : (∀ x ∈ map f s, p x) → ∀ (x : α) (hx : x ∈ s), (p ∘ f) x
⊢ (∀ x ∈ map f s, p x) ↔ ∀ x ∈ s, (p ∘ f) x
have refine_2 : (∀ x ∈ s, (p ∘ f) x) → ∀ (x : β) (hx : x ∈ map f s), p x
Tactic: refine ⟨fun _ _ hx ↦ ?_, fun _ _ hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α β : Type u
f : α → β
p : β → Prop
s : Seq α
h : ∀ x ∈ s, (p ∘ f) x
x : β
hx : x ∈ map f s
⊢ p x
have refine_2 : ∀ w ∈ s, ∀ (hx' : f w = x), p x
Tactic: obtain ⟨_, _, hx'⟩ := exists_of_mem_map hx
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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 x
have refine_2 : p (f w)
Tactic: rw [← hx']
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (hypothesis)
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)
⊢ p x
have hx₁ : 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
Cleared hypotheses: h_all, hx
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (hypothesis)
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 x
have h_all₁ : 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
Cleared hypotheses: h_all, hx
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
⊢ p x
have succ : ∀ (h_all : p x ∧ ∀ a ∈ tl, p a), p x
Tactic: rcases hx with (rfl | hx)
Cleared hypotheses: hd, hx, h_all
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
⊢ p x
have succ₁ : ∀ (hx : x ∈ take m tl), p x
Tactic: rcases hx with (rfl | hx)
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
⊢ p x
have succ : ∀ (h_all : ∀ (x : α), Membership.mem (γ := Seq α) nil x → p x) (hx : Membership.mem (γ := List α) (take (m + 1) nil) 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]
Cleared hypotheses: s, h_all, hx
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
⊢ p x
have succ₁ : ∀ (hd : α) (tl : Seq α) (h_all : ∀ x ∈ cons hd tl, p x) (hx : x ∈ take (m + 1) (cons hd tl)), 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]
Cleared hypotheses: s, h_all, hx
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
p : α → Prop
h_all : ∀ x ∈ s, p x
n : ℕ
x : α
hx : x ∈ take n s
⊢ p x
have zero : ∀ {s : Seq α} (h_all : ∀ x ∈ s, p x) (hx : x ∈ take 0 s), 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]
Cleared hypotheses: s, h_all, n, hx
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
⊢ p x
have 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
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]
Cleared hypotheses: s, h_all, n, hx
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (hypothesis)
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
⊢ p y
have hy₁ : ∃ (i : ℕ), some y = (s.set n x).get? i
Tactic: simp only [mem_iff_exists_get?] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
⊢ p y
have obtain : ∀ (m : ℕ) (hy : some y = (s.set n x).get? m), p y
Tactic: obtain ⟨m, hy⟩ := hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
⊢ p y
have inl : ∀ (hy : some y = (s.set n x).get? n), p y
Tactic: rcases eq_or_ne n m with (rfl | h_nm)
Cleared hypotheses: m, hy
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
⊢ p y
have inr : ∀ (h_nm : n ≠ m), p y
Tactic: rcases eq_or_ne n m with (rfl | h_nm)
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
⊢ p y
have pos : ∀ (h_term : s.TerminatedAt n), p y
Tactic: by_cases h_term : s.TerminatedAt n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
⊢ p y
have neg : ∀ (h_term : ¬s.TerminatedAt n), p y
Tactic: by_cases h_term : s.TerminatedAt n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (hypothesis)
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
⊢ p y
have hy₁ : some y = s.get? m
Tactic: rw [get?_set_of_ne _ _ h_nm.symm] at hy
Cleared hypotheses: hy, h_nm
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (hypothesis)
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
⊢ R x y
have hx₁ : hd = x
Tactic: simp only [get?_cons_zero, Option.mem_def, Option.some.injEq] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
⊢ R x y
have succ : ∀ (hx : x ∈ (Seq.cons hd tl).get? 0) (h_ij : 0 < k + 1), 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
Cleared hypotheses: i, hx, h_ij
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
⊢ R x y
have succ₁ : ∀ (n : ℕ) (hx : x ∈ (Seq.cons hd tl).get? (n + 1)) (h_ij : n + 1 < k + 1), 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
Cleared hypotheses: i, hx, h_ij
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
⊢ R x y
have zero : ∀ (h_ij : i < 0) (hy : y ∈ (Seq.cons hd tl).get? 0), 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
Cleared hypotheses: j, h_ij, hy
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
⊢ R x y
have succ : ∀ (k : ℕ) (h_ij : i < k + 1) (hy : y ∈ (Seq.cons hd tl).get? (k + 1)), 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
Cleared hypotheses: j, h_ij, hy
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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 ∈ tl, R hd x) ∧ ∀ (i j : ℕ), i < j → ∀ x ∈ tl.get? i, ∀ y ∈ tl.get? j, R x y
have refine : ∀ x ∈ tl, R hd x
Tactic: refine ⟨?_, fun i j h_ij ↦ h (i + 1) (j + 1) (by lia)⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (hypothesis)
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
⊢ R hd x
have hx₁ : ∃ (i : ℕ), some x = tl.get? i
Tactic: rw [mem_iff_exists_get?] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
⊢ R hd x
have obtain : ∀ (n : ℕ) (hx : some x = tl.get? n), R hd x
Tactic: obtain ⟨n, hx⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
R : α → α → Prop
hd : α
⊢ Pairwise R (cons hd nil)
have h_hd : ∀ (x : α), Membership.mem (γ := Seq α) nil x → R hd x
Tactic: apply Pairwise.cons
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
R : α → α → Prop
hd : α
h_hd : ∀ (x : α), Membership.mem (γ := Seq α) nil x → R hd x
⊢ Pairwise R (cons hd nil)
have h_tl : Pairwise R nil
Tactic: apply Pairwise.cons
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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)
⊢ Pairwise R (Seq.cons hd (Seq.cons tl_hd tl_tl))
have apply : ∀ x ∈ Seq.cons tl_hd tl_tl, R hd x
Tactic: apply Pairwise.cons _ h_tl
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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)
⊢ ∀ x ∈ Seq.cons tl_hd tl_tl, R hd x
have simp : R hd tl_hd ∧ ∀ a ∈ tl_tl, R hd a
Tactic: simp only [mem_cons_iff, forall_eq_or_imp]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
⊢ R x y
have obtain : ∀ (k : ℕ) (hj : j = i + k + 1), R x y
Tactic: obtain ⟨k, hj⟩ := Nat.exists_eq_add_of_lt h_ij
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
⊢ R x y
have rw : ∀ (hx : x ∈ (s.drop i).head) (y : α) (hy : y ∈ s.get? j) (k : ℕ) (hj : j = i + k + 1), R x y
Tactic: rw [← head_dropn] at hx
Cleared hypotheses: hx, y, hy, k, hj
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (hypothesis)
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
⊢ R x y
have hy₁ : y ∈ (s.drop i).get? (k + 1)
Tactic: rw [hj, ← head_dropn, Nat.add_assoc, dropn_add, head_dropn] at hy
Cleared hypotheses: hy, hj
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
⊢ R x y
have have : ∀ (this : motive (s.drop i)), R x y
Tactic: have := all_coind_drop_motive motive base (fun hd tl ih ↦ (step hd tl ih).right) i
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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)
⊢ R x y
have generalize : ∀ (s' : Seq α) (hx : x ∈ s'.head) (hy : y ∈ s'.get? (k + 1)) (this : motive s'), R x y
Tactic: generalize s.drop i = s' at *
Cleared hypotheses: hx, hy, this
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (hypothesis)
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)
⊢ R x y
have hx₁ : hd = x
Tactic: simp only [head_cons, Option.mem_def, Option.some.injEq, get?_cons_succ] at hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (hypothesis)
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
⊢ R x y
have hy₁ : tl.get? k = some y
Tactic: simp only [head_cons, Option.mem_def, Option.some.injEq, get?_cons_succ] at hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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'
⊢ R x y
have 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
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
Cleared hypotheses: s', hx, hy, this
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
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
⊢ R x y
have 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
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
Cleared hypotheses: s', hx, hy, this