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

Goal state before:
pp: T : Type u_2
S : Type u_3
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a b c : T
x1 x2 : S
haroots : (C a * X ^ 2 + C b * X + C c).aroots S = {x1, x2}
⊢ (algebraMap T S) c = (algebraMap T S) a * x1 * x2

Tactic:
by
  rw [aroots_def, show map (algebraMap T S) (C a * X ^ 2 + C b * X + C c) = C ((algebraMap T S) a) *
    X ^ 2 + C ((algebraMap T S) b) * X + C ((algebraMap T S) c) by simp] at haroots
  exact eq_mul_mul_of_roots_quadratic_eq_pair haroots

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
r a b : R
f✝ g f : M →ₚₗ[R] N
⊢ 0 • f = 0

Tactic:
by simp_rw [HSMul.hSMul, SMul.smul]; simp only [Nat.cast_zero, zero_smul f]

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 (h.comp (φ.range.val.comp ((↑(quotientKerEquivRangeₐ φ)).comp (mkₐ R (RingCon.ker ↑φ))))).toLinearMap)
      (f.toFun' A p) =
    (rTensor N (ψ.range.val.comp ψ.rangeRestrict).toLinearMap) (f.toFun' B q)

Tactic:
← quotientKerEquivRangeₐ_comp_mkₐ ψ,

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 (h.comp (φ.range.val.comp ((↑(quotientKerEquivRangeₐ φ)).comp (mkₐ R (RingCon.ker ↑φ))))).toLinearMap)
      (f.toFun' A p) =
    (rTensor N (ψ.range.val.comp ((↑(quotientKerEquivRangeₐ ψ)).comp (mkₐ R (RingCon.ker ↑ψ)))).toLinearMap)
      (f.toFun' B q)
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: z : ℤ
⊢ radical z = ↑(∏ p ∈ z.natAbs.primeFactors, p)

Tactic:
← radical_natAbs_eq_radical,

Goal state after:
z : ℤ
⊢ ↑(radical z.natAbs) = ↑(∏ p ∈ z.natAbs.primeFactors, p)
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: z : ℤ
⊢ 0 < radical z

Tactic:
← radical_natAbs_eq_radical,

Goal state after:
z : ℤ
⊢ 0 < ↑(radical z.natAbs)
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: z : ℤ
⊢ 1 < radical z ↔ 1 < z.natAbs

Tactic:
← radical_natAbs_eq_radical,

Goal state after:
z : ℤ
⊢ 1 < ↑(radical z.natAbs) ↔ 1 < z.natAbs
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
S : Type v
inst✝³ : CommSemiring S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
A : Subalgebra R T
φ : S →ₐ[R] T
hφ : A ≤ φ.range
t : T ⊗[R] M
u : ↥A ⊗[R] M
hu : (rTensor M A.val.toLinearMap) u = t
⊢ ∃ s, (rTensor M φ.toLinearMap) s = t

Tactic:
suffices h_surj : Function.Surjective ((φ.rangeRestrict.toLinearMap).rTensor M) by
    obtain ⟨p, hp⟩ := h_surj ((Subalgebra.inclusion hφ).toLinearMap.rTensor M u)
    use p
    rw [← hu, ← Subalgebra.val_comp_inclusion hφ, comp_toLinearMap, rTensor_comp,
      LinearMap.comp_apply, ← hp, ← LinearMap.comp_apply, ← rTensor_comp, ← comp_toLinearMap]
    simp

Goal state after:
R : Type u
inst✝⁶ : CommSemiring R
M : Type u_1
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type v
inst✝³ : CommSemiring S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
A : Subalgebra R T
φ : S →ₐ[R] T
hφ : A ≤ φ.range
t : T ⊗[R] M
u : ↥A ⊗[R] M
hu : (rTensor M A.val.toLinearMap) u = t
⊢ Function.Surjective ⇑(rTensor M φ.rangeRestrict.toLinearMap)
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
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ Function.Surjective (π R M S)

Tactic:
intro t
  obtain ⟨B : Subalgebra R S, hB : B.FG, ht : t ∈ range _⟩ := TensorProduct.Algebra.exists_of_fg t
  obtain ⟨s : Finset S, hs : (PolynomialLaw.φ R s).range = B⟩ := exists_range_φ_eq_of_fg hB
  obtain ⟨p, hp⟩ := exists_lift_of_mem_range_rTensor B (le_of_eq hs.symm) ht
  exact ⟨⟨s, p⟩, hp⟩

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : Ideal R
hp : p.IsPrime
eqbot : p = ⊥
this : Field (Localization.AtPrime p) := ⋯.toField
⊢ IsRegularLocalRing (Localization.AtPrime p)

Tactic:
infer_instance

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : Ideal R
hp : p.IsPrime
eqbot : ¬p = ⊥
this : IsDiscreteValuationRing (Localization.AtPrime p)
⊢ IsRegularLocalRing (Localization.AtPrime p)

Tactic:
infer_instance

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
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 : ↥(φ R s).range), (h.comp (φ R s).range.val) x ∈ (φ R s').range

Tactic:
by
    rintro ⟨x, hx⟩
    simp only [range_φ] at hx ⊢
    simp only [AlgHom.coe_comp, Subalgebra.coe_val, Function.comp_apply, Finset.coe_image,
      Algebra.adjoin_image, s']
    exact ⟨x, hx, rfl⟩

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
T : Type w
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
⊢ (rTensor N h.toLinearMap) (toFun S f t) = toFun T f ((rTensor M h.toLinearMap) t)

Tactic:
classical
  obtain ⟨⟨s, p⟩, ha⟩ := π_surjective t
  let s' := s.image h
  let h' : (φ R s).range →ₐ[R] (φ R s').range :=
    (h.comp (Subalgebra.val _)).codRestrict (φ R s').range (by
    rintro ⟨x, hx⟩
    simp only [range_φ] at hx ⊢
    simp only [AlgHom.coe_comp, Subalgebra.coe_val, Function.comp_apply, Finset.coe_image,
      Algebra.adjoin_image, s']
    exact ⟨x, hx, rfl⟩)
  let j : Fin s.card → Fin s'.card :=
    (s'.equivFin) ∘ (fun ⟨x, hx⟩ ↦ ⟨h x, Finset.mem_image_of_mem h hx⟩) ∘ (s.equivFin).symm
  have eq_h_comp : (φ R s').comp (rename j) = h.comp (φ R s) := by
    ext p
    simp only [φ, AlgHom.comp_apply, aeval_rename, comp_aeval]
    congr
    ext n
    simp only [Function.comp_apply, Equiv.symm_apply_apply, j]
  let p' := rTensor M (rename j).toLinearMap p
  have ha' : π R M T (⟨s', p'⟩ : lifts R M T) = rTensor M h.toLinearMap t := by
    simp only [← ha, π, p', ← LinearMap.comp_apply, ← rTensor_comp, ← comp_toLinearMap, eq_h_comp]
  rw [toFun_eq_rTensor_φ_toFun' f ha, toFun_eq_rTensor_φ_toFun' f ha', ← LinearMap.comp_apply,
    ← rTensor_comp, ← comp_toLinearMap]
  apply toFun'_eq_of_diagram f p p' h h'
  · simp only [val_comp_codRestrict, h']
  · simp only [p', ← LinearMap.comp_apply, ← rTensor_comp, ← comp_toLinearMap]
    congr
    ext n
    simp only [AlgHom.coe_comp, Function.comp_apply, coe_codRestrict,
      Subalgebra.coe_val, rename_X, h', j]
    simp only [φ, aeval_X, Equiv.symm_apply_apply]

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
mem : x ∈ maximalIdeal R
sub : Subsingleton ↑M ↔ Subsingleton (QuotSMulTop x ↑M)
n : ℕ
h : Module.Projective R (QuotSMulTop x ↑M)
this✝ : Free R (QuotSMulTop x ↑M)
ntr : Nontrivial (QuotSMulTop x ↑M)
this : x = 0
reg : Subsingleton ↑M
⊢ Subsingleton (QuotSMulTop x ↑M)

Tactic:
infer_instance

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
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H1 : r.degree < ↑n
H2 : 1 = (IsLocalRing.residue A) ((coeff (n, 0).1) g) * (IsLocalRing.residue A) (constantCoeff q)
⊢ IsUnit ((IsLocalRing.residue A) (constantCoeff q))

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
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H1 : r.degree < ↑n
H2 :
  1 =
    ∑ p ∈ Finset.antidiagonal n,
      (coeff p.1) ((map (IsLocalRing.residue A)) g) * (coeff p.2) ((map (IsLocalRing.residue A)) q)
p : ℕ × ℕ
hp : p ∈ Finset.antidiagonal n
hnotMem : p ∉ {(n, 0)}
⊢ (coeff p.1) ((map (IsLocalRing.residue A)) g) * (coeff p.2) ((map (IsLocalRing.residue A)) q) = 0

Tactic:
mul_comm

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
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H1 : r.degree < ↑n
H2 : 1 = (IsLocalRing.residue A) (constantCoeff q) * (IsLocalRing.residue A) ((coeff (n, 0).1) g)
⊢ IsUnit ((IsLocalRing.residue A) (constantCoeff q))

A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H1 : r.degree < ↑n
H2 :
  1 =
    ∑ p ∈ Finset.antidiagonal n,
      (coeff p.1) ((map (IsLocalRing.residue A)) g) * (coeff p.2) ((map (IsLocalRing.residue A)) q)
p : ℕ × ℕ
hp : p ∈ Finset.antidiagonal n
hnotMem : p ∉ {(n, 0)}
⊢ (coeff p.1) ((map (IsLocalRing.residue A)) g) * (coeff p.2) ((map (IsLocalRing.residue A)) q) = 0
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R₀ : Type u_1
R : Type u_2
M : Type u
N : Type u_3
S : Type u_4
inst✝⁹ : CommSemiring R₀
inst✝⁸ : Ring R
inst✝⁷ : Algebra R₀ R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R S
inst✝ : IsSemisimpleModule R S
⊢ IsSemisimpleModule R ↥(isotypicComponent R M S)

Tactic:
rw [isotypicComponent, sSup_eq_iSup]

Goal state after:
R₀ : Type u_1
R : Type u_2
M : Type u
N : Type u_3
S : Type u_4
inst✝⁹ : CommSemiring R₀
inst✝⁸ : Ring R
inst✝⁷ : Algebra R₀ R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R S
inst✝ : IsSemisimpleModule R S
⊢ IsSemisimpleModule R ↥(⨆ a ∈ {m | Nonempty (↥m ≃ₗ[R] S)}, a)
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R₀ : Type u_1
R : Type u_2
M : Type u
N : Type u_3
S : Type u_4
inst✝⁹ : CommSemiring R₀
inst✝⁸ : Ring R
inst✝⁷ : Algebra R₀ R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R S
inst✝ : IsSemisimpleModule R S
m : Submodule R M
x✝ : m ∈ {m | Nonempty (↥m ≃ₗ[R] S)}
e : ↥m ≃ₗ[R] S
this : IsSemisimpleModule R ↥m
⊢ IsSemisimpleModule R ↥m

Tactic:
infer_instance

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R₀ : Type u_1
R : Type u_2
M : Type u
N : Type u_3
S✝ : Type u_4
inst✝⁸ : CommSemiring R₀
inst✝⁷ : Ring R
inst✝⁶ : Algebra R₀ R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup S✝
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R S✝
S : Submodule R M
left✝ : IsSimpleModule R ↥S
⊢ IsSemisimpleModule R ↥↑⟨isotypicComponent R M ↥S, ⋯⟩

Tactic:
infer_instance

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
left✝ : IsSimpleModule R ↥S
s : Set (Submodule R M) := isotypicComponents R M \ {isotypicComponent R M ↥S}
ne : ¬isotypicComponent R M ↥S ⊓ sSup s = ⊥
⊢ IsSemisimpleModule R ↥(isotypicComponent R M ↥S)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
c : Submodule R M
hc : c ∈ isotypicComponents R M
s : Set (Submodule R M) := isotypicComponents R M \ {c}
ne : ¬c ⊓ sSup s = ⊥
this✝ : IsSemisimpleModule R ↥c
this : IsSemisimpleModule R ↥(c ⊓ sSup s)
w✝ : Submodule R M
left✝ : IsSimpleModule R ↥w✝
right✝ : isotypicComponent R M ↥w✝ ∉ {c}
⊢ IsSemisimpleModule R ↥↑⟨isotypicComponent R M ↥w✝, ⋯⟩

Tactic:
infer_instance

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

Goal state before:
pp: case of_equiv
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularRing R
ι : Type u_2
inst✝ : Finite ι
α✝ β✝ : Type u_2
e : α✝ ≃ β✝
H : IsRegularRing (MvPolynomial α✝ R)
⊢ IsRegularRing (MvPolynomial β✝ R)

Tactic:
| of_equiv e H =>

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

Goal state before:
pp: case h_empty
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularRing R
ι : Type u_2
inst✝ : Finite ι
⊢ IsRegularRing (MvPolynomial PEmpty.{u_2 + 1} R)

Tactic:
| h_empty =>

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∑ i ∈ range (n + 1), ↑p ^ i * wittMul p i ^ p ^ (n - i) = wittPolyProd p n

Tactic:
simp only [wittPolyProd]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∑ i ∈ range (n + 1), ↑p ^ i * wittMul p i ^ p ^ (n - i) =
    (rename (Prod.mk 0)) (wittPolynomial p ℤ n) * (rename (Prod.mk 1)) (wittPolynomial p ℤ n)
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
⊢ (succNthDefiningPoly p n a₁ a₂ bs).degree = ↑p

Tactic:
have : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1)) - X * C (a₂.coeff 0 ^ p ^ (n + 1))).degree =
      (p : WithBot ℕ) := by
    rw [degree_sub_eq_left_of_degree_lt, this]
    rw [this, degree_mul, degree_C, degree_X, add_zero]
    · exact mod_cast hp.out.one_lt
    · exact pow_ne_zero _ ha₂

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
this : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1)) - X * C (a₂.coeff 0 ^ p ^ (n + 1))).degree = ↑p
⊢ (succNthDefiningPoly p n a₁ a₂ bs).degree = ↑p
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (polyOfInterest p n).vars ⊆ univ ×ˢ range (n + 1)

Tactic:
by
  rw [polyOfInterest_vars_eq]; apply mul_polyOfInterest_vars

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: case refine_2
α : Type v
inst✝ : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
f : (x : Set α) → x ∈ s → Set α
hf : ∀ (x : Set α) (_ : x ∈ s), IsClub (f x _)
hxf : ∀ (x : Set α) (_ : x ∈ s), Disjoint x (f x _)
⊢ Disjoint (⋃₀ s) (⋂ x, f ↑x ⋯)

Tactic:
rw [disjoint_sUnion_left]
      exact fun x hx ↦ (hxf _ hx).mono_right (iInter_subset _ ⟨x, hx⟩)

Goal state after:
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: case inr
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : z.length ≤ x.length
⊢ z ∈ pullSub (pullSub T y) x ↔ z ∈ pullSub T (x ++ y)

Tactic:
· rw [mem_pullSub_short hl, mem_pullSub_short (by simp), mem_pullSub_short (by simp; lia)]
    simpa using fun _ ↦ (z.isPrefix_append_of_length hl).symm

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: case refine_2
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #↑s < cof α
f : (x : Set α) → x ∈ s → Set α
hf : ∀ (x : Set α) (_ : x ∈ s), IsClub (f x _)
hxf : ∀ (x : Set α) (_ : x ∈ s), Disjoint x (f x _)
⊢ Disjoint (⋃₀ s) (⋂ x, f ↑x ⋯)

Tactic:
rw [disjoint_sUnion_left]
      exact fun x hx ↦ (hxf _ hx).mono_right (iInter_subset _ ⟨x, hx⟩)

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

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

Tactic:
refine CNF.rec b ?_ (fun o ho H ↦ ?_) o
  · simp
  · rw [CNF.ne_zero ho, mem_cons]
    rintro (rfl | h)
    · rfl
    · exact (H h).trans (log_mono_right _ (mod_opow_log_lt_self b ho).le)

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
C : Lists α → Sort u_2
D : Lists' α true → Sort u_3
C0 : (a : α) → C (atom a)
C1 : (l : Lists' α true) → D l → C (of' l)
D0 : D Lists'.nil
D1 : (a : Lists α) → (l : Lists' α true) → C a → D l → D (Lists'.cons a l)
b : Bool
l : Lists' α b
⊢ C ⟨b, l⟩ ×'
    match b, l with
    | true, l => D l
    | false, x => PUnit

Tactic:
induction l with
  | atom => exact ⟨C0 _, ⟨⟩⟩
  | nil => exact ⟨C1 _ D0, D0⟩
  | cons' a l IH₁ IH =>
    have : D (Lists'.cons' a l) := D1 ⟨_, _⟩ _ IH₁.1 IH.2
    exact ⟨C1 _ this, this⟩

Goal state after:
Module: Mathlib.Topology.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : IsNormal f
⊢ Continuous f

Tactic:
rw [OrderTopology.continuous_iff]
  refine fun b ↦ ⟨?_, ((isLowerSet_Iio b).preimage hf.strictMono.monotone).isOpen⟩
  rw [← isClosed_compl_iff, ← Set.preimage_compl, Set.compl_Ioi]
  obtain ha | ⟨a, ha⟩ := ((isLowerSet_Iic b).preimage hf.strictMono.monotone).eq_univ_or_Iio
  · exact ha ▸ isClosed_univ
  · obtain h | h := (f ⁻¹' Iic b).eq_empty_or_nonempty
    · exact h ▸ isClosed_empty
    · have : Nonempty α := ⟨a⟩
      have : Nonempty β := ⟨b⟩
      rw [hf.preimage_Iic h (ha ▸ bddAbove_Iio)]
      exact isClosed_Iic

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

Goal state before:
pp: b : Ordinal.{u_1}
f₁ f₂ : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e₁ ∈ f₁.support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁
⊢ eval b (f₁ + f₂) = eval b f₁ + eval b f₂

Tactic:
induction f₁ using Finsupp.induction_on_max with
  | zero => simp
  | single_add e₁ x f₁ hf₁ hx IH =>
    rw [add_assoc, eval_single_add, eval_single_add' _ hf₁, IH, add_assoc]
    · simp_all
    · intro e₂ he₂
      obtain he₂ | he₂ := Finset.mem_union.1 <| support_add he₂
      · exact (hf₁ _ he₂).le
      · apply h _ _ _ he₂
        simp_all

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

Goal state before:
pp: ⊢ (↑1).NF

Tactic:
infer_instance

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

Goal state before:
pp: case neg
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
a : Ordinal.{u_1}
ha : a ∉ f.support
⊢ f a < b

Tactic:
· rw [notMem_support_iff.1 ha]
        exact (hb 0).pos

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

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

Tactic:
exact (CNF.sortedGT b o).nodup

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

Goal state before:
pp: o : Ordinal.{u_1}
S : Set (Set Ordinal.{u_1})
h : ∀ C ∈ S, IsClosedBelow C o
⊢ IsClosedBelow (⋂₀ S) o

Tactic:
rw [isClosedBelow_iff]

Goal state after:
o : Ordinal.{u_1}
S : Set (Set Ordinal.{u_1})
h : ∀ C ∈ S, IsClosedBelow C o
⊢ ∀ p < o, p.IsAcc (⋂₀ S) → p ∈ ⋂₀ S
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case zero
b : ONote
⊢ Decidable
    (match zero with
    | zero => True
    | e.oadd a a_1 => e.cmp b = Ordering.lt)

Tactic:
infer_instance

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

Goal state before:
pp: case oadd
b a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
⊢ Decidable
    (match a✝².oadd a✝¹ a✝ with
    | zero => True
    | e.oadd a a_1 => e.cmp b = Ordering.lt)

Tactic:
infer_instance

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

Goal state before:
pp: case a
x : PSet.{u_1}
⊢ ∀ ⦃y : PSet.{u_1}⦄, y ⊆ x → y.rank ≤ x.rank

Tactic:
intro

Goal state after:
case a
x y✝ : PSet.{u_1}
⊢ y✝ ⊆ x → y✝.rank ≤ x.rank
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case inl
x : Ordinal.{u_1}
h : x.invVeblen₁ = 0
⊢ x.invVeblen₂ ≤ x

Tactic:
invVeblen₂_le_iff,

Goal state after:
case inl
x : Ordinal.{u_1}
h : x.invVeblen₁ = 0
⊢ ω ^ x ≤ veblen x.invVeblen₁ x
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case a
x y : ZFSet.{u_1}
⊢ ∀ ⦃y_1 : ZFSet.{u_1}⦄, y_1 ∈ x ∨ y_1 ∈ y → y_1.rank < x.rank ∨ y_1.rank < y.rank

Tactic:
intro

Goal state after:
case a
x y y✝ : ZFSet.{u_1}
⊢ y✝ ∈ x ∨ y✝ ∈ y → y✝.rank < x.rank ∨ y✝.rank < y.rank
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: A : Class.{u_1}
x : ZFSet.{u_1}
H : ∀ (y : ZFSet.{u_1}), A y ↔ y = x
y : ZFSet.{u_1}
x✝ : A.iota y
x' : ZFSet.{u_1}
h : {x | ∀ (y : ZFSet.{u_1}), A y ↔ y = x} x'
yx' : y ∈ ↑x'
⊢ ↑x y

Tactic:
rwa [← (H x').1 <| (h x').2 rfl]

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

Goal state before:
pp: x y : ZFSet.{u}
hx : x.IsTransitive
hy : y.IsTransitive
⊢ ∀ y_1 ∈ {x, y}, y_1.IsTransitive

Tactic:
intro

Goal state after:
x y : ZFSet.{u}
hx : x.IsTransitive
hy : y.IsTransitive
y✝ : ZFSet.{u}
⊢ y✝ ∈ {x, y} → y✝.IsTransitive
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: case neg
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 ↦ x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hxy : x ⊆ y
hyx : ¬y ⊆ x
⊢ x = y ∨ x ∈ y

Tactic:
obtain ⟨m, hm, hm'⟩ := mem_wf.has_min (y \ x) (Set.sdiff_nonempty.2 hyx)
      have hmy : m ∈ y := by simp only [Set.mem_sdiff, SetLike.mem_coe] at hm; exact hm.1
      have hmx : m ⊆ x := by
        intro z hzm
        by_contra hzx
        exact hm' _ ⟨hy.mem_trans hzm hmy, hzx⟩ hzm
      obtain rfl | H := IH m x (Sym2.GameAdd.fst_snd hmy) (hy.mem hmy) hx hmx
      · exact Or.inr hmy
      · cases Set.notMem_of_mem_sdiff hm H

Goal state after: