awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
x : α
n : ℕ
⊢ Option.map (Prod.mk (n + 1)) (s.get? n) = Option.map (Prod.map Nat.succ id ∘ Prod.mk n) (s.get? n)

Tactic:
congr
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
h :
  ∀ (n : ℕ), (zipWith g (map f₁ s₁) (map f₂ s₂)).get? n = get? (zipWith (fun (a : α) (b : β) ↦ g (f₁ a) (f₂ b)) s₁ s₂) n
⊢ zipWith g (map f₁ s₁) (map f₂ s₂) = zipWith (fun (a : α) (b : β) ↦ g (f₁ a) (f₂ b)) s₁ s₂

Tactic:
ext1 n
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
h :
  Option.map₂ g (Option.map f₁ (s₁.get? n)) (Option.map f₂ (s₂.get? n)) =
    Option.map₂ (fun (a : α) (b : β) ↦ g (f₁ a) (f₂ b)) (s₁.get? n) (s₂.get? n)
⊢ (zipWith g (map f₁ s₁) (map f₂ s₂)).get? n = get? (zipWith (fun (a : α) (b : β) ↦ g (f₁ a) (f₂ b)) s₁ s₂) n

Tactic:
simp only [get?_zipWith, map_get?]

Premises used: Stream'.Seq.get?_zipWith, Stream'.Seq.map_get?
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
h :
  Option.map₂ g (Option.map f₁ none) (Option.map f₂ (s₂.get? n)) =
    Option.map₂ (fun (a : α) (b : β) ↦ g (f₁ a) (f₂ b)) none (s₂.get? n)
h₁ :
  ∀ (val : α),
    Option.map₂ g (Option.map f₁ (some val)) (Option.map f₂ (s₂.get? n)) =
      Option.map₂ (fun (a : α) (b : β) ↦ g (f₁ a) (f₂ b)) (some val) (s₂.get? n)
⊢ Option.map₂ g (Option.map f₁ (s₁.get? n)) (Option.map f₂ (s₂.get? n)) =
    Option.map₂ (fun (a : α) (b : β) ↦ g (f₁ a) (f₂ b)) (s₁.get? n) (s₂.get? n)

Tactic:
cases s₁.get? n

Premises used: Stream'.Seq.get?
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
h :
  Option.map₂ g (Option.map f₁ none) (Option.map f₂ none) =
    Option.map₂ (fun (a : α) (b : β) ↦ g (f₁ a) (f₂ b)) none none
h₁ :
  ∀ (val : β),
    Option.map₂ g (Option.map f₁ none) (Option.map f₂ (some val)) =
      Option.map₂ (fun (a : α) (b : β) ↦ g (f₁ a) (f₂ b)) none (some val)
⊢ Option.map₂ g (Option.map f₁ none) (Option.map f₂ (s₂.get? n)) =
    Option.map₂ (fun (a : α) (b : β) ↦ g (f₁ a) (f₂ b)) none (s₂.get? n)

Tactic:
cases s₂.get? n

Premises used: Stream'.Seq.get?
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
val : α
h :
  Option.map₂ g (Option.map f₁ (some val)) (Option.map f₂ none) =
    Option.map₂ (fun (a : α) (b : β) ↦ g (f₁ a) (f₂ b)) (some val) none
h₁ :
  ∀ (val_1 : β),
    Option.map₂ g (Option.map f₁ (some val)) (Option.map f₂ (some val_1)) =
      Option.map₂ (fun (a : α) (b : β) ↦ g (f₁ a) (f₂ b)) (some val) (some val_1)
⊢ Option.map₂ g (Option.map f₁ (some val)) (Option.map f₂ (s₂.get? n)) =
    Option.map₂ (fun (a : α) (b : β) ↦ g (f₁ a) (f₂ b)) (some val) (s₂.get? n)

Tactic:
cases s₂.get? n

Premises used: Stream'.Seq.get?
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
⊢ Option.map₂ g (Option.map f₁ none) (Option.map f₂ none) =
    Option.map₂ (fun (a : α) (b : β) ↦ g (f₁ a) (f₂ b)) none none

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
val : β
⊢ Option.map₂ g (Option.map f₁ none) (Option.map f₂ (some val)) =
    Option.map₂ (fun (a : α) (b : β) ↦ g (f₁ a) (f₂ b)) none (some val)

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
val : α
⊢ Option.map₂ g (Option.map f₁ (some val)) (Option.map f₂ none) =
    Option.map₂ (fun (a : α) (b : β) ↦ g (f₁ a) (f₂ b)) (some val) none

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
val : α
val_1 : β
⊢ Option.map₂ g (Option.map f₁ (some val)) (Option.map f₂ (some val_1)) =
    Option.map₂ (fun (a : α) (b : β) ↦ g (f₁ a) (f₂ b)) (some val) (some val_1)

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
α' : Type u'
s₁ : Seq α
s₂ : Seq β
f : α → α'
g : α' → β → γ
⊢ zipWith g (map f s₁) (map id s₂) = zipWith (fun (a : α) (b : β) ↦ g (f a) (id b)) s₁ s₂

Tactic:
zipWith_map _ _ _ (@id β) _

Premises used: id, Stream'.Seq.zipWith_map
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
α' : Type u'
s₁ : Seq α
s₂ : Seq β
f : α → α'
g : α' → β → γ
h : s₂ = map id s₂
⊢ zipWith g (map f s₁) s₂ = zipWith (fun (a : α) (b : β) ↦ g (f a) b) s₁ s₂

Tactic:
convert! zipWith_map _ _ _ (@id β) _

Premises used: id, Stream'.Seq.zipWith_map
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
α' : Type u'
s₁ : Seq α
s₂ : Seq β
f : α → α'
g : α' → β → γ
⊢ s₂ = map id s₂

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f : β → β'
g : α → β' → γ
⊢ zipWith g (map id s₁) (map f s₂) = zipWith (fun (a : α) (b : β) ↦ g (id a) (f b)) s₁ s₂

Tactic:
zipWith_map _ _ (@id α) _ _

Premises used: id, Stream'.Seq.zipWith_map
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f : β → β'
g : α → β' → γ
h : s₁ = map id s₁
⊢ zipWith g s₁ (map f s₂) = zipWith (fun (a : α) (b : β) ↦ g a (f b)) s₁ s₂

Tactic:
convert! zipWith_map _ _ (@id α) _ _

Premises used: id, Stream'.Seq.zipWith_map
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
γ : Type w
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f : β → β'
g : α → β' → γ
⊢ s₁ = map id s₁

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
h : ∀ (n : ℕ), ((map f₁ s₁).zip (map f₂ s₂)).get? n = (map (Prod.map f₁ f₂) (s₁.zip s₂)).get? n
⊢ (map f₁ s₁).zip (map f₂ s₂) = map (Prod.map f₁ f₂) (s₁.zip s₂)

Tactic:
ext1 n
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
h :
  Option.map₂ Prod.mk (Option.map f₁ (s₁.get? n)) (Option.map f₂ (s₂.get? n)) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk (s₁.get? n) (s₂.get? n))
⊢ ((map f₁ s₁).zip (map f₂ s₂)).get? n = (map (Prod.map f₁ f₂) (s₁.zip s₂)).get? n

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
h :
  Option.map₂ Prod.mk (Option.map f₁ none) (Option.map f₂ (s₂.get? n)) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk none (s₂.get? n))
h₁ :
  ∀ (val : α),
    Option.map₂ Prod.mk (Option.map f₁ (some val)) (Option.map f₂ (s₂.get? n)) =
      Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk (some val) (s₂.get? n))
⊢ Option.map₂ Prod.mk (Option.map f₁ (s₁.get? n)) (Option.map f₂ (s₂.get? n)) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk (s₁.get? n) (s₂.get? n))

Tactic:
cases s₁.get? n

Premises used: Stream'.Seq.get?
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
h :
  Option.map₂ Prod.mk (Option.map f₁ none) (Option.map f₂ none) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk none none)
h₁ :
  ∀ (val : β),
    Option.map₂ Prod.mk (Option.map f₁ none) (Option.map f₂ (some val)) =
      Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk none (some val))
⊢ Option.map₂ Prod.mk (Option.map f₁ none) (Option.map f₂ (s₂.get? n)) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk none (s₂.get? n))

Tactic:
cases s₂.get? n

Premises used: Stream'.Seq.get?
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
val : α
h :
  Option.map₂ Prod.mk (Option.map f₁ (some val)) (Option.map f₂ none) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk (some val) none)
h₁ :
  ∀ (val_1 : β),
    Option.map₂ Prod.mk (Option.map f₁ (some val)) (Option.map f₂ (some val_1)) =
      Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk (some val) (some val_1))
⊢ Option.map₂ Prod.mk (Option.map f₁ (some val)) (Option.map f₂ (s₂.get? n)) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk (some val) (s₂.get? n))

Tactic:
cases s₂.get? n

Premises used: Stream'.Seq.get?
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
⊢ Option.map₂ Prod.mk (Option.map f₁ none) (Option.map f₂ none) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk none none)

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
val : β
⊢ Option.map₂ Prod.mk (Option.map f₁ none) (Option.map f₂ (some val)) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk none (some val))

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
val : α
⊢ Option.map₂ Prod.mk (Option.map f₁ (some val)) (Option.map f₂ none) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk (some val) none)

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
val : α
val_1 : β
⊢ Option.map₂ Prod.mk (Option.map f₁ (some val)) (Option.map f₂ (some val_1)) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk (some val) (some val_1))

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
α' : Type u'
s₁ : Seq α
s₂ : Seq β
f : α → α'
⊢ (map f s₁).zip (map id s₂) = map (Prod.map f id) (s₁.zip s₂)

Tactic:
zip_map _ _ _ _

Premises used: Stream'.Seq.zip_map
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
α' : Type u'
s₁ : Seq α
s₂ : Seq β
f : α → α'
h : s₂ = map id s₂
⊢ (map f s₁).zip s₂ = map (Prod.map f id) (s₁.zip s₂)

Tactic:
convert! zip_map _ _ _ _

Premises used: Stream'.Seq.zip_map
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
α' : Type u'
s₁ : Seq α
s₂ : Seq β
f : α → α'
⊢ s₂ = map id s₂

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f : β → β'
⊢ (map id s₁).zip (map f s₂) = map (Prod.map id f) (s₁.zip s₂)

Tactic:
zip_map _ _ _ _

Premises used: Stream'.Seq.zip_map
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f : β → β'
h : s₁ = map id s₁
⊢ s₁.zip (map f s₂) = map (Prod.map id f) (s₁.zip s₂)

Tactic:
convert! zip_map _ _ _ _

Premises used: Stream'.Seq.zip_map
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f : β → β'
⊢ s₁ = map id s₁

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
init : β
f : β → α → β
⊢ (have f : Prod.{v, u} β (Seq α) → Option (β × Prod.{v, u} β (Seq α)) := fun (x : Prod.{v, u} β (Seq α)) ↦
      match (motive := Prod.{v, u} β (Seq α) → Option (β × Prod.{v, u} β (Seq α))) x with
      | (acc, x) =>
        match (motive := Option (Seq1 α) → Option (β × Prod.{v, u} β (Seq α))) x.destruct with
        | none => none
        | some (x, s) => some (f acc x, f acc x, s);
    cons init (corec f (init, nil))) =
    cons init nil

Tactic:
simp [corec_nil]

Premises used: Stream'.Seq.corec_nil
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
init : β
f : β → α → β
x : α
s : Seq α
e_s :
  corec
      (fun (x : Prod.{v, u} β (Seq α)) ↦
        match (motive := Option (Seq1 α) → Option (β × Prod.{v, u} β (Seq α))) x.2.destruct with
        | none => none
        | some (x_1, s) => some (f x.1 x_1, f x.1 x_1, s))
      (init, cons x s) =
    cons (f init x)
      (corec
        (fun (x : Prod.{v, u} β (Seq α)) ↦
          match (motive := Option (Seq1 α) → Option (β × Prod.{v, u} β (Seq α))) x.2.destruct with
          | none => none
          | some (x_1, s) => some (f x.1 x_1, f x.1 x_1, s))
        (f init x, s))
⊢ cons init
      (corec
        (fun (x : Prod.{v, u} β (Seq α)) ↦
          match (motive := Option (Seq1 α) → Option (β × Prod.{v, u} β (Seq α))) x.2.destruct with
          | none => none
          | some (x_1, s) => some (f x.1 x_1, f x.1 x_1, s))
        (init, cons x s)) =
    cons init
      (cons (f init x)
        (corec
          (fun (x : Prod.{v, u} β (Seq α)) ↦
            match (motive := Option (Seq1 α) → Option (β × Prod.{v, u} β (Seq α))) x.2.destruct with
            | none => none
            | some (x_1, s) => some (f x.1 x_1, f x.1 x_1, s))
          (f init x, s)))

Tactic:
congr
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
init : β
f : β → α → β
x : α
s : Seq α
e_s :
  (match (motive := Option (Seq1 α) → Option (β × Prod.{v, u} β (Seq α))) (init, cons x s).2.destruct with
    | none => none
    | some (x_1, s_1) => some (f (init, cons x s).1 x_1, f (init, cons x s).1 x_1, s_1)) =
    some (f init x, f init x, s)
⊢ corec
      (fun (x : Prod.{v, u} β (Seq α)) ↦
        match (motive := Option (Seq1 α) → Option (β × Prod.{v, u} β (Seq α))) x.2.destruct with
        | none => none
        | some (x_1, s) => some (f x.1 x_1, f x.1 x_1, s))
      (init, cons x s) =
    cons (f init x)
      (corec
        (fun (x : Prod.{v, u} β (Seq α)) ↦
          match (motive := Option (Seq1 α) → Option (β × Prod.{v, u} β (Seq α))) x.2.destruct with
          | none => none
          | some (x_1, s) => some (f x.1 x_1, f x.1 x_1, s))
        (f init x, s))

Tactic:
rw [corec_cons]

Premises used: Stream'.Seq.corec_cons
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
init : β
f : β → α → β
x : α
s : Seq α
⊢ (match (motive := Option (Seq1 α) → Option (β × Prod.{v, u} β (Seq α))) (init, cons x s).2.destruct with
    | none => none
    | some (x_1, s_1) => some (f (init, cons x s).1 x_1, f (init, cons x s).1 x_1, s_1)) =
    some (f init x, f init x, s)

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
β : Type v
init : β
f : β → α → β
s : Seq α
⊢ (s.fold init f).head = some init

Tactic:
simp [fold]

Premises used: Stream'.Seq.fold
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
f : α → α
s : Seq α
n m : ℕ
simp : (if m = n then Option.map f (s.get? n) else s.get? m) = if m = n then Option.map f (s.get? m) else s.get? m
⊢ (s.update n f).get? m = if m = n then Option.map f (s.get? m) else s.get? m

Tactic:
simp [update, Function.update]

Premises used: Function.update, Stream'.Seq.update
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
f : α → α
s : Seq α
n m : ℕ
pos : ∀ (h_if : m = n), Option.map f (s.get? n) = Option.map f (s.get? m)
neg : ∀ (h_if : ¬m = n), s.get? m = s.get? m
⊢ (if m = n then Option.map f (s.get? n) else s.get? m) = if m = n then Option.map f (s.get? m) else s.get? m

Tactic:
split_ifs with h_if
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
f : α → α
s : Seq α
n m : ℕ
h_if : m = n
⊢ Option.map f (s.get? n) = Option.map f (s.get? m)

Tactic:
simp [h_if]
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
f : α → α
s : Seq α
n m : ℕ
h_if : ¬m = n
⊢ s.get? m = s.get? m

Tactic:
rfl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
f : α → α
n : ℕ
h : ∀ (m : ℕ), (update nil n f).get? m = get? nil m
⊢ update nil n f = nil

Tactic:
ext1 m
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
f : α → α
n m : ℕ
⊢ (update nil n f).get? m = get? nil m

Tactic:
simp [get?_update]

Premises used: Stream'.Seq.get?_update
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
n : ℕ
x : α
⊢ set nil n x = nil

Tactic:
update_nil _ _

Premises used: Stream'.Seq.update_nil, Stream'.Seq.set
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
hd : α
tl : Seq α
f : α → α
h : ∀ (n : ℕ), ((cons hd tl).update 0 f).get? n = (cons (f hd) tl).get? n
⊢ (cons hd tl).update 0 f = cons (f hd) tl

Tactic:
ext1 n
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
hd : α
tl : Seq α
f : α → α
n : ℕ
h : ((cons hd tl).update 0 f).get? 0 = (cons (f hd) tl).get? 0
h₁ : ∀ (n : ℕ), ((cons hd tl).update 0 f).get? (n + 1) = (cons (f hd) tl).get? (n + 1)
⊢ ((cons hd tl).update 0 f).get? n = (cons (f hd) tl).get? n

Tactic:
cases n
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
hd : α
tl : Seq α
f : α → α
⊢ ((cons hd tl).update 0 f).get? 0 = (cons (f hd) tl).get? 0

Tactic:
simp [get?_update]

Premises used: Stream'.Seq.get?_update
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
hd : α
tl : Seq α
f : α → α
n : ℕ
⊢ ((cons hd tl).update 0 f).get? (n + 1) = (cons (f hd) tl).get? (n + 1)

Tactic:
simp [get?_update]

Premises used: Stream'.Seq.get?_update
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
hd : α
tl : Seq α
hd' : α
⊢ (cons hd tl).set 0 hd' = cons hd' tl

Tactic:
update_cons_zero _ _ _

Premises used: Stream'.Seq.update_cons_zero, Stream'.Seq.set
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
hd : α
tl : Seq α
f : α → α
n : ℕ
h : ∀ (n_1 : ℕ), ((cons hd tl).update (n + 1) f).get? n_1 = (cons hd (tl.update n f)).get? n_1
⊢ (cons hd tl).update (n + 1) f = cons hd (tl.update n f)

Tactic:
ext1 n
-- Module: Mathlib.Data.Seq.Basic
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
h₁ : ∀ (n : ℕ), ((cons hd tl).update (n_1 + 1) f).get? (n + 1) = (cons hd (tl.update n_1 f)).get? (n + 1)
⊢ ((cons hd tl).update (n_1 + 1) f).get? n = (cons hd (tl.update n_1 f)).get? n

Tactic:
cases n
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
hd : α
tl : Seq α
f : α → α
n : ℕ
⊢ ((cons hd tl).update (n + 1) f).get? 0 = (cons hd (tl.update n f)).get? 0

Tactic:
simp [get?_update]

Premises used: Stream'.Seq.get?_update
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
hd : α
tl : Seq α
f : α → α
n n_1 : ℕ
⊢ ((cons hd tl).update (n + 1) f).get? (n_1 + 1) = (cons hd (tl.update n f)).get? (n_1 + 1)

Tactic:
simp [get?_update]

Premises used: Stream'.Seq.get?_update
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
hd x : α
tl : Seq α
n : ℕ
⊢ (cons hd tl).set (n + 1) x = cons hd (tl.set n x)

Tactic:
update_cons_succ _ _ _ _

Premises used: Stream'.Seq.set, Stream'.Seq.update_cons_succ
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
x : α
s : Seq α
n : ℕ
h_not_terminated : ¬s.TerminatedAt n
⊢ (s.set n x).get? n = some x

Tactic:
simpa [set, update, ← Option.ne_none_iff_exists'] using h_not_terminated

Premises used: Stream'.Seq.update, Option.ne_none_iff_exists', Stream'.Seq.set
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
x : α
s : Seq α
n : ℕ
h_terminated : s.TerminatedAt n
⊢ (s.set n x).get? n = none

Tactic:
simpa [set, get?_update] using h_terminated

Premises used: Stream'.Seq.set, Stream'.Seq.get?_update
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
x : α
s : Seq α
m n : ℕ
h : n ≠ m
⊢ (s.set m x).get? n = s.get? n

Tactic:
simp [set, get?_update, h]

Premises used: Stream'.Seq.set, Stream'.Seq.get?_update
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
x : α
s : Seq α
m n : ℕ
h : m < n
h₁ : ∀ (i : ℕ), ((s.set m x).drop n).get? i = (s.drop n).get? i
⊢ (s.set m x).drop n = s.drop n

Tactic:
ext1 i
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
x : α
s : Seq α
m n : ℕ
h : m < n
i : ℕ
⊢ n + i ≠ m

Tactic:
lia
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
x : α
s : Seq α
m n : ℕ
h : m < n
i : ℕ
⊢ ((s.set m x).drop n).get? i = (s.drop n).get? i

Tactic:
simp [get?_set_of_ne _ _ (show n + i ≠ m by lia)]

Premises used: Stream'.Seq.get?_set_of_ne
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
p : α → Prop
hd : α
tl : Seq α
h_hd : p hd
h_tl : ∀ x ∈ tl, p x
simp : p hd ∧ ∀ a ∈ tl, p a
⊢ ∀ x ∈ cons hd tl, p x

Tactic:
simp only [mem_cons_iff, forall_eq_or_imp] at *

Premises used: forall_eq_or_imp, Stream'.Seq.mem_cons_iff
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
p : α → Prop
hd : α
tl : Seq α
h_hd : p hd
h_tl : ∀ x ∈ tl, p x
⊢ p hd ∧ ∀ a ∈ tl, p a

Tactic:
⟨h_hd, h_tl⟩

Premises used: And.intro
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
p : α → Prop
hd : α
tl : Seq α
h_hd : p hd
h_tl : ∀ x ∈ tl, p x
⊢ p hd ∧ ∀ a ∈ tl, p a

Tactic:
exact ⟨h_hd, h_tl⟩
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
p : α → Prop
s : Seq α
h : ∀ x ∈ s, p x
n : ℕ
x : α
hx : s.get? n = some x
⊢ p x

Tactic:
h _ (get?_mem hx)

Premises used: Stream'.Seq.get?_mem
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
p : α → Prop
s : Seq α
h : ∀ x ∈ s, p x
n : ℕ
x : α
hx : s.get? n = some x
⊢ p x

Tactic:
exact h _ (get?_mem hx)

Premises used: Stream'.Seq.get?_mem
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
p : α → Prop
s : Seq α
h : ∀ (n : ℕ) (x : α), s.get? n = some x → p x
⊢ ∀ (x : α), (∃ (i : ℕ), some x = s.get? i) → p x

Tactic:
grind
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (cons hd tl) → motive tl
⊢ motive (s.drop 0)

Tactic:
simpa
-- Module: Mathlib.Data.Seq.Basic
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)
succ : motive (s.drop m).tail
⊢ motive (s.drop (m + 1))

Tactic:
simp only [drop]

Premises used: Stream'.Seq.drop
-- Module: Mathlib.Data.Seq.Basic
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)
succ : ∀ (t : Seq α) (ih : motive t), motive t.tail
⊢ motive (s.drop m).tail

Tactic:
generalize s.drop m = t at *

Premises used: Stream'.Seq.drop
-- Module: Mathlib.Data.Seq.Basic
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)
succ₁ : ∀ (x : α) (s : Seq α) (ih : motive (cons x s)), motive (cons x s).tail
⊢ motive t.tail

Tactic:
cases t
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (cons hd tl) → motive tl
m : ℕ
ih : motive nil
⊢ motive (tail nil)

Tactic:
simpa
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (cons hd tl) → motive tl
m : ℕ
x : α
s_1 : Seq α
ih : motive (cons x s_1)
⊢ motive (cons x s_1).tail

Tactic:
step _ _ ih
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (cons hd tl) → motive tl
m : ℕ
x : α
s_1 : Seq α
ih : motive (cons x s_1)
⊢ motive (cons x s_1).tail

Tactic:
exact step _ _ ih
-- Module: Mathlib.Data.Seq.Basic
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)
succ : ∀ (m : ℕ) (ih : motive (s.drop m)), motive (s.drop (m + 1))
⊢ motive (s.drop n)

Tactic:
induction n with
  | zero => simpa
  | succ m ih =>
    simp only [drop]
    generalize s.drop m = t at *
    cases t
    · simpa
    · exact step _ _ ih

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
h : ∀ (n : ℕ) (x : α), s.get? n = some x → p x
⊢ ∀ x ∈ s, p x

Tactic:
apply all_of_get

Premises used: Stream'.Seq.all_of_get
-- 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 : ℕ
⊢ motive (s.drop n)

Tactic:
have := all_coind_drop_motive motive base (fun hd tl ih ↦ (step hd tl ih).right) n