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

Goal state before:
pp: case nil.nil
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
⊢ nil.destruct =
    Option.map
      (fun x ↦
        match x with
        | (hd, op') => (hd, ↑op' nil.tail))
      (match nil.head with
      | none =>
        match nil.destruct with
        | none => none
        | some (t_hd, t_tl) => some (t_hd, ⟨fun x ↦ t_tl, ⋯⟩)
      | some s_hd =>
        match (op (Seq.cons s_hd nil)).destruct with
        | none => none
        | some (t_hd, snd) => some (t_hd, ⟨fun s_tl ↦ (op (Seq.cons s_hd s_tl)).tail, ⋯⟩))

pp: case nil.cons
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
x✝ : α
s✝ : Stream'.Seq α
⊢ (Seq.cons x✝ s✝).destruct =
    Option.map
      (fun x ↦
        match x with
        | (hd, op') => (hd, ↑op' nil.tail))
      (match nil.head with
      | none =>
        match (Seq.cons x✝ s✝).destruct with
        | none => none
        | some (t_hd, t_tl) => some (t_hd, ⟨fun x ↦ t_tl, ⋯⟩)
      | some s_hd =>
        match (op (Seq.cons s_hd nil)).destruct with
        | none => none
        | some (t_hd, snd) => some (t_hd, ⟨fun s_tl ↦ (op (Seq.cons s_hd s_tl)).tail, ⋯⟩))

Tactic:
<;>

Goal state after:
case nil.nil
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
⊢ nil.destruct =
    Option.map
      (fun x ↦
        match x with
        | (hd, op') => (hd, ↑op' nil.tail))
      (match nil.head with
      | none =>
        match nil.destruct with
        | none => none
        | some (t_hd, t_tl) => some (t_hd, ⟨fun x ↦ t_tl, ⋯⟩)
      | some s_hd =>
        match (op (Seq.cons s_hd nil)).destruct with
        | none => none
        | some (t_hd, snd) => some (t_hd, ⟨fun s_tl ↦ (op (Seq.cons s_hd s_tl)).tail, ⋯⟩))

case nil.cons
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
x✝ : α
s✝ : Stream'.Seq α
⊢ (Seq.cons x✝ s✝).destruct =
    Option.map
      (fun x ↦
        match x with
        | (hd, op') => (hd, ↑op' nil.tail))
      (match nil.head with
      | none =>
        match (Seq.cons x✝ s✝).destruct with
        | none => none
        | some (t_hd, t_tl) => some (t_hd, ⟨fun x ↦ t_tl, ⋯⟩)
      | some s_hd =>
        match (op (Seq.cons s_hd nil)).destruct with
        | none => none
        | some (t_hd, snd) => some (t_hd, ⟨fun s_tl ↦ (op (Seq.cons s_hd s_tl)).tail, ⋯⟩))
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
c : ℝ
⊢ (Multiseries.const basis_hd basis_tl c).Sorted

Tactic:
simp only [Multiseries.const]
  exact const_sorted.cons_nil

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

Goal state before:
pp: case cons
c : ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
⊢ (const (basis_hd :: basis_tl) c).Approximates

Tactic:
simp only [const, Multiseries.const]

Goal state after:
case cons
c : ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
⊢ (mk (Multiseries.cons 0 (const basis_tl c) Multiseries.nil) fun x ↦ c).Approximates
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic

Goal state before:
pp: case cons.zero
r : ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
⊢ (monomialRpow (basis_hd :: basis_tl) (↑0) r).toFun = (basis_hd :: basis_tl)[0] ^ r

pp: case cons.succ
r : ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
i✝ : Fin basis_tl.length
⊢ (monomialRpow (basis_hd :: basis_tl) (↑i✝.succ) r).toFun = (basis_hd :: basis_tl)[i✝.succ] ^ r

Tactic:
<;>

Goal state after:
case cons.zero
r : ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
⊢ (monomialRpow (basis_hd :: basis_tl) (↑0) r).toFun = (basis_hd :: basis_tl)[0] ^ r

case cons.succ
r : ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
i✝ : Fin basis_tl.length
⊢ (monomialRpow (basis_hd :: basis_tl) (↑i✝.succ) r).toFun = (basis_hd :: basis_tl)[i✝.succ] ^ r
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates

Goal state before:
pp: case zero
⊢ AllZero (List.replicate 0 0)

pp: case succ
n✝ : ℕ
a✝ : AllZero (List.replicate n✝ 0)
⊢ AllZero (List.replicate (n✝ + 1) 0)

Tactic:
<;>

Goal state after:
case zero
⊢ AllZero (List.replicate 0 0)

case succ
n✝ : ℕ
a✝ : AllZero (List.replicate n✝ 0)
⊢ AllZero (List.replicate (n✝ + 1) 0)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
op : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
h : FriendlyOperation op
ms : Multiseries basis_hd basis_tl
⊢ Option.map
      (fun x ↦
        match x with
        | ((exp, coef), tl) => (exp, coef, tl))
      (Seq.destruct (op ms)) =
    Option.map
      (fun x ↦
        match x with
        | (exp, coef, op') => (exp, coef, ↑op' ms.tail))
      (h.unfold ms.head)

Tactic:
simp [Seq.FriendlyOperation.destruct_apply_eq_unfold h, FriendlyOperation.unfold, head]

Goal state after:
basis_hd : ℝ → ℝ
basis_tl : Basis
op : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
h : FriendlyOperation op
ms : Multiseries basis_hd basis_tl
⊢ Option.map
      ((fun x ↦
          match x with
          | ((exp, coef), tl) => (exp, coef, tl)) ∘
        fun x ↦ (x.1, ↑x.2 (Seq.tail ms)))
      (Seq.FriendlyOperation.unfold h (Seq.head ms)) =
    Option.map ((fun x ↦ (x.1, x.2.1, ↑x.2.2 ms.tail)) ∘ fun x ↦ (x.1.1, x.1.2, x.2))
      (Seq.FriendlyOperation.unfold h (Seq.head ms))
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case none
basis_hd : ℝ → ℝ
basis_tl : Basis
op : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
h : FriendlyOperation op
ms : Multiseries basis_hd basis_tl
⊢ Option.map
      ((fun x ↦
          match x with
          | ((exp, coef), tl) => (exp, coef, tl)) ∘
        fun x ↦ (x.1, ↑x.2 (Seq.tail ms)))
      none =
    Option.map ((fun x ↦ (x.1, x.2.1, ↑x.2.2 ms.tail)) ∘ fun x ↦ (x.1.1, x.1.2, x.2)) none

pp: case some
basis_hd : ℝ → ℝ
basis_tl : Basis
op : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
h : FriendlyOperation op
ms : Multiseries basis_hd basis_tl
val✝ : (ℝ × MultiseriesExpansion basis_tl) × Subtype Seq.FriendlyOperation
⊢ Option.map
      ((fun x ↦
          match x with
          | ((exp, coef), tl) => (exp, coef, tl)) ∘
        fun x ↦ (x.1, ↑x.2 (Seq.tail ms)))
      (some val✝) =
    Option.map ((fun x ↦ (x.1, x.2.1, ↑x.2.2 ms.tail)) ∘ fun x ↦ (x.1.1, x.1.2, x.2)) (some val✝)

Tactic:
<;>

Goal state after:
case none
basis_hd : ℝ → ℝ
basis_tl : Basis
op : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
h : FriendlyOperation op
ms : Multiseries basis_hd basis_tl
⊢ Option.map
      ((fun x ↦
          match x with
          | ((exp, coef), tl) => (exp, coef, tl)) ∘
        fun x ↦ (x.1, ↑x.2 (Seq.tail ms)))
      none =
    Option.map ((fun x ↦ (x.1, x.2.1, ↑x.2.2 ms.tail)) ∘ fun x ↦ (x.1.1, x.1.2, x.2)) none

case some
basis_hd : ℝ → ℝ
basis_tl : Basis
op : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
h : FriendlyOperation op
ms : Multiseries basis_hd basis_tl
val✝ : (ℝ × MultiseriesExpansion basis_tl) × Subtype Seq.FriendlyOperation
⊢ Option.map
      ((fun x ↦
          match x with
          | ((exp, coef), tl) => (exp, coef, tl)) ∘
        fun x ↦ (x.1, ↑x.2 (Seq.tail ms)))
      (some val✝) =
    Option.map ((fun x ↦ (x.1, x.2.1, ↑x.2.2 ms.tail)) ∘ fun x ↦ (x.1.1, x.1.2, x.2)) (some val✝)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case nil
basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ nil.leadingExp = ⊥ ↔ nil = nil

pp: case cons
basis_hd : ℝ → ℝ
basis_tl : Basis
exp✝ : ℝ
coef✝ : MultiseriesExpansion basis_tl
tl✝ : Multiseries basis_hd basis_tl
⊢ (cons exp✝ coef✝ tl✝).leadingExp = ⊥ ↔ cons exp✝ coef✝ tl✝ = nil

Tactic:
<;>

Goal state after:
case nil
basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ nil.leadingExp = ⊥ ↔ nil = nil

case cons
basis_hd : ℝ → ℝ
basis_tl : Basis
exp✝ : ℝ
coef✝ : MultiseriesExpansion basis_tl
tl✝ : Multiseries basis_hd basis_tl
⊢ (cons exp✝ coef✝ tl✝).leadingExp = ⊥ ↔ cons exp✝ coef✝ tl✝ = nil
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case h_coef
basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ ∀ x ∈ (mk Multiseries.nil 0).seq, x.2.Sorted

pp: case h_Pairwise
basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk Multiseries.nil 0).seq

Tactic:
<;>

Goal state after:
case h_coef
basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ ∀ x ∈ (mk Multiseries.nil 0).seq, x.2.Sorted

case h_Pairwise
basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk Multiseries.nil 0).seq
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case step.left.nil
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Prop
h_base : motive s
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
h : motive (Seq.cons (exp, coef) Seq.nil)
h_tl : (tl_exp, tl_coef) ∈ Seq.nil.head
h_step : leadingExp Seq.nil < ↑exp
⊢ tl_exp < exp

pp: case step.left.cons
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Prop
h_base : motive s
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
x✝ : ℝ × MultiseriesExpansion basis_tl
s✝ : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h : motive (Seq.cons (exp, coef) (Seq.cons x✝ s✝))
h_tl : (tl_exp, tl_coef) ∈ (Seq.cons x✝ s✝).head
h_step : leadingExp (Seq.cons x✝ s✝) < ↑exp
⊢ tl_exp < exp

Tactic:
<;>

Goal state after:
case step.left.nil
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Prop
h_base : motive s
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
h : motive (Seq.cons (exp, coef) Seq.nil)
h_tl : (tl_exp, tl_coef) ∈ Seq.nil.head
h_step : leadingExp Seq.nil < ↑exp
⊢ tl_exp < exp

case step.left.cons
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Prop
h_base : motive s
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
x✝ : ℝ × MultiseriesExpansion basis_tl
s✝ : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h : motive (Seq.cons (exp, coef) (Seq.cons x✝ s✝))
h_tl : (tl_exp, tl_coef) ∈ (Seq.cons x✝ s✝).head
h_step : leadingExp (Seq.cons x✝ s✝) < ↑exp
⊢ tl_exp < exp
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
  simp [Multiseries.Sorted.cons_nil h_coef]

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

Goal state before:
pp: coef : ℝ
exps : UnitMonomial
basis : Basis
h_exps : exps.AllZero
t : Monomial := { coef := coef, unit := exps }
⊢ Tendsto (fun a ↦ t.coef * t.unit.toFun basis a) atTop (𝓝 coef)

Tactic:
convert Filter.Tendsto.const_mul _ (UnitMonomial.toFun_tendsto_one_of_allZero h_exps)

Goal state after:
case e'_5
coef : ℝ
exps : UnitMonomial
basis : Basis
h_exps : exps.AllZero
t : Monomial := { coef := coef, unit := exps }
⊢ coef = t.coef * 1
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming

Goal state before:
pp: case mp
c : MultiseriesExpansion []
⊢ c.IsZero → c.toReal = 0

pp: case mpr
c : MultiseriesExpansion []
⊢ c.toReal = 0 → c.IsZero

Tactic:
<;>

Goal state after:
case mp
c : MultiseriesExpansion []
⊢ c.IsZero → c.toReal = 0

case mpr
c : MultiseriesExpansion []
⊢ c.toReal = 0 → c.IsZero
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming

Goal state before:
pp: case nil
basis_hd✝ : ℝ → ℝ
basis_tl✝ : List (ℝ → ℝ)
f✝ : ℝ → ℝ
h_approx : (mk Multiseries.nil f✝).Approximates
⊢ (mk Multiseries.nil f✝).toFun =ᶠ[atTop] 0

Tactic:
simpa using h_approx

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

Goal state before:
pp: case nil
basis_hd : ℝ → ℝ
basis_tl : Basis
f✝ : ℝ → ℝ
⊢ (mk Multiseries.nil f✝).seq.Trimmed

pp: case cons
basis_hd : ℝ → ℝ
basis_tl : Basis
exp✝ : ℝ
f✝ : ℝ → ℝ
coef✝ : MultiseriesExpansion basis_tl
h_trimmed✝ : coef✝.Trimmed
h_ne_zero✝ : ¬coef✝.IsZero
tl✝ : Multiseries basis_hd basis_tl
⊢ (mk (Multiseries.cons exp✝ coef✝ tl✝) f✝).seq.Trimmed

Tactic:
<;>

Goal state after:
case nil
basis_hd : ℝ → ℝ
basis_tl : Basis
f✝ : ℝ → ℝ
⊢ (mk Multiseries.nil f✝).seq.Trimmed

case cons
basis_hd : ℝ → ℝ
basis_tl : Basis
exp✝ : ℝ
f✝ : ℝ → ℝ
coef✝ : MultiseriesExpansion basis_tl
h_trimmed✝ : coef✝.Trimmed
h_ne_zero✝ : ¬coef✝.IsZero
tl✝ : Multiseries basis_hd basis_tl
⊢ (mk (Multiseries.cons exp✝ coef✝ tl✝) f✝).seq.Trimmed
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming

Goal state before:
pp: case cons.h_trimmed
basis_hd : ℝ → ℝ
basis_tl : Basis
exp✝ : ℝ
f✝ : ℝ → ℝ
coef✝ : MultiseriesExpansion basis_tl
h_trimmed✝ : coef✝.Trimmed
h_ne_zero✝ : ¬coef✝.IsZero
tl✝ : Multiseries basis_hd basis_tl
⊢ coef✝.Trimmed

pp: case cons.h_ne_zero
basis_hd : ℝ → ℝ
basis_tl : Basis
exp✝ : ℝ
f✝ : ℝ → ℝ
coef✝ : MultiseriesExpansion basis_tl
h_trimmed✝ : coef✝.Trimmed
h_ne_zero✝ : ¬coef✝.IsZero
tl✝ : Multiseries basis_hd basis_tl
⊢ ¬coef✝.IsZero

Tactic:
<;>

Goal state after:
case cons.h_trimmed
basis_hd : ℝ → ℝ
basis_tl : Basis
exp✝ : ℝ
f✝ : ℝ → ℝ
coef✝ : MultiseriesExpansion basis_tl
h_trimmed✝ : coef✝.Trimmed
h_ne_zero✝ : ¬coef✝.IsZero
tl✝ : Multiseries basis_hd basis_tl
⊢ coef✝.Trimmed

case cons.h_ne_zero
basis_hd : ℝ → ℝ
basis_tl : Basis
exp✝ : ℝ
f✝ : ℝ → ℝ
coef✝ : MultiseriesExpansion basis_tl
h_trimmed✝ : coef✝.Trimmed
h_ne_zero✝ : ¬coef✝.IsZero
tl✝ : Multiseries basis_hd basis_tl
⊢ ¬coef✝.IsZero
Module: Mathlib.Tactic.DeriveEncodable

Goal state before:
pp: case isTrue
a b : ℕ
h : a ≠ 0
this✝ : a ≤ a * a
this : b ≤ b * b
h✝ : a < b
⊢ b < b * b + a

pp: case isFalse
a b : ℕ
h : a ≠ 0
this✝ : a ≤ a * a
this : b ≤ b * b
h✝ : ¬a < b
⊢ b < a * a + a + b

Tactic:
<;>

Goal state after:
case isTrue
a b : ℕ
h : a ≠ 0
this✝ : a ≤ a * a
this : b ≤ b * b
h✝ : a < b
⊢ b < b * b + a

case isFalse
a b : ℕ
h : a ≠ 0
this✝ : a ≤ a * a
this : b ≤ b * b
h✝ : ¬a < b
⊢ b < a * a + a + b
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case nil
f basis_hd : ℝ → ℝ
basis_tl : Basis
f✝ : ℝ → ℝ
hf✝ : f✝ =ᶠ[atTop] 0
h_ms : mk Multiseries.nil f = mk Multiseries.nil f✝
⊢ f =ᶠ[atTop] 0

pp: case cons
f basis_hd : ℝ → ℝ
basis_tl : Basis
f✝ : ℝ → ℝ
exp✝ : ℝ
h_maj✝ : Majorized f✝ basis_hd exp✝
coef✝ : MultiseriesExpansion basis_tl
h_coef✝ : coef✝.Approximates
tl✝ : Multiseries basis_hd basis_tl
h_tl✝ : (mk tl✝ (f✝ - basis_hd ^ exp✝ * coef✝.toFun)).Approximates
h_ms : mk Multiseries.nil f = mk (Multiseries.cons exp✝ coef✝ tl✝) f✝
⊢ f =ᶠ[atTop] 0

Tactic:
<;>

Goal state after:
case nil
f basis_hd : ℝ → ℝ
basis_tl : Basis
f✝ : ℝ → ℝ
hf✝ : f✝ =ᶠ[atTop] 0
h_ms : mk Multiseries.nil f = mk Multiseries.nil f✝
⊢ f =ᶠ[atTop] 0

case cons
f basis_hd : ℝ → ℝ
basis_tl : Basis
f✝ : ℝ → ℝ
exp✝ : ℝ
h_maj✝ : Majorized f✝ basis_hd exp✝
coef✝ : MultiseriesExpansion basis_tl
h_coef✝ : coef✝.Approximates
tl✝ : Multiseries basis_hd basis_tl
h_tl✝ : (mk tl✝ (f✝ - basis_hd ^ exp✝ * coef✝.toFun)).Approximates
h_ms : mk Multiseries.nil f = mk (Multiseries.cons exp✝ coef✝ tl✝) f✝
⊢ f =ᶠ[atTop] 0
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case nil
f basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
f✝ : ℝ → ℝ
hf✝ : f✝ =ᶠ[atTop] 0
h_ms : mk (Multiseries.cons exp coef tl) f = mk Multiseries.nil f✝
⊢ coef.Approximates ∧ Majorized f basis_hd exp ∧ (mk tl (f - basis_hd ^ exp * coef.toFun)).Approximates

pp: case cons
f basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
f✝ : ℝ → ℝ
exp✝ : ℝ
h_maj✝ : Majorized f✝ basis_hd exp✝
coef✝ : MultiseriesExpansion basis_tl
h_coef✝ : coef✝.Approximates
tl✝ : Multiseries basis_hd basis_tl
h_tl✝ : (mk tl✝ (f✝ - basis_hd ^ exp✝ * coef✝.toFun)).Approximates
h_ms : mk (Multiseries.cons exp coef tl) f = mk (Multiseries.cons exp✝ coef✝ tl✝) f✝
⊢ coef.Approximates ∧ Majorized f basis_hd exp ∧ (mk tl (f - basis_hd ^ exp * coef.toFun)).Approximates

Tactic:
<;>

Goal state after:
case nil
f basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
f✝ : ℝ → ℝ
hf✝ : f✝ =ᶠ[atTop] 0
h_ms : mk (Multiseries.cons exp coef tl) f = mk Multiseries.nil f✝
⊢ coef.Approximates ∧ Majorized f basis_hd exp ∧ (mk tl (f - basis_hd ^ exp * coef.toFun)).Approximates

case cons
f basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
f✝ : ℝ → ℝ
exp✝ : ℝ
h_maj✝ : Majorized f✝ basis_hd exp✝
coef✝ : MultiseriesExpansion basis_tl
h_coef✝ : coef✝.Approximates
tl✝ : Multiseries basis_hd basis_tl
h_tl✝ : (mk tl✝ (f✝ - basis_hd ^ exp✝ * coef✝.toFun)).Approximates
h_ms : mk (Multiseries.cons exp coef tl) f = mk (Multiseries.cons exp✝ coef✝ tl✝) f✝
⊢ coef.Approximates ∧ Majorized f basis_hd exp ∧ (mk tl (f - basis_hd ^ exp * coef.toFun)).Approximates
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case lt
a : ONote
ha : a.NF
b : ONote
hb : b.NF
this : (a.cmp b).Compares a b
h : a.cmp b = Ordering.lt
⊢ Ordering.lt.Compares ⟨a, ha⟩ ⟨b, hb⟩

pp: case eq
a : ONote
ha : a.NF
b : ONote
hb : b.NF
this : (a.cmp b).Compares a b
h : a.cmp b = Ordering.eq
⊢ Ordering.eq.Compares ⟨a, ha⟩ ⟨b, hb⟩

pp: case gt
a : ONote
ha : a.NF
b : ONote
hb : b.NF
this : (a.cmp b).Compares a b
h : a.cmp b = Ordering.gt
⊢ Ordering.gt.Compares ⟨a, ha⟩ ⟨b, hb⟩

Tactic:
<;>

Goal state after:
case lt
a : ONote
ha : a.NF
b : ONote
hb : b.NF
this : (a.cmp b).Compares a b
h : a.cmp b = Ordering.lt
⊢ Ordering.lt.Compares ⟨a, ha⟩ ⟨b, hb⟩

case eq
a : ONote
ha : a.NF
b : ONote
hb : b.NF
this : (a.cmp b).Compares a b
h : a.cmp b = Ordering.eq
⊢ Ordering.eq.Compares ⟨a, ha⟩ ⟨b, hb⟩

case gt
a : ONote
ha : a.NF
b : ONote
hb : b.NF
this : (a.cmp b).Compares a b
h : a.cmp b = Ordering.gt
⊢ Ordering.gt.Compares ⟨a, ha⟩ ⟨b, hb⟩
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case lt
a : ONote
ha : a.NF
b : ONote
hb : b.NF
h : a.cmp b = Ordering.lt
this : Ordering.lt.Compares a b
⊢ Ordering.lt.Compares ⟨a, ha⟩ ⟨b, hb⟩

pp: case eq
a : ONote
ha : a.NF
b : ONote
hb : b.NF
h : a.cmp b = Ordering.eq
this : Ordering.eq.Compares a b
⊢ Ordering.eq.Compares ⟨a, ha⟩ ⟨b, hb⟩

pp: case gt
a : ONote
ha : a.NF
b : ONote
hb : b.NF
h : a.cmp b = Ordering.gt
this : Ordering.gt.Compares a b
⊢ Ordering.gt.Compares ⟨a, ha⟩ ⟨b, hb⟩

Tactic:
<;>

Goal state after:
case lt
a : ONote
ha : a.NF
b : ONote
hb : b.NF
h : a.cmp b = Ordering.lt
this : Ordering.lt.Compares a b
⊢ Ordering.lt.Compares ⟨a, ha⟩ ⟨b, hb⟩

case eq
a : ONote
ha : a.NF
b : ONote
hb : b.NF
h : a.cmp b = Ordering.eq
this : Ordering.eq.Compares a b
⊢ Ordering.eq.Compares ⟨a, ha⟩ ⟨b, hb⟩

case gt
a : ONote
ha : a.NF
b : ONote
hb : b.NF
h : a.cmp b = Ordering.gt
this : Ordering.gt.Compares a b
⊢ Ordering.gt.Compares ⟨a, ha⟩ ⟨b, hb⟩
Module: Mathlib.Tactic.ITauto

Goal state before:
pp: case and
q : AndKind
⊢ Ordering

pp: case iff
q : AndKind
⊢ Ordering

pp: case eq
q : AndKind
⊢ Ordering

Tactic:
<;>

Goal state after:
case and
q : AndKind
⊢ Ordering

case iff
q : AndKind
⊢ Ordering

case eq
q : AndKind
⊢ Ordering
Module: Mathlib.Tactic.ITauto

Goal state before:
pp: case var
q : IProp
a✝ : Nat
⊢ Ordering

pp: case true
q : IProp
⊢ Ordering

pp: case false
q : IProp
⊢ Ordering

pp: case and'
q : IProp
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

pp: case or
q a✝¹ a✝ : IProp
⊢ Ordering

pp: case imp
q a✝¹ a✝ : IProp
⊢ Ordering

Tactic:
<;>

Goal state after:
case var
q : IProp
a✝ : Nat
⊢ Ordering

case true
q : IProp
⊢ Ordering

case false
q : IProp
⊢ Ordering

case and'
q : IProp
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

case or
q a✝¹ a✝ : IProp
⊢ Ordering

case imp
q a✝¹ a✝ : IProp
⊢ Ordering
Module: Mathlib.Tactic.NormNum.IsSquare

Goal state before:
pp: case ha
a : ℚ
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
ha : IsRat a (Int.negOfNat n) d
q : ℚ
hq : -(↑n / ↑d) = q * q
⊢ 0 < ↑n

pp: case hb
a : ℚ
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
ha : IsRat a (Int.negOfNat n) d
q : ℚ
hq : -(↑n / ↑d) = q * q
⊢ 0 < ↑d

Tactic:
<;>

Goal state after:
case ha
a : ℚ
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
ha : IsRat a (Int.negOfNat n) d
q : ℚ
hq : -(↑n / ↑d) = q * q
⊢ 0 < ↑n

case hb
a : ℚ
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
ha : IsRat a (Int.negOfNat n) d
q : ℚ
hq : -(↑n / ↑d) = q * q
⊢ 0 < ↑d
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: case inr
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 ↑a = 1
hc' : c ≠ 0
this : NeZero c
⊢ jacobiSymNat a b = r

Tactic:
← Nat.mod_add_div b 2,

Goal state after:
case inr
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 ↑a = 1
hc' : c ≠ 0
this : NeZero c
⊢ jacobiSymNat a (b % 2 + 2 * (b / 2)) = r
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: case neg.hd
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
ha : a ≠ x ^ d
hx' : x' = ↑x
h : ↑a / ↑b = ↑x ^ d / ↑y ^ d
⊢ ↑y ^ d ≠ 0

pp: case neg
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
ha : a ≠ x ^ d
hx' : x' = ↑x
h : ↑a * ↑y ^ d = ↑x ^ d * ↑b
⊢ False

Tactic:
· simp [y]

Goal state after:
case neg
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
ha : a ≠ x ^ d
hx' : x' = ↑x
h : ↑a * ↑y ^ d = ↑x ^ d * ↑b
⊢ False
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
hy_den_pos : 0 < y_den
hx_inv : Invertible ↑x_den
hx_eq : x = ↑x_num * ⅟↑x_den
hy_inv : Invertible ↑y_den
hy_eq : y = ↑y_num * ⅟↑y_den
h1 : ↑y_num * ⅟↑y_den = ↑(↑y_num / ↑y_den)
⊢ Irrational ((↑x_num * ⅟↑x_den) ^ (↑y_num * ⅟↑y_den))

Tactic:
have h2 : (x_num * ⅟(x_den : ℝ) : ℝ) = ((x_num / x_den : ℚ) : ℝ) := by
    simp
    rfl

Goal state after:
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
hy_den_pos : 0 < y_den
hx_inv : Invertible ↑x_den
hx_eq : x = ↑x_num * ⅟↑x_den
hy_inv : Invertible ↑y_den
hy_eq : y = ↑y_num * ⅟↑y_den
h1 : ↑y_num * ⅟↑y_den = ↑(↑y_num / ↑y_den)
h2 : ↑x_num * ⅟↑x_den = ↑(↑x_num / ↑x_den)
⊢ Irrational ((↑x_num * ⅟↑x_den) ^ (↑y_num * ⅟↑y_den))
Module: Mathlib.Tactic.PNatToNat

Goal state before:
pp: case pos
val✝¹ : ℕ
property✝¹ : 0 < val✝¹
val✝ : ℕ
property✝ : 0 < val✝
h✝ : val✝ < val✝¹
⊢ val✝¹ - val✝ = val✝¹ - 1 - val✝ + 1

pp: case neg
val✝¹ : ℕ
property✝¹ : 0 < val✝¹
val✝ : ℕ
property✝ : 0 < val✝
h✝ : ¬val✝ < val✝¹
⊢ 1 = val✝¹ - 1 - val✝ + 1

Tactic:
<;>

Goal state after:
case pos
val✝¹ : ℕ
property✝¹ : 0 < val✝¹
val✝ : ℕ
property✝ : 0 < val✝
h✝ : val✝ < val✝¹
⊢ val✝¹ - val✝ = val✝¹ - 1 - val✝ + 1

case neg
val✝¹ : ℕ
property✝¹ : 0 < val✝¹
val✝ : ℕ
property✝ : 0 < val✝
h✝ : ¬val✝ < val✝¹
⊢ 1 = val✝¹ - 1 - val✝ + 1
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case pos
α : Type u
inst✝ : DecidableEq α
xs : List (α × α)
x y z : α
h✝ : y = x
⊢ (some z).getD x = z

pp: case neg
α : Type u
inst✝ : DecidableEq α
xs : List (α × α)
x y z : α
h✝ : ¬y = x
⊢ (dlookup x (map Prod.toSigma xs)).getD x = (dlookup x (map Prod.toSigma xs)).getD x

Tactic:
<;>

Goal state after:
case pos
α : Type u
inst✝ : DecidableEq α
xs : List (α × α)
x y z : α
h✝ : y = x
⊢ (some z).getD x = z

case neg
α : Type u
inst✝ : DecidableEq α
xs : List (α × α)
x y z : α
h✝ : ¬y = x
⊢ (dlookup x (map Prod.toSigma xs)).getD x = (dlookup x (map Prod.toSigma xs)).getD x