mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ IsOpen (imageOfDf f)

Tactic:
rw [imageOfDf, ofPred_exists fun i (x : PrimeSpectrum R) => coeff f i ∉ x.asIdeal]

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ IsOpen (⋃ i, {x | f.coeff i ∉ x.asIdeal})
Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
U : Set (PrimeSpectrum R[X])
s : Set R[X]
z : zeroLocus s = Uᶜ
⊢ IsOpen (PrimeSpectrum.comap C '' ⋃ i, (zeroLocus {↑i})ᶜ)

Tactic:
image_iUnion

Goal state after:
R : Type u_1
inst✝ : CommRing R
U : Set (PrimeSpectrum R[X])
s : Set R[X]
z : zeroLocus s = Uᶜ
⊢ IsOpen (⋃ i, PrimeSpectrum.comap C '' (zeroLocus {↑i})ᶜ)
Module: Mathlib.RingTheory.Valuation.Quotient

Goal state before:
pp: case a
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
⊢ (v.onQuot hJ).supp ≤ Ideal.map (Ideal.Quotient.mk J) v.supp

Tactic:
rintro ⟨x⟩ hx

Goal state after:
case a.mk
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
x✝ : R ⧸ J
x : R
hx : Quot.mk (⇑(Submodule.quotientRel J)) x ∈ (v.onQuot hJ).supp
⊢ Quot.mk (⇑(Submodule.quotientRel J)) x ∈ Ideal.map (Ideal.Quotient.mk J) v.supp
Module: Mathlib.RingTheory.Valuation.Extension

Goal state before:
pp: R : Type u_1
A : Type u_2
ΓR✝ : Type u_3
ΓA✝ : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring A
inst✝⁸ : LinearOrderedCommMonoidWithZero ΓR✝
inst✝⁷ : LinearOrderedCommMonoidWithZero ΓA✝
inst✝⁶ : Algebra R A
vR✝ : Valuation R ΓR✝
vA✝ : Valuation A ΓA✝
K : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Algebra K A
ΓR : Type u_6
ΓA : Type u_7
ΓK : Type u_8
inst✝³ : LinearOrderedCommGroupWithZero ΓR
inst✝² : LinearOrderedCommGroupWithZero ΓK
inst✝¹ : LinearOrderedCommGroupWithZero ΓA
vR : Valuation R ΓR
vK : Valuation K ΓK
vA : Valuation A ΓA
inst✝ : vR.HasExtension vA
x : ↥vR.integer
y : ↥vA.integer
z : A
⊢ ((algebraMap ↥vR.integer ↥vA.integer) x * y) • z = (algebraMap (↥vR.integer) A) x * y • z

Tactic:
exact mul_assoc _ _ _

Goal state after:
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: case e'_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∑ i ∈ range (n + 1), ↑p ^ i * wittStructureInt p (X 0 * X 1) i ^ p ^ (n - i) =
    ∑ x ∈ range (n + 1), (bind₁ (wittStructureInt p (X 0 * X 1))) ((monomial (Finsupp.single x (p ^ (n - x)))) (↑p ^ x))

Tactic:
congr 1 with i

Goal state after:
case e'_2.e_f
p : ℕ
hp : Fact (Nat.Prime p)
n i : ℕ
m✝ : Fin 2 × ℕ →₀ ℕ
⊢ MvPolynomial.coeff m✝ (↑p ^ i * wittStructureInt p (X 0 * X 1) i ^ p ^ (n - i)) =
    MvPolynomial.coeff m✝
      ((bind₁ (wittStructureInt p (X 0 * X 1))) ((monomial (Finsupp.single i (p ^ (n - i)))) (↑p ^ i)))
Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1))).degree = ↑p
⊢ a₂.coeff 0 ^ p ^ (n + 1) ≠ 0

Tactic:
· exact pow_ne_zero _ ha₂

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
s t : Set α
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
hα : cof α ≠ ℵ₀
⊢ IsStationary (s ∪ t) ↔ IsStationary s ∨ IsStationary t

Tactic:
simpa using isStationary_sUnion_iff_of_countable (s := {s, t}) hα

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case C1.antisymm.refl
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂✝ : Lists' α true
l₂ : l₁.Subset l₂✝
a✝ : l₂✝.Subset l₁
h₁ : of' l₁ ~ ⟨true, l₂✝⟩
h₂ : ⟨true, l₂✝⟩ ~ ⟨true, l₂✝⟩
⊢ of' l₁ ~ ⟨true, l₂✝⟩

Tactic:
exact h₁

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

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
⊢ ∃ a < (succ #α).ord, ∃ b < (succ #α).ord, a ≠ b ∧ lfpApprox f x a = lfpApprox f x b

Tactic:
have h_ninj := not_injective_limitation_set <| lfpApprox f x

Goal state after:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj : ¬Set.InjOn (lfpApprox f x) (Set.Iio (SuccOrder.succ #α).ord)
⊢ ∃ a < (succ #α).ord, ∃ b < (succ #α).ord, a ≠ b ∧ lfpApprox f x a = lfpApprox f x b
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a o₁ : Ordinal.{u}
⊢ ∀ ⦃b : Ordinal.{u}⦄, o₁ < b → veblenWith f o₁ a ≤ veblenWith f b a

Tactic:
o₂

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a o₁ o₂ : Ordinal.{u}
⊢ o₁ < o₂ → veblenWith f o₁ a ≤ veblenWith f o₂ a
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o₁ : Ordinal.{u}
⊢ ∀ ⦃b : Ordinal.{u}⦄, o₁ < b → (fun x ↦ veblenWith f x 0) o₁ < (fun x ↦ veblenWith f x 0) b

Tactic:
o₂

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o₁ o₂ : Ordinal.{u}
⊢ o₁ < o₂ → (fun x ↦ veblenWith f x 0) o₁ < (fun x ↦ veblenWith f x 0) o₂
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x y : ZFSet.{u}
x✝² x✝¹ : PSet.{u}
α✝ : Type u
A✝ : α✝ → PSet.{u}
x✝ : ⟦x✝¹⟧ ∈ ⟦PSet.mk α✝ A✝⟧
a : (PSet.mk α✝ A✝).Type
ya : x✝¹.Equiv ((PSet.mk α✝ A✝).Func a)
⊢ ZFSet.mk (Definable₁.out f x✝¹) ∈ image f (ZFSet.mk (PSet.mk α✝ A✝))

Tactic:
exact ⟨a, Definable₁.out_equiv f ya⟩

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

Goal state before:
pp: x : Ordinal.{u}
⊢ ω ^ x ∈ range (veblen x.invVeblen₁)

Tactic:
by_cases h : invVeblen₁ x = 0

Goal state after:
case pos
x : Ordinal.{u}
h : x.invVeblen₁ = 0
⊢ ω ^ x ∈ range (veblen x.invVeblen₁)

case neg
x : Ordinal.{u}
h : ¬x.invVeblen₁ = 0
⊢ ω ^ x ∈ range (veblen x.invVeblen₁)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case gt
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h₂ : (e₂.oadd n₂ a₂).NF
h' : (a₁.sub a₂).NFBelow e₁.repr
this : (e₁.cmp e₂).Compares e₁ e₂
h : e₁.cmp e₂ = Ordering.gt
⊢ (match Ordering.gt with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match (↑n₁).sub ↑n₂ with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁).NFBelow
    b

Tactic:
exact h₁

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

Goal state before:
pp: x y : ZFSet.{u}
hx : x.IsTransitive
hy : y.IsTransitive
z : ZFSet.{u}
hz : z ∈ x ∩ y
w : ZFSet.{u}
hw : w ∈ z
⊢ w ∈ x ∩ y

Tactic:
rw [mem_inter] at hz ⊢
  exact ⟨hx.mem_trans hw hz.1, hy.mem_trans hw hz.2⟩

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

Goal state before:
pp: case inl
y : ZFSet.{u}
hy : y.IsTransitive
y✝ : ZFSet.{u}
hx : y✝.IsTransitive
⊢ y✝.IsTransitive

pp: case inr
x : ZFSet.{u}
hx : x.IsTransitive
y✝ : ZFSet.{u}
hy : y✝.IsTransitive
⊢ y✝.IsTransitive

Tactic:
assumption'

Goal state after:
Module: Mathlib.Tactic.AddGroup

Goal state before:
pp: G : Type u_1
inst✝ : AddGroup G
a b : G
⊢ a + -b + -b = a + -2 • b

Tactic:
rw [add_assoc, _neg_neg_trick]

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

Goal state before:
pp: case zero
x✝ : NF 0
h₂ : zero.NF
⊢ (0 * zero).NF

Tactic:
exact NF.zero

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

Goal state before:
pp: case oadd
x✝ : NF 0
a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
h₂ : (a✝².oadd a✝¹ a✝).NF
⊢ (0 * a✝².oadd a✝¹ a✝).NF

Tactic:
exact NF.zero

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

Goal state before:
pp: case zero.zero
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
⊢ (match 0, 0 with
    | x, 0 => 0
    | 0, m.succ => e.oadd m.succPNat 0
    | k.succ, m => (e + a0.mulNat k).scale a + e.opowAux a0 a k m).NF

Tactic:
exact NF.zero

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

Goal state before:
pp: case zero.succ
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
n✝ : ℕ
⊢ (match n✝ + 1, 0 with
    | x, 0 => 0
    | 0, m.succ => e.oadd m.succPNat 0
    | k.succ, m => (e + a0.mulNat k).scale a + e.opowAux a0 a k m).NF

Tactic:
exact NF.zero

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

Goal state before:
pp: case neg
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
na : zero.NF
e₁ : o₁.split = (zero, 0)
h : ¬o₂ = 0
h' : o₂ ≠ zero
⊢ zero.NF

Tactic:
exact NF.zero

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

Goal state before:
pp: f g b : ℝ → ℝ
exp : ℝ
h_eq : g =ᶠ[atTop] f
h : Majorized f b exp
⊢ Majorized g b exp

Tactic:
simp only [Majorized] at *

Goal state after:
f g b : ℝ → ℝ
exp : ℝ
h_eq : g =ᶠ[atTop] f
h : ∀ exp' > exp, f =o[atTop] (b ^ exp')
⊢ ∀ exp' > exp, g =o[atTop] (b ^ exp')
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized

Goal state before:
pp: f b : ℝ → ℝ
exp1 exp2 : ℝ
h_lt : exp1 ≤ exp2
h : Majorized f b exp1
⊢ Majorized f b exp2

Tactic:
simp only [Majorized] at *

Goal state after:
f b : ℝ → ℝ
exp1 exp2 : ℝ
h_lt : exp1 ≤ exp2
h : ∀ exp' > exp1, f =o[atTop] (b ^ exp')
⊢ ∀ exp' > exp2, f =o[atTop] (b ^ exp')
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized

Goal state before:
pp: f g b : ℝ → ℝ
exp f_exp g_exp : ℝ
hf : Majorized f b f_exp
hg : Majorized g b g_exp
hf_exp : f_exp ≤ exp
hg_exp : g_exp ≤ exp
⊢ Majorized (f + g) b exp

Tactic:
simp only [Majorized] at *

Goal state after:
f g b : ℝ → ℝ
exp f_exp g_exp : ℝ
hf : ∀ exp' > f_exp, f =o[atTop] (b ^ exp')
hg : ∀ exp' > g_exp, g =o[atTop] (b ^ exp')
hf_exp : f_exp ≤ exp
hg_exp : g_exp ≤ exp
⊢ ∀ exp' > exp, (f + g) =o[atTop] (b ^ exp')
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized

Goal state before:
pp: f g b : ℝ → ℝ
f_exp g_exp : ℝ
hf : Majorized f b f_exp
hg : Majorized g b g_exp
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
⊢ Majorized (f * g) b (f_exp + g_exp)

Tactic:
simp only [Majorized] at *

Goal state after:
f g b : ℝ → ℝ
f_exp g_exp : ℝ
hf : ∀ exp' > f_exp, f =o[atTop] (b ^ exp')
hg : ∀ exp' > g_exp, g =o[atTop] (b ^ exp')
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
⊢ ∀ exp' > f_exp + g_exp, (f * g) =o[atTop] (b ^ exp')
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis

Goal state before:
pp: f g : ℝ → ℝ
a b : ℝ
hf : ∀ᶠ (x : ℝ) in atTop, 0 < f x
hg : Tendsto g atTop atTop
h : (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
hb : 0 < b
⊢ b • Real.log ∘ g - a • Real.log ∘ f ~[atTop] b • Real.log ∘ g

Tactic:
replace h : (a • Real.log ∘ f) =o[atTop] (b • Real.log ∘ g) :=
      (h.const_mul_left a).const_mul_right (hb.ne')

Goal state after:
f g : ℝ → ℝ
a b : ℝ
hf : ∀ᶠ (x : ℝ) in atTop, 0 < f x
hg : Tendsto g atTop atTop
hb : 0 < b
h : (a • Real.log ∘ f) =o[atTop] (b • Real.log ∘ g)
⊢ b • Real.log ∘ g - a • Real.log ∘ f ~[atTop] b • Real.log ∘ g
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
motive : (Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl) → Prop
h_base : motive op✝
h_step :
  ∀ (op : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl),
    motive op →
      ∃ T,
        ∀ (s : Multiseries basis_hd basis_tl),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (exp, coef, opf, op') => (exp, coef, ↑opf (↑op' s.tail)))
              (T s.head)
op : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl) → Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h_op : motive op
⊢ ∃ T,
    ∀ (s : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)),
      (op s).destruct =
        Option.map
          (fun x ↦
            match x with
            | (hd, opf, op') => (hd, ↑opf (↑op' s.tail)))
          (T s.head)

Tactic:
obtain ⟨T, hT⟩ := h_step op h_op

Goal state after:
basis_hd : ℝ → ℝ
basis_tl : Basis
op✝ : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
motive : (Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl) → Prop
h_base : motive op✝
h_step :
  ∀ (op : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl),
    motive op →
      ∃ T,
        ∀ (s : Multiseries basis_hd basis_tl),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (exp, coef, opf, op') => (exp, coef, ↑opf (↑op' s.tail)))
              (T s.head)
op : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl) → Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h_op : motive op
T :
  Option (ℝ × MultiseriesExpansion basis_tl) →
    Option (ℝ × MultiseriesExpansion basis_tl × Subtype FriendlyOperation × Subtype motive)
hT :
  ∀ (s : Multiseries basis_hd basis_tl),
    destruct (op s) =
      Option.map
        (fun x ↦
          match x with
          | (exp, coef, opf, op') => (exp, coef, ↑opf (↑op' s.tail)))
        (T s.head)
⊢ ∃ T,
    ∀ (s : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)),
      (op s).destruct =
        Option.map
          (fun x ↦
            match x with
            | (hd, opf, op') => (hd, ↑opf (↑op' s.tail)))
          (T s.head)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case zero
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
e₁ : o₁.split = (zero, m)
N₁ : zero.NF
r₁ : o₁.repr = zero.repr + ↑m
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

pp: case oadd
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
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

Tactic:
· rcases m with - | m
    · have hzero : (0 : ONote) = zero := rfl
      by_cases h : o₂ = 0
      · subst h; simp [-zero_def, opow_def, opowAux2, e₁, r₁, hzero]
      · have h' := mt repr_inj.1 h
        have hne : o₂ ≠ zero := fun he => h (he ▸ rfl)
        simp [-zero_def, opow_def, opowAux2, e₁, r₁, hne, hzero]
        exact (zero_opow h').symm
    · rcases e₂ : split' o₂ with ⟨b', k⟩
      obtain ⟨_, r₂⟩ := nf_repr_split' e₂
      by_cases h : m = 0
      · simp only [opowAux2, opow_def, e₁, h, r₁, r₂, OfNat.ofNat, Zero.zero, One.one,
          repr]
        simp [opow_add, opow_mul]
      simp only [opow_def, opowAux2, e₁, r₁, e₂, r₂, repr,
          Nat.cast_succ, _root_.zero_add, add_zero]
      rw [opow_add, opow_mul, opow_omega0]
      · simp
      · simpa [Nat.one_le_iff_ne_zero]
      · rw [← Nat.cast_succ, lt_omega0]
        exact ⟨_, rfl⟩

Goal state after:
case oadd
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
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
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
motive : (Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl) → Prop
h_base : motive op✝
h_step :
  ∀ (op : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl),
    motive op →
      ∃ T,
        ∀ (s : Multiseries basis_hd basis_tl),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (exp, coef, opf, op') => (exp, coef, ↑op' (↑opf s.tail)))
              (T s.head)
op : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl) → Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h_op : motive op
⊢ ∃ T,
    ∀ (s : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)),
      (op s).destruct =
        Option.map
          (fun x ↦
            match x with
            | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
          (T s.head)

Tactic:
obtain ⟨T, hT⟩ := h_step op h_op

Goal state after:
basis_hd : ℝ → ℝ
basis_tl : Basis
op✝ : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
motive : (Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl) → Prop
h_base : motive op✝
h_step :
  ∀ (op : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl),
    motive op →
      ∃ T,
        ∀ (s : Multiseries basis_hd basis_tl),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (exp, coef, opf, op') => (exp, coef, ↑op' (↑opf s.tail)))
              (T s.head)
op : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl) → Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h_op : motive op
T :
  Option (ℝ × MultiseriesExpansion basis_tl) →
    Option (ℝ × MultiseriesExpansion basis_tl × Subtype FriendlyOperation × Subtype motive)
hT :
  ∀ (s : Multiseries basis_hd basis_tl),
    destruct (op s) =
      Option.map
        (fun x ↦
          match x with
          | (exp, coef, opf, op') => (exp, coef, ↑op' (↑opf s.tail)))
        (T s.head)
⊢ ∃ T,
    ∀ (s : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)),
      (op s).destruct =
        Option.map
          (fun x ↦
            match x with
            | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
          (T s.head)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons.cons
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⁻¹
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
⊢ (fun a ↦
      (List.zipWith (fun exp b ↦ b a ^ exp) (List.map (fun x ↦ -x) (exp :: exps))
          (basis_hd :: basis_tl)).prod) =ᶠ[atTop]
    fun a ↦ (List.zipWith (fun exp b ↦ b a ^ exp) (exp :: exps) (basis_hd :: basis_tl)).prod⁻¹

Tactic:
apply ((h_basis.head_eventually_pos).and (ih (h_basis.tail))).mono
      intro x ⟨h_pos, ih⟩
      simp only [List.map_cons, List.zipWith_cons_cons, List.prod_cons, mul_inv_rev]
      grind [Real.rpow_neg h_pos.le]

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

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

Tactic:
rw [e, FundamentalSequenceProp] at iha

Goal state after:
case oadd.inl.none.inl.none.zero
a : ONote
m : ℕ+
b : ONote
iha : a = 0
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
e : a.fundamentalSequence = Sum.inl none
e' : m.natPred = 0
⊢ (a.oadd m b).repr = succ zero.repr ∧ ((a.oadd m b).NF → zero.NF)
Module: Mathlib.SetTheory.Ordinal.Notation

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

Tactic:
rw [e, FundamentalSequenceProp] at iha

Goal state after:
case oadd.inl.none.inl.none.succ
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
⊢ (a.oadd m b).repr = succ (zero.oadd m'.succPNat zero).repr ∧ ((a.oadd m b).NF → (zero.oadd m'.succPNat zero).NF)
Module: Mathlib.SetTheory.Ordinal.Notation

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

Tactic:
rw [e, FundamentalSequenceProp] at iha

Goal state after:
case oadd.inl.none.inl.some.zero
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')
e' : m.natPred = 0
⊢ IsSuccLimit (a.oadd m b).repr ∧
    (∀ (i : ℕ),
        a'.oadd i.succPNat zero < a'.oadd (i + 1).succPNat zero ∧
          a'.oadd i.succPNat zero < a.oadd m b ∧ ((a.oadd m b).NF → (a'.oadd i.succPNat zero).NF)) ∧
      ∀ a_1 < (a.oadd m b).repr, ∃ i, a_1 < (a'.oadd i.succPNat zero).repr
Module: Mathlib.SetTheory.Ordinal.Notation

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

Tactic:
rw [e, FundamentalSequenceProp] at iha

Goal state after:
case oadd.inl.none.inl.some.succ
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
⊢ IsSuccLimit (a.oadd m b).repr ∧
    (∀ (i : ℕ),
        a.oadd m'.succPNat (a'.oadd i.succPNat zero) < a.oadd m'.succPNat (a'.oadd (i + 1).succPNat zero) ∧
          a.oadd m'.succPNat (a'.oadd i.succPNat zero) < a.oadd m b ∧
            ((a.oadd m b).NF → (a.oadd m'.succPNat (a'.oadd i.succPNat zero)).NF)) ∧
      ∀ a_1 < (a.oadd m b).repr, ∃ i, a_1 < (a.oadd m'.succPNat (a'.oadd i.succPNat zero)).repr
Module: Mathlib.SetTheory.Ordinal.Notation

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

Tactic:
rw [e, FundamentalSequenceProp] at iha

Goal state after:
case oadd.inl.none.inr.zero
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
e' : m.natPred = 0
⊢ IsSuccLimit (a.oadd m b).repr ∧
    (∀ (i : ℕ),
        (f i).oadd 1 zero < (f (i + 1)).oadd 1 zero ∧
          (f i).oadd 1 zero < a.oadd m b ∧ ((a.oadd m b).NF → ((f i).oadd 1 zero).NF)) ∧
      ∀ a_1 < (a.oadd m b).repr, ∃ i, a_1 < ((f i).oadd 1 zero).repr