mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
x : ↥(f.domain ⊔ g.domain) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : ↥(f.domain ⊔ g.domain) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = ↑z
fg : ↥(f.domain ⊔ g.domain) → F := fun z ↦ ↑f ⟨x z, ⋯⟩ + ↑g ⟨y z, ⋯⟩
fg_eq : ∀ (x' : ↥f.domain) (y' : ↥g.domain) (z' : ↥(f.domain ⊔ g.domain)), ↑x' + ↑y' = ↑z' → fg z' = ↑f x' + ↑g y'
⊢ ∃ fg, ∀ (x : ↥f.domain) (y : ↥g.domain) (z : ↥(f.domain ⊔ g.domain)), ↑x + ↑y = ↑z → fg z = ↑f x + ↑g y

Tactic:
use { toFun := fg, map_add' := ?_, map_smul' := ?_ }, fg_eq

Goal state after:
case w.refine_1
R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
x : ↥(f.domain ⊔ g.domain) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : ↥(f.domain ⊔ g.domain) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = ↑z
fg : ↥(f.domain ⊔ g.domain) → F := fun z ↦ ↑f ⟨x z, ⋯⟩ + ↑g ⟨y z, ⋯⟩
fg_eq : ∀ (x' : ↥f.domain) (y' : ↥g.domain) (z' : ↥(f.domain ⊔ g.domain)), ↑x' + ↑y' = ↑z' → fg z' = ↑f x' + ↑g y'
⊢ ∀ (x y : ↥(f.domain ⊔ g.domain)), fg (x + y) = fg x + fg y

case w.refine_2
R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
x : ↥(f.domain ⊔ g.domain) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : ↥(f.domain ⊔ g.domain) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = ↑z
fg : ↥(f.domain ⊔ g.domain) → F := fun z ↦ ↑f ⟨x z, ⋯⟩ + ↑g ⟨y z, ⋯⟩
fg_eq : ∀ (x' : ↥f.domain) (y' : ↥g.domain) (z' : ↥(f.domain ⊔ g.domain)), ↑x' + ↑y' = ↑z' → fg z' = ↑f x' + ↑g y'
⊢ ∀ (m : R) (x : ↥(f.domain ⊔ g.domain)), fg (m • x) = σ m • fg x
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: case insert.h
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
comm : (↑(insert i s)).Pairwise (Commute on f)
h : (insert i s).SupIndep fun i ↦ (f i).ker
ih : (s.noncommProd f ⋯).ker = ⨆ x ∈ s, (f x).ker
⊢ Commute (f i) (s.noncommProd f ⋯)

Tactic:
exact s.noncommProd_commute _ _ _ fun j hj ↦
        comm (s.mem_insert_self i) (Finset.mem_insert_of_mem hj) (by lia)

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥⊥
⊢ Module.rank F ↥⊥ = 1

Tactic:
obtain ⟨κ, b⟩ := Module.Free.exists_basis (R := F) (M := (⊥ : Subalgebra F E))

Goal state after:
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
⊢ Module.rank F ↥⊥ = 1
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
⊢ (fun F ↦ ⇑F ∘ ι R) (liftAux R f) = f

Tactic:
by
      ext
      simp only [Function.comp_apply, ι_def]
      rfl

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
φ ψ χ : R[X]
⊢ (φ.comp ψ).comp χ = φ.comp (ψ.comp χ)

Tactic:
by
  refine Polynomial.induction_on φ ?_ ?_ ?_ <;>
    · intros
      simp_all only [add_comp, mul_comp, C_comp, X_comp, pow_succ, ← mul_assoc]

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

Goal state before:
pp: p : ℕ
hp : 2 ≤ p
m : ℕ
h : m < p
⊢ (∀ (x : ℕ), p = m * x → m = 1) ↔ ∀ (b : ℕ), p = m * b → ¬b < p

Tactic:
not_lt

Goal state after:
p : ℕ
hp : 2 ≤ p
m : ℕ
h : m < p
⊢ (∀ (x : ℕ), p = m * x → m = 1) ↔ ∀ (b : ℕ), p = m * b → p ≤ b
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R✝ : Type u_1
inst✝³ : AddMonoidWithOne R✝
p✝ a✝ b✝ : ℕ
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a b : ℕ
inst✝ : IsLeftCancelAdd R
hle : a ≤ b
⊢ ↑a = ↑b ↔ a % p = b % p

Tactic:
obtain ⟨c, rfl⟩ := Nat.exists_eq_add_of_le hle

Goal state after:
R✝ : Type u_1
inst✝³ : AddMonoidWithOne R✝
p✝ a✝ b : ℕ
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a : ℕ
inst✝ : IsLeftCancelAdd R
c : ℕ
hle : a ≤ a + c
⊢ ↑a = ↑(a + c) ↔ a % p = (a + c) % p
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case mpr
R✝ : Type u_1
inst✝³ : AddMonoidWithOne R✝
p✝ a✝ b : ℕ
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a : ℕ
inst✝ : IsLeftCancelAdd R
c : ℕ
hle : a ≤ a + c
h : a % p = (a + c) % p
this : (a + c - a) % p = 0
⊢ p ∣ c

Tactic:
simpa [Nat.dvd_iff_mod_eq_zero] using this

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

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
p q : ℕ
hp : CharP R p
hq : ExpChar R q
⊢ p = q ↔ Nat.Prime p

Tactic:
rcases hq with q | hq_prime
  · rw [(CharP.eq R hp (.ofCharZero R) : p = 0)]
    decide
  · exact ⟨fun hpq => hpq.symm ▸ hq_prime, fun _ => CharP.eq R hp ‹CharP R q›⟩

Goal state after:
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: case pos
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Ico b c)
x : α
hx : x ∈ Ico a c
g₀ : x ≤ b
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

Tactic:
exact h₀ ⟨hx.1, g₀⟩ (right_mem_Icc.2 (hx.1.trans g₀)) g₀

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
hf : f.toFun.ker = ⊥
⊢ f.inverse.graph = Submodule.map (↑(LinearEquiv.prodComm R E F)) f.graph

Tactic:
rw [inverse, Submodule.toLinearPMap_graph_eq _ (mem_inverse_graph_snd_eq_zero hf)]

Goal state after:
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: case pos
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Icc b c)
x : α
hx : x ∈ Icc a c
g₀ : x ≤ b
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

Tactic:
exact h₀ ⟨hx.1, g₀⟩ (right_mem_Icc.2 (hx.1.trans g₀)) g₀

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ (p * q).coeff 1 = p.coeff 0 * q.coeff 1 + p.coeff 1 * q.coeff 0

Tactic:
rw [coeff_mul, Nat.antidiagonal_eq_map]
  simp [sum_range_succ]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
n : ℕ
f : R[A]
⊢ (f ^ n).coeff.support.sup degb ≤ n • f.coeff.support.sup degb

Tactic:
← List.prod_replicate,

Goal state after:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
n : ℕ
f : R[A]
⊢ (List.replicate n f).prod.coeff.support.sup degb ≤ n • f.coeff.support.sup degb
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n k : ℕ
⊢ 1 ^ (n - k) * ↑(n.choose k) = ↑(n.choose k)

Tactic:
one_pow,

Goal state after:
R : Type u_1
inst✝ : Semiring R
n k : ℕ
⊢ 1 * ↑(n.choose k) = ↑(n.choose k)
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
h : (p ^ i).natDegree = i * p.natDegree
⊢ p ^ i = 0

Tactic:
← h,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (p ^ i).natDegree = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
h : (p ^ i).natDegree = i * p.natDegree
⊢ p ^ i = 0
Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic

Goal state before:
pp: R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
⊢ R[x] = adjoin R (⇑(aeval x) '' {X})

Tactic:
Set.image_singleton,

Goal state after:
R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
⊢ R[x] = R[(aeval x) X]
Module: Mathlib.Algebra.Polynomial.Eval.Degree

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

Tactic:
| succ k IH =>

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

Goal state before:
pp: case hf
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
dz : (map φ f).degree = 0
h : φ f.leadingCoeff = 0
u : IsUnit (φ f.leadingCoeff)
⊢ False

Tactic:
rw [h] at u

Goal state after:
case hf
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
dz : (map φ f).degree = 0
h : φ f.leadingCoeff = 0
u : IsUnit 0
⊢ False
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q p' q' : R[X]
hpq : p.comp q = X
hqp : q.comp p = X
hpq' : p'.comp q' = X
hqp' : q'.comp p' = X
h : p = p'
⊢ p.algEquivOfCompEqX q hpq hqp = p'.algEquivOfCompEqX q' hpq' hqp'

Tactic:
ext1; simp [h]

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

Goal state before:
pp: R : Type u
A : Type z
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
f : R[X]
G : Type u_3
inst✝² : Monoid G
inst✝¹ : MulSemiringAction G A
inst✝ : SMulCommClass G R A
g : G
x : A
⊢ (MulSemiringAction.toAlgHom R A g) ((aeval x) f) = g • (aeval x) f

Tactic:
MulSemiringAction.toAlgHom_apply

Goal state after:
R : Type u
A : Type z
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
f : R[X]
G : Type u_3
inst✝² : Monoid G
inst✝¹ : MulSemiringAction G A
inst✝ : SMulCommClass G R A
g : G
x : A
⊢ g • (aeval x) f = g • (aeval x) f
Module: Mathlib.Data.DFinsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : α → Type u_2
inst✝⁵ : DecidableEq α
M : α → Type u_3
P : α → Type u_4
inst✝⁴ : (a : α) → Zero (N a)
inst✝³ : (a : α) → Zero (M a)
inst✝² : (a : α) → Zero (P a)
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → DecidableEq (P a)
F : (a : α) → M a → N a → P a
F0 : ∀ (a : α), F a 0 0 = 0
f : Π₀ (a : α), M a
g₁ g₂ : Π₀ (a : α), N a
hF : ∀ (a : α) (f : M a), Function.Injective fun g ↦ F a f g
a : α
⊢ a ∈ (zipWith F F0 f g₁).neLocus (zipWith F F0 f g₂) ↔ a ∈ g₁.neLocus g₂

Tactic:
simpa only [mem_neLocus] using! (hF a _).ne_iff

Goal state after:
Module: Mathlib.Data.DFinsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : α → Type u_2
inst✝⁵ : DecidableEq α
M : α → Type u_3
P : α → Type u_4
inst✝⁴ : (a : α) → Zero (N a)
inst✝³ : (a : α) → Zero (M a)
inst✝² : (a : α) → Zero (P a)
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → DecidableEq (P a)
F : (a : α) → M a → N a → P a
F0 : ∀ (a : α), F a 0 0 = 0
f : Π₀ (a : α), M a
g₁ g₂ : Π₀ (a : α), N a
hF : ∀ (a : α) (f : M a), Function.Injective fun g ↦ F a f g
⊢ (zipWith F F0 f g₁).neLocus (zipWith F F0 f g₂) = g₁.neLocus g₂

Tactic:
by
  ext a
  simpa only [mem_neLocus] using! (hF a _).ne_iff

Goal state after:
Module: Mathlib.Data.DFinsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : α → Type u_2
inst✝⁵ : DecidableEq α
M : α → Type u_3
P : α → Type u_4
inst✝⁴ : (a : α) → Zero (N a)
inst✝³ : (a : α) → Zero (M a)
inst✝² : (a : α) → Zero (P a)
inst✝¹ : (a : α) → DecidableEq (M a)
inst✝ : (a : α) → DecidableEq (P a)
F : (a : α) → M a → N a → P a
F0 : ∀ (a : α), F a 0 0 = 0
f₁ f₂ : Π₀ (a : α), M a
g : Π₀ (a : α), N a
hF : ∀ (a : α) (g : N a), Function.Injective fun f ↦ F a f g
a : α
⊢ a ∈ (zipWith F F0 f₁ g).neLocus (zipWith F F0 f₂ g) ↔ a ∈ f₁.neLocus f₂

Tactic:
simpa only [mem_neLocus] using! (hF a _).ne_iff

Goal state after:
Module: Mathlib.Data.DFinsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : α → Type u_2
inst✝⁵ : DecidableEq α
M : α → Type u_3
P : α → Type u_4
inst✝⁴ : (a : α) → Zero (N a)
inst✝³ : (a : α) → Zero (M a)
inst✝² : (a : α) → Zero (P a)
inst✝¹ : (a : α) → DecidableEq (M a)
inst✝ : (a : α) → DecidableEq (P a)
F : (a : α) → M a → N a → P a
F0 : ∀ (a : α), F a 0 0 = 0
f₁ f₂ : Π₀ (a : α), M a
g : Π₀ (a : α), N a
hF : ∀ (a : α) (g : N a), Function.Injective fun f ↦ F a f g
⊢ (zipWith F F0 f₁ g).neLocus (zipWith F F0 f₂ g) = f₁.neLocus f₂

Tactic:
by
  ext a
  simpa only [mem_neLocus] using! (hF a _).ne_iff

Goal state after:
Module: Mathlib.Data.DFinsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → AddGroup (N a)
f g : Π₀ (a : α), N a
⊢ f.neLocus (f - g) = g.support

Tactic:
neLocus_self_sub_right

Goal state after:
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → AddGroup (N a)
f g : Π₀ (a : α), N a
⊢ g.support = g.support
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: case inl
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
i j : ℕ
hij : i + j = l + m
H : i = l → ¬j = m
hi : i < l
⊢ P.coeff i * Q.coeff j = 0

pp: case inr.inl
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
m : ℕ := Q.natDegree
i j : ℕ
IH : ∀ m > i, P.coeff m • Q = 0
hl : (P.coeff i • Q).natDegree = Q.natDegree
hij : i + j = i + m
H : i = i → ¬j = m
⊢ P.coeff i * Q.coeff j = 0

pp: case inr.inr
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
i j : ℕ
hij : i + j = l + m
H : i = l → ¬j = m
hi : l < i
⊢ P.coeff i * Q.coeff j = 0

Tactic:
· have hj : m < j := by lia
    rw [coeff_eq_zero_of_natDegree_lt hj, mul_zero]

Goal state after:
case inr.inl
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
m : ℕ := Q.natDegree
i j : ℕ
IH : ∀ m > i, P.coeff m • Q = 0
hl : (P.coeff i • Q).natDegree = Q.natDegree
hij : i + j = i + m
H : i = i → ¬j = m
⊢ P.coeff i * Q.coeff j = 0

case inr.inr
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
i j : ℕ
hij : i + j = l + m
H : i = l → ¬j = m
hi : l < i
⊢ P.coeff i * Q.coeff j = 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ
a : R
n : ℕ
⊢ C a * X s ^ n = (monomial (Finsupp.single s n)) a

Tactic:
by
  rw [← zero_add (Finsupp.single s n), monomial_add_single, C_apply]

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 : σ ↪ τ
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff (embDomain f d) ((rename ⇑f) φ) = coeff d φ

Tactic:
by
  rw [Finsupp.embDomain_eq_mapDomain f, coeff_rename_mapDomain f f.injective]

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

Goal state before:
pp: R : Type u
S₂ : Type w
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₂
f : R →+* S₂
g : σ → S₂
φ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), coeff d φ ≠ 0 → ∃ i ∈ d.support, g i = 0
⊢ (eval₂Hom f g) φ = 0

Tactic:
by
  rw [φ.as_sum, map_sum]
  refine Finset.sum_eq_zero fun d hd => ?_
  obtain ⟨i, hi, hgi⟩ : ∃ i ∈ d.support, g i = 0 := h d (Finsupp.mem_support_iff.mp hd)
  rw [eval₂Hom_monomial, Finsupp.prod, Finset.prod_eq_zero hi, mul_zero]
  rw [hgi, zero_pow]
  rwa [← Finsupp.mem_support_iff]

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hf : p.natDegree ≤ n + 1
hn : p.coeff n.succ = 0
h : p.natDegree = n.succ
⊢ False

Tactic:
← h,

Goal state after:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hf : p.natDegree ≤ n + 1
hn : p.coeff p.natDegree = 0
h : p.natDegree = n.succ
⊢ False
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
a : R
n : ℕ
inst✝ : Semiring R
this : DecidableEq R := Classical.decEq R
ha : a = 0
⊢ ((monomial n) a).natTrailingDegree ≤ n

Tactic:
by simp [ha]

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

Goal state before:
pp: R : Type u
a : R
n : ℕ
inst✝ : Semiring R
this : DecidableEq R := Classical.decEq R
ha : a = 0
⊢ ↑n ≤ ((monomial n) a).trailingDegree

Tactic:
by simp [ha]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).trailingDegree ≤ ↑(p.natTrailingDegree + q.natTrailingDegree)

Tactic:
apply trailingDegree_le_of_ne_zero

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).coeff (p.natTrailingDegree + q.natTrailingDegree) ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case neg
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)
H : ∀ x ∈ s, f x = 0
x : S
hx : x ∈ s
⊢ (f x).natDegree = ⊥

Tactic:
simp [H x hx]

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

Goal state before:
pp: case inl
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p.natDegree = 0
⊢ (map f p).natDegree ≤ 0

Tactic:
← h,

Goal state after:
case inl
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p.natDegree = 0
⊢ (map f p).natDegree ≤ p.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
pn : p.natDegree ≤ n
⊢ (p - q).natDegree ≤ n ↔ q.natDegree ≤ n

Tactic:
rwa [natDegree_sub, natDegree_sub_le_iff_left]

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

Goal state before:
pp: case succ
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
k : ℕ
IH : (p.comp^[k] q).natDegree = p.natDegree ^ k * q.natDegree
⊢ (p.comp^[k + 1] q).natDegree = p.natDegree ^ (k + 1) * q.natDegree

Tactic:
| succ k IH =>

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

Goal state before:
pp: case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
q : R[X]
hq : 0 < q.degree
⊢ (comp 0 q).degree = degree 0 * q.degree

Tactic:
zero_comp,

Goal state after:
case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
q : R[X]
hq : 0 < q.degree
⊢ degree 0 = degree 0 * q.degree
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 * 1 ^ (N - n) * x ^ n = i r * x ^ n

Tactic:
one_pow,

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 * x ^ n = i r * x ^ n
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
⊢ ((optionEquivLeft R σ) p).natDegree = degreeOf none p

Tactic:
by_cases c : p = 0
  · rw [c, map_zero, Polynomial.natDegree_zero, degreeOf_zero]
  · rw [Polynomial.natDegree, degree_optionEquivLeft R c, Nat.cast_withBot, WithBot.unbotD_coe]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : q.natDegree ≠ 0
a✝ : Nontrivial R
this : (p.comp q).natDegree = p.natDegree * q.natDegree
⊢ 1 * 1 ^ p.natDegree = 1

Tactic:
one_pow,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : q.natDegree ≠ 0
a✝ : Nontrivial R
this : (p.comp q).natDegree = p.natDegree * q.natDegree
⊢ 1 * 1 = 1
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
rwa [hp.leadingCoeff, one_mul, leadingCoeff_ne_zero]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
⊢ ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ p.natDegree → (φ (C r * X ^ n)).natDegree = fu (C r * X ^ n).natDegree

Tactic:
intro n r r0 _
    rw [natDegree_C_mul_X_pow _ _ r0, C_mul_X_pow_eq_monomial, φ_mon_nat _ _ r0]

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

Goal state before:
pp: case refine_2
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
f g : R[X]
hfg : p = f * g
⊢ (f * C g.leadingCoeff).Monic

Tactic:
rwa [Monic, leadingCoeff_mul, leadingCoeff_C, ← leadingCoeff_mul, ← hfg, ← Monic]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : ℕ
e : σ ≃ Fin n
φ : MvPolynomial (Option σ) R
⊢ (finSuccEquiv R n) ((rename ⇑(e.optionCongr.trans (_root_.finSuccEquiv n).symm)) φ) =
    Polynomial.map (rename ⇑e).toRingHom ((optionEquivLeft R σ) φ)

Tactic:
suffices (finSuccEquiv R n).toRingEquiv.toRingHom.comp (rename ((Equiv.optionCongr e).trans
        (_root_.finSuccEquiv n).symm)).toRingHom =
      (Polynomial.mapRingHom (rename e).toRingHom).comp (optionEquivLeft R σ) by
    exact DFunLike.congr_fun this φ
  apply ringHom_ext
  · simp [Polynomial.algebraMap_apply, algebraMap_eq, finSuccEquiv_apply, optionEquivLeft_apply]
  · rintro (i | i) <;> simp [finSuccEquiv_apply, optionEquivLeft_apply]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R
n i : ℕ
x✝ : i ∈ range n
⊢ x ^ i * 1 ^ (n - 1 - i) = x ^ i

Tactic:
one_pow,

Goal state after:
R : Type u_1
inst✝ : Semiring R
x : R
n i : ℕ
x✝ : i ∈ range n
⊢ x ^ i * 1 = x ^ i
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R
n : ℕ
this : (∑ i ∈ range n, (x + 1) ^ i * 1 ^ (n - 1 - i)) * x + 1 ^ n = (x + 1) ^ n
⊢ (∑ i ∈ range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n

Tactic:
one_pow,

Goal state after:
R : Type u_1
inst✝ : Semiring R
x : R
n : ℕ
this : (∑ i ∈ range n, (x + 1) ^ i * 1 ^ (n - 1 - i)) * x + 1 = (x + 1) ^ n
⊢ (∑ i ∈ range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n