awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis (goal)
Goal:
basis : Basis
h : WellFormedBasis basis
nil : ∀ (h : WellFormedBasis []), ∀ᶠ (x : ℝ) in atTop, ∀ (f : ℝ → ℝ), Membership.mem (γ := Basis) [] f → 0 < f x
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ f ∈ basis, 0 < f x
have cons : ∀ (hd : ℝ → ℝ) (tl : List (ℝ → ℝ)) (ih : ∀ (h : WellFormedBasis tl), ∀ᶠ (x : ℝ) in atTop, ∀ f ∈ tl, 0 < f x)
  (h : WellFormedBasis (hd :: tl)), ∀ᶠ (x : ℝ) in atTop, ∀ f ∈ hd :: tl, 0 < f x
Tactic: induction basis with
  | nil => simp
  | cons hd tl ih =>
    simp only [WellFormedBasis, List.pairwise_cons, List.mem_cons, forall_eq_or_imp] at h
    simp only [List.mem_cons, forall_eq_or_imp]
    exact (h.right.left.eventually <| eventually_gt_atTop 0).and (ih (by tauto))
Cleared hypotheses: basis, h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis (goal)
Goal:
hd : ℝ → ℝ
tl : Basis
h : WellFormedBasis (hd :: tl)
f : ℝ → ℝ
hf : f ∈ tl
⊢ (Real.log ∘ f) =o[atTop] (Real.log ∘ hd)
have rw : ∀
  (h :
    ((∀ a' ∈ tl, (Real.log ∘ a') =o[atTop] (Real.log ∘ hd)) ∧
        List.Pairwise (fun (x y : ℝ → ℝ) ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) tl) ∧
      ∀ f ∈ hd :: tl, Tendsto f atTop atTop)
  {f : ℝ → ℝ} (hf : f ∈ tl), (Real.log ∘ f) =o[atTop] (Real.log ∘ hd)
Tactic: rw [WellFormedBasis, List.pairwise_cons] at h
Cleared hypotheses: h, f, hf
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
⊢ WellFormedBasis (basis_hd :: basis_tl ++ [Real.log ∘ (basis_hd :: basis_tl).getLast ⋯])
have hf_tendsto : Tendsto (Real.log ∘ (basis_hd :: basis_tl).getLast sorry) atTop atTop
Tactic: apply h_basis.push
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis (goal)
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
hf_tendsto : Tendsto (Real.log ∘ (basis_hd :: basis_tl).getLast ⋯) atTop atTop
⊢ WellFormedBasis (basis_hd :: basis_tl ++ [Real.log ∘ (basis_hd :: basis_tl).getLast ⋯])
have hf_comp : ∀ (g : ℝ → ℝ),
  (basis_hd :: basis_tl).getLast? = some g →
    (Real.log ∘ Real.log ∘ (basis_hd :: basis_tl).getLast sorry) =o[atTop] (Real.log ∘ g)
Tactic: apply h_basis.push
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis (goal)
Goal:
basis : Basis
ex : BasisExtension basis
⊢ List.Sublist basis ex.getBasis
have nil : List.Sublist [] nil.getBasis
Tactic: induction ex with
  | nil => simp
  | keep _ ex ih => simpa [getBasis] using ih
  | insert _ ex ih => exact List.Sublist.cons _ ih
Cleared hypotheses: ex
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis (goal)
Goal:
basis : Basis
ex : BasisExtension basis
nil : List.Sublist [] BasisExtension.nil.getBasis
⊢ List.Sublist basis ex.getBasis
have keep : ∀ (basis_hd : ℝ → ℝ) {basis_tl : Basis} (ex : BasisExtension basis_tl) (ih : List.Sublist basis_tl ex.getBasis),
  (basis_hd :: basis_tl).Sublist (keep basis_hd ex).getBasis
Tactic: induction ex with
  | nil => simp
  | keep _ ex ih => simpa [getBasis] using ih
  | insert _ ex ih => exact List.Sublist.cons _ ih
Cleared hypotheses: ex
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis (goal)
Goal:
basis : Basis
ex : BasisExtension basis
nil : List.Sublist [] BasisExtension.nil.getBasis
keep :
  ∀ (basis_hd : ℝ → ℝ) {basis_tl : Basis} (ex : BasisExtension basis_tl) (ih : List.Sublist basis_tl ex.getBasis),
    (basis_hd :: basis_tl).Sublist (BasisExtension.keep basis_hd ex).getBasis
⊢ List.Sublist basis ex.getBasis
have insert : ∀ {basis : Basis} (f : ℝ → ℝ) (ex : BasisExtension basis) (ih : List.Sublist basis ex.getBasis),
  List.Sublist basis (insert f ex).getBasis
Tactic: induction ex with
  | nil => simp
  | keep _ ex ih => simpa [getBasis] using ih
  | insert _ ex ih => exact List.Sublist.cons _ ih
Cleared hypotheses: ex
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
⊢ CompleteSpace.{u_1} (Stream'.Seq α)
have suffices : IsClosed.{u_1} (X := Stream' (Option α)) fun (x : Stream' (Option α)) ↦ ∀ {n : ℕ}, x n = none → x (n + 1) = none
Tactic: suffices IsClosed (X := Stream' (Option α))
      (fun x ↦ ∀ {n : ℕ}, x n = none → x (n + 1) = none) by
    apply IsClosed.completeSpace_coe
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
⊢ IsClosed.{u_1} (X := Stream' (Option α)) fun (x : Stream' (Option α)) ↦ ∀ {n : ℕ}, x n = none → x (n + 1) = none
have 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
Tactic: rw [isClosed_iff_clusterPt]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
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
⊢ s (n + 1) = none
have 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
Tactic: rw [clusterPt_principal_iff] at hs
Cleared hypotheses: hs, n, hn
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
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
⊢ s (n + 1) = none
have 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
Tactic: obtain ⟨t, hts, ht⟩ := hs (Metric.ball s ((1 / 2 : ℝ) ^ (n + 1)))
    (Metric.ball_mem_nhds _ (by positivity))
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (hypothesis)
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
⊢ s (n + 1) = none
have hn₁ : t n = none
Tactic: rw [← PiNat.apply_eq_of_dist_lt hts (by simp)] at hn
Cleared hypotheses: hn, hts, ht
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
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
⊢ s (n + 1) = none
have rw : t (n + 1) = none
Tactic: rw [← PiNat.apply_eq_of_dist_lt hts (by rfl)]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
s t : Stream' α
⊢ dist s t ≤ 1
have pos : ∀ (h : s = t), dist s t ≤ 1
Tactic: by_cases h : s = t
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
s t : Stream' α
pos : ∀ (h : s = t), dist s t ≤ 1
⊢ dist s t ≤ 1
have neg : ∀ (h : ¬s = t), dist s t ≤ 1
Tactic: by_cases h : s = t
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
s t : Stream' α
h : ¬s = t
⊢ dist s t ≤ 1
have neg : (1 / 2) ^ PiNat.firstDiff (E := fun (n : ℕ) ↦ α) s t ≤ 1
Tactic: rw [PiNat.dist_eq_of_ne h]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
s t : Stream'.Seq α
h : s ≠ t
⊢ ∃ (n : ℕ), dist s t = HPow.hPow (α := ℝ) 2⁻¹ n
have rw : ∃ (n : ℕ),
  (1 / 2) ^ PiNat.firstDiff (E := fun (n : ℕ) ↦ Option α) (↑s : (n : ℕ) → Option α) (↑t : (n : ℕ) → Option α) =
    HPow.hPow (α := ℝ) 2⁻¹ n
Tactic: rw [Subtype.dist_eq, PiNat.dist_eq_of_ne (Subtype.coe_ne_coe.mpr h)]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
x : α
s t : Stream'.Seq α
⊢ dist (Seq.cons x s) (Seq.cons x t) = 2⁻¹ * dist s t
have pos : ∀ (h : s = t), dist (Seq.cons x s) (Seq.cons x t) = 2⁻¹ * dist s t
Tactic: by_cases! h : s = t
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
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
⊢ dist (Seq.cons x s) (Seq.cons x t) = 2⁻¹ * dist s t
have neg : ∀ (h : s ≠ t), dist (Seq.cons x s) (Seq.cons x t) = 2⁻¹ * dist s t
Tactic: by_cases! h : s = t
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (hypothesis)
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
have h' : Seq.cons x s ≠ Seq.cons x t
Tactic: have h' : cons x s ≠ cons x t := by
    simpa
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
h' : Seq.cons x s ≠ Seq.cons x t
⊢ dist (Seq.cons x s) (Seq.cons x t) = 2⁻¹ * dist s t
have 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 α)
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')]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
h' : Seq.cons x s ≠ Seq.cons x t
⊢ (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 α)
have 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)
Tactic: simp only [show (1 / 2 : ℝ) = 2⁻¹ by simp, ← pow_succ']
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
h' : Seq.cons x s ≠ Seq.cons x t
⊢ 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)
have 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
Tactic: congr
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
h' : Seq.cons x s ≠ Seq.cons x t
⊢ 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
have 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)
      sorry) =
  Nat.find (p := fun (n : ℕ) ↦ ¬s.get? n = t.get? n) sorry + 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]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
h' : Seq.cons x s ≠ Seq.cons x t
⊢ (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
have pos : ∀ (h_if : some x :: (↑s : Stream' (Option α)) = some x :: (↑t : Stream' (Option α))), False
Tactic: split_ifs with h_if
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
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
⊢ (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
have 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) sorry =
    Nat.find (p := fun (n : ℕ) ↦ ¬s.get? n = t.get? n) sorry + 1
Tactic: split_ifs with h_if
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
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 α))
⊢ False
have pos : ∀ (h' : True), Seq.cons x s = Seq.cons x t
Tactic: contrapose! h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
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 = Seq.cons x t
have pos : (↑(Seq.cons x s) : Stream' (Option α)) = (↑(Seq.cons x t) : Stream' (Option α))
Tactic: apply_fun Subtype.val using Subtype.val_injective
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
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 : ℕ) ↦ ¬s.get? n = t.get? n) ⋯ + 1
have neg : ¬¬(some x :: (↑s : Stream' (Option α))) 0 = (some x :: (↑t : Stream' (Option α))) 0
Tactic: convert! Nat.find_comp_succ _ _ _
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
s t : Stream'.Seq α
h : s.head = t.head
⊢ dist s t = 2⁻¹ * dist s.tail t.tail
have nil : ∀ (h : Seq.head nil = t.head), dist nil t = 2⁻¹ * dist (Seq.tail nil) t.tail
Tactic: cases s
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
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
⊢ dist s t = 2⁻¹ * dist s.tail t.tail
have 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
Tactic: cases s
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
t : Stream'.Seq α
h : Seq.head nil = t.head
⊢ dist nil t = 2⁻¹ * dist (Seq.tail nil) t.tail
have nil : ∀ (h : Eq.{u_1 + 1} (α := Option α) (Seq.head nil) (Seq.head nil)),
  dist.{u_1} (α := Stream'.Seq α) nil nil = 2⁻¹ * dist.{u_1} (α := Stream'.Seq α) (Seq.tail nil) (Seq.tail nil)
Tactic: cases t
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
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)
⊢ dist Seq.nil t = 2⁻¹ * dist (Seq.tail Seq.nil) t.tail
have 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
Tactic: cases t
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
t : Stream'.Seq α
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
have 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)
Tactic: cases t
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
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)
⊢ dist (Seq.cons x s) t = 2⁻¹ * dist (Seq.cons x s).tail t.tail
have 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
Tactic: cases t
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (hypothesis)
Goal:
α : Type u_1
h : Eq.{u_1 + 1} (α := Option α) (Seq.head nil) (Seq.head nil)
⊢ dist.{u_1} (α := Stream'.Seq α) nil nil = 2⁻¹ * dist.{u_1} (α := Stream'.Seq α) (Seq.tail nil) (Seq.tail nil)
have h₁ : True
Tactic: simp at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (hypothesis)
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
⊢ 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
have h₁ : x = x_1
Tactic: simp at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
s t : Stream'.Seq α
h : s.head ≠ t.head
⊢ dist s t = 1
have rw : (1 / 2) ^ PiNat.firstDiff (E := fun (n : ℕ) ↦ Option α) (↑s : Stream' (Option α)) (↑t : Stream' (Option α)) = 1
Tactic: rw [Subtype.dist_eq, PiNat.dist_eq_of_ne]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
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
⊢ dist s t = 1
have rw₁ : (↑s : Stream' (Option α)) ≠ (↑t : Stream' (Option α))
Tactic: rw [Subtype.dist_eq, PiNat.dist_eq_of_ne]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
s t : Stream'.Seq α
h : s.head ≠ t.head
⊢ (1 / 2) ^ PiNat.firstDiff (E := fun (n : ℕ) ↦ Option α) (↑s : Stream' (Option α)) (↑t : Stream' (Option α)) = 1
have h₁ : PiNat.firstDiff (E := fun (n : ℕ) ↦ Option α) (↑s : Stream' (Option α)) (↑t : Stream' (Option α)) = 0
Tactic: convert! pow_zero _
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
s t : Stream'.Seq α
h : s.head ≠ t.head
⊢ PiNat.firstDiff (E := fun (n : ℕ) ↦ Option α) (↑s : Stream' (Option α)) (↑t : Stream' (Option α)) = 0
have h₁ : ∀ (h : ¬(↑s : Stream' (Option α)) = (↑t : Stream' (Option α))),
  ¬(↑s : Stream' (Option α)) 0 = (↑t : Stream' (Option α)) 0
Tactic: simp only [PiNat.firstDiff, ne_eq, Classical.dite_not, dite_eq_left_iff,
      Nat.find_eq_zero]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
s t : Stream'.Seq α
h : s.head ≠ t.head
⊢ (↑s : Stream' (Option α)) ≠ (↑t : Stream' (Option α))
have rw : s ≠ t
Tactic: rw [Subtype.coe_ne_coe]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
s t : Stream'.Seq α
h : s.head ≠ t.head
⊢ s ≠ t
have contrapose : ∀ (h : s = t), s.head = t.head
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
x y : α
s t : Stream'.Seq α
h : x ≠ y
⊢ dist (Seq.cons x s) (Seq.cons y t) = 1
have h₁ : (Seq.cons x s).head ≠ (Seq.cons y t).head
Tactic: apply dist_eq_one_of_head
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
x : α
s : Stream'.Seq α
⊢ dist (Seq.cons x s) nil = 1
have h : (Seq.cons x s).head ≠ Seq.head nil
Tactic: apply dist_eq_one_of_head
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
x : α
s : Stream'.Seq α
⊢ dist nil (Seq.cons x s) = 1
have rw : dist (Seq.cons x s) nil = 1
Tactic: rw [dist_comm]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
s t : Stream'.Seq α
h : dist s t ≤ 2⁻¹
⊢ s = nil ∧ t = nil ∨ ∃ (hd : α) (s' : Stream'.Seq α) (t' : Stream'.Seq α), s = Seq.cons hd s' ∧ t = Seq.cons hd t'
have nil : ∀ (h : dist nil t ≤ 2⁻¹),
  Eq.{u_1 + 1} (α := Stream'.Seq α) nil nil ∧ t = nil ∨
    ∃ (hd : α) (s' : Stream'.Seq α) (t' : Stream'.Seq α), nil = Seq.cons hd s' ∧ t = Seq.cons hd t'
Tactic: cases s
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
s t : Stream'.Seq α
h : dist s t ≤ 2⁻¹
nil :
  ∀ (h : dist Seq.nil t ≤ 2⁻¹),
    Eq.{u_1 + 1} (α := Stream'.Seq α) Seq.nil Seq.nil ∧ t = Seq.nil ∨
      ∃ (hd : α) (s' : Stream'.Seq α) (t' : Stream'.Seq α), Seq.nil = Seq.cons hd s' ∧ t = Seq.cons hd t'
⊢ s = Seq.nil ∧ t = Seq.nil ∨
    ∃ (hd : α) (s' : Stream'.Seq α) (t' : Stream'.Seq α), s = Seq.cons hd s' ∧ t = Seq.cons hd t'
have cons : ∀ (x : α) (s : Stream'.Seq α) (h : dist (Seq.cons x s) t ≤ 2⁻¹),
  Seq.cons x s = Seq.nil ∧ t = Seq.nil ∨
    ∃ (hd : α) (s' : Stream'.Seq α) (t' : Stream'.Seq α), Seq.cons x s = Seq.cons hd s' ∧ t = Seq.cons hd t'
Tactic: cases s
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
t : Stream'.Seq α
h : dist nil t ≤ 2⁻¹
⊢ Eq.{u_1 + 1} (α := Stream'.Seq α) nil nil ∧ t = nil ∨
    ∃ (hd : α) (s' : Stream'.Seq α) (t' : Stream'.Seq α), nil = Seq.cons hd s' ∧ t = Seq.cons hd t'
have nil : ∀ (h : dist.{u_1} (α := Stream'.Seq α) nil nil ≤ 2⁻¹),
  Eq.{u_1 + 1} (α := Stream'.Seq α) nil nil ∧ Eq.{u_1 + 1} (α := Stream'.Seq α) nil nil ∨
    ∃ (hd : α) (s' : Stream'.Seq α) (t' : Stream'.Seq α), nil = Seq.cons hd s' ∧ nil = Seq.cons hd t'
Tactic: cases t
Cleared hypotheses: t, h