mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Regular.Free

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x : R
mem : x ∈ ⊥.jacobson
reg : IsSMulRegular M x
free : Free (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
this : Module.Finite (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
I : Type u_2 := Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b : Basis (Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)) (R ⧸ Ideal.span {x}) (QuotSMulTop x M) :=
  Free.chooseBasis (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b' : QuotSMulTop x M ≃ₗ[R] I →₀ R ⧸ Ideal.span {x} := LinearEquiv.restrictScalars R b.repr
f : (I →₀ R) →ₗ[R] QuotSMulTop x M := ↑b'.symm ∘ₗ Finsupp.mapRange.linearMap (Submodule.mkQ (Ideal.span {x}))
g : (I →₀ R) →ₗ[R] M
hg : (x • ⊤).mkQ ∘ₗ g = f
surjf : Function.Surjective ⇑f
lejac : Ideal.span {x} ≤ ⊥.jacobson
surjg : Function.Surjective ⇑g
⊢ (Finsupp.mapRange.linearMap (Submodule.mkQ (Ideal.span {x}))).ker = x • ⊤

Tactic:
rw [Finsupp.ker_mapRange, Submodule.ker_mkQ, ← (Ideal.span {x}).mul_top, ← smul_eq_mul,
      Finsupp.submodule_smul]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x : R
mem : x ∈ ⊥.jacobson
reg : IsSMulRegular M x
free : Free (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
this : Module.Finite (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
I : Type u_2 := Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b : Basis (Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)) (R ⧸ Ideal.span {x}) (QuotSMulTop x M) :=
  Free.chooseBasis (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b' : QuotSMulTop x M ≃ₗ[R] I →₀ R ⧸ Ideal.span {x} := LinearEquiv.restrictScalars R b.repr
f : (I →₀ R) →ₗ[R] QuotSMulTop x M := ↑b'.symm ∘ₗ Finsupp.mapRange.linearMap (Submodule.mkQ (Ideal.span {x}))
g : (I →₀ R) →ₗ[R] M
hg : (x • ⊤).mkQ ∘ₗ g = f
surjf : Function.Surjective ⇑f
lejac : Ideal.span {x} ≤ ⊥.jacobson
surjg : Function.Surjective ⇑g
⊢ (Ideal.span {x} • Finsupp.submodule fun x ↦ ⊤) = x • ⊤
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 :
  X ^ ((map (Ideal.Quotient.mk I)) g).order.toNat * q =
    ↑⋯.unit⁻¹ * (↑r - ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g) * q)
i✝¹ i✝ i : ℕ
⊢ (coeff i) ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g) ∈ I

Tactic:
simp_rw [Polynomial.coeff_coe, g.coeff_trunc_order_mem]

Goal state after:
Module: Mathlib.RingTheory.Regular.ProjectiveDimension

Goal state before:
pp: 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
mem : x ∈ maximalIdeal R
sub : Subsingleton ↑M ↔ Subsingleton (QuotSMulTop x ↑M)
n : ℕ
h : Module.Projective R (QuotSMulTop x ↑M)
this✝ : Free R (QuotSMulTop x ↑M)
ntr : Nontrivial (QuotSMulTop x ↑M)
this : x = 0
reg : Subsingleton ↑M
⊢ False

Tactic:
absurd not_subsingleton_iff_nontrivial.mpr ntr

Goal state after:
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
mem : x ∈ maximalIdeal R
sub : Subsingleton ↑M ↔ Subsingleton (QuotSMulTop x ↑M)
n : ℕ
h : Module.Projective R (QuotSMulTop x ↑M)
this✝ : Free R (QuotSMulTop x ↑M)
ntr : Nontrivial (QuotSMulTop x ↑M)
this : x = 0
reg : Subsingleton ↑M
⊢ Subsingleton (QuotSMulTop x ↑M)
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
a : A
f✝ f'✝ : A⟦X⟧
inst✝ : IsAdicComplete I A
f f' : A⟦X⟧ ⧸ Ideal.span {g}
⊢ Quotient.lift (fun f ↦ H.mod f) ⋯ (f + f') =
    Quotient.lift (fun f ↦ H.mod f) ⋯ f + Quotient.lift (fun f ↦ H.mod f) ⋯ f'

Tactic:
obtain ⟨f, rfl⟩ := Ideal.Quotient.mk_surjective f

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
a : A
f✝ f'✝ : A⟦X⟧
inst✝ : IsAdicComplete I A
f' : A⟦X⟧ ⧸ Ideal.span {g}
f : A⟦X⟧
⊢ Quotient.lift (fun f ↦ H.mod f) ⋯ ((Ideal.Quotient.mk (Ideal.span {g})) f + f') =
    Quotient.lift (fun f ↦ H.mod f) ⋯ ((Ideal.Quotient.mk (Ideal.span {g})) f) + Quotient.lift (fun f ↦ H.mod f) ⋯ f'
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
a✝ : A
f✝ f' : A⟦X⟧
inst✝ : IsAdicComplete I A
a : A
f : A⟦X⟧ ⧸ Ideal.span {g}
⊢ Quotient.lift (fun f ↦ H.mod f) ⋯ (a • f) = (RingHom.id A) a • Quotient.lift (fun f ↦ H.mod f) ⋯ f

Tactic:
obtain ⟨f, rfl⟩ := Ideal.Quotient.mk_surjective f

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
a✝ : A
f✝ f' : A⟦X⟧
inst✝ : IsAdicComplete I A
a : A
f : A⟦X⟧
⊢ Quotient.lift (fun f ↦ H.mod f) ⋯ (a • (Ideal.Quotient.mk (Ideal.span {g})) f) =
    (RingHom.id A) a • Quotient.lift (fun f ↦ H.mod f) ⋯ ((Ideal.Quotient.mk (Ideal.span {g})) f)
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.span {g}
⊢ (Ideal.Quotient.mk (Ideal.span {g})) ↑(H.mod' f) = f

Tactic:
obtain ⟨f, rfl⟩ := Ideal.Quotient.mk_surjective f

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' ((Ideal.Quotient.mk (Ideal.span {g})) f)) =
    (Ideal.Quotient.mk (Ideal.span {g})) f
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
g✝ : A⟦X⟧
I✝ : Ideal A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst✝ : IsAdicComplete I A
f : A[X] ⧸ Ideal.span {g}
h✝ : Nontrivial A
hI : I ≠ ⊤
this : Nontrivial (A ⧸ I)
⊢ ∃ r, r.degree < g.degree ∧ (Ideal.Quotient.mk (Ideal.span {g})) r = f

Tactic:
obtain ⟨f, rfl⟩ := Ideal.Quotient.mk_surjective f

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
g✝ : A⟦X⟧
I✝ : Ideal A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst✝ : IsAdicComplete I A
h✝ : Nontrivial A
hI : I ≠ ⊤
this : Nontrivial (A ⧸ I)
f : A[X]
⊢ ∃ r, r.degree < g.degree ∧ (Ideal.Quotient.mk (Ideal.span {g})) r = (Ideal.Quotient.mk (Ideal.span {g})) f
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
inst✝ : IsAdicComplete I A
x : A⟦X⟧ ⧸ Ideal.span {g}
⊢ H.algEquivQuotient.symm x = (Ideal.Quotient.mk (Ideal.span {f})) (⋯.mod' ((Ideal.quotientEquivAlgOfEq A ⋯) x))

Tactic:
simp [algEquivQuotient]

Goal state after:
Module: Mathlib.RingTheory.RegularLocalRing.Polynomial

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
p : Ideal R[X]
inst✝ : p.IsPrime
max : comap C p = maximalIdeal R
q : Ideal R[X] := ⋯
qle : q ≤ p
reg : ↑(Submodule.spanFinrank (maximalIdeal R)) = ringKrullDim R
fg' : (maximalIdeal R).FG
fg : (Submodule.generators (maximalIdeal R)).Finite
ht : (maximalIdeal R).height ≤ q.height
eq : ¬p = q
lt : q < p
this : (comap C p).IsMaximal
y : R[X]
left✝ : y.Monic
hy : p = Ideal.map C (comap C p) ⊔ span {y}
peq : p = span (⇑(algebraMap R R[X]) '' Submodule.generators (maximalIdeal R) ∪ {y})
⊢ ↑(Submodule.spanFinrank
        (span
          (⇑(algebraMap R[X] (Localization.AtPrime p)) ''
            (⇑(algebraMap R R[X]) '' Submodule.generators (maximalIdeal R) ∪ {y})))) ≤
    ↑((maximalIdeal R).height + 1)

Tactic:
rw [WithBot.coe_add, maximalIdeal_height_eq_ringKrullDim, WithBot.coe_one, ← reg,
      ← Nat.cast_one, ← Nat.cast_add, Nat.cast_le]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
p : Ideal R[X]
inst✝ : p.IsPrime
max : comap C p = maximalIdeal R
q : Ideal R[X] := Ideal.map C (maximalIdeal R)
qle : q ≤ p
reg : ↑(Submodule.spanFinrank (maximalIdeal R)) = ringKrullDim R
fg' : (maximalIdeal R).FG
fg : (Submodule.generators (maximalIdeal R)).Finite
ht : (maximalIdeal R).height ≤ q.height
eq : ¬p = q
lt : q < p
this : (comap C p).IsMaximal
y : R[X]
left✝ : y.Monic
hy : p = Ideal.map C (comap C p) ⊔ span {y}
peq : p = span (⇑(algebraMap R R[X]) '' Submodule.generators (maximalIdeal R) ∪ {y})
⊢ Submodule.spanFinrank
      (span
        (⇑(algebraMap R[X] (Localization.AtPrime p)) ''
          (⇑(algebraMap R R[X]) '' Submodule.generators (maximalIdeal R) ∪ {y}))) ≤
    Submodule.spanFinrank (maximalIdeal R) + 1
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
inst✝ : IsSimpleModule R M
S : Submodule R M
hS : IsSimpleModule R ↥S
⊢ Nonempty (↥S ≃ₗ[R] M)

Tactic:
isSimpleModule_iff_isAtom,

Goal state after:
R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
S : Submodule R M
hS : IsAtom S
⊢ Nonempty (↥S ≃ₗ[R] M)
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
inst✝ : IsSemisimpleModule R M
m : Submodule R M
h : m.IsFullyInvariant
S : Submodule R M
le : S ≤ m
x✝¹ : IsSimpleModule R ↥S
S' : Submodule R M
x✝ : S' ∈ {m | Nonempty (↥m ≃ₗ[R] ↥S)}
e : ↥S' ≃ₗ[R] ↥S
p : M →ₗ[R] M
eq : p ∘ₗ S.subtype = S'.subtype ∘ₗ ↑e.symm
⊢ S' ≤ m

Tactic:
refine le_trans ?_ (Submodule.map_le_iff_le_comap.mpr (le.trans (h p)))

Goal state after:
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
S : Submodule R M
le : S ≤ m
x✝¹ : IsSimpleModule R ↥S
S' : Submodule R M
x✝ : S' ∈ {m | Nonempty (↥m ≃ₗ[R] ↥S)}
e : ↥S' ≃ₗ[R] ↥S
p : M →ₗ[R] M
eq : p ∘ₗ S.subtype = S'.subtype ∘ₗ ↑e.symm
⊢ S' ≤ Submodule.map p S
Module: Mathlib.RingTheory.WittVector.Isocrystal

Goal state before:
pp: case h
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
⊢ Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)

Tactic:
let F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x

Goal state after:
case h
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
⊢ Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #↑s < cof α
h : IsStationary (⋃₀ s)
⊢ ∃ x ∈ s, IsStationary x

Tactic:
by
    contrapose! h
    simp_rw [not_isStationary_iff] at h ⊢
    choose f hf hxf using h
    refine ⟨⋂ x : s, f _ x.2, ?_, ?_⟩
    · apply IsClub.iInter hα <;> simpa
    · rw [disjoint_sUnion_left]
      exact fun x hx ↦ (hxf _ hx).mono_right (iInter_subset _ ⟨x, hx⟩)

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case cons'
α : Type u_1
b✝¹ b✝ : Bool
b : Lists' α b✝
a : Lists' α true
a_ih✝ :
  ∀ (h : true = b✝),
    let l' := ⋯ ▸ b;
    ofList l'.toList = l'
IH :
  ∀ (h : true = true),
    let l' := ⋯ ▸ a;
    ofList l'.toList = l'
h : true = true
⊢ let l' := ⋯ ▸ b.cons' a;
  ofList l'.toList = l'

Tactic:
| cons' b a _ IH =>

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' _

Goal state after:
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' ∈ (single e' x + f).support
Module: Mathlib.SetTheory.ZFC.PSet

Goal state before:
pp: x : PSet.{u}
⊢ (⋃₀ x).toSet = ⋃₀ (toSet '' x.toSet)

Tactic:
by
  ext
  simp

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

Goal state before:
pp: case eq.inr
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
nhl : ↑n₂ ≤ ↑n₁
nhr : ↑n₂ < ↑n₁ ∧ Ordering.gt = Ordering.eq ∨ ¬↑n₂ < ↑n₁ ∧ Ordering.eq = Ordering.eq
⊢ (Ordering.eq.then (Ordering.eq.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)

Tactic:
rcases nhr with nhr | nhr

Goal state after:
case eq.inr.inl
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
nhl : ↑n₂ ≤ ↑n₁
nhr : ↑n₂ < ↑n₁ ∧ Ordering.gt = Ordering.eq
⊢ (Ordering.eq.then (Ordering.eq.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)

case eq.inr.inr
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
nhl : ↑n₂ ≤ ↑n₁
nhr : ¬↑n₂ < ↑n₁ ∧ Ordering.eq = Ordering.eq
⊢ (Ordering.eq.then (Ordering.eq.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x : ZFSet.{u_1}
⊢ {x, x} = {x}

Tactic:
by
  ext
  simp

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

Goal state before:
pp: a : ZFSet.{u_1}
p : ZFSet.{u_1} → Prop
⊢ ↑(ZFSet.sep p a) = {x | x ∈ a ∧ p x}

Tactic:
by
  ext
  simp

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

Goal state before:
pp: case oadd.lt
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.lt
⊢ (e'.oadd n' a').NFBelow b

pp: case oadd.eq
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.eq
⊢ (e.oadd (n + n') a').NFBelow b

pp: case oadd.gt
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.gt
⊢ (e.oadd n (e'.oadd n' a')).NFBelow b

Tactic:
· exact h'

Goal state after:
case oadd.eq
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.eq
⊢ (e.oadd (n + n') a').NFBelow b

case oadd.gt
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.gt
⊢ (e.oadd n (e'.oadd n' a')).NFBelow b
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: ⊢ ⋃₀ ∅ = ∅

Tactic:
by
  ext
  simp

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

Goal state before:
pp: x : ZFSet.{u}
⊢ ↑(⋃₀ x) = ⋃₀ (SetLike.coe '' ↑x)

Tactic:
by
  ext
  simp

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

Goal state before:
pp: x y : ZFSet.{u}
hxy : x ⊆ y
⊢ x ∩ y = x

Tactic:
by ext; simpa using @hxy _

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

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

Tactic:
by
  ext
  simp

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

Goal state before:
pp: o : Ordinal.{u_1}
x : PSet.{u_1}
⊢ x.rank ≤ o ↔ ∀ y ∈ x, y.rank < o

Tactic:
exact rank_le_iff

Goal state after:
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
⊢ y = f z

Tactic:
let ⟨w, _, we⟩ := mem_image.1 yx
    let ⟨wz, fy⟩ := pair_injective we
    rw [← fy, wz]

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

Goal state before:
pp: x : ZFSet.{u}
o : Ordinal.{u}
⊢ x.rank ≤ o ↔ ∀ y ∈ x, y.rank < o

Tactic:
exact rank_le_iff

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

Goal state before:
pp: ⊢ ⋃₀ ∅ = ∅

Tactic:
by
  ext
  simp

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

Goal state before:
pp: case mp
x : ZFSet.{u}
h : x.IsTransitive
y : ZFSet.{u}
hy : y ∈ ⋃₀ x
⊢ y ∈ x

Tactic:
obtain ⟨z, hz, hz'⟩ := mem_sUnion.1 hy

Goal state after:
case mp
x : ZFSet.{u}
h : x.IsTransitive
y : ZFSet.{u}
hy : y ∈ ⋃₀ x
z : ZFSet.{u}
hz : z ∈ x
hz' : y ∈ z
⊢ y ∈ x
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: case mp
o : Ordinal.{u_1}
x : ZFSet.{u_1}
⊢ x ⊆ V_ o → ∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o

Tactic:
intro hx y hy

Goal state after:
case mp
o : Ordinal.{u_1}
x : ZFSet.{u_1}
hx : x ⊆ V_ o
y : ZFSet.{u_1}
hy : y ∈ x
⊢ y.rank < o
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: case mpr
o : Ordinal.{u_1}
x : ZFSet.{u_1}
⊢ (∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o) → x ⊆ V_ o

Tactic:
intro hx y hy

Goal state after:
case mpr
o : Ordinal.{u_1}
x : ZFSet.{u_1}
hx : ∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o
y : ZFSet.{u_1}
hy : y ∈ x
⊢ y ∈ V_ o
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
x✝ : ZFSet.{u_1}
⊢ x✝ ∈ ↑o.toZFSet ↔ x✝ ∈ toZFSet '' Iio o

Tactic:
simp [mem_toZFSet_iff]

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

Goal state before:
pp: z✝ : ZFSet.{u_1}
⊢ z✝ ∈ toZFSet 0 ↔ z✝ ∈ ∅

Tactic:
simp [mem_toZFSet_iff]

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

Goal state before:
pp: x : ONote
inst✝ : x.NF
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
⊢ x.scale (e.oadd n a) = Mul.mul (x.oadd 1 0) (e.oadd n a)

Tactic:
simp only [scale]

Goal state after:
x : ONote
inst✝ : x.NF
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
⊢ (x + e).oadd n (x.scale a) = Mul.mul (x.oadd 1 0) (e.oadd n a)
Module: Mathlib.Tactic.ComputeAsymptotics.Lemmas

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f : 𝕜 → α
c : 𝕜
h_neg : Tendsto (fun x ↦ f (c - x⁻¹)) atTop l
h_pos : Tendsto (fun x ↦ f (c + x⁻¹)) atTop l
⊢ Tendsto f (𝓝[≠] c) l

Tactic:
simpa [Tendsto, ← nhdsLT_sup_nhdsGT] using
    ⟨tendsto_nhdsLT_of_tendsto_atTop _ _ h_neg, tendsto_nhdsGT_of_tendsto_atTop _ _ h_pos⟩

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

Goal state before:
pp: case neg
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
h' : Seq.cons x s ≠ Seq.cons x t
h_if : ¬some x :: ↑s = some x :: ↑t
⊢ Nat.find ⋯ = Nat.find ⋯ + 1

Tactic:
· convert! Nat.find_comp_succ _ _ _
    simp [Stream'.cons]

Goal state after:
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 = 2⁻¹ * dist s.tail t.tail

Tactic:
cases s <;> cases t <;> simp at h <;> simp [h]

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

Goal state before:
pp: basis : Basis
n : ℕ
h : n < List.length basis
⊢ (monomial basis n).toFun = basis[n]

Tactic:
let n' : Fin basis.length := ⟨n, h⟩

Goal state after:
basis : Basis
n : ℕ
h : n < List.length basis
n' : Fin (List.length basis) := ⟨n, h⟩
⊢ (monomial basis n).toFun = basis[n]
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons.cons.inr
exps_hd : ℝ
exps_tl : List ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_length : (exps_hd :: exps_tl).length = (basis_hd :: basis_tl).length
h : exps_hd = 0 ∧ FirstNonzeroIsNeg exps_tl
⊢ Tendsto (toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop (𝓝 0)

Tactic:
· have h_eq : UnitMonomial.toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) =
                    UnitMonomial.toFun exps_tl basis_tl := by
          ext x; simp [UnitMonomial.toFun, h.left]
        rw [h_eq]
        exact toFun_tendsto_zero_of_firstNonzeroIsNeg h_basis.tail (by simpa using h_length) h.right

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

Goal state before:
pp: case step
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < ↑exp ∧ motive tl
⊢ ∀ (hd : ℝ × MultiseriesExpansion basis_tl) (tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)),
    motive (Seq.cons hd tl) → (∀ x ∈ tl.head, hd > x) ∧ motive tl

Tactic:
· intro (exp, coef) tl h
      constructor
      · intro (tl_exp, tl_coef) h_tl
        rw [gt_iff_lt, lt_iff_lt]
        replace h_step := (h_step exp coef tl h).right.left
        cases tl <;> simp [leadingExp, head] at h_tl h_step
        grind
      · grind [h_step exp coef tl h]

Goal state after: