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

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
σ : Type u_3
Φ : MvPolynomial idx ℤ
f : idx → σ
n : ℕ
⊢ (map (Int.castRingHom ℚ)) (wittStructureInt p ((rename f) Φ) n) =
    (map (Int.castRingHom ℚ)) ((rename (Prod.map f id)) (wittStructureInt p Φ n))

Tactic:
simp only [map_rename, map_wittStructureInt, wittStructureRat, rename_bind₁, rename_rename,
    bind₁_rename]

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
σ : Type u_3
Φ : MvPolynomial idx ℤ
f : idx → σ
n : ℕ
⊢ (bind₁ fun k ↦ (bind₁ ((fun i ↦ (rename (Prod.mk i)) (W_ ℚ k)) ∘ f)) ((map (Int.castRingHom ℚ)) Φ))
      (xInTermsOfW p ℚ n) =
    (bind₁ fun i ↦ (bind₁ fun i_1 ↦ (rename (Prod.map f id ∘ Prod.mk i_1)) (W_ ℚ i)) ((map (Int.castRingHom ℚ)) Φ))
      (xInTermsOfW p ℚ n)
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h✝ : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
m : ℕ
h : n ≤ m
⊢ R

Tactic:
induction h using Nat.leRec with
    | refl =>
      exact x
    | le_succ_of_le hle xk =>
      choose x hx using h xk
      use x

Goal state after:
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 : ModP O p
hx : x = 0
⊢ preVal K v O p x = 0

Tactic:
simp [hx]

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
m n : ℕ
hn : (coeff n) g ≠ 0
hm : (Perfection.coeff (ModP O p) p (max m n)) f ≠ 0
⊢ valAux K v O p (f * g) = valAux K v O p f * valAux K v O p g

Tactic:
replace hn := coeff_ne_zero_of_le hn (le_max_right m n)

Goal state after:
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
m n : ℕ
hm : (Perfection.coeff (ModP O p) p (max m n)) f ≠ 0
hn : (Perfection.coeff (ModP O p) p (max m n)) g ≠ 0
⊢ valAux K v O p (f * g) = valAux K v O p f * valAux K v O p g
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
n₁ n₂ n₃ : ℕ
h1 : n₁ ≤ n₂
h2 : n₂ ≤ n₃
⊢ (truncate h1).comp (truncate h2) = truncate ⋯

Tactic:
by
  ext1 x; simp only [truncate_truncate, Function.comp_apply, RingHom.coe_comp]

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
n : ℕ
⊢ (factorPowSucc 𝔭 (n + 1)).comp (fontaineThetaModPPow R p (n + 1)) = fontaineThetaModPPow R p n

Tactic:
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.WittVector.TeichmullerSeries

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
x : R
m n : ℕ
h✝ : m ≠ n
h : n < m
⊢ ((teichmuller p) x * ↑p ^ n).coeff m = 0

Tactic:
rw [← Nat.sub_add_cancel h.le, WittVector.mul_pow_charP_coeff_succ (teichmuller p x),
      WittVector.teichmuller_coeff_pos p x (m - n) (Nat.zero_lt_sub_of_lt h), zero_pow]
    simp [Nat.Prime.ne_zero Fact.out]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
f h : R⟦X⟧
g : R[X]
distinguish : g.IsDistinguishedAt I
notMem : PowerSeries.constantCoeff h ∉ I
eq : f = ↑g * h
H : (PowerSeries.map (Ideal.Quotient.mk I)) f = 0
⊢ False

Tactic:
by
  have mapf : f.map (Ideal.Quotient.mk I) = (Polynomial.X ^ g.natDegree : (R ⧸ I)[X]) *
      h.map (Ideal.Quotient.mk I) := by
    simp [← map_eq_X_pow distinguish, eq]
  apply_fun PowerSeries.coeff g.natDegree at H
  simp [mapf, PowerSeries.coeff_X_pow_mul', eq_zero_iff_mem, notMem] at H

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
h : x * y = 1
n : ℕ
⊢ eval (x + y) (dickson 1 1 (n + 2)) = x ^ (n + 2) + y ^ (n + 2)

Tactic:
simp only [eval_sub, eval_mul, dickson_one_one_eval_add_inv x y h _, eval_X, dickson_add_two,
      C_1, eval_one]
    conv_lhs => simp only [pow_succ', add_mul, mul_add, h, ← mul_assoc, mul_comm y x, one_mul]
    ring

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

Goal state before:
pp: case succ.succ
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → (hermite n).coeff k = 0
k : ℕ
hnk : Odd (n + 1 + (k + 1))
⊢ Odd (n + (k + 2))

pp: case succ.succ
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → (hermite n).coeff k = 0
k : ℕ
hnk : Odd (n + 1 + (k + 1))
⊢ Odd (n + k)

Tactic:
· rwa [Nat.succ_add_eq_add_succ] at hnk

Goal state after:
case succ.succ
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → (hermite n).coeff k = 0
k : ℕ
hnk : Odd (n + 1 + (k + 1))
⊢ Odd (n + k)
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 = C ⅟2 * X.comp (2 * Chebyshev.T ℚ ↑n)

Tactic:
X_comp,

Goal state after:
R : Type u_1
inst✝ : CommRing R
m n : ℕ
h : 1 = (Int.castRingHom R) 1
⊢ Chebyshev.T ℚ ↑n = C ⅟2 * (2 * Chebyshev.T ℚ ↑n)
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
⊢ False

Tactic:
apply H

Goal state after:
case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
⊢ Set.univ.Finite
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
q : F[X]
hq1 : p = (X - C 1) ^ rootMultiplicity 1 p * q
hq2 : ¬X - C 1 ∣ q
heq : p = q * (-1) ^ rootMultiplicity 1 p * (1 - X) ^ rootMultiplicity 1 p
x✝¹ : ℕ
x✝ : x✝¹ ∈ (q * (-1) ^ rootMultiplicity 1 p).support
⊢ ((q * (-1) ^ rootMultiplicity 1 p).coeff x✝¹ • preHilbertPoly F (d - rootMultiplicity 1 p - 1) x✝¹).natDegree ≤
    d - rootMultiplicity 1 p - 1

Tactic:
apply le_trans (natDegree_smul_le _ _)

Goal state after:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
q : F[X]
hq1 : p = (X - C 1) ^ rootMultiplicity 1 p * q
hq2 : ¬X - C 1 ∣ q
heq : p = q * (-1) ^ rootMultiplicity 1 p * (1 - X) ^ rootMultiplicity 1 p
x✝¹ : ℕ
x✝ : x✝¹ ∈ (q * (-1) ^ rootMultiplicity 1 p).support
⊢ (preHilbertPoly F (d - rootMultiplicity 1 p - 1) x✝¹).natDegree ≤ d - rootMultiplicity 1 p - 1
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

Goal state before:
pp: n : ℕ
⊢ ∑ i ∈ range (n + 1), ↑n ! * C ((-1) ^ i * ↑(n.choose i) * ↑((n + i).choose n)) * X ^ i = ↑n ! * shiftedLegendre n

Tactic:
simp [← mul_assoc, shiftedLegendre, mul_sum]

Goal state after:
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
A : Type u
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommSemiring T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq : (rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (rTensor M ψ.rangeRestrict.toLinearMap) q
θ : (RingCon.ker ↑φ).Quotient →ₐ[R] (RingCon.ker ↑ψ).Quotient :=
  (↑(quotientKerEquivRangeₐ ψ).symm).comp (h'.comp ↑(quotientKerEquivRangeₐ φ))
ht : (h.comp φ.range.val).comp ↑(quotientKerEquivRangeₐ φ) = ψ.range.val.comp ((↑(quotientKerEquivRangeₐ ψ)).comp θ)
⊢ (rTensor N (↑(quotientKerEquivRangeₐ ψ)).toLinearMap)
      ((rTensor N θ.toLinearMap)
        (f.toFun' (RingCon.ker ↑φ).Quotient ((rTensor M (mkₐ R (RingCon.ker ↑φ)).toLinearMap) p))) =
    (rTensor N (↑(quotientKerEquivRangeₐ ψ)).toLinearMap)
      (f.toFun' (RingCon.ker ↑ψ).Quotient ((rTensor M (mkₐ R (RingCon.ker ↑ψ)).toLinearMap) q))

Tactic:
isCompat_apply'

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
A : Type u
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommSemiring T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq : (rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (rTensor M ψ.rangeRestrict.toLinearMap) q
θ : (RingCon.ker ↑φ).Quotient →ₐ[R] (RingCon.ker ↑ψ).Quotient :=
  (↑(quotientKerEquivRangeₐ ψ).symm).comp (h'.comp ↑(quotientKerEquivRangeₐ φ))
ht : (h.comp φ.range.val).comp ↑(quotientKerEquivRangeₐ φ) = ψ.range.val.comp ((↑(quotientKerEquivRangeₐ ψ)).comp θ)
⊢ (rTensor N (↑(quotientKerEquivRangeₐ ψ)).toLinearMap)
      (f.toFun' (RingCon.ker ↑ψ).Quotient
        ((rTensor M θ.toLinearMap) ((rTensor M (mkₐ R (RingCon.ker ↑φ)).toLinearMap) p))) =
    (rTensor N (↑(quotientKerEquivRangeₐ ψ)).toLinearMap)
      (f.toFun' (RingCon.ker ↑ψ).Quotient ((rTensor M (mkₐ R (RingCon.ker ↑ψ)).toLinearMap) q))
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
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h✝ : π R M S ⟨s, p⟩ = π R M S ⟨s', p'⟩
u : ↥(φ R s).range ⊗[R] M := (rTensor M (φ R s).rangeRestrict.toLinearMap) p
hu : u = (rTensor M (φ R s).rangeRestrict.toLinearMap) p
uFG : (φ R s).range.FG
u' : ↥(φ R s').range ⊗[R] M := (rTensor M (φ R s').rangeRestrict.toLinearMap) p'
hu' : u' = (rTensor M (φ R s').rangeRestrict.toLinearMap) p'
u'FG : (φ R s').range.FG
huu' : (rTensor M (φ R s).range.val.toLinearMap) u = (rTensor M (φ R s').range.val.toLinearMap) u'
B : Subalgebra R S
hAB : (φ R s).range ≤ B
hA'B : (φ R s').range ≤ B
h : (rTensor M (Subalgebra.inclusion hAB).toLinearMap) u = (rTensor M (Subalgebra.inclusion hA'B).toLinearMap) u'
t : Finset S
hB : B = (φ R t).range
hAB' : (φ R s).range ≤ (φ R t).range
hA'B' : (φ R s').range ≤ (φ R t).range
this :
  ∃ q,
    (rTensor M (φ R t).rangeRestrict.toLinearMap) q =
      (rTensor M ((Subalgebra.inclusion ⋯).comp (Subalgebra.inclusion hAB)).toLinearMap) u
⊢ (rTensor N (φ R s).toLinearMap) (f.toFun' (MvPolynomial (Fin s.card) R) p) =
    (rTensor N (φ R s').toLinearMap) (f.toFun' (MvPolynomial (Fin s'.card) R) p')

Tactic:
obtain ⟨q, hq⟩ := this

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
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h✝ : π R M S ⟨s, p⟩ = π R M S ⟨s', p'⟩
u : ↥(φ R s).range ⊗[R] M := (rTensor M (φ R s).rangeRestrict.toLinearMap) p
hu : u = (rTensor M (φ R s).rangeRestrict.toLinearMap) p
uFG : (φ R s).range.FG
u' : ↥(φ R s').range ⊗[R] M := (rTensor M (φ R s').rangeRestrict.toLinearMap) p'
hu' : u' = (rTensor M (φ R s').rangeRestrict.toLinearMap) p'
u'FG : (φ R s').range.FG
huu' : (rTensor M (φ R s).range.val.toLinearMap) u = (rTensor M (φ R s').range.val.toLinearMap) u'
B : Subalgebra R S
hAB : (φ R s).range ≤ B
hA'B : (φ R s').range ≤ B
h : (rTensor M (Subalgebra.inclusion hAB).toLinearMap) u = (rTensor M (Subalgebra.inclusion hA'B).toLinearMap) u'
t : Finset S
hB : B = (φ R t).range
hAB' : (φ R s).range ≤ (φ R t).range
hA'B' : (φ R s').range ≤ (φ R t).range
q : MvPolynomial (Fin t.card) R ⊗[R] M
hq :
  (rTensor M (φ R t).rangeRestrict.toLinearMap) q =
    (rTensor M ((Subalgebra.inclusion ⋯).comp (Subalgebra.inclusion hAB)).toLinearMap) u
⊢ (rTensor N (φ R s).toLinearMap) (f.toFun' (MvPolynomial (Fin s.card) R) p) =
    (rTensor N (φ R s').toLinearMap) (f.toFun' (MvPolynomial (Fin s'.card) R) p')
Module: Mathlib.RingTheory.Regular.Free

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x : R
mem : x ∈ ⊥.jacobson
reg : IsSMulRegular M x
free : Free (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
this : Module.Finite (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
I : Type u_2 := Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b : Basis (Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)) (R ⧸ Ideal.span {x}) (QuotSMulTop x M) :=
  Free.chooseBasis (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b' : QuotSMulTop x M ≃ₗ[R] I →₀ R ⧸ Ideal.span {x} := LinearEquiv.restrictScalars R b.repr
f : (I →₀ R) →ₗ[R] QuotSMulTop x M := ↑b'.symm ∘ₗ Finsupp.mapRange.linearMap (Submodule.mkQ (Ideal.span {x}))
g : (I →₀ R) →ₗ[R] M
hg : (x • ⊤).mkQ ∘ₗ g = f
surjf : Function.Surjective ⇑f
lejac : Ideal.span {x} ≤ ⊥.jacobson
surjg : Function.Surjective ⇑g
⊢ (Ideal.span {x} • Finsupp.submodule fun x ↦ ⊤) = x • ⊤

Tactic:
simp [Submodule.ideal_span_singleton_smul]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
R' : Type u_2
inst✝¹ : CommRing R'
e : R ≃+* R'
inst✝ : IsRegularRing R
⊢ IsRegularRing R'

Tactic:
by
  have := isNoetherianRing_of_ringEquiv R e
  rw [isRegularRing_iff]
  intro p hp
  exact IsRegularLocalRing.of_ringEquiv <| IsLocalization.ringEquivOfRingEquiv
    (Localization.AtPrime (p.comap e)) (Localization.AtPrime p) e (e.map_primeCompl_comap_eq p)

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
p : Ideal R[X]
inst✝ : p.IsPrime
max : comap C p = maximalIdeal R
q : Ideal R[X] := Ideal.map C (maximalIdeal R)
qle : q ≤ p
⊢ ↑(Submodule.spanFinrank (maximalIdeal (Localization.AtPrime p))) ≤ ringKrullDim (Localization.AtPrime p)

Tactic:
have reg := (isRegularLocalRing_iff R).mp ‹_›

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
p : Ideal R[X]
inst✝ : p.IsPrime
max : comap C p = maximalIdeal R
q : Ideal R[X] := Ideal.map C (maximalIdeal R)
qle : q ≤ p
reg : ↑(Submodule.spanFinrank (maximalIdeal R)) = ringKrullDim R
⊢ ↑(Submodule.spanFinrank (maximalIdeal (Localization.AtPrime p))) ≤ ringKrullDim (Localization.AtPrime p)
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 : Type w
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S ⟨s, p⟩ = t
s' : Finset T := Finset.image (⇑h) s
x : S
hx✝ : x ∈ (φ R s).range
hx : x ∈ Algebra.adjoin R ↑s
⊢ (h.comp (φ R s).range.val) ⟨x, hx✝⟩ ∈ Algebra.adjoin R ↑s'

Tactic:
simp only [AlgHom.coe_comp, Subalgebra.coe_val, Function.comp_apply, Finset.coe_image,
      Algebra.adjoin_image, s']

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 : Type w
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S ⟨s, p⟩ = t
s' : Finset T := Finset.image (⇑h) s
x : S
hx✝ : x ∈ (φ R s).range
hx : x ∈ Algebra.adjoin R ↑s
⊢ h x ∈ Subalgebra.map h (Algebra.adjoin R ↑s)
Module: Mathlib.RingTheory.Regular.ProjectiveDimension

Goal state before:
pp: case coe
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)
aux : ∀ (n : ℕ), projectiveDimension (of R (QuotSMulTop x ↑M)) ≤ ↑n ↔ projectiveDimension M + 1 ≤ ↑n
N : ℕ∞
⊢ projectiveDimension (of R (QuotSMulTop x ↑M)) ≤ ↑N ↔ projectiveDimension M + 1 ≤ ↑N

Tactic:
induction N with

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)
aux : ∀ (n : ℕ), projectiveDimension (of R (QuotSMulTop x ↑M)) ≤ ↑n ↔ projectiveDimension M + 1 ≤ ↑n
N : WithBot ℕ∞
⊢ projectiveDimension (of R (QuotSMulTop x ↑M)) ≤ N ↔ projectiveDimension M + 1 ≤ N

Tactic:
induction N with

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
H✝ : (X ^ ((map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g q r
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H : (X ^ n).IsWeierstrassDivision g q r
f : A[X] := Polynomial.X ^ n - r
H1 : r.degree < (Polynomial.X ^ n).degree
⊢ f.degree = ↑n

Tactic:
Polynomial.degree_sub_eq_left_of_degree_lt H1,

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
H✝ : (X ^ ((map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g q r
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H : (X ^ n).IsWeierstrassDivision g q r
f : A[X] := Polynomial.X ^ n - r
H1 : r.degree < (Polynomial.X ^ n).degree
⊢ (Polynomial.X ^ n).degree = ↑n
Module: Mathlib.RingTheory.SimpleRing.DivisionRing

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ :
  Nontrivial M ∧
    ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module R N] (f : M →ₗ[R] N), f = 0 ∨ Function.Injective ⇑f
hM1 : Nontrivial M
hM2 : ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module R N] (f : M →ₗ[R] N), f = 0 ∨ Function.Injective ⇑f
p : Submodule R M
h : Function.Injective ⇑p.mkQ
x : M
hx : x ∈ p
⊢ p.mkQ x = p.mkQ 0

Tactic:
simp [hx]

Goal state after:
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
hx : x ∈ imageOfDf f
⊢ ¬{f} ⊆ ↑{ asIdeal := Ideal.map C x.asIdeal, isPrime := ⋯ }.asIdeal

Tactic:
singleton_subset_iff

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
hx : x ∈ imageOfDf f
⊢ f ∉ ↑{ asIdeal := Ideal.map C x.asIdeal, isPrime := ⋯ }.asIdeal
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
hx : x ∈ imageOfDf f
⊢ { asIdeal := Ideal.map C x.asIdeal, isPrime := ⋯ } ∈ (zeroLocus {f})ᶜ

Tactic:
rw [mem_compl_iff, mem_zeroLocus, singleton_subset_iff]
    obtain ⟨i, hi⟩ := hx
    exact fun a => hi (mem_map_C_iff.mp a i)

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n i : ℕ
m✝ : Fin 2 × ℕ →₀ ℕ
⊢ (Finsupp.single i (p ^ (n - i))) i ≠ 0 ∧
    Finsupp.single i (p ^ (n - i)) = Finsupp.single i ((Finsupp.single i (p ^ (n - i))) i)

Tactic:
simp only [and_true, Finsupp.single_eq_same, Ne]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n i : ℕ
m✝ : Fin 2 × ℕ →₀ ℕ
⊢ ¬p ^ (n - i) = 0
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
⊢ coeff b (b ^ e * x + y) = single e x + coeff b y

Tactic:
by
  ext e'
  rw [add_apply]
  obtain rfl | he := eq_or_ne e e'
  · rw [single_eq_same, coeff_eq_zero_of_lt hy, add_zero]
    apply coeff_of_mem_CNF
    rw [CNF.opow_mul_add hb hx hxb hy]
    exact mem_cons_self
  · rw [single_eq_of_ne' he, zero_add]
    by_cases h : e' ∈ (CNF b y).map Prod.fst
    · rw [mem_map] at h
      obtain ⟨⟨f, c⟩, hf, rfl⟩ := h
      rw [coeff_of_mem_CNF hf]
      apply coeff_of_mem_CNF
      rw [CNF.opow_mul_add hb hx hxb hy]
      exact mem_cons_of_mem _ hf
    · rw [coeff_of_notMem_CNF h, coeff_of_notMem_CNF]
      rw [mem_map] at h ⊢
      rw [CNF.opow_mul_add hb hx hxb hy]
      simp_all

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

Goal state before:
pp: b e' x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hx : x ≠ 0
IH : ∀ {e : Ordinal.{u_1}}, (∀ (e' : Ordinal.{u_1}), f e' < b) → (∀ e' ∈ f.support, e' < e) → eval b f < b ^ e
e : Ordinal.{u_1}
hb : ∀ (e'_1 : Ordinal.{u_1}), (single e' x + f) e'_1 < b
he : ∀ e'_1 ∈ (single e' x + f).support, e'_1 < e
he' : e' ∉ f.support
⊢ e' ∈ (single e' x + f).support

Tactic:
simp [hx]

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

Goal state before:
pp: case inl
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 : ↑n₁ < ↑n₂ ∧ Ordering.lt = 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✝)

pp: case inr
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 : ↑n₂ ≤ ↑n₁ ∧ (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✝)

Tactic:
· cases nh; contradiction

Goal state after:
case inr
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 : ↑n₂ ≤ ↑n₁ ∧ (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.Notation

Goal state before:
pp: case inr.inr
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
left✝ : ↑n₂ ≤ ↑n₁
nh : ¬↑n₂ < ↑n₁ ∧ 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✝)

Tactic:
· cases nh; contradiction

Goal state after: