awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
x y : α
s t : Stream'.Seq α
h : x ≠ y
⊢ (Seq.cons x s).head ≠ (Seq.cons y t).head

Tactic:
simpa
-- 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 = 1

Tactic:
apply dist_eq_one_of_head

Premises used: Tactic.ComputeAsymptotics.Seq.dist_eq_one_of_head
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
x : α
s : Stream'.Seq α
⊢ (Seq.cons x s).head ≠ Seq.head nil

Tactic:
simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
x : α
s : Stream'.Seq α
rw : dist (Seq.cons x s) nil = 1
⊢ dist nil (Seq.cons x s) = 1

Tactic:
rw [dist_comm]

Premises used: dist_comm
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
x : α
s : Stream'.Seq α
⊢ dist (Seq.cons x s) nil = 1

Tactic:
simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
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'
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'
⊢ s = Seq.nil ∧ t = Seq.nil ∨
    ∃ (hd : α) (s' : Stream'.Seq α) (t' : Stream'.Seq α), s = Seq.cons hd s' ∧ t = Seq.cons hd t'

Tactic:
cases s
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
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'
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'
⊢ 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'

Tactic:
cases t
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
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'
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'
⊢ 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'

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

Tactic:
norm_num at h
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
x : α
s : Stream'.Seq α
h : dist nil (Seq.cons x s) ≤ 2⁻¹
⊢ Eq.{u_1 + 1} (α := Stream'.Seq α) nil nil ∧ Seq.cons x s = nil ∨
    ∃ (hd : α) (s' : Stream'.Seq α) (t' : Stream'.Seq α), nil = Seq.cons hd s' ∧ Seq.cons x s = Seq.cons hd t'

Tactic:
norm_num at h
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
x : α
s : Stream'.Seq α
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:
norm_num at h
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
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⁻¹
⊢ dist (Seq.cons x s) (Seq.cons x_1 s_1) ≤ 1 / 2

Tactic:
norm_num at h
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
h : True
⊢ 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:
simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
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
cons : x_1 = x
⊢ 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:
simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
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
⊢ x_1 = x

Tactic:
grind [dist_cons_cons_eq_one]

Premises used: Tactic.ComputeAsymptotics.Seq.dist_cons_cons_eq_one
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
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⁻¹
inr : ∀ (hd : α) (s' t' : Stream'.Seq α), dist (Seq.cons hd s') (Seq.cons hd t') ≤ 2⁻¹
⊢ dist s t ≤ 2⁻¹

Tactic:
obtain ⟨rfl, rfl⟩ | ⟨hd, s', t', rfl, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
⊢ dist.{u_1} (α := Stream'.Seq α) nil nil ≤ 2⁻¹

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

Tactic:
simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
⊢ FriendlyOperation op ↔ ∀ (s t : Stream'.Seq α), dist (op s) (op t) ≤ dist s t

Tactic:
simp [FriendlyOperation, lipschitzWith_iff_dist_le_mul]

Premises used: lipschitzWith_iff_dist_le_mul, Tactic.ComputeAsymptotics.Seq.FriendlyOperation
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
⊢ FriendlyOperation.{u_1} (α := α) _root_.id

Tactic:
LipschitzWith.id

Premises used: LipschitzWith.id, Tactic.ComputeAsymptotics.Seq.FriendlyOperation
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op op' : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
h' : FriendlyOperation op'
⊢ LipschitzWith 1 op

Tactic:
rw [FriendlyOperation] at h h' ⊢

Premises used: Tactic.ComputeAsymptotics.Seq.FriendlyOperation
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op op' : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
h' : FriendlyOperation op'
h₁ : LipschitzWith 1 op
⊢ LipschitzWith 1 op'

Tactic:
rw [FriendlyOperation] at h h' ⊢

Premises used: Tactic.ComputeAsymptotics.Seq.FriendlyOperation
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op op' : Stream'.Seq α → Stream'.Seq α
h : LipschitzWith 1 op
h' : LipschitzWith 1 op'
⊢ LipschitzWith (HMul.hMul (α := NNReal) 1 1) (op ∘ op')

Tactic:
h.comp h'

Premises used: LipschitzWith.comp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op op' : Stream'.Seq α → Stream'.Seq α
h : LipschitzWith 1 op
h' : LipschitzWith 1 op'
h₁ : 1 = HMul.hMul (α := NNReal) 1 1
⊢ LipschitzWith 1 (op ∘ op')

Tactic:
convert! h.comp h'

Premises used: LipschitzWith.comp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op op' : Stream'.Seq α → Stream'.Seq α
h : LipschitzWith 1 op
h' : LipschitzWith 1 op'
⊢ 1 = HMul.hMul (α := NNReal) 1 1

Tactic:
simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
s : Stream'.Seq α
⊢ FriendlyOperation.{u_1} (α := α) fun (x : Stream'.Seq α) ↦ s

Tactic:
simp [friendlyOperation_iff_dist_le_dist]

Premises used: Tactic.ComputeAsymptotics.Seq.friendlyOperation_iff_dist_le_dist
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
γ : Type u_3
γ' : Type u_4
F : γ → Stream'.Seq α → Stream'.Seq α
g : γ' → γ
h : FriendlyOperationClass F
⊢ FriendlyOperationClass.{u_1, u_4} (α := α) fun (c : γ') ↦ F (g c)

Tactic:
grind [FriendlyOperationClass]

Premises used: Tactic.ComputeAsymptotics.Seq.FriendlyOperationClass
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op₁ op₂ : Stream'.Seq α → Stream'.Seq α
h₁ : FriendlyOperation op₁
h₂ : FriendlyOperation op₂
P : Option α → Prop
inst : DecidablePred P
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
⊢ FriendlyOperation.{u_1} (α := α) fun (s : Stream'.Seq α) ↦ if P s.head then op₁ s else op₂ s

Tactic:
rw [friendlyOperation_iff_dist_le_dist] at h₁ h₂ ⊢

Premises used: Tactic.ComputeAsymptotics.Seq.friendlyOperation_iff_dist_le_dist
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
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
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
⊢ 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

Premises used: Stream'.Seq.head
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
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 α
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:
simp [dist_eq_one_of_head h_head]

Premises used: Tactic.ComputeAsymptotics.Seq.dist_eq_one_of_head
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
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 α
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:
grind
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
s t : Stream'.Seq α
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
⊢ dist (op s) (op t) ≤ dist s t

Tactic:
rw [FriendlyOperation, lipschitzWith_iff_dist_le_mul] at h

Premises used: lipschitzWith_iff_dist_le_mul, Tactic.ComputeAsymptotics.Seq.FriendlyOperation
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
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:
simpa using h s t
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
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
left : LT.lt (α := NNReal) 2⁻¹ 1
right : LipschitzWith 2⁻¹ F
⊢ ContractingWith 2⁻¹ F

Tactic:
constructor
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
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
⊢ LT.lt (α := NNReal) 2⁻¹ 1

Tactic:
norm_num
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
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
⊢ LipschitzWith 2⁻¹ F

Tactic:
h
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
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
⊢ LipschitzWith 2⁻¹ F

Tactic:
exact h
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
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

Tactic:
have hF : ContractingWith 2⁻¹ F := by
    constructor
    · norm_num
    · exact h
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
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
h₁ : Function.IsFixedPt F f
⊢ ∃ (f : β → Stream'.Seq α), Function.IsFixedPt F f

Tactic:
use f
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
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
⊢ Function.IsFixedPt F f

Tactic:
hF.fixedPoint_isFixedPt

Premises used: ContractingWith.fixedPoint_isFixedPt
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
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
⊢ Function.IsFixedPt F f

Tactic:
exact hF.fixedPoint_isFixedPt

Premises used: ContractingWith.fixedPoint_isFixedPt
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : UniformFun.{u_2, u_1} β (Stream'.Seq α) → UniformFun.{u_2, u_1} β (Stream'.Seq α) :=
  fun (f : UniformFun.{u_2, u_1} β (Stream'.Seq α)) (b : β) ↦
    match (motive := Option (α × γ × β) → Stream'.Seq α) F b with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))
rw : ∀ (x y : UniformFun.{u_2, u_1} β (Stream'.Seq α)), dist (T x) (T y) ≤ (↑2⁻¹ : ℝ) * dist x y
⊢ LipschitzWith 2⁻¹ T

Tactic:
rw [lipschitzWith_iff_dist_le_mul]

Premises used: lipschitzWith_iff_dist_le_mul
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : UniformFun.{u_2, u_1} β (Stream'.Seq α) → UniformFun.{u_2, u_1} β (Stream'.Seq α) :=
  fun (f : UniformFun.{u_2, u_1} β (Stream'.Seq α)) (b : β) ↦
    match (motive := Option (α × γ × β) → Stream'.Seq α) F b with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))
f g : UniformFun.{u_2, u_1} β (Stream'.Seq α)
⊢ 0 ≤ (↑2⁻¹ : ℝ) * dist f g

Tactic:
positivity
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : UniformFun.{u_2, u_1} β (Stream'.Seq α) → UniformFun.{u_2, u_1} β (Stream'.Seq α) :=
  fun (f : UniformFun.{u_2, u_1} β (Stream'.Seq α)) (b : β) ↦
    match (motive := Option (α × γ × β) → Stream'.Seq α) F b with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))
f g : UniformFun.{u_2, u_1} β (Stream'.Seq α)
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
⊢ dist (T f) (T g) ≤ (↑2⁻¹ : ℝ) * dist f g

Tactic:
rw [UniformFun.dist_le (by positivity)]

Premises used: UniformFun.dist_le
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : UniformFun.{u_2, u_1} β (Stream'.Seq α) → UniformFun.{u_2, u_1} β (Stream'.Seq α) :=
  fun (f : UniformFun.{u_2, u_1} β (Stream'.Seq α)) (b : β) ↦
    match (motive := Option (α × γ × β) → Stream'.Seq α) F b with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))
f g : UniformFun.{u_2, u_1} β (Stream'.Seq α)
b : β
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
⊢ 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

Tactic:
simp only [UniformFun.toFun, UniformFun.ofFun, Equiv.coe_fn_symm_mk, NNReal.coe_inv,
      NNReal.coe_ofNat, T]

Premises used: Equiv.coe_fn_symm_mk, UniformFun.toFun, NNReal.coe_inv, NNReal.coe_ofNat, UniformFun.ofFun
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : UniformFun.{u_2, u_1} β (Stream'.Seq α) → UniformFun.{u_2, u_1} β (Stream'.Seq α) :=
  fun (f : UniformFun.{u_2, u_1} β (Stream'.Seq α)) (b : β) ↦
    match (motive := Option (α × γ × β) → Stream'.Seq α) F b with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))
f g : UniformFun.{u_2, u_1} β (Stream'.Seq α)
b : β
⊢ dist.{u_1} (α := Stream'.Seq α)
      (match (motive := Option (α × γ × β) → Stream'.Seq α) none with
        | none => nil
        | some (a, c, b') => Seq.cons a (op c (f b')) :
        Stream'.Seq α)
      (match (motive := Option (α × γ × β) → Stream'.Seq α) none with
        | none => nil
        | some (a, c, b') => Seq.cons a (op c (g b')) :
        Stream'.Seq α) ≤
    2⁻¹ * dist f g

Tactic:
simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : UniformFun.{u_2, u_1} β (Stream'.Seq α) → UniformFun.{u_2, u_1} β (Stream'.Seq α) :=
  fun (f : UniformFun.{u_2, u_1} β (Stream'.Seq α)) (b : β) ↦
    match (motive := Option (α × γ × β) → Stream'.Seq α) F b with
    | none => nil
    | Option.some (a, c, b') => Seq.cons a (op c (f b'))
f g : UniformFun.{u_2, u_1} β (Stream'.Seq α)
b : β
v : α × γ × β
some :
  ∀ (a : α) (c : γ) (b' : β),
    dist (α := Stream'.Seq α)
        (match (motive := Option (α × γ × β) → Stream'.Seq α) Option.some (a, c, b') with
          | none => nil
          | Option.some (a, c, b') => Seq.cons a (op c (f b')) :
          Stream'.Seq α)
        (match (motive := Option (α × γ × β) → Stream'.Seq α) Option.some (a, c, b') with
          | none => nil
          | Option.some (a, c, b') => Seq.cons a (op c (g b')) :
          Stream'.Seq α) ≤
      2⁻¹ * dist f g
⊢ dist (α := Stream'.Seq α)
      (match (motive := Option (α × γ × β) → Stream'.Seq α) Option.some v with
        | none => nil
        | Option.some (a, c, b') => Seq.cons a (op c (f b')) :
        Stream'.Seq α)
      (match (motive := Option (α × γ × β) → Stream'.Seq α) Option.some v with
        | none => nil
        | Option.some (a, c, b') => Seq.cons a (op c (g b')) :
        Stream'.Seq α) ≤
    2⁻¹ * dist f g

Tactic:
obtain ⟨a, c, b'⟩ := v
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : UniformFun.{u_2, u_1} β (Stream'.Seq α) → UniformFun.{u_2, u_1} β (Stream'.Seq α) :=
  fun (f : UniformFun.{u_2, u_1} β (Stream'.Seq α)) (b : β) ↦
    match (motive := Option (α × γ × β) → Stream'.Seq α) F b with
    | none => nil
    | Option.some (a, c, b') => Seq.cons a (op c (f b'))
f g : UniformFun.{u_2, u_1} β (Stream'.Seq α)
b : β
a : α
c : γ
b' : β
some : dist (op c (f b')) (op c (g b')) ≤ dist f g
⊢ dist (α := Stream'.Seq α)
      (match (motive := Option (α × γ × β) → Stream'.Seq α) Option.some (a, c, b') with
        | none => nil
        | Option.some (a, c, b') => Seq.cons a (op c (f b')) :
        Stream'.Seq α)
      (match (motive := Option (α × γ × β) → Stream'.Seq α) Option.some (a, c, b') with
        | none => nil
        | Option.some (a, c, b') => Seq.cons a (op c (g b')) :
        Stream'.Seq α) ≤
    2⁻¹ * dist f g

Tactic:
simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : UniformFun.{u_2, u_1} β (Stream'.Seq α) → UniformFun.{u_2, u_1} β (Stream'.Seq α) :=
  fun (f : UniformFun.{u_2, u_1} β (Stream'.Seq α)) (b : β) ↦
    match (motive := Option (α × γ × β) → Stream'.Seq α) F b with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))
f g : UniformFun.{u_2, u_1} β (Stream'.Seq α)
b : β
a : α
c : γ
b' : β
⊢ FriendlyOperation (op c)

Tactic:
have := h.friend c
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : UniformFun.{u_2, u_1} β (Stream'.Seq α) → UniformFun.{u_2, u_1} β (Stream'.Seq α) :=
  fun (f : UniformFun.{u_2, u_1} β (Stream'.Seq α)) (b : β) ↦
    match (motive := Option (α × γ × β) → Stream'.Seq α) F b with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))
f g : UniformFun.{u_2, u_1} β (Stream'.Seq α)
b : β
a : α
c : γ
b' : β
this : FriendlyOperation (op c)
⊢ ∀ (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

Premises used: lipschitzWith_iff_dist_le_mul, Tactic.ComputeAsymptotics.Seq.FriendlyOperation
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : UniformFun.{u_2, u_1} β (Stream'.Seq α) → UniformFun.{u_2, u_1} β (Stream'.Seq α) :=
  fun (f : UniformFun.{u_2, u_1} β (Stream'.Seq α)) (b : β) ↦
    match (motive := Option (α × γ × β) → Stream'.Seq α) F b with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))
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')) ≤ (↑1 : ℝ) * dist (f b') (g b')

Tactic:
specialize this (f b') (g b')