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

Goal state before:
pp: case pos
R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
n : ℕ
h : p ∣ n
⊢ (coeff n) ((expand p hp) φ) = (coeff (n / p)) φ

pp: case neg
R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
n : ℕ
h : ¬p ∣ n
⊢ (coeff n) ((expand p hp) φ) = 0

Tactic:
· obtain ⟨q, hq⟩ := h
    rw [hq, coeff_expand_mul, Nat.mul_div_cancel_left _ (p.pos_of_ne_zero hp)]

Goal state after:
case neg
R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
n : ℕ
h : ¬p ∣ n
⊢ (coeff n) ((expand p hp) φ) = 0
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: case inl
⊢ primeFactors 0 = Finset.map Nat.castEmbedding (Int.natAbs 0).primeFactors

pp: case inr
z : ℤ
hz : z ≠ 0
⊢ primeFactors z = Finset.map Nat.castEmbedding z.natAbs.primeFactors

Tactic:
· simp

Goal state after:
case inr
z : ℤ
hz : z ≠ 0
⊢ primeFactors z = Finset.map Nat.castEmbedding z.natAbs.primeFactors
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case eq_mul_add
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
⊢ 0 = g * 0 + ↑0

Tactic:
· simp

Goal state after:
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 : ℕ
⊢ (coeff (i + ((map (Ideal.Quotient.mk I)) g).order.toNat))
      (↑⋯.unit⁻¹ * (↑r - ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g) * q)) ∈
    I ^ (k + 1)

Tactic:
refine coeff_mul_mem_ideal_of_coeff_right_mem_ideal' (fun i ↦ ?_) _

Goal state after:
case succ
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
k : ℕ
ih : ∀ (i : ℕ), (coeff i) q ∈ I ^ k
h1 : ∀ (i : ℕ), (coeff i) ↑r ∈ I ^ (k + 1)
heq :
  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 : ℕ
⊢ (coeff i) (↑r - ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g) * q) ∈ I ^ (k + 1)
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 f' : A⟦X⟧
inst✝ : IsAdicComplete I A
⊢ H.div (f + f') = H.div f + H.div f'

Tactic:
have H1 := (H.isWeierstrassDivisionAt_div_mod f).add (H.isWeierstrassDivisionAt_div_mod f')
  have H2 := H.isWeierstrassDivisionAt_div_mod (f + f')
  exact (H.eq_of_mul_add_eq_mul_add H2.degree_lt H1.degree_lt
    (H2.eq_mul_add.symm.trans H1.eq_mul_add)).1

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
reg : IsSMulRegular (↑M) x
mem : x ∈ maximalIdeal R
sub : Subsingleton ↑M ↔ Subsingleton (QuotSMulTop x ↑M)
n✝ n : ℕ
S : ShortComplex (ModuleCat R) := ⋯
hS : S.ShortExact
h : HasProjectiveDimensionLE (of R (QuotSMulTop x ↑M)) (n + 1)
⊢ ∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L (n + 1))

Tactic:
intro L _

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
⊢ Subsingleton (Ext M L (n + 1))
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
n : ℕ
hn :
  ∀ (M : ModuleCat R) [Nontrivial ↑M] [Module.Finite R ↑M] (rs : List R),
    IsWeaklyRegular (↑M) rs →
      (∀ r ∈ rs, r ∈ maximalIdeal R) →
        rs.length = n → projectiveDimension (of R (↑M ⧸ Ideal.ofList rs • ⊤)) = projectiveDimension M + ↑n
M : ModuleCat R
inst✝¹ : Nontrivial ↑M
inst✝ : Module.Finite R ↑M
rs : List R
x : R
rs' : List R
mem : x ∈ maximalIdeal R ∧ ∀ a ∈ rs', a ∈ maximalIdeal R
reg : IsSMulRegular (↑M) x ∧ IsWeaklyRegular (QuotSMulTop x ↑M) rs'
this : Nontrivial (QuotSMulTop x ↑M)
len : rs'.length = n
⊢ projectiveDimension (of R (↑M ⧸ Ideal.ofList (x :: rs') • ⊤)) = projectiveDimension M + ↑(n + 1)

Tactic:
Nat.cast_add,

Goal state after:
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : Small.{v, u} R
inst✝³ : IsLocalRing R
inst✝² : IsNoetherianRing R
n : ℕ
hn :
  ∀ (M : ModuleCat R) [Nontrivial ↑M] [Module.Finite R ↑M] (rs : List R),
    IsWeaklyRegular (↑M) rs →
      (∀ r ∈ rs, r ∈ maximalIdeal R) →
        rs.length = n → projectiveDimension (of R (↑M ⧸ Ideal.ofList rs • ⊤)) = projectiveDimension M + ↑n
M : ModuleCat R
inst✝¹ : Nontrivial ↑M
inst✝ : Module.Finite R ↑M
rs : List R
x : R
rs' : List R
mem : x ∈ maximalIdeal R ∧ ∀ a ∈ rs', a ∈ maximalIdeal R
reg : IsSMulRegular (↑M) x ∧ IsWeaklyRegular (QuotSMulTop x ↑M) rs'
this : Nontrivial (QuotSMulTop x ↑M)
len : rs'.length = n
⊢ projectiveDimension (of R (↑M ⧸ Ideal.ofList (x :: rs') • ⊤)) = projectiveDimension M + (↑n + ↑1)
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
rs : List R
reg : RingTheory.Sequence.IsRegular R rs
⊢ projectiveDimension (of R (Shrink.{v, u} (R ⧸ Ideal.ofList rs))) = ↑rs.length

Tactic:
have mem_max : ∀ x ∈ rs, x ∈ maximalIdeal R := by
    intro x hx
    apply IsLocalRing.le_maximalIdeal reg.2.symm
    simpa using (Ideal.mem_span x).mpr fun p a ↦ a hx

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
rs : List R
reg : RingTheory.Sequence.IsRegular R rs
mem_max : ∀ x ∈ rs, x ∈ maximalIdeal R
⊢ projectiveDimension (of R (Shrink.{v, u} (R ⧸ Ideal.ofList rs))) = ↑rs.length
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).weierstrassDistinguished hg = g.weierstrassDistinguished ⋯

Tactic:
have H := g.isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit
    (fun h ↦ hg (by simp [Algebra.smul_def, h]))

Goal state after:
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
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
⊢ (a • g).weierstrassDistinguished hg = g.weierstrassDistinguished ⋯
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]))

Goal state after:
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
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
⊢ (a • g).weierstrassUnit hg = a • g.weierstrassUnit ⋯
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: case inl
R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
this : Subsingleton (ValueGroupWithZero R)ˣ
⊢ 0 < 1 → 0 ≤ 0

pp: case inr
R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
this : Subsingleton (ValueGroupWithZero R)ˣ
u : (ValueGroupWithZero R)ˣ
⊢ ↑u < 1 → ↑u ≤ 0

Tactic:
· simp

Goal state after:
case inr
R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
this : Subsingleton (ValueGroupWithZero R)ˣ
u : (ValueGroupWithZero R)ˣ
⊢ ↑u < 1 → ↑u ≤ 0
Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing

Goal state before:
pp: case succ
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hA : A.coeff 0 = ↑a
n : ℕ
a✝ : (A * { coeff := inverseCoeff a A }).coeff n = coeff 1 n
⊢ (A * { coeff := inverseCoeff a A }).coeff (n + 1) = coeff 1 (n + 1)

Tactic:
| succ n =>

Goal state after:
case succ
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hA : A.coeff 0 = ↑a
n : ℕ
a✝ : (A * { coeff := inverseCoeff a A }).coeff n = coeff 1 n
⊢ (A * { coeff := inverseCoeff a A }).coeff (n + 1) = coeff 1 (n + 1)
Module: Mathlib.RingTheory.WittVector.Compare

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
⊢ ((zmodEquivTrunc p m).symm.toRingHom.comp (TruncatedWittVector.truncate h)).comp (truncate n) =
    (zmodEquivTrunc p m).symm.toRingHom.comp (truncate m)

Tactic:
by
      rw [RingHom.comp_assoc, truncate_comp_wittVector_truncate]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : b.coeff 0 ^ p ^ m ≠ 0
hcm : a = (⇑verschiebung)^[m] ((⇑frobenius)^[m] b)
this : (⇑verschiebung ∘ ⇑frobenius)^[m] b = ((⇑verschiebung)^[m] ∘ (⇑frobenius)^[m]) b
⊢ ∃ m b, b.coeff 0 ≠ 0 ∧ a = ↑p ^ m * b

Tactic:
simp only [Function.comp_apply] at this

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : b.coeff 0 ^ p ^ m ≠ 0
hcm : a = (⇑verschiebung)^[m] ((⇑frobenius)^[m] b)
this : (⇑verschiebung ∘ ⇑frobenius)^[m] b = (⇑verschiebung)^[m] ((⇑frobenius)^[m] b)
⊢ ∃ m b, b.coeff 0 ≠ 0 ∧ a = ↑p ^ m * b
Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing

Goal state before:
pp: case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : b.coeff 0 ^ p ^ m ≠ 0
hcm : a = (⇑verschiebung ∘ ⇑frobenius)^[m] b
this : (⇑verschiebung ∘ ⇑frobenius)^[m] b = (⇑verschiebung)^[m] ((⇑frobenius)^[m] b)
⊢ a = ↑p ^ m * b

Tactic:
· simp_rw [← mul_left_iterate (p : 𝕎 k) m]
    convert! hcm using 2
    ext1 x
    rw [mul_comm, ← WittVector.verschiebung_frobenius x]; rfl

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
⊢ (X ^ p).degree + 0 = ↑p

pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
⊢ a₁.coeff 0 ^ p ^ (n + 1) ≠ 0

Tactic:
· simp

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
⊢ a₁.coeff 0 ^ p ^ (n + 1) ≠ 0
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| (∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
      ↑p ^ (n + 1) * X (0, n + 1)) *
    ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))

Tactic:
arg 2

Goal state after:
p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (polyOfInterest p n).vars =
    (↑p ^ (n + 1) *
        (wittMul p (n + 1) + ↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1) -
            X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) -
          X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)))).vars

Tactic:
have : (p : 𝕄) ^ (n + 1) = C ((p : ℤ) ^ (n + 1)) := by norm_cast

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
this : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
⊢ (polyOfInterest p n).vars =
    (↑p ^ (n + 1) *
        (wittMul p (n + 1) + ↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1) -
            X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) -
          X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)))).vars
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
s : Set (Set α)
inst✝ : OrderTop α
hs : ∀ x ∈ s, IsClub x
⊢ ⊤ ∈ ⋂₀ s

Tactic:
mem_sInter

Goal state after:
α : Type v
inst✝¹ : LinearOrder α
s : Set (Set α)
inst✝ : OrderTop α
hs : ∀ x ∈ s, IsClub x
⊢ ∀ t ∈ s, ⊤ ∈ t
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: case inl
α : Type v
inst✝ : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
hs : ∀ x ∈ s, IsClub x
h✝ : IsEmpty α
⊢ IsClub (⋂₀ s)

pp: case inr
α : Type v
inst✝ : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
⊢ IsClub (⋂₀ s)

Tactic:
· simp

Goal state after:
case inr
α : Type v
inst✝ : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
⊢ IsClub (⋂₀ s)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: case inl
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : IsEmpty α
⊢ IsClub (⋂₀ s)

pp: case inr
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
⊢ IsClub (⋂₀ s)

Tactic:
· simp

Goal state after:
case inr
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
⊢ IsClub (⋂₀ s)
Module: Mathlib.SetTheory.Cardinal.EventuallyConst

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
hf : Monotone f
this✝ : Nonempty α
hα : IsCofinal (range (rangeSplitting f))
this : LinearOrder ↑(range f) := ⋯.linearOrder
⊢ lift.{u, v} (cof ↑(range f)) ≤ lift.{u, v} #β

Tactic:
lift_le

Goal state after:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
hf : Monotone f
this✝ : Nonempty α
hα : IsCofinal (range (rangeSplitting f))
this : LinearOrder ↑(range f) := ⋯.linearOrder
⊢ cof ↑(range f) ≤ #β
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: case inl
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h✝ : IsEmpty α
⊢ IsClub (Function.fixedPoints f)

pp: case inr
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h✝ : Nonempty α
⊢ IsClub (Function.fixedPoints f)

Tactic:
· simp

Goal state after:
case inr
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h✝ : Nonempty α
⊢ IsClub (Function.fixedPoints f)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝ : LinearOrder α
ι : Sort u_1
f : ι → Set α
hα : cof α ≤ 1
⊢ IsStationary (⋃ i, f i) ↔ ∃ i, IsStationary (f i)

Tactic:
rw [← sUnion_range, isStationary_sUnion_iff_of_cof_le_one hα]

Goal state after:
α : Type v
inst✝ : LinearOrder α
ι : Sort u_1
f : ι → Set α
hα : cof α ≤ 1
⊢ (∃ x ∈ range f, IsStationary x) ↔ ∃ i, IsStationary (f i)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
ι : Type u
f : ι → Set α
hα : cof α ≠ ℵ₀
hι : lift.{v, u} #ι < lift.{u, v} (cof α)
⊢ (∃ x ∈ range f, IsStationary x) ↔ ∃ i, IsStationary (f i)

pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
ι : Type u
f : ι → Set α
hα : cof α ≠ ℵ₀
hι : lift.{v, u} #ι < lift.{u, v} (cof α)
⊢ #↑(range f) < cof α

Tactic:
· simp

Goal state after:
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
ι : Type u
f : ι → Set α
hα : cof α ≠ ℵ₀
hι : lift.{v, u} #ι < lift.{u, v} (cof α)
⊢ #↑(range f) < cof α
Module: Mathlib.SetTheory.Ordinal.Commute

Goal state before:
pp: o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih : ∀ y < o₁ + o₂, ∀ {o₁ o₂ : Ordinal.{u_1}}, AddCommute o₁ o₂ → o₁ + o₂ = y → ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂
hle : o₁ ≤ o₂
h₁ : o₁ ≠ 0
o₃ : Ordinal.{u_1} := o₂ - o₁
hsub : o₁ + o₃ = o₂
⊢ o₁ + (o₁ + o₃) = o₁ + (o₃ + o₁)

Tactic:
by grind

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

Goal state before:
pp: case right
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih : ∀ y < o₁ + o₂, ∀ {o₁ o₂ : Ordinal.{u_1}}, AddCommute o₁ o₂ → o₁ + o₂ = y → ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂
hle : o₁ ≤ o₂
h₁ : o₁ ≠ 0
o₃ : Ordinal.{u_1} := ⋯
hsub : o₁ + o₃ = o₂
hcomm' : AddCommute o₁ o₃
hlt : o₁ + o₃ < o₁ + o₂
o : Ordinal.{u_1}
n₁ n₃ : ℕ
hn₁ : o * ↑n₁ = o₁
hn₃ : o * ↑n₃ = o₃
⊢ o * ↑(n₁ + n₃) = o₂

Tactic:
Nat.cast_add,

Goal state after:
case right
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih : ∀ y < o₁ + o₂, ∀ {o₁ o₂ : Ordinal.{u_1}}, AddCommute o₁ o₂ → o₁ + o₂ = y → ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂
hle : o₁ ≤ o₂
h₁ : o₁ ≠ 0
o₃ : Ordinal.{u_1} := o₂ - o₁
hsub : o₁ + o₃ = o₂
hcomm' : AddCommute o₁ o₃
hlt : o₁ + o₃ < o₁ + o₂
o : Ordinal.{u_1}
n₁ n₃ : ℕ
hn₁ : o * ↑n₁ = o₁
hn₃ : o * ↑n₃ = o₃
⊢ o * (↑n₁ + ↑n₃) = o₂
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
g : Ordinal.{u} → α
h_inj : InjOn g (Iio (succ #α).ord)
h : lift.{u + 1, u} (succ #α) ≤ lift.{u + 1, u} #α
mk_initialSeg_subtype : #↑(Iio (succ #α).ord) = lift.{u + 1, u} (succ #α)
⊢ False

Tactic:
lift_le

Goal state after:
α : Type u
g : Ordinal.{u} → α
h_inj : InjOn g (Iio (succ #α).ord)
h : succ #α ≤ #α
mk_initialSeg_subtype : #↑(Iio (succ #α).ord) = lift.{u + 1, u} (succ #α)
⊢ False
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 (CNF b 0) = 0

Tactic:
zero_right,

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

Goal state before:
pp: case refine_1
b o : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b 0 → x.1 ≤ log b 0

pp: case refine_2
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)
⊢ x ∈ CNF b o → x.1 ≤ log b o

Tactic:
· simp

Goal state after:
case refine_2
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)
⊢ x ∈ CNF b o → x.1 ≤ log b o
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case refine_1
b o : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b 0 → x.2 < b

pp: case refine_2
b o✝ : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.2 < b
⊢ x ∈ CNF b o → x.2 < b

Tactic:
· simp

Goal state after:
case refine_2
b o✝ : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.2 < b
⊢ x ∈ CNF b o → x.2 < b
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case inl
b : Ordinal.{u_1}
hb : b ≤ 1
a : Ordinal.{u_1}
⊢ (coeff b 0) a = (single 0 0) a

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

Tactic:
· simp

Goal state after:
case inr
b : Ordinal.{u_1}
hb : b ≤ 1
o a : Ordinal.{u_1}
ho : o ≠ 0
⊢ (coeff b o) a = (single 0 o) a
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
o : Ordinal.{u} := ⋯
hfix : lfpApprox f x o ∈ fixedPoints ⇑f
⊢ lfpApprox f x o ≤ ↑(f.nextFixed x hx)

Tactic:
exact lfpApprox_le_of_mem_fixedPoints f (f.nextFixed x hx).2 (f.le_nextFixed hx) o

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

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

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
⊢ eval b (single e x + f) = b ^ e * x + eval b f

Tactic:
· simp

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
⊢ eval b (single e x + f) = b ^ e * x + eval b f
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e o₁ o₂ : ONote
n₁ n₂ : ℕ+
h₁ : (e.oadd n₁ o₁).NF
h : ↑n₁ < ↑n₂
⊢ e.oadd n₁ o₁ < e.oadd n₂ o₂

Tactic:
by
  simp only [lt_def, repr]
  grw [h₁.snd'.repr_lt, ← le_self_add]
  rwa [← mul_succ, mul_le_mul_iff_right₀ (opow_pos _ omega0_pos), succ_le_iff, Nat.cast_lt]

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

Goal state before:
pp: b o : Ordinal.{u_1}
⊢ foldr (fun x y ↦ b ^ x.1 * (coeff b o) x.1 + y) 0 (CNF b o) = foldr (fun p r ↦ b ^ p.1 * p.2 + r) 0 (CNF b o)

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

pp: b o : Ordinal.{u_1}
⊢ (map Prod.fst (CNF b o)).Nodup

Tactic:
· apply foldr_ext
    intro a ha x
    rw [coeff_of_mem_CNF ha]

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

b o : Ordinal.{u_1}
⊢ (map Prod.fst (CNF b o)).Nodup
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case inl
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
hf : IsNormal f
⊢ veblenWith f 0 a ∈ range f

pp: case inr
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
h : 0 < o
⊢ veblenWith f o a ∈ range f

Tactic:
· simp

Goal state after:
case inr
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
h : 0 < o
⊢ veblenWith f o a ∈ range f
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case inr
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
h : 0 < o
⊢ veblenWith f o a ∈ range f

Tactic:
← veblenWith_veblenWith_of_lt hf h

Goal state after:
case inr
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
h : 0 < o
⊢ veblenWith f 0 (veblenWith f o a) ∈ range f
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₂ a

Tactic:
← veblenWith_veblenWith_of_lt hf h

Goal state after:
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)