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

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

Tactic:
split_ifs

Goal state after:
case pos
A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
g : A⟦X⟧
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
h✝ : (map (IsLocalRing.residue A)) g ≠ 0
⊢ IsWeierstrassDivisorAt.mod ⋯ 0 = 0

case neg
A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
g : A⟦X⟧
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
h✝ : ¬(map (IsLocalRing.residue A)) g ≠ 0
⊢ 0 = 0
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
H : (X ^ ((map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g q r
⊢ IsUnit q

Tactic:
obtain ⟨H1 : r.degree < (g.map (IsLocalRing.residue A)).order.toNat, H2⟩ := H

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
H1 : r.degree < ↑((map (IsLocalRing.residue A)) g).order.toNat
H2 : X ^ ((map (IsLocalRing.residue A)) g).order.toNat = g * q + ↑r
⊢ IsUnit q
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
I : Ideal R
f : M →ₗ[R] N
surj : Function.Surjective ⇑f
inst✝ : Module.Flat R N
x : M
hx : x ∈ f.ker ⊓ I • ⊤
y : TensorProduct R (↥I) M
hy : (↑(TensorProduct.lid R M) ∘ₗ rTensor M (Submodule.subtype I)) y = x
⊢ x ∈ I • f.ker

Tactic:
have inj : Function.Injective ((TensorProduct.lid R N).comp (I.subtype.rTensor N)) := by
      simpa using Module.Flat.iff_rTensor_injective'.mp ‹_› I

Goal state after:
case refine_1
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
I : Ideal R
f : M →ₗ[R] N
surj : Function.Surjective ⇑f
inst✝ : Module.Flat R N
x : M
hx : x ∈ f.ker ⊓ I • ⊤
y : TensorProduct R (↥I) M
hy : (↑(TensorProduct.lid R M) ∘ₗ rTensor M (Submodule.subtype I)) y = x
inj : Function.Injective ⇑(↑(TensorProduct.lid R N) ∘ₗ rTensor N (Submodule.subtype I))
⊢ x ∈ I • f.ker
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: R✝ Γ : Type
inst✝⁶ : Ring R✝
inst✝⁵ : DecidableEq R✝
inst✝⁴ : IsDomain R✝
inst✝³ : LinearOrderedCommGroupWithZero Γ
R : Type
inst✝² : Semiring R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R
x✝¹ x✝ : R
⊢ (if x✝ = 0 then x✝¹ = 0 else True) ∨ if x✝¹ = 0 then x✝ = 0 else True

Tactic:
split_ifs

Goal state after:
case pos
R✝ Γ : Type
inst✝⁶ : Ring R✝
inst✝⁵ : DecidableEq R✝
inst✝⁴ : IsDomain R✝
inst✝³ : LinearOrderedCommGroupWithZero Γ
R : Type
inst✝² : Semiring R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R
x✝¹ x✝ : R
h✝¹ : x✝ = 0
h✝ : x✝¹ = 0
⊢ x✝¹ = 0 ∨ x✝ = 0

case neg
R✝ Γ : Type
inst✝⁶ : Ring R✝
inst✝⁵ : DecidableEq R✝
inst✝⁴ : IsDomain R✝
inst✝³ : LinearOrderedCommGroupWithZero Γ
R : Type
inst✝² : Semiring R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R
x✝¹ x✝ : R
h✝¹ : x✝ = 0
h✝ : ¬x✝¹ = 0
⊢ x✝¹ = 0 ∨ True

case pos
R✝ Γ : Type
inst✝⁶ : Ring R✝
inst✝⁵ : DecidableEq R✝
inst✝⁴ : IsDomain R✝
inst✝³ : LinearOrderedCommGroupWithZero Γ
R : Type
inst✝² : Semiring R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R
x✝¹ x✝ : R
h✝¹ : ¬x✝ = 0
h✝ : x✝¹ = 0
⊢ True ∨ x✝ = 0

case neg
R✝ Γ : Type
inst✝⁶ : Ring R✝
inst✝⁵ : DecidableEq R✝
inst✝⁴ : IsDomain R✝
inst✝³ : LinearOrderedCommGroupWithZero Γ
R : Type
inst✝² : Semiring R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R
x✝¹ x✝ : R
h✝¹ : ¬x✝ = 0
h✝ : ¬x✝¹ = 0
⊢ True ∨ True
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: R✝ Γ : Type
inst✝⁶ : Ring R✝
inst✝⁵ : DecidableEq R✝
inst✝⁴ : IsDomain R✝
inst✝³ : LinearOrderedCommGroupWithZero Γ
R : Type
inst✝² : Semiring R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R
z✝ y✝ x✝² : R
x✝¹ : if y✝ = 0 then x✝² = 0 else True
x✝ : if z✝ = 0 then y✝ = 0 else True
⊢ if z✝ = 0 then x✝² = 0 else True

Tactic:
split_ifs

Goal state after:
case pos
R✝ Γ : Type
inst✝⁶ : Ring R✝
inst✝⁵ : DecidableEq R✝
inst✝⁴ : IsDomain R✝
inst✝³ : LinearOrderedCommGroupWithZero Γ
R : Type
inst✝² : Semiring R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R
z✝ y✝ x✝² : R
x✝¹ : if y✝ = 0 then x✝² = 0 else True
x✝ : if z✝ = 0 then y✝ = 0 else True
h✝ : z✝ = 0
⊢ x✝² = 0
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: R✝ Γ : Type
inst✝⁶ : Ring R✝
inst✝⁵ : DecidableEq R✝
inst✝⁴ : IsDomain R✝
inst✝³ : LinearOrderedCommGroupWithZero Γ
R : Type
inst✝² : Semiring R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R
x✝² y✝ z✝ : R
x✝¹ : if z✝ = 0 then x✝² = 0 else True
x✝ : if z✝ = 0 then y✝ = 0 else True
⊢ if z✝ = 0 then x✝² + y✝ = 0 else True

Tactic:
split_ifs

Goal state after:
case pos
R✝ Γ : Type
inst✝⁶ : Ring R✝
inst✝⁵ : DecidableEq R✝
inst✝⁴ : IsDomain R✝
inst✝³ : LinearOrderedCommGroupWithZero Γ
R : Type
inst✝² : Semiring R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R
x✝² y✝ z✝ : R
x✝¹ : if z✝ = 0 then x✝² = 0 else True
x✝ : if z✝ = 0 then y✝ = 0 else True
h✝ : z✝ = 0
⊢ x✝² + y✝ = 0
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: R✝ Γ : Type
inst✝⁶ : Ring R✝
inst✝⁵ : DecidableEq R✝
inst✝⁴ : IsDomain R✝
inst✝³ : LinearOrderedCommGroupWithZero Γ
R : Type
inst✝² : Semiring R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R
x✝¹ y✝ z✝ : R
x✝ : ¬if 0 = 0 then z✝ = 0 else True
⊢ (if y✝ * z✝ = 0 then x✝¹ * z✝ = 0 else True) → if y✝ = 0 then x✝¹ = 0 else True

Tactic:
split_ifs

Goal state after:
case pos
R✝ Γ : Type
inst✝⁶ : Ring R✝
inst✝⁵ : DecidableEq R✝
inst✝⁴ : IsDomain R✝
inst✝³ : LinearOrderedCommGroupWithZero Γ
R : Type
inst✝² : Semiring R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R
x✝¹ y✝ z✝ : R
x✝ : ¬if 0 = 0 then z✝ = 0 else True
h✝¹ : y✝ * z✝ = 0
h✝ : y✝ = 0
⊢ x✝¹ * z✝ = 0 → x✝¹ = 0

case neg
R✝ Γ : Type
inst✝⁶ : Ring R✝
inst✝⁵ : DecidableEq R✝
inst✝⁴ : IsDomain R✝
inst✝³ : LinearOrderedCommGroupWithZero Γ
R : Type
inst✝² : Semiring R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R
x✝¹ y✝ z✝ : R
x✝ : ¬if 0 = 0 then z✝ = 0 else True
h✝¹ : y✝ * z✝ = 0
h✝ : ¬y✝ = 0
⊢ x✝¹ * z✝ = 0 → True

case pos
R✝ Γ : Type
inst✝⁶ : Ring R✝
inst✝⁵ : DecidableEq R✝
inst✝⁴ : IsDomain R✝
inst✝³ : LinearOrderedCommGroupWithZero Γ
R : Type
inst✝² : Semiring R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R
x✝¹ y✝ z✝ : R
x✝ : ¬if 0 = 0 then z✝ = 0 else True
h✝¹ : ¬y✝ * z✝ = 0
h✝ : y✝ = 0
⊢ True → x✝¹ = 0

case neg
R✝ Γ : Type
inst✝⁶ : Ring R✝
inst✝⁵ : DecidableEq R✝
inst✝⁴ : IsDomain R✝
inst✝³ : LinearOrderedCommGroupWithZero Γ
R : Type
inst✝² : Semiring R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R
x✝¹ y✝ z✝ : R
x✝ : ¬if 0 = 0 then z✝ = 0 else True
h✝¹ : ¬y✝ * z✝ = 0
h✝ : ¬y✝ = 0
⊢ True → True
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: R✝ Γ : Type
inst✝⁶ : Ring R✝
inst✝⁵ : DecidableEq R✝
inst✝⁴ : IsDomain R✝
inst✝³ : LinearOrderedCommGroupWithZero Γ
R : Type
inst✝² : Semiring R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R
⊢ ¬if 0 = 0 then 1 = 0 else True

Tactic:
split_ifs

Goal state after:
case pos
R✝ Γ : Type
inst✝⁶ : Ring R✝
inst✝⁵ : DecidableEq R✝
inst✝⁴ : IsDomain R✝
inst✝³ : LinearOrderedCommGroupWithZero Γ
R : Type
inst✝² : Semiring R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R
h✝ : 0 = 0
⊢ ¬1 = 0

case neg
R✝ Γ : Type
inst✝⁶ : Ring R✝
inst✝⁵ : DecidableEq R✝
inst✝⁴ : IsDomain R✝
inst✝³ : LinearOrderedCommGroupWithZero Γ
R : Type
inst✝² : Semiring R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R
h✝ : ¬0 = 0
⊢ ¬True
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: R Γ : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
inst✝¹ : IsDomain R
inst✝ : LinearOrderedCommGroupWithZero Γ
h : ValuativeRel R
hv : Valuation.Compatible 1
x✝¹ x✝ : R
⊢ 1 x✝¹ ≤ 1 x✝ ↔ if x✝ = 0 then x✝¹ = 0 else True

Tactic:
split_ifs

Goal state after:
case pos
R Γ : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
inst✝¹ : IsDomain R
inst✝ : LinearOrderedCommGroupWithZero Γ
h : ValuativeRel R
hv : Valuation.Compatible 1
x✝¹ x✝ : R
h✝ : x✝ = 0
⊢ 1 x✝¹ ≤ 1 x✝ ↔ x✝¹ = 0

case neg
R Γ : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
inst✝¹ : IsDomain R
inst✝ : LinearOrderedCommGroupWithZero Γ
h : ValuativeRel R
hv : Valuation.Compatible 1
x✝¹ x✝ : R
h✝ : ¬x✝ = 0
⊢ 1 x✝¹ ≤ 1 x✝ ↔ True
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
J I : Ideal R
sq : I ^ 2 = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
⊢ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J)) ≤ f.ker

Tactic:
pow_two

Goal state after:
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))
⊢ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J)) ≤ f.ker
Module: Mathlib.SetTheory.Cardinal.EventuallyConst

Goal state before:
pp: β : Type v
inst✝¹ : PartialOrder β
f : Cardinal.{v} → β
inst✝ : Small.{v, v} β
hf : Monotone f
⊢ EventuallyConst f atTop

Tactic:
by
  refine .of_monotone_of_lt_cof hf ?_
  simpa [← small_iff_lift_mk_lt_univ]

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

Goal state before:
pp: β : Type v
inst✝¹ : PartialOrder β
f : Ordinal.{v} → β
inst✝ : Small.{v, v} β
hf : Monotone f
⊢ EventuallyConst f atTop

Tactic:
by
  refine .of_monotone_of_lt_cof hf ?_
  simpa [← small_iff_lift_mk_lt_univ]

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

Goal state before:
pp: case pos
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ z.length
hp : x <+: z
⊢ z ∈ pullSub (pullSub T y) x ↔ z ∈ pullSub T (x ++ y)

Tactic:
obtain ⟨z, rfl⟩ := hp

Goal state after:
case pos
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ (x ++ z).length
⊢ x ++ z ∈ pullSub (pullSub T y) x ↔ x ++ z ∈ pullSub T (x ++ y)
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case ind
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x₁ x₂ : α
h : x₁ ≤ x₂
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x₁ y ≤ lfpApprox f x₂ y
⊢ x₁ ⊔ ⨆ b, ⨆ (_ : b < i), f (lfpApprox f x₁ b) ≤ x₂ ⊔ ⨆ b, ⨆ (_ : b < i), f (lfpApprox f x₂ b)

Tactic:
exact sup_le_sup h <| iSup₂_mono fun j hj ↦ f.mono (IH j hj)

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

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x a : α
ha : a ∈ fixedPoints ⇑f
hxa : x ≤ a
i : Ordinal.{u}
⊢ lfpApprox f x i ≤ a

Tactic:
by
  induction i using WellFoundedLT.induction with | ind i IH
  rw [lfpApprox]
  apply sup_le hxa
  rw [iSup₂_le_iff, ← ha.eq]
  exact fun y hy ↦ f.mono (IH y hy)

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

Goal state before:
pp: case inr
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
hf : f e = 0
⊢ eval b (single e x + f) = b ^ e * x + eval b f

Tactic:
rw [eval, support_single_add (by simpa) hx, Finset.sort_cons]

Goal state after:
case inr
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
hf : f e = 0
⊢ foldr (fun p r ↦ b ^ p * (single e x + f) p + r) 0 (e :: f.support.sort fun x1 x2 ↦ x1 ≥ x2) = b ^ e * x + eval b f

case inr.h₁
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
hf : f e = 0
⊢ ∀ b ∈ f.support, e ≥ b
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: ⊢ NF 1

Tactic:
rw [← ofNat_one]

Goal state after:
⊢ (↑1).NF
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: case refine_1
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsNormal (enumOrd s)
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
⊢ ⨆ i, f i ∈ s

pp: case refine_2
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
⊢ enumOrd s a ≤ o

Tactic:
· let g : ι → Ordinal.{u} := fun i => (enumOrdOrderIso s hs).symm ⟨_, hf i⟩
    suffices enumOrd s (⨆ i, g i) = ⨆ i, f i by
      rw [← this]
      exact enumOrd_mem hs _
    rw [h.map_iSup bddAbove_of_small]
    congr
    ext x
    change (enumOrdOrderIso s hs _).val = f x
    rw [OrderIso.apply_symm_apply]

Goal state after:
case refine_2
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
⊢ enumOrd s a ≤ o
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x : PSet.{u_1}
⊢ (mk x).Nonempty ↔ x.Nonempty

Tactic:
by
  refine ⟨?_, fun ⟨a, h⟩ => ⟨mk a, h⟩⟩
  rintro ⟨a, h⟩
  induction a using Quotient.inductionOn
  exact ⟨_, h⟩

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

Goal state before:
pp: e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this : a.NF
h' : (a.add o).repr = a.repr + o.repr
nf : (a + o).NF
⊢ (e.oadd n a + o).repr = (e.oadd n a).repr + o.repr

Tactic:
conv at nf => simp [HAdd.hAdd, Add.add]

Goal state after:
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this : a.NF
h' : (a.add o).repr = a.repr + o.repr
nf : (a.add o).NF
⊢ (e.oadd n a + o).repr = (e.oadd n a).repr + o.repr
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x y : ZFSet.{u}
hxy : x ⊆ y
z✝ : ZFSet.{u}
⊢ z✝ ∈ x ∩ y ↔ z✝ ∈ x

Tactic:
simpa using @hxy _

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
⊢ cmp (veblenWith f o₁ a) (veblenWith f o₂ b) =
    match cmp o₁ o₂ with
    | Ordering.eq => cmp a b
    | Ordering.lt => cmp a (veblenWith f o₂ b)
    | Ordering.gt => cmp (veblenWith f o₁ a) b

Tactic:
by
  obtain h | rfl | h := lt_trichotomy o₁ o₂
  on_goal 2 => simp [(veblenWith_right_strictMono hf _).cmp_map_eq]
  all_goals
    conv_lhs => rw [← veblenWith_veblenWith_of_lt hf h]
    simp [h.cmp_eq_lt, h.cmp_eq_gt, (veblenWith_right_strictMono hf _).cmp_map_eq]

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} ∨ z = {x, y} ↔ z = {x'} ∨ z = {x', y'}
⊢ x = x' ∧ ?m.27

Tactic:
by simpa [or_and_left] using (H {x}).1 (Or.inl rfl)

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

Goal state before:
pp: o : Ordinal.{u}
x y : ZFSet.{u}
h : x ⊆ y
hy : y ∈ V_ o
⊢ x ∈ V_ o

Tactic:
rw [mem_vonNeumann] at *
  exact (rank_mono h).trans_lt hy

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

Goal state before:
pp: ⊢ ∀ (y : ZFSet.{u_1}), y ∉ V_ 0

Tactic:
by simp [mem_vonNeumann]

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

Goal state before:
pp: ⊢ Monotone toZFSet

Tactic:
intro a b h x hx
  obtain ⟨c, hc, rfl⟩ := mem_toZFSet_iff.1 hx
  exact toZFSet_mem_toZFSet_of_lt (hc.trans_le h)

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

Goal state before:
pp: x✝¹ y z w : ZFSet.{u}
x✝ : { x // x.IsOrdinal }
x : ZFSet.{?u.18}
hx : x.IsOrdinal
⊢ (fun o ↦ ⟨o.toZFSet, ⋯⟩) ((fun x ↦ (↑x).rank) ⟨x, hx⟩) = ⟨x, hx⟩

Tactic:
simpa using hx.toZFSet_rank_eq

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

Goal state before:
pp: case neg.e_a.e_a
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
ao : a₁.repr + ω ^ e₁.repr * ↑↑n₁ = ω ^ e₁.repr * ↑↑n₁
e0 : ¬e₂ = 0
this✝ : e₁.NF
this : e₂.NF
⊢ ω ^ e₁.repr * ω ^ e₂.repr = (ω ^ e₁.repr * ↑↑n₁ + a₁.repr) * ω ^ e₂.repr

Tactic:
have := mt repr_inj.1 e0

Goal state after:
case neg.e_a.e_a
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
ao : a₁.repr + ω ^ e₁.repr * ↑↑n₁ = ω ^ e₁.repr * ↑↑n₁
e0 : ¬e₂ = 0
this✝¹ : e₁.NF
this✝ : e₂.NF
this : ¬e₂.repr = repr 0
⊢ ω ^ e₁.repr * ω ^ e₂.repr = (ω ^ e₁.repr * ↑↑n₁ + a₁.repr) * ω ^ e₂.repr
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.repr - 1) = e.repr

Tactic:
have := mt repr_inj.1 e0

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
this : ¬e.repr = repr 0
⊢ 1 + (e.repr - 1) = e.repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝ : e.NF
this : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + ↑m'
⊢ ω ^ e.repr = ω ^ 1 * ω ^ (e.repr - 1)

Tactic:
have := mt repr_inj.1 e0

Goal state after:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝¹ : e.NF
this✝ : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + ↑m'
this : ¬e.repr = repr 0
⊢ ω ^ e.repr = ω ^ 1 * ω ^ (e.repr - 1)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized

Goal state before:
pp: f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
t : ℝ
⊢ 0 < f t → (f ^ exp') t = 0 → (f ^ exp) t = 0

Tactic:
h1

Goal state after:
f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
t : ℝ
h1 : 0 < f t
⊢ (f ^ exp') t = 0 → (f ^ exp) t = 0
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis

Goal state before:
pp: case cons
hd : ℝ → ℝ
tl : List (ℝ → ℝ)
ih : WellFormedBasis tl → ∀ᶠ (x : ℝ) in atTop, ∀ f ∈ tl, 0 < f x
h :
  ((∀ a' ∈ tl, (Real.log ∘ a') =o[atTop] (Real.log ∘ hd)) ∧
      List.Pairwise (fun x y ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) tl) ∧
    Tendsto hd atTop atTop ∧ ∀ a ∈ tl, Tendsto a atTop atTop
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ f ∈ hd :: tl, 0 < f x

Tactic:
simp only [List.mem_cons, forall_eq_or_imp]

Goal state after:
case cons
hd : ℝ → ℝ
tl : List (ℝ → ℝ)
ih : WellFormedBasis tl → ∀ᶠ (x : ℝ) in atTop, ∀ f ∈ tl, 0 < f x
h :
  ((∀ a' ∈ tl, (Real.log ∘ a') =o[atTop] (Real.log ∘ hd)) ∧
      List.Pairwise (fun x y ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) tl) ∧
    Tendsto hd atTop atTop ∧ ∀ a ∈ tl, Tendsto a atTop atTop
⊢ ∀ᶠ (x : ℝ) in atTop, 0 < hd x ∧ ∀ a ∈ tl, 0 < a x
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, op') => (hd, ↑op' s.tail))
              (T s.head)
n : ℕ
ih :
  ∀ {op : Stream'.Seq α → Stream'.Seq α},
    motive op → ∀ (s t : Stream'.Seq α), dist s t ≤ 2⁻¹ ^ n → dist (op s) (op t) ≤ 2⁻¹ ^ n
op : Stream'.Seq α → Stream'.Seq α
h_base : motive op
s t : Stream'.Seq α
hn : dist s t ≤ 2⁻¹ ^ (n + 1)
T : Option α → Option (α × Subtype motive)
hT :
  ∀ (s : Stream'.Seq α),
    (op s).destruct =
      Option.map
        (fun x ↦
          match x with
          | (hd, op') => (hd, ↑op' s.tail))
        (T s.head)
⊢ s.head = t.head

Tactic:
replace hn : dist s t ≤ 2⁻¹ := by
        apply hn.trans
        simp only [pow_succ, inv_pos, Nat.ofNat_pos, mul_le_iff_le_one_left]
        apply pow_le_one₀ <;> norm_num

Goal state after:
α : Type u_1
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, op') => (hd, ↑op' s.tail))
              (T s.head)
n : ℕ
ih :
  ∀ {op : Stream'.Seq α → Stream'.Seq α},
    motive op → ∀ (s t : Stream'.Seq α), dist s t ≤ 2⁻¹ ^ n → dist (op s) (op t) ≤ 2⁻¹ ^ n
op : Stream'.Seq α → Stream'.Seq α
h_base : motive op
s t : Stream'.Seq α
T : Option α → Option (α × Subtype motive)
hT :
  ∀ (s : Stream'.Seq α),
    (op s).destruct =
      Option.map
        (fun x ↦
          match x with
          | (hd, op') => (hd, ↑op' s.tail))
        (T s.head)
hn : dist s t ≤ 2⁻¹
⊢ s.head = t.head
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o a : Ordinal.{u_1}
h : a < o * ω
i : Ordinal.{u_1}
hi : i < ω
h' : a < o * i
⊢ ∃ i, a < o * ↑i + o

Tactic:
obtain ⟨i, rfl⟩ := lt_omega0.1 hi

Goal state after:
o a : Ordinal.{u_1}
h : a < o * ω
i : ℕ
hi : ↑i < ω
h' : a < o * ↑i
⊢ ∃ i, a < o * ↑i + o
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons
x exp1 : ℝ
exps1 : List ℝ
ih :
  ∀ {m2 : UnitMonomial} {basis : Basis},
    WellFormedBasis basis →
      exps1.length = List.length m2 →
        (∀ f ∈ basis, 0 < f x) →
          (List.zipWith (fun exp b ↦ b x ^ exp) (List.zipWith (fun x1 x2 ↦ x1 + x2) exps1 m2) basis).prod =
            (List.zipWith (fun exp b ↦ b x ^ exp) exps1 basis).prod *
              (List.zipWith (fun exp b ↦ b x ^ exp) m2 basis).prod
m2 : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : (exp1 :: exps1).length = List.length m2
h_pos : ∀ f ∈ basis, 0 < f x
⊢ (List.zipWith (fun exp b ↦ b x ^ exp) (List.zipWith (fun x1 x2 ↦ x1 + x2) (exp1 :: exps1) m2) basis).prod =
    (List.zipWith (fun exp b ↦ b x ^ exp) (exp1 :: exps1) basis).prod *
      (List.zipWith (fun exp b ↦ b x ^ exp) m2 basis).prod

Tactic:
cases m2 with

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

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

Tactic:
FundamentalSequenceProp

Goal state after:
case oadd.inl.none
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b = 0
e : b.fundamentalSequence = Sum.inl none
⊢ match
    match a.fundamentalSequence, m.natPred with
    | Sum.inl none, 0 => Sum.inl (some zero)
    | Sum.inl none, m.succ => Sum.inl (some (zero.oadd m.succPNat zero))
    | Sum.inl (some a'), 0 => Sum.inr fun i ↦ a'.oadd i.succPNat zero
    | Sum.inl (some a'), m.succ => Sum.inr fun i ↦ a.oadd m.succPNat (a'.oadd i.succPNat zero)
    | Sum.inr f, 0 => Sum.inr fun i ↦ (f i).oadd 1 zero
    | Sum.inr f, m.succ => Sum.inr fun i ↦ a.oadd m.succPNat ((f i).oadd 1 zero) with
  | Sum.inl none => a.oadd m b = 0
  | Sum.inl (some a_1) => (a.oadd m b).repr = succ a_1.repr ∧ ((a.oadd m b).NF → a_1.NF)
  | Sum.inr f =>
    IsSuccLimit (a.oadd m b).repr ∧
      (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a.oadd m b ∧ ((a.oadd m b).NF → (f i).NF)) ∧
        ∀ a_1 < (a.oadd m b).repr, ∃ i, a_1 < (f i).repr