awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : UniformFun.{u_2, u_1} β (Stream'.Seq α) → UniformFun.{u_2, u_1} β (Stream'.Seq α) :=
  fun (f : UniformFun.{u_2, u_1} β (Stream'.Seq α)) (b : β) ↦
    match (motive := Option (α × γ × β) → Stream'.Seq α) F b with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))
hT : LipschitzWith 2⁻¹ T
f : β → Stream'.Seq α
hf : Function.IsFixedPt T f
b : β
h₁ :
  ∀ (x : Option (α × γ × β)) (hb : F b = x),
    match (motive := Option (α × γ × β) → Prop) x with
    | none =>
      Eq (α := Stream'.Seq α)
        (match (motive := Option (α × γ × β) → Stream'.Seq α) x with
          | none => nil
          | some (a, c, b') => Seq.cons a (op c (f b')) :
          Stream'.Seq α)
        (nil : Stream'.Seq α)
    | some (a, c, b') =>
      (match (motive := Option (α × γ × β) → Stream'.Seq α) x with
        | none => nil
        | some (a, c, b') => Seq.cons a (op c (f b'))) =
        Seq.cons a
          (op c
            (match (motive := Option (α × γ × β) → Stream'.Seq α) F b' with
            | none => nil
            | some (a, c, b') => Seq.cons a (op c (f b'))))
⊢ match (motive := Option (α × γ × β) → Prop) F b with
  | none =>
    Eq (α := Stream'.Seq α)
      (match (motive := Option (α × γ × β) → Stream'.Seq α) F b with
        | none => nil
        | some (a, c, b') => Seq.cons a (op c (f b')) :
        Stream'.Seq α)
      (nil : Stream'.Seq α)
  | some (a, c, b') =>
    (match (motive := Option (α × γ × β) → Stream'.Seq α) F b with
      | none => nil
      | some (a, c, b') => Seq.cons a (op c (f b'))) =
      Seq.cons a
        (op c
          (match (motive := Option (α × γ × β) → Stream'.Seq α) F b' with
          | none => nil
          | some (a, c, b') => Seq.cons a (op c (f b'))))

Tactic:
cases hb : F b with
  | none =>
    simp
  | some v =>
    obtain ⟨a, c, b'⟩ := v
    simp only [cons_eq_cons, true_and]
    congr
    change f b' = T f b'
    rw [hf]

Premises used: Option.some, Stream'.Seq.cons_eq_cons, Option.none, true_and
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
inst : FriendlyOperationClass op
b : β
h : F b = none
⊢ match (motive := Option (α × γ × β) → Prop) F b with
  | none =>
    ⋯.choose (p := fun (f : β → Stream'.Seq α) ↦
        ∀ (b : β),
          match (motive := Option (α × γ × β) → Prop) F b with
          | none => f b = nil
          | some (a, c, b') => f b = Seq.cons a (op c (f b')))
        b =
      nil
  | some (a, c, b') =>
    ⋯.choose (p := fun (f : β → Stream'.Seq α) ↦
        ∀ (b : β),
          match (motive := Option (α × γ × β) → Prop) F b with
          | none => f b = nil
          | some (a, c, b') => f b = Seq.cons a (op c (f b')))
        b =
      Seq.cons a
        (op c
          (⋯.choose (p := fun (f : β → Stream'.Seq α) ↦
            ∀ (b : β),
              match (motive := Option (α × γ × β) → Prop) F b with
              | none => f b = nil
              | some (a, c, b') => f b = Seq.cons a (op c (f b')))
            b'))

Tactic:
have := (FriendlyOperation.exists_fixed_point F op).choose_spec b
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
inst : FriendlyOperationClass op
b : β
h : F b = none
this :
  match (motive := Option (α × γ × β) → Prop) F b with
  | none =>
    ⋯.choose (p := fun (f : β → Stream'.Seq α) ↦
        ∀ (b : β),
          match (motive := Option (α × γ × β) → Prop) F b with
          | none => f b = nil
          | some (a, c, b') => f b = Seq.cons a (op c (f b')))
        b =
      nil
  | some (a, c, b') =>
    ⋯.choose (p := fun (f : β → Stream'.Seq α) ↦
        ∀ (b : β),
          match (motive := Option (α × γ × β) → Prop) F b with
          | none => f b = nil
          | some (a, c, b') => f b = Seq.cons a (op c (f b')))
        b =
      Seq.cons a
        (op c
          (⋯.choose (p := fun (f : β → Stream'.Seq α) ↦
            ∀ (b : β),
              match (motive := Option (α × γ × β) → Prop) F b with
              | none => f b = nil
              | some (a, c, b') => f b = Seq.cons a (op c (f b')))
            b'))
⊢ gcorec F op b = nil

Tactic:
simpa [h] using this
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
inst : FriendlyOperationClass op
b : β
a : α
c : γ
b' : β
h : F b = some (a, c, b')
⊢ match (motive := Option (α × γ × β) → Prop) F b with
  | none =>
    ⋯.choose (p := fun (f : β → Stream'.Seq α) ↦
        ∀ (b : β),
          match (motive := Option (α × γ × β) → Prop) F b with
          | none => f b = nil
          | some (a, c, b') => f b = Seq.cons a (op c (f b')))
        b =
      nil
  | some (a, c, b') =>
    ⋯.choose (p := fun (f : β → Stream'.Seq α) ↦
        ∀ (b : β),
          match (motive := Option (α × γ × β) → Prop) F b with
          | none => f b = nil
          | some (a, c, b') => f b = Seq.cons a (op c (f b')))
        b =
      Seq.cons a
        (op c
          (⋯.choose (p := fun (f : β → Stream'.Seq α) ↦
            ∀ (b : β),
              match (motive := Option (α × γ × β) → Prop) F b with
              | none => f b = nil
              | some (a, c, b') => f b = Seq.cons a (op c (f b')))
            b'))

Tactic:
have := (FriendlyOperation.exists_fixed_point F op).choose_spec b
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
inst : FriendlyOperationClass op
b : β
a : α
c : γ
b' : β
h : F b = some (a, c, b')
this :
  match (motive := Option (α × γ × β) → Prop) F b with
  | none =>
    ⋯.choose (p := fun (f : β → Stream'.Seq α) ↦
        ∀ (b : β),
          match (motive := Option (α × γ × β) → Prop) F b with
          | none => f b = nil
          | some (a, c, b') => f b = Seq.cons a (op c (f b')))
        b =
      nil
  | some (a, c, b') =>
    ⋯.choose (p := fun (f : β → Stream'.Seq α) ↦
        ∀ (b : β),
          match (motive := Option (α × γ × β) → Prop) F b with
          | none => f b = nil
          | some (a, c, b') => f b = Seq.cons a (op c (f b')))
        b =
      Seq.cons a
        (op c
          (⋯.choose (p := fun (f : β → Stream'.Seq α) ↦
            ∀ (b : β),
              match (motive := Option (α × γ × β) → Prop) F b with
              | none => f b = nil
              | some (a, c, b') => f b = Seq.cons a (op c (f b')))
            b'))
⊢ gcorec F op b = Seq.cons a (op c (gcorec F op b'))

Tactic:
simpa [h] using this
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
hd : α
simp : ∀ (s t : Stream'.Seq α), 2⁻¹ * dist s t ≤ dist s t
⊢ FriendlyOperation (Seq.cons hd)

Tactic:
simp only [friendlyOperation_iff_dist_le_dist, dist_cons_cons]

Premises used: Tactic.ComputeAsymptotics.Seq.dist_cons_cons, Tactic.ComputeAsymptotics.Seq.friendlyOperation_iff_dist_le_dist
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
hd : α
x y : Stream'.Seq α
linarith : dist x y < 2⁻¹ * dist x y → 2 / 2 = 1
linarith₁ : dist x y < 2⁻¹ * dist x y → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : dist x y < 2⁻¹ * dist x y → HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : dist x y < 2⁻¹ * dist x y → GT.gt (α := ℝ) 2 0
linarith₄ : dist x y < 2⁻¹ * dist x y → 2 * dist x y - HMul.hMul (α := ℝ) 1 1 * (1 * dist x y) + (0 - dist x y) = 0
⊢ 2⁻¹ * dist x y ≤ dist x y

Tactic:
linarith [dist_nonneg (x := x) (y := y)]

Premises used: dist_nonneg
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
hd : α
x y : Stream'.Seq α
h : 2⁻¹ * dist (op (Seq.cons hd x)).tail (op (Seq.cons hd y)).tail ≤ 2⁻¹ * dist x y
⊢ LT.lt (α := ℝ) 0 2⁻¹

Tactic:
norm_num
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
hd : α
x y : Stream'.Seq α
h : dist (op (Seq.cons hd x)) (op (Seq.cons hd y)) ≤ dist (Seq.cons hd x) (Seq.cons hd y)
rwa :
  ∀ (h : dist (op (Seq.cons hd x)) (op (Seq.cons hd y)) ≤ 2⁻¹ * dist x y),
    (op (Seq.cons hd x)).head = (op (Seq.cons hd y)).head
⊢ dist (op (Seq.cons hd x)).tail (op (Seq.cons hd y)).tail ≤ dist x y

Tactic:
rwa [dist_cons_cons, dist_eq_half_of_head, mul_le_mul_iff_right₀ (by norm_num)] at h

Premises used: Tactic.ComputeAsymptotics.Seq.dist_cons_cons, Tactic.ComputeAsymptotics.Seq.dist_eq_half_of_head, mul_le_mul_iff_right₀
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
hd : α
x y : Stream'.Seq α
h : dist (op (Seq.cons hd x)) (op (Seq.cons hd y)) ≤ 2⁻¹ * dist x y
⊢ dist (op (Seq.cons hd x)) (op (Seq.cons hd y)) ≤ 2⁻¹

Tactic:
grw [dist_le_one x y, mul_one] at h

Premises used: mul_one, Tactic.ComputeAsymptotics.Seq.dist_le_one
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
hd : α
x y : Stream'.Seq α
h : dist (op (Seq.cons hd x)) (op (Seq.cons hd y)) ≤ 2⁻¹
inl :
  ∀ (hx : op (Seq.cons hd x) = nil) (hy : op (Seq.cons hd y) = nil),
    (op (Seq.cons hd x)).head = (op (Seq.cons hd y)).head
inr :
  ∀ (w : α) (w_1 w_2 : Stream'.Seq α) (hx : op (Seq.cons hd x) = Seq.cons w w_1)
    (hy : op (Seq.cons hd y) = Seq.cons w w_2), (op (Seq.cons hd x)).head = (op (Seq.cons hd y)).head
⊢ (op (Seq.cons hd x)).head = (op (Seq.cons hd y)).head

Tactic:
obtain (⟨hx, hy⟩ | ⟨_, _, _, hx, hy⟩) := dist_le_half_iff.mp h

Premises used: Tactic.ComputeAsymptotics.Seq.dist_le_half_iff, Iff.mp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
hd : α
x y : Stream'.Seq α
h : dist (op (Seq.cons hd x)) (op (Seq.cons hd y)) ≤ 2⁻¹
hx : op (Seq.cons hd x) = nil
hy : op (Seq.cons hd y) = nil
⊢ (op (Seq.cons hd x)).head = (op (Seq.cons hd y)).head

Tactic:
simp [hx, hy]
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
hd : α
x y : Stream'.Seq α
h : dist (op (Seq.cons hd x)) (op (Seq.cons hd y)) ≤ 2⁻¹
w : α
w_1 w_2 : Stream'.Seq α
hx : op (Seq.cons hd x) = Seq.cons w w_1
hy : op (Seq.cons hd y) = Seq.cons w w_2
⊢ (op (Seq.cons hd x)).head = (op (Seq.cons hd y)).head

Tactic:
simp [hx, hy]
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
hd : α
h : FriendlyOperation op
simp_rw :
  ∀ (h : ∀ (s t : Stream'.Seq α), dist (op s) (op t) ≤ dist s t) (s t : Stream'.Seq α),
    dist (op (Seq.cons hd s)).tail (op (Seq.cons hd t)).tail ≤ dist s t
⊢ FriendlyOperation.{u_1} (α := α) fun (s : Stream'.Seq α) ↦ (op (Seq.cons hd s)).tail

Tactic:
simp_rw [friendlyOperation_iff_dist_le_dist] at h ⊢

Premises used: Tactic.ComputeAsymptotics.Seq.friendlyOperation_iff_dist_le_dist
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
hd : α
h : ∀ (s t : Stream'.Seq α), dist (op s) (op t) ≤ dist s t
x y : Stream'.Seq α
⊢ dist (op (Seq.cons hd x)) (op (Seq.cons hd y)) ≤ dist (Seq.cons hd x) (Seq.cons hd y)

Tactic:
specialize h (.cons hd x) (.cons hd y)

Premises used: Stream'.Seq.cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
hd : α
x y : Stream'.Seq α
h : dist (op (Seq.cons hd x)) (op (Seq.cons hd y)) ≤ dist (Seq.cons hd x) (Seq.cons hd y)
⊢ dist (op (Seq.cons hd x)).tail (op (Seq.cons hd y)).tail ≤ dist x y

Tactic:
dist_const_tail_cons_tail_le h

Premises used: Tactic.ComputeAsymptotics.Seq.dist_const_tail_cons_tail_le
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
hd : α
x y : Stream'.Seq α
h : dist (op (Seq.cons hd x)) (op (Seq.cons hd y)) ≤ dist (Seq.cons hd x) (Seq.cons hd y)
⊢ dist (op (Seq.cons hd x)).tail (op (Seq.cons hd y)).tail ≤ dist x y

Tactic:
exact dist_const_tail_cons_tail_le h

Premises used: Tactic.ComputeAsymptotics.Seq.dist_const_tail_cons_tail_le
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
a : α
s t : Stream'.Seq α
rw :
  ∀ (h : ∀ (s t : Stream'.Seq α), dist (op s) (op t) ≤ dist s t) {a : α} {s t : Stream'.Seq α},
    (op (Seq.cons a s)).head = (op (Seq.cons a t)).head
⊢ (op (Seq.cons a s)).head = (op (Seq.cons a t)).head

Tactic:
rw [friendlyOperation_iff_dist_le_dist] at h

Premises used: Tactic.ComputeAsymptotics.Seq.friendlyOperation_iff_dist_le_dist
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : ∀ (s t : Stream'.Seq α), dist (op s) (op t) ≤ dist s t
a : α
s t : Stream'.Seq α
⊢ dist (op (Seq.cons a s)) (op (Seq.cons a t)) ≤ dist (Seq.cons a s) (Seq.cons a t)

Tactic:
specialize h (.cons a s) (.cons a t)

Premises used: Stream'.Seq.cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
a : α
s t : Stream'.Seq α
h : dist (op (Seq.cons a s)) (op (Seq.cons a t)) ≤ dist (Seq.cons a s) (Seq.cons a t)
⊢ dist (op (Seq.cons a s)) (op (Seq.cons a t)) ≤ 2⁻¹ * dist s t

Tactic:
simp only [dist_cons_cons] at h

Premises used: Tactic.ComputeAsymptotics.Seq.dist_cons_cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
a : α
s t : Stream'.Seq α
h : dist (op (Seq.cons a s)) (op (Seq.cons a t)) ≤ 2⁻¹ * dist s t
apply : 2⁻¹ * dist s t ≤ 2⁻¹
⊢ dist (op (Seq.cons a s)) (op (Seq.cons a t)) ≤ 2⁻¹

Tactic:
apply h.trans

Premises used: LE.le.trans
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
a : α
s t : Stream'.Seq α
h : dist (op (Seq.cons a s)) (op (Seq.cons a t)) ≤ 2⁻¹ * dist s t
⊢ 2⁻¹ * dist s t ≤ 2⁻¹

Tactic:
simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
a : α
s t : Stream'.Seq α
h : dist (op (Seq.cons a s)) (op (Seq.cons a t)) ≤ 2⁻¹ * dist s t
⊢ dist (op (Seq.cons a s)) (op (Seq.cons a t)) ≤ 2⁻¹

Tactic:
replace h : dist (op (.cons a s)) (op (.cons a t)) ≤ 2⁻¹ := by
    apply h.trans
    simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
a : α
s t : Stream'.Seq α
h : dist (op (Seq.cons a s)) (op (Seq.cons a t)) ≤ 2⁻¹
⊢ op (Seq.cons a s) = nil ∧ op (Seq.cons a t) = nil ∨
    ∃ (hd : α) (s' : Stream'.Seq α) (t' : Stream'.Seq α),
      op (Seq.cons a s) = Seq.cons hd s' ∧ op (Seq.cons a t) = Seq.cons hd t'

Tactic:
rw [dist_le_half_iff] at h

Premises used: Tactic.ComputeAsymptotics.Seq.dist_le_half_iff
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
a : α
s t : Stream'.Seq α
h :
  op (Seq.cons a s) = nil ∧ op (Seq.cons a t) = nil ∨
    ∃ (hd : α) (s' : Stream'.Seq α) (t' : Stream'.Seq α),
      op (Seq.cons a s) = Seq.cons hd s' ∧ op (Seq.cons a t) = Seq.cons hd t'
generalize :
  ∀ (s' : Stream'.Seq α)
    (h :
      s' = nil ∧ op (Seq.cons a t) = nil ∨
        ∃ (hd : α) (s'_1 : Stream'.Seq α) (t' : Stream'.Seq α),
          s' = Seq.cons hd s'_1 ∧ op (Seq.cons a t) = Seq.cons hd t'),
    s'.head = (op (Seq.cons a t)).head
⊢ (op (Seq.cons a s)).head = (op (Seq.cons a t)).head

Tactic:
generalize op (Seq.cons a s) = s' at *

Premises used: Stream'.Seq.cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
a : α
s t s' : Stream'.Seq α
h :
  s' = nil ∧ op (Seq.cons a t) = nil ∨
    ∃ (hd : α) (s'_1 : Stream'.Seq α) (t' : Stream'.Seq α), s' = Seq.cons hd s'_1 ∧ op (Seq.cons a t) = Seq.cons hd t'
generalize :
  ∀ (t' : Stream'.Seq α)
    (h :
      s' = nil ∧ t' = nil ∨
        ∃ (hd : α) (s'_1 : Stream'.Seq α) (t'_1 : Stream'.Seq α), s' = Seq.cons hd s'_1 ∧ t' = Seq.cons hd t'_1),
    s'.head = t'.head
⊢ s'.head = (op (Seq.cons a t)).head

Tactic:
generalize op (Seq.cons a t) = t' at *

Premises used: Stream'.Seq.cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
a : α
s t s' t' : Stream'.Seq α
h :
  s' = nil ∧ t' = nil ∨
    ∃ (hd : α) (s'_1 : Stream'.Seq α) (t'_1 : Stream'.Seq α), s' = Seq.cons hd s'_1 ∧ t' = Seq.cons hd t'_1
inl : Eq.{u_1 + 1} (α := Option α) (Seq.head nil) (Seq.head nil)
inr : ∀ (hd : α) (s_tl t_tl : Stream'.Seq α), (Seq.cons hd s_tl).head = (Seq.cons hd t_tl).head
⊢ s'.head = t'.head

Tactic:
obtain ⟨rfl, rfl⟩ | ⟨hd, s_tl, t_tl, rfl, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
a : α
s t : Stream'.Seq α
⊢ Eq.{u_1 + 1} (α := Option α) (Seq.head nil) (Seq.head nil)

Tactic:
rfl
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
a : α
s t : Stream'.Seq α
hd : α
s_tl t_tl : Stream'.Seq α
⊢ (Seq.cons hd s_tl).head = (Seq.cons hd t_tl).head

Tactic:
rfl
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
s : Stream'.Seq α
unfold :
  (op s).destruct =
    Option.map
      (fun (x : α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation) ↦
        match (motive := α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation → Seq1 α) x with
        | (hd, op') => (hd, (↑op' : Stream'.Seq α → Stream'.Seq α) s.tail))
      (match (motive := Option α → Option (α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation))
        s.head with
      | none =>
        match (motive := Option (Seq1 α) → Option (α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation))
          (op nil).destruct with
        | none => none
        | some (t_hd, t_tl) => some (t_hd, Subtype.mk (p := FriendlyOperation) (fun (x : Stream'.Seq α) ↦ t_tl) ⋯)
      | some s_hd =>
        match (motive := Option (Seq1 α) → Option (α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation))
          (op (Seq.cons s_hd nil)).destruct with
        | none => none
        | some (t_hd, snd) =>
          some
            (t_hd, Subtype.mk (p := FriendlyOperation) (fun (s_tl : Stream'.Seq α) ↦ (op (Seq.cons s_hd s_tl)).tail) ⋯))
⊢ (op s).destruct =
    Option.map
      (fun (x : α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation) ↦
        match (motive := α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation → Seq1 α) x with
        | (hd, op') => (hd, (↑op' : Stream'.Seq α → Stream'.Seq α) s.tail))
      (h.unfold s.head)

Tactic:
unfold unfold

Premises used: Tactic.ComputeAsymptotics.Seq.FriendlyOperation.unfold
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
nil :
  ∀ (t : Stream'.Seq α),
    t.destruct =
      Option.map
        (fun (x : α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation) ↦
          match (motive := α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation → Seq1 α) x with
          | (hd, op') => (hd, (↑op' : Stream'.Seq α → Stream'.Seq α) (Seq.tail Seq.nil)))
        (match (motive := Option α → Option (α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation))
          Seq.head Seq.nil with
        | none =>
          match (motive :=
            Option (Seq1 α) → Option (α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation))
            t.destruct with
          | none => none
          | some (t_hd, t_tl) => some (t_hd, Subtype.mk (p := FriendlyOperation) (fun (x : Stream'.Seq α) ↦ t_tl) ⋯)
        | some s_hd =>
          match (motive :=
            Option (Seq1 α) → Option (α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation))
            (op (Seq.cons s_hd Seq.nil)).destruct with
          | none => none
          | some (t_hd, snd) =>
            some
              (t_hd,
                Subtype.mk (p := FriendlyOperation) (fun (s_tl : Stream'.Seq α) ↦ (op (Seq.cons s_hd s_tl)).tail) ⋯))
⊢ (op Seq.nil).destruct =
    Option.map
      (fun (x : α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation) ↦
        match (motive := α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation → Seq1 α) x with
        | (hd, op') => (hd, (↑op' : Stream'.Seq α → Stream'.Seq α) (Seq.tail Seq.nil)))
      (match (motive := Option α → Option (α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation))
        Seq.head Seq.nil with
      | none =>
        match (motive := Option (Seq1 α) → Option (α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation))
          (op Seq.nil).destruct with
        | none => none
        | some (t_hd, t_tl) => some (t_hd, Subtype.mk (p := FriendlyOperation) (fun (x : Stream'.Seq α) ↦ t_tl) ⋯)
      | some s_hd =>
        match (motive := Option (Seq1 α) → Option (α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation))
          (op (Seq.cons s_hd Seq.nil)).destruct with
        | none => none
        | some (t_hd, snd) =>
          some
            (t_hd, Subtype.mk (p := FriendlyOperation) (fun (s_tl : Stream'.Seq α) ↦ (op (Seq.cons s_hd s_tl)).tail) ⋯))

Tactic:
generalize op nil = t

Premises used: Stream'.Seq.nil
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
⊢ Eq.{u_1 + 1} (α := Option (Seq1 α)) (destruct nil)
    (Option.map
      (fun (x : α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation) ↦
        match (motive := α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation → Seq1 α) x with
        | (hd, op') => (hd, (↑op' : Stream'.Seq α → Stream'.Seq α) (Seq.tail nil)))
      (match (motive := Option α → Option (α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation))
        Seq.head nil with
      | none =>
        match (motive := Option (Seq1 α) → Option (α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation))
          destruct nil with
        | none => none
        | some (t_hd, t_tl) => some (t_hd, Subtype.mk (p := FriendlyOperation) (fun (x : Stream'.Seq α) ↦ t_tl) ⋯)
      | some s_hd =>
        match (motive := Option (Seq1 α) → Option (α × Subtype (α := Stream'.Seq α → Stream'.Seq α) FriendlyOperation))
          (op (Seq.cons s_hd nil)).destruct with
        | none => none
        | some (t_hd, snd) =>
          some
            (t_hd,
              Subtype.mk (p := FriendlyOperation) (fun (s_tl : Stream'.Seq α) ↦ (op (Seq.cons s_hd s_tl)).tail) ⋯)))

Tactic:
simp