mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
f g q : A⟦X⟧
r : A[X]
I : Ideal A
i : ℕ
hi : i < ((map (Ideal.Quotient.mk I)) g).order.toNat
H : f = g * q + ↑r
⊢ (coeff i) (f - ↑r) ∈ I

Tactic:
← sub_eq_iff_eq_add

Goal state after:
A : Type u_1
inst✝ : CommRing A
f g q : A⟦X⟧
r : A[X]
I : Ideal A
i : ℕ
hi : i < ((map (Ideal.Quotient.mk I)) g).order.toNat
H : f - ↑r = g * q
⊢ (coeff i) (f - ↑r) ∈ I
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
t : S ⊗[R] M
ht : (LinearMap.baseChange S f) t = 0
A : Subalgebra R S
hA : A.FG
ht_memA : t ∈ (rTensor M A.val.toLinearMap).range
u : ↥A ⊗[R] M
hu : (rTensor M A.val.toLinearMap) u = t
this :
  (rTensor N A.val.toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0 →
    ∃ B, B.FG ∧ ∃ (x : A ≤ B), (rTensor N (Subalgebra.inclusion ⋯).toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
hu' : (rTensor N A.val.toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
⊢ ∃ A, ∃ (_ : A.FG), ∃ u, (LinearMap.baseChange (↥A) f) u = 0 ∧ (rTensor M A.val.toLinearMap) u = t

Tactic:
obtain ⟨B, hB, hAB, hu'⟩ := this hu'

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
t : S ⊗[R] M
ht : (LinearMap.baseChange S f) t = 0
A : Subalgebra R S
hA : A.FG
ht_memA : t ∈ (rTensor M A.val.toLinearMap).range
u : ↥A ⊗[R] M
hu : (rTensor M A.val.toLinearMap) u = t
this :
  (rTensor N A.val.toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0 →
    ∃ B, B.FG ∧ ∃ (x : A ≤ B), (rTensor N (Subalgebra.inclusion ⋯).toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
hu'✝ : (rTensor N A.val.toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
B : Subalgebra R S
hB : B.FG
hAB : A ≤ B
hu' : (rTensor N (Subalgebra.inclusion ⋯).toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
⊢ ∃ A, ∃ (_ : A.FG), ∃ u, (LinearMap.baseChange (↥A) f) u = 0 ∧ (rTensor M A.val.toLinearMap) u = t
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case eq_mul_add
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
inst✝ : IsAdicComplete I A
hI : I ≠ ⊤
⊢ f = ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) (f - g * H.div f)) + g * H.div f

Tactic:
← sub_eq_iff_eq_add

Goal state after:
case eq_mul_add
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
inst✝ : IsAdicComplete I A
hI : I ≠ ⊤
⊢ f - g * H.div f = ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) (f - g * H.div f))
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case succ
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
heq :
  (mk fun i ↦ (coeff (i + ((map (Ideal.Quotient.mk I)) g).order.toNat)) g) *
        X ^ ((map (Ideal.Quotient.mk I)) g).order.toNat *
      q =
    ↑r - ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g) * q
k : ℕ
ih : ∀ (i : ℕ), (coeff i) q ∈ I ^ k
h1 : ∀ (i : ℕ), (coeff i) ↑r ∈ I ^ (k + 1)
⊢ ∀ (i : ℕ), (coeff i) q ∈ I ^ (k + 1)

Tactic:
replace heq := congr(H.isUnit_shift.unit⁻¹ * $heq)

Goal state after:
case succ
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
k : ℕ
ih : ∀ (i : ℕ), (coeff i) q ∈ I ^ k
h1 : ∀ (i : ℕ), (coeff i) ↑r ∈ I ^ (k + 1)
heq :
  ↑⋯.unit⁻¹ *
      ((mk fun i ↦ (coeff (i + ((map (Ideal.Quotient.mk I)) g).order.toNat)) g) *
          X ^ ((map (Ideal.Quotient.mk I)) g).order.toNat *
        q) =
    ↑⋯.unit⁻¹ * (↑r - ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g) * q)
⊢ ∀ (i : ℕ), (coeff i) q ∈ I ^ (k + 1)
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsAdicComplete I A
f : A⟦X⟧
⊢ (Ideal.Quotient.mk (Ideal.span {g})) ↑(H.mod' ((Ideal.Quotient.mk (Ideal.span {g})) f)) =
    (Ideal.Quotient.mk (Ideal.span {g})) f

Tactic:
mod'_mk_eq_mod,

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsAdicComplete I A
f : A⟦X⟧
⊢ (Ideal.Quotient.mk (Ideal.span {g})) ↑(H.mod f) = (Ideal.Quotient.mk (Ideal.span {g})) f
Module: Mathlib.RingTheory.Regular.ProjectiveDimension

Goal state before:
pp: case coe
R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsLocalRing R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
x : R
reg : IsSMulRegular (↑M) x
mem : x ∈ maximalIdeal R
sub : Subsingleton ↑M ↔ Subsingleton (QuotSMulTop x ↑M)
aux : ∀ (n : ℕ), projectiveDimension (of R (QuotSMulTop x ↑M)) ≤ ↑n ↔ projectiveDimension M + 1 ≤ ↑n
N : ℕ∞
⊢ projectiveDimension (of R (QuotSMulTop x ↑M)) ≤ ↑N ↔ projectiveDimension M + 1 ≤ ↑N

Tactic:
induction N with
    | top => simp
    | coe n => simpa using aux n

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case refine_2
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
H✝ : (X ^ ((map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g q r
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H : (X ^ n).IsWeierstrassDivision g q r
f : A[X] := Polynomial.X ^ n - r
H1 : r.degree < (Polynomial.X ^ n).degree
hfdeg : f.natDegree = n
this : X ^ n * ↑⋯.unit⁻¹ = g + ↑r * ↑⋯.unit⁻¹
⊢ g = ↑f * ↑⋯.unit⁻¹

Tactic:
← sub_eq_iff_eq_add

Goal state after:
case refine_2
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
H✝ : (X ^ ((map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g q r
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H : (X ^ n).IsWeierstrassDivision g q r
f : A[X] := Polynomial.X ^ n - r
H1 : r.degree < (Polynomial.X ^ n).degree
hfdeg : f.natDegree = n
this : X ^ n * ↑⋯.unit⁻¹ - ↑r * ↑⋯.unit⁻¹ = g
⊢ g = ↑f * ↑⋯.unit⁻¹
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
a : A
g : A⟦X⟧
hg : (map (IsLocalRing.residue A)) (a • g) ≠ 0
⊢ (a • g).weierstrassDistinguished hg = g.weierstrassDistinguished ⋯

Tactic:
by
  have H := g.isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit
    (fun h ↦ hg (by simp [Algebra.smul_def, h]))
  have H' := (a • g).isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit hg
  have ha : IsLocalRing.residue A a ≠ 0 := fun h ↦ hg (by simp [Algebra.smul_def, h])
  exact (H'.elim (H.smul (by simpa using ha))).1

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
a b : (ValueGroupWithZero R)ˣ
this : (valuation R).IsEquiv 1
r s : ↥(posSubmonoid R)
hr : (valuation R) ↑r / (valuation R) ↑s = ↑a
t u : ↥(posSubmonoid R)
ht : (valuation R) ↑t / (valuation R) ↑u = ↑b
⊢ (valuation R) ↑r / (valuation R) ↑s = (valuation R) ↑t / (valuation R) ↑u

Tactic:
div_eq_div_iff,

Goal state after:
R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
a b : (ValueGroupWithZero R)ˣ
this : (valuation R).IsEquiv 1
r s : ↥(posSubmonoid R)
hr : (valuation R) ↑r / (valuation R) ↑s = ↑a
t u : ↥(posSubmonoid R)
ht : (valuation R) ↑t / (valuation R) ↑u = ↑b
⊢ (valuation R) ↑r * (valuation R) ↑u = (valuation R) ↑t * (valuation R) ↑s

case hb
R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
a b : (ValueGroupWithZero R)ˣ
this : (valuation R).IsEquiv 1
r s : ↥(posSubmonoid R)
hr : (valuation R) ↑r / (valuation R) ↑s = ↑a
t u : ↥(posSubmonoid R)
ht : (valuation R) ↑t / (valuation R) ↑u = ↑b
⊢ (valuation R) ↑s ≠ 0

case hd
R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
a b : (ValueGroupWithZero R)ˣ
this : (valuation R).IsEquiv 1
r s : ↥(posSubmonoid R)
hr : (valuation R) ↑r / (valuation R) ↑s = ↑a
t u : ↥(posSubmonoid R)
ht : (valuation R) ↑t / (valuation R) ↑u = ↑b
⊢ (valuation R) ↑u ≠ 0
Module: Mathlib.RingTheory.WittVector.Isocrystal

Goal state before:
pp: p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
this✝ : Nontrivial V
x : V
h_dim : ∀ (w : V), ∃ c, c • x = w
hx : x ≠ 0
this : Φ(p, k) x ≠ 0
a : K(p, k)
ha : a • x = Φ(p, k) x
⊢ ∃ a, a ≠ 0 ∧ Φ(p, k) x = a • x

Tactic:
refine ⟨a, ?_, ha.symm⟩

Goal state after:
p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
this✝ : Nontrivial V
x : V
h_dim : ∀ (w : V), ∃ c, c • x = w
hx : x ≠ 0
this : Φ(p, k) x ≠ 0
a : K(p, k)
ha : a • x = Φ(p, k) x
⊢ a ≠ 0
Module: Mathlib.RingTheory.WittVector.Isocrystal

Goal state before:
pp: p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
⊢ StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V

Tactic:
by
    refine LinearEquiv.ofBijective F₀ ⟨?_, ?_⟩
    · rw [← LinearMap.ker_eq_bot]
      exact LinearMap.ker_toSpanSingleton K(p, k) hx
    · rw [← LinearMap.range_eq_top]
      rw [← (finrank_eq_one_iff_of_nonzero x hx).mp h_dim]
      rw [LinearMap.span_singleton_eq_range]

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

Goal state before:
pp: case inl
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
⊢ (coeff b (b ^ e * x + y)) e = (single e x) e + (coeff b y) e

Tactic:
rw [single_eq_same, coeff_eq_zero_of_lt hy, add_zero]
    apply coeff_of_mem_CNF
    rw [CNF.opow_mul_add hb hx hxb hy]
    exact mem_cons_self

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

Goal state before:
pp: e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : e = 0
⊢ a = 0

Tactic:
simpa [e0, NFBelow_zero] using h.snd'

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

Goal state before:
pp: n : ℕ
f : (Fin n → ZFSet.{u}) → ZFSet.{u}
inst✝ : Definable n f
xs ys : Fin n → PSet.{u}
h : ∀ (i : Fin n), xs i ≈ ys i
⊢ ⟦out f xs⟧ = ⟦out f ys⟧

Tactic:
mk_eq,

Goal state after:
n : ℕ
f : (Fin n → ZFSet.{u}) → ZFSet.{u}
inst✝ : Definable n f
xs ys : Fin n → PSet.{u}
h : ∀ (i : Fin n), xs i ≈ ys i
⊢ ZFSet.mk (out f xs) = ⟦out f ys⟧
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: n : ℕ
f : (Fin n → ZFSet.{u}) → ZFSet.{u}
inst✝ : Definable n f
xs ys : Fin n → PSet.{u}
h : ∀ (i : Fin n), xs i ≈ ys i
⊢ ZFSet.mk (out f xs) = ⟦out f ys⟧

Tactic:
mk_eq,

Goal state after:
n : ℕ
f : (Fin n → ZFSet.{u}) → ZFSet.{u}
inst✝ : Definable n f
xs ys : Fin n → PSet.{u}
h : ∀ (i : Fin n), xs i ≈ ys i
⊢ ZFSet.mk (out f xs) = ZFSet.mk (out f ys)
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x z : ZFSet.{u}
zx : z ∈ x
y : ZFSet.{u}
yx : (fun w ↦ z.pair w ∈ map f x) y
w : ZFSet.{u}
left✝ : w ∈ x
we : w.pair (f w) = z.pair y
wz : w = z
fy : f w = y
⊢ y = f z

Tactic:
rw [← fy, wz]

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

Goal state before:
pp: x : Class.{u_1}
y : ZFSet.{u_1}
⊢ (⋃₀ x) y ↔ ∃ z, x z ∧ y ∈ z

Tactic:
by
  constructor
  · rintro ⟨-, ⟨z, rfl, hxz⟩, hyz⟩
    exact ⟨z, hxz, hyz⟩
  · exact fun ⟨z, hxz, hyz⟩ => ⟨_, coe_mem.2 hxz, hyz⟩

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

Goal state before:
pp: ⊢ ⋂₀ ∅ = univ

Tactic:
by
  simp [sInter, Top.top]

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

Goal state before:
pp: f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x y : ZFSet.{u}
h : y ∈ x
z : ZFSet.{u}
x✝ : ∃ z_1 ∈ x, z_1.pair (f z_1) = y.pair z
w : ZFSet.{u}
left✝ : w ∈ x
pr : w.pair (f w) = y.pair z
wy : w = y
fw : f w = z
⊢ f w = f y

Tactic:
wy

Goal state after:
f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x y : ZFSet.{u}
h : y ∈ x
z : ZFSet.{u}
x✝ : ∃ z_1 ∈ x, z_1.pair (f z_1) = y.pair z
w : ZFSet.{u}
left✝ : w ∈ x
pr : w.pair (f w) = y.pair z
wy : w = y
fw : f w = z
⊢ f y = f y
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: case a
o : Ordinal.{u_1}
a✝ : PSet.{u_1}
⊢ ⟦a✝⟧ ∈ mk o.toPSet ↔ ∃ a < o, a.toZFSet = ⟦a✝⟧

Tactic:
mk_eq,

Goal state after:
case a
o : Ordinal.{u_1}
a✝ : PSet.{u_1}
⊢ mk a✝ ∈ mk o.toPSet ↔ ∃ a < o, a.toZFSet = mk a✝
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: case limit.refine_2
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
h : ⨆ i, (V_ ↑i).card < o.card
⊢ (V_ ((⨆ i, (V_ ↑i).card).ord + 1)).card ≤ ⨆ i, (V_ ↑i).card

Tactic:
refine le_ciSup bddAbove_of_small (⟨_, ho.succ_lt ?_⟩ : Set.Iio o)

Goal state after:
case limit.refine_2
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
h : ⨆ i, (V_ ↑i).card < o.card
⊢ (⨆ i, (V_ ↑i).card).ord < o
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝ : e.NF
this : a.NF
⊢ 1 + (e - 1) = e

Tactic:
refine repr_inj.1 ?_

Goal state after:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝ : e.NF
this : a.NF
⊢ (1 + (e - 1)).repr = e.repr
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
s : Stream' (Option α)
hs : ClusterPt s (Filter.principal {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none})
n : ℕ
hn : s n = none
⊢ s (n + 1) = none

Tactic:
rw [clusterPt_principal_iff] at hs

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
s : Stream' (Option α)
hs : ∀ U ∈ nhds s, (U ∩ {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none}).Nonempty
n : ℕ
hn : s n = none
⊢ s (n + 1) = none
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case nil.nil
α : Type u_1
h : dist nil nil ≤ 2⁻¹
⊢ nil = nil ∧ nil = nil ∨ ∃ hd s' t', nil = Seq.cons hd s' ∧ nil = Seq.cons hd t'

Tactic:
norm_num at h

Goal state after:
case nil.nil
α : Type u_1
h : True
⊢ nil = nil ∧ nil = nil ∨ ∃ hd s' t', nil = Seq.cons hd s' ∧ nil = Seq.cons hd t'
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case nil.cons
α : Type u_1
x✝ : α
s✝ : Stream'.Seq α
h : dist nil (Seq.cons x✝ s✝) ≤ 2⁻¹
⊢ nil = nil ∧ Seq.cons x✝ s✝ = nil ∨ ∃ hd s' t', nil = Seq.cons hd s' ∧ Seq.cons x✝ s✝ = Seq.cons hd t'

Tactic:
norm_num at h

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

Goal state before:
pp: case cons.nil
α : Type u_1
x✝ : α
s✝ : Stream'.Seq α
h : dist (Seq.cons x✝ s✝) nil ≤ 2⁻¹
⊢ Seq.cons x✝ s✝ = nil ∧ nil = nil ∨ ∃ hd s' t', Seq.cons x✝ s✝ = Seq.cons hd s' ∧ nil = Seq.cons hd t'

Tactic:
norm_num at h

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

Goal state before:
pp: case cons.cons
α : Type u_1
x✝¹ : α
s✝¹ : Stream'.Seq α
x✝ : α
s✝ : Stream'.Seq α
h : dist (Seq.cons x✝¹ s✝¹) (Seq.cons x✝ s✝) ≤ 2⁻¹
⊢ Seq.cons x✝¹ s✝¹ = nil ∧ Seq.cons x✝ s✝ = nil ∨
    ∃ hd s' t', Seq.cons x✝¹ s✝¹ = Seq.cons hd s' ∧ Seq.cons x✝ s✝ = Seq.cons hd t'

Tactic:
norm_num at h

Goal state after:
case cons.cons
α : Type u_1
x✝¹ : α
s✝¹ : Stream'.Seq α
x✝ : α
s✝ : Stream'.Seq α
h : dist (Seq.cons x✝¹ s✝¹) (Seq.cons x✝ s✝) ≤ 1 / 2
⊢ Seq.cons x✝¹ s✝¹ = nil ∧ Seq.cons x✝ s✝ = nil ∨
    ∃ hd s' t', Seq.cons x✝¹ s✝¹ = Seq.cons hd s' ∧ Seq.cons x✝ s✝ = Seq.cons hd t'
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α :=
  fun f b ↦
    match F b with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))
f g : β →ᵤ Stream'.Seq α
b : β
a : α
c : γ
b' : β
⊢ ∃ C, ∀ (a b : Stream'.Seq α), dist a b ≤ C

Tactic:
← Metric.boundedSpace_iff

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α :=
  fun f b ↦
    match F b with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))
f g : β →ᵤ Stream'.Seq α
b : β
a : α
c : γ
b' : β
⊢ BoundedSpace (Stream'.Seq α)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic

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

Tactic:
exact const_sorted.cons_nil

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

Goal state before:
pp: case h.h.h
γ : Type u_1
basis_hd : ℝ → ℝ
basis_tl : Basis
op : γ → Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
inst✝ : FriendlyOperationClass op
x✝ y✝ : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl → Prop
base : motive x✝ y✝
step :
  ∀ (x y : Multiseries basis_hd basis_tl),
    motive x y → x = y ∨ ∃ exp coef c x' y', x = cons exp coef (op c x') ∧ y = cons exp coef (op c y') ∧ motive x' y'
x y : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
ih : motive x y
h : x = y ∨ ∃ exp coef c x' y', x = cons exp coef (op c x') ∧ y = cons exp coef (op c y') ∧ motive x' y'
⊢ x = y ∨ ∃ hd u' v' c, x = Seq.cons hd (op c u') ∧ y = Seq.cons hd (op c v') ∧ motive u' v'

Tactic:
obtain h | ⟨exp, coef, c, x', y', rfl, rfl, h_next⟩ := h

Goal state after:
case h.h.h.inl
γ : Type u_1
basis_hd : ℝ → ℝ
basis_tl : Basis
op : γ → Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
inst✝ : FriendlyOperationClass op
x✝ y✝ : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl → Prop
base : motive x✝ y✝
step :
  ∀ (x y : Multiseries basis_hd basis_tl),
    motive x y → x = y ∨ ∃ exp coef c x' y', x = cons exp coef (op c x') ∧ y = cons exp coef (op c y') ∧ motive x' y'
x y : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
ih : motive x y
h : x = y
⊢ x = y ∨ ∃ hd u' v' c, x = Seq.cons hd (op c u') ∧ y = Seq.cons hd (op c v') ∧ motive u' v'

case h.h.h.inr
γ : Type u_1
basis_hd : ℝ → ℝ
basis_tl : Basis
op : γ → Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
inst✝ : FriendlyOperationClass op
x y : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl → Prop
base : motive x y
step :
  ∀ (x y : Multiseries basis_hd basis_tl),
    motive x y → x = y ∨ ∃ exp coef c x' y', x = cons exp coef (op c x') ∧ y = cons exp coef (op c y') ∧ motive x' y'
exp : ℝ
coef : MultiseriesExpansion basis_tl
c : γ
x' y' : Multiseries basis_hd basis_tl
h_next : motive x' y'
ih : motive (cons exp coef (op c x')) (cons exp coef (op c y'))
⊢ cons exp coef (op c x') = cons exp coef (op c y') ∨
    ∃ hd u' v' c_1,
      cons exp coef (op c x') = Seq.cons hd (op c_1 u') ∧
        cons exp coef (op c y') = Seq.cons hd (op c_1 v') ∧ motive u' v'
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: 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)
⊢ motive ms

Tactic:
by
  let ⟨s, f⟩ := ms
  cases s with
  | nil => apply nil
  | cons hd tl => apply cons

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:
apply coinduct fun {basis} ms =>
    ms.Approximates ∨ ∃ (h_basis : basis = basis_hd :: basis_tl), (motive (h_basis ▸ ms))

Goal state after:
case hyp
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))
⊢ ∀ {basis : Basis} (ms : MultiseriesExpansion basis),
    (ms.Approximates ∨ ∃ (h_basis : basis = basis_hd :: basis_tl), motive (h_basis ▸ ms)) →
      basis = [] ∨
        (∃ basis_hd basis_tl f, f =ᶠ[atTop] 0 ∧ basis = basis_hd :: basis_tl ∧ ms ≍ mk Multiseries.nil f) ∨
          ∃ basis_hd_1 f basis_tl_1 exp coef tl,
            (coef.Approximates ∨ ∃ (h_basis : basis_tl_1 = basis_hd :: basis_tl), motive (h_basis ▸ coef)) ∧
              Majorized f basis_hd_1 exp ∧
                ((mk tl (f - basis_hd_1 ^ exp * coef.toFun)).Approximates ∨
                    ∃ (h_basis : basis_hd_1 :: basis_tl_1 = basis_hd :: basis_tl),
                      motive (h_basis ▸ mk tl (f - basis_hd_1 ^ exp * coef.toFun))) ∧
                  basis = basis_hd_1 :: basis_tl_1 ∧ ms ≍ mk (Multiseries.cons exp coef tl) f

case x
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 ∨ ∃ (h_basis : basis_hd :: basis_tl = basis_hd :: basis_tl), motive (h_basis ▸ ms)