awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : dist (op c (f b')) (op c (g b')) ≤ (↑1 : ℝ) * dist (f b') (g b')
⊢ dist (op c (f b')) (op c (g b')) ≤ dist (f b') (g b')

Tactic:
simpa using this
-- 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' : β
H : BddAbove (α := ℝ) (Set.range fun (b : β) ↦ dist (f b) (g 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 α)

Tactic:
apply le_ciSup (f := fun b ↦ dist (f b) (g b))

Premises used: le_ciSup
-- 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' : β
rw : BoundedSpace.{u_1} (Stream'.Seq α)
⊢ ∃ (C : ℝ), ∀ (a b : Stream'.Seq α), dist a b ≤ C

Tactic:
rw [← Metric.boundedSpace_iff]

Premises used: Metric.boundedSpace_iff
-- 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' : β
⊢ BoundedSpace.{u_1} (Stream'.Seq α)

Tactic:
infer_instance
-- 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' : β
⊢ ∃ (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
-- 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 : ∃ (C : ℝ), ∀ (a b : Stream'.Seq α), dist a b ≤ C
H : ∀ (C : ℝ) (hC : ∀ (a b : Stream'.Seq α), dist a b ≤ C), BddAbove (α := ℝ) (Set.range fun (b : β) ↦ dist (f b) (g b))
⊢ BddAbove (α := ℝ) (Set.range fun (b : β) ↦ dist (f b) (g b))

Tactic:
obtain ⟨C, hC⟩ := this
-- 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' : β
C : ℝ
hC : ∀ (a b : Stream'.Seq α), dist a b ≤ C
h₁ : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (b : β) ↦ dist (f b) (g b))) C
⊢ BddAbove (α := ℝ) (Set.range fun (b : β) ↦ dist (f b) (g b))

Tactic:
use 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' : β
C : ℝ
hC : ∀ (a b : Stream'.Seq α), dist a b ≤ C
h₁ : ∀ (a : β), dist (f a) (g a) ≤ C
⊢ Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (b : β) ↦ dist (f b) (g b))) C

Tactic:
simp [upperBounds]

Premises used: upperBounds
-- 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' : β
C : ℝ
hC : ∀ (a b : Stream'.Seq α), dist a b ≤ C
⊢ ∀ (a : β), dist (f a) (g a) ≤ C

Tactic:
grind
-- 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' : β
_ : dist (op c (f b')) (op c (g b')) ≤ dist (f b') (g b')
_₁ : dist (f b') (g b') ≤ dist f g
⊢ dist (op c (f b')) (op c (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

Premises used: Dist.dist
-- 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 : β
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
⊢ 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:
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

Premises used: Option.some, Option.none
-- 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'))
⊢ 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
-- 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'))
hT : LipschitzWith 2⁻¹ T
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'))
⊢ ∃ (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

Premises used: Tactic.ComputeAsymptotics.Seq.exists_fixed_point_of_contractible
-- 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'))
hT : LipschitzWith 2⁻¹ T
f : β → Stream'.Seq α
hf : Function.IsFixedPt T f
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'))
⊢ ∃ (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:
use f
-- 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'))
hT : LipschitzWith 2⁻¹ T
f : β → Stream'.Seq α
hf : Function.IsFixedPt T f
b : β
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'))
⊢ 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:
rw [← hf]
-- 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'))
hT : LipschitzWith 2⁻¹ T
f : β → Stream'.Seq α
hf : Function.IsFixedPt T f
b : β
h₁ :
  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'))))
⊢ 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:
simp only [T]
-- 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'))
hT : LipschitzWith 2⁻¹ T
f : β → Stream'.Seq α
hf : Function.IsFixedPt T f
b : β
hb : F b = none
⊢ match (motive := Option (α × γ × β) → Prop) none with
  | none =>
    Eq.{u_1 + 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 α)
      (nil : Stream'.Seq α)
  | some (a, c, b') =>
    (match (motive := Option (α × γ × β) → Stream'.Seq α) none 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:
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'))
hT : LipschitzWith 2⁻¹ T
f : β → Stream'.Seq α
hf : Function.IsFixedPt T f
b : β
v : α × γ × β
hb : F b = some v
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'))))
⊢ 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'))))

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
    | 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')
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')))
⊢ 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:
simp only [cons_eq_cons, true_and]

Premises used: Stream'.Seq.cons_eq_cons, true_and
-- 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'))
hT : LipschitzWith 2⁻¹ T
f : β → Stream'.Seq α
hf : Function.IsFixedPt T f
b : β
a : α
c : γ
b' : β
hb : F b = some (a, c, b')
h₁ :
  f b' =
    match (motive := Option (α × γ × β) → Stream'.Seq α) F b' with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f 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')))

Tactic:
congr
-- 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'))
hT : LipschitzWith 2⁻¹ T
f : β → Stream'.Seq α
hf : Function.IsFixedPt T f
b : β
a : α
c : γ
b' : β
hb : F b = some (a, c, b')
h₁ : f b' = T f b'
⊢ f b' =
    match (motive := Option (α × γ × β) → Stream'.Seq α) F b' with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))

Tactic:
change f b' = T f b'
-- 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'))
hT : LipschitzWith 2⁻¹ T
f : β → Stream'.Seq α
hf : Function.IsFixedPt T f
b : β
a : α
c : γ
b' : β
hb : F b = some (a, c, b')
h₁ h₂ : f b' = f b'
⊢ f b' = T f b'

Tactic:
rw [hf]