mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
hpq : Disjoint p.vars q.vars
⊢ (p - q).vars = p.vars ∪ q.vars

Tactic:
rw [← vars_neg q] at hpq

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
hpq : Disjoint p.vars (-q).vars
⊢ (p - q).vars = p.vars ∪ q.vars
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S₁
p q : MvPolynomial σ R
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁵ : CommSemiring S
inst✝⁴ : CommSemiring A
inst✝³ : CommSemiring B
inst✝² : Algebra S R
inst✝¹ : Algebra S A
inst✝ : Algebra S B
f : R →ₐ[S] A
X : σ → A
r : S
⊢ (↑↑(eval₂Hom (↑f) X)).toFun ((algebraMap S (MvPolynomial σ R)) r) = (algebraMap S A) r

Tactic:
simp [IsScalarTower.algebraMap_eq S R (MvPolynomial σ R), algebraMap_eq]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
this : p.support.Nonempty
s : σ →₀ ℕ
hs1 : s ∈ p.support
hs2 : degreeOf i p = s i
⊢ degreeOf i p ≤ s i

Tactic:
rw [hs2]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
this : p.support.Nonempty
s : σ →₀ ℕ
hs1 : s ∈ p.support
hs2 : degreeOf i p = s i
h : s ∈ q.support
⊢ degreeOf i p ≤ degreeOf i q

Tactic:
rw [hs2]

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
this : p.support.Nonempty
s : σ →₀ ℕ
hs1 : s ∈ p.support
hs2 : degreeOf i p = s i
h : s ∈ q.support
⊢ s i ≤ degreeOf i q
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ¬(p = 0 ∨ p.coeff 0 ≠ 0) ↔ p ≠ 0 ∧ p.coeff 0 = 0

Tactic:
rw [not_or, not_ne_iff]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ ↑n ≤ (X ^ n).trailingDegree

Tactic:
simpa only [C_1, one_mul] using le_trailingDegree_C_mul_X_pow n (1 : R)

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

Goal state before:
pp: case pos
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ (s.sup' hs fun i ↦ (f i).degree) = s.sup (WithBot.some ∘ fun i ↦ (f i).natDegree)

Tactic:
←
        Finset.sup'_eq_sup hs

Goal state after:
case pos
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ (s.sup' hs fun i ↦ (f i).degree) = s.sup' hs (WithBot.some ∘ fun i ↦ (f i).natDegree)
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf : ∀ (f : R[X]), #f.support ≤ cf.succ → f.natDegree ≤ N → reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
f0 : ¬f = 0
⊢ reflect (N + O) ((f.eraseLead + C f.leadingCoeff * X ^ f.natDegree) * g) =
    reflect N (f.eraseLead + C f.leadingCoeff * X ^ f.natDegree) * reflect O g

Tactic:
add_mul,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf : ∀ (f : R[X]), #f.support ≤ cf.succ → f.natDegree ≤ N → reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
f0 : ¬f = 0
⊢ reflect (N + O) (f.eraseLead * g + C f.leadingCoeff * X ^ f.natDegree * g) =
    reflect N (f.eraseLead + C f.leadingCoeff * X ^ f.natDegree) * reflect O g
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf : ∀ (f : R[X]), #f.support ≤ cf.succ → f.natDegree ≤ N → reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
f0 : ¬f = 0
⊢ reflect (N + O) (f.eraseLead * g) + reflect (N + O) (C f.leadingCoeff * X ^ f.natDegree * g) =
    (reflect N f.eraseLead + reflect N (C f.leadingCoeff * X ^ f.natDegree)) * reflect O g

Tactic:
add_mul,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf : ∀ (f : R[X]), #f.support ≤ cf.succ → f.natDegree ≤ N → reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
f0 : ¬f = 0
⊢ reflect (N + O) (f.eraseLead * g) + reflect (N + O) (C f.leadingCoeff * X ^ f.natDegree * g) =
    reflect N f.eraseLead * reflect O g + reflect N (C f.leadingCoeff * X ^ f.natDegree) * reflect O g
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : IsLeftCancelMulZero R
r₁ r₂ : R
hr₂ : r₂ ≠ 0
r₃ : R
h : (C r₂ * X + C r₃).natDegree = 1
this : ∀ (x y : R), r₂ * x = r₂ * y → x = y
⊢ r₁ ∈ {x | (C r₂ * X + C r₃).IsRoot x} → ∀ ⦃y : R⦄, y ∈ {x | (C r₂ * X + C r₃).IsRoot x} → r₁ = y

Tactic:
grind [IsRoot, eval_add, eval_mul_X, eval_C]

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

Goal state before:
pp: case pos
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
q0 : q.natDegree = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

Tactic:
degree_le_zero_iff.mp (natDegree_eq_zero_iff_degree_le_zero.mp q0),

Goal state after:
case pos
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
q0 : q.natDegree = 0
⊢ (p.comp (C (q.coeff 0))).natDegree = p.natDegree * (C (q.coeff 0)).natDegree
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
n : ℕ
r : R
a✝ : r ≠ 0
hnN : n ≤ N
⊢ i r * (⅟x * x) ^ (N - n) * x ^ n = i r * x ^ n

Tactic:
invOf_mul_self,

Goal state after:
case refine_2
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
n : ℕ
r : R
a✝ : r ≠ 0
hnN : n ≤ N
⊢ i r * 1 ^ (N - n) * x ^ n = i r * x ^ n
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
⊢ (p * q).trailingCoeff = p.trailingCoeff * q.trailingCoeff

Tactic:
← reverse_leadingCoeff,

Goal state after:
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
⊢ (p * q).reverse.leadingCoeff = p.trailingCoeff * q.trailingCoeff
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
⊢ m ∈ Finset.image (cons i) (((finSuccEquiv R n) f).coeff i).support ↔ m ∈ {m ∈ f.support | m 0 = i}

Tactic:
rw [Finset.mem_filter, Finset.mem_image, mem_support_iff]

Goal state after:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
⊢ (∃ a ∈ (((finSuccEquiv R n) f).coeff i).support, cons i a = m) ↔ coeff m f ≠ 0 ∧ m 0 = i
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
α : Type u_1
f : α → R[X]
hf : ∀ i ∈ Function.mulSupport f, (f i).Monic
⊢ (finprod f).Monic

Tactic:
classical
  rw [finprod_def]
  split_ifs
  · exact monic_prod_of_monic _ _ fun a ha => hf a ((Set.Finite.mem_toFinset _).mp ha)
  · exact monic_one

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

Goal state before:
pp: case cons
S : Type u_1
inst✝ : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH : (∀ p ∈ tl, p.natDegree ≤ n) → tl.prod.coeff (tl.length * n) = (List.map (fun p ↦ p.coeff n) tl).prod
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
hl' : ∀ p ∈ tl, p.natDegree ≤ n
⊢ (hd * tl.prod).coeff ((tl.length + 1) * n) = hd.coeff n * (List.map (fun p ↦ p.coeff n) tl).prod

Tactic:
add_mul,

Goal state after:
case cons
S : Type u_1
inst✝ : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH : (∀ p ∈ tl, p.natDegree ≤ n) → tl.prod.coeff (tl.length * n) = (List.map (fun p ↦ p.coeff n) tl).prod
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
hl' : ∀ p ∈ tl, p.natDegree ≤ n
⊢ (hd * tl.prod).coeff (tl.length * n + 1 * n) = hd.coeff n * (List.map (fun p ↦ p.coeff n) tl).prod
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case h
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
h : coeff m f ≠ 0 ∧ m 0 = i
⊢ ¬coeff m f = 0 ∧ m = m

Tactic:
simp [h.1]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
t : Multiset R
⊢ (Multiset.map (fun x ↦ X - C x) t).prod.nextCoeff = -t.sum

Tactic:
by
  rw [nextCoeff_multiset_prod]
  · simp only [nextCoeff_X_sub_C]
    exact t.sum_hom (-AddMonoidHom.id R)
  · intros
    apply monic_X_sub_C

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun m i ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ i ∈ range n, f (n + 1) i = y * f n i
⊢ (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = (x + y) * (x + y) ^ n

Tactic:
add_mul,

Goal state after:
case succ
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun m i ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ i ∈ range n, f (n + 1) i = y * f n i
⊢ (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun m i ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ i ∈ range n, f (n + 1) i = y * f n i
⊢ (f (n + 1) n + ∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n

Tactic:
add_mul,

Goal state after:
case succ
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun m i ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ i ∈ range n, f (n + 1) i = y * f n i
⊢ f (n + 1) n * x + (∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
h : IsUnit (X ^ n - 1)
hn : n ≠ 0
⊢ n = 0

Tactic:
← @natDegree_one R,

Goal state after:
case inr
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
h : IsUnit (X ^ n - 1)
hn : n ≠ 0
⊢ n = natDegree 1
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : #f.support = 2
⊢ ∃ k m, ∃ (_ : k < m), ∃ x y, ∃ (_ : x ≠ 0) (_ : y ≠ 0), f = C x * X ^ k + C y * X ^ m

pp: case refine_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (∃ k m, ∃ (_ : k < m), ∃ x y, ∃ (_ : x ≠ 0) (_ : y ≠ 0), f = C x * X ^ k + C y * X ^ m) → #f.support = 2

Tactic:
· obtain ⟨k, x, hk, hx, rfl⟩ := card_support_eq.mp h
    refine ⟨k 0, k 1, hk Nat.zero_lt_one, x 0, x 1, hx 0, hx 1, ?_⟩
    rw [Fin.sum_univ_castSucc, Fin.sum_univ_one]
    rfl

Goal state after:
case refine_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (∃ k m, ∃ (_ : k < m), ∃ x y, ∃ (_ : x ≠ 0) (_ : y ≠ 0), f = C x * X ^ k + C y * X ^ m) → #f.support = 2
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x y : R
h : Commute x y
m n : ℕ
hmn : m ≤ n
⊢ (MulOpposite.op x - MulOpposite.op y) * ∑ x_1 ∈ Ico m n, MulOpposite.op y ^ (n - 1 - x_1) * MulOpposite.op x ^ x_1 =
    MulOpposite.op x ^ n - MulOpposite.op x ^ m * MulOpposite.op y ^ (n - m)

Tactic:
have : (∑ k ∈ Ico m n, MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k) =
      ∑ k ∈ Ico m n, MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k) := by
    refine sum_congr rfl fun k _ => ?_
    have hp := Commute.pow_pow (Commute.op h.symm) (n - 1 - k) k
    simpa [Commute, SemiconjBy] using hp

Goal state after:
R : Type u_1
inst✝ : Ring R
x y : R
h : Commute x y
m n : ℕ
hmn : m ≤ n
this :
  ∑ k ∈ Ico m n, MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k =
    ∑ k ∈ Ico m n, MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k)
⊢ (MulOpposite.op x - MulOpposite.op y) * ∑ x_1 ∈ Ico m n, MulOpposite.op y ^ (n - 1 - x_1) * MulOpposite.op x ^ x_1 =
    MulOpposite.op x ^ n - MulOpposite.op x ^ m * MulOpposite.op y ^ (n - m)
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: case refine_2
R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x ↑S))
t✝ : Finset A
x : A
t : Finset A
a✝ : x ∉ t
h : P (Algebra.adjoin R ↑t)
⊢ P (Algebra.adjoin R (insert x ↑t))

Tactic:
simpa only [Algebra.adjoin_insert_adjoin] using ih _ x h

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

Goal state before:
pp: case mp.inl
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg✝ : p.degree ≤ ↑n
hpI : p ∈ I.ofPolynomial
hpdeg : p.degree < ↑n
⊢ p.coeff n = 0

Tactic:
exact coeff_eq_zero_of_degree_lt hpdeg

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

Goal state before:
pp: case mpr.refine_1
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ ↑n
this : p.natDegree + (n - p.natDegree) = n
⊢ (p * X ^ (n - p.natDegree)).degree ≤ ↑n

Tactic:
apply le_trans (degree_mul_le _ _) _
      apply le_trans (add_le_add degree_le_natDegree (degree_X_pow_le _)) _
      rw [← Nat.cast_add, this]

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

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommRing R
P : Ideal R
⊢ P.IsPrime → (map C P).IsPrime

Tactic:
intro h
    constructor
    · rw [Ne, eq_top_iff_one, mem_map_C_iff, not_forall]
      use 0
      rw [coeff_one_zero, ← eq_top_iff_one]
      exact h.1
    · intro f g
      simp only [mem_map_C_iff]
      contrapose!
      rintro ⟨hf, hg⟩
      classical
        let m := Nat.find hf
        let n := Nat.find hg
        refine ⟨m + n, ?_⟩
        rw [coeff_mul, ← Finset.insert_erase ((Finset.mem_antidiagonal (a := (m, n))).mpr rfl),
          Finset.sum_insert (Finset.notMem_erase _ _), (P.add_mem_iff_left _).not]
        · apply mt h.2
          rw [not_or]
          exact ⟨Nat.find_spec hf, Nat.find_spec hg⟩
        apply P.sum_mem
        rintro ⟨i, j⟩ hij
        rw [Finset.mem_erase, Finset.mem_antidiagonal] at hij
        simp only [Ne, Prod.mk_inj, not_and_or] at hij
        obtain hi | hj : i < m ∨ j < n := by
          lia
        · rw [mul_comm]
          apply P.mul_mem_left
          exact Classical.not_not.1 (Nat.find_min hf hi)
        · apply P.mul_mem_left
          exact Classical.not_not.1 (Nat.find_min hg hj)

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R[X]
hI : comap C I = I.leadingCoeff
⊢ map C (comap C I) = I

Tactic:
refine le_antisymm map_comap_le (fun f hfI ↦ ?_)
  induction hn : f.natDegree using Nat.strong_induction_on generalizing f with | _ _ ih
  have h : C f.leadingCoeff * X ^ f.natDegree ∈ map C (comap C I) :=
    (map C (comap C I)).mul_mem_right (X ^ f.natDegree) <| mem_map_of_mem C <| by
      simpa [hI] using (I.mem_leadingCoeff f.leadingCoeff).2 ⟨f, hfI, rfl⟩
  rcases f.eraseLead_natDegree_lt_or_eraseLead_eq_zero with hlt | hzero
  · have he : f.eraseLead ∈ I := by simpa using I.sub_mem hfI (map_comap_le h)
    simpa using (map C (comap C I)).add_mem (ih _ (by simpa [hn] using hlt) _ he rfl) h
  · rwa [← f.eraseLead_add_C_mul_X_pow, hzero, zero_add]

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

Goal state before:
pp: case pos
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 = -↑a

pp: case neg
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 = -↑a

Tactic:
· ext
      · simp [hr]
      · simpa [hr] using hx

Goal state after:
case neg
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 = -↑a
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝⁴ : Ring R
S : Type v
inst✝³ : Ring S
R' : Type u_5
S' : Type u_6
inst✝² : Ring R'
inst✝¹ : Ring S'
f : R →+* S
f' : R' →+* S'
g : R →+* R'
g' : S →+* S'
hfg : f'.comp g = g'.comp f
I : Ideal S'
inst✝ : I.IsTwoSided
⊢ let leq := ⋯;
  (quotientMap I g' ⋯).comp (quotientMap (comap g' I) f ⋯) = (quotientMap I f' ⋯).comp (quotientMap (comap f' I) g leq)

Tactic:
refine RingHom.ext fun a => ?_
  obtain ⟨r, rfl⟩ := Quotient.mk_surjective a
  simp only [RingHom.comp_apply, quotientMap_mk]
  exact (Ideal.Quotient.mk I).congr_arg (_root_.trans (g'.comp_apply f r).symm
    (hfg ▸ f'.comp_apply g r))

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

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : Set A
p : (x : A) → x ∈ adjoin R s → Prop
mem : ∀ (x : A) (h : x ∈ s), p x ⋯
algebraMap : ∀ (r : R), p ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x + y) ⋯
mul : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯
star : ∀ (x : A) (hx : x ∈ adjoin R s), p x hx → p (Star.star x) ⋯
a : A
ha : a ∈ adjoin R s
x : A
hx✝ : x ∈ s ∪ Star.star s
hx : Star.star x ∈ s
⊢ Star.star x ∈ s ∪ Star.star s

Tactic:
simpa using Or.inl hx

Goal state after:
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case inl
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l₁ l₂ : List α
left✝ : l₂ ≠ []
e : l₁ ++ l₂ = is
⊢ l₁ ++ l₂ ~ is

Tactic:
simp [e]

Goal state after:
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ minimalPeriod f^[n] x ∣ minimalPeriod f x / (minimalPeriod f x).gcd n

pp: case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ minimalPeriod f x / (minimalPeriod f x).gcd n ∣ minimalPeriod f^[n] x

Tactic:
· apply IsPeriodicPt.minimalPeriod_dvd
    rw [IsPeriodicPt, IsFixedPt, ← iterate_mul, ← Nat.mul_div_assoc _ (gcd_dvd_left _ _),
      mul_comm, Nat.mul_div_assoc _ (gcd_dvd_right _ _), mul_comm, iterate_mul]
    exact (isPeriodicPt_minimalPeriod f x).iterate _

Goal state after:
case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ minimalPeriod f x / (minimalPeriod f x).gcd n ∣ minimalPeriod f^[n] x
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
⊢ ∀ {ts is l : List α}, l ~ is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux is

Tactic:
show ∀ (ts is l : List α),
      l ~ is ++ ts → (∃ (is' : _) (_ : is' ~ is), l = is' ++ ts) ∨ l ∈ permutationsAux ts is

Goal state after:
α : Type u_1
⊢ ∀ (ts is l : List α), l ~ is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux is
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case pos
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)

Tactic:
have hx' := minimalPeriod_pos_of_mem_periodicPts hx

Goal state after:
case pos
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
b : α
n : ℤ
⊢ a ^ (n % ↑(minimalPeriod (fun x ↦ a • x) b)) • b = a ^ n • b

Tactic:
rw [← period_eq_minimalPeriod, zpow_mod_period_smul]

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons.cons
α : Type u_1
inst✝ : DecidableEq α
x d : α
xs' : List α
hd : d ∈ xs'
y z : α
zs : List α
ih : (∀ x ∈ z :: zs, x ∈ xs') → (z :: zs).nextOr x d ∈ xs'
hxs' : ∀ x ∈ y :: z :: zs, x ∈ xs'
⊢ (y :: z :: zs).nextOr x d ∈ xs'

Tactic:
rw [nextOr]

Goal state after:
case cons.cons
α : Type u_1
inst✝ : DecidableEq α
x d : α
xs' : List α
hd : d ∈ xs'
y z : α
zs : List α
ih : (∀ x ∈ z :: zs, x ∈ xs') → (z :: zs).nextOr x d ∈ xs'
hxs' : ∀ x ∈ y :: z :: zs, x ∈ xs'
⊢ (if x = y then z else (z :: zs).nextOr x d) ∈ xs'
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: case refine_2
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : StarRing R
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : StarRing A
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R B
inst✝⁴ : StarRing B
inst✝³ : StarModule R A
s : Set A
inst✝² : FunLike F (↥(adjoin R s)) B
inst✝¹ : AlgHomClass F R (↥(adjoin R s)) B
inst✝ : StarHomClass F (↥(adjoin R s)) B
f g : F
h : ∀ (x : ↥(adjoin R s)), ↑x ∈ s → f x = g x
a : ↥(adjoin R s)
r : R
⊢ f ((algebraMap R ↥(adjoin R s)) r) = g ((algebraMap R ↥(adjoin R s)) r)

Tactic:
simp only [AlgHomClass.commutes]

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
x : α
hx : x ∈ l
⊢ l = l.reverse.reverse

Tactic:
exact (reverse_reverse l).symm

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons.cons
α : Type u_1
hd hd' : α
tl : List α
hl : (hd :: hd' :: tl).Nodup
⊢ (∃ x y, x ≠ y ∧ x ∈ ↑(hd :: hd' :: tl) ∧ y ∈ ↑(hd :: hd' :: tl)) ↔ 2 ≤ (hd :: hd' :: tl).length

Tactic:
simp only [mem_cons, mem_coe_iff, List.length, Ne, Nat.succ_le_succ_iff,
      Nat.zero_le, iff_true]

Goal state after:
case cons.cons
α : Type u_1
hd hd' : α
tl : List α
hl : (hd :: hd' :: tl).Nodup
⊢ ∃ x y, ¬x = y ∧ (x = hd ∨ x = hd' ∨ x ∈ tl) ∧ (y = hd ∨ y = hd' ∨ y ∈ tl)
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
⊢ q = ↑(g ^ minimalPeriod (fun x ↦ g • x) q • Quotient.out q)

Tactic:
Quotient.mk_smul_out,

Goal state after:
G : Type u
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
⊢ q = g ^ minimalPeriod (fun x ↦ g • x) q • q
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: case succ
n n✝ : ℕ
hk : n✝ + 1 ≠ 0
⊢ (n ^ (n✝ + 1)).primeFactors = n.primeFactors

Tactic:
rw [primeFactors_pow_succ]

Goal state after: