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

Goal state before:
pp: case C
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
τ : Type u_6
f : σ → τ
φ : MvPolynomial σ R
⊢ ∀ (a : R), constantCoeff ((rename f) (C a)) = constantCoeff (C a)

pp: case add
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
τ : Type u_6
f : σ → τ
φ : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    constantCoeff ((rename f) p) = constantCoeff p →
      constantCoeff ((rename f) q) = constantCoeff q → constantCoeff ((rename f) (p + q)) = constantCoeff (p + q)

pp: case mul_X
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
τ : Type u_6
f : σ → τ
φ : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    constantCoeff ((rename f) p) = constantCoeff p → constantCoeff ((rename f) (p * X n)) = constantCoeff (p * X n)

Tactic:
· intro a
    simp only [constantCoeff_C, rename_C]

Goal state after:
case add
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
τ : Type u_6
f : σ → τ
φ : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    constantCoeff ((rename f) p) = constantCoeff p →
      constantCoeff ((rename f) q) = constantCoeff q → constantCoeff ((rename f) (p + q)) = constantCoeff (p + q)

case mul_X
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
τ : Type u_6
f : σ → τ
φ : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    constantCoeff ((rename f) p) = constantCoeff p → constantCoeff ((rename f) (p * X n)) = constantCoeff (p * X n)
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
i : σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ ((∏ j ∈ s, f j).support.sup fun m ↦ m i) ≤ ∑ x ∈ s, (f x).support.sup fun m ↦ m i

Tactic:
exact supDegree_prod_le (by simp only [coe_zero, Pi.zero_apply]) (by simp)

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommRing R
p : MvPolynomial σ R
r : R
⊢ max p.totalDegree (C r).totalDegree = p.totalDegree

Tactic:
totalDegree_C,

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommRing R
p : MvPolynomial σ R
r : R
⊢ max p.totalDegree 0 = p.totalDegree
Module: Mathlib.Algebra.BigOperators.Finsupp.Fin

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
n : ℕ
σ : Fin n →₀ M
i : M
⊢ ((cons i σ).sum fun x e ↦ e) = i + σ.sum fun x e ↦ e

Tactic:
sum_fintype _ _ (fun _ => rfl),

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
n : ℕ
σ : Fin n →₀ M
i : M
⊢ ∑ i_1, (cons i σ) i_1 = i + σ.sum fun x e ↦ e
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 : 0 ∈ p.coeff.support
⊢ 0 ∉ p.support → (f (coeff 0 p) * Finsupp.prod 0 fun i k ↦ g i ^ k) = 0

Tactic:
intro

Goal state after:
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 : 0 ∈ p.coeff.support
a✝ : 0 ∉ p.support
⊢ (f (coeff 0 p) * Finsupp.prod 0 fun i k ↦ g i ^ k) = 0
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
p : MvPolynomial σ R
inst✝ : LinearOrder σ
⊢ leadingCoeff (⇑toLex) p = coeff (ofLex (supDegree (⇑toLex) p)) p

Tactic:
leadingCoeff

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
p : MvPolynomial σ R
inst✝ : LinearOrder σ
⊢ p.coeff (invFun (⇑toLex) (supDegree (⇑toLex) p)) = coeff (ofLex (supDegree (⇑toLex) p)) p
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
⊢ (p * X ^ n).natTrailingDegree = p.natTrailingDegree + n

Tactic:
by
  apply le_antisymm
  · refine natTrailingDegree_le_of_ne_zero fun h => mt trailingCoeff_eq_zero.mp hp ?_
    rwa [trailingCoeff, ← coeff_mul_X_pow]
  · rw [natTrailingDegree_eq_support_min' fun h => hp (mul_X_pow_eq_zero h), Finset.le_min'_iff]
    intro y hy
    have key : n ≤ y := by
      rw [mem_support_iff, coeff_mul_X_pow'] at hy
      exact by_contra fun h => hy (if_neg h)
    rw [mem_support_iff, coeff_mul_X_pow', if_pos key] at hy
    exact (le_tsub_iff_right key).mp (natTrailingDegree_le_of_ne_zero hy)

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

Goal state before:
pp: case zero.zero
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
g : R[X]
Cg : #g.support ≤ Nat.succ 0
Og : g.natDegree ≤ O
⊢ reflect (N + O) (C f.leadingCoeff * (C g.leadingCoeff * (X ^ g.natDegree * X ^ f.natDegree))) =
    reflect N (C f.leadingCoeff * X ^ f.natDegree) * reflect O (C g.leadingCoeff * X ^ g.natDegree)

Tactic:
← pow_add (X : R[X]),

Goal state after:
case zero.zero
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
g : R[X]
Cg : #g.support ≤ Nat.succ 0
Og : g.natDegree ≤ O
⊢ reflect (N + O) (C f.leadingCoeff * (C g.leadingCoeff * X ^ (g.natDegree + f.natDegree))) =
    reflect N (C f.leadingCoeff * X ^ f.natDegree) * reflect O (C g.leadingCoeff * X ^ g.natDegree)
Module: Mathlib.Algebra.MvPolynomial.Equiv

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 : ℕ
s : σ✝ →₀ ℕ
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : Unique σ
p✝ : R[X]
p : ℕ
n : R
x✝ :
  eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) (Polynomial.C n * Polynomial.X ^ p)) =
    Polynomial.C n * Polynomial.X ^ p
⊢ Polynomial.C n * eval₂ Polynomial.C (fun x ↦ Polynomial.X) (X default) ^ (p + 1) =
    Polynomial.C n * Polynomial.X ^ (p + 1)

Tactic:
eval₂_X

Goal state after:
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 σ
p✝ : R[X]
p : ℕ
n : R
x✝ :
  eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) (Polynomial.C n * Polynomial.X ^ p)) =
    Polynomial.C n * Polynomial.X ^ p
⊢ Polynomial.C n * Polynomial.X ^ (p + 1) = Polynomial.C n * Polynomial.X ^ (p + 1)
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Unique σ
f : R[X]
φ : R →+* S
a : S
⊢ eval₂ φ (fun x ↦ a) ((uniqueAlgEquiv R σ).symm f) = Polynomial.eval₂ φ a f

Tactic:
eval₂_uniqueAlgEquiv_symm

Goal state after:
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Unique σ
f : R[X]
φ : R →+* S
a : S
⊢ Polynomial.eval₂ φ a f = Polynomial.eval₂ φ a f
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case neg
R : Type u
inst✝ : Ring R
p : R[X]
a✝ : Nontrivial R
h : ¬p = 0
⊢ p.leadingCoeff * (-X).leadingCoeff ^ p.natDegree = (-1) ^ p.natDegree * p.leadingCoeff

Tactic:
simp [((Commute.neg_one_left _).pow_left _).eq, h]

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Ring R
p : R[X]
a✝ : Nontrivial R
h : ¬p = 0
⊢ (-X).natDegree ≠ 0

Tactic:
simp [((Commute.neg_one_left _).pow_left _).eq, h]

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Ring R
p : R[X]
a✝ : Nontrivial R
h : ¬p = 0
⊢ p.leadingCoeff * (-X).leadingCoeff ^ p.natDegree ≠ 0

Tactic:
simp [((Commute.neg_one_left _).pow_left _).eq, h]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial (Option σ) R
i : ℕ
m : σ →₀ ℕ
⊢ m ∈ (((optionEquivLeft R σ) f).coeff i).support ↔ optionElim i m ∈ f.support

Tactic:
by
  simp [← optionEquivLeft_coeff_some_coeff_none]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ Subsingleton R → (∀ (f g : R[X]), f = g) ∧ ∀ (a b : R), a = b

Tactic:
intro

Goal state after:
R : Type u
inst✝ : Semiring R
a✝ : Subsingleton R
⊢ (∀ (f g : R[X]), f = g) ∧ ∀ (a b : R), a = b
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.coeff f.natDegree = f.leadingCoeff

Tactic:
leadingCoeff

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.coeff f.natDegree = f.coeff f.natDegree
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
⊢ (↑(finSuccEquiv R n).symm).comp (Polynomial.C.comp C) = C

Tactic:
by
  refine RingHom.ext fun x => ?_
  rw [RingHom.comp_apply]
  refine
    (MvPolynomial.finSuccEquiv R n).injective
      (Trans.trans ((MvPolynomial.finSuccEquiv R n).apply_symm_apply _) ?_)
  simp only [MvPolynomial.finSuccEquiv_apply, MvPolynomial.eval₂Hom_C]

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

Goal state before:
pp: 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
⊢ (List.map natDegree tl).sum ≤ n * (List.map natDegree tl).length

Tactic:
mul_comm

Goal state after:
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
⊢ (List.map natDegree tl).sum ≤ (List.map natDegree tl).length * n
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case neg
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : ¬p = 1
a b : R[X]
ha : a.Monic
hb : b.Monic
⊢ a * b = p → a = 1 ∨ b = 1 ↔ a * b = p → a = 1 ∨ b.natDegree = 0

Tactic:
hb.natDegree_eq_zero

Goal state after:
case neg
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : ¬p = 1
a b : R[X]
ha : a.Monic
hb : b.Monic
⊢ a * b = p → a = 1 ∨ b = 1 ↔ a * b = p → a = 1 ∨ b = 1
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
⊢ Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0

Tactic:
by
  by_cases hp1 : p = 1; · simp [hp1]
  rw [irreducible_of_monic hp hp1, and_iff_right hp1]
  refine forall₄_congr fun a b ha hb => ?_
  rw [ha.natDegree_eq_zero, hb.natDegree_eq_zero]

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

Goal state before:
pp: case right
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
h✝ : Nontrivial R
a b : R[X]
ha : a.Monic
hb : b.Monic
hm : (a * b).Monic
hnd : (a * b).natDegree = 2
hdb : b.natDegree = 1
hda : a.natDegree + 1 = 2
⊢ (a * b).coeff 1 = a.coeff 0 + b.coeff 0

Tactic:
simpa only [nextCoeff, hnd, add_right_cancel hda, hdb] using! ha.nextCoeff_mul hb

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

Goal state before:
pp: case a
R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : AddLeftReflectLE R
inst✝³ : AddLeftMono R
inst✝² : ExistsAddOfLE R
inst✝¹ : Sub R
inst✝ : OrderedSub R
x y : R
hxy : x ≤ y
n x✝ : ℕ
a✝ : x✝ < n
⊢ x ^ (n - 1 - x✝) * y ^ (n - 1 - (n - 1 - x✝)) = y ^ x✝ * x ^ (n - 1 - x✝)

Tactic:
mul_comm

Goal state after:
case a
R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : AddLeftReflectLE R
inst✝³ : AddLeftMono R
inst✝² : ExistsAddOfLE R
inst✝¹ : Sub R
inst✝ : OrderedSub R
x y : R
hxy : x ≤ y
n x✝ : ℕ
a✝ : x✝ < n
⊢ y ^ (n - 1 - (n - 1 - x✝)) * x ^ (n - 1 - x✝) = y ^ x✝ * x ^ (n - 1 - x✝)
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : p = 0
hb₀ : b = 0
⊢ r ^ 0 ^ a - r ∣ r ^ 0 ^ b - r

Tactic:
hb₀,

Goal state after:
case pos
R : Type u_1
inst✝ : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : p = 0
hb₀ : b = 0
⊢ r ^ 0 ^ a - r ∣ r ^ 0 ^ 0 - r
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
⊢ 0 < p.natDegree ↔ p.natDegree ≠ 0

Tactic:
exact ⟨fun h => h.ne', fun h => lt_of_le_of_ne (Nat.zero_le _) h.symm⟩

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

Goal state before:
pp: case right
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
q r : R[X]
h : q * p = r * p
⊢ q = r

Tactic:
rw [← sub_eq_zero, ← hp.mul_left_eq_zero_iff, sub_mul, h, sub_self]

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

Goal state before:
pp: R : Type u
ι : Type w
s : Finset ι
inst✝² : CommRing R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v ↑s
⊢ (∑ i ∈ s, v i • map (algebraMap R A) (f i)).natDegree = s.sup fun i ↦ (f i).natDegree

Tactic:
by
  apply le_antisymm
  · exact natDegree_sum_le_of_forall_le _ _ fun i hi ↦ (natDegree_smul_le _ _).trans <|
      natDegree_map_le.trans <| Finset.le_sup (f := fun i ↦ (f i).natDegree) hi
  · apply Finset.sup_le
    intro i hi
    by_cases hf : f i = 0
    · simp [hf]
    apply le_natDegree_of_ne_zero
    rw [finsetSum_coeff]
    conv in (fun _ ↦ _) =>
      ext
      rw [coeff_smul, smul_eq_mul, coeff_map, mul_comm, ← Algebra.smul_def]
    intro H
    exact hf (leadingCoeff_eq_zero.mp (linearIndepOn_finset_iff.mp h _ H i hi))

Goal state after:
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
this : ∑ k ∈ range m, x ^ k * y ^ (n - 1 - k) = ∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))
⊢ (x - y) * (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) - ∑ x_1 ∈ range m, x ^ x_1 * (y ^ (m - 1 - x_1) * y ^ (n - m))) =
    x ^ n - x ^ m * y ^ (n - m)

Tactic:
simp_rw [← mul_assoc]

Goal state after:
R : Type u_1
inst✝ : Ring R
x y : R
h : Commute x y
m n : ℕ
hmn : m ≤ n
this : ∑ k ∈ range m, x ^ k * y ^ (n - 1 - k) = ∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))
⊢ (x - y) * (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) - ∑ x_1 ∈ range m, x ^ x_1 * y ^ (m - 1 - x_1) * y ^ (n - m)) =
    x ^ n - x ^ m * y ^ (n - m)
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
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) * ∑ k ∈ Ico m n, MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k) =
    MulOpposite.op x ^ n - MulOpposite.op x ^ m * MulOpposite.op y ^ (n - m)

Tactic:
convert! (Commute.op h).mul_geom_sum₂_Ico hmn

Goal state after:
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
⊢ ∀ (a : A) (s : Finset A), a ∉ s → P (Algebra.adjoin R ↑s) → P (Algebra.adjoin R ↑(insert a s))

Tactic:
intro x t _ h

Goal state after:
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))
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), f.coeff n ∈ I
n : ℕ
x✝ : n ∈ f.support
⊢ C (f.coeff n) * X ^ n ∈ map C I

Tactic:
mul_comm

Goal state after:
case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), f.coeff n ∈ I
n : ℕ
x✝ : n ∈ f.support
⊢ X ^ n * C (f.coeff n) ∈ map C I
Module: Mathlib.Algebra.Algebra.Subalgebra.Operations

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : ∑ i ∈ ι', l i * s i = 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
n : ι → ℕ
hn : ∀ (i : ι), s i ^ n i • x ∈ S'
s' : ι → ↥S' := fun x ↦ ⟨s x, ⋯⟩
l' : ι → ↥S' := fun x ↦ ⟨l x, ⋯⟩
e' : ∑ i ∈ ι', l' i * s' i = 1
this : Ideal.span (s' '' ↑ι') = ⊤
N : ℕ := ι'.sup n
hN : Ideal.span ((fun x ↦ x ^ N) '' s' '' ↑ι') = ⊤
⊢ x ∈ toSubmodule (ofId (↥S') S).range

Tactic:
apply (Algebra.ofId S' S).range.toSubmodule.mem_of_span_top_of_smul_mem _ hN

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : ∑ i ∈ ι', l i * s i = 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
n : ι → ℕ
hn : ∀ (i : ι), s i ^ n i • x ∈ S'
s' : ι → ↥S' := ⋯
l' : ι → ↥S' := ⋯
e' : ∑ i ∈ ι', l' i * s' i = 1
this : Ideal.span (s' '' ↑ι') = ⊤
N : ℕ := ⋯
hN : Ideal.span ((fun x ↦ x ^ N) '' s' '' ↑ι') = ⊤
⊢ ∀ (r : ↑((fun x ↦ x ^ N) '' s' '' ↑ι')), ↑r • x ∈ toSubmodule (ofId (↥S') S).range
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case inl
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (¬i = m ∨ ¬j = n) ∧ i + j = m + n
hi : i < m
⊢ f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P

Tactic:
mul_comm

Goal state after:
case inl
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (¬i = m ∨ ¬j = n) ∧ i + j = m + n
hi : i < m
⊢ g.coeff (i, j).2 * f.coeff (i, j).1 ∈ P
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
r : R
hr : (Ideal.span {r}).IsPrime
this : r ≠ 0
⊢ (Ideal.map C (Ideal.span {r})).IsPrime

Tactic:
infer_instance

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
⊢ Algebra.FiniteType A A

Tactic:
infer_instance

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case of
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
⊢ ∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = (of R M) m

Tactic:
have : m ∈ closure S := hS.symm ▸ mem_top _
    refine Submonoid.closure_induction (fun m hm => ?_) ?_ ?_ this
    · exact ⟨MvPolynomial.X ⟨m, hm⟩, MvPolynomial.aeval_X _ _⟩
    · exact ⟨1, map_one _⟩
    · rintro m₁ m₂ _ _ ⟨P₁, hP₁⟩ ⟨P₂, hP₂⟩
      exact
        ⟨P₁ * P₂, by
          rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single, one_mul]⟩

Goal state after:
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
h_eval₂_qpp' : ((aeval f) (q * (p * p'))) v = 0
⊢ ((aeval f) (p * q * q')) v = ((aeval f) (q' * (p * q))) v

Tactic:
mul_comm

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
⊢ ((aeval f) (q' * (p * q))) v = ((aeval f) (q' * (p * q))) v
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]
hpq : IsCoprime p q
⊢ ((aeval f) p).ker ⊔ ((aeval f) q).ker = ((aeval f) (p * q)).ker

Tactic:
apply le_antisymm sup_ker_aeval_le_ker_aeval_mul
  intro v hv
  rw [Submodule.mem_sup]
  rcases hpq with ⟨p', q', hpq'⟩
  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]
  have h_eval₂_pqq' :=
    calc
      aeval f (p * (q * q')) v = aeval f (q' * (p * q)) v := by rw [← mul_assoc, mul_comm]
      _ = 0 := by rw [aeval_mul, Module.End.mul_apply, LinearMap.mem_ker.1 hv, map_zero]
  rw [aeval_mul] at h_eval₂_qpp' h_eval₂_pqq'
  refine
    ⟨aeval f (q * q') v, LinearMap.mem_ker.1 h_eval₂_pqq', aeval f (p * p') v,
      LinearMap.mem_ker.1 h_eval₂_qpp', ?_⟩
  rw [add_comm, mul_comm p p', mul_comm q q']
  simpa only [map_add, map_mul, aeval_one] using! congr_arg (fun p : R[X] => aeval f p v) hpq'

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case refine_2.mem
R : Type u_1
inst✝ : CommRing R
M : Type u_1
x✝³ : AddCommMonoid M
x✝² : Module R M
x✝¹ : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective ⇑f
this✝² : AddCommGroup M := addCommMonoidToAddCommGroup R
this✝¹ : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective ⇑i := injective_subtype N
n : ↥N
hn : f n = 0
k : ℕ
mj : Fin k → M
hmj : Surjective ⇑((Module.piEquiv (Fin k) R M) mj)
b : Fin k → R
hb : ((Module.piEquiv (Fin k) R M) mj) b = i n
nj : Fin k → ↥N
hnj : ∀ (j : Fin k), f (nj j) = mj j
c : Fin k → Fin k → R
hc : ∀ (j : Fin k), ((Module.piEquiv (Fin k) R M) mj) (c j) = i (nj j)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this✝ : IsNoetherianRing ↥A
this : Module.Finite ↥A ↥M'
x✝ x : ↥N
hx : x ∈ {n} ∪ Set.range nj
⊢ (↑↥A f) x ∈ M'

Tactic:
change f x ∈ M'
      simp only [Set.singleton_union, Set.mem_insert_iff, Set.mem_range] at hx
      rcases hx with hx | ⟨j, rfl⟩
      · rw [hx, hn]; exact zero_mem _
      · exact subset_span (by simp [hnj])

Goal state after:
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℤ
⊢ ↑p ∣ b - a ↔ a ≡ b [ZMOD ↑p]

Tactic:
Int.modEq_iff_dvd

Goal state after:
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℤ
⊢ ↑p ∣ b - a ↔ ↑p ∣ b - a
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : CharZero R
p : ℕ
hp : Nat.Prime p
⊢ ↑p ≠ 0

Tactic:
by simp [hp.ne_zero]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Units.Fintype

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
⊢ Nat.card α - 1 = Nat.card { a // a ≠ 0 }

Tactic:
← Nat.card_congr (Equiv.sumCompl (· = (0 : α)))

Goal state after:
α : Type u_1
inst✝ : GroupWithZero α
⊢ Nat.card ({ a // a = 0 } ⊕ { a // ¬a = 0 }) - 1 = Nat.card { a // a ≠ 0 }
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: case inr
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy✝ : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hy : p ∣ y
⊢ y = p ∧ x = p

Tactic:
mul_comm

Goal state after:
case inr
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy✝ : y ≠ 1
h : y * x = p ^ 2
pdvdxy : p ∣ y * x
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hy : p ∣ y
⊢ y = p ∧ x = p
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
β : Type u_2
α' : Type u_3
β' : Type u_4
g : α → α'
g' : β → β'
t : α
ts ys : List α
r : List β
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ map g' (permutationsAux2 t ts r ys f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g ys) f').snd

Tactic:
induction ys generalizing f f' with

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
⊢ I • ⊤ ≤ Submodule.comap (Submodule.subtype (I ^ n)) (I ^ (n + 1))

Tactic:
intro

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
x✝ : ↥(I ^ n)
⊢ x✝ ∈ I • ⊤ → x✝ ∈ Submodule.comap (Submodule.subtype (I ^ n)) (I ^ (n + 1))