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

Goal state before:
pp: case inl
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 :
  ((X ^ ((map (Ideal.Quotient.mk I)) g).order.toNat *
          mk fun i ↦ (coeff (i + ((map (Ideal.Quotient.mk I)) g).order.toNat)) g) +
        ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g)) *
      q =
    ↑r
k : ℕ
ih : ∀ (i : ℕ), (coeff i) q ∈ I ^ k
i : ℕ
hi : i < ((map (Ideal.Quotient.mk I)) g).order.toNat
j : ℕ
hj : j ≤ i
⊢ (coeff j)
      ((X ^ ((map (Ideal.Quotient.mk I)) g).order.toNat *
          mk fun i ↦ (coeff (i + ((map (Ideal.Quotient.mk I)) g).order.toNat)) g) +
        ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g)) ∈
    I

Tactic:
map_add,

Goal state after:
case inl
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 :
  ((X ^ ((map (Ideal.Quotient.mk I)) g).order.toNat *
          mk fun i ↦ (coeff (i + ((map (Ideal.Quotient.mk I)) g).order.toNat)) g) +
        ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g)) *
      q =
    ↑r
k : ℕ
ih : ∀ (i : ℕ), (coeff i) q ∈ I ^ k
i : ℕ
hi : i < ((map (Ideal.Quotient.mk I)) g).order.toNat
j : ℕ
hj : j ≤ i
⊢ (coeff j)
        (X ^ ((map (Ideal.Quotient.mk I)) g).order.toNat *
          mk fun i ↦ (coeff (i + ((map (Ideal.Quotient.mk I)) g).order.toNat)) g) +
      (coeff j) ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g) ∈
    I
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
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)

Tactic:
← mul_assoc,

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: 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)

Tactic:
← mul_assoc,

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.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
f : M →ₚₗ[R] N
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] f.ground x = toFun S f (1 ⊗ₜ[R] x)

Tactic:
simp only [ground, toFun'_eq_toFun]

Goal state after:
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
f : M →ₚₗ[R] N
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] (⇑(TensorProduct.lid R N) ∘ toFun R f ∘ ⇑(TensorProduct.lid R M).symm) x = toFun S f (1 ⊗ₜ[R] x)
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H1 : r.degree < ↑n
H2 : 1 = (coeff n) ((map (IsLocalRing.residue A)) (g * q + ↑r))
⊢ IsUnit q

Tactic:
map_add,

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H1 : r.degree < ↑n
H2 : 1 = (coeff n) ((map (IsLocalRing.residue A)) (g * q)) + (coeff n) ((map (IsLocalRing.residue A)) ↑r)
⊢ IsUnit q
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
S : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup S
inst✝¹ : Module R M
inst✝ : Module R S
N : Submodule R M
⊢ IsIsotypicOfType R (↥N) S ↔ ∀ m ≤ N, ∀ [IsSimpleModule R ↥m], Nonempty (↥m ≃ₗ[R] S)

Tactic:
rw [Subtype.forall', ← (Submodule.MapSubtype.orderIso N).forall_congr_right]

Goal state after:
R : Type u_2
M : Type u
S : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup S
inst✝¹ : Module R M
inst✝ : Module R S
N : Submodule R M
⊢ IsIsotypicOfType R (↥N) S ↔
    ∀ (a : Submodule R ↥N) [IsSimpleModule R ↥↑((Submodule.MapSubtype.orderIso N).toEquiv a)],
      Nonempty (↥↑((Submodule.MapSubtype.orderIso N).toEquiv a) ≃ₗ[R] S)
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
⊢ IsIsotypic R ↥N ↔ ∀ m ≤ N, ∀ [IsSimpleModule R ↥m], IsIsotypicOfType R ↥N ↥m

Tactic:
rw [Subtype.forall', ← (Submodule.MapSubtype.orderIso N).forall_congr_right]

Goal state after:
R : Type u_2
M : Type u
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
⊢ IsIsotypic R ↥N ↔
    ∀ (a : Submodule R ↥N) [IsSimpleModule R ↥↑((Submodule.MapSubtype.orderIso N).toEquiv a)],
      IsIsotypicOfType R ↥N ↥↑((Submodule.MapSubtype.orderIso N).toEquiv a)
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: case add
R : Type u_1
inst✝ : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
x y : R
ymem : y ∈ I * J
z : R
zmem : z ∈ I * J
hy : f (J.toCotangent ⟨y, ⋯⟩) = 0
hz : f (J.toCotangent ⟨z, ⋯⟩) = 0
this : ⟨y + z, ⋯⟩ = ⟨y, ⋯⟩ + ⟨z, ⋯⟩
⊢ f (J.toCotangent (⟨y, ⋯⟩ + ⟨z, ⋯⟩)) = 0

Tactic:
map_add,

Goal state after:
case add
R : Type u_1
inst✝ : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
x y : R
ymem : y ∈ I * J
z : R
zmem : z ∈ I * J
hy : f (J.toCotangent ⟨y, ⋯⟩) = 0
hz : f (J.toCotangent ⟨z, ⋯⟩) = 0
this : ⟨y + z, ⋯⟩ = ⟨y, ⋯⟩ + ⟨z, ⋯⟩
⊢ f (J.toCotangent ⟨y, ⋯⟩ + J.toCotangent ⟨z, ⋯⟩) = 0
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: case add
R : Type u_1
inst✝ : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
x y : R
ymem : y ∈ I * J
z : R
zmem : z ∈ I * J
hy : f (J.toCotangent ⟨y, ⋯⟩) = 0
hz : f (J.toCotangent ⟨z, ⋯⟩) = 0
this : ⟨y + z, ⋯⟩ = ⟨y, ⋯⟩ + ⟨z, ⋯⟩
⊢ f (J.toCotangent ⟨y, ⋯⟩ + J.toCotangent ⟨z, ⋯⟩) = 0

Tactic:
map_add,

Goal state after:
case add
R : Type u_1
inst✝ : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
x y : R
ymem : y ∈ I * J
z : R
zmem : z ∈ I * J
hy : f (J.toCotangent ⟨y, ⋯⟩) = 0
hz : f (J.toCotangent ⟨z, ⋯⟩) = 0
this : ⟨y + z, ⋯⟩ = ⟨y, ⋯⟩ + ⟨z, ⋯⟩
⊢ f (J.toCotangent ⟨y, ⋯⟩) + f (J.toCotangent ⟨z, ⋯⟩) = 0
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
⊢ IsDiscrete R

Tactic:
by
  refine ⟨⟨0, zero_lt_one, fun x ↦ ?_⟩⟩
  have := subsingleton_units_valueGroupWithZero_of_trivialRel R Γ
  rcases GroupWithZero.eq_zero_or_unit x with rfl | ⟨u, rfl⟩
  · simp
  · rw [← Units.val_one, Units.val_lt_val]
    simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.UnivLE

Goal state before:
pp: case h
h✝ : univ.{v, u + 1} < univ.{u, v + 1}
w✝ : Cardinal.{u}
α : Type u
h : univ.{v, u + 1} = lift.{max (u + 1) (v + 1), u} (Quot.mk (⇑isEquivalent) α)
⊢ univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α

Tactic:
rw [univ_umax.{v, u}, ← lift_le.{u + 1}, lift_univ, lift_lift]

Goal state after:
case h
h✝ : univ.{v, u + 1} < univ.{u, v + 1}
w✝ : Cardinal.{u}
α : Type u
h : univ.{v, u + 1} = lift.{max (u + 1) (v + 1), u} (Quot.mk (⇑isEquivalent) α)
⊢ univ.{v, u + 1} ≤ lift.{max (v + 1) (u + 1), u} #α
Module: Mathlib.SetTheory.Cardinal.UnivLE

Goal state before:
pp: case refine_2
h : univ.{v, u + 1} < univ.{u, v + 1}
⊢ ∃ α, univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α

Tactic:
· obtain ⟨⟨α⟩, h⟩ := lt_univ'.mp h; use α
    rw [univ_umax.{v, u}, ← lift_le.{u + 1}, lift_univ, lift_lift]
    exact h.le

Goal state after:
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: case inl
A : Type u_1
T : ↥(tree A)
x y : List A
h : y ∈ pullSub (subAt T x) x
h' : y.length ≤ x.length
⊢ y ∈ ↑T

Tactic:
rw [mem_pullSub_short h'] at h

Goal state after:
case inl
A : Type u_1
T : ↥(tree A)
x y : List A
h : y <+: x ∧ [] ∈ subAt T x
h' : y.length ≤ x.length
⊢ y ∈ ↑T
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
b : Bool
h : true = b
l : Lists' α b
⊢ let l' := ⋯ ▸ l;
  ofList l'.toList = l'

Tactic:
induction l with
    | atom => cases h
    | nil => simp
    | cons' b a _ IH => simpa [cons] using IH rfl

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

Goal state before:
pp: case refine_2
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b o))

Tactic:
rcases le_or_gt b 1 with hb | hb
    · rw [CNF.of_le_one hb ho]
      exact pairwise_singleton _ _
    · obtain hob | hbo := lt_or_ge o b
      · rw [CNF.of_lt ho hob]
        exact pairwise_singleton _ _
      · rw [CNF.ne_zero ho, map_cons, pairwise_cons]
        refine ⟨fun a H ↦ ?_, IH⟩
        rw [mem_map] at H
        rcases H with ⟨⟨a, a'⟩, H, rfl⟩
        exact (fst_le_log H).trans_lt (log_mod_opow_log_lt_log_self hb hbo)

Goal state after:
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a✝ : Nontrivial α
ha✝ : ¬IsSuccLimit a
ha : IsMin a
⊢ {a} = Iio (Order.succ a)

Tactic:
simp [ha.Iic_eq]

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

Goal state before:
pp: case refine_2.refine_1
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsClosed s
a : Ordinal.{u}
ha : IsSuccLimit a
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
this✝ : sSup (enumOrd s '' Set.Iio a) ∈ closure (enumOrd s '' Set.Iio a)
this : sSup (enumOrd s '' Set.Iio a) ∈ s
⊢ sSup (enumOrd s '' Set.Iio a) ≤ o

Tactic:
apply csSup_le'

Goal state after:
case refine_2.refine_1
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsClosed s
a : Ordinal.{u}
ha : IsSuccLimit a
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
this✝ : sSup (enumOrd s '' Set.Iio a) ∈ closure (enumOrd s '' Set.Iio a)
this : sSup (enumOrd s '' Set.Iio a) ∈ s
⊢ o ∈ upperBounds (enumOrd s '' Set.Iio a)
Module: Mathlib.SetTheory.ZFC.PSet

Goal state before:
pp: ⊢ ¬∅.Nonempty

Tactic:
by simp [PSet.Nonempty]

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

Goal state before:
pp: x : ZFSet.{u}
⊢ x.powerset.card = 2 ^ x.card

Tactic:
rw [← lift_inj.{u, u + 1}]
  simpa [← cardinalMk_coe_sort] using mk_congr (powersetEquiv x)

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

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

Tactic:
by
  simpa [cardinalMk_coe_sort, ← coe_iUnion, ← lift_iSup bddAbove_of_small, -mem_iUnion] using
    iSup_mk_le_mk_iUnion (f := SetLike.coe ∘ f)

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

Goal state before:
pp: ⊢ ε_ 0 = nfp (fun a ↦ ω ^ a) 0

Tactic:
epsilon_eq_deriv,

Goal state after:
⊢ deriv (fun a ↦ ω ^ a) 0 = nfp (fun a ↦ ω ^ a) 0
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ε_ (succ o) = nfp (fun a ↦ ω ^ a) (succ (ε_ o))

Tactic:
epsilon_eq_deriv,

Goal state after:
o : Ordinal.{u_1}
⊢ deriv (fun a ↦ ω ^ a) (succ o) = nfp (fun a ↦ ω ^ a) (succ (ε_ o))
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: o : Ordinal.{u_1}
⊢ deriv (fun a ↦ ω ^ a) (succ o) = nfp (fun a ↦ ω ^ a) (succ (ε_ o))

Tactic:
epsilon_eq_deriv,

Goal state after:
o : Ordinal.{u_1}
⊢ deriv (fun a ↦ ω ^ a) (succ o) = nfp (fun a ↦ ω ^ a) (succ (deriv (fun a ↦ ω ^ a) o))
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ω ^ ε_ o = ε_ o

Tactic:
epsilon_eq_deriv,

Goal state after:
o : Ordinal.{u_1}
⊢ ω ^ deriv (fun a ↦ ω ^ a) o = deriv (fun a ↦ ω ^ a) o
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
⊢ (e₁.oadd n₁ a₁ - e₂.oadd n₂ a₂).repr = (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr

Tactic:
by
    have := h₁.snd; have := h₂.snd; have h' := repr_sub a₁ a₂
    conv_lhs at h' => dsimp [HSub.hSub, Sub.sub, sub]
    conv_lhs => dsimp only [HSub.hSub, Sub.sub]; dsimp only [sub]
    have ee := @cmp_compares _ _ h₁.fst h₂.fst
    cases h : cmp e₁ e₂ <;> simp only [h] at ee
    · rw [Ordinal.sub_eq_zero_iff_le.2]
      · rfl
      exact le_of_lt (oadd_lt_oadd_1 h₁ ee)
    · change e₁ = e₂ at ee
      subst e₂
      dsimp only
      cases mn : (n₁ : ℕ) - n₂ <;> dsimp only
      · by_cases en : n₁ = n₂
        · simpa [en]
        · simp only [en, ite_false]
          exact
            (Ordinal.sub_eq_zero_iff_le.2 <|
                le_of_lt <|
                  oadd_lt_oadd_2 h₁ <|
                    lt_of_le_of_ne (tsub_eq_zero_iff_le.1 mn) (mt PNat.eq en)).symm
      · simp only [Nat.succPNat, Nat.succ_eq_add_one, repr, PNat.mk_coe, ← succ_eq_add_one]
        rw [(tsub_eq_iff_eq_add_of_le <| le_of_lt <| Nat.lt_of_sub_eq_succ mn).1 mn, add_comm,
          Nat.cast_add, mul_add, add_assoc, add_sub_add_cancel]
        refine
          (Ordinal.sub_eq_of_add_eq <|
              add_of_omega0_opow_le h₂.snd'.repr_lt <| le_trans ?_ le_self_add).symm
        exact Ordinal.le_mul_left _ (Nat.cast_lt.2 <| Nat.succ_pos _)
    · exact
        (Ordinal.sub_eq_of_add_eq <|
            add_of_omega0_opow_le (h₂.below_of_lt ee).repr_lt <| omega0_le_oadd _ _ _).symm

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

Goal state before:
pp: a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h : a'.repr + ↑m < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑m) + R
α0 : 0 < α'
ω00 : 0 < ω0 ^ ↑k
Rl : R < ω ^ (a0.repr * succ ↑k)
⊢ ω0 ^ (↑k + 1) * α' + (ω0 ^ ↑k * (α' * ↑m) + R) = ω0 ^ succ ↑k * α' + (ω0 ^ ↑k * α' * ↑m + R)

Tactic:
← mul_assoc,

Goal state after:
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h : a'.repr + ↑m < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑m) + R
α0 : 0 < α'
ω00 : 0 < ω0 ^ ↑k
Rl : R < ω ^ (a0.repr * succ ↑k)
⊢ ω0 ^ (↑k + 1) * α' + (ω0 ^ ↑k * α' * ↑m + R) = ω0 ^ succ ↑k * α' + (ω0 ^ ↑k * α' * ↑m + R)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case succ.refine_2.e_a
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h : a'.repr + ↑m < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑m) + R
α0✝ : 0 < α'
ω00 : 0 < ω0 ^ ↑k
Rl : R < ω ^ (a0.repr * succ ↑k)
αd : ω ∣ α'
α0 : ¬IsMin α'
⊢ ω0 ^ succ ↑k * α' = (ω0 ^ ↑k * (ω0 * ↑↑n) + (ω0 ^ ↑k * a'.repr + R)) * α'

Tactic:
← mul_assoc,

Goal state after:
case succ.refine_2.e_a
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h : a'.repr + ↑m < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑m) + R
α0✝ : 0 < α'
ω00 : 0 < ω0 ^ ↑k
Rl : R < ω ^ (a0.repr * succ ↑k)
αd : ω ∣ α'
α0 : ¬IsMin α'
⊢ ω0 ^ succ ↑k * α' = (ω0 ^ ↑k * ω0 * ↑↑n + (ω0 ^ ↑k * a'.repr + R)) * α'
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
s t : Stream'.Seq α
h : s.head ≠ t.head
⊢ dist s t = 1

Tactic:
rw [Subtype.dist_eq, PiNat.dist_eq_of_ne]

Goal state after:
α : Type u_1
s t : Stream'.Seq α
h : s.head ≠ t.head
⊢ (1 / 2) ^ PiNat.firstDiff ↑s ↑t = 1

α : Type u_1
s t : Stream'.Seq α
h : s.head ≠ t.head
⊢ ↑s ≠ ↑t
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
γ : Type u_3
γ' : Type u_4
F : γ → Stream'.Seq α → Stream'.Seq α
g : γ' → γ
h : FriendlyOperationClass F
⊢ FriendlyOperationClass fun c ↦ F (g c)

Tactic:
by
  grind [FriendlyOperationClass]

Goal state after:
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 : β
⊢ dist (UniformFun.toFun (T f) b) (UniformFun.toFun (T g) b) ≤ ↑2⁻¹ * dist f g

Tactic:
simp only [UniformFun.toFun, UniformFun.ofFun, Equiv.coe_fn_symm_mk, NNReal.coe_inv,
      NNReal.coe_ofNat, T]

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 : β
⊢ dist
      (match F b with
      | none => nil
      | some (a, c, b') => Seq.cons a (op c (f b')))
      (match F b with
      | none => nil
      | some (a, c, b') => Seq.cons a (op c (g b'))) ≤
    2⁻¹ * dist f g
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: m : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
h_length : List.length m = List.length basis_tl
h_basis : WellFormedBasis (basis_hd :: basis_tl)
⊢ Majorized (m.toFun basis_tl) basis_hd 0

Tactic:
by
  induction m generalizing basis_hd basis_tl with
  | nil =>
    simp only [toFun_nil]
    exact Majorized.const (h_basis.tendsto_atTop (by simp))
  | cons hd tl ih =>
    cases basis_tl with
    | nil => simp at h_length
    | cons basis_tl_hd basis_tl_tl =>
      simp only [List.length_cons, Nat.add_right_cancel_iff, toFun_cons] at h_length ⊢
      rw [← add_zero 0]
      apply Majorized.mul (h_basis.tail_pow_majorized_head (by simp) _) _
        h_basis.head_eventually_pos
      exact fun exp h_exp ↦
        (ih h_length h_basis.tail 1 (by simp)).trans <|
        h_basis.tail_pow_majorized_head (by simp) 1 exp h_exp

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
⊢ (cons exp coef tl).tail = tl

Tactic:
by
  simp [tail, cons]

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
s : Multiseries basis_hd basis_tl
f : ℝ → ℝ
| ms

Tactic:
eq_mk ms

Goal state after:
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
s : Multiseries basis_hd basis_tl
f : ℝ → ℝ
| mk ms.seq ms.toFun
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: left right : Basis
t1 t2 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
h2 : List.length t2.unit = List.length right
h_coef2 : t2.coef ≠ 0
h_lt : t1.unit < List.replicate (List.length left) 0 ++ t2.unit
⊢ t1.toFun (left ++ right) =o[atTop] t2.toFun right

Tactic:
obtain ⟨coef2, exps2⟩ := t2
  let t2' : Monomial := ⟨coef2, List.replicate left.length 0 ++ exps2⟩
  have : t2'.toFun (left ++ right) = Monomial.toFun ⟨coef2, exps2⟩ right :=
    Monomial.zeros_append_toFun _
  rw [← this]
  apply isLittleO_of_lt_exps h_basis <;> simpa [t2']

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

Goal state before:
pp: left right : Basis
t1 t2 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
h2 : List.length t2.unit = List.length right
h_coef1 : t1.coef ≠ 0
h_lt : List.replicate (List.length left) 0 ++ t2.unit < t1.unit
⊢ t2.toFun right =o[atTop] t1.toFun (left ++ right)

Tactic:
obtain ⟨coef2, exps2⟩ := t2
  let t2' : Monomial := ⟨coef2, List.replicate left.length 0 ++ exps2⟩
  have : t2'.toFun (left ++ right) = Monomial.toFun ⟨coef2, exps2⟩ right :=
    Monomial.zeros_append_toFun _
  rw [← this]
  apply isLittleO_of_lt_exps h_basis <;> simpa [t2']

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

Goal state before:
pp: a : ONote
ha : a.NF
b : ONote
hb : b.NF
⊢ (cmp ⟨a, ha⟩ ⟨b, hb⟩).Compares ⟨a, ha⟩ ⟨b, hb⟩

Tactic:
dsimp [cmp]

Goal state after:
a : ONote
ha : a.NF
b : ONote
hb : b.NF
⊢ (a.cmp b).Compares ⟨a, ha⟩ ⟨b, hb⟩
Module: Mathlib.Tactic.LinearCombinationPrime

Goal state before:
pp: α : Type u_1
a a' b b' : α
inst✝ : AddGroup α
p : a - b = 0
H : a' - b' - (a - b) = 0
⊢ a' - b' = 0

Tactic:
rwa [sub_eq_zero, p] at H

Goal state after: