awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
⊢ CompleteSpace.{u_1} (Stream' α)

Tactic:
@PiNat.completeSpace _ (fun _ ↦ ⊥) (fun _ ↦ discreteTopology_bot _)

Premises used: Tactic.ComputeAsymptotics.Seq.instMetricSpaceStream'._aux_4, PiNat.completeSpace, Stream'
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
this : IsClosed.{u_1} (X := Stream' (Option α)) fun (x : Stream' (Option α)) ↦ ∀ {n : ℕ}, x n = none → x (n + 1) = none
⊢ CompleteSpace.{u_1} (Stream'.Seq α)

Tactic:
apply IsClosed.completeSpace_coe

Premises used: IsClosed.completeSpace_coe
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
suffices :
  IsClosed.{u_1} (X := Stream' (Option α)) fun (x : Stream' (Option α)) ↦ ∀ {n : ℕ}, x n = none → x (n + 1) = none
⊢ CompleteSpace.{u_1} (Stream'.Seq α)

Tactic:
suffices IsClosed (X := Stream' (Option α))
      (fun x ↦ ∀ {n : ℕ}, x n = none → x (n + 1) = none) by
    apply IsClosed.completeSpace_coe
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
rw :
  ∀ (a : Stream' (Option α)),
    ClusterPt a (Filter.principal fun (x : Stream' (Option α)) ↦ ∀ {n : ℕ}, x n = none → x (n + 1) = none) →
      Membership.mem (γ := Set (Stream' (Option α)))
        (fun (x : Stream' (Option α)) ↦ ∀ {n : ℕ}, x n = none → x (n + 1) = none) a
⊢ IsClosed.{u_1} (X := Stream' (Option α)) fun (x : Stream' (Option α)) ↦ ∀ {n : ℕ}, x n = none → x (n + 1) = none

Tactic:
rw [isClosed_iff_clusterPt]

Premises used: isClosed_iff_clusterPt
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
s : Stream' (Option α)
hs : ClusterPt s (Filter.principal fun (x : Stream' (Option α)) ↦ ∀ {n : ℕ}, x n = none → x (n + 1) = none)
n : ℕ
hn : s n = none
rw :
  ∀ (hs : ∀ U ∈ nhds s, (U ∩ fun (x : Stream' (Option α)) ↦ ∀ {n : ℕ}, x n = none → x (n + 1) = none).Nonempty) {n : ℕ}
    (hn : s n = none), s (n + 1) = none
⊢ s (n + 1) = none

Tactic:
rw [clusterPt_principal_iff] at hs

Premises used: clusterPt_principal_iff
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
s : Stream' (Option α)
hs : ∀ U ∈ nhds s, (U ∩ fun (x : Stream' (Option α)) ↦ ∀ {n : ℕ}, x n = none → x (n + 1) = none).Nonempty
n : ℕ
hn : s n = none
⊢ 0 < (1 / 2) ^ (n + 1)

Tactic:
positivity
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
s : Stream' (Option α)
hs : ∀ U ∈ nhds s, (U ∩ fun (x : Stream' (Option α)) ↦ ∀ {n : ℕ}, x n = none → x (n + 1) = none).Nonempty
n : ℕ
hn : s n = none
obtain :
  ∀ (t : Stream' (Option α)) (hts : t ∈ Metric.ball s ((1 / 2) ^ (n + 1)))
    (ht :
      Membership.mem (γ := Set (Stream' (Option α)))
        (fun (x : Stream' (Option α)) ↦ ∀ {n : ℕ}, x n = none → x (n + 1) = none) t),
    s (n + 1) = none
⊢ s (n + 1) = none

Tactic:
obtain ⟨t, hts, ht⟩ := hs (Metric.ball s ((1 / 2 : ℝ) ^ (n + 1)))
    (Metric.ball_mem_nhds _ (by positivity))

Premises used: HDiv.hDiv, Metric.ball, Metric.ball_mem_nhds, HPow.hPow, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
s : Stream' (Option α)
hs : ∀ U ∈ nhds s, (U ∩ fun (x : Stream' (Option α)) ↦ ∀ {n : ℕ}, x n = none → x (n + 1) = none).Nonempty
n : ℕ
hn : s n = none
t : Stream' (Option α)
hts : dist t s < (1 / 2) ^ (n + 1)
ht :
  Membership.mem (γ := Set (Stream' (Option α)))
    (fun (x : Stream' (Option α)) ↦ ∀ {n : ℕ}, x n = none → x (n + 1) = none) t
⊢ n ≤ n + 1

Tactic:
simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
s : Stream' (Option α)
hs : ∀ U ∈ nhds s, (U ∩ fun (x : Stream' (Option α)) ↦ ∀ {n : ℕ}, x n = none → x (n + 1) = none).Nonempty
n : ℕ
hn : s n = none
t : Stream' (Option α)
hts : dist t s < (1 / 2) ^ (n + 1)
ht :
  Membership.mem (γ := Set (Stream' (Option α)))
    (fun (x : Stream' (Option α)) ↦ ∀ {n : ℕ}, x n = none → x (n + 1) = none) t
⊢ t n = none

Tactic:
rw [← PiNat.apply_eq_of_dist_lt hts (by simp)] at hn

Premises used: PiNat.apply_eq_of_dist_lt
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
s : Stream' (Option α)
hs : ∀ U ∈ nhds s, (U ∩ fun (x : Stream' (Option α)) ↦ ∀ {n : ℕ}, x n = none → x (n + 1) = none).Nonempty
n : ℕ
hn : s n = none
t : Stream' (Option α)
hts : dist t s < (1 / 2) ^ (n + 1)
ht :
  Membership.mem (γ := Set (Stream' (Option α)))
    (fun (x : Stream' (Option α)) ↦ ∀ {n : ℕ}, x n = none → x (n + 1) = none) t
hn₁ : t n = none
⊢ dist t s < (1 / 2) ^ (n + 1)

Tactic:
rw [← PiNat.apply_eq_of_dist_lt hts (by simp)] at hn

Premises used: PiNat.apply_eq_of_dist_lt
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
s : Stream' (Option α)
hs : ∀ U ∈ nhds s, (U ∩ fun (x : Stream' (Option α)) ↦ ∀ {n : ℕ}, x n = none → x (n + 1) = none).Nonempty
n : ℕ
hn : s n = none
t : Stream' (Option α)
hts : dist t s < (1 / 2) ^ (n + 1)
ht :
  Membership.mem (γ := Set (Stream' (Option α)))
    (fun (x : Stream' (Option α)) ↦ ∀ {n : ℕ}, x n = none → x (n + 1) = none) t
hn₁ : t n = none
hts₁ : dist t s < (1 / 2) ^ (n + 1)
⊢ Membership.mem (γ := Set (Stream' (Option α)))
    (fun (x : Stream' (Option α)) ↦ ∀ {n : ℕ}, x n = none → x (n + 1) = none) t

Tactic:
rw [← PiNat.apply_eq_of_dist_lt hts (by simp)] at hn

Premises used: PiNat.apply_eq_of_dist_lt
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
s : Stream' (Option α)
hs : ∀ U ∈ nhds s, (U ∩ fun (x : Stream' (Option α)) ↦ ∀ {n : ℕ}, x n = none → x (n + 1) = none).Nonempty
n : ℕ
t : Stream' (Option α)
hn : t n = none
hts : dist t s < (1 / 2) ^ (n + 1)
ht :
  Membership.mem (γ := Set (Stream' (Option α)))
    (fun (x : Stream' (Option α)) ↦ ∀ {n : ℕ}, x n = none → x (n + 1) = none) t
⊢ n + 1 ≤ n + 1

Tactic:
rfl
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
s : Stream' (Option α)
hs : ∀ U ∈ nhds s, (U ∩ fun (x : Stream' (Option α)) ↦ ∀ {n : ℕ}, x n = none → x (n + 1) = none).Nonempty
n : ℕ
t : Stream' (Option α)
hn : t n = none
hts : dist t s < (1 / 2) ^ (n + 1)
ht :
  Membership.mem (γ := Set (Stream' (Option α)))
    (fun (x : Stream' (Option α)) ↦ ∀ {n : ℕ}, x n = none → x (n + 1) = none) t
rw : t (n + 1) = none
⊢ s (n + 1) = none

Tactic:
rw [← PiNat.apply_eq_of_dist_lt hts (by rfl)]

Premises used: PiNat.apply_eq_of_dist_lt
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
s : Stream' (Option α)
hs : ∀ U ∈ nhds s, (U ∩ fun (x : Stream' (Option α)) ↦ ∀ {n : ℕ}, x n = none → x (n + 1) = none).Nonempty
n : ℕ
t : Stream' (Option α)
hn : t n = none
hts : dist t s < (1 / 2) ^ (n + 1)
ht :
  Membership.mem (γ := Set (Stream' (Option α)))
    (fun (x : Stream' (Option α)) ↦ ∀ {n : ℕ}, x n = none → x (n + 1) = none) t
⊢ t (n + 1) = none

Tactic:
ht hn
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
s : Stream' (Option α)
hs : ∀ U ∈ nhds s, (U ∩ fun (x : Stream' (Option α)) ↦ ∀ {n : ℕ}, x n = none → x (n + 1) = none).Nonempty
n : ℕ
t : Stream' (Option α)
hn : t n = none
hts : dist t s < (1 / 2) ^ (n + 1)
ht :
  Membership.mem (γ := Set (Stream' (Option α)))
    (fun (x : Stream' (Option α)) ↦ ∀ {n : ℕ}, x n = none → x (n + 1) = none) t
⊢ t (n + 1) = none

Tactic:
exact ht hn
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
s t : Stream' α
pos : ∀ (h : s = t), dist s t ≤ 1
neg : ∀ (h : ¬s = t), dist s t ≤ 1
⊢ dist s t ≤ 1

Tactic:
by_cases h : s = t
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
s t : Stream' α
h : s = t
⊢ dist s t ≤ 1

Tactic:
simp [h]
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
s t : Stream' α
h : ¬s = t
neg : (1 / 2) ^ PiNat.firstDiff (E := fun (n : ℕ) ↦ α) s t ≤ 1
⊢ dist s t ≤ 1

Tactic:
rw [PiNat.dist_eq_of_ne h]

Premises used: PiNat.dist_eq_of_ne
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
s t : Stream' α
h : ¬s = t
⊢ (1 / 2) ^ PiNat.firstDiff (E := fun (n : ℕ) ↦ α) s t ≤ 1

Tactic:
bound
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
s t : Stream'.Seq α
⊢ dist s t ≤ 1

Tactic:
PiNat.dist_le_one _ _

Premises used: PiNat.dist_le_one, ite
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
⊢ BoundedSpace.{u_1} (Stream' α)

Tactic:
@PiNat.boundedSpace _ (fun _ ↦ ⊥) (fun _ ↦ discreteTopology_bot _)

Premises used: PiNat.boundedSpace, Stream'
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
⊢ BoundedSpace.{u_1} (Stream'.Seq α)

Tactic:
instBoundedSpaceSubtype

Premises used: Stream'.Seq, instBoundedSpaceSubtype
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
s t : Stream'.Seq α
h : s ≠ t
rw :
  ∃ (n : ℕ),
    (1 / 2) ^ PiNat.firstDiff (E := fun (n : ℕ) ↦ Option α) (↑s : (n : ℕ) → Option α) (↑t : (n : ℕ) → Option α) =
      HPow.hPow (α := ℝ) 2⁻¹ n
⊢ ∃ (n : ℕ), dist s t = HPow.hPow (α := ℝ) 2⁻¹ n

Tactic:
rw [Subtype.dist_eq, PiNat.dist_eq_of_ne (Subtype.coe_ne_coe.mpr h)]

Premises used: Iff.mpr, Subtype.dist_eq, PiNat.dist_eq_of_ne, Subtype.coe_ne_coe
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
s t : Stream'.Seq α
h : s ≠ t
⊢ ∃ (n : ℕ),
    (1 / 2) ^ PiNat.firstDiff (E := fun (n : ℕ) ↦ Option α) (↑s : (n : ℕ) → Option α) (↑t : (n : ℕ) → Option α) =
      HPow.hPow (α := ℝ) 2⁻¹ n

Tactic:
simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
x : α
s t : Stream'.Seq α
pos : ∀ (h : s = t), dist (Seq.cons x s) (Seq.cons x t) = 2⁻¹ * dist s t
neg : ∀ (h : s ≠ t), dist (Seq.cons x s) (Seq.cons x t) = 2⁻¹ * dist s t
⊢ dist (Seq.cons x s) (Seq.cons x t) = 2⁻¹ * dist s t

Tactic:
by_cases! h : s = t
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
x : α
s t : Stream'.Seq α
h : s = t
⊢ dist (Seq.cons x s) (Seq.cons x t) = 2⁻¹ * dist s t

Tactic:
simp [h]
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
⊢ Seq.cons x s ≠ Seq.cons x t

Tactic:
simpa
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
⊢ Seq.cons x s ≠ Seq.cons x t

Tactic:
have h' : cons x s ≠ cons x t := by
    simpa
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
h' : Seq.cons x s ≠ Seq.cons x t
neg :
  (1 / 2) ^
      PiNat.firstDiff (E := fun (n : ℕ) ↦ Option α) (↑(Seq.cons x s) : (n : ℕ) → Option α)
        (↑(Seq.cons x t) : (n : ℕ) → Option α) =
    2⁻¹ * (1 / 2) ^ PiNat.firstDiff (E := fun (n : ℕ) ↦ Option α) (↑s : (n : ℕ) → Option α) (↑t : (n : ℕ) → Option α)
⊢ dist (Seq.cons x s) (Seq.cons x t) = 2⁻¹ * dist s t

Tactic:
rw [Subtype.dist_eq, Subtype.dist_eq, PiNat.dist_eq_of_ne (Subtype.coe_ne_coe.mpr h),
    PiNat.dist_eq_of_ne (Subtype.coe_ne_coe.mpr h')]

Premises used: Iff.mpr, Subtype.dist_eq, PiNat.dist_eq_of_ne, Subtype.coe_ne_coe
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
h' : Seq.cons x s ≠ Seq.cons x t
⊢ 1 / 2 = 2⁻¹

Tactic:
simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
h' : Seq.cons x s ≠ Seq.cons x t
neg :
  HPow.hPow (α := ℝ) 2⁻¹
      (PiNat.firstDiff (E := fun (n : ℕ) ↦ Option α) (↑(Seq.cons x s) : (n : ℕ) → Option α)
        (↑(Seq.cons x t) : (n : ℕ) → Option α)) =
    HPow.hPow (α := ℝ) 2⁻¹
      (PiNat.firstDiff (E := fun (n : ℕ) ↦ Option α) (↑s : (n : ℕ) → Option α) (↑t : (n : ℕ) → Option α) + 1)
⊢ (1 / 2) ^
      PiNat.firstDiff (E := fun (n : ℕ) ↦ Option α) (↑(Seq.cons x s) : (n : ℕ) → Option α)
        (↑(Seq.cons x t) : (n : ℕ) → Option α) =
    2⁻¹ * (1 / 2) ^ PiNat.firstDiff (E := fun (n : ℕ) ↦ Option α) (↑s : (n : ℕ) → Option α) (↑t : (n : ℕ) → Option α)

Tactic:
simp only [show (1 / 2 : ℝ) = 2⁻¹ by simp, ← pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
h' : Seq.cons x s ≠ Seq.cons x t
neg :
  PiNat.firstDiff (E := fun (n : ℕ) ↦ Option α) (↑(Seq.cons x s) : (n : ℕ) → Option α)
      (↑(Seq.cons x t) : (n : ℕ) → Option α) =
    PiNat.firstDiff (E := fun (n : ℕ) ↦ Option α) (↑s : (n : ℕ) → Option α) (↑t : (n : ℕ) → Option α) + 1
⊢ HPow.hPow (α := ℝ) 2⁻¹
      (PiNat.firstDiff (E := fun (n : ℕ) ↦ Option α) (↑(Seq.cons x s) : (n : ℕ) → Option α)
        (↑(Seq.cons x t) : (n : ℕ) → Option α)) =
    HPow.hPow (α := ℝ) 2⁻¹
      (PiNat.firstDiff (E := fun (n : ℕ) ↦ Option α) (↑s : (n : ℕ) → Option α) (↑t : (n : ℕ) → Option α) + 1)

Tactic:
congr
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
h' : Seq.cons x s ≠ Seq.cons x t
neg :
  (if h : some x :: (↑s : Stream' (Option α)) = some x :: (↑t : Stream' (Option α)) then 0
    else
      Nat.find (p := fun (n : ℕ) ↦ ¬(some x :: (↑s : Stream' (Option α))) n = (some x :: (↑t : Stream' (Option α))) n)
        ⋯) =
    Nat.find (p := fun (n : ℕ) ↦ ¬s.get? n = t.get? n) ⋯ + 1
⊢ PiNat.firstDiff (E := fun (n : ℕ) ↦ Option α) (↑(Seq.cons x s) : (n : ℕ) → Option α)
      (↑(Seq.cons x t) : (n : ℕ) → Option α) =
    PiNat.firstDiff (E := fun (n : ℕ) ↦ Option α) (↑s : (n : ℕ) → Option α) (↑t : (n : ℕ) → Option α) + 1

Tactic:
simp only [val_cons, PiNat.firstDiff, ne_eq, Classical.dite_not, Subtype.coe_ne_coe.mpr h,
    not_false_eq_true, ↓reduceDIte, val_eq_get]

Premises used: Classical.dite_not, Iff.mpr, PiNat.firstDiff, reduceDIte, Stream'.Seq.val_eq_get, ne_eq, not_false_eq_true, Stream'.Seq.val_cons, Subtype.coe_ne_coe
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
h' : Seq.cons x s ≠ Seq.cons x t
pos : ∀ (h_if : some x :: (↑s : Stream' (Option α)) = some x :: (↑t : Stream' (Option α))), False
neg :
  ∀ (h_if : ¬some x :: (↑s : Stream' (Option α)) = some x :: (↑t : Stream' (Option α))),
    Nat.find (p := fun (n : ℕ) ↦ ¬(some x :: (↑s : Stream' (Option α))) n = (some x :: (↑t : Stream' (Option α))) n) ⋯ =
      Nat.find (p := fun (n : ℕ) ↦ ¬s.get? n = t.get? n) ⋯ + 1
⊢ (if h : some x :: (↑s : Stream' (Option α)) = some x :: (↑t : Stream' (Option α)) then 0
    else
      Nat.find (p := fun (n : ℕ) ↦ ¬(some x :: (↑s : Stream' (Option α))) n = (some x :: (↑t : Stream' (Option α))) n)
        ⋯) =
    Nat.find (p := fun (n : ℕ) ↦ ¬s.get? n = t.get? n) ⋯ + 1

Tactic:
split_ifs with h_if
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
h' : Seq.cons x s ≠ Seq.cons x t
h_if : some x :: (↑s : Stream' (Option α)) = some x :: (↑t : Stream' (Option α))
pos : ∀ (h' : True), Seq.cons x s = Seq.cons x t
⊢ False

Tactic:
contrapose! h'
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
h_if : some x :: (↑s : Stream' (Option α)) = some x :: (↑t : Stream' (Option α))
h' : True
⊢ Function.Injective.{max 1 (u_1 + 1), u_1 + 1} (α := { f : Stream' (Option α) // f.IsSeq })
    (Subtype.val (p := fun (f : Stream' (Option α)) ↦ f.IsSeq))

Tactic:
Subtype.val_injective

Premises used: Subtype.val_injective
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
h_if : some x :: (↑s : Stream' (Option α)) = some x :: (↑t : Stream' (Option α))
h' : True
pos : (↑(Seq.cons x s) : Stream' (Option α)) = (↑(Seq.cons x t) : Stream' (Option α))
⊢ Seq.cons x s = Seq.cons x t

Tactic:
apply_fun Subtype.val using Subtype.val_injective

Premises used: Subtype.val_injective, Subtype.val
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
h_if : some x :: (↑s : Stream' (Option α)) = some x :: (↑t : Stream' (Option α))
h' : True
⊢ (↑(Seq.cons x s) : Stream' (Option α)) = (↑(Seq.cons x t) : Stream' (Option α))

Tactic:
simpa
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
h' : Seq.cons x s ≠ Seq.cons x t
h_if : ¬some x :: (↑s : Stream' (Option α)) = some x :: (↑t : Stream' (Option α))
⊢ Nat.find (p := fun (n : ℕ) ↦ ¬(some x :: (↑s : Stream' (Option α))) n = (some x :: (↑t : Stream' (Option α))) n) ⋯ =
    Nat.find (p := fun (n : ℕ) ↦
        ¬(some x :: (↑s : Stream' (Option α))) (n + 1) = (some x :: (↑t : Stream' (Option α))) (n + 1)) ⋯ +
      1

Tactic:
Nat.find_comp_succ _ _ _

Premises used: Nat.find_comp_succ
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
h' : Seq.cons x s ≠ Seq.cons x t
h_if : ¬some x :: (↑s : Stream' (Option α)) = some x :: (↑t : Stream' (Option α))
neg : ¬¬(some x :: (↑s : Stream' (Option α))) 0 = (some x :: (↑t : Stream' (Option α))) 0
⊢ Nat.find (p := fun (n : ℕ) ↦ ¬(some x :: (↑s : Stream' (Option α))) n = (some x :: (↑t : Stream' (Option α))) n) ⋯ =
    Nat.find (p := fun (n : ℕ) ↦ ¬s.get? n = t.get? n) ⋯ + 1

Tactic:
convert! Nat.find_comp_succ _ _ _

Premises used: Nat.find_comp_succ
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
h' : Seq.cons x s ≠ Seq.cons x t
h_if : ¬some x :: (↑s : Stream' (Option α)) = some x :: (↑t : Stream' (Option α))
⊢ ¬¬(some x :: (↑s : Stream' (Option α))) 0 = (some x :: (↑t : Stream' (Option α))) 0

Tactic:
simp [Stream'.cons]

Premises used: Stream'.cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
s t : Stream'.Seq α
h : s.head = t.head
nil : ∀ (h : Seq.head Seq.nil = t.head), dist Seq.nil t = 2⁻¹ * dist (Seq.tail Seq.nil) t.tail
cons :
  ∀ (x : α) (s : Stream'.Seq α) (h : (Seq.cons x s).head = t.head),
    dist (Seq.cons x s) t = 2⁻¹ * dist (Seq.cons x s).tail t.tail
⊢ dist s t = 2⁻¹ * dist s.tail t.tail

Tactic:
cases s
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
t : Stream'.Seq α
h : Seq.head Seq.nil = t.head
nil :
  ∀ (h : Eq.{u_1 + 1} (α := Option α) (Seq.head Seq.nil) (Seq.head Seq.nil)),
    dist.{u_1} (α := Stream'.Seq α) Seq.nil Seq.nil =
      2⁻¹ * dist.{u_1} (α := Stream'.Seq α) (Seq.tail Seq.nil) (Seq.tail Seq.nil)
nil₁ :
  ∀ (x : α) (s : Stream'.Seq α) (h : Seq.head Seq.nil = (Seq.cons x s).head),
    dist Seq.nil (Seq.cons x s) = 2⁻¹ * dist (Seq.tail Seq.nil) (Seq.cons x s).tail
⊢ dist Seq.nil t = 2⁻¹ * dist (Seq.tail Seq.nil) t.tail

Tactic:
cases t
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
t : Stream'.Seq α
x : α
s : Stream'.Seq α
h : (Seq.cons x s).head = t.head
cons :
  ∀ (h : (Seq.cons x s).head = Seq.head nil), dist (Seq.cons x s) nil = 2⁻¹ * dist (Seq.cons x s).tail (Seq.tail nil)
cons₁ :
  ∀ (x_1 : α) (s_1 : Stream'.Seq α) (h : (Seq.cons x s).head = (Seq.cons x_1 s_1).head),
    dist (Seq.cons x s) (Seq.cons x_1 s_1) = 2⁻¹ * dist (Seq.cons x s).tail (Seq.cons x_1 s_1).tail
⊢ dist (Seq.cons x s) t = 2⁻¹ * dist (Seq.cons x s).tail t.tail

Tactic:
cases t
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
h : Eq.{u_1 + 1} (α := Option α) (Seq.head nil) (Seq.head nil)
⊢ True

Tactic:
simp at h
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
x : α
s : Stream'.Seq α
h : Seq.head nil = (Seq.cons x s).head
⊢ dist nil (Seq.cons x s) = 2⁻¹ * dist (Seq.tail nil) (Seq.cons x s).tail

Tactic:
simp at h
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
x : α
s : Stream'.Seq α
h : (Seq.cons x s).head = Seq.head nil
⊢ dist (Seq.cons x s) nil = 2⁻¹ * dist (Seq.cons x s).tail (Seq.tail nil)

Tactic:
simp at h
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
x : α
s : Stream'.Seq α
x_1 : α
s_1 : Stream'.Seq α
h : (Seq.cons x s).head = (Seq.cons x_1 s_1).head
⊢ x = x_1

Tactic:
simp at h
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
h : True
⊢ dist.{u_1} (α := Stream'.Seq α) nil nil = 2⁻¹ * dist.{u_1} (α := Stream'.Seq α) (Seq.tail nil) (Seq.tail nil)

Tactic:
simp [h]
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
x : α
s : Stream'.Seq α
x_1 : α
s_1 : Stream'.Seq α
h : x = x_1
⊢ dist (Seq.cons x s) (Seq.cons x_1 s_1) = 2⁻¹ * dist (Seq.cons x s).tail (Seq.cons x_1 s_1).tail

Tactic:
simp [h]
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
s t : Stream'.Seq α
h : s.head ≠ t.head
rw : (1 / 2) ^ PiNat.firstDiff (E := fun (n : ℕ) ↦ Option α) (↑s : Stream' (Option α)) (↑t : Stream' (Option α)) = 1
rw₁ : (↑s : Stream' (Option α)) ≠ (↑t : Stream' (Option α))
⊢ dist s t = 1

Tactic:
rw [Subtype.dist_eq, PiNat.dist_eq_of_ne]

Premises used: Subtype.dist_eq, PiNat.dist_eq_of_ne
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
s t : Stream'.Seq α
h : s.head ≠ t.head
⊢ HPow.hPow (β := ℕ) (1 / 2) 0 = 1

Tactic:
pow_zero _

Premises used: pow_zero
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
s t : Stream'.Seq α
h : s.head ≠ t.head
h₁ : PiNat.firstDiff (E := fun (n : ℕ) ↦ Option α) (↑s : Stream' (Option α)) (↑t : Stream' (Option α)) = 0
⊢ (1 / 2) ^ PiNat.firstDiff (E := fun (n : ℕ) ↦ Option α) (↑s : Stream' (Option α)) (↑t : Stream' (Option α)) = 1

Tactic:
convert! pow_zero _

Premises used: pow_zero
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
s t : Stream'.Seq α
h : s.head ≠ t.head
h₁ :
  ∀ (h : ¬(↑s : Stream' (Option α)) = (↑t : Stream' (Option α))),
    ¬(↑s : Stream' (Option α)) 0 = (↑t : Stream' (Option α)) 0
⊢ PiNat.firstDiff (E := fun (n : ℕ) ↦ Option α) (↑s : Stream' (Option α)) (↑t : Stream' (Option α)) = 0

Tactic:
simp only [PiNat.firstDiff, ne_eq, Classical.dite_not, dite_eq_left_iff,
      Nat.find_eq_zero]

Premises used: Classical.dite_not, PiNat.firstDiff, Nat.find_eq_zero, ne_eq, dite_eq_left_iff
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
s t : Stream'.Seq α
h : s.head ≠ t.head
h' : ¬(↑s : Stream' (Option α)) = (↑t : Stream' (Option α))
⊢ ¬(↑s : Stream' (Option α)) 0 = (↑t : Stream' (Option α)) 0

Tactic:
simpa [Stream'.cons]

Premises used: Stream'.cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
s t : Stream'.Seq α
h : s.head ≠ t.head
rw : s ≠ t
⊢ (↑s : Stream' (Option α)) ≠ (↑t : Stream' (Option α))

Tactic:
rw [Subtype.coe_ne_coe]

Premises used: Subtype.coe_ne_coe
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
s t : Stream'.Seq α
h : s.head ≠ t.head
contrapose : ∀ (h : s = t), s.head = t.head
⊢ s ≠ t

Tactic:
contrapose h
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
s t : Stream'.Seq α
h : s = t
⊢ s.head = t.head

Tactic:
simp [h]
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
x y : α
s t : Stream'.Seq α
h : x ≠ y
h₁ : (Seq.cons x s).head ≠ (Seq.cons y t).head
⊢ dist (Seq.cons x s) (Seq.cons y t) = 1

Tactic:
apply dist_eq_one_of_head

Premises used: Tactic.ComputeAsymptotics.Seq.dist_eq_one_of_head