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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
⊢ ((expand p hp) φ).order = p • φ.order

Tactic:
by
  by_cases! hφ : φ = 0
  · simpa [hφ] using (ENat.mul_top (by norm_cast)).symm
  · apply eq_of_le_of_ge
    · obtain ⟨d, hd₁, hd₂⟩ := exists_coeff_ne_zero_and_order (ne_zero_iff_order_finite.mp hφ)
      have : p • φ.order = (p • d).degree := by simp [← hd₂]
      rw [this]
      exact order_le <| (coeff_expand_smul p hp φ _) ▸ hd₁
    · refine MvPowerSeries.le_order fun d hd => ?_
      by_cases! h : ∀ i, p ∣ d i
      · obtain ⟨m, hm⟩ : ∃ m, p • m = d := ⟨d.mapRange (fun a ↦ a / p) (by simp),
          by ext i; simp [(Nat.mul_div_cancel' (h i))]⟩
        rw [← hm, coeff_expand_smul, coeff_of_lt_order]
        simp only [← hm, map_nsmul, smul_eq_mul, Nat.cast_mul, nsmul_eq_mul] at hd
        exact lt_of_mul_lt_mul_left' hd
      · obtain ⟨i, hi⟩ := h
        exact coeff_expand_of_not_dvd p hp φ hi

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: case h
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : ExpChar R p
f : MvPowerSeries σ R
n : σ →₀ ℕ
this :
  ↑((MvPolynomial.map (frobenius R p)) ((MvPolynomial.expand p) ((trunc' R (p • n)) f))) =
    (map (frobenius R p)) ↑((MvPolynomial.expand p) ((trunc' R (p • n)) f))
⊢ (MvPolynomial.map (frobenius R p)) ((MvPolynomial.expand p) ((trunc' R n) f)) =
    (MvPolynomial.map (frobenius R p)) ((trunc' R (p • n)) ↑((MvPolynomial.expand p) ((trunc' R (p • n)) f)))

Tactic:
trunc'_expand_trunc' p hp (le_self_nsmul zero_le hp)

Goal state after:
case h
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : ExpChar R p
f : MvPowerSeries σ R
n : σ →₀ ℕ
this :
  ↑((MvPolynomial.map (frobenius R p)) ((MvPolynomial.expand p) ((trunc' R (p • n)) f))) =
    (map (frobenius R p)) ↑((MvPolynomial.expand p) ((trunc' R (p • n)) f))
⊢ (MvPolynomial.map (frobenius R p)) ((trunc' R (p • n)) ↑((MvPolynomial.expand p) ((trunc' R (p • n)) f))) =
    (MvPolynomial.map (frobenius R p)) ((trunc' R (p • n)) ↑((MvPolynomial.expand p) ((trunc' R (p • n)) f)))
Module: Mathlib.RingTheory.Noetherian.Filter

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : ℕ →o Submodule R M
⊢ ∃ i, ∀ (j : ℕ), i ≤ j → f i = f j

Tactic:
exact (monotone_stabilizes_iff_noetherian.mpr inferInstance) f

Goal state after:
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case refine_1
K : Type u_2
inst✝ : Field K
x : RatFuncAdicCompl K
x✝ : x ∈ Subring.map (LaurentSeriesRingEquiv K).toRingHom (powerSeries_as_subring K)
f : K⸨X⸩
F : K⟦X⟧
left✝ : F ∈ ⊤.carrier
coe_F : (ofPowerSeries ℤ K) F = f
hF : (LaurentSeriesRingEquiv K).toRingHom f = x
⊢ x ∈ (adicCompletionIntegers K⟮X⟯ (idealX K)).toSubring

pp: case refine_2
K : Type u_2
inst✝ : Field K
x : RatFuncAdicCompl K
H : x ∈ (adicCompletionIntegers K⟮X⟯ (idealX K)).toSubring
⊢ x ∈ Subring.map (LaurentSeriesRingEquiv K).toRingHom (powerSeries_as_subring K)

Tactic:
· simp only [ValuationSubring.mem_toSubring, ← hF, ← coe_F]
    apply mem_integers_of_powerSeries

Goal state after:
case refine_2
K : Type u_2
inst✝ : Field K
x : RatFuncAdicCompl K
H : x ∈ (adicCompletionIntegers K⟮X⟯ (idealX K)).toSubring
⊢ x ∈ Subring.map (LaurentSeriesRingEquiv K).toRingHom (powerSeries_as_subring K)
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case hnc
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
n i : ℕ
a✝ : i ∈ range (n + 1)
⊢ ¬p ^ (n - i) = 0

Tactic:
exact ne_of_gt (pow_pos hp.1.pos _)

Goal state after:
Module: Mathlib.RingTheory.Teichmuller

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : CharP (R ⧸ I) p
x : Perfection (R ⧸ I) p
m : ℕ
⊢ Quotient.out ((coeff (R ⧸ I) p (m + 1)) x) ^ p ≡ Quotient.out ((coeff (R ⧸ I) p m) x) [SMOD I]

Tactic:
simp [SModEq.idealQuotientMk, coeff_pow_p']

Goal state after:
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:

Tactic:
_ = I.map ((T f).symm.toRingEquiv.toRingHom.comp (T f)) := by
      have : (T f).symm.toRingEquiv.toRingHom.comp (T f) = RingHom.id _ :=
        RingEquiv.symm_toRingHom_comp_toRingHom _
      rw [this, Ideal.map_id]
    _ = _ := by
      rw [← Ideal.map_map, Ideal.map_coe, Ideal.map_coe]
      exact congrArg _ rfl

Goal state after:
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_2
R : Type u_3
inst✝² : Field k
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : Algebra k R
fin : Algebra.FiniteType k R
n : ℕ
f : MvPolynomial (Fin n) k →ₐ[k] R
fsurj : Function.Surjective ⇑f
ϕ : (MvPolynomial (Fin n) k ⧸ ker f) ≃ₐ[k] R := quotientKerAlgEquivOfSurjective fsurj
⊢ ∃ s g, Function.Injective ⇑g ∧ g.IsIntegral

Tactic:
obtain ⟨s, _, g, injg, intg⟩ := exists_integral_inj_algHom_of_quotient (ker f) (ker_ne_top _)

Goal state after:
k : Type u_2
R : Type u_3
inst✝² : Field k
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : Algebra k R
fin : Algebra.FiniteType k R
n : ℕ
f : MvPolynomial (Fin n) k →ₐ[k] R
fsurj : Function.Surjective ⇑f
ϕ : (MvPolynomial (Fin n) k ⧸ ker f) ≃ₐ[k] R := quotientKerAlgEquivOfSurjective fsurj
s : ℕ
left✝ : s ≤ n
g : MvPolynomial (Fin s) k →ₐ[k] MvPolynomial (Fin n) k ⧸ ker f
injg : Function.Injective ⇑g
intg : g.IsIntegral
⊢ ∃ s g, Function.Injective ⇑g ∧ g.IsIntegral
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ C (1 / ↑p ^ n) * (wittStructureRat p Φ n * C (↑p ^ n)) =
    C (1 / ↑p ^ n) *
      ((bind₁ fun b ↦ (rename fun i ↦ (b, i)) (W_ ℚ n)) Φ -
        ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i))

Tactic:
rw [wittStructureRat_rec_aux]

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

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
i : ℕ
hi : i < n + 1
⊢ (expand p) (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i) =
    (expand p) ((map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))

Tactic:
simp only [IH i hi]

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
p : ℕ
f : Perfection M p
m n : ℕ
⊢ (coeffMonoidHom M p (m + n)) (f ^ p ^ n) = (coeffMonoidHom M p m) f

Tactic:
coeffMonoidHom_pow_p_pow

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
p : ℕ
f : Perfection M p
m n : ℕ
⊢ (coeffMonoidHom M p m) f = (coeffMonoidHom M p m) f
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
p : ℕ
f : Perfection M p
n m✝ m : ℕ
ih : (coeffMonoidHom M p (n + m)) ((⇑(powMonoidHom p))^[m] f) = (coeffMonoidHom M p n) f
⊢ (coeffMonoidHom M p (n + m).succ) ((powMonoidHom p) ((⇑(powMonoidHom p))^[m] f)) = (coeffMonoidHom M p n) f

Tactic:
coeffMonoidHom_powMonoidHom,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
p : ℕ
f : Perfection M p
n m✝ m : ℕ
ih : (coeffMonoidHom M p (n + m)) ((⇑(powMonoidHom p))^[m] f) = (coeffMonoidHom M p n) f
⊢ (coeffMonoidHom M p (n + m)) ((⇑(powMonoidHom p))^[m] f) = (coeffMonoidHom M p n) f
Module: Mathlib.RingTheory.WittVector.MulP

Goal state before:
pp: case «1»
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ (k : ℕ), (x * ↑n).coeff k = (aeval x.coeff) (wittMulN p n k)
k i : ℕ
⊢ Function.uncurry ![(x * ↑n).coeff, x.coeff] ((fun i ↦ i) ⟨1, ⋯⟩, i) =
    (aeval x.coeff) (Function.uncurry ![wittMulN p n, X] ((fun i ↦ i) ⟨1, ⋯⟩, i))

Tactic:
· simp [Function.uncurry, Matrix.cons_val_one, aeval_X]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
⊢ C (↑p ^ i) * (C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) + X i ^ p) ^ p ^ (n - i) *
        C (⅟↑p ^ n) -
      C (↑p ^ i) * X i ^ p ^ (n + 1 - i) * C (⅟↑p ^ n) =
    ∑ i_1 ∈ range (p ^ (n - i)),
      C ↑p *
        (MvPolynomial.map (Int.castRingHom ℚ))
          ((X i ^ p) ^ (p ^ (n - i) - (i_1 + 1)) * frobeniusPolyAux p i ^ (i_1 + 1) *
            C ↑((p ^ (n - i)).choose (i_1 + 1) / p ^ (n - i - v p (i_1 + 1)) * p ^ (i_1 - v p (i_1 + 1))))

Tactic:
add_pow,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
⊢ (C (↑p ^ i) *
          ∑ m ∈ range (p ^ (n - i) + 1),
            (C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i)) ^ m * (X i ^ p) ^ (p ^ (n - i) - m) *
              ↑((p ^ (n - i)).choose m)) *
        C (⅟↑p ^ n) -
      C (↑p ^ i) * X i ^ p ^ (n + 1 - i) * C (⅟↑p ^ n) =
    ∑ i_1 ∈ range (p ^ (n - i)),
      C ↑p *
        (MvPolynomial.map (Int.castRingHom ℚ))
          ((X i ^ p) ^ (p ^ (n - i) - (i_1 + 1)) * frobeniusPolyAux p i ^ (i_1 + 1) *
            C ↑((p ^ (n - i)).choose (i_1 + 1) / p ^ (n - i - v p (i_1 + 1)) * p ^ (i_1 - v p (i_1 + 1))))
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
r : O
h : (Ideal.Quotient.mk (Ideal.span {↑p})) r ≠ 0
hp : ↑p ∣ r
⊢ ↑p ∣ r

Tactic:
exact hp

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
⊢ (if P n then x.coeff n else 0) = (aeval x.coeff) (if P n then X n else 0)

Tactic:
split_ifs with hi <;> simp

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case inr.inr
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : f ≠ 0
hg : g ≠ 0
⊢ valAux K v O p (f + g) ≤ max (valAux K v O p f) (valAux K v O p g)

Tactic:
by_cases hfg : f + g = 0

Goal state after:
case pos
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : f ≠ 0
hg : g ≠ 0
hfg : f + g = 0
⊢ valAux K v O p (f + g) ≤ max (valAux K v O p f) (valAux K v O p g)

case neg
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : f ≠ 0
hg : g ≠ 0
hfg : ¬f + g = 0
⊢ valAux K v O p (f + g) ≤ max (valAux K v O p f) (valAux K v O p g)
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case neg
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
hf0 : ¬f = 0
n : ℕ
hn : (coeff n) f ≠ 0
⊢ valAux K v O p f = 0 ↔ f = 0

Tactic:
refine iff_of_false (fun hvf => hn ?_) hf0

Goal state after:
case neg
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
hf0 : ¬f = 0
n : ℕ
hn : (coeff n) f ≠ 0
hvf : valAux K v O p f = 0
⊢ (coeff n) f = 0
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: case e_a.e_a
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k ↦ (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)
n k : ℕ
⊢ (2 * n + 1) * (2 * n - 1)‼ * (2 * (n + 1) + (k + 1)).choose (k + 1) =
    (2 * n + 1) * (2 * n - 1)‼ * (2 * (n + 1) + k).choose k +
      (2 * n - 1)‼ * ((2 * n + (k + 2)).choose (k + 2) * (k + 2))

Tactic:
mul_comm (2 * n + 1)

Goal state after:
case e_a.e_a
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k ↦ (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)
n k : ℕ
⊢ (2 * n - 1)‼ * (2 * n + 1) * (2 * (n + 1) + (k + 1)).choose (k + 1) =
    (2 * n - 1)‼ * (2 * n + 1) * (2 * (n + 1) + k).choose k +
      (2 * n - 1)‼ * ((2 * n + (k + 2)).choose (k + 2) * (k + 2))
Module: Mathlib.RingTheory.Polynomial.Selmer

Goal state before:
pp: n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = z ^ 2
⊢ z ^ ?m.376 = 0

Tactic:
rwa [key, add_self_eq_zero] at h2

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c x1 x2 : R
ha : a ≠ 0
hvieta : b = -a * (x1 + x2) ∧ c = a * x1 * x2
this : C a * X ^ 2 + C b * X + C c = C a * (X - C x1) * (X - C x2)
⊢ (C a * X ^ 2 + C b * X + C c).roots = {x1, x2}

Tactic:
have h1 : C a * (X - C x1) ≠ 0 := mul_ne_zero (by simpa) (Polynomial.X_sub_C_ne_zero _)
      have h2 : C a * (X - C x1) * (X - C x2) ≠ 0 := mul_ne_zero h1 (Polynomial.X_sub_C_ne_zero _)
      simp [this, Polynomial.roots_mul h2, Polynomial.roots_mul h1]

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Expand

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
m : ℕ
⊢ (MvPowerSeries.coeff (p • Finsupp.single () m)) ((MvPowerSeries.expand p hp) φ) =
    (MvPowerSeries.coeff (Finsupp.single () m)) φ

Tactic:
MvPowerSeries.coeff_expand_smul

Goal state after:
R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
m : ℕ
⊢ (MvPowerSeries.coeff (Finsupp.single () m)) φ = (MvPowerSeries.coeff (Finsupp.single () m)) φ
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case inl
A : Type u_1
inst✝¹ : CommRing A
g : A[X]
H : g.IsDistinguishedAt ⊤
inst✝ : IsHausdorff ⊤ A
⊢ (↑g).IsWeierstrassDivisorAt ⊤

Tactic:
have := ‹IsHausdorff ⊤ A›.subsingleton
    exact isUnit_of_subsingleton _

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (rTensor N A.val.toLinearMap) t = (rTensor N A'.val.toLinearMap) t'
hj : (A ⊔ A').val.comp (Subalgebra.inclusion ⋯) = A.val
hj' : (A ⊔ A').val.comp (Subalgebra.inclusion ⋯) = A'.val
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (rTensor N (Subalgebra.inclusion hAB).toLinearMap) t = (rTensor N (Subalgebra.inclusion hA'B).toLinearMap) t'

Tactic:
simp only [← hj, ← hj', AlgHom.comp_toLinearMap, rTensor_comp, comp_apply] at h

Goal state after:
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
hj : (A ⊔ A').val.comp (Subalgebra.inclusion ⋯) = A.val
hj' : (A ⊔ A').val.comp (Subalgebra.inclusion ⋯) = A'.val
h :
  (rTensor N (A ⊔ A').val.toLinearMap) ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap) t) =
    (rTensor N (A ⊔ A').val.toLinearMap) ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap) t')
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (rTensor N (Subalgebra.inclusion hAB).toLinearMap) t = (rTensor N (Subalgebra.inclusion hA'B).toLinearMap) t'
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
⊢ H.div 0 = 0

Tactic:
simpa using H.div_smul 0 0

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case inr
A : Type u_1
inst✝¹ : CommRing A
g✝ : A⟦X⟧
I✝ : Ideal A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst✝ : IsAdicComplete I A
h✝ : Nontrivial A
hI : I ≠ ⊤
this : Nontrivial (A ⧸ I)
f : A[X]
hfdeg : f.degree < g.degree
h1 : g.degree = ↑((map (Ideal.Quotient.mk I)) ↑g).order.toNat
⊢ ∃ a, a * g = ⋯.mod ↑f - f

Tactic:
exact ⟨0, by simp [H.isWeierstrassDivisorAt'.mod_coe_eq_self (hfdeg.trans_eq h1)]⟩

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case degree_lt.refine_2
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
H : g.IsWeierstrassFactorization f h
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
hn : n = ((map (IsLocalRing.residue A)) g).order.toNat
⊢ (Polynomial.X ^ n).leadingCoeff = f.leadingCoeff

Tactic:
rw [(Polynomial.monic_X_pow n).leadingCoeff, H.isDistinguishedAt.monic.leadingCoeff]

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
hx : x ∈ imageOfDf f
⊢ PrimeSpectrum.comap C { asIdeal := Ideal.map C x.asIdeal, isPrime := ⋯ } = x

Tactic:
ext x
    refine ⟨fun h => ?_, fun h => subset_span (mem_image_of_mem C.1 h)⟩
    rw [← @coeff_C_zero R x _]
    exact mem_map_C_iff.mp h 0

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 (⋃ i, PrimeSpectrum.comap C '' (zeroLocus {↑i})ᶜ)

Tactic:
simp_rw [← imageOfDf_eq_comap_C_compl_zeroLocus]

Goal state after:
R : Type u_1
inst✝ : CommRing R
U : Set (PrimeSpectrum R[X])
s : Set R[X]
z : zeroLocus s = Uᶜ
⊢ IsOpen (⋃ i, imageOfDf ↑i)
Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
m n : ℕ
r' q' : 𝕎 k
hr' : r'.coeff 0 ≠ 0
hq' : q'.coeff 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
b : 𝕎 k := frobeniusRotation p hr' hq'
key : frobenius b * r' = q' * b
⊢ φ ((algebraMap (𝕎 k) (FractionRing (𝕎 k))) b) * Localization.mk (↑p ^ m * r') ⟨↑p ^ n * q', hq⟩ =
    ↑p ^ (↑m - ↑n) * (algebraMap (𝕎 k) (FractionRing (𝕎 k))) b

Tactic:
have hq'' : algebraMap (𝕎 k) (FractionRing (𝕎 k)) q' ≠ 0 := by
    have hq''' : q' ≠ 0 := fun h => hq' (by simp [h])
    simpa only [Ne, map_zero] using
      (IsFractionRing.injective (𝕎 k) (FractionRing (𝕎 k))).ne hq'''

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
m n : ℕ
r' q' : 𝕎 k
hr' : r'.coeff 0 ≠ 0
hq' : q'.coeff 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
b : 𝕎 k := frobeniusRotation p hr' hq'
key : frobenius b * r' = q' * b
hq'' : (algebraMap (𝕎 k) (FractionRing (𝕎 k))) q' ≠ 0
⊢ φ ((algebraMap (𝕎 k) (FractionRing (𝕎 k))) b) * Localization.mk (↑p ^ m * r') ⟨↑p ^ n * q', hq⟩ =
    ↑p ^ (↑m - ↑n) * (algebraMap (𝕎 k) (FractionRing (𝕎 k))) b
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

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

Tactic:
simpa only [coe_ofPred, card_typein, card_ord] using mk_Iio_ordinal (ord <| succ #α)

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

Goal state before:
pp: case inl
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
a : Ordinal.{u}
ha : a < (succ #α).ord
b : Ordinal.{u}
hb : b < (succ #α).ord
hne : a ≠ b
hf : lfpApprox f x a = lfpApprox f x b
hab : a ≤ b
⊢ lfpApprox f x (succ #α).ord ∈ fixedPoints ⇑f

Tactic:
| inl hab =>

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

Goal state before:
pp: case pos
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
f c : Ordinal.{u_1}
hf : (f, c) ∈ CNF b y
he : e ≠ (f, c).1
⊢ (coeff b (b ^ e * x + y)) (f, c).1 = (coeff b y) (f, c).1

Tactic:
coeff_of_mem_CNF hf

Goal state after:
case pos
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
f c : Ordinal.{u_1}
hf : (f, c) ∈ CNF b y
he : e ≠ (f, c).1
⊢ (coeff b (b ^ e * x + y)) (f, c).1 = c
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: case neg
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
s : Set α
ha : ∃ b, b < a
⊢ (∃ᶠ (y : α) in 𝓝 a, y ≠ a ∧ y ∈ s) ↔ (∃ b, b < a) ∧ ∀ b < a, (s ∩ Ioo b a).Nonempty

Tactic:
(hasBasis_nhds_Ioc_of_exists_lt ha).frequently_iff,

Goal state after:
case neg
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
s : Set α
ha : ∃ b, b < a
⊢ (∀ i < a, ∃ x ∈ Ioc i a, x ≠ a ∧ x ∈ s) ↔ (∃ b, b < a) ∧ ∀ b < a, (s ∩ Ioo b a).Nonempty
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e : ONote
n : ℕ+
a₁ a₂ : ONote
h : a₁ < a₂
⊢ e.oadd n a₁ < e.oadd n a₂

Tactic:
rw [lt_def]; unfold repr; gcongr

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

Goal state before:
pp: α : Type u
A : α → PSet.{u}
β : Type u
B : β → PSet.{u}
H : (mk α A).Equiv (mk β B)
⊢ ∀ y ∈ mk β B, Acc (fun x1 x2 ↦ x1 ∈ x2) y

Tactic:
rintro ⟨γ, C⟩ ⟨b, hc⟩

Goal state after:
α : Type u
A : α → PSet.{u}
β : Type u
B : β → PSet.{u}
H : (mk α A).Equiv (mk β B)
γ : Type u
C : γ → PSet.{u}
b : (mk β B).Type
hc : (mk γ C).Equiv ((mk β B).Func b)
⊢ Acc (fun x1 x2 ↦ x1 ∈ x2) (mk γ C)
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: o : Ordinal.{u_1}
α✝ : Type u_1
A : α✝ → PSet.{u_1}
⊢ (mk α✝ A).rank ≤ o ↔ ∀ ⦃y : PSet.{u_1}⦄, y ∈ mk α✝ A → y.rank < o

Tactic:
refine ⟨fun h _ h' => (rank_lt_of_mem h').trans_le h, fun h ↦ Ordinal.iSup_le fun a ↦ ?_⟩

Goal state after:
o : Ordinal.{u_1}
α✝ : Type u_1
A : α✝ → PSet.{u_1}
h : ∀ ⦃y : PSet.{u_1}⦄, y ∈ mk α✝ A → y.rank < o
a : α✝
⊢ succ (A a).rank ≤ o
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case a
o a : Ordinal.{u}
h : a < veblen o a
⊢ o ≤ (veblen o a).invVeblen₁

Tactic:
← mem_range_veblen_iff_le_invVeblen₁

Goal state after:
case a
o a : Ordinal.{u}
h : a < veblen o a
⊢ ω ^ veblen o a ∈ range (veblen o)
Module: Mathlib.SetTheory.Ordinal.Veblen

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

Tactic:
· rw [← veblen_veblen_of_lt ho, veblen_zero_apply, opow_right_inj one_lt_omega0]
      rintro rfl
      simp [invVeblen₁_veblen h, invVeblen₂_veblen ho.ne' h]

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

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

pp: case mpr
o : Ordinal.{u}
⊢ o = 0 ∨ o ∈ range Γ_ → o.invVeblen₁ = o

Tactic:
· 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

Goal state after:
case mpr
o : Ordinal.{u}
⊢ o = 0 ∨ o ∈ range Γ_ → o.invVeblen₁ = o
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case h₂
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} := ⋯
R : Ordinal.{0} := ⋯
ω0 : Ordinal.{0} := ⋯
α' : Ordinal.{0} := ⋯
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 α'
⊢ ω ^ (a0.repr * succ ↑k) ≤ ω0 ^ succ ↑k * ↑↑n

Tactic:
have := mul_le_mul_right (one_le_iff_pos.2 <| Nat.cast_pos'.2 n.pos) (ω0 ^ succ (k : Ordinal))

Goal state after:
case h₂
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 α'
this : ω0 ^ succ ↑k * 1 ≤ ω0 ^ succ ↑k * ↑↑n
⊢ ω ^ (a0.repr * succ ↑k) ≤ ω0 ^ succ ↑k * ↑↑n