awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
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'))
f g : UniformFun.{u_2, u_1} β (Stream'.Seq α)
b : β
a : α
c : γ
b' : β
_ : dist (op c (f b')) (op c (g b')) ≤ dist (f b') (g b')
⊢ dist (op c (f b')) (op c (g b')) ≤ dist f g
have _₁ : dist (f b') (g b') ≤ dist f g
Tactic: calc
        _ ≤ dist (f b') (g b') := by
          have := h.friend c
          rw [FriendlyOperation, lipschitzWith_iff_dist_le_mul] at this
          specialize this (f b') (g b')
          simpa using this
        _ ≤ _ := by
          simp only [UniformFun.dist_def]
          apply le_ciSup (f := fun b ↦ dist (f b) (g b))
          have : ∃ C, ∀ (a b : Seq α), dist a b ≤ C := by
            rw [← Metric.boundedSpace_iff]
            infer_instance
          obtain ⟨C, hC⟩ := this
          use C
          simp [upperBounds]
          grind
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
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'))
f g : UniformFun.{u_2, u_1} β (Stream'.Seq α)
b : β
⊢ dist (α := 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 α)
      (match (motive := Option (α × γ × β) → Stream'.Seq α) F b with
        | none => nil
        | some (a, c, b') => Seq.cons a (op c (g b')) :
        Stream'.Seq α) ≤
    2⁻¹ * dist f g
have cases : ∀ (x : Option (α × γ × β)),
  dist (α := Stream'.Seq α)
      (match (motive := Option (α × γ × β) → Stream'.Seq α) x with
        | none => nil
        | some (a, c, b') => Seq.cons a (op c (f b')) :
        Stream'.Seq α)
      (match (motive := Option (α × γ × β) → Stream'.Seq α) x with
        | none => nil
        | some (a, c, b') => Seq.cons a (op c (g b')) :
        Stream'.Seq α) ≤
    2⁻¹ * dist f g
Tactic: cases F b with
    | none => simp
    | some v =>
      obtain ⟨a, c, b'⟩ := v
      simp
      calc
        _ ≤ dist (f b') (g b') := by
          have := h.friend c
          rw [FriendlyOperation, lipschitzWith_iff_dist_le_mul] at this
          specialize this (f b') (g b')
          simpa using this
        _ ≤ _ := by
          simp only [UniformFun.dist_def]
          apply le_ciSup (f := fun b ↦ dist (f b) (g b))
          have : ∃ C, ∀ (a b : Seq α), dist a b ≤ C := by
            rw [← Metric.boundedSpace_iff]
            infer_instance
          obtain ⟨C, hC⟩ := this
          use C
          simp [upperBounds]
          grind
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (hypothesis)
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'))
⊢ ∃ (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'))
have hT : LipschitzWith 2⁻¹ T
Tactic: have hT : LipschitzWith 2⁻¹ T := by
    rw [lipschitzWith_iff_dist_le_mul]
    intro f g
    rw [UniformFun.dist_le (by positivity)]
    intro b
    simp only [UniformFun.toFun, UniformFun.ofFun, Equiv.coe_fn_symm_mk, NNReal.coe_inv,
      NNReal.coe_ofNat, T]
    cases F b with
    | none => simp
    | some v =>
      obtain ⟨a, c, b'⟩ := v
      simp
      calc
        _ ≤ dist (f b') (g b') := by
          have := h.friend c
          rw [FriendlyOperation, lipschitzWith_iff_dist_le_mul] at this
          specialize this (f b') (g b')
          simpa using this
        _ ≤ _ := by
          simp only [UniformFun.dist_def]
          apply le_ciSup (f := fun b ↦ dist (f b) (g b))
          have : ∃ C, ∀ (a b : Seq α), dist a b ≤ C := by
            rw [← Metric.boundedSpace_iff]
            infer_instance
          obtain ⟨C, hC⟩ := this
          use C
          simp [upperBounds]
          grind
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
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 α),
    ∀ (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'))
have obtain : ∀ (f : β → Stream'.Seq α) (hf : Function.IsFixedPt T f),
  ∃ (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'))
Tactic: obtain ⟨f, hf⟩ := exists_fixed_point_of_contractible T hT
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
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
⊢ ∃ (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'))
have h₁ : ∀ (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'))
Tactic: use f
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
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 : β
⊢ match (motive := Option (α × γ × β) → Prop) F b with
  | none => f b = nil
  | some (a, c, b') => f b = Seq.cons a (op c (f b'))
have h₁ : match (motive := Option (α × γ × β) → Prop) F b with
| none => T f b = nil
| some (a, c, b') => T f b = Seq.cons a (op c (T f b'))
Tactic: rw [← hf]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
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 : β
v : α × γ × β
hb : F b = some v
⊢ match (motive := Option (α × γ × β) → Prop) some v with
  | none =>
    Eq (α := Stream'.Seq α)
      (match (motive := Option (α × γ × β) → Stream'.Seq α) some v 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 α) some v 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'))))
have h₁ : ∀ (a : α) (c : γ) (b' : β) (hb : F b = some (a, c, b')),
  match (motive := Option (α × γ × β) → Prop) some (a, c, b') with
  | none =>
    Eq (α := Stream'.Seq α)
      (match (motive := Option (α × γ × β) → Stream'.Seq α) some (a, c, b') with
        | none => nil
        | some (a, c, b') => Seq.cons a (op c (f b')) :
        Stream'.Seq α)
      (nil : Stream'.Seq α)
  | some (a_1, c_1, b'_1) =>
    (match (motive := Option (α × γ × β) → Stream'.Seq α) some (a, c, b') with
      | none => nil
      | some (a, c, b') => Seq.cons a (op c (f b'))) =
      Seq.cons a_1
        (op c_1
          (match (motive := Option (α × γ × β) → Stream'.Seq α) F b'_1 with
          | none => nil
          | some (a, c, b') => Seq.cons a (op c (f b'))))
Tactic: obtain ⟨a, c, b'⟩ := v
Cleared hypotheses: v, hb
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
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 : β
a : α
c : γ
b' : β
hb : F b = some (a, c, b')
⊢ match (motive := Option (α × γ × β) → Prop) some (a, c, b') with
  | none =>
    Eq (α := Stream'.Seq α)
      (match (motive := Option (α × γ × β) → Stream'.Seq α) some (a, c, b') with
        | none => nil
        | some (a, c, b') => Seq.cons a (op c (f b')) :
        Stream'.Seq α)
      (nil : Stream'.Seq α)
  | some (a_1, c_1, b'_1) =>
    (match (motive := Option (α × γ × β) → Stream'.Seq α) some (a, c, b') with
      | none => nil
      | some (a, c, b') => Seq.cons a (op c (f b'))) =
      Seq.cons a_1
        (op c_1
          (match (motive := Option (α × γ × β) → Stream'.Seq α) F b'_1 with
          | none => nil
          | some (a, c, b') => Seq.cons a (op c (f b'))))
have h₁ : op c (f b') =
  op c
    (match (motive := Option (α × γ × β) → Stream'.Seq α) F b' with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b')))
Tactic: simp only [cons_eq_cons, true_and]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
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 : β
a : α
c : γ
b' : β
hb : F b = some (a, c, b')
⊢ op c (f b') =
    op c
      (match (motive := Option (α × γ × β) → Stream'.Seq α) F b' with
      | none => nil
      | some (a, c, b') => Seq.cons a (op c (f b')))
have h₁ : f b' =
  match (motive := Option (α × γ × β) → Stream'.Seq α) F b' with
  | none => nil
  | some (a, c, b') => Seq.cons a (op c (f b'))
Tactic: congr
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
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 : β
a : α
c : γ
b' : β
hb : F b = some (a, c, b')
⊢ f b' = T f b'
have h₁ : f b' = f b'
Tactic: rw [hf]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
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 : β
⊢ 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'))))
have 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'))))
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]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (hypothesis)
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
⊢ gcorec F op b = nil
have this : match (motive := Option (α × γ × β) → Prop) F b with
| none =>
  sorry.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') =>
  sorry.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
        (sorry.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
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (hypothesis)
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')
⊢ gcorec F op b = Seq.cons a (op c (gcorec F op b'))
have this : match (motive := Option (α × γ × β) → Prop) F b with
| none =>
  sorry.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') =>
  sorry.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
        (sorry.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
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
hd : α
⊢ FriendlyOperation (Seq.cons hd)
have simp : ∀ (s t : Stream'.Seq α), 2⁻¹ * dist s t ≤ dist s t
Tactic: simp only [friendlyOperation_iff_dist_le_dist, dist_cons_cons]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
hd : α
x y : Stream'.Seq α
⊢ 2⁻¹ * dist x y ≤ dist x y
have linarith : dist x y < 2⁻¹ * dist x y → 2 / 2 = 1
Tactic: linarith [dist_nonneg (x := x) (y := y)]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
hd : α
x y : Stream'.Seq α
linarith : dist x y < 2⁻¹ * dist x y → 2 / 2 = 1
⊢ 2⁻¹ * dist x y ≤ dist x y
have linarith₁ : dist x y < 2⁻¹ * dist x y → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [dist_nonneg (x := x) (y := y)]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
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
⊢ 2⁻¹ * dist x y ≤ dist x y
have linarith₂ : dist x y < 2⁻¹ * dist x y → HMul.hMul (α := ℝ) 2 1 = 2
Tactic: linarith [dist_nonneg (x := x) (y := y)]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
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
⊢ 2⁻¹ * dist x y ≤ dist x y
have linarith₃ : dist x y < 2⁻¹ * dist x y → GT.gt (α := ℝ) 2 0
Tactic: linarith [dist_nonneg (x := x) (y := y)]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
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
⊢ 2⁻¹ * dist x y ≤ dist x y
have 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
Tactic: linarith [dist_nonneg (x := x) (y := y)]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
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
have 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
Tactic: rwa [dist_cons_cons, dist_eq_half_of_head, mul_le_mul_iff_right₀ (by norm_num)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (hypothesis)
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
⊢ (op (Seq.cons hd x)).head = (op (Seq.cons hd y)).head
have h₁ : dist (op (Seq.cons hd x)) (op (Seq.cons hd y)) ≤ 2⁻¹
Tactic: grw [dist_le_one x y, mul_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
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⁻¹
⊢ (op (Seq.cons hd x)).head = (op (Seq.cons hd y)).head
have 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
Tactic: obtain (⟨hx, hy⟩ | ⟨_, _, _, hx, hy⟩) := dist_le_half_iff.mp h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
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
⊢ (op (Seq.cons hd x)).head = (op (Seq.cons hd y)).head
have 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
Tactic: obtain (⟨hx, hy⟩ | ⟨_, _, _, hx, hy⟩) := dist_le_half_iff.mp h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
hd : α
h : FriendlyOperation op
⊢ FriendlyOperation.{u_1} (α := α) fun (s : Stream'.Seq α) ↦ (op (Seq.cons hd s)).tail
have 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
Tactic: simp_rw [friendlyOperation_iff_dist_le_dist] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (hypothesis)
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)).tail (op (Seq.cons hd y)).tail ≤ dist x y
have h₁ : 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)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
a : α
s t : Stream'.Seq α
⊢ (op (Seq.cons a s)).head = (op (Seq.cons a t)).head
have 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
Tactic: rw [friendlyOperation_iff_dist_le_dist] at h
Cleared hypotheses: h, a, s, t
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (hypothesis)
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 α
⊢ (op (Seq.cons a s)).head = (op (Seq.cons a t)).head
have h₁ : 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)
Cleared hypotheses: h