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

Goal state before:
pp: R : Type u
M : Type v
ι : Type w
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndepOn R f s
hst : Disjoint s t
⊢ LinearIndepOn R (⇑(span R (f '' s)).mkQ ∘ f) t ↔ LinearIndepOn R f (s ∪ t)

Tactic:
linearIndepOn_union_iff_quotient hst,

Goal state after:
R : Type u
M : Type v
ι : Type w
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndepOn R f s
hst : Disjoint s t
⊢ LinearIndepOn R (⇑(span R (f '' s)).mkQ ∘ f) t ↔ LinearIndepOn R f s ∧ LinearIndepOn R (⇑(span R (f '' s)).mkQ ∘ f) t
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: case hsp
R✝ : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst✝⁸ : Semiring R✝
inst✝⁷ : CommSemiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R✝ M
R : Type u_2
V : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis m R ↥W
bQ : Basis n R (V ⧸ W)
b : m ⊕ n → V := Sum.elim (fun i ↦ ↑(bW i)) (surjInv ⋯ ∘ ⇑bQ)
br : ⇑W.mkQ ∘ b ∘ Sum.inr = ⇑bQ
⊢ span R (⇑W.mkQ '' range (surjInv ⋯ ∘ ⇑bQ)) = ⊤

Tactic:
← Set.range_comp,

Goal state after:
case hsp
R✝ : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst✝⁸ : Semiring R✝
inst✝⁷ : CommSemiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R✝ M
R : Type u_2
V : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis m R ↥W
bQ : Basis n R (V ⧸ W)
b : m ⊕ n → V := Sum.elim (fun i ↦ ↑(bW i)) (surjInv ⋯ ∘ ⇑bQ)
br : ⇑W.mkQ ∘ b ∘ Sum.inr = ⇑bQ
⊢ span R (range (⇑W.mkQ ∘ surjInv ⋯ ∘ ⇑bQ)) = ⊤
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W W' : Submodule K V
inst✝ : FiniteDimensional K ↥W
f : ↥W ≃ₗ[K] ↥W'
Q : Submodule K V
hQ : IsCompl W Q
eQ : (↥W × ↥Q) ≃ₗ[K] V := W.prodEquivOfIsCompl Q hQ
⊢ ∃ g, ∀ (x : ↥W), ↑(f x) = g ↑x

Tactic:
obtain ⟨Q', hQ'⟩ := Submodule.exists_isCompl W'

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W W' : Submodule K V
inst✝ : FiniteDimensional K ↥W
f : ↥W ≃ₗ[K] ↥W'
Q : Submodule K V
hQ : IsCompl W Q
eQ : (↥W × ↥Q) ≃ₗ[K] V := W.prodEquivOfIsCompl Q hQ
Q' : Submodule K V
hQ' : IsCompl W' Q'
⊢ ∃ g, ∀ (x : ↥W), ↑(f x) = g ↑x
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: case refine_1
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
this : Nontrivial K
h : Module.rank K V = 1
v₀ : V
hzero : v₀ = 0
hv : ∀ (v : V), ∃ r, 0 = v
⊢ False

Tactic:
exists_const

Goal state after:
case refine_1
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
this : Nontrivial K
h : Module.rank K V = 1
v₀ : V
hzero : v₀ = 0
hv : ∀ (v : V), 0 = v
⊢ False
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
f g : End K (Fin n → K)
hfg : f * g = 1
ginj : Injective ⇑g
i : (Fin n → K) →ₗ[K] Fin n → K
hi : g ∘ₗ i = id
this : i = f
⊢ g * f = 1

Tactic:
rwa [← this]

Goal state after:
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Submodule K V
w : V
hS : finrank K ↥S = 1
hw : w ∈ S
hw0 : w ≠ 0
this : FiniteDimensional K ↥S
⊢ finrank K ↥S ≤ finrank K ↥(K ∙ w)

Tactic:
rw [hS, finrank_span_singleton hw0]

Goal state after:
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
⊢ f ≤ f.sup g h

Tactic:
by
  refine ⟨le_sup_left, fun z₁ z₂ hz => ?_⟩
  rw [← add_zero (f _), ← g.map_zero]
  refine (sup_apply h _ _ _ ?_).symm
  simpa

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

Goal state before:
pp: p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
⊢ ∀ ⦃a b : ℕ⦄, p = a * b → IsUnit a ∨ IsUnit b

Tactic:
rintro a b rfl

Goal state after:
a b : ℕ
h : 2 ≤ a * b ∧ ∀ (m : ℕ), m ∣ a * b → m = 1 ∨ m = a * b
h1 : 1 < a * b
⊢ IsUnit a ∨ IsUnit b
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case inr
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ p.sqrt → ¬m ∣ p
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ mdvd : m ∣ p
k : ℕ
e : p = m * k
h✝ : mdvd = ⋯
hk : k ≤ p.sqrt
⊢ False

Tactic:
· rw [mul_comm] at e
          exact a k (Nat.lt_of_mul_lt_mul_right (a := m) (by rwa [one_mul, ← e])) hk ⟨m, e⟩

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

Goal state before:
pp: case neg
n m✝ : ℕ
n1 : ¬n = 1
⊢ 2 ≤ m✝ → m✝ ∣ n → n.minFac ≤ m✝

Tactic:
· apply (minFac_has_prop n1).2.2

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

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : AddMonoidWithOne R
q : ℕ
hq : ExpChar R q
inst✝ : CharZero R
⊢ 1 = q

pp: case prime
R : Type u_1
inst✝ : AddMonoidWithOne R
p q : ℕ
hq : ExpChar R q
hp' : Nat.Prime p
hchar✝ : CharP R p
⊢ p = q

Tactic:
· rcases hq with hq | hq'
    exacts [rfl, False.elim (Nat.not_prime_zero (CharP.eq R ‹_› (CharP.ofCharZero R) ▸ hq'))]

Goal state after:
case prime
R : Type u_1
inst✝ : AddMonoidWithOne R
p q : ℕ
hq : ExpChar R q
hp' : Nat.Prime p
hchar✝ : CharP R p
⊢ p = q
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: case h₀
R : Type u
inst✝ : Semiring R
p : R[X]
n d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + n)
h2 : (i, j) ≠ (d, n)
⊢ (p.coeff (i, j).1 * if (i, j).2 = n then 1 else 0) = 0

Tactic:
if_neg,

Goal state after:
case h₀
R : Type u
inst✝ : Semiring R
p : R[X]
n d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + n)
h2 : (i, j) ≠ (d, n)
⊢ p.coeff (i, j).1 * 0 = 0

case h₀.hnc
R : Type u
inst✝ : Semiring R
p : R[X]
n d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + n)
h2 : (i, j) ≠ (d, n)
⊢ ¬(i, j).2 = n
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_4
M : Type u_7
inst✝³ : CommSemiring R
inst✝² : AddMonoid M
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : Multiplicative M →* A
f : R[M]
⊢ ((lift R A M) F) f = f.coeff.sum fun a b ↦ b • F (Multiplicative.ofAdd a)

Tactic:
by
  simp only [lift_apply', Algebra.smul_def]

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ antidiagonal d
⊢ (p.coeff x.1 * if x.2 = n then 1 else 0) = 0

Tactic:
if_neg,

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ antidiagonal d
⊢ p.coeff x.1 * 0 = 0

case neg.hnc
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ antidiagonal d
⊢ ¬x.2 = n
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case refine_2
R : Type u_7
A : Type u_8
B : Type u_9
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : SemilatticeSup B
inst✝² : OrderBot B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      supDegree D (∏ i ∈ s, f i) ≤ ∑ i ∈ s, supDegree D (f i) →
        supDegree D (∏ i ∈ insert a s, f i) ≤ ∑ i ∈ insert a s, supDegree D (f i)

Tactic:
intro i s his ih
    rw [Finset.prod_insert his, Finset.sum_insert his]
    exact (supDegree_mul_le hadd).trans (by gcongr)

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ AddMonoidAlgebra.supDegree id p.toFinsupp = p.natDegree

Tactic:
obtain rfl | h := eq_or_ne p 0
  · simp
  apply WithBot.coe_injective
  rw [← AddMonoidAlgebra.supDegree_withBot_some_comp, Function.comp_id, supDegree_eq_degree,
    degree_eq_natDegree h, Nat.cast_withBot]
  rwa [support_toFinsupp, nonempty_iff_ne_empty, Ne, support_eq_empty]

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

Goal state before:
pp: case refine_1
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j) ∈ antidiagonal (p.natDegree + q.natDegree)
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
rw [mem_antidiagonal] at h₁

Goal state after:
case refine_1
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
this✝ : Nontrivial R
this : p.leadingCoeff * X.leadingCoeff ≠ 0
⊢ ↑p.natDegree < ↑p.natDegree + X.degree

Tactic:
degree_X,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
this✝ : Nontrivial R
this : p.leadingCoeff * X.leadingCoeff ≠ 0
⊢ ↑p.natDegree < ↑p.natDegree + 1
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
h : (-q).degree < p.degree
⊢ (p - q).degree = p.degree

Tactic:
rw [sub_eq_add_neg, degree_add_eq_left_of_degree_lt h]

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

Goal state before:
pp: S : Type v
inst✝ : CommRing S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ eval z f
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
hi : i ∉ f.support
⊢ f.coeff i * z ^ i = 0

Tactic:
notMem_support_iff

Goal state after:
S : Type v
inst✝ : CommRing S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ eval z f
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
hi : f.coeff i = 0
⊢ f.coeff i * z ^ i = 0
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 - g).neLocus f = g.support

Tactic:
by
  rw [neLocus_comm, neLocus_self_sub_right]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
m : σ →₀ ℕ
⊢ coeff m (X i) = if Finsupp.single i 1 = m then 1 else 0

Tactic:
by
  rw [← coeff_X_pow, pow_one]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ p.support \ q.support ⊔ q.support \ p.support ⊆ (p + q).support

Tactic:
Finset.sup_eq_union

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ p.support \ q.support ∪ q.support \ p.support ⊆ (p + q).support
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
g : τ → α
p : MvPolynomial σ R
⊢ (rename g) ((rename f) p) = (rename (g ∘ f)) p

Tactic:
by
  simp [MvPolynomial, rename, mapDomain.addMonoidHom_comp]

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

Goal state before:
pp: case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
φ : MvPolynomial σ R
C : (σ →₀ ℕ) → R
hc : ∀ (i : σ →₀ ℕ), coeff i φ = r * C i
c' : (σ →₀ ℕ) → R := fun i ↦ if i ∈ φ.support then C i else 0
ψ : MvPolynomial σ R := ∑ i ∈ φ.support, (monomial i) (c' i)
i : σ →₀ ℕ
hi : i ∉ φ.support
⊢ coeff i φ = r * 0

Tactic:
notMem_support_iff

Goal state after:
case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
φ : MvPolynomial σ R
C : (σ →₀ ℕ) → R
hc : ∀ (i : σ →₀ ℕ), coeff i φ = r * C i
c' : (σ →₀ ℕ) → R := fun i ↦ if i ∈ φ.support then C i else 0
ψ : MvPolynomial σ R := ∑ i ∈ φ.support, (monomial i) (c' i)
i : σ →₀ ℕ
hi : coeff i φ = 0
⊢ coeff i φ = r * 0
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
a : τ
ha : a ∈ s.support
hs : a ∉ range f
⊢ ((algebraMap R (MvPolynomial σ R)) c *
      s.prod fun i k ↦ (if h : i ∈ range f then X ((Equiv.ofInjective f hf).symm ⟨i, h⟩) else 0) ^ k) =
    0

Tactic:
Finsupp.prod

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
s : τ →₀ ℕ
c : R
a : τ
ha : a ∈ s.support
hs : a ∉ range f
⊢ (algebraMap R (MvPolynomial σ R)) c *
      ∏ a ∈ s.support, (if h : a ∈ range f then X ((Equiv.ofInjective f hf).symm ⟨a, h⟩) else 0) ^ s a =
    0
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p.degrees = 0 ↔ p.support ⊆ {0}

Tactic:
by
  rw [Finset.subset_singleton_iff', Multiset.eq_zero_iff_forall_notMem]
  refine ⟨fun h s hs ↦ ?_, fun h i hi ↦ ?_⟩
  · rw [← Finsupp.support_eq_empty]
    simp only [mem_degrees] at h
    grind
  rcases mem_degrees.mp hi with ⟨s, hs1, hs2⟩
  have := Finsupp.support_eq_empty.mpr (h s <| mem_support_iff.mpr hs1) ▸ hs2
  grind

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

Goal state before:
pp: R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
⊢ coeffsIn σ (M * N) = coeffsIn σ M * coeffsIn σ N

Tactic:
classical
  refine le_antisymm (coeffsIn_le.2 ?_) ?_
  · intro r hr s
    induction hr using Submodule.mul_induction_on' with
    | mem_mul_mem m hm n hn =>
      rw [← add_zero s, ← monomial_mul]
      apply Submodule.mul_mem_mul <;> simpa
    | add x _ y _ hx hy =>
      simpa [map_add] using add_mem hx hy
  · rw [Submodule.mul_le]
    intro x hx y hy k
    rw [MvPolynomial.coeff_mul]
    exact sum_mem fun c hc ↦ Submodule.mul_mem_mul (hx _) (hy _)

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

Goal state before:
pp: case neg
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f : R →+* S
p : MvPolynomial σ R
s : subS
hs : ∀ i ∈ p.support, f (coeff i p) ∈ s
v : σ → S
hv : ∀ (i : σ), v i ∈ s
i : σ →₀ ℕ
hi : i ∉ p.support
⊢ f (coeff i p) ∈ s

Tactic:
· rw [MvPolynomial.notMem_support_iff.1 hi, f.map_zero]
      exact zero_mem s

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j) ∈ antidiagonal (p.natTrailingDegree + q.natTrailingDegree)
h₂ : (i, j) ≠ (p.natTrailingDegree, q.natTrailingDegree)
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
rw [mem_antidiagonal] at h₁

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natTrailingDegree + q.natTrailingDegree
h₂ : (i, j) ≠ (p.natTrailingDegree, q.natTrailingDegree)
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0
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).coeff (p.natTrailingDegree + q.natTrailingDegree) ≠ 0

Tactic:
coeff_mul_natTrailingDegree_add_natTrailingDegree

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.trailingCoeff * q.trailingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
nd : ¬n = p.natDegree
⊢ (if n = (p + q).natDegree then 0 else p.coeff n + q.coeff n) = (if n = p.natDegree then 0 else p.coeff n) + q.coeff n

Tactic:
if_neg,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
nd : ¬n = p.natDegree
⊢ p.coeff n + q.coeff n = (if n = p.natDegree then 0 else p.coeff n) + q.coeff n

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : ¬n = q.natDegree
⊢ (if n = (p + q).natDegree then 0 else p.coeff n + q.coeff n) = p.coeff n + if n = q.natDegree then 0 else q.coeff n

Tactic:
if_neg,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : ¬n = q.natDegree
⊢ p.coeff n + q.coeff n = p.coeff n + if n = q.natDegree then 0 else q.coeff n

case neg.hnc
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : ¬n = q.natDegree
⊢ ¬n = (p + q).natDegree
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 fun i ↦ (f i).degree) = ↑(s.sup fun i ↦ (f i).natDegree)

Tactic:
rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs,
        Nat.cast_withBot, Finset.coe_sup' hs, ←
        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.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ f.eraseLead.coeff (f.natDegree - 1) = if f.natDegree = 0 then 0 else f.coeff (f.natDegree - 1)

Tactic:
if_neg,

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ f.eraseLead.coeff (f.natDegree - 1) = f.coeff (f.natDegree - 1)

case hnc
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ ¬f.natDegree = 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case neg
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:
by_cases p0 : p = 0
    · simp only [p0, zero_comp, natDegree_zero, zero_mul]
    · simp only [Ne, mul_eq_zero, leadingCoeff_eq_zero, p0, natDegree_comp_eq_of_mul_ne_zero,
        ne_zero_of_natDegree_gt (Nat.pos_of_ne_zero q0), not_false_eq_true, pow_ne_zero, or_self]

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
⊢ (X ^ n + p).coeff n = 1

Tactic:
by rw [coeff_add, coeff_X_pow, if_pos rfl, coeff_eq_zero_of_degree_lt H, add_zero]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.reverse.natTrailingDegree = 0

Tactic:
rw [natTrailingDegree_eq_zero, reverse_eq_zero, coeff_zero_reverse, leadingCoeff_ne_zero]

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f = 0 ∨ f ≠ 0
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.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
⊢ ∀ (a : ℕ), ∑ b, (C (x b) * X ^ k b).coeff a ≠ 0 ↔ a ∈ image k univ

Tactic:
coeff_C_mul_X_pow,

Goal state after:
R : Type u_1
inst✝ : Semiring R
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
⊢ ∀ (a : ℕ), (∑ x_1, if a = k x_1 then x x_1 else 0) ≠ 0 ↔ a ∈ image k univ
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
hj : ¬∃ j₀, j₀.castSucc = j
⊢ k i ∈ f.eraseLead.support

Tactic:
rw [mem_support_iff, hf, finsetSum_coeff]

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
hj : ¬∃ j₀, j₀.castSucc = j
⊢ ∑ b, (C (x b) * X ^ k b).coeff (k i) ≠ 0
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : WithBot ℕ
f : R[X]
⊢ f ∈ degreeLE R n ↔ f.degree ≤ n

Tactic:
by
  simp only [degreeLE, Submodule.mem_iInf, degree_le_iff_coeff_zero, LinearMap.mem_ker]; rfl

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

Goal state before:
pp: R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
p : ↥(degreeLT R n)
⊢ (X ^ n + ↑p).natDegree = n

Tactic:
natDegree_add_eq_left_of_degree_lt

Goal state after:
R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
p : ↥(degreeLT R n)
⊢ (X ^ n).natDegree = n

R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
p : ↥(degreeLT R n)
⊢ (↑p).degree < (X ^ n).degree
Module: Mathlib.RingTheory.Adjoin.Tower

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
s : Finset S
hs : adjoin R ↑s = ⊤
t : Finset A
ht : adjoin S ↑t = ⊤
⊢ adjoin R (⇑(algebraMap S A) '' ↑s ∪ ↑t) = ⊤

Tactic:
Algebra.adjoin_algebraMap_image_union_eq_adjoin_adjoin,

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
s : Finset S
hs : adjoin R ↑s = ⊤
t : Finset A
ht : adjoin S ↑t = ⊤
⊢ Subalgebra.restrictScalars R (adjoin ↥(adjoin R ↑s) ↑t) = ⊤
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ ⊤.leadingCoeff = ⊤

Tactic:
simp [← map_top C]

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

Goal state before:
pp: case e'_2
R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Finite σ
this : Fintype σ
d : ℕ
hd : Prime (C r) ↔ Prime r
⊢ Prime r ↔ Prime (Polynomial.C (C r))

Tactic:
· simp [← hd, Polynomial.prime_C_iff]

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: 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
⊢ Function.Injective ⇑f

Tactic:
let := addCommMonoidToAddCommGroup R (M := N)

Goal state after:
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
⊢ Function.Injective ⇑f