mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
⊢ valAux K v O p (f * g) = valAux K v O p f * valAux K v O p g

Tactic:
obtain rfl | hf := eq_or_ne f 0
  · simp
  obtain rfl | hg := eq_or_ne g 0
  · simp
  obtain ⟨m, hm⟩ : ∃ n, coeff n f ≠ 0 := not_forall.1 fun h => hf <| Perfection.ext h
  obtain ⟨n, hn⟩ : ∃ n, coeff n g ≠ 0 := not_forall.1 fun h => hg <| Perfection.ext h
  replace hm := coeff_ne_zero_of_le hm (le_max_left m n)
  replace hn := coeff_ne_zero_of_le hn (le_max_right m n)
  have hfg : coeff (max m n + 1) (f * g) ≠ 0 := by
    rw [map_mul]
    refine ModP.mul_ne_zero_of_pow_p_ne_zero (hv := hv) ?_ ?_
    · rw [coeff_pow_p f]; assumption
    · rw [coeff_pow_p g]; assumption
  rw [valAux_eq hv (coeff_add_ne_zero hm 1),
      valAux_eq hv (coeff_add_ne_zero hn 1), valAux_eq hv hfg]
  rw [map_mul] at hfg ⊢; rw [ModP.preVal_mul hv hfg, mul_pow]

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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
hp : Nat.Prime p
this : Nontrivial (PreTilt O p)
⊢ IsDomain (PreTilt O p)

Tactic:
have : NoZeroDivisors (PreTilt O p) :=
    ⟨fun hfg => by
      simp_rw [← map_eq_zero hv] at hfg ⊢; contrapose! hfg; rw [Valuation.map_mul]
      exact mul_ne_zero hfg.1 hfg.2⟩

Goal state after:
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
hp : Nat.Prime p
this✝ : Nontrivial (PreTilt O p)
this : NoZeroDivisors (PreTilt O p)
⊢ IsDomain (PreTilt O p)
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
⊢ 2 * C ⅟2 = 1

Tactic:
two_mul_C_half_eq_one

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
⊢ 1 = 1
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
⊢ g.degree = ↑(((PowerSeries.map (Ideal.Quotient.mk I)) f).order.lift ⋯)

Tactic:
have : Nontrivial R := _root_.nontrivial_iff.mpr
    ⟨0, PowerSeries.constantCoeff h, ne_of_mem_of_not_mem I.zero_mem notMem⟩
  rw [Polynomial.degree_eq_natDegree distinguish.monic.ne_zero, Nat.cast_inj, ← ENat.natCast_inj,
    ENat.natCast_lift, Eq.comm, PowerSeries.order_eq_nat]
  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]
  constructor
  · simp [mapf, PowerSeries.coeff_X_pow_mul', eq_zero_iff_mem, notMem]
  · intro i hi
    simp [mapf, PowerSeries.coeff_X_pow_mul', hi]

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

Goal state before:
pp: 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
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - C x * X + 1
hφ : φ ≠ 0
y : K
hy : ¬y = 0
⊢ x * y = (y + y⁻¹) * y ↔ y ^ 2 - x * y + 1 = 0

Tactic:
eq_comm,

Goal state after:
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
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - C x * X + 1
hφ : φ ≠ 0
y : K
hy : ¬y = 0
⊢ (y + y⁻¹) * y = x * y ↔ y ^ 2 - x * y + 1 = 0
Module: Mathlib.RingTheory.Polynomial.Morse

Goal state before:
pp: case hS1
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsDomain S
G : Type u_3
inst✝³ : Group G
inst✝² : MulSemiringAction G S
inst✝¹ : SMulCommClass G R S
f : R[X]
hf : (map (algebraMap R S) f).Splits
inst✝ : MulAction.IsPretransitive G ↑(f.rootSet S)
h : ∀ (m : MaximalSpectrum S), (f.rootSet S).ncard ≤ (f.rootSet (S ⧸ m.asIdeal)).ncard + 1
hG : ⨆ m, Ideal.inertia G m.asIdeal = ⊤
σ : G
hσ : σ ∈ ⋃ m, ↑(Ideal.inertia G m.asIdeal)
⊢ (MulAction.toPermHom G ↑(f.rootSet S)) σ = 1 ∨ ((MulAction.toPermHom G ↑(f.rootSet S)) σ).IsSwap

Tactic:
obtain ⟨m, hm⟩ := Set.mem_iUnion.mp hσ

Goal state after:
case hS1
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsDomain S
G : Type u_3
inst✝³ : Group G
inst✝² : MulSemiringAction G S
inst✝¹ : SMulCommClass G R S
f : R[X]
hf : (map (algebraMap R S) f).Splits
inst✝ : MulAction.IsPretransitive G ↑(f.rootSet S)
h : ∀ (m : MaximalSpectrum S), (f.rootSet S).ncard ≤ (f.rootSet (S ⧸ m.asIdeal)).ncard + 1
hG : ⨆ m, Ideal.inertia G m.asIdeal = ⊤
σ : G
hσ : σ ∈ ⋃ m, ↑(Ideal.inertia G m.asIdeal)
m : MaximalSpectrum S
hm : σ ∈ ↑(Ideal.inertia G m.asIdeal)
⊢ (MulAction.toPermHom G ↑(f.rootSet S)) σ = 1 ∨ ((MulAction.toPermHom G ↑(f.rootSet S)) σ).IsSwap
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)) φ

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

Goal state after:
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
⊢ (aeval fun n ↦ ↑(s.equivFin.symm n)).range = Algebra.adjoin R ↑s

Tactic:
← Algebra.adjoin_range_eq_range_aeval

Goal state after:
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
⊢ Algebra.adjoin R (Set.range fun n ↦ ↑(s.equivFin.symm n)) = Algebra.adjoin R ↑s
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 θ)
⊢ f.toFun' (RingCon.ker ↑ψ).Quotient
      ((rTensor M
          ((↑(quotientKerEquivRangeₐ ψ).symm).comp
              (h'.comp ((↑(quotientKerEquivRangeₐ φ)).comp (mkₐ R (RingCon.ker ↑φ))))).toLinearMap)
        p) =
    f.toFun' (RingCon.ker ↑ψ).Quotient ((rTensor M (mkₐ R (RingCon.ker ↑ψ)).toLinearMap) q)

Tactic:
rw [quotientKerEquivRangeₐ_comp_mkₐ, comp_toLinearMap,
    rTensor_comp_apply, hpq, ← rTensor_comp_apply, ← comp_toLinearMap,
    ← quotientKerEquivRangeₐ_comp_mkₐ, ← AlgHom.comp_assoc]

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 θ)
⊢ f.toFun' (RingCon.ker ↑ψ).Quotient
      ((rTensor M
          (((↑(quotientKerEquivRangeₐ ψ).symm).comp ↑(quotientKerEquivRangeₐ ψ)).comp
              (mkₐ R (RingCon.ker ↑ψ))).toLinearMap)
        q) =
    f.toFun' (RingCon.ker ↑ψ).Quotient ((rTensor M (mkₐ R (RingCon.ker ↑ψ)).toLinearMap) q)
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⁻¹
⊢ (coeff i) (↑((trunc n) g) * s₁ * ↑⋯.unit⁻¹) ∈ I ^ (k + 1)

Tactic:
pow_succ'

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⁻¹
⊢ (coeff i) (↑((trunc n) g) * s₁ * ↑⋯.unit⁻¹) ∈ I * I ^ k
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case inl
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
heq :
  ((X ^ ((map (Ideal.Quotient.mk I)) g).order.toNat *
          mk fun i ↦ (coeff (i + ((map (Ideal.Quotient.mk I)) g).order.toNat)) g) +
        ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g)) *
      q =
    ↑r
k : ℕ
ih : ∀ (i : ℕ), (coeff i) q ∈ I ^ k
i : ℕ
hi : i < ((map (Ideal.Quotient.mk I)) g).order.toNat
⊢ (coeff i)
      (((X ^ ((map (Ideal.Quotient.mk I)) g).order.toNat *
            mk fun i ↦ (coeff (i + ((map (Ideal.Quotient.mk I)) g).order.toNat)) g) +
          ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g)) *
        q) ∈
    I ^ (k + 1)

Tactic:
pow_succ'

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

Tactic:
pow_succ'

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) (↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g) * q) ∈ I * 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
inst✝ : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
heq : g * q = ↑r
k : ℕ
⊢ ∀ (i : ℕ), (coeff i) q ∈ I ^ k

Tactic:
induction k with
  | zero => simp
  | succ k ih =>
    rw [g.eq_X_pow_mul_shift_add_trunc (g.map (Ideal.Quotient.mk I)).order.toNat] at heq
    have h1 : ∀ i, coeff i r ∈ I ^ (k + 1) := fun i ↦ by
      rcases lt_or_ge i (g.map (Ideal.Quotient.mk I)).order.toNat with hi | hi
      · rw [← heq, pow_succ']
        refine coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal i (fun j hj ↦ ?_)
          (fun j _ ↦ ih j) i le_rfl
        rw [map_add, Polynomial.coeff_coe]
        refine Ideal.add_mem _ ?_ (g.coeff_trunc_order_mem I j)
        simp_rw [coeff_X_pow_mul', if_neg (lt_of_le_of_lt hj hi).not_ge, zero_mem]
      simp_rw [Polynomial.coeff_coe,
        Polynomial.coeff_eq_zero_of_degree_lt (lt_of_lt_of_le hdeg (by simpa)), zero_mem]
    rw [add_mul, mul_comm (X ^ _), ← eq_sub_iff_add_eq] at heq
    replace heq := congr(H.isUnit_shift.unit⁻¹ * $heq)
    rw [← mul_assoc, ← mul_assoc, IsUnit.val_inv_mul, one_mul] at heq
    intro i
    rw [← coeff_X_pow_mul _ (g.map (Ideal.Quotient.mk I)).order.toNat i, heq]
    refine coeff_mul_mem_ideal_of_coeff_right_mem_ideal' (fun i ↦ ?_) _
    rw [map_sub]
    refine Ideal.sub_mem _ (h1 _) ?_
    rw [pow_succ']
    refine coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal' (fun i ↦ ?_) ih _
    simp_rw [Polynomial.coeff_coe, g.coeff_trunc_order_mem]

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) := M.smulShortComplex x
hS : S.ShortExact
h : HasProjectiveDimensionLE (of R (QuotSMulTop x ↑M)) (n + 1)
L : ModuleCat R
a✝ : Module.Finite R ↑L
zero : Subsingleton (Ext (of R (QuotSMulTop x ↑M)) L (n + 2))
exac :
  { X₁ := AddCommGrpCat.of (Ext S.X₂ L (n + 1)), X₂ := AddCommGrpCat.of (Ext S.X₁ L (n + 1)),
      X₃ := AddCommGrpCat.of (Ext S.X₃ L (n + 2)), f := AddCommGrpCat.ofHom ((Ext.mk₀ S.f).precomp L ⋯),
      g := AddCommGrpCat.ofHom (hS.extClass.precomp L ⋯), zero := ⋯ }.Exact
this✝ : S.f = x • 𝟙 M
epi : Function.Surjective ⇑((Ext.mk₀ (x • 𝟙 M)).precomp L ⋯)
ntr : Nontrivial (Ext M L (n + 1))
this : x ∈ (annihilator R (Ext M L (n + 1))).jacobson
⊢ ⊤ = x • ⊤

Tactic:
eq_comm,

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
zero : Subsingleton (Ext (of R (QuotSMulTop x ↑M)) L (n + 2))
exac :
  { X₁ := AddCommGrpCat.of (Ext S.X₂ L (n + 1)), X₂ := AddCommGrpCat.of (Ext S.X₁ L (n + 1)),
      X₃ := AddCommGrpCat.of (Ext S.X₃ L (n + 2)), f := AddCommGrpCat.ofHom ((Ext.mk₀ S.f).precomp L ⋯),
      g := AddCommGrpCat.ofHom (hS.extClass.precomp L ⋯), zero := ⋯ }.Exact
this✝ : S.f = x • 𝟙 M
epi : Function.Surjective ⇑((Ext.mk₀ (x • 𝟙 M)).precomp L ⋯)
ntr : Nontrivial (Ext M L (n + 1))
this : x ∈ (annihilator R (Ext M L (n + 1))).jacobson
⊢ x • ⊤ = ⊤
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
hI : I ≠ ⊤
⊢ f.natDegree = ((map (Ideal.Quotient.mk I)) g).order.toNat

Tactic:
rw [Polynomial.natDegree, H.degree_eq_coe_lift_order_map_of_ne_top hI,
    ENat.lift_eq_toNat_of_lt_top]

Goal state after:
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
hI : I ≠ ⊤
⊢ WithBot.unbotD 0 ↑((map (Ideal.Quotient.mk I)) g).order.toNat = ((map (Ideal.Quotient.mk I)) g).order.toNat
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: case refine_2
R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
m : Submodule R M
h : m.IsFullyInvariant
⊢ m = sSup (Subtype.val '' OrderIso.setIsotypicComponents.symm ⟨m, h⟩)

Tactic:
convert! Subtype.ext_iff.mp (OrderIso.setIsotypicComponents.right_inv ⟨m, h⟩).symm

Goal state after:
R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
m : Submodule R M
h : m.IsFullyInvariant
⊢ sSup (Subtype.val '' OrderIso.setIsotypicComponents.symm ⟨m, h⟩) =
    ↑(OrderIso.setIsotypicComponents.toFun (OrderIso.setIsotypicComponents.invFun ⟨m, h⟩))
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: case h
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 ∈ f.ker ⊓ I • ⊤
y : TensorProduct R (↥I) M
hy : (↑(TensorProduct.lid R M) ∘ₗ rTensor M (Submodule.subtype I)) y = x
inj : Function.Injective ⇑(↑(TensorProduct.lid R N) ∘ₗ rTensor N (Submodule.subtype I))
comm1 :
  (↑(TensorProduct.lid R N) ∘ₗ rTensor N (Submodule.subtype I)) ∘ₗ lTensor (↥I) f =
    f ∘ₗ ↑(TensorProduct.lid R M) ∘ₗ rTensor M (Submodule.subtype I)
eq0 : (lTensor (↥I) f) y = 0
z : TensorProduct R ↥I ↥f.ker
hz : (lTensor (↥I) f.ker.subtype) z = y
comm2 :
  (↑(TensorProduct.lid R M) ∘ₗ rTensor M (Submodule.subtype I)) ∘ₗ lTensor (↥I) f.ker.subtype =
    f.ker.subtype ∘ₗ ↑(TensorProduct.lid R ↥f.ker) ∘ₗ rTensor (↥f.ker) (Submodule.subtype I)
⊢ f.ker.subtype ((↑(TensorProduct.lid R ↥f.ker) ∘ₗ rTensor (↥f.ker) (Submodule.subtype I)) z) = f.ker.subtype ⟨x, ⋯⟩

Tactic:
rw [← LinearMap.comp_apply, ← comm2, LinearMap.comp_apply, hz, hy, Submodule.subtype_apply]

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, a = ↑p ^ m * ↑b

Tactic:
by
  obtain ⟨m, b, h₁, h₂⟩ := exists_eq_pow_p_mul a ha
  let b₀ := Units.mk0 (b.coeff 0) h₁
  have hb₀ : b.coeff 0 = b₀ := rfl
  exact ⟨m, mkUnit hb₀, h₂⟩

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ↑p ^ (n + 1) * polyOfInterest p n = remainder p n - wittPolyProdRemainder p (n + 1)

Tactic:
by
  simp only [polyOfInterest, mul_sub, mul_add, sub_eq_iff_eq_add']
  rw [mul_polyOfInterest_aux4 p n]
  ring

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

Goal state before:
pp: case refine_1.inr
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
o : Ordinal.{u}
h : lfpApprox f x o = x
ho : o ≠ 0
⊢ f x = x ∨ o = 0

Tactic:
· have hpos : (0 : Ordinal) < o :=
        zero_lt_one.trans_le (one_le_iff_ne_zero.mpr ho)
      have hmem : lfpApprox f x 0 ∈ fixedPoints f :=
        lfpApprox_mem_fixedPoints_of_eq f hx hpos (le_refl _)
          ((lfpApprox_zero f).trans h.symm)
      have hfx : f x = x :=
        (mem_fixedPoints_iff.mp (by simpa [lfpApprox_zero] using hmem))
      exact Or.inl hfx

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

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

Tactic:
cases nh : cmpUsing (· < ·) (n₁ : ℕ) n₂

Goal state after:
case lt
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
nh : cmpUsing (fun x1 x2 ↦ x1 < x2) ↑n₁ ↑n₂ = Ordering.lt
⊢ (Ordering.eq.then (Ordering.lt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)

case eq
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
nh : cmpUsing (fun x1 x2 ↦ x1 < x2) ↑n₁ ↑n₂ = Ordering.eq
⊢ (Ordering.eq.then (Ordering.eq.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)

case gt
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
nh : cmpUsing (fun x1 x2 ↦ x1 < x2) ↑n₁ ↑n₂ = Ordering.gt
⊢ (Ordering.eq.then (Ordering.gt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u_1}
a : Ordinal.{u_1} × Ordinal.{u_1}
ha : a ∈ CNF b o
x : Ordinal.{u_1}
⊢ b ^ a.1 * (coeff b o) a.1 + x = b ^ a.1 * a.2 + x

Tactic:
rw [coeff_of_mem_CNF ha]

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

Goal state before:
pp: n : ℕ
f : (Fin n → ZFSet.{u}) → ZFSet.{u}
inst✝ : Definable n f
xs ys : Fin n → PSet.{u}
h : ∀ (i : Fin n), xs i ≈ ys i
⊢ (f fun x ↦ ZFSet.mk (xs x)) = ZFSet.mk (out f ys)

Tactic:
mk_out

Goal state after:
n : ℕ
f : (Fin n → ZFSet.{u}) → ZFSet.{u}
inst✝ : Definable n f
xs ys : Fin n → PSet.{u}
h : ∀ (i : Fin n), xs i ≈ ys i
⊢ (f fun x ↦ ZFSet.mk (xs x)) = f fun x ↦ ZFSet.mk (ys x)
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x y z : ZFSet.{u_1}
⊢ {x} = {y, z} ↔ x = y ∧ x = z

Tactic:
eq_comm,

Goal state after:
x y z : ZFSet.{u_1}
⊢ {y, z} = {x} ↔ x = y ∧ x = z
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: case mk.mk
α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ b, (A a).Equiv (B b)
a : (PSet.mk α A).Type
c : ((PSet.mk α A).Func a).Type
b : β
hb : (A a).Equiv (B b)
γ : Type u
Γ : γ → PSet.{u}
A_ih✝¹ : ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
ea : A a = PSet.mk γ Γ
δ : Type u
Δ : δ → PSet.{u}
A_ih✝ : ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
eb : B b = PSet.mk δ Δ
⊢ ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)

Tactic:
| _ δ Δ
     => 

Goal state after:
case mk.mk
α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ b, (A a).Equiv (B b)
a : (PSet.mk α A).Type
c : ((PSet.mk α A).Func a).Type
b : β
hb : (A a).Equiv (B b)
γ : Type u
Γ : γ → PSet.{u}
A_ih✝¹ : ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
ea : A a = PSet.mk γ Γ
δ : Type u
Δ : δ → PSet.{u}
A_ih✝ : ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
eb : B b = PSet.mk δ Δ
⊢ ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)