mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case h₀.inr
R : Type u
inst✝ : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ antidiagonal (df + dg)
hne : (df', dg') ≠ (df, dg)
hdf' : df' ≤ df
⊢ f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0

Tactic:
obtain h | hdg' := lt_or_ge dg dg'

Goal state after:
case h₀.inr.inl
R : Type u
inst✝ : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ antidiagonal (df + dg)
hne : (df', dg') ≠ (df, dg)
hdf' : df' ≤ df
h : dg < dg'
⊢ f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0

case h₀.inr.inr
R : Type u
inst✝ : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ antidiagonal (df + dg)
hne : (df', dg') ≠ (df, dg)
hdf' : df' ≤ df
hdg' : dg' ≤ dg
⊢ f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0
Module: Mathlib.Algebra.Polynomial.Monomial

Goal state before:
pp: case mpr
R : Type u
inst✝ : Semiring R
f : R[X]
⊢ (∃ n a, f = (monomial n) a) → f.support.card ≤ 1

Tactic:
rintro ⟨n, a, rfl⟩
    rw [← Finset.card_singleton n]
    apply Finset.card_le_card
    exact support_monomial_subset _ _

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
p q : R[X]
inst✝ : CommSemiring S
f : R →+* S
k : ℕ
t : S
⊢ eval₂ f t (p.comp^[k] q) = (fun x ↦ eval₂ f x p)^[k] (eval₂ f t q)

Tactic:
by
  induction k with
  | zero => simp
  | succ k IH => rw [Function.iterate_succ_apply', Function.iterate_succ_apply', eval₂_comp, IH]

Goal state after:
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
A : Type z
B : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
n : ℕ
⊢ ↑R (lcoeff B n) ∘ₗ (mapAlgHom f).toLinearMap = f.toLinearMap ∘ₗ ↑R (lcoeff A n)

Tactic:
by
  ext f; simp

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: case inr
α : Type u_5
M : Type u_6
N : Type u_7
inst✝³ : Zero M
inst✝² : AddCommMonoid N
inst✝¹ : PartialOrder N
inst✝ : IsOrderedAddMonoid N
f : α →₀ M
g : α → M → N
h : 0 ≤ fun x1 x2 ↦ g x1 x2
a : α
H : f a ≠ 0
⊢ g a ((single a (f a)) a) ≤ f.sum g

Tactic:
single_eq_same

Goal state after:
case inr
α : Type u_5
M : Type u_6
N : Type u_7
inst✝³ : Zero M
inst✝² : AddCommMonoid N
inst✝¹ : PartialOrder N
inst✝ : IsOrderedAddMonoid N
f : α →₀ M
g : α → M → N
h : 0 ≤ fun x1 x2 ↦ g x1 x2
a : α
H : f a ≠ 0
⊢ g a (f a) ≤ f.sum g
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: case inl
ι : Type u_1
α : Type u_3
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
j : ι
⊢ a - b = a - (single j b) j

Tactic:
single_eq_same

Goal state after:
case inl
ι : Type u_1
α : Type u_3
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
j : ι
⊢ a - b = a - b
Module: Mathlib.Data.DFinsupp.Order

Goal state before:
pp: case inl
ι : Type u_1
α : ι → Type u_2
inst✝⁵ : (i : ι) → AddCommMonoid (α i)
inst✝⁴ : (i : ι) → PartialOrder (α i)
inst✝³ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝² : (i : ι) → Sub (α i)
inst✝¹ : ∀ (i : ι), OrderedSub (α i)
inst✝ : DecidableEq ι
j : ι
a b : α j
⊢ a - b = a - (single j b) j

Tactic:
single_eq_same

Goal state after:
case inl
ι : Type u_1
α : ι → Type u_2
inst✝⁵ : (i : ι) → AddCommMonoid (α i)
inst✝⁴ : (i : ι) → PartialOrder (α i)
inst✝³ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝² : (i : ι) → Sub (α i)
inst✝¹ : ∀ (i : ι), OrderedSub (α i)
inst✝ : DecidableEq ι
j : ι
a b : α j
⊢ a - b = a - b
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
n : ℕ
⊢ (X s ^ n).support = {Finsupp.single s n}

Tactic:
classical
    rw [X_pow_eq_monomial, support_monomial, if_neg (one_ne_zero' R)]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
s : σ →₀ ℕ
c : R
⊢ (killCompl hf) ((monomial (Finsupp.mapDomain f s)) c) = (monomial s) c

Tactic:
simp [← rename_monomial]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case monomial
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
hf : Surjective ⇑f
i : σ →₀ ℕ
fr : S₁
⊢ ∃ a, (map f) a = (monomial i) fr

Tactic:
obtain ⟨r, rfl⟩ := hf fr
    exact ⟨monomial i r, map_monomial _ _ _⟩

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommRing R
i : σ
p : MvPolynomial σ R
⊢ degreeOf i (-p) = degreeOf i p

Tactic:
degreeOf,

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommRing R
i : σ
p : MvPolynomial σ R
⊢ Multiset.count i (-p).degrees = degreeOf i p
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommRing R
i : σ
p : MvPolynomial σ R
⊢ Multiset.count i (-p).degrees = degreeOf i p

Tactic:
degreeOf,

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommRing R
i : σ
p : MvPolynomial σ R
⊢ Multiset.count i (-p).degrees = Multiset.count i p.degrees
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case a.mul_X
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
f : σ → S₁
p : MvPolynomial σ R
n : σ
h : (aeval f) p ∈ Algebra.adjoin R (range f)
⊢ (aeval f) (p * X n) ∈ Algebra.adjoin R (range f)

Tactic:
| mul_X p n h =>

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: case neg.h₁
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬constantCoeff p = 0
⊢ 0 ∉ p.support → (f (coeff 0 p) * Finsupp.prod 0 fun i k ↦ g i ^ k) = 0

Tactic:
rw [constantCoeff_eq, coeff, ← Ne, ← Finsupp.mem_support_iff] at h0
    intro
    contradiction

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ f.support
h : ∀ (i : σ), n ≤ d i
⊢ n * Fintype.card σ = ∑ _s, n

Tactic:
Finset.sum_const,

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ f.support
h : ∀ (i : σ), n ≤ d i
⊢ n * Fintype.card σ = Finset.univ.card • n
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case pos
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
hm : 0 = m
⊢ coeff m p = coeff 0 p

Tactic:
rw [← hm]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p.totalDegree = 0 ↔ p = C (coeff 0 p)

Tactic:
by
  constructor <;> intro h
  · ext m; classical rw [coeff_C]; split_ifs with hm; · rw [← hm]
    apply coeff_eq_zero_of_totalDegree_lt; rw [h]
    exact Finset.sum_pos (fun i hi ↦ Nat.pos_of_ne_zero <| Finsupp.mem_support_iff.mp hi)
      (Finsupp.support_nonempty_iff.mpr <| Ne.symm hm)
  · rw [h, totalDegree_C]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
⊢ degreesLE R σ (s + t) = degreesLE R σ s * degreesLE R σ t

Tactic:
rw [le_antisymm_iff, Submodule.mul_le]
  refine ⟨fun x hx ↦ x.as_sum ▸ sum_mem fun i hi ↦ ?_,
    fun x hx y hy ↦ degrees_mul_le.trans (add_le_add hx hy)⟩
  replace hi : i.toMultiset ≤ s + t := (Finset.le_sup hi).trans hx
  let a := (i.toMultiset - t).toFinsupp
  let b := (i.toMultiset ⊓ t).toFinsupp
  have : a + b = i := Multiset.toFinsupp.symm.injective (by simp [a, b, Multiset.sub_add_inter])
  have ha : a.toMultiset ≤ s := by simpa [a, add_comm (a := t)] using hi
  have hb : b.toMultiset ≤ t := by simp [b, Multiset.inter_le_right]
  rw [show monomial i (x.coeff i) = monomial a (x.coeff i) * monomial b 1 by simp [this]]
  exact Submodule.mul_mem_mul ((degrees_monomial _ _).trans ha) ((degrees_monomial _ _).trans hb)

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : n < p.natTrailingDegree
hp : p = 0
⊢ ↑n < p.trailingDegree

Tactic:
rw [hp, trailingDegree_zero]
    exact WithTop.coe_lt_top n

Goal state after:
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: N i : ℕ
⊢ revAtFun N (revAtFun N i) = i

Tactic:
unfold revAtFun

Goal state after:
N i : ℕ
⊢ (if (if i ≤ N then N - i else i) ≤ N then N - if i ≤ N then N - i else i else if i ≤ N then N - i else i) = i
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
⊢ (p + q).eraseLead.coeff n = (p.eraseLead + q).coeff n

Tactic:
by_cases nd : n = p.natDegree

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
nd : n = p.natDegree
⊢ (p + q).eraseLead.coeff n = (p.eraseLead + q).coeff n

case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
nd : ¬n = p.natDegree
⊢ (p + q).eraseLead.coeff n = (p.eraseLead + q).coeff n
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
hnext : f.nextCoeff = 0
hlead : f.natDegree < 2
⊢ f.eraseLead = 0

Tactic:
rw [Nat.lt_succ_iff, Nat.le_one_iff_eq_zero_or_eq_one, natDegree_eq_zero, natDegree_eq_one]
    at hlead

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
hnext : f.nextCoeff = 0
hlead : (∃ x, C x = f) ∨ ∃ a, a ≠ 0 ∧ ∃ b, C a * X + C b = f
⊢ f.eraseLead = 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case hX
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ✝ →₀ ℕ
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : Unique σ
f : R[X] →+* MvPolynomial σ R := eval₂RingHom C (X default)
g : MvPolynomial σ R →+* R[X] := eval₂Hom Polynomial.C fun x ↦ Polynomial.X
i : σ
⊢ Polynomial.eval₂ C (X default) Polynomial.X = X i

Tactic:
Polynomial.eval₂_X

Goal state after:
case hX
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ✝ →₀ ℕ
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : Unique σ
f : R[X] →+* MvPolynomial σ R := eval₂RingHom C (X default)
g : MvPolynomial σ R →+* R[X] := eval₂Hom Polynomial.C fun x ↦ Polynomial.X
i : σ
⊢ X default = X i
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Unique σ
d : σ →₀ ℕ
r : R
⊢ (uniqueAlgEquiv R σ).symm ((Polynomial.monomial (d default)) r) = (monomial d) r

Tactic:
simp [MvPolynomial.monomial_eq]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
H : p.degree < ↑n
⊢ 1 + p.coeff n = 1

Tactic:
coeff_eq_zero_of_degree_lt H,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
H : p.degree < ↑n
⊢ 1 + 0 = 1
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case neg
S : Type u_1
inst✝ : Semiring S
l : List S[X]
p : S[X]
hp : p ∈ l
h : ¬p = 0
⊢ p.degree ≤ (List.map natDegree l).maximum

Tactic:
rw [degree_eq_natDegree h]
    apply List.le_maximum_of_mem'
    rw [List.mem_map]
    use p
    simp [hp]

Goal state after:
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case cons
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih : (Multiset.map leadingCoeff t).prod ≠ 0 → t.prod.leadingCoeff = (Multiset.map leadingCoeff t).prod
h : a.leadingCoeff * (Multiset.map leadingCoeff t).prod ≠ 0
⊢ a.leadingCoeff * t.prod.leadingCoeff = a.leadingCoeff * (Multiset.map leadingCoeff t).prod

Tactic:
rw [ih]

Goal state after:
case cons
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih : (Multiset.map leadingCoeff t).prod ≠ 0 → t.prod.leadingCoeff = (Multiset.map leadingCoeff t).prod
h : a.leadingCoeff * (Multiset.map leadingCoeff t).prod ≠ 0
⊢ (Multiset.map leadingCoeff t).prod ≠ 0
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case cons
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih : (Multiset.map leadingCoeff t).prod ≠ 0 → t.prod.leadingCoeff = (Multiset.map leadingCoeff t).prod
h : a.leadingCoeff * (Multiset.map leadingCoeff t).prod ≠ 0
⊢ a.leadingCoeff * t.prod.leadingCoeff ≠ 0

Tactic:
rw [ih]

Goal state after:
case cons
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih : (Multiset.map leadingCoeff t).prod ≠ 0 → t.prod.leadingCoeff = (Multiset.map leadingCoeff t).prod
h : a.leadingCoeff * (Multiset.map leadingCoeff t).prod ≠ 0
⊢ a.leadingCoeff * (Multiset.map leadingCoeff t).prod ≠ 0

case cons
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih : (Multiset.map leadingCoeff t).prod ≠ 0 → t.prod.leadingCoeff = (Multiset.map leadingCoeff t).prod
h : a.leadingCoeff * (Multiset.map leadingCoeff t).prod ≠ 0
⊢ (Multiset.map leadingCoeff t).prod ≠ 0
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case h
R : Type u
inst✝ : CommRing R
t : Multiset R
i✝ : R
a✝ : i✝ ∈ t
⊢ (X - C i✝).Monic

Tactic:
apply monic_X_sub_C

Goal state after:
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case hnc.h
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
w✝ : R
left✝ : w✝ ∈ t
⊢ (X - C w✝).Monic

Tactic:
apply monic_X_sub_C

Goal state after:
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.Monic
q : R[X]
hq : q = 0
⊢ (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0

pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.Monic
q : R[X]
hq : ¬q = 0
⊢ (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0

Tactic:
· suffices 0 < p.natDegree ↔ p.natDegree ≠ 0 by simp [hq, ← h.natDegree_eq_zero, iffComm]
    exact ⟨fun h => h.ne', fun h => lt_of_le_of_ne (Nat.zero_le _) h.symm⟩

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.Monic
q : R[X]
hq : ¬q = 0
⊢ (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p.Monic
q : R[X]
⊢ q * p = 0 ↔ q = 0

Tactic:
by_cases hq : q = 0 <;> simp [h.mul_left_ne_zero, hq]

Goal state after:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semiring R
k : ℕ
x : R
hx : x ≠ 0
⊢ #{k} = 1

Tactic:
card_singleton

Goal state after:
case refine_2
R : Type u_1
inst✝ : Semiring R
k : ℕ
x : R
hx : x ≠ 0
⊢ 1 = 1
Module: Mathlib.RingTheory.Adjoin.Tower

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst✝¹⁰ : CommSemiring C
inst✝⁹ : CommSemiring D
inst✝⁸ : CommSemiring E
inst✝⁷ : CommSemiring F
inst✝⁶ : Algebra C D
inst✝⁵ : Algebra C E
inst✝⁴ : Algebra C F
inst✝³ : Algebra D F
inst✝² : Algebra E F
inst✝¹ : IsScalarTower C D F
inst✝ : IsScalarTower C E F
S : Set D
T : Set E
hS : adjoin C S = ⊤
hT : adjoin C T = ⊤
⊢ Subalgebra.restrictScalars C (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C E F) ⊤)) (⇑(algebraMap D F) '' S)) =
    Subalgebra.restrictScalars C
      (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C D F) (adjoin C S))) (⇑(algebraMap E F) '' T))

Tactic:
← hT,

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst✝¹⁰ : CommSemiring C
inst✝⁹ : CommSemiring D
inst✝⁸ : CommSemiring E
inst✝⁷ : CommSemiring F
inst✝⁶ : Algebra C D
inst✝⁵ : Algebra C E
inst✝⁴ : Algebra C F
inst✝³ : Algebra D F
inst✝² : Algebra E F
inst✝¹ : IsScalarTower C D F
inst✝ : IsScalarTower C E F
S : Set D
T : Set E
hS : adjoin C S = ⊤
hT : adjoin C T = ⊤
⊢ Subalgebra.restrictScalars C
      (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C E F) (adjoin C T))) (⇑(algebraMap D F) '' S)) =
    Subalgebra.restrictScalars C
      (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C D F) (adjoin C S))) (⇑(algebraMap E F) '' T))
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mp
R : Type u
inst✝ : CommRing R
P : Ideal R
H : (map C P).IsPrime
this : (comap C (map C P)).IsPrime
⊢ P.IsPrime

Tactic:
convert! this using 1

Goal state after:
R : Type u
inst✝ : CommRing R
P : Ideal R
H : (map C P).IsPrime
this : (comap C (map C P)).IsPrime
⊢ P = comap C (map C P)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}
n : ℕ
_hn : n ∈ f.support
this✝ : C (f.coeff n) ∈ p
this : (monomial n) 1 • C (f.coeff n) ∈ p
⊢ C (f.coeff n) * X ^ n ∈ Ideal.span {g | ∃ i, g = C (f.coeff i)}

Tactic:
convert! this using 1

Goal state after:
R : Type u
inst✝ : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}
n : ℕ
_hn : n ∈ f.support
this✝ : C (f.coeff n) ∈ p
this : (monomial n) 1 • C (f.coeff n) ∈ p
⊢ C (f.coeff n) * X ^ n = (monomial n) 1 • C (f.coeff n)
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Semiring B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : FiniteType R A
f : A →ₐ[R] B
hf : Surjective ⇑f
⊢ ⊤.FG

Tactic:
by
    convert ‹FiniteType R A›.1.map f
    simpa only [map_top f, @eq_comm _ ⊤, eq_top_iff, AlgHom.mem_range] using! hf

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

Goal state before:
pp: case h.inr
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ ↑N
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
⊢ p ∈ Ideal.span ↑s

Tactic:
have h1 : p.degree = (q * Polynomial.X ^ (k - q.natDegree)).degree := by
            rw [Polynomial.degree_mul', Polynomial.degree_X_pow]
            · rw [Polynomial.degree_eq_natDegree hp0, Polynomial.degree_eq_natDegree hq0]
              rw [← Nat.cast_add, add_tsub_cancel_of_le, hn]
              · refine le_trans (Polynomial.natDegree_le_of_degree_le hdq) (le_of_lt h)
            rw [Polynomial.leadingCoeff_X_pow, mul_one]
            exact mt Polynomial.leadingCoeff_eq_zero.1 hq0

Goal state after:
case h.inr
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ ↑N
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
h1 : p.degree = (q * X ^ (k - q.natDegree)).degree
⊢ p ∈ Ideal.span ↑s
Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise

Goal state before:
pp: case refine_1
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝ : A
hx✝ : x✝ ∈ Algebra.adjoin R (↑S ∪ ↑T)
x : A
hx : x ∈ ↑S ∪ ↑T
⊢ x ∈ toSubmodule S * toSubmodule T

Tactic:
rcases hx with hxS | hxT

Goal state after:
case refine_1.inl
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝ : A
hx : x✝ ∈ Algebra.adjoin R (↑S ∪ ↑T)
x : A
hxS : x ∈ ↑S
⊢ x ∈ toSubmodule S * toSubmodule T

case refine_1.inr
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝ : A
hx : x✝ ∈ Algebra.adjoin R (↑S ∪ ↑T)
x : A
hxT : x ∈ ↑T
⊢ x ∈ toSubmodule S * toSubmodule T
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ ((aeval f) (p * q)).ker
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ∃ y ∈ ((aeval f) p).ker, ∃ z ∈ ((aeval f) q).ker, y + z = v

Tactic:
have h_eval₂_qpp' :=
    calc
      aeval f (q * (p * p')) v = aeval f (p' * (p * q)) v := by
        rw [mul_comm, mul_assoc, mul_comm, mul_assoc, mul_comm q p]
      _ = 0 := by rw [aeval_mul, Module.End.mul_apply, LinearMap.mem_ker.1 hv, map_zero]

Goal state after:
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ ((aeval f) (p * q)).ker
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' : ((aeval f) (q * (p * p'))) v = 0
⊢ ∃ y ∈ ((aeval f) p).ker, ∃ z ∈ ((aeval f) q).ker, y + z = v
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: R : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
⊢ 2 ≠ 0

Tactic:
rw [Ne, (by norm_cast : (2 : R) = (2 : ℕ)), ringChar.spec, Nat.dvd_prime Nat.prime_two]
  exact mt (or_iff_left hR).mp CharP.ringChar_ne_one

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: case pos.fst
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h : ∀ (r : R), r ≠ 0 → (algebraMap R A) r ∉ s
inst✝¹ : FunLike F (Unitization R ↥s) A
inst✝ : AlgHomClass F R (Unitization R ↥s) A
f : F
hf : ∀ (x : ↥s), f ↑x = ↑x
r : R
a : ↥s
hx : (algebraMap R A) r = -↑a
hr : r = 0
⊢ (Unitization.inl r).toProd.1 = (-↑a).toProd.1

Tactic:
simp [hr]

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : Field R
inst✝⁶ : StarRing R
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Algebra R A
inst✝² : StarModule R A
inst✝¹ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
inst✝ : StarMemClass S A
s : S
h1 : 1 ∉ s
starAlgHom : Unitization R ↥s →⋆ₐ[R] ↥(StarAlgebra.adjoin R ↑s) :=
  (unitization s).codRestrict (StarAlgebra.adjoin R ↑s) ⋯
⊢ Function.Bijective ⇑starAlgHom

Tactic:
by
    refine ⟨?_, fun x ↦ ?_⟩
    · have := AlgHomClass.unitization_injective s h1 ((StarSubalgebra.subtype _).comp starAlgHom)
        fun _ ↦ by simp [starAlgHom]
      rw [StarAlgHom.coe_comp] at this
      exact this.of_comp
    · obtain (⟨a, ha⟩ : (x : A) ∈ (unitization s).range) :=
        (unitization_range s).ge x.property
      exact ⟨a, Subtype.ext ha⟩

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p a k : ℕ
hp : Prime (a ^ k)
h : a ^ k = p
⊢ a = a ^ k ∧ k = 1

Tactic:
hp.eq_one_of_pow,

Goal state after:
p a k : ℕ
hp : Prime (a ^ k)
h : a ^ k = p
⊢ a = a ^ 1 ∧ 1 = 1
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R₁ : Type u_1
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R₁
inst✝³ : Ring A
inst✝² : Algebra R₁ A
inst✝¹ : Semiring B
inst✝ : Algebra R₁ B
f : A →ₐ[R₁] B
hf : Surjective ⇑f
a : A
⊢ (quotientKerAlgEquivOfSurjective hf).symm (f a) = (Quotient.mk (ker f)) a

Tactic:
apply (Ideal.quotientKerAlgEquivOfSurjective hf).injective
  simp

Goal state after: