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

Goal state before:
pp: case mp
K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T : (fun x ↦ ((algebraMap K⟮X⟯ K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩) x.2)) ⁻¹' T ⊆ S
R : Set K⸨X⸩
hR : R ∈ nhds 0
pre_R : (fun x ↦ x.2 - x.1) ⁻¹' R ⊆ T
⊢ ∃ t ∈ nhds 0, (fun x ↦ x.2 - x.1) ⁻¹' t ⊆ S

Tactic:
obtain ⟨d, hd⟩ := Valued.mem_nhds.mp hR

Goal state after:
case mp
K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T : (fun x ↦ ((algebraMap K⟮X⟯ K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩) x.2)) ⁻¹' T ⊆ S
R : Set K⸨X⸩
hR : R ∈ nhds 0
pre_R : (fun x ↦ x.2 - x.1) ⁻¹' R ⊆ T
d : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hd : {y | Valued.v.restrict (y - 0) < ↑d} ⊆ R
⊢ ∃ t ∈ nhds 0, (fun x ↦ x.2 - x.1) ⁻¹' t ⊆ S
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
⊢ t ∈ pairs σ k ↔ #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)

Tactic:
simp [pairs]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
k : ℕ
⊢ ↑k * ∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i = 1 * ↑k * ∑ i ∈ powersetCard k univ, ∏ i ∈ i, X i

Tactic:
one_mul

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
k : ℕ
⊢ ↑k * ∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i = ↑k * ∑ i ∈ powersetCard k univ, ∏ i ∈ i, X i
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : ↑(Finsupp.degree d) < p • φ.order
i : σ
hi : ¬p ∣ d i
⊢ (coeff d) ((expand p hp) φ) = 0

Tactic:
exact coeff_expand_of_not_dvd p hp φ hi

Goal state after:
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
⊢ ((MvPolynomial.finSuccEquiv k n) ((T f) ((MvPolynomial.monomial v) (MvPolynomial.coeff v f)))).leadingCoeff =
    (algebraMap k (MvPolynomial (Fin n) k)) (MvPolynomial.coeff v f)

Tactic:
rw [monomial_eq, Finsupp.prod_fintype]

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
⊢ ((MvPolynomial.finSuccEquiv k n)
        ((T f) (MvPolynomial.C (MvPolynomial.coeff v f) * ∏ i, MvPolynomial.X i ^ v i))).leadingCoeff =
    (algebraMap k (MvPolynomial (Fin n) k)) (MvPolynomial.coeff v f)

case h
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
⊢ ∀ (i : Fin (n + 1)), MvPolynomial.X i ^ 0 = 1
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
⊢ constantCoeff (xInTermsOfW p R n) = 0

Tactic:
induction n using Nat.strongRecOn with

Goal state after:
case ind
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : Fact (Nat.Prime p)
inst✝ : Invertible ↑p
n : ℕ
IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0
⊢ constantCoeff (xInTermsOfW p R n) = 0
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ n ∈ (xInTermsOfW p ℚ n).vars ∧ (xInTermsOfW p ℚ n).vars ⊆ range (n + 1)

Tactic:
induction n using Nat.strongRecOn with

Goal state after:
case ind
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
⊢ n ∈ (xInTermsOfW p ℚ n).vars ∧ (xInTermsOfW p ℚ n).vars ⊆ range (n + 1)
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: case zero
k : Type u_1
inst✝ : Field k
n : ℕ
I : Ideal (MvPolynomial (Fin 0) k)
hi : I ≠ ⊤
a b : MvPolynomial (Fin 0) k
hab : a - b ∈ I
ne : ¬a = b
eq : a - b = MvPolynomial.C (MvPolynomial.coeff 0 (a - b))
⊢ False

Tactic:
have ne : coeff 0 (a - b) ≠ 0 := fun h ↦ h ▸ eq ▸ sub_ne_zero_of_ne ne <| map_zero _

Goal state after:
case zero
k : Type u_1
inst✝ : Field k
n : ℕ
I : Ideal (MvPolynomial (Fin 0) k)
hi : I ≠ ⊤
a b : MvPolynomial (Fin 0) k
hab : a - b ∈ I
ne✝ : ¬a = b
eq : a - b = MvPolynomial.C (MvPolynomial.coeff 0 (a - b))
ne : MvPolynomial.coeff 0 (a - b) ≠ 0
⊢ False
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: case refine_2
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
⊢ ∀ (y : ℕ → MvPolynomial (idx × ℕ) ℚ),
    (fun φ ↦ ∀ (n : ℕ), (bind₁ φ) (W_ ℚ n) = (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ n)) Φ) y →
      y = wittStructureRat p Φ

Tactic:
· intro φ H
    funext n
    rw [show φ n = bind₁ φ (bind₁ (W_ ℚ) (xInTermsOfW p ℚ n)) by
        rw [bind₁_wittPolynomial_xInTermsOfW p, bind₁_X_right]]
    rw [bind₁_bind₁]
    exact eval₂Hom_congr (RingHom.ext_rat _ _) (funext H) 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
⊢ ∃ s g, Function.Injective ⇑g ∧ g.Finite

Tactic:
by
  obtain ⟨s, g, ⟨inj, int⟩⟩ := exists_integral_inj_algHom_of_fg k R
  have h : algebraMap k R = g.toRingHom.comp (algebraMap k (MvPolynomial (Fin s) k)) := by
    algebraize [g.toRingHom]
    rw [IsScalarTower.algebraMap_eq k (MvPolynomial (Fin s) k), algebraMap_toAlgebra']
  exact ⟨s, g, inj, int.to_finite
    (h ▸ RingHom.finiteType_algebraMap.mpr fin).of_comp_finiteType⟩

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

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH : ∀ m < n, 0 < m → (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ 1 * C ⅟↑p ^ n - (∑ x ∈ Finset.range n, C ↑p ^ x * (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) * C ⅟↑p ^ n = 0

Tactic:
one_mul

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH : ∀ m < n, 0 < m → (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ m) = 0
hn : 0 < n
⊢ C ⅟↑p ^ n - (∑ x ∈ Finset.range n, C ↑p ^ x * (bind₁ fun k ↦ 1) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) * C ⅟↑p ^ n = 0
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
⊢ (bind₁ (W_ R)) (xInTermsOfW p R n) = X n

Tactic:
induction n using Nat.strongRecOn with

Goal state after:
case ind
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ (bind₁ (W_ R)) (xInTermsOfW p R n) = X n
Module: Mathlib.RingTheory.Perfection

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

Tactic:
rw [pow_succ, pow_mul, Nat.add_succ, coeffMonoidHom_pow_p, ih]

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
⊢ 1 * 0 = 0

Tactic:
one_mul

Goal state after:
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
⊢ 0 = 0
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 : ℕ
x y : ModP O p
hxy0 : x * y ≠ 0
⊢ preVal K v O p (x * y) = preVal K v O p x * preVal K v O p y

Tactic:
have hx0 : x ≠ 0 := mt (by rintro rfl; rw [zero_mul]) hxy0
  have hy0 : y ≠ 0 := mt (by rintro rfl; rw [mul_zero]) hxy0
  obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective x
  obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective y
  rw [← map_mul (Ideal.Quotient.mk (Ideal.span {↑p})) r s] at hxy0 ⊢
  rw [preVal_mk hv hx0, preVal_mk hv hy0, preVal_mk hv hxy0, map_mul, v.map_mul]

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
⊢ (mk p fun n ↦ (aeval x.coeff) (frobeniusPoly p n)).coeff n = (aeval x.coeff) (frobeniusPoly p n)

Tactic:
coeff_mk

Goal state after:
p : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
⊢ (aeval x.coeff) (frobeniusPoly p n) = (aeval x.coeff) (frobeniusPoly p n)
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: p n : ℕ
R : Type u_1
x : TruncatedWittVector p n R
i : Fin n
⊢ coeff i (mk p fun i ↦ coeff i x) = coeff i x

Tactic:
coeff_mk

Goal state after:
p n : ℕ
R : Type u_1
x : TruncatedWittVector p n R
i : Fin n
⊢ coeff i x = coeff i x
Module: Mathlib.RingTheory.WittVector.InitTail

Goal state before:
pp: p n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n ↦ y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n ↦ if P n then x.coeff n else y.coeff n
n : ℕ
⊢ (if P n then z.coeff n else 0) = x.coeff n

Tactic:
coeff_mk

Goal state after:
p n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n ↦ y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n ↦ if P n then x.coeff n else y.coeff n
n : ℕ
⊢ (if P n then if P n then x.coeff n else y.coeff n else 0) = x.coeff n
Module: Mathlib.RingTheory.WittVector.InitTail

Goal state before:
pp: p n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n ↦ y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n ↦ if P n then x.coeff n else y.coeff n
hx : select P z = x
n : ℕ
⊢ (if ¬P n then z.coeff n else 0) = y.coeff n

Tactic:
coeff_mk

Goal state after:
p n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n ↦ y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n ↦ if P n then x.coeff n else y.coeff n
hx : select P z = x
n : ℕ
⊢ (if ¬P n then if P n then x.coeff n else y.coeff n else 0) = y.coeff n
Module: Mathlib.RingTheory.Perfectoid.FontaineTheta

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsAdicComplete 𝔭 R
n : ℕ
⊢ (factorPowSucc 𝔭 (n + 1)).comp (fontaineThetaModPPow R p (n + 1)) = fontaineThetaModPPow R p n

Tactic:
by
  apply eq_of_apply_teichmuller_eq ((factorPowSucc _ _).comp (fontaineThetaModPPow R p (n + 1)))
    (fontaineThetaModPPow R p n)
  · use n + 1
    have : p = Ideal.Quotient.mk (𝔭 ^ (n + 1)) p := by
      simp [map_natCast]
    rw [this, ← map_pow, Ideal.Quotient.eq_zero_iff_mem]
    exact Ideal.pow_mem_pow (mem_span_singleton_self _) _
  simp [fontaineThetaModPPow]

Goal state after:
Module: Mathlib.RingTheory.Perfectoid.FontaineTheta

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsAdicComplete 𝔭 R
hF : Function.Surjective ⇑(_root_.frobenius (ModP R p) p)
this : Ideal.map (fontaineTheta R p) (span {↑p}) = 𝔭
x✝ : IsHausdorff (Ideal.map (fontaineTheta R p) (span {↑p})) R
h : Function.Surjective (⇑(Ideal.Quotient.mk 𝔭) ∘ ⇑(fontaineTheta R p))
⊢ Function.Surjective (⇑(Ideal.Quotient.mk (Ideal.map (fontaineTheta R p) (span {↑p}))) ∘ ⇑(fontaineTheta R p))

Tactic:
rwa [Ideal.map_span, Set.image_singleton, map_natCast]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian

Goal state before:
pp: case zero
x : ℝ
⊢ Real.exp (-(x ^ 2 / 2)) = 1 * Real.exp (-(x ^ 2 / 2))

Tactic:
one_mul

Goal state after:
case zero
x : ℝ
⊢ Real.exp (-(x ^ 2 / 2)) = Real.exp (-(x ^ 2 / 2))
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
m n : ℕ
h : 1 = (Int.castRingHom R) 1
⊢ Chebyshev.T ℚ ↑n = 1 * Chebyshev.T ℚ ↑n

Tactic:
one_mul

Goal state after:
R : Type u_1
inst✝ : CommRing R
m n : ℕ
h : 1 = (Int.castRingHom R) 1
⊢ Chebyshev.T ℚ ↑n = Chebyshev.T ℚ ↑n
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚₗ[R] N
n : ℕ
f : M →ₚₗ[R] N
⊢ ↑(Int.negSucc n) • f = -(↑↑n.succ • f)

Tactic:
ext S _ _ m

Goal state after:
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚₗ[R] N
n : ℕ
f : M →ₚₗ[R] N
S : Type u
x✝¹ : CommSemiring S
x✝ : Algebra R S
m : S ⊗[R] M
⊢ (↑(Int.negSucc n) • f).toFun' S m = (-(↑↑n.succ • f)).toFun' S m
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ f : M →ₚₗ[R] N
⊢ -f + f = 0

Tactic:
ext S _ _ m

Goal state after:
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ f : M →ₚₗ[R] N
S : Type u
x✝¹ : CommSemiring S
x✝ : Algebra R S
m : S ⊗[R] M
⊢ (-f + f).toFun' S m = toFun' 0 S m
Module: Mathlib.RingTheory.PowerSeries.Log

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
this : ↑n + 1 = (algebraMap ℚ A) (↑n + 1)
⊢ (if n + 1 = 0 then 0 else (algebraMap ℚ A) ((-1) ^ (n + 1 + 1) / ↑(n + 1))) * (↑n + 1) =
    (coeff n) (mk fun n ↦ (algebraMap ℚ A) ((-1) ^ n))

Tactic:
coeff_mk

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
this : ↑n + 1 = (algebraMap ℚ A) (↑n + 1)
⊢ (if n + 1 = 0 then 0 else (algebraMap ℚ A) ((-1) ^ (n + 1 + 1) / ↑(n + 1))) * (↑n + 1) = (algebraMap ℚ A) ((-1) ^ n)
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
f : A⟦X⟧
k i✝¹ : ℕ
q : A⟦X⟧ := H.seq f k
s : A⟦X⟧ := f - g * q
n : ℕ := ((map (Ideal.Quotient.mk I)) g).order.toNat
hi : i✝¹ ≥ n
hq : ∀ {i : ℕ}, i ≥ n → (coeff i) s ∈ I ^ k
s₀ : A[X] := (trunc n) s
s₁ : A⟦X⟧ := mk fun i ↦ (coeff (i + n)) s
hs : s = X ^ n * s₁ + ↑s₀
q' : A⟦X⟧ := q + s₁ * ↑⋯.unit⁻¹
key : f - g * q' = ↑s₀ - ↑((trunc n) g) * s₁ * ↑⋯.unit⁻¹
i✝ i : ℕ
⊢ (coeff i) s₁ ∈ I ^ k

Tactic:
coeff_mk

Goal state after:
case succ
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i✝¹ : ℕ
q : A⟦X⟧ := H.seq f k
s : A⟦X⟧ := f - g * q
n : ℕ := ((map (Ideal.Quotient.mk I)) g).order.toNat
hi : i✝¹ ≥ n
hq : ∀ {i : ℕ}, i ≥ n → (coeff i) s ∈ I ^ k
s₀ : A[X] := (trunc n) s
s₁ : A⟦X⟧ := mk fun i ↦ (coeff (i + n)) s
hs : s = X ^ n * s₁ + ↑s₀
q' : A⟦X⟧ := q + s₁ * ↑⋯.unit⁻¹
key : f - g * q' = ↑s₀ - ↑((trunc n) g) * s₁ * ↑⋯.unit⁻¹
i✝ i : ℕ
⊢ (coeff (i + n)) s ∈ I ^ k
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✝ i : ℕ
⊢ (coeff i) (mk fun i ↦ (coeff (i + ((map (Ideal.Quotient.mk I)) g).order.toNat)) (f - g * H.seq f k)) ∈ I ^ k

Tactic:
coeff_mk

Goal state after:
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i✝ i : ℕ
⊢ (coeff (i + ((map (Ideal.Quotient.mk I)) g).order.toNat)) (f - g * H.seq f k) ∈ I ^ k
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 :
  1 * 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) q ∈ I ^ (k + 1)

Tactic:
one_mul

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 : ℕ), (coeff i) q ∈ I ^ (k + 1)
Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin

Goal state before:
pp: R₀ : Type u_1
R : Type u
inst✝⁵ : CommSemiring R₀
inst✝⁴ : Ring R
inst✝³ : Algebra R₀ R
inst✝² : IsSimpleRing R
inst✝¹ : IsArtinianRing R
inst✝ : Module.Finite R₀ R
⊢ ∃ n, ∃ (_ : NeZero n), ∃ D x x_1, ∃ (_ : Module.Finite R₀ D), Nonempty (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) D)

Tactic:
by
  have ⟨n, hn, I, _, ⟨e⟩⟩ := exists_algEquiv_matrix_end_mulOpposite R₀ R
  have := Module.Finite.equiv e.toLinearEquiv
  classical exact ⟨n, hn, _, _, _, .of_surjective
    (Matrix.entryLinearMap R₀ _ (0 : Fin n) (0 : Fin n)) fun f ↦ ⟨fun _ _ ↦ f, rfl⟩, ⟨e⟩⟩

Goal state after:
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
h1 : Function.Injective (comap f)
hint : f.kerLift.IsIntegral
hbij : Function.Bijective (comap f)
⊢ ∀ s ∈ Set.range fun r ↦ ↑(basicOpen r), IsOpen (comap f '' s)

Tactic:
rintro - ⟨s, rfl⟩

Goal state after:
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
h1 : Function.Injective (comap f)
hint : f.kerLift.IsIntegral
hbij : Function.Bijective (comap f)
s : S
⊢ IsOpen (comap f '' (fun r ↦ ↑(basicOpen r)) s)
Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph

Goal state before:
pp: case e'_3
k : Type u_1
K : Type u_2
R : Type u_3
inst✝⁵ : Field k
inst✝⁴ : Field K
inst✝³ : Algebra k K
inst✝² : CommRing R
inst✝¹ : Algebra k R
inst✝ : IsPurelyInseparable k K
q : ℕ := ringExpChar k
⊢ RingHom.ker (algebraMap R (R ⊗[k] K)) = ⊥

pp: case convert_3
k : Type u_1
K : Type u_2
R : Type u_3
inst✝⁵ : Field k
inst✝⁴ : Field K
inst✝³ : Algebra k K
inst✝² : CommRing R
inst✝¹ : Algebra k R
inst✝ : IsPurelyInseparable k K
q : ℕ := ⋯
⊢ OrderBot (Ideal R)

Tactic:
rw [← RingHom.injective_iff_ker_eq_bot]

Goal state after:
case e'_3
k : Type u_1
K : Type u_2
R : Type u_3
inst✝⁵ : Field k
inst✝⁴ : Field K
inst✝³ : Algebra k K
inst✝² : CommRing R
inst✝¹ : Algebra k R
inst✝ : IsPurelyInseparable k K
q : ℕ := ringExpChar k
⊢ Function.Injective ⇑(algebraMap R (R ⊗[k] K))
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Moebius

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h✝ : Subsingleton α
⊢ moebius b = 1 * moebius b

Tactic:
one_mul

Goal state after:
case inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h✝ : Subsingleton α
⊢ moebius b = moebius b
Module: Mathlib.RingTheory.Valuation.AlgebraInstances

Goal state before:
pp: K : Type u_1
inst✝⁶ : Field K
v : Valuation K (WithZero (Multiplicative ℤ))
L : Type u_2
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
E : Type ?u.16
inst✝³ : Field E
inst✝² : Algebra K E
inst✝¹ : Algebra L E
inst✝ : IsScalarTower K L E
⊢ ↑⟨(algebraMap L E) ↑0, ⋯⟩ = ↑0

Tactic:
by simp only [Subalgebra.coe_zero, map_zero]

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

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

Tactic:
simp_all [Valuation.one_apply_of_ne_zero, Valuation.one_apply_le_one]

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

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

Tactic:
simp_all [Valuation.one_apply_of_ne_zero, Valuation.one_apply_le_one]

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
I : Ideal R
f : M →ₗ[R] N
surj : Function.Surjective ⇑f
inst✝ : Module.Flat R N
x : M
hx : x ∈ I • f.ker
⊢ x ∈ f.ker ⊓ I • ⊤

Tactic:
induction hx using Submodule.smul_induction_on' with
    | smul r hr m hm =>
      simpa [LinearMap.mem_ker.mp hm] using Submodule.smul_mem_smul hr Submodule.mem_top
    | add y ymem z zmem hy hz => exact add_mem hy hz

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
h₁ : b.coeff 0 ≠ 0
h₂ : a = ↑p ^ m * b
⊢ ∃ m b, a = ↑p ^ m * ↑b

Tactic:
let b₀ := Units.mk0 (b.coeff 0) h₁

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
h₁ : b.coeff 0 ≠ 0
h₂ : a = ↑p ^ m * b
b₀ : kˣ := Units.mk0 (b.coeff 0) h₁
⊢ ∃ m b, a = ↑p ^ m * ↑b
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
this : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1))).degree = ↑p
⊢ 1 < ↑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
this : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1))).degree = ↑p
⊢ a₂.coeff 0 ^ p ^ (n + 1) ≠ 0

Tactic:
· exact mod_cast hp.out.one_lt

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
this : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1))).degree = ↑p
⊢ a₂.coeff 0 ^ p ^ (n + 1) ≠ 0
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.{v, u} (cof α) ≤ lift.{u, v} #β

Tactic:
rw [← lift_cof_congr_of_strictMono (rangeSplitting_strictMono hf) hα, 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.UnivLE

Goal state before:
pp: case refine_1
x✝ : ∃ α, univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α
α : Type u
le : univ.{v, u + 1} ≤ lift.{max (v + 1) (u + 1), u} #α
⊢ univ.{v, u + 1} < univ.{u, v + 1}

Tactic:
exact le.trans_lt (lift_lt_univ'.{u, v + 1} #α)

Goal state after:
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.Countable
hα : cof α < ℵ₀
⊢ IsStationary (⋃₀ s) ↔ ∃ x ∈ s, IsStationary x

Tactic:
apply isStationary_sUnion_iff_of_cof_le_one
    rwa [← cof_lt_aleph0_iff]

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

Goal state before:
pp: b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
hb' : b ≠ ⊥
⊢ (e, (b ^ e * x + y) / b ^ e) :: CNF b ((b ^ e * x + y) % b ^ e) = (e, x) :: CNF b y

Tactic:
mul_add_div _ (opow_ne_zero _ hb'),

Goal state after:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
hb' : b ≠ ⊥
⊢ (e, x + y / b ^ e) :: CNF b ((b ^ e * x + y) % b ^ e) = (e, x) :: CNF b y