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

Goal state before:
pp: case succ
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
d : ℕ
hd :
  (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) =
    eval (↑n)
      (match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i)
⊢ (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F (d + 1))) =
    eval (↑n)
      (match d + 1 with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i)

Tactic:
| succ d hd =>

Goal state after:
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: ⊢ primeFactors = Nat.primeFactors

Tactic:
ext n : 1

Goal state after:
n : ℕ
⊢ primeFactors n = n.primeFactors
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
M : Type u_1
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommMonoid N
inst✝² : Module R N
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
f : M →ₚₗ[R] N
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S ⟨s, p⟩ = t
⊢ toFun S f t = (rTensor N (φ R s).toLinearMap) (f.toFun' (MvPolynomial (Fin s.card) R) p)

Tactic:
PolynomialLaw.toFun,

Goal state after:
R : Type u
inst✝⁶ : CommSemiring R
M : Type u_1
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommMonoid N
inst✝² : Module R N
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
f : M →ₚₗ[R] N
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S ⟨s, p⟩ = t
⊢ Function.extend (π R M S) (toFunLifted S f) (fun x ↦ 0) t =
    (rTensor N (φ R s).toLinearMap) (f.toFun' (MvPolynomial (Fin s.card) R) p)
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
f : A⟦X⟧
k i : ℕ
hi : i ≥ ((map (Ideal.Quotient.mk I)) g).order.toNat
⊢ (coeff i) (f - g * H.seq f k) ∈ I ^ k

Tactic:
by
  induction k generalizing hi i with
  | zero => simp
  | succ k hq =>
    rw [seq]
    set q := H.seq f k
    set s := f - g * q
    set n := (g.map (Ideal.Quotient.mk I)).order.toNat
    have hs := s.eq_X_pow_mul_shift_add_trunc n
    set s₀ := s.trunc n
    set s₁ := PowerSeries.mk fun i ↦ coeff (i + n) s
    set q' := q + s₁ * H.isUnit_shift.unit⁻¹
    have key : f - g * q' = (s₀ : A⟦X⟧) - (g.trunc n : A⟦X⟧) * s₁ * H.isUnit_shift.unit⁻¹ := by
      trans s + g * (q - q')
      · simp_rw [s]; ring
      simp_rw [q']
      rw [sub_add_cancel_left, mul_neg, ← mul_assoc, mul_right_comm]
      nth_rw 1 [g.eq_X_pow_mul_shift_add_trunc n]
      rw [add_mul, mul_assoc, IsUnit.mul_val_inv, hs]
      ring
    rw [key, map_sub, Polynomial.coeff_coe, coeff_trunc, if_neg hi.not_gt, zero_sub, neg_mem_iff,
      pow_succ']
    refine coeff_mul_mem_ideal_of_coeff_left_mem_ideal' (fun i ↦ ?_) i
    refine coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal'
      (by simp [n, g.coeff_trunc_order_mem]) (fun i ↦ ?_) i
    rw [coeff_mk]
    exact hq (by simp)

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
R' : Type u_2
inst✝ : CommRing R'
e : R ≃+* R'
this✝ : IsLocalRing R'
this : IsNoetherianRing R'
⊢ ↑(Submodule.spanFinrank (maximalIdeal R')) = ringKrullDim R'

Tactic:
← ringKrullDim_eq_of_ringEquiv e,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
R' : Type u_2
inst✝ : CommRing R'
e : R ≃+* R'
this✝ : IsLocalRing R'
this : IsNoetherianRing R'
⊢ ↑(Submodule.spanFinrank (maximalIdeal R')) = ringKrullDim R
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
⊢ (coeff i)
      (((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) ∈
    I * I ^ k

Tactic:
refine coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal i (fun j hj ↦ ?_)
          (fun j _ ↦ ih j) i le_rfl

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) +
        ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g)) ∈
    I
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⟧
⊢ ∃ a, a * g = f - ↑(H.mod f)

Tactic:
use H.div f

Goal state after:
case h
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsAdicComplete I A
f : A⟦X⟧
⊢ H.div f * g = f - ↑(H.mod f)
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
e : (p : Submodule R ↥N) → ↥p ≃ₗ[R] ↥(Submodule.map N.subtype p)
⊢ 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)

Tactic:
Submodule.MapSubtype.orderIso,

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
e : (p : Submodule R ↥N) → ↥p ≃ₗ[R] ↥(Submodule.map N.subtype p)
⊢ IsIsotypicOfType R (↥N) S ↔
    ∀ (a : Submodule R ↥N)
      [IsSimpleModule R
          ↥↑({ toFun := fun p' ↦ ⟨Submodule.map N.subtype p', ⋯⟩, invFun := fun q ↦ Submodule.comap N.subtype ↑q,
                  left_inv := ⋯, right_inv := ⋯ }
                a)],
      Nonempty
        (↥↑({ toFun := fun p' ↦ ⟨Submodule.map N.subtype p', ⋯⟩, invFun := fun q ↦ Submodule.comap N.subtype ↑q,
                  left_inv := ⋯, right_inv := ⋯ }
                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
e : (p : Submodule R ↥N) → ↥p ≃ₗ[R] ↥(Submodule.map N.subtype p)
⊢ IsIsotypic R ↥N ↔
    ∀ (a : Submodule R ↥N) [IsSimpleModule R ↥↑((Submodule.MapSubtype.orderIso N).toEquiv a)],
      IsIsotypicOfType R ↥N ↥↑((Submodule.MapSubtype.orderIso N).toEquiv a)

Tactic:
Submodule.MapSubtype.orderIso,

Goal state after:
R : Type u_2
M : Type u
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
e : (p : Submodule R ↥N) → ↥p ≃ₗ[R] ↥(Submodule.map N.subtype p)
⊢ IsIsotypic R ↥N ↔
    ∀ (a : Submodule R ↥N)
      [IsSimpleModule R
          ↥↑({ toFun := fun p' ↦ ⟨Submodule.map N.subtype p', ⋯⟩, invFun := fun q ↦ Submodule.comap N.subtype ↑q,
                  left_inv := ⋯, right_inv := ⋯ }
                a)],
      IsIsotypicOfType R ↥N
        ↥↑({ toFun := fun p' ↦ ⟨Submodule.map N.subtype p', ⋯⟩, invFun := fun q ↦ Submodule.comap N.subtype ↑q,
                left_inv := ⋯, right_inv := ⋯ }
              a)
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
w✝ : Submodule R M
left✝ : IsSimpleModule R ↥w✝
⊢ IsIsotypic R ↥(isotypicComponent R M ↥w✝)

Tactic:
exact .isotypicComponent R M _

Goal state after:
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
w✝ : Submodule R M
left✝ : IsSimpleModule R ↥w✝
⊢ (isotypicComponent R M ↥w✝).IsFullyInvariant

Tactic:
exact .isotypicComponent R M _

Goal state after:
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
inst✝¹ : IsSimpleModule R S
inst✝ : IsSemisimpleModule R M
⊢ ⊤ ≤ isotypicComponent R M S ↔ IsIsotypicOfType R M S

Tactic:
le_isotypicComponent_iff,

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
inst✝¹ : IsSimpleModule R S
inst✝ : IsSemisimpleModule R M
⊢ IsIsotypicOfType R (↥⊤) S ↔ IsIsotypicOfType R M S
Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
i : ℕ
hi : f.coeff i ∉ x.asIdeal
⊢ f ∉ ↑{ asIdeal := Ideal.map C x.asIdeal, isPrime := ⋯ }.asIdeal

Tactic:
exact fun a => hi (mem_map_C_iff.mp a i)

Goal state after:
Module: Mathlib.RingTheory.WittVector.Compare

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((PadicInt.toZModPow n).comp (toPadicInt p)).comp (fromPadicInt p) = (PadicInt.toZModPow n).comp (RingHom.id ℤ_[p])

Tactic:
toPadicInt,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((PadicInt.toZModPow n).comp (PadicInt.lift ⋯)).comp (fromPadicInt p) = (PadicInt.toZModPow n).comp (RingHom.id ℤ_[p])
Module: Mathlib.RingTheory.WittVector.Isocrystal

Goal state before:
pp: case refine_1
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
⊢ F₀.ker = ⊥

Tactic:
exact LinearMap.ker_toSpanSingleton K(p, k) hx

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

Goal state before:
pp: case refine_2.inr
b o✝ : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
H : x ∈ CNF b (o % b ^ log b o) → x.1 ≤ log b (o % b ^ log b o)
h : x ∈ CNF b (o % b ^ log b o)
⊢ x.1 ≤ log b o

Tactic:
exact (H h).trans (log_mono_right _ (mod_opow_log_lt_self b ho).le)

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:
induction i using WellFoundedLT.induction with | ind i IH

Goal state after:
case ind
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x a : α
ha : a ∈ fixedPoints ⇑f
hxa : x ≤ a
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x y ≤ a
⊢ lfpApprox f x i ≤ a
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

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

Tactic:
rw [single_eq_of_ne ha]

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : IsNormal f
b : β
a : α
ha : f ⁻¹' Iic b = Iio a
⊢ IsClosed (f ⁻¹' Iic b)

Tactic:
obtain h | h := (f ⁻¹' Iic b).eq_empty_or_nonempty
    · exact h ▸ isClosed_empty
    · have : Nonempty α := ⟨a⟩
      have : Nonempty β := ⟨b⟩
      rw [hf.preimage_Iic h (ha ▸ bddAbove_Iio)]
      exact isClosed_Iic

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

Goal state before:
pp: e : ONote
n : ℕ+
a : ONote
⊢ ω ^ e.repr ≤ (e.oadd n a).repr

Tactic:
refine le_trans ?_ le_self_add
  simpa using! (mul_le_mul_iff_right₀ <| opow_pos (repr e) omega0_pos).2 (Nat.cast_le.2 n.2)

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

Goal state before:
pp: a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
tfae_2_to_3 : a ∈ closure (s ∩ Iic a) → (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a
tfae_3_to_4 : (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a → ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a
tfae_4_to_5 :
  (∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a) → ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a
⊢ (∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a) → a ∈ closure s

Tactic:
rintro ⟨ι, hne, f, hfs, rfl⟩

Goal state after:
s : Set Ordinal.{u}
ι : Type u
hne : Nonempty ι
f : ι → Ordinal.{u}
hfs : ∀ (i : ι), f i ∈ s
tfae_1_to_2 : ⨆ i, f i ∈ closure s → ⨆ i, f i ∈ closure (s ∩ Iic (⨆ i, f i))
tfae_2_to_3 :
  ⨆ i, f i ∈ closure (s ∩ Iic (⨆ i, f i)) → (s ∩ Iic (⨆ i, f i)).Nonempty ∧ sSup (s ∩ Iic (⨆ i, f i)) = ⨆ i, f i
tfae_3_to_4 :
  (s ∩ Iic (⨆ i, f i)).Nonempty ∧ sSup (s ∩ Iic (⨆ i, f i)) = ⨆ i, f i →
    ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = ⨆ i, f i
tfae_4_to_5 :
  (∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = ⨆ i, f i) →
    ∃ ι_1, Nonempty ι_1 ∧ ∃ f_1, (∀ (i : ι_1), f_1 i ∈ s) ∧ ⨆ i, f_1 i = ⨆ i, f i
⊢ ⨆ i, f i ∈ closure s
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case lt
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
nh : cmpUsing (fun x1 x2 ↦ x1 < x2) ↑n₁ ↑n₂ = Ordering.lt
⊢ (Ordering.eq.then (Ordering.lt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)

Tactic:
cmpUsing,

Goal state after:
case lt
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
nh : (if ↑n₁ < ↑n₂ then Ordering.lt else if ↑n₂ < ↑n₁ then Ordering.gt else Ordering.eq) = Ordering.lt
⊢ (Ordering.eq.then (Ordering.lt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case eq
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
nh : cmpUsing (fun x1 x2 ↦ x1 < x2) ↑n₁ ↑n₂ = 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:
cmpUsing,

Goal state after:
case eq
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
nh : (if ↑n₁ < ↑n₂ then Ordering.lt else if ↑n₂ < ↑n₁ then Ordering.gt else 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.Ordinal.Notation

Goal state before:
pp: case gt
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
nh : cmpUsing (fun x1 x2 ↦ x1 < x2) ↑n₁ ↑n₂ = Ordering.gt
⊢ (Ordering.eq.then (Ordering.gt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)

Tactic:
cmpUsing,

Goal state after:
case gt
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
nh : (if ↑n₁ < ↑n₂ then Ordering.lt else if ↑n₂ < ↑n₁ then Ordering.gt else Ordering.eq) = Ordering.gt
⊢ (Ordering.eq.then (Ordering.gt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
⊢ AccPt p (𝓟 S) ↔ AccPt ⟨p, hpo⟩ (comap Subtype.val (𝓟 S))

Tactic:
isOpen_Iio.isOpenEmbedding_subtypeVal.accPt_comap_iff

Goal state after:
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
⊢ AccPt p (𝓟 S) ↔ AccPt (↑⟨p, hpo⟩) (𝓟 S)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
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
h : e.cmp e' = Ordering.eq
this : Ordering.eq.Compares e e'
⊢ (e.oadd (n + n') a').NFBelow b

Tactic:
subst e'

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
n' : ℕ+
a' : ONote
h' : (e.oadd n' a').NFBelow b
h : e.cmp e = Ordering.eq
⊢ (e.oadd (n + n') a').NFBelow b
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a o₁ o₂ : Ordinal.{u}
h : o₁ < o₂
⊢ veblenWith f o₁ a ≤ veblenWith f o₁ (veblenWith f o₂ a)

Tactic:
exact (veblenWith_right_strictMono hf o₁).monotone (right_le_veblenWith hf o₂ a)

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

Goal state before:
pp: x y : PSet.{u_1}
⊢ (insert x y).rank = max (succ x.rank) y.rank

Tactic:
by
  apply le_antisymm
  · simp_rw [rank_le_iff, mem_insert_iff]
    rintro _ (h | h)
    · simp [rank_congr h]
    · simp [rank_lt_of_mem h]
  · apply max_le
    · exact (rank_lt_of_mem (mem_insert x y)).succ_le
    · exact rank_mono (subset_iff.2 fun z => mem_insert_of_mem x)

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

Goal state before:
pp: x : PSet.{u_1}
⊢ x.powerset.rank = succ x.rank

Tactic:
by
  apply le_antisymm
  · simp_rw [rank_le_iff, mem_powerset, lt_succ_iff]
    intro
    exact rank_mono
  · rw [succ_le_iff]
    apply rank_lt_of_mem
    simp

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

Goal state before:
pp: a : Ordinal.{u}
h : a < ω ^ a
⊢ a.invVeblen₂ = a

Tactic:
rw [invVeblen₂_eq_iff, invVeblen₁_of_lt_opow h, veblen_zero_apply]

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

Goal state before:
pp: o : Ordinal.{u}
⊢ o.invVeblen₁ = o ↔ o = 0 ∨ o ∈ range Γ_

Tactic:
constructor
  · rw [mem_range_gamma, or_iff_not_imp_left]
    refine fun h ho ↦ (left_le_veblen ..).antisymm' ?_
    conv_rhs => rw [← veblen_eq_of_lt_invVeblen₁ (h.trans_ne ho).bot_lt, bot_eq_zero,
      veblen_zero_apply, ← veblen_invVeblen₁_invVeblen₂, h]
    simp
  · aesop

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

Goal state before:
pp: x : Class.{u}
y : ZFSet.{u}
⊢ (⋂₀ x) y ↔ ∀ (z : ZFSet.{u}), x z → y ∈ z

Tactic:
refine ⟨fun hxy z hxz => hxy _ ⟨z, rfl, hxz⟩, ?_⟩

Goal state after:
x : Class.{u}
y : ZFSet.{u}
⊢ (∀ (z : ZFSet.{u}), x z → y ∈ z) → (⋂₀ x) y
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x ∉ y ↔ y ⊆ x

Tactic:
refine ⟨?_, fun hxy hyx ↦ mem_irrefl _ (hxy hyx)⟩

Goal state after:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x ∉ y → y ⊆ x
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case succ
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
k m : ℕ
⊢ (match k, m + 1 with
    | x, 0 => 0
    | 0, m.succ => e.oadd m.succPNat 0
    | k.succ, m => (e + a0.mulNat k).scale a + e.opowAux a0 a k m).NF

Tactic:
cases k with
    | zero => exact NF.oadd_zero _ _
    | succ k =>
      have := nf_opowAux e a0 a k
      simp only [mulNat_eq_mul]; infer_instance

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

Goal state before:
pp: case inr
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h✝ : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this✝ : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * ↑↑n + a.repr < ω ^ succ e.repr
h : e.repr < ω
⊢ ω ^ ω ≤ ω ^ (e.repr * ω)

Tactic:
simpa using mul_le_mul_left (one_le_iff_ne_zero.2 e0) ω

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

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

Tactic:
have : (fun t ↦ f t ^ exp / f t ^ exp') =ᶠ[atTop] fun t ↦ (f t) ^ (exp - exp') :=
      (h.eventually_gt_atTop 0).mono (fun _ h ↦ by simp [← Real.rpow_sub h])

Goal state after:
f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
this : (fun t ↦ f t ^ exp / f t ^ exp') =ᶠ[atTop] fun t ↦ f t ^ (exp - exp')
⊢ Tendsto (fun x ↦ (f ^ exp) x / (f ^ exp') x) atTop (𝓝 0)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.succ
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + ↑m
this✝ : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + ↑m < ω ^ a0.repr
aa : (a' + ↑m).repr = a'.repr + ↑m
b' : ONote
left✝ : b'.NF
k : ℕ
e₂ : o₂.split' = (b', k + 1)
r₂ : o₂.repr = ω * b'.repr + ↑(k + 1)
⊢ (match (scale 1 b', k + 1) with
      | (b, 0) => (a0 * b).oadd 1 0
      | (b, k.succ) =>
        (a0 * b + a0.mulNat k).scale (a0.oadd n a') + (a0 * b).opowAux a0 ((a0.oadd n a').mulNat m) k m).repr =
    (ω ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ o₂.repr

Tactic:
simp [r₂, opow_add, opow_mul, mul_assoc, add_assoc, repr_one]
      rw [repr_opow_aux₁ a00 al aa, scale_opowAux]
      simp only [repr_mul, repr_scale, repr_one,
        Nat.cast_one, opow_one, opow_mul]
      rw [← mul_add, ← add_assoc ((ω : Ordinal.{0}) ^ repr a0 * (n : ℕ))]
      congr 1
      rw [← pow_succ, ← opow_natCast, ← opow_natCast]
      exact (repr_opow_aux₂ _ ad a00 al _ _).2

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
s t : Multiseries basis_hd basis_tl
f g : ℝ → ℝ
h : (s, f) = (t, g)
⊢ s = t ∧ f = g

Tactic:
Prod.mk_inj

Goal state after:
basis_hd : ℝ → ℝ
basis_tl : Basis
s t : Multiseries basis_hd basis_tl
f g : ℝ → ℝ
h : s = t ∧ f = g
⊢ s = t ∧ f = g
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

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

Tactic:
simp only [toFun]

Goal state after:
basis : Basis
t1 t2 : Monomial
h_basis : WellFormedBasis basis
h1 : List.length t1.unit = List.length basis
h2 : List.length t2.unit = List.length basis
h_coef2 : t2.coef ≠ 0
h_lt : t1.unit < t2.unit
⊢ (t1.coef • t1.unit.toFun basis) =o[atTop] (t2.coef • t2.unit.toFun basis)