mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Morse

Goal state before:
pp: case hS2
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsDomain S
G : Type u_3
inst✝³ : Group G
inst✝² : MulSemiringAction G S
inst✝¹ : SMulCommClass G R S
f : R[X]
hf : (map (algebraMap R S) f).Splits
inst✝ : MulAction.IsPretransitive G ↑(f.rootSet S)
h : ∀ (m : MaximalSpectrum S), (f.rootSet S).ncard ≤ (f.rootSet (S ⧸ m.asIdeal)).ncard + 1
hG : ⨆ m, Ideal.inertia G m.asIdeal = ⊤
⊢ Subgroup.closure (⋃ m, ↑(Ideal.inertia G m.asIdeal)) = ⊤

Tactic:
· simpa [Subgroup.closure_iUnion]

Goal state after:
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✝ : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
heq : g * q = ↑r
⊢ q = 0 ∧ r = 0

Tactic:
suffices ∀ k i, coeff i q ∈ I ^ k by
    have hq : q = 0 := by
      ext i
      refine IsHausdorff.haus' (I := I) _ fun k ↦ ?_
      rw [SModEq.zero, smul_eq_mul, Ideal.mul_top]
      exact this _ _
    rw [hq, mul_zero, Eq.comm, Polynomial.coe_eq_zero_iff] at heq
    exact ⟨hq, heq⟩

Goal state after:
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 : g * q = ↑r
⊢ ∀ (k i : ℕ), (coeff i) q ∈ I ^ k
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
reg : IsSMulRegular (↑M) x
mem : x ∈ maximalIdeal R
sub : Subsingleton ↑M ↔ Subsingleton (QuotSMulTop x ↑M)
n✝ n : ℕ
S : ShortComplex (ModuleCat R) := M.smulShortComplex x
hS : S.ShortExact
h : HasProjectiveDimensionLE (of R (QuotSMulTop x ↑M)) (n + 1)
L : ModuleCat R
a✝ : Module.Finite R ↑L
zero : Subsingleton (Ext (of R (QuotSMulTop x ↑M)) L (n + 2))
exac :
  { X₁ := AddCommGrpCat.of (Ext S.X₂ L (n + 1)), X₂ := AddCommGrpCat.of (Ext S.X₁ L (n + 1)),
      X₃ := AddCommGrpCat.of (Ext S.X₃ L (n + 2)), f := AddCommGrpCat.ofHom ((Ext.mk₀ S.f).precomp L ⋯),
      g := AddCommGrpCat.ofHom (hS.extClass.precomp L ⋯), zero := ⋯ }.Exact
epi :
  Epi
    { X₁ := AddCommGrpCat.of (Ext S.X₂ L (n + 1)), X₂ := AddCommGrpCat.of (Ext S.X₁ L (n + 1)),
        X₃ := AddCommGrpCat.of (Ext S.X₃ L (n + 2)), f := AddCommGrpCat.ofHom ((Ext.mk₀ S.f).precomp L ⋯),
        g := AddCommGrpCat.ofHom (hS.extClass.precomp L ⋯), zero := ⋯ }.f
⊢ Subsingleton (Ext M L (n + 1))

Tactic:
have : S.f = x • 𝟙 M := rfl

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
reg : IsSMulRegular (↑M) x
mem : x ∈ maximalIdeal R
sub : Subsingleton ↑M ↔ Subsingleton (QuotSMulTop x ↑M)
n✝ n : ℕ
S : ShortComplex (ModuleCat R) := M.smulShortComplex x
hS : S.ShortExact
h : HasProjectiveDimensionLE (of R (QuotSMulTop x ↑M)) (n + 1)
L : ModuleCat R
a✝ : Module.Finite R ↑L
zero : Subsingleton (Ext (of R (QuotSMulTop x ↑M)) L (n + 2))
exac :
  { X₁ := AddCommGrpCat.of (Ext S.X₂ L (n + 1)), X₂ := AddCommGrpCat.of (Ext S.X₁ L (n + 1)),
      X₃ := AddCommGrpCat.of (Ext S.X₃ L (n + 2)), f := AddCommGrpCat.ofHom ((Ext.mk₀ S.f).precomp L ⋯),
      g := AddCommGrpCat.ofHom (hS.extClass.precomp L ⋯), zero := ⋯ }.Exact
epi :
  Epi
    { X₁ := AddCommGrpCat.of (Ext S.X₂ L (n + 1)), X₂ := AddCommGrpCat.of (Ext S.X₁ L (n + 1)),
        X₃ := AddCommGrpCat.of (Ext S.X₃ L (n + 2)), f := AddCommGrpCat.ofHom ((Ext.mk₀ S.f).precomp L ⋯),
        g := AddCommGrpCat.ofHom (hS.extClass.precomp L ⋯), zero := ⋯ }.f
this : S.f = x • 𝟙 M
⊢ Subsingleton (Ext M L (n + 1))
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
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H : (X ^ n).IsWeierstrassDivision g q r
H1 : r.degree < ↑n
f : A[X] := Polynomial.X ^ n - r
⊢ g.IsWeierstrassFactorization f ↑⋯.unit⁻¹

Tactic:
replace H1 : r.degree < (Polynomial.X (R := A) ^ n).degree := by rwa [Polynomial.degree_X_pow]

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
H✝ : (X ^ ((map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g q r
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H : (X ^ n).IsWeierstrassDivision g q r
f : A[X] := Polynomial.X ^ n - r
H1 : r.degree < (Polynomial.X ^ n).degree
⊢ g.IsWeierstrassFactorization f ↑⋯.unit⁻¹
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

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

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

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : IsSimpleRing R
tfae_1_to_2 : IsSemisimpleRing R → IsArtinianRing R
tfae_2_to_3 : IsArtinianRing R → ∃ I, IsAtom I
x✝ : ∃ I, IsAtom I
I : Ideal R
hI : IsAtom I
left✝ : Nontrivial R
h : ∀ (I : Ideal R), Submodule.IsFullyInvariant I → I = ⊥ ∨ I = ⊤
this : IsSimpleModule R ↥I
eq : isotypicComponent R R ↥I = ⊥
⊢ I ∈ {m | Nonempty (↥m ≃ₗ[R] ↥I)}

Tactic:
by exact ⟨.refl ..⟩

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
⊢ IsSimpleRing R ∧ IsArtinianRing R ↔ IsSemisimpleRing R ∧ IsIsotypic R R ∧ Nontrivial R

Tactic:
refine ⟨fun ⟨_, _⟩ ↦ ?_, fun ⟨_, _, _⟩ ↦ ?_⟩
  on_goal 1 => have := IsSimpleRing.isSemisimpleRing_iff_isArtinianRing.mpr ‹_›
  all_goals simp_rw [isIsotypic_iff_isFullyInvariant_imp_bot_or_top,
      isFullyInvariant_iff_isTwoSided, isSimpleRing_iff_isTwoSided_imp] at *
  · exact ⟨this, by rwa [and_comm]⟩
  · exact ⟨⟨‹_›, ‹_›⟩, inferInstance⟩

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
U : Set (PrimeSpectrum R[X])
s : Set R[X]
z : zeroLocus s = Uᶜ
⊢ IsOpen (PrimeSpectrum.comap C '' (⋂ i, zeroLocus {↑i})ᶜ)

Tactic:
compl_iInter,

Goal state after:
R : Type u_1
inst✝ : CommRing R
U : Set (PrimeSpectrum R[X])
s : Set R[X]
z : zeroLocus s = Uᶜ
⊢ IsOpen (PrimeSpectrum.comap C '' ⋃ i, (zeroLocus {↑i})ᶜ)
Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, x ^ n ∈ f.range
hker : RingHom.ker f ≤ nilradical R
q q' : PrimeSpectrum S
hqq' : ∀ (x : R), x ∈ (comap f q).asIdeal ↔ x ∈ (comap f q').asIdeal
x : S
n : ℕ
hn : n > 0
y : R
hy : f y = x ^ n
⊢ f y ∈ q.asIdeal ↔ f y ∈ q'.asIdeal

Tactic:
apply hqq'

Goal state after:
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: case refine_2.add
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 y : M
ymem : y ∈ I • f.ker
z : M
zmem : z ∈ I • f.ker
hy : y ∈ f.ker ⊓ I • ⊤
hz : z ∈ f.ker ⊓ I • ⊤
⊢ y + z ∈ f.ker ⊓ I • ⊤

Tactic:
exact add_mem hy hz

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
h : {k | p k}.Finite
⊢ count p n ≤ {k | p k}.ncard

Tactic:
rw [Set.ncard_def, ← ENat.natCast_le_natCast, ENat.natCast_toNat (by simpa)]

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
h : {k | p k}.Finite
⊢ ↑(count p n) ≤ {k | p k}.encard
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
S T : ↥(tree A)
x : List A
x✝ : pullSub S x ≤ T
⊢ S ≤ subAt T x

Tactic:
by rw [← subAt_pullSub S x]; gcongr

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

Goal state before:
pp: case refine_1
b o : Ordinal.{u_1}
⊢ foldr (fun p r ↦ b ^ p.1 * p.2 + r) 0 [] = 0

Tactic:
foldr_nil

Goal state after:
case refine_1
b o : Ordinal.{u_1}
⊢ 0 = 0
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case cons'
α : Type u_1
C : Lists α → Sort u_2
D : Lists' α true → Sort u_3
C0 : (a : α) → C (atom a)
C1 : (l : Lists' α true) → D l → C (of' l)
D0 : D Lists'.nil
D1 : (a : Lists α) → (l : Lists' α true) → C a → D l → D (Lists'.cons a l)
b b✝ : Bool
a : Lists' α b✝
l : Lists' α true
IH₁ :
  C ⟨b✝, a⟩ ×'
    match b✝, a with
    | true, l => D l
    | false, x => PUnit
IH :
  C ⟨true, l⟩ ×'
    match true, l with
    | true, l => D l
    | false, x => PUnit
⊢ C ⟨true, a.cons' l⟩ ×'
    match true, a.cons' l with
    | true, l => D l
    | false, x => PUnit

Tactic:
have : D (Lists'.cons' a l) := D1 ⟨_, _⟩ _ IH₁.1 IH.2

Goal state after:
case cons'
α : Type u_1
C : Lists α → Sort u_2
D : Lists' α true → Sort u_3
C0 : (a : α) → C (atom a)
C1 : (l : Lists' α true) → D l → C (of' l)
D0 : D Lists'.nil
D1 : (a : Lists α) → (l : Lists' α true) → C a → D l → D (Lists'.cons a l)
b b✝ : Bool
a : Lists' α b✝
l : Lists' α true
IH₁ :
  C ⟨b✝, a⟩ ×'
    match b✝, a with
    | true, l => D l
    | false, x => PUnit
IH :
  C ⟨true, l⟩ ×'
    match true, l with
    | true, l => D l
    | false, x => PUnit
this : D (a.cons' l)
⊢ C ⟨true, a.cons' l⟩ ×'
    match true, a.cons' l with
    | true, l => D l
    | false, x => PUnit
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
this : (∀ (l₁ : Lists α), trans l₁) ×' ∀ (l : Lists' α true) (l' : Lists α), l' ∈ l.toList → trans l'
⊢ ∀ {l₁ l₂ l₃ : Lists α}, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃

Tactic:
by exact this.1

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

Goal state before:
pp: b o : Ordinal.{u_1}
⊢ { entries := map Prod.toSigma (CNF b o), nodupKeys := ⋯ }.entries.keys.toFinset = (map Prod.fst (CNF b o)).toFinset

pp: b o : Ordinal.{u_1}
⊢ ∀ a ∈ { entries := map Prod.toSigma (CNF b o), nodupKeys := ⋯ }.entries, decide (a.snd ≠ 0) = true

Tactic:
· simp [List.keys]

Goal state after:
b o : Ordinal.{u_1}
⊢ ∀ a ∈ { entries := map Prod.toSigma (CNF b o), nodupKeys := ⋯ }.entries, decide (a.snd ≠ 0) = true
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o e c : Ordinal.{u_1}
h : (e, c) ∈ CNF b o
⊢ (AList.lookup e { entries := map Prod.toSigma (CNF b o), nodupKeys := ⋯ }).getD 0 = c

Tactic:
mem_lookup_iff.2,

Goal state after:
b o e c : Ordinal.{u_1}
h : (e, c) ∈ CNF b o
⊢ (some ?m.24).getD 0 = c

b o e c : Ordinal.{u_1}
h : (e, c) ∈ CNF b o
⊢ ⟨e, ?m.24⟩ ∈ { entries := map Prod.toSigma (CNF b o), nodupKeys := ⋯ }.entries

b o e c : Ordinal.{u_1}
h : (e, c) ∈ CNF b o
⊢ Ordinal.{u_1}
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case single_add.h
b : Ordinal.{u_1}
f₂ : Ordinal.{u_1} →₀ Ordinal.{u_1}
e₁ x : Ordinal.{u_1}
f₁ : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf₁ : ∀ c ∈ f₁.support, c < e₁
hx : x ≠ 0
IH : (∀ e₁ ∈ f₁.support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁) → eval b (f₁ + f₂) = eval b f₁ + eval b f₂
h : ∀ e₁_1 ∈ (single e₁ x + f₁).support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁_1
e₂ : Ordinal.{u_1}
⊢ e₂ ∈ (f₁ + f₂).support → e₂ ≤ e₁

Tactic:
he₂

Goal state after:
case single_add.h
b : Ordinal.{u_1}
f₂ : Ordinal.{u_1} →₀ Ordinal.{u_1}
e₁ x : Ordinal.{u_1}
f₁ : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf₁ : ∀ c ∈ f₁.support, c < e₁
hx : x ≠ 0
IH : (∀ e₁ ∈ f₁.support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁) → eval b (f₁ + f₂) = eval b f₁ + eval b f₂
h : ∀ e₁_1 ∈ (single e₁ x + f₁).support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁_1
e₂ : Ordinal.{u_1}
he₂ : e₂ ∈ (f₁ + f₂).support
⊢ e₂ ≤ e₁
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u_1}
⊢ List.Pairwise (fun x1 x2 ↦ x1 ≥ x2) (map Prod.fst (CNF b o))

Tactic:
exact (CNF.sortedGT b o).sortedGE.pairwise

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
h : o ≠ 0
⊢ a ∈ range (veblenWith f o) ↔ ∀ b < o, veblenWith f b a = a

Tactic:
rw [veblenWith_of_ne_zero f h, mem_range_derivFamily (fun _ ↦ isNormal_veblenWith hf _)]

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
h : o ≠ 0
⊢ (∀ (i : ↑(Iio o)), veblenWith f (↑i) a = a) ↔ ∀ b < o, veblenWith f b a = a
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.lt
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
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this✝ : e.NF
this : e'.NF
ee : (e.cmp e').Compares e e'
he : e.cmp e' = Ordering.lt
⊢ (match Ordering.lt with
      | Ordering.lt => e'.oadd n' a'
      | Ordering.eq => e.oadd (n + n') a'
      | Ordering.gt => e.oadd n (e'.oadd n' a')).repr =
    ω ^ e.repr * ↑↑n + (ω ^ e'.repr * ↑↑n' + a'.repr)

Tactic:
simp only [he, Ordering.compares_gt, Ordering.compares_lt,
        Ordering.compares_eq, repr, gt_iff_lt, PNat.add_coe, Nat.cast_add] at ee ⊢

Goal state after:
case oadd.lt
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
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this✝ : e.NF
this : e'.NF
he : e.cmp e' = Ordering.lt
ee : e < e'
⊢ ω ^ e'.repr * ↑↑n' + a'.repr = ω ^ e.repr * ↑↑n + (ω ^ e'.repr * ↑↑n' + a'.repr)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.eq
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
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this✝ : e.NF
this : e'.NF
ee : (e.cmp e').Compares e e'
he : e.cmp e' = Ordering.eq
⊢ (match Ordering.eq with
      | Ordering.lt => e'.oadd n' a'
      | Ordering.eq => e.oadd (n + n') a'
      | Ordering.gt => e.oadd n (e'.oadd n' a')).repr =
    ω ^ e.repr * ↑↑n + (ω ^ e'.repr * ↑↑n' + a'.repr)

Tactic:
simp only [he, Ordering.compares_gt, Ordering.compares_lt,
        Ordering.compares_eq, repr, gt_iff_lt, PNat.add_coe, Nat.cast_add] at ee ⊢

Goal state after:
case oadd.eq
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
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this✝ : e.NF
this : e'.NF
he : e.cmp e' = Ordering.eq
ee : e = e'
⊢ ω ^ e.repr * (↑↑n + ↑↑n') + a'.repr = ω ^ e.repr * ↑↑n + (ω ^ e'.repr * ↑↑n' + a'.repr)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.gt
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
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this✝ : e.NF
this : e'.NF
ee : (e.cmp e').Compares e e'
he : e.cmp e' = Ordering.gt
⊢ (match Ordering.gt with
      | Ordering.lt => e'.oadd n' a'
      | Ordering.eq => e.oadd (n + n') a'
      | Ordering.gt => e.oadd n (e'.oadd n' a')).repr =
    ω ^ e.repr * ↑↑n + (ω ^ e'.repr * ↑↑n' + a'.repr)

Tactic:
simp only [he, Ordering.compares_gt, Ordering.compares_lt,
        Ordering.compares_eq, repr, gt_iff_lt, PNat.add_coe, Nat.cast_add] at ee ⊢

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

Goal state before:
pp: x : ZFSet.{u_1}
⊢ ∀ ⦃a₂ b₁ b₂ : ZFSet.{u_1}⦄, x.pair b₁ = a₂.pair b₂ → x = a₂ ∧ b₁ = b₂

Tactic:
x'

Goal state after:
x x' : ZFSet.{u_1}
⊢ ∀ ⦃b₁ b₂ : ZFSet.{u_1}⦄, x.pair b₁ = x'.pair b₂ → x = x' ∧ b₁ = b₂
Module: Mathlib.SetTheory.ZFC.Basic

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

Tactic:
(Tactic.simpa
 "simpa"
 []
 []
 (Tactic.simpaArgsRest
  (Tactic.optConfig [])
  []
  []
  [(Tactic.simpArgs "[" [(Tactic.simpLemma [] [] `eq_comm)] "]")]
  ["using"
   (Term.app
    `H
    [(choice
      («term{_}» "{" [`y "," `y'] "}")
      (Term.structInst
       "{"
       []
       (Term.structInstFields
        [(Term.structInstField (Term.structInstLVal `y []) [])
         ","
         (Term.structInstField (Term.structInstLVal `y' []) [])])
       (Term.optEllipsis [])
       []
       "}"))])]))

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

Goal state before:
pp: x y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : y = x → y = y'
hx : y = x ∨ True ↔ y = x ∨ {x, y} = {x, y'}
⊢ x = x ∧ y = y'

Tactic:
or_true,

Goal state after:
x y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : y = x → y = y'
hx : True ↔ y = x ∨ {x, y} = {x, y'}
⊢ x = x ∧ y = y'
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: a x : Ordinal.{u}
⊢ x.invVeblen₂ < a ↔ ω ^ x < veblen x.invVeblen₁ a

Tactic:
rw [← veblen_lt_veblen_iff_right (o := x.invVeblen₁), veblen_invVeblen₁_invVeblen₂]

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

Goal state before:
pp: a x : Ordinal.{u}
⊢ a < x.invVeblen₂ ↔ veblen x.invVeblen₁ a < ω ^ x

Tactic:
rw [← veblen_lt_veblen_iff_right (o := x.invVeblen₁), veblen_invVeblen₁_invVeblen₂]

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

Goal state before:
pp: case refine_1.inl
a x : Ordinal.{u}
h : a < veblen 0 a
⊢ veblen 0 a = ω ^ x → x.invVeblen₁ = 0 ∧ x.invVeblen₂ = a

Tactic:
rw [veblen_zero] at h
      have := invVeblen₁_of_lt_opow h
      have := invVeblen₂_of_lt_opow h
      aesop

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

Goal state before:
pp: case h
x✝ x : PSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) y
⊢ lift.{u + 1, u} x.rank = ⨆ b, succ (lift.{u + 1, u} (↑b).rank)

Tactic:
apply (le_of_forall_lt _).antisymm (Ordinal.iSup_le _) <;> intro h

Goal state after:
x✝ x : PSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) y
h : Ordinal.{u + 1}
⊢ h < lift.{u + 1, u} x.rank → h < ⨆ i, succ (lift.{u + 1, u} (↑i).rank)

x✝ x : PSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) y
h : { b // b ∈ x }
⊢ succ (lift.{u + 1, u} (↑h).rank) ≤ lift.{u + 1, u} x.rank
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: x y : Class.{u}
h : Set.Nonempty x
⊢ y ∈ ⋂₀ x ↔ ∀ z ∈ x, y ∈ z

Tactic:
refine ⟨fun hy z => mem_of_mem_sInter hy, fun H => ?_⟩

Goal state after:
x y : Class.{u}
h : Set.Nonempty x
H : ∀ z ∈ x, y ∈ z
⊢ y ∈ ⋂₀ x
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case h
x✝ x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) y
⊢ lift.{u + 1, u} x.rank = ⨆ b, succ (lift.{u + 1, u} (↑b).rank)

Tactic:
apply (le_of_forall_lt _).antisymm (Ordinal.iSup_le _) <;> intro h

Goal state after:
x✝ x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) y
h : Ordinal.{u + 1}
⊢ h < lift.{u + 1, u} x.rank → h < ⨆ i, succ (lift.{u + 1, u} (↑i).rank)

x✝ x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) y
h : ↥x
⊢ succ (lift.{u + 1, u} (↑h).rank) ≤ lift.{u + 1, u} x.rank
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: case refine_2
o : Ordinal.{u_1}
z : ZFSet.{u_1}
a : Ordinal.{u_1}
ha : a < o
hx : a.toZFSet ∈ o.toZFSet
b : Ordinal.{u_1}
hb : b < a
hz : z ∈ b.toZFSet
hy : b.toZFSet ∈ a.toZFSet
⊢ z ∈ a.toZFSet

Tactic:
· obtain ⟨c, hc, rfl⟩ := mem_toZFSet_iff.1 hz
    exact toZFSet_mem_toZFSet_iff.2 (hc.trans hb)

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

Goal state before:
pp: case neg
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 : 1 + (e - 1) = e
⊢ (e - 1).oadd n a' = o' → m' = m → e.oadd n (scale 1 a') = scale 1 o' ∧ m' = m

Tactic:
intros

Goal state after:
case neg
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 : 1 + (e - 1) = e
a✝¹ : (e - 1).oadd n a' = o'
a✝ : m' = m
⊢ e.oadd n (scale 1 a') = scale 1 o' ∧ m' = m
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case neg
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
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + ↑m'
⊢ (e - 1).oadd n a' = o' → m' = m → o'.NF ∧ ω ^ e.repr * ↑↑n + (ω * a'.repr + ↑m') = ω * o'.repr + ↑m

Tactic:
intros

Goal state after:
case neg
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
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + ↑m'
a✝¹ : (e - 1).oadd n a' = o'
a✝ : m' = m
⊢ o'.NF ∧ ω ^ e.repr * ↑↑n + (ω * a'.repr + ↑m') = ω * o'.repr + ↑m
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 ^ succ ↑k * α' = (ω0 ^ ↑k * α' + R) * α'

Tactic:
have α0 : ¬IsMin α' := by
      rw [isMin_iff_eq_bot]
      exact α0.ne'

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 * α' + R) * α'
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case seq
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h_coef : ∀ x ∈ ms.seq, x.2.Sorted
h_Pairwise : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) ms.seq
⊢ ms.seq.Sorted

Tactic:
| seq _ h_coef h_Pairwise =>

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

Goal state before:
pp: case seq
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h_coef : ∀ x ∈ (mk ms.seq 0).seq, x.2.Sorted
h_Pairwise : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk ms.seq 0).seq
⊢ ms.Sorted

Tactic:
| seq _ h_coef h_Pairwise =>

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

Goal state before:
pp: case seq
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h_coef : ∀ x ∈ (mk (Multiseries.cons exp coef tl) 0).seq, x.2.Sorted
h_Pairwise : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk (Multiseries.cons exp coef tl) 0).seq
⊢ coef.Sorted ∧ tl.leadingExp < ↑exp ∧ tl.Sorted

Tactic:
| seq _ h_coef h_Pairwise =>

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h : ms.Trimmed
⊢ ms.seq.Trimmed

Tactic:
by
    cases h <;> constructor <;> grind

Goal state after: