mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: case h.right
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
⊢ (rTensor M B.val.toLinearMap) ((rTensor M (Subalgebra.inclusion hAB).toLinearMap) u) = t

Tactic:
· rw [← comp_apply, ← rTensor_comp, ← hu]
    congr

Goal state after:
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁸ : CommSemiring R
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_5
inst✝³ : AddCommMonoid P
inst✝² : Module R P
f : M →ₚₗ[R] N
g : N →ₚₗ[R] P
S : Type u_7
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S ⟨s, p⟩ = t
hb : π R N S ⟨s, f.toFun' (MvPolynomial (Fin s.card) R) p⟩ = toFun S f t
⊢ toFun S (g.comp f) t = (toFun S g ∘ toFun S f) t

Tactic:
rw [Function.comp_apply, toFun_eq_rTensor_φ_toFun' _ hb, toFun_eq_rTensor_φ_toFun' _ ha,
    comp_toFun', Function.comp_apply]

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

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
f : A⟦X⟧
inst✝ : IsPrecomplete (IsLocalRing.maximalIdeal A) A
⊢ f %ʷ 0 = 0

Tactic:
weierstrassMod,

Goal state after:
A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
f : A⟦X⟧
inst✝ : IsPrecomplete (IsLocalRing.maximalIdeal A) A
⊢ (if hg : (map (IsLocalRing.residue A)) 0 ≠ 0 then IsWeierstrassDivisorAt.mod ⋯ f else 0) = 0
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
f g : A⟦X⟧
hg : (map (IsLocalRing.residue A)) g ≠ 0
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
⊢ f.IsWeierstrassDivision g (if hg : (map (IsLocalRing.residue A)) g ≠ 0 then IsWeierstrassDivisorAt.div ⋯ f else 0)
    (f %ʷ g)

Tactic:
weierstrassMod,

Goal state after:
A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
f g : A⟦X⟧
hg : (map (IsLocalRing.residue A)) g ≠ 0
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
⊢ f.IsWeierstrassDivision g (if hg : (map (IsLocalRing.residue A)) g ≠ 0 then IsWeierstrassDivisorAt.div ⋯ f else 0)
    (if hg : (map (IsLocalRing.residue A)) g ≠ 0 then IsWeierstrassDivisorAt.mod ⋯ f else 0)
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
f g : A⟦X⟧
hg : (map (IsLocalRing.residue A)) g ≠ 0
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
⊢ f = (g * if hg : (map (IsLocalRing.residue A)) g ≠ 0 then IsWeierstrassDivisorAt.div ⋯ f else 0) + ↑(f %ʷ g)

Tactic:
weierstrassMod,

Goal state after:
A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
f g : A⟦X⟧
hg : (map (IsLocalRing.residue A)) g ≠ 0
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
⊢ f =
    (g * if hg : (map (IsLocalRing.residue A)) g ≠ 0 then IsWeierstrassDivisorAt.div ⋯ f else 0) +
      ↑(if hg : (map (IsLocalRing.residue A)) g ≠ 0 then IsWeierstrassDivisorAt.mod ⋯ f else 0)
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
g' : A⟦X⟧
f' : A[X]
h' : A⟦X⟧
H' : g'.IsWeierstrassFactorizationAt f' h' I
⊢ g * g' = ↑(f * f') * (h * h')

Tactic:
rw [H.eq_mul, H'.eq_mul, Polynomial.coe_mul]; ring

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.Congr

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
⊢ IsSimpleRing R ↔ Nontrivial R ∧ ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤

Tactic:
let e := orderIsoIsTwoSided (R := R)
  simp_rw [isSimpleRing_iff, isSimpleOrder_iff, orderIsoRingCon.toEquiv.nontrivial_congr,
    RingCon.nontrivial_iff, e.forall_congr_left, Subtype.forall, ← e.injective.eq_iff]
  simp [e, Subtype.ext_iff]

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: case refine_1
R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
m : Submodule R M
h : m.IsFullyInvariant
c : { x // x ∈ isotypicComponents R M }
left✝ : c ∈ OrderIso.setIsotypicComponents.symm ⟨m, h⟩
⊢ ↑c ∈ isotypicComponents R M

Tactic:
exact c.2

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Maximal.Topology

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x : MaximalSpectrum R
⊢ toPrimeSpectrum ⁻¹' {x.toPrimeSpectrum} = {x}

Tactic:
simpa only [← image_singleton] using preimage_image_eq {x} toPrimeSpectrum_injective

Goal state after:
Module: Mathlib.RingTheory.Valuation.Minpoly

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
Γ₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
x : L
hx : IsUnit x
⊢ v ((minpoly K x).coeff 0) ^ (finrank K L / (minpoly K x).natDegree) ≠ 0

Tactic:
have h_alg : Algebra.IsAlgebraic K L := Algebra.IsAlgebraic.of_finite K L

Goal state after:
K : Type u_1
inst✝⁴ : Field K
Γ₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
x : L
hx : IsUnit x
h_alg : Algebra.IsAlgebraic K L
⊢ v ((minpoly K x).coeff 0) ^ (finrank K L / (minpoly K x).natDegree) ≠ 0
Module: Mathlib.RingTheory.WittVector.Compare

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k₁ k₂ : ℕ
hk : k₁ ≤ k₂
⊢ ((TruncatedWittVector.truncate hk).comp (zmodEquivTrunc p k₂).toRingHom).comp (PadicInt.toZModPow k₂) =
    (zmodEquivTrunc p k₁).toRingHom.comp (PadicInt.toZModPow k₁)

Tactic:
commutes,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k₁ k₂ : ℕ
hk : k₁ ≤ k₂
⊢ ((zmodEquivTrunc p k₁).toRingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k₁)))).comp (PadicInt.toZModPow k₂) =
    (zmodEquivTrunc p k₁).toRingHom.comp (PadicInt.toZModPow k₁)
Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing

Goal state before:
pp: case a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hA : A.coeff 0 = ↑a
n : ℕ
a✝ : (A * { coeff := inverseCoeff a A }).coeff n = coeff 1 n
H_coeff : k :=
  A.coeff (n + 1) * ↑(a⁻¹ ^ p ^ (n + 1)) + nthRemainder p n (truncateFun (n + 1) A) fun i ↦ inverseCoeff a A ↑i
H : ↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹ = 1
ha : ↑a ^ p ^ (n + 1) = ↑(a ^ p ^ (n + 1))
ha_inv : ↑a⁻¹ ^ p ^ (n + 1) = ↑(a ^ p ^ (n + 1))⁻¹
⊢ A.coeff (n + 1) * ↑(a ^ p ^ (n + 1))⁻¹ +
            -↑(a ^ p ^ (n + 1))⁻¹ *
                (A.coeff (n + 1) * ↑(a ^ p ^ (n + 1))⁻¹ +
                  nthRemainder p n (truncateFun (n + 1) A) fun i ↦ inverseCoeff a A ↑i) *
              ↑(a ^ p ^ (n + 1)) +
          nthRemainder p n (truncateFun (n + 1) A) (truncateFun (n + 1) { coeff := inverseCoeff a A }) +
        -H_coeff * 1 -
      (0 + -H_coeff * (↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹)) =
    0

Tactic:
ring!

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

Goal state before:
pp: o₁ o₂ : Ordinal.{u_1}
⊢ AddCommute o₁ o₂ ↔ ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂

Tactic:
refine ⟨fun hcomm ↦ ?_, ?_⟩
  · induction h : o₁ + o₂ using WellFoundedLT.induction generalizing o₁ o₂ with | ind o ih
    subst h
    wlog hle : o₁ ≤ o₂
    · grind [hcomm.symm]
    rcases eq_or_ne o₁ 0 with (rfl | h₁)
    · exact ⟨o₂, 0, 1, by simp, by simp⟩
    let o₃ := o₂ - o₁
    have hsub : o₁ + o₃ = o₂ := Ordinal.add_sub_cancel_of_le hle
    have hcomm' : AddCommute o₁ o₃ := add_left_cancel (a := o₁) <| by grind
    have hlt : o₁ + o₃ < o₁ + o₂ := by simpa [hsub, hcomm.eq] using h₁.pos
    rcases ih _ hlt hcomm' rfl with ⟨o, n₁, n₃, hn₁, hn₃⟩
    use o, n₁, n₁ + n₃, hn₁
    rw [Nat.cast_add, mul_add, hn₁, hn₃, hsub]
  · rintro ⟨o, n₁, n₂, rfl, rfl⟩
    rw [addCommute_iff_eq, ← mul_add, ← mul_add, ← Nat.cast_add, add_comm, Nat.cast_add]

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

Goal state before:
pp: case h
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b
h_nab : a ≠ b
⊢ ↑a ≠ ↑b ∧ lfpApprox f x ↑a = lfpApprox f x ↑b

Tactic:
apply And.intro

Goal state after:
case h.left
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b
h_nab : a ≠ b
⊢ ↑a ≠ ↑b

case h.right
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b
h_nab : a ≠ b
⊢ lfpApprox f x ↑a = lfpApprox f x ↑b
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case inr.inr
b : Ordinal.{u_1}
hb : b ≤ 1
o a : Ordinal.{u_1}
ho : o ≠ 0
ha : a ≠ 0
⊢ (coeff b o) a = (single 0 o) a

Tactic:
single_eq_of_ne ha

Goal state after:
case inr.inr
b : Ordinal.{u_1}
hb : b ≤ 1
o a : Ordinal.{u_1}
ho : o ≠ 0
ha : a ≠ 0
⊢ (coeff b o) a = 0
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h_fix : ∃ y, lfpApprox f ⊥ (succ #α).ord = ↑y
x : ↑(fixedPoints ⇑f)
h_x : lfpApprox f ⊥ (succ #α).ord = ↑x
⊢ lfp f ≤ lfpApprox f ⊥ (succ #α).ord

Tactic:
rw [h_x]

Goal state after:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h_fix : ∃ y, lfpApprox f ⊥ (succ #α).ord = ↑y
x : ↑(fixedPoints ⇑f)
h_x : lfpApprox f ⊥ (succ #α).ord = ↑x
⊢ lfp f ≤ ↑x
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd'
e : ONote
n : ℕ+
a : ONote
b eb✝ : Ordinal.{0}
h₁ : e.NFBelow eb✝
h₂ : a.NFBelow e.repr
h₃ : e.repr < b
⊢ e.NF

Tactic:
exact ⟨⟨_, h₁⟩⟩

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

Goal state before:
pp: case single_add
b e' x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hx : x ≠ 0
IH : ∀ {e : Ordinal.{u_1}}, (∀ (e' : Ordinal.{u_1}), f e' < b) → (∀ e' ∈ f.support, e' < e) → eval b f < b ^ e
e : Ordinal.{u_1}
hb : ∀ (e'_1 : Ordinal.{u_1}), (single e' x + f) e'_1 < b
he : ∀ e'_1 ∈ (single e' x + f).support, e'_1 < e
he' : e' ∉ f.support
⊢ e' < e

Tactic:
apply he e' _
      simp [hx]

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

Goal state before:
pp: x x' y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z ∈ x.pair y ↔ z ∈ x'.pair y'
⊢ x = x' ∧ y = y'

Tactic:
pair,

Goal state after:
x x' y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z ∈ {{x}, {x, y}} ↔ z ∈ {{x'}, {x', y'}}
⊢ x = x' ∧ y = y'
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case a.h₁
x y : PSet.{u_1}
⊢ succ x.rank ≤ (insert x y).rank

Tactic:
exact (rank_lt_of_mem (mem_insert x y)).succ_le

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

Goal state before:
pp: case a
x y✝ : PSet.{u_1}
⊢ y✝ ⊆ x → y✝.rank ≤ x.rank

Tactic:
exact rank_mono

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ε_ 0 < Γ_ 0

Tactic:
simpa using iterate_veblen_lt_gamma_zero 2

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (veblen (Γ_ o) 0).invVeblen₂ = 0

Tactic:
invVeblen₂_veblen gamma_ne_zero veblen_pos

Goal state after:
o : Ordinal.{u_1}
⊢ 0 = 0
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ (⋃ (i : α), f i).rank = ⨆ i, (f i).rank

Tactic:
apply le_antisymm
  · simp_rw [rank_le_iff, mem_iUnion]
    intro y ⟨i, hy⟩
    exact (rank_lt_of_mem hy).trans_le (Ordinal.le_iSup _ _)
  · exact Ordinal.iSup_le fun i => rank_mono (subset_iUnion f i)

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

Goal state before:
pp: case pos
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : e = 0
p : 0 = o' ∧ ↑n = m
⊢ 0 = scale 1 o' ∧ ↑n = m

Tactic:
rcases p with ⟨rfl, rfl⟩

Goal state after:
case pos
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : e = 0
⊢ 0 = scale 1 0 ∧ ↑n = ↑n
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case pos
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : e = 0
p : 0 = o' ∧ ↑n = m
⊢ o'.NF ∧ ↑↑n + a.repr = ω * o'.repr + ↑m

Tactic:
rcases p with ⟨rfl, rfl⟩

Goal state after:
case pos
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : e = 0
⊢ NF 0 ∧ ↑↑n + a.repr = ω * repr 0 + ↑↑n
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o o' : ONote
m : ℕ
inst✝ : o.NF
h : o.split = (o', m)
a : ONote
n : ℕ
e : o.split' = (a, n)
s₁ : a.NF
s₂ : o.repr = ω * a.repr + ↑n
⊢ o'.NF ∧ o.repr = o'.repr + ↑m

Tactic:
rw [split_eq_scale_split' e] at h

Goal state after:
o o' : ONote
m : ℕ
inst✝ : o.NF
a : ONote
n : ℕ
h : (scale 1 a, n) = (o', m)
e : o.split' = (a, n)
s₁ : a.NF
s₂ : o.repr = ω * a.repr + ↑n
⊢ o'.NF ∧ o.repr = o'.repr + ↑m
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o o' : ONote
m : ℕ
inst✝ : o.NF
h : o.split = (o', m)
a : ONote
n : ℕ
e : o.split' = (a, n)
⊢ ω ∣ o'.repr

Tactic:
rw [split_eq_scale_split' e] at h

Goal state after:
o o' : ONote
m : ℕ
inst✝ : o.NF
a : ONote
n : ℕ
h : (scale 1 a, n) = (o', m)
e : o.split' = (a, n)
⊢ ω ∣ o'.repr
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized

Goal state before:
pp: f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
⊢ (f ^ exp) =o[atTop] (f ^ exp')

Tactic:
apply (isLittleO_iff_tendsto' _).mpr

Goal state after:
f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
⊢ Tendsto (fun x ↦ (f ^ exp) x / (f ^ exp') x) atTop (𝓝 0)

f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
⊢ ∀ᶠ (x : ℝ) in atTop, (f ^ exp') x = 0 → (f ^ exp) x = 0
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis

Goal state before:
pp: left right : Basis
f : ℝ → ℝ
h : WellFormedBasis (left ++ right)
hf_tendsto : Tendsto f atTop atTop
hf_comp_left : ∀ (g : ℝ → ℝ), List.getLast? left = some g → (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
hf_comp_right : ∀ (g : ℝ → ℝ), List.head? right = some g → (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
⊢ WellFormedBasis (left ++ f :: right)

Tactic:
have : WellFormedBasis (f :: right) := cons (h.of_sublist (by simp)) hf_tendsto
    (compare_right_aux (h.of_sublist (by simp)) hf_comp_right)
  apply compare_left_aux (h.of_sublist (by simp)) at hf_comp_left
  apply append (h.of_sublist (by simp)) this
  exact fun g hg ↦ compare_right_aux this (by grind)

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

Goal state before:
pp: case zero
basis_hd : ℝ → ℝ
basis_tl : Basis
r : ℝ
⊢ (Multiseries.cons r one Multiseries.nil).Sorted

Tactic:
exact Sorted.cons_nil const_sorted

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

Goal state before:
pp: basis : Basis
n : ℕ
h : n < List.length basis
n' : Fin (List.length basis) := ⟨n, h⟩
⊢ n = ↑n'

Tactic:
simp [n']

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

Goal state before:
pp: case inr
α : Sort u_1
hα : Nonempty α
o : Ordinal.{u_2}
f : α → Ordinal.{u_2}
H✝ : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ i, a < f i
b a : Ordinal.{u_2}
h : a - b < o
h' : b ≤ a
i : α
H : a - b < f i
⊢ a < b + f i

Tactic:
rwa [← Ordinal.add_sub_cancel_of_le h', add_lt_add_iff_left]

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

Goal state before:
pp: case h
α : 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 :
  (op s).destruct =
    Option.map
      (fun x ↦
        match x with
        | (hd, opf, op') => (hd, ↑opf (↑op' s.tail)))
      (T s.head)
⊢ ((opf ∘ op) s).destruct =
    Option.map
      (fun x ↦
        match x with
        | (hd, op') => (hd, ↑op' s.tail))
      ((fun hd? ↦
          match T hd? with
          | none =>
            Option.map
              (fun x ↦
                match x with
                | (hd, opf') => (hd, ⟨(fun x ↦ ↑opf' nil) ∘ op, ⋯⟩))
              (h_opf.unfold none)
          | some (hd, opf', op') =>
            Option.map
              (fun x ↦
                match x with
                | (hd', opf'') => (hd', ⟨(↑opf'' ∘ ↑opf') ∘ ↑op', ⋯⟩))
              (h_opf.unfold (some hd)))
        s.head)

Tactic:
simp only [Function.comp_apply]

Goal state after:
case h
α : 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 :
  (op s).destruct =
    Option.map
      (fun x ↦
        match x with
        | (hd, opf, op') => (hd, ↑opf (↑op' s.tail)))
      (T s.head)
⊢ (opf (op s)).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)))
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: exps_hd : ℝ
exps_tl : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_nonzero : 0 < exps_hd
h_equiv : log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) ~[atTop] exps_hd • log ∘ basis_hd
h_log : Tendsto (log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop atTop
x : ℝ
hx : 0 < toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) x
⊢ (rexp ∘ log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) x =
    toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) x

Tactic:
simp only [Function.comp_apply]

Goal state after:
exps_hd : ℝ
exps_tl : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_nonzero : 0 < exps_hd
h_equiv : log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) ~[atTop] exps_hd • log ∘ basis_hd
h_log : Tendsto (log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop atTop
x : ℝ
hx : 0 < toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) x
⊢ rexp (log (toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) x)) = toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) x
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: exps_hd : ℝ
exps_tl : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_nonzero : exps_hd < 0
h_equiv : log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) ~[atTop] exps_hd • log ∘ basis_hd
h_log : Tendsto (log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop atBot
hmono : Tendsto (rexp ∘ log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop (𝓝 0)
x : ℝ
hx : 0 < toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) x
⊢ (rexp ∘ log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) x =
    toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) x

Tactic:
simp only [Function.comp_apply]

Goal state after:
exps_hd : ℝ
exps_tl : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_nonzero : exps_hd < 0
h_equiv : log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) ~[atTop] exps_hd • log ∘ basis_hd
h_log : Tendsto (log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop atBot
hmono : Tendsto (rexp ∘ log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop (𝓝 0)
x : ℝ
hx : 0 < toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) x
⊢ rexp (log (toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) x)) = toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) x