awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
t : Stream'.Seq α
h : dist Seq.nil t ≤ 2⁻¹
nil :
  ∀ (h : dist.{u_1} (α := Stream'.Seq α) Seq.nil Seq.nil ≤ 2⁻¹),
    Eq.{u_1 + 1} (α := Stream'.Seq α) Seq.nil Seq.nil ∧ Eq.{u_1 + 1} (α := Stream'.Seq α) Seq.nil Seq.nil ∨
      ∃ (hd : α) (s' : Stream'.Seq α) (t' : Stream'.Seq α), Seq.nil = Seq.cons hd s' ∧ Seq.nil = Seq.cons hd t'
⊢ 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'
have nil₁ : ∀ (x : α) (s : Stream'.Seq α) (h : dist Seq.nil (Seq.cons x s) ≤ 2⁻¹),
  Eq.{u_1 + 1} (α := Stream'.Seq α) Seq.nil Seq.nil ∧ Seq.cons x s = Seq.nil ∨
    ∃ (hd : α) (s' : Stream'.Seq α) (t' : Stream'.Seq α), Seq.nil = Seq.cons hd s' ∧ Seq.cons x s = Seq.cons hd t'
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 : dist (Seq.cons x s) t ≤ 2⁻¹
⊢ Seq.cons x s = nil ∧ t = nil ∨
    ∃ (hd : α) (s' : Stream'.Seq α) (t' : Stream'.Seq α), Seq.cons x s = Seq.cons hd s' ∧ t = Seq.cons hd t'
have cons : ∀ (h : dist (Seq.cons x s) nil ≤ 2⁻¹),
  Seq.cons x s = nil ∧ Eq.{u_1 + 1} (α := Stream'.Seq α) nil nil ∨
    ∃ (hd : α) (s' : Stream'.Seq α) (t' : Stream'.Seq α), Seq.cons x s = Seq.cons hd s' ∧ nil = Seq.cons hd t'
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 : dist (Seq.cons x s) t ≤ 2⁻¹
cons :
  ∀ (h : dist (Seq.cons x s) nil ≤ 2⁻¹),
    Seq.cons x s = nil ∧ Eq.{u_1 + 1} (α := Stream'.Seq α) nil nil ∨
      ∃ (hd : α) (s' : Stream'.Seq α) (t' : Stream'.Seq α), Seq.cons x s = Seq.cons hd s' ∧ nil = Seq.cons hd t'
⊢ Seq.cons x s = nil ∧ t = nil ∨
    ∃ (hd : α) (s' : Stream'.Seq α) (t' : Stream'.Seq α), Seq.cons x s = Seq.cons hd s' ∧ t = Seq.cons hd t'
have cons₁ : ∀ (x_1 : α) (s_1 : Stream'.Seq α) (h : dist (Seq.cons x s) (Seq.cons x_1 s_1) ≤ 2⁻¹),
  Seq.cons x s = nil ∧ Seq.cons x_1 s_1 = nil ∨
    ∃ (hd : α) (s' : Stream'.Seq α) (t' : Stream'.Seq α),
      Seq.cons x s = Seq.cons hd s' ∧ Seq.cons x_1 s_1 = Seq.cons hd t'
Tactic: cases t
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (hypothesis)
Goal:
α : Type u_1
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'
have h₁ : True
Tactic: norm_num 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 : dist (Seq.cons x s) (Seq.cons x_1 s_1) ≤ 2⁻¹
⊢ Seq.cons x s = nil ∧ Seq.cons x_1 s_1 = nil ∨
    ∃ (hd : α) (s' : Stream'.Seq α) (t' : Stream'.Seq α),
      Seq.cons x s = Seq.cons hd s' ∧ Seq.cons x_1 s_1 = Seq.cons hd t'
have h₁ : dist (Seq.cons x s) (Seq.cons x_1 s_1) ≤ 1 / 2
Tactic: norm_num at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
x : α
s : Stream'.Seq α
x_1 : α
s_1 : Stream'.Seq α
h : dist (Seq.cons x s) (Seq.cons x_1 s_1) ≤ 1 / 2
⊢ Seq.cons x s = nil ∧ Seq.cons x_1 s_1 = nil ∨
    ∃ (hd : α) (s' : Stream'.Seq α) (t' : Stream'.Seq α),
      Seq.cons x s = Seq.cons hd s' ∧ Seq.cons x_1 s_1 = Seq.cons hd t'
have cons : x_1 = x
Tactic: simp
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
s t : Stream'.Seq α
h : s = nil ∧ t = nil ∨ ∃ (hd : α) (s' : Stream'.Seq α) (t' : Stream'.Seq α), s = Seq.cons hd s' ∧ t = Seq.cons hd t'
⊢ dist s t ≤ 2⁻¹
have inl : dist.{u_1} (α := Stream'.Seq α) nil nil ≤ 2⁻¹
Tactic: obtain ⟨rfl, rfl⟩ | ⟨hd, s', t', rfl, rfl⟩ := h
Cleared hypotheses: s, t, h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
s t : Stream'.Seq α
h : s = nil ∧ t = nil ∨ ∃ (hd : α) (s' : Stream'.Seq α) (t' : Stream'.Seq α), s = Seq.cons hd s' ∧ t = Seq.cons hd t'
inl : dist.{u_1} (α := Stream'.Seq α) nil nil ≤ 2⁻¹
⊢ dist s t ≤ 2⁻¹
have inr : ∀ (hd : α) (s' t' : Stream'.Seq α), dist (Seq.cons hd s') (Seq.cons hd t') ≤ 2⁻¹
Tactic: obtain ⟨rfl, rfl⟩ | ⟨hd, s', t', rfl, rfl⟩ := h
Cleared hypotheses: s, t, h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (hypothesis)
Goal:
α : Type u_1
op op' : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
h' : FriendlyOperation op'
⊢ FriendlyOperation (op ∘ op')
have h₁ : LipschitzWith 1 op
Tactic: rw [FriendlyOperation] at h h' ⊢
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (hypothesis)
Goal:
α : Type u_1
op op' : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
h' : FriendlyOperation op'
h₁ : LipschitzWith 1 op
⊢ FriendlyOperation (op ∘ op')
have h'₁ : LipschitzWith 1 op'
Tactic: rw [FriendlyOperation] at h h' ⊢
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
op op' : Stream'.Seq α → Stream'.Seq α
h : LipschitzWith 1 op
h' : LipschitzWith 1 op'
⊢ LipschitzWith 1 (op ∘ op')
have h₁ : 1 = HMul.hMul (α := NNReal) 1 1
Tactic: convert! h.comp h'
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
op₁ op₂ : Stream'.Seq α → Stream'.Seq α
h₁ : FriendlyOperation op₁
h₂ : FriendlyOperation op₂
P : Option α → Prop
inst : DecidablePred P
⊢ FriendlyOperation.{u_1} (α := α) fun (s : Stream'.Seq α) ↦ if P s.head then op₁ s else op₂ s
have rw : ∀ (h₁ : ∀ (s t : Stream'.Seq α), dist (op₁ s) (op₁ t) ≤ dist s t)
  (h₂ : ∀ (s t : Stream'.Seq α), dist (op₂ s) (op₂ t) ≤ dist s t) {P : Option α → Prop} [inst : DecidablePred P]
  (s t : Stream'.Seq α), dist (if P s.head then op₁ s else op₂ s) (if P t.head then op₁ t else op₂ t) ≤ dist s t
Tactic: rw [friendlyOperation_iff_dist_le_dist] at h₁ h₂ ⊢
Cleared hypotheses: h₁, h₂, P, inst
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
op₁ op₂ : Stream'.Seq α → Stream'.Seq α
h₁ : ∀ (s t : Stream'.Seq α), dist (op₁ s) (op₁ t) ≤ dist s t
h₂ : ∀ (s t : Stream'.Seq α), dist (op₂ s) (op₂ t) ≤ dist s t
P : Option α → Prop
inst : DecidablePred P
s t : Stream'.Seq α
⊢ dist (if P s.head then op₁ s else op₂ s) (if P t.head then op₁ t else op₂ t) ≤ dist s t
have pos : ∀ (h_head : s.head ≠ t.head), dist (if P s.head then op₁ s else op₂ s) (if P t.head then op₁ t else op₂ t) ≤ dist s t
Tactic: by_cases! h_head : s.head ≠ t.head
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
op₁ op₂ : Stream'.Seq α → Stream'.Seq α
h₁ : ∀ (s t : Stream'.Seq α), dist (op₁ s) (op₁ t) ≤ dist s t
h₂ : ∀ (s t : Stream'.Seq α), dist (op₂ s) (op₂ t) ≤ dist s t
P : Option α → Prop
inst : DecidablePred P
s t : Stream'.Seq α
pos :
  ∀ (h_head : s.head ≠ t.head), dist (if P s.head then op₁ s else op₂ s) (if P t.head then op₁ t else op₂ t) ≤ dist s t
⊢ dist (if P s.head then op₁ s else op₂ s) (if P t.head then op₁ t else op₂ t) ≤ dist s t
have neg : ∀ (h_head : s.head = t.head), dist (if P s.head then op₁ s else op₂ s) (if P t.head then op₁ t else op₂ t) ≤ dist s t
Tactic: by_cases! h_head : s.head ≠ t.head
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
s t : Stream'.Seq α
⊢ dist (op s) (op t) ≤ dist s t
have rw : ∀ (h : ∀ (x y : Stream'.Seq α), dist (op x) (op y) ≤ (↑1 : ℝ) * dist x y) {s t : Stream'.Seq α},
  dist (op s) (op t) ≤ dist s t
Tactic: rw [FriendlyOperation, lipschitzWith_iff_dist_le_mul] at h
Cleared hypotheses: h, s, t
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
β : Type u_2
F : UniformFun.{u_2, u_1} β (Stream'.Seq α) → UniformFun.{u_2, u_1} β (Stream'.Seq α)
h : LipschitzWith 2⁻¹ F
⊢ ContractingWith 2⁻¹ F
have left : LT.lt (α := NNReal) 2⁻¹ 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (hypothesis)
Goal:
α : Type u_1
β : Type u_2
F : UniformFun.{u_2, u_1} β (Stream'.Seq α) → UniformFun.{u_2, u_1} β (Stream'.Seq α)
h : LipschitzWith 2⁻¹ F
⊢ ∃ (f : β → Stream'.Seq α), Function.IsFixedPt F f
have hF : ContractingWith 2⁻¹ F
Tactic: have hF : ContractingWith 2⁻¹ F := by
    constructor
    · norm_num
    · exact h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (goal)
Goal:
α : Type u_1
β : Type u_2
F : UniformFun.{u_2, u_1} β (Stream'.Seq α) → UniformFun.{u_2, u_1} β (Stream'.Seq α)
h : LipschitzWith 2⁻¹ F
hF : ContractingWith 2⁻¹ F
f : UniformFun.{u_2, u_1} β (Stream'.Seq α) := ContractingWith.fixedPoint F hF
⊢ ∃ (f : β → Stream'.Seq α), Function.IsFixedPt F f
have h₁ : Function.IsFixedPt F f
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'))
⊢ LipschitzWith 2⁻¹ T
have rw : ∀ (x y : UniformFun.{u_2, u_1} β (Stream'.Seq α)), dist (T x) (T y) ≤ (↑2⁻¹ : ℝ) * dist x y
Tactic: rw [lipschitzWith_iff_dist_le_mul]
-- 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 α)
⊢ dist (T f) (T g) ≤ (↑2⁻¹ : ℝ) * dist f g
have rw : ∀ (x : β),
  dist.{u_1} (α := Stream'.Seq α)
      ((UniformFun.toFun : (a : β →ᵤ Stream'.Seq α) → β → Stream'.Seq α) (T f) x : Stream'.Seq α)
      ((UniformFun.toFun : (a : β →ᵤ Stream'.Seq α) → β → Stream'.Seq α) (T g) x : Stream'.Seq α) ≤
    (↑2⁻¹ : ℝ) * dist f g
Tactic: rw [UniformFun.dist_le (by positivity)]
-- 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.{u_1} (α := Stream'.Seq α)
      ((UniformFun.toFun : (a : β →ᵤ Stream'.Seq α) → β → Stream'.Seq α) (T f) b : Stream'.Seq α)
      ((UniformFun.toFun : (a : β →ᵤ Stream'.Seq α) → β → Stream'.Seq α) (T g) b : Stream'.Seq α) ≤
    (↑2⁻¹ : ℝ) * dist f g
have simp : 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
Tactic: simp only [UniformFun.toFun, UniformFun.ofFun, Equiv.coe_fn_symm_mk, NNReal.coe_inv,
      NNReal.coe_ofNat, T]
-- 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 : β
v : α × γ × β
⊢ dist (α := 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 α)
      (match (motive := Option (α × γ × β) → Stream'.Seq α) some v with
        | none => nil
        | some (a, c, b') => Seq.cons a (op c (g b')) :
        Stream'.Seq α) ≤
    2⁻¹ * dist f g
have some : ∀ (a : α) (c : γ) (b' : β),
  dist (α := 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 α)
      (match (motive := Option (α × γ × β) → Stream'.Seq α) some (a, c, b') with
        | none => nil
        | some (a, c, b') => Seq.cons a (op c (g b')) :
        Stream'.Seq α) ≤
    2⁻¹ * dist f g
Tactic: obtain ⟨a, c, b'⟩ := v
Cleared hypotheses: v
-- 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 (α := 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 α)
      (match (motive := Option (α × γ × β) → Stream'.Seq α) some (a, c, b') with
        | none => nil
        | some (a, c, b') => Seq.cons a (op c (g b')) :
        Stream'.Seq α) ≤
    2⁻¹ * dist f g
have some : dist (op c (f b')) (op c (g b')) ≤ dist f g
Tactic: simp
-- 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 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')
have this : FriendlyOperation (op c)
Tactic: have := h.friend c
-- 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 g : UniformFun.{u_2, u_1} β (Stream'.Seq α)
b : β
a : α
c : γ
b' : β
this : FriendlyOperation (op c)
⊢ dist (op c (f b')) (op c (g b')) ≤ dist (f b') (g b')
have this₁ : ∀ (x y : Stream'.Seq α), dist (op c x) (op c y) ≤ (↑1 : ℝ) * dist x y
Tactic: rw [FriendlyOperation, lipschitzWith_iff_dist_le_mul] at this
Cleared hypotheses: this
-- 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 g : UniformFun.{u_2, u_1} β (Stream'.Seq α)
b : β
a : α
c : γ
b' : β
this : ∀ (x y : Stream'.Seq α), dist (op c x) (op c y) ≤ (↑1 : ℝ) * dist x y
⊢ dist (op c (f b')) (op c (g b')) ≤ dist (f b') (g b')
have this₁ : dist (op c (f b')) (op c (g b')) ≤ (↑1 : ℝ) * dist (f b') (g b')
Tactic: specialize this (f b') (g b')
Cleared hypotheses: this
-- 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 (f b') (g b') ≤
    ⨆ (x : β),
      dist.{u_1} (α := Stream'.Seq α)
        ((UniformFun.toFun : (a : β →ᵤ Stream'.Seq α) → β → Stream'.Seq α) f x : Stream'.Seq α)
        ((UniformFun.toFun : (a : β →ᵤ Stream'.Seq α) → β → Stream'.Seq α) g x : Stream'.Seq α)
have H : BddAbove (α := ℝ) (Set.range fun (b : β) ↦ dist (f b) (g b))
Tactic: apply le_ciSup (f := fun b ↦ dist (f b) (g b))
-- 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' : β
⊢ ∃ (C : ℝ), ∀ (a b : Stream'.Seq α), dist a b ≤ C
have rw : BoundedSpace.{u_1} (Stream'.Seq α)
Tactic: rw [← Metric.boundedSpace_iff]
-- 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 g : UniformFun.{u_2, u_1} β (Stream'.Seq α)
b : β
a : α
c : γ
b' : β
⊢ BddAbove (α := ℝ) (Set.range fun (b : β) ↦ dist (f b) (g b))
have this : ∃ (C : ℝ), ∀ (a b : Stream'.Seq α), dist a b ≤ C
Tactic: have : ∃ C, ∀ (a b : Seq α), dist a b ≤ C := by
            rw [← Metric.boundedSpace_iff]
            infer_instance
-- 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' : β
this : ∃ (C : ℝ), ∀ (a b : Stream'.Seq α), dist a b ≤ C
⊢ BddAbove (α := ℝ) (Set.range fun (b : β) ↦ dist (f b) (g b))
have H : ∀ (C : ℝ) (hC : ∀ (a b : Stream'.Seq α), dist a b ≤ C), BddAbove (α := ℝ) (Set.range fun (b : β) ↦ dist (f b) (g b))
Tactic: obtain ⟨C, hC⟩ := this
Cleared hypotheses: this
-- 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' : β
C : ℝ
hC : ∀ (a b : Stream'.Seq α), dist a b ≤ C
⊢ BddAbove (α := ℝ) (Set.range fun (b : β) ↦ dist (f b) (g b))
have h₁ : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (b : β) ↦ dist (f b) (g b))) C
Tactic: use C
-- 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' : β
C : ℝ
hC : ∀ (a b : Stream'.Seq α), dist a b ≤ C
⊢ Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (b : β) ↦ dist (f b) (g b))) C
have h₁ : ∀ (a : β), dist (f a) (g a) ≤ C
Tactic: simp [upperBounds]
-- 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 g
have _ : dist (op c (f b')) (op c (g b')) ≤ dist (f b') (g b')
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