mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
tl_tl : Multiseries basis_hd basis_tl
h_coef : ∀ x ∈ (mk (Multiseries.cons exp coef (Multiseries.cons tl_exp tl_coef tl_tl)) 0).seq, x.2.Sorted
h_Pairwise✝ :
  Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk (Multiseries.cons exp coef (Multiseries.cons tl_exp tl_coef tl_tl)) 0).seq
h_all : ∀ x ∈ Multiseries.cons tl_exp tl_coef tl_tl, (exp, coef) > x
h_Pairwise : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (Multiseries.cons tl_exp tl_coef tl_tl)
⊢ (tl_exp, tl_coef) ∈ Multiseries.cons tl_exp tl_coef tl_tl

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: m : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length m = List.length basis
h_firstIsNeg : m.FirstNonzeroIsNeg
⊢ Tendsto (m.toFun basis) atTop (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: exps_hd : ℝ
exps_tl : List ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_allZero : exps_hd = 0 ∧ AllZero exps_tl
⊢ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) = toFun exps_tl basis_tl

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: m : UnitMonomial
basis : Basis
h_allZero : m.AllZero
⊢ Tendsto (m.toFun basis) atTop (𝓝 1)

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
tl_tl : Multiseries basis_hd basis_tl
h_coef : ∀ x ∈ (mk (Multiseries.cons exp coef (Multiseries.cons tl_exp tl_coef tl_tl)) 0).seq, x.2.Sorted
h_Pairwise✝ :
  Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk (Multiseries.cons exp coef (Multiseries.cons tl_exp tl_coef tl_tl)) 0).seq
h_all : ∀ x ∈ Multiseries.cons tl_exp tl_coef tl_tl, (exp, coef) > x
h_Pairwise : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (Multiseries.cons tl_exp tl_coef tl_tl)
x : ℝ × MultiseriesExpansion basis_tl
hx : x ∈ (mk (Multiseries.cons tl_exp tl_coef tl_tl) 0).seq
⊢ x ∈ (mk (Multiseries.cons exp coef (Multiseries.cons tl_exp tl_coef tl_tl)) 0).seq

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
exp1 : ℝ
m1 : List ℝ
h1 : (exp1 :: m1).length = (basis_hd :: basis_tl).length
m2 : List ℝ
h2 : (exp1 :: m2).length = (basis_hd :: basis_tl).length
h : List.Lex (fun x1 x2 ↦ x1 < x2) m1 m2
⊢ m1.length = basis_tl.length

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
exp1 : ℝ
m1 : List ℝ
h1 : (exp1 :: m1).length = (basis_hd :: basis_tl).length
m2 : List ℝ
h2 : (exp1 :: m2).length = (basis_hd :: basis_tl).length
h : List.Lex (fun x1 x2 ↦ x1 < x2) m1 m2
⊢ m2.length = basis_tl.length

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h : (Multiseries.cons exp coef tl).Sorted
⊢ coef.Sorted ∧ tl.leadingExp < ↑exp ∧ tl.Sorted

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
ms : Multiseries basis_hd basis_tl
h : ms.Sorted
⊢ ms.tail.Sorted

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
exp1 : ℝ
m1 : List ℝ
exp2 : ℝ
m2 : List ℝ
h : exp1 < exp2
h1 : m1.length = basis_tl.length
h2 : m2.length = basis_tl.length
⊢ m2.length = List.length (inv m1)

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons.cons.cons.rel.h
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
exp1 : ℝ
m1 : List ℝ
exp2 : ℝ
m2 : List ℝ
h : exp1 < exp2
h1 : m1.length = basis_tl.length
h2 : m2.length = basis_tl.length
⊢ Tendsto (toFun ((exp2 - exp1) :: mul m2 (inv m1)) (basis_hd :: basis_tl)) atTop atTop

Tactic:
apply toFun_tendsto_top_of_firstNonzeroIsPos h_basis

Goal state after:
case cons.cons.cons.rel.h.h_length
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
exp1 : ℝ
m1 : List ℝ
exp2 : ℝ
m2 : List ℝ
h : exp1 < exp2
h1 : m1.length = basis_tl.length
h2 : m2.length = basis_tl.length
⊢ ((exp2 - exp1) :: mul m2 (inv m1)).length = (basis_hd :: basis_tl).length

case cons.cons.cons.rel.h.h_firstIsPos
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
exp1 : ℝ
m1 : List ℝ
exp2 : ℝ
m2 : List ℝ
h : exp1 < exp2
h1 : m1.length = basis_tl.length
h2 : m2.length = basis_tl.length
⊢ FirstNonzeroIsPos ((exp2 - exp1) :: mul m2 (inv m1))
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: basis : Basis
m1 m2 : UnitMonomial
h_basis : WellFormedBasis basis
h1 : List.length m1 = List.length basis
h2 : List.length m2 = List.length basis
h_lt : m1 < m2
⊢ m1.toFun basis =o[atTop] m2.toFun basis

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: coef : ℝ
basis : Basis
⊢ { coef := coef, unit := [] }.toFun basis = fun x ↦ coef

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: coef exp : ℝ
m : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ { coef := coef, unit := exp :: m }.toFun (basis_hd :: basis_tl) =
    basis_hd ^ exp * { coef := coef, unit := m }.toFun basis_tl

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: t : Monomial
basis : Basis
h_coef : t.coef = 0
⊢ t.toFun basis = 0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: t : Monomial
basis : Basis
⊢ t.toFun basis = -t.neg.toFun basis

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: t1 t2 : Monomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length t1.unit = List.length t2.unit
⊢ (t1.mul t2).toFun basis =ᶠ[atTop] t1.toFun basis * t2.toFun basis

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: t : Monomial
basis : Basis
c : ℝ
⊢ (t.smul c).toFun basis = c • t.toFun basis

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: a : ONote
m : ℕ+
b : ONote
iha : a = 0
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
e : a.fundamentalSequence = Sum.inl none
m' : ℕ
e' : m.natPred = m' + 1
⊢ m = (m' + 1).succPNat

Tactic:
← e',

Goal state after:
a : ONote
m : ℕ+
b : ONote
iha : a = 0
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
e : a.fundamentalSequence = Sum.inl none
m' : ℕ
e' : m.natPred = m' + 1
⊢ m = m.natPred.succPNat
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: t : Monomial
basis : Basis
h_basis : WellFormedBasis basis
⊢ t.inv.toFun basis =ᶠ[atTop] (t.toFun basis)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: t : Monomial
⊢ List.length t.inv.unit = List.length t.unit

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: t : Monomial
basis : Basis
h_basis : WellFormedBasis basis
h_coef : 0 < t.coef
⊢ ∀ᶠ (x : ℝ) in atTop, 0 < t.toFun basis x

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: coef : ℝ
exps : UnitMonomial
left right : Basis
⊢ let t := { coef := coef, unit := List.replicate (List.length left) 0 ++ exps };
  t.toFun (left ++ right) = { coef := coef, unit := exps }.toFun right

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: coef : ℝ
exps : UnitMonomial
basis : Basis
h_coef : coef = 0
t : Monomial := { coef := coef, unit := exps }
⊢ t.coef = 0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: coef : ℝ
exps : UnitMonomial
basis : Basis
h_coef : coef = 0
⊢ let t := { coef := coef, unit := exps };
  Tendsto (t.toFun basis) atTop (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: coef : ℝ
exps : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length exps = List.length basis
h_exps : exps.FirstNonzeroIsNeg
⊢ let t := { coef := coef, unit := exps };
  Tendsto (t.toFun basis) atTop (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: coef : ℝ
exps : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length exps = List.length basis
h_coef : 0 < coef
h_exps : exps.FirstNonzeroIsPos
⊢ let t := { coef := coef, unit := exps };
  Tendsto (t.toFun basis) atTop atTop

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < ↑exp ∧ motive tl
⊢ s.Sorted

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
f : ℝ → ℝ
⊢ (mk Multiseries.nil f).Sorted

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
f : ℝ → ℝ
h_coef : coef.Sorted
⊢ (mk (Multiseries.cons exp coef Multiseries.nil) f).Sorted

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: coef : ℝ
exps : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length exps = List.length basis
h_coef : coef < 0
h_exps : exps.FirstNonzeroIsPos
⊢ let t := { coef := coef, unit := exps };
  Tendsto (t.toFun basis) atTop atBot

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
m' : ℕ
e' : m.natPred = m' + 1
⊢ m = (m' + 1).succPNat

Tactic:
← e',

Goal state after:
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
m' : ℕ
e' : m.natPred = m' + 1
⊢ m = m.natPred.succPNat
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
f : ℝ → ℝ
h_coef : coef.Sorted
h_comp : tl.leadingExp < ↑exp
h_tl : tl.Sorted
⊢ (mk (Multiseries.cons exp coef tl) f).Sorted

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
f : ℝ → ℝ
h : (mk (Multiseries.cons exp coef tl) f).Sorted
⊢ (Multiseries.cons exp coef tl).Sorted

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: coef : ℝ
exps : UnitMonomial
basis : Basis
h_exps : exps.AllZero
⊢ let t := { coef := coef, unit := exps };
  Tendsto (t.toFun basis) atTop (𝓝 coef)

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
f : ℝ → ℝ
h : (mk (Multiseries.cons exp coef tl) f).Sorted
⊢ coef.Sorted ∧ tl.leadingExp < ↑exp ∧ tl.Sorted

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: t : Monomial
basis_hd : ℝ → ℝ
basis_tl : Basis
h_length : List.length t.unit = List.length basis_tl
h_basis : WellFormedBasis (basis_hd :: basis_tl)
⊢ Majorized (t.toFun basis_tl) basis_hd 0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
f : ℝ → ℝ
h_sorted : ms.Sorted
⊢ (ms.replaceFun f).Sorted

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: basis : Basis
t1 t2 : Monomial
h_basis : WellFormedBasis basis
h1 : List.length t1.unit = List.length basis
h2 : List.length t2.unit = List.length basis
h_coef2 : t2.coef ≠ 0
h_lt : t1.unit < t2.unit
⊢ t1.toFun basis =o[atTop] t2.toFun basis

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_base : motive op
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
              (T s.head)
⊢ FriendlyOperation op

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
γ : Type u_3
s t : Stream'.Seq α
op : γ → Stream'.Seq α → Stream'.Seq α
inst✝ : FriendlyOperationClass op
motive : Stream'.Seq α → Stream'.Seq α → Prop
base : motive s t
step :
  ∀ (u v : Stream'.Seq α),
    motive u v → u = v ∨ ∃ hd u' v' c, u = Seq.cons hd (op c u') ∧ v = Seq.cons hd (op c v') ∧ motive u' v'
this : dist s t = 0
⊢ s = t

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: left right : Basis
t1 t2 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
h2 : List.length t2.unit = List.length right
h_coef2 : t2.coef ≠ 0
h_lt : t1.unit < List.replicate (List.length left) 0 ++ t2.unit
⊢ t1.toFun (left ++ right) =o[atTop] t2.toFun right

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
iha :
  IsSuccLimit a.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)) ∧ ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
⊢ m = (m' + 1).succPNat

Tactic:
← e',

Goal state after:
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
iha :
  IsSuccLimit a.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)) ∧ ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
⊢ m = m.natPred.succPNat
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
γ : Type u_3
s t : Stream'.Seq α
op : γ → Stream'.Seq α → Stream'.Seq α
inst✝ : FriendlyOperationClass op
motive : Stream'.Seq α → Stream'.Seq α → Prop
base : motive s t
step :
  ∀ (u v : Stream'.Seq α),
    motive u v → u = v ∨ ∃ hd u' v' c, u = Seq.cons hd (op c u') ∧ v = Seq.cons hd (op c v') ∧ motive u' v'
this : ∀ (n : ℕ), dist s t ≤ 2⁻¹ ^ n
⊢ dist s t = 0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: left right : Basis
t1 t2 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
h2 : List.length t2.unit = List.length right
h_coef1 : t1.coef ≠ 0
h_lt : List.replicate (List.length left) 0 ++ t2.unit < t1.unit
⊢ t2.toFun right =o[atTop] t1.toFun (left ++ right)

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming

Goal state before:
pp: c : MultiseriesExpansion []
⊢ c.IsZero ↔ c.toReal = 0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h : ms.IsZero
⊢ ms.seq = Multiseries.nil

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h : ms.seq = Multiseries.nil
⊢ ms.IsZero

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming

Goal state before:
pp: basis : Basis
ms : MultiseriesExpansion basis
h_zero : ms.IsZero
h_approx : ms.Approximates
⊢ ms.toFun =ᶠ[atTop] 0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
f : ℝ → ℝ
⊢ ¬(mk (Multiseries.cons exp coef tl) f).IsZero

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
γ : Type u_3
op : γ → Stream'.Seq α → Stream'.Seq α
inst✝ : FriendlyOperationClass op
motive : Stream'.Seq α → Stream'.Seq α → Prop
step :
  ∀ (u v : Stream'.Seq α),
    motive u v → u = v ∨ ∃ hd u' v' c, u = Seq.cons hd (op c u') ∧ v = Seq.cons hd (op c v') ∧ motive u' v'
n : ℕ
hd : α
u v : Stream'.Seq α
ih : dist u v ≤ 2⁻¹ ^ n
c : γ
h_next : motive u v
base : motive (Seq.cons hd (op c u)) (Seq.cons hd (op c v))
⊢ 2⁻¹ * dist (op c u) (op c v) ≤ 2⁻¹ * dist u v

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h : ms.Trimmed
⊢ ms.seq.Trimmed

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
γ : Type u_3
op : γ → Stream'.Seq α → Stream'.Seq α
inst✝ : FriendlyOperationClass op
motive : Stream'.Seq α → Stream'.Seq α → Prop
step :
  ∀ (u v : Stream'.Seq α),
    motive u v → u = v ∨ ∃ hd u' v' c, u = Seq.cons hd (op c u') ∧ v = Seq.cons hd (op c v') ∧ motive u' v'
n : ℕ
hd : α
u v : Stream'.Seq α
ih : dist u v ≤ 2⁻¹ ^ n
c : γ
h_next : motive u v
base : motive (Seq.cons hd (op c u)) (Seq.cons hd (op c v))
⊢ 2⁻¹ * dist u v ≤ 2⁻¹ ^ (n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h : ms.seq.Trimmed
⊢ ms.Trimmed

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ Multiseries.nil.Trimmed

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
γ : Type u_3
s t : Stream'.Seq α
op : γ → Stream'.Seq α → Stream'.Seq α
inst✝ : FriendlyOperationClass op
motive : Stream'.Seq α → Stream'.Seq α → Prop
base : motive s t
step :
  ∀ (u v : Stream'.Seq α),
    motive u v → u = v ∨ ∃ hd u' v' c, u = Seq.cons hd (op c u') ∧ v = Seq.cons hd (op c v') ∧ motive u' v'
⊢ s = t

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h : (Multiseries.cons exp coef tl).Trimmed
⊢ coef.Trimmed ∧ ¬coef.IsZero

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
f : ℝ → ℝ
h : (mk (Multiseries.cons exp coef tl) f).Trimmed
⊢ coef.Trimmed ∧ ¬coef.IsZero

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.DeriveCountable

Goal state before:
pp: p : Prop
a b b' : ℕ
h : b = b' → p
⊢ Nat.pair a b = Nat.pair a b' → p

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.DeriveCountable

Goal state before:
pp: p : Prop
a b a' b' : ℕ
h : a = a' → b = b' → p
⊢ Nat.pair a b = Nat.pair a' b' → p

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.DeriveEncodable

Goal state before:
pp: n : ℕ
h : (Nat.unpair n).1 ≠ 0
⊢ (Nat.unpair n).2 < n

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.DeriveEncodable

Goal state before:
pp: n : ℕ
p : ℕ × ℕ := Nat.unpair n
h : ¬p.1 = 0
this : p.1 ≤ n
⊢ 1 ≤ n

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.DeriveEncodable

Goal state before:
pp: s : S
⊢ S.decode s.encode = s

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
ms✝ : MultiseriesExpansion (basis_hd :: basis_tl)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop
h_base : motive ms✝
h_step :
  ∀ (ms : MultiseriesExpansion (basis_hd :: basis_tl)),
    motive ms →
      ms.seq = Multiseries.nil ∧ ms.toFun =ᶠ[atTop] 0 ∨
        ∃ exp coef tl,
          ms.seq = Multiseries.cons exp coef tl ∧
            coef.Approximates ∧
              Majorized ms.toFun basis_hd exp ∧ motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h_ms : motive ms
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h_seq : ms.seq = Multiseries.cons exp coef tl
h_coef : coef.Approximates
h_maj : Majorized ms.toFun basis_hd exp
h_tl : motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
⊢ coef.Approximates ∨ ∃ (h_basis : basis_tl = basis_hd :: basis_tl), motive (h_basis ▸ coef)

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.DeriveEncodable

Goal state before:
pp: n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
h : ¬(Nat.unpair n).1 = 0
⊢ 1 ≤ (Nat.unpair n).1

Tactic:
Nat.one_le_iff_ne_zero

Goal state after:
n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
h : ¬(Nat.unpair n).1 = 0
⊢ (Nat.unpair n).1 ≠ 0
Module: Mathlib.Tactic.DeriveEncodable

Goal state before:
pp: ih : ∀ m < 0, (S.decode m).encode = m
h : ¬(Nat.unpair 0).1 = 0
⊢ (Nat.unpair 0).1 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.DeriveEncodable

Goal state before:
pp: n' : ℕ
ih : ∀ m < n' + 1, (S.decode m).encode = m
h : ¬(Nat.unpair (n' + 1)).1 = 0
⊢ 1 ≤ n' + 1

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.DeriveEncodable

Goal state before:
pp: n : ℕ
⊢ (S.decode n).encode = n

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop
h_base : motive ms
h_step :
  ∀ (ms : MultiseriesExpansion (basis_hd :: basis_tl)),
    motive ms →
      ms.seq = Multiseries.nil ∧ ms.toFun =ᶠ[atTop] 0 ∨
        ∃ exp coef tl,
          ms.seq = Multiseries.cons exp coef tl ∧
            coef.Approximates ∧
              Majorized ms.toFun basis_hd exp ∧ motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
⊢ ms.Approximates

Tactic:
by

Goal state after: