mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x : ↥(unitsFstOne R A)
⊢ PreQuasiregular.equiv.symm (PreQuasiregular.equiv (↑↑x⁻¹).toProd.2 * PreQuasiregular.equiv (↑↑x).toProd.2) =
    PreQuasiregular.equiv.symm 1

Tactic:
simpa [-Units.inv_mul] using congr($(x.val.inv_mul).snd)

Goal state after:
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x : A
hx : IsUnit (1 + ↑x)
⊢ IsQuasiregular x

Tactic:
· exact ⟨(Unitization.unitsFstOne_mulEquiv_quasiregular R) ⟨hx.unit, by simp⟩, by simp⟩

Goal state after:
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁵ : Semifield R
inst✝⁴ : Semifield S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra S A
a b : A
f : S → R
ha : SpectrumRestricts a f
h : spectrum S a = spectrum S b
⊢ Set.RightInvOn f (⇑(algebraMap R S)) (quasispectrum S b)

Tactic:
rw [quasispectrum_eq_spectrum_union_zero, ← h, ← quasispectrum_eq_spectrum_union_zero]
    exact QuasispectrumRestricts.rightInvOn ha

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

Goal state before:
pp: case inl_add_inr.inl_add_inr
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
x_r : R
x_a : A
r✝ : R
a✝ : A
⊢ (algebraMap R C) x_r * (algebraMap R C) r✝ + (x_r • φ a✝ + r✝ • φ x_a + φ x_a * φ a✝) =
    (algebraMap R C) x_r * (algebraMap R C) r✝ + (algebraMap R C) x_r * φ a✝ +
      ((algebraMap R C) r✝ * φ x_a + φ x_a * φ a✝)

Tactic:
simp only [Algebra.algebraMap_eq_smul_one, smul_one_mul, add_assoc]

Goal state after:
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R✝ : Type u_1
A : Type u_2
F : Type u_3
R : Type u_4
S : Type u_5
inst✝⁹ : NonUnitalSemiring R
inst✝⁸ : PartialOrder R
inst✝⁷ : StarRing R
inst✝⁶ : StarOrderedRing R
inst✝⁵ : NonUnitalSemiring S
inst✝⁴ : PartialOrder S
inst✝³ : StarRing S
inst✝² : StarOrderedRing S
inst✝¹ : EquivLike F R S
inst✝ : StarRingEquivClass F R S
f : F
x y : R
⊢ f x ≤ f y ↔ x ≤ y

Tactic:
by
    refine ⟨fun h ↦ ?_, map_rel f⟩
    let f_inv : S →⋆ₙ+* R := (f : R ≃⋆+* S).symm
    have f_inv_f (r : R) : f_inv (f r) = r := EquivLike.inv_apply_apply f r
    rw [← f_inv_f x, ← f_inv_f y]
    exact NonUnitalStarRingHom.map_le_map_of_map_star f_inv h

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

Goal state before:
pp: 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
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Free R M
inst✝³ : (i : η) → AddCommMonoid (φ i)
inst✝² : (i : η) → Module R (φ i)
inst✝¹ : ∀ (i : η), Free R (φ i)
inst✝ : Fintype η
n : ℕ
hn✝ : Module.rank R M = ↑n
this✝ : Nontrivial R
this : lift.{u, v} ↑n = lift.{v, u} ↑n
hn : lift.{u, v} (Module.rank R M) = lift.{u, v} ↑n
⊢ M ≃ₗ[R] Fin n → R

Tactic:
rw [this] at hn

Goal state after:
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
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Free R M
inst✝³ : (i : η) → AddCommMonoid (φ i)
inst✝² : (i : η) → Module R (φ i)
inst✝¹ : ∀ (i : η), Free R (φ i)
inst✝ : Fintype η
n : ℕ
hn✝ : Module.rank R M = ↑n
this✝ : Nontrivial R
this : lift.{u, v} ↑n = lift.{v, u} ↑n
hn : lift.{u, v} (Module.rank R M) = lift.{v, u} ↑n
⊢ M ≃ₗ[R] Fin n → R
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s

Tactic:
rcases hn.eq_or_lt with h | h

Goal state after:
case inl
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
h : ↑n = Module.rank R M
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s

case inr
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
h : ↑n < Module.rank R M
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: case right
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
T : Submodule K V
hT : T < K ∙ v
⊢ T = ⊥

Tactic:
by_contra h

Goal state after:
case right
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
T : Submodule K V
hT : T < K ∙ v
h : ¬T = ⊥
⊢ False
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u
inst✝ : Semiring R
ι : Type u_1
⊢ Module.Finite R (ι →₀ R) ↔ Subsingleton R ∨ Finite ι

Tactic:
simp only [finite_finsupp_iff, Finite.self, true_and, or_iff_right_iff_imp]
  exact fun _ ↦ .inr inferInstance

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

Goal state before:
pp: case refine_2
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Submodule K V
hS : finrank K ↥S = 1
T : Submodule K V
hT : T < S
this✝ : FiniteDimensional K ↥S
this : FiniteDimensional K ↥T
⊢ finrank K ↥T = 0

Tactic:
by_contra h

Goal state after:
case refine_2
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Submodule K V
hS : finrank K ↥S = 1
T : Submodule K V
hT : T < S
this✝ : FiniteDimensional K ↥S
this : FiniteDimensional K ↥T
h : ¬finrank K ↥T = 0
⊢ False
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case mk.ofScalar
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
x : R
⊢ (liftAux R ((fun F ↦ ⇑F ∘ ι R) F)) (Quot.mk (Rel R X) (Pre.ofScalar x)) = F (Quot.mk (Rel R X) (Pre.ofScalar x))

Tactic:
| ofScalar x =>

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = (algebraMap R (FreeAlgebra R X)) r
f0 : FreeAlgebra R X →ₐ[R] R := (lift R) 0
f1 : FreeAlgebra R X →ₐ[R] R := (lift R) 1
hf0 : r = 0
hf1 : r = 1
⊢ False

Tactic:
exact zero_ne_one (hf0.symm.trans hf1)

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p r : R[X]
k : ℕ
⊢ (p * X ^ k).comp r = p.comp r * r ^ k

Tactic:
induction k with
  | zero => simp
  | succ k ih => simp [ih, pow_succ, ← mul_assoc, mul_X_comp]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case mp
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
M : Type u_7
inst✝³ : Monoid M
inst✝² : DistribMulAction M F
inst✝¹ : Module R F
inst✝ : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
h : ∃ y, ↑y = (x_fst, x_snd).1 ∧ ↑(z • f) y = (x_fst, x_snd).2
⊢ (x_fst, x_snd) ∈ Submodule.map (LinearMap.id.prodMap (z • LinearMap.id)) f.graph

Tactic:
rcases h with ⟨y, hy, h⟩

Goal state after:
case mp
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
M : Type u_7
inst✝³ : Monoid M
inst✝² : DistribMulAction M F
inst✝¹ : Module R F
inst✝ : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
y : ↥(z • f).domain
hy : ↑y = (x_fst, x_snd).1
h : ↑(z • f) y = (x_fst, x_snd).2
⊢ (x_fst, x_snd) ∈ Submodule.map (LinearMap.id.prodMap (z • LinearMap.id)) f.graph
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
⊢ ringChar R = 0 ↔ CharZero R

Tactic:
ringChar.eq_iff,

Goal state after:
R : Type u_1
inst✝ : NonAssocRing R
⊢ CharP R 0 ↔ CharZero R
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case mp
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
x_fst : E
x_snd : F
h : ∃ y, ↑y = (x_fst, x_snd).1 ∧ ↑(-f) y = (x_fst, x_snd).2
⊢ (x_fst, x_snd) ∈ Submodule.map (LinearMap.id.prodMap (-LinearMap.id)) f.graph

Tactic:
rcases h with ⟨y, hy, h⟩

Goal state after:
case mp
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
x_fst : E
x_snd : F
y : ↥(-f).domain
hy : ↑y = (x_fst, x_snd).1
h : ↑(-f) y = (x_fst, x_snd).2
⊢ (x_fst, x_snd) ∈ Submodule.map (LinearMap.id.prodMap (-LinearMap.id)) f.graph
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 g : E →ₗ.[R] F
h : f ≤ g
x : E × F
y : ↥f.domain
hx : ↑y = x.1 ∧ ↑f y = x.2
⊢ ↑g ⟨x.1, ⋯⟩ = ↑f y

Tactic:
refine (h.2 ?_).symm

Goal state after:
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 g : E →ₗ.[R] F
h : f ≤ g
x : E × F
y : ↥f.domain
hx : ↑y = x.1 ∧ ↑f y = x.2
⊢ ↑y = ↑⟨x.1, ⋯⟩
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ #(p * q).support ≤ #p.support * #q.support

Tactic:
by
  calc #(p * q).support
    _ = #(p.toFinsupp * q.toFinsupp).coeff.support := by rw [← support_toFinsupp, toFinsupp_mul]
    _ ≤ #(p.toFinsupp.coeff.support + q.toFinsupp.coeff.support) := by
      grw [AddMonoidAlgebra.support_coeff_mul_subset]
    _ ≤ #p.support * #q.support := Finset.card_image₂_le ..

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
f : R[X]
n✝ : ℕ
⊢ a * f.coeff n✝ = (a • f).coeff n✝

Tactic:
coeff_smul,

Goal state after:
R : Type u
inst✝ : Semiring R
a : R
f : R[X]
n✝ : ℕ
⊢ a * f.coeff n✝ = a • f.coeff n✝
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type v
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
D : α → β
s : Finset α
inst✝ : Nonempty α
b : β
hb : b ∈ range D
hmem : Function.invFun D b ∈ s
hmax : ∀ a ∈ s, D a ≤ b
⊢ s.sup D = b

Tactic:
by
  obtain ⟨a, rfl⟩ := hb
  rw [← Function.apply_invFun_apply (f := D)]
  apply sup_eq_of_isMaxOn hmem; intro
  rw [Function.apply_invFun_apply (f := D)]; apply hmax

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
f : R[A]
fs : List R[A]
⊢ (f :: fs).prod.coeff.support.sup degb ≤ (List.map (fun f ↦ f.coeff.support.sup degb) (f :: fs)).sum

Tactic:
by
    rw [List.prod_cons, List.map_cons, List.sum_cons]
    grw [sup_support_coeff_mul_le degbm, sup_support_list_prod_le degb0 degbm]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : CommSemiring R
inst✝⁴ : AddMonoid M
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
⊢ Additive.ofMul (domCongr R A 0) = 0

Tactic:
ext; simp [AddAut.zero_def]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
r : R
⊢ (p * (monomial n) r).coeff (d + n) = p.coeff d * r

Tactic:
rw [← C_mul_X_pow_eq_monomial, ← X_pow_mul, ← mul_assoc, coeff_mul_C, coeff_mul_X_pow]

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

Goal state before:
pp: case h₁
R : Type u
inst✝ : Semiring R
r : R
n k : ℕ
⊢ k ∉ range (n + 1) → (X ^ k).coeff k * r ^ (n - k) * ↑(n.choose k) = 0

Tactic:
· simp only [coeff_X_pow_self, one_mul, not_lt, Finset.mem_range]
    intro h
    rw [Nat.choose_eq_zero_of_lt h, Nat.cast_zero, mul_zero]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree < p.natDegree
⊢ p.natDegree = q.natDegree

Tactic:
by_contra h

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree < p.natDegree
h : ¬p.natDegree = q.natDegree
⊢ False
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree < p.natDegree
h : ¬p.natDegree = q.natDegree
x✝ : p.natDegree < q.natDegree ∨ q.natDegree < p.natDegree
⊢ False

Tactic:
cases Nat.lt_or_lt_of_ne h with

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.degree = q.degree
hlc : p.leadingCoeff + q.leadingCoeff ≠ 0
⊢ (p + q).leadingCoeff = p.leadingCoeff + q.leadingCoeff

Tactic:
have : natDegree (p + q) = natDegree p := by
    apply natDegree_eq_of_degree_eq
    rw [degree_add_eq_of_leadingCoeff_add_ne_zero hlc, h, max_self]
  simp only [leadingCoeff, this, natDegree_eq_of_degree_eq h, coeff_add]

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

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

Tactic:
refine mt ?_ h; exact fun hp => by rw [hp, leadingCoeff_zero, zero_mul]

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

Goal state before:
pp: R : Type u
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
h : p.leadingCoeff ^ n.succ ≠ 0
h₁ : p.leadingCoeff ^ n = 0
⊢ p.leadingCoeff ^ n.succ = 0

Tactic:
by rw [pow_succ, h₁, zero_mul]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ (n + 1) ≠ 0
h₁ : p.leadingCoeff ^ n = 0
⊢ p.leadingCoeff ^ (n + 1) = 0

Tactic:
by rw [pow_succ, h₁, zero_mul]

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

Goal state before:
pp: 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

Tactic:
hp1

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

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
ha : a ≠ 0
hp : IsRightRegular p.leadingCoeff
⊢ (a • p).coeff p.natDegree ≠ 0

Tactic:
coeff_smul,

Goal state after:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
ha : a ≠ 0
hp : IsRightRegular p.leadingCoeff
⊢ a • p.coeff p.natDegree ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

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

Tactic:
exact mul_ne_zero (mt leadingCoeff_eq_zero.1 hp) (mt leadingCoeff_eq_zero.1 hq)

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

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

Tactic:
rintro ⟨n, a, rfl⟩

Goal state after:
case mpr
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ ((monomial n) a).support.card ≤ 1
Module: Mathlib.Data.Finsupp.Antidiagonal

Goal state before:
pp: case refine_2
α : Type u
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
u v : β →₀ ℕ
h : u + v = embDomain f y
⊢ comapDomain (⇑f) u ⋯ + comapDomain (⇑f) v ⋯ = y

Tactic:
← comapDomain_add_of_injective f.injective,

Goal state after:
case refine_2
α : Type u
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
u v : β →₀ ℕ
h : u + v = embDomain f y
⊢ comapDomain (⇑f) (u + v) ⋯ = y
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
β : Type u_4
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : AddCommMonoid β
inst✝² : Preorder β
inst✝¹ : IsOrderedAddMonoid β
inst✝ : DecidableEq ι
f₁ f₂ : ι →₀ α
h : ι → α → β
hf : f₁ ≤ f₂
hh : ∀ i ∈ f₁.support ∪ f₂.support, Monotone (h i)
hh₀ : ∀ i ∈ f₁.support ∪ f₂.support, h i 0 = 0
⊢ f₁.sum h ≤ f₂.sum h

Tactic:
sum_of_support_subset _ Finset.subset_union_left _ hh₀,

Goal state after:
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : AddCommMonoid β
inst✝² : Preorder β
inst✝¹ : IsOrderedAddMonoid β
inst✝ : DecidableEq ι
f₁ f₂ : ι →₀ α
h : ι → α → β
hf : f₁ ≤ f₂
hh : ∀ i ∈ f₁.support ∪ f₂.support, Monotone (h i)
hh₀ : ∀ i ∈ f₁.support ∪ f₂.support, h i 0 = 0
⊢ ∑ x ∈ f₁.support ∪ f₂.support, h x (f₁ x) ≤ f₂.sum h
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : CommSemiring A'
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p✝ q✝ : R[X]
x : A
p q : R[X]
hpq : p.comp q = X
hqp : q.comp p = X
⊢ R[X] ≃ₐ[R] R[X]

Tactic:
refine AlgEquiv.ofAlgHom (aeval p) (aeval q) ?_ ?_ <;>
    exact AlgHom.ext fun _ ↦ by simp [← comp_eq_aeval, comp_assoc, hpq, hqp]

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

Goal state before:
pp: 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
this : P.coeff l * Q.leadingCoeff = 0
⊢ (P.coeff l • Q).coeff (P.coeff l • Q).natDegree = 0

Tactic:
coeff_smul,

Goal state after:
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
this : P.coeff l * Q.leadingCoeff = 0
⊢ P.coeff l • Q.coeff (P.coeff l • Q).natDegree = 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : ℕ
⊢ C ↑n = ↑n

Tactic:
by
  induction n <;> simp [*]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
a : R
ha : IsRegular a
⊢ IsRegular ((MvPolynomial.monomial m) a)

Tactic:
rw [← isLeftRegular_iff_isRegular]
  intro p q h
  ext d
  have h' := congr_arg (coeff (m + d)) h
  simp only [coeff_monomial_mul] at h'
  rw [← ha.left.eq_iff, h']

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

Goal state before:
pp: case pos
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
p : MvPolynomial σ S
h : ↑p.support ⊆ (fun m ↦ coeff m p) ⁻¹' ↑M
i : σ →₀ ℕ
hp : i ∈ p.support
⊢ coeff i p ∈ M

pp: case neg
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
p : MvPolynomial σ S
h : ↑p.support ⊆ (fun m ↦ coeff m p) ⁻¹' ↑M
i : σ →₀ ℕ
hp : i ∉ p.support
⊢ coeff i p ∈ M

Tactic:
· exact h hp

Goal state after:
case neg
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
p : MvPolynomial σ S
h : ↑p.support ⊆ (fun m ↦ coeff m p) ⁻¹' ↑M
i : σ →₀ ℕ
hp : i ∉ p.support
⊢ coeff i p ∈ M
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)

Tactic:
intro a
    simp only [constantCoeff_C, rename_C]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R
x : σ →₀ ℕ
H : x ∈ f.support
v : σ
h : v ∉ f.vars
⊢ x v = 0

Tactic:
by
  contrapose! h
  exact (mem_vars_iff_mem_support v).mpr ⟨x, H, Finsupp.mem_support_iff.mpr h⟩

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
x : σ
hx : x ∈ (p + q).vars
⊢ x ∈ p.vars ∪ q.vars

Tactic:
simp only [vars_def, Finset.mem_union, Multiset.mem_toFinset] at hx ⊢

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
x : σ
hx : x ∈ (p + q).degrees
⊢ x ∈ p.degrees ∨ x ∈ q.degrees
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
p : MvPolynomial σ R
n : ℕ
⊢ degreeOf i (p ^ n) ≤ n * degreeOf i p

Tactic:
by
  simpa using degreeOf_prod_le i (Finset.range n) (fun _ => p)

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

Goal state before:
pp: 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
d : σ →₀ ℕ
hd : d ∈ p.support
⊢ ¬d.support = ∅

Tactic:
Finsupp.support_eq_empty

Goal state after:
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
d : σ →₀ ℕ
hd : d ∈ p.support
⊢ ¬d = 0
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: 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
d : σ →₀ ℕ
hd : d ∈ p.support
hd0 : d ≠ 0
⊢ ¬d.support = ∅

Tactic:
Finsupp.support_eq_empty

Goal state after:
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
d : σ →₀ ℕ
hd : d ∈ p.support
hd0 : d ≠ 0
⊢ ¬d = 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
⊢ #f.eraseLead.support < #f.support

Tactic:
rw [eraseLead_support]

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
⊢ #(f.support.erase f.natDegree) < #f.support
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: case refine_2.inr.inl
R : Type u
inst✝ : Semiring R
p : R[X]
h₁ : p.Monic
h : p.natDegree ≤ p.natTrailingDegree
⊢ p.coeff p.natDegree = if p.natDegree = p.natDegree then 1 else 0

pp: case refine_2.inr.inr
R : Type u
inst✝ : Semiring R
p : R[X]
h₁ : p.Monic
h : p.natDegree ≤ p.natTrailingDegree
n : ℕ
hn : p.natDegree < n
⊢ p.coeff n = if n = p.natDegree then 1 else 0

Tactic:
· simpa only [if_pos rfl] using! h₁.leadingCoeff

Goal state after:
case refine_2.inr.inr
R : Type u
inst✝ : Semiring R
p : R[X]
h₁ : p.Monic
h : p.natDegree ≤ p.natTrailingDegree
n : ℕ
hn : p.natDegree < n
⊢ p.coeff n = if n = p.natDegree then 1 else 0