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

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

Tactic:
| nil =>

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

Goal state before:
pp: case nil
⊢ zero.Approximates

Tactic:
| nil =>

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

Goal state before:
pp: case nil
r : ℝ
n : Fin [].length
⊢ (monomialRpow [] (↑n) r).toFun = [][n] ^ r

Tactic:
| nil =>

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

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

Tactic:
| nil =>

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

Goal state before:
pp: case nil
n : ℕ
r : ℝ
⊢ (monomialRpow [] n r).Sorted

Tactic:
| nil =>

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

Goal state before:
pp: case nil
r : ℝ
n : Fin [].length
h_basis : WellFormedBasis []
⊢ (monomialRpow [] (↑n) r).Approximates

Tactic:
| nil =>

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

Goal state before:
pp: case oadd.succ
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + ↑m
this✝ : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + ↑m < ω ^ a0.repr
aa : (a' + ↑m).repr = a'.repr + ↑m
b' : ONote
left✝ : b'.NF
k : ℕ
e₂ : o₂.split' = (b', k + 1)
r₂ : o₂.repr = ω * b'.repr + ↑(k + 1)
⊢ ((ω ^ a0.repr) ^ ω) ^ b'.repr *
      ((ω ^ a0.repr) ^ k * (ω ^ a0.repr * ↑↑n + a'.repr) + (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr) =
    ((ω ^ a0.repr) ^ ω) ^ b'.repr * ((ω ^ a0.repr * ↑↑n + (a'.repr + ↑m)) ^ k * (ω ^ a0.repr * ↑↑n + (a'.repr + ↑m)))

Tactic:
← add_assoc ((ω : Ordinal.{0}) ^ repr a0 * (n : ℕ))

Goal state after:
case oadd.succ
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + ↑m
this✝ : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + ↑m < ω ^ a0.repr
aa : (a' + ↑m).repr = a'.repr + ↑m
b' : ONote
left✝ : b'.NF
k : ℕ
e₂ : o₂.split' = (b', k + 1)
r₂ : o₂.repr = ω * b'.repr + ↑(k + 1)
⊢ ((ω ^ a0.repr) ^ ω) ^ b'.repr *
      ((ω ^ a0.repr) ^ k * (ω ^ a0.repr * ↑↑n + a'.repr) + (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr) =
    ((ω ^ a0.repr) ^ ω) ^ b'.repr * ((ω ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ k * (ω ^ a0.repr * ↑↑n + a'.repr + ↑m))
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case nil
x : ℝ
m2 : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : [].length = List.length m2
h_pos : ∀ f ∈ basis, 0 < f x
⊢ (List.zipWith (fun exp b ↦ b x ^ exp) (List.zipWith (fun x1 x2 ↦ x1 + x2) [] m2) basis).prod =
    (List.zipWith (fun exp b ↦ b x ^ exp) [] basis).prod * (List.zipWith (fun exp b ↦ b x ^ exp) m2 basis).prod

Tactic:
| nil =>

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

Goal state before:
pp: case cons.nil
x exp1 : ℝ
exps1 : List ℝ
ih :
  ∀ {m2 : UnitMonomial} {basis : Basis},
    WellFormedBasis basis →
      exps1.length = List.length m2 →
        (∀ f ∈ basis, 0 < f x) →
          (List.zipWith (fun exp b ↦ b x ^ exp) (List.zipWith (fun x1 x2 ↦ x1 + x2) exps1 m2) basis).prod =
            (List.zipWith (fun exp b ↦ b x ^ exp) exps1 basis).prod *
              (List.zipWith (fun exp b ↦ b x ^ exp) m2 basis).prod
basis : Basis
h_basis : WellFormedBasis basis
h_pos : ∀ f ∈ basis, 0 < f x
h_length : (exp1 :: exps1).length = [].length
⊢ (List.zipWith (fun exp b ↦ b x ^ exp) (List.zipWith (fun x1 x2 ↦ x1 + x2) (exp1 :: exps1) []) basis).prod =
    (List.zipWith (fun exp b ↦ b x ^ exp) (exp1 :: exps1) basis).prod *
      (List.zipWith (fun exp b ↦ b x ^ exp) [] basis).prod

Tactic:
| nil =>

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

Goal state before:
pp: case cons.cons.nil
x exp1 : ℝ
exps1 : List ℝ
ih :
  ∀ {m2 : UnitMonomial} {basis : Basis},
    WellFormedBasis basis →
      exps1.length = List.length m2 →
        (∀ f ∈ basis, 0 < f x) →
          (List.zipWith (fun exp b ↦ b x ^ exp) (List.zipWith (fun x1 x2 ↦ x1 + x2) exps1 m2) basis).prod =
            (List.zipWith (fun exp b ↦ b x ^ exp) exps1 basis).prod *
              (List.zipWith (fun exp b ↦ b x ^ exp) m2 basis).prod
exp2 : ℝ
exps2 : List ℝ
h_length : (exp1 :: exps1).length = (exp2 :: exps2).length
h_basis : WellFormedBasis []
h_pos : ∀ f ∈ [], 0 < f x
⊢ (List.zipWith (fun exp b ↦ b x ^ exp) (List.zipWith (fun x1 x2 ↦ x1 + x2) (exp1 :: exps1) (exp2 :: exps2)) []).prod =
    (List.zipWith (fun exp b ↦ b x ^ exp) (exp1 :: exps1) []).prod *
      (List.zipWith (fun exp b ↦ b x ^ exp) (exp2 :: exps2) []).prod

Tactic:
| nil =>

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

Goal state before:
pp: o : ONote
⊢ o.FundamentalSequenceProp o.fundamentalSequence

Tactic:
induction o with
  | zero => exact rfl
  | oadd a m b iha ihb
   =>  _ 

Goal state after:
case oadd
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b.FundamentalSequenceProp b.fundamentalSequence
⊢ (a.oadd m b).FundamentalSequenceProp (a.oadd m b).fundamentalSequence
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case nil
basis : Basis
h_basis : WellFormedBasis basis
⊢ (fun a ↦ (List.zipWith (fun exp b ↦ b a ^ exp) (List.map (fun x ↦ -x) []) basis).prod) =ᶠ[atTop] fun a ↦
    (List.zipWith (fun exp b ↦ b a ^ exp) [] basis).prod⁻¹

Tactic:
| nil =>

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

Goal state before:
pp: case cons.nil
exp : ℝ
exps : List ℝ
ih :
  ∀ {basis : Basis},
    WellFormedBasis basis →
      (fun a ↦ (List.zipWith (fun exp b ↦ b a ^ exp) (List.map (fun x ↦ -x) exps) basis).prod) =ᶠ[atTop] fun a ↦
        (List.zipWith (fun exp b ↦ b a ^ exp) exps basis).prod⁻¹
h_basis : WellFormedBasis []
⊢ (fun a ↦ (List.zipWith (fun exp b ↦ b a ^ exp) (List.map (fun x ↦ -x) (exp :: exps)) []).prod) =ᶠ[atTop] fun a ↦
    (List.zipWith (fun exp b ↦ b a ^ exp) (exp :: exps) []).prod⁻¹

Tactic:
| nil =>

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

Goal state before:
pp: β : Type u_1
γ : Type u_2
basis_hd : ℝ → ℝ
basis_tl : Basis
F : β → Option (ℝ × MultiseriesExpansion basis_tl × γ × β)
op : γ → Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
inst✝ : FriendlyOperationClass op
b : β
h : F b = none
⊢ gcorec F op b = nil

Tactic:
unfold gcorec

Goal state after:
β : Type u_1
γ : Type u_2
basis_hd : ℝ → ℝ
basis_tl : Basis
F : β → Option (ℝ × MultiseriesExpansion basis_tl × γ × β)
op : γ → Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
inst✝ : FriendlyOperationClass op
b : β
h : F b = none
⊢ Seq.gcorec
      (fun a ↦
        Option.map
          (fun x ↦
            match x with
            | (exp, coef, c, next) => ((exp, coef), c, next))
          (F a))
      op b =
    nil
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: β : Type u_1
γ : Type u_2
basis_hd : ℝ → ℝ
basis_tl : Basis
F : β → Option (ℝ × MultiseriesExpansion basis_tl × γ × β)
op : γ → Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
inst✝ : FriendlyOperationClass op
b : β
exp : ℝ
coef : MultiseriesExpansion basis_tl
c : γ
next : β
h : F b = some (exp, coef, c, next)
⊢ gcorec F op b = cons exp coef (op c (gcorec F op next))

Tactic:
unfold gcorec

Goal state after:
β : Type u_1
γ : Type u_2
basis_hd : ℝ → ℝ
basis_tl : Basis
F : β → Option (ℝ × MultiseriesExpansion basis_tl × γ × β)
op : γ → Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
inst✝ : FriendlyOperationClass op
b : β
exp : ℝ
coef : MultiseriesExpansion basis_tl
c : γ
next : β
h : F b = some (exp, coef, c, next)
⊢ Seq.gcorec
      (fun a ↦
        Option.map
          (fun x ↦
            match x with
            | (exp, coef, c, next) => ((exp, coef), c, next))
          (F a))
      op b =
    cons exp coef
      (op c
        (Seq.gcorec
          (fun a ↦
            Option.map
              (fun x ↦
                match x with
                | (exp, coef, c, next) => ((exp, coef), c, next))
              (F a))
          op next))
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case nil
basis_hd : ℝ → ℝ
basis_tl : Basis
h_length : [].length = List.length basis_tl
h_basis : WellFormedBasis (basis_hd :: basis_tl)
⊢ Majorized (toFun [] basis_tl) basis_hd 0

Tactic:
| nil =>

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

Goal state before:
pp: case cons.nil
hd : ℝ
tl : List ℝ
ih :
  ∀ {basis_hd : ℝ → ℝ} {basis_tl : Basis},
    tl.length = List.length basis_tl → WellFormedBasis (basis_hd :: basis_tl) → Majorized (toFun tl basis_tl) basis_hd 0
basis_hd : ℝ → ℝ
h_length : (hd :: tl).length = [].length
h_basis : WellFormedBasis [basis_hd]
⊢ Majorized (toFun (hd :: tl) []) basis_hd 0

Tactic:
| nil =>

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

Goal state before:
pp: case nil
x : ℝ
basis : Basis
h_basis : WellFormedBasis basis
hx : ∀ f ∈ basis, 0 < f x
⊢ 0 < toFun [] basis x

Tactic:
| nil =>

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

Goal state before:
pp: case cons.nil
x exp : ℝ
exps : List ℝ
ih : ∀ {basis : Basis}, WellFormedBasis basis → (∀ f ∈ basis, 0 < f x) → 0 < toFun exps basis x
h_basis : WellFormedBasis []
hx : ∀ f ∈ [], 0 < f x
⊢ 0 < toFun (exp :: exps) [] x

Tactic:
| nil =>

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

Goal state before:
pp: case nil
m : UnitMonomial
right : Basis
⊢ (List.replicate [].length 0 ++ m).toFun ([] ++ right) = m.toFun right

Tactic:
| nil =>

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

Goal state before:
pp: case nil
x : ℝ
basis : Basis
h_basis : WellFormedBasis basis
hx : ∀ f ∈ basis, 0 < f x
⊢ 0 < toFun [] basis x ∧ (log ∘ toFun [] basis) x = toLogFun [] basis x

Tactic:
| nil =>

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

Goal state before:
pp: case cons.nil
x e : ℝ
es : List ℝ
ih :
  ∀ {basis : Basis},
    WellFormedBasis basis →
      (∀ f ∈ basis, 0 < f x) → 0 < toFun es basis x ∧ (log ∘ toFun es basis) x = toLogFun es basis x
h_basis : WellFormedBasis []
hx : ∀ f ∈ [], 0 < f x
⊢ 0 < toFun (e :: es) [] x ∧ (log ∘ toFun (e :: es) []) x = toLogFun (e :: es) [] x

Tactic:
| nil =>

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

Goal state before:
pp: case nil
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Sort u_1
nil : (f : ℝ → ℝ) → motive (mk Multiseries.nil f)
cons :
  (exp : ℝ) →
    (coef : MultiseriesExpansion basis_tl) →
      (tl : Multiseries basis_hd basis_tl) → (f : ℝ → ℝ) → motive (mk (Multiseries.cons exp coef tl) f)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
f : ℝ → ℝ
⊢ motive (Seq.nil, f)

Tactic:
| nil =>

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

Goal state before:
pp: case h.nil
α : 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, ↑opf (↑op' s.tail)))
              (T s.head)
motive' : (Stream'.Seq α → Stream'.Seq α) → Prop :=
  fun op ↦ ∃ opf op', op = opf ∘ op' ∧ FriendlyOperation opf ∧ motive op'
opf op : Stream'.Seq α → Stream'.Seq α
h_opf : FriendlyOperation opf
h_op : motive op
T : Option α → Option (α × Subtype FriendlyOperation × Subtype motive)
s : Stream'.Seq α
hT :
  nil.destruct =
    Option.map
      (fun x ↦
        match x with
        | (hd, opf, op') => (hd, ↑opf (↑op' s.tail)))
      (T s.head)
⊢ (opf nil).destruct =
    Option.map (fun x ↦ (x.1, ↑x.2 s.tail))
      (match T s.head with
      | none => Option.map (fun x ↦ (x.1, ⟨(fun x_1 ↦ ↑x.2 nil) ∘ op, ⋯⟩)) (h_opf.unfold none)
      | some (hd, opf', op') => Option.map (fun x ↦ (x.1, ⟨(↑x.2 ∘ ↑opf') ∘ ↑op', ⋯⟩)) (h_opf.unfold (some hd)))

Tactic:
| nil =>

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

Goal state before:
pp: case nil
exps_hd : ℝ
basis_hd : ℝ → ℝ
h_nonzero : exps_hd ≠ 0
basis_tl : Basis
hlo : ∀ b ∈ basis_tl, (log ∘ b) =o[atTop] (log ∘ basis_hd)
⊢ toLogFun [] basis_tl =o[atTop] (log ∘ basis_hd)

Tactic:
| nil =>

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

Goal state before:
pp: case cons.nil
exps_hd : ℝ
basis_hd : ℝ → ℝ
h_nonzero : exps_hd ≠ 0
e : ℝ
es : List ℝ
ih :
  ∀ {basis_tl : Basis},
    (∀ b ∈ basis_tl, (log ∘ b) =o[atTop] (log ∘ basis_hd)) → toLogFun es basis_tl =o[atTop] (log ∘ basis_hd)
hlo : ∀ b ∈ [], (log ∘ b) =o[atTop] (log ∘ basis_hd)
⊢ toLogFun (e :: es) [] =o[atTop] (log ∘ basis_hd)

Tactic:
| nil =>

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

Goal state before:
pp: case nil
basis : Basis
h_basis : WellFormedBasis basis
h_length : [].length = List.length basis
h_firstIsPos : FirstNonzeroIsPos []
⊢ Tendsto (toFun [] basis) atTop atTop

Tactic:
| nil =>

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

Goal state before:
pp: case cons.nil
exps_hd : ℝ
exps_tl : List ℝ
h_firstIsPos : FirstNonzeroIsPos (exps_hd :: exps_tl)
h_basis : WellFormedBasis []
h_length : (exps_hd :: exps_tl).length = [].length
⊢ Tendsto (toFun (exps_hd :: exps_tl) []) atTop atTop

Tactic:
| nil =>

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

Goal state before:
pp: case seq.right.nil
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
h_coef : ∀ x ∈ (mk (Multiseries.cons exp coef Multiseries.nil) 0).seq, x.2.Sorted
h_Pairwise : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk (Multiseries.cons exp coef Multiseries.nil) 0).seq
⊢ Multiseries.nil.leadingExp < ↑exp ∧ Multiseries.nil.Sorted

Tactic:
| nil =>

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

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

Tactic:
| nil =>

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

Goal state before:
pp: case cons.nil
exps_hd : ℝ
exps_tl : List ℝ
h_firstIsNeg : FirstNonzeroIsNeg (exps_hd :: exps_tl)
h_basis : WellFormedBasis []
h_length : (exps_hd :: exps_tl).length = [].length
⊢ Tendsto (toFun (exps_hd :: exps_tl) []) atTop (𝓝 0)

Tactic:
| nil =>

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

Goal state before:
pp: case nil
basis : Basis
h_allZero : AllZero []
⊢ Tendsto (toFun [] basis) atTop (𝓝 1)

Tactic:
| nil =>

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

Goal state before:
pp: case cons.nil
exps_hd : ℝ
exps_tl : List ℝ
h_allZero : AllZero (exps_hd :: exps_tl)
⊢ Tendsto (toFun (exps_hd :: exps_tl) []) atTop (𝓝 1)

Tactic:
| nil =>

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

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

Tactic:
| nil =>

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

Goal state before:
pp: case h.nil
α : Type u_1
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
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)
motive' : (Stream'.Seq α → Stream'.Seq α) → Prop :=
  fun op ↦ ∃ opf op', op = op' ∘ opf ∧ FriendlyOperation opf ∧ motive op'
opf op : Stream'.Seq α → Stream'.Seq α
h_opf : FriendlyOperation opf
h_op : motive op
T : Option α → Option (α × Subtype FriendlyOperation × Subtype motive)
hT :
  ∀ (s : Stream'.Seq α),
    (op s).destruct =
      Option.map
        (fun x ↦
          match x with
          | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
        (T s.head)
s : Stream'.Seq α
hF :
  nil.destruct =
    Option.map
      (fun x ↦
        match x with
        | (hd, op') => (hd, ↑op' s.tail))
      (h_opf.unfold s.head)
⊢ (op nil).destruct =
    Option.map (fun x ↦ (x.1, ↑x.2 s.tail))
      (match h_opf.unfold s.head with
      | none => Option.map (fun x ↦ (x.1, ⟨↑x.2.2 ∘ fun x_1 ↦ ↑x.2.1 nil, ⋯⟩)) (T none)
      | some (hd, opf') => Option.map (fun x ↦ (x.1, ⟨↑x.2.2 ∘ ↑x.2.1 ∘ ↑opf', ⋯⟩)) (T (some hd)))

Tactic:
| nil =>

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
  ext x
  simp [smul, toFun]
  ring

Goal state after:
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:
| nil =>

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

Goal state before:
pp: case nil
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
hs : ms.seq = Multiseries.nil
⊢ ms.Trimmed

Tactic:
| nil =>

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

Goal state before:
pp: case nil
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h_ms : Multiseries.cons exp coef tl = Multiseries.nil
⊢ coef.Trimmed ∧ ¬coef.IsZero

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Tactic.Sat.FromLRAT

Goal state before:
pp: case nil
p : Prop
as as₁ : List Prop
⊢ as = as₁.reverseAux [] → (mk as).implies p [] as₁.length → p

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Tactic.Sat.FromLRAT

Goal state before:
pp: case cons.nil
p a : Prop
as : List Prop
⊢ ∀ (n n' : ℕ), n' = [].length + n → ∀ (bs : List Prop), mk ([].reverseAux bs) n' ↔ mk bs n

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case e_opt.nil
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
⊢ Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) []) = List.dlookup x []

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case nil
α : Type u
inst✝ : DecidableEq α
x y : α
ys : List α
h₀ : [].Nodup
h₁ : [].length = ys.length
i : ℕ
h₂ : [][i]? = some x
⊢ applyId ([].zip ys) x = y ↔ ys[i]? = some y

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case some.nil
α : Type u
inst✝ : DecidableEq α
x val : α
ys : List α
h₀ : [].Nodup
h₃ : dlookup x (map Prod.toSigma ([].zip ys)) = some val
h₂ : ys.Nodup
h₁ : [].length = ys.length
⊢ val ∈ ys ↔ x ∈ []

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
⊢ x ∉ (map Prod.toSigma (xs.zip ys)).keys

Tactic:
simp only [List.keys, not_exists, Prod.toSigma, exists_and_right, exists_eq_right, List.mem_map,
    Function.comp_apply, List.map_map, Prod.exists]

Goal state after:
α : Type u
inst✝ : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
⊢ ∀ (x_1 : α), (x, x_1) ∉ xs.zip ys
Module: Mathlib.Topology.Algebra.Group.CompactOpen

Goal state before:
pp: A : Type u_2
B : Type u_3
inst✝⁵ : Monoid A
inst✝⁴ : Monoid B
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
x y : A
⊢ IsClosed {x_1 | x_1 (x * y) = x_1 x * x_1 y}

Tactic:
exact isClosed_eq (continuous_eval_const (x * y)) <|
      .mul (continuous_eval_const x) (continuous_eval_const y)

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type
inst✝ : DecidableEq α
xs✝ : List ((_ : α) × α)
h₀✝ : map Sigma.fst xs✝ ~ map Sigma.snd xs✝
h₁✝ : (map Sigma.snd xs✝).Nodup
xs' ys' : List α
h₀ : xs' ~ ys'
h₁ : ys'.Nodup
h₃ : xs'.length ≤ ys'.length
h₄ : ys'.length ≤ xs'.length
⊢ map Sigma.fst (map Prod.toSigma (xs'.zip ys')) ~ map Sigma.snd (map Prod.toSigma (xs'.zip ys'))

Tactic:
by simp only [comp_def, List.map_fst_zip, List.map_snd_zip, *, Prod.fst_toSigma,
          Prod.snd_toSigma, List.map_map]

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case nil
α : Type u
inst✝ : DecidableEq α
⊢ [] =
    map
      (fun x ↦
        match x with
        | (a, b) => ⟨a, b⟩)
      ((map Sigma.fst []).zip (map Sigma.snd []))

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Topology.Algebra.PontryaginDual

Goal state before:
pp: case refine_2
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : CommGroup G
inst✝⁸ : Group H
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup G
inst✝¹ : IsTopologicalGroup H
inst✝ : CompactSpace A
V : Set (PontryaginDual A) := {ψ | Set.MapsTo (⇑ψ) Set.univ (Circle.centeredArc (π / 2))}
hVopen : IsOpen V
ψ : PontryaginDual A
⊢ ψ = 1 → ψ ∈ V

Tactic:
rintro rfl _ _
      rw [Circle.mem_centeredArc (by linarith [pi_pos])]
      simp [pi_pos]

Goal state after:
Module: Mathlib.Topology.CantorBendixson

Goal state before:
pp: case inl
X : Type u
inst✝ : TopologicalSpace X
s : Set X
a : Ordinal.{u}
ha : sᵈ[a] ∈ fixedPoints ⇑relDerivedSet
i : Ordinal.{u}
hi : i < a
⊢ sᵈ[a] ⊆ sᵈ[i]

Tactic:
exact iteratedDerivedSet_antitone s hi.le

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Subcomplex

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
A : Set X
hA : A ⊆ ↑E
h : (∀ (n : ℕ) (j : ↑(E.I n)), IsClosed[t] (A ∩ ↑(map n ↑j) '' closedBall 0 1)) ∧ IsClosed[t] (A ∩ D)
⊢ IsClosed[t] A

Tactic:
apply isClosed_of_disjoint_openCell_or_isClosed_inter_closedCell
      (subset_trans hA (subset_complex (C := C) E)) h.2
    intro n _ j
    by_cases hj : j ∈ E.I n
    · exact Or.intro_right _ (h.1 n ⟨j, hj⟩)
    · exact Or.intro_left _ ((disjoint_openCell_subcomplex_of_not_mem E hj).symm.mono_left hA)

Goal state after:
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
uux : Ultrafilter (Ultrafilter X.A)
⊢ X.str (X.join uux) = X.str (Ultrafilter.map X.str uux)

Tactic:
by
  change ((β).μ.app _ ≫ X.a) _ = _
  rw [Monad.Algebra.assoc]
  rfl

Goal state after:
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
⊢ IsCompact Set.univ

Tactic:
rw [isCompact_iff_ultrafilter_le_nhds]

Goal state after:
X : Compactum
⊢ ∀ (f : Ultrafilter X.A), ↑f ≤ 𝓟 Set.univ → ∃ x ∈ Set.univ, ↑f ≤ 𝓝 x